diff options
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r-- | tools/coqdep_common.ml | 445 |
1 files changed, 445 insertions, 0 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml new file mode 100644 index 00000000..b71a47d0 --- /dev/null +++ b/tools/coqdep_common.ml @@ -0,0 +1,445 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: coqdep_common.ml 11984 2009-03-16 13:41:49Z letouzey $ *) + +open Printf +open Coqdep_lexer +open Unix + +(** [coqdep_boot] is a stripped-down version of [coqdep], whose + behavior is the one of [coqdep -boot]. Its only dependencies + are [Coqdep_lexer] and [Unix], and it should stay so. + If it need someday some additional information, pass it via + options (see for instance [option_natdynlk] below). +*) + +let stderr = Pervasives.stderr +let stdout = Pervasives.stdout + +let option_c = ref false +let option_noglob = ref false +let option_slash = ref false +let option_natdynlk = ref true + +let norecdir_list = ref ([]:string list) + +let suffixe = ref ".vo" + +type dir = string option + +(* filename for printing *) +let (//) s1 s2 = + if !option_slash then s1^"/"^s2 else Filename.concat s1 s2 + +(** [get_extension f l] checks whether [f] has one of the extensions + listed in [l]. It returns [f] without its extension, alongside with + the extension. When no extension match, [(f,"")] is returned *) + +let rec get_extension f = function + | [] -> (f, "") + | s :: _ when Filename.check_suffix f s -> (Filename.chop_suffix f s, s) + | _ :: l -> get_extension f l + +(** [basename_noext] removes both the directory part and the extension + (if necessary) of a filename *) + +let basename_noext filename = + let fn = Filename.basename filename in + try Filename.chop_extension fn with _ -> fn + +(** ML Files specified on the command line. In the entries: + - the first string is the basename of the file, without extension nor + directory part + - the second string of [mlAccu] is the extension (either .ml or .ml4) + - the [dir] part is the directory, with None used as the current directory +*) + +let mlAccu = ref ([] : (string * string * dir) list) +and mliAccu = ref ([] : (string * dir) list) +and mllibAccu = ref ([] : (string * dir) list) + +(** Coq files specifies on the command line: + - first string is the full filename, with only its extension removed + - second string is the absolute version of the previous (via getcwd) +*) + +let vAccu = ref ([] : (string * string) list) + +(** Queue operations *) + +let addQueue q v = q := v :: !q + +let safe_hash_add clq q (k,v) = + try + let v2 = Hashtbl.find q k in + if v<>v2 then + let rec add_clash = function + (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl + | cl::cltl -> cl::add_clash cltl + | [] -> [(k,[v;v2])] in + clq := add_clash !clq; + (* overwrite previous bindings, as coqc does *) + Hashtbl.add q k v + with Not_found -> Hashtbl.add q k v + +(** Files found in the loadpaths. + For the ML files, the string is the basename without extension. + To allow ML source filename to be potentially capitalized, + we perform a double search. +*) + +let mkknown () = + let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in + let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s + and iter f = Hashtbl.iter f h + and search x = + try Some (Hashtbl.find h (String.uncapitalize x)) + with Not_found -> + try Some (Hashtbl.find h (String.capitalize x)) + 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_mllib_known, _, search_mllib_known = mkknown () + +let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t) +let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) + +let clash_v = ref ([]: (string list * string list) list) + +let warning_module_notfound f s = + eprintf "*** Warning: in file %s, library " f; + eprintf "%s.v is required and has not been found in loadpath!\n" + (String.concat "." s); + flush stderr + +let warning_notfound f s = + eprintf "*** Warning: in file %s, the file " f; + eprintf "%s.v is required and has not been found !\n" s; + flush stderr + +let warning_declare f s = + eprintf "*** Warning: in file %s, declared ML module " f; + eprintf "%s has not been found !\n" s; + flush stderr + +let warning_clash file dir = + match List.assoc dir !clash_v with + (f1::f2::fl) -> + let f = Filename.basename f1 in + let d1 = Filename.dirname f1 in + let d2 = Filename.dirname f2 in + let dl = List.map Filename.dirname (List.rev fl) in + eprintf + "*** Warning: in file %s, \n required library %s is ambiguous!\n (found %s.v in " + file (String.concat "." dir) f; + List.iter (fun s -> eprintf "%s, " s) dl; + eprintf "%s and %s; used the latter)\n" d2 d1 + | _ -> assert false + +let safe_assoc verbose file k = + if verbose && List.mem_assoc k !clash_v then warning_clash file k; + Hashtbl.find vKnown k + +let absolute_dir dir = + let current = Sys.getcwd () in + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' + +let absolute_file_name basename odir = + let dir = match odir with Some dir -> dir | None -> "." in + absolute_dir dir // basename + +let file_name s = function + | None -> s + | Some "." -> s + | Some d -> d // s + +let depend_ML str = + match search_mli_known str, search_ml_known str with + | Some mlidir, Some mldir -> + let mlifile = file_name str mlidir + and mlfile = file_name str mldir in + (" "^mlifile^".cmi"," "^mlfile^".cmx") + | None, Some mldir -> + let mlfile = file_name str mldir in + (" "^mlfile^".cmo"," "^mlfile^".cmx") + | Some mlidir, None -> + let mlifile = file_name str mlidir in + (" "^mlifile^".cmi"," "^mlifile^".cmi") + | None, None -> "", "" + +let traite_fichier_ML md ext = + try + let chan = open_in (md ^ ext) in + let buf = Lexing.from_channel chan in + let deja_vu = ref [md] in + let a_faire = ref "" in + let a_faire_opt = ref "" in + begin try + while true do + let (Use_module str) = caml_action buf in + if List.mem str !deja_vu then + () + else begin + addQueue deja_vu str; + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt + end + done + with Fin_fichier -> () + end; + close_in chan; + (!a_faire, !a_faire_opt) + with Sys_error _ -> ("","") + +let traite_fichier_mllib md ext = + try + let chan = open_in (md ^ ext) in + let list = mllib_list (Lexing.from_channel chan) in + let a_faire = ref "" in + let a_faire_opt = ref "" in + List.iter + (fun str -> match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire := !a_faire^" "^file^".cmo"; + a_faire_opt := !a_faire_opt^" "^file^".cmx" + | None -> ()) list; + (!a_faire, !a_faire_opt) + with Sys_error _ -> ("","") + + +(* Makefile's escaping rules are awful: $ is escaped by doubling and + other special characters are escaped by backslash prefixing while + backslashes themselves must be escaped only if part of a sequence + followed by a special character (i.e. in case of ambiguity with a + use of it as escaping character). Moreover (even if not crucial) + it is apparently not possible to directly escape ';' and leading '\t'. *) + +let escape = + let s' = Buffer.create 10 in + fun s -> + Buffer.clear s'; + for i = 0 to String.length s - 1 do + let c = s.[i] in + if c = ' ' or c = '#' or c = ':' (* separators and comments *) + or c = '%' (* pattern *) + or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) + or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + then begin + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; + end; + if c = '$' then Buffer.add_char s' '$'; + Buffer.add_char s' c + done; + Buffer.contents s' + +let canonize f = + let f' = absolute_dir (Filename.dirname f) // Filename.basename f in + match List.filter (fun (_,full) -> f' = full) !vAccu with + | (f,_) :: _ -> escape f + | _ -> escape f + +let traite_fichier_Coq verbose f = + try + let chan = open_in f in + let buf = Lexing.from_channel chan in + let deja_vu_v = ref ([]: string list list) + and deja_vu_ml = ref ([] : string list) in + try + while true do + let tok = coq_action buf in + match tok with + | Require strl -> + List.iter (fun str -> + if not (List.mem str !deja_vu_v) then begin + addQueue deja_vu_v str; + try + let file_str = safe_assoc verbose f str in + printf " %s%s" (canonize file_str) !suffixe + with Not_found -> + if verbose && not (Hashtbl.mem coqlibKnown str) then + warning_module_notfound f str + end) strl + | RequireString s -> + let str = Filename.basename s in + if not (List.mem [str] !deja_vu_v) then begin + addQueue deja_vu_v [str]; + try + let file_str = Hashtbl.find vKnown [str] in + printf " %s%s" (canonize file_str) !suffixe + with Not_found -> + if not (Hashtbl.mem coqlibKnown [str]) then + warning_notfound f s + end + | Declare sl -> + let declare suff dir s = + let base = file_name s dir in + let opt = if !option_natdynlk then " "^base^".cmxs" else "" in + printf " %s%s%s" (escape base) suff opt + in + let decl str = + let s = basename_noext str in + if not (List.mem s !deja_vu_ml) then begin + addQueue deja_vu_ml s; + match search_mllib_known s with + | Some mldir -> declare ".cma" mldir s + | None -> + match search_ml_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> warning_declare f str + end + in List.iter decl sl + | Load str -> + let str = Filename.basename str in + if not (List.mem [str] !deja_vu_v) then begin + addQueue deja_vu_v [str]; + try + let file_str = Hashtbl.find vKnown [str] in + printf " %s.v" (canonize file_str) + with Not_found -> () + end + done + with Fin_fichier -> (); + close_in chan + with Sys_error _ -> () + + +let mL_dependencies () = + List.iter + (fun (name,ext,dirname) -> + let fullname = file_name name dirname in + let (dep,dep_opt) = traite_fichier_ML fullname ext in + let intf = match search_mli_known name with + | None -> "" + | Some mldir -> " "^(file_name name mldir)^".cmi" + in + let efullname = escape fullname in + printf "%s.cmo:%s%s\n" efullname dep intf; + printf "%s.cmx:%s%s\n" efullname dep_opt intf; + flush stdout) + (List.rev !mlAccu); + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let (dep,_) = traite_fichier_ML fullname ".mli" in + printf "%s.cmi:%s\n" (escape fullname) dep; + flush stdout) + (List.rev !mliAccu); + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in + let efullname = escape fullname in + printf "%s.cma:%s\n" efullname dep; + printf "%s.cmxa %s.cmxs:%s\n" efullname efullname dep_opt; + flush stdout) + (List.rev !mllibAccu) + +let coq_dependencies () = + List.iter + (fun (name,_) -> + let ename = escape name in + let glob = if !option_noglob then "" else " "^ename^".glob" in + printf "%s%s%s: %s.v" ename !suffixe glob ename; + traite_fichier_Coq true (name ^ ".v"); + printf "\n"; + flush stdout) + (List.rev !vAccu) + +let rec suffixes = function + | [] -> assert false + | [name] -> [[name]] + | dir::suffix as l -> l::suffixes suffix + +let add_known phys_dir log_dir f = + match get_extension f [".v";".ml";".mli";".ml4";".mllib"] with + | (basename,".v") -> + let name = log_dir@[basename] in + let file = phys_dir//basename in + let paths = suffixes name in + List.iter + (fun n -> safe_hash_add clash_v vKnown (n,file)) paths + | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) + | (basename,".mli") -> add_mli_known basename (Some phys_dir) + | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) + | _ -> () + +(* Visits all the directories under [dir], including [dir], + or just [dir] if [recur=false] *) + +let rec add_directory recur add_file phys_dir log_dir = + let dirh = opendir phys_dir in + try + while true do + let f = readdir dirh in + (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) + if f.[0] <> '.' && f.[0] <> '_' then + let phys_f = if phys_dir = "." then f else phys_dir//f in + match try (stat phys_f).st_kind with _ -> S_BLK with + | S_DIR when recur -> + if List.mem phys_f !norecdir_list then () + else + let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in + add_directory recur add_file phys_f log_dir' + | S_REG -> add_file phys_dir log_dir f + | _ -> () + done + with End_of_file -> closedir dirh + +let add_dir add_file phys_dir log_dir = + try add_directory false add_file phys_dir log_dir with Unix_error _ -> () + +let add_rec_dir add_file phys_dir log_dir = + handle_unix_error (add_directory true add_file phys_dir) log_dir + +let rec treat_file old_dirname old_name = + let name = Filename.basename old_name + and new_dirname = Filename.dirname old_name in + let dirname = + match (old_dirname,new_dirname) with + | (d, ".") -> d + | (None,d) -> Some d + | (Some d1,d2) -> Some (d1//d2) + in + let complete_name = file_name name dirname in + match try (stat complete_name).st_kind with _ -> S_BLK with + | S_DIR -> + (if name.[0] <> '.' then + let dir=opendir complete_name in + let newdirname = + match dirname with + | None -> name + | Some d -> d//name + in + try + while true do treat_file (Some newdirname) (readdir dir) done + with End_of_file -> closedir dir) + | S_REG -> + (match get_extension name [".v";".ml";".mli";".ml4";".mllib"] with + | (base,".v") -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,".mli") -> addQueue mliAccu (base,dirname) + | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | _ -> ()) + | _ -> () |