CVS: sml-dist/src/compiler/FLINT/kernel lty.sig, 1.1.2.6, 1.1.2.7 lty.sml, 1.1.2.11, 1.1.2.12 ltyextern.sig, 1.9.26.2, 1.9.26.3 ltyextern.sml, 1.19.24.8, 1.19.24.9

David MacQueen <[email protected]> Fri, 18 Aug 2006 15:58:49 -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-serv12356/src/compiler/FLINT/kernel

Modified Files:
      Tag: primop-branch-2
	lty.sig lty.sml ltyextern.sig ltyextern.sml 
Log Message:
adding kind checking to chkplexp.sml

Index: lty.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/Attic/lty.sig,v
retrieving revision 1.1.2.6
retrieving revision 1.1.2.7
diff -C2 -d -r1.1.2.6 -r1.1.2.7
*** lty.sig	18 Aug 2006 20:55:00 -0000	1.1.2.6
--- lty.sig	18 Aug 2006 22:58:46 -0000	1.1.2.7
***************
*** 191,194 ****
--- 191,195 ----
  val tkTycGen : unit -> (tkindEnv -> tyc -> tkind)
  val tkChkGen : unit -> (tkindEnv -> (tkind * tyc) -> unit)
+ val ltyChkGen : unit -> (tkindEnv -> lty -> tkind)
  
  end (* signature LTY *)

Index: lty.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/Attic/lty.sml,v
retrieving revision 1.1.2.11
retrieving revision 1.1.2.12
diff -C2 -d -r1.1.2.11 -r1.1.2.12
*** lty.sml	18 Aug 2006 21:19:55 -0000	1.1.2.11
--- lty.sml	18 Aug 2006 22:58:46 -0000	1.1.2.12
***************
*** 22,34 ****
  (* Type lambda bindings (TC_FN) bind several variables at a time,
   * i.e. they are n-ary for some n, with each type variable given a kind.
!  * A type variable is represented by a pair (d,i), where d is a
   * 1-based deBruijn index designating a lambda binder by its lambda
!  * nesting level, counting inside out, and i is a 0-based index
!  * into a list of the type variables bound by the corresponding binder.
!  * These (d,i) pairs are encoded into a single integer by tvEncode,
   * and the pair can be recovered from its encoding by tvDecode. *)
  
  type enc_tvar = int 
! fun tvEncode (d, i) = d * MVAL + i
  fun tvDecode x = ((x div MVAL), (x mod MVAL))
  
--- 22,34 ----
  (* Type lambda bindings (TC_FN) bind several variables at a time,
   * i.e. they are n-ary for some n, with each type variable given a kind.
!  * A type variable is represented by a pair (d,k), where d is a
   * 1-based deBruijn index designating a lambda binder by its lambda
!  * nesting level, counting inside out, and k is a 0-based index
!  * into the list of the type variables bound by that binder.
!  * These (d,k) pairs are encoded into a single integer by tvEncode,
   * and the pair can be recovered from its encoding by tvDecode. *)
  
  type enc_tvar = int 
! fun tvEncode (d, k) = d * MVAL + k
  fun tvDecode x = ((x div MVAL), (x mod MVAL))
  
***************
*** 44,49 ****
  (* definitions of named tyc variables.
     for now, these share the same namespace with lvars. *)
! (* [KM ???] Are these used at all? *)
! type tvar = LambdaVar.lvar
  val mkTvar = LambdaVar.mkLvar
  
--- 44,51 ----
  (* definitions of named tyc variables.
     for now, these share the same namespace with lvars. *)
! (* [KM ???] Are these used at all? Yes, they are used after
!  * translation into the flint language(?). Are these the
!  * "run-time" type parameters? *)
! type tvar = LambdaVar.lvar (* = int = enc_tvar *)
  val mkTvar = LambdaVar.mkLvar
  
***************
*** 51,64 ****
     into a single integer using tvEncode/tvDecode, named variables use
     the tvar as an integer.  The deBruijn-indexed list is kept sorted,
!    the named variables are in arbitrary order (for now) --league, 2 July 1998
   *)
  datatype aux_info
