{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}

module Language.Haskell.Liquid.Synthesize.Monad where


import           Language.Haskell.Liquid.Bare.Resolve
                                               as B
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Synthesize.GHC
                                         hiding ( SSEnv )
import           Language.Haskell.Liquid.Synthesize.Misc
                                         hiding ( notrace )
import qualified Language.Fixpoint.Smt.Interface
                                               as SMT
import           Language.Fixpoint.Types hiding ( SEnv
                                                , SVar
                                                , Error
                                                )
import qualified Language.Fixpoint.Types       as F
import qualified Language.Fixpoint.Types.Config
                                               as F
import           CoreSyn                        ( CoreExpr )
import qualified CoreSyn                       as GHC
import           Var
import           Control.Monad.State.Lazy
import qualified Data.HashMap.Strict           as M
import           Data.Maybe
import           Data.List
import           CoreUtils                      ( exprType )
import           Data.Tuple.Extra
import           TyCon
import           TyCoRep

localMaxMatchDepth :: SM Int 
localMaxMatchDepth :: SM Int
localMaxMatchDepth = Config -> Int
maxMatchDepth (Config -> Int) -> (SState -> Config) -> SState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig (CGEnv -> Config) -> (SState -> CGEnv) -> SState -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> CGEnv
sCGEnv (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

-------------------------------------------------------------------------------
-- | Synthesis Monad ----------------------------------------------------------
-------------------------------------------------------------------------------

-- The state keeps a unique index for generation of fresh variables 
-- and the environment of variables to types that is expanded on lambda terms
type SSEnv = M.HashMap Symbol (SpecType, Var)
type SSDecrTerm = [(Var, [Var])]

type ExprMemory = [(Type, CoreExpr, Int)]
type T = M.HashMap Type (CoreExpr, Int)
data SState 
  = SState { SState -> REnv
rEnv       :: !REnv 
           , SState -> SSEnv
ssEnv      :: !SSEnv -- Local Binders Generated during Synthesis 
           , SState -> Int
ssIdx      :: !Int
           , SState -> SSDecrTerm
ssDecrTerm :: !SSDecrTerm 
           , SState -> Context
sContext   :: !SMT.Context
           , SState -> CGInfo
sCGI       :: !CGInfo
           , SState -> CGEnv
sCGEnv     :: !CGEnv
           , SState -> Config
sFCfg      :: !F.Config
           , SState -> Int
sDepth     :: !Int
           , SState -> ExprMemory
sExprMem   :: !ExprMemory 
           , SState -> Int
sExprId    :: !Int
           , SState -> Int
sArgsId    :: !Int
           , SState -> Int
sArgsDepth :: !Int
           , SState -> [Var]
sUniVars   :: ![Var]
           , SState -> Var
sFix       :: !Var
           , SState -> [Type]
sGoalTys   :: ![Type]
           , SState -> Maybe [Var]
sGoalTyVar :: !(Maybe [TyVar])
           , SState -> Maybe [Type]
sUGoalTy   :: !(Maybe [Type])     -- Types used for instantiation.
                                               --   Produced by @withUnify@.
           , SState -> ([Var], [[Type]])
sForalls   :: !([Var], [[Type]])  -- [Var] are the parametric functions (except for the fixpoint)
                                               --    e.g. Constructors, top-level functions.
                                               -- [[Type]]: all the types that have instantiated [Var] so far.
           , SState -> Int
caseIdx    :: !Int                -- [ Temporary ] Index in list of scrutinees.
           , SState -> [(CoreExpr, Type, TyCon)]
scrutinees :: ![(CoreExpr, Type, TyCon)]
           }
type SM = StateT SState IO

localMaxAppDepth :: SM Int 
localMaxAppDepth :: SM Int
localMaxAppDepth = Config -> Int
maxAppDepth (Config -> Int) -> (SState -> Config) -> SState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig (CGEnv -> Config) -> (SState -> CGEnv) -> SState -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> CGEnv
sCGEnv (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

localMaxArgsDepth :: SM Int
localMaxArgsDepth :: SM Int
localMaxArgsDepth = Config -> Int
maxArgsDepth (Config -> Int) -> (SState -> Config) -> SState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig (CGEnv -> Config) -> (SState -> CGEnv) -> SState -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> CGEnv
sCGEnv (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

locally :: SM a -> SM a 
locally :: SM a -> SM a
locally SM a
act = do 
  SState
st <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
  a
r <- SM a
act 
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SState -> SState) -> StateT SState IO ())
-> (SState -> SState) -> StateT SState IO ()
forall a b. (a -> b) -> a -> b
$ \SState
s -> SState
s{sCGEnv :: CGEnv
sCGEnv = SState -> CGEnv
sCGEnv SState
st, sCGI :: CGInfo
sCGI = SState -> CGInfo
sCGI SState
st, sExprMem :: ExprMemory
sExprMem = SState -> ExprMemory
sExprMem SState
st, scrutinees :: [(CoreExpr, Type, TyCon)]
scrutinees = SState -> [(CoreExpr, Type, TyCon)]
scrutinees SState
st}
  a -> SM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r 


evalSM :: SM a -> SMT.Context -> SSEnv -> SState -> IO a 
evalSM :: SM a -> Context -> SSEnv -> SState -> IO a
evalSM SM a
act Context
ctx SSEnv
env SState
st = do 
  let st' :: SState
st' = SState
st {ssEnv :: SSEnv
ssEnv = SSEnv
env}
  a
r <- SM a -> SState -> IO a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT SM a
act SState
st'
  Context -> IO ExitCode
SMT.cleanupContext Context
ctx 
  a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r 

initState :: SMT.Context -> F.Config -> CGInfo -> CGEnv -> REnv -> Var -> [Var] -> SSEnv -> IO SState 
initState :: Context
-> Config
-> CGInfo
-> CGEnv
-> REnv
-> Var
-> [Var]
-> SSEnv
-> IO SState
initState Context
ctx Config
fcfg CGInfo
cgi CGEnv
cgenv REnv
renv Var
xtop [Var]
uniVars SSEnv
env = 
  SState -> IO SState
forall (m :: * -> *) a. Monad m => a -> m a
return (SState -> IO SState) -> SState -> IO SState
forall a b. (a -> b) -> a -> b
$ REnv
-> SSEnv
-> Int
-> SSDecrTerm
-> Context
-> CGInfo
-> CGEnv
-> Config
-> Int
-> ExprMemory
-> Int
-> Int
-> Int
-> [Var]
-> Var
-> [Type]
-> Maybe [Var]
-> Maybe [Type]
-> ([Var], [[Type]])
-> Int
-> [(CoreExpr, Type, TyCon)]
-> SState
SState REnv
renv SSEnv
env Int
0 [] Context
ctx CGInfo
cgi CGEnv
cgenv Config
fcfg Int
0 ExprMemory
exprMem0 Int
0 Int
0 Int
0 [Var]
uniVars Var
xtop [] Maybe [Var]
forall a. Maybe a
Nothing Maybe [Type]
forall a. Maybe a
Nothing ([], []) Int
0 []
  where exprMem0 :: ExprMemory
exprMem0 = SSEnv -> ExprMemory
initExprMem SSEnv
env

getSEnv :: SM SSEnv
getSEnv :: SM SSEnv
getSEnv = SState -> SSEnv
ssEnv (SState -> SSEnv) -> StateT SState IO SState -> SM SSEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 

getSEMem :: SM ExprMemory
getSEMem :: SM ExprMemory
getSEMem = SState -> ExprMemory
sExprMem (SState -> ExprMemory) -> StateT SState IO SState -> SM ExprMemory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

getSFix :: SM Var 
getSFix :: SM Var
getSFix = SState -> Var
sFix (SState -> Var) -> StateT SState IO SState -> SM Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

getSUniVars :: SM [Var]
getSUniVars :: SM [Var]
getSUniVars = SState -> [Var]
sUniVars (SState -> [Var]) -> StateT SState IO SState -> SM [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

getSDecrTerms :: SM SSDecrTerm 
getSDecrTerms :: SM SSDecrTerm
getSDecrTerms = SState -> SSDecrTerm
ssDecrTerm (SState -> SSDecrTerm) -> StateT SState IO SState -> SM SSDecrTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

addsEnv :: [(Var, SpecType)] -> SM () 
addsEnv :: [(Var, SpecType)] -> StateT SState IO ()
addsEnv [(Var, SpecType)]
xts = 
  ((Var, SpecType) -> StateT SState IO ())
-> [(Var, SpecType)] -> StateT SState IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Var
x,SpecType
t) -> (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {ssEnv :: SSEnv
ssEnv = Symbol -> (SpecType, Var) -> SSEnv -> SSEnv
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
x) (SpecType
t,Var
x) (SState -> SSEnv
ssEnv SState
s)})) [(Var, SpecType)]
xts  

