indentation.

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

1 files changed, 77 insertions, 124 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index dd23166446..15d64155be 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -487,139 +487,110 @@ let get_funs_constant mp dp =
 exception No_graph_found 
 exception Found_type of int 
 
-let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = 
-  let env = Global.env () 
+let make_scheme (fas:(constant*Rawterm.rawsort)list): Entries.definition_entry list =
+  let env = Global.env ()
   and sigma = Evd.empty in
-  let funs = List.map fst fas in 
-  let first_fun = List.hd funs in 
-
-
+  let funs = List.map fst fas in
+  let first_fun = List.hd funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = 
-    try 
-      fst (find_Function_infos  first_fun).graph_ind 
-    with Not_found -> raise No_graph_found 
-  in
+    try fst (find_Function_infos  first_fun).graph_ind 
+    with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map fst this_block_funs_indexes in 
   let prop_sort = InProp in
   let funs_indexes = 
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.map
-      (function const -> List.assoc const this_block_funs_indexes)
-      funs
-  in
+    List.map (fun const -> List.assoc const this_block_funs_indexes) funs in
   let ind_list = 
     List.map 
       (fun (idx) -> 
 	 let ind = first_fun_kn,idx in 
 	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort
-      )
-      funs_indexes
-  in
+	 ind,mib,mip,true,prop_sort) funs_indexes in
   let l_schemes = 
-    List.map
-      (Typing.type_of env sigma) 
-      (Indrec.build_mutual_indrec env sigma ind_list)
-  in 
+    List.map (Typing.type_of env sigma) 
+      (Indrec.build_mutual_indrec env sigma ind_list) in 
   let i = ref (-1) in
   let sorts = 
     List.rev_map (fun (_,x) -> 
-		Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
-	     ) 
-      fas 
-  in
+      Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)) 
+      fas in
   (* We create the first priciple by tactic *)
   let first_type,other_princ_types = 
     match l_schemes with 
 	s::l_schemes -> s,l_schemes
-      | _ -> anomaly ""
-  in
+      | _ -> anomaly "" in
   let (_,(const,_,_)) = 
     build_functional_principle false
-      first_type
-      (Array.of_list sorts)
-      this_block_funs
-      0
+      first_type (Array.of_list sorts) this_block_funs 0
       (prove_princ_for_struct false 0 (Array.of_list funs))
-      (fun _ _ _ -> ())
-  in      
+      (fun _ _ _ -> ()) in      
   incr i;
   let opacity = 
     let finfos = find_Function_infos this_block_funs.(0) in 
     try 
       let equation =  Option.get finfos.equation_lemma in  
       (Global.lookup_constant equation).Declarations.const_opaque 
-    with Option.IsNone -> (* non recursive definition *) 
-      false
-  in
+    with Option.IsNone -> false in (* non recursive definition *) 
   let const = {const with const_entry_opaque = opacity } in 
   (* The others are just deduced *)
   if other_princ_types = [] 
-  then
-    [const]
+  then [const]
   else
     let other_fun_princ_types = 
       let sorts = Array.of_list sorts in 
-      List.map (compute_new_princ_type_from_rel (build_rel_to_fun_info this_block_funs) sorts)
+      List.map (compute_new_princ_type_from_rel 
+		   (build_rel_to_fun_info this_block_funs) sorts)
 	other_princ_types in
