# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 0a2f5b86bdd7de6dc433fbcf20f7aad79ee28d7b # Parent 946c8e171ffdca793b1b2d0e94c23c8d68a3639e first step in sharing more code between ATP and Metis translation diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/ATP.thy Tue May 31 16:38:36 2011 +0200 @@ -6,12 +6,44 @@ header {* Automatic Theorem Provers (ATPs) *} theory ATP -imports Plain -uses "Tools/ATP/atp_problem.ML" +imports Meson +uses "Tools/ATP/atp_util.ML" + "Tools/ATP/atp_problem.ML" "Tools/ATP/atp_proof.ML" "Tools/ATP/atp_systems.ML" + ("Tools/ATP/atp_translate.ML") + ("Tools/ATP/atp_reconstruct.ML") begin +subsection {* Higher-order reasoning helpers *} + +definition fFalse :: bool where [no_atp]: +"fFalse \ False" + +definition fTrue :: bool where [no_atp]: +"fTrue \ True" + +definition fNot :: "bool \ bool" where [no_atp]: +"fNot P \ \ P" + +definition fconj :: "bool \ bool \ bool" where [no_atp]: +"fconj P Q \ P \ Q" + +definition fdisj :: "bool \ bool \ bool" where [no_atp]: +"fdisj P Q \ P \ Q" + +definition fimplies :: "bool \ bool \ bool" where [no_atp]: +"fimplies P Q \ (P \ Q)" + +definition fequal :: "'a \ 'a \ bool" where [no_atp]: +"fequal x y \ (x = y)" + + +subsection {* Setup *} + +use "Tools/ATP/atp_translate.ML" +use "Tools/ATP/atp_reconstruct.ML" + setup ATP_Systems.setup end diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/IsaMakefile Tue May 31 16:38:36 2011 +0200 @@ -300,7 +300,10 @@ $(SRC)/Provers/Arith/extract_common_term.ML \ Tools/ATP/atp_problem.ML \ Tools/ATP/atp_proof.ML \ + Tools/ATP/atp_reconstruct.ML \ Tools/ATP/atp_systems.ML \ + Tools/ATP/atp_translate.ML \ + Tools/ATP/atp_util.ML \ Tools/choice_specification.ML \ Tools/code_evaluation.ML \ Tools/groebner.ML \ @@ -353,8 +356,6 @@ Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/async_manager.ML \ - Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ - Tools/Sledgehammer/sledgehammer_atp_translate.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Metis.thy --- a/src/HOL/Metis.thy Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Metis.thy Tue May 31 16:38:36 2011 +0200 @@ -7,7 +7,7 @@ header {* Metis Proof Method *} theory Metis -imports Meson +imports ATP uses "~~/src/Tools/Metis/metis.ML" ("Tools/Metis/metis_translate.ML") ("Tools/Metis/metis_reconstruct.ML") @@ -15,31 +15,6 @@ ("Tools/try_methods.ML") begin - -subsection {* Higher-order reasoning helpers *} - -definition fFalse :: bool where [no_atp]: -"fFalse \ False" - -definition fTrue :: bool where [no_atp]: -"fTrue \ True" - -definition fNot :: "bool \ bool" where [no_atp]: -"fNot P \ \ P" - -definition fconj :: "bool \ bool \ bool" where [no_atp]: -"fconj P Q \ P \ Q" - -definition fdisj :: "bool \ bool \ bool" where [no_atp]: -"fdisj P Q \ P \ Q" - -definition fimplies :: "bool \ bool \ bool" where [no_atp]: -"fimplies P Q \ (P \ Q)" - -definition fequal :: "'a \ 'a \ bool" where [no_atp]: -"fequal x y \ (x = y)" - - subsection {* Literal selection helpers *} definition select :: "'a \ 'a" where diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Sledgehammer.thy Tue May 31 16:38:36 2011 +0200 @@ -11,8 +11,6 @@ uses "Tools/Sledgehammer/async_manager.ML" "Tools/Sledgehammer/sledgehammer_util.ML" "Tools/Sledgehammer/sledgehammer_filter.ML" - "Tools/Sledgehammer/sledgehammer_atp_translate.ML" - "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" "Tools/Sledgehammer/sledgehammer_provers.ML" "Tools/Sledgehammer/sledgehammer_minimize.ML" "Tools/Sledgehammer/sledgehammer_run.ML" diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200 @@ -70,9 +70,6 @@ -> 'd -> 'd val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula val is_format_typed : format -> bool - val timestamp : unit -> string - val hashw : word * word -> word - val hashw_string : string * word -> word val tptp_strings_for_atp_problem : format -> string problem -> string list val filter_cnf_ueq_problem : (string * string) problem -> (string * string) problem @@ -87,6 +84,9 @@ structure ATP_Problem : ATP_PROBLEM = struct +open ATP_Util + + (** ATP problem **) datatype 'a fo_term = ATerm of 'a * 'a fo_term list @@ -172,15 +172,6 @@ val is_format_typed = member (op =) [TFF, THF] -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now - -(* This hash function is recommended in "Compilers: Principles, Techniques, and - Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they - particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) -fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s - fun string_for_kind Axiom = "axiom" | string_for_kind Definition = "definition" | string_for_kind Lemma = "lemma" diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 31 16:38:36 2011 +0200 @@ -28,7 +28,6 @@ VampireTooOld | NoPerl | NoLibwwwPerl | - NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | @@ -44,7 +43,6 @@ type 'a proof = ('a, 'a, 'a fo_term) formula step list - val strip_spaces : bool -> (char -> bool) -> string -> string val short_output : bool -> string -> string val string_for_failure : failure -> string val extract_important_message : string -> string @@ -67,6 +65,7 @@ structure ATP_Proof : ATP_PROOF = struct +open ATP_Util open ATP_Problem exception UNRECOGNIZED_ATP_PROOF of unit @@ -85,7 +84,6 @@ VampireTooOld | NoPerl | NoLibwwwPerl | - NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | @@ -93,34 +91,6 @@ InternalError | UnknownError of string -fun strip_c_style_comment _ [] = [] - | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = - strip_spaces_in_list true is_evil cs - | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs -and strip_spaces_in_list _ _ [] = [] - | strip_spaces_in_list true is_evil (#"%" :: cs) = - strip_spaces_in_list true is_evil - (cs |> chop_while (not_equal #"\n") |> snd) - | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) = - strip_c_style_comment is_evil cs - | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1] - | strip_spaces_in_list skip_comments is_evil [c1, c2] = - strip_spaces_in_list skip_comments is_evil [c1] @ - strip_spaces_in_list skip_comments is_evil [c2] - | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) = - if Char.isSpace c1 then - strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) - else if Char.isSpace c2 then - if Char.isSpace c3 then - strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs) - else - str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @ - strip_spaces_in_list skip_comments is_evil (c3 :: cs) - else - str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) -fun strip_spaces skip_comments is_evil = - implode o strip_spaces_in_list skip_comments is_evil o String.explode - fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char @@ -182,12 +152,11 @@ | string_for_failure NoPerl = "Perl" ^ missing_message_tail | string_for_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail - | string_for_failure NoRealZ3 = - "The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path." | string_for_failure MalformedInput = "The generated problem is malformed. Please report this to the Isabelle \ \developers." | string_for_failure MalformedOutput = "The prover output is malformed." + | string_for_failure Interrupted = "The prover was interrupted." | string_for_failure Crashed = "The prover crashed." | string_for_failure InternalError = "An internal prover error occurred." | string_for_failure (UnknownError string) = diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/ATP/atp_reconstruct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200 @@ -0,0 +1,1100 @@ +(* Title: HOL/Tools/ATP/atp_reconstruct.ML + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Claire Quigley, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Proof reconstruction from ATP proofs. +*) + +signature ATP_RECONSTRUCT = +sig + type 'a proof = 'a ATP_Proof.proof + type locality = ATP_Translate.locality + type type_system = ATP_Translate.type_system + + datatype reconstructor = + Metis | + MetisFT | + SMT of string + + datatype play = + Played of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option| + Failed_to_Play + + type minimize_command = string list -> string + type one_line_params = + play * string * (string * locality) list * minimize_command * int * int + type isar_params = + bool * bool * int * type_system * string Symtab.table * int list list + * int * (string * locality) list vector * int Symtab.table * string proof + * thm + val repair_conjecture_shape_and_fact_names : + type_system -> string -> int list list -> int + -> (string * locality) list vector -> int list + -> int list list * int * (string * locality) list vector * int list + val used_facts_in_atp_proof : + Proof.context -> type_system -> int -> (string * locality) list vector + -> string proof -> (string * locality) list + val used_facts_in_unsound_atp_proof : + Proof.context -> type_system -> int list list -> int + -> (string * locality) list vector -> 'a proof -> string list option + val uses_typed_helpers : int list -> 'a proof -> bool + val reconstructor_name : reconstructor -> string + val one_line_proof_text : one_line_params -> string + val isar_proof_text : + Proof.context -> bool -> isar_params -> one_line_params -> string + val proof_text : + Proof.context -> bool -> isar_params -> one_line_params -> string +end; + +structure ATP_Reconstruct : ATP_RECONSTRUCT = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Translate + +datatype reconstructor = + Metis | + MetisFT | + SMT of string + +datatype play = + Played of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option | + Failed_to_Play + +type minimize_command = string list -> string +type one_line_params = + play * string * (string * locality) list * minimize_command * int * int +type isar_params = + bool * bool * int * type_system * string Symtab.table * int list list * int + * (string * locality) list vector * int Symtab.table * string proof * thm + +fun is_head_digit s = Char.isDigit (String.sub (s, 0)) +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) + +val is_typed_helper_name = + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix + +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec + + +(** SPASS's FLOTTER hack **) + +(* This is a hack required for keeping track of facts after they have been + clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is + also part of this hack. *) + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.position "." #> fst #> Substring.string + #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation + #> fst + +fun maybe_unprefix_fact_number type_sys = + polymorphism_of_type_sys type_sys <> Polymorphic + ? (space_implode "_" o tl o space_explode "_") + +fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape + fact_offset fact_names typed_helpers = + if String.isSubstring set_ClauseFormulaRelationN output then + let + val j0 = hd (hd conjecture_shape) + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + fun renumber_conjecture j = + conjecture_prefix ^ string_of_int (j - j0) + |> AList.find (fn (s, ss) => member (op =) ss s) name_map + |> map (fn s => find_index (curry (op =) s) seq + 1) + fun names_for_number j = + j |> AList.lookup (op =) name_map |> these + |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys + o unprefix fact_prefix)) + |> map (fn name => + (name, name |> find_first_in_list_vector fact_names |> the) + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) + in + (conjecture_shape |> map (maps renumber_conjecture), 0, + seq |> map names_for_number |> Vector.fromList, + name_map |> filter (forall is_typed_helper_name o snd) |> map fst) + end + else + (conjecture_shape, fact_offset, fact_names, typed_helpers) + +val vampire_step_prefix = "f" (* grrr... *) + +val extract_step_number = + Int.fromString o perhaps (try (unprefix vampire_step_prefix)) + +fun resolve_fact type_sys _ fact_names (_, SOME s) = + (case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in + case find_first_in_list_vector fact_names s' of + SOME x => [(s', x)] + | NONE => [] + end + | NONE => []) + | resolve_fact _ facts_offset fact_names (num, NONE) = + (case extract_step_number num of + SOME j => + let val j = j - facts_offset in + if j > 0 andalso j <= Vector.length fact_names then + Vector.sub (fact_names, j - 1) + else + [] + end + | NONE => []) + +fun is_fact type_sys conjecture_shape = + not o null o resolve_fact type_sys 0 conjecture_shape + +fun resolve_conjecture _ (_, SOME s) = + (case try (unprefix conjecture_prefix) s of + SOME s' => + (case Int.fromString s' of + SOME j => [j] + | NONE => []) + | NONE => []) + | resolve_conjecture conjecture_shape (num, NONE) = + case extract_step_number num of + SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of + ~1 => [] + | j => [j]) + | NONE => [] + +fun is_conjecture conjecture_shape = + not o null o resolve_conjecture conjecture_shape + +fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s + | is_typed_helper typed_helpers (num, NONE) = + (case extract_step_number num of + SOME i => member (op =) typed_helpers i + | NONE => false) + +val leo2_ext = "extcnf_equal_neg" +val isa_ext = Thm.get_name_hint @{thm ext} +val isa_short_ext = Long_Name.base_name isa_ext + +fun ext_name ctxt = + if Thm.eq_thm_prop (@{thm ext}, + singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then + isa_short_ext + else + isa_ext + +fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) = + union (op =) (resolve_fact type_sys facts_offset fact_names name) + | add_fact ctxt _ _ _ (Inference (_, _, deps)) = + if AList.defined (op =) deps leo2_ext then + insert (op =) (ext_name ctxt, General (* or Chained... *)) + else + I + | add_fact _ _ _ _ _ = I + +fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof = + if null atp_proof then Vector.foldl (op @) [] fact_names + else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof [] + +fun is_conjecture_referred_to_in_proof conjecture_shape = + exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name + | _ => false) + +fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset + fact_names atp_proof = + let + val used_facts = + used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof + in + if forall (is_locality_global o snd) used_facts andalso + not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then + SOME (map fst used_facts) + else + NONE + end + +fun uses_typed_helpers typed_helpers = + exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name + | _ => false) + + +(** Soft-core proof reconstruction: Metis one-liner **) + +fun reconstructor_name Metis = "metis" + | reconstructor_name MetisFT = "metisFT" + | reconstructor_name (SMT _) = "smt" + +fun reconstructor_settings (SMT settings) = settings + | reconstructor_settings _ = "" + +fun string_for_label (s, num) = s ^ string_of_int num + +fun show_time NONE = "" + | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" + +fun set_settings "" = "" + | set_settings settings = "using [[" ^ settings ^ "]] " +fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " + | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " + | apply_on_subgoal settings i n = + "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n +fun command_call name [] = name + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" +fun try_command_line banner time command = + banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "." +fun using_labels [] = "" + | using_labels ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " +fun reconstructor_command reconstructor i n (ls, ss) = + using_labels ls ^ + apply_on_subgoal (reconstructor_settings reconstructor) i n ^ + command_call (reconstructor_name reconstructor) ss +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + case minimize_command ss of + "" => "" + | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "." + +val split_used_facts = + List.partition (curry (op =) Chained o snd) + #> pairself (sort_distinct (string_ord o pairself fst)) + +fun one_line_proof_text (preplay, banner, used_facts, minimize_command, + subgoal, subgoal_count) = + let + val (chained, extra) = split_used_facts used_facts + val (reconstructor, ext_time) = + case preplay of + Played (reconstructor, time) => + (SOME reconstructor, (SOME (false, time))) + | Trust_Playable (reconstructor, time) => + (SOME reconstructor, + case time of + NONE => NONE + | SOME time => + if time = Time.zeroTime then NONE else SOME (true, time)) + | Failed_to_Play => (NONE, NONE) + val try_line = + case reconstructor of + SOME r => ([], map fst extra) + |> reconstructor_command r subgoal subgoal_count + |> try_command_line banner ext_time + | NONE => "One-line proof reconstruction failed." + in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end + +(** Hard-core proof reconstruction: structured Isar proofs **) + +(* Simple simplifications to ensure that sort annotations don't leave a trail of + spurious "True"s. *) +fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) = + Const (@{const_name Ex}, T) $ Abs (s, T', s_not t') + | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = + Const (@{const_name All}, T) $ Abs (s, T', s_not t') + | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2 + | s_not (@{const HOL.conj} $ t1 $ t2) = + @{const HOL.disj} $ s_not t1 $ s_not t2 + | s_not (@{const HOL.disj} $ t1 $ t2) = + @{const HOL.conj} $ s_not t1 $ s_not t2 + | 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 forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t + +val indent_size = 2 +val no_label = ("", ~1) + +val raw_prefix = "X" +val assum_prefix = "A" +val have_prefix = "F" + +fun raw_label_for_name conjecture_shape name = + case resolve_conjecture conjecture_shape name of + [j] => (conjecture_prefix, j) + | _ => case Int.fromString (fst name) of + SOME j => (raw_prefix, j) + | NONE => (raw_prefix ^ fst name, 0) + +(**** INTERPRETATION OF TSTP SYNTAX TREES ****) + +exception FO_TERM of string fo_term list +exception FORMULA of (string, 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 typ_from_fo_term tfrees (u as ATerm (a, us)) = + let val Ts = map (typ_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 tfrees (u as ATerm (a, us)) = + case (strip_prefix_and_unascii class_prefix a, + map (typ_from_fo_term tfrees) us) of + (SOME b, [T]) => (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_tptp_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 + +fun num_type_args thy s = + (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length + +(* First-order translation. No types are known for variables. "HOLogic.typeT" + should allow them to be inferred. *) +fun raw_term_from_pred thy sym_tab tfrees = + let + fun aux opt_T extra_us u = + case u of + ATerm (a, us) => + if String.isPrefix simple_type_prefix a then + @{const True} (* ignore TPTP type information *) + else if a = tptp_equal then + let val ts = map (aux NONE []) us in + if length ts = 2 andalso hd ts aconv List.last ts then + (* Vampire is keen on producing these. *) + @{const True} + else + list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) + end + else case strip_prefix_and_unascii const_prefix a of + SOME s => + let + val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const + in + if s' = type_tag_name then + case mangled_us @ us of + [typ_u, term_u] => + aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u + | _ => raise FO_TERM us + else if s' = predicator_name then + aux (SOME @{typ bool}) [] (hd us) + else if s' = app_op_name then + aux opt_T (nth us 1 :: extra_us) (hd us) + else if s' = type_pred_name then + @{const True} (* ignore type predicates *) + else + let + val num_ty_args = + length us - the_default 0 (Symtab.lookup sym_tab s) + val (type_us, term_us) = + chop num_ty_args us |>> append mangled_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 = + if not (null type_us) andalso + num_type_args thy s' = length type_us then + Sign.const_instance thy + (s', map (typ_from_fo_term tfrees) type_us) + else case opt_T of + SOME T => map fastype_of (term_ts @ extra_ts) ---> T + | NONE => HOLogic.typeT + val s' = s' |> unproxify_const + in list_comb (Const (s', T), term_ts @ extra_ts) end + 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_tptp_variable_name Char.toLower a, 0), T) + else + (* Skolem constants? *) + Var ((repair_tptp_variable_name Char.toUpper a, 0), T) + in list_comb (t, ts) end + in aux (SOME HOLogic.boolT) [] end + +fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) = + if String.isPrefix class_prefix s then + add_type_constraint pos (type_constraint_from_term tfrees u) + #> pair @{const True} + else + pair (raw_term_from_pred thy sym_tab tfrees u) + +val combinator_table = + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] + +fun uncombine_term thy = + let + fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) + | aux (Abs (s, T, t')) = Abs (s, T, aux t') + | aux (t as Const (x as (s, _))) = + (case AList.lookup (op =) combinator_table s of + SOME thm => thm |> prop_of |> specialize_type thy x + |> Logic.dest_equals |> snd + | NONE => t) + | aux t = t + in aux end + +(* Update schematic type variables with detected sort constraints. It's not + totally clear whether 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_var quant_of var_s t = + let + val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s) + |> map Var + in fold_rev quant_of vars t end + +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they + appear in the formula. *) +fun prop_from_formula thy sym_tab tfrees phi = + let + fun do_formula pos phi = + case phi of + AQuant (_, [], phi) => do_formula pos phi + | AQuant (q, (s, _) :: xs, phi') => + do_formula pos (AQuant (q, xs, phi')) + (* FIXME: TFF *) + #>> quantify_over_var (case q of + AForall => forall_of + | AExists => exists_of) + (repair_tptp_variable_name Char.toLower s) + | 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 + | _ => raise Fail "unexpected connective") + | AAtom tm => term_from_pred thy sym_tab tfrees pos tm + | _ => raise FORMULA [phi] + in repair_tvar_sorts (do_formula true phi Vartab.empty) end + +fun check_formula ctxt = + Type.constraint HOLogic.boolT + #> Syntax.check_term + (Proof_Context.set_mode Proof_Context.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 sym_tab tfrees (Definition (name, phi1, phi2)) ctxt = + let + val thy = Proof_Context.theory_of ctxt + val t1 = prop_from_formula thy sym_tab 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 sym_tab tfrees phi2 + val (t1, t2) = + HOLogic.eq_const HOLogic.typeT $ t1 $ t2 + |> unvarify_args |> uncombine_term thy |> check_formula ctxt + |> HOLogic.dest_eq + in + (Definition (name, t1, t2), + fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) + end + | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt = + let + val thy = Proof_Context.theory_of ctxt + val t = u |> prop_from_formula thy sym_tab tfrees + |> uncombine_term thy |> check_formula ctxt + in + (Inference (name, t, deps), + fold Variable.declare_term (OldTerm.term_frees t) ctxt) + end +fun decode_lines ctxt sym_tab tfrees lines = + fst (fold_map (decode_line sym_tab 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_dependency (old, new) dep = + if is_same_atp_step dep old then new else [dep] +fun replace_dependencies_in_line _ (line as Definition _) = line + | replace_dependencies_in_line p (Inference (name, t, deps)) = + Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) + +(* Discard facts; 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 type_sys conjecture_shape fact_names (Inference (name, t, [])) + lines = + (* No dependencies: fact, conjecture, or (for Vampire) internal facts or + definitions. *) + if is_fact type_sys fact_names name then + (* Facts are not proof lines. *) + if is_only_type_information t then + map (replace_dependencies_in_line (name, [])) 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 (name', _, _) :: post) => + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + else if is_conjecture conjecture_shape name then + Inference (name, s_not t, []) :: lines + else + map (replace_dependencies_in_line (name, [])) lines + | add_line _ _ _ (Inference (name, t, deps)) lines = + (* Type information will be deleted later; skip repetition test. *) + if is_only_type_information t then + Inference (name, 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 (name, t, deps) :: lines + | (pre, Inference (name', t', _) :: post) => + Inference (name, t', deps) :: + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + +(* Recursively delete empty lines (type information) from the proof. *) +fun add_nontrivial_line (Inference (name, t, [])) lines = + if is_only_type_information t then delete_dependency name lines + else Inference (name, t, []) :: lines + | add_nontrivial_line line lines = line :: lines +and delete_dependency name lines = + fold_rev add_nontrivial_line + (map (replace_dependencies_in_line (name, [])) 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 + +fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) = + (j, line :: map (replace_dependencies_in_line (name, [])) lines) + | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names + frees (Inference (name, t, deps)) (j, lines) = + (j + 1, + if is_fact type_sys fact_names name orelse + is_conjecture conjecture_shape name orelse + (* the last line must be kept *) + j = 0 orelse + (not (is_only_type_information t) andalso + null (Term.add_tvars t []) andalso + not (exists_subterm (is_bad_free frees) t) andalso + length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso + (* kill next to last line, which usually results in a trivial step *) + j <> 1) then + Inference (name, t, deps) :: lines (* keep line *) + else + map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) + +(** 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 isar_qualifier = Show | Then | Moreover | Ultimately + +datatype isar_step = + Fix of (string * typ) list | + Let of term * term | + Assume of label * term | + Have of isar_qualifier list * label * term * byline +and byline = + ByMetis of facts | + CaseSplit of isar_step list list * facts + +fun smart_case_split [] facts = ByMetis facts + | smart_case_split proofs facts = CaseSplit (proofs, facts) + +fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names + name = + if is_fact type_sys fact_names name then + apsnd (union (op =) + (map fst (resolve_fact type_sys facts_offset fact_names name))) + else + apfst (insert (op =) (raw_label_for_name conjecture_shape name)) + +fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) + | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) = + Assume (raw_label_for_name conjecture_shape name, t) + | step_for_line type_sys conjecture_shape facts_offset + fact_names j (Inference (name, t, deps)) = + Have (if j = 1 then [Show] else [], + raw_label_for_name conjecture_shape name, + fold_rev forall_of (map Var (Term.add_vars t [])) t, + ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape + facts_offset fact_names) + deps ([], []))) + +fun repair_name "$true" = "c_True" + | repair_name "$false" = "c_False" + | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) + | repair_name s = + if is_tptp_equal s orelse + (* seen in Vampire proofs *) + (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then + tptp_equal + else + s + +fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor + conjecture_shape facts_offset fact_names sym_tab params frees + atp_proof = + let + val lines = + atp_proof + |> clean_up_atp_proof_dependencies + |> nasty_atp_proof pool + |> map_term_names_in_atp_proof repair_name + |> decode_lines ctxt sym_tab tfrees + |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names) + |> rpair [] |-> fold_rev add_nontrivial_line + |> rpair (0, []) + |-> fold_rev (add_desired_line type_sys isar_shrink_factor + conjecture_shape fact_names frees) + |> snd + in + (if null params then [] else [Fix params]) @ + map2 (step_for_line type_sys conjecture_shape facts_offset fact_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 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. *) + val concl_l = (conjecture_prefix, length hyp_ts) + 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 (_, j), _)) :: proof, contra) = + if l = concl_l then first_pass (proof, contra ||> cons step) + else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j)) + | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = + let 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_l], [])) + 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, s_not t) + else + Have (qs, l, s_not t, + ByMetis (backpatch_label patches l))) + | (contra_ls as _ :: _, co_ls) => + let + val proofs = + map_filter + (fn l => + if l = concl_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, s_not 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 have_prefix, next_fact) + in (l', (l, l') :: subst, next_fact + 1) end + val relabel_facts = + apfst (maps (the_list o AList.lookup (op =) subst)) + 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 ctxt0 full_types i n = + let + val ctxt = + ctxt0 |> Config.put show_free_types false + |> Config.put show_types true + |> Config.put show_sorts true + fun fix_print_mode f x = + 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) + val reconstructor = if full_types then MetisFT else Metis + fun do_facts (ls, ss) = + reconstructor_command reconstructor 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 ctxt isar_proof_requested + (debug, full_types, isar_shrink_factor, type_sys, pool, + conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal) + (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = + let + val isar_shrink_factor = + (if isar_proof_requested then 1 else 2) * isar_shrink_factor + val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal + val frees = fold Term.add_frees (concl_t :: hyp_ts) [] + val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] + val one_line_proof = one_line_proof_text one_line_params + fun isar_proof_for () = + case atp_proof + |> isar_proof_from_atp_proof pool ctxt type_sys tfrees + isar_shrink_factor conjecture_shape facts_offset + fact_names sym_tab params frees + |> redirect_proof 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 subgoal subgoal_count of + "" => + if isar_proof_requested then + "\nNo structured proof available (proof too short)." + else + "" + | proof => + "\n\n" ^ (if isar_proof_requested then "Structured proof" + else "Perhaps this will work") ^ + ":\n" ^ Markup.markup Markup.sendback proof + val isar_proof = + if debug then + isar_proof_for () + else + case try isar_proof_for () of + SOME s => s + | NONE => if isar_proof_requested then + "\nWarning: The Isar proof construction failed." + else + "" + in one_line_proof ^ isar_proof end + +fun proof_text ctxt isar_proof isar_params + (one_line_params as (preplay, _, _, _, _, _)) = + (if isar_proof orelse preplay = Failed_to_Play then + isar_proof_text ctxt isar_proof isar_params + else + one_line_proof_text) one_line_params + +end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/ATP/atp_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -0,0 +1,1858 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Translation of HOL to FOL for Sledgehammer. +*) + +signature ATP_TRANSLATE = +sig + type 'a fo_term = 'a ATP_Problem.fo_term + type format = ATP_Problem.format + type formula_kind = ATP_Problem.formula_kind + type 'a problem = 'a ATP_Problem.problem + + type name = string * string + + datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + + datatype arity_literal = + TConsLit of name * name * name list | + TVarLit of name * name + + datatype arity_clause = + ArityClause of + {name: string, + prem_lits: arity_literal list, + concl_lits: arity_literal} + + datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + + datatype combterm = + CombConst of name * typ * typ list | + CombVar of name * typ | + CombApp of combterm * combterm + + datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained + + datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic + datatype type_level = + All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types + datatype type_heaviness = Heavy | Light + + datatype type_system = + Simple_Types of type_level | + Preds of polymorphism * type_level * type_heaviness | + Tags of polymorphism * type_level * type_heaviness + + type translated_formula + + val readable_names : bool Config.T + val type_tag_name : string + val bound_var_prefix : string + val schematic_var_prefix: string + val fixed_var_prefix: string + val tvar_prefix: string + val tfree_prefix: string + val const_prefix: string + val type_const_prefix: string + val class_prefix: string + val skolem_const_prefix : string + val old_skolem_const_prefix : string + val new_skolem_const_prefix : string + val fact_prefix : string + val conjecture_prefix : string + val helper_prefix : string + val typed_helper_suffix : string + val predicator_name : string + val app_op_name : string + val type_pred_name : string + val simple_type_prefix : string + val ascii_of: string -> string + val unascii_of: string -> string + val strip_prefix_and_unascii : string -> string -> string option + val proxify_const : string -> (int * (string * string)) option + val invert_const: string -> string + val unproxify_const: string -> string + val make_bound_var : string -> string + val make_schematic_var : string * int -> string + val make_fixed_var : string -> string + val make_schematic_type_var : string * int -> string + val make_fixed_type_var : string -> string + val make_fixed_const : string -> string + val make_fixed_type_const : string -> string + val make_type_class : string -> string + val make_arity_clauses : + theory -> string list -> class list -> class list * arity_clause list + val make_class_rel_clauses : + theory -> class list -> class list -> class_rel_clause list + val combtyp_of : combterm -> typ + val strip_combterm_comb : combterm -> combterm * combterm list + val atyps_of : typ -> typ list + val combterm_from_term : + theory -> (string * typ) list -> term -> combterm * typ list + val is_locality_global : locality -> bool + val type_sys_from_string : string -> type_system + val polymorphism_of_type_sys : type_system -> polymorphism + val level_of_type_sys : type_system -> type_level + val is_type_sys_virtually_sound : type_system -> bool + val is_type_sys_fairly_sound : type_system -> bool + val raw_type_literals_for_types : typ list -> type_literal list + val unmangled_const : string -> string * string fo_term list + val translate_atp_fact : + Proof.context -> format -> type_system -> bool -> (string * locality) * thm + -> translated_formula option * ((string * locality) * thm) + val helper_table : (string * (bool * thm list)) list + val tfree_classes_of_terms : term list -> string list + val tvar_classes_of_terms : term list -> string list + val type_consts_of_terms : theory -> term list -> string list + val prepare_atp_problem : + Proof.context -> format -> formula_kind -> formula_kind -> type_system + -> bool option -> term list -> term + -> (translated_formula option * ((string * 'a) * thm)) list + -> string problem * string Symtab.table * int * int + * (string * 'a) list vector * int list * int Symtab.table + val atp_problem_weights : string problem -> (string * real) list +end; + +structure ATP_Translate : ATP_TRANSLATE = +struct + +open ATP_Util +open ATP_Problem + +type name = string * string + +(* FIXME: avoid *) +fun union_all xss = fold (union (op =)) xss [] + +(* experimental *) +val generate_useful_info = false + +fun useful_isabelle_info s = + if generate_useful_info then + SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) + else + NONE + +val intro_info = useful_isabelle_info "intro" +val elim_info = useful_isabelle_info "elim" +val simp_info = useful_isabelle_info "simp" + +(* Readable names are often much shorter, especially if types are mangled in + names. Also, the logic for generating legal SNARK sort names is only + implemented for readable names. Finally, readable names are, well, more + readable. For these reason, they are enabled by default. *) +val readable_names = + Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) + +val type_tag_name = "ti" + +val bound_var_prefix = "B_" +val schematic_var_prefix = "V_" +val fixed_var_prefix = "v_" + +val tvar_prefix = "T_" +val tfree_prefix = "t_" + +val const_prefix = "c_" +val type_const_prefix = "tc_" +val class_prefix = "cl_" + +val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" +val old_skolem_const_prefix = skolem_const_prefix ^ "o" +val new_skolem_const_prefix = skolem_const_prefix ^ "n" + +val type_decl_prefix = "ty_" +val sym_decl_prefix = "sy_" +val sym_formula_prefix = "sym_" +val fact_prefix = "fact_" +val conjecture_prefix = "conj_" +val helper_prefix = "help_" +val class_rel_clause_prefix = "crel_"; +val arity_clause_prefix = "arity_" +val tfree_clause_prefix = "tfree_" + +val typed_helper_suffix = "_T" +val untyped_helper_suffix = "_U" + +val predicator_name = "hBOOL" +val app_op_name = "hAPP" +val type_pred_name = "is" +val simple_type_prefix = "ty_" + +(* Freshness almost guaranteed! *) +val sledgehammer_weak_prefix = "Sledgehammer:" + +(*Escaping of special characters. + Alphanumeric characters are left unchanged. + The character _ goes to __ + Characters in the range ASCII space to / go to _A to _P, respectively. + Other characters go to _nnn where nnn is the decimal ASCII code.*) +val upper_a_minus_space = Char.ord #"A" - Char.ord #" "; + +fun stringN_of_int 0 _ = "" + | stringN_of_int k n = + stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) + +fun ascii_of_char c = + if Char.isAlphaNum c then + String.str c + else if c = #"_" then + "__" + else if #" " <= c andalso c <= #"/" then + "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space)) + else + (* fixed width, in case more digits follow *) + "_" ^ stringN_of_int 3 (Char.ord c) + +val ascii_of = String.translate ascii_of_char + +(** Remove ASCII armoring from names in proof files **) + +(* We don't raise error exceptions because this code can run inside a worker + thread. Also, the errors are impossible. *) +val unascii_of = + let + fun un rcs [] = String.implode(rev rcs) + | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *) + (* Three types of _ escapes: __, _A to _P, _nnn *) + | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs + | un rcs (#"_" :: c :: cs) = + if #"A" <= c andalso c<= #"P" then + (* translation of #" " to #"/" *) + un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs + else + let val digits = List.take (c::cs, 3) handle Subscript => [] in + case Int.fromString (String.implode digits) of + SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2)) + | NONE => un (c:: #"_"::rcs) cs (* ERROR *) + end + | un rcs (c :: cs) = un (c :: rcs) cs + in un [] o String.explode end + +(* If string s has the prefix s1, return the result of deleting it, + un-ASCII'd. *) +fun strip_prefix_and_unascii s1 s = + if String.isPrefix s1 s then + SOME (unascii_of (String.extract (s, size s1, NONE))) + else + NONE + +val proxies = + [("c_False", + (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))), + ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))), + ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))), + ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))), + ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))), + ("c_implies", + (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))), + ("equal", + (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))] + +val proxify_const = AList.lookup (op =) proxies #> Option.map snd + +(* Readable names for the more common symbolic functions. Do not mess with the + table unless you know what you are doing. *) +val const_trans_table = + [(@{type_name Product_Type.prod}, "prod"), + (@{type_name Sum_Type.sum}, "sum"), + (@{const_name False}, "False"), + (@{const_name True}, "True"), + (@{const_name Not}, "Not"), + (@{const_name conj}, "conj"), + (@{const_name disj}, "disj"), + (@{const_name implies}, "implies"), + (@{const_name HOL.eq}, "equal"), + (@{const_name If}, "If"), + (@{const_name Set.member}, "member"), + (@{const_name Meson.COMBI}, "COMBI"), + (@{const_name Meson.COMBK}, "COMBK"), + (@{const_name Meson.COMBB}, "COMBB"), + (@{const_name Meson.COMBC}, "COMBC"), + (@{const_name Meson.COMBS}, "COMBS")] + |> Symtab.make + |> fold (Symtab.update o swap o snd o snd o snd) proxies + +(* Invert the table of translations between Isabelle and ATPs. *) +val const_trans_table_inv = + const_trans_table |> Symtab.dest |> map swap |> Symtab.make +val const_trans_table_unprox = + Symtab.empty + |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies + +val invert_const = perhaps (Symtab.lookup const_trans_table_inv) +val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox) + +fun lookup_const c = + case Symtab.lookup const_trans_table c of + SOME c' => c' + | NONE => ascii_of c + +(*Remove the initial ' character from a type variable, if it is present*) +fun trim_type_var s = + if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) + else raise Fail ("trim_type: Malformed type variable encountered: " ^ s) + +fun ascii_of_indexname (v,0) = ascii_of v + | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i + +fun make_bound_var x = bound_var_prefix ^ ascii_of x +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x + +fun make_schematic_type_var (x,i) = + tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i)) +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)) + +(* HOL.eq MUST BE "equal" because it's built into ATPs. *) +fun make_fixed_const @{const_name HOL.eq} = "equal" + | make_fixed_const c = const_prefix ^ lookup_const c + +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c + +fun make_type_class clas = class_prefix ^ ascii_of clas + +(** Definitions and functions for FOL clauses and formulas for TPTP **) + +(* The first component is the type class; the second is a "TVar" or "TFree". *) +datatype type_literal = + TyLitVar of name * name | + TyLitFree of name * name + + +(** Isabelle arities **) + +datatype arity_literal = + TConsLit of name * name * name list | + TVarLit of name * name + +fun gen_TVars 0 = [] + | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1); + +fun pack_sort (_,[]) = [] + | pack_sort (tvar, "HOL.type" :: srt) = + pack_sort (tvar, srt) (* IGNORE sort "type" *) + | pack_sort (tvar, cls :: srt) = + (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt) + +datatype arity_clause = + ArityClause of + {name: string, + prem_lits: arity_literal list, + concl_lits: arity_literal} + +(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *) +fun make_axiom_arity_clause (tcons, name, (cls, args)) = + let + val tvars = gen_TVars (length args) + val tvars_srts = ListPair.zip (tvars, args) + in + ArityClause {name = name, + prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)), + concl_lits = TConsLit (`make_type_class cls, + `make_fixed_type_const tcons, + tvars ~~ tvars)} + end + +fun arity_clause _ _ (_, []) = [] + | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) + arity_clause seen n (tcons,ars) + | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = + if member (op =) seen class then (*multiple arities for the same tycon, class pair*) + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) :: + arity_clause seen (n+1) (tcons,ars) + else + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: + arity_clause (class::seen) n (tcons,ars) + +fun multi_arity_clause [] = [] + | multi_arity_clause ((tcons, ars) :: tc_arlists) = + arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists + +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy + provided its arguments have the corresponding sorts.*) +fun type_class_pairs thy tycons classes = + let val alg = Sign.classes_of thy + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single + fun add_class tycon class = + cons (class, domain_sorts tycon class) + handle Sorts.CLASS_ERROR _ => I + fun try_classes tycon = (tycon, fold (add_class tycon) classes []) + in map try_classes tycons end; + +(*Proving one (tycon, class) membership may require proving others, so iterate.*) +fun iter_type_class_pairs _ _ [] = ([], []) + | iter_type_class_pairs thy tycons classes = + let val cpairs = type_class_pairs thy tycons classes + val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) + |> subtract (op =) classes |> subtract (op =) HOLogic.typeS + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses + in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; + +fun make_arity_clauses thy tycons = + iter_type_class_pairs thy tycons ##> multi_arity_clause + + +(** Isabelle class relations **) + +datatype class_rel_clause = + ClassRelClause of {name: string, subclass: name, superclass: name} + +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) +fun class_pairs _ [] _ = [] + | class_pairs thy subs supers = + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end + +fun make_class_rel_clause (sub,super) = + ClassRelClause {name = sub ^ "_" ^ super, + subclass = `make_type_class sub, + superclass = `make_type_class super} + +fun make_class_rel_clauses thy subs supers = + map make_class_rel_clause (class_pairs thy subs supers); + +datatype combterm = + CombConst of name * typ * typ list | + CombVar of name * typ | + CombApp of combterm * combterm + +fun combtyp_of (CombConst (_, T, _)) = T + | combtyp_of (CombVar (_, T)) = T + | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) + +(*gets the head of a combinator application, along with the list of arguments*) +fun strip_combterm_comb u = + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) + | stripc x = x + in stripc(u,[]) end + +fun atyps_of T = fold_atyps (insert (op =)) T [] + +fun new_skolem_const_name s num_T_args = + [new_skolem_const_prefix, s, string_of_int num_T_args] + |> space_implode Long_Name.separator + +(* Converts a term (with combinators) into a combterm. Also accumulates sort + infomation. *) +fun combterm_from_term thy bs (P $ Q) = + let + val (P', P_atomics_Ts) = combterm_from_term thy bs P + val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q + in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end + | combterm_from_term thy _ (Const (c, T)) = + let + val tvar_list = + (if String.isPrefix old_skolem_const_prefix c then + [] |> Term.add_tvarsT T |> map TVar + else + (c, T) |> Sign.const_typargs thy) + val c' = CombConst (`make_fixed_const c, T, tvar_list) + in (c', atyps_of T) end + | combterm_from_term _ _ (Free (v, T)) = + (CombConst (`make_fixed_var v, T, []), atyps_of T) + | combterm_from_term _ _ (Var (v as (s, _), T)) = + (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then + let + val Ts = T |> strip_type |> swap |> op :: + val s' = new_skolem_const_name s (length Ts) + in CombConst (`make_fixed_const s', T, Ts) end + else + CombVar ((make_schematic_var v, s), T), atyps_of T) + | combterm_from_term _ bs (Bound j) = + nth bs j + |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) + | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" + +datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained + +(* (quasi-)underapproximation of the truth *) +fun is_locality_global Local = false + | is_locality_global Assum = false + | is_locality_global Chained = false + | is_locality_global _ = true + +datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic +datatype type_level = + All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types +datatype type_heaviness = Heavy | Light + +datatype type_system = + Simple_Types of type_level | + Preds of polymorphism * type_level * type_heaviness | + Tags of polymorphism * type_level * type_heaviness + +fun try_unsuffixes ss s = + fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE + +fun type_sys_from_string s = + (case try (unprefix "poly_") s of + SOME s => (SOME Polymorphic, s) + | NONE => + case try (unprefix "mono_") s of + SOME s => (SOME Monomorphic, s) + | NONE => + case try (unprefix "mangled_") s of + SOME s => (SOME Mangled_Monomorphic, s) + | NONE => (NONE, s)) + ||> (fn s => + (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *) + case try_unsuffixes ["?", "_query"] s of + SOME s => (Nonmonotonic_Types, s) + | NONE => + case try_unsuffixes ["!", "_bang"] s of + SOME s => (Finite_Types, s) + | NONE => (All_Types, s)) + ||> apsnd (fn s => + case try (unsuffix "_heavy") s of + SOME s => (Heavy, s) + | NONE => (Light, s)) + |> (fn (poly, (level, (heaviness, core))) => + case (core, (poly, level, heaviness)) of + ("simple", (NONE, _, Light)) => Simple_Types level + | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) + | ("tags", (SOME Polymorphic, All_Types, _)) => + Tags (Polymorphic, All_Types, heaviness) + | ("tags", (SOME Polymorphic, _, _)) => + (* The actual light encoding is very unsound. *) + Tags (Polymorphic, level, Heavy) + | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) + | ("args", (SOME poly, All_Types (* naja *), Light)) => + Preds (poly, Const_Arg_Types, Light) + | ("erased", (NONE, All_Types (* naja *), Light)) => + Preds (Polymorphic, No_Types, Light) + | _ => raise Same.SAME) + handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") + +fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic + | polymorphism_of_type_sys (Preds (poly, _, _)) = poly + | polymorphism_of_type_sys (Tags (poly, _, _)) = poly + +fun level_of_type_sys (Simple_Types level) = level + | level_of_type_sys (Preds (_, level, _)) = level + | level_of_type_sys (Tags (_, level, _)) = level + +fun heaviness_of_type_sys (Simple_Types _) = Heavy + | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness + | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness + +fun is_type_level_virtually_sound level = + level = All_Types orelse level = Nonmonotonic_Types +val is_type_sys_virtually_sound = + is_type_level_virtually_sound o level_of_type_sys + +fun is_type_level_fairly_sound level = + is_type_level_virtually_sound level orelse level = Finite_Types +val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys + +fun is_setting_higher_order THF (Simple_Types _) = true + | is_setting_higher_order _ _ = false + +type translated_formula = + {name: string, + locality: locality, + kind: formula_kind, + combformula: (name, typ, combterm) formula, + atomic_types: typ list} + +fun update_combformula f ({name, locality, kind, combformula, atomic_types} + : translated_formula) = + {name = name, locality = locality, kind = kind, combformula = f combformula, + atomic_types = atomic_types} : translated_formula + +fun fact_lift f ({combformula, ...} : translated_formula) = f combformula + +val type_instance = Sign.typ_instance o Proof_Context.theory_of + +fun insert_type ctxt get_T x xs = + let val T = get_T x in + if exists (curry (type_instance ctxt) T o get_T) xs then xs + else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs + end + +(* The Booleans indicate whether all type arguments should be kept. *) +datatype type_arg_policy = + Explicit_Type_Args of bool | + Mangled_Type_Args of bool | + No_Type_Args + +fun should_drop_arg_type_args (Simple_Types _) = + false (* since TFF doesn't support overloading *) + | should_drop_arg_type_args type_sys = + level_of_type_sys type_sys = All_Types andalso + heaviness_of_type_sys type_sys = Heavy + +fun general_type_arg_policy type_sys = + if level_of_type_sys type_sys = No_Types then + No_Type_Args + else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then + Mangled_Type_Args (should_drop_arg_type_args type_sys) + else + Explicit_Type_Args (should_drop_arg_type_args type_sys) + +fun type_arg_policy type_sys s = + if s = @{const_name HOL.eq} orelse + (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then + No_Type_Args + else + general_type_arg_policy type_sys + +(*Make literals for sorted type variables*) +fun sorts_on_typs_aux (_, []) = [] + | sorts_on_typs_aux ((x,i), s::ss) = + let val sorts = sorts_on_typs_aux ((x,i), ss) + in + if s = the_single @{sort HOL.type} then sorts + else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts + else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts + end; + +fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s) + | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s) + | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\"" + +(*Given a list of sorted type variables, return a list of type literals.*) +val raw_type_literals_for_types = union_all o map sorts_on_typs + +fun type_literals_for_types format type_sys kind Ts = + if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then + [] + else + Ts |> raw_type_literals_for_types + |> filter (fn TyLitVar _ => kind <> Conjecture + | TyLitFree _ => kind = Conjecture) + +fun mk_aconns c phis = + let val (phis', phi') = split_last phis in + fold_rev (mk_aconn c) phis' phi' + end +fun mk_ahorn [] phi = phi + | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) +fun mk_aquant _ [] phi = phi + | mk_aquant q xs (phi as AQuant (q', xs', phi')) = + if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) + | mk_aquant q xs phi = AQuant (q, xs, phi) + +fun close_universally atom_vars phi = + let + fun formula_vars bounds (AQuant (_, xs, phi)) = + formula_vars (map fst xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (AAtom tm) = + union (op =) (atom_vars tm [] + |> filter_out (member (op =) bounds o fst)) + in mk_aquant AForall (formula_vars [] phi []) phi end + +fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] + | combterm_vars (CombConst _) = I + | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) +fun close_combformula_universally phi = close_universally combterm_vars phi + +fun term_vars (ATerm (name as (s, _), tms)) = + is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms +fun close_formula_universally phi = close_universally term_vars phi + +val homo_infinite_type_name = @{type_name ind} (* any infinite type *) +val homo_infinite_type = Type (homo_infinite_type_name, []) + +fun fo_term_from_typ higher_order = + let + fun term (Type (s, Ts)) = + ATerm (case (higher_order, s) of + (true, @{type_name bool}) => `I tptp_bool_type + | (true, @{type_name fun}) => `I tptp_fun_type + | _ => if s = homo_infinite_type_name then `I tptp_individual_type + else `make_fixed_type_const s, + map term Ts) + | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) + | term (TVar ((x as (s, _)), _)) = + ATerm ((make_schematic_type_var x, s), []) + in term end + +(* This shouldn't clash with anything else. *) +val mangled_type_sep = "\000" + +fun generic_mangled_type_name f (ATerm (name, [])) = f name + | generic_mangled_type_name f (ATerm (name, tys)) = + f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) + ^ ")" + +val bool_atype = AType (`I tptp_bool_type) + +fun make_simple_type s = + if s = tptp_bool_type orelse s = tptp_fun_type orelse + s = tptp_individual_type then + s + else + simple_type_prefix ^ ascii_of s + +fun ho_type_from_fo_term higher_order pred_sym ary = + let + fun to_atype ty = + AType ((make_simple_type (generic_mangled_type_name fst ty), + generic_mangled_type_name snd ty)) + fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) + fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty + | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys + fun to_ho (ty as ATerm ((s, _), tys)) = + if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty + in if higher_order then to_ho else to_fo ary end + +fun mangled_type higher_order pred_sym ary = + ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order + +fun mangled_const_name T_args (s, s') = + let + val ty_args = map (fo_term_from_typ false) T_args + fun type_suffix f g = + fold_rev (curry (op ^) o g o prefix mangled_type_sep + o generic_mangled_type_name f) ty_args "" + in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end + +val parse_mangled_ident = + Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode + +fun parse_mangled_type x = + (parse_mangled_ident + -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") + [] >> ATerm) x +and parse_mangled_types x = + (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x + +fun unmangled_type s = + s |> suffix ")" |> raw_explode + |> Scan.finite Symbol.stopper + (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ + quote s)) parse_mangled_type)) + |> fst + +val unmangled_const_name = space_explode mangled_type_sep #> hd +fun unmangled_const s = + let val ss = space_explode mangled_type_sep s in + (hd ss, map unmangled_type (tl ss)) + end + +fun introduce_proxies format type_sys = + let + fun intro top_level (CombApp (tm1, tm2)) = + CombApp (intro top_level tm1, intro false tm2) + | intro top_level (CombConst (name as (s, _), T, T_args)) = + (case proxify_const s of + SOME (_, proxy_base) => + if top_level orelse is_setting_higher_order format type_sys then + case (top_level, s) of + (_, "c_False") => (`I tptp_false, []) + | (_, "c_True") => (`I tptp_true, []) + | (false, "c_Not") => (`I tptp_not, []) + | (false, "c_conj") => (`I tptp_and, []) + | (false, "c_disj") => (`I tptp_or, []) + | (false, "c_implies") => (`I tptp_implies, []) + | (false, s) => + if is_tptp_equal s then (`I tptp_equal, []) + else (proxy_base |>> prefix const_prefix, T_args) + | _ => (name, []) + else + (proxy_base |>> prefix const_prefix, T_args) + | NONE => (name, T_args)) + |> (fn (name, T_args) => CombConst (name, T, T_args)) + | intro _ tm = tm + in intro true end + +fun combformula_from_prop thy format type_sys eq_as_iff = + let + fun do_term bs t atomic_types = + combterm_from_term thy bs (Envir.eta_contract t) + |>> (introduce_proxies format type_sys #> AAtom) + ||> union (op =) atomic_types + fun do_quant bs q s T t' = + let val s = Name.variant (map fst bs) s in + do_formula ((s, T) :: bs) t' + #>> mk_aquant q [(`make_bound_var s, SOME T)] + end + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> uncurry (mk_aconn c) + and do_formula bs t = + case t of + @{const Not} $ t1 => do_formula bs t1 #>> mk_anot + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t + | _ => do_term bs t + in do_formula [] end + +fun presimplify_term ctxt = + Skip_Proof.make_thm (Proof_Context.theory_of ctxt) + #> Meson.presimplify ctxt + #> prop_of + +fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j +fun conceal_bounds Ts t = + subst_bounds (map (Free o apfst concealed_bound_name) + (0 upto length Ts - 1 ~~ Ts), t) +fun reveal_bounds Ts = + subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) + (0 upto length Ts - 1 ~~ Ts)) + +fun extensionalize_term ctxt t = + let val thy = Proof_Context.theory_of ctxt in + t |> cterm_of thy |> Meson.extensionalize_conv ctxt + |> prop_of |> Logic.dest_equals |> snd + end + +fun introduce_combinators_in_term ctxt kind t = + let val thy = Proof_Context.theory_of ctxt in + if Meson.is_fol_term thy t then + t + else + let + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name All}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) + | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + t |> conceal_bounds Ts + |> Envir.eta_contract + |> cterm_of thy + |> Meson_Clausify.introduce_combinators_in_cterm + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + if kind = Conjecture then HOLogic.false_const + else HOLogic.true_const + end + +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the + same in Sledgehammer to prevent the discovery of unreplayable proofs. *) +fun freeze_term t = + let + fun aux (t $ u) = aux t $ aux u + | aux (Abs (s, T, t)) = Abs (s, T, aux t) + | aux (Var ((s, i), T)) = + Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) + | aux t = t + in t |> exists_subterm is_Var t ? aux end + +(* making fact and conjecture formulas *) +fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t = + let + val thy = Proof_Context.theory_of ctxt + val t = t |> Envir.beta_eta_contract + |> transform_elim_prop + |> Object_Logic.atomize_term thy + val need_trueprop = (fastype_of t = @{typ bool}) + val t = t |> need_trueprop ? HOLogic.mk_Trueprop + |> Raw_Simplifier.rewrite_term thy + (Meson.unfold_set_const_simps ctxt) [] + |> extensionalize_term ctxt + |> presimp ? presimplify_term ctxt + |> perhaps (try (HOLogic.dest_Trueprop)) + |> introduce_combinators_in_term ctxt kind + |> kind <> Axiom ? freeze_term + val (combformula, atomic_types) = + combformula_from_prop thy format type_sys eq_as_iff t [] + in + {name = name, locality = loc, kind = kind, combformula = combformula, + atomic_types = atomic_types} + end + +fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp + ((name, loc), t) = + case (keep_trivial, + make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of + (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => + if s = tptp_true then NONE else SOME formula + | (_, formula) => SOME formula + +fun make_conjecture ctxt format prem_kind type_sys ts = + let val last = length ts - 1 in + map2 (fn j => fn t => + let + val (kind, maybe_negate) = + if j = last then + (Conjecture, I) + else + (prem_kind, + if prem_kind = Conjecture then update_combformula mk_anot + else I) + in + t |> make_formula ctxt format type_sys true true + (string_of_int j) General kind + |> maybe_negate + end) + (0 upto last) ts + end + +(** Finite and infinite type inference **) + +fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S) + | deep_freeze_atyp T = T +val deep_freeze_type = map_atyps deep_freeze_atyp + +(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are + dangerous because their "exhaust" properties can easily lead to unsound ATP + proofs. On the other hand, all HOL infinite types can be given the same + models in first-order logic (via Löwenheim-Skolem). *) + +fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = + exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts + | should_encode_type _ _ All_Types _ = true + | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T + | should_encode_type _ _ _ _ = false + +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) + should_predicate_on_var T = + (heaviness = Heavy orelse should_predicate_on_var ()) andalso + should_encode_type ctxt nonmono_Ts level T + | should_predicate_on_type _ _ _ _ _ = false + +fun is_var_or_bound_var (CombConst ((s, _), _, _)) = + String.isPrefix bound_var_prefix s + | is_var_or_bound_var (CombVar _) = true + | is_var_or_bound_var _ = false + +datatype tag_site = Top_Level | Eq_Arg | Elsewhere + +fun should_tag_with_type _ _ _ Top_Level _ _ = false + | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T = + (case heaviness of + Heavy => should_encode_type ctxt nonmono_Ts level T + | Light => + case (site, is_var_or_bound_var u) of + (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T + | _ => false) + | should_tag_with_type _ _ _ _ _ _ = false + +fun homogenized_type ctxt nonmono_Ts level = + let + val should_encode = should_encode_type ctxt nonmono_Ts level + fun homo 0 T = if should_encode T then T else homo_infinite_type + | homo ary (Type (@{type_name fun}, [T1, T2])) = + homo 0 T1 --> homo (ary - 1) T2 + | homo _ _ = raise Fail "expected function type" + in homo end + +(** "hBOOL" and "hAPP" **) + +type sym_info = + {pred_sym : bool, min_ary : int, max_ary : int, types : typ list} + +fun add_combterm_syms_to_table ctxt explicit_apply = + let + fun consider_var_arity const_T var_T max_ary = + let + fun iter ary T = + if ary = max_ary orelse type_instance ctxt (var_T, T) then ary + else iter (ary + 1) (range_type T) + in iter 0 const_T end + fun add top_level tm (accum as (ho_var_Ts, sym_tab)) = + let val (head, args) = strip_combterm_comb tm in + (case head of + CombConst ((s, _), T, _) => + if String.isPrefix bound_var_prefix s then + if explicit_apply = NONE andalso can dest_funT T then + let + fun repair_min_arity {pred_sym, min_ary, max_ary, types} = + {pred_sym = pred_sym, + min_ary = + fold (fn T' => consider_var_arity T' T) types min_ary, + max_ary = max_ary, types = types} + val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T + in + if pointer_eq (ho_var_Ts', ho_var_Ts) then accum + else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab) + end + else + accum + else + let + val ary = length args + in + (ho_var_Ts, + case Symtab.lookup sym_tab s of + SOME {pred_sym, min_ary, max_ary, types} => + let + val types' = types |> insert_type ctxt I T + val min_ary = + if is_some explicit_apply orelse + pointer_eq (types', types) then + min_ary + else + fold (consider_var_arity T) ho_var_Ts min_ary + in + Symtab.update (s, {pred_sym = pred_sym andalso top_level, + min_ary = Int.min (ary, min_ary), + max_ary = Int.max (ary, max_ary), + types = types'}) + sym_tab + end + | NONE => + let + val min_ary = + case explicit_apply of + SOME true => 0 + | SOME false => ary + | NONE => fold (consider_var_arity T) ho_var_Ts ary + in + Symtab.update_new (s, {pred_sym = top_level, + min_ary = min_ary, max_ary = ary, + types = [T]}) + sym_tab + end) + end + | _ => accum) + |> fold (add false) args + end + in add true end +fun add_fact_syms_to_table ctxt explicit_apply = + fact_lift (formula_fold NONE + (K (add_combterm_syms_to_table ctxt explicit_apply))) + +val default_sym_table_entries : (string * sym_info) list = + [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), + (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), + (make_fixed_const predicator_name, + {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @ + ([tptp_false, tptp_true] + |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) + +fun sym_table_for_facts ctxt explicit_apply facts = + Symtab.empty + |> fold Symtab.default default_sym_table_entries + |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd + +fun min_arity_of sym_tab s = + case Symtab.lookup sym_tab s of + SOME ({min_ary, ...} : sym_info) => min_ary + | NONE => + case strip_prefix_and_unascii const_prefix s of + SOME s => + let val s = s |> unmangled_const_name |> invert_const in + if s = predicator_name then 1 + else if s = app_op_name then 2 + else if s = type_pred_name then 1 + else 0 + end + | NONE => 0 + +(* True if the constant ever appears outside of the top-level position in + literals, or if it appears with different arities (e.g., because of different + type instantiations). If false, the constant always receives all of its + arguments and is used as a predicate. *) +fun is_pred_sym sym_tab s = + case Symtab.lookup sym_tab s of + SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => + pred_sym andalso min_ary = max_ary + | NONE => false + +val predicator_combconst = + CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) +fun predicator tm = CombApp (predicator_combconst, tm) + +fun introduce_predicators_in_combterm sym_tab tm = + case strip_combterm_comb tm of + (CombConst ((s, _), _, _), _) => + if is_pred_sym sym_tab s then tm else predicator tm + | _ => predicator tm + +fun list_app head args = fold (curry (CombApp o swap)) args head + +fun explicit_app arg head = + let + val head_T = combtyp_of head + val (arg_T, res_T) = dest_funT head_T + val explicit_app = + CombConst (`make_fixed_const app_op_name, head_T --> head_T, + [arg_T, res_T]) + in list_app explicit_app [head, arg] end +fun list_explicit_app head args = fold explicit_app args head + +fun introduce_explicit_apps_in_combterm sym_tab = + let + fun aux tm = + case strip_combterm_comb tm of + (head as CombConst ((s, _), _, _), args) => + args |> map aux + |> chop (min_arity_of sym_tab s) + |>> list_app head + |-> list_explicit_app + | (head, args) => list_explicit_app head (map aux args) + in aux end + +fun chop_fun 0 T = ([], T) + | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = + chop_fun (n - 1) ran_T |>> cons dom_T + | chop_fun _ _ = raise Fail "unexpected non-function" + +fun filter_type_args _ _ _ [] = [] + | filter_type_args thy s arity T_args = + let + (* will throw "TYPE" for pseudo-constants *) + val U = if s = app_op_name then + @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global + else + s |> Sign.the_const_type thy + in + case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of + [] => [] + | res_U_vars => + let val U_args = (s, U) |> Sign.const_typargs thy in + U_args ~~ T_args + |> map_filter (fn (U, T) => + if member (op =) res_U_vars (dest_TVar U) then + SOME T + else + NONE) + end + end + handle TYPE _ => T_args + +fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = + let + val thy = Proof_Context.theory_of ctxt + fun aux arity (CombApp (tm1, tm2)) = + CombApp (aux (arity + 1) tm1, aux 0 tm2) + | aux arity (CombConst (name as (s, _), T, T_args)) = + let + val level = level_of_type_sys type_sys + val (T, T_args) = + (* Aggressively merge most "hAPPs" if the type system is unsound + anyway, by distinguishing overloads only on the homogenized + result type. Don't do it for lightweight type systems, though, + since it leads to too many unsound proofs. *) + if s = const_prefix ^ app_op_name andalso + length T_args = 2 andalso + not (is_type_sys_virtually_sound type_sys) andalso + heaviness_of_type_sys type_sys = Heavy then + T_args |> map (homogenized_type ctxt nonmono_Ts level 0) + |> (fn Ts => let val T = hd Ts --> nth Ts 1 in + (T --> T, tl Ts) + end) + else + (T, T_args) + in + (case strip_prefix_and_unascii const_prefix s of + NONE => (name, T_args) + | SOME s'' => + let + val s'' = invert_const s'' + fun filtered_T_args false = T_args + | filtered_T_args true = filter_type_args thy s'' arity T_args + in + case type_arg_policy type_sys s'' of + Explicit_Type_Args drop_args => + (name, filtered_T_args drop_args) + | Mangled_Type_Args drop_args => + (mangled_const_name (filtered_T_args drop_args) name, []) + | No_Type_Args => (name, []) + end) + |> (fn (name, T_args) => CombConst (name, T, T_args)) + end + | aux _ tm = tm + in aux 0 end + +fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab = + not (is_setting_higher_order format type_sys) + ? (introduce_explicit_apps_in_combterm sym_tab + #> introduce_predicators_in_combterm sym_tab) + #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys +fun repair_fact ctxt format nonmono_Ts type_sys sym_tab = + update_combformula (formula_map + (repair_combterm ctxt format nonmono_Ts type_sys sym_tab)) + +(** Helper facts **) + +(* The Boolean indicates that a fairly sound type encoding is needed. *) +val helper_table = + [("COMBI", (false, @{thms Meson.COMBI_def})), + ("COMBK", (false, @{thms Meson.COMBK_def})), + ("COMBB", (false, @{thms Meson.COMBB_def})), + ("COMBC", (false, @{thms Meson.COMBC_def})), + ("COMBS", (false, @{thms Meson.COMBS_def})), + ("fequal", + (* This is a lie: Higher-order equality doesn't need a sound type encoding. + However, this is done so for backward compatibility: Including the + equality helpers by default in Metis breaks a few existing proofs. *) + (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), + ("fFalse", (true, @{thms True_or_False})), + ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), + ("fTrue", (true, @{thms True_or_False})), + ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), + ("fNot", + (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), + ("fconj", + (false, + @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" + by (unfold fconj_def) fast+})), + ("fdisj", + (false, + @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" + by (unfold fdisj_def) fast+})), + ("fimplies", + (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" + "~ fimplies P Q | ~ P | Q" + by (unfold fimplies_def) fast+})), + ("If", (true, @{thms if_True if_False True_or_False}))] + +fun ti_ti_helper_fact () = + let + fun var s = ATerm (`I s, []) + fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) + in + Formula (helper_prefix ^ "ti_ti", Axiom, + AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")])) + |> close_formula_universally, simp_info, NONE) + end + +fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) = + case strip_prefix_and_unascii const_prefix s of + SOME mangled_s => + let + val thy = Proof_Context.theory_of ctxt + val unmangled_s = mangled_s |> unmangled_const_name + fun dub_and_inst c needs_fairly_sound (th, j) = + ((c ^ "_" ^ string_of_int j ^ + (if needs_fairly_sound then typed_helper_suffix + else untyped_helper_suffix), + General), + let val t = th |> prop_of in + t |> ((case general_type_arg_policy type_sys of + Mangled_Type_Args _ => true + | _ => false) andalso + not (null (Term.hidden_polymorphism t))) + ? (case types of + [T] => specialize_type thy (invert_const unmangled_s, T) + | _ => I) + end) + fun make_facts eq_as_iff = + map_filter (make_fact ctxt format type_sys false eq_as_iff false) + val fairly_sound = is_type_sys_fairly_sound type_sys + in + helper_table + |> maps (fn (metis_s, (needs_fairly_sound, ths)) => + if metis_s <> unmangled_s orelse + (needs_fairly_sound andalso not fairly_sound) then + [] + else + ths ~~ (1 upto length ths) + |> map (dub_and_inst mangled_s needs_fairly_sound) + |> make_facts (not needs_fairly_sound)) + end + | NONE => [] +fun helper_facts_for_sym_table ctxt format type_sys sym_tab = + Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab + [] + +fun translate_atp_fact ctxt format type_sys keep_trivial = + `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of) + +(***************************************************************) +(* Type Classes Present in the Axiom or Conjecture Clauses *) +(***************************************************************) + +fun set_insert (x, s) = Symtab.update (x, ()) s + +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) + +(* Remove this trivial type class (FIXME: similar code elsewhere) *) +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset + +fun tfree_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +fun tvar_classes_of_terms ts = + let val sorts_list = map (map #2 o OldTerm.term_tvars) ts + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; + +(*fold type constructors*) +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) + | fold_type_consts _ _ x = x; + +(*Type constructors used to instantiate overloaded constants are the only ones needed.*) +fun add_type_consts_in_term thy = + let + fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I + | aux (t $ u) = aux t #> aux u + | aux (Const x) = + fold (fold_type_consts set_insert) (Sign.const_typargs thy x) + | aux (Abs (_, _, u)) = aux u + | aux _ = I + in aux end + +fun type_consts_of_terms thy ts = + Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); + + +fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t + rich_facts = + let + val thy = Proof_Context.theory_of ctxt + val fact_ts = map (prop_of o snd o snd) rich_facts + val (facts, fact_names) = + rich_facts + |> map_filter (fn (NONE, _) => NONE + | (SOME fact, (name, _)) => SOME (fact, name)) + |> ListPair.unzip + (* Remove existing facts from the conjecture, as this can dramatically + boost an ATP's performance (for some reason). *) + val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val all_ts = goal_t :: fact_ts + val subs = tfree_classes_of_terms all_ts + val supers = tvar_classes_of_terms all_ts + val tycons = type_consts_of_terms thy all_ts + val conjs = + hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys + val (supers', arity_clauses) = + if level_of_type_sys type_sys = No_Types then ([], []) + else make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) + end + +fun fo_literal_from_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_from_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot + +fun type_pred_combterm ctxt nonmono_Ts type_sys T tm = + CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T]) + |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, + tm) + +fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum + | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = + accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) +fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false + | is_var_nonmonotonic_in_formula pos phi _ name = + formula_fold pos (var_occurs_positively_naked_in_term name) phi false + +fun mk_const_aterm x T_args args = + ATerm (x, map (fo_term_from_typ false) T_args @ args) + +fun tag_with_type ctxt format nonmono_Ts type_sys T tm = + CombConst (`make_fixed_const type_tag_name, T --> T, [T]) + |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys + |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level + |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) +and term_from_combterm ctxt format nonmono_Ts type_sys = + let + fun aux site u = + let + val (head, args) = strip_combterm_comb u + val (x as (s, _), T_args) = + case head of + CombConst (name, _, T_args) => (name, T_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg + else Elsewhere + val t = mk_const_aterm x T_args (map (aux arg_site) args) + val T = combtyp_of u + in + t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then + tag_with_type ctxt format nonmono_Ts type_sys T + else + I) + end + in aux end +and formula_from_combformula ctxt format nonmono_Ts type_sys + should_predicate_on_var = + let + val higher_order = is_setting_higher_order format type_sys + val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level + val do_bound_type = + case type_sys of + Simple_Types level => + homogenized_type ctxt nonmono_Ts level 0 + #> mangled_type higher_order false 0 #> SOME + | _ => K NONE + fun do_out_of_bound_type pos phi universal (name, T) = + if should_predicate_on_type ctxt nonmono_Ts type_sys + (fn () => should_predicate_on_var pos phi universal name) T then + CombVar (name, T) + |> type_pred_combterm ctxt nonmono_Ts type_sys T + |> do_term |> AAtom |> SOME + else + NONE + fun do_formula pos (AQuant (q, xs, phi)) = + let + val phi = phi |> do_formula pos + val universal = Option.map (q = AExists ? not) pos + in + AQuant (q, xs |> map (apsnd (fn NONE => NONE + | SOME T => do_bound_type T)), + (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) + (map_filter + (fn (_, NONE) => NONE + | (s, SOME T) => + do_out_of_bound_type pos phi universal (s, T)) + xs) + phi) + end + | do_formula pos (AConn conn) = aconn_map pos do_formula conn + | do_formula _ (AAtom tm) = AAtom (do_term tm) + in do_formula o SOME end + +fun bound_atomic_types format type_sys Ts = + mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) + (type_literals_for_types format type_sys Axiom Ts)) + +fun formula_for_fact ctxt format nonmono_Ts type_sys + ({combformula, atomic_types, ...} : translated_formula) = + combformula + |> close_combformula_universally + |> formula_from_combformula ctxt format nonmono_Ts type_sys + is_var_nonmonotonic_in_formula true + |> bound_atomic_types format type_sys atomic_types + |> close_formula_universally + +(* Each fact is given a unique fact number to avoid name clashes (e.g., because + of monomorphization). The TPTP explicitly forbids name clashes, and some of + the remote provers might care. *) +fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys + (j, formula as {name, locality, kind, ...}) = + Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then "" + else string_of_int j ^ "_") ^ + ascii_of name, + kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE, + case locality of + Intro => intro_info + | Elim => elim_info + | Simp => simp_info + | _ => NONE) + +fun formula_line_for_class_rel_clause + (ClassRelClause {name, subclass, superclass, ...}) = + let val ty_arg = ATerm (`I "T", []) in + Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))]) + |> close_formula_universally, intro_info, NONE) + end + +fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_from_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun formula_line_for_arity_clause + (ArityClause {name, prem_lits, concl_lits, ...}) = + Formula (arity_clause_prefix ^ ascii_of name, Axiom, + mk_ahorn (map (formula_from_fo_literal o apfst not + o fo_literal_from_arity_literal) prem_lits) + (formula_from_fo_literal + (fo_literal_from_arity_literal concl_lits)) + |> close_formula_universally, intro_info, NONE) + +fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys + ({name, kind, combformula, ...} : translated_formula) = + Formula (conjecture_prefix ^ name, kind, + formula_from_combformula ctxt format nonmono_Ts type_sys + is_var_nonmonotonic_in_formula false + (close_combformula_universally combformula) + |> close_formula_universally, NONE, NONE) + +fun free_type_literals format type_sys + ({atomic_types, ...} : translated_formula) = + atomic_types |> type_literals_for_types format type_sys Conjecture + |> map fo_literal_from_type_literal + +fun formula_line_for_free_type j lit = + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, + formula_from_fo_literal lit, NONE, NONE) +fun formula_lines_for_free_types format type_sys facts = + let + val litss = map (free_type_literals format type_sys) facts + val lits = fold (union (op =)) litss [] + in map2 formula_line_for_free_type (0 upto length lits - 1) lits end + +(** Symbol declarations **) + +fun should_declare_sym type_sys pred_sym s = + is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso + (case type_sys of + Simple_Types _ => true + | Tags (_, _, Light) => true + | _ => not pred_sym) + +fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) = + let + fun add_combterm in_conj tm = + let val (head, args) = strip_combterm_comb tm in + (case head of + CombConst ((s, s'), T, T_args) => + let val pred_sym = is_pred_sym repaired_sym_tab s in + if should_declare_sym type_sys pred_sym s then + Symtab.map_default (s, []) + (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, + in_conj)) + else + I + end + | _ => I) + #> fold (add_combterm in_conj) args + end + fun add_fact in_conj = + fact_lift (formula_fold NONE (K (add_combterm in_conj))) + in + Symtab.empty + |> is_type_sys_fairly_sound type_sys + ? (fold (add_fact true) conjs #> fold (add_fact false) facts) + end + +(* These types witness that the type classes they belong to allow infinite + models and hence that any types with these type classes is monotonic. *) +val known_infinite_types = + [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] + +(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it + out with monotonicity" paper presented at CADE 2011. *) +fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I + | add_combterm_nonmonotonic_types ctxt level _ + (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = + (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso + (case level of + Nonmonotonic_Types => + not (is_type_surely_infinite ctxt known_infinite_types T) + | Finite_Types => is_type_surely_finite ctxt T + | _ => true)) ? insert_type ctxt I (deep_freeze_type T) + | add_combterm_nonmonotonic_types _ _ _ _ = I +fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...} + : translated_formula) = + formula_fold (SOME (kind <> Conjecture)) + (add_combterm_nonmonotonic_types ctxt level) combformula +fun nonmonotonic_types_for_facts ctxt type_sys facts = + let val level = level_of_type_sys type_sys in + if level = Nonmonotonic_Types orelse level = Finite_Types then + [] |> fold (add_fact_nonmonotonic_types ctxt level) facts + (* We must add "bool" in case the helper "True_or_False" is added + later. In addition, several places in the code rely on the list of + nonmonotonic types not being empty. *) + |> insert_type ctxt I @{typ bool} + else + [] + end + +fun decl_line_for_sym ctxt format nonmono_Ts type_sys s + (s', T_args, T, pred_sym, ary, _) = + let + val (higher_order, T_arg_Ts, level) = + case type_sys of + Simple_Types level => (format = THF, [], level) + | _ => (false, replicate (length T_args) homo_infinite_type, No_Types) + in + Decl (sym_decl_prefix ^ s, (s, s'), + (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary)) + |> mangled_type higher_order pred_sym (length T_arg_Ts + ary)) + end + +fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false + +fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys + n s j (s', T_args, T, _, ary, in_conj) = + let + val (kind, maybe_negate) = + if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) + else (Axiom, I) + val (arg_Ts, res_T) = chop_fun ary T + val bound_names = + 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + val bounds = + bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) + val bound_Ts = + arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T + else NONE) + in + Formula (sym_formula_prefix ^ s ^ + (if n > 1 then "_" ^ string_of_int j else ""), kind, + CombConst ((s, s'), T, T_args) + |> fold (curry (CombApp o swap)) bounds + |> type_pred_combterm ctxt nonmono_Ts type_sys res_T + |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) + |> formula_from_combformula ctxt format nonmono_Ts type_sys + (K (K (K (K true)))) true + |> n > 1 ? bound_atomic_types format type_sys (atyps_of T) + |> close_formula_universally + |> maybe_negate, + intro_info, NONE) + end + +fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys + n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = + let + val ident_base = + sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") + val (kind, maybe_negate) = + if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) + else (Axiom, I) + val (arg_Ts, res_T) = chop_fun ary T + val bound_names = + 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + val bounds = bound_names |> map (fn name => ATerm (name, [])) + val cst = mk_const_aterm (s, s') T_args + val atomic_Ts = atyps_of T + fun eq tms = + (if pred_sym then AConn (AIff, map AAtom tms) + else AAtom (ATerm (`I tptp_equal, tms))) + |> bound_atomic_types format type_sys atomic_Ts + |> close_formula_universally + |> maybe_negate + val should_encode = should_encode_type ctxt nonmono_Ts All_Types + val tag_with = tag_with_type ctxt format nonmono_Ts type_sys + val add_formula_for_res = + if should_encode res_T then + cons (Formula (ident_base ^ "_res", kind, + eq [tag_with res_T (cst bounds), cst bounds], + simp_info, NONE)) + else + I + fun add_formula_for_arg k = + let val arg_T = nth arg_Ts k in + if should_encode arg_T then + case chop k bounds of + (bounds1, bound :: bounds2) => + cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, + eq [cst (bounds1 @ tag_with arg_T bound :: bounds2), + cst bounds], + simp_info, NONE)) + | _ => raise Fail "expected nonempty tail" + else + I + end + in + [] |> not pred_sym ? add_formula_for_res + |> fold add_formula_for_arg (ary - 1 downto 0) + end + +fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd + +fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys + (s, decls) = + case type_sys of + Simple_Types _ => + decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s) + | Preds _ => + let + val decls = + case decls of + decl :: (decls' as _ :: _) => + let val T = result_type_of_decl decl in + if forall (curry (type_instance ctxt o swap) T + o result_type_of_decl) decls' then + [decl] + else + decls + end + | _ => decls + val n = length decls + val decls = + decls + |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true) + o result_type_of_decl) + in + (0 upto length decls - 1, decls) + |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind + nonmono_Ts type_sys n s) + end + | Tags (_, _, heaviness) => + (case heaviness of + Heavy => [] + | Light => + let val n = length decls in + (0 upto n - 1 ~~ decls) + |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind + nonmono_Ts type_sys n s) + end) + +fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts + type_sys sym_decl_tab = + sym_decl_tab + |> Symtab.dest + |> sort_wrt fst + |> rpair [] + |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind + nonmono_Ts type_sys) + +fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) = + level = Nonmonotonic_Types orelse level = Finite_Types + | should_add_ti_ti_helper _ = false + +fun offset_of_heading_in_problem _ [] j = j + | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = + if heading = needle then j + else offset_of_heading_in_problem needle problem (j + length lines) + +val implicit_declsN = "Should-be-implicit typings" +val explicit_declsN = "Explicit typings" +val factsN = "Relevant facts" +val class_relsN = "Class relationships" +val aritiesN = "Arities" +val helpersN = "Helper facts" +val conjsN = "Conjectures" +val free_typesN = "Type variables" + +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys + explicit_apply hyp_ts concl_t facts = + let + val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = + translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts + val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply + val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys + val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab + val (conjs, facts) = (conjs, facts) |> pairself (map repair) + val repaired_sym_tab = + conjs @ facts |> sym_table_for_facts ctxt (SOME false) + val helpers = + repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys + |> map repair + val lavish_nonmono_Ts = + if null nonmono_Ts orelse + polymorphism_of_type_sys type_sys <> Polymorphic then + nonmono_Ts + else + [TVar (("'a", 0), HOLogic.typeS)] + val sym_decl_lines = + (conjs, helpers @ facts) + |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab + |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind + lavish_nonmono_Ts type_sys + val helper_lines = + 0 upto length helpers - 1 ~~ helpers + |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts + type_sys) + |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ()) + else I) + (* Reordering these might confuse the proof reconstruction code or the SPASS + FLOTTER hack. *) + val problem = + [(explicit_declsN, sym_decl_lines), + (factsN, + map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys) + (0 upto length facts - 1 ~~ facts)), + (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), + (aritiesN, map formula_line_for_arity_clause arity_clauses), + (helpersN, helper_lines), + (conjsN, + map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys) + conjs), + (free_typesN, + formula_lines_for_free_types format type_sys (facts @ conjs))] + val problem = + problem + |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) + |> (if is_format_typed format then + declare_undeclared_syms_in_atp_problem type_decl_prefix + implicit_declsN + else + I) + val (problem, pool) = + problem |> nice_atp_problem (Config.get ctxt readable_names) + val helpers_offset = offset_of_heading_in_problem helpersN problem 0 + val typed_helpers = + map_filter (fn (j, {name, ...}) => + if String.isSuffix typed_helper_suffix name then SOME j + else NONE) + ((helpers_offset + 1 upto helpers_offset + length helpers) + ~~ helpers) + fun add_sym_arity (s, {min_ary, ...} : sym_info) = + if min_ary > 0 then + case strip_prefix_and_unascii const_prefix s of + SOME s => Symtab.insert (op =) (s, min_ary) + | NONE => I + else + I + in + (problem, + case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + offset_of_heading_in_problem conjsN problem 0, + offset_of_heading_in_problem factsN problem 0, + fact_names |> Vector.fromList, + typed_helpers, + Symtab.empty |> Symtab.fold add_sym_arity sym_tab) + end + +(* FUDGE *) +val conj_weight = 0.0 +val hyp_weight = 0.1 +val fact_min_weight = 0.2 +val fact_max_weight = 1.0 +val type_info_default_weight = 0.8 + +fun add_term_weights weight (ATerm (s, tms)) = + is_tptp_user_symbol s ? Symtab.default (s, weight) + #> fold (add_term_weights weight) tms +fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = + formula_fold NONE (K (add_term_weights weight)) phi + | add_problem_line_weights _ _ = I + +fun add_conjectures_weights [] = I + | add_conjectures_weights conjs = + let val (hyps, conj) = split_last conjs in + add_problem_line_weights conj_weight conj + #> fold (add_problem_line_weights hyp_weight) hyps + end + +fun add_facts_weights facts = + let + val num_facts = length facts + fun weight_of j = + fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j + / Real.fromInt num_facts + in + map weight_of (0 upto num_facts - 1) ~~ facts + |> fold (uncurry add_problem_line_weights) + end + +(* Weights are from 0.0 (most important) to 1.0 (least important). *) +fun atp_problem_weights problem = + let val get = these o AList.lookup (op =) problem in + Symtab.empty + |> add_conjectures_weights (get free_typesN @ get conjsN) + |> add_facts_weights (get factsN) + |> fold (fold (add_problem_line_weights type_info_default_weight) o get) + [explicit_declsN, class_relsN, aritiesN] + |> Symtab.dest + |> sort (prod_ord Real.compare string_ord o pairself swap) + end + +end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/ATP/atp_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue May 31 16:38:36 2011 +0200 @@ -0,0 +1,257 @@ +(* Title: HOL/Tools/ATP/atp_util.ML + Author: Jasmin Blanchette, TU Muenchen + +General-purpose functions used by the ATP module. +*) + +signature ATP_UTIL = +sig + val timestamp : unit -> string + val hashw : word * word -> word + val hashw_string : string * word -> word + val strip_spaces : bool -> (char -> bool) -> string -> string + val nat_subscript : int -> string + val unyxml : string -> string + val maybe_quote : string -> string + val string_from_ext_time : bool * Time.time -> string + val string_from_time : Time.time -> string + val varify_type : Proof.context -> typ -> typ + val instantiate_type : theory -> typ -> typ -> typ -> typ + val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ + val typ_of_dtyp : + Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp + -> typ + val is_type_surely_finite : Proof.context -> typ -> bool + val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool + val monomorphic_term : Type.tyenv -> term -> term + val eta_expand : typ list -> term -> int -> term + val transform_elim_prop : term -> term + val specialize_type : theory -> (string * typ) -> term -> term + val strip_subgoal : + Proof.context -> thm -> int -> (string * typ) list * term list * term +end; + +structure ATP_Util : ATP_UTIL = +struct + +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now + +(* This hash function is recommended in "Compilers: Principles, Techniques, and + Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they + particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) +fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s + +fun strip_c_style_comment _ [] = [] + | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = + strip_spaces_in_list true is_evil cs + | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs +and strip_spaces_in_list _ _ [] = [] + | strip_spaces_in_list true is_evil (#"%" :: cs) = + strip_spaces_in_list true is_evil + (cs |> chop_while (not_equal #"\n") |> snd) + | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) = + strip_c_style_comment is_evil cs + | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1] + | strip_spaces_in_list skip_comments is_evil [c1, c2] = + strip_spaces_in_list skip_comments is_evil [c1] @ + strip_spaces_in_list skip_comments is_evil [c2] + | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) = + if Char.isSpace c1 then + strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) + else if Char.isSpace c2 then + if Char.isSpace c3 then + strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs) + else + str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @ + strip_spaces_in_list skip_comments is_evil (c3 :: cs) + else + str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) +fun strip_spaces skip_comments is_evil = + implode o strip_spaces_in_list skip_comments is_evil o String.explode + +val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) +fun nat_subscript n = + n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript + +val unyxml = XML.content_of o YXML.parse_body + +val is_long_identifier = forall Lexicon.is_identifier o space_explode "." +fun maybe_quote y = + let val s = unyxml y in + y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso + not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse + Keyword.is_keyword s) ? quote + end + +fun string_from_ext_time (plus, time) = + let val ms = Time.toMilliseconds time in + (if plus then "> " else "") ^ + (if plus andalso ms mod 1000 = 0 then + signed_string_of_int (ms div 1000) ^ " s" + else if ms < 1000 then + signed_string_of_int ms ^ " ms" + else + string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s") + end + +val string_from_time = string_from_ext_time o pair false + +fun varify_type ctxt T = + Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] + |> snd |> the_single |> dest_Const |> snd + +(* TODO: use "Term_Subst.instantiateT" instead? *) +fun instantiate_type thy T1 T1' T2 = + Same.commit (Envir.subst_type_same + (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 + handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) + +fun varify_and_instantiate_type ctxt T1 T1' T2 = + let val thy = Proof_Context.theory_of ctxt in + instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) + end + +fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) = + the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a)) + | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) = + Type (s, map (typ_of_dtyp descr typ_assoc) Us) + | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = + let val (s, ds, _) = the (AList.lookup (op =) descr i) in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end + +fun datatype_constrs thy (T as Type (s, Ts)) = + (case Datatype.get_info thy s of + SOME {index, descr, ...} => + let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in + map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) + constrs + end + | NONE => []) + | datatype_constrs _ _ = [] + +(* Similar to "Nitpick_HOL.bounded_exact_card_of_type". + 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means + cardinality 2 or more. The specified default cardinality is returned if the + cardinality of the type can't be determined. *) +fun tiny_card_of_type ctxt default_card assigns T = + let + val thy = Proof_Context.theory_of ctxt + val max = 2 (* 1 would be too small for the "fun" case *) + fun aux slack avoid T = + if member (op =) avoid T then + 0 + else case AList.lookup (Sign.typ_instance thy o swap) assigns T of + SOME k => k + | NONE => + case T of + Type (@{type_name fun}, [T1, T2]) => + (case (aux slack avoid T1, aux slack avoid T2) of + (k, 1) => if slack andalso k = 0 then 0 else 1 + | (0, _) => 0 + | (_, 0) => 0 + | (k1, k2) => + if k1 >= max orelse k2 >= max then max + else Int.min (max, Integer.pow k2 k1)) + | @{typ prop} => 2 + | @{typ bool} => 2 (* optimization *) + | @{typ nat} => 0 (* optimization *) + | Type ("Int.int", []) => 0 (* optimization *) + | Type (s, _) => + (case datatype_constrs thy T of + constrs as _ :: _ => + let + val constr_cards = + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types + o snd) constrs + in + if exists (curry (op =) 0) constr_cards then 0 + else Int.min (max, Integer.sum constr_cards) + end + | [] => + case Typedef.get_info ctxt s of + ({abs_type, rep_type, ...}, _) :: _ => + (* We cheat here by assuming that typedef types are infinite if + their underlying type is infinite. This is unsound in general + but it's hard to think of a realistic example where this would + not be the case. We are also slack with representation types: + If a representation type has the form "sigma => tau", we + consider it enough to check "sigma" for infiniteness. (Look + for "slack" in this function.) *) + (case varify_and_instantiate_type ctxt + (Logic.varifyT_global abs_type) T + (Logic.varifyT_global rep_type) + |> aux true avoid of + 0 => 0 + | 1 => 1 + | _ => default_card) + | [] => default_card) + (* Very slightly unsound: Type variables are assumed not to be + constrained to cardinality 1. (In practice, the user would most + likely have used "unit" directly anyway.) *) + | TFree _ => if default_card = 1 then 2 else default_card + (* Schematic type variables that contain only unproblematic sorts + (with no finiteness axiom) can safely be considered infinite. *) + | TVar _ => default_card + in Int.min (max, aux false [] T) end + +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0 +fun is_type_surely_infinite ctxt infinite_Ts T = + tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0 + +fun monomorphic_term subst t = + map_types (map_type_tvar (fn v => + case Type.lookup subst v of + SOME typ => typ + | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ + \variable", [t]))) t + +fun eta_expand _ t 0 = t + | eta_expand Ts (Abs (s, T, t')) n = + Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) + | eta_expand Ts t n = + fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t')) + (List.take (binder_types (fastype_of1 (Ts, t)), n)) + (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_theorem" in + "Meson_Clausify".) *) +fun transform_elim_prop t = + case Logic.strip_imp_concl t of + @{const Trueprop} $ Var (z, @{typ bool}) => + subst_Vars [(z, @{const False})] t + | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t + | _ => t + +fun specialize_type thy (s, T) t = + let + fun subst_for (Const (s', T')) = + if s = s' then + SOME (Sign.typ_match thy (T', T) Vartab.empty) + handle Type.TYPE_MATCH => NONE + else + NONE + | subst_for (t1 $ t2) = + (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2) + | subst_for (Abs (_, _, t')) = subst_for t' + | subst_for _ = NONE + in + case subst_for t of + SOME subst => monomorphic_term subst t + | NONE => raise Type.TYPE_MATCH + end + +fun strip_subgoal ctxt goal i = + let + val (t, (frees, params)) = + Logic.goal_params (prop_of goal) i + ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) + val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) + val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees + in (rev params, hyp_ts, concl_t) end + +end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 @@ -30,6 +30,7 @@ structure Metis_Reconstruct : METIS_RECONSTRUCT = struct +open ATP_Translate open Metis_Translate exception METIS of string * string diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 @@ -26,6 +26,7 @@ structure Metis_Tactics : METIS_TACTICS = struct +open ATP_Translate open Metis_Translate open Metis_Reconstruct diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -9,76 +9,21 @@ signature METIS_TRANSLATE = sig - type name = string * string - - datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - datatype arity_literal = - TConsLit of name * name * name list | - TVarLit of name * name - datatype arity_clause = - ArityClause of - {name: string, - prem_lits: arity_literal list, - concl_lits: arity_literal} - datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - datatype combterm = - CombConst of name * typ * typ list | - CombVar of name * typ | - CombApp of combterm * combterm - datatype fol_literal = FOLLiteral of bool * combterm + type type_literal = ATP_Translate.type_literal datatype mode = FO | HO | FT + type metis_problem = {axioms: (Metis_Thm.thm * thm) list, tfrees: type_literal list, old_skolems: (string * term) list} val metis_generated_var_prefix : string - val type_tag_name : string - val bound_var_prefix : string - val schematic_var_prefix: string - val fixed_var_prefix: string - val tvar_prefix: string - val tfree_prefix: string - val const_prefix: string - val type_const_prefix: string - val class_prefix: string val new_skolem_const_prefix : string - val proxify_const : string -> (int * (string * string)) option - val invert_const: string -> string - val unproxify_const: string -> string - val ascii_of: string -> string - val unascii_of: string -> string - val strip_prefix_and_unascii: string -> string -> string option - val make_bound_var : string -> string - val make_schematic_var : string * int -> string - val make_fixed_var : string -> string - val make_schematic_type_var : string * int -> string - val make_fixed_type_var : string -> string - val make_fixed_const : string -> string - val make_fixed_type_const : string -> string - val make_type_class : string -> string val num_type_args: theory -> string -> int val new_skolem_var_name_from_const : string -> string - val type_literals_for_types : typ list -> type_literal list - val make_class_rel_clauses : - theory -> class list -> class list -> class_rel_clause list - val make_arity_clauses : - theory -> string list -> class list -> class list * arity_clause list - val combtyp_of : combterm -> typ - val strip_combterm_comb : combterm -> combterm * combterm list - val atyps_of : typ -> typ list - val combterm_from_term : - theory -> (string * typ) list -> term -> combterm * typ list val reveal_old_skolem_terms : (string * term) list -> term -> term - val tfree_classes_of_terms : term list -> string list - val tvar_classes_of_terms : term list -> string list - val type_consts_of_terms : theory -> term list -> string list val string_of_mode : mode -> string - val metis_helpers : (string * (bool * thm list)) list val prepare_metis_problem : mode -> Proof.context -> bool -> thm list -> thm list list -> mode * metis_problem @@ -87,150 +32,9 @@ structure Metis_Translate : METIS_TRANSLATE = struct -val metis_generated_var_prefix = "_" - -val type_tag_name = "ti" - -val bound_var_prefix = "B_" -val schematic_var_prefix = "V_" -val fixed_var_prefix = "v_" - -val tvar_prefix = "T_"; -val tfree_prefix = "t_"; - -val const_prefix = "c_"; -val type_const_prefix = "tc_"; -val class_prefix = "class_"; - -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" -val old_skolem_const_prefix = skolem_const_prefix ^ "o" -val new_skolem_const_prefix = skolem_const_prefix ^ "n" - -fun union_all xss = fold (union (op =)) xss [] - -val metis_proxies = - [("c_False", - (@{const_name False}, (0, ("fFalse", @{const_name Metis.fFalse})))), - ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name Metis.fTrue})))), - ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name Metis.fNot})))), - ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name Metis.fconj})))), - ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name Metis.fdisj})))), - ("c_implies", - (@{const_name implies}, (2, ("fimplies", @{const_name Metis.fimplies})))), - ("equal", - (@{const_name HOL.eq}, (2, ("fequal", @{const_name Metis.fequal}))))] - -val proxify_const = AList.lookup (op =) metis_proxies #> Option.map snd - -(* Readable names for the more common symbolic functions. Do not mess with the - table unless you know what you are doing. *) -val const_trans_table = - [(@{type_name Product_Type.prod}, "prod"), - (@{type_name Sum_Type.sum}, "sum"), - (@{const_name False}, "False"), - (@{const_name True}, "True"), - (@{const_name Not}, "Not"), - (@{const_name conj}, "conj"), - (@{const_name disj}, "disj"), - (@{const_name implies}, "implies"), - (@{const_name HOL.eq}, "equal"), - (@{const_name If}, "If"), - (@{const_name Set.member}, "member"), - (@{const_name Meson.COMBI}, "COMBI"), - (@{const_name Meson.COMBK}, "COMBK"), - (@{const_name Meson.COMBB}, "COMBB"), - (@{const_name Meson.COMBC}, "COMBC"), - (@{const_name Meson.COMBS}, "COMBS")] - |> Symtab.make - |> fold (Symtab.update o swap o snd o snd o snd) metis_proxies - -(* Invert the table of translations between Isabelle and Metis. *) -val const_trans_table_inv = - const_trans_table |> Symtab.dest |> map swap |> Symtab.make -val const_trans_table_unprox = - Symtab.empty - |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) - metis_proxies - -val invert_const = perhaps (Symtab.lookup const_trans_table_inv) -val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox) +open ATP_Translate -(*Escaping of special characters. - Alphanumeric characters are left unchanged. - The character _ goes to __ - Characters in the range ASCII space to / go to _A to _P, respectively. - Other characters go to _nnn where nnn is the decimal ASCII code.*) -val A_minus_space = Char.ord #"A" - Char.ord #" "; - -fun stringN_of_int 0 _ = "" - | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ string_of_int (n mod 10); - -fun ascii_of_c c = - if Char.isAlphaNum c then String.str c - else if c = #"_" then "__" - else if #" " <= c andalso c <= #"/" - then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) - else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) - -val ascii_of = String.translate ascii_of_c; - -(** Remove ASCII armouring from names in proof files **) - -(*We don't raise error exceptions because this code can run inside the watcher. - Also, the errors are "impossible" (hah!)*) -fun unascii_aux rcs [] = String.implode(rev rcs) - | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) - (*Three types of _ escapes: __, _A to _P, _nnn*) - | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs - | unascii_aux rcs (#"_" :: c :: cs) = - if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) - then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs - else - let val digits = List.take (c::cs, 3) handle Subscript => [] - in - case Int.fromString (String.implode digits) of - NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) - | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) - end - | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs -val unascii_of = unascii_aux [] o String.explode - -(* If string s has the prefix s1, return the result of deleting it, - un-ASCII'd. *) -fun strip_prefix_and_unascii s1 s = - if String.isPrefix s1 s then - SOME (unascii_of (String.extract (s, size s1, NONE))) - else - NONE - -(*Remove the initial ' character from a type variable, if it is present*) -fun trim_type_var s = - if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) - else raise Fail ("trim_type: Malformed type variable encountered: " ^ s) - -fun ascii_of_indexname (v,0) = ascii_of v - | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; - -fun make_bound_var x = bound_var_prefix ^ ascii_of x -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x - -fun make_schematic_type_var (x,i) = - tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); - -fun lookup_const c = - case Symtab.lookup const_trans_table c of - SOME c' => c' - | NONE => ascii_of c - -(* HOL.eq MUST BE "equal" because it's built into ATPs. *) -fun make_fixed_const @{const_name HOL.eq} = "equal" - | make_fixed_const c = const_prefix ^ lookup_const c - -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c - -fun make_type_class clas = class_prefix ^ ascii_of clas; +val metis_generated_var_prefix = "_" (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem pseudoconstants, this information is encoded in the @@ -246,192 +50,6 @@ nth ss (length ss - 2) end - -(**** Definitions and functions for FOL clauses for TPTP format output ****) - -type name = string * string - -(**** Isabelle FOL clauses ****) - -(* The first component is the type class; the second is a TVar or TFree. *) -datatype type_literal = - TyLitVar of name * name | - TyLitFree of name * name - -(*Make literals for sorted type variables*) -fun sorts_on_typs_aux (_, []) = [] - | sorts_on_typs_aux ((x,i), s::ss) = - let val sorts = sorts_on_typs_aux ((x,i), ss) - in - if s = the_single @{sort HOL.type} then sorts - else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts - else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts - end; - -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) - | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); - -(*Given a list of sorted type variables, return a list of type literals.*) -fun type_literals_for_types Ts = - fold (union (op =)) (map sorts_on_typs Ts) [] - -(** make axiom and conjecture clauses. **) - -(**** Isabelle arities ****) - -datatype arity_literal = - TConsLit of name * name * name list | - TVarLit of name * name - -datatype arity_clause = - ArityClause of - {name: string, - prem_lits: arity_literal list, - concl_lits: arity_literal} - -fun gen_TVars 0 = [] - | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1); - -fun pack_sort(_,[]) = [] - | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) - | pack_sort(tvar, cls::srt) = - (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt) - -(*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause (tcons, name, (cls,args)) = - let - val tvars = gen_TVars (length args) - val tvars_srts = ListPair.zip (tvars, args) - in - ArityClause {name = name, - prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)), - concl_lits = TConsLit (`make_type_class cls, - `make_fixed_type_const tcons, - tvars ~~ tvars)} - end - - -(**** Isabelle class relations ****) - -datatype class_rel_clause = - ClassRelClause of {name: string, subclass: name, superclass: name} - -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) -fun class_pairs _ [] _ = [] - | class_pairs thy subs supers = - let - val class_less = Sorts.class_less (Sign.classes_of thy) - fun add_super sub super = class_less (sub, super) ? cons (sub, super) - fun add_supers sub = fold (add_super sub) supers - in fold add_supers subs [] end - -fun make_class_rel_clause (sub,super) = - ClassRelClause {name = sub ^ "_" ^ super, - subclass = `make_type_class sub, - superclass = `make_type_class super} - -fun make_class_rel_clauses thy subs supers = - map make_class_rel_clause (class_pairs thy subs supers); - - -(** Isabelle arities **) - -fun arity_clause _ _ (_, []) = [] - | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) - arity_clause seen n (tcons,ars) - | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = - if member (op =) seen class then (*multiple arities for the same tycon, class pair*) - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) :: - arity_clause seen (n+1) (tcons,ars) - else - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: - arity_clause (class::seen) n (tcons,ars) - -fun multi_arity_clause [] = [] - | multi_arity_clause ((tcons, ars) :: tc_arlists) = - arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists - -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy - provided its arguments have the corresponding sorts.*) -fun type_class_pairs thy tycons classes = - let val alg = Sign.classes_of thy - fun domain_sorts tycon = Sorts.mg_domain alg tycon o single - fun add_class tycon class = - cons (class, domain_sorts tycon class) - handle Sorts.CLASS_ERROR _ => I - fun try_classes tycon = (tycon, fold (add_class tycon) classes []) - in map try_classes tycons end; - -(*Proving one (tycon, class) membership may require proving others, so iterate.*) -fun iter_type_class_pairs _ _ [] = ([], []) - | iter_type_class_pairs thy tycons classes = - let val cpairs = type_class_pairs thy tycons classes - val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) - |> subtract (op =) classes |> subtract (op =) HOLogic.typeS - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; - -fun make_arity_clauses thy tycons = - iter_type_class_pairs thy tycons ##> multi_arity_clause - -datatype combterm = - CombConst of name * typ * typ list (* Const and Free *) | - CombVar of name * typ | - CombApp of combterm * combterm - -datatype fol_literal = FOLLiteral of bool * combterm - -(*********************************************************************) -(* convert a clause with type Term.term to a clause with type clause *) -(*********************************************************************) - -fun combtyp_of (CombConst (_, T, _)) = T - | combtyp_of (CombVar (_, T)) = T - | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) - -(*gets the head of a combinator application, along with the list of arguments*) -fun strip_combterm_comb u = - let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) - | stripc x = x - in stripc(u,[]) end - -fun atyps_of T = fold_atyps (insert (op =)) T [] - -fun new_skolem_const_name s num_T_args = - [new_skolem_const_prefix, s, string_of_int num_T_args] - |> space_implode Long_Name.separator - -(* Converts a term (with combinators) into a combterm. Also accumulates sort - infomation. *) -fun combterm_from_term thy bs (P $ Q) = - let - val (P', P_atomics_Ts) = combterm_from_term thy bs P - val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q - in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end - | combterm_from_term thy _ (Const (c, T)) = - let - val tvar_list = - (if String.isPrefix old_skolem_const_prefix c then - [] |> Term.add_tvarsT T |> map TVar - else - (c, T) |> Sign.const_typargs thy) - val c' = CombConst (`make_fixed_const c, T, tvar_list) - in (c', atyps_of T) end - | combterm_from_term _ _ (Free (v, T)) = - (CombConst (`make_fixed_var v, T, []), atyps_of T) - | combterm_from_term _ _ (Var (v as (s, _), T)) = - (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then - let - val Ts = T |> strip_type |> swap |> op :: - val s' = new_skolem_const_name s (length Ts) - in CombConst (`make_fixed_const s', T, Ts) end - else - CombVar ((make_schematic_var v, s), T), atyps_of T) - | combterm_from_term _ bs (Bound j) = - nth bs j - |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) - | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" - fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) | predicate_of thy (t, pos) = (combterm_from_term thy [] (Envir.eta_contract t), pos) @@ -442,7 +60,7 @@ literals_of_term1 (literals_of_term1 args thy P) thy Q | literals_of_term1 (lits, ts) thy P = let val ((pred, ts'), pol) = predicate_of thy (P, true) in - (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') + ((pol, pred) :: lits, union (op =) ts ts') end val literals_of_term = literals_of_term1 ([], []) @@ -491,43 +109,6 @@ | t => t) -(***************************************************************) -(* Type Classes Present in the Axiom or Conjecture Clauses *) -(***************************************************************) - -fun set_insert (x, s) = Symtab.update (x, ()) s - -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) - -(*Remove this trivial type class*) -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; - -fun tfree_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -fun tvar_classes_of_terms ts = - let val sorts_list = map (map #2 o OldTerm.term_tvars) ts - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; - -(*fold type constructors*) -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) - | fold_type_consts _ _ x = x; - -(*Type constructors used to instantiate overloaded constants are the only ones needed.*) -fun add_type_consts_in_term thy = - let - fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I - | aux (t $ u) = aux t #> aux u - | aux (Const x) = - fold (fold_type_consts set_insert) (Sign.const_typargs thy x) - | aux (Abs (_, _, u)) = aux u - | aux _ = I - in aux end - -fun type_consts_of_terms thy ts = - Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); - (* ------------------------------------------------------------------------- *) (* HOL to FOL (Isabelle to Metis) *) (* ------------------------------------------------------------------------- *) @@ -589,18 +170,18 @@ tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2])) (combtyp_of tm) -fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = +fun hol_literal_to_fol FO (pos, tm) = let val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm val tylits = if p = "equal" then [] else map metis_term_from_typ Ts val lits = map hol_term_to_fol_FO tms in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end - | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = + | hol_literal_to_fol HO (pos, tm) = (case strip_combterm_comb tm of (CombConst(("equal", _), _, _), tms) => metis_lit pos "=" (map hol_term_to_fol_HO tms) | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) - | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = + | hol_literal_to_fol FT (pos, tm) = (case strip_combterm_comb tm of (CombConst(("equal", _), _, _), tms) => metis_lit pos "=" (map hol_term_to_fol_FT tms) @@ -634,11 +215,11 @@ in if is_conjecture then (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), - type_literals_for_types types_sorts, old_skolems) + raw_type_literals_for_types types_sorts, old_skolems) else let val tylits = types_sorts |> filter_out (has_default_sort ctxt) - |> type_literals_for_types + |> raw_type_literals_for_types val mtylits = if type_lits then map (metis_of_type_literals false) tylits else [] in @@ -647,40 +228,6 @@ end end; -(* The Boolean indicates that a fairly sound type encoding is needed. *) -val metis_helpers = - [("COMBI", (false, @{thms Meson.COMBI_def})), - ("COMBK", (false, @{thms Meson.COMBK_def})), - ("COMBB", (false, @{thms Meson.COMBB_def})), - ("COMBC", (false, @{thms Meson.COMBC_def})), - ("COMBS", (false, @{thms Meson.COMBS_def})), - ("fequal", - (* This is a lie: Higher-order equality doesn't need a sound type encoding. - However, this is done so for backward compatibility: Including the - equality helpers by default in Metis breaks a few existing proofs. *) - (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] - fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), - ("fFalse", (true, @{thms True_or_False})), - ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), - ("fTrue", (true, @{thms True_or_False})), - ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), - ("fNot", - (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] - fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), - ("fconj", - (false, - @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" - by (unfold fconj_def) fast+})), - ("fdisj", - (false, - @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" - by (unfold fdisj_def) fast+})), - ("fimplies", - (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" - "~ fimplies P Q | ~ P | Q" - by (unfold fimplies_def) fast+})), - ("If", (true, @{thms if_True if_False True_or_False}))] - (* ------------------------------------------------------------------------- *) (* Logic maps manage the interface between HOL and first-order logic. *) (* ------------------------------------------------------------------------- *) @@ -697,7 +244,7 @@ fun init_tfrees ctxt = let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] - |> type_literals_for_types + |> raw_type_literals_for_types end; (*Insert non-logical axioms corresponding to all accumulated TFrees*) @@ -785,7 +332,7 @@ #> `(Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq fdefs)) val helper_ths = - metis_helpers + helper_table |> filter (is_used o prefix const_prefix o fst) |> maps (fn (_, (needs_full_types, thms)) => if needs_full_types andalso mode <> FT then [] diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue May 31 16:38:36 2011 +0200 @@ -860,7 +860,7 @@ out "solve "; out_outmost_f formula; out ";\n") in out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ - "// " ^ ATP_Problem.timestamp () ^ "\n"); + "// " ^ ATP_Util.timestamp () ^ "\n"); map out_problem problems end diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 31 16:38:36 2011 +0200 @@ -969,7 +969,7 @@ handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) -(* Similar to "Sledgehammer_ATP_Translate.tiny_card_of_type". *) +(* Similar to "ATP_Translate.tiny_card_of_type". *) fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card assigns T = let diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue May 31 16:38:36 2011 +0200 @@ -240,7 +240,7 @@ val parse_bool_option = Sledgehammer_Util.parse_bool_option val parse_time_option = Sledgehammer_Util.parse_time_option -val string_from_time = Sledgehammer_Util.string_from_time +val string_from_time = ATP_Util.string_from_time val i_subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" @@ -265,15 +265,15 @@ val simple_string_of_typ = Refute.string_of_typ val is_real_constr = Refute.is_IDT_constructor -val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp -val varify_type = Sledgehammer_Util.varify_type -val instantiate_type = Sledgehammer_Util.instantiate_type -val varify_and_instantiate_type = Sledgehammer_Util.varify_and_instantiate_type +val typ_of_dtyp = ATP_Util.typ_of_dtyp +val varify_type = ATP_Util.varify_type +val instantiate_type = ATP_Util.instantiate_type +val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type val is_of_class_const = Refute.is_const_of_class val get_class_def = Refute.get_classdef -val monomorphic_term = Sledgehammer_Util.monomorphic_term -val specialize_type = Sledgehammer_Util.specialize_type -val eta_expand = Sledgehammer_Util.eta_expand +val monomorphic_term = ATP_Util.monomorphic_term +val specialize_type = ATP_Util.specialize_type +val eta_expand = ATP_Util.eta_expand fun time_limit NONE = I | time_limit (SOME delay) = TimeLimit.timeLimit delay @@ -290,15 +290,15 @@ val pstrs = Pretty.breaks o map Pretty.str o space_explode " " -val unyxml = Sledgehammer_Util.unyxml +val unyxml = ATP_Util.unyxml -val maybe_quote = Sledgehammer_Util.maybe_quote +val maybe_quote = ATP_Util.maybe_quote fun pretty_maybe_quote pretty = let val s = Pretty.str_of pretty in if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty] end -val hashw = ATP_Problem.hashw -val hashw_string = ATP_Problem.hashw_string +val hashw = ATP_Util.hashw +val hashw_string = ATP_Util.hashw_string end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Nitpick/nitrox.ML --- a/src/HOL/Tools/Nitpick/nitrox.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Tue May 31 16:38:36 2011 +0200 @@ -13,6 +13,7 @@ structure Nitrox : NITROX = struct +open ATP_Util open ATP_Problem open ATP_Proof open Nitpick diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 31 11:21:47 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1098 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Claire Quigley, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Proof reconstruction for Sledgehammer. -*) - -signature SLEDGEHAMMER_ATP_RECONSTRUCT = -sig - type 'a proof = 'a ATP_Proof.proof - type locality = Sledgehammer_Filter.locality - type type_system = Sledgehammer_ATP_Translate.type_system - - datatype reconstructor = - Metis | - MetisFT | - SMT of string - - datatype play = - Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option| - Failed_to_Play - - type minimize_command = string list -> string - type one_line_params = - play * string * (string * locality) list * minimize_command * int * int - type isar_params = - bool * bool * int * type_system * string Symtab.table * int list list - * int * (string * locality) list vector * int Symtab.table * string proof - * thm - val repair_conjecture_shape_and_fact_names : - type_system -> string -> int list list -> int - -> (string * locality) list vector -> int list - -> int list list * int * (string * locality) list vector * int list - val used_facts_in_atp_proof : - Proof.context -> type_system -> int -> (string * locality) list vector - -> string proof -> (string * locality) list - val used_facts_in_unsound_atp_proof : - Proof.context -> type_system -> int list list -> int - -> (string * locality) list vector -> 'a proof -> string list option - val uses_typed_helpers : int list -> 'a proof -> bool - val reconstructor_name : reconstructor -> string - val one_line_proof_text : one_line_params -> string - val isar_proof_text : - Proof.context -> bool -> isar_params -> one_line_params -> string - val proof_text : - Proof.context -> bool -> isar_params -> one_line_params -> string -end; - -structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = -struct - -open ATP_Problem -open ATP_Proof -open Metis_Translate -open Sledgehammer_Util -open Sledgehammer_Filter -open Sledgehammer_ATP_Translate - -datatype reconstructor = - Metis | - MetisFT | - SMT of string - -datatype play = - Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option | - Failed_to_Play - -type minimize_command = string list -> string -type one_line_params = - play * string * (string * locality) list * minimize_command * int * int -type isar_params = - bool * bool * int * type_system * string Symtab.table * int list list * int - * (string * locality) list vector * int Symtab.table * string proof * thm - -fun is_head_digit s = Char.isDigit (String.sub (s, 0)) -val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) - -val is_typed_helper_name = - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix - -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - - -(** SPASS's FLOTTER hack **) - -(* This is a hack required for keeping track of facts after they have been - clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is - also part of this hack. *) - -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" - -fun extract_clause_sequence output = - let - val tokens_of = String.tokens (not o Char.isAlphaNum) - fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) - | extract_num _ = NONE - in output |> split_lines |> map_filter (extract_num o tokens_of) end - -val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," - -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" - --| Scan.option ($$ ",") -val parse_clause_formula_relation = - Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" - |-- Scan.repeat parse_clause_formula_pair -val extract_clause_formula_relation = - Substring.full #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.position "." #> fst #> Substring.string - #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation - #> fst - -fun maybe_unprefix_fact_number type_sys = - polymorphism_of_type_sys type_sys <> Polymorphic - ? (space_implode "_" o tl o space_explode "_") - -fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape - fact_offset fact_names typed_helpers = - if String.isSubstring set_ClauseFormulaRelationN output then - let - val j0 = hd (hd conjecture_shape) - val seq = extract_clause_sequence output - val name_map = extract_clause_formula_relation output - fun renumber_conjecture j = - conjecture_prefix ^ string_of_int (j - j0) - |> AList.find (fn (s, ss) => member (op =) ss s) name_map - |> map (fn s => find_index (curry (op =) s) seq + 1) - fun names_for_number j = - j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys - o unprefix fact_prefix)) - |> map (fn name => - (name, name |> find_first_in_list_vector fact_names |> the) - handle Option.Option => - error ("No such fact: " ^ quote name ^ ".")) - in - (conjecture_shape |> map (maps renumber_conjecture), 0, - seq |> map names_for_number |> Vector.fromList, - name_map |> filter (forall is_typed_helper_name o snd) |> map fst) - end - else - (conjecture_shape, fact_offset, fact_names, typed_helpers) - -val vampire_step_prefix = "f" (* grrr... *) - -val extract_step_number = - Int.fromString o perhaps (try (unprefix vampire_step_prefix)) - -fun resolve_fact type_sys _ fact_names (_, SOME s) = - (case try (unprefix fact_prefix) s of - SOME s' => - let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in - case find_first_in_list_vector fact_names s' of - SOME x => [(s', x)] - | NONE => [] - end - | NONE => []) - | resolve_fact _ facts_offset fact_names (num, NONE) = - (case extract_step_number num of - SOME j => - let val j = j - facts_offset in - if j > 0 andalso j <= Vector.length fact_names then - Vector.sub (fact_names, j - 1) - else - [] - end - | NONE => []) - -fun is_fact type_sys conjecture_shape = - not o null o resolve_fact type_sys 0 conjecture_shape - -fun resolve_conjecture _ (_, SOME s) = - (case try (unprefix conjecture_prefix) s of - SOME s' => - (case Int.fromString s' of - SOME j => [j] - | NONE => []) - | NONE => []) - | resolve_conjecture conjecture_shape (num, NONE) = - case extract_step_number num of - SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of - ~1 => [] - | j => [j]) - | NONE => [] - -fun is_conjecture conjecture_shape = - not o null o resolve_conjecture conjecture_shape - -fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s - | is_typed_helper typed_helpers (num, NONE) = - (case extract_step_number num of - SOME i => member (op =) typed_helpers i - | NONE => false) - -val leo2_ext = "extcnf_equal_neg" -val isa_ext = Thm.get_name_hint @{thm ext} -val isa_short_ext = Long_Name.base_name isa_ext - -fun ext_name ctxt = - if Thm.eq_thm_prop (@{thm ext}, - singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then - isa_short_ext - else - isa_ext - -fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) = - union (op =) (resolve_fact type_sys facts_offset fact_names name) - | add_fact ctxt _ _ _ (Inference (_, _, deps)) = - if AList.defined (op =) deps leo2_ext then - insert (op =) (ext_name ctxt, General (* or Chained... *)) - else - I - | add_fact _ _ _ _ _ = I - -fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof = - if null atp_proof then Vector.foldl (op @) [] fact_names - else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof [] - -fun is_conjecture_referred_to_in_proof conjecture_shape = - exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name - | _ => false) - -fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset - fact_names atp_proof = - let - val used_facts = - used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof - in - if forall (is_locality_global o snd) used_facts andalso - not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then - SOME (map fst used_facts) - else - NONE - end - -fun uses_typed_helpers typed_helpers = - exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name - | _ => false) - - -(** Soft-core proof reconstruction: Metis one-liner **) - -fun reconstructor_name Metis = "metis" - | reconstructor_name MetisFT = "metisFT" - | reconstructor_name (SMT _) = "smt" - -fun reconstructor_settings (SMT settings) = settings - | reconstructor_settings _ = "" - -fun string_for_label (s, num) = s ^ string_of_int num - -fun show_time NONE = "" - | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" - -fun set_settings "" = "" - | set_settings settings = "using [[" ^ settings ^ "]] " -fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " - | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " - | apply_on_subgoal settings i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n -fun command_call name [] = name - | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" -fun try_command_line banner time command = - banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "." -fun using_labels [] = "" - | using_labels ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun reconstructor_command reconstructor i n (ls, ss) = - using_labels ls ^ - apply_on_subgoal (reconstructor_settings reconstructor) i n ^ - command_call (reconstructor_name reconstructor) ss -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "." - -val split_used_facts = - List.partition (curry (op =) Chained o snd) - #> pairself (sort_distinct (string_ord o pairself fst)) - -fun one_line_proof_text (preplay, banner, used_facts, minimize_command, - subgoal, subgoal_count) = - let - val (chained, extra) = split_used_facts used_facts - val (reconstructor, ext_time) = - case preplay of - Played (reconstructor, time) => - (SOME reconstructor, (SOME (false, time))) - | Trust_Playable (reconstructor, time) => - (SOME reconstructor, - case time of - NONE => NONE - | SOME time => - if time = Time.zeroTime then NONE else SOME (true, time)) - | Failed_to_Play => (NONE, NONE) - val try_line = - case reconstructor of - SOME r => ([], map fst extra) - |> reconstructor_command r subgoal subgoal_count - |> try_command_line banner ext_time - | NONE => "One-line proof reconstruction failed." - in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end - -(** Hard-core proof reconstruction: structured Isar proofs **) - -(* Simple simplifications to ensure that sort annotations don't leave a trail of - spurious "True"s. *) -fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) = - Const (@{const_name Ex}, T) $ Abs (s, T', s_not t') - | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = - Const (@{const_name All}, T) $ Abs (s, T', s_not t') - | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2 - | s_not (@{const HOL.conj} $ t1 $ t2) = - @{const HOL.disj} $ s_not t1 $ s_not t2 - | s_not (@{const HOL.disj} $ t1 $ t2) = - @{const HOL.conj} $ s_not t1 $ s_not t2 - | 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 forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t -fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t - -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "X" -val assum_prefix = "A" -val have_prefix = "F" - -fun raw_label_for_name conjecture_shape name = - case resolve_conjecture conjecture_shape name of - [j] => (conjecture_prefix, j) - | _ => case Int.fromString (fst name) of - SOME j => (raw_prefix, j) - | NONE => (raw_prefix ^ fst name, 0) - -(**** INTERPRETATION OF TSTP SYNTAX TREES ****) - -exception FO_TERM of string fo_term list -exception FORMULA of (string, 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 typ_from_fo_term tfrees (u as ATerm (a, us)) = - let val Ts = map (typ_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 tfrees (u as ATerm (a, us)) = - case (strip_prefix_and_unascii class_prefix a, - map (typ_from_fo_term tfrees) us) of - (SOME b, [T]) => (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_tptp_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 sym_tab tfrees = - let - fun aux opt_T extra_us u = - case u of - ATerm (a, us) => - if String.isPrefix simple_type_prefix a then - @{const True} (* ignore TPTP type information *) - else if a = tptp_equal then - let val ts = map (aux NONE []) us in - if length ts = 2 andalso hd ts aconv List.last ts then - (* Vampire is keen on producing these. *) - @{const True} - else - list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) - end - else case strip_prefix_and_unascii const_prefix a of - SOME s => - let - val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const - in - if s' = type_tag_name then - case mangled_us @ us of - [typ_u, term_u] => - aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u - | _ => raise FO_TERM us - else if s' = predicator_name then - aux (SOME @{typ bool}) [] (hd us) - else if s' = app_op_name then - aux opt_T (nth us 1 :: extra_us) (hd us) - else if s' = type_pred_name then - @{const True} (* ignore type predicates *) - else - let - val num_ty_args = - length us - the_default 0 (Symtab.lookup sym_tab s) - val (type_us, term_us) = - chop num_ty_args us |>> append mangled_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 = - if num_type_args thy s' = length type_us then - Sign.const_instance thy - (s', map (typ_from_fo_term tfrees) type_us) - else case opt_T of - SOME T => map fastype_of (term_ts @ extra_ts) ---> T - | NONE => HOLogic.typeT - val s' = s' |> unproxify_const - in list_comb (Const (s', T), term_ts @ extra_ts) end - 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_tptp_variable_name Char.toLower a, 0), T) - else - (* Skolem constants? *) - Var ((repair_tptp_variable_name Char.toUpper a, 0), T) - in list_comb (t, ts) end - in aux (SOME HOLogic.boolT) [] end - -fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) = - if String.isPrefix class_prefix s then - add_type_constraint pos (type_constraint_from_term tfrees u) - #> pair @{const True} - else - pair (raw_term_from_pred thy sym_tab tfrees u) - -val combinator_table = - [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), - (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), - (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), - (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), - (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] - -fun uncombine_term thy = - let - fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) - | aux (Abs (s, T, t')) = Abs (s, T, aux t') - | aux (t as Const (x as (s, _))) = - (case AList.lookup (op =) combinator_table s of - SOME thm => thm |> prop_of |> specialize_type thy x - |> Logic.dest_equals |> snd - | NONE => t) - | aux t = t - in aux end - -(* Update schematic type variables with detected sort constraints. It's not - totally clear whether 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_var quant_of var_s t = - let - val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s) - |> map Var - in fold_rev quant_of vars t end - -(* Interpret an ATP formula as a HOL term, extracting sort constraints as they - appear in the formula. *) -fun prop_from_formula thy sym_tab tfrees phi = - let - fun do_formula pos phi = - case phi of - AQuant (_, [], phi) => do_formula pos phi - | AQuant (q, (s, _) :: xs, phi') => - do_formula pos (AQuant (q, xs, phi')) - (* FIXME: TFF *) - #>> quantify_over_var (case q of - AForall => forall_of - | AExists => exists_of) - (repair_tptp_variable_name Char.toLower s) - | 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 - | _ => raise Fail "unexpected connective") - | AAtom tm => term_from_pred thy sym_tab tfrees pos tm - | _ => raise FORMULA [phi] - in repair_tvar_sorts (do_formula true phi Vartab.empty) end - -fun check_formula ctxt = - Type.constraint HOLogic.boolT - #> Syntax.check_term - (Proof_Context.set_mode Proof_Context.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 sym_tab tfrees (Definition (name, phi1, phi2)) ctxt = - let - val thy = Proof_Context.theory_of ctxt - val t1 = prop_from_formula thy sym_tab 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 sym_tab tfrees phi2 - val (t1, t2) = - HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term thy |> check_formula ctxt - |> HOLogic.dest_eq - in - (Definition (name, t1, t2), - fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) - end - | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt = - let - val thy = Proof_Context.theory_of ctxt - val t = u |> prop_from_formula thy sym_tab tfrees - |> uncombine_term thy |> check_formula ctxt - in - (Inference (name, t, deps), - fold Variable.declare_term (OldTerm.term_frees t) ctxt) - end -fun decode_lines ctxt sym_tab tfrees lines = - fst (fold_map (decode_line sym_tab 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_dependency (old, new) dep = - if is_same_atp_step dep old then new else [dep] -fun replace_dependencies_in_line _ (line as Definition _) = line - | replace_dependencies_in_line p (Inference (name, t, deps)) = - Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) - -(* Discard facts; 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 type_sys conjecture_shape fact_names (Inference (name, t, [])) - lines = - (* No dependencies: fact, conjecture, or (for Vampire) internal facts or - definitions. *) - if is_fact type_sys fact_names name then - (* Facts are not proof lines. *) - if is_only_type_information t then - map (replace_dependencies_in_line (name, [])) 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 (name', _, _) :: post) => - pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" - else if is_conjecture conjecture_shape name then - Inference (name, s_not t, []) :: lines - else - map (replace_dependencies_in_line (name, [])) lines - | add_line _ _ _ (Inference (name, t, deps)) lines = - (* Type information will be deleted later; skip repetition test. *) - if is_only_type_information t then - Inference (name, 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 (name, t, deps) :: lines - | (pre, Inference (name', t', _) :: post) => - Inference (name, t', deps) :: - pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" - -(* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (Inference (name, t, [])) lines = - if is_only_type_information t then delete_dependency name lines - else Inference (name, t, []) :: lines - | add_nontrivial_line line lines = line :: lines -and delete_dependency name lines = - fold_rev add_nontrivial_line - (map (replace_dependencies_in_line (name, [])) 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 - -fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) = - (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names - frees (Inference (name, t, deps)) (j, lines) = - (j + 1, - if is_fact type_sys fact_names name orelse - is_conjecture conjecture_shape name orelse - (* the last line must be kept *) - j = 0 orelse - (not (is_only_type_information t) andalso - null (Term.add_tvars t []) andalso - not (exists_subterm (is_bad_free frees) t) andalso - length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso - (* kill next to last line, which usually results in a trivial step *) - j <> 1) then - Inference (name, t, deps) :: lines (* keep line *) - else - map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) - -(** 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 isar_qualifier = Show | Then | Moreover | Ultimately - -datatype isar_step = - Fix of (string * typ) list | - Let of term * term | - Assume of label * term | - Have of isar_qualifier list * label * term * byline -and byline = - ByMetis of facts | - CaseSplit of isar_step list list * facts - -fun smart_case_split [] facts = ByMetis facts - | smart_case_split proofs facts = CaseSplit (proofs, facts) - -fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names - name = - if is_fact type_sys fact_names name then - apsnd (union (op =) - (map fst (resolve_fact type_sys facts_offset fact_names name))) - else - apfst (insert (op =) (raw_label_for_name conjecture_shape name)) - -fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) - | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) = - Assume (raw_label_for_name conjecture_shape name, t) - | step_for_line type_sys conjecture_shape facts_offset - fact_names j (Inference (name, t, deps)) = - Have (if j = 1 then [Show] else [], - raw_label_for_name conjecture_shape name, - fold_rev forall_of (map Var (Term.add_vars t [])) t, - ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape - facts_offset fact_names) - deps ([], []))) - -fun repair_name "$true" = "c_True" - | repair_name "$false" = "c_False" - | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) - | repair_name s = - if is_tptp_equal s orelse - (* seen in Vampire proofs *) - (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then - tptp_equal - else - s - -fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor - conjecture_shape facts_offset fact_names sym_tab params frees - atp_proof = - let - val lines = - atp_proof - |> clean_up_atp_proof_dependencies - |> nasty_atp_proof pool - |> map_term_names_in_atp_proof repair_name - |> decode_lines ctxt sym_tab tfrees - |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names) - |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) - |-> fold_rev (add_desired_line type_sys isar_shrink_factor - conjecture_shape fact_names frees) - |> snd - in - (if null params then [] else [Fix params]) @ - map2 (step_for_line type_sys conjecture_shape facts_offset fact_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 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. *) - val concl_l = (conjecture_prefix, length hyp_ts) - 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 (_, j), _)) :: proof, contra) = - if l = concl_l then first_pass (proof, contra ||> cons step) - else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j)) - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = - let 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_l], [])) - 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, s_not t) - else - Have (qs, l, s_not t, - ByMetis (backpatch_label patches l))) - | (contra_ls as _ :: _, co_ls) => - let - val proofs = - map_filter - (fn l => - if l = concl_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, s_not 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 have_prefix, next_fact) - in (l', (l, l') :: subst, next_fact + 1) end - val relabel_facts = - apfst (maps (the_list o AList.lookup (op =) subst)) - 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 ctxt0 full_types i n = - let - val ctxt = - ctxt0 |> Config.put show_free_types false - |> Config.put show_types true - |> Config.put show_sorts true - fun fix_print_mode f x = - 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) - val reconstructor = if full_types then MetisFT else Metis - fun do_facts (ls, ss) = - reconstructor_command reconstructor 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 ctxt isar_proof_requested - (debug, full_types, isar_shrink_factor, type_sys, pool, - conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal) - (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = - let - val isar_shrink_factor = - (if isar_proof_requested then 1 else 2) * isar_shrink_factor - val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal - val frees = fold Term.add_frees (concl_t :: hyp_ts) [] - val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] - val one_line_proof = one_line_proof_text one_line_params - fun isar_proof_for () = - case atp_proof - |> isar_proof_from_atp_proof pool ctxt type_sys tfrees - isar_shrink_factor conjecture_shape facts_offset - fact_names sym_tab params frees - |> redirect_proof 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 subgoal subgoal_count of - "" => - if isar_proof_requested then - "\nNo structured proof available (proof too short)." - else - "" - | proof => - "\n\n" ^ (if isar_proof_requested then "Structured proof" - else "Perhaps this will work") ^ - ":\n" ^ Markup.markup Markup.sendback proof - val isar_proof = - if debug then - isar_proof_for () - else - case try isar_proof_for () of - SOME s => s - | NONE => if isar_proof_requested then - "\nWarning: The Isar proof construction failed." - else - "" - in one_line_proof ^ isar_proof end - -fun proof_text ctxt isar_proof isar_params - (one_line_params as (preplay, _, _, _, _, _)) = - (if isar_proof orelse preplay = Failed_to_Play then - isar_proof_text ctxt isar_proof isar_params - else - one_line_proof_text) one_line_params - -end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 31 11:21:47 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1389 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Translation of HOL to FOL for Sledgehammer. -*) - -signature SLEDGEHAMMER_ATP_TRANSLATE = -sig - type 'a fo_term = 'a ATP_Problem.fo_term - type format = ATP_Problem.format - type formula_kind = ATP_Problem.formula_kind - type 'a problem = 'a ATP_Problem.problem - type locality = Sledgehammer_Filter.locality - - datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic - datatype type_level = - All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types - datatype type_heaviness = Heavy | Light - - datatype type_system = - Simple_Types of type_level | - Preds of polymorphism * type_level * type_heaviness | - Tags of polymorphism * type_level * type_heaviness - - type translated_formula - - val readable_names : bool Config.T - val fact_prefix : string - val conjecture_prefix : string - val helper_prefix : string - val typed_helper_suffix : string - val predicator_name : string - val app_op_name : string - val type_pred_name : string - val simple_type_prefix : string - val type_sys_from_string : string -> type_system - val polymorphism_of_type_sys : type_system -> polymorphism - val level_of_type_sys : type_system -> type_level - val is_type_sys_virtually_sound : type_system -> bool - val is_type_sys_fairly_sound : type_system -> bool - val unmangled_const : string -> string * string fo_term list - val translate_atp_fact : - Proof.context -> format -> type_system -> bool -> (string * locality) * thm - -> translated_formula option * ((string * locality) * thm) - val prepare_atp_problem : - Proof.context -> format -> formula_kind -> formula_kind -> type_system - -> bool option -> term list -> term - -> (translated_formula option * ((string * 'a) * thm)) list - -> string problem * string Symtab.table * int * int - * (string * 'a) list vector * int list * int Symtab.table - val atp_problem_weights : string problem -> (string * real) list -end; - -structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = -struct - -open ATP_Problem -open Metis_Translate -open Sledgehammer_Util -open Sledgehammer_Filter - -(* experimental *) -val generate_useful_info = false - -fun useful_isabelle_info s = - if generate_useful_info then - SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) - else - NONE - -val intro_info = useful_isabelle_info "intro" -val elim_info = useful_isabelle_info "elim" -val simp_info = useful_isabelle_info "simp" - -(* Readable names are often much shorter, especially if types are mangled in - names. Also, the logic for generating legal SNARK sort names is only - implemented for readable names. Finally, readable names are, well, more - readable. For these reason, they are enabled by default. *) -val readable_names = - Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) - -val type_decl_prefix = "ty_" -val sym_decl_prefix = "sy_" -val sym_formula_prefix = "sym_" -val fact_prefix = "fact_" -val conjecture_prefix = "conj_" -val helper_prefix = "help_" -val class_rel_clause_prefix = "crel_"; -val arity_clause_prefix = "arity_" -val tfree_prefix = "tfree_" - -val typed_helper_suffix = "_T" -val untyped_helper_suffix = "_U" - -val predicator_name = "hBOOL" -val app_op_name = "hAPP" -val type_pred_name = "is" -val simple_type_prefix = "ty_" - -fun make_simple_type s = - if s = tptp_bool_type orelse s = tptp_fun_type orelse - s = tptp_individual_type then - s - else - simple_type_prefix ^ ascii_of s - -(* Freshness almost guaranteed! *) -val sledgehammer_weak_prefix = "Sledgehammer:" - -datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic -datatype type_level = - All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types -datatype type_heaviness = Heavy | Light - -datatype type_system = - Simple_Types of type_level | - Preds of polymorphism * type_level * type_heaviness | - Tags of polymorphism * type_level * type_heaviness - -fun try_unsuffixes ss s = - fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE - -fun type_sys_from_string s = - (case try (unprefix "poly_") s of - SOME s => (SOME Polymorphic, s) - | NONE => - case try (unprefix "mono_") s of - SOME s => (SOME Monomorphic, s) - | NONE => - case try (unprefix "mangled_") s of - SOME s => (SOME Mangled_Monomorphic, s) - | NONE => (NONE, s)) - ||> (fn s => - (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *) - case try_unsuffixes ["?", "_query"] s of - SOME s => (Nonmonotonic_Types, s) - | NONE => - case try_unsuffixes ["!", "_bang"] s of - SOME s => (Finite_Types, s) - | NONE => (All_Types, s)) - ||> apsnd (fn s => - case try (unsuffix "_heavy") s of - SOME s => (Heavy, s) - | NONE => (Light, s)) - |> (fn (poly, (level, (heaviness, core))) => - case (core, (poly, level, heaviness)) of - ("simple", (NONE, _, Light)) => Simple_Types level - | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) - | ("tags", (SOME Polymorphic, All_Types, _)) => - Tags (Polymorphic, All_Types, heaviness) - | ("tags", (SOME Polymorphic, _, _)) => - (* The actual light encoding is very unsound. *) - Tags (Polymorphic, level, Heavy) - | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) - | ("args", (SOME poly, All_Types (* naja *), Light)) => - Preds (poly, Const_Arg_Types, Light) - | ("erased", (NONE, All_Types (* naja *), Light)) => - Preds (Polymorphic, No_Types, Light) - | _ => raise Same.SAME) - handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") - -fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic - | polymorphism_of_type_sys (Preds (poly, _, _)) = poly - | polymorphism_of_type_sys (Tags (poly, _, _)) = poly - -fun level_of_type_sys (Simple_Types level) = level - | level_of_type_sys (Preds (_, level, _)) = level - | level_of_type_sys (Tags (_, level, _)) = level - -fun heaviness_of_type_sys (Simple_Types _) = Heavy - | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness - | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness - -fun is_type_level_virtually_sound level = - level = All_Types orelse level = Nonmonotonic_Types -val is_type_sys_virtually_sound = - is_type_level_virtually_sound o level_of_type_sys - -fun is_type_level_fairly_sound level = - is_type_level_virtually_sound level orelse level = Finite_Types -val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys - -fun is_setting_higher_order THF (Simple_Types _) = true - | is_setting_higher_order _ _ = false - -type translated_formula = - {name: string, - locality: locality, - kind: formula_kind, - combformula: (name, typ, combterm) formula, - atomic_types: typ list} - -fun update_combformula f ({name, locality, kind, combformula, atomic_types} - : translated_formula) = - {name = name, locality = locality, kind = kind, combformula = f combformula, - atomic_types = atomic_types} : translated_formula - -fun fact_lift f ({combformula, ...} : translated_formula) = f combformula - -val type_instance = Sign.typ_instance o Proof_Context.theory_of - -fun insert_type ctxt get_T x xs = - let val T = get_T x in - if exists (curry (type_instance ctxt) T o get_T) xs then xs - else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs - end - -(* The Booleans indicate whether all type arguments should be kept. *) -datatype type_arg_policy = - Explicit_Type_Args of bool | - Mangled_Type_Args of bool | - No_Type_Args - -fun should_drop_arg_type_args (Simple_Types _) = - false (* since TFF doesn't support overloading *) - | should_drop_arg_type_args type_sys = - level_of_type_sys type_sys = All_Types andalso - heaviness_of_type_sys type_sys = Heavy - -fun general_type_arg_policy type_sys = - if level_of_type_sys type_sys = No_Types then - No_Type_Args - else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then - Mangled_Type_Args (should_drop_arg_type_args type_sys) - else - Explicit_Type_Args (should_drop_arg_type_args type_sys) - -fun type_arg_policy type_sys s = - if s = @{const_name HOL.eq} orelse - (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then - No_Type_Args - else - general_type_arg_policy type_sys - -fun atp_type_literals_for_types format type_sys kind Ts = - if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then - [] - else - Ts |> type_literals_for_types - |> filter (fn TyLitVar _ => kind <> Conjecture - | TyLitFree _ => kind = Conjecture) - -fun mk_aconns c phis = - let val (phis', phi') = split_last phis in - fold_rev (mk_aconn c) phis' phi' - end -fun mk_ahorn [] phi = phi - | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) -fun mk_aquant _ [] phi = phi - | mk_aquant q xs (phi as AQuant (q', xs', phi')) = - if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) - | mk_aquant q xs phi = AQuant (q, xs, phi) - -fun close_universally atom_vars phi = - let - fun formula_vars bounds (AQuant (_, xs, phi)) = - formula_vars (map fst xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (AAtom tm) = - union (op =) (atom_vars tm [] - |> filter_out (member (op =) bounds o fst)) - in mk_aquant AForall (formula_vars [] phi []) phi end - -fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] - | combterm_vars (CombConst _) = I - | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) -fun close_combformula_universally phi = close_universally combterm_vars phi - -fun term_vars (ATerm (name as (s, _), tms)) = - is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms -fun close_formula_universally phi = close_universally term_vars phi - -val homo_infinite_type_name = @{type_name ind} (* any infinite type *) -val homo_infinite_type = Type (homo_infinite_type_name, []) - -fun fo_term_from_typ higher_order = - let - fun term (Type (s, Ts)) = - ATerm (case (higher_order, s) of - (true, @{type_name bool}) => `I tptp_bool_type - | (true, @{type_name fun}) => `I tptp_fun_type - | _ => if s = homo_infinite_type_name then `I tptp_individual_type - else `make_fixed_type_const s, - map term Ts) - | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) - | term (TVar ((x as (s, _)), _)) = - ATerm ((make_schematic_type_var x, s), []) - in term end - -(* This shouldn't clash with anything else. *) -val mangled_type_sep = "\000" - -fun generic_mangled_type_name f (ATerm (name, [])) = f name - | generic_mangled_type_name f (ATerm (name, tys)) = - f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) - ^ ")" - -val bool_atype = AType (`I tptp_bool_type) - -fun ho_type_from_fo_term higher_order pred_sym ary = - let - fun to_atype ty = - AType ((make_simple_type (generic_mangled_type_name fst ty), - generic_mangled_type_name snd ty)) - fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) - fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty - | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys - fun to_ho (ty as ATerm ((s, _), tys)) = - if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty - in if higher_order then to_ho else to_fo ary end - -fun mangled_type higher_order pred_sym ary = - ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order - -fun mangled_const_name T_args (s, s') = - let - val ty_args = map (fo_term_from_typ false) T_args - fun type_suffix f g = - fold_rev (curry (op ^) o g o prefix mangled_type_sep - o generic_mangled_type_name f) ty_args "" - in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end - -val parse_mangled_ident = - Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode - -fun parse_mangled_type x = - (parse_mangled_ident - -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") - [] >> ATerm) x -and parse_mangled_types x = - (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x - -fun unmangled_type s = - s |> suffix ")" |> raw_explode - |> Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ - quote s)) parse_mangled_type)) - |> fst - -val unmangled_const_name = space_explode mangled_type_sep #> hd -fun unmangled_const s = - let val ss = space_explode mangled_type_sep s in - (hd ss, map unmangled_type (tl ss)) - end - -fun introduce_proxies format type_sys = - let - fun intro top_level (CombApp (tm1, tm2)) = - CombApp (intro top_level tm1, intro false tm2) - | intro top_level (CombConst (name as (s, _), T, T_args)) = - (case proxify_const s of - SOME (_, proxy_base) => - if top_level orelse is_setting_higher_order format type_sys then - case (top_level, s) of - (_, "c_False") => (`I tptp_false, []) - | (_, "c_True") => (`I tptp_true, []) - | (false, "c_Not") => (`I tptp_not, []) - | (false, "c_conj") => (`I tptp_and, []) - | (false, "c_disj") => (`I tptp_or, []) - | (false, "c_implies") => (`I tptp_implies, []) - | (false, s) => - if is_tptp_equal s then (`I tptp_equal, []) - else (proxy_base |>> prefix const_prefix, T_args) - | _ => (name, []) - else - (proxy_base |>> prefix const_prefix, T_args) - | NONE => (name, T_args)) - |> (fn (name, T_args) => CombConst (name, T, T_args)) - | intro _ tm = tm - in intro true end - -fun combformula_from_prop thy format type_sys eq_as_iff = - let - fun do_term bs t atomic_types = - combterm_from_term thy bs (Envir.eta_contract t) - |>> (introduce_proxies format type_sys #> AAtom) - ||> union (op =) atomic_types - fun do_quant bs q s T t' = - let val s = Name.variant (map fst bs) s in - do_formula ((s, T) :: bs) t' - #>> mk_aquant q [(`make_bound_var s, SOME T)] - end - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 - #>> uncurry (mk_aconn c) - and do_formula bs t = - case t of - @{const Not} $ t1 => do_formula bs t1 #>> mk_anot - | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' - | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 - | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t - | _ => do_term bs t - in do_formula [] end - -fun presimplify_term ctxt = - Skip_Proof.make_thm (Proof_Context.theory_of ctxt) - #> Meson.presimplify ctxt - #> prop_of - -fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j -fun conceal_bounds Ts t = - subst_bounds (map (Free o apfst concealed_bound_name) - (0 upto length Ts - 1 ~~ Ts), t) -fun reveal_bounds Ts = - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) - (0 upto length Ts - 1 ~~ Ts)) - -fun extensionalize_term ctxt t = - let val thy = Proof_Context.theory_of ctxt in - t |> cterm_of thy |> Meson.extensionalize_conv ctxt - |> prop_of |> Logic.dest_equals |> snd - end - -fun introduce_combinators_in_term ctxt kind t = - let val thy = Proof_Context.theory_of ctxt in - if Meson.is_fol_term thy t then - t - else - let - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name All}, _)) $ t1 => - aux Ts (t0 $ eta_expand Ts t1 1) - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ t1 => - aux Ts (t0 $ eta_expand Ts t1 1) - | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - t |> conceal_bounds Ts - |> Envir.eta_contract - |> cterm_of thy - |> Meson_Clausify.introduce_combinators_in_cterm - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single - in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - if kind = Conjecture then HOLogic.false_const - else HOLogic.true_const - end - -(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the - same in Sledgehammer to prevent the discovery of unreplayable proofs. *) -fun freeze_term t = - let - fun aux (t $ u) = aux t $ aux u - | aux (Abs (s, T, t)) = Abs (s, T, aux t) - | aux (Var ((s, i), T)) = - Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) - | aux t = t - in t |> exists_subterm is_Var t ? aux end - -(* making fact and conjecture formulas *) -fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t = - let - val thy = Proof_Context.theory_of ctxt - val t = t |> Envir.beta_eta_contract - |> transform_elim_prop - |> Object_Logic.atomize_term thy - val need_trueprop = (fastype_of t = @{typ bool}) - val t = t |> need_trueprop ? HOLogic.mk_Trueprop - |> Raw_Simplifier.rewrite_term thy - (Meson.unfold_set_const_simps ctxt) [] - |> extensionalize_term ctxt - |> presimp ? presimplify_term ctxt - |> perhaps (try (HOLogic.dest_Trueprop)) - |> introduce_combinators_in_term ctxt kind - |> kind <> Axiom ? freeze_term - val (combformula, atomic_types) = - combformula_from_prop thy format type_sys eq_as_iff t [] - in - {name = name, locality = loc, kind = kind, combformula = combformula, - atomic_types = atomic_types} - end - -fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp - ((name, loc), t) = - case (keep_trivial, - make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of - (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => - if s = tptp_true then NONE else SOME formula - | (_, formula) => SOME formula - -fun make_conjecture ctxt format prem_kind type_sys ts = - let val last = length ts - 1 in - map2 (fn j => fn t => - let - val (kind, maybe_negate) = - if j = last then - (Conjecture, I) - else - (prem_kind, - if prem_kind = Conjecture then update_combformula mk_anot - else I) - in - t |> make_formula ctxt format type_sys true true - (string_of_int j) General kind - |> maybe_negate - end) - (0 upto last) ts - end - -(** Finite and infinite type inference **) - -fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S) - | deep_freeze_atyp T = T -val deep_freeze_type = map_atyps deep_freeze_atyp - -(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are - dangerous because their "exhaust" properties can easily lead to unsound ATP - proofs. On the other hand, all HOL infinite types can be given the same - models in first-order logic (via Löwenheim-Skolem). *) - -fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = - exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts - | should_encode_type _ _ All_Types _ = true - | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T - | should_encode_type _ _ _ _ = false - -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) - should_predicate_on_var T = - (heaviness = Heavy orelse should_predicate_on_var ()) andalso - should_encode_type ctxt nonmono_Ts level T - | should_predicate_on_type _ _ _ _ _ = false - -fun is_var_or_bound_var (CombConst ((s, _), _, _)) = - String.isPrefix bound_var_prefix s - | is_var_or_bound_var (CombVar _) = true - | is_var_or_bound_var _ = false - -datatype tag_site = Top_Level | Eq_Arg | Elsewhere - -fun should_tag_with_type _ _ _ Top_Level _ _ = false - | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T = - (case heaviness of - Heavy => should_encode_type ctxt nonmono_Ts level T - | Light => - case (site, is_var_or_bound_var u) of - (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T - | _ => false) - | should_tag_with_type _ _ _ _ _ _ = false - -fun homogenized_type ctxt nonmono_Ts level = - let - val should_encode = should_encode_type ctxt nonmono_Ts level - fun homo 0 T = if should_encode T then T else homo_infinite_type - | homo ary (Type (@{type_name fun}, [T1, T2])) = - homo 0 T1 --> homo (ary - 1) T2 - | homo _ _ = raise Fail "expected function type" - in homo end - -(** "hBOOL" and "hAPP" **) - -type sym_info = - {pred_sym : bool, min_ary : int, max_ary : int, types : typ list} - -fun add_combterm_syms_to_table ctxt explicit_apply = - let - fun consider_var_arity const_T var_T max_ary = - let - fun iter ary T = - if ary = max_ary orelse type_instance ctxt (var_T, T) then ary - else iter (ary + 1) (range_type T) - in iter 0 const_T end - fun add top_level tm (accum as (ho_var_Ts, sym_tab)) = - let val (head, args) = strip_combterm_comb tm in - (case head of - CombConst ((s, _), T, _) => - if String.isPrefix bound_var_prefix s then - if explicit_apply = NONE andalso can dest_funT T then - let - fun repair_min_arity {pred_sym, min_ary, max_ary, types} = - {pred_sym = pred_sym, - min_ary = - fold (fn T' => consider_var_arity T' T) types min_ary, - max_ary = max_ary, types = types} - val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T - in - if pointer_eq (ho_var_Ts', ho_var_Ts) then accum - else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab) - end - else - accum - else - let - val ary = length args - in - (ho_var_Ts, - case Symtab.lookup sym_tab s of - SOME {pred_sym, min_ary, max_ary, types} => - let - val types' = types |> insert_type ctxt I T - val min_ary = - if is_some explicit_apply orelse - pointer_eq (types', types) then - min_ary - else - fold (consider_var_arity T) ho_var_Ts min_ary - in - Symtab.update (s, {pred_sym = pred_sym andalso top_level, - min_ary = Int.min (ary, min_ary), - max_ary = Int.max (ary, max_ary), - types = types'}) - sym_tab - end - | NONE => - let - val min_ary = - case explicit_apply of - SOME true => 0 - | SOME false => ary - | NONE => fold (consider_var_arity T) ho_var_Ts ary - in - Symtab.update_new (s, {pred_sym = top_level, - min_ary = min_ary, max_ary = ary, - types = [T]}) - sym_tab - end) - end - | _ => accum) - |> fold (add false) args - end - in add true end -fun add_fact_syms_to_table ctxt explicit_apply = - fact_lift (formula_fold NONE - (K (add_combterm_syms_to_table ctxt explicit_apply))) - -val default_sym_table_entries : (string * sym_info) list = - [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), - (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), - (make_fixed_const predicator_name, - {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @ - ([tptp_false, tptp_true] - |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) - -fun sym_table_for_facts ctxt explicit_apply facts = - Symtab.empty - |> fold Symtab.default default_sym_table_entries - |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd - -fun min_arity_of sym_tab s = - case Symtab.lookup sym_tab s of - SOME ({min_ary, ...} : sym_info) => min_ary - | NONE => - case strip_prefix_and_unascii const_prefix s of - SOME s => - let val s = s |> unmangled_const_name |> invert_const in - if s = predicator_name then 1 - else if s = app_op_name then 2 - else if s = type_pred_name then 1 - else 0 - end - | NONE => 0 - -(* True if the constant ever appears outside of the top-level position in - literals, or if it appears with different arities (e.g., because of different - type instantiations). If false, the constant always receives all of its - arguments and is used as a predicate. *) -fun is_pred_sym sym_tab s = - case Symtab.lookup sym_tab s of - SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => - pred_sym andalso min_ary = max_ary - | NONE => false - -val predicator_combconst = - CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) -fun predicator tm = CombApp (predicator_combconst, tm) - -fun introduce_predicators_in_combterm sym_tab tm = - case strip_combterm_comb tm of - (CombConst ((s, _), _, _), _) => - if is_pred_sym sym_tab s then tm else predicator tm - | _ => predicator tm - -fun list_app head args = fold (curry (CombApp o swap)) args head - -fun explicit_app arg head = - let - val head_T = combtyp_of head - val (arg_T, res_T) = dest_funT head_T - val explicit_app = - CombConst (`make_fixed_const app_op_name, head_T --> head_T, - [arg_T, res_T]) - in list_app explicit_app [head, arg] end -fun list_explicit_app head args = fold explicit_app args head - -fun introduce_explicit_apps_in_combterm sym_tab = - let - fun aux tm = - case strip_combterm_comb tm of - (head as CombConst ((s, _), _, _), args) => - args |> map aux - |> chop (min_arity_of sym_tab s) - |>> list_app head - |-> list_explicit_app - | (head, args) => list_explicit_app head (map aux args) - in aux end - -fun chop_fun 0 T = ([], T) - | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = - chop_fun (n - 1) ran_T |>> cons dom_T - | chop_fun _ _ = raise Fail "unexpected non-function" - -fun filter_type_args _ _ _ [] = [] - | filter_type_args thy s arity T_args = - let - (* will throw "TYPE" for pseudo-constants *) - val U = if s = app_op_name then - @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global - else - s |> Sign.the_const_type thy - in - case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of - [] => [] - | res_U_vars => - let val U_args = (s, U) |> Sign.const_typargs thy in - U_args ~~ T_args - |> map_filter (fn (U, T) => - if member (op =) res_U_vars (dest_TVar U) then - SOME T - else - NONE) - end - end - handle TYPE _ => T_args - -fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = - let - val thy = Proof_Context.theory_of ctxt - fun aux arity (CombApp (tm1, tm2)) = - CombApp (aux (arity + 1) tm1, aux 0 tm2) - | aux arity (CombConst (name as (s, _), T, T_args)) = - let - val level = level_of_type_sys type_sys - val (T, T_args) = - (* Aggressively merge most "hAPPs" if the type system is unsound - anyway, by distinguishing overloads only on the homogenized - result type. Don't do it for lightweight type systems, though, - since it leads to too many unsound proofs. *) - if s = const_prefix ^ app_op_name andalso - length T_args = 2 andalso - not (is_type_sys_virtually_sound type_sys) andalso - heaviness_of_type_sys type_sys = Heavy then - T_args |> map (homogenized_type ctxt nonmono_Ts level 0) - |> (fn Ts => let val T = hd Ts --> nth Ts 1 in - (T --> T, tl Ts) - end) - else - (T, T_args) - in - (case strip_prefix_and_unascii const_prefix s of - NONE => (name, T_args) - | SOME s'' => - let - val s'' = invert_const s'' - fun filtered_T_args false = T_args - | filtered_T_args true = filter_type_args thy s'' arity T_args - in - case type_arg_policy type_sys s'' of - Explicit_Type_Args drop_args => - (name, filtered_T_args drop_args) - | Mangled_Type_Args drop_args => - (mangled_const_name (filtered_T_args drop_args) name, []) - | No_Type_Args => (name, []) - end) - |> (fn (name, T_args) => CombConst (name, T, T_args)) - end - | aux _ tm = tm - in aux 0 end - -fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab = - not (is_setting_higher_order format type_sys) - ? (introduce_explicit_apps_in_combterm sym_tab - #> introduce_predicators_in_combterm sym_tab) - #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys -fun repair_fact ctxt format nonmono_Ts type_sys sym_tab = - update_combformula (formula_map - (repair_combterm ctxt format nonmono_Ts type_sys sym_tab)) - -(** Helper facts **) - -fun ti_ti_helper_fact () = - let - fun var s = ATerm (`I s, []) - fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) - in - Formula (helper_prefix ^ "ti_ti", Axiom, - AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")])) - |> close_formula_universally, simp_info, NONE) - end - -fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) = - case strip_prefix_and_unascii const_prefix s of - SOME mangled_s => - let - val thy = Proof_Context.theory_of ctxt - val unmangled_s = mangled_s |> unmangled_const_name - fun dub_and_inst c needs_fairly_sound (th, j) = - ((c ^ "_" ^ string_of_int j ^ - (if needs_fairly_sound then typed_helper_suffix - else untyped_helper_suffix), - General), - let val t = th |> prop_of in - t |> ((case general_type_arg_policy type_sys of - Mangled_Type_Args _ => true - | _ => false) andalso - not (null (Term.hidden_polymorphism t))) - ? (case types of - [T] => specialize_type thy (invert_const unmangled_s, T) - | _ => I) - end) - fun make_facts eq_as_iff = - map_filter (make_fact ctxt format type_sys false eq_as_iff false) - val fairly_sound = is_type_sys_fairly_sound type_sys - in - metis_helpers - |> maps (fn (metis_s, (needs_fairly_sound, ths)) => - if metis_s <> unmangled_s orelse - (needs_fairly_sound andalso not fairly_sound) then - [] - else - ths ~~ (1 upto length ths) - |> map (dub_and_inst mangled_s needs_fairly_sound) - |> make_facts (not needs_fairly_sound)) - end - | NONE => [] -fun helper_facts_for_sym_table ctxt format type_sys sym_tab = - Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab - [] - -fun translate_atp_fact ctxt format type_sys keep_trivial = - `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of) - -fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t - rich_facts = - let - val thy = Proof_Context.theory_of ctxt - val fact_ts = map (prop_of o snd o snd) rich_facts - val (facts, fact_names) = - rich_facts - |> map_filter (fn (NONE, _) => NONE - | (SOME fact, (name, _)) => SOME (fact, name)) - |> ListPair.unzip - (* Remove existing facts from the conjecture, as this can dramatically - boost an ATP's performance (for some reason). *) - val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val all_ts = goal_t :: fact_ts - val subs = tfree_classes_of_terms all_ts - val supers = tvar_classes_of_terms all_ts - val tycons = type_consts_of_terms thy all_ts - val conjs = - hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys - val (supers', arity_clauses) = - if level_of_type_sys type_sys = No_Types then ([], []) - else make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) - end - -fun fo_literal_from_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_from_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot - -fun type_pred_combterm ctxt nonmono_Ts type_sys T tm = - CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T]) - |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, - tm) - -fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum - | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = - accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) -fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false - | is_var_nonmonotonic_in_formula pos phi _ name = - formula_fold pos (var_occurs_positively_naked_in_term name) phi false - -fun mk_const_aterm x T_args args = - ATerm (x, map (fo_term_from_typ false) T_args @ args) - -fun tag_with_type ctxt format nonmono_Ts type_sys T tm = - CombConst (`make_fixed_const type_tag_name, T --> T, [T]) - |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys - |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level - |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) -and term_from_combterm ctxt format nonmono_Ts type_sys = - let - fun aux site u = - let - val (head, args) = strip_combterm_comb u - val (x as (s, _), T_args) = - case head of - CombConst (name, _, T_args) => (name, T_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg - else Elsewhere - val t = mk_const_aterm x T_args (map (aux arg_site) args) - val T = combtyp_of u - in - t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then - tag_with_type ctxt format nonmono_Ts type_sys T - else - I) - end - in aux end -and formula_from_combformula ctxt format nonmono_Ts type_sys - should_predicate_on_var = - let - val higher_order = is_setting_higher_order format type_sys - val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level - val do_bound_type = - case type_sys of - Simple_Types level => - homogenized_type ctxt nonmono_Ts level 0 - #> mangled_type higher_order false 0 #> SOME - | _ => K NONE - fun do_out_of_bound_type pos phi universal (name, T) = - if should_predicate_on_type ctxt nonmono_Ts type_sys - (fn () => should_predicate_on_var pos phi universal name) T then - CombVar (name, T) - |> type_pred_combterm ctxt nonmono_Ts type_sys T - |> do_term |> AAtom |> SOME - else - NONE - fun do_formula pos (AQuant (q, xs, phi)) = - let - val phi = phi |> do_formula pos - val universal = Option.map (q = AExists ? not) pos - in - AQuant (q, xs |> map (apsnd (fn NONE => NONE - | SOME T => do_bound_type T)), - (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) - (map_filter - (fn (_, NONE) => NONE - | (s, SOME T) => - do_out_of_bound_type pos phi universal (s, T)) - xs) - phi) - end - | do_formula pos (AConn conn) = aconn_map pos do_formula conn - | do_formula _ (AAtom tm) = AAtom (do_term tm) - in do_formula o SOME end - -fun bound_atomic_types format type_sys Ts = - mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) - (atp_type_literals_for_types format type_sys Axiom Ts)) - -fun formula_for_fact ctxt format nonmono_Ts type_sys - ({combformula, atomic_types, ...} : translated_formula) = - combformula - |> close_combformula_universally - |> formula_from_combformula ctxt format nonmono_Ts type_sys - is_var_nonmonotonic_in_formula true - |> bound_atomic_types format type_sys atomic_types - |> close_formula_universally - -(* Each fact is given a unique fact number to avoid name clashes (e.g., because - of monomorphization). The TPTP explicitly forbids name clashes, and some of - the remote provers might care. *) -fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys - (j, formula as {name, locality, kind, ...}) = - Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then "" - else string_of_int j ^ "_") ^ - ascii_of name, - kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE, - case locality of - Intro => intro_info - | Elim => elim_info - | Simp => simp_info - | _ => NONE) - -fun formula_line_for_class_rel_clause - (ClassRelClause {name, subclass, superclass, ...}) = - let val ty_arg = ATerm (`I "T", []) in - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, - AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))]) - |> close_formula_universally, intro_info, NONE) - end - -fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_from_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun formula_line_for_arity_clause - (ArityClause {name, prem_lits, concl_lits, ...}) = - Formula (arity_clause_prefix ^ ascii_of name, Axiom, - mk_ahorn (map (formula_from_fo_literal o apfst not - o fo_literal_from_arity_literal) prem_lits) - (formula_from_fo_literal - (fo_literal_from_arity_literal concl_lits)) - |> close_formula_universally, intro_info, NONE) - -fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys - ({name, kind, combformula, ...} : translated_formula) = - Formula (conjecture_prefix ^ name, kind, - formula_from_combformula ctxt format nonmono_Ts type_sys - is_var_nonmonotonic_in_formula false - (close_combformula_universally combformula) - |> close_formula_universally, NONE, NONE) - -fun free_type_literals format type_sys - ({atomic_types, ...} : translated_formula) = - atomic_types |> atp_type_literals_for_types format type_sys Conjecture - |> map fo_literal_from_type_literal - -fun formula_line_for_free_type j lit = - Formula (tfree_prefix ^ string_of_int j, Hypothesis, - formula_from_fo_literal lit, NONE, NONE) -fun formula_lines_for_free_types format type_sys facts = - let - val litss = map (free_type_literals format type_sys) facts - val lits = fold (union (op =)) litss [] - in map2 formula_line_for_free_type (0 upto length lits - 1) lits end - -(** Symbol declarations **) - -fun should_declare_sym type_sys pred_sym s = - is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso - (case type_sys of - Simple_Types _ => true - | Tags (_, _, Light) => true - | _ => not pred_sym) - -fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) = - let - fun add_combterm in_conj tm = - let val (head, args) = strip_combterm_comb tm in - (case head of - CombConst ((s, s'), T, T_args) => - let val pred_sym = is_pred_sym repaired_sym_tab s in - if should_declare_sym type_sys pred_sym s then - Symtab.map_default (s, []) - (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, - in_conj)) - else - I - end - | _ => I) - #> fold (add_combterm in_conj) args - end - fun add_fact in_conj = - fact_lift (formula_fold NONE (K (add_combterm in_conj))) - in - Symtab.empty - |> is_type_sys_fairly_sound type_sys - ? (fold (add_fact true) conjs #> fold (add_fact false) facts) - end - -(* These types witness that the type classes they belong to allow infinite - models and hence that any types with these type classes is monotonic. *) -val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}] - -(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it - out with monotonicity" paper presented at CADE 2011. *) -fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I - | add_combterm_nonmonotonic_types ctxt level _ - (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = - (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso - (case level of - Nonmonotonic_Types => - not (is_type_surely_infinite ctxt known_infinite_types T) - | Finite_Types => is_type_surely_finite ctxt T - | _ => true)) ? insert_type ctxt I (deep_freeze_type T) - | add_combterm_nonmonotonic_types _ _ _ _ = I -fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...} - : translated_formula) = - formula_fold (SOME (kind <> Conjecture)) - (add_combterm_nonmonotonic_types ctxt level) combformula -fun nonmonotonic_types_for_facts ctxt type_sys facts = - let val level = level_of_type_sys type_sys in - if level = Nonmonotonic_Types orelse level = Finite_Types then - [] |> fold (add_fact_nonmonotonic_types ctxt level) facts - (* We must add "bool" in case the helper "True_or_False" is added - later. In addition, several places in the code rely on the list of - nonmonotonic types not being empty. *) - |> insert_type ctxt I @{typ bool} - else - [] - end - -fun decl_line_for_sym ctxt format nonmono_Ts type_sys s - (s', T_args, T, pred_sym, ary, _) = - let - val (higher_order, T_arg_Ts, level) = - case type_sys of - Simple_Types level => (format = THF, [], level) - | _ => (false, replicate (length T_args) homo_infinite_type, No_Types) - in - Decl (sym_decl_prefix ^ s, (s, s'), - (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary)) - |> mangled_type higher_order pred_sym (length T_arg_Ts + ary)) - end - -fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false - -fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys - n s j (s', T_args, T, _, ary, in_conj) = - let - val (kind, maybe_negate) = - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) - else (Axiom, I) - val (arg_Ts, res_T) = chop_fun ary T - val bound_names = - 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) - val bounds = - bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) - val bound_Ts = - arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T - else NONE) - in - Formula (sym_formula_prefix ^ s ^ - (if n > 1 then "_" ^ string_of_int j else ""), kind, - CombConst ((s, s'), T, T_args) - |> fold (curry (CombApp o swap)) bounds - |> type_pred_combterm ctxt nonmono_Ts type_sys res_T - |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_combformula ctxt format nonmono_Ts type_sys - (K (K (K (K true)))) true - |> n > 1 ? bound_atomic_types format type_sys (atyps_of T) - |> close_formula_universally - |> maybe_negate, - intro_info, NONE) - end - -fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys - n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = - let - val ident_base = - sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") - val (kind, maybe_negate) = - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) - else (Axiom, I) - val (arg_Ts, res_T) = chop_fun ary T - val bound_names = - 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) - val bounds = bound_names |> map (fn name => ATerm (name, [])) - val cst = mk_const_aterm (s, s') T_args - val atomic_Ts = atyps_of T - fun eq tms = - (if pred_sym then AConn (AIff, map AAtom tms) - else AAtom (ATerm (`I tptp_equal, tms))) - |> bound_atomic_types format type_sys atomic_Ts - |> close_formula_universally - |> maybe_negate - val should_encode = should_encode_type ctxt nonmono_Ts All_Types - val tag_with = tag_with_type ctxt format nonmono_Ts type_sys - val add_formula_for_res = - if should_encode res_T then - cons (Formula (ident_base ^ "_res", kind, - eq [tag_with res_T (cst bounds), cst bounds], - simp_info, NONE)) - else - I - fun add_formula_for_arg k = - let val arg_T = nth arg_Ts k in - if should_encode arg_T then - case chop k bounds of - (bounds1, bound :: bounds2) => - cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, - eq [cst (bounds1 @ tag_with arg_T bound :: bounds2), - cst bounds], - simp_info, NONE)) - | _ => raise Fail "expected nonempty tail" - else - I - end - in - [] |> not pred_sym ? add_formula_for_res - |> fold add_formula_for_arg (ary - 1 downto 0) - end - -fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd - -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys - (s, decls) = - case type_sys of - Simple_Types _ => - decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s) - | Preds _ => - let - val decls = - case decls of - decl :: (decls' as _ :: _) => - let val T = result_type_of_decl decl in - if forall (curry (type_instance ctxt o swap) T - o result_type_of_decl) decls' then - [decl] - else - decls - end - | _ => decls - val n = length decls - val decls = - decls - |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true) - o result_type_of_decl) - in - (0 upto length decls - 1, decls) - |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_sys n s) - end - | Tags (_, _, heaviness) => - (case heaviness of - Heavy => [] - | Light => - let val n = length decls in - (0 upto n - 1 ~~ decls) - |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_sys n s) - end) - -fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts - type_sys sym_decl_tab = - sym_decl_tab - |> Symtab.dest - |> sort_wrt fst - |> rpair [] - |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind - nonmono_Ts type_sys) - -fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) = - level = Nonmonotonic_Types orelse level = Finite_Types - | should_add_ti_ti_helper _ = false - -fun offset_of_heading_in_problem _ [] j = j - | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = - if heading = needle then j - else offset_of_heading_in_problem needle problem (j + length lines) - -val implicit_declsN = "Should-be-implicit typings" -val explicit_declsN = "Explicit typings" -val factsN = "Relevant facts" -val class_relsN = "Class relationships" -val aritiesN = "Arities" -val helpersN = "Helper facts" -val conjsN = "Conjectures" -val free_typesN = "Type variables" - -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - explicit_apply hyp_ts concl_t facts = - let - val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = - translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts - val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply - val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys - val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab - val (conjs, facts) = (conjs, facts) |> pairself (map repair) - val repaired_sym_tab = - conjs @ facts |> sym_table_for_facts ctxt (SOME false) - val helpers = - repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys - |> map repair - val lavish_nonmono_Ts = - if null nonmono_Ts orelse - polymorphism_of_type_sys type_sys <> Polymorphic then - nonmono_Ts - else - [TVar (("'a", 0), HOLogic.typeS)] - val sym_decl_lines = - (conjs, helpers @ facts) - |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab - |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind - lavish_nonmono_Ts type_sys - val helper_lines = - 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts - type_sys) - |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ()) - else I) - (* Reordering these might confuse the proof reconstruction code or the SPASS - FLOTTER hack. *) - val problem = - [(explicit_declsN, sym_decl_lines), - (factsN, - map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys) - (0 upto length facts - 1 ~~ facts)), - (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), - (aritiesN, map formula_line_for_arity_clause arity_clauses), - (helpersN, helper_lines), - (conjsN, - map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys) - conjs), - (free_typesN, - formula_lines_for_free_types format type_sys (facts @ conjs))] - val problem = - problem - |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) - |> (if is_format_typed format then - declare_undeclared_syms_in_atp_problem type_decl_prefix - implicit_declsN - else - I) - val (problem, pool) = - problem |> nice_atp_problem (Config.get ctxt readable_names) - val helpers_offset = offset_of_heading_in_problem helpersN problem 0 - val typed_helpers = - map_filter (fn (j, {name, ...}) => - if String.isSuffix typed_helper_suffix name then SOME j - else NONE) - ((helpers_offset + 1 upto helpers_offset + length helpers) - ~~ helpers) - fun add_sym_arity (s, {min_ary, ...} : sym_info) = - if min_ary > 0 then - case strip_prefix_and_unascii const_prefix s of - SOME s => Symtab.insert (op =) (s, min_ary) - | NONE => I - else - I - in - (problem, - case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - offset_of_heading_in_problem conjsN problem 0, - offset_of_heading_in_problem factsN problem 0, - fact_names |> Vector.fromList, - typed_helpers, - Symtab.empty |> Symtab.fold add_sym_arity sym_tab) - end - -(* FUDGE *) -val conj_weight = 0.0 -val hyp_weight = 0.1 -val fact_min_weight = 0.2 -val fact_max_weight = 1.0 -val type_info_default_weight = 0.8 - -fun add_term_weights weight (ATerm (s, tms)) = - is_tptp_user_symbol s ? Symtab.default (s, weight) - #> fold (add_term_weights weight) tms -fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = - formula_fold NONE (K (add_term_weights weight)) phi - | add_problem_line_weights _ _ = I - -fun add_conjectures_weights [] = I - | add_conjectures_weights conjs = - let val (hyps, conj) = split_last conjs in - add_problem_line_weights conj_weight conj - #> fold (add_problem_line_weights hyp_weight) hyps - end - -fun add_facts_weights facts = - let - val num_facts = length facts - fun weight_of j = - fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j - / Real.fromInt num_facts - in - map weight_of (0 upto num_facts - 1) ~~ facts - |> fold (uncurry add_problem_line_weights) - end - -(* Weights are from 0.0 (most important) to 1.0 (least important). *) -fun atp_problem_weights problem = - let val get = these o AList.lookup (op =) problem in - Symtab.empty - |> add_conjectures_weights (get free_typesN @ get conjsN) - |> add_facts_weights (get factsN) - |> fold (fold (add_problem_line_weights type_info_default_weight) o get) - [explicit_declsN, class_relsN, aritiesN] - |> Symtab.dest - |> sort (prod_ord Real.compare string_ord o pairself swap) - end - -end; diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 31 16:38:36 2011 +0200 @@ -7,7 +7,7 @@ signature SLEDGEHAMMER_FILTER = sig - datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained + type locality = ATP_Translate.locality type relevance_fudge = {local_const_multiplier : real, @@ -39,7 +39,6 @@ val new_monomorphizer : bool Config.T val ignore_no_atp : bool Config.T val instantiate_inducts : bool Config.T - val is_locality_global : locality -> bool val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list @@ -59,6 +58,7 @@ structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = struct +open ATP_Translate open Sledgehammer_Util val trace = @@ -73,14 +73,6 @@ val instantiate_inducts = Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) -datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained - -(* (quasi-)underapproximation of the truth *) -fun is_locality_global Local = false - | is_locality_global Assum = false - | is_locality_global Chained = false - | is_locality_global _ = true - type relevance_fudge = {local_const_multiplier : real, worse_irrel_freq : real, diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 16:38:36 2011 +0200 @@ -21,8 +21,8 @@ struct open ATP_Systems +open ATP_Translate open Sledgehammer_Util -open Sledgehammer_ATP_Translate open Sledgehammer_Provers open Sledgehammer_Minimize open Sledgehammer_Run diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue May 31 16:38:36 2011 +0200 @@ -7,8 +7,8 @@ signature SLEDGEHAMMER_MINIMIZE = sig - type locality = Sledgehammer_Filter.locality - type play = Sledgehammer_ATP_Reconstruct.play + type locality = ATP_Translate.locality + type play = ATP_Reconstruct.play type params = Sledgehammer_Provers.params val binary_min_facts : int Config.T @@ -24,10 +24,12 @@ structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = struct +open ATP_Util open ATP_Proof +open ATP_Translate +open ATP_Reconstruct open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_ATP_Reconstruct open Sledgehammer_Provers (* wrapper for calling external prover *) @@ -53,7 +55,7 @@ print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" - else "") ^ "...") + else "") ^ "...") val {goal, ...} = Proof.goal state val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200 @@ -9,12 +9,12 @@ signature SLEDGEHAMMER_PROVERS = sig type failure = ATP_Proof.failure - type locality = Sledgehammer_Filter.locality + type locality = ATP_Translate.locality type relevance_fudge = Sledgehammer_Filter.relevance_fudge - type translated_formula = Sledgehammer_ATP_Translate.translated_formula - type type_system = Sledgehammer_ATP_Translate.type_system - type play = Sledgehammer_ATP_Reconstruct.play - type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + type translated_formula = ATP_Translate.translated_formula + type type_system = ATP_Translate.type_system + type play = ATP_Reconstruct.play + type minimize_command = ATP_Reconstruct.minimize_command datatype mode = Auto_Try | Try | Normal | Minimize @@ -111,14 +111,14 @@ structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = struct +open ATP_Util open ATP_Problem open ATP_Proof open ATP_Systems -open Metis_Translate +open ATP_Translate +open ATP_Reconstruct open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_ATP_Translate -open Sledgehammer_ATP_Reconstruct (** The Sledgehammer **) @@ -838,8 +838,7 @@ [(22, CantConnect), (2, NoLibwwwPerl)] val z3_wrapper_failures = - [(10, NoRealZ3), - (11, InternalError), + [(11, InternalError), (12, InternalError), (13, InternalError)] val z3_failures = diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 31 16:38:36 2011 +0200 @@ -8,8 +8,8 @@ signature SLEDGEHAMMER_RUN = sig + type minimize_command = ATP_Reconstruct.minimize_command type relevance_override = Sledgehammer_Filter.relevance_override - type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params type prover = Sledgehammer_Provers.prover @@ -29,10 +29,11 @@ structure Sledgehammer_Run : SLEDGEHAMMER_RUN = struct +open ATP_Util +open ATP_Translate +open ATP_Reconstruct open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_ATP_Translate -open Sledgehammer_ATP_Reconstruct open Sledgehammer_Provers open Sledgehammer_Minimize diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 31 16:38:36 2011 +0200 @@ -11,26 +11,7 @@ val simplify_spaces : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option - val string_from_ext_time : bool * Time.time -> string - val string_from_time : Time.time -> string - val nat_subscript : int -> string - val unyxml : string -> string - val maybe_quote : string -> string - val typ_of_dtyp : - Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp - -> typ - val varify_type : Proof.context -> typ -> typ - val instantiate_type : theory -> typ -> typ -> typ -> typ - val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ - val is_type_surely_finite : Proof.context -> typ -> bool - val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool - val monomorphic_term : Type.tyenv -> term -> term - val eta_expand : typ list -> term -> int -> term - val transform_elim_prop : term -> term - val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int - val strip_subgoal : - Proof.context -> thm -> int -> (string * typ) list * term list * term val normalize_chained_theorems : thm list -> thm list val reserved_isar_keyword_table : unit -> unit Symtab.table end; @@ -38,10 +19,12 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct +open ATP_Util + fun plural_s n = if n = 1 then "" else "s" val serial_commas = Try.serial_commas -val simplify_spaces = ATP_Proof.strip_spaces false (K true) +val simplify_spaces = strip_spaces false (K true) fun parse_bool_option option name s = (case s of @@ -69,191 +52,8 @@ SOME (seconds (the secs)) end -fun string_from_ext_time (plus, time) = - let val ms = Time.toMilliseconds time in - (if plus then "> " else "") ^ - (if plus andalso ms mod 1000 = 0 then - signed_string_of_int (ms div 1000) ^ " s" - else if ms < 1000 then - signed_string_of_int ms ^ " ms" - else - string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s") - end - -val string_from_time = string_from_ext_time o pair false - -val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) -fun nat_subscript n = - n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript - -val unyxml = XML.content_of o YXML.parse_body - -val is_long_identifier = forall Lexicon.is_identifier o space_explode "." -fun maybe_quote y = - let val s = unyxml y in - y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso - not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse - Keyword.is_keyword s) ? quote - end - -fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) = - the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a)) - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) = - Type (s, map (typ_of_dtyp descr typ_assoc) Us) - | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = - let val (s, ds, _) = the (AList.lookup (op =) descr i) in - Type (s, map (typ_of_dtyp descr typ_assoc) ds) - end - -fun varify_type ctxt T = - Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] - |> snd |> the_single |> dest_Const |> snd - -(* TODO: use "Term_Subst.instantiateT" instead? *) -fun instantiate_type thy T1 T1' T2 = - Same.commit (Envir.subst_type_same - (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 - handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) - -fun varify_and_instantiate_type ctxt T1 T1' T2 = - let val thy = Proof_Context.theory_of ctxt in - instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) - end - -fun datatype_constrs thy (T as Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME {index, descr, ...} => - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in - map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) - constrs - end - | NONE => []) - | datatype_constrs _ _ = [] - -(* Similar to "Nitpick_HOL.bounded_exact_card_of_type". - 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means - cardinality 2 or more. The specified default cardinality is returned if the - cardinality of the type can't be determined. *) -fun tiny_card_of_type ctxt default_card assigns T = - let - val thy = Proof_Context.theory_of ctxt - val max = 2 (* 1 would be too small for the "fun" case *) - fun aux slack avoid T = - if member (op =) avoid T then - 0 - else case AList.lookup (Sign.typ_instance thy o swap) assigns T of - SOME k => k - | NONE => - case T of - Type (@{type_name fun}, [T1, T2]) => - (case (aux slack avoid T1, aux slack avoid T2) of - (k, 1) => if slack andalso k = 0 then 0 else 1 - | (0, _) => 0 - | (_, 0) => 0 - | (k1, k2) => - if k1 >= max orelse k2 >= max then max - else Int.min (max, Integer.pow k2 k1)) - | @{typ prop} => 2 - | @{typ bool} => 2 (* optimization *) - | @{typ nat} => 0 (* optimization *) - | @{typ int} => 0 (* optimization *) - | Type (s, _) => - (case datatype_constrs thy T of - constrs as _ :: _ => - let - val constr_cards = - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types - o snd) constrs - in - if exists (curry (op =) 0) constr_cards then 0 - else Int.min (max, Integer.sum constr_cards) - end - | [] => - case Typedef.get_info ctxt s of - ({abs_type, rep_type, ...}, _) :: _ => - (* We cheat here by assuming that typedef types are infinite if - their underlying type is infinite. This is unsound in general - but it's hard to think of a realistic example where this would - not be the case. We are also slack with representation types: - If a representation type has the form "sigma => tau", we - consider it enough to check "sigma" for infiniteness. (Look - for "slack" in this function.) *) - (case varify_and_instantiate_type ctxt - (Logic.varifyT_global abs_type) T - (Logic.varifyT_global rep_type) - |> aux true avoid of - 0 => 0 - | 1 => 1 - | _ => default_card) - | [] => default_card) - (* Very slightly unsound: Type variables are assumed not to be - constrained to cardinality 1. (In practice, the user would most - likely have used "unit" directly anyway.) *) - | TFree _ => if default_card = 1 then 2 else default_card - (* Schematic type variables that contain only unproblematic sorts - (with no finiteness axiom) can safely be considered infinite. *) - | TVar _ => default_card - in Int.min (max, aux false [] T) end - -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0 -fun is_type_surely_infinite ctxt infinite_Ts T = - tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0 - -fun monomorphic_term subst t = - map_types (map_type_tvar (fn v => - case Type.lookup subst v of - SOME typ => typ - | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ - \variable", [t]))) t - -fun eta_expand _ t 0 = t - | eta_expand Ts (Abs (s, T, t')) n = - Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) - | eta_expand Ts t n = - fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t')) - (List.take (binder_types (fastype_of1 (Ts, t)), n)) - (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) - -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_theorem" in - "Meson_Clausify".) *) -fun transform_elim_prop t = - case Logic.strip_imp_concl t of - @{const Trueprop} $ Var (z, @{typ bool}) => - subst_Vars [(z, @{const False})] t - | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t - | _ => t - -fun specialize_type thy (s, T) t = - let - fun subst_for (Const (s', T')) = - if s = s' then - SOME (Sign.typ_match thy (T', T) Vartab.empty) - handle Type.TYPE_MATCH => NONE - else - NONE - | subst_for (t1 $ t2) = - (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2) - | subst_for (Abs (_, _, t')) = subst_for t' - | subst_for _ = NONE - in - case subst_for t of - SOME subst => monomorphic_term subst t - | NONE => raise Type.TYPE_MATCH - end - val subgoal_count = Try.subgoal_count -fun strip_subgoal ctxt goal i = - let - val (t, (frees, params)) = - Logic.goal_params (prop_of goal) i - ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) - val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) - val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev params, hyp_ts, concl_t) end - val normalize_chained_theorems = maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) fun reserved_isar_keyword_table () = diff -r 946c8e171ffd -r 0a2f5b86bdd7 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/HOL/Tools/refute.ML Tue May 31 16:38:36 2011 +0200 @@ -393,7 +393,7 @@ (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) -val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp +val typ_of_dtyp = ATP_Util.typ_of_dtyp (* ------------------------------------------------------------------------- *) (* close_form: universal closure over schematic variables in 't' *) @@ -410,8 +410,8 @@ Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t end; -val monomorphic_term = Sledgehammer_Util.monomorphic_term -val specialize_type = Sledgehammer_Util.specialize_type +val monomorphic_term = ATP_Util.monomorphic_term +val specialize_type = ATP_Util.specialize_type (* ------------------------------------------------------------------------- *) (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *)