module Def_trans:sig
..end
typedef_macro =
Name.t list ->
Typed_ast.env -> Typed_ast.def -> (Typed_ast.env * Typed_ast.def list) option
def_macro
is the type of definition macros. A definition macro def_mac
gets the arguments
rev_path
, env
and d
. The argument d
is the definition the macro should process.
rev_path
represents the path of the module of definition d
as a list of names in reverse order.
env
is the local environment for the module of d
. This means that also the definitions in
the same module that follow d
are present. If the macro does not modify the definition, it should
return None
. Otherwise, it should return a pair Some (env', ds)
, where env'
is a updated environment
and ds
a list of definitions that replace d
.val list_to_mac : def_macro list -> def_macro
list_to_mac macro_list
collapses a list of def_macros
into a single one.
It looks for the first macro in the list that succeeds, i.e. returns not None
and
returns the result of this macro.val process_defs : Name.t list ->
def_macro ->
Name.t ->
Typed_ast.env -> Typed_ast.def list -> Typed_ast.env * Typed_ast.def list
process_defs rev_path def_mac mod_name env ds
is intended to run the macro def_mac
over all
definitions in module mod_name
. The argument rev_path
is the path to module mod_name
in reversed order.
env
is the environment containing module mod_name
and ds
is the list of definitions in this module.
If def_mac
modifies a definition d
to a list ds
, it is then run on all definitions in ds
.
If one of the is a module-definition, which is not modified by ds
, then def_macro
is run
on all definitions inside this module. For this recursive call the path, module name and environment are adapted.
The result of process_defs
is an updated environment and a new list of definitons.
val class_to_record : Target.target -> def_macro
def_macro
class_to_record
takes a
definition of a type class and turns it into a definition of a record type. The methods of the
class become field of the record. This record can then be used as the dictionary type for the
dictionary passing.val comment_out_inline_instances_and_classes : Target.target -> def_macro
val instance_to_dict : bool -> Target.target -> def_macro
instance_to_dict do_inline targ
turns instance declarations into a definition of a dictionary record.
If do_inline
is set, this definition will be inlined (for this the target argument is needed).val class_constraint_to_parameter : Target.target -> def_macro
val remove_opens : def_macro
remove_opens
removes all open / include and import statementsval remove_import_include : def_macro
remove_import_include
removes all import and include statements. Imports are deleted and
includes turned into open statements.val remove_import : def_macro
remove_import
removes all import statements.val remove_module_renames : def_macro
remove_module_renames
removes all module rename statements.val remove_types_with_target_rep : Target.target -> def_macro
val defs_with_target_rep_to_lemma : Typed_ast.env -> Target.target -> def_macro
val remove_vals : def_macro
val remove_indrelns : def_macro
val remove_indrelns_true_lhs : def_macro
val remove_classes : def_macro
val type_annotate_definitions : def_macro
val nvar_to_parameter : def_macro
val prune_target_bindings : Target.non_ident_target -> Typed_ast.def list -> Typed_ast.def list