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 95 - (view) (download)
Original Path: sml/trunk/src/compiler/FLINT/kernel/ltybasic.sml

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 :     | g (LK.TC_NVAR(v,d,i)) = "NTV(v" ^ (itos v) ^ "," ^ (itos d)
157 :     ^ "," ^ (itos i) ^ ")"
158 :     | g (LK.TC_PRIM pt) = PT.pt_print pt
159 :     | g (LK.TC_FN(ks, t)) =
160 : monnier 45 "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
161 : monnier 16 | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"
162 :     | g (LK.TC_APP(t, zs)) =
163 :     (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
164 :     | g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"
165 :     | g (LK.TC_PROJ (t, i)) =
166 :     "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
167 :     | g (LK.TC_SUM tcs) =
168 :     "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
169 :     | g (LK.TC_FIX ((_, tc, ts), i)) =
170 :     if tc_eqv(x,tcc_bool) then "B"
171 :     else if tc_eqv(x,tcc_list) then "LST"
172 : monnier 71 else (let (* val ntc = case ts of [] => tc
173 :     | _ => tcc_app(tc, ts) *)
174 :     val _ = 1
175 :     in ("DT{" ^ "DATA" (* ^ "[" ^ (tc_print tc)
176 :     ^ "] &&" ^ (plist(tc_print, ts))
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 71
262 : monnier 16 (***************************************************************************
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 :    
296 : monnier 95
297 :     (*
298 :     * $Log: ltybasic.sml,v $
299 :     * Revision 1.1.1.1 1998/04/08 18:39:40 george
300 :     * Version 110.5
301 :     *
302 :     *)

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