src/HOL/Tools/Metis/metis_translate.ML
author blanchet
Thu, 22 Sep 2011 16:30:47 +0200
changeset 45043 7e1a73fc0c8b
parent 45042 89341b897412
child 45508 b216dc1b3630
permissions -rw-r--r--
drop partial monomorphic instances in Metis, like in Sledgehammer
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
44411
e3629929b171 change Metis's default settings if type information axioms are generated
blanchet
parents: 44409
diff changeset
    12
  type type_enc = ATP_Translate.type_enc
e3629929b171 change Metis's default settings if type information axioms are generated
blanchet
parents: 44409
diff changeset
    13
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    14
  datatype isa_thm =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    15
    Isa_Reflexive_or_Trivial |
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    16
    Isa_Raw of thm
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
    17
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    18
  val metis_equal : string
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    19
  val metis_predicator : string
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    20
  val metis_app_op : string
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    21
  val metis_systematic_type_tag : string
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    22
  val metis_ad_hoc_type_tag : string
42098
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 41491
diff changeset
    23
  val metis_generated_var_prefix : string
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    24
  val trace : bool Config.T
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    25
  val verbose : bool Config.T
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    26
  val trace_msg : Proof.context -> (unit -> string) -> unit
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    27
  val verbose_warning : Proof.context -> string -> unit
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    28
  val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    29
  val reveal_old_skolem_terms : (string * term) list -> term -> term
40157
a2f01956220e renaming
blanchet
parents: 40145
diff changeset
    30
  val prepare_metis_problem :
44411
e3629929b171 change Metis's default settings if type information axioms are generated
blanchet
parents: 44409
diff changeset
    31
    Proof.context -> type_enc -> thm list -> thm list
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    32
    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
24310
af4af9993922 proper signature;
wenzelm
parents: 24183
diff changeset
    33
end
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    34
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39355
diff changeset
    35
structure Metis_Translate : METIS_TRANSLATE =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    36
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    37
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
    38
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    39
open ATP_Translate
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    40
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    41
val metis_equal = "="
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    42
val metis_predicator = "{}"
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    43
val metis_app_op = Metis_Name.toString Metis_Term.appName
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    44
val metis_systematic_type_tag =
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    45
  Metis_Name.toString Metis_Term.hasTypeFunctionName
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    46
val metis_ad_hoc_type_tag = "**"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    47
val metis_generated_var_prefix = "_"
17150
ce2a1aeb42aa DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents: 16976
diff changeset
    48
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    49
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
    50
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
    51
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    52
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
    53
