CVS: sml-dist/src/compiler/FLINT/kernel lty.sig, 1.1.2.2, 1.1.2.3 lty.sml, 1.1.2.3, 1.1.2.4
David MacQueen <[email protected]> Thu, 17 Aug 2006 13:36:51 -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-serv25080
Modified Files:
Tag: primop-branch-2
lty.sig lty.sml
Log Message:
new representation and interface for tycEnv
Index: lty.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/Attic/lty.sig,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -C2 -d -r1.1.2.2 -r1.1.2.3
*** lty.sig 15 Aug 2006 23:01:31 -0000 1.1.2.2
--- lty.sig 17 Aug 2006 20:36:49 -0000 1.1.2.3
***************
*** 38,48 ****
type tycEnv
! (* tycEnvElem: the tyc list is the set of arguments bound at an application,
! * if the tycEnv element was the result of a lazy beta-reduction (SOME case),
! * or NONE if the tycEnv element is the result of pushing a suspended subst
! * through a lambda abstraction. The int is the original lambda depth of the
! * arguments (SOME case) or of the lambda abstraction.
*)
! type tycEnvElem = (tyc list option * int)
(* token: a hook to add new tyc *)
--- 38,72 ----
type tycEnv
! (* tycEnvs are represented by an encoding as tycs. The abstract representation
! * of tycEnvs would be given by:
! *
! * datatype teBinder
! * = Beta of int * tyc list * tkind list
! * | Lamb of int * tkind list
! *
! * type tycEnv = teBinder list
! *
! * Invariant: a tycEnv cannot terminate with a Lamb, i.e. the last binder
! * in a tycEnv must be a Beta. tycEnvs are created when a closure is created
! * when reducing a beta-redex (rule r1), and they are always initially of
! * of the form Beta(0,args,ks)::nil.
*)
!
! datatype teBinder
! = Beta of int * tyc list * tkind list
! (* Beta(j,args,ks):
! created when reducing a beta redex (r1);
! j: the embedding level of the original redex -- 0 if the redex was
! created by r1, or the nesting level of the new closure if by r12;
! args: the tycs bound by the n-ary beta reduction, i.e. the arguments;
! ks: the operator domain kinds *)
! | Lamb of int * tkind list
! (* Lamb(j,ks):
! created when pushing a closure (Env) through a lambda (r10);
! j: the nesting level of the closure just before r10 is applied,
! i.e. the nesteing level of the abstraction relative to the
! point where the closure was originally created;
! ks: the kinds of the abstraction parameters *)
!
(* token: a hook to add new tyc *)
***************
*** 114,134 ****
(** utility functions on tycEnv *)
- (* values returned by lookupTycEnv *)
- datatype tycEnvElem
- = B of tkind list * tyc list
- | L of tkind list * int
-
- (* components of a tycEnv *)
- datatype tycEnvComp
- = TEempty
- | TEbind of tkind list * tyc list
- | TElam of tkind list * int * tycEnv
! exception UnboundTycEnv
! val emptyTycEnv : tycEnv
! val lookupTycEnv : tycEnv * int -> tycEnvElem
! val bindTycEnv : tkind list * tyc list -> tycEnv
! val lamTycEnv : tkind list * int * tycEnv -> tycEnv
! val splitTycEnv : tycEnv -> tycEnvComp
(** utility functions on tkindEnv *)
--- 138,146 ----
(** utility functions on tycEnv *)
! val teEmpty : tycEnv
! val teLookup : tycEnv * int -> teBinder option
! val teCons : teBinder * tycEnv -> tycEnv
! val teDest : tycEnv -> (teBinder * tycEnv) option
(** utility functions on tkindEnv *)
Index: lty.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/Attic/lty.sml,v
retrieving revision 1.1.2.3
retrieving revision 1.1.2.4
diff -C2 -d -r1.1.2.3 -r1.1.2.4
*** lty.sml 16 Aug 2006 23:25:03 -0000 1.1.2.3
--- lty.sml 17 Aug 2006 20:36:49 -0000 1.1.2.4
***************
*** 147,158 ****
*)
- (* tycEnvElem: the tyc list is the set of arguments bound at an application,
- * if the tycEnv element was the result of a lazy beta-reduction (SOME case),
- * or NONE if the tycEnv element is the result of pushing a suspended subst
- * through a lambda abstraction. The int is the original lambda depth of the
- * arguments (SOME case) or of the lambda abstraction.
- *)
- type tycEnvElem = (tyc list option * int)
-
(** definitions of lambda types *)
datatype ltyI
--- 147,150 ----
***************
*** 478,531 ****
***************************************************************************)
! (* virtual tycEnv datatype
! * datatype tycEnv
! * = Empty
! * | B of tkind list * tyc list
! * | L of tkind list * int * tycEnv
*)
! (** utility functions for manipulating the tycEnv **)
! val emptyTycEnv : tycEnv = tc_injX(TC_SUM[])
! fun bindTycEnv (ks: tkind list, tycs : tyc list): tycEnv =
! tc_injX(TC_FN(ks,TC_SEQ tycs))
! fun lamTycEnv (ks: tkind list, j: int, tenv: tycEnv) : tycEnv =
! tc_injX(TC_PROJ(TC_FN(ks,tenv),j))
! (* TycEnvUnbound -- raised when first element of a deBruijn index is
! * out of bounds *)
! exception UnboundTycEnv
! datatype tycEnvElem
! = B of tkind list * tyc list
! | L of tkind list * int
! (* 1-based index lookup *)
! fun lookupTycEnv(tenv : tycEnv, i) : tycEnvElem =
! if i > 1 then
! (case tc_outX tenv
! of TC_PROJ(TC_FN(_,tenv),_) => lookupTycEnv(tenv,i-1) (* L *)
! | TC_SUM _ | TC_PROJ _ => raise UnboundTycEnv (* Empty or B *)
! | _ => bug "unexpected tycEnv in tycEnvLookup")
! else if i = 1 then
! (case tc_outX tenv
! of TC_FN(ks,TC_SEQ(tycs)) => B(ks,tycs) (* Bind *)
! | TC_PROJ(TC_FN(ks,_,),j) => L(ks,j) (* Lam *)
! | TC_SUM _ => raise UnboundTycEnv (* Empty *)
! | _ => bug "unexpected tycEnv in tycEnvLookup")
! else bug "index 0 in tycEnvLookup"
! datatype tycEnvComp
! = TEempty
! | TEbind of tkind list * tyc list
! | TElam of tkind list * int * tycEnv
! fun splitTycEnv(tenv : tycEnv) : tycEnvComp =
! (case tc_outX tenv
! of TC_FN(ks,TC_SEQ(tycs)) => TEbind(ks,tycs) (* B *)
! | TC_PROJ(TC_FN(ks,tenv,),j) => TElam(ks,j,tenv) (* L *)
! | TC_SUM _ => TEempty)
--- 470,553 ----
***************************************************************************)
! (* tycEnvs are represented by an encoding as tycs. The abstract representation
! * of tycEnvs would be given by:
! *
! * datatype teBinder
! * = Beta of int * tyc list * tkind list
! * | Lamb of int * tkind list
! *
! * type tycEnv = teBinder list
! *
! * Invariant: a tycEnv cannot terminate with a Lamb, i.e. the last binder
! * in a tycEnv must be a Beta. tycEnvs are created when a closure is created
! * when reducing a beta-redex (rule r1), and they are always initially of
! * of the form Beta(0,args,ks)::nil.
*)
! datatype teBinder
! = Beta of int * tyc list * tkind list
! (* Beta(j,args,ks):
! created when reducing a beta redex (r1);
! j: the embedding level of the original redex -- 0 if the redex was
! created by r1, or the nesting level of the new closure if by r12;
! args: the tycs bound by the n-ary beta reduction, i.e. the arguments;
! ks: the operator domain kinds *)
! | Lamb of int * tkind list
! (* Lamb(j,ks):
! created when pushing a closure (Env) through a lambda (r10);
! j: the nesting level of the closure just before r10 is applied,
! i.e. the nesteing level of the abstraction relative to the
! point where the closure was originally created;
! ks: the kinds of the abstraction parameters *)
! val teEmpty : tycEnv = tc_injX(TC_SUM[])
! (** utility functions for manipulating tycEnvs and teBinders **)
! (* encoding teBinders as tycs:
! * Beta(j,args,ks) <=> TC_FN(ks,TC_PROJ(TC_SEQ args, j))
! * Lamb(j,ks) <=> TC_PROJ(TC_FN(ks,TC_SUM[]), j)
! *)
! fun teEncodeBinder (Beta(j,args,ks)) : tyc =
! tc_injX(TC_FN(ks,tc_injX(TC_PROJ(tc_injX(TC_SEQ args), j))))
! | teEncodeBinder (Lamb(j,ks)) =
! tc_injX(TC_PROJ(tc_injX(TC_FN(ks,tc_injX(TC_SUM[])), j)))
! fun teDecodeBinder (tyc : tyc) : teBinder =
! case tc_outX(tyc)
! of TC_FN(ks,tyc') =>
! (case tc_outX tyc'
! of TC_PROJ(tyc'',j) =>
! (case tc_outX tyc''
! of TC_SEQ(args) => Beta(j,args,ks)
! | bug "teDecodeBinder")
! | _ => bug "teDecodeBinder")
! | TC_PROJ(tyc',j) =>
! (case tc_outX tyc'
! of TC_FN(ks,_) => Lamb(j, ks)
! | _ => bug "teDecodeBinder")
! | _ => bug "teDecodeBinder"
! fun teCons (b: teBinder, tenv: tycEnv) : tycEnv =
! tc_injX(TC_PARROW(b,tenv))
! fun teDest (tenv: tycEnv) : (teBinder * tycEnv) option =
! case tc_outX tenv
! of TC_PARROW(b,tenv) => SOME(teDecodeBinder b, tenv)
! | TC_SUM [] => NONE
! | _ => bug "teDest"
! (* 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
! of SOME(binder, tenv') =>
! if i > 1 then teLookup(tenv',i-1)
! else if i = 1 then SOME binder
! else bug "index 0 in tycEnvLookup"
! | NONE => NONE
***************
*** 569,572 ****
--- 591,595 ----
end
+
(** testing the "pointer" equality on normalized tkind, tyc, and lty *)
fun tk_eq (x: tkind, y) = (x = y)
***************
*** 574,577 ****
--- 597,601 ----
fun lt_eq (x: lty, y) = (x = y)
+
(** utility functions for updating tycs and ltys *)
fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =
***************
*** 587,589 ****
--- 611,614 ----
| lty_upd _ = bug "unexpected lty_upd on already normalized lty"
+
end (* structure Lty *)
-------------------------------------------------------------------------
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