suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

stlc: non parametric maybe working; havent tried recursive types (ie cons)

Browse Source
This commit is contained in:
Stephen Chang 2014-08-12 17:58:56 -04:00
parent cb123987de
commit 3b9800919b
4 changed files with 150 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
stlc-tests.rkt
View File

@ -2,7 +2,7 @@
(check-type-error ((λ ([x : Int]) (+ x 1)) "10"))
(check-type ((λ ([x : Int]) (+ x 1)) 10) : Int)
(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11)
(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11) ; identifier used out of context
(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
; HO fn
@ -38,7 +38,7 @@
(check-type-error (null? {Int} "one"))
(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
;; begin and void
; begin and void
(check-type (void) : Unit)
(check-type-and-result (begin (void) 1) : Int => 1)
(check-type-and-result (begin (void) (void) 1) : Int => 1)
@ -52,7 +52,7 @@
(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a b c)) 1 2 3)
: Int => 6)
;; define
; define
(define (g [y : Int]) (+ (f y) 1))
(define (f [x : Int]) (+ x 1))
(check-type-and-result (f 10) : Int => 11)
@ -79,6 +79,25 @@
(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
: (Listof String))
;; recursive types
(define (a [x : Int]) (b x))
(define (b [x : Int]) (a x))
(define (ff [x : 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])
(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])))

146
stlc.rkt
View File

