#lang s-exp rosette

(require racket/gui/base)

(require "../core/wallingford.rkt")

(require "../applications/geothings.rkt")

(require "abstract-reactive-thing.rkt")

(require "reactive-macros.rkt")

(require (only-in racket [when racket-when]))

(provide when while racket-when max-value min-value integral reactive-thing% interesting-time?)

(define reactive-thing%

(class abstract-reactive-thing%

(super-new)

(define when-holders '()) ; list of whens

(define linearized-when-holders '())

(define while-holders '())

; symbolic-time is this thing's idea of the current time. It is in milliseconds, and is relative to time-at-startup.

(define-symbolic* symbolic-time real?)

; start time out at 0 (perhaps redundantly, this thing should also get an initialize message after all the constraints are added)

; not sure whether we need to do both, but this way means the stay is ok

(assert (equal? symbolic-time 0))

(send this solve)

(stay symbolic-time)

(define/override (start)

(update-time 0))

; to implement previous, we just need to evaluate the expression in the current (i.e. old) solution

(define/public (previous expr)

(send this wally-evaluate expr))

; these methods are for use by the macros (not for general public use, despite the 'public' declaration)

(define/public (add-when-holder w)

(set! when-holders (cons w when-holders)))

(define/public (add-linearized-when-holder w)

(set! linearized-when-holders (cons w linearized-when-holders)))

(define/public (add-while-holder w)

(set! while-holders (cons w while-holders)))

; max-min-values holds the current max (or min) value for a max-value or min-value expression, indexed by

; a gensym'd id for that occurence of max-value or min-value. Note that when linearizing a when condition,

; max-min-values will just be for the larger time of the interval being linearized.

(define max-min-values (make-hasheq))

; symbolic-integral-values is similar to max-min-values, except for integral expressions

(define symbolic-integral-values (make-hasheq))

; numeric-integral-values is also similar to max-min-values, except that the value is an instance of nstruct

(define numeric-integral-values (make-hasheq))

(struct nstruct (dt ; the delta time for the *next* time advance

var-value ; the value of the variable of integration when the integral expression was evaluated

expr-value ; the value of expr at that same time time

sum ; the cumulative sum of the values so far (i.e., the integral so far)

) #:transparent)

; linearized-tests are computed as we linearize whens - the keys are the ids for those whens. This assumes that they

; are computed for the current update-time, so we can just keep replacing the old ones.

(define linearized-tests (make-hasheq))

; struct to hold a linearized test (valid for times between first and last)

(struct linearized-test (expr first last) #:transparent)

(define/public (max-min-helper max-or-min f id interesting)

; For max-value: if max-value isn't initialized yet or if this is the first time in the while, save the current maximum

; and otherwise update it by finding the max of the old and new values. And analogously for min-value.

(let ([updated-value (if (or (not (hash-has-key? max-min-values id)) (eq? interesting 'first))

(f)

(max-or-min (f) (hash-ref max-min-values id)))])

(hash-set! max-min-values id updated-value)

updated-value))

; runtime function for code generated by integral macro for symbolic integration -- this should evaluate to the

; correct value for (integral expr) at the current time

(define/public (integral-symbolic-run-time-fn f id interesting)

; If the value for this integral isn't stored already, or if this is the first time through a 'while', save that value.

; Hack (hopefully temporary): if time=0, also save the value (i.e., reset the value for this integral). This is

; to get around a bug where the integral expression is being evaluated on startup before all variables have values.

(cond [(or (not (hash-has-key? symbolic-integral-values id)) (eq? interesting 'first) (equal? (send this milliseconds-evaluated) 0))

(hash-set! symbolic-integral-values id (f))

0]

[else (- (f) (hash-ref symbolic-integral-values id))]))

; Version of runtime integral method for use with code for numeric integration. Calling this method should return the current

; value of (integral expr) plus do some bookkeeping.

(define/public (integral-numeric-run-time-fn var-fn expr-fn id interesting dt)

(let* ([new-var-value (send this wally-evaluate (var-fn))]

[new-expr-value (send this wally-evaluate (expr-fn))]

; See if there is already a saved value for this id, if so use it. Hack (similar to symbolic evaluation hack):

; if time=0, ignore the old value, so that instead we *replace* it if present, to get around the bug where the

; integral expression is being evaluated on startup before all variables have values.

[new-sum (if (and (hash-has-key? numeric-integral-values id) (> (send this milliseconds-evaluated) 0))

(let* ([oldstruct (hash-ref numeric-integral-values id)]

[delta-sum (* 1/2 (+ new-expr-value (nstruct-expr-value oldstruct))

(- new-var-value (nstruct-var-value oldstruct)))])

(+ (nstruct-sum oldstruct) delta-sum))

0)])

(if (eq? interesting 'last)

(hash-remove! numeric-integral-values id)

(hash-set! numeric-integral-values id (nstruct dt new-var-value new-expr-value new-sum)))

new-sum))

(define/override (milliseconds)

symbolic-time)

(define/override (milliseconds-evaluated)

(send this wally-evaluate symbolic-time))

(define/override (concrete-image)

(send this wally-evaluate (send this image)))

; The variables push-sampling and pull-sampling say whether to do push or pull sampling respectively.

; (Note that we can do neither, just push sampling, just pull sampling, or both.)

; push-sampling starts out as null, and then is set to #t or #f the first time the (get-sampling) function

; is called. It doesn't change after that. pull-sampling starts out as an empty set. Whenever we enter

; a 'while' that needs pull sampling, we add the id for that 'while' to the pull-sampling set, and when we

; leave the 'while' we remove it. In addition, if there are 'always' constraints that imply we need to do

; pull sampling for the lifetime of the entire program, we add an id to pull-sampling (and never remove it).

; So if pull-sampling is a non-empty set, we do pull sampling at that time.

(define push-sampling null)

(define pull-sampling (mutable-set))

(define current-sampling #f) ; for saving the sampling, so that we can notify viewers if it changes

; The get-sampling method should return one of '() '(push) '(pull) or '(push pull)

(define/override (get-sampling)

(cond [(null? push-sampling) ; need to initialize things

; if there are when or while constraints, sampling should include push

(set! push-sampling (or (not (null? when-holders)) (not (null? while-holders))))

; If any of the always constraints include a temporal reference, sampling should always include pull,

; so add a token (for no good reason named 'always) to the set that will always be there.

(cond [(pull-sampling? (send this get-always-code)) (set-add! pull-sampling 'always)])

; If any while constraints are first active at the current time, add their ids to pull-sampling.

; Temporary (?) hack: if there are while constraints that are active at time 0, be sure and call

; get-sampling after the object is created so that this will be initialized properly.

(for ([w while-holders])

(let ([why (send this wally-evaluate ((while-holder-interesting w)))]

[id (while-holder-id w)]

[pull? (while-holder-pull? w)])

; 'why' is why this time is interesting, or #f if it's not

; 'id' is the unique ID for this while

(cond [(and (eq? why 'first) pull?) (set-add! pull-sampling id)])))])

; Once we get here, the variables are initialized. Return the kind of sampling to use.

(append (if push-sampling '(push) '()) (if (set-empty? pull-sampling) '() '(pull))))

; Find a time to advance to. This will be the smaller of the target and the smallest value that makes a

; 'when' test true or is an interesting time for a 'while'. If there aren't any such values

; between the current time and the target, then just return the target. Note that the calls to solve in this

; method don't change the current solution, which is held in an instance variable defined in thing%.

; Additionally, if there are constraints that use delta time (active numeric integral constraints or when

; constraints with the #:linearize option set), we can't advance by more than the smallest of the dt's --

; adjust the target time accordingly. Return two values: the time to advance to, and either #f or a new target.

; (The new target is used if we are doing a binary search for a time to advance to.)

(define/override (find-time mytime initial-target)

; For all active numeric integral expressions and when constraints with the #:linearize option set, find the

; smallest new times for each as the sum of the current time plus its dt (delta time). The target time will

; then be the minimum of the initial-target (supplied as an argument to this method) and the possible new times

; for each of the active numeric integral expressions and linearized when constraints.

;

; (printf "start of find-time mytime ~a initial-target ~a \n" (exact->inexact mytime) (exact->inexact initial-target))

(let* ([active-integral-times (map (lambda (n) (+ mytime (nstruct-dt n))) (hash-values numeric-integral-values))]

[linearized-when-times (map (lambda (n) (+ mytime (linearized-when-holder-dt n))) linearized-when-holders)]

[target (apply min (cons initial-target (append active-integral-times linearized-when-times)))])

; (printf "target ~a \n" (exact->inexact target))

; If there aren't any when or while statements, just return the target time, otherwise solve for the time

; to which to advance.

(cond [(and (null? when-holders) (null? linearized-when-holders) (null? while-holders)) (values target #f)]

[else (define solver (current-solver)) ; can use direct calls to solver b/c we aren't doing finitization!

; add all required always constraints and stays to the solver (this needs to be done before linearizing whens)

(send this solver-add-required solver)

; interesting-time says that either symbolic-time is the target time, or a time such that the test on a

; when holds, or it's an interesting time for a while. Define this first, and then assert later, since in the

; process of defining it we assert some constraints when linearizing.

(define interesting-time (or (equal? symbolic-time target)

(and (< symbolic-time target)

(or (ormap (lambda (w) ((when-holder-test w))) when-holders)

(ormap (lambda (w) (linearize-when w mytime target)) linearized-when-holders)

(ormap (lambda (w) ((while-holder-interesting w))) while-holders)))))

; (printf "interesting-time ~a \n linearized-when-holders ~a \n lineared-tests ~a \n" interesting-time linearized-when-holders

; (map (lambda (w) (linearize-when w mytime target)) linearized-when-holders))

(assert (> symbolic-time mytime))

(assert interesting-time)

(solver-assert solver (asserts))

; this doesn't work: (solver-assert solver (list (> symbolic-time mytime) interesting-time))

(solver-minimize solver (list symbolic-time)) ; ask Z3 to minimize the symbolic time objective

(define sol (solver-check solver))

(define min-time (evaluate symbolic-time sol))

; make sure that this is indeed a minimum (not an infinitesimal)

; trying to advance time by an infinitesimal amount could loop forever

(solver-assert solver (list (< symbolic-time min-time)))

(unless (unsat? (solver-check solver))

(error 'find-time "can only advance time by an infinitesimal amount"))

(clear-asserts!)

(solver-clear solver)

; make sure we aren't stuck

(racket-when (equal? mytime min-time)

(error 'find-time "unable to find a time to advance to that is greater than the current time"))

; If min-time might be due to a linearized test returning #t, we may want to refine the estimate, since it will

; in general be an approximation. First check for termination in this case: if find-time is being called with

; a target less than epsilon from mytime, we are looking at a very small interval, and presumably the

; linearization is reasonably accurate within that small interval. In that case terminate and return min-time.

; (The epsilon in this test is a property of the linearized when.) Otherwise call find-time again with a target

; half the distance from mytime, so that this will do a binary search. The initial dt is specified by the when

; holder -- it should be such that we don't miss a true minimum time. (This would happen, for example, with

; a test involving a sin function and a dt that just jumped to the next 0 of the expression.)

; Some possibilities for alternate algorithms that would (on the other hand) be more complicated to implement:

; rather than a binary search, it would probably be more efficient to try to refine the search to an interval

; around min-time. A different termination test, which might result in fewer iterations, would be to turn the

; test into an expression whose value is 0 iff the test is satisfied, and check whether the actual value of the

; test expression is within epsilon of the value of the linearized version of the expression at min-time.

(define active-linearized-whens (filter (lambda (w) (send this wally-evaluate (lookup-linearized-test w) sol)) linearized-when-holders))

(define min-epsilon (if (null? active-linearized-whens) #f (apply min (map linearized-when-holder-epsilon active-linearized-whens))))

(cond [(and min-epsilon (> (- target mytime) min-epsilon))

; (printf "recursive call in find-time target ~a mytime ~a \n" (exact->inexact target) (exact->inexact mytime))

(let-values ([(ans revised-target) (find-time mytime (+ mytime (/ (- target mytime) 2)))])

; (printf "about to return from recursive call in find-time mytime ~a target ~a min-time ~a ans ~a revised-target ~a \n"

; (exact->inexact mytime) (exact->inexact target) (exact->inexact min-time) (exact->inexact ans)

; (if revised-target (exact->inexact revised-target) revised-target))

(values ans (if revised-target revised-target target)))]

[else

; (printf "about to return from NONrecursive call in find-time mytime ~a min-time ~a target ~a \n"

; (exact->inexact mytime) (exact->inexact min-time) (exact->inexact target))

(values min-time #f)])])))

; Advance time to the smaller of the target and the smallest value that makes a 'when' test true or is an

; interesting time for a 'while'. Solve all constraints in active when and while constraints.

; If we advance time to something less than 'target', call advance-time-helper again.

; To accommodate a binary search for a time, we can also have a revised-target, which will be either just target

; (the normal case), or some time less than target (if we are doing a recursive search)

(define/override (advance-time-helper target [revised-target target])

(let ([mytime (send this milliseconds-evaluated)])

; (printf "start of advance-time-helper target ~a revised-target ~a mytime ~a \n"

; (exact->inexact target) (exact->inexact revised-target) (exact->inexact mytime))

; make sure we haven't gone by the target time already - if we have, don't do anything

(racket-when (< mytime revised-target)

(let-values ([(next-time new-revised-target) (find-time mytime revised-target)])

(update-time next-time)

; If new-revised-target is not #f, then we are doing a search for a time, and need to get to new-revised-target first,

; before tackling target

; (printf "after update-time my-actual-time ~a next-time ~a revised-target ~a new-revised-target ~a target ~a \n"

; (exact->inexact (send this milliseconds-evaluated)) (exact->inexact next-time)

; revised-target

; (if new-revised-target (exact->inexact new-revised-target) new-revised-target) (exact->inexact target))

(racket-when new-revised-target

; (printf "doing recursive call to advance-time-helper because new-revised-target is not #f \n")

(advance-time-helper target new-revised-target))

; if we didn't get to revised-target try again (note that this is independent of the new-revised-target stuff)

(racket-when (< next-time revised-target)

; (printf "doing recursive call to advance-time-helper because next-time ~a is less than revised-target ~a (target is ~a) \n"

; (exact->inexact next-time) (exact->inexact revised-target) (exact->inexact target))

(advance-time-helper revised-target))))))

; Return an expression that is a linearized version of the when test for linearized-when-holder w.

; To do this, see if there is already a cached linearized test that is currently valid (i.e., its last time

; is greater than mytime). If so, use its expression; otherwise generate a new one and cache it (potentially overwriting

; an old one whose end time has already passed).

(define (linearize-when w mytime target)

; (printf "calling linearize-when id ~a mytime ~a target ~a \n" (when-holder-id w) (exact->inexact mytime) (exact->inexact target))

(let ([c (hash-ref linearized-tests (when-holder-id w) #f)])

;(racket-when c (printf "found existing test first ~a last ~a \n"

; (exact->inexact (linearized-test-first c)) (exact->inexact (linearized-test-last c))))

; existing test is OK if the *first* time is <= mytime ---- but the last must exactly equal target

(if (and c (<= (linearized-test-first c) mytime) (= (linearized-test-last c) target))

(linearized-test-expr c)

(let ([d (= 0 (linearize (linearized-when-holder-linearized-test w) (when-holder-id w) mytime target))])

(hash-set! linearized-tests (when-holder-id w) (linearized-test d mytime target))

; (printf "updating test -- new test ~a \n" d)

d))))

; Return a symbolic expression that is a linear approximation of the value of f (a thunk) at symbolic-time. mytime is the

; current time, and target is the target new time. We will advance to target or something sooner -- in other words, the

; linear approximation is assumed valid just for the interval [mytime,target]. id is an id for expr, for caching.

(define (linearize f id mytime target)

; (printf "calling linearize f ~a id ~a mytime ~a target ~a \n" f id mytime target)

(let ([dt (- target mytime)]

[e0 (find-value f id mytime)]

[e1 (find-value f id target)])

(+ e0 (/ (* (- symbolic-time mytime) (- e1 e0)) dt))))

; Helper functions for linearize. find-value looks up the cached value of the expression identified by id for the given time,

; or computes it if not already in the cache and remembers it. linearized-value-cache is the cache. The keys are (id,time) pairs

; and the values are the corresponding values of the expression. This function assumes that the required constraints are in the

; solver's assertion store (added earlier using the solver-add-required method).

(define (find-value f id time)

(hash-ref! linearized-value-cache (cons id time) (lambda () (compute-linearized-value f id time))))

(define (compute-linearized-value f id time)

(define solver (current-solver))

; don't need to add required constraints - they should already been there

; (send this solver-add-required solver)

(solver-push solver)

(solver-assert solver (list (equal? symbolic-time time)))

(define sol (sol->exact (solver-check solver)))

; (printf "in compute-linearized-value time ~a value ~a sol ~a \n" time (evaluate (f) sol) sol)

(solver-pop solver)

(evaluate (f) sol))

(define linearized-value-cache (make-hash))

; helper function - either look up the cached linearized test for when holder w, or if none return its normal test

(define (lookup-linearized-test w)

;(printf "in lookup-linearized-test current time ~a newtime ~a w ~a linearized-tests ~a \n" (send this milliseconds-evaluated)

; newtime w linearized-tests)

(let ([c (hash-ref linearized-tests (when-holder-id w) #f)])

;(printf "c ~a actual test ~a \n" c ((when-holder-test w)))

(if c (linearized-test-expr c) ((when-holder-test w)))))

; helper method -- update my time to newtime

(define (update-time newtime)

; (printf "in update-time newtime ~a \n" (exact->inexact newtime))

(let ([notify-changed #f])

(assert (equal? symbolic-time newtime))

(define saved-asserts (asserts))

; Solve all constraints and then find which when tests hold. Put those whens in active-whens.

(send this solve)

(define active-whens (filter (lambda (w) (send this wally-evaluate ((when-holder-test w)))) when-holders))

(define active-linearized-whens (filter (lambda (w) (send this wally-evaluate (lookup-linearized-test w))) linearized-when-holders))

(define active-whiles (filter (lambda (w) (send this wally-evaluate ((while-holder-test w)))) while-holders))

; Assert the constraints in all of the bodies of the active whens and whiles. Also, solving clears the

; global assertion store, so add that back in. This includes the assertion that symbolic-time

; equals next-time. Then solve again.

(for-each (lambda (w) ((when-holder-body w))) active-whens)

(for-each (lambda (w) ((when-holder-body w))) active-linearized-whens)

; provide a parameter interesting-time? that is bound to a value indicating whether the current time is interesting,

; and evaluate the while-holder's body in that environment

(for-each (lambda (w) (parameterize ([interesting-time? (send this wally-evaluate ((while-holder-interesting w)))])

((while-holder-body w))))

active-whiles)

(for-each (lambda (a) (assert a)) saved-asserts)

(send this solve)

; Update the sampling regime if necessary, and if this object might have changed, notify viewers.

; First check if interesting-time is true for any while constraints. Do this before potentially

; updating the sampling regime and notifying any viewers, since this potentially affects both.

; We check all of the while constraints, not just the active ones, since in some cases interesting-time

; is true just before the while becomes active. If interesting-time is true for any while constraints:

; - Set notify-changed to true. (Even if we are using pull sampling, we want to do an extra push notification

; so that the viewer updates immediately. This is important for the end of the interval in which a 'while'

; holds, since often that will be the last state the object is in. Also, for good responsiveness we want to

; do it at the beginning of the interval in which the 'while' holds. And if it's just some other interesting

; time, well, maybe it's interesting for some reason ... so update then as well (this last is less clear-cut).

; - If this is the first time the while constraint holds, and if it includes temporal constraints in

; the body, then viewers of this thing should use pull notification as long as the constraint is

; active. To set this up, add the token for the while to the set pull-sampling.

; - If this is the last time that the while constraint holds, remove its token from the set pull-sampling

; if present.

(for ([w while-holders])

(let ([why (send this wally-evaluate ((while-holder-interesting w)))]

[id (while-holder-id w)]

[pull? (while-holder-pull? w)])

; 'why' is why this time is interesting, or #f if it's not

(cond [why (set! notify-changed #t)])

(cond [(and (eq? why 'first) pull?) (set-add! pull-sampling id)]

[(and (eq? why 'last) pull?) (set-remove! pull-sampling id)])))

; notify watchers if the sampling regime has changed (and remember it in current-sampling)

(let ([new-sampling (send this get-sampling)])

(cond [(not (equal? new-sampling current-sampling))

(set! current-sampling new-sampling)

(send this notify-watchers-update-sampling)]))

; If notify-changed is #t, or if any whens were activated, tell the viewers that this thing might

; have changed. (It might not actually have changed but that's ok -- we just don't want to miss

; telling them if it did.)

(cond [(or notify-changed (not (null? active-whens)))

(send this notify-watchers-changed)])))))