Fix some nasty bug with the evars-to-dependent sum encoding.

Also enclose traces with try with clauses to avoid detypinging anomalies.


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

8 files changed, 114 insertions, 82 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 437acb1f2..382ae2d5b 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -47,9 +47,9 @@ let subst_evars evs n t =
     | Evar (k, args) ->
 	(try 
 	   let index, hyps = evar_info k in
-	     trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
-		    int (List.length hyps) ++ str " hypotheses");
-
+	     (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+			 int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
+		
 	   let ex = mkRel (index + depth) in
 	     (* Evar arguments are created in inverse order, 
 		and we must not apply to defined ones (i.e. LetIn's)
@@ -140,15 +140,17 @@ let eterm_term evm t tycon =
     let id = id_of_string ("Evar" ^ string_of_int id) in
       tclTHEN acc (Tactics.assert_tac false (Name id) c)
   in
-    trace (str "Term given to eterm" ++ spc () ++
-	   Termops.print_constr_env (Global.env ()) t);
-    trace (str "Term constructed in eterm" ++ spc () ++
-	   Termops.print_constr_env (Global.env ()) t'');
-    ignore(option_map 
-	     (fun typ ->
-		trace (str "Type :" ++ spc () ++
-		       Termops.print_constr_env (Global.env ()) typ))
-	     tycon);
+    (try 
+       trace (str "Term given to eterm" ++ spc () ++
+	      Termops.print_constr_env (Global.env ()) t);
+       trace (str "Term constructed in eterm" ++ spc () ++
+	      Termops.print_constr_env (Global.env ()) t'');
+       ignore(option_map 
+		(fun typ ->
+		   trace (str "Type :" ++ spc () ++
+			  Termops.print_constr_env (Global.env ()) typ))
+		tycon);
+     with _ -> ());
     t'', tycon, evar_names
 
 let mkMetas n = 
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 5b857a688..4cbfe90cf 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -48,8 +48,10 @@ let subtac_one_fixpoint env isevars (f, decl) =
   let ((id, n, bl, typ, body), decl) = 
     Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
   in
-  let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
-		 Ppconstr.pr_constr_expr body)
+  let _ = 
+    try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
+	       Ppconstr.pr_constr_expr body)
+    with _ -> ()
   in ((id, n, bl, typ, body), decl)
     
 	      
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index cdad00372..f2a1a0185 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -53,7 +53,8 @@ module Coercion = struct
       | _ -> None
 	  
   and disc_exist env x =
-    trace (str "Disc_exist: " ++ my_print_constr env x);
+    (try trace (str "Disc_exist: " ++ my_print_constr env x)
+     with _ -> ());
     match kind_of_term x with
       | App (c, l) ->
 	  (match kind_of_term c with
@@ -66,7 +67,8 @@ module Coercion = struct
 
 
   let disc_proj_exist env x =
-    trace (str "disc_proj_exist: " ++ my_print_constr env x);
+    (try trace (str "disc_proj_exist: " ++ my_print_constr env x);
+     with _ -> ());
     match kind_of_term x with
       | App (c, l) ->
 	  (if Term.eq_constr c (Lazy.force sig_).proj1 
@@ -104,23 +106,27 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-      trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
-	     str " and "++ my_print_constr env y ++ 
-	     str " with evars: " ++ spc () ++
-	     my_print_evardefs !isevars);
+      (try trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+		  str " and "++ my_print_constr env y ++ 
+		  str " with evars: " ++ spc () ++
+		  my_print_evardefs !isevars);
+       with _ -> ());
     let rec coerce_unify env x y =
-      trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
-	     str " to "++ my_print_constr env y);
+      (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
+		  str " to "++ my_print_constr env y)
+       with _ -> ());
       try 
 	isevars := the_conv_x_leq env x y !isevars;
-	trace (str "Unified " ++ (my_print_constr env x) ++ 
-	       str " and "++ my_print_constr env y);
+	(try (trace (str "Unified " ++ (my_print_constr env x) ++ 
+		     str " and "++ my_print_constr env y));
+	 with _ -> ());
 	None
       with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
-	trace (str "coerce' from " ++ (my_print_constr env x) ++ 
-		 str " to "++ my_print_constr env y);
+	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ 
+		    str " to "++ my_print_constr env y);
+	 with _ -> ());
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
 	      (match s, s' with
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 552acf137..b09228c06 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,7 +56,7 @@ let interp_gen kind isevars env
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
   let c' = Subtac_utils.rewrite_cases env c' in
-    trace (str "Pretyping " ++ my_print_constr_expr c);
+    (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ());
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
     
@@ -201,10 +201,12 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
 	    | CWfRec r -> 		    
 		let n = out_some n in 
-		let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
-			       Ppconstr.pr_binders bl ++ str " : " ++ 
-			       Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
-			       Ppconstr.pr_constr_expr body)
+		let _ = 
+		  try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+			     Ppconstr.pr_binders bl ++ str " : " ++ 
+			     Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+			     Ppconstr.pr_constr_expr body)
+		  with _ -> ()
 		in
 		let env', binders_rel = interp_context isevars env0 bl in
 		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
