Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

4 files changed, 31 insertions, 221 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 14e2233f..ff4f7499 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1380,219 +1380,6 @@ let is_valid_hypothesis predicates_name =
 	| _ -> false 
   in
   is_valid_hypothesis 
-(*
-let fresh_id avoid na = 
-  let id =  
-    match na with 
-      | Name id -> id 
-      | Anonymous -> h_id 
-  in 
-  next_global_ident_away true id avoid
-
-
-let prove_principle_for_gen
-    (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
-    rec_arg_num rec_arg_type relation = 
-  fun g -> 
-    let type_of_goal = pf_concl g in 
-    let goal_ids = pf_ids_of_hyps g in 
-    let goal_elim_infos = compute_elim_sig type_of_goal in 
-    let params_names,ids = List.fold_left 
-      (fun (params_names,avoid) (na,_,_) -> 
-	 let new_id = fresh_id avoid na in 
-	 (new_id::params_names,new_id::avoid)
-      )
-      ([],goal_ids)
-      goal_elim_infos.params
-    in
-    let predicates_names,ids = 
-      List.fold_left 
-	(fun (predicates_names,avoid) (na,_,_) -> 
-	   let new_id = fresh_id avoid na in 
-	   (new_id::predicates_names,new_id::avoid)
-	)
-	([],ids)
-	goal_elim_infos.predicates
-    in
-    let branches_names,ids = 
-      List.fold_left 
-	(fun (branches_names,avoid) (na,_,_) -> 
-	   let new_id = fresh_id avoid na in 
-	   (new_id::branches_names,new_id::avoid)
-	)
-	([],ids)
-	goal_elim_infos.branches
-    in
-    let to_intro = params_names@predicates_names@branches_names in 
-    let nparams = List.length params_names in 
-    let rec_arg_num = rec_arg_num - nparams in 
-    let tac_intro_static = h_intros to_intro in 
-    let args_info = ref None in 
-    let arg_tac g =  (* introducing args *)
-      let ids = pf_ids_of_hyps g in 
-      let func_body = def_of_const (mkConst functional_ref) in
-      (* 	      let _ = Pp.msgnl (Printer.pr_lconstr func_body) in  *)
-      let (f_name, _, body1) = destLambda func_body in
-      let f_id =
-	match f_name with
-	  | Name f_id -> next_global_ident_away true f_id ids
-	  | Anonymous -> anomaly "anonymous function"
-      in
-      let n_names_types,_ = decompose_lam body1 in 
-      let n_ids,ids = 
-	List.fold_left 
-	  (fun (n_ids,ids) (n_name,_) -> 
-	     match n_name with 
-	       | Name id -> 
-		   let n_id = next_global_ident_away true id ids in 
-		   n_id::n_ids,n_id::ids
-	       | _ -> anomaly "anonymous argument"
-	  )
-	  ([],(f_id::ids))
-	  n_names_types
-      in
-      let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in
-      let args_ids = snd (list_chop nparams n_ids) in
-      args_info := Some (ids,args_ids,rec_arg_id);
-      h_intros args_ids g
-    in
-    let wf_tac = 
-      if is_mes 
-      then 
-	(fun b -> Recdef.tclUSER_if_not_mes b None)
-      else fun _ -> prove_with_tcc tcc_lemma_ref []
-    in
-    let start_tac g = 
-      let ids,args_ids,rec_arg_id = out_some !args_info in
-      let nargs = List.length args_ids in 
-      let pre_rec_arg = 
-	List.rev_map 
-	  mkVar 
-	  (fst (list_chop (rec_arg_num - 1) args_ids))
-      in
-      let args_before_rec = pre_rec_arg@(List.map mkVar params_names) in
-      let relation = substl args_before_rec relation in 
-      let input_type = substl args_before_rec rec_arg_type in 
-      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in 
-      let wf_rec_arg = 
-	next_global_ident_away true 
-	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
-	  (wf_thm::ids) 
-      in 
-      let hrec = next_global_ident_away true hrec_id (wf_rec_arg::wf_thm::ids) in 
-      let acc_inv = 
-	lazy (
-	  mkApp (
-	    delayed_force acc_inv_id,
-	    [|input_type;relation;mkVar rec_arg_id|]
-	  )
-	)
-      in
-      (tclTHENS
-	   (observe_tac 
-	      "first assert" 
-	      (assert_tac 
-		 true (* the assert thm is in first subgoal *)
-		 (Name wf_rec_arg) 
-		 (mkApp (delayed_force acc_rel,
-			 [|input_type;relation;mkVar rec_arg_id|])
-		 )
-	      )
-	   )
-	   [
-	     (* accesibility proof *) 
-	     tclTHENS 
-	       (observe_tac 
-		  "second assert" 
-		  (assert_tac 
-		     true 
-		     (Name wf_thm)
-		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  )
-	       )
-	       [ 
-		 (* interactive proof of the well_foundness of the relation *) 
-		 wf_tac is_mes;
-		 (* well_foundness -> Acc for any element *)
-		 observe_tac 
-		   "apply wf_thm" 
-		   (h_apply ((mkApp(mkVar wf_thm,
-				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
-		   )
-	       ]
-	     ;
-	     (* rest of the proof *)
-	     tclTHENSEQ
-	       [
-		 observe_tac "generalize" (fun g -> 
-		    let to_thin = 
-		      fst (list_chop ( nargs + 1) (pf_ids_of_hyps g))
-		    in
-		    let to_thin_c = List.rev_map mkVar to_thin in 
-		    tclTHEN (generalize to_thin_c) (observe_tac "thin" (h_clear false to_thin)) g
-		 );
-		 observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
-		h_intros args_ids;
-		h_intro wf_rec_arg;
-		Equality.rewriteLR (mkConst eq_ref);
-		(fun g' -> 
-		   let body = 
-		     let _,args = destApp (pf_concl g') in 
-		     array_last args
-		   in
-		   let body_info rec_hyps = 
-		     {
-		       nb_rec_hyps = List.length rec_hyps;
-		       rec_hyps = rec_hyps;
-		       eq_hyps = [];
-		       info = body
-		     }
-		   in 
-		   let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  wf_rec_arg|]) )  in
-		   let pte_info = 
-		     { proving_tac =
-			 (fun eqs -> 
-			    observe_tac "new_prove_with_tcc" 
-			      (new_prove_with_tcc is_mes acc_inv hrec  tcc_lemma_ref (List.map mkVar eqs))
-			 );
-		       is_valid = is_valid_hypothesis predicates_names 
-		     }
-		   in
-		   let ptes_info : pte_info Idmap.t = 
-		     List.fold_left
-		       (fun map pte_id -> 
-			  Idmap.add pte_id 
-			    pte_info			       
-			    map
-		       )
-		       Idmap.empty
-		       predicates_names
-		   in
-		   let make_proof rec_hyps = 
-		     build_proof 
-		       false 
-		       [f_ref]
-		       ptes_info
-		       (body_info rec_hyps)
-		   in
-		   instanciate_hyps_with_args 
-		     make_proof
-		     branches_names
-		     args_ids
-		     g'
-		     
-		) 
-	       ]
-	   ]
-	   g
-      )
-      in
-      tclTHENSEQ 
-	[tac_intro_static;
-	 arg_tac;
-	 start_tac
-	] g
-*)
 
 let prove_principle_for_gen
     (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
@@ -1627,14 +1414,22 @@ let prove_principle_for_gen
   in
   let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
   let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in 
+  observe (
+    str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++
+    str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ 
+      str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ 
+    str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ 
+	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++
+	     str "npost_rec_arg := " ++ int npost_rec_arg );
   let (post_rec_arg,pre_rec_arg) = 
     Util.list_chop npost_rec_arg princ_info.args
   in
   let rec_arg_id = 
-    match post_rec_arg with 
+    match List.rev post_rec_arg with 
       | (Name id,_,_)::_ -> id 
       | _ -> assert false 
   in
+  observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id));
   let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in 
   let relation = substl subst_constrs relation in 
   let input_type = substl subst_constrs rec_arg_type in 
@@ -1679,7 +1474,7 @@ let prove_principle_for_gen
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
       );
       observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
