Last change
on this file since 733 was
698,
checked in by mulligan, 10 years ago

Commit with changes to files to get our files to typecheck.

File size:
1.5 KB

Rev  Line  

[698]  1  include "ASM/BitVectorTrie.ma". 

[491]  2  

 3  definition BitVectorTrieSet ≝ BitVectorTrie unit. 

 4  

 5  let rec set_member (n: nat) (p: Vector bool n) (b: BitVectorTrieSet n) on p: bool ≝ 

 6  (match p return λx. λ_. n = x → bool with 

 7  [ VEmpty ⇒ 

 8  ( match b return λx. λ_. x = 0 → bool with 

 9  [ Leaf _ ⇒ λprf. true 

 10   Stub _ ⇒ λprf. false 

 11   _ ⇒ λabsd. ? 

 12  ]) 

 13   VCons o hd tl ⇒ 

 14  (match b return λx. λ_. x = S o → bool with 

 15  [ Leaf _ ⇒ λabsd. ? 

 16   Stub _ ⇒ λprf. false 

 17   Node p l r ⇒ 

 18  match hd with 

 19  [ true ⇒ λprf: S p = S o. set_member o tl (r⌈p ↦ o⌉) 

 20   false ⇒ λprf: S p = S o. set_member o tl (l⌈p ↦ o⌉) 

 21  ] 

 22  ]) 

 23  ]) (refl ? n). 

 24  [3,4: 

 25  @ injective_S 

 26  assumption 

 27  1,2: 

 28  destruct 

 29  ] 

 30  qed. 

 31  

 32  let rec set_union (n: nat) (b: BitVectorTrieSet n) on b: BitVectorTrieSet n → BitVectorTrieSet n ≝ 

 33  match b return λx. λ_. BitVectorTrieSet x → BitVectorTrieSet x with 

 34  [ Stub _ ⇒ λc. c 

 35   Leaf l ⇒ λc. Leaf ? l 

 36   Node p l r ⇒ 

 37  λc. 

 38  (match c return λx. λ_. x = (S p) → BitVectorTrieSet (S p) with 

 39  [ Node p' l' r' ⇒ λprf. Node ? ? (set_union ? l (l'⌈p' ↦ p⌉)) (set_union ? r (r'⌈p' ↦ p⌉)) 

 40   Stub _ ⇒ λprf. Node ? p l r 

 41   Leaf _ ⇒ λabsd. ? 

 42  ] (refl ? (S p))) 

 43  ]. 

 44  [1: 

 45  destruct(absd) 

 46  2,3: 

 47  @ injective_S 

 48  assumption 

 49  ] 

 50  qed. 

 51  

 52  definition set_insert ≝ 

 53  λn: nat. 

 54  λb: BitVector n. 

 55  λs: BitVectorTrieSet n. 

 56  insert unit n b it s. 

 57  

 58  definition set_empty ≝ λn. Stub unit n. 

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