From 541c1e64a923cc64c84e08a5fcac7593b69a82a6 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 22 Jul 2016 16:47:39 -0400 Subject: [PATCH] add list to typed rosette --- turnstile/examples/rosette/bv.rkt | 4 +++- turnstile/examples/rosette/fsm.rkt | 4 +++- 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 index 40b5838..68b9cb3 100644 --- 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 index 44a8938..a035bf2 100644 --- 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 index efd0768..ff5c1ab 100644 --- 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))