module list-any where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_!$\equiv$!_; refl; sym; trans; cong)
open Eq.!$\equiv$!-Reasoning
open import Data.Bool using (Bool; true; false; T; _!$\wedge$!_; _∨_; not)
open import Data.Nat using (!$\mathbb{N}$!; zero; suc; _+_; _*_; _∸_; _!$\leq$!_; s!$\leq$!s; z!$\leq$!n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (!$\neg$!_; Dec; yes; no)
open import Data.Product using (_!$\times$!_; ∃; ∃-syntax) renaming (_,_ to !$\langle$!_,_!$\rangle$!)
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 !$\mathbb{N}$!
test-l = 1 !$\text{::}$! 2 !$\text{::}$! []

data Any-test {A : Set} (P : A !$\rightarrow$! Set) : List A !$\rightarrow$! Set where
  here  : !$\forall$! {x : A} {xs : List A} !$\rightarrow$! P x !$\rightarrow$! Any-test P (x !$\text{::}$! xs)
  there : !$\forall$! {x : A} {xs : List A} !$\rightarrow$! Any-test P xs !$\rightarrow$! Any-test P (x !$\text{::}$! xs)

{-
_∈_ : !$\forall$! {A : Set} (x : A) (xs : List A) !$\rightarrow$! Set
x ∈ xs = Any (x !$\equiv$!_) xs
-}

_∈1_ : !$\forall$! (n : !$\mathbb{N}$!) (xs : List !$\mathbb{N}$!) !$\rightarrow$! Set
n ∈1 [] = Any-test (n !$\equiv$!_) []
n ∈1 l@(x !$\text{::}$! xs) with <-cmp n x
... | tri< a !$\neg$!b !$\neg$!c = Any-test (n !$\equiv$!_) xs
... | tri!$\approx$! !$\neg$!a b !$\neg$!c = Any-test (n !$\equiv$!_) l
... | tri> !$\neg$!a !$\neg$!b c = Any-test (n !$\equiv$!_) xs

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

data Any (P : !$\mathbb{N}$! !$\rightarrow$! Set) : rbt !$\rightarrow$! Set where
  here  : !$\forall$! {x : !$\mathbb{N}$!} {xs : rbt} !$\rightarrow$! P x !$\rightarrow$! Any P xs
  there : !$\forall$! {x : !$\mathbb{N}$!} {xs : rbt} !$\rightarrow$! Any P (get-rbt xs) !$\rightarrow$! Any P xs

_∈_ : !$\forall$! (n : !$\mathbb{N}$!) (xs : rbt) !$\rightarrow$! Bool
n ∈ bt-empty = false
n ∈ bt-node node with <-cmp n (node.number (tree.key node))
... | tri< a !$\neg$!b !$\neg$!c = n ∈ (tree.ltree node)
... | tri!$\approx$! !$\neg$!a b !$\neg$!c = true
... | tri> !$\neg$!a !$\neg$!b c = n ∈ (tree.rtree node)



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

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


test1kk = 100 ∈ (Env.vart testrbt6)