Module Ty

module Ty: sig .. end
Types


Type variables


type tvsymbol = private {
   tv_name : Ident.ident;
}
module Mtv: Extmap.S  with type key = tvsymbol
module Stv: Extset.S  with module M = Mtv
module Htv: Exthtbl.S  with type key = tvsymbol
val tv_compare : tvsymbol -> tvsymbol -> int
val tv_equal : tvsymbol -> tvsymbol -> bool
val tv_hash : tvsymbol -> int
val create_tvsymbol : Ident.preid -> tvsymbol
val tv_of_string : string -> tvsymbol

Type symbols and types


type tysymbol = private {
   ts_name : Ident.ident;
   ts_args : tvsymbol list;
   ts_def : ty option;
}
type ty = private {
   ty_node : ty_node;
   ty_tag : Weakhtbl.tag;
}
type ty_node = private 
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Mts: Extmap.S  with type key = tysymbol
module Sts: Extset.S  with module M = Mts
module Hts: Exthtbl.S  with type key = tysymbol
module Wts: Weakhtbl.S  with type key = tysymbol
module Mty: Extmap.S  with type key = ty
module Sty: Extset.S  with module M = Mty
module Hty: Exthtbl.S  with type key = ty
module Wty: Weakhtbl.S  with type key = ty
val ts_compare : tysymbol -> tysymbol -> int
val ty_compare : ty -> ty -> int
val ts_equal : tysymbol -> tysymbol -> bool
val ty_equal : ty -> ty -> bool
val ts_hash : tysymbol -> int
val ty_hash : ty -> int
exception BadTypeArity of tysymbol * int
exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVar of tvsymbol
val create_tysymbol : Ident.preid -> tvsymbol list -> ty option -> tysymbol
val ty_var : tvsymbol -> ty
val ty_app : tysymbol -> ty list -> ty

Generic traversal functions


val ty_map : (ty -> ty) -> ty -> ty
traverse only one level of constructor, if you want full traversal you need to call those function inside your function
val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool

Variable-wise map/fold


val ty_v_map : (tvsymbol -> ty) -> ty -> ty
visits every variable of the type
val ty_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ty -> 'a
val ty_v_all : (tvsymbol -> bool) -> ty -> bool
val ty_v_any : (tvsymbol -> bool) -> ty -> bool

Symbol-wise map/fold


val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
visits every symbol of the type
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch of ty * ty
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
ty_match sigma0 pat sub returns a type substitution sigma such that sigma pat = sub. Raises TypeMismatch if no substitution exists.
val ty_inst : ty Mtv.t -> ty -> ty
val ty_freevars : Stv.t -> ty -> Stv.t
val ty_closed : ty -> bool
ty_closed ty returns true when ty is not polymorphic
val ty_equal_check : ty -> ty -> unit
val ts_int : tysymbol
val ts_real : tysymbol
val ts_bool : tysymbol
val ty_int : ty
val ty_real : ty
val ty_bool : ty
val ts_func : tysymbol
val ts_pred : tysymbol
val ty_func : ty -> ty -> ty
val ty_pred : ty -> ty
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
val is_ts_tuple : tysymbol -> bool
val is_ts_tuple_id : Ident.ident -> int option

Operations on ty option


exception UnexpectedProp
val oty_compare : ty option -> ty option -> int
val oty_equal : ty option -> ty option -> bool
val oty_hash : ty option -> int
val oty_type : ty option -> ty
val oty_cons : ty list -> ty option -> ty list
val oty_match : ty Mtv.t -> ty option -> ty option -> ty Mtv.t
val oty_inst : ty Mtv.t -> ty option -> ty option
val oty_freevars : Stv.t -> ty option -> Stv.t