{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE BangPatterns #-}
module Language.Haskell.Liquid.Synthesize.Check (check, hasType, isWellTyped, checkError) where


import           Language.Fixpoint.Types.Constraints
import qualified Language.Fixpoint.Types.Config
                                               as F
import qualified Language.Fixpoint.Types       as F
import           Language.Fixpoint.Solver
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Generate
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Fresh
                                                ( trueTy )
import           Language.Haskell.Liquid.Constraint.ToFixpoint
import           Language.Haskell.Liquid.Synthesize.Monad
import           Language.Haskell.Liquid.Synthesize.GHC
import           Language.Haskell.Liquid.Misc   ( mapThd3 )
import           CoreSyn
import           Var
import           Control.Monad.State.Lazy
import           System.Console.CmdArgs.Verbosity
import           CoreUtils
import           Language.Haskell.Liquid.GHC.TypeRep
import           Language.Haskell.Liquid.Types
import           MkCore
import           DynFlags

hasType :: SpecType -> CoreExpr -> SM Bool
hasType :: SpecType -> CoreExpr -> SM Bool
hasType SpecType
t !CoreExpr
e' = String -> SM Bool -> SM Bool
forall a. String -> a -> a
notrace (String
" [ Check ] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show CoreExpr
e') (SM Bool -> SM Bool) -> SM Bool -> SM Bool
forall a b. (a -> b) -> a -> b
$ do 
  Var
x  <- SpecType -> SM Var
freshVar SpecType
t 
  SState
st <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
  let tpOfE :: Type
tpOfE = CoreExpr -> Type
exprType CoreExpr
e'
      ht :: Type
ht    = SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t
  if Type
tpOfE Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ht
    then IO Bool -> SM Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> SM Bool) -> IO Bool -> SM Bool
forall a b. (a -> b) -> a -> b
$ IO Bool -> IO Bool
forall a. IO a -> IO a
quietly (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ CGInfo
-> CGEnv -> Config -> Var -> CoreExpr -> Maybe SpecType -> IO Bool
check (SState -> CGInfo
sCGI SState
st) (SState -> CGEnv
sCGEnv SState
st) (SState -> Config
sFCfg SState
st) Var
x CoreExpr
e (SpecType -> Maybe SpecType
forall a. a -> Maybe a
Just SpecType
t) 
    else String -> SM Bool
forall a. HasCallStack => String -> a
error (String -> SM Bool) -> String -> SM Bool
forall a b. (a -> b) -> a -> b
$ String
" [ hasType ] Expression = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show CoreExpr
e' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showTy Type
tpOfE String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" , specType = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. Show a => a -> String
show SpecType
t
 where e :: CoreExpr
e = CoreExpr -> CoreExpr
tx CoreExpr
e' 

-- Returns true if the expression is well-typed.
isWellTyped :: CoreExpr -> SM Bool
isWellTyped :: CoreExpr -> SM Bool
isWellTyped CoreExpr
e =  do 
  SpecType
t <- CG SpecType -> SM SpecType
forall a. CG a -> SM a
liftCG (CG SpecType -> SM SpecType) -> CG SpecType -> SM SpecType
forall a b. (a -> b) -> a -> b
$ Type -> CG SpecType
trueTy (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
exprType CoreExpr
e 
  SpecType -> CoreExpr -> SM Bool
hasType SpecType
t CoreExpr
e 


tx :: CoreExpr -> CoreExpr
tx :: CoreExpr -> CoreExpr
tx (Case CoreExpr
e Var
b Type
t [Alt Var]
alts) = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
b Type
t ((CoreExpr -> CoreExpr) -> Alt Var -> Alt Var
forall t t3 t1 t2. (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
mapThd3 CoreExpr -> CoreExpr
tx (Alt Var -> Alt Var) -> [Alt Var] -> [Alt Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alts)
tx e :: CoreExpr
e@(Let Bind Var
_ CoreExpr
_) = let ([Bind Var]
bs,CoreExpr
e') = CoreExpr -> ([Bind Var], CoreExpr)
unbind CoreExpr
e in (Bind Var -> CoreExpr -> CoreExpr)
-> CoreExpr -> [Bind Var] -> CoreExpr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bind Var -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let CoreExpr
e' [Bind Var]
bs 
tx CoreExpr
e = CoreExpr
e 

unbind :: CoreExpr -> ([CoreBind], CoreExpr)
unbind :: CoreExpr -> ([Bind Var], CoreExpr)
unbind (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e) = let ([Bind Var]
bs,CoreExpr
e') = CoreExpr -> ([Bind Var], CoreExpr)
unbind CoreExpr
ex in ([Bind Var]
bs [Bind Var] -> [Bind Var] -> [Bind Var]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr -> Bind Var
forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
e'],CoreExpr
e)
unbind CoreExpr
e = ([], CoreExpr
e)


check :: CGInfo -> CGEnv -> F.Config -> Var -> CoreExpr -> Maybe SpecType -> IO Bool 
check :: CGInfo
-> CGEnv -> Config -> Var -> CoreExpr -> Maybe SpecType -> IO Bool
check CGInfo
cgi CGEnv
γ Config
cfg Var
x CoreExpr
e Maybe SpecType
t = do
    FInfo Cinfo
finfo <- TargetInfo -> CGInfo -> IO (FInfo Cinfo)
cgInfoFInfo TargetInfo
info' CGInfo
cs
    Result (Integer, Cinfo) -> Bool
forall a. Result a -> Bool
isSafe (Result (Integer, Cinfo) -> Bool)
-> IO (Result (Integer, Cinfo)) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver Cinfo
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve Config
cfg{srcFile :: String
F.srcFile = String
"SCheck" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Config -> String
F.srcFile Config
cfg} FInfo Cinfo
finfo 
  where 
    cs :: CGInfo
cs = TargetInfo -> CGInfo -> CGEnv -> CGInfo
generateConstraintsWithEnv TargetInfo
info' (CGInfo
cgi{hsCs :: [SubC]
hsCs = []}) (CGEnv
γ{grtys :: REnv
grtys = Symbol -> Maybe SpecType -> REnv -> REnv
insertREnv' (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) Maybe SpecType
t (CGEnv -> REnv
grtys CGEnv
γ)}) 
    info' :: TargetInfo
info' = TargetInfo
info {giSrc :: TargetSrc
giSrc = TargetSrc
giSrc', giSpec :: TargetSpec
giSpec = TargetSpec
giSpec'}
    giSrc' :: TargetSrc
giSrc' = (TargetInfo -> TargetSrc
giSrc TargetInfo
info) {giCbs :: [Bind Var]
giCbs = [[(Var, CoreExpr)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x, CoreExpr
e)]]}
    giSpec' :: TargetSpec
giSpec' = TargetSpec
giSpecOld{gsSig :: GhcSpecSig
gsSig = GhcSpecSig
gsSig'}
    giSpecOld :: TargetSpec
giSpecOld = TargetInfo -> TargetSpec
giSpec TargetInfo
info 
    gsSigOld :: GhcSpecSig
gsSigOld  = TargetSpec -> GhcSpecSig
gsSig TargetSpec
giSpecOld
    gsSig' :: GhcSpecSig
gsSig' = GhcSpecSig
gsSigOld {gsTySigs :: [(Var, LocSpecType)]
gsTySigs = Var
-> Maybe SpecType -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a a. a -> Maybe a -> [(a, Located a)] -> [(a, Located a)]
addTySig Var
x Maybe SpecType
t (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
gsSigOld)}
    info :: TargetInfo
info = CGInfo -> TargetInfo
ghcI CGInfo
cgi 

    insertREnv' :: Symbol -> Maybe SpecType -> REnv -> REnv
insertREnv' Symbol
_ Maybe SpecType
Nothing REnv
g = REnv
g 
    insertREnv' Symbol
x (Just SpecType
t) REnv
g = Symbol -> SpecType -> REnv -> REnv
insertREnv Symbol
x SpecType
t REnv
g
    
    addTySig :: a -> Maybe a -> [(a, Located a)] -> [(a, Located a)]
addTySig a
_ Maybe a
Nothing  [(a, Located a)]
ts = [(a, Located a)]
ts 
    addTySig a
x (Just a
t) [(a, Located a)]
ts = (a
x,a -> Located a
forall a. a -> Located a
dummyLoc a
t)(a, Located a) -> [(a, Located a)] -> [(a, Located a)]
forall a. a -> [a] -> [a]
:[(a, Located a)]
ts
    
checkError :: SpecType -> SM (Maybe CoreExpr)
checkError :: SpecType -> SM (Maybe CoreExpr)
checkError SpecType
t = do 
  Var
errVar <- SM Var
varError
  let errorExpr :: CoreExpr
errorExpr = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
errVar) (Type -> CoreExpr
forall b. Type -> Expr b
Type (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t))) CoreExpr
errorInt
      errorInt :: CoreExpr
errorInt  = DynFlags -> Int -> CoreExpr
mkIntExprInt DynFlags
unsafeGlobalDynFlags Int
42
  Bool
b <- SpecType -> CoreExpr -> SM Bool
hasType SpecType
t CoreExpr
errorExpr
  if Bool
b 
    then Maybe CoreExpr -> SM (Maybe CoreExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CoreExpr -> SM (Maybe CoreExpr))
-> Maybe CoreExpr -> SM (Maybe CoreExpr)
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
errorExpr
    else Maybe CoreExpr -> SM (Maybe CoreExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CoreExpr
forall a. Maybe a
Nothing

quietly :: IO a -> IO a
quietly :: IO a -> IO a
quietly IO a
act = do
  Verbosity
vb <- IO Verbosity
getVerbosity
  Verbosity -> IO ()
setVerbosity Verbosity
Quiet
  a
r  <- IO a
act
  Verbosity -> IO ()
setVerbosity Verbosity
vb
  a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r