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

module Language.Haskell.Liquid.Synthesize (
    synthesize
  ) where

import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Generate 
import qualified Language.Haskell.Liquid.Types.RefType as R
import           Language.Haskell.Liquid.Synthesize.Termination
import           Language.Haskell.Liquid.Synthesize.Generate
import           Language.Haskell.Liquid.Synthesize.GHC hiding (SSEnv)
import           Language.Haskell.Liquid.Synthesize.Monad
import           Language.Haskell.Liquid.Synthesize.Misc hiding (notrace)
import           Language.Haskell.Liquid.Constraint.Fresh (trueTy)
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           Language.Haskell.Liquid.Synthesize.Env

import           CoreSyn (CoreExpr)
import qualified CoreSyn as GHC
import           Var 
import           TyCon
import           DataCon
import           Text.PrettyPrint.HughesPJ (text, ($+$))
import           Control.Monad.State.Lazy
import qualified Data.HashMap.Strict as M 
import           Data.Maybe
import           CoreUtils (exprType)
import           TyCoRep

synthesize :: FilePath -> F.Config -> CGInfo -> IO [Error]
synthesize :: FilePath -> Config -> CGInfo -> IO [Error]
synthesize FilePath
tgt Config
fcfg CGInfo
cginfo = 
  ((Var, HoleInfo (CGInfo, CGEnv) SpecType) -> IO Error)
-> [(Var, HoleInfo (CGInfo, CGEnv) SpecType)] -> IO [Error]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, HoleInfo (CGInfo, CGEnv) SpecType) -> IO Error
forall a.
Symbolic a =>
(a, HoleInfo (CGInfo, CGEnv) SpecType) -> IO Error
go (HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> [(Var, HoleInfo (CGInfo, CGEnv) SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
 -> [(Var, HoleInfo (CGInfo, CGEnv) SpecType)])
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> [(Var, HoleInfo (CGInfo, CGEnv) SpecType)]
forall a b. (a -> b) -> a -> b
$ CGInfo -> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap CGInfo
cginfo)
  where 
    measures :: [Symbol]
measures = (Measure SpecType DataCon -> Symbol)
-> [Measure SpecType DataCon] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Located Symbol -> Symbol
forall a. Located a -> a
val (Located Symbol -> Symbol)
-> (Measure SpecType DataCon -> Located Symbol)
-> Measure SpecType DataCon
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure SpecType DataCon -> Located Symbol
forall ty ctor. Measure ty ctor -> Located Symbol
msName) ((GhcSpecData -> [Measure SpecType DataCon]
gsMeasures (GhcSpecData -> [Measure SpecType DataCon])
-> (CGInfo -> GhcSpecData) -> CGInfo -> [Measure SpecType DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecData
gsData (TargetSpec -> GhcSpecData)
-> (CGInfo -> TargetSpec) -> CGInfo -> GhcSpecData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> TargetSpec)
-> (CGInfo -> TargetInfo) -> CGInfo -> TargetSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> TargetInfo
ghcI) CGInfo
cginfo)
    go :: (a, HoleInfo (CGInfo, CGEnv) SpecType) -> IO Error
go (a
x, HoleInfo SpecType
_ SrcSpan
loc AREnv SpecType
env (CGInfo
cgi,CGEnv
cge)) = do 
      let topLvlBndr :: Var
topLvlBndr = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> Var
forall a. HasCallStack => FilePath -> a
error FilePath
"Top-level binder not found") (CGEnv -> Maybe Var
cgVar CGEnv
cge)
          typeOfTopLvlBnd :: SpecType
typeOfTopLvlBnd = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> SpecType
forall a. HasCallStack => FilePath -> a
error FilePath
"Type: Top-level symbol not found") (Symbol -> HashMap Symbol SpecType -> Maybe SpecType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
topLvlBndr) (AREnv SpecType -> HashMap Symbol SpecType
forall t. AREnv t -> HashMap Symbol t
reGlobal AREnv SpecType
env))
          coreProgram :: [CoreBind]
