Sound and Fury Signifying Nothing

[pigworker]

There's a bunch of stuff I want to do under the hood, none of which will deliver the slightest extension of positive functionality. Rather, it will put the house in order before we move on.

0 Chuck Out Dead Files

I did a lot of refactoring today, which involved making replacement candidates for old files under new names (e.g., LexAsk → Lexing). I also chopped up the old Ask.Src.ChkRaw to split out "library" code. The old files are now useless. They should go.

1 Monadify

We have a lot of code (in Ask.Src.ChkRaw) which passes stuff like Setup and Context around explicitly. That should be tidied up into a monad, so we can hide the plumbing, and so that it is less disruptive to change how we manage the setup or add extra machinery. Speaking of which...

2 Go Locally Nameless

At the moment, unquantified variables in a top-level goal are treated as Skolem constants and represented as de Bruijn indices. This is sustainable only as long as no local variable binding happens. We should go locally nameless so that we get both weakening and alpha-equivalence for free. That means plumbing a name supply, which is just another bit of environment to hide in the monad.

3 Typechecking

Even if we have, so far, only one type, viz. Prop, we should check that the formulae people write are well typed. Just now, spurious "constructors" generate propositions with no introduction rules. We'd give better feedback about beginner mistakes (e.g. prove AndI ?) and we'd be getting ready for more interesting types. Just now, we don't need any type synthesis. That said, having gone locally nameless, the reference to any given name should cache a pointer to the type of that name.

4 Extract Rules from Prop Declarations

The parser can already get us from tokens to "raw" syntax, in declarations like

prop Prop -> Prop where
  prove a -> b by ImpI where
    given a prove b

but we don't get all the way to actionable values of type Rule, hence the current holding pattern that is Ask.Src.HardwiredRules. If we actually turned the head of prop declarations into proper constructor declarations that feed into the typechecker and the body into rules, we could do that stuff in software. It would be good to allow Marx-hosted ask puzzles to choose the "prelude" to any given task.

The Contradiction rule (TIS AGIN NATURE!) presents an anomaly that we'll need to bikeshed, in that it is a rule which is not extracted from a prop declaration. So how is it to be declared? Perhaps (resisting whole new keywords)

import where
  prove p by Contradiction where
    given Not p prove False

The question is what top-level declaration introduces a block of rules that we insist upon without justification (and do not invert when computing the behaviour of from).

But I digress.

5 Head/Full Normalisation

Internally introduce a notion of "prop synonym". Implement the machinery to head-normalise terms, and then push to full on normalisation. Do pattern matching up to head normalisation and "is it given?" checking up to full normalisation. Without giving the users the opportunity to write definitions, nobody will notice that we have done this.

Epilogue

When we have done these things, nobody will notice the blindest bit of difference, but we shall be cooking with gas.

[pigworker]

So far, I've done 0 and 1.

[pigworker]

Now we're locally nameless. And we also have existential variables. The machinery is beginning to fall into place.

[pigworker]

This is all done.