PP (imandra-tools.Imandra_tools.Region

type custom = S.c

Type of custom symbolic node

type ty = TY.ty

module TY : Region_pp_intf.TYPE_CONV with type ty = ty

type nonrec node = ( ty, custom ) Region_pp_intf.node

Type of symbolic node

type nonrec view = ( ty, custom ) Region_pp_intf.view

val view : node -> view

val ty : node -> ty

val mk : ty:ty -> view -> node

module XF : sig ... end

Transformation/Traversal over nodes

val vars : node -> Region_pp_intf.var_name list

Returns list of var names in node

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

type refiner = node -> node list

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.

parameter unify
optional unifier heuristic

parameter refine
optional refiner heuristic

parameter inv
optional must be set to true when pprinting an invariant

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:Region_pp_intf.var_name ->
  unit ->
  Stdlib.Format.formatter ->
  Imandra_surface.Modular_region.t ->
  unit

Print a region

parameter pp
optional pprinter, defaults to pp

parameter unify
optional unifier heuristic

parameter refine
optional refiner heuristic

parameter p
optional custom override printer

parameter skip_invariant
omit invariant in region

parameter focus
var name to consider the "subject" of the region

val to_string : 
  ?unify:Unifier.unifier ->
  ?refine:refiner ->
  Imandra_surface.Modular_region.t ->
  string

Return a string representation of a pprinted region

parameter unify
optional unifier heuristic

parameter refine
optional refiner heuristic