1.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 00:49:04 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 00:49:38 2010 +0200
1.3 @@ -38,11 +38,10 @@
1.4 val const_prefix: string
1.5 val type_const_prefix: string
1.6 val class_prefix: string
1.7 - val union_all: ''a list list -> ''a list
1.8 val invert_const: string -> string
1.9 val ascii_of: string -> string
1.10 - val undo_ascii_of: string -> string
1.11 - val strip_prefix_and_undo_ascii: string -> string -> string option
1.12 + val unascii_of: string -> string
1.13 + val strip_prefix_and_unascii: string -> string -> string option
1.14 val make_bound_var : string -> string
1.15 val make_schematic_var : string * int -> string
1.16 val make_fixed_var : string -> string
1.17 @@ -140,29 +139,28 @@
1.18
1.19 (*We don't raise error exceptions because this code can run inside the watcher.
1.20 Also, the errors are "impossible" (hah!)*)
1.21 -fun undo_ascii_aux rcs [] = String.implode(rev rcs)
1.22 - | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
1.23 +fun unascii_aux rcs [] = String.implode(rev rcs)
1.24 + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
1.25 (*Three types of _ escapes: __, _A to _P, _nnn*)
1.26 - | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
1.27 - | undo_ascii_aux rcs (#"_" :: c :: cs) =
1.28 + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
1.29 + | unascii_aux rcs (#"_" :: c :: cs) =
1.30 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
1.31 - then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
1.32 + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
1.33 else
1.34 let val digits = List.take (c::cs, 3) handle Subscript => []
1.35 in
1.36 case Int.fromString (String.implode digits) of
1.37 - NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
1.38 - | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
1.39 + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
1.40 + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
1.41 end
1.42 - | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
1.43 -
1.44 -val undo_ascii_of = undo_ascii_aux [] o String.explode;
1.45 + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
1.46 +val unascii_of = unascii_aux [] o String.explode
1.47
1.48 (* If string s has the prefix s1, return the result of deleting it,
1.49 un-ASCII'd. *)
1.50 -fun strip_prefix_and_undo_ascii s1 s =
1.51 +fun strip_prefix_and_unascii s1 s =
1.52 if String.isPrefix s1 s then
1.53 - SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
1.54 + SOME (unascii_of (String.extract (s, size s1, NONE)))
1.55 else
1.56 NONE
1.57
1.58 @@ -512,8 +510,8 @@
1.59 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1.60 fun add_type_consts_in_term thy =
1.61 let
1.62 - val const_typargs = Sign.const_typargs thy
1.63 - fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
1.64 + fun aux (Const x) =
1.65 + fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
1.66 | aux (Abs (_, _, u)) = aux u
1.67 | aux (Const (@{const_name skolem_id}, _) $ _) = I
1.68 | aux (t $ u) = aux t #> aux u
2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 00:49:04 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 00:49:38 2010 +0200
2.3 @@ -228,15 +228,15 @@
2.4 | smart_invert_const s = invert_const s
2.5
2.6 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
2.7 - (case strip_prefix_and_undo_ascii tvar_prefix v of
2.8 + (case strip_prefix_and_unascii tvar_prefix v of
2.9 SOME w => make_tvar w
2.10 | NONE => make_tvar v)
2.11 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
2.12 - (case strip_prefix_and_undo_ascii type_const_prefix x of
2.13 + (case strip_prefix_and_unascii type_const_prefix x of
2.14 SOME tc => Term.Type (smart_invert_const tc,
2.15 map (hol_type_from_metis_term ctxt) tys)
2.16 | NONE =>
2.17 - case strip_prefix_and_undo_ascii tfree_prefix x of
2.18 + case strip_prefix_and_unascii tfree_prefix x of
2.19 SOME tf => mk_tfree ctxt tf
2.20 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
2.21
2.22 @@ -246,10 +246,10 @@
2.23 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
2.24 Metis.Term.toString fol_tm)
2.25 fun tm_to_tt (Metis.Term.Var v) =
2.26 - (case strip_prefix_and_undo_ascii tvar_prefix v of
2.27 + (case strip_prefix_and_unascii tvar_prefix v of
2.28 SOME w => Type (make_tvar w)
2.29 | NONE =>
2.30 - case strip_prefix_and_undo_ascii schematic_var_prefix v of
2.31 + case strip_prefix_and_unascii schematic_var_prefix v of
2.32 SOME w => Term (mk_var (w, HOLogic.typeT))
2.33 | NONE => Term (mk_var (v, HOLogic.typeT)) )
2.34 (*Var from Metis with a name like _nnn; possibly a type variable*)
2.35 @@ -266,7 +266,7 @@
2.36 and applic_to_tt ("=",ts) =
2.37 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
2.38 | applic_to_tt (a,ts) =
2.39 - case strip_prefix_and_undo_ascii const_prefix a of
2.40 + case strip_prefix_and_unascii const_prefix a of
2.41 SOME b =>
2.42 let val c = smart_invert_const b
2.43 val ntypes = num_type_args thy c
2.44 @@ -284,14 +284,14 @@
2.45 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
2.46 end
2.47 | NONE => (*Not a constant. Is it a type constructor?*)
2.48 - case strip_prefix_and_undo_ascii type_const_prefix a of
2.49 + case strip_prefix_and_unascii type_const_prefix a of
2.50 SOME b =>
2.51 Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
2.52 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
2.53 - case strip_prefix_and_undo_ascii tfree_prefix a of
2.54 + case strip_prefix_and_unascii tfree_prefix a of
2.55 SOME b => Type (mk_tfree ctxt b)
2.56 | NONE => (*a fixed variable? They are Skolem functions.*)
2.57 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
2.58 + case strip_prefix_and_unascii fixed_var_prefix a of
2.59 SOME b =>
2.60 let val opr = Term.Free(b, HOLogic.typeT)
2.61 in apply_list opr (length ts) (map tm_to_tt ts) end
2.62 @@ -307,16 +307,16 @@
2.63 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
2.64 Metis.Term.toString fol_tm)
2.65 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
2.66 - (case strip_prefix_and_undo_ascii schematic_var_prefix v of
2.67 + (case strip_prefix_and_unascii schematic_var_prefix v of
2.68 SOME w => mk_var(w, dummyT)
2.69 | NONE => mk_var(v, dummyT))
2.70 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
2.71 Const (@{const_name "op ="}, HOLogic.typeT)
2.72 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
2.73 - (case strip_prefix_and_undo_ascii const_prefix x of
2.74 + (case strip_prefix_and_unascii const_prefix x of
2.75 SOME c => Const (smart_invert_const c, dummyT)
2.76 | NONE => (*Not a constant. Is it a fixed variable??*)
2.77 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
2.78 + case strip_prefix_and_unascii fixed_var_prefix x of
2.79 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
2.80 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
2.81 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
2.82 @@ -327,10 +327,10 @@
2.83 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
2.84 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
2.85 | cvt (t as Metis.Term.Fn (x, [])) =
2.86 - (case strip_prefix_and_undo_ascii const_prefix x of
2.87 + (case strip_prefix_and_unascii const_prefix x of
2.88 SOME c => Const (smart_invert_const c, dummyT)
2.89 | NONE => (*Not a constant. Is it a fixed variable??*)
2.90 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
2.91 + case strip_prefix_and_unascii fixed_var_prefix x of
2.92 SOME v => Free (v, dummyT)
2.93 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
2.94 hol_term_from_metis_PT ctxt t))
2.95 @@ -410,11 +410,11 @@
2.96 " in " ^ Display.string_of_thm ctxt i_th);
2.97 NONE)
2.98 fun remove_typeinst (a, t) =
2.99 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
2.100 + case strip_prefix_and_unascii schematic_var_prefix a of
2.101 SOME b => SOME (b, t)
2.102 - | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
2.103 + | NONE => case strip_prefix_and_unascii tvar_prefix a of
2.104 SOME _ => NONE (*type instantiations are forbidden!*)
2.105 - | NONE => SOME (a,t) (*internal Metis var?*)
2.106 + | NONE => SOME (a,t) (*internal Metis var?*)
2.107 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
2.108 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
2.109 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 00:49:04 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 00:49:38 2010 +0200
3.3 @@ -191,9 +191,8 @@
3.4 fun name_for_number j =
3.5 let
3.6 val axioms =
3.7 - j |> AList.lookup (op =) name_map
3.8 - |> these |> map_filter (try (unprefix axiom_prefix))
3.9 - |> map undo_ascii_of
3.10 + j |> AList.lookup (op =) name_map |> these
3.11 + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
3.12 val chained = forall (is_true_for axiom_names) axioms
3.13 in (axioms |> space_implode " ", chained) end
3.14 in
3.15 @@ -296,8 +295,6 @@
3.16 extract_proof_and_outcome complete res_code proof_delims
3.17 known_failures output
3.18 in (output, msecs, proof, outcome) end
3.19 - val _ = print_d (fn () => "Preparing problem for " ^
3.20 - quote atp_name ^ "...")
3.21 val readable_names = debug andalso overlord
3.22 val (problem, pool, conjecture_offset, axiom_names) =
3.23 prepare_problem ctxt readable_names explicit_forall full_types
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:04 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:38 2010 +0200
4.3 @@ -246,18 +246,18 @@
4.4 constrained by information from type literals, or by type inference. *)
4.5 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
4.6 let val Ts = map (type_from_fo_term tfrees) us in
4.7 - case strip_prefix_and_undo_ascii type_const_prefix a of
4.8 + case strip_prefix_and_unascii type_const_prefix a of
4.9 SOME b => Type (invert_const b, Ts)
4.10 | NONE =>
4.11 if not (null us) then
4.12 raise FO_TERM [u] (* only "tconst"s have type arguments *)
4.13 - else case strip_prefix_and_undo_ascii tfree_prefix a of
4.14 + else case strip_prefix_and_unascii tfree_prefix a of
4.15 SOME b =>
4.16 let val s = "'" ^ b in
4.17 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
4.18 end
4.19 | NONE =>
4.20 - case strip_prefix_and_undo_ascii tvar_prefix a of
4.21 + case strip_prefix_and_unascii tvar_prefix a of
4.22 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
4.23 | NONE =>
4.24 (* Variable from the ATP, say "X1" *)
4.25 @@ -267,7 +267,7 @@
4.26 (* Type class literal applied to a type. Returns triple of polarity, class,
4.27 type. *)
4.28 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
4.29 - case (strip_prefix_and_undo_ascii class_prefix a,
4.30 + case (strip_prefix_and_unascii class_prefix a,
4.31 map (type_from_fo_term tfrees) us) of
4.32 (SOME b, [T]) => (pos, b, T)
4.33 | _ => raise FO_TERM [u]
4.34 @@ -309,7 +309,7 @@
4.35 [typ_u, term_u] =>
4.36 aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
4.37 | _ => raise FO_TERM us
4.38 - else case strip_prefix_and_undo_ascii const_prefix a of
4.39 + else case strip_prefix_and_unascii const_prefix a of
4.40 SOME "equal" =>
4.41 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
4.42 map (aux NONE []) us)
4.43 @@ -341,10 +341,10 @@
4.44 val ts = map (aux NONE []) (us @ extra_us)
4.45 val T = map fastype_of ts ---> HOLogic.typeT
4.46 val t =
4.47 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
4.48 + case strip_prefix_and_unascii fixed_var_prefix a of
4.49 SOME b => Free (b, T)
4.50 | NONE =>
4.51 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
4.52 + case strip_prefix_and_unascii schematic_var_prefix a of
4.53 SOME b => Var ((b, 0), T)
4.54 | NONE =>
4.55 if is_tptp_variable a then
4.56 @@ -575,7 +575,7 @@
4.57 String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
4.58 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
4.59 if tag = "cnf" orelse tag = "fof" then
4.60 - (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
4.61 + (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
4.62 SOME name =>
4.63 if member (op =) rest "file" then
4.64 SOME (name, is_true_for axiom_names name)
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 00:49:04 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 00:49:38 2010 +0200
5.3 @@ -407,7 +407,7 @@
5.4 16383 (* large number *)
5.5 else if full_types then
5.6 0
5.7 - else case strip_prefix_and_undo_ascii const_prefix s of
5.8 + else case strip_prefix_and_unascii const_prefix s of
5.9 SOME s' => num_type_args thy (invert_const s')
5.10 | NONE => 0)
5.11 | min_arity_of _ _ (SOME the_const_tab) s =