src/ZF/Tools/typechk.ML

--- a/src/ZF/Tools/typechk.ML	Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Tools/typechk.ML	Wed Jan 27 10:31:31 1999 +0100
@@ -1,11 +1,54 @@
 (*  Title:      ZF/typechk
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
+    Copyright   1999  University of Cambridge
 
 Tactics for type checking -- from CTT
 *)
 
+infix 4 addTCs delTCs;
+
+structure TypeCheck =
+struct
+datatype tcset =
+    TC of {rules: thm list,	(*the type-checking rules*)
+	   net: thm Net.net};   (*discrimination net of the same rules*)     
+
+
+
+val mem_thm = gen_mem eq_thm
+and rem_thm = gen_rem eq_thm;
+
+fun addTC (cs as TC{rules, net}, th) =
+  if mem_thm (th, rules) then 
+	 (warning ("Ignoring duplicate type-checking rule\n" ^ 
+		   string_of_thm th);
+	  cs)
+  else
+      TC{rules	= th::rules,
+	 net = Net.insert_term ((concl_of th, th), net, K false)};
+
+
+fun delTC (cs as TC{rules, net}, th) =
+  if mem_thm (th, rules) then
+      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
+	 rules	= rem_thm (rules,th)}
+  else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); 
+	cs);
+
+val op addTCs = foldl addTC;
+val op delTCs = foldl delTC;
+
+
+(*resolution using a net rather than rules*)
+fun net_res_tac maxr net =
+  SUBGOAL
+    (fn (prem,i) =>
+      let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
+      in 
+	 if length rls <= maxr then resolve_tac rls i else no_tac
+      end);
+
 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
       not (is_Var (head_of a))
   | is_rigid_elem _ = false;
@@ -17,18 +60,75 @@
 
 (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
   match_tac is too strict; would refuse to instantiate ?A*)
-fun typechk_step_tac tyrls =
-    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
+fun typecheck_step_tac (TC{net,...}) =
+    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
 
-fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
+fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
 
-val ZF_typechecks =
-    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
+(*Compiles a term-net for speed*)
+val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
+				     ballI,allI,conjI,impI];
 
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
-fun type_auto_tac tyrls hyps = SELECT_GOAL
-    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
-           ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
-			    ballI,allI,conjI,impI] 1));
+fun type_solver_tac tcset hyps = SELECT_GOAL
+    (DEPTH_SOLVE (etac FalseE 1
+		  ORELSE basic_res_tac 1
+		  ORELSE (ares_tac hyps 1
+			  APPEND typecheck_step_tac tcset)));
+
+
+
+fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
+    TC {rules = gen_union eq_thm (rules,rules'),
+	net = Net.merge (net, net', eq_thm)};
+
+(*print tcsets*)
+fun print_tc (TC{rules,...}) =
+    Pretty.writeln
+       (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
+
+
+structure TypecheckingArgs =
+  struct
+  val name = "ZF/type-checker";
+  type T = tcset ref;
+  val empty = ref (TC{rules=[], net=Net.empty});
+  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
+  fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
+  fun print _ (ref tc) = print_tc tc;
+  end;
+
+structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
 
+val setup = [TypecheckingData.init];
+
+val print_tcset = TypecheckingData.print;
+val tcset_ref_of_sg = TypecheckingData.get_sg;
+val tcset_ref_of = TypecheckingData.get;
+
+(* access global tcset *)
+
+val tcset_of_sg = ! o tcset_ref_of_sg;
+val tcset_of = tcset_of_sg o sign_of;
+
+val tcset = tcset_of o Context.the_context;
+val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
+
+(* change global tcset *)
+
+fun change_tcset f x = tcset_ref () := (f (tcset (), x));
+
+val AddTCs = change_tcset (op addTCs);
+val DelTCs = change_tcset (op delTCs);
+
+fun Typecheck_tac st = typecheck_tac (tcset()) st;
+
+fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
+end;
+
+
+open TypeCheck;
+
+
+