src/ZF/Tools/typechk.ML
author wenzelm
Sun Jul 29 14:29:54 2007 +0200 (2007-07-29)
changeset 24039 273698405054
parent 22846 fb79144af9a3
child 24826 78e6a3cea367
permissions -rw-r--r--
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
     1 (*  Title:      ZF/Tools/typechk.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Automated type checking (cf. CTT).
     7 *)
     8 
     9 signature TYPE_CHECK =
    10 sig
    11   val print_tcset: Proof.context -> unit
    12   val TC_add: attribute
    13   val TC_del: attribute
    14   val typecheck_tac: Proof.context -> tactic
    15   val type_solver_tac: Proof.context -> thm list -> int -> tactic
    16   val type_solver: solver
    17   val setup: theory -> theory
    18 end;
    19 
    20 structure TypeCheck: TYPE_CHECK =
    21 struct
    22 
    23 (* datatype tcset *)
    24 
    25 datatype tcset = TC of
    26  {rules: thm list,     (*the type-checking rules*)
    27   net: thm Net.net};   (*discrimination net of the same rules*)
    28 
    29 fun add_rule th (tcs as TC {rules, net}) =
    30   if member Thm.eq_thm_prop rules th then
    31     (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm 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" ^ Display.string_of_thm th); tcs);
    41 
    42 
    43 (* generic data *)
    44 
    45 structure Data = GenericDataFun
    46 (
    47   type T = tcset
    48   val empty = TC {rules = [], net = Net.empty};
    49   val extend = I;
    50 
    51   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
    52     TC {rules = Thm.merge_thms (rules, rules'),
    53         net = Net.merge Thm.eq_thm_prop (net, net')};
    54 );
    55 
    56 val TC_add = Thm.declaration_attribute (Data.map o add_rule);
    57 val TC_del = Thm.declaration_attribute (Data.map o del_rule);
    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 (ProofContext.pretty_thm 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("Trueprop",_) $ (Const("op :",_) $ 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 [TrueI,refl,reflexive_thm,iff_refl,
    97                                      ballI,allI,conjI,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 (etac 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 = Simplifier.mk_solver' "ZF typecheck" (fn ss =>
   108   type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss));
   109 
   110 
   111 (* concrete syntax *)
   112 
   113 val TC_att = Attrib.add_del_args TC_add TC_del;
   114 
   115 val typecheck_meth =
   116   Method.only_sectioned_args
   117     [Args.add -- Args.colon >> K (I, TC_add),
   118      Args.del -- Args.colon >> K (I, TC_del)]
   119   (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
   120 
   121 val _ = OuterSyntax.add_parsers
   122   [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
   123     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   124       Toplevel.keep (print_tcset o Toplevel.context_of)))];
   125 
   126 
   127 (* theory setup *)
   128 
   129 val setup =
   130   Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
   131   Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
   132   (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));
   133 
   134 end;