X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Frottener.ml;h=27c27766411e4177a85a68f0ad15e3146e1f0df0;hb=b89690596acb0b24f1fd45da28ac04b4ad217e98;hp=7114f018d8d1ae74569169fb47338e0e0b79ef37;hpb=dbf2689a206bb4f7a3b36f6e40a88a47c8ad6e09;p=helm.git

diff --git a/helm/software/matita/rottener.ml b/helm/software/matita/rottener.ml
index 7114f018d..27c277664 100644
--- a/helm/software/matita/rottener.ml
+++ b/helm/software/matita/rottener.ml
@@ -28,6 +28,9 @@ open Printf
 module Ast = GrafiteAst
 module Pt = CicNotationPt
 
+let error_token = "O"
+let error_token_len = String.length error_token
+
 let has_toplevel_term = function
   | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
         Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
@@ -56,39 +59,60 @@ let rotten_script ~fname statement =
     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
-      | [] -> []
+    let rec sanitize_tokens acc = function
+      | [] -> List.rev acc
       | (("IDENT",
           ("theorem" | "definition" | "lemma" | "record" | "inductive")), _)
-        :: (("IDENT", _), _) :: tl
+        :: (("IDENT", _), _) :: tl ->
+          (* avoid rottening of object names *)
+          sanitize_tokens acc tl
       | (("SYMBOL", ("∀" | "λ" | "Π")), _) :: (("IDENT", _), _) :: tl ->
+          (* avoid rottening of binders *)
           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
+          sanitize_tokens acc (remove_args tl)
+      | (("SYMBOL", "⇒"), _) as hd :: tl ->
+          (* avoid rottening of constructor names in pattern matching *)
+          let rec remove_until_branch_start = function
+            | (("SYMBOL", ("|" | "[")), _) :: tl -> tl
+            | hd :: tl -> remove_until_branch_start tl
+            | [] -> [] in
+          sanitize_tokens (hd :: remove_until_branch_start acc) tl
+      | hd :: tl -> (* every other identfier can be rottened! *)
+          sanitize_tokens (hd :: acc) tl in
     let idents =
       List.filter (function (("IDENT", _), _) -> true | _ -> false)
-        (sanitize_tokens tokens) in
+        (sanitize_tokens [] tokens) in
     List.nth idents (Random.int (List.length idents))
   in
+  let start_pos, end_pos =
+    Glib.Utf8.offset_to_pos statement 0 (Stdpp.first_pos target_pos),
+    Glib.Utf8.offset_to_pos statement 0 (Stdpp.last_pos target_pos) 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
+    ^ "O"
+    ^ 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 matches =
+    let rex =
+      Pcre.regexp ~flags:[`DOTALL]
+        (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in
+    try
+      Pcre.extract ~rex script
+    with Not_found -> assert false
+  in
+  let trailer = (* trailing comment with machine parseable error location *)
+    let preamble_len = Glib.Utf8.length matches.(1) in
+    sprintf "\n(*\nerror-at: %d-%d\n*)\n"
+    (preamble_len + Stdpp.first_pos target_pos)
+    (preamble_len + Stdpp.first_pos target_pos + error_token_len) in
+  let script' = sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
   let md5 = Digest.to_hex (Digest.string script') in
   HExtlib.output_file
-    ~filename:(sprintf "%s.rottened.%s.ma" (Filename.chop_extension fname) md5)
+    ~filename:(sprintf "%s.%s.rottened" fname md5)
     ~text:script'
 
 let grep () =
@@ -131,6 +155,6 @@ let handle_localized_exns f arg =
     eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn)
 
 let _ =
-  Random.init 17;
+  Random.self_init ();
   handle_localized_exns grep ()