--- 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))
--- 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)