!   = AX_REG of bool                      (* normalization flag *)
!             * enc_tvar list             (* free debruijn-indexed type vars *)
!             * tvar list                 (* free named type vars *)
!   | AX_NO                               (* no aux_info available *)
  
  (* these two are originally from SortedList -- which I wanted to get
   * rid off.  -- Matthias  11/2000 *)
  fun mergeTvs (l : tvar list, []) = l
    | mergeTvs ([], l) = l
--- 53,72 ----
     into a single integer using tvEncode/tvDecode, named variables use
     the tvar as an integer.  The deBruijn-indexed list is kept sorted,
!    the named variables are in arbitrary order (for now) --league, 2 July 1998.
! 
!    [DBM,8/18/06]: but the mergeTvs function below is used to merge both
!    enc_tvar (deBruijn) and tvar lists, and it assumes its argument lists
!    are sorted. 
   *)
  datatype aux_info
!   = AX_REG of bool           (* normalization flag *)
!             * enc_tvar list  (* free debruijn-indexed type vars, sorted *)
!             * tvar list      (* free named type vars, sorted? *)
!   | AX_NO                    (* no aux_info available *)
  
  (* these two are originally from SortedList -- which I wanted to get
   * rid off.  -- Matthias  11/2000 *)
+ (* mergeTvs: tvar list * tvar list -> tvar list
+  * merge two sorted lists of tvars into a sorted list, eliminating duplicates *)
  fun mergeTvs (l : tvar list, []) = l
    | mergeTvs ([], l) = l
***************
*** 68,78 ****
        else h' :: mergeTvs (l, t')
  
  fun fmergeTvs [] = []
!   | fmergeTvs (h :: t) = 
!     let fun loop ([], a) = a
! 	  | loop (h :: t, a) = loop (t, mergeTvs (h, a))
!     in
! 	loop (t, h)
!     end
  
  (*
--- 76,84 ----
        else h' :: mergeTvs (l, t')
  
+ (* fmergeTvs : tvar list list -> tvar list
+  * merge a list of sorted lists of tvars into a single sorted list,
+  * eliminating duplicates. *)
  fun fmergeTvs [] = []
