(module logic-practice mzscheme
  (require (lib "unit.ss")
           (lib "etc.ss")
           (lib "list.ss"))
  
  
  ;; A function^ model consists of a universe of elements,
  ;; and a 2-place predicate P between elements.
  (define-signature function^ (universe
                               P))
  
  
  ;; for-all*: (X* -> boolean) X* -> boolean
  ;; Returns true if all combinations of the universes applied with
  ;; f returns true.
  ;; FIXME: this definition is uglier than I'd like.
  (define (for-all* f . universes)
    (cond
      [(empty? (rest universes))
       (andmap f (first universes))]
      [else
       (apply for-all*
              (lambda args
                (andmap (lambda (x) (apply f (cons x args)))
                        (first universes)))
              (rest universes))]))
  
  
  ;; exists: (X -> boolean) (listof X) -> boolean
  ;; Returns true if some element of the universe makes f true.
  (define (exists? f universe)
    (not (for-all* (lambda (x) (not (f x))) universe)))
  
  
  ;; implies?: boolean boolean -> boolean
  ;; implication.
  (define (implies? x y)
    (cond
      [x y]
      [else true]))
  
  
  ;; function-model?: function@ -> boolean
  ;; Checks to see if the given unit satisfies what we
  ;; expect out of functions, that their domain is total
  ;; and that each element of the domain maps to
  ;; just one element of the range.
  ;;
  ;; In first-order logic:
  ;;    (for all x, y, z: P(x, y) and P(x, z) implies y = z)
  ;;    and
  ;;    (for all x: there exists y: P(x, y))
  (define (function-model? model@)
    (local ((define-unit-binding a-model@
              model@ (import) (export function^))
            
            (define-unit function-tester@
              (import function^)
              (export)
              (and (for-all* (lambda (x y z)
                               (implies? (and (P x y) (P x z))
                                         (equal? y z)))
                             universe universe universe)
                   (for-all* (lambda (x)
                               (exists? (lambda (y) (P x y))
                                        universe))
                             universe))))
      (invoke-unit
       (compound-unit/infer
        (import)
        (export)
        (link a-model@ function-tester@)))))
  
  
  (define-unit squaring@
    (import)
    (export function^)
    (define universe (list 0 1 2 3 4 '>4))
    (define (P x y)
      (cond 
        [(equal? x '>4)
         (equal? y '>4)]
        [(> (* x x) 4)
         (equal? y '>4)]
        [else
         (equal? y (* x x))])))
  
  
  (define-unit less-than@
    (import)
    (export function^)
    (define universe '(1 2 3))
    (define (P x y)
      (< x y))))