(module equiv mzscheme

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

  (define equiv-rules/c
    (recursive-contract (flat-named-contract "<equiv rules>" equiv-rules?)))
  (define predicate/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-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])

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

  (define (add-equiv-rule pred equiv rules)
    (make-equiv-rules
     (cons (make-equiv-rule pred equiv)
           (equiv-rules-rules rules))))

  (define (add-equiv-rule/leaf pred leaf-equiv rules)
    (add-equiv-rule pred (wrap-leaf-equiv leaf-equiv) rules))

  (define (wrap-leaf-equiv leaf-equiv)
    (lambda (_ one two) (leaf-equiv one two)))

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

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

  (define (empty-hypotheses)
    (make-hash-table 'weak))

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

  (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 (and (pred one) (pred two))
                 (equiv active-equiv one two)
                 (loop rest))))))

  (define (structural-equiv? active-equiv one two)
    (and (struct-type-equiv? one two)
         (struct-equiv? active-equiv one two)))

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

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

  (define (atom? v)
    (or (null? v)
        (boolean? v)
        (symbol? v)
        (char? v)))

  (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=?))

  (define (box-equiv? active-equiv one two)
    (active-equiv (unbox one) (unbox two)))

  (define (pair-equiv? active-equiv one two)
    (and (active-equiv (car one) (car two))
         (active-equiv (cdr one) (cdr two))))

  (define (vector-equiv? active-equiv one two)
    (and (= (vector-length one) (vector-length two))
         (srfi43:vector-every active-equiv one two)))

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

  (define default-equiv-rules
    (make-equiv-rules
     (list
      (make-equiv-rule atom? atom-equiv?)
      (make-equiv-rule number? number-equiv?)
      (make-equiv-rule pair? pair-equiv?)
      (make-equiv-rule box? box-equiv?)
      (make-equiv-rule string? string-equiv?)
      (make-equiv-rule bytes? bytes-equiv?)
      (make-equiv-rule vector? vector-equiv?)
      (make-equiv-rule hash-table? hash-table-equiv?)
      )))

  (define current-equiv-rules
    (make-parameter default-equiv-rules guard-equiv-rules))

  (define (equiv? one two)
    ((make-equiv (current-equiv-rules)) one two))

  )