module AiPL-Live where

{- caution if-then-else -}

{- honesty as a policy -}

{- binary search trees viewed from below -}

{- a bit of propositions as types
     an empty type of evidence for false things
     an inhabited type of evidencefor true things
-}

data Zero : Set where
record One : Set where constructor <>

data Nat : Set where
  ze : Nat
  su : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}

{- now compute the type of evidence for inequality -}

_<=_ : Nat -> Nat -> Set
ze <= y = One
su x <= ze = Zero
su x <= su y = x <= y

check : 4 <= y <= x 5
check = <>

data _+_ (S T : Set) : Set where
  inl : S -> S + T
  inr : T -> S + T

total : (x y : Nat) -> (x <= y) + (y <= x)
total ze y = inl <>
total (su x) ze = inr <>
total (su x) (su y) = total x y

{- extend a type with top and bottom elements -}

data Bnd (X : Set) : Set where
  bot : Bnd X
  val : X -> Bnd X
  top : Bnd X

{- extend inequality accordingly (note that Nat is just an example) -}

_<B=_ : Bnd Nat -> Bnd Nat -> Set
bot   <B= y      = One
_     <B= top    = One
val x <B= val y  = x <= y
_     <B= _      = Zero

{- so what's a binary search tree? -}

      -- vvvvvvvvvvvvvvv indices scoping over all constructors.
data BST (l u : Bnd Nat) : Set where
  leaf : l <B= u -> BST l u
  node : (x : Nat) -> BST l (val x) -> BST (val x) u -> BST l u

SomeBST : Set
SomeBST = BST bot top

{-
good : SomeBST
good = {!-l!}
-}

{-
insert0 : Nat -> SomeBST -> SomeBST
insert0 y t = ?
-}

{- dependent pairs -}

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst  -- type of second field depends on value of first
open Sg public -- "open" means "bring fst and snd into scope"
               -- "public" means files importing this module get fst and snd
infixr 4 _,_
_*_ : Set -> Set -> Set
S * T = Sg S (\ _ -> T)

Intv : Bnd Nat -> Bnd Nat -> Set
Intv l u = Sg Nat \ x -> (l <B= val x) * (val x <B= u)

insert : {l u : Bnd Nat} -> Intv l u -> BST l u -> BST l u
insert (y , ly , yu) (leaf lu) = node y (leaf ly) (leaf yu)
insert (y , ly , yu) (node x lx xu) with total y x
insert (y , ly , yu) (node x lx xu) | inl yx with insert (y , ly , yx) lx
... | r = node x r xu
insert (y , ly , yu) (node x lx xu) | inr xy with insert (y , xy , yu) xu
... | r = node x lx r

data OList (l u : Bnd Nat) : Set where
  nil : OList l u
  cons : OList l u

glueIn : forall {l u} y -> OList l (val y) -> OList (val y) u -> OList l u
glueIn y ly yu = {!!}

flatten : forall {l u} -> BST l u -> OList l u
flatten t = {!!}




data U : Set where
  `0 `1 : U
  _`+_ _`*X*_ : (S T : U) -> U
  `R : U

{- unpack this later
record Guess (X : Set) : Set where
  constructor !
  field
    {{guess}} : X  -- this field is hidden, to be inferred from context
-}

Body : U -> (Bnd Nat -> Bnd Nat -> Set) ->  (Bnd Nat -> Bnd Nat -> Set)
Body `0 R l u = Zero
Body `1 R l u = (l <B= u)
Body (S `+ T) R l u = Body S R l u + Body T R l u
Body (S `*X* T) R l u = Sg Nat \ x -> Body S R l (val x) * Body T R (val x) u
Body `R R l u = R l u

data Mu (F : U)(l u : Bnd Nat) : Set where
  [_] : Body F (Mu F) l u -> Mu F l u

IntvU : U
IntvU = `1 `*X* `1

iv : forall {l u} x -> l <B= val x -> val x <B= u -> Mu IntvU l u
iv = {!!}

BSTU : U
BSTU = `1 `+ (`R `*X* `R)

leafu :  forall {l u}(lu : l <B= u) -> Mu BSTU l u
leafu = {!!}
nodeu : forall {l u}(x : Nat)(lx : Mu BSTU l (val x))(xu : Mu BSTU (val x) u)
   -> Mu BSTU l u
nodeu x lx xu = {!!}

ListU : U
ListU = `1 `+ (`1 `*X* `R)