1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Feb 01 17:16:55 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 02 01:20:28 2012 +0100
1.3 @@ -96,7 +96,7 @@
1.4 val mk_aconns :
1.5 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.6 val unmangled_const : string -> string * (string, 'b) ho_term list
1.7 - val unmangled_const_name : string -> string
1.8 + val unmangled_const_name : string -> string list
1.9 val helper_table : ((string * bool) * thm list) list
1.10 val trans_lams_from_string :
1.11 Proof.context -> type_enc -> string -> term list -> term list * term list
1.12 @@ -149,13 +149,14 @@
1.13 val class_prefix = "cl_"
1.14
1.15 (* Freshness almost guaranteed! *)
1.16 +val atp_prefix = "ATP" ^ Long_Name.separator
1.17 val atp_weak_prefix = "ATP:"
1.18
1.19 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
1.20 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
1.21 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
1.22
1.23 -val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
1.24 +val skolem_const_prefix = atp_prefix ^ "Sko"
1.25 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
1.26 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
1.27
1.28 @@ -165,6 +166,7 @@
1.29 val sym_decl_prefix = "sy_"
1.30 val guards_sym_formula_prefix = "gsy_"
1.31 val tags_sym_formula_prefix = "tsy_"
1.32 +val app_op_alias_eq_prefix = "aa_"
1.33 val fact_prefix = "fact_"
1.34 val conjecture_prefix = "conj_"
1.35 val helper_prefix = "help_"
1.36 @@ -873,7 +875,10 @@
1.37 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
1.38
1.39 (* This shouldn't clash with anything else. *)
1.40 -val mangled_type_sep = "\000"
1.41 +val app_op_alias_sep = "\000"
1.42 +val mangled_type_sep = "\001"
1.43 +
1.44 +val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep
1.45
1.46 fun generic_mangled_type_name f (ATerm (name, [])) = f name
1.47 | generic_mangled_type_name f (ATerm (name, tys)) =
1.48 @@ -914,13 +919,23 @@
1.49 ho_type_from_ho_term type_enc pred_sym ary
1.50 o ho_term_from_typ format type_enc
1.51
1.52 -fun mangled_const_name format type_enc T_args (s, s') =
1.53 +fun aliased_app_op ary (s, s') =
1.54 + (s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
1.55 +fun unaliased_app_op (s, s') =
1.56 + case space_explode app_op_alias_sep s of
1.57 + [_] => (s, s')
1.58 + | [s1, s2] => (s1, unsuffix s2 s')
1.59 + | _ => raise Fail "ill-formed explicit application alias"
1.60 +
1.61 +fun raw_mangled_const_name type_name ty_args (s, s') =
1.62 let
1.63 - val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
1.64 fun type_suffix f g =
1.65 - fold_rev (curry (op ^) o g o prefix mangled_type_sep
1.66 - o generic_mangled_type_name f) ty_args ""
1.67 + fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
1.68 + ty_args ""
1.69 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
1.70 +fun mangled_const_name format type_enc =
1.71 + map_filter (ho_term_for_type_arg format type_enc)
1.72 + #> raw_mangled_const_name generic_mangled_type_name
1.73
1.74 val parse_mangled_ident =
1.75 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
1.76 @@ -939,9 +954,10 @@
1.77 quote s)) parse_mangled_type))
1.78 |> fst
1.79
1.80 -val unmangled_const_name = space_explode mangled_type_sep #> hd
1.81 +fun unmangled_const_name s =
1.82 + (s, s) |> unaliased_app_op |> fst |> space_explode mangled_type_sep
1.83 fun unmangled_const s =
1.84 - let val ss = space_explode mangled_type_sep s in
1.85 + let val ss = unmangled_const_name s in
1.86 (hd ss, map unmangled_type (tl ss))
1.87 end
1.88
1.89 @@ -992,19 +1008,21 @@
1.90 | intro _ _ tm = tm
1.91 in intro true [] end
1.92
1.93 +fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
1.94 + case unprefix_and_unascii const_prefix s of
1.95 + NONE => (name, T_args)
1.96 + | SOME s'' =>
1.97 + case type_arg_policy [] type_enc (invert_const s'') of
1.98 + Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
1.99 + | _ => (name, T_args)
1.100 fun mangle_type_args_in_iterm format type_enc =
1.101 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.102 let
1.103 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
1.104 | mangle (tm as IConst (_, _, [])) = tm
1.105 - | mangle (tm as IConst (name as (s, _), T, T_args)) =
1.106 - (case unprefix_and_unascii const_prefix s of
1.107 - NONE => tm
1.108 - | SOME s'' =>
1.109 - case type_arg_policy [] type_enc (invert_const s'') of
1.110 - Mangled_Type_Args =>
1.111 - IConst (mangled_const_name format type_enc T_args name, T, [])
1.112 - | _ => tm)
1.113 + | mangle (IConst (name, T, T_args)) =
1.114 + mangle_type_args_in_const format type_enc name T_args
1.115 + |> (fn (name, T_args) => IConst (name, T, T_args))
1.116 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1.117 | mangle tm = tm
1.118 in mangle end
1.119 @@ -1029,31 +1047,30 @@
1.120 end
1.121 handle TYPE _ => T_args
1.122
1.123 +fun filter_type_args_in_const _ _ _ _ _ [] = []
1.124 + | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
1.125 + case unprefix_and_unascii const_prefix s of
1.126 + NONE =>
1.127 + if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
1.128 + else T_args
1.129 + | SOME s'' =>
1.130 + let
1.131 + val s'' = invert_const s''
1.132 + fun filter_T_args false = T_args
1.133 + | filter_T_args true = filter_const_type_args thy s'' ary T_args
1.134 + in
1.135 + case type_arg_policy monom_constrs type_enc s'' of
1.136 + Explicit_Type_Args infer_from_term_args =>
1.137 + filter_T_args infer_from_term_args
1.138 + | No_Type_Args => []
1.139 + | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1.140 + end
1.141 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1.142 let
1.143 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1.144 - | filt _ (tm as IConst (_, _, [])) = tm
1.145 | filt ary (IConst (name as (s, _), T, T_args)) =
1.146 - (case unprefix_and_unascii const_prefix s of
1.147 - NONE =>
1.148 - (name,
1.149 - if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
1.150 - []
1.151 - else
1.152 - T_args)
1.153 - | SOME s'' =>
1.154 - let
1.155 - val s'' = invert_const s''
1.156 - fun filter_T_args false = T_args
1.157 - | filter_T_args true = filter_const_type_args thy s'' ary T_args
1.158 - in
1.159 - case type_arg_policy monom_constrs type_enc s'' of
1.160 - Explicit_Type_Args infer_from_term_args =>
1.161 - (name, filter_T_args infer_from_term_args)
1.162 - | No_Type_Args => (name, [])
1.163 - | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1.164 - end)
1.165 - |> (fn (name, T_args) => IConst (name, T, T_args))
1.166 + filter_type_args_in_const thy monom_constrs type_enc ary s T_args
1.167 + |> (fn T_args => IConst (name, T, T_args))
1.168 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1.169 | filt _ tm = tm
1.170 in filt 0 end
1.171 @@ -1064,8 +1081,7 @@
1.172 fun do_term bs t atomic_Ts =
1.173 iterm_from_term thy format bs (Envir.eta_contract t)
1.174 |>> (introduce_proxies_in_iterm type_enc
1.175 - #> mangle_type_args_in_iterm format type_enc
1.176 - #> AAtom)
1.177 + #> mangle_type_args_in_iterm format type_enc #> AAtom)
1.178 ||> union (op =) atomic_Ts
1.179 fun do_quant bs q pos s T t' =
1.180 let
1.181 @@ -1377,9 +1393,9 @@
1.182 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1.183 in_conj = false})
1.184
1.185 -datatype explicit_apply = Incomplete_Apply | Sufficient_Apply | Full_Apply
1.186 +datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
1.187
1.188 -fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
1.189 +fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
1.190 let
1.191 fun consider_var_ary const_T var_T max_ary =
1.192 let
1.193 @@ -1391,7 +1407,7 @@
1.194 iter (ary + 1) (range_type T)
1.195 in iter 0 const_T end
1.196 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1.197 - if explicit_apply = Sufficient_Apply andalso
1.198 + if app_op_level = Sufficient_Apply andalso
1.199 (can dest_funT T orelse T = @{typ bool}) then
1.200 let
1.201 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1.202 @@ -1410,64 +1426,63 @@
1.203 end
1.204 else
1.205 accum
1.206 + fun add_iterm_syms conj_fact top_level tm
1.207 + (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1.208 + let val (head, args) = strip_iterm_comb tm in
1.209 + (case head of
1.210 + IConst ((s, _), T, _) =>
1.211 + if String.isPrefix bound_var_prefix s orelse
1.212 + String.isPrefix all_bound_var_prefix s then
1.213 + add_universal_var T accum
1.214 + else if String.isPrefix exist_bound_var_prefix s then
1.215 + accum
1.216 + else
1.217 + let val ary = length args in
1.218 + ((bool_vars, fun_var_Ts),
1.219 + case Symtab.lookup sym_tab s of
1.220 + SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1.221 + let
1.222 + val pred_sym =
1.223 + pred_sym andalso top_level andalso not bool_vars
1.224 + val types' = types |> insert_type ctxt I T
1.225 + val in_conj = in_conj orelse conj_fact
1.226 + val min_ary =
1.227 + if app_op_level = Sufficient_Apply andalso
1.228 + not (pointer_eq (types', types)) then
1.229 + fold (consider_var_ary T) fun_var_Ts min_ary
1.230 + else
1.231 + min_ary
1.232 + in
1.233 + Symtab.update (s, {pred_sym = pred_sym,
1.234 + min_ary = Int.min (ary, min_ary),
1.235 + max_ary = Int.max (ary, max_ary),
1.236 + types = types', in_conj = in_conj})
1.237 + sym_tab
1.238 + end
1.239 + | NONE =>
1.240 + let
1.241 + val pred_sym = top_level andalso not bool_vars
1.242 + val min_ary =
1.243 + case app_op_level of
1.244 + Incomplete_Apply => ary
1.245 + | Sufficient_Apply =>
1.246 + fold (consider_var_ary T) fun_var_Ts ary
1.247 + | Full_Apply => 0
1.248 + in
1.249 + Symtab.update_new (s,
1.250 + {pred_sym = pred_sym, min_ary = min_ary,
1.251 + max_ary = ary, types = [T], in_conj = conj_fact})
1.252 + sym_tab
1.253 + end)
1.254 + end
1.255 + | IVar (_, T) => add_universal_var T accum
1.256 + | IAbs ((_, T), tm) =>
1.257 + accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
1.258 + | _ => accum)
1.259 + |> fold (add_iterm_syms conj_fact false) args
1.260 + end
1.261 fun add_fact_syms conj_fact =
1.262 - let
1.263 - fun add_iterm_syms top_level tm
1.264 - (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1.265 - let val (head, args) = strip_iterm_comb tm in
1.266 - (case head of
1.267 - IConst ((s, _), T, _) =>
1.268 - if String.isPrefix bound_var_prefix s orelse
1.269 - String.isPrefix all_bound_var_prefix s then
1.270 - add_universal_var T accum
1.271 - else if String.isPrefix exist_bound_var_prefix s then
1.272 - accum
1.273 - else
1.274 - let val ary = length args in
1.275 - ((bool_vars, fun_var_Ts),
1.276 - case Symtab.lookup sym_tab s of
1.277 - SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1.278 - let
1.279 - val pred_sym =
1.280 - pred_sym andalso top_level andalso not bool_vars
1.281 - val types' = types |> insert_type ctxt I T
1.282 - val in_conj = in_conj orelse conj_fact
1.283 - val min_ary =
1.284 - if explicit_apply = Sufficient_Apply andalso
1.285 - not (pointer_eq (types', types)) then
1.286 - fold (consider_var_ary T) fun_var_Ts min_ary
1.287 - else
1.288 - min_ary
1.289 - in
1.290 - Symtab.update (s, {pred_sym = pred_sym,
1.291 - min_ary = Int.min (ary, min_ary),
1.292 - max_ary = Int.max (ary, max_ary),
1.293 - types = types', in_conj = in_conj})
1.294 - sym_tab
1.295 - end
1.296 - | NONE =>
1.297 - let
1.298 - val pred_sym = top_level andalso not bool_vars
1.299 - val min_ary =
1.300 - case explicit_apply of
1.301 - Incomplete_Apply => ary
1.302 - | Sufficient_Apply =>
1.303 - fold (consider_var_ary T) fun_var_Ts ary
1.304 - | Full_Apply => 0
1.305 - in
1.306 - Symtab.update_new (s,
1.307 - {pred_sym = pred_sym, min_ary = min_ary,
1.308 - max_ary = ary, types = [T], in_conj = conj_fact})
1.309 - sym_tab
1.310 - end)
1.311 - end
1.312 - | IVar (_, T) => add_universal_var T accum
1.313 - | IAbs ((_, T), tm) =>
1.314 - accum |> add_universal_var T |> add_iterm_syms false tm
1.315 - | _ => accum)
1.316 - |> fold (add_iterm_syms false) args
1.317 - end
1.318 - in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end
1.319 + K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
1.320 in
1.321 ((false, []), Symtab.empty)
1.322 |> fold (add_fact_syms true) conjs
1.323 @@ -1482,7 +1497,7 @@
1.324 | NONE =>
1.325 case unprefix_and_unascii const_prefix s of
1.326 SOME s =>
1.327 - let val s = s |> unmangled_const_name |> invert_const in
1.328 + let val s = s |> unmangled_const_name |> hd |> invert_const in
1.329 if s = predicator_name then 1
1.330 else if s = app_op_name then 2
1.331 else if s = type_guard_name then 1
1.332 @@ -1507,25 +1522,34 @@
1.333 fun list_app head args = fold (curry (IApp o swap)) args head
1.334 fun predicator tm = IApp (predicator_combconst, tm)
1.335
1.336 -fun firstorderize_fact thy monom_constrs format type_enc sym_tab =
1.337 +fun do_app_op format type_enc head arg =
1.338 let
1.339 - fun do_app arg head =
1.340 - let
1.341 - val head_T = ityp_of head
1.342 - val (arg_T, res_T) = dest_funT head_T
1.343 - val app =
1.344 - IConst (app_op, head_T --> head_T, [arg_T, res_T])
1.345 - |> mangle_type_args_in_iterm format type_enc
1.346 - in list_app app [head, arg] end
1.347 + val head_T = ityp_of head
1.348 + val (arg_T, res_T) = dest_funT head_T
1.349 + val app =
1.350 + IConst (app_op, head_T --> head_T, [arg_T, res_T])
1.351 + |> mangle_type_args_in_iterm format type_enc
1.352 + in list_app app [head, arg] end
1.353 +
1.354 +fun firstorderize_fact thy monom_constrs format type_enc app_op_aliases
1.355 + sym_tab =
1.356 + let
1.357 + fun do_app arg head = do_app_op format type_enc head arg
1.358 fun list_app_ops head args = fold do_app args head
1.359 fun introduce_app_ops tm =
1.360 - case strip_iterm_comb tm of
1.361 - (head as IConst ((s, _), _, _), args) =>
1.362 - args |> map introduce_app_ops
1.363 - |> chop (min_ary_of sym_tab s)
1.364 - |>> list_app head
1.365 - |-> list_app_ops
1.366 - | (head, args) => list_app_ops head (map introduce_app_ops args)
1.367 + let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
1.368 + case head of
1.369 + IConst (name as (s, _), T, T_args) =>
1.370 + if app_op_aliases then
1.371 + let
1.372 + val ary = length args
1.373 + val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary
1.374 + in list_app (IConst (name, T, T_args)) args end
1.375 + else
1.376 + args |> chop (min_ary_of sym_tab s)
1.377 + |>> list_app head |-> list_app_ops
1.378 + | _ => list_app_ops head args
1.379 + end
1.380 fun introduce_predicators tm =
1.381 case strip_iterm_comb tm of
1.382 (IConst ((s, _), _, _), _) =>
1.383 @@ -1590,9 +1614,10 @@
1.384 atype_of_type_vars type_enc)
1.385 | _ => NONE) Ts)
1.386
1.387 -fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
1.388 +fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1.389 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1.390 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1.391 + |> mk_aquant AForall bounds
1.392 |> close_formula_universally
1.393 |> bound_tvars type_enc true atomic_Ts
1.394
1.395 @@ -1605,7 +1630,7 @@
1.396 val tagged_var = tag (var "X")
1.397 in
1.398 Formula (type_tag_idempotence_helper_name, Axiom,
1.399 - eq_formula type_enc [] false (tag tagged_var) tagged_var,
1.400 + eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
1.401 NONE, isabelle_info format eqN)
1.402 end
1.403
1.404 @@ -1619,7 +1644,7 @@
1.405 SOME mangled_s =>
1.406 let
1.407 val thy = Proof_Context.theory_of ctxt
1.408 - val unmangled_s = mangled_s |> unmangled_const_name
1.409 + val unmangled_s = mangled_s |> unmangled_const_name |> hd
1.410 fun dub needs_fairly_sound j k =
1.411 unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1.412 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1.413 @@ -1829,6 +1854,13 @@
1.414 fun mk_aterm format type_enc name T_args args =
1.415 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1.416
1.417 +fun do_bound_type ctxt format mono type_enc =
1.418 + case type_enc of
1.419 + Simple_Types (_, _, level) =>
1.420 + fused_type ctxt mono level 0
1.421 + #> ho_type_from_typ format type_enc false 0 #> SOME
1.422 + | _ => K NONE
1.423 +
1.424 fun tag_with_type ctxt format mono type_enc pos T tm =
1.425 IConst (type_tag, T --> T, [T])
1.426 |> mangle_type_args_in_iterm format type_enc
1.427 @@ -1873,11 +1905,6 @@
1.428 val thy = Proof_Context.theory_of ctxt
1.429 val level = level_of_type_enc type_enc
1.430 val do_term = ho_term_from_iterm ctxt format mono type_enc
1.431 - val do_bound_type =
1.432 - case type_enc of
1.433 - Simple_Types _ => fused_type ctxt mono level 0
1.434 - #> ho_type_from_typ format type_enc false 0 #> SOME
1.435 - | _ => K NONE
1.436 fun do_out_of_bound_type pos phi universal (name, T) =
1.437 if should_guard_type ctxt mono type_enc
1.438 (fn () => should_guard_var thy polym_constrs level pos phi
1.439 @@ -1896,6 +1923,7 @@
1.440 let
1.441 val phi = phi |> do_formula pos
1.442 val universal = Option.map (q = AExists ? not) pos
1.443 + val do_bound_type = do_bound_type ctxt format mono type_enc
1.444 in
1.445 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1.446 | SOME T => do_bound_type T)),
1.447 @@ -1995,7 +2023,8 @@
1.448 map (decl_line_for_class order) classes
1.449 | _ => []
1.450
1.451 -fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
1.452 +fun sym_decl_table_for_facts ctxt format type_enc sym_tab
1.453 + (conjs, facts, extra_tms) =
1.454 let
1.455 fun add_iterm_syms tm =
1.456 let val (head, args) = strip_iterm_comb tm in
1.457 @@ -2055,6 +2084,7 @@
1.458 Symtab.empty
1.459 |> is_type_enc_fairly_sound type_enc
1.460 ? (fold (fold add_fact_syms) [conjs, facts]
1.461 + #> fold add_iterm_syms extra_tms
1.462 #> (case type_enc of
1.463 Simple_Types (First_Order, Polymorphic, _) =>
1.464 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
1.465 @@ -2168,7 +2198,7 @@
1.466 Formula (tags_sym_formula_prefix ^
1.467 ascii_of (mangled_type format type_enc T),
1.468 Axiom,
1.469 - eq_formula type_enc (atomic_types_of T) false
1.470 + eq_formula type_enc (atomic_types_of T) [] false
1.471 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
1.472 NONE, isabelle_info format eqN)
1.473 end
1.474 @@ -2202,13 +2232,15 @@
1.475 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
1.476 end
1.477
1.478 +fun honor_conj_sym_kind in_conj conj_sym_kind =
1.479 + if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1.480 + else (Axiom, I)
1.481 +
1.482 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
1.483 j (s', T_args, T, _, ary, in_conj) =
1.484 let
1.485 val thy = Proof_Context.theory_of ctxt
1.486 - val (kind, maybe_negate) =
1.487 - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1.488 - else (Axiom, I)
1.489 + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
1.490 val (arg_Ts, res_T) = chop_fun ary T
1.491 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
1.492 val bounds =
1.493 @@ -2251,14 +2283,12 @@
1.494 val ident_base =
1.495 tags_sym_formula_prefix ^ s ^
1.496 (if n > 1 then "_" ^ string_of_int j else "")
1.497 - val (kind, maybe_negate) =
1.498 - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1.499 - else (Axiom, I)
1.500 + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
1.501 val (arg_Ts, res_T) = chop_fun ary T
1.502 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
1.503 val bounds = bound_names |> map (fn name => ATerm (name, []))
1.504 val cst = mk_aterm format type_enc (s, s') T_args
1.505 - val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
1.506 + val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
1.507 val should_encode = should_encode_type ctxt mono level
1.508 val tag_with = tag_with_type ctxt format mono type_enc NONE
1.509 val add_formula_for_res =
1.510 @@ -2351,6 +2381,74 @@
1.511 syms []
1.512 in mono_lines @ decl_lines end
1.513
1.514 +fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
1.515 +
1.516 +fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
1.517 + type_enc sym_tab base_s0 types in_conj =
1.518 + let
1.519 + fun do_alias ary =
1.520 + let
1.521 + val thy = Proof_Context.theory_of ctxt
1.522 + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
1.523 + val base_name = base_s0 |> `(make_fixed_const (SOME format))
1.524 + val T = case types of [T] => T | _ => robust_const_type thy base_s0
1.525 + val T_args = robust_const_typargs thy (base_s0, T)
1.526 + val (base_name as (base_s, _), T_args) =
1.527 + mangle_type_args_in_const format type_enc base_name T_args
1.528 + val base_ary = min_ary_of sym_tab base_s
1.529 + val T_args =
1.530 + T_args |> filter_type_args_in_const thy monom_constrs type_enc
1.531 + base_ary base_s
1.532 + fun do_const name = IConst (name, T, T_args)
1.533 + val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true)
1.534 + val name1 as (s1, _) =
1.535 + base_name |> ary - 1 > base_ary ? aliased_app_op (ary - 1)
1.536 + val name2 as (s2, _) = base_name |> aliased_app_op ary
1.537 + val (arg_Ts, _) = chop_fun ary T
1.538 + val bound_names =
1.539 + 1 upto ary |> map (`I o make_bound_var o string_of_int)
1.540 + val bounds = bound_names ~~ arg_Ts
1.541 + val (first_bounds, last_bound) =
1.542 + bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
1.543 + val tm1 =
1.544 + do_app_op format type_enc (list_app (do_const name1) first_bounds)
1.545 + last_bound
1.546 + val tm2 = list_app (do_const name2) (first_bounds @ [last_bound])
1.547 + val do_bound_type = do_bound_type ctxt format mono type_enc
1.548 + val eq =
1.549 + eq_formula type_enc (atomic_types_of T)
1.550 + (map (apsnd do_bound_type) bounds) false
1.551 + (do_term tm1) (do_term tm2)
1.552 + in
1.553 + ([tm1, tm2],
1.554 + [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE,
1.555 + isabelle_info format eqN)])
1.556 + |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
1.557 + else pair_append (do_alias (ary - 1)))
1.558 + end
1.559 + in do_alias end
1.560 +fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
1.561 + type_enc sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
1.562 + case unprefix_and_unascii const_prefix s of
1.563 + SOME mangled_s =>
1.564 + if String.isSubstring app_op_alias_sep mangled_s then
1.565 + let
1.566 + val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
1.567 + in
1.568 + do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
1.569 + mono type_enc sym_tab base_s0 types in_conj min_ary
1.570 + end
1.571 + else
1.572 + ([], [])
1.573 + | NONE => ([], [])
1.574 +fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
1.575 + mono type_enc app_op_aliases sym_tab =
1.576 + ([], [])
1.577 + |> app_op_aliases
1.578 + ? Symtab.fold_rev (pair_append
1.579 + o app_op_alias_lines_for_sym ctxt monom_constrs format
1.580 + conj_sym_kind mono type_enc sym_tab) sym_tab
1.581 +
1.582 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
1.583 Config.get ctxt type_tag_idempotence andalso
1.584 is_type_level_monotonicity_based level andalso
1.585 @@ -2359,6 +2457,7 @@
1.586
1.587 val implicit_declsN = "Should-be-implicit typings"
1.588 val explicit_declsN = "Explicit typings"
1.589 +val app_op_alias_eqsN = "Application aliases"
1.590 val factsN = "Relevant facts"
1.591 val class_relsN = "Class relationships"
1.592 val aritiesN = "Arities"
1.593 @@ -2388,17 +2487,18 @@
1.594 fun undeclared_syms_in_problem type_enc problem =
1.595 let
1.596 val declared = declared_syms_in_problem problem
1.597 - fun do_sym name ty =
1.598 - if member (op =) declared name then I else AList.default (op =) (name, ty)
1.599 - fun do_type (AType (name as (s, _), tys)) =
1.600 - is_tptp_user_symbol s
1.601 - ? do_sym name (fn () => nary_type_constr_type (length tys))
1.602 + fun do_sym (name as (s, _)) ty =
1.603 + if is_tptp_user_symbol s andalso not (member (op =) declared name) then
1.604 + AList.default (op =) (name, ty)
1.605 + else
1.606 + I
1.607 + fun do_type (AType (name, tys)) =
1.608 + do_sym name (fn () => nary_type_constr_type (length tys))
1.609 #> fold do_type tys
1.610 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
1.611 | do_type (ATyAbs (_, ty)) = do_type ty
1.612 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
1.613 - is_tptp_user_symbol s
1.614 - ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
1.615 + do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
1.616 #> fold (do_term false) tms
1.617 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
1.618 fun do_formula (AQuant (_, xs, phi)) =
1.619 @@ -2439,7 +2539,7 @@
1.620 |> List.partition is_poly_constr
1.621 |> pairself (map fst)
1.622
1.623 -val explicit_apply_threshold = 50
1.624 +val app_op_threshold = 50
1.625
1.626 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
1.627 lam_trans readable_names preproc hyp_ts concl_t facts =
1.628 @@ -2450,12 +2550,13 @@
1.629 because it takes only one existential variable ranging over "'a => 'b" to
1.630 ruin everything. Hence we do it only if there are few facts (which is
1.631 normally the case for "metis" and the minimizer). *)
1.632 - val explicit_apply =
1.633 + val app_op_level =
1.634 if polymorphism_of_type_enc type_enc = Polymorphic andalso
1.635 - length facts >= explicit_apply_threshold then
1.636 + length facts >= app_op_threshold then
1.637 Incomplete_Apply
1.638 else
1.639 Sufficient_Apply
1.640 + val app_op_aliases = (format = DFG DFG_Sorted)
1.641 val lam_trans =
1.642 if lam_trans = keep_lamsN andalso
1.643 not (is_type_enc_higher_order type_enc) then
1.644 @@ -2467,13 +2568,14 @@
1.645 lifted) =
1.646 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
1.647 concl_t facts
1.648 - val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
1.649 + val sym_tab = sym_table_for_facts ctxt type_enc app_op_level conjs facts
1.650 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
1.651 val (polym_constrs, monom_constrs) =
1.652 all_constrs_of_polymorphic_datatypes thy
1.653 |>> map (make_fixed_const (SOME format))
1.654 val firstorderize =
1.655 - firstorderize_fact thy monom_constrs format type_enc sym_tab
1.656 + firstorderize_fact thy monom_constrs format type_enc app_op_aliases
1.657 + sym_tab
1.658 val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
1.659 val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
1.660 val helpers =
1.661 @@ -2482,8 +2584,11 @@
1.662 val mono_Ts =
1.663 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
1.664 val class_decl_lines = decl_lines_for_classes type_enc classes
1.665 + val (app_op_alias_eq_tms, app_op_alias_eq_lines) =
1.666 + app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
1.667 + mono type_enc app_op_aliases sym_tab
1.668 val sym_decl_lines =
1.669 - (conjs, helpers @ facts)
1.670 + (conjs, helpers @ facts, app_op_alias_eq_tms)
1.671 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
1.672 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
1.673 type_enc mono_Ts
1.674 @@ -2499,6 +2604,7 @@
1.675 FLOTTER hack. *)
1.676 val problem =
1.677 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
1.678 + (app_op_alias_eqsN, app_op_alias_eq_lines),
1.679 (factsN,
1.680 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
1.681 ascii_of (not exporter) (not exporter) mono type_enc)