The (aux variable) module

Logic variables introduced by fresh

Posted on October 21, 2026 · by Massimo Nocentini · 2-minute read · Scheme

`test/symbol∼subscripts`: pass

(define (test/symbol∼subscripts _) (⊦= 'g₁₂₃ (symbol∼subscripts 'g123)))

((eta 0.0) (memory #(6291456 1956912 1048576)) (stdout "") (stderr ""))

`test/variable-printer`: pass

(define (test/variable-printer _)
  (⊦= "g₁₂₃" (display->string (V 'g123)))
  (⊦= "(g₁ hello)" (display->string (list (V 'g1) (V 'hello)))))

((eta 0.0) (memory #(6291456 1958504 1048576)) (stdout "") (stderr ""))

`test/fresh₁`: pass

(define (test/fresh₁ _)
  (let ((g₁ (with-output-to-string (τ (fresh₁ display))))
        (g₂ (with-output-to-string (τ (fresh₁ display)))))
    (⊨ (gensym-subscripted? g₁))
    (⊨ (gensym-subscripted? g₂))
    (⊭ (equal? g₁ g₂)))
  (fresh₁
    (λ (v)
       (⊨ (variable? v))
       (⊦= (symbol->string (symbol∼subscripts (variable-s v)))
           (display->string v)))))

((eta 0.001) (memory #(6291456 1959936 1048576)) (stdout "") (stderr ""))

`test/fresh`: pass

(define (test/fresh _)
  (let1 (vs (fresh (v w z) (list v w z)))
        (⊦= 3 (length vs))
        (⊨ (pairwise-different? vs))
        (let1 (str (with-output-to-string (τ (display vs))))
              (⊦= (string-append
                    "("
                    (display->string (car vs))
                    " "
                    (display->string (cadr vs))
                    " "
                    (display->string (caddr vs))
                    ")")
                  str)
              (⊨ (and (gensym-subscripted? (display->string (car vs)))
                      (gensym-subscripted? (display->string (cadr vs)))
                      (gensym-subscripted? (display->string (caddr vs))))))))

((eta 0.0) (memory #(6291456 1960968 1048576)) (stdout "") (stderr ""))

`test/variable-equal?`: pass

(define (test/variable-equal? _)
  (let ((one (V (gensym))) (two (V 'hello)) (three (V 'hello)))
    (⊦= #f (equal? one two))
    (⊦= #f (equal? one three))
    (⊦= #t (equal? two three))))

((eta 0.0) (memory #(6291456 1962136 1048576)) (stdout "") (stderr ""))

`test/V-rejects-non-symbols`: pass

(define (test/V-rejects-non-symbols _)
  (⊦= 'rejected (condition-case (begin (V 42) 'accepted) ((exn) 'rejected)))
  (⊦= 'rejected (condition-case (begin (V "g1") 'accepted) ((exn) 'rejected))))

((eta 0.0) (memory #(6291456 1968800 1048576)) (stdout "") (stderr ""))