Changeset 2645


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (6 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
Files:
2 added
1 deleted
46 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2316 r2645  
    44include "common/LabelledObjects.ma".
    55
    6 axiom ASMTag : String.
    76definition Identifier ≝ identifier ASMTag.
    87definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
  • src/ASM/BitVector.ma

    r2601 r2645  
    1010include "ASM/FoldStuff.ma".
    1111include "ASM/Vector.ma".
    12 include "ASM/String.ma".
    1312
    1413(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    226225qed.
    227226
    228 (*
    229 axiom bitvector_of_string:
    230   ∀n: nat.
    231   ∀s: String.
    232     BitVector n.
    233    
    234 axiom string_of_bitvector:
    235   ∀n: nat.
    236   ∀b: BitVector n.
    237     String.
    238 *)
    239 
    240227lemma bitvector_3_cases:
    241228  ∀w: BitVector 3.
  • src/ASM/I8051.ma

    r2286 r2645  
    11include "arithmetics/nat.ma".
    22include "basics/jmeq.ma".
    3 
    4 include "ASM/String.ma".
    5 (*include "ASM/ASM.ma".*)
    63include "ASM/Arithmetic.ma". 
    74
     
    104101    eqb r_as_nat s_as_nat.
    105102
    106 axiom print_register: Register → String.
    107 
    108103(* dpm: registers for stack manipulation *)
    109104definition RegisterSST ≝ Register10.
  • src/Clight/Cexec.ma

    r2608 r2645  
    99definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    1010  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
    11 
    12 axiom ValueIsNotABoolean : String.
    1311
    1412definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
     
    6462#A #B #P #m #e #f elim e; normalize; /2/; qed.
    6563
    66 
    67 axiom BadCast : String. (* TODO: refine into more precise errors? *)
    6864
    6965definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
     
    151147definition load_value_of_type' ≝
    152148λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
    153 
    154 axiom BadlyTypedTerm : String.
    155 axiom UnknownIdentifier : String.
    156 axiom BadLvalueTerm : String.
    157 axiom FailedLoad : String.
    158 axiom FailedOp : String.
    159149
    160150(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    317307].
    318308
    319 axiom WrongNumberOfParameters : String.
    320 axiom FailedStore : String.
    321 
    322309(* TODO: can we establish that length params = length vs in advance? *)
    323310let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
     
    358345let 〈loc,ofs〉 ≝ l in
    359346  store_value_of_type ty m loc ofs v.
    360 
    361 axiom NonsenseState : String.
    362 axiom ReturnMismatch : String.
    363 axiom UnknownLabel : String.
    364 axiom BadFunctionValue : String.
    365347
    366348let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
     
    531513].
    532514
    533 axiom MainMissing : String.
    534 
    535515definition make_global : clight_program → genv ≝
    536516λp. globalenv … (fst ??) p.
  • src/Clight/Csyntax.ma

    r2468 r2645  
    496496Open Local Scope string_scope.
    497497*)
    498 axiom UnknownField : String.
    499498
    500499let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
  • src/Clight/TypeComparison.ma

    r2468 r2645  
    22include "Clight/Csyntax.ma".
    33include "utilities/extranat.ma".
    4 
    5 axiom TypeMismatch : String.
    64
    75definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
  • src/Clight/test/addptrcharboth.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/badconditional.test.ma

    r2619 r2645  
    3939include "RTLabs/CostCheck.ma".
    4040
    41 axiom MISSING:String.
    42 axiom EXTERNAL:String.
    43 
    4441definition readable_body ≝
    4542λfn. insert_sort ?
  • src/Clight/test/controlflow.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/endptr.test.ma

    r2619 r2645  
    3333
    3434include "RTLabs/CostCheck.ma".
    35 
    36 axiom MISSING:String.
    37 axiom EXTERNAL:String.
    3835
    3936definition readable_body ≝
  • src/Clight/test/endptr2.test.ma

    r2619 r2645  
    3333
    3434include "RTLabs/CostCheck.ma".
    35 
    36 axiom MISSING:String.
    37 axiom EXTERNAL:String.
    3835
    3936definition readable_body ≝
  • src/Clight/test/forcont.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/goto-if.test.ma

    r2619 r2645  
    4545include "RTLabs/CostCheck.ma".
    4646
    47 axiom MISSING:String.
    48 axiom EXTERNAL:String.
    49 
    5047definition readable_body ≝
    5148λfn. insert_sort ?
  • src/Clight/test/implicit.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/implicitcond.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/sum.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/trivial.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • 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 ≝
  • 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] ≝
  • src/ERTL/ERTL.ma

    r2604 r2645  
    9797definition ertl_seq_joint ≝ extension_seq ERTL.
    9898coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
    99   on _s : ertl_seq to joint_seq ERTL.
     99  on _s : ertl_seq to joint_seq ERTL ?.
  • src/ERTLptr/ERTLptr.ma

    r2604 r2645  
    2929definition ertlptr_seq_joint ≝ extension_seq ERTLptr.
    3030coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint
    31   on _s : ertlptr_seq to joint_seq ERTLptr.
     31  on _s : ertlptr_seq to joint_seq ERTLptr ?.
    3232 
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2638 r2645  
    288288
    289289definition map_inf1 :  ∀A, B: Type[0].
    290   ∀tag: String.
     290  ∀tag: identifierTag.
    291291  ∀m:identifier_map tag A.
    292292   (∀a:A.(Σid. lookup tag A m id = Some A a) → B) →
     
    311311
    312312lemma map_inf_add : ∀ A, B : Type[0].
    313   ∀tag : String.
     313  ∀tag : identifierTag.
    314314  ∀m: identifier_map tag A.
    315315  ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    365365                                    id_is_in A (p1 x) (pm_node … opt_a l r).
    366366
    367 definition id_is_in : ∀A : Type[0]. ∀tag : String.
     367definition id_is_in : ∀A : Type[0]. ∀tag : identifierTag.
    368368identifier_map tag A → identifier tag → Prop ≝
    369369λA,tag,m,id.match id with
     
    373373(*
    374374lemma lookup_map : ∀A,B : Type[0].
    375   ∀tag : String.
     375  ∀tag : identifierTag.
    376376  ∀m : identifier_map tag A.
    377377  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    400400(*
    401401lemma lookup_map_weak : ∀ A,B : Type[0].
    402   ∀tag : String.
     402  ∀tag : identifierTag.
    403403  ∀m : identifier_map tag A.
    404404  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    410410
    411411lemma lookup_map_fail : ∀A,B : Type[0].
    412 ∀tag : String.
     412∀tag : identifierTag.
    413413  ∀m : identifier_map tag A.
    414414  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    464464
    465465lemma lookup_ok_to_update : ∀ A : Type[0].
    466 ∀ tag : String.
     466∀ tag : identifierTag.
    467467∀m,m' : identifier_map tag A. ∀id,a.
    468468(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? →
     
    531531
    532532lemma update_ok_to_lookup : ∀ A : Type[0].
    533 ∀ tag : String.
     533∀ tag : identifierTag.
    534534∀m,m' : identifier_map tag A. ∀id,a.
    535535update tag A m id a = return m' →
     
    585585               
    586586lemma update_lookup_after : ∀ A : Type[0].
    587 ∀ tag : String.
     587∀ tag : identifierTag.
    588588∀m,m' : identifier_map tag A. ∀id,a.
    589589update tag A m id a = return m' →
     
    602602qed.
    603603
    604 lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : String.
     604lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : identifierTag.
    605605∀m : identifier_map tag A.
    606606∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    628628
    629629lemma map_update_commute : ∀ A, B : Type[0].
    630 ∀tag : String.
     630∀tag : identifierTag.
    631631∀m1,m2 : identifier_map tag A.
    632632∀id,a.
     
    680680
    681681lemma lookup_map : ∀A,B : Type[0].
    682   ∀tag : String.
     682  ∀tag : identifierTag.
    683683  ∀m : identifier_map tag A.
    684684  ∀ f:A → B.
     
    723723qed.
    724724
    725 lemma map_add : ∀tag : String.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
     725lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
    726726map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
    727727#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
     
    754754unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
    755755 
    756 lemma map_update_commute : ∀tag : String.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
     756lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
    757757update tag B (map tag A B m f) id (f v) =
    758758!m' ← update tag A m id v; return map tag A B m' f.
     
    857857qed.
    858858*)
    859 lemma lookup_eq_id_map : ∀tag : String. ∀ A : Type[0].
     859lemma lookup_eq_id_map : ∀tag : identifierTag. ∀ A : Type[0].
    860860∀m,m' : identifier_map tag A.
    861861(∀id. lookup … m id = lookup … m' id
     
    866866
    867867(*
    868 lemma clean_leaf : ∀tag : String . ∀ A : Type[0].
     868lemma clean_leaf : ∀tag : identifierTag . ∀ A : Type[0].
    869869∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) →
    870870clean ?? m = empty_map ??.
  • src/LIN/joint_LTL_LIN.ma

    r2537 r2645  
    3636    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
    3737    (* has_tailcalls ≝ *) false
    38     (* paramsT ≝ *) unit
    39     (* localsT ≝ *) void.
     38    (* paramsT ≝ *) unit.
    4039
    4140interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2443 r2645  
    11include "LIN/joint_LTL_LIN.ma".
    2 include "joint/SemanticUtils.ma".
     2include "joint/semanticsUtils.ma".
    33
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
     
    77  λl,a.match a with
    88  [ Reg r ⇒ hw_reg_retrieve l r
    9   | Imm b ⇒ OK … b
     9  | Imm b ⇒ OK … (BVByte b)
    1010  ].
    1111
     
    1717  hw_reg_store RegisterA (hwreg_retrieve e r) e
    1818| int_to_reg r v ⇒
    19   hw_reg_store r v e
     19  hw_reg_store r (BVByte v) e
    2020| int_to_acc _ v ⇒
    21   hw_reg_store RegisterA v e
     21  hw_reg_store RegisterA (BVByte v) e
    2222].
    2323
     
    5555  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
    5656  (* pair_reg_move_     ≝ *) eval_registers_move
    57   (* fetch_ra           ≝ *) (load_ra …)
     57(*  (* fetch_ra           ≝ *) (load_ra …)
    5858  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    59   (* save_frame         ≝ *) (λp.λ_.λst.save_ra … st p)
     59*)  (* save_frame         ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*)
    6060  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
    61   (* fetch_external_args≝ *) ltl_lin_fetch_external_args
     61  (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
    6262  (* set_result         ≝ *) ltl_lin_set_result
    6363  (* call_args_for_main ≝ *) 0
     
    6565  (* read_result        ≝ *) (λ_.λ_.λ_.
    6666  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    67   (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
    68   (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     67  (* eval_ext_seq       ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*)
     68(*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
    6969  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    70   (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
    71   (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
     70*)  (* pop_frame          ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*)
     71(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
  • src/RTL/RTL_semantics.ma

    r2601 r2645  
    1 include "joint/SemanticUtils.ma".
     1include "joint/semanticsUtils.ma".
    22include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    33include alias "common/Identifiers.ma".
     
    2626
    2727(*CSC: could we use here a dependent type to avoid the Error case? *)
    28 axiom EmptyStack: String.
    29 axiom OutOfBounds: String.
    3028
    3129definition rtl_fetch_ra:
  • src/RTLabs/RTLabs_semantics.ma

    r2608 r2645  
    5959  update RegisterTag val locals reg v.
    6060
    61 axiom WrongNumberOfParameters : String.
    62 
    6361let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    6462match rs with
     
    7068] ].
    7169
    72 axiom BadRegister : String.
    7370
    7471definition reg_retrieve : register_env ? → register → res val ≝
    7572λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    76 
    77 axiom FailedOp : String.
    78 axiom MissingSymbol : String.
    79 
    80 axiom MissingStatement : String.
    81 axiom FailedConstant : String.
    82 axiom FailedLoad : String.
    83 axiom FailedStore : String.
    84 axiom BadFunction : String.
    85 axiom BadJumpTable : String.
    86 axiom BadJumpValue : String.
    87 axiom FinalState : String.
    88 axiom ReturnMismatch : String.
    8973
    9074definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
  • src/RTLabs/import.ma

    r2601 r2645  
    22include "RTLabs/RTLabs_semantics.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
     4let rec n_idents (n:nat) (tag:identifierTag) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
    55match n with
    66[ O ⇒ 〈[[ ]], g〉
     
    4242                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
    4343                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    44 
    45 axiom MissingRegister : String.
    46 axiom MissingLabel : String.
    4744
    4845(* Doesn't check for identifier overflow, but don't really need to care here. *)
     
    124121.
    125122
    126 axiom TypeMismatch : String.
    127 
    128123(* duplicated from Clight/toCminor.ma. *)
    129124definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
  • src/common/AST.ma

    r2624 r2645  
    2828   tag for symbols.  Note that Clight also uses them for locals due to
    2929   the ambiguous syntax. *)
    30 
    31 axiom SymbolTag : String.
    3230
    3331definition ident ≝ identifier SymbolTag.
  • src/common/Animation.ma

    r2533 r2645  
    1919| finished : trace → int → state → snapshot state
    2020| input_exhausted : trace → snapshot state.
    21 
    22 axiom StoppedMidIO : String.
    2321
    2422let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝
  • src/common/BackEndOps.ma

    r2548 r2645  
    3535          op1_implementation
    3636          op2_implementation.
    37 
    38 axiom UnsupportedOp : String.
    3937
    4038definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
  • src/common/ByteValues.ma

    r2608 r2645  
    110110
    111111include alias "arithmetics/nat.ma".
    112 
    113 axiom CorruptedPointer: String.
    114112
    115113(* CSC: use vectors in place of lists? Or even better products of tuples
     
    203201qed.
    204202
    205 axiom NotATwoBytesPointer: String.
    206 
    207203(* Should fail if the address is not representable as a pair
    208204   As we only have 16 bit addresses atm, it never fails *)
     
    219215 λp. list_to_pair ? (bevals_of_pc p) (refl …).
    220216
    221 (* axiom NotACodePointer: String.
     217(*
    222218definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
    223219 λp.
     
    227223  [ Code ⇒ λE.OK ? (mk_Sig … p E)
    228224  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
    229 
    230 axiom ValueNotABoolean: String.
    231225
    232226definition bool_of_beval: beval → res bool ≝
     
    244238  ].
    245239
    246 definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
     240definition Byte_of_val: ErrorMessage → beval → res Byte ≝ (*CSC: move elsewhere *)
    247241 λerr,b.match b with
    248242  [ BVByte b ⇒ OK … b
    249243  | _ ⇒ Error … [MSG err]].
    250244
    251 axiom NotAnInt32Val: String.
    252245definition Word_of_list_beval: list beval → res int ≝
    253246 λl.
     
    270263  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
    271264
    272 definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
     265definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
    273266 λerr,b.match b with
    274267  [ BBbit b ⇒ OK … b
  • src/common/CostLabel.ma

    r1268 r2645  
    11include "common/AST.ma".
    2 
    3 axiom CostTag : String.
    42
    53definition costlabel ≝ identifier CostTag.
  • src/common/Errors.ma

    r2500 r2645  
    66include "utilities/monad.ma".
    77include "utilities/option.ma".
     8include "common/ErrorMessages.ma".
    89
    910(* * Error reporting and the error monad. *)
     
    1617
    1718inductive errcode: Type[0] :=
    18   | MSG: String → errcode
    19   | CTX: ∀tag:String. identifier tag → errcode.
     19  | MSG: ErrorMessage → errcode
     20  | CTX: ∀tag:identifierTag. identifier tag → errcode.
    2021
    2122definition errmsg: Type[0] ≝ list errcode.
    2223
    23 definition msg : String → errmsg ≝ λs. [MSG s].
     24definition msg : ErrorMessage → errmsg ≝ λs. [MSG s].
    2425
    2526(* * * The error monad *)
     
    137138
    138139(* A monadic fold_left2 *)
    139 
    140 axiom WrongLength: String.
    141140
    142141let rec mfold_left2
  • src/common/Globalenvs.ma

    r2624 r2645  
    274274
    275275(* init *)
    276 
    277 axiom InitDataStoreFailed : String.
    278276
    279277definition add_globals : ∀F,V:Type[0].
     
    11361134] qed.
    11371135
    1138 record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     1136record related_globals_gen (tag:identifierTag) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
    11391137  rgg_find_symbol: ∀s.
    11401138    find_symbol … ge s = find_symbol … ge' s;
  • src/common/Graphs.ma

    r1882 r2645  
    44include "common/Identifiers.ma".
    55include "common/AST.ma".
    6 
    7 axiom LabelTag : String.
    86
    97definition label ≝ identifier LabelTag.
  • src/common/IO.ma

    r2468 r2645  
    1919  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    2020#ty cases ty; normalize; // * *; qed.
    21 
    22 axiom IllTypedEvent : String.
    2321
    2422definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
  • src/common/Identifiers.ma

    r2599 r2645  
    11include "basics/types.ma".
    2 include "ASM/String.ma".
    32include "utilities/binary/positive.ma".
    43include "utilities/lists.ma".
     
    109
    1110(* in common/PreIdentifiers.ma, via Errors.ma.
    12 inductive identifier (tag:String) : Type[0] ≝
     11inductive identifier (tag:identifierTag) : Type[0] ≝
    1312  an_identifier : Pos → identifier tag.
    1413*)
    1514
    16 record universe (tag:String) : Type[0] ≝
     15record universe (tag:identifierTag) : Type[0] ≝
    1716{
    1817  next_identifier : Pos
    1918}.
    2019
    21 definition new_universe : ∀tag:String. universe tag ≝
     20definition new_universe : ∀tag:identifierTag. universe tag ≝
    2221  λtag. mk_universe tag one.
    2322
    24 let rec fresh (tag:String) (u:universe tag) on u : identifier tag × (universe tag) ≝
     23let rec fresh (tag:identifierTag) (u:universe tag) on u : identifier tag × (universe tag) ≝
    2524  let id ≝ next_identifier ? u in
    2625  〈an_identifier tag id, mk_universe tag (succ id)〉.
     
    8281
    8382lemma eq_identifier_eq:
    84   ∀tag: String.
     83  ∀tag: identifierTag.
    8584  ∀l.
    8685  ∀r.
     
    104103
    105104axiom neq_identifier_neq:
    106   ∀tag: String.
     105  ∀tag: identifierTag.
    107106  ∀l, r: identifier tag.
    108107    eq_identifier tag l r = false → (l = r → False).
    109108
    110109include "basics/deqsets.ma".
    111 definition Deq_identifier : String → DeqSet ≝ λtag.
     110definition Deq_identifier : identifierTag → DeqSet ≝ λtag.
    112111  mk_DeqSet (identifier tag) (eq_identifier tag) ?.
    113112#x#y @eq_identifier_elim /2 by conj/ * #H % [#ABS destruct(ABS) | #G elim (H G)]
     
    130129
    131130axiom eq_identifier_sym:
    132   ∀tag: String.
     131  ∀tag: identifierTag.
    133132  ∀l  : identifier tag.
    134133  ∀r  : identifier tag.
     
    139138qed.
    140139
    141 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
     140definition identifier_eq : ∀tag:identifierTag. ∀x,y:identifier tag. (x=y) + (x≠y).
    142141#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
    143142#E [ % | %2 ]
     
    146145qed.
    147146
    148 definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
     147definition identifier_of_nat : ∀tag:identifierTag. nat → identifier tag ≝
    149148  λtag,n. an_identifier tag (succ_pos_of_nat  n).
    150149
     
    172171(* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that
    173172   the original environment was distinct. *)
    174 
    175 axiom DuplicateVariable : String.
    176173
    177174let rec check_member_env tag (A:Type[0]) (id:identifier tag) (l:list (identifier tag × A)) on l : res (All ? (λia. id ≠ \fst ia) l) ≝
     
    203200include "common/PositiveMap.ma".
    204201
    205 inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
     202inductive identifier_map (tag:identifierTag) (A:Type[0]) : Type[0] ≝
    206203  an_id_map : positive_map A → identifier_map tag A.
    207204 
    208 definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
     205definition empty_map : ∀tag:identifierTag. ∀A. identifier_map tag A ≝
    209206  λtag,A. an_id_map tag A (pm_leaf A).
    210207
     
    315312
    316313
    317 axiom MissingId : String.
    318 
    319314(* Only updates an existing entry; fails with an error otherwise. *)
    320315definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
     
    349344definition foldi:
    350345  ∀A, B: Type[0].
    351   ∀tag: String.
     346  ∀tag: identifierTag.
    352347  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
    353348λA,B,tag,f,m,b.
     
    359354definition fold_inf:
    360355  ∀A, B: Type[0].
    361   ∀tag: String.
     356  ∀tag: identifierTag.
    362357  ∀m:identifier_map tag A.
    363358  (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B ≝
     
    620615  λtag,s,i.add … s i it.
    621616
    622 definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
     617definition singleton_set : ∀tag:identifierTag. identifier tag → identifier_set tag ≝
    623618λtag,i. add_set tag (empty_set tag) i.
    624619
    625 let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
     620let rec union_set (tag:identifierTag) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
    626621  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
    627622    (match s with [ an_id_map s0 ⇒ s0 ])
     
    630625
    631626(* set minus is generalised to maps *)
    632 let rec minus_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝
     627let rec minus_set (tag:identifierTag) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝
    633628  an_id_map tag A (merge A B A (λo,o'.match o' with [None ⇒ o | Some _ ⇒ None ?])
    634629    (match s with [ an_id_map s0 ⇒ s0 ])
     
    643638interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
    644639
    645 definition IdentifierSet : String → Setoid ≝ λtag.
     640definition IdentifierSet : identifierTag → Setoid ≝ λtag.
    646641  mk_Setoid (identifier_set tag) (λs,s'.∀i.i ∈ s = (i ∈ s')) ???.
    647642  // qed.
     
    737732
    738733
    739 definition id_map_size : ∀tag : String.∀A. identifier_map tag A → ℕ ≝
     734definition id_map_size : ∀tag : identifierTag.∀A. identifier_map tag A → ℕ ≝
    740735  λtag,A,s.match s with [an_id_map p ⇒ |p|].
    741736
  • src/common/PreIdentifiers.ma

    r1515 r2645  
    66
    77include "basics/types.ma".
    8 include "ASM/String.ma".
    98include "utilities/binary/positive.ma".
    109
     
    1211   provide extra type checking. *)
    1312
    14 inductive identifier (tag:String) : Type[0] ≝
     13inductive identifierTag: Type[0] ≝
     14   Label : identifierTag
     15 | CostTag : identifierTag
     16 | RegisterTag : identifierTag
     17 | LabelTag : identifierTag
     18 | SymbolTag : identifierTag.
     19
     20inductive identifier (tag:identifierTag) : Type[0] ≝
    1521  an_identifier : Pos → identifier tag.
  • src/common/Registers.ma

    r2603 r2645  
    66(*include "ASM/I8051.ma".*)
    77include "common/Order.ma".
    8 
    9 axiom RegisterTag : String.
    108
    119definition register ≝ identifier RegisterTag.
  • src/common/Values.ma

    r2468 r2645  
    9292  | bool_of_val_null:
    9393      bool_of_val Vnull true.
    94 
    95 axiom ValueNotABoolean : String.
    9694
    9795definition eval_bool_of_val : val → res bool ≝
  • src/compiler.ma

    r2581 r2645  
    4949(* include "ASM/Policy.ma".
    5050
    51 axiom Jump_expansion_failed : String.
    52 
    5351definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
    5452λp.
  • src/joint/Joint.ma

    r2595 r2645  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "joint/String.ma".
    910
    1011(* Here is the structure of parameter records (downward edges are coercions,
     
    108109  | extension_seq : ext_seq p → joint_seq p globals.
    109110
    110 axiom EmptyString : String.
    111111definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
    112112
  • src/joint/String.ma

    r2643 r2645  
    1 include "basics/lists/list.ma".
     1include "basics/pts.ma".
    22
    3 include "ASM/Char.ma".
    4 
    5 definition String ≝ list Char.
     3(* Stupid definition, just to avoid an axiom in the extracted code *)
     4(* Strings at the moment are only used in comments in the back-end *)
     5axiom String: Type[0] ≝
     6   EmptyString : String.
  • src/joint/Traces.ma

    r2642 r2645  
    6666coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
    6767≝ make_global on _p : prog_params to evaluation_params.
    68 
    69 axiom BadMain : String.
    7068
    7169definition make_initial_state :
  • src/joint/joint_semantics.ma

    r2641 r2645  
    3939| both_is : beval → beval → internal_stack.
    4040
    41 axiom InternalStackFull : String.
    42 axiom InternalStackEmpty : String.
    43 
    4441definition is_push : internal_stack → beval → res internal_stack ≝
    4542λis,bv.match is with
     
    108105 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
    109106
    110 axiom BadProgramCounter : String.
    111 
    112107(*
    113108inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     
    122117  | FEnd2  : fin_step_flow p F Call. (* end flow *)
    123118*)
    124 
    125 axiom ProgramCounterOutOfCode : String.
    126 axiom PointNotFound : String.
    127 axiom LabelNotFound : String.
    128 axiom MissingSymbol : String.
    129 axiom FailedLoad : String.
    130 axiom BadFunction : String.
    131 axiom SuccessorNotProvided : String.
    132 axiom BadPointer : String.
    133119
    134120(* this can replace graph_fetch function and lin_fetch_function *)
     
    256242    return set_regs ? r st.
    257243 
    258 axiom FailedStore: String.
    259 
    260244definition push: ∀p.state p → beval → res (state p) ≝
    261245 λp,st,v.
     
    402386 set_pc … newpc st.
    403387
    404 axiom NoSuccessor : String.
    405388definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
    406389  program_counter → res (succ p) ≝
     
    524507      set_result … p vs dest st.
    525508
    526 axiom MissingStackSize : String.
    527 
    528509definition eval_internal_call ≝
    529510λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
     
    691672% qed.
    692673
    693 axiom ExternalMain: String.
    694 
    695674definition make_initial_state :
    696675 ∀pars: sem_params.
  • src/joint/semanticsUtils.ma

    r2601 r2645  
    4646; stackp : xpointer
    4747}.
    48 
    49 axiom BadRegister : String.
    5048
    5149definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
Note: See TracChangeset for help on using the changeset viewer.