atp-haskell 1.10 → 1.13

raw patch · 3 files changed

+20/−12 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• atp-haskell.cabal +1/−1
• src/Data/Logic/ATP/Resolution.hs +3/−2
• src/Data/Logic/ATP/Unif.hs +16/−9

@@ -1,5 +1,5 @@ Name:             atp-haskell-Version:          1.10+Version:          1.13 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

@@ -79,10 +79,11 @@             _ -> solve <$> get       _ -> solve <$> get -unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),+unifiable :: forall lit term atom v.+             (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),               atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>              lit -> lit -> Bool-unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty)+unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty :: Failing (Map v term))  -- ------------------------------------------------------------------------- -- Rename a clause.

@@ -9,9 +9,11 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}  module Data.Logic.ATP.Unif-    ( Unify(unify, UTermOf)+    ( Unify(unify', UTermOf)+    , unify     , unify_terms     , unify_literals     , unify_atoms@@ -52,8 +54,11 @@ -- EqualityT a) b)@. class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where     type UTermOf a-    unify :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()+    unify' :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m () +unify :: (Unify 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) =>                [(term,term)] -> StateT (Map v term) m () unify_terms = mapM_ (uncurry unify_term_pair)@@ -75,19 +80,19 @@           then mapM_ (uncurry unify_term_pair) (zip fargs gargs)           else fail "impossible unification" -istriv :: forall term v m. (IsTerm term, v ~ TVarOf term, Monad m) =>+istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>           v -> term -> StateT (Map v term) m Bool istriv x t =     foldTerm vr fn t     where       vr :: v -> StateT (Map v term) m Bool       vr y | x == y = return True-      vr y = (Map.lookup y <$> get) >>= maybe (return False) (istriv x)+      vr y = (Map.lookup y <$> get) >>= \(mt :: Maybe term) -> maybe (return False) (istriv x) mt       fn :: f -> [term] -> StateT (Map v term) m Bool       fn _ args = mapM (istriv x) args >>= bool (return False) (fail "cyclic") . or  -- | Solve to obtain a single instantiation.-solve :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>+solve :: (IsTerm term, v ~ TVarOf term) =>          Map v term -> Map v term solve env =     if env' == env then env else solve env'@@ -108,7 +113,8 @@ -- variable type.  Note that only one needs to be 'JustLiteral', if -- the unification succeeds the other must have been too, if it fails, -- who cares.-unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,+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 (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, Monad m) =>                   lit1 -> lit2 -> StateT (Map v term) m ()@@ -117,8 +123,9 @@     where       ho _ _ = Nothing       ne p q = Just $ unify_literals p q-      tf p q = if p == q then Just (unify_terms []) else Nothing-      at a1 a2 = Just (unify (a1, a2))+      -- tf :: Bool -> Bool -> Maybe (StateT (Map v term) m ())+      tf p q = if p == q then Just (unify_terms ([] :: [(term, term)])) else Nothing+      at a1 a2 = Just (unify' (a1, a2))  unify_atoms :: (JustApply atom1, term ~ TermOf atom1,                 JustApply atom2, term ~ TermOf atom2,@@ -144,7 +151,7 @@  instance Unify (SkAtom, SkAtom) where     type UTermOf (SkAtom, SkAtom) = TermOf SkAtom-    unify = uncurry unify_atoms_eq+    unify' = uncurry unify_atoms_eq  test01, test02, test03, test04 :: Test test01 = TestCase (assertEqual "Unify test 1"