src/CCL/typecheck.ML
 author clasohm Mon Jan 29 13:58:15 1996 +0100 (1996-01-29) changeset 1459 d12da312eff4 parent 757 2ca12511676d child 3537 79ac9b475621 permissions -rw-r--r--
expanded tabs
 clasohm@1459 ` 1` ```(* Title: CCL/typecheck ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@1459 ` 3` ``` Author: Martin Coen, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```*) ``` clasohm@0 ` 7` clasohm@0 ` 8` ```(*** Lemmas for constructors and subtypes ***) ``` clasohm@0 ` 9` clasohm@0 ` 10` ```(* 0-ary constructors do not need additional rules as they are handled *) ``` clasohm@0 ` 11` ```(* correctly by applying SubtypeI *) ``` clasohm@0 ` 12` ```(* ``` clasohm@0 ` 13` ```val Subtype_canTs = ``` clasohm@0 ` 14` ``` let fun tac prems = cut_facts_tac prems 1 THEN ``` clasohm@0 ` 15` ``` REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE ``` lcp@642 ` 16` ``` etac SubtypeE 1) ``` clasohm@0 ` 17` ``` fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) ``` clasohm@0 ` 18` ``` in map solve ``` clasohm@0 ` 19` ``` ["P(one) ==> one : {x:Unit.P(x)}", ``` clasohm@0 ` 20` ``` "P(true) ==> true : {x:Bool.P(x)}", ``` clasohm@0 ` 21` ``` "P(false) ==> false : {x:Bool.P(x)}", ``` clasohm@0 ` 22` ``` "a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", ``` clasohm@0 ` 23` ``` "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}", ``` clasohm@0 ` 24` ``` "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}", ``` clasohm@0 ` 25` ``` "P(zero) ==> zero : {x:Nat.P(x)}", ``` clasohm@0 ` 26` ``` "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}", ``` clasohm@0 ` 27` ``` "P([]) ==> [] : {x:List(A).P(x)}", ``` clasohm@289 ` 28` ``` "h : {x:A. t : {y:List(A).P(x\$y)}} ==> h\$t : {x:List(A).P(x)}" ``` clasohm@0 ` 29` ``` ] end; ``` clasohm@0 ` 30` ```*) ``` clasohm@0 ` 31` ```val Subtype_canTs = ``` clasohm@0 ` 32` ``` let fun tac prems = cut_facts_tac prems 1 THEN ``` clasohm@0 ` 33` ``` REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE ``` lcp@642 ` 34` ``` etac SubtypeE 1) ``` clasohm@0 ` 35` ``` fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) ``` clasohm@0 ` 36` ``` in map solve ``` clasohm@0 ` 37` ``` ["a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", ``` clasohm@0 ` 38` ``` "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}", ``` clasohm@0 ` 39` ``` "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}", ``` clasohm@0 ` 40` ``` "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}", ``` clasohm@289 ` 41` ``` "h : {x:A. t : {y:List(A).P(x\$y)}} ==> h\$t : {x:List(A).P(x)}" ``` clasohm@0 ` 42` ``` ] end; ``` clasohm@0 ` 43` clasohm@0 ` 44` ```val prems = goal Type.thy ``` clasohm@0 ` 45` ``` "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; ``` clasohm@0 ` 46` ```by (cut_facts_tac prems 1); ``` lcp@642 ` 47` ```by (etac (letB RS ssubst) 1); ``` lcp@642 ` 48` ```by (assume_tac 1); ``` clasohm@757 ` 49` ```qed "letT"; ``` clasohm@0 ` 50` clasohm@0 ` 51` ```val prems = goal Type.thy ``` clasohm@0 ` 52` ``` "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; ``` clasohm@0 ` 53` ```by (REPEAT (ares_tac (applyT::prems) 1)); ``` clasohm@757 ` 54` ```qed "applyT2"; ``` clasohm@0 ` 55` clasohm@0 ` 56` ```val prems = goal Type.thy ``` clasohm@0 ` 57` ``` "[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}"; ``` clasohm@0 ` 58` ```by (fast_tac (type_cs addSIs prems) 1); ``` clasohm@757 ` 59` ```qed "rcall_lemma1"; ``` clasohm@0 ` 60` clasohm@0 ` 61` ```val prems = goal Type.thy ``` clasohm@0 ` 62` ``` "[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}"; ``` clasohm@0 ` 63` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 64` ```by (fast_tac (type_cs addSIs prems) 1); ``` clasohm@757 ` 65` ```qed "rcall_lemma2"; ``` clasohm@0 ` 66` clasohm@0 ` 67` ```val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2]; ``` clasohm@0 ` 68` clasohm@0 ` 69` ```(***********************************TYPECHECKING*************************************) ``` clasohm@0 ` 70` clasohm@0 ` 71` ```fun bvars (Const("all",_) \$ Abs(s,_,t)) l = bvars t (s::l) ``` clasohm@0 ` 72` ``` | bvars _ l = l; ``` clasohm@0 ` 73` clasohm@0 ` 74` ```fun get_bno l n (Const("all",_) \$ Abs(s,_,t)) = get_bno (s::l) n t ``` clasohm@0 ` 75` ``` | get_bno l n (Const("Trueprop",_) \$ t) = get_bno l n t ``` clasohm@0 ` 76` ``` | get_bno l n (Const("Ball",_) \$ _ \$ Abs(s,_,t)) = get_bno (s::l) (n+1) t ``` clasohm@0 ` 77` ``` | get_bno l n (Const("op :",_) \$ t \$ _) = get_bno l n t ``` clasohm@0 ` 78` ``` | get_bno l n (t \$ s) = get_bno l n t ``` clasohm@0 ` 79` ``` | get_bno l n (Bound m) = (m-length(l),n); ``` clasohm@0 ` 80` clasohm@0 ` 81` ```(* Not a great way of identifying induction hypothesis! *) ``` clasohm@0 ` 82` ```fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse ``` clasohm@0 ` 83` ``` could_unify(x,hd (prems_of rcall2T)) orelse ``` clasohm@0 ` 84` ``` could_unify(x,hd (prems_of rcall3T)); ``` clasohm@0 ` 85` clasohm@0 ` 86` ```fun IHinst tac rls i = STATE (fn state => ``` clasohm@0 ` 87` ``` let val (_,_,Bi,_) = dest_state(state,i); ``` clasohm@0 ` 88` ``` val bvs = bvars Bi []; ``` clasohm@0 ` 89` ``` val ihs = filter could_IH (Logic.strip_assums_hyp Bi); ``` clasohm@0 ` 90` ``` val rnames = map (fn x=> ``` clasohm@0 ` 91` ``` let val (a,b) = get_bno [] 0 x ``` clasohm@0 ` 92` ``` in (nth_elem(a,bvs),b) end) ihs; ``` clasohm@0 ` 93` ``` fun try_IHs [] = no_tac ``` clasohm@0 ` 94` ``` | try_IHs ((x,y)::xs) = tac [("g",x)] (nth_elem(y-1,rls)) i ORELSE (try_IHs xs); ``` clasohm@0 ` 95` ``` in try_IHs rnames end); ``` clasohm@0 ` 96` clasohm@0 ` 97` ```(*****) ``` clasohm@0 ` 98` clasohm@0 ` 99` ```val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@ ``` clasohm@0 ` 100` ``` precTs@letrecTs@[letT]@Subtype_canTs; ``` clasohm@0 ` 101` clasohm@0 ` 102` ```fun is_rigid_prog t = ``` clasohm@0 ` 103` ``` case (Logic.strip_assums_concl t) of ``` clasohm@0 ` 104` ``` (Const("Trueprop",_) \$ (Const("op :",_) \$ a \$ _)) => (term_vars a = []) ``` clasohm@0 ` 105` ``` | _ => false; ``` clasohm@0 ` 106` clasohm@0 ` 107` ```fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i; ``` clasohm@0 ` 108` ``` in IHinst tac rcallTs i end THEN ``` clasohm@0 ` 109` ``` eresolve_tac rcall_lemmas i; ``` clasohm@0 ` 110` clasohm@0 ` 111` ```fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE ``` clasohm@0 ` 112` ``` rcall_tac i ORELSE ``` clasohm@0 ` 113` ``` ematch_tac [SubtypeE] i ORELSE ``` clasohm@0 ` 114` ``` match_tac [SubtypeI] i; ``` clasohm@0 ` 115` clasohm@0 ` 116` ```fun tc_step_tac prems i = STATE(fn state => ``` clasohm@0 ` 117` ``` if (i>length(prems_of state)) ``` clasohm@0 ` 118` ``` then no_tac ``` clasohm@0 ` 119` ``` else let val (_,_,c,_) = dest_state(state,i) ``` clasohm@0 ` 120` ``` in if is_rigid_prog c then raw_step_tac prems i else no_tac ``` clasohm@0 ` 121` ``` end); ``` clasohm@0 ` 122` clasohm@0 ` 123` ```fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i; ``` clasohm@0 ` 124` clasohm@0 ` 125` ```val tac = typechk_tac [] 1; ``` clasohm@0 ` 126` clasohm@0 ` 127` clasohm@0 ` 128` ```(*** Clean up Correctness Condictions ***) ``` clasohm@0 ` 129` clasohm@0 ` 130` ```val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' ``` clasohm@0 ` 131` ``` hyp_subst_tac); ``` clasohm@0 ` 132` clasohm@0 ` 133` ```val clean_ccs_tac = ``` clasohm@0 ` 134` ``` let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i; ``` clasohm@0 ` 135` ``` in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' ``` clasohm@0 ` 136` ``` eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' ``` clasohm@0 ` 137` ``` hyp_subst_tac)) end; ``` clasohm@0 ` 138` clasohm@0 ` 139` ```fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN ``` clasohm@0 ` 140` ``` clean_ccs_tac) i; ``` clasohm@0 ` 141` clasohm@0 ` 142`