Module Imandra_surface.Type

Imandra/Pure type definitions

type t =
| Var of var
| Arrow of string * t * t
| Tuple of t list
| Constr of def * t list

A general type expression for Imandra

and var = Uid.t

Variable, including 'a

and decl =
| Algebraic of adt_row list
| Record of rec_row list
| Alias of {
target : t;
}
| Skolem
| Builtin of Builtin.Ty.t
| Other

Definition of a named type

and adt_row = {
c : Uid.t;
labels : Uid.t list option;
args : t list;
}

List of constructors for an algebraic type

and rec_row = {
f : Uid.t;
ty : t;
}

List of record fields

and def = private {
params : var list;
name : Uid.t;
loc : Imandra_util.Iloc.t;
mutable decl : decl;
clique : Imandra_surface.Uid.Set.t;
doc : Imandra_document.Document.t option;
mutable validated : float option;
codegen_tags : (string * string) list;
}

A type definition, parametrized by some type variables

val sentinel_decl : decl
val set_decl : def -> decl -> unit
val chash : cb_id:(Uid.t -> unit) -> ?⁠local:Uid.Chash_map.t -> t Imandra_util.Chash.hasher

hash type structurally

val mk_def : ?⁠no_validate:bool -> ?⁠loc:Imandra_util.Iloc.t -> ?⁠doc:Imandra_document.Document.t -> ?⁠clique:Imandra_surface.Uid.Set.t -> ?⁠codegen_tags:(string * string) list -> name:Uid.t -> params:var list -> decl -> def
module Var : sig ... end
val equal : t -> t -> bool

Type equality

val equal_chase_deep : t -> t -> bool

Chase deep + type equality

val hash : t -> int

Hash type

val to_string : t -> string
val print : Stdlib.Format.formatter -> t -> unit
val to_doc : t -> Imandra_document.Document.t
type 'a printer = 'a CCFormat.printer
val print_as_ocaml_with : Uid.t printer -> t printer
val to_string_as_ocaml : t -> string
val print_as_ocaml : t printer
val print_def_as_ocaml : id:Uid.t printer -> ty:t printer -> def printer
val string_of_def : def -> string
val print_def : def printer
val def_to_doc : def -> Imandra_document.Document.t
val documentation : def -> Imandra_document.Document.t option
val validated : def -> bool
val print_defs : Stdlib.Format.formatter -> def list -> unit
val print_defs_as_ocaml : id:Uid.t printer -> ty:t printer -> def list printer
val print_clique : Imandra_surface.Uid.Set.t CCFormat.printer
val in_out_types : t -> t list * t

Open the toplevel function types

val n_args : t -> int

Number of arguments for a function type

val make_other : Uid.t -> def

Undefined type

val returns : t -> t

Return type of a function (same as snd (in_out_types ty))

val drop_n_args : int -> t -> t

Assuming the type has at least n arguments, remove the n first. Normally one should have drop_n_args (n_args ty) = returns ty

val is_param : t -> bool

Parametric type (higher order, or polymorphic)?

type subst = t Var.Map.t

Substitution: a binding from variables to types

val empty_subst : subst
val apply_subst : ?⁠rec_:bool -> t -> subst -> t

Apply substitution

parameter rec_

if true (default), substitute in RHS of substitution too.

val apply_subst' : ?⁠rec_:bool -> subst -> t -> t
val print_subst : Stdlib.Format.formatter -> subst -> unit
val string_of_subst : subst -> string
val free_vars : t -> Var.Set.t

Set of variables of the type

val free_vars_add : Var.Set.t -> t -> Var.Set.t

add free vars of the type to this set

val is_ground : t -> bool

Is the type ground (i.e. without variables)?

val is_poly : t -> bool

Is the type non-ground (i.e. with some variables)?

val is_ground_def : def -> bool

Is the definition parameter-free?

val name : def -> Uid.t
val mk_var : Var.t -> t
val mk_arrow_l : t list -> t -> t
val mk_skolem : Uid.t -> t

Skolem type

val is_inline_record_cstor : def -> Uid.t -> bool

is_inline_record_cstor def c returns true if c is a constructor of def with an inline record

Unification

val iter_def_uids : def -> (Uid.t -> unit) -> unit

Iterate on the IDs in the definition

val fold_def_uids : ('a -> Uid.t -> 'a) -> 'a -> def -> 'a

Fold on the IDs in the definition

val iter : t -> (t -> unit) -> unit

Iterate on immediate sub-types

val map : t -> f:(t -> t) -> t

Map on immediate sub-types

val chase : ?⁠subst:subst -> t -> t

follow bound variables and aliases at the root of the type. The returned type is either an arrow, a non-bound variable or a non-alias Constr.

val chase_deep : ?⁠subst:subst -> t -> t

Deep version of chase, normalizing arguments recursively

val match_ : ?⁠subst:subst -> t -> t -> subst option

match_ subst t1 t2 returns the most general substitution sigma that is an extension of subst such that sigma(t1) and t2 equal.

val unify : ?⁠subst:subst -> t -> t -> subst option

unify subst t1 t2 returns the most general substitution sigma that is an extension of subst such that sigma(t1) and sigma(t2) equal.

val alpha_equiv : ?⁠subst:subst -> can_bind:(Var.t -> bool) -> t -> t -> subst option

alpha_equiv ~can_bind t1 t2 searchs for sigma where sigma(t1) = t2 such that sigma only binds variables that satisfy can_bind. In practice, if t1 and t2 have disjoint variables and can_bind returns true only for variables of t1, then this checks for alpha-equivalence. NOTE: you need to apply is_renaming on the result

val is_renaming : subst -> bool
val apply_arrow_unify : ?⁠subst:subst -> t -> t list -> (t * subst) option

apply_arrow_unify ty_f args applies the function type ty_f to arguments, unifying types in the process. For example apply_unify ('a -> 'a) [(int->bool); int] would return bool

val same_base_type : t -> t -> bool

Same head constructor?

Basic predicates for built-in types

val is_int : t -> bool
val is_real : t -> bool
val is_float : t -> bool
val is_bool : t -> bool
val is_string : t -> bool
val is_reflect_term : t -> bool
val is_arith : t -> bool
val is_list : t -> bool
val is_option : t -> bool
val is_arrow : t -> bool
val int : unit -> t
val option : t -> t
val list : t -> t
val int : unit -> t
val bool : unit -> t
val real : unit -> t
val float : unit -> t
val string : unit -> t
module Builtins : sig ... end
module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t