wneuper/isa: src/HOL/Tools/Metis/metis

     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

     7 Translation of HOL to FOL for Metis.

     8 *)

    10 signature METIS_GENERATE =

    11 sig

    12   type type_enc = ATP_Problem_Generate.type_enc

    14   datatype isa_thm =

    15     Isa_Reflexive_or_Trivial |

    16     Isa_Lambda_Lifted |

    17     Isa_Raw of thm

    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 prepare_metis_problem :

    33     Proof.context -> type_enc -> string -> thm list -> thm list

    34     -> int Symtab.table * (Metis_Thm.thm * isa_thm) list

    35        * (unit -> (string * int) list)

    36        * ((string * term) list * (string * term) list)

    37 end

    39 structure Metis_Generate : METIS_GENERATE =

    40 struct

    42 open ATP_Problem

    43 open ATP_Problem_Generate

    45 val metis_equal = "="

    46 val metis_predicator = "{}"

    47 val metis_app_op = Metis_Name.toString Metis_Term.appName

    48 val metis_systematic_type_tag =

    49   Metis_Name.toString Metis_Term.hasTypeFunctionName

    50 val metis_ad_hoc_type_tag = "**"

    51 val metis_generated_var_prefix = "_"

    53 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)

    54 val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)

    56 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()

    57 fun verbose_warning ctxt msg =

    58   if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()

    60 val metis_name_table =

    61   [((tptp_equal, 2), (K metis_equal, false)),

    62    ((tptp_old_equal, 2), (K metis_equal, false)),

    63    ((prefixed_predicator_name, 1), (K metis_predicator, false)),

    64    ((prefixed_app_op_name, 2), (K metis_app_op, false)),

    65    ((prefixed_type_tag_name, 2),

    66     (fn type_enc =>

    67         if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag

    68         else metis_ad_hoc_type_tag, true))]

    70 fun old_skolem_const_name i j num_T_args =

    71   old_skolem_const_prefix ^ Long_Name.separator ^

    72   (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))

    74 fun conceal_old_skolem_terms i old_skolems t =

    75   if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then

    76     let

    77       fun aux old_skolems

    78              (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =

    79           let

    80             val (old_skolems, s) =

    81               if i = ~1 then

    82                 (old_skolems, @{const_name undefined})

    83               else case AList.find (op aconv) old_skolems t of

    84                 s :: _ => (old_skolems, s)

    85               | [] =>

    86                 let

    87                   val s = old_skolem_const_name i (length old_skolems)

    88                                                 (length (Term.add_tvarsT T []))

    89                 in ((s, t) :: old_skolems, s) end

    90           in (old_skolems, Const (s, T)) end

    91         | aux old_skolems (t1 $ t2) =

    92           let

    93             val (old_skolems, t1) = aux old_skolems t1

    94             val (old_skolems, t2) = aux old_skolems t2

    95           in (old_skolems, t1 $ t2) end

    96         | aux old_skolems (Abs (s, T, t')) =

    97           let val (old_skolems, t') = aux old_skolems t' in

    98             (old_skolems, Abs (s, T, t'))

    99           end

   100         | aux old_skolems t = (old_skolems, t)

   101     in aux old_skolems t end

   102   else

   103     (old_skolems, t)

   105 fun reveal_old_skolem_terms old_skolems =

   106   map_aterms (fn t as Const (s, _) =>

   107                  if String.isPrefix old_skolem_const_prefix s then

   108                    AList.lookup (op =) old_skolems s |> the

   109                    |> map_types (map_type_tvar (K dummyT))

   110                  else

   111                    t

   112                | t => t)

   114 fun reveal_lam_lifted lambdas =

   115   map_aterms (fn t as Const (s, _) =>

   116                  if String.isPrefix lam_lifted_prefix s then

   117                    case AList.lookup (op =) lambdas s of

   118                      SOME t =>

   119                      Const (@{const_name Metis.lambda}, dummyT)

   120                      $ map_types (map_type_tvar (K dummyT))

   121                                  (reveal_lam_lifted lambdas t)

   122                    | NONE => t

   123                  else

   124                    t

   125                | t => t)

   128 (* ------------------------------------------------------------------------- *)

   129 (* Logic maps manage the interface between HOL and first-order logic.        *)

   130 (* ------------------------------------------------------------------------- *)

   132 datatype isa_thm =

   133   Isa_Reflexive_or_Trivial |

   134   Isa_Lambda_Lifted |

   135   Isa_Raw of thm

   137 val proxy_defs = map (fst o snd o snd) proxy_table

   138 val prepare_helper =

   139   Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)

   141 fun metis_term_from_atp type_enc (ATerm (s, tms)) =

   142   if is_tptp_variable s then

   143     Metis_Term.Var (Metis_Name.fromString s)

   144   else

   145     (case AList.lookup (op =) metis_name_table (s, length tms) of

   146        SOME (f, swap) => (f type_enc, swap)

   147      | NONE => (s, false))

   148     |> (fn (s, swap) =>

   149            Metis_Term.Fn (Metis_Name.fromString s,

   150                           tms |> map (metis_term_from_atp type_enc)

   151                               |> swap ? rev))

   152 fun metis_atom_from_atp type_enc (AAtom tm) =

   153     (case metis_term_from_atp type_enc tm of

   154        Metis_Term.Fn x => x

   155      | _ => raise Fail "non CNF -- expected function")

   156   | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"

   157 fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =

   158     (false, metis_atom_from_atp type_enc phi)

   159   | metis_literal_from_atp type_enc phi =

   160     (true, metis_atom_from_atp type_enc phi)

   161 fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =

   162     maps (metis_literals_from_atp type_enc) phis

   163   | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]

   164 fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =

   165     let

   166       fun some isa =

   167         SOME (phi |> metis_literals_from_atp type_enc

   168                   |> Metis_LiteralSet.fromList

   169                   |> Metis_Thm.axiom, isa)

   170     in

   171       if ident = type_tag_idempotence_helper_name orelse

   172          String.isPrefix tags_sym_formula_prefix ident then

   173         Isa_Reflexive_or_Trivial |> some

   174       else if String.isPrefix conjecture_prefix ident then

   175         NONE

   176       else if String.isPrefix helper_prefix ident then

   177         case (String.isSuffix typed_helper_suffix ident,

   178               space_explode "_" ident) of

   179           (needs_fairly_sound, _ :: const :: j :: _) =>

   180           nth ((const, needs_fairly_sound)

   181                |> AList.lookup (op =) helper_table |> the)

   182               (the (Int.fromString j) - 1)

   183           |> prepare_helper

   184           |> Isa_Raw |> some

   185         | _ => raise Fail ("malformed helper identifier " ^ quote ident)

   186       else case try (unprefix fact_prefix) ident of

   187         SOME s =>

   188         let val s = s |> space_explode "_" |> tl |> space_implode "_"

   189           in

   190           case Int.fromString s of

   191             SOME j =>

   192             Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some

   193           | NONE =>

   194             if String.isPrefix lam_fact_prefix (unascii_of s) then

   195               Isa_Lambda_Lifted |> some

   196             else

   197               raise Fail ("malformed fact identifier " ^ quote ident)

   198         end

   199       | NONE => TrueI |> Isa_Raw |> some

   200     end

   201   | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"

   203 fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =

   204     eliminate_lam_wrappers t

   205   | eliminate_lam_wrappers (t $ u) =

   206     eliminate_lam_wrappers t $ eliminate_lam_wrappers u

   207   | eliminate_lam_wrappers (Abs (s, T, t)) =

   208     Abs (s, T, eliminate_lam_wrappers t)

   209   | eliminate_lam_wrappers t = t

   211 (* Function to generate metis clauses, including comb and type clauses *)

   212 fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =

   213   let

   214     val (conj_clauses, fact_clauses) =

   215       if polymorphism_of_type_enc type_enc = Polymorphic then

   216         (conj_clauses, fact_clauses)

   217       else

   218         conj_clauses @ fact_clauses

   219         |> map (pair 0)

   220         |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)

   221         |-> Monomorph.monomorph atp_schematic_consts_of

   222         |> fst |> chop (length conj_clauses)

   223         |> pairself (maps (map (zero_var_indexes o snd)))

   224     val num_conjs = length conj_clauses

   225     (* Pretend every clause is a "simp" rule, to guide the term ordering. *)

   226     val clauses =

   227       map2 (fn j => pair (Int.toString j, (Local, Simp)))

   228            (0 upto num_conjs - 1) conj_clauses @

   229       map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))

   230            (0 upto length fact_clauses - 1) fact_clauses

   231     val (old_skolems, props) =

   232       fold_rev (fn (name, th) => fn (old_skolems, props) =>

   233                    th |> prop_of |> Logic.strip_imp_concl

   234                       |> conceal_old_skolem_terms (length clauses) old_skolems

   235                       ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN)

   236                           ? eliminate_lam_wrappers

   237                       ||> (fn prop => (name, prop) :: props))

   238                clauses ([], [])

   239     (*

   240     val _ =

   241       tracing ("PROPS:\n" ^

   242                cat_lines (map (Syntax.string_of_term ctxt o snd) props))

   243     *)

   244     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans

   245     val (atp_problem, _, _, lifted, sym_tab) =

   246       prepare_atp_problem ctxt CNF Hypothesis Hypothesis type_enc false

   247                           lam_trans false false false [] @{prop False} props

   248     (*

   249     val _ = tracing ("ATP PROBLEM: " ^

   250                      cat_lines (lines_for_atp_problem CNF atp_problem))

   251     *)

   252     (* "rev" is for compatibility with existing proof scripts. *)

   253     val axioms =

   254       atp_problem

   255       |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev

   256     fun ord_info () = atp_problem_term_order_info atp_problem

   257   in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end

   259 end;

author	blanchet
	Tue, 20 Mar 2012 10:06:35 +0100
changeset 47910	1b36a05a070d
parent 47237	d4754183ccce
child 47917	62ca06cc5a99
permissions	-rw-r--r--