Cosmetic: no more whitespace at end of lines in extraction files

(diff says it's a big commit, whereas diff -w says it's an empty one ;-)

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

1 files changed, 145 insertions, 145 deletions

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 66cb8d4e17..1612c8dd84 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -27,73 +27,73 @@ let occur_kn_in_ref kn = function
   | ConstructRef ((kn',_),_) -> kn = kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
-      
-let modpath_of_r = function 
+
+let modpath_of_r = function
   | ConstRef kn -> con_modpath kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> modpath kn
   | VarRef _ -> assert false
-      
-let label_of_r = function 
+
+let label_of_r = function
   | ConstRef kn -> con_label kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> label kn
   | VarRef _ -> assert false
 
-let rec base_mp = function 
-  | MPdot (mp,l) -> base_mp mp 
-  | mp -> mp 
+let rec base_mp = function
+  | MPdot (mp,l) -> base_mp mp
+  | mp -> mp
 
 let rec mp_length = function
   | MPdot (mp, _) -> 1 + (mp_length mp)
   | _ -> 1
 
-let is_modfile = function 
-  | MPfile _ -> true 
+let is_modfile = function
+  | MPfile _ -> true
   | _ -> false
 
-let string_of_modfile = function 
+let string_of_modfile = function
   | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
   | _ -> assert false
 
-let rec modfile_of_mp = function 
+let rec modfile_of_mp = function
   | (MPfile _) as mp -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp 
+  | MPdot (mp,_) -> modfile_of_mp mp
   | _ -> raise Not_found
 
 let current_toplevel () = fst (Lib.current_prefix ())
 
-let is_toplevel mp = 
+let is_toplevel mp =
   mp = initial_path || mp = current_toplevel ()
 
-let at_toplevel mp = 
+let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let visible_kn kn = at_toplevel (base_mp (modpath kn))
 let visible_con kn = at_toplevel (base_mp (con_modpath kn))
 
-let rec prefixes_mp mp = match mp with 
+let rec prefixes_mp mp = match mp with
   | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
-  | _ -> MPset.singleton mp 
+  | _ -> MPset.singleton mp
 
 let rec get_nth_label_mp n = function
   | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
   | _ -> failwith "get_nth_label: not enough MPdot"
 
-let common_prefix_from_list mp0 mpl = 
-  let prefixes = prefixes_mp mp0 in 
-  let rec f = function 
+let common_prefix_from_list mp0 mpl =
+  let prefixes = prefixes_mp mp0 in
+  let rec f = function
     | [] -> raise Not_found
-    | mp :: l -> if MPset.mem mp prefixes then mp else f l 
+    | mp :: l -> if MPset.mem mp prefixes then mp else f l
   in f mpl
 
-let rec parse_labels ll = function 
-  | MPdot (mp,l) -> parse_labels (l::ll) mp 
+let rec parse_labels ll = function
+  | MPdot (mp,l) -> parse_labels (l::ll) mp
   | mp -> mp,ll
 
-let labels_of_mp mp = parse_labels [] mp 
+let labels_of_mp mp = parse_labels [] mp
 
-let labels_of_ref r = 
+let labels_of_ref r =
  let mp,_,l =
   match r with
      ConstRef con -> repr_con con
@@ -103,17 +103,17 @@ let labels_of_ref r =
  in
   parse_labels [l] mp
 
-let rec add_labels_mp mp = function 
-  | [] -> mp 
+let rec add_labels_mp mp = function
+  | [] -> mp
   | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
 
 
 (*S The main tables: constants, inductives, records, ... *)
 
-(* Theses tables are not registered within coq save/undo mechanism 
+(* Theses tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
-(*s Constants tables. *) 
+(*s Constants tables. *)
 
 let terms = ref (Cmap.empty : ml_decl Cmap.t)
 let init_terms () = terms := Cmap.empty
@@ -123,7 +123,7 @@ let lookup_term kn = Cmap.find kn !terms
 let types = ref (Cmap.empty : ml_schema Cmap.t)
 let init_types () = types := Cmap.empty
 let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types 
+let lookup_type kn = Cmap.find kn !types
 
 (*s Inductives table. *)
 
@@ -137,18 +137,18 @@ let lookup_ind kn = KNmap.find kn !inductives
 let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
-let add_recursors env kn = 
-  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in 
-  let mib = Environ.lookup_mind kn env in 
-  Array.iter 
-    (fun mip -> 
-       let id = mip.mind_typename in 
+let add_recursors env kn =
+  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in
+  let mib = Environ.lookup_mind kn env in
+  Array.iter
+    (fun mip ->
+       let id = mip.mind_typename in
        let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
+       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
        recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
     mib.mind_packets
 
-let is_recursor = function 
+let is_recursor = function
   | ConstRef kn -> Cset.mem kn !recursors
   | _ -> false
 
@@ -178,20 +178,20 @@ let modular () = !modular_ref
 
 (*s Tables synchronization. *)
 
-let reset_tables () = 
-  init_terms (); init_types (); init_inductives (); init_recursors (); 
+let reset_tables () =
+  init_terms (); init_types (); init_inductives (); init_recursors ();
   init_projs (); init_axioms ()
 
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
-   WARNING: for inductive objects, an extract_inductive must have been 
+   WARNING: for inductive objects, an extract_inductive must have been
    done before. *)
 
-let safe_id_of_global = function 
+let safe_id_of_global = function
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) -> 
+  | ConstructRef ((kn,i),j) ->
       (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
@@ -219,21 +219,21 @@ let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
 
 let err s = errorlabstrm "Extraction" s
 
-let warning_axioms () = 
-  let info_axioms = Refset.elements !info_axioms in 
-  if info_axioms = [] then () 
+let warning_axioms () =
+  let info_axioms = Refset.elements !info_axioms in
+  if info_axioms = [] then ()
   else begin
-    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
-    msg_warning 
+    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
+    msg_warning
       (str ("The following "^s^" must be realized in the extracted code:")
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
-  let log_axioms = Refset.elements !log_axioms in 
+  let log_axioms = Refset.elements !log_axioms in
   if log_axioms = [] then ()
   else begin
-    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" 
-    in 
+    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
+    in
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
        hov 1
@@ -254,51 +254,51 @@ let warning_both_mod_and_cst q mp r =
     str "First choice is assumed, for the second one please use " ++
     str "fully qualified name." ++ fnl ())
 
-let error_axiom_scheme r i = 
+let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
-       str " type variable(s).") 
+       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+       str " type variable(s).")
 
-let check_inside_module () = 
-  if Lib.is_modtype () then 
+let check_inside_module () =
+  if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
-	 str "Close it and try again.") 
-  else if Lib.is_module () then 
+	 str "Close it and try again.")
+  else if Lib.is_module () then
     msg_warning
       (str "Extraction inside an opened module is experimental.\n" ++
        str "In case of problem, close it first.\n")
 
-let check_inside_section () = 
-  if Lib.sections_are_opened () then 
+let check_inside_section () =
+  if Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
-let error_constant r = 
-  err (safe_pr_global r ++ str " is not a constant.") 
+let error_constant r =
+  err (safe_pr_global r ++ str " is not a constant.")
 
-let error_inductive r = 
+let error_inductive r =
   err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
 
-let error_nb_cons () = 
+let error_nb_cons () =
   err (str "Not the right number of constructors.")
 
-let error_module_clash s = 
-  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
-       str "This is not supported yet. Please do some renaming first.") 
+let error_module_clash s =
+  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++
+       str "This is not supported yet. Please do some renaming first.")
 
