Module `Rat_lit.Focus`

type t = | Left of op * Q.t Monome.Focus.t * Q.t Monome.t | Right of op * Q.t Monome.t * Q.t Monome.Focus.t: focus on a term in one of the two monomes

val mk_left : op -> Q.t Monome.Focus.t -> Q.t Monome.t -> t

val mk_right : op -> Q.t Monome.t -> Q.t Monome.Focus.t -> t

val get : lit -> Position.t -> t option

val get_exn : lit -> Position.t -> t

raises Invalid_argument: if the position doesn't fit

val focus_term : lit -> term -> t option: Attempt to focus on the given atomic term, if it occurs directly under the arith literal

val focus_term_exn : lit -> term -> t
val 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

val term : t -> term: Focused term

val focused_monome : t -> Q.t Monome.Focus.t: The focused monome

val opposite_monome : t -> Q.t Monome.t: The opposite monome (in Left and Right)

val is_max : ord:Ordering.t -> t -> bool: Is the focused term maximal in the literal?

val is_strictly_max : ord:Ordering.t -> t -> bool: Is the focused term maximal in the literal, ie is it greater than all the othe terms?

val 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

val product : t -> Q.t -> t: Product by a constant

val scale : t -> t -> t * t: Multiply the two literals by some constant so that their focused literals have the same coefficient

val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t: Apply a substitution

val unify : ?⁠subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> (t * t * Unif_subst.t) Sequence.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

val fold_terms : ?⁠pos:Position.t -> lit -> (t * Position.t) Sequence.t: Fold on focused terms in the literal, one by one, with the position of the focused term

val op : t -> op
val unfocus : t -> lit: Conversion back to a literal

val pp : t CCFormat.printer
val to_string : t -> string