diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2015, Nick Smallbone +Copyright (c) 2015-2017, Nick Smallbone All rights reserved. diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -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 "" "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 "" "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 diff --git a/README b/README deleted file mode 100644 --- a/README +++ /dev/null @@ -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! diff --git a/executable/Main.hs b/executable/Main.hs deleted file mode 100644 --- a/executable/Main.hs +++ /dev/null @@ -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 "" "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 "" "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)) diff --git a/misc/static-libstdc++ b/misc/static-libstdc++ new file mode 100644 --- /dev/null +++ b/misc/static-libstdc++ @@ -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 diff --git a/src/Data/Primitive/ByteArray/Checked.hs b/src/Data/Primitive/ByteArray/Checked.hs deleted file mode 100644 --- a/src/Data/Primitive/ByteArray/Checked.hs +++ /dev/null @@ -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 diff --git a/src/Data/Primitive/Checked.hs b/src/Data/Primitive/Checked.hs deleted file mode 100644 --- a/src/Data/Primitive/Checked.hs +++ /dev/null @@ -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 - diff --git a/src/Data/Primitive/SmallArray/Checked.hs b/src/Data/Primitive/SmallArray/Checked.hs deleted file mode 100644 --- a/src/Data/Primitive/SmallArray/Checked.hs +++ /dev/null @@ -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 diff --git a/src/Twee.hs b/src/Twee.hs deleted file mode 100644 --- a/src/Twee.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Array.hs b/src/Twee/Array.hs deleted file mode 100644 --- a/src/Twee/Array.hs +++ /dev/null @@ -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') diff --git a/src/Twee/Base.hs b/src/Twee/Base.hs deleted file mode 100644 --- a/src/Twee/Base.hs +++ /dev/null @@ -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 diff --git a/src/Twee/CP.hs b/src/Twee/CP.hs deleted file mode 100644 --- a/src/Twee/CP.hs +++ /dev/null @@ -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 diff --git a/src/Twee/ChurchList.hs b/src/Twee/ChurchList.hs deleted file mode 100644 --- a/src/Twee/ChurchList.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Constraints.hs b/src/Twee/Constraints.hs deleted file mode 100644 --- a/src/Twee/Constraints.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Equation.hs b/src/Twee/Equation.hs deleted file mode 100644 --- a/src/Twee/Equation.hs +++ /dev/null @@ -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) diff --git a/src/Twee/Heap.hs b/src/Twee/Heap.hs deleted file mode 100644 --- a/src/Twee/Heap.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Index.hs b/src/Twee/Index.hs deleted file mode 100644 --- a/src/Twee/Index.hs +++ /dev/null @@ -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)) diff --git a/src/Twee/Index/Lookup.hs b/src/Twee/Index/Lookup.hs deleted file mode 100644 --- a/src/Twee/Index/Lookup.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Join.hs b/src/Twee/Join.hs deleted file mode 100644 --- a/src/Twee/Join.hs +++ /dev/null @@ -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 diff --git a/src/Twee/KBO.hs b/src/Twee/KBO.hs deleted file mode 100644 --- a/src/Twee/KBO.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Label.hs b/src/Twee/Label.hs deleted file mode 100644 --- a/src/Twee/Label.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Pretty.hs b/src/Twee/Pretty.hs deleted file mode 100644 --- a/src/Twee/Pretty.hs +++ /dev/null @@ -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))) diff --git a/src/Twee/Proof.hs b/src/Twee/Proof.hs deleted file mode 100644 --- a/src/Twee/Proof.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Rule.hs b/src/Twee/Rule.hs deleted file mode 100644 --- a/src/Twee/Rule.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Rule/Index.hs b/src/Twee/Rule/Index.hs deleted file mode 100644 --- a/src/Twee/Rule/Index.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Task.hs b/src/Twee/Task.hs deleted file mode 100644 --- a/src/Twee/Task.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Term.hs b/src/Twee/Term.hs deleted file mode 100644 --- a/src/Twee/Term.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Term/Core.hs b/src/Twee/Term/Core.hs deleted file mode 100644 --- a/src/Twee/Term/Core.hs +++ /dev/null @@ -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 diff --git a/src/Twee/Utils.hs b/src/Twee/Utils.hs deleted file mode 100644 --- a/src/Twee/Utils.hs +++ /dev/null @@ -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) --} diff --git a/tests/BOO067-1.p b/tests/BOO067-1.p deleted file mode 100644 --- a/tests/BOO067-1.p +++ /dev/null @@ -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)) )). - -%-------------------------------------------------------------------------- diff --git a/tests/LAT072-1.p b/tests/LAT072-1.p deleted file mode 100644 --- a/tests/LAT072-1.p +++ /dev/null @@ -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))) )). - -%-------------------------------------------------------------------------- diff --git a/tests/ROB010-1.p b/tests/ROB010-1.p deleted file mode 100644 --- a/tests/ROB010-1.p +++ /dev/null @@ -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 )). diff --git a/tests/append-rev.p b/tests/append-rev.p deleted file mode 100644 --- a/tests/append-rev.p +++ /dev/null @@ -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)))). diff --git a/tests/db.p b/tests/db.p deleted file mode 100644 --- a/tests/db.p +++ /dev/null @@ -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))). diff --git a/tests/diff.p b/tests/diff.p deleted file mode 100644 --- a/tests/diff.p +++ /dev/null @@ -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)). diff --git a/tests/lat.p b/tests/lat.p deleted file mode 100644 --- a/tests/lat.p +++ /dev/null @@ -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))))))). diff --git a/tests/lcl.p b/tests/lcl.p deleted file mode 100644 --- a/tests/lcl.p +++ /dev/null @@ -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). diff --git a/tests/loop.p b/tests/loop.p deleted file mode 100644 --- a/tests/loop.p +++ /dev/null @@ -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)). diff --git a/tests/loop2.p b/tests/loop2.p deleted file mode 100644 --- a/tests/loop2.p +++ /dev/null @@ -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). diff --git a/tests/lukasiewicz.p b/tests/lukasiewicz.p deleted file mode 100644 --- a/tests/lukasiewicz.p +++ /dev/null @@ -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)). diff --git a/tests/nand.p b/tests/nand.p deleted file mode 100644 --- a/tests/nand.p +++ /dev/null @@ -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))) )). - -%-------------------------------------------------------------------------- diff --git a/tests/nicomachus.p b/tests/nicomachus.p deleted file mode 100644 --- a/tests/nicomachus.p +++ /dev/null @@ -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))). diff --git a/tests/ring.p b/tests/ring.p deleted file mode 100644 --- a/tests/ring.p +++ /dev/null @@ -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)). diff --git a/tests/ring2.p b/tests/ring2.p deleted file mode 100644 --- a/tests/ring2.p +++ /dev/null @@ -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)). diff --git a/tests/ring3.p b/tests/ring3.p deleted file mode 100644 --- a/tests/ring3.p +++ /dev/null @@ -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)). diff --git a/tests/ring4.p b/tests/ring4.p deleted file mode 100644 --- a/tests/ring4.p +++ /dev/null @@ -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)). diff --git a/tests/robbins-easy.p b/tests/robbins-easy.p deleted file mode 100644 --- a/tests/robbins-easy.p +++ /dev/null @@ -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). diff --git a/tests/robbins.p b/tests/robbins.p deleted file mode 100644 --- a/tests/robbins.p +++ /dev/null @@ -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). diff --git a/tests/semigroup.p b/tests/semigroup.p deleted file mode 100644 --- a/tests/semigroup.p +++ /dev/null @@ -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))). diff --git a/tests/semigroup2.p b/tests/semigroup2.p deleted file mode 100644 --- a/tests/semigroup2.p +++ /dev/null @@ -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)))))))))))))))))). diff --git a/tests/winkler-easy.p b/tests/winkler-easy.p deleted file mode 100644 --- a/tests/winkler-easy.p +++ /dev/null @@ -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). diff --git a/tests/winkler.p b/tests/winkler.p deleted file mode 100644 --- a/tests/winkler.p +++ /dev/null @@ -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). diff --git a/tests/winkler2.p b/tests/winkler2.p deleted file mode 100644 --- a/tests/winkler2.p +++ /dev/null @@ -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). diff --git a/tests/y.p b/tests/y.p deleted file mode 100644 --- a/tests/y.p +++ /dev/null @@ -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))). diff --git a/twee.cabal b/twee.cabal --- a/twee.cabal +++ b/twee.cabal @@ -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)