wenzelm@12189: (* Title: ZF/Tools/typechk.ML paulson@6049: ID: $Id$ 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@18708: val setup: theory -> theory 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@18736: fun add_rule th (tcs as TC {rules, net}) = wenzelm@22360: if member Thm.eq_thm_prop rules th then wenzelm@18736: (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs) wenzelm@18736: else wenzelm@18736: TC {rules = th :: rules, wenzelm@18736: net = Net.insert_term (K false) (Thm.concl_of th, th) net}; wenzelm@18736: wenzelm@18736: fun del_rule 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@22360: rules = remove Thm.eq_thm_prop th rules} wenzelm@18736: else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs); paulson@6153: paulson@6153: wenzelm@18736: (* generic data *) wenzelm@18736: wenzelm@18736: structure Data = GenericDataFun wenzelm@18736: ( wenzelm@18736: type T = tcset wenzelm@18736: val empty = TC {rules = [], net = Net.empty}; wenzelm@18736: val extend = I; paulson@6153: wenzelm@18736: fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) = wenzelm@24039: TC {rules = Thm.merge_thms (rules, rules'), wenzelm@22360: net = Net.merge Thm.eq_thm_prop (net, net')}; wenzelm@18736: ); wenzelm@18736: wenzelm@18736: val TC_add = Thm.declaration_attribute (Data.map o add_rule); wenzelm@18736: val TC_del = Thm.declaration_attribute (Data.map o del_rule); 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@22846: (map (ProofContext.pretty_thm 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: wenzelm@24826: fun is_rigid_elem (Const("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 paulson@6153: (DEPTH_SOLVE (etac 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@18736: val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => wenzelm@18736: type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); paulson@6153: paulson@6153: wenzelm@18736: (* concrete syntax *) wenzelm@12189: wenzelm@18736: val TC_att = Attrib.add_del_args TC_add TC_del; wenzelm@12189: wenzelm@18736: val typecheck_meth = wenzelm@18736: Method.only_sectioned_args wenzelm@18736: [Args.add -- Args.colon >> K (I, TC_add), wenzelm@18736: Args.del -- Args.colon >> K (I, TC_del)] wenzelm@30510: (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); wenzelm@12189: wenzelm@24867: val _ = wenzelm@24867: OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag wenzelm@18736: (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o wenzelm@24867: Toplevel.keep (print_tcset o Toplevel.context_of))); wenzelm@12189: wenzelm@12189: wenzelm@18736: (* theory setup *) wenzelm@12189: wenzelm@12189: val setup = wenzelm@18736: Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #> wenzelm@18736: Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #> wenzelm@26496: Simplifier.map_simpset (fn ss => ss setSolver type_solver); wenzelm@12189: wenzelm@12189: end;