coreProgram = TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc (TargetInfo -> TargetSrc) -> TargetInfo -> TargetSrc
forall a b. (a -> b) -> a -> b
$ CGInfo -> TargetInfo
ghcI CGInfo
cgi
          ([Var]
uniVars, [Var]
_) = [CoreBind] -> Var -> ([Var], [Var])
getUniVars [CoreBind]
coreProgram Var
topLvlBndr
          fromREnv' :: HashMap Symbol SpecType
fromREnv' = HashMap Symbol SpecType -> HashMap Symbol SpecType
filterREnv (AREnv SpecType -> HashMap Symbol SpecType
forall t. AREnv t -> HashMap Symbol t
reLocal AREnv SpecType
env)
          fromREnv'' :: HashMap Symbol SpecType
fromREnv'' = [(Symbol, SpecType)] -> HashMap Symbol SpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
rmClassVars (Type -> Bool)
-> ((Symbol, SpecType) -> Type) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType (SpecType -> Type)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) (HashMap Symbol SpecType -> [(Symbol, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol SpecType
fromREnv'))
          rmClassVars :: Type -> Bool
rmClassVars Type
t = case Type
t of { TyConApp TyCon
c [Type]
_ -> Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Bool
isClassTyCon (TyCon -> Bool) -> TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon
c; Type
_ -> Bool
True }
          fromREnv :: HashMap Symbol SpecType
fromREnv  = [(Symbol, SpecType)] -> HashMap Symbol SpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([Symbol] -> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
rmMeasures [Symbol]
measures (HashMap Symbol SpecType -> [(Symbol, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol SpecType
fromREnv''))
          isForall :: Type -> Bool
isForall Type
t = case Type
t of { ForAllTy{} -> Bool
True; Type
_ -> Bool
False}
          rEnvForalls :: HashMap Symbol SpecType
rEnvForalls = [(Symbol, SpecType)] -> HashMap Symbol SpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isForall (Type -> Bool)
-> ((Symbol, SpecType) -> Type) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType (SpecType -> Type)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) (HashMap Symbol SpecType -> [(Symbol, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol SpecType
fromREnv))
          fs :: [Var]
fs = ((Symbol, (SpecType, Var)) -> Var)
-> [(Symbol, (SpecType, Var))] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map ((SpecType, Var) -> Var
forall a b. (a, b) -> b
snd ((SpecType, Var) -> Var)
-> ((Symbol, (SpecType, Var)) -> (SpecType, Var))
-> (Symbol, (SpecType, Var))
-> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, (SpecType, Var)) -> (SpecType, Var)
forall a b. (a, b) -> b
snd) ([(Symbol, (SpecType, Var))] -> [Var])
-> [(Symbol, (SpecType, Var))] -> [Var]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol (SpecType, Var) -> [(Symbol, (SpecType, Var))]
forall k v. HashMap k v -> [(k, v)]
M.toList ([CoreBind]
-> Var -> HashMap Symbol SpecType -> HashMap Symbol (SpecType, Var)
symbolToVar [CoreBind]
coreProgram Var
topLvlBndr HashMap Symbol SpecType
rEnvForalls)

          ssenv0 :: HashMap Symbol (SpecType, Var)
ssenv0 = [CoreBind]
-> Var -> HashMap Symbol SpecType -> HashMap Symbol (SpecType, Var)
symbolToVar [CoreBind]
coreProgram Var
topLvlBndr HashMap Symbol SpecType
fromREnv
          (HashMap Symbol (SpecType, Var)
senv1, [Var]
foralls') = SpecType
-> CGInfo
-> HashMap Symbol (SpecType, Var)
-> (HashMap Symbol (SpecType, Var), [Var])
initSSEnv SpecType
typeOfTopLvlBnd CGInfo
cginfo HashMap Symbol (SpecType, Var)
ssenv0
      
      Context
ctx <- Config -> FilePath -> IO Context
SMT.makeContext Config
fcfg FilePath
tgt
      SState
state0 <- Context
-> Config
-> CGInfo
-> CGEnv
-> AREnv SpecType
-> Var
-> [Var]
-> HashMap Symbol (SpecType, Var)
-> IO SState
initState Context
ctx Config
fcfg CGInfo
cgi CGEnv
cge AREnv SpecType
env Var
topLvlBndr ([Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
uniVars) HashMap Symbol (SpecType, Var)
forall k v. HashMap k v
M.empty
      let foralls :: [Var]
foralls = [Var]
foralls' [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
fs
      [CoreExpr]
fills <- Context
-> CGInfo
-> HashMap Symbol (SpecType, Var)
-> SpecType
-> Var
-> SpecType
-> [Var]
-> SState
-> IO [CoreExpr]
synthesize' Context
ctx CGInfo
cgi HashMap Symbol (SpecType, Var)
senv1 SpecType
typeOfTopLvlBnd Var
topLvlBndr SpecType
typeOfTopLvlBnd [Var]
foralls SState
state0

      Error -> IO Error
forall (m :: * -> *) a. Monad m => a -> m a
return (Error -> IO Error) -> Error -> IO Error
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Doc -> HashMap Symbol SpecType -> Symbol -> SpecType -> Error
forall t.
SrcSpan -> Doc -> HashMap Symbol t -> Symbol -> t -> TError t
ErrHole SrcSpan
loc (
        if Bool -> Bool
not ([CoreExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreExpr]
fills)
          then FilePath -> Doc
text FilePath
"\n Hole Fills:" Doc -> Doc -> Doc
$+$ [FilePath] -> Doc
pprintMany ((CoreExpr -> FilePath) -> [CoreExpr] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (SpecType -> Var -> CoreExpr -> FilePath
coreToHs SpecType
typeOfTopLvlBnd Var
topLvlBndr (CoreExpr -> FilePath)
-> (CoreExpr -> CoreExpr) -> CoreExpr -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> CoreExpr
fromAnf) [CoreExpr]
fills)
          else Doc
forall a. Monoid a => a
mempty) HashMap Symbol SpecType
forall a. Monoid a => a
mempty (a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol a
x) SpecType
typeOfTopLvlBnd 


synthesize' :: SMT.Context -> CGInfo -> SSEnv -> SpecType ->  Var -> SpecType -> [Var] -> SState -> IO [CoreExpr]
synthesize' :: Context
-> CGInfo
-> HashMap Symbol (SpecType, Var)
-> SpecType
-> Var
-> SpecType
-> [Var]
-> SState
-> IO [CoreExpr]
synthesize' Context
ctx CGInfo
cgi HashMap Symbol (SpecType, Var)
senv SpecType
tx Var
xtop SpecType
ttop [Var]
foralls SState
st2
 = SM [CoreExpr]
-> Context
-> HashMap Symbol (SpecType, Var)
-> SState
-> IO [CoreExpr]
forall a.
SM a -> Context -> HashMap Symbol (SpecType, Var) -> SState -> IO a
evalSM (SpecType -> SM [CoreExpr]
go SpecType
tx) Context
ctx HashMap Symbol (SpecType, Var)
senv SState
st2
  where 

    go :: SpecType -> SM [CoreExpr]

    -- Type Abstraction 
    go :: SpecType -> SM [CoreExpr]
go (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
_x)      = Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
GHC.Lam (RTVU RTyCon RTyVar -> Var
forall c. RTVar RTyVar c -> Var
tyVarVar RTVU RTyCon RTyVar
a) (CoreExpr -> CoreExpr) -> SM [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) (n :: * -> *) a b.
(Functor m, Functor n) =>
(a -> b) -> m (n a) -> m (n b)
<$$> SpecType -> SM [CoreExpr]
go SpecType
t
          
    go t :: SpecType
t@(RApp RTyCon
c [SpecType]
_ts [RTProp RTyCon RTyVar RReft]
_ RReft
_r) = do  
      let coreProgram :: [CoreBind]
coreProgram = TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc (TargetInfo -> TargetSrc) -> TargetInfo -> TargetSrc
forall a b. (a -> b) -> a -> b
$ CGInfo -> TargetInfo
ghcI CGInfo
cgi
          args :: [Var]
args  = Int -> [Var] -> [Var]
forall a. Int -> [a] -> [a]
drop Int
1 ([CoreBind] -> Var -> [Var]
argsP [CoreBind]
coreProgram Var
xtop)
          (([Symbol], [SpecType], [RReft])
_, ([Symbol]
xs, [SpecType]
txs, [RReft]
_), SpecType
_) = SpecType
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [SpecType], [RReft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RType t t1 a], [a]),
    ([Symbol], [RType t t1 a], [a]), RType t t1 a)
bkArrow SpecType
ttop
      Var -> SpecType -> SM ()
addEnv Var
xtop (SpecType -> SM ()) -> SpecType -> SM ()
forall a b. (a -> b) -> a -> b
$ Var -> SpecType -> [Var] -> [(Symbol, SpecType)] -> SpecType
decrType Var
xtop SpecType
ttop [Var]
args ([Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
txs)

      if TCEmb TyCon -> RTyCon -> Bool
R.isNumeric (CGInfo -> TCEmb TyCon
tyConEmbed CGInfo
cgi) RTyCon
c
          then FilePath -> SM [CoreExpr]
forall a. HasCallStack => FilePath -> a
error FilePath
" [ Numeric in synthesize ] Update liquid fixpoint. "
          else do let ts :: [Type]
ts = Type -> [Type]
unifyWith (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t)
                  if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ts  then (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = Maybe [Type]
forall a. Maybe a
Nothing } )
                              else (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
ts } )
                  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sForalls :: ([Var], [[Type]])
sForalls = ([Var]
foralls, [])})
                  ExprMemory
emem0 <- HashMap Symbol (SpecType, Var) -> SM ExprMemory
insEMem0 HashMap Symbol (SpecType, Var)
senv
                  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sExprMem :: ExprMemory
sExprMem = ExprMemory
emem0 })
                  SpecType -> SM [CoreExpr]
