200 lines
6.7 KiB
Text
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.
|