Fix evars bug in mutual fixpoints with implicit types and bug in inequalities generation for multiple patterns.

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

2 files changed, 55 insertions, 41 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 4b33f9d86f..27efe04702 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1714,14 +1714,17 @@ let rec is_included x y =
 	if i = i' then List.for_all2 is_included args args'
 	else false
 
-(* liftsign is the current pattern's signature length *)
+(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its
+   full signature. However prevpatterns are in the original one signature per pattern form.
+ *)
 let build_ineqs prevpatterns pats liftsign =
   let _tomatchs = List.length pats in
   let diffs = 
     List.fold_left 
       (fun c eqnpats -> 
-	 let acc = List.fold_left2
-	   (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) 
+	  let acc = List.fold_left2
+	    (* ppat is the pattern we are discriminating against, curpat is the current one. *)
+	    (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) 
 	      (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
 	      match acc with
 		  None -> None
@@ -1731,21 +1734,19 @@ let build_ineqs prevpatterns pats liftsign =
 		      let lens = List.length ppat_sign in
 		      (* Accumulated length of previous pattern's signatures *)
 		      let len' = lens + len in
-			trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by "
-				  ++ int len');
+(* 			trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by " *)
+(* 				  ++ int len'); *)
+(* 			trace (str "treating " ++ my_print_constr (push_rel_context ppat_sign Environ.empty_env) ppat_c); *)
 		      let acc = 
 			((* Jump over previous prevpat signs *)
 			  lift_rel_context len ppat_sign @ sign, 
 			  len',
 			  succ n, (* nth pattern *)
 			  mkApp (Lazy.force eq_ind,
-				[| lift (lens + liftsign) ppat_ty ;
-				   liftn liftsign (succ lens) ppat_c ;
+				[| lift (len + liftsign) ppat_ty ;
+				   liftn (len + liftsign) (succ lens) ppat_c ;
 				   lift len' curpat_c |]) :: 
-			    List.map 
-			    (fun t -> 
-			      liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *)
-			      (lift lens t (* Jump over this prevpat signature *))) c)
+			    List.map (lift lens (* Jump over this prevpat signature *)) c)
 		      in Some acc
 		    else None)
 	   (Some ([], 0, 0, [])) eqnpats pats
@@ -1789,7 +1790,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 		  (idents, pat' :: newpatterns, cpat :: pats))
 	      ([], [], []) eqn.patterns sign
 	 in
-	 let newpatterns = List.rev newpatterns and pats = List.rev pats in
+	 let newpatterns = List.rev newpatterns and opats = List.rev pats in
 	 let rhs_rels, pats, signlen = 
 	   List.fold_left 
 	     (fun (renv, pats, n) (sign,c, (s, args), p) -> 
@@ -1801,18 +1802,17 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 		 (* lift to get outside of previous pattern's signatures. *)
 		 (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
 		 len + n))
-	     ([], [], 0) pats in
+	     ([], [], 0) opats in
 	 let pats, _ = List.fold_left 
 	   (* lift to get outside of past patterns to get terms in the combined environment. *)
 	   (fun (pats, n) (sign, c, (s, args), p) ->
 	     let len = List.length sign in
 	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
-	   ([], 0) pats 
+	   ([], 0) pats
 	 in
+	 let ineqs = build_ineqs prevpatterns pats signlen in
 	 let rhs_rels' = rels_of_patsign rhs_rels in
 	 let _signenv = push_rel_context rhs_rels' env in
-(* 	   trace (str "Env with signature is: " ++ my_print_env _signenv);  *)
-	 let ineqs = build_ineqs prevpatterns pats signlen in
 	 let eqs_rels = 
 	   let eqs = (*List.concat (List.rev eqs)*) context_of_arsign eqs in
 	   let args, nargs = 
@@ -1831,11 +1831,12 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 (* 	       trace (str " subtituted equalities " ++ my_print_rel_context _signenv eqs''); *)
 	     eqs''
 	 in
+	   trace (str "Env with signature is: " ++ my_print_env _signenv);
 	 let rhs_rels', lift_ineqs = 
 	   match ineqs with
 	       None -> eqs_rels @ rhs_rels', 0
 	     | Some ineqs -> 
-		 (* 		 let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in *)
+		 let _ = trace (str"Generated inequalities: " ++ my_print_constr _signenv ineqs) in
 		 lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels'), 1
 	 in
 	 let rhs_env = push_rels rhs_rels' env in
@@ -1873,7 +1874,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 	   let rhs = { eqn.rhs with it = branch } in
 	     (branch_decl :: branches,
 	      { eqn with patterns = newpatterns; rhs = rhs } :: eqns,
-	      pats :: prevpatterns))
+	      opats :: prevpatterns))
       ([], [], []) eqns
   in x, y
       
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index dded538b59..b9c25f2074 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -126,7 +126,7 @@ let collect_non_rec env =
       let i = 
         list_try_find_i
           (fun i f ->
-             if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
+             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
              then i else failwith "try_find_i")
           0 lnamerec 
       in
@@ -324,22 +324,18 @@ let nf_evar_context isevars ctx =
   List.map (fun (n, b, t) -> 
     (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
     
-let build_mutrec l boxed = 
+let build_mutrec lnameargsardef boxed = 
   let sigma = Evd.empty and env = Global.env () in 
   let nc = named_context env in
   let nc_len = named_context_length nc in
-  let lnameargsardef =
-    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*)
-    l
-  in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
   in
+  let isevars = ref (Evd.create_evar_defs sigma) in	  
     (* Build the recursive context and notations for the recursive types *)
   let (rec_sign,rec_env,rec_impls,arityl) = 
     List.fold_left 
       (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
-	 let isevars = ref (Evd.create_evar_defs sigma) in	  
 	 let arityc = Command.generalize_constr_expr arityc bl in
 	 let arity = interp_type isevars env arityc in
 	 let impl = 
@@ -347,7 +343,7 @@ let build_mutrec l boxed =
 	   then Impargs.compute_implicits env arity
 	   else [] in
 	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-	   ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
+	   ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (None, arity)::arl))
       ([],env,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
@@ -355,7 +351,6 @@ let build_mutrec l boxed =
       lnameargsardef [] in
 
   let recdef =
-
     (* Declare local notations *)
     let fs = States.freeze() in
     let def = 
@@ -363,17 +358,17 @@ let build_mutrec l boxed =
 	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
 	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
 	List.map2
-	  (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
+	  (fun ((_,_,bl,_,def),_) (info, arity) ->
 	     match info with
 		 None ->
 		   let def = abstract_constr_expr def bl in
-		     isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
+		     info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
 		       def arity
 	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
 		   let rec_env = push_rel_context fun_bl rec_env in
 		   let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls)
 				def intern_arity
-		   in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
+		   in info, it_mkLambda_or_LetIn cstr fun_bl)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -381,20 +376,36 @@ let build_mutrec l boxed =
   in
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env lrecnames recdef arityl nv in
+  if lnonrec <> [] then 
+    errorlabstrm "Subtac_command.build_mutrec"
+      (str "Non-recursive definitions not allowed in mutual fixpoint blocks");
   let recdefs = Array.length defrec in
-    (* Solve remaining evars *)
+    trace (str "built recursive definitions");
+    (* Normalize all types and defs with respect to *all* evars *)
+    Array.iteri 
+      (fun i (info, def) ->
+	let def = evar_nf isevars def in
+	let y, typ = arrec.(i) in
+	let typ = evar_nf isevars typ in
+	  arrec.(i) <- (y, typ);
+	  defrec.(i) <- (info, def))
+      defrec;
+    trace (str "normalized w.r.t. evars");
+  (* Normalize rec_sign which was built earlier *)
+  let rec_sign = nf_evar_context !isevars rec_sign in
+    trace (str "normalized context");
+  (* Get the interesting evars, those that were not instanciated *)
+  let isevars = Evd.undefined_evars !isevars in
+    trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
+  let evm = Evd.evars_of isevars in
+  trace (str "got the evm, recdefs is " ++ int recdefs);
+  (* Solve remaining evars *)
   let rec collect_evars i acc = 
     if i < recdefs then
-      let (isevars, info, def) = defrec.(i) in
-	(*       let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *)
-      let def = evar_nf isevars def in
-      let x, y, typ = arrec.(i) in
-      let typ = evar_nf isevars typ in
-      arrec.(i) <- (x, y, typ);
-      let rec_sign = nf_evar_context !isevars rec_sign in
-      let isevars = Evd.undefined_evars !isevars in
-	(*       let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *)
-      let evm = Evd.evars_of isevars in
+      let (info, def) = defrec.(i) in
+      let y, typ = arrec.(i) in
+	trace (str "got the def" ++ int i);
+      let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
       let id = namerec.(i) in
 	(* Generalize by the recursive prototypes  *)
       let def = 
@@ -402,12 +413,14 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
+      let evm = Subtac_utils.evars_of_term evm Evd.empty def in
       let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
   let defs = collect_evars 0 [] in
     Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec
+    
       
 let out_n = function
     Some n -> n