From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 26 Nov 2007 16:23:50 +0000 (+0000)
Subject: first draft of a script to mechanically introduce (disambiguation) errors into Matita... 
X-Git-Tag: make_still_working~5773
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbf2689a206bb4f7a3b36f6e40a88a47c8ad6e09;p=helm.git

first draft of a script to mechanically introduce (disambiguation) errors into Matita scripts
---

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index ad5a18892..a72357809 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -138,6 +138,13 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
 	$(H)echo "  OCAMLOPT $<"
 	$(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
 
+rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
+	$(H)echo "  OCAMLC $<"
+	$(H)$(OCAMLC) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMOS) $(MAINCMOS) rottener.ml
+rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
+	$(H)echo "  OCAMLOPT $<"
+	$(H)$(OCAMLOPT) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMXS) $(MAINCMXS) rottener.ml
+
 matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
 	$(H)echo "  OCAMLC $<"
 	$(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
@@ -184,6 +191,7 @@ matitaGeneratedGui.ml: matita.glade
 clean:
 	$(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
 		$(PROGRAMS) $(PROGRAMS_OPT) \
+		rottener rottener.opt \
 		$(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \
 		$(PROGRAMS_STATIC) \
 		$(PROGRAMS_UPX) \
diff --git a/helm/software/matita/rottener.ml b/helm/software/matita/rottener.ml
new file mode 100644
index 000000000..7114f018d
--- /dev/null
+++ b/helm/software/matita/rottener.ml
@@ -0,0 +1,136 @@
+(* 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
+
+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 = function
+      | [] -> []
+      | (("IDENT",
+          ("theorem" | "definition" | "lemma" | "record" | "inductive")), _)
+        :: (("IDENT", _), _) :: tl
+      | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl ->
+          let rec remove_args = function
+            | (("SYMBOL", ","), _) :: (("IDENT", _), _) :: tl ->
+                remove_args tl
+            | tl -> tl in
+          let tl' = remove_args tl in
+          sanitize_tokens tl'
+      | hd :: tl -> hd :: sanitize_tokens tl in
+    let idents =
+      List.filter (function (("IDENT", _), _) -> true | _ -> false)
+        (sanitize_tokens tokens) in
+    List.nth idents (Random.int (List.length idents))
+  in
+  let statement' =
+    (* positions in bytecount *)
+    let start_pos, end_pos =
+      Glib.Utf8.offset_to_pos statement 0 (Ploc.first_pos target_pos),
+      Glib.Utf8.offset_to_pos statement 0 (Ploc.last_pos target_pos) in
+    String.sub statement 0 start_pos
+    ^ "true"
+    ^ String.sub statement end_pos (String.length statement - end_pos)
+  in
+  let script = HExtlib.input_file fname in
+  let script' =
+    Pcre.replace ~pat:(Pcre.quote statement) ~templ:statement' script in
+  let md5 = Digest.to_hex (Digest.string script') in
+  HExtlib.output_file
+    ~filename:(sprintf "%s.rottened.%s.ma" (Filename.chop_extension 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.init 17;
+  handle_localized_exns grep ()
+