Remove types from Constant terms #2437
Conversation
There was a problem hiding this comment.
Looks generally reasonable upon a quick glance of the changes involved. Having to plumb around an extra ModuleMap argument in so many places is a bit unfortunate, but it's not clear how to avoid that would more invasive changes. I've left one inline comment about a particular spot where we may be able to avoid some of this plumbing.
|
|
||
| -- | Get the 'FunName' of a global definition | ||
| mrGlobalDef :: Ident -> MRM t FunName | ||
| mrGlobalDef :: (?mm :: ModuleMap) => Ident -> MRM t FunName |
There was a problem hiding this comment.
Do we need to pass around implicit ?mm :: ModuleMap constraints for things with a return type of MRM, like in this function? My understanding is that we can retrieve a ModuleMap using liftSC0 scGetModuleMap here (as is done in extCnsToFunName, for instance) without needing to plumb extra constraints.
There was a problem hiding this comment.
Indeed, I guess I missed that one. Maybe this means that I'll be able to remove the implicit parameter from a few other functions that call this one too.
There was a problem hiding this comment.
As it turns out, mrGlobalDef is not called by anything; it's dead code, so I just removed it. I rewrote mrCallsFun as you suggested, and that let me remove the constraint on mrFunBodyRecInfo.
Also remove `mrGlobalDef` as dead code.
Constant terms now use the new untyped
Nametype instead ofExtCns. The types of constants are now stored only in the global environment (in theModuleMap) instead of being redundantly stored also in the term AST. Fixes #2383.This change necessitated threading a
ModuleMapthroughout many operations in thesaw-core-coqpackage (moduleMonadifyin particular). Adding an implicit parameter seemed to be the least disruptive way to do this; eventually it would be nice to refactor that code to minimize the use of the implicit parameter.