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/branches/SMLNJ/src/compiler/FLINT/kernel/ltyextern.sml
ViewVC logotype

Annotation of /sml/branches/SMLNJ/src/compiler/FLINT/kernel/ltyextern.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 24 - (view) (download)

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 :    
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 :     val tc_whnm = LK.tc_whnm
27 :     val lt_whnm = LK.lt_whnm
28 :     val tc_norm = LK.tc_norm
29 :     val lt_norm = LK.lt_norm
30 :    
31 :     in
32 :    
33 :     open LtyBasic
34 :    
35 :     val tc_depth = LK.tc_depth
36 :     val tcs_depth = LK.tcs_depth
37 :    
38 :     (** instantiating a polymorphic type or an higher-order constructor *)
39 :     fun lt_inst (lt : lty, ts : tyc list) =
40 :     let val nt = lt_whnm lt
41 :     in (case ((* lt_outX *) lt_out nt, ts)
42 :     of (LK.LT_POLY(ks, b), ts) =>
43 : monnier 24 let fun h x = ltc_env(x, 1, 0, LK.tcInsert(LK.initTycEnv, (SOME ts, 0)))
44 :     in map h b
45 : monnier 16 end
46 :     | (_, []) => [nt] (* this requires further clarifications !!! *)
47 :     | _ => bug "incorrect lty instantiation in lt_inst")
48 : monnier 24 end
49 : monnier 16
50 :     val lt_inst_st = (map lt_norm) o lt_inst (* strict instantiation *)
51 :    
52 :     exception TkTycChk
53 :     exception LtyAppChk
54 :    
55 :     fun tkSel (tk, i) =
56 :     (case (tk_out tk)
57 :     of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)
58 :     | _ => raise TkTycChk)
59 :    
60 : monnier 24 fun tkApp (tk1, tk2) =
61 :     (case (tk_out tk1)
62 :     of LK.TK_FUN(a, b) => if tk_eqv(a, tk2) then b else raise TkTycChk
63 : monnier 16 | _ => raise TkTycChk)
64 :    
65 : monnier 24 val tkc_mono = tk_inj (LK.TK_MONO)
66 :     val tkc_seq = tk_inj o LK.TK_SEQ
67 :     val tkc_fun = tk_inj o LK.TK_FUN
68 :     fun tkc_arity 0 = tkc_mono
69 :     | tkc_arity n =
70 :     let fun h(n, r) = if n > 0 then h(n-1, tkc_mono::r)
71 :     else tkc_fun(tkc_seq r, tkc_mono)
72 :     in h(n, [])
73 :     end
74 :    
75 : monnier 16 (* Warning: the following tkTyc function has not considered the
76 :     * occurence of .TK_BOX, in other words, if there is TK_BOX present,
77 :     * then the tk_tyc checker will produce wrong results. (ZHONG)
78 :     *)
79 :     fun tk_tyc (t, kenv) =
80 :     let fun g x =
81 :     (case tc_out x
82 :     of (LK.TC_VAR (i, j)) => tkLookup(kenv, i, j)
83 :     | (LK.TC_NVAR _) => bug "TC_NVAR not supported yet in tk_tyc"
84 : monnier 24 | (LK.TC_PRIM pt) => tkc_arity (PrimTyc.pt_arity pt)
85 : monnier 16 | (LK.TC_FN(ks, tc)) =>
86 : monnier 24 tkc_fun(tkc_seq ks, tk_tyc(tc, tkInsert(kenv, ks)))
87 :     | (LK.TC_APP (tc, tcs)) => tkApp(g tc, tkc_seq(map g tcs))
88 : monnier 16 | (LK.TC_SEQ tcs) => tkc_seq (map g tcs)
89 :     | (LK.TC_PROJ(tc, i)) => tkSel(g tc, i)
90 :     | (LK.TC_SUM tcs) =>
91 :     let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs
92 :     in tkc_mono
93 :     end
94 :     | (LK.TC_FIX ((n, tc, ts), i)) =>
95 :     let val k = g tc
96 :     val nk = case ts of [] => k
97 : monnier 24 | _ => tkApp(k, tkc_seq(map g ts))
98 : monnier 16 in (case (tk_out nk)
99 :     of LK.TK_FUN(a, b) =>
100 : monnier 24 if tk_eqv(a, b) then tkSel(a, i)
101 :     else raise TkTycChk
102 : monnier 16 | _ => raise TkTycChk)
103 :     end
104 :     | (LK.TC_ABS tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)
105 :     | (LK.TC_BOX tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)
106 : monnier 24 | (LK.TC_TUPLE tcs) =>
107 : monnier 16 let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs
108 :     in tkc_mono
109 :     end
110 :     | (LK.TC_ARROW (_, ts1, ts2)) =>
111 :     let val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts1
112 :     val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts2
113 :     in tkc_mono
114 :     end
115 :     | _ => bug "unexpected TC_ENV or TC_CONT in tk_tyc")
116 :     in g t
117 :     end
118 :    
119 :     and tk_chk kenv (k, tc) =
120 :     if tk_eqv(k, tk_tyc(tc, kenv)) then () else raise TkTycChk
121 :    
122 :     fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =
123 :     let val nt = lt_whnm lt
124 :     in (case ((* lt_outX *) lt_out nt, ts)
125 :     of (LK.LT_POLY(ks, b), ts) =>
126 :     let val _ = ListPair.app (tk_chk kenv) (ks, ts)
127 :     fun h x = ltc_env(x, 1, 0, tcInsert(initTycEnv, (SOME ts, 0)))
128 :     in map h b
129 :     end
130 :     | (_, []) => [nt] (* ? problematic *)
131 :     | _ => raise LtyAppChk)
132 :     end
133 :    
134 :     (** a special lty application --- used inside the translate/specialize.sml *)
135 :     fun lt_sp_adj(ks, lt, ts, dist, bnl) =
136 :     let fun h(abslevel, ol, nl, tenv) =
137 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
138 :     else if abslevel > 0 then
139 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
140 :     else bug "unexpected cases in ltAdjSt"
141 :    
142 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
143 :     val nt = h(dist, 1, bnl, btenv)
144 : monnier 24 in lt_norm nt
145 : monnier 16 end
146 :    
147 :     (** a special tyc application --- used inside the translate/specialize.sml *)
148 :     fun tc_sp_adj(ks, tc, ts, dist, bnl) =
149 :     let fun h(abslevel, ol, nl, tenv) =
150 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
151 :     else if abslevel > 0 then
152 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
153 :     else bug "unexpected cases in tcAdjSt"
154 :    
155 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
156 :     val nt = h(dist, 1, bnl, btenv)
157 : monnier 24 in tc_norm nt
158 : monnier 16 end
159 :    
160 :     (** sinking the lty one-level down --- used inside the specialize.sml *)
161 :     fun lt_sp_sink (ks, lt, d, nd) =
162 :     let fun h(abslevel, ol, nl, tenv) =
163 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
164 :     else if abslevel > 0 then
165 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
166 :     else bug "unexpected cases in ltSinkSt"
167 :     val nt = h(nd-d, 0, 1, initTycEnv)
168 : monnier 24 in lt_norm nt
169 : monnier 16 end
170 :    
171 :     (** sinking the tyc one-level down --- used inside the specialize.sml *)
172 :     fun tc_sp_sink (ks, tc, d, nd) =
173 :     let fun h(abslevel, ol, nl, tenv) =
174 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
175 :     else if abslevel > 0 then
176 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
177 :     else bug "unexpected cases in ltSinkSt"
178 :     val nt = h(nd-d, 0, 1, initTycEnv)
179 : monnier 24 in tc_norm nt
180 : monnier 16 end
181 :    
182 :     (** utility functions used in CPS *)
183 :     fun lt_iscont lt =
184 :     (case lt_out lt
185 :     of LK.LT_CONT _ => true
186 :     | LK.LT_TYC tc =>
187 :     (case tc_out tc of LK.TC_CONT _ => true | _ => false)
188 :     | _ => false)
189 :    
190 :     fun ltw_iscont (lt, f, g, h) =
191 :     (case lt_out lt
192 :     of LK.LT_CONT t => f t
193 :     | LK.LT_TYC tc =>
194 :     (case tc_out tc of LK.TC_CONT x => g x | _ => h lt)
195 :     | _ => h lt)
196 :    
197 :    
198 :     fun tc_bug tc s = bug (s ^ "\n\n" ^ (tc_print tc) ^ "\n\n")
199 :     fun lt_bug lt s = bug (s ^ "\n\n" ^ (lt_print lt) ^ "\n\n")
200 :    
201 :     (** other misc utility functions *)
202 :     fun tc_select(tc, i) =
203 :     (case tc_out tc
204 : monnier 24 of LK.TC_TUPLE zs =>
205 : monnier 16 ((List.nth(zs, i)) handle _ => bug "wrong TC_TUPLE in tc_select")
206 :     | _ => tc_bug tc "wrong TCs in tc_select")
207 :    
208 :     fun lt_select(t, i) =
209 :     (case lt_out t
210 :     of LK.LT_STR ts =>
211 :     ((List.nth(ts, i)) handle _ => bug "incorrect LT_STR in lt_select")
212 :     | LK.LT_PST ts =>
213 :     let fun h [] = bug "incorrect LT_PST in lt_select"
214 :     | h ((j,a)::r) = if i=j then a else h r
215 :     in h ts
216 :     end
217 :     | LK.LT_TYC tc => ltc_tyc(tc_select(tc, i))
218 :     | _ => bug "incorrect lambda types in lt_select")
219 :    
220 :     fun tc_swap t =
221 :     (case (tc_out t)
222 :     of LK.TC_ARROW ((r1,r2), [s1], [s2]) => tcc_arrow((r2,r1), [s2], [s1])
223 :     | _ => bug "unexpected tycs in tc_swap")
224 :    
225 :     fun lt_swap t =
226 :     (case (lt_out t)
227 :     of (LK.LT_POLY (ks, [x])) => ltc_poly(ks, [lt_swap x])
228 :     | (LK.LT_TYC x) => ltc_tyc(tc_swap x)
229 :     | _ => bug "unexpected type in lt_swap")
230 :    
231 :     (** a version of ltc_arrow with singleton argument and return result *)
232 :     val ltc_arw = ltc_parrow
233 :    
234 :     (** not knowing what FUNCTION this is, to build a fct or an arw *)
235 :     fun ltc_fun (x, y) =
236 :     (case (lt_out x, lt_out y)
237 :     of (LK.LT_TYC _, LK.LT_TYC _) => ltc_parrow(x, y)
238 :     | _ => ltc_pfct(x, y))
239 :    
240 :     (* lt_arrow used by chkflint.sml, checklty.sml, chkplexp.sml, convert.sml
241 :     * and wrapping.sml only
242 :     *)
243 :     fun lt_arrow t =
244 :     (case (lt_out t)
245 :     of (LK.LT_FCT([t1], [t2])) => (t1, t2)
246 :     | (LK.LT_FCT(_, _)) => bug "unexpected case in lt_arrow"
247 :     | (LK.LT_CONT [t]) => (t, ltc_void)
248 :     | _ => (ltd_parrow t) handle _ =>
249 :     bug ("unexpected lt_arrow --- more info: \n\n"
250 :     ^ (lt_print t) ^ "\n\n"))
251 :    
252 :     (* lt_arrowN used by flintnm.sml and ltysingle.sml only, should go away soon *)
253 :     fun lt_arrowN t =
254 :     (case (lt_out t)
255 :     of (LK.LT_FCT(ts1, ts2)) => (ts1, ts2)
256 :     | (LK.LT_CONT ts) => (ts, [])
257 :     | _ => (let val (_, s1, s2) = ltd_arrow t
258 :     in (s1, s2)
259 :     end))
260 :    
261 :     end (* top-level local *)
262 :     end (* structure LtyExtern *)
263 :    

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