From 9f87206949f6c83051d5247f9dc798bf744279f4 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 14:43:02 +0000 Subject: [PATCH] =?UTF-8?q?maude:=20Phase=201=20parser=20=E2=80=94=20fmod/?= =?UTF-8?q?mod=20modules,=20signatures,=20mixfix=20terms=20(65=20tests)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Term representation (lib/maude/term.sx) plus a module parser (lib/maude/parser.sx) consuming lib/guest/lex + pratt: - whitespace+bracket tokenizer (--- / *** comments) - mixfix classification (split op names on _): infix/prefix/postfix/const - precedence-climbing term parser over a pratt table built from op decls - fmod/mod ... endfm/endm with sort/subsort/op/var/eq/ceq/rl/crl - transitive subsort hierarchy + operator overloading queries Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 15 + lib/maude/conformance.sh | 3 + lib/maude/parser.sx | 673 +++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 10 + lib/maude/scoreboard.md | 7 + lib/maude/term.sx | 114 +++++++ lib/maude/tests/parse.sx | 250 ++++++++++++++ plans/maude-on-sx.md | 27 +- 8 files changed, 1093 insertions(+), 6 deletions(-) create mode 100644 lib/maude/conformance.conf create mode 100755 lib/maude/conformance.sh create mode 100644 lib/maude/parser.sx create mode 100644 lib/maude/scoreboard.json create mode 100644 lib/maude/scoreboard.md create mode 100644 lib/maude/term.sx create mode 100644 lib/maude/tests/parse.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf new file mode 100644 index 00000000..4fccc519 --- /dev/null +++ b/lib/maude/conformance.conf @@ -0,0 +1,15 @@ +# Maude conformance config — sourced by lib/guest/conformance.sh. + +LANG_NAME=maude +MODE=dict + +PRELOADS=( + lib/guest/lex.sx + lib/guest/pratt.sx + lib/maude/term.sx + lib/maude/parser.sx +) + +SUITES=( + "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" +) diff --git a/lib/maude/conformance.sh b/lib/maude/conformance.sh new file mode 100755 index 00000000..cff21bc1 --- /dev/null +++ b/lib/maude/conformance.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# Thin wrapper — see lib/guest/conformance.sh and lib/maude/conformance.conf. +exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx new file mode 100644 index 00000000..0196e9fc --- /dev/null +++ b/lib/maude/parser.sx @@ -0,0 +1,673 @@ +;; lib/maude/parser.sx — Maude module parser. +;; +;; Consumes lib/guest/lex.sx (whitespace classes) and lib/guest/pratt.sx +;; (operator-table lookup), plus lib/maude/term.sx (term constructors). +;; +;; Maude tokens are whitespace-delimited words plus the bracketing chars +;; ( ) [ ] { } , — so an operator name like _+_ or s_ or if_then_else_fi is a +;; single token. Statements end at a whitespace-delimited "." token. +;; +;; Grammar handled here: +;; (fmod|mod) NAME is ... (endfm|endm) +;; sort/sorts NAMES . +;; subsort/subsorts A B < C < D . +;; op/ops NAMES : ARITY -> RESULT [ATTRS] . +;; var/vars NAMES : SORT . +;; eq LHS = RHS . ceq LHS = RHS if COND . +;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND . +;; +;; 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. + +;; ---------- tokenizer ---------- + +(define + mau/special-char? + (fn + (c) + (or + (= c "(") + (= c ")") + (= c "[") + (= c "]") + (= c "{") + (= c "}") + (= c ",")))) + +(define + mau/tokenize + (fn + (src) + (let + ((toks (list)) (pos 0) (n (len src))) + (define + peekc + (fn (o) (if (< (+ pos o) n) (nth src (+ pos o)) nil))) + (define curc (fn () (peekc 0))) + (define adv! (fn (k) (set! pos (+ pos k)))) + (define + at-comment? + (fn + () + (or + (and + (= (curc) "-") + (= (peekc 1) "-") + (= (peekc 2) "-")) + (and + (= (curc) "*") + (= (peekc 1) "*") + (= (peekc 2) "*"))))) + (define + skip-line! + (fn + () + (when + (and (< pos n) (not (= (curc) "\n"))) + (do (adv! 1) (skip-line!))))) + (define + read-word! + (fn + (start) + (do + (when + (and + (< pos n) + (not (lex-whitespace? (curc))) + (not (mau/special-char? (curc)))) + (do (adv! 1) (read-word! start))) + (slice src start pos)))) + (define + scan! + (fn + () + (cond + ((>= pos n) nil) + ((lex-whitespace? (curc)) (do (adv! 1) (scan!))) + ((at-comment?) (do (skip-line!) (scan!))) + ((mau/special-char? (curc)) + (do (append! toks (curc)) (adv! 1) (scan!))) + (else (do (append! toks (read-word! pos)) (scan!)))))) + (scan!) + toks))) + +;; ---------- list helpers ---------- + +(define + mau/take + (fn + (xs k) + (if + (or (= k 0) (empty? xs)) + (list) + (cons (first xs) (mau/take (rest xs) (- k 1)))))) + +(define + mau/drop + (fn + (xs k) + (if + (or (= k 0) (empty? xs)) + xs + (mau/drop (rest xs) (- k 1))))) + +(define + mau/append2 + (fn + (xs ys) + (if (empty? xs) ys (cons (first xs) (mau/append2 (rest xs) ys))))) + +(define + mau/take-until + (fn + (xs tok) + (if + (or (empty? xs) (= (first xs) tok)) + (list) + (cons (first xs) (mau/take-until (rest xs) tok))))) + +(define + mau/drop-until + (fn + (xs tok) + (cond + ((empty? xs) (list)) + ((= (first xs) tok) xs) + (else (mau/drop-until (rest xs) tok))))) + +;; ---------- mixfix classification ---------- + +(define + mau/op-form + (fn + (name) + (let + ((parts (split name "_"))) + (cond + ((= (len parts) 1) {:kind :const :token name}) + ((and (= (len parts) 3) (= (nth parts 0) "") (= (nth parts 2) "") (not (= (nth parts 1) ""))) + {:kind :infix :token (nth parts 1)}) + ((and (= (len parts) 2) (not (= (nth parts 0) "")) (= (nth parts 1) "")) + {:kind :prefix :token (nth parts 0)}) + ((and (= (len parts) 2) (= (nth parts 0) "") (not (= (nth parts 1) ""))) + {:kind :postfix :token (nth parts 1)}) + (else {:kind :mixfix :token name}))))) + +(define + mau/default-prec + (fn + (kind) + (cond + ((= kind "infix") 41) + ((= kind "prefix") 15) + ((= kind "postfix") 15) + (else 0)))) + +(define + mau/op-prec + (fn + (op form) + (let + ((p (get (get op :attrs) :prec))) + (if (= p nil) (mau/default-prec (get form :kind)) p)))) + +(define + mau/build-infix-table + (fn + (ops) + (if + (empty? ops) + (list) + (let + ((op (first ops)) (rest-tbl (mau/build-infix-table (rest ops)))) + (let + ((form (mau/op-form (get op :name)))) + (if + (= (get form :kind) "infix") + (cons + (list (get form :token) (mau/op-prec op form) (get op :name)) + rest-tbl) + rest-tbl)))))) + +(define + mau/build-prefix-table + (fn + (ops) + (if + (empty? ops) + (list) + (let + ((op (first ops)) (rest-tbl (mau/build-prefix-table (rest ops)))) + (let + ((form (mau/op-form (get op :name)))) + (if + (= (get form :kind) "prefix") + (cons + (list (get form :token) (mau/op-prec op form) (get op :name)) + rest-tbl) + rest-tbl)))))) + +;; ---------- term parsing ---------- + +(define mau/has-colon? (fn (tok) (contains? tok ":"))) + +(define + mau/atom->term + (fn + (tok vars) + (cond + ((mau/has-colon? tok) + (let + ((parts (split tok ":"))) + (mau/var (nth parts 0) (nth parts 1)))) + ((not (= (get vars tok) nil)) (mau/var tok (get vars tok))) + (else (mau/const tok))))) + +(define + mau/parse-term + (fn + (toks grammar) + (let + ((ts toks) + (pos 0) + (n (len toks)) + (infix-tbl (get grammar :infix)) + (prefix-tbl (get grammar :prefix)) + (vars (get grammar :vars)) + (prefix-rbp 1000)) + (define tcur (fn () (if (< pos n) (nth ts pos) nil))) + (define + tpeek + (fn (o) (if (< (+ pos o) n) (nth ts (+ pos o)) nil))) + (define tadv! (fn () (set! pos (+ pos 1)))) + (define + parse-args + (fn + () + (if + (= (tcur) ")") + (do (tadv!) (list)) + (let + ((acc (list))) + (define + more + (fn + () + (do + (append! acc (parse-expr 0)) + (when (= (tcur) ",") (do (tadv!) (more)))))) + (do (more) (when (= (tcur) ")") (tadv!)) acc))))) + (define + parse-primary + (fn + () + (let + ((t (tcur))) + (cond + ((= t "(") + (do + (tadv!) + (let + ((e (parse-expr 0))) + (do (when (= (tcur) ")") (tadv!)) e)))) + ((not (= (pratt-op-lookup prefix-tbl t) nil)) + (let + ((entry (pratt-op-lookup prefix-tbl t))) + (do + (tadv!) + (let + ((operand (parse-expr prefix-rbp))) + (mau/app (nth entry 2) (list operand)))))) + ((= (tpeek 1) "(") + (let + ((name t)) + (do (tadv!) (tadv!) (mau/app name (parse-args))))) + (else (do (tadv!) (mau/atom->term t vars))))))) + (define + parse-expr + (fn + (minbp) + (let + ((lhs (parse-primary))) + (define + climb + (fn + (acc) + (let + ((t (tcur))) + (let + ((entry (if (= t nil) nil (pratt-op-lookup infix-tbl t)))) + (if + (= entry nil) + acc + (let + ((lbp (pratt-op-prec entry))) + (if + (< lbp minbp) + acc + (do + (tadv!) + (let + ((rhs (parse-expr (+ lbp 1)))) + (climb + (mau/app + (nth entry 2) + (list acc rhs)))))))))))) + (climb lhs)))) + (parse-expr 0)))) + +;; ---------- statement splitting ---------- + +(define + mau/split-statements + (fn + (toks) + (let + ((stmts (list)) (cur (list))) + (define + flush! + (fn + () + (when + (not (empty? cur)) + (do (append! stmts cur) (set! cur (list)))))) + (define + loop + (fn + (ts) + (cond + ((empty? ts) (flush!)) + ((= (first ts) ".") (do (flush!) (loop (rest ts)))) + (else (do (append! cur (first ts)) (loop (rest ts))))))) + (do (loop toks) stmts)))) + +(define + mau/split-groups + (fn + (toks) + (let + ((groups (list)) (cur (list))) + (define flush! (fn () (do (append! groups cur) (set! cur (list))))) + (define + loop + (fn + (ts) + (cond + ((empty? ts) (flush!)) + ((= (first ts) "<") (do (flush!) (loop (rest ts)))) + (else (do (append! cur (first ts)) (loop (rest ts))))))) + (do (loop toks) groups)))) + +;; ---------- attributes ---------- + +(define mau/strip-brackets (fn (toks) (mau/take-until (rest toks) "]"))) + +(define + mau/parse-attr-tokens + (fn + (toks) + (let + ((acc {})) + (define + loop + (fn + (ts) + (cond + ((empty? ts) nil) + ((= (first ts) "assoc") + (do (dict-set! acc :assoc true) (loop (rest ts)))) + ((= (first ts) "comm") + (do (dict-set! acc :comm true) (loop (rest ts)))) + ((or (= (first ts) "idem") (= (first ts) "idempotent")) + (do (dict-set! acc :idem true) (loop (rest ts)))) + ((= (first ts) "ctor") + (do (dict-set! acc :ctor true) (loop (rest ts)))) + ((= (first ts) "id:") + (do + (dict-set! acc :id (nth ts 1)) + (loop (mau/drop ts 2)))) + ((= (first ts) "prec") + (do + (dict-set! acc :prec (parse-number (nth ts 1))) + (loop (mau/drop ts 2)))) + (else (loop (rest ts)))))) + (do (loop toks) acc)))) + +(define + mau/parse-attrs + (fn + (toks) + (if + (or (empty? toks) (not (= (first toks) "["))) + {} + (mau/parse-attr-tokens (mau/strip-brackets toks))))) + +;; ---------- signature collection ---------- + +(define + mau/append-each! + (fn (acc xs) (for-each (fn (x) (append! acc x)) xs))) + +(define + mau/register-ops! + (fn + (ops names arity result attrs) + (for-each (fn (nm) (append! ops {:name nm :attrs attrs :arity arity :result result})) names))) + +(define + mau/each-set-var! + (fn + (vars names sort) + (for-each (fn (nm) (dict-set! vars nm sort)) names))) + +(define + mau/cross-append! + (fn + (acc g1 g2) + (for-each + (fn + (sub) + (for-each (fn (super) (append! acc (list sub super))) g2)) + g1))) + +(define + mau/add-subsort-chain! + (fn + (acc groups) + (when + (and (not (empty? groups)) (not (empty? (rest groups)))) + (do + (mau/cross-append! acc (first groups) (nth groups 1)) + (mau/add-subsort-chain! acc (rest groups)))))) + +(define + mau/add-subsorts! + (fn (acc body) (mau/add-subsort-chain! acc (mau/split-groups body)))) + +(define + mau/add-vars! + (fn + (vars body) + (let + ((names (mau/take-until body ":")) + (sort (first (rest (mau/drop-until body ":"))))) + (mau/each-set-var! vars names sort)))) + +(define + mau/add-ops! + (fn + (ops body) + (let + ((names (mau/take-until body ":")) + (afterc (rest (mau/drop-until body ":")))) + (let + ((arity (mau/take-until afterc "->")) + (aftera (rest (mau/drop-until afterc "->")))) + (let + ((result (first aftera)) + (attrs (mau/parse-attrs (mau/drop aftera 1)))) + (mau/register-ops! ops names arity result attrs)))))) + +(define + mau/collect-sig! + (fn + (stmts sorts subsorts ops vars) + (for-each + (fn + (s) + (let + ((head (first s)) (body (rest s))) + (cond + ((or (= head "sort") (= head "sorts")) + (mau/append-each! sorts body)) + ((or (= head "subsort") (= head "subsorts")) + (mau/add-subsorts! subsorts body)) + ((or (= head "op") (= head "ops")) (mau/add-ops! ops body)) + ((or (= head "var") (= head "vars")) (mau/add-vars! vars body)) + (else nil)))) + stmts))) + +;; ---------- equations / rules ---------- + +(define + mau/parse-cond + (fn + (toks grammar) + (if + (mau/member? "=" toks) + (let + ((l (mau/take-until toks "=")) + (r (rest (mau/drop-until toks "=")))) + {:lhs (mau/parse-term l grammar) :kind :eq :rhs (mau/parse-term r grammar)}) + {:kind :bool :term (mau/parse-term toks grammar)}))) + +(define + mau/parse-eq + (fn + (body grammar conditional?) + (let + ((lhs-toks (mau/take-until body "=")) + (after (rest (mau/drop-until body "=")))) + (if + conditional? + (let + ((rhs-toks (mau/take-until after "if")) + (cond-toks (rest (mau/drop-until after "if")))) + {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) + {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term after grammar)})))) + +(define + mau/strip-label + (fn + (body) + (if + (and (not (empty? body)) (= (first body) "[")) + (let + ((label (nth body 1)) (after (mau/drop body 3))) + (if + (and (not (empty? after)) (= (first after) ":")) + {:label label :rest (rest after)} + {:label label :rest after})) + {:label nil :rest body}))) + +(define + mau/parse-rule + (fn + (body grammar conditional?) + (let + ((b (mau/strip-label body))) + (let + ((label (get b :label)) (rest-toks (get b :rest))) + (let + ((lhs-toks (mau/take-until rest-toks "=>")) + (after (rest (mau/drop-until rest-toks "=>")))) + (if + conditional? + (let + ((rhs-toks (mau/take-until after "if")) + (cond-toks (rest (mau/drop-until after "if")))) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term after grammar)})))))) + +(define + mau/collect-rules! + (fn + (stmts grammar eqs rules) + (for-each + (fn + (s) + (let + ((head (first s)) (body (rest s))) + (cond + ((= head "eq") (append! eqs (mau/parse-eq body grammar false))) + ((= head "ceq") (append! eqs (mau/parse-eq body grammar true))) + ((= head "rl") + (append! rules (mau/parse-rule body grammar false))) + ((= head "crl") + (append! rules (mau/parse-rule body grammar true))) + (else nil)))) + stmts))) + +;; ---------- module assembly ---------- + +(define mau/make-grammar (fn (ops vars) {:prefix (mau/build-prefix-table ops) :ops ops :vars vars :infix (mau/build-infix-table ops)})) + +(define + mau/build-module + (fn + (kind name body) + (let + ((stmts (mau/split-statements body)) + (sorts (list)) + (subsorts (list)) + (ops (list)) + (vars {}) + (eqs (list)) + (rules (list))) + (mau/collect-sig! stmts sorts subsorts ops vars) + (let + ((grammar (mau/make-grammar ops vars))) + (mau/collect-rules! stmts grammar eqs rules) + {:name name :grammar grammar :sorts sorts :eqs eqs :ops ops :t :module :vars vars :subsorts subsorts :kind kind :rules rules})))) + +(define + mau/parse-module + (fn + (src) + (let + ((toks (mau/tokenize src))) + (let + ((kind (nth toks 0)) (name (nth toks 1))) + (let + ((body (mau/take (mau/drop toks 3) (- (len toks) 4)))) + (mau/build-module kind name body)))))) + +;; ---------- signature queries ---------- + +(define mau/module-name (fn (m) (get m :name))) +(define mau/module-kind (fn (m) (get m :kind))) +(define mau/module-sorts (fn (m) (get m :sorts))) +(define mau/module-subsorts (fn (m) (get m :subsorts))) +(define mau/module-ops (fn (m) (get m :ops))) +(define mau/module-vars (fn (m) (get m :vars))) +(define mau/module-eqs (fn (m) (get m :eqs))) +(define mau/module-rules (fn (m) (get m :rules))) +(define mau/module-grammar (fn (m) (get m :grammar))) + +(define + mau/parse-term-in + (fn (m src) (mau/parse-term (mau/tokenize src) (mau/module-grammar m)))) + +(define + mau/collect-supers + (fn + (pairs s) + (cond + ((empty? pairs) (list)) + ((= (first (first pairs)) s) + (cons + (nth (first pairs) 1) + (mau/collect-supers (rest pairs) s))) + (else (mau/collect-supers (rest pairs) s))))) + +(define mau/supers-of (fn (m s) (mau/collect-supers (get m :subsorts) s))) + +(define + mau/dfs-reach + (fn + (m frontier target seen) + (cond + ((empty? frontier) false) + ((= (first frontier) target) true) + ((mau/member? (first frontier) seen) + (mau/dfs-reach m (rest frontier) target seen)) + (else + (mau/dfs-reach + m + (mau/append2 (mau/supers-of m (first frontier)) (rest frontier)) + target + (cons (first frontier) seen)))))) + +(define + mau/subsort? + (fn + (m sub super) + (mau/dfs-reach m (mau/supers-of m sub) super (list sub)))) + +(define mau/sort<=? (fn (m a b) (or (= a b) (mau/subsort? m a b)))) + +(define + mau/filter-ops + (fn + (ops name) + (cond + ((empty? ops) (list)) + ((= (get (first ops) :name) name) + (cons (first ops) (mau/filter-ops (rest ops) name))) + (else (mau/filter-ops (rest ops) name))))) + +(define + mau/ops-named + (fn (m name) (mau/filter-ops (mau/module-ops m) name))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json new file mode 100644 index 00000000..483579f1 --- /dev/null +++ b/lib/maude/scoreboard.json @@ -0,0 +1,10 @@ +{ + "lang": "maude", + "total_passed": 65, + "total_failed": 0, + "total": 65, + "suites": [ + {"name":"parse","passed":65,"failed":0,"total":65} + ], + "generated": "2026-06-07T14:42:29+00:00" +} diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md new file mode 100644 index 00000000..ca01f652 --- /dev/null +++ b/lib/maude/scoreboard.md @@ -0,0 +1,7 @@ +# maude scoreboard + +**65 / 65 passing** (0 failure(s)). + +| Suite | Passed | Total | Status | +|-------|--------|-------|--------| +| parse | 65 | 65 | ok | diff --git a/lib/maude/term.sx b/lib/maude/term.sx new file mode 100644 index 00000000..c29a04ae --- /dev/null +++ b/lib/maude/term.sx @@ -0,0 +1,114 @@ +;; lib/maude/term.sx — Maude term representation. +;; +;; A term is one of: +;; variable {:t :var :name "X" :sort "Nat"} +;; application {:t :app :op "_+_" :args (a b ...)} (constant: empty args) +;; +;; Sorts attach to variables; operator/result sorts live on op declarations +;; in the module signature, not on the term node. Overloading is resolved at +;; reduction time, so the parser only records the operator name. + +(define mau/var (fn (name sort) {:name name :t :var :sort sort})) + +(define mau/app (fn (op args) {:op op :t :app :args args})) + +(define mau/const (fn (op) {:op op :t :app :args (list)})) + +(define mau/var? (fn (t) (and (dict? t) (= (get t :t) "var")))) + +(define mau/app? (fn (t) (and (dict? t) (= (get t :t) "app")))) + +(define mau/term? (fn (t) (or (mau/var? t) (mau/app? t)))) + +(define mau/op (fn (t) (get t :op))) +(define mau/args (fn (t) (get t :args))) +(define mau/vname (fn (t) (get t :name))) +(define mau/vsort (fn (t) (get t :sort))) +(define mau/arity (fn (t) (len (get t :args)))) + +(define mau/const? (fn (t) (and (mau/app? t) (empty? (mau/args t))))) + +(define + mau/args=? + (fn + (as bs) + (cond + ((and (empty? as) (empty? bs)) true) + ((or (empty? as) (empty? bs)) false) + (else + (and + (mau/term=? (first as) (first bs)) + (mau/args=? (rest as) (rest bs))))))) + +(define + mau/term=? + (fn + (a b) + (cond + ((and (mau/var? a) (mau/var? b)) + (and + (= (mau/vname a) (mau/vname b)) + (= (mau/vsort a) (mau/vsort b)))) + ((and (mau/app? a) (mau/app? b)) + (and + (= (mau/op a) (mau/op b)) + (mau/args=? (mau/args a) (mau/args b)))) + (else false)))) + +(define + mau/join-args + (fn + (args) + (cond + ((empty? args) "") + ((empty? (rest args)) (mau/term->str (first args))) + (else + (str (mau/term->str (first args)) ", " (mau/join-args (rest args))))))) + +(define + mau/term->str + (fn + (t) + (cond + ((mau/var? t) (mau/vname t)) + ((mau/const? t) (mau/op t)) + ((mau/app? t) (str (mau/op t) "(" (mau/join-args (mau/args t)) ")")) + (else "?")))) + +(define + mau/member? + (fn + (x xs) + (cond + ((empty? xs) false) + ((= x (first xs)) true) + (else (mau/member? x (rest xs)))))) + +(define + mau/union + (fn + (xs ys) + (cond + ((empty? xs) ys) + ((mau/member? (first xs) ys) (mau/union (rest xs) ys)) + (else (cons (first xs) (mau/union (rest xs) ys)))))) + +(define + mau/term-vars + (fn + (t) + (cond + ((mau/var? t) (list (mau/vname t))) + ((mau/app? t) (mau/term-vars-list (mau/args t))) + (else (list))))) + +(define + mau/term-vars-list + (fn + (args) + (if + (empty? args) + (list) + (mau/union + (mau/term-vars (first args)) + (mau/term-vars-list (rest args)))))) diff --git a/lib/maude/tests/parse.sx b/lib/maude/tests/parse.sx new file mode 100644 index 00000000..d16669ff --- /dev/null +++ b/lib/maude/tests/parse.sx @@ -0,0 +1,250 @@ +;; lib/maude/tests/parse.sx — Phase 1: tokenizer, signatures, term/eq parsing. + +(define mpt-pass 0) +(define mpt-fail 0) +(define mpt-failures (list)) + +(define + mpt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mpt-pass (+ mpt-pass 1)) + (do + (set! mpt-fail (+ mpt-fail 1)) + (append! + mpt-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- modules under test ---- + +(define + mpt-peano + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat [assoc comm prec 33] .\n op _*_ : Nat Nat -> Nat [assoc comm] .\n vars X Y : Nat .\n eq 0 + X = X .\n eq s X + Y = s (X + Y) .\n eq 0 * X = 0 .\nendfm")) + +(define + mpt-natlist + (mau/parse-module + "fmod NATLIST is\n sorts Zero NzNat Nat List .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n subsort Nat < List .\n op 0 : -> Zero .\n op nil : -> List .\n op _;_ : List List -> List [assoc id: nil] .\n op head : List -> Nat .\n op length : List -> Nat .\n vars L M : List .\n var N : Nat .\n eq length(nil) = 0 .\n eq head(N ; L) = N .\nendfm")) + +;; ---- tokenizer ---- + +(define mpt-toks (mau/tokenize "op _+_ : Nat Nat -> Nat [assoc] .")) + +(mpt-check! "tok-count" (len mpt-toks) 11) +(mpt-check! "tok-op" (nth mpt-toks 0) "op") +(mpt-check! "tok-mixfix" (nth mpt-toks 1) "_+_") +(mpt-check! "tok-colon" (nth mpt-toks 2) ":") +(mpt-check! "tok-arrow" (nth mpt-toks 5) "->") +(mpt-check! "tok-lbrack" (nth mpt-toks 7) "[") +(mpt-check! "tok-dot" (nth mpt-toks 10) ".") +(mpt-check! + "tok-comment" + (len (mau/tokenize "sort Nat . --- a comment\nop 0 : -> Nat .")) + 9) + +;; ---- mixfix classification ---- + +(mpt-check! "form-infix" (get (mau/op-form "_+_") :kind) "infix") +(mpt-check! "form-infix-tok" (get (mau/op-form "_+_") :token) "+") +(mpt-check! "form-prefix" (get (mau/op-form "s_") :kind) "prefix") +(mpt-check! "form-prefix-tok" (get (mau/op-form "s_") :token) "s") +(mpt-check! "form-postfix" (get (mau/op-form "_!") :kind) "postfix") +(mpt-check! "form-const" (get (mau/op-form "nil") :kind) "const") +(mpt-check! + "form-mixfix" + (get (mau/op-form "if_then_else_fi") :kind) + "mixfix") + +;; ---- module header / sorts ---- + +(mpt-check! "mod-name" (mau/module-name mpt-peano) "PEANO") +(mpt-check! "mod-kind" (mau/module-kind mpt-peano) "fmod") +(mpt-check! "mod-sorts" (mau/module-sorts mpt-peano) (list "Nat")) +(mpt-check! + "natlist-sorts-count" + (len (mau/module-sorts mpt-natlist)) + 4) + +;; ---- subsorts (direct + transitive) ---- + +(mpt-check! "subsort-direct" (mau/subsort? mpt-natlist "NzNat" "Nat") true) +(mpt-check! "subsort-trans" (mau/subsort? mpt-natlist "NzNat" "List") true) +(mpt-check! "subsort-trans2" (mau/subsort? mpt-natlist "Zero" "List") true) +(mpt-check! "subsort-none" (mau/subsort? mpt-natlist "List" "Nat") false) +(mpt-check! "sort<=-refl" (mau/sort<=? mpt-natlist "Nat" "Nat") true) +(mpt-check! "sort<=-trans" (mau/sort<=? mpt-natlist "Zero" "List") true) + +;; ---- operators / overloading ---- + +(mpt-check! "ops-count" (len (mau/module-ops mpt-peano)) 4) +(mpt-check! + "op-arity" + (get (first (mau/ops-named mpt-peano "_+_")) :arity) + (list "Nat" "Nat")) +(mpt-check! + "op-result" + (get (first (mau/ops-named mpt-peano "s_")) :result) + "Nat") +(mpt-check! + "op-const-arity" + (len (get (first (mau/ops-named mpt-peano "0")) :arity)) + 0) +(mpt-check! + "natlist-ops-count" + (len (mau/module-ops mpt-natlist)) + 5) + +;; ---- attributes ---- + +(mpt-check! + "attr-assoc" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :assoc) + true) +(mpt-check! + "attr-comm" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :comm) + true) +(mpt-check! + "attr-prec" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :prec) + 33) +(mpt-check! + "attr-id" + (get (get (first (mau/ops-named mpt-natlist "_;_")) :attrs) :id) + "nil") +(mpt-check! + "attr-absent" + (get (get (first (mau/ops-named mpt-peano "_*_")) :attrs) :prec) + nil) + +;; ---- variables ---- + +(mpt-check! "var-sort" (get (mau/module-vars mpt-peano) "X") "Nat") +(mpt-check! "var-list-sort" (get (mau/module-vars mpt-natlist) "L") "List") + +;; ---- term parsing ---- + +(mpt-check! + "term-const" + (mau/term->str (mau/parse-term-in mpt-peano "0")) + "0") +(mpt-check! + "term-prefix-mixfix" + (mau/term->str (mau/parse-term-in mpt-peano "s 0")) + "s_(0)") +(mpt-check! + "term-nested-prefix" + (mau/term->str (mau/parse-term-in mpt-peano "s s 0")) + "s_(s_(0))") +(mpt-check! + "term-infix" + (mau/term->str (mau/parse-term-in mpt-peano "X + Y")) + "_+_(X, Y)") +(mpt-check! + "term-prec" + (mau/term->str (mau/parse-term-in mpt-peano "s X + Y")) + "_+_(s_(X), Y)") +(mpt-check! + "term-paren" + (mau/term->str (mau/parse-term-in mpt-peano "s (X + Y)")) + "s_(_+_(X, Y))") +(mpt-check! + "term-left-assoc" + (mau/term->str (mau/parse-term-in mpt-peano "X + Y + X")) + "_+_(_+_(X, Y), X)") +(mpt-check! + "term-prefix-form" + (mau/term->str (mau/parse-term-in mpt-peano "_+_(X, 0)")) + "_+_(X, 0)") +(mpt-check! + "term-funcall" + (mau/term->str (mau/parse-term-in mpt-natlist "length(nil)")) + "length(nil)") +(mpt-check! + "term-onthefly-var" + (mau/var? (mau/parse-term-in mpt-peano "Z:Nat")) + true) +(mpt-check! + "term-onthefly-sort" + (mau/vsort (mau/parse-term-in mpt-peano "Z:Nat")) + "Nat") +(mpt-check! + "term-var-vs-const" + (mau/var? (mau/parse-term-in mpt-peano "X")) + true) +(mpt-check! + "term-const-not-var" + (mau/var? (mau/parse-term-in mpt-peano "0")) + false) + +;; ---- equations ---- + +(mpt-check! "eq-count" (len (mau/module-eqs mpt-peano)) 3) +(mpt-check! + "eq-lhs" + (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :lhs)) + "_+_(s_(X), Y)") +(mpt-check! + "eq-rhs" + (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :rhs)) + "s_(_+_(X, Y))") +(mpt-check! + "eq-uncond" + (get (nth (mau/module-eqs mpt-peano) 0) :cond) + nil) +(mpt-check! + "natlist-eq-head" + (mau/term->str (get (nth (mau/module-eqs mpt-natlist) 1) :lhs)) + "head(_;_(N, L))") + +;; ---- conditional equations ---- + +(define + mpt-gcd + (mau/parse-module + "fmod GCD is\n sort Nat .\n op _>_ : Nat Nat -> Bool .\n op _-_ : Nat Nat -> Nat .\n op gcd : Nat Nat -> Nat .\n vars X Y : Nat .\n ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\nendfm")) + +(mpt-check! "ceq-count" (len (mau/module-eqs mpt-gcd)) 1) +(mpt-check! + "ceq-has-cond" + (= (get (first (mau/module-eqs mpt-gcd)) :cond) nil) + false) +(mpt-check! + "ceq-cond-kind" + (get (get (first (mau/module-eqs mpt-gcd)) :cond) :kind) + "eq") +(mpt-check! + "ceq-cond-lhs" + (mau/term->str (get (get (first (mau/module-eqs mpt-gcd)) :cond) :lhs)) + "_>_(X, Y)") + +;; ---- system module + rules ---- + +(define + mpt-vending + (mau/parse-module + "mod VENDING is\n sort State .\n op _coin : State -> State .\n op buy : State -> State .\n var S : State .\n rl [insert] : S coin => buy(S) .\n crl [guard] : buy(S) => S if S = S .\nendfm")) + +(mpt-check! "mod-kind-mod" (mau/module-kind mpt-vending) "mod") +(mpt-check! "rules-count" (len (mau/module-rules mpt-vending)) 2) +(mpt-check! + "rule-label" + (get (first (mau/module-rules mpt-vending)) :label) + "insert") +(mpt-check! + "rule-rhs" + (mau/term->str (get (first (mau/module-rules mpt-vending)) :rhs)) + "buy(S)") +(mpt-check! + "crl-label" + (get (nth (mau/module-rules mpt-vending) 1) :label) + "guard") +(mpt-check! + "crl-cond-kind" + (get (get (nth (mau/module-rules mpt-vending) 1) :cond) :kind) + "eq") + +(define mau-parse-tests-run! (fn () {:failures mpt-failures :total (+ mpt-pass mpt-fail) :passed mpt-pass :failed mpt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index e5526ffd..d559af7a 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -62,10 +62,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 ## Roadmap ### Phase 1 — Parser + signatures -- [ ] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations. -- [ ] Sort hierarchy with subsort relations. -- [ ] Operator overloading by arity + sort. -- [ ] Tests: parse classic examples (peano nat, list of naturals). +- [x] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations. +- [x] Sort hierarchy with subsort relations. +- [x] Operator overloading by arity + sort. +- [x] Tests: parse classic examples (peano nat, list of naturals). ### Phase 2 — Syntactic equational reduction - [ ] Apply equations left-to-right until no equation matches. @@ -125,7 +125,22 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting. ## Progress log -_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_ + +- **Phase 1 (parser + signatures) — DONE, 65/65.** `lib/maude/term.sx` (term + repr: var/app dicts, equality, vars, `term->str`) + `lib/maude/parser.sx` + (whitespace+bracket tokenizer with `---`/`***` comments; mixfix + classification by splitting op names on `_`; precedence-climbing term parser + over a pratt table built from op decls; `fmod`/`mod` modules with + sorts/subsorts/ops/vars/eqs/rules). Consumes `lib/guest/lex.sx` (ws classes) + and `lib/guest/pratt.sx` (op-table lookup). Verified on Peano (`s X + Y` + parses `_+_(s_(X), Y)` — prefix binds tighter than infix) and NatList + (transitive subsorts NzNat