From 5c058bffd600475db357596202a9b0e98bbb5740 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 27 May 2015 19:25:50 -0400 Subject: [PATCH] start sysf --- tapl/README.md | 3 ++- tapl/stx-utils.rkt | 4 +++- tapl/sysf.rkt | 31 +++++++++++++++++++++++++++++++ tapl/tests/sysf-tests.rkt | 25 +++++++++++++++++++++++++ tapl/typecheck.rkt | 36 +++++++++++++++++++++++++++++------- 5 files changed, 90 insertions(+), 9 deletions(-) create mode 100644 tapl/sysf.rkt create mode 100644 tapl/tests/sysf-tests.rkt diff --git a/tapl/README.md b/tapl/README.md index 27c641d..6c26097 100644 --- a/tapl/README.md +++ b/tapl/README.md @@ -10,4 +10,5 @@ A file extends its immediate parent file. - stlc+cons.rkt - stlc+box.rkt - stlc+sub.rkt - - stlc+rec+var+sub.rkt \ No newline at end of file + - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt) + - sysf.rkt \ No newline at end of file diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt index f01d0f5..69569e5 100644 --- a/tapl/stx-utils.rkt +++ b/tapl/stx-utils.rkt @@ -31,4 +31,6 @@ (string=? (syntax-e s1) (syntax-e s2))) (define (stx-sort stx cmp) - (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2)))))) \ No newline at end of file + (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2)))))) +(define (stx-fold f base . lsts) + (apply foldl f base (map syntax->list lsts))) \ No newline at end of file diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt new file mode 100644 index 0000000..44d822b --- /dev/null +++ b/tapl/sysf.rkt @@ -0,0 +1,31 @@ +#lang racket/base +(require + (for-syntax racket/base syntax/parse) +; (for-meta 2 racket/base) + "typecheck.rkt") +(require (except-in "stlc+lit.rkt" λ #%app) + (prefix-in stlc: (only-in "stlc+lit.rkt" λ #%app))) +(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) +(provide (except-out (all-from-out "stlc+lit.rkt") stlc:λ stlc:#%app)) +(provide Λ inst) + + +;; System F +;; Types: +;; - types from stlc+lit.rkt +;; Terms: +;; - terms from stlc+lit.rkt + +(define-type-constructor ∀) + +(define-syntax (Λ stx) + (syntax-parse stx + [(_ (tv:id ...) e) + #:with (tvs+ e- τ) (infer/tvs+erase #'e #'(tv ...)) + (⊢ #'e- #'(∀ tvs+ τ))])) +(define-syntax (inst stx) + (syntax-parse stx + [(_ e τ ...) + #:with (e- τ_e) (infer+erase #'e) + #:with ((~literal ∀) (tv ...) τ_body) #'τ_e + (⊢ #'e- (substs #'(τ ...) #'(tv ...) #'τ_body))])) \ No newline at end of file diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt new file mode 100644 index 0000000..3c696df --- /dev/null +++ b/tapl/tests/sysf-tests.rkt @@ -0,0 +1,25 @@ +#lang s-exp "../sysf.rkt" +(require "rackunit-typechecking.rkt") + +(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int)) + +;; previous tests ------------------------------------------------------------- +(check-type 1 : Int) +(check-not-type 1 : (→ Int Int)) +(typecheck-fail "one") ; unsupported literal +(typecheck-fail #f) ; unsupported literal +(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) +(check-not-type (λ ([x : Int]) x) : Int) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) +(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) +(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type +(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type +(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + : (→ (→ Int Int Int) Int Int Int)) +(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) +(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int +(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int +(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 3e36616..b022267 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -124,9 +124,18 @@ (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))] [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)])) - (define (infer+erase e) - (define e+ (expand/df e)) - (list e+ (eval-τ (typeof e+)))) + (define (infer+erase e [tvs #'()]) + (define e+ + (syntax-parse (expand/df #`(λ #,tvs #,e)) #:literals (#%expression) + [(lam tvs+ (#%expression e+)) #'e+] + [(lam tvs+ e+) #'e+])) + (list e+ (eval-τ (typeof e+) tvs))) + (define (infer/tvs+erase e [tvs #'()]) + (define-values (tvs+ e+) + (syntax-parse (expand/df #`(λ #,tvs #,e)) #:literals (#%expression) + [(lam tvs+ (#%expression e+)) (values #'tvs+ #'e+)] + [(lam tvs+ e+) (values #'tvs+ #'e+)])) + (list tvs+ e+ (eval-τ (typeof e+) tvs))) (define (infers+erase es) (stx-map infer+erase es)) (define (types=? τs1 τs2) @@ -155,7 +164,9 @@ #;(define (assert-types es τs) (stx-andmap assert-type es τs)) - (define (eval-τ τ) + (define (eval-τ τ [tvs #'()]) + (if (and (identifier? τ) (stx-member τ tvs)) + τ (syntax-parse τ [s:str τ] ; record field [_ @@ -169,8 +180,8 @@ maybe-app-τ (syntax-parse maybe-app-τ [(τ ...) - #:with (τ-exp ...) (stx-map eval-τ #'(τ ...)) - #'(τ-exp ...)]))])) + #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ ...)) + #'(τ-exp ...)]))]))) ;; type=? : Type Type -> Boolean ;; Indicates whether two types are equal @@ -267,7 +278,18 @@ (define-for-syntax (mk-pred x) (format-id x "~a?" x)) (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field)) - +(define-for-syntax (subst τ x e) + (syntax-parse e + [y:id + #:when (free-identifier=? e x) + τ] + [y:id #'y] + [(esub ...) + #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...)) + #'(esub_subst ...)])) +(define-for-syntax (substs τs xs e) + (stx-fold subst e τs xs)) + ;; type environment ----------------------------------------------------------- #;(begin-for-syntax