You may have gathered that Epigram 2 features some hardwired universes: enumerations, signatures, datatypes, propositions. The first three of these are themselves coded via datatypes (why stop there, I now ask myself?) and they all involve some fairly hairy looking operators doing rather generic stuff. Correspondingly, we get to hardwire the codes of these datatypes, the types of the operators, and all that stuff. In effect, we’re writing chunks of Epigram in Epigram, but from the inside out. Fortunately, core Epigram 2 now has a functioning typechecker oce more, which means we can tell the machine to typecheck all the hardwired stuff, slightly increasing the probability that we hardwired it right.
I should explain: we’ve been transposing the code so that each universe has its own file, explaining its syntax, typing rules, and so on; some extremely dumb utilities carve up the universe files and slot the relevant pieces into the syntax, the typechecker, ya da ya da. And now, each file of goodies comes with its lump of regression testing, ready to be glommed together and run at kickoff. There’s a word beginning with ‘a’. It’s ‘algebra’.
Tomorrow…oops, later today…it’ll be time to bolt the core that I’ve been refactoring into the proof state navigator that Nicolas and Peter have been building. Manual merge delight. I’ve still got a chunk of stuff to shift before the core is fully operational, but at least I can see the tunnel in the middle of the tunnel.