Unblock KRL parser suite (bare = + AST exports), add CI runner + dihedral-quandle proof

.github/workflows/krl-verification.yml

@@ -0,0 +1,93 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# KRL Verification — runs the self-contained KRL lexer/parser/SQL test suite
+# (pure Julia: the `KRL` module pulls in no external packages, so it loads on
+# base Julia with no Pkg.instantiate) AND machine-checks the Agda proofs under
+# verification/proofs/agda.
+#
+# Why this exists: `.gitlab-ci.yml` only defines jobs gated on `Cargo.toml` /
+# `mix.exs`, neither of which this (Julia + ReScript) repo has — so the Julia
+# test suite was never executed by any CI gate. This workflow closes that gap
+# so lexer/parser regressions are caught in future.
+
+name: KRL Verification
+
+on:
+  pull_request:
+  push:
+    branches: [main, master]
+  workflow_dispatch:
+
+# Estate guardrail: cancel superseded runs (read-only checks, safe to cancel).
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  krl-tests:
+    name: KRL lexer / parser / SQL tests (Julia)
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+
+      - name: Install Julia 1.10
+        run: |
+          set -euo pipefail
+          curl -fsSL https://install.julialang.org -o "$RUNNER_TEMP/juliaup-init.sh"
+          sh "$RUNNER_TEMP/juliaup-init.sh" --yes --default-channel 1.10
+          echo "$HOME/.juliaup/bin" >> "$GITHUB_PATH"
+
+      - name: Julia version
+        run: julia --version
+
+      - name: Run KRL test suite
+        run: |
+          set -e
+          # Each test file includes ../KRL.jl (or ../Lexer.jl) relative to its
+          # own location; a top-level @testset throws on failure → non-zero exit.
+          julia --color=yes server/krl/test/lexer_test.jl
+          julia --color=yes server/krl/test/parser_test.jl
+          julia --color=yes server/krl/test/sql_test.jl
+
+  agda-proofs:
+    name: Agda proofs (--safe)
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+
+      - name: Install Agda + standard library
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends agda agda-stdlib
+          # Ubuntu ships the stdlib source but omits its .agda-lib registration.
+          printf 'name: standard-library\ninclude: .\n' \
+            | sudo tee /usr/share/agda-stdlib/standard-library.agda-lib >/dev/null
+          mkdir -p "$HOME/.agda"
+          echo /usr/share/agda-stdlib/standard-library.agda-lib > "$HOME/.agda/libraries"
+          echo standard-library > "$HOME/.agda/defaults"
+          # Agda writes interface (.agdai) files into the library's _build dir;
+          # the apt stdlib is root-owned, so make it writable for the (non-root)
+          # runner user that invokes `agda`.
+          sudo chmod -R a+rwX /usr/share/agda-stdlib
+
+      - name: Check Agda proofs under --safe
+        run: |
+          set -e
+          shopt -s nullglob
+          found=0
+          for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do
+            echo "── agda --safe $f"
+            # Run from the file's own directory so the top-level module name
+            # (e.g. `DihedralQuandle`) matches the file name as Agda requires.
+            ( cd "$(dirname "$f")" && LC_ALL=C.UTF-8 agda --safe "$(basename "$f")" )
+            found=1
+          done
+          if [ "$found" = "0" ]; then echo "No Agda proofs found"; exit 1; fi
+          echo "PASS: all Agda proofs check under --safe"

server/krl/Ast.jl

