From 580ffdd1acb4268d27737cda039fc34105159a38 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 19 Jul 2016 15:46:55 -0400
Subject: [PATCH] add typed fsm forms except verification forms

---
 turnstile/examples/rosette/fsm.rkt             | 18 ++++++++++++++----
 turnstile/examples/tests/rosette/fsm-test.rkt  |  9 +++++----
 .../tests/rosette/run-all-rosette-tests.rkt    |  5 +++++
 3 files changed, 24 insertions(+), 8 deletions(-)
 create mode 100644 turnstile/examples/tests/rosette/run-all-rosette-tests.rkt

diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
index 0f8f15d..607e141 100644
--- a/turnstile/examples/rosette/fsm.rkt
+++ b/turnstile/examples/rosette/fsm.rkt
@@ -5,10 +5,13 @@
 ;; (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 (for-syntax lens "../../append-lens.rkt"))
+
 (define-base-types FSM Regexp State)
 
 (define-typed-syntax pregexp 
@@ -17,8 +20,6 @@
    --------
    [⊢ [[_ ≫ (pregexp- s-)] ⇒ : Regexp]]])
 
-
-
 (define-typed-syntax automaton #:datum-literals (: →)
   [(_ init-state:id
       [state:id : (label:id → target) ...] ...) ≫
@@ -32,17 +33,26 @@
                       (member t states)))
                   (format "transition to unknown state")]
    [#:with arr (datum->syntax #f '→)]
+   [#:with (t ...) 
+           (lens-view stx-append*-lens #'((target ...) ...))]
    [() ([state : State ≫ state-] ...) ⊢ 
-     [[init-state ≫ init-state-] ⇐ : State]
-     [[target ≫ target-] ⇐ : State] ... ...]
+    [[init-state ≫ init-state-] ⇐ : State]
+;     [[target ≫ target-] ⇐ : State] ... ...]
+    [[t ≫ t-] ⇐ : State] ...]
+   [#:with ((target- ...) ...) 
+           (lens-set stx-append*-lens #'((target ...) ...) #'(t- ...))]
    --------
    [⊢ [[_ ≫ (fsm:automaton init-state- 
               [state- : (label arr target-) ...] ...)] 
        ⇒ : FSM]]])
 
+(define-primop reject : State)
 
 (define-typed-syntax ?
  [(_ e ...+) ≫
    [⊢ [[e ≫ e-] ⇒ : ty]] ...
    --------
    [⊢ [[_ ≫ (ro:choose e ...)] ⇒ : (⊔ ty ...)]]])
+
+(define (apply-FSM f v) (f v))
+(define-primop apply-FSM : (→ FSM (List Symbol) Bool))
diff --git a/turnstile/examples/tests/rosette/fsm-test.rkt b/turnstile/examples/tests/rosette/fsm-test.rkt
index 77e5621..457fd72 100644
--- a/turnstile/examples/tests/rosette/fsm-test.rkt
+++ b/turnstile/examples/tests/rosette/fsm-test.rkt
@@ -23,10 +23,11 @@
            (r → (? s1 s2 end reject))]
    [end  : ]))
 
-;; ; example commands 
-;; (m '(c a r)) 
-;; (m '(c d r))
-;; (m '(c a d a r))
+; 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$")
diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
new file mode 100644
index 0000000..71d318c
--- /dev/null
+++ b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
@@ -0,0 +1,5 @@
+#lang racket/base
+(require "rosette-tests.rkt")
+(require "bv-tests.rkt")
+(require "bv-ref-tests.rkt")
+(require "fsm-test.rkt")