author | wenzelm |
Sun, 29 Jul 2007 14:29:54 +0200 | |
changeset 24039 | 273698405054 |
parent 22846 | fb79144af9a3 |
child 24826 | 78e6a3cea367 |
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 |
|
18736 | 6 |
Automated type checking (cf. CTT). |
6049 | 7 |
*) |
8 |
||
12189 | 9 |
signature TYPE_CHECK = |
10 |
sig |
|
21506 | 11 |
val print_tcset: Proof.context -> unit |
18736 | 12 |
val TC_add: attribute |
13 |
val TC_del: attribute |
|
14 |
val typecheck_tac: Proof.context -> tactic |
|
15 |
val type_solver_tac: Proof.context -> thm list -> int -> tactic |
|
16 |
val type_solver: solver |
|
18708 | 17 |
val setup: theory -> theory |
12189 | 18 |
end; |
19 |
||
20 |
structure TypeCheck: TYPE_CHECK = |
|
6153 | 21 |
struct |
12189 | 22 |
|
18736 | 23 |
(* datatype tcset *) |
24 |
||
25 |
datatype tcset = TC of |
|
26 |
{rules: thm list, (*the type-checking rules*) |
|
27 |
net: thm Net.net}; (*discrimination net of the same rules*) |
|
28 |
||
29 |
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
|
30 |
if member Thm.eq_thm_prop rules th then |
18736 | 31 |
(warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs) |
32 |
else |
|
33 |
TC {rules = th :: rules, |
|
34 |
net = Net.insert_term (K false) (Thm.concl_of th, th) net}; |
|
35 |
||
36 |
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
|
37 |
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
|
38 |
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
|
39 |
rules = remove Thm.eq_thm_prop th rules} |
18736 | 40 |
else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs); |
6153 | 41 |
|
42 |
||
18736 | 43 |
(* generic data *) |
44 |
||
45 |
structure Data = GenericDataFun |
|
46 |
( |
|
47 |
type T = tcset |
|
48 |
val empty = TC {rules = [], net = Net.empty}; |
|
49 |
val extend = I; |
|
6153 | 50 |
|
18736 | 51 |
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
|
52 |
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
|
53 |
net = Net.merge Thm.eq_thm_prop (net, net')}; |
18736 | 54 |
); |
55 |
||
56 |
val TC_add = Thm.declaration_attribute (Data.map o add_rule); |
|
57 |
val TC_del = Thm.declaration_attribute (Data.map o del_rule); |
|
58 |
||
59 |
val tcset_of = Data.get o Context.Proof; |
|
6153 | 60 |
|
22846 | 61 |
fun print_tcset ctxt = |
62 |
let val TC {rules, ...} = tcset_of ctxt in |
|
63 |
Pretty.writeln (Pretty.big_list "type-checking rules:" |
|
64 |
(map (ProofContext.pretty_thm ctxt) rules)) |
|
65 |
end; |
|
66 |
||
6153 | 67 |
|
18736 | 68 |
(* tactics *) |
6153 | 69 |
|
70 |
(*resolution using a net rather than rules*) |
|
71 |
fun net_res_tac maxr net = |
|
72 |
SUBGOAL |
|
73 |
(fn (prem,i) => |
|
74 |
let val rls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
12189 | 75 |
in |
76 |
if length rls <= maxr then resolve_tac rls i else no_tac |
|
6153 | 77 |
end); |
78 |
||
12189 | 79 |
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = |
6049 | 80 |
not (is_Var (head_of a)) |
81 |
| is_rigid_elem _ = false; |
|
82 |
||
12189 | 83 |
(*Try solving a:A by assumption provided a is rigid!*) |
6049 | 84 |
val test_assume_tac = SUBGOAL(fn (prem,i) => |
85 |
if is_rigid_elem (Logic.strip_assums_concl prem) |
|
86 |
then assume_tac i else eq_assume_tac i); |
|
87 |
||
12189 | 88 |
(*Type checking solves a:?A (a rigid, ?A maybe flexible). |
6049 | 89 |
match_tac is too strict; would refuse to instantiate ?A*) |
6153 | 90 |
fun typecheck_step_tac (TC{net,...}) = |
91 |
FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); |
|
6049 | 92 |
|
18736 | 93 |
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt)); |
6049 | 94 |
|
6153 | 95 |
(*Compiles a term-net for speed*) |
96 |
val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl, |
|
12189 | 97 |
ballI,allI,conjI,impI]; |
6049 | 98 |
|
99 |
(*Instantiates variables in typing conditions. |
|
100 |
drawback: does not simplify conjunctions*) |
|
18736 | 101 |
fun type_solver_tac ctxt hyps = SELECT_GOAL |
6153 | 102 |
(DEPTH_SOLVE (etac FalseE 1 |
12189 | 103 |
ORELSE basic_res_tac 1 |
104 |
ORELSE (ares_tac hyps 1 |
|
18736 | 105 |
APPEND typecheck_step_tac (tcset_of ctxt)))); |
12189 | 106 |
|
18736 | 107 |
val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => |
108 |
type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
|
6153 | 109 |
|
110 |
||
18736 | 111 |
(* concrete syntax *) |
12189 | 112 |
|
18736 | 113 |
val TC_att = Attrib.add_del_args TC_add TC_del; |
12189 | 114 |
|
18736 | 115 |
val typecheck_meth = |
116 |
Method.only_sectioned_args |
|
117 |
[Args.add -- Args.colon >> K (I, TC_add), |
|
118 |
Args.del -- Args.colon >> K (I, TC_del)] |
|
119 |
(fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); |
|
12189 | 120 |
|
18736 | 121 |
val _ = OuterSyntax.add_parsers |
122 |
[OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
|
123 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
|
124 |
Toplevel.keep (print_tcset o Toplevel.context_of)))]; |
|
12189 | 125 |
|
126 |
||
18736 | 127 |
(* theory setup *) |
12189 | 128 |
|
129 |
val setup = |
|
18736 | 130 |
Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #> |
131 |
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #> |
|
132 |
(fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy)); |
|
12189 | 133 |
|
134 |
end; |