Previous  Up  Next

Module Typed_ast_syntax


module Typed_ast_syntax: sig .. end
syntax functions for typed_ast

Types


val bool_ty : Types.t
The boolean type
val nat_ty : Types.t
The natural number type

Navigating Environments


val lookup_env_opt : Typed_ast.env -> Name.t list -> Typed_ast.local_env option
lookup_env_opt env path is used to navigate inside a environment env. It returns the local environment which is reachable via the path path. If no such environment exists, None is returned.
val lookup_env : Typed_ast.env -> Name.t list -> Typed_ast.local_env
lookup_env is similar to lookup_env_opt, but reports an internal error instead of returning None, if no environment can be found.
val env_apply : Typed_ast.env ->
       Ast.component option ->
       Name.t -> (Typed_ast.name_kind * Path.t * Ast.l) option
env_apply env comp_opt n looks up the name n in the environment env. If component comp is given, only this type of component is searched. Otherwise, it checks whether n refers to a type, field, constructor or constant. env_apply returns the kind of this name, it's full path and the location of the original definition.
val lookup_mod_descr_opt : Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr option
lookup_mod_descr_opt env path mod_name is used to navigate inside an environment env. It returns the module with name mod_name, which is reachable via the path path. If no such environment exists, None is returned.
val lookup_mod_descr : Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr
lookup_mod_descr env path mod_name is used to navigate inside an environment env. It returns the module with name mod_name, which is reachable via the path path. If no such environment exists, Reporting_basic is used to report an internal error.
val names_get_const : Typed_ast.env ->
       Name.t list -> Name.t -> Types.const_descr_ref * Typed_ast.const_descr
names_get_const env path n looks up the constant with name n reachable via path path in the environment env
val strings_get_const : Typed_ast.env ->
       string list -> string -> Types.const_descr_ref * Typed_ast.const_descr
strings_get_const is a wrapper around names_get_const that uses strings instead of names.
val get_const : Typed_ast.env -> string -> Types.const_descr_ref * Typed_ast.const_descr
get_const env label is a wrapper around string_get_const that maps a label to an actual constant description.
val const_exists : Typed_ast.env -> string -> bool
const_exists env label checks, whether the constant with label label is available in the environment env. If it is get_const env label succeeds, otherwise it fails.

names_get_const_ref env path n looks up the constant with name n reachable via path path in the environment env
val const_descr_to_kind : Types.const_descr_ref * Typed_ast.const_descr -> Typed_ast.name_kind
const_descr_to_kind r d assumes that d is the description associated with reference r. It then determines the kind of constant (field, constructor, constant) depending on the information stored in d.
val strings_get_const_id : Typed_ast.env ->
       Ast.l ->
       string list ->
       string ->
       Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
strings_get_const_id env l path n inst uses get_const env path n to construct a const_descr and then wraps it in an id using location l and instantiations inst.
val get_const_id : Typed_ast.env ->
       Ast.l ->
       string ->
       Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
get_const_id env l label inst uses strings_get_const_id with an indirection to look up a constant for a given label.
val strings_mk_const_exp : Typed_ast.env ->
       Ast.l -> string list -> string -> Types.t list -> Typed_ast.exp
strings_mk_const_exp uses get_const_id to construct a constant expression.
val mk_const_exp : Typed_ast.env -> Ast.l -> string -> Types.t list -> Typed_ast.exp
mk_const_exp uses strings_mk_const_exp with an indirection through a label.
val dest_field_types : Ast.l ->
       Typed_ast.env ->
       Types.const_descr_ref -> Types.t * Path.t * Typed_ast.const_descr
