src/ZF/Tools/typechk.ML
author wenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 58838 59203adfc33f
parent 58828 6d076fdd933d
child 58893 9e0ecb66d6a7
permissions -rw-r--r--
eliminated aliases;
wenzelm@12189
     1
(*  Title:      ZF/Tools/typechk.ML
paulson@6049
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6153
     3
    Copyright   1999  University of Cambridge
paulson@6049
     4
wenzelm@18736
     5
Automated type checking (cf. CTT).
paulson@6049
     6
*)
paulson@6049
     7
wenzelm@12189
     8
signature TYPE_CHECK =
wenzelm@12189
     9
sig
wenzelm@21506
    10
  val print_tcset: Proof.context -> unit
wenzelm@18736
    11
  val TC_add: attribute
wenzelm@18736
    12
  val TC_del: attribute
wenzelm@18736
    13
  val typecheck_tac: Proof.context -> tactic
wenzelm@18736
    14
  val type_solver_tac: Proof.context -> thm list -> int -> tactic
wenzelm@18736
    15
  val type_solver: solver
wenzelm@12189
    16
end;
wenzelm@12189
    17
wenzelm@12189
    18
structure TypeCheck: TYPE_CHECK =
paulson@6153
    19
struct
wenzelm@12189
    20
wenzelm@18736
    21
(* datatype tcset *)
wenzelm@18736
    22
wenzelm@18736
    23
datatype tcset = TC of
wenzelm@18736
    24
 {rules: thm list,     (*the type-checking rules*)
wenzelm@18736
    25
  net: thm Net.net};   (*discrimination net of the same rules*)
wenzelm@18736
    26
wenzelm@42439
    27
fun add_rule ctxt th (tcs as TC {rules, net}) =
wenzelm@22360
    28
  if member Thm.eq_thm_prop rules th then
wenzelm@42439
    29
    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
wenzelm@18736
    30
  else
wenzelm@42439
    31
    TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
wenzelm@18736
    32
wenzelm@42439
    33
fun del_rule ctxt th (tcs as TC {rules, net}) =
wenzelm@22360
    34
  if member Thm.eq_thm_prop rules th then
wenzelm@22360
    35
    TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
wenzelm@42439
    36
      rules = remove Thm.eq_thm_prop th rules}
wenzelm@42439
    37
  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
paulson@6153
    38
paulson@6153
    39
wenzelm@18736
    40
(* generic data *)
wenzelm@18736
    41
wenzelm@33519
    42
structure Data = Generic_Data
wenzelm@18736
    43
(
wenzelm@33519
    44
  type T = tcset;
wenzelm@18736
    45
  val empty = TC {rules = [], net = Net.empty};
wenzelm@18736
    46
  val extend = I;
wenzelm@33519
    47
  fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
wenzelm@33519
    48
    TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
wenzelm@18736
    49
);
wenzelm@18736
    50
wenzelm@42439
    51
val TC_add =
wenzelm@42439
    52
  Thm.declaration_attribute (fn thm => fn context =>
wenzelm@42439
    53
    Data.map (add_rule (Context.proof_of context) thm) context);
wenzelm@42439
    54
wenzelm@42439
    55
val TC_del =
wenzelm@42439
    56
  Thm.declaration_attribute (fn thm => fn context =>
wenzelm@42439
    57
    Data.map (del_rule (Context.proof_of context) thm) context);
wenzelm@18736
    58
wenzelm@18736
    59
val tcset_of = Data.get o Context.Proof;
paulson@6153
    60
wenzelm@22846
    61
fun print_tcset ctxt =
wenzelm@22846
    62
  let val TC {rules, ...} = tcset_of ctxt in
wenzelm@22846
    63
    Pretty.writeln (Pretty.big_list "type-checking rules:"
wenzelm@51584
    64
      (map (Display.pretty_thm_item ctxt) rules))
wenzelm@22846
    65
  end;
wenzelm@22846
    66
paulson@6153
    67
wenzelm@18736
    68
(* tactics *)
paulson@6153
    69
paulson@6153
    70
(*resolution using a net rather than rules*)
paulson@6153
    71
fun net_res_tac maxr net =
paulson@6153
    72
  SUBGOAL
paulson@6153
    73
    (fn (prem,i) =>
paulson@6153
    74
      let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
wenzelm@12189
    75
      in
wenzelm@12189
    76
         if length rls <= maxr then resolve_tac rls i else no_tac
paulson@6153
    77
      end);
paulson@6153
    78
haftmann@38522
    79
fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
paulson@6049
    80
      not (is_Var (head_of a))
paulson@6049
    81
  | is_rigid_elem _ = false;
paulson@6049
    82
wenzelm@12189
    83
(*Try solving a:A by assumption provided a is rigid!*)
paulson@6049
    84
val test_assume_tac = SUBGOAL(fn (prem,i) =>
paulson@6049
    85
    if is_rigid_elem (Logic.strip_assums_concl prem)
paulson@6049
    86
    then  assume_tac i  else  eq_assume_tac i);
paulson@6049
    87
wenzelm@12189
    88
(*Type checking solves a:?A (a rigid, ?A maybe flexible).
paulson@6049
    89
  match_tac is too strict; would refuse to instantiate ?A*)
paulson@6153
    90
fun typecheck_step_tac (TC{net,...}) =
paulson@6153
    91
    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
paulson@6049
    92
wenzelm@18736
    93
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
paulson@6049
    94
paulson@6153
    95
(*Compiles a term-net for speed*)
wenzelm@26287
    96
val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
wenzelm@26287
    97
                                     @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
paulson@6049
    98
paulson@6049
    99
(*Instantiates variables in typing conditions.
paulson@6049
   100
  drawback: does not simplify conjunctions*)
wenzelm@18736
   101
fun type_solver_tac ctxt hyps = SELECT_GOAL
wenzelm@58838
   102
    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
wenzelm@12189
   103
                  ORELSE basic_res_tac 1
wenzelm@12189
   104
                  ORELSE (ares_tac hyps 1
wenzelm@18736
   105
                          APPEND typecheck_step_tac (tcset_of ctxt))));
wenzelm@12189
   106
wenzelm@43596
   107
val type_solver =
wenzelm@51717
   108
  Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
wenzelm@51717
   109
    type_solver_tac ctxt (Simplifier.prems_of ctxt));
paulson@6153
   110
wenzelm@58828
   111
val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver));
wenzelm@58828
   112
paulson@6153
   113
wenzelm@18736
   114
(* concrete syntax *)
wenzelm@12189
   115
wenzelm@58828
   116
val _ =
wenzelm@58828
   117
  Theory.setup
wenzelm@58828
   118
   (Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del)
wenzelm@58828
   119
      "declaration of type-checking rule" #>
wenzelm@58828
   120
    Method.setup @{binding typecheck}
wenzelm@58828
   121
      (Method.sections
wenzelm@58828
   122
        [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
wenzelm@58828
   123
         Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
wenzelm@58828
   124
        >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
wenzelm@58828
   125
      "ZF type-checking");
wenzelm@12189
   126
wenzelm@24867
   127
val _ =
wenzelm@46961
   128
  Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
wenzelm@51658
   129
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@24867
   130
      Toplevel.keep (print_tcset o Toplevel.context_of)));
wenzelm@12189
   131
wenzelm@12189
   132
end;