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.