Work on pattern inequalities for pattern matching branches.

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

3 files changed, 155 insertions, 9 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index bf09bcb185..955ee8ac25 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -150,14 +150,6 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
-
-let filter_map f l = 
-  let rec aux acc = function
-      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
-		     | None -> aux acc tl)
-    | [] -> List.rev acc
-  in aux [] l
-
 let list_of_local_binders l = 
   let rec aux acc = function
       Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 7b96758ad7..b196bf913a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -177,6 +177,12 @@ open Tactics
 open Tacticals
 
 let id x = x
+let filter_map f l = 
+  let rec aux acc = function
+      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+		     | None -> aux acc tl)
+    | [] -> List.rev acc
+  in aux [] l
 
 let build_dependent_sum l =
   let rec aux names conttac conttype = function
@@ -279,13 +285,146 @@ let destruct_ex ext ex =
 
 open Rawterm
 
-
+let rec concatMap f l = 
+  match l with
+      hd :: tl -> f hd @ concatMap f tl      
+    | [] -> []
+	
 let list_mapi f = 
   let rec aux i = function 
       hd :: tl -> f i hd :: aux (succ i) tl 
     | [] -> []
   in aux 0
 
+(*
+let make_discr (loc, po, tml, eqns) =
+  let mkHole = RHole (dummy_loc, InternalHole) in
+  
+  let rec vars_of_pat = function
+      RPatVar (loc, n) -> (match n with Anonymous -> [] | Name n -> [n])
+    | RPatCstr (loc, csrt, pats, _) -> 
+	concatMap vars_of_pat pats
+  in
+  let rec constr_of_pat l = function 
+      RPatVar (loc, n) -> 
+	(match n with 
+	     Anonymous -> 
+	       let n = next_name_away_from "x" l in
+		 RVar n, (n :: l)
+	   | Name n -> RVar n, l)
+    | RPatCstr (loc, csrt, pats, _) -> 
+	let (args, vars) =
+	  List.fold_left
+	    (fun (args, vars) x ->
+	       let c, vars = constr_of_pat vars x in
+		 c :: args, vars)
+	    ([], l) pats
+	in		 
+	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
+  in
+  let rec constr_of_pat l = function 
+      RPatVar (loc, n) -> 
+	(match n with 
+	     Anonymous -> 
+	       let n = next_name_away_from "x" l in
+		 RVar n, (n :: l)
+	   | Name n -> RVar n, l)
+    | RPatCstr (loc, csrt, pats, _) -> 
+	let (args, vars) =
+	  List.fold_left
+	    (fun (args, vars) x ->
+	       let c, vars = constr_of_pat vars x in
+		 c :: args, vars)
+	    ([], l) pats
+	in		 
+	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
+  in
+  let constrs_of_pats v l =
+    List.fold_left 
+      (fun (v, acc) x -> 
+	 let x', v' = constr_of_pat v x in
+	   (l', v' :: acc))
+      (v, []) l
+  in
+  let rec pat_of_pat l = function
+      RPatVar (loc, n) -> 
+	let n', l = match n with
+	    Anonymous -> 
+	      let n = next_name_away_from "x" l in
+		n, n :: l
+	  | Name n -> n, n :: l 
+	in
+	  RPatVar (loc, Name n'), l
+    | RPatCstr (loc, cstr, pats, (loc, alias)) ->
+	let args, vars, s = 
+	  List.fold_left (fun (args, vars) x -> 
+			    let pat', vars = pat_of_pat vars pat in
+			      pat' :: args, vars)
+	    ([], alias :: l) pats
+	in RPatCstr (loc, cstr, args, (loc, alias)), vars
+  in
+  let pats_of_pats l =
+    List.fold_left 
+      (fun (v, acc) x -> 
+	 let x', v' = pat_of_pat v x in
+	   (v', x' :: acc))
+      ([], []) l
+  in
+  let eq_of_pat p used c = 
+    let constr, vars' = constr_of_pat used p in
+    let eq = RApp (dummy_loc, RRef (dummy_loc, Lazy.force eqind_ref), [mkHole; constr; c]) in
+      vars', eq
+  in
+  let eqs_of_pats ps used cstrs =
+    List.fold_left2 
+      (fun (vars, eqs) pat c ->
+	 let (vars', eq) = eq_of_pat pat c in
+	   match eqs with 
+	       None -> Some eq 
+	     | Some eqs ->
+		 Some (RApp (dummy_loc, RRef (dummy_loc, Lazy.force and_ref), [eq, eqs])))
+      (used, None) ps cstrs
+  in
+  let quantify c l =
+    List.fold_left
+      (fun acc name -> RProd (dummy_loc, name, mkHole, acc))
+      c l
+  in
+  let quantpats = 
+    List.fold_left
+      (fun (acc, pats) ((loc, idl, cpl, c) as x) ->
+	 let vars, cpl = pats_of_pats cpl in
+	 let l', constrs = constrs_of_pats vars cpl in	   
+	 let discrs = 
+	   List.map (fun (_, _, cpl', _) -> 
+		       let qvars, eqs = eqs_of_pats cpl' l' constrs in
+		       let neg = RApp (dummy_loc, RRef (dummy_loc, Lazy.force not_ref), [out_some eqs]) in
+		       let pat_ineq = quantify qvars neg in
+			 
+		    )
+	     pats in
+	   
+			 
+
+
+	   
+	   
+
+	   (x, pat_ineq))
+  in
+    List.fold_left 
+      (fun acc ((loc, idl, cpl, c0) pat) -> 
+    
+		
+		let c' = 
+		  List.fold_left 
+		    (fun acc (n, t) ->
+		       RLambda (dummy_loc, n, mkHole, acc))
+		    c eqs_types
+		in (loc, idl, cpl, c'))
+      eqns
+  i
+*)
 let rewrite_cases_aux (loc, po, tml, eqns) =
   let tml = list_mapi (fun i (c, (n, opt)) -> c, 
 		       ((match n with
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index ba5bdf2327..c14edad556 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,6 +1,15 @@
 
 Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+  
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
+  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  (S q' & r)
+  else (O & a).
+
+Obligations.
 
 Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) =>
 @existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a
@@ -8,6 +17,12 @@ Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a
 
 Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
   (a & a).
+
+Obligation 1.
+intros ; simpl ; auto.
+Qed.
+
+Solve Obligations using auto.
 reflexivity.
 Defined.