{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RecordWildCards     #-}

{-@ LIQUID "--diff"     @-}

module Language.Haskell.Liquid.Liquid (
   -- * Executable command
    liquid

   -- * Single query
  , runLiquid

   -- * Ghci State
  , MbEnv

   -- * Liquid Constraint Generation 
  , liquidConstraints

   -- * Checking a single module
  , checkTargetInfo
  ) where

import           Prelude hiding (error)
import           Data.Bifunctor
import qualified Data.HashSet as S 
import           System.Exit
import           Text.PrettyPrint.HughesPJ
import           Var                              (Var)
import           CoreSyn
import           HscTypes                         (SourceError)
import           GHC (HscEnv)
import           System.Console.CmdArgs.Verbosity (whenLoud, whenNormal)
import           Control.Monad (when, unless)
import qualified Data.Maybe as Mb
import qualified Data.List  as L 
import qualified Control.Exception as Ex
import qualified Language.Haskell.Liquid.UX.DiffCheck as DC
import           Language.Haskell.Liquid.Misc
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Solver
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Synthesize (synthesize)
import           Language.Haskell.Liquid.UX.Errors
import           Language.Haskell.Liquid.UX.CmdLine
import           Language.Haskell.Liquid.UX.Tidy
import           Language.Haskell.Liquid.GHC.Misc (showCBs, ignoreCoreBinds) -- howPpr)
import           Language.Haskell.Liquid.GHC.Interface
import           Language.Haskell.Liquid.Constraint.Generate
import           Language.Haskell.Liquid.Constraint.ToFixpoint
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.UX.Annotate (mkOutput)
import qualified Language.Haskell.Liquid.Termination.Structural as ST
import qualified Language.Haskell.Liquid.GHC.Misc          as GM 

type MbEnv = Maybe HscEnv

--------------------------------------------------------------------------------
liquid :: [String] -> IO b
--------------------------------------------------------------------------------
liquid :: [String] -> IO b
liquid [String]
args = do 
  Config
cfg     <- [String] -> IO Config
getOpts [String]
args 
  IO ()
printLiquidHaskellBanner
  (ExitCode
ec, MbEnv
_) <- MbEnv -> Config -> IO (ExitCode, MbEnv)
runLiquid MbEnv
forall a. Maybe a
Nothing Config
cfg
  ExitCode -> IO b
forall a. ExitCode -> IO a
exitWith ExitCode
ec

--------------------------------------------------------------------------------
liquidConstraints :: Config -> IO (Either [CGInfo] ExitCode) 
--------------------------------------------------------------------------------
liquidConstraints :: Config -> IO (Either [CGInfo] ExitCode)
liquidConstraints Config
cfg = do 
  Either ErrorResult ([TargetInfo], MbEnv)
z <- IO ([TargetInfo], MbEnv)
-> IO (Either ErrorResult ([TargetInfo], MbEnv))
forall a. IO a -> IO (Either ErrorResult a)
actOrDie (IO ([TargetInfo], MbEnv)
 -> IO (Either ErrorResult ([TargetInfo], MbEnv)))
-> IO ([TargetInfo], MbEnv)
-> IO (Either ErrorResult ([TargetInfo], MbEnv))
forall a b. (a -> b) -> a -> b
$ (HscEnv -> MbEnv)
-> ([TargetInfo], HscEnv) -> ([TargetInfo], MbEnv)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second HscEnv -> MbEnv
forall a. a -> Maybe a
Just (([TargetInfo], HscEnv) -> ([TargetInfo], MbEnv))
-> IO ([TargetInfo], HscEnv) -> IO ([TargetInfo], MbEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MbEnv -> Config -> [String] -> IO ([TargetInfo], HscEnv)
getTargetInfos MbEnv
forall a. Maybe a
Nothing Config
cfg (Config -> [String]
files Config
cfg)
  case Either ErrorResult ([TargetInfo], MbEnv)
z of
    Left ErrorResult
e -> do
      Config -> [String] -> Output Doc -> IO ()
exitWithResult Config
cfg (Config -> [String]
files Config
cfg) (Output Doc -> IO ()) -> Output Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ Output Doc
forall a. Monoid a => a
mempty { o_result :: ErrorResult
o_result = ErrorResult
e }
      Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode))
-> Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode)
forall a b. (a -> b) -> a -> b
$ ExitCode -> Either [CGInfo] ExitCode
forall a b. b -> Either a b
Right (ExitCode -> Either [CGInfo] ExitCode)
-> ExitCode -> Either [CGInfo] ExitCode
forall a b. (a -> b) -> a -> b
$ ErrorResult -> ExitCode
forall a. FixResult a -> ExitCode
resultExit ErrorResult
e 
    Right ([TargetInfo]
gs, MbEnv
_) -> 
      Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode))
-> Either [CGInfo] ExitCode -> IO (Either [CGInfo] ExitCode)
forall a b. (a -> b) -> a -> b
$ [CGInfo] -> Either [CGInfo] ExitCode
forall a b. a -> Either a b
Left ([CGInfo] -> Either [CGInfo] ExitCode)
-> [CGInfo] -> Either [CGInfo] ExitCode
forall a b. (a -> b) -> a -> b
$ (TargetInfo -> CGInfo) -> [TargetInfo] -> [CGInfo]
forall a b. (a -> b) -> [a] -> [b]
map TargetInfo -> CGInfo
generateConstraints [TargetInfo]
gs

