stack.idr

module Main

PosInt : Type
PosInt = Nat

data Inst : PosInt -> PosInt -> Type where
  PUSH : (v:Int) -> Inst n       (1 + n)
  ADD  :            Inst (2 + n) (1 + n)

data Prog : PosInt -> PosInt -> Type where
  Nil  :                         Prog i i
  (::) : Inst i j -> Prog j k -> Prog i k

run : Prog i j -> Vect i Int -> Vect j Int
run []              vs               = vs
run (PUSH v :: is)  vs               = run is (v :: vs)
run (ADD    :: is)  (v2 :: v1 :: vs) = run is (v1 + v2 :: vs)

main : IO ()
main = do
  print $ run [PUSH 4, PUSH (-5), ADD] []
  print $ run [ADD] [4, -5]
  -- print $ run [ADD] [] -- won't compile
  -- print $ run [ADD] [-5] -- won't compile


-- if prog = [ADD] and vs = [4,5], i = 2, (n + 2) = 2, n = Z, j = 1 : OK
-- if prog = [ADD] and vs = [],    i = Z, (n + 2) = Z               : IMPOSSIBLE