CVS: sml-dist/src/compiler/FLINT/kernel ltybasic.sig, 1.8.26.2, 1.8.26.3 ltybasic.sml, 1.13.24.2, 1.13.24.3 ltydef.sig, 1.4, 1.4.24.1 ltydef.sml, 1.4, 1.4.24.1 ltydict.sml, 1.2, 1.2.26.1 ltyextern.sml, 1.19.24.1, 1.19.24.2 ltykernel.sig, 1.11.24.5, 1.11.24.6 ltykernel.sml, 1.18.12.14, 1.18.12.15 pplty.sml, 1.1.2.8, 1.1.2.9
David MacQueen <[email protected]> Fri, 11 Aug 2006 13:42:26 -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-serv18989/src/compiler/FLINT/kernel
Modified Files:
Tag: primop-branch-2
ltybasic.sig ltybasic.sml ltydef.sig ltydef.sml ltydict.sml
ltyextern.sml ltykernel.sig ltykernel.sml pplty.sml
Log Message:
broke ltykernel into lty and ltykernel, improved pplty
Index: ltybasic.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltybasic.sig,v
retrieving revision 1.8.26.2
retrieving revision 1.8.26.3
diff -C2 -d -r1.8.26.2 -r1.8.26.3
*** ltybasic.sig 11 Aug 2006 04:09:23 -0000 1.8.26.2
--- ltybasic.sig 11 Aug 2006 20:42:23 -0000 1.8.26.3
***************
*** 116,120 ****
(** utility functions on tycEnv *)
! exception tcUnbound of LtyKernel.tycEnv * LtyKernel.tyc
type tycEnv = LtyKernel.tycEnv
val initTycEnv : tycEnv
--- 116,120 ----
(** utility functions on tycEnv *)
! exception tcUnbound
type tycEnv = LtyKernel.tycEnv
val initTycEnv : tycEnv
Index: ltybasic.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltybasic.sml,v
retrieving revision 1.13.24.2
retrieving revision 1.13.24.3
diff -C2 -d -r1.13.24.2 -r1.13.24.3
*** ltybasic.sml 28 Jul 2006 22:26:07 -0000 1.13.24.2
--- ltybasic.sml 11 Aug 2006 20:42:23 -0000 1.13.24.3
***************
*** 7,10 ****
--- 7,11 ----
local structure PT = PrimTyc
structure DI = DebIndex
+ structure LT = Lty
structure LK = LtyKernel
***************
*** 33,42 ****
(p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))
! fun pfflag (LK.FF_VAR b) =
let fun pff (true, true) = "rr" | pff (true, false) = "rc"
| pff (false, true) = "cr" | pff (false, false) = "cc"
in pff b
end
! | pfflag (LK.FF_FIXED) = "f"
fun parw(p, (ff, t1, t2)) =
--- 34,43 ----
(p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))
! fun pfflag (LT.FF_VAR b) =
let fun pff (true, true) = "rr" | pff (true, false) = "rc"
| pff (false, true) = "cr" | pff (false, false) = "cc"
in pff b
end
! | pfflag (LT.FF_FIXED) = "f"
fun parw(p, (ff, t1, t2)) =
***************
*** 48,52 ****
(** new a type variable, currently not used *)
! val mkTvar : unit -> tvar = LK.mkTvar
(** utility functions for constructing tkinds *)
--- 49,53 ----
(** new a type variable, currently not used *)
! val mkTvar : unit -> tvar = LT.mkTvar
(** utility functions for constructing tkinds *)
***************
*** 70,79 ****
val ffc_rrflint = ffc_var (true, true)
! fun ffc_fspec (x as LK.FF_FIXED, (true,true)) = x
! | ffc_fspec (x as LK.FF_VAR _, nx) = ffc_var nx
| ffc_fspec _ = bug "unexpected case in ffc_fspec"
! fun ffd_fspec (LK.FF_FIXED) = (true,true)
! | ffd_fspec (LK.FF_VAR x) = x
(** utility functions for constructing tycs *)
--- 71,80 ----
val ffc_rrflint = ffc_var (true, true)
! fun ffc_fspec (x as LT.FF_FIXED, (true,true)) = x
! | ffc_fspec (x as LT.FF_VAR _, nx) = ffc_var nx
| ffc_fspec _ = bug "unexpected case in ffc_fspec"
! fun ffd_fspec (LT.FF_FIXED) = (true,true)
! | ffd_fspec (LT.FF_VAR x) = x
(** utility functions for constructing tycs *)
***************
*** 146,215 ****
***************************************************************************)
! (** pretty printing of tkinds, tycs, and ltys *)
fun tk_print (x : tkind) =
! let fun g (LK.TK_MONO) = "K0"
! | g (LK.TK_BOX) = "KB0"
! | g (LK.TK_FUN (ks, k)) =
! "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
! | g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"
! in g (tk_out x)
! end
fun tc_print (x : tyc) =
! let fun g (LK.TC_VAR(i,j)) = "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
! | g (LK.TC_NVAR v) = "NTV(v" ^ (itos v) ^ ")"
! | g (LK.TC_PRIM pt) = PT.pt_print pt
! | g (LK.TC_FN(ks, t)) =
! "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
! | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"
! | g (LK.TC_APP(t, zs)) =
! (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
! | g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"
! | g (LK.TC_PROJ (t, i)) =
! "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
! | g (LK.TC_SUM tcs) =
! "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
! | g (LK.TC_FIX ((_, tc, ts), i)) =
! if tc_eqv(x,tcc_bool) then "B"
! else if tc_eqv(x,tcc_list) then "LST"
! else (let (* val ntc = case ts of [] => tc
! | _ => tcc_app(tc, ts) *)
! val _ = 1
! in ("DT{" ^ "DATA" ^ (* "[" ^ (tc_print tc)
! ^ "] &&" ^ (plist(tc_print, ts))
! ^ "&&" ^*) "===" ^ (itos i) ^ "}")
! end)
! | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"
! | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"
! | g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"
! | g (LK.TC_ARROW (ff,z1,z2)) =
! parw(fn u => plist(tc_print,u),(ff,z1,z2))
! | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"
! | g (LK.TC_TOKEN (k, t)) =
! if LK.token_isvalid k then
! (LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
! else bug "unexpected TC_TOKEN tyc in tc_print"
! | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
! | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"
! | g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"
! in g (tc_out x)
! end (* function tc_print *)
fun lt_print (x : lty) =
! let fun h (i, t) = "(" ^ (itos i) ^ "," ^ (lt_print t) ^ ")"
!
! fun g (LK.LT_TYC t) = tc_print t
! | g (LK.LT_STR zs) = "S{" ^ (plist(lt_print, zs)) ^ "}"
! | g (LK.LT_FCT (ts1,ts2)) =
! "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
! ^ (plist(lt_print, ts2)) ^ ")"
! | g (LK.LT_POLY(ks, ts)) =
! "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
! | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"
! | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"
! | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"
!
! in g (lt_out x)
! end (* function lt_print *)
(** finding out the depth for a tyc's innermost-bound free variables *)
--- 147,211 ----
***************************************************************************)
! (** (pretty?) printing of tkinds, tycs, and ltys -- see pplty.sml for real
! ** pretty printing **)
fun tk_print (x : tkind) =
! (case tk_out x
! of LT.TK_MONO => "K0"
! | LT.TK_BOX => "KB0"
! | LT.TK_FUN(ks, k) =>
! "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
! | LT.TK_SEQ zs => "KS(" ^ (plist(tk_print, zs)) ^ ")")
fun tc_print (x : tyc) =
! (case (tc_out x)
! of LT.TC_VAR(i,j) => "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
! | LT.TC_NVAR v => "NTV(v" ^ (itos v) ^ ")"
! | LT.TC_PRIM pt => PT.pt_print pt
! | LT.TC_FN(ks, t) =>
! "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
! | LT.TC_APP(t, []) => tc_print t ^ "[]"
! | LT.TC_APP(t, zs) =>
! (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
! | LT.TC_SEQ zs => "TS(" ^ (plist(tc_print,zs)) ^ ")"
! | LT.TC_PROJ (t, i) =>
! "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
! | LT.TC_SUM tcs =>
! "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
! | LT.TC_FIX ((_, tc, ts), i) =>
! if tc_eqv(x,tcc_bool) then "B"
! else if tc_eqv(x,tcc_list) then "LST"
! else (let (* val ntc = case ts of [] => tc
! | _ => tcc_app(tc, ts) *)
! val _ = 1
! in ("DT{" ^ "DATA" ^ (* "[" ^ (tc_print tc)
! ^ "] &&" ^ (plist(tc_print, ts))
! ^ "&&" ^*) "===" ^ (itos i) ^ "}")
! end)
! | LT.TC_ABS t => "Ax(" ^ (tc_print t) ^ ")"
! | LT.TC_BOX t => "Bx(" ^ (tc_print t) ^ ")"
! | LT.TC_TUPLE(_,zs) => "TT<" ^ (plist(tc_print, zs)) ^ ">"
! | LT.TC_ARROW (ff,z1,z2) =>
! parw(fn u => plist(tc_print,u),(ff,z1,z2))
! | LT.TC_PARROW _ => bug "unexpected TC_PARROW in tc_print"
! | LT.TC_TOKEN (k, t) =>
! if LT.token_isvalid k then
! (LT.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
! else bug "unexpected TC_TOKEN tyc in tc_print"
! | LT.TC_CONT ts => "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
! | LT.TC_IND _ => bug "unexpected TC_IND in tc_print"
! | LT.TC_ENV _ => bug "unexpected TC_ENV in tc_print")
fun lt_print (x : lty) =
! (case lt_out x
! of LT.LT_TYC t => tc_print t
! | LT.LT_STR zs => "S{" ^ (plist(lt_print, zs)) ^ "}"
! | LT.LT_FCT (ts1,ts2) =>
! "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
! ^ (plist(lt_print, ts2)) ^ ")"
! | LT.LT_POLY(ks, ts) =>
! "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
! | LT.LT_CONT ts => "CNT(" ^ (plist(lt_print, ts)) ^ ")"
! | LT.LT_IND _ => bug "unexpected LT_IND in lt_print"
! | LT.LT_ENV _ => bug "unexpected LT_ENV in lt_print")
(** finding out the depth for a tyc's innermost-bound free variables *)
***************
*** 220,246 ****
fun lt_adj (lt, d, nd) =
if d = nd then lt
! else ltc_env(lt, 0, nd - d, LK.initTycEnv)
fun tc_adj (tc, d, nd) =
if d = nd then tc
! else tcc_env(tc, 0, nd - d, LK.initTycEnv)
! (** the following functions does the smiliar thing as lt_adj and
! tc_adj; it adjusts an lty (or tyc) from depth d+k to depth nd+k,
assuming the last k levels are type abstractions. So lt_adj
is really lt_adj_k with k set to 0. Both functions are currently
! called inside the lcontract.sml only. *)
local
fun mkTycEnv (i, k, dd, e) =
! if i >= k then e else mkTycEnv(i+1, k, dd, LK.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, LK.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, LK.initTycEnv))
end (* lt_adj_k and tc_adj_k *)
--- 216,242 ----
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;
! they adjust an lty (or tyc) from depth d+k to depth nd+k,
assuming the last k levels are type abstractions. So lt_adj
is really lt_adj_k with k set to 0. Both functions are currently
! 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 *)
***************
*** 256,264 ****
***************************************************************************)
! type tkindEnv = LK.tkindEnv
! exception tkUnbound = LK.tkUnbound
! val initTkEnv = LK.initTkEnv
! val tkLookup = LK.tkLookup
! val tkInsert = LK.tkInsert
(***************************************************************************
--- 252,260 ----
***************************************************************************)
! type tkindEnv = LT.tkindEnv
! exception tkUnbound = LT.tkUnbound
! val initTkEnv = LT.initTkEnv
! val tkLookup = LT.tkLookup
! val tkInsert = LT.tkInsert
(***************************************************************************
***************
*** 266,273 ****
***************************************************************************)
! exception tcUnbound = LK.tcUnbound
! type tycEnv = LK.tycEnv
! val initTycEnv = LK.initTycEnv
! val tcInsert = LK.tcInsert
(***************************************************************************
--- 262,269 ----
***************************************************************************)
! exception tcUnbound = LT.tcUnbound
! type tycEnv = LT.tycEnv
! val initTycEnv = LT.initTycEnv
! val tcInsert = LT.tcInsert
(***************************************************************************
***************
*** 290,294 ****
if d=nd then lt
else if d > nd then bug "unexpected depth info in ltLookup"
! else ltc_env(lt, 0, nd - d, LK.initTycEnv)
(*easc*))
--- 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*))
Index: ltydef.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltydef.sig,v
retrieving revision 1.4
retrieving revision 1.4.24.1
diff -C2 -d -r1.4 -r1.4.24.1
*** ltydef.sig 1 Jun 2000 18:33:26 -0000 1.4
--- ltydef.sig 11 Aug 2006 20:42:23 -0000 1.4.24.1
***************
*** 17,28 ****
type depth = DebIndex.depth
type primtyc = PrimTyc.primtyc
! type tvar = LtyKernel.tvar
! type fflag = LtyKernel.fflag
! type rflag = LtyKernel.rflag
! type tkind = LtyKernel.tkind
! type tyc = LtyKernel.tyc
! type lty = LtyKernel.lty
(*
--- 17,28 ----
type depth = DebIndex.depth
type primtyc = PrimTyc.primtyc
! type tvar = Lty.tvar
! type fflag = Lty.fflag
! type rflag = Lty.rflag
! type tkind = Lty.tkind
! type tyc = Lty.tyc
! type lty = Lty.lty
(*
Index: ltydef.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltydef.sml,v
retrieving revision 1.4
retrieving revision 1.4.24.1
diff -C2 -d -r1.4 -r1.4.24.1
*** ltydef.sml 1 Jun 2000 18:33:26 -0000 1.4
--- ltydef.sml 11 Aug 2006 20:42:23 -0000 1.4.24.1
***************
*** 7,14 ****
local structure PT = PrimTyc
structure DI = DebIndex
structure LK = LtyKernel
fun bug msg = ErrorMsg.impossible("LtyDef: "^msg)
- val say = Control.Print.say
(** common utility functions *)
--- 7,14 ----
local structure PT = PrimTyc
structure DI = DebIndex
+ structure LT = Lty
structure LK = LtyKernel
fun bug msg = ErrorMsg.impossible("LtyDef: "^msg)
(** common utility functions *)
***************
*** 31,42 ****
type depth = DI.depth
type primtyc = PT.primtyc
! type tvar = LK.tvar
! type fflag = LK.fflag
! type rflag = LK.rflag
! type tkind = LK.tkind
! type tyc = LK.tyc
! type lty = LK.lty
(*
--- 31,42 ----
type depth = DI.depth
type primtyc = PT.primtyc
! type tvar = LT.tvar
! type fflag = LT.fflag
! type rflag = LT.rflag
! type tkind = LT.tkind
! type tyc = LT.tyc
! type lty = LT.lty
(*
***************
*** 54,61 ****
(** tkind constructors *)
! val tkc_mono : tkind = tk_inj (LK.TK_MONO)
! val tkc_box : tkind = tk_inj (LK.TK_BOX)
! val tkc_seq : tkind list -> tkind = tk_inj o LK.TK_SEQ
! val tkc_fun : tkind list * tkind -> tkind = tk_inj o LK.TK_FUN
(** tkind deconstructors *)
--- 54,61 ----
(** tkind constructors *)
! val tkc_mono : tkind = tk_inj (LT.TK_MONO)
! val tkc_box : tkind = tk_inj (LT.TK_BOX)
! val tkc_seq : tkind list -> tkind = tk_inj o LT.TK_SEQ
! val tkc_fun : tkind list * tkind -> tkind = tk_inj o LT.TK_FUN
(** tkind deconstructors *)
***************
*** 63,70 ****
val tkd_box : tkind -> unit = fn _ => ()
val tkd_seq : tkind -> tkind list = fn tk =>
! (case tk_out tk of LK.TK_SEQ x => x
| _ => bug "unexpected tkind in tkd_seq")
val tkd_fun : tkind -> tkind list * tkind = fn tk =>
! (case tk_out tk of LK.TK_FUN x => x
| _ => bug "unexpected tkind in tkd_fun")
--- 63,70 ----
val tkd_box : tkind -> unit = fn _ => ()
val tkd_seq : tkind -> tkind list = fn tk =>
! (case tk_out tk of LT.TK_SEQ x => x
| _ => bug "unexpected tkind in tkd_seq")
val tkd_fun : tkind -> tkind list * tkind = fn tk =>
! (case tk_out tk of LT.TK_FUN x => x
| _ => bug "unexpected tkind in tkd_fun")
***************
*** 73,79 ****
val tkp_box : tkind -> bool = fn tk => tk_eqv(tk, tkc_box)
val tkp_seq : tkind -> bool = fn tk =>
! (case tk_out tk of LK.TK_SEQ _ => true | _ => false)
val tkp_fun : tkind -> bool = fn tk =>
! (case tk_out tk of LK.TK_FUN _ => true | _ => false)
(** tkind one-arm switches *)
--- 73,79 ----
val tkp_box : tkind -> bool = fn tk => tk_eqv(tk, tkc_box)
val tkp_seq : tkind -> bool = fn tk =>
! (case tk_out tk of LT.TK_SEQ _ => true | _ => false)
val tkp_fun : tkind -> bool = fn tk =>
! (case tk_out tk of LT.TK_FUN _ => true | _ => false)
(** tkind one-arm switches *)
***************
*** 81,87 ****
fun tkw_box (tk, f, g) = if tk_eqv(tk, tkc_box) then f () else g tk
fun tkw_seq (tk, f, g) =
! (case tk_out tk of LK.TK_SEQ x => f x | _ => g tk)
fun tkw_fun (tk, f, g) =
! (case tk_out tk of LK.TK_FUN x => f x | _ => g tk)
--- 81,87 ----
fun tkw_box (tk, f, g) = if tk_eqv(tk, tkc_box) then f () else g tk
fun tkw_seq (tk, f, g) =
! (case tk_out tk of LT.TK_SEQ x => f x | _ => g tk)
fun tkw_fun (tk, f, g) =
! (case tk_out tk of LT.TK_FUN x => f x | _ => g tk)
***************
*** 103,129 ****
(** fflag and rflag constructors *)
! val ffc_var : bool * bool -> fflag = fn x => LK.FF_VAR x
! val ffc_fixed : fflag = LK.FF_FIXED
! val rfc_tmp : rflag = LK.RF_TMP
(** fflag and rflag deconstructors *)
val ffd_var : fflag -> bool * bool = fn x =>
! (case x of LK.FF_VAR x => x | _ => bug "unexpected fflag in ffd_var")
val ffd_fixed : fflag -> unit = fn x =>
! (case x of LK.FF_FIXED => () | _ => bug "unexpected fflag in ffd_fixed")
! val rfd_tmp : rflag -> unit = fn (LK.RF_TMP) => ()
(** fflag and rflag predicates *)
val ffp_var : fflag -> bool = fn x =>
! (case x of LK.FF_VAR _ => true | _ => false)
val ffp_fixed : fflag -> bool = fn x =>
! (case x of LK.FF_FIXED => true | _ => false)
! val rfp_tmp : rflag -> bool = fn (LK.RF_TMP) => true
(** fflag and rflag one-arm switch *)
fun ffw_var (ff, f, g) =
! (case ff of LK.FF_VAR x => f x | _ => g ff)
fun ffw_fixed (ff, f, g) =
! (case ff of LK.FF_FIXED => f () | _ => g ff)
fun rfw_tmp (rf, f, g) = f()
--- 103,129 ----
(** fflag and rflag constructors *)
! val ffc_var : bool * bool -> fflag = fn x => LT.FF_VAR x
! val ffc_fixed : fflag = LT.FF_FIXED
! val rfc_tmp : rflag = LT.RF_TMP
(** fflag and rflag deconstructors *)
val ffd_var : fflag -> bool * bool = fn x =>
! (case x of LT.FF_VAR x => x | _ => bug "unexpected fflag in ffd_var")
val ffd_fixed : fflag -> unit = fn x =>
! (case x of LT.FF_FIXED => () | _ => bug "unexpected fflag in ffd_fixed")
! val rfd_tmp : rflag -> unit = fn (LT.RF_TMP) => ()
(** fflag and rflag predicates *)
val ffp_var : fflag -> bool = fn x =>
! (case x of LT.FF_VAR _ => true | _ => false)
val ffp_fixed : fflag -> bool = fn x =>
! (case x of LT.FF_FIXED => true | _ => false)
! val rfp_tmp : rflag -> bool = fn (LT.RF_TMP) => true
(** fflag and rflag one-arm switch *)
fun ffw_var (ff, f, g) =
! (case ff of LT.FF_VAR x => f x | _ => g ff)
fun ffw_fixed (ff, f, g) =
! (case ff of LT.FF_FIXED => f () | _ => g ff)
fun rfw_tmp (rf, f, g) = f()
***************
*** 157,285 ****
(** tyc constructors *)
! val tcc_var : index * int -> tyc = tc_inj o LK.TC_VAR
! val tcc_nvar : tvar -> tyc = tc_inj o LK.TC_NVAR
! val tcc_prim : primtyc -> tyc = tc_inj o LK.TC_PRIM
! val tcc_fn : tkind list * tyc -> tyc = tc_inj o LK.TC_FN
! val tcc_app : tyc * tyc list -> tyc = tc_inj o LK.TC_APP
! val tcc_seq : tyc list -> tyc = tc_inj o LK.TC_SEQ
! val tcc_proj : tyc * int -> tyc = tc_inj o LK.TC_PROJ
! val tcc_sum : tyc list -> tyc = tc_inj o LK.TC_SUM
! val tcc_fix : (int * tyc * tyc list) * int -> tyc = tc_inj o LK.TC_FIX
! val tcc_wrap : tyc -> tyc = fn tc => tc_inj (LK.TC_TOKEN(LK.wrap_token, tc))
! val tcc_abs : tyc -> tyc = tc_inj o LK.TC_ABS
! val tcc_box : tyc -> tyc = tc_inj o LK.TC_BOX
! val tcc_tuple : tyc list -> tyc = fn ts => tc_inj (LK.TC_TUPLE (rfc_tmp, ts))
val tcc_arrow : fflag * tyc list * tyc list -> tyc = LK.tcc_arw
(** tyc deconstructors *)
val tcd_var : tyc -> index * int = fn tc =>
! (case tc_out tc of LK.TC_VAR x => x
| _ => bug "unexpected tyc in tcd_var")
val tcd_nvar : tyc -> tvar = fn tc =>
! (case tc_out tc of LK.TC_NVAR x => x
| _ => bug "unexpected tyc in tcd_nvar")
val tcd_prim : tyc -> primtyc = fn tc =>
! (case tc_out tc of LK.TC_PRIM x => x
| _ => bug "unexpected tyc in tcd_prim")
val tcd_fn : tyc -> tkind list * tyc = fn tc =>
! (case tc_out tc of LK.TC_FN x => x
| _ => bug "unexpected tyc in tcd_fn")
val tcd_app : tyc -> tyc * tyc list = fn tc =>
! (case tc_out tc of LK.TC_APP x => x
| _ => bug "unexpected tyc in tcd_app")
val tcd_seq : tyc -> tyc list = fn tc =>
! (case tc_out tc of LK.TC_SEQ x => x
| _ => bug "unexpected tyc in tcd_seq")
val tcd_proj : tyc -> tyc * int = fn tc =>
! (case tc_out tc of LK.TC_PROJ x => x
| _ => bug "unexpected tyc in tcd_proj")
val tcd_sum : tyc -> tyc list = fn tc =>
! (case tc_out tc of LK.TC_SUM x => x
| _ => bug "unexpected tyc in tcd_sum")
val tcd_fix : tyc -> (int * tyc * tyc list) * int = fn tc =>
! (case tc_out tc of LK.TC_FIX x => x
| _ => bug "unexpected tyc in tcd_fix")
val tcd_wrap : tyc -> tyc = fn tc =>
(case tc_out tc
! of LK.TC_TOKEN(tk, x) =>
! if LK.token_eq(tk, LK.wrap_token) then x
else bug "unexpected token tyc in tcd_wrap"
| _ => bug "unexpected regular tyc in tcd_wrap")
val tcd_abs : tyc -> tyc = fn tc =>
! (case tc_out tc of LK.TC_ABS x => x
| _ => bug "unexpected tyc in tcd_abs")
val tcd_box : tyc -> tyc = fn tc =>
! (case tc_out tc of LK.TC_BOX x => x
| _ => bug "unexpected tyc in tcd_box")
val tcd_tuple : tyc -> tyc list = fn tc =>
! (case tc_out tc of LK.TC_TUPLE (_,x) => x
| _ => bug "unexpected tyc in tcd_tuple")
val tcd_arrow : tyc -> fflag * tyc list * tyc list = fn tc =>
! (case tc_out tc of LK.TC_ARROW x => x
| _ => bug "unexpected tyc in tcd_arrow")
(** tyc predicates *)
val tcp_var : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_VAR _ => true | _ => false)
val tcp_nvar : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_NVAR _ => true | _ => false)
val tcp_prim : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_PRIM _ => true | _ => false)
val tcp_fn : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_FN _ => true | _ => false)
val tcp_app : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_APP _ => true | _ => false)
val tcp_seq : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_SEQ _ => true | _ => false)
val tcp_proj : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_PROJ _ => true | _ => false)
val tcp_sum : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_SUM _ => true | _ => false)
val tcp_fix : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_FIX _ => true | _ => false)
val tcp_wrap : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_TOKEN (tk, _) => LK.token_eq(tk, LK.wrap_token)
| _ => false)
val tcp_abs : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_ABS _ => true | _ => false)
val tcp_box : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_BOX _ => true | _ => false)
val tcp_tuple : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_TUPLE _ => true | _ => false)
val tcp_arrow : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_ARROW _ => true | _ => false)
(** tyc one-arm switches *)
fun tcw_var (tc, f, g) =
! (case tc_out tc of LK.TC_VAR x => f x | _ => g tc)
fun tcw_nvar (tc, f, g) =
! (case tc_out tc of LK.TC_NVAR x => f x | _ => g tc)
fun tcw_prim (tc, f, g) =
! (case tc_out tc of LK.TC_PRIM x => f x | _ => g tc)
fun tcw_fn (tc, f, g) =
! (case tc_out tc of LK.TC_FN x => f x | _ => g tc)
fun tcw_app (tc, f, g) =
! (case tc_out tc of LK.TC_APP x => f x | _ => g tc)
fun tcw_seq (tc, f, g) =
! (case tc_out tc of LK.TC_SEQ x => f x | _ => g tc)
fun tcw_proj (tc, f, g) =
! (case tc_out tc of LK.TC_PROJ x => f x | _ => g tc)
fun tcw_sum (tc, f, g) =
! (case tc_out tc of LK.TC_SUM x => f x | _ => g tc)
fun tcw_fix (tc, f, g) =
! (case tc_out tc of LK.TC_FIX x => f x | _ => g tc)
fun tcw_wrap (tc, f, g) =
(case tc_out tc
! of LK.TC_TOKEN(rk, x) =>
! if LK.token_eq(rk, LK.wrap_token) then f x else g tc
| _ => g tc)
fun tcw_abs (tc, f, g) =
! (case tc_out tc of LK.TC_ABS x => f x | _ => g tc)
fun tcw_box (tc, f, g) =
! (case tc_out tc of LK.TC_BOX x => f x | _ => g tc)
fun tcw_tuple (tc, f, g) =
! (case tc_out tc of LK.TC_TUPLE (_,x) => f x | _ => g tc)
fun tcw_arrow (tc, f, g) =
! (case tc_out tc of LK.TC_ARROW x => f x | _ => g tc)
--- 157,285 ----
(** tyc constructors *)
! val tcc_var : index * int -> tyc = tc_inj o LT.TC_VAR
! val tcc_nvar : tvar -> tyc = tc_inj o LT.TC_NVAR
! val tcc_prim : primtyc -> tyc = tc_inj o LT.TC_PRIM
! val tcc_fn : tkind list * tyc -> tyc = tc_inj o LT.TC_FN
! val tcc_app : tyc * tyc list -> tyc = tc_inj o LT.TC_APP
! val tcc_seq : tyc list -> tyc = tc_inj o LT.TC_SEQ
! val tcc_proj : tyc * int -> tyc = tc_inj o LT.TC_PROJ
! val tcc_sum : tyc list -> tyc = tc_inj o LT.TC_SUM
! val tcc_fix : (int * tyc * tyc list) * int -> tyc = tc_inj o LT.TC_FIX
! val tcc_wrap : tyc -> tyc = fn tc => tc_inj (LT.TC_TOKEN(LK.wrap_token, tc))
! val tcc_abs : tyc -> tyc = tc_inj o LT.TC_ABS
! val tcc_box : tyc -> tyc = tc_inj o LT.TC_BOX
! val tcc_tuple : tyc list -> tyc = fn ts => tc_inj (LT.TC_TUPLE (rfc_tmp, ts))
val tcc_arrow : fflag * tyc list * tyc list -> tyc = LK.tcc_arw
(** tyc deconstructors *)
val tcd_var : tyc -> index * int = fn tc =>
! (case tc_out tc of LT.TC_VAR x => x
| _ => bug "unexpected tyc in tcd_var")
val tcd_nvar : tyc -> tvar = fn tc =>
! (case tc_out tc of LT.TC_NVAR x => x
| _ => bug "unexpected tyc in tcd_nvar")
val tcd_prim : tyc -> primtyc = fn tc =>
! (case tc_out tc of LT.TC_PRIM x => x
| _ => bug "unexpected tyc in tcd_prim")
val tcd_fn : tyc -> tkind list * tyc = fn tc =>
! (case tc_out tc of LT.TC_FN x => x
| _ => bug "unexpected tyc in tcd_fn")
val tcd_app : tyc -> tyc * tyc list = fn tc =>
! (case tc_out tc of LT.TC_APP x => x
| _ => bug "unexpected tyc in tcd_app")
val tcd_seq : tyc -> tyc list = fn tc =>
! (case tc_out tc of LT.TC_SEQ x => x
| _ => bug "unexpected tyc in tcd_seq")
val tcd_proj : tyc -> tyc * int = fn tc =>
! (case tc_out tc of LT.TC_PROJ x => x
| _ => bug "unexpected tyc in tcd_proj")
val tcd_sum : tyc -> tyc list = fn tc =>
! (case tc_out tc of LT.TC_SUM x => x
| _ => bug "unexpected tyc in tcd_sum")
val tcd_fix : tyc -> (int * tyc * tyc list) * int = fn tc =>
! (case tc_out tc of LT.TC_FIX x => x
| _ => bug "unexpected tyc in tcd_fix")
val tcd_wrap : tyc -> tyc = fn tc =>
(case tc_out tc
! of LT.TC_TOKEN(tk, x) =>
! if LT.token_eq(tk, LK.wrap_token) then x
else bug "unexpected token tyc in tcd_wrap"
| _ => bug "unexpected regular tyc in tcd_wrap")
val tcd_abs : tyc -> tyc = fn tc =>
! (case tc_out tc of LT.TC_ABS x => x
| _ => bug "unexpected tyc in tcd_abs")
val tcd_box : tyc -> tyc = fn tc =>
! (case tc_out tc of LT.TC_BOX x => x
| _ => bug "unexpected tyc in tcd_box")
val tcd_tuple : tyc -> tyc list = fn tc =>
! (case tc_out tc of LT.TC_TUPLE (_,x) => x
| _ => bug "unexpected tyc in tcd_tuple")
val tcd_arrow : tyc -> fflag * tyc list * tyc list = fn tc =>
! (case tc_out tc of LT.TC_ARROW x => x
| _ => bug "unexpected tyc in tcd_arrow")
(** tyc predicates *)
val tcp_var : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_VAR _ => true | _ => false)
val tcp_nvar : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_NVAR _ => true | _ => false)
val tcp_prim : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_PRIM _ => true | _ => false)
val tcp_fn : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_FN _ => true | _ => false)
val tcp_app : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_APP _ => true | _ => false)
val tcp_seq : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_SEQ _ => true | _ => false)
val tcp_proj : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_PROJ _ => true | _ => false)
val tcp_sum : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_SUM _ => true | _ => false)
val tcp_fix : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_FIX _ => true | _ => false)
val tcp_wrap : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_TOKEN (tk, _) => LT.token_eq(tk, LK.wrap_token)
| _ => false)
val tcp_abs : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_ABS _ => true | _ => false)
val tcp_box : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_BOX _ => true | _ => false)
val tcp_tuple : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_TUPLE _ => true | _ => false)
val tcp_arrow : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_ARROW _ => true | _ => false)
(** tyc one-arm switches *)
fun tcw_var (tc, f, g) =
! (case tc_out tc of LT.TC_VAR x => f x | _ => g tc)
fun tcw_nvar (tc, f, g) =
! (case tc_out tc of LT.TC_NVAR x => f x | _ => g tc)
fun tcw_prim (tc, f, g) =
! (case tc_out tc of LT.TC_PRIM x => f x | _ => g tc)
fun tcw_fn (tc, f, g) =
! (case tc_out tc of LT.TC_FN x => f x | _ => g tc)
fun tcw_app (tc, f, g) =
! (case tc_out tc of LT.TC_APP x => f x | _ => g tc)
fun tcw_seq (tc, f, g) =
! (case tc_out tc of LT.TC_SEQ x => f x | _ => g tc)
fun tcw_proj (tc, f, g) =
! (case tc_out tc of LT.TC_PROJ x => f x | _ => g tc)
fun tcw_sum (tc, f, g) =
! (case tc_out tc of LT.TC_SUM x => f x | _ => g tc)
fun tcw_fix (tc, f, g) =
! (case tc_out tc of LT.TC_FIX x => f x | _ => g tc)
fun tcw_wrap (tc, f, g) =
(case tc_out tc
! of LT.TC_TOKEN(rk, x) =>
! if LT.token_eq(rk, LK.wrap_token) then f x else g tc
| _ => g tc)
fun tcw_abs (tc, f, g) =
! (case tc_out tc of LT.TC_ABS x => f x | _ => g tc)
fun tcw_box (tc, f, g) =
! (case tc_out tc of LT.TC_BOX x => f x | _ => g tc)
fun tcw_tuple (tc, f, g) =
! (case tc_out tc of LT.TC_TUPLE (_,x) => f x | _ => g tc)
fun tcw_arrow (tc, f, g) =
! (case tc_out tc of LT.TC_ARROW x => f x | _ => g tc)
***************
*** 299,340 ****
(** lty constructors *)
! val ltc_tyc : tyc -> lty = lt_inj o LK.LT_TYC
! val ltc_str : lty list -> lty = lt_inj o LK.LT_STR
! val ltc_fct : lty list * lty list -> lty = lt_inj o LK.LT_FCT
! val ltc_poly : tkind list * lty list -> lty = lt_inj o LK.LT_POLY
(** lty deconstructors *)
val ltd_tyc : lty -> tyc = fn lt =>
! (case lt_out lt of LK.LT_TYC x => x
| _ => bug "unexpected lty in ltd_tyc")
val ltd_str : lty -> lty list = fn lt =>
! (case lt_out lt of LK.LT_STR x => x
| _ => bug "unexpected lty in ltd_str")
val ltd_fct : lty -> lty list * lty list = fn lt =>
! (case lt_out lt of LK.LT_FCT x => x
| _ => bug "unexpected lty in ltd_fct")
val ltd_poly : lty -> tkind list * lty list = fn lt =>
! (case lt_out lt of LK.LT_POLY x => x
| _ => bug "unexpected lty in ltd_poly")
(** lty predicates *)
val ltp_tyc : lty -> bool = fn lt =>
! (case lt_out lt of LK.LT_TYC _ => true | _ => false)
val ltp_str : lty -> bool = fn lt =>
! (case lt_out lt of LK.LT_STR _ => true | _ => false)
val ltp_fct : lty -> bool = fn lt =>
! (case lt_out lt of LK.LT_FCT _ => true | _ => false)
val ltp_poly : lty -> bool = fn lt =>
! (case lt_out lt of LK.LT_POLY _ => true | _ => false)
(** lty one-arm switches *)
fun ltw_tyc (lt, f, g) =
! (case lt_out lt of LK.LT_TYC x => f x | _ => g lt)
fun ltw_str (lt, f, g) =
! (case lt_out lt of LK.LT_STR x => f x | _ => g lt)
fun ltw_fct (lt, f, g) =
! (case lt_out lt of LK.LT_FCT x => f x | _ => g lt)
fun ltw_poly (lt, f, g) =
! (case lt_out lt of LK.LT_POLY x => f x | _ => g lt)
--- 299,340 ----
(** lty constructors *)
! val ltc_tyc : tyc -> lty = lt_inj o LT.LT_TYC
! val ltc_str : lty list -> lty = lt_inj o LT.LT_STR
! val ltc_fct : lty list * lty list -> lty = lt_inj o LT.LT_FCT
! val ltc_poly : tkind list * lty list -> lty = lt_inj o LT.LT_POLY
(** lty deconstructors *)
val ltd_tyc : lty -> tyc = fn lt =>
! (case lt_out lt of LT.LT_TYC x => x
| _ => bug "unexpected lty in ltd_tyc")
val ltd_str : lty -> lty list = fn lt =>
! (case lt_out lt of LT.LT_STR x => x
| _ => bug "unexpected lty in ltd_str")
val ltd_fct : lty -> lty list * lty list = fn lt =>
! (case lt_out lt of LT.LT_FCT x => x
| _ => bug "unexpected lty in ltd_fct")
val ltd_poly : lty -> tkind list * lty list = fn lt =>
! (case lt_out lt of LT.LT_POLY x => x
| _ => bug "unexpected lty in ltd_poly")
(** lty predicates *)
val ltp_tyc : lty -> bool = fn lt =>
! (case lt_out lt of LT.LT_TYC _ => true | _ => false)
val ltp_str : lty -> bool = fn lt =>
! (case lt_out lt of LT.LT_STR _ => true | _ => false)
val ltp_fct : lty -> bool = fn lt =>
! (case lt_out lt of LT.LT_FCT _ => true | _ => false)
val ltp_poly : lty -> bool = fn lt =>
! (case lt_out lt of LT.LT_POLY _ => true | _ => false)
(** lty one-arm switches *)
fun ltw_tyc (lt, f, g) =
! (case lt_out lt of LT.LT_TYC x => f x | _ => g lt)
fun ltw_str (lt, f, g) =
! (case lt_out lt of LT.LT_STR x => f x | _ => g lt)
fun ltw_fct (lt, f, g) =
! (case lt_out lt of LT.LT_FCT x => f x | _ => g lt)
fun ltw_poly (lt, f, g) =
! (case lt_out lt of LT.LT_POLY x => f x | _ => g lt)
***************
*** 366,400 ****
(** tyc-lty predicates *)
val ltp_var : lty -> bool = fn t =>
! (case lt_out t of LK.LT_TYC x => tcp_var x | _ => false)
val ltp_prim : lty -> bool = fn t =>
! (case lt_out t of LK.LT_TYC x => tcp_prim x | _ => false)
val ltp_tuple : lty -> bool = fn t =>
! (case lt_out t of LK.LT_TYC x => tcp_tuple x | _ => false)
val ltp_arrow : lty -> bool = fn t =>
! (case lt_out t of LK.LT_TYC x => tcp_arrow x | _ => false)
(** tyc-lty one-arm switches *)
fun ltw_var (lt, f, g) =
(case lt_out lt
! of LK.LT_TYC tc =>
! (case tc_out tc of LK.TC_VAR x => f x | _ => g lt)
| _ => g lt)
fun ltw_prim (lt, f, g) =
(case lt_out lt
! of LK.LT_TYC tc =>
! (case tc_out tc of LK.TC_PRIM x => f x | _ => g lt)
| _ => g lt)
fun ltw_tuple (lt, f, g) =
(case lt_out lt
! of LK.LT_TYC tc =>
! (case tc_out tc of LK.TC_TUPLE (_, x) => f x | _ => g lt)
| _ => g lt)
fun ltw_arrow (lt, f, g) =
(case lt_out lt
! of LK.LT_TYC tc =>
! (case tc_out tc of LK.TC_ARROW x => f x | _ => g lt)
| _ => g lt)
--- 366,400 ----
(** tyc-lty predicates *)
val ltp_var : lty -> bool = fn t =>
! (case lt_out t of LT.LT_TYC x => tcp_var x | _ => false)
val ltp_prim : lty -> bool = fn t =>
! (case lt_out t of LT.LT_TYC x => tcp_prim x | _ => false)
val ltp_tuple : lty -> bool = fn t =>
! (case lt_out t of LT.LT_TYC x => tcp_tuple x | _ => false)
val ltp_arrow : lty -> bool = fn t =>
! (case lt_out t of LT.LT_TYC x => tcp_arrow x | _ => false)
(** tyc-lty one-arm switches *)
fun ltw_var (lt, f, g) =
(case lt_out lt
! of LT.LT_TYC tc =>
! (case tc_out tc of LT.TC_VAR x => f x | _ => g lt)
| _ => g lt)
fun ltw_prim (lt, f, g) =
(case lt_out lt
! of LT.LT_TYC tc =>
! (case tc_out tc of LT.TC_PRIM x => f x | _ => g lt)
| _ => g lt)
fun ltw_tuple (lt, f, g) =
(case lt_out lt
! of LT.LT_TYC tc =>
! (case tc_out tc of LT.TC_TUPLE (_, x) => f x | _ => g lt)
| _ => g lt)
fun ltw_arrow (lt, f, g) =
(case lt_out lt
! of LT.LT_TYC tc =>
! (case tc_out tc of LT.TC_ARROW x => f x | _ => g lt)
| _ => g lt)
***************
*** 411,436 ****
(** cont-tyc-lty constructors *)
! val tcc_cont : tyc list -> tyc = tc_inj o LK.TC_CONT
! val ltc_cont : lty list -> lty = lt_inj o LK.LT_CONT
(** cont-tyc-lty deconstructors *)
val tcd_cont : tyc -> tyc list = fn tc =>
! (case tc_out tc of LK.TC_CONT x => x
| _ => bug "unexpected tyc in tcd_cont")
val ltd_cont : lty -> lty list = fn lt =>
! (case lt_out lt of LK.LT_CONT x => x
| _ => bug "unexpected lty in ltd_cont")
(** cont-tyc-lty predicates *)
val tcp_cont : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_CONT _ => true | _ => false)
val ltp_cont : lty -> bool = fn lt =>
! (case lt_out lt of LK.LT_CONT _ => true | _ => false)
(** cont-tyc-lty one-arm switches *)
fun tcw_cont (tc, f, g) =
! (case tc_out tc of LK.TC_CONT x => f x | _ => g tc)
fun ltw_cont (lt, f, g) =
! (case lt_out lt of LK.LT_CONT x => f x | _ => g lt)
--- 411,436 ----
(** cont-tyc-lty constructors *)
! val tcc_cont : tyc list -> tyc = tc_inj o LT.TC_CONT
! val ltc_cont : lty list -> lty = lt_inj o LT.LT_CONT
(** cont-tyc-lty deconstructors *)
val tcd_cont : tyc -> tyc list = fn tc =>
! (case tc_out tc of LT.TC_CONT x => x
| _ => bug "unexpected tyc in tcd_cont")
val ltd_cont : lty -> lty list = fn lt =>
! (case lt_out lt of LT.LT_CONT x => x
| _ => bug "unexpected lty in ltd_cont")
(** cont-tyc-lty predicates *)
val tcp_cont : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_CONT _ => true | _ => false)
val ltp_cont : lty -> bool = fn lt =>
! (case lt_out lt of LT.LT_CONT _ => true | _ => false)
(** cont-tyc-lty one-arm switches *)
fun tcw_cont (tc, f, g) =
! (case tc_out tc of LT.TC_CONT x => f x | _ => g tc)
fun ltw_cont (lt, f, g) =
! (case lt_out lt of LT.LT_CONT x => f x | _ => g lt)
***************
*** 467,471 ****
val tcd_parrow : tyc -> tyc * tyc = fn tc =>
(case tc_out tc
! of LK.TC_ARROW (_, xs, ys) => (LK.tc_autotuple xs, LK.tc_autotuple ys)
| _ => bug "unexpected tyc in tcd_parrow")
val ltd_parrow : lty -> lty * lty = fn t =>
--- 467,471 ----
val tcd_parrow : tyc -> tyc * tyc = fn tc =>
(case tc_out tc
! of LT.TC_ARROW (_, xs, ys) => (LK.tc_autotuple xs, LK.tc_autotuple ys)
| _ => bug "unexpected tyc in tcd_parrow")
val ltd_parrow : lty -> lty * lty = fn t =>
***************
*** 486,509 ****
(** plambda tyc-lty predicates *)
val tcp_parrow : tyc -> bool = fn tc =>
! (case tc_out tc of LK.TC_ARROW (_, [x], [y]) => true | _ => false)
val ltp_parrow : lty -> bool = fn t =>
! (case lt_out t of LK.LT_TYC x => tcp_parrow x | _ => false)
val ltp_ppoly : lty -> bool = fn t =>
! (case lt_out t of LK.LT_POLY (_, [x]) => true | _ => false)
val ltp_pfct : lty -> bool = fn t =>
! (case lt_out t of LK.LT_FCT ([x], [y]) => true | _ => false)
(** plambda tyc-lty one-arm switches *)
fun tcw_parrow (tc, f, g) =
! (case tc_out tc of LK.TC_ARROW (_,[x],[y]) => f (x,y) | _ => g tc)
fun ltw_parrow (lt, f, g) =
(case lt_out lt
! of LK.LT_TYC tc =>
! (case tc_out tc of LK.TC_ARROW (_,[x],[y]) => f(x,y) | _ => g lt)
| _ => g lt)
fun ltw_ppoly (lt, f, g) =
! (case lt_out lt of LK.LT_POLY(ks,[x]) => f(ks,x) | _ => g lt)
fun ltw_pfct (lt, f, g) =
! (case lt_out lt of LK.LT_FCT([x],[y]) => f(x,y) | _ => g lt)
end (* top-level local *)
--- 486,509 ----
(** plambda tyc-lty predicates *)
val tcp_parrow : tyc -> bool = fn tc =>
! (case tc_out tc of LT.TC_ARROW (_, [x], [y]) => true | _ => false)
val ltp_parrow : lty -> bool = fn t =>
! (case lt_out t of LT.LT_TYC x => tcp_parrow x | _ => false)
val ltp_ppoly : lty -> bool = fn t =>
! (case lt_out t of LT.LT_POLY (_, [x]) => true | _ => false)
val ltp_pfct : lty -> bool = fn t =>
! (case lt_out t of LT.LT_FCT ([x], [y]) => true | _ => false)
(** plambda tyc-lty one-arm switches *)
fun tcw_parrow (tc, f, g) =
! (case tc_out tc of LT.TC_ARROW (_,[x],[y]) => f (x,y) | _ => g tc)
fun ltw_parrow (lt, f, g) =
(case lt_out lt
! of LT.LT_TYC tc =>
! (case tc_out tc of LT.TC_ARROW (_,[x],[y]) => f(x,y) | _ => g lt)
| _ => g lt)
fun ltw_ppoly (lt, f, g) =
! (case lt_out lt of LT.LT_POLY(ks,[x]) => f(ks,x) | _ => g lt)
fun ltw_pfct (lt, f, g) =
! (case lt_out lt of LT.LT_FCT([x],[y]) => f(x,y) | _ => g lt)
end (* top-level local *)
Index: ltydict.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltydict.sml,v
retrieving revision 1.2
retrieving revision 1.2.26.1
diff -C2 -d -r1.2 -r1.2.26.1
*** ltydict.sml 1 Jun 2000 18:33:26 -0000 1.2
--- ltydict.sml 11 Aug 2006 20:42:23 -0000 1.2.26.1
***************
*** 22,26 ****
struct
! local structure LT = LtyBasic
open LtyKernel
in
--- 22,26 ----
struct
! local
open LtyKernel
in
***************
*** 30,38 ****
structure TcDict = RedBlackMapFn(struct type ord_key = tyc
! val compare = tc_cmp
end)
structure LtDict = RedBlackMapFn(struct type ord_key = lty
! val compare = lt_cmp
end)
--- 30,38 ----
structure TcDict = RedBlackMapFn(struct type ord_key = tyc
! val compare = Lty.tc_cmp
end)
structure LtDict = RedBlackMapFn(struct type ord_key = lty
! val compare = Lty.lt_cmp
end)
Index: ltyextern.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltyextern.sml,v
retrieving revision 1.19.24.1
retrieving revision 1.19.24.2
diff -C2 -d -r1.19.24.1 -r1.19.24.2
*** ltyextern.sml 12 Jul 2006 22:02:12 -0000 1.19.24.1
--- ltyextern.sml 11 Aug 2006 20:42:23 -0000 1.19.24.2
***************
*** 7,10 ****
--- 7,11 ----
local structure PT = PrimTyc
structure DI = DebIndex
+ structure LT = Lty
structure LK = LtyKernel
structure PO = PrimOp (* really should not refer to this *)
***************
*** 42,47 ****
let val nt = lt_whnm lt
in (case ((* lt_outX *) lt_out nt, ts)
[...1095 lines suppressed...]
in
--- 908,925 ----
val t =
case lt_out lty of
! LT.LT_TYC t =>
ltc_tyc (tc_nvar_cvt tvoffs d t)
! | LT.LT_STR ts =>
ltc_str (rs ts)
! | LT.LT_FCT (ts, ts') =>
ltc_fct (rs ts, rs ts')
! | LT.LT_POLY (tks, ts) =>
ltc_poly (tks,
map (lt_nvar_cvt tvoffs (DI.next d)) ts)
! | LT.LT_CONT ts =>
ltc_cont (rs ts)
! | LT.LT_IND _ =>
bug "unexpected LT_IND in lt_nvar_cvt"
! | LT.LT_ENV _ =>
bug "unexpected LT_ENV in lt_nvar_cvt"
in
Index: ltykernel.sig
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltykernel.sig,v
retrieving revision 1.11.24.5
retrieving revision 1.11.24.6
diff -C2 -d -r1.11.24.5 -r1.11.24.6
*** ltykernel.sig 11 Aug 2006 04:09:23 -0000 1.11.24.5
--- ltykernel.sig 11 Aug 2006 20:42:23 -0000 1.11.24.6
***************
*** 2,82 ****
(* ltykernel.sig *)
! signature LTYKERNEL = sig
!
! (* definitions of kind and kind-environment *)
! type tkind
!
! datatype tkindI
! = TK_MONO (* ground mono tycon *)
! | TK_BOX (* boxed/tagged tycon *)
! | TK_SEQ of tkind list (* sequence of tycons *)
! | TK_FUN of tkind list * tkind (* tycon function *)
!
! (* definitions of named tyc variables *)
! type tvar = LambdaVar.lvar (* temporary, not used *)
! val mkTvar : unit -> tvar (* temporary, not used *)
!
! (* definitions of tyc and tyc-environment *)
! type tyc
! type tycEnv
! type token (* a hook to add new tyc *)
!
! datatype fflag (* calling conventions *)
! = FF_VAR of bool * bool (* is it fixed ? *)
! | FF_FIXED (* used after rep. analysis *)
!
! datatype rflag = RF_TMP (* tuple kind: a template *)
!
! datatype tycI
! = TC_VAR of DebIndex.index * int (* tyc variable *)
! | TC_NVAR of tvar (* named tyc variable *)
! | TC_PRIM of PrimTyc.primtyc (* primitive tyc *)
! | TC_FN of tkind list * tyc (* tyc abstraction *)
! | TC_APP of tyc * tyc list (* tyc application *)
! | TC_SEQ of tyc list (* tyc sequence *)
! | TC_PROJ of tyc * int (* tyc projection *)
!
! | TC_SUM of tyc list (* sum tyc *)
! | TC_FIX of (int * tyc * tyc list) * int (* recursive tyc *)
!
! | TC_TUPLE of rflag * tyc list (* std record tyc *)
! | TC_ARROW of fflag * tyc list * tyc list (* std function tyc *)
! | TC_PARROW of tyc * tyc (* special fun tyc, not used *)
!
! | TC_BOX of tyc (* boxed tyc *)
! | TC_ABS of tyc (* abstract tyc *)
! | TC_TOKEN of token * tyc (* extensible token tyc *)
! | TC_CONT of tyc list (* std continuation tyc *)
! | TC_IND of tyc * tycI (* indirect tyc thunk *)
! | TC_ENV of tyc * int * int * tycEnv (* tyc closure *)
! (* definition of lty *)
! type lty
! datatype ltyI
! = LT_TYC of tyc (* monomorphic type *)
! | LT_STR of lty list (* structure type *)
! | LT_FCT of lty list * lty list (* functor type *)
! | LT_POLY of tkind list * lty list (* polymorphic type *)
!
! | LT_CONT of lty list (* internal cont type *)
! | LT_IND of lty * ltyI (* indirect type thunk *)
! | LT_ENV of lty * int * int * tycEnv (* type closure *)
(** injections and projections on tkind, tyc, and lty *)
! val tk_inj : tkindI -> tkind
! val tc_inj : tycI -> tyc
! val lt_inj : ltyI -> lty
!
! val tk_out : tkind -> tkindI
! val tc_out : tyc -> tycI
! val lt_out : lty -> ltyI
!
! (** key comparison for tkind, tyc, and lty; used in pickling *)
! val tk_cmp : tkind * tkind -> order
! val tc_cmp : tyc * tyc -> order
! val lt_cmp : lty * lty -> order
! (** get the hash key of each lty, used by reps/coerce.sml; a hack! *)
! val lt_key : lty -> int
(** testing equivalence of tkinds, tycs, ltys, fflags, and rflags *)
--- 2,25 ----
(* ltykernel.sig *)
! signature LTYKERNEL =
! sig
! type tkind = Lty.tkind
! type fflag = Lty.fflag
! type rflag = Lty.rflag
! type tvar = Lty.tvar
! type tyc = Lty.tyc
! type lty = Lty.lty
! type token = Lty.token
! type tycEnv = Lty.tycEnv
(** injections and projections on tkind, tyc, and lty *)
! val tk_inj : Lty.tkindI -> tkind
! val tc_inj : Lty.tycI -> tyc
! val lt_inj : Lty.ltyI -> lty
! val tk_out : tkind -> Lty.tkindI
! val tc_out : tyc -> Lty.tycI
! val lt_out : lty -> Lty.ltyI
(** testing equivalence of tkinds, tycs, ltys, fflags, and rflags *)
***************
*** 91,105 ****
val lt_eqv_x : lty * lty -> bool
- (** utility functions on tycEnv *)
- exception tcUnbound of tycEnv * tyc
- val initTycEnv : tycEnv
- val tcInsert : tycEnv * (tyc list option * int) -> tycEnv
- val tcSplit : tycEnv -> ((tyc list option * int) * tycEnv) option
- (* val tycEnvOut : tycEnv -> tycI *)
-
- (** testing if a tyc (or lty) is in the normal form *)
- val tcp_norm : tyc -> bool
- val ltp_norm : lty -> bool
-
(** finding out the depth for a tyc's innermost-bound free variables *)
val tc_depth : tyc * DebIndex.depth -> DebIndex.depth
--- 34,37 ----
***************
*** 108,119 ****
val lt_nvars : lty -> tvar list
- (** utility functions on tkindEnv *)
- type tkindEnv
- exception tkUnbound
- val initTkEnv : tkindEnv
- val tkLookup : tkindEnv * int * int -> tkind
- val tkInsert : tkindEnv * tkind list -> tkindEnv
- val tkLookupFreeVars : tkindEnv * tyc -> tkind list option
-
(** utility functions for TC_ENV and LT_ENV types *)
val tcc_env : tyc * int * int * tycEnv -> tyc
--- 40,43 ----
***************
*** 151,159 ****
val wrap_token : token
- (** pretty printing of tkinds, tycs, and ltys *)
- (* (temporarily?) moved from ltybasic.sig *)
- val tk_print : tkind -> string
- val tc_print : tyc -> string
- val lt_print : lty -> string
-
end (* signature LTYKERNEL *)
--- 75,77 ----
Index: ltykernel.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/ltykernel.sml,v
retrieving revision 1.18.12.14
retrieving revision 1.18.12.15
diff -C2 -d -r1.18.12.14 -r1.18.12.15
*** ltykernel.sml 11 Aug 2006 04:09:23 -0000 1.18.12.14
--- ltykernel.sml 11 Aug 2006 20:42:23 -0000 1.18.12.15
***************
*** 1,3 ****
! (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *)
(* ltykernel.sml *)
--- 1,3 ----
! (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *)
(* ltykernel.sml *)
***************
*** 5,674 ****
struct
[...1031 lines suppressed...]
(** finding out the innermost binding depth for a tyc's free variables *)
fun tc_depth (x, d) =
! (* unfortunately we have to reduce everything to normal form
! * before we can talk about its list of free type variables. *)
! (case tc_vs (tc_norm x)
of NONE => bug "unexpected case in tc_depth"
| SOME [] => DI.top
! | SOME (a::_) => d + 1 - (#1(tvDecode a)))
fun tcs_depth ([], d) = DI.top
| tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
! (* these return the list of free NAMED tyvars, after nomalization *)
fun tc_nvars (tyc:tyc) =
! Lty.tc_nvars(tc_norm tyc)
+ fun lt_nvars (lty:lty) =
+ Lty.lt_nvars(lt_norm lty)
end (* abstraction LtyKernel *)
Index: pplty.sml
===================================================================
RCS file: /cvsroot/smlnj/sml-dist/src/compiler/FLINT/kernel/Attic/pplty.sml,v
retrieving revision 1.1.2.8
retrieving revision 1.1.2.9
diff -C2 -d -r1.1.2.8 -r1.1.2.9
*** pplty.sml 11 Aug 2006 04:09:23 -0000 1.1.2.8
--- pplty.sml 11 Aug 2006 20:42:23 -0000 1.1.2.9
***************
*** 7,16 ****
*)
! structure PPLTy =
struct
local
! structure LK = LtyKernel
structure PT = PrimTyc
structure PP = PrettyPrintNew
--- 7,16 ----
*)
! structure PPLty =
struct
local
! structure LK = Lty
structure PT = PrimTyc
structure PP = PrettyPrintNew
***************
*** 18,120 ****
in
! fun ppList ppstrm {sep, pp : 'a -> unit} list =
let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! in
! (ppSequence ppstrm
! {sep = fn ppstrm => (PP.string ppstrm sep;
! PP.break ppstrm {nsp=1, offset=0}),
! style = INCONSISTENT,
! pr = (fn _ => fn elem =>
! (openHOVBox 1;
! (* pps "("; *)
! pp elem;
! (* pps ")"; *)
! closeBox()))}
! list)
! end (* ppList *)
(* ppTKind : tkind -> unit
* Print a hashconsed representation of the kind *)
! fun ppTKind ppstrm (tk : LK.tkind) =
! let val ppTKind' = ppTKind ppstrm
! val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
val ppList' = ppList ppstrm
! fun ppTKindI(LK.TK_MONO) = pps "TK_MONO"
! | ppTKindI(LK.TK_BOX) = pps "TK_BOX"
! | ppTKindI(LK.TK_FUN (argTkinds, resTkind)) =
(* res_tkind is a TK_SEQ wrapping some tkinds
* These are produced by Elaborate/modules/instantiate.sml
*)
(openHOVBox 1;
! pps "TK_FUN (";
! ppList' {sep="* ", pp=ppTKind'} argTkinds;
! ppTKind' resTkind;
! pps ")";
closeBox())
! | ppTKindI(LK.TK_SEQ tkinds) =
! (openHOVBox 1;
! pps "TK_SEQ(";
! ppList' {sep=", ", pp=ppTKind'} tkinds;
! pps ")";
! closeBox())
! in ppTKindI (LK.tk_out tk)
end (* ppTKind *)
fun tycEnvFlatten(tycenv) =
! (print "flatten";
! (case LK.tcSplit(tycenv) of
! NONE => []
! | SOME(elem, rest) => elem::tycEnvFlatten(rest)))
! fun ppTycEnvElem ppstrm (tycop, i) =
! let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! in
! openHOVBox 1;
! (* pps "("; *)
! (case tycop of
! NONE => pps "*"
! | SOME(tycs) => ppList ppstrm {sep=",", pp=ppTyc ppstrm} tycs);
! pps ", ";
! PP.break ppstrm {nsp = 1, offset=0};
! ppi ppstrm i;
! (* pps ")"; *)
! closeBox()
end (* function ppTycEnvElem *)
! and ppTyc ppstrm (tycon : LK.tyc) =
(* FLINT variables are represented using deBruijn indices *)
! let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! (* eta-expansion of ppList to avoid
! value restriction *)
! val ppList' : {pp:'a -> unit, sep: string} -> 'a list -> unit = fn x => ppList ppstrm x
! val ppTKind' = ppTKind ppstrm
! val ppTyc' = ppTyc ppstrm
! fun ppTycI (LK.TC_VAR(depth, cnt)) =
! (pps "TC_VAR(";
! PP.break ppstrm {nsp=1,offset=1};
(* depth is a deBruijn index set in elabmod.sml/instantiate.sml *)
pps (DebIndex.di_print depth);
pps ",";
- PP.break ppstrm {nsp=1,offset=0};
(* cnt is computed in instantiate.sml sigToInst or
alternatively may be simply the IBOUND index *)
! pps (Int.toString cnt);
pps ")")
(* Named tyc VAR; is actually an lvar *)
! | ppTycI (LK.TC_NVAR tvar) =
! (pps "TC_NVAR(";
! PP.break ppstrm {nsp=1,offset=1};
! pps (Int.toString tvar);
! pps ")")
! | ppTycI (LK.TC_PRIM primtycon) =
! (pps "TC_PRIM(";
! PP.break ppstrm {nsp=1,offset=0};
pps (PT.pt_print primtycon);
pps ")")
! | ppTycI (LK.TC_FN (argTkinds, resultTyc)) =
(openHOVBox 1;
! pps "TC_FN(";
! PP.break ppstrm {nsp=1,offset=1};
! ppList' {sep="* ", pp=ppTKind'} argTkinds;
pps ",";
PP.break ppstrm {nsp=1,offset=0};
--- 18,118 ----
in
! fun ppSeq ppstrm {sep: string, pp : PP.stream -> 'a -> unit} (list: 'a list) =
let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! in ppSequence ppstrm
! {sep = fn ppstrm => (PP.string ppstrm sep;
! PP.break ppstrm {nsp=1, offset=0}),
! style = INCONSISTENT,
! pr = pp}
! list
! end (* ppSeq *)
!
! fun ppList ppstrm {sep: string, pp : PP.stream -> 'a -> unit} (list: 'a list) =
! ppClosedSequence ppstrm
! {front = fn ppstrm => (PP.string ppstrm "["),
! back = fn ppstrm => (PP.string ppstrm "]"),
! sep = fn ppstrm => (PP.string ppstrm sep;
! PP.break ppstrm {nsp=1, offset=0}),
! style = INCONSISTENT,
! pr = pp}
! list
(* ppTKind : tkind -> unit
* Print a hashconsed representation of the kind *)
! fun ppTKind pd ppstrm (tk : Lty.tkind) =
! if pd < 1 then pps ppstrm "<tk>" else
! let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! val ppTKind' = ppTKind (pd-1) ppstrm
val ppList' = ppList ppstrm
! fun ppTKindI(Lty.TK_MONO) = pps "MK"
! | ppTKindI(Lty.TK_BOX) = pps "BK"
! | ppTKindI(Lty.TK_FUN (argTkinds, resTkind)) =
(* res_tkind is a TK_SEQ wrapping some tkinds
* These are produced by Elaborate/modules/instantiate.sml
*)
(openHOVBox 1;
! pps "(";
! ppList' {sep=",", pp=ppTKind (pd-1)} argTkinds;
! pps "=>"; ppTKind' resTkind;
! pps ")";
closeBox())
! | ppTKindI(Lty.TK_SEQ tkinds) =
! (openHOVBox 1;
! pps "SK";
! ppList' {sep=",", pp=ppTKind (pd-1)} tkinds;
! closeBox())
! in ppTKindI (Lty.tk_outX tk)
end (* ppTKind *)
fun tycEnvFlatten(tycenv) =
! (case Lty.tcSplit(tycenv)
! of NONE => []
! | SOME(elem, rest) => elem::tycEnvFlatten(rest))
! fun ppTycEnvElem pd ppstrm ((tycop,i): Lty.tycEnvElem) =
! if pd < 1 then pps ppstrm "<tee>" else
! let val {openHOVBox, closeBox, pps, ppi, ...} = en_pp ppstrm
! in openHOVBox 1;
! pps "(";
! (case tycop
! of NONE => pps "*"
! | SOME(tycs) => ppList ppstrm {sep=",", pp=ppTyc (pd-1)} tycs);
! pps ",";
! ppi i;
! pps ")";
! closeBox()
end (* function ppTycEnvElem *)
! and ppTyc pd ppstrm (tycon : Lty.tyc) =
(* FLINT variables are represented using deBruijn indices *)
! if pd < 1 then pps ppstrm "<tyc>" else
! let val {openHOVBox, openHVBox, closeBox, pps, ppi, ...} = en_pp ppstrm
! val ppList' : {pp:PP.stream -> 'a -> unit, sep: string} -> 'a list -> unit =
! fn x => ppList ppstrm x
! (* eta-expansion of ppList to avoid value restriction *)
!
! val ppTKind' = ppTKind (pd-1) ppstrm
! val ppTyc' = ppTyc (pd-1) ppstrm
!
! fun ppTycI (Lty.TC_VAR(depth, cnt)) =
! (pps "TV(";
(* depth is a deBruijn index set in elabmod.sml/instantiate.sml *)
pps (DebIndex.di_print depth);
pps ",";
(* cnt is computed in instantiate.sml sigToInst or
alternatively may be simply the IBOUND index *)
! ppi cnt;
pps ")")
(* Named tyc VAR; is actually an lvar *)
! | ppTycI (Lty.TC_NVAR tvar) =
! (pps "NTV:"; ppi tvar)
! | ppTycI (Lty.TC_PRIM primtycon) =
! (pps "PRIM(";
pps (PT.pt_print primtycon);
pps ")")
! | ppTycI (Lty.TC_FN (argTkinds, resultTyc)) =
(openHOVBox 1;
! pps "FN(";
! ppList' {sep="*", pp=ppTKind (pd-1)} argTkinds;
pps ",";
PP.break ppstrm {nsp=1,offset=0};
***************
*** 122,183 ****
pps ")";
closeBox())
! | ppTycI (LK.TC_APP(contyc, tys)) =
(openHOVBox 1;
! pps "TC_APP(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' contyc;
pps ",";
PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep="* ", pp=ppTyc'} tys;
pps ")";
closeBox())
! | ppTycI (LK.TC_SEQ tycs) =
(openHOVBox 1;
! pps "TC_SEQ(";
! PP.break ppstrm {nsp=1,offset=1};
! ppList' {sep=", ", pp=ppTyc'} tycs;
pps ")";
closeBox())
! | ppTycI (LK.TC_PROJ(tycon, index)) =
(openHOVBox 1;
! pps "TC_PROJ(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' tycon;
! pps ", ";
PP.break ppstrm {nsp=1,offset=0};
pps (Int.toString index);
pps ")";
closeBox())
! | ppTycI (LK.TC_SUM(tycs)) =
! (pps "TC_SUM(";
! PP.break ppstrm {nsp=1,offset=1};
! ppList' {sep=", ", pp=ppTyc'} tycs;
pps ")")
(* TC_FIX is a recursive datatype constructor
from a (mutually-)recursive family *)
! | ppTycI (LK.TC_FIX((numStamps, datatypeFamily, freetycs), index)) =
(openHOVBox 1;
! pps "TC_FIX(";
! PP.break ppstrm {nsp=1,offset=1};
! print "LK.tc_out";
! (case (LK.tc_out datatypeFamily) of
! LK.TC_FN(params, rectyc) => (* generator function *)
let fun ppMus 0 = ()
! | ppMus i = (pps "mu";
! ppi ppstrm i;
pps " ";
ppMus (i - 1))
in
! (pps "RECTYCGEN(";
if (length params) > 0 then (pps "[";
! ppMus (length params);
pps "]")
else ();
! PP.break ppstrm {nsp=1,offset=1};
! print "LK.tc_out";
! (case (LK.tc_out rectyc) of
! (rectycI as LK.TC_FN _) => ppTycI rectycI
! | LK.TC_SEQ(dconstycs) =>
! ppTyc' (List.nth(dconstycs, index))
| tycI => ppTycI tycI);
PP.break ppstrm {nsp=0,offset=0};
--- 120,174 ----
pps ")";
closeBox())
! | ppTycI (Lty.TC_APP(contyc, tys)) =
(openHOVBox 1;
! pps "APP(";
ppTyc' contyc;
pps ",";
PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep=",", pp=ppTyc (pd-1)} tys;
pps ")";
closeBox())
! | ppTycI (Lty.TC_SEQ tycs) =
(openHOVBox 1;
! pps "SEQ(";
! ppList' {sep=",", pp=ppTyc (pd-1)} tycs;
pps ")";
closeBox())
! | ppTycI (Lty.TC_PROJ(tycon, index)) =
(openHOVBox 1;
! pps "PROJ(";
ppTyc' tycon;
! pps ",";
PP.break ppstrm {nsp=1,offset=0};
pps (Int.toString index);
pps ")";
closeBox())
! | ppTycI (Lty.TC_SUM(tycs)) =
! (pps "SUM(";
! ppList' {sep=",", pp=ppTyc (pd-1)} tycs;
pps ")")
(* TC_FIX is a recursive datatype constructor
from a (mutually-)recursive family *)
! | ppTycI (Lty.TC_FIX((numStamps, datatypeFamily, freetycs), index)) =
(openHOVBox 1;
! pps "FIX(";
! (case (Lty.tc_outX datatypeFamily) of
! Lty.TC_FN(params, rectyc) => (* generator function *)
let fun ppMus 0 = ()
! | ppMus i = (pps "mu";
! ppi i;
pps " ";
ppMus (i - 1))
in
! (pps "REC(";
if (length params) > 0 then (pps "[";
! ppi (length params);
pps "]")
else ();
! PP.break ppstrm {nsp=1,offset=1};
! (case (Lty.tc_outX rectyc) of
! (rectycI as Lty.TC_FN _) => ppTycI rectycI
! | Lty.TC_SEQ(dconstycs) =>
! ppTyc' (List.nth(dconstycs, index))
| tycI => ppTycI tycI);
PP.break ppstrm {nsp=0,offset=0};
***************
*** 199,203 ****
PP.break ppstrm {nsp=1, offset=0};
pps "freeTycs = ";
! ppList' {sep = ", ", pp = ppTyc'} freetycs;
pps ", ";
PP.break ppstrm {nsp=1, offset=0};
--- 190,194 ----
PP.break ppstrm {nsp=1, offset=0};
pps "freeTycs = ";
! ppList' {sep = ", ", pp = ppTyc} freetycs;
pps ", ";
PP.break ppstrm {nsp=1, offset=0};
***************
*** 206,269 ****
pps ")";
closeBox() *) )
! | ppTycI (LK.TC_ABS tyc) =
! (pps "TC_ABS(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' tyc;
pps ")")
! | ppTycI (LK.TC_BOX tyc) =
! (pps "TC_BOX(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' tyc;
pps ")")
(* rflag is a tuple kind template, a singleton datatype RF_TMP *)
! | ppTycI (LK.TC_TUPLE (rflag, tycs)) =
! (case tycs of
! [] => pps "UNIT"
! | _ => (pps "TC_TUPLE(";
! PP.break ppstrm {nsp=1,offset=1};
! ppList' {sep="* ", pp=ppTyc'} tycs;
! pps ")"))
(* fflag records the calling convention: either FF_FIXED or FF_VAR *)
! | ppTycI (LK.TC_ARROW (fflag, argTycs, resTycs)) =
! (pps "TC_ARROW(";
! PP.break ppstrm {nsp=1,offset=1};
! (case fflag of LK.FF_FIXED => pps "FF_FIXED"
! | LK.FF_VAR(b1, b2) => (pps "<FF_VAR>" (*;
! ppBool b1;
! pps ", ";
! ppBool b2;
! pps ")"*) ));
! ppList' {sep="* ", pp=ppTyc'} argTycs;
! pps ", ";
PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep="* ", pp=ppTyc'} resTycs;
pps ")")
(* According to ltykernel.sml comment, this arrow tyc is not used *)
! | ppTycI (LK.TC_PARROW (argTyc, resTyc)) =
! (pps "TC_PARROW(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' argTyc;
! pps ", ";
PP.break ppstrm {nsp=1,offset=0};
ppTyc' resTyc;
pps ")")
! | ppTycI (LK.TC_TOKEN (tok, tyc)) =
! (pps "TC_TOKEN(";
! PP.break ppstrm {nsp=1,offset=1};
! print "LK.token_name\n";
! pps (LK.token_name tok);
! pps ", ";
PP.break ppstrm {nsp=1,offset=0};
ppTyc' tyc;
pps ")")
! | ppTycI (LK.TC_CONT tycs) =
! (pps "TC_CONT(";
! PP.break ppstrm {nsp=1,offset=1};
! ppList' {sep=", ", pp=ppTyc'} tycs;
pps ")")
! | ppTycI (LK.TC_IND (tyc, tycI)) =
(openHOVBox 1;
! pps "TC_IND(";
! PP.break ppstrm {nsp=1,offset=1};
ppTyc' tyc;
pps ", ";
--- 197,253 ----
pps ")";
closeBox() *) )
! | ppTycI (Lty.TC_ABS tyc) =
! (pps "ABS(";
ppTyc' tyc;
pps ")")
! | ppTycI (Lty.TC_BOX tyc) =
! (pps "BOX(";
ppTyc' tyc;
pps ")")
(* rflag is a tuple kind template, a singleton datatype RF_TMP *)
! | ppTycI (Lty.TC_TUPLE(rflag, tycs)) =
! (ppClosedSequence ppstrm
! {front = (fn s => PP.string s "{"),
! sep = (fn s => PP.string s ","),
! back = (fn s => PP.string s "}"),
! pr = ppTyc (pd-1),
! style = INCONSISTENT}
! tycs)
(* fflag records the calling convention: either FF_FIXED or FF_VAR *)
! | ppTycI (Lty.TC_ARROW (fflag, argTycs, resTycs)) =
! (pps "ARR(";
! (case fflag of Lty.FF_FIXED => pps "FF_FIXED"
! | Lty.FF_VAR(b1, b2) =>
! (pps "<FF_VAR>" (*; ppBool b1; pps ",";
! ppBool b2; pps ")"*) ));
! pps ",";
PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep=",", pp=ppTyc (pd-1)} argTycs;
! pps ",";
! PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep=",", pp=ppTyc (pd-1)} resTycs;
pps ")")
(* According to ltykernel.sml comment, this arrow tyc is not used *)
! | ppTycI (Lty.TC_PARROW (argTyc, resTyc)) =
! (pps "PARR(";
ppTyc' argTyc;
! pps ",";
PP.break ppstrm {nsp=1,offset=0};
ppTyc' resTyc;
pps ")")
! | ppTycI (Lty.TC_TOKEN (tok, tyc)) =
! (pps "TOK(";
! pps (Lty.token_name tok);
! pps ",";
PP.break ppstrm {nsp=1,offset=0};
ppTyc' tyc;
pps ")")
! | ppTycI (Lty.TC_CONT tycs) =
! (pps "CONT(";
! ppList' {sep=", ", pp=ppTyc (pd-1)} tycs;
pps ")")
! | ppTycI (Lty.TC_IND (tyc, tycI)) =
(openHOVBox 1;
! pps "IND(";
ppTyc' tyc;
pps ", ";
***************
*** 272,306 ****
pps ")";
closeBox())
! | ppTycI (LK.TC_ENV (tyc, ol, nl, tenv)) =
! (openHOVBox 1;
! pps "TC_ENV(";
! PP.break ppstrm {nsp=1,offset=1};
! ppTyc' tyc;
! pps ", ";
! PP.break ppstrm {nsp=1,offset=0};
! pps "ol = ";
pps (Int.toString ol);
pps ", ";
! pps "nl = ";
pps (Int.toString nl);
! pps ", ";
PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep=", ", pp=(ppTycEnvElem ppstrm)} (tycEnvFlatten tenv);
closeBox())
! val _ = print "LK.tc_out 1 \n"
! in ppTycI (LK.tc_out tycon)
end (* ppTyc *)
! fun ppTycEnv ppstrm (tycEnv : LK.tycEnv) =
let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! in
! openHOVBox 1;
! pps "TycEnv(";
! ppList ppstrm {sep=", ", pp=ppTycEnvElem ppstrm} (tycEnvFlatten tycEnv);
! pps ")";
closeBox()
! end (* function ppTycEnv *)
end (* local *)
! end
--- 256,288 ----
pps ")";
closeBox())
! | ppTycI (Lty.TC_ENV (tyc, ol, nl, tenv)) =
! (openHVBox 1;
! pps "ENV(";
! pps "ol=";
pps (Int.toString ol);
pps ", ";
! pps "nl=";
pps (Int.toString nl);
! pps ",";
PP.break ppstrm {nsp=1,offset=0};
! ppTyc' tyc;
! pps ",";
! PP.break ppstrm {nsp=1,offset=0};
! ppList' {sep=",", pp=ppTycEnvElem (pd-1)} (tycEnvFlatten tenv);
closeBox())
! in ppTycI (Lty.tc_outX tycon)
end (* ppTyc *)
! fun ppTycEnv pd ppstrm (tycEnv : Lty.tycEnv) =
! if pd < 1 then pps ppstrm "<tycEnv>" else
let val {openHOVBox, closeBox, pps, ...} = en_pp ppstrm
! in openHOVBox 1;
! pps "TycEnv(";
! ppList ppstrm {sep=", ", pp=ppTycEnvElem (pd-1)} (tycEnvFlatten tycEnv);
! pps ")";
closeBox()
! end (* ppTycEnv *)
end (* local *)
! end (* structure PPLty *)
-------------------------------------------------------------------------
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