Region_pp_intf.PP_SIG
A Custom node pprinter
module XF : sig ... end
Transformation/Traversal over nodes
val has_symbolic_term : node -> bool
Returns true if node contains one or more vars
module Printer : sig ... end
Node printer
module Comparator : sig ... end
Node comparator
module Simplifier : sig ... end
Node simplifier
module Unifier : sig ... end
Node unifier
module Parser : sig ... end
Node parser
module Compactor : sig ... end
Node compactor
Refiner heuristic, the logical opposite of a unifier
: splits a node
into multiple ones
type pprinter =
?unify:Unifier.unifier ->
?refine:refiner ->
?inv:bool ->
Imandra_surface.Term.t list ->
node list
Type of a pprinter of Term.t
values into a list of nodes.
val pp : pprinter
PPrint a list of Term.t
values into a list of nodes.
val print :
?pp:pprinter ->
?unify:Unifier.unifier ->
?refine:refiner ->
?print:( node CCFormat.printer -> CCFormat.formatter -> node -> unit option ) ->
?skip_invariant:bool ->
?focus:var_name ->
unit ->
Stdlib.Format.formatter ->
Imandra_surface.Modular_region.t ->
unit
Print a region
val to_string :
?unify:Unifier.unifier ->
?refine:refiner ->
Imandra_surface.Modular_region.t ->
string
Return a string representation of a pprinted region