Changeset 2645 for src/common


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/common
Files:
1 added
13 edited

Legend:

Unmodified
Added
Removed
  • 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 ≝
Note: See TracChangeset for help on using the changeset viewer.