Timeline for How to implement separate compilation?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 18 at 20:16 | comment | added | Mike Shulman | Yes, I already keep track of what's been loaded since even when loading everything from source I don't want to load things multiple times. To tell which unit something comes from, my current idea is that each "identity" is actually a pair of integers, one labeling the unit it came from and one counting the definitions in that unit. Then the compiled file and the loading process both store a correspondence between loaded absolute file paths and numbers, and combining them we obtain a function from numbers to numbers that we apply to the first components of identities as we walk the terms. | |
| Jun 17 at 18:54 | comment | added | Andrej Bauer | I can recommend Xavier Leroy's A modular module system. Even though it's not directly addressing your concerns, it is a very nicely written paper that shows how to think about these matters. | |
| Jun 17 at 18:52 | comment | added | Andrej Bauer |
It ought to be at first sight. You also need to keep track of what's been loaded (probably you should know the absolute file path from which each unit was loaded) so that you don't load things several times. I am not sure how you can tell which unit each thing comes from. Do you have a qualified names, such as UnitA.cat? Do you have open UnitA statements?
|
|
| Jun 17 at 18:40 | comment | added | Mike Shulman | Thanks, I look forward to it. Having now written out the problem carefully, I think I can imagine a solution a bit better. Each compiled unit maintains a list of all the other units it imported, the identity offsets for each of them, and the range of identities that came from that unit. Then when loading it, whenever we encounter an identity in a stored term, we look it up to find what unit it came from, subtract the stored offset for that unit, and then add the corresponding offset for that same unit in the current run. Is that sufficient? | |
| Jun 15 at 21:53 | comment | added | Andrej Bauer | I'll amend my answer. | |
| Jun 15 at 15:45 | comment | added | Mike Shulman | As I said, I could write some code that tries to do this, but it's starting to feel about as complicated as manually munging De Bruijn indices when weakening under binders, and hence as easy to get wrong. So I was hoping that someone else had written out instructions or sample code that I could just copy and be more confident of not making a mistake. | |
| Jun 15 at 15:39 | comment | added | Mike Shulman | But now at the point that $A$ is loaded, maybe we've already loaded $B$ and shifted its $M_B$ by a different constant $C_B'$. So when we pass through the $A$ terms, we don't just have to rename all the $A$ identities by adding one constant $C_A$, we have to rename all the $B$ identities by subtracting $C_B$ and adding $C_B'$. So that means that when we encounter an identity while traversing the $A$ terms, we have to be able to tell which unit it came from originally, and have stored enough information to know what to add to it. | |
| Jun 15 at 15:39 | comment | added | Mike Shulman | Yes, this is indeed the first thing I thought of also. Thanks for writing it out clearly with justification. The complication that I was not sure what to do about is that the unit $A$ could itself import another unit $B$, which might already have been compiled at the time $A$ was compiled. So there is an $M_B$ from when $B$ was compiled, and then when $A$ is compiled it had to shift $M_B$ by adding a constant $C_B$ and those are the identities of the $B$ constants appearing in the saved $A$ terms. | |
| Jun 15 at 12:57 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 72 characters in body
|
| Jun 15 at 9:40 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 233 characters in body
|
| Jun 15 at 8:55 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 2 characters in body
|
| Jun 15 at 8:46 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 570 characters in body
|
| Jun 15 at 8:38 | history | answered | Andrej Bauer | CC BY-SA 4.0 |