1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
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.
|