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 : Stack ty -> Stack r) -> 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 : (Stack ty -> Stack r) -> Stack ds -> Stack ((F ty r) :: ds)
quote f = PushFn f

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

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

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

swap : Stack (x :: y :: d) -> Stack (y :: x :: d)
swap (PushFn x (PushFn y s)) = PushFn y (PushFn x s)
swap (PushFn x (PushVal y s)) = PushVal y (PushFn x s)
swap (PushVal x (PushVal y s)) = PushVal y (PushVal x s)
swap (PushVal x (PushFn y s)) = PushFn y (PushVal x s)

dip : Stack ((F f r) :: x :: f) -> (Stack (x :: r))
dip (PushFn g (PushVal x y)) = PushVal x (g y)
dip (PushFn g (PushFn x y)) = PushFn x (g y)

-- compose : (n : Nat) -> {0 s : Vect n Discrim} -> Stack ((F f r) :: (F f' 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)) -> Stack (r ++ r)
-- both (PushFn g s) = append (g (takeN n s)) (append (g (takeN n (popN n s))) (popN n (popN n s)))
-- both (PushFn g s) = append (takeN n' (?hole1 (takeN n s))) (?hole2 (takeN n (popN n s)))
-- both (PushFn g s) = append (g (takeN n s)) (append (g (takeN n (popN n s))) (popN n (popN n s)))

add : Stack ([V Nat, V Nat] ++ r) -> Stack ([V Nat] ++ r)
add (PushVal x z) = case z of (PushVal y st) =>  PushVal (x + y) st


-- specialCompose : (Stack x -> Stack y) -> (Stack x' -> y') -> (Stack ?x -> Stack ?y)

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


main : IO ()
main = putStrLn "a"