module Main
import Data.Vect

data Discrim = V Type | F (Vect n Discrim) (Vect n' Discrim)

Sig : Nat -> Type
Sig n = Vect n Discrim

data Stack : Vect n Discrim -> Type where
    Bot : Stack Nil
    PushVal : {0 t : Type} -> (a : t) -> (Stack d) -> Stack ((V t) :: d)
    PushFn : (fn : forall n. {0 rest : Vect n Discrim} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds)

push : {0 t : Type} -> (a : t) -> Stack d -> Stack ((V t) :: d)
push x y = PushVal x y

quote : (forall n. {0 rest : Sig n} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds)
quote f = PushFn f

dup : Stack (x :: rest) -> Stack (x :: x :: rest)
dup (PushVal x s) = (push x . push x) s
dup (PushFn x s) = (quote x . quote x) s

call : Stack ((F f r) :: (f ++ rest)) -> (Stack (r ++ rest))
call (PushFn g y) = g y

pop : Stack (x :: rest) -> Stack rest
pop (PushVal x s) = s
pop (PushFn x s) = s

compose : Stack ((F f r) :: (F r r') :: rest) -> (Stack ((F f r') :: rest))
compose (PushFn f s) = case s of (PushFn g s') => PushFn (g . f) s'

append : Stack x -> Stack y -> Stack (x ++ y)
append Bot s' = s'
append (PushVal x s) s' = PushVal x (append s s')
append (PushFn g s) s' = PushFn g (append s s')

popN : (n : Nat) -> {0 s : Vect n Discrim} -> Stack (s ++ s') -> Stack s'
popN 0 {s = []} st = st
popN (S n) {s = _ :: _} (PushVal x st) = popN n st
popN (S n) {s = _ :: _} (PushFn x st) = popN n st

takeN : (n : Nat) -> {0 s : Vect n Discrim} -> Stack (s ++ s') -> Stack s
takeN 0 {s = []} _ = Bot
takeN (S n) {s = _ :: _} (PushVal x st) = PushVal x (takeN n st)
takeN (S n) {s = _ :: _} (PushFn x st) = PushFn x (takeN n st)

both : {n : Nat} -> {n' : Nat} -> {f : Sig n} -> {r : Sig n'} -> Stack ((F f r) :: (f ++ f ++ rest)) -> Stack (r ++ r ++ rest)
both (PushFn g s) = append (takeN n' (g s)) (g (popN n s))

add : Stack (V Nat :: V Nat :: rest) -> Stack (V Nat :: rest)
add (PushVal x z) = case z of (PushVal y st) =>  PushVal (x + y) st

-- sum3 : ?
-- sum3 = add . add


main : IO ()
main = putStrLn "a"