nixpkgs-suyu/pkgs/applications/science/logic/sad/patch
2015-11-27 15:12:09 +00:00

200 lines
6.7 KiB
Text

diff -aur serious/sad-2.3-25/Alice/Core/Base.hs sad-2.3-25/Alice/Core/Base.hs
--- serious/sad-2.3-25/Alice/Core/Base.hs 2008-03-29 18:24:12.000000000 +0000
+++ sad-2.3-25/Alice/Core/Base.hs 2015-11-27 06:38:28.740840823 +0000
@@ -21,6 +21,7 @@
module Alice.Core.Base where
import Control.Monad
+import Control.Applicative
import Data.IORef
import Data.List
import Data.Time
@@ -61,10 +62,21 @@
type CRMC a b = IORef RState -> IO a -> (b -> IO a) -> IO a
newtype CRM b = CRM { runCRM :: forall a . CRMC a b }
+instance Functor CRM where
+ fmap = liftM
+
+instance Applicative CRM where
+ pure = return
+ (<*>) = ap
+
instance Monad CRM where
return r = CRM $ \ _ _ k -> k r
m >>= n = CRM $ \ s z k -> runCRM m s z (\ r -> runCRM (n r) s z k)
+instance Alternative CRM where
+ (<|>) = mplus
+ empty = mzero
+
instance MonadPlus CRM where
mzero = CRM $ \ _ z _ -> z
mplus m n = CRM $ \ s z k -> runCRM m s (runCRM n s z k) k
diff -aur serious/sad-2.3-25/Alice/Core/Thesis.hs sad-2.3-25/Alice/Core/Thesis.hs
--- serious/sad-2.3-25/Alice/Core/Thesis.hs 2008-03-05 13:10:50.000000000 +0000
+++ sad-2.3-25/Alice/Core/Thesis.hs 2015-11-27 06:35:08.311015166 +0000
@@ -21,6 +21,7 @@
module Alice.Core.Thesis (thesis) where
import Control.Monad
+import Control.Applicative
import Data.List
import Data.Maybe
@@ -126,11 +127,22 @@
newtype TM res = TM { runTM :: [String] -> [([String], res)] }
+instance Functor TM where
+ fmap = liftM
+
+instance Applicative TM where
+ pure = return
+ (<*>) = ap
+
instance Monad TM where
return r = TM $ \ s -> [(s, r)]
m >>= k = TM $ \ s -> concatMap apply (runTM m s)
where apply (s, r) = runTM (k r) s
+instance Alternative TM where
+ (<|>) = mplus
+ empty = mzero
+
instance MonadPlus TM where
mzero = TM $ \ _ -> []
mplus m k = TM $ \ s -> runTM m s ++ runTM k s
diff -aur serious/sad-2.3-25/Alice/Export/Base.hs sad-2.3-25/Alice/Export/Base.hs
--- serious/sad-2.3-25/Alice/Export/Base.hs 2008-03-09 09:36:39.000000000 +0000
+++ sad-2.3-25/Alice/Export/Base.hs 2015-11-27 06:32:47.782738005 +0000
@@ -39,7 +39,7 @@
-- Database reader
readPrDB :: String -> IO [Prover]
-readPrDB file = do inp <- catch (readFile file) $ die . ioeGetErrorString
+readPrDB file = do inp <- catchIOError (readFile file) $ die . ioeGetErrorString
let dws = dropWhile isSpace
cln = reverse . dws . reverse . dws
diff -aur serious/sad-2.3-25/Alice/Export/Prover.hs sad-2.3-25/Alice/Export/Prover.hs
--- serious/sad-2.3-25/Alice/Export/Prover.hs 2008-03-09 09:36:39.000000000 +0000
+++ sad-2.3-25/Alice/Export/Prover.hs 2015-11-27 06:36:47.632919161 +0000
@@ -60,7 +60,7 @@
when (askIB IBPdmp False ins) $ putStrLn tsk
seq (length tsk) $ return $
- do (wh,rh,eh,ph) <- catch run
+ do (wh,rh,eh,ph) <- catchIOError run
$ \ e -> die $ "run error: " ++ ioeGetErrorString e
hPutStrLn wh tsk ; hClose wh
diff -aur serious/sad-2.3-25/Alice/ForTheL/Base.hs sad-2.3-25/Alice/ForTheL/Base.hs
--- serious/sad-2.3-25/Alice/ForTheL/Base.hs 2008-03-09 09:36:39.000000000 +0000
+++ sad-2.3-25/Alice/ForTheL/Base.hs 2015-11-27 06:31:51.921230428 +0000
@@ -226,7 +226,7 @@
varlist = do vs <- chainEx (char ',') var
nodups vs ; return vs
-nodups vs = unless (null $ dups vs) $
+nodups vs = unless ((null :: [a] -> Bool) $ dups vs) $
fail $ "duplicate names: " ++ show vs
hidden = askPS psOffs >>= \ n -> return ('h':show n)
diff -aur serious/sad-2.3-25/Alice/Import/Reader.hs sad-2.3-25/Alice/Import/Reader.hs
--- serious/sad-2.3-25/Alice/Import/Reader.hs 2008-03-09 09:36:39.000000000 +0000
+++ sad-2.3-25/Alice/Import/Reader.hs 2015-11-27 06:36:41.818866167 +0000
@@ -24,7 +24,7 @@
import Control.Monad
import System.IO
import System.IO.Error
-import System.Exit
+import System.Exit hiding (die)
import Alice.Data.Text
import Alice.Data.Instr
@@ -44,7 +44,7 @@
readInit "" = return []
readInit file =
- do input <- catch (readFile file) $ die file . ioeGetErrorString
+ do input <- catchIOError (readFile file) $ die file . ioeGetErrorString
let tkn = tokenize input ; ips = initPS ()
inp = ips { psRest = tkn, psFile = file, psLang = "Init" }
liftM fst $ fireLPM instf inp
@@ -74,7 +74,7 @@
reader lb fs (ps:ss) [TI (InStr ISfile file)] =
do let gfl = if null file then hGetContents stdin
else readFile file
- input <- catch gfl $ die file . ioeGetErrorString
+ input <- catchIOError gfl $ die file . ioeGetErrorString
let tkn = tokenize input
ips = initPS $ (psProp ps) { tvr_expr = [] }
sps = ips { psRest = tkn, psFile = file, psOffs = psOffs ps }
diff -aur serious/sad-2.3-25/Alice/Parser/Base.hs sad-2.3-25/Alice/Parser/Base.hs
--- serious/sad-2.3-25/Alice/Parser/Base.hs 2008-03-09 09:36:40.000000000 +0000
+++ sad-2.3-25/Alice/Parser/Base.hs 2015-11-27 06:14:28.616734527 +0000
@@ -20,6 +20,7 @@
module Alice.Parser.Base where
+import Control.Applicative
import Control.Monad
import Data.List
@@ -45,11 +46,22 @@
type CPMC a b c = (c -> CPMS a b) -> (String -> CPMS a b) -> CPMS a b
newtype CPM a c = CPM { runCPM :: forall b . CPMC a b c }
+instance Functor (CPM a) where
+ fmap = liftM
+
+instance Applicative (CPM a) where
+ pure = return
+ (<*>) = ap
+
instance Monad (CPM a) where
return r = CPM $ \ k _ -> k r
m >>= n = CPM $ \ k l -> runCPM m (\ b -> runCPM (n b) k l) l
fail e = CPM $ \ _ l -> l e
+instance Alternative (CPM a) where
+ (<|>) = mplus
+ empty = mzero
+
instance MonadPlus (CPM a) where
mzero = CPM $ \ _ _ _ z -> z
mplus m n = CPM $ \ k l s -> runCPM m k l s . runCPM n k l s
diff -aur serious/sad-2.3-25/init.opt sad-2.3-25/init.opt
--- serious/sad-2.3-25/init.opt 2007-10-11 15:25:45.000000000 +0000
+++ sad-2.3-25/init.opt 2015-11-27 07:23:41.372816854 +0000
@@ -1,6 +1,6 @@
# Alice init options
-[library examples]
-[provers provers/provers.dat]
+[library @out@/examples]
+[provers @out@/provers/provers.dat]
[prover spass]
[timelimit 3]
[depthlimit 7]
diff -aur serious/sad-2.3-25/provers/provers.dat sad-2.3-25/provers/provers.dat
--- serious/sad-2.3-25/provers/provers.dat 2008-08-26 21:20:25.000000000 +0000
+++ sad-2.3-25/provers/provers.dat 2015-11-27 07:24:18.878169702 +0000
@@ -3,7 +3,7 @@
Pmoses
LMoses
Fmoses
-Cprovers/moses
+C@out@/provers/moses
Yproved in
Nfound unprovable in
Utimeout in
@@ -12,7 +12,7 @@
Pspass
LSPASS
Fdfg
-Cprovers/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d
+C@spass@/bin/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d
YSPASS beiseite: Proof found.
NSPASS beiseite: Completion found.
USPASS beiseite: Ran out of time.