-    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in 
-    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+    let first_princ_body,first_princ_type = 
+      const.Entries.const_entry_body, const.Entries.const_entry_type in 
+    (* the principle has form forall ...., fix .*)
+    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in 
     let (idxs,_),(_,ta,_ as decl) = destFix fix in 
     let other_result = 
       List.map (* we can now compute the other principles *)
 	(fun scheme_type -> 
-	   incr i;
-	   observe (Printer.pr_lconstr scheme_type);
-	   let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
-	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
-	   let f = fst (decompose_app applied_f) in
-	   try (* we search the number of the function in the fix block (name of the function) *)
-	     Array.iteri 
-	     (fun j t -> 
+	  incr i;
+	  observe (Printer.pr_lconstr scheme_type);
+	  let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
+	  let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
+	  let f = fst (decompose_app applied_f) in
+	  try (* we search the number of the function in the fix block (name of
+		 the function) *)
+	    Array.iteri 
+	      (fun j t -> 
 		let t =  snd (Sign.decompose_prod_assum t) in 
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in 
 		let g = fst (decompose_app applied_g) in
 		if eq_constr f g
 		then raise (Found_type j); 
 		observe (Printer.pr_lconstr f ++ str " <> " ++
-			   Printer.pr_lconstr g)
-		  
-	     )
-	     ta;
-	   (* If we reach this point, the two principle are not mutually recursive 
-	      We fall back to the previous method 
-	   *)
-	     let (_,(const,_,_)) = 
-	       build_functional_principle
-		 false 
-		 (List.nth other_princ_types (!i - 1))
-		 (Array.of_list sorts)
-		 this_block_funs
-		 !i
-		 (prove_princ_for_struct false !i (Array.of_list funs))
-		 (fun _ _ _ -> ())
-	     in 
-	     const
-	 with Found_type i -> 
-	   let princ_body = 
-	     Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
-	   in 
-	   {const with 
+			    Printer.pr_lconstr g))
+	      ta;
+	    (* If we reach this point, the two principle are not mutually recursive 
+	       We fall back to the previous method *)
+	    let (_,(const,_,_)) = 
+	      build_functional_principle
+		false (List.nth other_princ_types (!i - 1)) 
+		(Array.of_list sorts) this_block_funs !i
+		(prove_princ_for_struct false !i (Array.of_list funs))
+		(fun _ _ _ -> ()) in 
+	    const
+	  with Found_type i -> 
+	    let princ_body = 
+	      Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt in 
+	    {const with 
 	      Entries.const_entry_body = princ_body; 
-	      Entries.const_entry_type = Some scheme_type
-	   }
-      )
-      other_fun_princ_types
-    in
+	      Entries.const_entry_type = Some scheme_type})
+	other_fun_princ_types in
     const::other_result
 
 let build_scheme fas = 
   let bodies_types = 
     make_scheme 
       (List.map 
-	 (fun (_,f,sort) -> 
+	  (fun (_,f,sort) -> 
 	    let f_as_constant =
 	      try
 		match Nametab.global f with 
@@ -628,72 +599,54 @@ let build_scheme fas =
 	      with Not_found ->
 	      	Util.error ("Cannot find "^ Libnames.string_of_reference f)
 	    in
-	    (f_as_constant,sort)
-	 ) 
-	 fas
-      ) 
-  in 
+	    (f_as_constant,sort)) 
+	  fas) in 
   List.iter2 
     (fun (princ_id,_,_) def_entry -> 
-       ignore 
-	 (Declare.declare_constant 
+      ignore 
+	(Declare.declare_constant 
 	    princ_id 
 	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-       Flags.if_verbose 
-	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
-    )
-    fas
-    bodies_types
+      Flags.if_verbose 
+	(fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id)
+    fas bodies_types
   
 
 
 let build_case_scheme fa = 
   let env = Global.env () 
   and sigma = Evd.empty in
-(*   let id_to_constr id =  *)
-(*     Tacinterp.constr_of_id env  id *)
-(*   in  *)
-  let funs =  (fun (_,f,_) ->  
-		 try Libnames.constr_of_global (Nametab.global f)
-		 with Not_found -> 
-		   Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in 
+  (* let id_to_constr id = Tacinterp.constr_of_id env  id in  *)
+  let funs = 
+    (fun (_,f,_) ->  
+      try Libnames.constr_of_global (Nametab.global f)
+      with Not_found -> 
+	Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in 
   let first_fun = destConst  funs in 
-
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
-  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
-
-
-
+  let first_fun_kn = 
+    try fst (find_Function_infos  first_fun).graph_ind
+    with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map fst this_block_funs_indexes in 
   let prop_sort = InProp in
   let funs_indexes = 
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.assoc (destConst funs) this_block_funs_indexes
-  in
-  let ind_fun = 
-	 let ind = first_fun_kn,funs_indexes in 
-	 ind,prop_sort
-  in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
+    List.assoc (destConst funs) this_block_funs_indexes in
+  let ind_fun = let ind = first_fun_kn,funs_indexes in ind,prop_sort in
+  let scheme_type =  
+    (Typing.type_of env sigma) 
+      ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
   let sorts =
-    (fun (_,_,x) ->
-       Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
-    )
-      fa
-  in
+    (fun (_,_,x) -> 
+      Termops.new_sort_in_family (Pretyping.interp_elimination_sort x))
+      fa in
   let princ_name =  (fun (x,_,_) -> x) fa in
   let _ = 
 (*     observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
 (* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
 (* 	    ); *)
-    generate_functional_principle
-      false
-      scheme_type
-      (Some ([|sorts|]))
-      (Some princ_name)
-      this_block_funs
-      0
-      (prove_princ_for_struct false 0 [|destConst funs|])
-  in
+    generate_functional_principle false scheme_type (Some ([|sorts|]))
+      (Some princ_name) this_block_funs 0 
+      (prove_princ_for_struct false 0 [|destConst funs|]) in
   ()