!   | fmergeTvs (h :: t) = foldr mergeTvs h t
  
  (*
***************
*** 276,291 ****
          if ai < bi then LESS 
          else if ai > bi then GREATER
!            else if a = b then EQUAL
!                 else let val index = wtoi (andb(itow ai,itow(N-1)))
!                          fun g [] = bug "unexpected case in cmp"
!                            | g (w::rest) =
!                                  (case Weak.strong w
!                                    of SOME r => 
!                                         if a=r then LESS 
!                                         else if b=r then GREATER
!                                                     else g rest
!                                     | NONE => g rest)
!                       in g(Array.sub(table,index))
!                      end
  
  
--- 282,299 ----
          if ai < bi then LESS 
          else if ai > bi then GREATER
!         else if a = b then EQUAL (* pointer equality on refs *)
!         else (* ai = bi, so a,b in same bucket of table, use order
!               * a and b appear in the bucket *)
!              let val index = wtoi (andb(itow ai,itow(N-1)))
!                  fun g [] = bug "unexpected case in cmp"
!                    | g (w::rest) =
!                      (case Weak.strong w
!                        of SOME r => 
!                           if a=r then LESS 
!                           else if b=r then GREATER
!                           else g rest
!                         | NONE => g rest)
!               in g(Array.sub(table,index))
!              end
  
  
***************
*** 543,551 ****
        | SOME(binder, tenvRest) => binder::(teToBinders tenvRest)
  
! (* TeUnbound -- raised when first element of a deBruijn index is 
!  * out of bounds *)
! exception TeUnbound
! 
! (* 1-based index lookup: assume i >= 1 *)
  fun teLookup(tenv : tycEnv, i: int) : teBinder option =
        (case teDest tenv
--- 551,556 ----
        | SOME(binder, tenvRest) => binder::(teToBinders tenvRest)
  
! (* teLookup: tenv * int -> teBinder option
!  * 1-based index lookup: assume i >= 1, return NONE if i > "length" of tenv *)
  fun teLookup(tenv : tycEnv, i: int) : teBinder option =
        (case teDest tenv
***************
*** 695,698 ****
--- 700,705 ----
  fun tks_eqv (ks1, ks2) = tk_eq(tkc_seq ks1, tkc_seq ks2)
  
+ (* this is superceded by the following redefinition using tksSubkind
+  * instead of tks_eqv.  Does it make any difference? If so, example? *)
  fun tkApp (tk, tks) = 
    (case (tk_outX tk)
***************
*** 701,704 ****
--- 708,712 ----
         else raise TkTycChk "Param/Arg Tyc Kind mismatch"
       | _ => raise TkTycChk "Application of non-TK_FUN")
+ *)
  
  (* check the application of tycs of kinds `tks' to a type function of
***************
*** 734,741 ****
  struct
      structure TcDict = RedBlackMapFn
!                            (struct
!                                type ord_key = tyc
!                                val compare = tc_cmp
!                            end)
  
      type dict = (tkind * tkind) list TcDict.map ref
--- 742,749 ----
  struct
      structure TcDict = RedBlackMapFn
!                          (struct
!                             type ord_key = tyc
!                             val compare = tc_cmp
!                           end)
  
      type dict = (tkind * tkind) list TcDict.map ref
***************
*** 746,751 ****
           * in kenv? *)
          (* (might not be available for some tycs) *)
!         case tkLookupFreeVars (kenv, tyc) of
!             SOME ks_fvs => let
                  (* encode those as a kind sequence *)
                  val k_fvs = tkc_seq ks_fvs
--- 754,760 ----
           * in kenv? *)
          (* (might not be available for some tycs) *)
!         case tkLookupFreeVars (kenv, tyc)
!           of SOME ks_fvs =>
!              let
                  (* encode those as a kind sequence *)
                  val k_fvs = tkc_seq ks_fvs
***************
*** 820,825 ****
--- 829,838 ----
                                    of [x] => x
                                     | _ => tkc_seq a
+                               (* "sequencize" the domain to make it comparable
+                                * to b *)
                          in
  			    (* Kind check recursive tyc app ??*)
+                             (* [KM ???] seems bogus if arg is a proper subkind,
+                              * but probably ok if tkSubkind is really equivalence *)
                              if tkSubkind(arg, b) then (* order? *)
                                  (if n = 1 then b else tkSel(arg, i))
***************
*** 911,959 ****
  
  
! fun ltyChk (lty : lty) =
!     let val (tkChk, chkKindEnv) = tkTycGen'()
! 	fun ltyIChk (kenv : tkindEnv) (ltyI : ltyI) =
! 	    (case ltyI 
! 	      of LT_TYC(tyc) => 
! 		   (tkAssertIsMono (tkChk kenv tyc); tkc_mono)
! 	       | LT_STR(ltys) => tkc_seq(map (ltyChk' kenv) ltys)
! 	       | LT_FCT(paramLtys, rngLtys) => 
! 		   let val paramks = map (ltyChk' kenv) paramLtys
! 		       val tenv' = paramks :: kenv
! 		   in 
! 		       tkc_fun(paramks,
! 			      tkc_seq(map (ltyChk' tenv') rngLtys))
! 		   end
! 	       | LT_POLY(ks, ltys) => 
! 		   tkc_seq(map (ltyChk' (ks::kenv)) ltys)
! 		   (* ??? *)
! 	       | LT_CONT(ltys) => 
! 		   tkc_seq(map (ltyChk' kenv) ltys)
! 	       | LT_IND(newLty, oldLtyI) =>
! 		   let val newLtyKnd = (ltyChk' kenv) newLty
! 		   in if tk_eq(newLtyKnd, ltyIChk kenv oldLtyI)
! 		      then newLtyKnd
! 		      else bug "ltyChk[IND]: kind mismatch"
! 		   end
! 	       | LT_ENV(body, i, j, env) =>
! 		   (* Should be the same as checking TC_ENV and 
! 		    * therefore the two cases should probably just
! 		    * call the same helper function *)
! 		   (let val kenv' = 
! 			    List.drop(kenv, j)
! 			    handle Subscript => 
! 				   bug "[Env]: dropping too many frames"
! 			fun bindToKinds(Lamb(_,ks)) = ks
! 			  | bindToKinds(Beta(_,_,ks)) = ks
! 			fun addBindToKEnv(b,ke) = 
! 			    bindToKinds b :: ke
! 			val bodyKenv = 
! 			    foldr addBindToKEnv kenv' (teToBinders env)
! 		    in chkKindEnv(env,j,kenv);
! 		       ltyChk' bodyKenv body
! 		    end))
! 	and ltyChk' kenv lty = ltyIChk kenv (lt_outX lty)
!     in ltyChk' [] lty
!     end (* function ltyChk *)	   
  end (* local *)
  		   
--- 924,973 ----
  
  
! fun ltyChkGen () = 
! let val (tkChk, chkKindEnv) = tkTycGen'()
!     fun ltyIChk (kenv : tkindEnv) (ltyI : ltyI) =
!         (case ltyI 
!           of LT_TYC(tyc) => 
!                (tkAssertIsMono (tkChk kenv tyc); tkc_mono)
!            | LT_STR(ltys) => tkc_seq(map (ltyChk' kenv) ltys)
!            | LT_FCT(paramLtys, rngLtys) => 
!                let val paramks = map (ltyChk' kenv) paramLtys
!                    val tenv' = paramks :: kenv
!                in 
!                    tkc_fun(paramks,
!                           tkc_seq(map (ltyChk' tenv') rngLtys))
!                end
!            | LT_POLY(ks, ltys) => 
!                tkc_seq(map (ltyChk' (ks::kenv)) ltys)
!                (* ??? *)
!            | LT_CONT(ltys) => 
!                tkc_seq(map (ltyChk' kenv) ltys)
!            | LT_IND(newLty, oldLtyI) =>
!                let val newLtyKnd = (ltyChk' kenv) newLty
!                in if tk_eq(newLtyKnd, ltyIChk kenv oldLtyI)
!                   then newLtyKnd
!                   else bug "ltyChk[IND]: kind mismatch"
!                end
!            | LT_ENV(body, i, j, env) =>
!                (* Should be the same as checking TC_ENV and 
!                 * therefore the two cases should probably just
!                 * call the same helper function *)
!                (let val kenv' = 
!                         List.drop(kenv, j)
!                         handle Subscript => 
!                                bug "[Env]: dropping too many frames"
!                     fun bindToKinds(Lamb(_,ks)) = ks
!                       | bindToKinds(Beta(_,_,ks)) = ks
!                     fun addBindToKEnv(b,ke) = 
!                         bindToKinds b :: ke
!                     val bodyKenv = 
!                         foldr addBindToKEnv kenv' (teToBinders env)
!                 in chkKindEnv(env,j,kenv);
!                    ltyChk' bodyKenv body
!                 end))
!     and ltyChk' kenv lty = ltyIChk kenv (lt_outX lty)
!  in ltyChk'
! end (* function ltyChk *)	   
! 
  end (* local *)
  		   

Index: ltyextern.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltyextern.sig,v
retrieving revision 1.9.26.2
retrieving revision 1.9.26.3
diff -C2 -d -r1.9.26.2 -r1.9.26.3
*** ltyextern.sig	18 Aug 2006 17:28:28 -0000	1.9.26.2
--- ltyextern.sig	18 Aug 2006 22:58:46 -0000	1.9.26.3
***************
*** 49,52 ****
--- 49,58 ----
   *) 
  
+ (* kind checking functions (re-exported here from Lty) *)
+ val tkTycGen : unit -> (tkindEnv -> tyc -> tkind)
+ val tkChkGen : unit -> (tkindEnv -> (tkind * tyc) -> unit)
+ val ltyChkGen : unit -> (tkindEnv -> lty -> tkind)
+ 
+ (* perform polytype instantiation with kind checking *)
  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.8
retrieving revision 1.19.24.9
diff -C2 -d -r1.19.24.8 -r1.19.24.9
*** ltyextern.sml	18 Aug 2006 20:55:00 -0000	1.19.24.8
--- ltyextern.sml	18 Aug 2006 22:58:46 -0000	1.19.24.9
***************
*** 314,317 ****
--- 314,318 ----
  val tkTycGen : unit -> (tkindEnv -> tyc -> tkind) = LT.tkTycGen
  val tkChkGen : unit -> (tkindEnv -> (tkind * tyc) -> unit) = LT.tkChkGen
+ val ltyChkGen : unit -> (tkindEnv -> lty -> tkind) = LT.ltyChkGen
      
  (* lty application with kind-checking (exported) *)


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