@@ -234,10 +236,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		let _ = 
 		  let pr c = my_print_constr env c in
 		  let prr = Printer.pr_rel_context env in
-		    trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
-			     str "Intern bl" ++ prr intern_bl ++ spc () ++
-			     str "Extern bl" ++ prr new_bl ++ spc () ++
-			     str "Intern arity: " ++ pr intern_arity)
+		    try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+			       str "Intern bl" ++ prr intern_bl ++ spc () ++
+			       str "Extern bl" ++ prr new_bl ++ spc () ++
+			       str "Intern arity: " ++ pr intern_arity)
+		    with _ -> ()
 		in
 		let impl = 
 		  if Impargs.is_implicit_args()
@@ -286,8 +289,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
     let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
     let rec declare i fi =
-      trace (str "Declaring: " ++ pr_id fi ++ spc () ++
-	     my_print_constr env0 (recvec.(i)));
+      (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+		  my_print_constr env0 (recvec.(i)));
+       with _ -> ());
       let ce = 
 	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
           const_entry_type = Some arrec.(i);
@@ -332,10 +336,10 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
   let rec collect_evars i acc = 
     if i < recdefs then
       let (isevars, info, def) = defrec.(i) in
-      let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) 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 isevars = Evd.undefined_evars !isevars in
-      let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs 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 _, _, typ = arrec.(i) in
       let id = namerec.(i) in
@@ -358,10 +362,16 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 	trace (str (string_of_id fi) ++ str " is defined");*)
 	let evar_sum =
 	  if evars = [] then None
-	  else 
+	  else (
+	    (try trace (str "Building evars sum for : ");
+	       List.iter
+		 (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t))
+		 evars;
+	     with _ -> ());
 	    let sum = Subtac_utils.build_dependent_sum evars in
-	      trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum));
-	      Some sum
+	      (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum));
+	       with _ -> ());
+	      Some sum)
 	in
 	  collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
     else acc
@@ -371,32 +381,34 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
   (* Solve evars then create the definitions *)
   let real_evars = 
     filter_map (fun (id, kn, sum) ->
-		  match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None)
+		  match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
       defs
   in
     Subtac_utils.and_tac real_evars
       (fun f _ gr ->
-	 let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+	 let _ = trace (str "Got a proof of: " ++ pr_global gr ++
+			str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in
 	 let constant = match gr with Libnames.ConstRef c -> c
 	   | _ -> assert(false)
 	 in
 	   try
 	     (*let value = Environ.constant_value (Global.env ()) constant in*)
 	     let pis = f (mkConst constant) in
-	       trace (str "Accessors: " ++
-		      List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
-			pis (mt()));
-	       trace (str "Applied existentials: " ++
-		      (List.fold_right
-			 (fun (id, kn, sumg, pi) acc ->
-			    let args = Subtac_utils.destruct_ex pi sumg in
-			      my_print_constr env0 (mkApp (kn, Array.of_list args)))
-			 pis (mt ())));
+	       (try (trace (str "Accessors: " ++
+			   List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
+			     pis (mt()));
+		    trace (str "Applied existentials: " ++
+			   (List.fold_right
+			      (fun (id, kn, sumg, pi) acc ->
+				 let args = Subtac_utils.destruct_ex pi sumg in
+				   my_print_constr env0 (mkApp (kn, Array.of_list args)))
+			      pis (mt ()))))
+	       with _ -> ());
 	       let rec aux pis acc = function
 		   (id, kn, sum) :: tl ->
 		     (match sum with 
 			  None -> aux pis (kn :: acc) tl
-			| Some (sumg, _, _) -> 
+			| Some (_, sumg) -> 
 			    let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
 			    let args = Subtac_utils.destruct_ex pi sumg in
 			    let args = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 1d37900f1..d0240f5a5 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -116,25 +116,26 @@ let subtac_process env isevars id l c tycon =
   let evars () = evars_of !isevars in
   let _ = trace (str "Creating env with binders") in
   let env_binders, binders_rel = env_with_binders env isevars l in
-  let _ = trace (str "New env created:" ++ my_print_context env_binders) in
+  let _ = try (trace (str "New env created:" ++ my_print_context env_binders)) with _ -> () in
   let tycon = 
     match tycon with
 	None -> empty_tycon
       | Some t -> 
 	  let t = coqintern !isevars env_binders t in
-	  let _ = trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) in
+	  let _ = try trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) with _ -> () in
 	  let coqt, ttyp = interp env_binders isevars t empty_tycon in
-	  let _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) in
+	  let _ = try trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) with _ -> () in
 	    mk_tycon coqt
   in    
   let c = coqintern !isevars env_binders c in
   let c = Subtac_utils.rewrite_cases env c in
