diff --git a/atp-haskell.cabal b/atp-haskell.cabal --- a/atp-haskell.cabal +++ b/atp-haskell.cabal @@ -1,5 +1,5 @@ Name: atp-haskell -Version: 1.14.2 +Version: 1.14.3 Synopsis: Translation from Ocaml to Haskell of John Harrison's ATP code Description: This package is a liberal translation from OCaml to Haskell of the automated theorem prover written in OCaml in @@ -12,10 +12,10 @@ Maintainer: David Fox Bug-Reports: https://github.com/seereason/atp-haskell/issues Category: Logic, Theorem Provers -Cabal-version: >= 1.9 +Cabal-version: >= 1.10 Build-Type: Simple Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci -Tested-With: GHC == 7.10.3, GHC == 7.11.*, GHC == 8.6.5 +Tested-With: GHC == 7.10.3, GHC == 7.11.*, GHC == 8.6.5, GHC == 9.8.2 Source-Repository head type: git @@ -98,3 +98,4 @@ Main-Is: Main.hs Build-Depends: atp-haskell, base, containers, HUnit, time GHC-options: -Wall -O2 + Other-Modules: Extra diff --git a/src/Data/Logic/ATP/PropExamples.hs b/src/Data/Logic/ATP/PropExamples.hs --- a/src/Data/Logic/ATP/PropExamples.hs +++ b/src/Data/Logic/ATP/PropExamples.hs @@ -159,7 +159,7 @@ (n - k) k) -- | Equivalence problems for carry-select vs ripple carry adders. (p. 69) -mk_adder_test :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a) => +mk_adder_test :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a, Show a) => a -> a -> formula mk_adder_test n k = let [x, y, c, s, c0, s0, c1, s1, c2, s2] = diff --git a/src/Data/Logic/ATP/Tableaux.hs b/src/Data/Logic/ATP/Tableaux.hs --- a/src/Data/Logic/ATP/Tableaux.hs +++ b/src/Data/Logic/ATP/Tableaux.hs @@ -23,6 +23,7 @@ ) where import Data.Logic.ATP.Apply (HasApply(TermOf), pApp) +import Control.Monad.Fail import Control.Monad.RWS (RWS) import Control.Monad.State (execStateT, StateT) import Data.List as List (map) @@ -48,7 +49,7 @@ unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1, - atom2 ~ AtomOf lit2, term ~ TermOf atom2) => + atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) => lit1 -> lit2 -> StateT (Map v term) m () unify_complements p q = unify_literals p ((.~.) q) diff --git a/src/Data/Logic/ATP/Unif.hs b/src/Data/Logic/ATP/Unif.hs --- a/src/Data/Logic/ATP/Unif.hs +++ b/src/Data/Logic/ATP/Unif.hs @@ -24,7 +24,9 @@ , testUnif ) where -import Control.Monad.State -- (evalStateT, runStateT, State, StateT, get) +import Control.Monad.State hiding (fail) -- (evalStateT, runStateT, State, StateT, get) +import Prelude hiding (fail) +import Control.Monad.Fail import Data.Bool (bool) import Data.List as List (map) import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), JustApply, zipApplys) @@ -59,12 +61,12 @@ unify :: (Unify m a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a)) unify a mp0 = execStateT (unify' a) mp0 -unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) => +unify_terms :: (IsTerm term, v ~ TVarOf term, MonadFail m) => [(term,term)] -> StateT (Map v term) m () unify_terms = mapM_ (uncurry unify_term_pair) unify_term_pair :: forall term v f m. - (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => + (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => term -> term -> StateT (Map v term) m () unify_term_pair a b = foldTerm (vr b) (\ f fargs -> foldTerm (vr a) (fn f fargs) b) a @@ -80,7 +82,7 @@ then mapM_ (uncurry unify_term_pair) (zip fargs gargs) else fail "impossible unification" -istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => +istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => v -> term -> StateT (Map v term) m Bool istriv x t = foldTerm vr fn t @@ -99,12 +101,12 @@ where env' = Map.map (tsubst env) env -- | Unification reaching a final solved form (often this isn't needed). -fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => +fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => [(term,term)] -> m (Map v term) fullunify eqs = solve <$> execStateT (unify_terms eqs) Map.empty -- | Examples. -unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => +unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => [(term, term)] -> m [(term, term)] unify_and_apply eqs = fullunify eqs >>= \i -> return $ List.map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs @@ -116,7 +118,8 @@ unify_literals :: forall lit1 lit2 atom1 atom2 v term m. (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, - Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => + Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, + MonadFail m) => lit1 -> lit2 -> StateT (Map v term) m () unify_literals f1 f2 = fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2) @@ -129,14 +132,14 @@ unify_atoms :: (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, - v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) => + v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, MonadFail m) => (atom1, atom2) -> StateT (Map v term) m () unify_atoms (a1, a2) = maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2) unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, - PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) => + PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, MonadFail m) => atom1 -> atom2 -> StateT (Map v term) m () unify_atoms_eq a1 a2 = maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)])) @@ -149,7 +152,7 @@ -- where -- app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2) -instance Monad m => Unify m (SkAtom, SkAtom) where +instance MonadFail m => Unify m (SkAtom, SkAtom) where type UTermOf (SkAtom, SkAtom) = TermOf SkAtom unify' = uncurry unify_atoms_eq