--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
@@ -112,7 +112,7 @@
fun add_inferences_to_problem infers =
map (apsnd (map (add_inferences_to_problem_line infers)))
-fun ident_of_problem_line (Type_Decl (ident, _, _)) = ident
+fun ident_of_problem_line (Type_Decl (ident, _, _, _)) = ident
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -29,7 +29,7 @@
gen_prec : bool,
gen_simp : bool}
- datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
+ datatype polymorphism = Monomorphic | Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -44,7 +44,8 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Type_Decl of string * 'a * int |
+ Subclass_Decl of 'a * 'a list |
+ Type_Decl of string * 'a * int * 'a list |
Sym_Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -124,7 +125,7 @@
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
(string * string) problem -> (string * string) problem
- val declared_types_and_syms_in_problem : 'a problem -> 'a list * 'a list
+ val declared_in_problem : 'a problem -> 'a list * 'a list
val nice_atp_problem :
bool -> atp_format -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -161,7 +162,7 @@
gen_prec : bool,
gen_simp : bool}
-datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
+datatype polymorphism = Monomorphic | Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -176,7 +177,8 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Type_Decl of string * 'a * int |
+ Subclass_Decl of 'a * 'a list |
+ Type_Decl of string * 'a * int * 'a list |
Sym_Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -462,14 +464,13 @@
fun nary_type_constr_type n =
funpow n (curry AFun atype_of_types) atype_of_types
-fun tptp_string_for_problem_line format (Type_Decl (ident, sym, ary)) =
- tptp_string_for_problem_line format
+fun tptp_string_for_line format (Type_Decl (ident, sym, ary, _)) =
+ tptp_string_for_line format
(Sym_Decl (ident, sym, nary_type_constr_type ary))
- | tptp_string_for_problem_line format (Sym_Decl (ident, sym, ty)) =
+ | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
" : " ^ string_for_type format ty ^ ").\n"
- | tptp_string_for_problem_line format
- (Formula (ident, kind, phi, source, _)) =
+ | tptp_string_for_line format (Formula (ident, kind, phi, source, _)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
tptp_string_for_role kind ^ ",\n (" ^
tptp_string_for_formula format phi ^ ")" ^
@@ -481,7 +482,7 @@
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
- map (tptp_string_for_problem_line format) lines)
+ map (tptp_string_for_line format) lines)
fun arity_of_type (APi (tys, ty)) =
arity_of_type ty |>> Integer.add (length tys)
@@ -575,8 +576,8 @@
| _ => NONE)
|> flat |> commas |> maybe_enclose "predicates [" "]."
val sorts =
- filt (fn Type_Decl (_, sym, ary) => SOME (ty_ary ary sym) | _ => NONE) @
- [[ty_ary 0 dfg_individual_type]]
+ filt (fn Type_Decl (_, sym, ary, _) => SOME (ty_ary ary sym)
+ | _ => NONE) @ [[ty_ary 0 dfg_individual_type]]
|> flat |> commas |> maybe_enclose "sorts [" "]."
val ord_info = if gen_weights orelse gen_prec then ord_info () else []
val do_term_order_weights =
@@ -634,13 +635,12 @@
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
-fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
- | is_problem_line_negated _ = false
+fun is_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
+ | is_line_negated _ = false
-fun is_problem_line_cnf_ueq
- (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) =
+fun is_line_cnf_ueq (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) =
is_tptp_equal s
- | is_problem_line_cnf_ueq _ = false
+ | is_line_cnf_ueq _ = false
fun open_conjecture_term (ATerm (((s, s'), tys), tms)) =
ATerm ((if is_tptp_variable s then (s |> Name.desymbolize false, s')
@@ -699,31 +699,29 @@
end
| clausify_formula_line _ = []
-fun ensure_cnf_problem_line line =
+fun ensure_cnf_line line =
line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
-fun ensure_cnf_problem problem =
- problem |> map (apsnd (maps ensure_cnf_problem_line))
+fun ensure_cnf_problem problem = problem |> map (apsnd (maps ensure_cnf_line))
fun filter_cnf_ueq_problem problem =
problem
- |> map (apsnd (map open_formula_line
- #> filter is_problem_line_cnf_ueq
+ |> map (apsnd (map open_formula_line #> filter is_line_cnf_ueq
#> map negate_conjecture_line))
|> (fn problem =>
let
val lines = problem |> maps snd
- val conjs = lines |> filter is_problem_line_negated
+ val conjs = lines |> filter is_line_negated
in if length conjs = 1 andalso conjs <> lines then problem else [] end)
(** Symbol declarations **)
-fun add_declared_syms_in_problem_line (Type_Decl (_, sym, _)) = apfst (cons sym)
- | add_declared_syms_in_problem_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
- | add_declared_syms_in_problem_line _ = I
-fun declared_types_and_syms_in_problem problem =
- fold (fold add_declared_syms_in_problem_line o snd) problem ([], [])
+fun add_declared_in_line (Type_Decl (_, ty, _, _)) = apfst (cons ty)
+ | add_declared_in_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
+ | add_declared_in_line _ = I
+fun declared_in_problem problem =
+ fold (fold add_declared_in_line o snd) problem ([], [])
(** Nice names **)
@@ -858,16 +856,17 @@
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
- fun nice_problem_line (Type_Decl (ident, sym, ary)) =
- nice_name sym #>> (fn sym => Type_Decl (ident, sym, ary))
- | nice_problem_line (Sym_Decl (ident, sym, ty)) =
+ fun nice_line (Type_Decl (ident, sym, ary, sorts)) =
+ nice_name sym ##>> pool_map nice_name sorts
+ #>> (fn (sym, sorts) => Type_Decl (ident, sym, ary, sorts))
+ | nice_line (Sym_Decl (ident, sym, ty)) =
nice_name sym ##>> nice_type ty
#>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
- | nice_problem_line (Formula (ident, kind, phi, source, info)) =
+ | nice_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
- pool_map nice_problem_line lines #>> pair heading) problem
+ pool_map nice_line lines #>> pair heading) problem
in nice_problem problem empty_pool end
end;
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -2344,7 +2344,7 @@
NONE, isabelle_info defN helper_rank)
end
-fun problem_lines_for_mono_types ctxt mono type_enc Ts =
+fun lines_for_mono_types ctxt mono type_enc Ts =
case type_enc of
Native _ => []
| Guards _ => map (formula_line_for_guards_mono_type ctxt mono type_enc) Ts
@@ -2458,7 +2458,7 @@
end
| rationalize_decls _ decls = decls
-fun problem_lines_for_sym_decls ctxt mono type_enc (s, decls) =
+fun lines_for_sym_decls ctxt mono type_enc (s, decls) =
case type_enc of
Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)]
| Guards (_, level) =>
@@ -2482,12 +2482,12 @@
|> maps (formula_lines_for_tags_sym_decl ctxt mono type_enc n s)
end
-fun problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
+fun lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
let
val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
- val mono_lines = problem_lines_for_mono_types ctxt mono type_enc mono_Ts
+ val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts
val decl_lines =
- fold_rev (append o problem_lines_for_sym_decls ctxt mono type_enc) syms []
+ fold_rev (append o lines_for_sym_decls ctxt mono type_enc) syms []
in mono_lines @ decl_lines end
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2580,7 +2580,7 @@
| typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
in typ end
-fun undeclared_types_and_syms_in_problem problem =
+fun undeclared_in_problem problem =
let
fun do_sym (name as (s, _)) value =
if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
@@ -2599,24 +2599,24 @@
fold do_type (map_filter snd xs) #> do_formula phi
| do_formula (AConn (_, phis)) = fold do_formula phis
| do_formula (AAtom tm) = do_term true tm
- fun do_problem_line (Type_Decl _) = I
- | do_problem_line (Sym_Decl (_, _, ty)) = do_type ty
- | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
- val (tys, syms) = declared_types_and_syms_in_problem problem
+ fun do_line (Type_Decl _) = I
+ | do_line (Sym_Decl (_, _, ty)) = do_type ty
+ | do_line (Formula (_, _, phi, _, _)) = do_formula phi
+ val (tys, syms) = declared_in_problem problem
in
(Symtab.empty, Symtab.empty)
|>> fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys
||> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype))) syms
- |> fold (fold do_problem_line o snd) problem
+ |> fold (fold do_line o snd) problem
end
-fun declare_undeclared_types_and_syms_in_atp_problem problem =
+fun declare_undeclared_in_atp_problem problem =
let
- val (types, syms) = undeclared_types_and_syms_in_problem problem
+ val (types, syms) = undeclared_in_problem problem
val decls =
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
| (s, (sym, ary)) =>
- cons (Type_Decl (type_decl_prefix ^ s, sym, ary)))
+ cons (Type_Decl (type_decl_prefix ^ s, sym, ary, []))) (* ### FIXME *)
types [] @
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
| (s, (sym, ty)) =>
@@ -2699,14 +2699,18 @@
val sym_decl_lines =
(conjs, helpers @ facts, uncurried_alias_eq_tms)
|> sym_decl_table_for_facts thy type_enc sym_tab
- |> problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts
+ |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts
val num_facts = length facts
val fact_lines =
map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
(not exporter) mono type_enc (rank_of_fact_num num_facts))
(0 upto num_facts - 1 ~~ facts)
- val class_rel_lines =
- map (formula_line_for_class_rel_clause type_enc) class_rel_clauses
+ val (class_rel_lines, arity_lines) =
+ if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
+ ([], [])
+ else
+ (map (formula_line_for_class_rel_clause type_enc) class_rel_clauses,
+ map (formula_line_for_arity_clause type_enc) arity_clauses)
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt helper_prefix I false true mono
@@ -2717,7 +2721,7 @@
(uncurried_alias_eqsN, uncurried_alias_eq_lines),
(factsN, fact_lines),
(class_relsN, class_rel_lines),
- (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
+ (aritiesN, arity_lines),
(helpersN, helper_lines),
(free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
(conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)]
@@ -2728,7 +2732,7 @@
| FOF => I
| TFF (_, TPTP_Implicit) => I
| THF (_, TPTP_Implicit, _, _) => I
- | _ => declare_undeclared_types_and_syms_in_atp_problem)
+ | _ => declare_undeclared_in_atp_problem)
val (problem, pool) = problem |> nice_atp_problem readable_names format
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
min_ary > 0 ? Symtab.insert (op =) (s, min_ary)