-      observe_tac "h_fix" (h_fix (Some fix_id) (real_rec_arg_num + 1)); 
+      observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1)); 
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Equality.rewriteLR (mkConst eq_ref);
       observe_tac "finish" (fun gl' -> 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 89ebb75a..8ad2e72b 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -405,11 +405,26 @@ let generate_functional_principle
   let (id,(entry,g_kind,hook)) =
     build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook 
   in
+  (* Pr  1278 :
+     Don't forget to close the goal if an error is raised !!!!
+  *) 
   save false new_princ_name entry g_kind hook
-  with 
-    | Defining_principle _ as e -> raise e
-    | e -> raise (Defining_principle e)
-
+  with e -> 
+    begin
+      begin 
+	try 
+	  let id = Pfedit.get_current_proof_name () in 
+	  let s = string_of_id id in 
+	  let n = String.length "___________princ_________" in
+	  if String.length s >= n 
+	  then if String.sub s 0 n = "___________princ_________" 
+	  then Pfedit.delete_current_proof ()
+	  else ()
+	  else ()
+	with _ -> ()
+      end;
+      raise (Defining_principle e)
+    end
 (*   defined  () *)
 
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 82bb2869..6e2af224 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -266,7 +266,7 @@ let derive_inversion fix_names =
 	)
     with e -> 
       msg_warning 
-	(str "Cannot built inversion information" ++ 
+	(str "Cannot build functional inversion principle" ++ 
 	   if do_observe () then Cerrors.explain_exn e else mt ())
   with _ -> ()
 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index ed46ec72..ba5c2bbd 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -561,7 +561,7 @@ let ids_of_rawterm c =
       | RCases (loc,rtntypopt,tml,brchl) -> 
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
       | RRec _ -> failwith "Fix inside a constructor branch"
-      | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> []
+      | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
   in
   (* build the set *)
   List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)