dest_field_types l env f looks up the types of the field f in environment env. It first gets the description f_descr of the field f in env. It then looks up the type of f. For fields, this type is always of the form field_type --> (free_vars) rec_ty_path. dest_field_types checks that free_vars corresponds with the free typevariables of f_descr. If the type of f is not of the described from, or if free_vars does not correspond, the constant did not describe a proper field. In this case, dest_field_types fails. Otherwise, it returns (field_type, rec_ty_path, f_descr).
val get_field_type_descr : Ast.l -> Typed_ast.env -> Types.const_descr_ref -> Types.type_descr
get_field_type_descr l env f uses dest_field_types l env f to get the base type of the field f. It then looks up the description of this type in the environment.
val get_field_all_fields : Ast.l -> Typed_ast.env -> Types.const_descr_ref -> Types.const_descr_ref list
get_field_all_fields l env f uses get_field_type_descr l env f to look up the type description of the record type of the field f. It then returns a list of all the other fields of this record.
val lookup_class_descr : Ast.l -> Typed_ast.env -> Path.t -> Types.class_descr
lookup_class_descr l env c_path looks up the description of type-class c_path in environment env. If c_path is no valid type-class, an exception is raised.
val lookup_field_for_class_method : Ast.l -> Types.class_descr -> Types.const_descr_ref -> Types.const_descr_ref
lookup_field_for_class_method l cd method_ref looks up the field reference corresponding to the method identified by method_ref in the description cd of a type class. If the reference does not point to a method of this type-class, an exception is raised.
val lookup_inst_method_for_class_method : Ast.l -> Types.instance -> Types.const_descr_ref -> Types.const_descr_ref
lookup_inst_method_for_class_method l i method_ref looks up the instance method reference corresponding to the method identified by method_ref in the instance i. If the reference does not point to a method of this instance, an exception is raised.
val class_descr_get_dict_type : Types.class_descr -> Types.t -> Types.t
Given a class-description cd and an argument type arg, the function class_descr_get_dict_type cd arg generates the type of the dictionary for the class and argument type.
val class_all_methods_inlined_for_target : Ast.l -> Typed_ast.env -> Target.target -> Path.t -> bool
Some targets may choose to not use type-classes to implement certain functions. An example is the equality type-class, which is implemented using just the build-in equality of HOL, Coq and Isabelle instead of one determined by the type-class. If all methods of a type-class are specially treated like this, the type-class does not need to be generated at all. This involves not generating the record definition, not generating instances and not using dictionary style passing for the class. The function class_all_methods_inlined_for_target l env targ class_path checks, wether all methods of class_path are inlined for target targ.
val update_const_descr : Ast.l ->
       (Typed_ast.const_descr -> Typed_ast.const_descr) ->
       Types.const_descr_ref -> Typed_ast.env -> Typed_ast.env
update_const_descr l up c env updates the description of the constant c in environment env using the function up.
val c_env_store : Typed_ast.c_env ->
       Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
c_env_store c_env c_d stores the description c_d environment c_env. Thereby, a new unique reference is generated and returned along with the modified environment.
val c_env_save : Typed_ast.c_env ->
       Types.const_descr_ref option ->
       Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
c_env_save c_env c_ref_opt c_d is a combination of c_env_update and c_env_store. If c_ref_opt is given, c_env_update is called, otherwise c_env_store.

target-representations


