;; Affine contracts as in the paper "Affine Contracts for Affine
;; Types" by Jesse Tov and Riccardo Pucella, as submitted to ICFP'09.

#lang scheme

;;;;;
;;;;; Affine procedures
;;;;;

;; affine-procedure/c : contract?
;;
;; Contract for one-shot procedures -- checks that the procedure
;; is applied only once, but isn't concerned with the procedure's
;; domain and range.  Can only produce *negative* blame.
(define affine-procedure/c
  (make-proj-contract
   'affine-procedure/c
   (lambda (pos neg src name)
     (lambda (f)
       (if (procedure? f)
           (let ([blessed #t])
             (make-keyword-procedure
              (lambda (keys vals . args)
                (if blessed
                    (begin
                      (set! blessed #f)
                      (keyword-apply f keys vals args))
                    (raise-contract-error
                     f
                     src
                     neg
                     name
                     "affine function applied more than once")))))
           (raise-contract-error
            f
            src
            pos
            name
            "expected affine procedure, given: ~e"
            f))))
   procedure?))

;; (-o dom ... range)
;;
;; Contract for affine procedures, including domain and range
;; as in ->
(define-syntax -o
  (syntax-rules ()
    [(-o ARGS ...) (and/c (-> ARGS ...) affine-procedure/c)]))

;; (-o* (mandatory-dom ...) (optional-dom ...) rest range)
;;
;; Contract for affine procedues, as in ->*
(define-syntax -o*
  (syntax-rules ()
    [(-o* ARGS ...) (and/c (->* ARGS ...) affine-procedure/c)]))

(provide/contract
 [affine-procedure/c  contract?])

(provide -o -o*)

;;;;;
;;;;; Affine boxes
;;;;;

;; An affine box is represented as a struct containing
;; a thunk that either returns the boxed value or raises
;; a contract error.

;; make-affine-box-type : (X : symbol?)
;;   -> (values (any -> X)
;;              (any -> boolean?)
;;              (X -> any)
;;              (contract? -> contract?))
;;
;; To make a new affine box type.  Given its name (a symbol), returns
;; a constructor, a predicate, an accessor, and a function which, given
;; a contract c?, returns a contract for boxes containing a c?.
;;
;; make-affine-box-type : (X : symbol?) contract?
;;   -> (values (any -> X)
;;              (any -> boolean?)
;;              (X -> any)
;;              contract?)
;;
;; If the optional second argument is a contract X, then the fourth
;; return value is a contract checking for boxes containing X.
(define make-affine-box-type
  (case-lambda
    [(type-name)
     (define-values (affine-box make-affine-box affine-box?
                                affine-box-ref set-affine-box!)
                    (make-struct-type type-name
                                      #f
                                      1
                                      0))
     (define (rename fmt proc)
       (procedure-rename proc
                         (string->symbol
                           (format fmt type-name))))
     (values
       ;; constructor
       (rename "make-~a"
               (lambda (val) (make-affine-box (lambda () val))))
       ;; predicate
       (rename "~a?"
               affine-box?)
       ;; accessor
       (rename "~a-ref"
               (lambda (ab) ((affine-box-ref ab 0))))
       ;; contract
       (rename "~a/c"
               (lambda (c)
                 (let ([ctc (coerce-contract 'affine-box/c c)])
                   (make-proj-contract
                     (build-compound-type-name 'affine-box/c c)
                     (lambda (pos neg src name)
                       (lambda (ab)
                         (if (affine-box? ab)
                           (let ([blessed #t])
                             (make-affine-box
                               (lambda ()
                                 (if blessed
                                   (begin
                                     (set! blessed #f)
                                     ((((proj-get ctc) ctc) pos neg src name)
                                      ((affine-box-ref ab 0))))
                                   (raise-contract-error
                                     ab
                                     src
                                     neg
                                     name
                                     "~a unboxed more than once"
                                     type-name)))))
                           (raise-contract-error
                             ab
                             src
                             pos
                             name
                             "expected ~a, given: ~e"
                             type-name
                             ab))))
                     affine-box?)))))]
    [(type-name contract)
     (let-values ([(box box? box-ref box/c)
                   (make-affine-box-type type-name)])
                 (values
                   box box? box-ref (box/c contract)))]))

;; (define-affine-box box-name)
;;
;; Create a new affine box type, with constructor make-box-name,
;; predicate box-name?, selector box-name-ref, and contract maker
;; box-name/c.
;;
;; (define-affine-box box-name contract?)
;;
;; As with make-affine-box-type, we may give a contract for the
;; permissible contents of the box.
(define-syntax define-affine-box
  (lambda (stx)
    (syntax-case stx ()
      [(define-affine-box type-name rest ...)
       (begin
         (define (name fmt)
           (datum->syntax
             stx
             (string->symbol
               (format fmt (syntax->datum (syntax type-name))))
             stx))
         (identifier? (syntax type-name))
         (quasisyntax
           (define-values
             ((unsyntax (name "make-~a"))
              (unsyntax (name "~a?"))
              (unsyntax (name "~a-ref"))
              (unsyntax (name "~a/c")))
             (make-affine-box-type 'type-name rest ...))))])))

(define-affine-box affine-box)

(provide/contract
 [make-affine-box     (any/c . -> . affine-box?)]
 [affine-box?         (any/c . -> . boolean?)]
 [affine-box-ref      (affine-box? . -> . any/c)]
 [affine-box/c        (contract? . -> . contract?)])

(provide
  make-affine-box-type
  define-affine-box)