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
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
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;
}