val const_target_rep_to_loc : Typed_ast.const_target_rep -> Ast.l
const_target_rep_to_loc rep returns the location, at which rep is defined.
val const_target_rep_allow_override : Typed_ast.const_target_rep -> bool
const_target_rep_allow_override rep returns whether this representation can be redefined. Only auto-generated target-reps should be redefinable by the user.
val type_target_rep_to_loc : Types.type_target_rep -> Ast.l
type_target_rep_to_loc rep returns the location, at which rep is defined.
val type_target_rep_allow_override : Types.type_target_rep -> bool
type_target_rep_allow_override rep returns whether this representation can be redefined. Only auto-generated target-reps should be redefinable by the user.
val constant_descr_to_name : Target.target -> Typed_ast.const_descr -> bool * Name.t * Name.t option
constant_descr_to_name targ cd looks up the representation for target targ in the constant description cd. It returns a tuple (n_is_shown, n, n_ascii). The name n is the name of the constant for this target, n_ascii an optional ascii alternative. n_is_shown indiciates, whether this name is actually printed. Special representations or inline representation might have a name, that is not used for the output.
val const_descr_ref_to_ascii_name : Typed_ast.c_env -> Types.const_descr_ref -> Name.t
const_descr_ref_to_ascii_name env c tries to find a simple identifier for constant c. The exact identifier does not matter, but should somehow be familiar to the user. It looks up the constant names, ascii-representations and renamings for various backends. If everything fails, it just makes a name up.
val type_descr_to_name : Target.target -> Path.t -> Types.type_descr -> Name.t
type_descr_to_name targ ty td looks up the representation for target targ in the type description td. Since in constrast to constant-description, type-descriptions don't contain the full type-name, but only renamings, the orginal type-name is passed as argument ty. It is assumed that td really belongs to ty.
val constant_descr_rename : Target.non_ident_target ->
       Name.t ->
       Ast.l ->
       Typed_ast.const_descr -> Typed_ast.const_descr * (Ast.l * Name.t) option
const_descr_rename targ n' l' cd looks up the representation for target targ in the constant description cd. It then updates this description by renaming to the new name n' and new location l'. The updated description is returned along with information of where the constant was last renamed and to which name.
val mod_target_rep_rename : Target.non_ident_target ->
       string ->
       Name.t ->
       Ast.l ->
       Typed_ast.mod_target_rep Target.Targetmap.t ->
       Typed_ast.mod_target_rep Target.Targetmap.t
mod_descr_rename targ mod_name n' l' md updates the representation for target targ in the module description md by renaming to the new name n' and new location l'. In case a target representation was already present, a type-check error is raised.
val type_descr_rename : Target.non_ident_target ->
       Name.t ->
       Ast.l -> Types.type_descr -> Types.type_descr * (Ast.l * Name.t) option
type_descr_rename targ n' l' td looks up the representation for target targ in the type description td. It then updates this description by renaming to the new name n' and new location l'. The updated description is returned along with information of where the type was last renamed and to which name.
val type_defs_rename_type : Ast.l ->
       Types.type_defs ->
       Path.t -> Target.non_ident_target -> Name.t -> Types.type_defs
type_def_rename_type l d p t n renames the type with path p in the defs d to the name n for target t. Renaming means that the module structure is kept. Only the name is changed.
val const_descr_has_target_rep : Target.target -> Typed_ast.const_descr -> bool
const_descr_has_target_rep targ d checks whether the description d contains a target-representation for target targ.

Constructing, checking and destructing expressions