addsEmem :: [(Var, SpecType)] -> SM () 
addsEmem :: [(Var, SpecType)] -> StateT SState IO ()
addsEmem [(Var, SpecType)]
xts = do 
  Int
curAppDepth <- SState -> Int
sExprId (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  ((Var, SpecType) -> StateT SState IO ())
-> [(Var, SpecType)] -> StateT SState IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Var
x,SpecType
t) -> (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sExprMem :: ExprMemory
sExprMem = (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t, Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
x, Int
curAppDepthInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Type, CoreExpr, Int) -> ExprMemory -> ExprMemory
forall a. a -> [a] -> [a]
: (SState -> ExprMemory
sExprMem SState
s)})) [(Var, SpecType)]
xts  
  

addEnv :: Var -> SpecType -> SM ()
addEnv :: Var -> SpecType -> StateT SState IO ()
addEnv Var
x SpecType
t = do 
  (CGEnv -> CG CGEnv) -> StateT SState IO ()
liftCG0 (\CGEnv
γ -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"arg", Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
x, SpecType
t))
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {ssEnv :: SSEnv
ssEnv = Symbol -> (SpecType, Var) -> SSEnv -> SSEnv
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
x) (SpecType
t,Var
x) (SState -> SSEnv
ssEnv SState
s)}) 

addEmem :: Var -> SpecType -> SM ()
addEmem :: Var -> SpecType -> StateT SState IO ()
addEmem Var
x SpecType
t = do 
  let ht0 :: Type
ht0 = SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t
  Int
curAppDepth <- SState -> Int
sExprId (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  Var
xtop <- SM Var
getSFix 
  (Type
ht1, CoreExpr
_) <- SM (Type, CoreExpr)
instantiateTL
  let ht :: Type
ht = if Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
xtop then Type
ht1 else Type
ht0
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sExprMem :: ExprMemory
sExprMem = (Type
ht, Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
x, Int
curAppDepth) (Type, CoreExpr, Int) -> ExprMemory -> ExprMemory
forall a. a -> [a] -> [a]
: SState -> ExprMemory
sExprMem SState
s})

---------------------------------------------------------------------------------------------
--                         Handle structural termination checking                          --
---------------------------------------------------------------------------------------------
addDecrTerm :: Var -> [Var] -> SM ()
addDecrTerm :: Var -> [Var] -> StateT SState IO ()
addDecrTerm Var
x [Var]
vars = do
  SSDecrTerm
decrTerms <- SM SSDecrTerm
getSDecrTerms 
  case Var -> SSDecrTerm -> Maybe [Var]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x SSDecrTerm
decrTerms of 
    Maybe [Var]
Nothing    -> Var -> [Var] -> SSDecrTerm -> StateT SState IO ()
lookupAll Var
x [Var]
vars SSDecrTerm
decrTerms
    Just [Var]
vars' -> do
      let ix :: Maybe Int
ix = (Var, [Var]) -> SSDecrTerm -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (Var
x, [Var]
vars') SSDecrTerm
decrTerms
          newDecrs :: SSDecrTerm
newDecrs = Int -> (Var, [Var]) -> SSDecrTerm -> SSDecrTerm
forall a. Int -> a -> [a] -> [a]
thisReplace (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
" [ addDecrTerm ] Index ") Maybe Int
ix) (Var
x, [Var]
vars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
vars') SSDecrTerm
decrTerms
      (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { ssDecrTerm :: SSDecrTerm
ssDecrTerm =  SSDecrTerm
newDecrs })

-- 
lookupAll :: Var -> [Var] -> SSDecrTerm -> SM ()
lookupAll :: Var -> [Var] -> SSDecrTerm -> StateT SState IO ()
lookupAll Var
x [Var]
vars []               = (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {ssDecrTerm :: SSDecrTerm
ssDecrTerm = (Var
x, [Var]
vars) (Var, [Var]) -> SSDecrTerm -> SSDecrTerm
forall a. a -> [a] -> [a]
: SState -> SSDecrTerm
ssDecrTerm SState
s})
lookupAll Var
x [Var]
vars ((Var
xl, [Var]
vs):SSDecrTerm
decrs) =
  case (Var -> Bool) -> [Var] -> Maybe Var
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x) [Var]
vs of
    Maybe Var
Nothing -> Var -> [Var] -> SSDecrTerm -> StateT SState IO ()
lookupAll Var
x [Var]
vars SSDecrTerm
decrs
    Just Var
_  -> do
      SSDecrTerm
sDecrs <- SState -> SSDecrTerm
ssDecrTerm (SState -> SSDecrTerm) -> StateT SState IO SState -> SM SSDecrTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
      let newDecr :: (Var, [Var])
newDecr  = (Var
xl, [Var]
vars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
x] [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
vs)
          i :: Int
i        = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
" Write sth ") ((Var, [Var]) -> SSDecrTerm -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (Var
xl, [Var]
vs) SSDecrTerm
sDecrs)
          newDecrs :: SSDecrTerm
newDecrs = Int -> (Var, [Var]) -> SSDecrTerm -> SSDecrTerm
forall a. Int -> a -> [a] -> [a]
thisReplace Int
i (Var, [Var])
newDecr SSDecrTerm
decrs
      (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { ssDecrTerm :: SSDecrTerm
ssDecrTerm = SSDecrTerm
newDecrs })

thisReplace :: Int -> a -> [a] -> [a]
thisReplace :: Int -> a -> [a] -> [a]
thisReplace Int
i a
x [a]
l
  = [a]
