src/HOL/Tools/Metis/metis_translate.ML
author blanchet
Mon, 27 Jun 2011 14:56:28 +0200
changeset 43572 ae612a423dad
parent 43496 92f5a4c78b37
child 43626 a867ebb12209
permissions -rw-r--r--
added "sound" option to force Sledgehammer to be pedantically sound
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39958
88c9aa5666de tuned comments
blanchet
parents: 39953
diff changeset
     1
(*  Title:      HOL/Tools/Metis/metis_translate.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38024
diff changeset
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
     3
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
     4
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
36393
be73a2b2443b support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents: 36378
diff changeset
     5
    Author:     Jasmin Blanchette, TU Muenchen
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     6
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39355
diff changeset
     7
Translation of HOL to FOL for Metis.
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     8
*)
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     9
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39355
diff changeset
    10
signature METIS_TRANSLATE =
24310
af4af9993922 proper signature;
wenzelm
parents: 24183
diff changeset
    11
sig
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    12
  datatype isa_thm =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    13
    Isa_Reflexive_or_Trivial |
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    14
    Isa_Raw of thm
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    15
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    16
  val metis_equal : string
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    17
  val metis_predicator : string
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    18
  val metis_app_op : string
43106
6ec2a3c7b69e fixed new path finder for type information tag
blanchet
parents: 43104
diff changeset
    19
  val metis_type_tag : string
42098
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
    20
  val metis_generated_var_prefix : string
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    21
  val trace : bool Config.T
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    22
  val verbose : bool Config.T
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    23
  val trace_msg : Proof.context -> (unit -> string) -> unit
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    24
  val verbose_warning : Proof.context -> string -> unit
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    25
  val metis_name_table : ((string * int) * (string * bool)) list
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    26
  val reveal_old_skolem_terms : (string * term) list -> term -> term
40157
a2f01956220e renaming
blanchet
parents: 40145
diff changeset
    27
  val prepare_metis_problem :
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    28
    Proof.context -> string -> thm list -> thm list
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    29
    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
24310
af4af9993922 proper signature;
wenzelm
parents: 24183
diff changeset
    30
end
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    31
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39355
diff changeset
    32
