Changeset 764 for src/ASM/Util.ma


Ignore:
Timestamp:
Apr 20, 2011, 5:38:58 PM (9 years ago)
Author:
campbell
Message:

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r746 r764  
    8686 with precedence 10
    8787for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     88
     89(* Yeah, I probably ought to do something more general... *)
     90notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
     91with precedence 90 for @{ 'triple $a $b $c}.
     92interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
     93
     94notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
     95 with precedence 10
     96for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
    8897
    8998notation "⊥" with precedence 90
Note: See TracChangeset for help on using the changeset viewer.