src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42640 879d2d6b05ce
parent 42613 23b13b1bd565
child 42645 242bc53b98e5
equal deleted inserted replaced
42639:9d774c5d42a2 42640:879d2d6b05ce
     8 
     8 
     9 signature SLEDGEHAMMER_ATP_TRANSLATE =
     9 signature SLEDGEHAMMER_ATP_TRANSLATE =
    10 sig
    10 sig
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    12   type 'a problem = 'a ATP_Problem.problem
    12   type 'a problem = 'a ATP_Problem.problem
       
    13   type locality = Sledgehammer_Filter.locality
    13 
    14 
    14   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    15   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    15   datatype type_level =
    16   datatype type_level =
    16     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    17     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    17 
    18 
    35   val is_type_sys_virtually_sound : type_system -> bool
    36   val is_type_sys_virtually_sound : type_system -> bool
    36   val is_type_sys_fairly_sound : type_system -> bool
    37   val is_type_sys_fairly_sound : type_system -> bool
    37   val num_atp_type_args : theory -> type_system -> string -> int
    38   val num_atp_type_args : theory -> type_system -> string -> int
    38   val unmangled_const : string -> string * string fo_term list
    39   val unmangled_const : string -> string * string fo_term list
    39   val translate_atp_fact :
    40   val translate_atp_fact :
    40     Proof.context -> bool -> (string * 'a) * thm
    41     Proof.context -> bool -> (string * locality) * thm
    41     -> translated_formula option * ((string * 'a) * thm)
    42     -> translated_formula option * ((string * locality) * thm)
    42   val prepare_atp_problem :
    43   val prepare_atp_problem :
    43     Proof.context -> type_system -> bool -> term list -> term
    44     Proof.context -> type_system -> bool -> term list -> term
    44     -> (translated_formula option * ((string * 'a) * thm)) list
    45     -> (translated_formula option * ((string * 'a) * thm)) list
    45     -> string problem * string Symtab.table * int * int
    46     -> string problem * string Symtab.table * int * int
    46        * (string * 'a) list vector
    47        * (string * 'a) list vector
    51 struct
    52 struct
    52 
    53 
    53 open ATP_Problem
    54 open ATP_Problem
    54 open Metis_Translate
    55 open Metis_Translate
    55 open Sledgehammer_Util
    56 open Sledgehammer_Util
       
    57 open Sledgehammer_Filter
       
    58 
       
    59 (* experimental *)
       
    60 val generate_useful_info = false
    56 
    61 
    57 (* Readable names are often much shorter, especially if types are mangled in
    62 (* Readable names are often much shorter, especially if types are mangled in
    58    names. Also, the logic for generating legal SNARK sort names is only
    63    names. Also, the logic for generating legal SNARK sort names is only
    59    implemented for readable names. Finally, readable names are, well, more
    64    implemented for readable names. Finally, readable names are, well, more
    60    readable. For these reason, they are enabled by default. *)
    65    readable. For these reason, they are enabled by default. *)
   145   | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
   150   | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
   146   | formula_fold f (AAtom tm) = f tm
   151   | formula_fold f (AAtom tm) = f tm
   147 
   152 
   148 type translated_formula =
   153 type translated_formula =
   149   {name: string,
   154   {name: string,
       
   155    locality: locality,
   150    kind: formula_kind,
   156    kind: formula_kind,
   151    combformula: (name, typ, combterm) formula,
   157    combformula: (name, typ, combterm) formula,
   152    atomic_types: typ list}
   158    atomic_types: typ list}
   153 
   159 
   154 fun update_combformula f
   160 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
   155         ({name, kind, combformula, atomic_types} : translated_formula) =
   161                           : translated_formula) =
   156   {name = name, kind = kind, combformula = f combformula,
   162   {name = name, locality = locality, kind = kind, combformula = f combformula,
   157    atomic_types = atomic_types} : translated_formula
   163    atomic_types = atomic_types} : translated_formula
   158 
   164 
   159 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
   165 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
   160 
   166 
   161 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
   167 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
   403         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   409         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   404       | aux t = t
   410       | aux t = t
   405   in t |> exists_subterm is_Var t ? aux end
   411   in t |> exists_subterm is_Var t ? aux end
   406 
   412 
   407 (* making fact and conjecture formulas *)
   413 (* making fact and conjecture formulas *)
   408 fun make_formula ctxt eq_as_iff presimp name kind t =
   414 fun make_formula ctxt eq_as_iff presimp name loc kind t =
   409   let
   415   let
   410     val thy = Proof_Context.theory_of ctxt
   416     val thy = Proof_Context.theory_of ctxt
   411     val t = t |> Envir.beta_eta_contract
   417     val t = t |> Envir.beta_eta_contract
   412               |> transform_elim_term
   418               |> transform_elim_term
   413               |> Object_Logic.atomize_term thy
   419               |> Object_Logic.atomize_term thy
   419               |> introduce_combinators_in_term ctxt kind
   425               |> introduce_combinators_in_term ctxt kind
   420               |> kind <> Axiom ? freeze_term
   426               |> kind <> Axiom ? freeze_term
   421     val (combformula, atomic_types) =
   427     val (combformula, atomic_types) =
   422       combformula_from_prop thy eq_as_iff t []
   428       combformula_from_prop thy eq_as_iff t []
   423   in
   429   in
   424     {name = name, combformula = combformula, kind = kind,
   430     {name = name, locality = loc, kind = kind, combformula = combformula,
   425      atomic_types = atomic_types}
   431      atomic_types = atomic_types}
   426   end
   432   end
   427 
   433 
   428 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) =
   434 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
   429   case (keep_trivial, make_formula ctxt eq_as_iff presimp name Axiom t) of
   435   case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
   430     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   436     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   431     NONE
   437     NONE
   432   | (_, formula) => SOME formula
   438   | (_, formula) => SOME formula
   433 
   439 
   434 fun make_conjecture ctxt ts =
   440 fun make_conjecture ctxt ts =
   435   let val last = length ts - 1 in
   441   let val last = length ts - 1 in
   436     map2 (fn j => make_formula ctxt true true (string_of_int j)
   442     map2 (fn j => make_formula ctxt true true (string_of_int j) Chained
   437                                (if j = last then Conjecture else Hypothesis))
   443                                (if j = last then Conjecture else Hypothesis))
   438          (0 upto last) ts
   444          (0 upto last) ts
   439   end
   445   end
   440 
   446 
   441 (** "hBOOL" and "hAPP" **)
   447 (** "hBOOL" and "hAPP" **)
   580     let
   586     let
   581       val thy = Proof_Context.theory_of ctxt
   587       val thy = Proof_Context.theory_of ctxt
   582       val unmangled_s = mangled_s |> unmangled_const_name
   588       val unmangled_s = mangled_s |> unmangled_const_name
   583       fun dub_and_inst c needs_some_types (th, j) =
   589       fun dub_and_inst c needs_some_types (th, j) =
   584         ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
   590         ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
   585           false),
   591           Chained),
   586          let val t = th |> prop_of in
   592          let val t = th |> prop_of in
   587            t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
   593            t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
   588                  not (null (Term.hidden_polymorphism t)))
   594                  not (null (Term.hidden_polymorphism t)))
   589                 ? (case typ of
   595                 ? (case typ of
   590                      SOME T => specialize_type thy (invert_const unmangled_s, T)
   596                      SOME T => specialize_type thy (invert_const unmangled_s, T)
   738                 (atp_type_literals_for_types type_sys Axiom atomic_types))
   744                 (atp_type_literals_for_types type_sys Axiom atomic_types))
   739            (formula_from_combformula ctxt type_sys
   745            (formula_from_combformula ctxt type_sys
   740                 (close_combformula_universally combformula))
   746                 (close_combformula_universally combformula))
   741   |> close_formula_universally
   747   |> close_formula_universally
   742 
   748 
       
   749 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
       
   750 
   743 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   751 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   744    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   752    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   745    the remote provers might care. *)
   753    the remote provers might care. *)
   746 fun formula_line_for_fact ctxt prefix type_sys
   754 fun formula_line_for_fact ctxt prefix type_sys
   747                           (j, formula as {name, kind, ...}) =
   755                           (j, formula as {name, locality, kind, ...}) =
   748   Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   756   Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   749            formula_for_fact ctxt type_sys formula, NONE, NONE)
   757            formula_for_fact ctxt type_sys formula, NONE,
       
   758            if generate_useful_info then
       
   759              case locality of
       
   760                Intro => useful_isabelle_info "intro"
       
   761              | Elim => useful_isabelle_info "elim"
       
   762              | Simp => useful_isabelle_info "simp"
       
   763              | _ => NONE
       
   764            else
       
   765              NONE)
   750 
   766 
   751 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
   767 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
   752                                                        superclass, ...}) =
   768                                                        superclass, ...}) =
   753   let val ty_arg = ATerm (`I "T", []) in
   769   let val ty_arg = ATerm (`I "T", []) in
   754     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
   770     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,