# HG changeset patch # User blanchet # Date 1276333867 -7200 # Node ID 12cb33916e3759357a8fea1f4bf8e3243438b563 # Parent e8c34222814b4d50c164630c55dd7ff5c9675bc4 "raise Fail" for internal errors + one new internal error (instead of "Match") diff -r e8c34222814b -r 12cb33916e37 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 11 18:05:05 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Jun 12 11:11:07 2010 +0200 @@ -85,7 +85,7 @@ val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis.Term.Var v - | _ => error "hol_term_to_fol_FO"; + | _ => raise Fail "hol_term_to_fol_FO"; fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = @@ -198,7 +198,7 @@ fun apply_list rator nargs rands = let val trands = terms_of rands in if length trands = nargs then Term (list_comb(rator, trands)) - else error + else raise Fail ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ " expected " ^ Int.toString nargs ^ " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) @@ -233,7 +233,7 @@ | NONE => case strip_prefix tfree_prefix x of SOME tf => mk_tfree ctxt tf - | NONE => error ("fol_type_to_isa: " ^ x)); + | NONE => raise Fail ("fol_type_to_isa: " ^ x)); fun reintroduce_skolem_Eps thy skolem_somes = let @@ -274,7 +274,7 @@ Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) | _ => case tm_to_tt rator of Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) - | _ => error "tm_to_tt: HO application" + | _ => raise Fail "tm_to_tt: HO application" end | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) and applic_to_tt ("=",ts) = @@ -289,12 +289,13 @@ val tys = types_of (List.take(tts,ntypes)) in if length tys = ntypes then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) - else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) + else + raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ + " but gets " ^ Int.toString (length tys) ^ + " type arguments\n" ^ + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ + " the terms are \n" ^ + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) case strip_prefix tconst_prefix a of @@ -308,11 +309,11 @@ SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end - | NONE => error ("unexpected metis function: " ^ a) + | NONE => raise Fail ("unexpected metis function: " ^ a) in case tm_to_tt fol_tm of Term t => t - | _ => error "fol_tm_to_tt: Term expected" + | _ => raise Fail "fol_tm_to_tt: Term expected" end (*Maps fully-typed metis terms to isabelle terms*) @@ -331,7 +332,7 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) - | NONE => error ("hol_term_from_fol_FT bad constant: " ^ x)) + | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = cvt tm1 $ cvt tm2 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) @@ -384,7 +385,8 @@ fun lookth thpairs (fth : Metis.Thm.thm) = the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) - handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); + handle Option => + raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); fun is_TrueI th = Thm.eq_thm(TrueI,th); @@ -477,10 +479,10 @@ val prems_th1 = prems_of i_th1 val prems_th2 = prems_of i_th2 val index_th1 = get_index (mk_not i_atm) prems_th1 - handle Empty => error "Failed to find literal in th1" + handle Empty => raise Fail "Failed to find literal in th1" val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) val index_th2 = get_index i_atm prems_th2 - handle Empty => error "Failed to find literal in th2" + handle Empty => raise Fail "Failed to find literal in th2" val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end end; @@ -525,6 +527,10 @@ fun path_finder_HO tm [] = (tm, Term.Bound 0) | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + | path_finder_HO tm ps = + raise Fail ("equality_inf, path_finder_HO: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm) fun path_finder_FT tm [] _ = (tm, Term.Bound 0) | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = path_finder_FT tm ps t1 @@ -532,10 +538,11 @@ (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis.Term.toString t) + | path_finder_FT tm ps t = + raise Fail ("equality_inf, path_finder_FT: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + " fol-term: " ^ Metis.Term.toString t) fun path_finder FO tm ps _ = path_finder_FO tm ps | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = (*equality: not curried, as other predicates are*) @@ -587,7 +594,7 @@ fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); -(* TODO: use "fold" instead *) +(* FIXME: use "fold" instead *) fun translate _ _ _ thpairs [] = thpairs | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) = let val _ = trace_msg (fn () => "=============================================") @@ -684,10 +691,11 @@ tfrees = union (op =) tfree_lits tfrees, skolem_somes = skolem_somes} end; - val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} - |> fold (add_thm true) cls - |> add_tfrees - |> fold (add_thm false) ths + val lmap as {skolem_somes, ...} = + {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} + |> fold (add_thm true) cls + |> add_tfrees + |> fold (add_thm false) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists (*Now check for the existence of certain combinators*) @@ -701,7 +709,10 @@ lmap |> mode <> FO ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) in - (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) + (mode, add_type_thm (type_ext thy + (* FIXME: Call"kill_skolem_Eps" here? *) + (map ((*snd o kill_skolem_Eps ~1 skolem_somes o*) prop_of) + (cls @ ths))) lmap) end; fun refute cls =