author | wenzelm |
Sun, 15 Mar 2009 20:25:58 +0100 | |
changeset 30541 | 9f168bdc468a |
parent 30528 | 7173bf123335 |
child 30722 | 623d4831c8cf |
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 |
||
28 |
fun add_rule 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 |
18736 | 30 |
(warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs) |
31 |
else |
|
32 |
TC {rules = th :: rules, |
|
33 |
net = Net.insert_term (K false) (Thm.concl_of th, th) net}; |
|
34 |
||
35 |
fun del_rule 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
|
36 |
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
|
37 |
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, |
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21506
diff
changeset
|
38 |
rules = remove Thm.eq_thm_prop th rules} |
18736 | 39 |
else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs); |
6153 | 40 |
|
41 |
||
18736 | 42 |
(* generic data *) |
43 |
||
44 |
structure Data = GenericDataFun |
|
45 |
( |
|
46 |
type T = tcset |
|
47 |
val empty = TC {rules = [], net = Net.empty}; |
|
48 |
val extend = I; |
|
6153 | 49 |
|
18736 | 50 |
fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) = |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
51 |
TC {rules = Thm.merge_thms (rules, rules'), |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21506
diff
changeset
|
52 |
net = Net.merge Thm.eq_thm_prop (net, net')}; |
18736 | 53 |
); |
54 |
||
55 |
val TC_add = Thm.declaration_attribute (Data.map o add_rule); |
|
56 |
val TC_del = Thm.declaration_attribute (Data.map o del_rule); |
|
57 |
||
58 |
val tcset_of = Data.get o Context.Proof; |
|
6153 | 59 |
|
22846 | 60 |
fun print_tcset ctxt = |
61 |
let val TC {rules, ...} = tcset_of ctxt in |
|
62 |
Pretty.writeln (Pretty.big_list "type-checking rules:" |
|
63 |
(map (ProofContext.pretty_thm ctxt) rules)) |
|
64 |
end; |
|
65 |
||
6153 | 66 |
|
18736 | 67 |
(* tactics *) |
6153 | 68 |
|
69 |
(*resolution using a net rather than rules*) |
|
70 |
fun net_res_tac maxr net = |
|
71 |
SUBGOAL |
|
72 |
(fn (prem,i) => |
|
73 |
let val rls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
12189 | 74 |
in |
75 |
if length rls <= maxr then resolve_tac rls i else no_tac |
|
6153 | 76 |
end); |
77 |
||
24826 | 78 |
fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) = |
6049 | 79 |
not (is_Var (head_of a)) |
80 |
| is_rigid_elem _ = false; |
|
81 |
||
12189 | 82 |
(*Try solving a:A by assumption provided a is rigid!*) |
6049 | 83 |
val test_assume_tac = SUBGOAL(fn (prem,i) => |
84 |
if is_rigid_elem (Logic.strip_assums_concl prem) |
|
85 |
then assume_tac i else eq_assume_tac i); |
|
86 |
||
12189 | 87 |
(*Type checking solves a:?A (a rigid, ?A maybe flexible). |
6049 | 88 |
match_tac is too strict; would refuse to instantiate ?A*) |
6153 | 89 |
fun typecheck_step_tac (TC{net,...}) = |
90 |
FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); |
|
6049 | 91 |
|
18736 | 92 |
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt)); |
6049 | 93 |
|
6153 | 94 |
(*Compiles a term-net for speed*) |
26287 | 95 |
val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, |
96 |
@{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}]; |
|
6049 | 97 |
|
98 |
(*Instantiates variables in typing conditions. |
|
99 |
drawback: does not simplify conjunctions*) |
|
18736 | 100 |
fun type_solver_tac ctxt hyps = SELECT_GOAL |
6153 | 101 |
(DEPTH_SOLVE (etac FalseE 1 |
12189 | 102 |
ORELSE basic_res_tac 1 |
103 |
ORELSE (ares_tac hyps 1 |
|
18736 | 104 |
APPEND typecheck_step_tac (tcset_of ctxt)))); |
12189 | 105 |
|
18736 | 106 |
val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => |
107 |
type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
|
6153 | 108 |
|
109 |
||
18736 | 110 |
(* concrete syntax *) |
12189 | 111 |
|
18736 | 112 |
val typecheck_meth = |
30541 | 113 |
Method.sections |
18736 | 114 |
[Args.add -- Args.colon >> K (I, TC_add), |
115 |
Args.del -- Args.colon >> K (I, TC_del)] |
|
30541 | 116 |
>> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))); |
12189 | 117 |
|
24867 | 118 |
val _ = |
119 |
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
|
18736 | 120 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
24867 | 121 |
Toplevel.keep (print_tcset o Toplevel.context_of))); |
12189 | 122 |
|
123 |
||
18736 | 124 |
(* theory setup *) |
12189 | 125 |
|
126 |
val setup = |
|
30528 | 127 |
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #> |
30541 | 128 |
Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #> |
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26287
diff
changeset
|
129 |
Simplifier.map_simpset (fn ss => ss setSolver type_solver); |
12189 | 130 |
|
131 |
end; |