Changeset 2645 for src/Cminor
 Timestamp:
 Feb 7, 2013, 9:22:22 PM (7 years ago)
 Location:
 src/Cminor
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/Cminor_semantics.ma
r2608 r2645 83 83 state 84 84 . 85 86 axiom UnknownLocal : String.87 axiom FailedConstant : String.88 axiom FailedOp : String.89 axiom FailedLoad : String.90 85 91 86 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝ … … 128 123 qed. 129 124 130 axiom BadState : String.131 132 125 let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝ 133 126 match k return λk.cont_inv f en k → ? with … … 225 218 qed. 226 219 227 axiom WrongNumberOfParameters : String.228 229 220 (* TODO: perhaps should do a little type checking? *) 230 221 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝ … … 279 270 ] p. 280 271 [ @(π1 p)  @(π2 p) ] qed. 281 282 axiom FailedStore : String.283 axiom BadFunctionValue : String.284 axiom ReturnMismatch : String.285 272 286 273 definition eval_step : genv → state → IO io_out io_in (trace × state) ≝ … … 428 415 mk_trans_system … ? (λ_.is_final) eval_step. 429 416 430 axiom MainMissing : String.431 432 417 definition make_global : Cminor_program → genv ≝ 433 418 λp. globalenv … (λx.x) p. 
src/Cminor/Cminor_syntax.ma
r2601 r2645 32 32  #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/ 33 33 ] qed. 34 35 axiom Label : String.36 34 37 35 inductive stmt : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.