author | wenzelm |
Fri, 13 May 2011 23:58:40 +0200 | |
changeset 42795 | 66fcc9882784 |
parent 42439 | 9efdd0af15ac |
child 43596 | 78211f66cf8d |
permissions | -rw-r--r-- |
12189 | 1 |
(* Title: ZF/Tools/typechk.ML |
6049 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6153 | 3 |
Copyright 1999 University of Cambridge |
6049 | 4 |
|
18736 | 5 |
Automated type checking (cf. CTT). |
6049 | 6 |
*) |
7 |
||
12189 | 8 |
signature TYPE_CHECK = |
9 |
sig |
|
21506 | 10 |
val print_tcset: Proof.context -> unit |
18736 | 11 |
val TC_add: attribute |
12 |
val TC_del: attribute |
|
13 |
val typecheck_tac: Proof.context -> tactic |
|
14 |
val type_solver_tac: Proof.context -> thm list -> int -> tactic |
|
15 |
val type_solver: solver |
|
18708 | 16 |
val setup: theory -> theory |
12189 | 17 |
end; |
18 |
||
19 |
structure TypeCheck: TYPE_CHECK = |
|
6153 | 20 |
struct |
12189 | 21 |
|
18736 | 22 |
(* datatype tcset *) |
23 |
||
24 |
datatype tcset = TC of |
|
25 |
{rules: thm list, (*the type-checking rules*) |
|
26 |
net: thm Net.net}; (*discrimination net of the same rules*) |
|
27 |
||
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
28 |
fun add_rule ctxt th (tcs as TC {rules, net}) = |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21506
diff
changeset
|
29 |
if member Thm.eq_thm_prop rules th then |
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
30 |
(warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs) |
18736 | 31 |
else |
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
32 |
TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net}; |
18736 | 33 |
|
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
34 |
fun del_rule ctxt th (tcs as TC {rules, net}) = |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21506
diff
changeset
|
35 |
if member Thm.eq_thm_prop rules th then |
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21506
diff
changeset
|
36 |
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, |
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
37 |
rules = remove Thm.eq_thm_prop th rules} |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
38 |
else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs); |
6153 | 39 |
|
40 |
||
18736 | 41 |
(* generic data *) |
42 |
||
33519 | 43 |
structure Data = Generic_Data |
18736 | 44 |
( |
33519 | 45 |
type T = tcset; |
18736 | 46 |
val empty = TC {rules = [], net = Net.empty}; |
47 |
val extend = I; |
|
33519 | 48 |
fun merge (TC {rules, net}, TC {rules = rules', net = net'}) = |
49 |
TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')}; |
|
18736 | 50 |
); |
51 |
||
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
52 |
val TC_add = |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
53 |
Thm.declaration_attribute (fn thm => fn context => |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
54 |
Data.map (add_rule (Context.proof_of context) thm) context); |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
55 |
|
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
56 |
val TC_del = |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
57 |
Thm.declaration_attribute (fn thm => fn context => |
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
38522
diff
changeset
|
58 |
Data.map (del_rule (Context.proof_of context) thm) context); |
18736 | 59 |
|
60 |
val tcset_of = Data.get o Context.Proof; |
|
6153 | 61 |
|
22846 | 62 |
fun print_tcset ctxt = |
63 |
let val TC {rules, ...} = tcset_of ctxt in |
|
64 |
Pretty.writeln (Pretty.big_list "type-checking rules:" |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30722
diff
changeset
|
65 |
(map (Display.pretty_thm ctxt) rules)) |
22846 | 66 |
end; |
67 |
||
6153 | 68 |
|
18736 | 69 |
(* tactics *) |
6153 | 70 |
|
71 |
(*resolution using a net rather than rules*) |
|
72 |
fun net_res_tac maxr net = |
|
73 |
SUBGOAL |
|
74 |
(fn (prem,i) => |
|
75 |
let val rls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
12189 | 76 |
in |
77 |
if length rls <= maxr then resolve_tac rls i else no_tac |
|
6153 | 78 |
end); |
79 |
||
38522 | 80 |
fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) = |
6049 | 81 |
not (is_Var (head_of a)) |
82 |
| is_rigid_elem _ = false; |
|
83 |
||
12189 | 84 |
(*Try solving a:A by assumption provided a is rigid!*) |
6049 | 85 |
val test_assume_tac = SUBGOAL(fn (prem,i) => |
86 |
if is_rigid_elem (Logic.strip_assums_concl prem) |
|
87 |
then assume_tac i else eq_assume_tac i); |
|
88 |
||
12189 | 89 |
(*Type checking solves a:?A (a rigid, ?A maybe flexible). |
6049 | 90 |
match_tac is too strict; would refuse to instantiate ?A*) |
6153 | 91 |
fun typecheck_step_tac (TC{net,...}) = |
92 |
FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); |
|
6049 | 93 |
|
18736 | 94 |
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt)); |
6049 | 95 |
|
6153 | 96 |
(*Compiles a term-net for speed*) |
26287 | 97 |
val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, |
98 |
@{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}]; |
|
6049 | 99 |
|
100 |
(*Instantiates variables in typing conditions. |
|
101 |
drawback: does not simplify conjunctions*) |
|
18736 | 102 |
fun type_solver_tac ctxt hyps = SELECT_GOAL |
35409 | 103 |
(DEPTH_SOLVE (etac @{thm FalseE} 1 |
12189 | 104 |
ORELSE basic_res_tac 1 |
105 |
ORELSE (ares_tac hyps 1 |
|
18736 | 106 |
APPEND typecheck_step_tac (tcset_of ctxt)))); |
12189 | 107 |
|
18736 | 108 |
val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => |
109 |
type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
|
6153 | 110 |
|
111 |
||
18736 | 112 |
(* concrete syntax *) |
12189 | 113 |
|
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
114 |
val typecheck_setup = |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
115 |
Method.setup @{binding typecheck} |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
116 |
(Method.sections |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
117 |
[Args.add -- Args.colon >> K (I, TC_add), |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
118 |
Args.del -- Args.colon >> K (I, TC_del)] |
32170 | 119 |
>> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))) |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
120 |
"ZF type-checking"; |
12189 | 121 |
|
24867 | 122 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35409
diff
changeset
|
123 |
Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag |
18736 | 124 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
24867 | 125 |
Toplevel.keep (print_tcset o Toplevel.context_of))); |
12189 | 126 |
|
127 |
||
18736 | 128 |
(* theory setup *) |
12189 | 129 |
|
130 |
val setup = |
|
30528 | 131 |
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #> |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30541
diff
changeset
|
132 |
typecheck_setup #> |
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42439
diff
changeset
|
133 |
Simplifier.map_simpset_global (fn ss => ss setSolver type_solver); |
12189 | 134 |
|
135 |
end; |