From abf74414f0e88600e33170fd2bf1d750e3eacf1b Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 22 Jul 2016 14:16:24 -0400 Subject: [PATCH] fix choose in typed fsm lang - convert typed rosette and its langs to use rosette's #%module-begin --- turnstile/examples/rosette/bv.rkt | 9 ++- turnstile/examples/rosette/fsm.rkt | 63 +++++++++++-------- turnstile/examples/rosette/rosette.rkt | 28 ++++++++- turnstile/examples/tests/rosette/fsm-test.rkt | 21 ++++--- .../tests/rosette/run-all-rosette-tests.rkt | 3 +- 5 files changed, 82 insertions(+), 42 deletions(-) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 75281c3..40b5838 100644 --- 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 index b8f31a5..5567280 100644 --- 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 index 6624187..49e6d2e 100644 --- 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 index 457fd72..9289d02 100644 --- 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 index 332ae17..1e24334 100644 --- 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))