{- | Symbolic Execution for MiniDafny |
   ================================
-}

module SymbEx where

{- |

Symbolic execution is a technique for analyzing programs that allows
us to reason about what kinds of inputs lead to the execution of
particular parts of a program. The core idea is to build an
interpreter that operates, not on concrete, but on symbolic
representations of variables. 

-}

import Control.Monad (when,guard,forM_)
import Data.Map (Map, (!?))
import qualified Data.Map as Map
import Control.Monad.State
import Test.HUnit (Test(..), (~?=), (~:), runTestTT, Counts)
import qualified Data.List as List
import Data.Maybe (fromMaybe)
import Text.Read(readMaybe)

import Syntax
import Printer
import Z3 (convertAndCheck)

-- | Our store is now SYMBOLIC. Maps to expressions, not values.
type Store = Map Name Expression
-- | We record our path as an expression that holds down the path we've taken.
type Path = Expression

initialStore :: Store
initialStore = Map.empty

-- | State Monad over IO, state is combination of current environment and path.
type Eval = StateT (Store, Path) IO

-- | Helper function to print current context and path
printInContext :: String -> Eval ()
printInContext msg = do
  (s,p) <- get
  lift $ putStrLn msg
  lift $ putStrLn "Context:"
  forM_ (Map.assocs s) (\(x,e) ->  lift $ putStrLn $ x ++ " |-> " ++ pretty e) 
  lift $ putStrLn $ "Path: " ++ pretty p

-- | Same block as in previous homework!
eval :: Block -> Eval ()
eval (Block ss) = mapM_ evalS ss

-- | SMT-Based helpers
isTautology :: String -> Expression -> Eval Bool
isTautology str e = do
  (s, _) <- get :: Eval (Store, Path)
  let ps = map (\(x,e) -> Forall [] (Op2 (Var (Name x)) Eq e)) (Map.assocs s)
  lift $ convertAndCheck ps (Forall [] e) str

isSatisfiable :: String -> Expression -> Eval Bool
isSatisfiable str e = not <$> isTautology str (Op1 Not e)

evalS :: Statement -> Eval ()
evalS st = undefined
--evalS (While _ e ss) = error "While loops not supported"
--evalS (Assign (Proj _ _) _) = error "arrays not supported"

evalM :: Method -> IO ()
evalM (Method f _ _ _ ss) = do
  -- Spec?
  (s,p) <- execStateT (eval ss) (Map.empty, Val $ BoolVal True)
  return ()