-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | An equational theorem prover
--
-- Twee is an experimental equational theorem prover based on
-- Knuth-Bendix completion.
--
-- Given a set of equational axioms and a set of equational conjectures
-- it will try to prove the conjectures. It will terminate if the
-- conjectures are true but normally fail to terminate if they are false.
--
-- The input problem should be in TPTP format (see http://www.tptp.org).
-- You can use types and quantifiers, but apart from that the problem
-- must be equational.
--
-- This package contains only the library part of twee.
@package twee-lib
@version 2.4
-- | Assignment of unique IDs to values. Inspired by the intern
-- package.
module Data.Label
-- | A value of type a which has been given a unique ID.
data Label a
-- | Construct a Label a from its unique ID, which must be
-- the labelNum of an already existing Label. Extremely
-- unsafe!
unsafeMkLabel :: Int32 -> Label a
-- | The unique ID of a label.
labelNum :: Label a -> Int32
-- | Assign a label to a value.
label :: forall a. (Typeable a, Ord a) => a -> Label a
-- | Recover the underlying value from a label.
find :: Label a -> a
instance GHC.Show.Show (Data.Label.Label a)
instance GHC.Classes.Ord (Data.Label.Label a)
instance GHC.Classes.Eq (Data.Label.Label a)
module Twee.Profile
stamp :: symbol -> a -> a
stampWith :: symbol -> (a -> b) -> a -> a
stampM :: MonadIO m => symbol -> m a -> m a
profile :: IO ()
-- | A module which can run housekeeping tasks every so often.
module Twee.Task
-- | A task which runs in the monad m and produces a value of type
-- a.
data Task m a
-- | Create a new task that should be run a certain proportion of the time.
-- The first argument is how often in seconds the task should run, at
-- most. The second argument is the maximum percentage of time that
-- should be spent on the task.
newTask :: MonadIO m => Double -> Double -> m a -> m (Task m a)
-- | Run a task if it's time to run it.
checkTask :: MonadIO m => Task m a -> m (Maybe a)
-- | Miscellaneous utility functions.
module Twee.Utils
repeatM :: Monad m => m a -> m [a]
partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]
collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)]
isSorted :: Ord a => [a] -> Bool
isSortedBy :: Ord b => (a -> b) -> [a] -> Bool
usort :: Ord a => [a] -> [a]
usortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy' :: Ord b => (a -> b) -> [a] -> [a]
usortBy' :: Ord b => (a -> b) -> [a] -> [a]
orElse :: Ordering -> Ordering -> Ordering
unbuffered :: IO a -> IO a
labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]
fixpoint :: Eq a => (a -> a) -> a -> a
fixpointOn :: Eq b => (a -> b) -> (a -> a) -> a -> a
intMin :: Int -> Int -> Int
intMax :: Int -> Int -> Int
splitInterval :: Integral a => a -> (a, a) -> [(a, a)]
reservoir :: Int -> [(Integer, Int)]
data Sample a
Sample :: Integer -> [(Integer, Int)] -> [a] -> Sample a
emptySample :: Int -> Sample a
addSample :: (Int, [a]) -> Sample a -> Sample a
sampleValue :: Sample a -> [a]
mapSample :: (a -> b) -> Sample a -> Sample b
splits :: [a] -> [([a], [a])]
foldn :: (a -> a) -> a -> Int -> a
-- | Terms and substitutions.
--
-- Terms in twee are represented as arrays rather than as an algebraic
-- data type. This module defines pattern synonyms (App,
-- Var, Cons, Empty) which means that pattern
-- matching on terms works just as normal. The pattern synonyms can not
-- be used to create new terms; for that you have to use a builder
-- interface (Build).
--
-- This module also provides:
--
--
-- - pattern synonyms for iterating through a term one symbol at a time
-- (ConsSym);
-- - substitutions (Substitution, Subst,
-- subst);
-- - unification (unify) and matching (match);
-- - miscellaneous useful functions on terms.
--
module Twee.Term
-- | Term f is a term whose function symbols have type
-- f. It is either a Var or an App.
data Term f
-- | Matches a variable.
pattern Var :: Var -> Term f
-- | Matches a function application.
pattern App :: Fun f -> TermList f -> Term f
-- | Check if a term is a function application.
isApp :: Term f -> Bool
-- | Check if a term is a variable
isVar :: Term f -> Bool
-- | Convert a term to a termlist.
singleton :: Term f -> TermList f
-- | Find the length of a term.
len :: Term f -> Int
-- | TermList f is a list of terms whose function symbols
-- have type f. It is either a Cons or an Empty.
-- You can turn it into a [Term f] with unpack.
data TermList f
-- | Matches the empty termlist.
pattern Empty :: TermList f
-- | Matches a non-empty termlist, unpacking it into head and tail.
pattern Cons :: Term f -> TermList f -> TermList f
-- | Matches a non-empty termlist, unpacking it into head and everything
-- except the root symbol of the head. Useful for iterating through
-- terms one symbol at a time.
--
-- For example, if ts is the termlist [f(x,y), g(z)],
-- then let ConsSym u us = ts results in the following bindings:
--
--
-- u = f(x,y)
-- us = [x, y, g(z)]
--
pattern ConsSym :: Term f -> TermList f -> TermList f -> TermList f
hd :: TermList f -> Term f
tl :: TermList f -> TermList f
rest :: TermList f -> TermList f
-- | Like Cons, but does not check that the termlist is non-empty.
-- Use only if you are sure the termlist is non-empty.
pattern UnsafeCons :: Term f -> TermList f -> TermList f
-- | Like ConsSym, but does not check that the termlist is
-- non-empty. Use only if you are sure the termlist is non-empty.
pattern UnsafeConsSym :: Term f -> TermList f -> TermList f -> TermList f
uhd :: TermList f -> Term f
utl :: TermList f -> TermList f
urest :: TermList f -> TermList f
-- | The empty termlist.
empty :: forall f. TermList f
-- | Convert a termlist into an ordinary list of terms.
unpack :: TermList f -> [Term f]
-- | The length of (number of symbols in) a termlist.
lenList :: TermList f -> Int
-- | A function symbol. f is the underlying type of function
-- symbols defined by the user; Fun f is an f
-- together with an automatically-generated unique number.
data Fun f
-- | Construct a Fun from a function symbol.
fun :: Labelled f => f -> Fun f
-- | The unique number of a Fun. Must fit in 32 bits.
fun_id :: Fun f -> Int
-- | The underlying function symbol of a Fun.
fun_value :: Labelled f => Fun f -> f
-- | A pattern which extracts the fun_value from a Fun.
pattern F :: Labelled f => Int -> f -> Fun f
-- | A variable.
newtype Var
V :: Int -> Var
-- | The variable's number. Don't use huge variable numbers: they will be
-- truncated to 32 bits when stored in a term.
[var_id] :: Var -> Int
class Labelled f
label :: Labelled f => f -> Label f
label :: (Labelled f, Ord f, Typeable f) => f -> Label f
-- | Instances of Build can be turned into terms using build
-- or buildList, and turned into term builders using
-- builder. Has instances for terms, termlists, builders, and
-- Haskell lists.
class Build a where {
-- | The underlying type of function symbols.
type family BuildFun a;
}
-- | Convert a value into a Builder.
builder :: Build a => a -> Builder (BuildFun a)
-- | A monoid for building terms. mempty represents the empty
-- termlist, while mappend appends two termlists.
data Builder f
-- | Build a term. The given builder must produce exactly one term.
build :: Build a => a -> Term (BuildFun a)
-- | Build a termlist.
buildList :: Build a => a -> TermList (BuildFun a)
-- | Build a constant (a function with no arguments).
con :: Fun f -> Builder f
-- | Build a function application.
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
-- | Build a variable.
var :: Var -> Builder f
-- | Get the children (direct subterms) of a term.
children :: Term f -> TermList f
-- | Find all proper subterms of a term.
properSubterms :: Term f -> [Term f]
-- | Find all subterms of a termlist.
subtermsList :: TermList f -> [Term f]
-- | Find all subterms of a term.
subterms :: Term f -> [Term f]
-- | Find all subterms of a term, but in reverse order.
reverseSubtermsList :: TermList f -> [Term f]
reverseSubterms :: Term f -> [Term f]
-- | Check if a variable occurs in a term.
occurs :: Var -> Term f -> Bool
-- | Is a term a subterm of another one?
isSubtermOf :: Term f -> Term f -> Bool
-- | Is a term contained as a subterm in a given termlist?
isSubtermOfList :: Term f -> TermList f -> Bool
-- | Index into a termlist.
at :: Int -> TermList f -> Term f
-- | A class for values which act as substitutions.
--
-- Instances include Subst as well as functions from variables to
-- terms.
class Substitution s where {
-- | The underlying type of function symbols.
type family SubstFun s;
}
-- | Apply the substitution to a variable.
evalSubst :: Substitution s => s -> Var -> Builder (SubstFun s)
-- | Apply the substitution to a termlist.
substList :: Substitution s => s -> TermList (SubstFun s) -> Builder (SubstFun s)
-- | Apply a substitution to a term.
subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)
-- | A substitution which maps variables to terms of type Term
-- f.
newtype Subst f
Subst :: IntMap (TermList f) -> Subst f
[unSubst] :: Subst f -> IntMap (TermList f)
-- | The empty substitution.
emptySubst :: Subst f
-- | Construct a substitution from a list. Returns Nothing if a
-- variable is bound to several different terms.
listToSubst :: [(Var, Term f)] -> Maybe (Subst f)
-- | Convert a substitution to a list of bindings.
substToList :: Subst f -> [(Var, Term f)]
-- | Look up a variable in a substitution.
lookup :: Var -> Subst f -> Maybe (Term f)
-- | Look up a variable in a substitution, returning a termlist.
lookupList :: Var -> Subst f -> Maybe (TermList f)
-- | Add a new binding to a substitution.
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
-- | Add a new binding to a substitution, giving a termlist.
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)
-- | Add a new binding to a substitution. Overwrites any existing binding.
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f
-- | Remove a binding from a substitution.
retract :: Var -> Subst f -> Subst f
-- | Fold a function over a substitution.
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
-- | Check if all bindings of a substitution satisfy a given property.
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
-- | Compute the set of variables bound by a substitution.
substDomain :: Subst f -> [Var]
-- | Return the highest-number variable in a substitution plus 1.
substSize :: Subst f -> Int
-- | Check if two substitutions are compatible (they do not send the same
-- variable to different terms).
substCompatible :: Subst f -> Subst f -> Bool
-- | Take the union of two substitutions. The substitutions must be
-- compatible, which is not checked.
substUnion :: Subst f -> Subst f -> Subst f
-- | Check if a substitution is idempotent (applying it twice has the same
-- effect as applying it once).
idempotent :: Subst f -> Bool
-- | Check if a substitution has no effect on a given term.
idempotentOn :: Subst f -> TermList f -> Bool
-- | Return a substitution which renames the variables of a list of terms
-- to put them in a canonical order.
canonicalise :: [TermList f] -> Subst f
-- | match pat t matches the term t against the
-- pattern pat.
match :: Term f -> Term f -> Maybe (Subst f)
-- | A variant of match which extends an existing substitution.
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)
-- | A variant of match which works on termlists.
matchList :: TermList f -> TermList f -> Maybe (Subst f)
-- | A variant of match which works on termlists and extends an
-- existing substitution.
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
-- | A variant of match which works on lists of terms.
matchMany :: [Term f] -> [Term f] -> Maybe (Subst f)
-- | A variant of match which works on lists of terms, and extends
-- an existing substitution.
matchManyIn :: Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
-- | A variant of match which works on lists of termlists.
matchManyList :: [TermList f] -> [TermList f] -> Maybe (Subst f)
-- | A variant of match which works on lists of termlists, and
-- extends an existing substitution.
matchManyListIn :: Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
-- | t `isInstanceOf` pat checks if t is an
-- instance of pat.
isInstanceOf :: Term f -> Term f -> Bool
-- | Check if two terms are renamings of one another.
isVariantOf :: Term f -> Term f -> Bool
-- | Unify two terms.
unify :: Term f -> Term f -> Maybe (Subst f)
-- | Unify two termlists.
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
-- | Unify a collection of pairs of terms.
unifyMany :: [(Term f, Term f)] -> Maybe (Subst f)
-- | Unify a collection of pairs of terms, returning a triangle
-- substitution.
unifyManyTri :: [(Term f, Term f)] -> Maybe (TriangleSubst f)
-- | Unify two terms, returning a triangle substitution. This is slightly
-- faster than unify.
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
-- | Unify two terms, starting from an existing substitution.
unifyTriFrom :: Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
-- | Unify two termlists, returning a triangle substitution. This is
-- slightly faster than unify.
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
-- | A triangle substitution is one in which variables can be defined in
-- terms of each other, though not in a circular way.
--
-- The main use of triangle substitutions is in unification;
-- unifyTri returns one. A triangle substitution can be converted
-- to an ordinary substitution with close, or used directly using
-- its Substitution instance.
newtype TriangleSubst f
Triangle :: Subst f -> TriangleSubst f
[unTriangle] :: TriangleSubst f -> Subst f
-- | The empty triangle substitution.
emptyTriangleSubst :: TriangleSubst f
-- | Iterate a triangle substitution to make it idempotent.
close :: TriangleSubst f -> Subst f
-- | Convert a position in a term, expressed as a single number, into a
-- path.
positionToPath :: Term f -> Int -> [Int]
-- | Convert a path in a term into a position.
pathToPosition :: Term f -> [Int] -> Int
-- | Replace the term at a given position in a term with a different term.
replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f
-- | Replace the term at a given position in a term with a different term,
-- while simultaneously applying a substitution. Useful for building
-- critical pairs.
replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f
replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f
-- | Return the lowest- and highest-numbered variables in a term.
bound :: Term f -> (Var, Var)
-- | Return the lowest- and highest-numbered variables in a termlist.
boundList :: TermList f -> (Var, Var)
-- | Return the lowest- and highest-numbered variables in a list of
-- termlists.
boundLists :: [TermList f] -> (Var, Var)
-- | Map a function over the function symbols in a term.
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
-- | Map a function over the function symbols in a termlist.
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
-- | Compare the fun_values of two Funs.
(<<) :: (Labelled f, Ord f) => Fun f -> Fun f -> Bool
instance GHC.Classes.Ord (Twee.Term.Subst f)
instance GHC.Classes.Eq (Twee.Term.Subst f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Term.TriangleSubst f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Term.Core.Term f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Term.Core.TermList f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Term.Subst f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Term.Core.Fun f)
instance Twee.Term.Substitution (Twee.Term.TriangleSubst f)
instance Twee.Term.Substitution (Twee.Term.Subst f)
instance (Twee.Term.Build a, v GHC.Types.~ Twee.Term.Core.Var) => Twee.Term.Substitution (v -> a)
instance Twee.Term.Build (Twee.Term.Core.Builder f)
instance Twee.Term.Build (Twee.Term.Core.Term f)
instance Twee.Term.Build (Twee.Term.Core.TermList f)
instance Twee.Term.Build a => Twee.Term.Build [a]
-- | Pretty-printing of terms and assorted other values.
module Twee.Pretty
-- | Defines how to print out a function symbol.
newtype TermStyle
TermStyle :: (forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc) -> TermStyle
-- | Renders a function application. Takes the following arguments in this
-- order: Pretty-printing level, current precedence, pretty-printed
-- function symbol and list of arguments to the function.
[pPrintTerm] :: TermStyle -> forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc
-- | A class for customising the printing of function symbols.
class Pretty f => PrettyTerm f
-- | The style of the function symbol. Defaults to curried.
termStyle :: PrettyTerm f => f -> TermStyle
type ANSICode = String
data HighlightedTerm f
HighlightedTerm :: [ANSICode] -> Maybe [Int] -> Term f -> HighlightedTerm f
-- | Print a value to the console.
prettyPrint :: Pretty a => a -> IO ()
-- | Put one document beside another, i.e., <>. Renamed here
-- because (a different) <> is exported by Prelude.
(<#>) :: Doc -> Doc -> Doc
infixl 6 <#>
-- | The empty document. Used to avoid name clashes with empty.
pPrintEmpty :: Doc
-- | Print a tuple of values.
pPrintTuple :: [Doc] -> Doc
-- | Print a set of vlaues.
pPrintSet :: [Doc] -> Doc
-- | Generate a list of candidate names for pretty-printing.
supply :: [String] -> [String]
green :: ANSICode
bold :: ANSICode
highlight :: [ANSICode] -> Doc -> Doc
maybeHighlight :: [ANSICode] -> Maybe [Int] -> Doc -> Doc
-- | For operators like $ that should be printed as a blank space.
invisible :: TermStyle
-- | For functions that should be printed curried.
curried :: TermStyle
-- | For functions that should be printed uncurried.
uncurried :: TermStyle
-- | A helper function that deals with under- and oversaturated
-- applications.
fixedArity :: Int -> TermStyle -> TermStyle
-- | A helper function that drops a certain number of arguments.
implicitArguments :: Int -> TermStyle -> TermStyle
-- | For prefix operators.
prefix :: TermStyle
-- | For postfix operators.
postfix :: TermStyle
-- | For infix operators.
infixStyle :: Int -> TermStyle
-- | For tuples.
tupleStyle :: TermStyle
-- | Parenthesize an value if the boolean is true.
prettyParen :: Bool -> Doc -> Doc
-- | Pretty print a value with the prettyNormal level.
prettyShow :: Pretty a => a -> String
-- | The "normal" (Level 0) of detail.
prettyNormal :: PrettyLevel
-- | Level of detail in the pretty printed output. Level 0 is the least
-- detail.
newtype PrettyLevel
PrettyLevel :: Int -> PrettyLevel
-- | Pretty printing class. The precedence level is used in a similar way
-- as in the Show class. Minimal complete definition is either
-- pPrintPrec or pPrint.
class Pretty a
pPrintPrec :: Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrint :: Pretty a => a -> Doc
pPrintList :: Pretty a => PrettyLevel -> [a] -> Doc
-- | The general rendering interface. Please refer to the Style
-- and Mode types for a description of rendering mode, line
-- length and ribbons.
fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
-- | Render the Doc to a String using the given Style.
renderStyle :: Style -> Doc -> String
-- | Render the Doc to a String using the default Style
-- (see style).
render :: Doc -> String
-- | first returns its first argument if it is non-empty,
-- otherwise its second.
first :: Doc -> Doc -> Doc
-- | "Paragraph fill" version of sep.
fsep :: [Doc] -> Doc
-- | "Paragraph fill" version of cat.
fcat :: [Doc] -> Doc
-- | Either hcat or vcat.
cat :: [Doc] -> Doc
-- | Either hsep or vcat.
sep :: [Doc] -> Doc
-- | Beside, separated by space, unless one of the arguments is
-- empty. <+> is associative, with identity
-- empty.
(<+>) :: Doc -> Doc -> Doc
infixl 6 <+>
-- | Above, with no overlapping. $+$ is associative, with identity
-- empty.
($+$) :: Doc -> Doc -> Doc
infixl 5 $+$
-- | Above, except that if the last line of the first argument stops at
-- least one position before the first line of the second begins, these
-- two lines are overlapped. For example:
--
--
-- text "hi" $$ nest 5 (text "there")
--
--
-- lays out as
--
--
-- hi there
--
--
-- rather than
--
--
-- hi
-- there
--
--
-- $$ is associative, with identity empty, and also
-- satisfies
--
--
-- - (x $$ y) <> z = x $$ (y
-- <> z), if y non-empty.
--
($$) :: Doc -> Doc -> Doc
infixl 5 $$
-- |
-- punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]
--
punctuate :: Doc -> [Doc] -> [Doc]
-- |
-- hang d1 n d2 = sep [d1, nest n d2]
--
hang :: Doc -> Int -> Doc -> Doc
-- | Nest (or indent) a document by a given number of positions (which may
-- also be negative). nest satisfies the laws:
--
--
--
-- The side condition on the last law is needed because empty is a
-- left identity for <>.
nest :: Int -> Doc -> Doc
-- | List version of $$.
vcat :: [Doc] -> Doc
-- | List version of <+>.
hsep :: [Doc] -> Doc
-- | List version of <>.
hcat :: [Doc] -> Doc
-- | Perform some simplification of a built up GDoc.
reduceDoc :: Doc -> RDoc
-- | Apply doubleQuotes to Doc if boolean is true.
maybeDoubleQuotes :: Bool -> Doc -> Doc
-- | Apply quotes to Doc if boolean is true.
maybeQuotes :: Bool -> Doc -> Doc
-- | Apply braces to Doc if boolean is true.
maybeBraces :: Bool -> Doc -> Doc
-- | Apply brackets to Doc if boolean is true.
maybeBrackets :: Bool -> Doc -> Doc
-- | Apply parens to Doc if boolean is true.
maybeParens :: Bool -> Doc -> Doc
braces :: Doc -> Doc
brackets :: Doc -> Doc
parens :: Doc -> Doc
doubleQuotes :: Doc -> Doc
quotes :: Doc -> Doc
rational :: Rational -> Doc
double :: Double -> Doc
float :: Float -> Doc
integer :: Integer -> Doc
int :: Int -> Doc
rbrace :: Doc
lbrace :: Doc
rbrack :: Doc
lbrack :: Doc
rparen :: Doc
lparen :: Doc
equals :: Doc
space :: Doc
colon :: Doc
comma :: Doc
semi :: Doc
-- | Returns True if the document is empty
isEmpty :: Doc -> Bool
-- | Some text, but without any width. Use for non-printing text such as a
-- HTML or Latex tags
zeroWidthText :: String -> Doc
-- | Some text with any width. (text s = sizedText (length s) s)
sizedText :: Int -> String -> Doc
-- | Same as text. Used to be used for Bytestrings.
ptext :: String -> Doc
-- | A document of height 1 containing a literal string. text
-- satisfies the following laws:
--
--
--
-- The side condition on the last law is necessary because
-- text "" has height 1, while empty has no
-- height.
text :: String -> Doc
-- | A document of height and width 1, containing a literal character.
char :: Char -> Doc
-- | The abstract type of documents. A Doc represents a set of
-- layouts. A Doc with no occurrences of Union or NoDoc represents just
-- one layout.
data Doc
-- | The default style (mode=PageMode, lineLength=100,
-- ribbonsPerLine=1.5).
style :: Style
-- | A TextDetails represents a fragment of text that will be output at
-- some point in a Doc.
data TextDetails
-- | A single Char fragment
Chr :: {-# UNPACK #-} !Char -> TextDetails
-- | A whole String fragment
Str :: String -> TextDetails
-- | Used to represent a Fast String fragment but now deprecated and
-- identical to the Str constructor.
PStr :: String -> TextDetails
-- | A rendering style. Allows us to specify constraints to choose among
-- the many different rendering options.
data Style
Style :: Mode -> Int -> Float -> Style
-- | The rendering mode.
[mode] :: Style -> Mode
-- | Maximum length of a line, in characters.
[lineLength] :: Style -> Int
-- | Ratio of line length to ribbon length. A ribbon refers to the
-- characters on a line excluding indentation. So a
-- lineLength of 100, with a ribbonsPerLine of 2.0
-- would only allow up to 50 characters of ribbon to be displayed on a
-- line, while allowing it to be indented up to 50 characters.
[ribbonsPerLine] :: Style -> Float
-- | Rendering mode.
data Mode
-- | Normal rendering (lineLength and ribbonsPerLine
-- respected').
PageMode :: Mode
-- | With zig-zag cuts.
ZigZagMode :: Mode
-- | No indentation, infinitely long lines (lineLength ignored), but
-- explicit new lines, i.e., text "one" $$ text "two", are
-- respected.
LeftMode :: Mode
-- | All on one line, lineLength ignored and explicit new lines
-- ($$) are turned into spaces.
OneLineMode :: Mode
-- | Pretty printing class. The precedence level is used in a similar way
-- as in the Show class. Minimal complete definition is either
-- pPrintPrec or pPrint.
class Pretty a
pPrintPrec :: Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrint :: Pretty a => a -> Doc
pPrintList :: Pretty a => PrettyLevel -> [a] -> Doc
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Term f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Pretty.HighlightedTerm f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.TermList f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Subst f)
instance Text.PrettyPrint.HughesPJClass.Pretty Text.PrettyPrint.HughesPJ.Doc
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (Data.Set.Internal.Set a)
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.Term.Core.Var
instance (Text.PrettyPrint.HughesPJClass.Pretty k, Text.PrettyPrint.HughesPJClass.Pretty v) => Text.PrettyPrint.HughesPJClass.Pretty (Data.Map.Internal.Map k v)
instance (GHC.Classes.Eq a, GHC.Real.Integral a, Text.PrettyPrint.HughesPJClass.Pretty a) => Text.PrettyPrint.HughesPJClass.Pretty (GHC.Real.Ratio a)
instance (Text.PrettyPrint.HughesPJClass.Pretty f, Twee.Term.Labelled f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Fun f)
-- | A queue of passive critical pairs, using a memory-efficient
-- representation.
module Twee.PassiveQueue
-- | A datatype representing all the type parameters of the queue.
class (Eq (Id params), Integral (Id params), Ord (Score params), Unbox (PackedScore params), Unbox (PackedId params)) => Params params where {
-- | The score assigned to critical pairs. Smaller scores are better.
type family Score params;
-- | The type of ID numbers used to name rules.
type family Id params;
-- | A Score packed for storage into a Vector. Must be an
-- instance of Unbox.
type family PackedScore params;
-- | An Id packed for storage into a Vector. Must be an
-- instance of Unbox.
type family PackedId params;
}
-- | Pack a Score.
packScore :: Params params => proxy params -> Score params -> PackedScore params
-- | Unpack a PackedScore.
unpackScore :: Params params => proxy params -> PackedScore params -> Score params
-- | Pack an Id.
packId :: Params params => proxy params -> Id params -> PackedId params
-- | Unpack a PackedId.
unpackId :: Params params => proxy params -> PackedId params -> Id params
-- | A critical pair queue.
data Queue params
-- | A queued critical pair.
data Passive params
Passive :: !Score params -> !Id params -> !Id params -> {-# UNPACK #-} !Int -> Passive params
-- | The score of this critical pair.
[passive_score] :: Passive params -> !Score params
-- | The rule which does the outermost rewrite in this critical pair.
[passive_rule1] :: Passive params -> !Id params
-- | The rule which does the innermost rewrite in this critical pair.
[passive_rule2] :: Passive params -> !Id params
-- | The position of the overlap. See overlap_pos.
[passive_pos] :: Passive params -> {-# UNPACK #-} !Int
-- | The empty queue.
empty :: Queue params
-- | Add a set of Passives to the queue.
insert :: Params params => Id params -> [Passive params] -> Queue params -> Queue params
-- | Remove the minimum Passive from the queue.
removeMin :: Params params => Queue params -> Maybe (Passive params, Queue params)
-- | Map a function over all Passives.
mapMaybe :: Params params => (Passive params -> Maybe (Passive params)) -> Queue params -> Queue params
-- | Convert a queue into a list of Passives. The Passives
-- are produced in batches, with each batch labelled with its size.
toList :: Params params => Queue params -> [(Int, [Passive params])]
queueSize :: Params params => Queue params -> Int
instance Twee.PassiveQueue.Params params => GHC.Classes.Eq (Twee.PassiveQueue.PassiveSet params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Ord (Twee.PassiveQueue.PassiveSet params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Eq (Twee.PassiveQueue.Passive params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Ord (Twee.PassiveQueue.Passive params)
-- | Solving constraints on variable ordering.
module Twee.Constraints
data Atom f
Constant :: Fun f -> Atom f
Variable :: Var -> Atom f
atoms :: Term f -> [Atom f]
toTerm :: Atom f -> Term f
fromTerm :: Term f -> Maybe (Atom f)
data Formula f
Less :: Atom f -> Atom f -> Formula f
LessEq :: Atom f -> Atom f -> Formula f
And :: [Formula f] -> Formula f
Or :: [Formula f] -> Formula f
negateFormula :: Formula f -> Formula f
conj :: Foldable t => t (Formula f) -> Formula f
disj :: Foldable t => t (Formula f) -> Formula f
(&&&) :: Formula f -> Formula f -> Formula f
(|||) :: Formula f -> Formula f -> Formula f
true :: Formula f
false :: Formula f
data Branch f
Branch :: [Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
[funs] :: Branch f -> [Fun f]
[less] :: Branch f -> [(Atom f, Atom f)]
[equals] :: Branch f -> [(Atom f, Atom f)]
trueBranch :: Branch f
norm :: Eq f => Branch f -> Atom f -> Atom f
contradictory :: (Minimal f, Ord f, Labelled f) => Branch f -> Bool
formAnd :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f] -> [Branch f]
branches :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f]
addLess :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
addEquals :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
addTerm :: (Minimal f, Ordered f, Labelled f) => Atom f -> Branch f -> Branch f
newtype Model f
Model :: Map (Atom f) (Int, Int) -> Model f
modelToLiterals :: Model f -> [Formula f]
modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f
weakenModel :: Model f -> [Model f]
varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool
varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]
class Minimal f
minimal :: Minimal f => Fun f
lessEqInModel :: (Minimal f, Ordered f, Labelled f) => Model f -> Atom f -> Atom f -> Maybe Strictness
solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
class Ord f => Ordered f
-- | Return True if the first term is less than or equal to the
-- second, in the term ordering.
lessEq :: Ordered f => Term f -> Term f -> Bool
-- | Check if the first term is less than or equal to the second in the
-- given model, and decide whether the inequality is strict or nonstrict.
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness
lessEqSkolem :: Ordered f => Term f -> Term f -> Bool
-- | Describes whether an inequality is strict or nonstrict.
data Strictness
-- | The first term is strictly less than the second.
Strict :: Strictness
-- | The first term is less than or equal to the second.
Nonstrict :: Strictness
-- | Return True if the first argument is strictly less than the
-- second, in the term ordering.
lessThan :: Ordered f => Term f -> Term f -> Bool
-- | Return the direction in which the terms are oriented according to the
-- term ordering, or Nothing if they cannot be oriented. A result
-- of Just LT means that the first term is less
-- than or equal to the second.
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
instance GHC.Classes.Ord (Twee.Constraints.Atom f)
instance GHC.Classes.Eq (Twee.Constraints.Atom f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Constraints.Atom f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Constraints.Formula f)
instance GHC.Classes.Ord (Twee.Constraints.Formula f)
instance GHC.Classes.Eq (Twee.Constraints.Formula f)
instance GHC.Classes.Ord (Twee.Constraints.Branch f)
instance GHC.Classes.Eq (Twee.Constraints.Branch f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Constraints.Model f)
instance GHC.Classes.Eq (Twee.Constraints.Model f)
instance GHC.Show.Show Twee.Constraints.Strictness
instance GHC.Classes.Eq Twee.Constraints.Strictness
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Model f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Branch f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Formula f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Atom f)
-- | Useful operations on terms and similar. Also re-exports some generally
-- useful modules such as Term and Pretty.
module Twee.Base
-- | A monoid for building terms. mempty represents the empty
-- termlist, while mappend appends two termlists.
data Builder f
-- | A variable.
newtype Var
V :: Int -> Var
-- | The variable's number. Don't use huge variable numbers: they will be
-- truncated to 32 bits when stored in a term.
[var_id] :: Var -> Int
-- | A function symbol. f is the underlying type of function
-- symbols defined by the user; Fun f is an f
-- together with an automatically-generated unique number.
data Fun f
-- | Term f is a term whose function symbols have type
-- f. It is either a Var or an App.
data Term f
-- | TermList f is a list of terms whose function symbols
-- have type f. It is either a Cons or an Empty.
-- You can turn it into a [Term f] with unpack.
data TermList f
-- | Matches a function application.
pattern App :: Fun f -> TermList f -> Term f
-- | Matches a variable.
pattern Var :: Var -> Term f
-- | Like ConsSym, but does not check that the termlist is
-- non-empty. Use only if you are sure the termlist is non-empty.
pattern UnsafeConsSym :: Term f -> TermList f -> TermList f -> TermList f
uhd :: TermList f -> Term f
utl :: TermList f -> TermList f
urest :: TermList f -> TermList f
-- | Matches a non-empty termlist, unpacking it into head and everything
-- except the root symbol of the head. Useful for iterating through
-- terms one symbol at a time.
--
-- For example, if ts is the termlist [f(x,y), g(z)],
-- then let ConsSym u us = ts results in the following bindings:
--
--
-- u = f(x,y)
-- us = [x, y, g(z)]
--
pattern ConsSym :: Term f -> TermList f -> TermList f -> TermList f
hd :: TermList f -> Term f
tl :: TermList f -> TermList f
rest :: TermList f -> TermList f
-- | Like Cons, but does not check that the termlist is non-empty.
-- Use only if you are sure the termlist is non-empty.
pattern UnsafeCons :: Term f -> TermList f -> TermList f
-- | Matches a non-empty termlist, unpacking it into head and tail.
pattern Cons :: Term f -> TermList f -> TermList f
-- | Matches the empty termlist.
pattern Empty :: TermList f
-- | Index into a termlist.
at :: Int -> TermList f -> Term f
-- | The length of (number of symbols in) a termlist.
lenList :: TermList f -> Int
-- | Convert a term to a termlist.
singleton :: Term f -> TermList f
-- | Is a term contained as a subterm in a given termlist?
isSubtermOfList :: Term f -> TermList f -> Bool
class Labelled f
label :: Labelled f => f -> Label f
label :: (Labelled f, Ord f, Typeable f) => f -> Label f
-- | A triangle substitution is one in which variables can be defined in
-- terms of each other, though not in a circular way.
--
-- The main use of triangle substitutions is in unification;
-- unifyTri returns one. A triangle substitution can be converted
-- to an ordinary substitution with close, or used directly using
-- its Substitution instance.
newtype TriangleSubst f
Triangle :: Subst f -> TriangleSubst f
[unTriangle] :: TriangleSubst f -> Subst f
-- | A substitution which maps variables to terms of type Term
-- f.
newtype Subst f
Subst :: IntMap (TermList f) -> Subst f
[unSubst] :: Subst f -> IntMap (TermList f)
-- | A class for values which act as substitutions.
--
-- Instances include Subst as well as functions from variables to
-- terms.
class Substitution s where {
-- | The underlying type of function symbols.
type family SubstFun s;
}
-- | Apply the substitution to a variable.
evalSubst :: Substitution s => s -> Var -> Builder (SubstFun s)
-- | Apply the substitution to a termlist.
substList :: Substitution s => s -> TermList (SubstFun s) -> Builder (SubstFun s)
-- | Instances of Build can be turned into terms using build
-- or buildList, and turned into term builders using
-- builder. Has instances for terms, termlists, builders, and
-- Haskell lists.
class Build a where {
-- | The underlying type of function symbols.
type family BuildFun a;
}
-- | Convert a value into a Builder.
builder :: Build a => a -> Builder (BuildFun a)
-- | A pattern which extracts the fun_value from a Fun.
pattern F :: Labelled f => Int -> f -> Fun f
-- | Build a term. The given builder must produce exactly one term.
build :: Build a => a -> Term (BuildFun a)
-- | Build a termlist.
buildList :: Build a => a -> TermList (BuildFun a)
-- | Build a constant (a function with no arguments).
con :: Fun f -> Builder f
-- | Build a function application.
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
-- | Build a variable.
var :: Var -> Builder f
-- | Convert a substitution to a list of bindings.
substToList :: Subst f -> [(Var, Term f)]
-- | Fold a function over a substitution.
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
-- | Check if all bindings of a substitution satisfy a given property.
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
-- | Compute the set of variables bound by a substitution.
substDomain :: Subst f -> [Var]
-- | Return the highest-number variable in a substitution plus 1.
substSize :: Subst f -> Int
-- | Look up a variable in a substitution, returning a termlist.
lookupList :: Var -> Subst f -> Maybe (TermList f)
-- | Add a new binding to a substitution, giving a termlist.
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)
-- | Remove a binding from a substitution.
retract :: Var -> Subst f -> Subst f
-- | Add a new binding to a substitution. Overwrites any existing binding.
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f
-- | Check if two substitutions are compatible (they do not send the same
-- variable to different terms).
substCompatible :: Subst f -> Subst f -> Bool
-- | Take the union of two substitutions. The substitutions must be
-- compatible, which is not checked.
substUnion :: Subst f -> Subst f -> Subst f
-- | Check if a substitution is idempotent (applying it twice has the same
-- effect as applying it once).
idempotent :: Subst f -> Bool
-- | Check if a substitution has no effect on a given term.
idempotentOn :: Subst f -> TermList f -> Bool
-- | Iterate a triangle substitution to make it idempotent.
close :: TriangleSubst f -> Subst f
-- | The empty substitution.
emptySubst :: Subst f
-- | The empty triangle substitution.
emptyTriangleSubst :: TriangleSubst f
-- | Construct a substitution from a list. Returns Nothing if a
-- variable is bound to several different terms.
listToSubst :: [(Var, Term f)] -> Maybe (Subst f)
-- | match pat t matches the term t against the
-- pattern pat.
match :: Term f -> Term f -> Maybe (Subst f)
-- | A variant of match which extends an existing substitution.
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)
-- | A variant of match which works on termlists.
matchList :: TermList f -> TermList f -> Maybe (Subst f)
-- | A variant of match which works on termlists and extends an
-- existing substitution.
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
-- | A variant of match which works on lists of terms.
matchMany :: [Term f] -> [Term f] -> Maybe (Subst f)
-- | A variant of match which works on lists of terms, and extends
-- an existing substitution.
matchManyIn :: Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
-- | A variant of match which works on lists of termlists.
matchManyList :: [TermList f] -> [TermList f] -> Maybe (Subst f)
-- | A variant of match which works on lists of termlists, and
-- extends an existing substitution.
matchManyListIn :: Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
-- | Unify two terms.
unify :: Term f -> Term f -> Maybe (Subst f)
-- | Unify two termlists.
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
-- | Unify a collection of pairs of terms.
unifyMany :: [(Term f, Term f)] -> Maybe (Subst f)
-- | Unify a collection of pairs of terms, returning a triangle
-- substitution.
unifyManyTri :: [(Term f, Term f)] -> Maybe (TriangleSubst f)
-- | Unify two terms, returning a triangle substitution. This is slightly
-- faster than unify.
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
-- | Unify two terms, starting from an existing substitution.
unifyTriFrom :: Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
-- | Unify two termlists, returning a triangle substitution. This is
-- slightly faster than unify.
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
-- | The empty termlist.
empty :: forall f. TermList f
-- | Get the children (direct subterms) of a term.
children :: Term f -> TermList f
-- | Convert a termlist into an ordinary list of terms.
unpack :: TermList f -> [Term f]
-- | Look up a variable in a substitution.
lookup :: Var -> Subst f -> Maybe (Term f)
-- | Add a new binding to a substitution.
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
-- | Find the length of a term.
len :: Term f -> Int
-- | Return the lowest- and highest-numbered variables in a term.
bound :: Term f -> (Var, Var)
-- | Return the lowest- and highest-numbered variables in a termlist.
boundList :: TermList f -> (Var, Var)
-- | Return the lowest- and highest-numbered variables in a list of
-- termlists.
boundLists :: [TermList f] -> (Var, Var)
-- | Check if a variable occurs in a term.
occurs :: Var -> Term f -> Bool
-- | Find all subterms of a termlist.
subtermsList :: TermList f -> [Term f]
-- | Find all subterms of a term.
subterms :: Term f -> [Term f]
-- | Find all subterms of a term, but in reverse order.
reverseSubtermsList :: TermList f -> [Term f]
reverseSubterms :: Term f -> [Term f]
-- | Find all proper subterms of a term.
properSubterms :: Term f -> [Term f]
-- | Check if a term is a function application.
isApp :: Term f -> Bool
-- | Check if a term is a variable
isVar :: Term f -> Bool
-- | t `isInstanceOf` pat checks if t is an
-- instance of pat.
isInstanceOf :: Term f -> Term f -> Bool
-- | Check if two terms are renamings of one another.
isVariantOf :: Term f -> Term f -> Bool
-- | Is a term a subterm of another one?
isSubtermOf :: Term f -> Term f -> Bool
-- | Map a function over the function symbols in a term.
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
-- | Map a function over the function symbols in a termlist.
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f
-- | Replace the term at a given position in a term with a different term.
replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f
-- | Replace the term at a given position in a term with a different term,
-- while simultaneously applying a substitution. Useful for building
-- critical pairs.
replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f
-- | Convert a position in a term, expressed as a single number, into a
-- path.
positionToPath :: Term f -> Int -> [Int]
-- | Convert a path in a term into a position.
pathToPosition :: Term f -> [Int] -> Int
-- | Compare the fun_values of two Funs.
(<<) :: (Labelled f, Ord f) => Fun f -> Fun f -> Bool
-- | Construct a Fun from a function symbol.
fun :: Labelled f => f -> Fun f
-- | The underlying function symbol of a Fun.
fun_value :: Labelled f => Fun f -> f
-- | Generalisation of term functionality to things that contain terms
-- (e.g., rewrite rules and equations).
class Symbolic a where {
type family ConstantOf a;
}
-- | Compute a DList of all terms which appear in the argument (used
-- for e.g. computing free variables). See also terms.
termsDL :: Symbolic a => a -> DList (TermListOf a)
-- | Apply a substitution. When using the Symbolic type class, you
-- can use subst instead.
subst_ :: Symbolic a => (Var -> BuilderOf a) -> a -> a
-- | Apply a substitution.
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a
-- | Find all terms occuring in the argument.
terms :: Symbolic a => a -> [TermListOf a]
-- | A term compatible with a given Symbolic.
type TermOf a = Term (ConstantOf a)
-- | A termlist compatible with a given Symbolic.
type TermListOf a = TermList (ConstantOf a)
-- | A substitution compatible with a given Symbolic.
type SubstOf a = Subst (ConstantOf a)
-- | A triangle substitution compatible with a given Symbolic.
type TriangleSubstOf a = TriangleSubst (ConstantOf a)
-- | A builder compatible with a given Symbolic.
type BuilderOf a = Builder (ConstantOf a)
-- | The underlying type of function symbols of a given Symbolic.
type FunOf a = Fun (ConstantOf a)
-- | Find the variables occurring in the argument.
vars :: Symbolic a => a -> [Var]
-- | Test if the argument is ground.
isGround :: Symbolic a => a -> Bool
-- | Find the function symbols occurring in the argument.
funs :: Symbolic a => a -> [FunOf a]
-- | Count how many times a function symbol occurs in the argument.
occ :: Symbolic a => FunOf a -> a -> Int
-- | Count how many times a variable occurs in the argument.
occVar :: Symbolic a => Var -> a -> Int
-- | Rename the argument so that variables are introduced in a canonical
-- order (starting with V0, then V1 and so on).
canonicalise :: Symbolic a => a -> a
-- | Rename the second argument so that it does not mention any variable
-- which occurs in the first.
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
renameManyAvoiding :: Symbolic a => [a] -> [a]
-- | Return an x such that no variable >= x occurs in the argument.
freshVar :: Symbolic a => a -> Int
-- | Represents a unique identifier (e.g., for a rule).
newtype Id
Id :: Int32 -> Id
[unId] :: Id -> Int32
-- | An instance Has a b indicates that a value of type
-- a contains a value of type b which is somehow part
-- of the meaning of the a.
--
-- A number of functions use Has constraints to work in a more
-- general setting. For example, the functions in CP operate on
-- rewrite rules, but actually accept any a satisfying
-- Has a (Rule f).
--
-- Use taste when definining Has instances; don't do it
-- willy-nilly.
class Has a b
-- | Get at the thing.
the :: Has a b => a -> b
class Minimal f
minimal :: Minimal f => Fun f
-- | Build the minimal constant as a term.
minimalTerm :: Minimal f => Term f
-- | Check if a term is the minimal constant.
isMinimal :: Minimal f => Term f -> Bool
-- | Erase a given set of variables from the argument, replacing them with
-- the minimal constant.
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
-- | Erase all except a given set of variables from the argument, replacing
-- them with the minimal constant.
eraseExcept :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
-- | Replace all variables in the argument with the minimal constant.
ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
-- | For types which have a notion of arity.
class Arity f
-- | Measure the arity.
arity :: Arity f => f -> Int
class Ord f => Ordered f
-- | Return True if the first term is less than or equal to the
-- second, in the term ordering.
lessEq :: Ordered f => Term f -> Term f -> Bool
-- | Check if the first term is less than or equal to the second in the
-- given model, and decide whether the inequality is strict or nonstrict.
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness
lessEqSkolem :: Ordered f => Term f -> Term f -> Bool
-- | Return True if the first argument is strictly less than the
-- second, in the term ordering.
lessThan :: Ordered f => Term f -> Term f -> Bool
-- | Return the direction in which the terms are oriented according to the
-- term ordering, or Nothing if they cannot be oriented. A result
-- of Just LT means that the first term is less
-- than or equal to the second.
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
-- | A hack for encoding Horn clauses. See Score. The default
-- implementation of hasEqualsBonus should work OK.
class EqualsBonus f
hasEqualsBonus :: EqualsBonus f => f -> Bool
isEquals :: EqualsBonus f => f -> Bool
isTrue :: EqualsBonus f => f -> Bool
isFalse :: EqualsBonus f => f -> Bool
-- | Describes whether an inequality is strict or nonstrict.
data Strictness
-- | The first term is strictly less than the second.
Strict :: Strictness
-- | The first term is less than or equal to the second.
Nonstrict :: Strictness
-- | For types which have a notion of size. | The collection of constraints
-- which the type of function symbols must satisfy in order to be used by
-- twee.
type Function f = (Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)
instance GHC.Real.Integral Twee.Base.Id
instance GHC.Real.Real Twee.Base.Id
instance GHC.Num.Num Twee.Base.Id
instance GHC.Enum.Bounded Twee.Base.Id
instance GHC.Enum.Enum Twee.Base.Id
instance GHC.Show.Show Twee.Base.Id
instance GHC.Classes.Ord Twee.Base.Id
instance GHC.Classes.Eq Twee.Base.Id
instance (Twee.Term.Labelled f, Twee.Base.EqualsBonus f) => Twee.Base.EqualsBonus (Twee.Term.Core.Fun f)
instance (Twee.Term.Labelled f, Twee.Base.Arity f) => Twee.Base.Arity (Twee.Term.Core.Fun f)
instance Twee.Base.Symbolic (Twee.Term.Core.Term f)
instance Twee.Base.Symbolic (Twee.Term.Core.TermList f)
instance Twee.Base.Symbolic (Twee.Term.Subst f)
instance (Twee.Base.ConstantOf a GHC.Types.~ Twee.Base.ConstantOf b, Twee.Base.Symbolic a, Twee.Base.Symbolic b) => Twee.Base.Symbolic (a, b)
instance (Twee.Base.ConstantOf a GHC.Types.~ Twee.Base.ConstantOf b, Twee.Base.ConstantOf a GHC.Types.~ Twee.Base.ConstantOf c, Twee.Base.Symbolic a, Twee.Base.Symbolic b, Twee.Base.Symbolic c) => Twee.Base.Symbolic (a, b, c)
instance Twee.Base.Symbolic a => Twee.Base.Symbolic [a]
instance Twee.Base.Symbolic a => Twee.Base.Symbolic (GHC.Maybe.Maybe a)
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.Base.Id
-- | A term index to accelerate matching. An index is a multimap from terms
-- to arbitrary values.
--
-- The type of query supported is: given a search term, find all keys
-- such that the search term is an instance of the key, and return the
-- corresponding values.
module Twee.Index
-- | A term index: a multimap from Term f to a.
data Index f a
-- | An empty index.
empty :: Index f a
-- | Is the index empty?
null :: Index f a -> Bool
-- | An index with one entry.
singleton :: Term f -> a -> Index f a
-- | Insert an entry into the index.
insert :: (Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a
-- | Delete an entry from the index.
delete :: (Eq a, Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a
-- | Look up a term in the index. Finds all key-value such that the search
-- term is an instance of the key, and returns an instance of the the
-- value which makes the search term exactly equal to the key.
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]
-- | Look up a term in the index. Like lookup, but returns the exact
-- value that was inserted into the index, not an instance. Also returns
-- a substitution which when applied to the value gives you the matching
-- instance.
matches :: Term f -> Index f a -> [(Subst f, a)]
-- | Return all elements of the index.
elems :: Index f a -> [a]
-- | Create an index from a list of items
fromList :: (Symbolic a, ConstantOf a ~ f) => [(Term f, a)] -> Index f a
-- | Create an index from a list of items
fromListWith :: (Symbolic a, ConstantOf a ~ f) => (a -> Term f) -> [a] -> Index f a
-- | Check the invariant of an index. For debugging purposes.
invariant :: Index f a -> Bool
instance (Twee.Term.Labelled f, GHC.Show.Show f, GHC.Show.Show a) => GHC.Show.Show (Twee.Index.Index f a)
instance Data.DynamicArray.Default (Twee.Index.Index f a)
-- | Equations.
module Twee.Equation
data Equation f
(:=:) :: {-# UNPACK #-} !Term f -> {-# UNPACK #-} !Term f -> Equation f
[eqn_lhs] :: Equation f -> {-# UNPACK #-} !Term f
[eqn_rhs] :: Equation f -> {-# UNPACK #-} !Term f
type EquationOf a = Equation (ConstantOf a)
-- | Order an equation roughly left-to-right, and canonicalise its
-- variables. There is no guarantee that the result is oriented.
order :: Function f => Equation f -> Equation f
orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool
-- | Apply a function to both sides of an equation.
bothSides :: (Term f -> Term f') -> Equation f -> Equation f'
-- | Is an equation of the form t = t?
trivial :: Eq f => Equation f -> Bool
-- | A total order on equations. Equations with lesser terms are smaller.
simplerThan :: Function f => Equation f -> Equation f -> Bool
-- | Match one equation against another.
matchEquation :: Equation f -> Equation f -> Maybe (Subst f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Equation.Equation f)
instance GHC.Classes.Ord (Twee.Equation.Equation f)
instance GHC.Classes.Eq (Twee.Equation.Equation f)
instance Twee.Base.Symbolic (Twee.Equation.Equation f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Equation.Equation f)
-- | Equational proofs which are checked for correctedness.
module Twee.Proof
-- | A checked proof. If you have a value of type Proof f, it
-- should jolly well represent a valid proof!
--
-- The only way to construct a Proof f is by using
-- certify.
data Proof f
-- | 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 #-} !Proof f -> !Subst f -> Derivation f
-- | Apply an axiom to the root of a term
UseAxiom :: {-# UNPACK #-} !Axiom f -> !Subst f -> Derivation f
-- | Reflexivity. Refl t proves t = t.
Refl :: !Term f -> Derivation f
-- | Symmetry
Symm :: !Derivation f -> Derivation f
-- | Transivitity
Trans :: !Derivation f -> !Derivation f -> Derivation f
-- | Congruence. Parallel, i.e., takes a function symbol and one derivation
-- for each argument of that function.
Cong :: {-# UNPACK #-} !Fun f -> ![Derivation f] -> Derivation f
data Axiom f
Axiom :: {-# UNPACK #-} !Int -> !String -> !Equation f -> Axiom f
-- | The number of the axiom. Has no semantic meaning; for convenience
-- only.
[axiom_number] :: Axiom f -> {-# UNPACK #-} !Int
-- | A description of the axiom. Has no semantic meaning; for convenience
-- only.
[axiom_name] :: Axiom f -> !String
-- | The equation which the axiom asserts.
[axiom_eqn] :: Axiom f -> !Equation f
-- | Checks a Derivation and, if it is correct, returns a certified
-- Proof.
--
-- If the Derivation is incorrect, throws an exception.
certify :: Function f => Derivation f -> Proof f
equation :: Proof f -> Equation f
derivation :: Proof f -> Derivation f
lemma :: Proof f -> Subst f -> Derivation f
autoSubst :: Equation f -> Subst f
simpleLemma :: Function f => Proof f -> Derivation f
axiom :: Axiom f -> Derivation f
symm :: Derivation f -> Derivation f
trans :: Derivation f -> Derivation f -> Derivation f
cong :: Fun f -> [Derivation f] -> Derivation f
-- | Applies a derivation at a particular path in a term.
congPath :: [Int] -> Term f -> Derivation f -> Derivation f
-- | Simplify a derivation so that: * Symm occurs innermost * Trans is
-- right-associated * Each Cong has at least one non-Refl argument * Refl
-- is not used unnecessarily
simplify :: Function f => Derivation f -> Derivation f
-- | 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
steps :: Function f => Derivation f -> [Derivation f]
-- | Find all lemmas which are used in a derivation.
usedLemmas :: Derivation f -> [Proof f]
-- | Find all axioms which are used in a derivation.
usedAxioms :: Derivation f -> [Axiom f]
-- | Find all lemmas which are used in a derivation, together with the
-- substitutions used.
usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
-- | Find all axioms which are used in a derivation, together with the
-- substitutions used.
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]
-- | Find all ground instances of axioms which are used in the expanded
-- form of a derivation (no lemmas).
groundAxiomsAndSubsts :: Function f => Derivation f -> Map (Axiom f) (Set (Subst f))
eliminateDefinitions :: Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitionsFromGoal :: Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f
-- | Options for proof presentation.
data Config f
Config :: !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> (Axiom f -> Bool) -> Config f
-- | Never inline lemmas.
[cfg_all_lemmas] :: Config f -> !Bool
-- | Inline all lemmas.
[cfg_no_lemmas] :: Config f -> !Bool
-- | Make the proof ground.
[cfg_ground_proof] :: Config f -> !Bool
-- | Print out explicit substitutions.
[cfg_show_instances] :: Config f -> !Bool
-- | Print out proofs in colour.
[cfg_use_colour] :: Config f -> !Bool
-- | Print out which instances of some axioms were used.
[cfg_show_uses_of_axioms] :: Config f -> Axiom f -> Bool
-- | The default configuration.
defaultConfig :: Config f
-- | A proof, with all axioms and lemmas explicitly listed.
data Presentation f
Presentation :: [Axiom f] -> [Proof f] -> [ProvedGoal f] -> Presentation f
-- | The used axioms.
[pres_axioms] :: Presentation f -> [Axiom f]
-- | The used lemmas.
[pres_lemmas] :: Presentation f -> [Proof f]
-- | The goals proved.
[pres_goals] :: Presentation f -> [ProvedGoal f]
data ProvedGoal f
ProvedGoal :: Int -> String -> Proof f -> Equation f -> Subst f -> ProvedGoal f
[pg_number] :: ProvedGoal f -> Int
[pg_name] :: ProvedGoal f -> String
[pg_proof] :: ProvedGoal f -> Proof f
[pg_goal_hint] :: ProvedGoal f -> Equation f
[pg_witness_hint] :: ProvedGoal f -> Subst f
-- | Construct a ProvedGoal.
provedGoal :: Int -> String -> Proof f -> ProvedGoal f
-- | Check that pg_goal/pg_witness match up with pg_proof.
checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f
-- | Print a presented proof.
pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
-- | Simplify and present a proof.
present :: Function f => Config f -> [ProvedGoal f] -> Presentation f
-- | Format an equation nicely.
--
-- Used both here and in the main file.
describeEquation :: Function f => String -> String -> Maybe String -> Equation f -> Doc
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Proof.Axiom f)
instance GHC.Classes.Ord (Twee.Proof.Axiom f)
instance GHC.Classes.Eq (Twee.Proof.Axiom f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Proof.Proof f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Proof.Derivation f)
instance GHC.Classes.Eq (Twee.Proof.Derivation f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Proof.ProvedGoal f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Proof.Presentation f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Presentation f)
instance GHC.Classes.Eq (Twee.Proof.Proof f)
instance GHC.Classes.Ord (Twee.Proof.Proof f)
instance Twee.Base.Symbolic (Twee.Proof.Derivation f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Proof f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Derivation f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Axiom f)
-- | Term rewriting.
module Twee.Rule
-- | A rewrite rule.
data Rule f
Rule :: Orientation f -> !Proof f -> {-# UNPACK #-} !Term f -> {-# UNPACK #-} !Term f -> Rule f
-- | Information about whether and how the rule is oriented.
[orientation] :: Rule f -> Orientation f
-- | A proof that the rule holds.
[rule_proof] :: Rule f -> !Proof f
-- | The left-hand side of the rule.
[lhs] :: Rule f -> {-# UNPACK #-} !Term f
-- | The right-hand side of the rule.
[rhs] :: Rule f -> {-# UNPACK #-} !Term f
type RuleOf a = Rule (ConstantOf a)
ruleDerivation :: Rule f -> Derivation f
-- | A rule's orientation.
--
-- Oriented and WeaklyOriented rules are used only
-- left-to-right. Permutative and Unoriented rules are used
-- bidirectionally.
data Orientation f
-- | An oriented rule.
Oriented :: Orientation f
-- | A weakly oriented rule. The first argument is the minimal constant,
-- the second argument is a list of terms which are weakly oriented in
-- the rule.
--
-- A rule with orientation WeaklyOriented k ts can be
-- used unless all terms in ts are equal to k.
WeaklyOriented :: {-# UNPACK #-} !Fun f -> [Term f] -> Orientation f
-- | A permutative rule.
--
-- A rule with orientation Permutative ts can be used if
-- map fst ts is lexicographically greater than map snd
-- ts.
Permutative :: [(Term f, Term f)] -> Orientation f
-- | An unoriented rule.
Unoriented :: Orientation f
-- | Is a rule oriented or weakly oriented?
oriented :: Orientation f -> Bool
-- | Turn a rule into an equation.
unorient :: Rule f -> Equation f
-- | Turn an equation t :=: u into a rule t -> u by computing the
-- orientation info (e.g. oriented, permutative or unoriented).
--
-- Crashes if either t < u, or there is a variable in
-- u which is not in t. To avoid this problem, combine
-- with split.
orient :: Function f => Equation f -> Proof f -> Rule f
-- | Flip an unoriented rule so that it goes right-to-left.
backwards :: Rule f -> Rule f
-- | Compute the normal form of a term wrt only oriented rules.
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-- | Compute the normal form of a term wrt only oriented rules, using
-- outermost reduction.
simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-- | Compute the normal form of a term wrt only oriented rules, using
-- innermost reduction.
simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-- | Find a simplification step that applies to a term.
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)
-- | A strategy gives a set of possible reductions for a term.
type Strategy f = Term f -> [Reduction f]
-- | A reduction proof is just a sequence of rewrite steps, stored as a
-- list in reverse order. In each rewrite step, all subterms that are
-- exactly equal to the LHS of the rule are replaced by the RHS, i.e. the
-- rewrite step is performed as a parallel rewrite without matching.
type Reduction f = [Rule f]
-- | Transitivity for reduction sequences.
trans :: Reduction f -> Reduction f -> Reduction f
-- | Compute the final term resulting from a reduction, given the starting
-- term.
result :: Term f -> Reduction f -> Term f
-- | Turn a reduction into a proof.
reductionProof :: Function f => Term f -> Reduction f -> Derivation f
ruleResult :: Term f -> Rule f -> Term f
ruleProof :: Function f => Term f -> Rule f -> Derivation f
-- | Normalise a term wrt a particular strategy.
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
-- | Compute all normal forms of a set of terms wrt a particular strategy.
normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
-- | 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 -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successorsAndNormalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f))
-- | Apply a strategy anywhere in a term.
anywhere :: Strategy f -> Strategy f
-- | Apply a strategy anywhere in a term, preferring outermost reductions.
anywhereOutermost :: Strategy f -> Strategy f
-- | Apply a strategy anywhere in a term, preferring innermost reductions.
anywhereInnermost :: Strategy f -> Strategy f
-- | A strategy which rewrites using an index.
rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
-- | A strategy which applies one rule only.
tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
-- | Check if a rule can be applied, given an ordering <= on terms.
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
-- | Check if a rule can be applied normally.
reduces :: Function f => Rule f -> Subst f -> Bool
-- | Check if a rule can be applied and is oriented.
reducesOriented :: Function f => Rule f -> Subst f -> Bool
-- | Check if a rule can be applied in a particular model.
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool
-- | Check if a rule can be applied to the Skolemised version of a term.
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Rule.Orientation f)
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Rule.Rule f)
instance GHC.Classes.Eq (Twee.Rule.Rule f)
instance GHC.Classes.Ord (Twee.Rule.Rule f)
instance (f GHC.Types.~ g) => Twee.Base.Has (Twee.Rule.Rule f) (Twee.Rule.Rule g)
instance Twee.Base.Symbolic (Twee.Rule.Rule f)
instance (f GHC.Types.~ g) => Twee.Base.Has (Twee.Rule.Rule f) (Twee.Term.Core.Term g)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Rule f)
instance GHC.Classes.Eq (Twee.Rule.Orientation f)
instance GHC.Classes.Ord (Twee.Rule.Orientation f)
instance Twee.Base.Symbolic (Twee.Rule.Orientation f)
module Twee.Rule.Index
data RuleIndex f a
RuleIndex :: !Index f a -> !Index f a -> RuleIndex f a
[index_oriented] :: RuleIndex f a -> !Index f a
[index_all] :: RuleIndex f a -> !Index f a
empty :: RuleIndex f a
insert :: forall f a. (Symbolic a, ConstantOf a ~ f, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a
delete :: forall f a. (Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a
-- | Look up a term in the index. Like lookup, but returns the exact
-- value that was inserted into the index, not an instance. Also returns
-- a substitution which when applied to the value gives you the matching
-- instance.
matches :: Term f -> Index f a -> [(Subst f, a)]
-- | Look up a term in the index. Finds all key-value such that the search
-- term is an instance of the key, and returns an instance of the the
-- value which makes the search term exactly equal to the key.
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]
instance (Twee.Term.Labelled f, GHC.Show.Show f, GHC.Show.Show a) => GHC.Show.Show (Twee.Rule.Index.RuleIndex f a)
-- | An implementation of Knuth-Bendix ordering.
module Twee.KBO
-- | Check if one term is less than another in KBO.
lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
-- | Check if one term is less than another in a given model.
lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
class Sized a
-- | Compute the size.
size :: Sized a => a -> Integer
class Weighted f
argWeight :: Weighted f => f -> Integer
instance (Twee.KBO.Weighted f, Twee.Term.Labelled f) => Twee.KBO.Weighted (Twee.Term.Core.Fun f)
instance (Twee.Term.Labelled f, Twee.KBO.Sized f, Twee.KBO.Weighted f) => Twee.KBO.Sized (Twee.Term.Core.TermList f)
instance (Twee.Term.Labelled f, Twee.KBO.Sized f, Twee.KBO.Weighted f) => Twee.KBO.Sized (Twee.Term.Core.Term f)
instance (Twee.Term.Labelled f, Twee.KBO.Sized f, Twee.KBO.Weighted f) => Twee.KBO.Sized (Twee.Equation.Equation f)
instance (Twee.Term.Labelled f, Twee.KBO.Sized f) => Twee.KBO.Sized (Twee.Term.Core.Fun f)
-- | Critical pair generation.
module Twee.CP
-- | The set of positions at which a term can have critical overlaps.
data Positions f
NilP :: Positions f
ConsP :: {-# UNPACK #-} !Int -> !Positions f -> Positions f
type PositionsOf a = Positions (ConstantOf a)
-- | Like Positions but for an equation (one set of positions per term).
data Positions2 f
ForwardsPos :: !Positions f -> Positions2 f
BothPos :: !Positions f -> !Positions f -> Positions2 f
-- | Calculate the set of positions for a term.
positions :: Term f -> Positions f
-- | Calculate the set of positions for a rule.
positionsRule :: Rule f -> Positions2 f
positionsChurch :: Positions f -> ChurchList Int
-- | A critical overlap of one rule with another.
data Overlap a f
Overlap :: !a -> !a -> {-# UNPACK #-} !How -> {-# UNPACK #-} !Term f -> {-# UNPACK #-} !Equation f -> Overlap a f
-- | The rule which applies at the root.
[overlap_rule1] :: Overlap a f -> !a
-- | The rule which applies at some subterm.
[overlap_rule2] :: Overlap a f -> !a
-- | The position in the critical term which is rewritten.
[overlap_how] :: Overlap a f -> {-# UNPACK #-} !How
-- | The top term of the critical pair
[overlap_top] :: Overlap a f -> {-# UNPACK #-} !Term f
-- | The critical pair itself.
[overlap_eqn] :: Overlap a f -> {-# UNPACK #-} !Equation f
data Direction
Forwards :: Direction
Backwards :: Direction
direct :: Rule f -> Direction -> Rule f
data How
How :: !Direction -> !Direction -> {-# UNPACK #-} !Int -> How
[how_dir1] :: How -> !Direction
[how_dir2] :: How -> !Direction
[how_pos] :: How -> {-# UNPACK #-} !Int
packHow :: How -> Int
unpackHow :: Int -> How
-- | Represents the depth of a critical pair.
newtype Depth
Depth :: Int -> Depth
-- | Compute all overlaps of a rule with a set of rules.
overlaps :: forall a b f. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => Index f a -> [b] -> b -> [Overlap b f]
overlapsChurch :: forall f a b. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => Index f a -> [b] -> b -> ChurchList (Overlap b f)
directions :: Rule f -> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
asymmetricOverlaps :: (Function f, Has a (Rule f)) => Index f a -> b -> b -> Direction -> Direction -> Positions f -> Equation f -> Equation f -> ChurchList (Overlap b f)
-- | Create an overlap at a particular position in a term. Doesn't simplify
-- the overlap.
overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
-- | Simplify an overlap and remove it if it's trivial.
simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap b f -> Maybe (Overlap b f)
buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
termSubst :: TriangleSubst f -> Term f -> Term f
-- | The configuration for the critical pair weighting heuristic.
data Config
Config :: !Int -> !Int -> !Int -> !Int -> !Int -> !Int -> !Int -> Config
[cfg_lhsweight] :: Config -> !Int
[cfg_rhsweight] :: Config -> !Int
[cfg_funweight] :: Config -> !Int
[cfg_varweight] :: Config -> !Int
[cfg_depthweight] :: Config -> !Int
[cfg_dupcost] :: Config -> !Int
[cfg_dupfactor] :: Config -> !Int
-- | The default heuristic configuration.
defaultConfig :: Config
-- | Compute a score for a critical pair.
score :: Function f => Config -> Depth -> Overlap a f -> Int
-- | A critical pair together with information about how it was derived
data CriticalPair f
CriticalPair :: {-# UNPACK #-} !Equation f -> !Maybe (Term f) -> !Derivation f -> CriticalPair f
-- | The critical pair itself.
[cp_eqn] :: CriticalPair f -> {-# UNPACK #-} !Equation f
-- | The critical term, if there is one. (Axioms do not have a critical
-- term.)
[cp_top] :: CriticalPair f -> !Maybe (Term f)
-- | A derivation of the critical pair from the axioms.
[cp_proof] :: CriticalPair f -> !Derivation f
-- | Split a critical pair so that it can be turned into rules.
--
-- The resulting critical pairs have the property that no variable
-- appears on the right that is not on the left.
split :: Function f => CriticalPair f -> [CriticalPair f]
-- | Make a critical pair from two rules and an overlap.
makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f
instance GHC.Show.Show Twee.CP.Direction
instance GHC.Enum.Enum Twee.CP.Direction
instance GHC.Classes.Eq Twee.CP.Direction
instance GHC.Show.Show Twee.CP.How
instance (Twee.Term.Labelled f, GHC.Show.Show a, GHC.Show.Show f) => GHC.Show.Show (Twee.CP.Overlap a f)
instance GHC.Show.Show Twee.CP.Depth
instance GHC.Real.Integral Twee.CP.Depth
instance GHC.Enum.Enum Twee.CP.Depth
instance GHC.Real.Real Twee.CP.Depth
instance GHC.Num.Num Twee.CP.Depth
instance GHC.Classes.Ord Twee.CP.Depth
instance GHC.Classes.Eq Twee.CP.Depth
instance Twee.Base.Symbolic (Twee.CP.CriticalPair f)
instance (Twee.Term.Labelled f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.CP.CriticalPair f)
instance GHC.Show.Show (Twee.CP.Positions f)
-- | Tactics for joining critical pairs.
module Twee.Join
data Config
Config :: !Bool -> !Bool -> !Bool -> !Bool -> Config
[cfg_ground_join] :: Config -> !Bool
[cfg_use_connectedness_standalone] :: Config -> !Bool
[cfg_use_connectedness_in_ground_joining] :: Config -> !Bool
[cfg_set_join] :: Config -> !Bool
defaultConfig :: Config
joinCriticalPair :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> CriticalPair f -> Either (CriticalPair f, Model f) (Maybe (CriticalPair f), [CriticalPair f])
step1 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
step2 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
step3 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
allSteps :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
checkOrder :: Function f => CriticalPair f -> Maybe (CriticalPair f)
joinWith :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> (Term f -> Term f -> Reduction f) -> CriticalPair f -> Maybe (CriticalPair f)
subsumed :: (Has a (Rule f), Function f) => (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Equation f -> Bool
subsumed1 :: Has a (Rule f) => Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
groundJoin :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFrom :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFromMaybe :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
valid :: Function f => Model f -> Reduction f -> Bool
optimise :: (a -> [a]) -> (a -> Bool) -> a -> a
-- | The main prover loop.
module Twee
-- | The prover configuration.
data Config f
Config :: Maybe (Term f -> Bool) -> Int64 -> Int -> Bool -> Int -> Int -> Int -> Bool -> Bool -> Bool -> Config -> Config -> Config f -> Config f
[cfg_accept_term] :: Config f -> Maybe (Term f -> Bool)
[cfg_max_critical_pairs] :: Config f -> Int64
[cfg_max_cp_depth] :: Config f -> Int
[cfg_simplify] :: Config f -> Bool
[cfg_renormalise_percent] :: Config f -> Int
[cfg_cp_sample_size] :: Config f -> Int
[cfg_renormalise_threshold] :: Config f -> Int
[cfg_set_join_goals] :: Config f -> Bool
[cfg_always_simplify] :: Config f -> Bool
[cfg_complete_subsets] :: Config f -> Bool
[cfg_critical_pairs] :: Config f -> Config
[cfg_join] :: Config f -> Config
[cfg_proof_presentation] :: Config f -> Config f
-- | The prover state.
data State f
State :: !RuleIndex f (Rule f) -> !IntMap (Active f) -> !Index f (Equation f) -> ![Goal f] -> !Queue Params -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int64 -> {-# UNPACK #-} !Id -> !Sample (Maybe (Overlap (Active f) f)) -> !IntSet -> !Index f (Rule f) -> ![Message f] -> State f
[st_rules] :: State f -> !RuleIndex f (Rule f)
[st_active_set] :: State f -> !IntMap (Active f)
[st_joinable] :: State f -> !Index f (Equation f)
[st_goals] :: State f -> ![Goal f]
[st_queue] :: State f -> !Queue Params
[st_next_active] :: State f -> {-# UNPACK #-} !Id
[st_considered] :: State f -> {-# UNPACK #-} !Int64
[st_simplified_at] :: State f -> {-# UNPACK #-} !Id
[st_cp_sample] :: State f -> !Sample (Maybe (Overlap (Active f) f))
[st_not_complete] :: State f -> !IntSet
[st_complete] :: State f -> !Index f (Rule f)
[st_messages_rev] :: State f -> ![Message f]
-- | The default prover configuration.
defaultConfig :: Config f
-- | Does this configuration run the prover in a complete mode?
configIsComplete :: Config f -> Bool
-- | The initial state.
initialState :: Config f -> State f
-- | A message which is produced by the prover when something interesting
-- happens.
data Message f
-- | A new rule.
NewActive :: !Active f -> Message f
-- | A new joinable equation.
NewEquation :: !Equation f -> Message f
-- | A rule was deleted.
DeleteActive :: !Active f -> Message f
-- | The CP queue was simplified.
SimplifyQueue :: Message f
-- | All except these axioms are complete (with a suitable-chosen subset of
-- the rules).
NotComplete :: !IntSet -> Message f
-- | The rules were reduced wrt each other.
Interreduce :: Message f
-- | Status update: how many queued critical pairs there are.
Status :: !Int -> Message f
-- | Emit a message.
message :: PrettyTerm f => Message f -> State f -> State f
-- | Forget about all emitted messages.
clearMessages :: State f -> State f
-- | Get all emitted messages.
messages :: State f -> [Message f]
data Params
-- | Compute all critical pairs from a rule.
makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params]
makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params
-- | Turn a Passive back into an overlap. Doesn't try to simplify it.
findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (Overlap (Active f) f)
-- | Renormalise a queued Passive.
simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)
-- | Check if we should renormalise the queue.
shouldSimplifyQueue :: Function f => Config f -> State f -> Bool
-- | Renormalise the entire queue.
simplifyQueue :: Function f => Config f -> State f -> State f
-- | Enqueue a set of critical pairs.
enqueue :: Function f => State f -> Id -> [Passive Params] -> State f
-- | Dequeue a critical pair.
--
-- Also takes care of:
--
--
-- - removing any orphans from the head of the queue
-- - ignoring CPs that are too big
--
dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
data Active f
Active :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Info -> {-# UNPACK #-} !Rule f -> !Maybe (Term f) -> {-# UNPACK #-} !Proof f -> !Model f -> !Positions2 f -> Active f
[active_id] :: Active f -> {-# UNPACK #-} !Id
[active_info] :: Active f -> {-# UNPACK #-} !Info
[active_rule] :: Active f -> {-# UNPACK #-} !Rule f
[active_top] :: Active f -> !Maybe (Term f)
[active_proof] :: Active f -> {-# UNPACK #-} !Proof f
[active_model] :: Active f -> !Model f
[active_positions] :: Active f -> !Positions2 f
active_cp :: Active f -> CriticalPair f
activeRules :: Active f -> [Rule f]
data Info
Info :: {-# UNPACK #-} !Depth -> !IntSet -> Info
[info_depth] :: Info -> {-# UNPACK #-} !Depth
[info_max] :: Info -> !IntSet
addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f
sample :: Function f => Int -> [Passive Params] -> State f -> State f
resetSample :: Function f => Config f -> State f -> State f
simplifySample :: Function f => State f -> State f
addActiveOnly :: Function f => State f -> Active f -> State f
deleteActive :: Function f => State f -> Active f -> State f
consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing :: Function f => RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f
addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
addJoinable :: Function f => State f -> Equation f -> State f
checkCompleteness :: Function f => Config f -> State f -> State f
assumeComplete :: Function f => State f -> State f
data Goal f
Goal :: String -> Int -> Equation f -> Map (Term f) (Derivation f) -> Map (Term f) (Derivation f) -> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Term f, Reduction f) -> Goal f
[goal_name] :: Goal f -> String
[goal_number] :: Goal f -> Int
[goal_eqn] :: Goal f -> Equation f
[goal_expanded_lhs] :: Goal f -> Map (Term f) (Derivation f)
[goal_expanded_rhs] :: Goal f -> Map (Term f) (Derivation f)
[goal_lhs] :: Goal f -> Map (Term f) (Term f, Reduction f)
[goal_rhs] :: Goal f -> Map (Term f) (Term f, Reduction f)
addGoal :: Function f => Config f -> State f -> Goal f -> State f
normaliseGoals :: Function f => Config f -> State f -> State f
recomputeGoals :: Function f => Config f -> State f -> State f
resetGoal :: Goal f -> Goal f
rewriteGoalsBackwards :: Function f => State f -> State f
goal :: Int -> String -> Equation f -> Goal f
interreduce :: Function f => Config f -> State f -> State f
interreduce1 :: Function f => Config f -> State f -> Active f -> State f
data Output m f
Output :: (Message f -> m ()) -> Output m f
[output_message] :: Output m f -> Message f -> m ()
complete :: (Function f, MonadIO m) => Output m f -> Config f -> State f -> m (State f)
complete1 :: Function f => Config f -> State f -> (Bool, State f)
solved :: Function f => State f -> Bool
solutions :: Function f => State f -> [ProvedGoal f]
rules :: Function f => State f -> [Rule f]
completePure :: Function f => Config f -> State f -> State f
normaliseTerm :: Function f => State f -> Term f -> Reduction f
normalForms :: Function f => State f -> Term f -> Map (Term f) (Reduction f)
simplifyTerm :: Function f => State f -> Term f -> Term f
instance (Twee.Term.Labelled f, GHC.Show.Show f) => GHC.Show.Show (Twee.Goal f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Message f)
instance GHC.Classes.Eq (Twee.Active f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Active f)
instance Twee.Base.Has (Twee.Active f) Twee.Base.Id
instance Twee.Base.Has (Twee.Active f) Twee.CP.Depth
instance (f GHC.Types.~ g) => Twee.Base.Has (Twee.Active f) (Twee.Rule.Rule g)
instance (f GHC.Types.~ g) => Twee.Base.Has (Twee.Active f) (Twee.CP.Positions2 g)
instance Twee.PassiveQueue.Params Twee.Params