Improvements in subtac:

- Use return clause inference in addition to the
automatic generation of equalities for pattern-matching.
- Disallow generation of coercions between type constructors, 
which are not provable anyway.
- Improve inference for local (co-)fixpoints using the typing
constraint.


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

3 files changed, 90 insertions, 69 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 187d5c4da..8312c66da 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1977,6 +1977,47 @@ let nf_evars_env evar_defs (env : env) : env =
     Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
      ~init:env' env
       
+(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
+
+let prepare_predicate_from_arsign_tycon loc env tomatchs arsign c =
+  let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+  let subst, len = 
+    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+      let signlen = List.length sign in
+	match kind_of_term tm with
+	  | Rel n when dependent tm c 
+		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
+	      ((n, len) :: subst, len - signlen)
+	  | Rel _ when not (dependent tm c)
+		&& signlen > 1 (* The term is of a dependent type but does not appear in 
+				  the tycon, maybe some variable in its type does. *) ->
+	      (match tmtype with
+		  NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
+		| IsInd (_, IndType(indf,realargs)) ->
+		    List.fold_left
+		      (fun (subst, len) arg -> 
+			match kind_of_term arg with
+			  | Rel n when dependent arg c ->
+			      ((n, len) :: subst, pred len)
+			  | _ -> (subst, pred len))
+		      (subst, len) realargs)
+	  | _ -> (subst, len - signlen))
+      ([], nar) tomatchs arsign
+  in
+  let rec predicate lift c =
+    match kind_of_term c with
+      | Rel n when n > lift -> 
+	  (try 
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = List.assoc (n - lift) subst in
+		mkRel (idx + lift)
+	    with Not_found -> 
+	      (* A variable that is not matched, lift over the arsign. *)
+	      mkRel (n + nar))
+      | _ ->
+	  map_constr_with_binders succ predicate lift c 
+  in predicate 0 c
+
 let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
 
   let typing_fun tycon env = typing_fun tycon env isevars in
@@ -2002,15 +2043,14 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	  build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign
 
       in
-      let tycon = 
+      let tycon, arity = 
 	match valcon_of_tycon tycon with
-	| None -> mkExistential env isevars 
-	| Some t -> t
+	| None -> let ev = mkExistential env isevars in ev, ev
+	| Some t -> 
+	    t, prepare_predicate_from_arsign_tycon loc env tomatchs sign (lift tomatchs_len t)
       in
       let arity = 
-	it_mkProd_wo_LetIn
-	  (lift (signlen + neqs + tomatchs_len) tycon)
-	  (context_of_arsign eqs)
+	it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
       in
       let lets, matx = 
 	(* Type the rhs under the assumption of equations *)
@@ -2022,17 +2062,11 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
       let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
       let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
       let args = List.rev_map (lift len) args in
-      let sign = List.map (lift_rel_context len) sign in	
       let pred = liftn len (succ signlen) arity in
-      (* We build the elimination predicate if any and check its consistency *)
-      (* with the type of arguments to match *)
-      let _signenv = List.fold_right push_rels sign env in
+      let pred = build_initial_predicate true allnames pred in
 
