(module address-book-1 mzscheme
  ;; manual translation of the addressBook1 example
  ;; from Software Abstractions.
  
  ;; The system is described by four relations: 
  ;; Book, Name, Addr, and Book-addr.  
  ;; (The last is implicit from the sig description.
  (require "relations.ss")
  
  (provide transaction
           let-transaction
           
           make-Name
           make-Addr
           make-Book
           current-context
           
           add)
  
  
  (define current-context (make-parameter (make-context)))
  (define current-constraints (make-parameter '()))
  
  
  (define (push-new-constraint! constraint)
    (current-constraints (cons constraint (current-constraints))))
  
  
  ;; make-Name: datum -> relation
  (define (make-Name datum)
    (let ([r (make-singleton-relation datum)])
      (push-new-constraint!
       (constrain-relation-contains 'Name r))
      r))
  
  
  ;; make-Addr: datum -> relation
  (define (make-Addr datum)
    (let ([r (make-singleton-relation datum)])
      (push-new-constraint!
       (constrain-relation-contains 'Addr r))
      r))
  
  
  ;; make-Book: datum -> relation
  (define (make-Book datum)
    (let ([r (make-singleton-relation datum)])
      (push-new-constraint!
       (constrain-relation-contains 'Book r))
      r))
  
  
  
  ;; pred add(b, b': Book, n: Name, a: Addr) { b'.addr = b.addr + n->a }
  (define (add b b-prime n a)
    (constrain-equal (dot b-prime 'addr)
                     (sum
                      (dot b 'addr)
                      (arrow n a)))
    ;; Just returning a blanket #t is cheating; we shouldn't
    ;; be able to tell that we succeeded until the contrain-equal
    ;; is good.
    #t)
  
  
  (define (apply-constraint constraint)
    (constraint))
  
  (define (constrain-relation-contains relation-name other-relation)
    (lambda ()
      (context-set!
       (current-context)
       relation-name
       (relation-add
        (context-get (current-context) relation-name)
        other-relation))))
  
  
  ;; let-transaction: syntax
  ;; binding form: all the v values are evaluated in the context
  ;; of a transaction.
  (define-syntax (let-transaction stx)
    (syntax-case stx ()
      [(_ ([n v] ...)
          body ...)
       (syntax/loc stx
         (let-values ([(n ...)
                       (transaction
                        (values v ...))])
           body ...))]))
  
  
  (define-syntax (transaction stx)
    (syntax-case stx ()
      [(_ constraint-expr ...)
       (syntax/loc stx
         (transaction*
          (lambda () constraint-expr ...)))]))
  
  
  ;; I'm thinking that all the operations will be done within a
  ;; transaction.  The transaction should be responsible for
  ;; figuring out what needs to be stored in the database to 
  ;; satisfy the constraints.
  (define (transaction* constraint-accumulating-thunk)
    (parameterize ([current-constraints '()])
      (call-with-values
       constraint-accumulating-thunk
       (lambda vals
         (for-each apply-constraint (current-constraints))
         (apply values vals)))))
  
  
  ;; constrain-equal: constraint constraint -> constraint
  ;; I'm cheating here; I have to talk with Kathi and others to
  ;; see how to do this right.  I'm thinking I'll need to 
  ;; do some kind of unification?
  (define (constrain-equal lhs rhs)
    (lambda () (void)))
  
  
  ;; dot: constraint constraint -> constraint
  (define (dot lhs rhs)
    (void))
  
  ;; arrow: constraint constraint -> constraint
  (define (arrow lhs rhs)
    (void))
  
  ;; sum: constraint constraint -> constraint
  (define (sum lhs rhs)
    (void))
  
  
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  
  ;; pred del(b, b': Book, n: Name) {b'.addr = b.addr - n->Addr}
  (define (del)
    (void))
  
  ;; fun lookup(b : Book, n: Name): set Addr {n.(b.addr)}
  (define (lookup)
    (void))
  
  
  (define (show)
    (void)))