From 3b9800919b1ceee446e12237483394e748a19c05 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 12 Aug 2014 17:58:56 -0400 Subject: [PATCH] stlc: non parametric maybe working; havent tried recursive types (ie cons) --- stlc-tests.rkt | 25 ++++++++- stlc.rkt | 146 +++++++++++++++++++++++++++++++++++++++++-------- stx-utils.rkt | 5 +- sysf.rkt | 5 -- 4 files changed, 150 insertions(+), 31 deletions(-) diff --git a/stlc-tests.rkt b/stlc-tests.rkt index c5e6274..d6008be 100644 --- a/stlc-tests.rkt +++ b/stlc-tests.rkt @@ -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]))) \ No newline at end of file diff --git a/stlc.rkt b/stlc.rkt index 963cfc1..068a4e3 100644 --- a/stlc.rkt +++ b/stlc.rkt @@ -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 (Γ))))]) diff --git a/stx-utils.rkt b/stx-utils.rkt index d3b0d90..699700e 100644 --- a/stx-utils.rkt +++ b/stx-utils.rkt @@ -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))) \ No newline at end of file +(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))) \ No newline at end of file diff --git a/sysf.rkt b/sysf.rkt index f8f5fd6..c436bd2 100644 --- a/sysf.rkt +++ b/sysf.rkt @@ -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+)