Changeset 1680 for src/RTLabs/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/RTLabs/syntax.ma

    r1675 r1680  
    1919| St_call_id : ident → list register → option register → label → statement
    2020| St_call_ptr : register → list register → option register → label → statement
     21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
    2122| St_tailcall_id : ident → list register → statement
    2223| St_tailcall_ptr : register → list register → statement
     24*)
    2325| St_cond : register → label → label → statement
    2426| St_jumptable : register → list label → statement
     
    4648| St_call_id _ _ _ l ⇒ P l
    4749| St_call_ptr _ _ _ l ⇒ P l
     50(*
    4851| St_tailcall_id _ _ ⇒ True
    4952| St_tailcall_ptr _ _ ⇒ True
     53*)
    5054| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
    5155| St_jumptable _ ls ⇒ All ? P ls
     
    105109| St_call_id _ _ _ l ⇒ [l]
    106110| St_call_ptr _ _ _ l ⇒ [l]
     111(*
    107112| St_tailcall_id _ _ ⇒ [ ]
    108113| St_tailcall_ptr _ _ ⇒ [ ]
     114*)
    109115| St_cond _ l1 l2 ⇒ [l1; l2]
    110116| St_jumptable _ ls ⇒ ls
Note: See TracChangeset for help on using the changeset viewer.