equiv.ss
(module equiv mzscheme

(require (lib "etc.ss")
(lib "plt-match.ss")
(prefix srfi43: (lib "43.ss" "srfi"))
(lib "contract.ss"))

;; An EquivRules is (make-equiv-rules (Listof EquivRule))
;; An EquivRule is (make-equiv-rule (Predicate T) (NodeEquality T))
;; A (Pred T) is pred such that:
;;   - pred : Any -> Boolean
;;   - (pred v) iff v : T
;; A (BinPred A B) is pred such that:
;;   - pred : Any Any -> Boolean
;;   - (pred v1 v2) iff v1 : A and v2 : B
;; A (NodeEquiv A B) is ((Any Any -> Boolean) A B -> Boolean)
(define-struct equiv-rules (rules))
(define-struct equiv-rule (pred equiv))

(define equiv-rules/c (flat-named-contract "<equiv rules>" equiv-rules?))
(define predicate/c (any/c . -> . any))
(define binary-predicate/c (any/c any/c . -> . any))
(define equality/c (any/c any/c . -> . any))
(define node-equality/c (equality/c any/c any/c . -> . any))

(provide/contract
[equiv-rules/c flat-contract?]
[equiv-rules? predicate/c]
[default-equiv-rules equiv-rules/c]
(predicate/c node-equality/c equiv-rules/c . -> . equiv-rules/c)]
(binary-predicate/c node-equality/c equiv-rules/c . -> . equiv-rules/c)]
(predicate/c equality/c equiv-rules/c . -> . equiv-rules/c)]
[make-equiv (equiv-rules/c . -> . equality/c)]
[current-equiv-rules parameter?]
[equiv? equality/c])

;; (T -> Bool) -> T T -> Bool
;; Converts a unary predicate to its own conjunction over two arguments.
(define ((wrap-unary-pred p) one two)
(and (p one) (p two)))

;; (Pred T) (NodeEquiv T T) EquivRules -> EquivRules
;; see doc.txt
(make-equiv-rules
(cons (make-equiv-rule (wrap-unary-pred pred) equiv)
(equiv-rules-rules rules))))

;; (BinPred A B) (NodeEquiv A B) EquivRules -> EquivRules
;; see doc.txt
(make-equiv-rules
(cons (make-equiv-rule pred equiv)
(cons (make-equiv-rule (lambda (a b) (pred b a))
(lambda (=? a b) (equiv =? b a)))
(equiv-rules-rules rules)))))

;; (Pred T) (T T -> Bool) EquivRules -> EquivRules
;; see doc.txt

;; (A B -> Bool) -> (NodeEquiv A B)
;; Converts a nonrecursive predicate to a "node equivalence".
(define (wrap-leaf-equiv leaf-equiv)
(lambda (_ one two) (leaf-equiv one two)))

;; Any -> EquivRules
;; Returns any EquivRules unchanged, otherwise raises a contract error.
(define (guard-equiv-rules value)
(unless (equiv-rules? value)
(raise (make-exn:fail:contract
(format "current-equiv-rules: ~s is not an equiv-rules" value)
(current-continuation-marks))))
value)

;; EquivRules -> Any Any -> Boolean
;; Constructs a recursive equivalence predicate from a list of rules.
(define (make-equiv rules)
(lambda (one two)
(let* ([hypotheses (empty-hypotheses)])
(recur active-equiv ([one one]
[two two])
(or (eq? one two)
(check-hypotheses! hypotheses one two)
(extension-equiv? rules active-equiv one two)
(structural-equiv? active-equiv one two))))))

