content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--prune-unsorted" @-}
  
  -- From: https://github.com/jstolarek/sandbox/blob/master/agda/agda-curious
  
  module StackMachine where
  
  import Prelude hiding (max)
  
  type Val   = Int
  data Expr  = EVal Val | EAdd Expr Expr
  data Instr = Push Val | Add
  
  eval :: Expr -> Val
  eval (EVal v)     = v
  eval (EAdd e1 e2) = eval e1 + eval e2
  
  compile :: Expr -> [Instr]
  compile (EVal v)     = [Push v]
  compile (EAdd e1 e2) = compile e1 ++ compile e2 ++ [Add]
  
  {-@ run :: is:[Instr] -> {v:[Val] | len v >= needs is} -> [Val] @-}
  run :: [Instr] -> [Val] -> [Val]
  run (Add    : is) (v1:v2:vs) = run is ((v1 + v2) : vs)
  run (Push v : is) vs         = run is (    v     : vs)
  run []            vs         = vs
  run (Add    : _ ) _          = die "impossible"
  
  {-@ die :: {v:String | false} -> a @-}
  die :: String -> a
  die = error
  
  {-@ measure needs @-}
  needs :: [Instr] -> Int
  needs (i:is) = max (pops i) ((needs is) - (pushes i))
  needs []     = 0
  
  {-@ measure pops @-}
  pops :: Instr -> Int
  pops Add      = 2
  pops (Push _) = 0
  
  {-@ measure pushes @-}
  pushes :: Instr -> Int
  pushes Add      = (-1)
  pushes (Push _) = 1
  
  {-@ inline max @-}
  max :: Int -> Int -> Int
  max x y = if x > y then x else y
  
  {-
  
  Some intuition / examples about `need`
  
  needs []
    = 0
  needs [Add]
    = max 2 (0 + 1)
    = 2
  needs [Add, Add]
    = max 2 (2 + 1)
    = 3
  needs [Add, Add, Add]
    = max 2 (3 + 1)
    = 4
  
  
  needs [                              add ]
    = 2
  
  needs [                      push 4, add ]
    = max 0 (2 - 1)
    = 1
  
  needs [                 add, push 4, add ]
    = max 2 (1 + 1)
    = 2
  
  needs [         push 3, add, push 4, add ]
    = max 0 (2 - 1)
    = 1
  
  needs [ push 2, push 3, add, push 4, add ]
    = max 0 (1 - 1)
    = 0
  
  -}
  
  {- THEOREMS TODO
   
  thm :: e:Expr -> { run (compile e) [] == [eval e] }
  thm e vs
    = run (compile e) []
   .= run (compile e ++ []) []  `by` append_right_nil (compile e)
   .= run [] (eval e : [])      `by` lem e [] []
   .= [eval e]
   ** QED
  
  lem :: e:Expr -> is:[Instr] -> vs:[Val]
        -> { run (compile e ++ is) vs == run is (eval e : vs) }
  
  lem (Val v) is vs
    = run (compile (Val v) ++ is) vs
   .= run ([Push v] ++ is) vs
   .= run (Push v : is) vs       `eval` (++)
   .= v : vs
   ** QED
  
  lem (Add e1 e2) is vs
    = run (compile (Add e1 e2) ++ is) vs
   .= run (compile e1 ++ compile e2 ++ [Add] ++ is) vs
   .= run (compile e2 ++ [Add] ++ is) (eval e1 : vs)  `by`   (lem ...)
   .= run ([Add] ++ is) (eval e2 : eval e1 : vs)      `by`   (lem ...)
   .= run (Add : is) (eval e2 : eval e1 : vs)         `eval` (++)
   .= run is ((eval e1 + eval e1) : vs)
   ** QED
  
   -}
  