commit abf74414f0e88600e33170fd2bf1d750e3eacf1b
parent f7b4dde15bd8cceae2b1e5bc04a06f2cc96b12ac
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 22 Jul 2016 14:16:24 -0400
fix choose in typed fsm lang
- convert typed rosette and its langs to use rosette's #%module-begin
Diffstat:
5 files changed, 82 insertions(+), 42 deletions(-)
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -1,7 +1,10 @@
-#lang turnstile
-(extends "rosette.rkt" #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) ; extends typed rosette
+;#lang turnstile
+#lang racket/base
+(require (except-in "../../../turnstile/turnstile.rkt" #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal?)
+ (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
+(extends "rosette.rkt" ; extends typed rosette
+ #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
(require (prefix-in ro: rosette)) ; untyped
-;(require (except-in "rosette.rkt" #%app define)) ; typed
(require (only-in sdsl/bv/lang/bvops bvredand bvredor)
(prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
(require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
@@ -1,24 +1,35 @@
-#lang turnstile
-(extends "rosette.rkt"); #:except →) ; extends typed rosette
+;#lang turnstile
+#lang racket/base
+(require (except-in "../../../turnstile/turnstile.rkt" #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal?)
+ (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
+(extends "rosette.rkt" #:except #%datum #%app) ; extends typed rosette
(require (prefix-in ro: rosette)) ; untyped
(require (prefix-in ro: rosette/lib/synthax))
-;; (require (except-in "rosette.rkt" #%app define)) ; typed
-;; (require (only-in sdsl/bv/lang/bvops bvredand bvredor)
(require (prefix-in fsm: sdsl/fsm/fsm))
-(require (only-in sdsl/fsm/fsm reject))
-;(require (prefix-in fsm: (only-in sdsl/fsm/automaton automaton)))
-;; ;(require (only-in sdsl/fsm/fsm automaton))
-;; ;; (require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
+(require (only-in sdsl/fsm/fsm reject verify-automaton debug-automaton synthesize-automaton))
(require (for-syntax lens unstable/lens))
-(define-base-types FSM Regexp State)
+(define-base-types FSM State Pict)
-(define-typed-syntax pregexp
- [(_ s) ≫
- [⊢ [s ≫ s- ⇐ : String]]
+(define-typed-syntax #%datum
+ [(_ . v) ≫
+ #:when (regexp? (syntax-e #'v))
--------
- [⊢ [_ ≫ (pregexp- s-) ⇒ : Regexp]]])
+ [⊢ [_ ≫ (ro:#%datum . v) ⇒ : Regexp]]]
+ [(_ . v) ≫
+ --------
+ [_ ≻ (rosette:#%datum . v)]])
+
+(define-typed-syntax app #:export-as #%app
+ [(_ f e) ≫
+ [⊢ [f ≫ f- ⇐ : FSM]]
+ [⊢ [e ≫ e- ⇐ : (List Symbol)]]
+ --------
+ [⊢ [_ ≫ (ro:#%app f- e-) ⇒ : Bool]]]
+ [(_ f . es) ≫
+ --------
+ [_ ≻ (rosette:#%app f . es)]])
(define-typed-syntax automaton #:datum-literals (: →)
[(_ init-state:id
@@ -28,26 +39,28 @@
(format "initial state ~a is not declared state: ~a"
(syntax->datum #'init-state)
(syntax->datum #'(state ...)))
- ;#:fail-unless (let ([states (syntax->datum #'(state ...))])
- ; (for/and ([t (syntax->datum #'(target ... ...))])
- ; (member t states)))
- ; (format "transition to unknown state")
#:with arr (datum->syntax #f '→)
[() ([state ≫ state- : State] ...) ⊢
[init-state ≫ init-state- ⇐ : State]
[target ≫ target- ⇐ : State] ... ...]
--------
- [⊢ [_ ≫ (fsm:automaton init-state-
- [state- : (label arr target-) ...] ...)
- ⇒ : FSM]]])
+ [⊢ [_ ≫ (fsm:automaton init-state-
+ [state- : (label arr target-) ...] ...) ⇒ : FSM]]])
(define-primop reject : State)
+;(provide (rename-out [fsm:? ?]))
(define-typed-syntax ?
- [(_ e ...+) ≫
- [⊢ [e ≫ e- ⇒ : ty]] ...
+ [(ch e ...+) ≫
+ [⊢ [e ≫ e- ⇒ : ty]] ...
--------
- [⊢ [_ ≫ (ro:choose e ...) ⇒ : (⊔ ty ...)]]])
+ ;; the #'choose identifier itself must have the location of its use
+ ;; see define-synthax implementation, specifically syntax/source in utils
+ [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e ...) ⇒ : (⊔ ty ...)]]])
+
+;; (define (apply-FSM f v) (f v))
+;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool))
-(define (apply-FSM f v) (f v))
-(define-primop apply-FSM : (→ FSM (List Symbol) Bool))
+(define-primop verify-automaton : (→ FSM Regexp (List Symbol)))
+(define-primop debug-automaton : (→ FSM Regexp (List Symbol) Pict))
+(define-primop synthesize-automaton : (→ FSM Regexp Unit))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -1,9 +1,15 @@
-#lang turnstile
-(extends "../ext-stlc.rkt" #:except if)
+;#lang turnstile
+#lang racket/base
+(require (except-in "../../../turnstile/turnstile.rkt"
+ #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer?)
+ (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
+(provide (rename-out [ro:#%module-begin #%module-begin]))
+(extends "../ext-stlc.rkt" #:except if #%app #%module-begin)
(reuse List #:from "../stlc+cons.rkt")
(require (only-in "../stlc+reco+var.rkt" [define stlc:define]))
(require (only-in "../stlc+reco+var.rkt" define-type-alias))
(require (prefix-in ro: rosette))
+(require (prefix-in ro: rosette/lib/synthax))
(provide BVPred)
(define-simple-macro (define-rosette-primop op:id : ty)
@@ -27,10 +33,25 @@
(define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
(ro:define-symbolic y ... pred-))]])
+(define-typed-syntax choose
+ [(_ e ...+) ≫
+ [⊢ [e ≫ e- ⇒ : ty]] ...
+ --------
+ [⊢ [_ ≫ (ro:choose e ...) ⇒ : (⊔ ty ...)]]])
+
+(define-typed-syntax app #:export-as #%app
+ [(_ e_fn e_arg ...) ≫
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
+ #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+ (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+ [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
+ --------
+ [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]])
+
;; ----------------------------------------------------------------------------
;; Racket stuff
-(define-base-type Symbol)
+(define-base-types Symbol Regexp)
(define-typed-syntax quote
[(_ x:id) ≫
@@ -45,6 +66,7 @@
(define-rosette-primop boolean? : (→ Bool Bool))
(define-rosette-primop integer? : (→ Int Bool))
(define-rosette-primop string? : (→ String Bool))
+(define-rosette-primop pregexp : (→ String Regexp))
(define-typed-syntax equal?
[(equal? e1 e2) ≫
diff --git a/turnstile/examples/tests/rosette/fsm-test.rkt b/turnstile/examples/tests/rosette/fsm-test.rkt
@@ -9,8 +9,7 @@
(r → end)]
[end : ]))
-(define rx (pregexp "^c[ad]+r$"))
-
+(define rx #px"^c[ad]+r$")
(define M
(automaton init
@@ -23,11 +22,13 @@
(r → (? s1 s2 end reject))]
[end : ]))
-; example commands
-(check-type (apply-FSM m '(c a r)) : Bool -> #t)
-(check-type (apply-FSM m '(c d r)) : Bool -> #t)
-(check-type (apply-FSM m '(c a d a r)) : Bool -> #t)
-(check-type (apply-FSM m '(c a d a)) : Bool -> #f)
-;; (verify-automaton m #px"^c[ad]+r$")
-;; (debug-automaton m #px"^c[ad]+r$" '(c r))
-;; (synthesize-automaton M #px"^c[ad]+r$")
+(check-type (M '(c a r)) : Bool) ; symbolic result
+
+;; example commands
+(check-type (m '(c a r)) : Bool -> #t)
+(check-type (m '(c d r)) : Bool -> #t)
+(check-type (m '(c a d a r)) : Bool -> #t)
+(check-type (m '(c a d a)) : Bool -> #f)
+(check-type (verify-automaton m #px"^c[ad]+r$") : (List Symbol) -> '(c r))
+(check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : Pict)
+(check-type (synthesize-automaton M #px"^c[ad]+r$") : Unit)
diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
@@ -2,4 +2,5 @@
(require "rosette-tests.rkt")
(require "bv-tests.rkt")
;(require "bv-ref-tests.rkt")
-(require "fsm-test.rkt")
+; visit but dont instantiate, o.w. will get unsat
+(dynamic-require "fsm-test.rkt" (void))
