diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 39 |
1 files changed, 18 insertions, 21 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index edff48c85..0bf1ff952 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -97,28 +97,17 @@ type ml_ident = | Tmp of identifier (** We now store some typing information on constructors - and cases to avoid type-unsafe optimisations. - For cases, we also store the set of branches to merge - in a common pattern, either "_ -> c" or "x -> f x" + 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. *) -type constructor_info = { - c_kind : inductive_kind; - c_typs : ml_type list; -} - -type branch_same = - | BranchNone - | BranchFun of Intset.t - | BranchCst of Intset.t +(** 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 match_info = { - m_kind : inductive_kind; - m_typs : ml_type list; - m_same : branch_same -} - -type ml_branch = global_reference * ml_ident list * ml_ast +type ml_branch = ml_ident list * ml_pattern * ml_ast and ml_ast = | MLrel of int @@ -126,14 +115,22 @@ and ml_ast = | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference - | MLcons of constructor_info * global_reference * ml_ast list - | MLcase of match_info * ml_ast * ml_branch array + | MLcons of ml_type * global_reference * ml_ast list + | MLtuple of ml_ast list + | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy | MLaxiom | MLmagic of ml_ast +and ml_pattern = + | Pcons of global_reference * 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 global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + (*s ML declarations. *) type ml_decl = |