Simple quasi-unifier.

This commit is contained in:
Tony Garnock-Jones 2013-10-24 21:32:14 +01:00
commit 79851b8533
2 changed files with 120 additions and 0 deletions

90
pattern.rkt Normal file
View File

@ -0,0 +1,90 @@
#lang racket/base
(require racket/match)
(require (only-in racket/class object?))
(require "struct-map.rkt")
(provide ?
wildcard?
specialization?
ground?
intersect)
(struct exn:unification-failure ())
(define unification-failure (exn:unification-failure))
(define (fail) (raise unification-failure))
(struct wildcard ()
#:transparent
#:property prop:custom-write
(lambda (v port mode)
(display "?" port)))
(define ? (wildcard))
;; Any -> Boolean
;; Racket objects are structures, so we reject them explicitly for
;; now, leaving them opaque to unification.
(define (non-object-struct? x)
(and (struct? x)
(not (object? x))))
;; True iff a is a specialization (or instance) of b.
(define (specialization? a b)
(let walk ((a a) (b b))
(cond
[(wildcard? b) #t]
[(wildcard? a) #f]
[(and (pair? a) (pair? b))
(and (walk (car a) (car b)) (walk (cdr a) (cdr b)))]
[(and (vector? a) (vector? b) (= (vector-length a) (vector-length b)))
(for/and ([aa a] [bb b]) (walk aa bb))]
[(and (non-object-struct? a) (non-object-struct? b))
(walk (struct->vector a #f) (struct->vector b #f))]
[else (equal? a b)])))
;; Any -> Boolean
;; True iff the term is completely ground, that is has no variables or
;; canonical-variables in it.
(define (ground? x)
(let walk ((x x))
(cond
[(wildcard? x) #f]
[(pair? x) (and (walk (car x)) (walk (cdr x)))]
[(vector? x) (andmap walk (vector->list x))]
[(non-object-struct? x) (walk (struct->vector x #f))]
[else #t])))
;; Vector StructType -> Struct
(define (vector->struct v t)
(apply (struct-type-make-constructor t) (cdr (vector->list v))))
;; Any Any -> Any
(define (unify a b)
(cond
[(wildcard? a) b]
[(wildcard? b) a]
[(and (pair? a) (pair? b))
(cons (unify (car a) (car b)) (unify (cdr a) (cdr b)))]
[(and (vector? a) (vector? b))
(unless (= (vector-length a) (vector-length b)) (fail))
(for/vector ((va (in-vector a)) (vb (in-vector b))) (unify va vb))]
[(and (non-object-struct? a) (non-object-struct? b))
(define-values (ta ta-skipped?) (struct-info a))
(define-values (tb tb-skipped?) (struct-info b))
(unless (eq? ta tb) (fail))
(when ta-skipped? (fail))
(when tb-skipped? (fail))
(vector->struct (unify (struct->vector a) (struct->vector b)) ta)]
[(equal? a b)
a]
[else (fail)]))
;; Any Any (Any -> X) (-> X) -> X
(define (intersect a b ks kf)
(define-values (ok? result)
(with-handlers ([exn:unification-failure? (lambda (e) (values #f (void)))])
(values #t (unify a b))))
(if ok?
(ks result)
(kf)))

30
test-pattern.rkt Normal file
View File

@ -0,0 +1,30 @@
#lang racket/base
(require "pattern.rkt")
(require rackunit)
(struct a (x) #:prefab)
(struct b (x) #:transparent)
(define (intersect-or-void a b) (intersect a b values void))
(check-equal? (intersect-or-void ? ?) ?)
(check-equal? (intersect-or-void 'a ?) 'a)
(check-equal? (intersect-or-void 123 ?) 123)
(check-equal? (intersect-or-void (cons ? 2) (cons 1 ?)) (cons 1 2))
(check-equal? (intersect-or-void (cons 1 2) ?) (cons 1 2))
(check-equal? (intersect-or-void 1 2) (void))
(check-equal? (intersect-or-void (cons 1 2) (cons ? 2)) (cons 1 2))
(check-equal? (intersect-or-void (cons 1 2) (cons 3 2)) (void))
(check-equal? (intersect-or-void (cons 1 2) (cons 1 3)) (void))
(check-equal? (intersect-or-void (vector 1 2) (vector 1 2)) (vector 1 2))
(check-equal? (intersect-or-void (vector 1 2) (vector 1 2 3)) (void))
(check-equal? (intersect-or-void (a 'a) (a 'b)) (void))
(check-equal? (intersect-or-void (a 'a) (a 'a)) (a 'a))
(check-equal? (intersect-or-void (a 'a) (a ?)) (a 'a))
(check-equal? (intersect-or-void (a 'a) ?) (a 'a))
(check-equal? (intersect-or-void (b 'a) (b 'b)) (void))
(check-equal? (intersect-or-void (b 'a) (b 'a)) (b 'a))
(check-equal? (intersect-or-void (b 'a) (b ?)) (b 'a))
(check-equal? (intersect-or-void (b 'a) ?) (b 'a))