Module Region_pp.PPrinter

Default pprinter with no custom nodes

type custom = unit

Type of custom symbolic node

type ty = string
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