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]
   [add-equiv-rule
    (predicate/c node-equality/c equiv-rules/c . -> . equiv-rules/c)]
   [add-binary-equiv-rule
    (binary-predicate/c node-equality/c equiv-rules/c . -> . equiv-rules/c)]
   [add-equiv-rule/leaf
    (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
  (define (add-equiv-rule pred equiv rules)
    (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
  (define (add-binary-equiv-rule pred equiv rules)
    (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
  (define (add-equiv-rule/leaf pred leaf-equiv rules)
    (add-equiv-rule pred (wrap-leaf-equiv leaf-equiv) rules))

  ;; (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))

  )