<commit_before>(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen

Isar proof reconstruction from ATP proofs.
*)

signature SLEDGEHAMMER_ISAR =
sig
  type atp_step_name = ATP_Proof.atp_step_name
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
  type 'a atp_proof = 'a ATP_Proof.atp_proof
  type stature = ATP_Problem_Generate.stature
  type one_line_params = Sledgehammer_Proof_Methods.one_line_params

  val trace : bool Config.T

  type isar_params =
    bool * (string option * string option) * Time.time * real * bool * bool
    * (term, string) atp_step list * thm

  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
    int -> one_line_params -> string
end;

structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct

open ATP_Util
open ATP_Problem
open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Compress
open Sledgehammer_Isar_Minimize

structure String_Redirect = ATP_Proof_Redirect(
  type key = atp_step_name
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
  val string_of = fst)

open String_Redirect

val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)

val e_skolemize_rule = "skolemize"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
val z3_skolemize_rule = "sk"
val z3_th_lemma_rule = "th-lemma"

val skolemize_rules =
  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]

val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = String.isPrefix z3_th_lemma_rule
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule

fun raw_label_of_num num = (num, 0)

fun label_of_clause [(num, _)] = raw_label_of_num num
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)

fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))

fun is_True_prop t = t aconv @{prop True}

fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
       definitions. *)
    if role = Conjecture orelse role = Negated_Conjecture then line :: lines
    else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
    else if role = Axiom then lines (* axioms (facts) need no proof lines *)
    else map (replace_dependencies_in_line (name, [])) lines
  | add_line_pass1 line lines = line :: lines

fun add_lines_pass2 res _ [] = rev res
  | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
    let
      val is_last_line = null lines

      fun looks_interesting () =
        not (is_True_prop t) andalso not (t aconv prev_t) andalso null (Term.add_tvars t []) andalso
        length deps >= 2 andalso not (can the_single lines)

      fun is_skolemizing_line (_, _, _, rule', deps') =
        is_skolemize_rule rule' andalso member (op =) deps' name
      fun is_before_skolemize_rule () = exists is_skolemizing_line lines
    in
      if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
         is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
         is_before_skolemize_rule () then
        add_lines_pass2 (line :: res) t lines
      else
        add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
    end

type isar_params =
  bool * (string option * string option) * Time.time * real * bool * bool
  * (term, string) atp_step list * thm

val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]

val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
val datatype_methods = [Simp_Method, Simp_Size_Method]<commit_msg>refined filter for ATP steps to avoid 'have True' steps in E proofs<commit_after>(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen

Isar proof reconstruction from ATP proofs.
*)

signature SLEDGEHAMMER_ISAR =
sig
  type atp_step_name = ATP_Proof.atp_step_name
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
  type 'a atp_proof = 'a ATP_Proof.atp_proof
  type stature = ATP_Problem_Generate.stature
  type one_line_params = Sledgehammer_Proof_Methods.one_line_params

  val trace : bool Config.T

  type isar_params =
    bool * (string option * string option) * Time.time * real * bool * bool
    * (term, string) atp_step list * thm

  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
    int -> one_line_params -> string
end;

structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct

open ATP_Util
open ATP_Problem
open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Compress
open Sledgehammer_Isar_Minimize

structure String_Redirect = ATP_Proof_Redirect(
  type key = atp_step_name
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
  val string_of = fst)

open String_Redirect

val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)

val e_skolemize_rule = "skolemize"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
val z3_skolemize_rule = "sk"
val z3_th_lemma_rule = "th-lemma"

val skolemize_rules =
  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]

val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = String.isPrefix z3_th_lemma_rule
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule

fun raw_label_of_num num = (num, 0)

fun label_of_clause [(num, _)] = raw_label_of_num num
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)

fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))

fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
       definitions. *)
    if role = Conjecture orelse role = Negated_Conjecture then line :: lines
    else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines
    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
    else if role = Axiom then lines (* axioms (facts) need no proof lines *)
    else map (replace_dependencies_in_line (name, [])) lines
  | add_line_pass1 line lines = line :: lines

fun add_lines_pass2 res _ [] = rev res
  | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
    let
      fun looks_boring () =
        t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse
        length deps < 2

      fun is_skolemizing_line (_, _, _, rule', deps') =
        is_skolemize_rule rule' andalso member (op =) deps' name
      fun is_before_skolemize_rule () = exists is_skolemizing_line lines
    in
      if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
         is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse
         is_before_skolemize_rule () then
        add_lines_pass2 (line :: res) t lines
      else
        add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
    end

type isar_params =
  bool * (string option * string option) * Time.time * real * bool * bool
  * (term, string) atp_step list * thm

val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]

val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
val datatype_methods = [Simp_Method, Simp_Size_Method]
{'fraction_non_alphanumeric': 0.083161983093443, 'fraction_numerical': 0.003427004797806717, 'mean_word_length': 4.4514321295143215, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 28, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '1683666', 'n_tokens_mistral': 3200, 'n_tokens_neox': 3090, 'n_words': 856}