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