From 95aaf627b58eb73cb785fda7988891a31f9d704d Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 27 May 2015 16:07:39 -0400 Subject: [PATCH] add stlc+sub --- tapl/README.md | 2 +- tapl/stlc+sub.rkt | 85 +++++++++++++++++++++------- tapl/tests/rackunit-typechecking.rkt | 9 ++- tapl/tests/stlc+sub-tests.rkt | 44 +++++++++++++- 4 files changed, 115 insertions(+), 25 deletions(-) diff --git a/tapl/README.md b/tapl/README.md index 35bbf1a..d2e6588 100644 --- a/tapl/README.md +++ b/tapl/README.md @@ -9,4 +9,4 @@ A file extends its immediate parent file. - stlc+var.rkt - stlc+cons.rkt - stlc+box.rkt - - stlc+sub.rkt \ No newline at end of file + - stlc+sub.rkt \ No newline at end of file diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt index 4f319a6..18bbac7 100644 --- a/tapl/stlc+sub.rkt +++ b/tapl/stlc+sub.rkt @@ -1,35 +1,80 @@ #lang racket/base (require - (for-syntax racket/base syntax/parse) + (for-syntax racket/base syntax/parse racket/string "stx-utils.rkt") "typecheck.rkt") -(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ)) - (except-in "stlc.rkt" #%app λ) - (prefix-in lit: (only-in "stlc+lit.rkt" Int)) - (except-in "stlc+lit.rkt" Int)) -(provide (rename-out [stlc:#%app #%app] - [stlc:λ λ])) -(provide (all-from-out "stlc.rkt") - (all-from-out "stlc+lit.rkt")) -(provide Int) +(require (except-in "stlc+lit.rkt" #%app #%datum +) + (prefix-in stlc: (only-in "stlc+lit.rkt" #%datum))) +(provide (rename-out [app/tc #%app] [datum/tc #%datum])) +(provide (all-from-out "stlc+lit.rkt")) +(provide (for-syntax sub?)) ;; can't write any terms with no base types ;; Simply-Typed Lambda Calculus, plus subtyping ;; Types: ;; - types from stlc.rkt and stlc+lit.rkt +;; - Top, Num, Nat +;; Type relations: +;; - sub? +;; - Any <: Top +;; - Nat <: Int +;; - Int <: Num +;; - → ;; Terms: -;; - terms from stlc.rkt, stlc+lit.rkt +;; - terms from stlc.rkt, stlc+lit.rkt, except redefined: app and datum + +(define-base-type Top) +(define-base-type Num) +(define-base-type Nat) +;; TODO: implement define-subtype +;(define-subtype Int <: Num) +;(define-subtype Nat <: Int) + +(define-syntax (datum/tc stx) + (syntax-parse stx + [(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)] + [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)] + [(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)] + [(_ . x) #'(stlc:#%datum . x)])) + +(define-primop + : (→ Num Num Num)) (begin-for-syntax - (define (<: τ1 τ2) - (syntax-property τ1 'super τ2)) (define (sub? τ1 τ2) (or (type=? τ1 τ2) - (syntax-parse (list τ1 τ2) #:literals (→) - [((→ s1 s2) (→ t1 t2)) - (and (sub? #'t1 #'s1) - (sub? #'s1 #'t2))])))) - -(define-base-type Num) -(define-syntax Int (make-rename-transformer (⊢ #'lit:Int #'Num))) + (type=? #'Top τ2) + (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num) + [(Nat τ) (sub? #'Int #'τ)] + [(Int τ) (sub? #'Num #'τ)] + [(τ Num) (sub? #'τ #'Int)] + [(τ Int) (sub? #'τ #'Nat)] + [((→ s1 s2) (→ t1 t2)) + (and (sub? #'t1 #'s1) + (sub? #'s2 #'t2))] + [_ #f]))) + (define (subs? τs1 τs2) (stx-andmap sub? τs1 τs2))) + ;(define (subs? ts1 ts2) (stx-andmap (λ (t1 t2) (printf "~a <: ~a: ~a\n" (syntax->datum t1) (syntax->datum t2) (sub? t1 t2)) (sub? t1 t2)) ts1 ts2))) +(define-syntax (app/tc stx) + (syntax-parse stx #:literals (→) + [(_ e_fn e_arg ...) + #:with (e_fn- τ_fn) (infer+erase #'e_fn) + #:fail-unless (→? #'τ_fn) + (format "Type error: Attempting to apply a non-function ~a with type ~a\n" + (syntax->datum #'e_fn) (syntax->datum #'τ_fn)) + #:with (→ τ ... τ_res) #'τ_fn + #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) +; #:fail-unless (types=? #'(τ ...) #'(τ_arg ...)) + #:fail-unless (subs? #'(τ_arg ...) #'(τ ...)) + (string-append + (format + "Wrong number of args given to function ~a, or args have wrong type:\ngiven: " + (syntax->datum #'e_fn)) + (string-join + (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...))) + ", ") + "\nexpected arguments with type: " + (string-join + (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...))) + ", ")) + (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)])) diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index e7a6bce..9e84b5b 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -12,7 +12,9 @@ #:with e+ (expand/df #'e) #:with τ (typeof #'e+) #:fail-unless - (type=? #'τ #'τ-expected) + ;; use subtyping if it's bound in the context of #'e + (with-handlers ([exn:fail? (λ _ (type=? #'τ #'τ-expected))]) + ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected)) (format "Expression ~a [loc ~a:~a] has type ~a, expected ~a" (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e) @@ -26,7 +28,8 @@ #:with e+ (expand/df #'e) #:with τ (typeof #'e+) #:fail-when - (type=? #'τ #'not-τ) + (with-handlers ([exn:fail? (λ _ (type=? #'τ #'τ-not))]) + ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-not)) (format "(~a:~a) Expression ~a should not have type ~a" (syntax-line stx) (syntax-column stx) @@ -49,4 +52,4 @@ [(_ e : τ ⇒ v) #'(begin (check-type e : τ) - (check-equal? e v))])) \ No newline at end of file + (check-equal? e v))])) diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt index 26d129c..19fc3b1 100644 --- a/tapl/tests/stlc+sub-tests.rkt +++ b/tapl/tests/stlc+sub-tests.rkt @@ -1,4 +1,46 @@ #lang s-exp "../stlc+sub.rkt" (require "rackunit-typechecking.rkt") -;; cannot have tests without base types \ No newline at end of file +;; subtyping tests +(check-type 1 : Top) +(check-type 1 : Num) +(check-type 1 : Int) +(check-type 1 : Nat) +(check-type -1 : Top) +(check-type -1 : Num) +(check-type -1 : Int) +(check-not-type -1 : Nat) +(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1) +(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1) +(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) +(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) +(typecheck-fail ((λ ([x : Nat]) x) -1)) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output +(check-not-type (λ ([x : Int]) x) : (→ Int Nat)) +(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input +(check-not-type (λ ([x : Int]) x) : (→ Num Int)) + +;; previous tests ------------------------------------------------------------- +;; some change due to more specific types +(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) +;; changed test +(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)