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 has_toplevel_term = function
  32   | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
  33         Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
  34       (*| Pt.Inductive _*)
  35       (*| Pt.Record _*)
  36     ))))) ->
  37       true
  38   | _ -> false
  39
  40 let flush_token_stream (stream, loc_func) =
  41   let tok_count = ref ~-1 in
  42   let rec aux acc =
  43     let next_tok =
  44       try Some (Stream.next stream) with Stream.Failure -> None in
  45     match next_tok with
  46     | None | Some ("EOI", _) -> List.rev acc
  47     | Some tok ->
  48         incr tok_count;
  49         aux ((tok, loc_func !tok_count) :: acc) in
  50   aux []
  51
  52 let rotten_script ~fname statement =
  53   (* XXX terribly inefficient: the same script is read several times ... *)
  54   let lexer = CicNotationLexer.level2_ast_lexer in
  55   let token_stream, loc_func =
  56     lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_string statement)) in
  57   let tokens = flush_token_stream (token_stream, loc_func) in
  58   let target_token, target_pos =
  59     let rec sanitize_tokens = function
  60       | [] -> []
  61       | (("IDENT",
  62           ("theorem" | "definition" | "lemma" | "record" | "inductive")), _)
  63         :: (("IDENT", _), _) :: tl
  64       | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl ->
  65           let rec remove_args = function
  66             | (("SYMBOL", ","), _) :: (("IDENT", _), _) :: tl ->
  67                 remove_args tl
  68             | tl -> tl in
  69           let tl' = remove_args tl in
  70           sanitize_tokens tl'
  71       | hd :: tl -> hd :: sanitize_tokens tl in
  72     let idents =
  73       List.filter (function (("IDENT", _), _) -> true | _ -> false)
  74         (sanitize_tokens tokens) in
  75     List.nth idents (Random.int (List.length idents))
  76   in
  77   let statement' =
  78     (* positions in bytecount *)
  79     let start_pos, end_pos =
  80       Glib.Utf8.offset_to_pos statement 0 (Ploc.first_pos target_pos),
  81       Glib.Utf8.offset_to_pos statement 0 (Ploc.last_pos target_pos) in
  82     String.sub statement 0 start_pos
  83     ^ "true"
  84     ^ String.sub statement end_pos (String.length statement - end_pos)
  85   in
  86   let script = HExtlib.input_file fname in
  87   let script' =
  88     Pcre.replace ~pat:(Pcre.quote statement) ~templ:statement' script in
  89   let md5 = Digest.to_hex (Digest.string script') in
  90   HExtlib.output_file
  91     ~filename:(sprintf "%s.rottened.%s.ma" (Filename.chop_extension fname) md5)
  92     ~text:script'
  93
  94 let grep () =
  95   let recursive = ref false in
  96   let spec = [
  97     "-r", Arg.Set recursive, "enable directory recursion";
  98   ] in
  99   MatitaInit.add_cmdline_spec spec;
 100   MatitaInit.initialize_all ();
 101   let include_paths =
 102     Helm_registry.get_list Helm_registry.string "matita.includes" in
 103   let status =
 104     CicNotation2.load_notation ~include_paths
 105       BuildTimeConf.core_notation_script in
 106   let path =
 107     match Helm_registry.get_list Helm_registry.string "matita.args" with
 108     | [ path ] -> path
 109     | _ -> MatitaInit.die_usage () in
 110   let grep_fun =
 111     if !recursive then
 112       (fun dirname ->
 113         let sane_statements =
 114           GrafiteWalker.rgrep_statement ~status ~dirname has_toplevel_term in
 115         List.iter (fun (fname, statement) -> rotten_script ~fname statement)
 116           sane_statements)
 117     else
 118       (fun fname ->
 119         let sane_statements =
 120           GrafiteWalker.grep_statement ~status ~fname has_toplevel_term in
 121         List.iter (fun statement -> rotten_script ~fname statement)
 122           sane_statements)
 123   in
 124   grep_fun path
 125
 126 let handle_localized_exns f arg =
 127   try
 128     f arg
 129   with HExtlib.Localized (loc, exn) ->
 130     let loc_begin, loc_end = HExtlib.loc_of_floc loc in
 131     eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn)
 132
 133 let _ =
 134   Random.init 17;
 135   handle_localized_exns grep ()
 136