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

Last change on this file since 246 was 246, checked in by mulligan, 9 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
RevLine 
[246]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.