author | wenzelm |
Mon, 17 Oct 2005 23:10:24 +0200 | |
changeset 17886 | 9a4aea3a9ae1 |
parent 17057 | 0934ac31985f |
child 18708 | 4b3dadb4fe33 |
permissions | -rw-r--r-- |
12189 | 1 |
(* Title: ZF/Tools/typechk.ML |
6049 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
6153 | 4 |
Copyright 1999 University of Cambridge |
6049 | 5 |
|
12189 | 6 |
Tactics for type checking -- from CTT. |
6049 | 7 |
*) |
8 |
||
6153 | 9 |
infix 4 addTCs delTCs; |
10 |
||
12189 | 11 |
signature BASIC_TYPE_CHECK = |
12 |
sig |
|
13 |
type tcset |
|
14 |
val addTCs: tcset * thm list -> tcset |
|
15 |
val delTCs: tcset * thm list -> tcset |
|
16 |
val typecheck_tac: tcset -> tactic |
|
17 |
val type_solver_tac: tcset -> thm list -> int -> tactic |
|
18 |
val print_tc: tcset -> unit |
|
19 |
val print_tcset: theory -> unit |
|
20 |
val tcset_ref_of: theory -> tcset ref |
|
21 |
val tcset_of: theory -> tcset |
|
22 |
val tcset: unit -> tcset |
|
12202 | 23 |
val TCSET: (tcset -> tactic) -> tactic |
24 |
val TCSET': (tcset -> 'a -> tactic) -> 'a -> tactic |
|
12189 | 25 |
val AddTCs: thm list -> unit |
26 |
val DelTCs: thm list -> unit |
|
27 |
val TC_add_global: theory attribute |
|
28 |
val TC_del_global: theory attribute |
|
29 |
val TC_add_local: Proof.context attribute |
|
30 |
val TC_del_local: Proof.context attribute |
|
31 |
val Typecheck_tac: tactic |
|
32 |
val Type_solver_tac: thm list -> int -> tactic |
|
15090 | 33 |
val local_tcset_of: Proof.context -> tcset |
17886 | 34 |
val type_solver: solver |
12189 | 35 |
end; |
36 |
||
37 |
signature TYPE_CHECK = |
|
38 |
sig |
|
39 |
include BASIC_TYPE_CHECK |
|
40 |
val setup: (theory -> theory) list |
|
41 |
end; |
|
42 |
||
43 |
structure TypeCheck: TYPE_CHECK = |
|
6153 | 44 |
struct |
12189 | 45 |
|
6153 | 46 |
datatype tcset = |
12189 | 47 |
TC of {rules: thm list, (*the type-checking rules*) |
48 |
net: thm Net.net}; (*discrimination net of the same rules*) |
|
6153 | 49 |
|
50 |
||
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12311
diff
changeset
|
51 |
val mem_thm = gen_mem Drule.eq_thm_prop |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12311
diff
changeset
|
52 |
and rem_thm = gen_rem Drule.eq_thm_prop; |
6153 | 53 |
|
54 |
fun addTC (cs as TC{rules, net}, th) = |
|
12189 | 55 |
if mem_thm (th, rules) then |
56 |
(warning ("Ignoring duplicate type-checking rule\n" ^ |
|
57 |
string_of_thm th); |
|
58 |
cs) |
|
6153 | 59 |
else |
12189 | 60 |
TC{rules = th::rules, |
16800 | 61 |
net = Net.insert_term (K false) (concl_of th, th) net}; |
6153 | 62 |
|
63 |
||
64 |
fun delTC (cs as TC{rules, net}, th) = |
|
65 |
if mem_thm (th, rules) then |
|
16800 | 66 |
TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net, |
12189 | 67 |
rules = rem_thm (rules,th)} |
68 |
else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); |
|
69 |
cs); |
|
6153 | 70 |
|
15570 | 71 |
val op addTCs = Library.foldl addTC; |
72 |
val op delTCs = Library.foldl delTC; |
|
6153 | 73 |
|
74 |
||
75 |
(*resolution using a net rather than rules*) |
|
76 |
fun net_res_tac maxr net = |
|
77 |
SUBGOAL |
|
78 |
(fn (prem,i) => |
|
79 |
let val rls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
12189 | 80 |
in |
81 |
if length rls <= maxr then resolve_tac rls i else no_tac |
|
6153 | 82 |
end); |
83 |
||
12189 | 84 |
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = |
6049 | 85 |
not (is_Var (head_of a)) |
86 |
| is_rigid_elem _ = false; |
|
87 |
||
12189 | 88 |
(*Try solving a:A by assumption provided a is rigid!*) |
6049 | 89 |
val test_assume_tac = SUBGOAL(fn (prem,i) => |
90 |
if is_rigid_elem (Logic.strip_assums_concl prem) |
|
91 |
then assume_tac i else eq_assume_tac i); |
|
92 |
||
12189 | 93 |
(*Type checking solves a:?A (a rigid, ?A maybe flexible). |
6049 | 94 |
match_tac is too strict; would refuse to instantiate ?A*) |
6153 | 95 |
fun typecheck_step_tac (TC{net,...}) = |
96 |
FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); |
|
6049 | 97 |
|
6153 | 98 |
fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset); |
6049 | 99 |
|
6153 | 100 |
(*Compiles a term-net for speed*) |
101 |
val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl, |
|
12189 | 102 |
ballI,allI,conjI,impI]; |
6049 | 103 |
|
104 |
(*Instantiates variables in typing conditions. |
|
105 |
drawback: does not simplify conjunctions*) |
|
6153 | 106 |
fun type_solver_tac tcset hyps = SELECT_GOAL |
107 |
(DEPTH_SOLVE (etac FalseE 1 |
|
12189 | 108 |
ORELSE basic_res_tac 1 |
109 |
ORELSE (ares_tac hyps 1 |
|
110 |
APPEND typecheck_step_tac tcset))); |
|
6153 | 111 |
|
112 |
||
113 |
||
114 |
fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) = |
|
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12311
diff
changeset
|
115 |
TC {rules = gen_union Drule.eq_thm_prop (rules,rules'), |
16800 | 116 |
net = Net.merge Drule.eq_thm_prop (net, net')}; |
6153 | 117 |
|
118 |
(*print tcsets*) |
|
119 |
fun print_tc (TC{rules,...}) = |
|
120 |
Pretty.writeln |
|
121 |
(Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules)); |
|
122 |
||
123 |
||
12189 | 124 |
(** global tcset **) |
125 |
||
6153 | 126 |
structure TypecheckingArgs = |
16458 | 127 |
struct |
6153 | 128 |
val name = "ZF/type-checker"; |
129 |
type T = tcset ref; |
|
130 |
val empty = ref (TC{rules=[], net=Net.empty}); |
|
6556 | 131 |
fun copy (ref tc) = ref tc; |
16458 | 132 |
val extend = copy; |
133 |
fun merge _ (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2)); |
|
6153 | 134 |
fun print _ (ref tc) = print_tc tc; |
16458 | 135 |
end; |
6153 | 136 |
|
137 |
structure TypecheckingData = TheoryDataFun(TypecheckingArgs); |
|
6049 | 138 |
|
6153 | 139 |
val print_tcset = TypecheckingData.print; |
140 |
val tcset_ref_of = TypecheckingData.get; |
|
16458 | 141 |
val tcset_of = ! o tcset_ref_of; |
142 |
val tcset = tcset_of o Context.the_context; |
|
143 |
val tcset_ref = tcset_ref_of o Context.the_context; |
|
6153 | 144 |
|
16458 | 145 |
fun TCSET tacf st = tacf (tcset_of (Thm.theory_of_thm st)) st; |
146 |
fun TCSET' tacf i st = tacf (tcset_of (Thm.theory_of_thm st)) i st; |
|
12202 | 147 |
|
12189 | 148 |
|
6153 | 149 |
(* change global tcset *) |
150 |
||
151 |
fun change_tcset f x = tcset_ref () := (f (tcset (), x)); |
|
152 |
||
153 |
val AddTCs = change_tcset (op addTCs); |
|
154 |
val DelTCs = change_tcset (op delTCs); |
|
155 |
||
156 |
fun Typecheck_tac st = typecheck_tac (tcset()) st; |
|
157 |
||
158 |
fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps; |
|
159 |
||
160 |
||
161 |
||
12189 | 162 |
(** local tcset **) |
163 |
||
16458 | 164 |
structure LocalTypecheckingData = ProofDataFun |
165 |
(struct |
|
12189 | 166 |
val name = TypecheckingArgs.name; |
167 |
type T = tcset; |
|
168 |
val init = tcset_of; |
|
169 |
fun print _ tcset = print_tc tcset; |
|
16458 | 170 |
end); |
12189 | 171 |
|
15090 | 172 |
val local_tcset_of = LocalTypecheckingData.get; |
173 |
||
174 |
||
175 |
(* solver *) |
|
176 |
||
17886 | 177 |
val type_solver = Simplifier.mk_solver' "ZF types" (fn ss => |
178 |
type_solver_tac (local_tcset_of (Simplifier.the_context ss)) (Simplifier.prems_of_ss ss)); |
|
12189 | 179 |
|
180 |
||
181 |
(* attributes *) |
|
182 |
||
183 |
fun global_att f (thy, th) = |
|
184 |
let val r = tcset_ref_of thy |
|
185 |
in r := f (! r, th); (thy, th) end; |
|
186 |
||
187 |
fun local_att f (ctxt, th) = (LocalTypecheckingData.map (fn tcset => f (tcset, th)) ctxt, th); |
|
188 |
||
189 |
val TC_add_global = global_att addTC; |
|
190 |
val TC_del_global = global_att delTC; |
|
191 |
val TC_add_local = local_att addTC; |
|
192 |
val TC_del_local = local_att delTC; |
|
193 |
||
194 |
val TC_attr = |
|
195 |
(Attrib.add_del_args TC_add_global TC_del_global, |
|
196 |
Attrib.add_del_args TC_add_local TC_del_local); |
|
197 |
||
198 |
||
199 |
(* methods *) |
|
200 |
||
201 |
fun TC_args x = Method.only_sectioned_args |
|
202 |
[Args.add -- Args.colon >> K (I, TC_add_local), |
|
203 |
Args.del -- Args.colon >> K (I, TC_del_local)] x; |
|
204 |
||
205 |
fun typecheck ctxt = |
|
15090 | 206 |
Method.SIMPLE_METHOD (CHANGED (typecheck_tac (local_tcset_of ctxt))); |
12189 | 207 |
|
208 |
||
209 |
||
210 |
(** theory setup **) |
|
211 |
||
212 |
val setup = |
|
213 |
[TypecheckingData.init, LocalTypecheckingData.init, |
|
17886 | 214 |
fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy), |
12189 | 215 |
Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")], |
216 |
Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]]; |
|
217 |
||
218 |
||
219 |
(** outer syntax **) |
|
220 |
||
221 |
val print_tcsetP = |
|
222 |
OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker" |
|
17057 | 223 |
OuterKeyword.diag |
12189 | 224 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep |
225 |
(Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of))))); |
|
226 |
||
227 |
val _ = OuterSyntax.add_parsers [print_tcsetP]; |
|
228 |
||
229 |
||
230 |
end; |
|
231 |
||
232 |
structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck; |
|
233 |
open BasicTypeCheck; |