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
Replying to
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
Replying to
Implicit/explicit subst in formalization is up to taste IMO, implicit subst would have worked in nbe-martinlof as well. In Coq I would choose implicit subst because of autosubst. In practical implementation, implicit subst is better, or more precisely ...
1
1
... we streamline explicit subst in practical implementation so that it only appears in closures (where it's actually needed).
1
1
Show replies