It wasn't the worst thing to try and paper over, but I can definitely see why it might be problematic. This works (by renaming and checking equality for the same pattern variables), although it can be improved still to eliminate unnecessary let declarations and so on.
I had to "separate" the cases of patterns in the head and in the bodies of the match-clauses, which at least was easy enough with parameterized syntax-classes and some conventions.
#lang racket/base
(require
(only-in
racket/list flatten)
(only-in
racket/match match-lambda)
(only-in
racket/set list->set set-count)
(only-in
racket/format ~a)
(for-syntax
syntax/stx
racket/base
syntax/parse
racket/syntax
(only-in
racket/list remove-duplicates group-by)))
(struct mark [sum]
#:transparent
#:guard
(lambda (sum _)
(if (list? sum) (flatten sum) (list sum))))
(define (format-sum sum none some)
(if (null? sum) none (format some (apply ~a #:separator " " sum))))
(define ((mark-writer-maker none some) self port mode)
(define sum (mark-sum self))
(fprintf port (format-sum (mark-sum self) none some)))
(struct exp mark []
#:transparent
#:property prop:custom-print-quotable 'always
#:methods gen:custom-write
[(define write-proc (mark-writer-maker "○" "(~a)"))])
(struct log mark []
#:transparent
#:property prop:custom-print-quotable 'always
#:methods gen:custom-write
[(define write-proc (mark-writer-maker "□" "[~a]"))])
(struct neg mark []
#:transparent
#:property prop:custom-print-quotable 'always
#:methods gen:custom-write
[(define write-proc (mark-writer-maker "◇" "⟨~a⟩"))])
(define (same? . xs)
(= 1 (set-count (list->set xs))))
(begin-for-syntax
(define (push var)
(define mask (generate-temporary var))
(syntax-property mask 'self var))
(define-literal-set forms
#:datum-literals (≡ ○ □ ◇)
(unquote-splicing quasiquote unquote quote))
(define form? (literal-set->predicate forms))
(define-syntax-class
name
(pattern foo:id
#:when (not (form? #'foo))))
(define-syntax-class
(sum posn)
#:attributes
([ex 0]
[ns 0]
[ls 0])
#:literal-sets (forms)
#:local-conventions
([term (term posn)])
(pattern ,@var:name
#:when (eq? 'head posn)
#:attr sp (push #'var)
#:attr ex #',@sp
#:attr ns #'(sp)
#:attr ls #false)
(pattern ,@var:name
#:when (eq? 'body posn)
#:attr ex #',@var
#:attr ns #'(var)
#:attr ls #false)
(pattern var:name
#:attr ex #',var
#:attr ns #'(var)
#:attr ls #false)
(pattern (term ...)
#:attr ex #'(term.ex ...)
#:attr ns #'((~@ . term.ns) ...)
#:attr ls #true))
(define-syntax-class
(exp posn)
#:attributes
([ex 0]
[ns 0])
#:literal-sets (forms)
#:local-conventions
([sum (sum posn)])
(pattern ○
#:attr ex #',(exp null)
#:attr ns #'())
(pattern `sum
#:attr ex (if (attribute sum.ls) #',(exp `sum.ex) #',(exp sum))
#:attr ns #'sum.ns))
(define-syntax-class
(log posn)
#:attributes
([ex 0]
[ns 0])
#:literal-sets (forms)
#:local-conventions
([sum (sum posn)])
(pattern □
#:attr ex #',(log null)
#:attr ns #'())
(pattern ,sum
#:attr ex (if (attribute sum.ls) #',(log `sum.ex) #',(log sum))
#:attr ns #'sum.ns))
(define-syntax-class
(neg posn)
#:attributes
([ex 0]
[ns 0])
#:literal-sets (forms)
#:local-conventions
([sum (sum posn)])
(pattern ◇
#:attr ex #',(neg null)
#:attr ns #'())
(pattern 'sum
#:attr ex (if (attribute sum.ls) #',(neg `sum.ex) #',(neg sum))
#:attr ns #'sum.ns))
(define-syntax-class
(term posn)
#:attributes
([ex 0]
[ns 0])
#:local-conventions
([sum (sum posn)]
[exp (exp posn)]
[log (log posn)]
[neg (neg posn)])
(pattern ex:nat
#:attr ns #'())
(pattern (~or* sum exp log neg)
#:attr ex #'(~? sum.ex
(~? exp.ex
(~? log.ex
neg.ex)))
#:attr ns #'(~? sum.ns
(~? exp.ns
(~? log.ns
neg.ns)))))
(define-splicing-syntax-class
(terms posn)
#:attributes
([ex 0]
[ns 0])
#:local-conventions
([sum (sum posn)]
[term (term posn)])
(pattern sum
#:attr ex (if (attribute sum.ls) #'`sum.ex #'sum)
#:attr ns #'sum.ns)
(pattern {~seq term ...}
#:attr ex #'`(term.ex ...)
#:attr ns #'((~@ . term.ns) ...)))
(define-syntax-class
clause
#:attributes
([ex 0]
[as 0])
#:literal-sets (forms)
(pattern [as:name foo:expr ...]
#:attr ex #'(foo ...)))
(define (derive-cases clauses)
(define cls (stx->list clauses))
(for/list ([bd (in-list cls)])
(map (lambda (cl) `(,cl ,bd)) (remove bd cls))))
(define (var-name x)
(syntax-property x 'self))
(define (masked-vars names)
(filter var-name (stx->list names)))
(define (group-names names)
(define grouped (group-by var-name (masked-vars names) free-identifier=?))
(define samemap (map (lambda (g) (if (null? (cdr g)) (car g) #`(same? . #,g))) grouped))
(define rootmap (map (lambda (g) `(,(var-name (car g)) ,(car g))) grouped))
`(,samemap ,rootmap))
(define (map-groups names**)
(map (lambda (names*) (map group-names (stx->list names*))) (stx->list names**)))
(define-splicing-syntax-class
system
#:attributes
([ex 0]
[ns 0]
[as 0])
#:local-conventions
([hd (terms 'head)]
[bd (terms 'body)])
(pattern {~seq lhs:clause rhs:clause ...+}
#:with (({(hd) (bd)} ...) ...) (derive-cases #'(lhs.ex rhs.ex ...))
#:with (({cd lt} ...) ...) (map-groups #'((hd.ns ...) ...))
#:attr ex
#'(([hd.ex
#:when (and . cd)
(let lt bd.ex)]
...
[_ #false])
...)
#:attr ns #'((~@ . bd.ns) ... ...)
#:attr as #'(lhs.as rhs.as ...)))
(define (unique-names names)
(remove-duplicates (stx->list names) free-identifier=?))
(define ((format-rule stx ax) as)
(format-id stx "~a.~a" ax as #:subs? #true))
(define (format-rules stx ax as)
(map (format-rule stx ax) (stx->list as))))
(define-syntax (define-axiom stx)
(syntax-parse stx
[(_ name:id :system)
#:with (vars ...) (unique-names #'ns)
#:with (rule ...) (format-rules stx #'name #'as)
#:with (body ...) #'ex
#'(define-values (rule ...)
(let ([vars null] ...)
(values (match-lambda . body) ...)))]))
(define-syntax (el stx)
(syntax-parse stx
#:local-conventions
([terms (terms 'body)])
[(_ terms) #'terms.ex]))
(define-axiom arrange*
[gather
`(,@A ,(,@B ,@C ,@D))]
[spread
`(,@A ,B) `(,@A ,C) `(,@A ,D)])
(arrange*.gather
(el `(○ ○ ○ ,(3 ○))
`(○ ○ ○ ,(○ 4))
`(○ ○ ○ ,(○))))
;=> '((○ ○ ○ [3 ○ ○ 4 ○]))
; the macro above becomes
(define-values
(arrange*.gather arrange*.spread)
(let ((A null) (B null) (C null) (D null))
(values
(match-lambda
(`(,(exp `(,@A5 ,(log B))) ,(exp `(,@A6 ,(log C))) ,(exp `(,@A7 ,(log D))))
#:when
(and (same? A5 A6 A7))
(let ((A A5)) `(,(exp `(,@A ,(log `(,@B ,@C ,@D)))))))
(_ #f))
(match-lambda
(`(,(exp `(,@A8 ,(log `(,@B9 ,@C10 ,@D11)))))
#:when
(and A8 B9 C10 D11)
(let ((A A8) (B B9) (C C10) (D D11)) `(,(exp `(,@A ,(log B))) ,(exp `(,@A ,(log C))) ,(exp `(,@A ,(log D))))))
(_ #f)))))
The use of the let over the values is to ensure that asymmetric patterns (where a pattern variable occurs only in one or some but not all of the cases of the "axiom") remain valid, as in:
(define-axiom reflect
[create A 'A] [cancel ()])