Module Type

module Type: sig .. end
Types of terms

A type has to be hash-consed to be used in hash-consed terms.
Author(s): Christoph Sticksel



Types and hash-consing


type rangekind = 
| Range
| Enum
Tells if the range actually encodes an enumerated datatype
type kindtype = 
| Bool
| Int
| IntRange of Numeral.t * Numeral.t * rangekind
| Real
| Array of t * t
| Abstr of string
Type of an expression
type t 
Hashconsed type
val node_of_type : t -> kindtype
Return the value Type.kindtype in a hashconsed type

Hashtables, maps and sets


val compare_types : t -> t -> int
Comparison function on types
val equal_types : t -> t -> bool
Equality function on types
val hash_type : t -> int
Hashing function on types
module TypeHashtbl: Hashtbl.S  with type key = t
Hash table over types
module TypeSet: Set.S  with type elt = t
Set over types
module TypeMap: Map.S  with type key = t
Map over types

Constructor


val mk_type : kindtype -> t
Hashcons a type
val mk_bool : unit -> t
Return the boolean type
val mk_int : unit -> t
Return the integer type
val mk_int_range : Numeral.t -> Numeral.t -> t
Return the integer range type
val mk_real : unit -> t
Return the real decimal type
val mk_array : t -> t -> t
Return an array type of index sort and element sort
val mk_abstr : string -> t
Return an abstract type
val mk_enum : string option -> string list -> t
Return an enumerated datatype type
val import : t -> t
Import a type from a different instance into this hashcons table
val t_bool : t
The boolean type
val t_int : t
The integer type
val t_real : t
The real decimal type

Type checking


val check_type : t -> t -> bool
check_type s t returns true if s is a subtype of t

Predicates


val is_bool : t -> bool
Return true if the type is the Boolean type
val is_int : t -> bool
Return true if the type is the integer type
val is_int_range : t -> bool
Return true if the type is an integer range type
val is_enum : t -> bool
Return true if the type is an integer range type
val is_real : t -> bool
Return true if the type is the real type
val is_array : t -> bool
Return true if the type is an array type
val is_abstr : t -> bool
Return true if the type is abstract

Ranges


val bounds_of_int_range : t -> Numeral.t * Numeral.t
Return bounds of an integer range type, fail with Invalid_argument "bounds_of_int_range" if the type is not an integer range type.
val generalize : t -> t
Generalize a type (remove actual intranges)

Arrays


val index_type_of_array : t -> t
Return type of array index
val all_index_types_of_array : t -> t list
Return all array index types of a nested array type
val elem_type_of_array : t -> t
Return type of array elements
val last_elem_type_of_array : t -> t
Return all array index types of a nested array type

Enumerated datatypes


val constructors_of_enum : t -> string list
Return constructors of an enumerated datatype
val name_of_enum : t -> string option
Return the name of an enumerated datatype encoded as int ranges
val get_constr_of_num : Numeral.t -> string
Return the constructor encoded by the numeral argument
val get_all_abstr_types : unit -> t list
Return abstract types that have been built
val get_num_of_constr : string -> Numeral.t
Return the numeral encoding of a construcor of an enumerated datatype
val enum_of_constr : string -> t
Return the enumerated dataype to which the constructor belongs

Pretty-printing


val pp_print_type_node : Format.formatter -> kindtype -> unit
Pretty-print a type
val pp_print_type : Format.formatter -> t -> unit
Pretty-print a type
val print_type : t -> unit
Pretty-print a type to the standard formatter
val string_of_type : t -> string
Return a string representation of a type