Changeset 1285 for src/utilities


Ignore:
Timestamp:
Oct 3, 2011, 3:08:21 PM (9 years ago)
Author:
mulligan
Message:

more implementation on maps, final push to get rtl abs to rtl working

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/utilities/adt/table_adt.ma

    r1274 r1285  
    1313  | empty: table dom_type rng_type
    1414  | node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type.
    15  
    16 definition tbl_empty ≝ empty.
    17 
    18 definition tbl_size ≝
     15
     16definition tbl_height ≝
    1917  λdom_type : Type[0].
    2018  λrng_type : Type[0].
    … …  
    2523  ].
    2624
     25let rec tbl_size
     26  (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type)
     27    on the_table: nat ≝
     28  match the_table with
     29  [ empty ⇒ 0
     30  | node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r)
     31  ].
     32 
     33definition tbl_empty ≝
     34  λdom_type: Type[0].
     35  λrng_type: Type[0].
     36    empty dom_type rng_type.
     37
     38definition tbl_is_empty ≝
     39  λdom_type: Type[0].
     40  λrng_type: Type[0].
     41  λthe_table: table dom_type rng_type.
     42  match the_table with
     43  [ empty ⇒ true
     44  | _     ⇒ false
     45  ].
     46
     47definition tbl_is_empty_p ≝
     48  λdom_type: Type[0].
     49  λrng_type: Type[0].
     50  λthe_table: table dom_type rng_type.
     51  match the_table with
     52  [ empty ⇒ True
     53  | _     ⇒ False
     54  ].
     55
    2756let rec tbl_to_list
    2857  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
    … …  
    3261  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
    3362  ].
    34  
    35 axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
    36 
    37 axiom tbl_merge:
    38   ∀key_type, rng_type.
    39     (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type.
    40 
    41 axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
     63
     64let rec tbl_min_binding
     65  (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type)
     66    (proof: ¬ (tbl_is_empty_p … the_table))
     67      on the_table: key_type × rng_type ≝
     68  match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with
     69  [ empty               ⇒ λabsurd. ?
     70  | node sz key val l r ⇒ λproof.
     71    match l return λx. x = l → key_type × rng_type with
     72    [ empty ⇒ λproof. 〈key, val〉
     73    | _     ⇒ λproof. tbl_min_binding key_type rng_type l ?
     74    ] (refl … l)
     75  ] proof.
     76  [1: normalize in absurd;
     77      elim absurd;
     78      #ABSURD
     79      @⊥ @ABSURD @I
     80  |2: <proof
     81      normalize
     82      /2/
     83  ]
     84qed.
     85
     86definition tbl_create ≝
     87  λkey_type: Type[0].
     88  λrng_type: Type[0].
     89  λleft    : table key_type rng_type.
     90  λkey     : key_type.
     91  λval     : rng_type.
     92  λright   : table key_type rng_type.
     93  let hl ≝ tbl_height … left in
     94  let hr ≝ tbl_height … right in
     95  let height ≝ if gtb hl hr then hl + 1 else hr + 1 in
     96    node key_type rng_type height key val left right.
     97     
     98let rec tbl_balance
     99  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     100    (left: table key_type rng_type) (key: key_type) (val: rng_type)
     101      (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left))
     102        (right_proof: ¬ (tbl_is_empty_p … right))
     103          on left: table key_type rng_type ≝
     104  match gtb (tbl_height … left) ((tbl_height … right) + 2) with
     105  [ true  ⇒
     106    match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     107    [ empty              ⇒ λabsurd. ?
     108    | node _ lv ld ll lr ⇒ λnon_empty_proof.
     109      if gtb (tbl_height … ll) (tbl_height … lr) then
     110        tbl_create … ll lv ld (tbl_create … lr key val right)
     111      else
     112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     113        [ empty ⇒ λabsurd. ?
     114        | node _ lrv lrd lrl lrr ⇒ λ
     115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
     116        ]
     117    ] left_proof
     118  | false ⇒ ?
     119  ].
     120  [1: normalize in absurd;
     121      elim absurd
     122      #ABSURD
     123      @⊥ @ABSURD @I
     124  |*: cases daemon
     125  ]
     126qed.
     127 
     128let rec tbl_remove_min_binding
     129  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     130    (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table))
     131      on the_table: table key_type rng_type ≝
     132  match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     133  [ empty               ⇒ λabsurd. ?
     134  | node sz key val l r ⇒ λproof.
     135    match l return λx. x = l → table key_type rng_type with
     136    [ empty ⇒ λproof. r
     137    | _     ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r
     138    ] (refl … l)
     139  ] proof.
     140  [1: normalize in absurd;
     141      elim absurd;
     142      #ABSURD
     143      @⊥ @ABSURD @I
     144  |2: <proof
     145      normalize
     146      @nmk //
     147  ]
     148qed.
     149   
     150let rec tbl_insert
     151  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     152    (key: key_type) (val: rng_type) (the_table: table key_type rng_type)
     153      on the_table: table key_type rng_type ≝
     154  match the_table with
     155  [ empty                 ⇒ node … 1 key val (empty …) (empty …)
     156  | node sz key' val' l r ⇒
     157    match ord key key' with
     158    [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r
     159    | order_eq ⇒ node … sz key val l r
     160    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r)
     161    ]
     162  ].
     163 
     164let rec tbl_merge
     165  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
     166    (left: table dom_type rng_type) (right: table dom_type rng_type)
     167      on left: table dom_type rng_type ≝
     168  match left with
     169  [ empty ⇒ right
     170  | _     ⇒
     171    match right return λx. x = right → table dom_type rng_type with
     172    [ empty               ⇒ λid_proof. left
     173    | node sz key val l r ⇒ λid_proof.
     174      let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in
     175        tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?)
     176    ] (refl … right)
     177  ].
     178  <id_proof
     179  normalize /2/
     180qed.
     181
     182let rec tbl_remove
     183  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     184    (key: key_type) (the_table: table key_type rng_type)
     185      on the_table: table key_type rng_type ≝
     186  match the_table with
     187  [ empty                 ⇒ empty …
     188  | node sz key' val' l r ⇒
     189    match ord key key' with
     190    [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r
     191    | order_eq ⇒ tbl_merge … ord l r
     192    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r)
     193    ]
     194  ].
    42195 
    43196let rec tbl_find
    … …  
    87240  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
    88241  ].
    89  
    90 axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
    91                     → table key_type rng_type → bool.
     242     
     243axiom tbl_equal:
     244  ∀key_type, rng_type.
     245    (key_type → key_type → order) → (rng_type → rng_type → order) →
     246      table key_type rng_type → table key_type rng_type → bool.
    92247
    93248let rec tbl_mapi
    … …  
    117272  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
    118273  ].
    119 
    120 definition tbl_is_empty ≝
    121   λkey_type : Type[0].
    122   λrng_type : Type[0].
    123   λtable    : table key_type rng_type.
    124     tbl_size … table = 0.
    125274
    126275definition tbl_singleton ≝
    … …  
    129278  λkey      : key_type.
    130279  λrng      : rng_type.
    131     tbl_insert … key rng (tbl_empty …).
     280    node key_type rng_type 1 key rng (empty …) (empty …).
    132281
    133282definition tbl_from_list ≝
    134283  λkey_type : Type[0].
    135284  λrng_type : Type[0].
     285  λord      : key_type → key_type → order.
    136286  λthe_list : list (key_type × rng_type).
    137287    foldr … (λkey_rng.
    138288      let 〈key, rng〉 ≝ key_rng in
    139         tbl_insert … key rng) (tbl_empty …) the_list.
     289        tbl_insert … ord key rng) (tbl_empty …) the_list.
    140290
    141291definition tbl_filter ≝
    142292  λdom_type : Type[0].
    143293  λrng_type : Type[0].
     294  λord      : dom_type → dom_type → order.
    144295  λf        : rng_type → bool.
    145296  λthe_table: table dom_type rng_type.
    146297  let as_list  ≝ tbl_to_list … the_table in
    147298  let filtered ≝ filter … (λx. f (\snd x)) as_list in
    148     tbl_from_list … filtered.
    149 
     299    tbl_from_list … ord filtered.
     300
Note: See TracChangeset for help on using the changeset viewer.