packages feed

twee (empty) → 0.1

raw patch · 61 files changed

+4241/−0 lines, 61 filesdep +arraydep +basedep +containerssetup-changed

Dependencies added: array, base, containers, dlist, ghc-prim, heaps, jukebox, pretty, primitive, reflection, split, transformers, twee

Files

+ LICENSE view
@@ -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.
+ README view
@@ -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!
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ executable/Main.hs view
@@ -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 "<function>" "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))
+ src/Twee.hs view
@@ -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
+ src/Twee/Array.hs view
@@ -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')
+ src/Twee/Base.hs view
@@ -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
+ src/Twee/Constraints.hs view
@@ -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)
+ src/Twee/Index.hs view
@@ -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
+ src/Twee/Indexes.hs view
@@ -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))
+ src/Twee/KBO.hs view
@@ -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
+ src/Twee/LPO.hs view
@@ -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")
+ src/Twee/Label.hs view
@@ -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)
+ src/Twee/Pretty.hs view
@@ -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)))
+ src/Twee/Queue.hs view
@@ -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+
+ src/Twee/Rule.hs view
@@ -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)
+ src/Twee/Term.hs view
@@ -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)
+ src/Twee/Term/Core.hs view
@@ -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)
+ src/Twee/Utils.hs view
@@ -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
+ src/errors.h view
@@ -0,0 +1,3 @@+-- Inspired by Agda's undefined.h+#define __ ERROR("internal error")+#define ERROR(msg) (error (__FILE__ ++ ", line " ++ show (__LINE__ :: Int) ++ ": " ++ msg))
+ tests/ROB007-1.p view
@@ -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 )).++%--------------------------------------------------------------------------
+ tests/abelian.p view
@@ -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').
+ tests/and-or.p view
@@ -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').
+ tests/append-rev.p view
@@ -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)))).
+ tests/diff.p view
@@ -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)).
+ tests/groupoid.p view
@@ -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).
+ tests/lat.p view
@@ -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))))))).
+ tests/lcl.p view
@@ -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).
+ tests/length.p view
@@ -0,0 +1,2 @@+cnf(a, axiom, '++'(Xs, '++'(Ys, Zs)) = '++'('++'(Xs, Ys), Zs)).+cnf(a, axiom, length('++'(Xs, Ys)) = length('++'(Ys, Xs))).
+ tests/length2.p view
@@ -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)))).
+ tests/length3.p view
@@ -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))))).
+ tests/loop.p view
@@ -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)).
+ tests/loop2.p view
@@ -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).
+ tests/lukasiewicz.p view
@@ -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)).
+ tests/martin-nipkow-2.p view
@@ -0,0 +1,1 @@+cnf(a, axiom, '*'('*'(X,X),Y) = '*'(Y,'*'(X,X))).
+ tests/martin-nipkow.p view
@@ -0,0 +1,1 @@+cnf(a, axiom, '*'('*'(X,Y),Z) = '*'(Z,'*'(X,Y))).
+ tests/nand.p view
@@ -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))) )).++%--------------------------------------------------------------------------
+ tests/nicomachus.p view
@@ -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))).
+ tests/plus-combinator.p view
@@ -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)).
+ tests/plus-times.p view
@@ -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))).
+ tests/plus.p view
@@ -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).
+ tests/pretty.p view
@@ -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))).
+ tests/ring.p view
@@ -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)).
+ tests/ring2.p view
@@ -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)).
+ tests/ring3.p view
@@ -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)).
+ tests/ring4.p view
@@ -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)).
+ tests/robbins-easy.p view
@@ -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).
+ tests/robbins-hard.p view
@@ -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).
+ tests/robbins-quite-hard.p view
@@ -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).
+ tests/robbins2.p view
@@ -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).
+ tests/semigroup.p view
@@ -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))).
+ tests/semigroup2.p view
@@ -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)))))))))))))))))).
+ tests/winkler-easy.p view
@@ -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).
+ tests/winkler.p view
@@ -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).
+ tests/winkler2.p view
@@ -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).
+ tests/y-easier.p view
@@ -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)))).
+ tests/y-hard.p view
@@ -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))).
+ tests/y-inconsistent.p view
@@ -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))).
+ tests/y-really-hard.p view
@@ -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)))).
+ tests/y.p view
@@ -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))).
+ twee.cabal view
@@ -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