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

macrotypes/mlish and macrotypes/mlish+adhoc tests passing

Browse Source
This commit is contained in:
Stephen Chang 2017-01-31 14:30:46 -05:00
parent 03b6d6e713
commit a788c4a7d5
12 changed files with 20 additions and 246 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
macrotypes/examples/fomega3.rkt
View File

@ -1,32 +0,0 @@
#lang s-exp macrotypes/typecheck
(extends "fomega.rkt" #:except tyapp tyλ)
; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
; → is both type and kind --- but reuses parts of fomega.rkt,
; ie removes the duplication in fomega2.rkt
;; System F_omega
;; Type relation:
;; - redefine current-kind? and current-type so #%app and λ
;; work for both terms and types
;; Types:
;; - types from fomega.rkt
;; - String from stlc+reco+var
;; Terms:
;; - extend ∀ Λ inst from fomega.rkt
;; - #%datum from stlc+reco+var
;; types and kinds are now mixed, due to #%app and λ
(begin-for-syntax
(define old-kind? (current-kind?))
(current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k)))))
;; Try to keep "type?" backward compatible with its uses so far,
;; eg in the definition of λ or previous type constuctors.
;; (However, this is not completely possible, eg define-type-alias)
;; So now "type?" no longer validates types, rather it's a subset.
;; But we no longer need type? to validate types, instead we can use
;; (kind? (typeof t))
(current-type? (λ (t) (or (type? t)
(let ([k (typeof t)])
(or (★? k) (∀★? k)))
((current-kind?) t)))))

2
macrotypes/examples/fsub.rkt
View File

