--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 05 16:07:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 05 16:07:15 2012 +0200
@@ -26,8 +26,8 @@
datatype constr_optim = With_Constr_Optim | Without_Constr_Optim
datatype type_level =
All_Types |
+ Undercover_Types |
Nonmono_Types of strictness * uniformity |
- Undercover_Types |
Const_Types of constr_optim |
No_Types
type type_enc
@@ -137,8 +137,8 @@
datatype constr_optim = With_Constr_Optim | Without_Constr_Optim
datatype type_level =
All_Types |
+ Undercover_Types |
Nonmono_Types of strictness * uniformity |
- Undercover_Types |
Const_Types of constr_optim |
No_Types
@@ -834,10 +834,10 @@
(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
- Mangled_Type_Args |
+ Mangled_Type_Args | (* ### TODO: get rid of this *)
All_Type_Args |
- Not_Input_Type_Args |
- Constr_Input_Type_Args |
+ Noninfer_Type_Args |
+ Constr_Infer_Type_Args |
No_Type_Args
fun type_arg_policy constrs type_enc s =
@@ -847,7 +847,6 @@
else case type_enc of
Native (_, Raw_Polymorphic _, _) => All_Type_Args
| Native (_, Type_Class_Polymorphic, _) => All_Type_Args
- | Tags (_, All_Types) => No_Type_Args
| _ =>
let val level = level_of_type_enc type_enc in
if level = No_Types orelse s = @{const_name HOL.eq} orelse
@@ -855,11 +854,15 @@
No_Type_Args
else if poly = Mangled_Monomorphic then
Mangled_Type_Args
- else if level = All_Types orelse level = Undercover_Types then
- Not_Input_Type_Args
+ else if level = All_Types then
+ case type_enc of
+ Guards _ => Noninfer_Type_Args
+ | Tags _ => No_Type_Args
+ else if level = Undercover_Types then
+ Noninfer_Type_Args
else if member (op =) constrs s andalso
level <> Const_Types Without_Constr_Optim then
- Constr_Input_Type_Args
+ Constr_Infer_Type_Args
else
All_Type_Args
end
@@ -1170,9 +1173,9 @@
case type_arg_policy constrs type_enc s'' of
Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
| All_Type_Args => T_args
- | Not_Input_Type_Args =>
+ | Noninfer_Type_Args =>
filter_type_args (not o fst) thy s'' (chop_fun ary) T_args
- | Constr_Input_Type_Args =>
+ | Constr_Infer_Type_Args =>
filter_type_args fst thy s'' strip_type T_args
| No_Type_Args => []
end
@@ -1337,27 +1340,22 @@
(** Finite and infinite type inference **)
-fun tvar_footprint thy body s ary =
+fun tvar_footprint thy s ary =
(case unprefix_and_unascii const_prefix s of
SOME s =>
- let
- val (binder_Ts, body_T) =
- s |> invert_const |> robust_const_type thy |> chop_fun ary
- fun tvars_of T =
- [] |> Term.add_tvarsT T
- |> (fn Ts => if body then Ts
- else subtract (op =) (Term.add_tvarsT body_T []) Ts)
- |> map fst
- in binder_Ts |> map tvars_of end
+ let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
+ s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
+ |> map tvars_of
+ end
| NONE => [])
handle TYPE _ => []
-fun type_arg_cover thy pos body s ary =
+fun type_arg_cover thy pos s ary =
if is_tptp_equal s then
if pos = SOME false then [] else 0 upto ary - 1
else
let
- val footprint = tvar_footprint thy body s ary
+ val footprint = tvar_footprint thy s ary
val eq = (s = @{const_name HOL.eq})
fun cover _ [] = []
| cover seen ((i, tvars) :: args) =
@@ -1391,8 +1389,7 @@
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Löwenheim-Skolem). *)
-fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
- | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
+fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
(Nonmono_Types (strictness, _)) T =
let val thy = Proof_Context.theory_of ctxt in
@@ -1402,16 +1399,18 @@
is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
T)))
end
- | should_encode_type _ _ Undercover_Types _ = true
- | should_encode_type _ _ _ _ = false
+ | should_encode_type _ _ level _ =
+ (level = All_Types orelse level = Undercover_Types)
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
should_guard_var () andalso should_encode_type ctxt mono level T
| should_guard_type _ _ _ _ _ = false
-fun is_maybe_universal_var (IConst ((s, _), _, _)) =
- String.isPrefix bound_var_prefix s orelse
- String.isPrefix all_bound_var_prefix s
+fun is_maybe_universal_name s =
+ String.isPrefix bound_var_prefix s orelse
+ String.isPrefix all_bound_var_prefix s
+
+fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s
| is_maybe_universal_var (IVar _) = true
| is_maybe_universal_var _ = false
@@ -1433,7 +1432,7 @@
(case (site, is_maybe_universal_var u) of
(Eq_Arg pos, true) => pos <> SOME false
| (Arg (s, j, ary), true) =>
- member (op =) (type_arg_cover thy NONE true s ary) j
+ member (op =) (type_arg_cover thy NONE s ary) j
| _ => false)
| _ => should_encode_type ctxt mono level T
end
@@ -1516,8 +1515,7 @@
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, _), T, _) =>
- if String.isPrefix bound_var_prefix s orelse
- String.isPrefix all_bound_var_prefix s then
+ if is_maybe_universal_name s then
add_universal_var T accum
else if String.isPrefix exist_bound_var_prefix s then
accum
@@ -1998,7 +1996,7 @@
| is_undercover (ATerm (((s, _), _), tms)) =
let
val ary = length tms
- val cover = type_arg_cover thy pos true s ary
+ val cover = type_arg_cover thy pos s ary
in
exists (fn (j, tm) => tm = var andalso member (op =) cover j)
(0 upto ary - 1 ~~ tms) orelse
@@ -2010,11 +2008,11 @@
fun should_guard_var_in_formula thy level pos phi (SOME true) name =
(case level of
All_Types => true
+ | Undercover_Types =>
+ formula_fold pos (is_var_undercover_in_term thy name) phi false
| Nonmono_Types (_, Uniform) => true
| Nonmono_Types (_, Non_Uniform) =>
formula_fold pos (is_var_positively_naked_in_term name) phi false
- | Undercover_Types =>
- formula_fold pos (is_var_undercover_in_term thy name) phi false
| _ => false)
| should_guard_var_in_formula _ _ _ _ _ _ = true
@@ -2054,6 +2052,7 @@
Top_Level pos => pos
| Eq_Arg pos => pos
| _ => NONE
+ val T = ityp_of u
val t =
case head of
IConst (name as (s, _), _, T_args) =>
@@ -2074,13 +2073,8 @@
else
raise Fail "unexpected lambda-abstraction"
| IApp _ => raise Fail "impossible \"IApp\""
- val T = ityp_of u
- in
- if should_tag_with_type ctxt mono type_enc site u T then
- tag_with_type ctxt mono type_enc pos T t
- else
- t
- end
+ val tag = should_tag_with_type ctxt mono type_enc site u T
+ in t |> tag ? tag_with_type ctxt mono type_enc pos T end
in term (Top_Level pos) end
and formula_from_iformula ctxt mono type_enc should_guard_var =
let
@@ -2263,6 +2257,7 @@
else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
fun add_undefined_const T =
let
+ (* FIXME: make sure type arguments are filtered / clean up code *)
val (s, s') =
`(make_fixed_const NONE) @{const_name undefined}
|> (case type_arg_policy [] type_enc @{const_name undefined} of
@@ -2420,7 +2415,7 @@
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
val bound_Ts =
if exists (curry (op =) dummyT) T_args then
- let val cover = type_arg_cover thy NONE true s ary in
+ let val cover = type_arg_cover thy NONE s ary in
map2 (fn j => if member (op =) cover j then SOME else K NONE)
(0 upto ary - 1) arg_Ts
end
@@ -2455,30 +2450,22 @@
val bounds = bound_names |> map (fn name => ATerm ((name, []), []))
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 mono type_enc NONE
- val add_formula_for_res =
- if should_encode res_T then
- let
- val (lhs, rhs) =
- if level = Undercover_Types then
- let
- val lhs_cover = type_arg_cover thy NONE false s ary
- val rhs_cover = type_arg_cover thy NONE true s ary
- fun maybe_tag cover (j, arg_T) =
- member (op =) cover j ? tag_with arg_T
- fun covered_bounds cover =
- map2 (maybe_tag cover) (0 upto ary - 1 ~~ arg_Ts) bounds
- in (lhs_cover, rhs_cover) |> pairself (covered_bounds #> cst) end
- else
- `I (cst bounds)
- in
- cons (Formula (ident, role, eq (tag_with res_T lhs) rhs,
- NONE, isabelle_info defN helper_rank))
- end
- else
- I
- in [] |> not pred_sym ? add_formula_for_res end
+ fun formula c =
+ [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
+ defN helper_rank)]
+ in
+ if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
+ []
+ else if level = Undercover_Types then
+ let
+ val cover = type_arg_cover thy NONE s ary
+ fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
+ val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
+ in formula (cst bounds) end
+ else
+ formula (cst bounds)
+ end
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd