commit fcbab12a9a0ea7e81d84f111b0bfe6f77834c681
parent e05e60a5668d6c40dde62df5493fd8e7198c448f
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 3 Sep 2014 14:14:14 -0400
stlc+cons+defined-via-racket-ext: add top level define
Diffstat:
3 files changed, 395 insertions(+), 244 deletions(-)
diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
@@ -1,17 +1,21 @@
-#lang racket/base
+#lang racket
(require
+ racket/stxparam
(for-syntax
- racket/base syntax/parse syntax/parse/experimental/template
- racket/syntax syntax/stx
+ ;racket/base
+ syntax/parse syntax/parse/experimental/template
+ racket/syntax syntax/stx;racket/stxparam syntax/id-table
"stx-utils.rkt")
(for-meta 2 racket/base syntax/parse))
(require "typecheck.rkt")
-(provide (except-out (all-from-out racket/base) #%module-begin))
+(provide (except-out (all-from-out racket) #%module-begin))
;; Extension of Racket for implementing typed languages
-(provide define-simple-syntax/type-rule
+(provide define-typed-syntax ;define-typed-top-level-syntax
+ define-primop ;define-syntax/type-rule
declare-base-type declare-base-types)
+ ;$this (for-syntax extends))
(provide (rename-out [mb/ext #%module-begin]))
;; provide syntax-classes
(provide (for-syntax integer str boolean))
@@ -26,47 +30,103 @@
(define-syntax-rule (declare-base-types τ ...)
(begin (declare-base-type τ) ...))
+;(begin-for-syntax
+; (define defined-names (make-free-id-table)))
+;(define-syntax-parameter
+; $this
+; (λ (stx)
+; (syntax-parse stx
+; [(_ x)
+; #:when (printf "~a\n" (free-id-table-ref defined-names #'λ))
+; (free-id-table-ref defined-names #'x)])))
+
(begin-for-syntax
;; concrete-τ? : determines if a type is a concrete type or has pattern vars
;; result is used to determine whether to insert ellipses in the output pattern
(define (concrete-τ? τ)
(or (and (identifier? τ) (member τ lit-set free-identifier=?))
(and (not (identifier? τ)) (stx-andmap concrete-τ? τ))))
+ ;; ** syntax-class: type ----------------------------------------
(define-syntax-class type
(pattern any))
- ;; meta-term is the term pattern in meta-language
+ ;; **syntax-class: meta-term ----------------------------------------
+ ;; - is the term pattern in meta-language
;; (ie where the type rules are declared)
;; - matches type vars
(define-syntax-class meta-term #:datum-literals (:)
+ ;; define-like binding form
+ (pattern (name:id (f:id [x:id : τ] ... (~optional (~and ldots (~literal ...)))) : τ_result e ...)
+ #:attr args-pat/notypes (template ((f x ... (?? ldots)) e ...))
+ #:attr typevars-pat (template (τ_result τ ... (?? ldots))))
+ ;; lambda-like binding form
(pattern (name:id ([x:id : τ] ... (~optional (~and ldots (~literal ...)))) e ...)
- #:attr args/notypes (template ((x ... (?? ldots)) e ...))
- #:attr typevars (template (τ ... (?? ldots))))
+ #:attr args-pat/notypes (template ((x ... (?? ldots)) e ...))
+ #:attr typevars-pat (template (τ ... (?? ldots))))
+ ;; let-like binding form
+ (pattern (name:id ([x:id ex] ... (~optional (~and ldots (~literal ...)))) e ...)
+ #:attr args-pat/notypes (template (([x ex] ... (?? ldots)) e ...))
+ #:attr typevars-pat #'())
+ ;; the list of ids after the name is in curly parens and represents a type declaration
+ ;; for the arguments (which can be any type)
+ ;; example: cons
+ (pattern (name:id τs e ...)
+ #:when (curly-parens? #'τs)
+ #:attr args-pat/notypes #'(e ...)
+ #:attr typevars-pat #'τs)
(pattern (name:id e ...)
- #:attr args/notypes #'(e ...)
- #:attr typevars #'())
- #;(pattern (name:id . n)
- #:attr args/notypes #'n
- #:attr typevars #'()))
- ;; term matches concrete terms in the actual (typed) language
+ #:attr args-pat/notypes #'(e ...)
+ #:attr typevars-pat #'()))
+ ;; **syntax-class: term ----------------------------------------
+ ;; - matches concrete terms in the actual (typed) language
;; - matches concrete types
;; name identifier is the extended form
- (define-syntax-class term
+ (define-syntax-class term #:datum-literals (:)
+ ;; define-like binding form
+ (pattern (name:id (f:id [x:id : τ] ...) : τ_result e ...)
+; #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
+; (expand/df #'(λ (f x ...) e ...)))
+; ;; identifiers didnt get a type bc racket has no %#var form
+; #:with es++ (with-extended-type-env #'([x τ] ...)
+; (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+; #:attr expanded-args #'(xs+ . es++)
+ #:attr expanded-args #'((f x ...) e ...)
+ #:attr types #'(τ_result τ ...))
+ ;; lambda-like binding form
(pattern (name:id ([x:id : τ] ...) e ...)
#:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
- (expand/df #'(λ (x ...) e ...)))
+ (expand/df #'(λ (x ...) e ...)))
;; identifiers didnt get a type bc racket has no %#var form
#:with es++ (with-extended-type-env #'([x τ] ...)
- (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+ (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
#:attr expanded-args #'(xs+ . es++)
#:attr types #'(τ ...))
+ ;;let-like binding form
+ (pattern (name:id ([x:id ex] ...) e ...)
+ #:with (ex+ ...) (stx-map expand/df #'(ex ...))
+ #:with (τ ...) (stx-map typeof #'(ex+ ...))
+ #:with (lam (x+ ...) . es+) (with-extended-type-env #'([x τ] ...)
+ (expand/df #'(λ (x ...) e ...)))
+ ;; identifiers didnt get a type bc racket has no %#var form
+ #:with es++ (with-extended-type-env #'([x τ] ...)
+ (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+ #:attr expanded-args #'(([x+ ex+] ...) . es++)
+ #:attr types #'())
+ ;; the list of ids after the name is in curly parens and represents a type declaration
+ ;; for the arguments (which can be any type)
+ ;; example: cons
+ (pattern (name:id τs e ...)
+ #:when (curly-parens? #'τs)
+ #:with (e+ ...) (stx-map expand/df #'(e ...))
+ #:attr expanded-args #'(e+ ...)
+ #:attr types #'τs)
(pattern (name:id e ...)
#:with (e+ ...) (stx-map expand/df #'(e ...))
#:attr expanded-args #'(e+ ...)
- #:attr types #'())
- #;(pattern (name:id . n)
- #:attr expanded-args #'n
#:attr types #'()))
- (define-splicing-syntax-class τ-constraint #:datum-literals (:= : let typeof ==)
+ ;; **syntax-class: τ-constraint ----------------------------------------
+ (define-splicing-syntax-class
+ τ-constraint
+ #:datum-literals (:= : let typeof == Γ-extend)
(pattern (let τ := (typeof e))
#:attr pattern-directive #'(#:with τ (typeof #'e)))
(pattern (e : τ)
@@ -75,6 +135,9 @@
#:attr pattern-directive #'(#:fail-unless (type=? #'τ1 #'τ2)
(format "type ~a and ~a should be equal"
(syntax->datum #'τ1) (syntax->datum #'τ2))))
+ (pattern (Γ-extend [f : τ] ... (~optional (~and ldots (~literal ...))))
+ #:attr pattern-directive
+ #`(#:when (Γ (type-env-extend #'([f τ] ... #,@(template ((?? ldots))))))))
(pattern (~seq (e0 : τ0) (~literal ...))
#:when (concrete-τ? #'τ0)
#:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 (... ...)))))
@@ -83,14 +146,15 @@
#:attr pattern-directive #'(#:when (stx-andmap assert-type #'(e0 (... ...)) #'(τ0 (... ...)))))))
-
-;; define-term/type-rule
-(define-syntax (define-simple-syntax/type-rule stx)
+;; define-typed-syntax
+(define-syntax (define-typed-syntax stx)
(syntax-parse stx #:datum-literals (:)
[(_ meta-e:meta-term : meta-τ
(~optional (~seq #:where
- c:τ-constraint ...)))
+ c:τ-constraint ...))
+ (~optional (~seq #:expanded expanded-e)))
#:with fresh-name (generate-temporary #'meta-e.name)
+; #:when (free-id-table-set! defined-names #'meta-e.name #'fresh-name)
#:with lits lit-set
(template
(begin
@@ -100,24 +164,41 @@
[e:term
;; shadow pattern vars representing subterms with its expansion
;; - except for the name of the form, since result must use base form
- #:with meta-e.args/notypes #'e.expanded-args
- #:with meta-e.typevars #'e.types
+ #:with meta-e.args-pat/notypes #'e.expanded-args
+ #:with meta-e.typevars-pat #'e.types
(?? (?@ . ((?@ . c.pattern-directive) ...)))
- (⊢ (syntax/loc stx (meta-e.name . meta-e.args/notypes)) #'meta-τ)]
+ (⊢ (syntax/loc
+ stx
+ (?? expanded-e
+ (meta-e.name . meta-e.args-pat/notypes)))
+ #'meta-τ)]
[_ #:when (type-error #:src stx #:msg "type error") #'(void)]
))))]))
-
-;; overload mod-begin to check for define-literal-type-rule
+
+
+;; overload mod-begin to check for define-literal-type-rule and other top-level forms
(begin-for-syntax
- (define-syntax-class def #:datum-literals (define-literal-type-rule extends)
- (pattern (extends m ...)
- #:attr other #'() #:attr stxc #'() #:attr lit-τ #'()
- #:attr base-mod #'(m ...))
+ (define-syntax-class def #:datum-literals (define-literal-type-rule extends inherit-types)
+ (pattern (extends m f ...)
+; #:when (stx-map
+; (λ (f)
+; (free-id-table-set!
+; defined-names
+; f
+; (format-id #'m "ext:~a" f)))
+; #'(f ...))
+ #:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr inherited-τs #'()
+ #:attr base-mod #'(m) #:attr ext-fs #'(f ...))
+ (pattern (inherit-types τ ...)
+ #:attr inherited-τs #'(τ ...)
+ #:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'())
(pattern (define-literal-type-rule stx-class : τ)
- #:attr other #'() #:attr base-mod #'()
+ #:attr other #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'()
#:attr stxc #'(stx-class)
#:attr lit-τ #'(τ))
- (pattern any #:attr other #'(any) #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'())))
+ (pattern any
+ #:attr other #'(any)
+ #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'())))
(define-syntax (mb/ext stx)
(syntax-parse stx
@@ -125,6 +206,8 @@
#:with (stxc ...) (template ((?@ . d.stxc) ...))
#:with (lit-τ ...) (template ((?@ . d.lit-τ) ...))
#:with (base-mod ...) (template ((?@ . d.base-mod) ...))
+ #:with (inherited-τ ...) (template ((?@ . d.inherited-τs) ...))
+ #:when (set! lit-set (append (syntax->list #'(inherited-τ ...)) lit-set))
;; check that
#:fail-unless (let ([len (stx-length #'(base-mod ...))]) (or (zero? len) (= len 1)))
(format "Supply either 0 or 1 base modules. Given ~a"
@@ -132,48 +215,65 @@
#:with m (if (zero? (stx-length #'(base-mod ...)))
#'()
(car (syntax->list #'(base-mod ...))))
+ #:with (f ...) (template ((?@ . d.ext-fs) ...))
+ #:with (ext-f ...) (stx-map (λ (f) (format-id #'m "ext:~a" f)) #'(f ...))
+; (template ((?@ . d.ext-fs) ...)))
#:with my-datum (generate-temporary)
#:with datum-def
#`(define-syntax (my-datum stx)
(syntax-parse stx
[(_ . x) #:declare x stxc (⊢ (syntax/loc stx (r:#%datum . x)) #'lit-τ)]
...
+ ;; try previous version of #%datum, if it exists, ie if we are extending
#,@(if (stx-null? #'m)
- #'()
- #`([(_ . x)
-; ;; prev-datum = #%datum in the meta-language
-; #:with prev-datum (datum->syntax stx '#%datum)
-; #:with racket-datum (datum->syntax stx 'r:#%datum)
-; ; when prev-datum is not racket's #%datum
-; #:when (not (free-identifier=? #'prev-datum #'racket-datum))
- (syntax/loc stx (#,(datum->syntax stx 'ext:#%datum) . x))]))
+ #'()
+ #`([(_ . x)
+ (syntax/loc stx (#,(datum->syntax #'m 'ext:#%datum) . x))]))
[(_ . x)
#:when (type-error #:src stx #:msg "Don't know the type for literal: ~a" #'x)
(syntax/loc stx (r:#%datum . x))]))
- #`(#%module-begin
+ #:with my-mb (generate-temporary)
+ #:with mb-def
+ #'(define-syntax (my-mb stx)
+ (syntax-parse stx
+ [(_ def (... ...))
+ #:with mb-let (expand/df #'(r:let () def (... ...) (r:void)))
+ #'(r:#%module-begin mb-let)]))
+ #`(#%module-begin
+; (require (for-syntax syntax/id-table))
+; (begin-for-syntax
+; (define defined-names (make-free-id-table)))
#,@(if (stx-null? #'m)
#'()
- #`((require (prefix-in ext: m))
+ #`((require (only-in m inherited-τ ...))
+ (provide inherited-τ ...)
(require racket/provide)
+ (require (prefix-in ext: (except-in m inherited-τ ...)))
(provide
(filtered-out
(lambda (name)
+ #;(printf "inheriting from ~a: ~a\n"
+ #,(syntax->datum #'m)
+ (and (regexp-match? #rx"^ext:.+$" name)
+ (regexp-replace #rx"ext:" name "")))
(and (regexp-match? #rx"^ext:.+$" name)
(regexp-replace #rx"ext:" name "")))
(except-out (all-from-out m)
- #,(datum->syntax stx 'ext:#%datum)
- #,(datum->syntax stx 'ext:check-type-error)
- #,(datum->syntax stx 'ext:check-type)
- #,(datum->syntax stx 'ext:check-not-type)
- #,(datum->syntax stx 'ext:check-type-and-result)))
- )))
+ ext-f ...
+ #,(datum->syntax #'m 'ext:#%datum)
+ #,(datum->syntax #'m 'ext:#%module-begin)
+ #,(datum->syntax #'m 'ext:check-type-error)
+ #,(datum->syntax #'m 'ext:check-type)
+ #,(datum->syntax #'m 'ext:check-not-type)
+ #,(datum->syntax #'m 'ext:check-type-and-result))))))
(require (prefix-in r: racket/base))
- (provide (rename-out [r:#%module-begin #%module-begin]
- [r:#%top-interaction #%top-interaction]))
+ (provide (rename-out [r:#%top-interaction #%top-interaction]))
(provide (rename-out [my-datum #%datum]))
datum-def
+ (provide (rename-out [my-mb #%module-begin]))
+ mb-def
#,@(template ((?@ . d.other) ...))
- ;; testing forms
+ ;; testing forms --------------------
(require (for-syntax rackunit))
(require rackunit)
(provide check-equal?)
diff --git a/stlc+define+cons-via-racket-extended-tests.rkt b/stlc+define+cons-via-racket-extended-tests.rkt
@@ -7,73 +7,74 @@
;; check fns with literal or id bodies
(check-type (λ ([x : Int]) x) : (Int → Int))
-;(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
+(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
;; check fns with multi-expr body
-;(check-type (λ ([x : Int]) (void) x) : (Int → Int))
-;(check-type-error (λ ([x : Int]) 1 x))
-;(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
-;
+(check-type (λ ([x : Int]) (void) x) : (Int → Int))
+(check-type-error (λ ([x : Int]) 1 x))
+(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
+
+; printf
;(check-type (λ ([x : Int]) (printf {Int} "~a\n" x) x) : (Int → Int))
;(check-type-error (λ ([x : Int]) (printf {String} "~a\n" x) x))
;(check-type-error (λ ([x : Int]) (printf {Int} 1 x) x))
;(check-type (λ ([x : Int]) (printf "one") x) : (Int → Int))
;(check-type-error (λ ([x : Int]) (printf "~a" x) x))
;(check-type-and-result ((λ ([x : Int]) (printf {Int} "~a\n" x) (+ x 1)) 100) : Int => 101)
-;
-;;; multi arity primops
-;(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
-;(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
-;(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
-;(check-type-error (λ ([y : Int] [z : Int]) (= y)))
-;(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
-;(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
-;(check-type-error (λ ([y : Int] [z : Int]) (< y)))
-;(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
-;(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
-;(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
-;;; the following still fails bc varargs not handled
-;;(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
-;(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
-;(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
-;(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
-;
+
+;; multi arity primops
+(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
+(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
+(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
+(check-type-error (λ ([y : Int] [z : Int]) (= y)))
+(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
+(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
+(check-type-error (λ ([y : Int] [z : Int]) (< y)))
+(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
+(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
+(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
+;; the following HO example still fails bc varargs not handled
+;(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
+(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
+(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
+(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
+
;; HO fn
-;(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
-;(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
-;(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
-;(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
-;
-;;; shadowed var
-;(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
-;(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
-;
-;;; let
-;(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
-;(check-type-error (let ([x 1] [y "two"]) (+ x y)))
-;(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
-;
+(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
+(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
+(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
+(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
+
+;; shadowed var
+(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
+(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
+
+;; let
+(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
+(check-type-error (let ([x 1] [y "two"]) (+ x y)))
+(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
+
;;; lists
-;(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
-;(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
-;(check-type-error (cons {Int} 1 (null {String})))
-;(check-type-error (cons {Int} "one" (null {Int})))
-;(check-type-error (cons {String} 1 (null {Int})))
-;(check-type-error (cons {String} 1 (null {Int})))
-;(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
-;(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
-; : String => "one")
-;(check-type-and-result (null? {String} (null {String})) : Bool => #t)
-;(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
-;(check-type-error (null? {String} (null {Int})))
-;(check-type-error (null? {Int} (null {String})))
-;(check-type-error (null? {Int} 1))
-;(check-type-error (null? {Int} "one"))
-;(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
-;
+(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
+(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
+(check-type-error (cons {Int} 1 (null {String})))
+(check-type-error (cons {Int} "one" (null {Int})))
+(check-type-error (cons {String} 1 (null {Int})))
+(check-type-error (cons {String} 1 (null {Int})))
+(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
+(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
+ : String => "one")
+(check-type-and-result (null? {String} (null {String})) : Bool => #t)
+(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
+(check-type-error (null? {String} (null {Int})))
+(check-type-error (null? {Int} (null {String})))
+(check-type-error (null? {Int} 1))
+(check-type-error (null? {Int} "one"))
+(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
+
;; begin and void
(check-type (void) : Unit)
(check-type-and-result (begin (void) 1) : Int => 1)
@@ -82,51 +83,51 @@
(check-type-and-result (begin (+ 1 2)) : Int => 3)
(check-type-error (begin 1 2))
-;(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
-;(check-type-error (λ ([x : Int]) 1 1))
-;(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
-;(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
-; : Int => 6)
-;
+(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
+(check-type-error (λ ([x : Int]) 1 1))
+(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
+(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
+ : Int => 6)
+
;; define
-;(define (g [y : Int]) : Int
-; (+ (f y) 1))
-;(define (f [x : Int]) : Int
-; (+ x 1))
-;(check-type-and-result (f 10) : Int => 11)
-;(check-type-and-result (g 100) : Int => 102)
-;(check-not-type (f 10) : String)
-;(check-not-type (g 100) : String)
-;
-;;; if
-;(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
-;(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
-;(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
-;(check-type-error (if (null? {Int} (null {Int})) "one" 1))
+(define (g [y : Int]) : Int
+ (+ (f y) 1))
+(define (f [x : Int]) : Int
+ (+ x 1))
+(check-type-and-result (f 10) : Int => 11)
+(check-type-and-result (g 100) : Int => 102)
+(check-not-type (f 10) : String)
+(check-not-type (g 100) : String)
+
+;; if
+(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
+(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
+(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
+(check-type-error (if (null? {Int} (null {Int})) "one" 1))
(check-type-error (if 1 2 3))
(check-type-and-result (if #t 1 2) : Int => 1)
(check-type-and-result (if #f 1 2) : Int => 2)
(check-type-error (if #t 1 #f))
-;;;; recursive fn
-;(define (add1 [x : Int]) : Int
-; (+ x 1))
-;(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
-; (if (null? {Int} lst)
-; (null {Int})
-; (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
-;(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
-; : (Listof Int)
-; => (cons {Int} 2 (cons {Int} 3 (null {Int}))))
-;(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
-; : (Listof String))
-;
-;;; recursive types
-;(define (a [x : Int]) : Int (b x))
-;(define (b [x : Int]) : Int (a x))
-;(define (ff [x : Int]) : Int (ff x))
-;
-;;; define-type (non parametric)
+;;; recursive fn
+(define (add1 [x : Int]) : Int
+ (+ x 1))
+(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
+ (if (null? {Int} lst)
+ (null {Int})
+ (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
+(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
+ : (Listof Int)
+ => (cons {Int} 2 (cons {Int} 3 (null {Int}))))
+(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
+ : (Listof String))
+
+;; recursive types
+(define (a [x : Int]) : Int (b x))
+(define (b [x : Int]) : Int (a x))
+(define (ff [x : Int]) : Int (ff x))
+
+;; define-type (non parametric)
;(define-type MaybeInt (variant (None) (Just Int)))
;(check-type (None) : MaybeInt)
;(check-type (Just 10) : MaybeInt)
diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt
@@ -1,5 +1,6 @@
#lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
-(extends "stlc-via-racket-extended.rkt")
+(extends "stlc-via-racket-extended.rkt" λ)
+(inherit-types Int →)
;(require "stlc-via-racket-extended.rkt")
;(provide Int → + λ #%app #%top-interaction #%module-begin)
@@ -23,7 +24,7 @@
define-type cases
(rename-out
[datum/tc #%datum]
- [void/tc void] [printf/tc printf]
+ #;[void/tc void] [printf/tc printf]
[λ/tc λ] [let/tc let]
; for #%app, must prefix and re-provide because this file needs to use racket's #%app
[stlc:#%app #%app]
@@ -36,7 +37,7 @@
;; Simply-Typed Lambda Calculus+
;; - stlc extended with practical language feature
-;; - implemented in racket/extended lang
+;; - implemented in racket-extended lang
;; Features:
;; - stlc
;; - multi-expr lam bodies
@@ -71,6 +72,13 @@
#:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
#'(begin
(struct Cons (x ...) #:transparent))]))
+#;(define-syntax/type-rule #:keywords (variant)
+ [(define-type τ (variant (Cons τ_fld ...) ...))
+ #:where
+ (Γ-extend [Cons : (τ_fld ... → τ)] ...)
+ #:expanded
+ (begin (struct Cons (τ_fld ...) #:transparent) ...)])
+
#;(define-syntax (cases stx)
(syntax-parse stx #:literals (→)
[(_ e [Cons (x ...) body ... body_result] ...)
@@ -101,7 +109,7 @@
[(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)]
[(_ . x) #'(stlc:#%datum . x)]))
-(define-simple-syntax/type-rule
+(define-typed-syntax
(begin e ... e_result) : τ_result
#:where
(e : Unit) ...
@@ -118,7 +126,7 @@
(syntax-parse stx
[(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
-(define-simple-syntax/type-rule
+#;(define-simple-syntax/type-rule
(void) : Unit)
#;(define-syntax (printf/tc stx)
@@ -136,14 +144,15 @@
#:when (assert-String-type #'str+)
(⊢ (syntax/loc stx (printf str+)) #'Unit)]))
-;(define-primop + : (Int ... → Int))
-;(define-primop - : (Int Int ... → Int))
-;(define-primop = : (Int Int Int ... → Bool))
-;(define-primop < : (Int Int Int ... → Bool))
-;(define-primop or : (Bool ... → Bool))
-;(define-primop and : (Bool ... → Bool))
-;(define-primop not : (Bool → Bool))
-;(define-primop abs : (Int → Int))
+;(define-primop + : Int ... → Int)
+(define-primop - : Int Int ... → Int)
+(define-primop = : Int Int Int ... → Bool)
+(define-primop < : Int Int Int ... → Bool)
+(define-primop or : Bool ... → Bool)
+(define-primop and : Bool ... → Bool)
+(define-primop not : Bool → Bool)
+(define-primop abs : Int → Int)
+(define-primop void : → Unit)
#;(define-syntax (λ/tc stx)
@@ -165,6 +174,13 @@
#:with τ_body (typeof #'e_result++)
(⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(τ ... → τ_body))]))
+(define-typed-syntax
+ (λ ([x : τ] ...) e ... e_result) : (τ ... → τ_body)
+ #:where
+ (e : Unit) ...
+ (let τ_body := (typeof e_result)))
+
+
;; #%app
;; TODO: support varargs
#;(define-syntax (app/tc stx)
@@ -187,6 +203,12 @@
#:when (stx-andmap assert-Unit-type #'(e+ ...))
(⊢ (syntax/loc stx (let ([x+ e_x+] ...) e+ ... e_result+)) (typeof #'e_result+))]))
+(define-typed-syntax
+ (let ([x ex] ...) e ... e_result) : τ_result
+ #:where
+ (e : Unit) ...
+ (let τ_result := (typeof e_result)))
+
#;(define-syntax (if/tc stx)
(syntax-parse stx
[(_ e_test e1 e2)
@@ -200,7 +222,7 @@
#'e1 (typeof #'e1+)
#'e2 (typeof #'e2+)))
(⊢ (syntax/loc stx (if e_test+ e1+ e2+)) (typeof #'e1+))]))
-(define-simple-syntax/type-rule
+(define-typed-syntax
(if e_test e1 e2) : τ2
#:where
(e_test : Bool)
@@ -209,6 +231,28 @@
(τ1 == τ2))
;; lists ----------------------------------------------------------------------
+(define-typed-syntax
+ (cons {τ} e1 e2) : (Listof τ)
+ #:where
+ (e1 : τ)
+ (e2 : (Listof τ)))
+(define-typed-syntax
+ (null {τ}) : (Listof τ)
+ #:expanded
+ null)
+(define-typed-syntax
+ (null? {τ} e) : Bool
+ #:where
+ (e : (Listof τ)))
+(define-typed-syntax
+ (first {τ} e) : τ
+ #:where
+ (e : (Listof τ)))
+(define-typed-syntax
+ (rest {τ} e) : (Listof τ)
+ #:where
+ (e : (Listof τ)))
+
#;(define-syntax (cons/tc stx)
(syntax-parse stx
[(_ {T} e1 e2)
@@ -251,86 +295,92 @@
#'(define f (λ/tc ([x : τ] ...) e ...))]
[(_ x:id e) #'(define x e)]))
+(define-typed-syntax
+ (define (f [x : τ] ...) : τ_result e ...) : Unit
+ #:where
+ (Γ-extend [f : (τ ... → τ_result)])
+ #:expanded
+ (define f (ext:λ ([x : τ] ...) e ...)))
+
+;#;(begin-for-syntax
+; ;; EXTENSIBILITY NOTE:
+; ;; Originally, define-type was a #:literal instead of a #:datum-literal, but
+; ;; this became a problem when sysf extended define-type (but not modul-begin).
+; ;; Putting define-type in the #:literals list makes it always expect the stlc
+; ;; version of define-type, so it wasnt getting properly parsed in sysf.
+; ;;
+; ;; Similarly, I had to define the define-type pattern below to avoid explicitly
+; ;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
+; ;; version of define-type.
+; (define-syntax-class maybe-def #:datum-literals (define variant define-type)
+; (pattern define-fn
+; #:with (define (f x ...) body ...) #'define-fn
+; #:attr fndef #'(define-fn)
+; #:attr e #'() #:attr tydecl #'())
+; (pattern define-variant-type-decl
+; #:with (define-type TypeName (variant (Cons fieldτ ...) ...))
+; #'define-variant-type-decl
+; #:attr tydecl #'(define-variant-type-decl)
+; #:attr fndef #'() #:attr e #'())
+; (pattern define-type-decl
+; #:with (define-type TypeName:id (Cons:id fieldτ ...) ...)
+; #'define-type-decl
+; #:attr tydecl #'(define-type-decl)
+; #:attr fndef #'() #:attr e #'())
+; (pattern exp:expr
+; #:attr tydecl #'() #:attr fndef #'()
+; #:attr e #'(exp)))
+; (define-syntax-class strct #:literals (begin define-values define-syntaxes)
+; (pattern
+; (begin
+; (define-values (x ...) mk-strct-type-def)
+; (define-syntaxes (y) strct-info-def))
+; #:attr def-val #'(define-values (x ...) mk-strct-type-def)
+; #:attr def-syn #'(define-syntaxes (y) strct-info-def)))
+; (define-syntax-class def-val #:literals (define-values)
+; (pattern (define-values (x ...) vals)
+; #:attr lhs #'(x ...)
+; #:attr rhs #'vals))
+; (define-syntax-class def-syn #:literals (define-syntaxes)
+; (pattern (define-syntaxes (x) stxs)
+; #:attr lhs #'x
+; #:attr rhs #'stxs))
+; )
-#;(begin-for-syntax
- ;; EXTENSIBILITY NOTE:
- ;; Originally, define-type was a #:literal instead of a #:datum-literal, but
- ;; this became a problem when sysf extended define-type (but not modul-begin).
- ;; Putting define-type in the #:literals list makes it always expect the stlc
- ;; version of define-type, so it wasnt getting properly parsed in sysf.
- ;;
- ;; Similarly, I had to define the define-type pattern below to avoid explicitly
- ;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
- ;; version of define-type.
- (define-syntax-class maybe-def #:datum-literals (define variant define-type)
- (pattern define-fn
- #:with (define (f x ...) body ...) #'define-fn
- #:attr fndef #'(define-fn)
- #:attr e #'() #:attr tydecl #'())
- (pattern define-variant-type-decl
- #:with (define-type TypeName (variant (Cons fieldτ ...) ...))
- #'define-variant-type-decl
- #:attr tydecl #'(define-variant-type-decl)
- #:attr fndef #'() #:attr e #'())
- (pattern define-type-decl
- #:with (define-type TypeName:id (Cons:id fieldτ ...) ...)
- #'define-type-decl
- #:attr tydecl #'(define-type-decl)
- #:attr fndef #'() #:attr e #'())
- (pattern exp:expr
- #:attr tydecl #'() #:attr fndef #'()
- #:attr e #'(exp)))
- (define-syntax-class strct #:literals (begin define-values define-syntaxes)
- (pattern
- (begin
- (define-values (x ...) mk-strct-type-def)
- (define-syntaxes (y) strct-info-def))
- #:attr def-val #'(define-values (x ...) mk-strct-type-def)
- #:attr def-syn #'(define-syntaxes (y) strct-info-def)))
- (define-syntax-class def-val #:literals (define-values)
- (pattern (define-values (x ...) vals)
- #:attr lhs #'(x ...)
- #:attr rhs #'vals))
- (define-syntax-class def-syn #:literals (define-syntaxes)
- (pattern (define-syntaxes (x) stxs)
- #:attr lhs #'x
- #:attr rhs #'stxs))
- )
-
-#;(define-syntax (module-begin/tc stx)
- (syntax-parse stx #:literals (begin)
- [(_ mb-form:maybe-def ...)
- ;; handle define-type
- #:with (deftype ...) (template ((?@ . mb-form.tydecl) ...))
- #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
- #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
- #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
- #:with (def-val:def-val ...) #'(structdef+.def-val ...)
- #:with (def-val-lhs ...) #'(def-val.lhs ...)
- #:with (def-val-rhs ...) #'(def-val.rhs ...)
- #:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
- #:with (def-syn-lhs ...) #'(def-syn.lhs ...)
- #:with (def-syn-rhs ...) #'(def-syn.rhs ...)
- ;; handle defines
- #:with (deffn ...) (template ((?@ . mb-form.fndef) ...))
- #:with (deffn+:def-val ...) (stx-map expand/df/module-ctx #'(deffn ...))
- #:with (f ...) #'(deffn+.lhs ...)
- #:with (v ...) #'(deffn+.rhs ...)
- #:with (e ...) (template ((?@ . mb-form.e) ...))
- ;; base type env
- ; #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
-;; NOTE: for struct def, define-values *must* come before define-syntaxes
-;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
- (quasisyntax/loc stx
- (#%module-begin
- #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
- (let-syntax ([def-syn-lhs def-syn-rhs] ...)
- (letrec-values ([f v] ...) e ... (void)))))
- (define #,(datum->syntax stx 'runtime-env)
- (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
- (hash->list (Γ)))])
- (values (car x:τ) (cdr x:τ))))
- ))]))
+;#;(define-syntax (module-begin/tc stx)
+; (syntax-parse stx #:literals (begin)
+; [(_ mb-form:maybe-def ...)
+; ;; handle define-type
+; #:with (deftype ...) (template ((?@ . mb-form.tydecl) ...))
+; #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
+; #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
+; #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
+; #:with (def-val:def-val ...) #'(structdef+.def-val ...)
+; #:with (def-val-lhs ...) #'(def-val.lhs ...)
+; #:with (def-val-rhs ...) #'(def-val.rhs ...)
+; #:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
+; #:with (def-syn-lhs ...) #'(def-syn.lhs ...)
+; #:with (def-syn-rhs ...) #'(def-syn.rhs ...)
+; ;; handle defines
+; #:with (deffn ...) (template ((?@ . mb-form.fndef) ...))
+; #:with (deffn+:def-val ...) (stx-map expand/df/module-ctx #'(deffn ...))
+; #:with (f ...) #'(deffn+.lhs ...)
+; #:with (v ...) #'(deffn+.rhs ...)
+; #:with (e ...) (template ((?@ . mb-form.e) ...))
+; ;; base type env
+; ; #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
+;;; NOTE: for struct def, define-values *must* come before define-syntaxes
+;;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
+; (quasisyntax/loc stx
+; (#%module-begin
+; #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
+; (let-syntax ([def-syn-lhs def-syn-rhs] ...)
+; (letrec-values ([f v] ...) e ... (void)))))
+; (define #,(datum->syntax stx 'runtime-env)
+; (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
+; (hash->list (Γ)))])
+; (values (car x:τ) (cdr x:τ))))
+; ))]))
;; type checking testing: -----------------------------------------------------
;(require rackunit)
