src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42525 7a506b0b644f
parent 42524 3df98f0de5a0
child 42526 46d485f8d144
equal deleted inserted replaced
42524:3df98f0de5a0 42525:7a506b0b644f
    52 (* Freshness almost guaranteed! *)
    52 (* Freshness almost guaranteed! *)
    53 val sledgehammer_weak_prefix = "Sledgehammer:"
    53 val sledgehammer_weak_prefix = "Sledgehammer:"
    54 
    54 
    55 type translated_formula =
    55 type translated_formula =
    56   {name: string,
    56   {name: string,
    57    kind: kind,
    57    kind: formula_kind,
    58    combformula: (name, combterm) formula,
    58    combformula: (name, combterm) formula,
    59    ctypes_sorts: typ list}
    59    ctypes_sorts: typ list}
    60 
    60 
    61 datatype type_system =
    61 datatype type_system =
    62   Many_Typed |
    62   Many_Typed |
   309      if type_sys = Tags false then
   309      if type_sys = Tags false then
   310        let
   310        let
   311          fun var s = ATerm (`I s, [])
   311          fun var s = ATerm (`I s, [])
   312          fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   312          fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   313        in
   313        in
   314          [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
   314          [(Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
   315                AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   315            AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   316                |> close_formula_universally, NONE)]
   316            |> close_formula_universally, NONE)]
   317        end
   317        end
   318      else
   318      else
   319        [])
   319        [])
   320   end
   320   end
   321 
   321 
   496   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   496   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   497                 (atp_type_literals_for_types type_sys Axiom ctypes_sorts))
   497                 (atp_type_literals_for_types type_sys Axiom ctypes_sorts))
   498            (formula_for_combformula ctxt type_sys
   498            (formula_for_combformula ctxt type_sys
   499                                     (close_combformula_universally combformula))
   499                                     (close_combformula_universally combformula))
   500 
   500 
       
   501 fun logic_for_type_sys Many_Typed = Tff
       
   502   | logic_for_type_sys _ = Fof
       
   503 
   501 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   504 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   502    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   505    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   503    the remote provers might care. *)
   506    the remote provers might care. *)
   504 fun problem_line_for_fact ctxt prefix type_sys
   507 fun problem_line_for_fact ctxt prefix type_sys
   505                           (j, formula as {name, kind, ...}) =
   508                           (j, formula as {name, kind, ...}) =
   506   Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
   509   (logic_for_type_sys type_sys, prefix ^ string_of_int j ^ "_" ^ ascii_of name,
   507        formula_for_fact ctxt type_sys formula, NONE)
   510    kind, formula_for_fact ctxt type_sys formula, NONE)
   508 
   511 
   509 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   512 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   510                                                        superclass, ...}) =
   513                                                        superclass, ...}) =
   511   let val ty_arg = ATerm (("T", "T"), []) in
   514   let val ty_arg = ATerm (("T", "T"), []) in
   512     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   515     (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
   513          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   516      AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   514                            AAtom (ATerm (superclass, [ty_arg]))]), NONE)
   517                        AAtom (ATerm (superclass, [ty_arg]))]), NONE)
   515   end
   518   end
   516 
   519 
   517 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   520 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   518     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   521     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   519   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   522   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   520     (false, ATerm (c, [ATerm (sort, [])]))
   523     (false, ATerm (c, [ATerm (sort, [])]))
   521 
   524 
   522 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   525 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   523                                                 ...}) =
   526                                                 ...}) =
   524   Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   527   (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
   525        mk_ahorn (map (formula_for_fo_literal o apfst not
   528    mk_ahorn (map (formula_for_fo_literal o apfst not
   526                       o fo_literal_for_arity_literal) premLits)
   529                   o fo_literal_for_arity_literal) premLits)
   527                 (formula_for_fo_literal
   530             (formula_for_fo_literal
   528                      (fo_literal_for_arity_literal conclLit)), NONE)
   531                  (fo_literal_for_arity_literal conclLit)), NONE)
   529 
   532 
   530 fun problem_line_for_conjecture ctxt type_sys
   533 fun problem_line_for_conjecture ctxt type_sys
   531         ({name, kind, combformula, ...} : translated_formula) =
   534         ({name, kind, combformula, ...} : translated_formula) =
   532   Fof (conjecture_prefix ^ name, kind,
   535   (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
   533        formula_for_combformula ctxt type_sys
   536    formula_for_combformula ctxt type_sys
   534                                (close_combformula_universally combformula),
   537                            (close_combformula_universally combformula), NONE)
   535        NONE)
       
   536 
   538 
   537 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   539 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   538   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   540   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   539                |> map fo_literal_for_type_literal
   541                |> map fo_literal_for_type_literal
   540 
   542 
   541 fun problem_line_for_free_type j lit =
   543 fun problem_line_for_free_type j lit =
   542   Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
   544   (Fof, tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
   543        NONE)
   545    NONE)
   544 fun problem_lines_for_free_types type_sys facts =
   546 fun problem_lines_for_free_types type_sys facts =
   545   let
   547   let
   546     val litss = map (free_type_literals type_sys) facts
   548     val litss = map (free_type_literals type_sys) facts
   547     val lits = fold (union (op =)) litss []
   549     val lits = fold (union (op =)) litss []
   548   in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   550   in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   566   #> fold (consider_term (top_level andalso s = type_tag_name)) ts
   568   #> fold (consider_term (top_level andalso s = type_tag_name)) ts
   567 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   569 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   568   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   570   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   569   | consider_formula (AAtom tm) = consider_term true tm
   571   | consider_formula (AAtom tm) = consider_term true tm
   570 
   572 
   571 fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi
   573 fun consider_problem_line (_, _, _, phi, _) = consider_formula phi
   572 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   574 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   573 
   575 
   574 (* needed for helper facts if the problem otherwise does not involve equality *)
   576 (* needed for helper facts if the problem otherwise does not involve equality *)
   575 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false})
   577 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false})
   576 
   578 
   657       | aux (AAtom tm) =
   659       | aux (AAtom tm) =
   658         AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
   660         AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
   659                   |> repair_predicates_in_term pred_sym_tab)
   661                   |> repair_predicates_in_term pred_sym_tab)
   660   in aux #> close_formula_universally end
   662   in aux #> close_formula_universally end
   661 
   663 
   662 fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) =
   664 fun repair_problem_line thy type_sys sym_tab (logic, ident, kind, phi, source) =
   663   Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source)
   665   (logic, ident, kind, repair_formula thy type_sys sym_tab phi, source)
   664 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
   666 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
   665 
       
   666 fun dest_Fof (Fof z) = z
       
   667 
   667 
   668 val factsN = "Relevant facts"
   668 val factsN = "Relevant facts"
   669 val class_relsN = "Class relationships"
   669 val class_relsN = "Class relationships"
   670 val aritiesN = "Arity declarations"
   670 val aritiesN = "Arity declarations"
   671 val helpersN = "Helper facts"
   671 val helpersN = "Helper facts"
   694        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   694        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   695        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
   695        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
   696     val sym_tab = sym_table_for_problem explicit_apply problem
   696     val sym_tab = sym_table_for_problem explicit_apply problem
   697     val problem = problem |> repair_problem thy type_sys sym_tab
   697     val problem = problem |> repair_problem thy type_sys sym_tab
   698     val helper_facts =
   698     val helper_facts =
   699       get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
   699       get_helper_facts ctxt type_sys (maps (map #4 o snd) problem)
   700     val helper_lines =
   700     val helper_lines =
   701       helper_facts
   701       helper_facts
   702       |>> map (pair 0
   702       |>> map (pair 0
   703                #> problem_line_for_fact ctxt helper_prefix type_sys
   703                #> problem_line_for_fact ctxt helper_prefix type_sys
   704                #> repair_problem_line thy type_sys sym_tab)
   704                #> repair_problem_line thy type_sys sym_tab)
   720 val fact_max_weight = 1.0
   720 val fact_max_weight = 1.0
   721 
   721 
   722 fun add_term_weights weight (ATerm (s, tms)) =
   722 fun add_term_weights weight (ATerm (s, tms)) =
   723   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   723   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   724   #> fold (add_term_weights weight) tms
   724   #> fold (add_term_weights weight) tms
   725 fun add_problem_line_weights weight (Fof (_, _, phi, _)) =
   725 fun add_problem_line_weights weight (_, _, _, phi, _) =
   726   fold_formula (add_term_weights weight) phi
   726   fold_formula (add_term_weights weight) phi
   727 
   727 
   728 fun add_conjectures_weights [] = I
   728 fun add_conjectures_weights [] = I
   729   | add_conjectures_weights conjs =
   729   | add_conjectures_weights conjs =
   730     let val (hyps, conj) = split_last conjs in
   730     let val (hyps, conj) = split_last conjs in