CVS: sml-dist/kindch ch.sml, NONE, 1.1.2.1 test.sml, NONE, 1.1.2.1

Update of /cvsroot/smlnj/sml-dist/kindch
In directory sc8-pr-cvs8.sourceforge.net:/tmp/cvs-serv5109/kindch

Added Files:
      Tag: primop-branch-2
	ch.sml test.sml 
Log Message:
added kindch directory

--- NEW FILE: ch.sml ---
(* kinds *)

datatype kind
  = M  (* monotypes *)
  | F of kind list * kind  (* n-ary type functions *)

(* suspensions with arities *)

datatype te
  = Int
  | Arr of te * te
  | App of te * te list
  | Fn of kind list * te  (* should kind list be required to be nonempty? *)
  | Tv of int * int  (* Tv(d,k): d>=1, k>=0; d is level index, k is arg index *)
  | Env of te * int * int * env

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) *)

(* claimed invariant: env is nil, or of the form L*B *)
withtype env = bind list

fun error (msg: string) = raise Fail msg

(* environment lookup - 1 based indexing *)
fun lookEnv (env: env, n) : bind = 
    List.nth(env, n-1)
    handle Subscript => error "env depth"

(* argument list lookup - 0 based indexing *)
fun lookArgs (args: te list, n) : te =
    List.nth(args, n)
    handle Subscript => error "arity mismatch"

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)) =
      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 *)
            | 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 *)
  | red (Env(App(top,targs),i,j,env)) =  (* r9 *)
      App(Env(top,i,j,env), map (fn t => Env(t,i,j,env)) targs)
  | red (Env(Fn(ks,te), i, j, env)) = Fn(ks, Env(te, i+1, j+1, L(j,ks)::env)) (* r10 *)
  | red (Env(Env(te, i, j, env), 0, j', nil)) = Env(te, i, j+j', env)      (* r11 *)
  | red _ = raise NoRedex


(* kind checking *)

(* kind environment *)
type kenv = kind list list

fun eqKind (M,M) = true
  | eqKind (F(ks1,k1), F(ks2,k2)) =
     eqKinds(ks1,ks2) andalso eqKind(k1,k2)
  | eqKind _ = false

and eqKinds ([],[]) = true
  | eqKinds (k1::ks1,k2::ks2) = eqKind(k1,k2) andalso eqKinds(ks1,ks2)
  | eqKinds _ = false

fun lookKind(d, k, kenv) : kind =
    let val targs = List.nth(kenv,d-1)
                    handle Subscript => error "lookKind: depth"
     in List.nth(targs,k)
        handle Subscript => error "lookKind: args" 
    end

fun bindToKinds (L(_,ks)) = ks
  | bindToKinds (B(_,ks)) = ks

(* chkKind : te * kenv -> kind *)

fun chkKind(Fn(ks,b), kenv) =
      F(ks,chkKind(b,ks::kenv))
  | chkKind(Int, _) = M
  | chkKind(Arr(t1,t2),kenv) =
      if (eqKind(chkKind(t1,kenv),M) andalso
          eqKind(chkKind(t2,kenv),M))
      then M
      else error "chkKind: Arr"
  | chkKind(App(top,targs),kenv) = 
      (case chkKind(top,kenv)
         of F(ks,k) => 
              if eqKinds(ks,map (fn t => chkKind(t,kenv)) targs)
              then k else error "chkKind: App"
          | M => error "App: nonfunction operator")
  | chkKind(Tv(d,k), kenv) =
      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")

--- NEW FILE: test.sml ---
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]];

chkKind(te1,kenv0);

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);


-------------------------------------------------------------------------
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