src/HOL/Tools/Metis/metis_translate.ML
author blanchet
Tue Nov 15 22:15:51 2011 +0100 (2011-11-15)
changeset 45512 a6cce8032fff
parent 45511 9b0f8ca4388e
child 45513 25388cf06437
permissions -rw-r--r--
rename configuration option to more reasonable length
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@44411
    12
  type type_enc = ATP_Translate.type_enc
blanchet@44411
    13
blanchet@43159
    14
  datatype isa_thm =
blanchet@43159
    15
    Isa_Reflexive_or_Trivial |
blanchet@45511
    16
    Isa_Lambda_Lifted |
blanchet@43159
    17
    Isa_Raw of thm
blanchet@43159
    18
blanchet@43094
    19
  val metis_equal : string
blanchet@43094
    20
  val metis_predicator : string
blanchet@43094
    21
  val metis_app_op : string
blanchet@44492
    22
  val metis_systematic_type_tag : string
blanchet@44492
    23
  val metis_ad_hoc_type_tag : string
blanchet@42098
    24
  val metis_generated_var_prefix : string
blanchet@43231
    25
  val trace : bool Config.T
blanchet@43231
    26
  val verbose : bool Config.T
blanchet@45512
    27
  val lambda_trans : string Config.T
blanchet@43231
    28
  val trace_msg : Proof.context -> (unit -> string) -> unit
blanchet@43231
    29
  val verbose_warning : Proof.context -> string -> unit
blanchet@44492
    30
  val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
blanchet@39886
    31
  val reveal_old_skolem_terms : (string * term) list -> term -> term
blanchet@45508
    32
  val reveal_lambda_lifted : (string * term) list -> term -> term
blanchet@40157
    33
  val prepare_metis_problem :
blanchet@45508
    34
    Proof.context -> type_enc -> string -> thm list -> thm list
blanchet@45508
    35
    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
blanchet@45508
    36
       * ((string * term) list * (string * term) list)
wenzelm@24310
    37
end
paulson@15347
    38
blanchet@39494
    39
structure Metis_Translate : METIS_TRANSLATE =
paulson@15347
    40
struct
paulson@15347
    41
blanchet@43092
    42
open ATP_Problem
blanchet@43085
    43
open ATP_Translate
paulson@15347
    44
blanchet@43094
    45
val metis_equal = "="
blanchet@43094
    46
val metis_predicator = "{}"
blanchet@44492
    47
val metis_app_op = Metis_Name.toString Metis_Term.appName
blanchet@44492
    48
val metis_systematic_type_tag =
blanchet@44492
    49
  Metis_Name.toString Metis_Term.hasTypeFunctionName
blanchet@44492
    50
val metis_ad_hoc_type_tag = "**"
blanchet@43085
    51
val metis_generated_var_prefix = "_"
quigley@17150
    52
blanchet@43231
    53
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
blanchet@43231
    54
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
blanchet@45512
    55
val lambda_trans =
blanchet@45512
    56
  Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN)
blanchet@43231
    57
blanchet@43231
    58
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@43231
    59
fun verbose_warning ctxt msg =
blanchet@43231
    60
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
blanchet@43231
    61
blanchet@43094
    62
val metis_name_table =
blanchet@44492
    63
  [((tptp_equal, 2), (K metis_equal, false)),
blanchet@44492
    64
   ((tptp_old_equal, 2), (K metis_equal, false)),
blanchet@44492
    65
   ((prefixed_predicator_name, 1), (K metis_predicator, false)),
blanchet@44492
    66
   ((prefixed_app_op_name, 2), (K metis_app_op, false)),
blanchet@44492
    67
   ((prefixed_type_tag_name, 2),
blanchet@44782
    68
    (fn type_enc =>
blanchet@44782
    69
        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
blanchet@44782
    70
        else metis_ad_hoc_type_tag, true))]
blanchet@43094
    71
blanchet@39896
    72
fun old_skolem_const_name i j num_T_args =
blanchet@39896
    73
  old_skolem_const_prefix ^ Long_Name.separator ^
wenzelm@41491
    74
  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
blanchet@37577
    75
blanchet@39886
    76
fun conceal_old_skolem_terms i old_skolems t =
blanchet@39953
    77
  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
blanchet@37577
    78
    let
blanchet@39886
    79
      fun aux old_skolems
blanchet@39953
    80
             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
blanchet@37577
    81
          let
blanchet@39886
    82
            val (old_skolems, s) =
blanchet@37577
    83
              if i = ~1 then
blanchet@39886
    84
                (old_skolems, @{const_name undefined})
blanchet@39886
    85
              else case AList.find (op aconv) old_skolems t of
blanchet@39886
    86
                s :: _ => (old_skolems, s)
blanchet@37577
    87
              | [] =>
blanchet@37577
    88
                let
blanchet@39896
    89
                  val s = old_skolem_const_name i (length old_skolems)
blanchet@39896
    90
                                                (length (Term.add_tvarsT T []))
blanchet@39886
    91
                in ((s, t) :: old_skolems, s) end
blanchet@39886
    92
          in (old_skolems, Const (s, T)) end
