From e0f96296edc3e0071d49743c85b944720837c629 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 18 Jul 2016 18:30:51 -0400
Subject: [PATCH] start fsm, (bv tests not passing)

---
 turnstile/examples/rosette/bv.rkt             |  2 +-
 turnstile/examples/rosette/fsm.rkt            | 48 +++++++++++++++++++
 turnstile/examples/rosette/rosette.rkt        |  2 +-
 turnstile/examples/tests/rosette/fsm-test.rkt | 32 +++++++++++++
 4 files changed, 82 insertions(+), 2 deletions(-)
 create mode 100644 turnstile/examples/rosette/fsm.rkt
 create mode 100644 turnstile/examples/tests/rosette/fsm-test.rkt

diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
index 34ea710..7ca5aa2 100644
--- a/turnstile/examples/rosette/bv.rkt
+++ b/turnstile/examples/rosette/bv.rkt
@@ -1,5 +1,5 @@
 #lang turnstile
-(extends "rosette.rkt" #:except bv)
+(extends "rosette.rkt" #:except bv) ; extends typed rosette
 (require (prefix-in ro: rosette)) ; untyped 
 (require (except-in "rosette.rkt" #%app define)) ; typed
 (require (only-in sdsl/bv/lang/bvops bvredand bvredor)
diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
new file mode 100644
index 0000000..0f8f15d
--- /dev/null
+++ b/turnstile/examples/rosette/fsm.rkt
@@ -0,0 +1,48 @@
+#lang turnstile
+(extends "rosette.rkt"); #:except →) ; 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 (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))
+
+(define-base-types FSM Regexp State)
+
+(define-typed-syntax pregexp 
+  [(_ s) ≫
+   [⊢ [[s ≫ s-] ⇐ : String]]
+   --------
+   [⊢ [[_ ≫ (pregexp- s-)] ⇒ : Regexp]]])
+
+
+
+(define-typed-syntax automaton #:datum-literals (: →)
+  [(_ init-state:id
+      [state:id : (label:id → target) ...] ...) ≫
+   [#:fail-unless (member (syntax->datum #'init-state)
+                          (syntax->datum #'(state ...)))
+                  (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]]])
+
+
+(define-typed-syntax ?
+ [(_ e ...+) ≫
+   [⊢ [[e ≫ e-] ⇒ : ty]] ...
+   --------
+   [⊢ [[_ ≫ (ro:choose e ...)] ⇒ : (⊔ ty ...)]]])
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index a8af64d..0de8b68 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -99,7 +99,7 @@
 (define-type-alias BVPred (→ BV Bool))
 
 ;; TODO: fix me --- need subtyping?
-(define-type-alias Nat Int)
+(define-syntax Nat (make-rename-transformer #'Int))
 
 ;; TODO: support higher order case --- need intersect types?
 ;(define-rosette-primop bv : (→ Int BVPred BV)
diff --git a/turnstile/examples/tests/rosette/fsm-test.rkt b/turnstile/examples/tests/rosette/fsm-test.rkt
new file mode 100644
index 0000000..77e5621
--- /dev/null
+++ b/turnstile/examples/tests/rosette/fsm-test.rkt
@@ -0,0 +1,32 @@
+#lang s-exp "../../rosette/fsm.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define m 
+  (automaton init 
+   [init : (c → more)]
+   [more : (a → more) 
+           (d → more) 
+           (r → end)] 
+   [end : ]))
+
+(define rx (pregexp "^c[ad]+r$"))
+
+
+(define M 
+  (automaton init
+   [init : (c → (? s1 s2))]
+   [s1   : (a → (? s1 s2 end reject)) 
+           (d → (? s1 s2 end reject))
+           (r → (? s1 s2 end reject))]
+   [s2   : (a → (? s1 s2 end reject)) 
+           (d → (? s1 s2 end reject))
+           (r → (? s1 s2 end reject))]
+   [end  : ]))
+
+;; ; example commands 
+;; (m '(c a r)) 
+;; (m '(c d r))
+;; (m '(c a d a r))
+;; (verify-automaton m #px"^c[ad]+r$")
+;; (debug-automaton m #px"^c[ad]+r$" '(c r))
+;; (synthesize-automaton M #px"^c[ad]+r$")