src/HOL/Tools/Metis/metis_translate.ML
author blanchet
Tue, 15 Nov 2011 22:13:39 +0100
changeset 45510 96696c360b3e
parent 45508 b216dc1b3630
child 45511 9b0f8ca4388e
permissions -rw-r--r--
disable debugging output
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
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    26
  val lambda_translation : string Config.T
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    27
  val trace_msg : Proof.context -> (unit -> string) -> unit
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    28
  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
    29
  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
    30
  val reveal_old_skolem_terms : (string * term) list -> term -> term
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    31
  val reveal_lambda_lifted : (string * term) list -> term -> term
40157
a2f01956220e renaming
blanchet
parents: 40145
diff changeset
    32
  val prepare_metis_problem :
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    33
    Proof.context -> type_enc -> string -> thm list -> thm list
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    34
    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    35
       * ((string * term) list * (string * term) list)
24310
af4af9993922 proper signature;
wenzelm
parents: 24183
diff changeset
    36
end
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    37
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39355
diff changeset
    38
structure Metis_Translate : METIS_TRANSLATE =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    39
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    40
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
    41
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    42
open ATP_Translate
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    43
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    44
val metis_equal = "="
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    45
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
    46
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
    47
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
    48
  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
    49
val metis_ad_hoc_type_tag = "**"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43003
diff changeset
    50
val metis_generated_var_prefix = "_"
17150
ce2a1aeb42aa DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents: 16976
diff changeset
    51
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    52
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
    53
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    54
val lambda_translation =
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    55
  Attrib.setup_config_string @{binding metis_lambda_translation}
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
    56
      (K combinatorsN)
43231
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    57
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    58
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
    59
