src/HOL/Tools/Metis/metis_translate.ML
changeset 43295 30aaab778416
parent 43268 c0eaa8b9bff5
child 43304 6901ebafbb8d
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 16:20:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 16:20:19 2011 +0200
     1.3 @@ -145,6 +145,8 @@
     1.4        if ident = type_tag_idempotence_helper_name orelse
     1.5           String.isPrefix lightweight_tags_sym_formula_prefix ident then
     1.6          Isa_Reflexive_or_Trivial |> some
     1.7 +      else if String.isPrefix conjecture_prefix ident then
     1.8 +        NONE
     1.9        else if String.isPrefix helper_prefix ident then
    1.10          case (String.isSuffix typed_helper_suffix ident,
    1.11                space_explode "_" ident) of
    1.12 @@ -155,12 +157,11 @@
    1.13            |> prepare_helper
    1.14            |> Isa_Raw |> some
    1.15          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    1.16 -      else case try (unprefix conjecture_prefix) ident of
    1.17 +      else case try (unprefix fact_prefix) ident of
    1.18          SOME s =>
    1.19 -        let val j = the (Int.fromString s) in
    1.20 -          if j = length clauses then NONE
    1.21 -          else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
    1.22 -        end
    1.23 +        let
    1.24 +          val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
    1.25 +        in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
    1.26        | NONE => TrueI |> Isa_Raw |> some
    1.27      end
    1.28    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    1.29 @@ -169,31 +170,40 @@
    1.30  fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
    1.31    let
    1.32      val type_sys = type_sys_from_string type_sys
    1.33 +    val (conj_clauses, fact_clauses) =
    1.34 +      if polymorphism_of_type_sys type_sys = Polymorphic then
    1.35 +        (conj_clauses, fact_clauses)
    1.36 +      else
    1.37 +        conj_clauses @ fact_clauses
    1.38 +        |> map (pair 0)
    1.39 +        |> rpair ctxt
    1.40 +        |-> Monomorph.monomorph atp_schematic_consts_of
    1.41 +        |> fst |> chop (length conj_clauses)
    1.42 +        |> pairself (maps (map (zero_var_indexes o snd)))
    1.43 +    val num_conjs = length conj_clauses
    1.44      val clauses =
    1.45 -      conj_clauses @ fact_clauses
    1.46 -      |> (if polymorphism_of_type_sys type_sys = Polymorphic then
    1.47 -            I
    1.48 -          else
    1.49 -            map (pair 0)
    1.50 -            #> rpair ctxt
    1.51 -            #-> Monomorph.monomorph atp_schematic_consts_of
    1.52 -            #> fst #> maps (map (zero_var_indexes o snd)))
    1.53 +      map2 (fn j => pair (Int.toString j, Local))
    1.54 +           (0 upto num_conjs - 1) conj_clauses @
    1.55 +      (* "General" below isn't quite correct; the fact could be local. *)
    1.56 +      map2 (fn j => pair (Int.toString (num_conjs + j), General))
    1.57 +           (0 upto length fact_clauses - 1) fact_clauses
    1.58      val (old_skolems, props) =
    1.59 -      fold_rev (fn clause => fn (old_skolems, props) =>
    1.60 -                   clause |> prop_of |> Logic.strip_imp_concl
    1.61 -                          |> conceal_old_skolem_terms (length clauses)
    1.62 -                                                      old_skolems
    1.63 -                          ||> (fn prop => prop :: props))
    1.64 -           clauses ([], [])
    1.65 -(*
    1.66 -val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
    1.67 -*)
    1.68 +      fold_rev (fn (name, th) => fn (old_skolems, props) =>
    1.69 +                   th |> prop_of |> Logic.strip_imp_concl
    1.70 +                      |> conceal_old_skolem_terms (length clauses) old_skolems
    1.71 +                      ||> (fn prop => (name, prop) :: props))
    1.72 +               clauses ([], [])
    1.73 +    (*
    1.74 +    val _ =
    1.75 +      tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
    1.76 +    *)
    1.77      val (atp_problem, _, _, _, _, _, sym_tab) =
    1.78 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
    1.79 -                          @{prop False} []
    1.80 -(*
    1.81 -val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
    1.82 -*)
    1.83 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false []
    1.84 +                          @{prop False} props
    1.85 +    (*
    1.86 +    val _ = tracing ("ATP PROBLEM: " ^
    1.87 +                     cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
    1.88 +    *)
    1.89      (* "rev" is for compatibility *)
    1.90      val axioms =
    1.91        atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)