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

Make stuff from D4.1 work with my copy of matita.

File size:
2.0 KB

Rev  Line  

[533]  1  include "basics/types.ma". 

[475]  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.