diff options
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r-- | tools/coqdep.ml | 64 |
1 files changed, 29 insertions, 35 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e..110d3060 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,14 +36,6 @@ let warning_mult suf iter = in iter check -let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> - let name = log_dir@[basename] in - let paths = if recur then suffixes name else [name] in - List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths - | _ -> () - let sort () = let seen = Hashtbl.create 97 in let rec loop file = @@ -55,13 +47,13 @@ let sort () = try while true do match coq_action lb with - | Require sl -> + | Require (from, sl) -> List.iter (fun s -> - try loop (Hashtbl.find vKnown s) - with Not_found -> ()) + match search_v_known ?from s with + | None -> () + | Some f -> loop f) sl - | RequireString s -> loop s | _ -> () done with Fin_fichier -> @@ -297,18 +289,24 @@ struct module DAG = DAG(struct type t = string let compare = compare end) (** TODO: we should share this code with Coqdep_common *) +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let treat_coq_file chan = let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: string list list) - and deja_vu_ml = ref ([] : string list) in - let mark_v_done acc str = - let seen = List.mem str !deja_vu_v in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in + let mark_v_done from acc str = + let seen = VCache.mem (from, str) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v str in - try - let file_str = Hashtbl.find vKnown str in - (canonize file_str, !suffixe) :: acc - with Not_found -> acc + let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in + match search_v_known ?from str with + | None -> acc + | Some file_str -> (canonize file_str, !suffixe) :: acc else acc in let rec loop acc = @@ -317,11 +315,8 @@ let treat_coq_file chan = | None -> acc | Some action -> let acc = match action with - | Require strl -> - List.fold_left mark_v_done acc strl - | RequireString s -> - let str = Filename.basename s in - mark_v_done acc [str] + | Require (from, strl) -> + List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = let base = file_name s dir in @@ -330,8 +325,8 @@ let treat_coq_file chan = in let decl acc str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then - let () = addQueue deja_vu_ml s in + if not (StrSet.mem s !deja_vu_ml) then + let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with | Some mldir -> (declare ".cma" mldir s) :: acc | None -> @@ -343,13 +338,12 @@ let treat_coq_file chan = List.fold_left decl acc sl | Load str -> let str = Filename.basename str in - let seen = List.mem [str] !deja_vu_v in + let seen = VCache.mem (None, [str]) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v [str] in - try - let file_str = Hashtbl.find vKnown [str] in - (canonize file_str, ".v") :: acc - with Not_found -> acc + let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in + match search_v_known [str] with + | None -> acc + | Some file_str -> (canonize file_str, ".v") :: acc else acc | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) in @@ -461,7 +455,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () |