algebra for macro hiding

An algebra for visible terms

(Below I use brackets ([]) both for lists and for quasiquotation of terms. The meaning should usually be clear from context.)

Some preliminaries: types for terms and paths within a term.

type Term = ....
type Path = [PathPart]
data PathPart = Car | Cdr
-- path order: for the sake of concreteness, let's say outermost-first
-- that is, the path (Car::p') means take the car and then follow path p'
termAt : Term -> Path -> Term

The point is to define a type VT to represent the visible terms and an operation seek that checks whether a particular term is visible (and if so, where). There is a constructor of VT for the inital hidden term; other constructors correspond to events that happen in macro expansion that update our notion of what to look for.

-- VT represents the "visible subterms" of a hidden macro use
-- (possibly after it has been updated from other expansions)
data VT =
| Term(Term)
| AddScope(Term to Term, Term)
| Arm(Term to Term, Term)
| Disarm(Term to Term, Term)
| ... -- whatever else is needed

Attempt 1

seek : Term -> VT -> Maybe Path

The base case just searches within a term. This variant could be optimized as a hash table.

seek eS Term(eH) = return path    when eS occurs in eS at path
                 = fail           otherwise

The AddScope case combines the path of eS within the renaming's new part with the path of the renaming's old part within the parent vt.

seek eS AddScope(e to e', vt)
  = do { path1 <- seek eS Term(e')
         path2 <- seek e' vt
         return path2 ++ path1 }
    `disj` (seek eS vt)

Alas, this is wrong. It might be the case that the renamed term is "bigger than" (ie is not a subterm of) the visible term in vt---causing path2 <- seek e' vt to fail---but the subterm of e' corresponding to eS is a subterm of vt. For example: seek [e] AddScope([(x eS)] to [(x^s e^s)^s], term([(m e)]).

Attempt 2

We fix the AddScope case by narrowing the term to search for in the parent vt:

seek eS AddScope(e to e', vt)
  = do { path1 <- seek eS Term(e')
         path2 <- seek (termAt e path1) vt
         return path2 }
    `disj` (seek eS vt)

What if the rename (e to e') involves armed terms? We can't go searching within an armed term (or rather, if we do we won't find anything), so we need to make arm and disarm cancel out.

seek eS Arm(e to eA, vt)
  = do { path1 <- seek eS Term(eA)   -- path1 <- (if eS = eA then return [] else fail)
         path2 <- seek e vt
         return path2 ++ path1 }
    `disj` (seek eS vt)

seek eS Disarm(eA to eDA, vt)
  = do { path1 <- seek sS Term(eDA)
         path2 <- seek eA vt
         return path2 ++ path1 }
    `disj` (seek eS vt)

Unfortunately, this doesn't work either. The arm and disarm may cancel, but together they still propagate back a search for a term that doesn't occur in the base term. Consider this example:

seek e^s Disarm  ( [<(f^s e^s)^s>] to [(f^s e^s)^s],
         AddScope( [<(f e)>] to [<(f^s e^s)^s>],
         Arm     ( [(f e)] to [<(f e)>],
         Term    ( [(m e)] ))))

This time we can't fix the problem by eagerly narrowing the search, because of the armed intermediate term. Instead, we need to delay the narrowing obligation incurred by Disarm until it can be discharged by Arm. (We need to apply the delayed narrowing immediately after the Arm, not immediately before the Term. What if there were a renaming between them? Need to narrow to search the renaming.)

So we need to revisit the signature of seek to allow for delayed narrowings. But first, we should consider the following additional complications:

1. Arms and Disarms don't have to balance. We could arm the same term twice and disarm it once.
2. Nesting is also possible: an armed term might have an armed subterm; they must be disarmed separately.
3. The macro expander has a powerful inspector that disarms all dye packs. But a macro with a weak inspector might only disarm some of a term's dye packs.

On the other hand, the macro expander never emits a rename for terms within an armed term without first disarming it. So at least we don't have to worry about that case.

Point 1 (unbalanced) suggests an additional branch in the search. Point 2 (nesting) suggests that we should add a stack of delayed narrowings rather than just one. I intend to ignore point 3 for now, but it might get resolved automatically as a consequence of point 1.

Here's an example with nested arming:

seek e' Disarm  ( [<f' e'>'] to [(f' e')'],
        Disarm  ( [<g' <f' e'>'>'] to [(g' <f' e'>')'],
        AddScope( [<g <f e>>] to [<g' <f' e'>'>'],
        Arm     ( [(g <f e>)] to [<g <f e>>],
        Arm     ( [(f e)] to [<f e>],
        Term    ( [(m e)] ))))))

Attempt 3

seek : Term -> VT -> [Path] -> Maybe Path
-- the third argument is a stack of delayed narrowings

...

Attempt 4

I think that handles the "up the tree" cases. What about the "down the tree" cases? For example, suppose the following tree occurs in a hidden context:

      ...                  ...
   ---------            ---------
   e1 => e1'            e2 => e2'
  --------------------------------
  (#%app e1 e2) => (#%app e1' e2')

In particular, need to handle

• joining results of independent sub-expansions
• addition of syntax (the #%app form) around sub-expansion results --- or maybe not, if the updates were done in the context of the original hidden term to begin with (??)