{-# LANGUAGE ScopedTypeVariables #-}

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

module Language.Haskell.Liquid.Liquid (
   -- * Checking a single module
    checkTargetInfo
  ) where

import           Prelude hiding (error)
import           Data.Bifunctor
import qualified Data.HashSet as S 
import           Text.PrettyPrint.HughesPJ
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 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.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.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
import           Liquid.GHC.API as GHC hiding (text, vcat, ($+$), (<+>))

--------------------------------------------------------------------------------
checkTargetInfo :: TargetInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
checkTargetInfo :: TargetInfo -> IO (Output Doc)
checkTargetInfo TargetInfo
info = do
  Output Doc
out <- IO (Output Doc)
check
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Config -> Bool
compileSpec Config
cfg) forall a b. (a -> b) -> a -> b
$ String -> Output Doc -> IO ()
DC.saveResult String
tgt Output Doc
out
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Output Doc
out
  where
    check :: IO (Output Doc)
    check :: IO (Output Doc)
check
      | Config -> Bool
compileSpec Config
cfg = do
        -- donePhase Loud "Only compiling specifications [skipping verification]"
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty { o_result :: ErrorResult
o_result = forall a. Stats -> FixResult a
F.Safe forall a. Monoid a => a
mempty }
      | Bool
otherwise = do
        IO () -> IO ()
whenNormal 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 forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Loud String
"Transformed Core"
        IO () -> IO ()
whenLoud  forall a b. (a -> b) -> a -> b
$ do Moods -> String -> IO ()
donePhase Moods
Loud String
"transformRecExpr-1773-hoho"
                       String -> IO ()
putStrLn String
"*************** Transform Rec Expr CoreBinds *****************"
                       String -> IO ()
putStrLn 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

    cfg :: Config
    cfg :: Config
cfg  = forall t. HasConfig t => t -> Config
getConfig TargetInfo
info

    tgt :: FilePath
    tgt :: String
tgt  = TargetSrc -> String
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
info)

    cbs' :: [CoreBind]
    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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs) = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [[CoreBind] -> TargetSpec -> [Var] -> DiffCheck
DC.thin [CoreBind]
cbs TargetSpec
sp [Var]
vs]
  | Config -> Bool
timeBinds Config
cfg = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right 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 = forall a b. a -> Maybe b -> Either a [b]
maybeEither [CoreBind]
cbs 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     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = 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 :: forall a b. a -> Maybe b -> Either a [b]
maybeEither a
d Maybe b
Nothing  = forall a b. a -> Either a b
Left a
d
maybeEither a
_ (Just b
x) = 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 (forall a b. a -> Either a b
Left [CoreBind]
cbs')
liquidQueries Config
cfg String
tgt TargetInfo
info (Right [DiffCheck]
dcs)
  = forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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   = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffCheck -> [Var]
DC.checkedVars)   Either [CoreBind] DiffCheck
edc
  let oldOut :: Output Doc
oldOut  = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty)  DiffCheck -> Output Doc
DC.oldOutput                         Either [CoreBind] DiffCheck
edc
  let info1 :: TargetInfo
info1   = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (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''   = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either 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 forall a b. (a -> b) -> a -> b
$! TargetInfo
info3 
  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        <- forall msg a. Show msg => Maybe msg -> IO a -> IO a
timedAction Maybe [String]
names 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
  forall (m :: * -> *) a. Monad m => a -> m a
return      forall a b. (a -> b) -> a -> b
$ 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 = 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 forall a b. (a -> b) -> a -> b
$ Doc -> String
render forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [SubC]
hsCs CGInfo
cgi)
  String -> IO ()
putStrLn String
"***************************** FixCs *******************************"
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Doc -> String
render forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [FixSubC]
fixCs CGInfo
cgi)
  String -> IO ()
putStrLn String
"***************************** WfCs ********************************"
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Doc -> String
render forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [a] -> Doc
pprintMany (CGInfo -> [WfC]
hsWfs CGInfo
cgi)

