Add Dynamics%.

This commit is contained in:
Sergiu Ivanov 2022-09-15 20:40:07 +02:00
parent 567a721c8f
commit 60fd8b2a24
2 changed files with 43 additions and 1 deletions

View file

@ -33,7 +33,7 @@
build-interaction-graph/form build-signed-interaction-graph build-interaction-graph/form build-signed-interaction-graph
build-signed-interaction-graph/form build-signed-interaction-graph/form
Modality Mode dynamics% Modality Mode dynamics% Dynamics%
) )
(define-type (State a) (VariableMapping a)) (define-type (State a) (VariableMapping a))
@ -528,6 +528,28 @@
(for/list ([m mode]) (for/list ([m mode])
(cons m (update network s m)))))) (cons m (update network s m))))))
;; TODO: Find a better way to define the type of the class
;; dynamics%.
;;
;; TODO: Fix the parameter of State when Typed Racket supports
;; passing type parameters to the parent.
;;
;; NOTE: The type appearing when you type dynamics% in the REPL does
;; not directly type check.
(define-type (Dynamics% a)
(Class
(init (network (Network a) #:optional)
(mode Mode #:optional))
(field (network (Network a))
(mode Mode))
(step (-> (State Any) (Listof (State Any))))
(step/annotated (-> (State a) (Listof (Pairof Modality (State a)))))
(step* (-> (Listof (State Any)) (Listof (State Any))))
(build-state-graph (-> (Listof (State Any)) Graph))
(build-state-graph/annotated (-> (Listof (State Any)) Graph))
(build-state-graph* (-> (Listof (State Any)) (U Positive-Integer 'full) Graph))
(build-state-graph*/annotated (-> (Listof (State Any)) (U Positive-Integer 'full) Graph))))
(module+ test (module+ test
(let* ([n1 : (Network Boolean) (let* ([n1 : (Network Boolean)
(forms->boolean-network (hash 'x '(not y) (forms->boolean-network (hash 'x '(not y)

View file

@ -407,6 +407,26 @@ This is the only method of @racket[dds%] overridden in this class.
} }
@deftypeform[(Dynamics% a)]{
The type of an instance of @racket[dynamics%] with values of type @racket[a].
@ex[
(ann (inst dynamics% Boolean) (Dynamics% Boolean))
]
Note that, as of 2022-09-15, Typed Racket does not seem to allow to pass type
parameters from a child class to a parent class. Therefore, @racket[dynamics%]
inherits in fact from a @racket[dds%] with its first type parameter set to
@racket[(State Any)]. This can be seen by examining the type of
@racket[dynamics%].
@ex[dynamics%]
The type constructor @racket[Dynamics%] takes this limitation into account.
}
} }