diff --git a/liquid-platform.cabal b/liquid-platform.cabal --- a/liquid-platform.cabal +++ b/liquid-platform.cabal @@ -1,6 +1,6 @@ cabal-version: 1.22 name: liquid-platform -version: 0.9.0.2 +version: 0.9.2.5 synopsis: A battery-included platform for LiquidHaskell description: A battery-included platform for LiquidHaskell. license: BSD3 @@ -25,38 +25,15 @@ buildable: False else buildable: True - build-depends: liquid-base >= 4.15.1.0 && < 5 - , liquid-containers >= 0.6.4.1 && < 0.7 - , liquid-prelude >= 0.9.0.2 - , liquid-vector >= 0.12.3.1 && < 0.13 - , liquid-bytestring >= 0.10.12.1 && < 0.11 - , liquidhaskell >= 0.9.0.2 + build-depends: base >= 4.15.1.0 && < 5 + , containers >= 0.6.4.1 && < 0.7 + , liquid-prelude >= 0.9.2.5 + , liquid-vector >= 0.12.3.1.2 + , liquidhaskell >= 0.9.2.5 + , liquidhaskell-boot >= 0.9.2.5 , filepath , process >= 1.6.0.0 && < 1.7 , cmdargs >= 0.10 && < 0.11 if flag(devel) ghc-options: -Werror - - -executable gradual - main-is: src/Gradual.hs - build-depends: base >= 4.15.1.0 && < 5 - , cmdargs - , hscolour - , liquid-fixpoint >= 0.9.0.2 - , liquidhaskell >= 0.9.0.2 - default-language: Haskell2010 - buildable: False - ghc-options: -W -threaded - - if flag(devel) - ghc-options: -Werror - - -executable target - main-is: src/Target.hs - build-depends: base >= 4.8.1.0 && < 5, hint, liquidhaskell >= 0.8.10.2 - default-language: Haskell2010 - buildable: False - diff --git a/src/Gradual.hs b/src/Gradual.hs deleted file mode 100644 --- a/src/Gradual.hs +++ /dev/null @@ -1,86 +0,0 @@ -{-# LANGUAGE TupleSections #-} - --- module Main where - -import Language.Haskell.Liquid.Liquid (liquidConstraints) - -import Language.Haskell.Liquid.Types (GhcInfo(..), Cinfo) -import Language.Haskell.Liquid.Constraint.Types (CGInfo(..)) -- , FixWfC, SubC(..), CGEnv(..)) -import Language.Haskell.Liquid.UX.Config (Config(..)) -import Language.Haskell.Liquid.UX.CmdLine (getOpts) -import Language.Haskell.Liquid.Constraint.ToFixpoint (cgInfoFInfo, fixConfig) - -import qualified Language.Fixpoint.Types as F -import qualified Language.Fixpoint.Types.Config as F -import Language.Fixpoint.Solver (simplifyFInfo) -import Language.Fixpoint.Solver.Solve (solve) -import qualified Language.Fixpoint.Solver.GradualSolution as GS -import Language.Fixpoint.Misc (mapSnd) -import Language.Fixpoint.Graph.Partition (partition') - -import System.Exit (exitWith, exitSuccess, exitFailure) -import System.Environment (getArgs) -import System.Console.CmdArgs.Verbosity -import Control.Monad (when) - -import qualified Data.List as L - -import Gradual.Concretize -import Gradual.Types -import Gradual.Misc (mapSndM, mapMWithLog) -import Gradual.Uniquify -import Gradual.Refinements -import Gradual.PrettyPrinting -import qualified Gradual.GUI as GUI -import qualified Gradual.Trivial as T - -main :: IO a -main = do - cfg <- getArgs >>= getOpts - css <- quietly $ liquidConstraints (cfg{gradual=True}) - case css of - Left cgis -> mapM (runGradual (cfg{gradual=True})) cgis >> exitSuccess - Right e -> exitWith e - - -runGradual :: Config -> CGInfo -> IO [(GSub F.GWInfo,F.Result (Integer, Cinfo))] -runGradual cfg cgi = do - let fname = target (ghcI cgi) - let fcfg = fixConfig fname cfg - finfo <- quietly $ cgInfoFInfo (ghcI cgi) cgi - sinfo <- (uniquify . T.simplify) <$> (quietly $ simplifyFInfo fcfg finfo) - let (gsis, sis) = L.partition F.isGradual $ partition' Nothing (snd sinfo) - let gcfg = (makeGConfig cfg) {pNumber = length gsis} - sol <- mconcat <$> (quietly $ mapM (solve fcfg) sis) - let gcfgs = setPId gcfg <$> [1..(length gsis)] - when (not $ F.isSafe sol) $ do - putStrLn "The static part cannot be satisfied: UNSAFE" - exitFailure - whenLoud $ putStrLn ("\nNumber of Gradual Partitions : " ++ show (length gsis) ++"\n") - solss <- mapMWithLog "Running Partition" (uncurry $ solveSInfo fcfg) (zip gcfgs gsis) - GUI.render gcfg (fst sinfo) solss - exitSuccess - - - -solveSInfo :: F.Config -> GConfig -> F.SInfo Cinfo -> IO [GSub F.GWInfo] -solveSInfo fcfg gcfg sinfo = do - gmap <- makeGMap gcfg fcfg sinfo $ GS.init fcfg sinfo - let allgs = concretize gmap sinfo - putStrLn ("Total number of concretizations: " ++ show (length $ map snd allgs)) - res <- quietly $ mapM (mapSndM (solve fcfg)) allgs - case filter (F.isSafe . snd) res of - (x:xs) -> do putStrLn ( "["++ show (1 + length xs) ++ "/" ++ (show $ length res) ++ "] Solutions Found!" ++ if length xs > 0 then " e.g.," else "") - putStrLn (pretty $ (map (mapSnd snd) $ fromGSub $ fst x)) - return (fst <$> (x:xs)) - _ -> do putStrLn ("[0/" ++ (show $ length res) ++ "] Solutions. UNSAFE!\n") - whenLoud $ putStrLn ("UNSAFE PARTITION: " ++ show sinfo) - return [mempty] - -quietly :: IO a -> IO a -quietly act = do - vb <- getVerbosity - setVerbosity Quiet - r <- act - setVerbosity vb - return r diff --git a/src/Liquid.hs b/src/Liquid.hs --- a/src/Liquid.hs +++ b/src/Liquid.hs @@ -86,17 +86,6 @@ , "-no-link" , "-fplugin=LiquidHaskell" , "-plugin-package", "liquidhaskell" - , "-package", "liquid-ghc-prim" - , "-package", "liquid-base" - , "-package", "liquid-containers" - , "-package", "liquid-prelude" - , "-package", "liquid-vector" - , "-package", "liquid-bytestring" - , "-hide-package", "ghc-prim" - , "-hide-package", "base" - , "-hide-package", "containers" - , "-hide-package", "vector" - , "-hide-package", "bytestring" , "-fplugin-opt=LiquidHaskell:--normal" -- normal logging. ] <> map (mappend "-fplugin-opt=LiquidHaskell:") liquidArgs diff --git a/src/Target.hs b/src/Target.hs deleted file mode 100644 --- a/src/Target.hs +++ /dev/null @@ -1,29 +0,0 @@ -{-# LANGUAGE LambdaCase #-} --- module Main where - -import Language.Haskell.Interpreter -import System.Environment -import System.Exit -import System.IO -import Test.Target -import Text.Printf - -main :: IO () -main = do - [src, binder] <- getArgs - r <- runInterpreter $ do - loadModules [src] - mods <- getLoadedModules - -- liftIO $ print mods - setImportsQ $ map (\m -> (m,Nothing)) mods - ++ [("Test.Target", Nothing), ("Prelude", Nothing)] - set [languageExtensions := [TemplateHaskell]] - let expr = printf "$(targetResultTH '%s \"%s\")" binder src - -- liftIO $ putStrLn expr - interpret expr (as :: IO Result) - case r of - Left e -> hPrint stderr e >> exitWith (ExitFailure 2) - Right x -> x >>= \case - Errored e -> hPutStrLn stderr e >> exitWith (ExitFailure 2) - Failed s -> printf "Found counter-example: %s\n" s >> exitWith (ExitFailure 1) - Passed n -> printf "OK! Passed %d tests.\n" n >> exitSuccess