src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42545 a14b602fb3d5
parent 42544 75cb06eee990
child 42546 8591fcc56c34
equal deleted inserted replaced
42544:75cb06eee990 42545:a14b602fb3d5
   527         val (x, ty_args) =
   527         val (x, ty_args) =
   528           case head of
   528           case head of
   529             CombConst (name as (s, s'), _, ty_args) =>
   529             CombConst (name as (s, s'), _, ty_args) =>
   530             (case AList.lookup (op =) fname_table s of
   530             (case AList.lookup (op =) fname_table s of
   531                SOME (n, fname) =>
   531                SOME (n, fname) =>
   532 (*### FIXME: do earlier? *)
       
   533                (if top_level andalso length args = n then
   532                (if top_level andalso length args = n then
   534                   case s of
   533                   case s of
   535                     "c_False" => ("$false", s')
   534                     "c_False" => ("$false", s')
   536                   | "c_True" => ("$true", s')
   535                   | "c_True" => ("$true", s')
   537                   | _ => name
   536                   | _ => name
   582   | logic_for_type_sys _ = Fof
   581   | logic_for_type_sys _ = Fof
   583 
   582 
   584 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   583 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   585    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   584    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   586    the remote provers might care. *)
   585    the remote provers might care. *)
   587 fun problem_line_for_fact ctxt prefix type_sys
   586 fun formula_line_for_fact ctxt prefix type_sys
   588                           (j, formula as {name, kind, ...}) =
   587                           (j, formula as {name, kind, ...}) =
   589   Formula (logic_for_type_sys type_sys,
   588   Formula (logic_for_type_sys type_sys,
   590            prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   589            prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   591            formula_for_fact ctxt type_sys formula, NONE, NONE)
   590            formula_for_fact ctxt type_sys formula, NONE, NONE)
   592 
   591 
   593 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   592 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
   594                                                        superclass, ...}) =
   593                                                        superclass, ...}) =
   595   let val ty_arg = ATerm (`I "T", []) in
   594   let val ty_arg = ATerm (`I "T", []) in
   596     Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
   595     Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
   597              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   596              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   598                                AAtom (ATerm (superclass, [ty_arg]))])
   597                                AAtom (ATerm (superclass, [ty_arg]))])
   602 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   601 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   603     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   602     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   604   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   603   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   605     (false, ATerm (c, [ATerm (sort, [])]))
   604     (false, ATerm (c, [ATerm (sort, [])]))
   606 
   605 
   607 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   606 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   608                                                 ...}) =
   607                                                 ...}) =
   609   Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
   608   Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
   610            mk_ahorn (map (formula_for_fo_literal o apfst not
   609            mk_ahorn (map (formula_for_fo_literal o apfst not
   611                           o fo_literal_for_arity_literal) premLits)
   610                           o fo_literal_for_arity_literal) premLits)
   612                     (formula_for_fo_literal
   611                     (formula_for_fo_literal
   613                          (fo_literal_for_arity_literal conclLit))
   612                          (fo_literal_for_arity_literal conclLit))
   614            |> close_formula_universally, NONE, NONE)
   613            |> close_formula_universally, NONE, NONE)
   615 
   614 
   616 fun problem_line_for_conjecture ctxt type_sys
   615 fun formula_line_for_conjecture ctxt type_sys
   617         ({name, kind, combformula, ...} : translated_formula) =
   616         ({name, kind, combformula, ...} : translated_formula) =
   618   Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
   617   Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
   619            formula_for_combformula ctxt type_sys
   618            formula_for_combformula ctxt type_sys
   620                                    (close_combformula_universally combformula)
   619                                    (close_combformula_universally combformula)
   621            |> close_formula_universally, NONE, NONE)
   620            |> close_formula_universally, NONE, NONE)
   622 
   621 
   623 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   622 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   624   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   623   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   625                |> map fo_literal_for_type_literal
   624                |> map fo_literal_for_type_literal
   626 
   625 
   627 fun problem_line_for_free_type j lit =
   626 fun formula_line_for_free_type j lit =
   628   Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
   627   Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
   629            formula_for_fo_literal lit, NONE, NONE)
   628            formula_for_fo_literal lit, NONE, NONE)
   630 fun problem_lines_for_free_types type_sys facts =
   629 fun formula_lines_for_free_types type_sys facts =
   631   let
   630   let
   632     val litss = map (free_type_literals type_sys) facts
   631     val litss = map (free_type_literals type_sys) facts
   633     val lits = fold (union (op =)) litss []
   632     val lits = fold (union (op =)) litss []
   634   in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   633   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   635 
   634 
   636 (** "hBOOL" and "hAPP" **)
   635 (** "hBOOL" and "hAPP" **)
   637 
   636 
   638 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
   637 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
   639 
   638 
   658 
   657 
   659 fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
   658 fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
   660   formula_fold (consider_combterm_for_repair true) combformula
   659   formula_fold (consider_combterm_for_repair true) combformula
   661 
   660 
   662 (* The "equal" entry is needed for helper facts if the problem otherwise does
   661 (* The "equal" entry is needed for helper facts if the problem otherwise does
   663    not involve equality. The "hBOOL" and "hAPP" entries are needed for symbol
   662    not involve equality. The "hBOOL" entry is needed to ensure that no "hAPP"s
   664    declarations. *)
   663    are introduced for passing arguments to it. *)
   665 val default_entries =
   664 val default_entries =
   666   [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
   665   [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
   667    (make_fixed_const boolify_base,
   666    (make_fixed_const boolify_base,
   668     {pred_sym = true, min_arity = 1, max_arity = 1}),
   667     {pred_sym = true, min_arity = 1, max_arity = 1})]
   669    (make_fixed_const explicit_app_base,
       
   670     {pred_sym = false, min_arity = 2, max_arity = 2})]
       
   671 (* FIXME: last two entries needed? ### *)
       
   672 
   668 
   673 fun sym_table_for_facts explicit_apply facts =
   669 fun sym_table_for_facts explicit_apply facts =
   674   if explicit_apply then
   670   if explicit_apply then
   675     NONE
   671     NONE
   676   else
   672   else
   765 
   761 
   766 fun consider_fact_consts type_sys sym_tab
   762 fun consider_fact_consts type_sys sym_tab
   767                          ({combformula, ...} : translated_formula) =
   763                          ({combformula, ...} : translated_formula) =
   768   formula_fold (consider_combterm_consts type_sys sym_tab) combformula
   764   formula_fold (consider_combterm_consts type_sys sym_tab) combformula
   769 
   765 
       
   766 (* FIXME: needed? *)
   770 fun const_table_for_facts type_sys sym_tab facts =
   767 fun const_table_for_facts type_sys sym_tab facts =
   771   Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
   768   Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
   772                   ? fold (consider_fact_consts type_sys sym_tab) facts
   769                   ? fold (consider_fact_consts type_sys sym_tab) facts
   773 
   770 
   774 fun strip_and_map_combtyp 0 f ty = ([], f ty)
   771 fun strip_and_map_combtyp 0 f ty = ([], f ty)
   777        (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
   774        (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
   778        strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
   775        strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
   779      | _ => ([], f ty))
   776      | _ => ([], f ty))
   780   | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
   777   | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
   781 
   778 
   782 fun sym_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
   779 fun problem_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
   783   let
   780   let
   784     val thy = Proof_Context.theory_of ctxt
   781     val thy = Proof_Context.theory_of ctxt
   785     val arity = min_arity_of thy type_sys sym_tab s
   782     val arity = min_arity_of thy type_sys sym_tab s
   786   in
   783   in
   787     if type_sys = Many_Typed then
   784     if type_sys = Many_Typed then
   808                  |> mk_aquant AForall bounds
   805                  |> mk_aquant AForall bounds
   809                  |> formula_for_combformula ctxt type_sys,
   806                  |> formula_for_combformula ctxt type_sys,
   810                  NONE, NONE)
   807                  NONE, NONE)
   811       end
   808       end
   812   end
   809   end
   813 fun sym_decl_lines_for_const ctxt type_sys sym_tab (s, xs) =
   810 fun problem_lines_for_const ctxt type_sys sym_tab (s, xs) =
   814   map (sym_decl_line_for_const_entry ctxt type_sys sym_tab s) xs
   811   map (problem_line_for_const_entry ctxt type_sys sym_tab s) xs
   815 
   812 
   816 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   813 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   817     union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   814     union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   818   | add_tff_types_in_formula (AConn (_, phis)) =
   815   | add_tff_types_in_formula (AConn (_, phis)) =
   819     fold add_tff_types_in_formula phis
   816     fold add_tff_types_in_formula phis
   825     add_tff_types_in_formula phi
   822     add_tff_types_in_formula phi
   826 
   823 
   827 fun tff_types_in_problem problem =
   824 fun tff_types_in_problem problem =
   828   fold (fold add_tff_types_in_problem_line o snd) problem []
   825   fold (fold add_tff_types_in_problem_line o snd) problem []
   829 
   826 
   830 fun problem_line_for_tff_type (s, s') =
   827 fun decl_line_for_tff_type (s, s') =
   831   Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
   828   Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
   832 
   829 
   833 val type_declsN = "Types"
   830 val type_declsN = "Types"
   834 val sym_declsN = "Symbol types"
   831 val sym_declsN = "Symbol types"
   835 val factsN = "Relevant facts"
   832 val factsN = "Relevant facts"
   857     (* Reordering these might confuse the proof reconstruction code or the SPASS
   854     (* Reordering these might confuse the proof reconstruction code or the SPASS
   858        Flotter hack. *)
   855        Flotter hack. *)
   859     val problem =
   856     val problem =
   860       [(type_declsN, []),
   857       [(type_declsN, []),
   861        (sym_declsN, []),
   858        (sym_declsN, []),
   862        (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
   859        (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys)
   863                     (0 upto length facts - 1 ~~ facts)),
   860                     (0 upto length facts - 1 ~~ facts)),
   864        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
   861        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   865        (aritiesN, map problem_line_for_arity_clause arity_clauses),
   862        (aritiesN, map formula_line_for_arity_clause arity_clauses),
   866        (helpersN, []),
   863        (helpersN, []),
   867        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   864        (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
   868        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
   865        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
   869     val helper_facts =
   866     val helper_facts =
   870       problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
   867       problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
   871                                     | _ => NONE) o snd)
   868                                     | _ => NONE) o snd)
   872               |> get_helper_facts ctxt type_sys
   869               |> get_helper_facts ctxt type_sys
   873               |>> map (repair_fact thy type_sys sym_tab)
   870               |>> map (repair_fact thy type_sys sym_tab)
   874     val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
   871     val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
   875     val sym_decl_lines =
   872     val sym_decl_lines =
   876       Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys sym_tab)
   873       Symtab.fold_rev (append o problem_lines_for_const ctxt type_sys sym_tab)
   877                       const_tab []
   874                       const_tab []
   878     val helper_lines =
   875     val helper_lines =
   879       helper_facts
   876       helper_facts
   880       |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys)
   877       |>> map (pair 0 #> formula_line_for_fact ctxt helper_prefix type_sys)
   881       |> op @
   878       |> op @
   882     val problem =
   879     val problem =
   883       problem |> fold (AList.update (op =))
   880       problem |> fold (AList.update (op =))
   884                       [(sym_declsN, sym_decl_lines),
   881                       [(sym_declsN, sym_decl_lines),
   885                        (helpersN, helper_lines)]
   882                        (helpersN, helper_lines)]
   886     val type_decl_lines =
   883     val type_decl_lines =
   887       if type_sys = Many_Typed then
   884       if type_sys = Many_Typed then
   888         problem |> tff_types_in_problem |> map problem_line_for_tff_type
   885         problem |> tff_types_in_problem |> map decl_line_for_tff_type
   889       else
   886       else
   890         []
   887         []
   891     val (problem, pool) =
   888     val (problem, pool) =
   892       problem |> AList.update (op =) (type_declsN, type_decl_lines)
   889       problem |> AList.update (op =) (type_declsN, type_decl_lines)
   893               |> nice_atp_problem readable_names
   890               |> nice_atp_problem readable_names