# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID 1b864c4a3306dd798407d0ffae742069360b87ec # Parent 21232c8c879b9d5f1ac92f1bf7f32374219f7bb7 more work on DFG type classes diff -r 21232c8c879b -r 1b864c4a3306 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:40 2012 +0200 @@ -22,8 +22,9 @@ ML {* if do_it then - "/tmp/axs_mono_native.dfg" - |> generate_tptp_inference_file_for_theory ctxt thy DFG "mono_native" + "/tmp/axs_tc_native.dfg" + |> generate_tptp_inference_file_for_theory ctxt thy (DFG With_Type_Classes) + "tc_native" else () *} diff -r 21232c8c879b -r 1b864c4a3306 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 @@ -44,7 +44,7 @@ datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = - Subclass_Decl of 'a * 'a list | + Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int * 'a list | Sym_Decl of string * 'a * 'a ho_type | Formula of string * formula_role @@ -125,7 +125,7 @@ (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : (string * string) problem -> (string * string) problem - val declared_in_problem : 'a problem -> 'a list * 'a list + val declared_in_atp_problem : 'a problem -> ('a list * 'a list) * 'a list val nice_atp_problem : bool -> atp_format -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -177,7 +177,7 @@ datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = - Subclass_Decl of 'a * 'a list | + Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int * 'a list | Sym_Decl of string * 'a * 'a ho_type | Formula of string * formula_role @@ -461,12 +461,10 @@ val atype_of_types = AType (tptp_type_of_types, []) -fun nary_type_constr_type n = - funpow n (curry AFun atype_of_types) atype_of_types +fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types -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)) +fun tptp_string_for_line format (Type_Decl (ident, ty, ary, _)) = + tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary)) | 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" @@ -496,7 +494,7 @@ let val str_for_typ = string_for_type (DFG poly) fun str_for_bound_typ (ty, []) = str_for_typ ty - | str_for_bound_typ (ty, sorts) = str_for_typ ty ^ " : " ^ commas sorts + | str_for_bound_typ (ty, cls) = str_for_typ ty ^ " : " ^ commas cls fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of @@ -544,8 +542,8 @@ val str_for_typ = string_for_type (DFG poly) fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")" fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty)) - fun ty_ary 0 sym = sym - | ty_ary n sym = "(" ^ sym ^ ", " ^ string_of_int n ^ ")" + fun ty_ary 0 ty = ty + | ty_ary n ty = "(" ^ ty ^ ", " ^ string_of_int n ^ ")" fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")." fun pred_typ sym ty = let @@ -576,15 +574,18 @@ | _ => NONE) |> flat |> commas |> maybe_enclose "predicates [" "]." val sorts = - filt (fn Type_Decl (_, sym, ary, _) => SOME (ty_ary ary sym) + filt (fn Type_Decl (_, ty, ary, _) => SOME (ty_ary ary ty) | _ => NONE) @ [[ty_ary 0 dfg_individual_type]] |> flat |> commas |> maybe_enclose "sorts [" "]." + val classes = + filt (fn Class_Decl (_, cl, _) => SOME cl | _ => NONE) + |> flat |> commas |> maybe_enclose "classes [" "]." val ord_info = if gen_weights orelse gen_prec then ord_info () else [] val do_term_order_weights = (if gen_weights then ord_info else []) |> map (spair o apsnd string_of_int) |> commas |> maybe_enclose "weights [" "]." - val syms = [func_aries, pred_aries, do_term_order_weights, sorts] + val syms = [func_aries, pred_aries, do_term_order_weights, sorts, classes] val func_sigs = filt (fn Sym_Decl (_, sym, ty) => if is_function_atype ty then SOME (fun_typ sym ty) else NONE @@ -717,11 +718,12 @@ (** Symbol declarations **) -fun add_declared_in_line (Type_Decl (_, ty, _, _)) = apfst (cons ty) +fun add_declared_in_line (Class_Decl (_, cl, _)) = apfst (apfst (cons cl)) + | add_declared_in_line (Type_Decl (_, ty, _, _)) = apfst (apsnd (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 ([], []) +fun declared_in_atp_problem problem = + fold (fold add_declared_in_line o snd) problem (([], []), []) (** Nice names **) @@ -846,7 +848,7 @@ fun nice_formula (ATyQuant (q, xs, phi)) = pool_map nice_type (map fst xs) ##>> pool_map (pool_map nice_name) (map snd xs) ##>> nice_formula phi - #>> (fn ((tys, sorts), phi) => ATyQuant (q, tys ~~ sorts, phi)) + #>> (fn ((tys, cls), phi) => ATyQuant (q, tys ~~ cls, phi)) | nice_formula (AQuant (q, xs, phi)) = pool_map nice_name (map fst xs) ##>> pool_map (fn NONE => pair NONE @@ -856,9 +858,12 @@ | nice_formula (AConn (c, phis)) = pool_map nice_formula phis #>> curry AConn c | nice_formula (AAtom tm) = nice_term tm #>> AAtom - 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)) + fun nice_line (Class_Decl (ident, cl, cls)) = + nice_name cl ##>> pool_map nice_name cls + #>> (fn (cl, cls) => Class_Decl (ident, cl, cls)) + | nice_line (Type_Decl (ident, ty, ary, cls)) = + nice_name ty ##>> pool_map nice_name cls + #>> (fn (ty, cls) => Type_Decl (ident, ty, ary, cls)) | nice_line (Sym_Decl (ident, sym, ty)) = nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) diff -r 21232c8c879b -r 1b864c4a3306 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 @@ -437,25 +437,6 @@ concl = (class, Type (tc, tvars))} end -fun arity_clause _ _ (_, []) = [] - | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *) - arity_clause seen n (tcons, ars) - | arity_clause seen n (tcons, (ar as (class, _)) :: ars) = - if member (op =) seen class then - (* multiple arities for the same (tycon, class) pair *) - make_axiom_arity_clause (tcons, - lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n, - ar) :: - arity_clause seen (n + 1) (tcons, ars) - else - make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^ - ascii_of class, ar) :: - arity_clause (class :: seen) n (tcons, ars) - -fun multi_arity_clause [] = [] - | multi_arity_clause ((tcons, ars) :: tc_arlists) = - arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists - (* 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 = @@ -468,21 +449,37 @@ 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.*) +(* Proving one (tycon, class) membership may require proving others, so + iterate. *) fun iter_type_class_pairs _ _ [] = ([], []) | iter_type_class_pairs thy tycons classes = - let - fun maybe_insert_class s = - (s <> type_class andalso not (member (op =) classes s)) - ? insert (op =) s - val cpairs = type_class_pairs thy tycons classes - val newclasses = - [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (classes' @ classes, union (op =) cpairs' cpairs) end + let + fun maybe_insert_class s = + (s <> type_class andalso not (member (op =) classes s)) + ? insert (op =) s + val cpairs = type_class_pairs thy tycons classes + val newclasses = + [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses + in (classes' @ classes, union (op =) cpairs' cpairs) end + +fun arity_clause _ _ (_, []) = [] + | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = + arity_clause seen n (tcons, ars) (* ignore *) + | arity_clause seen n (tcons, (ar as (class, _)) :: ars) = + if member (op =) seen class then + (* multiple arities for the same (tycon, class) pair *) + make_axiom_arity_clause (tcons, + lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n, + ar) :: + arity_clause seen (n + 1) (tcons, ars) + else + make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^ + ascii_of class, ar) :: + arity_clause (class :: seen) n (tcons, ars) fun make_arity_clauses thy tycons = - iter_type_class_pairs thy tycons ##> multi_arity_clause + iter_type_class_pairs thy tycons ##> maps (arity_clause [] 1) (** Isabelle class relations **) @@ -494,19 +491,16 @@ (* Generate all pairs (sub, super) such that sub is a proper subclass of super in theory "thy". *) -fun class_pairs _ [] _ = [] - | class_pairs thy subs supers = - let - val class_less = Sorts.class_less (Sign.classes_of thy) - fun add_super sub super = class_less (sub, super) ? cons (sub, super) - fun add_supers sub = fold (add_super sub) supers - in fold add_supers subs [] end +fun class_pairs thy subs supers = + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end fun make_class_rel_clause (sub, super) = {name = sub ^ "_" ^ super, subclass = sub, superclass = super} - -fun make_class_rel_clauses thy subs supers = - map make_class_rel_clause (class_pairs thy subs supers) +fun make_class_rel_clauses thy = map make_class_rel_clause oo class_pairs thy (* intermediate terms *) datatype iterm = @@ -975,13 +969,12 @@ | _ => []) in AAtom (ATerm ((class, ty_args), tm_args)) end fun formulas_for_types type_enc add_sorts_on_typ Ts = - [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts + [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso + level_of_type_enc type_enc <> No_Types) + ? fold add_sorts_on_typ Ts |> map (type_class_atom type_enc) -fun mk_aconns c phis = - let val (phis', phi') = split_last phis in - fold_rev (mk_aconn c) phis' phi' - end +fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c)) fun mk_ahorn [] phi = phi | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) @@ -1739,8 +1732,7 @@ case filter is_TVar Ts of [] => I | Ts => - ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic) - ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)) + (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)) #> (case type_enc of Native (_, poly, _) => mk_atyquant AForall (map (fn TVar (x, S) => @@ -2170,7 +2162,7 @@ (** Symbol declarations **) -fun decl_line_for_class order phantoms s = +fun decl_line_for_class phantoms s = let val name as (s, _) = `make_type_class s in Sym_Decl (sym_decl_prefix ^ s, name, APi ([tvar_a_name], @@ -2182,8 +2174,8 @@ fun decl_lines_for_classes type_enc classes = case type_enc of - Native (order, Raw_Polymorphic phantoms, _) => - map (decl_line_for_class order phantoms) classes + Native (_, Raw_Polymorphic phantoms, _) => + map (decl_line_for_class phantoms) classes | _ => [] fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) = @@ -2573,7 +2565,7 @@ symbols (with "$i" as the type of individuals), but some provers (e.g., SNARK) require explicit declarations. The situation is similar for THF. *) -fun default_type pred_sym s = +fun default_type pred_sym = let fun typ 0 0 = if pred_sym then bool_atype else individual_atype | typ 0 tm_ary = AFun (individual_atype, typ 0 (tm_ary - 1)) @@ -2585,16 +2577,19 @@ fun do_sym (name as (s, _)) value = if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I fun do_type (AType (name, tys)) = - apfst (do_sym name (length tys)) #> fold do_type tys + apfst (apsnd (do_sym name (length tys))) #> fold do_type tys | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 | do_type (APi (_, ty)) = do_type ty - fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) = + fun do_term pred_sym (ATerm ((name, tys), tms)) = apsnd (do_sym name - (fn _ => default_type pred_sym s (length tys) (length tms))) + (fn _ => default_type pred_sym (length tys) (length tms))) #> fold do_type tys #> fold (do_term false) tms | do_term _ (AAbs (((_, ty), tm), args)) = do_type ty #> do_term false tm #> fold (do_term false) args - fun do_formula (ATyQuant (_, _, phi)) = do_formula phi + fun do_formula (ATyQuant (_, xs, phi)) = + fold (do_type o fst) xs + #> fold (fold (fn name => apfst (apfst (do_sym name ()))) o snd) xs + #> do_formula phi | do_formula (AQuant (_, xs, phi)) = fold do_type (map_filter snd xs) #> do_formula phi | do_formula (AConn (_, phis)) = fold do_formula phis @@ -2602,36 +2597,36 @@ 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 + val ((cls, tys), syms) = declared_in_atp_problem problem in - (Symtab.empty, Symtab.empty) - |>> fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys + ((Symtab.empty, Symtab.empty), Symtab.empty) + |>> apfst (fold (fn (s, _) => Symtab.default (s, (("", ""), ()))) cls) + |>> apsnd (fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys) ||> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype))) syms |> fold (fold do_line o snd) problem end -fun declare_undeclared_in_atp_problem problem = +fun declare_undeclared_in_problem heading problem = let - val (types, syms) = undeclared_in_problem problem + val ((cls, tys), syms) = undeclared_in_problem problem val decls = Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) + | (s, (sym, ())) => + cons (Class_Decl (type_decl_prefix ^ s, sym, []))) + cls [] @ + Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) | (s, (sym, ary)) => - cons (Type_Decl (type_decl_prefix ^ s, sym, ary, []))) (* ### FIXME *) - types [] @ + cons (Type_Decl (type_decl_prefix ^ s, sym, ary, []))) + tys [] @ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) | (s, (sym, ty)) => cons (Sym_Decl (type_decl_prefix ^ s, sym, ty ()))) syms [] - in (implicit_declsN, decls) :: problem end + in (heading, decls) :: problem end -fun exists_subdtype P = - let - fun ex U = P U orelse - (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false) - in ex end - -val is_poly_constr = - exists_subdtype (fn Datatype.DtTFree _ => true | _ => false) +fun is_poly_constr (Datatype.DtTFree _) = true + | is_poly_constr (Datatype.DtType (_, Us)) = exists is_poly_constr Us + | is_poly_constr _ = false fun all_constrs_of_polymorphic_datatypes thy = Symtab.fold (snd #> #descr #> maps (#3 o snd) @@ -2705,12 +2700,15 @@ 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, arity_lines) = + val (class_rel_lines, arity_lines, free_type_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) + map (formula_line_for_arity_clause type_enc) arity_clauses, + formula_lines_for_free_types type_enc (facts @ conjs)) val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (formula_line_for_fact ctxt helper_prefix I false true mono @@ -2723,7 +2721,7 @@ (class_relsN, class_rel_lines), (aritiesN, arity_lines), (helpersN, helper_lines), - (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)), + (free_typesN, free_type_lines), (conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)] val problem = problem |> (case format of @@ -2732,7 +2730,7 @@ | FOF => I | TFF (_, TPTP_Implicit) => I | THF (_, TPTP_Implicit, _, _) => I - | _ => declare_undeclared_in_atp_problem) + | _ => declare_undeclared_in_problem implicit_declsN) 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)