synthesizeBasic SpecType
t

    go (RAllP PVU RTyCon RTyVar
_ SpecType
t) = SpecType -> SM [CoreExpr]
go SpecType
t

    go (RRTy [(Symbol, SpecType)]
_env RReft
_ref Oblig
_obl SpecType
t) = SpecType -> SM [CoreExpr]
go SpecType
t

    go t :: SpecType
t@RFun{} 
         = do [Var]
ys <- (SpecType -> StateT SState IO Var)
-> [SpecType] -> StateT SState IO [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SpecType -> StateT SState IO Var
freshVar [SpecType]
txs
              let su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (Symbol -> Expr
EVar (Symbol -> Expr) -> (Var -> Symbol) -> Var -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Var -> Expr) -> [Var] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
ys) 
              ((Var, SpecType) -> SM ()) -> [(Var, SpecType)] -> SM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Var -> SpecType -> SM ()) -> (Var, SpecType) -> SM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> SpecType -> SM ()
addEnv) ([Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
ys ((Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
subst Subst
su)(SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
txs)) 
              let dt :: SpecType
dt = Var -> SpecType -> [Var] -> [(Symbol, SpecType)] -> SpecType
decrType Var
xtop SpecType
ttop [Var]
ys ([Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
txs)
              Var -> SpecType -> SM ()
addEnv Var
xtop SpecType
dt 
              ((Var, SpecType) -> SM ()) -> [(Var, SpecType)] -> SM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Var -> SpecType -> SM ()) -> (Var, SpecType) -> SM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> SpecType -> SM ()
addEmem) ([Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
ys (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
subst Subst
su (SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
txs)) 
              Var -> SpecType -> SM ()
addEmem Var
xtop SpecType
dt
              HashMap Symbol (SpecType, Var)
senv1 <- SM (HashMap Symbol (SpecType, Var))
getSEnv
              let goalType :: SpecType
goalType = Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
subst Subst
su SpecType
to
                  hsGoalTy :: Type
hsGoalTy = SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
goalType 
                  ts :: [Type]
ts = Type -> [Type]
unifyWith Type
hsGoalTy
              if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ts  then (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = Maybe [Type]
forall a. Maybe a
Nothing } )
                          else (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
ts } )
              (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sForalls :: ([Var], [[Type]])
sForalls = ([Var]
foralls, []) } )
              ExprMemory
emem0 <- HashMap Symbol (SpecType, Var) -> SM ExprMemory
insEMem0 HashMap Symbol (SpecType, Var)
senv1
              (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sExprMem :: ExprMemory
sExprMem = ExprMemory
emem0 })
              (Var -> SM ()) -> [Var] -> SM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Var
y -> Var -> [Var] -> SM ()
addDecrTerm Var
y []) [Var]
ys
              [(CoreExpr, Type, TyCon)]
scruts <- [Var] -> SM [(CoreExpr, Type, TyCon)]
synthesizeScrut [Var]
ys
              (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { scrutinees :: [(CoreExpr, Type, TyCon)]
scrutinees = [(CoreExpr, Type, TyCon)]
scruts })
              [Var] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
GHC.mkLams [Var]
ys (CoreExpr -> CoreExpr) -> SM [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) (n :: * -> *) a b.
(Functor m, Functor n) =>
(a -> b) -> m (n a) -> m (n b)
<$$> SpecType -> SM [CoreExpr]
synthesizeBasic SpecType
goalType
      where (([Symbol], [SpecType], [RReft])
_, ([Symbol]
xs, [SpecType]
txs, [RReft]
_), SpecType
to) = SpecType
-> (([Symbol], [SpecType], [RReft]),
    ([Symbol], [SpecType], [RReft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RType t t1 a], [a]),
    ([Symbol], [RType t t1 a], [a]), RType t t1 a)
