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

Remove unused block structure in Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r2176 r2232  
    159159    | Some sk ⇒ Some ? sk
    160160    ]
    161 | St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
    162 | St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
    163161| St_label l' s' ⇒ λInv.
    164162    match identifier_eq ? l l' with
     
    173171try @(π2 (π1 Inv))
    174172[ % [ @(π2 Inv) | @kInv ]
    175 | % [ @Inv | @kInv ]
    176173| % [ @(π2 Inv) | @kInv ]
    177174] qed.
     
    208205  | #sk #_ #E whd in E:(??%?); destruct
    209206  ]
    210 | #s1 #IH #k #f #en #Inv #kInv @IH
    211 | #s1 #IH #k #f #en #Inv #kInv @IH
    212207| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
    213208  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     
    286281axiom FailedStore : String.
    287282axiom BadFunctionValue : String.
    288 axiom BadSwitchValue : String.
    289 axiom UnknownLabel : String.
    290283axiom ReturnMismatch : String.
    291284
     
    329322        ! b ← eval_bool_of_val v;
    330323        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
    331     | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
    332     | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
    333     | St_exit n ⇒ λInv.
    334         ! k' ← k_exit n k ?? kInv;
    335         return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    336     | St_switch sz _ e cs default ⇒ λInv.
    337         ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    338         match v with
    339         [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    340             ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
    341             return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    342             (Error ? (msg BadSwitchValue))
    343         | _ ⇒ Error ? (msg BadSwitchValue)
    344         ]
    345324    | St_return eo ⇒
    346325        match eo return λeo. stmt_inv f en (St_return eo) → ? with
     
    411390| @(π2 Inv')
    412391| @(π1 Inv')
    413 | @(pi2 … k')
    414 | @(pi2 … k')
    415 | % [ @Inv | @kInv ]
    416392| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    417393| % [ @(π2 Inv) | @kInv ]
    418394| @stmt_inv_update @fInv
    419 | 10,11:
     395| 7,8:
    420396  @(stmt_P_mp … (f_inv f))
    421397  #s * #V #L %
Note: See TracChangeset for help on using the changeset viewer.