fun verbose_warning ctxt msg =
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    60
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
69f22ac07395 nicely thread monomorphism verbosity in Metis and Sledgehammer
blanchet
parents: 43224
diff changeset
    61
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    62
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
    63
  [((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
    64
   ((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
    65
   ((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
    66
   ((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
    67
   ((prefixed_type_tag_name, 2),
44782
blanchet
parents: 44768
diff changeset
    68
    (fn type_enc =>
blanchet
parents: 44768
diff changeset
    69
        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
blanchet
parents: 44768
diff changeset
    70
        else metis_ad_hoc_type_tag, true))]
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
    71
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    72
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
    73
  old_skolem_const_prefix ^ Long_Name.separator ^
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41156
diff changeset
    74
  (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
    75
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    76
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
    77
  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
    78
    let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    79
      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
    80
             (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
    81
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    82
            val (old_skolems, s) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    83
              if i = ~1 then
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    84
                (old_skolems, @{const_name undefined})
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    85
              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
    86
                s :: _ => (old_skolems, s)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    87
              | [] =>
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    88
                let
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39890
diff changeset
    89
                  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
    90
                                                (length (Term.add_tvarsT T []))
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    91
                in ((s, t) :: old_skolems, s) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    92
          in (old_skolems, Const (s, T)) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    93
        | aux old_skolems (t1 $ t2) =
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
    94
          let
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    95
            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
    96
            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
    97
          in (old_skolems, t1 $ t2) end
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    98
        | aux old_skolems (Abs (s, T, t')) =
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
    99
          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
   100
            (old_skolems, Abs (s, T, t'))
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   101
          end
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
   102
        | aux old_skolems t = (old_skolems, t)
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
   103
    in aux old_skolems t end
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   104
  else
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
   105
    (old_skolems, t)
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   106
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39720
diff changeset
   107
fun reveal_old_skolem_terms old_skolems =
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   108
  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
   109
                 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
   110
                   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
   111
                   |> map_types (map_type_tvar (K dummyT))
37632
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   112
                 else
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   113
                   t
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   114
               | t => t)
df12f798df99 move function
blanchet
parents: 37625
diff changeset
   115
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   116
fun reveal_lambda_lifted lambdas =
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   117
  map_aterms (fn t as Free (s, _) =>
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   118
                 if String.isPrefix lambda_lifted_prefix s then
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   119
                   case AList.lookup (op =) lambdas s of
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   120
                     SOME t => t |> map_types (map_type_tvar (K dummyT))
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   121
                   | NONE => t
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   122
                 else
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   123
                   t
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   124
               | t => t)
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   125
37577
5379f41a1322 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents: 37575
diff changeset
   126
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   127
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   128
(* 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
   129
(* ------------------------------------------------------------------------- *)
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   130
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   131
datatype isa_thm =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   132
  Isa_Reflexive_or_Trivial |
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   133
  Isa_Raw of thm
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   134
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   135
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
   136
val prepare_helper =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43132
diff changeset
   137
  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
   138
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
   139
fun metis_term_from_atp type_enc (ATerm (s, tms)) =
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   140
  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
   141
    Metis_Term.Var (Metis_Name.fromString s)
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43093
diff changeset
   142
  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
   143
    (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
   144
       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
   145
     | 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
   146
    |> (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
   147
           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
   148
                          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
   149
                              |> 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
   150
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
   151
    (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
   152
       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
   153
     | _ => 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
   154
  | 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
   155
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
   156
    (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
   157
  | 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
   158
    (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
   159
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
   160
    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
   161
  | 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
   162
fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   163
    let
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   164
      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
   165
        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
   166
                  |> Metis_LiteralSet.fromList
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   167
                  |> Metis_Thm.axiom, isa)
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   168
    in
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   169
      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
   170
         String.isPrefix tags_sym_formula_prefix ident then
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   171
        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
   172
      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
   173
        NONE
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   174
      else if String.isPrefix helper_prefix ident then
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   175
        case (String.isSuffix typed_helper_suffix ident,
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   176
              space_explode "_" ident) of
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   177
          (needs_fairly_sound, _ :: const :: j :: _) =>
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   178
          nth ((const, needs_fairly_sound)
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   179
               |> AList.lookup (op =) helper_table |> the)
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   180
              (the (Int.fromString j) - 1)
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   181
          |> prepare_helper
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   182
          |> Isa_Raw |> some
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   183
        | _ => 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
   184
      else case try (unprefix fact_prefix) ident of
43173
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   185
        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
   186
        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
   187
          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
   188
        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
   189
      | NONE => TrueI |> Isa_Raw |> some
b98daa96d043 don't pass "~ " to new Metis
blanchet
parents: 43160
diff changeset
   190
    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
   191
  | 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
   192
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   193
(* Function to generate metis clauses, including comb and type clauses *)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   194
fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   195
  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
   196
    val (conj_clauses, fact_clauses) =
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43572
diff changeset
   197
      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
   198
        (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
   199
      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
   200
        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
   201
        |> map (pair 0)
45043
7e1a73fc0c8b drop partial monomorphic instances in Metis, like in Sledgehammer
blanchet
parents: 45042
diff changeset
   202
        |> 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
   203
        |-> 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
   204
        |> 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
   205
        |> 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
   206
    val num_conjs = length conj_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   207
    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
   208
      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
   209
           (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
   210
      (* "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
   211
      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
   212
           (0 upto length fact_clauses - 1) fact_clauses
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   213
    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
   214
      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
   215
                   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
   216
                      |> 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
   217
                      ||> (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
   218
               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
   219
    (*
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
   220
    val _ =
45042
89341b897412 better type reconstruction -- prevents ill-instantiations in proof replay
blanchet
parents: 44782
diff changeset
   221
      tracing ("PROPS:\n" ^
89341b897412 better type reconstruction -- prevents ill-instantiations in proof replay
blanchet
parents: 44782
diff changeset
   222
               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
   223
    *)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   224
    val (lambda_trans, preproc) =
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   225
      if lambda_trans = combinatorsN then (no_lambdasN, false)
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   226
      else (lambda_trans, true)
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   227
    val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   228
      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   229
                          false preproc [] @{prop False} props
45510
96696c360b3e disable debugging output
blanchet
parents: 45508
diff changeset
   230
    (*
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
   231
    val _ = tracing ("ATP PROBLEM: " ^
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   232
                     cat_lines (lines_for_atp_problem CNF atp_problem))
45510
96696c360b3e disable debugging output
blanchet
parents: 45508
diff changeset
   233
    *)
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   234
    (* "rev" is for compatibility with existing proof scripts. *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   235
    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
   236
      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
   237
      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45043
diff changeset
   238
  in (sym_tab, axioms, (lifted, old_skolems)) end
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   239
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   240
end;