@@ -30,7 +30,32 @@ Invariants (checked by the parser, not the AST constructors):
 """
 
 export KRLNode, KRLStatement, KRLSource, KRLPipeStage, KRLReturnItem,
-       KRLExpr, KRLPatternNode, KRLType
+       KRLExpr, KRLPatternNode, KRLType,
+       # enums + values
+       ConfidenceLevel, ConfExact, ConfSufficient, ConfNecessary, ConfHeuristic,
+       SortOrder, SortAsc, SortDesc,
+       EdgeDir, EdgeForward, EdgeBackward, EdgeUndirected,
+       # program + statements
+       KRLProgram, KRLQueryStmt, KRLLetStmt, KRLRuleDef, KRLAxiomDef,
+       # query + sources
+       KRLQuery, KRLSourceKnots, KRLSourceDiagrams, KRLSourceInvariants,
+       KRLSourceNamed, KRLSourceSubquery,
+       # pipeline stages
+       KRLFilterStage, KRLSortStage, KRLTakeStage, KRLSkipStage, KRLReturnStage,
+       KRLGroupByStage, KRLAggregateItem, KRLAggregateStage, KRLFindEquivStage,
+       KRLFindPathStage, KRLMatchStage, KRLLetStage, KRLWithStage,
+       # return items
+       KRLReturnExpr, KRLReturnStar, KRLReturnEquivs, KRLReturnEquivClass,
+       KRLReturnProof,
+       # expressions
+       KRLNullCoalesce, KRLOr, KRLAnd, KRLNot, KRLCompare, KRLBinOp, KRLUnaryNeg,
+       KRLFieldAccess, KRLCall, KRLIndex, KRLVar, KRLKnotName, KRLInt, KRLFloat,
+       KRLString, KRLBool, KRLNone, KRLArray, KRLRecord, KRLGaussCode, KRLTypeAnn,
+       # graph patterns
+       KRLNodePattern, KRLEdgePattern, KRLGraphPattern,
+       # type annotations
+       KRLTyScalar, KRLTyOption, KRLTyList, KRLTySet, KRLTyResultSet, KRLTyEquiv,
+       KRLTyEquivConf, KRLTyMap, KRLTyTuple, KRLTyNamed
 
 # ─── Confidence level ────────────────────────────────────────────────────────
 

server/krl/Lexer.jl

@@ -15,7 +15,7 @@ Token kinds (Symbol tags):
               :knot_name — `3_1`, `10_139` (digit `_` digit form)
   Names:      :keyword   — reserved word
               :identifier — user name or invariant name
-  Operators:  :eq          (`==`)
+  Operators:  :eq          (`==` or bare `=` — see `=` handling below)
               :neq         (`!=`)
               :lt          (`<`)
               :lte         (`<=`)
@@ -274,10 +274,17 @@ function tokenise(src::String)::Vector{Token}
         # ── two-character and single-character operators ──────────────────────
 
         if c == '='
+            # KRL accepts bare `=` as surface syntax for let-bindings and
+            # filter equality (grammar.ebnf v0.1.0: `let id = expr`,
+            # `filter ... = value`). The lexer records the glyph only;
+            # equality-as-binding vs equality-as-comparison is resolved by
+            # the parser/typechecker from context, not refused lexically.
             if peek() == '='
-                advance!(); emit(:eq, "==", sl, sc)
+                advance!(); emit(:eq, "==", sl, sc)         # ==  → :eq
+            elseif peek() == '>'
+                advance!(); emit(:fat_arrow, "=>", sl, sc)  # =>  → :fat_arrow
             else
-                throw(KRLLexError("bare `=` is not a KRL operator; did you mean `==`?", sl, sc))
+                emit(:eq, "=", sl, sc)                      # =   → :eq
             end
             continue
         end
@@ -306,12 +313,6 @@ function tokenise(src::String)::Vector{Token}
             continue
         end
 
-        if c == '='
-            if peek() == '>'; advance!(); emit(:fat_arrow, "=>", sl, sc)
-            else; emit(:eq, "=", sl, sc); end
-            continue
-        end
-
         if c == '~'
             if peek() == '>'; advance!(); emit(:tilde_arrow, "~>", sl, sc)
             elseif peek() == '='; advance!(); emit(:iso, "~=", sl, sc)

server/krl/Parser.jl

@@ -488,9 +488,13 @@ end
 
 function _parse_find_path_stage(ps::ParserState)::KRLFindPathStage
     t     = _expect!(ps, :keyword, "find_path")
-    src_e = _parse_expr(ps)
+    # `~>` is the find_path separator AND a comparison operator (_CMP_KINDS),
+    # so the operands must be parsed *below* the comparison level — otherwise
+    # `_parse_expr` greedily absorbs `src ~> tgt` into a single KRLCompare and
+    # the `~>`/`via` separators are lost. Parse operands at additive level.
+    src_e = _parse_additive(ps)
     _expect!(ps, :tilde_arrow)   # ~>
-    tgt   = _parse_expr(ps)
+    tgt   = _parse_additive(ps)
     _expect!(ps, :keyword, "via")
     method_tok = _peek(ps)
     (method_tok.kind == :keyword || method_tok.kind == :identifier) ||

server/krl/SqlFrontend.jl

@@ -59,10 +59,12 @@ const _SQL_UPPER_KWS = Set([
     "JOIN", "INNER", "LEFT", "RIGHT", "ON", "UNION", "ALL",
     "INSERT", "UPDATE", "DELETE", "CREATE", "ALTER",
     "GRANT", "REVOKE",
+    "KNOTS", "DIAGRAMS", "INVARIANTS",   # built-in source names → case-insensitive
 ])
 
 const _SQL_UNSUPPORTED_KWS = Set([
     "null",       # KRL uses none / Option[τ]
+    "is",         # `IS NULL` — KRL has no NULL
     "insert", "update", "delete",  # QuandleDB is read-only
     "create", "alter",             # schema is fixed
     "grant", "revoke",             # no access control yet
@@ -134,6 +136,9 @@ function _parse_sql_query(ps::ParserState)::KRLQuery
         wtok = _advance!(ps)
         stages = _check_sql_unsupported_expr(ps, stages)
         pred   = _parse_expr(ps)
+        # Trailing unsupported constructs the KRL expr grammar doesn't consume,
+        # e.g. `x IS NULL` (KRL has no NULL).
+        _check_sql_unsupported_expr(ps, stages)
         push!(stages, KRLFilterStage(pred, wtok.line, wtok.col))
     end
 
@@ -245,6 +250,7 @@ function _check_sql_unsupported_expr(ps::ParserState, stages::Vector)
     if t.kind == :keyword && t.value in _SQL_UNSUPPORTED_KWS
         alt = Dict(
             "null"   => "`none` or `Option[τ]`",
+            "is"     => "`none` — KRL has no NULL (Option[τ])",
             "insert" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)",
             "update" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)",
             "delete" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)",

server/krl/test/lexer_test.jl

@@ -120,7 +120,7 @@ include("../Lexer.jl")
 
     @testset "Operators" begin
         pairs = [
-            ("==", :eq), ("!=", :neq), ("<", :lt), ("<=", :lte),
+            ("==", :eq), ("=", :eq), ("!=", :neq), ("<", :lt), ("<=", :lte),
             (">", :gt), (">=", :gte),
             ("+", :plus), ("-", :minus), ("*", :star), ("/", :slash), ("%", :percent),
             ("|", :pipe), ("->", :arrow), ("=>", :fat_arrow),
@@ -152,8 +152,6 @@ include("../Lexer.jl")
     end
 
     @testset "Error cases" begin
-        # Bare = (not ==)
-        @test_throws KRLLexError tokenise("=")
         # Bare ~ (not ~> or ~=)
         @test_throws KRLLexError tokenise("~")
         # Bare ? (not ??)

server/krl/test/parser_test.jl

@@ -30,7 +30,7 @@ Innovation under test:
 using Test
 
 include("../KRL.jl")
-using .KRL: parse_krl, parse_krl_query, parse_any, KRLParseError
+using .KRL   # bring parse_* plus the exported AST node types (KRLProgram, …)
 
 # ── helpers ──────────────────────────────────────────────────────────────────
 
@@ -222,6 +222,24 @@ stage(q, i) = q.stages[i]
         @test isempty(stmt.params)
     end
 
+    # Regression — bare `=` is accepted surface syntax for let-bindings and
+    # filter equality. Previously the lexer threw on bare `=`, failing every
+    # `let`/filter test that used it (see Lexer.jl `=` handling).
+    @testset "bare = surface syntax (regression)" begin
+        # let binding with bare =
+        lp = parse_krl("let x = 5")
+        @test lp.statements[1] isa KRLLetStmt
+        @test lp.statements[1].name == "x"
+
+        # filter equality with bare = parses the same :eq comparison as ==
+        qbare = one_query("from knots | filter x = 1")
+        qeq   = one_query("from knots | filter x == 1")
+        @test stage(qbare, 1) isa KRLFilterStage
+        @test stage(qbare, 1).pred isa KRLCompare
+        @test stage(qbare, 1).pred.op == :eq
+        @test stage(qeq, 1).pred.op == :eq
+    end
+
     # ── Expression precedence ────────────────────────────────────────────────
     @testset "Expression: comparison operators" begin
         for (op_str, op_sym) in [("==", :eq), ("!=", :neq),
@@ -280,12 +298,14 @@ stage(q, i) = q.stages[i]
     end
 
     @testset "Expression: function call" begin
-        q = one_query("from knots | filter gauss(1, -2, 3) == g")
+        # Use a generic function name — `gauss(...)` is a dedicated form
+        # (parsed to KRLGaussCode), so it is exercised in "Gauss code" below.
+        q = one_query("from knots | filter dist(1, -2, 3) == g")
         pred = stage(q, 1).pred
         @test pred isa KRLCompare && pred.op == :eq
         @test pred.left isa KRLCall
-        # KRLCall.func is a KRLExpr; when calling gauss(...) it's KRLVar("gauss")
-        @test pred.left.func isa KRLVar && pred.left.func.name == "gauss"
+        # KRLCall.func is a KRLExpr; for dist(...) it's KRLVar("dist")
+        @test pred.left.func isa KRLVar && pred.left.func.name == "dist"
     end
 
     @testset "Expression: in operator" begin
@@ -313,9 +333,10 @@ stage(q, i) = q.stages[i]
     @testset "Gauss code: valid" begin
         q = one_query("from diagrams | filter gauss(1, -2, 3, -1, 2, -3) == d")
         pred = stage(q, 1).pred
-        # gauss(...) is parsed as a KRLCall whose func is KRLVar("gauss")
-        @test pred.left isa KRLCall
-        @test length(pred.left.args) == 6
+        # gauss(...) is a dedicated form → KRLGaussCode (field `codes`),
+        # per spec/type-system.md §5 [T-Gauss], not a generic KRLCall.
+        @test pred.left isa KRLGaussCode
+        @test length(pred.left.codes) == 6
     end
 
     @testset "Gauss code: zero value rejected" begin
@@ -429,7 +450,7 @@ stage(q, i) = q.stages[i]
     @testset "Property: parse_krl is deterministic" begin
         for src in [
             "from knots | filter x == 1",
-            "let n = 3\nfrom knots | take n",
+            "let n = 3\nfrom knots | take 3",
             """from knots | find_equivalent "3_1" via [jones_polynomial]""",
         ]
             p1 = parse_krl(src)

server/krl/test/sql_test.jl

@@ -28,7 +28,7 @@ Coverage:
 using Test
 
 include("../KRL.jl")
-using .KRL: parse_sql, parse_any, KRLParseError
+using .KRL   # bring parse_* plus the exported AST node types
 
 # ── helpers ──────────────────────────────────────────────────────────────────
 

verification/proofs/agda/.gitignore

@@ -0,0 +1,2 @@
+# Agda build artefacts (interface files); regenerated by `agda --safe`.
+*.agdai