diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2015, Nick Smallbone + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Nick Smallbone nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,10 @@ +This is twee, a prover for equational problems. + +To install, run cabal install. + +Afterwards, invoke as twee nameofproblem.p. The problem should be in +TPTP format (http://www.tptp.org). You can find a few examples in the +tests directory. All axioms and conjectures must be equations, but you +can freely use types and quantifiers. + +Twee is experimental software, use at your own risk! diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/executable/Main.hs b/executable/Main.hs new file mode 100644 --- /dev/null +++ b/executable/Main.hs @@ -0,0 +1,277 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, CPP, GeneralizedNewtypeDeriving, TypeFamilies, RecordWildCards, FlexibleContexts, UndecidableInstances, NondecreasingIndentation #-} +#include "errors.h" + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative +#endif + +import Control.Monad +import Control.Monad.Trans.State.Strict +import Data.Char +import Data.Either +import Twee hiding (info) +import Twee.Base hiding (char, lookup, (<>)) +import Twee.Rule +import Twee.Utils +import Twee.Queue +import Data.Ord +import qualified Twee.Indexes as Indexes +import qualified Data.Map.Strict as Map +import qualified Twee.KBO as KBO +import qualified Twee.LPO as LPO +import qualified Data.Set as Set +import Data.Reflection +import qualified Data.IntMap as IntMap +import Data.IntMap(IntMap) +import Data.List.Split +import Data.List +import Data.Maybe +import Jukebox.Options +import Jukebox.Toolbox +import Jukebox.Name +import qualified Jukebox.Form as Jukebox +import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term) +import qualified Twee.Label as Label + +parseInitialState :: OptionParser (Twee f) +parseInitialState = + go <$> maxSize <*> general + <*> groundJoin <*> conn <*> set <*> setGoals <*> tracing <*> moreTracing <*> lweight <*> rweight <*> splits <*> cpSetSize <*> mixFIFO <*> mixPrio <*> skipComposite <*> interreduce <*> unsafeInterreduce <*> cancel <*> cancelSize <*> cancelConsts <*> atomicCancellation + where + go maxSize general groundJoin conn set setGoals tracing moreTracing lweight rweight splits cpSetSize mixFIFO mixPrio skipComposite interreduce unsafeInterreduce cancel cancelSize cancelConsts atomicCancellation = + (initialState mixFIFO mixPrio) { + maxSize = maxSize, + cpSplits = splits, + minimumCPSetSize = cpSetSize, + useGeneralSuperpositions = general, + useGroundJoining = groundJoin, + useConnectedness = conn, + useSetJoining = set, + useSetJoiningForGoals = setGoals, + useCancellation = cancel, + maxCancellationSize = cancelSize, + atomicCancellation = atomicCancellation, + unifyConstantsInCancellation = cancelConsts, + useInterreduction = interreduce, + useUnsafeInterreduction = unsafeInterreduce, + skipCompositeSuperpositions = skipComposite, + tracing = tracing, + moreTracing = moreTracing, + lhsWeight = lweight, + rhsWeight = rweight } + maxSize = flag "max-size" ["Maximum critical pair size"] Nothing (Just <$> argNum) + general = not <$> bool "no-general-superpositions" ["Disable considering only general superpositions"] + groundJoin = not <$> bool "no-ground-join" ["Disable ground joinability testing"] + conn = not <$> bool "no-connectedness" ["Disable connectedness testing"] + set = bool "set-join" ["Join by computing set of normal forms"] + setGoals = not <$> bool "no-set-join-goals" ["Disable joining goals by computing set of normal forms"] + tracing = not <$> bool "no-tracing" ["Disable tracing output"] + moreTracing = bool "more-tracing" ["Produce even more tracing output"] + lweight = flag "lhs-weight" ["Weight given to LHS of critical pair (default 2)"] 2 argNum + rweight = flag "rhs-weight" ["Weight given to RHS of critical pair (default 1)"] 1 argNum + splits = flag "split" ["Split CP sets into this many pieces on selection (default 20)"] 20 argNum + cpSetSize = flag "cp-set-minimum" ["Decay CP sets into single CPs when they get this small (default 20)"] 20 argNum + mixFIFO = flag "mix-fifo" ["Take this many CPs at a time from FIFO (default 0)"] 0 argNum + mixPrio = flag "mix-prio" ["Take this many CPs at a time from priority queue (default 10)"] 10 argNum + interreduce = bool "interreduce" ["Enable interreduction of left hand sides"] + unsafeInterreduce = not <$> bool "safe-interreduce" ["Disable some incomplete interreductions"] + cancel = not <$> bool "no-cancellation" ["Disable cancellation"] + cancelSize = flag "max-cancellation-size" ["Maximum size of cancellation laws"] Nothing (Just <$> argNum) + cancelConsts = bool "unify-consts-in-cancellation" ["Allow unification with a constant in cancellation"] + skipComposite = not <$> bool "composite-superpositions" ["Generate composite superpositions"] + atomicCancellation = not <$> bool "compound-cancellation" ["Allow cancellation laws to have non-atomic RHS"] + +data Order = KBO | LPO + +parseOrder :: OptionParser Order +parseOrder = + f <$> + bool "lpo" ["Use lexicographic path ordering instead of KBO"] + where + f False = KBO + f True = LPO + +parsePrecedence :: OptionParser [String] +parsePrecedence = + fmap (splitOn ",") + (flag "precedence" ["List of functions in descending order of precedence"] [] (arg "" "expected a function name" Just)) + +data Constant = + Constant { + conIndex :: Int, + conArity :: Int, + conSize :: Int, + conName :: String } + | Builtin Builtin + +data Builtin = CFalse | CTrue | CEquals deriving (Eq, Ord) + +instance Eq Constant where + x == y = x `compare` y == EQ +instance Ord Constant where + compare Constant{conIndex = x} Constant{conIndex = y} = compare x y + compare Constant{} Builtin{} = LT + compare Builtin{} Constant{} = GT + compare (Builtin x) (Builtin y) = compare x y +instance Sized Constant where + size Constant{conSize = n} = fromIntegral n + size Builtin{} = 0 +instance Arity Constant where + arity Constant{conSize = n} = n + arity (Builtin CEquals) = 2 + arity (Builtin _) = 0 + +instance Pretty Constant where + pPrint Constant{conName = name} = text name + pPrint (Builtin CEquals) = text "$equals" + pPrint (Builtin CTrue) = text "$true" + pPrint (Builtin CFalse) = text "$false" +instance PrettyTerm Constant where + termStyle con@Constant{} + | not (any isAlphaNum (conName con)) = + case conArity con of + 1 -> prefix + 2 -> infixStyle 5 + _ -> uncurried + termStyle _ = uncurried + +instance Given (IntMap Constant) => Numbered Constant where + fromInt 0 = Builtin CFalse + fromInt 1 = Builtin CTrue + fromInt 2 = Builtin CEquals + fromInt n = IntMap.findWithDefault __ (n-3) given + toInt Constant{conIndex = n} = n+3 + toInt (Builtin CFalse) = 0 + toInt (Builtin CTrue) = 1 + toInt (Builtin CEquals) = 2 + +instance (Given Order, Given (IntMap Constant)) => Ordered (Extended Constant) where + lessEq = + case given of + KBO -> KBO.lessEq + LPO -> LPO.lessEq + lessIn = + case given of + KBO -> KBO.lessIn + LPO -> LPO.lessIn + +instance Label.Labelled Jukebox.Function where + cache = functionCache + +{-# NOINLINE functionCache #-} +functionCache :: Label.Cache Jukebox.Function +functionCache = Label.mkCache + +instance Numbered Jukebox.Function where + fromInt n = fromMaybe __ (Label.find n) + toInt = Label.label + +toTwee :: Problem Clause -> ([Equation Jukebox.Function], [Term Jukebox.Function]) +toTwee prob = (lefts eqs, goals) + where + eq Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} = + Left (tm t :=: tm u) + eq Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])} = + Right (tm t :=: tm u) + eq _ = ERROR("Problem is not unit equality") + + eqs = map eq prob + + goals = + case rights eqs of + [] -> [] + [t :=: u] -> [t, u] + _ -> ERROR("Problem is not unit equality") + + tm (Jukebox.Var (Unique x _ _ ::: _)) = + build (var (MkVar (fromIntegral x))) + tm (f :@: ts) = + app f (map tm ts) + +addNarrowing :: + Given (IntMap Constant) => + ([Equation (Extended Constant)], [Term (Extended Constant)]) -> + ([Equation (Extended Constant)], [Term (Extended Constant)]) +addNarrowing (axioms, goals) + | length goals < 2 = (axioms, [app false [], app true []]) + where + false = Function (Builtin CFalse) + true = Function (Builtin CTrue) +addNarrowing (axioms, goals) + | length goals >= 2 && all isGround goals = (axioms, goals) +addNarrowing (axioms, [t, u]) + | otherwise = (axioms ++ equalities, [app false [], app true []]) + where + false = Function (Builtin CFalse) + true = Function (Builtin CTrue) + equals = Function (Builtin CEquals) + + equalities = + [app equals [build (var (MkVar 0)), build (var (MkVar 0))] :=: app true [], + app equals [t, u] :=: app false []] +addNarrowing _ = + ERROR("Don't know how to handle several non-ground goals") + +runTwee :: Twee (Extended Constant) -> Order -> [String] -> Problem Clause -> IO Answer +runTwee state order precedence obligs = do + let (axioms0, goals0) = toTwee obligs + prec c = (isNothing (elemIndex (base c) precedence), + fmap negate (elemIndex (base c) precedence), + negate (occ (toFun c) (axioms0, goals0))) + fs0 = map fromFun (usort (funs (axioms0, goals0))) + fs1 = sortBy (comparing prec) fs0 + fs2 = zipWith (\i (c ::: (FunType args _)) -> Constant i (length args) 1 (show c)) [1..] fs1 + m = IntMap.fromList [(conIndex f, f) | f <- fs2] + m' = Map.fromList (zip fs1 (map Function fs2)) + give m $ give order $ do + let replace = build . mapFun (toFun . flip (Map.findWithDefault __) m' . fromFun) + axioms1 = [replace t :=: replace u | t :=: u <- axioms0] + goals1 = map replace goals0 + (axioms2, goals2) = addNarrowing (axioms1, goals1) + + putStrLn "Axioms:" + mapM_ prettyPrint axioms2 + putStrLn "\nGoals:" + mapM_ prettyPrint goals2 + putStrLn "\nGo!" + + let + identical xs = not (Set.null (foldr1 Set.intersection xs)) + + loop = do + res <- complete1 + goals <- gets goals + when (res && (length goals <= 1 || not (identical goals))) loop + + s = + flip execState (addGoals (map Set.singleton goals2) state) $ do + mapM_ newEquation axioms2 + loop + + rs = map (critical . modelled . peel) (Indexes.elems (labelledRules s)) + + putStrLn "\nFinal rules:" + mapM_ prettyPrint rs + putStrLn "" + + putStrLn (report s) + putStrLn "Normalised goal terms:" + forM_ goals2 $ \t -> + prettyPrint (Rule Oriented t (result (normalise s t))) + + return $ + case () of + _ | identical (goals s) -> Unsatisfiable + | isJust (maxSize s) -> NoAnswer GaveUp + | otherwise -> Satisfiable + +main = do + let twee = Tool "twee" "twee - the Wonderful Equation Engine" "1" "Proves equations." + join . parseCommandLine twee . tool twee $ + greetingBox twee =>> + allFilesBox <*> + (parseProblemBox =>>= + toFofBox =>>= + clausifyBox =>>= + allObligsBox <*> + (runTwee <$> parseInitialState <*> parseOrder <*> parsePrecedence)) diff --git a/src/Twee.hs b/src/Twee.hs new file mode 100644 --- /dev/null +++ b/src/Twee.hs @@ -0,0 +1,982 @@ +-- Knuth-Bendix completion, with lots of exciting tricks for +-- unorientable equations. + +{-# LANGUAGE CPP, TypeFamilies, FlexibleContexts, RecordWildCards, ScopedTypeVariables, UndecidableInstances, StandaloneDeriving, PatternGuards, BangPatterns #-} +module Twee where + +#include "errors.h" +import Twee.Base hiding (empty, lookup) +import Twee.Constraints hiding (funs) +import Twee.Rule +import qualified Twee.Indexes as Indexes +import Twee.Indexes(Indexes, Rated(..)) +import qualified Twee.Index as Index +import Twee.Index(Index, Frozen) +import Twee.Queue hiding (queue) +import Twee.Utils +import Control.Monad +import Data.Maybe +import Data.Ord +import qualified Debug.Trace +import Control.Monad.Trans.State.Strict +import Data.List +import Text.Printf +import qualified Data.Set as Set +import Data.Set(Set) +import Data.Either +import qualified Data.Map.Strict as Map +import Data.Map.Strict(Map) + +-------------------------------------------------------------------------------- +-- Completion engine state. +-------------------------------------------------------------------------------- + +data Twee f = + Twee { + maxSize :: Maybe Int, + labelledRules :: {-# UNPACK #-} !(Indexes (Labelled (Modelled (Critical (Rule f))))), + extraRules :: {-# UNPACK #-} !(Indexes (Rule f)), + cancellationRules :: !(Index (Labelled (CancellationRule f))), + goals :: [Set (Term f)], + totalCPs :: Int, + processedCPs :: Int, + renormaliseAt :: Int, + minimumCPSetSize :: Int, + cpSplits :: Int, + queue :: !(Queue (Mix (Either1 FIFO Heap)) (Passive f)), + useGeneralSuperpositions :: Bool, + useGroundJoining :: Bool, + useConnectedness :: Bool, + useSetJoining :: Bool, + useSetJoiningForGoals :: Bool, + useCancellation :: Bool, + maxCancellationSize :: Maybe Int, + atomicCancellation :: Bool, + unifyConstantsInCancellation :: Bool, + useInterreduction :: Bool, + useUnsafeInterreduction :: Bool, + skipCompositeSuperpositions :: Bool, + tracing :: Bool, + moreTracing :: Bool, + lhsWeight :: Int, + rhsWeight :: Int, + joinStatistics :: Map JoinReason Int } + deriving Show + +initialState :: Int -> Int -> Twee f +initialState mixFIFO mixPrio = + Twee { + maxSize = Nothing, + labelledRules = Indexes.empty, + extraRules = Indexes.empty, + cancellationRules = Index.Nil, + goals = [], + totalCPs = 0, + processedCPs = 0, + renormaliseAt = 50, + minimumCPSetSize = 20, + cpSplits = 20, + queue = empty (emptyMix mixFIFO mixPrio (Left1 emptyFIFO) (Right1 emptyHeap)), + useGeneralSuperpositions = True, + useGroundJoining = True, + useConnectedness = True, + useSetJoining = False, + useSetJoiningForGoals = True, + useInterreduction = False, + useUnsafeInterreduction = True, + useCancellation = True, + atomicCancellation = True, + maxCancellationSize = Nothing, + unifyConstantsInCancellation = False, + skipCompositeSuperpositions = True, + tracing = True, + moreTracing = False, + lhsWeight = 2, + rhsWeight = 1, + joinStatistics = Map.empty } + +addGoals :: [Set (Term f)] -> Twee f -> Twee f +addGoals gs s = s { goals = gs ++ goals s } + +report :: Function f => Twee f -> String +report Twee{..} = + printf "Rules: %d total, %d oriented, %d unoriented, %d permutative, %d weakly oriented. " + (length rs) + (length [ () | Rule Oriented _ _ <- rs ]) + (length [ () | Rule Unoriented _ _ <- rs ]) + (length [ () | (Rule (Permutative _) _ _) <- rs ]) + (length [ () | (Rule (WeaklyOriented _) _ _) <- rs ]) ++ + printf "%d extra. %d historical.\n" + (length (Indexes.elems extraRules)) + n ++ + printf "Critical pairs: %d total, %d processed, %d queued compressed into %d.\n\n" + totalCPs + processedCPs + s + (length (toList queue)) ++ + printf "Critical pairs joined:\n" ++ + concat [printf "%6d %s.\n" n (prettyShow x) | (x, n) <- Map.toList joinStatistics] + where + rs = map (critical . modelled . peel) (Indexes.elems labelledRules) + Label n = nextLabel queue + s = sum (map passiveCount (toList queue)) + +enqueueM :: Function f => Passive f -> State (Twee f) () +enqueueM cps = do + traceM (NewCP cps) + modify' $ \s -> s { + queue = enqueue cps (queue s), + totalCPs = totalCPs s + passiveCount cps } + +reenqueueM :: Function f => Passive f -> State (Twee f) () +reenqueueM cps = do + modify' $ \s -> s { + queue = reenqueue cps (queue s) } + +dequeueM :: Function f => State (Twee f) (Maybe (Passive f)) +dequeueM = + state $ \s -> + case dequeue (queue s) of + Nothing -> (Nothing, s) + Just (x, q) -> (Just x, s { queue = q }) + +newLabelM :: State (Twee f) Label +newLabelM = + state $ \s -> + case newLabel (queue s) of + (l, q) -> (l, s { queue = q }) + +data Modelled a = + Modelled { + model :: Model (ConstantOf a), + positions :: [Int], + modelled :: a } + +instance Eq a => Eq (Modelled a) where x == y = modelled x == modelled y +instance Ord a => Ord (Modelled a) where compare = comparing modelled + +instance (PrettyTerm (ConstantOf a), Pretty a) => Pretty (Modelled a) where + pPrint Modelled{..} = pPrint modelled + +deriving instance (Show a, Show (ConstantOf a)) => Show (Modelled a) + +instance Symbolic a => Symbolic (Modelled a) where + type ConstantOf (Modelled a) = ConstantOf a + + term = term . modelled + termsDL = termsDL . modelled + replace f Modelled{..} = Modelled model positions (replace f modelled) + +-------------------------------------------------------------------------------- +-- Rewriting. +-------------------------------------------------------------------------------- + +instance Rated a => Rated (Labelled a) where + rating = rating . peel + maxRating = maxRating . peel +instance Rated a => Rated (Modelled a) where + rating = rating . modelled + maxRating = maxRating . modelled +instance Rated a => Rated (Critical a) where + rating = rating . critical + maxRating = maxRating . critical +instance Rated (Rule f) where + rating (Rule Oriented _ _) = 0 + rating (Rule WeaklyOriented{} _ _) = 0 + rating _ = 1 + maxRating _ = 1 + +{-# INLINE rulesFor #-} +rulesFor :: Function f => Int -> Twee f -> Frozen (Rule f) +rulesFor n k = + Index.map (critical . modelled . peel) (Indexes.freeze n (labelledRules k)) + +easyRules, rules, allRules :: Function f => Twee f -> Frozen (Rule f) +easyRules k = rulesFor 0 k +rules k = rulesFor 1 k `Index.union` Indexes.freeze 0 (extraRules k) +allRules k = rulesFor 1 k `Index.union` Indexes.freeze 1 (extraRules k) + +normaliseQuickly :: Function f => Twee f -> Term f -> Reduction f +normaliseQuickly s t = normaliseWith (rewrite "simplify" simplifies (easyRules s)) t + +normalise :: Function f => Twee f -> Term f -> Reduction f +normalise s t = normaliseWith (rewrite "reduce" reduces (rules s)) t + +normaliseIn :: Function f => Twee f -> Model f -> Term f -> Reduction f +normaliseIn s model t = + normaliseWith (rewrite "model" (reducesInModel model) (rules s)) t + +normaliseSub :: Function f => Twee f -> Term f -> Term f -> Reduction f +normaliseSub s top t + | useConnectedness s && lessEq t top && isNothing (unify t top) = + normaliseWith (rewrite "sub" (reducesSub top) (rules s)) t + | otherwise = Parallel [] t + +normaliseSkolem :: Function f => Twee f -> Term f -> Reduction f +normaliseSkolem s t = normaliseWith (rewrite "skolem" reducesSkolem (rules s)) t + +reduceCP :: + Function f => + Twee f -> JoinStage -> (Term f -> Term f) -> + Critical (Equation f) -> Either JoinReason (Critical (Equation f)) +reduceCP s stage f (Critical top (t :=: u)) + | t' == u' = Left (Trivial stage) + | subsumed s t' u' = Left (Subsumed stage) + | otherwise = Right (Critical top (t' :=: u')) + where + t' = f t + u' = f u + + subsumed s t u = here || there t u + where + here = + or [ rhs x == u | x <- Index.lookup t rs ] + there (Var x) (Var y) | x == y = True + there (Fun f ts) (Fun g us) | f == g = and (zipWith (subsumed s) (fromTermList ts) (fromTermList us)) + there _ _ = False + rs = allRules s + +data JoinStage = Initial | Simplification | Reducing | Subjoining deriving (Eq, Ord, Show) +data JoinReason = Trivial JoinStage | Subsumed JoinStage | SetJoining | GroundJoined deriving (Eq, Ord, Show) + +instance Pretty JoinStage where + pPrint Initial = text "no rewriting" + pPrint Simplification = text "simplification" + pPrint Reducing = text "reduction" + pPrint Subjoining = text "connectedness testing" + +instance Pretty JoinReason where + pPrint (Trivial stage) = text "joined after" <+> pPrint stage + pPrint (Subsumed stage) = text "subsumed after" <+> pPrint stage + pPrint SetJoining = text "joined with set of normal forms" + pPrint GroundJoined = text "ground joined" + +normaliseCPQuickly, normaliseCPReducing, normaliseCP :: + Function f => + Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f)) +normaliseCPQuickly s cp = + reduceCP s Initial id cp >>= + reduceCP s Simplification (result . normaliseQuickly s) + +normaliseCPReducing s cp = + normaliseCPQuickly s cp >>= + reduceCP s Reducing (result . normalise s) + +normaliseCP s cp@(Critical info _) = + case (cp1, cp2, cp3, cp4) of + (Right cp, Right _, Right _, Right _) -> Right cp + (Right _, Right _, Right _, Left x) -> Left x + (Right _, Right _, Left x, _) -> Left x + (Right _, Left x, _, _) -> Left x + (Left x, _, _, _) -> Left x + where + cp1 = + normaliseCPReducing s cp >>= + reduceCP s Subjoining (result . normaliseSub s (top info)) + + cp2 = + normaliseCPReducing s cp >>= + reduceCP s Subjoining (result . normaliseSub s (flipCP (top info))) . flipCP + + cp3 = setJoin cp + cp4 = setJoin (flipCP cp) + + flipCP :: Symbolic a => a -> a + flipCP t = replace (substList sub) t + where + n = maximum (0:map fromEnum (vars t)) + sub (MkVar x) = var (MkVar (n - x)) + + -- XXX shouldn't this also check subsumption? + setJoin (Critical info (t :=: u)) + | not (useSetJoining s) || + Set.null (norm t `Set.intersection` norm u) = + Right (Critical info (t :=: u)) + | otherwise = + Debug.Trace.traceShow (sep [text "Joined", nest 2 (pPrint (Critical info (t :=: u))), text "to", nest 2 (pPrint v)]) + Left SetJoining + where + norm t + | lessEq t (top info) && isNothing (unify t (top info)) = + normalForms (rewrite "setjoin" (reducesSub (top info)) (rules s)) [t] + | otherwise = Set.singleton t + v = Set.findMin (norm t `Set.intersection` norm u) + +-------------------------------------------------------------------------------- +-- Completion loop. +-------------------------------------------------------------------------------- + +complete :: Function f => State (Twee f) () +complete = do + res <- complete1 + when res complete + +complete1 :: Function f => State (Twee f) Bool +complete1 = do + Twee{..} <- get + let Label n = nextLabel queue + when (n >= renormaliseAt) $ do + normaliseCPs + modify (\s -> s { renormaliseAt = renormaliseAt * 3 `div` 2 }) + + res <- dequeueM + case res of + Just (SingleCP (CP info cp l1 l2)) -> do + res <- consider (cpWeight info) l1 l2 cp + when res renormaliseGoals + return True + Just (ManyCPs (CPs _ l lower upper size rule)) -> do + s <- get + modify (\s@Twee{..} -> s { totalCPs = totalCPs - size }) + + queueCPsSplit reenqueueM lower (l-1) rule + mapM_ (reenqueueM . SingleCP) (toCPs s l l rule) + queueCPsSplit reenqueueM (l+1) upper rule + complete1 + Nothing -> + return False + +renormaliseGoals :: Function f => State (Twee f) () +renormaliseGoals = do + Twee{..} <- get + if useSetJoiningForGoals then + modify $ \s -> s { goals = map (normalForms (rewrite "goal" reduces (rules s)) . Set.toList) goals } + else + modify $ \s -> s { goals = map (Set.fromList . map (result . normaliseWith (rewrite "goal" reduces (rules s))) . Set.toList) goals } + +normaliseCPs :: forall f. Function f => State (Twee f) () +normaliseCPs = do + s@Twee{..} <- get + traceM (NormaliseCPs s) + put s { queue = emptyFrom queue } + forM_ (toList queue) $ \cp -> + case cp of + SingleCP (CP _ cp l1 l2) -> queueCP enqueueM trivial l1 l2 cp + ManyCPs (CPs _ _ lower upper _ rule) -> queueCPs enqueueM lower upper (const ()) rule + modify (\s -> s { totalCPs = totalCPs }) + +consider :: + Function f => + Int -> Label -> Label -> Critical (Equation f) -> State (Twee f) Bool +consider w l1 l2 pair = do + traceM (Consider pair) + modify' (\s -> s { processedCPs = processedCPs s + 1 }) + s <- get + let record reason = modify' (\s -> s { joinStatistics = Map.insertWith (+) reason 1 (joinStatistics s) }) + hard (Trivial Subjoining) = True + hard (Subsumed Subjoining) = True + hard SetJoining = True + hard _ = False + tooBig (Critical _ (t :=: u)) = + case maxSize s of + Nothing -> False + Just sz -> size t > sz || size u > sz + if tooBig pair then return False else + case normaliseCP s pair of + Left reason -> do + record reason + when (hard reason) $ forM_ (map canonicalise (orient (critical pair))) $ \(Rule _ t u0) -> do + s <- get + let u = result (normaliseSub s t u0) + r = rule t u + addExtraRule r + traceM (Joined pair reason) + return False + Right pair | tooBig pair -> + return False + Right pair@(Critical _ eq) + | cancelledWeight s (groundJoinableEq s) eq > w -> do + traceM (Delay pair) + queueCP enqueueM (groundJoinableEq s) l1 l2 pair + return False + Right pair@(Critical _ eq) + | (_, eq') <- bestCancellation s (groundJoinableEq s) eq, + eq /= eq' -> do + traceM (Cancel pair eq') + res <- consider maxBound l1 l2 (Critical noCritInfo eq') + s <- get + queueCP enqueueM (groundJoinableEq s) l1 l2 pair + return res + Right (Critical info eq) -> + fmap or $ forM (map canonicalise (orient eq)) $ \r0@(Rule _ t u0) -> do + s <- get + let u = result (normaliseSub s t u0) + r = rule t u + info' = info { top = t } + case normaliseCP s (Critical info' (t :=: u)) of + Left reason -> do + when (hard reason) $ record reason + addExtraRule r + addExtraRule r0 + return False + Right eq -> + case groundJoin s (branches (And [])) eq of + Right eqs -> do + record GroundJoined + mapM_ (consider maxBound l1 l2) [ eq { critInfo = info' } | eq <- eqs ] + addExtraRule r + addExtraRule r0 + return False + Left model -> do + traceM (NewRule r) + l <- addRule (Modelled model (ruleOverlaps s (lhs r)) (Critical info r)) + queueCPsSplit enqueueM noLabel l (Labelled l r) + interreduce r + return True + +groundJoinableEq :: Function f => Twee f -> Equation f -> Bool +groundJoinableEq s eq = groundJoinable s (Critical noCritInfo eq) + +groundJoinable :: Function f => Twee f -> Critical (Equation f) -> Bool +groundJoinable s pair = + case normaliseCP s pair of + Left _ -> True + Right pair' -> + case groundJoin s (branches (And [])) pair' of + Left _ -> False + Right pairs -> all (groundJoinable s) pairs + +groundJoin :: Function f => + Twee f -> [Branch f] -> Critical (Equation f) -> Either (Model f) [Critical (Equation f)] +groundJoin s ctx r@(Critical info (t :=: u)) = + case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of + ([], instances) -> + let rs = [ subst sub r | sub <- instances ] in + Right (usort (map canonicalise rs)) + (model:_, _) + | not (useGroundJoining s) -> Left model + | isRight (normaliseCP s (Critical info (t' :=: u'))) -> Left model + | otherwise -> + let model1 = optimise model weakenModel (\m -> valid m nt && valid m nu) + model2 = optimise model1 weakenModel (\m -> isLeft (normaliseCP s (Critical info (result (normaliseIn s m t) :=: result (normaliseIn s m u))))) + + diag [] = Or [] + diag (r:rs) = negateFormula r ||| (weaken r &&& diag rs) + weaken (LessEq t u) = Less t u + weaken x = x + ctx' = formAnd (diag (modelToLiterals model2)) ctx in + + trace s (Discharge r model2) $ + groundJoin s ctx' r + where + nt = normaliseIn s model t + nu = normaliseIn s model u + t' = result nt + u' = result nu + +valid :: Function f => Model f -> Reduction f -> Bool +valid model red = all valid1 (steps red) + where + valid1 (rule, sub) = reducesInModel model rule sub + +optimise :: a -> (a -> [a]) -> (a -> Bool) -> a +optimise x f p = + case filter p (f x) of + y:_ -> optimise y f p + _ -> x + +addRule :: Function f => Modelled (Critical (Rule f)) -> State (Twee f) Label +addRule rule = do + l <- newLabelM + modify (\s -> s { labelledRules = Indexes.insert (Labelled l rule) (labelledRules s) }) + modify (addCancellationRule l (critical (modelled rule))) + return l + +addExtraRule :: Function f => Rule f -> State (Twee f) () +addExtraRule rule = do + s <- get + when (extraRuleSafe s rule) $ do + traceM (ExtraRule rule) + modify (\s -> s { extraRules = Indexes.insert rule (extraRules s) }) + +extraRuleSafe :: Function f => Twee f -> Rule f -> Bool +extraRuleSafe s _ | useUnsafeInterreduction s = True +extraRuleSafe s (Rule _ l _) = + null $ do + Index.Match (Rule _ l' _) _ <- Index.matches l (allRules s) + guard (l' `isInstanceOf` l) + +deleteRule :: Function f => Label -> Modelled (Critical (Rule f)) -> State (Twee f) () +deleteRule l rule = do + modify $ \s -> + s { labelledRules = Indexes.delete (Labelled l rule) (labelledRules s), + queue = deleteLabel l (queue s) } + modify (deleteCancellationRule l (critical (modelled rule))) + +data Simplification f = Simplify (Model f) (Modelled (Critical (Rule f))) | Reorient (Modelled (Critical (Rule f))) deriving Show + +instance (Numbered f, PrettyTerm f) => Pretty (Simplification f) where + pPrint (Simplify _ rule) = text "Simplify" <+> pPrint rule + pPrint (Reorient rule) = text "Reorient" <+> pPrint rule + +interreduce :: Function f => Rule f -> State (Twee f) () +interreduce new = do + rules <- gets (\s -> Indexes.elems (labelledRules s)) + forM_ rules $ \(Labelled l old) -> do + s <- get + case reduceWith s l new old of + Nothing -> return () + Just red -> do + traceM (Reduce red new) + case red of + Simplify model rule -> simplifyRule l model rule + Reorient rule@(Modelled _ _ (Critical info (Rule _ t u))) -> + when (useInterreduction s) $ do + deleteRule l rule + consider maxBound noLabel noLabel (Critical info (t :=: u)) + return () + +reduceWith :: Function f => Twee f -> Label -> Rule f -> Modelled (Critical (Rule f)) -> Maybe (Simplification f) +reduceWith s lab new old0@(Modelled model _ (Critical info old@(Rule _ l r))) + | not (isWeak new) && + not (lhs new `isInstanceOf` l) && + not (null (anywhere (tryRule reduces new) l)) = + Just (Reorient old0) + | not (isWeak new) && + not (lhs new `isInstanceOf` l) && + not (oriented (orientation new)) && + not (all isNothing [ match (lhs new) l' | l' <- subterms l ]) && + modelJoinable = + tryGroundJoin + | not (null (anywhere (tryRule reduces new) (rhs old))) = + Just (Simplify model old0) + | not (oriented (orientation old)) && + not (oriented (orientation new)) && + not (lhs new `isInstanceOf` r) && + not (all isNothing [ match (lhs new) r' | r' <- subterms r ]) && + modelJoinable = + tryGroundJoin + | otherwise = Nothing + where + s' = s { labelledRules = Indexes.delete (Labelled lab old0) (labelledRules s) } + modelJoinable = isLeft (normaliseCP s' (Critical info (lm :=: rm))) + lm = result (normaliseIn s' model l) + rm = result (normaliseIn s' model r) + tryGroundJoin = + case groundJoin s' (branches (And [])) (Critical info (l :=: r)) of + Left model' -> + Just (Simplify model' old0) + Right _ -> + Just (Reorient old0) + isWeak (Rule (WeaklyOriented _) _ _) = True + isWeak _ = False + +simplifyRule :: Function f => Label -> Model f -> Modelled (Critical (Rule f)) -> State (Twee f) () +simplifyRule l model r@(Modelled _ positions (Critical info (Rule _ lhs rhs))) = do + modify $ \s -> + s { + labelledRules = + Indexes.insert (Labelled l (Modelled model positions (Critical info (rule lhs (result (normalise s rhs)))))) + (Indexes.delete (Labelled l r) (labelledRules s)) } + modify (deleteCancellationRule l (critical (modelled r))) + modify (addCancellationRule l (critical (modelled r))) + +newEquation :: Function f => Equation f -> State (Twee f) () +newEquation (t :=: u) = do + consider maxBound noLabel noLabel (Critical noCritInfo (t :=: u)) + renormaliseGoals + return () + +noCritInfo :: Function f => CritInfo f +noCritInfo = CritInfo minimalTerm 0 + +-------------------------------------------------------------------------------- +-- Cancellation rules. +-------------------------------------------------------------------------------- + +data CancellationRule f = + CancellationRule { + cr_unified :: [[Term f]], + cr_rule :: {-# UNPACK #-} !(Rule f) } + deriving Show + +instance (Numbered f, PrettyTerm f) => Pretty (CancellationRule f) where + pPrint (CancellationRule tss rule) = + pPrint rule <+> text "cancelling" <+> pPrint tss + +instance Symbolic (CancellationRule f) where + type ConstantOf (CancellationRule f) = f + term (CancellationRule _ rule) = term rule + termsDL (CancellationRule tss rule) = + termsDL rule `mplus` termsDL tss + replace sub (CancellationRule tss rule) = + CancellationRule (replace sub tss) (replace sub rule) + +toCancellationRule :: Function f => Twee f -> Rule f -> Maybe (CancellationRule f) +toCancellationRule _ (Rule Permutative{} _ _) = Nothing +toCancellationRule _ (Rule WeaklyOriented{} _ _) = Nothing +toCancellationRule s (Rule or l r) + | not (null vs) && + (not (atomicCancellation s) || atomic r) = + Just (CancellationRule tss (Rule or' l' r)) + | otherwise = Nothing + where + consts = unifyConstantsInCancellation s + atomic (Var _) = True + atomic (Fun _ Empty) = True + atomic _ = False + + -- Variables that occur on lhs more than once, but not rhs + vs = usort (vars l \\ usort (vars l)) \\ usort (vars r) + cs = usort [ c | consts, Fun c Empty <- subterms l ] + + n = bound l `max` bound r + + l' = build (freshenVars (n + length cs) (singleton l)) + freshenVars !_ Empty = mempty + freshenVars n (Cons (Var x) ts) = + var y `mappend` freshenVars (n+1) ts + where + y = if x `elem` vs then MkVar n else x + freshenVars i (Cons (Fun f Empty) ts) | f `elem` cs = + var (MkVar m) `mappend` freshenVars (i+1) ts + where + m = n + fromMaybe __ (elemIndex f cs) + freshenVars n (Cons (Fun f ts) us) = + fun f (freshenVars (n+1) ts) `mappend` + freshenVars (n+lenList ts+1) us + + tss = + map (map (build . var . snd)) (partitionBy fst pairs) ++ + zipWith (\i c -> [build (con c), build (var (MkVar i))]) [n..] cs + pairs = concat (zipWith f (subterms l) (subterms l')) + where + f (Var x) (Var y) + | x `elem` vs = [(x, y)] + f _ _ = [] + + or' = subst (var . f) or + where + f x = fromMaybe __ (lookup x pairs) + +addCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f +addCancellationRule _ (Rule _ t u) s + | Just n <- maxCancellationSize s, size (t :=: u) > n = s +addCancellationRule l r s = + case toCancellationRule s r of + Nothing -> s + Just c + | moreTracing s && + Debug.Trace.traceShow (sep [text "Adding cancellation rule", nest 2 (pPrint c)]) False -> __ + Just c -> s { + cancellationRules = + Index.insert (Labelled l c) (cancellationRules s) } + +deleteCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f +deleteCancellationRule l r s = + case toCancellationRule s r of + Nothing -> s + Just c -> s { + cancellationRules = + Index.delete (Labelled l c) (cancellationRules s) } + +-------------------------------------------------------------------------------- +-- Critical pairs. +-------------------------------------------------------------------------------- + +data Critical a = + Critical { + critInfo :: CritInfo (ConstantOf a), + critical :: a } + +data CritInfo f = + CritInfo { + top :: Term f, + overlap :: Int } + +instance Eq a => Eq (Critical a) where x == y = critical x == critical y +instance Ord a => Ord (Critical a) where compare = comparing critical + +instance (PrettyTerm (ConstantOf a), Pretty a) => Pretty (Critical a) where + pPrint Critical{..} = pPrint critical + +deriving instance (Show a, Show (ConstantOf a)) => Show (Critical a) +deriving instance Show f => Show (CritInfo f) + +instance Symbolic a => Symbolic (Critical a) where + type ConstantOf (Critical a) = ConstantOf a + + term = term . critical + termsDL Critical{..} = termsDL (critical, critInfo) + replace f Critical{..} = Critical (replace f critInfo) (replace f critical) + +instance Symbolic (CritInfo f) where + type ConstantOf (CritInfo f) = f + + term = __ + termsDL = termsDL . top + replace f CritInfo{..} = CritInfo (replace f top) overlap + +data CPInfo = + CPInfo { + cpWeight :: {-# UNPACK #-} !Int, + cpWeight2 :: {-# UNPACK #-} !Int, + cpAge1 :: {-# UNPACK #-} !Label, + cpAge2 :: {-# UNPACK #-} !Label } + deriving (Eq, Ord, Show) + +data CP f = + CP { + info :: {-# UNPACK #-} !CPInfo, + cp :: {-# UNPACK #-} !(Critical (Equation f)), + l1 :: {-# UNPACK #-} !Label, + l2 :: {-# UNPACK #-} !Label } + deriving Show + +instance Eq (CP f) where x == y = info x == info y +instance Ord (CP f) where compare = comparing info +instance Labels (CP f) where labels x = [l1 x, l2 x] +instance (Numbered f, PrettyTerm f) => Pretty (CP f) where + pPrint = pPrint . cp + +data CPs f = + CPs { + best :: {-# UNPACK #-} !CPInfo, + label :: {-# UNPACK #-} !Label, + lower :: {-# UNPACK #-} !Label, + upper :: {-# UNPACK #-} !Label, + count :: {-# UNPACK #-} !Int, + from :: {-# UNPACK #-} !(Labelled (Rule f)) } + deriving Show + +instance Eq (CPs f) where x == y = best x == best y +instance Ord (CPs f) where compare = comparing best +instance Labels (CPs f) where labels (CPs _ _ _ _ _ (Labelled l _)) = [l] +instance (Numbered f, PrettyTerm f) => Pretty (CPs f) where + pPrint CPs{..} = text "Family of size" <+> pPrint count <+> text "from" <+> pPrint from + +data Passive f = + SingleCP {-# UNPACK #-} !(CP f) + | ManyCPs {-# UNPACK #-} !(CPs f) + deriving (Eq, Show) + +instance Ord (Passive f) where + compare = comparing f + where + f (SingleCP x) = info x + f (ManyCPs x) = best x +instance Labels (Passive f) where + labels (SingleCP x) = labels x + labels (ManyCPs x) = labels x +instance (Numbered f, PrettyTerm f) => Pretty (Passive f) where + pPrint (SingleCP cp) = pPrint cp + pPrint (ManyCPs cps) = pPrint cps + +passiveCount :: Passive f -> Int +passiveCount SingleCP{} = 1 +passiveCount (ManyCPs x) = count x + +data InitialCP f = + InitialCP { + cpId :: (Term f, Label), + cpOK :: Bool, + cpCP :: Labelled (Critical (Equation f)) } + +criticalPairs :: Function f => Twee f -> Label -> Label -> Rule f -> [Labelled (Critical (Equation f))] +criticalPairs s lower upper rule = + criticalPairs1 s (ruleOverlaps s (lhs rule)) rule (map (fmap (critical . modelled)) rules) ++ + [ cp + | Labelled l' (Modelled _ ns (Critical _ old)) <- rules, + cp <- criticalPairs1 s ns old [Labelled l' rule] ] + where + rules = filter (p . labelOf) (Indexes.elems (labelledRules s)) + p l = lower <= l && l <= upper + +ruleOverlaps :: Twee f -> Term f -> [Int] +ruleOverlaps s t = aux 0 Set.empty (singleton t) + where + aux !_ !_ Empty = [] + aux n m (Cons (Var _) t) = aux (n+1) m t + aux n m (ConsSym t@Fun{} u) + | useGeneralSuperpositions s && t `Set.member` m = aux (n+1) m u + | otherwise = n:aux (n+1) (Set.insert t m) u + +overlaps :: [Int] -> Term f -> Term f -> [(Subst f, Int)] +overlaps ns t1 t2@(Fun g _) = go 0 ns (singleton t1) [] + where + go !_ _ !_ _ | False = __ + go _ [] _ rest = rest + go _ _ Empty rest = rest + go n (m:ms) (ConsSym ~t@(Fun f _) u) rest + | m == n && f == g = here ++ go (n+1) ms u rest + | m == n = go (n+1) ms u rest + | otherwise = go (n+1) (m:ms) u rest + where + here = + case unify t t2 of + Nothing -> [] + Just sub -> [(sub, n)] +overlaps _ _ _ = [] + +emitReplacement :: Int -> Term f -> TermList f -> Builder f +emitReplacement n t = aux n + where + aux !_ !_ | False = __ + aux _ Empty = mempty + aux 0 (Cons _ u) = builder t `mappend` builder u + aux n (Cons (Var x) u) = var x `mappend` aux (n-1) u + aux n (Cons t@(Fun f ts) u) + | n < len t = + fun f (aux (n-1) ts) `mappend` builder u + | otherwise = + builder t `mappend` aux (n-len t) u + +criticalPairs1 :: Function f => Twee f -> [Int] -> Rule f -> [Labelled (Rule f)] -> [Labelled (Critical (Equation f))] +criticalPairs1 s ns r rs = do + let b = maximum (0:[ bound t | Labelled _ (Rule _ t _) <- rs ]) + Rule or t u = subst (\(MkVar x) -> var (MkVar (x+b))) r + Labelled l (Rule or' t' u') <- rs + (sub, pos) <- overlaps ns t t' + let left = subst sub u + right = subst sub (build (emitReplacement pos u' (singleton t))) + top = subst sub t + overlap = at pos (singleton t) + + inner = subst sub overlap + osz = size overlap + (size u - size t) + (size u' - size t') + + guard (left /= top && right /= top && left /= right) + when (or /= Oriented) $ guard (not (lessEq top right)) + when (or' /= Oriented) $ guard (not (lessEq top left)) + when (skipCompositeSuperpositions s) $ + guard (null (nested (anywhere (rewrite "prime" simplifies (easyRules s))) inner)) + return (Labelled l (Critical (CritInfo top osz) (left :=: right))) + +queueCP :: + Function f => + (Passive f -> State (Twee f) ()) -> + (Equation f -> Bool) -> Label -> Label -> Critical (Equation f) -> State (Twee f) () +queueCP enq joinable l1 l2 eq = do + s <- get + case toCP s l1 l2 joinable eq of + Nothing -> return () + Just cp -> enq (SingleCP cp) + +queueCPs :: + (Function f, Ord a) => + (Passive f -> State (Twee f) ()) -> + Label -> Label -> (Label -> a) -> Labelled (Rule f) -> State (Twee f) () +queueCPs enq lower upper f rule = do + s <- get + let cps = toCPs s lower upper rule + cpss = partitionBy (f . l2) cps + forM_ cpss $ \xs -> do + if length xs <= minimumCPSetSize s then + mapM_ (enq . SingleCP) xs + else + let best = minimum xs + l1' = minimum (map l1 xs) + l2' = minimum (map l2 xs) in + enq (ManyCPs (CPs (info best) (l2 best) l1' l2' (length xs) rule)) + +queueCPsSplit :: + Function f => + (Passive f -> State (Twee f) ()) -> + Label -> Label -> Labelled (Rule f) -> State (Twee f) () +queueCPsSplit enq l u rule = do + s <- get + let f x = fromIntegral (cpSplits s)*(x-l) `div` (u-l+1) + queueCPs enq l u f rule + +toCPs :: + Function f => + Twee f -> Label -> Label -> Labelled (Rule f) -> [CP f] +toCPs s lower upper (Labelled l rule) = + catMaybes [toCP s l l' trivial eqn | Labelled l' eqn <- criticalPairs s lower upper rule] + +toCP :: + Function f => + Twee f -> Label -> Label -> (Equation f -> Bool) -> Critical (Equation f) -> Maybe (CP f) +toCP s l1 l2 joinable cp = fmap toCP' (norm cp) + where + norm (Critical info (t :=: u)) = do + guard (t /= u) + let t' = result (normaliseQuickly s t) + u' = result (normaliseQuickly s u) + eq' = Critical info (t' :=: u') + guard (t' /= u') + return eq' + + toCP' eq@(Critical info (t :=: u)) = + CP (CPInfo w (-(overlap info)) l2 l1) eq l1 l2 + where + w = cancelledWeight s joinable (t :=: u) + +cancelledWeight :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> Int +cancelledWeight s joinable eq = fst (bestCancellation s joinable eq) + +bestCancellation :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> (Int, Equation f) +bestCancellation s _ eq | not (useCancellation s) = (weight s eq, eq) +bestCancellation s joinable (t :=: u) = (w, best) + where + cs = cancellations s joinable (t :=: u) + ws = zipWith (+) [0..] (map (weight s) cs) + w = minimum ws + best = snd (minimumBy (comparing fst) (zip ws cs)) + +weight, weight' :: Function f => Twee f -> Equation f -> Int +weight s eq = weight' s (order eq) + +weight' s (t :=: u) = + lhsWeight s*size' t + rhsWeight s*size' u + where + size' t = 4*(size t + len t) - length (vars t) - length (nub (vars t)) + +cancellations :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> [Equation f] +cancellations s joinable (t :=: u) = + t :=: u: + case cands of + [] -> [] + _ -> cancellations s joinable (minimumBy (comparing size) cands) + where + cands = + filter (\eq -> size eq < size (t :=: u)) $ + [ t' :=: u' | (sub, t') <- cancel t, let u' = result (normaliseQuickly s (subst sub u)), not (joinable (t' :=: u')) ] ++ + [ t' :=: u' | (sub, u') <- cancel u, let t' = result (normaliseQuickly s (subst sub t)), not (joinable (t' :=: u')) ] + cancel t = do + (i, u) <- zip [0..] (subterms t) + Labelled _ (CancellationRule tss (Rule _ _ u')) <- + Index.lookup u (Index.freeze (cancellationRules s)) + sub <- maybeToList (unifyMany [(t, u) | t:ts <- tss, u <- ts]) + let t' = result (normaliseQuickly s (subst sub (build (emitReplacement i u' (singleton t))))) + return (sub, t') + + unifyMany ps = + unifyList (buildList (map fst ps)) (buildList (map snd ps)) + +-------------------------------------------------------------------------------- +-- Tracing. +-------------------------------------------------------------------------------- + +data Event f = + NewRule (Rule f) + | ExtraRule (Rule f) + | NewCP (Passive f) + | Reduce (Simplification f) (Rule f) + | Consider (Critical (Equation f)) + | Joined (Critical (Equation f)) JoinReason + | Delay (Critical (Equation f)) + | Cancel (Critical (Equation f)) (Equation f) + | Discharge (Critical (Equation f)) (Model f) + | NormaliseCPs (Twee f) + +trace :: Function f => Twee f -> Event f -> a -> a +trace Twee{..} (NewRule rule) = traceIf tracing (hang (text "New rule") 2 (pPrint rule)) +trace Twee{..} (ExtraRule rule) = traceIf tracing (hang (text "Extra rule") 2 (pPrint rule)) +trace Twee{..} (NewCP cp) = traceIf moreTracing (hang (text "Critical pair") 2 (pPrint cp)) +trace Twee{..} (Reduce red rule) = traceIf tracing (sep [pPrint red, nest 2 (text "using"), nest 2 (pPrint rule)]) +trace Twee{..} (Consider eq) = traceIf moreTracing (sep [text "Considering", nest 2 (pPrint eq), text "under", nest 2 (pPrint (top (critInfo eq)))]) +trace Twee{..} (Joined eq reason) = traceIf moreTracing (sep [text "Joined", nest 2 (pPrint eq), text "under", nest 2 (pPrint (top (critInfo eq))), text "by", nest 2 (pPrint reason)]) +trace Twee{..} (Delay eq) = traceIf moreTracing (sep [text "Delaying", nest 2 (pPrint eq)]) +trace Twee{..} (Cancel eq eq') = traceIf tracing (sep [text "Cancelled", nest 2 (pPrint eq), text "into", nest 2 (pPrint eq')]) +trace Twee{..} (Discharge eq fs) = traceIf tracing (sep [text "Discharge", nest 2 (pPrint eq), text "under", nest 2 (pPrint fs)]) +trace Twee{..} (NormaliseCPs s) = traceIf tracing (text "" $$ text "Normalising unprocessed critical pairs." $$ text (report s) $$ text "") + +traceM :: Function f => Event f -> State (Twee f) () +traceM x = do + s <- get + trace s x (return ()) + +traceIf :: Bool -> Doc -> a -> a +traceIf True x = Debug.Trace.trace (show x) +traceIf False _ = id diff --git a/src/Twee/Array.hs b/src/Twee/Array.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Array.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE CPP #-} +module Twee.Array where + +#include "errors.h" +import qualified Data.Primitive as P +import Control.Monad.ST +import Data.List + +-- Zero-indexed dynamic arrays. +-- Optimised for lookup. Modification is slow. +data Array a = + Array { + arraySize :: {-# UNPACK #-} !Int, + arrayContents :: {-# UNPACK #-} !(P.Array a) } + +class Default a where def :: a + +toList :: Array a -> [(Int, a)] +toList arr = + [ (i, x) + | i <- [0..arraySize arr-1], + let x = P.indexArray (arrayContents arr) i ] + +instance Show a => Show (Array a) where + show arr = + "{" ++ + intercalate ", " + [ show i ++ "->" ++ show x + | (i, x) <- toList arr ] ++ + "}" + +newArray :: Default a => Array a +newArray = runST $ do + marr <- P.newArray 0 def + arr <- P.unsafeFreezeArray marr + return (Array 0 arr) + +{-# INLINE (!) #-} +(!) :: Default a => Array a -> Int -> a +arr ! n + | 0 <= n && n < arraySize arr = + P.indexArray (arrayContents arr) n + | otherwise = def + +{-# INLINEABLE update #-} +update :: Default a => Int -> a -> Array a -> Array a +update n x arr = runST $ do + let size = arraySize arr `max` (n+1) + marr <- P.newArray size def + P.copyArray marr 0 (arrayContents arr) 0 (arraySize arr) + P.writeArray marr n x + arr' <- P.unsafeFreezeArray marr + return (Array size arr') diff --git a/src/Twee/Base.hs b/src/Twee/Base.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Base.hs @@ -0,0 +1,187 @@ +{-# LANGUAGE TypeSynonymInstances, TypeFamilies, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, CPP, ConstraintKinds, UndecidableInstances, DeriveFunctor, StandaloneDeriving #-} +module Twee.Base( + Symbolic(..), terms, subst, TermOf, TermListOf, SubstOf, BuilderOf, FunOf, + vars, isGround, funs, occ, canonicalise, + Minimal(..), minimalTerm, isMinimal, + Skolem(..), Arity(..), Sized(..), Ordered(..), Strictness(..), Function, Extended(..), extended, unextended, + module Twee.Term, module Twee.Pretty) where + +#include "errors.h" +import Prelude hiding (lookup) +import Control.Monad +import qualified Data.DList as DList +import Twee.Term hiding (subst, canonicalise) +import qualified Twee.Term as Term +import Twee.Pretty +import Twee.Constraints hiding (funs) +import Data.DList(DList) + +-- Generalisation of term functionality to things that contain terms. +class Symbolic a where + type ConstantOf a + + term :: a -> TermOf a + termsDL :: a -> DList (TermListOf a) + replace :: (TermListOf a -> BuilderOf a) -> a -> a + +terms :: Symbolic a => a -> [TermListOf a] +terms = DList.toList . termsDL + +{-# INLINE subst #-} +subst :: (Symbolic a, Substitution (ConstantOf a) s) => s -> a -> a +subst sub x = replace (substList sub) x + +type TermOf a = Term (ConstantOf a) +type TermListOf a = TermList (ConstantOf a) +type SubstOf a = Subst (ConstantOf a) +type BuilderOf a = Builder (ConstantOf a) +type FunOf a = Fun (ConstantOf a) + +instance Symbolic (Term f) where + type ConstantOf (Term f) = f + term = id + termsDL = return . singleton + replace f = build . f . singleton + +instance Symbolic (TermList f) where + type ConstantOf (TermList f) = f + term = __ + termsDL = return + replace f = buildList . f + +instance (ConstantOf a ~ ConstantOf b, + Symbolic a, Symbolic b) => Symbolic (a, b) where + type ConstantOf (a, b) = ConstantOf a + term (x, _) = term x + termsDL (x, y) = termsDL x `mplus` termsDL y + replace f (x, y) = (replace f x, replace f y) + +instance (ConstantOf a ~ ConstantOf b, + ConstantOf a ~ ConstantOf c, + Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c) where + type ConstantOf (a, b, c) = ConstantOf a + term (x, _, _) = term x + termsDL (x, y, z) = termsDL x `mplus` termsDL y `mplus` termsDL z + replace f (x, y, z) = (replace f x, replace f y, replace f z) + +instance Symbolic a => Symbolic [a] where + type ConstantOf [a] = ConstantOf a + term _ = __ + termsDL = msum . map termsDL + replace f = map (replace f) + +{-# INLINE vars #-} +vars :: Symbolic a => a -> [Var] +vars x = [ v | t <- DList.toList (termsDL x), Var v <- subtermsList t ] + +{-# INLINE isGround #-} +isGround :: Symbolic a => a -> Bool +isGround = null . vars + +{-# INLINE funs #-} +funs :: Symbolic a => a -> [FunOf a] +funs x = [ f | t <- DList.toList (termsDL x), Fun f _ <- subtermsList t ] + +{-# INLINE occ #-} +occ :: Symbolic a => FunOf a -> a -> Int +occ x t = length (filter (== x) (funs t)) + +canonicalise :: Symbolic a => a -> a +canonicalise t = replace (Term.substList sub) t + where + sub = Term.canonicalise (DList.toList (termsDL t)) + +isMinimal :: (Numbered f, Minimal f) => Term f -> Bool +isMinimal (Fun f Empty) | f == minimal = True +isMinimal _ = False + +minimalTerm :: (Numbered f, Minimal f) => Term f +minimalTerm = build (con minimal) + +class Skolem f where + skolem :: Var -> f + +instance (Numbered f, Skolem f) => Skolem (Fun f) where + skolem = toFun . skolem + +class Arity f where + arity :: f -> Int + +instance (Numbered f, Arity f) => Arity (Fun f) where + arity = arity . fromFun + +class Sized a where + size :: a -> Int + +instance (Sized f, Numbered f) => Sized (Fun f) where + size = size . fromFun + +instance (Sized f, Numbered f) => Sized (TermList f) where + size = aux 0 + where + aux n Empty = n + aux n (ConsSym (Fun f _) t) = aux (n+size f) t + aux n (Cons (Var _) t) = aux (n+1) t + +instance (Sized f, Numbered f) => Sized (Term f) where + size = size . singleton + +class (Numbered f, Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f) => Function f +instance (Numbered f, Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f) => Function f + +data Extended f = + Minimal + | Skolem Int + | Function f + deriving (Eq, Ord, Show, Functor) + +instance Minimal (Extended f) where + minimal = Minimal + +instance Skolem (Extended f) where + skolem (MkVar x) = Skolem x + +instance Numbered f => Numbered (Extended f) where + fromInt 0 = Minimal + fromInt n + | odd n = Skolem ((n-1) `div` 2) + | otherwise = Function (fromInt ((n-2) `div` 2)) + + toInt Minimal = 0 + toInt (Skolem n) = 2*n+1 + toInt (Function f) = 2*toInt f+2 + +instance Pretty f => Pretty (Extended f) where + pPrintPrec _ _ Minimal = text "⊥" + pPrintPrec _ _ (Skolem n) = text "sk" <> pPrint n + pPrintPrec l p (Function f) = pPrintPrec l p f + +instance PrettyTerm f => PrettyTerm (Extended f) where + termStyle (Function f) = termStyle f + termStyle _ = uncurried + +instance Sized f => Sized (Extended f) where + size (Function f) = size f + size _ = 1 + +instance Arity f => Arity (Extended f) where + arity (Function f) = arity f + arity _ = 0 + +{-# INLINEABLE extended #-} +extended :: Numbered f => TermList f -> Builder (Extended f) +extended Empty = mempty +extended (Cons (Var x) ts) = var x `mappend` extended ts +extended (Cons (Fun f ts) us) = + fun (toFun (Function (fromFun f))) (extended ts) `mappend` + extended us + +{-# INLINEABLE unextended #-} +unextended :: Numbered f => TermList (Extended f) -> Builder f +unextended Empty = mempty +unextended (Cons (Var x) ts) = var x `mappend` unextended ts +unextended (Cons (Fun f ts) us) = + case fromFun f of + Function g -> fun (toFun g) (unextended ts) `mappend` unextended us + Minimal -> var (MkVar 0) `mappend` unextended us + Skolem n -> var (MkVar n) `mappend` unextended us diff --git a/src/Twee/Constraints.hs b/src/Twee/Constraints.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Constraints.hs @@ -0,0 +1,301 @@ +{-# LANGUAGE TypeFamilies, CPP, FlexibleContexts, UndecidableInstances, StandaloneDeriving, RecordWildCards, GADTs, ScopedTypeVariables, PatternGuards, PatternSynonyms #-} +module Twee.Constraints where + +#include "errors.h" +--import Twee.Base hiding (equals, Term, pattern Fun, pattern Var, lookup, funs) +import qualified Twee.Term as Flat +import qualified Data.Map.Strict as Map +import Twee.Pretty hiding (equals) +import Twee.Utils +import Data.Maybe +import Data.List +import Data.Function +import Data.Graph +import Data.Map.Strict(Map) +import Data.Ord +import Twee.Term hiding (lookup) + +data Atom f = Constant (Fun f) | Variable Var deriving Show +deriving instance Eq (Fun f) => Eq (Atom f) +deriving instance Ord (Fun f) => Ord (Atom f) + +{-# INLINE atoms #-} +atoms :: Term f -> [Atom f] +atoms t = aux (singleton t) + where + aux Empty = [] + aux (Cons (Fun f Empty) t) = Constant f:aux t + aux (Cons (Var x) t) = Variable x:aux t + aux (ConsSym _ t) = aux t + +toTerm :: Atom f -> Term f +toTerm (Constant f) = build (con f) +toTerm (Variable x) = build (var x) + +fromTerm :: Flat.Term f -> Maybe (Atom f) +fromTerm (Fun f Empty) = Just (Constant f) +fromTerm (Var x) = Just (Variable x) +fromTerm _ = Nothing + +instance (Numbered f, PrettyTerm f) => Pretty (Atom f) where + pPrint = pPrint . toTerm + +data Formula f = + Less (Atom f) (Atom f) + | LessEq (Atom f) (Atom f) + | And [Formula f] + | Or [Formula f] + deriving Show +deriving instance Eq (Fun f) => Eq (Formula f) +deriving instance Ord (Fun f) => Ord (Formula f) + +instance (Numbered f, PrettyTerm f) => Pretty (Formula f) where + pPrintPrec _ _ (Less t u) = hang (pPrint t <+> text "<") 2 (pPrint u) + pPrintPrec _ _ (LessEq t u) = hang (pPrint t <+> text "<=") 2 (pPrint u) + pPrintPrec _ _ (And []) = text "true" + pPrintPrec _ _ (Or []) = text "false" + pPrintPrec l p (And xs) = + pPrintParen (p > 10) + (fsep (punctuate (text " &") (nest_ (map (pPrintPrec l 11) xs)))) + where + nest_ (x:xs) = x:map (nest 2) xs + nest_ [] = __ + pPrintPrec l p (Or xs) = + pPrintParen (p > 10) + (fsep (punctuate (text " |") (nest_ (map (pPrintPrec l 11) xs)))) + where + nest_ (x:xs) = x:map (nest 2) xs + nest_ [] = __ + +negateFormula :: Formula f -> Formula f +negateFormula (Less t u) = LessEq u t +negateFormula (LessEq t u) = Less u t +negateFormula (And ts) = Or (map negateFormula ts) +negateFormula (Or ts) = And (map negateFormula ts) + +conj forms + | false `elem` forms' = false + | otherwise = + case forms' of + [x] -> x + xs -> And xs + where + flatten (And xs) = xs + flatten x = [x] + forms' = filter (/= true) (usort (concatMap flatten forms)) +disj forms + | true `elem` forms' = true + | otherwise = + case forms' of + [x] -> x + xs -> Or xs + where + flatten (Or xs) = xs + flatten x = [x] + forms' = filter (/= false) (usort (concatMap flatten forms)) + +x &&& y = conj [x, y] +x ||| y = disj [x, y] +true = And [] +false = Or [] + +data Branch f = + -- Branches are kept normalised wrt equals + Branch { + funs :: [Fun f], + less :: [(Atom f, Atom f)], + equals :: [(Atom f, Atom f)] } -- greatest atom first +deriving instance Eq (Fun f) => Eq (Branch f) +deriving instance Ord (Fun f) => Ord (Branch f) + +instance (Numbered f, PrettyTerm f) => Pretty (Branch f) where + pPrint Branch{..} = + braces $ fsep $ punctuate (text ",") $ + [pPrint x <+> text "<" <+> pPrint y | (x, y) <- less ] ++ + [pPrint x <+> text "=" <+> pPrint y | (x, y) <- equals ] + +trueBranch :: Branch f +trueBranch = Branch [] [] [] + +norm :: Eq f => Branch f -> Atom f -> Atom f +norm Branch{..} x = fromMaybe x (lookup x equals) + +contradictory :: (Numbered f, Minimal f, Ord f) => Branch f -> Bool +contradictory Branch{..} = + or [f == minimal | (_, Constant f) <- less] || + or [f /= g | (Constant f, Constant g) <- equals] || + any cyclic (stronglyConnComp + [(x, x, [y | (x', y) <- less, x == x']) | x <- usort (map fst less)]) + where + cyclic (AcyclicSCC _) = False + cyclic (CyclicSCC _) = True + +formAnd :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f] -> [Branch f] +formAnd f bs = usort (bs >>= add f) + where + add (Less t u) b = addLess t u b + add (LessEq t u) b = addLess t u b ++ addEquals t u b + add (And []) b = [b] + add (And (f:fs)) b = add f b >>= add (And fs) + add (Or fs) b = usort (concat [ add f b | f <- fs ]) + +branches :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f] +branches x = aux [x] + where + aux [] = [Branch [] [] []] + aux (And xs:ys) = aux (xs ++ ys) + aux (Or xs:ys) = usort $ concat [aux (x:ys) | x <- xs] + aux (Less t u:xs) = usort $ concatMap (addLess t u) (aux xs) + aux (LessEq t u:xs) = + usort $ + concatMap (addLess t u) (aux xs) ++ + concatMap (addEquals u t) (aux xs) + +addLess :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f] +addLess _ (Constant min) _ | min == minimal = [] +addLess (Constant min) _ b | min == minimal = [b] +addLess t0 u0 b@Branch{..} = + filter (not . contradictory) + [addTerm t (addTerm u b{less = usort ((t, u):less)})] + where + t = norm b t0 + u = norm b u0 + +addEquals :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f] +addEquals t0 u0 b@Branch{..} + | t == u || (t, u) `elem` equals = [b] + | otherwise = + filter (not . contradictory) + [addTerm t (addTerm u b { + equals = usort $ (t, u):[(x', y') | (x, y) <- equals, let (y', x') = sort2 (sub x, sub y), x' /= y'], + less = usort $ [(sub x, sub y) | (x, y) <- less] })] + where + sort2 (x, y) = (min x y, max x y) + (u, t) = sort2 (norm b t0, norm b u0) + + sub x + | x == t = u + | otherwise = x + +addTerm :: (Numbered f, Minimal f, Ord f) => Atom f -> Branch f -> Branch f +addTerm (Constant f) b + | f `notElem` funs b = + b { + funs = f:funs b, + less = [ (Constant f, Constant g) | g <- funs b, f < g ] ++ + [ (Constant g, Constant f) | g <- funs b, g < f ] ++ less b } +addTerm _ b = b + +newtype Model f = Model (Map (Atom f) (Int, Int)) + deriving Show +-- Representation: map from atom to (major, minor) +-- x < y if major x < major y +-- x <= y if major x = major y and minor x < minor y + +instance (Numbered f, PrettyTerm f) => Pretty (Model f) where + pPrint (Model m) + | Map.size m <= 1 = text "empty" + | otherwise = fsep (go (sortBy (comparing snd) (Map.toList m))) + where + go [(x, _)] = [pPrint x] + go ((x, (i, _)):xs@((_, (j, _)):_)) = + (pPrint x <+> text rel):go xs + where + rel = if i == j then "<=" else "<" + +modelToLiterals :: Model f -> [Formula f] +modelToLiterals (Model m) = go (sortBy (comparing snd) (Map.toList m)) + where + go [] = [] + go [_] = [] + go ((x, (i, _)):xs@((y, (j, _)):_)) = + rel x y:go xs + where + rel = if i == j then LessEq else Less + +modelFromOrder :: (Numbered f, Minimal f, Ord f) => [Atom f] -> Model f +modelFromOrder xs = + Model (Map.fromList [(x, (i, i)) | (x, i) <- zip xs [0..]]) + +weakenModel :: Ord (Fun f) => Model f -> [Model f] +weakenModel (Model m) = + [ Model (Map.delete x m) | x <- Map.keys m ] ++ + [ Model (Map.fromList xs) + | xs <- glue (sortBy (comparing snd) (Map.toList m)), + all ok (groupBy ((==) `on` (fst . snd)) xs) ] + where + glue [] = [] + glue [_] = [] + glue (a@(_x, (i1, j1)):b@(y, (i2, _)):xs) = + [ (a:(y, (i1, j1+1)):xs) | i1 < i2 ] ++ + map (a:) (glue (b:xs)) + + -- We must never make two constants equal + ok xs = length [x | (Constant x, _) <- xs] <= 1 + +varInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Var -> Bool +varInModel (Model m) x = Variable x `Map.member` m + +varGroups :: (Numbered f, Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))] +varGroups (Model m) = filter nonempty (go minimal (map fst (sortBy (comparing snd) (Map.toList m)))) + where + go f xs = + case span isVariable xs of + (_, []) -> [(f, map unVariable xs, Nothing)] + (ys, Constant g:zs) -> + (f, map unVariable ys, Just g):go g zs + isVariable (Constant _) = False + isVariable (Variable _) = True + unVariable (Variable x) = x + nonempty (_, [], _) = False + nonempty _ = True + +class Minimal a where + minimal :: a + +instance (Numbered f, Minimal f) => Minimal (Fun f) where + minimal = toFun minimal + +{-# INLINE lessEqInModel #-} +lessEqInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Atom f -> Atom f -> Maybe Strictness +lessEqInModel (Model m) x y + | Just (a, _) <- Map.lookup x m, + Just (b, _) <- Map.lookup y m, + a < b = Just Strict + | Just a <- Map.lookup x m, + Just b <- Map.lookup y m, + a < b = Just Nonstrict + | x == y = Just Nonstrict + | Constant a <- x, Constant b <- y, a < b = Just Strict + | Constant a <- x, a == minimal = Just Nonstrict + | otherwise = Nothing + +solve :: (Numbered f, Minimal f, Ord f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f) +solve xs branch@Branch{..} + | null equals && not (all true less) = + ERROR("Model " ++ prettyShow model ++ " is not a model of " ++ prettyShow branch ++ " (edges = " ++ prettyShow edges ++ ", vs = " ++ prettyShow vs ++ ")") + | null equals = Left model + | otherwise = Right sub + where + sub = fromMaybe __ . flattenSubst $ + [(x, toTerm y) | (Variable x, y) <- equals] ++ + [(y, toTerm x) | (x@Constant{}, Variable y) <- equals] + vs = Constant minimal:reverse (flattenSCCs (stronglyConnComp edges)) + edges = [(x, x, [y | (x', y) <- less', x == x']) | x <- as] + less' = less ++ [(Constant x, Constant y) | Constant x <- as, Constant y <- as, x < y] + as = usort $ xs ++ map fst less ++ map snd less + model = modelFromOrder vs + true (t, u) = lessEqInModel model t u == Just Strict + +class Ord f => Ordered f where + orientTerms :: Term f -> Term f -> Maybe Ordering + orientTerms t u + | t == u = Just EQ + | lessEq t u = Just LT + | lessEq u t = Just GT + | otherwise = Nothing + + lessEq :: Term f -> Term f -> Bool + lessIn :: Model f -> Term f -> Term f -> Maybe Strictness + +data Strictness = Strict | Nonstrict deriving (Eq, Show) diff --git a/src/Twee/Index.hs b/src/Twee/Index.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Index.hs @@ -0,0 +1,180 @@ +-- Term indexing (perfect discrimination trees). +{-# LANGUAGE BangPatterns, CPP, TypeFamilies, RecordWildCards #-} +-- We get some bogus warnings because of pattern synonyms. +{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} +{-# OPTIONS_GHC -funfolding-creation-threshold=1000000 -funfolding-use-threshold=1000000 #-} +module Twee.Index where + +#include "errors.h" +import qualified Prelude +import Prelude hiding (filter, map, null) +import Twee.Base hiding (var, fun, empty, vars, size) +import qualified Twee.Term as Term +import Twee.Array +import qualified Data.List as List +import Data.Maybe + +data Index a = + Index { + size :: {-# UNPACK #-} !Int, + here :: [Entry a], + fun :: {-# UNPACK #-} !(Array (Index a)), + var :: !(Index a) } | + Singleton { + key :: {-# UNPACK #-} !(TermListOf a), + value :: {-# UNPACK #-} !(Entry a) } | + Nil + deriving Show + +instance Default (Index a) where def = Nil + +data Entry a = + Entry { + e_key :: {-# UNPACK #-} !(TermOf a), + e_value :: a } + deriving (Eq, Show) + +{-# INLINE null #-} +null :: Index a -> Bool +null Nil = True +null _ = False + +{-# INLINEABLE singleton #-} +singleton :: Symbolic a => a -> Index a +singleton x = Singleton (Term.singleton t) (Entry t x) + where + t = term x + +{-# INLINEABLE insert #-} +insert :: Symbolic a => a -> Index a -> Index a +insert x0 !idx = aux (Term.singleton t) idx + where + aux t Nil = Singleton t x + aux t (Singleton u x) = aux t (expand u x) + aux Empty idx@Index{..} = idx { size = 0, here = x:here } + aux t@(ConsSym (Fun (MkFun f) _) u) idx = + idx { + size = lenList t `min` size idx, + fun = update f idx' (fun idx) } + where + idx' = aux u (fun idx ! f) + aux t@(ConsSym (Var _) u) idx = + idx { + size = lenList t `min` size idx, + var = aux u (var idx) } + t = term x0 + x = Entry t x0 + +{-# INLINE expand #-} +expand :: TermListOf a -> Entry a -> Index a +expand Empty x = Index 0 [x] newArray Nil +expand (ConsSym s t) x = + Index (1+lenList t) [] fun var + where + (fun, var) = + case s of + Fun (MkFun f) _ -> + (update f (Singleton t x) newArray, Nil) + Var _ -> + (newArray, Singleton t x) + +{-# INLINEABLE delete #-} +delete :: (Eq a, Symbolic a) => a -> Index a -> Index a +delete x0 !idx = aux (Term.singleton t) idx + where + aux _ Nil = Nil + aux t idx@(Singleton u y) + | t == u && x == y = Nil + | otherwise = idx + aux Empty idx = idx { here = List.delete x (here idx) } + aux (ConsSym (Fun (MkFun f) _) t) idx = + idx { fun = update f (aux t (fun idx ! f)) (fun idx) } + aux (ConsSym (Var _) t) idx = + idx { var = aux t (var idx) } + t = term x0 + x = Entry t x0 + +{-# INLINEABLE elem #-} +elem :: (Eq a, Symbolic a) => a -> Index a -> Bool +elem x0 !idx = aux (Term.singleton t) idx + where + aux _ Nil = False + aux t (Singleton u y) + | t == u && x == y = True + | otherwise = False + aux Empty idx = List.elem x (here idx) + aux (ConsSym (Fun (MkFun f) _) t) idx = + aux t (fun idx ! f) + aux (ConsSym (Var _) t) idx = aux t (var idx) + t = term x0 + x = Entry t x0 + +data Match a = + Match { + matchResult :: a, + matchSubst :: SubstOf a } + +newtype Frozen a = Frozen { matchesList_ :: TermListOf a -> [Match a] } + +matchesList :: TermListOf a -> Frozen a -> [Match a] +matchesList = flip matchesList_ + +{-# INLINEABLE lookup #-} +lookup :: Symbolic a => TermOf a -> Frozen a -> [a] +lookup t idx = [subst sub x | Match x sub <- matches t idx] + +{-# INLINE matches #-} +matches :: TermOf a -> Frozen a -> [Match a] +matches t idx = matchesList (Term.singleton t) idx + +freeze :: Index a -> Frozen a +freeze idx = Frozen $ \t -> find t idx [] + +find :: TermListOf a -> Index a -> [Match a] -> [Match a] +find t idx xs = aux t idx xs + where + aux !_ !_ _ | False = __ + aux _ Nil rest = rest + aux t Index{size = size} rest + | lenList t < size = rest + aux Empty Index{here = here} rest = {-# SCC "try_here" #-} try here rest + aux t (Singleton u x) rest + | isJust (matchList u t) = {-# SCC "try_singleton" #-} try [x] rest + | otherwise = rest + aux t@(ConsSym (Fun (MkFun n) _) ts) Index{fun = fun, var = var} rest = + case var of + Nil -> aux ts (fun ! n) rest + _ -> aux ts (fun ! n) (aux us var rest) + where + Cons _ us = t + aux (Cons _ ts) Index{var = var} rest = aux ts var rest + + {-# INLINE try #-} + try [] rest = rest + try xs rest = + {-# SCC "try" #-} + [ Match x sub + | Entry u x <- xs, + sub <- maybeToList (matchList (Term.singleton u) t) ] ++ + rest + +elems :: Index a -> [a] +elems Nil = [] +elems (Singleton _ x) = [e_value x] +elems idx = + Prelude.map e_value (here idx) ++ + concatMap elems (Prelude.map snd (toList (fun idx))) ++ + elems (var idx) + +{-# INLINE map #-} +map :: (ConstantOf a ~ ConstantOf b) => (a -> b) -> Frozen a -> Frozen b +map f (Frozen matches) = Frozen $ \t -> [Match (f x) sub | Match x sub <- matches t] + +{-# INLINE filter #-} +filter :: (a -> Bool) -> Frozen a -> Frozen a +filter p (Frozen matches) = Frozen $ \t -> + [ m | m@(Match x _) <- matches t, p x ] + +{-# INLINE union #-} +union :: Frozen a -> Frozen a -> Frozen a +union (Frozen f1) (Frozen f2) = Frozen $ \t -> f1 t ++ f2 t diff --git a/src/Twee/Indexes.hs b/src/Twee/Indexes.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Indexes.hs @@ -0,0 +1,44 @@ +-- Term indexing, where the inserted values can be given categories. +{-# LANGUAGE CPP, TypeFamilies, ScopedTypeVariables #-} +module Twee.Indexes where + +#include "errors.h" +import Twee.Base hiding (empty) +import qualified Twee.Index as Index +import Twee.Index(Index) +import Data.Array + +class Rated a where + rating :: a -> Int + maxRating :: a -> Int + +newtype Indexes a = + Indexes { + unIndexes :: Array Int (Index a) } + deriving Show + +{-# INLINE empty #-} +empty :: forall a. Rated a => Indexes a +empty = Indexes (listArray (0, maxRating (undefined :: a)) (repeat Index.Nil)) + +{-# INLINE singleton #-} +singleton :: (Symbolic a, Rated a) => a -> Indexes a +singleton x = insert x empty + +{-# INLINE insert #-} +insert :: forall a. (Symbolic a, Rated a) => a -> Indexes a -> Indexes a +insert x (Indexes idxs) = + Indexes (idxs // [(i, Index.insert x (idxs ! i)) | i <- [rating x..maxRating (undefined :: a)]]) + +{-# INLINE delete #-} +delete :: forall a. (Eq a, Symbolic a, Rated a) => a -> Indexes a -> Indexes a +delete x (Indexes idxs) = + Indexes (idxs // [(i, Index.delete x (idxs ! i)) | i <- [rating x..maxRating (undefined :: a)]]) + +{-# INLINE freeze #-} +freeze :: Int -> Indexes a -> Index.Frozen a +freeze n (Indexes idxs) = Index.freeze (idxs ! n) + +{-# INLINE elems #-} +elems :: forall a. Rated a => Indexes a -> [a] +elems (Indexes idxs) = Index.elems (idxs ! maxRating (undefined :: a)) diff --git a/src/Twee/KBO.hs b/src/Twee/KBO.hs new file mode 100644 --- /dev/null +++ b/src/Twee/KBO.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE CPP, PatternGuards #-} +module Twee.KBO where + +#include "errors.h" +import Twee.Base hiding (lessEq, lessIn) +import Data.List +import Twee.Constraints hiding (lessEq, lessIn) +import qualified Data.Map.Strict as Map +import Data.Map.Strict(Map) +import Data.Maybe +import Control.Monad + +lessEq :: Function f => Term f -> Term f -> Bool +lessEq (Fun f Empty) _ | f == minimal = True +lessEq (Var x) (Var y) | x == y = True +lessEq _ (Var _) = False +lessEq (Var x) t = x `elem` vars t +lessEq t@(Fun f ts) u@(Fun g us) = + (st < su || + (st == su && f < g) || + (st == su && f == g && lexLess ts us)) && + xs `isSubsequenceOf` ys + where + lexLess Empty Empty = True + lexLess (Cons t ts) (Cons u us) + | t == u = lexLess ts us + | otherwise = + lessEq t u && + case unify t u of + Nothing -> True + Just sub + | not (allSubst (\_ (Cons t Empty) -> isMinimal t) sub) -> ERROR("weird term inequality") + | otherwise -> lexLess (subst sub ts) (subst sub us) + lexLess _ _ = ERROR("incorrect function arity") + xs = sort (vars t) + ys = sort (vars u) + st = size t + su = size u + +lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness +lessIn model t u = + case sizeLessIn model t u of + Nothing -> Nothing + Just Strict -> Just Strict + Just Nonstrict -> lexLessIn model t u + +sizeLessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness +sizeLessIn model t u = + case minimumIn model m of + Just l + | l > -k -> Just Strict + | l == -k -> Just Nonstrict + _ -> Nothing + where + (k, m) = + foldr (addSize id) + (foldr (addSize negate) (0, Map.empty) (subterms t)) + (subterms u) + addSize op (Fun f _) (k, m) = (k + op (size f), m) + addSize op (Var x) (k, m) = (k, Map.insertWith (+) x (op 1) m) + +minimumIn :: Function f => Model f -> Map Var Int -> Maybe Int +minimumIn model t = + liftM2 (+) + (fmap sum (mapM minGroup (varGroups model))) + (fmap sum (mapM minOrphan (Map.toList t))) + where + minGroup (lo, xs, mhi) + | all (>= 0) sums = Just (sum coeffs * size lo) + | otherwise = + case mhi of + Nothing -> Nothing + Just hi -> + let coeff = negate (minimum coeffs) in + Just $ + sum coeffs * size lo + + coeff * (size lo - size hi) + where + coeffs = map (\x -> Map.findWithDefault 0 x t) xs + sums = scanr1 (+) coeffs + + minOrphan (x, k) + | varInModel model x = Just 0 + | k < 0 = Nothing + | otherwise = Just k + +lexLessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness +lexLessIn _ t u | t == u = Just Nonstrict +lexLessIn cond t u + | Just a <- fromTerm t, + Just b <- fromTerm u, + Just x <- lessEqInModel cond a b = Just x + | Just a <- fromTerm t, + any isJust + [ lessEqInModel cond a b + | v <- properSubterms u, Just b <- [fromTerm v]] = + Just Strict +lexLessIn cond (Fun f ts) (Fun g us) = + case compare f g of + LT -> Just Strict + GT -> Nothing + EQ -> loop ts us + where + loop Empty Empty = Just Nonstrict + loop (Cons t ts) (Cons u us) + | t == u = loop ts us + | otherwise = + case lessIn cond t u of + Nothing -> Nothing + Just Strict -> Just Strict + Just Nonstrict -> + let Just sub = unify t u in + loop (subst sub ts) (subst sub us) + loop _ _ = ERROR("incorrect function arity") +lexLessIn _ t _ | isMinimal t = Just Nonstrict +lexLessIn _ _ _ = Nothing diff --git a/src/Twee/LPO.hs b/src/Twee/LPO.hs new file mode 100644 --- /dev/null +++ b/src/Twee/LPO.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE CPP, PatternGuards #-} +module Twee.LPO where + +#include "errors.h" +import Twee.Base hiding (lessEq, lessIn) +import Twee.Constraints hiding (lessEq, lessIn) +import Data.Maybe +import Control.Monad + +lessEq :: Function f => Term f -> Term f -> Bool +lessEq (Var x) (Var y) = x == y +lessEq (Var x) t = x `elem` vars t +lessEq (Fun f _) (Var _) = f == minimal +lessEq t@(Fun f ts) u@(Fun g us) = + case compare f g of + LT -> + and [ lessEq t u | t <- fromTermList ts ] && + and [ isNothing (match u t) | t <- fromTermList ts ] + EQ -> lexLess t u ts us + GT -> or [ lessEq t u | u <- fromTermList us ] + where + lexLess _ _ Empty Empty = True + lexLess t u (Cons t' ts) (Cons u' us) + | t' == u' = lexLess t u ts us + | lessEq t' u' = + and [ lessEq t u | t <- fromTermList ts ] && + and [ isNothing (match u t) | t <- fromTermList ts ] && + case match u' t' of + Nothing -> True + Just sub -> + lexLess (subst sub t) (subst sub u) (subst sub ts) (subst sub us) + | otherwise = + or [ lessEq t u | u <- fromTermList us ] + lexLess _ _ _ _ = ERROR("incorrect function arity") + +lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness +lessIn model (Var x) t + | or [isJust (varLessIn x u) | u <- properSubterms t] = Just Strict + | Just str <- varLessIn x t = Just str + | otherwise = Nothing + where + varLessIn x t = fromTerm t >>= lessEqInModel model (Variable x) +lessIn model t (Var x) = do + a <- fromTerm t + lessEqInModel model a (Variable x) +lessIn model t@(Fun f ts) u@(Fun g us) = + case compare f g of + LT -> do + guard (and [ lessIn model t u == Just Strict | t <- fromTermList ts ]) + return Strict + EQ -> lexLess t u ts us + GT -> do + msum [ lessIn model t u | u <- fromTermList us ] + return Strict + where + lexLess _ _ Empty Empty = Just Nonstrict + lexLess t u (Cons t' ts) (Cons u' us) + | t' == u' = lexLess t u ts us + | Just str <- lessIn model t' u' = do + guard (and [ lessIn model t u == Just Strict | t <- fromTermList ts ]) + case str of + Strict -> Just Strict + Nonstrict -> + let Just sub = unify t' u' in + lexLess (subst sub t) (subst sub u) (subst sub ts) (subst sub us) + | otherwise = do + msum [ lessIn model t u | u <- fromTermList us ] + return Strict + lexLess _ _ _ _ = ERROR("incorrect function arity") diff --git a/src/Twee/Label.hs b/src/Twee/Label.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Label.hs @@ -0,0 +1,48 @@ +-- | Assignment of unique IDs to values. +-- Inspired by the 'intern' package. + +{-# LANGUAGE RecordWildCards, ScopedTypeVariables #-} +module Twee.Label where + +import Data.IORef +import System.IO.Unsafe +import qualified Data.IntMap.Strict as IntMap +import Data.IntMap.Strict(IntMap) +import qualified Data.Map.Strict as Map +import Data.Map.Strict(Map) + +class Ord a => Labelled a where + cache :: Cache a + initialId :: a -> Int + initialId _ = 0 + +type Cache a = IORef (CacheState a) +data CacheState a = + CacheState { + nextId :: {-# UNPACK #-} !Int, + to :: !(IntMap a), + from :: !(Map a Int) } + deriving Show + +mkCache :: forall a. Labelled a => Cache a +mkCache = unsafePerformIO (newIORef (CacheState (initialId (undefined :: a)) IntMap.empty Map.empty)) + +label :: Labelled a => a -> Int +label x = + compare x x `seq` + unsafeDupablePerformIO $ + atomicModifyIORef' cache $ \cache@CacheState{..} -> + case Map.lookup x from of + Nothing -> + (CacheState + (nextId+1) + (IntMap.insert nextId x to) + (Map.insert x nextId from), + nextId) + Just n -> (cache, n) + +find :: Labelled a => Int -> Maybe a +find n = + unsafeDupablePerformIO $ do + CacheState{..} <- readIORef cache + return (IntMap.lookup n to) diff --git a/src/Twee/Pretty.hs b/src/Twee/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Pretty.hs @@ -0,0 +1,165 @@ +-- | Pretty-printing of terms and assorted other values. + +{-# LANGUAGE Rank2Types, FlexibleContexts #-} +module Twee.Pretty(module Twee.Pretty, module Text.PrettyPrint.HughesPJClass, Pretty(..)) where + +import Text.PrettyPrint.HughesPJClass +import qualified Data.Map as Map +import Data.Map(Map) +import qualified Data.Set as Set +import Data.Set(Set) +import Data.Ratio +import Twee.Term + +-- * Miscellaneous 'Pretty' instances and utilities. + +prettyPrint :: Pretty a => a -> IO () +prettyPrint x = putStrLn (prettyShow x) + +pPrintParen :: Bool -> Doc -> Doc +pPrintParen True d = parens d +pPrintParen False d = d + +instance Pretty Doc where pPrint = id + +pPrintTuple :: [Doc] -> Doc +pPrintTuple = parens . fsep . punctuate comma + +instance Pretty a => Pretty (Set a) where + pPrint = pPrintSet . map pPrint . Set.toList + +pPrintSet :: [Doc] -> Doc +pPrintSet = braces . fsep . punctuate comma + +instance Pretty Var where + pPrint (MkVar x) = text "X" <> pPrint (x+1) + +instance (Pretty k, Pretty v) => Pretty (Map k v) where + pPrint = pPrintSet . map binding . Map.toList + where + binding (x, v) = hang (pPrint x <+> text "=>") 2 (pPrint v) + +instance (Eq a, Integral a, Pretty a) => Pretty (Ratio a) where + pPrint a + | denominator a == 1 = pPrint (numerator a) + | otherwise = text "(" <+> pPrint (numerator a) <> text "/" <> pPrint (denominator a) <+> text ")" + +-- | Generate a list of candidate names for pretty-printing. +supply :: [String] -> [String] +supply names = + names ++ + [ name ++ show i | i <- [2..], name <- names ] + +-- * Pretty-printing of terms. + +instance (Numbered f, Pretty f) => Pretty (Fun f) where + pPrintPrec l p = pPrintPrec l p . fromFun + +instance (Numbered f, PrettyTerm f) => Pretty (Term f) where + pPrintPrec l p (Var x) = pPrintPrec l p x + pPrintPrec l p (Fun f xs) = + pPrintTerm (termStyle (fromFun f)) l p (pPrint f) (termListToList xs) + +instance (Numbered f, PrettyTerm f) => Pretty (TermList f) where + pPrintPrec _ _ = pPrint . termListToList + +instance (Numbered f, PrettyTerm f) => Pretty (Subst f) where + pPrint sub = text "{" <> fsep (punctuate (text ",") docs) <> text "}" + where + docs = + [ hang (pPrint x <+> text "->") 2 (pPrint t) + | (x, t) <- listSubst sub ] + +-- | A class for customising the printing of function symbols. +class Pretty f => PrettyTerm f where + termStyle :: f -> TermStyle + termStyle _ = curried + +-- | Defines how to print out a function symbol. +newtype TermStyle = + TermStyle { + -- | Takes the pretty-printing level, precedence, + -- pretty-printed function symbol and list of arguments and prints the term. + pPrintTerm :: forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc } + +invisible, curried, uncurried, prefix, postfix :: TermStyle + +-- | For operators like @$@ that should be printed as a blank space. +invisible = + TermStyle $ \l p d -> + let + f [] = d + f [t] = pPrintPrec l p t + f (t:ts) = + pPrintParen (p > 10) $ + pPrint t <+> + (hsep (map (pPrintPrec l 11) ts)) + in f + +-- | For functions that should be printed curried. +curried = + TermStyle $ \l p d -> + let + f [] = d + f xs = + pPrintParen (p > 10) $ + d <+> + (hsep (map (pPrintPrec l 11) xs)) + in f + +-- | For functions that should be printed uncurried. +uncurried = + TermStyle $ \l _ d -> + let + f [] = d + f xs = + d <> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs))) + in f + +-- | A helper function that deals with under- and oversaturated applications. +fixedArity :: Int -> TermStyle -> TermStyle +fixedArity arity style = + TermStyle $ \l p d -> + let + f xs + | length xs < arity = pPrintTerm curried l p (parens d) xs + | length xs > arity = + pPrintParen (p > 10) $ + hsep (parens (pPrintTerm style l 0 d ys): + map (pPrintPrec l 11) zs) + | otherwise = pPrintTerm style l p d xs + where + (ys, zs) = splitAt arity xs + in f + +-- | A helper function that drops a certain number of arguments. +implicitArguments :: Int -> TermStyle -> TermStyle +implicitArguments n (TermStyle pp) = + TermStyle $ \l p d xs -> pp l p d (drop n xs) + +-- | For prefix operators. +prefix = + fixedArity 1 $ + TermStyle $ \l _ d [x] -> + d <> pPrintPrec l 11 x + +-- | For postfix operators. +postfix = + fixedArity 1 $ + TermStyle $ \l _ d [x] -> + pPrintPrec l 11 x <> d + +-- | For infix operators. +infixStyle :: Int -> TermStyle +infixStyle pOp = + fixedArity 2 $ + TermStyle $ \l p d [x, y] -> + pPrintParen (p > fromIntegral pOp) $ + pPrintPrec l (fromIntegral pOp+1) x <+> d <+> + pPrintPrec l (fromIntegral pOp+1) y + +-- | For tuples. +tupleStyle :: TermStyle +tupleStyle = + TermStyle $ \l _ _ xs -> + parens (hsep (punctuate comma (map (pPrintPrec l 0) xs))) diff --git a/src/Twee/Queue.hs b/src/Twee/Queue.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Queue.hs @@ -0,0 +1,157 @@ +-- A priority queue, with orphan murder. +{-# LANGUAGE TypeFamilies, GeneralizedNewtypeDeriving, DeriveFunctor, RecordWildCards, BangPatterns #-} +module Twee.Queue(module Twee.Queue, Heap.Heap) where + +import Twee.Base +import Data.Ord +import qualified Data.Set as Set +import Data.Set(Set) +import qualified Data.List as List +import qualified Data.Heap as Heap +import Control.Monad + +class Heuristic h where + insert :: Ord a => a -> h a -> h a + remove :: Ord a => h a -> Maybe (a, h a) + + reinsert :: Ord a => a -> h a -> h a + reinsert = insert + + members :: Ord a => h a -> [a] + members = List.unfoldr remove + +instance Heuristic Heap.Heap where + insert = Heap.insert + remove = Heap.viewMin + members = Heap.toUnsortedList + +emptyHeap :: Heap.Heap a +emptyHeap = Heap.empty + +data FIFO a = FIFO [a] [a] deriving Show + +emptyFIFO :: FIFO a +emptyFIFO = FIFO [] [] + +instance Heuristic FIFO where + insert x (FIFO xs ys) = FIFO (x:xs) ys + remove (FIFO [] []) = Nothing + remove (FIFO xs []) = remove (FIFO [] (reverse xs)) + remove (FIFO xs (y:ys)) = Just (y, FIFO xs ys) + + reinsert x (FIFO xs ys) = FIFO xs (x:ys) + members (FIFO xs ys) = ys ++ reverse xs + +data Either1 h1 h2 a = Left1 (h1 a) | Right1 (h2 a) deriving Show + +instance (Heuristic h1, Heuristic h2) => Heuristic (Either1 h1 h2) where + insert x (Left1 q) = Left1 (insert x q) + insert x (Right1 q) = Right1 (insert x q) + reinsert x (Left1 q) = Left1 (reinsert x q) + reinsert x (Right1 q) = Right1 (reinsert x q) + remove (Left1 q) = fmap (fmap Left1) (remove q) + remove (Right1 q) = fmap (fmap Right1) (remove q) + members (Left1 q) = members q + members (Right1 q) = members q + +data Mix h a = + Mix { + takeLeft :: {-# UNPACK #-} !Int, + takeRight :: {-# UNPACK #-} !Int, + takeNext :: {-# UNPACK #-} !Int, + left :: !(h a), + right :: !(h a) } + deriving Show + +emptyMix :: Int -> Int -> h a -> h a -> Mix h a +emptyMix m n l r = Mix m n m l r + +instance Heuristic h => Heuristic (Mix h) where + insert x mix = + mix { left = insert x (left mix), + right = insert x (right mix) } + + remove mix = go mix `mplus` go (swap mix) `mplus` go (reset mix) + where + go mix@Mix{..} = do + guard (takeNext > 0) + (x, left') <- remove left + return (x, mix { takeNext = takeNext - 1, left = left' }) + swap Mix{..} = Mix takeRight takeLeft takeRight right left + reset Mix{..} = Mix takeLeft takeRight takeLeft left right + + reinsert x mix = + mix { left = reinsert x (left mix), + right = reinsert x (right mix) } + + members mix = members (left mix) + +data Queue h a = + Queue { + queue :: !(h a), + emptyQueue :: h a, + queueLabels :: Set Label, + nextLabel :: Label } + deriving Show + +class Ord a => Labels a where + labels :: a -> [Label] + +empty :: h a -> Queue h a +empty q = Queue q q (Set.singleton noLabel) (noLabel+1) + +emptyFrom :: Queue q a -> Queue q a +emptyFrom q = q { queue = emptyQueue q } + +enqueue :: (Heuristic h, Labels a) => a -> Queue h a -> Queue h a +enqueue x q = q { queue = insert x (queue q) } + +reenqueue :: (Heuristic h, Labels a) => a -> Queue h a -> Queue h a +reenqueue x q = q { queue = reinsert x (queue q) } + +dequeue :: (Heuristic h, Labels a) => Queue h a -> Maybe (a, Queue h a) +dequeue q@Queue{queueLabels = ls, queue = q0} = aux q0 + where + aux q0 = do + (x, q1) <- remove q0 + if or [ l `Set.notMember` ls | l <- labels x ] then + aux q1 + else return (x, q { queue = q1 }) + +queueSize :: (Heuristic h, Labels a) => Queue h a -> Int +queueSize q = length (toList q) + +toList :: (Heuristic h, Labels a) => Queue h a -> [a] +toList Queue{..} = filter p (members queue) + where + p x = and [ l `Set.member` queueLabels | l <- labels x ] + +newtype Label = Label Int deriving (Eq, Ord, Num, Show, Integral, Enum, Real) + +noLabel :: Label +noLabel = 0 + +newLabel :: Queue h a -> (Label, Queue h a) +newLabel q@Queue{nextLabel = n, queueLabels = ls} = + (n, q { nextLabel = n+1, queueLabels = Set.insert n ls } ) + +deleteLabel :: Label -> Queue h a -> Queue h a +deleteLabel l q@Queue{queueLabels = ls} = q { queueLabels = Set.delete l ls } + +data Labelled a = Labelled { labelOf :: Label, peel :: a } deriving (Show, Functor) + +instance Eq (Labelled a) where x == y = labelOf x == labelOf y +instance Ord (Labelled a) where compare = comparing labelOf +instance Symbolic a => Symbolic (Labelled a) where + type ConstantOf (Labelled a) = ConstantOf a + term = term . peel + termsDL = termsDL . peel + replace f (Labelled l x) = Labelled l (replace f x) +instance Pretty a => Pretty (Labelled a) where pPrint = pPrint . peel + +moveLabel :: Functor f => Labelled (f a) -> f (Labelled a) +moveLabel (Labelled l x) = fmap (Labelled l) x + +unlabelled :: a -> Labelled a +unlabelled = Labelled noLabel + diff --git a/src/Twee/Rule.hs b/src/Twee/Rule.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Rule.hs @@ -0,0 +1,354 @@ +{-# LANGUAGE TypeFamilies, StandaloneDeriving, FlexibleContexts, UndecidableInstances, RecordWildCards, PatternGuards, CPP, BangPatterns #-} +module Twee.Rule where + +#include "errors.h" +import Twee.Base +import Twee.Constraints +import qualified Twee.Index as Index +import Twee.Index(Frozen) +import Control.Monad +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict +import Data.Maybe +import Data.List +import Twee.Utils +import qualified Data.Set as Set +import Data.Set(Set) +import qualified Twee.Term as Term + +-------------------------------------------------------------------------------- +-- Rewrite rules. +-------------------------------------------------------------------------------- + +data Rule f = + Rule { + orientation :: Orientation f, + lhs :: Term f, + rhs :: Term f } + deriving (Eq, Ord, Show) + +data Orientation f = + Oriented + | WeaklyOriented [Term f] + | Permutative [(Term f, Term f)] + | Unoriented + deriving Show + +instance Eq (Orientation f) where _ == _ = True +instance Ord (Orientation f) where compare _ _ = EQ + +oriented :: Orientation f -> Bool +oriented Oriented = True +oriented (WeaklyOriented _) = True +oriented _ = False + +instance Symbolic (Rule f) where + type ConstantOf (Rule f) = f + term = lhs + termsDL Rule{..} = termsDL (lhs, (rhs, orientation)) + replace f (Rule or l r) = Rule (replace f or) (replace f l) (replace f r) + +instance Symbolic (Orientation f) where + type ConstantOf (Orientation f) = f + term = __ + termsDL Oriented = mempty + termsDL (WeaklyOriented ts) = termsDL ts + termsDL (Permutative ts) = termsDL ts + termsDL Unoriented = mempty + replace _ Oriented = Oriented + replace f (WeaklyOriented ts) = WeaklyOriented (replace f ts) + replace f (Permutative ts) = Permutative (replace f ts) + replace _ Unoriented = Unoriented + +instance (Numbered f, PrettyTerm f) => Pretty (Rule f) where + pPrint (Rule Oriented l r) = pPrintRule l r + pPrint (Rule (WeaklyOriented ts) l r) = hang (pPrintRule l r) 2 (text "(weak on" <+> pPrint ts <> text ")") + pPrint (Rule (Permutative ts) l r) = hang (pPrintRule l r) 2 (text "(permutative on" <+> pPrint ts <> text ")") + pPrint (Rule Unoriented l r) = hang (pPrintRule l r) 2 (text "(unoriented)") + +pPrintRule :: (Numbered f, PrettyTerm f) => Term f -> Term f -> Doc +pPrintRule l r = hang (pPrint l <+> text "->") 2 (pPrint r) + +-------------------------------------------------------------------------------- +-- Equations. +-------------------------------------------------------------------------------- + +data Equation f = Term f :=: Term f deriving (Eq, Ord, Show) +type EquationOf a = Equation (ConstantOf a) + +instance Symbolic (Equation f) where + type ConstantOf (Equation f) = f + term = __ + termsDL (t :=: u) = termsDL (t, u) + replace f (t :=: u) = replace f t :=: replace f u + +instance (Numbered f, PrettyTerm f) => Pretty (Equation f) where + pPrint (x :=: y) = hang (pPrint x <+> text "=") 2 (pPrint y) + +instance (Numbered f, Sized f) => Sized (Equation f) where + size (x :=: y) = size x + size y + +order :: Function f => Equation f -> Equation f +order (l :=: r) + | l == r = l :=: r + | otherwise = + case compare (size l) (size r) of + LT -> r :=: l + GT -> l :=: r + EQ -> if lessEq l r then r :=: l else l :=: r + +unorient :: Rule f -> Equation f +unorient (Rule _ l r) = l :=: r + +orient :: Function f => Equation f -> [Rule f] +orient (l :=: r) | l == r = [] +orient (l :=: r) = + -- If we have an equation where some variables appear only on one side, e.g.: + -- f x y = g x z + -- then replace it with the equations: + -- f x y = f x k + -- g x z = g x k + -- f x k = g x k + -- where k is an arbitrary constant + [ rule l r' | ord /= Just LT && ord /= Just EQ ] ++ + [ rule r l' | ord /= Just GT && ord /= Just EQ ] ++ + [ rule l l' | not (null ls), ord /= Just GT ] ++ + [ rule r r' | not (null rs), ord /= Just LT ] + where + ord = orientTerms l' r' + l' = erase ls l + r' = erase rs r + ls = usort (vars l) \\ usort (vars r) + rs = usort (vars r) \\ usort (vars l) + + erase [] t = t + erase xs t = subst sub t + where + sub = fromMaybe __ $ flattenSubst [(x, minimalTerm) | x <- xs] + +rule :: Function f => Term f -> Term f -> Rule f +rule t u = Rule o t u + where + o | lessEq u t = + case unify t u of + Nothing -> Oriented + Just sub + | allSubst (\_ (Cons t Empty) -> isMinimal t) sub -> + WeaklyOriented (map (build . var . fst) (listSubst sub)) + | otherwise -> Unoriented + | lessEq t u = ERROR("wrongly-oriented rule") + | not (null (usort (vars u) \\ usort (vars t))) = + ERROR("unbound variables in rule") + | Just ts <- evalStateT (makePermutative t u) [], + permutativeOK t u ts = + Permutative ts + | otherwise = Unoriented + + permutativeOK _ _ [] = True + permutativeOK t u ((Var x, Var y):xs) = + lessIn model u t == Just Strict && + permutativeOK t' u' xs + where + model = modelFromOrder [Variable y, Variable x] + sub x' = if x == x' then var y else var x' + t' = subst sub t + u' = subst sub u + + makePermutative t u = do + msub <- gets flattenSubst + sub <- lift msub + aux (subst sub t) (subst sub u) + where + aux (Var x) (Var y) + | x == y = return [] + | otherwise = do + modify ((x, build $ var y):) + return [(build $ var x, build $ var y)] + + aux (Fun f ts) (Fun g us) + | f == g = + fmap concat (zipWithM makePermutative (fromTermList ts) (fromTermList us)) + + aux _ _ = mzero + +bothSides :: (Term f -> Term f') -> Equation f -> Equation f' +bothSides f (t :=: u) = f t :=: f u + +trivial :: Eq f => Equation f -> Bool +trivial (t :=: u) = t == u + +-------------------------------------------------------------------------------- +-- Rewriting. +-------------------------------------------------------------------------------- + +type Strategy f = Term f -> [Reduction f] + +data Reduction f = + Step (Rule f) (Subst f) + | Trans (Reduction f) (Reduction f) + | Parallel [(Int, Reduction f)] (Term f) + deriving Show + +result :: Reduction f -> Term f +result (Parallel [] t) = t +result (Trans _ p) = result p +result t = build (emitReduction t) + where + emitReduction (Step r sub) = Term.subst sub (rhs r) + emitReduction (Trans _ p) = emitReduction p + emitReduction (Parallel ps t) = emitParallel 0 ps (singleton t) + + emitParallel !_ _ _ | False = __ + emitParallel _ _ Empty = mempty + emitParallel _ [] t = builder t + emitParallel n ((m, _):_) t | m >= n + lenList t = builder t + emitParallel n ps@((m, _):_) (Cons t u) | m >= n + len t = + builder t `mappend` emitParallel (n + len t) ps u + emitParallel n ((m, _):ps) t | m < n = emitParallel n ps t + emitParallel n ((m, p):ps) (Cons t u) | m == n = + emitReduction p `mappend` emitParallel (n + len t) ps u + emitParallel n ps (Cons (Var x) u) = + var x `mappend` emitParallel (n + 1) ps u + emitParallel n ps (Cons (Fun f t) u) = + fun f (emitParallel (n+1) ps t) `mappend` + emitParallel (n + 1 + lenList t) ps u + +instance (Numbered f, PrettyTerm f) => Pretty (Reduction f) where + pPrint = pPrintReduction + +pPrintReduction :: (Numbered f, PrettyTerm f) => Reduction f -> Doc +pPrintReduction p = + case flatten p of + [p] -> pp p + ps -> pPrint (map pp ps) + where + flatten (Trans p q) = flatten p ++ flatten q + flatten p = [p] + + pp p = sep [pp0 p, nest 2 (text "giving" <+> pPrint (result p))] + pp0 (Step rule sub) = + sep [pPrint rule, + nest 2 (text "at" <+> pPrint sub)] + pp0 (Parallel [] _) = text "refl" + pp0 (Parallel [(0, p)] _) = pp0 p + pp0 (Parallel ps _) = + sep (punctuate (text " and") + [hang (pPrint n <+> text "->") 2 (pPrint p) | (n, p) <- ps]) + +steps :: Reduction f -> [(Rule f, Subst f)] +steps r = aux r [] + where + aux (Step r sub) = ((r, sub):) + aux (Trans p q) = aux p . aux q + aux (Parallel ps _) = foldr (.) id (map (aux . snd) ps) + +anywhere1 :: (Numbered f, PrettyTerm f) => Strategy f -> Reduction f -> Maybe (Reduction f) +anywhere1 strat p = aux [] 0 (singleton t) p t + where + aux _ !_ !_ _ !_ | False = __ + aux [] _ Empty _ _ = Nothing + aux ps _ Empty p t = Just (p `Trans` Parallel (reverse ps) t) + aux ps n (Cons (Var _) t) p u = aux ps (n+1) t p u + aux ps n (Cons t u) p v | q:_ <- strat t = + aux ((n, q):ps) (n+len t) u p v + aux ps n (ConsSym (Fun _ _) t) p u = + aux ps (n+1) t p u + + t = result p + +normaliseWith :: (Numbered f, PrettyTerm f) => Strategy f -> Term f -> Reduction f +normaliseWith strat t = aux 0 (Parallel [] t) + where + aux 1000 p = + ERROR("Possibly nonterminating rewrite:\n" ++ + prettyShow p) + aux n p = + case anywhere1 strat p of + Nothing -> p + Just q -> aux (n+1) q + +normalForms :: Function f => Strategy f -> [Term f] -> Set (Term f) +normalForms strat ts = go Set.empty Set.empty ts + where + go _ norm [] = norm + go dead norm (t:ts) + | t `Set.member` dead = go dead norm ts + | t `Set.member` norm = go dead norm ts + | null us = go dead (Set.insert t norm) ts + | otherwise = + go (Set.insert t dead) norm (us ++ ts) + where + us = map result (anywhere strat t) + +anywhere :: Strategy f -> Strategy f +anywhere strat t = aux 0 (singleton t) + where + aux !_ Empty = [] + aux n (Cons Var{} u) = aux (n+1) u + aux n (ConsSym u v) = + [Parallel [(n,p)] t | p <- strat u] ++ aux (n+1) v + +nested :: Strategy f -> Strategy f +nested strat t = [Parallel [(1,p)] t | p <- aux 0 (children t)] + where + aux !_ Empty = [] + aux n (Cons Var{} u) = aux (n+1) u + aux n (Cons u v) = + [Parallel [(n,p)] t | p <- strat u] ++ aux (n+len t) v + +{-# INLINE rewrite #-} +rewrite :: Function f => String -> (Rule f -> Subst f -> Bool) -> Frozen (Rule f) -> Strategy f +rewrite _phase p rules t = do + Index.Match rule sub <- Index.matches t rules + guard (p rule sub) + return (Step rule sub) + +tryRule :: Function f => (Rule f -> Subst f -> Bool) -> Rule f -> Strategy f +tryRule p rule t = do + sub <- maybeToList (match (lhs rule) t) + guard (p rule sub) + return (Step rule sub) + +simplifies :: Function f => Rule f -> Subst f -> Bool +simplifies (Rule Oriented _ _) _ = True +simplifies (Rule (WeaklyOriented ts) _ _) sub = + or [ not (isMinimal t) | t <- subst sub ts ] +simplifies (Rule (Permutative _) _ _) _ = False +simplifies (Rule Unoriented _ _) _ = False + +reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool +reducesWith _ (Rule Oriented _ _) _ = True +reducesWith _ (Rule (WeaklyOriented ts) _ _) sub = + or [ not (isMinimal t) | t <- subst sub ts ] +reducesWith p (Rule (Permutative ts) _ _) sub = + aux ts + where + aux [] = False + aux ((t, u):ts) + | t' == u' = aux ts + | otherwise = p u' t' + where + t' = subst sub t + u' = subst sub u +reducesWith p (Rule Unoriented t u) sub = + p u' t' && u' /= t' + where + t' = subst sub t + u' = subst sub u + +reduces :: Function f => Rule f -> Subst f -> Bool +reduces rule = reducesWith lessEq rule + +reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool +reducesInModel cond rule = reducesWith (\t u -> isJust (lessIn cond t u)) rule + +reducesSkolem :: Function f => Rule f -> Subst f -> Bool +reducesSkolem = reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) + where + skolemise = con . skolem + +reducesSub :: Function f => Term f -> Rule f -> Subst f -> Bool +reducesSub top rule sub = + reducesSkolem rule sub && lessEq u top && isNothing (unify u top) + where + u = subst sub (rhs rule) diff --git a/src/Twee/Term.hs b/src/Twee/Term.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Term.hs @@ -0,0 +1,473 @@ +-- Terms and substitutions, implemented using flatterms. +-- This module implements the usual term manipulation stuff +-- (matching, unification, etc.) on top of the primitives +-- in Twee.Term.Core. +{-# LANGUAGE BangPatterns, CPP, PatternSynonyms, RankNTypes, FlexibleContexts, ViewPatterns, FlexibleInstances, UndecidableInstances, ScopedTypeVariables, RecordWildCards, MultiParamTypeClasses, FunctionalDependencies, GADTs #-} +module Twee.Term( + module Twee.Term, + -- Stuff from Twee.Term.Core. + Term, TermList, at, lenList, + pattern Empty, pattern Cons, pattern ConsSym, + pattern UnsafeCons, pattern UnsafeConsSym, + Fun(..), Var(..), pattern Var, pattern Fun, singleton, Builder) where + +#include "errors.h" +import Prelude hiding (lookup) +import Twee.Term.Core +import Data.List hiding (lookup) +import Data.Maybe +import Data.Ord +import Data.Monoid +import Data.IntMap.Strict(IntMap) +import qualified Data.IntMap.Strict as IntMap + +-------------------------------------------------------------------------------- +-- A type class for builders. +-------------------------------------------------------------------------------- + +class Build f a | a -> f where + builder :: a -> Builder f + +instance Build f (Builder f) where + builder = id + +instance Build f (Term f) where + builder = emitTerm + +instance Build f (TermList f) where + builder = emitTermList + +instance Build f a => Build f [a] where + {-# INLINE builder #-} + builder = mconcat . map builder + +{-# INLINE build #-} +build :: Build f a => a -> Term f +build x = + case buildList x of + Cons t Empty -> t + +{-# INLINE buildList #-} +buildList :: Build f a => a -> TermList f +buildList x = buildTermList (builder x) + +{-# INLINE con #-} +con :: Fun f -> Builder f +con x = emitFun x mempty + +{-# INLINE fun #-} +fun :: Build f a => Fun f -> a -> Builder f +fun f ts = emitFun f (builder ts) + +var :: Var -> Builder f +var = emitVar + +-------------------------------------------------------------------------------- +-- Pattern synonyms for substitutions. +-------------------------------------------------------------------------------- + +{-# INLINE listSubstList #-} +listSubstList :: Subst f -> [(Var, TermList f)] +listSubstList (Subst sub) = [(MkVar x, t) | (x, t) <- IntMap.toList sub] + +{-# INLINE listSubst #-} +listSubst :: Subst f -> [(Var, Term f)] +listSubst sub = [(x, t) | (x, Cons t Empty) <- listSubstList sub] + +{-# INLINE foldSubst #-} +foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b +foldSubst op e !sub = foldr (uncurry op) e (listSubstList sub) + +{-# INLINE allSubst #-} +allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool +allSubst p = foldSubst (\x t y -> p x t && y) True + +{-# INLINE forMSubst_ #-} +forMSubst_ :: Monad m => Subst f -> (Var -> TermList f -> m ()) -> m () +forMSubst_ sub f = foldSubst (\x t m -> do { f x t; m }) (return ()) sub + +-------------------------------------------------------------------------------- +-- Substitution. +-------------------------------------------------------------------------------- + +class Substitution f s | s -> f where + evalSubst :: s -> Var -> Builder f + +instance (Build f a, v ~ Var) => Substitution f (v -> a) where + {-# INLINE evalSubst #-} + evalSubst sub x = builder (sub x) + +instance Substitution f (Subst f) where + {-# INLINE evalSubst #-} + evalSubst sub x = + case lookupList x sub of + Nothing -> var x + Just ts -> builder ts + +{-# INLINE subst #-} +subst :: Substitution f s => s -> Term f -> Builder f +subst sub t = substList sub (singleton t) + +{-# INLINE substList #-} +substList :: Substitution f s => s -> TermList f -> Builder f +substList sub ts = aux ts + where + aux Empty = mempty + aux (Cons (Var x) ts) = evalSubst sub x <> aux ts + aux (Cons (Fun f ts) us) = fun f (aux ts) <> aux us + +newtype Subst f = + Subst { + unSubst :: IntMap (TermList f) } + +{-# INLINE substSize #-} +substSize :: Subst f -> Int +substSize (Subst sub) + | IntMap.null sub = 0 + | otherwise = fst (IntMap.findMax sub) + 1 + +-- Look up a variable. +{-# INLINE lookupList #-} +lookupList :: Var -> Subst f -> Maybe (TermList f) +lookupList (MkVar x) (Subst sub) = IntMap.lookup x sub + +-- Add a new binding to a substitution. +{-# INLINE extendList #-} +extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f) +extendList (MkVar x) !t (Subst sub) = + case IntMap.lookup x sub of + Nothing -> Just $! Subst (IntMap.insert x t sub) + Just u + | t == u -> Just (Subst sub) + | otherwise -> Nothing + +-- Remove a binding from a substitution. +{-# INLINE retract #-} +retract :: Var -> Subst f -> Subst f +retract (MkVar x) (Subst sub) = Subst (IntMap.delete x sub) + +-- Add a new binding to a substitution. +-- Overwrites any existing binding. +{-# INLINE unsafeExtendList #-} +unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f +unsafeExtendList (MkVar x) !t (Subst sub) = Subst (IntMap.insert x t sub) + +-- Composition of substitutions. +substCompose :: Substitution f s => Subst f -> s -> Subst f +substCompose (Subst !sub1) !sub2 = + Subst (IntMap.map (buildList . substList sub2) sub1) + +-- Are two substitutions compatible? +substCompatible :: Subst f -> Subst f -> Bool +substCompatible (Subst !sub1) (Subst !sub2) = + IntMap.null (IntMap.mergeWithKey f g h sub1 sub2) + where + f _ t u + | t == u = Nothing + | otherwise = Just t + g _ = IntMap.empty + h _ = IntMap.empty + +-- Take the union of two substitutions, which must be compatible. +substUnion :: Subst f -> Subst f -> Subst f +substUnion (Subst !sub1) (Subst !sub2) = + Subst (IntMap.union sub1 sub2) + +-- Is a substitution idempotent? +{-# INLINE idempotent #-} +idempotent :: Subst f -> Bool +idempotent !sub = allSubst (\_ t -> sub `idempotentOn` t) sub + +-- Does a substitution affect a term? +{-# INLINE idempotentOn #-} +idempotentOn :: Subst f -> TermList f -> Bool +idempotentOn !sub = aux + where + aux Empty = True + aux (ConsSym Fun{} t) = aux t + aux (Cons (Var x) t) = isNothing (lookupList x sub) && aux t + +-- Iterate a substitution to make it idempotent. +close :: TriangleSubst f -> Subst f +close (Triangle sub) + | idempotent sub = sub + | otherwise = close (Triangle (substCompose sub sub)) + +-- Return a substitution for canonicalising a list of terms. +canonicalise :: [TermList f] -> Subst f +canonicalise [] = emptySubst +canonicalise (t:ts) = loop emptySubst vars t ts + where + n = maximum (0:map boundList (t:ts)) + vars = + buildTermList $ + mconcat [emitVar (MkVar i) | i <- [0..n]] + + loop !_ !_ !_ !_ | False = __ + loop sub _ Empty [] = sub + loop sub vs Empty (t:ts) = loop sub vs t ts + loop sub vs (ConsSym Fun{} t) ts = loop sub vs t ts + loop sub vs0@(Cons v vs) (Cons (Var x) t) ts = + case extend x v sub of + Just sub -> loop sub vs t ts + Nothing -> loop sub vs0 t ts + +-- The empty substitution. +{-# NOINLINE emptySubst #-} +emptySubst = Subst IntMap.empty + +-- Turn a substitution list into a substitution. +flattenSubst :: [(Var, Term f)] -> Maybe (Subst f) +flattenSubst sub = matchList pat t + where + pat = buildList (map (var . fst) sub) + t = buildList (map snd sub) + +-------------------------------------------------------------------------------- +-- Matching. +-------------------------------------------------------------------------------- + +{-# INLINE match #-} +match :: Term f -> Term f -> Maybe (Subst f) +match pat t = matchList (singleton pat) (singleton t) + +matchList :: TermList f -> TermList f -> Maybe (Subst f) +matchList !pat !t + | lenList t < lenList pat = Nothing + | otherwise = + let loop !_ !_ !_ | False = __ + loop sub Empty _ = Just sub + loop _ _ Empty = __ + loop sub (ConsSym (Fun f _) pat) (ConsSym (Fun g _) t) + | f == g = loop sub pat t + loop sub (Cons (Var x) pat) (Cons t u) = do + sub <- extend x t sub + loop sub pat u + loop _ _ _ = Nothing + in loop emptySubst pat t + +-------------------------------------------------------------------------------- +-- Unification. +-------------------------------------------------------------------------------- + +newtype TriangleSubst f = Triangle { unTriangle :: Subst f } + deriving Show + +instance Substitution f (TriangleSubst f) where + evalSubst (Triangle sub) x = substTri sub x + +{-# INLINE substTri #-} +substTri :: Subst f -> Var -> Builder f +substTri sub x = aux x + where + aux x = + case lookupList x sub of + Nothing -> var x + Just ts -> substList aux ts + +{-# INLINE unify #-} +unify :: Term f -> Term f -> Maybe (Subst f) +unify t u = unifyList (singleton t) (singleton u) + +unifyList :: TermList f -> TermList f -> Maybe (Subst f) +unifyList t u = do + sub <- unifyListTri t u + return $! close sub + +{-# INLINE unifyTri #-} +unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f) +unifyTri t u = unifyListTri (singleton t) (singleton u) + +unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f) +unifyListTri !t !u = fmap Triangle (loop emptySubst t u) + where + loop !_ !_ !_ | False = __ + loop sub Empty _ = Just sub + loop _ _ Empty = __ + loop sub (ConsSym (Fun f _) t) (ConsSym (Fun g _) u) + | f == g = loop sub t u + loop sub (Cons (Var x) t) (Cons u v) = do + sub <- var sub x u + loop sub t v + loop sub (Cons t u) (Cons (Var x) v) = do + sub <- var sub x t + loop sub u v + loop _ _ _ = Nothing + + var sub x t = + case lookupList x sub of + Just u -> loop sub u (singleton t) + Nothing -> var1 sub x t + + var1 sub x t@(Var y) + | x == y = return sub + | otherwise = + case lookup y sub of + Just t -> var1 sub x t + Nothing -> extend x t sub + + var1 sub x t = do + occurs sub x (singleton t) + extend x t sub + + occurs !_ !_ Empty = Just () + occurs sub x (ConsSym Fun{} t) = occurs sub x t + occurs sub x (ConsSym (Var y) t) + | x == y = Nothing + | otherwise = do + occurs sub x t + case lookupList y sub of + Nothing -> Just () + Just u -> occurs sub x u + +-------------------------------------------------------------------------------- +-- Miscellaneous stuff. +-------------------------------------------------------------------------------- + +children :: Term f -> TermList f +children t = + case singleton t of + UnsafeConsSym _ ts -> ts + +fromTermList :: TermList f -> [Term f] +fromTermList Empty = [] +fromTermList (Cons t ts) = t:fromTermList ts + +instance Show (Term f) where + show (Var x) = show x + show (Fun f Empty) = show f + show (Fun f ts) = show f ++ "(" ++ intercalate "," (map show (fromTermList ts)) ++ ")" + +instance Show (TermList f) where + show = show . fromTermList + +instance Show (Subst f) where + show subst = + show + [ (i, t) + | i <- [0..substSize subst-1], + Just t <- [lookup (MkVar i) subst] ] + +{-# INLINE lookup #-} +lookup :: Var -> Subst f -> Maybe (Term f) +lookup x s = do + Cons t Empty <- lookupList x s + return t + +{-# INLINE extend #-} +extend :: Var -> Term f -> Subst f -> Maybe (Subst f) +extend x t sub = extendList x (singleton t) sub + +{-# INLINE len #-} +len :: Term f -> Int +len = lenList . singleton + +{-# INLINE emitTerm #-} +emitTerm :: Term f -> Builder f +emitTerm t = emitTermList (singleton t) + +-- Find the lowest-numbered variable that doesn't appear in a term. +{-# INLINE bound #-} +bound :: Term f -> Int +bound t = boundList (singleton t) + +{-# INLINE boundList #-} +boundList :: TermList f -> Int +boundList t = aux 0 t + where + aux n Empty = n + aux n (ConsSym Fun{} t) = aux n t + aux n (ConsSym (Var (MkVar x)) t) + | x >= n = aux (x+1) t + | otherwise = aux n t + +-- Check if a variable occurs in a term. +{-# INLINE occurs #-} +occurs :: Var -> Term f -> Bool +occurs x t = occursList x (singleton t) + +{-# INLINE occursList #-} +occursList :: Var -> TermList f -> Bool +occursList !x = aux + where + aux Empty = False + aux (ConsSym Fun{} t) = aux t + aux (ConsSym (Var y) t) = x == y || aux t + +{-# INLINE termListToList #-} +termListToList :: TermList f -> [Term f] +termListToList Empty = [] +termListToList (Cons t ts) = t:termListToList ts + +-- The empty term list. +{-# NOINLINE emptyTermList #-} +emptyTermList :: TermList f +emptyTermList = buildList (mempty :: Builder f) + +-- Functions for building terms. + +{-# INLINE subtermsList #-} +subtermsList :: TermList f -> [Term f] +subtermsList t = unfoldr op t + where + op Empty = Nothing + op (ConsSym t u) = Just (t, u) + +{-# INLINE subterms #-} +subterms :: Term f -> [Term f] +subterms = subtermsList . singleton + +{-# INLINE properSubtermsList #-} +properSubtermsList :: TermList f -> [Term f] +properSubtermsList Empty = [] +properSubtermsList (ConsSym _ t) = subtermsList t + +{-# INLINE properSubterms #-} +properSubterms :: Term f -> [Term f] +properSubterms = properSubtermsList . singleton + +isFun :: Term f -> Bool +isFun Fun{} = True +isFun _ = False + +isVar :: Term f -> Bool +isVar Var{} = True +isVar _ = False + +isInstanceOf :: Term f -> Term f -> Bool +t `isInstanceOf` pat = isJust (match pat t) + +isVariantOf :: Term f -> Term f -> Bool +t `isVariantOf` u = t `isInstanceOf` u && u `isInstanceOf` t + +mapFun :: (Fun f -> Fun g) -> Term f -> Builder g +mapFun f = mapFunList f . singleton + +mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g +mapFunList f ts = aux ts + where + aux Empty = mempty + aux (Cons (Var x) ts) = var x `mappend` aux ts + aux (Cons (Fun ff ts) us) = fun (f ff) (aux ts) `mappend` aux us + +-------------------------------------------------------------------------------- +-- Typeclass for getting at the 'f' in a 'Term f'. +-------------------------------------------------------------------------------- + +class Numbered f where + fromInt :: Int -> f + toInt :: f -> Int + +fromFun :: Numbered f => Fun f -> f +fromFun (MkFun n) = fromInt n + +toFun :: Numbered f => f -> Fun f +toFun f = MkFun (toInt f) + +instance (Ord f, Numbered f) => Ord (Fun f) where + compare = comparing fromFun + +pattern App f ts <- Fun (fromFun -> f) (fromTermList -> ts) + +app :: Numbered a => a -> [Term a] -> Term a +app f ts = build (fun (toFun f) ts) diff --git a/src/Twee/Term/Core.hs b/src/Twee/Term/Core.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Term/Core.hs @@ -0,0 +1,287 @@ +-- Terms and substitutions, implemented using flatterms. +-- This module contains all the low-level icky bits +-- and provides primitives for building higher-level stuff. +{-# LANGUAGE BangPatterns, CPP, PatternGuards, PatternSynonyms, ViewPatterns, RecordWildCards, GeneralizedNewtypeDeriving, RankNTypes, MagicHash, UnboxedTuples, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, ScopedTypeVariables #-} +module Twee.Term.Core where + +#include "errors.h" +import Data.Primitive +import Control.Monad.ST.Strict +import Data.Bits +import Data.Int +import GHC.Types(Int(..)) +import GHC.Prim +import GHC.ST hiding (liftST) +import Data.Ord + +-------------------------------------------------------------------------------- +-- Symbols. A symbol is a single function or variable in a flatterm. +-------------------------------------------------------------------------------- + +data Symbol = + Symbol { + -- Is it a function? + isFun :: Bool, + -- What is its number? + index :: Int, + -- What is the size of the term rooted at this symbol? + size :: Int } + +instance Show Symbol where + show Symbol{..} + | isFun = show (MkFun index) ++ "=" ++ show size + | otherwise = show (MkVar index) + +-- Convert symbols to/from Int64 for storage in flatterms. +-- The encoding: +-- * bits 0-30: size +-- * bit 31: 0 (variable) or 1 (function) +-- * bits 32-63: index +{-# INLINE toSymbol #-} +toSymbol :: Int64 -> Symbol +toSymbol n = + Symbol (testBit n 31) + (fromIntegral (n `unsafeShiftR` 32)) + (fromIntegral (n .&. 0x7fffffff)) + +{-# INLINE fromSymbol #-} +fromSymbol :: Symbol -> Int64 +fromSymbol Symbol{..} | index < 0 = ERROR("negative symbol index") +fromSymbol Symbol{..} = + fromIntegral size + + fromIntegral index `unsafeShiftL` 32 + + fromIntegral (fromEnum isFun) `unsafeShiftL` 31 + +-------------------------------------------------------------------------------- +-- Flatterms, or rather lists of terms. +-------------------------------------------------------------------------------- + +-- A TermList is a slice of an unboxed array of symbols. +data TermList f = + TermList { + low :: {-# UNPACK #-} !Int, + high :: {-# UNPACK #-} !Int, + array :: {-# UNPACK #-} !ByteArray } + +at :: Int -> TermList f -> Term f +at n (TermList lo hi arr) + | n < 0 || n + lo >= hi = ERROR("term index out of bounds") + | otherwise = + case TermList (lo+n) hi arr of + Cons t _ -> t + +{-# INLINE lenList #-} +-- The length (number of symbols in) a flatterm. +lenList :: TermList f -> Int +lenList (TermList low high _) = high - low + +-- A term is a special case of a termlist. +-- We store it as the termlist together with the root symbol. +data Term f = + Term { + root :: {-# UNPACK #-} !Int64, + termlist :: {-# UNPACK #-} !(TermList f) } + +instance Eq (Term f) where + x == y = termlist x == termlist y + +instance Ord (Term f) where + compare = comparing termlist + +-- Pattern synonyms for termlists: +-- * Empty :: TermList f +-- Empty is the empty termlist. +-- * Cons t ts :: Term f -> TermList f -> TermList f +-- Cons t ts is the termlist t:ts. +-- * ConsSym t ts :: Term f -> TermList f -> TermList f +-- ConsSym t ts is like Cons t ts but ts also includes t's children +-- (operationally, ts seeks one term to the right in the termlist). +-- * UnsafeCons/UnsafeConsSym: like Cons and ConsSym but don't check +-- that the termlist is non-empty. +pattern Empty <- (patHead -> Nothing) +pattern Cons t ts <- (patHead -> Just (t, _, ts)) +pattern ConsSym t ts <- (patHead -> Just (t, ts, _)) +pattern UnsafeCons t ts <- (unsafePatHead -> Just (t, _, ts)) +pattern UnsafeConsSym t ts <- (unsafePatHead -> Just (t, ts, _)) + +{-# INLINE unsafePatHead #-} +unsafePatHead :: TermList f -> Maybe (Term f, TermList f, TermList f) +unsafePatHead TermList{..} = + Just (Term x (TermList low (low+size) array), + TermList (low+1) high array, + TermList (low+size) high array) + where + x = indexByteArray array low + Symbol{..} = toSymbol x + +{-# INLINE patHead #-} +patHead :: TermList f -> Maybe (Term f, TermList f, TermList f) +patHead t@TermList{..} + | low == high = Nothing + | otherwise = unsafePatHead t + +-- Pattern synonyms for single terms. +-- * Var :: Var -> Term f +-- * Fun :: Fun f -> TermList f -> Term f +newtype Fun f = MkFun Int deriving Eq +newtype Var = MkVar Int deriving (Eq, Ord, Enum) +instance Show (Fun f) where show (MkFun x) = "f" ++ show x +instance Show Var where show (MkVar x) = "x" ++ show x + +pattern Var x <- Term (patRoot -> Left x) _ +pattern Fun f ts <- Term (patRoot -> Right (f :: Fun f)) (patNext -> (ts :: TermList f)) + +{-# INLINE patRoot #-} +patRoot :: Int64 -> Either Var (Fun f) +patRoot root + | isFun = Right (MkFun index) + | otherwise = Left (MkVar index) + where + Symbol{..} = toSymbol root + +{-# INLINE patNext #-} +patNext :: TermList f -> TermList f +patNext (TermList lo hi array) = TermList (lo+1) hi array + +-- Convert a term to a termlist. +{-# INLINE singleton #-} +singleton :: Term f -> TermList f +singleton Term{..} = termlist + +-- We can implement equality almost without access to the +-- internal representation of the termlists, but we cheat by +-- comparing Int64s instead of Symbols. +instance Eq (TermList f) where + {-# INLINE (==) #-} + t == u = lenList t == lenList u && eqSameLength t u + +eqSameLength :: TermList f -> TermList f -> Bool +eqSameLength Empty !_ = True +eqSameLength (ConsSym s1 t) (UnsafeConsSym s2 u) = + root s1 == root s2 && eqSameLength t u + +instance Ord (TermList f) where + {-# INLINE compare #-} + compare t u = + case compare (lenList t) (lenList u) of + EQ -> compareContents t u + x -> x + +compareContents :: TermList f -> TermList f -> Ordering +compareContents Empty !_ = EQ +compareContents (ConsSym s1 t) (UnsafeConsSym s2 u) = + case compare (root s1) (root s2) of + EQ -> compareContents t u + x -> x + +-------------------------------------------------------------------------------- +-- Building terms imperatively. +-------------------------------------------------------------------------------- + +-- A monad for building terms. +newtype Builder f = + Builder { + unBuilder :: + -- Takes: the term array and size, and current position in the term. + -- Returns the final position, which may be out of bounds. + forall s. Builder1 s } + +type Builder1 s = State# s -> MutableByteArray# s -> Int# -> Int# -> (# State# s, Int# #) + +instance Monoid (Builder f) where + {-# INLINE mempty #-} + mempty = Builder built + {-# INLINE mappend #-} + Builder m1 `mappend` Builder m2 = Builder (m1 `then_` m2) + +{-# INLINE buildTermList #-} +buildTermList :: Builder f -> TermList f +buildTermList builder = runST $ do + let + Builder m = builder + loop n@(I# n#) = do + MutableByteArray marray# <- + newByteArray (n * sizeOf (fromSymbol __)) + n' <- + ST $ \s -> + case m s marray# n# 0# of + (# s, n# #) -> (# s, I# n# #) + if n' <= n then do + !array <- unsafeFreezeByteArray (MutableByteArray marray#) + return (TermList 0 n' array) + else loop (n'*2) + loop 16 + +{-# INLINE getArray #-} +getArray :: (MutableByteArray s -> Builder1 s) -> Builder1 s +getArray k = \s array n i -> k (MutableByteArray array) s array n i + +{-# INLINE getSize #-} +getSize :: (Int -> Builder1 s) -> Builder1 s +getSize k = \s array n i -> k (I# n) s array n i + +{-# INLINE getIndex #-} +getIndex :: (Int -> Builder1 s) -> Builder1 s +getIndex k = \s array n i -> k (I# i) s array n i + +{-# INLINE putIndex #-} +putIndex :: Int -> Builder1 s +putIndex (I# i) = \s _ _ _ -> (# s, i #) + +{-# INLINE liftST #-} +liftST :: ST s () -> Builder1 s +liftST (ST m) = + \s _ _ i -> + case m s of + (# s, () #) -> (# s, i #) + +{-# INLINE built #-} +built :: Builder1 s +built = \s _ _ i -> (# s, i #) + +{-# INLINE then_ #-} +then_ :: Builder1 s -> Builder1 s -> Builder1 s +then_ m1 m2 = + \s array n i -> + case m1 s array n i of + (# s, i #) -> m2 s array n i + +{-# INLINE checked #-} +checked :: Int -> Builder1 s -> Builder1 s +checked j m = + getSize $ \n -> + getIndex $ \i -> + if i + j <= n then m else putIndex (i + j) + +{-# INLINE emitSymbolBuilder #-} +emitSymbolBuilder :: Symbol -> Builder f -> Builder f +emitSymbolBuilder x inner = + Builder $ checked 1 $ + getArray $ \array -> + getIndex $ \n -> + putIndex (n+1) `then_` + unBuilder inner `then_` + getIndex (\m -> + liftST $ writeByteArray array n (fromSymbol x { size = m - n })) + +-- Emit a function symbol. +-- The second argument is called to emit the function's arguments. +{-# INLINE emitFun #-} +emitFun :: Fun f -> Builder f -> Builder f +emitFun (MkFun f) inner = emitSymbolBuilder (Symbol True f 0) inner + +-- Emit a variable. +{-# INLINE emitVar #-} +emitVar :: Var -> Builder f +emitVar (MkVar x) = emitSymbolBuilder (Symbol False x 1) mempty + +-- Emit a whole termlist. +{-# INLINE emitTermList #-} +emitTermList :: TermList f -> Builder f +emitTermList (TermList lo hi array) = + Builder $ checked (hi-lo) $ + getArray $ \marray -> + getIndex $ \n -> + let k = sizeOf (fromSymbol __) in + liftST (copyByteArray marray (n*k) array (lo*k) ((hi-lo)*k)) `then_` + putIndex (n + hi-lo) diff --git a/src/Twee/Utils.hs b/src/Twee/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Twee/Utils.hs @@ -0,0 +1,89 @@ +-- | Miscellaneous utility functions. + +{-# LANGUAGE CPP #-} +module Twee.Utils where + +import Control.Arrow((&&&)) +import Control.Exception +import Data.List(groupBy, sortBy) +import Data.Ord(comparing) +import System.IO + +repeatM :: Monad m => m a -> m [a] +repeatM = sequence . repeat + +partitionBy :: Ord b => (a -> b) -> [a] -> [[a]] +partitionBy value = + map (map fst) . + groupBy (\x y -> snd x == snd y) . + sortBy (comparing snd) . + map (id &&& value) + +collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)] +collate f = map g . partitionBy fst + where + g xs = (fst (head xs), f (map snd xs)) + +isSorted :: Ord a => [a] -> Bool +isSorted xs = and (zipWith (<=) xs (tail xs)) + +isSortedBy :: Ord b => (a -> b) -> [a] -> Bool +isSortedBy f xs = isSorted (map f xs) + +usort :: Ord a => [a] -> [a] +usort = usortBy compare + +usortBy :: (a -> a -> Ordering) -> [a] -> [a] +usortBy f = map head . groupBy (\x y -> f x y == EQ) . sortBy f + +sortBy' :: Ord b => (a -> b) -> [a] -> [a] +sortBy' f = map snd . sortBy (comparing fst) . map (\x -> (f x, x)) + +usortBy' :: Ord b => (a -> b) -> [a] -> [a] +usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x)) + +orElse :: Ordering -> Ordering -> Ordering +EQ `orElse` x = x +x `orElse` _ = x + +unbuffered :: IO a -> IO a +unbuffered x = do + buf <- hGetBuffering stdout + bracket_ + (hSetBuffering stdout NoBuffering) + (hSetBuffering stdout buf) + x + +newtype Max a = Max { getMax :: Maybe a } + +getMaxWith :: Ord a => a -> Max a -> a +getMaxWith x (Max (Just y)) = x `max` y +getMaxWith x (Max Nothing) = x + +instance Ord a => Monoid (Max a) where + mempty = Max Nothing + Max (Just x) `mappend` y = Max (Just (getMaxWith x y)) + Max Nothing `mappend` y = y + +newtype Min a = Min { getMin :: Maybe a } + +getMinWith :: Ord a => a -> Min a -> a +getMinWith x (Min (Just y)) = x `min` y +getMinWith x (Min Nothing) = x + +instance Ord a => Monoid (Min a) where + mempty = Min Nothing + Min (Just x) `mappend` y = Min (Just (getMinWith x y)) + Min Nothing `mappend` y = y + +labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)] +labelM f = mapM (\x -> do { y <- f x; return (x, y) }) + +#if __GLASGOW_HASKELL__ < 710 +isSubsequenceOf :: Ord a => [a] -> [a] -> Bool +[] `isSubsequenceOf` ys = True +(x:xs) `isSubsequenceOf` [] = False +(x:xs) `isSubsequenceOf` (y:ys) + | x == y = xs `isSubsequenceOf` ys + | otherwise = (x:xs) `isSubsequenceOf` ys +#endif diff --git a/src/errors.h b/src/errors.h new file mode 100644 --- /dev/null +++ b/src/errors.h @@ -0,0 +1,3 @@ +-- Inspired by Agda's undefined.h +#define __ ERROR("internal error") +#define ERROR(msg) (error (__FILE__ ++ ", line " ++ show (__LINE__ :: Int) ++ ": " ++ msg)) diff --git a/tests/ROB007-1.p b/tests/ROB007-1.p new file mode 100644 --- /dev/null +++ b/tests/ROB007-1.p @@ -0,0 +1,41 @@ +% Goes into a loop! + +%-------------------------------------------------------------------------- +% File : ROB007-1 : TPTP v6.2.0. Released v1.0.0. +% Domain : Robbins Algebra +% Problem : Absorbed within negation element => Boolean +% Version : [Win90] (equality) axioms. +% English : If there exist a, b such that -(a+b) = -b, then the algebra +% is Boolean. + +% Refs : [HMT71] Henkin et al. (1971), Cylindrical Algebras +% : [Win90] Winker (1990), Robbins Algebra: Conditions that make a +% : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit +% Source : [Win90] +% Names : Theorem 1.2 [Win90] +% : RA5 [LW92] + +% Status : Unknown +% Rating : 1.00 v2.0.0 +% Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 2 RR) +% Number of atoms : 5 ( 5 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 4 ( 2 constant; 0-2 arity) +% Number of variables : 7 ( 0 singleton) +% Maximal term depth : 6 ( 3 average) +% SPC : CNF_UNK_UEQ + +% Comments : Commutativity, associativity, and Huntington's axiom +% axiomatize Boolean algebra. +%-------------------------------------------------------------------------- +%----Include axioms for Robbins algebra +include('Axioms/ROB001-0.ax'). +%-------------------------------------------------------------------------- +cnf(condition,hypothesis, + ( negate(add(a,b)) = negate(b) )). + +cnf(prove_huntingtons_axiom,negated_conjecture, + ( add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b )). + +%-------------------------------------------------------------------------- diff --git a/tests/abelian.p b/tests/abelian.p new file mode 100644 --- /dev/null +++ b/tests/abelian.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('0', X) = X). +cnf(a, axiom, '+'(X, '-'(X)) = '0'). diff --git a/tests/and-or.p b/tests/and-or.p new file mode 100644 --- /dev/null +++ b/tests/and-or.p @@ -0,0 +1,12 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '*'(X, Y) = '*'(Y, X)). +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '+'(X, '0') = X). +cnf(a, axiom, '*'(X, '0') = '0'). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(a, axiom, '+'(X, '*'(Y, Z)) = '*'('+'(X, Y), '+'(X, Z))). +cnf(a, axiom, not(not(X)) = X). +cnf(a, axiom, not('+'(X, Y)) = '*'(not(X), not(Y))). +cnf(a, axiom, '+'(X, not(X)) = '1'). +cnf(a, axiom, '*'(X, not(X)) = '0'). diff --git a/tests/append-rev.p b/tests/append-rev.p new file mode 100644 --- /dev/null +++ b/tests/append-rev.p @@ -0,0 +1,4 @@ +cnf(a, axiom, rev(rev(X)) = X). +cnf(a, axiom, '++'(X,'++'(Y,Z)) = '++'('++'(X,Y),Z)). +cnf(a, axiom, '++'(rev(X),rev(Y)) = rev('++'(Y,X))). +cnf(a, axiom, '++'(a,rev(b)) != rev('++'(b, rev(a)))). diff --git a/tests/diff.p b/tests/diff.p new file mode 100644 --- /dev/null +++ b/tests/diff.p @@ -0,0 +1,4 @@ +cnf(a, axiom, diff(X, diff(Y, X)) = X). +cnf(a, axiom, diff(X, diff(X, Y)) = diff(Y, diff(Y, X))). +cnf(a, axiom, diff(diff(X, Y), Z) = diff(diff(X, Z), diff(Y, Z))). +cnf(a, axiom, diff(diff(a, c), b) != diff(diff(a, b), c)). diff --git a/tests/groupoid.p b/tests/groupoid.p new file mode 100644 --- /dev/null +++ b/tests/groupoid.p @@ -0,0 +1,3 @@ +% Entropic groupoid, taken from unfailing completion paper +cnf(a, axiom, '*'('*'(X,Y),'*'(Z,W)) = '*'('*'(X,Z),'*'(Y,W))). +cnf(a, axiom, '*'('*'(X,Y),X) = X). diff --git a/tests/lat.p b/tests/lat.p new file mode 100644 --- /dev/null +++ b/tests/lat.p @@ -0,0 +1,16 @@ +cnf(idempotence_of_meet, axiom, meet(X, X)=X). +cnf(idempotence_of_join, axiom, join(X, X)=X). +cnf(absorption1, axiom, meet(X, join(X, Y))=X). +cnf(absorption2, axiom, join(X, meet(X, Y))=X). +cnf(commutativity_of_meet, axiom, meet(X, Y)=meet(Y, X)). +cnf(commutativity_of_join, axiom, join(X, Y)=join(Y, X)). +cnf(associativity_of_meet, axiom, + meet(meet(X, Y), Z)=meet(X, meet(Y, Z))). +cnf(associativity_of_join, axiom, + join(join(X, Y), Z)=join(X, join(Y, Z))). +cnf(equation_H34, axiom, + meet(X, join(Y, meet(Z, U)))=meet(X, + join(Y, meet(Z, join(Y, meet(U, join(Y, Z))))))). +cnf(prove_H28, axiom, + meet(a, join(b, meet(a, meet(c, d))))!=meet(a, + join(b, meet(c, meet(d, join(a, meet(b, d))))))). diff --git a/tests/lcl.p b/tests/lcl.p new file mode 100644 --- /dev/null +++ b/tests/lcl.p @@ -0,0 +1,7 @@ +cnf(wajsberg_1, axiom, implies(truth, X)=X). +cnf(wajsberg_3, axiom, + implies(implies(X, Y), Y)=implies(implies(Y, X), X)). +cnf(wajsberg_4, axiom, + implies(implies(not(X), not(Y)), implies(Y, X))=truth). +cnf(lemma_antecedent, axiom, implies(X, Y)=implies(Y, X)). +cnf(prove_wajsberg_lemma, axiom, x!=y). diff --git a/tests/length.p b/tests/length.p new file mode 100644 --- /dev/null +++ b/tests/length.p @@ -0,0 +1,2 @@ +cnf(a, axiom, '++'(Xs, '++'(Ys, Zs)) = '++'('++'(Xs, Ys), Zs)). +cnf(a, axiom, length('++'(Xs, Ys)) = length('++'(Ys, Xs))). diff --git a/tests/length2.p b/tests/length2.p new file mode 100644 --- /dev/null +++ b/tests/length2.p @@ -0,0 +1,3 @@ +cnf(a, axiom, '++'(Xs, '++'(Ys, Zs)) = '++'('++'(Xs, Ys), Zs)). +cnf(a, axiom, length('++'(Xs, Ys)) = length('++'(Ys, Xs))). +cnf(a, axiom, length('++'('++'(c,a),b)) != length('++'(a,'++'(b,c)))). diff --git a/tests/length3.p b/tests/length3.p new file mode 100644 --- /dev/null +++ b/tests/length3.p @@ -0,0 +1,2 @@ +cnf(a, axiom, length('++'(Xs, '++'(Ys, '++'(Zs, Ws)))) = length('++'(Ws, '++'(Xs, '++'(Ys, Zs))))). +cnf(a, axiom, length('++'(Xs, '++'(Xs, '++'(Ys, Zs)))) = length('++'(Xs, '++'(Ys, '++'(Zs, Xs))))). diff --git a/tests/loop.p b/tests/loop.p new file mode 100644 --- /dev/null +++ b/tests/loop.p @@ -0,0 +1,6 @@ +cnf(a, axiom, '*'(X, '^'(X, Y)) = Y). +cnf(a, axiom, '^'(X, '*'(X, Y)) = Y). +cnf(a, axiom, '*'('/'(X, Y), Y) = X). +cnf(a, axiom, '/'('*'(X, Y), Y) = X). +cnf(a, axiom, '*'(X, '*'(Y, '*'(X, Z))) = '*'('*'('*'(X, Y), X), Z)). +cnf(a, axiom, '^'(a,a) != '/'(a,a)). diff --git a/tests/loop2.p b/tests/loop2.p new file mode 100644 --- /dev/null +++ b/tests/loop2.p @@ -0,0 +1,6 @@ +cnf(a, axiom, mult(X, ld(X, Y)) = Y). +cnf(a, axiom, ld(X, mult(X, Y)) = Y). +cnf(a, axiom, mult(rd(X, Y), Y) = X). +cnf(a, axiom, rd(mult(X, Y), Y) = X). +cnf(a, axiom, mult(X, mult(Y, mult(X, Z))) = mult(mult(mult(X, Y), X), Z)). +cnf(a, axiom, mult(a,rd(b,b)) != a). diff --git a/tests/lukasiewicz.p b/tests/lukasiewicz.p new file mode 100644 --- /dev/null +++ b/tests/lukasiewicz.p @@ -0,0 +1,6 @@ +cnf(a, axiom, implies(true, X) = X). +cnf(a, axiom, implies(implies(X, Y), implies(implies(Y, Z), implies(X, Z))) = true). +cnf(a, axiom, implies(implies(not(X), not(Y)), implies(Y, X)) = true). +cnf(a, axiom, implies(implies(X, Y), Y) = implies(implies(Y, X), X)). +cnf(a, axiom, or(X, Y) = implies(not(X), Y)). +cnf(a, axiom, or(a,or(b,c)) != or(or(a,b),c)). diff --git a/tests/martin-nipkow-2.p b/tests/martin-nipkow-2.p new file mode 100644 --- /dev/null +++ b/tests/martin-nipkow-2.p @@ -0,0 +1,1 @@ +cnf(a, axiom, '*'('*'(X,X),Y) = '*'(Y,'*'(X,X))). diff --git a/tests/martin-nipkow.p b/tests/martin-nipkow.p new file mode 100644 --- /dev/null +++ b/tests/martin-nipkow.p @@ -0,0 +1,1 @@ +cnf(a, axiom, '*'('*'(X,Y),Z) = '*'(Z,'*'(X,Y))). diff --git a/tests/nand.p b/tests/nand.p new file mode 100644 --- /dev/null +++ b/tests/nand.p @@ -0,0 +1,37 @@ +%-------------------------------------------------------------------------- +% File : LAT071-1 : TPTP v6.2.0. Released v2.6.0. +% Domain : Lattice Theory (Orthomodularlattices) +% Problem : Given single axiom OML-21C, prove associativity +% Version : [MRV03] (equality) axioms. +% English : Given a single axiom candidate OML-21C for orthomodular lattices +% (OML) in terms of the Sheffer Stroke, prove a Sheffer stroke form +% of associativity. + +% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt +% Source : [MRV03] +% Names : OML-21C-associativity [MRV03] + +% Status : Open +% Rating : 1.00 v2.6.0 +% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) +% Number of atoms : 2 ( 2 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 4 ( 3 constant; 0-2 arity) +% Number of variables : 4 ( 2 singleton) +% Maximal term depth : 6 ( 4 average) +% SPC : CNF_UNK_UEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Single axiom OML-21C +cnf(oml_21C,axiom, + ( f(f(B,A),f(f(f(f(B,A),A),f(C,A)),f(f(A,A),D))) = A )). + +cnf(a, axiom, f(z, f(z, z)) = k). + +%----Denial of Sheffer stroke associativity +cnf(associativity,negated_conjecture, + ( f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))) )). + +%-------------------------------------------------------------------------- diff --git a/tests/nicomachus.p b/tests/nicomachus.p new file mode 100644 --- /dev/null +++ b/tests/nicomachus.p @@ -0,0 +1,18 @@ +cnf(a, axiom, plus(X, Y) = plus(Y, X)). +cnf(a, axiom, plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)). +cnf(a, axiom, times(X, Y) = times(Y, X)). +cnf(a, axiom, times(X, times(Y, Z)) = times(times(X, Y), Z)). +cnf(a, axiom, plus(X, zero) = X). +cnf(a, axiom, times(X, zero) = zero). +cnf(a, axiom, times(X, one) = X). +cnf(a, axiom, times(X, plus(Y, Z)) = plus(times(X, Y), times(X, Z))). +cnf(a, axiom, times(plus(X, Y), Z) = plus(times(X, Z), times(Y, Z))). +cnf(a, axiom, plus(s(X), Y) = s(plus(X, Y))). +cnf(a, axiom, times(s(X), Y) = plus(Y, times(X, Y))). +cnf(a, axiom, sum(zero) = zero). +cnf(a, axiom, sum(s(N)) = plus(s(N), sum(N))). +cnf(a, axiom, cubes(zero) = zero). +cnf(a, axiom, cubes(s(N)) = plus(times(s(N), times(s(N), s(N))), cubes(N))). +cnf(a, axiom, plus(sum(N), sum(N)) = times(N, s(N))). +cnf(a, axiom, times(sum(a), sum(a)) = cubes(a)). +cnf(a, axiom, times(sum(s(a)), sum(s(a))) != cubes(s(a))). diff --git a/tests/plus-combinator.p b/tests/plus-combinator.p new file mode 100644 --- /dev/null +++ b/tests/plus-combinator.p @@ -0,0 +1,2 @@ +cnf(a, axiom, app(app('+', X), Y) = app(app('+', Y), X)). +cnf(a, axiom, app(app('+', X), app(app('+', Y), Z)) = app(app('+', app(app('+', X), Y)), Z)). diff --git a/tests/plus-times.p b/tests/plus-times.p new file mode 100644 --- /dev/null +++ b/tests/plus-times.p @@ -0,0 +1,8 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '*'(X, Y) = '*'(Y, X)). +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '+'(X, '0') = X). +cnf(a, axiom, '*'(X, '0') = '0'). +cnf(a, axiom, '*'(X, '1') = X). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). diff --git a/tests/plus.p b/tests/plus.p new file mode 100644 --- /dev/null +++ b/tests/plus.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'(X, '0') = X). +cnf(a, axiom, '+'(X, X) = X). diff --git a/tests/pretty.p b/tests/pretty.p new file mode 100644 --- /dev/null +++ b/tests/pretty.p @@ -0,0 +1,19 @@ +cnf(a, axiom, length('[]') = '0'). +cnf(a, axiom, '+'(X, '0') = X). +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '++'(Xs, '[]') = Xs). +cnf(a, axiom, '++'('[]', Xs) = Xs). +cnf(a, axiom, '++'(Xs, '++'(Ys, Zs)) = '++'('++'(Xs, Ys), Zs)). +cnf(a, axiom, length('++'(Xs, Ys)) = '+'(length(Xs), length(Ys))). +cnf(a, axiom, nest('0', X) = X). +cnf(a, axiom, '<>'(X, text('[]')) = X). +cnf(a, axiom, nest('+'(I, J), X) = nest(I, nest(J, X))). +cnf(a, axiom, '$$'(X, '$$'(Y, Z)) = '$$'('$$'(X, Y), Z)). +cnf(a, axiom, '<>'(X, nest(I, Y)) = '<>'(X, Y)). +cnf(a, axiom, '<>'(nest(I, X), Y) = nest(I, '<>'(X, Y))). +cnf(a, axiom, '<>'('$$'(X, Y), Z) = '$$'(X, '<>'(Y, Z))). +cnf(a, axiom, '<>'('<>'(X, Y), Z) = '<>'(X, '<>'(Y, Z))). +cnf(a, axiom, '<>'(text(X), text(Y)) = text('++'(X, Y))). +cnf(a, axiom, '$$'(nest(I, X), nest(I, Y)) = nest(I, '$$'(X, Y))). +cnf(a, axiom, '<>'(text(Xs), '$$'('<>'(text('[]'), X), Y)) = '$$'('<>'(text(Xs), X), nest(length(Xs), Y))). diff --git a/tests/ring.p b/tests/ring.p new file mode 100644 --- /dev/null +++ b/tests/ring.p @@ -0,0 +1,10 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('0', X) = X). +cnf(a, axiom, '+'(X, '-'(X)) = '0'). +%'*'(X, '1') = X +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(a, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(a, axiom, X = '*'(X, '*'(X, X))). +cnf(a, axiom, '*'(a, b) != '*'(b, a)). diff --git a/tests/ring2.p b/tests/ring2.p new file mode 100644 --- /dev/null +++ b/tests/ring2.p @@ -0,0 +1,9 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('0', X) = X). +cnf(a, axiom, '+'(X, '-'(X)) = '0'). +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(a, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(a, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, '*'(X, X)))))). +cnf(a, axiom, '*'(a, b) != '*'(b, a)). diff --git a/tests/ring3.p b/tests/ring3.p new file mode 100644 --- /dev/null +++ b/tests/ring3.p @@ -0,0 +1,10 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('0', X) = X). +cnf(a, axiom, '+'(X, '-'(X)) = '0'). +%'*'(X, '1') = X +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(a, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(a, axiom, X = '*'(X, '*'(X, '*'(X, X)))). +cnf(a, axiom, '*'(a, b) != '*'(b, a)). diff --git a/tests/ring4.p b/tests/ring4.p new file mode 100644 --- /dev/null +++ b/tests/ring4.p @@ -0,0 +1,10 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('0', X) = X). +cnf(a, axiom, '+'(X, '-'(X)) = '0'). +%'*'(X, '1') = X +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(a, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(a, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, X))))). +cnf(a, axiom, '*'(a, b) != '*'(b, a)). diff --git a/tests/robbins-easy.p b/tests/robbins-easy.p new file mode 100644 --- /dev/null +++ b/tests/robbins-easy.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'('-'('+'('-'(X), Y)), '-'('+'('-'(X), '-'(Y)))) = X). +cnf(a, axiom, '-'('+'('-'('+'(a, b)), '-'('+'(a, '-'(b))))) != a). diff --git a/tests/robbins-hard.p b/tests/robbins-hard.p new file mode 100644 --- /dev/null +++ b/tests/robbins-hard.p @@ -0,0 +1,5 @@ +cnf(a, axiom, '-+'(X, Y) = '-'('+'(X, Y))). +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/robbins-quite-hard.p b/tests/robbins-quite-hard.p new file mode 100644 --- /dev/null +++ b/tests/robbins-quite-hard.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '+'(X, X) != X). diff --git a/tests/robbins2.p b/tests/robbins2.p new file mode 100644 --- /dev/null +++ b/tests/robbins2.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '-'('-'(a)) != a). diff --git a/tests/semigroup.p b/tests/semigroup.p new file mode 100644 --- /dev/null +++ b/tests/semigroup.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(a, axiom, '*'(X, X) = '*'(X, '*'(X, X))). +cnf(a, axiom, '*'('*'(X, X), Y) = '*'(Y, '*'(X, X))). +cnf(a, axiom, '*'('*'(a, b), '*'(a, b)) != '*'('*'(a, a), '*'(b, b))). diff --git a/tests/semigroup2.p b/tests/semigroup2.p new file mode 100644 --- /dev/null +++ b/tests/semigroup2.p @@ -0,0 +1,26 @@ +% File : GRP'1'96'-''1' : TPTP v6.'1'.'0'. Released v2.2.'0'. +% Domain : Group Theory (Semigroups) +% Problem : In semigroups, xyyy=yyyx '->' (uy)'^'9 = u'^'9v'^'9. +% Version : [MP96] (equality) axioms. +% English : +% Refs : [McC98] McCune ('1'998), Email to G. Sutcliffe +% : [MP96] McCune & Padmanabhan ('1'996), Automated Deduction in Eq +% : [McC95] McCune ('1'995), Four Challenge Problems in Equational L +% Source : [McC98] +% Names : CS'-'3 [MP96] +% : Problem B [McC95] +% Status : Unsatisfiable +% Rating : '1'.'0''0' v4.'0'.'1', '0'.93 v4.'0'.'0', '0'.92 v3.7.'0', '0'.89 v3.4.'0', '1'.'0''0' v3.3.'0', '0'.93 v3.'1'.'0', '1'.'0''0' v2.2.'1' +% Syntax : Number of clauses : 3 ( '0' non'-'Horn; 3 unit; '1' RR) +% Number of atoms : 3 ( 3 equality) +% Maximal clause size : '1' ( '1' average) +% Number of predicates : '1' ( '0' propositional; 2'-'2 arity) +% Number of functors : 3 ( 2 constant; '0''-'2 arity) +% Number of variables : 5 ( '0' singleton) +% Maximal term depth : '1'8 ( 8 average) +% SPC : CNF_UNS_RFO_PEQ_UEQ +% Comments : The problem was originally posed for cancellative semigroups, +% Otter does this with a nonstandard representation [MP96]. +cnf(a, axiom, '*'('*'(A,B),C)='*'(A,'*'(B,C))). +cnf(a, axiom, '*'(A,'*'(B,'*'(B,B)))='*'(B,'*'(B,'*'(B,A)))). +cnf(a, axiom, '*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,b))))))))))))))))) != '*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,b)))))))))))))))))). diff --git a/tests/winkler-easy.p b/tests/winkler-easy.p new file mode 100644 --- /dev/null +++ b/tests/winkler-easy.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'(X, X) = X). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winkler.p b/tests/winkler.p new file mode 100644 --- /dev/null +++ b/tests/winkler.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'(c, c) = c). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/winkler2.p b/tests/winkler2.p new file mode 100644 --- /dev/null +++ b/tests/winkler2.p @@ -0,0 +1,6 @@ +% Needs case split on X < c. +cnf(a, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(a, axiom, '+'(c, d) = c). +cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(a, axiom, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a). diff --git a/tests/y-easier.p b/tests/y-easier.p new file mode 100644 --- /dev/null +++ b/tests/y-easier.p @@ -0,0 +1,5 @@ +cnf(a, axiom, app(app(k, X), Y) = X). +cnf(a, axiom, app(app(app(s, X), Y), Z) = app(app(X, Z), app(Y, Z))). +cnf(a, axiom, app(app(app(b, X), Y), Z) = app(X, app(Y, Z))). +cnf(a, axiom, app(m, X) = app(X, X)). +cnf(a, axiom, app(X, a(X)) != app(a(X), app(X, a(X)))). diff --git a/tests/y-hard.p b/tests/y-hard.p new file mode 100644 --- /dev/null +++ b/tests/y-hard.p @@ -0,0 +1,3 @@ +cnf(a, axiom, '@'('@'(k, X), Y) = X). +cnf(a, axiom, '@'('@'('@'(s, X), Y), Z) = '@'('@'(X, Z), '@'(Y, Z))). +cnf(a, axiom, '@'(X, a) != '@'(a, '@'(X, a))). diff --git a/tests/y-inconsistent.p b/tests/y-inconsistent.p new file mode 100644 --- /dev/null +++ b/tests/y-inconsistent.p @@ -0,0 +1,13 @@ +% Obviously inconsistent because w X Y = X X Y = X. +% Interesting thing is the final rules: +% w '@' X'0' '->' X'0' '@' X'0' (unoriented) +% X'0' '@' X'0' '->' w '@' X'0' (unoriented) +% X'0' '@' X'1' '->' X'0' '@' ? (weak on [X'1']) +% X'0' '@' X'1' '->' w '@' X'0' (unoriented) +% We should maybe use X'0' '@' X'1' '->' X'0' '@' ? to simplify the +% other rules (many of which would still be oriented the same) +cnf(a, axiom, '@'('@'('@'(c, X), Y), Z) = '@'(X, '@'(Y, Z))). +cnf(a, axiom, '@'('@'('@'(f, X), Y), Z) = '@'('@'(X, Z), Y)). +cnf(a, axiom, '@'(w, X) = '@'(X, X)). +cnf(a, axiom, '@'('@'(w, X), Y) = X). +cnf(a, axiom, '@'(X, a) != '@'(a, '@'(X, a))). diff --git a/tests/y-really-hard.p b/tests/y-really-hard.p new file mode 100644 --- /dev/null +++ b/tests/y-really-hard.p @@ -0,0 +1,3 @@ +cnf(a, axiom, '@'('@'(k, X), Y) = X). +cnf(a, axiom, '@'('@'('@'(s, X), Y), Z) = '@'('@'(X, Z), '@'(Y, Z))). +cnf(a, axiom, '@'(X, a(X)) != '@'(a(X), '@'(X, a(X)))). diff --git a/tests/y.p b/tests/y.p new file mode 100644 --- /dev/null +++ b/tests/y.p @@ -0,0 +1,4 @@ +cnf(a, axiom, '@'('@'('@'(c, X), Y), Z) = '@'(X, '@'(Y, Z))). +cnf(a, axiom, '@'('@'('@'(f, X), Y), Z) = '@'('@'(X, Z), Y)). +cnf(a, axiom, '@'(w, X) = '@'(X, X)). +cnf(a, axiom, '@'(X, a) != '@'(a, '@'(X, a))). diff --git a/twee.cabal b/twee.cabal new file mode 100644 --- /dev/null +++ b/twee.cabal @@ -0,0 +1,76 @@ +name: twee +version: 0.1 +synopsis: An equational theorem prover +homepage: http://github.com/nick8325/twee +license: BSD3 +license-file: LICENSE +author: Nick Smallbone +maintainer: nicsma@chalmers.se +category: Theorem Provers +build-type: Simple +cabal-version: >=1.10 +extra-source-files: README src/errors.h tests/*.p +description: + Twee is an experimental equational theorem prover based on + Knuth-Bendix completion. + . + Given a set of equational axioms and a set of equational + conjectures it will try to prove the conjectures. + It will terminate if the conjectures are true but normally + fail to terminate if they are false. + . + The input problem should be in TPTP format (see + http://www.tptp.org). You can use types and quantifiers, but apart + from that the problem must be equational. + +source-repository head + type: git + location: git://github.com/nick8325/twee.git + branch: master + +library + exposed-modules: + Twee + Twee.Array + Twee.Base + Twee.Pretty + Twee.Constraints + Twee.Index + Twee.Indexes + Twee.Queue + Twee.Rule + Twee.Term + Twee.Term.Core + Twee.Utils + Twee.KBO + Twee.LPO + Twee.Label + build-depends: + base >= 4 && < 5, + containers, + transformers, + dlist, + pretty, + heaps, + ghc-prim, + primitive, + reflection, + array + hs-source-dirs: src + include-dirs: src + ghc-options: -W -fno-warn-incomplete-patterns -fno-full-laziness + default-language: Haskell2010 + +executable twee + main-is: executable/Main.hs + default-language: Haskell2010 + build-depends: base, + twee, + containers, + transformers, + pretty, + array, + reflection, + split, + jukebox >= 0.2 + ghc-options: -W -fno-warn-incomplete-patterns -fno-full-laziness