[697] | 1 | include "basics/types.ma". |
---|
[475] | 2 | |
---|
[761] | 3 | include "utilities/option.ma". |
---|
[698] | 4 | include "ASM/BitVector.ma". |
---|
[475] | 5 | |
---|
| 6 | inductive 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 | |
---|
[726] | 11 | let 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 | |
---|
[475] | 20 | let 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 | ] |
---|
| 46 | qed. |
---|
| 47 | |
---|
| 48 | let 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 | |
---|
| 58 | let 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 | ] |
---|
[761] | 77 | qed. |
---|
| 78 | |
---|
| 79 | let 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 | ] |
---|
| 101 | qed. |
---|
[779] | 102 | |
---|
| 103 | let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
| 104 | match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with |
---|
| 105 | [ Stub _ ⇒ λc. c |
---|
| 106 | | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ] |
---|
| 107 | | Node p l r ⇒ |
---|
| 108 | λc. |
---|
| 109 | (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with |
---|
| 110 | [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉)) |
---|
| 111 | | Stub _ ⇒ λprf. Node ? p l r |
---|
| 112 | | Leaf _ ⇒ λabsd. ? |
---|
| 113 | ] (refl ? (S p))) |
---|
| 114 | ]. |
---|
| 115 | [1: |
---|
| 116 | destruct(absd) |
---|
| 117 | |2,3: |
---|
| 118 | @ injective_S |
---|
| 119 | assumption |
---|
| 120 | ] |
---|
| 121 | qed. |
---|