Module Imandra_tools_ast.Ast

type field_type =
| Tuple
| Record
| Ctor of string(*

constructor field

*)
| Human(*

field access printed with english syntax

*)

Type of symbolic field

type coll_type =
| Tuple
| List
| Set

Type of sequential collection

type assoc_type =
| List
| Set

Type of associative collection

type var_name = string
type type_name = string
type ctor_info = type_name * int
and ('ty, 'c) 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 constructors

and ('ty, 'c) node = {
view : ( 'ty, 'c ) view;
ty : 'ty;
}