Implementation of date arithmetic in Rosette

rosette-dates.rkt

#lang rosette
(require rosette/lib/angelic)

(require (except-in rosette < <= -)
         (prefix-in old (only-in rosette < <= -)))

(define-struct date [Y M D] #:transparent)

(define (is-leap-year Y) (and (= (remainder Y 4) 0) (=> (= (remainder Y 100) 0) (= (remainder Y 400) 0))))
(define (num-days Y M)
  (cond [(= M 1) 31]
        [(and (= M 2) (not (is-leap-year Y))) 28]
        [(and (= M 2) (is-leap-year Y)) 29]
        [(= M 3) 31]
        [(= M 4) 30]
        [(= M 5) 31]
        [(= M 6) 30]
        [(= M 7) 31]
        [(= M 8) 31]
        [(= M 9) 30]
        [(= M 10) 31]
        [(= M 11) 30]
        [(= M 12) 31]))
(define (assert-valid-date d) (assert (<= 1 (date-D d) (num-days (date-Y d) (date-M d)))))

(define (symbolic-date)
  (define-symbolic* Y integer?)
  (define M (choose* 1 2 3 4 5 6 7 8 9 10 11 12))        
  (define-symbolic* D integer?)
  (define d (make-date Y M D))
  (assert-valid-date d)
  d)


  

(define (date<= x y)
  (and (<= (date-Y x) (date-Y y))
       (=> (= (date-Y x) (date-Y y))
           (and (<= (date-M x) (date-M y))
                (=> (= (date-M x) (date-M y))
                    (<= (date-D x) (date-D y)))))))

(define (date< x y)
  (and (<= (date-Y x) (date-Y y))
       (=> (= (date-Y x) (date-Y y))
           (and (<= (date-M x) (date-M y))
                (=> (= (date-M x) (date-M y))
                    (< (date-D x) (date-D y)))))))

(define (days-since-start-of-year d)
  (define Y (date-Y d))
  (define M (date-M d))
  (define D (date-D d))
  (define is-leap (is-leap-year Y))
  (+ (- D 1) (if is-leap
                 (cond [(= M 1) 0]
                       [(= M 2) 31]
                       [(= M 3) 60]
                       [(= M 4) 91]
                       [(= M 5) 121]
                       [(= M 6) 152]
                       [(= M 7) 182]
                       [(= M 8) 213]
                       [(= M 9) 244]
                       [(= M 10) 274]
                       [(= M 11) 305]
                       [(= M 12) 335])
      
                 (cond [(= M 1) 0]
                       [(= M 2) 31]
                       [(= M 3) 59]
                       [(= M 4) 90]
                       [(= M 5) 120]
                       [(= M 6) 151]
                       [(= M 7) 181]
                       [(= M 8) 212]
                       [(= M 9) 243]
                       [(= M 10) 273]
                       [(= M 11) 304]
                       [(= M 12) 334]))))


(define (days-since-1900-01-01 d)
  (define y (date-Y d))
  (define yp (- y 1))
  
  ;; First, compute days from 1900-01-01 to y-01-01
  ;; We need to know how many of the 1900, 1901, ... (y-1) years are leap years
  ;; 1900, 1901, 1902, 1903, 1904, 1905, 1906, 1907, 1908, 1909, ...
  ;; First, say that every year divisible by 4 is a leap year:
  ;; 1900*, 1901, 1902, 1903, 1904*, 1905, 1906, 1907, 1908*, 1909, ...
  ;; leap years = 1 + (yp - 1900) / 4  (integer division round down)
  ;; but this overcounts, since divisible by 100 shouldn't be leap years, so adjust:
  ;; leap years = 1 + (yp - 1900) / 4 - (1 + (yp - 1900) / 100)
  ;; but this undercounts, since divisible by 400 should be leap years, so adjust:
  ;; leap years = 1 + (yp - 1900) / 4 - (1 + (yp - 1900) / 100) + (yp - 1600) / 400
  ;; simplify:
  ;; leap years = (yp - 1900) / 4 - (yp - 1900) / 100 + (yp - 1600) / 400

  (define num-full-years (- y 1900))
  (define num-leap-years (+ (- (quotient (- yp 1900) 4) (quotient (- yp 1900) 100)) (quotient (- yp 1600) 400)))
  (define num-normal-years (- num-full-years num-leap-years))
  (define days-in-1900-to-y-01-01 (+ (* 365 num-normal-years) (* 366 num-leap-years)))
  (+ days-in-1900-to-y-01-01 (days-since-start-of-year d)))
  

(define (date- x y)
  (- (days-since-1900-01-01 x) (days-since-1900-01-01 y)))



(define (<= . xs)
  (if (andmap date? xs)
      (for/and ([x xs]
                [y (cdr xs)])
        (date<= x y))
      (apply old<= xs)))

(define (< . xs)
  (if (andmap date? xs)
      (for/and ([x xs]
                [y (cdr xs)])
        (date< x y))
      (apply old<= xs)))

(define (- . xs)
  (if (andmap date? xs)
      (begin
        (assert (= (length xs) 2))
        (date- (first xs) (second xs)))
      (apply old- xs)))


;; WARNING --- DATE SUBTRACTION CURRENTLY WONT WORK RIGHT AT OR BEFORE 1900! ----
;; Ok, as long as other constraints make sure that doesn't happen


(define 2022-01-01 (make-date 2022 1 1))
(define 2023-01-01 (make-date 2023 1 1))
(define 2023-01-15 (make-date 2023 1 15))
(define x          (symbolic-date))

(assert (<= 2022-01-01 x))
(assert (<= x 2023-01-01))
(assert (> (- 2023-01-15 x) 30))


(define model (solve #t))
(evaluate x model)