don't pass "~ " to new Metis
authorblanchet
Mon Jun 06 20:36:35 2011 +0200 (2011-06-06)
changeset 43173b98daa96d043
parent 43172 ea57961db57e
child 43174 f497a1e97d37
don't pass "~ " to new Metis
src/HOL/Tools/Metis/metis_translate.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -318,25 +318,29 @@
     1.4      uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
     1.5    | metis_literals_from_atp phi = [metis_literal_from_atp phi]
     1.6  fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
     1.7 -    (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
     1.8 -         |> Metis_Thm.axiom,
     1.9 -     if ident = type_tag_idempotence_helper_name orelse
    1.10 -        String.isPrefix lightweight_tags_sym_formula_prefix ident then
    1.11 -       Isa_Reflexive_or_Trivial
    1.12 -     else if String.isPrefix helper_prefix ident then
    1.13 -       case space_explode "_" ident  of
    1.14 -         _ :: const :: j :: _ =>
    1.15 -         Isa_Raw (nth (AList.lookup (op =) helper_table const |> the |> snd)
    1.16 -                      (the (Int.fromString j) - 1)
    1.17 -                  |> prepare_helper)
    1.18 -       | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    1.19 -     else case try (unprefix conjecture_prefix) ident of
    1.20 -       SOME s =>
    1.21 -       let val j = the (Int.fromString s) in
    1.22 -         Isa_Raw (if j = length clauses then TrueI
    1.23 -                  else Meson.make_meta_clause (nth clauses j))
    1.24 -       end
    1.25 -     | NONE => Isa_Raw TrueI)
    1.26 +    let
    1.27 +      fun some isa =
    1.28 +        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
    1.29 +                  |> Metis_Thm.axiom, isa)
    1.30 +    in
    1.31 +      if ident = type_tag_idempotence_helper_name orelse
    1.32 +         String.isPrefix lightweight_tags_sym_formula_prefix ident then
    1.33 +        Isa_Reflexive_or_Trivial |> some
    1.34 +      else if String.isPrefix helper_prefix ident then
    1.35 +        case space_explode "_" ident  of
    1.36 +          _ :: const :: j :: _ =>
    1.37 +          nth (AList.lookup (op =) helper_table const |> the |> snd)
    1.38 +              (the (Int.fromString j) - 1)
    1.39 +          |> prepare_helper |> Isa_Raw |> some
    1.40 +        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    1.41 +      else case try (unprefix conjecture_prefix) ident of
    1.42 +        SOME s =>
    1.43 +        let val j = the (Int.fromString s) in
    1.44 +          if j = length clauses then NONE
    1.45 +          else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
    1.46 +        end
    1.47 +      | NONE => TrueI |> Isa_Raw |> some
    1.48 +    end
    1.49    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    1.50  
    1.51  val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
    1.52 @@ -359,7 +363,7 @@
    1.53          prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
    1.54                              false false (map prop_of clauses) @{prop False} []
    1.55        val axioms =
    1.56 -        atp_problem |> maps (map (metis_axiom_from_atp clauses) o snd)
    1.57 +        atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
    1.58      in
    1.59        (MX, sym_tab,
    1.60         {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})