--------------------------------------------------------------------------------
runLiquid :: MbEnv -> Config -> IO (ExitCode, MbEnv)
--------------------------------------------------------------------------------
runLiquid :: MbEnv -> Config -> IO (ExitCode, MbEnv)
runLiquid MbEnv
mE Config
cfg  = do 
  [String]
reals <- MbEnv -> Config -> [String] -> IO [String]
realTargets MbEnv
mE Config
cfg (Config -> [String]
files Config
cfg)
  IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. PPrint a => a -> String
showpp (String -> Doc
text String
"Targets:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (String -> Doc
text (String -> Doc) -> [String] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
reals))
  Config -> MbEnv -> [String] -> IO (ExitCode, MbEnv)
checkTargets Config
cfg MbEnv
mE [String]
reals

checkTargets :: Config -> MbEnv -> [FilePath] -> IO (ExitCode, MbEnv)
checkTargets :: Config -> MbEnv -> [String] -> IO (ExitCode, MbEnv)
checkTargets Config
cfg  = MbEnv -> [String] -> IO (ExitCode, MbEnv)
go 
  where
    go :: MbEnv -> [String] -> IO (ExitCode, MbEnv)
go MbEnv
env []     = (ExitCode, MbEnv) -> IO (ExitCode, MbEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
ExitSuccess, MbEnv
env)
    go MbEnv
