src/HOL/Tools/Metis/metis_translate.ML
author blanchet
Wed Jun 08 08:47:43 2011 +0200 (2011-06-08)
changeset 43268 c0eaa8b9bff5
parent 43259 30c141dc22d6
child 43295 30aaab778416
permissions -rw-r--r--
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet@39958
     1
(*  Title:      HOL/Tools/Metis/metis_translate.ML
blanchet@38027
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
blanchet@39497
     3
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
blanchet@39497
     4
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@36393
     5
    Author:     Jasmin Blanchette, TU Muenchen
paulson@15347
     6
blanchet@39494
     7
Translation of HOL to FOL for Metis.
paulson@15347
     8
*)
paulson@15347
     9
blanchet@39494
    10
signature METIS_TRANSLATE =
wenzelm@24310
    11
sig
blanchet@43085
    12
  type type_literal = ATP_Translate.type_literal
blanchet@37577
    13
blanchet@43159
    14
  datatype isa_thm =
blanchet@43159
    15
    Isa_Reflexive_or_Trivial |
blanchet@43159
    16
    Isa_Raw of thm
blanchet@43159
    17
blanchet@43094
    18
  val metis_equal : string
blanchet@43094
    19
  val metis_predicator : string
blanchet@43094
    20
  val metis_app_op : string
blanchet@43106
    21
  val metis_type_tag : string
blanchet@42098
    22
  val metis_generated_var_prefix : string
blanchet@43231
    23
  val trace : bool Config.T
blanchet@43231
    24
  val verbose : bool Config.T
blanchet@43231
    25
  val trace_msg : Proof.context -> (unit -> string) -> unit
blanchet@43231
    26
  val verbose_warning : Proof.context -> string -> unit
blanchet@43104
    27
  val metis_name_table : ((string * int) * (string * bool)) list
blanchet@39886
    28
  val reveal_old_skolem_terms : (string * term) list -> term -> term
blanchet@40157
    29
  val prepare_metis_problem :
blanchet@43212
    30
    Proof.context -> string -> thm list -> thm list
blanchet@43212
    31
    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
wenzelm@24310
    32
end
paulson@15347
    33
blanchet@39494
    34
structure Metis_Translate : METIS_TRANSLATE =
paulson@15347
    35
struct
paulson@15347
    36
blanchet@43092
    37
open ATP_Problem
blanchet@43085
    38
open ATP_Translate
paulson@15347
    39
blanchet@43094
    40
val metis_equal = "="
blanchet@43094
    41
val metis_predicator = "{}"
blanchet@43094
    42
val metis_app_op = "."
blanchet@43104
    43
val metis_type_tag = ":"
blanchet@43085
    44
val metis_generated_var_prefix = "_"
quigley@17150
    45
blanchet@43231
    46
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
blanchet@43231
    47
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
blanchet@43231
    48
blanchet@43231
    49
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@43231
    50
fun verbose_warning ctxt msg =
blanchet@43231
    51
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
blanchet@43231
    52
blanchet@43094
    53
