From: Enrico Tassi Date: Sun, 6 Jan 2008 15:48:38 +0000 (+0000) Subject: irediced usage of matita.includes, that is now set by X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4a62bde42e3655a7829b9281d9b9057dc32c0471 irediced usage of matita.includes, that is now set by matitaInit and should be read once at the beginning of every main, removed rottener --- diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 07ca6a6f1..c948272ef 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -692,7 +692,7 @@ EXTEND fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let _root, buri, fullpath = + let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let status = diff --git a/components/grafite_parser/grafiteWalker.ml b/components/grafite_parser/grafiteWalker.ml index 742532113..7e722bccf 100644 --- a/components/grafite_parser/grafiteWalker.ml +++ b/components/grafite_parser/grafiteWalker.ml @@ -34,10 +34,8 @@ let get_loc = loc let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) - ~fname test + ~fname ~include_paths test = - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in let content = HExtlib.input_file fname in let lexbuf = Ulexing.from_utf8_string content in let parse_fun status = @@ -61,7 +59,7 @@ let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) let ma_extension_test fname = Filename.check_suffix fname ".ma" let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) - ~dirname test + ~dirname ~include_paths test = let files = HExtlib.find ~test:fname_test dirname in List.flatten @@ -72,6 +70,6 @@ let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) | None -> None | Some f -> Some (fun s -> f (fname, s)) in List.map (fun raw -> fname, raw) - (grep_statement ?status ?callback ~fname test)) + (grep_statement ?status ?callback ~fname ~include_paths test)) files) diff --git a/components/grafite_parser/grafiteWalker.mli b/components/grafite_parser/grafiteWalker.mli index b4ca6f0d7..c9df8ab48 100644 --- a/components/grafite_parser/grafiteWalker.mli +++ b/components/grafite_parser/grafiteWalker.mli @@ -33,7 +33,9 @@ type statement_test = val grep_statement: ?status: LexiconEngine.status -> ?callback: (string -> unit) -> - fname:string -> statement_test -> + fname:string -> + include_paths: string list -> + statement_test -> string list (** As above, but act on all file (recursively) located under directory @@ -43,6 +45,8 @@ val grep_statement: val rgrep_statement: ?status: LexiconEngine.status -> ?callback: (string * string -> unit) -> - ?fname_test:(string -> bool) -> dirname:string -> statement_test -> + ?fname_test:(string -> bool) -> dirname:string -> + include_paths: string list -> + statement_test -> (string * string) list diff --git a/components/library/librarian.ml b/components/library/librarian.ml index 417035a81..591813676 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -56,7 +56,7 @@ let find_root_for ~include_paths file = HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path ;; - + let baseuri_of_script ?(include_paths=[]) file = let root, buri, path = find_root_for ~include_paths file in let path = HExtlib.normalize_path path in @@ -75,10 +75,12 @@ let baseuri_of_script ?(include_paths=[]) file = try Filename.chop_extension name with Invalid_argument "Filename.chop_extension" -> name in + let extra = String.concat "/" extra_buri in root, remove_trailing_slash (HExtlib.normalize_path - (buri ^ "/" ^ chop (String.concat "/" extra_buri))), - path + (buri ^ "/" ^ chop extra)), + path, + extra ;; let find_roots_in_dir dir = diff --git a/components/library/librarian.mli b/components/library/librarian.mli index 5280dbbf8..90b7ef168 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -4,11 +4,13 @@ val find_root: string -> string val parse_root: string -> (string*string) list -(* baseuri_of_script ?(inc:REG[matita.includes]) fname -> root, buri, fullpath +(* baseuri_of_script ?(inc:REG[matita.includes]) fname + * -> + * root, buri, fullpath, rootrelativepath * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, * /home/pippo/devel/a.ma *) val baseuri_of_script: - ?include_paths:string list -> string -> string * string * string + ?include_paths:string list -> string -> string * string * string * string (* finds all the roots files in the specified dir *) val find_roots_in_dir: string -> string list diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 255a0dde1..d5cad512a 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -695,19 +695,17 @@ class script ~(source_view: GSourceView.source_view) let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses baseuri = - (* these include_paths are used only to load the initial notation *) - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in let lexicon_status = - CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script in + CicNotation2.load_notation ~include_paths:[] + BuildTimeConf.core_notation_script + in let grafite_status = GrafiteSync.init baseuri in grafite_status,lexicon_status in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) - val mutable include_paths = + val mutable include_paths = (* FIXME, reset every time a new root is entered *) Helm_registry.get_list Helm_registry.string "matita.includes" val scriptId = fresh_script_id () @@ -726,7 +724,7 @@ object (self) match filename_ with | None -> default_buri | Some f -> - try let root, buri, fname = Librarian.baseuri_of_script f in buri + try let _root, buri, _fname, _tgt = Librarian.baseuri_of_script f in buri with Librarian.NoRootFor _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f diff --git a/matita/matitac.ml b/matita/matitac.ml index 968bdf505..199b04157 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -101,11 +101,9 @@ let main_compiler () = HLog.error ("Too many roots found, move into one and retry: "^ String.concat ", " roots);exit 1); | [hd] -> - let root, buri, file = Librarian.baseuri_of_script hd in - Make.load_deps_file (root ^ "/depends"), - let target = HExtlib.chop_prefix (root^"/") file in + let root, buri, file, target = Librarian.baseuri_of_script hd in HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'"); - [target] + Make.load_deps_file (root ^ "/depends"), [target] | _ -> HLog.error "Only one target (or none) can be specified.";exit 1 in (* must be called after init since args are set by cmdline parsing *) diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 7bc3a1b7e..5886c2467 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -103,7 +103,7 @@ let rec compile fname = Helm_registry.get_list Helm_registry.string "matita.includes" in (* sanity checks *) - let root,baseuri,fname = Librarian.baseuri_of_script ~include_paths fname in + let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in @@ -230,7 +230,7 @@ module F = let string_of_target_object s = s;; let target_of mafile = - let _,baseuri,_ = Librarian.baseuri_of_script mafile in + let _,baseuri,_,_ = Librarian.baseuri_of_script mafile in LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true ;; diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml index 8409eb7bc..466104644 100644 --- a/matita/matitaclean.ml +++ b/matita/matitaclean.ml @@ -95,7 +95,7 @@ let main () = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> - let _,u,_ = Librarian.baseuri_of_script ~include_paths:[] suri in + let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 995230c45..6a2dccb91 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -43,7 +43,7 @@ let main () = let baseuri_of_script s = try Hashtbl.find baseuri_of s with Not_found -> - let _,b,_ = Librarian.baseuri_of_script ~include_paths s in + let _,b,_,_ = Librarian.baseuri_of_script ~include_paths s in Hashtbl.add baseuri_of s b; Hashtbl.add baseuri_of_inv b s; b diff --git a/matita/rottener.ml b/matita/rottener.ml deleted file mode 100644 index dfb64037e..000000000 --- a/matita/rottener.ml +++ /dev/null @@ -1,169 +0,0 @@ -(* Copyright (C) 2007, 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/ - *) - -open Printf - -module Ast = GrafiteAst -module Pt = CicNotationPt - - (* set to false to change identifier instead of adding extra identifiers *) -let add_ident = ref true - -let error_token = "O" -let error_token_len = String.length error_token - -let has_toplevel_term = function - | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, ( - Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _) - (*| Pt.Inductive _*) - (*| Pt.Record _*) - ))))) -> - true - | _ -> false - -let flush_token_stream (stream, loc_func) = - let tok_count = ref ~-1 in - let rec aux acc = - let next_tok = - try Some (Stream.next stream) with Stream.Failure -> None in - match next_tok with - | None | Some ("EOI", _) -> List.rev acc - | Some tok -> - incr tok_count; - aux ((tok, loc_func !tok_count) :: acc) in - aux [] - -let rotten_script ~fname statement = - (* XXX terribly inefficient: the same script is read several times ... *) - let lexer = CicNotationLexer.level2_ast_lexer in - let token_stream, loc_func = - lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_string statement)) in - let tokens = flush_token_stream (token_stream, loc_func) in - let target_token, target_pos = - let rec sanitize_tokens acc = function - | [] -> List.rev acc - | (("IDENT", - ("theorem" | "definition" | "lemma" | "record" | "inductive")), _) - :: (("IDENT", _), _) :: tl -> - (* avoid rottening of object names *) - sanitize_tokens acc tl - | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl -> - (* avoid rottening of binders *) - let rec remove_args = function - | (("SYMBOL", ","), _) :: (("IDENT", _), _) :: tl -> - remove_args tl - | tl -> tl in - sanitize_tokens acc (remove_args tl) - | (("SYMBOL", "⇒"), _) as hd :: tl -> - (* avoid rottening of constructor names in pattern matching *) - let rec remove_until_branch_start = function - | (("SYMBOL", ("|" | "[")), _) :: tl -> tl - | hd :: tl -> remove_until_branch_start tl - | [] -> [] in - sanitize_tokens (hd :: remove_until_branch_start acc) tl - | hd :: tl -> (* every other identfier can be rottened! *) - sanitize_tokens (hd :: acc) tl in - let idents = - List.filter (function (("IDENT", _), _) -> true | _ -> false) - (sanitize_tokens [] tokens) in - List.nth idents (Random.int (List.length idents)) - in - let start_pos, end_pos = (* positions in bytecount *) - Glib.Utf8.offset_to_pos statement 0 (Stdpp.first_pos target_pos), - Glib.Utf8.offset_to_pos statement 0 (Stdpp.last_pos target_pos) in - let statement' = - if !add_ident then - String.sub statement 0 start_pos - ^ "O " - ^ String.sub statement start_pos (String.length statement - start_pos) - else - String.sub statement 0 start_pos - ^ "O" - ^ String.sub statement end_pos (String.length statement - end_pos) - in - let script = HExtlib.input_file fname in - let matches = - let rex = - Pcre.regexp ~flags:[`DOTALL] - (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in - try - Pcre.extract ~rex script - with Not_found -> assert false - in - let trailer = (* trailing comment with machine parseable error location *) - let preamble_len = Glib.Utf8.length matches.(1) in - sprintf "\n(*\nerror-at: %d-%d\n*)\n" - (preamble_len + Stdpp.first_pos target_pos) - (preamble_len + Stdpp.first_pos target_pos + error_token_len) in - let script' = - sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in - let md5 = Digest.to_hex (Digest.string script') in - HExtlib.output_file - ~filename:(sprintf "%s.%s.rottened" fname md5) - ~text:script' - -let grep () = - let recursive = ref false in - let spec = [ - "-r", Arg.Set recursive, "enable directory recursion"; - ] in - MatitaInit.add_cmdline_spec spec; - MatitaInit.initialize_all (); - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - let status = - CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script in - let path = - match Helm_registry.get_list Helm_registry.string "matita.args" with - | [ path ] -> path - | _ -> MatitaInit.die_usage () in - let grep_fun = - if !recursive then - (fun dirname -> - let sane_statements = - GrafiteWalker.rgrep_statement ~status ~dirname has_toplevel_term in - List.iter (fun (fname, statement) -> rotten_script ~fname statement) - sane_statements) - else - (fun fname -> - let sane_statements = - GrafiteWalker.grep_statement ~status ~fname has_toplevel_term in - List.iter (fun statement -> rotten_script ~fname statement) - sane_statements) - in - grep_fun path - -let handle_localized_exns f arg = - try - f arg - with HExtlib.Localized (loc, exn) -> - let loc_begin, loc_end = HExtlib.loc_of_floc loc in - eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn) - -let _ = - Random.self_init (); - handle_localized_exns grep () -