jon.recoil.org

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 equal : 'a obj -> 'a -> 'a -> bool
val join : 'a obj -> 'a -> 'a -> 'a
val meet : 'a obj -> 'a -> 'a -> 'a
val print : 'a obj -> Solver_intf.Fmt.formatter -> 'a -> unit
val compare_obj : 'a obj -> 'b obj -> int

Total ordering on objects, used for internal map keys. This is not a lattice ordering or semantic equality check. If this returns 0, then equal_obj must return Misc.Is_eq.

val equal_obj : 'a obj -> 'b obj -> ('a, 'b) Misc.is_eq

Equality on objects recognized by the solver. This is the only object comparison that carries type equality evidence.

val print_obj : Solver_intf.Fmt.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 compare_morph : 'b obj -> ('a0, 'b, 'd0) morph -> ('a1, 'b, 'd1) morph -> int

Total ordering on morphisms with a shared target object, used for internal map keys. This is not a lattice ordering or semantic equality check. If this returns 0, then equal_morph must return Misc.Is_eq.

val equal_morph : 'b obj -> ('a0, 'b, 'd0) morph -> ('a1, 'b, 'd1) morph -> ('a0, 'a1) Misc.is_eq

Equality on morphisms with a shared target object recognized by the solver. This is the only morphism comparison that carries source type equality evidence.

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

Print morphism