Module Imandra_tools.Region_pp_intf

module type TYPE_CONV = sig ... end
type comparison =
| UnComparable
| Equivalent
| NotEquivalent
| GreaterThan
| LessThan

Symbolic comparison result over nodes

type field_type = Imandra_tools_ast.Ast.field_type =
| Tuple
| Record
| Ctor of string(*

constructor field

*)
| Human(*

field access printed with english syntax

*)

Type of symbolic field

type coll_type = Imandra_tools_ast.Ast.coll_type =
| Tuple
| List
| Set

Type of sequential collection

type assoc_type = Imandra_tools_ast.Ast.assoc_type =
| List
| Set

Type of associative collection

type type_name = string
type var_name = string
type ctor_info = type_name * int
type ('ty, 'c) view = ( 'ty, 'c ) Imandra_tools_ast.Ast.view =
| Var of var_name
| String of string
| Real of Q.t
| Int of Z.t
| Boolean of bool
| Custom of 'c
| Coll of coll_type * ( 'ty, 'c ) node list
| Map of (( 'ty, 'c ) node * ( 'ty, 'c ) node) list * ( 'ty, 'c ) node
| Struct of type_name * (string * ( 'ty, 'c ) node) list
| Funcall of ( 'ty, 'c ) node * ( 'ty, 'c ) node list
| Obj of type_name * ( 'ty, 'c ) node list
| FieldOf of field_type * string * ( 'ty, 'c ) node
| Contains of assoc_type * ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Plus of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Minus of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Mult of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Div of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Geq of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Gt of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Between of bool * bool * ( 'ty, 'c ) node * ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Not of ( 'ty, 'c ) node
| Or of ( 'ty, 'c ) node list
| And of ( 'ty, 'c ) node list
| Eq of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Neq of ( 'ty, 'c ) node * ( 'ty, 'c ) node
| Is of type_name * ctor_info list * ( 'ty, 'c ) node

Type of symbolic node

and ('ty, 'c) node = ( 'ty, 'c ) Imandra_tools_ast.Ast.node = {
view : ( 'ty, 'c ) view;
ty : 'ty;
}
module type SIG = sig ... end

Custom node extensions

module type PP_SIG = sig ... end

A Custom node pprinter