src/HOL/Tools/ATP/atp_problem.ML
author desharna
Thu, 05 Aug 2021 17:43:16 +0200
changeset 74393 b9837b07684d
parent 74339 a5bab59d580b
child 74433 304f22435bc7
permissions -rw-r--r--
fixed $ite syntax in TPTP THX generation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38047
9033c03cc214 consequence of directory renaming
blanchet
parents: 38046
diff changeset
     1
(*  Title:      HOL/Tools/ATP/atp_problem.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38025
diff changeset
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     4
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39384
diff changeset
     5
Abstract representation of ATP problems and TPTP syntax.
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     6
*)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     7
38019
e207a64e1e0b complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
blanchet
parents: 38018
diff changeset
     8
signature ATP_PROBLEM =
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
     9
sig
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    10
  datatype ('a, 'b) atp_term =
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    11
    ATerm of ('a * 'b list) * ('a, 'b) atp_term list |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    12
    AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    13
  datatype atp_quantifier = AForall | AExists
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    14
  datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    15
  datatype ('a, 'b, 'c, 'd) atp_formula =
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    16
    ATyQuant of atp_quantifier * ('b * 'd list) list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    17
        * ('a, 'b, 'c, 'd) atp_formula |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    18
    AQuant of atp_quantifier * ('a * 'b option) list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    19
        * ('a, 'b, 'c, 'd) atp_formula |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    20
    AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list |
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    21
    AAtom of 'c
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37993
diff changeset
    22
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    23
  datatype 'a atp_type =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
    24
    AType of ('a * 'a list) * 'a atp_type list |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    25
    AFun of 'a atp_type * 'a atp_type |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    26
    APi of 'a list * 'a atp_type
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
    27
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    28
  type term_order =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    29
    {is_lpo : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    30
     gen_weights : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    31
     gen_prec : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    32
     gen_simp : bool}
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
    33
72824
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72588
diff changeset
    34
  datatype fool = Without_FOOL | With_FOOL
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
    35
  datatype polymorphism = Monomorphic | Polymorphic
73155
e05b77e1ab21 proper parsing of type encoding;
desharna
parents: 73154
diff changeset
    36
  datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
    37
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
    38
  datatype atp_format =
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
    39
    CNF |
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
    40
    CNF_UEQ |
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
    41
    FOF |
72824
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72588
diff changeset
    42
    TFF of fool * polymorphism |
72893
febfb98d0941 renamed data type
desharna
parents: 72877
diff changeset
    43
    THF of fool * polymorphism * thf_flavor |
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
    44
    DFG of polymorphism
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
    45
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    46
  datatype atp_formula_role =
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 48438
diff changeset
    47
    Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
    48
    Plain | Type_Role | Unknown
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 48438
diff changeset
    49
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    50
  datatype 'a atp_problem_line =
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
    51
    Class_Decl of string * 'a * 'a list |
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
    52
    Type_Decl of string * 'a * int |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    53
    Sym_Decl of string * 'a * 'a atp_type |
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
    54
    Datatype_Decl of
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
    55
      string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    56
    Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    57
    Formula of (string * string) * atp_formula_role
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    58
               * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    59
               * (string, string atp_type) atp_term option
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    60
               * (string, string atp_type) atp_term list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
    61
  type 'a atp_problem = (string * 'a atp_problem_line list) list
37992
7911e78a7122 renamed internal function
blanchet
parents: 37962
diff changeset
    62
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    63
  val tptp_cnf : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    64
  val tptp_fof : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    65
  val tptp_tff : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    66
  val tptp_thf : string
42967
blanchet
parents: 42966
diff changeset
    67
  val tptp_has_type : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
    68
  val tptp_type_of_types : string
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
    69
  val tptp_bool_type : string
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
    70
  val tptp_individual_type : string
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
    71
  val tptp_fun_type : string
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
    72
  val tptp_product_type : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    73
  val tptp_forall : string
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
    74
  val tptp_ho_forall : string
44650
dbdfadbd3829 use new syntax for Pi binder in TFF1 output
blanchet
parents: 44620
diff changeset
    75
  val tptp_pi_binder : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    76
  val tptp_exists : string
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
    77
  val tptp_ho_exists : string
44495
4c2242c8a96c added choice operator output for
nik
parents: 44407
diff changeset
    78
  val tptp_choice : string
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
    79
  val tptp_ho_choice : string
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57300
diff changeset
    80
  val tptp_hilbert_choice : string
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57300
diff changeset
    81
  val tptp_hilbert_the : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    82
  val tptp_not : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    83
  val tptp_and : string
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
    84
  val tptp_not_and : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    85
  val tptp_or : string
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
    86
  val tptp_not_or : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    87
  val tptp_implies : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    88
  val tptp_if : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    89
  val tptp_iff : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    90
  val tptp_not_iff : string
74115
bc263f1f68cd added support for TFX's and THF's $ite to Sledgehammer
desharna
parents: 73157
diff changeset
    91
  val tptp_ite : string
74339
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
    92
  val tptp_let : string
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    93
  val tptp_app : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    94
  val tptp_not_infix : string
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
    95
  val tptp_equal : string
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
    96
  val tptp_not_equal : string
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
    97
  val tptp_old_equal : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    98
  val tptp_false : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    99
  val tptp_true : string
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   100
  val tptp_lambda : string
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   101
  val tptp_empty_list : string
73154
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   102
  val tptp_unary_builtins : string list
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   103
  val tptp_binary_builtins : string list
58600
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 57811
diff changeset
   104
  val dfg_individual_type : string
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   105
  val isabelle_info_prefix : string
