X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=70240068fe71624063bac38e4ffdaf33bf652d0d;hb=51d82e0a8a4d4ed86d2646edb2654e565ac34a82;hp=c1ccce7808c9cdacc1c79baa21bcb96460efc562;hpb=ebc063e65d908c9f35619c92454dbbe76bdabd40;p=helm.git diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index c1ccce780..70240068f 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -1,8 +1,45 @@ -module TA = TacticAst +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * 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 GA = GrafiteAst module U = UriManager let deps = Hashtbl.create (Array.length Sys.argv) -let baseuri = ref [] +let baseuris = ref [] let aliases = Hashtbl.create (Array.length Sys.argv) (* @@ -16,54 +53,119 @@ let buri alias = U.buri_of_uri (U.uri_of_string alias) let resolve alias = - try - Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri)) - with - | Not_found -> None + 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 +;; + +(* 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 () = - for i = 1 to Array.length Sys.argv - 1 do - let file = Sys.argv.(i) in + MatitaInit.initialize_notation (); + let files = ref [] in + Arg.parse arg_spec (add_l files) usage; + List.iter + (fun file -> let ic = open_in file in - let stms = - try - CicTextualParser2.parse_statements (Stream.of_channel ic) - with - (CicTextualParser2.Parse_error _) as exc -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exc); - exit 1 - in - close_in ic; - List.iter - (function - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuri := (uri, file) :: !baseuri - | TA.Executable (_, TA.Command - (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | _ -> ()) - stms; + 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 d -> Hashtbl.add deps file d) + | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u)) aliases; - done; - for i = 1 to Array.length Sys.argv - 1 do - let file = Sys.argv.(i) in + (* remove notation ids *) + List.iter CicNotation.remove_notation !notation_ids; + ) !files; + List.iter + (fun file -> let deps = Hashtbl.find_all deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in let deps = file :: deps in - Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) - (String.concat " " deps) - done + 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 +;; - -let _ = main () +let _ = + main ()