From 3d92dbdde32e62c2060ea590a72d50679b477fc0 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 31 Aug 2016 18:49:25 -0400 Subject: [PATCH] add #lang turnstile/lang; change #lang turnstile's #%module-begin --- turnstile/examples/exist.rkt | 2 +- turnstile/examples/ext-stlc.rkt | 2 +- turnstile/examples/fomega.rkt | 2 +- turnstile/examples/fomega2.rkt | 2 +- turnstile/examples/fomega3.rkt | 2 +- turnstile/examples/fsub.rkt | 2 +- turnstile/examples/infer.rkt | 2 +- turnstile/examples/mlish.rkt | 2 +- turnstile/examples/rosette/bv.rkt | 6 ------ turnstile/examples/rosette/fsm.rkt | 7 +------ turnstile/examples/rosette/ifc.rkt | 7 +------ turnstile/examples/rosette/rosette.rkt | 15 ++------------- turnstile/examples/rosette/rosette2.rkt | 5 +++-- turnstile/examples/stlc+box.rkt | 2 +- turnstile/examples/stlc+cons.rkt | 2 +- turnstile/examples/stlc+effect.rkt | 2 +- turnstile/examples/stlc+lit.rkt | 2 +- turnstile/examples/stlc+rec-iso.rkt | 2 +- turnstile/examples/stlc+reco+sub.rkt | 2 +- turnstile/examples/stlc+reco+var.rkt | 2 +- turnstile/examples/stlc+sub.rkt | 2 +- turnstile/examples/stlc+tup.rkt | 2 +- turnstile/examples/stlc+union+case.rkt | 2 +- turnstile/examples/stlc+union.rkt | 2 +- turnstile/examples/stlc.rkt | 2 +- turnstile/examples/sysf.rkt | 2 +- turnstile/lang.rkt | 9 +++++++++ turnstile/lang/.DS_Store | Bin 0 -> 6148 bytes turnstile/lang/lang/reader.rkt | 2 ++ turnstile/lang/reader.rkt | 2 +- turnstile/main.rkt | 6 ++++++ turnstile/turnstile.rkt | 9 +++++---- 32 files changed, 51 insertions(+), 59 deletions(-) create mode 100644 turnstile/lang.rkt create mode 100644 turnstile/lang/.DS_Store create mode 100644 turnstile/lang/lang/reader.rkt create mode 100644 turnstile/main.rkt diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 5f149ea..868ac40 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+reco+var.rkt") (reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=? diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt index de82559..f380703 100644 --- a/turnstile/examples/ext-stlc.rkt +++ b/turnstile/examples/ext-stlc.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+lit.rkt" #:except #%datum) (provide ⊔ (for-syntax current-join)) diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt index 02da793..91b6271 100644 --- a/turnstile/examples/fomega.rkt +++ b/turnstile/examples/fomega.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt index e935c3b..16cc43b 100644 --- a/turnstile/examples/fomega2.rkt +++ b/turnstile/examples/fomega2.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") diff --git a/turnstile/examples/fomega3.rkt b/turnstile/examples/fomega3.rkt index 8a558b5..6459123 100644 --- a/turnstile/examples/fomega3.rkt +++ b/turnstile/examples/fomega3.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "sysf.rkt" #:except #%datum ∀ Λ inst) (reuse String #%datum #:from "stlc+reco+var.rkt") (require (only-in "fomega.rkt" current-kind? ∀★? ★? kind?)) diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index ff918e3..f45138d 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+reco+sub.rkt" #:except +) (require (rename-in (only-in "sysf.rkt" ∀? ∀ ~∀) [~∀ ~sysf:∀] [∀ sysf:∀])) diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt index 14a4fc5..0628b83 100644 --- a/turnstile/examples/infer.rkt +++ b/turnstile/examples/infer.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "ext-stlc.rkt" #:except #%app λ ann) (reuse inst #:from "sysf.rkt") (require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ)) diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index 07363f4..a259187 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (require racket/fixnum racket/flonum (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 53d420f..1825baa 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -1,10 +1,4 @@ #lang turnstile -;#lang racket/base -#;(require (except-in "../../../turnstile/turnstile.rkt" - #%module-begin - zero? void error sub1 or and not add1 = >= <= < > - * + boolean? integer? real? positive? string? quote pregexp - make-parameter equal? eq? list ~Any) - (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) (extends "rosette2.rkt" ; extends typed rosette #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) (require (only-in "../stlc+lit.rkt" define-primop)) diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt index a035bf2..dec8358 100644 --- a/turnstile/examples/rosette/fsm.rkt +++ b/turnstile/examples/rosette/fsm.rkt @@ -1,9 +1,4 @@ -;#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? list) - (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) +#lang turnstile (extends "rosette.rkt" #:except #%datum #%app) ; extends typed rosette (require (prefix-in ro: rosette)) ; untyped (require (prefix-in ro: rosette/lib/synthax)) diff --git a/turnstile/examples/rosette/ifc.rkt b/turnstile/examples/rosette/ifc.rkt index ccfb813..bb5a3d1 100644 --- a/turnstile/examples/rosette/ifc.rkt +++ b/turnstile/examples/rosette/ifc.rkt @@ -1,9 +1,4 @@ -;#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? list) - (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) +#lang turnstile (extends "rosette.rkt" #:except) ; extends typed rosette (require (prefix-in ro: rosette)) ; untyped (require (prefix-in ro: rosette/lib/synthax)) diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt index b4a6254..73f707f 100644 --- a/turnstile/examples/rosette/rosette.rkt +++ b/turnstile/examples/rosette/rosette.rkt @@ -1,22 +1,11 @@ -;#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? list) - (for-syntax (except-in "../../../turnstile/turnstile.rkt"))) -(provide (rename-out [ro:#%module-begin #%module-begin])) +#lang turnstile (extends "../stlc+union+case.rkt" #:except if #%app #%module-begin add1 sub1 +) (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)) (require (prefix-in ro: rosette/lib/synthax)) -(provide BVPred) +(provide BVPred (rename-out [ro:#%module-begin #%module-begin])) (define-simple-macro (define-rosette-primop op:id : ty) (begin diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 91a5f35..9a9c8da 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -1,12 +1,13 @@ #lang turnstile (extends "../stlc.rkt" - #:except #%app →) + #:except #%module-begin #%app →) (reuse #%datum #:from "../stlc+union.rkt") (reuse define-type-alias #:from "../stlc+reco+var.rkt") (reuse define-named-type-alias #:from "../stlc+union.rkt") (reuse list #:from "../stlc+cons.rkt") -(provide Any Nothing +(provide (rename-out [ro:#%module-begin #%module-begin]) + Any Nothing CU U C→ → (for-syntax ~C→ C→?) Ccase-> ; TODO: symbolic case-> not supported yet diff --git a/turnstile/examples/stlc+box.rkt b/turnstile/examples/stlc+box.rkt index 19eeb4e..db65a84 100644 --- a/turnstile/examples/stlc+box.rkt +++ b/turnstile/examples/stlc+box.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+cons.rkt") ;; Simply-Typed Lambda Calculus, plus mutable references diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt index 23fdcfc..b366783 100644 --- a/turnstile/examples/stlc+cons.rkt +++ b/turnstile/examples/stlc+cons.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+reco+var.rkt") ;; Simply-Typed Lambda Calculus, plus cons diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt index 775e338..0ca4753 100644 --- a/turnstile/examples/stlc+effect.rkt +++ b/turnstile/examples/stlc+effect.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ) ;; Simply-Typed Lambda Calculus, plus mutable references diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt index ddc88e0..4f3d33d 100644 --- a/turnstile/examples/stlc+lit.rkt +++ b/turnstile/examples/stlc+lit.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc.rkt") (provide define-primop) diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt index 278ba66..7e5306b 100644 --- a/turnstile/examples/stlc+rec-iso.rkt +++ b/turnstile/examples/stlc+rec-iso.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+tup.rkt") (reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt") diff --git a/turnstile/examples/stlc+reco+sub.rkt b/turnstile/examples/stlc+reco+sub.rkt index 0cfe227..e8efe17 100644 --- a/turnstile/examples/stlc+reco+sub.rkt +++ b/turnstile/examples/stlc+reco+sub.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+sub.rkt" #:except #%app #%datum) (extends "stlc+reco+var.rkt" #:except #%datum + *) ;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt index bd1bf8b..c68bff9 100644 --- a/turnstile/examples/stlc+reco+var.rkt +++ b/turnstile/examples/stlc+reco+var.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*) (require (only-in "stlc+tup.rkt" [~× ~stlc:×])) (provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*)) diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt index b2493c0..7bb477d 100644 --- a/turnstile/examples/stlc+sub.rkt +++ b/turnstile/examples/stlc+sub.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+lit.rkt" #:except #%datum +) (reuse Bool String add1 #:from "ext-stlc.rkt") (require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)) diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt index d0312e6..985db16 100644 --- a/turnstile/examples/stlc+tup.rkt +++ b/turnstile/examples/stlc+tup.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "ext-stlc.rkt") (require (for-syntax racket/list)) diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt index 1567098..50018f5 100644 --- a/turnstile/examples/stlc+union+case.rkt +++ b/turnstile/examples/stlc+union+case.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+union.rkt" #:except #%app add1 sub1) (provide case→) diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt index a17b92e..2d66c41 100644 --- a/turnstile/examples/stlc+union.rkt +++ b/turnstile/examples/stlc+union.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "ext-stlc.rkt" #:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?) diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt index 73c0f70..9b1b4c6 100644 --- a/turnstile/examples/stlc.rkt +++ b/turnstile/examples/stlc.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (provide only-in (for-syntax current-type=? types=?)) (begin-for-syntax diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt index 106900b..85f9579 100644 --- a/turnstile/examples/sysf.rkt +++ b/turnstile/examples/sysf.rkt @@ -1,4 +1,4 @@ -#lang turnstile +#lang turnstile/lang (extends "stlc+lit.rkt") (reuse #:from "stlc+rec-iso.rkt") ; want this type=? diff --git a/turnstile/lang.rkt b/turnstile/lang.rkt new file mode 100644 index 0000000..a7c5960 --- /dev/null +++ b/turnstile/lang.rkt @@ -0,0 +1,9 @@ +#lang racket/base + +(provide (all-from-out + "turnstile.rkt" + macrotypes/typecheck)) + +(require "turnstile.rkt" + (only-in macrotypes/typecheck #%module-begin)) + diff --git a/turnstile/lang/.DS_Store b/turnstile/lang/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..5df42f891728c1fc9b8fa2ce7f2665d6f3a096b4 GIT binary patch literal 6148 zcmeHKJ8r^25S>XJ2`LRy8p^!_H&`L(1Y95pOQe865qftyV9t>{cGRmJE;q zGH_Hg$Kw2_D2Cf;nkL}d@|1)%C{=Y8bjtr22f5m_{?Xq3qm9n=E xUe0=LfxbXbf?Q9B@m37 literal 0 HcmV?d00001 diff --git a/turnstile/lang/lang/reader.rkt b/turnstile/lang/lang/reader.rkt new file mode 100644 index 0000000..c3e7100 --- /dev/null +++ b/turnstile/lang/lang/reader.rkt @@ -0,0 +1,2 @@ +#lang s-exp syntax/module-reader +turnstile/lang diff --git a/turnstile/lang/reader.rkt b/turnstile/lang/reader.rkt index a3c5d96..bd71fd8 100644 --- a/turnstile/lang/reader.rkt +++ b/turnstile/lang/reader.rkt @@ -1,2 +1,2 @@ #lang s-exp syntax/module-reader -turnstile/turnstile +turnstile/main diff --git a/turnstile/main.rkt b/turnstile/main.rkt new file mode 100644 index 0000000..c9fbf34 --- /dev/null +++ b/turnstile/main.rkt @@ -0,0 +1,6 @@ +#lang racket/base + +(provide #%module-begin (all-from-out "turnstile.rkt")) + +(require "turnstile.rkt") + diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 0546f88..4b7fa90 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -4,10 +4,11 @@ define-typed-syntax (for-syntax syntax-parse/typed-syntax)) -(require (rename-in - macrotypes/typecheck - [define-typed-syntax -define-typed-syntax] - )) +(require (except-in (rename-in + macrotypes/typecheck + [define-typed-syntax -define-typed-syntax] + ) + #%module-begin)) (module typecheck+ racket/base (provide (all-defined-out))