61862
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   106
  val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   107
  val extract_isabelle_status : (string, 'a) atp_term list -> string option
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   108
  val extract_isabelle_rank : (string, 'a) atp_term list -> int
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   109
  val inductionN : string
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   110
  val introN : string
47148
7b5846065c1b be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
blanchet
parents: 47146
diff changeset
   111
  val inductiveN : string
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   112
  val elimN : string
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   113
  val simpN : string
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   114
  val non_rec_defN : string
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   115
  val rec_defN : string
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   116
  val rankN : string
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   117
  val minimum_rank : int
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   118
  val default_rank : int
47030
7e80e14247fc internal renamings
blanchet
parents: 46643
diff changeset
   119
  val default_term_order_weight : int
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   120
  val is_tptp_equal : string -> bool
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   121
  val is_built_in_tptp_symbol : string -> bool
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   122
  val is_tptp_variable : string -> bool
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   123
  val is_tptp_user_symbol : string -> bool
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   124
  val bool_atype : (string * string) atp_type
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   125
  val individual_atype : (string * string) atp_type
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   126
  val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
42942
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   127
  val mk_aconn :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   128
    atp_connective -> ('a, 'b, 'c, 'd) atp_formula
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   129
    -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   130
  val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   131
  val mk_apps :  (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   132
  val mk_simple_aterm:  'a -> ('a, 'b) atp_term
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   133
  val aconn_fold :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   134
    bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   135
    -> 'b -> 'b
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   136
  val aconn_map :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   137
    bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula)
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   138
    -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   139
  val formula_fold :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   140
    bool option -> (bool option -> 'c -> 'e -> 'e)
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   141
    -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e
48135
a44f34694406 added sorts to datastructure
blanchet
parents: 48133
diff changeset
   142
  val formula_map :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   143
    ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   144
  val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
45303
bd03b08161ac added DFG unsorted support (like in the old days)
blanchet
parents: 45301
diff changeset
   145
  val is_format_higher_order : atp_format -> bool
61862
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   146
  val tptp_string_of_format : atp_format -> string
72588
1f959abe99d5 Add more tacing to sledgehammer_isar_trace
desharna
parents: 69733
diff changeset
   147
  val tptp_string_of_role : atp_formula_role -> string
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   148
  val tptp_string_of_line : atp_format -> string atp_problem_line -> string
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   149
  val lines_of_atp_problem :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   150
    atp_format -> term_order -> (unit -> (string * int) list)
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   151
    -> string atp_problem -> string list
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   152
  val ensure_cnf_problem :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   153
    (string * string) atp_problem -> (string * string) atp_problem
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   154
  val filter_cnf_ueq_problem :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   155
    (string * string) atp_problem -> (string * string) atp_problem
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   156
  val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39384
diff changeset
   157
  val nice_atp_problem :
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   158
    bool -> atp_format -> ('a * (string * string) atp_problem_line list) list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   159
    -> ('a * string atp_problem_line list) list
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38014
diff changeset
   160
       * (string Symtab.table * string Symtab.table) option
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   161
end;
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   162
38019
e207a64e1e0b complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
blanchet
parents: 38018
diff changeset
   163
structure ATP_Problem : ATP_PROBLEM =
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   164
struct
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
   165
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43000
diff changeset
   166
open ATP_Util
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43000
diff changeset
   167
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   168
val parens = enclose "(" ")"
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   169
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   170
(** ATP problem **)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   171
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   172
datatype ('a, 'b) atp_term =
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   173
  ATerm of ('a * 'b list) * ('a, 'b) atp_term list |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   174
  AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   175
datatype atp_quantifier = AForall | AExists
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   176
datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   177
datatype ('a, 'b, 'c, 'd) atp_formula =
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   178
  ATyQuant of atp_quantifier * ('b * 'd list) list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   179
      * ('a, 'b, 'c, 'd) atp_formula |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   180
  AQuant of atp_quantifier * ('a * 'b option) list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   181
      * ('a, 'b, 'c, 'd) atp_formula |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   182
  AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list |
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   183
  AAtom of 'c
37961
6a48c85a211a first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents: 37931
diff changeset
   184
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   185
datatype 'a atp_type =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   186
  AType of ('a * 'a list) * 'a atp_type list |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   187
  AFun of 'a atp_type * 'a atp_type |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   188
  APi of 'a list * 'a atp_type
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   189
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   190
type term_order =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   191
  {is_lpo : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   192
   gen_weights : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   193
   gen_prec : bool,
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   194
   gen_simp : bool}
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   195
72824
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72588
diff changeset
   196
datatype fool = Without_FOOL | With_FOOL
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   197
datatype polymorphism = Monomorphic | Polymorphic
73155
e05b77e1ab21 proper parsing of type encoding;
desharna
parents: 73154
diff changeset
   198
datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
44499
8870232a87ad make TFF output less explicit where possible
blanchet
parents: 44495
diff changeset
   199
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   200
datatype atp_format =
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
   201
  CNF |
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
   202
  CNF_UEQ |
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
   203
  FOF |
72824
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72588
diff changeset
   204
  TFF of fool * polymorphism |
72893
febfb98d0941 renamed data type
desharna
parents: 72877
diff changeset
   205
  THF of fool * polymorphism * thf_flavor |
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   206
  DFG of polymorphism
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
   207
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   208
datatype atp_formula_role =
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 48438
diff changeset
   209
  Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   210
  Plain | Type_Role | Unknown
50012
01cb92151a53 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents: 48438
diff changeset
   211
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   212
datatype 'a atp_problem_line =
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   213
  Class_Decl of string * 'a * 'a list |
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   214
  Type_Decl of string * 'a * int |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   215
  Sym_Decl of string * 'a * 'a atp_type |
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   216
  Datatype_Decl of
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   217
    string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   218
  Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   219
  Formula of (string * string) * atp_formula_role
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   220
             * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   221
             * (string, string atp_type) atp_term option
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   222
             * (string, string atp_type) atp_term list
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 52995
diff changeset
   223
type 'a atp_problem = (string * 'a atp_problem_line list) list
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   224
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   225
(* official TPTP syntax *)
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   226
val tptp_cnf = "cnf"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   227
val tptp_fof = "fof"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   228
val tptp_tff = "tff"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   229
val tptp_thf = "thf"
42967
blanchet
parents: 42966
diff changeset
   230
val tptp_has_type = ":"
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   231
val tptp_type_of_types = "$tType"
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   232
val tptp_bool_type = "$o"
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   233
val tptp_individual_type = "$i"
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   234
val tptp_fun_type = ">"
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   235
val tptp_product_type = "*"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   236
val tptp_forall = "!"
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   237
val tptp_ho_forall = "!!"
44650
dbdfadbd3829 use new syntax for Pi binder in TFF1 output
blanchet
parents: 44620
diff changeset
   238
val tptp_pi_binder = "!>"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   239
val tptp_exists = "?"
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   240
val tptp_ho_exists = "??"
44495
4c2242c8a96c added choice operator output for
nik
parents: 44407
diff changeset
   241
val tptp_choice = "@+"
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   242
val tptp_ho_choice = "@@+"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   243
val tptp_not = "~"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   244
val tptp_and = "&"
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   245
val tptp_not_and = "~&"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   246
val tptp_or = "|"
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   247
val tptp_not_or = "~|"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   248
val tptp_implies = "=>"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   249
val tptp_if = "<="
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   250
val tptp_iff = "<=>"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   251
val tptp_not_iff = "<~>"
74115
bc263f1f68cd added support for TFX's and THF's $ite to Sledgehammer
desharna
parents: 73157
diff changeset
   252
val tptp_ite = "$ite"
74339
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   253
val tptp_let = "$let"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   254
val tptp_app = "@"
57709
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57300
diff changeset
   255
val tptp_hilbert_choice = "@+"
9cda0c64c37a imported patch hilbert_choice_support
fleury
parents: 57300
diff changeset
   256
val tptp_hilbert_the = "@-"
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   257
val tptp_not_infix = "!"
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   258
val tptp_equal = "="
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   259
val tptp_not_equal = "!="
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   260
val tptp_old_equal = "equal"
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   261
val tptp_false = "$false"
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   262
val tptp_true = "$true"
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   263
val tptp_lambda = "^"
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   264
val tptp_empty_list = "[]"
58600
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 57811
diff changeset
   265
73154
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   266
val tptp_unary_builtins = [tptp_not]
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   267
val tptp_binary_builtins =
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   268
  [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   269
58600
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 57811
diff changeset
   270
val dfg_individual_type = "iii" (* cannot clash *)
c9e8ad426ab1 get rid of 'individual' type in DFG proofs
blanchet
parents: 57811
diff changeset
   271
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   272
val isabelle_info_prefix = "isabelle_"
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   273
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   274
val inductionN = "induction"
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   275
val introN = "intro"
47148
7b5846065c1b be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
blanchet
parents: 47146
diff changeset
   276
val inductiveN = "inductive"
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   277
val elimN = "elim"
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   278
val simpN = "simp"
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   279
val non_rec_defN = "non_rec_def"
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   280
val rec_defN = "rec_def"
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   281
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   282
val rankN = "rank"
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   283
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   284
val minimum_rank = 0
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   285
val default_rank = 1000
47030
7e80e14247fc internal renamings
blanchet
parents: 46643
diff changeset
   286
val default_term_order_weight = 1
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   287
61862
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   288
(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   289
   metainformation. *)
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   290
fun isabelle_info generate_info status rank =
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   291
  if generate_info then
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   292
    [] |> rank <> default_rank
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   293
          ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   294
                         [ATerm ((string_of_int rank, []), [])]))
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   295
       |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   296
  else
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   297
    []
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   298
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   299
fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   300
    try (unprefix isabelle_info_prefix) s
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   301
  | extract_isabelle_status _ = NONE
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   302
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   303
fun extract_isabelle_rank (tms as _ :: _) =
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   304
    (case List.last tms of
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   305
       ATerm ((_, []), [ATerm ((rank, []), [])]) => the (Int.fromString rank)
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   306
     | _ => default_rank)
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   307
  | extract_isabelle_rank _ = default_rank
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   308
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   309
fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal)
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   310
fun is_built_in_tptp_symbol s =
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   311
  s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0)))
