Demo

module Demo where

data Bool : Set where
  True : Bool
  False : Bool

not : Bool -> Bool
not True = False
not False = True

if_then_else_ : Bool -> Bool -> Bool -> Bool
if True then t else e = t
if False then t else e = e

data Nat : Set where
  Zero : Nat
  Succ : Nat → Nat

_+_ : Nat → Nat → Nat
Zero + y = y
Succ x + y = Succ (x + y)

{-# BUILTIN NATURAL Nat #-}


postulate
  Char : Set

{-# BUILTIN CHAR Char #-}

cond : ∀ {a : Set} -> Bool -> a -> a -> a
cond True t e = t
cond False t e = e

test : Nat
test = cond True 3 45

id : ∀ {a : Set} -> a -> a 
id x = x

data List (a : Set) : Set where
  Nil : List a 
  Cons : a -> List a -> List a

_++_ : {a : Set} -> List a -> List a -> List a
Nil ++ ys = ys
Cons x xs ++ ys = Cons x (xs ++ ys)

xs : List Nat
xs = Cons 3 (Cons 4 (Cons 5 Nil))


map : {a b : Set} -> (a -> b) -> List a -> List b
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just : a -> Maybe a

_!!_ : {a : Set} -> List a -> Nat -> Maybe a
Nil !! Zero = Nothing
Cons x xs !! Zero = Just x
Nil !! Succ i = Nothing
Cons x xs !! Succ i = xs !! i

length : {a : Set} -> List a -> Nat
length Nil = Zero
length (Cons x xs) = Succ (length xs)

data _<_ : Nat -> Nat -> Set where
  Base : forall {n} -> Zero < Succ n
  Step : ∀ {n m} -> n < m -> Succ n < Succ m

lemma : 3 < 6
lemma = Step (Step (Step Base))

impossible : {a : Set} -> (n : Nat) -> n < Zero -> a
impossible n ()

lookup : {a : Set} -> (n : Nat) -> (xs : List a) -> n < length xs -> a
lookup n Nil ()
lookup Zero (Cons x xs) p = x
lookup (Succ n) (Cons x xs) (Step p) = lookup n xs p

data Vec (a : Set) : Nat -> Set where
  Nil : Vec a Zero
  Cons : {n : Nat} -> a -> Vec a n -> Vec a (Succ n)

head : {a : Set} -> (xs : List a) -> 0 < length xs -> a
head Nil ()
head (Cons x xs) p = x

vhead : {a : Set} {n : Nat} -> Vec a (Succ n) -> a
vhead (Cons x xs) = x

vlookup : {a : Set} {n : Nat} -> Vec a n -> (m : Nat) -> m < n -> a
vlookup Nil m ()
vlookup (Cons x xs) Zero p = x
vlookup (Cons x xs) (Succ n) (Step p) = vlookup xs n p

data Fin : Nat -> Set where
  FZero : {n : Nat} -> Fin (Succ n)
  FSucc : {n : Nat} -> Fin n -> Fin (Succ n)

vlookup' : {a : Set} {n : Nat} -> Vec a n -> Fin n -> a
vlookup' (Cons x xs) FZero = x
vlookup' (Cons x xs) (FSucc i) = vlookup' xs i

vappend : (a : Set) (n m : Nat) -> Vec a n -> Vec a m -> Vec a (n + m)
vappend a .Zero m Nil ys = ys
vappend a .(Succ k) m (Cons {k} x xs) ys = Cons x (vappend a k m xs ys)


data _==_ : Nat -> Nat -> Set where
  Refl : {n : Nat} -> n == n

q : 1 == 1
q = Refl 

r : (0 + (1 + 2)) == (3 + 0)
r = Refl

q' : (n : Nat) -> (Zero + n) == n
q' n = Refl

sym : (x y : Nat) -> x == y -> y == x
sym x .x Refl = Refl

trans : {x y z : Nat} -> x == y -> y == z -> x == z
trans Refl q = q

cong : {x y : Nat} -> (f : Nat -> Nat) -> x == y -> f x == f y
cong f Refl = Refl

plus-zero : (n : Nat) -> (n + Zero) == n
plus-zero Zero = Refl
plus-zero (Succ n) = let ih = plus-zero n in cong Succ ih

infixr 2 _⟨_⟩_
_⟨_⟩_ : (x : Nat) -> { y z : Nat} -> x == y -> y == z -> x == z
_⟨_⟩_ x = trans

_■ : forall x -> x == x
_■ x = Refl

plus-zero' : (n : Nat) -> (n + Zero) == n
plus-zero' Zero = Refl
plus-zero' (Succ n) = 
  (Succ n) + Zero
    ⟨ Refl ⟩
  Succ (n + Zero)
    ⟨ cong Succ (plus-zero' n) ⟩
  Succ n ■

foo : (x y : Nat) -> x == (y + 4) -> (y + 4) == x
foo .(y + 4) y Refl = Refl

data Either (a b : Set) : Set where
  Inl : a -> Either a b
  Inr : b -> Either a b

data Empty : Set where

Not : Set -> Set
Not a  = a -> Empty

bar : Not (0 == 1)
bar ()

zs-lemma : (y : Nat) -> (Not (Zero == Succ y))
zs-lemma y ()

eq : (x y : Nat) -> Either (x == y) (Not (x == y))
eq Zero Zero = Inl Refl
eq Zero (Succ y) = Inr (λ () )
eq (Succ x) Zero = Inr (λ ())
eq (Succ x) (Succ y) with eq x y
eq (Succ .y) (Succ y)| Inl Refl = Inl Refl
... | Inr q = Inr (\sxy -> q (h sxy))
  where
  h : {x y : Nat} -> Succ x == Succ y -> x == y
  h Refl = Refl

filter : {a : Set} -> (a -> Bool) -> List a -> List a
filter p Nil = Nil
filter p (Cons x xs) with p x
filter p (Cons x xs) | True = Cons x (filter p xs)
filter p (Cons x xs) | False = filter p xs

data SubList {a : Set} : List a -> List a -> Set where
  Base : {xs : List a} -> SubList Nil xs
  Keep : forall {x xs ys} -> SubList xs ys -> SubList (Cons x xs) (Cons x ys)
  Drop : forall {y xs ys} -> SubList xs ys -> SubList xs (Cons y ys)

exampleSL : SubList (Cons 1 Nil) (Cons 2 (Cons 1 (Cons 3 Nil)))
exampleSL = Drop (Keep Base)

filter-lemma : {a : Set} -> (p : a -> Bool) -> (xs : List a) -> SubList (filter p xs) xs
filter-lemma p Nil = Base
filter-lemma p (Cons x xs) with p x
filter-lemma p (Cons x xs) | True = Keep (filter-lemma p xs)
filter-lemma p (Cons x xs) | False = Drop (filter-lemma p xs)



silly : 3 < 1 -> 1 == 2
silly (Step ())

exfalso : Empty -> {a : Set} ->  a
exfalso ()

undefined : {a : Set} -> a
undefined = {!!}

data Unit : Set where
  tt : Unit

printfType : List Char -> Set
printfType Nil = Unit
printfType (Cons x Nil) = Unit
printfType (Cons '%' (Cons 'd' cs)) = Nat -> printfType cs
printfType (Cons '%' (Cons 's' cs)) = List Char -> printfType cs
printfType (Cons x (Cons c cs)) = printfType (Cons c cs)

printf : (string : List Char) -> printfType string
printf str = {!!}

data U : Set where
  FOO : U
  BOOL : U
  EITHER : U -> U -> U

el : U -> Set
el FOO = Nat 
el BOOL = Bool
el (EITHER u u₁) = Either (el u) (el u₁)

eqA : (a : Set) -> a -> a -> Bool
eqA a x y = {!a!}

eqU : {u : U} -> el u -> el u -> Bool
eqU {FOO} = {!eqNat x y!}
eqU {BOOL} = {!eqBool x y!}
eqU {EITHER u u₁} = {!eqEither ....!}

eqExample : Bool
eqExample = eqU  3 3

double : Nat -> Nat
double Zero = Zero
double (Succ n) = Succ (Succ (double n))

data OddEven : Nat -> Set where
  IsOdd : (k : Nat) -> OddEven (Succ (double k))
  IsEven : (k : Nat) -> OddEven (double k)

check? : (n : Nat) -> OddEven n
check? Zero = IsEven Zero
check? (Succ Zero) = IsOdd Zero
check? (Succ (Succ n)) with check? n
check? (Succ (Succ .(Succ (double k)))) | IsOdd k = IsOdd (Succ k)
check? (Succ (Succ .(double k))) | IsEven k = IsEven (Succ k)

div2 : (n : Nat) -> Nat
div2 n with check? n
div2 .(Succ (double k)) | IsOdd k = k
div2 .(double k) | IsEven k = k 

natLemma : {P : Nat -> Set} -> (n : Nat) -> P n
natLemma n with check? n
natLemma ._ | IsOdd k = {!!}
natLemma ._ | IsEven k = {!!} 

forget : {n : Nat} -> Fin n -> Nat
forget i = {!!}

data Bounded (bound : Nat) : Nat -> Set where
  InBound : (i : Fin bound) -> Bounded bound (forget i)
  OutOfBounds : (n : Nat) -> Bounded bound ((Succ n) + bound)

boundCheck? : (bound : Nat) -> (n : Nat) -> Bounded bound n
boundCheck? bound n = {!!}

safelookup : {a : Set} {bound : Nat} -> Vec a bound -> Nat -> Maybe a
safelookup {a} {bound} xs n with boundCheck? bound n
safelookup xs ._ | InBound i = {!!}
safelookup xs ._ | OutOfBounds n = {!!}







data Ty : Set where
  I : Ty
  _=>_ : Ty -> Ty -> Ty

elTy : Ty -> Set
elTy I = Unit
elTy (ty => ty₁) = elTy ty -> elTy ty₁

Context : Set
Context = List Ty

data Ref : Context -> Ty -> Set where
  Top : forall {ctx ty} -> Ref (Cons ty ctx) ty
  Pop : forall {ctx ty ty'} -> Ref ctx ty -> Ref (Cons ty' ctx) ty

data Term : Context -> Ty -> Set where
  Var : forall {ctx ty} -> Ref ctx ty -> Term ctx ty
  Lam : forall {ctx s t} -> Term (Cons s ctx) t -> Term ctx (s => t )
  App : forall {ctx s t} -> Term ctx (s => t) -> Term ctx s -> Term ctx t

data Env : Context -> Set where
  Cons : forall {ty ctx} -> elTy ty -> Env ctx -> Env (Cons ty ctx)
  Nil : Env Nil

envLookup : forall {ctx ty} -> Ref ctx ty -> Env ctx -> elTy ty
envLookup Top (Cons x env) = x
envLookup (Pop r) (Cons x env) = envLookup r env

eval : forall {ctx ty} -> Term ctx ty -> Env ctx -> elTy ty
eval (Var x) env = envLookup x env
eval (Lam body) env = \x -> eval body (Cons x env)
eval (App t1 t2) env = let f = eval t1 env in
                   let x = eval t2 env
                   in f x