-      let pred =
-	(* prepare_predicate_from_tycon loc typing_fun isevars env tomatchs eqs allnames signlen sign tycon in *)
-	build_initial_predicate true allnames pred in
-	(* We push the initial terms to match and push their alias to rhs' envs *)
-	(* names of aliases will be recovered from patterns (hence Anonymous here) *)
+      (* We push the initial terms to match and push their alias to rhs' envs *)
+      (* names of aliases will be recovered from patterns (hence Anonymous here) *)
       let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
 	
       let pb =
@@ -2054,7 +2088,6 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	  { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
 	    uj_type = nf_isevar !isevars tycon; }
 	in j
-(* 	  inh_conv_coerce_to_tycon loc env isevars j tycon0 *)
     else
       (* We build the elimination predicate if any and check its consistency *)
       (* with the type of arguments to match *)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4a1869053..11a7f1941 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -149,17 +150,17 @@ module Coercion = struct
 		  try isevars := the_conv_x_leq env eqT eqT' !isevars
 		  with Reduction.NotConvertible -> raise NoSubtacCoercion
 		in
+		(* Disallow equalities on arities *)
+		if Reduction.is_arity env eqT then raise NoSubtacCoercion;
 		let restargs = lift_args 1 
 		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
 		in 
 		let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
 		let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
-(* 		let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *)
 		let evar = make_existential loc env isevars eq in
 		let eq_app x = mkApp (Lazy.force eq_rect,
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
-(* 		  trace (str"Inserting coercion at application"); *)
 		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	  else Some co
 	in aux [] typ typ' 0 (fun x -> x)
@@ -445,13 +446,6 @@ module Coercion = struct
 
 
   let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
-(*     (try *)
-(*        debug 1 (str "inh_conv_coerce_to_fail called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
-(* 	      Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
     try (the_conv_x_leq env t c1 evd, v)
     with Reduction.NotConvertible ->
     try inh_coerce_to_fail env evd rigidonly v t c1
@@ -481,18 +475,14 @@ module Coercion = struct
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
-(*     (try *)
-(*        trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *)
-(* 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *)
-(* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
-(* 	      Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
+    let evd = nf_evar_defs evd in
     match n with
 	None ->
 	  let (evd', val') = 
 	    try 
-	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+	      inh_conv_coerce_to_fail loc env evd rigidonly
+		(Some (nf_isevar evd cj.uj_val))
+		(nf_isevar evd cj.uj_type) (nf_isevar evd t)
 	    with NoCoercion ->
 	      let sigma = evars_of evd in
 		try
@@ -509,13 +499,6 @@ module Coercion = struct
   let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
-(*     (try *)
-(*        trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
-(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
     let nabsinit, nabs =
       match abs with
 	  None -> 0, 0
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 808039de6..16180d169 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -221,43 +222,47 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let names = Array.map (fun id -> Name id) names in
 	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
 	let newenv = push_rec_types (names,ftys,[||]) env in
+	let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
 	let vdefj =
 	  array_map2_i 
 	    (fun i ctxt def ->
-               (* we lift nbfix times the type in tycon, because of
-		* the nbfix variables pushed to newenv *)
-               let (ctxt,ty) =
-		 decompose_prod_n_assum (rel_context_length ctxt)
-                   (lift nbfix ftys.(i)) in
-               let nenv = push_rel_context ctxt newenv in
-               let j = pretype (mk_tycon ty) nenv isevars lvar def in
-		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
-		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+	      let fty = 
+		let ty = ftys.(i) in
+		  if i = fixi then (
+		    Option.iter (fun tycon ->
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars ftys.(i) tycon)
+		      tycon;
+		    nf_isevar !isevars ty)
+		  else ty
+	      in
+              (* we lift nbfix times the type in tycon, because of
+	       * the nbfix variables pushed to newenv *)
+              let (ctxt,ty) =
+		decompose_prod_n_assum (rel_context_length ctxt)
+                  (lift nbfix fty) in
+              let nenv = push_rel_context ctxt newenv in
+              let j = pretype (mk_tycon ty) nenv isevars lvar def in
+		{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env isevars names ftys vdefj;
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
-	      let guard_indexes = Array.mapi 
+	      (* First, let's find the guard indexes. *)
+	      (* If recursive argument was not given by user, we try all args.
+	         An earlier approach was to look only for inductive arguments,
+		 but doing it properly involves delta-reduction, and it finally 
+                 doesn't seem worth the effort (except for huge mutual 
+		 fixpoints ?) *)
+	      let possible_indexes = Array.to_list (Array.mapi 
 		(fun i (n,_) -> match n with 
-		   | Some n -> n 
-		   | None -> 
-		       (* Recursive argument was not given by the user : We
-			  check that there is only one inductive argument *)
-		       let ctx = ctxtv.(i) in 
-		       let isIndApp t = 
-			 isInd (fst (decompose_app (strip_head_cast t))) in
-			 (* This could be more precise (e.g. do some delta) *)
-		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
-		       try (list_unique_index true lb) - 1
-		       with Not_found -> 
-			 Util.user_err_loc
-			   (loc,"pretype",
-			    Pp.str "cannot guess decreasing argument of fix"))
-		vn 
-	      in
-	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
-	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) ftys.(i)
+		   | Some n -> [n]
+		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+		vn)
+	      in 
+	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let indexes = search_guard loc env possible_indexes fixdecls in 
+	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i -> 
 	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);