Extraction: Richer patterns in matchs as proposed by P.N. Tollitte

 The MLcase has notably changed:
  - No more case_info in it, but only a type annotation
  - No more "one branch for one constructor", but rather a sequence
    of patterns. Earlier "full" pattern correspond to pattern Pusual.
    Patterns Pwild and Prel allow to encode optimized matchs without
    hacks as earlier. Other pattern situations aren't used (yet)
    by extraction, but only by P.N Tollitte's code.

 A MLtuple constructor has been introduced. It isn't used by
 the extraction for the moment, but only but P.N. Tollitte's code.

 Many pretty-print functions in ocaml.ml and other have been reorganized

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7

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 =