Module Monome.Focus

module Focus: sig .. end

Focus on a specific term

type 'a t = {

`term : Monome.term;`
`coeff : 'a;`	`(*`	Never 0	`*)`
`rest : 'a Monome.monome;`

}

val get : 'a Monome.monome -> int -> 'a t

Raises Invalid_argument if the index is invalid

val focus_term : 'a Monome.monome -> 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.monome -> Monome.term -> 'a t

Same as Monome.Focus.focus_term, but
Raises Failure on failure

val to_monome : 'a t -> 'a Monome.monome

Conversion back to an unfocused monome

val coeff : 'a t -> 'a

val term : 'a t -> Monome.term

val rest : 'a t -> 'a Monome.monome

val sum : 'a t -> 'a Monome.monome -> 'a t

val difference : 'a t -> 'a Monome.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:(Monome.term -> Monome.term) ->
       ?coeff:('a -> 'a) ->
       ?rest:('a Monome.monome -> 'a Monome.monome) ->
       'a t -> 'a t

val scale : Z.t t ->
       Z.t t -> Z.t t * Z.t t

Scale to the same coefficient

val is_max : ord:Libzipperposition.Ordering.t -> 'a t -> bool

Is the focused term maximal in the monome?

val fold_m : pos:Libzipperposition.Position.t ->
       'a Monome.monome ->
       'b -> ('b -> 'a t -> Libzipperposition.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 : renaming:Libzipperposition.Substs.Renaming.t ->
       Libzipperposition.Substs.t ->
       'a t Libzipperposition.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 apply_subst_no_renaming : Libzipperposition.Substs.t ->
       'a t Libzipperposition.Scoped.t -> 'a t

Apply a substitution but doesn't rename free variables. Careful with the collisions

Here we don't unify full (focused) monomes together, but only the focused part (and possibly some unfocused terms too) together. For instance, unifying f(x)* + 2a and f(y)* + f(z) + b (where focused terms are starred) will yield both (1,1,x=y) and (1,2,x=y=z) since f(z) becomes focused too.

Again, arith constants are not unifiable with unshielded variables.

val unify_ff : ?subst:Libzipperposition.Substs.t ->
       'a t Libzipperposition.Scoped.t ->
       'a t Libzipperposition.Scoped.t ->
       ('a t * 'a t * Libzipperposition.Substs.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:Libzipperposition.Substs.t ->
       'a Monome.monome Libzipperposition.Scoped.t ->
       'a Monome.monome Libzipperposition.Scoped.t ->
       ('a t * 'a t * Libzipperposition.Substs.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:Libzipperposition.Substs.t ->
       'a t Libzipperposition.Scoped.t ->
       ('a t * Libzipperposition.Substs.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:Libzipperposition.Substs.t ->
       'a Monome.monome Libzipperposition.Scoped.t ->
       ('a t * Libzipperposition.Substs.t) Sequence.t

Unify at least two terms of the monome together

val pp : 'a t CCFormat.printer