@ -26,7 +26,7 @@
(begin-for-syntax
(define (expose t)
(cond [(identifier? t)
(define sub (typeof t #:tag '<:))
(define sub (detach t '<:))
(if sub (expose sub) t)]
[else t]))
(current-promote expose)

4
macrotypes/examples/mlish+adhoc.rkt
View File

@ -383,7 +383,7 @@
(format "Improper use of constructor ~a; expected ~a args, got ~a"
(syntax->datum #'Name) (stx-length #'(X ...))
(stx-length (stx-cdr #'stx))))])]
[X (make-rename-transformer (⊢ X #%type))] ...)
[X (make-rename-transformer (⊢ X :: #%type))] ...)
(void ty_flat ...)))))
#:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
(stx-map
@ -854,7 +854,7 @@
(expand/df
#'(lambda (X ...)
(let-syntax
([X (make-rename-transformer (assign-type #'X #'#%type))] ...)
([X (make-rename-transformer (mk-type #'X))] ...)
(let-syntax
;; must have this inner macro bc body of lambda may require
;; ops defined by TC to be bound

2
macrotypes/examples/mlish.rkt
View File

@ -447,7 +447,7 @@
(format "Improper use of constructor ~a; expected ~a args, got ~a"
(syntax->datum #'Name) (stx-length #'(X ...))
(stx-length (stx-cdr #'stx))))])]
[X (make-rename-transformer (⊢ X #%type))] ...)
[X (make-rename-transformer (⊢ X :: #%type))] ...)
(void ty_flat ...)))))
#:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
(stx-map

2
macrotypes/examples/tests/ext-stlc-tests.rkt
View File

@ -53,7 +53,7 @@
(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
(typecheck-fail (ann Bool : Int)
#:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool")
#:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)

200
macrotypes/examples/tests/fomega3-tests.rkt
View File

@ -1,200 +0,0 @@
#lang s-exp "../fomega3.rkt"
(require "rackunit-typechecking.rkt")
(check-type Int : ★)
(check-type String : ★)
(typecheck-fail →)
(check-type (→ Int Int) : ★)
(typecheck-fail (→ →))
(typecheck-fail (→ 1))
(check-type 1 : Int)
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
: (∀ ([X : ★]) (→ X X)))
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
(check-type (λ ([t : ★]) t) : (→ ★ ★))
(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
(check-type ((λ ([t : ★]) t) Int) : ★)
(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
;; partial-apply →
(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
: (→ ★ ★))
; f's type must have kind ★
(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
(∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
(check-type (inst
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
: (→ (→ Int String) (→ Int String)))
(typecheck-fail
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
;#:with-msg "not a valid type: 1")
;; applied f too early
(typecheck-fail (inst
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
(check-type ((inst
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
(λ ([x : Int]) "int")) : (→ Int String))
(check-type (((inst
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
;; tapl examples, p441
(typecheck-fail
(define-type-alias tmp 1))
;#:with-msg "not a valid type: 1")
(define-type-alias Id (λ ([X : ★]) X))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
;; tapl examples, p451
(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
;(check-type Pair : (→ ★ ★ ★))
(check-type Pair : (→ ★ ★ (∀★ ★)))
(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
; parametric pair constructor
(check-type
(Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
: (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
; concrete Pair Int String constructor
(check-type
(inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String)
: (→ Int String (Pair Int String)))
; Pair Int String value
(check-type
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1")
: (Pair Int String))
; fst: parametric
(check-type
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
: (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X)))
; fst: concrete Pair Int String accessor
(check-type
(inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
: (→ (Pair Int String) Int))
; apply fst
(check-type
((inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1"))
: Int ⇒ 1)
; snd
(check-type
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
: (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y)))
(check-type
(inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
: (→ (Pair Int String) String))
(check-type
((inst
(Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
Int String) 1 "1"))
: String ⇒ "1")
;;; sysf tests wont work, unless augmented with kinds
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
: (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
; first inst should be discarded
(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
; second inst is discarded
(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
;; polymorphic arguments
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
(check-type
(inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
(check-type
((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
: Int ⇒ 10)
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
(Λ ([s : ★]) (λ ([y : s]) y)))
: Int ⇒ 10)
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
;(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)

6
macrotypes/examples/tests/general-tests.rkt
View File

@ -15,9 +15,9 @@
(define-type-constructor -> #:arity > 0)
(define-binding-type mu #:arity = 1 #:bvs = 1)
(define-binding-type forall #:bvs = 1 #:arity = 1)
(define-binding-type exist #:no-attach-kind #:bvs = 1 #:arity = 1)
(define-binding-type exist2 #:bvs = 1 #:arity = 1 #:no-attach-kind)
(define-binding-type exist3 #:bvs = 1 #:no-attach-kind #:arity = 1)
(define-binding-type exist #:extra-info void #:bvs = 1 #:arity = 1)
(define-binding-type exist2 #:bvs = 1 #:arity = 1 #:extra-info void)
(define-binding-type exist3 #:bvs = 1 #:extra-info void #:arity = 1)
(check-stx-err
(define-binding-type exist4 #:bvs = 1 #:no-attach- #:arity = 1)

2
macrotypes/examples/tests/infer-tests.rkt
View File

@ -246,7 +246,7 @@
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given #f\n *expression: Bool")
(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Bool")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)

4
macrotypes/examples/tests/mlish-tests.rkt
View File

@ -64,6 +64,8 @@
(check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
(check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil)
(check-type (λ ([x : (List Int)]) x) : (→/test (List Int) (List Int)))
(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
@ -675,7 +677,7 @@
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)

8
macrotypes/typecheck.rkt
View File

@ -194,7 +194,8 @@
;; If Val is a non-empty list, return first element, otherwise return Val.
(define (get-stx-prop/car stx tag)
(define v (syntax-property stx tag))
(if (cons? v) (car v) v))
(let L ([v v])
(if (cons? v) (L (car v)) v)))
;; A Tag is a Symbol serving as a stx prop key for some kind of metadata.
;; e.g., ': for types, ':: for kinds, etc.
@ -408,6 +409,7 @@
(combine-out . ts) (combine-out . t-s)
(for-syntax (combine-out . t-expanders) . t?s)))
modes)]))))
;; base types --------------------------------------------------------
(define-syntax define-base-type
(syntax-parser
[(_ (~var τ id)) ; default to 'key2 and #%tag
@ -448,6 +450,7 @@
(syntax-parser
[(_ (~var x id) (... ...))
#'(begin (define-base-type x) (... ...))]))
;; type constructors -------------------------------------------------
(define-syntax define-internal-type-constructor
(syntax-parser
; [(_ (~var x id) . rst)
@ -899,7 +902,8 @@
(define (typecheck-fail-msg/1 τ_expected τ_given expression)
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
(type->str τ_expected)
(type->str τ_given)
(or (and (syntax-e τ_given) (type->str τ_given))
"an invalid expression")
(syntax->datum (get-orig expression))))
;; typecheck-fail-msg/1/no-expr : Type Type Stx -> String

2
turnstile/examples/fsub.rkt
View File

@ -26,7 +26,7 @@
(begin-for-syntax
(define (expose t)
(cond [(identifier? t)
(define sub (typeof t #:tag '<:))
(define sub (detach t '<:))
(if sub (expose sub) t)]
[else t]))
(current-promote expose)

2
turnstile/examples/tests/ext-stlc-tests.rkt
View File

@ -53,7 +53,7 @@
(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
(typecheck-fail (ann Bool : Int)
#:with-msg "ann: type mismatch: expected Int, given #f\n *expression: Bool")
#:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)