20 text {* Setup for testing Metis exhaustively *} |
20 text {* Setup for testing Metis exhaustively *} |
21 |
21 |
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
23 |
23 |
24 ML {* |
24 ML {* |
25 open ATP_Translate |
25 (* The commented-out type systems are too incomplete for our exhaustive |
26 |
26 tests. *) |
27 val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic] |
|
28 val levels = |
|
29 [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types] |
|
30 val heaviness = [Heavyweight, Lightweight] |
|
31 val type_syss = |
27 val type_syss = |
32 (levels |> map Simple_Types) @ |
28 ["erased", |
33 (map_product pair levels heaviness |
29 "poly_preds", |
34 (* The following two families of type systems are too incomplete for our |
30 "poly_preds_heavy", |
35 tests. *) |
31 "poly_tags", |
36 |> remove (op =) (Nonmonotonic_Types, Heavyweight) |
32 "poly_tags_heavy", |
37 |> remove (op =) (Finite_Types, Heavyweight) |
33 "poly_args", |
38 |> map_product pair polymorphisms |
34 "mono_preds", |
39 |> map_product (fn constr => fn (poly, (level, heaviness)) => |
35 "mono_preds_heavy", |
40 constr (poly, level, heaviness)) |
36 "mono_tags", |
41 [Preds, Tags]) |
37 "mono_tags_heavy", |
|
38 "mono_args", |
|
39 "mangled_preds", |
|
40 "mangled_preds_heavy", |
|
41 "mangled_tags", |
|
42 "mangled_tags_heavy", |
|
43 "mangled_args", |
|
44 "simple", |
|
45 "poly_preds?", |
|
46 (* "poly_preds_heavy?", *) |
|
47 (* "poly_tags?", *) |
|
48 (* "poly_tags_heavy?", *) |
|
49 "mono_preds?", |
|
50 "mono_preds_heavy?", |
|
51 "mono_tags?", |
|
52 "mono_tags_heavy?", |
|
53 "mangled_preds?", |
|
54 "mangled_preds_heavy?", |
|
55 "mangled_tags?", |
|
56 "mangled_tags_heavy?", |
|
57 "simple?", |
|
58 "poly_preds!", |
|
59 (* "poly_preds_heavy!", *) |
|
60 (* "poly_tags!", *) |
|
61 (* "poly_tags_heavy!", *) |
|
62 "mono_preds!", |
|
63 "mono_preds_heavy!", |
|
64 "mono_tags!", |
|
65 "mono_tags_heavy!", |
|
66 "mangled_preds!", |
|
67 "mangled_preds_heavy!", |
|
68 "mangled_tags!", |
|
69 "mangled_tags_heavy!", |
|
70 "simple!"] |
42 |
71 |
43 fun new_metis_exhaust_tac ctxt ths = |
72 fun new_metis_exhaust_tac ctxt ths = |
44 let |
73 let |
45 fun tac [] st = all_tac st |
74 fun tac [] st = all_tac st |
46 | tac (type_sys :: type_syss) st = |
75 | tac (type_sys :: type_syss) st = |