Last change
on this file since 491 was
491,
checked in by mulligan, 8 years ago

Initial commit of (part)formalisation of LIN intermediate language.

File size:
1.5 KB

Line  

1  include "cerco/BitVectorTrie.ma". 

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.