-let error_unknown_module m = 
-  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 
+let error_unknown_module m =
+  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
-let error_scheme () = 
+let error_scheme () =
   err (str "No Scheme modular extraction available yet.")
 
-let error_not_visible r = 
+let error_not_visible r =
   err (safe_pr_global r ++ str " is not directly visible.\n" ++
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
-let error_MPfile_as_mod mp b = 
-  let s1 = if b then "asked" else "required" in 
+let error_MPfile_as_mod mp b =
+  let s1 = if b then "asked" else "required" in
   let s2 = if b then "extract some objects of this module or\n" else "" in
   err (str ("Extraction of file "^(string_of_modfile mp)^
 	    ".v as a module is "^s1^".\n"^
@@ -309,19 +309,19 @@ let error_record r =
   err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
        fnl () ++ str "To help extraction, please use an explicit name.")
 
-let check_loaded_modfile mp = match base_mp mp with 
-  | MPfile dp -> if not (Library.library_is_loaded dp) then 
+let check_loaded_modfile mp = match base_mp mp with
+  | MPfile dp -> if not (Library.library_is_loaded dp) then
       err (str ("Please load library "^(string_of_dirpath dp^" first.")))
   | _ -> ()
 
-let info_file f =   
-  Flags.if_verbose message 
+let info_file f =
+  Flags.if_verbose message
     ("The file "^f^" has been created by extraction.")
 
 
 (*S The Extraction auxiliary commands *)
 
-(* The objects defined below should survive an arbitrary time, 
+(* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
 (*s Extraction AutoInline *)
@@ -330,11 +330,11 @@ let auto_inline_ref = ref true
 
 let auto_inline () = !auto_inline_ref
 
-let _ = declare_bool_option 
+let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction AutoInline";
 	   optkey = SecondaryTable ("Extraction", "AutoInline");
-	   optread = auto_inline; 
+	   optread = auto_inline;
 	   optwrite = (:=) auto_inline_ref}
 
 (*s Extraction TypeExpand *)
@@ -343,17 +343,17 @@ let type_expand_ref = ref true
 
 let type_expand () = !type_expand_ref
 
-let _ = declare_bool_option 
+let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction TypeExpand";
 	   optkey = SecondaryTable ("Extraction", "TypeExpand");
-	   optread = type_expand; 
+	   optread = type_expand;
 	   optwrite = (:=) type_expand_ref}
 
 (*s Extraction Optimize *)
 
-type opt_flag = 
-    { opt_kill_dum : bool; (* 1 *) 
+type opt_flag =
+    { opt_kill_dum : bool; (* 1 *)
       opt_fix_fun : bool;   (* 2 *)
       opt_case_iot : bool;  (* 4 *)
       opt_case_idr : bool;  (* 8 *)
@@ -367,12 +367,12 @@ type opt_flag =
 
 let kth_digit n k = (n land (1 lsl k) <> 0)
 
-let flag_of_int n = 
+let flag_of_int n =
     { opt_kill_dum = kth_digit n 0;
       opt_fix_fun = kth_digit n 1;
       opt_case_iot = kth_digit n 2;
       opt_case_idr = kth_digit n 3;
-      opt_case_idg = kth_digit n 4; 
+      opt_case_idg = kth_digit n 4;
       opt_case_cst = kth_digit n 5;
       opt_case_fun = kth_digit n 6;
       opt_case_app = kth_digit n 7;
@@ -380,7 +380,7 @@ let flag_of_int n =
       opt_lin_let = kth_digit n 9;
       opt_lin_beta = kth_digit n 10 }
 
-(* For the moment, we allow by default everything except the type-unsafe 
+(* For the moment, we allow by default everything except the type-unsafe
    optimization [opt_case_idg]. *)
 
 let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024
@@ -392,19 +392,19 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
 
 let optims () = !opt_flag_ref
 
-let _ = declare_bool_option 
-	  {optsync = true; 
+let _ = declare_bool_option
+	  {optsync = true;
 	   optname = "Extraction Optimize";
 	   optkey = SecondaryTable ("Extraction", "Optimize");
-	   optread = (fun () -> !int_flag_ref <> 0); 
+	   optread = (fun () -> !int_flag_ref <> 0);
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let _ = declare_int_option
           { optsync = true;
             optname = "Extraction Flag";
-            optkey = SecondaryTable("Extraction","Flag"); 
-            optread = (fun _ -> Some !int_flag_ref); 
-            optwrite = (function 
+            optkey = SecondaryTable("Extraction","Flag");
+            optread = (fun _ -> Some !int_flag_ref);
+            optwrite = (function
                           | None -> chg_flag 0
                           | Some i -> chg_flag (max i 0))}
 
@@ -417,20 +417,20 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let (extr_lang,_) = 
-  declare_object 
-    {(default_object "Extraction Lang") with  
+let (extr_lang,_) =
+  declare_object
+    {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
        load_function = (fun _ (_,l) -> lang_ref := l);
        export_function = (fun x -> Some x)}
 
-let _ = declare_summary "Extraction Lang" 
+let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
 	    unfreeze_function = ((:=) lang_ref);
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_module = true;
-	    survive_section = true }  
-	  
+	    survive_section = true }
+
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
@@ -443,22 +443,22 @@ let to_inline r = Refset.mem r (fst !inline_table)
 
 let to_keep r = Refset.mem r (snd !inline_table)
 
-let add_inline_entries b l = 
-  let f b = if b then Refset.add else Refset.remove in 
-  let i,k = !inline_table in 
-  inline_table := 
-  (List.fold_right (f b) l i), 
+let add_inline_entries b l =
+  let f b = if b then Refset.add else Refset.remove in
+  let i,k = !inline_table in
+  inline_table :=
+  (List.fold_right (f b) l i),
   (List.fold_right (f (not b)) l k)
 
 (* Registration of operations for rollback. *)
 
 let (inline_extraction,_) =
-  declare_object 
-    {(default_object "Extraction Inline") with 
+  declare_object
+    {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -473,36 +473,36 @@ let _ = declare_summary "Extraction Inline"
 (* Grammar entries. *)
 
 let extraction_inline b l =
-  check_inside_section (); 
-  let refs = List.map Nametab.global l in 
-  List.iter 
-    (fun r -> match r with 
+  check_inside_section ();
+  let refs = List.map Nametab.global l in
+  List.iter
+    (fun r -> match r with
        | ConstRef _ -> ()
-       | _ -> error_constant r) refs; 
+       | _ -> error_constant r) refs;
   Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
 (* Printing part *)
 
-let print_extraction_inline () = 
-  let (i,n)= !inline_table in 
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in 
-  msg 
-    (str "Extraction Inline:" ++ fnl () ++ 
+let print_extraction_inline () =
+  let (i,n)= !inline_table in
+  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+  msg
+    (str "Extraction Inline:" ++ fnl () ++
      Refset.fold
-       (fun r p -> 
+       (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
-     str "Extraction NoInline:" ++ fnl () ++ 
+     str "Extraction NoInline:" ++ fnl () ++
      Refset.fold
-       (fun r p -> 
+       (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
-let (reset_inline,_) = 
+let (reset_inline,_) =
   declare_object
-    {(default_object "Reset Extraction Inline") with  
+    {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table);
        export_function = (fun x -> Some x)}
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
@@ -511,8 +511,8 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 (*s Extract Constant/Inductive. *)
 
 (* UGLY HACK: to be defined in [extraction.ml] *)
-let use_type_scheme_nb_args, register_type_scheme_nb_args = 
-  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r 
+let use_type_scheme_nb_args, register_type_scheme_nb_args =
+  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
 let customs = ref Refmap.empty
 
@@ -520,7 +520,7 @@ let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
 
 let is_custom r = Refmap.mem r !customs
 
-let is_inline_custom r = (is_custom r) && (to_inline r) 
+let is_inline_custom r = (is_custom r) && (to_inline r)
 
 let find_custom r = snd (Refmap.find r !customs)
 
@@ -528,13 +528,13 @@ let find_type_custom r = Refmap.find r !customs
 
 (* Registration of operations for rollback. *)
 
-let (in_customs,_) = 
-  declare_object 
-    {(default_object "ML extractions") with 
+let (in_customs,_) =
+  declare_object
+    {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
@@ -550,17 +550,17 @@ let _ = declare_summary "ML extractions"
 
 let extract_constant_inline inline r ids s =
   check_inside_section ();
-  let g = Nametab.global r in 
-  match g with 
-    | ConstRef kn -> 
-	let env = Global.env () in 
-	let typ = Typeops.type_of_constant env kn in 
+  let g = Nametab.global r in
+  match g with
+    | ConstRef kn ->
+	let env = Global.env () in
+	let typ = Typeops.type_of_constant env kn in
 	let typ = Reduction.whd_betadeltaiota env typ in
-	if Reduction.is_arity env typ 
-	  then begin 
-	    let nargs = use_type_scheme_nb_args env typ in 
+	if Reduction.is_arity env typ
+	  then begin
+	    let nargs = use_type_scheme_nb_args env typ in
 	    if List.length ids <> nargs then error_axiom_scheme g nargs
-	  end; 
+	  end;
 	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,ids,s))
     | _ -> error_constant g
@@ -568,19 +568,19 @@ let extract_constant_inline inline r ids s =
 
 let extract_inductive r (s,l) =
   check_inside_section ();
-  let g = Nametab.global r in 
+  let g = Nametab.global r in
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
 	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if n <> List.length l then error_nb_cons (); 
+	if n <> List.length l then error_nb_cons ();
 	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	list_iter_i
-	  (fun j s -> 
-	     let g = ConstructRef (ip,succ j) in 
+	  (fun j s ->
+	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
-    | _ -> error_inductive g 
+    | _ -> error_inductive g