Update sdsl/* to use #lang rosette

emina · Feb 28, 2016 · 9a71501 · 9a71501
1 parent 536ca9c
commit 9a71501
Show file tree

Hide file tree

Showing 73 changed files with 81 additions and 81 deletions.
diff --git a/sdsl/bv/bv.rkt b/sdsl/bv/bv.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "lang/form.rkt" "lang/bvops.rkt")
 

diff --git a/sdsl/bv/lang/bvops.rkt b/sdsl/bv/lang/bvops.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require 
   (prefix-in $ (only-in rosette bv bveq bvslt bvsgt bvsle bvsge bvult bvugt bvule bvuge)))

diff --git a/sdsl/bv/lang/program.rkt b/sdsl/bv/lang/program.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket [eq? ==]) 
          (only-in "bvops.rkt" bv bv*))
@@ -153,4 +153,4 @@
 (define t (trace* p))
 (term->datum (trace-out t))
 (asserts)
-|#  
+|#  
diff --git a/sdsl/fsm/automaton.rkt b/sdsl/fsm/automaton.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "viz.rkt" (rename-in rosette/lib/synthax [choose ?]))
 

diff --git a/sdsl/fsm/fsm.rkt b/sdsl/fsm/fsm.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "automaton.rkt" "query.rkt")
 

diff --git a/sdsl/fsm/lib.rkt b/sdsl/fsm/lib.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require 
  rosette/lib/lift 

diff --git a/sdsl/fsm/query.rkt b/sdsl/fsm/query.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require 
  "automaton.rkt" "lib.rkt"

diff --git a/sdsl/ifc/basic.rkt b/sdsl/ifc/basic.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt")
 (provide (all-defined-out))

diff --git a/sdsl/ifc/call.rkt b/sdsl/ifc/call.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt" )
 
@@ -168,4 +168,4 @@ m1k|#
         (goto (pop m) (Rpc r))
         (goto (push (pop m) (@ v (∨ Lv Lpc))) (Rpc r)))))
 
-|#
+|#
diff --git a/sdsl/ifc/indistinguishable.rkt b/sdsl/ifc/indistinguishable.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/match "machine.rkt")
 

diff --git a/sdsl/ifc/instruction.rkt b/sdsl/ifc/instruction.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/match rosette/lib/angelic "value.rkt")
 

diff --git a/sdsl/ifc/jump.rkt b/sdsl/ifc/jump.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt")
 

diff --git a/sdsl/ifc/machine.rkt b/sdsl/ifc/machine.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/match "value.rkt" "instruction.rkt")
 

diff --git a/sdsl/ifc/test.rkt b/sdsl/ifc/test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt" "indistinguishable.rkt" "verify.rkt"
          "basic.rkt" "jump.rkt" "call.rkt")

diff --git a/sdsl/ifc/value.rkt b/sdsl/ifc/value.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/match)
 

diff --git a/sdsl/ifc/verify-EENI-demo.rkt b/sdsl/ifc/verify-EENI-demo.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt" "indistinguishable.rkt" "verify.rkt"
          "basic.rkt" "jump.rkt" "call.rkt")

diff --git a/sdsl/ifc/verify.rkt b/sdsl/ifc/verify.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "machine.rkt" "indistinguishable.rkt")
 
@@ -90,4 +90,4 @@
     [(list (instruction (? union? r) _) _ ...)        
      (sort (map object-name (union-values r)) string<? #:key symbol->string)]
     [(list (instruction (? procedure? proc) _) ...) 
-     (map object-name proc)]))
+     (map object-name proc)]))
diff --git a/sdsl/synthcl/lang/builtins.rkt b/sdsl/synthcl/lang/builtins.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (for-syntax (only-in rosette make-list)) (only-in racket/syntax format-symbol)
          "types.rkt" 

diff --git a/sdsl/synthcl/lang/env.rkt b/sdsl/synthcl/lang/env.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require syntax/id-table "types.rkt" "builtins.rkt")
 

diff --git a/sdsl/synthcl/lang/errors.rkt b/sdsl/synthcl/lang/errors.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (provide raise-arity-error raise-operator-arity-error 
          raise-no-common-type-error raise-bad-type-error
@@ -20,4 +20,4 @@
    expr subexpr))
 
 (define (raise-bad-form-error expected expr [subexpr #f])
-  (raise-syntax-error #f (format "expected ~a" expected) expr subexpr))
+  (raise-syntax-error #f (format "expected ~a" expected) expr subexpr))
diff --git a/sdsl/synthcl/lang/forms.rkt b/sdsl/synthcl/lang/forms.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require racket/stxparam racket/splicing
          (for-syntax "types.rkt" "errors.rkt" (only-in racket make-list) (only-in syntax/stx stx-null?))

diff --git a/sdsl/synthcl/lang/main.rkt b/sdsl/synthcl/lang/main.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (for-syntax "typecheck.rkt" "types.rkt" 
                      (only-in rosette in-dict dict-keys)

diff --git a/sdsl/synthcl/lang/operators.rkt b/sdsl/synthcl/lang/operators.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (for-syntax "types.rkt" "errors.rkt" (only-in racket/syntax with-syntax*)) 
          "types.rkt" (prefix-in model/ "../model/operators.rkt"))

diff --git a/sdsl/synthcl/lang/queries.rkt b/sdsl/synthcl/lang/queries.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "util.rkt" racket/stxparam 
          (only-in rackunit test-pred) 

diff --git a/sdsl/synthcl/lang/sugar.rkt b/sdsl/synthcl/lang/sugar.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require racket/syntax syntax/id-table "operators.rkt" "forms.rkt"
          (for-template (only-in rosette #%app) "operators.rkt" "forms.rkt"))
@@ -30,4 +30,4 @@
     [(expr ...)
      (with-syntax ([(expr* ...) (map desugar (syntax->list stx))])
        (quasisyntax/loc stx (expr* ...)))]
-    [_ stx]))
+    [_ stx]))
diff --git a/sdsl/synthcl/lang/typecheck.rkt b/sdsl/synthcl/lang/typecheck.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (for-template (only-in "forms.rkt" app-or-ref) 
                        (only-in racket quote #%app #%datum) 

diff --git a/sdsl/synthcl/lang/types.rkt b/sdsl/synthcl/lang/types.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 ; Provides a mapping from OpenCL type identifiers to 
 ; the type instances / predicates in the OpenCL model.

diff --git a/sdsl/synthcl/lang/util.rkt b/sdsl/synthcl/lang/util.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "types.rkt")
 

diff --git a/sdsl/synthcl/model/buffer.rkt b/sdsl/synthcl/model/buffer.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "flags.rkt" "type.rkt" "pointers.rkt" "memory.rkt" "context.rkt" "work.rkt"
          rosette/lib/match)

diff --git a/sdsl/synthcl/model/context.rkt b/sdsl/synthcl/model/context.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "memory.rkt" rosette/lib/match)
 

diff --git a/sdsl/synthcl/model/errors.rkt b/sdsl/synthcl/model/errors.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (provide raise-conversion-error raise-pointer-cast-error raise-context-error)
 

diff --git a/sdsl/synthcl/model/flags.rkt b/sdsl/synthcl/model/flags.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (provide (all-defined-out))
 
@@ -10,4 +10,4 @@
 (define-flags 
   [CL_MEM_READ_WRITE 1] 
   [CL_MEM_WRITE_ONLY 2]
-  [CL_MEM_READ_ONLY 4])
+  [CL_MEM_READ_ONLY 4])
diff --git a/sdsl/synthcl/model/kernel.rkt b/sdsl/synthcl/model/kernel.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/syntax format-symbol) "context.rkt" "buffer.rkt" "program.rkt" "errors.rkt")
 

diff --git a/sdsl/synthcl/model/memory.rkt b/sdsl/synthcl/model/memory.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "errors.rkt" "work.rkt" "type.rkt" "reals.rkt" 
          (only-in "pointers.rkt" gen:pointer)               

diff --git a/sdsl/synthcl/model/objects.rkt b/sdsl/synthcl/model/objects.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "type.rkt" "context.rkt" "queue.rkt" "program.rkt" "kernel.rkt" "buffer.rkt"  
          rosette/lib/match)

diff --git a/sdsl/synthcl/model/operators.rkt b/sdsl/synthcl/model/operators.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "type.rkt" "reals.rkt"  
          (only-in rosette [/ @/] [bitvector->integer bv->int] [sqrt @sqrt]))

diff --git a/sdsl/synthcl/model/pointers.rkt b/sdsl/synthcl/model/pointers.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "type.rkt" "reals.rkt" "errors.rkt" 
          (for-syntax (only-in racket/syntax format-id)))
@@ -106,4 +106,4 @@
 (pointer-ref bb* 5)
 (pointer-set! bb* 5 #t)
 (pointer-set! bb* 6 10)
-(pointer-ref bb* 5)|#
+(pointer-ref bb* 5)|#
diff --git a/sdsl/synthcl/model/program.rkt b/sdsl/synthcl/model/program.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (for-syntax (only-in rosette/lib/util/syntax read-module)
                      (only-in racket filter-map))

diff --git a/sdsl/synthcl/model/queue.rkt b/sdsl/synthcl/model/queue.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "context.rkt" "buffer.rkt" "kernel.rkt" 
          "work.rkt" "runtime.rkt" "memory.rkt"

diff --git a/sdsl/synthcl/model/reals.rkt b/sdsl/synthcl/model/reals.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "type.rkt" "errors.rkt"
          rosette/lib/match (only-in racket/syntax format-symbol)

diff --git a/sdsl/synthcl/model/runtime.rkt b/sdsl/synthcl/model/runtime.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require "memory.rkt" "reals.rkt" "type.rkt" "pointers.rkt")
 
@@ -63,4 +63,4 @@
      ((local-pointer-set! self) val))
 
    (define (pointer->list self)
-     (list ((local-pointer-get self))))])
+     (list ((local-pointer-get self))))])
diff --git a/sdsl/synthcl/model/type.rkt b/sdsl/synthcl/model/type.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (provide type? type-name type-base gen:type)
 

diff --git a/sdsl/synthcl/model/work.rkt b/sdsl/synthcl/model/work.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 
 (provide current-work-size current-global-id 

diff --git a/sdsl/synthcl/test/memory.rkt b/sdsl/synthcl/test/memory.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rackunit rackunit/text-ui rosette/lib/roseunit
          "../model/memory.rkt" "../model/work.rkt" 

diff --git a/sdsl/synthcl/test/operators.rkt b/sdsl/synthcl/test/operators.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rackunit rackunit/text-ui rosette/lib/roseunit
          (prefix-in $ "../model/operators.rkt") 

diff --git a/sdsl/synthcl/test/reals.rkt b/sdsl/synthcl/test/reals.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rackunit rackunit/text-ui rosette/lib/roseunit "../model/reals.rkt")
 

diff --git a/sdsl/synthcl/test/work.rkt b/sdsl/synthcl/test/work.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rackunit rackunit/text-ui rosette/lib/roseunit "../model/work.rkt") 
 

diff --git a/sdsl/websynth/benchmarks/alanon_arkansas_16.rkt b/sdsl/websynth/benchmarks/alanon_arkansas_16.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/alanon_arkansas_2.rkt b/sdsl/websynth/benchmarks/alanon_arkansas_2.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/alanon_arkansas_4.rkt b/sdsl/websynth/benchmarks/alanon_arkansas_4.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/alanon_arkansas_8.rkt b/sdsl/websynth/benchmarks/alanon_arkansas_8.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/imdb250_16.rkt b/sdsl/websynth/benchmarks/imdb250_16.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/imdb250_2.rkt b/sdsl/websynth/benchmarks/imdb250_2.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/imdb250_4.rkt b/sdsl/websynth/benchmarks/imdb250_4.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/imdb250_8.rkt b/sdsl/websynth/benchmarks/imdb250_8.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/itunes100_16.rkt b/sdsl/websynth/benchmarks/itunes100_16.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")

diff --git a/sdsl/websynth/benchmarks/itunes100_2.rkt b/sdsl/websynth/benchmarks/itunes100_2.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require (only-in racket/runtime-path define-runtime-path))
 (require "../dom.rkt")