system for automated deduction: init at 2.3-25

2 files changed, 233 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/sad/default.nix b/pkgs/applications/science/logic/sad/default.nix
new file mode 100644
index 000000000000..d9d36b991177
--- /dev/null
+++ b/pkgs/applications/science/logic/sad/default.nix
@@ -0,0 +1,33 @@
+{ stdenv, fetchurl, ghc, spass }:
+
+stdenv.mkDerivation {
+  name = "system-for-automated-deduction-2.3.25";
+  src = fetchurl {
+    url = "http://nevidal.org/download/sad-2.3-25.tar.gz";
+    sha256 = "10jd93xgarik7xwys5lq7fx4vqp7c0yg1gfin9cqfch1k1v8ap4b";
+  };
+  buildInputs = [ ghc spass ];
+  patches = [ ./patch ];
+  postPatch = ''
+    substituteInPlace Alice/Main.hs --replace init.opt $out/init.opt
+    '';
+  installPhase = ''
+    mkdir -p $out/{bin,provers}
+    install alice $out/bin
+    install provers/moses $out/provers
+    substituteAll provers/provers.dat $out/provers/provers.dat
+    substituteAll init.opt $out/init.opt
+    cp -r examples $out
+    '';
+  inherit spass;
+  meta = {
+    description = "A program for automated proving of mathematical texts";
+    longDescription = ''
+      The system for automated deduction is intended for automated processing of formal mathematical texts 
+      written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language
+      '';
+    license = stdenv.lib.licenses.gpl3Plus;
+    maintainers = [ stdenv.lib.maintainers.schmitthenner ];
+    homepage = http://nevidal.org/sad.en.html;
+  };  
+}
diff --git a/pkgs/applications/science/logic/sad/patch b/pkgs/applications/science/logic/sad/patch
new file mode 100644
index 000000000000..a5b1d6177083
--- /dev/null
+++ b/pkgs/applications/science/logic/sad/patch
@@ -0,0 +1,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.