Code cleaning in Function

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

4 files changed, 114 insertions, 122 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 77c9de92c..14ee8efa2 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -39,7 +39,8 @@ let functional_induction with_clean c princl pat =
 		      let finfo = (* we first try to find out a graph on f *)
 			try find_Function_infos c' 
 			with Not_found -> 
-			  errorlabstrm "" (str "Cannot find induction information on "++Printer.pr_lconstr (mkConst c') )
+			  errorlabstrm "" (str "Cannot find induction information on "++
+					     Printer.pr_lconstr (mkConst c') )
 		      in
 		      match Tacticals.elimination_sort_of_goal g with 
 			| InProp -> finfo.prop_lemma
@@ -49,8 +50,9 @@ let functional_induction with_clean c princl pat =
 		    let princ =  (* then we get the principle *)
 		      try mkConst (out_some princ_option )
 		      with Failure "out_some" -> 
-			(*i If there is not default lemma defined then, we cross our finger and try to 
-		    find a lemma named f_ind (or f_rec, f_rect) i*)
+			(*i If there is not default lemma defined then, 
+			  we cross our finger and try to find a lemma named f_ind 
+			  (or f_rec, f_rect) i*)
 			let princ_name = 
 			  Indrec.make_elimination_ident
 			    (id_of_label (con_label c'))
@@ -90,39 +92,39 @@ let functional_induction with_clean c princl pat =
     let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in 
     let old_idl = Idset.diff old_idl princ_vars in 
     let subst_and_reduce g = 
-      let idl = 
-	map_succeed 
-	  (fun id -> 
-	    if Idset.mem id old_idl then failwith "subst_and_reduce";
-	    id 
-	  )
-	  (Tacmach.pf_ids_of_hyps g)
-      in 
-      let flag = 
-	Rawterm.Cbv
-	  {Rawterm.all_flags 
-	  with Rawterm.rDelta = false; 		 
-	  }
-      in
       if with_clean 
       then
+	let idl = 
+	  map_succeed 
+	    (fun id -> 
+	       if Idset.mem id old_idl then failwith "subst_and_reduce";
+	       id 
+	    )
+	    (Tacmach.pf_ids_of_hyps g)
+	in 
+	let flag = 
+	  Rawterm.Cbv
+	    {Rawterm.all_flags 
+	     with Rawterm.rDelta = false; 		 
+	    }
+	in
 	Tacticals.tclTHEN
 	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
 	  (Hiddentac.h_reduce flag Tacticals.allClauses)	
 	  g
       else Tacticals.tclIDTAC g 
-
+	
     in
     Tacticals.tclTHEN
       (choose_dest_or_ind 
-	princ_infos
-	args_as_induction_constr
-	princ'
-	pat)
+	 princ_infos
+	 args_as_induction_constr
+	 princ'
+	 pat)
       subst_and_reduce
       g
-
-
+      
+      
 
 
 type annot = 
@@ -243,17 +245,22 @@ let derive_inversion fix_names =
     Invfun.derive_correctness 
       Functional_principles_types.make_scheme
       functional_induction 
-	  (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
+      (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
       (*i The next call to mk_rel_id is valid since we have just construct the graph 
 	Ensures by : register_built
 	i*) 
-      (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
+      (List.map
+	 (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+	 fix_names
+      )
   with e -> 
-    msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
+    msg_warning 
+      (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
 	  
 let generate_principle 
     do_built fix_rec_l recdefs  interactive_proof parametrize 
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
+    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
+      Tacmach.tactic) : unit =
   let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
@@ -365,7 +372,8 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Command.generalize_constr_expr unbounded_eq args in 
-  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+      nb_args relation =
     try 
       pre_hook 
 	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
@@ -469,7 +477,9 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 		     in 
 		     let annot = 
 		       try Some (list_index (Name id) names - 1), Topconstr.CStructRec 
-		       with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) 
+		       with Not_found -> 
+			 raise (UserError("",str "Cannot find argument " ++ 
+					    Ppconstr.pr_id id)) 
 		     in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
 		 | (name,None,args,types,body),recdef -> 
@@ -479,7 +489,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 			 (dummy_loc,"Function",
 			  Pp.str "the recursive argument needs to be specified in Function")
 		     else 
-		       (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+		       (name,(Some 0, Topconstr.CStructRec),args,types,body),
+		     (None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
@@ -517,9 +528,13 @@ let rec add_args id new_args b =
   | CArrow(loc,b1,b2) -> 
       CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) -> 
-      CProdN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args  b1)
+      CProdN(loc,
+	     List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, 
+	     add_args id new_args  b1)
   | CLambdaN(loc,nal,b1) -> 
-      CLambdaN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, add_args id new_args  b1)
+      CLambdaN(loc,
+	       List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, 
+	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) -> 
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
   | CAppExpl(loc,(pf,r),exprl) -> 
@@ -530,10 +545,13 @@ let rec add_args id new_args b =
 	| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
       end
   | CApp(loc,(pf,b),bl) -> 
-      CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl)
+      CApp(loc,(pf,add_args id new_args b), 
+	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
   | CCases(loc,b_option,cel,cal) -> 
       CCases(loc,option_map (add_args id new_args) b_option,
-	     List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,option_map (add_args id new_args) b_option)) cel, 
+	     List.map (fun (b,(na,b_option)) -> 
+			 add_args id new_args b,
+			 (na,option_map (add_args id new_args) b_option)) cel, 
 	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) -> 
@@ -578,41 +596,16 @@ let make_graph (f_ref:global_reference) =
 	let env = Global.env () in
 	let body = (force b) in
 	let extern_body,extern_type = 
-	  let old_implicit_args = Impargs.is_implicit_args ()
-	  and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
-	  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
-	  let old_rawprint = !Options.raw_print in 
-	  Options.raw_print := true;
-	  Impargs.make_implicit_args false;
-	  Impargs.make_strict_implicit_args false;
-	  Impargs.make_contextual_implicit_args false;
-	  try 
-	    let res =  Constrextern.extern_constr false env body in 
-	    let res' = Constrextern.extern_type false env  c_body.const_type in 
-	    Impargs.make_implicit_args old_implicit_args;
-	    Impargs.make_strict_implicit_args old_strict_implicit_args;
-	    Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-	    Options.raw_print := old_rawprint;
-	    res,res'
-	  with
-	    | UserError(s,msg) as e -> 
-		Impargs.make_implicit_args old_implicit_args;
-		Impargs.make_strict_implicit_args old_strict_implicit_args;
-		Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-		Options.raw_print := old_rawprint;
-		raise e
-	    | e -> 
-		Impargs.make_implicit_args old_implicit_args;
-		Impargs.make_strict_implicit_args old_strict_implicit_args;
-		Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-		Options.raw_print := old_rawprint;
-		raise e
+	  with_full_print 
+	    (fun () -> 
+	       (Constrextern.extern_constr false env body, 
+		Constrextern.extern_type false env  c_body.const_type
+	       )
+	    )
+	    ()
 	in
 	let rec get_args b t : Topconstr.local_binder list * 
 	    Topconstr.constr_expr * Topconstr.constr_expr = 
-(* 	  Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
-(* 	  Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
-(* 	  Pp.msgnl (fnl ()); *)
 	  match b with 
 	    | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
 		begin
@@ -637,7 +630,8 @@ let make_graph (f_ref:global_reference) =
 		    else t
 		  in 
 		  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-		  (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
+		  (List.map (fun (nal,ta) -> 
+			       (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
 		end
 	    | _ -> [],b,t
 	in
@@ -659,7 +653,8 @@ let make_graph (f_ref:global_reference) =
 			   )
 		       in 
 		       let rec_id = 
-			 match List.nth bl' (out_some n)  with |(_,Name id) -> id | _ -> anomaly ""
+			 match List.nth bl' (out_some n)  with 
+			   |(_,Name id) -> id | _ -> anomaly ""
 		       in
 		       let new_args = 
 			 List.flatten 
@@ -667,7 +662,10 @@ let make_graph (f_ref:global_reference) =
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
 			      	 | Topconstr.LocalRawAssum (nal,_) -> 
-				     List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+				     List.map 
+				       (fun (loc,n) -> 
+					  CRef(Libnames.Ident(loc, Nameops.out_name n))) 
+				       nal
 			      )
 			      nal_tas
 			   )
@@ -685,7 +683,9 @@ let make_graph (f_ref:global_reference) =
 	do_generate_principle false false expr_list;
 	(* We register the infos *)
 	let mp,dp,_ = repr_con c in 
-	List.iter (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) expr_list
+	List.iter 
+	  (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) 
+	  expr_list
 
 
 (* let make_graph _ = assert false	 *)
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index f41aac205..20263c188 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -233,6 +233,32 @@ let get_proof_clean do_reduce =
   Pfedit.delete_current_proof ();
   result
 
+let with_full_print f a = 
+  let old_implicit_args = Impargs.is_implicit_args ()
+  and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
+  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+  let old_rawprint = !Options.raw_print in 
+  Options.raw_print := true;
+  Impargs.make_implicit_args false;
+  Impargs.make_strict_implicit_args false;
+  Impargs.make_contextual_implicit_args false;
+  try 
+    let res = f a in 
+    Impargs.make_implicit_args old_implicit_args;
+    Impargs.make_strict_implicit_args old_strict_implicit_args;
+    Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+    Options.raw_print := old_rawprint;
+    res
+  with  
+    | e -> 
+	Impargs.make_implicit_args old_implicit_args;
+	Impargs.make_strict_implicit_args old_strict_implicit_args;
+	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+	Options.raw_print := old_rawprint;
+	raise e
+
+
+
 
 
 
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 00e1ce8d9..2142d29b3 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -73,6 +73,12 @@ val get_proof_clean : bool ->
     
 
 
+(* [with_full_print f a] applies [f] to [a] in full printing environment 
+   
+   This function preserves the print settings 
+*)
+val with_full_print : ('a -> 'b) -> 'a -> 'b
+
 
 (*****************)
 
@@ -103,3 +109,4 @@ val pr_table : unit -> Pp.std_ppcmds
 
 val function_debug : bool ref 
 val do_observe : unit -> bool
+
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index dbf2f9441..1b5ed99f5 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1108,19 +1108,7 @@ let build_inductive
       (function result (* (args',concl') *) -> 
 	 let rt = compose_raw_context result.context result.value in 
 	 let nb_args = List.length funsargs.(i) in 
-(* 	   let old_implicit_args = Impargs.is_implicit_args () *)
-(* 	   and old_strict_implicit_args =  Impargs.is_strict_implicit_args () *)
-(* 	   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *)
-(* 	   let old_rawprint = !Options.raw_print in  *)
-(* 	   Options.raw_print := true; *)
-(* 	   Impargs.make_implicit_args false; *)
-(* 	   Impargs.make_strict_implicit_args false; *)
-(* 	   Impargs.make_contextual_implicit_args false; *)
-(* 	   Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
-(* 	   Impargs.make_implicit_args old_implicit_args; *)
-(* 	   Impargs.make_strict_implicit_args old_strict_implicit_args; *)
-(* 	   Impargs.make_contextual_implicit_args old_contextual_implicit_args; *)
-(* 	   Options.raw_print := old_rawprint; *)
+	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
 	 fst (
 	   rebuild_cons nb_args relnames.(i)
 	     []
@@ -1182,8 +1170,6 @@ let build_inductive
      Then save the graphs and reset Printing options to their primitive values 
   *)
   let rel_arities = Array.mapi rel_arity funsargs in
-  let old_rawprint = !Options.raw_print in 
-  Options.raw_print := true;
   let rel_params =  
     List.map 
       (fun (n,t,is_defined) -> 
@@ -1199,7 +1185,11 @@ let build_inductive
   let ext_rels_constructors = 
     Array.map (List.map 
       (fun (id,t) -> 
-	 false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t))
+	 false,((dummy_loc,id),
+		Options.with_option
+		  Options.raw_print
+		  (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
+	       )
       ))
       (rel_constructors)
   in
@@ -1232,58 +1222,27 @@ let build_inductive
 (* 	rel_inds *)
 (*     ) *)
 (*   in *)
-  let old_implicit_args = Impargs.is_implicit_args ()
-  and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
-  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
-  Impargs.make_implicit_args false;
-  Impargs.make_strict_implicit_args false;
-  Impargs.make_contextual_implicit_args false;
   let _time2 = System.get_time () in 
-(*   Pp.msgnl (str "Bulding Inductive : " ++ str (string_of_float (System.time_difference time1 time2))); *)
   try 
-    Options.silently (Command.build_mutual rel_inds) true;
-    let _time3 = System.get_time () in 
-(*     Pp.msgnl (str "Bulding Done: "++ str (string_of_float (System.time_difference time2 time3)));  *)
-(* 	let msg = *)
-(* 	  str "while trying to define"++ spc () ++ *)
-(* 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () *)
-(* 	in *)
-(*  	Pp.msgnl msg; *)
-    Impargs.make_implicit_args old_implicit_args;
-    Impargs.make_strict_implicit_args old_strict_implicit_args;
-    Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-    Options.raw_print := old_rawprint;
-  with
+    with_full_print (Options.silently (Command.build_mutual rel_inds)) true
+  with 
     | UserError(s,msg) ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	Impargs.make_implicit_args old_implicit_args;
-	Impargs.make_strict_implicit_args old_strict_implicit_args;
-	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-	Options.raw_print := old_rawprint;
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
 	    msg
 	in
 	observe (msg);
-	raise 
-	  (UserError(s, msg))
+	raise (UserError(s, msg))
     | e -> 
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	Impargs.make_implicit_args old_implicit_args;
-	Impargs.make_strict_implicit_args old_strict_implicit_args;
-	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
-	Options.raw_print := old_rawprint;
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
  	observe msg;
-	raise 
-	  (UserError("",msg))
-
-
-
+	raise (UserError("",msg))