src/HOL/Tools/Metis/metis_generate.ML
author wenzelm
Tue Jun 02 09:16:19 2015 +0200 (2015-06-02)
changeset 60358 aebfbcab1eb8
parent 59877 a04ea4709c8d
child 61860 2ce3d12015b3
permissions -rw-r--r--
clarified context;
blanchet@46320
     1
(*  Title:      HOL/Tools/Metis/metis_generate.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@46320
    10
signature METIS_GENERATE =
wenzelm@24310
    11
sig
blanchet@46320
    12
  type type_enc = ATP_Problem_Generate.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@43231
    27
  val trace_msg : Proof.context -> (unit -> string) -> unit
blanchet@43231
    28
  val verbose_warning : Proof.context -> string -> unit
blanchet@44492
    29
  val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
blanchet@39886
    30
  val reveal_old_skolem_terms : (string * term) list -> term -> term
blanchet@45569
    31
  val reveal_lam_lifted : (string * term) list -> term -> term
blanchet@57263
    32
  val generate_metis_problem : Proof.context -> type_enc -> string -> thm list -> thm list ->
blanchet@57263
    33
    int Symtab.table * (Metis_Thm.thm * isa_thm) list * (unit -> (string * int) list)
blanchet@57263
    34
    * ((string * term) list * (string * term) list)
wenzelm@24310
    35
end
paulson@15347
    36
blanchet@46320
    37
structure Metis_Generate : METIS_GENERATE =
paulson@15347
    38
struct
paulson@15347
    39
blanchet@43092
    40
open ATP_Problem
blanchet@46320
    41
open ATP_Problem_Generate
paulson@15347
    42
blanchet@43094
    43
val metis_equal = "="
blanchet@43094
    44
val metis_predicator = "{}"
blanchet@44492
    45
val metis_app_op = Metis_Name.toString Metis_Term.appName
blanchet@44492
    46
val metis_systematic_type_tag =
blanchet@44492
    47
  Metis_Name.toString Metis_Term.hasTypeFunctionName
blanchet@44492
    48
val metis_ad_hoc_type_tag = "**"
blanchet@43085
    49
val metis_generated_var_prefix = "_"
quigley@17150
    50
blanchet@43231
    51
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
blanchet@43231
    52
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
blanchet@43231
    53
blanchet@43231
    54
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@43231
    55
fun verbose_warning ctxt msg =
blanchet@43231
    56
  if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
blanchet@43231
    57
blanchet@43094
    58
val metis_name_table =
blanchet@44492
    59
  [((tptp_equal, 2), (K metis_equal, false)),
blanchet@44492
    60
   ((tptp_old_equal, 2), (K metis_equal, false)),
blanchet@44492
    61
   ((prefixed_predicator_name, 1), (K metis_predicator, false)),
blanchet@44492
    62
   ((prefixed_app_op_name, 2), (K metis_app_op, false)),
blanchet@44492
    63
   ((prefixed_type_tag_name, 2),
blanchet@44782
    64
    (fn type_enc =>
blanchet@44782
    65
        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
blanchet@44782
    66
        else metis_ad_hoc_type_tag, true))]
blanchet@43094
    67
blanchet@39896
    68
fun old_skolem_const_name i j num_T_args =
wenzelm@59877
    69
  Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args])
blanchet@37577
    70
blanchet@39886
    71
fun conceal_old_skolem_terms i old_skolems t =
blanchet@39953
    72
  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
blanchet@37577
    73
    let
blanchet@39886
    74
      fun aux old_skolems
blanchet@39953
    75
             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
blanchet@37577
    76
          let
blanchet@39886
    77
            val (old_skolems, s) =
blanchet@37577
    78
              if i = ~1 then
blanchet@39886
    79
                (old_skolems, @{const_name undefined})
blanchet@57408
    80
              else
blanchet@57408
    81
                (case AList.find (op aconv) old_skolems t of
blanchet@57408
    82
                  s :: _ => (old_skolems, s)
blanchet@57408
    83
                | [] =>
blanchet@57408
    84
                  let
blanchet@57408
    85
                    val s =
blanchet@57408
    86
                      old_skolem_const_name i (length old_skolems) (length (Term.add_tvarsT T []))
blanchet@57408
    87
                  in ((s, t) :: old_skolems, s) end)
blanchet@39886
    88
          in (old_skolems, Const (s, T)) end
blanchet@39886
    89
        | aux old_skolems (t1 $ t2) =
blanchet@37577
    90
          let
blanchet@39886
    91
            val (old_skolems, t1) = aux old_skolems t1
blanchet@39886
    92
            val (old_skolems, t2) = aux old_skolems t2
blanchet@39886
    93
          in (old_skolems, t1 $ t2) end
