HR IR Conversion

This article goes over some of the idea of HR to IR conversion

HR ⟷ IR Conversion

The Pass which can be found here deals with the conversion between Core HR and Core IR.

HR ⟶ IR

This phase simply removes the names from the HR form and constructs a De-Brujin index from the names given in HR.

  • The algorithm for this for Terms and Elims is rather simple

    1. When we see a binder (Pi, Lam, Sig, or Let), push the name to the stack for the form in which it is scoped over. Recurse and form and reconstruct said binder.

    2. For forms without names, recurse and reconstruct.

    3. When a name appears, look up it's index from the stack, this is the De-Brujin index we care about. If the Index is not there then we mark it as a Global

HR-Pattern's work in a different way, since patterns are disconnected from terms themselves and do not interact, they work on a system of registering pattern variables, when we come across the binder form =

Outstanding Questions

  • Since for Terms and Elims we don't account for pattern variables, and just mark everything unknown as Global, how does Pattern's affect this? It seems we would mark any PatternVar above this form as a Global and lose that information

IR ⟶ HR

This conversion adds back names to the IR form. This is mainly used for Pretty Printing.

  • The algorithm for Terms and Elims is once again rather simple

    1. When we see a binder (Pi, Lam, Sig, or Let), generate a new name, and push it to the stack. Recurse and form the reconsturct said binder

    2. Forms without names just recurse and reconsturct.

    3. When a name appears, lookup the index from the stack, that position is the name which we care about.

Last modified June 17, 2021 : Push the new tags to link to them better (9c5d3ab)