Adopt canonical call syntax and wire in orphaned tokens

- Function calls are f(a, b) via a postfix argument list; juxtaposition
  application removed; nullary calls f() supported
- Wire DEFINITION (x ≜ e), ALLOC/RELEASE postfix (r ⊕ / r ⊖), channel
  operations (⇀_ch e / ↽_ch e), and qualified module access (M‧f)
- Delete tokens with no rule and no example: QUERY (?), EXISTS, IMPORT,
  ARROW, DOT; delete the unary ? prefix operator
- Canonical handler clause: ↯pattern ⟹ expr (pattern is an identifier or
  a string); clauses separated by semicolons
- SEMICOLON has one role: sequence separator with optional trailing use
- Disambiguate braces structurally: record ({a: e}), set ({a, b}), block
- IDENTIFIER no longer allows a leading underscore, so subscripts such as
  ⌉_db_lock and ↽_socket lex as UNDERSCORE + IDENTIFIER
- Add '/' as ASCII alias of ÷; add unary minus; pathLiteral accepts
  🖫identifier as well as 🖫"…"
- Exactly one ASCII escape per glyph (drop \lam, \gets, \ne, \le, \ge,
  \vee, \wedge, \cup alias forms, \N, \Z, \Q, \R, \C, \B)
- Replace deprecated ANTLRInputStream with CharStreams in the test
  harness: it fed UTF-16 units and could never tokenize the
  supplementary-plane glyphs 𝔹, 𝓜 and 🖫
- Update LexerTest/ParserTest to canonical syntax; add coverage for
  subscript lexing, channels, resources, module access, unary minus,
  nullary calls, and negative tests for juxtaposition and the ternary
This commit is contained in:
developtheweb 2026-07-09 02:51:12 -04:00
parent 5230273ab1
commit f076a1dade
6 changed files with 253 additions and 111 deletions

View file

@ -11,3 +11,19 @@ against the existing examples.
- **The Java package for generated code comes from `-package` in build.gradle only**; rejected: `@header` package declaration in the grammar (combined with `-package` it generates a duplicate `package` statement that does not compile). - **The Java package for generated code comes from `-package` in build.gradle only**; rejected: `@header` package declaration in the grammar (combined with `-package` it generates a duplicate `package` statement that does not compile).
- **ANTLR warnings fail the build** (`-Werror` in build.gradle); rejected: warnings as advisory output (they hid the shadowed-token bugs). - **ANTLR warnings fail the build** (`-Werror` in build.gradle); rejected: warnings as advisory output (they hid the shadowed-token bugs).
- **The choice-type rule is `⟨ expr ⟩`** with the interior `|` consumed by `condExpr`; rejected: explicit `⟨ expr | expr ⟩` (the interior expr already consumes the bar, making the explicit BAR unreachable). - **The choice-type rule is `⟨ expr ⟩`** with the interior `|` consumed by `condExpr`; rejected: explicit `⟨ expr | expr ⟩` (the interior expr already consumes the bar, making the explicit BAR unreachable).
- **Function calls are `f(a, b)` — a postfix argument list, nullary `f()` included**; rejected: Haskell juxtaposition `f x` (programmer convention, fails the Fatima test — children learn `f(x)` in school).
- **SEMICOLON has one role: sequence separator (trailing `;` permitted)**; the program, blocks, `(...)`, `⌈...⌉`, `...`, `⌜...⌝`, `⌞...⌟` and `⟳(...)` all contain one `seqExpr`; rejected: a separate statement-terminator rule duplicating the same token (two roles for one symbol).
- **Braces disambiguate structurally**: `IDENTIFIER :` → record, two-plus comma-separated exprs → set, everything else (incl. `{}` and `{x}`) → block; a singleton set literal cannot be written (deferred to M1); rejected: parser-order coin flips left undocumented.
- **`≜` defines, `←` assigns; both wired into the chain** with `≜` binding looser than `←`, both right-associative; rejected: `≜` tokenized but unreachable.
- **`⊕`/`⊖` are postfix resource operators** (`database ⊕`, `conn ⊖`), matching every example; rejected: prefix form `⊕open(path)` that appeared only in the whitepaper.
- **Channel operations are subscripted prefix operators** `⇀_ch expr` / `↽_ch expr`; rejected: leaving SEND/RECEIVE orphaned.
- **`‧` is qualified module access** (`Mathematics‧sin(angle)`), a postfix `‧IDENTIFIER`; rejected: leaving MIDDOT orphaned, or `.` (removed — one access syntax).
- **Handler clauses are `↯pattern ⟹ expr`, semicolon-separated**, where pattern is an identifier (binds the exception) or a string (matches a message); rejected: `↯e ⇒ expr` (⇒ is EXPORT; the clause arrow should mirror the guarded-alternative arrow ⟹).
- **IDENTIFIER may not start with `_`**, so subscripts (`⌉_db_lock`, `↽_socket`) lex as UNDERSCORE + IDENTIFIER; rejected: identifiers with a leading underscore (made every subscript lex as one identifier token).
- **`/` is an ASCII alias of ÷ (DIV)** so `π/4` parses; rejected: ÷-only division (unreachable on most keyboards).
- **Unary minus exists** (`-x`), sharing the MINUS token at prefix level; rejected: binary-only minus (cannot write negative numbers); unary plus was NOT added (`x ++ y` stays invalid).
- **`pathLiteral` accepts `🖫"…"` and `🖫identifier`**, as required by `readFile(🖫path)` in example 03.
- **Deleted tokens: `?` (QUERY), `∃` (EXISTS), `⇐` (IMPORT), `→` (ARROW), `.` (DOT)** — defined but used by no parser rule and no example; dead operators are debt; each returns in M1 only with a documented semantic. Rejected: keeping them tokenized-but-unreachable.
- **Exactly one ASCII escape per glyph** (`\lambda` not `\lam`, `\leftarrow` not `\gets`, `\neq` not `\ne`, `\nat` not `\N`, …); rejected: alias sets (two ways to write the same token).
- **`%` (modulo), `∑`, `√`, `²`, `|x|`, ranges `[a..b]`, indexing/slicing, `where`, and record field access are NOT in M0** — every document says so instead of using them; deferred to M1 with semantics, not smuggled in via prose.
- **Lambda parameters are a bare comma-separated pattern list** (`λa, b: body`); rejected: parenthesized parameter lists `λ(a, b):` (two ways to write parameters).

