Module Solver.Solver_mono

Solver that supports lattices with monotone morphisms between them.

Parameters

Signature

type changes

Represents a sequence of state mutations caused by mode operations. All mutating operations in this module take a log:changes ref option and append to it all changes made, regardless of success or failure. It is option only for performance reasons; the caller should never provide log:None. The caller is responsible for taking care of the appended log: they can either revert the changes using undo_changes, or commit the changes to the global log in types.ml.

val empty_changes : changes

An empty sequence of changes.

val undo_changes : changes -> unit

Undo the sequence of changes recorded.

type ('a, 'd) mode constraint 'd = 'l * 'r

A mode with carrier type 'a and allowance 'd. See Note Allowance in allowance.mli.

include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) mode
type ('a, _, 'd) sided = ('a, 'd) mode
val disallow_right : ('a, 'b, 'l * 'r) sided -> ('a, 'b, 'l * Allowance.disallowed) sided

Disallows on the right.

val disallow_left : ('a, 'b, 'l * 'r) sided -> ('a, 'b, Allowance.disallowed * 'r) sided

Disallows a the left.

val allow_right : ('a, 'b, 'l * Allowance.allowed) sided -> ('a, 'b, 'l * 'r) sided

Generalizes a right-hand-side allowed to be any allowance.

val allow_left : ('a, 'b, Allowance.allowed * 'r) sided -> ('a, 'b, 'l * 'r) sided

Generalizes a left-hand-side allowed to be any allowance.

val of_const : 'a C.obj -> ?hint:('l * 'r) Hint.Const.t -> 'a -> ('a, 'l * 'r) mode

Returns the mode representing the given constant, explained by the optional hint.

val to_const_exn : 'a C.obj -> ('a, Allowance.allowed * Allowance.allowed) mode -> 'a

Given a mode whose lower and upper bounds are equal, returns that bound. Raises exception if the condition does not hold.

val min : 'a C.obj -> ('a, 'l * 'r) mode

The minimum mode in the lattice

val max : 'a C.obj -> ('a, 'l * 'r) mode

The maximum mode in the lattice

val zap_to_floor : 'a C.obj -> ('a, Allowance.allowed * 'r) mode -> log:changes ref option -> 'a

Pushes the mode variable to the lowest constant possible. Expensive. WARNING: the lattice must be finite for this to terminate.

val zap_to_ceil : 'a C.obj -> ('a, 'l * Allowance.allowed) mode -> log:changes ref option -> 'a

Pushes the mode variable to the highest constant possible.

val newvar : 'a C.obj -> ('a, 'l * 'r) mode

Create a new mode variable of the full range.

val erase_hints : unit -> unit

Remove hints from all vars that have been created. This doesn't affect hints that were applied on top of vars. For example:

let m = newvar () in submode m (apply ~hint:hint0 g n); let m' = apply ~hint:hint1 f m in erase_hints ()

The last line erases the hints on m (caused by n), but m' has an immutable hint on top of m, which is not affected.

type ('a, 'd) hint_raw constraint 'd = 'l * 'r

Raw hint returned by failed submode a b. To consume it, see populate_hint.

type 'a error_raw = {
  1. left : 'a;
  2. left_hint : ('a, Allowance.left_only) hint_raw;
  3. right : 'a;
  4. right_hint : ('a, Allowance.right_only) hint_raw;
}

Raw error returned by failed submode a b. left will be the lowest mode a can be, and right will be the highest mode b can be. And left <= right will be false, which is why the submode failed. left_hint explains why left is high, and right_hint explains why right is low. To consume them, see populate_hint or populate_error.

val submode : Hint.Pinpoint.t -> 'a C.obj -> ('a, Allowance.allowed * 'r) mode -> ('a, 'l * Allowance.allowed) mode -> log:changes ref option -> (unit, 'a error_raw) result

Try to constrain the first mode below the second mode. pinpoint describes the thing that has both modes.

val newvar_above : 'a C.obj -> ('a, Allowance.allowed * 'r_) mode -> ('a, 'l * 'r) mode * bool

