X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=5b22cb70b9cbe9abce580c4d254a0344b009a3d4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=88cac82807ff10953bb6549372b70c5a49b94de2;hpb=efdb0db81ef2594a2aced0310997ef0d74462254;p=helm.git diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 88cac8280..5b22cb70b 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -23,107 +23,77 @@ * http://helm.cs.unibo.it/ *) -let paths_to_search_in = ref [];; - -let add_l l = fun s -> l := s :: !l ;; - -let arg_spec = [ - "-I", Arg.String (add_l paths_to_search_in), - " Adds path to the list of searched paths for the include command"; -] -let usage = - Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:" - BuildTimeConf.version - -module TA = GrafiteAst +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 -*) - -let buri alias = - U.buri_of_uri (U.uri_of_string alias) - -let resolve alias = - let buri = buri alias in - if List.exists (fun u -> u = buri) !baseuris 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 - | p :: tl -> - try - close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path - with Sys_error _ -> aux tl - in - let paths = !paths_to_search_in in - try - aux paths - with Sys_error _ as exc -> - MatitaLog.error ("Unable to read " ^ path); - MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); - raise exc -;; - let main () = - Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; - let files = ref [] in - Arg.parse arg_spec (add_l files) usage; + (* all are maps from "file" to "something" *) + let include_deps = Hashtbl.create (Array.length Sys.argv) in + let baseuri_of = Hashtbl.create (Array.length Sys.argv) in + let uri_deps = Hashtbl.create (Array.length Sys.argv) in + let buri alias = U.buri_of_uri (U.uri_of_string alias) in + let resolve alias current_buri = + let buri = buri alias in + if buri <> current_buri then Some buri else None + in + let find path = + let rec aux = function + | [] -> close_in (open_in path); path + | p :: tl -> + try + close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path + with Sys_error _ -> aux tl + in + let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in + try + aux paths + with Sys_error _ as exc -> + MatitaLog.error ("Unable to read " ^ path); + MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + raise exc + in + MatitaInit.load_configuration_file (); + MatitaInit.parse_cmdline (); List.iter (fun file -> let ic = open_in file in - let istream = Stream.of_channel ic in - (try - while true do - try - match GrafiteParser.parse_statement istream with - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuris := uri :: !baseuris - | TA.Executable (_, TA.Command - (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find 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 - ) !files; + let istream = Ulexing.from_utf8_channel ic in + 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 = MatitacleanLib.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) + (Helm_registry.get_list Helm_registry.string "matita.args"); + 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 = HExtlib.list_uniq deps in let deps = file :: deps in - let moo = MatitaMisc.obj_file_of_script file in + let moo = MatitacleanLib.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 -;; - -let _ = - main () + Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) + (Helm_registry.get_list Helm_registry.string "matita.args") +