left [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
right
    where left :: [a]
left  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [a]
l
          right :: [a]
right = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
i [a]
l

-- | Entry point.
structuralCheck :: [CoreExpr] -> SM [CoreExpr]
structuralCheck :: [CoreExpr] -> SM [CoreExpr]
structuralCheck [CoreExpr]
es 
  = do  SSDecrTerm
decr <- SState -> SSDecrTerm
ssDecrTerm (SState -> SSDecrTerm) -> StateT SState IO SState -> SM SSDecrTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
        Var
fix <- SState -> Var
sFix (SState -> Var) -> StateT SState IO SState -> SM Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
        [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return ((CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter (SSDecrTerm -> Var -> CoreExpr -> Bool
notStructural SSDecrTerm
decr Var
fix) [CoreExpr]
es)

structCheck :: Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck :: Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck Var
xtop var :: CoreExpr
var@(GHC.Var Var
v)
  = if Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
xtop 
      then (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
xtop, [])
      else (Maybe Var
forall a. Maybe a
Nothing, [CoreExpr
var])
structCheck Var
xtop (GHC.App CoreExpr
e1 (GHC.Type Type
_))
  = Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck Var
xtop CoreExpr
e1
structCheck Var
xtop (GHC.App CoreExpr
e1 CoreExpr
e2)
  =  (Maybe Var
mbVar, CoreExpr
e2CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
:[CoreExpr]
es)
    where (Maybe Var
mbVar, [CoreExpr]
es) = Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck Var
xtop CoreExpr
e1
structCheck Var
xtop (GHC.Let Bind Var
_ CoreExpr
e) 
  = Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck Var
xtop CoreExpr
e
structCheck Var
_ CoreExpr
e 
  = String -> (Maybe Var, [CoreExpr])
forall a. HasCallStack => String -> a
error (String
" StructCheck " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show CoreExpr
e)

notStructural :: SSDecrTerm -> Var -> CoreExpr -> Bool
notStructural :: SSDecrTerm -> Var -> CoreExpr -> Bool
notStructural SSDecrTerm
decr Var
xtop CoreExpr
e
  = case Maybe Var
v of
      Maybe Var
Nothing -> Bool
True
      Just Var
_  -> (CoreExpr -> Bool -> Bool) -> Bool -> [CoreExpr] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\CoreExpr
x Bool
b -> CoreExpr -> SSDecrTerm -> Bool
isDecreasing' CoreExpr
x SSDecrTerm
decr Bool -> Bool -> Bool
|| Bool
b) Bool
False [CoreExpr]
args
  where (Maybe Var
v, [CoreExpr]
args) = Var -> CoreExpr -> (Maybe Var, [CoreExpr])
structCheck Var
xtop CoreExpr
e

isDecreasing' :: CoreExpr -> SSDecrTerm -> Bool
isDecreasing' :: CoreExpr -> SSDecrTerm -> Bool
isDecreasing' (GHC.Var Var
v) SSDecrTerm
decr
  = Var
v Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Var, [Var]) -> Var) -> SSDecrTerm -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, [Var]) -> Var
forall a b. (a, b) -> a
fst SSDecrTerm
decr
isDecreasing' CoreExpr
_e SSDecrTerm
_decr
  = Bool
True
---------------------------------------------------------------------------------------------
--                               END OF STRUCTURAL CHECK                                   --
---------------------------------------------------------------------------------------------

liftCG0 :: (CGEnv -> CG CGEnv) -> SM () 
liftCG0 :: (CGEnv -> CG CGEnv) -> StateT SState IO ()
liftCG0 CGEnv -> CG CGEnv
act = do 
  SState
st <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
  let (CGEnv
cgenv, CGInfo
cgi) = CG CGEnv -> CGInfo -> (CGEnv, CGInfo)
forall s a. State s a -> s -> (a, s)
runState (CGEnv -> CG CGEnv
act (SState -> CGEnv
sCGEnv SState
st)) (SState -> CGInfo
sCGI SState
st) 
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sCGI :: CGInfo
sCGI = CGInfo
cgi, sCGEnv :: CGEnv
sCGEnv = CGEnv
cgenv}) 


liftCG :: CG a -> SM a 
liftCG :: CG a -> SM a
liftCG CG a
act = do 
  SState
st <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
  let (a
x, CGInfo
cgi) = CG a -> CGInfo -> (a, CGInfo)
forall s a. State s a -> s -> (a, s)
runState CG a
act (SState -> CGInfo
sCGI SState
st) 
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sCGI :: CGInfo
sCGI = CGInfo
cgi})
  a -> SM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x 


freshVarType :: Type -> SM Var
freshVarType :: Type -> SM Var
freshVarType Type
t = (\Int
i -> Maybe String -> Int -> Type -> Var
mkVar (String -> Maybe String
forall a. a -> Maybe a
Just String
"x") Int
i Type
t) (Int -> Var) -> SM Int -> SM Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SM Int
incrSM


freshVar :: SpecType -> SM Var
freshVar :: SpecType -> SM Var
freshVar = Type -> SM Var
freshVarType (Type -> SM Var) -> (SpecType -> Type) -> SpecType -> SM Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType

withIncrDepth :: Monoid a => SM a -> SM a
withIncrDepth :: SM a -> SM a
withIncrDepth SM a
m = do 
    SState
s <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
    Int
matchBound <- SM Int
localMaxMatchDepth 
    let d :: Int
d = SState -> Int
sDepth SState
s
    if Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
matchBound
      then a -> SM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall a. Monoid a => a
mempty
      else do SState -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SState
s{sDepth :: Int
sDepth = Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1}
              a