51878
f11039b31bae handle dummy atp terms
smolkas
parents: 51646
diff changeset
   312
fun is_tptp_variable s = s <> "" andalso Char.isUpper (String.sub (s, 0))
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   313
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   314
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   315
val bool_atype = AType ((`I tptp_bool_type, []), [])
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   316
val individual_atype = AType ((`I tptp_individual_type, []), [])
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   317
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   318
fun raw_polarities_of_conn ANot = (SOME false, NONE)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   319
  | raw_polarities_of_conn AAnd = (SOME true, SOME true)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   320
  | raw_polarities_of_conn AOr = (SOME true, SOME true)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   321
  | raw_polarities_of_conn AImplies = (SOME false, SOME true)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   322
  | raw_polarities_of_conn AIff = (NONE, NONE)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   323
fun polarities_of_conn NONE = K (NONE, NONE)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   324
  | polarities_of_conn (SOME pos) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58600
diff changeset
   325
    raw_polarities_of_conn #> not pos ? apply2 (Option.map not)
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   326
42942
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   327
fun mk_anot (AConn (ANot, [phi])) = phi
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   328
  | mk_anot phi = AConn (ANot, [phi])
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   329
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   330
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   331
fun mk_app t u = ATerm ((tptp_app, []), [t, u])
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   332
fun mk_apps f xs = fold (fn x => fn f => mk_app f x) xs f
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   333
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   334
fun mk_simple_aterm p = ATerm ((p, []), [])
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   335
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   336
fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   337
  | aconn_fold pos f (AImplies, [phi1, phi2]) =
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   338
    f (Option.map not pos) phi1 #> f pos phi2
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   339
  | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   340
  | aconn_fold pos f (AOr, phis) = fold (f pos) phis
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   341
  | aconn_fold _ f (_, phis) = fold (f NONE) phis
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   342
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   343
fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   344
  | aconn_map pos f (AImplies, [phi1, phi2]) =
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   345
    AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   346
  | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   347
  | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   348
  | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   349
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   350
fun formula_fold pos f =
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   351
  let
44501
5bde887b4785 make polymorphic encodings more complete
blanchet
parents: 44499
diff changeset
   352
    fun fld pos (AQuant (_, _, phi)) = fld pos phi
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   353
      | fld pos (ATyQuant (_, _, phi)) = fld pos phi
44501
5bde887b4785 make polymorphic encodings more complete
blanchet
parents: 44499
diff changeset
   354
      | fld pos (AConn conn) = aconn_fold pos fld conn
5bde887b4785 make polymorphic encodings more complete
blanchet
parents: 44499
diff changeset
   355
      | fld pos (AAtom tm) = f pos tm
5bde887b4785 make polymorphic encodings more complete
blanchet
parents: 44499
diff changeset
   356
  in fld pos end
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   357
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   358
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   359
  | formula_map f (ATyQuant (q, xs, phi)) = ATyQuant (q, xs, formula_map f phi)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   360
  | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   361
  | formula_map f (AAtom tm) = AAtom (f tm)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   362
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   363
fun strip_api (APi (tys, ty)) = strip_api ty |>> append tys
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   364
  | strip_api ty = ([], ty)
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   365
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   366
fun strip_afun (AFun (ty1, ty2)) = strip_afun ty2 |>> cons ty1
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   367
  | strip_afun ty = ([], ty)
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   368
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   369
fun strip_atype ty = ty |> strip_api ||> strip_afun
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   370
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   371
fun is_function_atype ty = snd (snd (strip_atype ty)) <> AType ((tptp_bool_type, []), [])
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   372
fun is_predicate_atype ty = not (is_function_atype ty)
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   373
fun is_nontrivial_predicate_atype (AType _) = false
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   374
  | is_nontrivial_predicate_atype ty = is_predicate_atype ty
46442
1e07620d724c added possibility of generating KBO weights to DFG problems
blanchet
parents: 46414
diff changeset
   375
45303
bd03b08161ac added DFG unsorted support (like in the old days)
blanchet
parents: 45301
diff changeset
   376
fun is_format_higher_order (THF _) = true
bd03b08161ac added DFG unsorted support (like in the old days)
blanchet
parents: 45301
diff changeset
   377
  | is_format_higher_order _ = false
44499
8870232a87ad make TFF output less explicit where possible
blanchet
parents: 44495
diff changeset
   378
fun is_format_typed (TFF _) = true
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44739
diff changeset
   379
  | is_format_typed (THF _) = true
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   380
  | is_format_typed (DFG _) = true
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 43987
diff changeset
   381
  | is_format_typed _ = false
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   382
72877
4eea17b3ac58 Tuned parentheses in TPTP output
desharna
parents: 72824
diff changeset
   383
fun is_format_with_fool (THF (With_FOOL, _, _)) = true
4eea17b3ac58 Tuned parentheses in TPTP output
desharna
parents: 72824
diff changeset
   384
  | is_format_with_fool (TFF (With_FOOL, _)) = true
4eea17b3ac58 Tuned parentheses in TPTP output
desharna
parents: 72824
diff changeset
   385
  | is_format_with_fool _ = false
4eea17b3ac58 Tuned parentheses in TPTP output
desharna
parents: 72824
diff changeset
   386
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   387
fun tptp_string_of_role Axiom = "axiom"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   388
  | tptp_string_of_role Definition = "definition"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   389
  | tptp_string_of_role Lemma = "lemma"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   390
  | tptp_string_of_role Hypothesis = "hypothesis"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   391
  | tptp_string_of_role Conjecture = "conjecture"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   392
  | tptp_string_of_role Negated_Conjecture = "negated_conjecture"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   393
  | tptp_string_of_role Plain = "plain"
57255
488046fdda59 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents: 56847
diff changeset
   394
  | tptp_string_of_role Type_Role = "type"
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   395
  | tptp_string_of_role Unknown = "unknown"
38631
979a0b37f981 prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents: 38613
diff changeset
   396
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   397
fun tptp_string_of_app _ func [] = func
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   398
  | tptp_string_of_app format func args =
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   399
    if is_format_higher_order format then
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   400
      "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   401
    else
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   402
      func ^ "(" ^ commas args ^ ")"