blanchet@39886
    94
        | aux old_skolems (Abs (s, T, t')) =
blanchet@39886
    95
          let val (old_skolems, t') = aux old_skolems t' in
blanchet@39886
    96
            (old_skolems, Abs (s, T, t'))
blanchet@37577
    97
          end
blanchet@39886
    98
        | aux old_skolems t = (old_skolems, t)
blanchet@39886
    99
    in aux old_skolems t end
blanchet@37577
   100
  else
blanchet@39886
   101
    (old_skolems, t)
blanchet@37577
   102
blanchet@39886
   103
fun reveal_old_skolem_terms old_skolems =
blanchet@37632
   104
  map_aterms (fn t as Const (s, _) =>
blanchet@57408
   105
      if String.isPrefix old_skolem_const_prefix s then
blanchet@57408
   106
        AList.lookup (op =) old_skolems s |> the
blanchet@57408
   107
        |> map_types (map_type_tvar (K dummyT))
blanchet@57408
   108
      else
blanchet@57408
   109
        t
blanchet@57408
   110
    | t => t)
blanchet@37632
   111
blanchet@52150
   112
fun reveal_lam_lifted lifted =
blanchet@45511
   113
  map_aterms (fn t as Const (s, _) =>
blanchet@57408
   114
      if String.isPrefix lam_lifted_prefix s then
blanchet@57408
   115
        (case AList.lookup (op =) lifted s of
blanchet@57408
   116
          SOME t =>
blanchet@57408
   117
          Const (@{const_name Metis.lambda}, dummyT)
blanchet@57408
   118
          $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
blanchet@57408
   119
        | NONE => t)
blanchet@57408
   120
      else
blanchet@57408
   121
        t
blanchet@57408
   122
    | t => t)
blanchet@45508
   123
blanchet@37577
   124
blanchet@39497
   125
(* ------------------------------------------------------------------------- *)
blanchet@39497
   126
(* Logic maps manage the interface between HOL and first-order logic.        *)
blanchet@39497
   127
(* ------------------------------------------------------------------------- *)
blanchet@39497
   128
blanchet@43159
   129
datatype isa_thm =
blanchet@43159
   130
  Isa_Reflexive_or_Trivial |
blanchet@45511
   131
  Isa_Lambda_Lifted |
blanchet@43159
   132
  Isa_Raw of thm
blanchet@43159
   133
blanchet@43159
   134
val proxy_defs = map (fst o snd o snd) proxy_table
wenzelm@54742
   135
fun prepare_helper ctxt =
wenzelm@60358
   136
  Meson.make_meta_clause ctxt #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
blanchet@43159
   137
blanchet@52031
   138
fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
blanchet@43094
   139
  if is_tptp_variable s then
blanchet@43268
   140
    Metis_Term.Var (Metis_Name.fromString s)
blanchet@43094
   141
  else
blanchet@44492
   142
    (case AList.lookup (op =) metis_name_table (s, length tms) of
blanchet@44492
   143
       SOME (f, swap) => (f type_enc, swap)
blanchet@44492
   144
     | NONE => (s, false))
blanchet@44492
   145
    |> (fn (s, swap) =>
blanchet@44492
   146
           Metis_Term.Fn (Metis_Name.fromString s,
blanchet@52031
   147
                          tms |> map (metis_term_of_atp type_enc)
blanchet@44492
   148
                              |> swap ? rev))
blanchet@52031
   149
fun metis_atom_of_atp type_enc (AAtom tm) =
blanchet@52031
   150
    (case metis_term_of_atp type_enc tm of
blanchet@43104
   151
       Metis_Term.Fn x => x
blanchet@43104
   152
     | _ => raise Fail "non CNF -- expected function")
blanchet@52031
   153
  | metis_atom_of_atp _ _ = raise Fail "not CNF -- expected atom"
blanchet@52031
   154
fun metis_literal_of_atp type_enc (AConn (ANot, [phi])) =
blanchet@52031
   155
    (false, metis_atom_of_atp type_enc phi)
blanchet@52031
   156
  | metis_literal_of_atp type_enc phi = (true, metis_atom_of_atp type_enc phi)
blanchet@52031
   157
fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
blanchet@52031
   158
    maps (metis_literals_of_atp type_enc) phis
blanchet@52031
   159
  | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
wenzelm@54742
   160
fun metis_axiom_of_atp ctxt type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
blanchet@43173
   161
    let
blanchet@43173
   162
      fun some isa =
blanchet@52031
   163
        SOME (phi |> metis_literals_of_atp type_enc
blanchet@44492
   164
                  |> Metis_LiteralSet.fromList
blanchet@43173
   165
                  |> Metis_Thm.axiom, isa)
blanchet@43173
   166
    in
blanchet@47046
   167
      if String.isPrefix tags_sym_formula_prefix ident then
blanchet@43173
   168
        Isa_Reflexive_or_Trivial |> some
blanchet@43295
   169
      else if String.isPrefix conjecture_prefix ident then
blanchet@43295
   170
        NONE
blanchet@43173
   171
      else if String.isPrefix helper_prefix ident then
blanchet@57408
   172
        (case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
blanchet@43194
   173
          (needs_fairly_sound, _ :: const :: j :: _) =>
blanchet@57263
   174
          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
blanchet@57263
   175
            (the (Int.fromString j) - 1)
wenzelm@54742
   176
          |> snd |> prepare_helper ctxt
blanchet@43194
   177
          |> Isa_Raw |> some
blanchet@57408
   178
        | _ => raise Fail ("malformed helper identifier " ^ quote ident))
blanchet@57408
   179
      else
blanchet@57408
   180
        (case try (unprefix fact_prefix) ident of
blanchet@57408
   181
          SOME s =>
blanchet@57408
   182
          let val s = s |> space_explode "_" |> tl |> space_implode "_" in
blanchet@57408
   183
            (case Int.fromString s of
wenzelm@60358
   184
              SOME j => Meson.make_meta_clause ctxt (snd (nth clauses j)) |> Isa_Raw |> some
blanchet@57408
   185
            | NONE =>
blanchet@57408
   186
              if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
blanchet@57408
   187
              else raise Fail ("malformed fact identifier " ^ quote ident))
blanchet@57408
   188
          end
blanchet@57408
   189
        | NONE => some (Isa_Raw TrueI))
blanchet@43173
   190
    end
wenzelm@54742
   191
  | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
blanchet@43092
   192
blanchet@57263
   193
fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = eliminate_lam_wrappers t
blanchet@57263
   194
  | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
blanchet@57263
   195
  | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
blanchet@45569
   196
  | eliminate_lam_wrappers t = t
blanchet@45569
   197
blanchet@39497
   198
(* Function to generate metis clauses, including comb and type clauses *)
blanchet@57263
   199
fun generate_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
blanchet@43212
   200
  let
blanchet@43295
   201
    val (conj_clauses, fact_clauses) =
blanchet@48131
   202
      if is_type_enc_polymorphic type_enc then
blanchet@43295
   203
        (conj_clauses, fact_clauses)
blanchet@43295
   204
      else
blanchet@43295
   205
        conj_clauses @ fact_clauses
blanchet@43295
   206
        |> map (pair 0)
blanchet@53479
   207
        |> Monomorph.monomorph atp_schematic_consts_of ctxt
blanchet@53479
   208
        |> chop (length conj_clauses)
wenzelm@59058
   209
        |> apply2 (maps (map (zero_var_indexes o snd)))
blanchet@43295
   210
    val num_conjs = length conj_clauses
blanchet@47039
   211
    (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
blanchet@43212
   212
    val clauses =
blanchet@57263
   213
      map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
blanchet@47039
   214
      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
blanchet@57263
   215
        (0 upto length fact_clauses - 1) fact_clauses
blanchet@43212
   216
    val (old_skolems, props) =
blanchet@43295
   217
      fold_rev (fn (name, th) => fn (old_skolems, props) =>
wenzelm@59582
   218
           th |> Thm.prop_of |> Logic.strip_imp_concl
blanchet@57263
   219
              |> conceal_old_skolem_terms (length clauses) old_skolems
blanchet@57263
   220
              ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
blanchet@57263
   221
              ||> (fn prop => (name, prop) :: props))
blanchet@57263
   222
         clauses ([], [])
blanchet@43295
   223
    (*
blanchet@43295
   224
    val _ =
blanchet@45042
   225
      tracing ("PROPS:\n" ^
blanchet@45042
   226
               cat_lines (map (Syntax.string_of_term ctxt o snd) props))
blanchet@43295
   227
    *)
blanchet@46365
   228
    val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
blanchet@57263
   229
    val (atp_problem, _, lifted, sym_tab) =
blanchet@57263
   230
      generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
blanchet@57263
   231
        @{prop False} props
blanchet@45510
   232
    (*
blanchet@43295
   233
    val _ = tracing ("ATP PROBLEM: " ^
blanchet@51998
   234
                     cat_lines (lines_of_atp_problem CNF atp_problem))
blanchet@45510
   235
    *)
blanchet@45508
   236
    (* "rev" is for compatibility with existing proof scripts. *)
blanchet@57263
   237
    val axioms = atp_problem
wenzelm@54742
   238
      |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
blanchet@47039
   239
    fun ord_info () = atp_problem_term_order_info atp_problem
blanchet@57408
   240
  in
blanchet@57408
   241
    (sym_tab, axioms, ord_info, (lifted, old_skolems))
blanchet@57408
   242
  end
blanchet@39497
   243
paulson@15347
   244
end;