Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/compiler/FLINT/kernel/ltyextern.sml
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 17 - (view) (download)
Original Path: sml/branches/SMLNJ/src/compiler/FLINT/kernel/ltyextern.sml

1 : monnier 16 (* Copyright (c) 1997 YALE FLINT PROJECT *)
2 :     (* ltyextern.sml *)
3 :    
4 :     structure LtyExtern : LTYEXTERN =
5 :     struct
6 :    
7 :     local structure PT = PrimTyc
8 :     structure DI = DebIndex
9 :     structure LK = LtyKernel
10 :     structure PO = PrimOp (* really should not refer to this *)
11 :     structure FL = FLINT
12 :    
13 :     fun bug msg = ErrorMsg.impossible("LtyExtern: "^msg)
14 :     val say = Control.Print.say
15 :    
16 :     (** common utility functions *)
17 :     val tk_inj = LK.tk_inj
18 :     val tk_out = LK.tk_out
19 :    
20 :     val tc_inj = LK.tc_inj
21 :     val tc_out = LK.tc_out
22 :    
23 :     val lt_inj = LK.lt_inj
24 :     val lt_out = LK.lt_out
25 :    
26 :     val tcc_env = LK.tcc_env
27 :     val ltc_env = LK.ltc_env
28 :     val tc_whnm = LK.tc_whnm
29 :     val lt_whnm = LK.lt_whnm
30 :     val tc_norm = LK.tc_norm
31 :     val lt_norm = LK.lt_norm
32 :    
33 :     in
34 :    
35 :     open LtyBasic
36 :    
37 :     val tc_depth = LK.tc_depth
38 :     val tcs_depth = LK.tcs_depth
39 :    
40 :     (** instantiating a polymorphic type or an higher-order constructor *)
41 :     fun lt_inst (lt : lty, ts : tyc list) =
42 :     let val nt = lt_whnm lt
43 :     in (case ((* lt_outX *) lt_out nt, ts)
44 :     of (LK.LT_POLY(ks, b), ts) =>
45 :     let val nenv = LK.tcInsert(LK.initTycEnv, (SOME ts, 0))
46 :     in map (fn x => ltc_env(x, 1, 0, nenv)) b
47 :     end
48 :     | (_, []) => [nt] (* this requires further clarifications !!! *)
49 :     | _ => bug "incorrect lty instantiation in lt_inst")
50 :     end
51 :    
52 :     fun lt_pinst (lt : lty, ts : tyc list) =
53 :     (case lt_inst (lt, ts) of [y] => y | _ => bug "unexpected lt_pinst")
54 :    
55 :     val lt_inst_st = (map lt_norm) o lt_inst (* strict instantiation *)
56 :     val lt_pinst_st = lt_norm o lt_pinst (* strict instantiation *)
57 :    
58 :     exception TkTycChk
59 :     exception LtyAppChk
60 :    
61 :     fun tkSel (tk, i) =
62 :     (case (tk_out tk)
63 :     of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)
64 :     | _ => raise TkTycChk)
65 :    
66 :     fun tks_eqv (ks1, ks2) = tk_eqv(tkc_seq ks1, tkc_seq ks2)
67 :    
68 :     fun tkApp (tk, tks) =
69 :     (case (tk_out tk)
70 :     of LK.TK_FUN(a, b) => if tks_eqv(a, tks) then b else raise TkTycChk
71 :     | _ => raise TkTycChk)
72 :    
73 :     (* Warning: the following tkTyc function has not considered the
74 :     * occurence of .TK_BOX, in other words, if there is TK_BOX present,
75 :     * then the tk_tyc checker will produce wrong results. (ZHONG)
76 :     *)
77 :     fun tk_tyc (t, kenv) =
78 :     let fun g x =
79 :     (case tc_out x
80 :     of (LK.TC_VAR (i, j)) => tkLookup(kenv, i, j)
81 :     | (LK.TC_NVAR _) => bug "TC_NVAR not supported yet in tk_tyc"
82 :     | (LK.TC_PRIM pt) => tkc_int (PrimTyc.pt_arity pt)
83 :     | (LK.TC_FN(ks, tc)) =>
84 :     tkc_fun(ks, tk_tyc(tc, tkInsert(kenv, ks)))
85 :     | (LK.TC_APP (tc, tcs)) => tkApp(g tc, map g tcs)
86 :     | (LK.TC_SEQ tcs) => tkc_seq (map g tcs)
87 :     | (LK.TC_PROJ(tc, i)) => tkSel(g tc, i)
88 :     | (LK.TC_SUM tcs) =>
89 :     let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs
90 :     in tkc_mono
91 :     end
92 :     | (LK.TC_FIX ((n, tc, ts), i)) =>
93 :     let val k = g tc
94 :     val nk = case ts of [] => k
95 :     | _ => tkApp(k, map g ts)
96 :     in (case (tk_out nk)
97 :     of LK.TK_FUN(a, b) =>
98 :     let val arg = case a of [x] => x
99 :     | _ => tkc_seq a
100 :     in if tk_eqv(arg, b) then
101 :     (if n = 1 then b else tkSel(arg, i))
102 :     else raise TkTycChk
103 :     end
104 :     | _ => raise TkTycChk)
105 :     end
106 :     | (LK.TC_ABS tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)
107 :     | (LK.TC_BOX tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)
108 :     | (LK.TC_TUPLE (_,tcs)) =>
109 :     let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs
110 :     in tkc_mono
111 :     end
112 :     | (LK.TC_ARROW (_, ts1, ts2)) =>
113 :     let val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts1
114 :     val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts2
115 :     in tkc_mono
116 :     end
117 :     | _ => bug "unexpected TC_ENV or TC_CONT in tk_tyc")
118 :     in g t
119 :     end
120 :    
121 :     and tk_chk kenv (k, tc) =
122 :     if tk_eqv(k, tk_tyc(tc, kenv)) then () else raise TkTycChk
123 :    
124 :     fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =
125 :     let val nt = lt_whnm lt
126 :     in (case ((* lt_outX *) lt_out nt, ts)
127 :     of (LK.LT_POLY(ks, b), ts) =>
128 :     let val _ = ListPair.app (tk_chk kenv) (ks, ts)
129 :     fun h x = ltc_env(x, 1, 0, tcInsert(initTycEnv, (SOME ts, 0)))
130 :     in map h b
131 :     end
132 :     | (_, []) => [nt] (* ? problematic *)
133 :     | _ => raise LtyAppChk)
134 :     end
135 :    
136 :     (** a special lty application --- used inside the translate/specialize.sml *)
137 :     fun lt_sp_adj(ks, lt, ts, dist, bnl) =
138 :     let fun h(abslevel, ol, nl, tenv) =
139 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
140 :     else if abslevel > 0 then
141 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
142 :     else bug "unexpected cases in ltAdjSt"
143 :    
144 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
145 :     val nt = h(dist, 1, bnl, btenv)
146 :     in nt (* was lt_norm nt *)
147 :     end
148 :    
149 :     (** a special tyc application --- used inside the translate/specialize.sml *)
150 :     fun tc_sp_adj(ks, tc, ts, dist, bnl) =
151 :     let fun h(abslevel, ol, nl, tenv) =
152 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
153 :     else if abslevel > 0 then
154 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
155 :     else bug "unexpected cases in tcAdjSt"
156 :    
157 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
158 :     val nt = h(dist, 1, bnl, btenv)
159 :     in nt (* was tc_norm nt *)
160 :     end
161 :    
162 :     (** sinking the lty one-level down --- used inside the specialize.sml *)
163 :     fun lt_sp_sink (ks, lt, d, nd) =
164 :     let fun h(abslevel, ol, nl, tenv) =
165 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
166 :     else if abslevel > 0 then
167 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
168 :     else bug "unexpected cases in ltSinkSt"
169 :     val nt = h(nd-d, 0, 1, initTycEnv)
170 :     in nt (* was lt_norm nt *)
171 :     end
172 :    
173 :     (** sinking the tyc one-level down --- used inside the specialize.sml *)
174 :     fun tc_sp_sink (ks, tc, d, nd) =
175 :     let fun h(abslevel, ol, nl, tenv) =
176 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
177 :     else if abslevel > 0 then
178 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
179 :     else bug "unexpected cases in ltSinkSt"
180 :     val nt = h(nd-d, 0, 1, initTycEnv)
181 :     in nt (* was tc_norm nt *)
182 :     end
183 :    
184 :     (** utility functions used in CPS *)
185 :     fun lt_iscont lt =
186 :     (case lt_out lt
187 :     of LK.LT_CONT _ => true
188 :     | LK.LT_TYC tc =>
189 :     (case tc_out tc of LK.TC_CONT _ => true | _ => false)
190 :     | _ => false)
191 :    
192 :     fun ltw_iscont (lt, f, g, h) =
193 :     (case lt_out lt
194 :     of LK.LT_CONT t => f t
195 :     | LK.LT_TYC tc =>
196 :     (case tc_out tc of LK.TC_CONT x => g x | _ => h lt)
197 :     | _ => h lt)
198 :    
199 :    
200 :     fun tc_bug tc s = bug (s ^ "\n\n" ^ (tc_print tc) ^ "\n\n")
201 :     fun lt_bug lt s = bug (s ^ "\n\n" ^ (lt_print lt) ^ "\n\n")
202 :    
203 :     (** other misc utility functions *)
204 :     fun tc_select(tc, i) =
205 :     (case tc_out tc
206 :     of LK.TC_TUPLE (_,zs) =>
207 :     ((List.nth(zs, i)) handle _ => bug "wrong TC_TUPLE in tc_select")
208 :     | _ => tc_bug tc "wrong TCs in tc_select")
209 :    
210 :     fun lt_select(t, i) =
211 :     (case lt_out t
212 :     of LK.LT_STR ts =>
213 :     ((List.nth(ts, i)) handle _ => bug "incorrect LT_STR in lt_select")
214 :     | LK.LT_PST ts =>
215 :     let fun h [] = bug "incorrect LT_PST in lt_select"
216 :     | h ((j,a)::r) = if i=j then a else h r
217 :     in h ts
218 :     end
219 :     | LK.LT_TYC tc => ltc_tyc(tc_select(tc, i))
220 :     | _ => bug "incorrect lambda types in lt_select")
221 :    
222 :     fun tc_swap t =
223 :     (case (tc_out t)
224 :     of LK.TC_ARROW ((r1,r2), [s1], [s2]) => tcc_arrow((r2,r1), [s2], [s1])
225 :     | _ => bug "unexpected tycs in tc_swap")
226 :    
227 :     fun lt_swap t =
228 :     (case (lt_out t)
229 :     of (LK.LT_POLY (ks, [x])) => ltc_poly(ks, [lt_swap x])
230 :     | (LK.LT_TYC x) => ltc_tyc(tc_swap x)
231 :     | _ => bug "unexpected type in lt_swap")
232 :    
233 :     (** functions that manipulate the FLINT function and record types *)
234 :     fun ltc_fkfun (FL.FK_FCT, atys, rtys) =
235 :     ltc_fct (atys, rtys)
236 :     | ltc_fkfun (FL.FK_FUN {fixed, ...}, atys, rtys) =
237 :     ltc_arrow(fixed, atys, rtys)
238 :    
239 :     fun ltd_fkfun lty =
240 :     if ltp_fct lty then ltd_fct lty
241 :     else let val (_, atys, rtys) = ltd_arrow lty
242 :     in (atys, rtys)
243 :     end
244 :    
245 :     fun ltc_rkind (FL.RK_TUPLE _, lts) = ltc_tuple lts
246 :     | ltc_rkind (FL.RK_STRUCT, lts) = ltc_str lts
247 :     | ltc_rkind (FL.RK_VECTOR t, _) = ltc_vector (ltc_tyc t)
248 :    
249 :     fun ltd_rkind (lt, i) = lt_select (lt, i)
250 :    
251 :     (** a version of ltc_arrow with singleton argument and return result *)
252 :     val ltc_arw = ltc_parrow
253 :    
254 :     (** not knowing what FUNCTION this is, to build a fct or an arw *)
255 :     fun ltc_fun (x, y) =
256 :     (case (lt_out x, lt_out y)
257 :     of (LK.LT_TYC _, LK.LT_TYC _) => ltc_parrow(x, y)
258 :     | _ => ltc_pfct(x, y))
259 :    
260 :     (* lt_arrow used by chkflint.sml, checklty.sml, chkplexp.sml, convert.sml
261 :     * and wrapping.sml only
262 :     *)
263 :     fun lt_arrow t =
264 :     (case (lt_out t)
265 :     of (LK.LT_FCT([t1], [t2])) => (t1, t2)
266 :     | (LK.LT_FCT(_, _)) => bug "unexpected case in lt_arrow"
267 :     | (LK.LT_CONT [t]) => (t, ltc_void)
268 :     | _ => (ltd_parrow t) handle _ =>
269 :     bug ("unexpected lt_arrow --- more info: \n\n"
270 :     ^ (lt_print t) ^ "\n\n"))
271 :    
272 :     (* lt_arrowN used by flintnm.sml and ltysingle.sml only, should go away soon *)
273 :     fun lt_arrowN t =
274 :     (case (lt_out t)
275 :     of (LK.LT_FCT(ts1, ts2)) => (ts1, ts2)
276 :     | (LK.LT_CONT ts) => (ts, [])
277 :     | _ => (let val (_, s1, s2) = ltd_arrow t
278 :     in (s1, s2)
279 :     end))
280 :    
281 :     fun tc_upd_prim tc =
282 :     let fun h(LK.TC_PRIM pt) =
283 :     if PT.ubxupd pt then PO.UNBOXEDUPDATE
284 :     else if PT.bxupd pt then PO.BOXEDUPDATE
285 :     else PO.UPDATE
286 :     | h(LK.TC_TUPLE _ | LK.TC_ARROW _) = PO.BOXEDUPDATE
287 :     | h(LK.TC_FIX ((1,tc,ts), 0)) =
288 :     let val ntc = case ts of [] => tc
289 :     | _ => tcc_app(tc, ts)
290 :     in (case (tc_out ntc)
291 :     of LK.TC_FN([k],b) => h (tc_out b)
292 :     | _ => PO.UPDATE)
293 :     end
294 :     | h(LK.TC_SUM tcs) =
295 :     let fun g (a::r) = if tc_eqv(a, tcc_unit) then g r else false
296 :     | g [] = true
297 :     in if (g tcs) then PO.UNBOXEDUPDATE else PO.UPDATE
298 :     end
299 :     | h _ = PO.UPDATE
300 :     in h(tc_out tc)
301 :     end
302 :    
303 :    
304 :     end (* top-level local *)
305 :     end (* structure LtyExtern *)
306 :    

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