# HG changeset patch # User blanchet # Date 1335384033 -7200 # Node ID 0b2b7ff318675e722dc06949d5bfb2e07cfb1c39 # Parent 857b20f4a4b6a97c39edbcb4248d96cdf799eb7e don't use the native choice operator if the type encoding isn't higher-order diff -r 857b20f4a4b6 -r 0b2b7ff31867 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Apr 25 22:00:33 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Apr 25 22:00:33 2012 +0200 @@ -117,7 +117,6 @@ val is_function_type : string ho_type -> bool val is_predicate_type : string ho_type -> bool val is_format_higher_order : atp_format -> bool - val is_format_typed : atp_format -> bool val lines_for_atp_problem : atp_format -> term_order -> (unit -> (string * int) list) -> string problem -> string list diff -r 857b20f4a4b6 -r 0b2b7ff31867 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 25 22:00:33 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 25 22:00:33 2012 +0200 @@ -117,6 +117,58 @@ type name = string * string +datatype scope = Global | Local | Assum | Chained +datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def +type stature = scope * status + +datatype order = + First_Order | + Higher_Order of thf_flavor +datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic +datatype strictness = Strict | Non_Strict +datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars +datatype type_level = + All_Types | + Noninf_Nonmono_Types of strictness * granularity | + Fin_Nonmono_Types of granularity | + Const_Arg_Types | + No_Types + +datatype type_enc = + Native of order * polymorphism * type_level | + Guards of polymorphism * type_level | + Tags of polymorphism * type_level + +fun is_type_enc_native (Native _) = true + | is_type_enc_native _ = false +fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true + | is_type_enc_higher_order _ = false + +fun polymorphism_of_type_enc (Native (_, poly, _)) = poly + | polymorphism_of_type_enc (Guards (poly, _)) = poly + | polymorphism_of_type_enc (Tags (poly, _)) = poly + +fun level_of_type_enc (Native (_, _, level)) = level + | level_of_type_enc (Guards (_, level)) = level + | level_of_type_enc (Tags (_, level)) = level + +fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain + | granularity_of_type_level (Fin_Nonmono_Types grain) = grain + | granularity_of_type_level _ = All_Vars + +fun is_type_level_quasi_sound All_Types = true + | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true + | is_type_level_quasi_sound _ = false +val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc + +fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true + | is_type_level_fairly_sound level = is_type_level_quasi_sound level +val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc + +fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true + | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true + | is_type_level_monotonicity_based _ = false + val no_lamsN = "no_lams" (* used internally; undocumented *) val hide_lamsN = "hide_lams" val liftingN = "lifting" @@ -316,7 +368,7 @@ fun default c = const_prefix ^ lookup_const c in fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal - | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c = + | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c = if c = choice_const then tptp_choice else default c | make_fixed_const _ c = default c end @@ -518,83 +570,36 @@ (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort infomation. *) -fun iterm_from_term thy format bs (P $ Q) = +fun iterm_from_term thy type_enc bs (P $ Q) = let - val (P', P_atomics_Ts) = iterm_from_term thy format bs P - val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q + val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P + val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end - | iterm_from_term thy format _ (Const (c, T)) = - (IConst (`(make_fixed_const (SOME format)) c, T, + | iterm_from_term thy type_enc _ (Const (c, T)) = + (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_typargs thy (c, T)), atomic_types_of T) | iterm_from_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T) - | iterm_from_term _ format _ (Var (v as (s, _), T)) = + | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let val Ts = T |> strip_type |> swap |> op :: val s' = new_skolem_const_name s (length Ts) - in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end + in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end else IVar ((make_schematic_var v, s), T), atomic_types_of T) | iterm_from_term _ _ bs (Bound j) = nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T)) - | iterm_from_term thy format bs (Abs (s, T, t)) = + | iterm_from_term thy type_enc bs (Abs (s, T, t)) = let fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string val s = vary s val name = `make_bound_var s - val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t + val (tm, atomic_Ts) = + iterm_from_term thy type_enc ((s, (name, T)) :: bs) t in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end -datatype scope = Global | Local | Assum | Chained -datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def -type stature = scope * status - -datatype order = First_Order | Higher_Order -datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic -datatype strictness = Strict | Non_Strict -datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars -datatype type_level = - All_Types | - Noninf_Nonmono_Types of strictness * granularity | - Fin_Nonmono_Types of granularity | - Const_Arg_Types | - No_Types - -datatype type_enc = - Native of order * polymorphism * type_level | - Guards of polymorphism * type_level | - Tags of polymorphism * type_level - -fun is_type_enc_higher_order (Native (Higher_Order, _, _)) = true - | is_type_enc_higher_order _ = false - -fun polymorphism_of_type_enc (Native (_, poly, _)) = poly - | polymorphism_of_type_enc (Guards (poly, _)) = poly - | polymorphism_of_type_enc (Tags (poly, _)) = poly - -fun level_of_type_enc (Native (_, _, level)) = level - | level_of_type_enc (Guards (_, level)) = level - | level_of_type_enc (Tags (_, level)) = level - -fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain - | granularity_of_type_level (Fin_Nonmono_Types grain) = grain - | granularity_of_type_level _ = All_Vars - -fun is_type_level_quasi_sound All_Types = true - | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true - | is_type_level_quasi_sound _ = false -val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc - -fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true - | is_type_level_fairly_sound level = is_type_level_quasi_sound level -val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc - -fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true - | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true - | is_type_level_monotonicity_based _ = false - (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and Mirabelle. *) val queries = ["?", "_query"] @@ -643,11 +648,12 @@ | ("native_higher", (SOME poly, _)) => (case (poly, level) of (Polymorphic, All_Types) => - Native (Higher_Order, Polymorphic, All_Types) + Native (Higher_Order THF_With_Choice, Polymorphic, All_Types) | (_, Noninf_Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => if granularity_of_type_level level = All_Vars then - Native (Higher_Order, Mangled_Monomorphic, level) + Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, + level) else raise Same.SAME | _ => raise Same.SAME) @@ -669,9 +675,16 @@ | _ => raise Same.SAME) handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") -fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) (Native (order, _, level)) = - Native (order, Mangled_Monomorphic, level) - | adjust_type_enc (THF _) type_enc = type_enc +fun adjust_order THF_Without_Choice (Higher_Order _) = + Higher_Order THF_Without_Choice + | adjust_order _ type_enc = type_enc + +fun adjust_type_enc (THF (TPTP_Polymorphic, _, flavor)) + (Native (order, poly, level)) = + Native (adjust_order flavor order, poly, level) + | adjust_type_enc (THF (TPTP_Monomorphic, _, flavor)) + (Native (order, _, level)) = + Native (adjust_order flavor order, Mangled_Monomorphic, level) | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (DFG DFG_Sorted) (Native (_, _, level)) = @@ -923,14 +936,14 @@ fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s) -fun ho_term_from_typ format type_enc = +fun ho_term_from_typ type_enc = let fun term (Type (s, Ts)) = ATerm (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_format_typed format then + is_type_enc_native type_enc then `I tptp_individual_type else `make_fixed_type_const s, @@ -939,8 +952,8 @@ | term (TVar (x, _)) = ATerm (tvar_name x, []) in term end -fun ho_term_for_type_arg format type_enc T = - if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T) +fun ho_term_for_type_arg type_enc T = + if T = dummyT then NONE else SOME (ho_term_from_typ type_enc T) (* This shouldn't clash with anything else. *) val uncurried_alias_sep = "\000" @@ -954,8 +967,8 @@ ^ ")" | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction" -fun mangled_type format type_enc = - generic_mangled_type_name fst o ho_term_from_typ format type_enc +fun mangled_type type_enc = + generic_mangled_type_name fst o ho_term_from_typ type_enc fun make_native_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse @@ -983,9 +996,9 @@ | to_ho _ = raise Fail "unexpected type abstraction" in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end -fun ho_type_from_typ format type_enc pred_sym ary = +fun ho_type_from_typ type_enc pred_sym ary = ho_type_from_ho_term type_enc pred_sym ary - o ho_term_from_typ format type_enc + o ho_term_from_typ type_enc fun aliased_uncurried ary (s, s') = (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) @@ -1001,8 +1014,8 @@ fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f) ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end -fun mangled_const_name format type_enc = - map_filter (ho_term_for_type_arg format type_enc) +fun mangled_const_name type_enc = + map_filter (ho_term_for_type_arg type_enc) #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = @@ -1076,20 +1089,20 @@ | intro _ _ tm = tm in intro true [] end -fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args = +fun mangle_type_args_in_const type_enc (name as (s, _)) T_args = case unprefix_and_unascii const_prefix s of NONE => (name, T_args) | SOME s'' => case type_arg_policy [] type_enc (invert_const s'') of - Mangled_Type_Args => (mangled_const_name format type_enc T_args name, []) + Mangled_Type_Args => (mangled_const_name type_enc T_args name, []) | _ => (name, T_args) -fun mangle_type_args_in_iterm format type_enc = +fun mangle_type_args_in_iterm type_enc = if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then let fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2) | mangle (tm as IConst (_, _, [])) = tm | mangle (IConst (name, T, T_args)) = - mangle_type_args_in_const format type_enc name T_args + mangle_type_args_in_const type_enc name T_args |> (fn (name, T_args) => IConst (name, T, T_args)) | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm) | mangle tm = tm @@ -1143,13 +1156,13 @@ | filt _ tm = tm in filt 0 end -fun iformula_from_prop ctxt format type_enc eq_as_iff = +fun iformula_from_prop ctxt type_enc eq_as_iff = let val thy = Proof_Context.theory_of ctxt fun do_term bs t atomic_Ts = - iterm_from_term thy format bs (Envir.eta_contract t) + iterm_from_term thy type_enc bs (Envir.eta_contract t) |>> (introduce_proxies_in_iterm type_enc - #> mangle_type_args_in_iterm format type_enc #> AAtom) + #> mangle_type_args_in_iterm type_enc #> AAtom) ||> union (op =) atomic_Ts fun do_quant bs q pos s T t' = let @@ -1233,11 +1246,11 @@ end handle TERM _ => @{const True} -fun make_formula ctxt format type_enc eq_as_iff name stature kind t = +fun make_formula ctxt type_enc eq_as_iff name stature kind t = let val (iformula, atomic_Ts) = - iformula_from_prop ctxt format type_enc eq_as_iff - (SOME (kind <> Conjecture)) t [] + iformula_from_prop ctxt type_enc eq_as_iff (SOME (kind <> Conjecture)) t + [] |>> close_iformula_universally in {name = name, stature = stature, kind = kind, iformula = iformula, @@ -1245,8 +1258,8 @@ end fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) = - case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF) - name stature Axiom of + case t |> make_formula ctxt type_enc (eq_as_iff andalso format <> CNF) name + stature Axiom of formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula | formula => SOME formula @@ -1261,8 +1274,7 @@ fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (kind, t)) => t |> kind = Conjecture ? s_not - |> make_formula ctxt format type_enc (format <> CNF) name stature - kind) + |> make_formula ctxt type_enc (format <> CNF) name stature kind) (** Finite and infinite type inference **) @@ -1543,19 +1555,18 @@ fun list_app head args = fold (curry (IApp o swap)) args head fun predicator tm = IApp (predicator_combconst, tm) -fun mk_app_op format type_enc head arg = +fun mk_app_op type_enc head arg = let val head_T = ityp_of head val (arg_T, res_T) = dest_funT head_T val app = IConst (app_op, head_T --> head_T, [arg_T, res_T]) - |> mangle_type_args_in_iterm format type_enc + |> mangle_type_args_in_iterm type_enc in list_app app [head, arg] end -fun firstorderize_fact thy monom_constrs format type_enc sym_tab - uncurried_aliases = +fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases = let - fun do_app arg head = mk_app_op format type_enc head arg + fun do_app arg head = mk_app_op type_enc head arg fun list_app_ops head args = fold do_app args head fun introduce_app_ops tm = let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in @@ -1766,7 +1777,7 @@ else error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".") -fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts +fun translate_formulas ctxt prem_kind format type_enc lam_trans presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt @@ -1817,9 +1828,9 @@ val type_guard = `(make_fixed_const NONE) type_guard_name -fun type_guard_iterm format type_enc T tm = +fun type_guard_iterm type_enc T tm = IApp (IConst (type_guard, T --> @{typ bool}, [T]) - |> mangle_type_args_in_iterm format type_enc, tm) + |> mangle_type_args_in_iterm type_enc, tm) fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = @@ -1868,23 +1879,22 @@ should_encode_type ctxt mono level T | should_generate_tag_bound_decl _ _ _ _ _ = false -fun mk_aterm format type_enc name T_args args = - ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) +fun mk_aterm type_enc name T_args args = + ATerm (name, map_filter (ho_term_for_type_arg type_enc) T_args @ args) -fun do_bound_type ctxt format mono type_enc = +fun do_bound_type ctxt mono type_enc = case type_enc of Native (_, _, level) => - fused_type ctxt mono level 0 - #> ho_type_from_typ format type_enc false 0 #> SOME + fused_type ctxt mono level 0 #> ho_type_from_typ type_enc false 0 #> SOME | _ => K NONE -fun tag_with_type ctxt format mono type_enc pos T tm = +fun tag_with_type ctxt mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) - |> mangle_type_args_in_iterm format type_enc - |> ho_term_from_iterm ctxt format mono type_enc pos + |> mangle_type_args_in_iterm type_enc + |> ho_term_from_iterm ctxt mono type_enc pos |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") -and ho_term_from_iterm ctxt format mono type_enc pos = +and ho_term_from_iterm ctxt mono type_enc pos = let fun beta_red bs (IApp (IAbs ((name, _), tm), tm')) = beta_red ((name, beta_red bs tm') :: bs) tm @@ -1909,14 +1919,12 @@ IConst (name as (s, _), _, T_args) => let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere - in - map (term arg_site) args |> mk_aterm format type_enc name T_args - end + in map (term arg_site) args |> mk_aterm type_enc name T_args end | IVar (name, _) => - map (term Elsewhere) args |> mk_aterm format type_enc name [] + 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 format type_enc true 0 T), + AAbs ((name, ho_type_from_typ type_enc true 0 T), term Elsewhere tm) else raise Fail "unexpected lambda-abstraction" @@ -1924,28 +1932,27 @@ val T = ityp_of u in if should_tag_with_type ctxt mono type_enc site u T then - tag_with_type ctxt format mono type_enc pos T t + tag_with_type ctxt mono type_enc pos T t else t end in term (Top_Level pos) o beta_red [] end -and formula_from_iformula ctxt polym_constrs format mono type_enc - should_guard_var = +and formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc - val do_term = ho_term_from_iterm ctxt format mono type_enc + val do_term = ho_term_from_iterm ctxt mono type_enc fun do_out_of_bound_type pos phi universal (name, T) = if should_guard_type ctxt mono type_enc (fn () => should_guard_var thy polym_constrs level pos phi universal name) T then IVar (name, T) - |> type_guard_iterm format type_enc T + |> type_guard_iterm type_enc T |> do_term pos |> AAtom |> SOME else if should_generate_tag_bound_decl ctxt mono type_enc universal T then let val var = ATerm (name, []) - val tagged_var = tag_with_type ctxt format mono type_enc pos T var + val tagged_var = tag_with_type ctxt mono type_enc pos T var in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end else NONE @@ -1953,7 +1960,7 @@ let val phi = phi |> do_formula pos val universal = Option.map (q = AExists ? not) pos - val do_bound_type = do_bound_type ctxt format mono type_enc + val do_bound_type = do_bound_type ctxt mono type_enc in AQuant (q, xs |> map (apsnd (fn NONE => NONE | SOME T => do_bound_type T)), @@ -1972,11 +1979,11 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) -fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos +fun formula_line_for_fact ctxt polym_constrs prefix encode freshen pos mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, iformula - |> formula_from_iformula ctxt polym_constrs format mono type_enc + |> formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var_in_formula (if pos then SOME true else NONE) |> close_formula_universally |> bound_tvars type_enc true atomic_types, @@ -2017,11 +2024,11 @@ (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), NONE, isabelle_info inductiveN helper_rank) -fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc +fun formula_line_for_conjecture ctxt polym_constrs mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, iformula - |> formula_from_iformula ctxt polym_constrs format mono type_enc + |> formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var_in_formula (SOME false) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) @@ -2062,8 +2069,7 @@ Native (order, Polymorphic, _) => map (decl_line_for_class order) classes | _ => [] -fun sym_decl_table_for_facts thy format type_enc sym_tab - (conjs, facts, extra_tms) = +fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) = let fun add_iterm_syms tm = let val (head, args) = strip_iterm_comb tm in @@ -2107,7 +2113,7 @@ val (s, s') = `(make_fixed_const NONE) @{const_name undefined} |> (case type_arg_policy [] type_enc @{const_name undefined} of - Mangled_Type_Args => mangled_const_name format type_enc [T] + Mangled_Type_Args => mangled_const_name type_enc [T] | _ => I) in Symtab.map_default (s, []) @@ -2222,37 +2228,36 @@ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end -fun formula_line_for_guards_mono_type ctxt format mono type_enc T = +fun formula_line_for_guards_mono_type ctxt mono type_enc T = Formula (guards_sym_formula_prefix ^ - ascii_of (mangled_type format type_enc T), + ascii_of (mangled_type type_enc T), Axiom, IConst (`make_bound_var "X", T, []) - |> type_guard_iterm format type_enc T + |> type_guard_iterm type_enc T |> AAtom - |> formula_from_iformula ctxt [] format mono type_enc + |> formula_from_iformula ctxt [] mono type_enc always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), NONE, isabelle_info inductiveN helper_rank) -fun formula_line_for_tags_mono_type ctxt format mono type_enc T = +fun formula_line_for_tags_mono_type ctxt mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in Formula (tags_sym_formula_prefix ^ - ascii_of (mangled_type format type_enc T), + ascii_of (mangled_type type_enc T), Axiom, eq_formula type_enc (atomic_types_of T) [] false - (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, + (tag_with_type ctxt mono type_enc NONE T x_var) x_var, NONE, isabelle_info defN helper_rank) end -fun problem_lines_for_mono_types ctxt format mono type_enc Ts = +fun problem_lines_for_mono_types ctxt mono type_enc Ts = case type_enc of Native _ => [] - | Guards _ => - map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts - | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts + | Guards _ => map (formula_line_for_guards_mono_type ctxt mono type_enc) Ts + | Tags _ => map (formula_line_for_tags_mono_type ctxt mono type_enc) Ts -fun decl_line_for_sym ctxt format mono type_enc s +fun decl_line_for_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) = let val thy = Proof_Context.theory_of ctxt @@ -2269,7 +2274,7 @@ in Decl (sym_decl_prefix ^ s, (s, s'), T |> fused_type ctxt mono (level_of_type_enc type_enc) ary - |> ho_type_from_typ format type_enc pred_sym 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)) end @@ -2278,8 +2283,8 @@ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) else (Axiom, I) -fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s - j (s', T_args, T, _, ary, in_conj) = +fun formula_line_for_guards_sym_decl ctxt conj_sym_kind mono type_enc n s j + (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind @@ -2306,9 +2311,9 @@ (if n > 1 then "_" ^ string_of_int j else ""), kind, IConst ((s, s'), T, T_args) |> fold (curry (IApp o swap)) bounds - |> type_guard_iterm format type_enc res_T + |> type_guard_iterm type_enc res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_iformula ctxt [] format mono type_enc + |> formula_from_iformula ctxt [] mono type_enc always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) @@ -2316,7 +2321,7 @@ NONE, isabelle_info inductiveN helper_rank) end -fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s +fun formula_lines_for_tags_sym_decl ctxt conj_sym_kind mono type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt @@ -2329,10 +2334,10 @@ val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names |> map (fn name => ATerm (name, [])) - val cst = mk_aterm format type_enc (s, s') T_args + val cst = mk_aterm type_enc (s, s') T_args val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym val should_encode = should_encode_type ctxt mono level - val tag_with = tag_with_type ctxt format mono type_enc NONE + val tag_with = tag_with_type ctxt mono type_enc NONE val add_formula_for_res = if should_encode res_T then let @@ -2367,10 +2372,9 @@ end | rationalize_decls _ decls = decls -fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc - (s, decls) = +fun problem_lines_for_sym_decls ctxt conj_sym_kind mono type_enc (s, decls) = case type_enc of - Native _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)] + Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)] | Guards (_, level) => let val thy = Proof_Context.theory_of ctxt @@ -2381,7 +2385,7 @@ o result_type_of_decl) in (0 upto length decls - 1, decls) - |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono + |-> map2 (formula_line_for_guards_sym_decl ctxt conj_sym_kind mono type_enc n s) end | Tags (_, level) => @@ -2390,42 +2394,40 @@ else let val n = length decls in (0 upto n - 1 ~~ decls) - |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono + |> maps (formula_lines_for_tags_sym_decl ctxt conj_sym_kind mono type_enc n s) end -fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc - mono_Ts sym_decl_tab = +fun problem_lines_for_sym_decl_table ctxt conj_sym_kind 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 format mono type_enc mono_Ts + val mono_lines = problem_lines_for_mono_types ctxt mono type_enc mono_Ts val decl_lines = - fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind - mono type_enc) + fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind mono + type_enc) syms [] in mono_lines @ decl_lines end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind - mono type_enc sym_tab0 sym_tab base_s0 types in_conj = +fun do_uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono + type_enc sym_tab0 sym_tab base_s0 types in_conj = let fun do_alias ary = let val thy = Proof_Context.theory_of ctxt val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind - val base_name = base_s0 |> `(make_fixed_const (SOME format)) + val base_name = base_s0 |> `(make_fixed_const (SOME type_enc)) val T = case types of [T] => T | _ => robust_const_type thy base_s0 val T_args = robust_const_typargs thy (base_s0, T) val (base_name as (base_s, _), T_args) = - mangle_type_args_in_const format type_enc base_name T_args + mangle_type_args_in_const type_enc base_name T_args val base_ary = min_ary_of sym_tab0 base_s fun do_const name = IConst (name, T, T_args) val filter_ty_args = filter_type_args_in_iterm thy monom_constrs type_enc - val ho_term_of = - ho_term_from_iterm ctxt format mono type_enc (SOME true) + val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true) val name1 as (s1, _) = base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) val name2 as (s2, _) = base_name |> aliased_uncurried ary @@ -2436,13 +2438,12 @@ val (first_bounds, last_bound) = bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last val tm1 = - mk_app_op format type_enc (list_app (do_const name1) first_bounds) - last_bound + mk_app_op type_enc (list_app (do_const name1) first_bounds) last_bound |> filter_ty_args val tm2 = list_app (do_const name2) (first_bounds @ [last_bound]) |> filter_ty_args - val do_bound_type = do_bound_type ctxt format mono type_enc + val do_bound_type = do_bound_type ctxt mono type_enc val eq = eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) bounds) false @@ -2455,29 +2456,28 @@ else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono - type_enc sym_tab0 sym_tab - (s, {min_ary, types, in_conj, ...} : sym_info) = +fun uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono type_enc + sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const in - do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind - mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary + do_uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono + type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], []) -fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind - mono type_enc uncurried_aliases sym_tab0 sym_tab = +fun uncurried_alias_lines_for_sym_table ctxt monom_constrs conj_sym_kind mono + type_enc uncurried_aliases sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append - o uncurried_alias_lines_for_sym ctxt monom_constrs format - conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab + o uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind + mono type_enc sym_tab0 sym_tab) sym_tab val implicit_declsN = "Should-be-implicit typings" val explicit_declsN = "Explicit typings" @@ -2596,15 +2596,15 @@ lam_trans val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, lifted) = - translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts + translate_formulas ctxt prem_kind format type_enc lam_trans preproc hyp_ts concl_t facts val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc val (polym_constrs, monom_constrs) = all_constrs_of_polymorphic_datatypes thy - |>> map (make_fixed_const (SOME format)) + |>> map (make_fixed_const (SOME type_enc)) fun firstorderize in_helper = - firstorderize_fact thy monom_constrs format type_enc sym_tab0 + firstorderize_fact thy monom_constrs type_enc sym_tab0 (uncurried_aliases andalso not in_helper) val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) val sym_tab = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts @@ -2615,23 +2615,23 @@ helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc val class_decl_lines = decl_lines_for_classes type_enc classes val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_for_sym_table ctxt monom_constrs format - conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab + uncurried_alias_lines_for_sym_table ctxt monom_constrs conj_sym_kind mono + type_enc uncurried_aliases sym_tab0 sym_tab val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) - |> sym_decl_table_for_facts thy format type_enc sym_tab - |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono - type_enc mono_Ts + |> sym_decl_table_for_facts thy type_enc sym_tab + |> problem_lines_for_sym_decl_table ctxt conj_sym_kind mono type_enc + mono_Ts val num_facts = length facts val fact_lines = - map (formula_line_for_fact ctxt polym_constrs format fact_prefix + map (formula_line_for_fact ctxt polym_constrs fact_prefix ascii_of (not exporter) (not exporter) mono type_enc (rank_of_fact_num num_facts)) (0 upto num_facts - 1 ~~ facts) val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I - false true mono type_enc (K default_rank)) + |> map (formula_line_for_fact ctxt polym_constrs helper_prefix I false + true mono type_enc (K default_rank)) (* Reordering these might confuse the proof reconstruction code or the SPASS FLOTTER hack. *) val problem = @@ -2644,8 +2644,8 @@ (helpersN, helper_lines), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)), (conjsN, - map (formula_line_for_conjecture ctxt polym_constrs format mono - type_enc) conjs)] + map (formula_line_for_conjecture ctxt polym_constrs mono type_enc) + conjs)] val problem = problem |> (case format of