Isar attribute and method setup;
authorwenzelm
Wed Nov 14 23:19:09 2001 +0100 (2001-11-14)
changeset 121894729bbf86626
parent 12188 e4279b7fb8cc
child 12190 32a9c240f225
Isar attribute and method setup;
src/ZF/Tools/typechk.ML
     1.1 --- a/src/ZF/Tools/typechk.ML	Wed Nov 14 23:18:37 2001 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Wed Nov 14 23:19:09 2001 +0100
     1.3 @@ -1,40 +1,68 @@
     1.4 -(*  Title:      ZF/typechk
     1.5 +(*  Title:      ZF/Tools/typechk.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1999  University of Cambridge
     1.9  
    1.10 -Tactics for type checking -- from CTT
    1.11 +Tactics for type checking -- from CTT.
    1.12  *)
    1.13  
    1.14  infix 4 addTCs delTCs;
    1.15  
    1.16 -structure TypeCheck =
    1.17 +signature BASIC_TYPE_CHECK =
    1.18 +sig
    1.19 +  type tcset
    1.20 +  val addTCs: tcset * thm list -> tcset
    1.21 +  val delTCs: tcset * thm list -> tcset
    1.22 +  val typecheck_tac: tcset -> tactic
    1.23 +  val type_solver_tac: tcset -> thm list -> int -> tactic
    1.24 +  val print_tc: tcset -> unit
    1.25 +  val print_tcset: theory -> unit
    1.26 +  val tcset_ref_of: theory -> tcset ref
    1.27 +  val tcset_of: theory -> tcset
    1.28 +  val tcset: unit -> tcset
    1.29 +  val AddTCs: thm list -> unit
    1.30 +  val DelTCs: thm list -> unit
    1.31 +  val TC_add_global: theory attribute
    1.32 +  val TC_del_global: theory attribute
    1.33 +  val TC_add_local: Proof.context attribute
    1.34 +  val TC_del_local: Proof.context attribute
    1.35 +  val Typecheck_tac: tactic
    1.36 +  val Type_solver_tac: thm list -> int -> tactic
    1.37 +end;
    1.38 +
    1.39 +signature TYPE_CHECK =
    1.40 +sig
    1.41 +  include BASIC_TYPE_CHECK
    1.42 +  val setup: (theory -> theory) list
    1.43 +end;
    1.44 +
    1.45 +structure TypeCheck: TYPE_CHECK =
    1.46  struct
    1.47 +
    1.48  datatype tcset =
    1.49 -    TC of {rules: thm list,	(*the type-checking rules*)
    1.50 -	   net: thm Net.net};   (*discrimination net of the same rules*)     
    1.51 -
    1.52 +    TC of {rules: thm list,     (*the type-checking rules*)
    1.53 +           net: thm Net.net};   (*discrimination net of the same rules*)
    1.54  
    1.55  
    1.56  val mem_thm = gen_mem eq_thm
    1.57  and rem_thm = gen_rem eq_thm;
    1.58  
    1.59  fun addTC (cs as TC{rules, net}, th) =
    1.60 -  if mem_thm (th, rules) then 
    1.61 -	 (warning ("Ignoring duplicate type-checking rule\n" ^ 
    1.62 -		   string_of_thm th);
    1.63 -	  cs)
    1.64 +  if mem_thm (th, rules) then
    1.65 +         (warning ("Ignoring duplicate type-checking rule\n" ^
    1.66 +                   string_of_thm th);
    1.67 +          cs)
    1.68    else
    1.69 -      TC{rules	= th::rules,
    1.70 -	 net = Net.insert_term ((concl_of th, th), net, K false)};
    1.71 +      TC{rules  = th::rules,
    1.72 +         net = Net.insert_term ((concl_of th, th), net, K false)};
    1.73  
    1.74  
    1.75  fun delTC (cs as TC{rules, net}, th) =
    1.76    if mem_thm (th, rules) then
    1.77        TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
    1.78 -	 rules	= rem_thm (rules,th)}
    1.79 -  else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); 
    1.80 -	cs);
    1.81 +         rules  = rem_thm (rules,th)}
    1.82 +  else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    1.83 +        cs);
    1.84  
    1.85  val op addTCs = foldl addTC;
    1.86  val op delTCs = foldl delTC;
    1.87 @@ -45,20 +73,20 @@
    1.88    SUBGOAL
    1.89      (fn (prem,i) =>
    1.90        let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
    1.91 -      in 
    1.92 -	 if length rls <= maxr then resolve_tac rls i else no_tac
    1.93 +      in
    1.94 +         if length rls <= maxr then resolve_tac rls i else no_tac
    1.95        end);
    1.96  
    1.97 -fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
    1.98 +fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
    1.99        not (is_Var (head_of a))
   1.100    | is_rigid_elem _ = false;
   1.101  
   1.102 -(*Try solving a:A by assumption provided a is rigid!*) 
   1.103 +(*Try solving a:A by assumption provided a is rigid!*)
   1.104  val test_assume_tac = SUBGOAL(fn (prem,i) =>
   1.105      if is_rigid_elem (Logic.strip_assums_concl prem)
   1.106      then  assume_tac i  else  eq_assume_tac i);
   1.107  
   1.108 -(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
   1.109 +(*Type checking solves a:?A (a rigid, ?A maybe flexible).
   1.110    match_tac is too strict; would refuse to instantiate ?A*)
   1.111  fun typecheck_step_tac (TC{net,...}) =
   1.112      FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
   1.113 @@ -67,21 +95,21 @@
   1.114  
   1.115  (*Compiles a term-net for speed*)
   1.116  val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
   1.117 -				     ballI,allI,conjI,impI];
   1.118 +                                     ballI,allI,conjI,impI];
   1.119  
   1.120  (*Instantiates variables in typing conditions.
   1.121    drawback: does not simplify conjunctions*)
   1.122  fun type_solver_tac tcset hyps = SELECT_GOAL
   1.123      (DEPTH_SOLVE (etac FalseE 1
   1.124 -		  ORELSE basic_res_tac 1
   1.125 -		  ORELSE (ares_tac hyps 1
   1.126 -			  APPEND typecheck_step_tac tcset)));
   1.127 +                  ORELSE basic_res_tac 1
   1.128 +                  ORELSE (ares_tac hyps 1
   1.129 +                          APPEND typecheck_step_tac tcset)));
   1.130  
   1.131  
   1.132  
   1.133  fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
   1.134      TC {rules = gen_union eq_thm (rules,rules'),
   1.135 -	net = Net.merge (net, net', eq_thm)};
   1.136 +        net = Net.merge (net, net', eq_thm)};
   1.137  
   1.138  (*print tcsets*)
   1.139  fun print_tc (TC{rules,...}) =
   1.140 @@ -89,6 +117,8 @@
   1.141         (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
   1.142  
   1.143  
   1.144 +(** global tcset **)
   1.145 +
   1.146  structure TypecheckingArgs =
   1.147    struct
   1.148    val name = "ZF/type-checker";
   1.149 @@ -103,12 +133,11 @@
   1.150  
   1.151  structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   1.152  
   1.153 -val setup = [TypecheckingData.init];
   1.154 -
   1.155  val print_tcset = TypecheckingData.print;
   1.156  val tcset_ref_of_sg = TypecheckingData.get_sg;
   1.157  val tcset_ref_of = TypecheckingData.get;
   1.158  
   1.159 +
   1.160  (* access global tcset *)
   1.161  
   1.162  val tcset_of_sg = ! o tcset_ref_of_sg;
   1.163 @@ -117,6 +146,7 @@
   1.164  val tcset = tcset_of o Context.the_context;
   1.165  val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   1.166  
   1.167 +
   1.168  (* change global tcset *)
   1.169  
   1.170  fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   1.171 @@ -127,10 +157,71 @@
   1.172  fun Typecheck_tac st = typecheck_tac (tcset()) st;
   1.173  
   1.174  fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
   1.175 -end;
   1.176 -
   1.177 -
   1.178 -open TypeCheck;
   1.179  
   1.180  
   1.181  
   1.182 +(** local tcset **)
   1.183 +
   1.184 +structure LocalTypecheckingArgs =
   1.185 +struct
   1.186 +  val name = TypecheckingArgs.name;
   1.187 +  type T = tcset;
   1.188 +  val init = tcset_of;
   1.189 +  fun print _ tcset = print_tc tcset;
   1.190 +end;
   1.191 +
   1.192 +structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
   1.193 +
   1.194 +
   1.195 +(* attributes *)
   1.196 +
   1.197 +fun global_att f (thy, th) =
   1.198 +  let val r = tcset_ref_of thy
   1.199 +  in r := f (! r, th); (thy, th) end;
   1.200 +
   1.201 +fun local_att f (ctxt, th) = (LocalTypecheckingData.map (fn tcset => f (tcset, th)) ctxt, th);
   1.202 +
   1.203 +val TC_add_global = global_att addTC;
   1.204 +val TC_del_global = global_att delTC;
   1.205 +val TC_add_local = local_att addTC;
   1.206 +val TC_del_local = local_att delTC;
   1.207 +
   1.208 +val TC_attr =
   1.209 + (Attrib.add_del_args TC_add_global TC_del_global,
   1.210 +  Attrib.add_del_args TC_add_local TC_del_local);
   1.211 +
   1.212 +
   1.213 +(* methods *)
   1.214 +
   1.215 +fun TC_args x = Method.only_sectioned_args
   1.216 +  [Args.add -- Args.colon >> K (I, TC_add_local),
   1.217 +   Args.del -- Args.colon >> K (I, TC_del_local)] x;
   1.218 +
   1.219 +fun typecheck ctxt =
   1.220 +  Method.SIMPLE_METHOD (CHANGED (typecheck_tac (LocalTypecheckingData.get ctxt)));
   1.221 +
   1.222 +
   1.223 +
   1.224 +(** theory setup **)
   1.225 +
   1.226 +val setup =
   1.227 + [TypecheckingData.init, LocalTypecheckingData.init,
   1.228 +  Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
   1.229 +  Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
   1.230 +
   1.231 +
   1.232 +(** outer syntax **)
   1.233 +
   1.234 +val print_tcsetP =
   1.235 +  OuterSyntax.improper_command "print_tcset" "print context of ZF type-checker"
   1.236 +    OuterSyntax.Keyword.diag
   1.237 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
   1.238 +      (Toplevel.node_case print_tcset (LocalTypecheckingData.print o Proof.context_of)))));
   1.239 +
   1.240 +val _ = OuterSyntax.add_parsers [print_tcsetP];
   1.241 +
   1.242 +
   1.243 +end;
   1.244 +
   1.245 +structure BasicTypeCheck: BASIC_TYPE_CHECK = TypeCheck;
   1.246 +open BasicTypeCheck;