The rain inside has stopped, now that the window in the office upstairs has been closed. Meanwhile, we’ve been reconstructing Ecce to have a matriarchal proof state. The file EcceThump.lhs (which we’ll be splitting into more sensibly named and structured pieces real soon now) is where we’re at. Just now, it even compiles. As I write, the ManChap is hacking up the navigation operations. Together, we’ve been trying to figure out the (anti-)progress propagation stuff. We might even have something worth playing with in a day or two.
But what is a matriarchal proof state? Another one of my ghastly metaphors, you’ve probably guessed. The citizens of this state are (male) parameters and (female) definitions. Definitions all carry a possibly empty module of children, but parameters can’t have subobjects.
Hangonamo! What’s the general idea? The idea is to represent a sequence of parametrised definitions in a more structured way. If you do a bit of work in Epigram 1, then press the magic Alt-Return (Squiggly-Return on a Mac) and look at the trace in the *Epigram-bin* buffer, you’ll see where we’re coming from: it’s a huge and flat sequence of definitions, all with long-names, and often having long parameter sequences just the same as the definition next door. The long-names show the traces of the female line right back to Eve, evidence of a grouping structure which has been flattened out in order to bring sub-definitions into scope. Ecce has been designed to give the same behaviour without flattening the structure.
Syntactically, a thing is a boy or a girl. A girl has a module of things and a definition…
Thing ::= UId : InTerm | UId [Thing*] => Status : InTerm
…which may be unknowable (brown), unknown (yellow), or known (green).
Status ::= # | ? | InTerm
Age increases left-to-right. The boys scope only over their younger siblings and their mother’s definition. The girls scope over all that, but also their younger great*auncles. (An auncle is an aunt or an uncle. Also known as a pibling.)
That is, you can flatten a proof state by lambda-lifting all the definitions over every parameter on the path back to the root. But you don’t have to, because Ecce does it for you. The references we generate corresponding to these proof states are the long-named, lambda-lifted ones. So, same semantics as ever, but we’re preserving the structure. We no longer need to contain subdefinitions inside opaque ‘guesses’. They’re subdefinitions, but they’re lambda-lifted and globally in scope!
More about this, in some more formal style, as soon as I can.
Pulled some patches, Sunday evening. Looks like some good progress. Also looks like I’ve screwed up a few things. Will get on the case in the morning. Cheers, James!
As you may be able to divine from the darcs activity, I’ve been hacking on the train again. Mostly bug-hunting, to be honest. Upshot, we have some sort of navigable proof state with hole-filling and hole-emptying. The way is now clear for much tactic hacking.