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}) =
|
|
30 |
if member Drule.eq_thm_prop rules th then
|
|
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}) =
|
|
37 |
if member Drule.eq_thm_prop rules th then
|
|
38 |
TC {net = Net.delete_term Drule.eq_thm_prop (Thm.concl_of th, th) net,
|
|
39 |
rules = remove Drule.eq_thm_prop th rules}
|
|
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 |
val name = "ZF/type-checking";
|
|
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'}) =
|
20193
|
53 |
TC {rules = Drule.merge_rules (rules, rules'),
|
18736
|
54 |
net = Net.merge Drule.eq_thm_prop (net, net')};
|
|
55 |
|
|
56 |
fun print context (TC {rules, ...}) =
|
|
57 |
Pretty.writeln (Pretty.big_list "type-checking rules:"
|
|
58 |
(map (ProofContext.pretty_thm (Context.proof_of context)) rules));
|
|
59 |
);
|
|
60 |
|
21506
|
61 |
val print_tcset = Data.print o Context.Proof;
|
18736
|
62 |
|
|
63 |
val TC_add = Thm.declaration_attribute (Data.map o add_rule);
|
|
64 |
val TC_del = Thm.declaration_attribute (Data.map o del_rule);
|
|
65 |
|
|
66 |
val tcset_of = Data.get o Context.Proof;
|
6153
|
67 |
|
|
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 |
|
12189
|
80 |
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ 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*)
|
|
97 |
val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
|
12189
|
98 |
ballI,allI,conjI,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 |
|
18736
|
114 |
val TC_att = Attrib.add_del_args TC_add TC_del;
|
12189
|
115 |
|
18736
|
116 |
val typecheck_meth =
|
|
117 |
Method.only_sectioned_args
|
|
118 |
[Args.add -- Args.colon >> K (I, TC_add),
|
|
119 |
Args.del -- Args.colon >> K (I, TC_del)]
|
|
120 |
(fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
|
12189
|
121 |
|
18736
|
122 |
val _ = OuterSyntax.add_parsers
|
|
123 |
[OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
|
|
124 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
|
|
125 |
Toplevel.keep (print_tcset o Toplevel.context_of)))];
|
12189
|
126 |
|
|
127 |
|
18736
|
128 |
(* theory setup *)
|
12189
|
129 |
|
|
130 |
val setup =
|
18736
|
131 |
Data.init #>
|
|
132 |
Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
|
|
133 |
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
|
|
134 |
(fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));
|
12189
|
135 |
|
|
136 |
end;
|