From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Nov 2007 11:19:14 +0000 (+0000)
Subject: avoid rottening of constructor names in pattern matchings
X-Git-Tag: make_still_working~5768
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ba64c01b703caf47b4654c8fc954a8aa7818173;p=helm.git

avoid rottening of constructor names in pattern matchings
---

diff --git a/helm/software/matita/rottener.ml b/helm/software/matita/rottener.ml
index 9888e11e7..82f4d5947 100644
--- a/helm/software/matita/rottener.ml
+++ b/helm/software/matita/rottener.ml
@@ -59,22 +59,32 @@ 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 =