src/ZF/Tools/typechk.ML
author wenzelm
Fri Apr 30 18:10:03 1999 +0200 (1999-04-30)
changeset 6556 daa00919502b
parent 6153 bff90585cce5
child 12109 bd6eb9194a5d
permissions -rw-r--r--
theory data: copy;
     1 (*  Title:      ZF/typechk
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Tactics for type checking -- from CTT
     7 *)
     8 
     9 infix 4 addTCs delTCs;
    10 
    11 structure TypeCheck =
    12 struct
    13 datatype tcset =
    14     TC of {rules: thm list,	(*the type-checking rules*)
    15 	   net: thm Net.net};   (*discrimination net of the same rules*)     
    16 
    17 
    18 
    19 val mem_thm = gen_mem eq_thm
    20 and rem_thm = gen_rem eq_thm;
    21 
    22 fun addTC (cs as TC{rules, net}, th) =
    23   if mem_thm (th, rules) then 
    24 	 (warning ("Ignoring duplicate type-checking rule\n" ^ 
    25 		   string_of_thm th);
    26 	  cs)
    27   else
    28       TC{rules	= th::rules,
    29 	 net = Net.insert_term ((concl_of th, th), net, K false)};
    30 
    31 
    32 fun delTC (cs as TC{rules, net}, th) =
    33   if mem_thm (th, rules) then
    34       TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
    35 	 rules	= rem_thm (rules,th)}
    36   else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); 
    37 	cs);
    38 
    39 val op addTCs = foldl addTC;
    40 val op delTCs = foldl delTC;
    41 
    42 
    43 (*resolution using a net rather than rules*)
    44 fun net_res_tac maxr net =
    45   SUBGOAL
    46     (fn (prem,i) =>
    47       let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
    48       in 
    49 	 if length rls <= maxr then resolve_tac rls i else no_tac
    50       end);
    51 
    52 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
    53       not (is_Var (head_of a))
    54   | is_rigid_elem _ = false;
    55 
    56 (*Try solving a:A by assumption provided a is rigid!*) 
    57 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    58     if is_rigid_elem (Logic.strip_assums_concl prem)
    59     then  assume_tac i  else  eq_assume_tac i);
    60 
    61 (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
    62   match_tac is too strict; would refuse to instantiate ?A*)
    63 fun typecheck_step_tac (TC{net,...}) =
    64     FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
    65 
    66 fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
    67 
    68 (*Compiles a term-net for speed*)
    69 val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
    70 				     ballI,allI,conjI,impI];
    71 
    72 (*Instantiates variables in typing conditions.
    73   drawback: does not simplify conjunctions*)
    74 fun type_solver_tac tcset hyps = SELECT_GOAL
    75     (DEPTH_SOLVE (etac FalseE 1
    76 		  ORELSE basic_res_tac 1
    77 		  ORELSE (ares_tac hyps 1
    78 			  APPEND typecheck_step_tac tcset)));
    79 
    80 
    81 
    82 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
    83     TC {rules = gen_union eq_thm (rules,rules'),
    84 	net = Net.merge (net, net', eq_thm)};
    85 
    86 (*print tcsets*)
    87 fun print_tc (TC{rules,...}) =
    88     Pretty.writeln
    89        (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
    90 
    91 
    92 structure TypecheckingArgs =
    93   struct
    94   val name = "ZF/type-checker";
    95   type T = tcset ref;
    96   val empty = ref (TC{rules=[], net=Net.empty});
    97   fun copy (ref tc) = ref tc;
    98   val prep_ext = copy;
    99   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   100   fun print _ (ref tc) = print_tc tc;
   101   end;
   102 
   103 structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   104 
   105 val setup = [TypecheckingData.init];
   106 
   107 val print_tcset = TypecheckingData.print;
   108 val tcset_ref_of_sg = TypecheckingData.get_sg;
   109 val tcset_ref_of = TypecheckingData.get;
   110 
   111 (* access global tcset *)
   112 
   113 val tcset_of_sg = ! o tcset_ref_of_sg;
   114 val tcset_of = tcset_of_sg o sign_of;
   115 
   116 val tcset = tcset_of o Context.the_context;
   117 val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   118 
   119 (* change global tcset *)
   120 
   121 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   122 
   123 val AddTCs = change_tcset (op addTCs);
   124 val DelTCs = change_tcset (op delTCs);
   125 
   126 fun Typecheck_tac st = typecheck_tac (tcset()) st;
   127 
   128 fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
   129 end;
   130 
   131 
   132 open TypeCheck;
   133 
   134 
   135