From fecd3e4b0ddc4e6a7dfb587424a4cba4846dd9c8 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:46:32 +0000 Subject: [PATCH] maude: order-sorted least-sort inference (14 tests, 250 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/sorts.sx — mau/term-sort computes the least sort of a term (smallest result sort among op declarations whose arg sorts the actuals satisfy modulo subsorting); overloaded f(1)=NzNat vs f(s 0)=Nat. mau/has-sort? for membership-style checks. Answers the plan's order-sorted substrate question. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 7 +-- lib/maude/scoreboard.md | 3 +- lib/maude/sorts.sx | 87 ++++++++++++++++++++++++++++++++++++++ lib/maude/tests/sorts.sx | 53 +++++++++++++++++++++++ plans/maude-on-sx.md | 6 +++ 6 files changed, 154 insertions(+), 4 deletions(-) create mode 100644 lib/maude/sorts.sx create mode 100644 lib/maude/tests/sorts.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index d1a48e30..c9aa1d3e 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -8,6 +8,7 @@ PRELOADS=( lib/guest/pratt.sx lib/maude/term.sx lib/maude/parser.sx + lib/maude/sorts.sx lib/maude/reduce.sx lib/maude/matching.sx lib/maude/conditional.sx @@ -27,6 +28,7 @@ SUITES=( "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!)" + "sorts:lib/maude/tests/sorts.sx:(mau-sorts-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/scoreboard.json b/lib/maude/scoreboard.json index 6c88479a..aaa8c406 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 236, + "total_passed": 250, "total_failed": 0, - "total": 236, + "total": 250, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -10,6 +10,7 @@ {"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":"sorts","passed":14,"failed":0,"total":14}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, @@ -17,5 +18,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:43:54+00:00" + "generated": "2026-06-07T15:46:14+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 61abe2cc..5fa4b499 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**236 / 236 passing** (0 failure(s)). +**250 / 250 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -10,6 +10,7 @@ | conditional | 19 | 19 | ok | | owise | 8 | 8 | ok | | gather | 7 | 7 | ok | +| sorts | 14 | 14 | ok | | rewrite | 21 | 21 | ok | | searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | diff --git a/lib/maude/sorts.sx b/lib/maude/sorts.sx new file mode 100644 index 00000000..6f50308b --- /dev/null +++ b/lib/maude/sorts.sx @@ -0,0 +1,87 @@ +;; lib/maude/sorts.sx — order-sorted least-sort inference. +;; +;; Order-sorted signatures: subsorts induce a partial order on sorts, and an +;; overloaded operator can have several declarations. The LEAST SORT of a term +;; is the smallest result sort among the operator declarations whose argument +;; sorts the actual arguments satisfy (modulo subsorting). This is what lets +;; `f(1)` be a NzNat while `f(s 0)` is only a Nat when f is declared at both. +;; +;; mau/term-sort M T -> least sort of T (string, "?" if unknown) +;; mau/has-sort? M T SORT -> does T's least sort fit under SORT? + +(define + mau/arg-sorts-ok? + (fn + (m argsorts declared) + (cond + ((and (empty? argsorts) (empty? declared)) true) + ((or (empty? argsorts) (empty? declared)) false) + ((mau/sort<=? m (first argsorts) (first declared)) + (mau/arg-sorts-ok? m (rest argsorts) (rest declared))) + (else false)))) + +(define + mau/matching-ops + (fn + (m name argsorts) + (filter + (fn + (op) + (and + (= (len (get op :arity)) (len argsorts)) + (mau/arg-sorts-ok? m argsorts (get op :arity)))) + (mau/ops-named m name)))) + +(define + mau/least-loop + (fn + (m best rst) + (cond + ((empty? rst) best) + ((mau/sort<=? m (first rst) best) + (mau/least-loop m (first rst) (rest rst))) + (else (mau/least-loop m best (rest rst)))))) + +(define + mau/least-sort + (fn + (m sorts) + (if (empty? sorts) "?" (mau/least-loop m (first sorts) (rest sorts))))) + +(define + mau/result-sort + (fn + (m name argsorts) + (let + ((cands (mau/matching-ops m name argsorts))) + (if + (empty? cands) + (let + ((any (mau/ops-named m name))) + (if (empty? any) "?" (get (first any) :result))) + (mau/least-sort m (map (fn (op) (get op :result)) cands)))))) + +(define + mau/term-sort + (fn + (m t) + (cond + ((mau/var? t) (mau/vsort t)) + ((mau/app? t) + (mau/result-sort + m + (mau/op t) + (map (fn (a) (mau/term-sort m a)) (mau/args t)))) + (else "?")))) + +(define + mau/term-sort-src + (fn (m src) (mau/term-sort m (mau/parse-term-in m src)))) + +(define + mau/has-sort? + (fn (m t sort) (mau/sort<=? m (mau/term-sort m t) sort))) + +(define + mau/has-sort-src? + (fn (m src sort) (mau/has-sort? m (mau/parse-term-in m src) sort))) diff --git a/lib/maude/tests/sorts.sx b/lib/maude/tests/sorts.sx new file mode 100644 index 00000000..ac2b113f --- /dev/null +++ b/lib/maude/tests/sorts.sx @@ -0,0 +1,53 @@ +;; lib/maude/tests/sorts.sx — order-sorted least-sort inference. + +(define mso-pass 0) +(define mso-fail 0) +(define mso-failures (list)) + +(define + mso-check! + (fn + (name got expected) + (if + (= got expected) + (set! mso-pass (+ mso-pass 1)) + (do + (set! mso-fail (+ mso-fail 1)) + (append! + mso-failures + (str name " expected: " expected " got: " got)))))) + +(define + mso-m + (mau/parse-module + "fmod NUMS is\n sorts Zero NzNat Nat .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n op 0 : -> Zero .\n op 1 : -> NzNat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op p : NzNat -> NzNat .\n op f : Nat -> Nat .\n op f : NzNat -> NzNat .\nendfm")) + +;; constants take their declared result sort +(mso-check! "sort-zero" (mau/term-sort-src mso-m "0") "Zero") +(mso-check! "sort-one" (mau/term-sort-src mso-m "1") "NzNat") + +;; application: arg subsort of declared domain +(mso-check! "sort-s0" (mau/term-sort-src mso-m "s 0") "Nat") +(mso-check! "sort-plus" (mau/term-sort-src mso-m "0 + 1") "Nat") +(mso-check! "sort-p" (mau/term-sort-src mso-m "p(1)") "NzNat") + +;; variable keeps its sort +(mso-check! "sort-var" (mau/term-sort mso-m (mau/var "X" "Nat")) "Nat") + +;; LEAST sort under overloading: f(1) fits both f decls -> the smaller, NzNat +(mso-check! "least-f-1" (mau/term-sort-src mso-m "f(1)") "NzNat") +;; f(s 0): s 0 is Nat, only fits f : Nat -> Nat +(mso-check! "least-f-s0" (mau/term-sort-src mso-m "f(s 0)") "Nat") +;; nested: f(f(1)) -> f(NzNat) -> NzNat +(mso-check! "least-nested" (mau/term-sort-src mso-m "f(f(1))") "NzNat") + +;; membership-style sort checks +(mso-check! "has-zero-nat" (mau/has-sort-src? mso-m "0" "Nat") true) +(mso-check! "has-one-nat" (mau/has-sort-src? mso-m "1" "Nat") true) +(mso-check! "has-zero-not-nznat" (mau/has-sort-src? mso-m "0" "NzNat") false) +(mso-check! "has-refl" (mau/has-sort-src? mso-m "1" "NzNat") true) + +;; unknown operator -> "?" +(mso-check! "sort-unknown" (mau/term-sort mso-m (mau/const "ghost")) "?") + +(define mau-sorts-tests-run! (fn () {:failures mso-failures :total (+ mso-pass mso-fail) :passed mso-pass :failed mso-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 4f723ea9..bb6a5839 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -112,6 +112,12 @@ 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] Order-sorted least-sort inference (`lib/maude/sorts.sx`) — `mau/term-sort` + computes the least sort of a term: the smallest result sort among the op + declarations whose argument sorts the actual args satisfy (modulo subsorting), + so an overloaded `f(1)` is `NzNat` but `f(s 0)` is `Nat`. `mau/has-sort?` + for membership-style checks. Answers the plan's substrate question — order- + sorted signatures fit cleanly. 14 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