env (String
f:[String]
fs) = do IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> String -> IO ()
colorPhaseLn Moods
Loud (String
"[Checking: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]") String
""
                       (ExitCode
ec, MbEnv
env') <- MbEnv -> Config -> [String] -> IO (ExitCode, MbEnv)
runLiquidTargets MbEnv
env Config
cfg [String
f] 
                       case ExitCode
ec of 
                         ExitCode
ExitSuccess -> MbEnv -> [String] -> IO (ExitCode, MbEnv)
go MbEnv
env' [String]
fs
                         ExitCode
_           -> (ExitCode, MbEnv) -> IO (ExitCode, MbEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
ec, MbEnv
env')


--------------------------------------------------------------------------------
-- | @runLiquid@ checks a *target-list* of files, ASSUMING that we have 
--   already  run LH on ALL the (transitive) home imports -- i.e. other 
--   imports files for which we have source -- in order to build the .bspec 
--   files for those specs.
--------------------------------------------------------------------------------
runLiquidTargets :: MbEnv -> Config -> [FilePath] -> IO (ExitCode, MbEnv)
--------------------------------------------------------------------------------
runLiquidTargets :: MbEnv -> Config -> [String] -> IO (ExitCode, MbEnv)
runLiquidTargets MbEnv
mE Config
cfg [String]
targetFiles = do
  Either ErrorResult ([TargetInfo], MbEnv)
z <- IO ([TargetInfo], MbEnv)
-> IO (Either ErrorResult ([TargetInfo], MbEnv))
forall a. IO a -> IO (Either ErrorResult a)
actOrDie (IO ([TargetInfo], MbEnv)
 -> IO (Either ErrorResult ([TargetInfo], MbEnv)))
-> IO ([TargetInfo], MbEnv)
-> IO (Either ErrorResult ([TargetInfo], MbEnv))
forall a b. (a -> b) -> a -> b
$ (HscEnv -> MbEnv)
-> ([TargetInfo], HscEnv) -> ([TargetInfo], MbEnv)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second HscEnv -> MbEnv
forall a. a -> Maybe a
Just (([TargetInfo], HscEnv) -> ([TargetInfo], MbEnv))
-> IO ([TargetInfo], HscEnv) -> IO ([TargetInfo], MbEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MbEnv -> Config -> [String] -> IO ([TargetInfo], HscEnv)
getTargetInfos MbEnv
mE Config
cfg [String]
targetFiles
  case Either ErrorResult ([TargetInfo], MbEnv)
z of
    Left ErrorResult
e -> do
      Config -> [String] -> Output Doc -> IO ()
exitWithResult Config
cfg [String]
targetFiles (Output Doc -> IO ()) -> Output Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ Output Doc
forall a. Monoid a => a
mempty { o_result :: ErrorResult
o_result = ErrorResult
e }
      (ExitCode, MbEnv) -> IO (ExitCode, MbEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ErrorResult -> ExitCode
forall a. FixResult a -> ExitCode
resultExit ErrorResult
e, MbEnv
mE)
    Right ([TargetInfo]
gs, MbEnv
mE') -> do
      Output Doc
d <- Config -> Output Doc -> [TargetInfo] -> IO (Output Doc)
checkMany Config
cfg Output Doc
forall a. Monoid a => a
mempty [TargetInfo]
gs
      (ExitCode, MbEnv) -> IO (ExitCode, MbEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Output Doc -> ExitCode
forall a. Output a -> ExitCode
ec Output Doc
d, MbEnv
mE')
  where
    ec :: Output a -> ExitCode
ec = ErrorResult -> ExitCode
forall a. FixResult a -> ExitCode
resultExit (ErrorResult -> ExitCode)
-> (Output a -> ErrorResult) -> Output a -> ExitCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Output a -> ErrorResult
forall a. Output a -> ErrorResult
o_result

--------------------------------------------------------------------------------
checkMany :: Config -> Output Doc -> [TargetInfo] -> IO (Output Doc)
--------------------------------------------------------------------------------
checkMany :: Config -> Output Doc -> [TargetInfo] -> IO (Output Doc)
checkMany Config
cfg Output Doc
d (TargetInfo
g:[TargetInfo]
gs) = do
  Output Doc
d' <- Config -> TargetInfo -> IO (Output Doc)
checkOne Config
cfg TargetInfo
g
  Config -> Output Doc -> [TargetInfo] -> IO (Output Doc)
checkMany Config
cfg (Output Doc
d Output Doc -> Output Doc -> Output Doc
forall a. Monoid a => a -> a -> a
`mappend` Output Doc
d') [TargetInfo]
gs

checkMany Config
_ Output Doc
d [] =
  Output Doc -> IO (Output Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return Output Doc
d

--------------------------------------------------------------------------------
checkOne :: Config -> TargetInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
checkOne :: Config -> TargetInfo -> IO (Output Doc)
checkOne Config
cfg TargetInfo
g = do
  Either ErrorResult (Output Doc)
z <- IO (Output Doc) -> IO (Either ErrorResult (Output Doc))
forall a. IO a -> IO (Either ErrorResult a)
actOrDie (IO (Output Doc) -> IO (Either ErrorResult (Output Doc)))
-> IO (Output Doc) -> IO (Either ErrorResult (Output Doc))
forall a b. (a -> b) -> a -> b
$ TargetInfo -> IO (Output Doc)
liquidOne TargetInfo
g
  case Either ErrorResult (Output Doc)
z of
    Left  ErrorResult
e -> do
      let out :: Output a
out = Output a
forall a. Monoid a => a
mempty { o_result :: ErrorResult
o_result = ErrorResult
e }
      Config -> [String] -> Output Doc -> IO ()
exitWithResult Config
cfg [TargetSrc -> String
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
g)] Output Doc
forall a. Output a
out
      Output Doc -> IO (Output Doc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Output Doc
forall a. Output a
out
    Right Output Doc
r -> Output Doc -> IO (Output Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return Output Doc
r


actOrDie :: IO a -> IO (Either ErrorResult a)
actOrDie :: IO a -> IO (Either ErrorResult a)
actOrDie IO a
act =
    (a -> Either ErrorResult a
forall a b. b -> Either a b
Right (a -> Either ErrorResult a) -> IO a -> IO (Either ErrorResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO a
act)
      IO (Either ErrorResult a)
-> (SourceError -> IO (Either ErrorResult a))
-> IO (Either ErrorResult a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Ex.catch` (\(SourceError
e :: SourceError) -> SourceError -> IO (Either ErrorResult a)
forall a b. Result a => a -> IO (Either ErrorResult b)
handle SourceError
e)
      IO (Either ErrorResult a)
-> (Error -> IO (Either ErrorResult a))
-> IO (Either ErrorResult a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Ex.catch` (\(Error
e :: Error)       -> Error -> IO (Either ErrorResult a)
forall a b. Result a => a -> IO (Either ErrorResult b)
handle Error
e)
      IO (Either ErrorResult a)
-> (UserError -> IO (Either ErrorResult a))
-> IO (Either ErrorResult a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Ex.catch` (\(UserError
e :: UserError)   -> UserError -> IO (Either ErrorResult a)
forall a b. Result a => a -> IO (Either ErrorResult b)
handle UserError
e)
      IO (Either ErrorResult a)
-> ([Error] -> IO (Either ErrorResult a))
-> IO (Either ErrorResult a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Ex.catch` (\([Error]
e :: [Error])     -> [Error] -> IO (Either ErrorResult a)
forall a b. Result a => a -> IO (Either ErrorResult b)
handle [Error]
e)

handle :: (Result a) => a -> IO (Either ErrorResult b)
handle :: a -> IO (Either ErrorResult b)
handle = Either ErrorResult b -> IO (Either ErrorResult b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorResult b -> IO (Either ErrorResult b))
-> (a -> Either ErrorResult b) -> a -> IO (Either ErrorResult b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorResult -> Either ErrorResult b
forall a b. a -> Either a b
Left (ErrorResult -> Either ErrorResult b)
-> (a -> ErrorResult) -> a -> Either ErrorResult b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ErrorResult
forall a. Result a => a -> ErrorResult
result

--------------------------------------------------------------------------------
liquidOne :: TargetInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
liquidOne :: TargetInfo -> IO (Output Doc)
liquidOne TargetInfo
info = do
  Output Doc
out' <- TargetInfo -> IO (Output Doc)
checkTargetInfo TargetInfo
info
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Config -> Bool
compileSpec Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Output Doc -> IO ()
DC.saveResult String
tgt Output Doc
out'
  Config -> [String] -> Output Doc -> IO ()
exitWithResult Config
cfg [String
tgt] Output Doc
out'
  Output Doc -> IO (Output Doc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Output Doc
out'
  where
    cfg :: Config
cfg  = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info
    tgt :: String
tgt  = TargetSrc -> String
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
info)

--------------------------------------------------------------------------------
checkTargetInfo :: TargetInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
checkTargetInfo :: TargetInfo -> IO (Output Doc)
checkTargetInfo TargetInfo
info
  | Config -> Bool
compileSpec Config
cfg = do 
    Moods -> String -> IO ()
donePhase Moods
Loud String
"Only compiling specifications [skipping verification]"
    Output Doc -> IO (Output Doc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Output Doc
forall a. Monoid a => a
mempty { o_result :: ErrorResult
o_result = Stats -> ErrorResult
forall a. Stats -> FixResult a
F.Safe Stats
forall a. Monoid a => a
mempty }
  | Bool
otherwise = do
    IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Loud String
"Extracted Core using GHC"
    -- whenLoud  $ do putStrLn $ showpp info
                 -- putStrLn "*************** Original CoreBinds ***************************"
                 -- putStrLn $ render $ pprintCBs (cbs info)
    IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Loud String
"Transformed Core"
    IO () -> IO ()
whenLoud  (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do Moods -> String -> IO ()
donePhase Moods
Loud String
"transformRecExpr"
                   String -> IO ()
putStrLn String
"*************** Transform Rec Expr CoreBinds *****************"
                   String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> [CoreBind] -> String
showCBs (Config -> Bool
untidyCore Config
cfg) [CoreBind]
cbs'
                   -- putStrLn $ render $ pprintCBs cbs'
                   -- putStrLn $ showPpr cbs'
    Either [CoreBind] [DiffCheck]
edcs <- Config
-> [CoreBind]
-> String
-> TargetInfo
-> IO (Either [CoreBind] [DiffCheck])
newPrune Config
cfg [CoreBind]
cbs' String
tgt TargetInfo
info
    Config
-> String
-> TargetInfo
-> Either [CoreBind] [DiffCheck]
-> IO (Output Doc)
liquidQueries Config
cfg String
tgt TargetInfo
info Either [CoreBind] [DiffCheck]
edcs
  where 
    cfg :: Config
cfg  = TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info
    tgt :: String
tgt  = TargetSrc -> String
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    cbs' :: [CoreBind]
cbs' = TargetSrc -> [CoreBind]
giCbs (TargetInfo -> TargetSrc
giSrc TargetInfo
info)

newPrune :: Config -> [CoreBind] -> FilePath -> TargetInfo -> IO (Either [CoreBind] [DC.DiffCheck])
newPrune :: Config
-> [CoreBind]
-> String
-> TargetInfo
-> IO (Either [CoreBind] [DiffCheck])
newPrune Config
cfg [CoreBind]
cbs String
tgt TargetInfo
info
  | Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs) = Either [CoreBind] [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CoreBind] [DiffCheck]
 -> IO (Either [CoreBind] [DiffCheck]))
-> ([DiffCheck] -> Either [CoreBind] [DiffCheck])
-> [DiffCheck]
-> IO (Either [CoreBind] [DiffCheck])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DiffCheck] -> Either [CoreBind] [DiffCheck]
forall a b. b -> Either a b
Right ([DiffCheck] -> IO (Either [CoreBind] [DiffCheck]))
-> [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall a b. (a -> b) -> a -> b
$ [[CoreBind] -> TargetSpec -> [Var] -> DiffCheck
DC.thin [CoreBind]
cbs TargetSpec
sp [Var]
vs]
  | Config -> Bool
timeBinds Config
cfg = Either [CoreBind] [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CoreBind] [DiffCheck]
 -> IO (Either [CoreBind] [DiffCheck]))
-> ([DiffCheck] -> Either [CoreBind] [DiffCheck])
-> [DiffCheck]
-> IO (Either [CoreBind] [DiffCheck])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DiffCheck] -> Either [CoreBind] [DiffCheck]
forall a b. b -> Either a b
Right ([DiffCheck] -> IO (Either [CoreBind] [DiffCheck]))
-> [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall a b. (a -> b) -> a -> b
$ [[CoreBind] -> TargetSpec -> [Var] -> DiffCheck
DC.thin [CoreBind]
cbs TargetSpec
sp [Var
v] | Var
v <- [Var]
expVars]
  | Config -> Bool
diffcheck Config
cfg = [CoreBind] -> Maybe DiffCheck -> Either [CoreBind] [DiffCheck]
forall a b. a -> Maybe b -> Either a [b]
maybeEither [CoreBind]
cbs (Maybe DiffCheck -> Either [CoreBind] [DiffCheck])
-> IO (Maybe DiffCheck) -> IO (Either [CoreBind] [DiffCheck])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [CoreBind] -> TargetSpec -> IO (Maybe DiffCheck)
DC.slice String
tgt [CoreBind]
cbs TargetSpec
sp
  | Bool
otherwise     = Either [CoreBind] [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [CoreBind] [DiffCheck]
 -> IO (Either [CoreBind] [DiffCheck]))
-> Either [CoreBind] [DiffCheck]
-> IO (Either [CoreBind] [DiffCheck])
forall a b. (a -> b) -> a -> b
$ [CoreBind] -> Either [CoreBind] [DiffCheck]
forall a b. a -> Either a b
Left (HashSet Var -> [CoreBind] -> [CoreBind]
ignoreCoreBinds HashSet Var
ignores [CoreBind]
cbs)
  where
    ignores :: HashSet Var
ignores       = GhcSpecVars -> HashSet Var
gsIgnoreVars (TargetSpec -> GhcSpecVars
gsVars TargetSpec
sp)
    vs :: [Var]
vs            = GhcSpecVars -> [Var]
gsTgtVars    (TargetSpec -> GhcSpecVars
gsVars TargetSpec
sp)
    sp :: TargetSpec
sp            = TargetInfo -> TargetSpec
giSpec       TargetInfo
info
    expVars :: [Var]
expVars       = TargetSrc -> [Var]
exportedVars (TargetInfo -> TargetSrc
giSrc TargetInfo
info)

exportedVars :: TargetSrc -> [Var]
exportedVars :: TargetSrc -> [Var]
exportedVars TargetSrc
src = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (TargetSrc -> Var -> Bool
isExportedVar TargetSrc
src) (TargetSrc -> [Var]
giDefVars TargetSrc
src)

maybeEither :: a -> Maybe b -> Either a [b]
maybeEither :: a -> Maybe b -> Either a [b]
maybeEither a
d Maybe b
Nothing  = a -> Either a [b]
forall a b. a -> Either a b
Left a
d
maybeEither a
_ (Just b
x) = [b] -> Either a [b]
forall a b. b -> Either a b
Right [b
x]

liquidQueries :: Config -> FilePath -> TargetInfo -> Either [CoreBind] [DC.DiffCheck] -> IO (Output Doc)
liquidQueries :: Config
-> String
-> TargetInfo
-> Either [CoreBind] [DiffCheck]
-> IO (Output Doc)
liquidQueries Config
cfg String
tgt TargetInfo
info (Left [CoreBind]
cbs')
  = Config
-> String
-> TargetInfo
-> Either [CoreBind] DiffCheck
-> IO (Output Doc)
liquidQuery Config
cfg String
tgt TargetInfo
info ([CoreBind] -> Either [CoreBind] DiffCheck
forall a b. a -> Either a b
Left [CoreBind]
cbs')
liquidQueries Config
cfg String
tgt TargetInfo
info (Right [DiffCheck]
dcs)
  = [Output Doc] -> Output Doc
forall a. Monoid a => [a] -> a
mconcat ([Output Doc] -> Output Doc) -> IO [Output Doc] -> IO (Output Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DiffCheck -> IO (Output Doc)) -> [DiffCheck] -> IO [Output Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Config
-> String
-> TargetInfo
-> Either [CoreBind] DiffCheck
-> IO (Output Doc)
liquidQuery Config
cfg String
tgt TargetInfo
info (Either [CoreBind] DiffCheck -> IO (Output Doc))
-> (DiffCheck -> Either [CoreBind] DiffCheck)
-> DiffCheck
-> IO (Output Doc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffCheck -> Either [CoreBind] DiffCheck
forall a b. b -> Either a b
Right) [DiffCheck]
dcs

liquidQuery   :: Config -> FilePath -> TargetInfo -> Either [CoreBind] DC.DiffCheck -> IO (Output Doc)
liquidQuery :: Config
-> String
-> TargetInfo
-> Either [CoreBind] DiffCheck
-> IO (Output Doc)
liquidQuery Config
cfg String
tgt TargetInfo
info Either [CoreBind] DiffCheck
edc = do
  let names :: Maybe [String]
names   = ([CoreBind] -> Maybe [String])
-> (DiffCheck -> Maybe [String])
-> Either [CoreBind] DiffCheck
-> Maybe [String]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe [String] -> [CoreBind] -> Maybe [String]
forall a b. a -> b -> a
const Maybe [String]
forall a. Maybe a
Nothing) ([String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String])
-> (DiffCheck -> [String]) -> DiffCheck -> Maybe [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> String) -> [Var] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var -> String
forall a. Show a => a -> String
show ([Var] -> [String])
-> (DiffCheck -> [Var]) -> DiffCheck -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffCheck -> [Var]
DC.checkedVars)   Either [CoreBind] DiffCheck
edc
  let oldOut :: Output Doc
oldOut  = ([CoreBind] -> Output Doc)
-> (DiffCheck -> Output Doc)
-> Either [CoreBind] DiffCheck
-> Output Doc
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Output Doc -> [CoreBind] -> Output Doc
forall a b. a -> b -> a
const Output Doc
forall a. Monoid a => a
mempty)  DiffCheck -> Output Doc
DC.oldOutput                         Either [CoreBind] DiffCheck
edc
  let info1 :: TargetInfo
info1   = ([CoreBind] -> TargetInfo)
-> (DiffCheck -> TargetInfo)
-> Either [CoreBind] DiffCheck
-> TargetInfo
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (TargetInfo -> [CoreBind] -> TargetInfo
forall a b. a -> b -> a
const TargetInfo
info)    (\DiffCheck
z -> TargetInfo
info {giSpec :: TargetSpec
giSpec = DiffCheck -> TargetSpec
DC.newSpec DiffCheck
z}) Either [CoreBind] DiffCheck
edc
  let cbs'' :: [CoreBind]
cbs''   = ([CoreBind] -> [CoreBind])
-> (DiffCheck -> [CoreBind])
-> Either [CoreBind] DiffCheck
-> [CoreBind]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [CoreBind] -> [CoreBind]
forall a. a -> a
id              DiffCheck -> [CoreBind]
DC.newBinds                          Either [CoreBind] DiffCheck
edc
  let info2 :: TargetInfo
info2   = TargetInfo
info1 { giSrc :: TargetSrc
giSrc = (TargetInfo -> TargetSrc
giSrc TargetInfo
info1) {giCbs :: [CoreBind]
giCbs = [CoreBind]
cbs''}}
  let info3 :: TargetInfo
info3   = TargetInfo -> TargetInfo
updTargetInfoTermVars TargetInfo
info2 
  let cgi :: CGInfo
cgi     = {-# SCC "generateConstraints" #-} TargetInfo -> CGInfo
generateConstraints (TargetInfo -> CGInfo) -> TargetInfo -> CGInfo
forall a b. (a -> b) -> a -> b
$! TargetInfo
info3 
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
False (CGInfo -> IO ()
dumpCs CGInfo
cgi)
  -- whenLoud $ mapM_ putStrLn [ "****************** CGInfo ********************"
                            -- , render (pprint cgi)                            ]
  Output Doc
out        <- Maybe [String] -> IO (Output Doc) -> IO (Output Doc)
forall msg a. Show msg => Maybe msg -> IO a -> IO a
timedAction Maybe [String]
names (IO (Output Doc) -> IO (Output Doc))
-> IO (Output Doc) -> IO (Output Doc)
forall a b. (a -> b) -> a -> b
$ Config
-> String
-> CGInfo
-> TargetInfo
-> Maybe [String]
-> IO (Output Doc)
solveCs Config
cfg String
tgt CGInfo
cgi TargetInfo
info3 Maybe [String]
names
  Output Doc -> IO (Output Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return      (Output Doc -> IO (Output Doc)) -> Output Doc -> IO (Output Doc)
forall a b. (a -> b) -> a -> b
$ [Output Doc] -> Output Doc
forall a. Monoid a => [a] -> a
mconcat [Output Doc
oldOut, Output Doc
out]

updTargetInfoTermVars    :: TargetInfo -> TargetInfo 
updTargetInfoTermVars :: TargetInfo -> TargetInfo
updTargetInfoTermVars TargetInfo
i  = TargetInfo -> [Var] -> TargetInfo
updInfo TargetInfo
i  (TargetInfo -> [Var]
ST.terminationVars TargetInfo
i) 
  where 
    updInfo :: TargetInfo -> [Var] -> TargetInfo
updInfo   TargetInfo
info [Var]
vs = TargetInfo
info { giSpec :: TargetSpec
giSpec = TargetSpec -> [Var] -> TargetSpec
updSpec   (TargetInfo -> TargetSpec
giSpec TargetInfo
info) [Var]
vs }
    updSpec :: TargetSpec -> [Var] -> TargetSpec
updSpec   TargetSpec
sp   [Var]
vs = TargetSpec
sp   { gsTerm :: GhcSpecTerm
gsTerm = GhcSpecTerm -> [Var] -> GhcSpecTerm
updSpTerm (TargetSpec -> GhcSpecTerm
gsTerm TargetSpec
sp)   [Var]
vs }
    updSpTerm :: GhcSpecTerm -> [Var] -> GhcSpecTerm
updSpTerm GhcSpecTerm
gsT  [Var]
vs = GhcSpecTerm
gsT  { gsNonStTerm :: HashSet Var
gsNonStTerm = [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var]
vs         } 
      
dumpCs :: CGInfo -> IO ()
dumpCs :: CGInfo -> IO ()
dumpCs CGInfo
cgi = do
  String -> IO ()
putStrLn String
"***************************** SubCs *******************************"
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [SubC] -> Doc
forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [SubC]
hsCs CGInfo
cgi)
  String -> IO ()
putStrLn String
"***************************** FixCs *******************************"
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [FixSubC] -> Doc
forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [FixSubC]
fixCs CGInfo
cgi)
  String -> IO ()
putStrLn String
"***************************** WfCs ********************************"
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [WfC] -> Doc
forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [WfC]
hsWfs CGInfo
cgi)

pprintMany :: (PPrint a) => [a] -> Doc
pprintMany :: [a] -> Doc
pprintMany [a]
xs = [Doc] -> Doc
vcat [ a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
x Doc -> Doc -> Doc
$+$ String -> Doc
text String
" " | a
x <- [a]
xs ]

solveCs :: Config -> FilePath -> CGInfo -> TargetInfo -> Maybe [String] -> IO (Output Doc)
solveCs :: Config
-> String
-> CGInfo
-> TargetInfo
-> Maybe [String]
-> IO (Output Doc)
solveCs Config
cfg String
tgt CGInfo
cgi TargetInfo
info Maybe [String]
names = do
  FInfo Cinfo
finfo            <- TargetInfo -> CGInfo -> IO (FInfo Cinfo)
cgInfoFInfo TargetInfo
info CGInfo
cgi
  let fcfg :: Config
fcfg          = String -> Config -> Config
fixConfig String
tgt Config
cfg
  F.Result FixResult (Integer, Cinfo)
r0 FixSolution
sol GFixSolution
_ <- Solver Cinfo
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve Config
fcfg FInfo Cinfo
finfo
  let failBs :: HashSet (Located Var)
failBs        = GhcSpecTerm -> HashSet (Located Var)
gsFail (GhcSpecTerm -> HashSet (Located Var))
-> GhcSpecTerm -> HashSet (Located Var)
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecTerm
gsTerm (TargetSpec -> GhcSpecTerm) -> TargetSpec -> GhcSpecTerm
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info
  let (FixResult (Integer, Cinfo)
r,[Cinfo]
rf)        = HashSet Var
-> FixResult (Integer, Cinfo)
-> (FixResult (Integer, Cinfo), [Cinfo])
forall a.
HashSet Var
-> FixResult (a, Cinfo) -> (FixResult (a, Cinfo), [Cinfo])
splitFails ((Located Var -> Var) -> HashSet (Located Var) -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map Located Var -> Var
forall a. Located a -> a
val HashSet (Located Var)
failBs) FixResult (Integer, Cinfo)
r0 
  let resErr :: FixResult Error
resErr        = FixSolution -> Error -> Error
forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol (Error -> Error)
-> ((Integer, Cinfo) -> Error) -> (Integer, Cinfo) -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> Error
cinfoError (Cinfo -> Error)
-> ((Integer, Cinfo) -> Cinfo) -> (Integer, Cinfo) -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Cinfo) -> Cinfo
forall a b. (a, b) -> b
snd ((Integer, Cinfo) -> Error)
-> FixResult (Integer, Cinfo) -> FixResult Error
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (Integer, Cinfo)
r
  -- resModel_        <- fmap (e2u cfg sol) <$> getModels info cfg resErr
  let resModel_ :: ErrorResult
resModel_     = Config -> FixSolution -> Error -> UserError
e2u Config
cfg FixSolution
sol (Error -> UserError) -> FixResult Error -> ErrorResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult Error
resErr
  let resModel' :: ErrorResult
resModel'     = ErrorResult
resModel_  ErrorResult -> [UserError] -> ErrorResult
forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> Error -> UserError
e2u Config
cfg FixSolution
sol (Error -> UserError) -> [Error] -> [UserError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [Error]
logErrors CGInfo
cgi)
                                 ErrorResult -> [UserError] -> ErrorResult
forall a. FixResult a -> [a] -> FixResult a
`addErrors` [Located Var] -> [Cinfo] -> [UserError]
makeFailErrors (HashSet (Located Var) -> [Located Var]
forall a. HashSet a -> [a]
S.toList HashSet (Located Var)
failBs) [Cinfo]
rf 
                                 ErrorResult -> [UserError] -> ErrorResult
forall a. FixResult a -> [a] -> FixResult a
`addErrors` [Located Var] -> [CoreBind] -> [UserError]
makeFailUseErrors (HashSet (Located Var) -> [Located Var]
forall a. HashSet a -> [a]
S.toList HashSet (Located Var)
failBs) (TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
  let lErrors :: [Error]
lErrors       = FixSolution -> Error -> Error
forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol (Error -> Error) -> [Error] -> [Error]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [Error]
logErrors CGInfo
cgi
  [Error]
hErrors          <- if (Config -> Bool
typedHoles Config
cfg) 
                        then String -> Config -> CGInfo -> IO [Error]
synthesize String
tgt Config
fcfg (CGInfo
cgi{holesMap :: HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap = FixSolution
-> HoleInfo (CGInfo, CGEnv) SpecType
-> HoleInfo (CGInfo, CGEnv) SpecType
forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol (HoleInfo (CGInfo, CGEnv) SpecType
 -> HoleInfo (CGInfo, CGEnv) SpecType)
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap  CGInfo
cgi}) 
                        else [Error] -> IO [Error]
forall (m :: * -> *) a. Monad m => a -> m a
return [] 
  let resModel :: ErrorResult
resModel      = ErrorResult
resModel' ErrorResult -> [UserError] -> ErrorResult
forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> Error -> UserError
e2u Config
cfg FixSolution
sol (Error -> UserError) -> [Error] -> [UserError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Error]
lErrors [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ [Error]
hErrors)) 
  let out0 :: Output Doc
out0          = Config
-> ErrorResult
-> FixSolution
-> AnnInfo (Annot SpecType)
-> Output Doc
mkOutput Config
cfg ErrorResult
resModel FixSolution
sol (CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
cgi)
  Output Doc -> IO (Output Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return            (Output Doc -> IO (Output Doc)) -> Output Doc -> IO (Output Doc)
forall a b. (a -> b) -> a -> b
$ Output Doc
out0 { o_vars :: Maybe [String]
o_vars    = Maybe [String]
names    }
                           { o_result :: ErrorResult
o_result  = ErrorResult
resModel }


e2u :: Config -> F.FixSolution -> Error -> UserError
e2u :: Config -> FixSolution -> Error -> UserError
e2u Config
cfg FixSolution
s = (SpecType -> Doc) -> Error -> UserError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Error -> UserError) -> (Error -> Error) -> Error -> UserError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> FixSolution -> Error -> Error
tidyError Config
cfg FixSolution
s

-- writeCGI tgt cgi = {-# SCC "ConsWrite" #-} writeFile (extFileName Cgi tgt) str
--   where
--     str          = {-# SCC "PPcgi" #-} showpp cgi


makeFailUseErrors :: [F.Located Var] -> [CoreBind] -> [UserError]
makeFailUseErrors :: [Located Var] -> [CoreBind] -> [UserError]
makeFailUseErrors [Located Var]
fbs [CoreBind]
cbs = [ Located Var -> [Var] -> UserError
forall a a t. (PPrint a, PPrint a) => Located a -> [a] -> TError t
mkError Located Var
x [Var]
bs | Located Var
x <- [Located Var]
fbs
                                          , let bs :: [Var]
bs = Var -> [Var]
clients (Located Var -> Var
forall a. Located a -> a
val Located Var
x)
                                          , Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
bs) ]  
  where 
    mkError :: Located a -> [a] -> TError t
mkError Located a
x [a]
bs = SrcSpan -> Doc -> [Doc] -> TError t
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrFailUsed (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
x) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
x) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
bs)
    clients :: Var -> [Var]
clients Var
x    = ((Var, [Var]) -> Var) -> [(Var, [Var])] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, [Var]) -> Var
forall a b. (a, b) -> a
fst ([(Var, [Var])] -> [Var]) -> [(Var, [Var])] -> [Var]
forall a b. (a -> b) -> a -> b
$ ((Var, [Var]) -> Bool) -> [(Var, [Var])] -> [(Var, [Var])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
x ([Var] -> Bool) -> ((Var, [Var]) -> [Var]) -> (Var, [Var]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, [Var]) -> [Var]
forall a b. (a, b) -> b
snd) [(Var, [Var])]
allClients

    allClients :: [(Var, [Var])]
allClients = (CoreBind -> [(Var, [Var])]) -> [CoreBind] -> [(Var, [Var])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [(Var, [Var])]
go [CoreBind]
cbs 

    go :: CoreBind -> [(Var,[Var])]
    go :: CoreBind -> [(Var, [Var])]
go (NonRec Var
x Expr Var
e) = [(Var
x, Expr Var -> [Var]
forall a. CBVisitable a => a -> [Var]
readVars Expr Var
e)] 
    go (Rec [(Var, Expr Var)]
xes)    = [(Var
x,[Var]
cls) | Var
x <- ((Var, Expr Var) -> Var) -> [(Var, Expr Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Expr Var) -> Var
forall a b. (a, b) -> a
fst [(Var, Expr Var)]
xes] where cls :: [Var]
cls = (Expr Var -> [Var]) -> [Expr Var] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr Var -> [Var]
forall a. CBVisitable a => a -> [Var]
readVars ((Var, Expr Var) -> Expr Var
forall a b. (a, b) -> b
snd ((Var, Expr Var) -> Expr Var) -> [(Var, Expr Var)] -> [Expr Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Expr Var)]
xes)

makeFailErrors :: [F.Located Var] -> [Cinfo] -> [UserError]
makeFailErrors :: [Located Var] -> [Cinfo] -> [UserError]
makeFailErrors [Located Var]
bs [Cinfo]
cis = [ Located Var -> UserError
forall a t. PPrint a => Located a -> TError t
mkError Located Var
x | Located Var
x <- [Located Var]
bs, Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (Located Var -> Var
forall a. Located a -> a
val Located Var
x) [Var]
vs ]  
  where 
    mkError :: Located a -> TError t
mkError  Located a
x = SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrFail (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
x) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
x)
    vs :: [Var]
vs         = [Var
v | Just Var
v <- (Cinfo -> Maybe Var
ci_var (Cinfo -> Maybe Var) -> [Cinfo] -> [Maybe Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cinfo]
cis) ]

splitFails :: S.HashSet Var -> F.FixResult (a, Cinfo) -> (F.FixResult (a, Cinfo),  [Cinfo])
splitFails :: HashSet Var
-> FixResult (a, Cinfo) -> (FixResult (a, Cinfo), [Cinfo])
splitFails HashSet Var
_ r :: FixResult (a, Cinfo)
r@(F.Crash [(a, Cinfo)]
_ String
_) = (FixResult (a, Cinfo)
r,[Cinfo]
forall a. Monoid a => a
mempty)
splitFails HashSet Var
_ r :: FixResult (a, Cinfo)
r@(F.Safe Stats
_)    = (FixResult (a, Cinfo)
r,[Cinfo]
forall a. Monoid a => a
mempty)
splitFails HashSet Var
fs (F.Unsafe Stats
s [(a, Cinfo)]
xs)  = ([(a, Cinfo)] -> FixResult (a, Cinfo)
forall a. [a] -> FixResult a
mkRes [(a, Cinfo)]
r, (a, Cinfo) -> Cinfo
forall a b. (a, b) -> b
snd ((a, Cinfo) -> Cinfo) -> [(a, Cinfo)] -> [Cinfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Cinfo)]
rfails)
  where 
    ([(a, Cinfo)]
rfails,[(a, Cinfo)]
r) = ((a, Cinfo) -> Bool)
-> [(a, Cinfo)] -> ([(a, Cinfo)], [(a, Cinfo)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Bool -> (Var -> Bool) -> Maybe Var -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Bool
False (Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
fs) (Maybe Var -> Bool)
-> ((a, Cinfo) -> Maybe Var) -> (a, Cinfo) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> Maybe Var
ci_var (Cinfo -> Maybe Var)
-> ((a, Cinfo) -> Cinfo) -> (a, Cinfo) -> Maybe Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Cinfo) -> Cinfo
forall a b. (a, b) -> b
snd) [(a, Cinfo)]
xs 
    mkRes :: [a] -> FixResult a
mkRes [] = Stats -> FixResult a
forall a. Stats -> FixResult a
F.Safe Stats
s
    mkRes [a]
ys = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
F.Unsafe Stats
s [a]
ys