Annotation of /sml/trunk/src/compiler/FLINT/kernel/ltybasic.sml

Parent Directory | Revision Log

---

Revision 65 - (view) (download)

1 :	monnier	16	(* Copyright (c) 1997 YALE FLINT PROJECT *)
2 :			(* ltybasic.sml *)
3 :
4 :			structure LtyBasic : LTYBASIC =
5 :			struct
6 :
7 :			local structure PT = PrimTyc
8 :			structure DI = DebIndex
9 :			structure LK = LtyKernel
10 :
11 :			fun bug msg = ErrorMsg.impossible("LtyExtern: "^msg)
12 :			val say = Control.Print.say
13 :
14 :			(** common utility functions *)
15 :			val tk_inj = LK.tk_inj
16 :			val tk_out = LK.tk_out
17 :
18 :			val tc_inj = LK.tc_inj
19 :			val tc_out = LK.tc_out
20 :
21 :			val lt_inj = LK.lt_inj
22 :			val lt_out = LK.lt_out
23 :
24 :			val tcc_env = LK.tcc_env
25 :			val ltc_env = LK.ltc_env
26 :
27 :			val itos = Int.toString
28 :			fun plist(p, []) = ""
29 :			| plist(p, x::xs) =
30 :			(p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))
31 :
32 :	monnier	45	fun pfflag (LK.FF_VAR b) =
33 :			let fun pff (true, true) = "rr" | pff (true, false) = "rc"
34 :			| pff (false, true) = "cr" | pff (false, false) = "cc"
35 :			in pff b
36 :			end
37 :			| pfflag (LK.FF_FIXED) = "f"
38 :
39 :			fun parw(p, (ff, t1, t2)) =
40 :			"<" ^ (p t1) ^ "> -" ^ pfflag ff ^ "-> <" ^ (p t2) ^ ">"
41 :	monnier	16	in
42 :
43 :			open LtyDef
44 :
45 :			(** new a type variable, currently not used *)
46 :			val mkTvar : unit -> tvar = LK.mkTvar
47 :
48 :			(** utility functions for constructing tkinds *)
49 :			fun tkc_arg n =
50 :			let fun h (n, r) = if n < 1 then r else h(n-1, tkc_mono::r)
51 :			in h(n, [])
52 :			end
53 :
54 :	monnier	45	val tkc_fn1 = tkc_fun(tkc_arg 1, tkc_mono)
55 :			val tkc_fn2 = tkc_fun(tkc_arg 2, tkc_mono)
56 :			val tkc_fn3 = tkc_fun(tkc_arg 3, tkc_mono)
57 :	monnier	16
58 :			fun tkc_int 0 = tkc_mono
59 :			| tkc_int 1 = tkc_fn1
60 :			| tkc_int 2 = tkc_fn2
61 :			| tkc_int 3 = tkc_fn3
62 :	monnier	45	| tkc_int i = tkc_fun(tkc_arg i, tkc_mono)
63 :	monnier	16
64 :	monnier	45	(** primitive fflags and rflags *)
65 :			val ffc_plambda = ffc_var (false, false)
66 :			val ffc_rrflint = ffc_var (true, true)
67 :
68 :			fun ffc_fspec (x as LK.FF_FIXED, (true,true)) = x
69 :			| ffc_fspec (x as LK.FF_VAR _, nx) = ffc_var nx
70 :			| ffc_fspec _ = bug "unexpected case in ffc_fspec"
71 :
72 :			fun ffd_fspec (LK.FF_FIXED) = (true,true)
73 :			| ffd_fspec (LK.FF_VAR x) = x
74 :
75 :	monnier	16	(** utility functions for constructing tycs *)
76 :			val tcc_int = tcc_prim PT.ptc_int31
77 :			val tcc_int32 = tcc_prim PT.ptc_int32
78 :			val tcc_real = tcc_prim PT.ptc_real
79 :			val tcc_string = tcc_prim PT.ptc_string
80 :			val tcc_exn = tcc_prim PT.ptc_exn
81 :			val tcc_void = tcc_prim PT.ptc_void
82 :			val tcc_unit = tcc_tuple []
83 :			val tcc_bool =
84 :			let val tbool = tcc_sum [tcc_unit, tcc_unit]
85 :			val tsig_bool = tcc_fn ([tkc_mono], tbool)
86 :			in tcc_fix((1, tsig_bool, []), 0)
87 :			end
88 :
89 :			val tcc_list = (* not exported, used for the printing purpose *)
90 :			let val alpha = tcc_var (DI.innermost, 0)
91 :			val tlist = tcc_var (DI.innersnd, 0)
92 :			val alist = tcc_app (tlist, [alpha])
93 :			val tcc_cons = tcc_tuple [alpha, alist]
94 :			val tlist = tcc_fn([tkc_mono], tcc_sum [tcc_cons, tcc_unit])
95 :			(** the order here should be consistent with
96 :			that in basics/basictypes.sml **)
97 :			val tsig_list = tcc_fn([tkc_int 1], tlist)
98 :			in tcc_fix((1, tsig_list, []), 0)
99 :			end
100 :
101 :			fun tcc_tv i = tcc_var(DI.innermost, i)
102 :			fun tcc_ref x = tcc_app(tcc_prim PT.ptc_ref, [x])
103 :			fun tcc_array x = tcc_app(tcc_prim PT.ptc_array, [x])
104 :			fun tcc_vector x = tcc_app(tcc_prim PT.ptc_vector, [x])
105 :			fun tcc_etag x = tcc_app(tcc_prim PT.ptc_etag, [x])
106 :
107 :			(** primitive lambda ltys *)
108 :			val ltc_int = ltc_tyc tcc_int
109 :			val ltc_int32 = ltc_tyc tcc_int32
110 :			val ltc_real = ltc_tyc tcc_real
111 :			val ltc_string = ltc_tyc tcc_string
112 :			val ltc_exn = ltc_tyc tcc_exn
113 :			val ltc_void = ltc_tyc tcc_void
114 :			val ltc_unit = ltc_tyc tcc_unit
115 :			val ltc_bool = ltc_tyc tcc_bool
116 :
117 :			val ltc_tv = ltc_tyc o tcc_tv
118 :			val ltc_ref = ltc_tyc o tcc_ref o ltd_tyc
119 :			val ltc_array = ltc_tyc o tcc_array o ltd_tyc
120 :			val ltc_vector = ltc_tyc o tcc_vector o ltd_tyc
121 :			val ltc_etag = ltc_tyc o tcc_etag o ltd_tyc
122 :
123 :			val ltc_top = ltc_ppoly([tkc_mono], ltc_tv 0)
124 :
125 :			(***************************************************************************
126 :			* UTILITY FUNCTIONS FOR TESTING EQUIVALENCE *
127 :			***************************************************************************)
128 :
129 :	monnier	45	(** testing equivalence of tkinds, tycs, ltys, fflags, and rflags *)
130 :	monnier	16	val tk_eqv : tkind * tkind -> bool = LK.tk_eqv
131 :			val tc_eqv : tyc * tyc -> bool = LK.tc_eqv
132 :			val lt_eqv : lty * lty -> bool = LK.lt_eqv
133 :	monnier	45	val ff_eqv : fflag * fflag -> bool = LK.ff_eqv
134 :			val rf_eqv : rflag * rflag -> bool = LK.rf_eqv
135 :	monnier	16
136 :			(** testing the equivalence for tycs and ltys with relaxed constraints *)
137 :	monnier	45	val tc_eqv_x : tyc * tyc -> bool = LK.tc_eqv_x
138 :			val lt_eqv_x : lty * lty -> bool = LK.lt_eqv_x
139 :	monnier	16	val tc_eqv_bx : tyc * tyc -> bool = LK.tc_eqv_bx
140 :			val lt_eqv_bx : lty * lty -> bool = LK.lt_eqv_bx
141 :
142 :			(***************************************************************************
143 :			* UTILITY FUNCTIONS FOR PRETTY PRINTING *
144 :			***************************************************************************)
145 :
146 :			(** pretty printing of tkinds, tycs, and ltys *)
147 :			fun tk_print (x : tkind) =
148 :			let fun g (LK.TK_MONO) = "K0"
149 :			| g (LK.TK_BOX) = "KB0"
150 :	monnier	45	| g (LK.TK_FUN (ks, k)) =
151 :			"<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
152 :	monnier	16	| g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"
153 :			in g (tk_out x)
154 :			end
155 :
156 :			fun tc_print (x : tyc) =
157 :			let fun g (LK.TC_VAR(i,j)) = "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
158 :			| g (LK.TC_NVAR(v,d,i)) = "NTV(v" ^ (itos v) ^ "," ^ (itos d)
159 :			^ "," ^ (itos i) ^ ")"
160 :			| g (LK.TC_PRIM pt) = PT.pt_print pt
161 :			| g (LK.TC_FN(ks, t)) =
162 :	monnier	45	"(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
163 :	monnier	16	| g (LK.TC_APP(t, [])) = tc_print t ^ "[]"
164 :			| g (LK.TC_APP(t, zs)) =
165 :			(tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
166 :			| g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"
167 :			| g (LK.TC_PROJ (t, i)) =
168 :			"TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
169 :			| g (LK.TC_SUM tcs) =
170 :			"TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
171 :			| g (LK.TC_FIX ((_, tc, ts), i)) =
172 :			if tc_eqv(x,tcc_bool) then "B"
173 :			else if tc_eqv(x,tcc_list) then "LST"
174 :			else (let val ntc = case ts of [] => tc
175 :			| _ => tcc_app(tc, ts)
176 :	monnier	45	in ("DT{" ^ "DATA" (* (tc_print ntc) *)
177 :			^ "===" ^ (itos i) ^ "}")
178 :	monnier	16	end)
179 :			| g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"
180 :			| g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"
181 :	monnier	45	| g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"
182 :			| g (LK.TC_ARROW (ff,z1,z2)) =
183 :			parw(fn u => plist(tc_print,u),(ff,z1,z2))
184 :	monnier	16	| g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"
185 :	monnier	45	| g (LK.TC_TOKEN (k, t)) =
186 :			if LK.token_isvalid k then
187 :			(LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
188 :			else bug "unexpected TC_TOKEN tyc in tc_print"
189 :	monnier	16	| g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
190 :			| g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"
191 :			| g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"
192 :			in g (tc_out x)
193 :			end (* function tc_print *)
194 :
195 :			fun lt_print (x : lty) =
196 :			let fun h (i, t) = "(" ^ (itos i) ^ "," ^ (lt_print t) ^ ")"
197 :
198 :			fun g (LK.LT_TYC t) = tc_print t
199 :			| g (LK.LT_STR zs) = "S{" ^ (plist(lt_print, zs)) ^ "}"
200 :			| g (LK.LT_PST zs) = "PS{" ^ (plist(h, zs)) ^ "}"
201 :			| g (LK.LT_FCT (ts1,ts2)) =
202 :			"(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
203 :			^ (plist(lt_print, ts2)) ^ ")"
204 :			| g (LK.LT_POLY(ks, ts)) =
205 :	monnier	45	"(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
206 :	monnier	16	| g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"
207 :			| g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"
208 :			| g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"
209 :
210 :			in g (lt_out x)
211 :			end (* function lt_print *)
212 :
213 :			(** finding out the depth for a tyc's innermost-bound free variables *)
214 :			val tc_depth : tyc * depth -> depth = LK.tc_depth
215 :			val tcs_depth: tyc list * depth -> depth = LK.tcs_depth
216 :
217 :			(** adjusting an lty or tyc from one depth to another *)
218 :			fun lt_adj (lt, d, nd) =
219 :	monnier	45	if d = nd then lt
220 :			else ltc_env(lt, 0, nd - d, LK.initTycEnv)
221 :	monnier	16
222 :			fun tc_adj (tc, d, nd) =
223 :	monnier	45	if d = nd then tc
224 :			else tcc_env(tc, 0, nd - d, LK.initTycEnv)
225 :	monnier	16
226 :	monnier	45	(** the following functions does the smiliar thing as lt_adj and
227 :			tc_adj; it adjusts an lty (or tyc) from depth d+k to depth nd+k,
228 :			assuming the last k levels are type abstractions. So lt_adj
229 :			is really lt_adj_k with k set to 0. Both functions are currently
230 :			called inside the lcontract.sml only. *)
231 :			local
232 :			fun mkTycEnv (i, k, dd, e) =
233 :			if i >= k then e else mkTycEnv(i+1, k, dd, LK.tcInsert(e,(NONE, dd+i)))
234 :
235 :			in
236 :			fun lt_adj_k (lt, d, nd, k) =
237 :			if d = nd then lt
238 :			else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
239 :
240 :			fun tc_adj_k (tc, d, nd, k) =
241 :	monnier	16	if d = nd then tc
242 :	monnier	45	else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
243 :	monnier	16
244 :	monnier	45	end (* lt_adj_k and tc_adj_k *)
245 :
246 :	monnier	16	(** automatically flattening the argument or the result type *)
247 :			val lt_autoflat : lty -> bool * lty list * bool = LK.lt_autoflat
248 :
249 :	monnier	45	(** testing if a tyc is a unknown constructor *)
250 :			val tc_unknown : tyc -> bool = LK.tc_unknown
251 :
252 :	monnier	16	(***************************************************************************
253 :			* UTILITY FUNCTIONS ON TKIND ENVIRONMENT *
254 :			***************************************************************************)
255 :
256 :	league	65	type tkindEnv = LK.tkindEnv
257 :			exception tkUnbound = LK.tkUnbound
258 :			val initTkEnv = LK.initTkEnv
259 :			val tkLookup = LK.tkLookup
260 :			val tkInsert = LK.tkInsert
261 :	monnier	16
262 :			(***************************************************************************
263 :			* UTILITY FUNCTIONS ON TYC ENVIRONMENT *
264 :			***************************************************************************)
265 :
266 :			exception tcUnbound = LK.tcUnbound
267 :			type tycEnv = LK.tycEnv
268 :			val initTycEnv = LK.initTycEnv
269 :			val tcInsert = LK.tcInsert
270 :
271 :			(***************************************************************************
272 :			* UTILITY FUNCTIONS ON LTY ENVIRONMENT *
273 :			***************************************************************************)
274 :
275 :			(** utility values and functions on ltyEnv *)
276 :			type ltyEnv = (lty * DebIndex.depth) IntmapF.intmap
277 :
278 :			exception ltUnbound
279 :			val initLtyEnv : ltyEnv = IntmapF.empty
280 :
281 :			fun ltLookup (venv, lv, nd) =
282 :			let val (lt, d) = (IntmapF.lookup venv lv) handle _ =>
283 :			(say "**** hmmm, I didn't find the variable ";
284 :			say (Int.toString lv); say "\n";
285 :			raise ltUnbound)
286 :			in if d=nd then lt
287 :			else if d > nd then bug "unexpected depth info in ltLookup"
288 :			else ltc_env(lt, 0, nd - d, LK.initTycEnv)
289 :			end
290 :
291 :			fun ltInsert (venv, lv, lt, d) = IntmapF.add(venv, lv, (lt, d))
292 :
293 :			end (* top-level local *)
294 :			end (* structure LtyBasic *)
295 :

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0