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≈ @$\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≈ @$\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' 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)