1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon May 17 10:18:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon May 17 12:15:37 2010 +0200
     1.3 @@ -217,6 +217,8 @@
     1.4  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
     1.5    | strip_happ args x = (x, args);
     1.6  
     1.7 +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
     1.8 +
     1.9  fun fol_type_to_isa _ (Metis.Term.Var v) =
    1.10       (case strip_prefix tvar_prefix v of
    1.11            SOME w => make_tvar w

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 10:18:14 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 12:15:37 2010 +0200
     2.3 @@ -14,7 +14,6 @@
     2.4    val invert_const: string -> string
     2.5    val invert_type_const: string -> string
     2.6    val num_type_args: theory -> string -> int
     2.7 -  val make_tvar: string -> typ
     2.8    val strip_prefix: string -> string -> string option
     2.9    val metis_line: int -> int -> string list -> string
    2.10    val metis_proof_text:
    2.11 @@ -235,26 +234,27 @@
    2.12          SOME c' => c'
    2.13        | NONE => c;
    2.14  
    2.15 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
    2.16 -fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
    2.17 -fun make_var (b,T) = Var((b,0),T);
    2.18 -
    2.19  (* Type variables are given the basic sort "HOL.type". Some will later be
    2.20    constrained by information from type literals, or by type inference. *)
    2.21 -fun type_from_node (u as IntLeaf _) = raise NODE [u]
    2.22 -  | type_from_node (u as StrNode (a, us)) =
    2.23 -    let val Ts = map type_from_node us in
    2.24 +fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
    2.25 +  | type_from_node tfrees (u as StrNode (a, us)) =
    2.26 +    let val Ts = map (type_from_node tfrees) us in
    2.27        case strip_prefix tconst_prefix a of
    2.28          SOME b => Type (invert_type_const b, Ts)
    2.29        | NONE =>
    2.30          if not (null us) then
    2.31            raise NODE [u]  (* only "tconst"s have type arguments *)
    2.32          else case strip_prefix tfree_prefix a of
    2.33 -          SOME b => TFree ("'" ^ b, HOLogic.typeS)
    2.34 +          SOME b =>
    2.35 +          let val s = "'" ^ b in
    2.36 +            TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
    2.37 +          end
    2.38          | NONE =>
    2.39            case strip_prefix tvar_prefix a of
    2.40 -            SOME b => make_tvar b
    2.41 -          | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
    2.42 +            SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
    2.43 +          | NONE =>
    2.44 +            (* Variable from the ATP, say "X1" *)
    2.45 +            TypeInfer.param 0 (a, HOLogic.typeS)
    2.46      end
    2.47  
    2.48  (*Invert the table of translations between Isabelle and ATPs*)
    2.49 @@ -287,7 +287,7 @@
    2.50  
    2.51  (* First-order translation. No types are known for variables. "HOLogic.typeT"
    2.52     should allow them to be inferred.*)
    2.53 -fun term_from_node thy full_types =
    2.54 +fun term_from_node thy full_types tfrees =
    2.55    let
    2.56      fun aux opt_T args u =
    2.57        case u of
    2.58 @@ -298,7 +298,8 @@
    2.59        | StrNode (a, us) =>
    2.60          if a = type_wrapper_name then
    2.61            case us of
    2.62 -            [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
    2.63 +            [term_u, typ_u] =>
    2.64 +            aux (SOME (type_from_node tfrees typ_u)) args term_u
    2.65            | _ => raise NODE us
    2.66          else case strip_prefix const_prefix a of
    2.67            SOME "equal" =>
    2.68 @@ -324,7 +325,8 @@
    2.69                            (* Extra args from "hAPP" come after any arguments
    2.70                               given directly to the constant. *)
    2.71                            Sign.const_instance thy (c,
    2.72 -                                    map type_from_node (drop num_term_args us)))
    2.73 +                                    map (type_from_node tfrees)
    2.74 +                                        (drop num_term_args us)))
    2.75            in list_comb (t, ts) end
    2.76          | NONE => (* a free or schematic variable *)
    2.77            let
    2.78 @@ -335,21 +337,22 @@
    2.79                  SOME b => Free (b, T)
    2.80                | NONE =>
    2.81                  case strip_prefix schematic_var_prefix a of
    2.82 -                  SOME b => make_var (b, T)
    2.83 +                  SOME b => Var ((b, 0), T)
    2.84                  | NONE =>
    2.85                    (* Variable from the ATP, say "X1" *)
    2.86 -                  make_var (fix_atp_variable_name a, T)
    2.87 +                  Var ((fix_atp_variable_name a, 0), T)
    2.88            in list_comb (t, ts) end
    2.89    in aux end
    2.90  
    2.91  (* Type class literal applied to a type. Returns triple of polarity, class,
    2.92     type. *)
    2.93 -fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
    2.94 -    type_constraint_from_node (not pos) u
    2.95 -  | type_constraint_from_node pos u = case u of
    2.96 +fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
    2.97 +    type_constraint_from_node (not pos) tfrees u
    2.98 +  | type_constraint_from_node pos tfrees u = case u of
    2.99          IntLeaf _ => raise NODE [u]
   2.100        | StrNode (a, us) =>
   2.101 -            (case (strip_prefix class_prefix a, map type_from_node us) of
   2.102 +            (case (strip_prefix class_prefix a,
   2.103 +                   map (type_from_node tfrees) us) of
   2.104                   (SOME b, [T]) => (pos, b, T)
   2.105                 | _ => raise NODE [u])
   2.106  
   2.107 @@ -395,24 +398,24 @@
   2.108           |> clause_for_literals thy
   2.109  
   2.110  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   2.111 -fun lits_of_nodes thy full_types (vt, lits) us =
   2.112 -  case us of
   2.113 -    [] => (vt, finish_clause thy lits)
   2.114 -  | (u :: us) =>
   2.115 -    lits_of_nodes thy full_types
   2.116 -        (add_type_constraint (type_constraint_from_node true u) vt, lits) us
   2.117 -    handle NODE _ =>
   2.118 -           lits_of_nodes thy full_types
   2.119 -                         (vt, term_from_node thy full_types (SOME @{typ bool})
   2.120 -                                             [] u :: lits) us
   2.121 +fun lits_of_nodes thy full_types tfrees =
   2.122 +  let
   2.123 +    fun aux (vt, lits) [] = (vt, finish_clause thy lits)
   2.124 +      | aux (vt, lits) (u :: us) =
   2.125 +        aux (add_type_constraint
   2.126 +                 (type_constraint_from_node true tfrees u) vt, lits) us
   2.127 +        handle NODE _ =>
   2.128 +               aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
   2.129 +                                       [] u :: lits) us
   2.130 +  in aux end
   2.131  
   2.132 -(*Update TVars/TFrees with detected sort constraints.*)
   2.133 -fun repair_sorts vt =
   2.134 +(* Update TVars with detected sort constraints. It's not totally clear when
   2.135 +   this code is necessary. *)
   2.136 +fun repair_tvar_sorts vt =
   2.137    let
   2.138      fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   2.139        | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
   2.140 -      | do_type (TFree (x, s)) =
   2.141 -        TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
   2.142 +      | do_type (TFree z) = TFree z
   2.143      fun do_term (Const (a, T)) = Const (a, do_type T)
   2.144        | do_term (Free (a, T)) = Free (a, do_type T)
   2.145        | do_term (Var (xi, T)) = Var (xi, do_type T)
   2.146 @@ -444,45 +447,28 @@
   2.147  (* Interpret a list of syntax trees as a clause, given by "real" literals and
   2.148     sort constraints. "vt" holds the initial sort constraints, from the
   2.149     conjecture clauses. *)
   2.150 -fun clause_of_nodes ctxt full_types vt us =
   2.151 +fun clause_of_nodes ctxt full_types tfrees us =
   2.152    let
   2.153      val thy = ProofContext.theory_of ctxt
   2.154 -    val (vt, t) = lits_of_nodes thy full_types (vt, []) us
   2.155 -  in repair_sorts vt t end
   2.156 +    val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
   2.157 +  in repair_tvar_sorts vt t end
   2.158  fun check_formula ctxt =
   2.159    TypeInfer.constrain @{typ bool}
   2.160    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   2.161  
   2.162 -(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
   2.163 -    clauses. **)
   2.164 -
   2.165 -fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
   2.166 -  | add_tfree_constraint _ = I
   2.167 -fun tfree_constraints_of_clauses vt [] = vt
   2.168 -  | tfree_constraints_of_clauses vt ([lit] :: uss) =
   2.169 -    (tfree_constraints_of_clauses (add_tfree_constraint
   2.170 -                                    (type_constraint_from_node true lit) vt) uss
   2.171 -     handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
   2.172 -     tfree_constraints_of_clauses vt uss)
   2.173 -  | tfree_constraints_of_clauses vt (_ :: uss) =
   2.174 -    tfree_constraints_of_clauses vt uss
   2.175 -
   2.176  
   2.177  (**** Translation of TSTP files to Isar Proofs ****)
   2.178  
   2.179  fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   2.180    | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   2.181  
   2.182 -fun clauses_in_lines (Definition (_, u, us)) = u :: us
   2.183 -  | clauses_in_lines (Inference (_, us, _)) = us
   2.184 -
   2.185 -fun decode_line full_types vt (Definition (num, u, us)) ctxt =
   2.186 +fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
   2.187      let
   2.188 -      val t1 = clause_of_nodes ctxt full_types vt [u]
   2.189 +      val t1 = clause_of_nodes ctxt full_types tfrees [u]
   2.190        val vars = snd (strip_comb t1)
   2.191        val frees = map unvarify_term vars
   2.192        val unvarify_args = subst_atomic (vars ~~ frees)
   2.193 -      val t2 = clause_of_nodes ctxt full_types vt us
   2.194 +      val t2 = clause_of_nodes ctxt full_types tfrees us
   2.195        val (t1, t2) =
   2.196          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   2.197          |> unvarify_args |> uncombine_term |> check_formula ctxt
   2.198 @@ -491,19 +477,16 @@
   2.199        (Definition (num, t1, t2),
   2.200         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   2.201      end
   2.202 -  | decode_line full_types vt (Inference (num, us, deps)) ctxt =
   2.203 +  | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
   2.204      let
   2.205 -      val t = us |> clause_of_nodes ctxt full_types vt
   2.206 +      val t = us |> clause_of_nodes ctxt full_types tfrees
   2.207                   |> unskolemize_term |> uncombine_term |> check_formula ctxt
   2.208      in
   2.209        (Inference (num, t, deps),
   2.210         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   2.211      end
   2.212 -fun decode_lines ctxt full_types lines =
   2.213 -  let
   2.214 -    val vt = tfree_constraints_of_clauses Vartab.empty
   2.215 -                                          (map clauses_in_lines lines)
   2.216 -  in #1 (fold_map (decode_line full_types vt) lines ctxt) end
   2.217 +fun decode_lines ctxt full_types tfrees lines =
   2.218 +  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   2.219  
   2.220  fun aint_inference _ (Definition _) = true
   2.221    | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   2.222 @@ -674,13 +657,13 @@
   2.223            forall_vars t,
   2.224            ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
   2.225  
   2.226 -fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
   2.227 -                         conjecture_shape thm_names params frees =
   2.228 +fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   2.229 +                         atp_proof conjecture_shape thm_names params frees =
   2.230    let
   2.231      val lines =
   2.232        atp_proof ^ "$" (* the $ sign acts as a sentinel *)
   2.233        |> parse_proof pool
   2.234 -      |> decode_lines ctxt full_types
   2.235 +      |> decode_lines ctxt full_types tfrees
   2.236        |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   2.237        |> rpair [] |-> fold_rev add_nontrivial_line
   2.238        |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
   2.239 @@ -839,7 +822,7 @@
   2.240        apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   2.241      fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   2.242          (case AList.lookup (op aconv) assums t of
   2.243 -           SOME l' => (proof, (l', l) :: subst, assums)
   2.244 +           SOME l' => (proof, (l, l') :: subst, assums)
   2.245           | NONE => (step :: proof, subst, (t, l) :: assums))
   2.246        | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   2.247          (Have (qs, l, t,
   2.248 @@ -988,11 +971,12 @@
   2.249      val thy = ProofContext.theory_of ctxt
   2.250      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   2.251      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   2.252 +    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   2.253      val n = Logic.count_prems (prop_of goal)
   2.254      val (one_line_proof, lemma_names) =
   2.255        metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   2.256      fun isar_proof_for () =
   2.257 -      case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
   2.258 +      case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   2.259                                  atp_proof conjecture_shape thm_names params
   2.260                                  frees
   2.261             |> redirect_proof thy conjecture_shape hyp_ts concl_t