package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Focus on a specific term

type 'a t = {
  1. term : term;
  2. coeff : 'a;
    (*

    Never 0

    *)
  3. 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 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
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.

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:Unif_subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> ('a t * 'a t * Unif_subst.t) Iter.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) Iter.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) Iter.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) Iter.t

Unify at least two terms of the monome together

val pp : _ t CCFormat.printer