wenzelm@12189: (* Title: ZF/Tools/typechk.ML paulson@6049: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@6153: Copyright 1999 University of Cambridge paulson@6049: wenzelm@18736: Automated type checking (cf. CTT). paulson@6049: *) paulson@6049: wenzelm@12189: signature TYPE_CHECK = wenzelm@12189: sig wenzelm@21506: val print_tcset: Proof.context -> unit wenzelm@18736: val TC_add: attribute wenzelm@18736: val TC_del: attribute wenzelm@18736: val typecheck_tac: Proof.context -> tactic wenzelm@18736: val type_solver_tac: Proof.context -> thm list -> int -> tactic wenzelm@18736: val type_solver: solver wenzelm@12189: end; wenzelm@12189: wenzelm@12189: structure TypeCheck: TYPE_CHECK = paulson@6153: struct wenzelm@12189: wenzelm@18736: (* datatype tcset *) wenzelm@18736: wenzelm@18736: datatype tcset = TC of wenzelm@18736: {rules: thm list, (*the type-checking rules*) wenzelm@18736: net: thm Net.net}; (*discrimination net of the same rules*) wenzelm@18736: wenzelm@42439: fun add_rule ctxt th (tcs as TC {rules, net}) = wenzelm@22360: if member Thm.eq_thm_prop rules th then wenzelm@42439: (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs) wenzelm@18736: else wenzelm@42439: TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net}; wenzelm@18736: wenzelm@42439: fun del_rule ctxt th (tcs as TC {rules, net}) = wenzelm@22360: if member Thm.eq_thm_prop rules th then wenzelm@22360: TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, wenzelm@42439: rules = remove Thm.eq_thm_prop th rules} wenzelm@42439: else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs); paulson@6153: paulson@6153: wenzelm@18736: (* generic data *) wenzelm@18736: wenzelm@33519: structure Data = Generic_Data wenzelm@18736: ( wenzelm@33519: type T = tcset; wenzelm@18736: val empty = TC {rules = [], net = Net.empty}; wenzelm@18736: val extend = I; wenzelm@33519: fun merge (TC {rules, net}, TC {rules = rules', net = net'}) = wenzelm@33519: TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')}; wenzelm@18736: ); wenzelm@18736: wenzelm@42439: val TC_add = wenzelm@42439: Thm.declaration_attribute (fn thm => fn context => wenzelm@42439: Data.map (add_rule (Context.proof_of context) thm) context); wenzelm@42439: wenzelm@42439: val TC_del = wenzelm@42439: Thm.declaration_attribute (fn thm => fn context => wenzelm@42439: Data.map (del_rule (Context.proof_of context) thm) context); wenzelm@18736: wenzelm@18736: val tcset_of = Data.get o Context.Proof; paulson@6153: wenzelm@22846: fun print_tcset ctxt = wenzelm@22846: let val TC {rules, ...} = tcset_of ctxt in wenzelm@22846: Pretty.writeln (Pretty.big_list "type-checking rules:" wenzelm@51584: (map (Display.pretty_thm_item ctxt) rules)) wenzelm@22846: end; wenzelm@22846: paulson@6153: wenzelm@18736: (* tactics *) paulson@6153: paulson@6153: (*resolution using a net rather than rules*) paulson@6153: fun net_res_tac maxr net = paulson@6153: SUBGOAL paulson@6153: (fn (prem,i) => paulson@6153: let val rls = Net.unify_term net (Logic.strip_assums_concl prem) wenzelm@12189: in wenzelm@12189: if length rls <= maxr then resolve_tac rls i else no_tac paulson@6153: end); paulson@6153: haftmann@38522: fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) = paulson@6049: not (is_Var (head_of a)) paulson@6049: | is_rigid_elem _ = false; paulson@6049: wenzelm@12189: (*Try solving a:A by assumption provided a is rigid!*) paulson@6049: val test_assume_tac = SUBGOAL(fn (prem,i) => paulson@6049: if is_rigid_elem (Logic.strip_assums_concl prem) paulson@6049: then assume_tac i else eq_assume_tac i); paulson@6049: wenzelm@12189: (*Type checking solves a:?A (a rigid, ?A maybe flexible). paulson@6049: match_tac is too strict; would refuse to instantiate ?A*) paulson@6153: fun typecheck_step_tac (TC{net,...}) = paulson@6153: FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); paulson@6049: wenzelm@18736: fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt)); paulson@6049: paulson@6153: (*Compiles a term-net for speed*) wenzelm@26287: val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, wenzelm@26287: @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}]; paulson@6049: paulson@6049: (*Instantiates variables in typing conditions. paulson@6049: drawback: does not simplify conjunctions*) wenzelm@18736: fun type_solver_tac ctxt hyps = SELECT_GOAL wenzelm@58838: (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1 wenzelm@12189: ORELSE basic_res_tac 1 wenzelm@12189: ORELSE (ares_tac hyps 1 wenzelm@18736: APPEND typecheck_step_tac (tcset_of ctxt)))); wenzelm@12189: wenzelm@43596: val type_solver = wenzelm@51717: Simplifier.mk_solver "ZF typecheck" (fn ctxt => wenzelm@51717: type_solver_tac ctxt (Simplifier.prems_of ctxt)); paulson@6153: wenzelm@58828: val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver)); wenzelm@58828: paulson@6153: wenzelm@18736: (* concrete syntax *) wenzelm@12189: wenzelm@58828: val _ = wenzelm@58828: Theory.setup wenzelm@58828: (Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) wenzelm@58828: "declaration of type-checking rule" #> wenzelm@58828: Method.setup @{binding typecheck} wenzelm@58828: (Method.sections wenzelm@58828: [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}), wenzelm@58828: Args.del -- Args.colon >> K (Method.modifier TC_del @{here})] wenzelm@58828: >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))) wenzelm@58828: "ZF type-checking"); wenzelm@12189: wenzelm@24867: val _ = wenzelm@46961: Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck" wenzelm@51658: (Scan.succeed (Toplevel.unknown_context o wenzelm@24867: Toplevel.keep (print_tcset o Toplevel.context_of))); wenzelm@12189: wenzelm@12189: end;