val mk_name_lskips_annot : Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.name_lskips_annot
mk_name_lskips_annot creates an annoted name
val dest_var_exp : Typed_ast.exp -> Name.t option
Destructor for variable expressions
val is_var_exp : Typed_ast.exp -> bool
is_var_exp e checks whether e is a variable expression
val dest_tup_exp : int option -> Typed_ast.exp -> Typed_ast.exp list option
Destructor for tuple expressions. Similar to pattern destructors for tuples an optional argument to check the number of elements of the tuple.
val is_tup_exp : int option -> Typed_ast.exp -> bool
is_tup_exp s_opt e checks whether e is a tuple of size s_opt.
val is_var_tup_exp : Typed_ast.exp -> bool
is_var_tup_exp e checks, whether e is an expression consisting only of variables and tuples. I.e. simple variable expressions, tuples containing only variables and tuples containing other variable-tuples are accepted.
val mk_tf_exp : bool -> Typed_ast.exp
mk_tf_exp creates true and false expressions.
val dest_tf_exp : Typed_ast.exp -> bool option
dest_tf_exp destructs true and false expressions.
val is_tf_exp : bool -> Typed_ast.exp -> bool
is_tf_exp v e checks whether e is a true or false expression.
val dest_const_exp : Typed_ast.exp -> Types.const_descr_ref Types.id option
Destructor for constants expressions
val is_const_exp : Typed_ast.exp -> bool
is_const_exp e checks whether e is a constant expression
val dest_num_exp : Typed_ast.exp -> int option
dest_num_exp e destructs a number literal expression.
val is_num_exp : Typed_ast.exp -> bool
is_num_exp checks whether e is a number literal expression.
val mk_num_exp : Types.t -> int -> Typed_ast.exp
mk_num_exp creates a number literal expression.
val is_empty_backend_exp : Typed_ast.exp -> bool
is_empty_backend_exp checks whether the expression is ``
val mk_eq_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_eq_exp env e1 e2 constructs the expression e1 = e2. The environment env is needed to lookup the equality constant.
val mk_and_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_and_exp env e1 e2 constructs the expression e1 && e2. The environment env is needed to lookup the conjunction constant.
val mk_and_exps : Typed_ast.env -> Typed_ast.exp list -> Typed_ast.exp
mk_and_exps env es constructs the conjunction of all expressions in es. The environment env is needed to lookup the conjunction constant.
val mk_le_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_le_exp env e1 e2 constructs the expression e1 <= e2. The environment env is needed to lookup the less-equal constant.
val mk_sub_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_sub_exp env e1 e2 constructs the expression e1 - e2. The environment env is needed to lookup the subtraction constant.
val mk_from_list_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp
mk_from_list_exp env e constructs the expression Set.from_list e. The environment env is needed to lookup the from-list constant.
val mk_cross_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_cross_exp env e1 e2 constructs the expression cross e1 e2. The environment env is needed to lookup the cross constant.
val mk_set_sigma_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_set_sigma_exp env e1 e2 constructs the expression set_sigma e1 e2. The environment env is needed to lookup the sigma constant.
val mk_set_filter_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_set_filter_exp env e_P e_s constructs the expression Set.filter e_P e_s. The environment env is needed to lookup the constant.
val mk_set_image_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_set_image_exp env e_f e_s constructs the expression Set.image e_f e_s. The environment env is needed to lookup the constant.
val mk_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
mk_fun_exp [p1, ..., pn] e constructs the expression fun p1 ... pn -> e.
val mk_opt_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
mk_opt_fun_exp pL e returns mk_fun_exp pL e if pL is not empty and e otherwise.
val mk_app_exp : Ast.l -> Types.type_defs -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_app_exp d e1 e2 constructs the expression e1 e2. The type definitions d are needed for typechecking.
val mk_list_app_exp : Ast.l ->
       Types.type_defs -> Typed_ast.exp -> Typed_ast.exp list -> Typed_ast.exp
mk_list_app_exp d f [a1 ... an] constructs the expression f a1 ... an by repeatedly calling mk_app_exp.
val mk_eta_expansion_exp : Types.type_defs -> Name.t list -> Typed_ast.exp -> Typed_ast.exp
mk_eta_expansion_exp d vars e for variables vars = [x1, ..., xn] tries to build the expression fun x1 ... xn -> (e x1 ... xn). The variable names might be changed to ensure that they are distinct to each other and all variables already present in e.
val mk_paren_exp : Typed_ast.exp -> Typed_ast.exp
mk_paren_exp e adds parenthesis around expression e. Standard whitespaces are applied. This means that whitespace (except comments) are deleted before expression e.
val mk_opt_paren_exp : Typed_ast.exp -> Typed_ast.exp
mk_opt_paren_exp e adds parenthesis around expression e if it seems sensible. For parenthesis, variable expressions and tuples, the parenthesis are skipped, though.
val may_need_paren : Typed_ast.exp -> bool
may_need_paren e checks, whether e might need parenthesis. If returns, whether mk_opt_paren_exp e would modify the expression.
val mk_case_exp : bool ->
       Ast.l ->
       Typed_ast.exp ->
       (Typed_ast.pat * Typed_ast.exp) list -> Types.t -> Typed_ast.exp
