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.8 +Version: 1.9 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 diff --git a/src/Data/Logic/ATP/Meson.hs b/src/Data/Logic/ATP/Meson.hs --- a/src/Data/Logic/ATP/Meson.hs +++ b/src/Data/Logic/ATP/Meson.hs @@ -33,7 +33,7 @@ import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf), pnf, runSkolem, SkolemT, simpdnf', specialize, toSkolem) import Data.Logic.ATP.Tableaux (K(K), tab) import Data.Logic.ATP.Term (fApp, IsTerm(FunOf, TVarOf), vt) -import Data.Logic.ATP.Unif (Unify, unify_literals) +import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Set as Set import Test.HUnit @@ -176,7 +176,7 @@ -- ------------------------------------------------------------------------- mexpand1 :: (JustLiteral lit, Ord lit, - HasApply atom, IsTerm term, Unify atom atom, + HasApply atom, IsTerm term, Unify (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, Ord fof, + (IsFirstOrder fof, Unify (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, Ord fof, HasSkolem function, Monad m, + (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)) meson1 maxdl fm = @@ -230,7 +230,7 @@ -- With repetition checking and divide-and-conquer search. -- ------------------------------------------------------------------------- -equal :: (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term, +equal :: (JustLiteral lit, HasApply atom, Unify (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, +mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (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, IsTerm term, +mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify (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, Ord fof + Unify (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, Ord fof, + (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)) @@ -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, HasSkolem function, Monad m, Ord fof, +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)) meson = meson2 diff --git a/src/Data/Logic/ATP/Pretty.hs b/src/Data/Logic/ATP/Pretty.hs --- a/src/Data/Logic/ATP/Pretty.hs +++ b/src/Data/Logic/ATP/Pretty.hs @@ -9,7 +9,6 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -{-# OPTIONS_GHC -ddump-splices #-} module Data.Logic.ATP.Pretty ( (<>) @@ -105,7 +104,11 @@ pPrint = pPrint . Map.toList -- | Version of assertEqual that uses the pretty printer instead of show. -assertEqual' :: (?loc :: CallStack, Eq a, Pretty a) => +assertEqual' :: ( +#ifndef ghcjs_HOST_OS + ?loc :: CallStack, +#endif + Eq a, Pretty a) => String -- ^ The message prefix -> a -- ^ The expected value -> a -- ^ The actual value diff --git a/src/Data/Logic/ATP/Resolution.hs b/src/Data/Logic/ATP/Resolution.hs --- a/src/Data/Logic/ATP/Resolution.hs +++ b/src/Data/Logic/ATP/Resolution.hs @@ -40,7 +40,7 @@ import Data.Logic.ATP.Skolem (askolemize, Formula, Function(Skolem), HasSkolem(SVarOf), pnf, runSkolem, simpdnf', SkAtom, skolemize, SkolemT, specialize, SkTerm) import Data.Logic.ATP.Term (fApp, foldTerm, IsTerm(FunOf, TVarOf), prefix, V, vt) -import Data.Logic.ATP.Unif (solve, Unify, unify_literals) +import Data.Logic.ATP.Unif (solve, Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Maybe (fromMaybe) import Data.Set as Set @@ -68,7 +68,7 @@ -- | MGU of a set of literals. mgu :: forall lit atom term v. - (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term, + (JustLiteral lit, HasApply atom, Unify (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 = @@ -79,7 +79,7 @@ _ -> solve <$> get _ -> solve <$> get -unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify atom atom, +unifiable :: (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) @@ -100,7 +100,7 @@ -- General resolution rule, incorporating factoring as in Robinson's paper. -- ------------------------------------------------------------------------- -resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term, +resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify (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 = @@ -117,7 +117,7 @@ -- ps2 :: Set fof ps2 = Set.filter (unifiable ((.~.) p)) cl2 -resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term, +resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify (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 = @@ -129,7 +129,7 @@ -- Basic "Argonne" loop. -- ------------------------------------------------------------------------- -resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom, +resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (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 = @@ -145,13 +145,13 @@ pure_resolution1 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, IsFirstOrder fof, - Unify atom atom, + Unify (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, Ord fof, HasSkolem function, Monad m, + (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)) resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof)) @@ -220,7 +220,7 @@ -- | With deletion of tautologies and bi-subsumption with "unused". resolution2 :: forall fof atom term v function m. - (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, + (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)) resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof)) @@ -228,13 +228,13 @@ pure_resolution2 :: forall fof atom term v. (IsFirstOrder fof, Ord fof, Pretty fof, HasApply atom, IsTerm term, - Unify atom atom, Match (atom, atom) v term, + Unify (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, Match (atom, atom) v term, + Unify (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 = @@ -295,20 +295,20 @@ -- | Positive (P1) resolution. presolution :: forall fof atom term v function m. - (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, + (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)) 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, Match (atom, atom) v term, Ord fof, Pretty fof, + (IsFirstOrder fof, Unify (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, + Match (atom, atom) v term, Unify (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 = @@ -323,7 +323,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, +presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (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 = @@ -333,7 +333,7 @@ -- | Introduce a set-of-support restriction. resolution3 :: forall fof atom term v function m. - (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, + (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)) resolution3 fm = @@ -342,7 +342,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, + Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof) => fof -> Failing Bool pure_resolution3 fm = 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 @@ -37,7 +37,7 @@ import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:))) import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf, toSkolem), runSkolem, simpdnf', skolemize, SkTerm) import Data.Logic.ATP.Term (fApp, IsTerm(TVarOf, FunOf), vt) -import Data.Logic.ATP.Unif (Unify, unify_literals) +import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Set as Set import Data.String (IsString(..)) @@ -45,14 +45,17 @@ import Test.HUnit hiding (State) -- | Unify complementary literals. -unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2, Unify atom1 atom2, - atom1 ~ AtomOf lit1, atom2 ~ AtomOf lit2, term ~ TermOf atom1, term ~ TermOf atom2, v ~ TVarOf term) => +unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2, + Unify (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 () unify_complements p q = unify_literals p ((.~.) q) -- | Unify and refute a set of disjuncts. -unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term, - atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => +unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, + Unify (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 @@ -65,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, + (JustLiteral lit, Ord lit, HasApply atom, Unify (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 = @@ -78,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, HasSkolem function, Show formula, + (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 @@ -107,7 +110,7 @@ -- Comparison of number of ground instances. -- ------------------------------------------------------------------------- -compare :: (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula, +compare :: (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, Int) @@ -175,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, + (IsFirstOrder formula, Unify (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 = @@ -211,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, +tabrefute :: (IsFirstOrder formula, Unify (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, Pretty formula, HasSkolem function, +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) @@ -285,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, Ord formula, Pretty formula, HasSkolem function, + (IsFirstOrder formula, Unify (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)] 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 @@ -3,6 +3,7 @@ -- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) {-# OPTIONS -Wall #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} @@ -10,7 +11,7 @@ {-# LANGUAGE TypeFamilies #-} module Data.Logic.ATP.Unif - ( Unify(unify) + ( Unify(unify, UTermOf) , unify_terms , unify_literals , unify_atoms @@ -31,31 +32,27 @@ import Data.Logic.ATP.Lib (Failing(Success, Failure)) import Data.Logic.ATP.Lit (IsLiteral, JustLiteral, zipLiterals') import Data.Logic.ATP.Skolem (SkAtom, SkTerm) -import Data.Logic.ATP.Term (IsTerm(..)) +import Data.Logic.ATP.Term (IsTerm(..), IsVariable) import Data.Map.Strict as Map import Data.Maybe (fromMaybe) -- import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<))) import Test.HUnit hiding (State) --- | Main unification procedure. -class TermOf a ~ TermOf b => Unify a b where - unify :: a -> b -> StateT (Map (TVarOf (TermOf a)) (TermOf a)) Failing () - -- ^ Unify the two elements of a pair, collecting variable - -- assignments in the state. - -{- -instance Unify a b => Unify [a] [b] where - unify [] [] = return () - unify (x : xs) (y : ys) = unify x y >> unify xs ys - unify _ _ = fail "unify - list length mismatch" - -instance Unify a b => Unify (Seq a) (Seq b) where - unify xs ys = - case (viewl xs, viewl ys) of - (EmptyL, EmptyL) -> return () - (x :< xs', y :< ys') -> unify x y >> unify xs' ys' - _ -> fail "unify - Seq list length mismatch" --} +-- | Main unification procedure. The result of unification is a +-- mapping of variables to terms, so although we can unify two +-- dissimilar types, they must at least have the same term type (which +-- means the variable type will also match.) The result of unifying +-- the two arguments is added to the state, while failure is signalled +-- in the Failing monad. +-- +-- One might think that Unify should take two type parameters, the +-- types of two values to be unified, but there are instances where a +-- 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 + type UTermOf a + unify :: a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) Failing () unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing () unify_terms = mapM_ (uncurry unify_term_pair) @@ -111,7 +108,7 @@ -- who cares. 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, v ~ TVarOf term) => + Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) Failing () unify_literals f1 f2 = fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2) @@ -119,7 +116,7 @@ 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) + at a1 a2 = Just (unify (a1, a2)) unify_atoms :: (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, @@ -143,8 +140,9 @@ -- where -- app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2) -instance Unify SkAtom SkAtom where - unify = unify_atoms_eq +instance Unify (SkAtom, SkAtom) where + type UTermOf (SkAtom, SkAtom) = TermOf SkAtom + unify = uncurry unify_atoms_eq test01, test02, test03, test04 :: Test test01 = TestCase (assertEqual "Unify test 1"