search

zydeco-lang / zydeco

a proof-of-concept programming language based on Call-by-push-value
Other
49 stars 2 forks source link

Introduce name resolution phase #12

Closed ricky136973 closed 3 weeks ago

ricky136973 commented 2 years ago

We find it necessary at the current stage to have a name resolution phase that does the following things:

LighghtEeloo commented 1 year ago

Let's suspend this till we have for all and exists types.

LighghtEeloo commented 1 year ago

Now that our language is getting richer and richer features, it's a good time to introduce a name resolution phase for the AST before it is sent to the type-directed elaboration phase. This phase aims to convert the names within the AST into a unique form, addressing the issue of alpha-equivalence. Below is an outline of the proposed implementation:

  1. Implement #44.
  2. Implement NameMap, a lookup table from a qualified name (NameRef) to its definition site (NameDef). The definition site is stored in EntityMap below, which is using EntityId to refer to the content of the definitions. Therefore the NameMap is actually of a map of NameView -> EntityId, where NameView is a qualified view of a name. It's only used internally in the name resolution phase.
  3. Implement EntityMap, a SlotMap from an EntityId to an Entity. The Entity stands for a definition of any sort, which could be of term, type or kind sort at the moment. It could change after a dependent type system is introduced. The specific implementation is chosen because slotmaps naturally comes with an Id with an arena like model. It would be helpful for later pushing through the idea of a query system designed for a language server.

The proposal above is only an advice or desired interface. Since @SchwarzXia is also implementing #44 which is closely related to the topic, it might be a good idea to leave the detail to the implementor. Further details and specific implementation steps will be determined and documented as the process unfolds.

LighghtEeloo commented 3 weeks ago

A name resolution phase is included in the current version. Closing.