if "monomorphize" is enabled, mangle the type information in the names by default
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Apr 04 18:53:35 2011 +0200
@@ -123,6 +123,16 @@
fun pool_map f xs =
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+val no_qualifiers =
+ let
+ fun skip [] = []
+ | skip (#"." :: cs) = skip cs
+ | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs
+ and keep [] = []
+ | keep (#"." :: cs) = skip cs
+ | keep (c :: cs) = c :: keep cs
+ in String.explode #> rev #> keep #> rev #> String.implode end
+
(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
that "HOL.eq" is correctly mapped to equality. *)
@@ -132,7 +142,7 @@
s
else
let
- val s = s |> Long_Name.base_name
+ val s = s |> no_qualifiers
|> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
in if member (op =) reserved_nice_names s then full_name else s end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon Apr 04 18:53:35 2011 +0200
@@ -345,23 +345,23 @@
end
| SOME b =>
let
- val c = invert_const b
+ val (c, mangled_us) = b |> unmangled_const |>> invert_const
val num_ty_args = num_atp_type_args thy type_sys c
- val (type_us, term_us) = chop num_ty_args us
+ val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
(* Extra args from "hAPP" come after any arguments given directly to
the constant. *)
val term_ts = map (aux NONE []) term_us
val extra_ts = map (aux NONE []) extra_us
- val t =
- Const (c, case opt_T of
- SOME T => map fastype_of term_ts ---> T
- | NONE =>
- if num_type_args thy c = length type_us then
- Sign.const_instance thy (c,
- map (type_from_fo_term tfrees) type_us)
- else
- HOLogic.typeT)
- in list_comb (t, term_ts @ extra_ts) end
+ val T =
+ case opt_T of
+ SOME T => map fastype_of term_ts ---> T
+ | NONE =>
+ if num_type_args thy c = length type_us then
+ Sign.const_instance thy (c,
+ map (type_from_fo_term tfrees) type_us)
+ else
+ HOLogic.typeT
+ in list_comb (Const (c, T), term_ts @ extra_ts) end
| NONE => (* a free or schematic variable *)
let
val ts = map (aux NONE []) (us @ extra_us)
@@ -399,7 +399,8 @@
| uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
| uncombine_term (t as Const (x as (s, _))) =
(case AList.lookup (op =) combinator_table s of
- SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+ SOME thm => thm |> prop_of |> specialize_type @{theory} x
+ |> Logic.dest_equals |> snd
| NONE => t)
| uncombine_term t = t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Apr 04 18:53:35 2011 +0200
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_ATP_TRANSLATE =
sig
+ type 'a fo_term = 'a ATP_Problem.fo_term
type 'a problem = 'a ATP_Problem.problem
type translated_formula
@@ -15,6 +16,7 @@
Tags of bool |
Preds of bool |
Const_Args |
+ Mangled |
No_Types
val precise_overloaded_args : bool Unsynchronized.ref
@@ -25,6 +27,7 @@
val translate_atp_fact :
Proof.context -> bool -> (string * 'a) * thm
-> translated_formula option * ((string * 'a) * thm)
+ val unmangled_const : string -> string * string fo_term list
val prepare_atp_problem :
Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
@@ -63,6 +66,7 @@
Tags of bool |
Preds of bool |
Const_Args |
+ Mangled |
No_Types
fun types_dangerous_types (Tags _) = true
@@ -84,10 +88,22 @@
Tags full_types => not full_types andalso is_overloaded thy s
| Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
| Const_Args => is_overloaded thy s
+ | Mangled => true
| No_Types => false
+datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
+
+fun type_arg_policy thy type_sys s =
+ if needs_type_args thy type_sys s then
+ if type_sys = Mangled then Mangled_Types else Explicit_Type_Args
+ else
+ No_Type_Args
+
fun num_atp_type_args thy type_sys s =
- if needs_type_args thy type_sys s then num_type_args thy s else 0
+ if type_arg_policy thy type_sys s = Explicit_Type_Args then
+ num_type_args thy s
+ else
+ 0
fun atp_type_literals_for_types type_sys Ts =
if type_sys = No_Types then [] else type_literals_for_types Ts
@@ -389,6 +405,41 @@
("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
+(* We are crossing our fingers that it doesn't clash with anything else. *)
+val mangled_type_sep = "\000"
+
+fun mangled_combtyp f (CombTFree name) = f name
+ | mangled_combtyp f (CombType (name, tys)) =
+ "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
+ | mangled_combtyp _ _ = raise Fail "impossible schematic type variable"
+
+fun mangled_type_suffix f g tys =
+ fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
+ tys ""
+
+val parse_mangled_ident =
+ Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
+
+fun parse_mangled_type x =
+ ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")"
+ -- parse_mangled_ident >> (ATerm o swap)
+ || parse_mangled_ident >> (ATerm o rpair [])) x
+and parse_mangled_types x =
+ (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
+
+fun unmangled_type s =
+ s |> suffix ")" |> raw_explode
+ |> Scan.finite Symbol.stopper
+ (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
+ quote s)) parse_mangled_type))
+ |> fst
+ |> tap (fn u => PolyML.makestring u |> warning) (*###*)
+
+fun unmangled_const s =
+ let val ss = space_explode mangled_type_sep s in
+ (hd ss, map unmangled_type (tl ss))
+ end
+
fun fo_term_for_combterm ctxt type_sys =
let
val thy = ProofContext.theory_of ctxt
@@ -411,11 +462,14 @@
case strip_prefix_and_unascii const_prefix s of
NONE => (name, ty_args)
| SOME s'' =>
- let
- val s'' = invert_const s''
- val ty_args =
- if needs_type_args thy type_sys s'' then ty_args else []
- in (name, ty_args) end)
+ let val s'' = invert_const s'' in
+ case type_arg_policy thy type_sys s'' of
+ No_Type_Args => (name, [])
+ | Explicit_Type_Args => (name, ty_args)
+ | Mangled_Types =>
+ ((s ^ mangled_type_suffix fst ascii_of ty_args,
+ s' ^ mangled_type_suffix snd I ty_args), [])
+ end)
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
val t =
@@ -529,7 +583,9 @@
String.isPrefix class_prefix s then
16383 (* large number *)
else case strip_prefix_and_unascii const_prefix s of
- SOME s' => num_atp_type_args thy type_sys (invert_const s')
+ SOME s' =>
+ s' |> unmangled_const |> fst |> invert_const
+ |> num_atp_type_args thy type_sys
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 04 18:53:35 2011 +0200
@@ -190,9 +190,6 @@
end)]
end
-val smart_full_type_sys = Tags true
-val smart_partial_type_sys = Const_Args
-
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
@@ -245,10 +242,14 @@
("tags", full_types) => Tags full_types
| ("preds", full_types) => Preds full_types
| ("const_args", false) => Const_Args
+ | ("mangled", false) => if monomorphize then Mangled else Const_Args
| ("none", false) => No_Types
| (type_sys, full_types) =>
- if member (op =) ["const_args", "none", "smart"] type_sys then
- if full_types then smart_full_type_sys else smart_partial_type_sys
+ if member (op =) ["const_args", "mangled", "none", "smart"]
+ type_sys then
+ if full_types then Tags true
+ else if monomorphize then Mangled
+ else Const_Args
else
error ("Unknown type system: " ^ quote type_sys ^ ".")
val explicit_apply = lookup_bool "explicit_apply"