# HG changeset patch # User blanchet # Date 1282776578 -7200 # Node ID 69fea359d3f8cf24bf68ac601eb6fe02c1775ebb # Parent b264ae66cede2f635fd8ee85e6b9b9ae4ea8a650 renaming diff -r b264ae66cede -r 69fea359d3f8 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- 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 diff -r b264ae66cede -r 69fea359d3f8 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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) diff -r b264ae66cede -r 69fea359d3f8 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r b264ae66cede -r 69fea359d3f8 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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) diff -r b264ae66cede -r 69fea359d3f8 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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 =