From dc164dc2eebf014759a6ef7cccb4febc891390d2 Mon Sep 17 00:00:00 2001 From: Fabian Schmitthenner Date: Fri, 27 Nov 2015 07:55:56 +0000 Subject: system for automated deduction: init at 2.3-25 --- pkgs/applications/science/logic/sad/default.nix | 33 ++++ pkgs/applications/science/logic/sad/patch | 200 ++++++++++++++++++++++++ 2 files changed, 233 insertions(+) create mode 100644 pkgs/applications/science/logic/sad/default.nix create mode 100644 pkgs/applications/science/logic/sad/patch (limited to 'pkgs/applications/science') 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. -- cgit 1.4.1