CVS: sml-dist/src/compiler/FLINT/kernel ltybasic.sig, 1.8.26.3, 1.8.26.4 ltybasic.sml, 1.13.24.3, 1.13.24.4 ltyextern.sig, 1.9, 1.9.26.1 ltyextern.sml, 1.19.24.3, 1.19.24.4 ltykernel.sml, 1.18.12.17, 1.18.12.18

David MacQueen <[email protected]> Thu, 17 Aug 2006 16:13:16 -0700
Newsgroups gmane.comp.lang.sml.smlnj.commits
Message-ID <[email protected]>
Update of /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel
In directory sc8-pr-cvs8.sourceforge.net:/tmp/cvs-serv28570/src/compiler/FLINT/kernel

Modified Files:
      Tag: primop-branch-2
	ltybasic.sig ltybasic.sml ltyextern.sig ltyextern.sml 
	ltykernel.sml 
Log Message:
preparing for kind checking

Index: ltybasic.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltybasic.sig,v
retrieving revision 1.8.26.3
retrieving revision 1.8.26.4
diff -C2 -d -r1.8.26.3 -r1.8.26.4
*** ltybasic.sig	11 Aug 2006 20:42:23 -0000	1.8.26.3
--- ltybasic.sig	17 Aug 2006 23:13:13 -0000	1.8.26.4
***************
*** 116,123 ****
  
  (** utility functions on tycEnv *)
! exception tcUnbound
! type tycEnv = LtyKernel.tycEnv
! val initTycEnv : tycEnv
! val tcInsert : tycEnv * (tyc list option * int) -> tycEnv
  
  (** the ltyEnv maps from lvar to its lty; notice lty is depth-dependent *)
--- 116,123 ----
  
  (** utility functions on tycEnv *)
! type tycEnv = Lty.tycEnv
! datatype teBinder = datatype Lty.teBinder
! val teEmpty : tycEnv
! val teCons : teBinder * tycEnv -> tycEnv
  
  (** the ltyEnv maps from lvar to its lty; notice lty is depth-dependent *)

Index: ltybasic.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltybasic.sml,v
retrieving revision 1.13.24.3
retrieving revision 1.13.24.4
diff -C2 -d -r1.13.24.3 -r1.13.24.4
*** ltybasic.sml	11 Aug 2006 20:42:23 -0000	1.13.24.3
--- ltybasic.sml	17 Aug 2006 23:13:14 -0000	1.13.24.4
***************
*** 216,224 ****
  fun lt_adj (lt, d, nd) = 
    if d = nd then lt 
!   else ltc_env(lt, 0, nd - d, LT.initTycEnv)
  
  fun tc_adj (tc, d, nd) = 
    if d = nd then tc 
!   else tcc_env(tc, 0, nd - d, LT.initTycEnv)
  
  (** The following functions are similiar to lt_adj and tc_adj;
--- 216,224 ----
  fun lt_adj (lt, d, nd) = 
    if d = nd then lt 
!   else ltc_env(lt, 0, nd - d, LT.teEmpty)
  
  fun tc_adj (tc, d, nd) = 
    if d = nd then tc 
!   else tcc_env(tc, 0, nd - d, LT.teEmpty)
  
  (** The following functions are similiar to lt_adj and tc_adj;
***************
*** 228,242 ****
      called only in lcontract.sml. *)
  local
! fun mkTycEnv (i, k, dd, e) = 
!   if i >= k then e else mkTycEnv(i+1, k, dd, LT.tcInsert(e,(NONE, dd+i)))
  
  in 
  fun lt_adj_k (lt, d, nd, k) = 
    if d = nd then lt 
!   else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.initTycEnv))
  
  fun tc_adj_k (tc, d, nd, k) = 
    if d = nd then tc 
!   else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.initTycEnv))
  
  end (* lt_adj_k and tc_adj_k *)
--- 228,244 ----
      called only in lcontract.sml. *)
  local
