--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
@@ -18,7 +18,7 @@
val verbose : bool Config.T
val verbose_warning : Proof.context -> string -> unit
val hol_term_from_metis :
- mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
+ Proof.context -> mode -> int Symtab.table -> Metis_Term.term -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term * term -> bool
val replay_one_inference :
@@ -53,13 +53,16 @@
| terms_of (SomeType _ :: tts) = terms_of tts;
fun types_of [] = []
- | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
- if String.isPrefix metis_generated_var_prefix 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 (SomeTerm (Var ((a, idx), _)) :: tts) =
+ types_of tts
+ |> (if String.isPrefix metis_generated_var_prefix a then
+ (* Variable generated by Metis, which might have been a type
+ variable. *)
+ cons (TVar (("'" ^ a, idx), HOLogic.typeS))
+ else
+ I)
| types_of (SomeTerm _ :: tts) = types_of tts
- | types_of (SomeType T :: tts) = T :: types_of tts;
+ | types_of (SomeType T :: tts) = T :: types_of tts
fun apply_list rator nargs rands =
let val trands = terms_of rands
@@ -76,19 +79,12 @@
(* 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) = Var ((w, 1), T)
-
-(*include the default sort, if available*)
-fun mk_tfree ctxt w =
- let val ww = "'" ^ w
- in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
+fun make_var (w, T) = Var ((w, 1), T)
(*Remove the "apply" operator from an HO term*)
fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
| strip_happ args x = (x, args)
-fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-
fun hol_type_from_metis_term _ (Metis_Term.Var v) =
(case strip_prefix_and_unascii tvar_prefix v of
SOME w => make_tvar w
@@ -99,7 +95,7 @@
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
case strip_prefix_and_unascii tfree_prefix x of
- SOME tf => mk_tfree ctxt tf
+ SOME tf => make_tfree ctxt tf
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
(*Maps metis terms to isabelle terms*)
@@ -112,8 +108,8 @@
SOME w => SomeType (make_tvar w)
| NONE =>
case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
- | NONE => SomeTerm (mk_var (v, HOLogic.typeT)))
+ SOME w => SomeTerm (make_var (w, HOLogic.typeT))
+ | NONE => SomeTerm (make_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 (".", _)) =
@@ -158,7 +154,7 @@
SomeType (Type (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 => SomeType (mk_tfree ctxt b)
+ SOME b => SomeType (make_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
case strip_prefix_and_unascii fixed_var_prefix a of
SOME b =>
@@ -184,8 +180,8 @@
end
fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
(case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => mk_var(w, dummyT)
- | NONE => mk_var(v, dummyT))
+ SOME w => make_var (w, dummyT)
+ | NONE => make_var (v, dummyT))
| cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
Const (@{const_name HOL.eq}, HOLogic.typeT)
| cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
@@ -226,19 +222,16 @@
end
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
-fun hol_term_from_metis_MX sym_tab ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- atp_term_from_metis #> term_from_atp thy false sym_tab []
- (* FIXME ### tfrees instead of []? *) NONE
- end
+fun hol_term_from_metis_MX ctxt sym_tab =
+ atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
-fun hol_term_from_metis FO _ = hol_term_from_metis_PT
- | hol_term_from_metis HO _ = hol_term_from_metis_PT
- | hol_term_from_metis FT _ = hol_term_from_metis_FT
- | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
+fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
+ | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
+ | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
+ | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
- let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
+ let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -271,7 +264,7 @@
(* INFERENCE RULE: AXIOM *)
-(* This causes variables to have an index of 1 by default. See also "mk_var"
+(* This causes variables to have an index of 1 by default. See also "make_var"
above. *)
fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
@@ -304,7 +297,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode sym_tab ctxt y
+ val t = hol_term_from_metis ctxt mode sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -340,7 +333,7 @@
(* Like RSN, but we rename apart only the type variables. Vars here typically
have an index of 1, and the use of RSN would increase this typically to 3.
- Instantiations of those Vars could then fail. See comment on "mk_var". *)
+ Instantiations of those Vars could then fail. See comment on "make_var". *)
fun resolve_inc_tyvars thy tha i thb =
let
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha