module type PRINT = sig end
Printing of constraints may be parametrized by an implementation
of the signature
PRINT
. All printing are performed using the module
Format
of the Objective Caml standard library. A general purpose
instance implementation is provided by
Dalton_templates.Print
.
val ghost : string
The string to be printed in place of ghost variables (i.e.
unconstrained anonymous variables), e.g. "_"
val left_destructor : 'a Dalton_aux.printer -> Format.formatter -> 'a -> unit
val right_destructor : 'a Dalton_aux.printer -> Format.formatter -> 'a -> unit
val left_destructor_skel : 'a Dalton_aux.printer -> Format.formatter -> 'a -> unit
val right_destructor_skel : 'a Dalton_aux.printer -> Format.formatter -> 'a -> unit
val same_skel : 'a Dalton_aux.printer -> Format.formatter -> 'a list -> unit
same_skel printer ppf list
prints a same-skeleton constraint
involving elements of the list list
. A printer printer
is given
as argument for printing each element of the list.
val equal : 'a Dalton_aux.printer -> Format.formatter -> 'a list -> unit
same_skel printer ppf list
prints an equality involving elements
of the list list
. A printer printer
is given as argument for
printing each element of the list.
leq lhs_printer rhs_printer ppf lhs rhs
prints the inequality
lhs < rhs
on the formatter ppf
. Two printers lhs_printer
and rhs_printer
are provided for printing the left-hand and
right-hand sides, respectively.
val leq : 'a Dalton_aux.printer ->
'b Dalton_aux.printer -> Format.formatter -> 'a -> 'b -> unit
val lhs : 'a Dalton_aux.printer -> Format.formatter -> 'a list -> unit
lhs printer ppf list
prints the left-hand side of an inequality,
consisting in the elements of list the list
. A printer printer
is given as argument for printing each element of the list.
val rhs : 'a Dalton_aux.printer -> Format.formatter -> 'a list -> unit
rhs printer ppf list
prints the right-hand side of an inequality,
consisting in the elements of list the list
. A printer printer
is given as argument for printing each element of the list.
val cset_begin : Format.formatter -> unit
cset_begin ppf
is called before printing a constraint set on the
formatter ppf
.
val cset_end : Format.formatter -> unit
cset_end ppf
is called at the end of the printing a constraint set
on the formatter ppf
.
val cset_item : 'a Dalton_aux.printer -> Format.formatter -> 'a -> unit
Every constraint c
of a constraint set is printed on the formatter
ppf
by a call of the form cset_item printer ppf c
where printer
is a suitable printer for the constraint.