mk_case_exp final l e rows ty constructs a case (match) expression. In contrast to Typed_ast.mk_case it uses standard spacing and adds parenthesis.
val mk_let_exp : Ast.l -> Name.t * Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_let_exp l (n, e1) e2 constructs the expression let n = e1 in e2 using default spacing.
val mk_if_exp : Ast.l -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
mk_if_exp l c e_t e_f constructs the expression if c then e_t else e_f using default spacing.
val mk_undefined_exp : Ast.l -> string -> Types.t -> Typed_ast.exp
mk_undefined_exp l m ty constructs an undefined expression of type ty with message m.
val mk_dummy_exp : Types.t -> Typed_ast.exp
mk_dummy_exp ty constructs a dummy expression of type ty. This is an expression that should never be looked at. It is only guaranteed to be an expression of this type.
val dest_app_exp : Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp) option
dest_app_exp e tries to destruct an function application expression e.
val strip_app_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
strip_app_exp e tries to destruct multiple function applications. It returns a pair (base_fun, arg_list) such that e is of the form base_fun arg_list_1 ... arg_list_n. If e is not a function application expression, the list arg_list is empty.
val dest_infix_exp : Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp * Typed_ast.exp) option
dest_infix_exp e tries to destruct an infix expression e. If e is of the form l infix_op r then Some (l, infix_op, r) is returned, otherwise None.
val is_infix_exp : Typed_ast.exp -> bool
is_infix_exp e checks whether e is an infix operation
val strip_infix_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
strip_infix_exp e is similar to dest_infix_exp, but returns the result in the same way as strip_app_exp. If e is of the form l infix_op r then (infix_op, [l;r]) is returned, otherwise (e, []).
val strip_app_infix_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list * bool
strip_app_infix_exp e is a combination of strip_infix_exp and strip_app_exp. The additional boolean result states, whether e is an infix operation. If e is an infix operation strip_infix_exp is called and the additional boolean result is true. Otherwise strip_app_exp is called and the result is set to false.

Constructing, checking and destructing definitions


val is_type_def_abbrev : Typed_ast.def -> bool
is_type_def_abbrev d checks whether the definition d is a type-abbreviation definition.
val is_type_def_record : Typed_ast.def -> bool
is_type_def_abbrev d checks whether the definition d is a definition of a record_type.

Collecting information about uses constants, types, modules ...



type used_entities = {
   used_consts : Types.const_descr_ref list;
   used_consts_set : Types.Cdset.t;
   used_types : Path.t list;
   used_types_set : Types.Pset.t;
   used_modules : Path.t list;
   used_modules_set : Types.Pset.t;
   used_tnvars : Types.TNset.t;
}
The type used_entities collects lists of used constant references, modules and types of some expression, definition, pattern ... used_entities is using lists, because the order in which entities occur might be important for renaming. However, these lists should not contain duplicates.
val empty_used_entities : used_entities
An empty collection of entities
val add_exp_entities : used_entities ->
       Typed_ast.exp -> used_entities
val add_def_aux_entities : Target.target ->
       bool ->
       used_entities ->
       Typed_ast.def_aux -> used_entities
add_def_aux_entities targ only_new ue def adds all the modules, types, constants ... used by definition def for target targ to ue. If the flag only_new is set, only the newly defined are added. Notice, that the identity backend won't throw parts of modules away. Therefore the result for the identiy backend is the union of the results for all other backends.
val add_def_entities : Target.target ->
       bool ->
       used_entities ->
       Typed_ast.def -> used_entities
add_def_entities is called add_def_aux_entities after extracting the appropriate def_aux.
val get_checked_modules_entities : Target.target ->
       bool -> Typed_ast.checked_module list -> used_entities
get_checked_module_entities targ only_new ml gets all the modules, types, constants ... used by modules ml for target targ. If the flag only_new is set, only the newly defined are returned. Notice, that the identity backend won't throw parts of modules away. Therefore the result for the identiy backend is the union of the results for all other backends.

