# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID a5ab5964065fd85b33bdc88d33b01f0438eafb4c # Parent 9aa0fad4e864e9157d24dc0376c2f49b6e8a4a67 implement polymorphic DFG output, without type classes for now diff -r 9aa0fad4e864 -r a5ab5964065f src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200 @@ -13,6 +13,7 @@ datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c) formula = + ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula | AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula | AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c @@ -20,7 +21,7 @@ datatype 'a ho_type = AType of 'a * 'a ho_type list | AFun of 'a ho_type * 'a ho_type | - ATyAbs of 'a list * 'a ho_type + APi of 'a list * 'a ho_type type term_order = {is_lpo : bool, @@ -145,6 +146,7 @@ datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c) formula = + ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula | AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula | AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c @@ -152,7 +154,7 @@ datatype 'a ho_type = AType of 'a * 'a ho_type list | AFun of 'a ho_type * 'a ho_type | - ATyAbs of 'a list * 'a ho_type + APi of 'a list * 'a ho_type type term_order = {is_lpo : bool, @@ -284,23 +286,27 @@ fun formula_fold pos f = let fun fld pos (AQuant (_, _, phi)) = fld pos phi + | fld pos (ATyQuant (_, _, phi)) = fld pos phi | fld pos (AConn conn) = aconn_fold pos fld conn | fld pos (AAtom tm) = f pos tm in fld pos end fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) + | formula_map f (ATyQuant (q, xs, phi)) = ATyQuant (q, xs, formula_map f phi) | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) -fun is_function_type (AFun (_, ty)) = is_function_type ty +fun is_function_type (APi (_, ty)) = is_function_type ty + | is_function_type (AFun (_, ty)) = is_function_type ty | is_function_type (AType (s, _)) = s <> tptp_type_of_types andalso s <> tptp_bool_type | is_function_type _ = false -fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty +fun is_predicate_type (APi (_, ty)) = is_predicate_type ty + | is_predicate_type (AFun (_, ty)) = is_predicate_type ty | is_predicate_type (AType (s, _)) = (s = tptp_bool_type) | is_predicate_type _ = false -fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty - | is_nontrivial_predicate_type _ = false +fun is_nontrivial_predicate_type (AType _) = false + | is_nontrivial_predicate_type ty = is_predicate_type ty fun is_format_higher_order (THF _) = true | is_format_higher_order _ = false @@ -315,13 +321,14 @@ | tptp_string_for_role Hypothesis = "hypothesis" | tptp_string_for_role Conjecture = "conjecture" -fun tptp_string_for_app format func args = - if is_format_higher_order format then - "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" - else - func ^ "(" ^ commas args ^ ")" +fun tptp_string_for_app _ func [] = func + | tptp_string_for_app format func args = + if is_format_higher_order format then + "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" + else + func ^ "(" ^ commas args ^ ")" -fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty) +fun flatten_type (APi (tys, ty)) = APi (tys, flatten_type ty) | flatten_type (ty as AFun (ty1 as AType _, ty2)) = (case flatten_type ty2 of AFun (ty' as AType (s, tys), ty) => @@ -334,6 +341,9 @@ val dfg_individual_type = "iii" (* cannot clash *) +val suffix_type_of_types = + suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types) + fun str_for_type format ty = let val dfg = case format of DFG _ => true | _ => false @@ -352,10 +362,12 @@ (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^ (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2 |> not rhs ? enclose "(" ")" - | str _ (ATyAbs (ss, ty)) = - tptp_pi_binder ^ "[" ^ - commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) - ss) ^ "]: " ^ str false ty + | str _ (APi (ss, ty)) = + if dfg then + "[" ^ commas ss ^ "], " ^ str true ty + else + tptp_pi_binder ^ "[" ^ commas (map suffix_type_of_types ss) ^ "]: " ^ + str false ty in str true ty end fun string_for_type (format as THF _) ty = str_for_type format ty @@ -380,8 +392,7 @@ "") fun tptp_string_for_term _ (ATerm ((s, []), [])) = s - | tptp_string_for_term _ (ATerm ((s, tys), [])) = s (* ### FIXME *) - | tptp_string_for_term format (ATerm ((s, tys), ts)) = (* ### FIXME *) + | tptp_string_for_term format (ATerm ((s, tys), ts)) = (if s = tptp_empty_list then (* used for lists in the optional "source" field of a derivation *) "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]" @@ -405,7 +416,10 @@ tptp_string_for_term format tm ^ "" |> enclose "(" ")") (map (tptp_string_for_term format) args) - | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts)) + | _ => + tptp_string_for_app format s + (map (string_for_type format) tys + @ map (tptp_string_for_term format) ts)) | tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) = tptp_string_for_app format ("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ @@ -413,7 +427,12 @@ (map (tptp_string_for_term format) args) | tptp_string_for_term _ _ = raise Fail "unexpected term in first-order format" -and tptp_string_for_formula format (AQuant (q, xs, phi)) = +and tptp_string_for_formula format (ATyQuant (q, xs, phi)) = + tptp_string_for_quantifier q ^ + "[" ^ commas (map (suffix_type_of_types o string_for_type format) xs) ^ + "]: " ^ tptp_string_for_formula format phi + |> enclose "(" ")" + | tptp_string_for_formula format (AQuant (q, xs, phi)) = tptp_string_for_quantifier q ^ "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ tptp_string_for_formula format phi @@ -459,14 +478,21 @@ "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: map (tptp_string_for_problem_line format) lines) -fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty - | arity_of_type _ = 0 +fun arity_of_type (APi (tys, ty)) = + arity_of_type ty |>> Integer.add (length tys) + | arity_of_type (AFun (_, ty)) = arity_of_type ty ||> Integer.add 1 + | arity_of_type _ = (0, 0) -fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 - | binder_atypes _ = [] +fun string_of_arity (0, n) = string_of_int n + | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n + +fun strip_atype (APi (tys, ty)) = strip_atype ty |>> apfst (append tys) + | strip_atype (AFun (ty1, ty2)) = strip_atype ty2 |>> apsnd (cons ty1) + | strip_atype ty = (([], []), ty) fun dfg_string_for_formula poly gen_simp info = let + val str_for_typ = string_for_type (DFG poly) fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of @@ -481,7 +507,8 @@ else if s = tptp_true then "true" else if s = tptp_false then "false" else s) ^ - (if null tys then "" else "<...>") (* ### FIXME *) ^ + (if null tys then "" + else "<" ^ commas (map (string_for_type (DFG poly)) tys) ^ ">") ^ (if null tms then "" else "(" ^ commas (map (str_for_term false) tms) ^ ")") | str_for_term _ _ = raise Fail "unexpected term in first-order format" @@ -492,8 +519,11 @@ | str_for_conn _ AOr = "or" | str_for_conn _ AImplies = "implies" | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level - fun str_for_formula top_level (AQuant (q, xs, phi)) = - str_for_quant q ^ "(" ^ "[" ^ + fun str_for_formula top_level (ATyQuant (q, xs, phi)) = + str_for_quant q ^ "_sorts([" ^ commas (map str_for_typ xs) ^ + "], " ^ str_for_formula top_level phi ^ ")" + | str_for_formula top_level (AQuant (q, xs, phi)) = + str_for_quant q ^ "([" ^ commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^ str_for_formula top_level phi ^ ")" | str_for_formula top_level (AConn (c, phis)) = @@ -507,13 +537,19 @@ fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = let - fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")" - fun ary sym = curry spair sym o arity_of_type - fun fun_typ sym ty = - "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")." + 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 [] sym = sym + | ty_ary tys sym = "(" ^ sym ^ ", " ^ string_of_int (length tys) ^ ")" + fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")." fun pred_typ sym ty = - "predicate(" ^ - commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")." + let + val ((ty_vars, tys), _) = strip_atype ty + val (ty_vars, tys) = + strip_atype ty |> fst + |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"]) + in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end fun formula pred (Formula (ident, kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in @@ -528,23 +564,27 @@ fun filt f = problem |> map (map_filter f o snd) |> filter_out null val func_aries = filt (fn Decl (_, sym, ty) => - if is_function_type ty then SOME (ary sym ty) else NONE + if is_function_type ty then SOME (tm_ary sym ty) else NONE | _ => NONE) |> flat |> commas |> maybe_enclose "functions [" "]." val pred_aries = filt (fn Decl (_, sym, ty) => - if is_predicate_type ty then SOME (ary sym ty) else NONE + if is_predicate_type ty then SOME (tm_ary sym ty) else NONE | _ => NONE) |> flat |> commas |> maybe_enclose "predicates [" "]." val sorts = - filt (fn Decl (_, sym, AType (s, [])) => - if s = tptp_type_of_types then SOME sym else NONE + filt (fn Decl (_, sym, ty) => + (case strip_atype ty of + (([], tys), AType (s, [])) => + if s = tptp_type_of_types then SOME (ty_ary tys sym) else NONE + | _ => NONE) | _ => NONE) @ [[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 = (if gen_weights then ord_info else []) - |> map spair |> commas |> maybe_enclose "weights [" "]." + |> map (spair o apsnd string_of_int) |> commas + |> maybe_enclose "weights [" "]." val syms = [func_aries, pred_aries, do_term_order_weights, sorts] val func_sigs = filt (fn Decl (_, sym, ty) => @@ -798,15 +838,18 @@ fun nice_type (AType (name, tys)) = nice_name name ##>> pool_map nice_type tys #>> AType | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun - | nice_type (ATyAbs (names, ty)) = - pool_map nice_name names ##>> nice_type ty #>> ATyAbs + | nice_type (APi (names, ty)) = + pool_map nice_name names ##>> nice_type ty #>> APi fun nice_term (ATerm ((name, tys), ts)) = nice_name name ##>> pool_map nice_type tys ##>> pool_map nice_term ts #>> ATerm | nice_term (AAbs (((name, ty), tm), args)) = nice_name name ##>> nice_type ty ##>> nice_term tm ##>> pool_map nice_term args #>> AAbs - fun nice_formula (AQuant (q, xs, phi)) = + fun nice_formula (ATyQuant (q, xs, phi)) = + pool_map nice_type xs ##>> nice_formula phi + #>> (fn (xs, phi) => ATyQuant (q, xs, phi)) + | nice_formula (AQuant (q, xs, phi)) = pool_map nice_name (map fst xs) ##>> pool_map (fn NONE => pair NONE | SOME ty => nice_type ty #>> SOME) (map snd xs) diff -r 9aa0fad4e864 -r a5ab5964065f src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 @@ -359,9 +359,9 @@ fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v fun make_fixed_var x = fixed_var_prefix ^ ascii_of x -fun make_schematic_type_var (x, i) = - tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) +fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i)) +fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s)) +fun tvar_name (x as (s, _)) = (make_tvar x, s) (* "HOL.eq" and choice are mapped to the ATP's equivalents *) local @@ -407,32 +407,36 @@ | _ => I) fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty +val tvar_a_str = "'a" +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS) +val tvar_a_name = tvar_name (tvar_a_str, 0) +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]) + (** Definitions and functions for FOL clauses and formulas for TPTP **) (** Isabelle arities **) -type arity_atom = name * name * name list - val type_class = the_single @{sort type} type arity_clause = {name : string, - prem_atoms : arity_atom list, - concl_atom : arity_atom} + prems : (string * typ) list, + concl : string * typ} -fun add_prem_atom tvar = - fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, [])) +fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T)) (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *) -fun make_axiom_arity_clause (tcons, name, (cls, args)) = +fun make_axiom_arity_clause (tc, name, (class, args)) = let - val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args) - val tvars_srts = ListPair.zip (tvars, args) + val tvars = + map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type})) + (1 upto length args) in - {name = name, - prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts, - concl_atom = (`make_type_class cls, `make_fixed_type_const tcons, - tvars ~~ tvars)} + {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [], + concl = (class, Type (tc, tvars))} end fun arity_clause _ _ (_, []) = [] @@ -487,8 +491,8 @@ type class_rel_clause = {name : string, - subclass : name, - superclass : name} + subclass : string, + superclass : string} (* Generate all pairs (sub, super) such that sub is a proper subclass of super in theory "thy". *) @@ -501,8 +505,7 @@ in fold add_supers subs [] end fun make_class_rel_clause (sub, super) = - {name = sub ^ "_" ^ super, subclass = `make_type_class sub, - superclass = `make_type_class 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) @@ -528,14 +531,6 @@ fun atomic_types_of T = fold_atyps (insert (op =)) T [] -val tvar_a_str = "'a" -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS) -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str) -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]) - fun new_skolem_const_name s num_T_args = [new_skolem_const_prefix, s, string_of_int num_T_args] |> Long_Name.implode @@ -872,79 +867,9 @@ end end -(* Make atoms for sorted type variables. *) -fun generic_add_sorts_on_type (_, []) = I - | generic_add_sorts_on_type ((x, i), s :: ss) = - generic_add_sorts_on_type ((x, i), ss) - #> (if s = the_single @{sort HOL.type} then - I - else if i = ~1 then - insert (op =) (`make_type_class s, `make_fixed_type_var x) - else - insert (op =) (`make_type_class s, - (make_schematic_type_var (x, i), x))) -fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S) - | add_sorts_on_tfree _ = I -fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z - | add_sorts_on_tvar _ = I - -fun type_class_formula type_enc class arg = - AAtom (ATerm ((class, []), arg :: - (case type_enc of - Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) => - [ATerm ((TYPE_name, []), [arg])] - | _ => []))) -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 - |> map (fn (class, name) => - type_class_formula type_enc class (ATerm ((name, []), []))) - -fun mk_aconns c phis = - let val (phis', phi') = split_last phis in - fold_rev (mk_aconn c) phis' phi' - end -fun mk_ahorn [] phi = phi - | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) -fun mk_aquant _ [] phi = phi - | mk_aquant q xs (phi as AQuant (q', xs', phi')) = - if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) - | mk_aquant q xs phi = AQuant (q, xs, phi) - -fun close_universally add_term_vars phi = - let - fun add_formula_vars bounds (AQuant (_, xs, phi)) = - add_formula_vars (map fst xs @ bounds) phi - | add_formula_vars bounds (AConn (_, phis)) = - fold (add_formula_vars bounds) phis - | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm - in mk_aquant AForall (add_formula_vars [] phi []) phi end - -fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) = - (if is_tptp_variable s andalso - not (String.isPrefix tvar_prefix s) andalso - not (member (op =) bounds name) then - insert (op =) (name, NONE) - else - I) - #> fold (add_term_vars bounds) tms - | add_term_vars bounds (AAbs (((name, _), tm), args)) = - add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args -fun close_formula_universally phi = close_universally add_term_vars phi - -fun add_iterm_vars bounds (IApp (tm1, tm2)) = - fold (add_iterm_vars bounds) [tm1, tm2] - | add_iterm_vars _ (IConst _) = I - | add_iterm_vars bounds (IVar (name, T)) = - not (member (op =) bounds name) ? insert (op =) (name, SOME T) - | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm - -fun close_iformula_universally phi = close_universally add_iterm_vars phi - val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) val fused_infinite_type = Type (fused_infinite_type_name, []) -fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s) - fun ho_term_from_typ type_enc = let fun term (Type (s, Ts)) = @@ -957,7 +882,7 @@ else `make_fixed_type_const s, []), map term Ts) - | term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), []) + | term (TFree (s, _)) = ATerm ((`make_tfree s, []), []) | term (TVar (x, _)) = ATerm ((tvar_name x, []), []) in term end @@ -1011,6 +936,87 @@ ho_type_from_ho_term type_enc pred_sym ary o ho_term_from_typ type_enc +(* Make atoms for sorted type variables. *) +fun generic_add_sorts_on_type _ [] = I + | generic_add_sorts_on_type T (s :: ss) = + generic_add_sorts_on_type T ss + #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T)) +fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S + | add_sorts_on_tfree _ = I +fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S + | add_sorts_on_tvar _ = I + +fun process_type_args type_enc T_args = + if is_type_enc_native type_enc then + (map (ho_type_from_typ type_enc false 0) T_args, []) + else + ([], map_filter (ho_term_for_type_arg type_enc) T_args) + +fun type_class_atom type_enc (class, T) = + let + val class = `make_type_class class + val (ty_args, tm_args) = process_type_args type_enc [T] + val tm_args = + tm_args @ + (case type_enc of + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) => + [ATerm ((TYPE_name, ty_args), [])] + | _ => []) + 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 + |> 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_ahorn [] phi = phi + | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) + +fun mk_aquant _ [] phi = phi + | mk_aquant q xs (phi as AQuant (q', xs', phi')) = + if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) + | mk_aquant q xs phi = AQuant (q, xs, phi) + +fun mk_atyquant _ [] phi = phi + | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) = + if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi) + | mk_atyquant q xs phi = ATyQuant (q, xs, phi) + +fun close_universally add_term_vars phi = + let + fun add_formula_vars bounds (ATyQuant (_, _, phi)) = + add_formula_vars bounds phi + | add_formula_vars bounds (AQuant (_, xs, phi)) = + add_formula_vars (map fst xs @ bounds) phi + | add_formula_vars bounds (AConn (_, phis)) = + fold (add_formula_vars bounds) phis + | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm + in mk_aquant AForall (add_formula_vars [] phi []) phi end + +fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) = + (if is_tptp_variable s andalso + not (String.isPrefix tvar_prefix s) andalso + not (member (op =) bounds name) then + insert (op =) (name, NONE) + else + I) + #> fold (add_term_vars bounds) tms + | add_term_vars bounds (AAbs (((name, _), tm), args)) = + add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args +fun close_formula_universally phi = close_universally add_term_vars phi + +fun add_iterm_vars bounds (IApp (tm1, tm2)) = + fold (add_iterm_vars bounds) [tm1, tm2] + | add_iterm_vars _ (IConst _) = I + | add_iterm_vars bounds (IVar (name, T)) = + not (member (op =) bounds name) ? insert (op =) (name, SOME T) + | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm + +fun close_iformula_universally phi = close_universally add_iterm_vars phi + fun aliased_uncurried ary (s, s') = (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) fun unaliased_uncurried (s, s') = @@ -1718,18 +1724,16 @@ @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))] |> map (apsnd (map (apsnd zero_var_indexes))) -fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types - | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) = - SOME atype_of_types (* ### FIXME *) - | atype_of_type_vars _ = NONE - fun bound_tvars type_enc sorts Ts = - (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)) - #> mk_aquant AForall - (map_filter (fn TVar (x as (s, _), _) => - SOME ((make_schematic_type_var x, s), - atype_of_type_vars type_enc) - | _ => NONE) Ts) + case filter is_TVar Ts of + [] => I + | Ts => + (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)) + #> (if is_type_enc_native type_enc then + mk_atyquant AForall + (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts) + else + mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts)) fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) @@ -1994,11 +1998,9 @@ | should_generate_tag_bound_decl _ _ _ _ _ = false fun mk_aterm type_enc name T_args args = -(* ### FIXME - if is_type_enc_polymorphic type_enc then - ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args) - else *) - ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args) + let val (ty_args, tm_args) = process_type_args type_enc T_args in + ATerm ((name, ty_args), tm_args @ args) + end fun do_bound_type ctxt mono type_enc = case type_enc of @@ -2032,7 +2034,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, ho_type_from_typ type_enc true 0 T), + AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T), term Elsewhere tm), map (term Elsewhere) args) else raise Fail "unexpected lambda-abstraction" @@ -2063,7 +2065,10 @@ in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end else NONE - fun do_formula pos (AQuant (q, xs, phi)) = + fun do_formula pos (ATyQuant (q, xs, phi)) = + ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs, + do_formula pos phi) + | do_formula pos (AQuant (q, xs, phi)) = let val phi = phi |> do_formula pos val universal = Option.map (q = AExists ? not) pos @@ -2108,29 +2113,25 @@ fun formula_line_for_class_rel_clause type_enc ({name, subclass, superclass, ...} : class_rel_clause) = - let val ty_arg = ATerm ((tvar_a_name, []), []) in - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, - AConn (AImplies, - [type_class_formula type_enc subclass ty_arg, - type_class_formula type_enc superclass ty_arg]) - |> mk_aquant AForall - [(tvar_a_name, atype_of_type_vars type_enc)], + Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, + AConn (AImplies, + [type_class_atom type_enc (subclass, tvar_a), + type_class_atom type_enc (superclass, tvar_a)]) + |> bound_tvars type_enc false [tvar_a], + NONE, isabelle_info inductiveN helper_rank) + +fun formula_line_for_arity_clause type_enc + ({name, prems, concl} : arity_clause) = + let + val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) [] + in + Formula (arity_clause_prefix ^ name, Axiom, + mk_ahorn (map (type_class_atom type_enc) prems) + (type_class_atom type_enc concl) + |> bound_tvars type_enc true atomic_Ts, NONE, isabelle_info inductiveN helper_rank) end -fun formula_from_arity_atom type_enc (class, t, args) = - ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args) - |> type_class_formula type_enc class - -fun formula_line_for_arity_clause type_enc - ({name, prem_atoms, concl_atom} : arity_clause) = - Formula (arity_clause_prefix ^ name, Axiom, - mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) - (formula_from_arity_atom type_enc concl_atom) - |> mk_aquant AForall - (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), - NONE, isabelle_info inductiveN helper_rank) - fun formula_line_for_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) = Formula (conjecture_prefix ^ name, role, @@ -2140,21 +2141,14 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) -fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true - | type_enc_needs_free_types (Native _) = false - | type_enc_needs_free_types _ = true - -fun formula_line_for_free_type j phi = - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, []) fun formula_lines_for_free_types type_enc (facts : ifact list) = - if type_enc_needs_free_types type_enc then - let - val phis = - fold (union (op =)) (map #atomic_types facts) [] - |> formulas_for_types type_enc add_sorts_on_tfree - in map2 formula_line_for_free_type (0 upto length phis - 1) phis end - else - [] + let + fun line j phi = + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, []) + val phis = + fold (union (op =)) (map #atomic_types facts) [] + |> formulas_for_types type_enc add_sorts_on_tfree + in map2 line (0 upto length phis - 1) phis end (** Symbol declarations **) @@ -2162,11 +2156,11 @@ let val name as (s, _) = `make_type_class s in Decl (sym_decl_prefix ^ s, name, if order = First_Order then - ATyAbs ([tvar_a_name], - if phantoms = Without_Phantom_Type_Vars then - AFun (a_itself_atype, bool_atype) - else - bool_atype) + APi ([tvar_a_name], + if phantoms = Without_Phantom_Type_Vars then + AFun (a_itself_atype, bool_atype) + else + bool_atype) else AFun (atype_of_types, bool_atype)) end @@ -2207,7 +2201,8 @@ #> fold add_iterm_syms args end val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift - fun add_formula_var_types (AQuant (_, xs, phi)) = + fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi + | add_formula_var_types (AQuant (_, xs, phi)) = fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs #> add_formula_var_types phi | add_formula_var_types (AConn (_, phis)) = @@ -2359,7 +2354,7 @@ T |> fused_type ctxt mono (level_of_type_enc type_enc) ary |> ho_type_from_typ type_enc pred_sym ary |> not (null T_args) - ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args)) + ? curry APi (map (tvar_name o fst o dest_TVar) T_args)) end fun honor_conj_sym_role in_conj = @@ -2574,8 +2569,9 @@ else individual_atype | _ => individual_atype - fun typ 0 = if pred_sym then bool_atype else ind - | typ ary = AFun (ind, typ (ary - 1)) + fun typ 0 0 = if pred_sym then bool_atype else ind + | typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1)) + | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary) in typ end fun nary_type_constr_type n = @@ -2592,13 +2588,15 @@ do_sym name (fn () => nary_type_constr_type (length tys)) #> fold do_type tys | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 - | do_type (ATyAbs (_, ty)) = do_type ty + | do_type (APi (_, ty)) = do_type ty fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) = - do_sym name (fn _ => default_type type_enc pred_sym s (length tms)) + do_sym name + (fn _ => default_type type_enc pred_sym s (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 (AQuant (_, xs, phi)) = + fun do_formula (ATyQuant (_, _, phi)) = 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 | do_formula (AAtom tm) = do_term true tm @@ -2794,16 +2792,19 @@ else (s, tms) | make_head_roll _ = ("", []) -fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi +fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi + | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis | strip_up_to_predicator (AAtom tm) = [strip_predicator tm] -fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi +fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi + | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) = strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1) | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi)) -fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi +fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi + | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi | strip_iff_etc (AConn (AIff, [phi1, phi2])) = pairself strip_up_to_predicator (phi1, phi2) | strip_iff_etc _ = ([], [])