module Main

data Discrim = V Type | F (List Discrim) Discrim

Sig : Type
Sig = List Discrim

data Stack : List Discrim -> Type where
    Bot : Stack []
    PushVal : {t : Type} -> (a : t) -> (Stack d) -> Stack ((V t) :: d)
    PushFn : {ty : Sig} -> {r : Discrim} -> (fn : {other : Sig} -> Stack (ty ++ other) -> Stack (r :: other)) -> (Stack ds) -> Stack ((F ty r) :: ds)

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

quote : {ty : Sig} -> {r : Discrim} -> ({d : Sig} -> Stack (ty ++ d) -> Stack (r :: d)) -> Stack ds -> Stack ((F ty r) :: ds)
quote f = PushFn f

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

-- compose : {rest :Sig} -> Stack ((F f r) :: (F g r') :: (f ++ g ++ rest)) -> (Stack ((F ) :: rest))
-- compose (PushFn f s) = case s of (PushFn g s') => quote {ty = ?idk} (f . g) s'


add : {other : Sig} -> Stack (V Nat :: V Nat :: other) -> Stack (V Nat :: other)
add (PushVal x z) = case z of (PushVal y st) =>  PushVal (x + y) st

main : IO ()
main = putStrLn "a"