Use camlp4 to accept some specific non-exhaustive patterns in groebner

 The camlp4 extension "refutpat" provides a syntax let* for pattern
 that are non-exhaustive on purpose (e.g. let* x::l = foo in ...).
 A Failure is raised if the pattern doesn't match the expression.

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

5 files changed, 53 insertions, 13 deletions

diff --git a/_tags b/_tags
index f73b9ddd2..97957e81e 100644
--- a/_tags
+++ b/_tags
@@ -23,6 +23,7 @@
 
 "parsing/lexer.ml4": use_macro
 "lib/compat.ml4": use_macro
+"lib/refutpat.ml4": use_extend, use_MLast
 "parsing/g_xml.ml4": use_extend
 "parsing/q_constr.ml4": use_extend, use_MLast
 "parsing/argextend.ml4": use_extend, use_MLast
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
new file mode 100644
index 000000000..f2575def4
--- /dev/null
+++ b/lib/refutpat.ml4
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
+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 f8d5d0681..104231f97 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -111,6 +111,7 @@ let libcoqrun = "kernel/byterun/libcoqrun.a"
 
 let grammar = "parsing/grammar.cma"
 let qconstr = "parsing/q_constr.cmo"
+let refutpat = "lib/refutpat.cmo"
 
 let initialcoq = "states/initial.coq"
 let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"]
@@ -253,6 +254,7 @@ let extra_rules () = begin
 
   flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P grammar);
   flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
+  flag_and_dep ["is_ml4"; "p4mod"; "use_refutpat"] (P refutpat);
 
 (** 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 968b25bd2..6d28450fd 100644
--- a/plugins/_tags
+++ b/plugins/_tags
@@ -20,6 +20,7 @@
 "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
 
 
diff --git a/plugins/groebner/ideal.ml b/plugins/groebner/ideal.ml4
index 4570f69d8..73db36d46 100644
--- a/plugins/groebner/ideal.ml
+++ b/plugins/groebner/ideal.ml4
@@ -6,6 +6,9 @@
 (*         *       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
 
@@ -738,7 +741,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' = 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
@@ -767,7 +770,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' = p in
   let (c,r)= (normal_form d p' g mg false) in
   plusP d [(P.multP a c,v)] r
 
@@ -798,8 +801,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' = !h in
+	let* (b,u)::q' = (!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
@@ -827,7 +830,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 = !ls in
     ls := ls1;
     if !homogeneous && p.pol<>[] && deg_hom p.pol > deg_hom !pol_courant
     then info "h"
@@ -858,7 +861,7 @@ let hashtbl_multiplicative d lf =
   hashtbl_reductor := Hashtbl.create 51;
   List.iter
     (fun g ->
-      let (_,u)::_ = g.pol in
+      let (_,u) = List.hd g.pol in
       Hashpol.add mg g.pol (monom_multiplicative d u lf))
     lf;
   (*info ("temps de hashtbl_multiplicative: "
@@ -956,8 +959,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' = !h in
+        let* (b,u)::q' = (!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
@@ -984,14 +987,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 = 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 = !lq in
     lq := lq1;
 (*
     if p.pol = p.anc 
@@ -1247,12 +1250,12 @@ let divide_rem_with_critical_pair = ref false
 let choix_spol d p l =
   if !divide_rem_with_critical_pair
   then (
-    let (_,m)::_ = p in
+    let (_,m) = List.hd p in
     try (
       let q =
 	List.find
 	  (fun q ->
-	    let (_,m')::_ = q in
+	    let (_,m') = List.hd q in
 	    div_mon_test d m m')
 	  l in
       q::(list_diff l q))
@@ -1269,7 +1272,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 = choix_spol d !pol_courant lpc in
 	  if !homogeneous && a<>[] && deg_hom a > deg_hom !pol_courant
 	  then (info "h";pbuchf lp lpc2)
 	  else