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