[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 | |
---|
[782] | 11 | axiom fold: |
---|
| 12 | ∀A, B: Type[0]. |
---|
| 13 | ∀n: nat. |
---|
| 14 | ∀f: BitVector n → A → B → B. |
---|
| 15 | ∀t: BitVectorTrie A n. |
---|
| 16 | ∀b: B. |
---|
| 17 | B. |
---|
| 18 | |
---|
[726] | 19 | let rec lookup_opt (A: Type[0]) (n: nat) |
---|
| 20 | (b: BitVector n) (t: BitVectorTrie A n) on t |
---|
| 21 | : option A ≝ |
---|
| 22 | (match t return λx.λ_. BitVector x → option A with |
---|
| 23 | [ Leaf l ⇒ λ_.Some ? l |
---|
| 24 | | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l) |
---|
| 25 | | Stub _ ⇒ λ_.None ? |
---|
| 26 | ]) b. |
---|
| 27 | |
---|
[475] | 28 | let rec lookup (A: Type[0]) (n: nat) |
---|
| 29 | (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b |
---|
| 30 | : A ≝ |
---|
| 31 | (match b return λx.λ_. x = n → A with |
---|
| 32 | [ VEmpty ⇒ |
---|
| 33 | (match t return λx.λ_. O = x → A with |
---|
| 34 | [ Leaf l ⇒ λ_.l |
---|
| 35 | | Node h l r ⇒ λK.⊥ |
---|
| 36 | | Stub s ⇒ λ_.a |
---|
| 37 | ]) |
---|
| 38 | | VCons o hd tl ⇒ |
---|
| 39 | match t return λx.λ_. (S o) = x → A with |
---|
| 40 | [ Leaf l ⇒ λK.⊥ |
---|
| 41 | | Node h l r ⇒ |
---|
| 42 | match hd with |
---|
| 43 | [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a |
---|
| 44 | | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a |
---|
| 45 | ] |
---|
| 46 | | Stub s ⇒ λ_. a] |
---|
| 47 | ]) (refl ? n). |
---|
| 48 | [1,2: |
---|
| 49 | destruct |
---|
| 50 | |*: |
---|
| 51 | @ injective_S |
---|
| 52 | // |
---|
| 53 | ] |
---|
| 54 | qed. |
---|
| 55 | |
---|
| 56 | let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝ |
---|
| 57 | match b with |
---|
| 58 | [ VEmpty ⇒ Leaf A a |
---|
| 59 | | VCons o hd tl ⇒ |
---|
| 60 | match hd with |
---|
| 61 | [ true ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) |
---|
| 62 | | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) |
---|
| 63 | ] |
---|
| 64 | ]. |
---|
| 65 | |
---|
| 66 | let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
| 67 | (match b with |
---|
| 68 | [ VEmpty ⇒ λ_. Leaf A a |
---|
| 69 | | VCons o hd tl ⇒ λt. |
---|
| 70 | match t return λy.λ_. S o = y → BitVectorTrie A (S o) with |
---|
| 71 | [ Leaf l ⇒ λprf.⊥ |
---|
| 72 | | Node p l r ⇒ λprf. |
---|
| 73 | match hd with |
---|
| 74 | [ true ⇒ Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉)) |
---|
| 75 | | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉) |
---|
| 76 | ] |
---|
| 77 | | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a) |
---|
| 78 | ] (refl ? (S o)) |
---|
| 79 | ]). |
---|
| 80 | [ destruct |
---|
| 81 | |*: |
---|
| 82 | @ injective_S |
---|
| 83 | // |
---|
| 84 | ] |
---|
[761] | 85 | qed. |
---|
| 86 | |
---|
| 87 | let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ |
---|
| 88 | (match b with |
---|
| 89 | [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with |
---|
| 90 | [ Leaf _ ⇒ λ_. Some ? (Leaf A a) |
---|
| 91 | | Stub _ ⇒ λ_. None ? |
---|
| 92 | | Node _ _ _ ⇒ λprf. ⊥ |
---|
| 93 | ] (refl ? O) |
---|
| 94 | | VCons o hd tl ⇒ λt. |
---|
| 95 | match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with |
---|
| 96 | [ Leaf l ⇒ λprf.⊥ |
---|
| 97 | | Node p l r ⇒ λprf. |
---|
| 98 | match hd with |
---|
| 99 | [ true ⇒ option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉)) |
---|
| 100 | | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉)) |
---|
| 101 | ] |
---|
| 102 | | Stub p ⇒ λprf. None ? |
---|
| 103 | ] (refl ? (S o)) |
---|
| 104 | ]). |
---|
| 105 | [ 1,2: destruct |
---|
| 106 | |*: |
---|
| 107 | @ injective_S @sym_eq @prf |
---|
| 108 | ] |
---|
| 109 | qed. |
---|
[779] | 110 | |
---|
| 111 | let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
| 112 | match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with |
---|
| 113 | [ Stub _ ⇒ λc. c |
---|
| 114 | | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ] |
---|
| 115 | | Node p l r ⇒ |
---|
| 116 | λc. |
---|
| 117 | (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with |
---|
| 118 | [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉)) |
---|
| 119 | | Stub _ ⇒ λprf. Node ? p l r |
---|
| 120 | | Leaf _ ⇒ λabsd. ? |
---|
| 121 | ] (refl ? (S p))) |
---|
| 122 | ]. |
---|
| 123 | [1: |
---|
| 124 | destruct(absd) |
---|
| 125 | |2,3: |
---|
| 126 | @ injective_S |
---|
| 127 | assumption |
---|
| 128 | ] |
---|
| 129 | qed. |
---|