]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/rottener.ml
ok
[helm.git] / helm / software / matita / rottener.ml
1 (* Copyright (C) 2007, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 module Ast = GrafiteAst
29 module Pt = CicNotationPt
30
31 let error_token = "O"
32 let error_token_len = String.length error_token
33
34 let has_toplevel_term = function
35   | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
36         Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
37       (*| Pt.Inductive _*)
38       (*| Pt.Record _*)
39     ))))) ->
40       true
41   | _ -> false
42
43 let flush_token_stream (stream, loc_func) =
44   let tok_count = ref ~-1 in
45   let rec aux acc =
46     let next_tok =
47       try Some (Stream.next stream) with Stream.Failure -> None in
48     match next_tok with
49     | None | Some ("EOI", _) -> List.rev acc
50     | Some tok ->
51         incr tok_count;
52         aux ((tok, loc_func !tok_count) :: acc) in
53   aux []
54
55 let rotten_script ~fname statement =
56   (* XXX terribly inefficient: the same script is read several times ... *)
57   let lexer = CicNotationLexer.level2_ast_lexer in
58   let token_stream, loc_func =
59     lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_string statement)) in
60   let tokens = flush_token_stream (token_stream, loc_func) in
61   let target_token, target_pos =
62     let rec sanitize_tokens acc = function
63       | [] -> List.rev acc
64       | (("IDENT",
65           ("theorem" | "definition" | "lemma" | "record" | "inductive")), _)
66         :: (("IDENT", _), _) :: tl ->
67           (* avoid rottening of object names *)
68           sanitize_tokens acc tl
69       | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl ->
70           (* avoid rottening of binders *)
71           let rec remove_args = function
72             | (("SYMBOL", ","), _) :: (("IDENT", _), _) :: tl ->
73                 remove_args tl
74             | tl -> tl in
75           sanitize_tokens acc (remove_args tl)
76       | (("SYMBOL", "⇒"), _) as hd :: tl ->
77           (* avoid rottening of constructor names in pattern matching *)
78           let rec remove_until_branch_start = function
79             | (("SYMBOL", ("|" | "[")), _) :: tl -> tl
80             | hd :: tl -> remove_until_branch_start tl
81             | [] -> [] in
82           sanitize_tokens (hd :: remove_until_branch_start acc) tl
83       | hd :: tl -> (* every other identfier can be rottened! *)
84           sanitize_tokens (hd :: acc) tl in
85     let idents =
86       List.filter (function (("IDENT", _), _) -> true | _ -> false)
87         (sanitize_tokens [] tokens) in
88     List.nth idents (Random.int (List.length idents))
89   in
90   let start_pos, end_pos =
91     Glib.Utf8.offset_to_pos statement 0 (Stdpp.first_pos target_pos),
92     Glib.Utf8.offset_to_pos statement 0 (Stdpp.last_pos target_pos) in
93   let statement' =
94     (* positions in bytecount *)
95     String.sub statement 0 start_pos
96     ^ "O"
97     ^ String.sub statement end_pos (String.length statement - end_pos) in
98   let script = HExtlib.input_file fname in
99   let matches =
100     let rex =
101       Pcre.regexp ~flags:[`DOTALL]
102         (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in
103     try
104       Pcre.extract ~rex script
105     with Not_found -> assert false
106   in
107   let trailer = (* trailing comment with machine parseable error location *)
108     let preamble_len = Glib.Utf8.length matches.(1) in
109     sprintf "\n(*\nerror-at: %d-%d\n*)\n"
110     (preamble_len + Stdpp.first_pos target_pos)
111     (preamble_len + Stdpp.first_pos target_pos + error_token_len) in
112   let script' = sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
113   let md5 = Digest.to_hex (Digest.string script') in
114   HExtlib.output_file
115     ~filename:(sprintf "%s.%s.rottened" fname md5)
116     ~text:script'
117
118 let grep () =
119   let recursive = ref false in
120   let spec = [
121     "-r", Arg.Set recursive, "enable directory recursion";
122   ] in
123   MatitaInit.add_cmdline_spec spec;
124   MatitaInit.initialize_all ();
125   let include_paths =
126     Helm_registry.get_list Helm_registry.string "matita.includes" in
127   let status =
128     CicNotation2.load_notation ~include_paths
129       BuildTimeConf.core_notation_script in
130   let path =
131     match Helm_registry.get_list Helm_registry.string "matita.args" with
132     | [ path ] -> path
133     | _ -> MatitaInit.die_usage () in
134   let grep_fun =
135     if !recursive then
136       (fun dirname ->
137         let sane_statements =
138           GrafiteWalker.rgrep_statement ~status ~dirname has_toplevel_term in
139         List.iter (fun (fname, statement) -> rotten_script ~fname statement)
140           sane_statements)
141     else
142       (fun fname ->
143         let sane_statements =
144           GrafiteWalker.grep_statement ~status ~fname has_toplevel_term in
145         List.iter (fun statement -> rotten_script ~fname statement)
146           sane_statements)
147   in
148   grep_fun path
149
150 let handle_localized_exns f arg =
151   try
152     f arg
153   with HExtlib.Localized (loc, exn) ->
154     let loc_begin, loc_end = HExtlib.loc_of_floc loc in
155     eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn)
156
157 let _ =
158   Random.self_init ();
159   handle_localized_exns grep ()
160