James the First

First instalment of an Epigram 1 change I’ve been intending to do for ages. Almost no effort required! I’ve fixed things so that variables named but not declared in the premises of a rule get inserted implicitly at the left end of the rule (as James McKinna used to argue) rather than as locally as possible (as Randy Pollack used to argue). vcons now gets X and n implicitly before x and xs; n used to come in the middle, unless you explicitly forced it leftward. Generally, I find that partial applications work more pleasantly more often with James’s convention. You can still force things rightward with an explicit premise (which doesn’t mean the arg has to be explicit).

Anyhow, I imagine this change may cause minor damage. I’ve tried a few examples, and I had to tweak a thing or two: mostly stuff that was a bit chancy anyway and should have been cleaned up long ago. I suggest that regulars try out their favourites and howl if they aren’t readily fixable.

There will be a second and more subtle change: at the moment, uninstantiated metavariables in rules are generalised to yield implicit arguments wherever they end up; these also should be shunted leftward where possible. Probably won’t do any damage, except to code which relies on the current morally random placement.

I don’t think we should generate new binaries just yet; I’ll try and get this cleaned up as soon as possible.

3 Responses to “James the First”

  1. Conor Says:

    Peter’s regression testing found an unusual bug which (because I forgot the format of the Meta-Return entrails) looked worse than it was. Even so, it was a weird scope error in the unification algorithm which should have kicked us more noticeably before now. I wonder why it hadn’t.

  2. pwm Says:

    Another oddity, why does this no longer mean what I think it does:

    n : Nat ; f : Fin n -> X
    ————————
    vtab _n f : Vec X n

    vtab _n f []

    in the context of the shed n : *…

  3. Conor Says:

    That’s a bug. Basically, I’m not done with the changes yet. Phase 1 requires X to be far left exactly because it hasn’t been declared. Manual override should, er, override. When I next get a mo…

    Meanwhile, the fix is to say n; X ; Fin n -> X to ensure that n can stand before X.

Leave a Reply