# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID 21232c8c879b9d5f1ac92f1bf7f32374219f7bb7 # Parent b755096701ec8b2d3d020d6f3f92255e8ed715ad more work on class support diff -r b755096701ec -r 21232c8c879b src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r b755096701ec -r 21232c8c879b src/HOL/Tools/ATP/atp_problem.ML --- 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; diff -r b755096701ec -r 21232c8c879b src/HOL/Tools/ATP/atp_problem_generate.ML --- 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)