Previous  Up  Next

Module Typed_ast


module Typed_ast: sig .. end
Sets of Names
module NameSet: Set.S  with type elt = Name.t and type t = Set.Make(Name).t
Sets of Names 
module Nfmap: Finite_map.Fmap  with type k = Name.t
Name keyed finite maps 
val nfmap_domain : 'a Nfmap.t -> NameSet.t
type name_l = Name.lskips_t * Ast.l 
type lskips = Ast.lex_skips
Whitespace, comments, and newlines
type 'a lskips_seplist = ('a, lskips) Seplist.t 
val no_lskips : lskips
The empty lskip
val space : lskips
A space lskip
val lskips_only_comments : lskips list -> lskips
Get only the comments (and a trailing space)
val lskips_only_comments_first : lskips list -> lskips
Get the first lskip of the list and only comments from the rest

type env_tag =
| K_let (*A let definition, the most common case. Convers val as well, details see above.*)
| K_field (*A field*)
| K_constr (*A type constructor*)
| K_relation (*A relation*)
| K_method (*A class method*)
| K_instance (*A method instance*)
env_tag is used by const_descr to describe the type of constant. Constants can be defined in multiple ways: the most common way is via a let-statement. Record-type definitions introduce fields-accessor functions and variant types introduce constructors. There are methods, instances and relations as well. A let definition can be made via a val definition and multiple, target specific lets.
type p_env = (Path.t * Ast.l) Nfmap.t
Maps a type name to the unique path representing that type and the first location this type is defined
type lit = (lit_aux, unit) Types.annot

type lit_aux =
| L_true of lskips
| L_false of lskips
| L_zero of lskips (*This is a bit, not a num*)
| L_one of lskips (*see above*)
| L_numeral of lskips * int (*A numeral literal, it has fixed type "numeral" and is used in patterns and after translating L_num to it.*)
| L_num of lskips * int (*A number literal. This is like a numeral one wrapped with the "from_numeral" function*)
| L_char of lskips * char
| L_string of lskips * string
| L_unit of lskips * lskips
| L_vector of lskips * string * string (*For vectors of bits, specified with hex or binary, first string is either 0b or 0x, second is the binary or hex number as a string*)
| L_undefined of lskips * string (*A special undefined value that explicitly states that nothing is known about it. This is useful for expressing underspecified functions. It has been introduced to easier support pattern compilation of non-exhaustive patterns.*) 
type const_descr_ref = Types.const_descr_ref

type name_kind =
| Nk_typeconstr of Path.t
| Nk_const of const_descr_ref
| Nk_constr of const_descr_ref
| Nk_field of const_descr_ref
| Nk_module of Path.t
| Nk_class of Path.t 
type pat = (pat_aux, pat_annot) Types.annot

type pat_annot = {
   pvars : Types.t Nfmap.t;
}
type pat_aux =
| P_wild of lskips
| P_as of lskips * pat * lskips * name_l
* lskips
| P_typ of lskips * pat * lskips * Types.src_t
* lskips
| P_var of Name.lskips_t
| P_const of const_descr_ref Types.id * pat list
| P_backend of lskips * Ident.t * Types.t * pat list
| P_record of lskips
* (const_descr_ref Types.id * lskips * pat)
lskips_seplist * lskips
| P_vector of lskips * pat lskips_seplist * lskips
| P_vectorC of lskips * pat list * lskips
| P_tup of lskips * pat lskips_seplist * lskips
| P_list of lskips * pat lskips_seplist * lskips
| P_paren of lskips * pat * lskips
| P_cons of pat * lskips * pat
| P_num_add of name_l * lskips * lskips * int
| P_lit of lit
| P_var_annot of Name.lskips_t * Types.src_t (*A type-annotated pattern variable. This is redundant with the combination of the P_typ and P_var cases above, but useful as a macro target.*)

type cr_special_fun =
| CR_special_uncurry of int (*CR_special_uncurry n formats a function with n arguments curried, i.e. turn the arguments into a tupled argument, surrounded by parenthesis and separated by ","*)
| CR_special_rep of string list * exp list (*CR_special_rep sr args encodes a user given special representation. replace the arguments in the expression list and then interleave the results with sr*)

