From 3bb4886f0f80afe7d3a6dfc23cb374c43d02ad41 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:44:25 +0000 Subject: [PATCH] maude: gather / parse-time associativity for cons lists (7 tests, 236 total) Infix ops parse left (default / gather (E e)) or right (gather (e E)) per the gather attribute, so _:_ [gather (e E)] reads a : b : c as right-nested. Full insertion sort now runs over bare cons lists with no parentheses. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 1 + lib/maude/parser.sx | 42 ++++++++++++++++++++---- lib/maude/scoreboard.json | 7 ++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/gather.sx | 66 ++++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 4 +++ 6 files changed, 112 insertions(+), 11 deletions(-) create mode 100644 lib/maude/tests/gather.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 51249a66..d1a48e30 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -26,6 +26,7 @@ SUITES=( "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)" + "gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx index 13cf03bf..e6db3558 100644 --- a/lib/maude/parser.sx +++ b/lib/maude/parser.sx @@ -19,7 +19,8 @@ ;; Terms: prefix application f(a,b) (op name may contain underscores, e.g. ;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix ;; _+_ written `X + Y`, parsed by precedence climbing over a table built -;; from the op declarations. +;; from the op declarations. Infix associativity follows `gather`: (E e)=left +;; (default), (e E)=right (e.g. cons _:_), so `a : b : c` parses right-nested. ;; ---------- tokenizer ---------- @@ -173,6 +174,21 @@ ((p (get (get op :attrs) :prec))) (if (= p nil) (mau/default-prec (get form :kind)) p)))) +;; parse associativity from a gather spec: (E e)=left, (e E)=right. +(define + mau/gather-assoc + (fn + (attrs) + (let + ((g (get attrs :gather))) + (if + (or (= g nil) (< (len g) 2)) + "left" + (cond + ((= (nth g 1) "E") "right") + ((= (nth g 0) "E") "left") + (else "left")))))) + (define mau/build-infix-table (fn @@ -187,7 +203,11 @@ (if (= (get form :kind) "infix") (cons - (list (get form :token) (mau/op-prec op form) (get op :name)) + (list + (get form :token) + (mau/op-prec op form) + (get op :name) + (mau/gather-assoc (get op :attrs))) rest-tbl) rest-tbl)))))) @@ -310,11 +330,13 @@ (do (tadv!) (let - ((rhs (parse-expr (+ lbp 1)))) - (climb - (mau/app - (nth entry 2) - (list acc rhs)))))))))))) + ((rbp (if (= (nth entry 3) "right") lbp (+ lbp 1)))) + (let + ((rhs (parse-expr rbp))) + (climb + (mau/app + (nth entry 2) + (list acc rhs))))))))))))) (climb lhs)))) (parse-expr 0)))) @@ -398,6 +420,12 @@ (do (dict-set! acc :label (nth ts 1)) (loop (mau/drop ts 2)))) + ((= (first ts) "gather") + (let + ((after2 (mau/drop ts 2))) + (do + (dict-set! acc :gather (mau/take-until after2 ")")) + (loop (rest (mau/drop-until after2 ")")))))) (else (loop (rest ts)))))) (do (loop toks) acc)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 7cd864a9..6c88479a 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,14 +1,15 @@ { "lang": "maude", - "total_passed": 229, + "total_passed": 236, "total_failed": 0, - "total": 229, + "total": 236, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"owise","passed":8,"failed":0,"total":8}, + {"name":"gather","passed":7,"failed":0,"total":7}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, @@ -16,5 +17,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:39:50+00:00" + "generated": "2026-06-07T15:43:54+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index c092d674..61abe2cc 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**229 / 229 passing** (0 failure(s)). +**236 / 236 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -9,6 +9,7 @@ | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | | owise | 8 | 8 | ok | +| gather | 7 | 7 | ok | | rewrite | 21 | 21 | ok | | searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | diff --git a/lib/maude/tests/gather.sx b/lib/maude/tests/gather.sx new file mode 100644 index 00000000..453743c1 --- /dev/null +++ b/lib/maude/tests/gather.sx @@ -0,0 +1,66 @@ +;; lib/maude/tests/gather.sx — gather / parse-time associativity. + +(define mga-pass 0) +(define mga-fail 0) +(define mga-failures (list)) + +(define + mga-check! + (fn + (name got expected) + (if + (= got expected) + (set! mga-pass (+ mga-pass 1)) + (do + (set! mga-fail (+ mga-fail 1)) + (append! + mga-failures + (str name " expected: " expected " got: " got)))))) + +(define + mga-m + (mau/parse-module + "fmod L is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op _+_ : Nat Nat -> Nat .\n op _-_ : Nat Nat -> Nat [gather (E e)] .\n vars X Y : Nat .\nendfm")) + +;; cons is right-associative: a : b : c == a : (b : c) +(mga-check! + "cons-right" + (mau/term->str (mau/parse-term-in mga-m "0 : s 0 : nil")) + "_:_(0, _:_(s_(0), nil))") +;; + has no gather -> default left-assoc +(mga-check! + "plus-left" + (mau/term->str (mau/parse-term-in mga-m "X + Y + X")) + "_+_(_+_(X, Y), X)") +;; explicit (E e) is left +(mga-check! + "minus-left" + (mau/term->str (mau/parse-term-in mga-m "X - Y - X")) + "_-_(_-_(X, Y), X)") +;; gather attr recorded +(mga-check! + "gather-recorded" + (get (get (first (mau/ops-named mga-m "_:_")) :attrs) :gather) + (list "e" "E")) + +;; ---- full insertion sort over BARE cons lists (no parens needed) ---- + +(define + mga-sort + (mau/parse-module + "fmod SORT is\n sorts Nat List Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op insert : Nat List -> List .\n op sort : List -> List .\n vars M N : Nat .\n var L : List .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n eq insert(N, nil) = N : nil .\n ceq insert(N, M : L) = N : M : L if N <= M = true .\n ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n eq sort(nil) = nil .\n eq sort(N : L) = insert(N, sort(L)) .\nendfm")) + +(mga-check! + "sort-bare" + (mau/creduce->str mga-sort "sort(s s s 0 : s 0 : s s 0 : nil)") + "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))") +(mga-check! + "sort-bare-5" + (mau/creduce->str mga-sort "sort(s s 0 : 0 : s 0 : nil)") + "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))") +(mga-check! + "insert-bare" + (mau/creduce->str mga-sort "insert(s 0, 0 : s s 0 : nil)") + "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))") + +(define mau-gather-tests-run! (fn () {:failures mga-failures :total (+ mga-pass mga-fail) :passed mga-pass :failed mga-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 8c69c575..4f723ea9 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -112,6 +112,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / `mau/search-length` return the shortest sequence of states start..goal (the solution moves), not just yes/no. 8 tests. +- [x] `gather` / parse-time associativity — infix ops parse left (default, + `(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]` + reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons + lists (no parens). 7 tests. - [x] `owise` equations — parser now reads trailing eq attributes (`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass (ordinary equations first, owise last), so an owise catch-all fires only when