Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way

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

5 files changed, 34 insertions, 48 deletions

diff --git a/.gitignore b/.gitignore
index f0dd91db9..98479902a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -106,7 +106,6 @@ ide/config_parser.mli
 
 lib/pp.ml
 lib/compat.ml
-lib/refutpat.ml
 parsing/g_xml.ml
 parsing/g_prim.ml
 parsing/q_util.ml
@@ -141,7 +140,6 @@ plugins/funind/g_indfun.ml
 plugins/omega/g_omega.ml
 plugins/quote/g_quote.ml
 plugins/groebner/groebner.ml
-plugins/groebner/ideal.ml
 plugins/micromega/g_micromega.ml
 plugins/subtac/g_subtac.ml
 plugins/fourier/g_fourier.ml
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
deleted file mode 100644
index ef2801941..000000000
--- a/lib/refutpat.ml4
+++ /dev/null
@@ -1,31 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pcaml
-
-(** * Non-irrefutable patterns
-
-    This small camlp4 extension creates a "let*" variant of the "let"
-    syntax that allow the use of a non-exhaustive pattern. The typical
-    usage is:
-
-      let* x::l = foo in ...
-
-    when foo is already known to be non-empty. This way, no warnings by ocamlc.
-    A Failure is raised if the pattern doesn't match the expression.
-*)
-
-
-EXTEND
- expr:
-   [[ "let"; "*"; p = patt; "="; e1 = expr; "in"; e2 = expr ->
-       <:expr< match $e1$ with
-	        [ $p$ -> $e2$
-                | _ -> failwith "Refutable pattern failed"
-                ] >> ]];
-END
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 6f148ba73..acb37d246 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -276,7 +276,6 @@ let extra_rules () = begin
 
   flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma");
   flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo");
-  flag_and_dep ["p4mod"; "use_refutpat"] (P "lib/refutpat.cmo");
 
 (** Special case of toplevel/mltop.ml4:
     - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx
diff --git a/plugins/_tags b/plugins/_tags
index 2d1d5a760..d29dde4ee 100644
--- a/plugins/_tags
+++ b/plugins/_tags
@@ -18,7 +18,6 @@
 "extraction/g_extraction.ml4": use_grammar
 "ring/g_ring.ml4": use_grammar
 "fourier/g_fourier.ml4": use_grammar
-"groebner/ideal.ml4": use_refutpat
 "groebner/groebner.ml4": use_grammar
 "decl_mode/g_decl_mode.ml4": use_grammar
 
diff --git a/plugins/groebner/ideal.ml4 b/plugins/groebner/ideal.ml
index eae849921..b41d6d8e3 100644
--- a/plugins/groebner/ideal.ml4
+++ b/plugins/groebner/ideal.ml
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "lib/refutpat.cmo" i*)
-(* NB: The above camlp4 extension adds a let* syntax for refutable patterns *)
-
 (*
    Nullstellensatz par calcul de base de Grobner
 
@@ -24,6 +21,30 @@
 
 open Utile
 
+(* NB: Loic is using a coding-style "let x::q = ... in ..." that
+   produces lots of warnings about non-exhaustive pattern matchs.
+   Even worse, it is not clear whether a [Match_failure] could
+   happen (and be catched by a "with _ ->") or not. Loic told me
+   it shouldn't happen.
+
+   In a first time, I used a camlp4 extension (search history
+   for lib/refutpat.ml4) for introducing an ad-hoc syntax
+   "let* x::q = ...". This is now removed (too complex during
+   porting to camlp4).
+
+   Now, we simply use the following function that turns x::q
+   into (x,q) and hence an irrefutable pattern. Yes, this adds
+   a (small) cost since the intermediate pair is allocated
+   (in opt, the cost might even be 0 due to inlining).
+   If somebody want someday to remove this extra cost,
+   (x::q) could also be turned brutally into (x,q) by Obj.magic
+   (beware: be sure no floats are around in this case).
+*)
+
+let of_cons = function
+  | [] -> assert false
+  | x::q -> x,q
+
 exception NotInIdeal
 
 module type S = sig
@@ -741,7 +762,7 @@ let normal_form d p g mg onlyhead =
     | (a,v)::p' ->
 	(try
 	   let q = find_reductor d v g mg in
-	   let* (b,u)::q' = q.pol in
+	   let (b,u),q' = of_cons q.pol in
 	   let c = P.pgcdP a b in
 	   let a' = P.divP b c in
 	   let b' = P.oppP (P.divP a c) in
@@ -770,7 +791,7 @@ let reduce_rem d r lt lq =
   r
 
 let tail_normal_form d p g mg =
-  let* (a,v)::p' = p in
+  let (a,v),p' = of_cons p in
   let (c,r)= (normal_form d p' g mg false) in
   plusP d [(P.multP a c,v)] r
 
@@ -801,8 +822,8 @@ let head_normal_form d p lt mt =
     then ((* info "=";*) [])
     else (
       while !h <> [] && (!g).pol <> [] do
-	let* (a,v)::p' = !h in
-	let* (b,u)::q' = (!g).pol in
+	let (a,v),p' = of_cons !h in
+	let (b,u),q' = of_cons (!g).pol in
 	let c = P.pgcdP a b in
 	let a' = P.divP b c in
 	let b' = P.oppP (P.divP a c) in
@@ -830,7 +851,7 @@ let head_reduce d lq lt mt =
   let ls = ref lq in
   let lq = ref [] in
   while !ls <> [] do
-    let* p::ls1 = !ls in
+    let p,ls1 = of_cons !ls in
     ls := ls1;
     if !homogeneous && p.pol<>[] && deg_hom p.pol > deg_hom !pol_courant
     then info "h"
@@ -959,8 +980,8 @@ let head_normal_form3 d p lt mt =
     then ((* info "=";*) [])
     else (
       while !h <> [] && (!g).pol <> [] do
-	let* (a,v)::p' = !h in
-        let* (b,u)::q' = (!g).pol in
+	let (a,v),p' = of_cons !h in
+        let (b,u),q' = of_cons (!g).pol in
 	let c = P.pgcdP a b in
 	let a' = P.divP b c in
 	let b' = P.oppP (P.divP a c) in
@@ -987,14 +1008,14 @@ let janet3 d lf p0 =
   let r = ref p0 in
   let lf = List.map (pol_to_pol3 d) lf in
 
-  let* f::lf1 = lf in
+  let f,lf1 = of_cons lf in
   let lt = ref [f] in
   let mt = ref (hashtbl_multiplicative d !lt) in
   let lq = ref lf1 in
   r := reduce_rem  d !r !lt !lq ; (* janet_normal_form  d !r !lt !mt ;*)
   info ("reste: "^(stringPcut !r)^"\n");
   while !lq <> [] && !r <> [] do
-    let* p::lq1 = !lq in
+    let p,lq1 = of_cons !lq in
     lq := lq1;
 (*
     if p.pol = p.anc
@@ -1272,7 +1293,7 @@ let pbuchf d pq p lp0=
       match lpc with
         [] -> test_dans_ideal d p lp lp0
       | _ ->
-	  let* a::lpc2 = choix_spol d !pol_courant lpc in
+	  let a,lpc2 = of_cons (choix_spol d !pol_courant lpc) in
 	  if !homogeneous && a<>[] && deg_hom a > deg_hom !pol_courant
 	  then (info "h";pbuchf lp lpc2)
 	  else