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/DEVNOTES/Primops/primop2-note-1
ViewVC logotype

Annotation of /sml/trunk/compiler/DEVNOTES/Primops/primop2-note-1

Parent Directory Parent Directory | Revision Log Revision Log


Revision 5026 - (view) (download)

1 : dbm 2265 Primop2 Notes
2 :    
3 :     Primop2 Branch Info
4 :     ===================
5 :    
6 :     The development branch name is:
7 :    
8 :     primop-branch-2
9 :    
10 :     The tag for the root of primop-branch-2 is:
11 :    
12 :     dbm-20060615-base-primop-branch-2
13 :    
14 :    
15 :     ======================================================================
16 :     The Program
17 :    
18 :     Our goal is to clean-up and simplify the code of the SML/NJ Front End
19 :     (everything before the translate phase), and as far as possible turn it
20 :     into a self-contained SML front end "library" that could be used outside
21 :     the SML/NJ compiler. There are several related subgoals:
22 :    
23 :     1. A major part of this effort aims to remove dependencies on FLINT
24 :     constructs and interfaces from the front end. This requires that we
25 :     understand what the FLINT-related values and computations are used for
26 :     so that we can reproduce that functionality in the translate phase,
27 :     ultimately producing the same FLINT intermediate language.
28 :    
29 :     2. We want to avoid transformations of the abstract syntax before type
30 :     checking, since these transformations reduce the faithfulness of the
31 :     abstract syntax to the original source and lead to less useful and less
32 :     accurate type error messages. Abstract syntax transformations/normalizations
33 :     that have presumably been introduced to be helpful for FLINT should be
34 :     be moved into the translate phase. All we need to do is make sure
35 :     that the abstract syntax captures and retains all static information that
36 :     the translate phase will need to produce the correct plambda code.
37 :    
38 :     3. We want to simplify the FLINT code (and ultimately the object code)
39 :     by eliminating the real array => realarray representation
40 :     optimization. We need to understand what parts of the translation is
41 :     specifically supporting this optimization, so that those parts can be
42 :     simplified.
43 :    
44 :    
45 :     ======================================================================
46 :     Questions:
47 :    
48 :     1. Where have wordTycon and wordTy gone?
49 :     In primop, they were defined in ElabData/types/core-basictypes.sml.
50 :     Now they are in Elaborator/types/basictypes.s??
51 :    
52 :     1.1. What is the reason for the split of basic type building between
53 :     core-basictypes (in ElabData/types) and basictypes (in
54 :     Elaborator/types)?
55 :    
56 :     2. What is the purpose of the ty lists in VARexp and CONexp
57 :     constructors of exp in ElabData/syntax/absyn.s??
58 :     Should be able to replace list of metavariables by (instantiated)
59 :     variable type. Or, since in most cases this is not relevant (it's
60 :     represented by [] currently), it should be a type option. This type
61 :     would the the instantiated "variable type", i.e. based on a generic
62 :     instantiation of the typ field of the VALvar, etc. [We could just use
63 : jhr 5026 UNDEFty as the default, unneeded value instead of NONE, but using
64 : dbm 2265 ty option is cleaner and more explicit about what is going on.]
65 :    
66 :     Files affected:
67 :     ElabData/syntax/absyn.s?? [done - except for option]
68 :     Elaborator/types/typecheck.sml [done - except for option]
69 :     Elaborator/modules/sigmatch.sml [?]
70 :     FLINT/trans/translate.sml [?]
71 :    
72 :     3. Question in comment on generalizePat in Elaborator/types/typecheck.sml.
73 :    
74 :     4. Why do CONpats (see CONpat case of patType in typecheck.sml) need
75 :     the "insts" value? Similarly for CONexps. What do they have to do with
76 :     primops? Where is this information used? Is this related to the
77 :     special role of ref?
78 :    
79 :     5. Catalogue of primops:
80 :     We need a complete catalog of all primops, with their initial types (primop
81 :     generic type), and the modules and types where they are ultimately defined
82 :     in the Basis modules.
83 :    
84 :     6. Numbered primops:
85 :     Perhaps in the front end, primops can be respresented by a simple number
86 :     (defined in the basic primop module). The mapping between primop numbers
87 :     and their generic types could be implemented as a table or finite map.
88 :     Generic primops that are used at different types could be split into a set
89 : jhr 5026 of primop numbers, one for each final (variable) type. FLINT would be
90 : dbm 2265 responsible for recognizing that several primop numbers represent the same
91 :     generic underlying primop. Then the primop numbers could be mapped to their
92 : jhr 5026 exact (variable) type in the Inline module. One problem here is that some
93 : dbm 2265 type constructors appearing in variable types are not defined (yet) in
94 :     the PrimTypes module -- presumably we could fix this by adding them as
95 :     additional primite types. Examples are probably array and vector tycons.
96 :     notes
97 :    
98 :     7. InlInfo datatype ii/selectors and utility functions
99 :     Why is the module ElabData/Basics/II (which defines the datatype ii
100 :     and selectors) separate from module Semant/Basics/InlInfo (which
101 : jhr 5026 defines utility functions and on the datatype ii)?
102 : dbm 2265
103 : jhr 5026 Functions in InlInfo appear to be used only in the TopLevel profiling
104 : dbm 2265 hooks. The remaining use is in the ElabData/types/TypesUtil.isValue
105 :     function. Unfortunately, there is some funny business going on in that
106 :     the functions in InlInfo require the PrimOp module which is not
107 :     available in ElabData/types/TypesUtil.
108 :    
109 :     We've merged these into a single module InlInfo. This depends on PrimOp.
110 :     This caused the sigmatch functor to be moved to Semant/modules.
111 :    
112 :    
113 :     8. Dynamic access and inline info. Are these mutually exclusive (i.e.
114 :     something has a dynamic value accessed via the access info, or it is
115 :     a primop accessed via the inline info), or to they both work in parallel
116 :     (i.e. a primop also has a function closure representation stored in
117 :     a slot in the dynamic vector for its home structure)?
118 :    
119 :     9. Structure/substructure primop IDs and signature slot information
120 :     are split among the structure and signature representations
121 :     respectively. Are substructure primop IDs (and other substructure
122 :     components such as realization, access, signature) available directly
123 :     in the static environment?
124 :    
125 :     No. Although the root structure strrec's are entered into the static
126 :     environment, all substructure information can only be found within the
127 : jhr 5026 strrec of the root structure.
128 : dbm 2265
129 : jhr 5026
130 : dbm 2265 ======================================================================
131 :     Old Primop Notes (from old primop branch, mostly obsolete)
132 :    
133 :     These notes are my attempt to figure out what appears to be a very kludgy
134 :     treatement of how primops interact with the type checker. I want to define
135 :     what the basic problem is, understand what the current code is doing to deal
136 :     with the problem, and then either eliminate the problem or find a more elegant
137 :     solution.
138 :    
139 :     1. PrimOp dependency in type checker
140 :    
141 :     The isValue function in TypesUtil needs to check for the CAST primop, which
142 :     it does using InlInfo.pureInfo (badly named function). Thus
143 :    
144 :     TypeCheck --> TypesUtil --> InlInfo --> PrimOp
145 :    
146 :     Before, this was factored out by making TypeCheck into a functor TypeCheckFn
147 :     which was then applied (in Semant/types/typecheck.sml) to InlInfo.pureInfo.
148 :    
149 :     The other dependency on ii2ty is eliminated by having VARexp carry the
150 :     whole instantiated type rather than the list of generic meta-type-variables
151 :     (with their instantiations).
152 :    
153 :    
154 :     2. Role of boundtvs
155 :    
156 :     "boundtvs" is a field of the VB (variable binding) record, containing
157 :     a list of tyvars.
158 :    
159 :     Where is boundtvs set?
160 :    
161 :     Most VB constructions throughout the front end (e.g. all in ElabCore)
162 :     set boundtvs to [] or pass a value of boundtvs through
163 :     (Elaborator/elaborate/elabutil.sml). There are 3 places where it is
164 :     potentially set to a non-nil list:
165 :    
166 :     (1) TypeCheck/decType0 (Elaborator/types/typecheck.sml).
167 :     In the VALdec case, variable bindings are constructed where boundtvs
168 :     is the set of meta tyvars that are generalized by generalizePat
169 :     applied to the pattern.
170 :    
171 :     [From the way generalizePat is written, there can be only one variable
172 :     in the pattern whose type is polymorphic (i.e. has tyvars generalized).]
173 :    
174 :    
175 :     (2) SigMatch/matchElems (Elaborator/modules/sigmatch.sml).
176 :     In the cases for VALspec/VALspec, and VALspec/CONspec. Here the value for
177 :     boundtvs (btvs) is computed by SigMatch/matchTypes, which in turn calls
178 :     SigMatch/eqvTnspTy after checking that the spec type and actual type are
179 :     compatible.
180 :    
181 :     eqvTnspTy (mnemonic for what?) creates a generic instantiation of the
182 :     actual type (actInst, with generic meta-tyvars actInstTvs), a separate
183 :     generic instantiation (specInst, specInstTvs) of the specty type,
184 :     which may be less polymorphic than actualty, and then unifies actInst
185 :     and specInst. This unification may cause tyvars in actInstTvs to be
186 :     instantiated. Then specInstTvs is transformed by TU.tyvarType to
187 :     produce the second result, boundTvs.
188 :    
189 :     TU.tyvarType turns type expressions that represent meta type variables
190 :     into the tyvars that they contain, stripping off VARtys and following
191 :     instantiations. Note that instantiatePoly returns a list of type
192 :     _expressions_ (VARty's) as its second result.
193 :    
194 : jhr 5026 fun eqvTnspTy (specty: ty, actualty: ty) : (ty * tyvar list) =
195 : dbm 2265 let val actualty = TU.prune actualty
196 :     val (actInst, actInstTvs) = TU.instantiatePoly actualty
197 :     val (specInst, specInstTvs) = TU.instantiatePoly specty
198 :     val _ = ((Unify.unifyTy(actInst, specInst))
199 :     handle _ => bug "unexpected types in eqvTnspTy")
200 :     val boundTvs = map TU.tyvarType specInstTvs
201 :     in (actInst, boundTvs)
202 :     end
203 :    
204 :     The unification will cause some tyvars in actInstTvs to be
205 :     instantiated to non-type-variable type terms (subterms of specInst),
206 :     where specty is more specific than actualty). Where corresponding
207 :     subterms are both type variables, the specty tyvar (a member of
208 :     specInstTvs) will be instantiated to the corresponding actualty type
209 :     variable (a member of actInstTvs) because of the right-to-left
210 :     instantiation bias in Unify/unifyTyvars [Elaborator/types/unify.sml].
211 :    
212 :     So the resultant type term actInst may contain (uninstantiated) tyvars
213 :     in specInstTvs as well as some (uninstantiated) tyvars in actInstTvs.
214 :     For the latter tyvars, the matching tyvar in specInstTvs will have
215 :     been instantiated to it. So the specInstTvs will contain all the
216 :     tyvars occuring in actInst, some of which will be uninstantiated,
217 :     while others will be instantiated to tyvars in actInstTvs. Applying
218 :     TU.tyvarType will strip off the instantiations, so that the resulting
219 :     boundtvs will contain a mixture of the tyvars from actInstTvs and
220 :     specInstTvs.
221 :    
222 :     Example:
223 :    
224 :     actualty = 'a * 'b -> 'b -> 'a
225 :     specty = 'c list * 'c -> 'c -> 'c list
226 :     actInst = 'X * 'Y -> 'Y -> 'X
227 :     actInstTvs = ['X, 'Y]
228 :     specInst = 'Z list * 'Z -> 'Z -> 'Z list
229 :     specInstTvs = ['Z]
230 :     -------------------
231 :     after unification:
232 :     -------------------
233 :     actInst = {{'Y/'Z} list/'X} * 'Y -> {{'Y/'Z} list/'X}
234 :     boundtvs = [tyvar('Y)]
235 :    
236 :     where {ty/'X} represents the meta type variable 'X instantiated
237 :     to type ty.
238 :    
239 :     If unifyTyvars had a left-to-right instantiation bias instead of a
240 :     right-to-left bias, the unification would instantiate all the tyvars
241 :     in actInstTvs and none of the tyvars in specInstTvs, so the resultant
242 :     type actInst will be equivalent to specInst -- note that in this
243 :     special case unification will not have to adjust any type variable
244 :     attributes, since all depths will be infinity and the consistency of
245 :     equality properties will already have been guaranteed by the previous
246 :     call of TU.compareTypes in matchTypes.
247 :    
248 :     In this case, eqvTnspTy could just return specInst and specInstTvs
249 :     without bothering to perform the useless unification. It is not clear
250 :     why this would not suffice anyway, i.e. eqvTnspTy could simply be
251 :     replaced by TU.instantiatePoly applied to specty, with tyvarType then
252 :     mapped over the resulting specInstTvs. The simplified version of
253 :     eqvTnspTy would be
254 :    
255 : jhr 5026 fun eqvTnspTy (specty: ty) : (ty * tyvar list) =
256 : dbm 2265 let val (specInst, specInstTvs) = TU.instantiatePoly specty
257 :     in (specInst, map TU.tyvarType specInstTvs)
258 :     end
259 :    
260 :     and the actualty argument would not be needed.
261 :    
262 :     Maybe the interaction is more complicated if, for instance, specty
263 :     contains type abbreviations that are not used in the corresponding
264 :     places in actualty? Unification would then cause these type
265 :     abbreviations to be expanded. But how could this matter?
266 :    
267 :    
268 :     (3) SigMatch/packElems in the VALspec case.
269 :     Here the value btvs for boundtvs is calculated by SigMatch/absEqvTy.
270 :     absEqvTy is similar to eqvTnspTy, in that it generically instantiations
271 :     the actual and spec types and then unifies them.
272 :    
273 :     fun absEqvTy (specty: ty, actualty: ty) : (ty * tyvar list * ty * bool) =
274 :     let val actualty = TU.prune actualty
275 :     val specty = TU.prune specty
276 :     val (actInst, actInstTvs) = TU.instantiatePoly actualty
277 :     val (specInst, specInstTvs) = TU.instantiatePoly specty
278 :     val _ = ListPair.app Unify.unifyTy (actInstTvs, specInstTvs)
279 :    
280 :     val res = (Unify.unifyTy(actInst, specInst); true) handle _ => false
281 :     (* ???? what is this doing? *)
282 :    
283 :     val boundTvs = map TU.tyvarType actInstTvs
284 :     (* should I use specInstTvs here instead, why actInstTvs ? *)
285 :    
286 :     in (actInst, boundtvs, specInst, res)
287 :     end
288 :    
289 :     This function is defined in a very obscure way, and returns both the
290 :     instantiated actualTy (actInst) and instantiated specTy (specInst),
291 :     after attempting to unify them. But first, _some_ of the type
292 :     variables of actInstTvs and specInstTvs are identified by the
293 :     ListPair.app unifyTy line (note that these two lists may have
294 :     different lengths, and it is not clear why identifying initial
295 :     segments of these two lists of type variables makes sense.
296 :    
297 :     If the unification is successful, then actInst and specInst are
298 :     essentially the same type. If the unification fails, then we have two
299 :     inequivalent, but partially unified type expressions. What is going
300 :     on here?
301 :    
302 :    
303 :     3. VARexp type checking hack for primops.
304 :    
305 :     Here is the code for the VARexp case in expType (Elaborator/types/typecheck.sml):
306 :    
307 :     case exp
308 :     of VARexp(r as ref(VALvar{typ, info, ...}), _) =>
309 :     (case ii2ty info of
310 :     SOME st =>
311 :     let val (sty, insts) = instantiatePoly(st)
312 :     val (nty, _) = instantiatePoly(!typ)
313 :     in
314 :     unifyTy(sty, nty) handle _ => (); (* ??? *)
315 :     (VARexp(r, insts), sty)
316 :     end
317 :     | NONE =>
318 :     let val (ty, insts) = instantiatePoly(!typ)
319 :     in (VARexp(r, insts), ty)
320 :     end)
321 :    
322 :     This uses ii2ty (passed as a parameter to the TypeCheckingFn, but uniquely
323 : jhr 5026 defined to be InstantiateParam.ii2ty in Semant/types/typecheck.sml) to extract
324 : dbm 2265 a type from the info field, if possible (i.e. when the VALvar is associated
325 :     with a primop).
326 :    
327 :     The reason for this use of unification seems to be that there are some primops
328 :     (e.g. length) that are used for several different operations (therefore
329 :     different VALvars), and the VALvar types are speciallized instances of a
330 :     more polymorphic type associtated with the primop (in the info field).
331 :    
332 :    
333 :     What is the ultimate consumer of the boundtv field?
334 :    
335 :    
336 :     Relevant Files and Modules
337 :     --------------------------
338 :     Primitive Types
339 :    
340 :     CorePrimTycNum (ElabData/basics/core-ptnum.sml)
341 :     core prim-type numbers (essentially the same as Elaborator/basics/ptnum.sml
342 : jhr 5026 except only language-standard types are included)
343 : dbm 2265 see: Elaborator/basics/ptnum.sml
344 :     defs: CORE_PRIM_TYC_NUM, CorePrimTycNum
345 :    
346 :     PrimTycNum (Elaborator/basics/ptnum.sml)
347 :     prim type numbers, augmenting ElabData/basics/core-ptnum.sml with
348 :     implementation dependent types
349 :     see: ElabData/basics/core-ptnum.sml
350 :     defs: PRIM_TYC_NUM, PrimTycNum: PRIM_TYC_NUM
351 :    
352 :     CoreBasicTypes (ElabData/types/core-basictypes.sml)
353 :     building the primitive types and associated values (containing only
354 :     implementation independent, language-standard basic types?)
355 :     see: Elaborator/types/basictypes.sml
356 :     defs: CoreBasicTypes
357 :    
358 :     BasicTypes (Elaborator/types/basictypes.sig,sml)
359 :     define basic (built-in) types; most are just defined in terms of
360 :     types from CoreBasicTypes [MOVE to ElabData?]
361 :     see: ElabData/types/core-basictypes.sml
362 :     defs: BasicTypes
363 :    
364 :     PrimEnv: PRIM_ENV (Semant/statenv/prim.sml)
365 : jhr 5026 define static env primEnv, containing module bindings for
366 :     primitive types (PrimTypes), primops (Inline), and unrolled
367 : dbm 2265 lists (UnrolledList)
368 : jhr 5026 defs: PRIM_ENV, PrimEnv: PRIM_ENV
369 : dbm 2265
370 :    
371 :     Primops
372 :    
373 :     PrimOp (FLINT/kernel/primop.sml)
374 :     the types (primop, etc.) used to represent primops and their
375 :     attributes. There are no type specs in these primop representations.
376 :     PrimOp imports CTypes, which are defined in MLRISC! (MLRISC/c-calls/ctype.sml)
377 :    
378 :     PrimEnv (Semant/statenv/prim.sml)
379 : jhr 5026 builds Inline structure, containing bindings to primops
380 : dbm 2265 this is where all primops are actually created and initially bound
381 :     to identifiers. They will be rebound later in InLineT (below), and
382 : jhr 5026 then again in the Basis module definitions. What role does the
383 : dbm 2265 intermediate InLineT play?
384 :    
385 :     Matthias revised this to assign accurate (final?) types to the
386 :     primop variables. Do these change in InLineT or in the Basis modules?
387 :    
388 :     InLineT (../system/smlnj/init/built-in.sml)
389 :    
390 :    
391 :     Inline Info
392 :    
393 :     II (ElabData/basics/ii.sml)
394 :     FLINT related information for inlining (why is this in elaborator?)
395 : jhr 5026 datatype ii used for "inline info". Actual atomic inline info
396 : dbm 2265 represented here by type exn (a hack to delay referencing the actual
397 :     inline info representation defined in
398 :     defs: II
399 :    
400 :     InlInfo (Semant/basics/inlinfo.sig,sml)
401 :     inlinfo.sig/sml
402 :     functions for creating and examining inlining info, using an exception
403 :     E to package primop-type pairs into the II.ii datatype.
404 :     defs: INL_INFO, InlInfo: INL_INFO
405 :    
406 : jhr 5026 [II has been folded into InlInfo, and the code of InlInfo has been
407 : dbm 2265 simplified, eliminating the exn hack. Interface function names have
408 :     bin changed (e.g. pureInfo => isPrimCast). ii2ty has been added with
409 :     new name primopTy (moved from InstantiateParam).]
410 :    
411 :    
412 :     Semant
413 :    
414 :     ElabData and Elaborate CM groups cannot refernce FLINT and MLRISC stuff,
415 :     which are part of the Core group. Therefore places where the front end
416 :     depend on FLINT (e.g. PrimOp, PLambdaType (in InstantiateParam)) have to
417 :     be in Semant, which is part of Core group.
418 :    
419 :     This means that many of the elaboration modules are functorized, ultimately
420 :     on PrimOp related values (former TypeCheckFn) or on PLambdaType stuff
421 :     (InstantiateFn in Elaborate requires parameter InstantiateParam from Semant).
422 :    
423 :    
424 :     ======================================================================
425 :    
426 :     Example for VARexp typing:
427 :    
428 :     val x = Array.length
429 :    
430 :     let
431 :    
432 :     v = the VALvar for Array.length.
433 :     st = ii2ty v.info = 'a -> int (the generic primop type)
434 :     sty = X -> int (generic instantiation of st, X a fresh type metavariable)
435 :     insts = [X]
436 :    
437 :     v.typ = 'a array -> int
438 :     nty = Y array -> int (generic inst. of v.typ, Y a fresh type metavar)
439 :    
440 :     unify (sty, nty) ==> X |-> Y array
441 : jhr 5026
442 : dbm 2265 After type generalization of the val binding:
443 :     boundtvs = [Y] (in VB)
444 :     insts = [X] (in VARexp)
445 :    
446 :     These last don't agree (different metavariables), so in mkVBS in
447 :     Translate (FLINT/trans/translate.sml), the first VB case will take the
448 :     else branch and apply mkPE.
449 :    
450 :     It appears that the boundtvs is used in mkPE (Translate) to provide type
451 :     parameters to primop invocations. [Why boundtvs and not insts?]
452 :    
453 :    
454 :     ======================================================================
455 :    
456 :     [FLINT] Questions:
457 :    
458 :     The primop-branch-2 code contains a number of questions in comments
459 :     marked by the string "[KM ???]". You can find them by grepping the
460 :     source for that string.
461 :    
462 :     The following questions are in more or less random order, added as
463 :     they came up in our reading of the code. Most but not all relate to
464 :     the interaction of FLINT and the front end, or to FLINT internals.
465 :    
466 :    
467 :     1. What is the relevance of the comment in system/smlnj/init/dummy.sml
468 :     to the code in that file?
469 :    
470 :    
471 :     2. What is the meaning of the comment after the PrimTypes
472 :     (re)declaration at the top of system/smlnj/init/built-in.sml?
473 :    
474 :    
475 :     3. The Single Generalization Conjecture (SGC): Each type metavariable
476 :     that is not instantiated is generalized at a single variable binding.
477 :     Consequence: the metavariable can be updated with a deBruijn index for
478 :     the corresponding generalized polymorphic variable. [The code for
479 :     mkPE in translate.sml seems to imply this is not the case.]
480 :    
481 :     If the SGC is true, then the "restore" function in Translate.mkPE is
482 :     unnecessary, as the metavariables in question will only be used once.
483 :    
484 :     The SGC has been tested experimentally by removing the call of restore
485 : jhr 5026 in mkPE, and bootstrapping the compiler. The runtime check in mkPE
486 : dbm 2265 that tests for previously used generalized metavariables was not
487 :     triggered.
488 :    
489 :    
490 :     4. More on Single Generalization Conjecture
491 :    
492 :     Here is an expression containing two mutually recursive functions that
493 :     have the same return type, which will be polymorphic. It seems likely
494 :     that the return type will be represented by the same type metavariable
495 :     in both parts of the mutually recursive definition, and that this
496 :     metavariable is generalized twice, once for the type of f and once for
497 :     g. This needs to be verified by a careful look at the type checking
498 :     process though.
499 :    
500 :     let fun f () = g ()
501 :     and g () = f ()
502 :     in ()
503 :     end;
504 :    
505 :     Another variant would that would show the types of f and g would be:
506 :    
507 :     fun h () =
508 :     let fun f () = g ()
509 :     and g () = f ()
510 :     in (f,g)
511 :     end;
512 :    
513 :     val h = fn : unit -> (unit -> 'a) * (unit -> 'b)
514 :    
515 :     Here it is clear that f and g have independent polymorphic types,
516 :     indicating two independent generalizations.
517 :    
518 :    
519 :     5. Two lexp types in FLINT
520 :     There are two types named lexp: PLambda.lexp (in FLINT/plambda/plambda.sml)
521 :     and FLINT.lexp (in FLINT/flint/flint.sml). The two lexp's have quite different
522 :     definitions. What are the roles of these two lexp types?
523 :    
524 :    
525 :     6. mkAccInfo in Translate (FLINT/trans/translate.sml) ignores the
526 :     second argument (formerly info, now prim). Why is this? Doesn't this
527 :     mean that primops get lost?
528 :    
529 :    
530 :     7. What is the point of PACKexp? In mkExp in Translate (FLINT/trans/translate.sml)
531 :     it is just stripped off.
532 :    
533 :    
534 :     8. Complex abstract syntax for a simple structure declaration.
535 :    
536 :     A simple declaration like
537 :    
538 :     structure X = struct val x = Array.length end
539 :    
540 :     generates a surprising complex abstract syntax representation, looking
541 :     something like (using some shorthand notations) ...
542 :    
543 :     STRB{name = "X",
544 :     str = bindStr,
545 :     def = LETstr (
546 :     STRdec [
547 :     STRB{name = "<tempStr>",
548 :     str = resStr
549 :     def = LETstr (
550 :     VB{pat = vv_x, exp = VARexp(vv_len)), ...}
551 :     STRstr([VALbind(vv_x)])}],
552 :     VARstr(resStr)
553 :     )
554 :     }
555 :    
556 :     where resStr is the structure record returned for the rhs strexp by
557 :     elabStr, and bindStr is the same as resStr except the dacc field is
558 :     replaced by a new lvar, vv_x is the VALvar for the bound variable x,
559 :     and vv_len is the VALvar for Array.length.
560 :    
561 :     This strips down to a skeleton like:
562 :    
563 :     let lv_b = (* lv_b = lvar for bindStr *)
564 :     let lv_r = ... (* lv_r = lvar for resStr *)
565 :     in let <component var decls>
566 :     in [component vars]
567 :     in lv_r
568 :    
569 :     What is the purpose of the outer layer of let binding, and the shift
570 :     in lvars from lv_r to lv_b?
571 :    
572 :    
573 :     9. In Absyn, why do CONexp's also have a tyvar list parameter (like VARexp?).
574 :     Is this only relevant to a few special constructors (maybe ref?), or is it
575 :     also used for ordinary user defined constructors? Similarly for CONpat.
576 :    
577 :     ----------------------------------------------------------------------
578 :    
579 :     10. In ltykernel.sml (lty.sml), the datatype rflag only has one variant,
580 : jhr 5026 and therefore doesn't seem to convey any useful information. Was this
581 : dbm 2265 introduced to make some useful distinction in the future, but this
582 :     distinction was never used or implemented? Can we get rid of this
583 :     useless flag?
584 :    
585 :     11. In ltyextern.sml, the subkinding relation is actually an equality
586 :     relation because there are both rules:
587 :    
588 :     BOX <: MONO
589 :     MONO <: BOX
590 :    
591 : jhr 5026 Is there is reason why we are not just using equality for now? Do we
592 : dbm 2265 really need a subkinding relation? Or was this complication introduced
593 :     in anticipation of some more refined analysis that never got implemented?
594 :    
595 :     12. The kind checker in LtyExternal (tkChkGen) is incomplete, in that
596 :     it does not and cannot properly check closures (Env terms). When kind
597 :     checking an Env(tyc,i,j,tenv) expr, we must type check the tenv as well
598 :     as the body, and we need to extract kind environment info from the tenv
599 :     to use when type checking the body. This means we need to add kind
600 :     specifications to each binder in tenv, so we can translate tenv into
601 :     (a prefix of) a kind environment. We have modified tycEnv to include
602 :     the kind specifications at each binding level, and we have modified the
603 :     kind checker to do a complete check of Env tycs. The kind checker is
604 :     now defined in kernel/lty.sml (structure Lty) and re-exported from
605 :     LtyExtern.
606 :    
607 :     13. In translate.sml, mkVar is calling mkAccInfo, which just drops the
608 :     prim!!!
609 :    
610 : jhr 5026 fun mkVar (v as V.VALvar{access, prim, typ, path}, d) =
611 : dbm 2265 mkAccInfo(access, prim, fn () => toLty d (!typ), getNameOp path)
612 :     | mkVar _ = bug "unexpected vars in mkVar"
613 :    
614 :    
615 :    
616 :    
617 :     ======================================================================
618 :     Invariants for tyc and lty equivalence (and type normalization)
619 :    
620 :     * TC_IND tycs will never have normal flag true, similarly for LT_IND ltys
621 :     and LT_TYC(TC_IND _) ltys. Conversely, if the normal flag is true, the
622 :     body should not be an IND form.
623 :    
624 :     * tycs returned by tc_lzrd, tc_whnm, and tc_norm with not be of the TC_IND form.
625 :     Similarly, ltys returned by lt_lzrd, lt_whnm, and lt_norm will not be of the
626 :     LT_IND or LT_TYC(TC_IND _) forms.
627 :    
628 :     * AUX_REG(true_,_) is computed only by the hashing constructors (*_injX),
629 :     which detect normal forms when calling tc_mk and lt_mk to compute the
630 :     aux value for a type term being hashed.
631 :    
632 :     * upd_tyc and upd_lty only operate on non-normal first args
633 :     (AUX_REG(false,_,_) or NO_AUX), and their result (the updated
634 :     first argument), retain this property of not having a true normal flag.
635 :    
636 :     * tc_eq and lt_eq (pointer equality for tycs and ltys) will only be applied
637 :     to arguments with normalization flag set true.

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