packages feed

twee 2.0 → 2.1

raw patch · 55 files changed

+656/−6152 lines, 55 filesdep +twee-libdep −dlistdep −ghc-primdep −primitivedep ~basedep ~jukebox

Dependencies added: twee-lib

Dependencies removed: dlist, ghc-prim, primitive, transformers, twee

Dependency ranges changed: base, jukebox

Files

LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2015, Nick Smallbone+Copyright (c) 2015-2017, Nick Smallbone  All rights reserved.
+ Main.hs view
@@ -0,0 +1,625 @@+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-}+import Control.Monad+import Data.Char+import Data.Either+import Twee hiding (message)+import Twee.Base hiding (char, lookup, vars)+import Twee.Rule(lhs, rhs, unorient)+import Twee.Equation+import qualified Twee.Proof as Proof+import Twee.Proof hiding (Config, defaultConfig)+import qualified Twee.Join as Join+import Twee.Utils+import qualified Twee.CP as CP+import Data.Ord+import qualified Data.Map.Strict as Map+import qualified Twee.KBO as KBO+import Data.List.Split+import Data.List+import Data.Maybe+import Jukebox.Options+import Jukebox.Toolbox+import Jukebox.Name hiding (lhs, rhs)+import qualified Jukebox.Form as Jukebox+import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Lemma)+import Jukebox.Tools.EncodeTypes+import Jukebox.TPTP.Print+import Jukebox.Tools.HornToUnit+import qualified Data.IntMap.Strict as IntMap+import System.IO+import System.Exit+import qualified Data.Set as Set++data MainFlags =+  MainFlags {+    flags_proof :: Bool,+    flags_trace :: Maybe (String, String) }++parseMainFlags :: OptionParser MainFlags+parseMainFlags =+  MainFlags <$> proof <*> trace+  where+    proof =+      inGroup "Output options" $+      bool "proof" ["Produce proofs (on by default)."]+      True+    trace =+      expert $+      inGroup "Output options" $+      flag "trace"+        ["Write a Prolog-format execution trace to this file (off by default)."]+        Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)+    argModule = arg "<module>" "expected a Prolog module name" Just++parseConfig :: OptionParser Config+parseConfig =+  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*>+    (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*>+    (Join.Config <$> ground_join <*> connectedness <*> set_join) <*>+    (Proof.Config <$> all_lemmas <*> flat_proof <*> show_instances)+  where+    maxSize =+      inGroup "Resource limits" $+      flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] maxBound argNum+    maxCPs =+      inGroup "Resource limits" $+      flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum+    maxCPDepth =+      inGroup "Resource limits" $+      flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum+    simplify =+      expert $+      inGroup "Completion heuristics" $+      bool "simplify"+        ["Simplify rewrite rules with respect to one another (on by default)."]+        True+    normPercent =+      expert $+      inGroup "Completion heuristics" $+      defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" (cfg_renormalise_percent) argNum+    lweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" (CP.cfg_lhsweight . cfg_critical_pairs) argNum+    rweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" (CP.cfg_rhsweight . cfg_critical_pairs) argNum+    funweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "fun-weight" "Weight given to function symbols" (CP.cfg_funweight . cfg_critical_pairs) argNum+    varweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "var-weight" "Weight given to variable symbols" (CP.cfg_varweight . cfg_critical_pairs) argNum+    depthweight =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "depth-weight" "Weight given to critical pair depth" (CP.cfg_depthweight . cfg_critical_pairs) argNum+    dupcost =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "dup-cost" "Cost of duplicate subterms" (CP.cfg_dupcost . cfg_critical_pairs) argNum+    dupfactor =+      expert $+      inGroup "Critical pair weighting heuristics" $+      defaultFlag "dup-factor" "Size factor of duplicate subterms" (CP.cfg_dupfactor . cfg_critical_pairs) argNum+    ground_join =+      expert $+      inGroup "Critical pair joining heuristics" $+      bool "ground-joining"+        ["Test terms for ground joinability (on by default)."]+        True+    connectedness =+      expert $+      inGroup "Critical pair joining heuristics" $+      bool "connectedness"+        ["Test terms for subconnectedness (on by default)."]+        True+    set_join =+      expert $+      inGroup "Critical pair joining heuristics" $+      bool "set-join"+        ["Compute all normal forms when joining critical pairs (off by default)."]+        False+    all_lemmas =+      expert $+      inGroup "Proof presentation" $+      bool "all-lemmas"+        ["Produce a proof with one lemma for each critical pair (off by default)."]+        False+    flat_proof =+      expert $+      inGroup "Proof presentation" $+      bool "no-lemmas"+        ["Produce a proof with no lemmas (off by default).",+         "May lead to exponentially large proofs."]+        False+    show_instances =+      expert $+      inGroup "Proof presentation" $+      bool "show-instances"+        ["Show which instances of each axiom and lemma were used (off by default)."]+        False+    defaultFlag name desc field parser =+      flag name [desc ++ " (" ++ show def ++ " by default)."] def parser+      where+        def = field defaultConfig++parsePrecedence :: OptionParser [String]+parsePrecedence =+  expert $+  inGroup "Term order options" $+  fmap (splitOn ",")+  (flag "precedence" ["List of functions in descending order of precedence."] [] (arg "<function>" "expected a function name" Just))++data Constant =+  Constant {+    con_prec  :: {-# UNPACK #-} !Precedence,+    con_id    :: {-# UNPACK #-} !Jukebox.Function,+    con_arity :: {-# UNPACK #-} !Int,+    con_size  :: {-# UNPACK #-} !Int,+    con_bonus :: !Bool }+  deriving (Eq, Ord)++data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int+  deriving (Eq, Ord)++instance Sized Constant where+  size Constant{..} = con_size+instance Arity Constant where+  arity Constant{..} = con_arity++instance Pretty Constant where+  pPrint Constant{..} = text (base con_id)++instance PrettyTerm Constant where+  termStyle Constant{..}+    | "$to_" `isPrefixOf` (base con_id) = invisible+    | any isAlphaNum (base con_id) = uncurried+    | otherwise =+      case con_arity of+        1 -> prefix+        2 -> infixStyle 5+        _ -> uncurried++instance Ordered (Extended Constant) where+  lessEq t u = {-# SCC lessEq #-} KBO.lessEq t u+  lessIn model t u = {-# SCC lessIn #-} KBO.lessIn model t u++instance EqualsBonus Constant where+  hasEqualsBonus = con_bonus+  isEquals = Main.isEquals . con_id+  isTrue = Main.isTrue . con_id+  isFalse = Main.isFalse . con_id++data TweeContext =+  TweeContext {+    ctx_var     :: Jukebox.Variable,+    ctx_minimal :: Jukebox.Function,+    ctx_true    :: Jukebox.Function,+    ctx_false   :: Jukebox.Function,+    ctx_equals  :: Jukebox.Function,+    ctx_type    :: Type }++-- Convert back and forth between Twee and Jukebox.+tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Extended Constant+tweeConstant flags TweeContext{..} prec fun+  | fun == ctx_minimal = Minimal+  | otherwise = Function (Constant prec fun (Jukebox.arity fun) (sz fun) (bonus fun))+  where+    sz fun = if isType fun then 0 else 1+    bonus fun =+      (isIfeq fun && encoding flags /= Asymmetric2) ||+      Main.isEquals fun++isType :: Jukebox.Function -> Bool+isType fun = "$to_" `isPrefixOf` base (name fun)++isIfeq :: Jukebox.Function -> Bool+isIfeq fun = "$ifeq" `isPrefixOf` base (name fun)++isEquals :: Jukebox.Function -> Bool+isEquals fun = "$equals" `isPrefixOf` base (name fun)++isTrue :: Jukebox.Function -> Bool+isTrue fun = "$true" `isPrefixOf` base (name fun)++isFalse :: Jukebox.Function -> Bool+isFalse fun = "$false" `isPrefixOf` base (name fun)++jukeboxFunction :: TweeContext -> Extended Constant -> Jukebox.Function+jukeboxFunction _ (Function Constant{..}) = con_id+jukeboxFunction TweeContext{..} Minimal = ctx_minimal+jukeboxFunction TweeContext{..} (Skolem _) =+  error "Skolem variable leaked into rule"++tweeTerm :: HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term (Extended Constant)+tweeTerm flags ctx prec t = build (tm t)+  where+    tm (Jukebox.Var (Unique x _ _ ::: _)) =+      var (V (fromIntegral x))+    tm (f :@: ts) =+      app (fun (tweeConstant flags ctx (prec f) f)) (map tm ts)++jukeboxTerm :: TweeContext -> Term (Extended Constant) -> Jukebox.Term+jukeboxTerm TweeContext{..} (Var (V x)) =+  Jukebox.Var (Unique (fromIntegral x) "X" defaultRenamer ::: ctx_type)+jukeboxTerm ctx@TweeContext{..} (App f t) =+  jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts+  where+    ts = unpack t++makeContext :: Problem Clause -> TweeContext+makeContext prob = run prob $ \prob -> do+  let+    ty =+      case types' prob of+        []   -> indType+        [ty] -> ty++  var     <- newSymbol "X" ty+  minimal <- newFunction "$constant" [] ty+  true    <- newFunction "$true" [] ty+  false   <- newFunction "$false" [] ty+  equals  <- newFunction "$equals" [ty, ty] ty++  return TweeContext {+    ctx_var = var,+    ctx_minimal = minimal,+    ctx_true = true,+    ctx_false = false,+    ctx_equals = equals,+    ctx_type = ty }++-- Encode existentials so that all goals are ground.+addNarrowing :: TweeContext -> Problem Clause -> Problem Clause+addNarrowing TweeContext{..} prob =+  unchanged ++ equalityClauses+  where+    (unchanged, nonGroundGoals) = partitionEithers (map f prob)+      where+        f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])}+          | not (ground x) || not (ground y) =+            Right (inp, (x, y))+        f inp = Left inp++    equalityClauses+      | null nonGroundGoals = []+      | otherwise =+        -- Turn a != b & c != d & ...+        -- into eq(a,b)=false & eq(c,d)=false & eq(X,X)=true & true!=false (esa)+        -- and then extract the individual components (thm)+        let+          equalityLiterals =+            -- true != false+            ("true_equals_false", Neg ((ctx_true :@:) [] Jukebox.:=: (ctx_false :@: []))):+            -- eq(X,X)=true+            ("reflexivity", Pos (ctx_equals :@: [Jukebox.Var ctx_var, Jukebox.Var ctx_var] Jukebox.:=: (ctx_true :@: []))):+            -- [eq(a,b)=false, eq(c,d)=false, ...]+            [ (tag, Pos (ctx_equals :@: [x, y] Jukebox.:=: (ctx_false :@: [])))+            | (Input{tag = tag}, (x, y)) <- nonGroundGoals ]++          -- Equisatisfiable to the input clauses+          justification =+            Input {+              tag  = "new_negated_conjecture",+              kind = Jukebox.Ax NegatedConjecture,+              what =+                let form = And (map (Literal . snd) equalityLiterals) in+                ForAll (Bind (Set.fromList (vars form)) form),+              source =+                Inference "encode_existential" "esa"+                  (map (fmap toForm . fst) nonGroundGoals) }++          input tag form =+            Input {+              tag = tag,+              kind = Conj Conjecture,+              what = clause [form],+              source =+                Inference "split_conjunct" "thm" [justification] }++        in [input tag form | (tag, form) <- equalityLiterals]++data PreEquation =+  PreEquation {+    pre_name :: String,+    pre_form :: Input Form,+    pre_eqn  :: (Jukebox.Term, Jukebox.Term) }++-- Split the problem into axioms and ground goals.+identifyProblem ::+  TweeContext -> Problem Clause -> Either (Input Clause) ([PreEquation], [PreEquation])+identifyProblem TweeContext{..} prob =+  fmap partitionEithers (mapM identify prob)++  where+    pre inp x =+      PreEquation {+        pre_name = tag inp,+        pre_form = fmap toForm inp,+        pre_eqn = x }++    identify inp@Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} =+      return $ Left (pre inp (t, u))+    identify inp@Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])}+      | ground t && ground u =+        return $ Right (pre inp (t, u))+    identify inp@Input{what = Clause (Bind _ [])} =+      -- The empty clause can appear after clausification if+      -- the conjecture was trivial+      return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: []))+    identify inp = Left inp++runTwee :: GlobalFlags -> TSTPFlags -> MainFlags -> HornFlags -> Config -> [String] -> (IO () -> IO ()) -> Problem Clause -> IO Answer+runTwee globals (TSTPFlags tstp) main horn config precedence later obligs = {-# SCC runTwee #-} do+  let+    -- Encode whatever needs encoding in the problem+    ctx = makeContext obligs+    prob = addNarrowing ctx obligs++  (axioms0, goals0) <-+    case identifyProblem ctx prob of+      Left inp -> do+        mapM_ (hPutStrLn stderr) [+          "The problem contains the following clause, which is not a unit equality:",+          indent (show (pPrintClauses [inp])),+          "Twee only handles unit equality problems."]+        exitWith (ExitFailure 1)+      Right x -> return x++  let+    -- Work out a precedence for function symbols+    prec c =+      Precedence+        (isType c)+        (isNothing (elemIndex (base c) precedence))+        (fmap negate (elemIndex (base c) precedence))+        (negate (Map.findWithDefault 0 c occs))+    occs = funsOcc prob++    -- Translate everything to Twee.+    toEquation (t, u) =+      canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u)++    goals =+      [ goal n pre_name (toEquation pre_eqn)+      | (n, PreEquation{..}) <- zip [1..] goals0 ]+    axioms =+      [ Axiom n pre_name (toEquation pre_eqn)+      | (n, PreEquation{..}) <- zip [1..] axioms0 ]++    withGoals = foldl' (addGoal config) initialState goals+    withAxioms = foldl' (addAxiom config) withGoals axioms++  -- Set up tracing.+  sayTrace <-+    case flags_trace main of+      Nothing -> return $ \_ -> return ()+      Just (file, mod) -> do+        h <- openFile file WriteMode+        hSetBuffering h LineBuffering+        let put msg = hPutStrLn h msg+        put $ ":- module(" ++ mod ++ ", [step/1, lemma/1])."+        put ":- discontiguous(step/1)."+        put ":- discontiguous(lemma/1)."+        put ":- style_check(-singleton)."+        return $ \msg -> hPutStrLn h msg+  +  let+    say msg = unless (quiet globals) (putStrLn msg)+    line = say ""+    output = Output {+      output_message = \msg -> do+        say (prettyShow msg)+        sayTrace (show (traceMsg msg)) }++    traceMsg (NewActive active) =+      step "add" [traceActive active]+    traceMsg (NewEquation eqn) =+      step "hard" [traceEqn eqn]+    traceMsg (DeleteActive active) =+      step "delete" [traceActive active]+    traceMsg SimplifyQueue =+      step "simplify_queue" []+    traceMsg Interreduce =+      step "interreduce" []++    traceActive Active{..} =+      traceApp "rule" [pPrint active_id, traceEqn (unorient active_rule)]+    traceEqn (t :=: u) =+      pPrintPrec prettyNormal 6 t <+> text "=" <+> pPrintPrec prettyNormal 6 u+    traceApp f xs =+      pPrintTerm uncurried prettyNormal 0 (text f) xs++    step :: String -> [Doc] -> Doc+    step f xs = traceApp "step" [traceApp f xs] <> text "."++  say "Here is the input problem:"+  forM_ axioms $ \Axiom{..} ->+    say $ show $ nest 2 $+      describeEquation "Axiom"+        (show axiom_number) (Just axiom_name) axiom_eqn+  forM_ goals $ \Goal{..} ->+    say $ show $ nest 2 $+      describeEquation "Goal"+        (show goal_number) (Just goal_name) goal_eqn+  line++  state <- complete output config withAxioms+  line++  when (solved state && flags_proof main) $ later $ do+    let+      pres = present (cfg_proof_presentation config) (solutions state)++    sayTrace ""+    forM_ (pres_lemmas pres) $ \Lemma{..} ->+      sayTrace $ show $+        traceApp "lemma" [traceEqn (equation lemma_proof)] <> text "."++    when tstp $ do+      putStrLn "% SZS output start CNFRefutation"+      print $ pPrintProof $+        presentToJukebox ctx (curry toEquation)+          (zip (map axiom_number axioms) (map pre_form axioms0))+          (zip (map goal_number goals) (map pre_form goals0))+          pres+      putStrLn "% SZS output end CNFRefutation"+      putStrLn ""++    putStrLn "The conjecture is true! Here is a proof."+    putStrLn ""+    print $ pPrintPresentation (cfg_proof_presentation config) pres+    putStrLn ""++  when (not (quiet globals) && not (solved state)) $ later $ do+    let+      state' = interreduce config state+      score rule =+        (size (lhs rule), lhs rule,+         size (rhs rule), rhs rule)+      actives =+        sortBy (comparing (score . active_rule)) $+        IntMap.elems (st_active_ids state')++    when (tstp && configIsComplete config) $ do+      putStrLn "% SZS output start Saturation"+      print $ pPrintProof $+        map pre_form axioms0 +++        map pre_form goals0 +++        [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $+            toForm $ clause+              [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))]+        | rule <- rules state ]+      putStrLn "% SZS output end Saturation"+      putStrLn ""++    if configIsComplete config then do+      putStrLn "Ran out of critical pairs. This means the conjecture is not true."+    else do+      putStrLn "Gave up on reaching the given resource limit."+    putStrLn "Here is the final rewrite system:"+    forM_ actives $ \active ->+      putStrLn ("  " ++ prettyShow (canonicalise (active_rule active)))+    putStrLn ""++  return $+    if solved state then Unsat Unsatisfiable Nothing+    else if configIsComplete config then Sat Satisfiable Nothing+    else NoAnswer GaveUp++-- Transform a proof presentation into a Jukebox proof.+presentToJukebox ::+  TweeContext ->+  (Jukebox.Term -> Jukebox.Term -> Equation (Extended Constant)) ->+  -- Axioms, indexed by axiom number.+  [(Int, Input Form)] ->+  -- N.B. the formula here proves the negated goal.+  [(Int, Input Form)] ->+  Presentation (Extended Constant) ->+  Problem Form+presentToJukebox ctx toEquation axioms goals Presentation{..} =+  [ Input {+      tag = pg_name,+      kind = Jukebox.Ax Jukebox.Axiom,+      what = false,+      source =+        Inference "resolution" "thm"+          [-- A proof of t != u+           existentialHack pg_goal_hint (fromJust (lookup pg_number goals)),+           -- A proof of t = u+           fromJust (Map.lookup pg_number goal_proofs)] }+  | ProvedGoal{..} <- pres_goals ]++  where+    axiom_proofs =+      Map.fromList+        [ (axiom_number, fromJust (lookup axiom_number axioms))+        | Axiom{..} <- pres_axioms ]++    lemma_proofs =+      Map.fromList [(lemma_id, tstp lemma_proof) | Lemma{..} <- pres_lemmas]++    goal_proofs =+      Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals]++    tstp :: Proof (Extended Constant) -> Input Form+    tstp = deriv . derivation++    deriv :: Derivation (Extended Constant) -> Input Form+    deriv p@(Trans q r) = derivFrom (deriv r:sources q) p+    deriv p = derivFrom (sources p) p++    derivFrom :: [Input Form] -> Derivation (Extended Constant) -> Input Form+    derivFrom sources p =+      Input {+        tag = "step",+        kind = Jukebox.Ax Jukebox.Axiom,+        what = jukeboxEquation (equation (certify p)),+        source =+          Inference "rw" "thm" sources }++    jukeboxEquation :: Equation (Extended Constant) -> Form+    jukeboxEquation (t :=: u) =+      toForm $ clause [Pos (jukeboxTerm ctx t Jukebox.:=: jukeboxTerm ctx u)]++    sources :: Derivation (Extended Constant) -> [Input Form]+    sources p =+      [ fromJust (Map.lookup lemma_id lemma_proofs)+      | Lemma{..} <- usortBy (comparing lemma_id) (usedLemmas p) ] +++      [ fromJust (Map.lookup axiom_number axiom_proofs)+      | Axiom{..} <- usort (usedAxioms p) ]++    -- An ugly hack: since Twee.Proof decodes $true = $false into a+    -- proof of the existentially quantified goal, we need to do the+    -- same decoding at the Jukebox level.+    existentialHack eqn input =+      case find input of+        [] -> error $ "bug in TSTP output: can't fix up decoded existential"+        (inp:_) -> inp+        where+          -- Check if this looks like the correct clause;+          -- if not, try its ancestors.+          find inp | ok inp = [inp]+          find Input{source = Inference _ _ inps} =+            concatMap find inps+          find _ = []++          ok inp =+            case toClause (what inp) of+              Nothing -> False+              Just (Clause (Bind _ [Neg (t' Jukebox.:=: u')])) ->+                let+                  eqn' = toEquation t' u'+                  ts = buildList [eqn_lhs eqn, eqn_rhs eqn]+                  us = buildList [eqn_lhs eqn', eqn_rhs eqn']+                in+                  isJust (matchList ts us) && isJust (matchList us ts)++main = do+  hSetBuffering stdout LineBuffering+  join . parseCommandLineWithExtraArgs+    ["--no-conjunctive-conjectures", "--no-split"]+    "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $+      globalFlags *> parseMainFlags *>+      -- hack: get --quiet and --no-proof options to appear before --tstp+      forAllFilesBox <*>+        (readProblemBox =>>=+         expert clausifyBox =>>=+         forAllConjecturesBox <*>+           (combine <$>+             expert hornToUnitBox <*>+             (toFormulasBox =>>=+              expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=+              expert clausifyBox =>>= expert oneConjectureBox) <*>+             (runTwee <$> globalFlags <*> tstpFlags <*> parseMainFlags <*> expert hornFlags <*> parseConfig <*> parsePrecedence)))+  where+    combine horn encode prove later prob = do+      res <- horn prob+      case res of+        Left ans -> return ans+        Right prob ->+          encode prob >>= prove later
− README 
@@ -1,10 +0,0 @@-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!
− executable/Main.hs 
@@ -1,594 +0,0 @@-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-}-import Control.Monad-import Data.Char-import Data.Either-import Twee hiding (message)-import Twee.Base hiding (char, lookup, vars)-import Twee.Rule(lhs, rhs, unorient)-import Twee.Equation-import qualified Twee.Proof as Proof-import Twee.Proof hiding (Config, defaultConfig)-import qualified Twee.Join as Join-import Twee.Utils-import qualified Twee.CP as CP-import Data.Ord-import qualified Data.Map.Strict as Map-import qualified Twee.KBO as KBO-import Data.List.Split-import Data.List-import Data.Maybe-import Jukebox.Options-import Jukebox.Toolbox-import Jukebox.Name hiding (lhs, rhs)-import qualified Jukebox.Form as Jukebox-import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Lemma)-import Jukebox.Tools.EncodeTypes-import Jukebox.TPTP.Print-import Jukebox.Tools.Clausify(ClausifyFlags(..), clausify)-import qualified Data.Set as Set-import qualified Data.IntMap.Strict as IntMap-import System.IO-import System.Exit--data MainFlags =-  MainFlags {-    flags_proof :: Bool,-    flags_trace :: Maybe (String, String) }--parseMainFlags :: OptionParser MainFlags-parseMainFlags =-  MainFlags <$> proof <*> trace-  where-    proof =-      inGroup "Output options" $-      bool "proof" ["Produce proofs (on by default)."]-      True-    trace =-      expert $-      inGroup "Output options" $-      flag "trace"-        ["Write a Prolog-format execution trace to this file (off by default)."]-        Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)-    argModule = arg "<module>" "expected a Prolog module name" Just--parseConfig :: OptionParser Config-parseConfig =-  Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*>-    (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*>-    (Join.Config <$> ground_join <*> connectedness <*> set_join) <*>-    (Proof.Config <$> all_lemmas <*> flat_proof <*> show_instances)-  where-    maxSize =-      inGroup "Resource limits" $-      flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] maxBound argNum-    maxCPs =-      inGroup "Resource limits" $-      flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum-    maxCPDepth =-      inGroup "Resource limits" $-      flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum-    simplify =-      expert $-      inGroup "Completion heuristics" $-      bool "simplify"-        ["Simplify rewrite rules with respect to one another (on by default)."]-        True-    normPercent =-      expert $-      inGroup "Completion heuristics" $-      defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" (cfg_renormalise_percent) argNum-    lweight =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "lhs-weight" "Weight given to LHS of critical pair" (CP.cfg_lhsweight . cfg_critical_pairs) argNum-    rweight =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "rhs-weight" "Weight given to RHS of critical pair" (CP.cfg_rhsweight . cfg_critical_pairs) argNum-    funweight =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "fun-weight" "Weight given to function symbols" (CP.cfg_funweight . cfg_critical_pairs) argNum-    varweight =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "var-weight" "Weight given to variable symbols" (CP.cfg_varweight . cfg_critical_pairs) argNum-    depthweight =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "depth-weight" "Weight given to critical pair depth" (CP.cfg_depthweight . cfg_critical_pairs) argNum-    dupcost =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "dup-cost" "Cost of duplicate subterms" (CP.cfg_dupcost . cfg_critical_pairs) argNum-    dupfactor =-      expert $-      inGroup "Critical pair weighting heuristics" $-      defaultFlag "dup-factor" "Size factor of duplicate subterms" (CP.cfg_dupfactor . cfg_critical_pairs) argNum-    ground_join =-      expert $-      inGroup "Critical pair joining heuristics" $-      bool "ground-joining"-        ["Test terms for ground joinability (on by default)."]-        True-    connectedness =-      expert $-      inGroup "Critical pair joining heuristics" $-      bool "connectedness"-        ["Test terms for subconnectedness (off by default)."]-        False-    set_join =-      expert $-      inGroup "Critical pair joining heuristics" $-      bool "set-join"-        ["Compute all normal forms when joining critical pairs (off by default)."]-        False-    all_lemmas =-      expert $-      inGroup "Proof presentation" $-      bool "all-lemmas"-        ["Produce a proof with one lemma for each critical pair (off by default)."]-        False-    flat_proof =-      expert $-      inGroup "Proof presentation" $-      bool "no-lemmas"-        ["Produce a proof with no lemmas (off by default).",-         "May lead to exponentially large proofs."]-        False-    show_instances =-      expert $-      inGroup "Proof presentation" $-      bool "show-instances"-        ["Show which instances of each axiom and lemma were used (off by default)."]-        False-    defaultFlag name desc field parser =-      flag name [desc ++ " (" ++ show def ++ " by default)."] def parser-      where-        def = field defaultConfig--parsePrecedence :: OptionParser [String]-parsePrecedence =-  expert $-  inGroup "Term order options" $-  fmap (splitOn ",")-  (flag "precedence" ["List of functions in descending order of precedence."] [] (arg "<function>" "expected a function name" Just))--data Constant =-  Constant {-    con_prec  :: {-# UNPACK #-} !Precedence,-    con_id    :: {-# UNPACK #-} !Jukebox.Function,-    con_arity :: {-# UNPACK #-} !Int }-  deriving (Eq, Ord)--data Precedence = Precedence !Bool !(Maybe Int) !Int-  deriving (Eq, Ord)--instance Sized Constant where-  size Constant{..} = 1-    --if con_arity <= 1 then 1 else 0-instance Arity Constant where-  arity Constant{..} = con_arity--instance Pretty Constant where-  pPrint Constant{..} = text (base con_id)--instance PrettyTerm Constant where-  termStyle Constant{..}-    | any isAlphaNum (base con_id) = uncurried-    | otherwise =-      case con_arity of-        1 -> prefix-        2 -> infixStyle 5-        _ -> uncurried--instance Ordered (Extended Constant) where-  lessEq t u = {-# SCC lessEq #-} KBO.lessEq t u-  lessIn model t u = {-# SCC lessIn #-} KBO.lessIn model t u--data TweeContext =-  TweeContext {-    ctx_var     :: Jukebox.Variable,-    ctx_minimal :: Jukebox.Function,-    ctx_true    :: Jukebox.Function,-    ctx_false   :: Jukebox.Function,-    ctx_equals  :: Jukebox.Function,-    ctx_type    :: Type }---- Convert back and forth between Twee and Jukebox.-tweeConstant :: TweeContext -> Precedence -> Jukebox.Function -> Extended Constant-tweeConstant TweeContext{..} prec fun-  | fun == ctx_minimal = Minimal-  | fun == ctx_true = TrueCon-  | fun == ctx_false = FalseCon-  | fun == ctx_equals = EqualsCon-  | otherwise = Function (Constant prec fun (Jukebox.arity fun))--jukeboxFunction :: TweeContext -> Extended Constant -> Jukebox.Function-jukeboxFunction _ (Function Constant{..}) = con_id-jukeboxFunction TweeContext{..} EqualsCon = ctx_equals-jukeboxFunction TweeContext{..} TrueCon = ctx_true-jukeboxFunction TweeContext{..} FalseCon = ctx_false-jukeboxFunction TweeContext{..} Minimal = ctx_minimal-jukeboxFunction TweeContext{..} (Skolem _) =-  error "Skolem variable leaked into rule"--tweeTerm :: TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term (Extended Constant)-tweeTerm ctx prec t = build (tm t)-  where-    tm (Jukebox.Var (Unique x _ _ ::: _)) =-      var (V (fromIntegral x))-    tm (f :@: ts) =-      app (fun (tweeConstant ctx (prec f) f)) (map tm ts)--jukeboxTerm :: TweeContext -> Term (Extended Constant) -> Jukebox.Term-jukeboxTerm TweeContext{..} (Var (V x)) =-  Jukebox.Var (Unique (fromIntegral x) "X" defaultRenamer ::: ctx_type)-jukeboxTerm ctx@TweeContext{..} (App f t) =-  jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts-  where-    ts = unpack t--makeContext :: Problem Clause -> TweeContext-makeContext prob = run prob $ \prob -> do-  let-    ty =-      case types' prob of-        []   -> indType-        [ty] -> ty--  var     <- newSymbol "X" ty-  minimal <- newFunction "$constant" [] ty-  equals  <- newFunction "$equals" [ty, ty] ty-  false   <- newFunction "$false_term" [] ty-  true    <- newFunction "$true_term" [] ty--  return TweeContext {-    ctx_var = var,-    ctx_minimal = minimal,-    ctx_equals = equals,-    ctx_false = false,-    ctx_true = true,-    ctx_type = ty }---- Encode existentials so that all goals are ground.-addNarrowing :: TweeContext -> Problem Clause -> Problem Clause-addNarrowing TweeContext{..} prob =-  unchanged ++ equalityClauses-  where-    (unchanged, nonGroundGoals) = partitionEithers (map f prob)-      where-        f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])}-          | not (ground x) || not (ground y) =-            Right (inp, (x, y))-        f inp = Left inp--    equalityClauses-      | null nonGroundGoals = []-      | otherwise =-        -- Turn a != b & c != d & ...-        -- into eq(a,b)=false & eq(c,d)=false & eq(X,X)=true & true!=false (esa)-        -- and then extract the individual components (thm)-        let-          equalityLiterals =-            -- true != false-            ("true_equals_false", Neg ((ctx_true :@:) [] Jukebox.:=: (ctx_false :@: []))):-            -- eq(X,X)=true-            ("reflexivity", Pos (ctx_equals :@: [Jukebox.Var ctx_var, Jukebox.Var ctx_var] Jukebox.:=: (ctx_true :@: []))):-            -- [eq(a,b)=false, eq(c,d)=false, ...]-            [ (tag, Pos (ctx_equals :@: [x, y] Jukebox.:=: (ctx_false :@: [])))-            | (Input{tag = tag}, (x, y)) <- nonGroundGoals ]--          -- Equisatisfiable to the input clauses-          justification =-            Input {-              tag  = "new_negated_conjecture",-              kind = Jukebox.Ax NegatedConjecture,-              what =-                let form = And (map (Literal . snd) equalityLiterals) in-                ForAll (Bind (Set.fromList (vars form)) form),-              source =-                Inference "encode_existential" "esa"-                  (map (fmap toForm . fst) nonGroundGoals) }--          input tag form =-            Input {-              tag = tag,-              kind = Conj Conjecture,-              what = clause [form],-              source =-                Inference "split_conjunct" "thm" [justification] }--        in [input tag form | (tag, form) <- equalityLiterals]--data PreEquation =-  PreEquation {-    pre_name :: String,-    pre_form :: Input Form,-    pre_eqn  :: (Jukebox.Term, Jukebox.Term) }---- Split the problem into axioms and ground goals.-identifyProblem ::-  TweeContext -> Problem Clause -> Either (Input Clause) ([PreEquation], [PreEquation])-identifyProblem TweeContext{..} prob =-  fmap partitionEithers (mapM identify prob)--  where-    pre inp x =-      PreEquation {-        pre_name = tag inp,-        pre_form = fmap toForm inp,-        pre_eqn = x }--    identify inp@Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} =-      return $ Left (pre inp (t, u))-    identify inp@Input{what = Clause (Bind _ [Neg (t Jukebox.:=: u)])}-      | ground t && ground u =-        return $ Right (pre inp (t, u))-    identify inp@Input{what = Clause (Bind _ [])} =-      -- The empty clause can appear after clausification if-      -- the conjecture was trivial-      return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: []))-    identify inp = Left inp--runTwee :: GlobalFlags -> TSTPFlags -> MainFlags -> Config -> [String] -> (IO () -> IO ()) -> Problem Clause -> IO Answer-runTwee globals (TSTPFlags tstp) main config precedence later obligs = {-# SCC runTwee #-} do-  let-    -- Encode whatever needs encoding in the problem-    ctx = makeContext obligs-    prob = addNarrowing ctx obligs--  (axioms0, goals0) <--    case identifyProblem ctx prob of-      Left inp -> do-        mapM_ (hPutStrLn stderr) [-          "The problem contains the following clause, which is not a unit equality:",-          indent (show (pPrintClauses [inp])),-          "Twee only handles unit equality problems."]-        exitWith (ExitFailure 1)-      Right x -> return x--  let-    -- Work out a precedence for function symbols-    prec c =-      Precedence-        (isNothing (elemIndex (base c) precedence))-        (fmap negate (elemIndex (base c) precedence))-        (negate (funOcc c prob))--    -- Translate everything to Twee.-    toEquation (t, u) =-      canonicalise (tweeTerm ctx prec t :=: tweeTerm ctx prec u)--    goals =-      [ goal n pre_name (toEquation pre_eqn)-      | (n, PreEquation{..}) <- zip [1..] goals0 ]-    axioms =-      [ Axiom n pre_name (toEquation pre_eqn)-      | (n, PreEquation{..}) <- zip [1..] axioms0 ]--    withGoals = foldl' (addGoal config) initialState goals-    withAxioms = foldl' (addAxiom config) withGoals axioms--  -- Set up tracing.-  sayTrace <--    case flags_trace main of-      Nothing -> return $ \_ -> return ()-      Just (file, mod) -> do-        h <- openFile file WriteMode-        hSetBuffering h LineBuffering-        let put msg = hPutStrLn h msg-        put $ ":- module(" ++ mod ++ ", [step/1, lemma/1])."-        put ":- discontiguous(step/1)."-        put ":- discontiguous(lemma/1)."-        put ":- style_check(-singleton)."-        return $ \msg -> hPutStrLn h msg-  -  let-    say msg = unless (quiet globals) (putStrLn msg)-    line = say ""-    output = Output {-      output_report = \_ -> return (),-      output_message = \msg -> do-        say (prettyShow msg)-        sayTrace (show (traceMsg msg)) }--    traceMsg (NewActive active) =-      step "add" [traceActive active]-    traceMsg (NewEquation eqn) =-      step "hard" [traceEqn eqn]-    traceMsg (DeleteActive active) =-      step "delete" [traceActive active]-    traceMsg SimplifyQueue =-      step "simplify_queue" []-    traceMsg Interreduce =-      step "interreduce" []--    traceActive Active{..} =-      traceApp "rule" [pPrint active_id, traceEqn (unorient active_rule)]-    traceEqn (t :=: u) =-      pPrintPrec prettyNormal 6 t <+> text "=" <+> pPrintPrec prettyNormal 6 u-    traceApp f xs =-      pPrintTerm uncurried prettyNormal 0 (text f) xs--    step :: String -> [Doc] -> Doc-    step f xs = traceApp "step" [traceApp f xs] <> text "."--  say "Here is the input problem:"-  forM_ axioms $ \Axiom{..} ->-    say $ show $ nest 2 $-      describeEquation "Axiom"-        (show axiom_number) (Just axiom_name) axiom_eqn-  forM_ goals $ \Goal{..} ->-    say $ show $ nest 2 $-      describeEquation "Goal"-        (show goal_number) (Just goal_name) goal_eqn-  line--  state <- complete output config withAxioms-  line--  when (solved state && flags_proof main) $ later $ do-    let-      pres = present (cfg_proof_presentation config) (solutions state)--    sayTrace ""-    forM_ (pres_lemmas pres) $ \Lemma{..} ->-      sayTrace $ show $-        traceApp "lemma" [traceEqn (equation lemma_proof)] <> text "."--    when tstp $ do-      putStrLn "% SZS output start CNFRefutation"-      print $ pPrintProof $-        presentToJukebox ctx (curry toEquation)-          (zip (map axiom_number axioms) (map pre_form axioms0))-          (zip (map goal_number goals) (map pre_form goals0))-          pres-      putStrLn "% SZS output end CNFRefutation"-      putStrLn ""--    putStrLn "The conjecture is true! Here is a proof."-    putStrLn ""-    print $ pPrintPresentation (cfg_proof_presentation config) pres-    putStrLn ""--  when (not (quiet globals) && not (solved state)) $ later $ do-    let-      state' = interreduce config state-      score rule =-        (size (lhs rule), lhs rule,-         size (rhs rule), rhs rule)-      actives =-        sortBy (comparing (score . active_rule)) $-        IntMap.elems (st_active_ids state')--    when (tstp && configIsComplete config) $ do-      putStrLn "% SZS output start Saturation"-      print $ pPrintProof $-        map pre_form axioms0 ++-        map pre_form goals0 ++-        [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $-            toForm $ clause-              [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))]-        | rule <- rules state ]-      putStrLn "% SZS output end Saturation"-      putStrLn ""--    if configIsComplete config then do-      putStrLn "Ran out of critical pairs. This means the conjecture is not true."-    else do-      putStrLn "Gave up on reaching the given resource limit."-    putStrLn "Here is the final rewrite system:"-    forM_ actives $ \active ->-      putStrLn ("  " ++ prettyShow (canonicalise (active_rule active)))-    putStrLn ""--  return $-    if solved state then Unsat Unsatisfiable-    else if configIsComplete config then Sat Satisfiable-    else NoAnswer GaveUp---- Transform a proof presentation into a Jukebox proof.-presentToJukebox ::-  TweeContext ->-  (Jukebox.Term -> Jukebox.Term -> Equation (Extended Constant)) ->-  -- Axioms, indexed by axiom number.-  [(Int, Input Form)] ->-  -- N.B. the formula here proves the negated goal.-  [(Int, Input Form)] ->-  Presentation (Extended Constant) ->-  Problem Form-presentToJukebox ctx toEquation axioms goals Presentation{..} =-  [ Input {-      tag = pg_name,-      kind = Jukebox.Ax Jukebox.Axiom,-      what = false,-      source =-        Inference "resolution" "thm"-          [-- A proof of t != u-           existentialHack pg_goal_hint (fromJust (lookup pg_number goals)),-           -- A proof of t = u-           fromJust (Map.lookup pg_number goal_proofs)] }-  | ProvedGoal{..} <- pres_goals ]--  where-    axiom_proofs =-      Map.fromList-        [ (axiom_number, fromJust (lookup axiom_number axioms))-        | Axiom{..} <- pres_axioms ]--    lemma_proofs =-      Map.fromList [(lemma_id, tstp lemma_proof) | Lemma{..} <- pres_lemmas]--    goal_proofs =-      Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals]--    tstp :: Proof (Extended Constant) -> Input Form-    tstp = deriv . derivation--    deriv :: Derivation (Extended Constant) -> Input Form-    deriv p@(Trans q r) = derivFrom (deriv r:sources q) p-    deriv p = derivFrom (sources p) p--    derivFrom :: [Input Form] -> Derivation (Extended Constant) -> Input Form-    derivFrom sources p =-      Input {-        tag = "step",-        kind = Jukebox.Ax Jukebox.Axiom,-        what = jukeboxEquation (equation (certify p)),-        source =-          Inference "rw" "thm" sources }--    jukeboxEquation :: Equation (Extended Constant) -> Form-    jukeboxEquation (t :=: u) =-      toForm $ clause [Pos (jukeboxTerm ctx t Jukebox.:=: jukeboxTerm ctx u)]--    sources :: Derivation (Extended Constant) -> [Input Form]-    sources p =-      [ fromJust (Map.lookup lemma_id lemma_proofs)-      | Lemma{..} <- usortBy (comparing lemma_id) (usedLemmas p) ] ++-      [ fromJust (Map.lookup axiom_number axiom_proofs)-      | Axiom{..} <- usort (usedAxioms p) ]--    -- An ugly hack: since Twee.Proof decodes $true = $false into a-    -- proof of the existentially quantified goal, we need to do the-    -- same decoding at the Jukebox level.-    existentialHack eqn input =-      case find input of-        [] -> error $ "bug in TSTP output: can't fix up decoded existential"-        (inp:_) -> inp-        where-          -- Check if this looks like the correct clause;-          -- if not, try its ancestors.-          find inp | ok inp = [inp]-          find Input{source = Inference _ _ inps} =-            concatMap find inps-          find _ = []--          ok inp =-            case toClause (what inp) of-              Nothing -> False-              Just (Clause (Bind _ [Neg (t' Jukebox.:=: u')])) ->-                let-                  eqn' = toEquation t' u'-                  ts = buildList [eqn_lhs eqn, eqn_rhs eqn]-                  us = buildList [eqn_lhs eqn', eqn_rhs eqn']-                in-                  isJust (matchList ts us) && isJust (matchList us ts)--main = do-  let-    -- Always use splitting-    clausifyBox =-      pure (\prob -> return $! clausify (ClausifyFlags True) prob)-  hSetBuffering stdout LineBuffering-  join . parseCommandLine "Twee, an equational theorem prover" .-    version ("twee version " ++ VERSION_twee) $-    globalFlags *> parseMainFlags *>-      -- hack: get --quiet and --no-proof options to appear before --tstp-    forAllFilesBox <*>-      (readProblemBox =>>=-       expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=-       expert clausifyBox =>>=-       forAllConjecturesBox <*>-         (runTwee <$> globalFlags <*> tstpFlags <*> parseMainFlags <*> parseConfig <*> parsePrecedence))
+ misc/static-libstdc++ view
@@ -0,0 +1,24 @@+#!/bin/zsh+typeset -a args++process() {+    for arg in $*; do+        case $arg in+            \"*\")+                process $(echo $arg | cut -c2- | rev | cut -c2- | rev)+                ;;+            @*)+                process $(cat $(echo $arg | cut -c2-))+                ;;+            -lstdc++ | -fuse-ld=gold)+                ;;+            *)+                args+=$arg+                ;;+        esac+    done+}++process $*++exec g++ -static-libgcc -static-libstdc++ $args
− src/Data/Primitive/ByteArray/Checked.hs 
@@ -1,71 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}-module Data.Primitive.ByteArray.Checked(-  module Data.Primitive.ByteArray,-  module Data.Primitive.ByteArray.Checked) where--import Control.Monad.Primitive-import qualified Data.Primitive.ByteArray as P-import Data.Primitive(Prim)-import Data.Primitive.ByteArray(-  ByteArray(..), MutableByteArray(..),-  newByteArray, newPinnedByteArray, newAlignedPinnedByteArray,-  byteArrayContents, mutableByteArrayContents,-  sameMutableByteArray,-  unsafeFreezeByteArray, unsafeThawByteArray,-  sizeofByteArray, sizeofMutableByteArray)-import Data.Primitive.Checked-import Data.Word--instance Sized ByteArray where-  size = sizeofByteArray-instance Sized (MutableByteArray m) where-  size = sizeofMutableByteArray--{-# INLINE readByteArray #-}-readByteArray :: forall m a. (PrimMonad m, Prim a) => MutableByteArray (PrimState m) -> Int -> m a-readByteArray arr n =-  checkPrim (undefined :: a) arr n $-  P.readByteArray arr n--{-# INLINE writeByteArray #-}-writeByteArray :: (PrimMonad m, Prim a) => MutableByteArray (PrimState m) -> Int -> a -> m ()-writeByteArray arr n x =-  checkPrim x arr n $-  P.writeByteArray arr n x--{-# INLINE indexByteArray #-}-indexByteArray :: forall a. Prim a => ByteArray -> Int -> a-indexByteArray arr n =-  checkPrim (undefined :: a) arr n $-  P.indexByteArray arr n--{-# INLINE copyByteArray #-}-copyByteArray :: PrimMonad m => MutableByteArray (PrimState m) -> Int -> ByteArray -> Int -> Int -> m ()-copyByteArray arr1 n1 arr2 n2 len =-  range arr1 n1 len $-  range arr2 n2 len $-  P.copyByteArray arr1 n1 arr2 n2 len--{-# INLINE moveByteArray #-}-moveByteArray :: PrimMonad m => MutableByteArray (PrimState m) -> Int -> MutableByteArray (PrimState m) -> Int -> Int -> m ()-moveByteArray arr1 n1 arr2 n2 len =-  range arr1 n1 len $-  range arr2 n2 len $-  P.moveByteArray arr1 n1 arr2 n2 len--{-# INLINE copyMutableByteArray #-}-copyMutableByteArray :: PrimMonad m => MutableByteArray (PrimState m) -> Int -> MutableByteArray (PrimState m) -> Int -> Int -> m ()-copyMutableByteArray arr1 n1 arr2 n2 len =-  range arr1 n1 len $-  range arr2 n2 len $-  P.copyMutableByteArray arr1 n1 arr2 n2 len--{-# INLINE setByteArray #-}-setByteArray :: (Prim a, PrimMonad m) => MutableByteArray (PrimState m) -> Int -> Int -> a -> m ()-setByteArray arr n len x =-  rangePrim x arr n len $-  P.setByteArray arr n len x--{-# INLINE fillByteArray #-}-fillByteArray :: PrimMonad m => MutableByteArray (PrimState m) -> Int -> Int -> Word8 -> m ()-fillByteArray = setByteArray
− src/Data/Primitive/Checked.hs 
@@ -1,32 +0,0 @@-module Data.Primitive.Checked where--import Data.Primitive(Prim, sizeOf)--class Sized a where-  size :: a -> Int--{-# INLINE check #-}-check :: Sized a => a -> Int -> b -> b-check arr n x-  | n >= 0 && n < size arr = x-  | otherwise = error "out-of-bounds array access"--{-# INLINE range #-}-range :: Sized a => a -> Int -> Int -> b -> b-range arr n len x-  | len < 0 = error "array slice has negative length"-  | len == 0 = x-  | otherwise =-    check arr n $-    check arr (n+len-1) $ x--{-# INLINE checkPrim #-}-checkPrim :: (Sized a, Prim b) => b -> a -> Int -> c -> c-checkPrim x arr n res =-  range arr (n*sizeOf x) (sizeOf x) res-  -{-# INLINE rangePrim #-}-rangePrim :: (Sized a, Prim b) => b -> a -> Int -> Int -> c -> c-rangePrim x arr n len res =-  range arr (n*sizeOf x) (len*sizeOf x) res-
− src/Data/Primitive/SmallArray/Checked.hs 
@@ -1,77 +0,0 @@-module Data.Primitive.SmallArray.Checked(-  module Data.Primitive.SmallArray,-  module Data.Primitive.SmallArray.Checked) where--import Control.Monad.Primitive-import qualified Data.Primitive.SmallArray as P-import Data.Primitive.SmallArray(-  SmallArray(..), SmallMutableArray(..), newSmallArray, unsafeFreezeSmallArray,-  unsafeThawSmallArray, sizeofSmallArray, sizeofSmallMutableArray)-import Data.Primitive.Checked--instance Sized (SmallArray a) where-  size = sizeofSmallArray-instance Sized (SmallMutableArray m a) where-  size = sizeofSmallMutableArray--{-# INLINE readSmallArray #-}-readSmallArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> m a-readSmallArray arr n =-  check arr n $-  P.readSmallArray arr n--{-# INLINE writeSmallArray #-}-writeSmallArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> a -> m ()-writeSmallArray arr n x =-  check arr n $-  P.writeSmallArray arr n x--{-# INLINE indexSmallArrayM #-}-indexSmallArrayM :: Monad m => SmallArray a -> Int -> m a-indexSmallArrayM arr n =-  check arr n $-  P.indexSmallArrayM arr n--{-# INLINE indexSmallArray #-}-indexSmallArray :: SmallArray a -> Int -> a-indexSmallArray arr n =-  check arr n $-  P.indexSmallArray arr n--{-# INLINE cloneSmallArray #-}-cloneSmallArray :: SmallArray a -> Int -> Int -> SmallArray a-cloneSmallArray arr n len =-  range arr n len $-  P.cloneSmallArray arr n len--{-# INLINE cloneSmallMutableArray #-}-cloneSmallMutableArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> Int -> m (SmallMutableArray (PrimState m) a)-cloneSmallMutableArray arr n len =-  range arr n len $-  P.cloneSmallMutableArray arr n len--{-# INLINE freezeSmallArray #-}-freezeSmallArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> Int -> m (SmallArray a)-freezeSmallArray arr n len =-  range arr n len $-  P.freezeSmallArray arr n len--{-# INLINE thawSmallArray #-}-thawSmallArray :: PrimMonad m => SmallArray a -> Int -> Int -> m (SmallMutableArray (PrimState m) a)-thawSmallArray arr n len =-  range arr n len $-  P.thawSmallArray arr n len--{-# INLINE copySmallArray #-}-copySmallArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> SmallArray a -> Int -> Int -> m ()-copySmallArray arr1 n1 arr2 n2 len =-  range arr1 n1 len $-  range arr2 n2 len $-  P.copySmallArray arr1 n1 arr2 n2 len--{-# INLINE copySmallMutableArray #-}-copySmallMutableArray :: PrimMonad m => SmallMutableArray (PrimState m) a -> Int -> SmallMutableArray (PrimState m) a -> Int -> Int -> m ()-copySmallMutableArray arr1 n1 arr2 n2 len =-  range arr1 n1 len $-  range arr2 n2 len $-  P.copySmallMutableArray arr1 n1 arr2 n2 len
− src/Twee.hs 
@@ -1,666 +0,0 @@-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies #-}-module Twee where--import Twee.Base-import Twee.Rule-import Twee.Equation-import qualified Twee.Proof as Proof-import Twee.Proof(Proof, Axiom(..), Lemma(..), ProvedGoal(..), provedGoal, certify, derivation, symm)-import Twee.CP hiding (Config)-import qualified Twee.CP as CP-import Twee.Join hiding (Config, defaultConfig)-import qualified Twee.Join as Join-import qualified Twee.Rule.Index as RuleIndex-import Twee.Rule.Index(RuleIndex(..))-import qualified Twee.Index as Index-import Twee.Index(Index)-import Twee.Constraints-import Twee.Utils-import Twee.Task-import qualified Twee.Heap as Heap-import Twee.Heap(Heap)-import qualified Data.IntMap.Strict as IntMap-import Data.IntMap(IntMap)-import Data.Maybe-import Data.List-import Data.Function-import qualified Data.Set as Set-import Data.Set(Set)-import Text.Printf-import Data.Int-import Data.Ord-import Control.Monad-import Control.Monad.IO.Class-import Control.Monad.Trans.Class-import qualified Control.Monad.Trans.State.Strict as StateM-import Data.Word-import Data.Bits--------------------------------------------------------------------------- Configuration and prover state.-------------------------------------------------------------------------data Config =-  Config {-    cfg_max_term_size          :: Int,-    cfg_max_critical_pairs     :: Int64,-    cfg_max_cp_depth           :: Int,-    cfg_simplify               :: Bool,-    cfg_renormalise_percent    :: Int,-    cfg_critical_pairs         :: CP.Config,-    cfg_join                   :: Join.Config,-    cfg_proof_presentation     :: Proof.Config }--data State f =-  State {-    st_rules          :: !(RuleIndex f (ActiveRule f)),-    st_active_ids     :: !(IntMap (Active f)),-    st_rule_ids       :: !(IntMap (ActiveRule f)),-    st_joinable       :: !(Index f (Equation f)),-    st_goals          :: ![Goal f],-    st_queue          :: !(Heap (PackedPassive f)),-    st_next_active    :: {-# UNPACK #-} !Id,-    st_next_rule      :: {-# UNPACK #-} !RuleId,-    st_considered     :: {-# UNPACK #-} !Int64,-    st_messages_rev   :: ![Message f] }--defaultConfig :: Config-defaultConfig =-  Config {-    cfg_max_term_size = maxBound,-    cfg_max_critical_pairs = maxBound,-    cfg_max_cp_depth = maxBound,-    cfg_simplify = True,-    cfg_renormalise_percent = 5,-    cfg_critical_pairs =-      CP.Config {-        cfg_lhsweight = 3,-        cfg_rhsweight = 1,-        cfg_funweight = 7,-        cfg_varweight = 6,-        cfg_depthweight = 16,-        cfg_dupcost = 7,-        cfg_dupfactor = 0 },-    cfg_join = Join.defaultConfig,-    cfg_proof_presentation = Proof.defaultConfig }--configIsComplete :: Config -> Bool-configIsComplete Config{..} =-  cfg_max_term_size == maxBound &&-  cfg_max_critical_pairs == maxBound &&-  cfg_max_cp_depth == maxBound--initialState :: State f-initialState =-  State {-    st_rules = RuleIndex.nil,-    st_active_ids = IntMap.empty,-    st_rule_ids = IntMap.empty,-    st_joinable = Index.Nil,-    st_goals = [],-    st_queue = Heap.empty,-    st_next_active = 1,-    st_next_rule = 0,-    st_considered = 0,-    st_messages_rev = [] }--------------------------------------------------------------------------- Messages.-------------------------------------------------------------------------data Message f =-    NewActive !(Active f)-  | NewEquation !(Equation f)-  | DeleteActive !(Active f)-  | SimplifyQueue-  | Interreduce--instance Function f => Pretty (Message f) where-  pPrint (NewActive rule) = pPrint rule-  pPrint (NewEquation eqn) =-    text "  (hard)" <+> pPrint eqn-  pPrint (DeleteActive rule) =-    text "  (delete rule " <> pPrint (active_id rule) <> text ")"-  pPrint SimplifyQueue =-    text "  (simplifying queued critical pairs...)"-  pPrint Interreduce =-    text "  (simplifying rules with respect to one another...)"--message :: PrettyTerm f => Message f -> State f -> State f-message !msg state@State{..} =-  state { st_messages_rev = msg:st_messages_rev }--clearMessages :: State f -> State f-clearMessages state@State{..} =-  state { st_messages_rev = [] }--messages :: State f -> [Message f]-messages state = reverse (st_messages_rev state)--------------------------------------------------------------------------- The CP queue.-------------------------------------------------------------------------data Passive f =-  Passive {-    passive_score :: {-# UNPACK #-} !Int32,-    passive_rule1 :: {-# UNPACK #-} !RuleId,-    passive_rule2 :: {-# UNPACK #-} !RuleId,-    passive_pos   :: {-# UNPACK #-} !Int32 }-  deriving (Eq, Show)--instance Ord (Passive f) where-  compare = comparing f-    where-      f Passive{..} =-        (passive_score,-         intMax (fromIntegral passive_rule1) (fromIntegral passive_rule2),-         passive_rule1,-         passive_rule2,-         passive_pos)--data PackedPassive f =-  PackedPassive {-# UNPACK #-} !Word64 {-# UNPACK #-} !Word64-  deriving (Eq, Ord, Show)--packPassive :: Passive f -> PackedPassive f-packPassive (Passive score rule1 rule2 pos) =-  -- Do this so that Ord instance matches with Passive-  if rule1 > rule2 then-    PackedPassive-      (pack score (fromIntegral rule1))-      (pack (fromIntegral rule2) (pos `shiftL` 1))-  else-    PackedPassive-      (pack score (fromIntegral rule2))-      (pack (fromIntegral rule1) (pos `shiftL` 1 + 1))-  where-    pack :: Int32 -> Int32 -> Word64-    pack x y =-      fromIntegral x `shiftL` 32 + fromIntegral y--unpackPassive :: PackedPassive f -> Passive f-unpackPassive (PackedPassive x y) =-  if testBit pos1 0 then-    Passive score (fromIntegral rule2) (fromIntegral rule1) pos-  else-    Passive score (fromIntegral rule1) (fromIntegral rule2) pos-  where-    (score, rule1) = unpack x-    (rule2, pos1) = unpack y-    pos = pos1 `shiftR` 1--    unpack :: Word64 -> (Int32, Int32)-    unpack x = (fromIntegral (x `shiftR` 32), fromIntegral x)---- Compute all critical pairs from a rule and condense into a Passive.-{-# INLINEABLE makePassive #-}-makePassive :: Function f => Config -> State f -> ActiveRule f -> [Passive f]-makePassive Config{..} State{..} rule =-  {-# SCC makePassive #-}-  [ Passive (fromIntegral (score cfg_critical_pairs o)) (rule_rid rule1) (rule_rid rule2) (fromIntegral (overlap_pos o))-  | (rule1, rule2, o) <- overlaps (Depth cfg_max_cp_depth) (index_oriented st_rules) rules rule ]-  where-    rules = IntMap.elems st_rule_ids---- Turn a Passive back into an overlap.--- Doesn't try to simplify it.-{-# INLINEABLE findPassive #-}-findPassive :: forall f. Function f => Config -> State f -> Passive f -> Maybe (ActiveRule f, ActiveRule f, Overlap f)-findPassive Config{..} State{..} Passive{..} = {-# SCC findPassive #-} do-  rule1 <- IntMap.lookup (fromIntegral passive_rule1) st_rule_ids-  rule2 <- IntMap.lookup (fromIntegral passive_rule2) st_rule_ids-  let !depth = 1 + max (the rule1) (the rule2)-  overlap <--    overlapAt (fromIntegral passive_pos) depth-      (renameAvoiding (the rule2 :: Rule f) (the rule1)) (the rule2)-  return (rule1, rule2, overlap)---- Renormalise a queued Passive.-{-# INLINEABLE simplifyPassive #-}-simplifyPassive :: Function f => Config -> State f -> Passive f -> Maybe (Passive f)-simplifyPassive config@Config{..} state@State{..} passive = {-# SCC simplifyPassive #-} do-  (_, _, overlap) <- findPassive config state passive-  overlap <- simplifyOverlap (index_oriented st_rules) overlap-  return passive {-    passive_score = fromIntegral $-      fromIntegral (passive_score passive) `intMin`-      score cfg_critical_pairs overlap }---- Renormalise the entire queue.-{-# INLINEABLE simplifyQueue #-}-simplifyQueue :: Function f => Config -> State f -> State f-simplifyQueue config state =-  {-# SCC simplifyQueue #-}-  state { st_queue = simp (st_queue state) }-  where-    simp =-      Heap.mapMaybe (fmap packPassive . simplifyPassive config state . unpackPassive)---- Enqueue a critical pair.-{-# INLINEABLE enqueue #-}-enqueue :: Function f => State f -> Passive f -> State f-enqueue state passive =-  {-# SCC enqueue #-}-  state { st_queue = Heap.insert (packPassive passive) (st_queue state) }---- Dequeue a critical pair.--- Also takes care of:---   * removing any orphans from the head of the queue---   * splitting ManyCPs up as necessary---   * ignoring CPs that are too big-{-# INLINEABLE dequeue #-}-dequeue :: Function f => Config -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f)-dequeue config@Config{..} state@State{..} =-  {-# SCC dequeue #-}-  case deq 0 st_queue of-    -- Explicitly make the queue empty, in case it e.g. contained a-    -- lot of orphans-    Nothing -> (Nothing, state { st_queue = Heap.empty })-    Just (overlap, n, queue) ->-      (Just overlap,-       state { st_queue = queue, st_considered = st_considered + n })-  where-    deq !n queue = do-      (packedPassive, queue) <- Heap.removeMin queue-      let passive = unpackPassive packedPassive-      case findPassive config state passive of-        Just (rule1, rule2, overlap)-          | passive_score passive >= 0,-            Just Overlap{overlap_eqn = t :=: u} <--              simplifyOverlap (index_oriented st_rules) overlap,-            size t <= cfg_max_term_size,-            size u <= cfg_max_term_size,-            Just cp <- makeCriticalPair rule1 rule2 overlap ->-              return ((cp, rule1, rule2), n+1, queue)-        _ -> deq (n+1) queue--------------------------------------------------------------------------- Active rewrite rules.-------------------------------------------------------------------------data Active f =-  Active {-    active_id    :: {-# UNPACK #-} !Id,-    active_depth :: {-# UNPACK #-} !Depth,-    active_rule  :: {-# UNPACK #-} !(Rule f),-    active_top   :: !(Maybe (Term f)),-    active_proof :: {-# UNPACK #-} !(Proof f),-    -- A model in which the rule is false (used when reorienting)-    active_model :: !(Model f),-    active_rules :: ![ActiveRule f] }--active_cp :: Active f -> CriticalPair f-active_cp Active{..} =-  CriticalPair {-    cp_eqn = unorient active_rule,-    cp_depth = active_depth,-    cp_top = active_top,-    cp_proof = derivation active_proof }---- An active oriented in a particular direction.-data ActiveRule f =-  ActiveRule {-    rule_active    :: {-# UNPACK #-} !Id,-    rule_rid       :: {-# UNPACK #-} !RuleId,-    rule_depth     :: {-# UNPACK #-} !Depth,-    rule_rule      :: {-# UNPACK #-} !(Rule f),-    rule_proof     :: {-# UNPACK #-} !(Proof f),-    rule_positions :: !(Positions f) }--instance PrettyTerm f => Symbolic (ActiveRule f) where-  type ConstantOf (ActiveRule f) = f-  termsDL ActiveRule{..} =-    termsDL rule_rule `mplus`-    termsDL (derivation rule_proof)-  subst_ sub r@ActiveRule{..} =-    r {-      rule_rule = rule',-      rule_proof = certify (subst_ sub (derivation rule_proof)),-      rule_positions = positions (lhs rule') }-    where-      rule' = subst_ sub rule_rule--instance Eq (Active f) where-  (==) = (==) `on` active_id--instance Eq (ActiveRule f) where-  (==) = (==) `on` rule_rid--instance Function f => Pretty (Active f) where-  pPrint Active{..} =-    pPrint active_id <> text "." <+> pPrint (canonicalise active_rule)--instance Has (ActiveRule f) Id where the = rule_active-instance Has (ActiveRule f) Depth where the = rule_depth-instance f ~ g => Has (ActiveRule f) (Rule g) where the = rule_rule-instance f ~ g => Has (ActiveRule f) (Proof g) where the = rule_proof-instance f ~ g => Has (ActiveRule f) (Lemma g) where the x = Lemma (the x) (the x)-instance f ~ g => Has (ActiveRule f) (Positions g) where the = rule_positions--newtype RuleId = RuleId Id deriving (Eq, Ord, Show, Num, Real, Integral, Enum)---- Add a new active.-{-# INLINEABLE addActive #-}-addActive :: Function f => Config -> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f-addActive config state@State{..} active0 =-  {-# SCC addActive #-}-  let-    active@Active{..} = active0 st_next_active st_next_rule (succ st_next_rule)-    state' =-      message (NewActive active) $-      addActiveOnly state{st_next_active = st_next_active+1, st_next_rule = st_next_rule+2} active-    passives =-      concatMap (makePassive config state') active_rules-  in if subsumed st_joinable st_rules (unorient active_rule) then-    state-  else-    normaliseGoals $-    foldl' enqueue state' passives---- Add an active without generating critical pairs. Used in interreduction.-{-# INLINEABLE addActiveOnly #-}-addActiveOnly :: Function f => State f -> Active f -> State f-addActiveOnly state@State{..} active@Active{..} =-  state {-    st_rules = foldl' insertRule st_rules active_rules,-    st_active_ids = IntMap.insert (fromIntegral active_id) active st_active_ids,-    st_rule_ids = foldl' insertRuleId st_rule_ids active_rules }-  where-    insertRule rules rule@ActiveRule{..} =-      RuleIndex.insert (lhs rule_rule) rule rules-    insertRuleId rules rule@ActiveRule{..} =-      IntMap.insert (fromIntegral rule_rid) rule rules---- Delete an active. Used in interreduction, not suitable for general use.-{-# INLINE deleteActive #-}-deleteActive :: Function f => State f -> Active f -> State f-deleteActive state@State{..} Active{..} =-  state {-    st_rules = foldl' deleteRule st_rules active_rules,-    st_active_ids = IntMap.delete (fromIntegral active_id) st_active_ids,-    st_rule_ids = foldl' deleteRuleId st_rule_ids active_rules }-  where-    deleteRule rules rule =-      RuleIndex.delete (lhs (rule_rule rule)) rule rules-    deleteRuleId rules ActiveRule{..} =-      IntMap.delete (fromIntegral rule_rid) rules---- Try to join a critical pair.-{-# INLINEABLE consider #-}-consider :: Function f => Config -> State f -> CriticalPair f -> State f-consider config state cp =-  considerUsing (st_rules state) config state cp---- Try to join a critical pair, but using a different set of critical--- pairs for normalisation.-{-# INLINEABLE considerUsing #-}-considerUsing ::-  Function f =>-  RuleIndex f (ActiveRule f) -> Config -> State f -> CriticalPair f -> State f-considerUsing rules config@Config{..} state@State{..} cp0 =-  {-# SCC consider #-}-  -- Important to canonicalise the rule so that we don't get-  -- bigger and bigger variable indices over time-  let cp = canonicalise cp0 in-  case joinCriticalPair cfg_join st_joinable rules Nothing cp of-    Right (mcp, cps) ->-      let-        state' = foldl' (considerUsing rules config) state cps-      in case mcp of-        Just cp -> addJoinable state' (cp_eqn cp)-        Nothing -> state'--    Left (cp, model) ->-      foldl' (addCP config model) state (split cp)--{-# INLINEABLE addCP #-}-addCP :: Function f => Config -> Model f -> State f -> CriticalPair f -> State f-addCP config model state@State{..} CriticalPair{..} =-  addActive config state $ \n k1 k2 ->-  let-    pf = certify cp_proof-    rule = orient cp_eqn--    makeRule k r p =-      ActiveRule {-        rule_active = n,-        rule_rid = k,-        rule_depth = cp_depth,-        rule_rule = r rule,-        rule_proof = p pf,-        rule_positions = positions (lhs (r rule)) }-  in-  Active {-    active_id = n,-    active_depth = cp_depth,-    active_rule = rule,-    active_model = model,-    active_top = cp_top,-    active_proof = pf,-    active_rules =-      usortBy (comparing (canonicalise . rule_rule)) $-        makeRule k1 id id:-        [ makeRule k2 backwards (certify . symm . derivation)-        | not (oriented (orientation rule)) ] }---- Add a new equation.-{-# INLINEABLE addAxiom #-}-addAxiom :: Function f => Config -> State f -> Axiom f -> State f-addAxiom config state axiom =-  consider config state $-    CriticalPair {-      cp_eqn = axiom_eqn axiom,-      cp_depth = 0,-      cp_top = Nothing,-      cp_proof = Proof.axiom axiom }---- Record an equation as being joinable.-{-# INLINEABLE addJoinable #-}-addJoinable :: Function f => State f -> Equation f -> State f-addJoinable state eqn@(t :=: u) =-  message (NewEquation eqn) $-  state {-    st_joinable =-      Index.insert t (t :=: u) $-      Index.insert u (u :=: t) (st_joinable state) }---- For goal terms we store the set of all their normal forms.--- Name and number are for information only.-data Goal f =-  Goal {-    goal_name   :: String,-    goal_number :: Int,-    goal_eqn    :: Equation f,-    goal_lhs    :: Set (Resulting f),-    goal_rhs    :: Set (Resulting f) }---- Add a new goal.-{-# INLINEABLE addGoal #-}-addGoal :: Function f => Config -> State f -> Goal f -> State f-addGoal _config state@State{..} goal =-  normaliseGoals state { st_goals = goal:st_goals }---- Normalise all goals.-{-# INLINEABLE normaliseGoals #-}-normaliseGoals :: Function f => State f -> State f-normaliseGoals state@State{..} =-  {-# SCC normaliseGoals #-}-  state {-    st_goals =-      map (goalMap (successors (rewrite reduces (index_all st_rules)) . Set.toList)) st_goals }-  where-    goalMap f goal@Goal{..} =-      goal { goal_lhs = f goal_lhs, goal_rhs = f goal_rhs }---- Create a goal.-{-# INLINE goal #-}-goal :: Int -> String -> Equation f -> Goal f-goal n name (t :=: u) =-  Goal {-    goal_name = name,-    goal_number = n,-    goal_eqn = t :=: u,-    goal_lhs = Set.singleton (reduce (Refl t)),-    goal_rhs = Set.singleton (reduce (Refl u)) }--------------------------------------------------------------------------- Interreduction.--------------------------------------------------------------------------- Simplify all rules.-{-# INLINEABLE interreduce #-}-interreduce :: Function f => Config -> State f -> State f-interreduce config@Config{..} state =-  {-# SCC interreduce #-}-  let-    state' =-      foldl' (interreduce1 config)-        -- Clear out st_joinable, since we don't know which-        -- equations have made use of each active.-        state { st_joinable = Index.Nil }-        (IntMap.elems (st_active_ids state))-    in state' { st_joinable = st_joinable state }--{-# INLINEABLE interreduce1 #-}-interreduce1 :: Function f => Config -> State f -> Active f -> State f-interreduce1 config@Config{..} state active =-  -- Exclude the active from the rewrite rules when testing-  -- joinability, otherwise it will be trivially joinable.-  case-    joinCriticalPair cfg_join-      (st_joinable state)-      (st_rules (deleteActive state active))-      (Just (active_model active)) (active_cp active)-  of-    Right (_, cps) ->-      flip (foldl' (consider config)) cps $-      message (DeleteActive active) $-      deleteActive state active-    Left (cp, model)-      | not (cp_eqn cp `isInstanceOf` cp_eqn (active_cp active)) ->-        flip (foldl' (addCP config model)) (split cp) $-        message (DeleteActive active) $-        deleteActive state active-      | model /= active_model active ->-        flip addActiveOnly active { active_model = model } $-        deleteActive state active-      | otherwise ->-        state-  where-    (t :=: u) `isInstanceOf` (t' :=: u') = isJust $ do-      sub <- match t' t-      matchIn sub u' u---------------------------------------------------------------------------- The main loop.-------------------------------------------------------------------------data Output m f =-  Output {-    output_report  :: State f -> m (),-    output_message :: Message f -> m () }--{-# INLINE complete #-}-complete :: (Function f, MonadIO m) => Output m f -> Config -> State f -> m (State f)-complete Output{..} config@Config{..} state =-  flip StateM.execStateT state $ do-    tasks <- sequence-      [newTask 1 (fromIntegral cfg_renormalise_percent / 100) $ do-         lift $ output_message SimplifyQueue-         state <- StateM.get-         StateM.put $! simplifyQueue config state,-       newTask 0.25 0.05 $ do-         when cfg_simplify $ do-           lift $ output_message Interreduce-           state <- StateM.get-           StateM.put $! interreduce config state,-       newTask 10 1 $ do-         state <- StateM.get-         lift $ output_report state]--    let-      loop = do-        progress <- StateM.state (complete1 config)-        state <- StateM.get-        lift $ mapM_ output_message (messages state)-        StateM.put (clearMessages state)-        mapM_ checkTask tasks-        when progress loop--    loop--{-# INLINEABLE complete1 #-}-complete1 :: Function f => Config -> State f -> (Bool, State f)-complete1 config@Config{..} state-  | st_considered state >= cfg_max_critical_pairs =-    (False, state)-  | solved state = (False, state)-  | otherwise =-    case dequeue config state of-      (Nothing, state) -> (False, state)-      (Just (overlap, _, _), state) ->-        (True, consider config state overlap)--{-# INLINEABLE solved #-}-solved :: Function f => State f -> Bool-solved = not . null . solutions---- Return whatever goals we have proved and their proofs.-{-# INLINEABLE solutions #-}-solutions :: Function f => State f -> [ProvedGoal f]-solutions State{..} = {-# SCC solutions #-} do-  Goal{goal_lhs = ts, goal_rhs = us, ..} <- st_goals-  guard (not (null (Set.intersection ts us)))-  let t:_ = filter (`Set.member` us) (Set.toList ts)-      u:_ = filter (== t) (Set.toList us)-      -- Strict so that we check the proof before returning a solution-      !p =-        Proof.certify $-          reductionProof (reduction t) `Proof.trans`-          Proof.symm (reductionProof (reduction u))-  return (provedGoal goal_number goal_name p)---- Return all current rewrite rules.-{-# INLINEABLE rules #-}-rules :: Function f => State f -> [Rule f]-rules = map active_rule . IntMap.elems . st_active_ids--{-# INLINEABLE report #-}-report :: Function f => State f -> String-report State{..} =-  printf "Statistics:\n" ++-  printf "  %d rules, of which %d oriented, %d unoriented, %d permutative, %d weakly oriented.\n"-    (length orients)-    (length [ () | Oriented <- orients ])-    (length [ () | Unoriented <- orients ])-    (length [ () | Permutative{} <- orients ])-    (length [ () | WeaklyOriented{} <- orients ]) ++-  printf "  %d queued critical pairs.\n" queuedPairs ++-  printf "  %d critical pairs considered so far." st_considered-  where-    orients = map (orientation . active_rule) (IntMap.elems st_active_ids)-    queuedPairs = Heap.size st_queue--------------------------------------------------------------------------- For code which uses twee as a library.-------------------------------------------------------------------------{-# INLINEABLE completePure #-}-completePure :: Function f => Config -> State f -> State f-completePure cfg state-  | progress = completePure cfg (clearMessages state')-  | otherwise = state'-  where-    (progress, state') = complete1 cfg state--{-# INLINEABLE normaliseTerm #-}-normaliseTerm :: Function f => State f -> Term f -> Resulting f-normaliseTerm State{..} t =-  normaliseWith (const True) (rewrite reduces (index_all st_rules)) t--{-# INLINEABLE simplifyTerm #-}-simplifyTerm :: Function f => State f -> Term f -> Term f-simplifyTerm State{..} t =-  simplify (index_oriented st_rules) t
− src/Twee/Array.hs 
@@ -1,67 +0,0 @@--- | Zero-indexed dynamic arrays, optimised for lookup.--- Modification is slow. Uninitialised indices have a default value.-{-# LANGUAGE CPP #-}-module Twee.Array where--#ifdef BOUNDS_CHECKS-import qualified Data.Primitive.SmallArray.Checked as P-#else-import qualified Data.Primitive.SmallArray as P-#endif-import Control.Monad.ST-import Data.List---- | A type which has a default value.-class Default a where-  -- | The default value.-  def :: a---- | An array.-data Array a =-  Array {-    -- | The size of the array.-    arraySize     :: {-# UNPACK #-} !Int,-    -- | The contents of the array.-    arrayContents :: {-# UNPACK #-} !(P.SmallArray a) }---- | Convert an array to a list of (index, value) pairs.-{-# INLINE toList #-}-toList :: Array a -> [(Int, a)]-toList arr =-  [ (i, x)-  | i <- [0..arraySize arr-1],-    let x = P.indexSmallArray (arrayContents arr) i ]--instance Show a => Show (Array a) where-  show arr =-    "{" ++-    intercalate ", "-      [ show i ++ "->" ++ show x-      | (i, x) <- toList arr ] ++-    "}"---- | Create an empty array.-newArray :: Default a => Array a-newArray = runST $ do-  marr <- P.newSmallArray 0 def-  arr  <- P.unsafeFreezeSmallArray marr-  return (Array 0 arr)---- | Index into an array. O(1) time.-{-# INLINE (!) #-}-(!) :: Default a => Array a -> Int -> a-arr ! n-  | 0 <= n && n < arraySize arr =-    P.indexSmallArray (arrayContents arr) n-  | otherwise = def---- | Update the array. O(n) time.-{-# 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.newSmallArray size def-  P.copySmallArray marr 0 (arrayContents arr) 0 (arraySize arr)-  P.writeSmallArray marr n $! x-  arr' <- P.unsafeFreezeSmallArray marr-  return (Array size arr')
− src/Twee/Base.hs 
@@ -1,232 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, DeriveGeneric, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}--- To suppress a warning about hiding Arity-{-# OPTIONS_GHC -fno-warn-dodgy-imports #-}-module Twee.Base(-  Id(..), Symbolic(..), subst, GSymbolic(..), Has(..), terms, TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,-  vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding,-  Minimal(..), minimalTerm, isMinimal, erase,-  Skolem(..), Arity(..), Sized(..), Ordered(..), lessThan, orientTerms, Equals(..), Strictness(..), Function, Extended(..),-  module Twee.Term, module Twee.Pretty) where--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)-import GHC.Generics hiding (Arity)-import Data.Typeable-import Data.Int-import Data.Maybe-import qualified Data.IntMap.Strict as IntMap---- Represents a unique identifier (e.g., for a rule).-newtype Id = Id { unId :: Int32 }-  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral)--instance Pretty Id where-  pPrint = text . show . unId---- Generalisation of term functionality to things that contain terms.-class Symbolic a where-  type ConstantOf a--  termsDL :: a -> DList (TermListOf a)-  default termsDL :: (Generic a, GSymbolic (ConstantOf a) (Rep a)) => a -> DList (TermListOf a)-  termsDL = gtermsDL . from-  subst_ :: (Var -> BuilderOf a) -> a -> a-  default subst_ :: (Generic a, GSymbolic (ConstantOf a) (Rep a)) => (Var -> BuilderOf a) -> a -> a-  subst_ sub = to . gsubst sub . from--class GSymbolic k f where-  gtermsDL :: f a -> DList (TermList k)-  gsubst :: (Var -> Builder k) -> f a -> f a--instance GSymbolic k V1 where-  gtermsDL _ = undefined-  gsubst _ x = x-instance GSymbolic k U1 where-  gtermsDL _ = mzero-  gsubst _ x = x-instance (GSymbolic k f, GSymbolic k g) => GSymbolic k (f :*: g) where-  gtermsDL (x :*: y) = gtermsDL x `mplus` gtermsDL y-  gsubst sub (x :*: y) = gsubst sub x :*: gsubst sub y-instance (GSymbolic k f, GSymbolic k g) => GSymbolic k (f :+: g) where-  gtermsDL (L1 x) = gtermsDL x-  gtermsDL (R1 x) = gtermsDL x-  gsubst sub (L1 x) = L1 (gsubst sub x)-  gsubst sub (R1 x) = R1 (gsubst sub x)-instance GSymbolic k f => GSymbolic k (M1 i c f) where-  gtermsDL (M1 x) = gtermsDL x-  gsubst sub (M1 x) = M1 (gsubst sub x)-instance (Symbolic a, ConstantOf a ~ k) => GSymbolic k (K1 i a) where-  gtermsDL (K1 x) = termsDL x-  gsubst sub (K1 x) = K1 (subst_ sub x)--subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a-subst sub x = subst_ (evalSubst sub) x--terms :: Symbolic a => a -> [TermListOf a]-terms = DList.toList . termsDL--type TermOf a = Term (ConstantOf a)-type TermListOf a = TermList (ConstantOf a)-type SubstOf a = Subst (ConstantOf a)-type TriangleSubstOf a = TriangleSubst (ConstantOf a)-type BuilderOf a = Builder (ConstantOf a)-type FunOf a = Fun (ConstantOf a)--instance Symbolic (Term f) where-  type ConstantOf (Term f) = f-  termsDL = return . singleton-  subst_ sub = build . Term.subst sub--instance Symbolic (TermList f) where-  type ConstantOf (TermList f) = f-  termsDL = return-  subst_ sub = buildList . Term.substList sub--instance Symbolic (Subst f) where-  type ConstantOf (Subst f) = f-  termsDL (Subst sub) = termsDL (IntMap.elems sub)-  subst_ sub (Subst s) = Subst (fmap (subst_ sub) s)--instance (ConstantOf a ~ ConstantOf b, Symbolic a, Symbolic b) => Symbolic (a, b) where-  type ConstantOf (a, b) = ConstantOf a--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--instance Symbolic a => Symbolic [a] where-  type ConstantOf [a] = ConstantOf a--instance Symbolic a => Symbolic (Maybe a) where-  type ConstantOf (Maybe a) = ConstantOf a--class Has a b where-  the :: a -> b--instance Has a a where-  the = id--{-# 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), App f _ <- subtermsList t ]--{-# INLINE occ #-}-occ :: Symbolic a => FunOf a -> a -> Int-occ x t = length (filter (== x) (funs t))--{-# INLINE occVar #-}-occVar :: Symbolic a => Var -> a -> Int-occVar x t = length (filter (== x) (vars t))--{-# INLINEABLE canonicalise #-}-canonicalise :: Symbolic a => a -> a-canonicalise t = subst sub t-  where-    sub = Term.canonicalise (DList.toList (termsDL t))--{-# INLINEABLE renameAvoiding #-}-renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b-renameAvoiding x y =-  subst (\(V x) -> var (V (x+n))) y-  where-    V n = maximum (V 0:map boundList (terms x))--isMinimal :: Minimal f => Term f -> Bool-isMinimal (App f Empty) | f == minimal = True-isMinimal _ = False--minimalTerm :: Minimal f => Term f-minimalTerm = build (con minimal)--erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a-erase [] t = t-erase xs t = subst sub t-  where-    sub = fromMaybe undefined $ flattenSubst [(x, minimalTerm) | x <- xs]--class Skolem f where-  skolem  :: Var -> Fun f--class Arity f where-  arity :: f -> Int--instance Arity f => Arity (Fun f) where-  arity = arity . fun_value--class Sized a where-  size  :: a -> Int--instance Sized f => Sized (Fun f) where-  size = size . fun_value--instance Sized f => Sized (TermList f) where-  size = aux 0-    where-      aux n Empty = n-      aux n (ConsSym (App f _) t) = aux (n+size f) t-      aux n (Cons (Var _) t) = aux (n+1) t--instance Sized f => Sized (Term f) where-  size = size . singleton--type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, Equals f)--class Equals f where-  equalsCon, trueCon, falseCon :: Fun f--data Extended f =-    Minimal-  | Skolem Var-  | Function f-  | EqualsCon | TrueCon | FalseCon-  deriving (Eq, Ord, Show, Functor)--instance Pretty f => Pretty (Extended f) where-  pPrintPrec _ _ Minimal = text "?"-  pPrintPrec _ _ (Skolem (V n)) = text "sk" <> pPrint n-  pPrintPrec l p (Function f) = pPrintPrec l p f-  pPrintPrec _ _ EqualsCon = text "$equals"-  pPrintPrec _ _ TrueCon   = text "$true"-  pPrintPrec _ _ FalseCon  = text "$false"--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 EqualsCon = 0-  size TrueCon = 0-  size FalseCon = 0-  size _ = 1--instance Arity f => Arity (Extended f) where-  arity (Function f) = arity f-  arity EqualsCon = 2-  arity _ = 0--instance (Typeable f, Ord f) => Minimal (Extended f) where-  minimal = fun Minimal--instance (Typeable f, Ord f) => Skolem (Extended f) where-  skolem x = fun (Skolem x)--instance (Typeable f, Ord f) => Equals (Extended f) where-  equalsCon = fun EqualsCon-  trueCon   = fun TrueCon-  falseCon  = fun FalseCon
− src/Twee/CP.hs 
@@ -1,325 +0,0 @@--- Critical pairs.-{-# LANGUAGE BangPatterns, FlexibleContexts, ScopedTypeVariables, MultiParamTypeClasses, RecordWildCards, OverloadedStrings, TypeFamilies, DeriveGeneric, GeneralizedNewtypeDeriving #-}-module Twee.CP where--import qualified Twee.Term as Term-import Twee.Base-import Twee.Rule-import Twee.Index(Index)-import qualified Data.Set as Set-import Control.Monad-import Data.Maybe-import Data.List-import qualified Twee.ChurchList as ChurchList-import Twee.ChurchList (ChurchList(..))-import Twee.Utils-import Twee.Equation-import qualified Twee.Proof as Proof-import Twee.Proof(Derivation, Lemma, congPath)-import GHC.Generics---- The set of positions at which a term can have critical overlaps.-data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)-type PositionsOf a = Positions (ConstantOf a)--instance Show (Positions f) where-  show = show . ChurchList.toList . positionsChurch--positions :: Term f -> Positions f-positions t = aux 0 Set.empty (singleton t)-  where-    -- Consider only general superpositions.-    aux !_ !_ Empty = NilP-    aux n m (Cons (Var _) t) = aux (n+1) m t-    aux n m (ConsSym t@App{} u)-      | t `Set.member` m = aux (n+1) m u-      | otherwise = ConsP n (aux (n+1) (Set.insert t m) u)--{-# INLINE positionsChurch #-}-positionsChurch :: Positions f -> ChurchList Int-positionsChurch posns =-  ChurchList $ \c n ->-    let-      pos NilP = n-      pos (ConsP x posns) = c x (pos posns)-    in-      pos posns---- A critical overlap of one rule with another.-data Overlap f =-  Overlap {-    overlap_depth :: {-# UNPACK #-} !Depth,-    overlap_top   :: {-# UNPACK #-} !(Term f),-    overlap_inner :: {-# UNPACK #-} !(Term f),-    overlap_pos   :: {-# UNPACK #-} !Int,-    overlap_eqn   :: {-# UNPACK #-} !(Equation f) }-  deriving Show-type OverlapOf a = Overlap (ConstantOf a)--newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)---- Compute all overlaps of a rule with a set of rules.-{-# INLINEABLE overlaps #-}-overlaps ::-  (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) =>-  Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]-overlaps max_depth idx rules r =-  ChurchList.toList (overlapsChurch max_depth idx rules r)--{-# INLINE overlapsChurch #-}-overlapsChurch :: forall f a.-  (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) =>-  Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)-overlapsChurch max_depth idx rules r1 = do-  guard (the r1 < max_depth)-  r2 <- ChurchList.fromList rules-  guard (the r2 < max_depth)-  let !depth = 1 + max (the r1) (the r2)-  do { o <- asymmetricOverlaps idx depth (the r1) r1' (the r2); return (r1, r2, o) } `mplus`-    do { o <- asymmetricOverlaps idx depth (the r2) (the r2) r1'; return (r2, r1, o) }-  where-    !r1' = renameAvoiding (map the rules :: [Rule f]) (the r1)--{-# INLINE asymmetricOverlaps #-}-asymmetricOverlaps ::-  (Function f, Has a (Rule f), Has a Depth) =>-  Index f a -> Depth -> Positions f -> Rule f -> Rule f -> ChurchList (Overlap f)-asymmetricOverlaps idx depth posns r1 r2 = do-  n <- positionsChurch posns-  ChurchList.fromMaybe $-    overlapAt n depth r1 r2 >>=-    simplifyOverlap idx---- Create an overlap at a particular position in a term.--- Doesn't simplify or check for primeness.-{-# INLINE overlapAt #-}-overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)-overlapAt !n !depth (Rule _ !outer !outer') (Rule _ !inner !inner') = do-  let t = at n (singleton outer)-  sub <- unifyTri inner t-  let-    top = {-# SCC overlap_top #-} termSubst sub outer-    innerTerm = {-# SCC overlap_inner #-} termSubst sub inner-    -- Make sure to keep in sync with overlapProof-    lhs = {-# SCC overlap_eqn_1 #-} termSubst sub outer'-    rhs = {-# SCC overlap_eqn_2 #-}-      buildReplacePositionSub sub n (singleton inner') (singleton outer)--  guard (lhs /= rhs)-  return Overlap {-    overlap_depth = depth,-    overlap_top = top,-    overlap_inner = innerTerm,-    overlap_pos = n,-    overlap_eqn = lhs :=: rhs }---- Simplify an overlap and remove it if it's trivial.-{-# INLINE simplifyOverlap #-}-simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap f)-simplifyOverlap idx overlap@Overlap{overlap_eqn = lhs :=: rhs, ..}-  | lhs == rhs'  = Nothing-  | lhs' == rhs' = Nothing-  | otherwise = Just overlap{overlap_eqn = lhs' :=: rhs'}-  where-    lhs' = simplify idx lhs-    rhs' = simplify idx rhs---- Put these in separate functions to avoid code blowup-buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f-buildReplacePositionSub !sub !n !inner' !outer =-  build (replacePositionSub sub n inner' outer)--termSubst :: TriangleSubst f -> Term f -> Term f-termSubst sub t = build (Term.subst sub t)---- The critical pair ordering heuristic.-data Config =-  Config {-    cfg_lhsweight :: !Int,-    cfg_rhsweight :: !Int,-    cfg_funweight :: !Int,-    cfg_varweight :: !Int,-    cfg_depthweight :: !Int,-    cfg_dupcost :: !Int,-    cfg_dupfactor :: !Int }---- We compute:---   cfg_lhsweight * size l + cfg_rhsweight * size r--- where l is the biggest term and r is the smallest,--- and variables have weight 1 and functions have weight cfg_funweight.-{-# INLINEABLE score #-}-score :: Function f => Config -> Overlap f -> Int-score config overlap@Overlap{overlap_eqn = t :=: u} =-  -- Look at the length to decide on various special cases-  case (len t, len u) of-    (1, 1) ->-      -- true = false-      fromMaybe (normalScore config overlap)-        (trueEqualsFalse t u `mplus` trueEqualsFalse u t)-    (1, _) ->-      -- false = equals(t, u) where t, u unifiable-      fromMaybe (normalScore config overlap)-        (equalsFalse t u)-    (_, 1) ->-      -- equals(t, u) = false where t, u unifiable-      fromMaybe (normalScore config overlap)-        (equalsFalse u t)-    _ -> normalScore config overlap-  where-    -- N.B. the code above puts the arguments in the right order-    trueEqualsFalse (App true Empty) (App false Empty)-      | true == trueCon && false == falseCon = Just 1-    trueEqualsFalse _ _ = Nothing--    equalsFalse (App false Empty) (App equals (Cons t (Cons u Empty)))-      | false == falseCon && equals == equalsCon =-        if isJust (unify t u) then Just 2-        else Just (normalScore config overlap{overlap_eqn = t :=: u})-    equalsFalse _ _ = Nothing--{-# INLINEABLE normalScore #-}-normalScore :: Function f => Config -> Overlap f -> Int-normalScore Config{..} Overlap{..} =-  fromIntegral overlap_depth * cfg_depthweight +-  (m + n) * cfg_rhsweight +-  intMax m n * (cfg_lhsweight - cfg_rhsweight)-  where-    l :=: r = overlap_eqn-    m = size' 0 (singleton l)-    n = size' 0 (singleton r)--    size' !n Empty = n-    size' n (Cons t ts)-      | len t > 1, t `isSubtermOfList` ts =-        size' (n+cfg_dupcost+cfg_dupfactor*size t) ts-    size' n (Cons (Var _) ts) =-      size' (n+cfg_varweight) ts-    size' n (ConsSym (App f _) ts) =-      size' (n+cfg_funweight*size f) ts--------------------------------------------------------------------------- Higher-level handling of critical pairs.--------------------------------------------------------------------------- A critical pair together with information about how it was derived-data CriticalPair f =-  CriticalPair {-    cp_eqn   :: {-# UNPACK #-} !(Equation f),-    cp_depth :: {-# UNPACK #-} !Depth,-    cp_top   :: !(Maybe (Term f)),-    cp_proof :: !(Derivation f) }-  deriving Generic--instance Symbolic (CriticalPair f) where-  type ConstantOf (CriticalPair f) = f-  termsDL CriticalPair{..} =-    termsDL cp_eqn `mplus` termsDL cp_top `mplus` termsDL cp_proof-  subst_ sub CriticalPair{..} =-    CriticalPair {-      cp_eqn = subst_ sub cp_eqn,-      cp_depth = cp_depth,-      cp_top = subst_ sub cp_top,-      cp_proof = subst_ sub cp_proof }--instance PrettyTerm f => Pretty (CriticalPair f) where-  pPrint CriticalPair{..} =-    vcat [-      pPrint cp_eqn,-      nest 2 (text "top:" <+> pPrint cp_top) ]---- Split a critical pair so that it can be turned into rules.--- See the comment below.-split :: Function f => CriticalPair f -> [CriticalPair f]-split CriticalPair{cp_eqn = l :=: r, ..}-  | l == r = []-  | otherwise =-    -- If we have something which is almost a rule, except that some-    -- variables appear only on the right-hand side, e.g.:-    --   f x y -> g x z-    -- then we replace it with the following two rules:-    --   f x y -> g x ?-    --   g x z -> g x ?-    -- where the second rule is weakly oriented and ? is the minimal-    -- constant.-    ---    -- If we have an unoriented equation with a similar problem, e.g.:-    --   f x y = g x z-    -- then we replace it with potentially three rules:-    --   f x ? = g x ?-    --   f x y -> f x ?-    --   g x z -> g x ?--    -- The main rule l -> r' or r -> l' or l' = r'-    [ CriticalPair {-        cp_eqn   = l :=: r',-        cp_depth = cp_depth,-        cp_top   = eraseExcept (vars l) cp_top,-        cp_proof = eraseExcept (vars l) cp_proof }-    | ord == Just GT ] ++-    [ CriticalPair {-        cp_eqn   = r :=: l',-        cp_depth = cp_depth,-        cp_top   = eraseExcept (vars r) cp_top,-        cp_proof = Proof.symm (eraseExcept (vars r) cp_proof) }-    | ord == Just LT ] ++-    [ CriticalPair {-        cp_eqn   = l' :=: r',-        cp_depth = cp_depth,-        cp_top   = eraseExcept (vars l) $ eraseExcept (vars r) cp_top,-        cp_proof = eraseExcept (vars l) $ eraseExcept (vars r) cp_proof }-    | ord == Nothing ] ++--    -- Weak rules l -> l' or r -> r'-    [ CriticalPair {-        cp_eqn   = l :=: l',-        cp_depth = cp_depth + 1,-        cp_top   = Nothing,-        cp_proof = cp_proof `Proof.trans` Proof.symm (erase ls cp_proof) }-    | not (null ls), ord /= Just GT ] ++-    [ CriticalPair {-        cp_eqn   = r :=: r',-        cp_depth = cp_depth + 1,-        cp_top   = Nothing,-        cp_proof = Proof.symm cp_proof `Proof.trans` erase rs cp_proof }-    | 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)--      eraseExcept vs t =-        erase (usort (vars t) \\ usort vs) t--{-# INLINEABLE makeCriticalPair #-}-makeCriticalPair ::-  (Has a (Rule f), Has a (Lemma f), Has a Id, Function f) =>-  a -> a -> Overlap f -> Maybe (CriticalPair f)-makeCriticalPair r1 r2 overlap@Overlap{..}-  | lessEq overlap_top t = Nothing-  | lessEq overlap_top u = Nothing-  | otherwise =-    Just $-      CriticalPair overlap_eqn-        overlap_depth-        (Just overlap_top)-        (overlapProof r1 r2 overlap)-  where-    t :=: u = overlap_eqn---- Return a proof for a critical pair.-{-# INLINEABLE overlapProof #-}-overlapProof ::-  forall a f.-  (Has a (Rule f), Has a (Lemma f), Has a Id) =>-  a -> a -> Overlap f -> Derivation f-overlapProof left right Overlap{..} =-  Proof.symm (reductionProof (step left leftSub))-  `Proof.trans`-  congPath path overlap_top (reductionProof (step right rightSub))-  where-    Just leftSub = match (lhs (the left)) overlap_top-    Just rightSub = match (lhs (the right)) overlap_inner--    path = positionToPath (lhs (the left) :: Term f) overlap_pos
− src/Twee/ChurchList.hs 
@@ -1,99 +0,0 @@--- Church-encoded lists. Used in Twee.CP to make sure that fusion happens.-{-# LANGUAGE Rank2Types, BangPatterns #-}-module Twee.ChurchList where--import Prelude(Functor(..), Applicative(..), Monad(..), Bool(..), Maybe(..), (.), ($), id)-import qualified Prelude-import GHC.Magic(oneShot)-import GHC.Exts(build)-import Control.Monad(MonadPlus(..), liftM2)-import Control.Applicative(Alternative(..))--newtype ChurchList a =-  ChurchList (forall b. (a -> b -> b) -> b -> b)--{-# INLINE foldr #-}-foldr :: (a -> b -> b) -> b -> ChurchList a -> b-foldr op e (ChurchList f) = eta (f op (eta e))-  -- Using eta here seems to help with eta-expanding foldl'--{-# INLINE[0] eta #-}-eta :: a -> a-eta x = x-{-# RULES "eta" forall f. eta f = \x -> f x #-}--{-# INLINE nil #-}-nil :: ChurchList a-nil = ChurchList (\_ n -> n)--{-# INLINE unit #-}-unit :: a -> ChurchList a-unit x = ChurchList (\c n -> c x n)--{-# INLINE cons #-}-cons :: a -> ChurchList a -> ChurchList a-cons x xs = ChurchList (\c n -> c x (foldr c n xs))--{-# INLINE append #-}-append :: ChurchList a -> ChurchList a -> ChurchList a-append xs ys = ChurchList (\c n -> foldr c (foldr c n ys) xs)--{-# INLINE join #-}-join :: ChurchList (ChurchList a) -> ChurchList a-join xss = ChurchList (\c n -> foldr (\xs ys -> foldr c ys xs) n xss)--instance Functor ChurchList where-  {-# INLINE fmap #-}-  fmap f xs = ChurchList (\c n -> foldr (c . f) n xs)--instance Applicative ChurchList where-  {-# INLINE pure #-}-  pure = return-  {-# INLINE (<*>) #-}-  (<*>) = liftM2 ($)--instance Monad ChurchList where-  {-# INLINE return #-}-  return = unit-  {-# INLINE (>>=) #-}-  xs >>= f = join (fmap f xs)--instance Alternative ChurchList where-  {-# INLINE empty #-}-  empty = nil-  {-# INLINE (<|>) #-}-  (<|>) = append--instance MonadPlus ChurchList where-  {-# INLINE mzero #-}-  mzero = empty-  {-# INLINE mplus #-}-  mplus = (<|>)--{-# INLINE fromList #-}-fromList :: [a] -> ChurchList a-fromList xs = ChurchList (\c n -> Prelude.foldr c n xs)--{-# INLINE toList #-}-toList :: ChurchList a -> [a]-toList (ChurchList f) = build f--{-# INLINE foldl' #-}-foldl' :: (b -> a -> b) -> b -> ChurchList a -> b-foldl' op e xs =-  foldr (\x f -> oneShot (\ (!acc) -> f (op acc x))) id xs e--{-# INLINE filter #-}-filter :: (a -> Bool) -> ChurchList a -> ChurchList a-filter p xs =-  ChurchList $ \c n ->-    let            -      {-# INLINE op #-}-      op x xs = if p x then c x xs else xs-    in-      foldr op n xs--{-# INLINE fromMaybe #-}-fromMaybe :: Maybe a -> ChurchList a-fromMaybe Nothing = nil-fromMaybe (Just x) = unit x
− src/Twee/Constraints.hs 
@@ -1,297 +0,0 @@-{-# LANGUAGE FlexibleContexts, UndecidableInstances, RecordWildCards #-}-module Twee.Constraints where----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, Eq, Ord)--{-# INLINE atoms #-}-atoms :: Term f -> [Atom f]-atoms t = aux (singleton t)-  where-    aux Empty = []-    aux (Cons (App 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 (App f Empty) = Just (Constant f)-fromTerm (Var x) = Just (Variable x)-fromTerm _ = Nothing--instance 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 (Eq, Ord, Show)--instance 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_ [] = undefined-  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_ [] = undefined--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)],  -- sorted-    equals      :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair-  deriving (Eq, Ord)--instance 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 :: (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 :: (Minimal f, Ordered 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 :: (Minimal f, Ordered 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 :: (Minimal f, Ordered 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 :: (Minimal f, Ordered 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 :: (Minimal f, Ordered f) => Atom f -> Branch f -> Branch f-addTerm (Constant f) b-  | f `notElem` funs b =-    b {-      funs = f:funs b,-      less =-        usort $-          [ (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 (Eq, 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 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 :: (Minimal f, Ord f) => [Atom f] -> Model f-modelFromOrder xs =-  Model (Map.fromList [(x, (i, i)) | (x, i) <- zip xs [0..]])--weakenModel :: 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 :: (Minimal f, Ord f) => Model f -> Var -> Bool-varInModel (Model m) x = Variable x `Map.member` m--varGroups :: (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 f where-  minimal :: Fun f--{-# INLINE lessEqInModel #-}-lessEqInModel :: (Minimal f, Ordered 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 :: (Minimal f, Ordered 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 undefined . 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, x /= Constant minimal]-      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-  lessEq :: Term f -> Term f -> Bool-  lessIn :: Model f -> Term f -> Term f -> Maybe Strictness--data Strictness = Strict | Nonstrict deriving (Eq, Show)--lessThan :: Ordered f => Term f -> Term f -> Bool-lessThan t u = lessEq t u && isNothing (unify t u)--orientTerms :: Ordered f => 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
− src/Twee/Equation.hs 
@@ -1,55 +0,0 @@-{-# LANGUAGE DeriveGeneric, TypeFamilies #-}-module Twee.Equation where--import Twee.Base-import GHC.Generics-import Data.Maybe------------------------------------------------------------------------------------- Equations.-----------------------------------------------------------------------------------data Equation f =-  (:=:) {-    eqn_lhs :: {-# UNPACK #-} !(Term f),-    eqn_rhs :: {-# UNPACK #-} !(Term f) }-  deriving (Eq, Ord, Show, Generic)-type EquationOf a = Equation (ConstantOf a)--instance Symbolic (Equation f) where-  type ConstantOf (Equation f) = f--instance PrettyTerm f => Pretty (Equation f) where-  pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y--instance Sized f => Sized (Equation f) where-  size (x :=: y) = size x + size y---- Order an equation roughly left-to-right.--- However, there is no guarantee that the result is oriented.-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---- Apply a function to both sides of an equation.-bothSides :: (Term f -> Term f') -> Equation f -> Equation f'-bothSides f (t :=: u) = f t :=: f u---- Is an equation of the form t = t?-trivial :: Eq f => Equation f -> Bool-trivial (t :=: u) = t == u--simplerThan :: Function f => Equation f -> Equation f -> Bool-eq1 `simplerThan` eq2 =-  t1 `lessEq` t2 &&-  (isNothing (unify t1 t2) || (u1 `lessEq` u2))-  where-    t1 :=: u1 = skolemise eq1-    t2 :=: u2 = skolemise eq2--    skolemise = subst (con . skolem)
− src/Twee/Heap.hs 
@@ -1,130 +0,0 @@-{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}--- Skew heaps.-module Twee.Heap(-  Heap, empty, insert, removeMin, mapMaybe, size) where--data Heap a = Heap {-# UNPACK #-} !Int !(Heap1 a) deriving Show-data Heap1 a = Nil | Node a (Heap1 a) (Heap1 a) deriving Show--{-# INLINEABLE merge #-}-merge :: Ord a => Heap a -> Heap a -> Heap a-merge (Heap n1 h1) (Heap n2 h2) = Heap (n1+n2) (merge1 h1 h2)--{-# INLINEABLE merge1 #-}-merge1 :: forall a. Ord a => Heap1 a -> Heap1 a -> Heap1 a-merge1 = m1-  where-    -- For some reason using m1 improves the code generation...-    m1 :: Heap1 a -> Heap1 a -> Heap1 a-    m1 Nil h = h-    m1 h Nil = h-    m1 h1@(Node x1 l1 r1) h2@(Node x2 l2 r2)-      | x1 <= x2 = (Node x1 $! m1 r1 h2) l1-      | otherwise = (Node x2 $! m1 r2 h1) l2--{-# INLINE unit #-}-unit :: a -> Heap a-unit !x = Heap 1 (Node x Nil Nil)--{-# INLINE empty #-}-empty :: Heap a-empty = Heap 0 Nil--{-# INLINEABLE insert #-}-insert :: Ord a => a -> Heap a -> Heap a-insert x h = merge (unit x) h--{-# INLINEABLE removeMin #-}-removeMin :: Ord a => Heap a -> Maybe (a, Heap a)-removeMin (Heap _ Nil) = Nothing-removeMin (Heap n (Node x l r)) = Just (x, Heap (n-1) (merge1 l r))--{-# INLINEABLE mapMaybe #-}-mapMaybe :: Ord b => (a -> Maybe b) -> Heap a -> Heap b-mapMaybe f (Heap _ h) = Heap (sz 0 h') h'-  where-    sz !n Nil = n-    sz !n (Node _ l r) = sz (sz (n+1) l) r--    h' = go h--    go Nil = Nil-    go (Node x l r) =-      case f x of-        Nothing -> merge1 l' r'-        Just !y -> down y l' r'-      where-        !l' = go l-        !r' = go r--    down x l@(Node y ll lr) r@(Node z rl rr)-      | y < x && y <= z =-        (Node y $! down x ll lr) r-      | z < x && z <= y =-        Node z l $! down x rl rr-    down x Nil (Node y l r)-      | y < x =-        Node y Nil $! down x l r-    down x (Node y l r) Nil-      | y < x =-        (Node y $! down x l r) Nil-    down x l r = Node x l r--{-# INLINE size #-}-size :: Heap a -> Int-size (Heap n _) = n---- Testing code:--- import Test.QuickCheck--- import qualified Data.List as List--- import qualified Data.Maybe as Maybe---- instance (Arbitrary a, Ord a) => Arbitrary (Heap a) where---   arbitrary = sized arb---     where---       arb 0 = return empty---       arb n =---         frequency---           [(1, unit <$> arbitrary),---            (n-1, merge <$> arb' <*> arb')]---         where---           arb' = arb (n `div` 2)---- toList :: Ord a => Heap a -> [a]--- toList = List.unfoldr removeMin---- invariant :: Ord a => Heap a -> Bool--- invariant h@(Heap n h1) =---   n == length (toList h) && ord h1---   where---     ord Nil = True---     ord (Node x l r) = ord1 x l && ord1 x r----     ord1 _ Nil = True---     ord1 x h@(Node y _ _) = x <= y && ord h---- prop_1 h = withMaxSuccess 10000 $ invariant h--- prop_2 x h = withMaxSuccess 10000 $ invariant (insert x h)--- prop_3 h =---   withMaxSuccess 1000 $---   case removeMin h of---     Nothing -> discard---     Just (_, h) -> invariant h--- prop_4 h = withMaxSuccess 10000 $ List.sort (toList h) == toList h--- prop_5 x h = withMaxSuccess 10000 $ toList (insert x h) == List.insert x (toList h)--- prop_6 x h =---   withMaxSuccess 1000 $---   case removeMin h of---     Nothing -> discard---     Just (x, h') -> toList h == List.insert x (toList h')--- prop_7 h1 h2 = withMaxSuccess 10000 $---   invariant (merge h1 h2)--- prop_8 h1 h2 = withMaxSuccess 10000 $---   toList (merge h1 h2) == List.sort (toList h1 ++ toList h2)--- prop_9 (Blind f) h = withMaxSuccess 10000 $---   invariant (mapMaybe f h)--- prop_10 (Blind f) h = withMaxSuccess 1000000 $---   toList (mapMaybe f h) == List.sort (Maybe.mapMaybe f (toList h))---- return []--- main = $quickCheckAll
− src/Twee/Index.hs 
@@ -1,161 +0,0 @@--- Term indexing (perfect-ish discrimination trees).-{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts #-}--- We get some bogus warnings because of pattern synonyms.-{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}-module Twee.Index(module Twee.Index, module Twee.Index.Lookup) where--import qualified Prelude-import Prelude hiding (filter, map, null)-import Data.Maybe-import Twee.Base hiding (var, fun, empty, size, singleton, prefix, funs, lookupList)-import qualified Twee.Term as Term-import Twee.Array-import qualified Data.List as List-import Twee.Utils-import Twee.Index.Lookup--{-# INLINE null #-}-null :: Index f a -> Bool-null Nil = True-null _ = False--{-# INLINEABLE singleton #-}-singleton :: Term f -> a -> Index f a-singleton !t x = singletonEntry (key t) x--{-# INLINE singletonEntry #-}-singletonEntry :: TermList f -> a -> Index f a-singletonEntry t x = Index 0 t [x] newArray newVarIndex--{-# INLINE withPrefix #-}-withPrefix :: TermList f -> Index f a -> Index f a-withPrefix Empty idx = idx-withPrefix _ Nil = Nil-withPrefix t idx@Index{..} =-  idx{prefix = buildList (builder t `mappend` builder prefix)}--insert :: Term f -> a -> Index f a -> Index f a-insert !t x !idx = {-# SCC insert #-} aux (key t) idx-  where-    aux t Nil = singletonEntry t x-    aux (Cons t ts) idx@Index{prefix = Cons u us} | t == u =-      withPrefix (Term.singleton t) (aux ts idx{prefix = us})-    aux t idx@Index{prefix = Cons{}} = aux t (expand idx)--    aux Empty idx =-      idx { size = 0, here = x:here idx }-    aux t@(ConsSym (App f _) u) idx =-      idx {-        size = lenList t `min` size idx,-        fun  = update (fun_id f) idx' (fun idx) }-      where-        idx' = aux u (fun idx ! fun_id f)-    aux t@(ConsSym (Var v) u) idx =-      idx {-        size = lenList t `min` size idx,-        var  = updateVarIndex v idx' (var idx) }-      where-        idx' = aux u (lookupVarIndex v (var idx))--{-# INLINE expand #-}-expand :: Index f a -> Index f a-expand idx@Index{prefix = ConsSym t ts} =-  case t of-    Var v ->-      Index (size idx + 1 + lenList ts) emptyTermList [] newArray-        (updateVarIndex v idx { prefix = ts } newVarIndex)-    App f _ ->-      Index (size idx + 1 + lenList ts) emptyTermList []-        (update (fun_id f) idx { prefix = ts } newArray) newVarIndex--key :: Term f -> TermList f-key t = buildList . aux . Term.singleton $ t-  where-    repeatedVars = [x | x <- usort (vars t), occVar x t > 1]--    aux Empty = mempty-    aux (ConsSym (App f _) t) =-      con f `mappend` aux t-    aux (ConsSym (Var x) t) =-      Term.var (-      case List.elemIndex x (take varIndexCapacity repeatedVars) of-         Nothing -> V 2-         Just n  -> V n) `mappend` aux t--{-# INLINEABLE delete #-}-delete :: Eq a => Term f -> a -> Index f a -> Index f a-delete !t x !idx = {-# SCC delete #-} aux (key t) idx-  where-    aux _ Nil = Nil-    aux (Cons t ts) idx@Index{prefix = Cons u us} | t == u =-      withPrefix (Term.singleton t) (aux ts idx{prefix = us})-    aux _ idx@Index{prefix = Cons{}} = idx--    aux Empty idx-      | x `List.elem` here idx =-        idx { here = List.delete x (here idx) }-      | otherwise =-        error "deleted term not found in index"-    aux (ConsSym (App f _) t) idx =-      idx { fun = update (fun_id f) (aux t (fun idx ! fun_id f)) (fun idx) }-    aux (ConsSym (Var v) t) idx =-      idx { var = updateVarIndex v (aux t (lookupVarIndex v (var idx))) (var idx) }--{-# INLINEABLE elem #-}-elem :: Eq a => Term f -> a -> Index f a -> Bool-elem !t x !idx = aux (key t) idx-  where-    aux _ Nil = False-    aux (Cons t ts) idx@Index{prefix = Cons u us} | t == u =-      aux ts idx{prefix = us}-    aux _ Index{prefix = Cons{}} = False--    aux Empty idx = List.elem x (here idx)-    aux (ConsSym (App f _) t) idx =-      aux t (fun idx ! fun_id f)-    aux (ConsSym (Var v) t) idx =-      aux t (lookupVarIndex v (var idx))--approxMatchesList :: TermList f -> Index f a -> [a]-approxMatchesList t idx =-  {-# SCC approxMatchesList #-}-  run (Frame emptySubst2 t idx Stop)--{-# INLINE approxMatches #-}-approxMatches :: Term f -> Index f a -> [a]-approxMatches t idx = approxMatchesList (Term.singleton t) idx--{-# INLINEABLE matchesList #-}-matchesList :: Has a (Term f) => TermList f -> Index f a -> [(Subst f, a)]-matchesList t idx =-  [ (sub, x)-  | x <- approxMatchesList t idx,-    sub <- maybeToList (matchList (Term.singleton (the x)) t)]--{-# INLINE matches #-}-matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]-matches t idx = matchesList (Term.singleton t) idx--{-# INLINEABLE lookupList #-}-lookupList :: (Has a b, Symbolic b, Has b (TermOf b)) => TermListOf b -> Index (ConstantOf b) a -> [b]-lookupList t idx =-  [ subst sub x-  | x <- List.map the (approxMatchesList t idx),-    sub <- maybeToList (matchList (Term.singleton (the x)) t)]--{-# INLINE lookup #-}-lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]-lookup t idx = lookupList (Term.singleton t) idx--{-# NOINLINE run #-}-run :: Stack f a -> [a]-run Stop = []-run Frame{..} = run ({-# SCC run_inner #-} step frame_subst frame_term frame_index frame_rest)-run Yield{..} = {-# SCC run_found #-} yield_found ++ run yield_rest--elems :: Index f a -> [a]-elems Nil = []-elems idx =-  here idx ++-  concatMap elems (Prelude.map snd (toList (fun idx))) ++-  concatMap elems (varIndexElems (var idx))
− src/Twee/Index/Lookup.hs 
@@ -1,119 +0,0 @@--- Term indexing (perfect-ish discrimination trees).--- This module contains the type definitions and lookup function.--- We put lookup in a separate module because it needs to be compiled--- with inlining switched up to max, and compiling the rest of the module--- like that is too slow.-{-# LANGUAGE BangPatterns, RecordWildCards #-}-{-# OPTIONS_GHC -funfolding-creation-threshold=10000 -funfolding-use-threshold=10000 #-}-module Twee.Index.Lookup where--import Twee.Base hiding (var, fun, empty, size, singleton, prefix, funs)-import qualified Twee.Term as Term-import Twee.Term.Core(TermList(..))-import Twee.Array--data Index f a =-  Index {-    size   :: {-# UNPACK #-} !Int, -- size of smallest term, not including prefix-    prefix :: {-# UNPACK #-} !(TermList f),-    here   :: [a],-    fun    :: {-# UNPACK #-} !(Array (Index f a)),-    var    :: {-# UNPACK #-} !(VarIndex f a) } |-  Nil-  deriving Show--instance Default (Index f a) where def = Nil--data VarIndex f a =-  VarIndex {-    var0 :: !(Index f a),-    var1 :: !(Index f a),-    hole :: !(Index f a) }-  deriving Show--{-# INLINE newVarIndex #-}-newVarIndex :: VarIndex f a-newVarIndex = VarIndex Nil Nil Nil--{-# INLINE lookupVarIndex #-}-lookupVarIndex :: Var -> VarIndex f a -> Index f a-lookupVarIndex (V 0) vidx = var0 vidx-lookupVarIndex (V 1) vidx = var1 vidx-lookupVarIndex _ vidx = hole vidx--{-# INLINE updateVarIndex #-}-updateVarIndex :: Var -> Index f a -> VarIndex f a -> VarIndex f a-updateVarIndex (V 0) idx vidx = vidx { var0 = idx }-updateVarIndex (V 1) idx vidx = vidx { var1 = idx }-updateVarIndex _ idx vidx = vidx { hole = idx }--varIndexElems :: VarIndex f a -> [Index f a]-varIndexElems vidx = [var0 vidx, var1 vidx, hole vidx]--varIndexToList :: VarIndex f a -> [(Int, Index f a)]-varIndexToList vidx = [(0, var0 vidx), (1, var1 vidx), (2, hole vidx)]--varIndexCapacity :: Int-varIndexCapacity = 2--data Subst2 f = Subst2 {-# UNPACK #-} !Int {-# UNPACK #-} !Int {-# UNPACK #-} !Int {-# UNPACK #-} !Int--emptySubst2 :: Subst2 f-emptySubst2 = Subst2 0 0 0 0--{-# INLINE extend2 #-}-extend2 :: Var -> TermList f -> Subst2 f -> Maybe (Subst2 f)-extend2 (V 0) t (Subst2 _ 0 x y) = Just (Subst2 (low t) (high t) x y)-extend2 (V 0) t (Subst2 x y _ _) | t /= TermList x y (array t) = Nothing-extend2 (V 1) u (Subst2 x y _ 0) = Just (Subst2 x y (low u) (high u))-extend2 (V 1) u (Subst2 _ _ x y) | u /= TermList x y (array u) = Nothing-extend2 _ _ sub = Just sub--data Stack f a =-  Frame {-    frame_subst :: {-# UNPACK #-} !(Subst2 f),-    frame_term  :: {-# UNPACK #-} !(TermList f),-    frame_index :: !(Index f a),-    frame_rest  :: !(Stack f a) }-  | Yield {-    yield_found :: [a],-    yield_rest  :: !(Stack f a) }-  | Stop--step !_ !_ _ _ | False = undefined-step _ _ Nil rest = rest-step _ t Index{size = size, prefix = prefix} rest-  | lenList t < size + lenList prefix = rest-step sub t Index{..} rest = pref sub t prefix here fun var rest--pref !_ !_ !_ _ !_ !_ _ | False = undefined-pref _ Empty Empty [] _ _ rest = rest-pref _ Empty Empty here _ _ rest = Yield here rest-pref _ Empty _ _ _ _ _ = undefined -- implies lenList t < size + lenList prefix above-pref sub (Cons t ts) (Cons (Var x) us) here fun var rest =-  case extend2 x (Term.singleton t) sub of-    Nothing  -> rest-    Just sub -> pref sub ts us here fun var rest-pref sub (ConsSym (App f _) ts) (ConsSym (App g _) us) here fun var rest-  | f == g = pref sub ts us here fun var rest-pref _ _ (Cons _ _) _ _ _ rest = rest-pref sub t@(Cons u us) Empty _ fun var rest =-  tryFun sub v vs fun (tryVar sub u us var rest)-  where-    UnsafeConsSym v vs = t--    {-# INLINE tryFun #-}-    tryFun sub (App f _) ts fun rest =-      case fun ! fun_id f of-        Nil -> rest-        idx -> Frame sub ts idx rest-    tryFun _ _ _ _ rest = rest--    {-# INLINE tryVar #-}-    tryVar sub t ts var rest =-      foldr op rest (varIndexToList var)-      where-        op (x, idx@Index{}) rest-          | Just sub <- extend2 (V x) (Term.singleton t) sub =-              Frame sub ts idx rest-        op _ rest = rest
− src/Twee/Join.hs 
@@ -1,212 +0,0 @@--- Tactics for joining critical pairs.-{-# LANGUAGE FlexibleContexts, BangPatterns, RecordWildCards, TypeFamilies, DeriveGeneric #-}-module Twee.Join where--import Twee.Base-import Twee.Rule-import Twee.Equation-import Twee.Proof(Lemma)-import qualified Twee.Proof as Proof-import Twee.CP hiding (Config)-import Twee.Constraints-import qualified Twee.Index as Index-import Twee.Index(Index)-import Twee.Rule.Index(RuleIndex(..))-import Twee.Utils-import Data.Maybe-import Data.Either-import Data.Ord-import qualified Data.Set as Set--data Config =-  Config {-    cfg_ground_join :: !Bool,-    cfg_use_connectedness :: !Bool,-    cfg_set_join :: !Bool }--defaultConfig :: Config-defaultConfig =-  Config {-    cfg_ground_join = True,-    cfg_use_connectedness = False,-    cfg_set_join = False }--{-# INLINEABLE joinCriticalPair #-}-joinCriticalPair ::-  (Function f, Has a (Rule f), Has a (Lemma f)) =>-  Config ->-  Index f (Equation f) -> RuleIndex f a ->-  Maybe (Model f) -> -- A model to try before checking ground joinability-  CriticalPair f ->-  Either-    -- Failed to join critical pair.-    -- Returns simplified critical pair and model in which it failed to hold.-    (CriticalPair f, Model f)-    -- Split critical pair into several instances.-    -- Returns list of instances which must be joined,-    -- and an optional equation which can be added to the joinable set-    -- after successfully joining all instances.-    (Maybe (CriticalPair f), [CriticalPair f])-joinCriticalPair config eqns idx mmodel cp@CriticalPair{cp_eqn = t :=: u} =-  {-# SCC joinCriticalPair #-}-  case allSteps config eqns idx cp of-    Nothing ->-      Right (Nothing, [])-    _ | cfg_set_join config &&-        not (null $ Set.intersection-          (normalForms (rewrite reduces (index_all idx)) [reduce (Refl t)])-          (normalForms (rewrite reduces (index_all idx)) [reduce (Refl u)])) ->-      Right (Just cp, [])-    Just cp ->-      case groundJoinFromMaybe config eqns idx mmodel (branches (And [])) cp of-        Left model -> Left (cp, model)-        Right cps -> Right (Just cp, cps)--{-# INLINEABLE step1 #-}-{-# INLINEABLE step2 #-}-{-# INLINEABLE step3 #-}-{-# INLINEABLE allSteps #-}-step1, step2, step3, allSteps ::-  (Function f, Has a (Rule f), Has a (Lemma f)) =>-  Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)-allSteps config eqns idx cp =-  step1 config eqns idx cp >>=-  step2 config eqns idx >>=-  step3 config eqns idx-step1 _ eqns idx = joinWith eqns idx (\t _ -> normaliseWith (const True) (rewrite reducesOriented (index_oriented idx)) t)-step2 _ eqns idx = joinWith eqns idx (\t _ -> normaliseWith (const True) (rewrite reduces (index_all idx)) t)-step3 Config{..} eqns idx cp-  | not cfg_use_connectedness = Just cp-  | otherwise =-    case cp_top cp of-      Just top ->-        case (join (cp, top), join (flipCP (cp, top))) of-          (Just _, Just _) -> Just cp-          _ -> Nothing-      _ -> Just cp-  where-    join (cp, top) =-      joinWith eqns idx (\t u -> normaliseWith (`lessThan` top) (rewrite (ok t u) (index_all idx)) t) cp--    ok t u rule sub =-      unorient rule `simplerThan` (t :=: u) &&-      reducesSkolem rule sub--    flipCP :: Symbolic a => a -> a-    flipCP t = subst sub t-      where-        n = maximum (0:map fromEnum (vars t))-        sub (V x) = var (V (n - x))---{-# INLINEABLE joinWith #-}-joinWith ::-  (Has a (Rule f), Has a (Lemma f)) =>-  Index f (Equation f) -> RuleIndex f a -> (Term f -> Term f -> Resulting f) -> CriticalPair f -> Maybe (CriticalPair f)-joinWith eqns idx reduce cp@CriticalPair{cp_eqn = lhs :=: rhs, ..}-  | subsumed eqns idx eqn = Nothing-  | otherwise =-    Just cp {-      cp_eqn = eqn,-      cp_proof =-        Proof.symm (reductionProof (reduction lred)) `Proof.trans`-        cp_proof `Proof.trans`-        reductionProof (reduction rred) }-  where-    lred = reduce lhs rhs-    rred = reduce rhs lhs-    eqn = result lred :=: result rred--{-# INLINEABLE subsumed #-}-subsumed ::-  (Has a (Rule f), Has a (Lemma f)) =>-  Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool-subsumed eqns idx (t :=: u)-  | t == u = True-  | or [ rhs rule == u | rule <- Index.lookup t (index_all idx) ] = True-  | or [ rhs rule == t | rule <- Index.lookup u (index_all idx) ] = True-    -- No need to do this symmetrically because addJoinable adds-    -- both orientations of each equation-  | or [ u == subst sub u'-       | t' :=: u' <- Index.approxMatches t eqns,-         sub <- maybeToList (match t' t) ] = True-subsumed eqns idx (App f ts :=: App g us)-  | f == g =-    let-      sub Empty Empty = False-      sub (Cons t ts) (Cons u us) =-        subsumed eqns idx (t :=: u) && sub ts us-      sub _ _ = error "Function used with multiple arities"-    in-      sub ts us-subsumed _ _ _ = False--{-# INLINEABLE groundJoin #-}-groundJoin ::-  (Function f, Has a (Rule f), Has a (Lemma f)) =>-  Config -> Index f (Equation f) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]-groundJoin config eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} =-  case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of-    ([], instances) ->-      let cps = [ subst sub cp | sub <- instances ] in-      Right (usortBy (comparing (canonicalise . order . cp_eqn)) cps)-    (model:_, _) ->-      groundJoinFrom config eqns idx model ctx cp--{-# INLINEABLE groundJoinFrom #-}-groundJoinFrom ::-  (Function f, Has a (Rule f), Has a (Lemma f)) =>-  Config -> Index f (Equation f) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]-groundJoinFrom config@Config{..} eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}-  | not cfg_ground_join ||-    (modelOK model && isJust (allSteps config eqns idx cp { cp_eqn = t' :=: u' })) = Left model-  | otherwise =-      let model1 = optimise model weakenModel (\m -> not (modelOK m) || (valid m (reduction nt) && valid m (reduction nu)))-          model2 = optimise model1 weakenModel (\m -> not (modelOK m) || isNothing (allSteps config eqns idx cp { cp_eqn = result (normaliseIn m t u) :=: result (normaliseIn m u t) }))--          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--      groundJoin config eqns idx ctx' cp-  where-    normaliseIn m t u = normaliseWith (const True) (rewrite (ok t u m) (index_all idx)) t-    ok t u m rule sub =-      reducesInModel m rule sub &&-      unorient rule `simplerThan` (t :=: u)--    nt = normaliseIn model t u-    nu = normaliseIn model u t-    t' = result nt-    u' = result nu--    -- XXX not safe to exploit the top term if we then add the equation to-    -- the joinable set. (It might then be used to join a CP with an entirely-    -- different top term.)-    modelOK _ = True-{-    modelOK m =-      case cp_top of-        Nothing -> True-        Just top ->-          isNothing (lessIn m top t) && isNothing (lessIn m top u)-}--{-# INLINEABLE groundJoinFromMaybe #-}-groundJoinFromMaybe ::-  (Function f, Has a (Rule f), Has a (Lemma f)) =>-  Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]-groundJoinFromMaybe config eqns idx Nothing = groundJoin config eqns idx-groundJoinFromMaybe config eqns idx (Just model) = groundJoinFrom config eqns idx model--{-# INLINEABLE valid #-}-valid :: Function f => Model f -> Reduction f -> Bool-valid model red =-  and [ reducesInModel model rule sub-      | Step _ rule sub <- steps red ]--optimise :: a -> (a -> [a]) -> (a -> Bool) -> a-optimise x f p =-  case filter p (f x) of-    y:_ -> optimise y f p-    _   -> x
− src/Twee/KBO.hs 
@@ -1,114 +0,0 @@-{-# LANGUAGE PatternGuards #-}-module Twee.KBO where--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 (App 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@(App f ts) u@(App 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 (App 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 (App f ts) (App g us)-  | f == g = loop ts us-  | f << g = Just Strict-  | otherwise = Nothing-  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/Label.hs 
@@ -1,111 +0,0 @@--- | Assignment of unique IDs to values.--- Inspired by the 'intern' package.--{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns #-}-module Twee.Label(Label, unsafeMkLabel, labelNum, label, find) where--import Data.IORef-import System.IO.Unsafe-import qualified Data.Map.Strict as Map-import Data.Map.Strict(Map)-import qualified Data.IntMap.Strict as IntMap-import Data.IntMap.Strict(IntMap)-import Data.Typeable-import GHC.Exts-import Unsafe.Coerce-import Data.Int--newtype Label a = Label { labelNum :: Int32 }-  deriving (Eq, Ord, Show)-unsafeMkLabel :: Int32 -> Label a-unsafeMkLabel = Label--type Cache a = Map a Int32--data Caches =-  Caches {-    caches_nextId :: {-# UNPACK #-} !Int32,-    caches_from   :: !(Map TypeRep (Cache Any)),-    caches_to     :: !(IntMap Any) }--{-# NOINLINE cachesRef #-}-cachesRef :: IORef Caches-cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty IntMap.empty))--atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a-atomicModifyCaches f = do-  -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the-  -- compare-and-swap. This causes bad things to happen when 'label'-  -- is used reentrantly (i.e. the Ord instance itself calls label).-  -- This function only lets the swap happen if caches_nextId didn't-  -- change (i.e., no new values were inserted).-  !caches <- readIORef cachesRef-  -- First compute the update.-  let !(!caches', !x) = f caches-  -- Now see if anyone else updated the cache in between-  -- (can happen if f called 'label', or in a concurrent setting).-  ok <- atomicModifyIORef' cachesRef $ \cachesNow ->-    if caches_nextId caches == caches_nextId cachesNow-    then (caches', True)-    else (cachesNow, False)-  if ok then return x else atomicModifyCaches f--toAnyCache :: Cache a -> Cache Any-toAnyCache = unsafeCoerce--fromAnyCache :: Cache Any -> Cache a-fromAnyCache = unsafeCoerce--toAny :: a -> Any-toAny = unsafeCoerce--fromAny :: Any -> a-fromAny = unsafeCoerce--{-# NOINLINE label #-}-label :: forall a. (Typeable a, Ord a) => a -> Label a-label x =-  unsafeDupablePerformIO $ do-    -- Common case: label is already there.-    caches <- readIORef cachesRef-    case tryFind caches of-      Just l -> return l-      Nothing -> do-        -- Rare case: label was not there.-        x <- atomicModifyCaches $ \caches ->-          case tryFind caches of-            Just l -> (caches, l)-            Nothing ->-              insert caches-        return x--  where-    ty = typeOf x--    tryFind :: Caches -> Maybe (Label a)-    tryFind Caches{..} =-      Label <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)--    insert :: Caches -> (Caches, Label a)-    insert caches@Caches{..} =-      if n < 0 then error "label overflow" else-      (caches {-         caches_nextId = n+1,-         caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,-         caches_to = IntMap.insert (fromIntegral n) (toAny x) caches_to },-       Label n)-      where-        n = caches_nextId-        cache =-          fromAnyCache $-          Map.findWithDefault Map.empty ty caches_from--find :: Label a -> a--- N.B. must force n before calling readIORef, otherwise a call of--- the form---   find (label x)--- doesn't work.-find (Label !n) = unsafeDupablePerformIO $ do-  Caches{..} <- readIORef cachesRef-  x <- return $! fromAny (IntMap.findWithDefault undefined (fromIntegral n) caches_to)-  return x
− src/Twee/Pretty.hs 
@@ -1,179 +0,0 @@--- | Pretty-printing of terms and assorted other values.--{-# LANGUAGE Rank2Types #-}-module Twee.Pretty(module Twee.Pretty, module Text.PrettyPrint.HughesPJClass, Pretty(..)) where--import Text.PrettyPrint.HughesPJClass hiding (empty)-import qualified Text.PrettyPrint.HughesPJClass as PP-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--pPrintEmpty :: Doc-pPrintEmpty = PP.empty--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 (V n) =-    text $-      vars !! (n `mod` length vars):-      case n `div` length vars of-        0 -> ""-        m -> show (m+1)-    where-      vars = "XYZWVUTS"--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 Pretty f => Pretty (Fun f) where-  pPrintPrec l p = pPrintPrec l p . fun_value--instance PrettyTerm f => PrettyTerm (Fun f) where-  termStyle f = termStyle (fun_value f)--instance PrettyTerm f => Pretty (Term f) where-  pPrintPrec l p (Var x) = pPrintPrec l p x-  pPrintPrec l p (App f xs) =-    pPrintTerm (termStyle f) l p (pPrint f) (termListToList xs)--instance PrettyTerm f => Pretty (TermList f) where-  pPrintPrec _ _ = pPrint . termListToList--instance 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 (pPrintTerm style l 11 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/Proof.hs 
@@ -1,660 +0,0 @@-{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables #-}-module Twee.Proof(-  Proof, Derivation(..), Lemma(..), Axiom(..),-  certify, equation, derivation,-  lemma, axiom, symm, trans, cong, simplify, congPath,-  usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,-  Config(..), defaultConfig, Presentation(..),-  ProvedGoal(..), provedGoal, checkProvedGoal,-  pPrintPresentation, present, describeEquation) where--import Twee.Base-import Twee.Equation-import Twee.Utils-import Control.Monad-import Data.Maybe-import Data.List-import Data.Ord-import qualified Data.Set as Set-import qualified Data.Map.Strict as Map--------------------------------------------------------------------------- Equational proofs. Only valid proofs can be constructed.--------------------------------------------------------------------------- A checked proof. If you have a value of type Proof f,--- it should jolly well represent a valid proof!-data Proof f =-  Proof {-    equation   :: !(Equation f),-    derivation :: !(Derivation f) }-  deriving (Eq, Show)---- A derivation is an unchecked proof. It might be wrong!--- The way to check it is to call "certify" to turn it into a Proof.-data Derivation f =-    -- Apply an existing rule (with proof!) to the root of a term-    UseLemma {-# UNPACK #-} !(Lemma f) !(Subst f)-    -- Apply an axiom to the root of a term-  | UseAxiom {-# UNPACK #-} !(Axiom f) !(Subst f)-    -- Reflexivity-  | Refl !(Term f)-    -- Symmetry-  | Symm !(Derivation f)-    -- Transivitity-  | Trans !(Derivation f) !(Derivation f)-    -- Congruence-  | Cong {-# UNPACK #-} !(Fun f) ![Derivation f]-  deriving (Eq, Show)---- A lemma, which includes a proof.-data Lemma f =-  Lemma {-    lemma_id :: {-# UNPACK #-} !Id,-    lemma_proof :: !(Proof f) }-  deriving Show---- An axiom, which comes without proof.-data Axiom f =-  Axiom {-    axiom_number :: {-# UNPACK #-} !Int,-    axiom_name :: !String,-    axiom_eqn :: !(Equation f) }-  deriving (Eq, Ord, Show)---- The trusted core of the module.--- Turns a derivation into a proof, while checking the derivation.-{-# INLINEABLE certify #-}-certify :: PrettyTerm f => Derivation f -> Proof f-certify p =-  {-# SCC certify #-}-  case check p of-    Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)-    Just eqn -> Proof eqn p-  where-    check (UseLemma Lemma{..} sub) =-      return (subst sub (equation lemma_proof))-    check (UseAxiom Axiom{..} sub) =-      return (subst sub axiom_eqn)-    check (Refl t) =-      return (t :=: t)-    check (Symm p) = do-      t :=: u <- check p-      return (u :=: t)-    check (Trans p q) = do-      t :=: u1 <- check p-      u2 :=: v <- check q-      guard (u1 == u2)-      return (t :=: v)-    check (Cong f ps) = do-      eqns <- mapM check ps-      return-        (build (app f (map eqn_lhs eqns)) :=:-         build (app f (map eqn_rhs eqns)))--------------------------------------------------------------------------- Everything below this point need not be trusted, since all proof--- construction goes through the "proof" function.--------------------------------------------------------------------------- Typeclass instances.-instance Eq (Lemma f) where-  x == y = compare x y == EQ-instance Ord (Lemma f) where-  compare =-    comparing (\x ->-      -- Don't look into lemma proofs when comparing derivations,-      -- to avoid exponential blowup-      (lemma_id x, equation (lemma_proof x)))--instance Symbolic (Derivation f) where-  type ConstantOf (Derivation f) = f-  termsDL (UseLemma _ sub) = termsDL sub-  termsDL (UseAxiom _ sub) = termsDL sub-  termsDL (Refl t) = termsDL t-  termsDL (Symm p) = termsDL p-  termsDL (Trans p q) = termsDL p `mplus` termsDL q-  termsDL (Cong _ ps) = termsDL ps--  subst_ sub (UseLemma lemma s) = UseLemma lemma (subst_ sub s)-  subst_ sub (UseAxiom axiom s) = UseAxiom axiom (subst_ sub s)-  subst_ sub (Refl t) = Refl (subst_ sub t)-  subst_ sub (Symm p) = symm (subst_ sub p)-  subst_ sub (Trans p q) = trans (subst_ sub p) (subst_ sub q)-  subst_ sub (Cong f ps) = cong f (subst_ sub ps)--instance Function f => Pretty (Proof f) where-  pPrint = pPrintLemma defaultConfig prettyShow-instance PrettyTerm f => Pretty (Derivation f) where-  pPrint (UseLemma lemma sub) =-    text "subst" <> pPrintTuple [pPrint lemma, pPrint sub]-  pPrint (UseAxiom axiom sub) =-    text "subst" <> pPrintTuple [pPrint axiom, pPrint sub]-  pPrint (Refl t) =-    text "refl" <> pPrintTuple [pPrint t]-  pPrint (Symm p) =-    text "symm" <> pPrintTuple [pPrint p]-  pPrint (Trans p q) =-    text "trans" <> pPrintTuple [pPrint p, pPrint q]-  pPrint (Cong f ps) =-    text "cong" <> pPrintTuple (pPrint f:map pPrint ps)--instance PrettyTerm f => Pretty (Axiom f) where-  pPrint Axiom{..} =-    text "axiom" <>-    pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]--instance PrettyTerm f => Pretty (Lemma f) where-  pPrint Lemma{..} =-    text "lemma" <>-    pPrintTuple [pPrint lemma_id, pPrint (equation lemma_proof)]---- Simplify a derivation.--- After simplification, a derivation has the following properties:---   * Symm is pushed down next to Step---   * Refl only occurs inside Cong or at the top level---   * Trans is right-associated and is pushed inside Cong if possible-simplify :: Minimal f => (Lemma f -> Maybe (Derivation f)) -> Derivation f -> Derivation f-simplify lem p = simp p-  where-    simp p@(UseLemma lemma sub) =-      case lem lemma of-        Nothing -> p-        Just q ->-          let-            -- Get rid of any variables that are not bound by sub-            -- (e.g., ones which only occur internally in q)-            dead = usort (vars q) \\ substDomain sub-          in simp (subst sub (erase dead q))-    simp (Symm p) = symm (simp p)-    simp (Trans p q) = trans (simp p) (simp q)-    simp (Cong f ps) = cong f (map simp ps)-    simp p = p---- Smart constructors for derivations.-lemma :: Lemma f -> Subst f -> Derivation f-lemma lem@Lemma{..} sub = UseLemma lem sub--axiom :: Axiom f -> Derivation f-axiom ax@Axiom{..} =-  UseAxiom ax $-    fromJust $-    flattenSubst [(x, build (var x)) | x <- vars axiom_eqn]--symm :: Derivation f -> Derivation f-symm (Refl t) = Refl t-symm (Symm p) = p-symm (Trans p q) = trans (symm q) (symm p)-symm (Cong f ps) = cong f (map symm ps)-symm p = Symm p--trans :: Derivation f -> Derivation f -> Derivation f-trans Refl{} p = p-trans p Refl{} = p-trans (Trans p q) r =-  -- Right-associate uses of transitivity.-  -- p cannot be a Trans (if it was created with the smart-  -- constructors) but q could be.-  Trans p (trans q r)--- Collect adjacent uses of congruence.-trans (Cong f ps) (Cong g qs) | f == g =-  transCong f ps qs-trans (Cong f ps) (Trans (Cong g qs) r) | f == g =-  trans (transCong f ps qs) r-trans p q = Trans p q--transCong :: Fun f -> [Derivation f] -> [Derivation f] -> Derivation f-transCong f ps qs =-  cong f (zipWith trans ps qs)--cong :: Fun f -> [Derivation f] -> Derivation f-cong f ps =-  case sequence (map unRefl ps) of-    Nothing -> Cong f ps-    Just ts -> Refl (build (app f ts))-  where-    unRefl (Refl t) = Just t-    unRefl _ = Nothing---- Find all lemmas which are used in a derivation.-usedLemmas :: Derivation f -> [Lemma f]-usedLemmas p = map fst (usedLemmasAndSubsts p)--usedLemmasAndSubsts :: Derivation f -> [(Lemma f, Subst f)]-usedLemmasAndSubsts p = lem p []-  where-    lem (UseLemma lemma sub) = ((lemma, sub):)-    lem (Symm p) = lem p-    lem (Trans p q) = lem p . lem q-    lem (Cong _ ps) = foldr (.) id (map lem ps)-    lem _ = id---- Find all axioms which are used in a derivation.-usedAxioms :: Derivation f -> [Axiom f]-usedAxioms p = map fst (usedAxiomsAndSubsts p)--usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]-usedAxiomsAndSubsts p = ax p []-  where-    ax (UseAxiom axiom sub) = ((axiom, sub):)-    ax (Symm p) = ax p-    ax (Trans p q) = ax p . ax q-    ax (Cong _ ps) = foldr (.) id (map ax ps)-    ax _ = id---- Applies a derivation at a particular path in a term.-congPath :: [Int] -> Term f -> Derivation f -> Derivation f-congPath [] _ p = p-congPath (n:ns) (App f t) p | n <= length ts =-  cong f $-    map Refl (take n ts) ++-    [congPath ns (ts !! n) p] ++-    map Refl (drop (n+1) ts)-  where-    ts = unpack t-congPath _ _ _ = error "bad path"--------------------------------------------------------------------------- Pretty-printing of proofs.--------------------------------------------------------------------------- Options for proof presentation.-data Config =-  Config {-    cfg_all_lemmas :: !Bool,-    cfg_no_lemmas :: !Bool,-    cfg_show_instances :: !Bool }--defaultConfig :: Config-defaultConfig =-  Config {-    cfg_all_lemmas = False,-    cfg_no_lemmas = False,-    cfg_show_instances = False }---- A proof, with all axioms and lemmas explicitly listed.-data Presentation f =-  Presentation {-    pres_axioms :: [Axiom f],-    pres_lemmas :: [Lemma f],-    pres_goals  :: [ProvedGoal f] }-  deriving Show---- Note: only the pg_proof field should be trusted!--- The remaining fields are for information only.-data ProvedGoal f =-  ProvedGoal {-    pg_number  :: Int,-    pg_name    :: String,-    pg_proof   :: Proof f,--    -- Extra fields for existentially-quantified goals, giving the original goal-    -- and the existential witness. These fields are not verified. If you want-    -- to check them, use checkProvedGoal.-    ---    -- In general, subst pg_witness_hint pg_goal_hint == equation pg_proof.-    -- For non-existential goals, pg_goal_hint == equation pg_proof-    -- and pg_witness_hint is the empty substitution.-    pg_goal_hint    :: Equation f,-    pg_witness_hint :: Subst f }-  deriving Show--provedGoal :: Int -> String -> Proof f -> ProvedGoal f-provedGoal number name proof =-  ProvedGoal {-    pg_number = number,-    pg_name = name,-    pg_proof = proof,-    pg_goal_hint = equation proof,-    pg_witness_hint = emptySubst }---- Check that pg_goal/pg_witness match up with pg_proof.-checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f-checkProvedGoal pg@ProvedGoal{..}-  | subst pg_witness_hint pg_goal_hint == equation pg_proof =-    pg-  | otherwise =-    error $ show $-      text "Invalid ProvedGoal!" $$-      text "Claims to prove" <+> pPrint pg_goal_hint $$-      text "with witness" <+> pPrint pg_witness_hint <> text "," $$-      text "but actually proves" <+> pPrint (equation pg_proof)--instance Function f => Pretty (Presentation f) where-  pPrint = pPrintPresentation defaultConfig--present :: Function f => Config -> [ProvedGoal f] -> Presentation f-present config goals =-  -- First find all the used lemmas, then hand off to presentWithGoals-  presentWithGoals config goals-    (used Set.empty (concatMap (usedLemmas . derivation . pg_proof) goals))-  where-    used lems [] = Set.elems lems-    used lems (x:xs)-      | x `Set.member` lems = used lems xs-      | otherwise =-        used (Set.insert x lems)-          (usedLemmas (derivation (lemma_proof x)) ++ xs)--presentWithGoals ::-  Function f =>-  Config -> [ProvedGoal f] -> [Lemma f] -> Presentation f-presentWithGoals config@Config{..} goals lemmas-  -- We inline a lemma if one of the following holds:-  --   * It only has one step-  --   * It is subsumed by an earlier lemma-  --   * It is only used once-  --   * It has to do with $equals (for printing of the goal proof)-  --   * The option cfg_no_lemmas is true-  -- First we compute all inlinings, then apply simplify to remove them,-  -- then repeat if any lemma was inlined-  | Map.null inlinings =-    let-      axioms = usort $-        concatMap (usedAxioms . derivation . pg_proof) goals ++-        concatMap (usedAxioms . derivation . lemma_proof) lemmas-    in-      Presentation axioms-        [ lemma { lemma_proof = flattenProof lemma_proof }-        | lemma@Lemma{..} <- lemmas ]-        [ decodeGoal (goal { pg_proof = flattenProof pg_proof })-        | goal@ProvedGoal{..} <- goals ]--  | otherwise =-    let-      inline lemma = Map.lookup lemma inlinings--      goals' =-        [ decodeGoal (goal { pg_proof = certify $ simplify inline (derivation pg_proof) })-        | goal@ProvedGoal{..} <- goals ]-      lemmas' =-        [ Lemma n (certify $ simplify inline (derivation p))-        | lemma@(Lemma n p) <- lemmas, not (lemma `Map.member` inlinings) ]-    in-      presentWithGoals config goals' lemmas'--  where-    inlinings =-      Map.fromList-        [ (lemma, p)-        | lemma <- lemmas, Just p <- [tryInline lemma]]--    tryInline (Lemma n p)-      | shouldInline n p = Just (derivation p)-    tryInline (Lemma n p)-      -- Check for subsumption by an earlier lemma-      | Just (Lemma m q) <- Map.lookup (canonicalise (t :=: u)) equations, m < n =-        Just (subsume p (derivation q))-      | Just (Lemma m q) <- Map.lookup (canonicalise (u :=: t)) equations, m < n =-        Just (subsume p (Symm (derivation q)))-      where-        t :=: u = equation p-    tryInline _ = Nothing--    shouldInline n p =-      cfg_no_lemmas ||-      oneStep (derivation p) ||-      (not cfg_all_lemmas &&-       (isJust (decodeEquality (eqn_lhs (equation p))) ||-        isJust (decodeEquality (eqn_rhs (equation p))) ||-        Map.lookup n uses == Just 1))-  -    subsume p q =-      -- Rename q so its variables match p's-      subst sub q-      where-        t  :=: u  = equation p-        t' :=: u' = equation (certify q)-        Just sub  = matchList (buildList [t', u']) (buildList [t, u])--    -- Record which lemma proves each equation-    equations =-      Map.fromList-        [ (canonicalise (equation lemma_proof), lemma)-        | lemma@Lemma{..} <- lemmas]--    -- Count how many times each lemma is used-    uses =-      Map.fromListWith (+)-        [ (lemma_id, 1)-        | Lemma{..} <--            concatMap usedLemmas-              (map (derivation . pg_proof) goals ++-               map (derivation . lemma_proof) lemmas) ]--    -- Check if a proof only has one step.-    -- Trans only occurs at the top level by this point.-    oneStep Trans{} = False-    oneStep _ = True---- Pretty-print the proof of a single lemma.-pPrintLemma :: Function f => Config -> (Id -> String) -> Proof f -> Doc-pPrintLemma Config{..} lemmaName p =-  ppTerm (eqn_lhs (equation q)) $$ pp (derivation q)-  where-    q = flattenProof p--    pp (Trans p q) = pp p $$ pp q-    pp p =-      (text "= { by" <+>-       ppStep-         (nub (map (show . ppLemma) (usedLemmasAndSubsts p)) ++-          nub (map (show . ppAxiom) (usedAxiomsAndSubsts p))) <+>-       text "}" $$-       ppTerm (eqn_rhs (equation (certify p))))--    ppTerm t = text "  " <> pPrint t--    ppStep [] = text "reflexivity" -- ??-    ppStep [x] = text x-    ppStep xs =-      hcat (punctuate (text ", ") (map text (init xs))) <+>-      text "and" <+>-      text (last xs)--    ppLemma (Lemma{..}, sub) =-      text "lemma" <+> text (lemmaName lemma_id) <> showSubst sub-    ppAxiom (Axiom{..}, sub) =-      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <> showSubst sub--    showSubst sub-      | cfg_show_instances && not (null (listSubst sub)) =-        text " with " <>-        fsep (punctuate comma-          [ pPrint x <+> text "->" <+> pPrint t-          | (x, t) <- listSubst sub ])-      | otherwise = pPrintEmpty---- Transform a proof so that each step uses exactly one axiom--- or lemma. The proof will have the following form afterwards:---   * Trans only occurs at the outermost level and is right-associated---   * Each Cong has exactly one non-Refl argument (no parallel rewriting)---   * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom---   * Refl only occurs as an argument to Cong, or outermost if the---     whole proof is a single reflexivity step-flattenProof :: Function f => Proof f -> Proof f-flattenProof =-  certify . flat . simplify (const Nothing) . derivation-  where-    flat (Trans p q) = trans (flat p) (flat q)-    flat p@(Cong f ps) =-      foldr trans (reflAfter p)-        [ Cong f $-            map reflAfter (take i ps) ++-            [p] ++-            map reflBefore (drop (i+1) ps)-        | (i, q) <- zip [0..] qs,-          p <- steps q ]-      where-        qs = map flat ps-    flat p = p--    reflBefore p = Refl (eqn_lhs (equation (certify p)))-    reflAfter p  = Refl (eqn_rhs (equation (certify p)))--    steps Refl{} = []-    steps (Trans p q) = steps p ++ steps q-    steps p = [p]--    trans (Trans p q) r = trans p (trans q r)-    trans Refl{} p = p-    trans p Refl{} = p-    trans p q = Trans p q---- Transform a derivation into a list of single steps.--- Each step has the following form:---   * Trans does not occur---   * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom---   * Each Cong has exactly one non-Refl argument (no parallel rewriting)---   * Refl only occurs as an argument to Cong-derivSteps :: Function f => Derivation f -> [Derivation f]-derivSteps = steps . derivation . flattenProof . certify-  where-    steps Refl{} = []-    steps (Trans p q) = steps p ++ steps q-    steps p = [p]--pPrintPresentation :: forall f. Function f => Config -> Presentation f -> Doc-pPrintPresentation config (Presentation axioms lemmas goals) =-  vcat $ intersperse (text "") $-    vcat [ describeEquation "Axiom" (show n) (Just name) eqn-         | Axiom n name eqn <- axioms ]:-    [ pp "Lemma" (num n) Nothing (equation p) emptySubst p-    | Lemma n p <- lemmas ] ++-    [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_witness_hint pg_proof-    | (num, ProvedGoal{..}) <- zip [1..] goals ]-  where-    pp kind n mname eqn witness p =-      describeEquation kind n mname eqn $$-      ppWitness witness $$-      text "Proof:" $$-      pPrintLemma config num p--    num x = show (fromJust (Map.lookup x nums))-    nums = Map.fromList (zip (map lemma_id lemmas) [n+1 ..])-    n = maximum $ 0:map axiom_number axioms--    ppWitness sub-      | sub == emptySubst = pPrintEmpty-      | otherwise =-          vcat [-            text "The goal is true when:",-            nest 2 $ vcat-              [ pPrint x <+> text "=" <+> pPrint t-              | (x, t) <- listSubst sub ],-            if minimal `elem` funs sub then-              text "where" <+> doubleQuotes (pPrint (minimal :: Fun f)) <+>-              text "stands for an arbitrary term of your choice."-            else pPrintEmpty,-            text ""]---- Format an equation nicely. Used both here and in the main file.-describeEquation ::-  PrettyTerm f =>-  String -> String -> Maybe String -> Equation f -> Doc-describeEquation kind num mname eqn =-  text kind <+> text num <>-  (case mname of-     Nothing -> text ""-     Just name -> text (" (" ++ name ++ ")")) <>-  text ":" <+> pPrint eqn <> text "."--------------------------------------------------------------------------- Making proofs of existential goals more readable.--------------------------------------------------------------------------- The idea: the only axioms which mention $equals, $true and $false--- are:---   * $equals(x,x) = $true  (reflexivity)---   * $equals(t,u) = $false (conjecture)--- This implies that a proof $true = $false must have the following--- structure, if we expand out all lemmas:---   $true = $equals(s,s) = ... = $equals(t,u) = $false.------ The substitution in the last step $equals(t,u) = $false is in fact the--- witness to the existential.------ Furthermore, we can make it so that the inner "..." doesn't use the $equals--- axioms. If it does, one of the "..." steps results in either $true or $false,--- and we can chop off everything before the $true or after the $false.------ Once we have done that, every proof step in the "..." must be a congruence--- step of the shape---   $equals(t, u) = $equals(v, w).--- This is because there are no other axioms which mention $equals. Hence we can--- split the proof of $equals(s,s) = $equals(t,u) into separate proofs of s=t--- and s=u.------ What we have got out is:---   * the witness to the existential---   * a proof that both sides of the conjecture are equal--- and we can present that to the user.---- Decode $equals(t,u) into an equation t=u.-decodeEquality :: Function f => Term f -> Maybe (Equation f)-decodeEquality (App equals (Cons t (Cons u Empty)))-  | equals == equalsCon = Just (t :=: u)-decodeEquality _ = Nothing---- Tries to transform a proof of $true = $false into a proof of--- the original existentially-quantified formula.-decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f-decodeGoal pg =-  case maybeDecodeGoal pg of-    Nothing -> pg-    Just (name, witness, goal, deriv) ->-      checkProvedGoal $-      pg {-        pg_name = name,-        pg_proof = certify deriv,-        pg_goal_hint = goal,-        pg_witness_hint = witness }--maybeDecodeGoal :: forall f. Function f =>-  ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)-maybeDecodeGoal ProvedGoal{..}-  -- N.B. presentWithGoals takes care of expanding any lemma which mentions-  -- $equals, and flattening the proof.-  | u == false = extract (derivSteps deriv)-    -- Orient the equation so that $false is the RHS.-  | t == false = extract (derivSteps (symm deriv))-  | otherwise = Nothing-  where-    false = build (con falseCon)-    true = build (con trueCon)-    t :=: u = equation pg_proof-    deriv = derivation pg_proof--    -- Detect $true = $equals(t, t).-    decodeReflexivity :: Derivation f -> Maybe (Term f)-    decodeReflexivity (Symm (UseAxiom Axiom{..} sub)) = do-      guard (eqn_rhs axiom_eqn == true)-      (t :=: u) <- decodeEquality (eqn_lhs axiom_eqn)-      guard (t == u)-      return (subst sub t)-    decodeReflexivity _ = Nothing--    -- Detect $equals(t, u) = $false.-    decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)-    decodeConjecture (UseAxiom Axiom{..} sub) = do-      guard (eqn_rhs axiom_eqn == false)-      eqn <- decodeEquality (eqn_lhs axiom_eqn)-      return (axiom_name, eqn, sub)-    decodeConjecture _ = Nothing--    extract (p:ps) = do-      -- Start by finding $true = $equals(t,u).-      t <- decodeReflexivity p-      cont (Refl t) (Refl t) ps-    extract [] = Nothing--    cont p1 p2 (p:ps)-      | Just t <- decodeReflexivity p =-        cont (Refl t) (Refl t) ps-      | Just (name, eqn, sub) <- decodeConjecture p =-        -- If p1: s=t and p2: s=u-        -- then symm p1 `trans` p2: t=u.-        return (name, sub, eqn, symm p1 `trans` p2)-      | Cong eq [p1', p2'] <- p, eq == equalsCon =-        cont (p1 `trans` p1') (p2 `trans` p2') ps-    cont _ _ _ = Nothing
− src/Twee/Rule.hs 
@@ -1,454 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleContexts, RecordWildCards, BangPatterns, OverloadedStrings, DeriveGeneric, MultiParamTypeClasses, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}-module Twee.Rule where--import Twee.Base-import Twee.Constraints-import qualified Twee.Index as Index-import Twee.Index(Index)-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-import GHC.Generics-import Data.Ord-import Twee.Equation-import qualified Twee.Proof as Proof-import Twee.Proof(Derivation, Lemma(..))-import Data.Tuple------------------------------------------------------------------------------------- Rewrite rules.-----------------------------------------------------------------------------------data Rule f =-  Rule {-    orientation :: !(Orientation f),-    -- Invariant:-    -- For oriented rules: vars rhs `isSubsetOf` vars lhs-    -- For unoriented rules: vars lhs == vars rhs-    lhs :: {-# UNPACK #-} !(Term f),-    rhs :: {-# UNPACK #-} !(Term f) }-  deriving (Eq, Ord, Show, Generic)-type RuleOf a = Rule (ConstantOf a)--data Orientation f =-    -- Oriented rules: used only left-to-right-    Oriented-  | WeaklyOriented {-# UNPACK #-} !(Fun f) [Term f]-    -- Unoriented rules: used bidirectionally-  | 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--weaklyOriented :: Orientation f -> Bool-weaklyOriented WeaklyOriented{} = True-weaklyOriented _ = False--instance Symbolic (Rule f) where-  type ConstantOf (Rule f) = f--instance f ~ g => Has (Rule f) (Term g) where-  the = lhs--instance Symbolic (Orientation f) where-  type ConstantOf (Orientation f) = f--  termsDL Oriented = mzero-  termsDL (WeaklyOriented _ ts) = termsDL ts-  termsDL (Permutative ts) = termsDL ts-  termsDL Unoriented = mzero--  subst_ _   Oriented = Oriented-  subst_ sub (WeaklyOriented min ts) = WeaklyOriented min (subst_ sub ts)-  subst_ sub (Permutative ts) = Permutative (subst_ sub ts)-  subst_ _   Unoriented = Unoriented--instance PrettyTerm f => Pretty (Rule f) where-  pPrint (Rule or l r) =-    pPrint l <+> text (showOrientation or) <+> pPrint r-    where-      showOrientation Oriented = "->"-      showOrientation WeaklyOriented{} = "~>"-      showOrientation Permutative{} = "<->"-      showOrientation Unoriented = "="---- Turn a rule into an equation.-unorient :: Rule f -> Equation f-unorient (Rule _ l r) = l :=: r---- Turn an equation t :=: u into a rule t -> u by computing the--- orientation info (e.g. oriented, permutative or unoriented).--- Crashes if t -> u is not a valid rule.-orient :: Function f => Equation f -> Rule f-orient (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 minimal (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 (App f ts) (App g us)-            | f == g =-              fmap concat (zipWithM makePermutative (unpack ts) (unpack us))--          aux _ _ = mzero---- Flip an unoriented rule so that it goes right-to-left.-backwards :: Rule f -> Rule f-backwards (Rule or t u) = Rule (back or) u t-  where-    back (Permutative xs) = Permutative (map swap xs)-    back Unoriented = Unoriented-    back _ = error "Can't turn oriented rule backwards"------------------------------------------------------------------------------------- Extra-fast rewriting, without proof output or unorientable rules.------------------------------------------------------------------------------------- Compute the normal form of a term wrt only oriented rules.-{-# INLINEABLE simplify #-}-simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f-simplify !idx !t = {-# SCC simplify #-} simplify1 idx t--{-# INLINEABLE simplify1 #-}-simplify1 :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f-simplify1 idx t-  | t == u = t-  | otherwise = simplify idx u-  where-    u = build (simp (singleton t))--    simp Empty = mempty-    simp (Cons (Var x) t) = var x `mappend` simp t-    simp (Cons t u)-      | Just (rule, sub) <- simpleRewrite idx t =-        Term.subst sub (rhs rule) `mappend` simp u-    simp (Cons (App f ts) us) =-      app f (simp ts) `mappend` simp us---- Check if a term can be simplified.-{-# INLINEABLE canSimplify #-}-canSimplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Bool-canSimplify idx t = canSimplifyList idx (singleton t)--{-# INLINEABLE canSimplifyList #-}-canSimplifyList :: (Function f, Has a (Rule f)) => Index f a -> TermList f -> Bool-canSimplifyList idx t =-  {-# SCC canSimplifyList #-}-  any (isJust . simpleRewrite idx) (filter isApp (subtermsList t))---- Find a simplification step that applies to a term.-{-# INLINEABLE simpleRewrite #-}-simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)-simpleRewrite idx t =-  -- Use instead of maybeToList to make fusion work-  foldr (\x _ -> Just x) Nothing $ do-    rule <- the <$> Index.approxMatches t idx-    guard (oriented (orientation rule))-    sub <- maybeToList (match (lhs rule) t)-    guard (reducesOriented rule sub)-    return (rule, sub)------------------------------------------------------------------------------------- Rewriting, with proof output.-----------------------------------------------------------------------------------type Strategy f = Term f -> [Reduction f]---- A multi-step rewrite proof t ->* u-data Reduction f =-    -- Apply a single rewrite rule to the root of a term-    Step {-# UNPACK #-} !(Lemma f) !(Rule f) !(Subst f)-    -- Reflexivity-  | Refl {-# UNPACK #-} !(Term f)-    -- Transivitity-  | Trans !(Reduction f) !(Reduction f)-    -- Congruence-  | Cong {-# UNPACK #-} !(Fun f) ![Reduction f]-  deriving Show--instance Symbolic (Reduction f) where-  type ConstantOf (Reduction f) = f-  termsDL (Step _ _ sub) = termsDL sub-  termsDL (Refl t) = termsDL t-  termsDL (Trans p q) = termsDL p `mplus` termsDL q-  termsDL (Cong _ ps) = termsDL ps--  subst_ sub (Step lemma rule s) = Step lemma rule (subst_ sub s)-  subst_ sub (Refl t) = Refl (subst_ sub t)-  subst_ sub (Trans p q) = Trans (subst_ sub p) (subst_ sub q)-  subst_ sub (Cong f ps) = Cong f (subst_ sub ps)--instance Function f => Pretty (Reduction f) where-  pPrint = pPrint . reductionProof---- Smart constructors for Trans and Cong which simplify Refl.-trans :: Reduction f -> Reduction f -> Reduction f-trans Refl{} p = p-trans p Refl{} = p--- Make right-associative to improve performance of 'result'-trans p (Trans q r) = Trans (Trans p q) r-trans p q = Trans p q--cong :: Fun f -> [Reduction f] -> Reduction f-cong f ps-  | all isRefl ps = Refl (result (reduce (Cong f ps)))-  | otherwise = Cong f ps-  where-    isRefl Refl{} = True-    isRefl _ = False---- The list of all rewrite rules used in a rewrite proof-steps :: Reduction f -> [Reduction f]-steps r = aux r []-  where-    aux step@Step{} = (step:)-    aux (Refl _) = id-    aux (Trans p q) = aux p . aux q-    aux (Cong _ ps) = foldr (.) id (map aux ps)---- Turn a reduction into a proof.-reductionProof :: Reduction f -> Derivation f-reductionProof (Step lemma _ sub) =-  Proof.lemma lemma sub-reductionProof (Refl t) = Proof.Refl t-reductionProof (Trans p q) =-  Proof.trans (reductionProof p) (reductionProof q)-reductionProof (Cong f ps) = Proof.cong f (map reductionProof ps)---- Construct a basic rewrite step.-{-# INLINE step #-}-step :: (Has a (Rule f), Has a (Lemma f)) => a -> Subst f -> Reduction f-step x sub = Step (the x) (the x) sub--------------------------------------------------------------------------- A rewrite proof with the final term attached.--- Has an Ord instance which compares the final term.-------------------------------------------------------------------------data Resulting f =-  Resulting {-    result :: {-# UNPACK #-} !(Term f),-    reduction :: !(Reduction f) }-  deriving (Show, Generic)--instance Eq (Resulting f) where x == y = compare x y == EQ-instance Ord (Resulting f) where compare = comparing result--instance Symbolic (Resulting f) where-  type ConstantOf (Resulting f) = f--instance Function f => Pretty (Resulting f) where-  pPrint = pPrint . reduction--reduce :: Reduction f -> Resulting f-reduce p =-  Resulting (res p) p-  where-    res (Trans _ q) = res q-    res (Refl t) = t-    res p = {-# SCC res_emitRes #-} build (emitResult p)--    emitResult (Step _ r sub) = Term.subst sub (rhs r)-    emitResult (Refl t) = builder t-    emitResult (Trans _ q) = emitResult q-    emitResult (Cong f ps) = app f (map emitResult ps)------------------------------------------------------------------------------------- Strategy combinators.------------------------------------------------------------------------------------- Normalise a term wrt a particular strategy.-{-# INLINE normaliseWith #-}-normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Resulting f-normaliseWith ok strat t = {-# SCC normaliseWith #-} res-  where-    res = aux 0 (Refl t) t-    aux 1000 p _ =-      error $-        "Possibly nonterminating rewrite:\n" ++ prettyShow p-    aux n p t =-      case parallel strat t of-        (q:_) | u <- result (reduce q), ok u ->-          aux (n+1) (p `trans` q) u-        _ -> Resulting t p---- Compute all normal forms of a set of terms wrt a particular strategy.-normalForms :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)-normalForms strat ps = snd (successorsAndNormalForms strat ps)---- Compute all successors of a set of terms (a successor of a term t--- is a term u such that t ->* u).-successors :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)-successors strat ps = Set.union qs rs-  where-    (qs, rs) = successorsAndNormalForms strat ps--{-# INLINEABLE successorsAndNormalForms #-}-successorsAndNormalForms :: Function f => Strategy f -> [Resulting f] ->-  (Set (Resulting f), Set (Resulting f))-successorsAndNormalForms strat ps =-  {-# SCC successorsAndNormalForms #-} go Set.empty Set.empty ps-  where-    go dead norm [] = (dead, norm)-    go dead norm (p:ps)-      | p `Set.member` dead = go dead norm ps-      | p `Set.member` norm = go dead norm ps-      | null qs = go dead (Set.insert p norm) ps-      | otherwise =-        go (Set.insert p dead) norm (qs ++ ps)-      where-        qs =-          [ reduce (reduction p `Trans` q)-          | q <- anywhere strat (result p) ]---- Apply a strategy anywhere in a term.-anywhere :: Strategy f -> Strategy f-anywhere strat t = strat t ++ nested (anywhere strat) t---- Apply a strategy to some child of the root function.-nested :: Strategy f -> Strategy f-nested _ Var{} = []-nested strat (App f ts) =-  cong f <$> inner [] ts-  where-    inner _ Empty = []-    inner before (Cons t u) =-      [ reverse before ++ [p] ++ map Refl (unpack u)-      | p <- strat t ] ++-      inner (Refl t:before) u---- Apply a strategy in parallel in as many places as possible.--- Takes only the first rewrite of each strategy.-{-# INLINE parallel #-}-parallel :: PrettyTerm f => Strategy f -> Strategy f-parallel strat t =-  case par t of-    Refl{} -> []-    p -> [p]-  where-    par t | p:_ <- strat t = p-    par (App f ts) = cong f (inner [] ts)-    par t = Refl t--    inner before Empty = reverse before-    inner before (Cons t u) = inner (par t:before) u------------------------------------------------------------------------------------- Basic strategies. These only apply at the root of the term.------------------------------------------------------------------------------------- A strategy which rewrites using an index.-{-# INLINE rewrite #-}-rewrite :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f-rewrite p rules t = do-  rule <- Index.approxMatches t rules-  tryRule p rule t---- A strategy which applies one rule only.-{-# INLINEABLE tryRule #-}-tryRule :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f-tryRule p rule t = do-  sub <- maybeToList (match (lhs (the rule)) t)-  guard (p (the rule) sub)-  return (step rule sub)---- Check if a rule can be applied, given an ordering <= on terms.-{-# INLINEABLE reducesWith #-}-reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool-reducesWith _ (Rule Oriented _ _) _ = True-reducesWith _ (Rule (WeaklyOriented min ts) _ _) sub =-  -- Be a bit careful here not to build new terms-  -- (reducesWith is used in simplify).-  -- This is the same as:-  --   any (not . isMinimal) (subst sub ts)-  any (not . isMinimal . expand) ts-  where-    expand t@(Var x) = fromMaybe t (Term.lookup x sub)-    expand t = t--    isMinimal (App f Empty) = f == min-    isMinimal _ = False-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---- Check if a rule can be applied normally.-{-# INLINEABLE reduces #-}-reduces :: Function f => Rule f -> Subst f -> Bool-reduces rule sub = reducesWith lessEq rule sub---- Check if a rule can be applied and is oriented.-{-# INLINEABLE reducesOriented #-}-reducesOriented :: Function f => Rule f -> Subst f -> Bool-reducesOriented rule sub =-  oriented (orientation rule) && reducesWith undefined rule sub---- Check if a rule can be applied in various circumstances.-{-# INLINEABLE reducesInModel #-}-reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool-reducesInModel cond rule sub =-  reducesWith (\t u -> isJust (lessIn cond t u)) rule sub--{-# INLINEABLE reducesSkolem #-}-reducesSkolem :: Function f => Rule f -> Subst f -> Bool-reducesSkolem rule sub =-  reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) rule sub-  where-    skolemise = con . skolem
− src/Twee/Rule/Index.hs 
@@ -1,45 +0,0 @@-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts #-}-module Twee.Rule.Index(-  RuleIndex(..),-  nil, insert, delete,-  approxMatches, matches, lookup) where--import Prelude hiding (lookup)-import Twee.Base hiding (lookup)-import Twee.Rule-import Twee.Index hiding (insert, delete)-import qualified Twee.Index as Index--data RuleIndex f a =-  RuleIndex {-    index_oriented :: !(Index f a),-    index_weak     :: !(Index f a),-    index_all      :: !(Index f a) }-  deriving Show--nil :: RuleIndex f a-nil = RuleIndex Nil Nil Nil--insert :: forall f a. Has a (Rule f) => Term f -> a -> RuleIndex f a -> RuleIndex f a-insert t x RuleIndex{..} =-  RuleIndex {-    index_oriented = insertWhen (oriented or) index_oriented,-    index_weak = insertWhen (weaklyOriented or) index_weak,-    index_all = insertWhen True index_all }-  where-    Rule or _ _ = the x :: Rule f--    insertWhen False idx = idx-    insertWhen True idx = Index.insert t x idx--delete :: forall f a. (Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a-delete t x RuleIndex{..} =-  RuleIndex {-    index_oriented = deleteWhen (oriented or) index_oriented,-    index_weak = deleteWhen (weaklyOriented or) index_weak,-    index_all = deleteWhen True index_all }-  where-    Rule or _ _ = the x :: Rule f--    deleteWhen False idx = idx-    deleteWhen True idx = Index.delete t x idx
− src/Twee/Task.hs 
@@ -1,52 +0,0 @@--- A module which can run housekeeping tasks every so often.-{-# LANGUAGE RecordWildCards #-}-module Twee.Task where--import System.CPUTime-import Data.IORef-import Control.Monad.IO.Class--data TaskData m a =-  Task {-    -- When was the task created?-    task_start :: !Integer,-    -- When was the task last run?-    task_last :: !Integer,-    -- How long have we spent on this task so far?-    task_spent :: !Integer,-    -- How often should we run this task at most, in seconds?-    task_frequency :: !Double,-    -- What proportion of our time should we spend on the task?-    task_budget :: !Double,-    -- The task itself-    task_what :: m a }-type Task m a = IORef (TaskData m a)---- Create a new task that should be run a certain proportion--- of the time.-newTask :: MonadIO m => Double -> Double -> m a -> m (Task m a)-newTask freq budget what = liftIO $ do-  now <- getCPUTime-  newIORef (Task now now 0 freq budget what)---- Run a task if it's time to run it.-checkTask :: MonadIO m => Task m a -> m (Maybe a)-checkTask ref = do-  task@Task{..} <- liftIO $ readIORef ref-  now <- liftIO getCPUTime-  if not (taskDue now task) then return Nothing else do-    res <- task_what-    after <- liftIO getCPUTime-    liftIO $ writeIORef ref task {-      task_last = after,-      task_spent = task_spent + (after-now) }-    return (Just res)---- Check if a task should be run now.-taskDue :: Integer -> TaskData m a -> Bool-taskDue now Task{..} =-  -- Don't run more than the frequency says.-  fromInteger (now - task_last) >= task_frequency * 10^12 &&-  -- Run if we spent less than task_budget proportion of the total time so far.-  -- Use > rather than >= so that tasks with zero budget never get run.-  fromInteger (now - task_start) * task_budget > fromInteger task_spent
− src/Twee/Term.hs 
@@ -1,544 +0,0 @@--- 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, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables #-}-module Twee.Term(-  module Twee.Term,-  -- Stuff from Twee.Term.Core.-  Term, TermList, at, lenList,-  isSubtermOfList, isVarOf,-  pattern Empty, pattern Cons, pattern ConsSym,-  pattern UnsafeCons, pattern UnsafeConsSym,-  Fun, fun, fun_id, fun_value, Var(..), pattern Var, pattern App, singleton, Builder) where--import Prelude hiding (lookup)-import Twee.Term.Core-import Data.List hiding (lookup, find)-import Data.Maybe-import Data.Monoid-import Data.IntMap.Strict(IntMap)-import qualified Data.IntMap.Strict as IntMap------------------------------------------------------------------------------------- A type class for builders.-----------------------------------------------------------------------------------class Build a where-  type BuildFun a-  builder :: a -> Builder (BuildFun a)--instance Build (Builder f) where-  type BuildFun (Builder f) = f-  builder = id--instance Build (Term f) where-  type BuildFun (Term f) = f-  builder = emitTerm--instance Build (TermList f) where-  type BuildFun (TermList f) = f-  builder = emitTermList--instance Build a => Build [a] where-  type BuildFun [a] = BuildFun a-  {-# INLINE builder #-}-  builder = mconcat . map builder--{-# INLINE build #-}-build :: Build a => a -> Term (BuildFun a)-build x =-  case buildList x of-    Cons t Empty -> t--{-# INLINE buildList #-}-buildList :: Build a => a -> TermList (BuildFun a)-buildList x = {-# SCC buildList #-} buildTermList (builder x)--{-# INLINE con #-}-con :: Fun f -> Builder f-con x = emitApp x mempty--{-# INLINE app #-}-app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)-app f ts = emitApp f (builder ts)--var :: Var -> Builder f-var = emitVar------------------------------------------------------------------------------------- Functions for substitutions.-----------------------------------------------------------------------------------{-# INLINE listSubstList #-}-listSubstList :: Subst f -> [(Var, TermList f)]-listSubstList (Subst sub) = [(V 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--{-# INLINE substDomain #-}-substDomain :: Subst f -> [Var]-substDomain (Subst sub) = map V (IntMap.keys sub)------------------------------------------------------------------------------------- Substitution.-----------------------------------------------------------------------------------class Substitution s where-  type SubstFun s-  evalSubst :: s -> Var -> Builder (SubstFun s)--  {-# INLINE substList #-}-  substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s)-  substList sub ts = aux ts-    where-      aux Empty = mempty-      aux (Cons (Var x) ts) = evalSubst sub x <> aux ts-      aux (Cons (App f ts) us) = app f (aux ts) <> aux us--instance (Build a, v ~ Var) => Substitution (v -> a) where-  type SubstFun (v -> a) = BuildFun a--  {-# INLINE evalSubst #-}-  evalSubst sub x = builder (sub x)--instance Substitution (Subst f) where-  type SubstFun (Subst f) = f--  {-# INLINE evalSubst #-}-  evalSubst sub x =-    case lookupList x sub of-      Nothing -> var x-      Just ts -> builder ts--{-# INLINE subst #-}-subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)-subst sub t = substList sub (singleton t)--newtype Subst f =-  Subst {-    unSubst :: IntMap (TermList f) }-  deriving Eq--{-# 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 x (Subst sub) = IntMap.lookup (var_id x) sub---- Add a new binding to a substitution.-{-# INLINE extendList #-}-extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)-extendList x !t (Subst sub) =-  case IntMap.lookup (var_id x) sub of-    Nothing -> Just $! Subst (IntMap.insert (var_id 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 x (Subst sub) = Subst (IntMap.delete (var_id x) sub)---- Add a new binding to a substitution.--- Overwrites any existing binding.-{-# INLINE unsafeExtendList #-}-unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f-unsafeExtendList x !t (Subst sub) = Subst (IntMap.insert (var_id x) t sub)---- Composition of substitutions.-substCompose :: Substitution s => Subst (SubstFun s) -> s -> Subst (SubstFun s)-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 App{} 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 (V 0:map boundList (t:ts))-    vars =-      buildTermList $-        mconcat [emitVar x | x <- [V 0..n]]--    loop !_ !_ !_ !_ | False = undefined-    loop sub _ Empty [] = sub-    loop sub vs Empty (t:ts) = loop sub vs t ts-    loop sub vs (ConsSym App{} 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)--{-# INLINE matchIn #-}-matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)-matchIn sub pat t = matchListIn sub (singleton pat) (singleton t)--{-# INLINE matchList #-}-matchList :: TermList f -> TermList f -> Maybe (Subst f)-matchList pat t = matchListIn emptySubst pat t--matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)-matchListIn !sub !pat !t-  | lenList t < lenList pat = Nothing-  | otherwise =-    let loop !_ !_ !_ | False = undefined-        loop sub Empty _ = Just sub-        loop _ _ Empty = undefined -- implies lenList t < lenList pat-        loop sub (ConsSym (App f _) pat) (ConsSym (App 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 {-# SCC match #-} loop sub pat t------------------------------------------------------------------------------------- Unification.-----------------------------------------------------------------------------------newtype TriangleSubst f = Triangle { unTriangle :: Subst f }-  deriving Show--instance Substitution (TriangleSubst f) where-  type SubstFun (TriangleSubst f) = f--  {-# INLINE evalSubst #-}-  evalSubst (Triangle sub) x =-    case lookupList x sub of-      Nothing  -> var x-      Just ts  -> substList (Triangle sub) ts--  -- Redefine substList to get better inlining behaviour-  {-# INLINE substList #-}-  substList (Triangle sub) ts = aux ts-    where-      aux Empty = mempty-      aux (Cons (Var x) ts) = auxVar x <> aux ts-      aux (Cons (App f ts) us) = app f (aux ts) <> aux us--      auxVar x =-        case lookupList x sub of-          Nothing -> var x-          Just ts -> aux ts--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--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 ({-# SCC unify #-} loop emptySubst t u)-  where-    loop !_ !_ !_ | False = undefined-    loop sub Empty _ = Just sub-    loop _ _ Empty = error "funny term in unification"-      -- could happen if input lists have different lengths,-      -- or a function is used with inconsistent arities-    loop sub (ConsSym (App f _) t) (ConsSym (App 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 App{} 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.-----------------------------------------------------------------------------------empty :: forall f. TermList f-empty = buildList (mempty :: Builder f)--children :: Term f -> TermList f-children t =-  case singleton t of-    UnsafeConsSym _ ts -> ts--unpack :: TermList f -> [Term f]-unpack t = unfoldr op t-  where-    op Empty = Nothing-    op (Cons t ts) = Just (t, ts)--instance Show (Term f) where-  show (Var x) = show x-  show (App f Empty) = show f-  show (App f ts) = show f ++ "(" ++ intercalate "," (map show (unpack ts)) ++ ")"--instance Show (TermList f) where-  show = show . unpack--instance Show (Subst f) where-  show subst =-    show-      [ (i, t)-      | i <- [0..substSize subst-1],-        Just t <- [lookup (V 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 -> Var-bound t = boundList (singleton t)--{-# INLINE boundList #-}-boundList :: TermList f -> Var-boundList t = aux (V 0) t-  where-    aux n Empty = n-    aux n (ConsSym App{} t) = aux n t-    aux n (ConsSym (Var x) t)-      | x >= n = aux (succ x) 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 App{} 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)--{-# 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 properSubterms #-}-properSubterms :: Term f -> [Term f]-properSubterms = subtermsList . children--isApp :: Term f -> Bool-isApp App{} = True-isApp _     = 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--isSubtermOf :: Term f -> Term f -> Bool-t `isSubtermOf` u = t `isSubtermOfList` singleton u--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 (App ff ts) us) = app (f ff) (aux ts) `mappend` aux us--{-# INLINE replacePosition #-}-replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f-replacePosition n !x = aux n-  where-    aux !_ !_ | False = undefined-    aux _ Empty = mempty-    aux 0 (Cons _ t) = builder x `mappend` builder t-    aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t-    aux n (Cons t@(App f ts) u)-      | n < len t =-        app f (aux (n-1) ts) `mappend` builder u-      | otherwise =-        builder t `mappend` aux (n-len t) u--{-# INLINE replacePositionSub #-}-replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f-replacePositionSub sub n !x = aux n-  where-    aux !_ !_ | False = undefined-    aux _ Empty = mempty-    aux n (Cons t u)-      | n < len t = inside n t `mappend` outside u-      | otherwise = outside (singleton t) `mappend` aux (n-len t) u--    inside 0 _ = outside x-    inside n (App f ts) = app f (aux (n-1) ts)-    inside _ _ = undefined -- implies n >= len t--    outside t = substList sub t---- Convert a position in a term into a path.-positionToPath :: Term f -> Int -> [Int]-positionToPath t n = term t n-  where-    term _ 0 = []-    term t n = list 0 (children t) (n-1)--    list _ Empty _ = error "bad position"-    list k (Cons t u) n-      | n < len t = k:term t n-      | otherwise = list (k+1) u (n-len t)---- Convert a path in a term into a position.-pathToPosition :: Term f -> [Int] -> Int-pathToPosition t ns = term 0 t ns-  where-    term k _ [] = k-    term k t (n:ns) = list (k+1) (children t) n ns--    list _ Empty _ _ = error "bad path"-    list k (Cons t _) 0 ns = term k t ns-    list k (Cons t u) n ns =-      list (k+len t) u (n-1) ns--pattern F :: f -> Fun f-pattern F x <- (fun_value -> x)--(<<) :: Ord f => Fun f -> Fun f -> Bool-f << g = fun_value f < fun_value g
− src/Twee/Term/Core.hs 
@@ -1,350 +0,0 @@--- Terms and substitutions, implemented using flatterms.--- This module contains all the low-level icky bits--- and provides primitives for building higher-level stuff.-{-# LANGUAGE CPP, PatternSynonyms, ViewPatterns,-    MagicHash, UnboxedTuples, BangPatterns,-    RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving #-}-module Twee.Term.Core where--import Data.Primitive(sizeOf)-#ifdef BOUNDS_CHECKS-import Data.Primitive.ByteArray.Checked-#else-import Data.Primitive.ByteArray-#endif-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-import Twee.Label-import Data.Typeable------------------------------------------------------------------------------------- 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 (F index) ++ "=" ++ show size-    | otherwise = show (V 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{..} =-  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 || lo+n >= hi = error "term index out of bounds"-  | otherwise =-    case TermList (lo+n) hi arr of-      UnsafeCons 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--- * App :: Fun f -> TermList f -> Term f--newtype Fun f = F { fun_id :: Int }-instance Eq (Fun f) where-  f == g = fun_id f == fun_id g-instance Ord (Fun f) where-  compare = comparing fun_id--fun :: (Ord f, Typeable f) => f -> Fun f-fun f = F (fromIntegral (labelNum (label f)))--fun_value :: Fun f -> f-fun_value f = find (unsafeMkLabel (fromIntegral (fun_id f)))--newtype Var = V { var_id :: Int } deriving (Eq, Ord, Enum)-instance Show (Fun f) where show f = "f" ++ show (fun_id f)-instance Show Var     where show x = "x" ++ show (var_id x)--pattern Var x <- (patTerm -> Left x)-pattern App f ts <- (patTerm -> Right (f, ts))--{-# INLINE patTerm #-}-patTerm :: Term f -> Either Var (Fun f, TermList f)-patTerm t@Term{..}-  | isFun     = Right (F index, ts)-  | otherwise = Left (V index)-  where-    Symbol{..} = toSymbol root-    !(UnsafeConsSym _ ts) = singleton t---- 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-  -- Manual worker-wrapper to prevent too much from being inlined.-  t == u = eqTermList t u--{-# INLINE eqTermList #-}-eqTermList :: TermList f -> TermList f -> Bool-eqTermList-  (TermList (I# low1) (I# high1) (ByteArray array1))-  (TermList (I# low2) (I# high2) (ByteArray array2)) =-    weqTermList low1 high1 array1 low2 high2 array2--{-# NOINLINE weqTermList #-}-weqTermList ::-  Int# -> Int# -> ByteArray# ->-  Int# -> Int# -> ByteArray# ->-  Bool-weqTermList low1 high1 array1 low2 high2 array2 =-  lenList t == lenList u && eqSameLength t u-  where-    t = TermList (I# low1) (I# high1) (ByteArray array1)-    u = TermList (I# low2) (I# high2) (ByteArray array2)-    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 f }--type Builder1 s f = 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 mbytearray# <--        newByteArray (n * sizeOf (fromSymbol undefined))-      n' <--        ST $ \s ->-          case m s mbytearray# n# 0# of-            (# s, n# #) -> (# s, I# n# #)-      if n' <= n then do-        !bytearray <- unsafeFreezeByteArray (MutableByteArray mbytearray#)-        return (TermList 0 n' bytearray)-       else loop (n'*2)-  loop 32--{-# INLINE getByteArray #-}-getByteArray :: (MutableByteArray s -> Builder1 s f) -> Builder1 s f-getByteArray k = \s bytearray n i -> k (MutableByteArray bytearray) s bytearray n i--{-# INLINE getSize #-}-getSize :: (Int -> Builder1 s f) -> Builder1 s f-getSize k = \s bytearray n i -> k (I# n) s bytearray n i--{-# INLINE getIndex #-}-getIndex :: (Int -> Builder1 s f) -> Builder1 s f-getIndex k = \s bytearray n i -> k (I# i) s bytearray n i--{-# INLINE putIndex #-}-putIndex :: Int -> Builder1 s f-putIndex (I# i) = \s _ _ _ -> (# s, i #)--{-# INLINE liftST #-}-liftST :: ST s () -> Builder1 s f-liftST (ST m) =-  \s _ _ i ->-  case m s of-    (# s, () #) -> (# s, i #)--{-# INLINE built #-}-built :: Builder1 s f-built = \s _ _ i -> (# s, i #)--{-# INLINE then_ #-}-then_ :: Builder1 s f -> Builder1 s f -> Builder1 s f-then_ m1 m2 =-  \s bytearray n i ->-    case m1 s bytearray n i of-      (# s, i #) -> m2 s bytearray n i--{-# INLINE checked #-}-checked :: Int -> Builder1 s f -> Builder1 s f-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 $-    getByteArray $ \bytearray ->-    getIndex $ \n ->-    putIndex (n+1) `then_`-    unBuilder inner `then_`-    getIndex (\m ->-      liftST $ writeByteArray bytearray n (fromSymbol x { size = m - n }))---- Emit a function application.-{-# INLINE emitApp #-}-emitApp :: Fun f -> Builder f -> Builder f-emitApp (F n) inner = emitSymbolBuilder (Symbol True n 0) inner---- Emit a variable.-{-# INLINE emitVar #-}-emitVar :: Var -> Builder f-emitVar x = emitSymbolBuilder (Symbol False (var_id x) 1) mempty---- Emit a whole termlist.-{-# INLINE emitTermList #-}-emitTermList :: TermList f -> Builder f-emitTermList (TermList lo hi array) =-  Builder $ checked (hi-lo) $-    getByteArray $ \mbytearray ->-    getIndex $ \n ->-    let k = sizeOf (fromSymbol undefined) in-    liftST (copyByteArray mbytearray (n*k) array (lo*k) ((hi-lo)*k)) `then_`-    putIndex (n + hi-lo)--------------------------------------------------------------------------- Efficient subterm testing.-------------------------------------------------------------------------{-# INLINE isSubtermOfList #-}-isSubtermOfList :: Term f -> TermList f -> Bool-isSubtermOfList t u =-  isSubArrayOf (singleton t) u---- N.B. this one should not be exported from Twee.Term--- because subarray is not the same as subterm if t is not--- a singleton-isSubArrayOf :: TermList f -> TermList f -> Bool-isSubArrayOf t u =-  lenList t <= lenList u && (here t u || next t u)-  where-    here Empty _ = True-    here (ConsSym s1 t) (UnsafeConsSym s2 u) =-      root s1 == root s2 && here t u--    -- This is safe because lenList t <= lenList u-    -- so if u = Empty, then t = Empty and here t u = True.-    next t (UnsafeConsSym _ u) = isSubArrayOf t u--{-# INLINE isVarOf #-}-isVarOf :: Var -> TermList f -> Bool-isVarOf (V x) t = isSymbolOf (fromSymbol (Symbol False x 1)) t--isSymbolOf :: Int64 -> TermList f -> Bool-isSymbolOf !_ Empty = False-isSymbolOf n (ConsSym t ts) = root t == n || isSymbolOf n ts
− src/Twee/Utils.hs 
@@ -1,145 +0,0 @@--- | Miscellaneous utility functions.--{-# LANGUAGE CPP, MagicHash #-}-module Twee.Utils where--import Control.Arrow((&&&))-import Control.Exception-import Data.List(groupBy, sortBy)-import Data.Ord(comparing)-import System.IO-import GHC.Prim-import GHC.Types-import Data.Bits---import Test.QuickCheck hiding ((.&.))--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--{-# INLINE fixpoint #-}-fixpoint :: Eq a => (a -> a) -> a -> a-fixpoint f x = fxp x-  where-    fxp x-      | x == y = x-      | otherwise = fxp y-      where-        y = f x---- From "Bit twiddling hacks": branchless min and max-{-# INLINE intMin #-}-intMin :: Int -> Int -> Int-intMin x y =-  y `xor` ((x `xor` y) .&. negate (x .<. y))-  where-    I# x .<. I# y = I# (x <# y)--{-# INLINE intMax #-}-intMax :: Int -> Int -> Int-intMax x y =-  x `xor` ((x `xor` y) .&. negate (x .<. y))-  where-    I# x .<. I# y = I# (x <# y)---- Split an interval (inclusive bounds) into a particular number of blocks-splitInterval :: Integral a => a -> (a, a) -> [(a, a)]-splitInterval k (lo, hi) =-  [ (lo+i*blockSize, (lo+(i+1)*blockSize-1) `min` hi)-  | i <- [0..k-1] ]-  where-    size = (hi-lo+1)-    blockSize = (size + k - 1) `div` k -- division rounding up-{--prop_split_1 (Positive k) (lo, hi) =-  -- Check that all elements occur exactly once-  concat [[x..y] | (x, y) <- splitInterval k (lo, hi)] === [lo..hi]---- Check that we have the correct number and distribution of blocks-prop_split_2 (Positive k) (lo, hi) =-  counterexample (show splits) $ conjoin-    [counterexample "Reason: too many splits" $-       length splits <= k,-     counterexample "Reason: too few splits" $-       length [lo..hi] >= k ==> length splits == k,-     counterexample "Reason: uneven distribution" $-      not (null splits) ==>-       minimum (map length splits) + 1 >= maximum (map length splits)]-  where-    splits = splitInterval k (lo, hi)--}
− tests/BOO067-1.p 
@@ -1,32 +0,0 @@-%---------------------------------------------------------------------------% File     : BOO067-1 : TPTP v6.3.0. Released v2.6.0.-% Domain   : Boolean Algebra (Ternary)-% Problem  : Ternary Boolean Algebra Single axiom is complete, part 1-% Version  : [MP96] (equality) axioms.-% English  :--% Refs     : [McC98] McCune (1998), Email to G. Sutcliffe-%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq-% Source   : [TPTP]-% Names    :--% Status   : Unsatisfiable-% Rating   : 0.42 v6.3.0, 0.35 v6.2.0, 0.29 v6.1.0, 0.31 v6.0.0, 0.48 v5.5.0, 0.47 v5.4.0, 0.33 v5.3.0, 0.25 v5.2.0, 0.29 v5.1.0, 0.33 v5.0.0, 0.29 v4.1.0, 0.18 v4.0.1, 0.36 v4.0.0, 0.38 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.21 v3.1.0, 0.33 v2.7.0, 0.27 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    :    7 (   5 constant; 0-3 arity)-%            Number of variables   :    7 (   0 singleton)-%            Maximal term depth    :    5 (   3 average)-% SPC      : CNF_UNS_RFO_PEQ_UEQ--% Comments : A UEQ part of BOO035-1-%---------------------------------------------------------------------------cnf(single_axiom,axiom,-    ( multiply(multiply(A,inverse(A),B),inverse(multiply(multiply(C,D,E),F,multiply(C,D,G))),multiply(D,multiply(G,F,E),C)) = B )).--cnf(prove_tba_axioms_1,negated_conjecture,-    (  multiply(multiply(d,e,a),b,multiply(d,e,c)) != multiply(d,e,multiply(a,b,c)) )).--%--------------------------------------------------------------------------
− tests/LAT072-1.p 
@@ -1,37 +0,0 @@-%---------------------------------------------------------------------------% File     : LAT072-1 : TPTP v6.3.0. Released v2.6.0.-% Domain   : Lattice Theory (Ortholattices)-% Problem  : Given single axiom OML-23A, prove associativity-% Version  : [MRV03] (equality) axioms.-% English  : Given a single axiom candidate OML-23A 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-23A-associativity [MRV03]--% Status   : Unsatisfiable-% Rating   : 0.95 v6.3.0, 0.94 v6.2.0, 0.93 v6.1.0, 0.94 v6.0.0, 0.95 v5.4.0, 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    :    7 (   4 average)-% SPC      : CNF_UNS_RFO_PEQ_UEQ--% Comments :-%---------------------------------------------------------------------------%----Single axiom OML-23A-cnf(oml_23A,axiom,-    ( f(f(f(f(B,A),f(A,C)),D),f(A,f(f(C,f(f(A,A),C)),C))) = A )).--cnf(a, axiom, f(X,Y) = f(Y, X)).--%----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/ROB010-1.p 
@@ -1,11 +0,0 @@-cnf(condition,hypothesis,-    ( negate(add(a,negate(b))) = c )).--cnf(prove_result,negated_conjecture,-    (  negate(add(c,negate(add(b,a)))) != a )).--cnf(commutativity_of_add,axiom,-    ( add(X,Y) = add(Y,X) )).--cnf(robbins_axiom,axiom,-    ( negate(add(negate(add(X,Y)),negate(add(X,negate(Y))))) = X )).
− tests/append-rev.p 
@@ -1,4 +0,0 @@-cnf(rev_rev, axiom, rev(rev(X)) = X).-cnf(app_assoc, axiom, '++'(X,'++'(Y,Z)) = '++'('++'(X,Y),Z)).-cnf(rev_app, axiom, '++'(rev(X),rev(Y)) = rev('++'(Y,X))).-cnf(conjecture, negated_conjecture, '++'(a,rev(b)) != rev('++'(b, rev(a)))).
− tests/db.p 
@@ -1,17 +0,0 @@-% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf-% appendix b. theorem 3.4, clause 8.-cnf(a, axiom, '^'(X, Y) = '^'(Y, X)).-cnf(a, axiom, '^'(X, '^'(Y, Z)) = '^'(Y, '^'(X, Z))).-cnf(a, axiom, '^'('^'(X, Y), Z) = '^'(X, '^'(Y, Z))).-cnf(a, axiom, v(X, Y) = v(Y, X)).-cnf(a, axiom, v(X, v(Y, Z)) = v(Y, v(X, Z))).-cnf(a, axiom, v(v(X, Y), Z) = v(X, v(Y, Z))).-cnf(a, axiom, v(X, '^'(X, Y)) = X).-cnf(a, axiom, '^'(X, v(X, Y)) = X).-cnf(a, axiom, upme(X,Y,Z) = '^'(X, v(Y, Z))).-cnf(a, axiom, lome(X,Y,Z) = v('^'(X, Y), '^'(X, Z))).-cnf(a, axiom, upjo(X,Y,Z) = '^'(v(X, Y), v(X, Z))).-cnf(a, axiom, lojo(X,Y,Z) = v(X, '^'(Y, Z))).-cnf(a, axiom, v(upme('^'(a, X1),Y1,Z1), '^'(Y1, Z1)) = '^'(v('^'('^'(a, X1), Y1), Z1), v('^'('^'(a, X1), Z1), Y1))).-cnf(a, axiom, upme(X,Y,Z) = v(upme(X,Y,'^'(a, Z)), upme(X,Z,'^'(a, Y)))).-fof(a, conjecture, (upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2))).
− tests/diff.p 
@@ -1,4 +0,0 @@-cnf('x\\(y\\x)=x', axiom, '\\'(X, '\\'(Y, X)) = X).-cnf('x\\(x\\y)=y\\(y\\x)', axiom, '\\'(X, '\\'(X, Y)) = '\\'(Y, '\\'(Y, X))).-cnf('(x\\y)\\z=(x\\z)\\(y\\z)', axiom, '\\'('\\'(X, Y), Z) = '\\'('\\'(X, Z), '\\'(Y, Z))).-cnf(conjecture, negated_conjecture, '\\'('\\'(a, c), b) != '\\'('\\'(a, b), c)).
− tests/lat.p 
@@ -1,16 +0,0 @@-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, negated_conjecture,-    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 
@@ -1,7 +0,0 @@-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, negated_conjecture, x!=y).
− tests/loop.p 
@@ -1,6 +0,0 @@-cnf(mult_ld, axiom, '*'(X, '^'(X, Y)) = Y).-cnf(ld_mult, axiom, '^'(X, '*'(X, Y)) = Y).-cnf(mult_rd, axiom, '*'('/'(X, Y), Y) = X).-cnf(rd_mult, axiom, '/'('*'(X, Y), Y) = X).-cnf(moufang, axiom, '*'(X, '*'(Y, '*'(X, Z))) = '*'('*'('*'(X, Y), X), Z)).-cnf(conjecture, negated_conjecture, '^'(a,a) != '/'(a,a)).
− tests/loop2.p 
@@ -1,6 +0,0 @@-cnf('*-\\', axiom, '*'(X, '\\'(X, Y)) = Y).-cnf('\\-*', axiom, '\\'(X, '*'(X, Y)) = Y).-cnf('*-/', axiom, '*'('/'(X, Y), Y) = X).-cnf('/-*', axiom, '/'('*'(X, Y), Y) = X).-cnf(moufang, axiom, '*'(X, '*'(Y, '*'(X, Z))) = '*'('*'('*'(X, Y), X), Z)).-cnf(conjecture, negated_conjecture, '*'(a,'/'(b,b)) != a).
− tests/lukasiewicz.p 
@@ -1,6 +0,0 @@-cnf(imp_true, axiom, implies(true, X) = X).-cnf(imp_compose, axiom, implies(implies(X, Y), implies(implies(Y, Z), implies(X, Z))) = true).-cnf(imp_not, axiom, implies(implies(not(X), not(Y)), implies(Y, X)) = true).-cnf(imp_switch, axiom, implies(implies(X, Y), Y) = implies(implies(Y, X), X)).-cnf(or_def, axiom, or(X, Y) = implies(not(X), Y)).-cnf(conjecture, negated_conjecture, or(a,or(b,c)) != or(or(a,b),c)).
− tests/nand.p 
@@ -1,37 +0,0 @@-%---------------------------------------------------------------------------% 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 
@@ -1,18 +0,0 @@-cnf(plus_comm, axiom, plus(X, Y) = plus(Y, X)).-cnf(plus_assoc, axiom, plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)).-cnf(times_comm, axiom, times(X, Y) = times(Y, X)).-cnf(times_assoc, axiom, times(X, times(Y, Z)) = times(times(X, Y), Z)).-cnf(plus_zero, axiom, plus(X, zero) = X).-cnf(times_zero, axiom, times(X, zero) = zero).-cnf(times_one, axiom, times(X, one) = X).-cnf(distr, axiom, times(X, plus(Y, Z)) = plus(times(X, Y), times(X, Z))).-cnf(distr, axiom, times(plus(X, Y), Z) = plus(times(X, Z), times(Y, Z))).-cnf(plus_s, axiom, plus(s(X), Y) = s(plus(X, Y))).-cnf(times_s, axiom, times(s(X), Y) = plus(Y, times(X, Y))).-cnf(sum_zero, axiom, sum(zero) = zero).-cnf(sum_s, axiom, sum(s(N)) = plus(s(N), sum(N))).-cnf(cubes_zero, axiom, cubes(zero) = zero).-cnf(cubes_s, axiom, cubes(s(N)) = plus(times(s(N), times(s(N), s(N))), cubes(N))).-cnf(plus_sum, axiom, plus(sum(N), sum(N)) = times(N, s(N))).-cnf(ih, axiom, times(sum(a), sum(a)) = cubes(a)).-cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a))) != cubes(s(a))).
− tests/ring.p 
@@ -1,9 +0,0 @@-cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(plus_zero, axiom, '+'('0', X) = X).-cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0').-cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).-cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))).-cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))).-cnf(cube, axiom, X = '*'(X, '*'(X, X))).-cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
− tests/ring2.p 
@@ -1,9 +0,0 @@-cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(plus_zero, axiom, '+'('0', X) = X).-cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0').-cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).-cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))).-cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))).-cnf(power_six, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, '*'(X, X)))))).-cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
− tests/ring3.p 
@@ -1,9 +0,0 @@-cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(plus_zero, axiom, '+'('0', X) = X).-cnf(plus_neg, axiom, '+'(X, '-'(X)) = '0').-cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).-cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))).-cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))).-cnf(power_four, axiom, X = '*'(X, '*'(X, '*'(X, X)))).-cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
− tests/ring4.p 
@@ -1,9 +0,0 @@-cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(plus_zero, axiom, '+'('0', X) = X).-cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0').-cnf(times_ssoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).-cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))).-cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))).-cnf(power_five, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, X))))).-cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
− tests/robbins-easy.p 
@@ -1,4 +0,0 @@-cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(funny, axiom, '+'('-'('+'('-'(X), Y)), '-'('+'('-'(X), '-'(Y)))) = X).-cnf(conjecture, negated_conjecture, '-'('+'('-'('+'(a, b)), '-'('+'(a, '-'(b))))) != a).
− tests/robbins.p 
@@ -1,4 +0,0 @@-cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X).-cnf(conjecture, negated_conjecture, '-'('-'(a)) != a).
− tests/semigroup.p 
@@ -1,4 +0,0 @@-cnf(assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).-cnf(two_three, axiom, '*'(X, X) = '*'(X, '*'(X, X))).-cnf(twiddle, axiom, '*'('*'(X, X), Y) = '*'(Y, '*'(X, X))).-cnf(conjecture, negated_conjecture, '*'('*'(a, b), '*'(a, b)) != '*'('*'(a, a), '*'(b, b))).
− tests/semigroup2.p 
@@ -1,26 +0,0 @@-% File     : GRP196-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 (1998), Email to G. Sutcliffe-%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq-%          : [McC95] McCune (1995), Four Challenge Problems in Equational L-% Source   : [McC98]-% Names    : CS-3 [MP96]-%          : Problem B [McC95]-% Status   : Unsatisfiable-% Rating   : 1.00 v4.0.1, 0.93 v4.0.0, 0.92 v3.7.0, 0.89 v3.4.0, 1.00 v3.3.0, 0.93 v3.1.0, 1.00 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    :   18 (   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(assoc, axiom, '*'('*'(A,B),C)='*'(A,'*'(B,C))).-cnf(twiddle, axiom, '*'(A,'*'(B,'*'(B,B)))='*'(B,'*'(B,'*'(B,A)))).-cnf(conjecture, negated_conjecture, '*'(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 
@@ -1,6 +0,0 @@-% Needs case split on X < c.-cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(idem, axiom, '+'(X, X) = X).-cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X).-cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a).
− tests/winkler.p 
@@ -1,6 +0,0 @@-% Needs case split on X < c.-cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(idem_c, axiom, '+'(c, c) = c).-cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X).-cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a).
− tests/winkler2.p 
@@ -1,6 +0,0 @@-% Needs case split on X < c.-cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)).-cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).-cnf(plus_c_d, axiom, '+'(c, d) = c).-cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X).-cnf(conjecture, negated_conjecture, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a).
− tests/y.p 
@@ -1,3 +0,0 @@-fof(k_def, axiom, ![X, Y]: '@'('@'(k, X), Y) = X).-fof(s_def, axiom, ![X, Y, Z]: '@'('@'('@'(s, X), Y), Z) = '@'('@'(X, Z), '@'(Y, Z))).-fof(conjecture, conjecture, ?[Y]: ![F]: '@'(Y, F) = '@'(F, '@'(Y, F))).
twee.cabal view
@@ -1,5 +1,5 @@ name:                twee-version:             2.0+version:             2.1 synopsis:            An equational theorem prover homepage:            http://github.com/nick8325/twee license:             BSD3@@ -9,7 +9,7 @@ category:            Theorem Provers build-type:          Simple cabal-version:       >=1.10-extra-source-files:  README tests/*.p+extra-source-files:  misc/static-libstdc++ description:    Twee is an experimental equational theorem prover based on    Knuth-Bendix completion.@@ -40,63 +40,15 @@   description: Build using LLVM backend for faster code.   default: False -flag bounds-checks-  description: Use bounds checks for all array operations.-  default: False--library-  exposed-modules:-    Twee-    Twee.Array-    Twee.Base-    Twee.ChurchList-    Twee.Constraints-    Twee.CP-    Twee.Equation-    Twee.Heap-    Twee.Index-    Twee.Index.Lookup-    Twee.Join-    Twee.KBO-    Twee.Label-    Twee.Pretty-    Twee.Proof-    Twee.Rule-    Twee.Rule.Index-    Twee.Term-    Twee.Term.Core-    Twee.Task-    Twee.Utils-  build-depends:-    base >= 4 && < 5,-    containers,-    transformers,-    dlist,-    pretty,-    ghc-prim,-    primitive >= 0.6.2.0-  hs-source-dirs:      src-  ghc-options:         -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100-  default-language:    Haskell2010--  if flag(llvm)-    ghc-options: -fllvm-  if flag(bounds-checks)-    cpp-options: -DBOUNDS_CHECKS-    exposed-modules:-      Data.Primitive.SmallArray.Checked-      Data.Primitive.ByteArray.Checked-      Data.Primitive.Checked- executable twee-  main-is:             executable/Main.hs+  main-is:             Main.hs   default-language:    Haskell2010-  build-depends:       base,-                       twee,+  build-depends:       base < 5,+                       twee-lib == 2.1,                        containers,                        pretty,                        split,-                       jukebox >= 0.3+                       jukebox >= 0.3.2   ghc-options:         -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100    if flag(llvm)