liquid-platform (empty) → 0.8.10.1
raw patch · 5 files changed
+294/−0 lines, 5 filesdep +basedep +cmdargsdep +hint
Dependencies added: base, cmdargs, hint, hscolour, liquid-base, liquid-bytestring, liquid-containers, liquid-fixpoint, liquid-prelude, liquid-vector, liquidhaskell, process
Files
- LICENSE +30/−0
- liquid-platform.cabal +59/−0
- src/Gradual.hs +86/−0
- src/Liquid.hs +90/−0
- src/Target.hs +29/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013-2014, Ranjit Jhala++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Ranjit Jhala nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ liquid-platform.cabal view
@@ -0,0 +1,59 @@+cabal-version: 1.22+name: liquid-platform+version: 0.8.10.1+synopsis: A battery-included platform for LiquidHaskell+description: A battery-included platform for LiquidHaskell.+license: BSD3+license-file: LICENSE+copyright: 2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.+author: Ranjit Jhala, Niki Vazou, Eric Seidel+maintainer: Ranjit Jhala <jhala@cs.ucsd.edu>+category: Language+homepage: https://github.com/ucsd-progsys/liquidhaskell+build-type: Simple++flag devel+ default: False+ manual: True+ description: turn on stricter error reporting for development++executable liquidhaskell+ main-is: src/Liquid.hs+ default-language: Haskell2010+ ghc-options: -W -threaded+ if impl(ghc < 8.10.1)+ buildable: False+ else+ buildable: True+ build-depends: liquid-base >= 4.14.0.0 && < 5+ , liquid-containers >= 0.6.2.1 && < 0.7+ , liquid-prelude >= 0.8.10.1+ , liquid-vector >= 0.12.1.2 && < 0.13+ , liquid-bytestring >= 0.10.0.0 && < 0.11+ , liquidhaskell >= 0.8.10.1+ , 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.8.1.0 && < 5+ , cmdargs+ , hscolour+ , liquid-fixpoint >= 0.7.0.5+ , liquidhaskell >= 0.8.10.1+ 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.1+ default-language: Haskell2010+ buildable: False+
+ src/Gradual.hs view
@@ -0,0 +1,86 @@+{-# 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
@@ -0,0 +1,90 @@+{-# LANGUAGE LambdaCase #-}++{-| Calling LiquidHaskell via the source plugin.+ This executable is a simple wrapper around 'ghc', which gets passed an '-fplugin' option.+-}++import Control.Monad++import System.Environment (lookupEnv, getArgs)+import System.Process+import System.Exit+import Data.Maybe+import Data.Either (partitionEithers)+import Data.Bifunctor+import Data.Functor ((<&>))+import qualified System.Console.CmdArgs.Explicit as CmdArgs+import Data.List (partition, isPrefixOf, (\\))++import Language.Haskell.Liquid.UX.CmdLine (config, printLiquidHaskellBanner, getOpts)++type GhcArg = String+type LiquidArg = String++partitionArgs :: [String] -> ([GhcArg], [LiquidArg])+partitionArgs args = partitionEithers (map parseArg args)+ where+ parseArg :: String -> Either GhcArg LiquidArg+ parseArg a+ | forwardToGhc a = Left a+ | otherwise = bimap (const a) (const a) (CmdArgs.process config [a])++ -- Unfortunate consequence of the facts things like '-i' needs to be forwarded to GHC+ -- and not the LH executable.+ forwardToGhc :: String -> Bool+ forwardToGhc = isPrefixOf "-i"+++helpNeeded :: [String] -> Bool+helpNeeded = elem "--help"+++main :: IO a+main = do++ -- If no args are passed, display the help instead of ghc's "no input files." To do so,+ -- due to the fact GHC needs to always have an input file to actually run a source plugin, we+ -- run this with '--interactive'.+ args <- getArgs <&> \case [] -> ["--interactive", "--help"]+ xs -> "--make" : xs++ ghcPath <- fromMaybe "ghc" <$> lookupEnv "LIQUID_GHC_PATH"++ -- Strip targets out of the arguments, so that we can forward them to GHC before they+ -- get intercepted by the LH parser.+ let (cliArgs, targets) = partition (isPrefixOf "-") args+ let (ghcArgs, liquidArgs) = partitionArgs cliArgs++ -- NOTE: Typically for the executable we want to recompile everything-everytime so that+ -- we could always get an "answer" out of LH. However, using `-fforce-recomp` as the default+ -- is dangerous, because the executable is used also during tests, so runtime is going to be+ -- badly affected. If users wants to enable recompilation, they would simply pass+ -- '-fforce-recomp' as a CLI argument.++ let p = proc ghcPath $ [ "-O0"+ , "-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+ <> ghcArgs+ <> targets++ -- Call into 'getOpts' so that things like the json reporter will correctly set the verbosity of the+ -- logging and avoid printing the banner.+ _ <- getOpts (args \\ ghcArgs)+ unless (helpNeeded args) printLiquidHaskellBanner++ withCreateProcess p $ \_mbStdIn _mbStdOut _mbStdErr pHandle -> waitForProcess pHandle >>= exitWith
+ src/Target.hs view
@@ -0,0 +1,29 @@+{-# 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