From: Enrico Tassi Date: Tue, 20 Sep 2005 14:16:34 +0000 (+0000) Subject: fixed matitadep: now it should consider ALL depndencies X-Git-Tag: LAST_BEFORE_NEW~84 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b6a37cbbfe7d1535080be0e728dd8aa3c112880;p=helm.git fixed matitadep: now it should consider ALL depndencies --- diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 70240068f..9fafa4907 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -38,26 +38,18 @@ let usage = module GA = GrafiteAst module U = UriManager -let deps = Hashtbl.create (Array.length Sys.argv) -let baseuris = ref [] -let aliases = Hashtbl.create (Array.length Sys.argv) - -(* -let uri_of_alias = function - | Ident_alias (_, uri) - | Symbol_alias (_, _, uri) - | Number_alias (_, uri) -> uri -*) +(* all are maps from "file" to "something" *) +let include_deps = Hashtbl.create (Array.length Sys.argv) +let baseuri_of = Hashtbl.create (Array.length Sys.argv) +let uri_deps = Hashtbl.create (Array.length Sys.argv) let buri alias = U.buri_of_uri (U.uri_of_string alias) -let resolve alias = +let resolve alias current_buri= let buri = buri alias in - if List.exists (fun u -> u = buri) !baseuris then Some buri else None + if buri <> current_buri then Some buri else None - (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) - let find path = let rec aux = function | [] -> close_in (open_in path); path @@ -75,96 +67,52 @@ let find path = raise exc ;; -(* note, this function works cause moo files are transitively closed *) -let process_notation_of_file file = - let ic = open_in file in - let istream = Stream.of_channel ic in - let notation_ids = ref [] in - try - while true do - match GrafiteParser.parse_statement istream with - | GA.Executable (_, GA.Command (_, notation)) -> - let stm, ids = CicNotation.process_notation notation in - notation_ids := ids @ !notation_ids - | _ -> () - done; [] - with - | End_of_file -> close_in ic; !notation_ids - | CicNotationParser.Parse_error _ as exn -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exn); - raise exn - let main () = - MatitaInit.initialize_notation (); + MatitaInit.load_config_only (); let files = ref [] in Arg.parse arg_spec (add_l files) usage; List.iter (fun file -> let ic = open_in file in let istream = Stream.of_channel ic in - let notation_ids = ref [] in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - (match stm with - | GA.Executable (_, GA.Command (_, notation)) -> - let stm, ids = CicNotation.process_notation notation in - notation_ids := ids @ !notation_ids - | _ -> ()); - match stm with - | GA.Executable (_, GA.Command (_, GA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuris := uri :: !baseuris - | GA.Executable (_, GA.Command - (_, GA.Alias (_, GA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | GA.Executable (_, GA.Command (_, GA.Include (_, path))) -> - (* maybe to process coq.ma is useles since it contains only - * interpretations... no idea if notations will be added later *) - let moo_file = - MatitaMisc.obj_file_of_script ( - if path <> "coq.ma" then find path else path) - in - let ids = process_notation_of_file moo_file in - notation_ids := ids @ !notation_ids; - (try - Hashtbl.add deps file moo_file - with - Sys_error _ -> - MatitaLog.error - ("In file " ^ file ^ " unable to include " ^ path) - ) - | _ -> () - with - CicNotationParser.Parse_error _ as exn -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exn); - () - done - with - | End_of_file -> close_in ic); - Hashtbl.iter - (fun file alias -> - let dep = resolve alias in - match dep with - | None -> () - | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u)) - aliases; - (* remove notation ids *) - List.iter CicNotation.remove_notation !notation_ids; - ) !files; + let dependencies = GrafiteParser.parse_dependencies istream in + close_in ic; + List.iter + (function + | GrafiteAst.UriDep uri -> + let uri = UriManager.string_of_uri uri in + Hashtbl.add uri_deps file uri + | GrafiteAst.BaseuriDep uri -> + let uri = MatitaMisc.strip_trailing_slash uri in + Hashtbl.add baseuri_of file uri + | GrafiteAst.IncludeDep path -> + try + let ma_file = if path <> "coq.ma" then find path else path in + let moo_file = MatitaMisc.obj_file_of_script ma_file in + Hashtbl.add include_deps file moo_file + with Sys_error _ -> + MatitaLog.warn + ("Unable to find " ^ path ^ " that is included in " ^ file)) + dependencies) + !files; + Hashtbl.iter + (fun file alias -> + let dep = resolve alias (Hashtbl.find baseuri_of file) in + match dep with + | None -> () + | Some u -> + Hashtbl.add include_deps file (MatitaMisc.obj_file_of_baseuri u)) + uri_deps; List.iter (fun file -> - let deps = Hashtbl.find_all deps file in + let deps = Hashtbl.find_all include_deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in let deps = file :: deps in let moo = MatitaMisc.obj_file_of_script file in Printf.printf "%s: %s\n" moo (String.concat " " deps); - Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo - ) !files + Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) + !files ;; let _ =