1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200
1.3 @@ -18,7 +18,7 @@
1.4 val verbose : bool Config.T
1.5 val verbose_warning : Proof.context -> string -> unit
1.6 val hol_term_from_metis :
1.7 - mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
1.8 + Proof.context -> mode -> int Symtab.table -> Metis_Term.term -> term
1.9 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
1.10 val untyped_aconv : term * term -> bool
1.11 val replay_one_inference :
1.12 @@ -53,13 +53,16 @@
1.13 | terms_of (SomeType _ :: tts) = terms_of tts;
1.14
1.15 fun types_of [] = []
1.16 - | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
1.17 - if String.isPrefix metis_generated_var_prefix a then
1.18 - (*Variable generated by Metis, which might have been a type variable.*)
1.19 - TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
1.20 - else types_of tts
1.21 + | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
1.22 + types_of tts
1.23 + |> (if String.isPrefix metis_generated_var_prefix a then
1.24 + (* Variable generated by Metis, which might have been a type
1.25 + variable. *)
1.26 + cons (TVar (("'" ^ a, idx), HOLogic.typeS))
1.27 + else
1.28 + I)
1.29 | types_of (SomeTerm _ :: tts) = types_of tts
1.30 - | types_of (SomeType T :: tts) = T :: types_of tts;
1.31 + | types_of (SomeType T :: tts) = T :: types_of tts
1.32
1.33 fun apply_list rator nargs rands =
1.34 let val trands = terms_of rands
1.35 @@ -76,19 +79,12 @@
1.36 (* We use 1 rather than 0 because variable references in clauses may otherwise
1.37 conflict with variable constraints in the goal...at least, type inference
1.38 often fails otherwise. See also "axiom_inf" below. *)
1.39 -fun mk_var (w, T) = Var ((w, 1), T)
1.40 -
1.41 -(*include the default sort, if available*)
1.42 -fun mk_tfree ctxt w =
1.43 - let val ww = "'" ^ w
1.44 - in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
1.45 +fun make_var (w, T) = Var ((w, 1), T)
1.46
1.47 (*Remove the "apply" operator from an HO term*)
1.48 fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
1.49 | strip_happ args x = (x, args)
1.50
1.51 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
1.52 -
1.53 fun hol_type_from_metis_term _ (Metis_Term.Var v) =
1.54 (case strip_prefix_and_unascii tvar_prefix v of
1.55 SOME w => make_tvar w
1.56 @@ -99,7 +95,7 @@
1.57 map (hol_type_from_metis_term ctxt) tys)
1.58 | NONE =>
1.59 case strip_prefix_and_unascii tfree_prefix x of
1.60 - SOME tf => mk_tfree ctxt tf
1.61 + SOME tf => make_tfree ctxt tf
1.62 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
1.63
1.64 (*Maps metis terms to isabelle terms*)
1.65 @@ -112,8 +108,8 @@
1.66 SOME w => SomeType (make_tvar w)
1.67 | NONE =>
1.68 case strip_prefix_and_unascii schematic_var_prefix v of
1.69 - SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
1.70 - | NONE => SomeTerm (mk_var (v, HOLogic.typeT)))
1.71 + SOME w => SomeTerm (make_var (w, HOLogic.typeT))
1.72 + | NONE => SomeTerm (make_var (v, HOLogic.typeT)))
1.73 (*Var from Metis with a name like _nnn; possibly a type variable*)
1.74 | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
1.75 | tm_to_tt (t as Metis_Term.Fn (".", _)) =
1.76 @@ -158,7 +154,7 @@
1.77 SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
1.78 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
1.79 case strip_prefix_and_unascii tfree_prefix a of
1.80 - SOME b => SomeType (mk_tfree ctxt b)
1.81 + SOME b => SomeType (make_tfree ctxt b)
1.82 | NONE => (*a fixed variable? They are Skolem functions.*)
1.83 case strip_prefix_and_unascii fixed_var_prefix a of
1.84 SOME b =>
1.85 @@ -184,8 +180,8 @@
1.86 end
1.87 fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
1.88 (case strip_prefix_and_unascii schematic_var_prefix v of
1.89 - SOME w => mk_var(w, dummyT)
1.90 - | NONE => mk_var(v, dummyT))
1.91 + SOME w => make_var (w, dummyT)
1.92 + | NONE => make_var (v, dummyT))
1.93 | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
1.94 Const (@{const_name HOL.eq}, HOLogic.typeT)
1.95 | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
1.96 @@ -226,19 +222,16 @@
1.97 end
1.98 | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
1.99
1.100 -fun hol_term_from_metis_MX sym_tab ctxt =
1.101 - let val thy = Proof_Context.theory_of ctxt in
1.102 - atp_term_from_metis #> term_from_atp thy false sym_tab []
1.103 - (* FIXME ### tfrees instead of []? *) NONE
1.104 - end
1.105 +fun hol_term_from_metis_MX ctxt sym_tab =
1.106 + atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
1.107
1.108 -fun hol_term_from_metis FO _ = hol_term_from_metis_PT
1.109 - | hol_term_from_metis HO _ = hol_term_from_metis_PT
1.110 - | hol_term_from_metis FT _ = hol_term_from_metis_FT
1.111 - | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
1.112 +fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
1.113 + | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
1.114 + | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
1.115 + | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
1.116
1.117 fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
1.118 - let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
1.119 + let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
1.120 val _ = trace_msg ctxt (fn () => " calling type inference:")
1.121 val _ = app (fn t => trace_msg ctxt
1.122 (fn () => Syntax.string_of_term ctxt t)) ts
1.123 @@ -271,7 +264,7 @@
1.124
1.125 (* INFERENCE RULE: AXIOM *)
1.126
1.127 -(* This causes variables to have an index of 1 by default. See also "mk_var"
1.128 +(* This causes variables to have an index of 1 by default. See also "make_var"
1.129 above. *)
1.130 fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
1.131
1.132 @@ -304,7 +297,7 @@
1.133 fun subst_translation (x,y) =
1.134 let val v = find_var x
1.135 (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
1.136 - val t = hol_term_from_metis mode sym_tab ctxt y
1.137 + val t = hol_term_from_metis ctxt mode sym_tab y
1.138 in SOME (cterm_of thy (Var v), t) end
1.139 handle Option.Option =>
1.140 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
1.141 @@ -340,7 +333,7 @@
1.142
1.143 (* Like RSN, but we rename apart only the type variables. Vars here typically
1.144 have an index of 1, and the use of RSN would increase this typically to 3.
1.145 - Instantiations of those Vars could then fail. See comment on "mk_var". *)
1.146 + Instantiations of those Vars could then fail. See comment on "make_var". *)
1.147 fun resolve_inc_tyvars thy tha i thb =
1.148 let
1.149 val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha