src/HOL/Tools/ATP/atp_proof.ML
author blanchet
Mon, 12 Jul 2021 16:30:17 +0200
changeset 73972 b304285fd800
parent 73971 96a05b8462f9
child 74006 1a0a536b8aaf
permissions -rw-r--r--
parse logical operators in the right order w.r.t. backtracking
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/ATP/atp_proof.ML
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     3
    Author:     Claire Quigley, Cambridge University Computer Laboratory
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
57697
44341963ade3 correctly translate THF functions from terms to types
blanchet
parents: 57656
diff changeset
     5
    Author:     Mathias Fleury, ENS Rennes
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     6
42876
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42848
diff changeset
     7
Abstract representation of ATP proofs and TSTP/SPASS syntax.
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     8
*)
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
     9
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    10
signature ATP_PROOF =
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    11
sig
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    12
  type 'a atp_type = 'a ATP_Problem.atp_type
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    13
  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    14
  type atp_formula_role = ATP_Problem.atp_formula_role
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    15
  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    16
  type 'a atp_problem = 'a ATP_Problem.atp_problem
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    17
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42962
diff changeset
    18
  exception UNRECOGNIZED_ATP_PROOF of unit
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42962
diff changeset
    19
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    20
  datatype atp_failure =
58654
3e1cad27fc2f special treatment of extensionality in minimizer
blanchet
parents: 58600
diff changeset
    21
    MaybeUnprovable |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    22
    Unprovable |
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43029
diff changeset
    23
    GaveUp |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    24
    ProofMissing |
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42876
diff changeset
    25
    ProofIncomplete |
57266
6a3b5085fb8f fixed parsing of one-argument 'file()' in TSTP files
blanchet
parents: 57261
diff changeset
    26
    ProofUnparsable |
44915
635ae0a73688 simplified unsound proof detection by removing impossible case
blanchet
parents: 44784
diff changeset
    27
    UnsoundProof of bool * string list |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    28
    TimedOut |
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42943
diff changeset
    29
    Inappropriate |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    30
    OutOfResources |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    31
    MalformedInput |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    32
    MalformedOutput |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    33
    Interrupted |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    34
    Crashed |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    35
    InternalError |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
    36
    UnknownError of string
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
    37
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    38
  type atp_step_name = string * string list
53587
3fb81ab13ea3 generalized data structure, for extension with SMT solver proofs
blanchet
parents: 53586
diff changeset
    39
  type ('a, 'b) atp_step =
3fb81ab13ea3 generalized data structure, for extension with SMT solver proofs
blanchet
parents: 53586
diff changeset
    40
    atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    41
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    42
  type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    43
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    44
  val agsyholN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    45
  val alt_ergoN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    46
  val eN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    47
  val iproverN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    48
  val leo2N : string
67021
41f1f8c4259b integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents: 66545
diff changeset
    49
  val leo3N : string
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
    50
  val pirateN : string
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    51
  val satallaxN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    52
  val spassN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    53
  val vampireN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    54
  val waldmeisterN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    55
  val z3_tptpN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    56
  val zipperpositionN : string
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    57
  val remote_prefix : string
72588
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72403
diff changeset
    58
  val dummy_tfxN : string
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
    59
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
    60
  val agsyhol_core_rule : string
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
    61
  val spass_input_rule : string
55192
b75b52c7cf94 unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
blanchet
parents: 54836
diff changeset
    62
  val spass_pre_skolemize_rule : string
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
    63
  val spass_skolemize_rule : string
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
    64
  val z3_tptp_core_rule : string
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
    65
41259
13972ced98d9 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents: 41222
diff changeset
    66
  val short_output : bool -> string -> string
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    67
  val string_of_atp_failure : atp_failure -> string
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
    68
  val extract_important_message : string -> string
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    69
  val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
    70
  val extract_tstplike_proof_and_outcome :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    71
    bool -> (string * string) list -> (atp_failure * string) list -> string
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    72
    -> string * atp_failure option
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    73
  val is_same_atp_step : atp_step_name -> atp_step_name -> bool
42961
f30ae82cb62e eliminated more code duplication in Nitrox
blanchet
parents: 42953
diff changeset
    74
  val scan_general_id : string list -> string * string list
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
    75
  val parse_fol_formula : string list ->
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    76
    (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
    77
  val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    78
  val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
    79
  val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57697
diff changeset
    80
72399
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    81
  val skip_term : string list -> string * string list
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    82
  val parse_hol_formula : string list ->
57714
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    83
    ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula *
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    84
    string list
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    85
  val dummy_atype : string ATP_Problem.atp_type
72399
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    86
  val role_of_tptp_string : string -> ATP_Problem.atp_formula_role
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    87
  val parse_line : string -> ('a * string ATP_Problem.atp_problem_line list) list ->
57714
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    88
    string list -> ((string * string list) * ATP_Problem.atp_formula_role *
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    89
    (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    90
      'c) ATP_Problem.atp_formula
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
    91
    * string * (string * 'd list) list) list * string list
57716
4546c9fdd8a7 Improving robustness and indentation corrections.
fleury
parents: 57714
diff changeset
    92
  val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
4546c9fdd8a7 Improving robustness and indentation corrections.
fleury
parents: 57714
diff changeset
    93
    ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
70586
57df8a85317a clarified signature;
wenzelm
parents: 68250
diff changeset
    94
  val vampire_step_name_ord : (string * 'a) ord
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57697
diff changeset
    95
  val core_of_agsyhol_proof :  string -> string list option
72355
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
    96
  val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string
72399
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    97
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
    98
  val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
    99
end;
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   100
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   101
structure ATP_Proof : ATP_PROOF =
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   102
struct
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   103
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43050
diff changeset
   104
open ATP_Util
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   105
open ATP_Problem
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   106
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   107
val agsyholN = "agsyhol"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   108
val alt_ergoN = "alt_ergo"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   109
val eN = "e"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   110
val iproverN = "iprover"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   111
val leo2N = "leo2"
67021
41f1f8c4259b integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents: 66545
diff changeset
   112
val leo3N = "leo3"
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   113
val pirateN = "pirate"
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   114
val satallaxN = "satallax"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   115
val spassN = "spass"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   116
val vampireN = "vampire"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   117
val waldmeisterN = "waldmeister"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   118
val z3_tptpN = "z3_tptp"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   119
val zipperpositionN = "zipperposition"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   120
val remote_prefix = "remote_"
72588
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72403
diff changeset
   121
val dummy_tfxN = "dummy_tfx"
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   122
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   123
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   124
val spass_input_rule = "Inp"
55192
b75b52c7cf94 unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
blanchet
parents: 54836
diff changeset
   125
val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   126
val spass_skolemize_rule = "__Sko" (* arbitrary *)
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   127
val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   128
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42962
diff changeset
   129
exception UNRECOGNIZED_ATP_PROOF of unit
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42962
diff changeset
   130
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   131
datatype atp_failure =
58654
3e1cad27fc2f special treatment of extensionality in minimizer
blanchet
parents: 58600
diff changeset
   132
  MaybeUnprovable |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   133
  Unprovable |
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43029
diff changeset
   134
  GaveUp |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   135
  ProofMissing |
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42876
diff changeset
   136
  ProofIncomplete |
57266
6a3b5085fb8f fixed parsing of one-argument 'file()' in TSTP files
blanchet
parents: 57261
diff changeset
   137
  ProofUnparsable |
44915
635ae0a73688 simplified unsound proof detection by removing impossible case
blanchet
parents: 44784
diff changeset
   138
  UnsoundProof of bool * string list |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   139
  TimedOut |
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42943
diff changeset
   140
  Inappropriate |
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   141
  OutOfResources |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   142
  MalformedInput |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   143
  MalformedOutput |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   144
  Interrupted |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   145
  Crashed |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   146
  InternalError |
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42550
diff changeset
   147
  UnknownError of string
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   148
41259
13972ced98d9 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents: 41222
diff changeset
   149
fun short_output verbose output =
42060
889d767ce5f4 make Minimizer honor "verbose" and "debug" options better
blanchet
parents: 41944
diff changeset
   150
  if verbose then
889d767ce5f4 make Minimizer honor "verbose" and "debug" options better
blanchet
parents: 41944
diff changeset
   151
    if output = "" then "No details available" else elide_string 1000 output
889d767ce5f4 make Minimizer honor "verbose" and "debug" options better
blanchet
parents: 41944
diff changeset
   152
  else
889d767ce5f4 make Minimizer honor "verbose" and "debug" options better
blanchet
parents: 41944
diff changeset
   153
    ""
41259
13972ced98d9 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents: 41222
diff changeset
   154
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41738
diff changeset
   155
val missing_message_tail =
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   156
  " appears to be missing; you will need to install it if you want to invoke \
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   157
  \remote provers"
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   158
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   159
fun from_lemmas [] = ""
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   160
  | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
42876
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42848
diff changeset
   161
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   162
fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   163
  | string_of_atp_failure Unprovable = "The generated problem is unprovable"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   164
  | string_of_atp_failure GaveUp = "The prover gave up"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   165
  | string_of_atp_failure ProofMissing =
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   166
    "The prover claims the conjecture is a theorem but did not provide a proof"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   167
  | string_of_atp_failure ProofIncomplete =
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   168
    "The prover claims the conjecture is a theorem but provided an incomplete proof"
57266
6a3b5085fb8f fixed parsing of one-argument 'file()' in TSTP files
blanchet
parents: 57261
diff changeset
   169
  | string_of_atp_failure ProofUnparsable =
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   170
    "The prover claims the conjecture is a theorem but provided an unparsable proof"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   171
  | string_of_atp_failure (UnsoundProof (false, ss)) =
73971
96a05b8462f9 improved warning
blanchet
parents: 73436
diff changeset
   172
    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   173
    "; specify a sound type encoding or omit the \"type_enc\" option"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   174
  | string_of_atp_failure (UnsoundProof (true, ss)) =
73971
96a05b8462f9 improved warning
blanchet
parents: 73436
diff changeset
   175
    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   176
    ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   177
  | string_of_atp_failure TimedOut = "Timed out"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   178
  | string_of_atp_failure Inappropriate =
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   179
    "The generated problem lies outside the prover's scope"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   180
  | string_of_atp_failure OutOfResources = "The prover ran out of resources"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   181
  | string_of_atp_failure MalformedInput = "The generated problem is malformed"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   182
  | string_of_atp_failure MalformedOutput = "The prover output is malformed"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   183
  | string_of_atp_failure Interrupted = "The prover was interrupted"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   184
  | string_of_atp_failure Crashed = "The prover crashed"
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   185
  | string_of_atp_failure InternalError = "An internal prover error occurred"
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   186
  | string_of_atp_failure (UnknownError s) =
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41738
diff changeset
   187
    "A prover error occurred" ^
66545
97c441c8665d tuned messages
blanchet
parents: 66544
diff changeset
   188
    (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s)
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   189
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   190
fun extract_delimited (begin_delim, end_delim) output =
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   191
  (case first_field begin_delim output of
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   192
    SOME (_, tail) =>
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   193
    (case first_field "\n" tail of
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   194
      SOME (_, tail') =>
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   195
      if end_delim = "" then
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   196
        tail'
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   197
      else
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   198
        (case first_field end_delim tail' of
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   199
          SOME (body, _) => body
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   200
        | NONE => "")
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   201
    | NONE => "")
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   202
  | NONE => "")
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   203
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   204
val tstp_important_message_delims =
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   205
  ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   206
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   207
fun extract_important_message output =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   208
  (case extract_delimited tstp_important_message_delims output of
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   209
    "" => ""
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   210
  | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   211
           |> map (perhaps (try (unprefix "%")))
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   212
           |> map (perhaps (try (unprefix " ")))
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   213
           |> space_implode "\n " |> quote)
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   214
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   215
(* Splits by the first possible of a list of delimiters. *)
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   216
fun extract_tstplike_proof delims output =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   217
  (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   218
    (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   219
  | _ => "")
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   220
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   221
fun extract_known_atp_failure known_failures output =
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   222
  known_failures
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   223
  |> find_first (fn (_, pattern) => String.isSubstring pattern output)
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   224
  |> Option.map fst
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39457
diff changeset
   225
57017
blanchet
parents: 56404
diff changeset
   226
fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output =
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   227
  let
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   228
    val known_atp_failure = extract_known_atp_failure known_failures output
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   229
    val tstplike_proof = extract_tstplike_proof proof_delims output
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   230
  in
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   231
    (case (tstplike_proof, known_atp_failure) of
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   232
      (_, SOME ProofIncomplete) => ("", NONE)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   233
    | (_, SOME ProofUnparsable) => ("", NONE)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   234
    | ("", SOME ProofMissing) => ("", NONE)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   235
    | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   236
    | res as ("", _) => res
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   237
    | (tstplike_proof, _) => (tstplike_proof, NONE))
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   238
  end
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   239
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53225
diff changeset
   240
type atp_step_name = string * string list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   241
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   242
fun is_same_atp_step (s1, _) (s2, _) = s1 = s2
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   243
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   244
val vampire_fact_prefix = "f"
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   245
52755
4183c3219745 simplified Vampire hack -- no need to run it for other ATPs
blanchet
parents: 52077
diff changeset
   246
fun vampire_step_name_ord p =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   247
  let val q = apply2 fst p in
52755
4183c3219745 simplified Vampire hack -- no need to run it for other ATPs
blanchet
parents: 52077
diff changeset
   248
    (* The "unprefix" part is to cope with Vampire's output. *)
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   249
    (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of
52755
4183c3219745 simplified Vampire hack -- no need to run it for other ATPs
blanchet
parents: 52077
diff changeset
   250
      (SOME i, SOME j) => int_ord (i, j)
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   251
    | _ => raise Fail "not Vampire")
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   252
  end
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   253
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   254
type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   255
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   256
type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   257
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   258
(**** PARSING OF TSTP FORMAT ****)
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   259
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   260
(* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   261
   with "$" and possibly with "!" in them (for "z3_tptp"). *)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   262
val scan_general_id =
47917
b287682bf917 improve parsing of Waldmeister dependencies (and kill obsolete hack)
blanchet
parents: 47787
diff changeset
   263
  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   264
  || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode))
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   265
    -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) ""
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   266
    >> op ^
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   267
70805
c39bd607203b generalized parsing, for e.g. Leo-III
blanchet
parents: 70586
diff changeset
   268
fun skip_term x =
45208
9a00f9cc8707 marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
blanchet
parents: 45203
diff changeset
   269
  let
45235
7187bce94e88 more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents: 45209
diff changeset
   270
    fun skip _ accum [] = (accum, [])
54803
41a109a00c53 fixed variable confusion introduced by 'tuning' change 565f9af86d67
blanchet
parents: 54799
diff changeset
   271
      | skip n accum (ss as s :: ss') =
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57697
diff changeset
   272
        if (s = "," orelse s = ".") andalso n = 0 then
54799
blanchet
parents: 54788
diff changeset
   273
          (accum, ss)
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   274
        else if member (op =) [")", "]"] s then
54803
41a109a00c53 fixed variable confusion introduced by 'tuning' change 565f9af86d67
blanchet
parents: 54799
diff changeset
   275
          if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   276
        else if member (op =) ["(", "["] s then
54803
41a109a00c53 fixed variable confusion introduced by 'tuning' change 565f9af86d67
blanchet
parents: 54799
diff changeset
   277
          skip (n + 1) (s :: accum) ss'
54799
blanchet
parents: 54788
diff changeset
   278
        else
54803
41a109a00c53 fixed variable confusion introduced by 'tuning' change 565f9af86d67
blanchet
parents: 54799
diff changeset
   279
          skip n (s :: accum) ss'
54799
blanchet
parents: 54788
diff changeset
   280
  in
70805
c39bd607203b generalized parsing, for e.g. Leo-III
blanchet
parents: 70586
diff changeset
   281
    (skip 0 [] #>> (rev #> implode)) x
54799
blanchet
parents: 54788
diff changeset
   282
  end
70805
c39bd607203b generalized parsing, for e.g. Leo-III
blanchet
parents: 70586
diff changeset
   283
and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
45208
9a00f9cc8707 marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
blanchet
parents: 45203
diff changeset
   284
9a00f9cc8707 marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
blanchet
parents: 45203
diff changeset
   285
datatype source =
9a00f9cc8707 marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
blanchet
parents: 45203
diff changeset
   286
  File_Source of string * string option |
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   287
  Inference_Source of string * string list |
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   288
  Introduced_Source of string
45208
9a00f9cc8707 marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
blanchet
parents: 45203
diff changeset
   289
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48130
diff changeset
   290
val dummy_phi = AAtom (ATerm (("", []), []))
57697
44341963ade3 correctly translate THF functions from terms to types
blanchet
parents: 57656
diff changeset
   291
val dummy_atype = AType (("", []), [])
45235
7187bce94e88 more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents: 45209
diff changeset
   292
54769
3d6ac2f68bf3 correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents: 53587
diff changeset
   293
(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
50011
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   294
fun parse_dependency x =
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   295
  (parse_inference_source >> snd
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   296
   || scan_general_id --| skip_term >> single) x
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   297
and parse_dependencies x =
61476
1884c40f1539 tuned signature;
wenzelm
parents: 61329
diff changeset
   298
  (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency)
1884c40f1539 tuned signature;
wenzelm
parents: 61329
diff changeset
   299
   >> (filter_out (curry (op =) "theory"))) x
50011
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   300
and parse_file_source x =
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   301
  (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   302
   -- Scan.option ($$ "," |-- scan_general_id
57266
6a3b5085fb8f fixed parsing of one-argument 'file()' in TSTP files
blanchet
parents: 57261
diff changeset
   303
     --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x
50011
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   304
and parse_inference_source x =
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   305
  (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   306
   --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   307
   -- parse_dependencies --| $$ "]" --| $$ ")") x
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   308
and parse_introduced_source x =
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   309
  (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   310
   --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x
50011
f046cf7be176 correct parsing of E dependencies
blanchet
parents: 48716
diff changeset
   311
and parse_source x =
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   312
  (parse_file_source >> File_Source >> SOME
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   313
   || parse_inference_source >> Inference_Source >> SOME
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   314
   || parse_introduced_source >> Introduced_Source >> SOME
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   315
   || scan_general_id >> (fn s => SOME (Inference_Source ("", [s]))) (* for E *)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   316
   || skip_term >> K NONE) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   317
54799
blanchet
parents: 54788
diff changeset
   318
fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42965
diff changeset
   319
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54811
diff changeset
   320
fun parse_class x = scan_general_id x
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54811
diff changeset
   321
and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   322
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   323
fun parse_type x =
66428
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   324
  (($$ "(" |-- parse_type --| $$ ")"
70805
c39bd607203b generalized parsing, for e.g. Leo-III
blanchet
parents: 70586
diff changeset
   325
    || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type
67022
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   326
       >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *))
66428
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   327
    || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   328
        -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   329
       >> AType)
67022
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   330
   -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
66428
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   331
  >> (fn (a, NONE) => a
67022
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   332
       | (a, SOME (bin_op, b)) =>
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   333
         if bin_op = tptp_app then
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   334
           (case a of
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   335
             AType (s_clss, tys) => AType (s_clss, tys @ [b])
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   336
           | _ => raise UNRECOGNIZED_ATP_PROOF ())
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   337
         else if bin_op = tptp_fun_type then
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   338
           AFun (a, b)
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   339
         else if bin_op = tptp_product_type then
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   340
           AType ((tptp_product_type, []), [a, b])
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   341
         else
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   342
           raise Fail "impossible case")) x
66544
3e838cf5e80c improved Vampire proof parser
blanchet
parents: 66428
diff changeset
   343
and parse_types x =
3e838cf5e80c improved Vampire proof parser
blanchet
parents: 66428
diff changeset
   344
  (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   345
58477
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   346
(* We currently half ignore types. *)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   347
fun parse_fol_optional_type_signature x =
58600
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 58477
diff changeset
   348
  (Scan.option ($$ tptp_has_type |-- parse_type)
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 58477
diff changeset
   349
   >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 58477
diff changeset
   350
        | res => res)) x
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   351
and parse_fol_arg x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   352
  ($$ "(" |-- parse_fol_term --| $$ ")" --| parse_fol_optional_type_signature
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   353
   || scan_general_id -- parse_fol_optional_type_signature
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   354
       -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   355
       -- Scan.optional ($$ "(" |-- parse_fol_terms --| $$ ")") []
58477
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   356
     >> (fn (((s, ty_opt), tyargs), args) =>
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   357
       if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   358
         ATerm ((s, the_list ty_opt), [])
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   359
       else
8438bae06e63 parse back type of SPASS proof variables
blanchet
parents: 58324
diff changeset
   360
         ATerm ((s, tyargs), args))) x
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   361
and parse_fol_term x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   362
  (parse_fol_arg -- Scan.repeat ($$ tptp_app |-- parse_fol_arg)
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   363
   --| parse_fol_optional_type_signature >> list_app) x
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   364
and parse_fol_terms x = (parse_fol_term ::: Scan.repeat ($$ "," |-- parse_fol_term)) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   365
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   366
fun parse_fol_atom x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   367
  (parse_fol_term --
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   368
    Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_fol_term)
39598
57413334669d make SML/NJ happier
blanchet
parents: 39491
diff changeset
   369
   >> (fn (u1, NONE) => AAtom u1
45881
3be79bdcc702 fixed parsing of TPTP atoms
blanchet
parents: 45551
diff changeset
   370
        | (u1, SOME (neg, u2)) =>
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48130
diff changeset
   371
          AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   372
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   373
(* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   374
fun parse_fol_literal x =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   375
  ((Scan.repeat ($$ tptp_not) >> length)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   376
      -- ($$ "(" |-- parse_fol_formula --| $$ ")"
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   377
          || parse_fol_quantified_formula
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   378
          || parse_fol_atom)
42605
8734eb0033b3 Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly
blanchet
parents: 42603
diff changeset
   379
      >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   380
and parse_fol_formula x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   381
  (parse_fol_literal
43163
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   382
   -- Scan.option ((Scan.this_string tptp_implies
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   383
                    || Scan.this_string tptp_iff
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   384
                    || Scan.this_string tptp_not_iff
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   385
                    || Scan.this_string tptp_if
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   386
                    || $$ tptp_or
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   387
                    || $$ tptp_and) -- parse_fol_formula)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   388
   >> (fn (phi1, NONE) => phi1
43163
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   389
        | (phi1, SOME (c, phi2)) =>
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   390
          if c = tptp_implies then mk_aconn AImplies phi1 phi2
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   391
          else if c = tptp_iff then mk_aconn AIff phi1 phi2
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   392
          else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2)
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   393
          else if c = tptp_if then mk_aconn AImplies phi2 phi1
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   394
          else if c = tptp_or then mk_aconn AOr phi1 phi2
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   395
          else if c = tptp_and then mk_aconn AAnd phi1 phi2
31babd4b1552 killed odd connectives
blanchet
parents: 43085
diff changeset
   396
          else raise Fail ("impossible connective " ^ quote c))) x
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   397
and parse_fol_quantified_formula x =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   398
  (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   399
   --| $$ "[" -- parse_fol_terms --| $$ "]" --| $$ ":" -- parse_fol_literal
61030
aeb578badc1c robust handling of Vampire 4 proofs
blanchet
parents: 59577
diff changeset
   400
   >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   401
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   402
val parse_tstp_extra_arguments =
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   403
  Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) NONE
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   404
47927
c35238d19bb9 repair the Waldmeister endgame only for Waldmeister proofs
blanchet
parents: 47926
diff changeset
   405
val waldmeister_conjecture_name = "conjecture_1"
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   406
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   407
fun is_same_term subst tm1 tm2 =
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   408
  let
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   409
    fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2))
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   410
          (SOME subst) =
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   411
        if typ1 <> typ2 andalso length args1 = length args2 then NONE
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   412
        else
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   413
          let val ls = length subst in
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   414
            SOME ((var1, var2) :: subst)
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   415
            |> do_term_pair body1 body2
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   416
            |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst)
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   417
                 | NONE => NONE)
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   418
            |> (if length args1 = length args2
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   419
              then fold2 do_term_pair args1 args2
57258
67d85a8aa6cc Moving the remote prefix deleting on Sledgehammer's side
fleury
parents: 57257
diff changeset
   420
              else K NONE)
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   421
          end
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   422
      | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58654
diff changeset
   423
        (case apply2 is_tptp_variable (s1, s2) of
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   424
          (true, true) =>
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   425
          (case AList.lookup (op =) subst s1 of
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   426
            SOME s2' => if s2' = s2 then SOME subst else NONE
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   427
          | NONE =>
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   428
            if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst)
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   429
            else NONE)
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   430
        | (false, false) =>
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   431
          if s1 = s2 then
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   432
            SOME subst
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   433
          else
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   434
            NONE
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   435
        | _ => NONE) |> (if length args1 = length args2
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   436
                       then fold2 do_term_pair args1 args2
57258
67d85a8aa6cc Moving the remote prefix deleting on Sledgehammer's side
fleury
parents: 57257
diff changeset
   437
                       else K NONE)
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   438
      | do_term_pair _ _ _ = NONE
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   439
  in
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   440
    SOME subst |> do_term_pair tm1 tm2 |> is_some
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   441
  end
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   442
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   443
fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   444
    q1 = q2 andalso length xs1 = length xs2 andalso
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   445
    is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   446
  | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   447
    c1 = c2 andalso length phis1 = length phis2 andalso
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   448
    forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
57202
blanchet
parents: 57154
diff changeset
   449
  | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
47926
c6d5418ee770 fixed Waldmeister commutativity hack
blanchet
parents: 47921
diff changeset
   450
    is_same_term subst tm1 tm2 orelse
54799
blanchet
parents: 54788
diff changeset
   451
    (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2)
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   452
  | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   453
  | is_same_formula _ _ _ _ = false
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   454
50521
bec828f3364e generate comments with original names for debugging
blanchet
parents: 50236
diff changeset
   455
fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) =
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   456
    if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   457
  | matching_formula_line_identifier _ _ = NONE
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   458
54799
blanchet
parents: 54788
diff changeset
   459
fun find_formula_in_problem phi =
blanchet
parents: 54788
diff changeset
   460
  maps snd
blanchet
parents: 54788
diff changeset
   461
  #> map_filter (matching_formula_line_identifier phi)
blanchet
parents: 54788
diff changeset
   462
  #> try (single o hd)
blanchet
parents: 54788
diff changeset
   463
  #> the_default []
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   464
54799
blanchet
parents: 54788
diff changeset
   465
fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms))
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47927
diff changeset
   466
  | commute_eq _ = raise Fail "expected equation"
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   467
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   468
fun role_of_tptp_string "axiom" = Axiom
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   469
  | role_of_tptp_string "definition" = Definition
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   470
  | role_of_tptp_string "lemma" = Lemma
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   471
  | role_of_tptp_string "hypothesis" = Hypothesis
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   472
  | role_of_tptp_string "conjecture" = Conjecture
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   473
  | role_of_tptp_string "negated_conjecture" = Negated_Conjecture
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   474
  | role_of_tptp_string "plain" = Plain
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   475
  | role_of_tptp_string "type" = Type_Role
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   476
  | role_of_tptp_string _ = Unknown
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 50011
diff changeset
   477
57697
44341963ade3 correctly translate THF functions from terms to types
blanchet
parents: 57656
diff changeset
   478
val tptp_binary_ops =
73972
b304285fd800 parse logical operators in the right order w.r.t. backtracking
blanchet
parents: 73971
diff changeset
   479
  [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and,
b304285fd800 parse logical operators in the right order w.r.t. backtracking
blanchet
parents: 73971
diff changeset
   480
   tptp_not_or, tptp_not_iff, tptp_app]
57256
cf43583f9bb9 imported patch leo2_skolem_simplication
fleury
parents: 57255
diff changeset
   481
57714
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
   482
fun parse_one_in_list xs =
4856a7b8b9c3 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents: 57709
diff changeset
   483
  foldl1 (op ||) (map Scan.this_string xs)
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   484
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   485
fun parse_binary_op x =
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   486
  (parse_one_in_list tptp_binary_ops
57697
44341963ade3 correctly translate THF functions from terms to types
blanchet
parents: 57656
diff changeset
   487
   >> (fn c => if c = tptp_equal then "equal" else c)) x
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   488
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   489
val parse_fol_quantifier =
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   490
   parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the]
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   491
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   492
val parse_hol_quantifier =
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   493
   parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the]
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   494
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   495
fun mk_ho_of_fo_quant q =
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   496
  if q = tptp_forall then tptp_ho_forall
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   497
  else if q = tptp_exists then tptp_ho_exists
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   498
  else if q = tptp_hilbert_choice then tptp_hilbert_choice
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57707
diff changeset
   499
  else if q = tptp_hilbert_the then tptp_hilbert_the
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   500
  else raise Fail ("unrecognized quantification: " ^ q)
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   501
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   502
fun remove_hol_app (ATerm ((x, ty), arg)) =
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   503
    if x = tptp_app then
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   504
      (case arg of
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   505
        ATerm ((x, ty), arg) :: t => remove_hol_app (ATerm ((x, ty), map remove_hol_app arg @ t))
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   506
      | [AAbs ((var, tvar), phi), t] =>
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   507
        remove_hol_app (AAbs ((var, tvar), map remove_hol_app phi @ [t])))
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   508
    else
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   509
      ATerm ((x, ty), map remove_hol_app arg)
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   510
  | remove_hol_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_hol_app arg), t)
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   511
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   512
fun parse_hol_typed_var x =
66428
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   513
  (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   514
     --| Scan.option (Scan.this_string ","))
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   515
   || $$ "(" |-- parse_hol_typed_var --| $$ ")") x
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   516
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   517
fun parse_simple_hol_term x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   518
  (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   519
      >> (fn ((q, ys), t) =>
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   520
          fold_rev
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   521
            (fn (var, ty) => fn r =>
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   522
                AAbs (((var, the_default dummy_atype ty), r), [])
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   523
                |> (if tptp_lambda <> q then
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   524
                      mk_app (q |> mk_ho_of_fo_quant
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   525
                                |> mk_simple_aterm)
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   526
                    else I))
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   527
            ys t)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   528
  || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not)
