1 | include "basics/types.ma". |
---|

2 | |
---|

3 | include "ASM/BitVector.ma". |
---|

4 | |
---|

5 | inductive 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 | |
---|

10 | let 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 | |
---|

19 | let 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 | ] |
---|

45 | qed. |
---|

46 | |
---|

47 | let 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 | |
---|

57 | let 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 | ] |
---|

76 | qed. |
---|