commit 541c1e64a923cc64c84e08a5fcac7593b69a82a6 parent 8b81c9369262684478afaf1c15b5f14f833540b9 Author: Stephen Chang <stchang@ccs.neu.edu> Date: Fri, 22 Jul 2016 16:47:39 -0400 add list to typed rosette Diffstat:
| M | turnstile/examples/rosette/bv.rkt | | | 4 | +++- |
| M | turnstile/examples/rosette/fsm.rkt | | | 4 | +++- |
| M | turnstile/examples/rosette/rosette.rkt | | | 10 | ++++++++-- |
3 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt @@ -1,6 +1,8 @@ ;#lang turnstile #lang racket/base -(require (except-in "../../../turnstile/turnstile.rkt" #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal?) +(require (except-in "../../../turnstile/turnstile.rkt" + #%module-begin + zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal? list) (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) (extends "rosette.rkt" ; extends typed rosette #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt @@ -1,6 +1,8 @@ ;#lang turnstile #lang racket/base -(require (except-in "../../../turnstile/turnstile.rkt" #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal?) +(require (except-in "../../../turnstile/turnstile.rkt" + #%module-begin + zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal? list) (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) (extends "rosette.rkt" #:except #%datum #%app) ; extends typed rosette (require (prefix-in ro: rosette)) ; untyped diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt @@ -1,11 +1,17 @@ ;#lang turnstile #lang racket/base +;; (require racket/require) +;; (require +;; (except-in +;; (subtract-in "../../../turnstile/turnstile.rkt" +;; (except-in "../ext-stlc.rkt" #%app #%top #%datum)))) (require (except-in "../../../turnstile/turnstile.rkt" - #%module-begin zero? void sub1 or and not add1 = - * + boolean? integer?) + #%module-begin + zero? void sub1 or and not add1 = - * + boolean? integer? list) (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) (provide (rename-out [ro:#%module-begin #%module-begin])) (extends "../ext-stlc.rkt" #:except if #%app #%module-begin) -(reuse List #:from "../stlc+cons.rkt") +(reuse List list #:from "../stlc+cons.rkt") (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))