bkArrow SpecType
t 

    go SpecType
t = FilePath -> SM [CoreExpr]
forall a. HasCallStack => FilePath -> a
error (FilePath
" Unmatched t = " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SpecType -> FilePath
forall a. Show a => a -> FilePath
show SpecType
t)

synthesizeBasic :: SpecType -> SM [CoreExpr]
synthesizeBasic :: SpecType -> SM [CoreExpr]
synthesizeBasic SpecType
t = do
  let ts :: [Type]
ts = Type -> [Type]
unifyWith (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t) -- All the types that are used for instantiation.
  if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ts  then  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = Maybe [Type]
forall a. Maybe a
Nothing } )
              else  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sUGoalTy :: Maybe [Type]
sUGoalTy = [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
ts } )
  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sGoalTys :: [Type]
sGoalTys = [] })
  SpecType -> SM ()
fixEMem SpecType
t
  [CoreExpr]
es <- SpecType -> SM [CoreExpr]
genTerms SpecType
t
  if [CoreExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreExpr]
es  then SpecType -> SM [CoreExpr]
synthesizeMatch SpecType
t
              else [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
es

synthesizeMatch :: SpecType -> SM [CoreExpr]
synthesizeMatch :: SpecType -> SM [CoreExpr]
synthesizeMatch SpecType
t = do
  [(CoreExpr, Type, TyCon)]
scruts <- SState -> [(CoreExpr, Type, TyCon)]
scrutinees (SState -> [(CoreExpr, Type, TyCon)])
-> StateT SState IO SState -> SM [(CoreExpr, Type, TyCon)]
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
  Int
i <- SM Int
incrCase 
  case Int -> [(CoreExpr, Type, TyCon)] -> Maybe Int
forall a. Int -> [a] -> Maybe Int
safeIxScruts Int
i [(CoreExpr, Type, TyCon)]
scruts of
    Maybe Int
Nothing ->  [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just Int
id ->  if [(CoreExpr, Type, TyCon)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CoreExpr, Type, TyCon)]
scruts
                  then [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                  else SM [CoreExpr] -> SM [CoreExpr]
forall a. Monoid a => SM a -> SM a
withIncrDepth (SpecType -> (CoreExpr, Type, TyCon) -> SM [CoreExpr]
matchOnExpr SpecType
t ([(CoreExpr, Type, TyCon)]
scruts [(CoreExpr, Type, TyCon)] -> Int -> (CoreExpr, Type, TyCon)
forall a. [a] -> Int -> a
!! Int
id))

synthesizeScrut :: [Var] -> SM [(CoreExpr, Type, TyCon)]
synthesizeScrut :: [Var] -> SM [(CoreExpr, Type, TyCon)]
synthesizeScrut [Var]
vs = do
  [CoreExpr]
exprs <- [Var] -> SM [CoreExpr]
synthesizeScrutinee [Var]
vs
  let exprs' :: [(Type, CoreExpr)]
exprs' = (CoreExpr -> (Type, CoreExpr)) -> [CoreExpr] -> [(Type, CoreExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\CoreExpr
e -> (CoreExpr -> Type
exprType CoreExpr
e, CoreExpr
e)) [CoreExpr]
exprs
      isDataCon :: Var -> Bool
isDataCon Var
v = case Var -> Type
varType Var
v of { TyConApp TyCon
c [Type]
_ -> Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Bool
isClassTyCon (TyCon -> Bool) -> TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon
c; Type
_ -> Bool
False }
      vs0 :: [Var]
vs0 = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isDataCon [Var]
vs
      es0 :: [Expr b]
es0 = (Var -> Expr b) -> [Var] -> [Expr b]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Expr b
forall b. Var -> Expr b
GHC.Var [Var]
vs0 
      es1 :: [(Type, CoreExpr)]
es1 = (CoreExpr -> (Type, CoreExpr)) -> [CoreExpr] -> [(Type, CoreExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\CoreExpr
e -> (CoreExpr -> Type
exprType CoreExpr
e, CoreExpr
e)) [CoreExpr]
forall b. [Expr b]
es0
      es2 :: [(CoreExpr, Type, TyCon)]
es2 = [(CoreExpr
e, Type
t, TyCon
c) | (t :: Type
t@(TyConApp TyCon
c [Type]
_), CoreExpr
e) <- [(Type, CoreExpr)]
es1]
  [(CoreExpr, Type, TyCon)] -> SM [(CoreExpr, Type, TyCon)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(CoreExpr, Type, TyCon)]
es2 [(CoreExpr, Type, TyCon)]
-> [(CoreExpr, Type, TyCon)] -> [(CoreExpr, Type, TyCon)]
forall a. [a] -> [a] -> [a]
++ [(CoreExpr
e, Type
t, TyCon
c) | (t :: Type
t@(TyConApp TyCon
c [Type]
_), CoreExpr
e) <- [(Type, CoreExpr)]
exprs'])

matchOnExpr :: SpecType -> (CoreExpr, Type, TyCon) -> SM [CoreExpr]
matchOnExpr :: SpecType -> (CoreExpr, Type, TyCon) -> SM [CoreExpr]
matchOnExpr SpecType
t (GHC.Var Var
v, Type
tx, TyCon
c) 
  = SpecType -> (Var, Type, TyCon) -> SM [CoreExpr]
matchOn SpecType
t (Var
v, Type
tx, TyCon
c)
matchOnExpr SpecType
t (CoreExpr
e, Type
tx, TyCon
c)
  = do  Var
freshV <- Type -> StateT SState IO Var
freshVarType Type
tx
        SpecType
freshSpecTy <- 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
tx
        -- use consE
        Var -> SpecType -> SM ()
addEnv Var
freshV SpecType
freshSpecTy
        [CoreExpr]
es <- SpecType -> (Var, Type, TyCon) -> SM [CoreExpr]
matchOn SpecType
t (Var
freshV, Type
tx, TyCon
c)
        [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
$ CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
GHC.Let (Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
GHC.NonRec Var
freshV CoreExpr
e) (CoreExpr -> CoreExpr) -> [CoreExpr] -> [CoreExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreExpr]
es

matchOn :: SpecType -> (Var, Type, TyCon) -> SM [CoreExpr]
matchOn :: SpecType -> (Var, Type, TyCon) -> SM [CoreExpr]
matchOn SpecType
t (Var
v, Type
tx, TyCon
c) =
  (CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
GHC.Case (Var -> CoreExpr
forall b. Var -> Expr b
GHC.Var Var
v) Var
v Type
tx ([Alt Var] -> CoreExpr)
-> ([[Alt Var]] -> [[Alt Var]]) -> [[Alt Var]] -> [CoreExpr]
forall (m :: * -> *) (n :: * -> *) a b.
(Functor m, Functor n) =>
(a -> b) -> m (n a) -> m (n b)
<$$> [[Alt Var]] -> [[Alt Var]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence) ([[Alt Var]] -> [CoreExpr])
-> StateT SState IO [[Alt Var]] -> SM [CoreExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCon -> StateT SState IO [Alt Var])
-> [DataCon] -> StateT SState IO [[Alt Var]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SpecType -> (Var, Type) -> DataCon -> StateT SState IO [Alt Var]
makeAlt SpecType
t (Var
v, Type
tx)) (TyCon -> [DataCon]
tyConDataCons TyCon
c)


makeAlt :: SpecType -> (Var, Type) -> DataCon -> SM [GHC.CoreAlt]
makeAlt :: SpecType -> (Var, Type) -> DataCon -> StateT SState IO [Alt Var]
makeAlt SpecType
t (Var
x, TyConApp TyCon
_ [Type]
ts) DataCon
c = StateT SState IO [Alt Var] -> StateT SState IO [Alt Var]
forall a. SM a -> SM a
locally (StateT SState IO [Alt Var] -> StateT SState IO [Alt Var])
-> StateT SState IO [Alt Var] -> StateT SState IO [Alt Var]
forall a b. (a -> b) -> a -> b
$ do
  [SpecType]
ts <- 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) -> [Type] -> CG [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> CG SpecType
trueTy [Type]
τs
  [Var]
xs <- (SpecType -> StateT SState IO Var)
-> [SpecType] -> StateT SState IO [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SpecType -> StateT SState IO Var
freshVar [SpecType]
ts    
  [(CoreExpr, Type, TyCon)]
newScruts <- [Var] -> SM [(CoreExpr, Type, TyCon)]
synthesizeScrut [Var]
xs
  (SState -> SState) -> SM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { scrutinees :: [(CoreExpr, Type, TyCon)]
scrutinees = SState -> [(CoreExpr, Type, TyCon)]
scrutinees SState
s [(CoreExpr, Type, TyCon)]
-> [(CoreExpr, Type, TyCon)] -> [(CoreExpr, Type, TyCon)]
forall a. [a] -> [a] -> [a]
++ [(CoreExpr, Type, TyCon)]
newScruts } )
  [(Var, SpecType)] -> SM ()
addsEnv ([(Var, SpecType)] -> SM ()) -> [(Var, SpecType)] -> SM ()
forall a b. (a -> b) -> a -> b
$ [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [SpecType]
ts 
  [(Var, SpecType)] -> SM ()
addsEmem ([(Var, SpecType)] -> SM ()) -> [(Var, SpecType)] -> SM ()
forall a b. (a -> b) -> a -> b
$ [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [SpecType]
ts 
  Var -> [Var] -> SM ()
addDecrTerm Var
x [Var]
xs
  (CGEnv -> CG CGEnv) -> SM ()
liftCG0 (\CGEnv
γ -> CGEnv
-> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
caseEnv CGEnv
γ Var
x [AltCon]
forall a. Monoid a => a
mempty (DataCon -> AltCon
GHC.DataAlt DataCon
c) [Var]
xs Maybe [Int]
forall a. Maybe a
Nothing)
  [CoreExpr]
es <- SpecType -> SM [CoreExpr]
synthesizeBasic SpecType
t
  [Alt Var] -> StateT SState IO [Alt Var]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Alt Var] -> StateT SState IO [Alt Var])
-> [Alt Var] -> StateT SState IO [Alt Var]
forall a b. (a -> b) -> a -> b
$ (DataCon -> AltCon
GHC.DataAlt DataCon
c, [Var]
xs, ) (CoreExpr -> Alt Var) -> [CoreExpr] -> [Alt Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreExpr]
es
  where 
    ([Var]
_, [Type]
_, [Type]
τs) = DataCon -> [Type] -> ([Var], [Type], [Type])
dataConInstSig DataCon
c [Type]
ts
makeAlt SpecType
_ (Var, Type)
_ DataCon
_ = FilePath -> StateT SState IO [Alt Var]
forall a. HasCallStack => FilePath -> a
error FilePath
"makeAlt.bad argument "