Changeset 2645 for src/Cminor


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
Location:
src/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_semantics.ma

    r2608 r2645  
    8383            state
    8484.
    85 
    86 axiom UnknownLocal : String.
    87 axiom FailedConstant : String.
    88 axiom FailedOp : String.
    89 axiom FailedLoad : String.
    9085
    9186let 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) ≝
     
    128123qed.
    129124
    130 axiom BadState : String.
    131 
    132125let 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') ≝
    133126match k return λk.cont_inv f en k → ? with
     
    225218qed.
    226219
    227 axiom WrongNumberOfParameters : String.
    228 
    229220(* TODO: perhaps should do a little type checking? *)
    230221let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
     
    279270] p.
    280271[ @(π1 p) | @(π2 p) ] qed.
    281 
    282 axiom FailedStore : String.
    283 axiom BadFunctionValue : String.
    284 axiom ReturnMismatch : String.
    285272
    286273definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
     
    428415  mk_trans_system … ? (λ_.is_final) eval_step.
    429416
    430 axiom MainMissing : String.
    431 
    432417definition make_global : Cminor_program → genv ≝
    433418λp. globalenv … (λx.x) p.
  • src/Cminor/Cminor_syntax.ma

    r2601 r2645  
    3232| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
    3333] qed.
    34 
    35 axiom Label : String.
    3634
    3735inductive stmt : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.