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   (* set to false to change identifier instead of adding extra identifiers *)
  32 let add_ident = ref true
  33
  34 let error_token = "O"
  35 let error_token_len = String.length error_token
  36
  37 let has_toplevel_term = function
  38   | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
  39         Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
  40       (*| Pt.Inductive _*)
  41       (*| Pt.Record _*)
  42     ))))) ->
  43       true
  44   | _ -> false
  45
  46 let flush_token_stream (stream, loc_func) =
  47   let tok_count = ref ~-1 in
  48   let rec aux acc =
  49     let next_tok =
  50       try Some (Stream.next stream) with Stream.Failure -> None in
  51     match next_tok with
  52     | None | Some ("EOI", _) -> List.rev acc
  53     | Some tok ->
  54         incr tok_count;
  55         aux ((tok, loc_func !tok_count) :: acc) in
  56   aux []
  57
  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
  66       | [] -> List.rev acc
  67       | (("IDENT",
  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 ->
  76                 remove_args tl
  77             | tl -> tl in
  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
  84             | [] -> [] in
  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
  88     let idents =
  89       List.filter (function (("IDENT", _), _) -> true | _ -> false)
  90         (sanitize_tokens [] tokens) in
  91     List.nth idents (Random.int (List.length idents))
  92   in
  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
  96   let statement' =
  97     if !add_ident then
  98       String.sub statement 0 start_pos
  99       ^ "O "
 100       ^ String.sub statement start_pos (String.length statement - start_pos)
 101     else
 102       String.sub statement 0 start_pos
 103       ^ "O"
 104       ^ String.sub statement end_pos (String.length statement - end_pos)
 105   in
 106   let script = HExtlib.input_file fname in
 107   let matches =
 108     let rex =
 109       Pcre.regexp ~flags:[`DOTALL]
 110         (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in
 111     try
 112       Pcre.extract ~rex script
 113     with Not_found -> assert false
 114   in
 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
 120   let script' =
 121     sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
 122   let md5 = Digest.to_hex (Digest.string script') in
 123   HExtlib.output_file
 124     ~filename:(sprintf "%s.%s.rottened" fname md5)
 125     ~text:script'
 126
 127 let grep () =
 128   let recursive = ref false in
 129   let spec = [
 130     "-r", Arg.Set recursive, "enable directory recursion";
 131   ] in
 132   MatitaInit.add_cmdline_spec spec;
 133   MatitaInit.initialize_all ();
 134   let include_paths =
 135     Helm_registry.get_list Helm_registry.string "matita.includes" in
 136   let status =
 137     CicNotation2.load_notation ~include_paths
 138       BuildTimeConf.core_notation_script in
 139   let path =
 140     match Helm_registry.get_list Helm_registry.string "matita.args" with
 141     | [ path ] -> path
 142     | _ -> MatitaInit.die_usage () in
 143   let grep_fun =
 144     if !recursive then
 145       (fun dirname ->
 146         let sane_statements =
 147           GrafiteWalker.rgrep_statement ~status ~dirname has_toplevel_term in
 148         List.iter (fun (fname, statement) -> rotten_script ~fname statement)
 149           sane_statements)
 150     else
 151       (fun fname ->
 152         let sane_statements =
 153           GrafiteWalker.grep_statement ~status ~fname has_toplevel_term in
 154         List.iter (fun statement -> rotten_script ~fname statement)
 155           sane_statements)
 156   in
 157   grep_fun path
 158
 159 let handle_localized_exns f arg =
 160   try
 161     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)
 165
 166 let _ =
 167   Random.self_init ();
 168   handle_localized_exns grep ()
 169