44787
3c0741556e19 fixed THF type constructor syntax
blanchet
parents: 44754
diff changeset
   403
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   404
fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty)
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   405
  | uncurry_type (ty as AFun (ty1 as AType _, ty2)) =
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   406
    (case uncurry_type ty2 of
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   407
       AFun (ty' as AType ((s, _), tys), ty) =>
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   408
       AFun (AType ((tptp_product_type, []),
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   409
         ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   410
     | _ => ty)
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   411
  | uncurry_type (ty as AType _) = ty
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   412
  | uncurry_type _ =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   413
    raise Fail "unexpected higher-order type in first-order format"
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   414
57267
8b87114357bd integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents: 57256
diff changeset
   415
val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   416
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   417
fun str_of_type format ty =
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   418
  let
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   419
    val dfg = (case format of DFG _ => true | _ => false)
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   420
    fun str _ (AType ((s, _), [])) =
46338
b02ff6b17599 better handling of individual type for DFG format (SPASS)
blanchet
parents: 46320
diff changeset
   421
        if dfg andalso s = tptp_individual_type then dfg_individual_type else s
61550
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   422
      | str rhs (AType ((s, _), tys)) =
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   423
        if s = tptp_fun_type then
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   424
          let val [ty1, ty2] = tys in
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   425
            str rhs (AFun (ty1, ty2))
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   426
          end
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   427
        else
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   428
          let val ss = tys |> map (str false) in
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   429
            if s = tptp_product_type then
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   430
              ss |> space_implode
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   431
                        (if dfg then ", " else " " ^ tptp_product_type ^ " ")
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   432
                 |> (not dfg andalso length ss > 1) ? parens
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   433
            else
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   434
              tptp_string_of_app format s ss
16e2313e855c make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
blanchet
parents: 59058
diff changeset
   435
          end
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   436
      | str rhs (AFun (ty1, ty2)) =
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   437
        (str false ty1 |> dfg ? parens) ^ " " ^
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   438
        (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   439
        |> not rhs ? parens
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   440
      | str _ (APi (ss, ty)) =
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   441
        if dfg then
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   442
          "[" ^ commas ss ^ "], " ^ str true ty
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   443
        else
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   444
          tptp_pi_binder ^ "[" ^ commas (map suffix_type_of_types ss) ^ "]: " ^
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   445
          str false ty
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   446
  in str true ty end
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   447
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   448
fun string_of_type (format as THF _) ty = str_of_type format ty
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   449
  | string_of_type format ty = str_of_type format (uncurry_type ty)
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   450
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   451
fun tptp_string_of_quantifier AForall = tptp_forall
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   452
  | tptp_string_of_quantifier AExists = tptp_exists
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   453
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   454
fun tptp_string_of_connective ANot = tptp_not
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   455
  | tptp_string_of_connective AAnd = tptp_and
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   456
  | tptp_string_of_connective AOr = tptp_or
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   457
  | tptp_string_of_connective AImplies = tptp_implies
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   458
  | tptp_string_of_connective AIff = tptp_iff
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   459
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   460
fun string_of_bound_var format (s, ty) =
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   461
  s ^
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   462
  (if is_format_typed format then
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   463
     " " ^ tptp_has_type ^ " " ^
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   464
     (ty |> the_default (AType ((tptp_individual_type, []), [])) |> string_of_type format)
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   465
   else
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44589
diff changeset
   466
     "")
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   467
73154
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   468
fun tptp_string_of_term _ (ATerm ((s, []), [])) =
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   469
    s |> member (op =) (tptp_unary_builtins @ tptp_binary_builtins) s ? parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   470
  | tptp_string_of_term format (ATerm ((s, tys), ts)) =
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   471
    let
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   472
      val of_type = string_of_type format
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   473
      val of_term = tptp_string_of_term format
57300
7e22d7b75e2a added parentheses around type arguments in THF
blanchet
parents: 57267
diff changeset
   474
      fun app () =
7e22d7b75e2a added parentheses around type arguments in THF
blanchet
parents: 57267
diff changeset
   475
        tptp_string_of_app format s
7e22d7b75e2a added parentheses around type arguments in THF
blanchet
parents: 57267
diff changeset
   476
          (map (of_type #> is_format_higher_order format ? parens) tys @ map of_term ts)
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   477
    in
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   478
      if s = tptp_empty_list then
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   479
        (* used for lists in the optional "source" field of a derivation *)
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   480
        "[" ^ commas (map of_term ts) ^ "]"
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   481
      else if is_tptp_equal s then
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   482
        space_implode (" " ^ tptp_equal ^ " ") (map of_term ts)
72877
4eea17b3ac58 Tuned parentheses in TPTP output
desharna
parents: 72824
diff changeset
   483
        |> (is_format_higher_order format orelse is_format_with_fool format) ? parens
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   484
      else if s = tptp_ho_forall orelse s = tptp_ho_exists then
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   485
        (case ts of
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   486
          [AAbs (((s', ty), tm), [])] =>
73157
02b6ca455be4 proper proxification for fool + refactoring
desharna
parents: 73155
diff changeset
   487
          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work
02b6ca455be4 proper proxification for fool + refactoring
desharna
parents: 73155
diff changeset
   488
             around LEO-II, Leo-III, and Satallax parser limitation. *)
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   489
          tptp_string_of_formula format
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   490
              (AQuant (if s = tptp_ho_forall then AForall else AExists,
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   491
                      [(s', SOME ty)], AAtom tm))
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   492
        | _ => app ())
74339
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   493
      else if s = tptp_let then
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   494
        (case ts of
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   495
          [t1, AAbs (((s', ty), tm), [])] =>
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   496
            let
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   497
              val declaration = s' ^ " : " ^ of_type ty
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   498
              val definition = s' ^ " := " ^ of_term t1
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   499
              val usage = of_term tm
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   500
            in
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   501
            s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")"
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   502
            end
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output
desharna
parents: 74115
diff changeset
   503
        | _ => app ())
74393
b9837b07684d fixed $ite syntax in TPTP THX generation
desharna
parents: 74339
diff changeset
   504
      else if s = tptp_ite then
b9837b07684d fixed $ite syntax in TPTP THX generation
desharna
parents: 74339
diff changeset
   505
        (case ts of
b9837b07684d fixed $ite syntax in TPTP THX generation
desharna
parents: 74339
diff changeset
   506
          [t1, t2, t3] => s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")"
b9837b07684d fixed $ite syntax in TPTP THX generation
desharna
parents: 74339
diff changeset
   507
        | _ => app ())
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   508
      else if s = tptp_choice then
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   509
        (case ts of
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   510
          [AAbs (((s', ty), tm), args)] =>
73157
02b6ca455be4 proper proxification for fool + refactoring
desharna
parents: 73155
diff changeset
   511
          (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
02b6ca455be4 proper proxification for fool + refactoring
desharna
parents: 73155
diff changeset
   512
             abstraction. *)
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   513
          tptp_string_of_app format
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   514
              (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   515
               "]: " ^ of_term tm ^ ""
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   516
               |> parens) (map of_term args)
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   517
        | _ => app ())
73154
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   518
      else if member (op =) tptp_unary_builtins s then
73153
6771d34129c9 proper generation of TPTP output for higher order builtins
desharna
parents: 72895
diff changeset
   519
        (* generate e.g. "~ t" instead of "~ @ t". *)
6771d34129c9 proper generation of TPTP output for higher order builtins
desharna
parents: 72895
diff changeset
   520
        (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens)
73154
224eacc4d579 proper handling of builtins in TFX
desharna
parents: 73153
diff changeset
   521
      else if member (op =) tptp_binary_builtins s then
73153
6771d34129c9 proper generation of TPTP output for higher order builtins
desharna
parents: 72895
diff changeset
   522
        (* generate e.g. "t1 & t2" instead of "& @ t1 @ t2". *)
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   523
        (case ts of
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   524
          [t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   525
        | _ => app ())
52074
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   526
      else
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   527
        app ()
bc053db0801e tuned code
blanchet
parents: 52027
diff changeset
   528
    end
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   529
  | tptp_string_of_term (format as THF _) (AAbs (((s, ty), tm), args)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   530
    tptp_string_of_app format
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   531
        ("(^[" ^ s ^ " : " ^ string_of_type format ty ^ "]: " ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   532
         tptp_string_of_term format tm ^ ")")
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   533
        (map (tptp_string_of_term format) args)
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   534
  | tptp_string_of_term _ _ =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   535
    raise Fail "unexpected term in first-order format"
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   536
and tptp_string_of_formula format (ATyQuant (q, xs, phi)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   537
    tptp_string_of_quantifier q ^
48135
a44f34694406 added sorts to datastructure
blanchet
parents: 48133
diff changeset
   538
    "[" ^
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   539
    commas (map (suffix_type_of_types o string_of_type format o fst) xs) ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   540
    "]: " ^ tptp_string_of_formula format phi
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   541
    |> parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   542
  | tptp_string_of_formula format (AQuant (q, xs, phi)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   543
    tptp_string_of_quantifier q ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   544
    "[" ^ commas (map (string_of_bound_var format) xs) ^ "]: " ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   545
    tptp_string_of_formula format phi
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   546
    |> parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   547
  | tptp_string_of_formula format
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   548
        (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42967
diff changeset
   549
    space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   550
                  (map (tptp_string_of_term format) ts)
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   551
    |> is_format_higher_order format ? parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   552
  | tptp_string_of_formula format (AConn (c, [phi])) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   553
    tptp_string_of_connective c ^ " " ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   554
    (tptp_string_of_formula format phi
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   555
     |> is_format_higher_order format ? parens)
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   556
    |> parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   557
  | tptp_string_of_formula format (AConn (c, phis)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   558
    space_implode (" " ^ tptp_string_of_connective c ^ " ")
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   559
                  (map (tptp_string_of_formula format) phis)
52075
f363f54a1936 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
blanchet
parents: 52074
diff changeset
   560
    |> parens
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   561
  | tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm
37961
6a48c85a211a first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents: 37931
diff changeset
   562
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   563
fun tptp_string_of_format CNF = tptp_cnf
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   564
  | tptp_string_of_format CNF_UEQ = tptp_cnf
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   565
  | tptp_string_of_format FOF = tptp_fof
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   566
  | tptp_string_of_format (TFF _) = tptp_tff
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   567
  | tptp_string_of_format (THF _) = tptp_thf
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   568
  | tptp_string_of_format (DFG _) = raise Fail "non-TPTP format"
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   569
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   570
val atype_of_types = AType ((tptp_type_of_types, []), [])
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   571
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   572
fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   573
50522
19dbd7554076 generate original name as a comment in SPASS problems as well
blanchet
parents: 50521
diff changeset
   574
fun maybe_alt "" = ""
19dbd7554076 generate original name as a comment in SPASS problems as well
blanchet
parents: 50521
diff changeset
   575
  | maybe_alt s = " % " ^ s
50521
bec828f3364e generate comments with original names for debugging
blanchet
parents: 50012
diff changeset
   576
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   577
fun tptp_string_of_line format (Type_Decl (ident, ty, ary)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   578
    tptp_string_of_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   579
  | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   580
    tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   581
    " : " ^ string_of_type format ty ^ ").\n"
61862
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   582
  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) =
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   583
    tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
57811
faab5feffb42 put comments between TPTP lines to comply with TPTP BNF
blanchet
parents: 57709
diff changeset
   584
    tptp_string_of_role kind ^ "," ^ "\n    (" ^
faab5feffb42 put comments between TPTP lines to comply with TPTP BNF
blanchet
parents: 57709
diff changeset
   585
    tptp_string_of_formula format phi ^ ")" ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   586
    (case source of
57811
faab5feffb42 put comments between TPTP lines to comply with TPTP BNF
blanchet
parents: 57709
diff changeset
   587
      SOME tm => ", " ^ tptp_string_of_term format tm
61862
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   588
    | NONE => if null info then "" else ", []") ^
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   589
    (case info of
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   590
      [] => ""
2ce3d12015b3 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents: 61550
diff changeset
   591
    | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^
57811
faab5feffb42 put comments between TPTP lines to comply with TPTP BNF
blanchet
parents: 57709
diff changeset
   592
    ")." ^ maybe_alt alt ^ "\n"
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   593
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   594
fun tptp_lines format =
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   595
  maps (fn (_, []) => []
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   596
         | (heading, lines) =>
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 39453
diff changeset
   597
           "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   598
           map (tptp_string_of_line format) lines)
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   599
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   600
fun arity_of_type (APi (tys, ty)) =
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   601
    arity_of_type ty |>> Integer.add (length tys)
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   602
  | arity_of_type (AFun (_, ty)) = arity_of_type ty ||> Integer.add 1
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   603
  | arity_of_type _ = (0, 0)
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   604
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   605
fun string_of_arity (0, n) = string_of_int n
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   606
  | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   607
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48142
diff changeset
   608
val dfg_class_inter = space_implode " & "
0186df5074c8 renamed experimental option
blanchet
parents: 48142
diff changeset
   609
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   610
fun dfg_string_of_term (ATerm ((s, tys), tms)) =
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   611
    s ^
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   612
    (if null tys then ""
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   613
     else "<" ^ commas (map (string_of_type (DFG Polymorphic)) tys) ^ ">") ^
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   614
    (if null tms then ""
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   615
     else "(" ^ commas (map dfg_string_of_term tms) ^ ")")
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   616
  | dfg_string_of_term _ = raise Fail "unexpected atom in first-order format"
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   617
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   618
fun dfg_string_of_formula poly gen_simp info =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   619
  let
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   620
    val str_of_typ = string_of_type (DFG poly)
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   621
    fun str_of_bound_typ (ty, []) = str_of_typ ty
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   622
      | str_of_bound_typ (ty, cls) = str_of_typ ty ^ " : " ^ dfg_class_inter cls
46379
de5dd84717c1 distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents: 46378
diff changeset
   623
    fun suffix_tag top_level s =
48129
933d43c31689 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents: 48004
diff changeset
   624
      if top_level then
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   625
        (case extract_isabelle_status info of
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48143
diff changeset
   626
          SOME s' =>
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   627
          if s' = non_rec_defN then s ^ ":lt"
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   628
          else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then s ^ ":lr"
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   629
          else s
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   630
        | NONE => s)
46379
de5dd84717c1 distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents: 46378
diff changeset
   631
      else
de5dd84717c1 distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet
parents: 46378
diff changeset
   632
        s
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   633
    fun str_of_atom top_level (ATerm ((s, tys), tms)) =
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   634
        let
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   635
          val s' =
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   636
            if is_tptp_equal s then "equal" |> suffix_tag top_level
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   637
            else if s = tptp_true then "true"
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   638
            else if s = tptp_false then "false"
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   639
            else s
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   640
        in dfg_string_of_term (ATerm ((s', tys), tms)) end
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   641
      | str_of_atom _ _ = raise Fail "unexpected atom in first-order format"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   642
    fun str_of_quant AForall = "forall"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   643
      | str_of_quant AExists = "exists"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   644
    fun str_of_conn _ ANot = "not"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   645
      | str_of_conn _ AAnd = "and"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   646
      | str_of_conn _ AOr = "or"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   647
      | str_of_conn _ AImplies = "implies"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   648
      | str_of_conn top_level AIff = "equiv" |> suffix_tag top_level
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   649
    fun str_of_formula top_level (ATyQuant (q, xs, phi)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   650
        str_of_quant q ^ "_sorts([" ^ commas (map str_of_bound_typ xs) ^ "], " ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   651
        str_of_formula top_level phi ^ ")"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   652
      | str_of_formula top_level (AQuant (q, xs, phi)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   653
        str_of_quant q ^ "([" ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   654
        commas (map (string_of_bound_var (DFG poly)) xs) ^ "], " ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   655
        str_of_formula top_level phi ^ ")"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   656
      | str_of_formula top_level (AConn (c, phis)) =
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   657
        str_of_conn top_level c ^ "(" ^
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   658
        commas (map (str_of_formula false) phis) ^ ")"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   659
      | str_of_formula top_level (AAtom tm) = str_of_atom top_level tm
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   660
  in str_of_formula true end
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   661
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   662
fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   663
  | maybe_enclose bef aft s = bef ^ s ^ aft
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   664
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   665
fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   666
  let
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   667
    val typ = string_of_type (DFG poly)
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   668
    val term = dfg_string_of_term
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   669
    fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   670
    fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty))
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   671
    fun ty_ary 0 ty = ty
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   672
      | ty_ary n ty = "(" ^ ty ^ ", " ^ string_of_int n ^ ")"
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   673
    fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ typ ty ^ ")."
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   674
    fun pred_typ sym ty =
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   675
      let
52025
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   676
        val (ty_vars, (tys, _)) =
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   677
          strip_atype ty
9f94930b12e6 more work on SPASS datatypes
blanchet
parents: 52004
diff changeset
   678
          |>> (fn [] => [] | xs => ["[" ^ commas xs ^ "]"])
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   679
      in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   680
    fun bound_tvar (ty, []) = ty
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   681
      | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
52004
6f3cab60621f more work on SPASS datatypes
blanchet
parents: 52003
diff changeset
   682
    fun binder_typ xs ty =
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   683
      (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   684
      typ ty
52004
6f3cab60621f more work on SPASS datatypes
blanchet
parents: 52003
diff changeset
   685
    fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   686
    fun datatype_decl xs ty tms exhaust =
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   687
      "datatype(" ^ commas (binder_typ xs ty :: map term tms @ (if exhaust then [] else ["..."])) ^
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   688
      ")."
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   689
    fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
50522
19dbd7554076 generate original name as a comment in SPASS problems as well
blanchet
parents: 50521
diff changeset
   690
    fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   691
        if pred kind then
48129
933d43c31689 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents: 48004
diff changeset
   692
          let val rank = extract_isabelle_rank info in
57811
faab5feffb42 put comments between TPTP lines to comply with TPTP BNF
blanchet
parents: 57709
diff changeset
   693
            "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ ", " ^ ident ^
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   694
            (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
50522
19dbd7554076 generate original name as a comment in SPASS problems as well
blanchet
parents: 50521
diff changeset
   695
            ")." ^ maybe_alt alt
19dbd7554076 generate original name as a comment in SPASS problems as well
blanchet
parents: 50521
diff changeset
   696
            |> SOME
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46393
diff changeset
   697
          end
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   698
        else
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   699
          NONE
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   700
      | formula _ _ = NONE
46413
505465fae291 tuned SPASS DFG output
blanchet
parents: 46406
diff changeset
   701
    fun filt f = problem |> map (map_filter f o snd) |> filter_out null
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   702
    val func_aries =
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   703
      filt (fn Sym_Decl (_, sym, ty) =>
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   704
               if is_function_atype ty then SOME (tm_ary sym ty) else NONE
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   705
             | _ => NONE)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   706
      |> flat |> commas |> maybe_enclose "functions [" "]."
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   707
    val pred_aries =
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   708
      filt (fn Sym_Decl (_, sym, ty) =>
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   709
               if is_predicate_atype ty then SOME (tm_ary sym ty) else NONE
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   710
             | _ => NONE)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   711
      |> flat |> commas |> maybe_enclose "predicates [" "]."
48129
933d43c31689 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents: 48004
diff changeset
   712
    val sorts =
52000
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   713
      filt (try (fn Type_Decl (_, ty, ary) => ty_ary ary ty)) @
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   714
      [[ty_ary 0 dfg_individual_type]]
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   715
      |> flat |> commas |> maybe_enclose "sorts [" "]."
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   716
    val classes =
52000
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   717
      filt (try (fn Class_Decl (_, cl, _) => cl))
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   718
      |> flat |> commas |> maybe_enclose "classes [" "]."
48129
933d43c31689 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents: 48004
diff changeset
   719
    val ord_info = if gen_weights orelse gen_prec then ord_info () else []
933d43c31689 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents: 48004
diff changeset
   720
    val do_term_order_weights =
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   721
      (if gen_weights then ord_info else [])
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   722
      |> map (spair o apsnd string_of_int) |> commas
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   723
      |> maybe_enclose "weights [" "]."
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   724
    val syms = [func_aries, pred_aries, do_term_order_weights, sorts, classes]
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   725
    val func_decls =
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   726
      filt (fn Sym_Decl (_, sym, ty) =>
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   727
               if is_function_atype ty then SOME (fun_typ sym ty) else NONE
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   728
             | _ => NONE) |> flat
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   729
    val pred_decls =
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   730
      filt (fn Sym_Decl (_, sym, ty) =>
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48135
diff changeset
   731
               if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty)
46391
8d8d3c1f1854 really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
blanchet
parents: 46382
diff changeset
   732
               else NONE
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   733
             | _ => NONE) |> flat
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   734
    val datatype_decls =
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   735
      filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => datatype_decl xs ty tms exhaust))
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
   736
      |> flat
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   737
    val sort_decls =
52000
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   738
      filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   739
    val subclass_decls =
52000
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   740
      filt (try (fn Class_Decl (_, sub, supers) =>
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   741
                    map (subclass_of sub) supers))
650b7c6b8164 tuned code
blanchet
parents: 51998
diff changeset
   742
      |> flat |> flat
51997
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   743
    val decls =
8dbe623a7804 added datatype declaration syntax for next-gen SPASS
blanchet
parents: 51878
diff changeset
   744
      func_decls @ pred_decls @ datatype_decls @ sort_decls @ subclass_decls
46413
505465fae291 tuned SPASS DFG output
blanchet
parents: 46406
diff changeset
   745
    val axioms =
67405
e9ab4ad7bd15 uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents: 67399
diff changeset
   746
      filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
46413
505465fae291 tuned SPASS DFG output
blanchet
parents: 46406
diff changeset
   747
    val conjs =
67405
e9ab4ad7bd15 uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents: 67399
diff changeset
   748
      filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   749
    val settings =
47054
b86864a2b16e removed obsolete temporary hack
blanchet
parents: 47053
diff changeset
   750
      (if is_lpo then ["set_flag(Ordering, 1)."] else []) @
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   751
      (if gen_prec then
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   752
         [ord_info |> map fst |> rev |> commas
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   753
                   |> maybe_enclose "set_precedence(" ")."]
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   754
       else
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47030
diff changeset
   755
         [])
47053
blanchet
parents: 47041
diff changeset
   756
    fun list_of _ [] = []
blanchet
parents: 47041
diff changeset
   757
      | list_of heading ss =
blanchet
parents: 47041
diff changeset
   758
        "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
blanchet
parents: 47041
diff changeset
   759
        ["end_of_list.\n\n"]
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   760
  in
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   761
    "\nbegin_problem(isabelle).\n\n" ::
47053
blanchet
parents: 47041
diff changeset
   762
    list_of "descriptions"
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   763
            ["name({**}).", "author({**}).", "status(unknown).",
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   764
             "description({**})."] @
47053
blanchet
parents: 47041
diff changeset
   765
    list_of "symbols" syms @
blanchet
parents: 47041
diff changeset
   766
    list_of "declarations" decls @
blanchet
parents: 47041
diff changeset
   767
    list_of "formulae(axioms)" axioms @
blanchet
parents: 47041
diff changeset
   768
    list_of "formulae(conjectures)" conjs @
blanchet
parents: 47041
diff changeset
   769
    list_of "settings(SPASS)" settings @
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   770
    ["end_problem.\n"]
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   771
  end
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   772
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51997
diff changeset
   773
fun lines_of_atp_problem format ord ord_info problem =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   774
  "% This file was generated by Isabelle (most likely Sledgehammer)\n\
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 44787
diff changeset
   775
  \% " ^ timestamp () ^ "\n" ::
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   776
  (case format of
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   777
     DFG poly => dfg_lines poly ord ord_info
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   778
   | _ => tptp_lines format) problem
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   779
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   780
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   781
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   782
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   783
fun is_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   784
  | is_line_negated _ = false
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   785
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   786
fun is_line_cnf_ueq (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) =
43193
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   787
    is_tptp_equal s
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   788
  | is_line_cnf_ueq _ = false
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   789
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   790
fun open_conjecture_term (ATerm (((s, s'), tys), tms)) =
56811
b66639331db5 optional case enforcement
haftmann
parents: 56683
diff changeset
   791
    ATerm ((if is_tptp_variable s then (s |> Name.desymbolize (SOME false), s')
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   792
            else (s, s'), tys), tms |> map open_conjecture_term)
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43422
diff changeset
   793
  | open_conjecture_term _ = raise Fail "unexpected higher-order term"
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   794
fun open_formula conj =
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   795
  let
43193
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   796
    (* We are conveniently assuming that all bound variable names are
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   797
       distinct, which should be the case for the formulas we generate. *)
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   798
    fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   799
      | opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   800
      | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   801
      | opn pos (AConn (c, [phi1, phi2])) =
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   802
        let val (pos1, pos2) = polarities_of_conn pos c in
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   803
          AConn (c, [opn pos1 phi1, opn pos2 phi2])
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   804
        end
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   805
      | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
43422
dcbedaf6f80c added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
blanchet
parents: 43295
diff changeset
   806
      | opn _ phi = phi
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   807
  in opn (SOME (not conj)) end
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   808
fun open_formula_line (Formula (ident, kind, phi, source, info)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   809
    Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42942
diff changeset
   810
  | open_formula_line line = line
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   811
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   812
fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
42942
ad34216cff2f removed SNARK hack now that SNARK is fixed
blanchet
parents: 42939
diff changeset
   813
    Formula (ident, Hypothesis, mk_anot phi, source, info)
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   814
  | negate_conjecture_line line = line
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   815
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   816
exception CLAUSIFY of unit
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   817
43126
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   818
(* This "clausification" only expands syntactic sugar, such as "phi => psi" to
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   819
   "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   820
   attempt to distribute conjunctions over disjunctions. *)
43193
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   821
fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot]
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   822
  | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   823
  | clausify_formula true (AConn (AOr, [phi1, phi2])) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58600
diff changeset
   824
    (phi1, phi2) |> apply2 (clausify_formula true)
43193
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   825
                 |> uncurry (map_product (mk_aconn AOr))
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   826
  | clausify_formula false (AConn (AAnd, [phi1, phi2])) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58600
diff changeset
   827
    (phi1, phi2) |> apply2 (clausify_formula false)
43193
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   828
                 |> uncurry (map_product (mk_aconn AOr))
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   829
  | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   830
    clausify_formula true (AConn (AOr, [mk_anot phi1, phi2]))
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   831
  | clausify_formula true (AConn (AIff, phis)) =
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   832
    clausify_formula true (AConn (AImplies, phis)) @
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   833
    clausify_formula true (AConn (AImplies, rev phis))
e11bd628f1a5 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents: 43163
diff changeset
   834
  | clausify_formula _ _ = raise CLAUSIFY ()
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   835
50521
bec828f3364e generate comments with original names for debugging
blanchet
parents: 50012
diff changeset
   836
fun clausify_formula_line (Formula ((ident, alt), kind, phi, source, info)) =
43126
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   837
    let
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   838
      val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   839
    in
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   840
      map2 (fn phi => fn j =>
50521
bec828f3364e generate comments with original names for debugging
blanchet
parents: 50012
diff changeset
   841
               Formula ((ident ^ replicate_string (j - 1) "x", alt), kind, phi,
bec828f3364e generate comments with original names for debugging
blanchet
parents: 50012
diff changeset
   842
                        source, info))
43126
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   843
           phis (1 upto n)
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   844
    end
a7db0afd5200 clausify "<=>" (needed for some type information)
blanchet
parents: 43098
diff changeset
   845
  | clausify_formula_line _ = []
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   846
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   847
fun ensure_cnf_line line =
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   848
  line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43092
diff changeset
   849
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   850
fun ensure_cnf_problem problem = problem |> map (apsnd (maps ensure_cnf_line))
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   851
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   852
fun filter_cnf_ueq_problem problem =
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   853
  problem
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   854
  |> map (apsnd (map open_formula_line #> filter is_line_cnf_ueq
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   855
                 #> map negate_conjecture_line))
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42961
diff changeset
   856
  |> (fn problem =>
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   857
         let
43824
0234156d3fbe don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
blanchet
parents: 43692
diff changeset
   858
           val lines = problem |> maps snd
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   859
           val conjs = lines |> filter is_line_negated
43824
0234156d3fbe don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
blanchet
parents: 43692
diff changeset
   860
         in if length conjs = 1 andalso conjs <> lines then problem else [] end)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38014
diff changeset
   861
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   862
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   863
(** Symbol declarations **)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   864
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   865
fun add_declared_in_line (Class_Decl (_, cl, _)) = apfst (apfst (cons cl))
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   866
  | add_declared_in_line (Type_Decl (_, ty, _)) = apfst (apsnd (cons ty))
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   867
  | add_declared_in_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
   868
  | add_declared_in_line _ = I
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   869
fun declared_in_atp_problem problem =
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   870
  fold (fold add_declared_in_line o snd) problem (([], []), [])
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   871
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   872
(** Nice names **)
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37642
diff changeset
   873
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   874
val no_qualifiers =
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   875
  let
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   876
    fun skip [] = []
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   877
      | skip (#"." :: cs) = skip cs
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   878
      | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   879
    and keep [] = []
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   880
      | keep (#"." :: cs) = skip cs
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   881
      | keep (c :: cs) = c :: keep cs
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   882
  in String.explode #> rev #> keep #> rev #> String.implode end
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 41769
diff changeset
   883
42761
8ea9c6fa8b53 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents: 42752
diff changeset
   884
(* Long names can slow down the ATPs. *)
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42722
diff changeset
   885
val max_readable_name_size = 20
42567
d012947edd36 shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs
blanchet
parents: 42543
diff changeset
   886
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   887
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   888
   unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   889
   ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   890
   is still necessary). *)
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   891
val reserved_nice_names = [tptp_old_equal, "op", "eq"]
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   892
46414
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   893
(* hack to get the same hashing across Mirabelle runs (see "mirabelle.pl") *)
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   894
fun cleanup_mirabelle_name s =
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   895
  let
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   896
    val mirabelle_infix = "_Mirabelle_"
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   897
    val random_suffix_len = 10
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   898
    val (s1, s2) = Substring.position mirabelle_infix (Substring.full s)
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   899
  in
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   900
    if Substring.isEmpty s2 then
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   901
      s
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   902
    else
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   903
      Substring.string s1 ^
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   904
      Substring.string (Substring.triml (size mirabelle_infix + random_suffix_len) s2)
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   905
  end
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   906
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   907
fun readable_name protect full_name s =
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   908
  (if s = full_name then
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   909
     s
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   910
   else
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   911
     s |> no_qualifiers
52076
bfa28e1cba77 freeze types in Sledgehammer goal, not just terms
blanchet
parents: 52075
diff changeset
   912
       |> unquote_tvar
56811
b66639331db5 optional case enforcement
haftmann
parents: 56683
diff changeset
   913
       |> Name.desymbolize (SOME (Char.isUpper (String.sub (full_name, 0))))
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   914
       |> (fn s =>
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   915
              if size s > max_readable_name_size then
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   916
                String.substring (s, 0, max_readable_name_size div 2 - 4) ^
46414
4ed12518fb81 improved hashing w.r.t. Mirabelle, to help debugging
blanchet
parents: 46413
diff changeset
   917
                string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^
56847
3e369d8610c4 improved whitelist (cf. be1874de8344)
blanchet
parents: 56811
diff changeset
   918
                String.extract (s, size s - max_readable_name_size div 2 + 4, NONE)
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   919
              else
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   920
                s)
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   921
       |> (fn s =>
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   922
              if member (op =) reserved_nice_names s then full_name else s))
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   923
  |> protect
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
   924
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   925
fun nice_name _ (full_name, _) NONE = (full_name, NONE)
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   926
  | nice_name protect (full_name, desired_name) (SOME the_pool) =
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   927
    if is_built_in_tptp_symbol full_name then
39384
76603e40bd4c in debug mode, don't touch "$true" and "$false"
blanchet
parents: 39109
diff changeset
   928
      (full_name, SOME the_pool)
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   929
    else
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   930
      (case Symtab.lookup (fst the_pool) full_name of
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   931
        SOME nice_name => (nice_name, SOME the_pool)
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   932
      | NONE =>
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   933
        let
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   934
          val nice_prefix = readable_name protect full_name desired_name
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   935
          fun add j =
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   936
            let
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   937
              val nice_name = nice_prefix ^ (if j = 1 then "" else string_of_int j)
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   938
            in
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   939
              (case Symtab.lookup (snd the_pool) nice_name of
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   940
                SOME full_name' =>
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   941
                if full_name = full_name' then (nice_name, the_pool) else add (j + 1)
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   942
              | NONE =>
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   943
                (nice_name,
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   944
                 (Symtab.update_new (full_name, nice_name) (fst the_pool),
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   945
                  Symtab.update_new (nice_name, full_name) (snd the_pool))))
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   946
            end
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   947
        in add 1 |> apsnd SOME end)
37624
3ee568334813 move "nice names" from Metis to TPTP format
blanchet
parents: 37617
diff changeset
   948
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   949
fun avoid_clash_with_dfg_keywords s =
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   950
  let val n = String.size s in
46443
c86276014571 improved KBO weights -- beware of explicit applications
blanchet
parents: 46442
diff changeset
   951
    if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
c86276014571 improved KBO weights -- beware of explicit applications
blanchet
parents: 46442
diff changeset
   952
       String.isSubstring "_" s then
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   953
      s
47150
6df6e56fd7cd tuning (in particular, Symtab instead of AList)
blanchet
parents: 47148
diff changeset
   954
    else if is_tptp_variable s then
52353
dba3d398c322 SPASS has more Uppercase keywords than I was fearing -- better always append _
blanchet
parents: 52076
diff changeset
   955
      s ^ "_"
46378
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   956
    else
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   957
      String.substring (s, 0, n - 1) ^
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   958
      String.str (Char.toUpper (String.sub (s, n - 1)))
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   959
  end
7769bf5c2a17 nicer keyword class avoidance scheme
blanchet
parents: 46338
diff changeset
   960
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   961
fun nice_atp_problem readable_names format problem =
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   962
  let
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   963
    val empty_pool =
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   964
      if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46445
diff changeset
   965
    val avoid_clash =
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   966
      (case format of
72824
c7e2a9bdc585 Added support for TFX to Sledgehammer
desharna
parents: 72588
diff changeset
   967
        DFG _ => avoid_clash_with_dfg_keywords
54829
157c7dfcbcd8 tuning 'case' expressions
blanchet
parents: 54820
diff changeset
   968
      | _ => I)
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46445
diff changeset
   969
    val nice_name = nice_name avoid_clash
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   970
52001
2fb33d73c366 more work on implementing datatype output for new SPASS
blanchet
parents: 52000
diff changeset
   971
    fun nice_bound_tvars xs =
52003
blanchet
parents: 52002
diff changeset
   972
      fold_map (nice_name o fst) xs
blanchet
parents: 52002
diff changeset
   973
      ##>> fold_map (fold_map nice_name o snd) xs
52001
2fb33d73c366 more work on implementing datatype output for new SPASS
blanchet
parents: 52000
diff changeset
   974
      #>> op ~~
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   975
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   976
    fun nice_type (AType ((name, clss), tys)) =
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   977
        nice_name name ##>> fold_map nice_name clss ##>> fold_map nice_type tys #>> AType
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   978
      | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   979
      | nice_type (APi (names, ty)) = fold_map nice_name names ##>> nice_type ty #>> APi
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   980
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
   981
    fun nice_term (ATerm ((name, tys), ts)) =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   982
        nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts #>> ATerm
47911
2168126446bb extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"
blanchet
parents: 47768
diff changeset
   983
      | nice_term (AAbs (((name, ty), tm), args)) =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   984
        nice_name name ##>> nice_type ty ##>> nice_term tm ##>> fold_map nice_term args #>> AAbs
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
   985
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   986
    fun nice_formula (ATyQuant (q, xs, phi)) =
52003
blanchet
parents: 52002
diff changeset
   987
        fold_map (nice_type o fst) xs
blanchet
parents: 52002
diff changeset
   988
        ##>> fold_map (fold_map nice_name o snd) xs
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
   989
        ##>> nice_formula phi
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
   990
        #>> (fn ((tys, cls), phi) => ATyQuant (q, tys ~~ cls, phi))
48133
a5ab5964065f implement polymorphic DFG output, without type classes for now
blanchet
parents: 48132
diff changeset
   991
      | nice_formula (AQuant (q, xs, phi)) =
52003
blanchet
parents: 52002
diff changeset
   992
        fold_map (nice_name o fst) xs
blanchet
parents: 52002
diff changeset
   993
        ##>> fold_map (fn (_, NONE) => pair NONE
blanchet
parents: 52002
diff changeset
   994
                        | (_, SOME ty) => nice_type ty #>> SOME) xs
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   995
        ##>> nice_formula phi
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   996
        #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   997
      | nice_formula (AConn (c, phis)) =
52002
eff7d1799a70 no need to reinvent the wheel ("fold_map")
blanchet
parents: 52001
diff changeset
   998
        fold_map nice_formula phis #>> curry AConn c
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
   999
      | nice_formula (AAtom tm) = nice_term tm #>> AAtom
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1000
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
  1001
    fun nice_line (Class_Decl (ident, cl, cls)) =
52002
eff7d1799a70 no need to reinvent the wheel ("fold_map")
blanchet
parents: 52001
diff changeset
  1002
        nice_name cl ##>> fold_map nice_name cls
48141
1b864c4a3306 more work on DFG type classes
blanchet
parents: 48140
diff changeset
  1003
        #>> (fn (cl, cls) => Class_Decl (ident, cl, cls))
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
  1004
      | nice_line (Type_Decl (ident, ty, ary)) =
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
  1005
        nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
  1006
      | nice_line (Sym_Decl (ident, sym, ty)) =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1007
        nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
  1008
      | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
52002
eff7d1799a70 no need to reinvent the wheel ("fold_map")
blanchet
parents: 52001
diff changeset
  1009
        nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
56683
7f4ae504e059 reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
blanchet
parents: 54829
diff changeset
  1010
        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48141
diff changeset
  1011
      | nice_line (Class_Memb (ident, xs, ty, cl)) =
52001
2fb33d73c366 more work on implementing datatype output for new SPASS
blanchet
parents: 52000
diff changeset
  1012
        nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
2fb33d73c366 more work on implementing datatype output for new SPASS
blanchet
parents: 52000
diff changeset
  1013
        #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
48140
21232c8c879b more work on class support
blanchet
parents: 48139
diff changeset
  1014
      | nice_line (Formula (ident, kind, phi, source, info)) =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1015
        nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1016
45939
711fec5b4f61 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
blanchet
parents: 45938
diff changeset
  1017
    fun nice_problem problem =
54820
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1018
      fold_map (fn (heading, lines) => fold_map nice_line lines #>> pair heading) problem
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1019
  in
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1020
    nice_problem problem empty_pool
d9ab86c044fd extended ATP types with sorts
blanchet
parents: 54788
diff changeset
  1021
  end
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
  1022
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
diff changeset
  1023
end;