liquid-platform 0.9.0.2 → 0.9.2.5
raw patch · 4 files changed
+7/−156 lines, 4 filesdep +containersdep +liquidhaskell-bootdep −hintdep −hscolourdep −liquid-basedep ~basedep ~cmdargsdep ~liquid-prelude
Dependencies added: containers, liquidhaskell-boot
Dependencies removed: hint, hscolour, liquid-base, liquid-bytestring, liquid-containers, liquid-fixpoint
Dependency ranges changed: base, cmdargs, liquid-prelude, liquid-vector, liquidhaskell
Files
- liquid-platform.cabal +7/−30
- src/Gradual.hs +0/−86
- src/Liquid.hs +0/−11
- src/Target.hs +0/−29
liquid-platform.cabal view
@@ -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-
− src/Gradual.hs
@@ -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
src/Liquid.hs view
@@ -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
− src/Target.hs
@@ -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