separate general type checking fns from stlc
This commit is contained in:
Stephen Chang
parent
857fee962f
commit
723c5bbaec
121
stlc.rkt
121
stlc.rkt
|
|
@ -2,9 +2,10 @@
|
|||
(require
|
||||
racket/match
|
||||
(for-syntax racket/base syntax/parse syntax/parse/experimental/template
|
||||
racket/set syntax/id-table syntax/stx racket/list racket/syntax
|
||||
racket/set syntax/stx racket/syntax
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse))
|
||||
(for-meta 2 racket/base syntax/parse)
|
||||
"typecheck.rkt")
|
||||
(provide
|
||||
(except-out
|
||||
(all-from-out racket/base)
|
||||
|
|
@ -28,39 +29,9 @@
|
|||
;; - user (recursive) function definitions
|
||||
;; - user (recursive) (variant) type-definitions
|
||||
|
||||
;; for types, just need the identifier bound
|
||||
(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
|
||||
(define base-type-env (hash))
|
||||
;; Γ : [Hashof var-symbol => type-stx]
|
||||
;; - can't use free-identifier=? for the hash table (or free-id-table)
|
||||
;; because env must be set before expanding λ body (ie before going under λ)
|
||||
;; so x's in the body won't be free-id=? to the one in the table
|
||||
;; use symbols instead of identifiers for now --- should be fine because
|
||||
;; I'm manually managing the environment
|
||||
(define Γ (make-parameter base-type-env))
|
||||
|
||||
;; generated type vars
|
||||
(define fvs (make-parameter (set)))
|
||||
(define fvs-subst (make-parameter (hash)))
|
||||
(define (fvs-subst-set x τ)
|
||||
(hash-set (fvs-subst) (syntax->datum x) τ))
|
||||
(define (do-subst/τ τ)
|
||||
(syntax-parse τ
|
||||
[x:id
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
|
||||
[τ:id #'τ]
|
||||
[(tycon τ ...)
|
||||
#:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
|
||||
#'(tycon τ-subst ...)]))
|
||||
(define (do-subst h)
|
||||
(for/hash ([(x τ) (in-hash h)])
|
||||
(values x (do-subst/τ τ)))))
|
||||
(define-and-provide-builtin-types Int String Bool → Listof Unit)
|
||||
(define-for-syntax (assert-Unit-type e) (assert-type e #'Unit))
|
||||
(define-for-syntax (assert-Int-type e) (assert-type e #'Int))
|
||||
|
||||
;; testing fns ----------------------------------------------------------------
|
||||
(require (for-syntax rackunit))
|
||||
|
|
@ -94,86 +65,6 @@
|
|||
(provide (rename-out [my-check-equal? check-equal?]))
|
||||
(define-syntax-rule (my-check-equal? x y) (check-equal? x y))
|
||||
|
||||
(define-for-syntax (type=? τ1 τ2)
|
||||
; (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
|
||||
(syntax-parse #`(#,τ1 #,τ2) #:literals (→)
|
||||
[(x:id τ)
|
||||
#:when (and (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-has-key? (fvs-subst) (syntax->datum #'x)))
|
||||
(type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
|
||||
[(x:id τ)
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
#:when (fvs-subst (fvs-subst-set #'x #'τ))
|
||||
#t]
|
||||
[(τ x:id)
|
||||
#:when (and (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-has-key? (fvs-subst) (syntax->datum #'x)))
|
||||
(type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
|
||||
[(τ x:id)
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
#:when (fvs-subst (fvs-subst-set #'x #'τ))
|
||||
#t]
|
||||
[(x:id y:id) (free-identifier=? τ1 τ2)]
|
||||
[((tycon1 τ1 ...) (tycon2 τ2 ...))
|
||||
(and (free-identifier=? #'tycon1 #'tycon2)
|
||||
(= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
|
||||
(stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
|
||||
[_ #f]))
|
||||
|
||||
;; return #t if (typeof e)=τ, else type error
|
||||
(begin-for-syntax
|
||||
(define (assert-type e τ)
|
||||
(or (type=? (typeof e) τ)
|
||||
(error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
|
||||
(syntax->datum e)
|
||||
(syntax-line e) (syntax-column e)
|
||||
(syntax->datum (typeof e))
|
||||
(syntax->datum τ))))
|
||||
(define (assert-Unit-type e) (assert-type e #'Unit))
|
||||
(define (assert-Int-type e) (assert-type e #'Int)))
|
||||
|
||||
;; type env and other helper fns ----------------------------------------------
|
||||
;; attaches type τ to e (as syntax property)
|
||||
(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
|
||||
|
||||
;; retrieves type of τ (from syntax property)
|
||||
(define-for-syntax (typeof stx) (syntax-property stx 'type))
|
||||
|
||||
(define-for-syntax (type-env-lookup x) (hash-ref (Γ) (syntax->datum x)))
|
||||
;; returns a new hash table extended with type associations x:τs
|
||||
(define-for-syntax (type-env-extend x:τs)
|
||||
(define xs (stx-map stx-car x:τs))
|
||||
(define τs (stx-map stx-cadr x:τs))
|
||||
(apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
|
||||
;; must be macro because type env must be extended first, before expandinb body
|
||||
(begin-for-syntax
|
||||
(define-syntax (with-extended-type-env stx)
|
||||
(syntax-parse stx
|
||||
[(_ x-τs e)
|
||||
#'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
|
||||
|
||||
;; expand/df ------------------------------------------------------------------
|
||||
;; depth-first expand
|
||||
(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
|
||||
;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
|
||||
;; ow forms like lambda and app won't get properly assigned types
|
||||
[else (local-expand e 'expression null ctx)]))
|
||||
(define-for-syntax (expand/df/module-ctx def)
|
||||
(local-expand def 'module #f))
|
||||
(define-for-syntax (expand/df/mb-ctx def)
|
||||
(local-expand def 'module-begin #f))
|
||||
|
||||
|
||||
|
||||
;; define-type ----------------------------------------------------------------
|
||||
(define-syntax (define-type stx)
|
||||
(syntax-parse stx #:datum-literals (variant)
|
||||
|
|
|
|||
120
typecheck.rkt
Normal file
120
typecheck.rkt
Normal file
|
|
@ -0,0 +1,120 @@
|
|||
#lang racket/base
|
||||
(require (for-syntax racket/base syntax/parse syntax/stx
|
||||
racket/set racket/list
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse))
|
||||
(provide (all-defined-out)
|
||||
(for-syntax (all-defined-out)))
|
||||
|
||||
;; for types, just need the identifier bound
|
||||
(define-syntax-rule (define-and-provide-builtin-type τ)
|
||||
(begin (define τ #f) (provide τ)))
|
||||
(define-syntax-rule (define-and-provide-builtin-types τ ...)
|
||||
(begin (define-and-provide-builtin-type τ) ...))
|
||||
|
||||
;; general type-checking functions
|
||||
|
||||
(define-for-syntax (type=? τ1 τ2)
|
||||
; (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
|
||||
(syntax-parse #`(#,τ1 #,τ2)
|
||||
[(x:id τ)
|
||||
#:when (and (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-has-key? (fvs-subst) (syntax->datum #'x)))
|
||||
(type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
|
||||
[(x:id τ)
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
#:when (fvs-subst (fvs-subst-set #'x #'τ))
|
||||
#t]
|
||||
[(τ x:id)
|
||||
#:when (and (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-has-key? (fvs-subst) (syntax->datum #'x)))
|
||||
(type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
|
||||
[(τ x:id)
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
#:when (fvs-subst (fvs-subst-set #'x #'τ))
|
||||
#t]
|
||||
[(x:id y:id) (free-identifier=? τ1 τ2)]
|
||||
[((tycon1 τ1 ...) (tycon2 τ2 ...))
|
||||
(and (free-identifier=? #'tycon1 #'tycon2)
|
||||
(= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
|
||||
(stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
|
||||
[_ #f]))
|
||||
|
||||
;; return #t if (typeof e)=τ, else type error
|
||||
(define-for-syntax (assert-type e τ)
|
||||
(or (type=? (typeof e) τ)
|
||||
(error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
|
||||
(syntax->datum e)
|
||||
(syntax-line e) (syntax-column e)
|
||||
(syntax->datum (typeof e))
|
||||
(syntax->datum τ))))
|
||||
|
||||
;; attaches type τ to e (as syntax property)
|
||||
(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
|
||||
|
||||
;; retrieves type of τ (from syntax property)
|
||||
(define-for-syntax (typeof stx) (syntax-property stx 'type))
|
||||
|
||||
;; type environment -----------------------------------------------------------
|
||||
(begin-for-syntax
|
||||
(define base-type-env (hash))
|
||||
;; Γ : [Hashof var-symbol => type-stx]
|
||||
;; - can't use free-identifier=? for the hash table (or free-id-table)
|
||||
;; because env must be set before expanding λ body (ie before going under λ)
|
||||
;; so x's in the body won't be free-id=? to the one in the table
|
||||
;; use symbols instead of identifiers for now --- should be fine because
|
||||
;; I'm manually managing the environment
|
||||
(define Γ (make-parameter base-type-env))
|
||||
|
||||
(define (type-env-lookup x) (hash-ref (Γ) (syntax->datum x)))
|
||||
|
||||
;; returns a new hash table extended with type associations x:τs
|
||||
(define (type-env-extend x:τs)
|
||||
(define xs (stx-map stx-car x:τs))
|
||||
(define τs (stx-map stx-cadr x:τs))
|
||||
(apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
|
||||
|
||||
;; must be macro because type env must be extended first, before expandinb body
|
||||
(define-syntax (with-extended-type-env stx)
|
||||
(syntax-parse stx
|
||||
[(_ x-τs e)
|
||||
#'(parameterize ([Γ (type-env-extend x-τs)]) e)]))
|
||||
|
||||
;; generated type vars
|
||||
(define fvs (make-parameter (set)))
|
||||
(define fvs-subst (make-parameter (hash)))
|
||||
(define (fvs-subst-set x τ)
|
||||
(hash-set (fvs-subst) (syntax->datum x) τ))
|
||||
(define (do-subst/τ τ)
|
||||
(syntax-parse τ
|
||||
[x:id
|
||||
#:when (set-member? (fvs) (syntax->datum #'x))
|
||||
(hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
|
||||
[τ:id #'τ]
|
||||
[(tycon τ ...)
|
||||
#:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
|
||||
#'(tycon τ-subst ...)]))
|
||||
(define (do-subst h)
|
||||
(for/hash ([(x τ) (in-hash h)])
|
||||
(values x (do-subst/τ τ)))))
|
||||
|
||||
;; expand/df ------------------------------------------------------------------
|
||||
;; depth-first expand
|
||||
(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
|
||||
;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
|
||||
;; ow forms like lambda and app won't get properly assigned types
|
||||
[else (local-expand e 'expression null ctx)]))
|
||||
(define-for-syntax (expand/df/module-ctx def)
|
||||
(local-expand def 'module #f))
|
||||
(define-for-syntax (expand/df/mb-ctx def)
|
||||
(local-expand def 'module-begin #f))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user