Creates a new mode variable above the given mode and returns true. In the speical case where the given mode is top, returns the constant top and false.

val newvar_below : 'a C.obj -> ('a, 'l_ * Allowance.allowed) mode -> ('a, 'l * 'r) mode * bool

Creates a new mode variable below the given mode and returns true. In the speical case where the given mode is bottom, returns the constant bottom and false.

val join : 'a C.obj -> ('a, Allowance.allowed * 'r) mode list -> ('a, Allowance.left_only) mode

Returns the join of the list of modes.

val meet : 'a C.obj -> ('a, 'l * Allowance.allowed) mode list -> ('a, Allowance.right_only) mode

Return the meet of the list of modes.

val get_floor : 'a C.obj -> ('a, Allowance.allowed * 'r) mode -> 'a

Returns the lower bound of the mode. Because of our conservative internal representation, further constraining is needed for precise bound. This operation is therefore expensive and requires the mode to be allowed on the left. WARNING: the lattice must be finite for this to terminate.

val get_ceil : 'a C.obj -> ('a, 'l * Allowance.allowed) mode -> 'a

Returns the upper bound of the mode. Notes for get_floor applies.

val get_loose_floor : 'a C.obj -> ('a, 'l * 'r) mode -> 'a

Similar to get_floor but does not run the further constraining needed for a precise bound. As a result, the returned bound is loose; i.e., it might be lower than the real floor.

val get_loose_ceil : 'a C.obj -> ('a, 'l * 'r) mode -> 'a

Similar to get_ceil but does not run the further constraining needed for a precise bound. As a result, the returned bound is loose; i.e., it might be higher than the real ceil.

val print : ?verbose:bool -> 'a C.obj -> Format.formatter -> ('a, 'l * 'r) mode -> unit

Printing a mode for debugging.

val apply : 'b C.obj -> ?hint:('l * 'r) Hint.Morph.t -> ('a, 'b, 'l * 'r) C.morph -> ('a, 'l * 'r) mode -> ('b, 'l * 'r) mode

Apply a monotone morphism explained by an optional hint

type ('a, 'd) hint =
  1. | Apply : 'd Hint.Morph.t * ('b, 'a, 'd) C.morph * ('b, 'd) ahint -> ('a, 'd) hint
    (*

    Apply morph_hint morph x_hint says the current bound is derived by applying morphism morph (explained by morph_hint) to another bound explained by x_hint

    *)
  2. | Const : 'd Hint.Const.t -> ('a, 'd) hint
    (*

    Const const_hint says the current bound is explained by const_hint

    *)
  3. | Branch : 'd Solver_intf.branch * ('a, 'd) ahint * ('a, 'd) ahint -> ('a, 'd) hint
    (*

    branch b hint0 hint1 says the current bound is jointly explained by hint0 and hint1.

    *)
constraint 'd = _ * _

('a, 'd) hint explains a bound of type 'a and allowance 'd, but doesn't contain the bound itself.

and ('a, 'd) ahint = 'a * ('a, 'd) hint constraint 'd = _ * _

('a, 'd) ahint is a bound of type 'a explained by a ('a, 'd) hint.

type 'a error = {
  1. left : ('a, Allowance.left_only) ahint;
  2. right : ('a, Allowance.right_only) ahint;
}

Mode error that's suitable for consumption.

val populate_hint : 'a C.obj -> 'a -> ('a, 'l * 'r) hint_raw -> ('a, 'l * 'r) ahint

Takes a bound with a hint_raw given by submode, and returns a ahint that's suitable for consumption.

val populate_error : 'a C.obj -> 'a error_raw -> 'a error

Takes a error_raw returned by submode, and returns an error hint that's suitable for consumption.

module Unhint : sig ... end