Changeset 2176 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r1878 r2176  
    99| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1010| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
    11 | Mem : ∀t,r. expr (ASTptr r) → expr t
     11| Mem : ∀t. expr ASTptr → expr t
    1212| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1313| Ecost : ∀t. costlabel → expr t → expr t.
     
    2020| Op1 _ _ _ e ⇒ expr_vars ? e P
    2121| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    22 | Mem _ _ e ⇒ expr_vars ? e P
     22| Mem _ e ⇒ expr_vars ? e P
    2323| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
    2424| Ecost _ _ e ⇒ expr_vars ? e P
     
    3838| St_skip : stmt
    3939| St_assign : ∀t. ident → expr t → stmt
    40 | St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
     40| St_store : ∀t. expr ASTptr → expr t → stmt
    4141(* ident for returned value, expression to identify fn, args. *)
    42 | St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     42| St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt
    4343(* We don't use these at the moment, and they're getting in the way.
    44 | St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     44| St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt
    4545*)
    4646| St_seq : stmt → stmt → stmt
     
    8080match s with
    8181[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    82 | St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     82| St_store _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    8383| 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
    8484(*
     
    113113[ //
    114114| #t #id #e * /4/
    115 | #t #r #e1 #e2 * /4/
     115| #t #e1 #e2 * /4/
    116116| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
    117117(*
Note: See TracChangeset for help on using the changeset viewer.