author | wenzelm |
Tue, 21 Jul 2009 01:03:18 +0200 | |
changeset 32091 | 30e2ffbba718 |
parent 30722 | 623d4831c8cf |
child 32170 | 541b35729992 |
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 |
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
|
30 |
(warning ("Ignoring duplicate type-checking rule\n" ^ |
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
|
31 |
Display.string_of_thm_without_context th); tcs) |
18736 | 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} |
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
|
40 |
else (warning ("No such type-checking rule\n" ^ |
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
|
41 |
Display.string_of_thm_without_context th); tcs); |
6153 | 42 |
|
43 |
||
18736 | 44 |
(* generic data *) |
45 |
||
46 |
structure Data = GenericDataFun |
|
47 |
( |
|
48 |
type T = tcset |
|
49 |
val empty = TC {rules = [], net = Net.empty}; |
|
50 |
val extend = I; |
|
6153 | 51 |
|
18736 | 52 |
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
|
53 |
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
|
54 |
net = Net.merge Thm.eq_thm_prop (net, net')}; |
18736 | 55 |
); |
56 |
||
57 |
val TC_add = Thm.declaration_attribute (Data.map o add_rule); |
|
58 |
val TC_del = Thm.declaration_attribute (Data.map o del_rule); |
|
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 |
||
24826 | 80 |
fun is_rigid_elem (Const("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 |
6153 | 103 |
(DEPTH_SOLVE (etac 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)] |
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
|
119 |
>> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))) |
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 _ = |
123 |
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.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 #> |
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26287
diff
changeset
|
133 |
Simplifier.map_simpset (fn ss => ss setSolver type_solver); |
12189 | 134 |
|
135 |
end; |