Running into an issue with my elaborator. It seems that I get lots of bloated definition when I elaborate to my core syntax - seemingly because `synth_term` unfolds variables to their definitions a bit too eagerly. Was wondering if you had any tips! cc.
Conversation
This is the main part that does the work of elaborating items: github.com/brendanzab/rus - I'm thinking it might be worth limiting the the `read_back_value` line to lookup variables in my implementation of nbe?
2
So you want to weaken forward declared types to the scope of their definitions. Readback is not good because you don't want normal forms in elab output. I can think of several solutions varying in simplicity and generality.
1
1
a) Implement weakening directly on core syntax, store plain elaborated types in forward_declarations, weaken them as needed. This is pretty efficient because you only need to weaken each forward declared type once.
1
1
b) Distinguish "top" and "local" contexts already in syntax, use de Bruijn levels for top variables, thereby making weakening free.
1
2
c) Just don't weaken forward decl types. You only ever lose scoping information by weakening, you can still do everything if forward types stay in their original scope.
1
1
c) seems nicest and easiest to me for your current impl, a) is OK and simple but I'd generally avoid weakening, b) is not so simple but you may need it anyway if you also want non-bloated meta solutions.
1
By c) do you mean just storing the types as values in the elaborated AST?
1
I mean, when you elaborate a forward type, it's valid in the current context, and then you leave the type in that context, so check_items returns something which contains forward types and definitions interleaved (or in any way which remembers scopes).
2
1
Ooh, and just don't store the synthesized type when they are omitted, right! Gotcha! 🙂
2
Ok, here we go - this looks better now! I had to add annotations into the core syntax otherwise my validator broke in some places, but I think that's ok! github.com/brendanzab/rus