diff -r 7cf8beb31e0f -r e820beaf7d8c src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Sep 02 08:40:25 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1038 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Claire Quigley, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Transfer of proofs from external provers. -*) - -signature SLEDGEHAMMER_PROOF_RECONSTRUCT = -sig - type locality = Sledgehammer_Fact_Filter.locality - type minimize_command = string list -> string - type metis_params = - bool * minimize_command * string * (string * locality) list vector * thm - * int - type isar_params = - string Symtab.table * bool * int * Proof.context * int list list - type text_result = string * (string * locality) list - - val metis_proof_text : metis_params -> text_result - val isar_proof_text : isar_params -> metis_params -> text_result - val proof_text : bool -> isar_params -> metis_params -> text_result -end; - -structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = -struct - -open ATP_Problem -open Metis_Clauses -open Sledgehammer_Util -open Sledgehammer_Fact_Filter -open Sledgehammer_Translate - -type minimize_command = string list -> string -type metis_params = - bool * minimize_command * string * (string * locality) list vector * thm * int -type isar_params = - string Symtab.table * bool * int * Proof.context * int list list -type text_result = string * (string * locality) list - -(* Simple simplifications to ensure that sort annotations don't leave a trail of - spurious "True"s. *) -fun s_not @{const False} = @{const True} - | s_not @{const True} = @{const False} - | s_not (@{const Not} $ t) = t - | s_not t = @{const Not} $ t -fun s_conj (@{const True}, t2) = t2 - | s_conj (t1, @{const True}) = t1 - | s_conj p = HOLogic.mk_conj p -fun s_disj (@{const False}, t2) = t2 - | s_disj (t1, @{const False}) = t1 - | s_disj p = HOLogic.mk_disj p -fun s_imp (@{const True}, t2) = t2 - | s_imp (t1, @{const False}) = s_not t1 - | s_imp p = HOLogic.mk_imp p -fun s_iff (@{const True}, t2) = t2 - | s_iff (t1, @{const True}) = t1 - | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 - -fun mk_anot (AConn (ANot, [phi])) = phi - | mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) - -fun index_in_shape x = find_index (exists (curry (op =) x)) -fun is_axiom_number axiom_names num = - num > 0 andalso num <= Vector.length axiom_names andalso - not (null (Vector.sub (axiom_names, num - 1))) -fun is_conjecture_number conjecture_shape num = - index_in_shape num conjecture_shape >= 0 - -fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = - Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t') - | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = - Const (@{const_name All}, T) $ Abs (s, T', negate_term t') - | negate_term (@{const HOL.implies} $ t1 $ t2) = - @{const HOL.conj} $ t1 $ negate_term t2 - | negate_term (@{const HOL.conj} $ t1 $ t2) = - @{const HOL.disj} $ negate_term t1 $ negate_term t2 - | negate_term (@{const HOL.disj} $ t1 $ t2) = - @{const HOL.conj} $ negate_term t1 $ negate_term t2 - | negate_term (@{const Not} $ t) = t - | negate_term t = @{const Not} $ t - -datatype ('a, 'b, 'c, 'd, 'e) raw_step = - Definition of 'a * 'b * 'c | - Inference of 'a * 'd * 'e list - -fun raw_step_number (Definition (num, _, _)) = num - | raw_step_number (Inference (num, _, _)) = num - -(**** PARSING OF TSTP FORMAT ****) - -(*Strings enclosed in single quotes, e.g. filenames*) -val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode; - -val scan_dollar_name = - Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) - -fun repair_name _ "$true" = "c_True" - | repair_name _ "$false" = "c_False" - | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *) - | repair_name _ "equal" = "c_equal" (* needed by SPASS? *) - | repair_name pool s = - case Symtab.lookup pool s of - SOME s' => s' - | NONE => - if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then - "c_equal" (* seen in Vampire proofs *) - else - s -(* Generalized first-order terms, which include file names, numbers, etc. *) -val parse_potential_integer = - (scan_dollar_name || scan_quoted) >> K NONE - || scan_integer >> SOME -fun parse_annotation x = - ((parse_potential_integer ::: Scan.repeat ($$ " " |-- parse_potential_integer) - >> map_filter I) -- Scan.optional parse_annotation [] - >> uncurry (union (op =)) - || $$ "(" |-- parse_annotations --| $$ ")" - || $$ "[" |-- parse_annotations --| $$ "]") x -and parse_annotations x = - (Scan.optional (parse_annotation - ::: Scan.repeat ($$ "," |-- parse_annotation)) [] - >> (fn numss => fold (union (op =)) numss [])) x - -(* Vampire proof lines sometimes contain needless information such as "(0:3)", - which can be hard to disambiguate from function application in an LL(1) - parser. As a workaround, we extend the TPTP term syntax with such detritus - and ignore it. *) -fun parse_vampire_detritus x = - (scan_integer |-- $$ ":" --| scan_integer >> K []) x - -fun parse_term pool x = - ((scan_dollar_name >> repair_name pool) - -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool) - --| $$ ")") [] - --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") [] - >> ATerm) x -and parse_terms pool x = - (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x - -fun parse_atom pool = - parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "=" - -- parse_term pool) - >> (fn (u1, NONE) => AAtom u1 - | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2])) - | (u1, SOME (SOME _, u2)) => - mk_anot (AAtom (ATerm ("c_equal", [u1, u2])))) - -fun fo_term_head (ATerm (s, _)) = s - -(* TPTP formulas are fully parenthesized, so we don't need to worry about - operator precedence. *) -fun parse_formula pool x = - (($$ "(" |-- parse_formula pool --| $$ ")" - || ($$ "!" >> K AForall || $$ "?" >> K AExists) - --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":" - -- parse_formula pool - >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) - || $$ "~" |-- parse_formula pool >> mk_anot - || parse_atom pool) - -- Scan.option ((Scan.this_string "=>" >> K AImplies - || Scan.this_string "<=>" >> K AIff - || Scan.this_string "<~>" >> K ANotIff - || Scan.this_string "<=" >> K AIf - || $$ "|" >> K AOr || $$ "&" >> K AAnd) - -- parse_formula pool) - >> (fn (phi1, NONE) => phi1 - | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x - -val parse_tstp_extra_arguments = - Scan.optional ($$ "," |-- parse_annotation - --| Scan.option ($$ "," |-- parse_annotations)) [] - -(* Syntax: (fof|cnf)\(, , \). - The could be an identifier, but we assume integers. *) - fun parse_tstp_line pool = - ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") - |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ "," - -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." - >> (fn (((num, role), phi), deps) => - case role of - "definition" => - (case phi of - AConn (AIff, [phi1 as AAtom _, phi2]) => - Definition (num, phi1, phi2) - | AAtom (ATerm ("c_equal", _)) => - Inference (num, phi, deps) (* Vampire's equality proxy axiom *) - | _ => raise Fail "malformed definition") - | _ => Inference (num, phi, deps)) - -(**** PARSING OF VAMPIRE OUTPUT ****) - -(* Syntax: . *) -fun parse_vampire_line pool = - scan_integer --| $$ "." -- parse_formula pool -- parse_annotation - >> (fn ((num, phi), deps) => Inference (num, phi, deps)) - -(**** PARSING OF SPASS OUTPUT ****) - -(* SPASS returns clause references of the form "x.y". We ignore "y", whose role - is not clear anyway. *) -val parse_dot_name = scan_integer --| $$ "." --| scan_integer - -val parse_spass_annotations = - Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name - --| Scan.option ($$ ","))) [] - -(* It is not clear why some literals are followed by sequences of stars and/or - pluses. We ignore them. *) -fun parse_decorated_atom pool = - parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ") - -fun mk_horn ([], []) = AAtom (ATerm ("c_False", [])) - | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits - | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits) - | mk_horn (neg_lits, pos_lits) = - mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, - foldr1 (mk_aconn AOr) pos_lits) - -fun parse_horn_clause pool = - Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|" - -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">" - -- Scan.repeat (parse_decorated_atom pool) - >> (mk_horn o apfst (op @)) - -(* Syntax: [0:] - || -> . *) -fun parse_spass_line pool = - scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id - -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "." - >> (fn ((num, deps), u) => Inference (num, u, deps)) - -fun parse_line pool = - parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool -fun parse_lines pool = Scan.repeat1 (parse_line pool) -fun parse_proof pool = - fst o Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output") - (parse_lines pool))) - o explode o strip_spaces_except_between_ident_chars - -(**** INTERPRETATION OF TSTP SYNTAX TREES ****) - -exception FO_TERM of string fo_term list -exception FORMULA of (string, string fo_term) formula list -exception SAME of unit - -(* Type variables are given the basic sort "HOL.type". Some will later be - constrained by information from type literals, or by type inference. *) -fun type_from_fo_term tfrees (u as ATerm (a, us)) = - let val Ts = map (type_from_fo_term tfrees) 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 - | NONE => - case strip_prefix_and_unascii tvar_prefix a of - SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) - | NONE => - (* Variable from the ATP, say "X1" *) - Type_Infer.param 0 (a, HOLogic.typeS) - end - -(* Type class literal applied to a type. Returns triple of polarity, class, - type. *) -fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = - case (strip_prefix_and_unascii class_prefix a, - map (type_from_fo_term tfrees) us) of - (SOME b, [T]) => (pos, b, T) - | _ => raise FO_TERM [u] - -(** Accumulate type constraints in a formula: negative type literals **) -fun add_var (key, z) = Vartab.map_default (key, []) (cons z) -fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) - | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) - | add_type_constraint _ = I - -fun repair_atp_variable_name f s = - let - fun subscript_name s n = s ^ nat_subscript n - val s = String.map f s - in - case space_explode "_" s of - [_] => (case take_suffix Char.isDigit (String.explode s) of - (cs1 as _ :: _, cs2 as _ :: _) => - subscript_name (String.implode cs1) - (the (Int.fromString (String.implode cs2))) - | (_, _) => s) - | [s1, s2] => (case Int.fromString s2 of - SOME n => subscript_name s1 n - | NONE => s) - | _ => s - end - -(* First-order translation. No types are known for variables. "HOLogic.typeT" - should allow them to be inferred. *) -fun raw_term_from_pred thy full_types tfrees = - let - fun aux opt_T extra_us u = - case u of - ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 - | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 - | ATerm (a, us) => - if a = type_wrapper_name then - case us of - [typ_u, term_u] => - aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u - | _ => raise FO_TERM us - else case strip_prefix_and_unascii const_prefix a of - SOME "equal" => - list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), - map (aux NONE []) us) - | SOME b => - let - val c = invert_const b - val num_type_args = num_type_args thy c - val (type_us, term_us) = - chop (if full_types then 0 else num_type_args) us - (* Extra args from "hAPP" come after any arguments given directly to - the constant. *) - val term_ts = map (aux NONE []) term_us - val extra_ts = map (aux NONE []) extra_us - val t = - Const (c, if full_types then - case opt_T of - SOME T => map fastype_of term_ts ---> T - | NONE => - if num_type_args = 0 then - Sign.const_instance thy (c, []) - else - raise Fail ("no type information for " ^ quote c) - else - Sign.const_instance thy (c, - map (type_from_fo_term tfrees) type_us)) - in list_comb (t, term_ts @ extra_ts) end - | NONE => (* a free or schematic variable *) - let - val ts = map (aux NONE []) (us @ extra_us) - val T = map fastype_of ts ---> HOLogic.typeT - val t = - case strip_prefix_and_unascii fixed_var_prefix a of - SOME b => Free (b, T) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix a of - SOME b => Var ((b, 0), T) - | NONE => - if is_tptp_variable a then - Var ((repair_atp_variable_name Char.toLower a, 0), T) - else - (* Skolem constants? *) - Var ((repair_atp_variable_name Char.toUpper a, 0), T) - in list_comb (t, ts) end - in aux (SOME HOLogic.boolT) [] end - -fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = - if String.isPrefix class_prefix s then - add_type_constraint (type_constraint_from_term pos tfrees u) - #> pair @{const True} - else - pair (raw_term_from_pred thy full_types tfrees u) - -val combinator_table = - [(@{const_name COMBI}, @{thm COMBI_def_raw}), - (@{const_name COMBK}, @{thm COMBK_def_raw}), - (@{const_name COMBB}, @{thm COMBB_def_raw}), - (@{const_name COMBC}, @{thm COMBC_def_raw}), - (@{const_name COMBS}, @{thm COMBS_def_raw})] - -fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) - | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') - | uncombine_term (t as Const (x as (s, _))) = - (case AList.lookup (op =) combinator_table s of - SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd - | NONE => t) - | uncombine_term t = t - -(* Update schematic type variables with detected sort constraints. It's not - totally clear when this code is necessary. *) -fun repair_tvar_sorts (t, tvar_tab) = - let - fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) - | do_type (TVar (xi, s)) = - TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) - | do_type (TFree z) = TFree z - fun do_term (Const (a, T)) = Const (a, do_type T) - | do_term (Free (a, T)) = Free (a, do_type T) - | do_term (Var (xi, T)) = Var (xi, do_type T) - | do_term (t as Bound _) = t - | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) - | do_term (t1 $ t2) = do_term t1 $ do_term t2 - in t |> not (Vartab.is_empty tvar_tab) ? do_term end - -fun quantify_over_free quant_s free_s body_t = - case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of - [] => body_t - | frees as (_, free_T) :: _ => - Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t) - -(* Interpret an ATP formula as a HOL term, extracting sort constraints as they - appear in the formula. *) -fun prop_from_formula thy full_types tfrees phi = - let - fun do_formula pos phi = - case phi of - AQuant (_, [], phi) => do_formula pos phi - | AQuant (q, x :: xs, phi') => - do_formula pos (AQuant (q, xs, phi')) - #>> quantify_over_free (case q of - AForall => @{const_name All} - | AExists => @{const_name Ex}) - (repair_atp_variable_name Char.toLower x) - | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not - | AConn (c, [phi1, phi2]) => - do_formula (pos |> c = AImplies ? not) phi1 - ##>> do_formula pos phi2 - #>> (case c of - AAnd => s_conj - | AOr => s_disj - | AImplies => s_imp - | AIf => s_imp o swap - | AIff => s_iff - | ANotIff => s_not o s_iff) - | AAtom tm => term_from_pred thy full_types tfrees pos tm - | _ => raise FORMULA [phi] - in repair_tvar_sorts (do_formula true phi Vartab.empty) end - -fun check_formula ctxt = - Type_Infer.constrain HOLogic.boolT - #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) - - -(**** Translation of TSTP files to Isar Proofs ****) - -fun unvarify_term (Var ((s, 0), T)) = Free (s, T) - | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) - -fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt = - let - val thy = ProofContext.theory_of ctxt - val t1 = prop_from_formula thy full_types tfrees phi1 - val vars = snd (strip_comb t1) - val frees = map unvarify_term vars - val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_formula thy full_types tfrees phi2 - val (t1, t2) = - HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term |> check_formula ctxt - |> HOLogic.dest_eq - in - (Definition (num, t1, t2), - fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) - end - | decode_line full_types tfrees (Inference (num, u, deps)) ctxt = - let - val thy = ProofContext.theory_of ctxt - val t = u |> prop_from_formula thy full_types tfrees - |> uncombine_term |> check_formula ctxt - in - (Inference (num, t, deps), - fold Variable.declare_term (OldTerm.term_frees t) ctxt) - end -fun decode_lines ctxt full_types tfrees lines = - fst (fold_map (decode_line full_types tfrees) lines ctxt) - -fun is_same_inference _ (Definition _) = false - | is_same_inference t (Inference (_, t', _)) = t aconv t' - -(* No "real" literals means only type information (tfree_tcs, clsrel, or - clsarity). *) -val is_only_type_information = curry (op aconv) HOLogic.true_const - -fun replace_one_dep (old, new) dep = if dep = old then new else [dep] -fun replace_deps_in_line _ (line as Definition _) = line - | replace_deps_in_line p (Inference (num, t, deps)) = - Inference (num, t, fold (union (op =) o replace_one_dep p) deps []) - -(* Discard axioms; consolidate adjacent lines that prove the same formula, since - they differ only in type information.*) -fun add_line _ _ (line as Definition _) lines = line :: lines - | add_line conjecture_shape axiom_names (Inference (num, t, [])) lines = - (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or - definitions. *) - if is_axiom_number axiom_names num then - (* Axioms are not proof lines. *) - if is_only_type_information t then - map (replace_deps_in_line (num, [])) lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (_, []) => lines (*no repetition of proof line*) - | (pre, Inference (num', _, _) :: post) => - pre @ map (replace_deps_in_line (num', [num])) post - else if is_conjecture_number conjecture_shape num then - Inference (num, negate_term t, []) :: lines - else - map (replace_deps_in_line (num, [])) lines - | add_line _ _ (Inference (num, t, deps)) lines = - (* Type information will be deleted later; skip repetition test. *) - if is_only_type_information t then - Inference (num, t, deps) :: lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (* FIXME: Doesn't this code risk conflating proofs involving different - types? *) - (_, []) => Inference (num, t, deps) :: lines - | (pre, Inference (num', t', _) :: post) => - Inference (num, t', deps) :: - pre @ map (replace_deps_in_line (num', [num])) post - -(* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (Inference (num, t, [])) lines = - if is_only_type_information t then delete_dep num lines - else Inference (num, t, []) :: lines - | add_nontrivial_line line lines = line :: lines -and delete_dep num lines = - fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) [] - -(* ATPs sometimes reuse free variable names in the strangest ways. Removing - offending lines often does the trick. *) -fun is_bad_free frees (Free x) = not (member (op =) frees x) - | is_bad_free _ _ = false - -(* Vampire is keen on producing these. *) -fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _) - $ t1 $ t2)) = (t1 aconv t2) - | is_trivial_formula _ = false - -fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = - (j, line :: map (replace_deps_in_line (num, [])) lines) - | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees - (Inference (num, t, deps)) (j, lines) = - (j + 1, - if is_axiom_number axiom_names num orelse - is_conjecture_number conjecture_shape num orelse - (not (is_only_type_information t) andalso - null (Term.add_tvars t []) andalso - not (exists_subterm (is_bad_free frees) t) andalso - not (is_trivial_formula t) andalso - (null lines orelse (* last line must be kept *) - (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then - Inference (num, t, deps) :: lines (* keep line *) - else - map (replace_deps_in_line (num, deps)) lines) (* drop line *) - -(** EXTRACTING LEMMAS **) - -(* Like "split_line", but ignores "\n" that follow a comma (as in SNARK's - output). *) -val split_proof_lines = - let - fun aux [] [] = [] - | aux line [] = [implode (rev line)] - | aux line ("," :: "\n" :: rest) = aux ("," :: line) rest - | aux line ("\n" :: rest) = aux line [] @ aux [] rest - | aux line (s :: rest) = aux (s :: line) rest - in aux [] o explode end - -(* A list consisting of the first number in each line is returned. For TSTP, - interesting lines have the form "fof(108, axiom, ...)", where the number - (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where - the first number (108) is extracted. For Vampire, we look for - "108. ... [input]". *) -fun used_facts_in_atp_proof axiom_names atp_proof = - let - fun axiom_names_at_index num = - let val j = Int.fromString num |> the_default ~1 in - if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1) - else [] - end - val tokens_of = - String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") - fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = - if tag = "cnf" orelse tag = "fof" then - (case strip_prefix_and_unascii axiom_prefix (List.last rest) of - SOME name => - if member (op =) rest "file" then - ([(name, name |> find_first_in_list_vector axiom_names |> the)] - handle Option.Option => - error ("No such fact: " ^ quote name ^ ".")) - else - axiom_names_at_index num - | NONE => axiom_names_at_index num) - else - [] - | do_line (num :: "0" :: "Inp" :: _) = axiom_names_at_index num - | do_line (num :: rest) = - (case List.last rest of "input" => axiom_names_at_index num | _ => []) - | do_line _ = [] - in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end - -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "X" -val assum_prefix = "A" -val fact_prefix = "F" - -fun string_for_label (s, num) = s ^ string_of_int num - -fun metis_using [] = "" - | metis_using ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_apply _ 1 = "by " - | metis_apply 1 _ = "apply " - | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " -fun metis_name full_types = if full_types then "metisFT" else "metis" -fun metis_call full_types [] = metis_name full_types - | metis_call full_types ss = - "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" -fun metis_command full_types i n (ls, ss) = - metis_using ls ^ metis_apply i n ^ metis_call full_types ss -fun metis_line full_types i n ss = - "Try this command: " ^ - Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => - "\nTo minimize the number of lemmas, try this: " ^ - Markup.markup Markup.sendback command ^ "." - -fun used_facts axiom_names = - used_facts_in_atp_proof axiom_names - #> List.partition (curry (op =) Chained o snd) - #> pairself (sort_distinct (string_ord o pairself fst)) - -fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, - goal, i) = - let - val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof - val n = Logic.count_prems (prop_of goal) - in - (metis_line full_types i n (map fst other_lemmas) ^ - minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), - other_lemmas @ chained_lemmas) - end - -(** Isar proof construction and manipulation **) - -fun merge_fact_sets (ls1, ss1) (ls2, ss2) = - (union (op =) ls1 ls2, union (op =) ss1 ss2) - -type label = string * int -type facts = label list * string list - -datatype qualifier = Show | Then | Moreover | Ultimately - -datatype step = - Fix of (string * typ) list | - Let of term * term | - Assume of label * term | - Have of qualifier list * label * term * byline -and byline = - ByMetis of facts | - CaseSplit of step list list * facts - -fun smart_case_split [] facts = ByMetis facts - | smart_case_split proofs facts = CaseSplit (proofs, facts) - -fun add_fact_from_dep axiom_names num = - if is_axiom_number axiom_names num then - apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1)))) - else - apfst (insert (op =) (raw_prefix, num)) - -fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t -fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t - -fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2) - | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) - | step_for_line axiom_names j (Inference (num, t, deps)) = - Have (if j = 1 then [Show] else [], (raw_prefix, num), - forall_vars t, - ByMetis (fold (add_fact_from_dep axiom_names) deps ([], []))) - -fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor - atp_proof conjecture_shape axiom_names params frees = - let - val lines = - atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - |> parse_proof pool - |> sort (int_ord o pairself raw_step_number) - |> decode_lines ctxt full_types tfrees - |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) - |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor - conjecture_shape axiom_names frees) - |> snd - in - (if null params then [] else [Fix params]) @ - map2 (step_for_line axiom_names) (length lines downto 1) lines - end - -(* When redirecting proofs, we keep information about the labels seen so far in - the "backpatches" data structure. The first component indicates which facts - should be associated with forthcoming proof steps. The second component is a - pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should - become assumptions and "drop_ls" are the labels that should be dropped in a - case split. *) -type backpatches = (label * facts) list * (label list * label list) - -fun used_labels_of_step (Have (_, _, _, by)) = - (case by of - ByMetis (ls, _) => ls - | CaseSplit (proofs, (ls, _)) => - fold (union (op =) o used_labels_of) proofs ls) - | used_labels_of_step _ = [] -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] - -fun new_labels_of_step (Fix _) = [] - | new_labels_of_step (Let _) = [] - | new_labels_of_step (Assume (l, _)) = [l] - | new_labels_of_step (Have (_, l, _, _)) = [l] -val new_labels_of = maps new_labels_of_step - -val join_proofs = - let - fun aux _ [] = NONE - | aux proof_tail (proofs as (proof1 :: _)) = - if exists null proofs then - NONE - else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then - aux (hd proof1 :: proof_tail) (map tl proofs) - else case hd proof1 of - Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) - if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') - | _ => false) (tl proofs) andalso - not (exists (member (op =) (maps new_labels_of proofs)) - (used_labels_of proof_tail)) then - SOME (l, t, map rev proofs, proof_tail) - else - NONE - | _ => NONE - in aux [] o map rev end - -fun case_split_qualifiers proofs = - case length proofs of - 0 => [] - | 1 => [Then] - | _ => [Ultimately] - -fun redirect_proof conjecture_shape hyp_ts concl_t proof = - let - (* The first pass outputs those steps that are independent of the negated - conjecture. The second pass flips the proof by contradiction to obtain a - direct proof, introducing case splits when an inference depends on - several facts that depend on the negated conjecture. *) - fun find_hyp num = - nth hyp_ts (index_in_shape num conjecture_shape) - handle Subscript => - raise Fail ("Cannot find hypothesis " ^ Int.toString num) - val concl_ls = map (pair raw_prefix) (List.last conjecture_shape) - val canonicalize_labels = - map (fn l => if member (op =) concl_ls l then hd concl_ls else l) - #> distinct (op =) - fun first_pass ([], contra) = ([], contra) - | first_pass ((step as Fix _) :: proof, contra) = - first_pass (proof, contra) |>> cons step - | first_pass ((step as Let _) :: proof, contra) = - first_pass (proof, contra) |>> cons step - | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = - if member (op =) concl_ls l then - first_pass (proof, contra ||> l = hd concl_ls ? cons step) - else - first_pass (proof, contra) |>> cons (Assume (l, find_hyp num)) - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = - let - val ls = canonicalize_labels ls - val step = Have (qs, l, t, ByMetis (ls, ss)) - in - if exists (member (op =) (fst contra)) ls then - first_pass (proof, contra |>> cons l ||> cons step) - else - first_pass (proof, contra) |>> cons step - end - | first_pass _ = raise Fail "malformed proof" - val (proof_top, (contra_ls, contra_proof)) = - first_pass (proof, (concl_ls, [])) - val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst - fun backpatch_labels patches ls = - fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) - fun second_pass end_qs ([], assums, patches) = - ([Have (end_qs, no_label, concl_t, - ByMetis (backpatch_labels patches (map snd assums)))], patches) - | second_pass end_qs (Assume (l, t) :: proof, assums, patches) = - second_pass end_qs (proof, (t, l) :: assums, patches) - | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, - patches) = - if member (op =) (snd (snd patches)) l andalso - not (member (op =) (fst (snd patches)) l) andalso - not (AList.defined (op =) (fst patches) l) then - second_pass end_qs (proof, assums, patches ||> apsnd (append ls)) - else - (case List.partition (member (op =) contra_ls) ls of - ([contra_l], co_ls) => - if member (op =) qs Show then - second_pass end_qs (proof, assums, - patches |>> cons (contra_l, (co_ls, ss))) - else - second_pass end_qs - (proof, assums, - patches |>> cons (contra_l, (l :: co_ls, ss))) - |>> cons (if member (op =) (fst (snd patches)) l then - Assume (l, negate_term t) - else - Have (qs, l, negate_term t, - ByMetis (backpatch_label patches l))) - | (contra_ls as _ :: _, co_ls) => - let - val proofs = - map_filter - (fn l => - if member (op =) concl_ls l then - NONE - else - let - val drop_ls = filter (curry (op <>) l) contra_ls - in - second_pass [] - (proof, assums, - patches ||> apfst (insert (op =) l) - ||> apsnd (union (op =) drop_ls)) - |> fst |> SOME - end) contra_ls - val (assumes, facts) = - if member (op =) (fst (snd patches)) l then - ([Assume (l, negate_term t)], (l :: co_ls, ss)) - else - ([], (co_ls, ss)) - in - (case join_proofs proofs of - SOME (l, t, proofs, proof_tail) => - Have (case_split_qualifiers proofs @ - (if null proof_tail then end_qs else []), l, t, - smart_case_split proofs facts) :: proof_tail - | NONE => - [Have (case_split_qualifiers proofs @ end_qs, no_label, - concl_t, smart_case_split proofs facts)], - patches) - |>> append assumes - end - | _ => raise Fail "malformed proof") - | second_pass _ _ = raise Fail "malformed proof" - val proof_bottom = - second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst - in proof_top @ proof_bottom end - -(* FIXME: Still needed? Probably not. *) -val kill_duplicate_assumptions_in_proof = - let - fun relabel_facts subst = - apfst (map (fn l => AList.lookup (op =) subst l |> the_default l)) - fun do_step (step as Assume (l, t)) (proof, subst, assums) = - (case AList.lookup (op aconv) assums t of - SOME l' => (proof, (l, l') :: subst, assums) - | NONE => (step :: proof, subst, (t, l) :: assums)) - | do_step (Have (qs, l, t, by)) (proof, subst, assums) = - (Have (qs, l, t, - case by of - ByMetis facts => ByMetis (relabel_facts subst facts) - | CaseSplit (proofs, facts) => - CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: - proof, subst, assums) - | do_step step (proof, subst, assums) = (step :: proof, subst, assums) - and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev - in do_proof end - -val then_chain_proof = - let - fun aux _ [] = [] - | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof - | aux l' (Have (qs, l, t, by) :: proof) = - (case by of - ByMetis (ls, ss) => - Have (if member (op =) ls l' then - (Then :: qs, l, t, - ByMetis (filter_out (curry (op =) l') ls, ss)) - else - (qs, l, t, ByMetis (ls, ss))) - | CaseSplit (proofs, facts) => - Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: - aux l proof - | aux _ (step :: proof) = step :: aux no_label proof - in aux no_label end - -fun kill_useless_labels_in_proof proof = - let - val used_ls = used_labels_of proof - fun do_label l = if member (op =) used_ls l then l else no_label - fun do_step (Assume (l, t)) = Assume (do_label l, t) - | do_step (Have (qs, l, t, by)) = - Have (qs, do_label l, t, - case by of - CaseSplit (proofs, facts) => - CaseSplit (map (map do_step) proofs, facts) - | _ => by) - | do_step step = step - in map do_step proof end - -fun prefix_for_depth n = replicate_string (n + 1) - -val relabel_proof = - let - fun aux _ _ _ [] = [] - | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = - if l = no_label then - Assume (l, t) :: aux subst depth (next_assum, next_fact) proof - else - let val l' = (prefix_for_depth depth assum_prefix, next_assum) in - Assume (l', t) :: - aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof - end - | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = - let - val (l', subst, next_fact) = - if l = no_label then - (l, subst, next_fact) - else - let - val l' = (prefix_for_depth depth fact_prefix, next_fact) - in (l', (l, l') :: subst, next_fact + 1) end - val relabel_facts = - apfst (map (fn l => - case AList.lookup (op =) subst l of - SOME l' => l' - | NONE => raise Fail ("unknown label " ^ - quote (string_for_label l)))) - val by = - case by of - ByMetis facts => ByMetis (relabel_facts facts) - | CaseSplit (proofs, facts) => - CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) - in - Have (qs, l', t, by) :: - aux subst depth (next_assum, next_fact) proof - end - | aux subst depth nextp (step :: proof) = - step :: aux subst depth nextp proof - in aux [] 0 (1, 1) end - -fun string_for_proof ctxt full_types i n = - let - fun fix_print_mode f x = - setmp_CRITICAL show_no_free_types true - (setmp_CRITICAL show_types true - (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) f)) x - fun do_indent ind = replicate_string (ind * indent_size) " " - fun do_free (s, T) = - maybe_quote s ^ " :: " ^ - maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) - fun do_label l = if l = no_label then "" else string_for_label l ^ ": " - fun do_have qs = - (if member (op =) qs Moreover then "moreover " else "") ^ - (if member (op =) qs Ultimately then "ultimately " else "") ^ - (if member (op =) qs Then then - if member (op =) qs Show then "thus" else "hence" - else - if member (op =) qs Show then "show" else "have") - val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - fun do_facts (ls, ss) = - metis_command full_types 1 1 - (ls |> sort_distinct (prod_ord string_ord int_ord), - ss |> sort_distinct string_ord) - and do_step ind (Fix xs) = - do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" - | do_step ind (Let (t1, t2)) = - do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" - | do_step ind (Assume (l, t)) = - do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" - | do_step ind (Have (qs, l, t, ByMetis facts)) = - do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" - | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = - space_implode (do_indent ind ^ "moreover\n") - (map (do_block ind) proofs) ^ - do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ - do_facts facts ^ "\n" - and do_steps prefix suffix ind steps = - let val s = implode (map (do_step ind) steps) in - replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ - String.extract (s, ind * indent_size, - SOME (size s - ind * indent_size - 1)) ^ - suffix ^ "\n" - end - and do_block ind proof = do_steps "{ " " }" (ind + 1) proof - (* One-step proofs are pointless; better use the Metis one-liner - directly. *) - and do_proof [Have (_, _, _, ByMetis _)] = "" - | do_proof proof = - (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - do_indent 0 ^ "proof -\n" ^ - do_steps "" "" 1 proof ^ - do_indent 0 ^ (if n <> 1 then "next" else "qed") - in do_proof end - -fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (other_params as (full_types, _, atp_proof, axiom_names, - goal, i)) = - let - val (params, hyp_ts, concl_t) = strip_subgoal goal i - val frees = fold Term.add_frees (concl_t :: hyp_ts) [] - val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] - val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = metis_proof_text other_params - fun isar_proof_for () = - case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor - atp_proof conjecture_shape axiom_names params - frees - |> redirect_proof conjecture_shape hyp_ts concl_t - |> kill_duplicate_assumptions_in_proof - |> then_chain_proof - |> kill_useless_labels_in_proof - |> relabel_proof - |> string_for_proof ctxt full_types i n of - "" => "\nNo structured proof available." - | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof - val isar_proof = - if debug then - isar_proof_for () - else - try isar_proof_for () - |> the_default "\nWarning: The Isar proof construction failed." - in (one_line_proof ^ isar_proof, lemma_names) end - -fun proof_text isar_proof isar_params other_params = - (if isar_proof then isar_proof_text isar_params else metis_proof_text) - other_params - -end;