From c9d76e9cd6953625778bf4b173430d674e15f05d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Feb 2020 22:39:46 +0100 Subject: [coqdep] mli cleanup, remove unused functions --- tools/coqdep.ml | 46 +--------------------------------------------- tools/coqdep_common.ml | 31 +++++++++++++++++++++++++++++-- tools/coqdep_common.mli | 31 ++++++++++--------------------- 3 files changed, 40 insertions(+), 68 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 745cf950b5..950c784325 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,9 +9,8 @@ (************************************************************************) open Format -open Coqdep_lexer -open Coqdep_common open Minisys +open Coqdep_common (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -29,47 +28,6 @@ open Minisys let option_sort = ref false -let warning_mult suf iter = - let tab = Hashtbl.create 151 in - let check f d = - begin try - let d' = Hashtbl.find tab f in - if (Filename.dirname (file_name f d)) - <> (Filename.dirname (file_name f d')) then begin - coqdep_warning "the file %s is defined twice!" (f ^ suf) - end - with Not_found -> () end; - Hashtbl.add tab f d - in - iter check - -let sort () = - let seen = Hashtbl.create 97 in - let rec loop file = - let file = canonize file in - if not (Hashtbl.mem seen file) then begin - Hashtbl.add seen file (); - let cin = open_in (file ^ ".v") in - let lb = Lexing.from_channel cin in - try - while true do - match coq_action lb with - | Require (from, sl) -> - List.iter - (fun s -> - match search_v_known ?from s with - | None -> () - | Some f -> loop f) - sl - | _ -> () - done - with Fin_fichier -> - close_in cin; - printf "%s%s " file !suffixe - end - in - List.iter (fun (name,_) -> loop name) !vAccu - let usage () = eprintf " usage: coqdep [options] +\n"; eprintf " options:\n"; @@ -159,8 +117,6 @@ let coqdep () = List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; if !option_c then mL_dependencies (); coq_dependencies (); diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index bd72a52adf..5ece595f13 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -125,8 +125,8 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, iter_ml_known, search_ml_known = mkknown () -let add_mli_known, iter_mli_known, search_mli_known = mkknown () +let add_ml_known, _, search_ml_known = mkknown () +let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -616,3 +616,30 @@ let rec treat_file old_dirname old_name = | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> ()) | _ -> () + +let sort () = + let seen = Hashtbl.create 97 in + let rec loop file = + let file = canonize file in + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + let cin = open_in (file ^ ".v") in + let lb = Lexing.from_channel cin in + try + while true do + match coq_action lb with + | Require (from, sl) -> + List.iter + (fun s -> + match search_v_known ?from s with + | None -> () + | Some f -> loop f) + sl + | _ -> () + done + with Fin_fichier -> + close_in cin; + printf "%s%s " file !suffixe + end + in + List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 96266b8e36..1820db4a1e 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -20,44 +20,34 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a twice.*) val find_dir_logpath: string -> string list +(** Options *) val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref - val write_vos : bool ref -(** output vos and vok dependencies *) +val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable - val option_dynlink : dynlink ref + val norec_dirs : StrSet.t ref -val suffixe : string ref + type dir = string option -val get_extension : string -> string list -> string * string -val basename_noext : string -> string +val treat_file : dir -> string -> unit + +(** ML-related manipulation *) val mlAccu : (string * string * dir) list ref val mliAccu : (string * dir) list ref val mllibAccu : (string * dir) list ref -val vAccu : (string * string) list ref -val addQueue : 'a list ref -> 'a -> unit val add_ml_known : string -> dir -> string -> unit -val iter_ml_known : (string -> dir -> unit) -> unit -val search_ml_known : string -> dir option val add_mli_known : string -> dir -> string -> unit -val iter_mli_known : (string -> dir -> unit) -> unit -val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit -val search_mllib_known : string -> dir option -val search_v_known : ?from:string list -> string list -> string option -val file_name : string -> string option -> string -val escape : string -> string -val canonize : string -> string val mL_dependencies : unit -> unit + val coq_dependencies : unit -> unit -val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit -val add_caml_known : string -> string list -> string -> unit + val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used @@ -73,5 +63,4 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val treat_file : dir -> string -> unit -val error_cannot_parse : string -> int * int -> 'a +val sort : unit -> unit -- cgit v1.2.3