blanchet@39886
    93
        | aux old_skolems (t1 $ t2) =
blanchet@37577
    94
          let
blanchet@39886
    95
            val (old_skolems, t1) = aux old_skolems t1
blanchet@39886
    96
            val (old_skolems, t2) = aux old_skolems t2
blanchet@39886
    97
          in (old_skolems, t1 $ t2) end
blanchet@39886
    98
        | aux old_skolems (Abs (s, T, t')) =
blanchet@39886
    99
          let val (old_skolems, t') = aux old_skolems t' in
blanchet@39886
   100
            (old_skolems, Abs (s, T, t'))
blanchet@37577
   101
          end
blanchet@39886
   102
        | aux old_skolems t = (old_skolems, t)
blanchet@39886
   103
    in aux old_skolems t end
blanchet@37577
   104
  else
blanchet@39886
   105
    (old_skolems, t)
blanchet@37577
   106
blanchet@39886
   107
fun reveal_old_skolem_terms old_skolems =
blanchet@37632
   108
  map_aterms (fn t as Const (s, _) =>
blanchet@39896
   109
                 if String.isPrefix old_skolem_const_prefix s then
blanchet@39886
   110
                   AList.lookup (op =) old_skolems s |> the
blanchet@43826
   111
                   |> map_types (map_type_tvar (K dummyT))
blanchet@37632
   112
                 else
blanchet@37632
   113
                   t
blanchet@37632
   114
               | t => t)
blanchet@37632
   115
blanchet@45508
   116
fun reveal_lambda_lifted lambdas =
blanchet@45511
   117
  map_aterms (fn t as Const (s, _) =>
blanchet@45508
   118
                 if String.isPrefix lambda_lifted_prefix s then
blanchet@45508
   119
                   case AList.lookup (op =) lambdas s of
blanchet@45511
   120
                     SOME t =>
blanchet@45511
   121
                     Const (@{const_name Metis.lambda}, dummyT)
blanchet@45511
   122
                     $ map_types (map_type_tvar (K dummyT)) t
blanchet@45508
   123
                   | NONE => t
blanchet@45508
   124
                 else
blanchet@45508
   125
                   t
blanchet@45508
   126
               | t => t)
blanchet@45508
   127
blanchet@37577
   128
blanchet@39497
   129
(* ------------------------------------------------------------------------- *)
blanchet@39497
   130
(* Logic maps manage the interface between HOL and first-order logic.        *)
blanchet@39497
   131
(* ------------------------------------------------------------------------- *)
blanchet@39497
   132
blanchet@43159
   133
datatype isa_thm =
blanchet@43159
   134
  Isa_Reflexive_or_Trivial |
blanchet@45511
   135
  Isa_Lambda_Lifted |
blanchet@43159
   136
  Isa_Raw of thm
blanchet@43159
   137
blanchet@43159
   138
val proxy_defs = map (fst o snd o snd) proxy_table
blanchet@43159
   139
val prepare_helper =
blanchet@43159
   140
  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
blanchet@43159
   141
blanchet@44492
   142
fun metis_term_from_atp type_enc (ATerm (s, tms)) =
blanchet@43094
   143
  if is_tptp_variable s then
blanchet@43268
   144
    Metis_Term.Var (Metis_Name.fromString s)
blanchet@43094
   145
  else
blanchet@44492
   146
    (case AList.lookup (op =) metis_name_table (s, length tms) of
blanchet@44492
   147
       SOME (f, swap) => (f type_enc, swap)
blanchet@44492
   148
     | NONE => (s, false))
blanchet@44492
   149
    |> (fn (s, swap) =>
blanchet@44492
   150
           Metis_Term.Fn (Metis_Name.fromString s,
blanchet@44492
   151
                          tms |> map (metis_term_from_atp type_enc)
blanchet@44492
   152
                              |> swap ? rev))
blanchet@44492
   153
fun metis_atom_from_atp type_enc (AAtom tm) =
blanchet@44492
   154
    (case metis_term_from_atp type_enc tm of
blanchet@43104
   155
       Metis_Term.Fn x => x
blanchet@43104
   156
     | _ => raise Fail "non CNF -- expected function")
blanchet@44492
   157
  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
blanchet@44492
   158
fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
blanchet@44492
   159
    (false, metis_atom_from_atp type_enc phi)
blanchet@44492
   160
  | metis_literal_from_atp type_enc phi =
blanchet@44492
   161
    (true, metis_atom_from_atp type_enc phi)
blanchet@44492
   162
fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
blanchet@44492
   163
    maps (metis_literals_from_atp type_enc) phis
blanchet@44492
   164
  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
blanchet@44492
   165
fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
blanchet@43173
   166
    let
blanchet@43173
   167
      fun some isa =
blanchet@44492
   168
        SOME (phi |> metis_literals_from_atp type_enc
blanchet@44492
   169
                  |> Metis_LiteralSet.fromList
blanchet@43173
   170
                  |> Metis_Thm.axiom, isa)
blanchet@43173
   171
    in
blanchet@43173
   172
      if ident = type_tag_idempotence_helper_name orelse
blanchet@44396
   173
         String.isPrefix tags_sym_formula_prefix ident then
blanchet@43173
   174
        Isa_Reflexive_or_Trivial |> some
blanchet@43295
   175
      else if String.isPrefix conjecture_prefix ident then
blanchet@43295
   176
        NONE
blanchet@43173
   177
      else if String.isPrefix helper_prefix ident then
blanchet@43194
   178
        case (String.isSuffix typed_helper_suffix ident,
blanchet@43194
   179
              space_explode "_" ident) of
blanchet@43194
   180
          (needs_fairly_sound, _ :: const :: j :: _) =>
blanchet@43194
   181
          nth ((const, needs_fairly_sound)
blanchet@43194
   182
               |> AList.lookup (op =) helper_table |> the)
blanchet@43173
   183
              (the (Int.fromString j) - 1)
blanchet@43194
   184
          |> prepare_helper
blanchet@43194
   185
          |> Isa_Raw |> some
blanchet@43173
   186
        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
blanchet@43295
   187
      else case try (unprefix fact_prefix) ident of
blanchet@43173
   188
        SOME s =>
blanchet@45511
   189
        let val s = s |> space_explode "_" |> tl |> space_implode "_"
blanchet@45511
   190
          in
blanchet@45511
   191
          case Int.fromString s of
blanchet@45511
   192
            SOME j =>
blanchet@45511
   193
            Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
blanchet@45511
   194
          | NONE =>
blanchet@45511
   195
            if String.isPrefix lambda_fact_prefix (unascii_of s) then
blanchet@45511
   196
              Isa_Lambda_Lifted |> some
blanchet@45511
   197
            else
blanchet@45511
   198
              raise Fail ("malformed fact identifier " ^ quote ident)
blanchet@45511
   199
        end
blanchet@43173
   200
      | NONE => TrueI |> Isa_Raw |> some
blanchet@43173
   201
    end
blanchet@44492
   202
  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
blanchet@43092
   203
blanchet@39497
   204
(* Function to generate metis clauses, including comb and type clauses *)
blanchet@45508
   205
fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses =
blanchet@43212
   206
  let
blanchet@43295
   207
    val (conj_clauses, fact_clauses) =
blanchet@43626
   208
      if polymorphism_of_type_enc type_enc = Polymorphic then
blanchet@43295
   209
        (conj_clauses, fact_clauses)
blanchet@43295
   210
      else
blanchet@43295
   211
        conj_clauses @ fact_clauses
blanchet@43295
   212
        |> map (pair 0)
blanchet@45043
   213
        |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)
blanchet@43295
   214
        |-> Monomorph.monomorph atp_schematic_consts_of
blanchet@43295
   215
        |> fst |> chop (length conj_clauses)
blanchet@43295
   216
        |> pairself (maps (map (zero_var_indexes o snd)))
blanchet@43295
   217
    val num_conjs = length conj_clauses
blanchet@43212
   218
    val clauses =
blanchet@43295
   219
      map2 (fn j => pair (Int.toString j, Local))
blanchet@43295
   220
           (0 upto num_conjs - 1) conj_clauses @
blanchet@43295
   221
      (* "General" below isn't quite correct; the fact could be local. *)
blanchet@43295
   222
      map2 (fn j => pair (Int.toString (num_conjs + j), General))
blanchet@43295
   223
           (0 upto length fact_clauses - 1) fact_clauses
blanchet@43212
   224
    val (old_skolems, props) =
blanchet@43295
   225
      fold_rev (fn (name, th) => fn (old_skolems, props) =>
blanchet@43295
   226
                   th |> prop_of |> Logic.strip_imp_concl
blanchet@43295
   227
                      |> conceal_old_skolem_terms (length clauses) old_skolems
blanchet@43295
   228
                      ||> (fn prop => (name, prop) :: props))
blanchet@43295
   229
               clauses ([], [])
blanchet@43295
   230
    (*
blanchet@43295
   231
    val _ =
blanchet@45042
   232
      tracing ("PROPS:\n" ^
blanchet@45042
   233
               cat_lines (map (Syntax.string_of_term ctxt o snd) props))
blanchet@43295
   234
    *)
blanchet@45511
   235
    val lambda_trans =
blanchet@45511
   236
      if lambda_trans = combinatorsN then no_lambdasN else lambda_trans
blanchet@45508
   237
    val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
blanchet@45508
   238
      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
blanchet@45511
   239
                          false false [] @{prop False} props
blanchet@45510
   240
    (*
blanchet@43295
   241
    val _ = tracing ("ATP PROBLEM: " ^
blanchet@45508
   242
                     cat_lines (lines_for_atp_problem CNF atp_problem))
blanchet@45510
   243
    *)
blanchet@45508
   244
    (* "rev" is for compatibility with existing proof scripts. *)
blanchet@43212
   245
    val axioms =
blanchet@44492
   246
      atp_problem
blanchet@44492
   247
      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
blanchet@45508
   248
  in (sym_tab, axioms, (lifted, old_skolems)) end
blanchet@39497
   249
paulson@15347
   250
end;