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

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

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

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