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