;; dvanhorn@cs.uvm.edu
;; Contract for SRFI 19 time.ss
;; Initial negotiation Mon Mar 15 18:40:43 EST 2004

(module time-contract mzscheme
  (require (lib "contract.ss")
           (lib "time.ss" "srfi" "19"))
  
  ;; Contract Helpers
  ;; FIXME: Moving these defns below the provide/contract form causes
  ;; "reference to an identifier before its definition" errors, which
  ;; seems like a bug given this is a module.
  (define (tm:time-duration? x)
    (and (time? x) (equal? (time-type x) time-duration)))
  (define (tm:time-monotonic? x)
    (and (time? x) (equal? (time-type x) time-monotonic)))
  (define (tm:time-process? x)
    (and (time? x) (equal? (time-type x) time-process)))
  (define (tm:time-tai? x)
    (and (time? x) (equal? (time-type x) time-tai)))
  (define (tm:time-thread? x)
    (and (time? x) (equal? (time-type x) time-thread)))
  (define (tm:time-utc? x)
    (and (time? x) (equal? (time-type x) time-utc)))
  (define tm:jd? number?)  ;; Should negatives be included?
  (define tm:mjd? number?)
  
  ;; Curried time type equality
  ;; time -> time -> bool => #t when type t1 = type t2
  (define (tm:time-type=* t1)
    (lambda (t2)
      (equal? (time-type t1) (time-type t2))))
  
  ;; Curried distinct memory location predicate
  (define (tm:neq?* x)
    (lambda (y)
      (not (eq? x y))))
  
  ;; any -> bool => #t when s is a time-type
  (define (tm:time-type? x)
    (ormap (lambda (y) (equal? x y))
           (list time-tai time-utc time-monotonic time-thread
                 time-process time-duration time-gc)))
  
  ;; end of contract helpers
  
  ;; Contract for SRFI 19
  ;; ====================
  (provide/contract
   
   ;; Constants
   ;; =========
   (time-tai       symbol?)
   (time-utc       symbol?)
   (time-monotonic symbol?)
   (time-thread    symbol?)
   (time-process   symbol?)
   (time-duration  symbol?)
   (time-gc        symbol?) ;; MzScheme extension
   
   ;; Current time and clock resolution
   ;; =================================
   (current-date                (opt-> () (integer?) srfi:date?))
   (current-julian-day          (-> tm:jd?))
   (current-modified-julian-day (-> tm:mjd?))
   (current-time                (opt-> () (tm:time-type?) time?))
   (time-resolution             (opt-> () (tm:time-type?) integer?))
   
   ;; Time object and accessors
   ;; =========================
   (make-time       (-> tm:time-type? (integer-in 0 9999999) integer? time?))
   (time?           (-> any? boolean?))
   (time-type       (-> time? tm:time-type?))
   (time-nanosecond (-> time? (integer-in 0 9999999)))
   (time-second     (-> time? integer?))
   
   (set-time-type!       (-> time? tm:time-type? void?))
   (set-time-nanosecond! (-> time? (integer-in 0 9999999) void?))
   (set-time-second!     (-> time? integer? void?))
   
   ;; relies on inspector
   (copy-time            (->d time? 
                              (lambda (in) 
                                (and/c
                                 (lambda (out) (equal? in out))
                                 (tm:neq?* in)))))

   ;; Time comparison procedures
   ;; ==========================
   (time<=? (->r ((x time?) (_ (and/c time? (tm:time-type=* x)))) boolean?))
   (time<?  (->r ((x time?) (_ (and/c time? (tm:time-type=* x)))) boolean?))
   (time=?  (->r ((x time?) (_ (and/c time? (tm:time-type=* x)))) boolean?))
   (time>=? (->r ((x time?) (_ (and/c time? (tm:time-type=* x)))) boolean?))
   (time>?  (->r ((x time?) (_ (and/c time? (tm:time-type=* x)))) boolean?))
   
   ;; Time arithmetic procedures
   ;; ==========================
   (time-difference    (->r ((x time?) (y (and/c time? (tm:time-type=* x))))
                            (and/c tm:time-duration? 
                                   (tm:neq?* x) 
                                   (tm:neq?* y))))
   (time-difference!   (->r ((x time?) (_ (and/c time? (tm:time-type=* x))))
                            tm:time-duration?))
   (add-duration       (->r ((x time?) (_ tm:time-duration?))
                            (and/c (tm:time-type=* x) (tm:neq?* x))))
   (add-duration!      (->r ((x time?) (_ tm:time-duration?)) 
                            (tm:time-type=* x)))
   (subtract-duration  (->r ((x time?) (_ tm:time-duration?))
                            (and/c (tm:time-type=* x) (tm:neq?* x))))
   (subtract-duration! (->r ((x time?) (_ tm:time-duration?))
                            (tm:time-type=* x)))
   
   ;; Date object and accessors
   ;; =========================
   (make-srfi:date (-> (integer-in 0 9999999) ;; nanoseconds
                       (integer-in 0 60)      ;; seconds
                       (integer-in 0 59)      ;; minutes
                       (integer-in 0 23)      ;; hour
                       (integer-in 0 31)      ;; day
                       (integer-in 0 12)      ;; month
                       integer?               ;; year
                       integer?               ;; zone-offset
                       srfi:date?))
   (srfi:date?       (-> any? boolean?))
   (date-nanosecond  (-> srfi:date? (integer-in 0 9999999)))
   (srfi:date-second (-> srfi:date? (integer-in 0 60)))
   (srfi:date-minute (-> srfi:date? (integer-in 0 59)))
   (srfi:date-hour   (-> srfi:date? (integer-in 0 23)))
   (srfi:date-day    (-> srfi:date? (integer-in 0 31)))
   (srfi:date-month  (-> srfi:date? (integer-in 0 12)))
   (srfi:date-year   (-> srfi:date? integer?))
   (date-zone-offset (-> srfi:date? integer?))
   (date-year-day    (-> srfi:date? integer?))
   (date-week-day    (-> srfi:date? integer?))
   (date-week-number (-> srfi:date? integer?))
   
   ;; Time/Date/Julian Day/Modified Julian Day Converters
   ;; ===================================================
   (date->julian-day              (-> srfi:date? tm:jd?))
   (date->modified-julian-day     (-> srfi:date? tm:mjd?))
   (date->time-monotonic          (-> srfi:date? tm:time-monotonic?))
   (date->time-tai                (-> srfi:date? tm:time-tai?))
   (date->time-utc                (-> srfi:date? tm:time-utc?))
   
   (julian-day->date              (opt-> (tm:jd?) (integer?) srfi:date?))
   (julian-day->time-monotonic    (-> tm:jd? tm:time-monotonic?))
   (julian-day->time-tai          (-> tm:jd? tm:time-tai?))
   (julian-day->time-utc          (-> tm:jd? tm:time-utc?))
   
   (modified-julian-day->date (opt-> (tm:mjd?) (integer?) srfi:date?))
   (modified-julian-day->time-monotonic (-> tm:mjd? tm:time-monotonic?))
   (modified-julian-day->time-tai       (-> tm:mjd? tm:time-tai?))
   (modified-julian-day->time-utc       (-> tm:mjd? tm:time-utc?))
   
   (time-monotonic->date (opt-> (tm:time-monotonic?) (integer?) srfi:date?))
   (time-monotonic->julian-day          (-> tm:time-monotonic? tm:jd?))
   (time-monotonic->modified-julian-day (-> tm:time-monotonic? tm:mjd?))
   (time-monotonic->time-tai            (-> tm:time-monotonic? tm:time-tai?))
   (time-monotonic->time-tai!           (-> tm:time-monotonic? tm:time-tai?))
   (time-monotonic->time-utc            (-> tm:time-monotonic? tm:time-utc?))
   (time-monotonic->time-utc!           (-> tm:time-monotonic? tm:time-utc?))
   
   (time-tai->date (opt-> (tm:time-tai?) (integer?) srfi:date?))
   (time-tai->julian-day          (-> tm:time-tai? tm:jd?))
   (time-tai->modified-julian-day (-> tm:time-tai? tm:mjd?))
   (time-tai->time-monotonic      (-> tm:time-tai? tm:time-monotonic?))
   (time-tai->time-monotonic!     (-> tm:time-tai? tm:time-monotonic?))
   (time-tai->time-utc            (-> tm:time-tai? tm:time-utc?))
   (time-tai->time-utc!           (-> tm:time-tai? tm:time-utc?))
   
   (time-utc->date (opt-> (tm:time-utc?) (integer?) srfi:date?))
   (time-utc->julian-day          (-> tm:time-utc? tm:jd?))
   (time-utc->modified-julian-day (-> tm:time-utc? tm:mjd?))
   (time-utc->time-monotonic      (-> tm:time-utc? tm:time-monotonic?))
   (time-utc->time-monotonic!     (-> tm:time-utc? tm:time-monotonic?))
   (time-utc->time-tai            (-> tm:time-utc? tm:time-tai?))
   (time-utc->time-tai!           (-> tm:time-utc? tm:time-tai?))
   
   ;; Date to String/String to Date Converters
   ;; ========================================
   (date->string (opt-> (srfi:date?) (string?) string?))
   (string->date (-> string? string? srfi:date?))
   
   ) ;; end of provide/contract for srfi-19.
  ) ;; end of module time-contract
