source: Deliverables/D4.1/Matita/BitVectorTrie.ma @ 246

Last change on this file since 246 was 246, checked in by mulligan, 10 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

File size: 3.1 KB
Line 
1include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
2include "Programming/Datatypes/Compare.ma".
3include "Programming/Datatypes/Bool.ma".
4include "Programming/Datatypes/Maybe.ma".
5
6ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝
7  Leaf: A → BitVectorTrie A Z
8| Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
9| Stub: ∀n: Nat. BitVectorTrie A n.
10
11notation "hvbox(t⌈h ↦ o⌉)"
12  with precedence 45
13  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
14
15notation "⊥" with precedence 90
16  for @{ match ? in False with [ ] }.
17
18nlet rec lookup (A: Type[0]) (n: Nat)
19                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
20       : A ≝
21  (match b return λx.λ_. x = n → A with
22    [ Empty ⇒
23      (match t return λx.λ_. Z = x → A with
24        [ Leaf l ⇒ λ_.l
25        | Node h l r ⇒ λK.⊥
26        | Stub s ⇒ λ_.a
27        ])
28    | Cons o hd tl ⇒
29      match t return λx.λ_. (S o) = x → A with
30        [ Leaf l ⇒ λK.⊥
31        | Node h l r ⇒
32           match hd with
33             [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
34             | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
35             ]
36        | Stub s ⇒ λ_. a
37        ]
38    ]) (refl ? n).
39    ndestruct; //.
40nqed.
41
42nlet rec prepare_trie_for_insertion (A: Type[0]) (n: Nat)
43                                    (b: BitVector n) (a:A) on b
44       : BitVectorTrie A n ≝
45   match b with
46    [ Empty ⇒ Leaf A a
47    | Cons o hd tl ⇒
48      match hd with
49        [ True ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
50        | False ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
51        ]
52    ].
53
54nlet rec insert (A: Type[0]) (n: Nat)
55                (b: BitVector n) (a: A) on b:
56                 BitVectorTrie A n → BitVectorTrie A n ≝
57  (match b with
58    [ Empty ⇒ λ_. Leaf A a
59    | Cons o hd tl ⇒ λt.
60          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
61            [ Leaf l ⇒ λprf.⊥
62            | Node p l r ⇒ λprf.
63               match hd with
64                [ True ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
65                | False ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
66                ]
67            | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)
68            ] (refl ? (S o))
69    ]).
70    ##[ ndestruct;
71    ##| ndestruct; @;
72    ##| ndestruct; @;
73    ##| ndestruct; @;
74    ##| ndestruct; @;
75    ##| #H; nassumption;
76    ##]
77nqed.
78
79nlemma insert_lookup_stub:
80  ∀A: Type[0].
81  ∀n: Nat.
82  ∀b: BitVector n.
83  ∀t: BitVectorTrie A n.
84  ∀a, c: A.
85    (lookup A n b (insert A n b a (Stub A n)) a) = a.
86  #A n b t a c.
87  nelim b.
88  //.
89  #N H V H2.
90  nnormalize.
91  @.
92nqed.
93
94ncheck length.
95
96(*
97nlemma test:
98  ∀n: Nat.
99  ∀b: BitVector n.
100    length n b = n.
101  #n b.
102  nelim b.
103  //.
104  #N H V IH.
105  ncases H.
106*)
107
108nlemma insert_lookup_leaf:
109  ∀A: Type[0].
110  ∀n: Nat.
111  ∀b: BitVector n.
112  ∀a, c: A.
113  ∀t: BitVectorTrie A n.
114    lookup A ? b (insert A ? b a t) c = a.
115  #A n b a c t.
116  nelim b.
117  nnormalize.
118  @.
119  #N H V IH.
Note: See TracBrowser for help on using the repository browser.