@ -1,5 +1,6 @@
#lang racket/base
(require
racket/match
(for-syntax racket/base syntax/parse syntax/parse/experimental/template
racket/set syntax/id-table syntax/stx racket/list racket/syntax
"stx-utils.rkt")
@ -13,11 +14,13 @@
))
(provide
define-type cases
(rename-out
[λ/tc λ] [app/tc #%app] [let/tc let] [letrec/tc letrec]
[begin/tc begin] [void/tc void]
[if/tc if] [+/tc +]
;[top/tc #%top] [define/tc define]
;[top/tc #%top]
;[define/tc define]
[datum/tc #%datum] [module-begin/tc #%module-begin]
[cons/tc cons] [null/tc null] [null?/tc null?] [first/tc first] [rest/tc rest]))
@ -25,9 +28,9 @@
;; - type of top level (or module level) vars not checked
;; for types, just need the identifier bound
(define-syntax-rule (define-type τ) (begin (define τ #f) (provide τ)))
(define-syntax-rule (define-types τ ...) (begin (define-type τ) ...))
(define-types Int String Bool → Listof Unit)
(define-syntax-rule (define-builtin-type τ) (begin (define τ #f) (provide τ)))
(define-syntax-rule (define-builtin-types τ ...) (begin (define-builtin-type τ) ...))
(define-builtin-types Int String Bool → Listof Unit)
;; type environment
(begin-for-syntax
@ -56,7 +59,10 @@
#'(tycon τ-subst ...)]))
(define (do-subst h)
(for/hash ([(x τ) (in-hash h)])
(values x (do-subst/τ τ)))))
(values x (do-subst/τ τ))))
;; internal definition context
(define intdef-ctx (make-parameter (syntax-local-make-definition-context))))
;; testing fns ----------------------------------------------------------------
(require (for-syntax rackunit))
@ -69,7 +75,7 @@
(define-syntax (check-type stx)
(syntax-parse stx #:datum-literals (:)
[(_ e : τ)
#:with e+ (local-expand #'e 'expression null)
#:with e+ (expand/df #'e)
#:when (check-true (assert-type #'e+ #'τ)
(format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
#'(void)]))
@ -119,6 +125,7 @@
(begin-for-syntax
(define (assert-type e τ)
(or (type=? (typeof e) τ)
; (let ([e (local-expand e 'expression null)])
(error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
(syntax->datum e)
(syntax-line e) (syntax-column e)
@ -147,17 +154,56 @@
[(_ x-τs e)
#'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
;; expand/df ------------------------------------------------------------------
;; depth-first expand
(define-for-syntax (expand/df e)
(if (identifier? e)
(⊢ e (type-env-lookup e)) ; handle this here bc there's no #%var form
(local-expand e 'expression null)))
(define-for-syntax (expand/df e [ctx #f])
; (printf "expanding: ~a\n" e)
; (printf "typeenv: ~a\n" (Γ))
(cond
;; 1st case handles struct constructors that are not the same name as struct
;; (should always be an identifier)
[(syntax-property e 'constructor-for) => (λ (Cons)
(⊢ e (type-env-lookup Cons)))]
;; 2nd case handles identifiers that are not struct constructors
[(identifier? e) (⊢ e (type-env-lookup e))] ; handle this here bc there's no #%var form
[else (local-expand e 'expression null ctx)]))
(define-for-syntax (expand/df/module-ctx def)
(local-expand def 'module null))
(local-expand def 'module #f))
(define-for-syntax (expand/df/mb-ctx def)
(local-expand def 'module-begin null))
(local-expand def 'module-begin #f))
;; define-type ----------------------------------------------------------------
(define-syntax (define-type stx)
(syntax-parse stx #:datum-literals (variant)
[(_ τ:id (variant (Cons:id τ_fld ...) ...))
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
#:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)] ...)))
#'(begin
(struct Cons (x ...)) ...)]))
(define-syntax (cases stx)
(syntax-parse stx
[(_ e [Cons (x ...) body ... body_result] ...)
#:with e+ (expand/df #'e)
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
#:with ((→ τ ... τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
#:with ((lam xs+ body+ ... body_result+) ...)
(stx-map (λ (bods xs τs)
(with-extended-type-env
(stx-map list xs τs)
(expand/df #`(λ #,xs #,@bods))))
#'((body ... body_result) ...)
#'((x ...) ...)
#'((τ ...) ...))
#:when (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((body+ ...) ...))
#:with (τ_result ...) (stx-map typeof #'(body_result+ ...))
#:when (or (null? (syntax->list #'(τ_result ...)))
(andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
(cdr (syntax->list #'(τ_result ...)))))
#'(match e+ [(Cons+ x ...) body+ ... body_result+] ...)]))
;; typed forms ----------------------------------------------------------------
(define-syntax (datum/tc stx)
(syntax-parse stx
@ -232,6 +278,7 @@
#:datum-literals (:t)
[(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
[(_ e_fn e_arg ...)
; #:when (printf "app: ~a\n" (syntax->datum #'e_fn))
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
#:with (→ τ ... τ_res) (typeof #'e_fn+)
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
@ -303,35 +350,90 @@
(syntax/loc stx (#%top . x+))]))
(begin-for-syntax
(define-syntax-class maybe-def #:datum-literals (: define)
(define-syntax-class maybe-def #:datum-literals (: define variant) #:literals (define-type)
(pattern (define (f:id [x:id : τx] ...) body ...)
#:with τ_result (generate-temporary #'f)
#:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
#:attr name #'(f)
#:attr val #'((λ/tc ([x : τx] ...) body ...))
#:attr τ #'((→ τx ... τ_result))
#:attr e #'())
; (pattern (define x:id exp:expr)
; #:attr name #'(x)
; #:attr val #'(exp)
; #:attr τ ???
#:attr e #'() #:attr tydecl #'() #:attr names #'())
(pattern (define-type TypeName (variant (Cons fieldτ ...) ...))
#:attr name #'() #:attr τ #'() #:attr val #'() #:attr e #'()
#:attr tydecl #'((define-type TypeName (variant (Cons fieldτ ...) ...)))
#:attr names #'((Cons ...)))
(pattern exp:expr
#:attr name #'() #:attr τ #'() #:attr val #'()
#:attr e #'(exp))))
#:attr name #'() #:attr τ #'() #:attr val #'() #:attr tydecl #'() #:attr names #'()
#: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 ...) mk-strct-type-def)
#:attr lhs #'(x ...)
#:attr rhs #'mk-strct-type-def))
(define-syntax-class def-syn #:literals (define-syntaxes)
(pattern
(define-syntaxes (x) strct-info-def)
#:attr lhs #'x
#:attr rhs #'strct-info-def))
)
(define-for-syntax (add-struct-to-ctx strct ctx)
(syntax-parse strct #:literals (begin define-values define-syntaxes)
[(begin
(define-values (x ...) mk-strct-type-def)
(define-syntaxes (y) strct-info-def))
#:when (printf "~a\n" #'y)
(begin
(syntax-local-bind-syntaxes (list #'y) #'strct-info-def ctx)
#;(syntax-local-bind-syntaxes (syntax->list #'(x ...)) #f ctx))]))
(define-syntax (module-begin/tc stx)
(syntax-parse stx
(syntax-parse stx #:literals (begin)
[(_ mb-form:maybe-def ...)
#: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 (f ...) (template ((?@ . mb-form.name) ...))
#:with (v ...) (template ((?@ . mb-form.val) ...))
#:with (τ ...) (template ((?@ . mb-form.τ) ...))
#:with (e ...) (template ((?@ . mb-form.e) ...))
#:with (def-val:def-val ...) #'(structdef+.def-val ...)
#:with (def-val-lhs ...) #'(def-val.lhs ...)
#;(stx-map
(λ (xs) (stx-map
(λ (x) (printf "~a" x)(format-id (car (syntax->list #'(f ...))) "~a" x))
xs))
#'(def-val.lhs ...))
#:with (def-val-rhs ...) #'(def-val.rhs ...)
#:when (printf "lhs: ~a\n" #'(def-val-lhs ...))
#:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
#:with (def-syn-lhs ...) #'(def-syn.lhs ...)
#:with (def-syn-rhs ...) #'(def-syn.rhs ...)
#:when (Γ (type-env-extend #'([f τ] ...)))
#:when (intdef-ctx (syntax-local-make-definition-context))
#:when (stx-map (λ (strct) (add-struct-to-ctx strct (intdef-ctx))) #'(structdef+ ...))
; #:when (syntax-local-bind-syntaxes (syntax->list #'(Cons ...)) #f (intdef-ctx))
; #:when (syntax-local-bind-syntaxes (syntax->list #'(Cons ...)) null (intdef-ctx))
; #:with letrec+ (expand/df #'(letrec/tc ([f : τ v] ...) e ... (void)) (intdef-ctx))
#:when (printf "fvs :~a\n" (fvs))
; #:when (printf "mb: ~a\n" (syntax->datum (expand/df #'(letrec ([f v] ...) e ...))))
;; error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
;; cause: for struct def, define-values must come before define-syntaxes
(quasisyntax/loc stx
(#%module-begin
#,(expand/df #'(letrec/tc ([f : τ v] ...) e ... (void)))
; structdef+ ...
#,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
(let-syntax ([def-syn-lhs def-syn-rhs] ...)
(letrec/tc ([f : τ v] ...) e ... (void))
)));(intdef-ctx)))
(define #,(datum->syntax stx 'runtime-env)
(for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
(hash->list (do-subst (Γ))))])

5
stx-utils.rkt
View File

@ -3,4 +3,7 @@
(provide (all-defined-out))
(define (stx-cadr stx) (car (stx-cdr stx)))
(define (stx-andmap f . stx-lsts) (apply andmap f (map syntax->list stx-lsts)))
(define (stx-andmap f . stx-lsts)
(apply andmap f (map syntax->list stx-lsts)))
(define (stx-flatten stxs)
(apply append (stx-map syntax->list stxs)))

5
sysf.rkt
View File

@ -234,11 +234,6 @@
(syntax-parse stx #:literals (→ void)
#:datum-literals (:t)
[(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
[(_ void) #'(printf "ddd")]
; [(_ check-type e ...) #'(check-type e ...)]
; [(_ check-type-and-result e ...) #'(check-type e ...)]
; [(_ check-type e ...) #'(check-type e ...)]
; [(_ check-type e ...) #'(check-type e ...)]
[(_ e_fn e_arg ...)
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
#:with (→ τ ... τ_res) (typeof #'e_fn+)