module list-any where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Level using (Level)
--open import plfa.part1.Isomorphism using (_≃_; _⇔_)

open import Data.List
open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

open import rbt_t

-- infix 4 _∈_ _∉_

test-l : List ℕ
test-l = 1 ∷ 2 ∷ []

data Any-test {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any-test P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any-test P xs → Any-test P (x ∷ xs)

{-
_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs
-}

_∈1_ : ∀ (n : ℕ) (xs : List ℕ) → Set
n ∈1 [] = Any-test (n ≡_) []
n ∈1 l@(x ∷ xs) with <-cmp n x
... | tri< a ¬b ¬c = Any-test (n ≡_) xs
... | tri≈ ¬a b ¬c = Any-test (n ≡_) l
... | tri> ¬a ¬b c = Any-test (n ≡_) xs

test : 1 ∈1 test-l
test = here refl

data Any (P : ℕ → Set) : rbt → Set where
  here  : ∀ {x : ℕ} {xs : rbt} → P x → Any P xs
  there : ∀ {x : ℕ} {xs : rbt} → Any P (get-rbt xs) → Any P xs

_∈_ : ∀ (n : ℕ) (xs : rbt) → Bool
n ∈ bt-empty = false
n ∈ bt-node node with <-cmp n (node.number (tree.key node))
... | tri< a ¬b ¬c = n ∈ (tree.ltree node)
... | tri≈ ¬a b ¬c = true
... | tri> ¬a ¬b c = n ∈ (tree.rtree node)



testany1 : rbt → Set
testany1 bt-empty = {!!}
testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!}

testrbt1 = whileTestPCall' bt-empty 0
testrbt2 = whileTestPCall' (Env.vart testrbt1) 1
testrbt3 = whileTestPCall' (Env.vart testrbt2) 2
testrbt4 = whileTestPCall' (Env.vart testrbt3) 3
testrbt5 = whileTestPCall' (Env.vart testrbt4) 4
testrbt6 = whileTestPCall' (Env.vart testrbt5) 5
testrbt7 = whileTestPCall' (Env.vart testrbt6) 6


test1kk = 100 ∈ (Env.vart testrbt6)