! fun mkTycEnv (i, k, dd, te) = 
!   if i >= k then te 
!   else mkTycEnv(i+1, k, dd, LT.teCons(LT.Lamb(dd+i,[]),te))
!   (* dbm: no ks available *)
  
  in 
  fun lt_adj_k (lt, d, nd, k) = 
    if d = nd then lt 
!   else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.teEmpty))
  
  fun tc_adj_k (tc, d, nd, k) = 
    if d = nd then tc 
!   else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.teEmpty))
  
  end (* lt_adj_k and tc_adj_k *)
***************
*** 262,269 ****
   ***************************************************************************)
  
- exception tcUnbound = LT.tcUnbound
  type tycEnv = LT.tycEnv
! val initTycEnv = LT.initTycEnv
! val tcInsert = LT.tcInsert
  
  (***************************************************************************
--- 264,271 ----
   ***************************************************************************)
  
  type tycEnv = LT.tycEnv
! datatype teBinder = datatype LT.teBinder
! val teEmpty = LT.teEmpty
! val teCons = LT.teCons
  
  (***************************************************************************
***************
*** 286,290 ****
  	  if d=nd then lt
  	  else if d > nd then bug "unexpected depth info in ltLookup"
! 	       else ltc_env(lt, 0, nd - d, LT.initTycEnv)
    (*easc*))
  
--- 288,292 ----
  	  if d=nd then lt
  	  else if d > nd then bug "unexpected depth info in ltLookup"
! 	       else ltc_env(lt, 0, nd - d, LT.teEmpty)
    (*easc*))
  

Index: ltyextern.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltyextern.sig,v
retrieving revision 1.9
retrieving revision 1.9.26.1
diff -C2 -d -r1.9 -r1.9.26.1
*** ltyextern.sig	1 Jun 2000 18:33:26 -0000	1.9
--- ltyextern.sig	17 Aug 2006 23:13:14 -0000	1.9.26.1
***************
*** 44,48 ****
  val lt_pinst    : lty * tyc list -> lty
  
! exception TkTycChk
  exception LtyAppChk
  val lt_inst_chk_gen : unit -> lty * tyc list * tkindEnv -> lty list
--- 44,48 ----
  val lt_pinst    : lty * tyc list -> lty
  
! exception TkTycChk of string (* kind checker exception *)
  exception LtyAppChk
  val lt_inst_chk_gen : unit -> lty * tyc list * tkindEnv -> lty list

