Changeset 1680 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Feb 9, 2012, 1:22:28 PM (8 years ago)
Author:
campbell
Message:

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r1631 r1680  
    4343(* ident for returned value, expression to identify fn, args. *)
    4444| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     45(* We don't use these at the moment, and they're getting in the way.
    4546| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     47*)
    4648| St_seq : stmt → stmt → stmt
    4749| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
     
    8284| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    8385| 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(*
    8487| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     88*)
    8589| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    8690| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     
    113117| #t #r #q #e1 #e2 * /4/
    114118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     119(*
    115120| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     121*)
    116122| #s1 #s2 #H1 #H2 * /3/
    117123| #sz #sg #e #s1 #s2 #H1 #H2 /5/
    118 | 8,9: #s #H1 #H2 /2/
     124| 7,8: #s #H1 #H2 /2/
    119125| //
    120126| /5/
Note: See TracChangeset for help on using the changeset viewer.