1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 26 09:12:00 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 26 10:42:22 2010 +0200
1.3 @@ -447,33 +447,29 @@
1.4 \label{relevance-filter}
1.5
1.6 \begin{enum}
1.7 -\opdefault{relevance\_threshold}{int}{40}
1.8 -Specifies the threshold above which facts are considered relevant by the
1.9 -relevance filter. The option ranges from 0 to 100, where 0 means that all
1.10 -theorems are relevant.
1.11 +\opdefault{relevance\_thresholds}{int\_pair}{45~95}
1.12 +Specifies the thresholds above which facts are considered relevant by the
1.13 +relevance filter. The first threshold is used for the first iteration of the
1.14 +relevance filter and the second threshold is used for the last iteration (if it
1.15 +is reached). The effective threshold is quadratically interpolated for the other
1.16 +iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
1.17 +are relevant and 100 only theorems that refer to previously seen constants.
1.18
1.19 -\opdefault{relevance\_convergence}{int}{31}
1.20 -Specifies the convergence factor, expressed as a percentage, used by the
1.21 -relevance filter. This factor is used by the relevance filter to scale down the
1.22 -relevance of facts at each iteration of the filter.
1.23 -
1.24 -\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
1.25 -Specifies the maximum number of facts that may be added during one iteration of
1.26 -the relevance filter. If the option is set to \textit{smart}, it is set to a
1.27 -value that was empirically found to be appropriate for the ATP. A typical value
1.28 -would be 50.
1.29 +\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
1.30 +Specifies the maximum number of facts that may be returned by the relevance
1.31 +filter. If the option is set to \textit{smart}, it is set to a value that was
1.32 +empirically found to be appropriate for the ATP. A typical value would be 300.
1.33
1.34 \opsmartx{theory\_relevant}{theory\_irrelevant}
1.35 Specifies whether the theory from which a fact comes should be taken into
1.36 consideration by the relevance filter. If the option is set to \textit{smart},
1.37 -it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
1.38 -because empirical results suggest that these are the best settings.
1.39 +it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
1.40 +empirical results suggest that these are the best settings.
1.41
1.42 -\opfalse{defs\_relevant}{defs\_irrelevant}
1.43 -Specifies whether the definition of constants occurring in the formula to prove
1.44 -should be considered particularly relevant. Enabling this option tends to lead
1.45 -to larger problems and typically slows down the ATPs.
1.46 -
1.47 +%\opfalse{defs\_relevant}{defs\_irrelevant}
1.48 +%Specifies whether the definition of constants occurring in the formula to prove
1.49 +%should be considered particularly relevant. Enabling this option tends to lead
1.50 +%to larger problems and typically slows down the ATPs.
1.51 \end{enum}
1.52
1.53 \subsection{Output Format}
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 26 09:12:00 2010 +0200
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 26 10:42:22 2010 +0200
2.3 @@ -290,10 +290,12 @@
2.4 | NONE => get_prover (default_atp_name ()))
2.5 end
2.6
2.7 +type locality = Sledgehammer_Fact_Filter.locality
2.8 +
2.9 local
2.10
2.11 datatype sh_result =
2.12 - SH_OK of int * int * (string * bool) list |
2.13 + SH_OK of int * int * (string * locality) list |
2.14 SH_FAIL of int * int |
2.15 SH_ERROR
2.16
2.17 @@ -355,8 +357,8 @@
2.18 case result of
2.19 SH_OK (time_isa, time_atp, names) =>
2.20 let
2.21 - fun get_thms (name, chained) =
2.22 - ((name, chained), thms_of_name (Proof.context_of st) name)
2.23 + fun get_thms (name, loc) =
2.24 + ((name, loc), thms_of_name (Proof.context_of st) name)
2.25 in
2.26 change_data id inc_sh_success;
2.27 change_data id (inc_sh_lemmas (length names));
2.28 @@ -445,7 +447,7 @@
2.29 then () else
2.30 let
2.31 val named_thms =
2.32 - Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
2.33 + Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
2.34 val minimize = AList.defined (op =) args minimizeK
2.35 val metis_ft = AList.defined (op =) args metis_ftK
2.36
3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 26 09:12:00 2010 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 26 10:42:22 2010 +0200
3.3 @@ -19,7 +19,7 @@
3.4 has_incomplete_mode: bool,
3.5 proof_delims: (string * string) list,
3.6 known_failures: (failure * string) list,
3.7 - default_max_relevant_per_iter: int,
3.8 + default_max_relevant: int,
3.9 default_theory_relevant: bool,
3.10 explicit_forall: bool,
3.11 use_conjecture_for_hypotheses: bool}
3.12 @@ -52,7 +52,7 @@
3.13 has_incomplete_mode: bool,
3.14 proof_delims: (string * string) list,
3.15 known_failures: (failure * string) list,
3.16 - default_max_relevant_per_iter: int,
3.17 + default_max_relevant: int,
3.18 default_theory_relevant: bool,
3.19 explicit_forall: bool,
3.20 use_conjecture_for_hypotheses: bool}
3.21 @@ -125,10 +125,20 @@
3.22 priority ("Available ATPs: " ^
3.23 commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
3.24
3.25 -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
3.26 +fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
3.27
3.28 (* E prover *)
3.29
3.30 +(* Give older versions of E an extra second, because the "eproof" script wrongly
3.31 + subtracted an entire second to account for the overhead of the script
3.32 + itself, which is in fact much lower. *)
3.33 +fun e_bonus () =
3.34 + case getenv "E_VERSION" of
3.35 + "" => 1000
3.36 + | version =>
3.37 + if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
3.38 + else 0
3.39 +
3.40 val tstp_proof_delims =
3.41 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
3.42
3.43 @@ -137,8 +147,7 @@
3.44 required_execs = [],
3.45 arguments = fn _ => fn timeout =>
3.46 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
3.47 - \--soft-cpu-limit=" ^
3.48 - string_of_int (to_generous_secs timeout),
3.49 + \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
3.50 has_incomplete_mode = false,
3.51 proof_delims = [tstp_proof_delims],
3.52 known_failures =
3.53 @@ -150,7 +159,7 @@
3.54 "# Cannot determine problem status within resource limit"),
3.55 (OutOfResources, "SZS status: ResourceOut"),
3.56 (OutOfResources, "SZS status ResourceOut")],
3.57 - default_max_relevant_per_iter = 80 (* FUDGE *),
3.58 + default_max_relevant = 500 (* FUDGE *),
3.59 default_theory_relevant = false,
3.60 explicit_forall = false,
3.61 use_conjecture_for_hypotheses = true}
3.62 @@ -165,7 +174,7 @@
3.63 required_execs = [("SPASS_HOME", "SPASS")],
3.64 arguments = fn complete => fn timeout =>
3.65 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
3.66 - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
3.67 + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
3.68 |> not complete ? prefix "-SOS=1 ",
3.69 has_incomplete_mode = true,
3.70 proof_delims = [("Here is a proof", "Formulae used in the proof")],
3.71 @@ -177,7 +186,7 @@
3.72 (MalformedInput, "Undefined symbol"),
3.73 (MalformedInput, "Free Variable"),
3.74 (SpassTooOld, "tptp2dfg")],
3.75 - default_max_relevant_per_iter = 40 (* FUDGE *),
3.76 + default_max_relevant = 350 (* FUDGE *),
3.77 default_theory_relevant = true,
3.78 explicit_forall = true,
3.79 use_conjecture_for_hypotheses = true}
3.80 @@ -190,10 +199,11 @@
3.81 val vampire_config : prover_config =
3.82 {exec = ("VAMPIRE_HOME", "vampire"),
3.83 required_execs = [],
3.84 - arguments = fn _ => fn timeout =>
3.85 - "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
3.86 - " --thanks Andrei --input_file",
3.87 - has_incomplete_mode = false,
3.88 + arguments = fn complete => fn timeout =>
3.89 + ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
3.90 + " --thanks Andrei --input_file")
3.91 + |> not complete ? prefix "--sos on ",
3.92 + has_incomplete_mode = true,
3.93 proof_delims =
3.94 [("=========== Refutation ==========",
3.95 "======= End of refutation ======="),
3.96 @@ -206,7 +216,7 @@
3.97 (Unprovable, "Satisfiability detected"),
3.98 (Unprovable, "Termination reason: Satisfiable"),
3.99 (VampireTooOld, "not a valid option")],
3.100 - default_max_relevant_per_iter = 45 (* FUDGE *),
3.101 + default_max_relevant = 400 (* FUDGE *),
3.102 default_theory_relevant = false,
3.103 explicit_forall = false,
3.104 use_conjecture_for_hypotheses = true}
3.105 @@ -246,38 +256,38 @@
3.106 | SOME sys => sys
3.107
3.108 fun remote_config system_name system_versions proof_delims known_failures
3.109 - default_max_relevant_per_iter default_theory_relevant
3.110 - use_conjecture_for_hypotheses =
3.111 + default_max_relevant default_theory_relevant
3.112 + use_conjecture_for_hypotheses : prover_config =
3.113 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
3.114 required_execs = [],
3.115 arguments = fn _ => fn timeout =>
3.116 - " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
3.117 + " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
3.118 the_system system_name system_versions,
3.119 has_incomplete_mode = false,
3.120 proof_delims = insert (op =) tstp_proof_delims proof_delims,
3.121 known_failures =
3.122 known_failures @ known_perl_failures @
3.123 [(TimedOut, "says Timeout")],
3.124 - default_max_relevant_per_iter = default_max_relevant_per_iter,
3.125 + default_max_relevant = default_max_relevant,
3.126 default_theory_relevant = default_theory_relevant,
3.127 explicit_forall = true,
3.128 use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
3.129
3.130 fun remotify_config system_name system_versions
3.131 - ({proof_delims, known_failures, default_max_relevant_per_iter,
3.132 + ({proof_delims, known_failures, default_max_relevant,
3.133 default_theory_relevant, use_conjecture_for_hypotheses, ...}
3.134 : prover_config) : prover_config =
3.135 remote_config system_name system_versions proof_delims known_failures
3.136 - default_max_relevant_per_iter default_theory_relevant
3.137 + default_max_relevant default_theory_relevant
3.138 use_conjecture_for_hypotheses
3.139
3.140 val remotify_name = prefix "remote_"
3.141 fun remote_prover name system_name system_versions proof_delims known_failures
3.142 - default_max_relevant_per_iter default_theory_relevant
3.143 + default_max_relevant default_theory_relevant
3.144 use_conjecture_for_hypotheses =
3.145 (remotify_name name,
3.146 remote_config system_name system_versions proof_delims known_failures
3.147 - default_max_relevant_per_iter default_theory_relevant
3.148 + default_max_relevant default_theory_relevant
3.149 use_conjecture_for_hypotheses)
3.150 fun remotify_prover (name, config) system_name system_versions =
3.151 (remotify_name name, remotify_config system_name system_versions config)
3.152 @@ -285,11 +295,11 @@
3.153 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
3.154 val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
3.155 val remote_sine_e =
3.156 - remote_prover "sine_e" "SInE" [] []
3.157 - [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
3.158 + remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
3.159 + 1000 (* FUDGE *) false true
3.160 val remote_snark =
3.161 remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
3.162 - 50 (* FUDGE *) false true
3.163 + 350 (* FUDGE *) false true
3.164
3.165 (* Setup *)
3.166
4.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 09:12:00 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 10:42:22 2010 +0200
4.3 @@ -38,11 +38,10 @@
4.4 val const_prefix: string
4.5 val type_const_prefix: string
4.6 val class_prefix: string
4.7 - val union_all: ''a list list -> ''a list
4.8 val invert_const: string -> string
4.9 val ascii_of: string -> string
4.10 - val undo_ascii_of: string -> string
4.11 - val strip_prefix_and_undo_ascii: string -> string -> string option
4.12 + val unascii_of: string -> string
4.13 + val strip_prefix_and_unascii: string -> string -> string option
4.14 val make_bound_var : string -> string
4.15 val make_schematic_var : string * int -> string
4.16 val make_fixed_var : string -> string
4.17 @@ -121,7 +120,7 @@
4.18 Alphanumeric characters are left unchanged.
4.19 The character _ goes to __
4.20 Characters in the range ASCII space to / go to _A to _P, respectively.
4.21 - Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
4.22 + Other characters go to _nnn where nnn is the decimal ASCII code.*)
4.23 val A_minus_space = Char.ord #"A" - Char.ord #" ";
4.24
4.25 fun stringN_of_int 0 _ = ""
4.26 @@ -132,9 +131,7 @@
4.27 else if c = #"_" then "__"
4.28 else if #" " <= c andalso c <= #"/"
4.29 then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
4.30 - else if Char.isPrint c
4.31 - then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
4.32 - else ""
4.33 + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
4.34
4.35 val ascii_of = String.translate ascii_of_c;
4.36
4.37 @@ -142,29 +139,28 @@
4.38
4.39 (*We don't raise error exceptions because this code can run inside the watcher.
4.40 Also, the errors are "impossible" (hah!)*)
4.41 -fun undo_ascii_aux rcs [] = String.implode(rev rcs)
4.42 - | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
4.43 +fun unascii_aux rcs [] = String.implode(rev rcs)
4.44 + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
4.45 (*Three types of _ escapes: __, _A to _P, _nnn*)
4.46 - | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
4.47 - | undo_ascii_aux rcs (#"_" :: c :: cs) =
4.48 + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
4.49 + | unascii_aux rcs (#"_" :: c :: cs) =
4.50 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
4.51 - then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
4.52 + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
4.53 else
4.54 let val digits = List.take (c::cs, 3) handle Subscript => []
4.55 in
4.56 case Int.fromString (String.implode digits) of
4.57 - NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
4.58 - | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
4.59 + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
4.60 + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
4.61 end
4.62 - | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
4.63 -
4.64 -val undo_ascii_of = undo_ascii_aux [] o String.explode;
4.65 + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
4.66 +val unascii_of = unascii_aux [] o String.explode
4.67
4.68 (* If string s has the prefix s1, return the result of deleting it,
4.69 un-ASCII'd. *)
4.70 -fun strip_prefix_and_undo_ascii s1 s =
4.71 +fun strip_prefix_and_unascii s1 s =
4.72 if String.isPrefix s1 s then
4.73 - SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
4.74 + SOME (unascii_of (String.extract (s, size s1, NONE)))
4.75 else
4.76 NONE
4.77
4.78 @@ -514,8 +510,8 @@
4.79 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
4.80 fun add_type_consts_in_term thy =
4.81 let
4.82 - val const_typargs = Sign.const_typargs thy
4.83 - fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
4.84 + fun aux (Const x) =
4.85 + fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
4.86 | aux (Abs (_, _, u)) = aux u
4.87 | aux (Const (@{const_name skolem_id}, _) $ _) = I
4.88 | aux (t $ u) = aux t #> aux u
5.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 09:12:00 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 10:42:22 2010 +0200
5.3 @@ -228,15 +228,15 @@
5.4 | smart_invert_const s = invert_const s
5.5
5.6 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
5.7 - (case strip_prefix_and_undo_ascii tvar_prefix v of
5.8 + (case strip_prefix_and_unascii tvar_prefix v of
5.9 SOME w => make_tvar w
5.10 | NONE => make_tvar v)
5.11 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
5.12 - (case strip_prefix_and_undo_ascii type_const_prefix x of
5.13 + (case strip_prefix_and_unascii type_const_prefix x of
5.14 SOME tc => Term.Type (smart_invert_const tc,
5.15 map (hol_type_from_metis_term ctxt) tys)
5.16 | NONE =>
5.17 - case strip_prefix_and_undo_ascii tfree_prefix x of
5.18 + case strip_prefix_and_unascii tfree_prefix x of
5.19 SOME tf => mk_tfree ctxt tf
5.20 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
5.21
5.22 @@ -246,10 +246,10 @@
5.23 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
5.24 Metis.Term.toString fol_tm)
5.25 fun tm_to_tt (Metis.Term.Var v) =
5.26 - (case strip_prefix_and_undo_ascii tvar_prefix v of
5.27 + (case strip_prefix_and_unascii tvar_prefix v of
5.28 SOME w => Type (make_tvar w)
5.29 | NONE =>
5.30 - case strip_prefix_and_undo_ascii schematic_var_prefix v of
5.31 + case strip_prefix_and_unascii schematic_var_prefix v of
5.32 SOME w => Term (mk_var (w, HOLogic.typeT))
5.33 | NONE => Term (mk_var (v, HOLogic.typeT)) )
5.34 (*Var from Metis with a name like _nnn; possibly a type variable*)
5.35 @@ -266,7 +266,7 @@
5.36 and applic_to_tt ("=",ts) =
5.37 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
5.38 | applic_to_tt (a,ts) =
5.39 - case strip_prefix_and_undo_ascii const_prefix a of
5.40 + case strip_prefix_and_unascii const_prefix a of
5.41 SOME b =>
5.42 let val c = smart_invert_const b
5.43 val ntypes = num_type_args thy c
5.44 @@ -284,14 +284,14 @@
5.45 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
5.46 end
5.47 | NONE => (*Not a constant. Is it a type constructor?*)
5.48 - case strip_prefix_and_undo_ascii type_const_prefix a of
5.49 + case strip_prefix_and_unascii type_const_prefix a of
5.50 SOME b =>
5.51 Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
5.52 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
5.53 - case strip_prefix_and_undo_ascii tfree_prefix a of
5.54 + case strip_prefix_and_unascii tfree_prefix a of
5.55 SOME b => Type (mk_tfree ctxt b)
5.56 | NONE => (*a fixed variable? They are Skolem functions.*)
5.57 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
5.58 + case strip_prefix_and_unascii fixed_var_prefix a of
5.59 SOME b =>
5.60 let val opr = Term.Free(b, HOLogic.typeT)
5.61 in apply_list opr (length ts) (map tm_to_tt ts) end
5.62 @@ -307,16 +307,16 @@
5.63 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
5.64 Metis.Term.toString fol_tm)
5.65 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
5.66 - (case strip_prefix_and_undo_ascii schematic_var_prefix v of
5.67 + (case strip_prefix_and_unascii schematic_var_prefix v of
5.68 SOME w => mk_var(w, dummyT)
5.69 | NONE => mk_var(v, dummyT))
5.70 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
5.71 Const (@{const_name "op ="}, HOLogic.typeT)
5.72 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
5.73 - (case strip_prefix_and_undo_ascii const_prefix x of
5.74 + (case strip_prefix_and_unascii const_prefix x of
5.75 SOME c => Const (smart_invert_const c, dummyT)
5.76 | NONE => (*Not a constant. Is it a fixed variable??*)
5.77 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
5.78 + case strip_prefix_and_unascii fixed_var_prefix x of
5.79 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
5.80 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
5.81 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
5.82 @@ -327,10 +327,10 @@
5.83 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
5.84 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
5.85 | cvt (t as Metis.Term.Fn (x, [])) =
5.86 - (case strip_prefix_and_undo_ascii const_prefix x of
5.87 + (case strip_prefix_and_unascii const_prefix x of
5.88 SOME c => Const (smart_invert_const c, dummyT)
5.89 | NONE => (*Not a constant. Is it a fixed variable??*)
5.90 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
5.91 + case strip_prefix_and_unascii fixed_var_prefix x of
5.92 SOME v => Free (v, dummyT)
5.93 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
5.94 hol_term_from_metis_PT ctxt t))
5.95 @@ -410,11 +410,11 @@
5.96 " in " ^ Display.string_of_thm ctxt i_th);
5.97 NONE)
5.98 fun remove_typeinst (a, t) =
5.99 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
5.100 + case strip_prefix_and_unascii schematic_var_prefix a of
5.101 SOME b => SOME (b, t)
5.102 - | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
5.103 + | NONE => case strip_prefix_and_unascii tvar_prefix a of
5.104 SOME _ => NONE (*type instantiations are forbidden!*)
5.105 - | NONE => SOME (a,t) (*internal Metis var?*)
5.106 + | NONE => SOME (a,t) (*internal Metis var?*)
5.107 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
5.108 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
5.109 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 09:12:00 2010 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 10:42:22 2010 +0200
6.3 @@ -9,6 +9,7 @@
6.4 signature SLEDGEHAMMER =
6.5 sig
6.6 type failure = ATP_Systems.failure
6.7 + type locality = Sledgehammer_Fact_Filter.locality
6.8 type relevance_override = Sledgehammer_Fact_Filter.relevance_override
6.9 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
6.10 type params =
6.11 @@ -18,11 +19,9 @@
6.12 atps: string list,
6.13 full_types: bool,
6.14 explicit_apply: bool,
6.15 - relevance_threshold: real,
6.16 - relevance_convergence: real,
6.17 - max_relevant_per_iter: int option,
6.18 + relevance_thresholds: real * real,
6.19 + max_relevant: int option,
6.20 theory_relevant: bool option,
6.21 - defs_relevant: bool,
6.22 isar_proof: bool,
6.23 isar_shrink_factor: int,
6.24 timeout: Time.time}
6.25 @@ -30,16 +29,16 @@
6.26 {subgoal: int,
6.27 goal: Proof.context * (thm list * thm),
6.28 relevance_override: relevance_override,
6.29 - axioms: ((string * bool) * thm) list option}
6.30 + axioms: ((string * locality) * thm) list option}
6.31 type prover_result =
6.32 {outcome: failure option,
6.33 message: string,
6.34 pool: string Symtab.table,
6.35 - used_thm_names: (string * bool) list,
6.36 + used_thm_names: (string * locality) list,
6.37 atp_run_time_in_msecs: int,
6.38 output: string,
6.39 proof: string,
6.40 - axiom_names: (string * bool) vector,
6.41 + axiom_names: (string * locality) vector,
6.42 conjecture_shape: int list list}
6.43 type prover = params -> minimize_command -> problem -> prover_result
6.44
6.45 @@ -87,11 +86,9 @@
6.46 atps: string list,
6.47 full_types: bool,
6.48 explicit_apply: bool,
6.49 - relevance_threshold: real,
6.50 - relevance_convergence: real,
6.51 - max_relevant_per_iter: int option,
6.52 + relevance_thresholds: real * real,
6.53 + max_relevant: int option,
6.54 theory_relevant: bool option,
6.55 - defs_relevant: bool,
6.56 isar_proof: bool,
6.57 isar_shrink_factor: int,
6.58 timeout: Time.time}
6.59 @@ -100,17 +97,17 @@
6.60 {subgoal: int,
6.61 goal: Proof.context * (thm list * thm),
6.62 relevance_override: relevance_override,
6.63 - axioms: ((string * bool) * thm) list option}
6.64 + axioms: ((string * locality) * thm) list option}
6.65
6.66 type prover_result =
6.67 {outcome: failure option,
6.68 message: string,
6.69 pool: string Symtab.table,
6.70 - used_thm_names: (string * bool) list,
6.71 + used_thm_names: (string * locality) list,
6.72 atp_run_time_in_msecs: int,
6.73 output: string,
6.74 proof: string,
6.75 - axiom_names: (string * bool) vector,
6.76 + axiom_names: (string * locality) vector,
6.77 conjecture_shape: int list list}
6.78
6.79 type prover = params -> minimize_command -> problem -> prover_result
6.80 @@ -174,10 +171,9 @@
6.81 Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
6.82 |-- Scan.repeat parse_clause_formula_pair
6.83 val extract_clause_formula_relation =
6.84 - Substring.full
6.85 - #> Substring.position set_ClauseFormulaRelationN
6.86 - #> snd #> Substring.string #> strip_spaces #> explode
6.87 - #> parse_clause_formula_relation #> fst
6.88 + Substring.full #> Substring.position set_ClauseFormulaRelationN
6.89 + #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
6.90 + #> explode #> parse_clause_formula_relation #> fst
6.91
6.92 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
6.93 axiom_names =
6.94 @@ -190,17 +186,19 @@
6.95 val seq = extract_clause_sequence output
6.96 val name_map = extract_clause_formula_relation output
6.97 fun renumber_conjecture j =
6.98 - conjecture_prefix ^ Int.toString (j - j0)
6.99 + conjecture_prefix ^ string_of_int (j - j0)
6.100 |> AList.find (fn (s, ss) => member (op =) ss s) name_map
6.101 |> map (fn s => find_index (curry (op =) s) seq + 1)
6.102 fun name_for_number j =
6.103 let
6.104 val axioms =
6.105 - j |> AList.lookup (op =) name_map
6.106 - |> these |> map_filter (try (unprefix axiom_prefix))
6.107 - |> map undo_ascii_of
6.108 - val chained = forall (is_true_for axiom_names) axioms
6.109 - in (axioms |> space_implode " ", chained) end
6.110 + j |> AList.lookup (op =) name_map |> these
6.111 + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
6.112 + val loc =
6.113 + case axioms of
6.114 + [axiom] => find_first_in_vector axiom_names axiom General
6.115 + | _ => General
6.116 + in (axioms |> space_implode " ", loc) end
6.117 in
6.118 (conjecture_shape |> map (maps renumber_conjecture),
6.119 seq |> map name_for_number |> Vector.fromList)
6.120 @@ -213,12 +211,11 @@
6.121
6.122 fun prover_fun atp_name
6.123 {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
6.124 - known_failures, default_max_relevant_per_iter, default_theory_relevant,
6.125 + known_failures, default_max_relevant, default_theory_relevant,
6.126 explicit_forall, use_conjecture_for_hypotheses}
6.127 ({debug, verbose, overlord, full_types, explicit_apply,
6.128 - relevance_threshold, relevance_convergence,
6.129 - max_relevant_per_iter, theory_relevant,
6.130 - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
6.131 + relevance_thresholds, max_relevant, theory_relevant, isar_proof,
6.132 + isar_shrink_factor, timeout, ...} : params)
6.133 minimize_command
6.134 ({subgoal, goal, relevance_override, axioms} : problem) =
6.135 let
6.136 @@ -226,7 +223,7 @@
6.137 val thy = ProofContext.theory_of ctxt
6.138 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
6.139
6.140 - fun print s = (priority s; if debug then tracing s else ())
6.141 + val print = priority
6.142 fun print_v f = () |> verbose ? print o f
6.143 fun print_d f = () |> debug ? print o f
6.144
6.145 @@ -234,15 +231,13 @@
6.146 case axioms of
6.147 SOME axioms => axioms
6.148 | NONE =>
6.149 - (relevant_facts full_types relevance_threshold relevance_convergence
6.150 - defs_relevant
6.151 - (the_default default_max_relevant_per_iter
6.152 - max_relevant_per_iter)
6.153 + (relevant_facts full_types relevance_thresholds
6.154 + (the_default default_max_relevant max_relevant)
6.155 (the_default default_theory_relevant theory_relevant)
6.156 relevance_override goal hyp_ts concl_t
6.157 |> tap ((fn n => print_v (fn () =>
6.158 - "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
6.159 - " for " ^ quote atp_name ^ ".")) o length))
6.160 + "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
6.161 + " for " ^ quote atp_name ^ ".")) o length))
6.162
6.163 (* path to unique problem file *)
6.164 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
6.165 @@ -261,6 +256,7 @@
6.166 else error ("No such directory: " ^ the_dest_dir ^ ".")
6.167 end;
6.168
6.169 + val measure_run_time = verbose orelse Config.get ctxt measure_runtime
6.170 val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
6.171 (* write out problem file and call prover *)
6.172 fun command_line complete timeout probfile =
6.173 @@ -268,10 +264,8 @@
6.174 val core = File.shell_path command ^ " " ^ arguments complete timeout ^
6.175 " " ^ File.shell_path probfile
6.176 in
6.177 - (if Config.get ctxt measure_runtime then
6.178 - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
6.179 - else
6.180 - "exec " ^ core) ^ " 2>&1"
6.181 + (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
6.182 + else "exec " ^ core) ^ " 2>&1"
6.183 end
6.184 fun split_time s =
6.185 let
6.186 @@ -300,14 +294,11 @@
6.187 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
6.188 else
6.189 I)
6.190 - |>> (if Config.get ctxt measure_runtime then split_time
6.191 - else rpair 0)
6.192 + |>> (if measure_run_time then split_time else rpair 0)
6.193 val (proof, outcome) =
6.194 extract_proof_and_outcome complete res_code proof_delims
6.195 known_failures output
6.196 in (output, msecs, proof, outcome) end
6.197 - val _ = print_d (fn () => "Preparing problem for " ^
6.198 - quote atp_name ^ "...")
6.199 val readable_names = debug andalso overlord
6.200 val (problem, pool, conjecture_offset, axiom_names) =
6.201 prepare_problem ctxt readable_names explicit_forall full_types
6.202 @@ -358,6 +349,11 @@
6.203 proof_text isar_proof
6.204 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
6.205 (full_types, minimize_command, proof, axiom_names, th, subgoal)
6.206 + |>> (fn message =>
6.207 + message ^ (if verbose then
6.208 + "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
6.209 + else
6.210 + ""))
6.211 | SOME failure => (string_for_failure failure, [])
6.212 in
6.213 {outcome = outcome, message = message, pool = pool,
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 09:12:00 2010 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 10:42:22 2010 +0200
7.3 @@ -5,19 +5,21 @@
7.4
7.5 signature SLEDGEHAMMER_FACT_FILTER =
7.6 sig
7.7 + datatype locality = General | Theory | Local | Chained
7.8 +
7.9 type relevance_override =
7.10 {add: Facts.ref list,
7.11 del: Facts.ref list,
7.12 only: bool}
7.13
7.14 val trace : bool Unsynchronized.ref
7.15 - val name_thms_pair_from_ref :
7.16 + val name_thm_pairs_from_ref :
7.17 Proof.context -> unit Symtab.table -> thm list -> Facts.ref
7.18 - -> (unit -> string * bool) * thm list
7.19 + -> ((string * locality) * thm) list
7.20 val relevant_facts :
7.21 - bool -> real -> real -> bool -> int -> bool -> relevance_override
7.22 + bool -> real * real -> int -> bool -> relevance_override
7.23 -> Proof.context * (thm list * 'a) -> term list -> term
7.24 - -> ((string * bool) * thm) list
7.25 + -> ((string * locality) * thm) list
7.26 end;
7.27
7.28 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
7.29 @@ -30,6 +32,8 @@
7.30
7.31 val respect_no_atp = true
7.32
7.33 +datatype locality = General | Theory | Local | Chained
7.34 +
7.35 type relevance_override =
7.36 {add: Facts.ref list,
7.37 del: Facts.ref list,
7.38 @@ -37,13 +41,22 @@
7.39
7.40 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
7.41
7.42 -fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
7.43 - let val ths = ProofContext.get_fact ctxt xref in
7.44 - (fn () => let
7.45 - val name = Facts.string_of_ref xref
7.46 - val name = name |> Symtab.defined reserved name ? quote
7.47 - val chained = forall (member Thm.eq_thm chained_ths) ths
7.48 - in (name, chained) end, ths)
7.49 +fun repair_name reserved multi j name =
7.50 + (name |> Symtab.defined reserved name ? quote) ^
7.51 + (if multi then "(" ^ Int.toString j ^ ")" else "")
7.52 +
7.53 +fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
7.54 + let
7.55 + val ths = ProofContext.get_fact ctxt xref
7.56 + val name = Facts.string_of_ref xref
7.57 + val multi = length ths > 1
7.58 + in
7.59 + (ths, (1, []))
7.60 + |-> fold (fn th => fn (j, rest) =>
7.61 + (j + 1, ((repair_name reserved multi j name,
7.62 + if member Thm.eq_thm chained_ths th then Chained
7.63 + else General), th) :: rest))
7.64 + |> snd
7.65 end
7.66
7.67 (***************************************************************)
7.68 @@ -53,61 +66,81 @@
7.69 (*** constants with types ***)
7.70
7.71 (*An abstraction of Isabelle types*)
7.72 -datatype const_typ = CTVar | CType of string * const_typ list
7.73 +datatype pseudotype = PVar | PType of string * pseudotype list
7.74 +
7.75 +fun string_for_pseudotype PVar = "?"
7.76 + | string_for_pseudotype (PType (s, Ts)) =
7.77 + (case Ts of
7.78 + [] => ""
7.79 + | [T] => string_for_pseudotype T
7.80 + | Ts => string_for_pseudotypes Ts ^ " ") ^ s
7.81 +and string_for_pseudotypes Ts =
7.82 + "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
7.83
7.84 (*Is the second type an instance of the first one?*)
7.85 -fun match_type (CType(con1,args1)) (CType(con2,args2)) =
7.86 - con1=con2 andalso match_types args1 args2
7.87 - | match_type CTVar _ = true
7.88 - | match_type _ CTVar = false
7.89 -and match_types [] [] = true
7.90 - | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
7.91 +fun match_pseudotype (PType (a, T), PType (b, U)) =
7.92 + a = b andalso match_pseudotypes (T, U)
7.93 + | match_pseudotype (PVar, _) = true
7.94 + | match_pseudotype (_, PVar) = false
7.95 +and match_pseudotypes ([], []) = true
7.96 + | match_pseudotypes (T :: Ts, U :: Us) =
7.97 + match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
7.98
7.99 (*Is there a unifiable constant?*)
7.100 -fun const_mem const_tab (c, c_typ) =
7.101 - exists (match_types c_typ) (these (Symtab.lookup const_tab c))
7.102 +fun pseudoconst_mem f const_tab (c, c_typ) =
7.103 + exists (curry (match_pseudotypes o f) c_typ)
7.104 + (these (Symtab.lookup const_tab c))
7.105
7.106 -(*Maps a "real" type to a const_typ*)
7.107 -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
7.108 - | const_typ_of (TFree _) = CTVar
7.109 - | const_typ_of (TVar _) = CTVar
7.110 +fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
7.111 + | pseudotype_for (TFree _) = PVar
7.112 + | pseudotype_for (TVar _) = PVar
7.113 +(* Pairs a constant with the list of its type instantiations. *)
7.114 +fun pseudoconst_for thy (c, T) =
7.115 + (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
7.116 + handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
7.117
7.118 -(*Pairs a constant with the list of its type instantiations (using const_typ)*)
7.119 -fun const_with_typ thy (c,typ) =
7.120 - let val tvars = Sign.const_typargs thy (c,typ) in
7.121 - (c, map const_typ_of tvars) end
7.122 - handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
7.123 +fun string_for_pseudoconst (s, []) = s
7.124 + | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
7.125 +fun string_for_super_pseudoconst (s, [[]]) = s
7.126 + | string_for_super_pseudoconst (s, Tss) =
7.127 + s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
7.128
7.129 -(*Add a const/type pair to the table, but a [] entry means a standard connective,
7.130 - which we ignore.*)
7.131 -fun add_const_to_table (c, ctyps) =
7.132 - Symtab.map_default (c, [ctyps])
7.133 - (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
7.134 +val abs_prefix = "Sledgehammer.abs"
7.135 +val skolem_prefix = "Sledgehammer.sko"
7.136 +
7.137 +(* Add a pseudoconstant to the table, but a [] entry means a standard
7.138 + connective, which we ignore.*)
7.139 +fun add_pseudoconst_to_table also_skolem (c, ctyps) =
7.140 + if also_skolem orelse not (String.isPrefix skolem_prefix c) then
7.141 + Symtab.map_default (c, [ctyps])
7.142 + (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
7.143 + else
7.144 + I
7.145
7.146 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
7.147
7.148 -val fresh_prefix = "Sledgehammer.FRESH."
7.149 val flip = Option.map not
7.150 (* These are typically simplified away by "Meson.presimplify". *)
7.151 val boring_consts =
7.152 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
7.153
7.154 -fun get_consts thy pos ts =
7.155 +fun get_pseudoconsts thy also_skolems pos ts =
7.156 let
7.157 (* We include free variables, as well as constants, to handle locales. For
7.158 each quantifiers that must necessarily be skolemized by the ATP, we
7.159 introduce a fresh constant to simulate the effect of Skolemization. *)
7.160 fun do_term t =
7.161 case t of
7.162 - Const x => add_const_to_table (const_with_typ thy x)
7.163 - | Free (s, _) => add_const_to_table (s, [])
7.164 + Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
7.165 + | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
7.166 | t1 $ t2 => fold do_term [t1, t2]
7.167 - | Abs (_, _, t') => do_term t'
7.168 + | Abs (_, _, t') =>
7.169 + do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
7.170 | _ => I
7.171 fun do_quantifier will_surely_be_skolemized body_t =
7.172 do_formula pos body_t
7.173 - #> (if will_surely_be_skolemized then
7.174 - add_const_to_table (gensym fresh_prefix, [])
7.175 + #> (if also_skolems andalso will_surely_be_skolemized then
7.176 + add_pseudoconst_to_table true (gensym skolem_prefix, [])
7.177 else
7.178 I)
7.179 and do_term_or_formula T =
7.180 @@ -164,31 +197,25 @@
7.181
7.182 (**** Constant / Type Frequencies ****)
7.183
7.184 -(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
7.185 - constant name and second by its list of type instantiations. For the latter, we need
7.186 - a linear ordering on type const_typ list.*)
7.187 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
7.188 + first by constant name and second by its list of type instantiations. For the
7.189 + latter, we need a linear ordering on "pseudotype list". *)
7.190
7.191 -local
7.192 +fun pseudotype_ord p =
7.193 + case p of
7.194 + (PVar, PVar) => EQUAL
7.195 + | (PVar, PType _) => LESS
7.196 + | (PType _, PVar) => GREATER
7.197 + | (PType q1, PType q2) =>
7.198 + prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
7.199
7.200 -fun cons_nr CTVar = 0
7.201 - | cons_nr (CType _) = 1;
7.202 -
7.203 -in
7.204 -
7.205 -fun const_typ_ord TU =
7.206 - case TU of
7.207 - (CType (a, Ts), CType (b, Us)) =>
7.208 - (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
7.209 - | (T, U) => int_ord (cons_nr T, cons_nr U);
7.210 -
7.211 -end;
7.212 -
7.213 -structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
7.214 +structure CTtab =
7.215 + Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
7.216
7.217 fun count_axiom_consts theory_relevant thy (_, th) =
7.218 let
7.219 fun do_const (a, T) =
7.220 - let val (c, cts) = const_with_typ thy (a, T) in
7.221 + let val (c, cts) = pseudoconst_for thy (a, T) in
7.222 (* Two-dimensional table update. Constant maps to types maps to
7.223 count. *)
7.224 CTtab.map_default (cts, 0) (Integer.add 1)
7.225 @@ -205,8 +232,8 @@
7.226 (**** Actual Filtering Code ****)
7.227
7.228 (*The frequency of a constant is the sum of those of all instances of its type.*)
7.229 -fun const_frequency const_tab (c, cts) =
7.230 - CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
7.231 +fun pseudoconst_freq match const_tab (c, cts) =
7.232 + CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
7.233 (the (Symtab.lookup const_tab c)) 0
7.234 handle Option.Option => 0
7.235
7.236 @@ -216,183 +243,206 @@
7.237
7.238 (* "log" seems best in practice. A constant function of one ignores the constant
7.239 frequencies. *)
7.240 -fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
7.241 -fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
7.242 +fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
7.243 +(* TODO: experiment
7.244 +fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
7.245 +*)
7.246 +fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
7.247 +
7.248 +(* FUDGE *)
7.249 +val skolem_weight = 1.0
7.250 +val abs_weight = 2.0
7.251
7.252 (* Computes a constant's weight, as determined by its frequency. *)
7.253 -val rel_const_weight = rel_log o real oo const_frequency
7.254 -val irrel_const_weight = irrel_log o real oo const_frequency
7.255 -(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
7.256 -
7.257 -fun axiom_weight const_tab relevant_consts axiom_consts =
7.258 - let
7.259 - val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
7.260 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
7.261 - val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0
7.262 - val res = rel_weight / (rel_weight + irrel_weight)
7.263 - in if Real.isFinite res then res else 0.0 end
7.264 -
7.265 -(* OLD CODE:
7.266 -(*Relevant constants are weighted according to frequency,
7.267 - but irrelevant constants are simply counted. Otherwise, Skolem functions,
7.268 - which are rare, would harm a formula's chances of being picked.*)
7.269 -fun axiom_weight const_tab relevant_consts axiom_consts =
7.270 - let
7.271 - val rel = filter (const_mem relevant_consts) axiom_consts
7.272 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
7.273 - val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
7.274 - in if Real.isFinite res then res else 0.0 end
7.275 +val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
7.276 +fun irrel_weight const_tab (c as (s, _)) =
7.277 + if String.isPrefix skolem_prefix s then skolem_weight
7.278 + else if String.isPrefix abs_prefix s then abs_weight
7.279 + else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
7.280 +(* TODO: experiment
7.281 +fun irrel_weight _ _ = 1.0
7.282 *)
7.283
7.284 -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
7.285 -fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
7.286 +(* FUDGE *)
7.287 +fun locality_multiplier General = 1.0
7.288 + | locality_multiplier Theory = 1.1
7.289 + | locality_multiplier Local = 1.3
7.290 + | locality_multiplier Chained = 2.0
7.291
7.292 -fun consts_of_term thy t =
7.293 - Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
7.294 +fun axiom_weight loc const_tab relevant_consts axiom_consts =
7.295 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
7.296 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
7.297 + ([], []) => 0.0
7.298 + | (_, []) => 1.0
7.299 + | (rel, irrel) =>
7.300 + let
7.301 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
7.302 + |> curry Real.* (locality_multiplier loc)
7.303 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
7.304 + val res = rel_weight / (rel_weight + irrel_weight)
7.305 + in if Real.isFinite res then res else 0.0 end
7.306
7.307 +(* TODO: experiment
7.308 +fun debug_axiom_weight const_tab relevant_consts axiom_consts =
7.309 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
7.310 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
7.311 + ([], []) => 0.0
7.312 + | (_, []) => 1.0
7.313 + | (rel, irrel) =>
7.314 + let
7.315 +val _ = tracing (PolyML.makestring ("REL: ", rel))
7.316 +val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
7.317 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
7.318 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
7.319 + val res = rel_weight / (rel_weight + irrel_weight)
7.320 + in if Real.isFinite res then res else 0.0 end
7.321 +*)
7.322 +
7.323 +fun pseudoconsts_of_term thy t =
7.324 + Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
7.325 + (get_pseudoconsts thy true (SOME true) [t]) []
7.326 fun pair_consts_axiom theory_relevant thy axiom =
7.327 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
7.328 - |> consts_of_term thy)
7.329 -
7.330 -exception CONST_OR_FREE of unit
7.331 -
7.332 -fun dest_Const_or_Free (Const x) = x
7.333 - | dest_Const_or_Free (Free x) = x
7.334 - | dest_Const_or_Free _ = raise CONST_OR_FREE ()
7.335 -
7.336 -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
7.337 -fun defines thy thm gctypes =
7.338 - let val tm = prop_of thm
7.339 - fun defs lhs rhs =
7.340 - let val (rator,args) = strip_comb lhs
7.341 - val ct = const_with_typ thy (dest_Const_or_Free rator)
7.342 - in
7.343 - forall is_Var args andalso const_mem gctypes ct andalso
7.344 - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
7.345 - end
7.346 - handle CONST_OR_FREE () => false
7.347 - in
7.348 - case tm of
7.349 - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
7.350 - defs lhs rhs
7.351 - | _ => false
7.352 - end;
7.353 + |> pseudoconsts_of_term thy)
7.354
7.355 type annotated_thm =
7.356 - ((unit -> string * bool) * thm) * (string * const_typ list) list
7.357 + (((unit -> string) * locality) * thm) * (string * pseudotype list) list
7.358
7.359 -(*For a reverse sort, putting the largest values first.*)
7.360 -fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
7.361 +fun take_most_relevant max_max_imperfect max_relevant remaining_max
7.362 + (candidates : (annotated_thm * real) list) =
7.363 + let
7.364 + val max_imperfect =
7.365 + Real.ceil (Math.pow (max_max_imperfect,
7.366 + Real.fromInt remaining_max
7.367 + / Real.fromInt max_relevant))
7.368 + val (perfect, imperfect) =
7.369 + candidates |> List.partition (fn (_, w) => w > 0.99999)
7.370 + ||> sort (Real.compare o swap o pairself snd)
7.371 + val ((accepts, more_rejects), rejects) =
7.372 + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
7.373 + in
7.374 + trace_msg (fn () => "Number of candidates: " ^
7.375 + string_of_int (length candidates));
7.376 + trace_msg (fn () => "Effective threshold: " ^
7.377 + Real.toString (#2 (hd accepts)));
7.378 + trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
7.379 + "): " ^ (accepts
7.380 + |> map (fn ((((name, _), _), _), weight) =>
7.381 + name () ^ " [" ^ Real.toString weight ^ "]")
7.382 + |> commas));
7.383 + (accepts, more_rejects @ rejects)
7.384 + end
7.385
7.386 -(* Limit the number of new facts, to prevent runaway acceptance. *)
7.387 -fun take_best max_new (new_pairs : (annotated_thm * real) list) =
7.388 - let val nnew = length new_pairs in
7.389 - if nnew <= max_new then
7.390 - (map #1 new_pairs, [])
7.391 - else
7.392 - let
7.393 - val new_pairs = sort compare_pairs new_pairs
7.394 - val accepted = List.take (new_pairs, max_new)
7.395 - in
7.396 - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
7.397 - ", exceeds the limit of " ^ Int.toString max_new));
7.398 - trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
7.399 - trace_msg (fn () => "Actually passed: " ^
7.400 - space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
7.401 - (map #1 accepted, List.drop (new_pairs, max_new))
7.402 - end
7.403 - end;
7.404 -
7.405 +(* FUDGE *)
7.406 val threshold_divisor = 2.0
7.407 val ridiculous_threshold = 0.1
7.408 +val max_max_imperfect_fudge_factor = 0.66
7.409
7.410 -fun relevance_filter ctxt relevance_threshold relevance_convergence
7.411 - defs_relevant max_new theory_relevant
7.412 +fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
7.413 ({add, del, ...} : relevance_override) axioms goal_ts =
7.414 - if relevance_threshold > 1.0 then
7.415 - []
7.416 - else if relevance_threshold < 0.0 then
7.417 - axioms
7.418 - else
7.419 - let
7.420 - val thy = ProofContext.theory_of ctxt
7.421 - val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
7.422 - Symtab.empty
7.423 - val goal_const_tab = get_consts thy (SOME false) goal_ts
7.424 - val _ =
7.425 - trace_msg (fn () => "Initial constants: " ^
7.426 - commas (goal_const_tab
7.427 - |> Symtab.dest
7.428 - |> filter (curry (op <>) [] o snd)
7.429 - |> map fst))
7.430 - val add_thms = maps (ProofContext.get_fact ctxt) add
7.431 - val del_thms = maps (ProofContext.get_fact ctxt) del
7.432 - fun iter j threshold rel_const_tab =
7.433 - let
7.434 - fun relevant ([], rejects) [] =
7.435 - (* Nothing was added this iteration. *)
7.436 - if j = 0 andalso threshold >= ridiculous_threshold then
7.437 - (* First iteration? Try again. *)
7.438 - iter 0 (threshold / threshold_divisor) rel_const_tab
7.439 - (map (apsnd SOME) rejects)
7.440 + let
7.441 + val thy = ProofContext.theory_of ctxt
7.442 + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
7.443 + Symtab.empty
7.444 + val add_thms = maps (ProofContext.get_fact ctxt) add
7.445 + val del_thms = maps (ProofContext.get_fact ctxt) del
7.446 + val max_max_imperfect =
7.447 + Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
7.448 + fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
7.449 + let
7.450 + fun game_over rejects =
7.451 + (* Add "add:" facts. *)
7.452 + if null add_thms then
7.453 + []
7.454 + else
7.455 + map_filter (fn ((p as (_, th), _), _) =>
7.456 + if member Thm.eq_thm add_thms th then SOME p
7.457 + else NONE) rejects
7.458 + fun relevant [] rejects hopeless [] =
7.459 + (* Nothing has been added this iteration. *)
7.460 + if j = 0 andalso threshold >= ridiculous_threshold then
7.461 + (* First iteration? Try again. *)
7.462 + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
7.463 + hopeless hopeful
7.464 + else
7.465 + game_over (rejects @ hopeless)
7.466 + | relevant candidates rejects hopeless [] =
7.467 + let
7.468 + val (accepts, more_rejects) =
7.469 + take_most_relevant max_max_imperfect max_relevant remaining_max
7.470 + candidates
7.471 + val rel_const_tab' =
7.472 + rel_const_tab
7.473 + |> fold (add_pseudoconst_to_table false)
7.474 + (maps (snd o fst) accepts)
7.475 + fun is_dirty (c, _) =
7.476 + Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
7.477 + val (hopeful_rejects, hopeless_rejects) =
7.478 + (rejects @ hopeless, ([], []))
7.479 + |-> fold (fn (ax as (_, consts), old_weight) =>
7.480 + if exists is_dirty consts then
7.481 + apfst (cons (ax, NONE))
7.482 + else
7.483 + apsnd (cons (ax, old_weight)))
7.484 + |>> append (more_rejects
7.485 + |> map (fn (ax as (_, consts), old_weight) =>
7.486 + (ax, if exists is_dirty consts then NONE
7.487 + else SOME old_weight)))
7.488 + val threshold =
7.489 + threshold + (1.0 - threshold)
7.490 + * Math.pow (decay, Real.fromInt (length accepts))
7.491 + val remaining_max = remaining_max - length accepts
7.492 + in
7.493 + trace_msg (fn () => "New or updated constants: " ^
7.494 + commas (rel_const_tab' |> Symtab.dest
7.495 + |> subtract (op =) (Symtab.dest rel_const_tab)
7.496 + |> map string_for_super_pseudoconst));
7.497 + map (fst o fst) accepts @
7.498 + (if remaining_max = 0 then
7.499 + game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
7.500 + else
7.501 + iter (j + 1) remaining_max threshold rel_const_tab'
7.502 + hopeless_rejects hopeful_rejects)
7.503 + end
7.504 + | relevant candidates rejects hopeless
7.505 + (((ax as (((_, loc), th), axiom_consts)), cached_weight)
7.506 + :: hopeful) =
7.507 + let
7.508 + val weight =
7.509 + case cached_weight of
7.510 + SOME w => w
7.511 + | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
7.512 +(* TODO: experiment
7.513 +val name = fst (fst (fst ax)) ()
7.514 +val _ = if String.isPrefix "lift.simps(3" name then
7.515 +tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
7.516 +else
7.517 +()
7.518 +*)
7.519 + in
7.520 + if weight >= threshold then
7.521 + relevant ((ax, weight) :: candidates) rejects hopeless hopeful
7.522 else
7.523 - (* Add "add:" facts. *)
7.524 - if null add_thms then
7.525 - []
7.526 - else
7.527 - map_filter (fn ((p as (_, th), _), _) =>
7.528 - if member Thm.eq_thm add_thms th then SOME p
7.529 - else NONE) rejects
7.530 - | relevant (new_pairs, rejects) [] =
7.531 - let
7.532 - val (new_rels, more_rejects) = take_best max_new new_pairs
7.533 - val rel_const_tab' =
7.534 - rel_const_tab |> fold add_const_to_table (maps snd new_rels)
7.535 - fun is_dirty c =
7.536 - const_mem rel_const_tab' c andalso
7.537 - not (const_mem rel_const_tab c)
7.538 - val rejects =
7.539 - more_rejects @ rejects
7.540 - |> map (fn (ax as (_, consts), old_weight) =>
7.541 - (ax, if exists is_dirty consts then NONE
7.542 - else SOME old_weight))
7.543 - val threshold =
7.544 - threshold + (1.0 - threshold) * relevance_convergence
7.545 - in
7.546 - trace_msg (fn () => "relevant this iteration: " ^
7.547 - Int.toString (length new_rels));
7.548 - map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
7.549 - end
7.550 - | relevant (new_rels, rejects)
7.551 - (((ax as ((name, th), axiom_consts)), cached_weight)
7.552 - :: rest) =
7.553 - let
7.554 - val weight =
7.555 - case cached_weight of
7.556 - SOME w => w
7.557 - | NONE => axiom_weight const_tab rel_const_tab axiom_consts
7.558 - in
7.559 - if weight >= threshold orelse
7.560 - (defs_relevant andalso defines thy th rel_const_tab) then
7.561 - (trace_msg (fn () =>
7.562 - fst (name ()) ^ " passes: " ^ Real.toString weight
7.563 - ^ " consts: " ^ commas (map fst axiom_consts));
7.564 - relevant ((ax, weight) :: new_rels, rejects) rest)
7.565 - else
7.566 - relevant (new_rels, (ax, weight) :: rejects) rest
7.567 - end
7.568 - in
7.569 - trace_msg (fn () => "relevant_facts, current threshold: " ^
7.570 - Real.toString threshold);
7.571 - relevant ([], [])
7.572 - end
7.573 - in
7.574 - axioms |> filter_out (member Thm.eq_thm del_thms o snd)
7.575 - |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
7.576 - |> iter 0 relevance_threshold goal_const_tab
7.577 - |> tap (fn res => trace_msg (fn () =>
7.578 + relevant candidates ((ax, weight) :: rejects) hopeless hopeful
7.579 + end
7.580 + in
7.581 + trace_msg (fn () =>
7.582 + "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
7.583 + Real.toString threshold ^ ", constants: " ^
7.584 + commas (rel_const_tab |> Symtab.dest
7.585 + |> filter (curry (op <>) [] o snd)
7.586 + |> map string_for_super_pseudoconst));
7.587 + relevant [] [] hopeless hopeful
7.588 + end
7.589 + in
7.590 + axioms |> filter_out (member Thm.eq_thm del_thms o snd)
7.591 + |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
7.592 + |> iter 0 max_relevant threshold0
7.593 + (get_pseudoconsts thy false (SOME false) goal_ts) []
7.594 + |> tap (fn res => trace_msg (fn () =>
7.595 "Total relevant: " ^ Int.toString (length res)))
7.596 - end
7.597 + end
7.598 +
7.599
7.600 (***************************************************************)
7.601 (* Retrieving and filtering lemmas *)
7.602 @@ -533,22 +583,24 @@
7.603
7.604 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
7.605 let
7.606 - val is_chained = member Thm.eq_thm chained_ths
7.607 - val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
7.608 + val thy = ProofContext.theory_of ctxt
7.609 + val thy_prefix = Context.theory_name thy ^ Long_Name.separator
7.610 + val global_facts = PureThy.facts_of thy
7.611 val local_facts = ProofContext.facts_of ctxt
7.612 val named_locals = local_facts |> Facts.dest_static []
7.613 + val is_chained = member Thm.eq_thm chained_ths
7.614 (* Unnamed, not chained formulas with schematic variables are omitted,
7.615 because they are rejected by the backticks (`...`) parser for some
7.616 reason. *)
7.617 - fun is_bad_unnamed_local th =
7.618 - exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
7.619 - (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
7.620 + fun is_good_unnamed_local th =
7.621 + forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
7.622 + andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
7.623 val unnamed_locals =
7.624 - local_facts |> Facts.props |> filter_out is_bad_unnamed_local
7.625 + local_facts |> Facts.props |> filter is_good_unnamed_local
7.626 |> map (pair "" o single)
7.627 val full_space =
7.628 - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
7.629 - fun add_valid_facts foldx facts =
7.630 + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
7.631 + fun add_facts global foldx facts =
7.632 foldx (fn (name0, ths) =>
7.633 if name0 <> "" andalso
7.634 forall (not o member Thm.eq_thm add_thms) ths andalso
7.635 @@ -559,10 +611,16 @@
7.636 I
7.637 else
7.638 let
7.639 + val base_loc =
7.640 + if not global then Local
7.641 + else if String.isPrefix thy_prefix name0 then Theory
7.642 + else General
7.643 val multi = length ths > 1
7.644 fun backquotify th =
7.645 "`" ^ Print_Mode.setmp [Print_Mode.input]
7.646 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
7.647 + |> String.translate (fn c => if Char.isPrint c then str c else "")
7.648 + |> simplify_spaces
7.649 fun check_thms a =
7.650 case try (ProofContext.get_thms ctxt) a of
7.651 NONE => false
7.652 @@ -575,54 +633,48 @@
7.653 not (member Thm.eq_thm add_thms th) then
7.654 rest
7.655 else
7.656 - (fn () =>
7.657 - (if name0 = "" then
7.658 - th |> backquotify
7.659 - else
7.660 - let
7.661 - val name1 = Facts.extern facts name0
7.662 - val name2 = Name_Space.extern full_space name0
7.663 - in
7.664 - case find_first check_thms [name1, name2, name0] of
7.665 - SOME name =>
7.666 - let
7.667 - val name =
7.668 - name |> Symtab.defined reserved name ? quote
7.669 - in
7.670 - if multi then name ^ "(" ^ Int.toString j ^ ")"
7.671 - else name
7.672 - end
7.673 - | NONE => ""
7.674 - end, is_chained th), (multi, th)) :: rest)) ths
7.675 + (((fn () =>
7.676 + if name0 = "" then
7.677 + th |> backquotify
7.678 + else
7.679 + let
7.680 + val name1 = Facts.extern facts name0
7.681 + val name2 = Name_Space.extern full_space name0
7.682 + in
7.683 + case find_first check_thms [name1, name2, name0] of
7.684 + SOME name => repair_name reserved multi j name
7.685 + | NONE => ""
7.686 + end), if is_chained th then Chained else base_loc),
7.687 + (multi, th)) :: rest)) ths
7.688 #> snd
7.689 end)
7.690 in
7.691 - [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
7.692 - |> add_valid_facts Facts.fold_static global_facts global_facts
7.693 + [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
7.694 + |> add_facts true Facts.fold_static global_facts global_facts
7.695 end
7.696
7.697 (* The single-name theorems go after the multiple-name ones, so that single
7.698 names are preferred when both are available. *)
7.699 fun name_thm_pairs ctxt respect_no_atp =
7.700 - List.partition (fst o snd) #> op @
7.701 - #> map (apsnd snd)
7.702 + List.partition (fst o snd) #> op @ #> map (apsnd snd)
7.703 #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
7.704
7.705 (***************************************************************)
7.706 (* ATP invocation methods setup *)
7.707 (***************************************************************)
7.708
7.709 -fun relevant_facts full_types relevance_threshold relevance_convergence
7.710 - defs_relevant max_new theory_relevant
7.711 - (relevance_override as {add, del, only})
7.712 +fun relevant_facts full_types (threshold0, threshold1) max_relevant
7.713 + theory_relevant (relevance_override as {add, del, only})
7.714 (ctxt, (chained_ths, _)) hyp_ts concl_t =
7.715 let
7.716 + val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
7.717 + 1.0 / Real.fromInt (max_relevant + 1))
7.718 val add_thms = maps (ProofContext.get_fact ctxt) add
7.719 val reserved = reserved_isar_keyword_table ()
7.720 val axioms =
7.721 (if only then
7.722 - maps ((fn (n, ths) => map (pair n o pair false) ths)
7.723 - o name_thms_pair_from_ref ctxt reserved chained_ths) add
7.724 + maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
7.725 + o name_thm_pairs_from_ref ctxt reserved chained_ths) add
7.726 else
7.727 all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
7.728 |> name_thm_pairs ctxt (respect_no_atp andalso not only)
7.729 @@ -630,11 +682,14 @@
7.730 in
7.731 trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
7.732 " theorems");
7.733 - relevance_filter ctxt relevance_threshold relevance_convergence
7.734 - defs_relevant max_new theory_relevant relevance_override
7.735 - axioms (concl_t :: hyp_ts)
7.736 - |> map (apfst (fn f => f ()))
7.737 - |> sort_wrt (fst o fst)
7.738 + (if threshold0 > 1.0 orelse threshold0 > threshold1 then
7.739 + []
7.740 + else if threshold0 < 0.0 then
7.741 + axioms
7.742 + else
7.743 + relevance_filter ctxt threshold0 decay max_relevant theory_relevant
7.744 + relevance_override axioms (concl_t :: hyp_ts))
7.745 + |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
7.746 end
7.747
7.748 end;
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Thu Aug 26 09:12:00 2010 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Thu Aug 26 10:42:22 2010 +0200
8.3 @@ -7,11 +7,12 @@
8.4
8.5 signature SLEDGEHAMMER_FACT_MINIMIZE =
8.6 sig
8.7 + type locality = Sledgehammer_Fact_Filter.locality
8.8 type params = Sledgehammer.params
8.9
8.10 val minimize_theorems :
8.11 - params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
8.12 - -> ((string * bool) * thm list) list option * string
8.13 + params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
8.14 + -> ((string * locality) * thm list) list option * string
8.15 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
8.16 end;
8.17
8.18 @@ -40,24 +41,20 @@
8.19 "")
8.20 end
8.21
8.22 -fun test_theorems ({debug, verbose, overlord, atps, full_types,
8.23 - relevance_threshold, relevance_convergence,
8.24 - defs_relevant, isar_proof, isar_shrink_factor, ...}
8.25 - : params)
8.26 +fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
8.27 + isar_shrink_factor, ...} : params)
8.28 (prover : prover) explicit_apply timeout subgoal state
8.29 - name_thms_pairs =
8.30 + axioms =
8.31 let
8.32 val _ =
8.33 - priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
8.34 + priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
8.35 val params =
8.36 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
8.37 full_types = full_types, explicit_apply = explicit_apply,
8.38 - relevance_threshold = relevance_threshold,
8.39 - relevance_convergence = relevance_convergence,
8.40 - max_relevant_per_iter = NONE, theory_relevant = NONE,
8.41 - defs_relevant = defs_relevant, isar_proof = isar_proof,
8.42 + relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
8.43 + theory_relevant = NONE, isar_proof = isar_proof,
8.44 isar_shrink_factor = isar_shrink_factor, timeout = timeout}
8.45 - val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
8.46 + val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
8.47 val {context = ctxt, facts, goal} = Proof.goal state
8.48 val problem =
8.49 {subgoal = subgoal, goal = (ctxt, (facts, goal)),
8.50 @@ -67,7 +64,7 @@
8.51 in
8.52 priority (case outcome of
8.53 NONE =>
8.54 - if length used_thm_names = length name_thms_pairs then
8.55 + if length used_thm_names = length axioms then
8.56 "Found proof."
8.57 else
8.58 "Found proof with " ^ n_theorems used_thm_names ^ "."
8.59 @@ -93,10 +90,9 @@
8.60 val fudge_msecs = 1000
8.61
8.62 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
8.63 - | minimize_theorems
8.64 - (params as {debug, atps = atp :: _, full_types, isar_proof,
8.65 - isar_shrink_factor, timeout, ...})
8.66 - i n state name_thms_pairs =
8.67 + | minimize_theorems (params as {debug, atps = atp :: _, full_types,
8.68 + isar_proof, isar_shrink_factor, timeout, ...})
8.69 + i n state axioms =
8.70 let
8.71 val thy = Proof.theory_of state
8.72 val prover = get_prover_fun thy atp
8.73 @@ -106,13 +102,12 @@
8.74 val (_, hyp_ts, concl_t) = strip_subgoal goal i
8.75 val explicit_apply =
8.76 not (forall (Meson.is_fol_term thy)
8.77 - (concl_t :: hyp_ts @
8.78 - maps (map prop_of o snd) name_thms_pairs))
8.79 + (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
8.80 fun do_test timeout =
8.81 test_theorems params prover explicit_apply timeout i state
8.82 val timer = Timer.startRealTimer ()
8.83 in
8.84 - (case do_test timeout name_thms_pairs of
8.85 + (case do_test timeout axioms of
8.86 result as {outcome = NONE, pool, used_thm_names,
8.87 conjecture_shape, ...} =>
8.88 let
8.89 @@ -122,11 +117,11 @@
8.90 |> Time.fromMilliseconds
8.91 val (min_thms, {proof, axiom_names, ...}) =
8.92 sublinear_minimize (do_test new_timeout)
8.93 - (filter_used_facts used_thm_names name_thms_pairs) ([], result)
8.94 + (filter_used_facts used_thm_names axioms) ([], result)
8.95 val n = length min_thms
8.96 val _ = priority (cat_lines
8.97 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
8.98 - (case length (filter (snd o fst) min_thms) of
8.99 + (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
8.100 0 => ""
8.101 | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
8.102 in
8.103 @@ -154,15 +149,14 @@
8.104 val ctxt = Proof.context_of state
8.105 val reserved = reserved_isar_keyword_table ()
8.106 val chained_ths = #facts (Proof.goal state)
8.107 - val name_thms_pairs =
8.108 - map (apfst (fn f => f ())
8.109 - o name_thms_pair_from_ref ctxt reserved chained_ths) refs
8.110 + val axioms =
8.111 + maps (map (apsnd single)
8.112 + o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
8.113 in
8.114 case subgoal_count state of
8.115 0 => priority "No subgoal!"
8.116 | n =>
8.117 - (kill_atps ();
8.118 - priority (#2 (minimize_theorems params i n state name_thms_pairs)))
8.119 + (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
8.120 end
8.121
8.122 end;
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 26 09:12:00 2010 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 26 10:42:22 2010 +0200
9.3 @@ -67,11 +67,9 @@
9.4 ("verbose", "false"),
9.5 ("overlord", "false"),
9.6 ("explicit_apply", "false"),
9.7 - ("relevance_threshold", "40"),
9.8 - ("relevance_convergence", "31"),
9.9 - ("max_relevant_per_iter", "smart"),
9.10 + ("relevance_thresholds", "45 95"),
9.11 + ("max_relevant", "smart"),
9.12 ("theory_relevant", "smart"),
9.13 - ("defs_relevant", "false"),
9.14 ("isar_proof", "false"),
9.15 ("isar_shrink_factor", "1")]
9.16
9.17 @@ -84,7 +82,6 @@
9.18 ("partial_types", "full_types"),
9.19 ("implicit_apply", "explicit_apply"),
9.20 ("theory_irrelevant", "theory_relevant"),
9.21 - ("defs_irrelevant", "defs_relevant"),
9.22 ("no_isar_proof", "isar_proof")]
9.23
9.24 val params_for_minimize =
9.25 @@ -158,6 +155,14 @@
9.26 SOME n => n
9.27 | NONE => error ("Parameter " ^ quote name ^
9.28 " must be assigned an integer value.")
9.29 + fun lookup_int_pair name =
9.30 + case lookup name of
9.31 + NONE => (0, 0)
9.32 + | SOME s => case s |> space_explode " " |> map Int.fromString of
9.33 + [SOME n1, SOME n2] => (n1, n2)
9.34 + | _ => error ("Parameter " ^ quote name ^
9.35 + "must be assigned a pair of integer values \
9.36 + \(e.g., \"60 95\")")
9.37 fun lookup_int_option name =
9.38 case lookup name of
9.39 SOME "smart" => NONE
9.40 @@ -168,25 +173,20 @@
9.41 val atps = lookup_string "atps" |> space_explode " "
9.42 val full_types = lookup_bool "full_types"
9.43 val explicit_apply = lookup_bool "explicit_apply"
9.44 - val relevance_threshold =
9.45 - 0.01 * Real.fromInt (lookup_int "relevance_threshold")
9.46 - val relevance_convergence =
9.47 - 0.01 * Real.fromInt (lookup_int "relevance_convergence")
9.48 - val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
9.49 + val relevance_thresholds =
9.50 + lookup_int_pair "relevance_thresholds"
9.51 + |> pairself (fn n => 0.01 * Real.fromInt n)
9.52 + val max_relevant = lookup_int_option "max_relevant"
9.53 val theory_relevant = lookup_bool_option "theory_relevant"
9.54 - val defs_relevant = lookup_bool "defs_relevant"
9.55 val isar_proof = lookup_bool "isar_proof"
9.56 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
9.57 val timeout = lookup_time "timeout"
9.58 in
9.59 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
9.60 full_types = full_types, explicit_apply = explicit_apply,
9.61 - relevance_threshold = relevance_threshold,
9.62 - relevance_convergence = relevance_convergence,
9.63 - max_relevant_per_iter = max_relevant_per_iter,
9.64 - theory_relevant = theory_relevant, defs_relevant = defs_relevant,
9.65 - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
9.66 - timeout = timeout}
9.67 + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
9.68 + theory_relevant = theory_relevant, isar_proof = isar_proof,
9.69 + isar_shrink_factor = isar_shrink_factor, timeout = timeout}
9.70 end
9.71
9.72 fun get_params thy = extract_params (default_raw_params thy)
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 09:12:00 2010 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 10:42:22 2010 +0200
10.3 @@ -8,19 +8,20 @@
10.4
10.5 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
10.6 sig
10.7 + type locality = Sledgehammer_Fact_Filter.locality
10.8 type minimize_command = string list -> string
10.9
10.10 val metis_proof_text:
10.11 - bool * minimize_command * string * (string * bool) vector * thm * int
10.12 - -> string * (string * bool) list
10.13 + bool * minimize_command * string * (string * locality) vector * thm * int
10.14 + -> string * (string * locality) list
10.15 val isar_proof_text:
10.16 string Symtab.table * bool * int * Proof.context * int list list
10.17 - -> bool * minimize_command * string * (string * bool) vector * thm * int
10.18 - -> string * (string * bool) list
10.19 + -> bool * minimize_command * string * (string * locality) vector * thm * int
10.20 + -> string * (string * locality) list
10.21 val proof_text:
10.22 bool -> string Symtab.table * bool * int * Proof.context * int list list
10.23 - -> bool * minimize_command * string * (string * bool) vector * thm * int
10.24 - -> string * (string * bool) list
10.25 + -> bool * minimize_command * string * (string * locality) vector * thm * int
10.26 + -> string * (string * locality) list
10.27 end;
10.28
10.29 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
10.30 @@ -234,7 +235,7 @@
10.31 fst o Scan.finite Symbol.stopper
10.32 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
10.33 (parse_lines pool)))
10.34 - o explode o strip_spaces
10.35 + o explode o strip_spaces_except_between_ident_chars
10.36
10.37 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
10.38
10.39 @@ -246,18 +247,18 @@
10.40 constrained by information from type literals, or by type inference. *)
10.41 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
10.42 let val Ts = map (type_from_fo_term tfrees) us in
10.43 - case strip_prefix_and_undo_ascii type_const_prefix a of
10.44 + case strip_prefix_and_unascii type_const_prefix a of
10.45 SOME b => Type (invert_const b, Ts)
10.46 | NONE =>
10.47 if not (null us) then
10.48 raise FO_TERM [u] (* only "tconst"s have type arguments *)
10.49 - else case strip_prefix_and_undo_ascii tfree_prefix a of
10.50 + else case strip_prefix_and_unascii tfree_prefix a of
10.51 SOME b =>
10.52 let val s = "'" ^ b in
10.53 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
10.54 end
10.55 | NONE =>
10.56 - case strip_prefix_and_undo_ascii tvar_prefix a of
10.57 + case strip_prefix_and_unascii tvar_prefix a of
10.58 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
10.59 | NONE =>
10.60 (* Variable from the ATP, say "X1" *)
10.61 @@ -267,7 +268,7 @@
10.62 (* Type class literal applied to a type. Returns triple of polarity, class,
10.63 type. *)
10.64 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
10.65 - case (strip_prefix_and_undo_ascii class_prefix a,
10.66 + case (strip_prefix_and_unascii class_prefix a,
10.67 map (type_from_fo_term tfrees) us) of
10.68 (SOME b, [T]) => (pos, b, T)
10.69 | _ => raise FO_TERM [u]
10.70 @@ -309,7 +310,7 @@
10.71 [typ_u, term_u] =>
10.72 aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
10.73 | _ => raise FO_TERM us
10.74 - else case strip_prefix_and_undo_ascii const_prefix a of
10.75 + else case strip_prefix_and_unascii const_prefix a of
10.76 SOME "equal" =>
10.77 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
10.78 map (aux NONE []) us)
10.79 @@ -341,10 +342,10 @@
10.80 val ts = map (aux NONE []) (us @ extra_us)
10.81 val T = map fastype_of ts ---> HOLogic.typeT
10.82 val t =
10.83 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
10.84 + case strip_prefix_and_unascii fixed_var_prefix a of
10.85 SOME b => Free (b, T)
10.86 | NONE =>
10.87 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
10.88 + case strip_prefix_and_unascii schematic_var_prefix a of
10.89 SOME b => Var ((b, 0), T)
10.90 | NONE =>
10.91 if is_tptp_variable a then
10.92 @@ -575,10 +576,10 @@
10.93 String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
10.94 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
10.95 if tag = "cnf" orelse tag = "fof" then
10.96 - (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
10.97 + (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
10.98 SOME name =>
10.99 if member (op =) rest "file" then
10.100 - SOME (name, is_true_for axiom_names name)
10.101 + SOME (name, find_first_in_vector axiom_names name General)
10.102 else
10.103 axiom_name_at_index num
10.104 | NONE => axiom_name_at_index num)
10.105 @@ -624,8 +625,8 @@
10.106
10.107 fun used_facts axiom_names =
10.108 used_facts_in_atp_proof axiom_names
10.109 - #> List.partition snd
10.110 - #> pairself (sort_distinct (string_ord) o map fst)
10.111 + #> List.partition (curry (op =) Chained o snd)
10.112 + #> pairself (sort_distinct (string_ord o pairself fst))
10.113
10.114 fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
10.115 goal, i) =
10.116 @@ -633,9 +634,9 @@
10.117 val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
10.118 val n = Logic.count_prems (prop_of goal)
10.119 in
10.120 - (metis_line full_types i n other_lemmas ^
10.121 - minimize_line minimize_command (other_lemmas @ chained_lemmas),
10.122 - map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
10.123 + (metis_line full_types i n (map fst other_lemmas) ^
10.124 + minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
10.125 + other_lemmas @ chained_lemmas)
10.126 end
10.127
10.128 (** Isar proof construction and manipulation **)
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 09:12:00 2010 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 10:42:22 2010 +0200
11.3 @@ -18,8 +18,8 @@
11.4 val tfrees_name : string
11.5 val prepare_problem :
11.6 Proof.context -> bool -> bool -> bool -> bool -> term list -> term
11.7 - -> ((string * bool) * thm) list
11.8 - -> string problem * string Symtab.table * int * (string * bool) vector
11.9 + -> ((string * 'a) * thm) list
11.10 + -> string problem * string Symtab.table * int * (string * 'a) vector
11.11 end;
11.12
11.13 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
11.14 @@ -39,11 +39,11 @@
11.15 (* Freshness almost guaranteed! *)
11.16 val sledgehammer_weak_prefix = "Sledgehammer:"
11.17
11.18 -datatype fol_formula =
11.19 - FOLFormula of {name: string,
11.20 - kind: kind,
11.21 - combformula: (name, combterm) formula,
11.22 - ctypes_sorts: typ list}
11.23 +type fol_formula =
11.24 + {name: string,
11.25 + kind: kind,
11.26 + combformula: (name, combterm) formula,
11.27 + ctypes_sorts: typ list}
11.28
11.29 fun mk_anot phi = AConn (ANot, [phi])
11.30 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
11.31 @@ -190,15 +190,14 @@
11.32 |> kind <> Axiom ? freeze_term
11.33 val (combformula, ctypes_sorts) = combformula_for_prop thy t []
11.34 in
11.35 - FOLFormula {name = name, combformula = combformula, kind = kind,
11.36 - ctypes_sorts = ctypes_sorts}
11.37 + {name = name, combformula = combformula, kind = kind,
11.38 + ctypes_sorts = ctypes_sorts}
11.39 end
11.40
11.41 -fun make_axiom ctxt presimp ((name, chained), th) =
11.42 +fun make_axiom ctxt presimp ((name, loc), th) =
11.43 case make_formula ctxt presimp name Axiom (prop_of th) of
11.44 - FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
11.45 - NONE
11.46 - | formula => SOME ((name, chained), formula)
11.47 + {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
11.48 + | formula => SOME ((name, loc), formula)
11.49 fun make_conjecture ctxt ts =
11.50 let val last = length ts - 1 in
11.51 map2 (fn j => make_formula ctxt true (Int.toString j)
11.52 @@ -215,7 +214,7 @@
11.53 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
11.54 | count_combformula (AConn (_, phis)) = fold count_combformula phis
11.55 | count_combformula (AAtom tm) = count_combterm tm
11.56 -fun count_fol_formula (FOLFormula {combformula, ...}) =
11.57 +fun count_fol_formula ({combformula, ...} : fol_formula) =
11.58 count_combformula combformula
11.59
11.60 val optional_helpers =
11.61 @@ -326,13 +325,13 @@
11.62 | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
11.63 in aux end
11.64
11.65 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
11.66 +fun formula_for_axiom full_types
11.67 + ({combformula, ctypes_sorts, ...} : fol_formula) =
11.68 mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
11.69 (type_literals_for_types ctypes_sorts))
11.70 (formula_for_combformula full_types combformula)
11.71
11.72 -fun problem_line_for_fact prefix full_types
11.73 - (formula as FOLFormula {name, kind, ...}) =
11.74 +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
11.75 Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
11.76
11.77 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
11.78 @@ -357,11 +356,11 @@
11.79 (fo_literal_for_arity_literal conclLit)))
11.80
11.81 fun problem_line_for_conjecture full_types
11.82 - (FOLFormula {name, kind, combformula, ...}) =
11.83 + ({name, kind, combformula, ...} : fol_formula) =
11.84 Fof (conjecture_prefix ^ name, kind,
11.85 formula_for_combformula full_types combformula)
11.86
11.87 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
11.88 +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
11.89 map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
11.90
11.91 fun problem_line_for_free_type lit =
11.92 @@ -407,7 +406,7 @@
11.93 16383 (* large number *)
11.94 else if full_types then
11.95 0
11.96 - else case strip_prefix_and_undo_ascii const_prefix s of
11.97 + else case strip_prefix_and_unascii const_prefix s of
11.98 SOME s' => num_type_args thy (invert_const s')
11.99 | NONE => 0)
11.100 | min_arity_of _ _ (SOME the_const_tab) s =
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 09:12:00 2010 +0200
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 10:42:22 2010 +0200
12.3 @@ -6,10 +6,11 @@
12.4
12.5 signature SLEDGEHAMMER_UTIL =
12.6 sig
12.7 - val is_true_for : (string * bool) vector -> string -> bool
12.8 + val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
12.9 val plural_s : int -> string
12.10 val serial_commas : string -> string list -> string list
12.11 - val strip_spaces : string -> string
12.12 + val simplify_spaces : string -> string
12.13 + val strip_spaces_except_between_ident_chars : string -> string
12.14 val parse_bool_option : bool -> string -> string -> bool option
12.15 val parse_time_option : string -> string -> Time.time option
12.16 val scan_integer : string list -> int * string list
12.17 @@ -28,8 +29,9 @@
12.18 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
12.19 struct
12.20
12.21 -fun is_true_for v s =
12.22 - Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
12.23 +fun find_first_in_vector vec key default =
12.24 + Vector.foldl (fn ((key', value'), value) =>
12.25 + if key' = key then value' else value) default vec
12.26
12.27 fun plural_s n = if n = 1 then "" else "s"
12.28
12.29 @@ -39,24 +41,27 @@
12.30 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
12.31 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
12.32
12.33 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
12.34 -
12.35 -fun strip_spaces_in_list [] = ""
12.36 - | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
12.37 - | strip_spaces_in_list [c1, c2] =
12.38 - strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
12.39 - | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
12.40 +fun strip_spaces_in_list _ [] = ""
12.41 + | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
12.42 + | strip_spaces_in_list is_evil [c1, c2] =
12.43 + strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
12.44 + | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
12.45 if Char.isSpace c1 then
12.46 - strip_spaces_in_list (c2 :: c3 :: cs)
12.47 + strip_spaces_in_list is_evil (c2 :: c3 :: cs)
12.48 else if Char.isSpace c2 then
12.49 if Char.isSpace c3 then
12.50 - strip_spaces_in_list (c1 :: c3 :: cs)
12.51 + strip_spaces_in_list is_evil (c1 :: c3 :: cs)
12.52 else
12.53 - str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
12.54 - strip_spaces_in_list (c3 :: cs)
12.55 + str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
12.56 + strip_spaces_in_list is_evil (c3 :: cs)
12.57 else
12.58 - str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
12.59 -val strip_spaces = strip_spaces_in_list o String.explode
12.60 + str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
12.61 +fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
12.62 +
12.63 +val simplify_spaces = strip_spaces (K true)
12.64 +
12.65 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
12.66 +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
12.67
12.68 fun parse_bool_option option name s =
12.69 (case s of