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/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
Note: See TracChangeset for help on using the changeset viewer.