more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done

--- 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

--- 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

--- 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