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

module Language.Haskell.Liquid.Synthesize.Generate where

import           Language.Haskell.Liquid.Types
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.Synthesize.Check
import           CoreSyn                        ( CoreExpr )
import qualified CoreSyn                       as GHC
import           Data.Maybe
import           Control.Monad.State.Lazy
import           Language.Haskell.Liquid.Constraint.Fresh
                                                ( trueTy )
import           Data.List
import           CoreUtils (exprType)
import           Var
import           Data.Tuple.Extra
import           Debug.Trace
import           Language.Fixpoint.Types.PrettyPrint (tracepp)
import           TyCoRep

-- Generate terms that have type t: This changes the @ExprMemory@ in @SM@ state.
-- Return expressions type checked against type @specTy@.
genTerms :: SpecType -> SM [CoreExpr] 
genTerms :: SpecType -> SM [CoreExpr]
genTerms = SearchMode -> SpecType -> SM [CoreExpr]
genTerms' SearchMode
ResultMode 


data SearchMode 
  = ArgsMode          -- ^ searching for arguments of functions that can eventually 
                      --   produce the top level hole fill
  | ResultMode        -- ^ searching for the hole fill 
  deriving (SearchMode -> SearchMode -> Bool
(SearchMode -> SearchMode -> Bool)
-> (SearchMode -> SearchMode -> Bool) -> Eq SearchMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SearchMode -> SearchMode -> Bool
$c/= :: SearchMode -> SearchMode -> Bool
== :: SearchMode -> SearchMode -> Bool
$c== :: SearchMode -> SearchMode -> Bool
Eq, Int -> SearchMode -> ShowS
[SearchMode] -> ShowS
SearchMode -> String
(Int -> SearchMode -> ShowS)
-> (SearchMode -> String)
-> ([SearchMode] -> ShowS)
-> Show SearchMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SearchMode] -> ShowS
$cshowList :: [SearchMode] -> ShowS
show :: SearchMode -> String
$cshow :: SearchMode -> String
showsPrec :: Int -> SearchMode -> ShowS
$cshowsPrec :: Int -> SearchMode -> ShowS
Show) 

genTerms' :: SearchMode -> SpecType -> SM [CoreExpr] 
genTerms' :: SearchMode -> SpecType -> SM [CoreExpr]
genTerms' SearchMode
i SpecType
specTy = 
  do  [Type]
goalTys <- SState -> [Type]
sGoalTys (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
      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
== SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
specTy) [Type]
goalTys of 
        Maybe Type
Nothing -> (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sGoalTys :: [Type]
sGoalTys = (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
specTy) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: SState -> [Type]
sGoalTys SState
s })
        Just Type
_  -> () -> StateT SState IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      SpecType -> StateT SState IO ()
fixEMem SpecType
specTy 
      [(Type, CoreExpr, Int)]
fnTys <- Type -> SM [(Type, CoreExpr, Int)]
functionCands (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
specTy)
      [CoreExpr]
es    <- SpecType -> SM [CoreExpr]
withTypeEs SpecType
specTy 
      [CoreExpr]
es0   <- [CoreExpr] -> SM [CoreExpr]
structuralCheck [CoreExpr]
es

      Maybe CoreExpr
err <- SpecType -> SM (Maybe CoreExpr)
checkError SpecType
specTy 
      case Maybe CoreExpr
err of 
        Maybe CoreExpr
Nothing ->
          (CoreExpr -> StateT SState IO Bool)
