src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 37516 c81c86bfc18a
parent 37509 f39464d971c4
child 37538 97ab019d5ac8
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 23 12:43:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 23 14:36:23 2010 +0200
     1.3 @@ -26,6 +26,8 @@
     1.4  open Sledgehammer_Fact_Filter
     1.5  open Sledgehammer_TPTP_Format
     1.6  
     1.7 +exception METIS of string * string
     1.8 +
     1.9  val trace = Unsynchronized.ref false;
    1.10  fun trace_msg msg = if !trace then tracing (msg ()) else ();
    1.11  
    1.12 @@ -435,10 +437,8 @@
    1.13              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
    1.14              Syntax.string_of_term ctxt (term_of y)))));
    1.15    in cterm_instantiate substs' i_th end
    1.16 -  handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
    1.17 -       | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
    1.18 -                             "\n(Perhaps you want to try \"metisFT\" if you \
    1.19 -                             \haven't done so already.)")
    1.20 +  handle THM (msg, _, _) => raise METIS ("inst_inf", msg)
    1.21 +       | ERROR msg => raise METIS ("inst_inf", msg)
    1.22  
    1.23  (* INFERENCE RULE: RESOLVE *)
    1.24  
    1.25 @@ -507,7 +507,7 @@
    1.26                  val adjustment = get_ty_arg_size thy tm1
    1.27                  val p' = if adjustment > p then p else p-adjustment
    1.28                  val tm_p = List.nth(args,p')
    1.29 -                  handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
    1.30 +                  handle Subscript => raise METIS ("equality_inf", Int.toString p ^ " adj " ^
    1.31                      Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
    1.32                  val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
    1.33                                        "  " ^ Syntax.string_of_term ctxt tm_p)
    1.34 @@ -599,7 +599,7 @@
    1.35              length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
    1.36        in
    1.37            if nprems_of th = n_metis_lits then ()
    1.38 -          else error "Metis: proof reconstruction has gone wrong";
    1.39 +          else raise METIS ("translate", "Proof reconstruction has gone wrong.");
    1.40            translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
    1.41        end;
    1.42  
    1.43 @@ -723,9 +723,7 @@
    1.44  
    1.45  fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
    1.46  
    1.47 -exception METIS of string;
    1.48 -
    1.49 -(* Main function to start metis proof and reconstruction *)
    1.50 +(* Main function to start Metis proof and reconstruction *)
    1.51  fun FOL_SOLVE mode ctxt cls ths0 =
    1.52    let val thy = ProofContext.theory_of ctxt
    1.53        val th_cls_pairs =
    1.54 @@ -776,40 +774,48 @@
    1.55                          (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    1.56                           [ith])
    1.57                    | _ => (trace_msg (fn () => "Metis: No result");
    1.58 -                          [])
    1.59 +                          raise METIS ("FOL_SOLVE", ""))
    1.60              end
    1.61          | Metis.Resolution.Satisfiable _ =>
    1.62              (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
    1.63 -             [])
    1.64 +             raise METIS ("FOL_SOLVE", ""))
    1.65    end;
    1.66  
    1.67 -fun metis_general_tac mode ctxt ths i st0 =
    1.68 +fun generic_metis_tac mode ctxt ths i st0 =
    1.69    let val _ = trace_msg (fn () =>
    1.70          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    1.71    in
    1.72 -    if exists_type type_has_topsort (prop_of st0)
    1.73 -    then raise METIS "Metis: Proof state contains the universal sort {}"
    1.74 +    if exists_type type_has_topsort (prop_of st0) then
    1.75 +      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
    1.76      else
    1.77        (Meson.MESON (maps neg_clausify)
    1.78 -        (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
    1.79 -          THEN Meson_Tactic.expand_defs_tac st0) st0
    1.80 +                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    1.81 +                   ctxt i
    1.82 +       THEN Meson_Tactic.expand_defs_tac st0) st0
    1.83 +     handle ERROR msg => raise METIS ("generic_metis_tac", msg)
    1.84    end
    1.85 -  handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
    1.86 +  handle METIS (loc, msg) =>
    1.87 +         if mode = HO then
    1.88 +           (warning ("Metis: Falling back on \"metisFT\".");
    1.89 +            generic_metis_tac FT ctxt ths i st0)
    1.90 +         else if msg = "" then
    1.91 +           Seq.empty
    1.92 +         else
    1.93 +           raise error ("Metis (" ^ loc ^ "): " ^ msg)
    1.94  
    1.95 -val metis_tac = metis_general_tac HO;
    1.96 -val metisF_tac = metis_general_tac FO;
    1.97 -val metisFT_tac = metis_general_tac FT;
    1.98 +val metis_tac = generic_metis_tac HO
    1.99 +val metisF_tac = generic_metis_tac FO
   1.100 +val metisFT_tac = generic_metis_tac FT
   1.101  
   1.102 -fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   1.103 -  SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   1.104 +fun method name mode =
   1.105 +  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   1.106 +    SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths)))
   1.107  
   1.108  val setup =
   1.109 -  type_lits_setup #>
   1.110 -  method @{binding metis} HO "METIS for FOL and HOL problems" #>
   1.111 -  method @{binding metisF} FO "METIS for FOL problems" #>
   1.112 -  method @{binding metisFT} FT "METIS with fully-typed translation" #>
   1.113 -  Method.setup @{binding finish_clausify}
   1.114 -    (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
   1.115 -    "cleanup after conversion to clauses";
   1.116 +  type_lits_setup
   1.117 +  #> method @{binding metis} HO "Metis for FOL/HOL problems"
   1.118 +  #> method @{binding metisF} FO "Metis for FOL problems"
   1.119 +  #> method @{binding metisFT} FT
   1.120 +            "Metis for FOL/HOL problems with fully-typed translation"
   1.121  
   1.122  end;