type const_target_rep =
| CR_inline of Ast.l * bool * name_lskips_annot list * exp (*CR_inline (loc, allow_override, vars, e) means inlining the constant with the expression e and replacing the variable vars inside e with the arguments of the constant. The flag allow_override signals whether the declaration might be safely overriden. Automatically generated target-representations (e.g. for ocaml constructors) should be changeable by the user, whereas multiple user-defined ones should cause a type error.*)
| CR_infix of Ast.l * bool * Ast.fixity_decl * Ident.t (*CR_infix (loc, allow_override, fixity, i) declares infix notation for the constant with the giving identifier.*)
| CR_undefined of Ast.l * bool (*CR_undefined (loc, allow_override) declares undefined constant.*)
| CR_simple of Ast.l * bool * name_lskips_annot list * exp (*CR_simple (loc, allow_override, vars, e) is similar to CR_inline. Instead of inlining during macro expansion and therefore allowing further processing afterwards, CR_simple performs the inlining only during printing in the backend.*)
| CR_special of Ast.l * bool * cr_special_fun * name_lskips_annot list (*CR_special (loc, allow_override, to_out, vars) describes special formating of this constant. The (renamed) constant (including path prefix) and all arguments are transformed to output. to_out represents a function that is then given the formatted name and the appropriate number of these outputs. The expected arguments are described by vars. If there are more arguments than variables, they are appended. If there are less, for expressions local functions are introduced. For patterns, an exception is thrown. Since values of const_target_rep need to be written out to file via output_value in order to cache libraries, it cannot be a function of type Output.t list -> Output.t list directly. Instead, the type cr_special_fun is used as an indirection.*)

type rel_io =
| Rel_mode_in
| Rel_mode_out
rel_io represents whether an argument of an inductive relation is considerred as an input or an output
type rel_mode = rel_io list
rel_output_type specifies the type of the result

type rel_output_type =
| Out_list (*Return a list of possible outputs*)
| Out_pure (*Return one possible output or fail if no such output exists*)
| Out_option (*Return one possible output or None if no such output exists*)
| Out_unique (*Return the output if it is unique or None otherwise*)

type rel_info = {
   ri_witness : (Path.t * const_descr_ref Nfmap.t) option; (*Contains the path of the witness type and a mapping from rules to constructors. None if no witness type has been generated*)
   ri_check : const_descr_ref option; (*A reference to the witness checking function or None if it is not generated*)
   ri_fns : ((rel_mode * bool * rel_output_type) *
const_descr_ref)
list;		 (*A list of functions generated from the relation together with their modes*)
}
rel_info represents information about functions and types genereated from this relation 0

type const_descr = {
   const_binding : Path.t; (*The path to the definition*)
   const_tparams : Types.tnvar list; (*Its type parameters. Must have length 1 for class methods.*)
   const_class : (Path.t * Types.tnvar) list; (*Its class constraints (must refer to above type parameters). Must have length 1 for class methods*)
   const_no_class : const_descr_ref Target.Targetmap.t; (*If the constant has constraints, i.e. const_class is not empty, we need another constant without constraints for dictionary passing. This field stores the reference to this constant, if one such constant has aready been generated.*)
   const_ranges : Types.range list; (*Its length constraints (must refer to above type parameters). Can be equality or GtEq inequalities*)
   const_type : Types.t; (*Its type*)
   relation_info : rel_info option; (*If the constant is a relation, it might contain additional information about this relation. However, it might be None for some relations as well.*)
   env_tag : env_tag; (*What kind of definition it is.*)
   const_targets : Target.Targetset.t; (*The set of targets the constant is defined for.*)
   spec_l : Ast.l; (*The location for the first occurrence of a definition/specification of this constant.*)
   target_rename : (Ast.l * Name.t) Target.Targetmap.t; (*Target-specific renames of for this constant.*)
   target_ascii_rep : (Ast.l * Name.t) Target.Targetmap.t; (*Optional ASCII representation for this constant.*)
   target_rep : const_target_rep Target.Targetmap.t; (*Target-specific representation of for this constant*)
   compile_message : string Target.Targetmap.t; (*An optional warning message that should be printed, if the constant is used*)
   termination_setting : Ast.termination_setting Target.Targetmap.t; (*Can termination be proved automatically by various backends?*)
}
The description of a top-level definition
type v_env = const_descr_ref Nfmap.t 
type f_env = const_descr_ref Nfmap.t 
type m_env = Path.t Nfmap.t 
type e_env = mod_descr Types.Pfmap.t 
type c_env
local_env represents local_environments, i.e. essentially maps from names to the entities they represent

