src/ZF/Tools/typechk.ML
author wenzelm
Thu Nov 15 18:15:13 2001 +0100 (2001-11-15)
changeset 12202 af10de5ec7cc
parent 12189 4729bbf86626
child 12311 ce5f9e61c037
permissions -rw-r--r--
added TCSET(') tacticals;
     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 end;
    34 
    35 signature TYPE_CHECK =
    36 sig
    37   include BASIC_TYPE_CHECK
    38   val setup: (theory -> theory) list
    39 end;
    40 
    41 structure TypeCheck: TYPE_CHECK =
    42 struct
    43 
    44 datatype tcset =
    45     TC of {rules: thm list,     (*the type-checking rules*)
    46            net: thm Net.net};   (*discrimination net of the same rules*)
    47 
    48 
    49 val mem_thm = gen_mem eq_thm
    50 and rem_thm = gen_rem eq_thm;
    51 
    52 fun addTC (cs as TC{rules, net}, th) =
    53   if mem_thm (th, rules) then
    54          (warning ("Ignoring duplicate type-checking rule\n" ^
    55                    string_of_thm th);
    56           cs)
    57   else
    58       TC{rules  = th::rules,
    59          net = Net.insert_term ((concl_of th, th), net, K false)};
    60 
    61 
    62 fun delTC (cs as TC{rules, net}, th) =
    63   if mem_thm (th, rules) then
    64       TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
    65          rules  = rem_thm (rules,th)}
    66   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    67         cs);
    68 
    69 val op addTCs = foldl addTC;
    70 val op delTCs = foldl delTC;
    71 
    72 
    73 (*resolution using a net rather than rules*)
    74 fun net_res_tac maxr net =
    75   SUBGOAL
    76     (fn (prem,i) =>
    77       let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
    78       in
    79          if length rls <= maxr then resolve_tac rls i else no_tac
    80       end);
    81 
    82 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
    83       not (is_Var (head_of a))
    84   | is_rigid_elem _ = false;
    85 
    86 (*Try solving a:A by assumption provided a is rigid!*)
    87 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    88     if is_rigid_elem (Logic.strip_assums_concl prem)
    89     then  assume_tac i  else  eq_assume_tac i);
    90 
    91 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
    92   match_tac is too strict; would refuse to instantiate ?A*)
    93 fun typecheck_step_tac (TC{net,...}) =
    94     FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
    95 
    96 fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
    97 
    98 (*Compiles a term-net for speed*)
    99 val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
   100                                      ballI,allI,conjI,impI];
   101 
   102 (*Instantiates variables in typing conditions.
   103   drawback: does not simplify conjunctions*)
   104 fun type_solver_tac tcset hyps = SELECT_GOAL
   105     (DEPTH_SOLVE (etac FalseE 1
   106                   ORELSE basic_res_tac 1
   107                   ORELSE (ares_tac hyps 1
   108                           APPEND typecheck_step_tac tcset)));
   109 
   110 
   111 
   112 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
   113     TC {rules = gen_union eq_thm (rules,rules'),
   114         net = Net.merge (net, net', eq_thm)};
   115 
   116 (*print tcsets*)
   117 fun print_tc (TC{rules,...}) =
   118     Pretty.writeln
   119        (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
   120 
   121 
   122 (** global tcset **)
   123 
   124 structure TypecheckingArgs =
   125   struct
   126   val name = "ZF/type-checker";
   127   type T = tcset ref;
   128   val empty = ref (TC{rules=[], net=Net.empty});
   129   fun copy (ref tc) = ref tc;
   130   val finish = I;
   131   val prep_ext = copy;
   132   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   133   fun print _ (ref tc) = print_tc tc;
   134   end;
   135 
   136 structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   137 
   138 val print_tcset = TypecheckingData.print;
   139 val tcset_ref_of_sg = TypecheckingData.get_sg;
   140 val tcset_ref_of = TypecheckingData.get;
   141 
   142 
   143 (* access global tcset *)
   144 
   145 val tcset_of_sg = ! o tcset_ref_of_sg;
   146 val tcset_of = tcset_of_sg o sign_of;
   147 
   148 val tcset = tcset_of o Context.the_context;
   149 val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   150 
   151 fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
   152 fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
   153 
   154 
   155 (* change global tcset *)
   156 
   157 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   158 
   159 val AddTCs = change_tcset (op addTCs);
   160 val DelTCs = change_tcset (op delTCs);
   161 
   162 fun Typecheck_tac st = typecheck_tac (tcset()) st;
   163 
   164 fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
   165 
   166 
   167 
   168 (** local tcset **)
   169 
   170 structure LocalTypecheckingArgs =
   171 struct
   172   val name = TypecheckingArgs.name;
   173   type T = tcset;
   174   val init = tcset_of;
   175   fun print _ tcset = print_tc tcset;
   176 end;
   177 
   178 structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
   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 (LocalTypecheckingData.get ctxt)));
   207 
   208 
   209 
   210 (** theory setup **)
   211 
   212 val setup =
   213  [TypecheckingData.init, LocalTypecheckingData.init,
   214   Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
   215   Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
   216 
   217 
   218 (** outer syntax **)
   219 
   220 val print_tcsetP =
   221   OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
   222     OuterSyntax.Keyword.diag
   223     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   224       (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
   225 
   226 val _ = OuterSyntax.add_parsers [print_tcsetP];
   227 
   228 
   229 end;
   230 
   231 structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck;
   232 open BasicTypeCheck;