unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
authorblanchet
Wed Apr 28 15:34:55 2010 +0200 (2010-04-28)
changeset 364916769f8eacaac
parent 36490 5abf45444a16
child 36492 60532b9bcd1c
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 14:19:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 15:34:55 2010 +0200
     1.3 @@ -185,7 +185,8 @@
     1.4        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
     1.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
     1.6  
     1.7 -val max_dfg_symbol_length = 63
     1.8 +val max_dfg_symbol_length =
     1.9 +  if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
    1.10  
    1.11  (* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    1.12  fun controlled_length dfg s =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 14:19:26 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 15:34:55 2010 +0200
     2.3 @@ -33,10 +33,6 @@
     2.4  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
     2.5  struct
     2.6  
     2.7 -datatype ('a, 'b, 'c, 'd, 'e) raw_step =
     2.8 -  Definition of 'a * 'b * 'c |
     2.9 -  Inference of 'a * 'd * 'e list
    2.10 -
    2.11  open Sledgehammer_Util
    2.12  open Sledgehammer_FOL_Clause
    2.13  open Sledgehammer_Fact_Preprocessor
    2.14 @@ -54,6 +50,25 @@
    2.15        SOME s' => s'
    2.16      | NONE => s
    2.17  
    2.18 +(* Hack: Could return false positives (e.g., a user happens to declare a
    2.19 +   constant called "SomeTheory.sko_means_shoe_in_swedish". *)
    2.20 +val is_skolem_const_name = String.isPrefix skolem_prefix o Long_Name.base_name
    2.21 +
    2.22 +fun smart_lambda v t =
    2.23 +    Abs (case v of
    2.24 +           Const (s, _) => if is_skolem_const_name s then "g"
    2.25 +                           else Long_Name.base_name s
    2.26 +         | Var ((s, _), _) => s
    2.27 +         | Free (s, _) => s
    2.28 +         | _ => "", fastype_of v, abstract_over (v, t))
    2.29 +
    2.30 +fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
    2.31 +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ smart_lambda v t
    2.32 +
    2.33 +datatype ('a, 'b, 'c, 'd, 'e) raw_step =
    2.34 +  Definition of 'a * 'b * 'c |
    2.35 +  Inference of 'a * 'd * 'e list
    2.36 +
    2.37  (**** PARSING OF TSTP FORMAT ****)
    2.38  
    2.39  (* Syntax trees, either term list or formulae *)
    2.40 @@ -294,8 +309,7 @@
    2.41    | add_constraint ((false, cl, TVar(ix,_)), vt) = add_var (ix,cl) vt
    2.42    | add_constraint (_, vt) = vt;
    2.43  
    2.44 -fun is_positive_literal (@{const Trueprop} $ t) = is_positive_literal t
    2.45 -  | is_positive_literal (@{const Not} $ _) = false
    2.46 +fun is_positive_literal (@{const Not} $ _) = false
    2.47    | is_positive_literal t = true
    2.48  
    2.49  fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    2.50 @@ -310,11 +324,6 @@
    2.51      @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
    2.52    | negate_term _ (@{const Not} $ t) = t
    2.53    | negate_term _ t = @{const Not} $ t
    2.54 -fun negate_formula thy (@{const Trueprop} $ t) =
    2.55 -    @{const Trueprop} $ negate_term thy t
    2.56 -  | negate_formula thy t =
    2.57 -    if fastype_of t = @{typ prop} then Logic.mk_implies (t, @{prop False})
    2.58 -    else @{const Not} $ t
    2.59  
    2.60  fun clause_for_literals _ [] = HOLogic.false_const
    2.61    | clause_for_literals _ [lit] = lit
    2.62 @@ -559,12 +568,13 @@
    2.63    else
    2.64      apfst (insert (op =) (raw_prefix, num))
    2.65  
    2.66 -fun quantify_over_all_vars t = fold_rev Logic.all (map Var ((*Term.add_vars t###*) [])) t
    2.67 +fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
    2.68 +
    2.69  fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
    2.70    | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
    2.71    | step_for_line thm_names j (Inference (num, t, deps)) =
    2.72      Have (if j = 1 then [Show] else [], (raw_prefix, num),
    2.73 -          quantify_over_all_vars (HOLogic.mk_Trueprop t),
    2.74 +          forall_vars t,
    2.75            Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
    2.76  
    2.77  fun strip_spaces_in_list [] = ""
    2.78 @@ -653,25 +663,26 @@
    2.79  
    2.80  val index_in_shape = find_index o exists o curry (op =)
    2.81  
    2.82 -fun direct_proof thy conjecture_shape hyp_ts concl_t proof =
    2.83 +fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
    2.84    let
    2.85      val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
    2.86      fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
    2.87      fun first_pass ([], contra) = ([], contra)
    2.88 -      | first_pass ((ps as Fix _) :: proof, contra) =
    2.89 -        first_pass (proof, contra) |>> cons ps
    2.90 -      | first_pass ((ps as Let _) :: proof, contra) =
    2.91 -        first_pass (proof, contra) |>> cons ps
    2.92 -      | first_pass ((ps as Assume (l, t)) :: proof, contra) =
    2.93 +      | first_pass ((step as Fix _) :: proof, contra) =
    2.94 +        first_pass (proof, contra) |>> cons step
    2.95 +      | first_pass ((step as Let _) :: proof, contra) =
    2.96 +        first_pass (proof, contra) |>> cons step
    2.97 +      | first_pass ((step as Assume (l, t)) :: proof, contra) =
    2.98          if member (op =) concl_ls l then
    2.99 -          first_pass (proof, contra ||> cons ps)
   2.100 +          first_pass (proof, contra ||> cons step)
   2.101          else
   2.102            first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
   2.103 -      | first_pass ((ps as Have (qs, l, t, Facts (ls, ss))) :: proof, contra) =
   2.104 +      | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
   2.105 +                    contra) =
   2.106          if exists (member (op =) (fst contra)) ls then
   2.107 -          first_pass (proof, contra |>> cons l ||> cons ps)
   2.108 +          first_pass (proof, contra |>> cons l ||> cons step)
   2.109          else
   2.110 -          first_pass (proof, contra) |>> cons ps
   2.111 +          first_pass (proof, contra) |>> cons step
   2.112        | first_pass _ = raise Fail "malformed proof"
   2.113      val (proof_top, (contra_ls, contra_proof)) =
   2.114        first_pass (proof, (concl_ls, []))
   2.115 @@ -681,8 +692,7 @@
   2.116      fun second_pass end_qs ([], assums, patches) =
   2.117          ([Have (end_qs, no_label,
   2.118                  if length assums < length concl_ls then
   2.119 -                  clause_for_literals thy
   2.120 -                                      (map (negate_formula thy o fst) assums)
   2.121 +                  clause_for_literals thy (map (negate_term thy o fst) assums)
   2.122                  else
   2.123                    concl_t,
   2.124                  Facts (backpatch_labels patches (map snd assums)))], patches)
   2.125 @@ -701,9 +711,9 @@
   2.126                             (proof, assums,
   2.127                              patches |>> cons (contra_l, (l :: co_ls, ss)))
   2.128                 |>> cons (if member (op =) (fst (snd patches)) l then
   2.129 -                           Assume (l, negate_formula thy t)
   2.130 +                           Assume (l, negate_term thy t)
   2.131                           else
   2.132 -                           Have (qs, l, negate_formula thy t,
   2.133 +                           Have (qs, l, negate_term thy t,
   2.134                                   Facts (backpatch_label patches l)))
   2.135               else
   2.136                 second_pass end_qs (proof, assums,
   2.137 @@ -747,10 +757,10 @@
   2.138    let
   2.139      fun relabel_facts subst =
   2.140        apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   2.141 -    fun do_step (ps as Assume (l, t)) (proof, subst, assums) =
   2.142 +    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   2.143          (case AList.lookup (op aconv) assums t of
   2.144             SOME l' => (proof, (l', l) :: subst, assums)
   2.145 -         | NONE => (ps :: proof, subst, (t, l) :: assums))
   2.146 +         | NONE => (step :: proof, subst, (t, l) :: assums))
   2.147        | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   2.148          (Have (qs, l, t,
   2.149                 case by of
   2.150 @@ -758,14 +768,22 @@
   2.151                 | CaseSplit (proofs, facts) =>
   2.152                   CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   2.153           proof, subst, assums)
   2.154 -      | do_step ps (proof, subst, assums) = (ps :: proof, subst, assums)
   2.155 +      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   2.156      and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   2.157    in do_proof end
   2.158  
   2.159 +fun unskolemize_term t =
   2.160 +  fold exists_of (Term.add_consts t []
   2.161 +                  |> filter (is_skolem_const_name o fst) |> map Const) t
   2.162 +
   2.163 +fun unskolemize_step (Have (qs, l, t, by)) =
   2.164 +    Have (qs, l, unskolemize_term t, by)
   2.165 +  | unskolemize_step step = step
   2.166 +
   2.167  val then_chain_proof =
   2.168    let
   2.169      fun aux _ [] = []
   2.170 -      | aux _ ((ps as Assume (l, _)) :: proof) = ps :: aux l proof
   2.171 +      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   2.172        | aux l' (Have (qs, l, t, by) :: proof) =
   2.173          (case by of
   2.174             Facts (ls, ss) =>
   2.175 @@ -777,7 +795,7 @@
   2.176           | CaseSplit (proofs, facts) =>
   2.177             Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   2.178          aux l proof
   2.179 -      | aux _ (ps :: proof) = ps :: aux no_label proof
   2.180 +      | aux _ (step :: proof) = step :: aux no_label proof
   2.181    in aux no_label end
   2.182  
   2.183  fun kill_useless_labels_in_proof proof =
   2.184 @@ -791,7 +809,7 @@
   2.185                  CaseSplit (proofs, facts) =>
   2.186                  CaseSplit (map (map kill) proofs, facts)
   2.187                | _ => by)
   2.188 -      | kill ps = ps
   2.189 +      | kill step = step
   2.190    in map kill proof end
   2.191  
   2.192  fun prefix_for_depth n = replicate_string (n + 1)
   2.193 @@ -827,7 +845,8 @@
   2.194            Have (qs, l', t, by) ::
   2.195            aux subst depth (next_assum, next_fact) proof
   2.196          end
   2.197 -      | aux subst depth nextp (ps :: proof) = ps :: aux subst depth nextp proof
   2.198 +      | aux subst depth nextp (step :: proof) =
   2.199 +        step :: aux subst depth nextp proof
   2.200    in aux [] 0 (1, 1) end
   2.201  
   2.202  fun string_for_proof ctxt i n =
   2.203 @@ -896,8 +915,9 @@
   2.204      fun isar_proof_for () =
   2.205        case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
   2.206                                  frees
   2.207 -           |> direct_proof thy conjecture_shape hyp_ts concl_t
   2.208 +           |> redirect_proof thy conjecture_shape hyp_ts concl_t
   2.209             |> kill_duplicate_assumptions_in_proof
   2.210 +           |> map unskolemize_step
   2.211             |> then_chain_proof
   2.212             |> kill_useless_labels_in_proof
   2.213             |> relabel_proof
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 14:19:26 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 15:34:55 2010 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  
     3.5  signature SLEDGEHAMMER_UTIL =
     3.6  sig
     3.7 +  val is_new_spass_version : bool
     3.8    val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
     3.9    val plural_s : int -> string
    3.10    val serial_commas : string -> string list -> string list
    3.11 @@ -22,6 +23,18 @@
    3.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    3.13  struct
    3.14  
    3.15 +val is_new_spass_version =
    3.16 +  case getenv "SPASS_VERSION" of
    3.17 +    "" => case getenv "SPASS_HOME" of
    3.18 +            "" => false
    3.19 +          | s =>
    3.20 +            (* Hack: Preliminary versions of the SPASS 3.7 package don't set
    3.21 +               "SPASS_VERSION". *)
    3.22 +            String.isSubstring "/spass-3.7/" s
    3.23 +  | s => case s |> space_explode "." |> map Int.fromString of
    3.24 +           SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
    3.25 +         | _ => false
    3.26 +
    3.27  fun pairf f g x = (f x, g x)
    3.28  
    3.29  fun plural_s n = if n = 1 then "" else "s"