66428
745a43ff2d5f extended TSTP type parser + tuned messages
blanchet
parents: 63692
diff changeset
   529
  || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   530
    >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   531
  || parse_hol_quantifier >> mk_simple_aterm
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   532
  || $$ "(" |-- parse_hol_term --| $$ ")"
58324
65651cb9d191 correction in the thf0 parser ("(=)" found in a Satallax proof).
fleury
parents: 58091
diff changeset
   533
  || parse_binary_op >> mk_simple_aterm) x
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   534
and parse_hol_term x =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   535
  (parse_simple_hol_term -- Scan.option (parse_binary_op -- parse_hol_term)
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   536
    >> (fn (t1, SOME (c, t2)) =>
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   537
           if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2]
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   538
         | (t, NONE) => t)) x
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   539
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   540
fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   541
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   542
fun parse_tstp_hol_line problem =
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   543
  (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ ","
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   544
  -- Symbol.scan_ascii_id --| $$ "," -- (parse_hol_formula || skip_term >> K dummy_phi)
67022
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   545
     -- parse_tstp_extra_arguments --| $$ ")"
61329
426c9c858099 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents: 61030
diff changeset
   546
  --| $$ "."
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   547
  >> (fn (((num, role), phi), src) =>
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   548
      let
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   549
        val role' = role_of_tptp_string role
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   550
        val ((name, phi), rule, deps) =
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   551
          (case src of
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   552
            SOME (File_Source (_, SOME s)) =>
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   553
            if role' = Definition then
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   554
              (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   555
            else
70935
535ff1eac86c removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
blanchet
parents: 70934
diff changeset
   556
              (((num, [s]), phi), "", [])
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   557
          | SOME (Inference_Source (rule, deps)) => (((num, []), phi), rule, deps)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   558
          | SOME (Introduced_Source rule) => (((num, []), phi), rule, [])
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   559
          | _ => (((num, [num]), phi), "", []))
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   560
      in
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   561
        [(name, role', phi, rule, map (rpair []) deps)]
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   562
      end)
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   563
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   564
fun parse_tstp_fol_line problem =
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   565
  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
50236
476a3350589c clarified Symbol.scan_ascii_id;
wenzelm
parents: 50012
diff changeset
   566
    |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   567
    -- (parse_fol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
45235
7187bce94e88 more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents: 45209
diff changeset
   568
    --| $$ ")" --| $$ "."
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   569
   >> (fn (((num, role0), phi), src) =>
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   570
          let
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   571
            val role = role_of_tptp_string role0
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   572
            val ((name, phi), role', rule, deps) =
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   573
              (* Waldmeister isn't exactly helping. *)
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   574
              (case src of
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   575
                SOME (File_Source (_, SOME s)) =>
47927
c35238d19bb9 repair the Waldmeister endgame only for Waldmeister proofs
blanchet
parents: 47926
diff changeset
   576
                (if s = waldmeister_conjecture_name then
54799
blanchet
parents: 54788
diff changeset
   577
                   (case find_formula_in_problem (mk_anot phi) problem of
57202
blanchet
parents: 57154
diff changeset
   578
                     (* Waldmeister hack: Get the original orientation of the equation to avoid
blanchet
parents: 57154
diff changeset
   579
                        confusing Isar. *)
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   580
                     [(s, phi')] =>
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   581
                     ((num, [s]),
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   582
                      phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   583
                   | _ => ((num, []), phi))
47921
fc26d5538868 ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents: 47917
diff changeset
   584
                 else
70935
535ff1eac86c removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
blanchet
parents: 70934
diff changeset
   585
                   ((num, [s]), phi),
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   586
                 role, "", [])
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   587
              | SOME (File_Source _) =>
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   588
                (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   589
              | SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps)
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   590
              | SOME (Introduced_Source rule) => (((num, []), phi), Lemma, rule, [])
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   591
              | _ => (((num, [num]), phi), role, "", []))
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   592
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   593
            fun mk_step () = (name, role', phi, rule, map (rpair []) deps)
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   594
          in
57785
0388026060d1 deal with E definitions
blanchet
parents: 57716
diff changeset
   595
            [(case role' of
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   596
               Definition =>
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   597
               (case phi of
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 57215
diff changeset
   598
                 AAtom (ATerm (("equal", _), _)) =>
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   599
                  (* Vampire's equality proxy axiom *)
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   600
                  (name, Definition, phi, rule, map (rpair []) deps)
57257
0d5e34ba4d28 Correcting the type parser
fleury
parents: 57256
diff changeset
   601
               | _ => mk_step ())
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   602
             | _ => mk_step ())]
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42882
diff changeset
   603
          end)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   604
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   605
fun parse_tstp_line problem = parse_tstp_fol_line problem || parse_tstp_hol_line problem
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   606
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   607
(**** PARSING OF SPASS OUTPUT ****)
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   608
57786
1f0efb4974fc tuned comments
blanchet
parents: 57785
diff changeset
   609
(* SPASS returns clause references of the form "x.y". We ignore "y". *)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   610
val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   611
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   612
val parse_spass_annotations =
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   613
  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   614
57786
1f0efb4974fc tuned comments
blanchet
parents: 57785
diff changeset
   615
(* We ignore the stars and the pluses that follow literals. *)
39602
ae2c3059f8cc make SML/NJ happier
blanchet
parents: 39598
diff changeset
   616
fun parse_decorated_atom x =
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   617
  (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   618
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48130
diff changeset
   619
fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
58091
ecf5826ba234 reworked unskolemization for SPASS
blanchet
parents: 58080
diff changeset
   620
  | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   621
39645
6eb38a00ae47 make SML/NJ happy
blanchet
parents: 39602
diff changeset
   622
fun parse_horn_clause x =
6eb38a00ae47 make SML/NJ happy
blanchet
parents: 39602
diff changeset
   623
  (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
6eb38a00ae47 make SML/NJ happy
blanchet
parents: 39602
diff changeset
   624
     -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
6eb38a00ae47 make SML/NJ happy
blanchet
parents: 39602
diff changeset
   625
     -- Scan.repeat parse_decorated_atom
6eb38a00ae47 make SML/NJ happy
blanchet
parents: 39602
diff changeset
   626
   >> (mk_horn o apfst (op @))) x
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   627
46390
6467c99c4872 don't stumble on SPASS debug output
blanchet
parents: 45881
diff changeset
   628
val parse_spass_debug =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   629
  Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")")
46390
6467c99c4872 don't stumble on SPASS debug output
blanchet
parents: 45881
diff changeset
   630
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   631
(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms> .
46427
4fd25dadbd94 cleaned up new SPASS parsing
blanchet
parents: 46390
diff changeset
   632
           derived from formulae <ident>* *)
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 47972
diff changeset
   633
fun parse_spass_line x =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   634
  (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":"
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   635
     -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 47972
diff changeset
   636
     -- Scan.option (Scan.this_string "derived from formulae "
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 47972
diff changeset
   637
                     |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 47972
diff changeset
   638
   >> (fn ((((num, rule), deps), u), names) =>
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   639
          [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
45162
170dffc6df75 parse Satallax unsat cores
blanchet
parents: 44915
diff changeset
   640
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   641
fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   642
fun parse_pirate_dependencies x =
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   643
  Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   644
fun parse_pirate_file_source x =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   645
  ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   646
     --| $$ ")") x
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   647
fun parse_pirate_inference_source x =
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   648
  (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   649
fun parse_pirate_source x =
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   650
  (parse_pirate_file_source >> (fn s => File_Source ("", SOME s))
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   651
   || parse_pirate_inference_source >> Inference_Source) x
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   652
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   653
(* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   654
fun parse_pirate_line x =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   655
  (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   656
     --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")"
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   657
   >> (fn ((((num, u), source))) =>
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   658
     let
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   659
       val (names, rule, deps) =
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   660
         (case source of
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   661
           File_Source (_, SOME s) => ([s], spass_input_rule, [])
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   662
         | Inference_Source (rule, deps) => ([], rule, deps))
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   663
     in
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   664
       [((num, names), Unknown, u, rule, map (rpair []) deps)]
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   665
     end)) x
48539
0debf65972c7 extract Z3 unsat cores (for "z3_tptp")
blanchet
parents: 48316
diff changeset
   666
52077
788b27dfaefa parse agsyHOL proofs (as unsat cores)
blanchet
parents: 52073
diff changeset
   667
fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
788b27dfaefa parse agsyHOL proofs (as unsat cores)
blanchet
parents: 52073
diff changeset
   668
56404
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   669
(* Syntax: SZS core <name> ... <name> *)
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   670
fun parse_z3_tptp_core_line x =
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   671
  (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
9cb137ec6ec8 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
blanchet
parents: 56397
diff changeset
   672
   >> map (core_inference z3_tptp_core_rule)) x
43481
51857e7fa64b clean up SPASS FLOTTER hack
blanchet
parents: 43473
diff changeset
   673
57258
67d85a8aa6cc Moving the remote prefix deleting on Sledgehammer's side
fleury
parents: 57257
diff changeset
   674
fun parse_line local_name problem =
67022
49309fe530fd more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
blanchet
parents: 67021
diff changeset
   675
  (* Satallax is handled separately, in "atp_satallax.ML". *)
72398
5d1a7b688f6d recognize THF proofs properly
desharna
parents: 72355
diff changeset
   676
  if local_name = spassN then parse_spass_line
59577
012c6165bbd2 SPASS-Pirate is now called Pirate
blanchet
parents: 59058
diff changeset
   677
  else if local_name = pirateN then parse_pirate_line
57258
67d85a8aa6cc Moving the remote prefix deleting on Sledgehammer's side
fleury
parents: 57257
diff changeset
   678
  else if local_name = z3_tptpN then parse_z3_tptp_core_line
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   679
  else parse_tstp_line problem
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57017
diff changeset
   680
52077
788b27dfaefa parse agsyHOL proofs (as unsat cores)
blanchet
parents: 52073
diff changeset
   681
fun core_of_agsyhol_proof s =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   682
  (case split_lines s of
52077
788b27dfaefa parse agsyHOL proofs (as unsat cores)
blanchet
parents: 52073
diff changeset
   683
    "The transformed problem consists of the following conjectures:" :: conj ::
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   684
    _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54772
diff changeset
   685
  | _ => NONE)
52077
788b27dfaefa parse agsyHOL proofs (as unsat cores)
blanchet
parents: 52073
diff changeset
   686
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   687
fun clean_up_dependencies _ [] = []
51201
f176855a1ee2 tuning (removed redundant datatype)
blanchet
parents: 51198
diff changeset
   688
  | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   689
    (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   690
    clean_up_dependencies (name :: seen) steps
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
   691
42975
284f9a7af1c9 eta-expand to make SML/NJ happy
blanchet
parents: 42973
diff changeset
   692
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   693
50704
cd1fcda1ea88 rename variable in binder, not just in body
blanchet
parents: 50590
diff changeset
   694
fun map_term_names_in_atp_proof f =
cd1fcda1ea88 rename variable in binder, not just in body
blanchet
parents: 50590
diff changeset
   695
  let
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54811
diff changeset
   696
    fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys)
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   697
      | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   698
      | map_type (APi (ss, ty)) = APi (map f ss, map_type ty)
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   699
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   700
    fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts)
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   701
      | map_term (AAbs (((s, ty), tm), args)) =
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   702
        AAbs (((f s, map_type ty), map_term tm), map map_term args)
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   703
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   704
    fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi)
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   705
      | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis)
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   706
      | map_formula (AAtom t) = AAtom (map_term t)
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   707
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 55192
diff changeset
   708
    fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps)
54811
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   709
  in
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   710
    map map_step
df56a01f5684 parse SPASS-Pirate types
blanchet
parents: 54803
diff changeset
   711
  end
39454
acb25e9cf6fb factor out the inverse of "nice_atp_problem"
blanchet
parents: 39453
diff changeset
   712
57261
49c1db0313e6 give Z3 TPTP proofs a chance
blanchet
parents: 57258
diff changeset
   713
fun nasty_name pool s = Symtab.lookup pool s |> the_default s
50704
cd1fcda1ea88 rename variable in binder, not just in body
blanchet
parents: 50590
diff changeset
   714
39454
acb25e9cf6fb factor out the inverse of "nice_atp_problem"
blanchet
parents: 39453
diff changeset
   715
fun nasty_atp_proof pool =
50704
cd1fcda1ea88 rename variable in binder, not just in body
blanchet
parents: 50590
diff changeset
   716
  not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
39454
acb25e9cf6fb factor out the inverse of "nice_atp_problem"
blanchet
parents: 39453
diff changeset
   717
72355
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   718
fun string_of_list f xs = enclose "[" "]" (commas (map f xs))
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   719
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   720
fun string_of_atp_step_name (s, ss) = "(" ^ s ^ ", " ^ string_of_list I ss ^ ")"
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   721
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   722
fun string_of_atp_step f g (name, role, x, y, names) =
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   723
  let
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   724
    val name' = string_of_atp_step_name name
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   725
    val role' = ATP_Problem.tptp_string_of_role role
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   726
    val x' = f x
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   727
    val y' = g y
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   728
    val names' = string_of_list string_of_atp_step_name names
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   729
  in
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   730
    "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")"
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   731
  end
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 70939
diff changeset
   732
72399
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   733
fun parse_proof local_name problem =
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   734
  strip_spaces_except_between_idents
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   735
  #> raw_explode
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   736
  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   737
       (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem))))
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   738
  #> fst
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   739
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   740
fun atp_proof_of_tstplike_proof _ _ "" = []
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   741
  | atp_proof_of_tstplike_proof local_prover problem tstp =
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   742
    (case core_of_agsyhol_proof tstp of
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   743
      SOME facts => facts |> map (core_inference agsyhol_core_rule)
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   744
    | NONE =>
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   745
      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   746
      |> parse_proof local_prover problem
72967
11de287ed481 tweaked tptp parsing when source info is missing
desharna
parents: 72689
diff changeset
   747
      |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))))
72399
f8900a5ad4a7 drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents: 72398
diff changeset
   748
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents:
diff changeset
   749
end;