commit 9de0cea48139f425bae2f85b70c22e6973383b49
parent fcbab12a9a0ea7e81d84f111b0bfe6f77834c681
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 3 Sep 2014 18:42:11 -0400
stlc+cons+defined-via-racket-ext: cases working, all tests passing; todo: abstract the meta(term) stx class
Diffstat:
3 files changed, 130 insertions(+), 68 deletions(-)
diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
@@ -54,6 +54,15 @@
;; (ie where the type rules are declared)
;; - matches type vars
(define-syntax-class meta-term #:datum-literals (:)
+ ;; cases
+ (pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+ (~optional (~and ldots (~literal ...))))
+ #:with (~datum cases) #'name
+ #:attr args-pat/notypes (template (e_test [Cons (x ...) body ...] ... (?? ldots)))
+ #:attr typevars-pat #'())
+ ;; define-type
+ (pattern (name:id τ_name:id τ_body)
+ #:attr args-pat/notypes #'()
+ #:attr typevars-pat #'(τ_name τ_body))
;; 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 ...))
@@ -81,6 +90,27 @@
;; - matches concrete types
;; name identifier is the extended form
(define-syntax-class term #:datum-literals (:)
+ ;; cases
+ (pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+)
+ #:with (~datum cases) #'name
+ #:with e_test+ (expand/df #'e_test)
+ #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
+ #:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
+ #:with ((lam (x+ ...) body+ ... body_result+) ...)
+ (stx-map (λ (bods xs τs)
+ (with-extended-type-env
+ (stx-map list xs τs)
+ (expand/df #`(λ #,xs #,@bods))))
+ #'((body ...) ...)
+ #'((x ...) ...)
+ #'((τ ...) ...))
+ #:attr expanded-args #'(e_test+ [Cons+ (x+ ...) body+ ... body_result+] ...)
+ #:attr types #'())
+ ;; define-type
+ (pattern (name:id τ_name:id τ_body)
+ ;;don't expand
+ #:attr expanded-args #'()
+ #:attr types #'(τ_name τ_body))
;; define-like binding form
(pattern (name:id (f:id [x:id : τ] ...) : τ_result e ...)
; #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
@@ -89,6 +119,7 @@
; #:with es++ (with-extended-type-env #'([x τ] ...)
; (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
; #:attr expanded-args #'(xs+ . es++)
+ ;; don't expand
#:attr expanded-args #'((f x ...) e ...)
#:attr types #'(τ_result τ ...))
;; lambda-like binding form
@@ -126,7 +157,11 @@
;; **syntax-class: τ-constraint ----------------------------------------
(define-splicing-syntax-class
τ-constraint
- #:datum-literals (:= : let typeof == Γ-extend)
+ #:datum-literals (:= : let typeof == Γ-extend with when:)
+ (pattern (when: e)
+ #:attr pattern-directive #'(#:when e))
+ (pattern (with pat e)
+ #:attr pattern-directive #'(#:with pat e))
(pattern (let τ := (typeof e))
#:attr pattern-directive #'(#:with τ (typeof #'e)))
(pattern (e : τ)
@@ -138,6 +173,8 @@
(pattern (Γ-extend [f : τ] ... (~optional (~and ldots (~literal ...))))
#:attr pattern-directive
#`(#:when (Γ (type-env-extend #'([f τ] ... #,@(template ((?? ldots))))))))
+ (pattern (~seq (let τ := (typeof e)) (~literal ...))
+ #:attr pattern-directive #'(#:with (τ (... ...)) (stx-map typeof #'(e (... ...)))))
(pattern (~seq (e0 : τ0) (~literal ...))
#:when (concrete-τ? #'τ0)
#:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 (... ...)))))
@@ -156,24 +193,23 @@
#: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
- (provide (rename-out [fresh-name meta-e.name]))
- (define-syntax (fresh-name stx)
- (syntax-parse stx #:literals lits
- [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-pat/notypes #'e.expanded-args
- #:with meta-e.typevars-pat #'e.types
- (?? (?@ . ((?@ . c.pattern-directive) ...)))
+ #`(begin
+ (provide (rename-out [fresh-name meta-e.name]))
+ (define-syntax (fresh-name stx)
+ (syntax-parse stx #:literals lits
+ [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-pat/notypes #'e.expanded-args
+ #:with meta-e.typevars-pat #'e.types
+ #,@(template ((?? (?@ . ((?@ . c.pattern-directive) ...)))))
(⊢ (syntax/loc
stx
- (?? expanded-e
- (meta-e.name . meta-e.args-pat/notypes)))
+ #,@(template ((?? 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 and other top-level forms
diff --git a/stlc+define+cons-via-racket-extended-tests.rkt b/stlc+define+cons-via-racket-extended-tests.rkt
@@ -128,55 +128,55 @@
(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)
-;(check-type-error (Just "ten"))
-;(check-type-error (Just (None)))
-;(define (maybeint->bool [maybint : MaybeInt]) : Bool
-; (cases maybint
-; [None () #f]
-; [Just (x) #t]))
-;(check-type-and-result (maybeint->bool (None)) : Bool => #f)
-;(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
-;(check-type-error (maybeint->bool 25))
-;(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
-; (cases maybint
-; [None () #f]
-; [Just (x) x])))
-;
-;(define-type IntList (variant (Null) (Cons Int IntList)))
-;(check-type-and-result (Null) : IntList => (Null))
-;(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
-;(check-type-error (Cons "one" (Null)))
-;(check-type-error (Cons 1 2))
-;(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
-; (cases lst
-; [Null () (Null)]
-; [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
-;(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
-;(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
-;(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null))))
-; : IntList => (Cons 3 (Cons 2 (Null))))
-;(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
-;(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-;(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
-; (cases lst
-; [BoolNull () (Null)]
-; [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
-;(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
-;(check-type-and-result
-; (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
-; : IntList => (Cons 1 (Null)))
-;(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
-;;; check typename is available
-;(check-type (λ ([lst : IntList])
-; (cases lst
-; [Null () (None)]
-; [Cons (x xs) (Just x)]))
-; : (IntList → MaybeInt))
-;(check-type ((λ ([lst : IntList])
-; (cases lst
-; [Null () (None)]
-; [Cons (x xs) (Just x)]))
-; (Null)) : MaybeInt)
-\ No newline at end of file
+(define-type MaybeInt (variant (None) (Just Int)))
+(check-type (None) : MaybeInt)
+(check-type (Just 10) : MaybeInt)
+(check-type-error (Just "ten"))
+(check-type-error (Just (None)))
+(define (maybeint->bool [maybint : MaybeInt]) : Bool
+ (cases maybint
+ [None () #f]
+ [Just (x) #t]))
+(check-type-and-result (maybeint->bool (None)) : Bool => #f)
+(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
+(check-type-error (maybeint->bool 25))
+(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
+ (cases maybint
+ [None () #f]
+ [Just (x) x])))
+
+(define-type IntList (variant (Null) (Cons Int IntList)))
+(check-type-and-result (Null) : IntList => (Null))
+(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
+(check-type-error (Cons "one" (Null)))
+(check-type-error (Cons 1 2))
+(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
+ (cases lst
+ [Null () (Null)]
+ [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
+(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
+(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
+(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null))))
+ : IntList => (Cons 3 (Cons 2 (Null))))
+(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
+(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
+(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
+ (cases lst
+ [BoolNull () (Null)]
+ [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
+(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
+(check-type-and-result
+ (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
+ : IntList => (Cons 1 (Null)))
+(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
+;; check typename is available
+(check-type (λ ([lst : IntList])
+ (cases lst
+ [Null () (None)]
+ [Cons (x xs) (Just x)]))
+ : (IntList → MaybeInt))
+(check-type ((λ ([lst : IntList])
+ (cases lst
+ [Null () (None)]
+ [Cons (x xs) (Just x)]))
+ (Null)) : MaybeInt)
+\ No newline at end of file
diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt
@@ -1,6 +1,7 @@
#lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
(extends "stlc-via-racket-extended.rkt" λ)
(inherit-types Int →)
+(require (for-syntax syntax/stx) "typecheck.rkt")
;(require "stlc-via-racket-extended.rkt")
;(provide Int → + λ #%app #%top-interaction #%module-begin)
@@ -72,6 +73,15 @@
#:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
#'(begin
(struct Cons (x ...) #:transparent))]))
+
+(define-typed-syntax
+ (define-type τ (variant (Cons τ_fld ...) ...)) : Unit
+ #:where
+ (Γ-extend [Cons : (τ_fld ... → τ)] ...)
+ (with (flds ...) (stx-map generate-temporaries #'((τ_fld ...) ...)))
+ #:expanded
+ (begin (struct Cons flds #:transparent) ...))
+
#;(define-syntax/type-rule #:keywords (variant)
[(define-type τ (variant (Cons τ_fld ...) ...))
#:where
@@ -101,6 +111,22 @@
(cdr (syntax->list #'(τ_result ...)))))
(⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
(car (syntax->list #'(τ_result ...))))]))
+(define-typed-syntax
+ (cases e_test [Cons (x ...) e_body ... e_result] ...) : τ_res
+ #:where
+; (e_body : Unit) ... ...
+ (let (τ ... → τ_Cons) := (typeof Cons)) ...
+ (when: (or (null? (syntax->list #'(τ_Cons ...)))
+ (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_Cons ...)))))
+ (cdr (syntax->list #'(τ_Cons ...))))))
+ (when: (assert-type #'e_test (stx-car #'(τ_Cons ...))))
+ (let τ_result := (typeof e_result)) ...
+ (when: (or (null? (syntax->list #'(τ_result ...)))
+ (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
+ (cdr (syntax->list #'(τ_result ...))))))
+ (with τ_res (stx-car #'(τ_result ...)))
+ #:expanded
+ (match e_test [(Cons x ...) e_body ... e_result] ...))
;; typed forms ----------------------------------------------------------------
#;(define-syntax (datum/tc stx)