type local_env = {
   m_env : m_env; (*module map*)
   p_env : p_env; (*type map*)
   f_env : f_env; (*field map*)
   v_env : v_env; (*constructor and constant map*)
}
type env = {
   local_env : local_env; (*the current local environment*)
   c_env : c_env; (*global map from constant references to the constant descriptions*)
   t_env : Types.type_defs; (*global type-information*)
   i_env : Types.i_env; (*global instances information*)
   e_env : e_env; (*global map from module paths to the module descriptions*)
}
type mod_target_rep =
| MR_rename of Ast.l * Name.t (*Rename the module*)

type mod_descr = {
   mod_binding : Path.t; (*The full path of this module*)
   mod_env : local_env; (*The local environment of the module*)
   mod_target_rep : mod_target_rep Target.Targetmap.t; (*how to represent the module for different backends*)
   mod_filename : string option; (*the filename the module is defined in (if it is a top-level module)*)
   mod_in_output : bool; (*is this module written to a file (true) or an existing file used (false) ?*)
} 
type exp

type exp_subst =
| Sub of exp
| Sub_rename of Name.t

type exp_aux = private
| Var of Name.lskips_t
| Backend of lskips * Ident.t (*An identifier that should be used literally by a backend. The identifier does not contain whitespace. Initial whitespace is represented explicitly.*)
| Nvar_e of lskips * Nvar.t
| Constant of const_descr_ref Types.id
| Fun of lskips * pat list * lskips * exp
| Function of lskips
* (pat * lskips * exp * Ast.l)
lskips_seplist * lskips
| App of exp * exp
| Infix of exp * exp * exp (*The middle exp must be a Var, Constant, or Constructor*)
| Record of lskips * fexp lskips_seplist * lskips
| Recup of lskips * exp * lskips
* fexp lskips_seplist * lskips
| Field of exp * lskips * const_descr_ref Types.id
| Vector of lskips * exp lskips_seplist * lskips
| VectorSub of exp * lskips * Types.src_nexp * lskips
* Types.src_nexp * lskips
| VectorAcc of exp * lskips * Types.src_nexp * lskips
| Case of bool * lskips * exp * lskips
* (pat * lskips * exp * Ast.l)
lskips_seplist * lskips		 (*The boolean flag as first argument is used to prevent pattern compilation from looping in rare cases. If set to true, no pattern compilation is tried. The default value is false.*)
| Typed of lskips * exp * lskips * Types.src_t
* lskips
| Let of lskips * letbind * lskips * exp
| Tup of lskips * exp lskips_seplist * lskips
| List of lskips * exp lskips_seplist * lskips
| Paren of lskips * exp * lskips
| Begin of lskips * exp * lskips
| If of lskips * exp * lskips * exp
* lskips * exp
| Lit of lit
| Set of lskips * exp lskips_seplist * lskips
| Setcomp of lskips * exp * lskips * exp
* lskips * NameSet.t
| Comp_binding of bool * lskips * exp * lskips * lskips
* quant_binding list * lskips * exp
* lskips		 (*true for list comprehensions, false for set comprehensions*)
| Quant of Ast.q * quant_binding list * lskips * exp
| Do of lskips * Path.t Types.id * do_line list
* lskips * exp * lskips
* (Types.t * bind_tyargs_order)		 (*The last argument is the type of the value in the monad*)

type do_line =
| Do_line of (pat * lskips * exp * lskips)

