author | wenzelm |
Mon, 17 May 2010 23:54:15 +0200 | |
changeset 36960 | 01594f816e3a |
parent 35409 | 5c5bb83f2bae |
child 38522 | de7984a7172b |
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 |
||
33519 | 46 |
structure Data = Generic_Data |
18736 | 47 |
( |
33519 | 48 |
type T = tcset; |
18736 | 49 |
val empty = TC {rules = [], net = Net.empty}; |
50 |
val extend = I; |
|
33519 | 51 |
fun merge (TC {rules, net}, TC {rules = rules', net = net'}) = |
52 |
TC {rules = Thm.merge_thms (rules, rules'), 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:" |
|
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
|
63 |
(map (Display.pretty_thm ctxt) rules)) |
22846 | 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 |
35409 | 101 |
(DEPTH_SOLVE (etac @{thm 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 |
|
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
|
112 |
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
|
113 |
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
|
114 |
(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
|
115 |
[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
|
116 |
Args.del -- Args.colon >> K (I, TC_del)] |
32170 | 117 |
>> 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
|
118 |
"ZF type-checking"; |
12189 | 119 |
|
24867 | 120 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35409
diff
changeset
|
121 |
Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag |
18736 | 122 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
24867 | 123 |
Toplevel.keep (print_tcset o Toplevel.context_of))); |
12189 | 124 |
|
125 |
||
18736 | 126 |
(* theory setup *) |
12189 | 127 |
|
128 |
val setup = |
|
30528 | 129 |
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
|
130 |
typecheck_setup #> |
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26287
diff
changeset
|
131 |
Simplifier.map_simpset (fn ss => ss setSolver type_solver); |
12189 | 132 |
|
133 |
end; |