src/ZF/Tools/typechk.ML
author wenzelm
Sat Jan 21 23:02:29 2006 +0100 (2006-01-21)
changeset 18736 541d04c79e12
parent 18708 4b3dadb4fe33
child 20193 46f5ef758422
permissions -rw-r--r--
simplified type attribute;
removed obsolete tcset operations -- clean data/attribute/method setup;
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@18736
     6
Automated type checking (cf. CTT).
paulson@6049
     7
*)
paulson@6049
     8
wenzelm@12189
     9
signature TYPE_CHECK =
wenzelm@12189
    10
sig
wenzelm@18736
    11
  val print_tcset: Context.generic -> unit
wenzelm@18736
    12
  val TC_add: attribute
wenzelm@18736
    13
  val TC_del: attribute
wenzelm@18736
    14
  val typecheck_tac: Proof.context -> tactic
wenzelm@18736
    15
  val type_solver_tac: Proof.context -> thm list -> int -> tactic
wenzelm@18736
    16
  val type_solver: solver
wenzelm@18708
    17
  val setup: theory -> theory
wenzelm@12189
    18
end;
wenzelm@12189
    19
wenzelm@12189
    20
structure TypeCheck: TYPE_CHECK =
paulson@6153
    21
struct
wenzelm@12189
    22
wenzelm@18736
    23
(* datatype tcset *)
wenzelm@18736
    24
wenzelm@18736
    25
datatype tcset = TC of
wenzelm@18736
    26
 {rules: thm list,     (*the type-checking rules*)
wenzelm@18736
    27
  net: thm Net.net};   (*discrimination net of the same rules*)
wenzelm@18736
    28
wenzelm@18736
    29
fun add_rule th (tcs as TC {rules, net}) =
wenzelm@18736
    30
  if member Drule.eq_thm_prop rules th then
wenzelm@18736
    31
    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
wenzelm@18736
    32
  else
wenzelm@18736
    33
    TC {rules = th :: rules,
wenzelm@18736
    34
        net = Net.insert_term (K false) (Thm.concl_of th, th) net};
wenzelm@18736
    35
wenzelm@18736
    36
fun del_rule th (tcs as TC {rules, net}) =
wenzelm@18736
    37
  if member Drule.eq_thm_prop rules th then
wenzelm@18736
    38
    TC {net = Net.delete_term Drule.eq_thm_prop (Thm.concl_of th, th) net,
wenzelm@18736
    39
        rules = remove Drule.eq_thm_prop th rules}
wenzelm@18736
    40
  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
paulson@6153
    41
paulson@6153
    42
wenzelm@18736
    43
(* generic data *)
wenzelm@18736
    44
wenzelm@18736
    45
structure Data = GenericDataFun
wenzelm@18736
    46
