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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2601 r2645  
    8585definition var_types ≝ identifier_map SymbolTag (var_type × type).
    8686
    87 axiom UndeclaredIdentifier : String.
    88 
    8987definition lookup' ≝
    9088λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
     
    249247
    250248alias id "CMexpr" = "cic:/matita/cerco/Cminor/Cminor_syntax/expr.ind(1,0,0)".
    251 
    252 axiom BadlyTypedAccess : String.
    253 axiom BadLvalue : String.
    254 axiom MissingField : String.
    255249
    256250(* type_should_eq enforces that two types are equal and eliminates this equality by
     
    605599λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    606600*)
    607 axiom FIXME : String.
    608601
    609602(* Given a source and target type, translate an expession of type source to type target *)
     
    941934definition lenv ≝ identifier_map SymbolTag (identifier Label).
    942935
    943 axiom MissingLabel : String.
    944 
    945936(* Find the Cminor label corresponding to [l] or fail. *)
    946937definition lookup_label ≝
     
    11791170  return_ok rettyp s' ∧                           (* return statements have correct typ *)
    11801171  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
    1181 
    1182 axiom ReturnMismatch : String.
    11831172
    11841173let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
     
    15081497] qed.
    15091498
    1510 axiom ParamGlobalMixup : String.
    1511 
    15121499(* params and statement aren't real parameters, they're just there for giving the invariant. *)
    15131500definition alloc_params :
     
    15331520@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
    15341521qed.
    1535 
    1536 axiom DuplicateLabel : String.
    15371522
    15381523definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.