module Zoo4eg

id : {A : U} -> A -> A
id = \x => x   -- elaborated to \{A} x. x

-- implicit arg types can be omitted
const : {A B : U} -> A -> B -> A
const = \x y => x

-- function arguments can be grouped:
group1 : {A B : U}(x y z : A) -> B -> B
group1 = \x y z b => b

group2 : {A B : U}(x y z : A) -> B -> B
group2 = \x y z b => b

-- explicit id function used for annotation as in Idris
the : (A : _) -> A -> A
the = \_ x => x

-- implicit args can be explicitly given
-- NB kovacs left off the type (different syntax), so I put a hole in there
argTest1 : _
argTest1 = const {U} {U} U

-- I've decided not to do = in the {} for now.
-- let argTest2 = const {B = U} U;  -- only give B, the second implicit arg

-- again no type, this hits a lambda in infer.
-- I think we need to create two metas and make a pi of them.
insert2 : _
insert2 = (\{A} x => the A x) U -- (\{A} x => the A x) {U} U

Bool : U
Bool = (B : _) -> B -> B -> B

true : Bool
true = \B t f => t

false : Bool
false = \B t f => f

List : U -> U
List = \A => (L : _) -> (A -> L -> L) -> L -> L

nil : {A : U} -> List A
nil = \L cons nil => nil

cons : {A : U} -> A -> List A -> List A
cons = \ x xs L cons nil => cons x (xs L cons nil)

map : {A B : U} -> (A -> B) -> List A -> List B
map = \{A} {B} f xs L c n => xs L (\a => c (f a)) n

list1 : List Bool
list1 = cons true (cons false (cons true nil))

-- dependent function composition
comp : {A : U} {B : A -> U} {C : {a : A} -> B a -> U}
       (f : {a : A} (b : B a) -> C b)
       (g : (a : A) -> B a)
       (a : A)
       -> C (g a)
comp = \f g a => f (g a)

-- TODO unsolved metas in dependent function composition
-- compExample : List Bool
-- compExample = comp (cons true) (cons false) nil

Nat : U
Nat = (N : U) -> (N -> N) -> N -> N

mul : Nat -> Nat -> Nat
mul = \a b N s z => a _ (b _ s) z

ten : Nat
ten = \N s z => (s (s (s (s (s (s (s (s (s (s z))))))))))

hundred : _
hundred = mul ten ten

-- Leibniz equality
Eq : {A: U} -> A -> A -> U
Eq = \{A} x y => (P : A -> U) -> P x -> P y

refl : {A : U} {x : A} -> Eq x x
refl = \_ px => px

sym : {A x y : _} -> Eq {A} x y -> Eq y x
sym = \p => p (\y => Eq y x) refl

eqtest : Eq (mul ten ten) hundred
eqtest = refl