Changeset 2232 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jul 23, 2012, 2:05:10 PM (7 years ago)
Author:
campbell
Message:

Remove unused block structure in Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r2176 r2232  
    4646| St_seq : stmt → stmt → stmt
    4747| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
    48 | St_loop : stmt → stmt
    49 | St_block : stmt → stmt
    50 | St_exit : nat → stmt
    51 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    52 | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    5348| St_return : option (𝚺t. expr t) → stmt
    5449| St_label : identifier Label → stmt → stmt
     
    6055[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    6156| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    62 | St_loop s' ⇒ P s ∧ stmt_P P s'
    63 | St_block s' ⇒ P s ∧ stmt_P P s'
    6457| St_label _ s' ⇒ P s ∧ stmt_P P s'
    6558| St_cost _ s' ⇒ P s ∧ stmt_P P s'
     
    7164[ #s1 #s2 * * /2/
    7265| #sz #sg #e #s1 #s2 * * /2/
    73 | 3,4: #s * /2/
    74 | 5,6: #i #s normalize * /2/
     66| *: #i #s normalize * /2/
    7567] qed.
    7668
     
    8678*)
    8779| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    88 | St_switch _ _ e _ _ ⇒ expr_vars ? e P
    8980| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
    9081| _ ⇒ True
     
    10394[ #s1 #s2 #H1 #H2 normalize * * /4/
    10495| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
    105 | #s #H * /5/
    106 | #s #H * /5/
    10796| #l #s #H * /5/
    10897| #l #s #H * /5/
     
    120109| #s1 #s2 #H1 #H2 * /3/
    121110| #sz #sg #e #s1 #s2 #H1 #H2 /5/
    122 | 7,8: #s #H1 #H2 /2/
    123 | //
    124 | /5/
    125111| * normalize [ // | *; normalize /3/ ]
    126112| /2/
     
    137123[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    138124| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    139 | St_loop s ⇒ labels_of s
    140 | St_block s ⇒ labels_of s
    141125| St_label l s ⇒ l::(labels_of s)
    142126| St_cost _ s ⇒ labels_of s
Note: See TracChangeset for help on using the changeset viewer.