--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 16 17:30:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Fri Sep 17 00:35:19 2010 +0200
@@ -27,24 +27,24 @@
val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
-datatype term_or_type = Term of Term.term | Type of Term.typ;
+datatype term_or_type = SomeTerm of term | SomeType of typ
fun terms_of [] = []
- | terms_of (Term t :: tts) = t :: terms_of tts
- | terms_of (Type _ :: tts) = terms_of tts;
+ | terms_of (SomeTerm t :: tts) = t :: terms_of tts
+ | terms_of (SomeType _ :: tts) = terms_of tts;
fun types_of [] = []
- | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
+ | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
if String.isPrefix "_" a then
(*Variable generated by Metis, which might have been a type variable.*)
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
else types_of tts
- | types_of (Term _ :: tts) = types_of tts
- | types_of (Type T :: tts) = T :: types_of tts;
+ | types_of (SomeTerm _ :: tts) = types_of tts
+ | types_of (SomeType T :: tts) = T :: types_of tts;
fun apply_list rator nargs rands =
let val trands = terms_of rands
- in if length trands = nargs then Term (list_comb(rator, trands))
+ in if length trands = nargs then SomeTerm (list_comb(rator, trands))
else raise Fail
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
" expected " ^ Int.toString nargs ^
@@ -57,7 +57,7 @@
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
with variable constraints in the goal...at least, type inference often fails otherwise.
SEE ALSO axiom_inf below.*)
-fun mk_var (w,T) = Term.Var((w,1), T);
+fun mk_var (w, T) = Var ((w, 1), T)
(*include the default sort, if available*)
fun mk_tfree ctxt w =
@@ -79,8 +79,8 @@
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
(case strip_prefix_and_unascii type_const_prefix x of
- SOME tc => Term.Type (smart_invert_const tc,
- map (hol_type_from_metis_term ctxt) tys)
+ SOME tc => Type (smart_invert_const tc,
+ map (hol_type_from_metis_term ctxt) tys)
| NONE =>
case strip_prefix_and_unascii tfree_prefix x of
SOME tf => mk_tfree ctxt tf
@@ -93,11 +93,11 @@
Metis_Term.toString fol_tm)
fun tm_to_tt (Metis_Term.Var v) =
(case strip_prefix_and_unascii tvar_prefix v of
- SOME w => Type (make_tvar w)
+ SOME w => SomeType (make_tvar w)
| NONE =>
case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => Term (mk_var (w, HOLogic.typeT))
- | NONE => Term (mk_var (v, HOLogic.typeT)) )
+ SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
+ | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
| tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
| tm_to_tt (t as Metis_Term.Fn (".",_)) =
@@ -105,12 +105,12 @@
in case rator of
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)))
+ SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
| _ => 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) =
- Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
@@ -132,20 +132,20 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix_and_unascii type_const_prefix a of
SOME b =>
- Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
+ SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix_and_unascii tfree_prefix a of
- SOME b => Type (mk_tfree ctxt b)
+ SOME b => SomeType (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
case strip_prefix_and_unascii fixed_var_prefix a of
SOME b =>
- let val opr = Term.Free(b, HOLogic.typeT)
+ let val opr = Free (b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
| NONE => raise Fail ("unexpected metis function: " ^ a)
in
case tm_to_tt fol_tm of
- Term t => t
- | _ => raise Fail "fol_tm_to_tt: Term expected"
+ SomeTerm t => t
+ | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
end
(*Maps fully-typed metis terms to isabelle terms*)
@@ -237,25 +237,29 @@
(ProofContext.theory_of ctxt)
(singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
-(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying
+(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
sorts. Instead we try to arrange that new TVars are distinct and that types
- can be inferred from terms.*)
+ can be inferred from terms. *)
fun inst_inf ctxt mode skolems thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
- val i_th = lookth thpairs th
+ val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
- let val v = find_var x
- (* We call "reveal_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode ctxt y
- in SOME (cterm_of thy (Var v), t) end
- handle Option =>
- (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^
- " in " ^ Display.string_of_thm ctxt i_th);
- NONE)
+ let val v = find_var x
+ (* We call "reveal_skolem_terms" and "infer_types" below. *)
+ val t = hol_term_from_metis mode ctxt y
+ in SOME (cterm_of thy (Var v), t) end
+ handle Option.Option =>
+ (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
+ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
+ | TYPE _ =>
+ (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
+ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
fun remove_typeinst (a, t) =
case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => SOME (b, t)
@@ -403,7 +407,7 @@
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
- fun path_finder_FO tm [] = (tm, Term.Bound 0)
+ fun path_finder_FO tm [] = (tm, Bound 0)
| path_finder_FO tm (p::ps) =
let val (tm1,args) = strip_comb tm
val adjustment = get_ty_arg_size thy tm1
@@ -420,14 +424,15 @@
in
(r, list_comb (tm1, replace_item_list t p' args))
end
- fun path_finder_HO tm [] = (tm, Term.Bound 0)
+ fun path_finder_HO tm [] = (tm, 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 = " ^
+ raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+ "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)
+ fun path_finder_FT tm [] _ = (tm, Bound 0)
| path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
path_finder_FT tm ps t1
| path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
@@ -435,7 +440,8 @@
| 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 =
- raise Fail ("equality_inf, path_finder_FT: path = " ^
+ raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+ "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)
@@ -463,7 +469,7 @@
in (tm, nt $ tm_rslt) end
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
val (tm_subst, body) = path_finder_lit i_atm fp
- val tm_abs = Term.Abs ("x", type_of tm_subst, body)
+ val tm_abs = Abs ("x", type_of tm_subst, body)
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
@@ -502,7 +508,7 @@
val n_metis_lits =
length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
val _ = if nprems_of th = n_metis_lits then ()
- else error "Cannot replay Metis proof in Isabelle."
+ else error "Cannot replay Metis proof in Isabelle: Out of sync."
in (fol_th, th) :: thpairs end
end;