<commit_before>(*  Title:      HOL/Tools/ATP/atp_util.ML
    Author:     <NAME>, <NAME>

General-purpose functions used by the ATP module.
*)

signature ATP_UTIL =
sig
  val timestamp : unit -> string
  val hash_string : string -> int
  val hash_term : term -> int
  val strip_spaces : bool -> (char -> bool) -> string -> string
  val strip_spaces_except_between_idents : string -> string
  val nat_subscript : int -> string
  val unyxml : string -> string
  val maybe_quote : string -> string
  val string_from_ext_time : bool * Time.time -> string
  val string_from_time : Time.time -> string
  val type_instance : Proof.context -> typ -> typ -> bool
  val type_generalization : Proof.context -> typ -> typ -> bool
  val type_intersect : Proof.context -> typ -> typ -> bool
  val type_equiv : Proof.context -> typ * typ -> bool
  val varify_type : Proof.context -> typ -> typ
  val instantiate_type : theory -> typ -> typ -> typ -> typ
  val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
  val typ_of_dtyp :
    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
    -> typ
  val is_type_surely_finite : Proof.context -> typ -> bool
  val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
  val s_not : term -> term
  val s_conj : term * term -> term
  val s_disj : term * term -> term
  val s_imp : term * term -> term
  val s_iff : term * term -> term
  val close_form : term -> term
  val monomorphic_term : Type.tyenv -> term -> term
  val eta_expand : typ list -> term -> int -> term
  val transform_elim_prop : term -> term
  val specialize_type : theory -> (string * typ) -> term -> term
  val strip_subgoal :
    Proof.context -> thm -> int -> (string * typ) list * term list * term
end;

structure ATP_Util : ATP_UTIL =
struct

val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now

(* This hash function is recommended in "Compilers: Principles, Techniques, and
   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
  | hashw_term _ = 0w0

fun hash_string s = Word.toInt (hashw_string (s, 0w0))
val hash_term = Word.toInt o hashw_term

fun strip_c_style_comment _ [] = []
  | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
    strip_spaces_in_list true is_evil cs
  | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
and strip_spaces_in_list _ _ [] = []
  | strip_spaces_in_list true is_evil (#"%" :: cs) =
    strip_spaces_in_list true is_evil
                         (cs |> chop_while (not_equal #"\n") |> snd)
  | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
    strip_c_style_comment is_evil cs
  | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
  | strip_spaces_in_list skip_comments is_evil [c1, c2] =
    strip_spaces_in_list skip_comments is_evil [c1] @
    strip_spaces_in_list skip_comments is_evil [c2]
  | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
    if Char.isSpace c1 then
      strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
    else if Char.isSpace c2 then
      if Char.isSpace c3 then
        strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
      else
        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
        strip_spaces_in_list skip_comments is_evil (c3 :: cs)
    else
      str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
fun strip_spaces skip_comments is_evil =
  implode o strip_spaces_in_list skip_comments is_evil o String.explode

fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
val strip_spaces_except_between_idents = strip_spaces true is_ident_char

val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript

val unyxml = XML.content_of o YXML.parse_body

val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
fun maybe_quote y =
  let val s = unyxml y in
    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
           Keyword.is_keyword s) ? quote<commit_msg>tail recursive proof preprocessing (needed for huge proofs)<commit_after>(*  Title:      HOL/Tools/ATP/atp_util.ML
    Author:     <NAME>, <NAME>

General-purpose functions used by the ATP module.
*)

signature ATP_UTIL =
sig
  val timestamp : unit -> string
  val hash_string : string -> int
  val hash_term : term -> int
  val strip_spaces : bool -> (char -> bool) -> string -> string
  val strip_spaces_except_between_idents : string -> string
  val nat_subscript : int -> string
  val unyxml : string -> string
  val maybe_quote : string -> string
  val string_from_ext_time : bool * Time.time -> string
  val string_from_time : Time.time -> string
  val type_instance : Proof.context -> typ -> typ -> bool
  val type_generalization : Proof.context -> typ -> typ -> bool
  val type_intersect : Proof.context -> typ -> typ -> bool
  val type_equiv : Proof.context -> typ * typ -> bool
  val varify_type : Proof.context -> typ -> typ
  val instantiate_type : theory -> typ -> typ -> typ -> typ
  val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
  val typ_of_dtyp :
    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
    -> typ
  val is_type_surely_finite : Proof.context -> typ -> bool
  val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
  val s_not : term -> term
  val s_conj : term * term -> term
  val s_disj : term * term -> term
  val s_imp : term * term -> term
  val s_iff : term * term -> term
  val close_form : term -> term
  val monomorphic_term : Type.tyenv -> term -> term
  val eta_expand : typ list -> term -> int -> term
  val transform_elim_prop : term -> term
  val specialize_type : theory -> (string * typ) -> term -> term
  val strip_subgoal :
    Proof.context -> thm -> int -> (string * typ) list * term list * term
end;

structure ATP_Util : ATP_UTIL =
struct

val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now

(* This hash function is recommended in "Compilers: Principles, Techniques, and
   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
  | hashw_term _ = 0w0

fun hash_string s = Word.toInt (hashw_string (s, 0w0))
val hash_term = Word.toInt o hashw_term

fun strip_spaces skip_comments is_evil =
  let
    fun strip_c_style_comment [] accum = accum
      | strip_c_style_comment (#"*" :: #"/" :: cs) accum =
        strip_spaces_in_list true cs accum
      | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
    and strip_spaces_in_list _ [] accum = rev accum
      | strip_spaces_in_list true (#"%" :: cs) accum =
        strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd)
                             accum
      | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum =
        strip_c_style_comment cs accum
      | strip_spaces_in_list _ [c1] accum =
        accum |> not (Char.isSpace c1) ? cons c1
      | strip_spaces_in_list skip_comments (cs as [_, _]) accum =
        accum |> fold (strip_spaces_in_list skip_comments o single) cs
      | strip_spaces_in_list skip_comments (c1 :: c2 :: c3 :: cs) accum =
        if Char.isSpace c1 then
          strip_spaces_in_list skip_comments (c2 :: c3 :: cs) accum
        else if Char.isSpace c2 then
          if Char.isSpace c3 then
            strip_spaces_in_list skip_comments (c1 :: c3 :: cs) accum
          else
            strip_spaces_in_list skip_comments (c3 :: cs)
                (c1 :: accum |> forall is_evil [c1, c3] ? cons #" ")
        else
          strip_spaces_in_list skip_comments (c2 :: c3 :: cs) (cons c1 accum)
  in
    String.explode
    #> rpair [] #-> strip_spaces_in_list skip_comments
    #> rev #> String.implode
  end

fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
val strip_spaces_except_between_idents = strip_spaces true is_ident_char

val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript

val unyxml = XML.content_of o YXML.parse_body

val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
fun maybe_quote y =
  let val s = unyxml y in
    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
           Keyword.is_keyword s) ? quote
{'fraction_non_alphanumeric': 0.11257371524852569, 'fraction_numerical': 0.009056444818871103, 'mean_word_length': 3.1635247698377906, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 148, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 6}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3841332', 'n_tokens_mistral': 3397, 'n_tokens_neox': 3253, 'n_words': 987}