Skip to content

Commit

Permalink
Merge pull request #17 from quasarbright/main
Browse files Browse the repository at this point in the history
alpha-equivalent?
  • Loading branch information
michaelballantyne authored May 10, 2024
2 parents 17862e3 + c38998b commit 1e9964c
Show file tree
Hide file tree
Showing 3 changed files with 150 additions and 6 deletions.
3 changes: 2 additions & 1 deletion main.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@
symbol-table-set!
symbol-table-ref

free-identifiers))
free-identifiers
alpha-equivalent?))

(require "private/syntax/interface.rkt"
"private/runtime/compile.rkt"
Expand Down
74 changes: 71 additions & 3 deletions private/runtime/binding-operations.rkt
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
#lang racket/base

(provide free-identifiers)
(provide free-identifiers
alpha-equivalent?)

(require racket/list
racket/dict
syntax/parse
syntax/id-table
ee-lib
(for-template "./compile.rkt"))

Expand Down Expand Up @@ -49,6 +52,7 @@
(syntax-parse stx
[((~literal #%host-expression) . _)
(raise-host-expression-error-or-value
'free-identifiers
allow-host?
(list))]
[(a . b) (append (all-references #'a allow-host?)
Expand All @@ -64,6 +68,7 @@
(syntax-parse stx
[((~literal #%host-expression) . _)
(raise-host-expression-error-or-value
'free-identifiers
allow-host?
(list))]
[(a . b)
Expand All @@ -74,10 +79,10 @@
(list))]
[_ (list)]))

(define (raise-host-expression-error-or-value allow-host? value-if-allowed)
(define (raise-host-expression-error-or-value who-sym allow-host? value-if-allowed)
(if allow-host?
value-if-allowed
(error 'free-identifiers "can't compute the free identifiers of a #%host-expression")))
(error who-sym "can't enter a #%host-expression")))

(define (deduplicate-references ids)
(remove-duplicates ids identifier=?))
Expand All @@ -86,3 +91,66 @@
(for/list ([x xs]
#:unless (member x ys identifier=?))
x))

; Syntax, Syntax [#:allow-host? Boolean] -> Boolean
; Are the two expressions alpha-equivalent?
(define (alpha-equivalent? stx-a stx-b #:allow-host? [allow-host? #f])
(define bound-reference=? (alpha-equivalent?/bindings stx-a stx-b allow-host?))
(and bound-reference=?
(alpha-equivalent?/refrences stx-a stx-b bound-reference=? allow-host?)))

; Syntax Syntax Boolean -> (or/c #f (Identifier Identifier -> Boolean))
; check that the bindings of both expressions can be alpha-equivalent.
; returns bound-reference=?, or #f if the binding check fails.
(define (alpha-equivalent?/bindings stx-a stx-b allow-host?)
(define table-a (make-free-id-table))
(define table-b (make-free-id-table))
(define (bind! identifier-a identifier-b)
(define x (gensym))
(free-id-table-set! table-a identifier-a x)
(free-id-table-set! table-b identifier-b x))
(define (bound-reference=? identifier-a identifier-b)
(and (dict-has-key? table-a identifier-a)
(dict-has-key? table-b identifier-b)
(eq? (free-id-table-ref table-a identifier-a)
(free-id-table-ref table-b identifier-b))))
(define binders-a (all-binders stx-a allow-host?))
(define binders-b (all-binders stx-b allow-host?))
; must traverse binders before references
; in case a variable is referenced before it is bound,
; like mutual recursion
(for ([binder-a binders-a]
[binder-b binders-b])
(bind! binder-a binder-b))
(and (= (length binders-a) (length binders-b))
bound-reference=?))

; Syntax Syntax (Identifier Identifier -> Boolean) Boolean -> Boolean
; check that the references are alpha-equivalent.
(define (alpha-equivalent?/refrences stx-a stx-b bound-reference=? allow-host?)
(let loop ([stx-a stx-a] [stx-b stx-b])
(syntax-parse (list stx-a stx-b)
[(~or (((~literal #%host-expression) . _) _)
(_ ((~literal #%host-expression) . _)))
(raise-host-expression-error-or-value
'alpha-equivalent?
allow-host?
#f)]
[(a:id b:id)
(cond
[(and (compiled-binder? #'a)
(compiled-binder? #'b))
; bindings assumed to be equivalent
#t]
[(and (compiled-reference? #'a)
(compiled-reference? #'b))
(or (bound-reference=? #'a #'b)
; if they're free references
(identifier=? #'a #'b))]
[else (free-identifier=? #'a #'b)])]
[(() ()) #t]
[((a-car . a-cdr) (b-car . b-cdr))
(and (loop #'a-car #'b-car)
(loop #'a-cdr #'b-cdr))]
[(a b) (equal? (syntax->datum #'a)
(syntax->datum #'b))])))
79 changes: 77 additions & 2 deletions tests/binding-operations.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,10 @@
(host e:racket-expr)

(lambda (x:var) e:expr)
#:binding (scope (bind x) e))
#:binding (scope (bind x) e)

(letrec ([x:var e:expr] ...) body:expr)
#:binding (scope (bind x) e (scope body)))

(host-interface/definition
(define-var v:var)
Expand Down Expand Up @@ -41,7 +44,7 @@
'(x z))

(check-exn
#rx"free-identifiers: can't compute the free identifiers of a #%host-expression"
#rx"free-identifiers: can't enter a #%host-expression"
(lambda ()
(convert-compile-time-error
(expr/free-vars-as-symbols
Expand All @@ -62,3 +65,75 @@
z))
'(z))

(syntax-spec
(host-interface/expression
(expr/alpha-equivalent? a:expr b:expr)
#`#,(alpha-equivalent? #'a #'b #:allow-host? #f)))

(check-true
(expr/alpha-equivalent?
1
1))

(check-false
(expr/alpha-equivalent?
1
2))

(check-true
(expr/alpha-equivalent?
x
x))

(check-false
(expr/alpha-equivalent?
x
y))

(check-true
(expr/alpha-equivalent?
(+ x y)
(+ x y)))

(check-false
(expr/alpha-equivalent?
(+ x y)
(+ x z)))

(check-true
(expr/alpha-equivalent?
(lambda (a) (+ x a))
(lambda (b) (+ x b))))

(check-false
(expr/alpha-equivalent?
(lambda (a) x)
(lambda (x) x)))

(check-true
(expr/alpha-equivalent?
(letrec ([f g]
[g f])
f)
(letrec ([g f]
[f g])
g)))

(check-exn
; for some reason, including "alpha-equivalent?: " causes the test to fail
#rx"can't enter a #%host-expression"
(lambda ()
(convert-compile-time-error
(expr/alpha-equivalent?
(+ x (host PI))
(+ x (host PI))))))

(syntax-spec
(host-interface/expression
(expr/alpha-equivalent?/ignore-host a:expr b:expr)
#`#,(alpha-equivalent? #'a #'b #:allow-host? #t)))

(check-false
(expr/alpha-equivalent?/ignore-host
(+ x (host PI))
(+ x (host PI))))

0 comments on commit 1e9964c

Please sign in to comment.