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/primop-branch-3/compiler/FLINT/kernel/ltybasic.sml
ViewVC logotype

Annotation of /sml/branches/primop-branch-3/compiler/FLINT/kernel/ltybasic.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2221 - (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
140 :     (***************************************************************************
141 :     * UTILITY FUNCTIONS FOR PRETTY PRINTING *
142 :     ***************************************************************************)
143 :    
144 :     (** pretty printing of tkinds, tycs, and ltys *)
145 :     fun tk_print (x : tkind) =
146 :     let fun g (LK.TK_MONO) = "K0"
147 :     | g (LK.TK_BOX) = "KB0"
148 : monnier 45 | g (LK.TK_FUN (ks, k)) =
149 :     "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
150 : monnier 16 | g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"
151 :     in g (tk_out x)
152 :     end
153 :    
154 :     fun tc_print (x : tyc) =
155 :     let fun g (LK.TC_VAR(i,j)) = "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
156 : monnier 197 | g (LK.TC_NVAR v) = "NTV(v" ^ (itos v) ^ ")"
157 : monnier 16 | g (LK.TC_PRIM pt) = PT.pt_print pt
158 :     | g (LK.TC_FN(ks, t)) =
159 : monnier 45 "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
160 : monnier 16 | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"
161 :     | g (LK.TC_APP(t, zs)) =
162 :     (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
163 :     | g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"
164 :     | g (LK.TC_PROJ (t, i)) =
165 :     "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
166 :     | g (LK.TC_SUM tcs) =
167 :     "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
168 :     | g (LK.TC_FIX ((_, tc, ts), i)) =
169 :     if tc_eqv(x,tcc_bool) then "B"
170 :     else if tc_eqv(x,tcc_list) then "LST"
171 : monnier 71 else (let (* val ntc = case ts of [] => tc
172 :     | _ => tcc_app(tc, ts) *)
173 :     val _ = 1
174 :     in ("DT{" ^ "DATA" (* ^ "[" ^ (tc_print tc)
175 :     ^ "] &&" ^ (plist(tc_print, ts))
176 :     ^ "&&" *) ^ "===" ^ (itos i) ^ "}")
177 : monnier 16 end)
178 :     | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"
179 :     | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"
180 : monnier 45 | g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"
181 :     | g (LK.TC_ARROW (ff,z1,z2)) =
182 :     parw(fn u => plist(tc_print,u),(ff,z1,z2))
183 : monnier 16 | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"
184 : monnier 45 | g (LK.TC_TOKEN (k, t)) =
185 :     if LK.token_isvalid k then
186 :     (LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
187 :     else bug "unexpected TC_TOKEN tyc in tc_print"
188 : monnier 16 | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
189 :     | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"
190 :     | g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"
191 :     in g (tc_out x)
192 :     end (* function tc_print *)
193 :    
194 :     fun lt_print (x : lty) =
195 :     let fun h (i, t) = "(" ^ (itos i) ^ "," ^ (lt_print t) ^ ")"
196 :    
197 :     fun g (LK.LT_TYC t) = tc_print t
198 :     | g (LK.LT_STR zs) = "S{" ^ (plist(lt_print, zs)) ^ "}"
199 :     | g (LK.LT_FCT (ts1,ts2)) =
200 :     "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
201 :     ^ (plist(lt_print, ts2)) ^ ")"
202 :     | g (LK.LT_POLY(ks, ts)) =
203 : monnier 45 "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
204 : monnier 16 | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"
205 :     | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"
206 :     | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"
207 :    
208 :     in g (lt_out x)
209 :     end (* function lt_print *)
210 :    
211 :     (** finding out the depth for a tyc's innermost-bound free variables *)
212 :     val tc_depth : tyc * depth -> depth = LK.tc_depth
213 :     val tcs_depth: tyc list * depth -> depth = LK.tcs_depth
214 :    
215 :     (** adjusting an lty or tyc from one depth to another *)
216 :     fun lt_adj (lt, d, nd) =
217 : monnier 45 if d = nd then lt
218 :     else ltc_env(lt, 0, nd - d, LK.initTycEnv)
219 : monnier 16
220 :     fun tc_adj (tc, d, nd) =
221 : monnier 45 if d = nd then tc
222 :     else tcc_env(tc, 0, nd - d, LK.initTycEnv)
223 : monnier 16
224 : monnier 45 (** the following functions does the smiliar thing as lt_adj and
225 :     tc_adj; it adjusts an lty (or tyc) from depth d+k to depth nd+k,
226 :     assuming the last k levels are type abstractions. So lt_adj
227 :     is really lt_adj_k with k set to 0. Both functions are currently
228 :     called inside the lcontract.sml only. *)
229 :     local
230 :     fun mkTycEnv (i, k, dd, e) =
231 :     if i >= k then e else mkTycEnv(i+1, k, dd, LK.tcInsert(e,(NONE, dd+i)))
232 :    
233 :     in
234 :     fun lt_adj_k (lt, d, nd, k) =
235 :     if d = nd then lt
236 :     else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
237 :    
238 :     fun tc_adj_k (tc, d, nd, k) =
239 : monnier 16 if d = nd then tc
240 : monnier 45 else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
241 : monnier 16
242 : monnier 45 end (* lt_adj_k and tc_adj_k *)
243 :    
244 : monnier 16 (** automatically flattening the argument or the result type *)
245 :     val lt_autoflat : lty -> bool * lty list * bool = LK.lt_autoflat
246 :    
247 : monnier 45 (** testing if a tyc is a unknown constructor *)
248 :     val tc_unknown : tyc -> bool = LK.tc_unknown
249 :    
250 : monnier 16 (***************************************************************************
251 :     * UTILITY FUNCTIONS ON TKIND ENVIRONMENT *
252 :     ***************************************************************************)
253 :    
254 : league 65 type tkindEnv = LK.tkindEnv
255 :     exception tkUnbound = LK.tkUnbound
256 :     val initTkEnv = LK.initTkEnv
257 :     val tkLookup = LK.tkLookup
258 :     val tkInsert = LK.tkInsert
259 : monnier 71
260 : monnier 16 (***************************************************************************
261 :     * UTILITY FUNCTIONS ON TYC ENVIRONMENT *
262 :     ***************************************************************************)
263 :    
264 :     exception tcUnbound = LK.tcUnbound
265 :     type tycEnv = LK.tycEnv
266 :     val initTycEnv = LK.initTycEnv
267 :     val tcInsert = LK.tcInsert
268 :    
269 :     (***************************************************************************
270 :     * UTILITY FUNCTIONS ON LTY ENVIRONMENT *
271 :     ***************************************************************************)
272 :    
273 :     (** utility values and functions on ltyEnv *)
274 : monnier 504 type ltyEnv = (lty * DebIndex.depth) IntRedBlackMap.map
275 : monnier 16
276 :     exception ltUnbound
277 : monnier 504 val initLtyEnv : ltyEnv = IntRedBlackMap.empty
278 : monnier 16
279 :     fun ltLookup (venv, lv, nd) =
280 : monnier 504 (case IntRedBlackMap.find(venv, lv)
281 : monnier 422 of NONE =>
282 :     (say "**** hmmm, I didn't find the variable ";
283 :     say (Int.toString lv); say "\n";
284 :     raise ltUnbound)
285 :     | SOME (lt, d) =>
286 :     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 :     (*easc*))
290 : monnier 16
291 : monnier 504 fun ltInsert (venv, lv, lt, d) = IntRedBlackMap.insert(venv, lv, (lt, d))
292 : monnier 16
293 :     end (* top-level local *)
294 :     end (* structure LtyBasic *)

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