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