Extraction_plugin.Miniml
module InfvInst : sig ... end
type signature = sign list
type ml_schema = int * ml_type
type ml_ind_packet = {
ip_typename : Names.Id.t; |
ip_typename_ref : global; |
ip_consnames : Names.Id.t array; |
ip_consnames_ref : global array; |
ip_logical : bool; |
ip_sign : signature; |
ip_vars : Names.Id.t list; |
ip_types : ml_type list array; |
}
type ml_ind = {
ind_kind : inductive_kind; |
ind_nparams : int; |
ind_packets : ml_ind_packet array; |
ind_equiv : equiv; |
}
We now store some typing information on constructors and cases to avoid type-unsafe optimisations. This will be either the type of the applied constructor or the type of the head of the match.
Nota : the constructor MLtuple
and the extension of MLcase
to general patterns have been proposed by P.N. Tollitte for his Relation Extraction plugin. MLtuple
is currently not used by the main extraction, as well as deep patterns.
type ml_branch = ml_ident list * ml_pattern * ml_ast
and ml_ast =
| MLrel of int |
| MLapp of ml_ast * ml_ast list |
| MLlam of ml_ident * ml_ast |
| MLletin of ml_ident * ml_ast * ml_ast |
| MLglob of global |
| MLcons of ml_type * global * ml_ast list |
| MLtuple of ml_ast list |
| MLcase of ml_type * ml_ast * ml_branch array |
| MLfix of int * Names.Id.t array * ml_ast array |
| MLexn of string |
| MLdummy of kill_reason |
| MLaxiom of string |
| MLmagic of ml_ast |
| MLuint of Uint63.t |
| MLfloat of Float64.t |
| MLstring of Pstring.t |
| MLparray of ml_ast array * ml_ast |
and ml_pattern =
| Pcons of global * ml_pattern list | |
| Ptuple of ml_pattern list | |
| Prel of int | (* Cf. the idents in the branch. |
| Pwild | |
| Pusual of global | (* Shortcut for Pcons (r, |
and ml_module_type =
| MTident of Names.ModPath.t |
| MTfunsig of Names.MBId.t * ml_module_type * ml_module_type |
| MTsig of Names.ModPath.t * ml_module_sig |
| MTwith of ml_module_type * ml_with_declaration |
and ml_with_declaration =
| ML_With_type of InfvInst.t * Names.Id.t list * Names.Id.t list * ml_type |
| ML_With_module of Names.Id.t list * Names.ModPath.t |
and ml_module_sig = (Names.Label.t * ml_specif) list
and ml_module_expr =
| MEident of Names.ModPath.t |
| MEfunctor of Names.MBId.t * ml_module_type * ml_module_expr |
| MEstruct of Names.ModPath.t * ml_module_structure |
| MEapply of ml_module_expr * ml_module_expr |
and ml_module_structure = (Names.Label.t * ml_structure_elem) list
type ml_structure = (Names.ModPath.t * ml_module_structure) list
type ml_signature = (Names.ModPath.t * ml_module_sig) list
type 's language_descr = {
keywords : Names.Id.Set.t; |
file_suffix : string; |
file_naming : 's -> Names.ModPath.t -> string; |
preamble : 's -> Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t; |
pp_struct : 's -> ml_structure -> Pp.t; |
sig_suffix : string option; |
sig_preamble : 's -> Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t; |
pp_sig : 's -> ml_signature -> Pp.t; |
pp_decl : 's -> ml_decl -> Pp.t; |
}