maude: Phase 1 parser — fmod/mod modules, signatures, mixfix terms (65 tests)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m14s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m14s
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) <noreply@anthropic.com>
This commit is contained in:
15
lib/maude/conformance.conf
Normal file
15
lib/maude/conformance.conf
Normal file
@@ -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!)"
|
||||
)
|
||||
3
lib/maude/conformance.sh
Executable file
3
lib/maude/conformance.sh
Executable file
@@ -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" "$@"
|
||||
673
lib/maude/parser.sx
Normal file
673
lib/maude/parser.sx
Normal file
@@ -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)))
|
||||
10
lib/maude/scoreboard.json
Normal file
10
lib/maude/scoreboard.json
Normal file
@@ -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"
|
||||
}
|
||||
7
lib/maude/scoreboard.md
Normal file
7
lib/maude/scoreboard.md
Normal file
@@ -0,0 +1,7 @@
|
||||
# maude scoreboard
|
||||
|
||||
**65 / 65 passing** (0 failure(s)).
|
||||
|
||||
| Suite | Passed | Total | Status |
|
||||
|-------|--------|-------|--------|
|
||||
| parse | 65 | 65 | ok |
|
||||
114
lib/maude/term.sx
Normal file
114
lib/maude/term.sx
Normal file
@@ -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))))))
|
||||
250
lib/maude/tests/parse.sx
Normal file
250
lib/maude/tests/parse.sx
Normal file
@@ -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}))
|
||||
@@ -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<Nat<List; `_;_` overloaded; `id: nil` / `prec`
|
||||
attrs). ceq/rl/crl parsed structurally (cond split on `if`, label in `[..]`).
|
||||
Suite + conformance driver wired (`lib/maude/conformance.{conf,sh}`, MODE=dict).
|
||||
- Notes for next phases: terms are `{:t :app :op N :args (...)}` /
|
||||
`{:t :var :name N :sort S}`; module carries a `:grammar` so
|
||||
`mau/parse-term-in` can parse term strings against its op table. Overloading
|
||||
is recorded but NOT resolved at parse time (resolve at reduce time).
|
||||
|
||||
## Blockers
|
||||
_(speculative — equational matching is algorithmically heavy and may surface JIT issues)_
|
||||
_(none)_
|
||||
|
||||
Reference in New Issue
Block a user