;; A Hypotheses is a (WeakHashTable Any (WeakHashTable Any #t)).
;; If values one,two are hypothesized to be equivalent in hyp : Hypotheses,
;; then (hash-table-get (hash-table-get hyp a) b) = #t.

;; -> Hypotheses
;; Constructs an empty set of hypotheses.
(define (empty-hypotheses)
(make-hash-table 'weak))

;; Hypotheses Any Any -> Boolean
;; Reports whether values one,two are hypothesized to be equal;
;; adds them as a new hypothesis for subsequent checks.
(define (check-hypotheses! table one two)
(let* ([entry-one
(hash-table-get
table one
(lambda ()
(let* ([table* (make-hash-table 'weak)])
(hash-table-put! table one table*)
table*)))]
[entry-two
(hash-table-get
entry-one two
(lambda ()
(hash-table-put! entry-one two #t)
#f))])
entry-two))

;; EquivRules (Any Any -> Bool) Any Any -> Bool
;; Checks whether one,two are equivalent according to the given rules,
;; passing along the given recursive equivalence predicate.
(define (extension-equiv? rules active-equiv one two)
(recur loop ([rules (equiv-rules-rules rules)])
(and (pair? rules)
(let* ([rule (car rules)]
[rest (cdr rules)]
[pred (equiv-rule-pred rule)]
[equiv (equiv-rule-equiv rule)])
(if (pred one two)
(equiv active-equiv one two)
(loop rest))))))

;; (Any Any -> Bool) Any Any -> Bool
;; Reports whether one,two have equivalent structure types
;; and equivalent substructures according to the given recursive
;; equivalence predicate.
(define (structural-equiv? active-equiv one two)
(and (struct-type-equiv? one two)
(struct-equiv? active-equiv one two)))

;; Any Any -> Bool
;; Reports whether two values have the same immediate structure type.
(define (struct-type-equiv? one two)
(let*-values ([(type-one skipped?-one) (struct-info one)]
[(type-two skipped?-two) (struct-info two)])
(and (not skipped?-one)
(not skipped?-two)
type-one
type-two
(eq? type-one type-two))))

;; (Any Any -> Bool) Any Any -> Bool
;; Reports whether two values' substructures are equivalent
;; according to the given predicate.
(define (struct-equiv? active-equiv one two)
(let* ([opaque (gensym)]
[vec-one (struct->vector one opaque)]
[vec-two (struct->vector two opaque)])
(and (= (vector-length vec-one) (vector-length vec-two))
(srfi43:vector-every
(lambda (one two)
(and (not (eq? one opaque))
(not (eq? two opaque))
(active-equiv one two)))
vec-one
vec-two))))

;; (Pred Atom)
;; Reports whether a value belongs to a builtin type with no substructure
;; (empty list, boolean, symbol, or character).
(define (atom? v)
(or (null? v)
(boolean? v)
(symbol? v)
(char? v)))

;; *-equiv? : (NodeEquiv * *)
;; Node equivalence predicates for builtin types without recursive
;; substructure: atoms, numbers, strings, and byte strings.
(define atom-equiv? (wrap-leaf-equiv eq?))
(define number-equiv? (wrap-leaf-equiv =))
(define string-equiv? (wrap-leaf-equiv string=?))
(define bytes-equiv? (wrap-leaf-equiv bytes=?))

;; : (NodeEquiv Box Box)
;; Recursive equivalence for boxes.
(define (box-equiv? active-equiv one two)
(active-equiv (unbox one) (unbox two)))

;; : (NodeEquiv Pair Pair)
;; Recursive equivalence for pairs.
(define (pair-equiv? active-equiv one two)
(and (active-equiv (car one) (car two))
(active-equiv (cdr one) (cdr two))))

;; : (NodeEquiv Vector Vector)
;; Recursive equivalence for vectors.
(define (vector-equiv? active-equiv one two)
(and (= (vector-length one) (vector-length two))
(srfi43:vector-every active-equiv one two)))

;; : (NodeEquiv HashTable HashTable)
;; Recursive equivalence for hash tables.
(define (hash-table-equiv? active-equiv one two)
(let/ec return
;; Make sure one is a subset of two
(hash-table-for-each
one
(lambda (k _)
(hash-table-get two k (lambda () (return #f)))))
;; Make sure two is a subset of one
(hash-table-for-each
two
(lambda (k _)
(hash-table-get one k (lambda () (return #f)))))
;; Make sure bound values are equal
(hash-table-for-each
one
(lambda (k v)
(unless (active-equiv v (hash-table-get two k))
(return #f))))
;; Done
#t))

;; : EquivRules
;; see doc.txt
(define default-equiv-rules
(make-equiv-rules
(map
(lambda (l)
(make-equiv-rule (wrap-unary-pred (car l)) (cadr l)))
(list
(list atom? atom-equiv?)
(list number? number-equiv?)
(list pair? pair-equiv?)
(list box? box-equiv?)
(list string? string-equiv?)
(list bytes? bytes-equiv?)
(list vector? vector-equiv?)
(list hash-table? hash-table-equiv?)
))))

;; : (Parameter EquivRules)
;; see doc.txt
(define current-equiv-rules
(make-parameter default-equiv-rules guard-equiv-rules))

;; : Any Any -> Boolean
;; see doc.txt
(define (equiv? one two)
((make-equiv (current-equiv-rules)) one two))

)