Module Rat_lit.FocusSource

Sourcetype t =
  1. | Left of op * Q.t Monome.Focus.t * Q.t Monome.t
  2. | Right of op * Q.t Monome.t * Q.t Monome.Focus.t

focus on a term in one of the two monomes

Sourceval mk_left : op -> Q.t Monome.Focus.t -> Q.t Monome.t -> t
Sourceval mk_right : op -> Q.t Monome.t -> Q.t Monome.Focus.t -> t
Sourceval get : lit -> Position.t -> t option
Sourceval get_exn : lit -> Position.t -> t
Sourceval focus_term : lit -> term -> t option

Attempt to focus on the given atomic term, if it occurs directly under the arith literal

Sourceval focus_term_exn : lit -> term -> t
Sourceval replace : t -> Q.t Monome.t -> lit

replace a m replaces mf.coeff × mf.term with m where mf is the focused monome in a, and return the resulting literal

Sourceval term : t -> term

Focused term

Sourceval focused_monome : t -> Q.t Monome.Focus.t

The focused monome

Sourceval opposite_monome : t -> Q.t Monome.t

The opposite monome (in Left and Right)

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

Is the focused term maximal in the literal?

Sourceval is_strictly_max : ord:Ordering.t -> t -> bool

Is the focused term maximal in the literal, ie is it greater than all the other terms?

Sourceval map_lit : f_m:(Q.t Monome.t -> Q.t Monome.t) -> f_mf:(Q.t Monome.Focus.t -> Q.t Monome.Focus.t) -> t -> t

Apply a function to the monomes and focused monomes

Sourceval product : t -> Q.t -> t

Product by a constant

Sourceval scale : t -> t -> t * t

Multiply the two literals by some constant so that their focused literals have the same coefficient

Sourceval apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t

Apply a substitution

Sourceval unify : ?subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> (t * t * Unif_subst.t) Iter.t

Unify the two focused terms, and possibly other terms of their respective focused monomes; yield the new literals accounting for the unification along with the unifier

Sourceval fold_terms : ?pos:Position.t -> lit -> (t * Position.t) Iter.t

Fold on focused terms in the literal, one by one, with the position of the focused term

Sourceval op : t -> op
Sourceval unfocus : t -> lit

Conversion back to a literal

Sourceval to_string : t -> string