content: {-@ LIQUID "--exact-data-con" @-}
  {-@ LIQUID "--higherorder"    @-}
  {-@ LIQUID "--ple"            @-} 
  {-@ LIQUID "--no-totality"    @-} 
  
  module Compiler where
  
  import Language.Haskell.Liquid.ProofCombinators
  
  -- | Expressions ---------------------------------------------------------------
  
  {-@ data Expr [eSize] @-}
  data Expr
    = Val Int
    | Add Expr Expr
  
  {-@ measure eSize @-}
  {-@ eSize :: Expr -> {v:Int | 1 <= v} @-}
  eSize :: Expr -> Int
  eSize (Val n)     = 1
  eSize (Add e1 e2) = 1 + eSize e1 + eSize e2
  
  {-@ invariant {v:Expr | 1 <= eSize v } @-}
  
  -- | Interpreter ---------------------------------------------------------------
  
  {-@ reflect interp @-}
  interp :: Expr -> Int
  interp (Val n)     = n
  interp (Add e1 e2) = interp e1 + interp e2
  
  -- | Code ----------------------------------------------------------------------
  
  {-@ data Code [cSize] @-}
  data Code
    = HALT
    | PUSH Int Code
    | ADD      Code
  
  {-@ measure cSize @-}
  {-@ cSize :: Code -> Nat @-}
  cSize :: Code -> Int
  cSize HALT       = 0
  cSize (PUSH n c) = 1 + cSize c
  cSize (ADD    c) = 1 + cSize c
  
  -- | Stack ---------------------------------------------------------------------
  data Stack
    = Emp
    | Arg Int Stack
  
  -- | Compiler ------------------------------------------------------------------
  
  {-@ reflect compileC @-}
  compileC :: Expr -> Code -> Code
  compileC (Val n) c     = PUSH n c
  compileC (Add e1 e2) c = compileC e2 (compileC e1 (ADD c))
  
  {-@ reflect compile @-}
  compile :: Expr -> Code
  compile e = compileC e HALT
  
  -- | VM ------------------------------------------------------------------------
  
  {-@ reflect run @-}
  run :: Code -> Stack -> Int
  run HALT       (Arg n s)         = n
  run (ADD c)    (Arg n (Arg m s)) = run c (Arg (n + m) s)
  run (PUSH n c) s                 = run c (Arg n       s)
  
  {-@ reflect compileAndRun @-}
  compileAndRun :: Expr -> Int
  compileAndRun e = run (compileC e HALT) Emp
  
  -- | Correctness ---------------------------------------------------------------
  
  {-@ thmCompileC :: e:Expr -> c:Code -> s:Stack ->
        { run (compileC e c) s = run c (Arg (interp e) s) }
    @-}
  thmCompileC :: Expr -> Code -> Stack -> Proof
  thmCompileC (Val n)     c s =  () 
  thmCompileC (Add e1 e2) c s =  thmCompileC e2 (compileC e1  (ADD c)) s
                             &&& thmCompileC e1 (ADD c) (Arg (interp e2) s)
  
  {-@ thmCompileAndRun :: e:Expr -> { compileAndRun e == interp e } @-}
  thmCompileAndRun :: Expr -> Proof
  thmCompileAndRun e = thmCompileC e HALT Emp
  
  
  {- thmCompileC (Add e1 e2) c s
     = [ -- run (compileC (Add e1 e2) c) s
        -- ==. run (compileC e2 (compileC e1 (ADD c))) s
        {- ? -} thmCompileC e2 (compileC e1  (ADD c)) s
        -- ==. run (compileC e1 (ADD c)) (Arg (interp e2) s)
      , {- ? -} thmCompileC e1 (ADD c) (Arg (interp e2) s)
        -- ==. run (ADD c) (Arg (interp e1) (Arg (interp e2) s))
        -- ==. run c (Arg (interp e1 + interp e2) s)
        -- ==. run c (Arg (interp (Add e1 e2)) s)
      ] *** QED
   -}
  
  
  
  
  
  
  
  ---
  