From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 24 Dec 2010 11:53:29 +0100
Subject: Imported Upstream version 8.3pl1

---
 plugins/extraction/miniml.mli | 33 ++++++++++++++++++++++++---------
 1 file changed, 24 insertions(+), 9 deletions(-)

(limited to 'plugins/extraction/miniml.mli')

diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 7ff11b90..20092815 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
@@ -53,7 +53,7 @@ type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type inductive_info =
+type inductive_kind =
   | Singleton
   | Coinductive
   | Standard
@@ -85,7 +85,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
@@ -98,12 +98,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
 
@@ -113,8 +128,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
-- 
cgit v1.2.3