View file

@ -5,56 +5,76 @@ grammar MPL;
// ============================================================================ // ============================================================================
// PARSER RULES // PARSER RULES
//
// Structural decisions (see DECISIONS.md for rationale):
//
// * SEMICOLON has exactly one role: it separates expressions in a sequence
// (`seqExpr`). A trailing semicolon is permitted. There is no separate
// "statement terminator" concept; the program, blocks, parenthesized
// groups, atomic sections, RAII scopes and code quotations all contain a
// single seqExpr.
//
// * Braces are disambiguated structurally:
// - record: `{ name: expr, ... }` — at least one `IDENTIFIER : expr`
// - set: `{ a, b, ... }` — at least TWO comma-separated exprs
// - block: everything else, including `{}` and `{ x }`
// A singleton set cannot be written literally (use ∅ and set operations
// in M1); singleton braces always parse as a block.
//
// * Function calls are `f(a, b)` only — a postfix argument list. Haskell
// juxtaposition (`f x`) was removed. Nullary calls `f()` are supported.
//
// * ≜ defines (right-associative, binds looser than ←); ← assigns.
//
// * Guarded alternatives `(condition ⟹ result) | fallback` are the one
// conditional form, wired in as the condExpr precedence level.
// ============================================================================ // ============================================================================
program program
: statement* EOF : seqExpr? EOF
;
statement
: expr SEMICOLON
| expr // Allow last statement without semicolon
;
// Expression hierarchy following precedence table (lowest to highest)
expr
: seqExpr // Level -2: Statement sequencing
; ;
seqExpr seqExpr
: parallelExpr (SEMICOLON parallelExpr)* : expr (SEMICOLON expr)* SEMICOLON?
;
// Expression precedence chain, lowest binding first.
expr
: parallelExpr
; ;
parallelExpr parallelExpr
: assignExpr (PARALLEL assignExpr)* // Level -1: Parallel composition : defExpr (PARALLEL defExpr)* // ‖ parallel composition
;
defExpr
: assignExpr (DEFINITION defExpr)? // ≜ definition (right-assoc)
; ;
assignExpr assignExpr
: condExpr (LEFTARROW assignExpr)? // Level 0: Assignment (right-assoc) : condExpr (LEFTARROW assignExpr)? // ← assignment (right-assoc)
; ;
// Guarded alternatives: (condition ⟹ result) | fallback // Guarded alternatives: (condition ⟹ result) | fallback
// This is the canonical conditional form. It lives in the precedence chain // The one conditional form. The BAR inside ⟨a|b⟩ is also consumed here.
// (below assignment, above implication) instead of being a left-recursive
// standalone rule, which previously caused ANTLR error(119).
condExpr condExpr
: impliesExpr (BAR impliesExpr)* : impliesExpr (BAR impliesExpr)*
; ;
impliesExpr impliesExpr
: orExpr (IMPLIES impliesExpr)? // Level 1: Implication (right-assoc) : orExpr (IMPLIES impliesExpr)? // ⟹ guard/implication (right-assoc)
; ;
orExpr orExpr
: andExpr (OR andExpr)* // Level 2: Logical OR (left-assoc) : andExpr (OR andExpr)* // logical OR
; ;
andExpr andExpr
: compareExpr (AND compareExpr)* // Level 3: Logical AND (left-assoc) : cmpExpr (AND cmpExpr)* // ∧ logical AND
; ;
compareExpr cmpExpr
: addExpr (compareOp addExpr)? // Level 4: Comparisons (non-assoc) : addExpr (compareOp addExpr)? // comparisons (non-associative)
; ;
compareOp compareOp
@ -62,48 +82,60 @@ compareOp
; ;
addExpr addExpr
: mulExpr ((PLUS | MINUS) mulExpr)* // Level 5: Addition/subtraction : mulExpr ((PLUS | MINUS) mulExpr)*
; ;
mulExpr mulExpr
: composeExpr ((TIMES | DIV | AST) composeExpr)* // Level 6: Multiplication : composeExpr ((TIMES | DIV | AST) composeExpr)*
; ;
composeExpr composeExpr
: unaryExpr (COMPOSE unaryExpr)* // Level 7: Composition : unaryExpr (COMPOSE unaryExpr)* // ∘ function composition
; ;
unaryExpr unaryExpr
: prefixOp* postfixExpr // Level 8: Prefix operators : (prefixOp | channelOp)* postfixExpr
; ;
// MINUS doubles as unary negation: -x
prefixOp prefixOp
: RAISE | TRACE | QUERY | BREAK | DELAY : RAISE | TRACE | BREAK | DELAY | MINUS
; ;
// Exception handling is a postfix construct: expr ↴ { ↯name ⇒ handler } // Channel operations are subscripted prefix operators: ⇀_ch expr, ↽_ch expr
// Formerly a standalone rule reachable from atomExpr, which cycled back into channelOp
// expr and caused ANTLR error(119) (mutual left recursion). : (SEND | RECEIVE) UNDERSCORE IDENTIFIER
;
// Postfix operators: call, qualified access, resource alloc/release, handler.
postfixExpr postfixExpr
: appExpr handlerSuffix* : atomExpr postfixOp*
; ;
handlerSuffix postfixOp
: HANDLE LBRACE handlerClause+ RBRACE : callArgs // f(a, b) — the one call syntax
| MIDDOT IDENTIFIER // Module‧member
| ALLOC // resource ⊕
| RELEASE // resource ⊖
| HANDLE handlerBlock // expr ↴ { ↯pat ⟹ expr; ... }
; ;
callArgs
: LPAREN (expr (COMMA expr)*)? RPAREN
;
handlerBlock
: LBRACE handlerClause (SEMICOLON handlerClause)* SEMICOLON? RBRACE
;
// ↯identifier binds the exception; ↯"literal" matches a specific message.
// The clause arrow is ⟹, mirroring guarded alternatives.
handlerClause handlerClause
: RAISE IDENTIFIER EXPORT expr : RAISE (IDENTIFIER | STRING) IMPLIES expr
;
appExpr
: atomExpr atomExpr* // Level 9: Function application
; ;
atomExpr atomExpr
: primary : LPAREN seqExpr RPAREN
| LPAREN expr RPAREN
| block
| lambda | lambda
| forall | forall
| choiceType | choiceType
@ -114,6 +146,10 @@ atomExpr
| periodicTask | periodicTask
| moduleDecl | moduleDecl
| pathLiteral | pathLiteral
| record
| set
| block
| primary
; ;
primary primary
@ -128,13 +164,11 @@ primary
| EMPTYSET | EMPTYSET
| typeSymbol | typeSymbol
| list | list
| set
| record
; ;
greekVar greekVar
: ALPHA | BETA | GAMMA | DELTA | EPSILON | ZETA | ETA | THETA : ALPHA | BETA | GAMMA | DELTA | EPSILON | ZETA | ETA | THETA
| IOTA | KAPPA | LAMBDA_VAR | MU | NU | XI | OMICRON | PI | IOTA | KAPPA | LAMBDA_VAR | MU | NU | XI | OMICRON | PI
| RHO | SIGMA | TAU | UPSILON | PHI | CHI | PSI | OMEGA | RHO | SIGMA | TAU | UPSILON | PHI | CHI | PSI | OMEGA
; ;
@ -142,16 +176,13 @@ typeSymbol
: NAT | INT | RAT | REAL | COMPLEX | BOOL : NAT | INT | RAT | REAL | COMPLEX | BOOL
; ;
block // λx: body λx,y: body λx∈: body — parameters are a bare pattern list.
: LBRACE statement* RBRACE
;
lambda lambda
: LAMBDA_VAR pattern (IN expr)? COLON expr : LAMBDA_VAR pattern (IN condExpr)? COLON expr
; ;
forall forall
: FORALL pattern IN expr COLON expr : FORALL pattern IN condExpr COLON expr
; ;
// The | inside ⟨a|b⟩ is consumed by condExpr, so the rule needs no explicit BAR. // The | inside ⟨a|b⟩ is consumed by condExpr, so the rule needs no explicit BAR.
@ -160,23 +191,23 @@ choiceType
; ;
atomicSection atomicSection
: LCEIL expr RCEIL (UNDERSCORE IDENTIFIER)? : LCEIL seqExpr RCEIL (UNDERSCORE IDENTIFIER)?
; ;
raiiScope raiiScope
: LRAII statement* RRAII : LRAII seqExpr? RRAII
; ;
codeQuote codeQuote
: ULCORNER expr URCORNER : ULCORNER seqExpr URCORNER
; ;
codeEval codeEval
: LLCORNER expr LRCORNER : LLCORNER seqExpr LRCORNER
; ;
periodicTask periodicTask
: PERIODIC LPAREN expr COMMA NUMBER IDENTIFIER? RPAREN : PERIODIC LPAREN seqExpr COMMA NUMBER IDENTIFIER? RPAREN
; ;
moduleDecl moduleDecl
@ -184,7 +215,7 @@ moduleDecl
; ;
pathLiteral pathLiteral
: PATH STRING : PATH (STRING | IDENTIFIER)
; ;
// Rewritten from the left-recursive, empty-tail form that caused error(148). // Rewritten from the left-recursive, empty-tail form that caused error(148).
@ -202,8 +233,9 @@ list
: LBRACK (expr (COMMA expr)*)? RBRACK : LBRACK (expr (COMMA expr)*)? RBRACK
; ;
// At least two elements — singleton braces parse as a block (see header note).
set set
: LBRACE (expr (COMMA expr)*)? RBRACE : LBRACE expr (COMMA expr)+ RBRACE
; ;
record record
@ -214,8 +246,15 @@ fieldAssignment
: IDENTIFIER COLON expr : IDENTIFIER COLON expr
; ;
block
: LBRACE seqExpr? RBRACE
;
// ============================================================================ // ============================================================================
// LEXER RULES // LEXER RULES
//
// Exactly one ASCII escape per glyph (One Right Answer). The authoritative
// escape table is glyph-escapes.md, which must match these rules exactly.
// ============================================================================ // ============================================================================
// Keywords // Keywords
@ -234,7 +273,7 @@ ETA : 'η' | '\\eta' ;
THETA : 'θ' | '\\theta' ; THETA : 'θ' | '\\theta' ;
IOTA : 'ι' | '\\iota' ; IOTA : 'ι' | '\\iota' ;
KAPPA : 'κ' | '\\kappa' ; KAPPA : 'κ' | '\\kappa' ;
LAMBDA_VAR : 'λ' | '\\lambda' | '\\lam' ; LAMBDA_VAR : 'λ' | '\\lambda' ;
MU : 'μ' | '\\mu' ; MU : 'μ' | '\\mu' ;
NU : 'ν' | '\\nu' ; NU : 'ν' | '\\nu' ;
XI : 'ξ' | '\\xi' ; XI : 'ξ' | '\\xi' ;
@ -250,41 +289,40 @@ PSI : 'ψ' | '\\psi' ;
OMEGA : 'ω' | '\\omega' ; OMEGA : 'ω' | '\\omega' ;
// Type symbols // Type symbols
NAT : '' | '\\nat' | '\\N' ; NAT : '' | '\\nat' ;
INT : '' | '\\int' | '\\Z' ; INT : '' | '\\int' ;
RAT : '' | '\\rat' | '\\Q' ; RAT : '' | '\\rat' ;
REAL : '' | '\\real' | '\\R' ; REAL : '' | '\\real' ;
COMPLEX : '' | '\\complex' | '\\C' ; COMPLEX : '' | '\\complex' ;
BOOL : '𝔹' | '\\bool' | '\\B' ; BOOL : '𝔹' | '\\bool' ;
// Operators by precedence // Operators by precedence
SEMICOLON : ';' ; SEMICOLON : ';' ;
PARALLEL : '‖' | '\\parallel' ; PARALLEL : '‖' | '\\parallel' ;
LEFTARROW : '←' | '\\leftarrow' | '\\gets' ; LEFTARROW : '←' | '\\leftarrow' ;
// '\Rightarrow' belongs to EXPORT (⇒); giving it to IMPLIES too fully // '\Rightarrow' belongs to EXPORT (⇒); giving it to IMPLIES too fully
// shadowed EXPORT's escape (ANTLR warning 184). // shadowed EXPORT's escape (ANTLR warning 184).
IMPLIES : '⟹' | '\\implies' ; IMPLIES : '⟹' | '\\implies' ;
OR : '' | '\\or' | '\\vee' ; OR : '' | '\\or' ;
AND : '∧' | '\\and' | '\\wedge' ; AND : '∧' | '\\and' ;
EQ : '=' ; EQ : '=' ;
NEQ : '≠' | '\\neq' | '\\ne' ; NEQ : '≠' | '\\neq' ;
LT : '<' ; LT : '<' ;
GT : '>' ; GT : '>' ;
LEQ : '≤' | '\\leq' | '\\le' ; LEQ : '≤' | '\\leq' ;
GEQ : '≥' | '\\geq' | '\\ge' ; GEQ : '≥' | '\\geq' ;
APPROX : '≈' | '\\approx' ; APPROX : '≈' | '\\approx' ;
SIM : '' | '\\sim' ; SIM : '' | '\\sim' ;
PLUS : '+' ; PLUS : '+' ;
MINUS : '-' ; MINUS : '-' ;
TIMES : '×' | '\\times' ; TIMES : '×' | '\\times' ;
DIV : '÷' | '\\div' ; DIV : '÷' | '\\div' | '/' ;
AST : '' | '\\ast' ; AST : '' | '\\ast' ;
COMPOSE : '∘' | '\\circ' ; COMPOSE : '∘' | '\\circ' ;
// Unary operators // Unary operators
RAISE : '↯' | '\\raise' ; RAISE : '↯' | '\\raise' ;
TRACE : '✎' | '\\trace' ; TRACE : '✎' | '\\trace' ;
QUERY : '?' | '\\query' ;
BREAK : '⧈' | '\\break' ; BREAK : '⧈' | '\\break' ;
DELAY : '⏲' | '\\delay' ; DELAY : '⏲' | '\\delay' ;
@ -292,13 +330,11 @@ DELAY : '⏲' | '\\delay' ;
// (LAMBDA was fully shadowed by LAMBDA_VAR — warning 184; LAMBDA_VAR is the // (LAMBDA was fully shadowed by LAMBDA_VAR — warning 184; LAMBDA_VAR is the
// single λ token and the lambda parser rule uses it.) // single λ token and the lambda parser rule uses it.)
FORALL : '∀' | '\\forall' ; FORALL : '∀' | '\\forall' ;
EXISTS : '∃' | '\\exists' ;
DEFINITION : '≜' | '\\coloneq' ; DEFINITION : '≜' | '\\coloneq' ;
HANDLE : '↴' | '\\handle' ; HANDLE : '↴' | '\\handle' ;
ALLOC : '⊕' | '\\oplus' ; ALLOC : '⊕' | '\\oplus' ;
RELEASE : '⊖' | '\\ominus' ; RELEASE : '⊖' | '\\ominus' ;
MODULE : '𝓜' | '\\module' ; MODULE : '𝓜' | '\\module' ;
IMPORT : '⇐' | '\\Leftarrow' ;
EXPORT : '⇒' | '\\Rightarrow' ; EXPORT : '⇒' | '\\Rightarrow' ;
SEND : '⇀' | '\\send' ; SEND : '⇀' | '\\send' ;
RECEIVE : '↽' | '\\receive' ; RECEIVE : '↽' | '\\receive' ;
@ -328,15 +364,15 @@ LRCORNER : '⌟' | '\\lrcorner' ;
// Other symbols // Other symbols
COLON : ':' ; COLON : ':' ;
COMMA : ',' ; COMMA : ',' ;
DOT : '.' ;
UNDERSCORE : '_' ; UNDERSCORE : '_' ;
BAR : '|' ; BAR : '|' ;
ARROW : '→' | '\\rightarrow' | '\\to' ;
MIDDOT : '‧' ; MIDDOT : '‧' ;
// Identifiers // Identifiers. A leading underscore is NOT allowed: subscripts such as
// ⌉_db_lock and ↽_socket must lex as UNDERSCORE + IDENTIFIER, not as a
// single identifier "_db_lock".
IDENTIFIER IDENTIFIER
: [a-zA-Z_][a-zA-Z0-9_]* : [a-zA-Z][a-zA-Z0-9_]*
; ;
// Numbers // Numbers
@ -390,4 +426,4 @@ MULTILINE_COMMENT
// Whitespace // Whitespace
WS WS
: [ \t\r\n]+ -> skip : [ \t\r\n]+ -> skip
; ;