-> [CoreExpr] -> SM [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m [a] -> m [a]
filterElseM (SpecType -> CoreExpr -> StateT SState IO Bool
hasType SpecType
specTy) [CoreExpr]
es0 (SM [CoreExpr] -> SM [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall a b. (a -> b) -> a -> b
$ 
            SearchMode
-> SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFill SearchMode
i SpecType
specTy Int
0 [(Type, CoreExpr, Int)]
fnTys
        Just CoreExpr
e -> [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr
e]

genArgs :: SpecType -> SM [CoreExpr]
genArgs :: SpecType -> SM [CoreExpr]
genArgs SpecType
t =
  do  [Type]
goalTys <- SState -> [Type]
sGoalTys (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
      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
== SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t) [Type]
goalTys of 
        Maybe Type
Nothing -> do (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sGoalTys :: [Type]
sGoalTys = SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: SState -> [Type]
sGoalTys SState
s }) 
                      SpecType -> StateT SState IO ()
fixEMem SpecType
t 
                      [(Type, CoreExpr, Int)]
fnTys <- Type -> SM [(Type, CoreExpr, Int)]
functionCands (SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t)
                      [CoreExpr]
es <- SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFillArgs SpecType
t Int
0 [(Type, CoreExpr, Int)]
fnTys
                      if [CoreExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreExpr]
es
                        then  [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                        else  do  -- modify (\s -> s {sExprId = sExprId s + 1})
                                  [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
es
        Just Type
_  -> [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []

withDepthFillArgs :: SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFillArgs :: SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFillArgs SpecType
t Int
depth [(Type, CoreExpr, Int)]
cs = do
  [(Type, CoreExpr, Int)]
thisEm <- SState -> [(Type, CoreExpr, Int)]
sExprMem (SState -> [(Type, CoreExpr, Int)])
-> StateT SState IO SState -> SM [(Type, CoreExpr, 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
  [CoreExpr]
es <- [(Type, CoreExpr, Int)]
-> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
argsFill [(Type, CoreExpr, Int)]
thisEm [(Type, CoreExpr, Int)]
cs []
  Int
argsDepth <- SM Int
localMaxArgsDepth

  (CoreExpr -> StateT SState IO Bool)
-> [CoreExpr] -> SM [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m [a] -> m [a]
filterElseM (SpecType -> CoreExpr -> StateT SState IO Bool
hasType SpecType
t) [CoreExpr]
es (SM [CoreExpr] -> SM [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall a b. (a -> b) -> a -> b
$
    if Int
depth Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
argsDepth
      then  String -> SM [CoreExpr] -> SM [CoreExpr]
forall a. String -> a -> a
trace (String
" [ withDepthFillArgs ] argsDepth = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
argsDepth) (SM [CoreExpr] -> SM [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall a b. (a -> b) -> a -> b
$ SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFillArgs SpecType
t (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Type, CoreExpr, Int)]
cs
      else  [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []

argsFill :: ExprMemory -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
argsFill :: [(Type, CoreExpr, Int)]
-> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
argsFill [(Type, CoreExpr, Int)]
_   []               [CoreExpr]
es0 = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
es0 
argsFill [(Type, CoreExpr, Int)]
em0 ((Type, CoreExpr, Int)
c:[(Type, CoreExpr, Int)]
cs) [CoreExpr]
es0 =
  case Type -> Maybe (Type, [Type])
subgoals ((Type, CoreExpr, Int) -> Type
forall a b c. (a, b, c) -> a
fst3 (Type, CoreExpr, Int)
c) of
    Maybe (Type, [Type])
Nothing             -> [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [] 
    Just (Type
resTy, [Type]
subGs) -> 
      do  let argCands :: [[(CoreExpr, Int)]]
argCands = (Type -> [(CoreExpr, Int)]) -> [Type] -> [[(CoreExpr, Int)]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Type, CoreExpr, Int)] -> Type -> [(CoreExpr, Int)]
withSubgoal [(Type, CoreExpr, Int)]
em0) [Type]
subGs
              toGen :: Bool
toGen    = ([(CoreExpr, Int)] -> Bool -> Bool)
-> Bool -> [[(CoreExpr, Int)]] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[(CoreExpr, Int)]
x Bool
b -> (Bool -> Bool
not (Bool -> Bool)
-> ([(CoreExpr, Int)] -> Bool) -> [(CoreExpr, Int)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(CoreExpr, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(CoreExpr, Int)]
x Bool -> Bool -> Bool
&& Bool
b) Bool
True (String -> [[(CoreExpr, Int)]] -> [[(CoreExpr, Int)]]
forall a. PPrint a => String -> a -> a
tracepp (String
" [ argsFill ] for c = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show ((Type, CoreExpr, Int) -> CoreExpr
forall a b c. (a, b, c) -> b
snd3 (Type, CoreExpr, Int)
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" argCands ") [[(CoreExpr, Int)]]
argCands)
          [CoreExpr]
es <- do  Int
curExprId <- 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
                    if Bool
toGen then 
                      Int
-> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
prune Int
curExprId (Type, CoreExpr, Int)
c [[(CoreExpr, Int)]]
argCands
                      else [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          Int
curExprId <- 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
          let nextEm :: [(Type, CoreExpr, Int)]
nextEm = (CoreExpr -> (Type, CoreExpr, Int))
-> [CoreExpr] -> [(Type, CoreExpr, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Type
resTy, , Int
curExprId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [CoreExpr]
es
          (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sExprMem :: [(Type, CoreExpr, Int)]
sExprMem = [(Type, CoreExpr, Int)]
nextEm [(Type, CoreExpr, Int)]
-> [(Type, CoreExpr, Int)] -> [(Type, CoreExpr, Int)]
forall a. [a] -> [a] -> [a]
++ SState -> [(Type, CoreExpr, Int)]
sExprMem SState
s })
          [(Type, CoreExpr, Int)]
-> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
argsFill [(Type, CoreExpr, Int)]
em0 [(Type, CoreExpr, Int)]
cs ([CoreExpr]
es [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr]
es0)

withDepthFill :: SearchMode -> SpecType -> Int -> [(Type, GHC.CoreExpr, Int)] -> SM [CoreExpr]
withDepthFill :: SearchMode
-> SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFill SearchMode
i SpecType
t Int
depth [(Type, CoreExpr, Int)]
tmp = do
  [CoreExpr]
exprs <- SearchMode
-> Int -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
fill SearchMode
i Int
depth [(Type, CoreExpr, Int)]
tmp []
  Int
appDepth <- SM Int
localMaxAppDepth

  (CoreExpr -> StateT SState IO Bool)
-> [CoreExpr] -> SM [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m [a] -> m [a]
filterElseM (SpecType -> CoreExpr -> StateT SState IO Bool
hasType SpecType
t) [CoreExpr]
exprs (SM [CoreExpr] -> SM [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall a b. (a -> b) -> a -> b
$ 
      if Int
depth Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
appDepth
        then do (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s { sExprId :: Int
sExprId = SState -> Int
sExprId SState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 })
                SearchMode
-> SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
withDepthFill SearchMode
i SpecType
t (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Type, CoreExpr, Int)]
tmp
        else [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []

fill :: SearchMode -> Int -> [(Type, GHC.CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr] 
fill :: SearchMode
-> Int -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
fill SearchMode
_ Int
_     []                 [CoreExpr]
accExprs 
  = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
accExprs
fill SearchMode
i Int
depth ((Type, CoreExpr, Int)
c : [(Type, CoreExpr, Int)]
cs) [CoreExpr]
accExprs 
  = case Type -> Maybe (Type, [Type])
subgoals ((Type, CoreExpr, Int) -> Type
forall a b c. (a, b, c) -> a
fst3 (Type, CoreExpr, Int)
c) of 
      Maybe (Type, [Type])
Nothing             -> [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- Not a function type
      Just (Type
resTy, [Type]
subGs) ->
        do  [SpecType]
specSubGs <- 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 -> StateT CGInfo Identity SpecType)
-> [Type] -> CG [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> StateT CGInfo Identity SpecType
trueTy ((Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isFunction) [Type]
subGs)
            (SpecType -> SM [CoreExpr]) -> [SpecType] -> StateT SState IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SpecType -> SM [CoreExpr]
genArgs [SpecType]
specSubGs
            [(Type, CoreExpr, Int)]
em <- SState -> [(Type, CoreExpr, Int)]
sExprMem (SState -> [(Type, CoreExpr, Int)])
-> StateT SState IO SState -> SM [(Type, CoreExpr, 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 argCands :: [[(CoreExpr, Int)]]
argCands  = (Type -> [(CoreExpr, Int)]) -> [Type] -> [[(CoreExpr, Int)]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Type, CoreExpr, Int)] -> Type -> [(CoreExpr, Int)]
withSubgoal [(Type, CoreExpr, Int)]
em) [Type]
subGs
                toGen :: Bool
toGen    = ([(CoreExpr, Int)] -> Bool -> Bool)
-> Bool -> [[(CoreExpr, Int)]] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[(CoreExpr, Int)]
x Bool
b -> (Bool -> Bool
not (Bool -> Bool)
-> ([(CoreExpr, Int)] -> Bool) -> [(CoreExpr, Int)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(CoreExpr, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(CoreExpr, Int)]
x Bool -> Bool -> Bool
&& Bool
b) Bool
True [[(CoreExpr, Int)]]
argCands
            [CoreExpr]
newExprs <- do  Int
curExprId <- 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 
                            if Bool
toGen 
                              then Int
-> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
prune Int
curExprId (Type, CoreExpr, Int)
c (String -> [[(CoreExpr, Int)]] -> [[(CoreExpr, Int)]]
forall a. PPrint a => String -> a -> a
tracepp (String
" [ fill " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
curExprId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ] For c = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show ((Type, CoreExpr, Int) -> CoreExpr
forall a b c. (a, b, c) -> b
snd3 (Type, CoreExpr, Int)
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" argCands ") [[(CoreExpr, Int)]]
argCands)
                              else [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
            Int
curExprId <- 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
            let nextEm :: [(Type, CoreExpr, Int)]
nextEm = (CoreExpr -> (Type, CoreExpr, Int))
-> [CoreExpr] -> [(Type, CoreExpr, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Type
resTy, , Int
curExprId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [CoreExpr]
newExprs
            (SState -> SState) -> StateT SState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SState
s -> SState
s {sExprMem :: [(Type, CoreExpr, Int)]
sExprMem = [(Type, CoreExpr, Int)]
nextEm [(Type, CoreExpr, Int)]
-> [(Type, CoreExpr, Int)] -> [(Type, CoreExpr, Int)]
forall a. [a] -> [a] -> [a]
++ SState -> [(Type, CoreExpr, Int)]
sExprMem SState
s }) 
            let accExprs' :: [CoreExpr]
accExprs' = [CoreExpr]
newExprs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr]
accExprs
            SearchMode
-> Int -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
fill SearchMode
i Int
depth [(Type, CoreExpr, Int)]
cs [CoreExpr]
accExprs' 

-------------------------------------------------------------------------------------------
-- |                       Pruning terms for function application                      | --
-------------------------------------------------------------------------------------------
type Depth = Int

feasible :: Depth -> (CoreExpr, Int) -> Bool
feasible :: Int -> (CoreExpr, Int) -> Bool
feasible Int
d (CoreExpr, Int)
c = (CoreExpr, Int) -> Int
forall a b. (a, b) -> b
snd (CoreExpr, Int)
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
d

feasibles :: Depth -> Int -> [(CoreExpr, Int)] -> [Int]
feasibles :: Int -> Int -> [(CoreExpr, Int)] -> [Int]
feasibles Int
_ Int
_ []
  = []
feasibles Int
d Int
i ((CoreExpr, Int)
c:[(CoreExpr, Int)]
cs) 
  = if Int -> (CoreExpr, Int) -> Bool
feasible Int
d (CoreExpr, Int)
c 
      then Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int -> Int -> [(CoreExpr, Int)] -> [Int]
feasibles Int
d (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(CoreExpr, Int)]
cs
      else Int -> Int -> [(CoreExpr, Int)] -> [Int]
feasibles Int
d (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(CoreExpr, Int)]
cs

isFeasible :: Depth -> [[(CoreExpr, Int)]] -> [[Int]]
isFeasible :: Int -> [[(CoreExpr, Int)]] -> [[Int]]
isFeasible Int
d =  ([(CoreExpr, Int)] -> [Int]) -> [[(CoreExpr, Int)]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> [(CoreExpr, Int)] -> [Int]
feasibles Int
d Int
0)

findFeasibles :: Depth -> [[(CoreExpr, Int)]] -> ([[Int]], [Int])
findFeasibles :: Int -> [[(CoreExpr, Int)]] -> ([[Int]], [Int])
findFeasibles Int
d [[(CoreExpr, Int)]]
cs = ([[Int]]
fs, [Int]
ixs)
  where fs :: [[Int]]
fs  = Int -> [[(CoreExpr, Int)]] -> [[Int]]
isFeasible Int
d [[(CoreExpr, Int)]]
cs
        ixs :: [Int]
ixs = [Int
i | (Int
i, [Int]
f) <- [Int] -> [[Int]] -> [(Int, [Int])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [[Int]]
fs, Bool -> Bool
not ([Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
f)]

toExpr :: [Int] ->                    --  Produced from @isFeasible@.
                                      --   Assumed in increasing order.
          [(GHC.CoreExpr, Int)] ->    --  The candidate expressions.
          ([(GHC.CoreExpr, Int)],     --  Expressions from 2nd argument.
           [(GHC.CoreExpr, Int)])     --  The rest of the expressions
toExpr :: [Int]
-> [(CoreExpr, Int)] -> ([(CoreExpr, Int)], [(CoreExpr, Int)])
toExpr [Int]
ixs [(CoreExpr, Int)]
args = ( [ [(CoreExpr, Int)]
args [(CoreExpr, Int)] -> Int -> (CoreExpr, Int)
forall a. [a] -> Int -> a
!! Int
i | (Int
ix, Int
i) <- [(Int, Int)]
is, Int
ix Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i ], 
                    [ [(CoreExpr, Int)]
args [(CoreExpr, Int)] -> Int -> (CoreExpr, Int)
forall a. [a] -> Int -> a
!! Int
i | (Int
ix, Int
i) <- [(Int, Int)]
is, Int
ix Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i ])
    where is :: [(Int, Int)]
is = [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Int]
ixs

fixCands :: Int -> [Int] -> [[(CoreExpr, Int)]] -> ([[(CoreExpr, Int)]], [[(CoreExpr, Int)]])
fixCands :: Int
-> [Int]
-> [[(CoreExpr, Int)]]
-> ([[(CoreExpr, Int)]], [[(CoreExpr, Int)]])
fixCands Int
i [Int]
ixs [[(CoreExpr, Int)]]
args 
  = let cs :: [(CoreExpr, Int)]
cs = [[(CoreExpr, Int)]]
args [[(CoreExpr, Int)]] -> Int -> [(CoreExpr, Int)]
forall a. [a] -> Int -> a
!! Int
i
        ([(CoreExpr, Int)]
cur, [(CoreExpr, Int)]
next)    = [Int]
-> [(CoreExpr, Int)] -> ([(CoreExpr, Int)], [(CoreExpr, Int)])
toExpr [Int]
ixs [(CoreExpr, Int)]
cs
        ([[(CoreExpr, Int)]]
args0, [[(CoreExpr, Int)]]
args1) = (Int
-> [(CoreExpr, Int)] -> [[(CoreExpr, Int)]] -> [[(CoreExpr, Int)]]
forall a. Int -> a -> [a] -> [a]
replace (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(CoreExpr, Int)]
cur [[(CoreExpr, Int)]]
args, Int
-> [(CoreExpr, Int)] -> [[(CoreExpr, Int)]] -> [[(CoreExpr, Int)]]
forall a. Int -> a -> [a] -> [a]
replace (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(CoreExpr, Int)]
next [[(CoreExpr, Int)]]
args)
    in  ([[(CoreExpr, Int)]]
args0, [[(CoreExpr, Int)]]
args1)

-- | The first argument should be an 1-based index.
replace :: Int -> a -> [a] -> [a]
replace :: Int -> a -> [a] -> [a]
replace 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

repeatFix :: [Int] -> [[Int]] -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> [CoreExpr] -> SM [CoreExpr]
repeatFix :: [Int]
-> [[Int]]
-> (Type, CoreExpr, Int)
-> [[(CoreExpr, Int)]]
-> [CoreExpr]
-> SM [CoreExpr]
repeatFix [ ] [[Int]]
_ (Type, CoreExpr, Int)
_ [[(CoreExpr, Int)]]
_ [CoreExpr]
es 
  = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
es
repeatFix (Int
i:[Int]
is) [[Int]]
ixs (Type, CoreExpr, Int)
toFill [[(CoreExpr, Int)]]
args [CoreExpr]
es
  = do  let ([[(CoreExpr, Int)]]
args0, [[(CoreExpr, Int)]]
args1) = Int
-> [Int]
-> [[(CoreExpr, Int)]]
-> ([[(CoreExpr, Int)]], [[(CoreExpr, Int)]])
fixCands Int
i ([[Int]]
ixs [[Int]] -> Int -> [Int]
forall a. [a] -> Int -> a
!! Int
i) [[(CoreExpr, Int)]]
args
        [CoreExpr]
es0 <- (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
fillOne (Type, CoreExpr, Int)
toFill [[(CoreExpr, Int)]]
args0
        [CoreExpr]
es1 <- [CoreExpr] -> SM [CoreExpr]
structuralCheck [CoreExpr]
es0
        [CoreExpr]
es2 <- ([CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr]
es) ([CoreExpr] -> [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> StateT SState IO Bool) -> [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM CoreExpr -> StateT SState IO Bool
isWellTyped [CoreExpr]
es1
        [Int]
-> [[Int]]
-> (Type, CoreExpr, Int)
-> [[(CoreExpr, Int)]]
-> [CoreExpr]
-> SM [CoreExpr]
repeatFix [Int]
is [[Int]]
ixs (Type, CoreExpr, Int)
toFill [[(CoreExpr, Int)]]
args1 [CoreExpr]
es2

prune :: Depth -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
prune :: Int
-> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
prune Int
d (Type, CoreExpr, Int)
toFill [[(CoreExpr, Int)]]
args 
  = do  let ([[Int]]
ixs, [Int]
is) = Int -> [[(CoreExpr, Int)]] -> ([[Int]], [Int])
findFeasibles Int
d [[(CoreExpr, Int)]]
args 
        [Int]
-> [[Int]]
-> (Type, CoreExpr, Int)
-> [[(CoreExpr, Int)]]
-> [CoreExpr]
-> SM [CoreExpr]
repeatFix [Int]
is [[Int]]
ixs (Type, CoreExpr, Int)
toFill [[(CoreExpr, Int)]]
args []


----------------------------------------------------------------------------
--  | Term generation: Perform type and term application for functions. | --
----------------------------------------------------------------------------

fillOne :: (Type, GHC.CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
fillOne :: (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
fillOne (Type, CoreExpr, Int)
_ [] 
  = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
fillOne (Type
t, CoreExpr
e, Int
_) [[(CoreExpr, Int)]]
cs 
  = [CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr]
applyTerms [CoreExpr
e] [[(CoreExpr, Int)]]
cs (((Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type])
-> (Type -> (Type, [Type])) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Type, [Type]) -> (Type, [Type])
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Type, [Type]) -> (Type, [Type]))
-> (Type -> Maybe (Type, [Type])) -> Type -> (Type, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, [Type])
subgoals) Type
t)

applyTerm :: [GHC.CoreExpr] -> [(CoreExpr, Int)] -> Type -> SM [CoreExpr]
applyTerm :: [CoreExpr] -> [(CoreExpr, Int)] -> Type -> SM [CoreExpr]
applyTerm [CoreExpr]
es [(CoreExpr, Int)]
args Type
t = do
  [[CoreExpr]]
es1 <- ((CoreExpr, Int) -> SM [CoreExpr])
-> [(CoreExpr, Int)] -> StateT SState IO [[CoreExpr]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(CoreExpr, Int)
x -> [CoreExpr] -> (CoreExpr, Int) -> Type -> SM [CoreExpr]
applyArg [CoreExpr]
es (CoreExpr, Int)
x Type
t) [(CoreExpr, Int)]
args
  [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[CoreExpr]] -> [CoreExpr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CoreExpr]]
es1)

applyArg :: [GHC.CoreExpr] -> (CoreExpr, Int) -> Type -> SM [CoreExpr]
applyArg :: [CoreExpr] -> (CoreExpr, Int) -> Type -> SM [CoreExpr]
applyArg [CoreExpr]
es (CoreExpr
arg, Int
_) Type
t 
  = do  !Int
idx <- SM Int
incrSM
        [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return  [ case CoreExpr
arg of GHC.Var Id
_ -> CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
GHC.App CoreExpr
e CoreExpr
arg
                              CoreExpr
_         ->  let letv :: Id
letv = Maybe String -> Int -> Type -> Id
mkVar (String -> Maybe String
forall a. a -> Maybe a
Just (String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)) Int
idx Type
t
                                            in  Bind Id -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
GHC.Let (Id -> CoreExpr -> Bind Id
forall b. b -> Expr b -> Bind b
GHC.NonRec Id
letv CoreExpr
arg) (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
GHC.App CoreExpr
e (Id -> CoreExpr
forall b. Id -> Expr b
GHC.Var Id
letv))
                | CoreExpr
e <- [CoreExpr]
es 
                ]

applyTerms :: [GHC.CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr]
applyTerms :: [CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr]
applyTerms [CoreExpr]
es []     []      
  = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreExpr]
es
applyTerms [CoreExpr]
es0 ([(CoreExpr, Int)]
c:[[(CoreExpr, Int)]]
cs) (Type
t:[Type]
ts) 
  = do  [CoreExpr]
es1 <- [CoreExpr] -> [(CoreExpr, Int)] -> Type -> SM [CoreExpr]
applyTerm [CoreExpr]
es0 [(CoreExpr, Int)]
c Type
t
        [CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr]
applyTerms [CoreExpr]
es1 [[(CoreExpr, Int)]]
cs [Type]
ts
applyTerms [CoreExpr]
_es [[(CoreExpr, Int)]]
_cs [Type]
_ts 
  = String -> SM [CoreExpr]
forall a. HasCallStack => String -> a
error String
"[ applyTerms ] Wildcard. " 

--------------------------------------------------------------------------------------
prodScrutinees :: [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr]
prodScrutinees :: [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr]
prodScrutinees []     []     = [CoreExpr] -> SM [CoreExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
prodScrutinees ((Type, CoreExpr, Int)
c:[(Type, CoreExpr, Int)]
cs) ([[(CoreExpr, Int)]]
a:[[[(CoreExpr, Int)]]]
as) = do 
  [CoreExpr]
es <- (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
fillOne (Type, CoreExpr, Int)
c [[(CoreExpr, Int)]]
a
  ([CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr]
es) ([CoreExpr] -> [CoreExpr]) -> SM [CoreExpr] -> SM [CoreExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr]
prodScrutinees [(Type, CoreExpr, Int)]
cs [[[(CoreExpr, Int)]]]
as
prodScrutinees [(Type, CoreExpr, Int)]
_ [[[(CoreExpr, Int)]]]
_ = String -> SM [CoreExpr]
forall a. HasCallStack => String -> a
error String
" prodScrutinees "

synthesizeScrutinee :: [Var] -> SM [CoreExpr]
synthesizeScrutinee :: [Id] -> SM [CoreExpr]
synthesizeScrutinee [Id]
vars = do
  SState
s <- StateT SState IO SState
forall s (m :: * -> *). MonadState s m => m s
get
  let foralls :: [Id]
foralls = (([Id], [[Type]]) -> [Id]
forall a b. (a, b) -> a
fst (([Id], [[Type]]) -> [Id])
-> (SState -> ([Id], [[Type]])) -> SState -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SState -> ([Id], [[Type]])
sForalls) SState
s
      insVs :: [Id]
insVs = SState -> [Id]
sUniVars SState
s
      fix :: Id
fix   = SState -> Id
sFix SState
s
      -- Assign higher priority to function candidates that return tuples
      fnCs0 :: [Id]
fnCs0 = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
returnsTuple [Id]
foralls 
      fnCs :: [Id]
fnCs  = if Id -> Bool
returnsTuple Id
fix then Id
fix Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
fnCs0 else [Id]
fnCs0

      fnEs :: [Expr b]
fnEs  = (Id -> Expr b) -> [Id] -> [Expr b]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Expr b
forall b. Id -> Expr b
GHC.Var [Id]
fnCs
      fnCs' :: [CoreExpr]
fnCs' = (CoreExpr -> CoreExpr) -> [CoreExpr] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\CoreExpr
e -> CoreExpr -> Maybe [Id] -> CoreExpr
instantiate CoreExpr
e ([Id] -> Maybe [Id]
forall a. a -> Maybe a
Just [Id]
insVs)) [CoreExpr]
forall b. [Expr b]
fnEs
      sGs :: [[Type]]
sGs   = (CoreExpr -> [Type]) -> [CoreExpr] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type])
-> (Maybe (Type, [Type]) -> (Type, [Type]))
-> Maybe (Type, [Type])
-> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Type, [Type]) -> (Type, [Type])
forall a. HasCallStack => Maybe a -> a
fromJust) (Maybe (Type, [Type]) -> [Type])
-> (CoreExpr -> Maybe (Type, [Type])) -> CoreExpr -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, [Type])
subgoals (Type -> Maybe (Type, [Type]))
-> (CoreExpr -> Type) -> CoreExpr -> Maybe (Type, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Type
exprType) [CoreExpr]
fnCs'
      argCands :: [[[(CoreExpr, Int)]]]
argCands = ([Type] -> [[(CoreExpr, Int)]])
-> [[Type]] -> [[[(CoreExpr, Int)]]]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> [(CoreExpr, Int)]) -> [Type] -> [[(CoreExpr, Int)]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Type, CoreExpr, Int)] -> Type -> [(CoreExpr, Int)]
withSubgoal [(Type, CoreExpr, Int)]
forall b. [(Type, Expr b, Int)]
vs)) [[Type]]
sGs
      fnCs'' :: [(Type, CoreExpr, Int)]
fnCs'' = (CoreExpr -> (Type, CoreExpr, Int))
-> [CoreExpr] -> [(Type, CoreExpr, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\CoreExpr
e -> (CoreExpr -> Type
exprType CoreExpr
e, CoreExpr
e, Int
0)) [CoreExpr]
fnCs'
      
      vs' :: [Id]
vs' = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isFunction) (Type -> Bool) -> (Id -> Type) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
varType) [Id]
vars
      vs :: [(Type, Expr b, Int)]
vs  = (Id -> (Type, Expr b, Int)) -> [Id] -> [(Type, Expr b, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Id
v -> (Id -> Type
varType Id
v, Id -> Expr b
forall b. Id -> Expr b
GHC.Var Id
v, Int
0)) [Id]
vs'
  [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr]
prodScrutinees [(Type, CoreExpr, Int)]
fnCs'' [[[(CoreExpr, Int)]]]
argCands