Module Extraction_plugin.Miniml

type kill_reason =
| Ktype
| Kprop
| Kimplicit of Names.GlobRef.t * int
type sign =
| Keep
| Kill of kill_reason
type signature = sign list
type ml_type =
| Tarr of ml_type * ml_type
| Tglob of Names.GlobRef.t * ml_type list
| Tvar of int
| Tvar' of int
| Tmeta of ml_meta
| Tdummy of kill_reason
| Tunknown
| Taxiom
and ml_meta = {
id : int;
mutable contents : ml_type option;
}
type ml_schema = int * ml_type
type inductive_kind =
| Singleton
| Coinductive
| Standard
| Record of Names.GlobRef.t option list
type ml_ind_packet = {
ip_typename : Names.Id.t;
ip_consnames : Names.Id.t array;
ip_logical : bool;
ip_sign : signature;
ip_vars : Names.Id.t list;
ip_types : ml_type list array;
}
type equiv =
| NoEquiv
| Equiv of Names.KerName.t
| RenEquiv of string
type ml_ind = {
ind_kind : inductive_kind;
ind_nparams : int;
ind_packets : ml_ind_packet array;
ind_equiv : equiv;
}
type ml_ident =
| Dummy
| Id of Names.Id.t
| Tmp of Names.Id.t

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 Names.GlobRef.t
| MLcons of ml_type * Names.GlobRef.t * 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
| MLmagic of ml_ast
| MLuint of Uint63.t
| MLfloat of Float64.t
| MLparray of ml_ast array * ml_ast
and ml_pattern =
| Pcons of Names.GlobRef.t * ml_pattern list
| Ptuple of ml_pattern list
| Prel of int(*

Cf. the idents in the branch. Prel 1 is the last one.

*)
| Pwild
| Pusual of Names.GlobRef.t(*

Shortcut for Pcons (r,Prel n;...;Prel 1) *

*)
type ml_decl =
| Dind of Names.MutInd.t * ml_ind
| Dtype of Names.GlobRef.t * Names.Id.t list * ml_type
| Dterm of Names.GlobRef.t * ml_ast * ml_type
| Dfix of Names.GlobRef.t array * ml_ast array * ml_type array
type ml_spec =
| Sind of Names.MutInd.t * ml_ind
| Stype of Names.GlobRef.t * Names.Id.t list * ml_type option
| Sval of Names.GlobRef.t * ml_type
type ml_specif =
| Spec of ml_spec
| Smodule of ml_module_type
| Smodtype of ml_module_type
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 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
type ml_structure_elem =
| SEdecl of ml_decl
| SEmodule of ml_module
| SEmodtype of ml_module_type
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
and ml_module = {
ml_mod_expr : ml_module_expr;
ml_mod_type : ml_module_type;
}
type ml_structure = (Names.ModPath.t * ml_module_structure) list
type ml_signature = (Names.ModPath.t * ml_module_sig) list
type unsafe_needs = {
mldummy : bool;
tdummy : bool;
tunknown : bool;
magic : bool;
}
type language_descr = {
keywords : Names.Id.Set.t;
file_suffix : string;
file_naming : Names.ModPath.t -> string;
preamble : Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t;
pp_struct : ml_structure -> Pp.t;
sig_suffix : string option;
sig_preamble : Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t;
pp_sig : ml_signature -> Pp.t;
pp_decl : ml_decl -> Pp.t;
}