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