Merge pull request #4 from bmastenbrook/lang-reader

Make #lang rosette and #lang rosette/safe work
emina · Feb 26, 2016 · 016b47b · 016b47b
2 parents 035b949 + 165c3dc
commit 016b47b
Show file tree

Hide file tree

Showing 8 changed files with 15 additions and 11 deletions.
diff --git a/doc/guide/scribble/datatypes/test.rkt b/doc/guide/scribble/datatypes/test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 
 
@@ -33,4 +33,4 @@
 (label (if b (suit 'club) 3))
 
 (define env (solve (assert (suit<? s (suit 'diamond)))))
-(evaluate s env)
+(evaluate s env)
diff --git a/doc/guide/scribble/essentials/poly.rkt b/doc/guide/scribble/essentials/poly.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 ;(configure [bitwidth 8])
 
@@ -40,4 +40,4 @@
                 (assert (< (abs y) 10))
                 (assert (not (= (poly x) 0)))
                 (assert (= (poly x) (poly y))))))
-env
+env
diff --git a/doc/guide/scribble/essentials/queries.rkt b/doc/guide/scribble/essentials/queries.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 (define (poly x)
   (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
@@ -30,4 +30,4 @@
                               #:guarantee (same-as-poly factored-sketch n))))
 
 (print-forms sol)
-
+
diff --git a/doc/guide/scribble/libs/rosette-lib-test.rkt b/doc/guide/scribble/libs/rosette-lib-test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/meta/meta)
 
@@ -25,4 +25,4 @@
  (synthesize #:forall (list i)
              #:assume (assert (>= i 0))
              #:guarantee (assert (= (div2mul4 i) (* 4 (quotient i 2))))))
-(print-forms m2)
+(print-forms m2)
diff --git a/doc/guide/scribble/reflection/test.rkt b/doc/guide/scribble/reflection/test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (define-symbolic b boolean?)
 (define v (vector 1))

diff --git a/doc/guide/scribble/welcome/welcome.scrbl b/doc/guide/scribble/welcome/welcome.scrbl
@@ -66,11 +66,11 @@ The Rosette system ships with two dialects of the Rosette language:
 
 To use the safe dialect, start your programs with the following line:
 
-@racketmod[s-exp rosette/safe]
+@racketmod[rosette/safe]
 
 To use the unsafe dialect, type this line instead:
 
-@racketmod[s-exp rosette]
+@racketmod[rosette]
 
 We strongly recommend that you start with the safe dialect, which includes a core subset of Racket.  The unsafe dialect includes all of Racket, but unless you understand and observe the restrictions on using non-core features, your seemingly correct programs may crash or produce unexpected results.
 
diff --git a/rosette/lang/reader.rkt b/rosette/lang/reader.rkt
@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+rosette
diff --git a/rosette/safe/lang/reader.rkt b/rosette/safe/lang/reader.rkt
@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+rosette/safe