atp-haskell 1.13 → 1.14
raw patch · 5 files changed
+43/−42 lines, 5 filesdep +extraPVP ok
version bump matches the API change (PVP)
Dependencies added: extra
API changes (from Hackage documentation)
- Data.Logic.ATP.Unif: instance Data.Logic.ATP.Unif.Unify (Data.Logic.ATP.Skolem.SkAtom, Data.Logic.ATP.Skolem.SkAtom)
+ Data.Logic.ATP.Apply: type family TermOf atom;
+ Data.Logic.ATP.Apply: }
+ Data.Logic.ATP.Equate: infix 6 .=.
+ Data.Logic.ATP.Formulas: type family AtomOf formula;
+ Data.Logic.ATP.Formulas: }
+ Data.Logic.ATP.Lit: infix 6 ¬
+ Data.Logic.ATP.Pretty: infixr 6 <>
+ Data.Logic.ATP.Prop: infixl 2 <==>
+ Data.Logic.ATP.Prop: infixl 4 ∨
+ Data.Logic.ATP.Prop: infixl 5 `·`
+ Data.Logic.ATP.Prop: infixr 3 →
+ Data.Logic.ATP.Quantified: infixr 1 ∃
+ Data.Logic.ATP.Quantified: type family VarOf formula;
+ Data.Logic.ATP.Quantified: }
+ Data.Logic.ATP.Skolem: type family SVarOf function;
+ Data.Logic.ATP.Skolem: }
+ Data.Logic.ATP.Term: type family FunOf term;
+ Data.Logic.ATP.Term: }
+ Data.Logic.ATP.Unif: instance GHC.Base.Monad m => Data.Logic.ATP.Unif.Unify m (Data.Logic.ATP.Skolem.SkAtom, Data.Logic.ATP.Skolem.SkAtom)
+ Data.Logic.ATP.Unif: type family UTermOf a;
+ Data.Logic.ATP.Unif: }
- Data.Logic.ATP.Apply: class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where type family PredOf atom type family TermOf atom
+ Data.Logic.ATP.Apply: class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where type PredOf atom type TermOf atom where {
- Data.Logic.ATP.DefCNF: defcnf1 :: (IsPropositional pf, JustPropositional pf, NumAtom (AtomOf pf), Ord pf) => pf -> pf
+ Data.Logic.ATP.DefCNF: defcnf1 :: forall pf. (IsPropositional pf, JustPropositional pf, NumAtom (AtomOf pf), Ord pf) => pf -> pf
- Data.Logic.ATP.DefCNF: defcnf3 :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf
+ Data.Logic.ATP.DefCNF: defcnf3 :: forall pf. (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> pf
- Data.Logic.ATP.Equal: equalitize :: (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, IsQuantified formula, HasEquate atom, IsTerm term, Ord formula, Ord atom) => formula -> formula
+ Data.Logic.ATP.Equal: equalitize :: forall formula atom term v function. (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, IsQuantified formula, HasEquate atom, IsTerm term, Ord formula, Ord atom) => formula -> formula
- Data.Logic.ATP.Equal: function_congruence :: (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) => (function, Int) -> Set fof
+ Data.Logic.ATP.Equal: function_congruence :: forall fof atom term v p function. (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) => (function, Int) -> Set fof
- Data.Logic.ATP.FOL: holdsQuantified :: (IsQuantified formula, FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom, FiniteInterpretation formula function predicate (VarOf formula) dom) => Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool
+ Data.Logic.ATP.FOL: holdsQuantified :: forall formula function predicate dom. (IsQuantified formula, FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom, FiniteInterpretation formula function predicate (VarOf formula) dom) => Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool
- Data.Logic.ATP.Formulas: class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where type family AtomOf formula
+ Data.Logic.ATP.Formulas: class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where type AtomOf formula where {
- Data.Logic.ATP.Herbrand: davisputnam :: (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int
+ Data.Logic.ATP.Herbrand: davisputnam :: forall formula atom term v function. (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int
- Data.Logic.ATP.Herbrand: davisputnam' :: (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> formula -> formula -> Int
+ Data.Logic.ATP.Herbrand: davisputnam' :: forall formula atom term v function. (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> formula -> formula -> Int
- Data.Logic.ATP.Herbrand: gilmore :: (IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> Int
+ Data.Logic.ATP.Herbrand: gilmore :: forall fof atom term v function. (IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> Int
- Data.Logic.ATP.Herbrand: herbloop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, HasApply atom, IsTerm term) => (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)) -> (Set (Set lit) -> Bool) -> Set (Set lit) -> Set term -> Set (function, Int) -> [TVarOf term] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]
+ Data.Logic.ATP.Herbrand: herbloop :: forall lit atom function v term. (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, HasApply atom, IsTerm term) => (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)) -> (Set (Set lit) -> Bool) -> Set (Set lit) -> Set term -> Set (function, Int) -> [TVarOf term] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]
- Data.Logic.ATP.Lib: allnonemptysubsets :: Ord a => Set a -> Set (Set a)
+ Data.Logic.ATP.Lib: allnonemptysubsets :: forall a. Ord a => Set a -> Set (Set a)
- Data.Logic.ATP.Lib: allpairs :: (SetLike set, Ord c) => (a -> b -> c) -> set a -> set b -> set c
+ Data.Logic.ATP.Lib: allpairs :: forall a b c set. (SetLike set, Ord c) => (a -> b -> c) -> set a -> set b -> set c
- Data.Logic.ATP.Lib: allsets :: (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
+ Data.Logic.ATP.Lib: allsets :: forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
- Data.Logic.ATP.Lib: allsubsets :: Ord a => Set a -> Set (Set a)
+ Data.Logic.ATP.Lib: allsubsets :: forall a. Ord a => Set a -> Set (Set a)
- Data.Logic.ATP.Lib: optimize :: (SetLike s, Foldable s) => (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
+ Data.Logic.ATP.Lib: optimize :: forall s a b. (SetLike s, Foldable s) => (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
- Data.Logic.ATP.Lib: slMap :: (SetLike c, Ord b) => (a -> b) -> c a -> c b
+ Data.Logic.ATP.Lib: slMap :: forall a b. (SetLike c, Ord b) => (a -> b) -> c a -> c b
- Data.Logic.ATP.Lib: slView :: SetLike c => c a -> Maybe (a, c a)
+ Data.Logic.ATP.Lib: slView :: forall a. SetLike c => c a -> Maybe (a, c a)
- Data.Logic.ATP.Lib: undefine :: Ord k => k -> Map k a -> Map k a
+ Data.Logic.ATP.Lib: undefine :: forall k a. Ord k => k -> Map k a -> Map k a
- Data.Logic.ATP.Meson: meson :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
+ Data.Logic.ATP.Meson: meson :: (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
- Data.Logic.ATP.Meson: meson1 :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
+ Data.Logic.ATP.Meson: meson1 :: forall m fof atom predicate term function v. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
- Data.Logic.ATP.Meson: meson2 :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
+ Data.Logic.ATP.Meson: meson2 :: forall m fof atom term function v. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
- Data.Logic.ATP.Parser: def :: Stream s m Char => GenLanguageDef s u m
+ Data.Logic.ATP.Parser: def :: forall s u m. Stream s m Char => GenLanguageDef s u m
- Data.Logic.ATP.Parser: existentialQuantifier :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: existentialQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: folconstant :: (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
+ Data.Logic.ATP.Parser: folconstant :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
- Data.Logic.ATP.Parser: folconstant_numeric :: (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
+ Data.Logic.ATP.Parser: folconstant_numeric :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => ParsecT t t1 t2 term
- Data.Logic.ATP.Parser: folconstant_reserved :: (IsTerm term, Stream t t2 Char) => String -> ParsecT t t1 t2 term
+ Data.Logic.ATP.Parser: folconstant_reserved :: forall term t t1 t2. (IsTerm term, Stream t t2 Char) => String -> ParsecT t t1 t2 term
- Data.Logic.ATP.Parser: folfunction :: (IsTerm term, Stream s m Char) => ParsecT s u m term
+ Data.Logic.ATP.Parser: folfunction :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
- Data.Logic.ATP.Parser: folfunction_infix :: (IsTerm term, Stream s m Char) => ParsecT s u m term
+ Data.Logic.ATP.Parser: folfunction_infix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
- Data.Logic.ATP.Parser: folparser :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: folparser :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: folpredicate :: (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: folpredicate :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: folpredicate_infix :: (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: folpredicate_infix :: forall formula s u m. (IsFormula formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: folsubterm :: (IsTerm term, Stream s m Char) => ParsecT s u m term
+ Data.Logic.ATP.Parser: folsubterm :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
- Data.Logic.ATP.Parser: folsubterm_prefix :: (IsTerm term, Stream s m Char) => ParsecT s u m term
+ Data.Logic.ATP.Parser: folsubterm_prefix :: forall term s u m. (IsTerm term, Stream s m Char) => ParsecT s u m term
- Data.Logic.ATP.Parser: folterm :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: folterm :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: forallQuantifier :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: forallQuantifier :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: litexprparser :: (IsLiteral formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
+ Data.Logic.ATP.Parser: litexprparser :: forall formula s u m. (IsLiteral formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
- Data.Logic.ATP.Parser: litparser :: (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: litparser :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: litterm :: (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: litterm :: forall formula s u m. (JustLiteral formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: m_angles :: Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
+ Data.Logic.ATP.Parser: m_angles :: forall t t1 t2. Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
- Data.Logic.ATP.Parser: m_identifier :: Stream t t2 Char => ParsecT t t1 t2 String
+ Data.Logic.ATP.Parser: m_identifier :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 String
- Data.Logic.ATP.Parser: m_integer :: Stream t t2 Char => ParsecT t t1 t2 Integer
+ Data.Logic.ATP.Parser: m_integer :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 Integer
- Data.Logic.ATP.Parser: m_parens :: Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
+ Data.Logic.ATP.Parser: m_parens :: forall t t1 t2. Stream t t2 Char => forall a. ParsecT t t1 t2 a -> ParsecT t t1 t2 a
- Data.Logic.ATP.Parser: m_reserved :: Stream t t2 Char => String -> ParsecT t t1 t2 ()
+ Data.Logic.ATP.Parser: m_reserved :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 ()
- Data.Logic.ATP.Parser: m_reservedOp :: Stream t t2 Char => String -> ParsecT t t1 t2 ()
+ Data.Logic.ATP.Parser: m_reservedOp :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 ()
- Data.Logic.ATP.Parser: m_symbol :: Stream t t2 Char => String -> ParsecT t t1 t2 String
+ Data.Logic.ATP.Parser: m_symbol :: forall t t1 t2. Stream t t2 Char => String -> ParsecT t t1 t2 String
- Data.Logic.ATP.Parser: m_whiteSpace :: Stream t t2 Char => ParsecT t t1 t2 ()
+ Data.Logic.ATP.Parser: m_whiteSpace :: forall t t1 t2. Stream t t2 Char => ParsecT t t1 t2 ()
- Data.Logic.ATP.Parser: propexprparser :: (IsPropositional formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
+ Data.Logic.ATP.Parser: propexprparser :: forall formula s u m. (IsPropositional formula, Stream s m Char) => ParsecT s u m formula -> ParsecT s u m formula
- Data.Logic.ATP.Parser: propparser :: (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: propparser :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: propterm :: (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
+ Data.Logic.ATP.Parser: propterm :: forall formula s u m. (JustPropositional formula, HasEquate (AtomOf formula), Stream s m Char) => ParsecT s u m formula
- Data.Logic.ATP.Parser: quantifierId :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula
+ Data.Logic.ATP.Parser: quantifierId :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula
- Data.Logic.ATP.Parser: quantifierOp :: (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula
+ Data.Logic.ATP.Parser: quantifierOp :: forall formula s u m. (IsQuantified formula, HasEquate (AtomOf formula), Stream s m Char) => String -> (String -> formula -> formula) -> ParsecT s u m formula
- Data.Logic.ATP.Pretty: pPrint :: Pretty a => a -> Doc
+ Data.Logic.ATP.Pretty: pPrint :: a -> Doc
- Data.Logic.ATP.Pretty: pPrintPrec :: Pretty a => PrettyLevel -> Rational -> a -> Doc
+ Data.Logic.ATP.Pretty: pPrintPrec :: PrettyLevel -> Rational -> a -> Doc
- Data.Logic.ATP.Prolog: renamerule :: (IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Int -> PrologRule lit -> (PrologRule lit, Int)
+ Data.Logic.ATP.Prolog: renamerule :: forall lit atom term v. (IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Int -> PrologRule lit -> (PrologRule lit, Int)
- Data.Logic.ATP.Prop: cnf' :: (JustPropositional pf, Ord pf) => pf -> pf
+ Data.Logic.ATP.Prop: cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
- Data.Logic.ATP.Prop: dnf :: (JustPropositional pf, Ord pf) => pf -> pf
+ Data.Logic.ATP.Prop: dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
- Data.Logic.ATP.Prop: prettyPropositional :: JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc
+ Data.Logic.ATP.Prop: prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc
- Data.Logic.ATP.Quantified: associativityQuantified :: IsQuantified formula => formula -> Associativity
+ Data.Logic.ATP.Quantified: associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity
- Data.Logic.ATP.Quantified: class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where type family VarOf formula
+ Data.Logic.ATP.Quantified: class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where type VarOf formula where {
- Data.Logic.ATP.Quantified: convertQuantified :: (IsQuantified f1, IsQuantified f2) => (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
+ Data.Logic.ATP.Quantified: convertQuantified :: forall f1 f2. (IsQuantified f1, IsQuantified f2) => (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
- Data.Logic.ATP.Quantified: precedenceQuantified :: IsQuantified formula => formula -> Precedence
+ Data.Logic.ATP.Quantified: precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence
- Data.Logic.ATP.Quantified: prettyQuantified :: (IsQuantified fof, v ~ VarOf fof) => Side -> PrettyLevel -> Rational -> fof -> Doc
+ Data.Logic.ATP.Quantified: prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) => Side -> PrettyLevel -> Rational -> fof -> Doc
- Data.Logic.ATP.Resolution: presolution :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
+ Data.Logic.ATP.Resolution: presolution :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
- Data.Logic.ATP.Resolution: resolution1 :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
+ Data.Logic.ATP.Resolution: resolution1 :: forall m fof atom term v function. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
- Data.Logic.ATP.Resolution: resolution2 :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
+ Data.Logic.ATP.Resolution: resolution2 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
- Data.Logic.ATP.Resolution: resolution3 :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
+ Data.Logic.ATP.Resolution: resolution3 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))
- Data.Logic.ATP.Skolem: class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where type family SVarOf function
+ Data.Logic.ATP.Skolem: class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where type SVarOf function where {
- Data.Logic.ATP.Tableaux: prawitz :: (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int
+ Data.Logic.ATP.Tableaux: prawitz :: forall formula atom term function v. (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int
- Data.Logic.ATP.Tableaux: tab :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
+ Data.Logic.ATP.Tableaux: tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
- Data.Logic.ATP.Term: class (Eq term, Ord term, Pretty term, Show term, IsString term, HasFixity term, IsVariable (TVarOf term), IsFunction (FunOf term)) => IsTerm term where type family TVarOf term type family FunOf term
+ Data.Logic.ATP.Term: class (Eq term, Ord term, Pretty term, Show term, IsString term, HasFixity term, IsVariable (TVarOf term), IsFunction (FunOf term)) => IsTerm term where type TVarOf term type FunOf term where {
- Data.Logic.ATP.Unif: class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where type family UTermOf a
+ Data.Logic.ATP.Unif: class (Monad m, IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify m a where type UTermOf a where {
- Data.Logic.ATP.Unif: unify :: (Unify a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a))
+ Data.Logic.ATP.Unif: unify :: (Unify m a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a))
- Data.Logic.ATP.Unif: unify' :: (Unify a, Monad m) => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
+ Data.Logic.ATP.Unif: unify' :: Unify m a => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
- Data.Logic.ATP.Unif: unify_literals :: (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 ()
+ Data.Logic.ATP.Unif: 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) => lit1 -> lit2 -> StateT (Map v term) m ()
Files
- atp-haskell.cabal +2/−1
- src/Data/Logic/ATP/Meson.hs +9/−9
- src/Data/Logic/ATP/Resolution.hs +16/−16
- src/Data/Logic/ATP/Tableaux.hs +11/−11
- src/Data/Logic/ATP/Unif.hs +5/−5
atp-haskell.cabal view
@@ -1,5 +1,5 @@ Name: atp-haskell-Version: 1.13+Version: 1.14 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@@ -26,6 +26,7 @@ applicative-extras, base >= 4.8 && < 5, containers,+ extra, HUnit, mtl, parsec,
src/Data/Logic/ATP/Meson.hs view
@@ -176,7 +176,7 @@ -- ------------------------------------------------------------------------- mexpand1 :: (JustLiteral lit, Ord lit,- HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),+ HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (PrologRule lit) -> Set lit@@ -206,7 +206,7 @@ -- ------------------------------------------------------------------------- puremeson1 :: forall fof atom term v function.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) => Maybe Depth -> fof -> Failing Depth@@ -219,7 +219,7 @@ (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom) meson1 :: forall m fof atom predicate term function v.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth)) meson1 maxdl fm =@@ -230,7 +230,7 @@ -- With repetition checking and divide-and-conquer search. -- ------------------------------------------------------------------------- -equal :: (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,+equal :: (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> lit -> lit -> Bool equal env fm1 fm2 =@@ -257,7 +257,7 @@ (e1,n2+r1,k1)) (env,n1,k) -mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),+mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (PrologRule lit) -> Set lit@@ -284,7 +284,7 @@ mexpand2' = mexpands rules (Set.insert g ancestors) asm cont (Prolog asm c, k') = renamerule k rule -mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,+mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (PrologRule lit) -> Set lit@@ -317,7 +317,7 @@ puremeson2 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, IsFirstOrder fof,- Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof ) => Maybe Depth -> fof -> Failing Depth puremeson2 maxdl fm = snd <$> deepen f (Depth 0) maxdl@@ -328,7 +328,7 @@ (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom) meson2 :: forall m fof atom term function v.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))@@ -336,7 +336,7 @@ askolemize ((.~.)(generalize fm)) >>= return . Set.map (puremeson2 maxdl . list_conj) . (simpdnf' :: fof -> Set (Set fof)) -meson :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,+meson :: (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth)) meson = meson2
src/Data/Logic/ATP/Resolution.hs view
@@ -68,7 +68,7 @@ -- | MGU of a set of literals. mgu :: forall lit atom term v.- (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,+ (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> StateT (Map v term) Failing (Map v term) mgu l =@@ -80,7 +80,7 @@ _ -> solve <$> get unifiable :: forall lit term atom v.- (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),+ (JustLiteral lit, IsTerm term, HasApply atom, Unify Failing (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 :: Failing (Map v term))@@ -101,7 +101,7 @@ -- General resolution rule, incorporating factoring as in Robinson's paper. -- ------------------------------------------------------------------------- -resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,+resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> lit -> Set lit -> Set lit resolvents cl1 cl2 p acc =@@ -118,7 +118,7 @@ -- ps2 :: Set fof ps2 = Set.filter (unifiable ((.~.) p)) cl2 -resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,+resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> Set lit resolve_clauses cls1 cls2 =@@ -130,7 +130,7 @@ -- Basic "Argonne" loop. -- ------------------------------------------------------------------------- -resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),+resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool resloop1 used unused =@@ -146,13 +146,13 @@ pure_resolution1 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, IsFirstOrder fof,- Unify (atom, atom), term ~ UTermOf (atom, atom),+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, Pretty fof ) => fof -> Failing Bool pure_resolution1 fm = resloop1 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom))) resolution1 :: forall m fof atom term v function.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof))@@ -221,7 +221,7 @@ -- | With deletion of tautologies and bi-subsumption with "unused". resolution2 :: forall fof atom term v function m.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof))@@ -229,13 +229,13 @@ pure_resolution2 :: forall fof atom term v. (IsFirstOrder fof, Ord fof, Pretty fof, HasApply atom, IsTerm term,- Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) => fof -> Failing Bool pure_resolution2 fm = resloop2 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom))) resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,- Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool resloop2 used unused =@@ -296,20 +296,20 @@ -- | Positive (P1) resolution. presolution :: forall fof atom term v function m.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) presolution fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_presolution . list_conj) . (simpdnf' :: fof -> Set (Set fof)) pure_presolution :: forall fof atom term v.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => fof -> Failing Bool pure_presolution fm = presloop Set.empty (simpcnf id (specialize id (pnf fm :: fof) :: PFormula atom) :: Set (Set (LFormula atom))) presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,- Match (atom, atom) v term, Unify (atom, atom), term ~ UTermOf (atom, atom),+ Match (atom, atom) v term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool presloop used unused =@@ -324,7 +324,7 @@ then Success True else presloop used' (Set.fold (incorporate cl) ros news) -presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),+presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> Set lit presolve_clauses cls1 cls2 =@@ -334,7 +334,7 @@ -- | Introduce a set-of-support restriction. resolution3 :: forall fof atom term v function m.- (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+ (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution3 fm =@@ -343,7 +343,7 @@ pure_resolution3 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, IsFirstOrder fof,- Unify (atom, atom), term ~ UTermOf (atom, atom),+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof) => fof -> Failing Bool pure_resolution3 fm =
src/Data/Logic/ATP/Tableaux.hs view
@@ -46,20 +46,20 @@ -- | Unify complementary literals. unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,- Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,+ Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1, atom2 ~ AtomOf lit2, term ~ TermOf atom2) =>- lit1 -> lit2 -> StateT (Map v term) Failing ()+ lit1 -> lit2 -> StateT (Map v term) m () unify_complements p q = unify_literals p ((.~.) q) -- | Unify and refute a set of disjuncts. unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,- Unify (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,+ Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) => Set (Set lit) -> Map v term -> Failing (Map v term) unify_refute djs env = case Set.minView djs of- Nothing -> Success env+ Nothing -> pure env Just (d, odjs) -> settryfind (\ (p, n) -> execStateT (unify_complements p n) env >>= unify_refute odjs) pairs where@@ -68,7 +68,7 @@ -- | Hence a Prawitz-like procedure (using unification on DNF). prawitz_loop :: forall lit atom v term.- (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),+ (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int) prawitz_loop djs0 fvs djs n =@@ -81,7 +81,7 @@ newvar k = vt (fromString ("_" ++ show (n * length fvs + k))) prawitz :: forall formula atom term function v.- (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,+ (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int@@ -110,7 +110,7 @@ -- Comparison of number of ground instances. -- ------------------------------------------------------------------------- -compare :: (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,+compare :: (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> (Int, Int)@@ -178,7 +178,7 @@ -- | More standard tableau procedure, effectively doing DNF incrementally. (p. 177) tableau :: forall formula atom term v function.- (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),+ (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) => [formula] -> Depth -> RWS () () () (Failing (K, Map v term)) tableau fms n0 =@@ -214,14 +214,14 @@ tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term)) tryLit fm' l = failing (return . Failure) (\env' -> cont (k, env')) (execStateT (unify_complements fm' l) env) -tabrefute :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),+tabrefute :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth) tabrefute limit fms = let r = deepen (\n -> (,n) <$> evalRS (tableau fms n) () ()) (Depth 0) limit in failing Failure (Success . fst) r -tab :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,+tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth)@@ -288,7 +288,7 @@ -- Try to split up the initial formula first; often a big improvement. -- ------------------------------------------------------------------------- splittab :: forall formula atom term v function.- (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,+ (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> [Failing ((K, Map v term), Depth)]
src/Data/Logic/ATP/Unif.hs view
@@ -52,11 +52,11 @@ -- single type contains both - for example, in template-haskell we -- want to unify a and b in a predicate such as this: @(AppT (AppT -- EqualityT a) b)@.-class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where+class (Monad m, IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify m a where type UTermOf a- unify' :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()+ unify' :: 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 :: (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) =>@@ -116,7 +116,7 @@ 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) =>+ Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) m () unify_literals f1 f2 = fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)@@ -149,7 +149,7 @@ -- where -- app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2) -instance Unify (SkAtom, SkAtom) where+instance Monad m => Unify m (SkAtom, SkAtom) where type UTermOf (SkAtom, SkAtom) = TermOf SkAtom unify' = uncurry unify_atoms_eq