From d44f8943273140b12fe59d0c4ae548089609ffc9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 16:39:23 +0000 Subject: [PATCH 1/2] feat(grammar): one normative grammar, with a conformance test (E7) spec/ephapax-v2-grammar.ebnf (150 productions) and ephapax.pest (125 rules) had only 68 names in common, and no test compared them. Owner decision 2026-11-10: the parser grammar is the source. The specification file now has 2 parts. - Part 1 is the parser grammar. A test of ephapax-parser (`grammar_conformance`) makes it from ephapax.pest, with the comments of that file, and fails when the 2 files are not the same grammar. `UPDATE_GRAMMAR=1 cargo test -p ephapax-parser grammar_conformance` writes it again. - Part 2 keeps each of the 82 design productions that are not rules of the parser, as the design wrote them. Each one has a mark: `[ALIAS rule]` (25: the parser has the construct as `rule`) or `[UNIMPLEMENTED]` (57) with a fixture. A "DESIGN FORM" comment keeps the design form of a production that part 1 has in a smaller form. The specification does not shrink. The test proves each production: - each rule of the parser is in the parse tree of a fixture in tests/v2-grammar/productions (5 rules can not be in a tree; the test names them and the reason); - the 2 parsers refuse each fixture in tests/v2-grammar/unimplemented; - each alias names a rule of the parser; - rules + aliases + refused = all productions: 0 unaccounted for. Import and extern syntax: part 1 has the forms of the parser (`import a/b(x, y)`, `extern "abi" { ... }`); the design form `import X from "f"` is in part 2 with the mark UNIMPLEMENTED. Not in this change: an unimplemented production is refused with a syntax error, not with an error that names the production. pest_meta is a dev-dependency of ephapax-parser. It was in the lock file already, as a dependency of pest_derive. Tests: 614 all-target. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- Cargo.lock | 1 + EXPLAINME.adoc | 10 +- TEST-NEEDS.adoc | 6 +- spec/ephapax-v2-grammar.ebnf | 1104 +++++++++++------ src/ephapax-parser/Cargo.toml | 3 + src/ephapax-parser/src/grammar_conformance.rs | 368 ++++++ src/ephapax-parser/src/lib.rs | 2 + tests/v2-grammar/productions/declarations.eph | 37 + tests/v2-grammar/productions/expressions.eph | 72 ++ .../unimplemented/annotation_args.eph | 7 + .../unimplemented/borrow_pattern.eph | 6 + tests/v2-grammar/unimplemented/capability.eph | 6 + .../unimplemented/capability_annotation.eph | 7 + tests/v2-grammar/unimplemented/comptime.eph | 9 + tests/v2-grammar/unimplemented/concat.eph | 6 + tests/v2-grammar/unimplemented/contract.eph | 9 + tests/v2-grammar/unimplemented/deref.eph | 6 + tests/v2-grammar/unimplemented/effect.eph | 8 + tests/v2-grammar/unimplemented/effect_row.eph | 6 + tests/v2-grammar/unimplemented/effect_ty.eph | 6 + tests/v2-grammar/unimplemented/finally.eph | 6 + .../v2-grammar/unimplemented/handle_mode.eph | 6 + .../v2-grammar/unimplemented/handler_decl.eph | 8 + .../v2-grammar/unimplemented/handler_ref.eph | 6 + tests/v2-grammar/unimplemented/impl.eph | 8 + .../v2-grammar/unimplemented/import_from.eph | 6 + tests/v2-grammar/unimplemented/prod_ty.eph | 6 + tests/v2-grammar/unimplemented/reexport.eph | 6 + .../unimplemented/resume_after_params.eph | 6 + tests/v2-grammar/unimplemented/splice.eph | 6 + tests/v2-grammar/unimplemented/trait.eph | 8 + .../unimplemented/tuple_pattern.eph | 6 + tests/v2-grammar/unimplemented/type_desc.eph | 6 + .../unimplemented/type_param_bound.eph | 6 + tests/v2-grammar/unimplemented/where.eph | 6 + 35 files changed, 1361 insertions(+), 414 deletions(-) create mode 100644 src/ephapax-parser/src/grammar_conformance.rs create mode 100644 tests/v2-grammar/productions/declarations.eph create mode 100644 tests/v2-grammar/productions/expressions.eph create mode 100644 tests/v2-grammar/unimplemented/annotation_args.eph create mode 100644 tests/v2-grammar/unimplemented/borrow_pattern.eph create mode 100644 tests/v2-grammar/unimplemented/capability.eph create mode 100644 tests/v2-grammar/unimplemented/capability_annotation.eph create mode 100644 tests/v2-grammar/unimplemented/comptime.eph create mode 100644 tests/v2-grammar/unimplemented/concat.eph create mode 100644 tests/v2-grammar/unimplemented/contract.eph create mode 100644 tests/v2-grammar/unimplemented/deref.eph create mode 100644 tests/v2-grammar/unimplemented/effect.eph create mode 100644 tests/v2-grammar/unimplemented/effect_row.eph create mode 100644 tests/v2-grammar/unimplemented/effect_ty.eph create mode 100644 tests/v2-grammar/unimplemented/finally.eph create mode 100644 tests/v2-grammar/unimplemented/handle_mode.eph create mode 100644 tests/v2-grammar/unimplemented/handler_decl.eph create mode 100644 tests/v2-grammar/unimplemented/handler_ref.eph create mode 100644 tests/v2-grammar/unimplemented/impl.eph create mode 100644 tests/v2-grammar/unimplemented/import_from.eph create mode 100644 tests/v2-grammar/unimplemented/prod_ty.eph create mode 100644 tests/v2-grammar/unimplemented/reexport.eph create mode 100644 tests/v2-grammar/unimplemented/resume_after_params.eph create mode 100644 tests/v2-grammar/unimplemented/splice.eph create mode 100644 tests/v2-grammar/unimplemented/trait.eph create mode 100644 tests/v2-grammar/unimplemented/tuple_pattern.eph create mode 100644 tests/v2-grammar/unimplemented/type_desc.eph create mode 100644 tests/v2-grammar/unimplemented/type_param_bound.eph create mode 100644 tests/v2-grammar/unimplemented/where.eph diff --git a/Cargo.lock b/Cargo.lock index 97b1706f..7a9d1e3f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -909,6 +909,7 @@ dependencies = [ "ephapax-typing", "pest", "pest_derive", + "pest_meta", "smol_str", "thiserror 2.0.18", ] diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 184e5872..8a5eaa55 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -574,9 +574,13 @@ the per-crate breakdown). Key test categories: == Design Documents -* `spec/ephapax-v2-grammar.ebnf` — complete v2 grammar (modules, - generics, effects, traits, comptime, contracts) — work in flight - on `feat/v2-grammar-*` branches +* `spec/ephapax-v2-grammar.ebnf` - the v2 grammar in 2 parts. Part 1 + is the parser grammar: a test of `ephapax-parser` + (`grammar_conformance`) makes it from `ephapax.pest`, so the 2 files + are one grammar. Part 2 keeps the v2 design productions that the + parser does not have (traits, effect declarations, comptime, + contracts), each with the mark `[ALIAS rule]` or `[UNIMPLEMENTED]`; + the parser refuses the fixture of each `[UNIMPLEMENTED]` production * `docs/specs/DESIGN-DECISIONS.adoc` — 17 ADRs with rationale * `docs/specs/LANGUAGE-COMPARISON.adoc` — comparison against 10 languages * `docs/vision/EPHAPAX-VISION.adoc` — design rationale, why dyadic + diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index b5fe471d..0a053e12 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *611 tests* (`+cargo test --workspace --all-targets+`); +* Total: *614 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 611 +* Documented all-target tests: 614 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 611 pass, 0 fail +* [x] cargo test –workspace –all-targets — 614 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/spec/ephapax-v2-grammar.ebnf b/spec/ephapax-v2-grammar.ebnf index e8994a86..e66e79b2 100644 --- a/spec/ephapax-v2-grammar.ebnf +++ b/spec/ephapax-v2-grammar.ebnf @@ -5,103 +5,553 @@ * Ephapax v2 Grammar Specification * ================================ * - * Complete grammar covering: modules, generics, comptime meta plane, - * traits, algebraic effects, contracts, FFI capabilities, visibility, - * annotations, iterators, and pattern matching. + * This file and src/ephapax-parser/src/ephapax.pest are ONE normative + * grammar (v2 plan rung E7; owner decision 2026-11-10: the parser + * grammar is the source). * * Architecture: - * SURFACE GRAMMAR (this file) → desugar → CORE CALCULUS (existing) + * SURFACE GRAMMAR (this file) -> desugar -> CORE CALCULUS * * The core calculus (binary sums, case, inl/inr, let/let!, regions) * remains unchanged. Everything here desugars into it. * - * Two planes: - * DATA PLANE — runtime, linear/affine, regions, effects - * META PLANE — compile-time, total, pure, unrestricted + * The file has 2 parts. + * + * PART 1: THE PARSER GRAMMAR. It says what the parser accepts. A test + * makes it from ephapax.pest, and fails when the 2 files are not the + * same grammar. Do not edit part 1 by hand. After a change of + * ephapax.pest, run: + * + * UPDATE_GRAMMAR=1 cargo test -p ephapax-parser grammar_conformance + * + * Each rule is in the parse tree of a fixture in + * tests/v2-grammar/productions. + * + * PART 2: THE V2 DESIGN, NOT IN THE PARSER BY THAT NAME. These are the + * productions of the v2 design grammar that are not rules of the + * parser: traits, effect and handler declarations, the comptime meta + * plane, contracts, capabilities, and some other forms. Each one is as + * the design wrote it, and each one has a mark on the line before it: + * + * [ALIAS rule] The parser has the construct as `rule` of part 1. + * Part 1 is the current form. + * [UNIMPLEMENTED] The parser does not have it. The parser refuses + * the fixture that the mark names. + * + * A "DESIGN FORM" comment keeps the design form of a production that + * part 1 has in a smaller form. + * + * The specification does not shrink: a production leaves part 2 only + * when the parser has it. Which form wins, where the design and the + * parser write one construct in 2 ways, is an owner decision for each + * construct. + * + * The same test counts the productions: each one is a rule of the parser, + * an alias, or a refused production. 0 productions are unaccounted for. + * + * Notation of part 1 (ISO EBNF, with 2 additions for a PEG): + * a , b a, then b a | b a, or else b (the first match) + * [ a ] a or nothing { a } a, 0 or more times + * { a }- a, 1 or more times + * &( a ) a follows here (lookahead, takes no input) + * !( a ) a does not follow here (lookahead, takes no input) + * ? ... ? a character range, or a character with no printed form + * Names in upper case with no production are from pest: + * ASCII_ALPHA, ASCII_ALPHA_UPPER, ASCII_ALPHANUMERIC, ASCII_DIGIT, ANY + * (one character), SOI and EOI (start and end of the input). + * White space and comments (WHITESPACE, COMMENT) can stand between 2 + * parts of a production, but not in an atomic production. + * + * Two planes of the design: + * DATA PLANE - runtime, linear/affine, regions, effects + * META PLANE - compile-time, total, pure, unrestricted * * The meta plane (comptime) can observe types and generate code. * It cannot reference runtime values or violate linearity. * Harvard separation: meta plane output is validated by the type checker. - * - * Status: ACTIVE — the v2 surface grammar, landing in phases. - * This is the second-draft grammar. The v1 surface (parsed straight - * into the core, no desugaring layer) worked for the core calculus - * but could not grow into modules / generics / effects / comptime; - * v2 adds the surface -> desugar -> core layer that v1 lacked. See - * ../V1-TO-V2.adoc for the full v1 -> v2 story. - * - * The specification below is complete. Implementation proceeds in - * phases, each gated by its own CLI test - * (src/ephapax-cli/tests/v2_grammar_phase_*.rs); landed phases pass. - * "Draft" here means the surface is still growing toward full - * coverage, NOT that it is abandoned or wrong. + * See ../V1-TO-V2.adoc for the v1 -> v2 story. *) +(* ################################################################ *) +(* PART 1: THE PARSER GRAMMAR *) +(* ################################################################ *) + +(* BEGIN GENERATED: the parser grammar, from ephapax.pest. Do not edit. *) + + +(* Ephapax Grammar - PEG Parser *) + +(* Top-level rules *) +module = SOI , [ module_decl ] , { import_decl | declaration } , EOI ; +expression_only = SOI , expression , EOI ; + +(* Module Declaration *) + +module_decl = "module" , qualified_name ; + +(* Only the header, for `declared_module_name`. *) +module_header = SOI , module_decl ; + +(* Qualified name: Foo.Bar.Baz OR Foo/Bar/Baz (slash- and dot-segments both *) +(* allowed and treated as equivalent at the AST level - see canonicalisation *) +(* in `parse_module` / `parse_surface_module`). Slash-paths matter for the *) +(* `hypatia/ui/bridge` style used by downstream consumers; dot-paths are *) +(* historical. *) +qualified_name = ( ASCII_ALPHA | "_" ) , { ASCII_ALPHANUMERIC | "_" | "." | "/" } ; (* atomic: no white space between the parts *) + +(* Imports *) + +import_decl = "import" , qualified_name , [ "(" , identifier , { "," , identifier } , ")" ] ; + +(* Declarations *) + +declaration = { annotation } , ( extern_block | data_decl | fn_decl | type_decl | const_decl ) ; + +(* `@identifier` decorators attached to top-level declarations. Currently *) +(* parser-only - annotations are parsed and stored on the surface AST so *) +(* they survive round-tripping, but the typechecker and codegen ignore *) +(* them. They exist so that downstream tools (hypatia's `@tail_recursive`, *) +(* future `@inline`, `@no_mangle`, etc.) can hang metadata off a decl *) +(* without breaking the parser today. *) +annotation = "@" , identifier ; + +(* Extern Blocks *) +(* `extern "abi" { items... }` declares foreign types and function *) +(* signatures. Items have no body; codegen lowers fn items to host *) +(* `import` directives and treats type items as opaque externs. *) +(* Example: *) +(* extern "gossamer" { *) +(* type Window *) +(* fn window_open(title: String, body: String): Window *) +(* } *) + +extern_block = "extern" , string , "{" , { extern_item } , "}" ; +extern_item = extern_type_item | extern_fn_item ; +extern_type_item = "type" , identifier ; +extern_fn_item = "fn" , identifier , "(" , [ param_list ] , ")" , ( ":" | "->" ) , ty ; + +(* Top-level constant binding: let NAME = expr *) +const_decl = "let" , identifier , [ ":" , ty ] , "=" , expression ; + +(* Optional "pub" prefix for visibility *) +visibility = "pub" ; + +(* Optional generic type parameters: , *) +fn_type_params = "<" , identifier , { "," , identifier } , ">" ; + +fn_decl = [ visibility ] , "fn" , identifier , [ fn_type_params ] , "(" , [ param_list ] , ")" , ( ":" | "->" ) , ty , "=" , expression ; + +param_list = param , { "," , param } ; + +param = identifier , ":" , ty ; + +type_decl = [ visibility ] , [ linearity ] , "type" , identifier , "=" , ( named_record_type_def | record_type_def | sum_type_def | ty ) ; + +(* Named record: TypeName = ConstructorName { field: Type, ... } *) +named_record_type_def = constructor_name , "{" , record_field , { "," , record_field } , [ "," ] , "}" ; + +linearity = "linear" | "affine" ; + +(* Data type declaration: data Option(a) = None | Some(a) *) +(* Optional `pub` prefix makes the type + its constructors importable. *) +data_decl = [ visibility ] , "data" , constructor_name , [ type_params ] , "=" , [ "|" ] , data_variant , { "|" , data_variant } ; + +type_params = "(" , identifier , { "," , identifier } , ")" ; + +data_variant = constructor_name , [ "(" , [ ty_list ] , ")" ] ; +ty_list = ty , { "," , ty } ; + +(* Constructor names start with uppercase *) +constructor_name = ASCII_ALPHA_UPPER , { ASCII_ALPHANUMERIC | "_" } ; (* atomic: no white space between the parts *) + +sum_type_def = [ "|" ] , sum_variant , { "|" , sum_variant } ; +sum_variant = identifier , [ "(" , ty , ")" ] ; + +record_type_def = "{" , record_field , { "," , record_field } , [ "," ] , "}" ; +record_field = identifier , ":" , ty ; + +(* Types *) + +ty = sum_ty , [ "->" , ty ] ; + +sum_ty = type_atom , { "+" , type_atom } ; + +type_atom = base_ty + | string_ty + | borrow_ty + | list_ty + | product_ty + | record_ty + | named_ty + | type_var + ; + +(* Type variables are single lowercase or uppercase identifiers that are NOT *) +(* constructor names with arguments. The named_ty rule handles constructors. *) +(* For single uppercase letters like T, A, B - the parser tries named_ty first, *) +(* which matches as a nullary constructor. The type checker resolves whether *) +(* it's a type variable or a constructor based on scope. *) + +(* Named type application: Option(I32), Result(String@r, Error), Color *) +(* Nullary named types (no parens) are also valid: Color, Unit, etc. *) +named_ty = constructor_name , [ "(" , ty_list , ")" ] ; + +record_ty = "{" , record_field , { "," , record_field } , "}" ; + +base_ty = unit_ty | "Bool" | "I32" | "I64" | "F32" | "F64" ; +unit_ty = "()" ; + +string_ty = "String" , [ "@" , identifier ] ; + +borrow_ty = "&" , [ mut_marker ] , type_atom ; + +mut_marker = "mut" , !( ASCII_ALPHANUMERIC | "_" ) ; (* atomic: no white space between the parts *) + +list_ty = "[" , ty , "]" ; + +product_ty = "(" , ty , { "," , ty }- , ")" ; + +type_var = identifier ; + +(* Expressions *) + +expression = seq_expr ; + +(* Statement sequencing: e1 ; e2 ; e3 (last expression is the result) *) +seq_expr = single_expr , { ";" , single_expr } ; + +single_expr = block_expr + | let_lin_expr + | let_expr + | lambda_expr + | if_expr + | region_expr + | match_expr + | case_expr + | handle_expr + | or_expr + ; + +(* One or more `sequential_let`s followed by a trailing result expression. *) +(* The trailing expression can itself be any `expression` (which folds back *) +(* through `seq_expr` / `single_expr`), so nested block forms and explicit *) +(* `let ... in ...` both compose normally. *) +block_expr = { sequential_let }- , expression ; + +sequential_let = ( "let!" | "let" ) , let_binder , [ ":" , ty ] , "=" , block_rhs ; + +(* A `sequential_let`'s rhs may be any expression form *except* a top-level *) +(* `let`/`let!` - those participate in the block via the next iteration of *) +(* `sequential_let`. *) +block_rhs = lambda_expr + | if_expr + | region_expr + | match_expr + | case_expr + | handle_expr + | or_expr + ; + +(* Pattern matching: match x of | None => 0 | Some(v) => v end *) +match_expr = "match" , expression , "of" , [ "|" ] , match_arm , { "|" , match_arm } , "end" ; + +match_arm = pattern , [ "if" , expression ] , "=>" , expression ; + +pattern = constructor_pattern + | pair_pattern + | wildcard_pattern + | literal_pattern + | var_pattern + ; + +constructor_pattern = constructor_name , [ "(" , [ pattern_list ] , ")" ] ; +pair_pattern = "(" , pattern , "," , pattern , ")" ; +wildcard_pattern = "_" ; +literal_pattern = literal ; +var_pattern = identifier ; + +pattern_list = pattern , { "," , pattern } ; + +let_expr = "let" , let_binder , [ ":" , ty ] , "=" , expression , "in" , expression ; + +let_lin_expr = "let!" , let_binder , [ ":" , ty ] , "=" , expression , "in" , expression ; + +(* Either a single identifier (the common case) or a parenthesised tuple *) +(* of identifiers for destructuring binds: *) +(* let (a, b) = pair() in ... *) +(* let! (ch2, msg_bytes) = ipc_recv(ch) in ... *) +(* Tuple binders desugar to a 1-arm `match scrutinee of | (a, b) => body end` *) +(* at parse time, reusing the existing pair-pattern handling. *) +let_binder = tuple_binder | identifier ; +tuple_binder = "(" , identifier , { "," , identifier }- , ")" ; + +lambda_expr = "fn" , "(" , identifier , ":" , ty , ")" , "->" , expression ; + +if_expr = "if" , expression , "then" , expression , "else" , expression ; + +region_expr = "region" , identifier , ( ":" | "{" ) , expression , [ "}" ] ; + +case_expr = "case" , expression , "of" , "inl" , "(" , identifier , ")" , "->" , expression , "inr" , "(" , identifier , ")" , "->" , expression , "end" ; + +(* Effect handling: handle expr with { return(x) => e | Op(args, resume) => e } end *) +handle_expr = "handle" , expression , "with" , [ "|" ] , handler_clause , { "|" , handler_clause } , "end" ; + +handler_clause = handler_return_clause | handler_op_clause ; + +(* return(x) => expr *) +handler_return_clause = "return" , "(" , identifier , ")" , "=>" , expression ; + +(* Op(param1, param2, resume) => expr *) +(* resume may optionally have a mode: resume(once) or resume(multi) *) +handler_op_clause = identifier , "(" , [ handler_param_list ] , ")" , "=>" , expression ; + +handler_param_list = handler_param , { "," , handler_param } ; +handler_param = resume_param | identifier ; + +resume_param = "resume" , [ "(" , resume_mode , ")" ] ; +resume_mode = "once" | "multi" ; + +(* Binary Operators (by precedence, lowest to highest) *) + +or_expr = and_expr , { "||" , and_expr } ; + +and_expr = eq_expr , { "&&" , eq_expr } ; + +eq_expr = cmp_expr , { eq_op , cmp_expr } ; +eq_op = "==" | "!=" ; + +cmp_expr = add_expr , { cmp_op , add_expr } ; +cmp_op = "<=" | ">=" | "<" | ">" ; + +add_expr = mul_expr , { add_op , mul_expr } ; +add_op = "+" | "-" ; + +mul_expr = unary_expr , { mul_op , unary_expr } ; +mul_op = "*" | "/" | "%" ; + +(* Unary and Postfix Expressions *) + +unary_expr = "!" , unary_expr | "-" , unary_expr | postfix_expr ; + +postfix_expr = atom_expr , { postfix_op } ; + +postfix_op = call_op | type_app_op | index_op | member_op ; + +call_op = "(" , [ call_args ] , ")" ; +call_args = expression , { "," , expression } ; +(* Explicit type arguments of a generic function: `id[I32](3)`. Only *) +(* before a call, and before `index_op`: `xs[i](3)` has the two readings *) +(* when `i` is one name. The desugarer reads that case as an index, unless *) +(* the name is a type parameter of the function it is in. *) +type_app_op = "[" , ty_list , "]" , &( "(" ) ; +index_op = "[" , expression , "]" ; +member_op = "." , ( integer | identifier | constructor_name ) ; + +(* Atomic Expressions *) + +atom_expr = perform_expr + | ffi_expr + | string_method + | inl_expr + | inr_expr + | borrow_expr + | fst_expr + | snd_expr + | drop_expr + | copy_expr + | construct_expr + | record_literal + | list_literal + | paren_or_pair + | literal + | variable + ; + +(* Perform an effect operation: perform Op(args...) *) +perform_expr = "perform" , identifier , [ "(" , [ expr_list ] , ")" ] ; + +(* Named constructor: Some(42), None, Ok(value), or named record: GsaApp { field = val } *) +construct_expr = constructor_name , [ "(" , [ expr_list ] , ")" | "{" , record_field_assign , { "," , record_field_assign } , [ "," ] , "}" ] ; + +(* FFI call: __ffi("symbol_name", arg1, arg2, ...) *) +(* Calls a C ABI function from a linked shared library. *) +ffi_expr = "__ffi" , "(" , string , { "," , expression } , ")" ; + +record_literal = "{" , record_field_assign , { "," , record_field_assign } , [ "," ] , "}" ; +(* Three surface forms, all producing the same AST node: *) +(* 1. `field: ty = value` (typed, explicit assignment) *) +(* 2. `field = value` (untyped, explicit assignment) *) +(* 3. `field: value` (ML/Haskell-style shorthand - value *) +(* expression directly after `:`, no `=`) *) +(* PEG ordering: the `=` forms are tried first; the shorthand fires *) +(* only when no `=` follows the named-ty. *) +record_field_assign = identifier , ":" , ty , "=" , expression + | identifier , "=" , expression + | identifier , ":" , expression + ; + +string_method = "String" , "." , identifier , [ "@" , identifier ] , "(" , [ expr_list ] , ")" ; + +expr_list = expression , { "," , expression } ; + +inl_expr = "inl" , "[" , ty , "]" , "(" , expression , ")" ; +inr_expr = "inr" , "[" , ty , "]" , "(" , expression , ")" ; + +borrow_expr = "&" , [ mut_marker ] , unary_expr ; + +fst_expr = "fst" , "(" , expression , ")" ; +snd_expr = "snd" , "(" , expression , ")" ; +drop_expr = "drop" , "(" , expression , ")" ; +copy_expr = "copy" , "(" , expression , ")" ; + +list_literal = "[" , [ expression , { "," , expression } ] , "]" ; + +paren_or_pair = "(" , [ expression , { "," , expression } ] , ")" ; + +variable = identifier ; + +(* Literals *) + +literal = unit_literal | boolean | float32 | float | integer | string ; + +unit_literal = "()" ; +boolean = "true" | "false" ; + +integer = { ASCII_DIGIT }- ; (* atomic: no white space between the parts *) +float = { ASCII_DIGIT }- , "." , { ASCII_DIGIT }- ; (* atomic: no white space between the parts *) +(* An F32 literal carries the `f32` suffix (`1.5f32`); an unsuffixed float *) +(* literal is F64. *) +float32 = { ASCII_DIGIT }- , "." , { ASCII_DIGIT }- , "f32" ; (* atomic: no white space between the parts *) + +string = '"' , string_inner , '"' ; (* atomic: no white space between the parts *) +string_inner = { escape | !( '"' | "\" ) , ANY } ; (* atomic: no white space between the parts *) +escape = "\" , ( "n" | "r" | "t" | "\" | '"' ) ; (* atomic: no white space between the parts *) + +(* Identifiers and Whitespace *) + +identifier = !( keyword_boundary ) , ( ASCII_ALPHA | "_" ) , { ASCII_ALPHANUMERIC | "_" } ; (* atomic: no white space between the parts *) + +(* Keywords must be followed by a non-identifier character (word boundary) *) +keyword_boundary = ( "let!" | "let" | "in" | "fn" | "if" | "then" | "else" | "region" | "case" | "of" | "inl" | "inr" | "end" | "fst" | "snd" | "drop" | "copy" | "type" | "data" | "match" | "extern" | "true" | "false" | "pub" | "import" | "module" | "linear" | "mut" | "perform" | "handle" | "with" | "return" | "resume" | "once" | "multi" | "Bool" | "I32" | "I64" | "F32" | "F64" | "String" ) , !( ASCII_ALPHANUMERIC | "_" ) ; + +keyword = "let" + | "let!" + | "in" + | "fn" + | "if" + | "then" + | "else" + | "region" + | "case" + | "of" + | "inl" + | "inr" + | "end" + | "fst" + | "snd" + | "drop" + | "copy" + | "type" + | "data" + | "match" + | "extern" + | "true" + | "false" + | "pub" + | "import" + | "module" + | "linear" + | "mut" + | "perform" + | "handle" + | "with" + | "return" + | "resume" + | "once" + | "multi" + | "Bool" + | "I32" + | "I64" + | "F32" + | "F64" + | "String" + ; + +WHITESPACE = " " | ? TAB ? | ? LF ? | ? CR ? ; (* silent: no node in the parse tree *) +COMMENT = "--" , { !( ? LF ? ) , ANY } + | "//" , { !( ? LF ? ) , ANY } + | "/*" , { !( "*/" ) , ANY } , "*/" + ; (* silent: no node in the parse tree *) + +(* END GENERATED *) + + +(* ################################################################ *) +(* PART 2: THE V2 DESIGN, NOT IN THE PARSER BY THAT NAME *) +(* ################################################################ *) + (* ================================================================ *) -(* 1. TOP LEVEL *) +(* 1. TOP LEVEL *) (* ================================================================ *) (* A source file is a module. *) +(* [ALIAS module] the parser takes imports and declarations in any order *) source_file = { module_header } , { import } , { top_decl } ; -module_header = "module" , module_path , [ capability_decl ] ; +(* DESIGN FORM of module_header. The parser rule module_header in part 1 is the current form. + * This form has productions that are not implemented: capability_decl. + * + * module_header = "module" , module_path , [ capability_decl ] ; + *) +(* [ALIAS qualified_name] the parser rule is the current form *) module_path = IDENT , { "." , IDENT } ; + (* ================================================================ *) -(* 2. MODULES AND IMPORTS *) +(* 2. MODULES AND IMPORTS *) (* ================================================================ *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/import_from.eph (the parser has import_decl: `import a/b` and `import a/b(x, y)`) *) import = "import" , import_spec , "from" , STRING ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/import_from.eph *) import_spec = IDENT (* import Foo from "foo" *) | "{" , IDENT , { "," , IDENT } , "}" (* import { a, b } from "foo" *) | "*" , "as" , IDENT (* import * as Foo from "foo" *) ; (* Re-export: make imported names visible to importers of this module *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/reexport.eph *) reexport = "pub" , import ; -(* ================================================================ *) -(* 3. VISIBILITY *) -(* ================================================================ *) - -(* Default: private to module. `pub` makes visible to importers. *) -visibility = [ "pub" ] ; (* ================================================================ *) -(* 4. ANNOTATIONS *) +(* 4. ANNOTATIONS *) (* ================================================================ *) -(* Annotations are compile-time metadata on declarations. *) -(* The comptime meta plane processes them. *) +(* DESIGN FORM of annotation. The parser rule annotation in part 1 is the current form. + * This form has productions that are not implemented: annotation_args. + * + * annotation = "@" , IDENT , [ "(" , annotation_args , ")" ] ; + *) -annotation = "@" , IDENT , [ "(" , annotation_args , ")" ] ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/annotation_args.eph *) annotation_args = annotation_arg , { "," , annotation_arg } ; + +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/annotation_args.eph *) annotation_arg = IDENT | STRING | INTEGER | annotation ; -(* Common annotations: - * @inline — inline this function at call sites - * @noinline — never inline - * @tail_recursive — verify tail recursion (comptime-checked) - * @no_alloc — verify no allocation (comptime-checked) - * @repr(C) — C-compatible memory layout - * @repr(packed) — no padding - * @deprecated(msg) — emit warning on use - * @comptime — execute at compile time - * @reflectable — generate runtime TypeDesc - * @derive(Eq, Show) — generate trait impls via comptime - * @pure — no side effects (comptime-verified) - * @total — always terminates (comptime-verified) - *) (* ================================================================ *) -(* 5. DECLARATIONS *) +(* 5. DECLARATIONS *) (* ================================================================ *) +(* [ALIAS declaration] the parser has no trait, impl, effect, handler or comptime declaration *) top_decl = { annotation } , visibility , decl_body ; +(* [ALIAS declaration] the parser has no trait, impl, effect, handler or comptime declaration *) decl_body = fn_decl | data_decl | type_decl @@ -112,86 +562,86 @@ decl_body = fn_decl | comptime_decl ; -(* --- 5a. Functions --- *) +(* DESIGN FORM of fn_decl. The parser rule fn_decl in part 1 is the current form. + * This form has productions that are not implemented: contract_block, effect_annotation, where_clause. + * + * fn_decl = "fn" , IDENT , [ type_params ] , + * "(" , [ param_list ] , ")" , ":" , ty , + * [ where_clause ] , + * [ contract_block ] , + * [ effect_annotation ] , + * "=" , expr ; + *) -fn_decl = "fn" , IDENT , [ type_params ] , - "(" , [ param_list ] , ")" , ":" , ty , - [ where_clause ] , - [ contract_block ] , - [ effect_annotation ] , - "=" , expr ; +(* DESIGN FORM of type_params. The parser rule type_params in part 1 is the current form. + * This form has productions that are not implemented: type_param. + * + * type_params = "[" , type_param , { "," , type_param } , "]" ; + *) -type_params = "[" , type_param , { "," , type_param } , "]" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/type_param_bound.eph (the parser has type parameters with no bound: fn_type_params, type_params) *) type_param = IDENT , [ ":" , trait_bound ] ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/type_param_bound.eph *) trait_bound = CTOR_IDENT , { "+" , CTOR_IDENT } ; -(* e.g. [a: Eq + Show] means a must implement Eq and Show *) - -param_list = param , { "," , param } ; -param = IDENT , ":" , ty ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/where.eph *) where_clause = "where" , constraint , { "," , constraint } ; -constraint = IDENT , ":" , trait_bound ; -(* where clause allows complex bounds that don't fit in type_params *) - -(* --- 5b. Data types --- *) - -data_decl = "data" , CTOR_IDENT , [ type_params ] , "=" , - [ "|" ] , data_variant , { "|" , data_variant } ; - -data_variant = CTOR_IDENT , [ "(" , ty_list , ")" ] ; - -ty_list = ty , { "," , ty } ; - -(* --- 5c. Type aliases --- *) -type_decl = "type" , IDENT , [ type_params ] , "=" , ty ; - -(* --- 5d. Traits --- *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/where.eph *) +constraint = IDENT , ":" , trait_bound ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/trait.eph *) trait_decl = "trait" , CTOR_IDENT , "(" , type_param , ")" , [ ":" , trait_bound ] , (* supertrait bounds *) "=" , { trait_item } , "end" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/trait.eph *) trait_item = { annotation } , trait_fn_sig ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/trait.eph *) trait_fn_sig = "fn" , IDENT , [ type_params ] , "(" , [ param_list ] , ")" , ":" , ty , [ "=" , expr ] (* default implementation *) ; -(* --- 5e. Trait implementations --- *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/impl.eph *) impl_decl = "impl" , CTOR_IDENT , "(" , ty , ")" , [ where_clause ] , "=" , { impl_item } , "end" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/impl.eph *) impl_item = { annotation } , fn_decl ; -(* --- 5f. Effects --- *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect.eph *) effect_decl = "effect" , CTOR_IDENT , [ type_params ] , "=" , { effect_op } , "end" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect.eph *) effect_op = "fn" , IDENT , [ type_params ] , "(" , [ param_list ] , ")" , ":" , ty ; -(* --- 5g. Effect handlers --- *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/handler_decl.eph *) handler_decl = "handler" , IDENT , [ type_params ] , "for" , CTOR_IDENT , [ type_params ] , [ "with" , "(" , param_list , ")" ] , (* handler-local state *) "=" , { handler_clause } , "end" ; -handler_clause = return_clause - | op_clause - | finally_clause - ; +(* DESIGN FORM of handler_clause. The parser rule handler_clause in part 1 is the current form. + * This form has productions that are not implemented: finally_clause, op_clause. + * + * handler_clause = return_clause + * | op_clause + * | finally_clause + * ; + *) (* What to do when the handled computation returns normally *) +(* [ALIAS handler_return_clause] the parser rule is the current form *) return_clause = "return" , "(" , IDENT , ")" , "=>" , expr ; (* Handler for an effect operation *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/handler_decl.eph (the parser has handler_op_clause, with `resume` in the parameter list) *) op_clause = "|" , IDENT , "(" , [ param_list ] , ")" , [ "," , resume_binding ] , "=>" , expr ; @@ -202,40 +652,45 @@ op_clause = "|" , IDENT , "(" , [ param_list ] , ")" , * the continuation captures linear values) * - multi: multi-shot, type error if linear captures exist * - omitted: compiler infers from captures *) +(* [ALIAS resume_param] the parser rule is the current form *) resume_binding = "resume" , [ "(" , resume_mode , ")" ] ; -resume_mode = "once" | "multi" ; (* Cleanup when continuation is discarded without resuming. * CRITICAL for linear safety: if a handler doesn't call resume, * any linear values captured by the continuation must be consumed. * The finally clause handles this. *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/finally.eph *) finally_clause = "finally" , "=>" , expr ; -(* --- 5h. Comptime declarations (meta plane) --- *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_decl = "@comptime" , "{" , { comptime_item } , "}" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_item = comptime_fn | comptime_let ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_fn = "fn" , IDENT , "(" , [ comptime_param_list ] , ")" , ":" , comptime_ty , "=" , comptime_expr ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_param_list = comptime_param , { "," , comptime_param } ; + +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_param = IDENT , ":" , comptime_ty ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_let = "let" , IDENT , "=" , comptime_expr ; + (* ================================================================ *) -(* 6. CONTRACTS *) +(* 6. CONTRACTS *) (* ================================================================ *) -(* Contracts are pre/post conditions and invariants. *) -(* Static contracts are verified at comptime. *) -(* Dynamic contracts emit runtime checks (erasable in release). *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/contract.eph *) contract_block = { contract_clause } ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/contract.eph *) contract_clause = "requires" , expr (* precondition *) | "ensures" , result_expr (* postcondition *) | "invariant" , expr (* maintained through body *) @@ -246,44 +701,56 @@ contract_clause = "requires" , expr (* precondition *) * the result as an unrestricted snapshot. This is needed because * linear values are consumed by the body and cannot be referenced * in ensures directly. old() implicitly borrows. *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/contract.eph *) result_expr = expr ; + +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/contract.eph *) old_expr = "old" , "(" , expr , ")" ; + (* ================================================================ *) -(* 7. FFI CAPABILITIES *) +(* 7. FFI CAPABILITIES *) (* ================================================================ *) -(* Module-level capability declaration restricts what FFI can do. *) -(* Comptime-verified: if a module declares capabilities, every *) -(* __ffi call must fit within them. *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/capability.eph *) capability_decl = "capabilities" , ":" , "[" , capability , { "," , capability } , "]" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/capability.eph *) capability = "memory_read" (* can read from raw memory *) | "memory_write" (* can write to raw memory *) | "io" (* can perform I/O *) | "network" (* can access network *) | "filesystem" (* can access filesystem *) | "process" (* can spawn/signal processes *) - | "ffi_unrestricted" (* no restrictions — escape hatch *) + | "ffi_unrestricted" (* no restrictions - escape hatch *) | IDENT (* user-defined capability *) ; -(* FFI calls carry capability requirements *) -ffi_expr = "__ffi" , [ capability_annotation ] , - "(" , STRING , { "," , expr } , ")" ; +(* DESIGN FORM of ffi_expr. The parser rule ffi_expr in part 1 is the current form. + * This form has productions that are not implemented: capability_annotation. + * + * ffi_expr = "__ffi" , [ capability_annotation ] , + * "(" , STRING , { "," , expr } , ")" ; + *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/capability_annotation.eph *) capability_annotation = "@capabilities" , "(" , capability , { "," , capability } , ")" ; + (* ================================================================ *) -(* 8. TYPES *) +(* 8. TYPES *) (* ================================================================ *) -ty = effect_ty ; +(* DESIGN FORM of ty. The parser rule ty in part 1 is the current form. + * This form has productions that are not implemented: effect_ty. + * + * ty = effect_ty ; + *) (* Effect annotation on function types: a -> b with IO + State(s) *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect_ty.eph *) effect_ty = fun_ty , [ "with" , effect_row ] ; (* Effect rows support both concrete effects and effect variables. @@ -291,48 +758,36 @@ effect_ty = fun_ty , [ "with" , effect_row ] ; * polymorphism over effects: * fn map[a, b, E: Effect](f: a -> b with E, xs: List(a)): List(b) with E * No `with` clause = pure (no effects). *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect_row.eph *) effect_row = effect_ref , { "+" , effect_ref } | IDENT (* effect variable *) | effect_ref , { "+" , effect_ref } , "+" , IDENT (* concrete + variable *) ; + +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect_row.eph *) effect_ref = CTOR_IDENT , [ "(" , ty_list , ")" ] ; +(* [ALIAS ty] the parser rule is the current form *) fun_ty = sum_ty , [ "->" , ty ] ; -sum_ty = prod_ty , { "+" , prod_ty } ; +(* DESIGN FORM of sum_ty. The parser rule sum_ty in part 1 is the current form. + * This form has productions that are not implemented: prod_ty. + * + * sum_ty = prod_ty , { "+" , prod_ty } ; + *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/prod_ty.eph *) prod_ty = type_atom , { "*" , type_atom } ; -type_atom = base_ty - | string_ty - | borrow_ty - | list_ty - | tuple_ty - | named_ty - | type_var - | "(" , ty , ")" - ; - -base_ty = "()" | "Bool" | "I32" | "I64" | "F32" | "F64" ; - -string_ty = "String" , [ "@" , IDENT ] ; - -borrow_ty = "&" , type_atom ; - -list_ty = "[" , ty , "]" ; - +(* [ALIAS product_ty] the parser rule is the current form *) tuple_ty = "(" , ty , "," , ty , { "," , ty } , ")" ; -(* Named type application: Option(I32), Result(String@r, Error) *) -(* Also bare names for nullary types: Color, Unit *) -named_ty = CTOR_IDENT , [ "(" , ty_list , ")" ] ; - -type_var = IDENT ; (* ================================================================ *) -(* 9. EXPRESSIONS *) +(* 9. EXPRESSIONS *) (* ================================================================ *) +(* [ALIAS expression] the parser rule is the current form *) expr = let_expr | let_lin_expr | lambda_expr @@ -344,194 +799,127 @@ expr = let_expr | perform_expr | or_expr ; -(* NOTE: No for-loops. Use recursion + fold + @tail_recursive. - * The compiler recognises tail-recursive patterns and compiles - * to efficient WASM loops. See ADR-015. *) -(* --- Bindings --- *) - -let_expr = "let" , pattern , [ ":" , ty ] , "=" , expr , "in" , expr ; - -let_lin_expr = "let!" , pattern , [ ":" , ty ] , "=" , expr , "in" , expr ; - -(* Note: let now accepts patterns, not just identifiers. - * let (a, b) = pair in ... - * let! Some(x) = opt in ... (partial — must be exhaustive or in match) *) - -(* --- Functions --- *) - -lambda_expr = "fn" , [ type_params ] , - "(" , [ param_list ] , ")" , - [ ":" , ty ] , - [ effect_annotation ] , - "->" , expr ; +(* DESIGN FORM of lambda_expr. The parser rule lambda_expr in part 1 is the current form. + * This form has productions that are not implemented: effect_annotation. + * + * lambda_expr = "fn" , [ type_params ] , + * "(" , [ param_list ] , ")" , + * [ ":" , ty ] , + * [ effect_annotation ] , + * "->" , expr ; + *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/effect_row.eph *) effect_annotation = "with" , effect_row ; -(* --- Control flow --- *) - -if_expr = "if" , expr , "then" , expr , "else" , expr ; - -(* --- Pattern matching --- *) - -match_expr = "match" , expr , "of" , - [ "|" ] , match_arm , { "|" , match_arm } , - "end" ; - -match_arm = pattern , [ "if" , expr ] , "=>" , expr ; - -(* --- Regions --- *) - -region_expr = "region" , IDENT , "{" , expr , "}" ; - -(* --- Binary case (core — still valid for expert use) --- *) - -case_expr = "case" , expr , "of" , - "inl" , "(" , IDENT , ")" , "->" , expr , - "inr" , "(" , IDENT , ")" , "->" , expr , - "end" ; - -(* --- Effects --- *) - -(* Perform an effect operation. - * REGION SAFETY: arguments must not reference regions that the handler - * might outlive. Use borrows (&) for region-bound values. *) -perform_expr = "perform" , IDENT , [ "(" , [ expr_list ] , ")" ] ; - -(* Handle effects with a handler. - * handle_mode: "shallow" handles first occurrence only (default: deep). - * handler_state: optional handler-local state. - * The handler body contains return, operation, and finally clauses. *) -handle_expr = "handle" , [ handle_mode ] , expr , "with" , - handler_ref , "end" ; +(* DESIGN FORM of handle_expr. The parser rule handle_expr in part 1 is the current form. + * This form has productions that are not implemented: handle_mode, handler_ref. + * + * handle_expr = "handle" , [ handle_mode ] , expr , "with" , + * handler_ref , "end" ; + *) -handle_mode = "shallow" ; (* default: deep — handle all occurrences *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/handle_mode.eph *) +handle_mode = "shallow" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/handler_ref.eph *) handler_ref = IDENT (* named handler *) | [ "(" , param_list , ")" ] , (* handler-local state *) { inline_handler_clause } (* inline handler *) ; +(* [ALIAS handler_clause] the parser has no finally clause *) inline_handler_clause = return_clause | inline_op_clause | finally_clause ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/resume_after_params.eph (the parser has handler_op_clause, with `resume` in the parameter list) *) inline_op_clause = "|" , IDENT , "(" , [ param_list ] , ")" , [ "," , resume_binding ] , "=>" , expr ; + (* ================================================================ *) -(* 10. PATTERNS *) +(* 10. PATTERNS *) (* ================================================================ *) -pattern = constructor_pattern - | pair_pattern - | tuple_pattern - | wildcard_pattern - | literal_pattern - | borrow_pattern - | var_pattern - | "(" , pattern , ")" - ; - -constructor_pattern = CTOR_IDENT , [ "(" , pattern_list , ")" ] ; +(* DESIGN FORM of pattern. The parser rule pattern in part 1 is the current form. + * This form has productions that are not implemented: borrow_pattern, tuple_pattern. + * + * pattern = constructor_pattern + * | pair_pattern + * | tuple_pattern + * | wildcard_pattern + * | literal_pattern + * | borrow_pattern + * | var_pattern + * | "(" , pattern , ")" + * ; + *) -pair_pattern = "(" , pattern , "," , pattern , ")" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/tuple_pattern.eph (the parser has the pattern of 2 parts as pair_pattern) *) tuple_pattern = "(" , pattern , "," , pattern , { "," , pattern } , ")" ; -wildcard_pattern = "_" ; -literal_pattern = literal ; + +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/borrow_pattern.eph *) borrow_pattern = "&" , pattern ; -var_pattern = IDENT ; -pattern_list = pattern , { "," , pattern } ; (* ================================================================ *) -(* 11. BINARY AND UNARY OPERATORS *) +(* 11. BINARY AND UNARY OPERATORS *) (* ================================================================ *) -or_expr = and_expr , { "||" , and_expr } ; -and_expr = eq_expr , { "&&" , eq_expr } ; -eq_expr = cmp_expr , { ( "==" | "!=" ) , cmp_expr } ; -cmp_expr = add_expr , { ( "<" | "<=" | ">" | ">=" ) , add_expr } ; -add_expr = mul_expr , { ( "+" | "-" ) , mul_expr } ; -mul_expr = concat_expr , { ( "*" | "/" | "%" ) , concat_expr } ; -concat_expr = unary_expr , { "++" , unary_expr } ; - -unary_expr = "!" , unary_expr - | "-" , unary_expr - | postfix_expr - ; +(* DESIGN FORM of mul_expr. The parser rule mul_expr in part 1 is the current form. + * This form has productions that are not implemented: concat_expr. + * + * mul_expr = concat_expr , { ( "*" | "/" | "%" ) , concat_expr } ; + *) -postfix_expr = atom_expr , { postfix_op } ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/concat.eph *) +concat_expr = unary_expr , { "++" , unary_expr } ; -postfix_op = call_op | index_op | member_op | type_app_op ; -call_op = "(" , [ expr_list ] , ")" ; -index_op = "[" , expr , "]" ; -member_op = "." , ( INTEGER | IDENT ) ; -type_app_op = "[" , ty_list , "]" ; -(* Type application: identity[I32](42) — explicit type argument *) (* ================================================================ *) -(* 12. ATOMIC EXPRESSIONS *) +(* 12. ATOMIC EXPRESSIONS *) (* ================================================================ *) -atom_expr = ffi_expr - | string_method - | inl_expr - | inr_expr - | borrow_expr - | deref_expr - | drop_expr - | copy_expr - | construct_expr - | list_literal - | paren_or_pair - | block_expr - | comptime_splice - | type_desc_expr - | literal - | variable - ; - -string_method = "String" , "." , IDENT , [ "@" , IDENT ] , - "(" , [ expr_list ] , ")" ; - -inl_expr = "inl" , "[" , ty , "]" , "(" , expr , ")" ; -inr_expr = "inr" , "[" , ty , "]" , "(" , expr , ")" ; +(* DESIGN FORM of atom_expr. The parser rule atom_expr in part 1 is the current form. + * This form has productions that are not implemented: comptime_splice, deref_expr, type_desc_expr. + * + * atom_expr = ffi_expr + * | string_method + * | inl_expr + * | inr_expr + * | borrow_expr + * | deref_expr + * | drop_expr + * | copy_expr + * | construct_expr + * | list_literal + * | paren_or_pair + * | block_expr + * | comptime_splice + * | type_desc_expr + * | literal + * | variable + * ; + *) -borrow_expr = "&" , unary_expr ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/deref.eph *) deref_expr = "*" , unary_expr ; -drop_expr = "drop" , "(" , expr , ")" ; -copy_expr = "copy" , "(" , expr , ")" ; - -(* Named constructor: Some(42), None, Ok(value) *) -construct_expr = CTOR_IDENT , [ "(" , [ expr_list ] , ")" ] ; - -list_literal = "[" , [ expr , { "," , expr } ] , "]" ; - -paren_or_pair = "(" , [ expr , { "," , expr } ] , ")" ; - -block_expr = "{" , { expr , ";" } , expr , "}" ; (* Splice comptime result into runtime code *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/splice.eph *) comptime_splice = "@splice" , "(" , comptime_expr , ")" ; (* Runtime type descriptor (unrestricted value, Harvard-safe) *) +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/type_desc.eph *) type_desc_expr = "@type_desc_of" , "(" , ty , ")" ; -expr_list = expr , { "," , expr } ; - -variable = IDENT ; - -literal = "()" | BOOLEAN | FLOAT32 | FLOAT | INTEGER | STRING ; (* ================================================================ *) -(* 13. COMPTIME EXPRESSIONS (META PLANE) *) +(* 13. COMPTIME EXPRESSIONS (META PLANE) *) (* ================================================================ *) -(* Comptime expressions are total and pure by definition. *) -(* They can inspect types and generate surface AST. *) -(* They CANNOT reference runtime values. *) -(* Their output is validated by the type checker (Harvard guarantee). *) - +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_ty = "Type" (* reified type *) | "TypeDesc" (* runtime type descriptor *) | "SurfaceDecl" (* surface AST declaration *) @@ -543,6 +931,7 @@ comptime_ty = "Type" (* reified type *) | IDENT ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_expr = comptime_intrinsic | comptime_match | comptime_if @@ -553,6 +942,7 @@ comptime_expr = comptime_intrinsic | IDENT ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_intrinsic = "@type_desc_of" , "(" , ty , ")" | "@fields_of" , "(" , ty , ")" | "@constructors_of" , "(" , ty , ")" @@ -568,196 +958,94 @@ comptime_intrinsic = "@type_desc_of" , "(" , ty , ")" | "@warning" , "(" , STRING , ")" (* compile warning *) ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_match = "match" , comptime_expr , "of" , { "|" , comptime_pattern , "=>" , comptime_expr } , "end" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_pattern = CTOR_IDENT , [ "(" , comptime_pattern_list , ")" ] | "_" | IDENT | comptime_literal ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_pattern_list = comptime_pattern , { "," , comptime_pattern } ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_if = "if" , comptime_expr , "then" , comptime_expr , "else" , comptime_expr ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_let_in = "let" , IDENT , "=" , comptime_expr , "in" , comptime_expr ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_call = IDENT , "(" , [ comptime_expr , { "," , comptime_expr } ] , ")" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_list = "[" , [ comptime_expr , { "," , comptime_expr } ] , "]" ; +(* [UNIMPLEMENTED] refused: tests/v2-grammar/unimplemented/comptime.eph *) comptime_literal = INTEGER | STRING | BOOLEAN | "()" ; + (* ================================================================ *) -(* 14. TERMINALS *) +(* 14. TERMINALS *) (* ================================================================ *) (* Lowercase identifier: variables, functions, type variables *) +(* [ALIAS identifier] the parser rule is the current form *) IDENT = LOWER_ALPHA , { ALPHA_NUM | "_" } ; (* Uppercase identifier: constructors, type names, trait names *) +(* [ALIAS constructor_name] the parser rule is the current form *) CTOR_IDENT = UPPER_ALPHA , { ALPHA_NUM | "_" } ; +(* [ALIAS integer] the parser rule is the current form *) INTEGER = DIGIT , { DIGIT } ; + +(* [ALIAS float] the parser rule is the current form *) FLOAT = DIGIT , { DIGIT } , "." , DIGIT , { DIGIT } ; + (* An F32 literal carries the `f32` suffix: 1.5f32. An unsuffixed float literal is F64. An INTEGER is I32 when it fits, else I64; a `-` written directly on the digits is part of the literal. *) +(* [ALIAS float32] the parser rule is the current form *) FLOAT32 = FLOAT , "f32" ; + +(* [ALIAS boolean] the parser rule is the current form *) BOOLEAN = "true" | "false" ; + +(* [ALIAS string] the parser rule is the current form *) STRING = '"' , { CHAR } , '"' ; +(* [ALIAS ASCII_ALPHA] the parser takes an upper-case letter at the start of an identifier too *) LOWER_ALPHA = "a" | ... | "z" | "_" ; + +(* [ALIAS ASCII_ALPHA_UPPER] the parser rule is the current form *) UPPER_ALPHA = "A" | ... | "Z" ; + +(* [ALIAS ASCII_ALPHANUMERIC] the parser rule is the current form *) ALPHA_NUM = LOWER_ALPHA | UPPER_ALPHA | DIGIT ; + +(* [ALIAS ASCII_DIGIT] the parser rule is the current form *) DIGIT = "0" | ... | "9" ; + +(* [ALIAS string_inner] the parser rule is the current form *) CHAR = (* any character except unescaped '"' *) ; -(* ================================================================ *) -(* 15. KEYWORDS *) -(* ================================================================ *) - -(* Reserved words that cannot be used as IDENT: - * - * module import from pub - * fn let let! in type data - * trait impl effect handler - * if then else match of end case - * old shallow finally return resume once multi - * inl inr region - * drop copy - * handle perform with where - * requires ensures invariant - * capabilities - * true false - * Bool I32 I64 F32 F64 String - *) (* ================================================================ *) -(* 16. WHITESPACE AND COMMENTS *) +(* 16. WHITESPACE AND COMMENTS *) (* ================================================================ *) -WHITESPACE = " " | "\t" | "\n" | "\r" ; +(* [ALIAS COMMENT] the parser rule is the current form *) LINE_COMMENT = "//" , { NOT_NEWLINE } ; + +(* [ALIAS COMMENT] the parser rule is the current form *) BLOCK_COMMENT = "/*" , { NOT_STAR_SLASH } , "*/" ; (* Doc comments generate documentation *) +(* [ALIAS COMMENT] the parser reads `///` as a line comment *) DOC_COMMENT = "///" , { NOT_NEWLINE } ; - - -(* ================================================================ *) -(* APPENDIX A: DESUGARING TARGETS *) -(* ================================================================ *) - -(* Each surface feature desugars to the core calculus: - * - * | Surface | Core | - * |------------------------|-----------------------------------| - * | data T = A | B(x) | type T = () + x (binary sums) | - * | match e of ... | nested case/inl/inr | - * | Construct(args) | inl/inr chains | - * | Named(T1, T2) | substituted binary sum type | - * | fn f[a](x: a): a | monomorphised or Λa. ... | - * | trait T(a) = ... | @derive → comptime generation | - * | | polymorphic → dictionary records | - * | (no for-loops) | recursion + fold + @tail_recursive| - * | perform Op(args) | effect operation call | - * | handle e with h | handler application | - * | requires P | if !P then abort else ... | - * | ensures P | let result = ... in assert(P) | - * | old(expr) | evaluated before body, borrows | - * | @comptime { ... } | run at compile time, splice result| - * | @derive(Eq) | comptime-generated impl block | - * | pub fn ... | (visibility checked, then erased) | - * | @inline fn ... | (inlining directive, then erased) | - * | capabilities: [...] | (comptime-verified, then erased) | - *) - - -(* ================================================================ *) -(* APPENDIX B: LINEAR SAFETY INVARIANTS *) -(* ================================================================ *) - -(* These invariants must hold across ALL features: - * - * 1. CONSUMPTION (dyadic): - * - let! bindings are consumed exactly once (linear discipline) - * - let bindings are consumed at most once (affine — implicit drop OK) - * - match arms on linear values must be exhaustive - * - effect handlers: resume(once) when continuation captures linear values - * - finally clause must consume captured linears if resume not called - * - * 2. REGIONS: - * - values referencing region r cannot escape r (NoRegionInType) - * - closures capturing region-bound values are region-scoped - * - effect operations CANNOT pass region-bound values to handlers - * outside the region (prevents dangling references) - * - use borrows (&) for region-bound values in effect operations - * - * 3. COMPTIME SEPARATION (Harvard): - * - @comptime blocks cannot reference runtime values - * - TypeDesc is unrestricted (freely copyable) - * - @splice output is validated by the type checker - * - comptime functions are total and pure - * - * 4. EFFECTS: - * - no `with` clause = pure (no effects) - * - effect handlers must handle all operations in the effect - * - resume(once): one-shot, required when linear captures exist - * - resume(multi): multi-shot, type error if linear captures exist - * - finally clause: runs when continuation discarded, must clean up - * - effect variables must be explicit (no implicit effect polymorphism) - * - * 5. CONTRACTS: - * - requires: evaluated before body, borrows arguments - * - ensures: evaluated after body, can reference `result` and `old(expr)` - * - old(expr): borrows before consumption, captures as unrestricted - * - invariant: maintained across body execution - * - * 6. CAPABILITIES: - * - __ffi calls must satisfy module capability declarations - * - capability checking is comptime (zero runtime cost) - * - ffi_unrestricted is an explicit escape hatch - * - * 7. GENERICS: - * - [a] defaults to linear (most restrictive = compatible with all types) - * - [a: Affine] opts into affine (can drop) - * - [a: Unrestricted] opts into unrestricted (can copy and drop) - *) - - -(* ================================================================ *) -(* APPENDIX C: INTERACTION MATRIX *) -(* ================================================================ *) - -(* How features interact with linear/affine types: - * - * | Feature | Linear (let!) interaction | - * |----------------|-------------------------------------------| - * | Generics | [a] defaults to linear (most restrictive).| - * | | Generic code works with ALL types. | - * | | [a: Affine] or [a: Unrestricted] opt out. | - * | Traits | Observe traits borrow (&). Transform | - * | | traits consume and return. Trait bound | - * | | documents ownership cost. | - * | Effects | perform consumes linear args. | - * | | resume(once) when continuation captures | - * | | linear values (prevents laundering). | - * | | finally clause for cleanup on discard. | - * | | Region-bound values: borrow, don't pass. | - * | Contracts | requires borrows (&) to inspect. | - * | | ensures uses old(expr) for pre-state. | - * | Comptime | Cannot reference linear runtime values. | - * | | Harvard separation guarantees this. | - * | FFI | Linear values passed to FFI are consumed. | - * | | Capabilities restrict what FFI can do. | - * | Patterns | Case vars use Param discipline. | - * | | Linear types demand consumption. | - * | | Wildcards on let!-bound = error. | - * | | Wildcards on let-bound = implicit drop. | - * | Modules | Name scoping only. No interaction with | - * | | linearity, regions, or effects. | - *) diff --git a/src/ephapax-parser/Cargo.toml b/src/ephapax-parser/Cargo.toml index 3be2f4a5..ccaf4a71 100644 --- a/src/ephapax-parser/Cargo.toml +++ b/src/ephapax-parser/Cargo.toml @@ -24,6 +24,9 @@ pest = "2.7" pest_derive = "2.7" [dev-dependencies] +# The grammar conformance test reads ephapax.pest with the parser that +# pest_derive uses (already in the lock file, same version). +pest_meta = "2.7" ephapax-desugar = { path = "../ephapax-desugar" } ephapax-typing = { path = "../ephapax-typing" } criterion = { workspace = true } diff --git a/src/ephapax-parser/src/grammar_conformance.rs b/src/ephapax-parser/src/grammar_conformance.rs new file mode 100644 index 00000000..24aaa52a --- /dev/null +++ b/src/ephapax-parser/src/grammar_conformance.rs @@ -0,0 +1,368 @@ +// SPDX-License-Identifier: MPL-2.0 +// Owner: Jonathan D.A. Jewell +// +//! One normative grammar (v2 plan rung E7). +//! +//! `spec/ephapax-v2-grammar.ebnf` has 2 parts: +//! +//! 1. The parser grammar. This module makes it from `ephapax.pest`, and +//! a test fails when the 2 files are not the same grammar. Each rule +//! is in the parse tree of a fixture. +//! 2. The productions of the v2 design that the parser does not have by +//! that name. Each one has a mark: `[ALIAS rule]` (the parser has the +//! construct as `rule`) or `[UNIMPLEMENTED]` with a fixture that the +//! parser refuses. +//! +//! So no production is unaccounted for. To write part 1 again after a +//! change of `ephapax.pest`: +//! +//! ```text +//! UPDATE_GRAMMAR=1 cargo test -p ephapax-parser grammar_conformance +//! ``` + +use std::collections::{BTreeMap, BTreeSet}; +use std::path::{Path, PathBuf}; + +use pest::Parser as _; +use pest_meta::ast::{Expr, RuleType}; + +use crate::{parse_module, parse_surface_module, EphapaxParser, Rule}; + +const PEST: &str = include_str!("ephapax.pest"); +const BEGIN: &str = "(* BEGIN GENERATED: the parser grammar, from ephapax.pest. Do not edit. *)"; +const END: &str = "(* END GENERATED *)"; + +/// Rules that are in the grammar and never in a parse tree, with the +/// reason. Each other rule must be in the parse tree of a fixture. +const NO_PAIR: &[(&str, &str)] = &[ + ("WHITESPACE", "silent"), + ("COMMENT", "silent"), + ("string_inner", "inside the atomic rule `string`"), + ("escape", "inside the atomic rule `string`"), + ("keyword", "only in the lookahead of `identifier`"), + ("keyword_boundary", "only in the lookahead of `identifier`"), +]; + +fn repo() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("../..") +} + +fn ebnf_path() -> PathBuf { + repo().join("spec/ephapax-v2-grammar.ebnf") +} + +fn pest_rules() -> BTreeMap { + let pairs = pest_meta::parser::parse(pest_meta::parser::Rule::grammar_rules, PEST) + .expect("ephapax.pest parses"); + pest_meta::parser::consume_rules(pairs) + .expect("ephapax.pest is a valid grammar") + .into_iter() + .map(|rule| (rule.name, (rule.ty, rule.expr))) + .collect() +} + +/// A terminal. EBNF has no escapes: a control character has a name. +fn terminal(text: &str) -> String { + match text { + "\n" => "? LF ?".into(), + "\r" => "? CR ?".into(), + "\t" => "? TAB ?".into(), + _ if text.contains('"') => format!("'{text}'"), + _ => format!("\"{text}\""), + } +} + +/// The alternatives of a choice, in order. +fn alternatives(expr: &Expr) -> Vec<&Expr> { + match expr { + Expr::Choice(left, right) => { + let mut all = alternatives(left); + all.extend(alternatives(right)); + all + } + other => vec![other], + } +} + +/// EBNF text of a pest expression. `level` is where the text goes: 0 in +/// a choice, 1 in a sequence, 2 where one item must stand. +fn ebnf(expr: &Expr, level: u8) -> String { + let (text, own) = match expr { + Expr::Str(text) => (terminal(text), 2), + Expr::Range(from, to) => (format!("? {} to {} ?", terminal(from), terminal(to)), 2), + Expr::Ident(name) => (name.clone(), 2), + Expr::PosPred(inner) => (format!("&( {} )", ebnf(inner, 0)), 2), + Expr::NegPred(inner) => (format!("!( {} )", ebnf(inner, 0)), 2), + Expr::Seq(left, right) => (format!("{} , {}", ebnf(left, 1), ebnf(right, 1)), 1), + Expr::Choice(..) => { + let parts: Vec = alternatives(expr).iter().map(|e| ebnf(e, 1)).collect(); + (parts.join(" | "), 0) + } + Expr::Opt(inner) => (format!("[ {} ]", ebnf(inner, 0)), 2), + Expr::Rep(inner) => (format!("{{ {} }}", ebnf(inner, 0)), 2), + Expr::RepOnce(inner) => (format!("{{ {} }}-", ebnf(inner, 0)), 2), + // snip: the other pest forms (counted repeats, the stack) are not + // in ephapax.pest. One that arrives shows as it is, for a review. + other => (format!("? pest: {other:?} ?"), 2), + }; + if own < level { + format!("( {text} )") + } else { + text + } +} + +/// One rule as an EBNF production. +fn production(name: &str, ty: RuleType, expr: &Expr) -> String { + let note = match ty { + RuleType::Normal => "", + RuleType::Silent => " (* silent: no node in the parse tree *)", + RuleType::Atomic => " (* atomic: no white space between the parts *)", + RuleType::CompoundAtomic => " (* compound atomic *)", + RuleType::NonAtomic => " (* non-atomic *)", + }; + let one_line = format!("{name} = {} ;{note}", ebnf(expr, 0)); + let parts = alternatives(expr); + if one_line.len() <= 96 || parts.len() == 1 { + return one_line; + } + let indent = " ".repeat(name.len() + 1); + let parts: Vec = parts.iter().map(|e| ebnf(e, 1)).collect(); + format!( + "{name} = {}\n{indent};{note}", + parts.join(&format!("\n{indent}| ")) + ) +} + +/// The name of the rule that a line of `ephapax.pest` starts, if any. +fn rule_start(line: &str) -> Option<&str> { + let (name, rest) = line.split_once('=')?; + let name = name.trim_end(); + let named = !name.is_empty() && name.chars().all(|c| c.is_ascii_alphanumeric() || c == '_'); + let opens = rest.trim_start().trim_start_matches(['_', '@', '$', '!']); + (named && !line.starts_with(' ') && opens.starts_with('{')).then_some(name) +} + +/// `{` minus `}` in a line of a rule, outside strings and comments. +fn brace_depth(line: &str) -> i32 { + let (mut depth, mut quote, mut chars) = (0, None, line.chars().peekable()); + while let Some(c) = chars.next() { + match (quote, c) { + (Some(_), '\\') => { + chars.next(); + } + (Some(q), _) if c == q => quote = None, + (Some(_), _) => {} + (None, '"' | '\'') => quote = Some(c), + (None, '/') if chars.peek() == Some(&'/') => break, + (None, '{') => depth += 1, + (None, '}') => depth -= 1, + (None, _) => {} + } + } + depth +} + +/// Part 1 of the specification grammar: each rule of `ephapax.pest` in +/// the order of that file, with the comments of that file. +fn generated() -> String { + let rules = pest_rules(); + let mut out = String::new(); + let mut comment: Vec = Vec::new(); + let flush = |comment: &mut Vec, out: &mut String| { + for line in comment.drain(..) { + out.push_str(&format!("(* {} *)\n", line.replace("*)", "* )"))); + } + }; + let mut lines = PEST.lines(); + while let Some(line) = lines.next() { + if let Some(text) = line.strip_prefix("//") { + // A line of `=` or `-` is a banner of the pest file, and the + // specification file has its own licence lines. + let text = text.trim(); + let banner = text.chars().all(|c| c == '=' || c == '-'); + if !banner && !text.starts_with("SPDX-") && !text.starts_with("Owner:") { + comment.push(text.replace('\u{2014}', "-")); + } + } else if let Some(name) = rule_start(line) { + flush(&mut comment, &mut out); + let (ty, expr) = &rules[name]; + out.push_str(&production(name, *ty, expr)); + out.push('\n'); + let mut depth = brace_depth(line); + while depth > 0 { + depth += brace_depth(lines.next().expect("the rule has an end")); + } + } else if !comment.is_empty() { + // The end of a paragraph of comments. + flush(&mut comment, &mut out); + out.push('\n'); + } else if !out.ends_with("\n\n") { + out.push('\n'); + } + } + out.trim_end().to_string() + "\n" +} + +/// The 3 parts of the specification file: before part 1, part 1, after. +fn split(text: &str) -> (&str, &str, &str) { + let (head, rest) = text.split_once(BEGIN).expect("the BEGIN GENERATED line"); + let (part, tail) = rest.split_once(END).expect("the END GENERATED line"); + (head, part, tail) +} + +/// The names of the productions that a grammar text defines, in order. A +/// production starts at the start of a line. +fn defined(text: &str) -> Vec<&str> { + text.lines() + .filter_map(|line| { + let (name, _) = line.split_once('=')?; + let name = name.trim_end(); + let named = !name.is_empty() + && !line.starts_with(' ') + && name.chars().all(|c| c.is_ascii_alphanumeric() || c == '_'); + named.then_some(name) + }) + .collect() +} + +#[test] +fn the_specification_grammar_says_what_the_parser_accepts() { + let path = ebnf_path(); + let text = std::fs::read_to_string(&path).expect("read the specification grammar"); + let (head, part, tail) = split(&text); + let want = format!("\n\n{}\n", generated()); + if std::env::var_os("UPDATE_GRAMMAR").is_some() && part != want { + std::fs::write(&path, format!("{head}{BEGIN}{want}{END}{tail}")) + .expect("write the specification grammar"); + return; + } + assert!( + part == want, + "spec/ephapax-v2-grammar.ebnf is not the grammar of ephapax.pest. Run:\n \ + UPDATE_GRAMMAR=1 cargo test -p ephapax-parser grammar_conformance" + ); + // Each rule of the parser is a production, one time. + let names = defined(part); + let rules = pest_rules(); + assert_eq!(names.len(), rules.len()); + assert!(names.iter().all(|name| rules.contains_key(*name))); +} + +/// Each `.eph` file below `dir`. +fn eph_files(dir: &Path, out: &mut Vec) { + let Ok(entries) = std::fs::read_dir(dir) else { + return; + }; + for entry in entries.flatten() { + let path = entry.path(); + if path.is_dir() { + eph_files(&path, out); + } else if path.extension().is_some_and(|ext| ext == "eph") { + out.push(path); + } + } +} + +/// The rules in the parse tree of `source`, parsed from the rule `entry`. +fn rules_in(entry: Rule, source: &str) -> Option> { + let pairs = EphapaxParser::parse(entry, source).ok()?; + Some( + pairs + .flatten() + .map(|pair| format!("{:?}", pair.as_rule())) + .collect(), + ) +} + +/// Part 1: each rule of the parser is in the parse tree of a fixture, or +/// it is in [`NO_PAIR`]. +#[test] +fn each_parser_rule_is_in_a_fixture() { + let mut seen = BTreeSet::new(); + let fixtures = repo().join("tests/v2-grammar"); + let mut files = Vec::new(); + eph_files(&fixtures.join("productions"), &mut files); + assert!( + !files.is_empty(), + "no fixture in tests/v2-grammar/productions" + ); + for file in &files { + let source = std::fs::read_to_string(file).expect("read fixture"); + let rules = rules_in(Rule::module, &source) + .unwrap_or_else(|| panic!("{} does not parse", file.display())); + seen.extend(rules); + } + // The 2 other entry points of the grammar. + seen.extend(rules_in(Rule::expression_only, "1 + 2").expect("an expression parses")); + seen.extend(rules_in(Rule::module_header, "module a.b\nfn").expect("a header parses")); + + let no_pair: BTreeSet<&str> = NO_PAIR.iter().map(|(name, _)| *name).collect(); + let wrong: Vec = pest_rules() + .into_keys() + .filter(|name| seen.contains(name) == no_pair.contains(name.as_str())) + .collect(); + assert!( + wrong.is_empty(), + "these rules are in no fixture and not in NO_PAIR, or in both: {wrong:?}. \ + Add a fixture to tests/v2-grammar/productions, or correct NO_PAIR." + ); +} + +/// Part 2: each production that is not a rule of the parser has a mark. +/// An `[ALIAS rule]` names a rule of the parser. The parser refuses the +/// fixture of an `[UNIMPLEMENTED]` production. +#[test] +fn each_design_production_is_an_alias_or_is_refused() { + let text = std::fs::read_to_string(ebnf_path()).expect("read the specification grammar"); + let (head, part, tail) = split(&text); + assert!(defined(head).is_empty(), "a production before part 1"); + + let rules = pest_rules(); + // Names that the parser grammar uses and pest defines. + let builtins: BTreeSet<&str> = PEST + .split(|c: char| !(c.is_ascii_alphanumeric() || c == '_')) + .filter(|word| word.starts_with("ASCII_")) + .collect(); + let mut names: BTreeSet<&str> = defined(part).into_iter().collect(); + let mut mark: Option<&str> = None; + let (mut aliases, mut refused) = (0, 0); + for line in tail.lines() { + if let Some(rest) = line.strip_prefix("(* [") { + mark = Some(rest); + continue; + } + let Some(&name) = defined(line).first() else { + continue; + }; + assert!(names.insert(name), "`{name}` has 2 definitions"); + let mark = mark + .take() + .unwrap_or_else(|| panic!("`{name}` has no mark: it is unaccounted for")); + if let Some(rest) = mark.strip_prefix("ALIAS ") { + let rule = rest.split(']').next().unwrap_or_default(); + assert!( + rules.contains_key(rule) || builtins.contains(rule), + "`{name}` is an alias of `{rule}`, which the parser does not have" + ); + aliases += 1; + } else { + let fixture = mark + .strip_prefix("UNIMPLEMENTED] refused: ") + .and_then(|rest| rest.split(' ').next()) + .unwrap_or_else(|| panic!("`{name}`: the mark `{mark}` is not a known mark")); + let source = std::fs::read_to_string(repo().join(fixture)) + .unwrap_or_else(|_| panic!("`{name}`: no fixture {fixture}")); + assert!( + parse_surface_module(&source, "fixture").is_err() + && parse_module(&source, "fixture").is_err(), + "`{name}` has the mark UNIMPLEMENTED, but the parser accepts {fixture}" + ); + refused += 1; + } + } + assert!(mark.is_none(), "a mark with no production after it"); + // 0 productions unaccounted for: a rule of the parser, an alias, or + // a production that the parser refuses. + assert_eq!(names.len(), rules.len() + aliases + refused); +} diff --git a/src/ephapax-parser/src/lib.rs b/src/ephapax-parser/src/lib.rs index 23fcb6e6..c00647b8 100644 --- a/src/ephapax-parser/src/lib.rs +++ b/src/ephapax-parser/src/lib.rs @@ -26,6 +26,8 @@ use pest_derive::Parser; use smol_str::SmolStr; pub mod error; +#[cfg(test)] +mod grammar_conformance; pub mod surface; pub use error::{ParseError, Report}; diff --git a/tests/v2-grammar/productions/declarations.eph b/tests/v2-grammar/productions/declarations.eph new file mode 100644 index 00000000..b7bb7af6 --- /dev/null +++ b/tests/v2-grammar/productions/declarations.eph @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: MPL-2.0 +// Grammar fixture (v2 plan rung E7): module header, imports, and each +// kind of declaration. The grammar conformance test of ephapax-parser +// reads the parse tree of this file; nothing runs it. +module fixtures/declarations + +import lib/math +import lib.shapes(area, Shape) + +extern "host" { + type Window + fn window_open(title: String): Window + fn window_close(w: Window) -> () +} + +let limit: I32 = 10 +let name = 7 + +pub data Option(a) = None | Some(a) +data Shape = | Dot | Seg(I32) | Rect(I32, I32) + +pub type Id = I32 +type Pair = (I32, I64) +linear type Handle = I32 +affine type Token = I32 +type Point = { x: I32, y: I32 } +type App = GsaApp { title: String, width: I32, } +type Color = red | green(I32) | blue +type Callback = I32 -> I32 + () + +@inline +@tail_recursive +pub fn id(x: a): a = x + +fn first(p: (a, b)): a = fst(p) + +fn unit(): () = () diff --git a/tests/v2-grammar/productions/expressions.eph b/tests/v2-grammar/productions/expressions.eph new file mode 100644 index 00000000..e37911fd --- /dev/null +++ b/tests/v2-grammar/productions/expressions.eph @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: MPL-2.0 +// Grammar fixture (v2 plan rung E7): each expression, pattern and type +// form of the parser grammar. The grammar conformance test of +// ephapax-parser reads the parse tree of this file; nothing runs it, +// and the type checker does not see it. +module fixtures/expressions + +data Option(a) = None | Some(a) + +fn literals(): () = + let a = () in + let b = true in + let c = 1.5f32 in + let d = 2.5 in + let e = 42 in + let f = "text\n" in + () + +fn operators(x: I32, y: I32): Bool = + !(x + y * 2 - y / 3 % 4 < 9) || x <= y && x == y || x != -y + +fn lets(p: (I32, I32)): I32 = + let (a, b) = p in + let! c: I32 = a in + let d = b + let! e = c + d + e + +fn control(o: Option(I32), s: I32 + I32): I32 = + let f = fn(n: I32) -> n + 1 in + let g = if true then 1 else 2 in + let h = match o of + | None => 0 + | Some(0) => 1 + | Some(n) if n > 5 => n + | _ => 2 + end in + let i = match (g, h) of | (a, b) => a + b end in + let k = match () of | () => 0 end in + let j = case s of inl(l) -> l inr(r) -> r end in + f(g) + i + j + +fn regions(): I32 = + region r { + let! s = String.new@r("hi") + let n = String.len(&s) + let m = &mut n + drop(s); + copy(n) + } + +fn sums(n: I32): I32 + Bool = + if n > 0 then inl[Bool](n) else inr[I32](false) + +fn aggregates(xs: [I32], rec: { x: I32, y: I32 }, t: &I32): I32 = + let ys = [1, 2, 3] in + let p = (ys[0], xs[1]) in + let q = { x = 1, y: I32 = 2, z: 3, } in + let w = Point { x = 1 } in + let v = Some(snd(p)) in + let u = id[I32](fst(p)) in + p.0 + lib.helper(u, 2) + unit() + +fn effects(): I32 = + handle perform get(1) + perform tick with + | return(x) => x + | get(n, resume) => n + | put(resume(once)) => 0 + | all(resume(multi)) => 1 + end + +fn foreign(n: I32): I32 = __ffi("host_add", n, 1) diff --git a/tests/v2-grammar/unimplemented/annotation_args.eph b/tests/v2-grammar/unimplemented/annotation_args.eph new file mode 100644 index 00000000..a5da73d6 --- /dev/null +++ b/tests/v2-grammar/unimplemented/annotation_args.eph @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +@inline(always) +fn f(): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/borrow_pattern.eph b/tests/v2-grammar/unimplemented/borrow_pattern.eph new file mode 100644 index 00000000..905004dd --- /dev/null +++ b/tests/v2-grammar/unimplemented/borrow_pattern.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(x: &I32): I32 = match x of | &y => 0 end diff --git a/tests/v2-grammar/unimplemented/capability.eph b/tests/v2-grammar/unimplemented/capability.eph new file mode 100644 index 00000000..2a869983 --- /dev/null +++ b/tests/v2-grammar/unimplemented/capability.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m capabilities: [io] + +fn main(): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/capability_annotation.eph b/tests/v2-grammar/unimplemented/capability_annotation.eph new file mode 100644 index 00000000..5c039a99 --- /dev/null +++ b/tests/v2-grammar/unimplemented/capability_annotation.eph @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +@capabilities(io) +fn main(): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/comptime.eph b/tests/v2-grammar/unimplemented/comptime.eph new file mode 100644 index 00000000..734b96a7 --- /dev/null +++ b/tests/v2-grammar/unimplemented/comptime.eph @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +@comptime { + fn size(t: Type): I32 = 0 + let n = 1 +} diff --git a/tests/v2-grammar/unimplemented/concat.eph b/tests/v2-grammar/unimplemented/concat.eph new file mode 100644 index 00000000..c8f988de --- /dev/null +++ b/tests/v2-grammar/unimplemented/concat.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = 1 ++ 2 diff --git a/tests/v2-grammar/unimplemented/contract.eph b/tests/v2-grammar/unimplemented/contract.eph new file mode 100644 index 00000000..eb773a5e --- /dev/null +++ b/tests/v2-grammar/unimplemented/contract.eph @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(x: I32): I32 + requires x > 0 + ensures result > old(x) += x diff --git a/tests/v2-grammar/unimplemented/deref.eph b/tests/v2-grammar/unimplemented/deref.eph new file mode 100644 index 00000000..c24d4e6f --- /dev/null +++ b/tests/v2-grammar/unimplemented/deref.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(x: &I32): I32 = *x diff --git a/tests/v2-grammar/unimplemented/effect.eph b/tests/v2-grammar/unimplemented/effect.eph new file mode 100644 index 00000000..0255d19f --- /dev/null +++ b/tests/v2-grammar/unimplemented/effect.eph @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +effect State = + fn get(): I32 +end diff --git a/tests/v2-grammar/unimplemented/effect_row.eph b/tests/v2-grammar/unimplemented/effect_row.eph new file mode 100644 index 00000000..25e222f1 --- /dev/null +++ b/tests/v2-grammar/unimplemented/effect_row.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(): I32 with IO = 0 diff --git a/tests/v2-grammar/unimplemented/effect_ty.eph b/tests/v2-grammar/unimplemented/effect_ty.eph new file mode 100644 index 00000000..352aae21 --- /dev/null +++ b/tests/v2-grammar/unimplemented/effect_ty.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(g: I32 -> I32 with IO): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/finally.eph b/tests/v2-grammar/unimplemented/finally.eph new file mode 100644 index 00000000..882e4fc2 --- /dev/null +++ b/tests/v2-grammar/unimplemented/finally.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = handle f() with | return(x) => x | finally => 0 end diff --git a/tests/v2-grammar/unimplemented/handle_mode.eph b/tests/v2-grammar/unimplemented/handle_mode.eph new file mode 100644 index 00000000..6ea5d20a --- /dev/null +++ b/tests/v2-grammar/unimplemented/handle_mode.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = handle shallow f() with | return(x) => x end diff --git a/tests/v2-grammar/unimplemented/handler_decl.eph b/tests/v2-grammar/unimplemented/handler_decl.eph new file mode 100644 index 00000000..4faf76a9 --- /dev/null +++ b/tests/v2-grammar/unimplemented/handler_decl.eph @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +handler counter for State = + | get() => 0 +end diff --git a/tests/v2-grammar/unimplemented/handler_ref.eph b/tests/v2-grammar/unimplemented/handler_ref.eph new file mode 100644 index 00000000..2e261dc6 --- /dev/null +++ b/tests/v2-grammar/unimplemented/handler_ref.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = handle f() with h end diff --git a/tests/v2-grammar/unimplemented/impl.eph b/tests/v2-grammar/unimplemented/impl.eph new file mode 100644 index 00000000..19452ae6 --- /dev/null +++ b/tests/v2-grammar/unimplemented/impl.eph @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +impl Show(I32) = + fn show(x: I32): I32 = x +end diff --git a/tests/v2-grammar/unimplemented/import_from.eph b/tests/v2-grammar/unimplemented/import_from.eph new file mode 100644 index 00000000..8fdf77f9 --- /dev/null +++ b/tests/v2-grammar/unimplemented/import_from.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +import Foo from "foo" diff --git a/tests/v2-grammar/unimplemented/prod_ty.eph b/tests/v2-grammar/unimplemented/prod_ty.eph new file mode 100644 index 00000000..171d91e8 --- /dev/null +++ b/tests/v2-grammar/unimplemented/prod_ty.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(p: I32 * I32): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/reexport.eph b/tests/v2-grammar/unimplemented/reexport.eph new file mode 100644 index 00000000..806eb977 --- /dev/null +++ b/tests/v2-grammar/unimplemented/reexport.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +pub import lib diff --git a/tests/v2-grammar/unimplemented/resume_after_params.eph b/tests/v2-grammar/unimplemented/resume_after_params.eph new file mode 100644 index 00000000..17121327 --- /dev/null +++ b/tests/v2-grammar/unimplemented/resume_after_params.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = handle f() with | return(x) => x | get(), resume => 1 end diff --git a/tests/v2-grammar/unimplemented/splice.eph b/tests/v2-grammar/unimplemented/splice.eph new file mode 100644 index 00000000..0d9e7ef3 --- /dev/null +++ b/tests/v2-grammar/unimplemented/splice.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = @splice(x) diff --git a/tests/v2-grammar/unimplemented/trait.eph b/tests/v2-grammar/unimplemented/trait.eph new file mode 100644 index 00000000..e74f8ac2 --- /dev/null +++ b/tests/v2-grammar/unimplemented/trait.eph @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +trait Show(a) = + fn show(x: a): I32 +end diff --git a/tests/v2-grammar/unimplemented/tuple_pattern.eph b/tests/v2-grammar/unimplemented/tuple_pattern.eph new file mode 100644 index 00000000..c750613e --- /dev/null +++ b/tests/v2-grammar/unimplemented/tuple_pattern.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn f(t: (I32, I32, I32)): I32 = match t of | (a, b, c) => a end diff --git a/tests/v2-grammar/unimplemented/type_desc.eph b/tests/v2-grammar/unimplemented/type_desc.eph new file mode 100644 index 00000000..07bf0959 --- /dev/null +++ b/tests/v2-grammar/unimplemented/type_desc.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn main(): I32 = @type_desc_of(I32) diff --git a/tests/v2-grammar/unimplemented/type_param_bound.eph b/tests/v2-grammar/unimplemented/type_param_bound.eph new file mode 100644 index 00000000..feef6aa8 --- /dev/null +++ b/tests/v2-grammar/unimplemented/type_param_bound.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn show(x: a): I32 = 0 diff --git a/tests/v2-grammar/unimplemented/where.eph b/tests/v2-grammar/unimplemented/where.eph new file mode 100644 index 00000000..0903c3b4 --- /dev/null +++ b/tests/v2-grammar/unimplemented/where.eph @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Not implemented: the parser must refuse this file. See the mark +// [UNIMPLEMENTED] in spec/ephapax-v2-grammar.ebnf, part 2. +module m + +fn keep(x: a): a where a: Show = x From 5775cc35bd09f750265286fd880a68473021ed15 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 16:43:49 +0000 Subject: [PATCH 2/2] fix(typing): a match guard cannot consume a use-once value 2 review findings on #431, each checked against the code. - A guard could consume a linear value and return false. The next arm is checked from the state after the scrutinee, so it used the value a second time: `check` accepted the program, and the interpreter stopped with "Linear value used after consumption". The checker now refuses a guard that consumes a binding that can be used one time, from outside the match or from the pattern of the arm (`GuardConsumesLinear`). A guard can read or borrow such a binding. The surface syntax reaches this case since the guard lowering of #431. - A type alias is visible in each module, and the alias registered last had the name. So `pub data Tally = T(Count)` of a module with `type Count = I32` got the `Count` of an importer that declares `type Count = Bool`. A module now gets its own alias first, and the body of a data type expands in the scope of its module. Tests: 2 refused programs and 1 alias case in the gate tests of run_wasm.rs. 614 all-target. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- src/ephapax-cli/tests/run_wasm.rs | 38 +++++++++++++++++++++++++++++++ src/ephapax-desugar/src/lib.rs | 29 +++++++++++++++++------ src/ephapax-typing/src/lib.rs | 32 ++++++++++++++++++++++++++ 3 files changed, 92 insertions(+), 7 deletions(-) diff --git a/src/ephapax-cli/tests/run_wasm.rs b/src/ephapax-cli/tests/run_wasm.rs index 00bfc8f7..cb44e3d0 100644 --- a/src/ephapax-cli/tests/run_wasm.rs +++ b/src/ephapax-cli/tests/run_wasm.rs @@ -279,6 +279,8 @@ fn a_module_names_a_data_type_only_through_a_pub_import() { "lib.eph", "module lib\n\ndata Inner = I(I32)\n\npub data Outer = O(Inner)\n\n\ pub data Box = MkBox(I32)\n\ndata Secret = Hidden(I32)\n\n\ + type Count = I32\n\npub data Tally = T(Count)\n\n\ + pub fn total(t: Tally): I32 = match t of | T(n) => n end\n\n\ pub fn mk(n: I32): Outer = O(I(n))\n\n\ pub fn get(o: Outer): I32 = match o of | O(i) => match i of | I(n) => n end end\n\n\ pub fn unbox(b: Box): I32 = match b of | MkBox(v) => v end\n\n\ @@ -320,6 +322,13 @@ fn a_module_names_a_data_type_only_through_a_pub_import() { "match Wrap(mk(6)) of | Wrap(o) => get(o) end", "6", ), + // `Tally` has the `Count` of `lib` in its field, also in a module + // that has its own alias `Count`. + ( + "import lib\n\ntype Count = Bool\n\nfn yes(c: Count): Count = c\n", + "if yes(true) then total(T(7)) else 0", + "7", + ), // A declaration of the module shadows an imported one. ( "import lib\n\ndata Box = MkBox(I32, I32)\n", @@ -489,6 +498,35 @@ fn a_false_guard_gives_the_value_to_the_next_arm() { } } + // A guard that consumes a linear value: a false guard gives the value + // to the next arm, which would use it a second time. `s` is from + // outside the match; `n` is a part of the scrutinee. + for (scrutinee, guard, name) in [ + ("Named(t, 3)", "eat(s)", "s"), + ("Named(s, 3)", "eat(n)", "n"), + ] { + write( + "consume.eph", + &format!( + "module consume\n\ndata Entry = Empty | Named(String@r, I32)\n\n\ + fn eat(s: String@r): Bool = let n = String.len(s) in n > 100\n\n\ + fn main(): I32 =\n region r {{\n let! s = String.new@r(\"hello\")\n \ + let! t = String.new@r(\"other\")\n match {scrutinee} of\n \ + | Named(n, k) if {guard} => String.len(n)\n \ + | Named(n, k) => String.len(n) + String.len(s) + String.len(t)\n \ + | Empty => 0\n end\n }}\n" + ), + ); + let out = ephapax(tmp.path(), &["check", "consume.eph"]); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success() + && stderr.contains(&format!("The guard of a match arm consumes `{name}`")), + "{guard}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ); + } + // (match, text of the load error) for (matched, error) in [ // A guarded arm does not cover its constructor. diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index 849f9331..854f26d1 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -214,9 +214,11 @@ pub struct DataRegistry { /// form so `desugar_named_type` can recursively expand them on /// demand. The stored value is whatever the parser produced for the /// alias body (record/sum decls already pre-lowered to `Prod`/`Sum`/ - /// `Tuple` by `parse_type_decl`), and the key of the module that - /// declares the alias: the body expands in the scope of that module. - type_aliases: HashMap, + /// `Tuple` by `parse_type_decl`). An alias is visible in each module. + /// Each entry has the key of the module that declares the alias: the + /// body expands in the scope of that module, and a module that + /// declares an alias of the same name gets its own. + type_aliases: HashMap>, } impl DataRegistry { @@ -292,11 +294,20 @@ impl DataRegistry { /// form. Lookups in `desugar_named_type` find the entry and /// recursively desugar it. pub fn register_type_alias(&mut self, home: &str, name: SmolStr, ty: SurfaceTy) { - self.type_aliases.insert(name, (ty, home.into())); + let entries = self.type_aliases.entry(name).or_default(); + entries.retain(|(module, _)| module != home); + entries.push((home.into(), ty)); } - fn lookup_type_alias(&self, name: &str) -> Option<&(SurfaceTy, SmolStr)> { - self.type_aliases.get(name) + /// The alias `name` as the module `scope` sees it, with the key of + /// the module that declares it: the alias of `scope`, or else the + /// alias that was registered last. + fn lookup_type_alias(&self, scope: &str, name: &str) -> Option<&(SmolStr, SurfaceTy)> { + let entries = self.type_aliases.get(name)?; + entries + .iter() + .find(|(module, _)| module == scope) + .or(entries.last()) } /// Look up a constructor by its name in the module `scope`. @@ -939,7 +950,11 @@ impl Desugarer { // `type Foo = T` aliases — recursively desugar the stored surface // form. Aliases are monomorphic here (parameterised aliases would // carry their args via the body). - if let Some((aliased, home)) = self.registry.lookup_type_alias(name.as_str()).cloned() { + let alias = self + .registry + .lookup_type_alias(&self.scope.borrow(), name.as_str()) + .cloned(); + if let Some((home, aliased)) = alias { if !args.is_empty() { return Err(DesugarError::TypeArityMismatch { name: name.to_string(), diff --git a/src/ephapax-typing/src/lib.rs b/src/ephapax-typing/src/lib.rs index cc3dbe08..bdd6233b 100644 --- a/src/ephapax-typing/src/lib.rs +++ b/src/ephapax-typing/src/lib.rs @@ -141,6 +141,12 @@ pub enum TypeError { )] PolymorphicRecursion(Var), + /// The guard of a match arm consumes a binding that can be used one + /// time. A false guard gives the value to the next arm, so the + /// binding would be used 2 times. + #[error("The guard of a match arm consumes `{0}`, which can be used one time. A guard can read or borrow it: a false guard gives the value to the next arm")] + GuardConsumesLinear(Var), + /// Type arguments on a name that is not a generic function. #[error("`{0}` is not a generic function and cannot take type arguments")] NotGeneric(Var), @@ -365,6 +371,24 @@ impl Context { self.clone() } + /// A binding that can be used one time, and that is used here but + /// was not used in `before` (the first one by name, if there are 2). + fn consumed_since(&self, before: &Context) -> Option { + let unused_before = |name: &Var, entry: &CtxEntry| { + before + .vars + .get(name) + .is_some_and(|old| old.id == entry.id && !old.used) + }; + self.vars + .iter() + .filter(|(name, entry)| { + entry.forbids_reuse() && entry.used && unused_before(name, entry) + }) + .map(|(name, _)| name.clone()) + .min() + } + /// Check that two contexts agree on linear variable usage. pub fn check_branch_agreement(&self, other: &Context) -> Result<(), TypeError> { for (name, entry) in &self.vars { @@ -1823,8 +1847,16 @@ impl TypeChecker { } if let Some(guard) = &arm.guard { + // A false guard gives the value to the next arm, and that + // arm is checked from the state after the scrutinee. So + // the guard must leave each use-once binding as it found + // it: it can read or borrow one, not consume it. + let before = self.ctx.snapshot(); let guard_ty = self.check(guard)?; self.unify(guard.span, &Ty::Base(BaseTy::Bool), &guard_ty)?; + if let Some(name) = self.ctx.consumed_since(&before) { + return Err(self.at(guard.span, TypeError::GuardConsumesLinear(name))); + } } let body_ty = self.check(&arm.body)?;