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