--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 00:49:38 2010 +0200
@@ -38,11 +38,10 @@
val const_prefix: string
val type_const_prefix: string
val class_prefix: string
- val union_all: ''a list list -> ''a list
val invert_const: string -> string
val ascii_of: string -> string
- val undo_ascii_of: string -> string
- val strip_prefix_and_undo_ascii: string -> string -> string option
+ 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
@@ -140,29 +139,28 @@
(*We don't raise error exceptions because this code can run inside the watcher.
Also, the errors are "impossible" (hah!)*)
-fun undo_ascii_aux rcs [] = String.implode(rev rcs)
- | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
+fun unascii_aux rcs [] = String.implode(rev rcs)
+ | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
(*Three types of _ escapes: __, _A to _P, _nnn*)
- | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
- | undo_ascii_aux rcs (#"_" :: c :: cs) =
+ | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
+ | unascii_aux rcs (#"_" :: c :: cs) =
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
- then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
+ 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 => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
- | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
+ NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
+ | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
end
- | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
-
-val undo_ascii_of = undo_ascii_aux [] o String.explode;
+ | 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_undo_ascii s1 s =
+fun strip_prefix_and_unascii s1 s =
if String.isPrefix s1 s then
- SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
+ SOME (unascii_of (String.extract (s, size s1, NONE)))
else
NONE
@@ -512,8 +510,8 @@
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
fun add_type_consts_in_term thy =
let
- val const_typargs = Sign.const_typargs thy
- fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
+ fun aux (Const x) =
+ fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
| aux (Abs (_, _, u)) = aux u
| aux (Const (@{const_name skolem_id}, _) $ _) = I
| aux (t $ u) = aux t #> aux u
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 00:49:38 2010 +0200
@@ -228,15 +228,15 @@
| smart_invert_const s = invert_const s
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
- (case strip_prefix_and_undo_ascii tvar_prefix v of
+ (case strip_prefix_and_unascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
- (case strip_prefix_and_undo_ascii type_const_prefix x of
+ (case strip_prefix_and_unascii type_const_prefix x of
SOME tc => Term.Type (smart_invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
- case strip_prefix_and_undo_ascii tfree_prefix x of
+ case strip_prefix_and_unascii tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
@@ -246,10 +246,10 @@
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case strip_prefix_and_undo_ascii tvar_prefix v of
+ (case strip_prefix_and_unascii tvar_prefix v of
SOME w => Type (make_tvar w)
| NONE =>
- case strip_prefix_and_undo_ascii schematic_var_prefix v of
+ case strip_prefix_and_unascii schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -266,7 +266,7 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case strip_prefix_and_undo_ascii const_prefix a of
+ case strip_prefix_and_unascii const_prefix a of
SOME b =>
let val c = smart_invert_const b
val ntypes = num_type_args thy c
@@ -284,14 +284,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix_and_undo_ascii type_const_prefix a of
+ case strip_prefix_and_unascii type_const_prefix a of
SOME b =>
Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix_and_undo_ascii tfree_prefix a of
+ case strip_prefix_and_unascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix_and_undo_ascii fixed_var_prefix a of
+ case strip_prefix_and_unascii fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -307,16 +307,16 @@
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case strip_prefix_and_undo_ascii schematic_var_prefix v of
+ (case strip_prefix_and_unascii schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case strip_prefix_and_undo_ascii const_prefix x of
+ (case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_undo_ascii fixed_var_prefix x of
+ case strip_prefix_and_unascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -327,10 +327,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case strip_prefix_and_undo_ascii const_prefix x of
+ (case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_undo_ascii fixed_var_prefix x of
+ case strip_prefix_and_unascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
hol_term_from_metis_PT ctxt t))
@@ -410,11 +410,11 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case strip_prefix_and_undo_ascii schematic_var_prefix a of
+ case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
+ | NONE => case strip_prefix_and_unascii tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
- | NONE => SOME (a,t) (*internal Metis var?*)
+ | NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 00:49:38 2010 +0200
@@ -191,9 +191,8 @@
fun name_for_number j =
let
val axioms =
- j |> AList.lookup (op =) name_map
- |> these |> map_filter (try (unprefix axiom_prefix))
- |> map undo_ascii_of
+ j |> AList.lookup (op =) name_map |> these
+ |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
val chained = forall (is_true_for axiom_names) axioms
in (axioms |> space_implode " ", chained) end
in
@@ -296,8 +295,6 @@
extract_proof_and_outcome complete res_code proof_delims
known_failures output
in (output, msecs, proof, outcome) end
- val _ = print_d (fn () => "Preparing problem for " ^
- quote atp_name ^ "...")
val readable_names = debug andalso overlord
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:38 2010 +0200
@@ -246,18 +246,18 @@
constrained by information from type literals, or by type inference. *)
fun type_from_fo_term tfrees (u as ATerm (a, us)) =
let val Ts = map (type_from_fo_term tfrees) us in
- case strip_prefix_and_undo_ascii type_const_prefix a of
+ 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_undo_ascii tfree_prefix a of
+ 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_undo_ascii tvar_prefix a of
+ case strip_prefix_and_unascii tvar_prefix a of
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
(* Variable from the ATP, say "X1" *)
@@ -267,7 +267,7 @@
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
- case (strip_prefix_and_undo_ascii class_prefix a,
+ case (strip_prefix_and_unascii class_prefix a,
map (type_from_fo_term tfrees) us) of
(SOME b, [T]) => (pos, b, T)
| _ => raise FO_TERM [u]
@@ -309,7 +309,7 @@
[typ_u, term_u] =>
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
| _ => raise FO_TERM us
- else case strip_prefix_and_undo_ascii const_prefix a of
+ else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
map (aux NONE []) us)
@@ -341,10 +341,10 @@
val ts = map (aux NONE []) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_undo_ascii fixed_var_prefix a of
+ case strip_prefix_and_unascii fixed_var_prefix a of
SOME b => Free (b, T)
| NONE =>
- case strip_prefix_and_undo_ascii schematic_var_prefix a of
+ case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
@@ -575,7 +575,7 @@
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
if tag = "cnf" orelse tag = "fof" then
- (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
SOME name =>
if member (op =) rest "file" then
SOME (name, is_true_for axiom_names name)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 00:49:38 2010 +0200
@@ -407,7 +407,7 @@
16383 (* large number *)
else if full_types then
0
- else case strip_prefix_and_undo_ascii const_prefix s of
+ else case strip_prefix_and_unascii const_prefix s of
SOME s' => num_type_args thy (invert_const s')
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =