Merge pull request #4 from bmastenbrook/lang-reader

emina · emina · commit 016b47bb3fe3 · 2016-02-26T11:52:43.000-08:00
Make #lang rosette and #lang rosette/safe work
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

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-#lang s-exp rosette`
	`1`	`+#lang rosette`
`2`	`2`
`3`	`3`	`(define-symbolic b boolean?)`
`4`	`4`	`(define v (vector 1))`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+#lang s-exp syntax/module-reader`
	`2`	`+rosette`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+#lang s-exp syntax/module-reader`
	`2`	`+rosette/safe`