# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 40e50afbc20308e530b98868788f15146b39d701 # Parent 93ec303e19173e50723692002e651a2b0635fd9a tuning diff -r 93ec303e1917 -r 40e50afbc203 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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]) diff -r 93ec303e1917 -r 40e50afbc203 src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r 93ec303e1917 -r 40e50afbc203 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 93ec303e1917 -r 40e50afbc203 src/HOL/Tools/Metis/metis_translate.ML --- 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)