1 (* Copyright (C) 2007, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module Ast = GrafiteAst
29 module Pt = CicNotationPt
31 (* set to false to change identifier instead of adding extra identifiers *)
32 let add_ident = ref true
35 let error_token_len = String.length error_token
37 let has_toplevel_term = function
38 | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
39 Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
46 let flush_token_stream (stream, loc_func) =
47 let tok_count = ref ~-1 in
50 try Some (Stream.next stream) with Stream.Failure -> None in
52 | None | Some ("EOI", _) -> List.rev acc
55 aux ((tok, loc_func !tok_count) :: acc) in
58 let rotten_script ~fname statement =
59 (* XXX terribly inefficient: the same script is read several times ... *)
60 let lexer = CicNotationLexer.level2_ast_lexer in
61 let token_stream, loc_func =
62 lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_string statement)) in
63 let tokens = flush_token_stream (token_stream, loc_func) in
64 let target_token, target_pos =
65 let rec sanitize_tokens acc = function
68 ("theorem" | "definition" | "lemma" | "record" | "inductive")), _)
69 :: (("IDENT", _), _) :: tl ->
70 (* avoid rottening of object names *)
71 sanitize_tokens acc tl
72 | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl ->
73 (* avoid rottening of binders *)
74 let rec remove_args = function
75 | (("SYMBOL", ","), _) :: (("IDENT", _), _) :: tl ->
78 sanitize_tokens acc (remove_args tl)
79 | (("SYMBOL", "⇒"), _) as hd :: tl ->
80 (* avoid rottening of constructor names in pattern matching *)
81 let rec remove_until_branch_start = function
82 | (("SYMBOL", ("|" | "[")), _) :: tl -> tl
83 | hd :: tl -> remove_until_branch_start tl
85 sanitize_tokens (hd :: remove_until_branch_start acc) tl
86 | hd :: tl -> (* every other identfier can be rottened! *)
87 sanitize_tokens (hd :: acc) tl in
89 List.filter (function (("IDENT", _), _) -> true | _ -> false)
90 (sanitize_tokens [] tokens) in
91 List.nth idents (Random.int (List.length idents))
93 let start_pos, end_pos = (* positions in bytecount *)
94 Glib.Utf8.offset_to_pos statement 0 (Stdpp.first_pos target_pos),
95 Glib.Utf8.offset_to_pos statement 0 (Stdpp.last_pos target_pos) in
98 String.sub statement 0 start_pos
100 ^ String.sub statement start_pos (String.length statement - start_pos)
102 String.sub statement 0 start_pos
104 ^ String.sub statement end_pos (String.length statement - end_pos)
106 let script = HExtlib.input_file fname in
109 Pcre.regexp ~flags:[`DOTALL]
110 (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in
112 Pcre.extract ~rex script
113 with Not_found -> assert false
115 let trailer = (* trailing comment with machine parseable error location *)
116 let preamble_len = Glib.Utf8.length matches.(1) in
117 sprintf "\n(*\nerror-at: %d-%d\n*)\n"
118 (preamble_len + Stdpp.first_pos target_pos)
119 (preamble_len + Stdpp.first_pos target_pos + error_token_len) in
121 sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
122 let md5 = Digest.to_hex (Digest.string script') in
124 ~filename:(sprintf "%s.%s.rottened" fname md5)
128 let recursive = ref false in
130 "-r", Arg.Set recursive, "enable directory recursion";
132 MatitaInit.add_cmdline_spec spec;
133 MatitaInit.initialize_all ();
135 Helm_registry.get_list Helm_registry.string "matita.includes" in
137 CicNotation2.load_notation ~include_paths
138 BuildTimeConf.core_notation_script in
140 match Helm_registry.get_list Helm_registry.string "matita.args" with
142 | _ -> MatitaInit.die_usage () in
146 let sane_statements =
147 GrafiteWalker.rgrep_statement ~status ~dirname has_toplevel_term in
148 List.iter (fun (fname, statement) -> rotten_script ~fname statement)
152 let sane_statements =
153 GrafiteWalker.grep_statement ~status ~fname has_toplevel_term in
154 List.iter (fun statement -> rotten_script ~fname statement)
159 let handle_localized_exns f arg =
162 with HExtlib.Localized (loc, exn) ->
163 let loc_begin, loc_end = HExtlib.loc_of_floc loc in
164 eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn)
168 handle_localized_exns grep ()