type bind_tyargs_order =
| BTO_input_output (*['a, 'b]*)
| BTO_output_input (*['b, 'a]*)
A bind constant of a monad M has type M 'a -> ('a -> M 'b) -> M 'b. Here, I call 'a the input type and 'b the output type. Depending on how the bind constant is defined in detail its free type variable list (stored in constant-description record, field const_tparams) might be either of the form ['a, 'b] or ['b, 'a]. This type is used to distinguish the two possibilities.
type fexp = const_descr_ref Types.id * lskips * exp * Ast.l 
type name_lskips_annot = (Name.lskips_t, unit) Types.annot

type quant_binding =
| Qb_var of name_lskips_annot
| Qb_restr of bool * lskips * pat * lskips * exp
* lskips		 (*true for list quantifiers, false for set quantifiers*) 
type funcl_aux = name_lskips_annot * const_descr_ref *
       pat list * (lskips * Types.src_t) option *
       lskips * exp 
type letbind = letbind_aux * Ast.l

type letbind_aux =
| Let_val of pat * (lskips * Types.src_t) option * lskips
* exp		 (*Let_val (p, ty_opt, sk, e) describes binding the pattern p to exp e in a local let statement, i.e. a statement like let p = e in ...*)
| Let_fun of name_lskips_annot * pat list
* (lskips * Types.src_t) option * lskips
* exp		 (*Let_fun (n, ps, ty_opt, sk, e) describes defining a local function f with arguments ps locally. It repre0sents a statement like let n ps = e in .... Notice that the arguments of Let_fun are similar to funcl_aux. However, funcl_aux has a constant-references, as it is used in top-level definitions, whereas Let_fun is used only for local functions.*) 
type tyvar = lskips * Ulib.Text.t * Ast.l 
type nvar = lskips * Ulib.Text.t * Ast.l

type tnvar =
| Tn_A of tyvar
| Tn_N of nvar

