source: src/ASM/BitVectorTrie.ma @ 697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

File size: 2.0 KB
Line 
1include "basics/types.ma".
2
3include "cerco/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 (A: Type[0]) (n: nat)
11                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
12       : A ≝
13  (match b return λx.λ_. x = n → A with
14    [ VEmpty ⇒
15      (match t return λx.λ_. O = x → A with
16        [ Leaf l ⇒ λ_.l
17        | Node h l r ⇒ λK.⊥
18        | Stub s ⇒ λ_.a
19        ])
20    | VCons o hd tl ⇒
21      match t return λx.λ_. (S o) = x → A with
22        [ Leaf l ⇒ λK.⊥
23        | Node h l r ⇒
24           match hd with
25             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
26             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
27             ]
28        | Stub s ⇒ λ_. a]
29    ]) (refl ? n).
30  [1,2:
31    destruct
32  |*:
33    @ injective_S
34    //
35  ]
36qed.
37
38let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
39   match b with
40    [ VEmpty ⇒ Leaf A a
41    | VCons o hd tl ⇒
42      match hd with
43        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
44        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
45        ]
46    ].
47
48let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
49  (match b with
50    [ VEmpty ⇒ λ_. Leaf A a
51    | VCons o hd tl ⇒ λt.
52          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
53            [ Leaf l ⇒ λprf.⊥
54            | Node p l r ⇒ λprf.
55               match hd with
56                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
57                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
58                ]
59            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
60            ] (refl ? (S o))
61    ]).
62  [ destruct
63  |*:
64    @ injective_S
65    //
66  ]
67qed.
Note: See TracBrowser for help on using the repository browser.