generalize proof reconstruction code;
authorblanchet
Tue Sep 14 17:36:27 2010 +0200 (2010-09-14)
changeset 39368f661064b2b80
parent 39367 ce60294425a0
child 39369 8e585c7d418a
generalize proof reconstruction code;
first step towards support for nonnumeric formula names, needed for E 1.2
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Sep 14 17:23:16 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Sep 14 17:36:27 2010 +0200
     1.3 @@ -62,12 +62,27 @@
     1.4    | mk_anot phi = AConn (ANot, [phi])
     1.5  fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
     1.6  
     1.7 +datatype tstp_name = Str of string | Num of int
     1.8 +
     1.9 +fun tstp_name_ord (Str s, Str t) = string_ord (s, t)
    1.10 +  | tstp_name_ord (Str _, Num _) = LESS
    1.11 +  | tstp_name_ord (Num i, Num j) = int_ord (i, j)
    1.12 +  | tstp_name_ord (Num _, Str _) = GREATER
    1.13 +
    1.14  fun index_in_shape x = find_index (exists (curry (op =) x))
    1.15 -fun is_axiom_number axiom_names num =
    1.16 -  num > 0 andalso num <= Vector.length axiom_names andalso
    1.17 -  not (null (Vector.sub (axiom_names, num - 1)))
    1.18 -fun is_conjecture_number conjecture_shape num =
    1.19 -  index_in_shape num conjecture_shape >= 0
    1.20 +fun resolve_axiom axiom_names (Str str) =
    1.21 +    (case find_first_in_list_vector axiom_names str of
    1.22 +       SOME x => [(str, x)]
    1.23 +     | NONE => [])
    1.24 +  | resolve_axiom axiom_names (Num num) =
    1.25 +    if num > 0 andalso num <= Vector.length axiom_names then
    1.26 +      Vector.sub (axiom_names, num - 1)
    1.27 +    else
    1.28 +      []
    1.29 +val is_axiom_name = not o null oo resolve_axiom
    1.30 +fun is_conjecture_name _ (Str str) = String.isPrefix conjecture_prefix str
    1.31 +  | is_conjecture_name conjecture_shape (Num num) =
    1.32 +    index_in_shape num conjecture_shape >= 0
    1.33  
    1.34  fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    1.35      Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    1.36 @@ -82,12 +97,12 @@
    1.37    | negate_term (@{const Not} $ t) = t
    1.38    | negate_term t = @{const Not} $ t
    1.39  
    1.40 -datatype ('a, 'b, 'c, 'd, 'e) raw_step =
    1.41 -  Definition of 'a * 'b * 'c |
    1.42 -  Inference of 'a * 'd * 'e list
    1.43 +datatype ('a, 'b, 'c) raw_step =
    1.44 +  Definition of tstp_name * 'a * 'b |
    1.45 +  Inference of tstp_name * 'c * tstp_name list
    1.46  
    1.47 -fun raw_step_number (Definition (num, _, _)) = num
    1.48 -  | raw_step_number (Inference (num, _, _)) = num
    1.49 +fun raw_step_name (Definition (name, _, _)) = name
    1.50 +  | raw_step_name (Inference (name, _, _)) = name
    1.51  
    1.52  (**** PARSING OF TSTP FORMAT ****)
    1.53  
    1.54 @@ -184,18 +199,19 @@
    1.55               "definition" =>
    1.56               (case phi of
    1.57                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
    1.58 -                Definition (num, phi1, phi2)
    1.59 +                Definition (Num num, phi1, phi2)
    1.60                | AAtom (ATerm ("c_equal", _)) =>
    1.61 -                Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
    1.62 +                (* Vampire's equality proxy axiom *)
    1.63 +                Inference (Num num, phi, map Num deps)
    1.64                | _ => raise Fail "malformed definition")
    1.65 -           | _ => Inference (num, phi, deps))
    1.66 +           | _ => Inference (Num num, phi, map Num deps))
    1.67  
    1.68  (**** PARSING OF VAMPIRE OUTPUT ****)
    1.69  
    1.70  (* Syntax: <num>. <formula> <annotation> *)
    1.71  fun parse_vampire_line pool =
    1.72    scan_integer --| $$ "." -- parse_formula pool -- parse_annotation
    1.73 -  >> (fn ((num, phi), deps) => Inference (num, phi, deps))
    1.74 +  >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
    1.75  
    1.76  (**** PARSING OF SPASS OUTPUT ****)
    1.77  
    1.78 @@ -230,7 +246,7 @@
    1.79  fun parse_spass_line pool =
    1.80    scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
    1.81      -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
    1.82 -  >> (fn ((num, deps), u) => Inference (num, u, deps))
    1.83 +  >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
    1.84  
    1.85  fun parse_line pool =
    1.86    parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
    1.87 @@ -447,7 +463,7 @@
    1.88  fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
    1.89    | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
    1.90  
    1.91 -fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt =
    1.92 +fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
    1.93      let
    1.94        val thy = ProofContext.theory_of ctxt
    1.95        val t1 = prop_from_formula thy full_types tfrees phi1
    1.96 @@ -460,16 +476,16 @@
    1.97          |> unvarify_args |> uncombine_term |> check_formula ctxt
    1.98          |> HOLogic.dest_eq
    1.99      in
   1.100 -      (Definition (num, t1, t2),
   1.101 +      (Definition (name, t1, t2),
   1.102         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   1.103      end
   1.104 -  | decode_line full_types tfrees (Inference (num, u, deps)) ctxt =
   1.105 +  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   1.106      let
   1.107        val thy = ProofContext.theory_of ctxt
   1.108        val t = u |> prop_from_formula thy full_types tfrees
   1.109                  |> uncombine_term |> check_formula ctxt
   1.110      in
   1.111 -      (Inference (num, t, deps),
   1.112 +      (Inference (name, t, deps),
   1.113         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   1.114      end
   1.115  fun decode_lines ctxt full_types tfrees lines =
   1.116 @@ -484,69 +500,69 @@
   1.117  
   1.118  fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
   1.119  fun replace_deps_in_line _ (line as Definition _) = line
   1.120 -  | replace_deps_in_line p (Inference (num, t, deps)) =
   1.121 -    Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
   1.122 +  | replace_deps_in_line p (Inference (name, t, deps)) =
   1.123 +    Inference (name, t, fold (union (op =) o replace_one_dep p) deps [])
   1.124  
   1.125  (* Discard axioms; consolidate adjacent lines that prove the same formula, since
   1.126     they differ only in type information.*)
   1.127  fun add_line _ _ (line as Definition _) lines = line :: lines
   1.128 -  | add_line conjecture_shape axiom_names (Inference (num, t, [])) lines =
   1.129 +  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   1.130      (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   1.131         definitions. *)
   1.132 -    if is_axiom_number axiom_names num then
   1.133 +    if is_axiom_name axiom_names name then
   1.134        (* Axioms are not proof lines. *)
   1.135        if is_only_type_information t then
   1.136 -        map (replace_deps_in_line (num, [])) lines
   1.137 +        map (replace_deps_in_line (name, [])) lines
   1.138        (* Is there a repetition? If so, replace later line by earlier one. *)
   1.139        else case take_prefix (not o is_same_inference t) lines of
   1.140          (_, []) => lines (*no repetition of proof line*)
   1.141 -      | (pre, Inference (num', _, _) :: post) =>
   1.142 -        pre @ map (replace_deps_in_line (num', [num])) post
   1.143 -    else if is_conjecture_number conjecture_shape num then
   1.144 -      Inference (num, negate_term t, []) :: lines
   1.145 +      | (pre, Inference (name', _, _) :: post) =>
   1.146 +        pre @ map (replace_deps_in_line (name', [name])) post
   1.147 +    else if is_conjecture_name conjecture_shape name then
   1.148 +      Inference (name, negate_term t, []) :: lines
   1.149      else
   1.150 -      map (replace_deps_in_line (num, [])) lines
   1.151 -  | add_line _ _ (Inference (num, t, deps)) lines =
   1.152 +      map (replace_deps_in_line (name, [])) lines
   1.153 +  | add_line _ _ (Inference (name, t, deps)) lines =
   1.154      (* Type information will be deleted later; skip repetition test. *)
   1.155      if is_only_type_information t then
   1.156 -      Inference (num, t, deps) :: lines
   1.157 +      Inference (name, t, deps) :: lines
   1.158      (* Is there a repetition? If so, replace later line by earlier one. *)
   1.159      else case take_prefix (not o is_same_inference t) lines of
   1.160        (* FIXME: Doesn't this code risk conflating proofs involving different
   1.161           types? *)
   1.162 -       (_, []) => Inference (num, t, deps) :: lines
   1.163 -     | (pre, Inference (num', t', _) :: post) =>
   1.164 -       Inference (num, t', deps) ::
   1.165 -       pre @ map (replace_deps_in_line (num', [num])) post
   1.166 +       (_, []) => Inference (name, t, deps) :: lines
   1.167 +     | (pre, Inference (name', t', _) :: post) =>
   1.168 +       Inference (name, t', deps) ::
   1.169 +       pre @ map (replace_deps_in_line (name', [name])) post
   1.170  
   1.171  (* Recursively delete empty lines (type information) from the proof. *)
   1.172 -fun add_nontrivial_line (Inference (num, t, [])) lines =
   1.173 -    if is_only_type_information t then delete_dep num lines
   1.174 -    else Inference (num, t, []) :: lines
   1.175 +fun add_nontrivial_line (Inference (name, t, [])) lines =
   1.176 +    if is_only_type_information t then delete_dep name lines
   1.177 +    else Inference (name, t, []) :: lines
   1.178    | add_nontrivial_line line lines = line :: lines
   1.179 -and delete_dep num lines =
   1.180 -  fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
   1.181 +and delete_dep name lines =
   1.182 +  fold_rev add_nontrivial_line (map (replace_deps_in_line (name, [])) lines) []
   1.183  
   1.184  (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   1.185     offending lines often does the trick. *)
   1.186  fun is_bad_free frees (Free x) = not (member (op =) frees x)
   1.187    | is_bad_free _ _ = false
   1.188  
   1.189 -fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
   1.190 -    (j, line :: map (replace_deps_in_line (num, [])) lines)
   1.191 +fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   1.192 +    (j, line :: map (replace_deps_in_line (name, [])) lines)
   1.193    | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   1.194 -                     (Inference (num, t, deps)) (j, lines) =
   1.195 +                     (Inference (name, t, deps)) (j, lines) =
   1.196      (j + 1,
   1.197 -     if is_axiom_number axiom_names num orelse
   1.198 -        is_conjecture_number conjecture_shape num orelse
   1.199 +     if is_axiom_name axiom_names name orelse
   1.200 +        is_conjecture_name conjecture_shape name orelse
   1.201          (not (is_only_type_information t) andalso
   1.202           null (Term.add_tvars t []) andalso
   1.203           not (exists_subterm (is_bad_free frees) t) andalso
   1.204           (null lines orelse (* last line must be kept *)
   1.205            (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
   1.206 -       Inference (num, t, deps) :: lines  (* keep line *)
   1.207 +       Inference (name, t, deps) :: lines  (* keep line *)
   1.208       else
   1.209 -       map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
   1.210 +       map (replace_deps_in_line (name, deps)) lines)  (* drop line *)
   1.211  
   1.212  (** EXTRACTING LEMMAS **)
   1.213  
   1.214 @@ -570,8 +586,7 @@
   1.215    let
   1.216      fun axiom_names_at_index num =
   1.217        let val j = Int.fromString num |> the_default ~1 in
   1.218 -        if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1)
   1.219 -        else []
   1.220 +        resolve_axiom axiom_names (Num j)
   1.221        end
   1.222      val tokens_of =
   1.223        String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
   1.224 @@ -603,6 +618,9 @@
   1.225  
   1.226  fun string_for_label (s, num) = s ^ string_of_int num
   1.227  
   1.228 +fun raw_label_for_name (Str str) = (raw_prefix ^ str, 0)
   1.229 +  | raw_label_for_name (Num num) = (raw_prefix, num)
   1.230 +
   1.231  fun metis_using [] = ""
   1.232    | metis_using ls =
   1.233      "using " ^ space_implode " " (map string_for_label ls) ^ " "
   1.234 @@ -664,19 +682,20 @@
   1.235  fun smart_case_split [] facts = ByMetis facts
   1.236    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   1.237  
   1.238 -fun add_fact_from_dep axiom_names num =
   1.239 -  if is_axiom_number axiom_names num then
   1.240 -    apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1))))
   1.241 +fun add_fact_from_dep axiom_names name =
   1.242 +  if is_axiom_name axiom_names name then
   1.243 +    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   1.244    else
   1.245 -    apfst (insert (op =) (raw_prefix, num))
   1.246 +    apfst (insert (op =) (raw_label_for_name name))
   1.247  
   1.248  fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   1.249  fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
   1.250  
   1.251  fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.252 -  | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
   1.253 -  | step_for_line axiom_names j (Inference (num, t, deps)) =
   1.254 -    Have (if j = 1 then [Show] else [], (raw_prefix, num),
   1.255 +  | step_for_line _ _ (Inference (name, t, [])) =
   1.256 +    Assume (raw_label_for_name name, t)
   1.257 +  | step_for_line axiom_names j (Inference (name, t, deps)) =
   1.258 +    Have (if j = 1 then [Show] else [], raw_label_for_name name,
   1.259            forall_vars t,
   1.260            ByMetis (fold (add_fact_from_dep axiom_names) deps ([], [])))
   1.261  
   1.262 @@ -686,7 +705,7 @@
   1.263      val lines =
   1.264        atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
   1.265        |> parse_proof pool
   1.266 -      |> sort (int_ord o pairself raw_step_number)
   1.267 +      |> sort (tstp_name_ord o pairself raw_step_name)
   1.268        |> decode_lines ctxt full_types tfrees
   1.269        |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   1.270        |> rpair [] |-> fold_rev add_nontrivial_line