source: src/ASM/BitVectorTrie.ma @ 726

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

Change identifiers to Words in Clight and RTLabs semantics.

File size: 2.4 KB
Line 
1include "basics/types.ma".
2
3include "ASM/BitVector.ma".
4
5inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
6  Leaf: A → BitVectorTrie A O
7| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
8| Stub: ∀n: nat. BitVectorTrie A n.
9
10let rec lookup_opt (A: Type[0]) (n: nat)
11                (b: BitVector n) (t: BitVectorTrie A n) on t
12       : option A ≝
13 (match t return λx.λ_. BitVector x → option A with
14  [ Leaf l ⇒ λ_.Some ? l
15  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
16  | Stub _ ⇒ λ_.None ?
17  ]) b.
18
19let rec lookup (A: Type[0]) (n: nat)
20                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
21       : A ≝
22  (match b return λx.λ_. x = n → A with
23    [ VEmpty ⇒
24      (match t return λx.λ_. O = x → A with
25        [ Leaf l ⇒ λ_.l
26        | Node h l r ⇒ λK.⊥
27        | Stub s ⇒ λ_.a
28        ])
29    | VCons o hd tl ⇒
30      match t return λx.λ_. (S o) = x → A with
31        [ Leaf l ⇒ λK.⊥
32        | Node h l r ⇒
33           match hd with
34             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
35             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
36             ]
37        | Stub s ⇒ λ_. a]
38    ]) (refl ? n).
39  [1,2:
40    destruct
41  |*:
42    @ injective_S
43    //
44  ]
45qed.
46
47let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
48   match b with
49    [ VEmpty ⇒ Leaf A a
50    | VCons o hd tl ⇒
51      match hd with
52        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
53        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
54        ]
55    ].
56
57let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
58  (match b with
59    [ VEmpty ⇒ λ_. Leaf A a
60    | VCons o hd tl ⇒ λt.
61          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
62            [ Leaf l ⇒ λprf.⊥
63            | Node p l r ⇒ λprf.
64               match hd with
65                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
66                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
67                ]
68            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
69            ] (refl ? (S o))
70    ]).
71  [ destruct
72  |*:
73    @ injective_S
74    //
75  ]
76qed.
Note: See TracBrowser for help on using the repository browser.