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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

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