Module Monome.Focus

Focus on a specific term

type 'a t = {
term : term;
coeff : 'a;

Never 0

rest : 'a monome;
}
val get : 'a monome -> int -> 'a t
raises Invalid_argument

if the index is invalid

val focus_term : 'a monome -> term -> 'a t option

Focus on the given term, if it is one of the members of the given monome.

val focus_term_exn : 'a monome -> term -> 'a t

Same as focus_term, but

raises Failure

on failure

val to_monome : 'a t -> 'a monome

Conversion back to an unfocused monome

val coeff : 'a t -> 'a
val term : 'a t -> term
val rest : 'a t -> 'a monome
val sum : 'a t -> 'a monome -> 'a t
val difference : 'a t -> 'a monome -> 'a t
val uminus : 'a t -> 'a t
val product : 'a t -> 'a -> 'a t
raises Invalid_argument

if the number is 0

val map : ?⁠term:(term -> term) -> ?⁠coeff:('a -> 'a) -> ?⁠rest:('a monome -> 'a monome) -> 'a t -> 'a t
val scale : 'a t -> 'a t -> 'a t * 'a t

Scale to the same coefficient

val is_max : ord:Ordering.t -> _ t -> bool

Is the focused term maximal in the monome?

val fold_m : pos:Position.t -> 'a monome -> 'b -> ('b -> 'a t -> Position.t -> 'b) -> 'b

Fold on terms of the given monome, focusing on them one by one, along with the position of the focused term

val apply_subst : Subst.Renaming.t -> Subst.t -> 'a t Scoped.t -> 'a t

Apply a substitution. This can modify the set of terms in rest because some of them may become equal to the focused term.

val unify_ff : ?⁠subst:Unif_subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> ('a t * 'a t * Unif_subst.t) Sequence.t

Unify two focused monomes. All returned unifiers are unifiers of the focused terms, but maybe also of other unfocused terms; Focused monomes are modified by unification because several terms might merge with the focused term, so the new ones are returned with the unifier itself

val unify_mm : ?⁠subst:Unif_subst.t -> 'a monome Scoped.t -> 'a monome Scoped.t -> ('a t * 'a t * Unif_subst.t) Sequence.t

Unify parts of two monomes m1 and m2. For each such unifier we return the versions of m1 and m2 where the unified terms are focused.

val unify_self : ?⁠subst:Unif_subst.t -> 'a t Scoped.t -> ('a t * Unif_subst.t) Sequence.t

Extend the substitution to other terms within the focused monome, if possible. For instance it might return 2f(x)+a, {x=y} for the monome f(x)+f(y)+a where f(x) is focused.

val unify_self_monome : ?⁠subst:Unif_subst.t -> 'a monome Scoped.t -> ('a t * Unif_subst.t) Sequence.t

Unify at least two terms of the monome together

val pp : _ t CCFormat.printer