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