From c372cbaa040eed06d9d3a80caead66064b70f5fa Mon Sep 17 00:00:00 2001 From: Alexey Radul Date: Mon, 31 Jul 2023 17:55:16 -0400 Subject: [PATCH] A rationale for why NameMapE is a reasonable data structure as typed. --- src/lib/Name.hs | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/lib/Name.hs b/src/lib/Name.hs index f8e9c7040..94b14d98c 100644 --- a/src/lib/Name.hs +++ b/src/lib/Name.hs @@ -3256,11 +3256,26 @@ instance HoistableB b => HoistableB (WithAttrB a b) where -- === extra data structures === --- A map from names in some scope to values that do not contain names. This is --- not trying to enforce completeness -- a name in the scope can fail to be in --- the map. - --- Hoisting the map removes entries that are no longer in scope. +-- A map from names in some scope to values that may contain names +-- from the same scope. This is not trying to enforce completeness -- +-- a name in the scope can fail to be in the map. + +-- Hoisting the map removes entries for names that are no longer in +-- scope, and then attempts to hoist the remaining values. + +-- This structure is useful for bottom-up code traversals. Once one +-- has traversed some term in scope n, one may be carrying information +-- associated with (some of) the free variables of the term. These +-- free variables are necessarily in the scope n, though they need by +-- no means be all the names in the scope n (that's what a Subst is +-- for). But, if the traversal is alpha-invariant, it cannot be +-- carrying any information about names bound within the term, only +-- the free ones. +-- +-- Further, if the information being carried is E-kinded, the names +-- therein should be resolvable in the same scope n, since those are +-- the only names that are given meaning by the context of the term +-- being traversed. newtype NameMapE (c::C) (e:: E) (n::S) = UnsafeNameMapE (RawNameMap (e n)) deriving (Eq, Semigroup, Monoid, Store) @@ -3330,6 +3345,9 @@ instance RenameE e => RenameE (NameMapE c e) where instance HoistableE e => HoistableE (NameMapE c e) where freeVarsE = undefined +-- A small short-cut: When the information in a NameMapE does not, in +-- fact, reference any names, hoisting the entries cannot fail. + type NameMap (c::C) (a:: *) = NameMapE c (LiftE a) hoistNameMap :: (BindsNames b, Show a)