-  let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in
+  let _ = try trace (str "Internalized term: " ++ my_print_rawconstr env c)  with _ -> () in
   let coqc, ctyp = interp env_binders isevars c tycon in
-  let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
+  let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
 		 str "Coq type: " ++ my_print_constr env_binders ctyp)
+  with _ -> () 
   in
-  let _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) in
+  let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ()))  with _ -> () in
     
   let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel 
   and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
@@ -142,10 +143,11 @@ let subtac_process env isevars id l c tycon =
   let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
   let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
 
-  let _ = trace (str "After evar normalization: " ++ spc () ++
+  let _ = try trace (str "After evar normalization: " ++ spc () ++
 		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
 		 ++ str "Coq type: " ++ my_print_constr env fullctyp) 
+     with _ -> () 
   in
   let evm = non_instanciated_map env isevars in
-  let _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in
+  let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
     evm, fullcoqc, fullctyp
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 823ff41af..7bfaa0c5c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -43,7 +43,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   module Cases = Cases.Cases_F(Coercion)
 
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
-  let allow_anonymous_refs = ref false
+  let allow_anonymous_refs = ref true
 
   let evd_comb0 f isevars =
     let (evd',x) = f !isevars in
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 966aa80a9..59c858a6a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -118,8 +118,8 @@ let print_args env args =
 let make_existential loc env isevars c =
   let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
   let (key, args) = destEvar evar in
-    debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
-	     print_args env args);
+    (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+		  print_args env args) with _ -> ());
     evar
 
 let make_existential_expr loc env c =
@@ -160,26 +160,27 @@ open Tactics
 open Tacticals
 
 let build_dependent_sum l =
-  let rec aux (acc, tac, typ) = function
+  let rec aux (tac, typ) = function
       (n, t) :: tl ->
 	let t' = mkLambda (Name n, t, typ) in
-	  trace (str ("treating " ^ string_of_id n) ++
-		 str "assert: " ++ my_print_constr (Global.env ()) t);
+	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
+	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+	   with _ -> ());
 	let tac' = 
-	  tclTHEN (assert_tac true (Name n) t) 
-	    (tclTHENLIST
-	       [intros;
-		(tclTHENSEQ 
-		   [tclTRY (constructor_tac (Some 1) 1 
-		       (Rawterm.ImplicitBindings [mkVar n]));
-		    tac]);
-	       ])
+	  tclTHENS (assert_tac true (Name n) t) 
+	    ([intros;
+	      (tclTHENSEQ 
+		 [constructor_tac (Some 1) 1 
+		    (Rawterm.ImplicitBindings [mkVar n]);
+		  tac]);
+	     ])
 	in
-	  aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl
-    | [] -> acc, tac, typ
+	let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
+	  aux (tac', newt) tl
+    | [] -> tac, typ
   in 
     match l with 
-	(_, hd) :: tl -> aux (hd, intros, hd) tl
+	(_, hd) :: tl -> aux (intros, hd) tl
       | [] -> raise (Invalid_argument "build_dependent_sum")
 
 open Proof_type
@@ -218,7 +219,8 @@ let and_tac l hook =
   let and_proof_id, and_goal, and_tac, and_extract = 
     match l with
       | [] -> raise (Invalid_argument "and_tac: empty list of goals")
-      | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+      | (hdid, x, hdg, hdt) :: tl -> 
+	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
   in
   let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
     Command.start_proof and_proofid goal_kind and_goal
@@ -238,7 +240,13 @@ let destruct_ex ext ex =
 		   try (args.(0), args.(1))
 		   with _ -> assert(false)
 		 in
-		   (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc)
+		 let pi1 = (mk_ex_pi1 dom rng acc) in
+		 let rng_body = 
+		   match kind_of_term rng with
+		       Lambda (_, _, t) -> subst1 pi1 t
+		     | t -> rng
+		 in
+		   pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
 	     | _ -> [acc])
       | _ -> [acc]
   in aux ex ext
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 5ef3af18e..a90f281ff 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -78,7 +78,7 @@ val mkProj1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 
-val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types
+val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
 val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->  
   ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit