# HG changeset patch # User blanchet # Date 1306916983 -7200 # Node ID 8c32a0160b0dc2af50123544ccfbe5a0af5c93fb # Parent 0c82e00ba63ec5f3ce93f5fb124a1130949d38de more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done diff -r 0c82e00ba63e -r 8c32a0160b0d src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200 @@ -43,11 +43,13 @@ val uses_typed_helpers : int list -> 'a proof -> bool val reconstructor_name : reconstructor -> string val one_line_proof_text : one_line_params -> string + val make_tvar : string -> typ + val make_tfree : Proof.context -> string -> typ val term_from_atp : - theory -> bool -> int Symtab.table -> (string * sort) list -> typ option - -> string fo_term -> term + Proof.context -> bool -> int Symtab.table -> typ option -> string fo_term + -> term val prop_from_atp : - theory -> bool -> int Symtab.table -> (string * sort) list + Proof.context -> bool -> int Symtab.table -> (string, string, string fo_term) formula -> term val isar_proof_text : Proof.context -> bool -> isar_params -> one_line_params -> string @@ -344,6 +346,12 @@ fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) +fun make_tfree ctxt w = + let val ww = "'" ^ w in + TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) + end + val indent_size = 2 val no_label = ("", ~1) @@ -366,21 +374,18 @@ (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information from type literals, or by type inference. *) -fun typ_from_atp tfrees (u as ATerm (a, us)) = - let val Ts = map (typ_from_atp tfrees) us in +fun typ_from_atp ctxt (u as ATerm (a, us)) = + let val Ts = map (typ_from_atp ctxt) us in case strip_prefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) | NONE => if not (null us) then raise FO_TERM [u] (* only "tconst"s have type arguments *) else case strip_prefix_and_unascii tfree_prefix a of - SOME b => - let val s = "'" ^ b in - TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS) - end + SOME b => make_tfree ctxt b | NONE => case strip_prefix_and_unascii tvar_prefix a of - SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) + SOME b => make_tvar b | NONE => (* Variable from the ATP, say "X1" *) Type_Infer.param 0 (a, HOLogic.typeS) @@ -388,9 +393,8 @@ (* Type class literal applied to a type. Returns triple of polarity, class, type. *) -fun type_constraint_from_term tfrees (u as ATerm (a, us)) = - case (strip_prefix_and_unascii class_prefix a, - map (typ_from_atp tfrees) us) of +fun type_constraint_from_term ctxt (u as ATerm (a, us)) = + case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of (SOME b, [T]) => (b, T) | _ => raise FO_TERM [u] @@ -419,8 +423,9 @@ (* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to be inferred. *) -fun term_from_atp thy textual sym_tab tfrees = +fun term_from_atp ctxt textual sym_tab = let + val thy = Proof_Context.theory_of ctxt (* see also "mk_var" in "Metis_Reconstruct" *) val var_index = if textual then 0 else 1 fun do_term extra_ts opt_T u = @@ -445,7 +450,7 @@ if s' = type_tag_name then case mangled_us @ us of [typ_u, term_u] => - do_term extra_ts (SOME (typ_from_atp tfrees typ_u)) term_u + do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u | _ => raise FO_TERM us else if s' = predicator_name then do_term [] (SOME @{typ bool}) (hd us) @@ -469,7 +474,7 @@ val T = if not (null type_us) andalso num_type_args thy s' = length type_us then - (s', map (typ_from_atp tfrees) type_us) + (s', map (typ_from_atp ctxt) type_us) |> Sign.const_instance thy else case opt_T of SOME T => map fastype_of term_ts ---> T @@ -493,12 +498,12 @@ in list_comb (t, ts) end in do_term [] end -fun term_from_atom thy textual sym_tab tfrees pos (u as ATerm (s, _)) = +fun term_from_atom ctxt textual sym_tab pos (u as ATerm (s, _)) = if String.isPrefix class_prefix s then - add_type_constraint pos (type_constraint_from_term tfrees u) + add_type_constraint pos (type_constraint_from_term ctxt u) #> pair @{const True} else - pair (term_from_atp thy textual sym_tab tfrees (SOME @{typ bool}) u) + pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u) val combinator_table = [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), @@ -543,7 +548,7 @@ (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the formula. *) -fun prop_from_atp thy textual sym_tab tfrees phi = +fun prop_from_atp ctxt textual sym_tab phi = let fun do_formula pos phi = case phi of @@ -567,7 +572,7 @@ | AIff => s_iff | ANotIff => s_not o s_iff | _ => raise Fail "unexpected connective") - | AAtom tm => term_from_atom thy textual sym_tab tfrees pos tm + | AAtom tm => term_from_atom ctxt textual sym_tab pos tm | _ => raise FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end @@ -581,14 +586,14 @@ fun unvarify_term (Var ((s, 0), T)) = Free (s, T) | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) -fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt = +fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt = let val thy = Proof_Context.theory_of ctxt - val t1 = prop_from_atp thy true sym_tab tfrees phi1 + val t1 = prop_from_atp ctxt true sym_tab phi1 val vars = snd (strip_comb t1) val frees = map unvarify_term vars val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_atp thy true sym_tab tfrees phi2 + val t2 = prop_from_atp ctxt true sym_tab phi2 val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt @@ -597,17 +602,17 @@ (Definition (name, t1, t2), fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) end - | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt = + | decode_line sym_tab (Inference (name, u, deps)) ctxt = let val thy = Proof_Context.theory_of ctxt - val t = u |> prop_from_atp thy true sym_tab tfrees + val t = u |> prop_from_atp ctxt true sym_tab |> uncombine_term thy |> infer_formula_types ctxt in (Inference (name, t, deps), fold Variable.declare_term (OldTerm.term_frees t) ctxt) end -fun decode_lines ctxt sym_tab tfrees lines = - fst (fold_map (decode_line sym_tab tfrees) lines ctxt) +fun decode_lines ctxt sym_tab lines = + fst (fold_map (decode_line sym_tab) lines ctxt) fun is_same_inference _ (Definition _) = false | is_same_inference t (Inference (_, t', _)) = t aconv t' @@ -743,7 +748,7 @@ else s -fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor +fun isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor conjecture_shape facts_offset fact_names sym_tab params frees atp_proof = let @@ -752,7 +757,7 @@ |> clean_up_atp_proof_dependencies |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name - |> decode_lines ctxt sym_tab tfrees + |> decode_lines ctxt sym_tab |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) @@ -1063,13 +1068,11 @@ (if isar_proof_requested then 1 else 2) * isar_shrink_factor val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val frees = fold Term.add_frees (concl_t :: hyp_ts) [] - val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] val one_line_proof = one_line_proof_text one_line_params fun isar_proof_for () = case atp_proof - |> isar_proof_from_atp_proof pool ctxt type_sys tfrees - isar_shrink_factor conjecture_shape facts_offset - fact_names sym_tab params frees + |> isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor + conjecture_shape facts_offset fact_names sym_tab params frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof diff -r 0c82e00ba63e -r 8c32a0160b0d src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 0c82e00ba63e -r 8c32a0160b0d src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 @@ -59,8 +59,7 @@ fun cterm_from_metis ctxt sym_tab wrap tm = let val thy = Proof_Context.theory_of ctxt in - tm |> hol_term_from_metis MX sym_tab ctxt - |> wrap + tm |> hol_term_from_metis ctxt MX sym_tab |> wrap |> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |> cterm_of thy