source: src/ASM/BitVectorTrie.ma @ 779

Last change on this file since 779 was 779, checked in by campbell, 9 years ago

Add merging of tries and identifier sets (based on Dominic's earlier code).
Not used at present (I decided to implement the part that would have used it
differently).

File size: 4.0 KB
Line 
1include "basics/types.ma".
2
3include "utilities/option.ma".
4include "ASM/BitVector.ma".
5
6inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
7  Leaf: A → BitVectorTrie A O
8| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
9| Stub: ∀n: nat. BitVectorTrie A n.
10
11let rec lookup_opt (A: Type[0]) (n: nat)
12                (b: BitVector n) (t: BitVectorTrie A n) on t
13       : option A ≝
14 (match t return λx.λ_. BitVector x → option A with
15  [ Leaf l ⇒ λ_.Some ? l
16  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
17  | Stub _ ⇒ λ_.None ?
18  ]) b.
19
20let rec lookup (A: Type[0]) (n: nat)
21                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
22       : A ≝
23  (match b return λx.λ_. x = n → A with
24    [ VEmpty ⇒
25      (match t return λx.λ_. O = x → A with
26        [ Leaf l ⇒ λ_.l
27        | Node h l r ⇒ λK.⊥
28        | Stub s ⇒ λ_.a
29        ])
30    | VCons o hd tl ⇒
31      match t return λx.λ_. (S o) = x → A with
32        [ Leaf l ⇒ λK.⊥
33        | Node h l r ⇒
34           match hd with
35             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
36             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
37             ]
38        | Stub s ⇒ λ_. a]
39    ]) (refl ? n).
40  [1,2:
41    destruct
42  |*:
43    @ injective_S
44    //
45  ]
46qed.
47
48let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
49   match b with
50    [ VEmpty ⇒ Leaf A a
51    | VCons o hd tl ⇒
52      match hd with
53        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
54        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
55        ]
56    ].
57
58let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
59  (match b with
60    [ VEmpty ⇒ λ_. Leaf A a
61    | VCons o hd tl ⇒ λt.
62          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
63            [ Leaf l ⇒ λprf.⊥
64            | Node p l r ⇒ λprf.
65               match hd with
66                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
67                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
68                ]
69            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
70            ] (refl ? (S o))
71    ]).
72  [ destruct
73  |*:
74    @ injective_S
75    //
76  ]
77qed.
78
79let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
80  (match b with
81    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
82                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
83                   | Stub _ ⇒ λ_. None ?
84                   | Node _ _ _ ⇒ λprf. ⊥
85                   ] (refl ? O)
86    | VCons o hd tl ⇒ λt.
87          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
88            [ Leaf l ⇒ λprf.⊥
89            | Node p l r ⇒ λprf.
90               match hd with
91                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
92                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
93                ]
94            | Stub p ⇒ λprf. None ?
95            ] (refl ? (S o))
96    ]).
97  [ 1,2: destruct
98  |*:
99    @ injective_S @sym_eq @prf
100  ]
101qed.
102
103let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
104  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
105  [ Stub _ ⇒ λc. c
106  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
107  | Node p l r ⇒
108    λc.
109    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
110    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
111    | Stub _ ⇒ λprf. Node ? p l r
112    | Leaf _ ⇒ λabsd. ?
113    ] (refl ? (S p)))
114  ].
115  [1:
116      destruct(absd)
117  |2,3:
118      @ injective_S
119        assumption
120  ]
121qed.
Note: See TracBrowser for help on using the repository browser.