{-# 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           Control.Monad (when)
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 qualified Language.Fixpoint.Misc as F
import           Language.Fixpoint.Solver
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Visitors
import           Language.Haskell.Liquid.UX.Errors
import           Language.Haskell.Liquid.UX.CmdLine
import           Language.Haskell.Liquid.UX.Config
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
  out <- IO (Output Doc)
check
  when (diffcheck cfg && not (compileSpec cfg)) $ DC.saveResult tgt out
  pure out
  where
    check :: IO (Output Doc)
    check :: IO (Output Doc)
check
      | Config -> Bool
compileSpec Config
cfg = do
        -- donePhase Loud "Only compiling specifications [skipping verification]"
        Output Doc -> IO (Output Doc)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Output Doc
forall a. Monoid a => a
mempty { o_result = F.Safe mempty }
      | Bool
otherwise = do
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Verbosity
loggingVerbosity Config
cfg Verbosity -> Verbosity -> Bool
forall a. Eq a => a -> a -> Bool
== Verbosity
Normal) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Moods -> String -> IO ()
F.donePhase Moods
F.Loud String
"Extracted Core using GHC"
          Moods -> String -> IO ()
F.donePhase Moods
F.Loud String
"Transformed Core"
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Verbosity
loggingVerbosity Config
cfg Verbosity -> Verbosity -> Bool
forall a. Eq a => a -> a -> Bool
== Verbosity
Loud) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Moods -> String -> IO ()
F.donePhase Moods
F.Loud String
"transformRecExpr-1773-hoho"
          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'
        edcs <- Config
-> [CoreBind]
-> String
-> TargetInfo
-> IO (Either [CoreBind] [DiffCheck])
newPrune Config
cfg [CoreBind]
cbs' String
tgt TargetInfo
info
        liquidQueries cfg tgt info edcs

    cfg :: Config
    cfg :: Config
cfg  = TargetInfo -> Config
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 ([Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs) = Either [CoreBind] [DiffCheck] -> IO (Either [CoreBind] [DiffCheck])
forall a. a -> IO a
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 a. a -> IO a
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 a. a -> IO a
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 :: forall a b. 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 = DC.newSpec 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 = (giSrc info1) {giCbs = 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)                            ]
  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
  return      $ mconcat [oldOut, 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 = updSpec   (giSpec info) vs }
    updSpec :: TargetSpec -> [Var] -> TargetSpec
updSpec   TargetSpec
sp   [Var]
vs = TargetSpec
sp   { gsTerm = updSpTerm (gsTerm sp)   vs }
    updSpTerm :: GhcSpecTerm -> [Var] -> GhcSpecTerm
updSpTerm GhcSpecTerm
gsT  [Var]
vs = GhcSpecTerm
gsT  { gsNonStTerm = S.fromList 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 :: forall a. PPrint a => [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            <- TargetInfo -> CGInfo -> IO (FInfo Cinfo)
cgInfoFInfo TargetInfo
info CGInfo
cgi
  let fcfg          = String -> Config -> Config
fixConfig String
tgt Config
cfg
  F.Result {resStatus=r0, resSolution=sol} <- solve fcfg finfo
  let 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 (r,rf)        = splitFails (S.map val failBs) r0 
  let resErr        = (Cinfo -> TError SpecType)
-> (Integer, Cinfo) -> (Integer, TError SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (FixSolution -> TError SpecType -> TError SpecType
forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol (TError SpecType -> TError SpecType)
-> (Cinfo -> TError SpecType) -> Cinfo -> TError SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> TError SpecType
cinfoError) ((Integer, Cinfo) -> (Integer, TError SpecType))
-> FixResult (Integer, Cinfo)
-> FixResult (Integer, TError SpecType)
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_     = Config -> FixSolution -> (Integer, TError SpecType) -> UserError
cidE2u Config
cfg FixSolution
sol ((Integer, TError SpecType) -> UserError)
-> FixResult (Integer, TError SpecType) -> FixResult UserError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (Integer, TError SpecType)
resErr
  let resModel'     = FixResult UserError
resModel_  FixResult UserError -> [UserError] -> FixResult UserError
forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> TError SpecType -> UserError
e2u Config
cfg FixSolution
sol (TError SpecType -> UserError) -> [TError SpecType] -> [UserError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [TError SpecType]
logErrors CGInfo
cgi)
                                 FixResult UserError -> [UserError] -> FixResult UserError
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 
                                 FixResult UserError -> [UserError] -> FixResult UserError
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       = FixSolution -> TError SpecType -> TError SpecType
forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution FixSolution
sol (TError SpecType -> TError SpecType)
-> [TError SpecType] -> [TError SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGInfo -> [TError SpecType]
logErrors CGInfo
cgi
  let resModel      = FixResult UserError
resModel' FixResult UserError -> [UserError] -> FixResult UserError
forall a. FixResult a -> [a] -> FixResult a
`addErrors` (Config -> FixSolution -> TError SpecType -> UserError
e2u Config
cfg FixSolution
sol (TError SpecType -> UserError) -> [TError SpecType] -> [UserError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TError SpecType]
lErrors)
  let out0          = Config
-> FixResult UserError
-> FixSolution
-> AnnInfo (Annot SpecType)
-> Output Doc
mkOutput Config
cfg FixResult UserError
resModel FixSolution
sol (CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
cgi)
  return            $ out0 { o_vars    = names    }
                           { o_result  = resModel }


e2u :: Config -> F.FixSolution -> Error -> UserError
e2u :: Config -> FixSolution -> TError SpecType -> UserError
e2u Config
cfg FixSolution
s = (SpecType -> Doc) -> TError SpecType -> UserError
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint (TError SpecType -> UserError)
-> (TError SpecType -> TError SpecType)
-> TError SpecType
-> UserError
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' = TError SpecType -> TError SpecType
forall {t}. TError t -> TError t
attachSubcId TError SpecType
e
   in (SpecType -> Doc) -> TError SpecType -> UserError
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> Doc
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 = Just subcId }
    attachSubcId es :: TError t
es@ErrSubTypeModel{} = TError t
es { cid = Just 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 = [ 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 a. [a] -> 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 a. Eq a => a -> [a] -> 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         = (Cinfo -> Maybe Var) -> [Cinfo] -> [Var]
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,[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