Permalink
Browse files

The new ocaml compiler (4.00) has a lot of very cool warnings,

especially about unused definitions, unused opens and unused rec
flags.

The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.

(a) "unused rec flags". They cannot change the semantics of the program
    but only allow the inliner to do a better job.

(b) "unused type definitions". I only removed type definitions that were
    given to functors that do not require them. Some type definitions were
    used as documentation to obtain better error messages, but were not
    ascribed to any definition. I superficially mentioned them in one
    arbitrary chosen definition to remove the warning. This is unaesthetic
    but I did not find a better way.

(c) "unused for loop index". The following idiom of imperative
    programming is used at several places: "for i = 1 to n do
    that_side_effect () done".  I replaced "i" with "_i" to remove the
    warning... but, there is a combinator named "Util.repeat" that
    would only cost us a function call while improving readibility.
    Should'nt we use it?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 338608a commit 18ebb3f525a965358d96eab7df493450009517b5 regisgia committed Sep 14, 2012
Showing with 167 additions and 172 deletions.
  1. +2 −2 dev/top_printers.ml
  2. +1 −1 grammar/q_coqast.ml4
  3. +1 −1 interp/notation.ml
  4. +2 −2 interp/notation_ops.ml
  5. +1 −1 kernel/cbytegen.ml
  6. +2 −2 kernel/environ.ml
  7. +1 −1 kernel/mod_subst.ml
  8. +3 −3 kernel/term.ml
  9. +1 −1 kernel/typeops.ml
  10. +2 −2 lib/bigint.ml
  11. +3 −3 lib/dnet.ml
  12. +2 −2 lib/explore.ml
  13. +0 −1 lib/hashcons.ml
  14. +1 −3 lib/pp.ml
  15. +4 −4 lib/profile.ml
  16. +1 −1 lib/rtree.ml
  17. +1 −1 lib/serialize.ml
  18. +1 −1 lib/system.ml
  19. +16 −16 lib/util.ml
  20. +1 −1 lib/xml_utils.ml
  21. +1 −1 library/declaremods.ml
  22. +1 −1 library/impargs.ml
  23. +3 −5 library/nametab.ml
  24. +3 −3 parsing/lexer.ml4
  25. +2 −2 plugins/cc/ccalgo.ml
  26. +1 −1 plugins/cc/cctac.ml
  27. +2 −2 plugins/decl_mode/decl_interp.ml
  28. +3 −3 plugins/decl_mode/decl_proof_instr.ml
  29. +2 −2 plugins/extraction/extraction.ml
  30. +1 −1 plugins/extraction/mlutil.ml
  31. +1 −1 plugins/extraction/ocaml.ml
  32. +1 −1 plugins/extraction/table.ml
  33. +1 −1 plugins/firstorder/formula.ml
  34. +1 −1 plugins/firstorder/sequent.ml
  35. +5 −5 plugins/fourier/fourier.ml
  36. +6 −6 plugins/fourier/fourierR.ml
  37. +1 −1 plugins/funind/functional_principles_types.ml
  38. +2 −2 plugins/funind/indfun.ml
  39. +4 −4 plugins/funind/merge.ml
  40. +1 −1 plugins/micromega/certificate.ml
  41. +4 −4 plugins/micromega/coq_micromega.ml
  42. +3 −3 plugins/micromega/micromega.ml
  43. +2 −2 plugins/micromega/mutils.ml
  44. +1 −1 plugins/micromega/polynomial.ml
  45. +1 −1 plugins/nsatz/ideal.ml
  46. +1 −1 plugins/nsatz/nsatz.ml4
  47. +6 −6 plugins/nsatz/polynom.ml
  48. +6 −6 plugins/omega/coq_omega.ml
  49. +4 −4 plugins/romega/refl_omega.ml
  50. +1 −1 plugins/syntax/ascii_syntax.ml
  51. +1 −1 plugins/xml/acic2Xml.ml4
  52. +1 −1 plugins/xml/xml.ml4
  53. +1 −1 pretyping/cases.ml
  54. +4 −4 pretyping/coercion.ml
  55. +2 −2 pretyping/detyping.ml
  56. +2 −2 pretyping/evarutil.ml
  57. +2 −2 pretyping/inductiveops.ml
  58. +2 −2 pretyping/namegen.ml
  59. +1 −1 pretyping/reductionops.ml
  60. +1 −1 pretyping/tacred.ml
  61. +1 −1 pretyping/term_dnet.ml
  62. +3 −3 pretyping/termops.ml
  63. +1 −1 pretyping/typing.ml
  64. +1 −1 printing/ppconstr.ml
  65. +1 −1 printing/pptactic.ml
  66. +1 −1 proofs/logic.ml
  67. +1 −1 proofs/proof_global.ml
  68. +2 −2 proofs/proofview.ml
  69. +1 −1 proofs/tactic_debug.ml
  70. +1 −1 tactics/inv.ml
  71. +6 −6 tactics/tacinterp.ml
  72. +3 −3 tactics/tactics.ml
  73. +1 −1 tools/coq_makefile.ml
  74. +1 −1 tools/coq_tex.ml4
  75. +1 −1 tools/coqdep.ml
  76. +2 −2 tools/coqdoc/output.ml
  77. +1 −1 toplevel/auto_ind_decl.ml
  78. +2 −2 toplevel/backtrack.ml
  79. +1 −1 toplevel/command.ml
  80. +1 −1 toplevel/indschemes.ml
  81. +1 −1 toplevel/metasyntax.ml
