suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix rosette tests again

Browse Source
This commit is contained in:
Stephen Chang 2016-07-19 16:27:38 -04:00
parent 580ffdd1ac
commit 6e7a8aedf3
2 changed files with 4 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
turnstile/examples/rosette/rosette.rkt
View File

@ -1,10 +1,8 @@
#lang turnstile
;(require (only-in rosette bv bitvector))
;(require (only-in rosette [exact-integer? integer?]))
(extends "../ext-stlc.rkt" #:except if)
(reuse List #:from "../stlc+cons.rkt")
(require (prefix-in stlc: (only-in "../stlc+reco+var.rkt" define λ)))
(require (only-in "../stlc+reco+var.rkt" define-type-alias Int Bool →))
(require (only-in "../stlc+reco+var.rkt" [define stlc:define]))
(require (only-in "../stlc+reco+var.rkt" define-type-alias))
(require (prefix-in ro: rosette))
(provide BVPred)
@ -91,7 +89,7 @@
--------
[_ ≻ (begin-
(define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
(stlc:define f- (stlc:λ ([x : ty] ...) e)))]])
(stlc:define f- (ext-stlc:λ ([x : ty] ...) e)))]])
(define-base-type Stx)

2
turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
View File

@ -1,5 +1,5 @@
#lang racket/base
(require "rosette-tests.rkt")
(require "bv-tests.rkt")
(require "bv-ref-tests.rkt")
;(require "bv-ref-tests.rkt")
(require "fsm-test.rkt")