fun verbose_warning ctxt msg =
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    54
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    55
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    56
val metis_name_table =
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    57
  [((tptp_equal, 2), (K metis_equal, false)),
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    58
   ((tptp_old_equal, 2), (K metis_equal, false)),
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    59
   ((prefixed_predicator_name, 1), (K metis_predicator, false)),
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    60
   ((prefixed_app_op_name, 2), (K metis_app_op, false)),
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
    61
   ((prefixed_type_tag_name, 2),
44782
blanchet
parents: 44768
diff changeset
    62
    (fn type_enc =>
blanchet
parents: 44768
diff changeset
    63
        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
blanchet
parents: 44768
diff changeset
    64
        else metis_ad_hoc_type_tag, true))]
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    65
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    66
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
    67
  old_skolem_const_prefix ^ Long_Name.separator ^
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41156
diff changeset
    68
  (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
    69
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    70
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
    71
  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
    72
    let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    73
      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
    74
             (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
    75
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    76
            val (old_skolems, s) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    77
              if i = ~1 then
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    78
                (old_skolems, @{const_name undefined})
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    79
              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
    80
                s :: _ => (old_skolems, s)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    81
              | [] =>
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    82
                let
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    83
                  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
    84
                                                (length (Term.add_tvarsT T []))
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    85
                in ((s, t) :: old_skolems, s) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    86
          in (old_skolems, Const (s, T)) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    87
        | aux old_skolems (t1 $ t2) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    88
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    89
            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
    90
            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
    91
          in (old_skolems, t1 $ t2) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    92
        | aux old_skolems (Abs (s, T, t')) =
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    93
          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
    94
            (old_skolems, Abs (s, T, t'))
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    95
          end
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    96
        | aux old_skolems t = (old_skolems, t)
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    97
    in aux old_skolems t end
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    98
  else
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    99
    (old_skolems, t)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   100
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
   101
fun reveal_old_skolem_terms old_skolems =
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   102
  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
   103
                 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
   104
                   AList.lookup (op =) old_skolems s |> the
43826
2b094d17f432 fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
blanchet
parents: 43626
diff changeset
   105
                   |> map_types (map_type_tvar (K dummyT))
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   106
                 else
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   107
                   t
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   108
               | t => t)
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   109
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   110
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   111
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   112
(* 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
   113
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   114
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   115
datatype isa_thm =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   116
  Isa_Reflexive_or_Trivial |
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   117
  Isa_Raw of thm
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   118
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   119
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
   120
val prepare_helper =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   121
  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
   122
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   123
fun metis_term_from_atp type_enc (ATerm (s, tms)) =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   124
  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
   125
    Metis_Term.Var (Metis_Name.fromString s)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   126
  else
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   127
    (case AList.lookup (op =) metis_name_table (s, length tms) of
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   128
       SOME (f, swap) => (f type_enc, swap)
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   129
     | NONE => (s, false))
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   130
    |> (fn (s, swap) =>
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   131
           Metis_Term.Fn (Metis_Name.fromString s,
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   132
                          tms |> map (metis_term_from_atp type_enc)
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   133
                              |> swap ? rev))
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   134
fun metis_atom_from_atp type_enc (AAtom tm) =
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   135
    (case metis_term_from_atp type_enc tm of
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43103
diff changeset
   136
       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
   137
     | _ => raise Fail "non CNF -- expected function")
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   138
  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   139
fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   140
    (false, metis_atom_from_atp type_enc phi)
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   141
  | metis_literal_from_atp type_enc phi =
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   142
    (true, metis_atom_from_atp type_enc phi)
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   143
fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   144
    maps (metis_literals_from_atp type_enc) phis
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   145
  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   146
fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   147
    let
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   148
      fun some isa =
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   149
        SOME (phi |> metis_literals_from_atp type_enc
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   150
                  |> Metis_LiteralSet.fromList
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   151
                  |> Metis_Thm.axiom, isa)
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   152
    in
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   153
      if ident = type_tag_idempotence_helper_name orelse
44396
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
   154
         String.isPrefix tags_sym_formula_prefix ident then
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   155
        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
   156
      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
   157
        NONE
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   158
      else if String.isPrefix helper_prefix ident then
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   159
        case (String.isSuffix typed_helper_suffix ident,
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   160
              space_explode "_" ident) of
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   161
          (needs_fairly_sound, _ :: const :: j :: _) =>
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   162
          nth ((const, needs_fairly_sound)
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   163
               |> AList.lookup (op =) helper_table |> the)
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   164
              (the (Int.fromString j) - 1)
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   165
          |> prepare_helper
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   166
          |> Isa_Raw |> some
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   167
        | _ => 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
   168
      else case try (unprefix fact_prefix) ident of
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   169
        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
   170
        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
   171
          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
   172
        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
   173
      | NONE => TrueI |> Isa_Raw |> some
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   174
    end
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   175
  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   176
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   177
(* Function to generate metis clauses, including comb and type clauses *)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   178
fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   179
  let
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
   180
    val (conj_clauses, fact_clauses) =
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   181
      if polymorphism_of_type_enc type_enc = Polymorphic then
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
   182
        (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
   183
      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
   184
        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
   185
        |> map (pair 0)
45043
7e1a73fc0c8b drop partial monomorphic instances in Metis, like in Sledgehammer
blanchet
parents: 45042
diff changeset
   186
        |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)
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
   187
        |-> 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
   188
        |> 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
   189
        |> 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
   190
    val num_conjs = length conj_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   191
    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
   192
      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
   193
           (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
   194
      (* "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
   195
      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
   196
           (0 upto length fact_clauses - 1) fact_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   197
    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
   198
      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
   199
                   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
   200
                      |> 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
   201
                      ||> (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
   202
               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
   203
    (*
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
    val _ =
45042
89341b897412 better type reconstruction -- prevents ill-instantiations in proof replay
blanchet
parents: 44782
diff changeset
   205
      tracing ("PROPS:\n" ^
89341b897412 better type reconstruction -- prevents ill-instantiations in proof replay
blanchet
parents: 44782
diff changeset
   206
               cat_lines (map (Syntax.string_of_term ctxt o snd) 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
   207
    *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   208
    val (atp_problem, _, _, _, _, _, sym_tab) =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
   209
      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
   210
                          false 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
   211
    (*
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
   212
    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
   213
                     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
   214
    *)
44409
b529d9501d64 prefer the lighter, slightly unsound monotonicity-based encodings for Metis
blanchet
parents: 44397
diff changeset
   215
    (* "rev" is for compatibility. *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   216
    val axioms =
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   217
      atp_problem
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   218
      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   219
  in (sym_tab, axioms, old_skolems) end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   220
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   221
end;