Module Int_lit.Focus
type t
=
|
Left of op * Z.t Monome.Focus.t * Z.t Monome.t
|
Right of op * Z.t Monome.t * Z.t Monome.Focus.t
|
Div of Z.t Monome.Focus.t divides
focus on a term in one of the two monomes
val mk_left : op -> Z.t Monome.Focus.t -> Z.t Monome.t -> t
val mk_right : op -> Z.t Monome.t -> Z.t Monome.Focus.t -> t
val mk_div : ?sign:bool -> Z.t -> power:int -> Z.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 -> Z.t Monome.t -> lit
replace a m
replacesmf.coeff × mf.term
withm
wheremf
is the focused monome ina
, and return the resulting literal
val focused_monome : t -> Z.t Monome.Focus.t
The focused monome
val opposite_monome_exn : t -> Z.t Monome.t
Unsafe version of
opposite_monome
.- raises Invalid_argument
if the literal is a
Div
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:(Z.t Monome.t -> Z.t Monome.t) -> f_mf:(Z.t Monome.Focus.t -> Z.t Monome.Focus.t) -> t -> t
Apply a function to the monomes and focused monomes
val scale : t -> t -> t * t
Multiply the two literals by some constant so that their focused literals have the same coefficient
val scale_power : t -> int -> t
For a "divides" literal, bring it to the given power.
- raises Invalid_argument
if the current power is strictly greater than the argument (cannot scale down), or if the literal is not a
Div
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