module Interpreter where 
{-@ LIQUID "--totality" @-}
data BinOp a = Plus | Times

data Exp a  = EConst Int | EBinOp (BinOp a) (Exp a) (Exp a)

data Instr a = IConst Int | IBinOp (BinOp a)

data List a = Nil | Cons a (List a)


{-@ autosize Prog @-}
data Prog a = Emp | PInst (Instr a) (Prog a)
type Stack = List Int

data SMaybe a = SNothing a | SJust a

{-@ measure binOpDenote @-}
binOpDenote :: Int -> Int -> BinOp a -> Int 
binOpDenote x y Plus  = (x+y)
binOpDenote x y Times = (x*y)

{-@ measure expDenote @-}
expDenote :: Exp a -> Int 
expDenote (EConst n)       = n
expDenote (EBinOp b e1 e2) = binOpDenote (expDenote e1) (expDenote e2) b

{-@foo :: s:Stack -> {v:SMaybe Stack| v = SNothing s || v = SJust s } @-}
foo :: Stack -> SMaybe Stack
foo = undefined 

{-@ measure instrDenote @-}
instrDenote :: Stack -> Instr a -> SMaybe Stack
{-@ instrDenote :: s:Stack -> i:{v:Instr a | isIBinOp v => lenL s >= 2} 
                -> {v:SMaybe {st:Stack | if (isIBinOp i) then (lenL st = lenL s - 1) else (lenL st = lenL s + 1)} | v = instrDenote s i} @-}
instrDenote s (IConst n) = SJust (Cons n s)
instrDenote s (IBinOp b) = 
	let x  = headL s in 
	let s1 = tailL s in 
	let y  = headL s1 in 
	let s2 = tailL s1 in 
	SJust (Cons (binOpDenote x y b) s2)


{-@ invariant {v:Prog a | binOps v >= 0} @-}
{-@ measure binOps @-}
binOps :: Prog a -> Int 
binOps Emp = 0 
binOps (PInst x xs) = if isIBinOp x then 1 + (binOps xs) else binOps xs 



{- measure progDenote :: Stack -> Prog -> SMaybe Stack @-}
{-@ measure progDenote @-}
{-@ Decrease progDenote 2 @-}
progDenote :: Stack -> Prog a -> SMaybe Stack
{-@ progDenote :: s:Stack -> p:{v:Prog a | lenL s >= 2 * binOps v }  -> {v: SMaybe Stack | v = progDenote s p} @-}
progDenote s Emp = SJust s
progDenote s (PInst x xs) = SNothing s 
{-
progDenote s (PInst x xs) | SJust s' <- instrDenote s x = progDenote s' xs
                          | otherwise                   = SNothing s
-}

{-
{- compile :: e:Exp -> {v:Prog | (progDenote Nil v) == Nothing } @-}
{- compile :: e:Exp -> {v:Prog | (progDenote Nil v) == Just (Cons (expDenote e) Nil)} @-}
compile :: Exp -> Prog
compile (EConst n)       = single (IConst n)  
compile (EBinOp b e1 e2) = compile e2 `append` compile e1 `append` (single $ IBinOp b) 

-}



-- Hard Wire the measures so that I can provide exact types for Nil and Cons
{-@ SNothing :: s:s -> {v:SMaybe s | v = SNothing s && not (isSJust v)} @-}
{-@ SJust    :: s:s -> {v:SMaybe s | v = SJust s && (isSJust v) && (fromSJust v = s)} @-}
{-@ Cons     :: x:a -> xs:List a -> {v:List a | v = Cons x xs && headL v = x && tailL v = xs && lenL v = 1 + lenL xs} @-}
{-@ Nil      :: {v:List a | v = Nil  && lenL v = 0} @-}
iconst = IConst


{-@ measure isSJust :: SMaybe a -> Prop @-}
{-@ isSJust :: x:SMaybe a -> {v:Bool | Prop v <=> isSJust x}  @-}
isSJust (SJust _) = True 
isSJust (SNothing _ ) = False

{-@ measure fromSJust :: SMaybe a -> a @-}
{-@ fromSJust :: x:{v:SMaybe a | isSJust v} -> {v:a | v = fromSJust x}  @-}
fromSJust (SJust x) = x

{-@ measure isIBinOp @-}
isIBinOp (IBinOp _) = True
isIBinOp _          = False

{-@ measure headL :: List a -> a @-}
{-@ headL :: xs:{v:List a | lenL v > 0} -> {v:a | v = headL xs} @-}
headL :: List a -> a
headL (Cons x _) = x

{-@ measure tailL :: List a -> List a @-}
{-@ tailL :: xs:{v:List a | lenL v > 0} -> {v: List a | v = tailL xs && lenL v = lenL xs - 1} @-}
tailL :: List a -> List a
tailL (Cons _ xs) = xs


{-@ measure lenL :: List a -> Int @-}
{-@ invariant {v:List a | lenL v >= 0 } @-}
lenL :: List a -> Int 
lenL (Cons _ xs) = 1 + lenL xs 
lenL Nil         = 0 



-- List operations
{-@ autosize Exp @-}
{-@ data List [lenL] @-}

(Cons x xs) `append` ys = cons x $ append xs ys
Nil         `append` ys = ys 

emp      = Nil
single x = Cons x Nil
cons x xs = Cons x xs