added context type solver;
authorwenzelm
Fri Jul 30 10:44:27 2004 +0200 (2004-07-30)
changeset 15090970c2668c694
parent 15089 430264838064
child 15091 77d160469390
added context type solver;
src/ZF/Tools/typechk.ML
     1.1 --- a/src/ZF/Tools/typechk.ML	Fri Jul 30 10:42:19 2004 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Fri Jul 30 10:44:27 2004 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4    val TC_del_local: Proof.context attribute
     1.5    val Typecheck_tac: tactic
     1.6    val Type_solver_tac: thm list -> int -> tactic
     1.7 +  val local_tcset_of: Proof.context -> tcset
     1.8 +  val context_type_solver: context_solver
     1.9  end;
    1.10  
    1.11  signature TYPE_CHECK =
    1.12 @@ -175,6 +177,13 @@
    1.13  end;
    1.14  
    1.15  structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
    1.16 +val local_tcset_of = LocalTypecheckingData.get;
    1.17 +
    1.18 +
    1.19 +(* solver *)
    1.20 +
    1.21 +val context_type_solver =
    1.22 +  Simplifier.mk_context_solver "context types" (type_solver_tac o local_tcset_of);
    1.23  
    1.24  
    1.25  (* attributes *)
    1.26 @@ -202,7 +211,7 @@
    1.27     Args.del -- Args.colon >> K (I, TC_del_local)] x;
    1.28  
    1.29  fun typecheck ctxt =
    1.30 -  Method.SIMPLE_METHOD (CHANGED (typecheck_tac (LocalTypecheckingData.get ctxt)));
    1.31 +  Method.SIMPLE_METHOD (CHANGED (typecheck_tac (local_tcset_of ctxt)));
    1.32  
    1.33  
    1.34  
    1.35 @@ -210,6 +219,7 @@
    1.36  
    1.37  val setup =
    1.38   [TypecheckingData.init, LocalTypecheckingData.init,
    1.39 +  Simplifier.add_context_unsafe_solver context_type_solver,
    1.40    Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
    1.41    Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
    1.42