File ‹Tools/typechk.ML›
signature TYPE_CHECK =
sig
val print_tcset: Proof.context -> unit
val TC_add: attribute
val TC_del: attribute
val typecheck_tac: Proof.context -> tactic
val type_solver_tac: Proof.context -> thm list -> int -> tactic
val type_solver: solver
end;
structure TypeCheck: TYPE_CHECK =
struct
datatype tcset = TC of
{rules: thm list,
net: thm Net.net};
fun add_rule ctxt th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
(warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs)
else
TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
fun del_rule ctxt th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
rules = remove Thm.eq_thm_prop th rules}
else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs);
structure Data = Generic_Data
(
type T = tcset;
val empty = TC {rules = [], net = Net.empty};
fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
);
val TC_add =
Thm.declaration_attribute (fn thm => fn context =>
Data.map (add_rule (Context.proof_of context) (Thm.trim_context thm)) context);
val TC_del =
Thm.declaration_attribute (fn thm => fn context =>
Data.map (del_rule (Context.proof_of context) thm) context);
val tcset_of = Data.get o Context.Proof;
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
(map (Thm.pretty_thm_item ctxt) rules))
end;
fun net_res_tac ctxt maxr net =
SUBGOAL
(fn (prem, i) =>
let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
in
if length rls <= maxr then resolve_tac ctxt rls i else no_tac
end);
fun is_rigid_elem \<^Const_>‹Trueprop for \<^Const_>‹mem for a _›› = not (is_Var (head_of a))
| is_rigid_elem _ = false;
fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) =>
if is_rigid_elem (Logic.strip_assums_concl prem)
then assume_tac ctxt i else eq_assume_tac i);
fun typecheck_step_tac ctxt =
let val TC {net, ...} = tcset_of ctxt
in FIRSTGOAL (test_assume_tac ctxt ORELSE' net_res_tac ctxt 3 net) end;
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt);
val basic_net =
Tactic.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI};
fun type_solver_tac ctxt hyps = SELECT_GOAL
(DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1
ORELSE resolve_from_net_tac ctxt basic_net 1
ORELSE (ares_tac ctxt hyps 1
APPEND typecheck_step_tac ctxt)));
val type_solver =
Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
type_solver_tac ctxt (Simplifier.prems_of ctxt));
val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver));
val _ =
Theory.setup
(Attrib.setup \<^binding>‹TC› (Attrib.add_del TC_add TC_del)
"declaration of type-checking rule" #>
Method.setup \<^binding>‹typecheck›
(Method.sections
[Args.add -- Args.colon >> K (Method.modifier TC_add ⌂),
Args.del -- Args.colon >> K (Method.modifier TC_del ⌂)]
>> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
"ZF type-checking");
val _ =
Outer_Syntax.command \<^command_keyword>‹print_tcset› "print context of ZF typecheck"
(Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of)));
end;