Parameter Solver_mono.C

include Solver_intf.Lattices with type 'a elt := 'a
type 'a obj

Lattice identifers, indexed by 'a the carrier type of that lattice

val min : 'a obj -> 'a
val max : 'a obj -> 'a
val le : 'a obj -> 'a -> 'a -> bool
val join : 'a obj -> 'a -> 'a -> 'a
val meet : 'a obj -> 'a -> 'a -> 'a
val print : 'a obj -> Format.formatter -> 'a -> unit
val eq_obj : 'a obj -> 'b obj -> ('a, 'b) Ocaml_utils.Misc_stdlib.eq option
val print_obj : Format.formatter -> 'a obj -> unit
type ('a, 'b, 'd) morph constraint 'd = 'l * 'r

Morphism from object of base type 'a to object of base type 'b with allowance 'd. See Note Allowance in allowance.mli.

'd is 'l * 'r, where 'l can be:

  • allowed, meaning the morphism can be on the left because it has right adjoint.
  • disallowed, meaning the morphism cannot be on the left because it does not have right adjoint. Similar for 'r.
val src : 'b obj -> ('a, 'b, 'd) morph -> 'a obj

Give the source object of a morphism

val id : ('a, 'a, 'd) morph

Give the identity morphism on an object

val compose : 'c obj -> ('b, 'c, 'd) morph -> ('a, 'b, 'd) morph -> ('a, 'c, 'd) morph

Compose two morphisms

val left_adjoint : 'b obj -> ('a, 'b, 'l * Allowance.allowed) morph -> ('b, 'a, Allowance.left_only) morph

Give left adjoint of a morphism

val right_adjoint : 'b obj -> ('a, 'b, Allowance.allowed * 'r) morph -> ('b, 'a, Allowance.right_only) morph

Give the right adjoint of a morphism

include Allowance.Allow_disallow with type ('a, 'b, 'd) sided = ('a, 'b, 'd) morph
type ('a, 'b, 'd) sided = ('a, 'b, 'd) morph
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 apply : 'b obj -> ('a, 'b, 'd) morph -> 'a -> 'b

Apply morphism on constant

val eq_morph : ('a0, 'b, 'l0 * 'r0) morph -> ('a1, 'b, 'l1 * 'r1) morph -> ('a0, 'a1) Ocaml_utils.Misc_stdlib.eq option

Checks if two morphisms are equal. If so, returns Some Refl. Used for deduplication only; it is fine (but not recommended) to return None for equal morphisms.

While a morph must be acompanied by a destination obj to uniquely identify a morphism, two morph sharing the same destination can be compared on their own.

val print_morph : 'b obj -> Format.formatter -> ('a, 'b, 'd) morph -> unit

Print morphism