package logtk

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

Module Monome.FocusSource

Focus on a specific term

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

    Never 0

    *)
  3. rest : 'a monome;
}
Sourceval get : 'a monome -> int -> 'a t
Sourceval focus_term : 'a monome -> term -> 'a t option

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

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

Same as focus_term, but

Sourceval to_monome : 'a t -> 'a monome

Conversion back to an unfocused monome

Sourceval coeff : 'a t -> 'a
Sourceval term : 'a t -> term
Sourceval rest : 'a t -> 'a monome
Sourceval sum : 'a t -> 'a monome -> 'a t
Sourceval difference : 'a t -> 'a monome -> 'a t
Sourceval uminus : 'a t -> 'a t
Sourceval product : 'a t -> 'a -> 'a t
Sourceval map : ?term:(term -> term) -> ?coeff:('a -> 'a) -> ?rest:('a monome -> 'a monome) -> 'a t -> 'a t
Sourceval scale : 'a t -> 'a t -> 'a t * 'a t

Scale to the same coefficient

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

Is the focused term maximal in the monome?

Sourceval 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

Sourceval 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.

Sourceval 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

Sourceval 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.

Sourceval 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.

Sourceval 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