src/ZF/Tools/typechk.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17886 9a4aea3a9ae1
child 18736 541d04c79e12
permissions -rw-r--r--
setup: theory -> theory;
     1 (*  Title:      ZF/Tools/typechk.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Tactics for type checking -- from CTT.
     7 *)
     8 
     9 infix 4 addTCs delTCs;
    10 
    11 signature BASIC_TYPE_CHECK =
    12 sig
    13   type tcset
    14   val addTCs: tcset * thm list -> tcset
    15   val delTCs: tcset * thm list -> tcset
    16   val typecheck_tac: tcset -> tactic
    17   val type_solver_tac: tcset -> thm list -> int -> tactic
    18   val print_tc: tcset -> unit
    19   val print_tcset: theory -> unit
    20   val tcset_ref_of: theory -> tcset ref
    21   val tcset_of: theory -> tcset
    22   val tcset: unit -> tcset
    23   val TCSET: (tcset -> tactic) -> tactic
    24   val TCSET': (tcset -> 'a -> tactic) -> 'a -> tactic
    25   val AddTCs: thm list -> unit
    26   val DelTCs: thm list -> unit
    27   val TC_add_global: theory attribute
    28   val TC_del_global: theory attribute
    29   val TC_add_local: Proof.context attribute
    30   val TC_del_local: Proof.context attribute
    31   val Typecheck_tac: tactic
    32   val Type_solver_tac: thm list -> int -> tactic
    33   val local_tcset_of: Proof.context -> tcset
    34   val type_solver: solver
    35 end;
    36 
    37 signature TYPE_CHECK =
    38 sig
    39   include BASIC_TYPE_CHECK
    40   val setup: theory -> theory
    41 end;
    42 
    43 structure TypeCheck: TYPE_CHECK =
    44 struct
    45 
    46 datatype tcset =
    47     TC of {rules: thm list,     (*the type-checking rules*)
    48            net: thm Net.net};   (*discrimination net of the same rules*)
    49 
    50 
    51 val mem_thm = gen_mem Drule.eq_thm_prop
    52 and rem_thm = gen_rem Drule.eq_thm_prop;
    53 
    54 fun addTC (cs as TC{rules, net}, th) =
    55   if mem_thm (th, rules) then
    56          (warning ("Ignoring duplicate type-checking rule\n" ^
    57                    string_of_thm th);
    58           cs)
    59   else
    60       TC{rules  = th::rules,
    61          net = Net.insert_term (K false) (concl_of th, th) net};
    62 
    63 
    64 fun delTC (cs as TC{rules, net}, th) =
    65   if mem_thm (th, rules) then
    66       TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net,
    67          rules  = rem_thm (rules,th)}
    68   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    69         cs);
    70 
    71 val op addTCs = Library.foldl addTC;
    72 val op delTCs = Library.foldl delTC;
    73 
    74 
    75 (*resolution using a net rather than rules*)
    76 fun net_res_tac maxr net =
    77   SUBGOAL
    78     (fn (prem,i) =>
    79       let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
    80       in
    81          if length rls <= maxr then resolve_tac rls i else no_tac
    82       end);
    83 
    84 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
    85       not (is_Var (head_of a))
    86   | is_rigid_elem _ = false;
    87 
    88 (*Try solving a:A by assumption provided a is rigid!*)
    89 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    90     if is_rigid_elem (Logic.strip_assums_concl prem)
    91     then  assume_tac i  else  eq_assume_tac i);
    92 
    93 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
    94   match_tac is too strict; would refuse to instantiate ?A*)
    95 fun typecheck_step_tac (TC{net,...}) =
    96     FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
    97 
    98 fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
    99 
   100 (*Compiles a term-net for speed*)
   101 val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
   102                                      ballI,allI,conjI,impI];
   103 
   104 (*Instantiates variables in typing conditions.
   105   drawback: does not simplify conjunctions*)
   106 fun type_solver_tac tcset hyps = SELECT_GOAL
   107     (DEPTH_SOLVE (etac FalseE 1
   108                   ORELSE basic_res_tac 1
   109                   ORELSE (ares_tac hyps 1
   110                           APPEND typecheck_step_tac tcset)));
   111 
   112 
   113 
   114 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
   115     TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
   116         net = Net.merge Drule.eq_thm_prop (net, net')};
   117 
   118 (*print tcsets*)
   119 fun print_tc (TC{rules,...}) =
   120     Pretty.writeln
   121        (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
   122 
   123 
   124 (** global tcset **)
   125 
   126 structure TypecheckingArgs =
   127 struct
   128   val name = "ZF/type-checker";
   129   type T = tcset ref;
   130   val empty = ref (TC{rules=[], net=Net.empty});
   131   fun copy (ref tc) = ref tc;
   132   val extend = copy;
   133   fun merge _ (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   134   fun print _ (ref tc) = print_tc tc;
   135 end;
   136 
   137 structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   138 
   139 val print_tcset = TypecheckingData.print;
   140 val tcset_ref_of = TypecheckingData.get;
   141 val tcset_of = ! o tcset_ref_of;
   142 val tcset = tcset_of o Context.the_context;
   143 val tcset_ref = tcset_ref_of o Context.the_context;
   144 
   145 fun TCSET tacf st = tacf (tcset_of (Thm.theory_of_thm st)) st;
   146 fun TCSET' tacf i st = tacf (tcset_of (Thm.theory_of_thm st)) i st;
   147 
   148 
   149 (* change global tcset *)
   150 
   151 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   152 
   153 val AddTCs = change_tcset (op addTCs);
   154 val DelTCs = change_tcset (op delTCs);
   155 
   156 fun Typecheck_tac st = typecheck_tac (tcset()) st;
   157 
   158 fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
   159 
   160 
   161 
   162 (** local tcset **)
   163 
   164 structure LocalTypecheckingData = ProofDataFun
   165 (struct
   166   val name = TypecheckingArgs.name;
   167   type T = tcset;
   168   val init = tcset_of;
   169   fun print _ tcset = print_tc tcset;
   170 end);
   171 
   172 val local_tcset_of = LocalTypecheckingData.get;
   173 
   174 
   175 (* solver *)
   176 
   177 val type_solver = Simplifier.mk_solver' "ZF types" (fn ss =>
   178   type_solver_tac (local_tcset_of (Simplifier.the_context ss)) (Simplifier.prems_of_ss ss));
   179 
   180 
   181 (* attributes *)
   182 
   183 fun global_att f (thy, th) =
   184   let val r = tcset_ref_of thy
   185   in r := f (! r, th); (thy, th) end;
   186 
   187 fun local_att f (ctxt, th) = (LocalTypecheckingData.map (fn tcset => f (tcset, th)) ctxt, th);
   188 
   189 val TC_add_global = global_att addTC;
   190 val TC_del_global = global_att delTC;
   191 val TC_add_local = local_att addTC;
   192 val TC_del_local = local_att delTC;
   193 
   194 val TC_attr =
   195  (Attrib.add_del_args TC_add_global TC_del_global,
   196   Attrib.add_del_args TC_add_local TC_del_local);
   197 
   198 
   199 (* methods *)
   200 
   201 fun TC_args x = Method.only_sectioned_args
   202   [Args.add -- Args.colon >> K (I, TC_add_local),
   203    Args.del -- Args.colon >> K (I, TC_del_local)] x;
   204 
   205 fun typecheck ctxt =
   206   Method.SIMPLE_METHOD (CHANGED (typecheck_tac (local_tcset_of ctxt)));
   207 
   208 
   209 
   210 (** theory setup **)
   211 
   212 val setup =
   213  (TypecheckingData.init #>
   214   LocalTypecheckingData.init #>
   215   (fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy)) #>
   216   Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")] #>
   217   Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]);
   218 
   219 
   220 (** outer syntax **)
   221 
   222 val print_tcsetP =
   223   OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
   224     OuterKeyword.diag
   225     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   226       (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
   227 
   228 val _ = OuterSyntax.add_parsers [print_tcsetP];
   229 
   230 
   231 end;
   232 
   233 structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck;
   234 open BasicTypeCheck;