Epilogue

We need a generic protocol for communicating and elaborating concrete syntax. This creates a problem. How specific should we be wrt the syntactic categories of Epigram? My inclination is not at all. We either need a generic technology which will adapt to arbitrary syntactic categories, or we need to flatten the syntactic categories. At the moment, I don’t feel like figuring out how to do the former. So I suggest we adopt some very general setup like this

type Concrete shed = (Mark, CTree shed)
data CTree shed
  = CShed shed
  | CNode Node [Concrete shed]


Remarks

• It’s polymorphic in the contents of sheds, but the elaborator is only ever sent Concrete ()
• The type Mark is some equality type which belongs to the UI: it is used to mark information coming back from the elaborator as concrete syntax is processed.
• The type Node represents both the terminal and nonterminal symbols, whatever they may be. Blah code will need to interrogate this type in arbitrary ways, so things might get a touch existential. As in
  data Blah
  = ...
  | ∀α. Case (Node → Maybe α, [String]) (α → Blah) Blah

  The function tests if the node suits the success continuation. If so, the strings name the subnodes and the success continuation executes; if not, the failure case runs. Of course, the whole thing suspends if we have a shed rather than a node.

Parsing to this representation requires that we can generate suitable elements of Mark (I suspect this may involve refs.) The real exciting stuff in the parser is more likely to involve figuring names out—more on that anon.

Printing. Hmm.

This entry was posted on Monday, June 6th, 2005 at 3:49 pm and is filed under General, Hacking. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.