Changeset 1872 for src/Cminor/syntax.ma
 Timestamp:
 Apr 4, 2012, 6:48:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/syntax.ma
r1680 r1872 10 10  Cst : ∀t. constant → expr t 11 11  Op1 : ∀t,t'. unary_operation t t' → expr t → expr t' 12  Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'13  Mem : ∀t,r. memory_chunk →expr (ASTptr r) → expr t12  Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t' 13  Mem : ∀t,r. expr (ASTptr r) → expr t 14 14  Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t 15 15  Ecost : ∀t. costlabel → expr t → expr t. … … 22 22  Op1 _ _ _ e ⇒ expr_vars ? e P 23 23  Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 24  Mem _ _ _e ⇒ expr_vars ? e P24  Mem _ _ e ⇒ expr_vars ? e P 25 25  Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P 26 26  Ecost _ _ e ⇒ expr_vars ? e P … … 40 40  St_skip : stmt 41 41  St_assign : ∀t. ident → expr t → stmt 42  St_store : ∀t,r. memory_chunk →expr (ASTptr r) → expr t → stmt42  St_store : ∀t,r. expr (ASTptr r) → expr t → stmt 43 43 (* ident for returned value, expression to identify fn, args. *) 44 44  St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt … … 82 82 match s with 83 83 [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P 84  St_store _ _ _e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P84  St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 85 85  St_call oi e es ⇒ match oi with [ None ⇒ True  Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es 86 86 (* … … 115 115 [ // 116 116  #t #id #e * /4/ 117  #t #r # q #e1 #e2 * /4/117  #t #r #e1 #e2 * /4/ 118 118  * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/  *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 119 119 (*
Note: See TracChangeset
for help on using the changeset viewer.