val metis_name_table =
blanchet@43104
    54
  [((tptp_equal, 2), (metis_equal, false)),
blanchet@43104
    55
   ((tptp_old_equal, 2), (metis_equal, false)),
blanchet@43174
    56
   ((prefixed_predicator_name, 1), (metis_predicator, false)),
blanchet@43130
    57
   ((prefixed_app_op_name, 2), (metis_app_op, false)),
blanchet@43130
    58
   ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
blanchet@43094
    59
blanchet@39896
    60
fun old_skolem_const_name i j num_T_args =
blanchet@39896
    61
  old_skolem_const_prefix ^ Long_Name.separator ^
wenzelm@41491
    62
  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
blanchet@37577
    63
blanchet@39886
    64
fun conceal_old_skolem_terms i old_skolems t =
blanchet@39953
    65
  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
blanchet@37577
    66
    let
blanchet@39886
    67
      fun aux old_skolems
blanchet@39953
    68
             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
blanchet@37577
    69
          let
blanchet@39886
    70
            val (old_skolems, s) =
blanchet@37577
    71
              if i = ~1 then
blanchet@39886
    72
                (old_skolems, @{const_name undefined})
blanchet@39886
    73
              else case AList.find (op aconv) old_skolems t of
blanchet@39886
    74
                s :: _ => (old_skolems, s)
blanchet@37577
    75
              | [] =>
blanchet@37577
    76
                let
blanchet@39896
    77
                  val s = old_skolem_const_name i (length old_skolems)
blanchet@39896
    78
                                                (length (Term.add_tvarsT T []))
blanchet@39886
    79
                in ((s, t) :: old_skolems, s) end
blanchet@39886
    80
          in (old_skolems, Const (s, T)) end
blanchet@39886
    81
        | aux old_skolems (t1 $ t2) =
blanchet@37577
    82
          let
blanchet@39886
    83
            val (old_skolems, t1) = aux old_skolems t1
blanchet@39886
    84
            val (old_skolems, t2) = aux old_skolems t2
blanchet@39886
    85
          in (old_skolems, t1 $ t2) end
blanchet@39886
    86
        | aux old_skolems (Abs (s, T, t')) =
blanchet@39886
    87
          let val (old_skolems, t') = aux old_skolems t' in
blanchet@39886
    88
            (old_skolems, Abs (s, T, t'))
blanchet@37577
    89
          end
blanchet@39886
    90
        | aux old_skolems t = (old_skolems, t)
blanchet@39886
    91
    in aux old_skolems t end
blanchet@37577
    92
  else
blanchet@39886
    93
    (old_skolems, t)
blanchet@37577
    94
blanchet@39886
    95
fun reveal_old_skolem_terms old_skolems =
blanchet@37632
    96
  map_aterms (fn t as Const (s, _) =>
blanchet@39896
    97
                 if String.isPrefix old_skolem_const_prefix s then
blanchet@39886
    98
                   AList.lookup (op =) old_skolems s |> the
blanchet@37632
    99
                   |> map_types Type_Infer.paramify_vars
blanchet@37632
   100
                 else
blanchet@37632
   101
                   t
blanchet@37632
   102
               | t => t)
blanchet@37632
   103
blanchet@37577
   104
blanchet@39497
   105
(* ------------------------------------------------------------------------- *)
blanchet@39497
   106
(* Logic maps manage the interface between HOL and first-order logic.        *)
blanchet@39497
   107
(* ------------------------------------------------------------------------- *)
blanchet@39497
   108
blanchet@43159
   109
datatype isa_thm =
blanchet@43159
   110
  Isa_Reflexive_or_Trivial |
blanchet@43159
   111
  Isa_Raw of thm
blanchet@43159
   112
blanchet@43159
   113
val proxy_defs = map (fst o snd o snd) proxy_table
blanchet@43159
   114
val prepare_helper =
blanchet@43159
   115
  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
blanchet@43159
   116
blanchet@43092
   117
fun metis_term_from_atp (ATerm (s, tms)) =
blanchet@43094
   118
  if is_tptp_variable s then
blanchet@43268
   119
    Metis_Term.Var (Metis_Name.fromString s)
blanchet@43094
   120
  else
blanchet@43268
   121
    let
blanchet@43268
   122
      val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
blanchet@43268
   123
                      |> the_default (s, false)
blanchet@43268
   124
    in
blanchet@43268
   125
      Metis_Term.Fn (Metis_Name.fromString s,
blanchet@43268
   126
                     tms |> map metis_term_from_atp |> swap ? rev)
blanchet@43104
   127
    end
blanchet@43104
   128
fun metis_atom_from_atp (AAtom tm) =
blanchet@43104
   129
    (case metis_term_from_atp tm of
blanchet@43104
   130
       Metis_Term.Fn x => x
blanchet@43104
   131
     | _ => raise Fail "non CNF -- expected function")
blanchet@43092
   132
  | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
blanchet@43092
   133
fun metis_literal_from_atp (AConn (ANot, [phi])) =
blanchet@43092
   134
    (false, metis_atom_from_atp phi)
blanchet@43092
   135
  | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
blanchet@43268
   136
fun metis_literals_from_atp (AConn (AOr, phis)) =
blanchet@43268
   137
    maps metis_literals_from_atp phis
blanchet@43092
   138
  | metis_literals_from_atp phi = [metis_literal_from_atp phi]
blanchet@43092
   139
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
blanchet@43173
   140
    let
blanchet@43173
   141
      fun some isa =
blanchet@43173
   142
        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
blanchet@43173
   143
                  |> Metis_Thm.axiom, isa)
blanchet@43173
   144
    in
blanchet@43173
   145
      if ident = type_tag_idempotence_helper_name orelse
blanchet@43173
   146
         String.isPrefix lightweight_tags_sym_formula_prefix ident then
blanchet@43173
   147
        Isa_Reflexive_or_Trivial |> some
blanchet@43173
   148
      else if String.isPrefix helper_prefix ident then
blanchet@43194
   149
        case (String.isSuffix typed_helper_suffix ident,
blanchet@43194
   150
              space_explode "_" ident) of
blanchet@43194
   151
          (needs_fairly_sound, _ :: const :: j :: _) =>
blanchet@43194
   152
          nth ((const, needs_fairly_sound)
blanchet@43194
   153
               |> AList.lookup (op =) helper_table |> the)
blanchet@43173
   154
              (the (Int.fromString j) - 1)
blanchet@43194
   155
          |> prepare_helper
blanchet@43194
   156
          |> Isa_Raw |> some
blanchet@43173
   157
        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
blanchet@43173
   158
      else case try (unprefix conjecture_prefix) ident of
blanchet@43173
   159
        SOME s =>
blanchet@43173
   160
        let val j = the (Int.fromString s) in
blanchet@43173
   161
          if j = length clauses then NONE
blanchet@43173
   162
          else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
blanchet@43173
   163
        end
blanchet@43173
   164
      | NONE => TrueI |> Isa_Raw |> some
blanchet@43173
   165
    end
blanchet@43092
   166
  | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
blanchet@43092
   167
blanchet@39497
   168
(* Function to generate metis clauses, including comb and type clauses *)
blanchet@43212
   169
fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
blanchet@43212
   170
  let
blanchet@43212
   171
    val type_sys = type_sys_from_string type_sys
blanchet@43212
   172
    val clauses =
blanchet@43212
   173
      conj_clauses @ fact_clauses
blanchet@43212
   174
      |> (if polymorphism_of_type_sys type_sys = Polymorphic then
blanchet@43212
   175
            I
blanchet@43212
   176
          else
blanchet@43212
   177
            map (pair 0)
blanchet@43232
   178
            #> rpair ctxt
blanchet@43248
   179
            #-> Monomorph.monomorph atp_schematic_consts_of
blanchet@43212
   180
            #> fst #> maps (map (zero_var_indexes o snd)))
blanchet@43212
   181
    val (old_skolems, props) =
blanchet@43212
   182
      fold_rev (fn clause => fn (old_skolems, props) =>
blanchet@43212
   183
                   clause |> prop_of |> Logic.strip_imp_concl
blanchet@43212
   184
                          |> conceal_old_skolem_terms (length clauses)
blanchet@43212
   185
                                                      old_skolems
blanchet@43212
   186
                          ||> (fn prop => prop :: props))
blanchet@43212
   187
           clauses ([], [])
blanchet@43193
   188
(*
blanchet@43193
   189
val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
blanchet@43193
   190
*)
blanchet@43212
   191
    val (atp_problem, _, _, _, _, _, sym_tab) =
blanchet@43259
   192
      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
blanchet@43259
   193
                          @{prop False} []
blanchet@43193
   194
(*
blanchet@43224
   195
val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
blanchet@43193
   196
*)
blanchet@43212
   197
    (* "rev" is for compatibility *)
blanchet@43212
   198
    val axioms =
blanchet@43212
   199
      atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
blanchet@43212
   200
                  |> rev
blanchet@43212
   201
  in (sym_tab, axioms, old_skolems) end
blanchet@39497
   202
paulson@15347
   203
end;