jukebox 0.4.2 → 0.4.3
raw patch · 4 files changed
+25/−22 lines, 4 filesdep +fail
Dependencies added: fail
Files
- executable/Main.hs +6/−1
- jukebox.cabal +9/−19
- src/Jukebox/Sat/Easy.hs +1/−1
- src/Jukebox/TPTP/Parsec.hs +9/−1
executable/Main.hs view
@@ -32,7 +32,12 @@ ["help"] -> help ["--help"] -> help ["--version"] ->- putStrLn $ "Jukebox version " ++ VERSION_jukebox+ putStrLn $ "Jukebox version " +++#ifdef VERSION_jukebox+ VERSION_jukebox+#else+ "unknown"+#endif (('-':_):_) -> usage "Expected a tool name as first argument" (arg:args) -> case [tool | tool <- tools, name tool == arg] of
jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.4.2+Version: 0.4.3 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone@@ -19,10 +19,6 @@ License-file: LICENSE extra-source-files: src/errors.h gcc-static-libstdc++ -flag minisat- Description: Use minisat. Required for monotonicity inference.- Default: True- flag static-cxx description: Build a binary which statically links against libstdc++. default: False@@ -33,21 +29,10 @@ Library Build-depends: base >= 4 && < 5, array, transformers >= 0.4.0.0, directory,- filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo+ filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo,+ minisat if !impl(ghc >= 8.0)- Build-depends: semigroups- if impl(ghc >= 8.6)- extensions: NoMonadFailDesugaring- if flag(minisat)- Build-depends: minisat- Exposed-modules:- Jukebox.Sat- Jukebox.Sat.ThreeValued- Jukebox.Sat.Equality- Jukebox.Sat.Minimise- Jukebox.Sat.Easy- else- cpp-options: -DNO_MINISAT+ Build-depends: semigroups, fail ghc-options: -W -fno-warn-incomplete-patterns Build-tools: alex Hs-source-dirs: src@@ -58,6 +43,11 @@ Jukebox.Options Jukebox.ExternalProvers.E Jukebox.ExternalProvers.SPASS+ Jukebox.Sat+ Jukebox.Sat.ThreeValued+ Jukebox.Sat.Equality+ Jukebox.Sat.Minimise+ Jukebox.Sat.Easy Jukebox.SMTLIB Jukebox.Toolbox Jukebox.Tools.Clausify
src/Jukebox/Sat/Easy.hs view
@@ -77,7 +77,7 @@ modelValue x = do s <- Sat1 ask l <- var x- Just b <- liftIO (MiniSat.modelValue s l)+ ~(Just b) <- liftIO (MiniSat.modelValue s l) return b addForm :: Ord a => Form a -> Sat1 a ()
src/Jukebox/TPTP/Parsec.hs view
@@ -1,10 +1,11 @@-{-# LANGUAGE RankNTypes, BangPatterns, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies #-}+{-# LANGUAGE RankNTypes, BangPatterns, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies, CPP #-} {-# OPTIONS_GHC -funfolding-creation-threshold=10000 -funfolding-use-threshold=10000 #-} module Jukebox.TPTP.Parsec where import Control.Applicative import Control.Monad import Data.List+import Control.Monad.Fail -- Parser type and monad instances @@ -35,6 +36,13 @@ return x = Parsec (\ok err inp exp -> ok x err inp exp) {-# INLINE (>>=) #-} x >>= f = Parsec (\ok err inp exp -> runParsec x (\y err inp exp -> runParsec (f y) ok err inp exp) err inp exp)++#if __GLASGOW_HASKELL__ < 808+ {-# INLINE fail #-}+ fail _ = parseError []+#endif++instance MonadFail (Parsec a) where {-# INLINE fail #-} fail _ = parseError []