r <- SM a
m
              (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SState -> SState) -> StateT SState IO ())
-> (SState -> SState) -> StateT SState IO ()
forall a b. (a -> b) -> a -> b
$ \SState
s -> SState
s{sDepth :: Int
sDepth = Int
d}
              a -> SM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
        
  
incrSM :: SM Int 
incrSM :: SM Int
incrSM = do SState
s <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
            SState -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SState
s{ssIdx :: Int
ssIdx = SState -> Int
ssIdx SState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1}
            Int -> SM Int
forall (m :: * -> *) a. Monad m => a -> m a
return (SState -> Int
ssIdx SState
s)

incrCase :: SM Int 
incrCase :: SM Int
incrCase
  = do  SState
s <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
        SState -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SState
s { caseIdx :: Int
caseIdx = SState -> Int
caseIdx SState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
        Int -> SM Int
forall (m :: * -> *) a. Monad m => a -> m a
return (SState -> Int
caseIdx SState
s)
  
safeIxScruts :: Int -> [a] -> Maybe Int
safeIxScruts :: Int -> [a] -> Maybe Int
safeIxScruts Int
i [a]
l 
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
l = Maybe Int
forall a. Maybe a
Nothing
  | Bool
otherwise     = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i

symbolExpr :: Type -> F.Symbol -> SM CoreExpr 
symbolExpr :: Type -> Symbol -> SM CoreExpr
symbolExpr Type
τ Symbol
x = SM Int
incrSM SM Int -> (Int -> SM CoreExpr) -> SM CoreExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Int
i -> CoreExpr -> SM CoreExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr -> SM CoreExpr) -> CoreExpr -> SM CoreExpr
forall a b. (a -> b) -> a -> b
$ String -> CoreExpr -> CoreExpr
forall a. PPrint a => String -> a -> a
F.notracepp (String
"symExpr for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$  Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var (Var -> CoreExpr) -> Var -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Maybe String -> Int -> Type -> Var
mkVar (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Symbol -> String
F.symbolString Symbol
x) Int
i Type
τ)


-------------------------------------------------------------------------------------------------------
----------------------------------------- Handle ExprMemory -------------------------------------------
-------------------------------------------------------------------------------------------------------

-- | Initializes @ExprMemory@ structure.
--    1. Transforms refinement types to conventional (Haskell) types.
--    2. All @Depth@s are initialized to 0.
initExprMem :: SSEnv -> ExprMemory
initExprMem :: SSEnv -> ExprMemory
initExprMem SSEnv
sEnv = ((Symbol, (SpecType, Var)) -> (Type, CoreExpr, Int))
-> [(Symbol, (SpecType, Var))] -> ExprMemory
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
_, (SpecType
t, Var
v)) -> (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t, Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
v, Int
0)) (SSEnv -> [(Symbol, (SpecType, Var))]
forall k v. HashMap k v -> [(k, v)]
M.toList SSEnv
sEnv)


-------------- Init @ExprMemory@ with instantiated functions with the right type (sUGoalTy) -----------
insEMem0 :: SSEnv -> SM ExprMemory
insEMem0 :: SSEnv -> SM ExprMemory
insEMem0 SSEnv
senv = do
  Var
xtop      <- SM Var
getSFix
  (Type
ttop, CoreExpr
_) <- SM (Type, CoreExpr)
instantiateTL
  Maybe [Type]
