src/ZF/Tools/typechk.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 15090 970c2668c694
child 16458 4c6fd0c01d28
permissions -rw-r--r--
Move towards standard functions.
     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 context_type_solver: context_solver
    35 end;
    36 
    37 signature TYPE_CHECK =
    38 sig
    39   include BASIC_TYPE_CHECK
    40   val setup: (theory -> theory) list
    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 ((concl_of th, th), net, K false)};
    62 
    63 
    64 fun delTC (cs as TC{rules, net}, th) =
    65   if mem_thm (th, rules) then
    66       TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
    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 (net, net', Drule.eq_thm_prop)};
   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 prep_ext = 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_sg = TypecheckingData.get_sg;
   141 val tcset_ref_of = TypecheckingData.get;
   142 
   143 
   144 (* access global tcset *)
   145 
   146 val tcset_of_sg = ! o tcset_ref_of_sg;
   147 val tcset_of = tcset_of_sg o sign_of;
   148 
   149 val tcset = tcset_of o Context.the_context;
   150 val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   151 
   152 fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
   153 fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
   154 
   155 
   156 (* change global tcset *)
   157 
   158 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   159 
   160 val AddTCs = change_tcset (op addTCs);
   161 val DelTCs = change_tcset (op delTCs);
   162 
   163 fun Typecheck_tac st = typecheck_tac (tcset()) st;
   164 
   165 fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
   166 
   167 
   168 
   169 (** local tcset **)
   170 
   171 structure LocalTypecheckingArgs =
   172 struct
   173   val name = TypecheckingArgs.name;
   174   type T = tcset;
   175   val init = tcset_of;
   176   fun print _ tcset = print_tc tcset;
   177 end;
   178 
   179 structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
   180 val local_tcset_of = LocalTypecheckingData.get;
   181 
   182 
   183 (* solver *)
   184 
   185 val context_type_solver =
   186   Simplifier.mk_context_solver "context types" (type_solver_tac o local_tcset_of);
   187 
   188 
   189 (* attributes *)
   190 
   191 fun global_att f (thy, th) =
   192   let val r = tcset_ref_of thy
   193   in r := f (! r, th); (thy, th) end;
   194 
   195 fun local_att f (ctxt, th) = (LocalTypecheckingData.map (fn tcset => f (tcset, th)) ctxt, th);
   196 
   197 val TC_add_global = global_att addTC;
   198 val TC_del_global = global_att delTC;
   199 val TC_add_local = local_att addTC;
   200 val TC_del_local = local_att delTC;
   201 
   202 val TC_attr =
   203  (Attrib.add_del_args TC_add_global TC_del_global,
   204   Attrib.add_del_args TC_add_local TC_del_local);
   205 
   206 
   207 (* methods *)
   208 
   209 fun TC_args x = Method.only_sectioned_args
   210   [Args.add -- Args.colon >> K (I, TC_add_local),
   211    Args.del -- Args.colon >> K (I, TC_del_local)] x;
   212 
   213 fun typecheck ctxt =
   214   Method.SIMPLE_METHOD (CHANGED (typecheck_tac (local_tcset_of ctxt)));
   215 
   216 
   217 
   218 (** theory setup **)
   219 
   220 val setup =
   221  [TypecheckingData.init, LocalTypecheckingData.init,
   222   Simplifier.add_context_unsafe_solver context_type_solver,
   223   Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
   224   Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
   225 
   226 
   227 (** outer syntax **)
   228 
   229 val print_tcsetP =
   230   OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
   231     OuterSyntax.Keyword.diag
   232     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   233       (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
   234 
   235 val _ = OuterSyntax.add_parsers [print_tcsetP];
   236 
   237 
   238 end;
   239 
   240 structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck;
   241 open BasicTypeCheck;