View file

@ -52,6 +52,7 @@ public class LexerTest extends MPLTestBase {
assertTokenTypes("-", MPLLexer.MINUS); assertTokenTypes("-", MPLLexer.MINUS);
assertTokenTypes("×", MPLLexer.TIMES); assertTokenTypes("×", MPLLexer.TIMES);
assertTokenTypes("÷", MPLLexer.DIV); assertTokenTypes("÷", MPLLexer.DIV);
assertTokenTypes("/", MPLLexer.DIV); // ASCII alias, e.g. π/4
assertTokenTypes("", MPLLexer.AST); assertTokenTypes("", MPLLexer.AST);
assertTokenTypes("", MPLLexer.COMPOSE); assertTokenTypes("", MPLLexer.COMPOSE);
@ -74,6 +75,21 @@ public class LexerTest extends MPLTestBase {
assertTokenTypes("", MPLLexer.LEFTARROW); assertTokenTypes("", MPLLexer.LEFTARROW);
assertTokenTypes("", MPLLexer.DEFINITION); assertTokenTypes("", MPLLexer.DEFINITION);
} }
@Test
public void testEscapeDisambiguation() throws IOException {
// \implies is (IMPLIES); \Rightarrow is (EXPORT). Formerly both
// mapped to IMPLIES, fully shadowing EXPORT's escape (warning 184).
assertTokenTypes("\\implies", MPLLexer.IMPLIES);
assertTokenTypes("\\Rightarrow", MPLLexer.EXPORT);
assertTokenTypes("", MPLLexer.EXPORT);
}
@Test
public void testModuleAccess() throws IOException {
assertTokenTypes("Mathematics‧sin",
MPLLexer.IDENTIFIER, MPLLexer.MIDDOT, MPLLexer.IDENTIFIER);
}
@Test @Test
public void testEffectOperators() throws IOException { public void testEffectOperators() throws IOException {
@ -123,9 +139,23 @@ public class LexerTest extends MPLTestBase {
@Test @Test
public void testIdentifiers() throws IOException { public void testIdentifiers() throws IOException {
assertTokenTypes("foo", MPLLexer.IDENTIFIER); assertTokenTypes("foo", MPLLexer.IDENTIFIER);
assertTokenTypes("_bar", MPLLexer.IDENTIFIER);
assertTokenTypes("baz123", MPLLexer.IDENTIFIER); assertTokenTypes("baz123", MPLLexer.IDENTIFIER);
assertTokenTypes("camelCase", MPLLexer.IDENTIFIER); assertTokenTypes("camelCase", MPLLexer.IDENTIFIER);
assertTokenTypes("db_lock", MPLLexer.IDENTIFIER);
}
@Test
public void testSubscripts() throws IOException {
// Identifiers must not start with an underscore, so that subscripted
// constructs lex as UNDERSCORE + IDENTIFIER instead of one identifier.
// (Previously "⌉_db_lock" lexed as RCEIL + IDENTIFIER "_db_lock".)
assertTokenTypes("_bar", MPLLexer.UNDERSCORE, MPLLexer.IDENTIFIER);
assertTokenTypes("⌉_db_lock",
MPLLexer.RCEIL, MPLLexer.UNDERSCORE, MPLLexer.IDENTIFIER);
assertTokenTypes("↽_socket",
MPLLexer.RECEIVE, MPLLexer.UNDERSCORE, MPLLexer.IDENTIFIER);
assertTokenTypes("⇀_socket",
MPLLexer.SEND, MPLLexer.UNDERSCORE, MPLLexer.IDENTIFIER);
} }
@Test @Test
@ -140,6 +170,8 @@ public class LexerTest extends MPLTestBase {
public void testPathLiterals() throws IOException { public void testPathLiterals() throws IOException {
assertTokenTypes("🖫 \"path\"", MPLLexer.PATH, MPLLexer.STRING); assertTokenTypes("🖫 \"path\"", MPLLexer.PATH, MPLLexer.STRING);
assertTokenTypes("\\path \"path\"", MPLLexer.PATH, MPLLexer.STRING); assertTokenTypes("\\path \"path\"", MPLLexer.PATH, MPLLexer.STRING);
// Identifier form, e.g. readFile(🖫path)
assertTokenTypes("🖫path", MPLLexer.PATH, MPLLexer.IDENTIFIER);
} }
@Test @Test

View file

@ -34,23 +34,29 @@ public class MPLTestBase {
} }
private ParseTree parseWithErrors(String input, boolean collectErrors, List<String> errorList) throws IOException { private ParseTree parseWithErrors(String input, boolean collectErrors, List<String> errorList) throws IOException {
ANTLRInputStream inputStream = new ANTLRInputStream(input); // CharStreams works in Unicode code points; the deprecated
// ANTLRInputStream fed UTF-16 units and broke on supplementary-plane
// glyphs such as 𝔹, 𝓜 and 🖫.
CharStream inputStream = CharStreams.fromString(input);
MPLLexer lexer = new MPLLexer(inputStream); MPLLexer lexer = new MPLLexer(inputStream);
CommonTokenStream tokens = new CommonTokenStream(lexer); CommonTokenStream tokens = new CommonTokenStream(lexer);
MPLParser parser = new MPLParser(tokens); MPLParser parser = new MPLParser(tokens);
if (collectErrors && errorList != null) { if (collectErrors && errorList != null) {
parser.removeErrorListeners(); BaseErrorListener listener = new BaseErrorListener() {
parser.addErrorListener(new BaseErrorListener() {
@Override @Override
public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol, public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol,
int line, int charPositionInLine, String msg, int line, int charPositionInLine, String msg,
RecognitionException e) { RecognitionException e) {
errorList.add(String.format("line %d:%d %s", line, charPositionInLine, msg)); errorList.add(String.format("line %d:%d %s", line, charPositionInLine, msg));
} }
}); };
lexer.removeErrorListeners();
lexer.addErrorListener(listener);
parser.removeErrorListeners();
parser.addErrorListener(listener);
} }
return parser.program(); return parser.program();
} }
@ -84,7 +90,7 @@ public class MPLTestBase {
* Get all tokens from input * Get all tokens from input
*/ */
protected List<Token> tokenize(String input) throws IOException { protected List<Token> tokenize(String input) throws IOException {
ANTLRInputStream inputStream = new ANTLRInputStream(input); CharStream inputStream = CharStreams.fromString(input);
MPLLexer lexer = new MPLLexer(inputStream); MPLLexer lexer = new MPLLexer(inputStream);
List<Token> tokens = new ArrayList<>(); List<Token> tokens = new ArrayList<>();

View file

@ -59,15 +59,14 @@ public class ParseExamples {
} }
private static void parseFile(Path file) throws IOException { private static void parseFile(Path file) throws IOException {
String content = Files.readString(file); // CharStreams works in Unicode code points; the deprecated
// ANTLRInputStream broke on supplementary-plane glyphs (𝓜, 🖫).
ANTLRInputStream input = new ANTLRInputStream(content); CharStream input = CharStreams.fromPath(file);
MPLLexer lexer = new MPLLexer(input); MPLLexer lexer = new MPLLexer(input);
CommonTokenStream tokens = new CommonTokenStream(lexer); CommonTokenStream tokens = new CommonTokenStream(lexer);
MPLParser parser = new MPLParser(tokens); MPLParser parser = new MPLParser(tokens);
// Collect errors // Fail on both lexer and parser errors
parser.removeErrorListeners();
var errorListener = new BaseErrorListener() { var errorListener = new BaseErrorListener() {
@Override @Override
public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol, public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol,
@ -76,8 +75,11 @@ public class ParseExamples {
throw new RuntimeException(String.format("line %d:%d %s", line, charPositionInLine, msg)); throw new RuntimeException(String.format("line %d:%d %s", line, charPositionInLine, msg));
} }
}; };
lexer.removeErrorListeners();
lexer.addErrorListener(errorListener);
parser.removeErrorListeners();
parser.addErrorListener(errorListener); parser.addErrorListener(errorListener);
// Parse // Parse
parser.program(); parser.program();
} }

View file

@ -53,12 +53,15 @@ public class ParserTest extends MPLTestBase {
assertParses("(x ← y);"); assertParses("(x ← y);");
} }
// Function calls are f(a, b) only juxtaposition (f x) was removed.
@Test @Test
public void testFunctionApplication() throws IOException { public void testFunctionCalls() throws IOException {
assertParses("f x;"); assertParses("f(x);");
assertParses("g a b c;"); assertParses("g(a, b, c);");
assertParses("sin π;"); assertParses("sin(π);");
assertParses("(f x) y;"); assertParses("f(x)(y);");
assertParses("f();"); // nullary call
assertParses("mergeResults();");
} }
@Test @Test
@ -66,14 +69,15 @@ public class ParserTest extends MPLTestBase {
assertParses("λx: x + 1;"); assertParses("λx: x + 1;");
assertParses("λx∈: x × 2;"); assertParses("λx∈: x × 2;");
assertParses("λa: λb: a + b;"); assertParses("λa: λb: a + b;");
assertParses("(λx: x × x) 5;"); assertParses("λa, b: a + b;"); // multi-parameter pattern
assertParses("(λx: x × x)(5);"); // was (λx: x × x) 5 juxtaposition removed
} }
@Test @Test
public void testForall() throws IOException { public void testForall() throws IOException {
assertParses("∀x∈S: P x;"); assertParses("∀x∈S: P(x);"); // was P x juxtaposition removed
assertParses("∀n∈: n ≥ 0;"); assertParses("∀n∈: n ≥ 0;");
assertParses("∀x∈A: ∀y∈B: f x y;"); assertParses("∀x∈A: ∀y∈B: f(x, y);"); // was f x y juxtaposition removed
} }
@Test @Test
@ -81,19 +85,31 @@ public class ParserTest extends MPLTestBase {
assertParses("f ≜ λx: x + 1;"); assertParses("f ≜ λx: x + 1;");
assertParses("pi ≜ 3.14159;"); assertParses("pi ≜ 3.14159;");
assertParses("id ≜ λx: x;"); assertParses("id ≜ λx: x;");
assertParses("π ≜ 3.14159;"); // greek letter on the left
} }
@Test @Test
public void testBlocks() throws IOException { public void testBlocks() throws IOException {
assertParses("{ x ← 1; y ← 2; x + y }"); assertParses("{ x ← 1; y ← 2; x + y }");
assertParses("{ a ← b; { c ← d; } e }"); // Was "{ a ← b; { c ← d; } e }": the inner block juxtaposed with e
// relied on juxtaposition application, which was removed.
assertParses("{ a ← b; { c ← d; }; e }");
assertParses("{ }"); assertParses("{ }");
assertParses("{ x }"); // singleton braces are a block
} }
@Test @Test
public void testConditionals() throws IOException { public void testConditionals() throws IOException {
assertParses("x > 0 ⟹ x | -x;"); assertParses("x > 0 ⟹ x | -x;");
assertParses("(n = 0 ⟹ 1) | (n × fact (n-1));"); assertParses("(n = 0 ⟹ 1) | (n × fact(n-1));");
assertParses("(n≤1 ⟹ 1) | (n×factorial(n-1));");
}
@Test
public void testUnaryMinus() throws IOException {
assertParses("-x;");
assertParses("a - -b;");
assertParses("f(-1);");
} }
@Test @Test
@ -129,26 +145,52 @@ public class ParserTest extends MPLTestBase {
assertParses("\"error\";"); assertParses("\"error\";");
assertParses("\"log message\";"); assertParses("\"log message\";");
assertParses("⏲ 100;"); assertParses("⏲ 100;");
assertParses("x ↴ {↯e ⇒ handle e};"); // Canonical handler clause: pattern expr (was e handle e)
assertParses("x ↴ {↯e ⟹ handle(e)};");
assertParses("x ↴ {↯\"Invalid user\" ⟹ ⊥};");
// Multiple clauses are semicolon-separated
assertParses("x ↴ {↯\"overflow\" ⟹ 0; ↯e ⟹ ↯e};");
}
@Test
public void testResources() throws IOException {
assertParses("conn ← database ⊕;");
assertParses("conn ⊖;");
assertParses("socket ← bind(port) ⊕;");
}
@Test
public void testChannels() throws IOException {
assertParses("data ← ↽_socket request;");
assertParses("⇀_socket response;");
}
@Test
public void testModuleAccess() throws IOException {
assertParses("Mathematics‧sin(angle);");
assertParses("A‧B‧f(x);");
} }
@Test @Test
public void testParallel() throws IOException { public void testParallel() throws IOException {
assertParses("a ‖ b;"); assertParses("a ‖ b;");
assertParses("task1 ‖ task2 ‖ task3;"); assertParses("task1 ‖ task2 ‖ task3;");
assertParses("(f x) ‖ (g y);"); assertParses("f(x) ‖ g(y);"); // was (f x) (g y) juxtaposition removed
} }
@Test @Test
public void testAtomic() throws IOException { public void testAtomic() throws IOException {
assertParses("⌈x ← x + 1⌉;"); assertParses("⌈x ← x + 1⌉;");
assertParses("⌈critical section⌉_lock;"); // Was "⌈critical section⌉_lock" juxtaposition removed
assertParses("⌈criticalSection()⌉_lock;");
assertParses("⌈a ← 1; b ← 2⌉_db_lock;");
} }
@Test @Test
public void testRAII() throws IOException { public void testRAII() throws IOException {
assertParses(" r ← resource ⊕; use r ;"); // Was "use r" / "open \"file\"" / "read f" juxtaposition removed
assertParses(" f ← open \"file\"; read f ;"); assertParses(" r ← resource ⊕; use(r) ;");
assertParses(" f ← open(\"file\"); read(f) ;");
} }
@Test @Test
@ -167,6 +209,7 @@ public class ParserTest extends MPLTestBase {
public void testPaths() throws IOException { public void testPaths() throws IOException {
assertParses("🖫\"file.txt\";"); assertParses("🖫\"file.txt\";");
assertParses("\\path\"directory/file\";"); assertParses("\\path\"directory/file\";");
assertParses("readFile(🖫path);"); // identifier form
} }
@Test @Test
@ -174,8 +217,8 @@ public class ParserTest extends MPLTestBase {
// Factorial // Factorial
assertParses("factorial ≜ λn∈: (n≤1 ⟹ 1) | (n×factorial(n-1));"); assertParses("factorial ≜ λn∈: (n≤1 ⟹ 1) | (n×factorial(n-1));");
// File processing // File processing (canonical handler clause is pattern expr)
assertParses("processFile ≜ λpath: { data ← readFile(🖫path); result ← transform(data); writeFile(result, 🖫\"output.txt\"); ⟨\"success\"|\"failed\"⟩ } ↴ {↯e ⟨⊥|e⟩};"); assertParses("processFile ≜ λpath: { data ← readFile(🖫path); result ← transform(data); writeFile(result, 🖫\"output.txt\"); ⟨\"success\"|\"failed\"⟩ } ↴ {↯e ⟨⊥|e⟩};");
// Network server // Network server
assertParses("server ≜ λport: socket ← bind(port) ⊕; ∀request∈acceptLoop(socket): ( data ← ↽_socket request; response ← processRequest(data); ⇀_socket response ) ‖ handleNext() ;"); assertParses("server ≜ λport: socket ← bind(port) ⊕; ∀request∈acceptLoop(socket): ( data ← ↽_socket request; response ← processRequest(data); ⇀_socket response ) ‖ handleNext() ;");
@ -197,6 +240,13 @@ public class ParserTest extends MPLTestBase {
// Invalid lambda syntax // Invalid lambda syntax
assertDoesNotParse("λ: x;"); assertDoesNotParse("λ: x;");
assertDoesNotParse("λx y: x + y;"); assertDoesNotParse("λx y: x + y;");
// Juxtaposition application was removed calls need parentheses
assertDoesNotParse("f x;");
assertDoesNotParse("g a b c;");
// The C-style ternary is not MPL use (cond a) | b
assertDoesNotParse("cond ? a : b;");
} }
@Test @Test