src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42521 02df3b78a438
parent 42520 d1f7c4a01dbe
child 42522 413b56894f82
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:23 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:23 2011 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4      -> translated_formula option * ((string * 'a) * thm)
     1.5    val unmangled_const : string -> string * string fo_term list
     1.6    val prepare_atp_problem :
     1.7 -    Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
     1.8 +    Proof.context -> bool -> type_system -> bool -> term list -> term
     1.9      -> (translated_formula option * ((string * 'a) * thm)) list
    1.10      -> string problem * string Symtab.table * int * (string * 'a) list vector
    1.11    val atp_problem_weights : string problem -> (string * real) list
    1.12 @@ -291,7 +291,7 @@
    1.13    metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
    1.14    |> Symtab.make
    1.15  
    1.16 -fun get_helper_facts ctxt explicit_forall type_sys formulas =
    1.17 +fun get_helper_facts ctxt type_sys formulas =
    1.18    let
    1.19      val no_dangerous_types = type_system_types_dangerous_types type_sys
    1.20      val ct = init_counters |> fold count_formula formulas
    1.21 @@ -317,7 +317,7 @@
    1.22         in
    1.23           [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
    1.24                 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
    1.25 -               |> explicit_forall ? close_universally, NONE)]
    1.26 +               |> close_universally, NONE)]
    1.27         end
    1.28       else
    1.29         [])
    1.30 @@ -652,7 +652,7 @@
    1.31    else
    1.32      t |> not (is_pred_sym pred_sym_tab s) ? boolify
    1.33  
    1.34 -fun repair_formula thy explicit_forall type_sys sym_tab =
    1.35 +fun repair_formula thy type_sys sym_tab =
    1.36    let
    1.37      val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab
    1.38      fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
    1.39 @@ -660,13 +660,11 @@
    1.40        | aux (AAtom tm) =
    1.41          AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
    1.42                    |> repair_predicates_in_term pred_sym_tab)
    1.43 -  in aux #> explicit_forall ? close_universally end
    1.44 +  in aux #> close_universally end
    1.45  
    1.46 -fun repair_problem_line thy explicit_forall type_sys sym_tab
    1.47 -                        (Fof (ident, kind, phi, source)) =
    1.48 -  Fof (ident, kind, repair_formula thy explicit_forall type_sys sym_tab phi,
    1.49 -       source)
    1.50 -fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
    1.51 +fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) =
    1.52 +  Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source)
    1.53 +fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
    1.54  
    1.55  fun dest_Fof (Fof z) = z
    1.56  
    1.57 @@ -682,8 +680,8 @@
    1.58      if heading = needle then j
    1.59      else offset_of_heading_in_problem needle problem (j + length lines)
    1.60  
    1.61 -fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
    1.62 -                        explicit_apply hyp_ts concl_t facts =
    1.63 +fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
    1.64 +                        concl_t facts =
    1.65    let
    1.66      val thy = Proof_Context.theory_of ctxt
    1.67      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
    1.68 @@ -699,13 +697,14 @@
    1.69         (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
    1.70         (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
    1.71      val sym_tab = sym_table_for_problem explicit_apply problem
    1.72 -    val problem = problem |> repair_problem thy explicit_forall type_sys sym_tab
    1.73 +    val problem = problem |> repair_problem thy type_sys sym_tab
    1.74 +    val helper_facts =
    1.75 +      get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
    1.76      val helper_lines =
    1.77 -      get_helper_facts ctxt explicit_forall type_sys
    1.78 -                       (maps (map (#3 o dest_Fof) o snd) problem)
    1.79 +      helper_facts
    1.80        |>> map (pair 0
    1.81                 #> problem_line_for_fact ctxt helper_prefix type_sys
    1.82 -               #> repair_problem_line thy explicit_forall type_sys sym_tab)
    1.83 +               #> repair_problem_line thy type_sys sym_tab)
    1.84        |> op @
    1.85      val (problem, pool) =
    1.86        problem |> AList.update (op =) (helpersN, helper_lines)