diff options
| author | letouzey | 2010-12-21 11:31:57 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-21 11:31:57 +0000 |
| commit | e3696e15775c44990018d1d4aea01c9bf662cd73 (patch) | |
| tree | 6f14fb168ffe95ef0dd25984a99e0678f53bd89e /plugins/extraction/miniml.mli | |
| parent | b1ae368ec3228f7340076ba0d3bc465f79ed44fa (diff) | |
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 31 |
1 files changed, 23 insertions, 8 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index ea18cbee65..85cd4a42bf 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -51,7 +51,7 @@ type ml_schema = int * ml_type (*s ML inductive types. *) -type inductive_info = +type inductive_kind = | Singleton | Coinductive | Standard @@ -83,7 +83,7 @@ type equiv = | RenEquiv of string type ml_ind = { - ind_info : inductive_info; + ind_kind : inductive_kind; ind_nparams : int; ind_packets : ml_ind_packet array; ind_equiv : equiv @@ -96,12 +96,27 @@ type ml_ident = | Id of identifier | Tmp of identifier -(* list of branches to merge in a common pattern *) +(** 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" +*) + +type constructor_info = { + c_kind : inductive_kind; + c_typs : ml_type list; +} -type case_info = +type branch_same = | BranchNone - | BranchFun of int list - | BranchCst of int list + | BranchFun of Intset.t + | BranchCst of Intset.t + +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 @@ -111,8 +126,8 @@ and ml_ast = | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference - | MLcons of inductive_info * global_reference * ml_ast list - | MLcase of (inductive_info*case_info) * ml_ast * ml_branch array + | MLcons of constructor_info * global_reference * ml_ast list + | MLcase of match_info * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy |