hey hey! Just wondering what you think of bitbucket.org/pl-uwr/nbe-mar - been curious of approaches to nbe that might be formalizable, but concerned this might end up slowing things down. Eg. not sure how the explicit substs would fare - increasing pointer indirection?
Conversation
Also wondering if you plan on doing pattern matching compilation during the elaboration phase at stage in smalltt - atm I’m trying to add it in my port of nbe-for-mltt, but it seems quite tricky to do after name resolution has been done - have to handle db indices+pattern indices
1
Curious if has any thoughts on how to tackle pattern elaboration in a lang like nbe-for-mltt/mini-tt too. Come across any other examples I might be able to steal from? 😅
1
I think mini-tt by Coquand et al. already has a simple and pretty nice pattern matching implementation, which can be extended to dependent single case split for indexed inductive families. This is only relevant though if you want dep. matching with recursive defs.
1
Oh yeah, mini-tt does hame case trees. I was planning on elaborating pattern matching to case trees like in ‘Elaborating dependent (co)pattern matching’ - once I figure out the paper. Not sure how the handle names in it though.
I was assuming I would desugar my concrete (named) syntax into db indices + pattern indices, then elaborate those nested patterns into case trees, but that might mean I have to do icky, slow db index shifts. So maybe I need to defer name resolution to elaboration time? 😟
1
Ahh, I see that in smalltt you do exactly that! You preserve names all the way into the presyntax. This should make pattern matching compilation a bit easier!