atp-haskell 1.14.2 → 1.14.3
raw patch · 4 files changed
+20/−15 lines, 4 files
Files
- atp-haskell.cabal +4/−3
- src/Data/Logic/ATP/PropExamples.hs +1/−1
- src/Data/Logic/ATP/Tableaux.hs +2/−1
- src/Data/Logic/ATP/Unif.hs +13/−10
atp-haskell.cabal view
@@ -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 <dsf@seereason.com> 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
src/Data/Logic/ATP/PropExamples.hs view
@@ -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] =
src/Data/Logic/ATP/Tableaux.hs view
@@ -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)
src/Data/Logic/ATP/Unif.hs view
@@ -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