src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 36967 3c804030474b
parent 36924 ff01d3ae9ad4
child 36968 62e29faa3718
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 10:18:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 12:15:37 2010 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val invert_const: string -> string
     1.5    val invert_type_const: string -> string
     1.6    val num_type_args: theory -> string -> int
     1.7 -  val make_tvar: string -> typ
     1.8    val strip_prefix: string -> string -> string option
     1.9    val metis_line: int -> int -> string list -> string
    1.10    val metis_proof_text:
    1.11 @@ -235,26 +234,27 @@
    1.12          SOME c' => c'
    1.13        | NONE => c;
    1.14  
    1.15 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
    1.16 -fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
    1.17 -fun make_var (b,T) = Var((b,0),T);
    1.18 -
    1.19  (* Type variables are given the basic sort "HOL.type". Some will later be
    1.20    constrained by information from type literals, or by type inference. *)
    1.21 -fun type_from_node (u as IntLeaf _) = raise NODE [u]
    1.22 -  | type_from_node (u as StrNode (a, us)) =
    1.23 -    let val Ts = map type_from_node us in
    1.24 +fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
    1.25 +  | type_from_node tfrees (u as StrNode (a, us)) =
    1.26 +    let val Ts = map (type_from_node tfrees) us in
    1.27        case strip_prefix tconst_prefix a of
    1.28          SOME b => Type (invert_type_const b, Ts)
    1.29        | NONE =>
    1.30          if not (null us) then
    1.31            raise NODE [u]  (* only "tconst"s have type arguments *)
    1.32          else case strip_prefix tfree_prefix a of
    1.33 -          SOME b => TFree ("'" ^ b, HOLogic.typeS)
    1.34 +          SOME b =>
    1.35 +          let val s = "'" ^ b in
    1.36 +            TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
    1.37 +          end
    1.38          | NONE =>
    1.39            case strip_prefix tvar_prefix a of
    1.40 -            SOME b => make_tvar b
    1.41 -          | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
    1.42 +            SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
    1.43 +          | NONE =>
    1.44 +            (* Variable from the ATP, say "X1" *)
    1.45 +            TypeInfer.param 0 (a, HOLogic.typeS)
    1.46      end
    1.47  
    1.48  (*Invert the table of translations between Isabelle and ATPs*)
    1.49 @@ -287,7 +287,7 @@
    1.50  
    1.51  (* First-order translation. No types are known for variables. "HOLogic.typeT"
    1.52     should allow them to be inferred.*)
    1.53 -fun term_from_node thy full_types =
    1.54 +fun term_from_node thy full_types tfrees =
    1.55    let
    1.56      fun aux opt_T args u =
    1.57        case u of
    1.58 @@ -298,7 +298,8 @@
    1.59        | StrNode (a, us) =>
    1.60          if a = type_wrapper_name then
    1.61            case us of
    1.62 -            [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
    1.63 +            [term_u, typ_u] =>
    1.64 +            aux (SOME (type_from_node tfrees typ_u)) args term_u
    1.65            | _ => raise NODE us
    1.66          else case strip_prefix const_prefix a of
    1.67            SOME "equal" =>
    1.68 @@ -324,7 +325,8 @@
    1.69                            (* Extra args from "hAPP" come after any arguments
    1.70                               given directly to the constant. *)
    1.71                            Sign.const_instance thy (c,
    1.72 -                                    map type_from_node (drop num_term_args us)))
    1.73 +                                    map (type_from_node tfrees)
    1.74 +                                        (drop num_term_args us)))
    1.75            in list_comb (t, ts) end
    1.76          | NONE => (* a free or schematic variable *)
    1.77            let
    1.78 @@ -335,21 +337,22 @@
    1.79                  SOME b => Free (b, T)
    1.80                | NONE =>
    1.81                  case strip_prefix schematic_var_prefix a of
    1.82 -                  SOME b => make_var (b, T)
    1.83 +                  SOME b => Var ((b, 0), T)
    1.84                  | NONE =>
    1.85                    (* Variable from the ATP, say "X1" *)
    1.86 -                  make_var (fix_atp_variable_name a, T)
    1.87 +                  Var ((fix_atp_variable_name a, 0), T)
    1.88            in list_comb (t, ts) end
    1.89    in aux end
    1.90  
    1.91  (* Type class literal applied to a type. Returns triple of polarity, class,
    1.92     type. *)
    1.93 -fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
    1.94 -    type_constraint_from_node (not pos) u
    1.95 -  | type_constraint_from_node pos u = case u of
    1.96 +fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
    1.97 +    type_constraint_from_node (not pos) tfrees u
    1.98 +  | type_constraint_from_node pos tfrees u = case u of
    1.99          IntLeaf _ => raise NODE [u]
   1.100        | StrNode (a, us) =>
   1.101 -            (case (strip_prefix class_prefix a, map type_from_node us) of
   1.102 +            (case (strip_prefix class_prefix a,
   1.103 +                   map (type_from_node tfrees) us) of
   1.104                   (SOME b, [T]) => (pos, b, T)
   1.105                 | _ => raise NODE [u])
   1.106  
   1.107 @@ -395,24 +398,24 @@
   1.108           |> clause_for_literals thy
   1.109  
   1.110  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   1.111 -fun lits_of_nodes thy full_types (vt, lits) us =
   1.112 -  case us of
   1.113 -    [] => (vt, finish_clause thy lits)
   1.114 -  | (u :: us) =>
   1.115 -    lits_of_nodes thy full_types
   1.116 -        (add_type_constraint (type_constraint_from_node true u) vt, lits) us
   1.117 -    handle NODE _ =>
   1.118 -           lits_of_nodes thy full_types
   1.119 -                         (vt, term_from_node thy full_types (SOME @{typ bool})
   1.120 -                                             [] u :: lits) us
   1.121 +fun lits_of_nodes thy full_types tfrees =
   1.122 +  let
   1.123 +    fun aux (vt, lits) [] = (vt, finish_clause thy lits)
   1.124 +      | aux (vt, lits) (u :: us) =
   1.125 +        aux (add_type_constraint
   1.126 +                 (type_constraint_from_node true tfrees u) vt, lits) us
   1.127 +        handle NODE _ =>
   1.128 +               aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
   1.129 +                                       [] u :: lits) us
   1.130 +  in aux end
   1.131  
   1.132 -(*Update TVars/TFrees with detected sort constraints.*)
   1.133 -fun repair_sorts vt =
   1.134 +(* Update TVars with detected sort constraints. It's not totally clear when
   1.135 +   this code is necessary. *)
   1.136 +fun repair_tvar_sorts vt =
   1.137    let
   1.138      fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   1.139        | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
   1.140 -      | do_type (TFree (x, s)) =
   1.141 -        TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
   1.142 +      | do_type (TFree z) = TFree z
   1.143      fun do_term (Const (a, T)) = Const (a, do_type T)
   1.144        | do_term (Free (a, T)) = Free (a, do_type T)
   1.145        | do_term (Var (xi, T)) = Var (xi, do_type T)
   1.146 @@ -444,45 +447,28 @@
   1.147  (* Interpret a list of syntax trees as a clause, given by "real" literals and
   1.148     sort constraints. "vt" holds the initial sort constraints, from the
   1.149     conjecture clauses. *)
   1.150 -fun clause_of_nodes ctxt full_types vt us =
   1.151 +fun clause_of_nodes ctxt full_types tfrees us =
   1.152    let
   1.153      val thy = ProofContext.theory_of ctxt
   1.154 -    val (vt, t) = lits_of_nodes thy full_types (vt, []) us
   1.155 -  in repair_sorts vt t end
   1.156 +    val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
   1.157 +  in repair_tvar_sorts vt t end
   1.158  fun check_formula ctxt =
   1.159    TypeInfer.constrain @{typ bool}
   1.160    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   1.161  
   1.162 -(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
   1.163 -    clauses. **)
   1.164 -
   1.165 -fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
   1.166 -  | add_tfree_constraint _ = I
   1.167 -fun tfree_constraints_of_clauses vt [] = vt
   1.168 -  | tfree_constraints_of_clauses vt ([lit] :: uss) =
   1.169 -    (tfree_constraints_of_clauses (add_tfree_constraint
   1.170 -                                    (type_constraint_from_node true lit) vt) uss
   1.171 -     handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
   1.172 -     tfree_constraints_of_clauses vt uss)
   1.173 -  | tfree_constraints_of_clauses vt (_ :: uss) =
   1.174 -    tfree_constraints_of_clauses vt uss
   1.175 -
   1.176  
   1.177  (**** Translation of TSTP files to Isar Proofs ****)
   1.178  
   1.179  fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   1.180    | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   1.181  
   1.182 -fun clauses_in_lines (Definition (_, u, us)) = u :: us
   1.183 -  | clauses_in_lines (Inference (_, us, _)) = us
   1.184 -
   1.185 -fun decode_line full_types vt (Definition (num, u, us)) ctxt =
   1.186 +fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
   1.187      let
   1.188 -      val t1 = clause_of_nodes ctxt full_types vt [u]
   1.189 +      val t1 = clause_of_nodes ctxt full_types tfrees [u]
   1.190        val vars = snd (strip_comb t1)
   1.191        val frees = map unvarify_term vars
   1.192        val unvarify_args = subst_atomic (vars ~~ frees)
   1.193 -      val t2 = clause_of_nodes ctxt full_types vt us
   1.194 +      val t2 = clause_of_nodes ctxt full_types tfrees us
   1.195        val (t1, t2) =
   1.196          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   1.197          |> unvarify_args |> uncombine_term |> check_formula ctxt
   1.198 @@ -491,19 +477,16 @@
   1.199        (Definition (num, t1, t2),
   1.200         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   1.201      end
   1.202 -  | decode_line full_types vt (Inference (num, us, deps)) ctxt =
   1.203 +  | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
   1.204      let
   1.205 -      val t = us |> clause_of_nodes ctxt full_types vt
   1.206 +      val t = us |> clause_of_nodes ctxt full_types tfrees
   1.207                   |> unskolemize_term |> uncombine_term |> check_formula ctxt
   1.208      in
   1.209        (Inference (num, t, deps),
   1.210         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   1.211      end
   1.212 -fun decode_lines ctxt full_types lines =
   1.213 -  let
   1.214 -    val vt = tfree_constraints_of_clauses Vartab.empty
   1.215 -                                          (map clauses_in_lines lines)
   1.216 -  in #1 (fold_map (decode_line full_types vt) lines ctxt) end
   1.217 +fun decode_lines ctxt full_types tfrees lines =
   1.218 +  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   1.219  
   1.220  fun aint_inference _ (Definition _) = true
   1.221    | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   1.222 @@ -674,13 +657,13 @@
   1.223            forall_vars t,
   1.224            ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
   1.225  
   1.226 -fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
   1.227 -                         conjecture_shape thm_names params frees =
   1.228 +fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   1.229 +                         atp_proof conjecture_shape thm_names params frees =
   1.230    let
   1.231      val lines =
   1.232        atp_proof ^ "$" (* the $ sign acts as a sentinel *)
   1.233        |> parse_proof pool
   1.234 -      |> decode_lines ctxt full_types
   1.235 +      |> decode_lines ctxt full_types tfrees
   1.236        |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   1.237        |> rpair [] |-> fold_rev add_nontrivial_line
   1.238        |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
   1.239 @@ -839,7 +822,7 @@
   1.240        apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   1.241      fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   1.242          (case AList.lookup (op aconv) assums t of
   1.243 -           SOME l' => (proof, (l', l) :: subst, assums)
   1.244 +           SOME l' => (proof, (l, l') :: subst, assums)
   1.245           | NONE => (step :: proof, subst, (t, l) :: assums))
   1.246        | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   1.247          (Have (qs, l, t,
   1.248 @@ -988,11 +971,12 @@
   1.249      val thy = ProofContext.theory_of ctxt
   1.250      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.251      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.252 +    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   1.253      val n = Logic.count_prems (prop_of goal)
   1.254      val (one_line_proof, lemma_names) =
   1.255        metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   1.256      fun isar_proof_for () =
   1.257 -      case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
   1.258 +      case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   1.259                                  atp_proof conjecture_shape thm_names params
   1.260                                  frees
   1.261             |> redirect_proof thy conjecture_shape hyp_ts concl_t