Bst.agda

Bst.agda

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Bool
open import Data.Maybe
open import Data.Product


module Bst {l} (A : Set l) (_≤A_ : A → A → Bool) where


_isoBool_ : A → A → (_≤A_ : A → A → Bool) → Bool
(d isoBool d') _≤_ = (d ≤ d') ∧ (d' ≤ d)

isoBool-intro : {_≤A_ : A → A → Bool} {x y : A} → x ≤A y ≡ true → y ≤A x ≡ true → ((x isoBool y) _≤A_) ≡ true
isoBool-intro {x = x} {y = y} p₁ p₂ rewrite p₁ | p₂ = refl


data Singleton {l'} {B : Set l'} (x : B) : Set l' where
  _with≡_ : (y : B) → x ≡ y → Singleton x


inspect : ∀ {l'} {B : Set l'} (x : B) → Singleton x
inspect x = x with≡ refl



data Bst : A → A → Set l where
  leaf : {l u : A} → l ≤A u ≡ true → Bst l u
  node : {l l' u' u : A} → (d : A) → Bst l' d → Bst d u' →
         l ≤A l' ≡ true → u' ≤A u ≡ true →
         Bst l u


search : ∀ {l u} → (d : A) → Bst l u → Maybe (Σ A (λ d' → ((d isoBool d') _≤A_) ≡ true))
search d (leaf _) = nothing
search d (node d' l r _ _) with inspect (d ≤A d')
search d (node d' l r _ _) | true with≡ p₁ with inspect (d' ≤A d)
search d (node d' l r _ _) | true with≡ p₁ | true with≡ p₂ = just (d' , {!!})
search d (node d' l r _ _) | true with≡ p₁ | false with≡ p₂ = search d l
search d (node d' l r _ _) | false with≡ p₁ = search d r

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality using (_≅_; inspect; [_]; ≅-to-≡)
open import Data.Bool
open import Data.Maybe
open import Data.Product


module Bst2 {l} (A : Set l) (_≤A_ : A → A → Bool) where

_isoBool_ : A → A → (_≤A_ : A → A → Bool) → Bool
(d isoBool d') _≤_ = (d ≤ d') ∧ (d' ≤ d)

isoBool-intro : ∀ {_≤A_ x y} → x ≤A y ≡ true → y ≤A x ≡ true → ((x isoBool y) _≤A_) ≡ true
isoBool-intro {x = x} {y = y} p₁ p₂ rewrite p₁ | p₂ = refl

data Bst : A → A → Set l where
  leaf : {l u : A} → l ≤A u ≡ true → Bst l u
  node : {l l' u' u : A} → (d : A) → Bst l' d → Bst d u' →
         l ≤A l' ≡ true → u' ≤A u ≡ true →
         Bst l u

search : ∀ {l u} → (d : A) → Bst l u → Maybe (Σ A (λ d' → ((d isoBool d') _≤A_) ≡ true))
search d (leaf _) = nothing
search d (node d' l r _ _) with d ≤A d' | inspect (_≤A_ d) d'
search d (node d' l r _ _) | true  | [ eq ] with d' ≤A d | inspect (_≤A_ d') d
search d (node d' l r _ _) | true  | [ eq ] | true | [eq] = just (d , isoBool-intro {!!} {!!})
search d (node d' l r _ _) | true  | [ eq ] | false | [eq] = search d l
search d (node d' l r _ _) | false | [ eq ] = search d r