mbUTy     <- SState -> Maybe [Type]
sUGoalTy (SState -> Maybe [Type])
-> StateT SState IO SState -> StateT SState IO (Maybe [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
  [Var]
uniVs <- SState -> [Var]
sUniVars (SState -> [Var]) -> StateT SState IO SState -> SM [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get

  let ts :: [Type]
ts = [Type] -> Maybe [Type] -> [Type]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Type]
mbUTy
  [[Type]]
ts0 <- ([Var], [[Type]]) -> [[Type]]
forall a b. (a, b) -> b
snd (([Var], [[Type]]) -> [[Type]])
-> (SState -> ([Var], [[Type]])) -> SState -> [[Type]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> ([Var], [[Type]])
sForalls (SState -> [[Type]])
-> StateT SState IO SState -> StateT SState IO [[Type]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  [Var]
fs0 <- ([Var], [[Type]]) -> [Var]
forall a b. (a, b) -> a
fst (([Var], [[Type]]) -> [Var])
-> (SState -> ([Var], [[Type]])) -> SState -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> ([Var], [[Type]])
sForalls (SState -> [Var]) -> StateT SState IO SState -> SM [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ( \SState
s -> SState
s { sForalls :: ([Var], [[Type]])
sForalls = ([Var]
fs0, [Type]
ts [Type] -> [[Type]] -> [[Type]]
forall a. a -> [a] -> [a]
: [[Type]]
ts0) } )

  let handleIt :: CoreExpr -> (CoreExpr, Type)
handleIt CoreExpr
e = case CoreExpr
e of  GHC.Var Var
v -> if Var
xtop Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v 
                                              then (CoreExpr -> Maybe [Var] -> CoreExpr
instantiate CoreExpr
e ([Var] -> Maybe [Var]
forall a. a -> Maybe a
Just [Var]
uniVs), Type
ttop) 
                                              else CoreExpr -> (CoreExpr, Type)
change CoreExpr
e
                              CoreExpr
_         -> CoreExpr -> (CoreExpr, Type)
change CoreExpr
e
      change :: CoreExpr -> (CoreExpr, Type)
change CoreExpr
e =  let { e' :: CoreExpr
e' = CoreExpr -> Maybe [Type] -> CoreExpr
instantiateTy CoreExpr
e Maybe [Type]
mbUTy; t' :: Type
t' = CoreExpr -> Type
exprType CoreExpr
e' } 
                  in  (CoreExpr
e', Type
t')

      em0 :: ExprMemory
em0 = SSEnv -> ExprMemory
initExprMem SSEnv
senv
  ExprMemory -> SM ExprMemory
forall (m :: * -> *) a. Monad m => a -> m a
return (ExprMemory -> SM ExprMemory) -> ExprMemory -> SM ExprMemory
forall a b. (a -> b) -> a -> b
$ ((Type, CoreExpr, Int) -> (Type, CoreExpr, Int))
-> ExprMemory -> ExprMemory
forall a b. (a -> b) -> [a] -> [b]
map (\(Type
_, CoreExpr
e, Int
i) -> let (CoreExpr
e', Type
t') = CoreExpr -> (CoreExpr, Type)
handleIt CoreExpr
e
                              in  (Type
t', CoreExpr
e', Int
i)) ExprMemory
em0

instantiateTy :: CoreExpr -> Maybe [Type] -> CoreExpr
instantiateTy :: CoreExpr -> Maybe [Type] -> CoreExpr
instantiateTy CoreExpr
e Maybe [Type]
mbTy = 
  case Maybe [Type]
mbTy of 
    Maybe [Type]
Nothing  -> CoreExpr
e
    Just [Type]
tys -> case [Type] -> CoreExpr -> Maybe CoreExpr
applyTy [Type]
tys CoreExpr
e of 
                  Maybe CoreExpr
Nothing -> CoreExpr
e
                  Just CoreExpr
e0 -> CoreExpr
e0

-- | Used for instantiation: Applies types to an expression.
--   > The result does not have @forall@.
--   Nothing as a result suggests that there are more types than foralls in the expression.
applyTy :: [Type] -> GHC.CoreExpr -> Maybe GHC.CoreExpr
applyTy :: [Type] -> CoreExpr -> Maybe CoreExpr
applyTy []     CoreExpr
e =  case CoreExpr -> Type
exprType CoreExpr
e of 
                      ForAllTy{} -> Maybe CoreExpr
forall a. Maybe a
Nothing
                      Type
_          -> CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e
applyTy (Type
t:[Type]
ts) CoreExpr
e =  case CoreExpr -> Type
exprType CoreExpr
e of
                      ForAllTy{} -> [Type] -> CoreExpr -> Maybe CoreExpr
applyTy [Type]
ts (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
GHC.App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
GHC.Type Type
t))
                      Type
_          -> Maybe CoreExpr
forall a. Maybe a
Nothing

-- | Instantiation based on current goal-type.
fixEMem :: SpecType -> SM ()
fixEMem :: SpecType -> StateT SState IO ()
fixEMem SpecType
t
  = do  ([Var]
fs, [[Type]]
ts) <- SState -> ([Var], [[Type]])
sForalls (SState -> ([Var], [[Type]]))
-> StateT SState IO SState -> StateT SState IO ([Var], [[Type]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
        let uTys :: [Type]
uTys = Type -> [Type]
unifyWith (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t)
        Bool
needsFix <- case ([Type] -> Bool) -> [[Type]] -> Maybe [Type]
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ([Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
uTys) [[Type]]
ts of 
                      Maybe [Type]
Nothing -> Bool -> StateT SState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True   -- not yet instantiated
                      Just [Type]
_  -> Bool -> StateT SState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- already instantiated

        Bool -> StateT SState IO () -> StateT SState IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
needsFix (StateT SState IO () -> StateT SState IO ())
-> StateT SState IO () -> StateT SState IO ()
forall a b. (a -> b) -> a -> b
$
          do  (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sForalls :: ([Var], [[Type]])
sForalls = ([Var]
fs, [Type]
uTys [Type] -> [[Type]] -> [[Type]]
forall a. a -> [a] -> [a]
: [[Type]]
ts)})
              let notForall :: CoreExpr -> Bool
notForall CoreExpr
e = case CoreExpr -> Type
exprType CoreExpr
e of {ForAllTy{} -> Bool
False; Type
_ -> Bool
True}
                  es :: [CoreExpr]
es = (Var -> CoreExpr) -> [Var] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\Var
v -> CoreExpr -> Maybe [Type] -> CoreExpr
instantiateTy (Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
v) ([Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
uTys)) [Var]
fs
                  fixEs :: [CoreExpr]
fixEs = (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreExpr -> Bool
notForall [CoreExpr]
es
              Int
thisDepth <- SState -> Int
sDepth (SState -> Int) -> StateT SState IO SState -> SM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
              let fixedEMem :: ExprMemory
fixedEMem = (CoreExpr -> (Type, CoreExpr, Int)) -> [CoreExpr] -> ExprMemory
forall a b. (a -> b) -> [a] -> [b]
map (\CoreExpr
e -> (CoreExpr -> Type
exprType CoreExpr
e, CoreExpr
e, Int
thisDepth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) [CoreExpr]
fixEs
              (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sExprMem :: ExprMemory
sExprMem = ExprMemory
fixedEMem ExprMemory -> ExprMemory -> ExprMemory
forall a. [a] -> [a] -> [a]
++ SState -> ExprMemory
sExprMem SState
s})

------------------------------------------------------------------------------------------------
------------------------------ Special handle for the current fixpoint -------------------------
------------------------------------------------------------------------------------------------

-- | Instantiate the top-level variable.
instantiateTL :: SM (Type, GHC.CoreExpr)
instantiateTL :: SM (Type, CoreExpr)
instantiateTL = do
  [Var]
uniVars <- SM [Var]
getSUniVars 
  Var
xtop <- SM Var
getSFix
  let e :: CoreExpr
e = Maybe CoreExpr -> CoreExpr
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe CoreExpr -> CoreExpr) -> Maybe CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ [Var] -> CoreExpr -> Maybe CoreExpr
apply [Var]
uniVars (Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
xtop)
  (Type, CoreExpr) -> SM (Type, CoreExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr -> Type
exprType CoreExpr
e, CoreExpr
e)

-- | Applies type variables (1st argument) to an expression.
--   The expression is guaranteed to have the same level of 
--   parametricity (same number of @forall@) as the length of the 1st argument.
--   > The result has zero @forall@.
apply :: [Var] -> GHC.CoreExpr -> Maybe GHC.CoreExpr
apply :: [Var] -> CoreExpr -> Maybe CoreExpr
apply []     CoreExpr
e = 
  case CoreExpr -> Type
exprType CoreExpr
e of 
    ForAllTy {} -> Maybe CoreExpr
forall a. Maybe a
Nothing
    Type
_           -> CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
e
apply (Var
v:[Var]
vs) CoreExpr
e 
  = case CoreExpr -> Type
exprType CoreExpr
e of 
      ForAllTy{} -> [Var] -> CoreExpr -> Maybe CoreExpr
apply [Var]
vs (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
GHC.App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
GHC.Type (Var -> Type
TyVarTy Var
v)))
      Type
_          -> Maybe CoreExpr
forall a. Maybe a
Nothing

instantiate :: CoreExpr -> Maybe [Var] -> CoreExpr
instantiate :: CoreExpr -> Maybe [Var] -> CoreExpr
instantiate CoreExpr
e Maybe [Var]
mbt = 
  case Maybe [Var]
mbt of
    Maybe [Var]
Nothing     -> CoreExpr
e
    Just [Var]
tyVars -> case [Var] -> CoreExpr -> Maybe CoreExpr
apply [Var]
tyVars CoreExpr
e of 
                      Maybe CoreExpr
Nothing -> CoreExpr
e
                      Just CoreExpr
e' -> CoreExpr
e'

-----------------------------------------------------------------------------------------------------

withTypeEs :: SpecType -> SM [CoreExpr] 
withTypeEs :: SpecType -> SM [CoreExpr]
withTypeEs SpecType
t = do 
    ExprMemory
em <- SState -> ExprMemory
sExprMem (SState -> ExprMemory) -> StateT SState IO SState -> SM ExprMemory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get 
    [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Type, CoreExpr, Int) -> CoreExpr) -> ExprMemory -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Type, CoreExpr, Int) -> CoreExpr
forall a b c. (a, b, c) -> b
snd3 (((Type, CoreExpr, Int) -> Bool) -> ExprMemory -> ExprMemory
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Type, CoreExpr, Int)
x -> (Type, CoreExpr, Int) -> Type
forall a b c. (a, b, c) -> a
fst3 (Type, CoreExpr, Int)
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t) ExprMemory
em)) 

findCandidates :: Type ->         -- Goal type: Find all candidate expressions of this type,
                                  --   or that produce this type (i.e. functions).
                  SM ExprMemory
findCandidates :: Type -> SM ExprMemory
findCandidates Type
goalTy = do
  ExprMemory
sEMem <- SState -> ExprMemory
sExprMem (SState -> ExprMemory) -> StateT SState IO SState -> SM ExprMemory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  ExprMemory -> SM ExprMemory
forall (m :: * -> *) a. Monad m => a -> m a
return (((Type, CoreExpr, Int) -> Bool) -> ExprMemory -> ExprMemory
forall a. (a -> Bool) -> [a] -> [a]
filter ((Type -> Type -> Bool
goalType Type
goalTy) (Type -> Bool)
-> ((Type, CoreExpr, Int) -> Type) -> (Type, CoreExpr, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, CoreExpr, Int) -> Type
forall a b c. (a, b, c) -> a
fst3) ExprMemory
sEMem)

functionCands :: Type -> SM [(Type, GHC.CoreExpr, Int)]
functionCands :: Type -> SM ExprMemory
functionCands Type
goalTy = do 
  ExprMemory
all <- Type -> SM ExprMemory
findCandidates Type
goalTy 
  ExprMemory -> SM ExprMemory
forall (m :: * -> *) a. Monad m => a -> m a
return (((Type, CoreExpr, Int) -> Bool) -> ExprMemory -> ExprMemory
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isFunction (Type -> Bool)
-> ((Type, CoreExpr, Int) -> Type) -> (Type, CoreExpr, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, CoreExpr, Int) -> Type
forall a b c. (a, b, c) -> a
fst3) ExprMemory
all)


---------------------------------------------------------------------------------
--------------------------- Generate error expression ---------------------------
---------------------------------------------------------------------------------

varError :: SM Var
varError :: SM Var
varError = do 
  TargetInfo
info    <- CGInfo -> TargetInfo
ghcI (CGInfo -> TargetInfo)
-> (SState -> CGInfo) -> SState -> TargetInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> CGInfo
sCGI (SState -> TargetInfo)
-> StateT SState IO SState -> StateT SState IO TargetInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  let env :: Env
env  = Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
B.makeEnv (TargetSpec -> Config
gsConfig (TargetSpec -> Config) -> TargetSpec -> Config
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info) (TargetSrc -> GhcSrc
toGhcSrc (TargetSrc -> GhcSrc) -> TargetSrc -> GhcSrc
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info) LogicMap
forall a. Monoid a => a
mempty [(ModName, BareSpec)]
forall a. Monoid a => a
mempty 
  let name :: ModName
name = TargetSrc -> ModName
giTargetMod (TargetSrc -> ModName) -> TargetSrc -> ModName
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info
  Var -> SM Var
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> SM Var) -> Var -> SM Var
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Var
B.lookupGhcVar Env
env ModName
name String
"Var" (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
"Language.Haskell.Liquid.Synthesize.Error.err")

toGhcSrc :: TargetSrc -> GhcSrc 
toGhcSrc :: TargetSrc -> GhcSrc
toGhcSrc TargetSrc
a = Src :: String
-> String
-> ModName
-> [Bind Var]
-> [TyCon]
-> Maybe [ClsInst]
-> HashSet Var
-> [Var]
-> [Var]
-> [Var]
-> HashSet StableName
-> [TyCon]
-> [(Symbol, DataCon)]
-> [TyCon]
-> QImports
-> HashSet Symbol
-> [TyThing]
-> GhcSrc
Src
      { _giIncDir :: String
_giIncDir    = TargetSrc -> String
giIncDir TargetSrc
a
      , _giTarget :: String
_giTarget    = TargetSrc -> String
giTarget TargetSrc
a
      , _giTargetMod :: ModName
_giTargetMod = TargetSrc -> ModName
giTargetMod TargetSrc
a
      , _giCbs :: [Bind Var]
_giCbs       = TargetSrc -> [Bind Var]
giCbs TargetSrc
a
      , _gsTcs :: [TyCon]
_gsTcs       = TargetSrc -> [TyCon]
gsTcs TargetSrc
a
      , _gsCls :: Maybe [ClsInst]
_gsCls       = TargetSrc -> Maybe [ClsInst]
gsCls TargetSrc
a
      , _giDerVars :: HashSet Var
_giDerVars   = TargetSrc -> HashSet Var
giDerVars TargetSrc
a
      , _giImpVars :: [Var]
_giImpVars   = TargetSrc -> [Var]
giImpVars TargetSrc
a
      , _giDefVars :: [Var]
_giDefVars   = TargetSrc -> [Var]
giDefVars TargetSrc
a
      , _giUseVars :: [Var]
_giUseVars   = TargetSrc -> [Var]
giUseVars TargetSrc
a
      , _gsExports :: HashSet StableName
_gsExports   = TargetSrc -> HashSet StableName
gsExports TargetSrc
a
      , _gsFiTcs :: [TyCon]
_gsFiTcs     = TargetSrc -> [TyCon]
gsFiTcs TargetSrc
a
      , _gsFiDcs :: [(Symbol, DataCon)]
_gsFiDcs     = TargetSrc -> [(Symbol, DataCon)]
gsFiDcs TargetSrc
a
      , _gsPrimTcs :: [TyCon]
_gsPrimTcs   = TargetSrc -> [TyCon]
gsPrimTcs TargetSrc
a
      , _gsQualImps :: QImports
_gsQualImps  = TargetSrc -> QImports
gsQualImps TargetSrc
a
      , _gsAllImps :: HashSet Symbol
_gsAllImps   = TargetSrc -> HashSet Symbol
gsAllImps TargetSrc
a
      , _gsTyThings :: [TyThing]
_gsTyThings  = TargetSrc -> [TyThing]
gsTyThings TargetSrc
a
      }