structure Metis_Translate : METIS_TRANSLATE =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    33
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    34
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
    35
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    36
open ATP_Translate
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    37
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    38
val metis_equal = "="
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    39
val metis_predicator = "{}"
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    40
val metis_app_op = "."
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    41
val metis_type_tag = ":"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    42
val metis_generated_var_prefix = "_"
17150
ce2a1aeb42aa DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents: 16976
diff changeset
    43
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    44
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    45
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    46
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    47
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    48
fun verbose_warning ctxt msg =
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    49
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    50
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    51
val metis_name_table =
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    52
  [((tptp_equal, 2), (metis_equal, false)),
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
    53
   ((tptp_old_equal, 2), (metis_equal, false)),
43174
f497a1e97d37 skip "hBOOL" in new Metis path finder
blanchet
parents: 43173
diff changeset
    54
   ((prefixed_predicator_name, 1), (metis_predicator, false)),
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    55
   ((prefixed_app_op_name, 2), (metis_app_op, false)),
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    56
   ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    57
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    58
fun old_skolem_const_name i j num_T_args =
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    59
  old_skolem_const_prefix ^ Long_Name.separator ^
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41156
diff changeset
    60
  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    61
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    62
fun conceal_old_skolem_terms i old_skolems t =
39953
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39946
diff changeset
    63
  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    64
    let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    65
      fun aux old_skolems
39953
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39946
diff changeset
    66
             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    67
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    68
            val (old_skolems, s) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    69
              if i = ~1 then
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    70
                (old_skolems, @{const_name undefined})
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    71
              else case AList.find (op aconv) old_skolems t of
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    72
                s :: _ => (old_skolems, s)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    73
              | [] =>
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    74
                let
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    75
                  val s = old_skolem_const_name i (length old_skolems)
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    76
                                                (length (Term.add_tvarsT T []))
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    77
                in ((s, t) :: old_skolems, s) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    78
          in (old_skolems, Const (s, T)) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    79
        | aux old_skolems (t1 $ t2) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    80
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    81
            val (old_skolems, t1) = aux old_skolems t1
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    82
            val (old_skolems, t2) = aux old_skolems t2
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    83
          in (old_skolems, t1 $ t2) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    84
        | aux old_skolems (Abs (s, T, t')) =
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    85
          let val (old_skolems, t') = aux old_skolems t' in
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    86
            (old_skolems, Abs (s, T, t'))
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    87
          end
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    88
        | aux old_skolems t = (old_skolems, t)
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    89
    in aux old_skolems t end
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    90
  else
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    91
    (old_skolems, t)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    92
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    93
fun reveal_old_skolem_terms old_skolems =
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
    94
  map_aterms (fn t as Const (s, _) =>
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    95
                 if String.isPrefix old_skolem_const_prefix s then
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    96
                   AList.lookup (op =) old_skolems s |> the
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
    97
                   |> map_types Type_Infer.paramify_vars
df12f798df99 move function
blanchet
parents: 37625
diff changeset
    98
                 else
df12f798df99 move function
blanchet
parents: 37625
diff changeset
    99
                   t
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   100
               | t => t)
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   101
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   102
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   103
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   104
(* Logic maps manage the interface between HOL and first-order logic.        *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   105
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   106
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   107
datatype isa_thm =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   108
  Isa_Reflexive_or_Trivial |
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   109
  Isa_Raw of thm
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   110
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   111
val proxy_defs = map (fst o snd o snd) proxy_table
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   112
val prepare_helper =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   113
  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   114
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   115
fun metis_term_from_atp (ATerm (s, tms)) =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   116
  if is_tptp_variable s then
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   117
    Metis_Term.Var (Metis_Name.fromString s)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   118
  else
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   119
    let
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   120
      val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   121
                      |> the_default (s, false)
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   122
    in
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   123
      Metis_Term.Fn (Metis_Name.fromString s,
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   124
                     tms |> map metis_term_from_atp |> swap ? rev)
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   125
    end
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   126
fun metis_atom_from_atp (AAtom tm) =
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   127
    (case metis_term_from_atp tm of
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   128
       Metis_Term.Fn x => x
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   129
     | _ => raise Fail "non CNF -- expected function")
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   130
  | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   131
fun metis_literal_from_atp (AConn (ANot, [phi])) =
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   132
    (false, metis_atom_from_atp phi)
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   133
  | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
43268
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   134
fun metis_literals_from_atp (AConn (AOr, phis)) =
c0eaa8b9bff5 removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents: 43259
diff changeset
   135
    maps metis_literals_from_atp phis
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   136
  | metis_literals_from_atp phi = [metis_literal_from_atp phi]
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   137
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   138
    let
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   139
      fun some isa =
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   140
        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   141
                  |> Metis_Thm.axiom, isa)
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   142
    in
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   143
      if ident = type_tag_idempotence_helper_name orelse
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   144
         String.isPrefix lightweight_tags_sym_formula_prefix ident then
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   145
        Isa_Reflexive_or_Trivial |> some
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   146
      else if String.isPrefix conjecture_prefix ident then
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   147
        NONE
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   148
      else if String.isPrefix helper_prefix ident then
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   149
        case (String.isSuffix typed_helper_suffix ident,
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   150
              space_explode "_" ident) of
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   151
          (needs_fairly_sound, _ :: const :: j :: _) =>
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   152
          nth ((const, needs_fairly_sound)
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   153
               |> AList.lookup (op =) helper_table |> the)
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   154
              (the (Int.fromString j) - 1)
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   155
          |> prepare_helper
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   156
          |> Isa_Raw |> some
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   157
        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   158
      else case try (unprefix fact_prefix) ident of
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   159
        SOME s =>
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   160
        let
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   161
          val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   162
        in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   163
      | NONE => TrueI |> Isa_Raw |> some
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   164
    end
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   165
  | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   166
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   167
(* Function to generate metis clauses, including comb and type clauses *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   168
fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   169
  let
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   170
    val type_sys = type_sys_from_string type_sys
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   171
    val (conj_clauses, fact_clauses) =
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   172
      if polymorphism_of_type_sys type_sys = Polymorphic then
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   173
        (conj_clauses, fact_clauses)
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   174
      else
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   175
        conj_clauses @ fact_clauses
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   176
        |> map (pair 0)
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   177
        |> rpair ctxt
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   178
        |-> Monomorph.monomorph atp_schematic_consts_of
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   179
        |> fst |> chop (length conj_clauses)
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   180
        |> pairself (maps (map (zero_var_indexes o snd)))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   181
    val num_conjs = length conj_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   182
    val clauses =
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   183
      map2 (fn j => pair (Int.toString j, Local))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   184
           (0 upto num_conjs - 1) conj_clauses @
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   185
      (* "General" below isn't quite correct; the fact could be local. *)
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   186
      map2 (fn j => pair (Int.toString (num_conjs + j), General))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   187
           (0 upto length fact_clauses - 1) fact_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   188
    val (old_skolems, props) =
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   189
      fold_rev (fn (name, th) => fn (old_skolems, props) =>
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   190
                   th |> prop_of |> Logic.strip_imp_concl
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   191
                      |> conceal_old_skolem_terms (length clauses) old_skolems
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   192
                      ||> (fn prop => (name, prop) :: props))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   193
               clauses ([], [])
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   194
    (*
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   195
    val _ =
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   196
      tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   197
    *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   198
    val (atp_problem, _, _, _, _, _, sym_tab) =
43572
ae612a423dad added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents: 43496
diff changeset
   199
      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
ae612a423dad added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents: 43496
diff changeset
   200
                          false [] @{prop False} props
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   201
    (*
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   202
    val _ = tracing ("ATP PROBLEM: " ^
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   203
                     cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43268
diff changeset
   204
    *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   205
    (* "rev" is for compatibility *)
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   206
    val axioms =
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   207
      atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   208
                  |> rev
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   209
  in (sym_tab, axioms, old_skolems) end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   210
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   211
end;