|
1
|
1 module list-any where
|
|
|
2
|
|
|
3 import Relation.Binary.PropositionalEquality as Eq
|
|
|
4 open Eq using (_≡_; refl; sym; trans; cong)
|
|
|
5 open Eq.≡-Reasoning
|
|
|
6 open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
|
|
|
7 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
|
|
8 open import Data.Nat.Properties using
|
|
|
9 (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
|
|
10 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
11 open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
|
|
12 open import Function using (_∘_)
|
|
|
13 open import Level using (Level)
|
|
|
14 --open import plfa.part1.Isomorphism using (_≃_; _⇔_)
|
|
|
15
|
|
|
16 open import Data.List
|
|
|
17 open import Data.Nat.Properties as NatProp -- <-cmp
|
|
|
18 open import Relation.Binary
|
|
|
19
|
|
|
20 open import rbt_t
|
|
|
21
|
|
|
22 -- infix 4 _∈_ _∉_
|
|
|
23
|
|
|
24 test-l : List ℕ
|
|
|
25 test-l = 1 ∷ 2 ∷ []
|
|
|
26
|
|
|
27 data Any-test {A : Set} (P : A → Set) : List A → Set where
|
|
|
28 here : ∀ {x : A} {xs : List A} → P x → Any-test P (x ∷ xs)
|
|
|
29 there : ∀ {x : A} {xs : List A} → Any-test P xs → Any-test P (x ∷ xs)
|
|
|
30
|
|
|
31 {-
|
|
|
32 _∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
|
|
|
33 x ∈ xs = Any (x ≡_) xs
|
|
|
34 -}
|
|
|
35
|
|
|
36 _∈1_ : ∀ (n : ℕ) (xs : List ℕ) → Set
|
|
|
37 n ∈1 [] = Any-test (n ≡_) []
|
|
|
38 n ∈1 l@(x ∷ xs) with <-cmp n x
|
|
|
39 ... | tri< a ¬b ¬c = Any-test (n ≡_) xs
|
|
|
40 ... | tri≈ ¬a b ¬c = Any-test (n ≡_) l
|
|
|
41 ... | tri> ¬a ¬b c = Any-test (n ≡_) xs
|
|
|
42
|
|
|
43 test : 1 ∈1 test-l
|
|
|
44 test = here refl
|
|
|
45
|
|
|
46 data Any (P : ℕ → Set) : rbt → Set where
|
|
|
47 here : ∀ {x : ℕ} {xs : rbt} → P x → Any P xs
|
|
|
48 there : ∀ {x : ℕ} {xs : rbt} → Any P (get-rbt xs) → Any P xs
|
|
|
49
|
|
|
50 _∈_ : ∀ (n : ℕ) (xs : rbt) → Bool
|
|
|
51 n ∈ bt-empty = false
|
|
|
52 n ∈ bt-node node with <-cmp n (node.number (tree.key node))
|
|
|
53 ... | tri< a ¬b ¬c = n ∈ (tree.ltree node)
|
|
|
54 ... | tri≈ ¬a b ¬c = true
|
|
|
55 ... | tri> ¬a ¬b c = n ∈ (tree.rtree node)
|
|
|
56
|
|
|
57
|
|
|
58
|
|
|
59 testany1 : rbt → Set
|
|
|
60 testany1 bt-empty = {!!}
|
|
|
61 testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!}
|
|
|
62
|
|
|
63 testrbt1 = whileTestPCall' bt-empty 0
|
|
|
64 testrbt2 = whileTestPCall' (Env.vart testrbt1) 1
|
|
|
65 testrbt3 = whileTestPCall' (Env.vart testrbt2) 2
|
|
|
66 testrbt4 = whileTestPCall' (Env.vart testrbt3) 3
|
|
|
67 testrbt5 = whileTestPCall' (Env.vart testrbt4) 4
|
|
|
68 testrbt6 = whileTestPCall' (Env.vart testrbt5) 5
|
|
|
69 testrbt7 = whileTestPCall' (Env.vart testrbt6) 6
|
|
|
70
|
|
|
71
|
|
|
72 test1kk = 100 ∈ (Env.vart testrbt6)
|
|
|
73
|
