source: src/ASM/BitVectorTrie.ma @ 761

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

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File size: 3.4 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.
Note: See TracBrowser for help on using the repository browser.