Files
rose-ash/lib/maude/parser.sx
giles 9f87206949
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m14s
maude: Phase 1 parser — fmod/mod modules, signatures, mixfix terms (65 tests)
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>
2026-06-07 14:43:02 +00:00

674 lines
18 KiB
Plaintext

;; 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)))