(
wenzelm@18736
    47
  val name = "ZF/type-checking";
wenzelm@18736
    48
  type T = tcset
wenzelm@18736
    49
  val empty = TC {rules = [], net = Net.empty};
wenzelm@18736
    50
  val extend = I;
paulson@6153
    51
wenzelm@18736
    52
  fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
wenzelm@18736
    53
    TC {rules = gen_union Drule.eq_thm_prop (rules, rules'),
wenzelm@18736
    54
        net = Net.merge Drule.eq_thm_prop (net, net')};
wenzelm@18736
    55
wenzelm@18736
    56
  fun print context (TC {rules, ...}) =
wenzelm@18736
    57
    Pretty.writeln (Pretty.big_list "type-checking rules:"
wenzelm@18736
    58
      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
wenzelm@18736
    59
);
wenzelm@18736
    60
wenzelm@18736
    61
val print_tcset = Data.print;
wenzelm@18736
    62
wenzelm@18736
    63
val TC_add = Thm.declaration_attribute (Data.map o add_rule);
wenzelm@18736
    64
val TC_del = Thm.declaration_attribute (Data.map o del_rule);
wenzelm@18736
    65
wenzelm@18736
    66
val tcset_of = Data.get o Context.Proof;
paulson@6153
    67
paulson@6153
    68
wenzelm@18736
    69
(* tactics *)
paulson@6153
    70
paulson@6153
    71
(*resolution using a net rather than rules*)
paulson@6153
    72
fun net_res_tac maxr net =
paulson@6153
    73
  SUBGOAL
paulson@6153
    74
    (fn (prem,i) =>
paulson@6153
    75
      let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
wenzelm@12189
    76
      in
wenzelm@12189
    77
         if length rls <= maxr then resolve_tac rls i else no_tac
paulson@6153
    78
      end);
paulson@6153
    79
wenzelm@12189
    80
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
paulson@6049
    81
      not (is_Var (head_of a))
paulson@6049
    82
  | is_rigid_elem _ = false;
paulson@6049
    83
wenzelm@12189
    84
(*Try solving a:A by assumption provided a is rigid!*)
paulson@6049
    85
val test_assume_tac = SUBGOAL(fn (prem,i) =>
paulson@6049
    86
    if is_rigid_elem (Logic.strip_assums_concl prem)
paulson@6049
    87
    then  assume_tac i  else  eq_assume_tac i);
paulson@6049
    88
wenzelm@12189
    89
(*Type checking solves a:?A (a rigid, ?A maybe flexible).
paulson@6049
    90
  match_tac is too strict; would refuse to instantiate ?A*)
paulson@6153
    91
fun typecheck_step_tac (TC{net,...}) =
paulson@6153
    92
    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
paulson@6049
    93
wenzelm@18736
    94
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
paulson@6049
    95
paulson@6153
    96
(*Compiles a term-net for speed*)
paulson@6153
    97
val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
wenzelm@12189
    98
                                     ballI,allI,conjI,impI];
paulson@6049
    99
paulson@6049
   100
(*Instantiates variables in typing conditions.
paulson@6049
   101
  drawback: does not simplify conjunctions*)
wenzelm@18736
   102
fun type_solver_tac ctxt hyps = SELECT_GOAL
paulson@6153
   103
    (DEPTH_SOLVE (etac FalseE 1
wenzelm@12189
   104
                  ORELSE basic_res_tac 1
wenzelm@12189
   105
                  ORELSE (ares_tac hyps 1
wenzelm@18736
   106
                          APPEND typecheck_step_tac (tcset_of ctxt))));
wenzelm@12189
   107
wenzelm@18736
   108
val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss =>
wenzelm@18736
   109
  type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss));
paulson@6153
   110
paulson@6153
   111
wenzelm@18736
   112
(* concrete syntax *)
wenzelm@12189
   113
wenzelm@18736
   114
val TC_att = Attrib.add_del_args TC_add TC_del;
wenzelm@12189
   115
wenzelm@18736
   116
val typecheck_meth =
wenzelm@18736
   117
  Method.only_sectioned_args
wenzelm@18736
   118
    [Args.add -- Args.colon >> K (I, TC_add),
wenzelm@18736
   119
     Args.del -- Args.colon >> K (I, TC_del)]
wenzelm@18736
   120
  (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
wenzelm@12189
   121
wenzelm@18736
   122
val _ = OuterSyntax.add_parsers
wenzelm@18736
   123
  [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
wenzelm@18736
   124
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
wenzelm@18736
   125
      Toplevel.keep (print_tcset o Toplevel.context_of)))];
wenzelm@12189
   126
wenzelm@12189
   127
wenzelm@18736
   128
(* theory setup *)
wenzelm@12189
   129
wenzelm@12189
   130
val setup =
wenzelm@18736
   131
  Data.init #>
wenzelm@18736
   132
  Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
wenzelm@18736
   133
  Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
wenzelm@18736
   134
  (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));
wenzelm@12189
   135
wenzelm@12189
   136
end;