type texp =
| Te_opaque (*introduce just a new type name without definition*)
| Te_abbrev of lskips * Types.src_t (*a type abbreviation with the type Te_abbrev*)
| Te_record of lskips * lskips
* (name_l * const_descr_ref * lskips *
Types.src_t)
lskips_seplist * lskips		 (*Te_record (_, _, field_list, _) defines a record type. The fields and their types are stored in field_list. The entries of field_list consist of the name of the field, the reference to it's constant description and the type of the field as well as white-spaces.*)
| Te_variant of lskips
* (name_l * const_descr_ref * lskips *
Types.src_t lskips_seplist)
lskips_seplist		 (*Te_variant (_, _, constr_list, _) defines a variant type. The constructors and their types are stored in constr_list. The entries of constr_list consist of the name of the constructor, the reference to it's constant description and the type of it's arguments as well as white-spaces.*)
Type exepressions for defining types

type range =
| GtEq of Ast.l * Types.src_nexp * lskips * Types.src_nexp
| Eq of Ast.l * Types.src_nexp * lskips * Types.src_nexp

type constraints =
| Cs_list of (Ident.t * tnvar) lskips_seplist
* lskips option * range lskips_seplist
* lskips

type constraint_prefix =
| Cp_forall of lskips * tnvar list * lskips
* constraints option		 
type typschm = constraint_prefix option * Types.src_t 
type instschm = constraint_prefix option * lskips * Ident.t * Path.t *
       Types.src_t * lskips
Instance Scheme, constraint prefix, sk, class-ident as printed, resolved class-path the id points to, instantiation type, sk
val cr_special_fun_uses_name : cr_special_fun -> bool
cr_special_fun_uses_name f checks, whether f uses it's first argument, i.e. whether it uses the formatted name of the constant. This information is important to determine, whether the constant needs to be renamed.
type targets_opt = (bool * lskips * Ast.target lskips_seplist *
        lskips)
       option
targets_opt is represents a set of targets. There are 3 types of values 
val in_targets_opt : Target.target -> targets_opt -> bool
in_targets_opt targ targets_opt checks whether the target `targ` is in the set of targets represented by `targets_opt`. If targ is the a human readable target, true is returned.
val in_target_set : Target.target -> Target.Targetset.t -> bool
in_target_set targ targetset checks whether the target `targ` is in the set of targets targetset. It is intended for checking whether to output certain parts of the TAST. Therefore, in_target_set returns true for all human readable targets and only checks for others.
val targets_opt_to_list : targets_opt -> Target.non_ident_target list
target_opt_to_list targets_opt returns a distinct list of all the targets in the option.
type val_spec = lskips * name_l * const_descr_ref *
       Ast.ascii_opt * lskips * typschm 
type class_val_spec = lskips * targets_opt * name_l *
       const_descr_ref * Ast.ascii_opt * lskips * Types.src_t

type fun_def_rec_flag =
| FR_non_rec
| FR_rec of lskips
fun_def_rec_flag is used to encode, whether a Fun_def is recursive. The recursive one carries some whitespace for printing after the rec-keyword.

type val_def =
| Let_def of lskips * targets_opt
* (pat * (Name.t * const_descr_ref) list *
(lskips * Types.src_t) option * lskips *
exp)
| Fun_def of lskips * fun_def_rec_flag * targets_opt
* funcl_aux lskips_seplist		 (*Fun_def (sk1, rec_flag, topt, clauses) encodes a function definition, which might consist of multiple clauses.*)
| Let_inline of lskips * lskips * targets_opt
* name_lskips_annot * const_descr_ref
* name_lskips_annot list * lskips * exp

type name_sect =
| Name_restrict of (lskips * name_l * lskips * lskips *
string * lskips)

type indreln_rule_quant_name =
| QName of name_lskips_annot
| Name_typ of lskips * name_lskips_annot * lskips
* Types.src_t * lskips

type indreln_rule_aux =
| Rule of Name.lskips_t * lskips * lskips
* indreln_rule_quant_name list * lskips
* exp option * lskips * name_lskips_annot
* const_descr_ref * exp list
A rule of the form Rule(clause_name_opt, sk1, sk2, bound_vars, sk3, left_hand_side_opt, sk4, rel_name, c, args) encodes a clause clause_name: forall bound_vars. (left_hand_side ==> rel_name args). c is the reference of the relation rel_name.
type indreln_rule = indreln_rule_aux * Ast.l

type indreln_witness =
| Indreln_witness of lskips * lskips * Name.lskips_t * lskips
Name of the witness type to be generated

type indreln_indfn =
| Indreln_fn of Name.lskips_t * lskips * Types.src_t * lskips option
Name and mode of a function to be generated from an inductive relation

type indreln_name =
| RName of lskips * Name.lskips_t * const_descr_ref
* lskips * typschm * indreln_witness option
* (lskips * Name.lskips_t * lskips) option
* indreln_indfn list option * lskips
Type annotation for the relation and information on what to generate from it. RName(sk1, rel_name, rel_name_ref, sk2, rel_type, witness_opt, check_opt, indfns opt, sk3)

type target_rep_rhs =
| Target_rep_rhs_infix of lskips * Ast.fixity_decl * lskips * Ident.t (*Declaration of an infix constant*)
| Target_rep_rhs_term_replacement of exp (*the standard term replacement, replace with the exp for the given backend*)
| Target_rep_rhs_type_replacement of Types.src_t (*the standard term replacement, replace with the type for the given backend*)
| Target_rep_rhs_special of lskips * lskips * string * exp list (*fancy represenation of terms*)
| Target_rep_rhs_undefined (*undefined, don't throw a problem during typeching, but during output*)

type declare_def =
| Decl_compile_message of lskips * targets_opt * lskips
* const_descr_ref Types.id * lskips * lskips
* string		 (*Decl_compile_message_decl (sk1, targs, sk2, c, sk3, sk4, message), declares printing waring message message, if constant c is used for one of the targets in targs*)
| Decl_target_rep_term of lskips * Ast.target * lskips * Ast.component
* const_descr_ref Types.id * name_lskips_annot list
* lskips * target_rep_rhs		 (*Decl_target_rep_term (sk1, targ, sk2, comp, c, args, sk3, rhs) declares a target-representation for target targ and constant c with arguments args. Since fields and constant live in different namespaces, comp is used to declare whether a field or a constant is meant. The rhs constains details about the representation.*)
| Decl_target_rep_type of lskips * Ast.target * lskips * lskips
* Path.t Types.id * tnvar list * lskips * Types.src_t		 (*Decl_target_rep_type (sk1, targ, sk2, sk3, id, args, sk4, rhs) declares a target-representation. for target targ and type id with arguments args.*)
| Decl_ascii_rep of lskips * targets_opt * lskips * Ast.component
* name_kind Types.id * lskips * lskips
* Name.t
| Decl_rename of lskips * targets_opt * lskips * Ast.component
* name_kind Types.id * lskips * Name.lskips_t
| Decl_rename_current_module of lskips * targets_opt * lskips
* lskips * lskips * Name.lskips_t
| Decl_termination_argument of lskips * targets_opt * lskips
* const_descr_ref Types.id * lskips
* Ast.termination_setting
| Decl_pattern_match_decl of lskips * targets_opt * lskips
* Ast.exhaustivity_setting * Path.t Types.id * tnvar list
* lskips * lskips
* const_descr_ref Types.id lskips_seplist
* lskips * const_descr_ref Types.id option

type def_aux =
| Type_def of lskips
* (name_l * tnvar list * Path.t * texp *
name_sect option)
lskips_seplist		 (*Type_def (sk, sl) defines one or more types. The entries of sl are the type definitions. They contain a name of the type, the full path of the defined type, the free type variables, the main type definiton and restrictions on variable names of this type*)
| Val_def of val_def (*The list contains the class constraints on those variables*)
| Lemma of lskips * Ast.lemma_typ * targets_opt * name_l
* lskips * exp
| Module of lskips * name_l * Path.t * lskips
* lskips * def list * lskips
| Rename of lskips * name_l * Path.t * lskips
* Path.t Types.id		 (*Renaming an already defined module*)
| OpenImport of Ast.open_import * Path.t Types.id list (*open and/or import modules*)
| OpenImportTarget of Ast.open_import * targets_opt * (lskips * string) list (*open and/or import modules only for specific targets*)
| Indreln of lskips * targets_opt
* indreln_name lskips_seplist
* indreln_rule lskips_seplist		 (*Inductive relations*)
| Val_spec of val_spec
| Class of Ast.class_decl * lskips * name_l * tnvar
* Path.t * lskips * class_val_spec list
* lskips
| Instance of Ast.instance_decl * Types.instance_ref * instschm
* val_def list * lskips		 (*Instance (default?, instance_scheme, methods, sk2)*)
| Comment of def (*Does not appear in the source, used to comment out definitions for certain backends*)
| Declaration of declare_def (*Declarations that change the behaviour of lem, but have no semantic meaning*) 
type def = (def_aux * lskips option) * Ast.l * local_env
A definition consists of a the real definition represented as a def_aux, followed by some white-space. There is also the location of the definition and the local-environment present after the definition has been processed.
val tnvar_to_types_tnvar : tnvar -> Types.tnvar * Ast.l
val empty_local_env : local_env
val empty_env : env
val e_env_lookup : Ast.l -> e_env -> Path.t -> mod_descr
e_env_lookup l e_env p looks up the module with path p in environment e_env and returns the corresponding description. If this lookup fails, a fatal error is thrown using location l for the error message.
val c_env_lookup : Ast.l ->
       c_env -> const_descr_ref -> const_descr
c_env_lookup l c_env c_ref looks up the constant reference c_ref in environment c_env and returns the corresponding description. If this lookup fails, a fatal error is thrown using location l for the error message.
val c_env_store_raw : c_env ->
       const_descr -> c_env * const_descr_ref
c_env_store_raw 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. It stores the real c_d passed. The function c_env_store preprocesses c_d to add common features like for example capitalizing constructors for the Ocaml backend.
val c_env_update : c_env ->
       const_descr_ref -> const_descr -> c_env
c_env_update c_env c_ref c_d updates the description of constant c_ref with c_d in environment c_env.
val env_c_env_update : env ->
       const_descr_ref -> const_descr -> env
env_c_env_update env c_ref c_d updates the description of constant c_ref with c_d in environment env.
val c_env_all_consts : c_env -> const_descr_ref list
c_env_all_consts c_env returns the constants defined in c_env
val exp_to_locn : exp -> Ast.l
val exp_to_typ : exp -> Types.t
val append_lskips : lskips -> exp -> exp
append_lskips adds new whitespace/newline/comments to the front of an expression (before any existing whitespace/newline/comments in front of the expression)
val pat_append_lskips : lskips -> pat -> pat
val alter_init_lskips : (lskips -> lskips * lskips) ->
       exp -> exp * lskips
alter_init_lskips finds all of the whitespace/newline/comments preceding an expression and passes it to the supplied function in a single invocation. The preceding whitespace/newline/comments are replaced with the fst of the function's result, and the snd of the function's result is returned from alter_init_lskips
val pat_alter_init_lskips : (lskips -> lskips * lskips) ->
       pat -> pat * lskips
val def_aux_alter_init_lskips : (lskips -> lskips * lskips) ->
       def_aux -> def_aux * lskips
val def_alter_init_lskips : (lskips -> lskips * lskips) ->
       def -> def * lskips
val oi_alter_init_lskips : (lskips -> lskips * lskips) ->
       Ast.open_import -> Ast.open_import * lskips
val pp_const_descr : Format.formatter -> const_descr -> unit
val pp_env : Format.formatter -> env -> unit
val pp_local_env : Format.formatter -> local_env -> unit
val pp_c_env : Format.formatter -> c_env -> unit
val pp_instances : Format.formatter -> Types.instance list Types.Pfmap.t -> unit

type imported_modules =
| IM_paths of Path.t list
| IM_targets of targets_opt * string list

type checked_module = {
   filename : string;
   module_path : Path.t;
   imported_modules : imported_modules list;
   imported_modules_rec : imported_modules list;
   untyped_ast : Ast.defs * Ast.lex_skips;
   typed_ast : def list * Ast.lex_skips;
   generate_output : bool;
} 
type var_avoid_f = bool * (Name.t -> bool) * (Ulib.Text.t -> (Name.t -> bool) -> Name.t)
var_avoid_f is a type of a tuple (avoid_ty_vars, name_ok, do_rename). The flag avoid_ty_vars states, whether clashes with type variables should be avoided. The name_ok n checks whether the name n is OK. If it is not OK, the function do_rename n_text check renames n. As input it takes the text of n, a function check that checks whether the new name clashes with any names to be avoided or existing variable names in the context.
module type Exp_context = sig .. end
module Exps_in_context: 
functor (C : Exp_context) -> sig .. end
val local_env_union : local_env -> local_env -> local_env
val funcl_aux_seplist_group : funcl_aux lskips_seplist ->
       bool * lskips option *
       (Name.t * funcl_aux lskips_seplist) list
Mutually recursive function definitions may contain multiple clauses for the same function. These can however appear interleaved with clauses for other functions. funcl_aux_seplist_group seplist sorts the clauses according to the function names and states, whether any resorting was necessary. Moreover, the initial lskip is returned, if present.
val class_path_to_dict_name : Path.t -> Types.tnvar -> Name.t
class_path_to_dict_name cp tv creates a name for the class cp with type argument tv. This name is used during dictionary passing. If a function has a type constraint that type-variable tv is of type-class cp, the function call class_path_to_dict_name cp tv is used to generate the name of a new argument. This argument is a dictionary that is used to eliminate the use of type classes.

This design is very fragile and should probably be changed in the future! class_path_to_dict_name needs to generate names that globally do not clash with anything else, including names generated by class_path_to_dict_name itself. The generated name is independently used by both definition macros adding the argument to the definition and expression macros that use the added argument. The name used in both places has to coincide! Therefore, the name cannot be modified depending on the context. Renaming to avoid clashes with other arguments / local variables is not possible.

val ident_get_lskip : 'a Types.id -> Ast.lex_skips
val ident_replace_lskip : Types.ident_option -> Ast.lex_skips -> Types.ident_option
val oi_get_lskip : Ast.open_import -> Ast.lex_skips