Miscellaneous


val remove_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
remove_init_ws should be used with function like Typed_ast.alter_init_lskips. It removes whitespace expect comments.
val drop_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
drop_init_ws should be used with function like Typed_ast.alter_init_lskips. It removes whitespace including comments.
val space_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
space_init_ws should be used with function like Typed_ast.alter_init_lskips. It replaces whitespace including comments with a single space.
val space_com_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
space_com_init_ws should be used with function like Typed_ast.alter_init_lskips. It replaces whitespace except comments with a single space.
val strip_paren_typ_exp : Typed_ast.exp -> Typed_ast.exp
strip_paren_typ_exp e strips parenthesis and type-annotations form expression e. Warning: This might delete white-space!
val is_recursive_def : Typed_ast.def_aux -> bool * bool
is_recursive_def d checks whether d is recursive. It returns a pair of booleans (is_syntactic_rec, is_real_rec). The flag is_syntactic_rec states, whether the definition was made using the rec-keyword. The flag is_real_rec states, whether the function actually appears inside its own definition.
val try_termination_proof : Target.target -> Typed_ast.c_env -> Typed_ast.def_aux -> bool * bool * bool
try_termination_proof targ c_env d calls is_recursive_def d. It further checks, whether a termination proof for target targ should be tried by checking the termination settings of all involved constants. It returns a triple (is_syntactic_rec, is_real_rec, try_auto_termination).
val is_pp_loc : Ast.l -> bool
is_pp_loc l checks whether l is of the form Ast.Trans (true, _, _). This means that the entity marked with l should be formated using a pretty printer that calculates whitespaces new instead of using the ones provided by the user.
val is_pp_exp : Typed_ast.exp -> bool
val is_pp_def : Typed_ast.def -> bool
val val_def_get_name : Typed_ast.val_def -> Name.t option
val_def_get_name d tries to extract the name of the defined function.
val val_def_get_class_constraints_no_target_rep : Typed_ast.env ->
       Target.target -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
val_def_get_class_constraints_no_target_rep env targ vd collects the class constraints of all top-level function definitions in vd, which don't have a target-specific representation for target targ. Warning: contraints may appear multiple times in the resulting list
val val_def_get_class_constraints : Typed_ast.env -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
val_def_get_class_constraints env vd collects the class constraints of all top-level function definitions in vd. Warning: contraints may appear multiple times in the resulting list
val val_def_get_free_tnvars : Typed_ast.env -> Typed_ast.val_def -> Types.TNset.t
val_def_get_free_tnvars env vd returns the set of all free type-variables used by vd.
val env_tag_to_string : Typed_ast.env_tag -> string
env_tag_to_string tag formats tag as a string. This functions should only be used for human-readable output in e.g. error-messages.
val constr_family_to_id : Ast.l ->
       Typed_ast.env ->
       Types.t ->
       Types.constr_family_descr ->
       (Types.const_descr_ref Types.id list *
        (Types.t -> Types.const_descr_ref Types.id) option)
       option
constr_family_to_id l env ty cf tries to instantiate the constructor family cf to be used on a match statement where the matched type is ty. If it succeeeds the properly instantiated construtor ids + the instantiated case split function is returned. However, returning the case-split function is a bit complicated. It depends on the return type of match expression as well. Moreover, it might not be there at all, if the targets build-in pattern matching should be used to construct one. Therefore, an optional function from a type (the return type) to an id is returned for the case-split function.
val check_constr_family : Ast.l -> Typed_ast.env -> Types.t -> Types.constr_family_descr -> unit
check_constr_family is similar to constr_family_to_id. It does not return the instantiations though, but produces a nicely formatted error, in case no such instantiations could be found.
val check_for_inline_cycles : Target.target -> Typed_ast.c_env -> unit
check_for_inline_cycles targ env checks whether any constant in env would be inlined (possible over several steps) onto itself. If this happens, an exception is thrown.