Changeset 1515 for src/common


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
Location:
src/common
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r1253 r1515  
    2626  λseed: B.
    2727  match graph with
    28   [ an_id_map map ⇒ fold A B 16 f map seed
     28  [ an_id_map map ⇒ fold A B f map seed
    2929  ].
    3030
  • src/common/Identifiers.ma

    r1316 r1515  
    11include "basics/types.ma".
    22include "ASM/String.ma".
    3 include "ASM/Arithmetic.ma".
     3include "utilities/binary/positive.ma".
    44include "common/Errors.ma".
    55include "utilities/option.ma".
     
    1010(* in common/PreIdentifiers.ma, via Errors.ma.
    1111inductive identifier (tag:String) : Type[0] ≝
    12   an_identifier : Word → identifier tag.
     12  an_identifier : Pos → identifier tag.
    1313*)
    1414
    1515record universe (tag:String) : Type[0] ≝
    1616{
    17   next_identifier : Word;
    18   counter_overflow: bool
     17  next_identifier : Pos
    1918}.
    2019
    2120definition new_universe : ∀tag:String. universe tag ≝
    22   λtag. mk_universe tag (zero ?) false.
     21  λtag. mk_universe tag one.
    2322
    2423(* Fresh identifier generation uses delayed overflow checking.  To make sure
     
    2827  λtag.
    2928  λuniv: universe tag.
    30   let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
    31     if get_index_v … carries 0 ? then
    32       〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
    33     else
    34       〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
    35   //
    36 qed.
    37 
    38 axiom TooManyIdentifiers : String.
    39 
    40 definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
    41   λtag, univ.
    42   if counter_overflow ? univ
    43   then Error ? (msg TooManyIdentifiers)
    44   else OK ? it.
     29  let id ≝ next_identifier ? univ in
     30  〈an_identifier tag id, mk_universe tag (succ id)〉.
    4531
    4632definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    5036    match r with
    5137    [ an_identifier r' ⇒
    52       eq_bv ? l' r'
     38      eqb l' r'
    5339    ]
    5440  ].
     
    5844  P (eq_identifier t x y).
    5945#P #t * #x * #y #T #F
    60 change with (P (eq_bv ???))
    61 @eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
     46change with (P (eqb ??))
     47@(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
    6248qed.
    6349   
     
    6955  ].
    7056
     57lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
     58#tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
     59qed.
     60
     61lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
     62#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     63qed.
     64
    7165definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    72 #tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
     66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
    7367#E [ % | %2 ]
    74 lapply E @eq_bv_elim
     68lapply E @eqb_elim
    7569[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
    7670qed.
    7771
    7872definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
    79   λtag,n. an_identifier tag (bitvector_of_nat ? n).
     73  λtag,n. an_identifier tag (succ_pos_of_nat n).
    8074
    8175
    8276(* Maps from identifiers to arbitrary types. *)
    8377
    84 include "ASM/BitVectorTrie.ma".
     78include "common/PositiveMap.ma".
    8579
    8680inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
    87   an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     81  an_id_map : positive_map A → identifier_map tag A.
    8882 
    8983definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    90   λtag,A. an_id_map tag A (Stub A 16).
    91 
    92 definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
    93   λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
    94                               (match m with [ an_id_map m' ⇒ m' ]).
     84  λtag,A. an_id_map tag A (pm_leaf A).
     85
     86let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
     87  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
     88               (match m with [ an_id_map m' ⇒ m' ]).
     89
     90definition lookup_def ≝
     91λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
     92
     93let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
     94  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
    9595
    9696(* Always adds the identifier to the map. *)
    97 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
    98 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    99                                            (match m with [ an_id_map m' ⇒ m' ])).
     97let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
     98  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
     99                            (match m with [ an_id_map m' ⇒ m' ])).
    100100
    101101lemma lookup_add_hit : ∀tag,A,m,i,a.
     
    106106
    107107lemma lookup_add_miss : ∀tag,A,m,i,j,a.
    108   (notb (eq_identifier tag i j))
     108  i ≠ j
    109109  lookup tag A (add tag A m j a) i = lookup tag A m i.
    110 #tag #A * #m * #i * #j #a
    111 change with (notb (eq_bv ???) → ?)
    112 @lookup_opt_insert_miss
     110#tag #A * #m * #i * #j #a #H
     111@lookup_opt_insert_miss /2/
    113112qed.
    114113
     
    117116  lookup tag A (add tag A m j a) i ≠ None ?.
    118117#tag #A #m #i #j #a #H
    119 lapply (lookup_add_miss … m i j a)
    120 @eq_identifier_elim
    121 [ #E #_ >E >lookup_add_hit % #N destruct
    122 | #_ #H' >H' //
     118cases (identifier_eq ? i j)
     119[ #E >E >lookup_add_hit % #N destruct
     120| #NE >lookup_add_miss //
    123121] qed.
    124122
     
    129127cases (identifier_eq ? i j)
    130128[ #E >E >lookup_add_hit #H %1 destruct % //
    131 | #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     129| #NE >lookup_add_miss /2/
    132130] qed.
    133131
     
    135133definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
    136134λtag,A,m.
    137   fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
    138            (match m with [ an_id_map m' ⇒ m' ]) [ ].
     135  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
     136          (match m with [ an_id_map m' ⇒ m' ]) [ ].
    139137
    140138axiom MissingId : String.
     
    143141definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
    144142λtag,A,m,l,a.
    145   match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    146                     (match m with [ an_id_map m' ⇒ m' ]) with
     143  match update A (match l with [ an_identifier l' ⇒ l' ]) a
     144                 (match m with [ an_id_map m' ⇒ m' ]) with
    147145  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
    148146  | Some m' ⇒ OK ? (an_id_map tag A m')
     
    155153λA,B,tag,f,m,b.
    156154  match m with
    157   [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
     155  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
    158156
    159157(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     
    162160definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
    163161λtag,A,m,i. lookup … m i ≠ None ?.
     162
     163lemma member_present : ∀tag,A,m,id.
     164  member tag A m id = true → present tag A m id.
     165#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
     166[ #E destruct
     167| #x #E % #E' destruct
     168] qed.
     169
     170include "ASM/Util.ma".
    164171
    165172definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     
    171178  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
    172179  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
    173   let u' ≝ update A 16 l' a m' in
    174   match u' return λx. update ????? = x → ? with
     180  let u' ≝ update A l' a m' in
     181  match u' return λx. update ???? = x → ? with
    175182  [ None ⇒ λE.⊥
    176183  | Some m' ⇒ λ_. an_id_map tag A m'
    177184  ] (refl ? u').
    178 whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
    179 cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
     185cases l in p E; cases m; -l' -m' #m' #l'
     186whd in ⊢ (% → ?)
     187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
    180188#NL #U cases NL #H @H @(update_fail … U)
    181189qed.
     
    188196whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
    189197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
    190 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
     198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
    191199  % #E' destruct
    192 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
    193   <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
     200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
     201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    194202] qed.
    195203
     
    197205
    198206inductive identifier_set (tag:String) : Type[0] ≝
    199   an_id_set : BitVectorTrie unit 16 → identifier_set tag.
     207  an_id_set : positive_map unit → identifier_set tag.
    200208
    201209definition empty_set : ∀tag:String. identifier_set tag ≝
    202 λtag. an_id_set tag (Stub unit 16).
     210λtag. an_id_set tag (pm_leaf unit).
    203211
    204212let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
    205   an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
    206                              it (match s with [ an_id_set s' ⇒ s' ])).
     213  an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
     214                          it (match s with [ an_id_set s' ⇒ s' ])).
    207215
    208216definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
     
    210218
    211219let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
    212   match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
    213                         (match s with [ an_id_set s' ⇒ s' ]) with
     220  match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
     221                     (match s with [ an_id_set s' ⇒ s' ]) with
    214222  [ None ⇒ false
    215223  | Some _ ⇒ true
     
    217225
    218226let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
    219   an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
    220                                (match s' with [ an_id_set s1 ⇒ s1 ])).
     227  an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
     228                            (match s' with [ an_id_set s1 ⇒ s1 ])).
    221229
    222230interpretation "identifier set union" 'union a b = (union_set ? a b).
     
    231239
    232240lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    233 #tag * #s cases (BitVectorTrie_Sn … s)
    234 [ * #x * #y #E >E //
    235 | #E >E //
    236 ] qed.
     241#tag * * // qed.
  • src/common/PreIdentifiers.ma

    r797 r1515  
    77include "basics/types.ma".
    88include "ASM/String.ma".
    9 include "ASM/Arithmetic.ma".
     9include "utilities/binary/positive.ma".
    1010
    1111(* identifiers and their generators are tagged to differentiate them, and to
     
    1313
    1414inductive identifier (tag:String) : Type[0] ≝
    15   an_identifier : Word → identifier tag.
     15  an_identifier : Pos → identifier tag.
Note: See TracChangeset for help on using the changeset viewer.