module Types: sig
.. end
Structural comparison of types, without expanding type abbreviations.
Probably better not to use. Consider using compare_expand
instead.
type
tnvar =
val pp_tnvar : Format.formatter -> tnvar -> unit
val tnvar_to_rope : tnvar -> Ulib.Text.t
val tnvar_compare : tnvar -> tnvar -> int
module TNvar: sig
.. end
module Pfmap: Finite_map.Fmap
with type k = Path.t
module Pset: Set.S
with type elt = Path.t
module TNfmap: Finite_map.Fmap
with type k = TNvar.t
module TNset: sig
.. end
type
t_uvar
type
n_uvar
type
t = {
}
type
t_aux =
type
nexp = {
}
type
nexp_aux =
type
range =
| |
LtEq of Ast.l * nexp |
| |
Eq of Ast.l * nexp |
| |
GtEq of Ast.l * nexp |
val range_with : range -> nexp -> range
val range_of_n : range -> nexp
val mk_gt_than : Ast.l -> nexp -> nexp -> range
val mk_eq_to : Ast.l -> nexp -> nexp -> range
val compare : t -> t -> int
Structural comparison of types, without expanding type abbreviations.
Probably better not to use. Consider using compare_expand
instead.
val multi_fun : t list -> t -> t
val type_subst : t TNfmap.t -> t -> t
val nexp_subst : t TNfmap.t -> nexp -> nexp
val free_vars : t -> TNset.t
val is_var_type : t -> bool
val is_instance_type : t -> bool
is the type ok to be used in an non-default type-class instantiation?
val tnvar_to_name : tnvar -> Name.t
val tnvar_to_type : tnvar -> t
val tnvar_split : tnvar list -> tnvar list * tnvar list
type
const_descr_ref
A reference to a constant description. These constant description references
are used by typed_ast
. This module also contains the appropriate mapping
functionality to constant descriptions. However, the references need to
be defined here, because types need information about associated constants.
Record types need a list of all their field constants. Moreover, every type
can contain a list of constructor descriptions.
val string_of_const_descr_ref : const_descr_ref -> string
string_of_const_descr_ref
formats a reference in a human readable form.
No other guarentees are given. This function should only be used for debugging
and reporting internal errors. Its implementation can change at any point to
something completely different and should not be relied on.
module Cdmap: Finite_map.Fmap
with type k = const_descr_ref
module Cdset: Set.S
with type elt = const_descr_ref
type 'a
cdmap
cdmap
is a type for maps of const_descr_ref. In contrast to finite maps
represented by module Cdmap
, the keys might be autogenerated.
val cdmap_empty : unit -> 'a cdmap
Constructs an empty cdmap
val cdmap_lookup : 'a cdmap -> const_descr_ref -> 'a option
cdmap_lookup m r
looks up the reference r
in map m
val cdmap_update : 'a cdmap -> const_descr_ref -> 'a -> 'a cdmap
cdmap_update m r v
updates map m
at reference r
with value v
.
val cdmap_insert : 'a cdmap -> 'a -> 'a cdmap * const_descr_ref
cdmap_insert m v
inserts value v
into m
. A fresh (not occurring in m
) reference
is generated for v
and returned together with the modifed map.
val cdmap_domain : 'a cdmap -> const_descr_ref list
cdmap_domain m
returns the list of all const description references in the map
val nil_const_descr_ref : const_descr_ref
nil_const_descr_ref
is a nil reference, i.e. a reference that will never be bound
by any cdmap.
val is_nil_const_descr_ref : const_descr_ref -> bool
is_nil_const_descr_ref r
checks whether r
is the nil reference.
type ('a, 'b)
annot = {
|
term : 'a ; |
|
locn : Ast.l ; |
|
typ : t ; |
|
rest : 'b ; |
}
val annot_to_typ : ('a, 'b) annot -> t
type
ident_option =
| |
Id_none of Ast.lex_skips |
| |
Id_some of Ident.t |
type 'a
id = {
|
id_path : ident_option ; |
|
id_locn : Ast.l ; |
|
descr : 'a ; |
|
instantiation : t list ; |
}
Represents a usage of an 'a (usually in constr_descr, field_descr,
const_descr)
type
src_t = (src_t_aux, unit) annot
type
src_t_aux =
type
src_nexp = {
}
type
src_nexp_aux =
| |
Nexp_var of Ast.lex_skips * Nvar.t |
| |
Nexp_const of Ast.lex_skips * int |
| |
Nexp_mult of src_nexp * Ast.lex_skips * src_nexp |
| |
Nexp_add of src_nexp * Ast.lex_skips * src_nexp |
| |
Nexp_paren of Ast.lex_skips * src_nexp * Ast.lex_skips |
val src_t_to_t : src_t -> t
val src_type_subst : src_t TNfmap.t -> src_t -> src_t
val id_alter_init_lskips : (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
'a id -> 'a id * Ast.lex_skips
val typ_alter_init_lskips : (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
src_t -> src_t * Ast.lex_skips
val nexp_alter_init_lskips : (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
src_nexp -> src_nexp * Ast.lex_skips
type
constr_family_descr = {
|
constr_list : const_descr_ref list ; |
|
constr_exhaustive : bool ; |
|
constr_case_fun : const_descr_ref option ; |
|
constr_default : bool ; |
|
constr_targets : Target.Targetset.t ; |
}
type
type_target_rep =
| |
TYR_simple of Ast.l * bool * Ident.t |
| |
TYR_subst of Ast.l * bool * tnvar list * src_t |
the target representation of a type
type
type_descr = {
}
a type description *
type
class_descr = {
}
type
tc_def =
type
type_defs = tc_def Pfmap.t
val type_defs_update_tc_type : Ast.l ->
type_defs ->
Path.t -> (type_descr -> type_descr option) -> type_defs
type_defs_update_tc_type l d p up
updates the description of type p
in d
using the function up
.
If there is no type p
in d
or if up
returns None
, an exception is raised.
val type_defs_update_tc_class : Ast.l ->
type_defs ->
Path.t -> (class_descr -> class_descr option) -> type_defs
type_defs_update_tc_class l d p up
updates the description of type p
in d
using the function up
.
If there is no type p
in d
or if up
returns None
, an exception is raised.
val type_defs_update_fields : Ast.l ->
type_defs -> Path.t -> const_descr_ref list -> type_defs
type_defs_update_fields l d p fl
updates the fields of type p
in d
.
val type_defs_add_constr_family : Ast.l ->
type_defs -> Path.t -> constr_family_descr -> type_defs
val type_defs_get_constr_families : Ast.l ->
type_defs ->
Target.target ->
t -> const_descr_ref -> constr_family_descr list
type_defs_get_constr_families l d targ t c
gets all constructor family descriptions for type t
for target targ
in type environment d
, which contain the constant c
.
val type_defs_lookup_typ : Ast.l -> type_defs -> t -> type_descr option
type_defs_lookup_typ l d t
looks up the description of type t
in defs d
.
val type_defs_lookup : Ast.l -> type_defs -> Path.t -> type_descr
type_defs_lookup l d p
looks up the description of type with path p
in defs d
.
val type_defs_update : type_defs -> Path.t -> type_descr -> type_defs
type_defs_update d p td
updates the description of type with path p
in defs d
with td
.
val mk_tc_type_abbrev : tnvar list -> t -> tc_def
Generates a type abbreviation
val mk_tc_type : tnvar list -> string option -> tc_def
mk_tc_type vars reg_exp_opt
generates a simple description of a type,
which uses the type arguments vars
and the reg_exp_opt
for restricting
the names of variables of this type.
val match_types : t -> t -> t TNfmap.t option
match_types t_pat t
tries to match type t_pat
against type t
.
If it succeeds, it returns a substitution sub
that applied to t_pat
returns t
.
This function is rather simple. It does not use type synonyms or other fancy features.
type
instance = {
}
an instance of a type class
type
typ_constraints =
val head_norm : type_defs -> t -> t
val dest_fn_type : type_defs option -> t -> (t * t) option
dest_fn_type d_opt t
tries to destruct a function type
t
. Before the destruction, head_norm d t
is applied, if
d_opt
is of the form Some d
. If the result is a function type,
t1 --> t2
, the Some (t1, t2)
is returned. Otherwise the result
is None
.
val strip_fn_type : type_defs option -> t -> t list * t
strip_fn_type d t
tries to destruct a function type t
by applying dest_fn
repeatedly.
val check_equal : type_defs -> t -> t -> bool
check_equal d t1 t2
checks whether t1
and t2
are equal in type environment d
.
It expands the type to perform this check. Therefore, it is more reliable than compare t1 t2 = 0
,
which only performs a structural check, but does not unfold type definitions.
val assert_equal : Ast.l -> string -> type_defs -> t -> t -> unit
assert_equal l m d t1 t2
performs the same check as check_equal d t1 t2
. However, while
check_equal returns wether the types are equal, assert_equal
raises a type-exception
in case they are not. l
and m
are used for printing this exception.
val compare_expand : type_defs -> t -> t -> int
compare_expand d t1 t2
is similar check_equal d t1 t2
. Instead of just checking for equality,
it compare the values though. During this comparison, type abbrivations are unfolded. Therefore,
it is in general preferable to the very similar method compare
, which perform comparisons without
unfolding.
type
instance_ref
A reference to an instance.
val string_of_instance_ref : instance_ref -> string
string_of_instance_ref
formats a reference in a human readable form.
No other guarentees are given. This function should only be used for debugging
and reporting internal errors. Its implementation can change at any point to
something completely different and should not be relied on.
type
i_env
an instance environment carries information about all defined instances
val empty_i_env : i_env
an empty instance environment
val i_env_add : i_env -> instance -> i_env * instance_ref
i_env_add i_env i
adds an additional instance i
to the instance environment.
It returns the modified environment as well as the reference of the added instance.
val i_env_lookup : Ast.l -> i_env -> instance_ref -> instance
i_env_lookup l i_env ref
looks up the reference in environment i_env
.
If this reference is not present, an exception is raised.
val get_matching_instance : type_defs ->
Path.t * t ->
i_env -> (instance * t TNfmap.t) option
get_matching_instance type_env (class, ty) i_env
searches for an
instantiation of type class class
instantianted with type ty
in the type invironment i_env
. The type environment type_env
is necessary to match ty
against other instantiations of
class
. An instance can itself have free type variables. If a
matching instance is found, it is returned to together with the
substition, which needs to be applied to the free type variables
of the instance in order to match type t
excactly. The
typevariables of an instances might have attached type
constraints. It is not (!) checked, that the found substitution
satisfies these constraints. However, they are taken into account
to rule out impossible instances, if there are multiple options.
val nexp_from_list : nexp list -> nexp
module type Global_defs = sig
.. end
module Constraint:
val pp_type : Format.formatter -> t -> unit
val pp_nexp : Format.formatter -> nexp -> unit
val pp_range : Format.formatter -> range -> unit
val pp_class_constraint : Format.formatter -> Path.t * tnvar -> unit
val pp_instance : Format.formatter -> instance -> unit
val pp_typschm : Format.formatter ->
tnvar list -> (Path.t * tnvar) list -> t -> unit
val t_to_string : t -> string
val print_debug_typ_raw : string -> t list -> unit
print_debug_typ_raw s [ty0, ..., tn]
prints a debug message s t0, ..., tn
using Reporting_basic.print_debug
.
val t_to_var_name : t -> Name.t