--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -359,8 +359,8 @@
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
-fun typ_from_fo_term tfrees (u as ATerm (a, us)) =
- let val Ts = map (typ_from_fo_term tfrees) us in
+fun typ_from_atp tfrees (u as ATerm (a, us)) =
+ let val Ts = map (typ_from_atp tfrees) us in
case strip_prefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
@@ -383,7 +383,7 @@
type. *)
fun type_constraint_from_term tfrees (u as ATerm (a, us)) =
case (strip_prefix_and_unascii class_prefix a,
- map (typ_from_fo_term tfrees) us) of
+ map (typ_from_atp tfrees) us) of
(SOME b, [T]) => (b, T)
| _ => raise FO_TERM [u]
@@ -410,20 +410,17 @@
| _ => s
end
-fun num_type_args thy s =
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred. *)
-fun raw_term_from_pred thy sym_tab tfrees =
+fun term_from_atp thy sym_tab tfrees =
let
- fun aux opt_T extra_us u =
+ fun do_term extra_us opt_T u =
case u of
ATerm (a, us) =>
if String.isPrefix simple_type_prefix a then
@{const True} (* ignore TPTP type information *)
else if a = tptp_equal then
- let val ts = map (aux NONE []) us in
+ let val ts = map (do_term [] NONE) us in
if length ts = 2 andalso hd ts aconv List.last ts then
(* Vampire is keen on producing these. *)
@{const True}
@@ -438,12 +435,12 @@
if s' = type_tag_name then
case mangled_us @ us of
[typ_u, term_u] =>
- aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
+ do_term extra_us (SOME (typ_from_atp tfrees typ_u)) term_u
| _ => raise FO_TERM us
else if s' = predicator_name then
- aux (SOME @{typ bool}) [] (hd us)
+ do_term [] (SOME @{typ bool}) (hd us)
else if s' = app_op_name then
- aux opt_T (nth us 1 :: extra_us) (hd us)
+ do_term (nth us 1 :: extra_us) opt_T (hd us)
else if s' = type_pred_name then
@{const True} (* ignore type predicates *)
else
@@ -454,13 +451,13 @@
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 term_ts = map (do_term [] NONE) term_us
+ val extra_ts = map (do_term [] NONE) extra_us
val T =
if not (null type_us) andalso
num_type_args thy s' = length type_us then
- Sign.const_instance thy
- (s', map (typ_from_fo_term tfrees) type_us)
+ (s', map (typ_from_atp tfrees) type_us)
+ |> Sign.const_instance thy
else case opt_T of
SOME T => map fastype_of (term_ts @ extra_ts) ---> T
| NONE => HOLogic.typeT
@@ -469,7 +466,7 @@
end
| NONE => (* a free or schematic variable *)
let
- val ts = map (aux NONE []) (us @ extra_us)
+ val ts = map (do_term [] NONE) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
case strip_prefix_and_unascii fixed_var_prefix a of
@@ -484,14 +481,14 @@
(* Skolem constants? *)
Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
in list_comb (t, ts) end
- in aux (SOME HOLogic.boolT) [] end
+ in do_term [] end
-fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) =
+fun term_from_atom thy sym_tab tfrees pos (u as ATerm (s, _)) =
if String.isPrefix class_prefix s then
add_type_constraint pos (type_constraint_from_term tfrees u)
#> pair @{const True}
else
- pair (raw_term_from_pred thy sym_tab tfrees u)
+ pair (term_from_atp thy sym_tab tfrees (SOME @{typ bool}) u)
val combinator_table =
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
@@ -560,7 +557,7 @@
| AIff => s_iff
| ANotIff => s_not o s_iff
| _ => raise Fail "unexpected connective")
- | AAtom tm => term_from_pred thy sym_tab tfrees pos tm
+ | AAtom tm => term_from_atom thy sym_tab tfrees pos tm
| _ => raise FORMULA [phi]
in repair_tvar_sorts (do_formula true phi Vartab.empty) end
@@ -569,7 +566,7 @@
#> Syntax.check_term
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-(**** Translation of TSTP files to Isar Proofs ****)
+(**** Translation of TSTP files to Isar proofs ****)
fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -86,6 +86,8 @@
val make_fixed_const : string -> string
val make_fixed_type_const : string -> string
val make_type_class : string -> string
+ val new_skolem_var_name_from_const : string -> string
+ val num_type_args : theory -> string -> int
val make_arity_clauses :
theory -> string list -> class list -> class list * arity_clause list
val make_class_rel_clauses :
@@ -166,7 +168,7 @@
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
-val class_rel_clause_prefix = "crel_";
+val class_rel_clause_prefix = "crel_"
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"
@@ -186,7 +188,7 @@
The character _ goes to __
Characters in the range ASCII space to / go to _A to _P, respectively.
Other characters go to _nnn where nnn is the decimal ASCII code.*)
-val upper_a_minus_space = Char.ord #"A" - Char.ord #" ";
+val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
fun stringN_of_int 0 _ = ""
| stringN_of_int k n =
@@ -311,6 +313,20 @@
fun make_type_class clas = class_prefix ^ ascii_of clas
+fun new_skolem_var_name_from_const s =
+ let val ss = s |> space_explode Long_Name.separator in
+ nth ss (length ss - 2)
+ end
+
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_const_prefix s then
+ s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
(** Definitions and functions for FOL clauses and formulas for TPTP **)
(* The first component is the type class; the second is a "TVar" or "TFree". *)
@@ -326,7 +342,7 @@
TVarLit of name * name
fun gen_TVars 0 = []
- | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1);
+ | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
fun pack_sort (_,[]) = []
| pack_sort (tvar, "HOL.type" :: srt) =
@@ -370,13 +386,14 @@
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
provided its arguments have the corresponding sorts.*)
fun type_class_pairs thy tycons classes =
- let val alg = Sign.classes_of thy
- fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
- fun add_class tycon class =
- cons (class, domain_sorts tycon class)
- handle Sorts.CLASS_ERROR _ => I
- fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
- in map try_classes tycons end;
+ let
+ val alg = Sign.classes_of thy
+ fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
+ fun add_class tycon class =
+ cons (class, domain_sorts tycon class)
+ handle Sorts.CLASS_ERROR _ => I
+ fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
+ in map try_classes tycons end
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
fun iter_type_class_pairs _ _ [] = ([], [])
@@ -385,7 +402,7 @@
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
|> subtract (op =) classes |> subtract (op =) HOLogic.typeS
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
+ in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
fun make_arity_clauses thy tycons =
iter_type_class_pairs thy tycons ##> multi_arity_clause
@@ -413,7 +430,7 @@
superclass = `make_type_class super}
fun make_class_rel_clauses thy subs supers =
- map make_class_rel_clause (class_pairs thy subs supers);
+ map make_class_rel_clause (class_pairs thy subs supers)
datatype combterm =
CombConst of name * typ * typ list |
@@ -601,14 +618,16 @@
general_type_arg_policy type_sys
(*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
- | sorts_on_typs_aux ((x,i), s::ss) =
- let val sorts = sorts_on_typs_aux ((x,i), ss)
- in
- if s = the_single @{sort HOL.type} then sorts
- else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
- else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
- end;
+fun sorts_on_typs_aux (_, []) = []
+ | sorts_on_typs_aux ((x, i), s :: ss) =
+ sorts_on_typs_aux ((x, i), ss)
+ |> (if s = the_single @{sort HOL.type} then
+ I
+ else if i = ~1 then
+ cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
+ else
+ cons (TyLitVar (`make_type_class s,
+ (make_schematic_type_var (x, i), x))))
fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)
| sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)
@@ -1286,17 +1305,17 @@
(* Remove this trivial type class (FIXME: similar code elsewhere) *)
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
-fun tfree_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+fun classes_of_terms get_Ts =
+ map (map #2 o get_Ts)
+ #> List.foldl add_classes Symtab.empty
+ #> delete_type #> Symtab.keys
-fun tvar_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
+val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
(*fold type constructors*)
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
- | fold_type_consts _ _ x = x;
+ | fold_type_consts _ _ x = x
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
fun add_type_consts_in_term thy =
@@ -1310,7 +1329,7 @@
in aux end
fun type_consts_of_terms thy ts =
- Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
+ Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)
fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -212,8 +212,10 @@
hol_term_from_metis_PT ctxt t)
in fol_tm |> cvt end
-fun hol_term_from_metis FT = hol_term_from_metis_FT
- | hol_term_from_metis _ = hol_term_from_metis_PT
+fun hol_term_from_metis FO = hol_term_from_metis_PT
+ | hol_term_from_metis HO = hol_term_from_metis_PT
+ | hol_term_from_metis FT = hol_term_from_metis_FT
+(* | hol_term_from_metis New = ###*)
fun hol_terms_from_metis ctxt mode old_skolems fol_tms =
let val ts = map (hol_term_from_metis mode ctxt) fol_tms
@@ -453,9 +455,11 @@
val metis_eq = Metis_Term.Fn ("=", []);
-fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
- | get_ty_arg_size _ _ = 0;
+(* Equality has no type arguments *)
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0
+ | get_ty_arg_size thy (Const (s, _)) =
+ (num_type_args thy s handle TYPE _ => 0)
+ | get_ty_arg_size _ _ = 0
fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
let val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -19,9 +19,6 @@
old_skolems: (string * term) list}
val metis_generated_var_prefix : string
- val new_skolem_const_prefix : string
- val num_type_args: theory -> string -> int
- val new_skolem_var_name_from_const : string -> string
val reveal_old_skolem_terms : (string * term) list -> term -> term
val string_of_mode : mode -> string
val prepare_metis_problem :
@@ -36,20 +33,6 @@
val metis_generated_var_prefix = "_"
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_const_prefix s then
- s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
-fun new_skolem_var_name_from_const s =
- let val ss = s |> space_explode Long_Name.separator in
- nth ss (length ss - 2)
- end
-
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) =
(combterm_from_term thy [] (Envir.eta_contract t), pos)