Index: ltyextern.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltyextern.sml,v
retrieving revision 1.19.24.3
retrieving revision 1.19.24.4
diff -C2 -d -r1.19.24.3 -r1.19.24.4
*** ltyextern.sml	17 Aug 2006 20:54:13 -0000	1.19.24.3
--- ltyextern.sml	17 Aug 2006 23:13:14 -0000	1.19.24.4
***************
*** 44,48 ****
     in (case ((* lt_outX *) lt_out nt, ts)
          of (LT.LT_POLY(ks, b), ts) => 
!              let val nenv = LT.tcInsert(LT.initTycEnv, (SOME ts, 0))
                in map (fn x => ltc_env(x, 1, 0, nenv)) b
               end
--- 44,48 ----
     in (case ((* lt_outX *) lt_out nt, ts)
          of (LT.LT_POLY(ks, b), ts) => 
!              let val nenv = LT.teCons(LT.Beta(0,ts,ks), LT.teEmpty)
                in map (fn x => ltc_env(x, 1, 0, nenv)) b
               end
***************
*** 101,105 ****
  fun tkSel (tk, i) = 
    (case (tk_out tk)
!     of (LT.TK_SEQ ks) => (List.nth(ks, i) handle Subscript => raise TkTycChk "Invalid TC_SEQ index")
       | _ => raise TkTycChk "Projecting out of non-tyc sequence")
  
--- 101,107 ----
  fun tkSel (tk, i) = 
    (case (tk_out tk)
!     of (LT.TK_SEQ ks) => 
!        (List.nth(ks, i)
!         handle Subscript => raise TkTycChk "Invalid TC_SEQ index")
       | _ => raise TkTycChk "Projecting out of non-tyc sequence")
  
***************
*** 108,112 ****
  fun tkApp (tk, tks) = 
    (case (tk_out tk)
!     of LT.TK_FUN(a, b) => if tks_eqv(a, tks) then b else raise TkTycChk "Param/Arg Tyc Kind mismatch"
       | _ => raise TkTycChk "Application of non-TK_FUN")
  
--- 110,116 ----
  fun tkApp (tk, tks) = 
    (case (tk_out tk)
!     of LT.TK_FUN(a, b) =>
!        if tks_eqv(a, tks) then b
!        else raise TkTycChk "Param/Arg Tyc Kind mismatch"
       | _ => raise TkTycChk "Application of non-TK_FUN")
  
***************
*** 117,121 ****
    (case (tk_out tk)
      of LT.TK_FUN(a, b) =>
!        if tksSubkind(tks, a) then b else raise TkTycChk "Param/Arg Tyc Kind mismatch"
       | _ => raise TkTycChk "Application of non-TK_FUN") 
  
--- 121,126 ----
    (case (tk_out tk)
      of LT.TK_FUN(a, b) =>
!        if tksSubkind(tks, a) then b
!        else raise TkTycChk "Param/Arg Tyc Kind mismatch"
       | _ => raise TkTycChk "Application of non-TK_FUN") 
  
***************
*** 218,231 ****
  		    (* Kind check freetycs *)
                      val nk =
!                         case ts of
!                             [] => k 
!                           | _ => tkApp(k, map g ts)
                  in
                      case (tk_out nk) of
                          LT.TK_FUN(a, b) => 
                          let val arg =
!                                 case a of
!                                     [x] => x
!                                   | _ => tkc_seq a
                          in
  			    (* Kind check recursive tyc app ??*)
--- 223,236 ----
  		    (* Kind check freetycs *)
                      val nk =
!                         case ts
!                           of [] => k 
!                            | _ => tkApp(k, map g ts)
                  in
                      case (tk_out nk) of
                          LT.TK_FUN(a, b) => 
                          let val arg =
!                                 case a
!                                   of [x] => x
!                                    | _ => tkc_seq a
                          in
  			    (* Kind check recursive tyc app ??*)
***************
*** 279,284 ****
                of (LT.LT_POLY(ks, b), ts) => 
                   let val _ = ListPair.app (tkChk kenv) (ks, ts)
!                      fun h x = ltc_env(x, 1, 0,
!                                        tcInsert(initTycEnv, (SOME ts, 0)))
                   in map h b
                   end
--- 284,288 ----
                of (LT.LT_POLY(ks, b), ts) => 
                   let val _ = ListPair.app (tkChk kenv) (ks, ts)
!                      fun h x = ltc_env(x, 1, 0, teCons(Beta(0,ts,ks),teEmpty))
                   in map h b
                   end
***************
*** 295,302 ****
            if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
            else if abslevel > 0 then 
!                  h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
                 else bug "unexpected cases in ltAdjSt"
  
!         val btenv = tcInsert(initTycEnv, (SOME ts, 0))
          val nt = h(dist, 1, bnl, btenv)
       in nt (* was lt_norm nt *)
--- 299,306 ----
            if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
            else if abslevel > 0 then 
!                  h(abslevel-1, ol+1, nl+1, teCons(Lamb(nl,ks (* dbm ??? *)), tenv))
                 else bug "unexpected cases in ltAdjSt"
  
!         val btenv = teCons(Beta(0,ts,ks (* dbm ??? *)),teEmpty)
          val nt = h(dist, 1, bnl, btenv)
       in nt (* was lt_norm nt *)
***************
*** 308,315 ****
            if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
            else if abslevel > 0 then 
!                  h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
                 else bug "unexpected cases in tcAdjSt"
  
!         val btenv = tcInsert(initTycEnv, (SOME ts, 0))
          val nt = h(dist, 1, bnl, btenv)
       in nt (* was tc_norm nt *)
--- 312,319 ----
            if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
            else if abslevel > 0 then 
!                  h(abslevel-1, ol+1, nl+1, teCons(Lamb(nl,ks (* dbm ??? *)), tenv))
                 else bug "unexpected cases in tcAdjSt"
  
!         val btenv = teCons(Beta(0,ts,ks (* dbm ??? *)), teEmpty)
          val nt = h(dist, 1, bnl, btenv)
       in nt (* was tc_norm nt *)
***************
*** 321,327 ****
            if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
            else if abslevel > 0 then
!                  h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
                 else bug "unexpected cases in ltSinkSt"
!         val nt = h(nd-d, 0, 1, initTycEnv)
       in nt (* was lt_norm nt *)
      end
--- 325,331 ----
            if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
            else if abslevel > 0 then
!                  h(abslevel-1, ol+1, nl+1, teCons(Lamb(nl,ks (* dbm ??? *)), tenv))
                 else bug "unexpected cases in ltSinkSt"
!         val nt = h(nd-d, 0, 1, teEmpty)
       in nt (* was lt_norm nt *)
      end
***************
*** 332,338 ****
            if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
            else if abslevel > 0 then
!                  h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
                 else bug "unexpected cases in ltSinkSt"
!         val nt = h(nd-d, 0, 1, initTycEnv)
       in nt (* was tc_norm nt *)
      end
--- 336,342 ----
            if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
            else if abslevel > 0 then
!                  h(abslevel-1, ol+1, nl+1, teCons(Lamb(nl,ks), tenv))
                 else bug "unexpected cases in ltSinkSt"
!         val nt = h(nd-d, 0, 1, teEmpty)
       in nt (* was tc_norm nt *)
      end
***************
*** 630,634 ****
          (* encode the lty and depth info using LT_ENV
           * (only first 2 args are useful) *)
!         val ltydepth = lt_inj (LT.LT_ENV (lty, d, 0, LT.initTycEnv))
      in
          case LtDict.find(!dict, ltydepth) of
--- 634,638 ----
          (* encode the lty and depth info using LT_ENV
           * (only first 2 args are useful) *)
!         val ltydepth = lt_inj (LT.LT_ENV (lty, d, 0, LT.teEmpty))
      in
          case LtDict.find(!dict, ltydepth) of
***************
*** 902,906 ****
          (* encode the lty and depth info using LT_ENV
           * (only first 2 args are useful) *)
!         val ltydepth = lt_inj (LT.LT_ENV (lty, d, 0, LT.initTycEnv))
      in
          case LtDict.find(!dict, ltydepth) of
--- 906,910 ----
          (* encode the lty and depth info using LT_ENV
           * (only first 2 args are useful) *)
!         val ltydepth = lt_inj (LT.LT_ENV (lty, d, 0, LT.teEmpty))
      in
          case LtDict.find(!dict, ltydepth) of

Index: ltykernel.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltykernel.sml,v
retrieving revision 1.18.12.17
retrieving revision 1.18.12.18
diff -C2 -d -r1.18.12.17 -r1.18.12.18
*** ltykernel.sml	17 Aug 2006 21:55:48 -0000	1.18.12.17
--- ltykernel.sml	17 Aug 2006 23:13:14 -0000	1.18.12.18
***************
*** 50,56 ****
              val neweff = 
                if i > ol then (ol <> nl)
!               else (* case tcLookup(i, tenv)
!                        of (NONE, n) => (nl - n) <> i
!                         | (SOME ts, n) =>
                               (let val y = List.nth(ts, j)
                                 in (case tc_outX y
--- 50,57 ----
              val neweff = 
                if i > ol then (ol <> nl)
!               else true
!                   (* case teLookup(i, tenv)
!                        of SOME(Lamb(n,_)) => (nl - n) <> i
!                         | SOME(Beta(n,ts,_)) =>
                               (let val y = List.nth(ts, j)
                                 in (case tc_outX y
***************
*** 58,62 ****
                                          ((nj <> j) orelse ((ni+nl-n) <> i))
                                       | _ => true)
!                               end) *) true
           in neweff orelse (withEff(r, ol, nl, tenv))
          end
--- 59,63 ----
                                          ((nj <> j) orelse ((ni+nl-n) <> i))
                                       | _ => true)
!                               end) *)
           in neweff orelse (withEff(r, ol, nl, tenv))
          end
***************
*** 64,93 ****
  
  fun tcc_env(x, ol, nl, tenv) =
!   (let fun checkTCVAR tyc = case (tc_outX tyc) of
!        TC_VAR(i,j) => (case teLookup(tenv, i) 
! 			of SOME(Beta(j, tcs, _)) => 
! 			   if j >= length tcs 
! 			   then (print "tcc_env TC_VAR ";
! 				 print (Int.toString j);
! 				 print "B tcs length ";
! 				 print (Int.toString (length tcs));
! 				 raise Fail "Bad TC_ENV TC_VAR")
! 			   else ()
! 			 | SOME(Lamb(j)) => 
! 			   print "TC_VAR referencing LAMB"
! 			 | _ => ())
!      | TC_ENV(tc, _, _, _)  => (print "TC_ENV("; 
! 				checkTCVAR(tc); 
! 				print ")\n")
!      | _ => () (* print ("tcc_env OTHER " ^ tci_print tci ^"\n") *) 
     in checkTCVAR(x); 
!     let val tvs = tc_vs x
!    in case tvs
!        of NONE => tcc_env_int(x, ol, nl, tenv)
!         | SOME [] => x
!         | SOME nvs => if withEff(nvs, ol, nl, tenv) 
!                       then tcc_env_int(x, ol, nl, tenv)
!                       else x 
!     end
     end)
  
--- 65,105 ----
  
  fun tcc_env(x, ol, nl, tenv) =
!   (let fun checkTCVAR tyc =  (* GK -- debugging *)
!            case (tc_outX tyc)
!              of TC_VAR(i,j) =>
!                  (case teLookup(tenv,i)
! 		   of SOME(Beta(_,ts,ks)) =>
!                         if j >= length ts
! 			then (print "tcc_env TC_VAR ";
! 			      print (Int.toString j);
! 			      print ", ts length = ";
! 			      print (Int.toString (length ts));
!                               print "\n";
! 			      raise Fail "Bad TC_ENV TC_VAR")
! 			else ()
!                     | SOME(Lamb(_,ks)) =>
!                         if j >= length ks
! 			then (print "tcc_env TC_VAR ";
! 			      print (Int.toString j);
! 			      print ", ks length = ";
! 			      print (Int.toString (length ks));
!                               print "\n";
! 			      raise Fail "Bad TC_ENV TC_VAR")
! 			else ()
! 		    | NONE => (print "tcc_env TC_VAR: i out of bounds: ";
!                                print (Int.toString i); print "\n"))
!               | TC_ENV(tc, _, _, _)  =>
!                  (print "TC_ENV("; checkTCVAR(tc); print ")\n")
!               | _ => () (* print ("tcc_env OTHER " ^ tci_print tci ^"\n") *) 
     in checkTCVAR(x); 
!    (* original body --- *)
!    let val tvs = tc_vs x
!     in case tvs
!         of NONE => tcc_env_int(x, ol, nl, tenv)
!          | SOME [] => x
!          | SOME nvs => if withEff(nvs, ol, nl, tenv) 
!                        then tcc_env_int(x, ol, nl, tenv)
!                        else x 
!    end
     end)
  
***************
*** 184,190 ****
  val flatten_limit = 9  
  
! (* tcUnbound2 -- raised when second index of a deBruijn index pair is
   * out of bounds *)
! exception tcUnbound2
  
  fun isKnown tc = 
--- 196,202 ----
  val flatten_limit = 9  
  
! (* teUnbound2 -- raised when second index of a deBruijn index pair is
   * out of bounds *)
! exception teUnbound2
  
  fun isKnown tc = 
***************
*** 266,275 ****
                    of TC_VAR (n,k) => 
                         if (n <= ol) then  (* n is bound in tenv *)
!                          (case teLookup(tenv, n) 
!                            of SOME(Lamb(nl', _)) => 
! 			        tcc_var(nl - nl', k) (* rule r5 *)
!                             | SOME(Beta(nl', ts, _)) =>  
!                                  let val y = List.nth(ts, k) 
!                                              handle Subscript => 
                      (with_pp(fn s =>
                         let val {break,newline,openHVBox,openHOVBox,
--- 278,288 ----
                    of TC_VAR (n,k) => 
                         if (n <= ol) then  (* n is bound in tenv *)
!                          (case teLookup(tenv, n)
!                            of NONE => bug "tc_lzrd: short tenv"
!                             | SOME(Lamb(nl',ks)) =>   (* rule r5 *)
!                                 tcc_var(nl - nl', k)
!                             | SOME(Beta(nl',ts,ks)) =>  (* rule r6 *)
!                                 let val y = List.nth(ts, k) 
!                                             handle Subscript => (* kind error! *)
                      (with_pp(fn s =>
                         let val {break,newline,openHVBox,openHOVBox,
***************
*** 290,305 ****
                            newline(); PP.flushStream s
  			end);
! 			raise tcUnbound2)
                                   in h(y, 0, nl - nl', teEmpty)  (* rule r6 *)
!                                  end
! 			(* Could not find TV(n,_) in tenv 
! 			   and ol = length tenv invariant 
! 			   failed! *)
! 			    | NONE => raise tcUnbound) 
                         else tcc_var(n-ol+nl, k) (* rule r4 *)
                     | TC_NVAR _ => x
                     | TC_PRIM _ => x    (* rule r7 *)
                     | TC_FN (ks, tc) => 
!                       let val tenv' = teCons(Lamb(nl, ks), tenv)
                         in tcc_fn(ks, 
  				 tcc_env(tc, ol+1, nl+1, tenv') 
--- 303,314 ----
                            newline(); PP.flushStream s
  			end);
! 			raise teUnbound2)
                                   in h(y, 0, nl - nl', teEmpty)  (* rule r6 *)
!                                  end)
                         else tcc_var(n-ol+nl, k) (* rule r4 *)
                     | TC_NVAR _ => x
                     | TC_PRIM _ => x    (* rule r7 *)
                     | TC_FN (ks, tc) => 
!                       let val tenv' = teCons(Lamb(nl,ks),tenv)
                         in tcc_fn(ks, 
  				 tcc_env(tc, ol+1, nl+1, tenv') 
***************
*** 347,351 ****
                     | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2)
                     | LT_POLY (ks, ts) => 
!                        let val tenv' = teCons(Lamb (nl, ks), tenv)
                          in ltc_poly(ks, 
                               map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts)
--- 356,360 ----
                     | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2)
                     | LT_POLY (ks, ts) => 
!                        let val tenv' = teCons(Lamb(nl,ks), tenv)
                          in ltc_poly(ks, 
                               map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts)
***************
*** 405,443 ****
         of TC_APP(tc, tcs) =>
  	    ((* print "\ntc_whnm: TC_APP\n"; *)
!             (let val tc' = tc_whnm tc 
! 		     handle Fail _ => raise Fail "TC_APP in tc_whnm 1"
                in case (tc_outX tc')
                    of TC_FN(ks, b) =>  
                         let fun base () = 
!                              (b, 1, 0, teCons(Beta(0, tcs, ks), teEmpty))
                             val sp = 
                               (case tc_outX b
                                 of TC_ENV(b', ol', nl', te') => 
                                      (case teDest te'
!                                       of SOME(Lamb(n, ks'), te) =>
!                                          if (n = nl'-1) andalso (ol' > 0)
!                                          then (b', ol', n, 
!                                                teCons(Beta(n, tcs, ks),
! 						      te))
! 					      (* Which ks correspond to
! 					         this Beta? *)
!                                          else base()
                                         | _ => base())
                                  | _ => base()) 
                             val res = tc_whnm(tcc_env sp) 
! 			             handle Fail _ => 
! 					    raise Fail "TC_APP in tc_whnm 2" 
                          in tyc_upd(nt, res); res
                         end
                     | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) =>
                         bug "unexpected tycs in tc_whnm-TC_APP"
!                    | _ => let val xx = tcc_app(tc', tcs) 
!                            in stripInd xx
!                           end
!              end))
          | TC_PROJ(tc, i) =>
! 	   ((* print "\ntc_whnm: TC_PROJ\n"; *) 
! 	   (let val tc' = tc_whnm tc
!               in (case (tc_outX tc')
                     of (TC_SEQ tcs) => 
                          let val res = List.nth(tcs, i)
--- 414,449 ----
         of TC_APP(tc, tcs) =>
  	    ((* print "\ntc_whnm: TC_APP\n"; *)
!              let val tc' = tc_whnm tc
!                            handle Fail _ =>
!                                   raise Fail "TC_APP in tc_whnm 1"
                in case (tc_outX tc')
                    of TC_FN(ks, b) =>  
                         let fun base () = 
!                              (b, 1, 0, teCons(Beta(0,tcs,ks),teEmpty))  (* r1 *)
                             val sp = 
                               (case tc_outX b
                                 of TC_ENV(b', ol', nl', te') => 
                                      (case teDest te'
!                                       of SOME(Lamb(n,ks'), te) =>
!                                            if (n = nl'-1) andalso (ol' > 0)
!                                            then (* r12 *)
!                                              (b', ol', n, teCons(Beta(n,tcs,ks),te))
!                                            else base()
!                                            (* dbm: ks and ks' should be the same *)
                                         | _ => base())
                                  | _ => base()) 
                             val res = tc_whnm(tcc_env sp) 
! 			             handle Fail _ =>
!                                             raise Fail "TC_APP in tc_whnm 2" 
                          in tyc_upd(nt, res); res
                         end
                     | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) =>
                         bug "unexpected tycs in tc_whnm-TC_APP"
!                    | _ => stripInd(tcc_app(tc', tcs))
!              end)
          | TC_PROJ(tc, i) =>
! 	    ((* print "\ntc_whnm: TC_PROJ\n"; *) 
! 	     let val tc' = tc_whnm tc
!               in case (tc_outX tc')
                     of (TC_SEQ tcs) => 
                          let val res = List.nth(tcs, i)
***************
*** 450,457 ****
                         (TC_IND _) | (TC_TUPLE _)) =>
                           bug "unexpected tycs in tc_whnm-TC_PROJ"
!                     | _ => let val xx = tcc_proj(tc', i)
!                             in stripInd xx
!                            end)
!              end))
          | TC_TOKEN(k, tc)  =>
  	    ((* print "\ntc_whnm: TC_TOKEN\n"; *)
--- 456,461 ----
                         (TC_IND _) | (TC_TUPLE _)) =>
                           bug "unexpected tycs in tc_whnm-TC_PROJ"
!                     | _ => stripInd(tcc_proj(tc', i))
!              end)
          | TC_TOKEN(k, tc)  =>
  	    ((* print "\ntc_whnm: TC_TOKEN\n"; *)


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