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@12189: Tactics for type checking -- from CTT.
paulson@6049: *)
paulson@6049: 
paulson@6153: infix 4 addTCs delTCs;
paulson@6153: 
wenzelm@12189: signature BASIC_TYPE_CHECK =
wenzelm@12189: sig
wenzelm@12189:   type tcset
wenzelm@12189:   val addTCs: tcset * thm list -> tcset
wenzelm@12189:   val delTCs: tcset * thm list -> tcset
wenzelm@12189:   val typecheck_tac: tcset -> tactic
wenzelm@12189:   val type_solver_tac: tcset -> thm list -> int -> tactic
wenzelm@12189:   val print_tc: tcset -> unit
wenzelm@12189:   val print_tcset: theory -> unit
wenzelm@12189:   val tcset_ref_of: theory -> tcset ref
wenzelm@12189:   val tcset_of: theory -> tcset
wenzelm@12189:   val tcset: unit -> tcset
wenzelm@12202:   val TCSET: (tcset -> tactic) -> tactic
wenzelm@12202:   val TCSET': (tcset -> 'a -> tactic) -> 'a -> tactic
wenzelm@12189:   val AddTCs: thm list -> unit
wenzelm@12189:   val DelTCs: thm list -> unit
wenzelm@12189:   val TC_add_global: theory attribute
wenzelm@12189:   val TC_del_global: theory attribute
wenzelm@12189:   val TC_add_local: Proof.context attribute
wenzelm@12189:   val TC_del_local: Proof.context attribute
wenzelm@12189:   val Typecheck_tac: tactic
wenzelm@12189:   val Type_solver_tac: thm list -> int -> tactic
wenzelm@15090:   val local_tcset_of: Proof.context -> tcset
wenzelm@15090:   val context_type_solver: context_solver
wenzelm@12189: end;
wenzelm@12189: 
wenzelm@12189: signature TYPE_CHECK =
wenzelm@12189: sig
wenzelm@12189:   include BASIC_TYPE_CHECK
wenzelm@12189:   val setup: (theory -> theory) list
wenzelm@12189: end;
wenzelm@12189: 
wenzelm@12189: structure TypeCheck: TYPE_CHECK =
paulson@6153: struct
wenzelm@12189: 
paulson@6153: datatype tcset =
wenzelm@12189:     TC of {rules: thm list,     (*the type-checking rules*)
wenzelm@12189:            net: thm Net.net};   (*discrimination net of the same rules*)
paulson@6153: 
paulson@6153: 
wenzelm@13105: val mem_thm = gen_mem Drule.eq_thm_prop
wenzelm@13105: and rem_thm = gen_rem Drule.eq_thm_prop;
paulson@6153: 
paulson@6153: fun addTC (cs as TC{rules, net}, th) =
wenzelm@12189:   if mem_thm (th, rules) then
wenzelm@12189:          (warning ("Ignoring duplicate type-checking rule\n" ^
wenzelm@12189:                    string_of_thm th);
wenzelm@12189:           cs)
paulson@6153:   else
wenzelm@12189:       TC{rules  = th::rules,
wenzelm@12189:          net = Net.insert_term ((concl_of th, th), net, K false)};
paulson@6153: 
paulson@6153: 
paulson@6153: fun delTC (cs as TC{rules, net}, th) =
paulson@6153:   if mem_thm (th, rules) then
wenzelm@13105:       TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
wenzelm@12189:          rules  = rem_thm (rules,th)}
wenzelm@12189:   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
wenzelm@12189:         cs);
paulson@6153: 
skalberg@15570: val op addTCs = Library.foldl addTC;
skalberg@15570: val op delTCs = Library.foldl delTC;
paulson@6153: 
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@12189: fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ 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: 
paulson@6153: fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
paulson@6049: 
paulson@6153: (*Compiles a term-net for speed*)
paulson@6153: val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
wenzelm@12189:                                      ballI,allI,conjI,impI];
paulson@6049: 
paulson@6049: (*Instantiates variables in typing conditions.
paulson@6049:   drawback: does not simplify conjunctions*)
paulson@6153: fun type_solver_tac tcset 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@12189:                           APPEND typecheck_step_tac tcset)));
paulson@6153: 
paulson@6153: 
paulson@6153: 
paulson@6153: fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
wenzelm@13105:     TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
wenzelm@13105:         net = Net.merge (net, net', Drule.eq_thm_prop)};
paulson@6153: 
paulson@6153: (*print tcsets*)
paulson@6153: fun print_tc (TC{rules,...}) =
paulson@6153:     Pretty.writeln
paulson@6153:        (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
paulson@6153: 
paulson@6153: 
wenzelm@12189: (** global tcset **)
wenzelm@12189: 
paulson@6153: structure TypecheckingArgs =
paulson@6153:   struct
paulson@6153:   val name = "ZF/type-checker";
paulson@6153:   type T = tcset ref;
paulson@6153:   val empty = ref (TC{rules=[], net=Net.empty});
wenzelm@6556:   fun copy (ref tc) = ref tc;
wenzelm@6556:   val prep_ext = copy;
paulson@6153:   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
paulson@6153:   fun print _ (ref tc) = print_tc tc;
paulson@6153:   end;
paulson@6153: 
paulson@6153: structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
paulson@6049: 
paulson@6153: val print_tcset = TypecheckingData.print;
paulson@6153: val tcset_ref_of_sg = TypecheckingData.get_sg;
paulson@6153: val tcset_ref_of = TypecheckingData.get;
paulson@6153: 
wenzelm@12189: 
paulson@6153: (* access global tcset *)
paulson@6153: 
paulson@6153: val tcset_of_sg = ! o tcset_ref_of_sg;
paulson@6153: val tcset_of = tcset_of_sg o sign_of;
paulson@6153: 
paulson@6153: val tcset = tcset_of o Context.the_context;
paulson@6153: val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
paulson@6153: 
wenzelm@12202: fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
wenzelm@12202: fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
wenzelm@12202: 
wenzelm@12189: 
paulson@6153: (* change global tcset *)
paulson@6153: 
paulson@6153: fun change_tcset f x = tcset_ref () := (f (tcset (), x));
paulson@6153: 
paulson@6153: val AddTCs = change_tcset (op addTCs);
paulson@6153: val DelTCs = change_tcset (op delTCs);
paulson@6153: 
paulson@6153: fun Typecheck_tac st = typecheck_tac (tcset()) st;
paulson@6153: 
paulson@6153: fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
paulson@6153: 
paulson@6153: 
paulson@6153: 
wenzelm@12189: (** local tcset **)
wenzelm@12189: 
wenzelm@12189: structure LocalTypecheckingArgs =
wenzelm@12189: struct
wenzelm@12189:   val name = TypecheckingArgs.name;
wenzelm@12189:   type T = tcset;
wenzelm@12189:   val init = tcset_of;
wenzelm@12189:   fun print _ tcset = print_tc tcset;
wenzelm@12189: end;
wenzelm@12189: 
wenzelm@12189: structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
wenzelm@15090: val local_tcset_of = LocalTypecheckingData.get;
wenzelm@15090: 
wenzelm@15090: 
wenzelm@15090: (* solver *)
wenzelm@15090: 
wenzelm@15090: val context_type_solver =
wenzelm@15090:   Simplifier.mk_context_solver "context types" (type_solver_tac o local_tcset_of);
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: (* attributes *)
wenzelm@12189: 
wenzelm@12189: fun global_att f (thy, th) =
wenzelm@12189:   let val r = tcset_ref_of thy
wenzelm@12189:   in r := f (! r, th); (thy, th) end;
wenzelm@12189: 
wenzelm@12189: fun local_att f (ctxt, th) = (LocalTypecheckingData.map (fn tcset => f (tcset, th)) ctxt, th);
wenzelm@12189: 
wenzelm@12189: val TC_add_global = global_att addTC;
wenzelm@12189: val TC_del_global = global_att delTC;
wenzelm@12189: val TC_add_local = local_att addTC;
wenzelm@12189: val TC_del_local = local_att delTC;
wenzelm@12189: 
wenzelm@12189: val TC_attr =
wenzelm@12189:  (Attrib.add_del_args TC_add_global TC_del_global,
wenzelm@12189:   Attrib.add_del_args TC_add_local TC_del_local);
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: (* methods *)
wenzelm@12189: 
wenzelm@12189: fun TC_args x = Method.only_sectioned_args
wenzelm@12189:   [Args.add -- Args.colon >> K (I, TC_add_local),
wenzelm@12189:    Args.del -- Args.colon >> K (I, TC_del_local)] x;
wenzelm@12189: 
wenzelm@12189: fun typecheck ctxt =
wenzelm@15090:   Method.SIMPLE_METHOD (CHANGED (typecheck_tac (local_tcset_of ctxt)));
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: (** theory setup **)
wenzelm@12189: 
wenzelm@12189: val setup =
wenzelm@12189:  [TypecheckingData.init, LocalTypecheckingData.init,
wenzelm@15090:   Simplifier.add_context_unsafe_solver context_type_solver,
wenzelm@12189:   Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
wenzelm@12189:   Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: (** outer syntax **)
wenzelm@12189: 
wenzelm@12189: val print_tcsetP =
wenzelm@12189:   OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
wenzelm@12189:     OuterSyntax.Keyword.diag
wenzelm@12189:     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
wenzelm@12189:       (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
wenzelm@12189: 
wenzelm@12189: val _ = OuterSyntax.add_parsers [print_tcsetP];
wenzelm@12189: 
wenzelm@12189: 
wenzelm@12189: end;
wenzelm@12189: 
wenzelm@12189: structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck;
wenzelm@12189: open BasicTypeCheck;