module Ast = GrafiteAst
module Pt = CicNotationPt
+ (* set to false to change identifier instead of adding extra identifiers *)
+let add_ident = ref true
+
let error_token = "O"
let error_token_len = String.length error_token
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 (Ploc.first_pos target_pos),
- Glib.Utf8.offset_to_pos statement 0 (Ploc.last_pos target_pos) in
+ let start_pos, end_pos = (* positions in bytecount *)
+ 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 *)
- String.sub statement 0 start_pos
- ^ "O"
- ^ String.sub statement end_pos (String.length statement - end_pos) in
+ if !add_ident then
+ String.sub statement 0 start_pos
+ ^ "O "
+ ^ String.sub statement start_pos (String.length statement - start_pos)
+ else
+ String.sub statement 0 start_pos
+ ^ "O"
+ ^ String.sub statement end_pos (String.length statement - end_pos)
+ in
let script = HExtlib.input_file fname in
let matches =
let rex =
with Not_found -> assert false
in
let trailer = (* trailing comment with machine parseable error location *)
- let preamble_len = String.length matches.(1) in
- sprintf "\n(*\nerror-at: %d-%d\n*)\n" (preamble_len + start_pos)
- (preamble_len + start_pos + error_token_len) in
- let script' = sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
+ 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 () =
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 ()