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, 9 insertions, 6 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b780b64bb3..549830fe7c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -476,6 +476,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ind_equiv = equiv }
     in
     add_ind kn mib i;
+    add_inductive_kind kn i.ind_kind;
     i
 
 (*s [extract_type_cons] extracts the type of an inductive
@@ -572,6 +573,8 @@ let rec extract_term env mle mlt c args =
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
 	let env' = push_rel (Name id, Some c1, t1) env in
+	(* We directly push the args inside the [LetIn].
+           TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
 	(try
 	  check_default env t1;
@@ -735,8 +738,8 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 	| Tglob (_,l) -> List.map type_simpl l
 	| _ -> assert false
       in
-      let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
-      put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
+      let typ = Tglob(IndRef ip, typeargs) in
+      put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -800,22 +803,22 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
-	(r, List.rev ids, e')
+	(List.rev ids, Pusual r, e')
       in
       if mi.ind_kind = Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
 	  assert (br_size = 1);
-	  let (_,ids,e') = extract_branch 0 in
+	  let (ids,_,e') = extract_branch 0 in
 	  assert (List.length ids = 1);
 	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
 	let typs = List.map type_simpl (Array.to_list metas) in
-	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
-	in MLcase (info, a, Array.init br_size extract_branch)
+	let typ = Tglob (IndRef ip,typs) in
+	MLcase (typ, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)