fsm.rkt (2066B)
1 #lang turnstile 2 (extends "rosette.rkt" #:except #%datum #%app) ; extends typed rosette 3 (require (prefix-in ro: rosette)) ; untyped 4 (require (prefix-in ro: rosette/lib/synthax)) 5 (require (prefix-in fsm: sdsl/fsm/fsm)) 6 (require (only-in sdsl/fsm/fsm 7 reject verify-automaton debug-automaton synthesize-automaton)) 8 (provide (rename-out [rosette:choose ?])) 9 10 (provide FSM State Pict 11 (typed-out [reject : State] 12 [verify-automaton : (→ FSM Regexp (List Symbol))] 13 [debug-automaton : (→ FSM Regexp (List Symbol) Pict)] 14 [synthesize-automaton : (→ FSM Regexp Unit)]) 15 #%datum #%app automaton) 16 17 (define-base-types FSM State Pict) 18 19 ;; extend rosette:#%datum to handle regexp literals 20 (define-typed-syntax #%datum 21 [(_ . v) ≫ 22 #:when (regexp? (syntax-e #'v)) 23 -------- 24 [⊢ [_ ≫ (ro:#%datum . v) ⇒ : Regexp]]] 25 [(_ . v) ≫ 26 -------- 27 [_ ≻ (rosette:#%datum . v)]]) 28 29 ;; extend rosette:#%app to work with FSM 30 (define-typed-syntax #%app 31 [(_ f e) ≫ 32 [⊢ [f ≫ f- ⇐ : FSM]] 33 [⊢ [e ≫ e- ⇐ : (List Symbol)]] 34 -------- 35 [⊢ [_ ≫ (ro:#%app f- e-) ⇒ : Bool]]] 36 [(_ f . es) ≫ 37 -------- 38 [_ ≻ (rosette:#%app f . es)]]) 39 40 (define-typed-syntax automaton #:datum-literals (: →) 41 [(_ init-state:id 42 [state:id : (label:id → target) ...] ...) ≫ 43 #:fail-unless (member (syntax->datum #'init-state) 44 (syntax->datum #'(state ...))) 45 (format "initial state ~a is not declared state: ~a" 46 (syntax->datum #'init-state) 47 (syntax->datum #'(state ...))) 48 #:with arr (datum->syntax #f '→) 49 [() ([state ≫ state- : State] ...) ⊢ 50 [init-state ≫ init-state- ⇐ : State] 51 [target ≫ target- ⇐ : State] ... ...] 52 -------- 53 [⊢ [_ ≫ (fsm:automaton init-state- 54 [state- : (label arr target-) ...] ...) ⇒ : FSM]]]) 55 56 ;; (define (apply-FSM f v) (f v)) 57 ;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool)) 58