# HG changeset patch # User blanchet # Date 1387464437 -3600 # Node ID d9ab86c044fdc3925abfbada8a51fa87a0ed71c5 # Parent 6e78f87ed554cad643fedadd1d378125a79ed87f extended ATP types with sorts diff -r 6e78f87ed554 -r d9ab86c044fd src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 19 15:04:21 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 19 15:47:17 2013 +0100 @@ -21,7 +21,7 @@ AAtom of 'c datatype 'a atp_type = - AType of 'a * 'a atp_type list | + AType of ('a * 'a list) * 'a atp_type list | AFun of 'a atp_type * 'a atp_type | APi of 'a list * 'a atp_type @@ -165,7 +165,7 @@ AAtom of 'c datatype 'a atp_type = - AType of 'a * 'a atp_type list | + AType of ('a * 'a list) * 'a atp_type list | AFun of 'a atp_type * 'a atp_type | APi of 'a list * 'a atp_type @@ -273,8 +273,8 @@ fun is_tptp_variable s = s <> "" andalso Char.isUpper (String.sub (s, 0)) val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) -val bool_atype = AType (`I tptp_bool_type, []) -val individual_atype = AType (`I tptp_individual_type, []) +val bool_atype = AType ((`I tptp_bool_type, []), []) +val individual_atype = AType ((`I tptp_individual_type, []), []) fun raw_polarities_of_conn ANot = (SOME false, NONE) | raw_polarities_of_conn AAnd = (SOME true, SOME true) @@ -324,8 +324,7 @@ fun strip_atype ty = ty |> strip_api ||> strip_afun -fun is_function_atype ty = - snd (snd (strip_atype ty)) <> AType (tptp_bool_type, []) +fun is_function_atype ty = snd (snd (strip_atype ty)) <> AType ((tptp_bool_type, []), []) fun is_predicate_atype ty = not (is_function_atype ty) fun is_nontrivial_predicate_atype (AType _) = false | is_nontrivial_predicate_atype ty = is_predicate_atype ty @@ -356,9 +355,9 @@ fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty) | uncurry_type (ty as AFun (ty1 as AType _, ty2)) = (case uncurry_type ty2 of - AFun (ty' as AType (s, tys), ty) => - AFun (AType (tptp_product_type, - ty1 :: (if s = tptp_product_type then tys else [ty'])), ty) + AFun (ty' as AType ((s, _), tys), ty) => + AFun (AType ((tptp_product_type, []), + ty1 :: (if s = tptp_product_type then tys else [ty'])), ty) | _ => ty) | uncurry_type (ty as AType _) = ty | uncurry_type _ = @@ -372,9 +371,9 @@ fun str_of_type format ty = let val dfg = case format of DFG _ => true | _ => false - fun str _ (AType (s, [])) = + fun str _ (AType ((s, _), [])) = if dfg andalso s = tptp_individual_type then dfg_individual_type else s - | str _ (AType (s, tys)) = + | str _ (AType ((s, _), tys)) = let val ss = tys |> map (str false) in if s = tptp_product_type then ss |> space_implode @@ -411,8 +410,7 @@ s ^ (if is_format_typed format then " " ^ tptp_has_type ^ " " ^ - (ty |> the_default (AType (tptp_individual_type, [])) - |> string_of_type format) + (ty |> the_default (AType ((tptp_individual_type, []), [])) |> string_of_type format) else "") @@ -507,7 +505,7 @@ | tptp_string_of_format (THF _) = tptp_thf | tptp_string_of_format (DFG _) = raise Fail "non-TPTP format" -val atype_of_types = AType (tptp_type_of_types, []) +val atype_of_types = AType ((tptp_type_of_types, []), []) fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types @@ -910,21 +908,22 @@ | DFG _ => avoid_clash_with_dfg_keywords | _ => I val nice_name = nice_name avoid_clash + fun nice_bound_tvars xs = fold_map (nice_name o fst) xs ##>> fold_map (fold_map nice_name o snd) xs #>> op ~~ - fun nice_type (AType (name, tys)) = - nice_name name ##>> fold_map nice_type tys #>> AType + + fun nice_type (AType ((name, clss), tys)) = + nice_name name ##>> fold_map nice_name clss ##>> fold_map nice_type tys #>> AType | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun - | nice_type (APi (names, ty)) = - fold_map nice_name names ##>> nice_type ty #>> APi + | nice_type (APi (names, ty)) = fold_map nice_name names ##>> nice_type ty #>> APi + fun nice_term (ATerm ((name, tys), ts)) = - nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts - #>> ATerm + nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts #>> ATerm | nice_term (AAbs (((name, ty), tm), args)) = - nice_name name ##>> nice_type ty ##>> nice_term tm - ##>> fold_map nice_term args #>> AAbs + nice_name name ##>> nice_type ty ##>> nice_term tm ##>> fold_map nice_term args #>> AAbs + fun nice_formula (ATyQuant (q, xs, phi)) = fold_map (nice_type o fst) xs ##>> fold_map (fold_map nice_name o snd) xs @@ -939,14 +938,14 @@ | nice_formula (AConn (c, phis)) = fold_map nice_formula phis #>> curry AConn c | nice_formula (AAtom tm) = nice_term tm #>> AAtom + fun nice_line (Class_Decl (ident, cl, cls)) = nice_name cl ##>> fold_map nice_name cls #>> (fn (cl, cls) => Class_Decl (ident, cl, cls)) | nice_line (Type_Decl (ident, ty, ary)) = nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) | nice_line (Sym_Decl (ident, sym, ty)) = - nice_name sym ##>> nice_type ty - #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) + nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) | nice_line (Datatype_Decl (ident, xs, ty, tms)) = nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms)) @@ -954,11 +953,12 @@ nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) | nice_line (Formula (ident, kind, phi, source, info)) = - nice_formula phi - #>> (fn phi => Formula (ident, kind, phi, source, info)) + nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info)) + fun nice_problem problem = - fold_map (fn (heading, lines) => - fold_map nice_line lines #>> pair heading) problem - in nice_problem problem empty_pool end + fold_map (fn (heading, lines) => fold_map nice_line lines #>> pair heading) problem + in + nice_problem problem empty_pool + end end; diff -r 6e78f87ed554 -r d9ab86c044fd src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 15:04:21 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 15:47:17 2013 +0100 @@ -439,8 +439,8 @@ val tvar_a_name = tvar_name tvar_a_z val itself_name = `make_fixed_type_const @{type_name itself} val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE} -val tvar_a_atype = AType (tvar_a_name, []) -val a_itself_atype = AType (itself_name, [tvar_a_atype]) +val tvar_a_atype = AType ((tvar_a_name, []), []) +val a_itself_atype = AType ((itself_name, []), [tvar_a_atype]) (** Definitions and functions for FOL clauses and formulas for TPTP **) @@ -479,8 +479,7 @@ | all_class_pairs thy tycons cls = let fun maybe_insert_class s = - (s <> class_of_types andalso not (member (op =) cls s)) - ? insert (op =) s + (s <> class_of_types andalso not (member (op =) cls s)) ? insert (op =) s val pairs = class_pairs thy tycons cls val new_cls = [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs @@ -495,12 +494,10 @@ else if member (op =) seen cl then (* multiple clauses for the same (tycon, cl) pair *) make_axiom_tcon_clause (tcons, - lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, - ar) :: + lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, ar) :: tcon_clause seen (n + 1) ((tcons, ars) :: rest) else - make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, - ar) :: + make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, ar) :: tcon_clause (cl :: seen) n ((tcons, ars) :: rest) fun make_tcon_clauses thy tycons = @@ -905,28 +902,26 @@ val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) val fused_infinite_type = Type (fused_infinite_type_name, []) -fun raw_ho_type_of_typ type_enc = +fun raw_atp_type_of_typ type_enc = let fun term (Type (s, Ts)) = - AType (case (is_type_enc_higher_order type_enc, s) of + AType ((case (is_type_enc_higher_order type_enc, s) of (true, @{type_name bool}) => `I tptp_bool_type | (true, @{type_name fun}) => `I tptp_fun_type - | _ => if s = fused_infinite_type_name andalso - is_type_enc_native type_enc then - `I tptp_individual_type - else - `make_fixed_type_const s, - map term Ts) - | term (TFree (s, _)) = AType (`make_tfree s, []) - | term (TVar z) = AType (tvar_name z, []) + | _ => + if s = fused_infinite_type_name andalso is_type_enc_native type_enc then + `I tptp_individual_type + else + `make_fixed_type_const s, []), map term Ts) + | term (TFree (s, _)) = AType ((`make_tfree s, []), []) + | term (TVar (z as (_, S))) = AType ((tvar_name z, []), []) in term end -fun atp_term_of_ho_type (AType (name, tys)) = - ATerm ((name, []), map atp_term_of_ho_type tys) - | atp_term_of_ho_type _ = raise Fail "unexpected type" +fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys) + | atp_term_of_atp_type _ = raise Fail "unexpected type" -fun ho_type_of_type_arg type_enc T = - if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T) +fun atp_type_of_type_arg type_enc T = + if T = dummyT then NONE else SOME (raw_atp_type_of_typ type_enc T) (* This shouldn't clash with anything else. *) val uncurried_alias_sep = "\000" @@ -934,29 +929,23 @@ val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep -fun generic_mangled_type_name f (AType (name, [])) = f name - | generic_mangled_type_name f (AType (name, tys)) = - f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) - ^ ")" +fun generic_mangled_type_name f (AType ((name, _), [])) = f name + | generic_mangled_type_name f (AType ((name, _), tys)) = + f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")" | generic_mangled_type_name _ _ = raise Fail "unexpected type" -fun mangled_type type_enc = - generic_mangled_type_name fst o raw_ho_type_of_typ type_enc +fun mangled_type type_enc = generic_mangled_type_name fst o raw_atp_type_of_typ type_enc fun make_native_type s = - if s = tptp_bool_type orelse s = tptp_fun_type orelse - s = tptp_individual_type then - s - else - native_type_prefix ^ ascii_of s + if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s + else native_type_prefix ^ ascii_of s -fun native_ho_type_of_raw_ho_type type_enc pred_sym ary = +fun native_atp_type_of_raw_atp_type type_enc pred_sym ary = let fun to_mangled_atype ty = - AType ((make_native_type (generic_mangled_type_name fst ty), - generic_mangled_type_name snd ty), []) - fun to_poly_atype (AType (name, tys)) = - AType (name, map to_poly_atype tys) + AType (((make_native_type (generic_mangled_type_name fst ty), + generic_mangled_type_name snd ty), []), []) + fun to_poly_atype (AType ((name, clss), tys)) = AType ((name, clss), map to_poly_atype tys) | to_poly_atype _ = raise Fail "unexpected type" val to_atype = if is_type_enc_polymorphic type_enc then to_poly_atype @@ -965,14 +954,13 @@ fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys | to_fo _ _ = raise Fail "unexpected type" - fun to_ho (ty as AType ((s, _), tys)) = + fun to_ho (ty as AType (((s, _), _), tys)) = if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty | to_ho _ = raise Fail "unexpected type" in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end -fun native_ho_type_of_typ type_enc pred_sym ary = - native_ho_type_of_raw_ho_type type_enc pred_sym ary - o raw_ho_type_of_typ type_enc +fun native_atp_type_of_typ type_enc pred_sym ary = + native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc (* Make atoms for sorted type variables. *) fun generic_add_sorts_on_type _ [] = I @@ -986,10 +974,9 @@ fun process_type_args type_enc T_args = if is_type_enc_native type_enc then - (map (native_ho_type_of_typ type_enc false 0) T_args, []) + (map (native_atp_type_of_typ type_enc false 0) T_args, []) else - ([], map_filter (Option.map atp_term_of_ho_type - o ho_type_of_type_arg type_enc) T_args) + ([], map_filter (Option.map atp_term_of_atp_type o atp_type_of_type_arg type_enc) T_args) fun class_atom type_enc (cl, T) = let @@ -998,9 +985,9 @@ val tm_args = tm_args @ (case type_enc of - Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) => - [ATerm ((TYPE_name, ty_args), [])] - | _ => []) + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) => + [ATerm ((TYPE_name, ty_args), [])] + | _ => []) in AAtom (ATerm ((cl, ty_args), tm_args)) end fun class_atoms type_enc (cls, T) = @@ -1070,7 +1057,7 @@ ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end fun mangled_const_name type_enc = - map_filter (ho_type_of_type_arg type_enc) + map_filter (atp_type_of_type_arg type_enc) #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = @@ -1788,11 +1775,9 @@ #> (case type_enc of Native (_, poly, _) => mk_atyquant AForall (map (fn TVar (z as (_, S)) => - (AType (tvar_name z, []), - if poly = Type_Class_Polymorphic then - map (`make_class) (normalize_classes S) - else - [])) Ts) + (AType ((tvar_name z, []), []), + if poly = Type_Class_Polymorphic then map (`make_class) (normalize_classes S) + else [])) Ts) | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))) fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = @@ -2065,11 +2050,10 @@ end fun do_bound_type ctxt mono type_enc = - case type_enc of + (case type_enc of Native (_, _, level) => - fused_type ctxt mono level 0 #> native_ho_type_of_typ type_enc false 0 - #> SOME - | _ => K NONE + fused_type ctxt mono level 0 #> native_atp_type_of_typ type_enc false 0 #> SOME + | _ => K NONE) fun tag_with_type ctxt mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) @@ -2103,7 +2087,7 @@ map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => if is_type_enc_higher_order type_enc then - AAbs (((name, native_ho_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *) + AAbs (((name, native_atp_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *) term Elsewhere tm), map (term Elsewhere) args) else raise Fail "unexpected lambda-abstraction" @@ -2130,8 +2114,7 @@ else NONE fun do_formula pos (ATyQuant (q, xs, phi)) = - ATyQuant (q, map (apfst (native_ho_type_of_typ type_enc false 0)) xs, - do_formula pos phi) + ATyQuant (q, map (apfst (native_atp_type_of_typ type_enc false 0)) xs, do_formula pos phi) | do_formula pos (AQuant (q, xs, phi)) = let val phi = phi |> do_formula pos @@ -2193,10 +2176,8 @@ fun line_of_tcon_clause type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, - map (fn (cls, T) => - (T |> dest_TVar |> tvar_name, map (`make_class) cls)) - prems, - native_ho_type_of_typ type_enc false 0 T, `make_class cl) + map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems, + native_atp_type_of_typ type_enc false 0 T, `make_class cl) else Formula ((tcon_clause_prefix ^ name, ""), Axiom, mk_ahorn (maps (class_atoms type_enc) prems) @@ -2220,10 +2201,10 @@ fun line j (cl, T) = if type_classes then Class_Memb (class_memb_prefix ^ string_of_int j, [], - native_ho_type_of_typ type_enc false 0 T, `make_class cl) + native_atp_type_of_typ type_enc false 0 T, `make_class cl) else Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis, - class_atom type_enc (cl, T), NONE, []) + class_atom type_enc (cl, T), NONE, []) val membs = fold (union (op =)) (map #atomic_types facts) [] |> class_membs_of_types type_enc add_sorts_on_tfree @@ -2430,7 +2411,7 @@ in Sym_Decl (sym_decl_prefix ^ s, (s, s'), T |> fused_type ctxt mono (level_of_type_enc type_enc) ary - |> native_ho_type_of_typ type_enc pred_sym ary + |> native_atp_type_of_typ type_enc pred_sym ary |> not (null T_args) ? curry APi (map (tvar_name o dest_TVar) T_args)) end @@ -2572,7 +2553,7 @@ fun datatype_of_ctrs (ctrs as (_, T1) :: _) = let val ctrs' = map do_ctr ctrs in if forall is_some ctrs' then - SOME (native_ho_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs') + SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs') else NONE end @@ -2583,8 +2564,8 @@ [] | datatypes_of_sym_table _ _ _ _ _ _ = [] -fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) = - let val xs = map (fn AType (name, []) => name) ty_args in +fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) = + let val xs = map (fn AType ((name, _), []) => name) ty_args in Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs) end @@ -2685,7 +2666,7 @@ if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I fun do_class name = apfst (apfst (do_sym name ())) val do_bound_tvars = fold do_class o snd - fun do_type (AType (name, tys)) = + fun do_type (AType ((name, _), 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 diff -r 6e78f87ed554 -r d9ab86c044fd src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 19 15:04:21 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 19 15:47:17 2013 +0100 @@ -258,11 +258,11 @@ fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f -fun parse_sort x = scan_general_id x -and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x +fun parse_class x = scan_general_id x +and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x fun parse_type x = - (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}") + (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [] -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] >> AType) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x @@ -530,7 +530,7 @@ fun map_term_names_in_atp_proof f = let - fun map_type (AType (s, tys)) = AType (f s, map map_type tys) + fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys) | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) diff -r 6e78f87ed554 -r d9ab86c044fd src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 15:04:21 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 15:47:17 2013 +0100 @@ -108,15 +108,21 @@ TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end +exception ATP_CLASS of string list exception ATP_TYPE of string atp_type list exception ATP_TERM of (string, string atp_type) atp_term list exception ATP_FORMULA of (string, string, (string, string atp_type) atp_term, string) atp_formula list exception SAME of unit +fun class_of_atp_class cls = + (case unprefix_and_unascii class_prefix cls of + SOME s => s + | NONE => raise ATP_CLASS [cls]) + (* 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_of_atp_type ctxt (ty as AType (a, tys)) = +fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = let val Ts = map (typ_of_atp_type ctxt) tys in (case unprefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) @@ -130,10 +136,12 @@ (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". Sometimes variables from the ATP are indistinguishable from Isabelle variables, which forces us to use a type parameter in all cases. *) - Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS))) + Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), + (if null clss then HOLogic.typeS + else map class_of_atp_class clss)))) end -fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType (s, map atp_type_of_atp_term us) +fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us) fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term