View
@@ -289,7 +289,7 @@ let print_pure_constr csr =
print_string "Fix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
- let rec print_fix () =
+ let print_fix () =
for k = 0 to (Array.length tl) - 1 do
open_vbox 0;
name_display lna.(k); print_string "/";
@@ -303,7 +303,7 @@ let print_pure_constr csr =
print_string "CoFix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
- let rec print_fix () =
+ let print_fix () =
for k = 0 to (Array.length tl) - 1 do
open_vbox 1;
name_display lna.(k); print_cut(); print_string ":";
View
@@ -208,7 +208,7 @@ let rec mlexpr_of_argtype loc = function
<:expr< Genarg.PairArgType $t1$ $t2$ >>
| Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-let rec mlexpr_of_may_eval f = function
+let mlexpr_of_may_eval f = function
| Genredexpr.ConstrEval (r,c) ->
<:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
| Genredexpr.ConstrContext ((loc,id),c) ->
View
@@ -392,7 +392,7 @@ let interp_prim_token =
let interp_prim_token_cases_pattern_expr loc looked_for p =
interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p
-let rec interp_notation loc ntn local_scopes =
+let interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
try find_interpretation ntn (find_notation ntn) scopes
with Not_found ->
View
@@ -110,7 +110,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
| NPatVar n -> GPatVar (loc,(false,n))
| NRef x -> GRef (loc,x)
-let rec glob_constr_of_notation_constr loc x =
+let glob_constr_of_notation_constr loc x =
let rec aux () x =
glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
in aux () x
@@ -544,7 +544,7 @@ let rec match_iterated_binders islambda decls = function
let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
(List.remove_assoc x sigmavar,sigmalist,sigmabinders)
-let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
+let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
let rec aux sigma acc rest =
try
let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
View
@@ -220,7 +220,7 @@ let pos_rel i r sz =
(* non-terminating instruction (branch, raise, return, appterm) *)
(* in front of it. *)
-let rec discard_dead_code cont = cont
+let discard_dead_code cont = cont
(*function
[] -> []
| (Klabel _ | Krestart ) :: _ as cont -> cont
View
@@ -317,7 +317,7 @@ let compile_constant_body = Cbytegen.compile_constant_body
exception Hyp_not_found
-let rec apply_to_hyp (ctxt,vals) id f =
+let apply_to_hyp (ctxt,vals) id f =
let rec aux rtail ctxt vals =
match ctxt, vals with
| (idc,c,ct as d)::ctxt, v::vals ->
@@ -330,7 +330,7 @@ let rec apply_to_hyp (ctxt,vals) id f =
| _, _ -> assert false
in aux [] ctxt vals
-let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
let rec aux ctxt vals =
match ctxt,vals with
| (idc,c,ct as d)::ctxt, v::vals ->
View
@@ -147,7 +147,7 @@ let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver
let mp_of_delta resolve mp =
try Deltamap.find_mp mp resolve with Not_found -> mp
-let rec find_prefix resolve mp =
+let find_prefix resolve mp =
let rec sub_mp = function
| MPdot(mp,l) as mp_sup ->
(try Deltamap.find_mp mp_sup resolve
View
@@ -108,6 +108,8 @@ type ('constr, 'types) kind_of_term =
-rectypes of the Caml compiler to be set *)
type constr = (constr,constr) kind_of_term
+type strategy = types option
+
type existential = existential_key * constr array
type rec_declaration = name array * constr array * constr array
type fixpoint = (int array * int) * rec_declaration
@@ -429,7 +431,7 @@ let rec under_casts f c = match kind_of_term c with
(******************************************************************)
(* flattens application lists throwing casts in-between *)
-let rec collapse_appl c = match kind_of_term c with
+let collapse_appl c = match kind_of_term c with
| App (f,cl) ->
let rec collapse_rec f cl2 =
match kind_of_term (strip_outer_cast f) with
@@ -647,8 +649,6 @@ let rec constr_ord m n=
type types = constr
-type strategy = types option
-
type named_declaration = identifier * constr option * types
type rel_declaration = name * constr option * types
View
@@ -95,7 +95,7 @@ let judge_of_variable env id =
(* Checks if a context of variable can be instantiated by the
variables of the current env *)
(* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
+let check_hyps_inclusion env sign =
Sign.fold_named_context
(fun (id,_,ty1) () ->
let ty2 = named_type id env in
View
@@ -100,7 +100,7 @@ let normalize_neg n =
input: an array with first bloc in [-base;base[ and others in [0;base[
output: a canonical array *)
-let rec normalize n =
+let normalize n =
if Array.length n = 0 then n
else if n.(0) = -1 then normalize_neg n
else if n.(0) = 0 then normalize_pos n
@@ -172,7 +172,7 @@ let sub n m =
if d >= 0 then sub_to (Array.copy n) m d
else let r = neg m in add_to r n (Array.length r - Array.length n)
-let rec mult m n =
+let mult m n =
if m = zero or n = zero then zero else
let l = Array.length m + Array.length n in
let r = Array.create l 0 in
View
@@ -169,13 +169,13 @@ struct
(* Sets with a neutral element for inter *)
module OSet (S:Set.S) = struct
type t = S.t option
- let union s1 s2 = match s1,s2 with
+ let union s1 s2 : t = match s1,s2 with
| (None, _ | _, None) -> None
| Some a, Some b -> Some (S.union a b)
- let inter s1 s2 = match s1,s2 with
+ let inter s1 s2 : t = match s1,s2 with
| (None, a | a, None) -> a
| Some a, Some b -> Some (S.inter a b)
- let is_empty = function
+ let is_empty : t -> bool = function
| None -> false
| Some s -> S.is_empty s
(* optimization hack: Not_found is catched in fold_pattern *)
View
@@ -21,7 +21,7 @@ module Make = functor(S : SearchProblem) -> struct
type position = int list
- let msg_with_position p pp =
+ let msg_with_position (p : position) pp =
let rec pp_rec = function
| [] -> mt ()
| [i] -> int i
@@ -58,7 +58,7 @@ module Make = functor(S : SearchProblem) -> struct
let empty = [],[]
- let push x (h,t) = (x::h,t)
+ let push x (h,t) : _ queue = (x::h,t)
let pop = function
| h, x::t -> x, (h,t)
View
@@ -60,7 +60,6 @@ module Make(X:Comp) =
*)
module Htbl = Hashtbl.Make(
struct type t=X.t
- type u=X.u
let hash=X.hash
let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
end)
View
@@ -71,8 +71,6 @@ type ppcmd = (int*string) ppcmd_token
type std_ppcmds = ppcmd Stream.t
-type 'a ppdirs = 'a ppdir_token Stream.t
-
let is_empty s =
try Stream.empty s; true with Stream.Failure -> false
@@ -175,7 +173,7 @@ let rec eval_ppcmds l =
Stream.of_list (aux l)
(* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
+let escape_string s =
let rec escape_at s i =
if i<0 then s
else if s.[i] == '"' then
View
@@ -221,7 +221,7 @@ let loops = 10000
let time_overhead_A_D () =
let e = create_record () in
let before = get_time () in
- for i=1 to loops do
+ for _i = 1 to loops do
(* This is a copy of profile1 for overhead estimation *)
let dw = dummy_spent_alloc () in
match !dummy_stack with [] -> assert false | p::_ ->
@@ -245,15 +245,15 @@ let time_overhead_A_D () =
done;
let after = get_time () in
let beforeloop = get_time () in
- for i=1 to loops do () done;
+ for _i = 1 to loops do () done;
let afterloop = get_time () in
float_of_int ((after - before) - (afterloop - beforeloop))
/. float_of_int loops
let time_overhead_B_C () =
let dummy_x = 0 in
let before = get_time () in
- for i=1 to loops do
+ for _i = 1 to loops do
try
dummy_last_alloc := get_alloc ();
let _r = dummy_f dummy_x in
@@ -264,7 +264,7 @@ let time_overhead_B_C () =
done;
let after = get_time () in
let beforeloop = get_time () in
- for i=1 to loops do () done;
+ for _i = 1 to loops do () done;
let afterloop = get_time () in
float_of_int ((after - before) - (afterloop - beforeloop))
/. float_of_int loops
View
@@ -101,7 +101,7 @@ let rec map f t = match t with
| Node (a,sons) -> Node (f a, Array.map (map f) sons)
| Rec(j,defs) -> Rec (j, Array.map (map f) defs)
-let rec smartmap f t = match t with
+let smartmap f t = match t with
Param _ -> t
| Node (a,sons) ->
let a'=f a and sons' = Util.array_smartmap (map f) sons in
View
@@ -508,7 +508,7 @@ let pr_option_value = function
| StringValue s -> s
| BoolValue b -> if b then "true" else "false"
-let rec pr_setoptions opts =
+let pr_setoptions opts =
let map (key, v) =
let key = String.concat " " key in
key ^ " := " ^ (pr_option_value v)
View
@@ -58,7 +58,7 @@ let where_in_path ?(warn=true) path filename =
then (lpe,f) :: search rem
else search rem
| [] -> [] in
- let rec check_and_warn l =
+ let check_and_warn l =
match l with
| [] -> raise Not_found
| (lpe, f) :: l' ->
View
@@ -548,7 +548,7 @@ let rec list_fold_left3 f accu l1 l2 l3 =
a1
[]] *)
-let rec list_fold_right_and_left f l hd =
+let list_fold_right_and_left f l hd =
let rec aux tl = function
| [] -> hd
| a::l -> let hd = aux (a::tl) l in f hd a tl
@@ -636,7 +636,7 @@ let list_uniquize l =
| [] -> List.rev acc
in aux [] l
-let rec list_distinct l =
+let list_distinct l =
let visited = Hashtbl.create 23 in
let rec loop = function
| h::t ->
@@ -774,7 +774,7 @@ let rec list_skipn n l = match n,l with
| _, [] -> failwith "list_skipn"
| n, _::l -> list_skipn (pred n) l
-let rec list_skipn_at_least n l =
+let list_skipn_at_least n l =
try list_skipn n l with Failure _ -> []
let list_prefix_of prefl l =
@@ -852,7 +852,7 @@ let list_union_map f l acc =
[list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
and so on if there are more elements in the lists. *)
-let rec list_cartesian op l1 l2 =
+let list_cartesian op l1 l2 =
list_map_append (fun x -> List.map (op x) l2) l1
(* [list_cartesians] is an n-ary cartesian product: it iterates
@@ -874,12 +874,12 @@ let rec list_combine3 x y z =
(* Keep only those products that do not return None *)
-let rec list_cartesian_filter op l1 l2 =
+let list_cartesian_filter op l1 l2 =
list_map_append (fun x -> list_map_filter (op x) l2) l1
(* Keep only those products that do not return None *)
-let rec list_cartesians_filter op init ll =
+let list_cartesians_filter op init ll =
List.fold_right (list_cartesian_filter op) ll [init]
(* Drop the last element of a list *)
@@ -1217,15 +1217,6 @@ let array_filter_along f filter v =
let array_filter_with filter v =
Array.of_list (list_filter_with filter (Array.to_list v))
-(* Stream *)
-
-let stream_nth n st =
- try List.nth (Stream.npeek (n+1) st) n
- with Failure _ -> raise Stream.Failure
-
-let stream_njunk n st =
- for i = 1 to n do Stream.junk st done
-
(* Matrices *)
let matrix_transpose mat =
@@ -1247,7 +1238,7 @@ let iterate f =
iterate_f
let repeat n f x =
- for i = 1 to n do f x done
+ let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n
let iterate_for a b f x =
let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
@@ -1258,6 +1249,15 @@ let app_opt f x =
| Some f -> f x
| None -> x
+(* Stream *)
+
+let stream_nth n st =
+ try List.nth (Stream.npeek (n+1) st) n
+ with Failure _ -> raise Stream.Failure
+
+let stream_njunk n st =
+ repeat n Stream.junk st
+
(* Delayed computations *)
type 'a delayed = unit -> 'a
View
@@ -116,7 +116,7 @@ let buffer_attr (n,v) =
done;
Buffer.add_char tmp '"'
-let rec print_attr chan (n, v) =
+let print_attr chan (n, v) =
Printf.fprintf chan " %s=\"" n;
let l = String.length v in
for p = 0 to l-1 do
View
@@ -1043,7 +1043,7 @@ let iter_all_segments f =
List.iter apply_obj objects)
!modtab_objects
in
- let rec apply_node = function
+ let apply_node = function
| sp, Leaf o -> f sp o
| _ -> ()
in
View
@@ -695,7 +695,7 @@ let rec select_impargs_size n = function
| (LessArgsThan p, impls)::l ->
if n <= p then impls else select_impargs_size n l
-let rec select_stronger_impargs = function
+let select_stronger_impargs = function
| [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
| (_,impls)::_ -> impls
Oops, something went wrong.

0 comments on commit 18ebb3f

Please sign in to comment.