Scoping, no really
Peter and I started writing the Scoper earlier. See Scoper.lhs. In particular, check out the definition of Concrete, which is about as simple as it’s likely to get. We’ve suspended any funny ideas about imperative data structures for concrete syntax, but we are using imperative refs for ‘acts of naming’, allowing change of the associated string.
Given some feverish after-dinner hacking with Wouter, we now have scoping for a good chunk of CTerm, including all of CPat, and it seems to be doing the right thing. Our mechanism for accumulating ‘shadows’ is in place, but we haven’t yet implemented anything which might discharge a shadow, so it’s hard to see the point just now.
How to play: run ghci -fglasgow-exts Scoper.lhs in a colourful shell, and try typing
testScoper (B0 :< ScShadow) Blue cSigs
X : *
Y : all X : * => X
x : X
Or
testScoper (B0 :< ScShadow) () cTerm
lam f => f x x
Or
testScoper (B0 :< ScShadow) () cTerm
lam (lam x => (f x ; g x)) => f x
You’ll be glad you did.
We need to finish off the Scoper for the rest of the concrete syntax, and also to start prettyprinting the result. It’s just possible that these might be sufficiently orthogonal tasks to work in parallel…