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