twee-lib-2.4.2: An equational theorem prover

Twee.CP

Description

Critical pair generation.

Synopsis

Documentation

data Positions f Source #

The set of positions at which a term can have critical overlaps.

Constructors

 NilP ConsP !Int !(Positions f)

Instances

Instances details
 Source # Instance detailsDefined in Twee.CP MethodsshowsPrec :: Int -> Positions f -> ShowS #show :: Positions f -> String #showList :: [Positions f] -> ShowS #

data Positions2 f Source #

Like Positions but for an equation (one set of positions per term).

Constructors

 ForwardsPos !(Positions f) BothPos !(Positions f) !(Positions f)

Instances

Instances details
 f ~ g => Has (Active f) (Positions2 g) Source # Instance detailsDefined in Twee Methodsthe :: Active f -> Positions2 g Source #

Calculate the set of positions for a term.

Calculate the set of positions for a rule.

positionsChurch :: Positions f -> ChurchList Int Source #

data Overlap a f Source #

A critical overlap of one rule with another.

Constructors

 Overlap Fieldsoverlap_rule1 :: !aThe rule which applies at the root.overlap_rule2 :: !aThe rule which applies at some subterm.overlap_how :: !HowThe position in the critical term which is rewritten, together with the direction of the two rules.overlap_top :: !(Term f)The top term of the critical pairoverlap_eqn :: !(Equation f)The critical pair itself.

Instances

Instances details
 (Labelled f, Show a, Show f) => Show (Overlap a f) Source # Instance detailsDefined in Twee.CP MethodsshowsPrec :: Int -> Overlap a f -> ShowS #show :: Overlap a f -> String #showList :: [Overlap a f] -> ShowS #

data How Source #

Constructors

 How Fieldshow_pos :: !Int how_dir1 :: !Direction how_dir2 :: !Direction

Instances

Instances details
 Source # Instance detailsDefined in Twee.CP MethodsshowsPrec :: Int -> How -> ShowS #show :: How -> String #showList :: [How] -> ShowS # Source # Instance detailsDefined in Twee.CP Methods Source # Instance detailsDefined in Twee.CP Methods(==) :: How -> How -> Bool #(/=) :: How -> How -> Bool # Source # Instance detailsDefined in Twee.CP Methodscompare :: How -> How -> Ordering #(<) :: How -> How -> Bool #(<=) :: How -> How -> Bool #(>) :: How -> How -> Bool #(>=) :: How -> How -> Bool #max :: How -> How -> How #min :: How -> How -> How #

data Direction Source #

Constructors

 Forwards Backwards

Instances

Instances details
 Source # Instance detailsDefined in Twee.CP MethodsenumFrom :: Direction -> [Direction] # Source # Instance detailsDefined in Twee.CP MethodsshowList :: [Direction] -> ShowS # Source # Instance detailsDefined in Twee.CP Methods Source # Instance detailsDefined in Twee.CP Methods

newtype Depth Source #

Represents the depth of a critical pair.

Constructors

 Depth Int

Instances

Instances details
 Source # Instance detailsDefined in Twee.CP Methodssucc :: Depth -> Depth #pred :: Depth -> Depth #toEnum :: Int -> Depth #enumFrom :: Depth -> [Depth] #enumFromThen :: Depth -> Depth -> [Depth] #enumFromTo :: Depth -> Depth -> [Depth] #enumFromThenTo :: Depth -> Depth -> Depth -> [Depth] # Source # Instance detailsDefined in Twee.CP Methods(+) :: Depth -> Depth -> Depth #(-) :: Depth -> Depth -> Depth #(*) :: Depth -> Depth -> Depth #abs :: Depth -> Depth # Source # Instance detailsDefined in Twee.CP Methodsquot :: Depth -> Depth -> Depth #rem :: Depth -> Depth -> Depth #div :: Depth -> Depth -> Depth #mod :: Depth -> Depth -> Depth #quotRem :: Depth -> Depth -> (Depth, Depth) #divMod :: Depth -> Depth -> (Depth, Depth) # Source # Instance detailsDefined in Twee.CP Methods Source # Instance detailsDefined in Twee.CP MethodsshowsPrec :: Int -> Depth -> ShowS #show :: Depth -> String #showList :: [Depth] -> ShowS # Source # Instance detailsDefined in Twee.CP Methods(==) :: Depth -> Depth -> Bool #(/=) :: Depth -> Depth -> Bool # Source # Instance detailsDefined in Twee.CP Methods(<) :: Depth -> Depth -> Bool #(<=) :: Depth -> Depth -> Bool #(>) :: Depth -> Depth -> Bool #(>=) :: Depth -> Depth -> Bool #max :: Depth -> Depth -> Depth #min :: Depth -> Depth -> Depth # Source # Instance detailsDefined in Twee Methodsthe :: Active f -> Depth Source #

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] Source #

Compute all overlaps of a rule with a set of rules.

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) Source #

directions :: Rule f -> Positions2 f -> ChurchList (Direction, Positions f, Equation f) Source #

asymmetricOverlaps :: (Function f, Has a (Rule f)) => Index f a -> b -> b -> Direction -> Direction -> Positions f -> Equation f -> Equation f -> ChurchList (Overlap b f) Source #

overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f) Source #

Create an overlap at a particular position in a term. Doesn't simplify the overlap.

overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f) Source #

simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap b f -> Maybe (Overlap b f) Source #

Simplify an overlap and remove it if it's trivial.

data Config Source #

The configuration for the critical pair weighting heuristic.

Constructors

 Config Fieldscfg_lhsweight :: !Int cfg_rhsweight :: !Int cfg_funweight :: !Int cfg_varweight :: !Int cfg_depthweight :: !Int cfg_dupcost :: !Int cfg_dupfactor :: !Int

The default heuristic configuration.

score :: Function f => Config -> Depth -> Overlap a f -> Int Source #

Compute a score for a critical pair.

Higher-level handling of critical pairs.

data CriticalPair f Source #

A critical pair together with information about how it was derived

Constructors

 CriticalPair Fieldscp_eqn :: !(Equation f)The critical pair itself.cp_top :: !(Maybe (Term f))The critical term, if there is one. (Axioms do not have a critical term.)cp_proof :: !(Derivation f)A derivation of the critical pair from the axioms.

Instances

Instances details
 (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) Source # Instance detailsDefined in Twee.CP MethodspPrint :: CriticalPair f -> Doc #pPrintList :: PrettyLevel -> [CriticalPair f] -> Doc # Source # Instance detailsDefined in Twee.CP Associated Types Methodssubst_ :: (Var -> BuilderOf (CriticalPair f)) -> CriticalPair f -> CriticalPair f Source # type ConstantOf (CriticalPair f) Source # Instance detailsDefined in Twee.CP type ConstantOf (CriticalPair f) = f

split :: Function f => CriticalPair f -> [CriticalPair f] Source #

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.

makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f Source #

Make a critical pair from two rules and an overlap.