Last change
on this file since 688 was
475,
checked in by mulligan, 9 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

File size:
2.0 KB

Line  

1  include "basics/sums.ma". 

2  

3  include "cerco/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 (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  ] 

36  qed. 

37  

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

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

67  qed. 

Note: See
TracBrowser
for help on using the repository browser.