rogerburtonpatel / vml

Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
5 stars 0 forks source link

Review Feb 18 work #33

Closed rogerburtonpatel closed 4 months ago

rogerburtonpatel commented 4 months ago

Review tex/syntax-and-judgement/pplus/syntax-judgement-pplus.pdf. It has a Makefile to build it this time, and you don't need simplebnf installed.

  1. What do you think of the metavariable $p^{t}$ for Top-level patterns? I don't love it.
  2. Do you know any tricks for speeding up latex compilation? I've tried setting no compression; didn't help much.
  3. I borrow heavily from your rules for pattern matching. How can I appropriately credit you?
  4. Your evaluation judgement in nanoML has a $\sigma$: $\langle e, \rho, \sigma \rangle \Downarrow v$. I believe this is for typing, though the $\sigma + \rho'$ on for rule $\textrm{CaseMatch}$ on page 492 suggests otherwise. Is this a typo, or is $\sigma$ important or necessary in untyped PPlus?
  5. There are a few notes under rab. Grepping for \rab should find them.

Review src/pplus/pplus-parse.sml and .../pplus-lex.sml.

  1. I wonder about my use of COMMA, BACKSLASH, etc, and if the way I've done it is reasonable.
  2. Removing bracketed from the toplevelpatterns causes an OOM crash. My theory is that toplevelpattern attempting to immediately parse a toplevelpattern under fix is poison. Can I work around this somehow?
nrnrnr commented 4 months ago

The document:

  1. I don't love top-level patterns, period. Why have two levels?

  2. On my machine your LaTeX is running in 1.6 seconds. I tried annotate-output but it didn't illuminate things. But something is happening about here in your .log file:

    (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd
    File: umsb.fd 2013/01/14 v3.01 AMS symbols B
    )
    > Step: init table outer spec.
    > Step: parse table options.
    > Step: split table.
    > Step: init table inner spec.
    > Step: parse table inner spec.
    > Step: execute table commands.
    > Step: calculate cell and line sizes.
    > Step: build the whole table.

    I'd try tracking that to its lair.

  3. "These rules are a variation on the rules found in Ramsey (2022, Section 8.X)," for some value of X.

  4. How vexing. The sigma should not be there, and it should be rho + rho', not sigma + rho'. Both faults are an artifact of using the wrong \eval macro in that chapter.

  5. I have no particular thoughts about the \rab notes.

rogerburtonpatel commented 4 months ago
  1. I'll think on this. I have reasons for separating the two which I intend(ed) to bring up in our next meeting; seeing you strongly suggest otherwise is making me reconsider. 2-4. Got it. 5- The question is: You have a few paragraphs about having a literal as the case scrutinee, about what disjoint union means, and about how + works. Should I include these close to verbatim, or reference them in your book with a brief description? I'm thinking the latter.
nrnrnr commented 4 months ago

The code:

  1. It's a bit odd to have the two different lexical categories RESERVED and SPECIAL. Why aren't comma and friends reserved words?

    It's also not clear that the LEFT and RIGHT are useful in your setting.

    Bottom line: could be simpler, probably not worth changing.

  2. Parsing combinators are effectively LL(k), which means you can't have left recursion. Let me spitball an EBNF grammar, adapted from Wirth's classic grammar for Pascal:

    p ::= term {| term} term ::= factor {, factor} factor ::= atom {when exp} atom ::= x | K {atom} | ❨p❩

nrnrnr commented 4 months ago
  1. Don't incorporate technical material by reference. You should explain disjoint union and +, but not necessarily the way I did. Your proximate audience is your thesis committee. Your ultimate audience is PL professionals.

    On further reflection, Alva may benefit from a detailed explanation.

rogerburtonpatel commented 4 months ago

p ::= term {| term} term ::= factor {, factor} factor ::= atom <- exp // pattern guard; expression results in atom | atom {when exp} // side condition; expression results in true atom ::= x | K {atom} | ❨p❩

I like this, except that a pattern guard can look like ❨p❩ <- exp, which could look like This when condition <- exp, which is a bit odd.

nrnrnr commented 4 months ago

Embrace the oddness!