From ad6978a432144581a9c88402ed4e75151571f9fb Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 2 Nov 2016 13:27:11 -0400
Subject: [PATCH] add fsm3

---
 turnstile/examples/rosette/fsm.rkt            | 15 ++--
 turnstile/examples/rosette/fsm3.rkt           | 85 +++++++++++++++++++
 turnstile/examples/rosette/lib/synthax3.rkt   |  5 +-
 turnstile/examples/rosette/query/debug3.rkt   | 37 +++++---
 turnstile/examples/rosette/rosette-notes.txt  | 32 +++++++
 turnstile/examples/rosette/rosette3.rkt       |  4 +-
 turnstile/examples/tests/rosette/fsm-test.rkt |  3 +
 .../tests/rosette/rosette3/fsm3-tests.rkt     | 57 +++++++++++++
 .../rosette3/run-all-rosette-tests-script.rkt |  1 +
 9 files changed, 218 insertions(+), 21 deletions(-)
 create mode 100644 turnstile/examples/rosette/fsm3.rkt
 create mode 100644 turnstile/examples/tests/rosette/rosette3/fsm3-tests.rkt

diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
index 4ce391b..4f12604 100644
--- a/turnstile/examples/rosette/fsm.rkt
+++ b/turnstile/examples/rosette/fsm.rkt
@@ -1,13 +1,14 @@
 #lang turnstile
 (extends "rosette.rkt" #:except #%datum #%app) ; extends typed rosette
-(require (prefix-in ro: rosette)) ; untyped 
-(require (prefix-in ro: rosette/lib/synthax))
-(require (prefix-in fsm: sdsl/fsm/fsm))
-(require (only-in sdsl/fsm/fsm
-                  reject verify-automaton debug-automaton synthesize-automaton))
-(provide (rename-out [rosette:choose ?]))
+(require (for-syntax lens unstable/lens)
+         (prefix-in ro: rosette) ; untyped
+         ;(prefix-in ro: rosette/lib/synthax)
+         (prefix-in fsm: sdsl/fsm/fsm))
 
-(provide FSM State Pict
+(begin-for-syntax (current-host-lang (lambda (id) (format-id id "fsm:~a" id))))
+
+(provide (rename-out [rosette:choose ?])
+         FSM State Pict
          (typed-out [reject : State]
                     [verify-automaton : (→ FSM Regexp (List Symbol))]
                     [debug-automaton : (→ FSM Regexp (List Symbol) Pict)]
diff --git a/turnstile/examples/rosette/fsm3.rkt b/turnstile/examples/rosette/fsm3.rkt
new file mode 100644
index 0000000..ce32e95
--- /dev/null
+++ b/turnstile/examples/rosette/fsm3.rkt
@@ -0,0 +1,85 @@
+#lang turnstile
+(extends "rosette3.rkt" #:except #%datum #%app define) ; extends typed rosette
+(require (for-syntax lens unstable/lens)
+         (prefix-in ro: rosette) ; untyped 
+         (prefix-in rosette3: "lib/synthax3.rkt")
+         (prefix-in rosette3: "query/debug3.rkt")
+         (prefix-in fsm: sdsl/fsm/fsm))
+
+(begin-for-syntax
+  (current-host-lang (lambda (id) (format-id id "fsm:~a" id))))
+
+(provide (rename-out [rosette3:choose ?] [app #%app] [rosette3:define/debug define])
+         FSM CFSM State CState
+         (typed-out [reject : CState]
+                    [verify-automaton : (C→ FSM CRegexp (CListof CSymbol))]
+                    [debug-automaton : (C→ FSM CRegexp (CListof CSymbol) CPict)]
+                    [synthesize-automaton : (C→ FSM CRegexp CUnit)])
+         #%datum automaton)
+
+(define-base-types CFSM CState)
+(define-named-type-alias State (U CState))
+(define-named-type-alias FSM (U CFSM))
+
+;; extend rosette:#%datum to handle regexp literals
+(define-typed-syntax #%datum
+  [(_ . v) ≫
+   #:when (regexp? (syntax-e #'v))
+   --------
+   [⊢ (ro:#%datum . v) ⇒ CRegexp]]
+  [(_ . v) ≫
+   --------
+   [≻ (rosette3:#%datum . v)]])
+
+;; extend rosette:#%app to work with FSM
+(define-typed-syntax app
+  ;; CFSM produces CBool
+  [(_ f e) ≫
+   [⊢ [f ≫ f- ⇐ : CFSM]]
+   [⊢ [e ≫ e- ⇐ : (CListof CSymbol)]]
+   --------
+   [⊢ (ro:#%app f- e-) ⇒ CBool]]
+  ;; (symb) FSM produces (symb) Bool
+  [(_ f e) ≫
+   [⊢ [f ≫ f- ⇐ : FSM]]
+   [⊢ [e ≫ e- ⇐ : (CListof CSymbol)]]
+   --------
+   [⊢ (ro:#%app f- e-) ⇒ Bool]]
+  [(_ f . es) ≫
+   --------
+   [≻ (rosette3:#%app f . es)]])
+
+(define-typed-syntax automaton
+  ;; fsm with CStates have type CFSM, else is symbolic FSM
+  [(_ init-state:id
+      [state:id (~datum :) (label:id (~datum →) 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 ...)))
+   #:with arr (datum->syntax #f '→)
+   [() ([state ≫ state- : CState] ...) ⊢ 
+    [init-state ≫ init-state- ⇐ : CState]
+    [target ≫ target- ⇐ : CState] ... ...]
+   --------
+   [⊢ (fsm:automaton init-state- 
+       [state- : (label arr target-) ...] ...) ⇒ CFSM]]
+  [(_ init-state:id
+      [state:id (~datum :) (label:id (~datum →) 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 ...)))
+   #:with arr (datum->syntax #f '→)
+   [() ([state ≫ state- : CState] ...) ⊢ 
+    [init-state ≫ init-state- ⇐ : CState]
+    [target ≫ target- ⇐ : State] ... ...]
+   --------
+   [⊢ (fsm:automaton init-state-
+       [state- : (label arr target-) ...] ...) ⇒ FSM]])
+
+;; (define (apply-FSM f v) (f v))
+;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool))
+
diff --git a/turnstile/examples/rosette/lib/synthax3.rkt b/turnstile/examples/rosette/lib/synthax3.rkt
index 2a1fd06..08234b6 100644
--- a/turnstile/examples/rosette/lib/synthax3.rkt
+++ b/turnstile/examples/rosette/lib/synthax3.rkt
@@ -39,10 +39,11 @@
   [(ch e ...+) ≫
    [⊢ [e ≫ e- ⇒ : ty]] ...
    #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
-   --------
    ;; 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/disarmed ...) ⇒ : (t/ro:U ty ...)]]])
+   #:with ch/disarmed (replace-stx-loc #'ro:choose #'ch)
+   --------
+   [⊢ (ch/disarmed e/disarmed ...) ⇒ (t/ro:U ty ...)]])
 
 ;; TODO: not sure how to handle define-synthax
 ;; it defines a macro, but may refer to itself in #:base and #:else
diff --git a/turnstile/examples/rosette/query/debug3.rkt b/turnstile/examples/rosette/query/debug3.rkt
index e6c86fc..e93c5ee 100644
--- a/turnstile/examples/rosette/query/debug3.rkt
+++ b/turnstile/examples/rosette/query/debug3.rkt
@@ -6,23 +6,40 @@
 
 (provide define/debug debug)
 
+;; - ideally, I could separate expansion of typed rosette and rosette,
+;; ie, expansion in ty/ro would stop at ro ids
+;; - concretely, e cannot be fully expanded bc then it misses
+;;   the "tracking app" stx param
+;; non-solutions:
+;; 1) use stop list with ro:#%app and ro:#%plain-app, so that
+;;    stx-param can replace ro:#%app
+;; - didnt work, ie didnt stop at ro:#%app bc stop list infused with racket ids
+;; 2) use e instead of e- and accept dup expansion
+;; - get syntax taint err
+;; 3) export app and app-track from rosette and manually insert
+;;    a stx-param
+;; - still get stx taint err
 (define-typed-syntax define/debug #:datum-literals (: -> →)
   [(_ x:id e) ≫
-   [⊢ [e ≫ e- ⇒ : τ]]
+   [⊢ e #;(syntax-parameterize ([ro:app ro:app-track]) e) ≫ e- ⇒ τ]
    #:with y (generate-temporary #'x)
    --------
-   [_ ≻ (begin-
-          (define-syntax- x (make-rename-transformer (⊢ y : τ)))
-          (ro:define/debug y e-))]]
+   [≻ (begin-
+        (define-syntax- x (make-rename-transformer (⊢ y : τ)))
+        ;; TODO: this doesnt completely work
+        ;; - specifically, using e- means #%app wont be stx-param'ed
+        ;; to the right thing (app-track) since e- is fully expanded
+        ;; and the param'ed app is already gone
+        ;; - but using e wont work either due to stx taint errs
+        (ro:define/debug y e-))]]
   [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫
-;   [⊢ [e ≫ e- ⇒ : ty_e]]
    #:with f- (generate-temporary #'f)
    --------
-   [_ ≻ (begin-
-          (define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out))))
-          (ro:define/debug f- 
-            (t/ro:λ ([x : ty] ...) 
-                    (t/ro:ann (t/ro:begin e ...) : ty_out))))]])
+   [≻ (begin-
+        (define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out))))
+        (ro:define/debug f-
+          (t/ro:λ ([x : ty] ...)
+            (t/ro:ann (t/ro:begin e ...) : ty_out))))]])
 
 (define-typed-syntax debug
   [(_ (pred? ...+) e) ≫
diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
index c5a7f55..acf480b 100644
--- a/turnstile/examples/rosette/rosette-notes.txt
+++ b/turnstile/examples/rosette/rosette-notes.txt
@@ -1,3 +1,35 @@
+2016-11-02 --------------------
+** Problem: typed forms should not expand all the way down
+
+- doing so interferes with the ability to layer a type system on top of a
+  Racket-embedded DSL
+
+Specific problems (assume host lang ids have prefix "host:")
+1) syntax parameters
+
+typed #%app expands to #'(host:#%app e1+ e2+)
+
+stx parameterizes in host:#%app will not catch param instances in e1 and e2
+since e1+ and e2+ are already fully expanded
+
+see rosette:define/debug as an example
+
+2) syntax taints
+
+If the host lang (eg rosette) uses syntax rules, then the typed layer will
+induce taint errs when trying to decompose expanded stx objs
+
+** Possible solution:
+
+Delimit expansion with special (prompt) macro representing the host lang.
+
+Further requirements for this solution:
+1) cannot wrap stx objs with extra racket forms, as infer does
+- workound by converting to explicit internal definition contexts rather than
+  lambda wrappers?
+2) local expand must use a stop list containing host lang prompt macro
+
+
 2016-09-08 --------------------
 
 ** Problem: Constant is unsound:
diff --git a/turnstile/examples/rosette/rosette3.rkt b/turnstile/examples/rosette/rosette3.rkt
index eda6437..2d27abe 100644
--- a/turnstile/examples/rosette/rosette3.rkt
+++ b/turnstile/examples/rosette/rosette3.rkt
@@ -45,7 +45,7 @@
          ;; BV types
          CBV BV
          CBVPred BVPred
-         CSolution CSolver CPict CSyntax)
+         CSolution CSolver CPict CSyntax CRegexp CSymbol)
 
 (begin-for-syntax
   (define (mk-ro:-id id) (format-id id "ro:~a" id))
@@ -71,7 +71,7 @@
   (define (concrete? t)
     (not (or (Any? t) (U*? t) (Constant*? t)))))
 
-(define-base-types Any CBV CStx CSymbol)
+(define-base-types Any CBV CStx CSymbol CRegexp)
 ;; CVectorof includes all vectors
 ;; CIVectorof includes only immutable vectors
 ;; CMVectorof includes only mutable vectors
diff --git a/turnstile/examples/tests/rosette/fsm-test.rkt b/turnstile/examples/tests/rosette/fsm-test.rkt
index e7dd395..4276c97 100644
--- a/turnstile/examples/tests/rosette/fsm-test.rkt
+++ b/turnstile/examples/tests/rosette/fsm-test.rkt
@@ -41,3 +41,6 @@
 (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)
+ (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/rosette3/fsm3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/fsm3-tests.rkt
new file mode 100644
index 0000000..575b552
--- /dev/null
+++ b/turnstile/examples/tests/rosette/rosette3/fsm3-tests.rkt
@@ -0,0 +1,57 @@
+#lang s-exp "../../../rosette/fsm3.rkt"
+(require "../../rackunit-typechecking.rkt")
+
+(define m 
+  (automaton init 
+   [init : (c → more)]
+   [more : (a → more) 
+           (d → more) 
+           (r → end)] 
+   [end : ]))
+
+(define rx #px"^c[ad]+r$")
+
+(typecheck-fail (automaton init)
+                #:with-msg "initial state init is not declared state")
+(typecheck-fail (automaton init [init : (c → more)])
+                #:with-msg "unbound identifier")
+(typecheck-fail (automaton init [init : (c → "more")])
+                #:with-msg "expected State, given String")
+
+(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  : ]))
+
+(check-type (M '(c a r)) : Bool) ; symbolic result
+(check-not-type (M '(c a r)) : CBool) ; symbolic result
+(check-type (if (M '(c a r)) 1 2) : Int)
+(check-not-type (if (M '(c a r)) 1 2) : CInt)
+
+;;  example commands 
+(check-type (m '(c a r)) : CBool -> #t)
+(check-type (m '(c a r)) : Bool -> #t)
+(check-type (m '(c d r)) : CBool -> #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$") : (CListof CSymbol) -> '(c r))
+;; TODO: get this to display the debugging output
+;; it's currently #f because defing/debug in query/debug3.rkt
+;; expands e before rosette's tracking-app stx-param is declared
+;; see notes in query/debug3.rkt for more info
+(check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : CPict -> #f)
+(check-type (synthesize-automaton M #px"^c[ad]+r$") : CUnit)
+(check-type
+ (with-output-to-string (λ () (synthesize-automaton M #px"^c[ad]+r$")))
+ : CString
+ ->
+ "/home/stchang/NEU_Research/macrotypes/turnstile/examples/tests/rosette/rosette3/fsm3-tests.rkt:21:0\n'(define M\n   (automaton\n    init\n    (init : (c → s2))\n    (s1 : (a → s1) (d → s1) (r → end))\n    (s2 : (a → s1) (d → s1) (r → reject))\n    (end :)))\n")
+
+;(debug-automaton m #px"^c[ad]+r$" '(c r))
diff --git a/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
index c4c1fc2..c201625 100644
--- a/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
@@ -19,5 +19,6 @@
  "rosette-guide-sec7-tests.rkt"  "Guide Sec. 7 Reflecting on Symbolic Values")
 
 (do-tests "bv-tests.rkt" "BV SDSL - General"
+          "fsm3-tests.rkt" "FSM"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")