liquidhaskell-0.8.6.0: src/Language/Haskell/Liquid/Liquid.hs
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--diff" @-}
module Language.Haskell.Liquid.Liquid (
-- * Executable command
liquid
-- * Single query
, runLiquid
-- * Ghci State
, MbEnv
-- * Liquid Constraint Generation
, liquidConstraints
) 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)
import qualified Control.Exception as Ex
-- import qualified Language.Fixpoint.Types.Config as FC
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.Types.RefType (applySolution)
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.Model
-- import Language.Haskell.Liquid.Transforms.Rec
import Language.Haskell.Liquid.UX.Annotate (mkOutput)
import qualified Language.Haskell.Liquid.Termination.Structural as ST
type MbEnv = Maybe HscEnv
--------------------------------------------------------------------------------
liquid :: [String] -> IO b
--------------------------------------------------------------------------------
liquid args = do
cfg <- getOpts args
(ec, _) <- runLiquid Nothing cfg
exitWith ec
--------------------------------------------------------------------------------
liquidConstraints :: Config -> IO (Either [CGInfo] ExitCode)
--------------------------------------------------------------------------------
liquidConstraints cfg = do
z <- actOrDie $ second Just <$> getGhcInfos Nothing cfg (files cfg)
case z of
Left e -> do
exitWithResult cfg (files cfg) $ mempty { o_result = e }
return $ Right $ resultExit e
Right (gs, _) ->
return $ Left $ map generateConstraints gs
--------------------------------------------------------------------------------
runLiquid :: MbEnv -> Config -> IO (ExitCode, MbEnv)
--------------------------------------------------------------------------------
runLiquid mE cfg = do
reals <- realTargets mE cfg (files cfg)
putStrLn $ showpp (text "Targets:" <+> vcat (text <$> reals))
checkTargets cfg mE reals
checkTargets :: Config -> MbEnv -> [FilePath] -> IO (ExitCode, MbEnv)
checkTargets cfg = go
where
go env [] = return (ExitSuccess, env)
go env (f:fs) = do colorPhaseLn Loud ("[Checking: " ++ f ++ "]") ""
(ec, env') <- runLiquidTargets env cfg [f]
case ec of
ExitSuccess -> go env' fs
_ -> return (ec, 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 mE cfg targetFiles = do
z <- actOrDie $ second Just <$> getGhcInfos mE cfg targetFiles
case z of
Left e -> do
exitWithResult cfg targetFiles $ mempty { o_result = e }
return (resultExit e, mE)
Right (gs, mE') -> do
d <- checkMany cfg mempty gs
return (ec d, mE')
where
ec = resultExit . o_result
--------------------------------------------------------------------------------
checkMany :: Config -> Output Doc -> [GhcInfo] -> IO (Output Doc)
--------------------------------------------------------------------------------
checkMany cfg d (g:gs) = do
d' <- checkOne cfg g
checkMany cfg (d `mappend` d') gs
checkMany _ d [] =
return d
--------------------------------------------------------------------------------
checkOne :: Config -> GhcInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
checkOne cfg g = do
z <- actOrDie $ liquidOne g
case z of
Left e -> exitWithResult cfg [giTarget (giSrc g)] $ mempty { o_result = e }
Right r -> return r
actOrDie :: IO a -> IO (Either ErrorResult a)
actOrDie act =
(Right <$> act)
`Ex.catch` (\(e :: SourceError) -> handle e)
`Ex.catch` (\(e :: Error) -> handle e)
`Ex.catch` (\(e :: UserError) -> handle e)
`Ex.catch` (\(e :: [Error]) -> handle e)
handle :: (Result a) => a -> IO (Either ErrorResult b)
handle = return . Left . result
--------------------------------------------------------------------------------
liquidOne :: GhcInfo -> IO (Output Doc)
--------------------------------------------------------------------------------
liquidOne info
| compileSpec cfg = do
donePhase Loud "Only compiling specifications [skipping verification]"
exitWithResult cfg [tgt] (mempty { o_result = F.Safe })
| otherwise = do
whenNormal $ donePhase Loud "Extracted Core using GHC"
-- whenLoud $ do putStrLn $ showpp info
-- putStrLn "*************** Original CoreBinds ***************************"
-- putStrLn $ render $ pprintCBs (cbs info)
whenNormal $ donePhase Loud "Transformed Core"
whenLoud $ do donePhase Loud "transformRecExpr"
putStrLn "*************** Transform Rec Expr CoreBinds *****************"
putStrLn $ showCBs (untidyCore cfg) cbs'
-- putStrLn $ render $ pprintCBs cbs'
-- putStrLn $ showPpr cbs'
edcs <- newPrune cfg cbs' tgt info
out' <- liquidQueries cfg tgt info edcs
DC.saveResult tgt out'
exitWithResult cfg [tgt] out'
where
cfg = getConfig info
tgt = giTarget (giSrc info)
cbs' = giCbs (giSrc info)
newPrune :: Config -> [CoreBind] -> FilePath -> GhcInfo -> IO (Either [CoreBind] [DC.DiffCheck])
newPrune cfg cbs tgt info
| not (null vs) = return . Right $ [DC.thin cbs sp vs]
| timeBinds cfg = return . Right $ [DC.thin cbs sp [v] | v <- expVars]
| diffcheck cfg = maybeEither cbs <$> DC.slice tgt cbs sp
| otherwise = return $ Left (ignoreCoreBinds ignores cbs)
where
ignores = gsIgnoreVars (gsVars sp)
vs = gsTgtVars (gsVars sp)
sp = giSpec info
expVars = exportedVars (giSrc info)
exportedVars :: GhcSrc -> [Var]
exportedVars src = filter (isExportedVar src) (giDefVars src)
maybeEither :: a -> Maybe b -> Either a [b]
maybeEither d Nothing = Left d
maybeEither _ (Just x) = Right [x]
liquidQueries :: Config -> FilePath -> GhcInfo -> Either [CoreBind] [DC.DiffCheck] -> IO (Output Doc)
liquidQueries cfg tgt info (Left cbs')
= liquidQuery cfg tgt info (Left cbs')
liquidQueries cfg tgt info (Right dcs)
= mconcat <$> mapM (liquidQuery cfg tgt info . Right) dcs
liquidQuery :: Config -> FilePath -> GhcInfo -> Either [CoreBind] DC.DiffCheck -> IO (Output Doc)
liquidQuery cfg tgt info edc = do
let names = either (const Nothing) (Just . map show . DC.checkedVars) edc
let oldOut = either (const mempty) DC.oldOutput edc
let info1 = either (const info) (\z -> info {giSpec = DC.newSpec z}) edc
let cbs'' = either id DC.newBinds edc
let info2 = info1 { giSrc = (giSrc info1) {giCbs = cbs''}}
let info3 = updGhcInfoTermVars info2
let cgi = {-# SCC "generateConstraints" #-} generateConstraints $! info3
when False (dumpCs cgi)
-- whenLoud $ mapM_ putStrLn [ "****************** CGInfo ********************"
-- , render (pprint cgi) ]
out <- timedAction names $ solveCs cfg tgt cgi info3 names
return $ mconcat [oldOut, out]
updGhcInfoTermVars :: GhcInfo -> GhcInfo
updGhcInfoTermVars i = updInfo i (ST.terminationVars i)
where
updInfo info vs = info { giSpec = updSpec (giSpec info) vs }
updSpec sp vs = sp { gsTerm = updSpTerm (gsTerm sp) vs }
updSpTerm gsT vs = gsT { gsNonStTerm = S.fromList vs }
dumpCs :: CGInfo -> IO ()
dumpCs cgi = do
putStrLn "***************************** SubCs *******************************"
putStrLn $ render $ pprintMany (hsCs cgi)
putStrLn "***************************** FixCs *******************************"
putStrLn $ render $ pprintMany (fixCs cgi)
putStrLn "***************************** WfCs ********************************"
putStrLn $ render $ pprintMany (hsWfs cgi)
pprintMany :: (PPrint a) => [a] -> Doc
pprintMany xs = vcat [ F.pprint x $+$ text " " | x <- xs ]
instance Show Cinfo where
show = show . F.toFix
solveCs :: Config -> FilePath -> CGInfo -> GhcInfo -> Maybe [String] -> IO (Output Doc)
solveCs cfg tgt cgi info names = do
finfo <- cgInfoFInfo info cgi
F.Result r sol _ <- solve (fixConfig tgt cfg) finfo
let resErr = applySolution sol . cinfoError . snd <$> r
-- resModel_ <- fmap (e2u cfg sol) <$> getModels info cfg resErr
let resModel_ = e2u cfg sol <$> resErr
let resModel = resModel_ `addErrors` (e2u cfg sol <$> logErrors cgi)
let out0 = mkOutput cfg resModel sol (annotMap cgi)
return $ out0 { o_vars = names }
{ o_result = resModel }
e2u :: Config -> F.FixSolution -> Error -> UserError
e2u cfg s = fmap F.pprint . tidyError cfg s
-- writeCGI tgt cgi = {-# SCC "ConsWrite" #-} writeFile (extFileName Cgi tgt) str
-- where
-- str = {-# SCC "PPcgi" #-} showpp cgi