CVS: sml-dist/kindch ch.sml, 1.1.2.1, 1.1.2.2 test.sml, 1.1.2.2, 1.1.2.3
David MacQueen <[email protected]> Wed, 16 Aug 2006 16:25:05 -0700
| Newsgroups | gmane.comp.lang.sml.smlnj.commits |
|---|---|
| Message-ID | <[email protected]> |
Update of /cvsroot/smlnj/sml-dist/kindch
In directory sc8-pr-cvs8.sourceforge.net:/tmp/cvs-serv29289/kindch
Modified Files:
Tag: primop-branch-2
ch.sml test.sml
Log Message:
completed prototype kind checker
Index: ch.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/kindch/Attic/ch.sml,v
retrieving revision 1.1.2.1
retrieving revision 1.1.2.2
diff -C2 -d -r1.1.2.1 -r1.1.2.2
*** ch.sml 14 Aug 2006 21:42:33 -0000 1.1.2.1
--- ch.sml 16 Aug 2006 23:25:03 -0000 1.1.2.2
***************
*** 1,6 ****
--- 1,13 ----
+ (* invariants:
+ * i = length env
+ * last(env) is a B
+ *)
+
(* kinds *)
datatype kind
= M (* monotypes *)
+ | X (* boxed types *)
+ | Y (* strange *)
| F of kind list * kind (* n-ary type functions *)
***************
*** 16,20 ****
and bind
! = B of te list * kind list
(* suspended subst produced by lazy beta reduction (r1) *)
| L of int * kind list (* lifted lambda binding (r10) *)
--- 23,27 ----
and bind
! = B of int * te list * kind list
(* suspended subst produced by lazy beta reduction (r1) *)
| L of int * kind list (* lifted lambda binding (r10) *)
***************
*** 37,42 ****
exception NoRedex
! (* reduction -- this is not a complete evaluator *)
! fun red (App(Fn(ks,body),args)) = Env(body, 1, 0, B(args,ks)::nil) (* r1 *)
| red (Env(te, 0, 0, nil)) = te (* r2: closure wrt empty env *)
| red (Env(Tv(n,k), i, j, env)) =
--- 44,61 ----
exception NoRedex
! (* r12 is the beta-redex special case where the body of the lambda
! * abstraction is a closure that has been pushed through the lambda
! * (as opposed to created in situ, by contraction of a body that was
! * a beta-redex. Not entirely sure that this configuration could not
! * also be reached via a variable lookup, where the original body
! * of the lambda abstraction was a (relatively) free variable. *)
!
! (* reduction rules -- this is not a complete evaluator *)
! fun red (App(Fn(ks,b as Env(b',i,j,L(j',_)::env)),args)) =
! if j = j'+1 then Env(b', i, j', B(j',args,ks)::env) (* r12 *)
! (* the test j = j'+1 is meant to ensure that the body closure
! * arrived there by being pushed through the lambda *)
! else Env(b, 1, 0, B(0,args,ks)::nil) (* r1 *)
! | red (App(Fn(ks,b),args)) = Env(b, 1, 0, B(0,args,ks)::nil) (* r1 *)
| red (Env(te, 0, 0, nil)) = te (* r2: closure wrt empty env *)
| red (Env(Tv(n,k), i, j, env)) =
***************
*** 44,49 ****
else (* n <= i *) (* "bound" Tv *)
(case lookEnv(env, n)
! of L(j', _) => Tv(j-j', k) (* r5: lambda bound *)
! | B(args, _) => Env(lookArgs(args, k), 0, j, nil)) (* r6: env bound *)
| red (Env(Int, _, _, _)) = Int (* r7 *)
| red (Env(Arr(t1,t2),i,j,env)) = Arr(Env(t1,i,j,env), Env(t2,i,j,env)) (* r8 *)
--- 63,69 ----
else (* n <= i *) (* "bound" Tv *)
(case lookEnv(env, n)
! of L(j', _) => Tv(j-j', k) (* r5: lambda bound variable *)
! | B(j',args, _) => (* r6: env bound *)
! Env(lookArgs(args, k), 0, j-j', nil))
| red (Env(Int, _, _, _)) = Int (* r7 *)
| red (Env(Arr(t1,t2),i,j,env)) = Arr(Env(t1,i,j,env), Env(t2,i,j,env)) (* r8 *)
***************
*** 54,57 ****
--- 74,96 ----
| red _ = raise NoRedex
+ exception NotEnvRedex
+
+ (* reduction rules -- this is not a complete evaluator *)
+ fun envRed (Env(te, 0, 0, nil)) = te (* r2: closure wrt empty env *)
+ | envRed (Env(Tv(n,k), i, j, env)) =
+ if n > i then Tv(n-i+j,k) (* r4: rfree Tv *)
+ else (* n <= i *) (* "bound" Tv *)
+ (case lookEnv(env, n)
+ of L(j', _) => Tv(j-j', k) (* r5: lambda bound variable *)
+ | B(j',args, _) => (* r6: env bound *)
+ Env(lookArgs(args, k), 0, j-j', nil))
+ | envRed (Env(Int, _, _, _)) = Int (* r7 *)
+ | envRed (Env(Arr(t1,t2),i,j,env)) = Arr(Env(t1,i,j,env), Env(t2,i,j,env)) (* r8 *)
+ | envRed (Env(App(top,targs),i,j,env)) = (* r9 *)
+ App(Env(top,i,j,env), map (fn t => Env(t,i,j,env)) targs)
+ | envRed (Env(Fn(ks,te), i, j, env)) = Fn(ks, Env(te, i+1, j+1, L(j,ks)::env)) (* r10 *)
+ | envRed (Env(Env(te, i, j, env), 0, j', nil)) = Env(te, i, j+j', env) (* r11 *)
+ | envRed _ = raise NotEnvRedex
+
(* kind checking *)
***************
*** 61,64 ****
--- 100,105 ----
fun eqKind (M,M) = true
+ | eqKind (X,X) = true
+ | eqKind (Y,Y) = true
| eqKind (F(ks1,k1), F(ks2,k2)) =
eqKinds(ks1,ks2) andalso eqKind(k1,k2)
***************
*** 77,81 ****
fun bindToKinds (L(_,ks)) = ks
! | bindToKinds (B(_,ks)) = ks
(* chkKind : te * kenv -> kind *)
--- 118,122 ----
fun bindToKinds (L(_,ks)) = ks
! | bindToKinds (B(_,_,ks)) = ks
(* chkKind : te * kenv -> kind *)
***************
*** 98,111 ****
lookKind(d, k, kenv)
| chkKind(Env(te,0,j,nil), kenv) = (* from r6; i should be 0 *)
! (chkKind(te,List.drop(kenv,j))
! handle Subscript => error "chkKind[Env]: dropping too many frames")
| chkKind(Env(te,i,j,env), kenv) = (* env not nil *)
! ((case List.last env
! of B(args,ks) =>
! let val kenv' = List.drop(kenv,j)
! in eqKinds(ks, map (fn t => chkKind(t,kenv')) args);
! chkKind(te, foldr (fn (b,kenv) => bindToKinds b :: kenv) nil env)
! end
! | _ => error "chkKind: env not ending in B")
! handle Empty => error "chkKind[Env]: unexpected empty environment"
! | Subscript => error "chkKind[Env]: dropping too many frames")
--- 139,250 ----
lookKind(d, k, kenv)
| chkKind(Env(te,0,j,nil), kenv) = (* from r6; i should be 0 *)
! (chkKind(te,List.drop(kenv,j))
! handle Subscript => error "chkKind[Env]: dropping too many frames")
| chkKind(Env(te,i,j,env), kenv) = (* env not nil *)
! (let val kenv' = List.drop(kenv,j)
! in chkKindEnv(env,j,kenv);
! chkKind(te, foldr (fn (b,ke) => bindToKinds b :: ke) kenv' env)
! end
! handle Subscript => error "chkKind[Env]: dropping too many frames")
!
! (* because an environment may have more than one bind (B) frame, we must
! * kind check all such B frames in the environment *)
! and chkKindEnv(env,j,kenv) : unit =
! let fun chkFrame(L(_,_)) = () (* nothing to check *)
! | chkFrame(B(j',args,ks)) =
! let val kenv' = List.drop(kenv, j-j')
! in if eqKinds(ks, map (fn t => chkKind(t,kenv')) args)
! then ()
! else error "chkKindEnv: B frame kinds mismatch"
! end
! in app chkFrame env
! end
!
! fun lzrd (te: te) =
! let fun g(x) =
! let fun loop x = loop(envRed x)
! in loop x handle NotEnvRedex => x
! end
! in g te
! end
!
! fun isNorm Int = true
! | isNorm (Arr(t1,t2)) = isNorm t1 andalso isNorm t2
! | isNorm (Tv _) = true
! | isNorm (Fn(_,b)) = isNorm b
! | isNorm (App(Fn _,_)) = false
! | isNorm (App(top,targs)) = isNorm top andalso List.all isNorm targs
! | isNorm (Env _) = false
!
! fun whnm (te: te) =
! if isNorm te then te else
! case lzrd te
! of (App(Fn(ks,b as Env(b',i,j,L(j',_)::env)),args)) =>
! if j = j'+1 then whnm(Env(b', i, j', B(j',args,ks)::env)) (* r12 *)
! else Env(b, 1, 0, B(0,args,ks)::nil) (* r1 *)
! | (App(t,args)) =>
! let val t' = whnm t
! in case t'
! of Fn(ks,b) => whnm(Env(b,1,0,B(0,args,ks)::nil))
! | _ => App(t',args)
! end
! | (Env _) => error "whnm: unexpected Env"
! | t => t
!
! fun bsnorm (te: te) =
! let val te' = whnm te
! in case te'
! of Int => Int
! | Arr(t1,t2) => Arr(bsnorm t1,bsnorm t2)
! | Tv _ => te'
! | App(t1,t2) => App(bsnorm t1,map bsnorm t2)
! | Fn(ks,b) => Fn(ks,bsnorm b)
! | Env _ => error "Env in bsnorm"
! end
!
! fun revcat(a::rest,b) = revcat(rest,a::b)
! | revcat(nil,b) = b
!
! fun red (App(Fn(ks,b as Env(b',i,j,L(j',_)::env)),args)) =
! if j = j'+1 then (print "r12\n"; Env(b', i, j', B(j',args,ks)::env)) (* r12 *)
! (* the test j = j'+1 is meant to ensure that the body closure
! * arrived there by being pushed through the lambda *)
! else (print "r1a\n"; Env(b, 1, 0, B(0,args,ks)::nil)) (* r1 *)
! | red (App(Fn(ks,b),args)) = (print "r1b\n"; Env(b, 1, 0, B(0,args,ks)::nil)) (* r1 *)
! | red (Env(te, 0, 0, nil)) = (print "r2\n"; te) (* r2: closure wrt empty env *)
! | red (Env(Tv(n,k), i, j, env)) =
! if n > i then (print "r4\n"; Tv(n-i+j,k)) (* r4: rfree Tv *)
! else (* n <= i *) (* "bound" Tv *)
! (case lookEnv(env, n)
! of L(j', _) => (print "r5\n"; Tv(j-j', k)) (* r5: lambda bound variable *)
! | B(j',args, _) => (* r6: env bound *)
! (print "r6\n"; Env(lookArgs(args, k), 0, j-j', nil)))
! | red (Env(Int, _, _, _)) = (print "r7\n"; Int) (* r7 *)
! | red (Env(Arr(t1,t2),i,j,env)) =
! (print "r8\n"; Arr(Env(t1,i,j,env), Env(t2,i,j,env))) (* r8 *)
! | red (Env(App(top,targs),i,j,env)) = (* r9 *)
! (print "r9\n"; App(Env(top,i,j,env), map (fn t => Env(t,i,j,env)) targs))
! | red (Env(Fn(ks,te), i, j, env)) =
! (print "r10\n"; Fn(ks, Env(te, i+1, j+1, L(j,ks)::env))) (* r10 *)
! | red (Env(Env(te, i, j, env), 0, j', nil)) =
! (print "r11\n"; Env(te, i, j+j', env)) (* r11 *)
! | red (t as App(top,targs)) =
! if isNorm top then
! let fun loop(xs,[]) = t
! | loop(xs,y::ys) =
! if isNorm y then loop(y::xs,ys)
! else App(top,revcat(xs,(red y :: ys)))
! in loop([],targs)
! end
! else App(red top, targs)
! | red (t as Arr(t1,t2)) =
! if isNorm t1 then
! if isNorm t2 then t
! else Arr(t1,red t2)
! else Arr(red t1,t2)
! | red (t as Fn(ks,b)) = if isNorm b then t else Fn(ks,red b)
! | red t = t
!
! fun eval t = (chkKind(t,nil); if isNorm t then t else eval(red t))
!
! fun step t = (chkKind(t,nil); red t)
Index: test.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/kindch/Attic/test.sml,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -C2 -d -r1.1.2.2 -r1.1.2.3
*** test.sml 15 Aug 2006 16:47:39 -0000 1.1.2.2
--- test.sml 16 Aug 2006 23:25:03 -0000 1.1.2.3
***************
*** 1,18 ****
! (* original: (\x:M=>M.\y:M.(x y)) a b -- a,b free vars *)
! (* after r1,r10: \[M].Env((#2,0 [#1,0]), 2, 1, L(0,[M],B([#1,0],[[M]=>M]))) *)
val te1 =
! App(Fn([M],Env(App(Tv(2,0),[Tv(1,0)]),2,1,[L(0,[M]),B([Tv(1,0)],[F([M],M)])])),
[Tv(2,0)]);
val kenv0 = [[F([M],M)],[M]]; (* a:M=>M, b:M *)
! chkKind(te1,kenv0);
! (* original: @(\x:M=>M.\y:M.@(\z:M.\u:M.z), (x y)), a); kenv0 = a:M=>M *)
(* after r1, r10, r9, ..., r11: *)
val te2 =
Fn([M],
Fn([F([M],M)],
! Env(App(Tv(2,0),[Tv(1,0)]),2,2,[L(0,[M]),B([Tv(1,0)],[F([M],M)])])));
! chkKind(te2,kenv0);
--- 1,49 ----
! (* original: (\x:M=>M.\y:M.(x y)) a b
! * -- external kind environment a: [M]=>M, b: M
! * expected kind: M *)
! (* after r1,r10: \[M].Env((#2,0 [#1,0]), 2, 1, L(0,[M],B(0,[#1,0],[[M]=>M]))) *)
! val te0 = Fn([F([M],M)],Fn([M],App(App(Fn([F([M],M)],Fn([M],App(Tv(2,0),[Tv(1,0)]))),
! [Tv(2,0)]),[Tv(1,0)])));
!
! (*
val te1 =
! App(Fn([M],Env(App(Tv(2,0),[Tv(1,0)]),2,1,[L(0,[M]),B(0,[Tv(1,0)],[F([M],M)])])),
[Tv(2,0)]);
val kenv0 = [[F([M],M)],[M]]; (* a:M=>M, b:M *)
! val k1 = chkKind(te1,kenv0);
! (* original: @(\x:M=>M.\y:M.@(\z:M.\u:M.z, @(x,y)), a); kenv0 = a:M=>M *)
(* after r1, r10, r9, ..., r11: *)
val te2 =
Fn([M],
Fn([F([M],M)],
! Env(App(Tv(2,0),[Tv(1,0)]),2,2,[L(0,[M]),B(0,[Tv(1,0)],[F([M],M)])])));
! val k2 = chkKind(te2,kenv0);
! *)
!
! val te2 = Fn([F([M],M)],App(Fn([F([M],M)],Fn([M],App(Fn([M],Fn([M],Tv(2,0))),
! [App(Tv(2,0),[Tv(1,0)])]))), [Tv(1,0)]));
!
! (* \x:M=>M.\y:M.@(x, @(\z:(M=>M)=>M.@(z, @(x,y),@(\w:(M=>M)=>(M=>M).w,x)))) *)
! val te3 = Fn([F([M],M)], (* \x: M=>M *)
! Fn([M], (* \y: M *)
! App(Tv(2,0), (* @(x, *)
! [App(
! Fn([F([M],M)], (* \z: (M=>M)=>M *)
! App(Tv(1,0), (* @(z, *)
! [App(Tv(3,0),[Tv(2,0)])])), (* @(x,y) *)
! [App(Fn([F([M],M)], (* \w: (M=>M)=>(M=>M) *)
! Tv(1,0)), (* w *)
! [Tv(2,0)])])]))); (* x *)
!
!
!
! val te4 = Fn([X],
! App(Fn([X],
! App(Fn([X],
! Fn([Y],Tv(2,0))),
! [Tv(1,0)])),
! [Tv(1,0)]));
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642