pprintMany :: (PPrint a) => [a] -> Doc
pprintMany :: forall a. PPrint a => [a] -> Doc
pprintMany [a]
xs = [Doc] -> Doc
vcat [ 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 {resStatus :: forall a. Result a -> FixResult a
resStatus=FixResult (Integer, Cinfo)
r0, resSolution :: forall a. Result a -> FixSolution
resSolution=FixSolution
sol} <- forall a.
(PPrint 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 forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecTerm
gsTerm forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info
  let (FixResult (Integer, Cinfo)
r,[Cinfo]
rf)        = forall a.
HashSet Var
-> FixResult (a, Cinfo) -> (FixResult (a, Cinfo), [Cinfo])
splitFails (forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map forall a. Located a -> a
val HashSet (Located Var)
failBs) FixResult (Integer, Cinfo)
r0 
  let resErr :: FixResult (Integer, TError SpecType)
resErr        = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> TError SpecType
cinfoError) 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 -> (Integer, TError SpecType) -> UserError
cidE2u Config
cfg FixSolution
sol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (Integer, TError SpecType)
resErr
  let resModel' :: ErrorResult
resModel'     = ErrorResult
resModel_  forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> TError SpecType -> UserError
e2u Config
cfg FixSolution
sol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [TError SpecType]
logErrors CGInfo
cgi)
                                 forall a. FixResult a -> [a] -> FixResult a
`addErrors` [Located Var] -> [Cinfo] -> [UserError]
makeFailErrors (forall a. HashSet a -> [a]
S.toList HashSet (Located Var)
failBs) [Cinfo]
rf 
                                 forall a. FixResult a -> [a] -> FixResult a
`addErrors` [Located Var] -> [CoreBind] -> [UserError]
makeFailUseErrors (forall a. HashSet a -> [a]
S.toList HashSet (Located Var)
failBs) (TargetSrc -> [CoreBind]
giCbs forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
  let lErrors :: [TError SpecType]
lErrors       = forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [TError SpecType]
logErrors CGInfo
cgi
  let resModel :: ErrorResult
resModel      = ErrorResult
resModel' forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> TError SpecType -> UserError
e2u Config
cfg FixSolution
sol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TError SpecType]
lErrors)
  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)
  forall (m :: * -> *) a. Monad m => a -> m a
return            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 -> TError SpecType -> UserError
e2u Config
cfg FixSolution
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. PPrint a => a -> Doc
F.pprint forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> FixSolution -> TError SpecType -> TError SpecType
tidyError Config
cfg FixSolution
s

cidE2u :: Config -> F.FixSolution -> (Integer, Error) -> UserError
cidE2u :: Config -> FixSolution -> (Integer, TError SpecType) -> UserError
cidE2u Config
cfg FixSolution
s (Integer
subcId, TError SpecType
e) =
  let e' :: TError SpecType
e' = forall {t}. TError t -> TError t
attachSubcId TError SpecType
e
   in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. PPrint a => a -> Doc
F.pprint (Config -> FixSolution -> TError SpecType -> TError SpecType
tidyError Config
cfg FixSolution
s TError SpecType
e')
  where
    attachSubcId :: TError t -> TError t
attachSubcId es :: TError t
es@ErrSubType{}      = TError t
es { cid :: Maybe Integer
cid = forall a. a -> Maybe a
Just Integer
subcId }
    attachSubcId es :: TError t
es@ErrSubTypeModel{} = TError t
es { cid :: Maybe Integer
cid = forall a. a -> Maybe a
Just Integer
subcId }
    attachSubcId TError t
es = TError t
es

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

    allClients :: [(Var, [Var])]
allClients = 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, forall a. CBVisitable a => a -> [Var]
readVars Expr Var
e)] 
    go (Rec [(Var, Expr Var)]
xes)    = [(Var
x,[Var]
cls) | Var
x <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Var, Expr Var)]
xes] where cls :: [Var]
cls = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. CBVisitable a => a -> [Var]
readVars (forall a b. (a, b) -> b
snd 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 = [ forall {a} {t}. PPrint a => Located a -> TError t
mkError Located Var
x | Located Var
x <- [Located Var]
bs, forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (forall a. Located a -> a
val Located Var
x) [Var]
vs ]  
  where 
    mkError :: Located a -> TError t
mkError  Located a
x = forall t. SrcSpan -> Doc -> TError t
ErrFail (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc Located a
x) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val Located a
x)
    vs :: [Var]
vs         = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Cinfo -> Maybe Var
ci_var [Cinfo]
cis

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