commit d1814cb57acb142c2cd63c1b53cf95eba89b06d1
parent 0255003ff7184116d3a25a5664061ea4eed0910f
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 28 Aug 2015 16:57:38 -0400
code cleanup; add define-sub-relation
- all tests passing
Diffstat:
15 files changed, 236 insertions(+), 1309 deletions(-)
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -1,11 +1,10 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
+(require (except-in "stlc+reco+var.rkt" #%app λ let)
(prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let))
- (only-in "stlc+rec-iso.rkt" type=?))
+ (only-in "stlc+rec-iso.rkt")) ; to get current-type=?
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let)
- (all-from-out "stlc+rec-iso.rkt"))
+(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let))
(provide ∃ pack open)
;; existential types
@@ -76,5 +75,7 @@
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
;;
#:with [_ (x-) (e-) (τ_e)]
- (infer #'(e) #:tvctx #'([tv : #%type]) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
+ (infer #'(e)
+ #:tvctx #'([tv : #%type])
+ #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
(⊢ (let ([x- e_packed-]) e-) : τ_e)]))
\ No newline at end of file
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -47,37 +47,24 @@
(define-syntax (and/tc stx)
(syntax-parse stx
[(_ e1 e2)
-; #:with e1- (inferBool+erase #'e1)
-; #:with e2- (inferBool+erase #'e2)
#:with e1- (⇑ e1 as Bool)
#:with e2- (⇑ e2 as Bool)
-; #:with (e1- τ1) (infer+erase #'e1)
-; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
-; #:with (e2- τ2) (infer+erase #'e2)
-; #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2))
(⊢ (and e1- e2-) : Bool)]))
(define-syntax (or/tc stx)
(syntax-parse stx
[(_ e1 e2)
-; #:with e1- (inferBool+erase #'e1)
-; #:with e2- (inferBool+erase #'e2)
#:with e1- (⇑ e1 as Bool)
#:with e2- (⇑ e2 as Bool)
-; #:with (e1- τ1) (infer+erase #'e1)
-; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
-; #:with (e2- τ2) (infer+erase #'e2)
-; #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2))
(⊢ (or e1- e2-) : Bool)]))
(define-syntax (if/tc stx)
(syntax-parse stx
[(_ e_tst e1 e2)
#:with e_tst- (⇑ e_tst as Bool)
-; #:with (e_tst- τ_tst) (infer+erase #'e_tst)
-; #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
#:with (e1- τ1) (infer+erase #'e1)
#:with (e2- τ2) (infer+erase #'e2)
+ ; double check because typing relation may not be reflexive
#:fail-unless (or (typecheck? #'τ1 #'τ2)
(typecheck? #'τ2 #'τ1))
(format "branches must have the same type: given ~a and ~a"
@@ -90,18 +77,7 @@
(define-syntax (begin/tc stx)
(syntax-parse stx
[(_ e_unit ... e)
- ;#:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
#:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
-; #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
-; #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
-; (string-append
-; "all begin expressions except the last one should have type Unit\n"
-; (string-join
-; (stx-map
-; (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
-; #'(e_unit ...) #'(τ_unit ...))
-; "\n")
-; "\n")
#:with (e- τ) (infer+erase #'e)
(⊢ (begin e_unit- ... e-) : τ)]))
@@ -118,7 +94,7 @@
(syntax-parse stx
[(_ ([x e] ...) e_body)
#:with ((e- τ) ...) (infers+erase #'(e ...))
- #:with ((x- ...) e_body- τ_body) (infer/type-ctxt+erase #'([x τ] ...) #'e_body)
+ #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'e_body)
(⊢ (let ([x- e-] ...) e_body-) : τ_body)]))
(define-syntax (let*/tc stx)
@@ -131,7 +107,7 @@
(syntax-parse stx
[(_ ([b:type-bind e] ...) e_body)
#:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
- (infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
+ (infers/ctx+erase #'(b ...) #'(e ... e_body))
#:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
(string-append
"type check fail, args have wrong type:\n"
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,17 +1,12 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀ type-eval type=?)
- (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ type-eval ∀ ~∀ type=?))
+(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
+ (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
[sysf:~∀ ~sysf:∀])
(only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ] #;[app/tc #%app] #;[λ/tc λ] #;[datum/tc #%datum]))
-#;(provide (except-out (all-from-out "sysf.rkt")
- sysf:∀ sysf:#%app sysf:λ
- (for-syntax sysf:type-eval sysf:type=?)))
-(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval sysf:type=?))
- (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ tyλ tyapp
- (for-syntax type-eval type=?))
+(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
+(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
+(provide ∀ inst Λ tyλ tyapp)
;; System F_omega
;; Type relation:
@@ -21,6 +16,7 @@
;; - terms from sysf.rkt
(define-syntax-category kind)
+
(begin-for-syntax
(current-kind? (λ (k) (or (#%type? k) (kind? k))))
;; Try to keep "type?" remain backward compatible with its uses so far,
@@ -40,6 +36,7 @@
#'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
(begin-for-syntax
+ (define sysf:type-eval (current-type-eval))
;; extend type-eval to handle tyapp
;; - requires manually handling all other forms
(define (type-eval τ)
@@ -51,62 +48,27 @@
[((~or (~literal ∀)(~literal →)
(~literal ⇒)(~literal tyapp)) . _)
((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal tyλ) _ ...) (sysf:type-eval τ)] ; dont eval under tyλ
[((~literal #%plain-lambda) (x ...) τ_body ...)
#:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
(syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
[((~literal #%plain-app) arg ...)
#:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
(syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- [_ #;(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
- (sysf:type-eval τ)]))
+ [_ (sysf:type-eval τ)])) ; dont eval under tyλ
(current-type-eval type-eval))
(define-base-kind ★)
(define-kind-constructor ⇒ #:arity >= 1)
(define-kind-constructor ∀★ #:arity >= 0)
-;; for now, handle kind checking in the types themselves
-;; TODO: move kind checking to a common place (like #%app)?
-;; when expanding: check and erase kinds
-
-;; TODO: need some kind of "promote" abstraction,
-;; so I dont have to manually add kinds to all types
-#;(define-basic-checked-id-stx String : ★)
-#;(define-basic-checked-id-stx Int : ★)
-;(define-base-type Str)
-;(provide String)
-;(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
-;(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
-
-;; → in Fω is not first-class, can't pass it around
-#;(define-basic-checked-stx → : ★ #:arity >= 1)
-#;(define-syntax (→ stx)
- (syntax-parse stx
- [(_ τ ... τ_res)
- #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
- #:when (typecheck? #'k_res #'★)
- #:when (same-types? #'(k ... k_res))
- (⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
-
-#;(define-syntax (∀ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
- #:when (★? #'k_body)
- (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
-
(define-syntax (∀ stx)
(syntax-parse stx
[(_ bvs:kind-ctx τ_body)
;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ #:with (tvs- τ_body- k_body)
+ (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
; expand so kind gets overwritten
(⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
-; (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@@ -132,67 +94,48 @@
(type-error
#:src #'any
#:msg "Expected ∀ type, got: ~a" #'any))))])))
- (define (type=? t1 t2)
- ;(printf "t1 = ~a\n" (syntax->datum t1))
- ;(printf "t2 = ~a\n" (syntax->datum t2))
- (or (and (★? t1) (#%type? t2))
- (and (#%type? t1) (★? t2))
- (and (syntax-parse (list t1 t2) #:datum-literals (:)
- [((~∀ ([tv1 : k1]) tbody1)
- (~∀ ([tv2 : k2]) tbody2))
- (type=? #'k1 #'k2)]
- [_ #t])
- (sysf:type=? t1 t2))))
+ (define old-type=? (current-type=?))
+ (define (type=? t1 t2)
+ (or (and (★? t1) (#%type? t2))
+ (and (#%type? t1) (★? t2))
+ (and (syntax-parse (list t1 t2) #:datum-literals (:)
+ [((~∀ ([tv1 : k1]) tbody1)
+ (~∀ ([tv2 : k2]) tbody2))
+ ((current-type=?) #'k1 #'k2)]
+ [_ #t])
+ (old-type=? t1 t2))))
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-#;(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) e)
- #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
- (⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
(define-syntax (Λ stx)
(syntax-parse stx
[(_ bvs:kind-ctx e)
- #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ #:with ((tv- ...) e- τ_e)
+ (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
-#;(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ ...)
- #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
- #:when (stx-andmap
- (λ (t k)
- (or (kind? k)
- (type-error #:src t
- #:msg "not a valid type: ~a" t)))
- #'(τ ...) #'(k_τ ...))
- #:with (e- ∀τ) (infer+erase #'e)
- #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
- #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
- (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
+
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ ...)
#:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
- #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
- #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
- (type-error #:src t #:msg "not a valid type: ~a" t)))
- #'(τ ...) #'(k_τ ...))
+ #:with ([τ- k_τ] ...)
+ (infers+erase #'(τ ...) #:expand (current-type-eval))
+ #:when (stx-andmap
+ (λ (t k) (or ((current-kind?) k)
+ (type-error #:src t #:msg "not a valid type: ~a" t)))
+ #'(τ ...) #'(k_τ ...))
#:when (typechecks? #'(k_τ ...) #'(k ...))
(⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
;; TODO: merge with regular λ and app?
+;; - see fomega2.rkt
(define-syntax (tyλ stx)
(syntax-parse stx
[(_ bvs:kind-ctx τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ #:with (tvs- τ_body- k_body)
+ (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
#:when ((current-kind?) #'k_body)
(⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
-#;(define-syntax (tyλ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
- (⊢ (λ tvs- τ_body-) : (⇒ b.tag ... k_body))]))
(define-syntax (tyapp stx)
(syntax-parse stx
@@ -213,138 +156,4 @@
(format "Expected: ~a arguments with type(s): "
(stx-length #'(k_in ...)))
(string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
-#;(define-syntax (tyapp stx)
- (syntax-parse stx
- [(_ τ_fn τ_arg ...)
- #:with [τ_fn- (~⇒* k_in ... k_out)] (infer+erase #'τ_fn)
-; #:fail-unless (⇒? #'k_fn)
-; (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
-; (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
-; #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'τ_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(τ_arg ...))
- (stx-map type->str #'(k_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with kind(s): "
- (stx-length #'(k_in ...)))
- (string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
-;
-; #:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
-; (string-append
-; (format
-; "Wrong number of args given to tyλ ~a:\ngiven: "
-; (syntax->datum #'τ_fn))
-; (string-join
-; (map
-; (λ (t k) (format "~a : ~a" t k))
-; (syntax->datum #'(τ_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-; ", ")
-; (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
-; #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
-; (string-append
-; (format
-; "Arguments to tyλ ~a have wrong type:\ngiven: "
-; (syntax->datum #'τ_fn))
-; (string-join
-; (map
-; (λ (t k) (format "~a : ~a" t k))
-; (syntax->datum #'(τ_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-; ", ")
-; "\nexpected arguments with type: "
-; (string-join
-; (map ~a (syntax->datum #`#,(stx-map get-orig #'(k ...))))
-; ", "))
-; ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
-; ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
-; (⊢ (#%app τ_fn- τ_arg- ...) : k_res)]))
-
-;; must override #%app and λ and primops to use new →
-;; TODO: parameterize →?
-
-#;(define-primop + : (→ Int Int Int) : ★)
-
-#;(define-syntax (λ/tc stx)
- (syntax-parse stx #:datum-literals (:)
- [(_ ([x : τ] ...) e)
- ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
- #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
- #:when (stx-andmap ★? #'(k ...))
- #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
- (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
-
-#;(define-syntax (app/tc stx)
- (syntax-parse stx
- [(_ e_fn e_arg ...)
- #:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
- #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
- #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in ...)))
- (string-join (stx-map type->str #'(τ_in ...)) ", "))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
-; #:with [e_fn- τ_fn] (infer+erase #'e_fn)
-; ;; this is sysf:→?, it's not defined in fomega so import without prefix
-; #: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 ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
-; #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
-; #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
-; (string-append
-; (format
-; "Wrong number of args given to function ~a:\ngiven: "
-; (syntax->datum #'e_fn))
-; (string-join
-; (map
-; (λ (e t) (format "~a : ~a" e t))
-; (syntax->datum #'(e_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-; ", ")
-; (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
-; #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
-; (string-append
-; (format
-; "Arguments to function ~a have wrong type:\ngiven: "
-; (syntax->datum #'e_fn))
-; (string-join
-; (map
-; (λ (e t) (format "~a : ~a" e t))
-; (syntax->datum #'(e_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-; ", ")
-; "\nexpected arguments with type: "
-; (string-join
-; (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
-; ", "))
-; (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
-
-;; must override #%datum to use new kinded-Int, etc
-#;(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . n:integer) (⊢ (#%datum . n) : Int)]
- [(_ . s:str) (⊢ (#%datum . s) : String)]
- [(_ . x)
- #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
- #'(#%datum . x)]))
-\ No newline at end of file
+ (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
+\ No newline at end of file
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -1,17 +1,15 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀ type-eval type=?)
- (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ type-eval ∀ ~∀ type=?))
+(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
+ (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
[sysf:~∀ ~sysf:∀])
(only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ] #;[app/tc #%app] #;[λ/tc λ] #;[datum/tc #%datum]))
-#;(provide (except-out (all-from-out "sysf.rkt")
- sysf:∀ sysf:#%app sysf:λ
- (for-syntax sysf:type-eval sysf:type=?)))
-(provide (except-out (all-from-out "sysf.rkt") (for-syntax sysf:type-eval sysf:type=?))
- (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ ;tyλ tyapp
- (for-syntax type-eval type=?))
+(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
+(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
+(provide ∀ inst Λ)
+
+; same as fomega except here λ and #%app works as both regular and type versions
+;; uses definition from stlc, but tweaks type? and kind? predicates
;; System F_omega
;; Type relation:
@@ -21,6 +19,7 @@
;; - terms from sysf.rkt
(define-syntax-category kind)
+
(begin-for-syntax
(current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
;; Try to keep "type?" remain backward compatible with its uses so far,
@@ -39,10 +38,10 @@
(syntax-parser
[(_ alias:id τ)
#:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
-; #:fail-unless (or (type? #'k_τ) (kind? #'k_τ)) (format "not a valid type: ~a\n" (type->str #'τ))
#'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
(begin-for-syntax
+ (define sysf:type-eval (current-type-eval))
;; extend type-eval to handle tyapp
;; - requires manually handling all other forms
(define (type-eval τ)
@@ -51,78 +50,20 @@
(syntax-parse τ
[((~literal #%plain-app) τ_fn τ_arg ...)
#:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
- ;#:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
- ;[((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
-; [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
-; [((~literal λ/tc) _ ...) (sysf:type-eval τ)]
-; [((~literal app/tc) _ ...) ((current-type-eval) (sysf:type-eval τ))]
[((~literal #%plain-lambda) (x ...) τ_body ...)
#:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
(syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
[((~literal #%plain-app) arg ...)
#:with (arg+ ...) (stx-map beta #'(arg ...))
(syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))]
[_ τ]))
- #;(define (type-eval τ)
- (syntax-parse τ
- [((~literal #%plain-app) τ_fn τ_arg ...)
- #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
- #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
- (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
- [((~or (~literal ∀)(~literal →)
- (~literal ⇒)#;(~literal tyapp)) . _)
- ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
- ;[((~literal tyλ) _ ...) (sysf:type-eval τ)] ; dont eval under tyλ
- [((~literal #%plain-lambda) (x ...) τ_body ...)
- #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
- (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
- [((~literal #%plain-app) arg ...)
- #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
- (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- [_ #;(~or x:id ((~literal tyλ) . _)) ; dont eval under tyλ
- (sysf:type-eval τ)]))
(current-type-eval type-eval))
(define-base-kind ★)
(define-kind-constructor ⇒ #:arity >= 1)
(define-kind-constructor ∀★ #:arity >= 0)
-;; for now, handle kind checking in the types themselves
-;; TODO: move kind checking to a common place (like #%app)?
-;; when expanding: check and erase kinds
-
-;; TODO: need some kind of "promote" abstraction,
-;; so I dont have to manually add kinds to all types
-#;(define-basic-checked-id-stx String : ★)
-#;(define-basic-checked-id-stx Int : ★)
-;(define-base-type Str)
-;(provide String)
-;(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
-;(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
-
-;; → in Fω is not first-class, can't pass it around
-#;(define-basic-checked-stx → : ★ #:arity >= 1)
-#;(define-syntax (→ stx)
- (syntax-parse stx
- [(_ τ ... τ_res)
- #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
- #:when (typecheck? #'k_res #'★)
- #:when (same-types? #'(k ... k_res))
- (⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
-
-#;(define-syntax (∀ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
- #:when (★? #'k_body)
- (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
-
(define-syntax (∀ stx)
(syntax-parse stx
[(_ bvs:kind-ctx τ_body)
@@ -130,7 +71,6 @@
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
; expand so kind gets overwritten
(⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
-; (⊢ (λ tvs- b.tag ... τ_body-) : ★)]))
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@@ -156,44 +96,26 @@
(type-error
#:src #'any
#:msg "Expected ∀ type, got: ~a" #'any))))])))
- (define (type=? t1 t2)
- ;(printf "t1 = ~a\n" (syntax->datum t1))
- ;(printf "t2 = ~a\n" (syntax->datum t2))
- (or (and (★? t1) (#%type? t2))
- (and (#%type? t1) (★? t2))
- (and (syntax-parse (list t1 t2) #:datum-literals (:)
- [((~∀ ([tv1 : k1]) tbody1)
- (~∀ ([tv2 : k2]) tbody2))
- (type=? #'k1 #'k2)]
- [_ #t])
- (sysf:type=? t1 t2))))
+ (define sysf:type=? (current-type=?))
+ (define (type=? t1 t2)
+ (or (and (★? t1) (#%type? t2))
+ (and (#%type? t1) (★? t2))
+ (and (syntax-parse (list t1 t2) #:datum-literals (:)
+ [((~∀ ([tv1 : k1]) tbody1)
+ (~∀ ([tv2 : k2]) tbody2))
+ ((current-type=?) #'k1 #'k2)]
+ [_ #t])
+ (sysf:type=? t1 t2))))
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-#;(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) e)
- #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'(b ...) #'e)
- (⊢ e- : (∀ ([tv- : b.tag] ...) τ_e))]))
(define-syntax (Λ stx)
(syntax-parse stx
[(_ bvs:kind-ctx e)
- #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ #:with ((tv- ...) e- τ_e)
+ (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
-#;(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ ...)
- #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
- #:when (stx-andmap
- (λ (t k)
- (or (kind? k)
- (type-error #:src t
- #:msg "not a valid type: ~a" t)))
- #'(τ ...) #'(k_τ ...))
- #:with (e- ∀τ) (infer+erase #'e)
- #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
- #:when (typechecks? #'(k_τ ...) #'(k_tv ...))
- (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))]))
+
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ ...)
@@ -203,172 +125,4 @@
(type-error #:src t #:msg "not a valid type: ~a" t)))
#'(τ ...) #'(k_τ ...))
#:when (typechecks? #'(k_τ ...) #'(k ...))
- (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]))
-
-;; TODO: merge with regular λ and app?
-#;(define-syntax (tyλ stx)
- (syntax-parse stx
- [(_ bvs:kind-ctx τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
- #:when ((current-kind?) #'k_body)
- (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
-#;(define-syntax (tyλ stx)
- (syntax-parse stx
- [(_ (b:kinded-binding ...) τ_body)
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'(b ...) #'τ_body)
- (⊢ (λ tvs- τ_body-) : (⇒ b.tag ... k_body))]))
-
-#;(define-syntax (tyapp stx)
- (syntax-parse stx
- [(_ τ_fn τ_arg ...)
- #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'τ_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(τ_arg ...))
- (stx-map type->str #'(k_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(k_in ...)))
- (string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
-#;(define-syntax (tyapp stx)
- (syntax-parse stx
- [(_ τ_fn τ_arg ...)
- #:with [τ_fn- (~⇒* k_in ... k_out)] (infer+erase #'τ_fn)
-; #:fail-unless (⇒? #'k_fn)
-; (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
-; (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
-; #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'τ_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(τ_arg ...))
- (stx-map type->str #'(k_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with kind(s): "
- (stx-length #'(k_in ...)))
- (string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
-;
-; #:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
-; (string-append
-; (format
-; "Wrong number of args given to tyλ ~a:\ngiven: "
-; (syntax->datum #'τ_fn))
-; (string-join
-; (map
-; (λ (t k) (format "~a : ~a" t k))
-; (syntax->datum #'(τ_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-; ", ")
-; (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
-; #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
-; (string-append
-; (format
-; "Arguments to tyλ ~a have wrong type:\ngiven: "
-; (syntax->datum #'τ_fn))
-; (string-join
-; (map
-; (λ (t k) (format "~a : ~a" t k))
-; (syntax->datum #'(τ_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
-; ", ")
-; "\nexpected arguments with type: "
-; (string-join
-; (map ~a (syntax->datum #`#,(stx-map get-orig #'(k ...))))
-; ", "))
-; ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
-; ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
-; (⊢ (#%app τ_fn- τ_arg- ...) : k_res)]))
-
-;; must override #%app and λ and primops to use new →
-;; TODO: parameterize →?
-
-#;(define-primop + : (→ Int Int Int) : ★)
-
-#;(define-syntax (λ/tc stx)
- (syntax-parse stx #:datum-literals (:)
- [(_ ([x : τ] ...) e)
- ;#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(τ ...)))
- #:with (k ...) (stx-map (λ (t) (typeof ((current-type-eval) t))) #'(τ ...))
- #:when (stx-andmap ★? #'(k ...))
- #:with (xs- e- τ_res) (infer/type-ctxt+erase #'([x : τ] ...) #'e)
- (⊢ (λ xs- e-) : (→ τ ... τ_res))]))
-
-#;(define-syntax (app/tc stx)
- (syntax-parse stx
- [(_ e_fn e_arg ...)
- #:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
- #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
- #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in ...)))
- (string-join (stx-map type->str #'(τ_in ...)) ", "))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
-; #:with [e_fn- τ_fn] (infer+erase #'e_fn)
-; ;; this is sysf:→?, it's not defined in fomega so import without prefix
-; #: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 ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
-; #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
-; #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
-; (string-append
-; (format
-; "Wrong number of args given to function ~a:\ngiven: "
-; (syntax->datum #'e_fn))
-; (string-join
-; (map
-; (λ (e t) (format "~a : ~a" e t))
-; (syntax->datum #'(e_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-; ", ")
-; (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
-; #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
-; (string-append
-; (format
-; "Arguments to function ~a have wrong type:\ngiven: "
-; (syntax->datum #'e_fn))
-; (string-join
-; (map
-; (λ (e t) (format "~a : ~a" e t))
-; (syntax->datum #'(e_arg ...))
-; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
-; ", ")
-; "\nexpected arguments with type: "
-; (string-join
-; (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
-; ", "))
-; (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
-
-;; must override #%datum to use new kinded-Int, etc
-#;(define-syntax (datum/tc stx)
- (syntax-parse stx
- [(_ . n:integer) (⊢ (#%datum . n) : Int)]
- [(_ . s:str) (⊢ (#%datum . s) : String)]
- [(_ . x)
- #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
- #'(#%datum . x)]))
-\ No newline at end of file
+ (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]))
+\ No newline at end of file
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -1,21 +1,25 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "stlc+reco+sub.rkt" #%app λ + type=?)
- (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ sub?))
- (only-in "sysf.rkt" ∀? type=?)
- (prefix-in sysf: (only-in "sysf.rkt" ∀ #;type=?))
+(require (except-in "stlc+reco+sub.rkt" #%app λ +)
+ (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ))
+ (only-in "sysf.rkt" ∀?)
+ (prefix-in sysf: (only-in "sysf.rkt" ∀))
(rename-in (only-in "sysf.rkt" ~∀) [~∀ ~sysf:∀]))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]) (for-syntax sub?))
-(provide (except-out (all-from-out "stlc+reco+sub.rkt")
- stlc:#%app stlc:λ (for-syntax stlc:sub?))
- (except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax #;sysf:type=? ~sysf:∀)))
-(provide ∀ Λ inst (for-syntax #;type=?))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
+(provide (except-out (all-from-out "stlc+reco+sub.rkt") stlc:#%app stlc:λ)
+ (except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax ~sysf:∀)))
+(provide ∀ Λ inst)
;; System F<:
;; Types:
;; - types from sysf.rkt
+;; - extend ∀ with bounds
;; Terms:
;; - terms from sysf.rkt
+;; - extend Λ and inst
+;; Other
+;; - current-promote, expose
+;; - extend current-sub? to call current-promote
(define-primop + : (→ Nat Nat Nat))
@@ -31,19 +35,14 @@
(if sub (expose sub) t)]
[else t]))
(current-promote expose)
- #;(define (type=? t1 t2)
- (displayln (typeof t1))
- (displayln (typeof t2))
- (and (sysf:type=? t1 t2)
- (sysf:type=? (typeof t1) (typeof t2))))
- #;(current-type=? type=?)
- ; need this, to lift base-types; is there another way to do this?
+ (define stlc:sub? (current-sub?))
(define (sub? t1 t2)
(stlc:sub? ((current-promote) t1) t2))
(current-sub? sub?)
(current-typecheck-relation (current-sub?)))
-(define-type-constructor <: #:arity >= 0) ; quasi-kind, but must be type constructor because its arguments are types
+; quasi-kind, but must be type constructor because its arguments are types
+(define-type-constructor <: #:arity >= 0)
(begin-for-syntax
(current-type? (λ (t) (or (type? t) (<:? (typeof t))))))
@@ -51,13 +50,10 @@
;; 1) typechecking the body of
;; 2) instantiation of ∀
;; Problem: need type annotations, even in expanded form
-;(define ∀-internal void)
+;; Solution: store type annotations in a (quasi) kind <:
(define-syntax ∀
(syntax-parser #:datum-literals (<:)
[(_ ([tv:id <: τ:type] ...) τ_body)
- ;#:with ((tv- ...) τ_body- k) (infer/ctx+erase #'([tv : #%type] ...) #'τ_body)
- ;#:when (#%type? #'k)
- ;(mk-type #'(λ (tv- ...) (∀-internal τ.norm ... τ_body-)))]))
; eval first to overwrite the old #%type
(⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))]))
(begin-for-syntax
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -4,7 +4,8 @@
(require (except-in "stlc.rkt" #%app)
(prefix-in stlc: (only-in "stlc.rkt" #%app)))
(provide (except-out (all-from-out "stlc.rkt") stlc:#%app))
-(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]) define-primop)
+(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum])
+ define-primop)
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@@ -14,6 +15,8 @@
;; - terms from stlc.rkt
;; - numeric literals
;; - prim +
+;; Typechecking forms:
+;; - define-primop
(define-base-type Int)
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -1,13 +1,13 @@
#lang racket/base
(require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ type=?))
- (except-in "stlc+reco+var.rkt" #%app λ type=? × tup proj)
- (only-in "stlc+tup.rkt" × tup proj))
+(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ))
+ (except-in "stlc+reco+var.rkt" #%app λ × tup proj)
+ (only-in "stlc+tup.rkt" × tup proj)) ; want tuples, not records
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
(provide (except-out (all-from-out "stlc+reco+var.rkt")
- stlc:#%app stlc:λ (for-syntax stlc:type=?))
+ stlc:#%app stlc:λ)
(all-from-out "stlc+tup.rkt"))
-(provide μ fld unfld (for-syntax type=?))
+(provide μ fld unfld)
;; stlc + (iso) recursive types
;; Types:
@@ -20,6 +20,7 @@
(define-type-constructor μ #:arity = 1 #:bvs = 1)
(begin-for-syntax
+ (define stlc:type=? (current-type=?))
;; extend to handle μ, ie lambdas
(define (type=? τ1 τ2)
; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -2,16 +2,14 @@
(require "typecheck.rkt")
;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
;; but extend sub? from stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum sub?)
- (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum sub?))
+(require (except-in "stlc+sub.rkt" #%app #%datum)
+ (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum))
(except-in "stlc+reco+var.rkt" #%app #%datum +)
(prefix-in stlc+reco+var: (only-in "stlc+reco+var.rkt" #%datum)))
(provide (rename-out [stlc+sub:#%app #%app]
[datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum
- (for-syntax stlc+sub:sub?))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum)
(except-out (all-from-out "stlc+reco+var.rkt") stlc+reco+var:#%datum))
-(provide (for-syntax sub?))
;; Simply-Typed Lambda Calculus, plus subtyping, plus records
;; Types:
@@ -27,10 +25,12 @@
[(_ . x) #'(stlc+reco+var:#%datum . x)]))
(begin-for-syntax
+ (define old-sub? (current-sub?))
(define (sub? τ1 τ2)
; (printf "t1 = ~a\n" (syntax->datum τ1))
; (printf "t2 = ~a\n" (syntax->datum τ2))
(or
+ (old-sub? τ1 τ2)
(syntax-parse (list τ1 τ2)
[((~× [k : τk] ...) (~× [l : τl] ...))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
@@ -50,7 +50,6 @@
#:with (k_match τk_match) (stx-assoc #'label #'([k τk] ...))
((current-sub?) #'τk_match #'τlabel)])
#'([l τl] ...))]
- [_ #f])
- (stlc+sub:sub? τ1 τ2)))
+ [_ #f])))
(current-sub? sub?)
(current-typecheck-relation (current-sub?)))
\ No newline at end of file
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -3,7 +3,7 @@
(require (only-in racket/bool symbol=?))
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let × ×?))
(except-in "stlc+tup.rkt" #%app begin tup proj let ×)
- (rename-in (only-in "stlc+tup.rkt" ~×) [~× ~stlc:×]))
+ (rename-in (only-in "stlc+tup.rkt" ~×) [~× ~stlc:×]))
(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
[define/tc define]))
(provide (except-out (all-from-out "stlc+tup.rkt")
@@ -14,19 +14,19 @@
;; Simply-Typed Lambda Calculus, plus records and variants
-;; Type relations:
-;; - type=? extended to strings
-;; define-type-alias (also provided to programmer)
;; Types:
;; - types from stlc+tup.rkt
-;; - extend tuple type × to include records
+;; - redefine tuple type × to records
;; - sum type constructor ∨
;; Terms:
;; - terms from stlc+tup.rkt
-;; - extend tup to include records
+;; - redefine tup to records
;; - sums (var)
;; TopLevel:
;; - define (values only)
+;; - define-type-alias
+;; Typechecking forms
+;; - same-types?
(begin-for-syntax
(define (same-types? τs)
@@ -38,7 +38,6 @@
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ:type)
- ; must eval, otherwise undefined types will be allowed
#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
; re-define tuples as records
@@ -92,7 +91,8 @@
[any
(type-error #:src #'any
#:msg (string-append
- "Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
+ "Improper usage of type constructor ∨: ~a,"
+ "expected (∨ [label:id : τ:type] ...+)")
#'any)]))
(begin-for-syntax
(define ∨? ∨/internal?)
@@ -133,7 +133,7 @@
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
#:with (((x-) e_l- τ_el) ...)
- (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+ (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
#:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
(⊢ (let ([l_e (car e-)])
(cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -4,7 +4,7 @@
(prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)))
(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]))
(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
-(provide (for-syntax sub? subs? current-sub?))
+(provide (for-syntax subs? current-sub?))
;; Simply-Typed Lambda Calculus, plus subtyping
;; Types:
@@ -22,9 +22,6 @@
(define-base-type Top)
(define-base-type Num)
(define-base-type Nat)
-;; TODO: implement define-subtype, for now hardcode relations
-;(define-subtype Int <: Num)
-;(define-subtype Nat <: Int)
(define-primop + : (→ Num Num Num))
(define-primop * : (→ Num Num Num))
@@ -38,22 +35,57 @@
(begin-for-syntax
(define (sub? t1 t2)
- ; only need this because recursive calls made with unexpanded types
+ ; need this because recursive calls made with unexpanded types
(define τ1 ((current-type-eval) t1))
(define τ2 ((current-type-eval) t2))
; (printf "t1 = ~a\n" (syntax->datum τ1))
; (printf "t2 = ~a\n" (syntax->datum τ2))
(or ((current-type=?) τ1 τ2)
- (syntax-parse (list τ1 τ2)
- [(_ ~Top) #t]
- [(~Nat τ) ((current-sub?) #'Int #'τ)]
- [(~Int τ) ((current-sub?) #'Num #'τ)]
- [(τ ~Num) ((current-sub?) #'τ #'Int)]
- [(τ ~Int) ((current-sub?) #'τ #'Nat)]
- [((~→ s1 ... s2) (~→ t1 ... t2))
- (and (subs? #'(t1 ...) #'(s1 ...))
- ((current-sub?) #'s2 #'t2))]
- [_ #f])))
+ (Top? τ2)))
(define current-sub? (make-parameter sub?))
(current-typecheck-relation sub?)
- (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2)))
+ (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2))
+
+ (define-syntax (define-sub-relation stx)
+ (syntax-parse stx #:datum-literals (<: =>)
+ [(_ τ1:id <: τ2:id)
+ #:with τ1-expander (format-id #'τ1 "~~~a" #'τ1)
+ #:with τ2-expander (format-id #'τ2 "~~~a" #'τ2)
+ #:with fn (generate-temporary)
+ #:with old-sub? (generate-temporary)
+ #'(begin
+ (define old-sub? (current-sub?))
+ (define (fn t1 t2)
+ (define τ1 ((current-type-eval) t1))
+ (define τ2 ((current-type-eval) t2))
+ (syntax-parse (list τ1 τ2)
+ [(τ1-expander τ) ((current-sub?) #'τ2 #'τ)]
+ [(τ τ2-expander) ((current-sub?) #'τ #'τ1)]
+ [_ #f]))
+ (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2))))
+ (current-typecheck-relation (current-sub?)))]
+ [(_ (~seq τ1:id <: τ2:id (~and (~literal ...) ddd))
+ (~seq τ3:id <: τ4:id)
+ =>
+ (tycon1 . rst1) <: (tycon2 . rst2))
+ #:with tycon1-expander (format-id #'tycon1 "~~~a" #'tycon1)
+ #:with tycon2-expander (format-id #'tycon2 "~~~a" #'tycon2)
+ #:with fn (generate-temporary)
+ #:with old-sub? (generate-temporary)
+ #'(begin
+ (define old-sub? (current-sub?))
+ (define (fn t1 t2)
+ (define τ1 ((current-type-eval) t1))
+ (define τ2 ((current-type-eval) t2))
+ (syntax-parse (list τ1 τ2)
+ [((tycon1-expander . rst1) (tycon2-expander . rst2))
+ (and (subs? #'(τ1 ddd) #'(τ2 ddd))
+ ((current-sub?) #'τ3 #'τ4))]
+ [_ #f]))
+ (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2))))
+ (current-typecheck-relation (current-sub?)))]))
+
+ (define-sub-relation Nat <: Int)
+ (define-sub-relation Int <: Num)
+ (define-sub-relation t1 <: s1 ... s2 <: t2 => (→ s1 ... s2) <: (→ t1 ... t2)))
+
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -14,9 +14,7 @@
;; - terms from ext-stlc.rkt
;; - tup and proj
-(define-type-constructor ×)
-;(define-basic-checked-stx ×)
-;(define-type-constructor (× τ ...) #:declare τ type)
+(define-type-constructor ×) ; default arity >=0
(define-syntax (tup stx)
(syntax-parse stx
@@ -26,7 +24,6 @@
(define-syntax (proj stx)
(syntax-parse stx
[(_ e_tup n:nat)
-; #:with [e_tup- τs_tup] (infer×+erase #'e_tup)
#:with [e_tup- τs_tup] (⇑ e_tup as ×)
#:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
(⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -1,34 +1,44 @@
#lang racket/base
(require "typecheck.rkt")
(provide (rename-out [λ/tc λ] [app/tc #%app]))
-(provide (for-syntax type=? types=? current-type=? type-eval))
-(provide #%module-begin #%top-interaction #%top require) ; from racket
+(provide (for-syntax current-type=? types=?))
+(provide #%module-begin #%top-interaction #%top require) ; useful racket forms
;; Simply-Typed Lambda Calculus
-;; - no base type, so cannot write any terms
+;; - no base types; can't write any terms
;; Types: multi-arg → (1+)
;; Terms:
;; - var
-;; - multi-arg lambda (0+)
-;; - multi-arg app (0+)
+;; - multi-arg λ (0+)
+;; - multi-arg #%app (0+)
+;; Other:
+;; - "type" syntax category; defines:
+;; - define-base-type
+;; - define-type-constructor
+;; Typechecking forms:
+;; - current-type-eval
+;; - current-type=?
(begin-for-syntax
;; type eval
- ;; - type-eval = =full expansion == canonical type representation
+ ;; - type-eval == full expansion == canonical type representation
;; - must expand because:
;; - checks for unbound identifiers (ie, undefined types)
+ ;; - checks for valid types, ow can't distinguish types and terms
+ ;; - could parse types but separate parser leads to duplicate code
;; - later, expanding enables reuse of same mechanisms for kind checking
;; and type application
(define (type-eval τ)
- (or #;(expanded-type? τ) ; don't expand if already expanded
- (add-orig (expand/df τ) τ)))
-
+ ; TODO: optimization: don't expand if expanded
+ ; currently, this causes problems when
+ ; combining unexpanded and expanded types to create new types
+ (add-orig (expand/df τ) τ))
+
(current-type-eval type-eval)
;; type=? : Type Type -> Boolean
- ;; Indicates whether two types are equal
- ;; type equality == structurally free-identifier=?
- ;; assumes canonical (ie expanded) representation
+ ;; Two types are equivalent when structurally free-identifier=?
+ ;; - assumes canonical (ie expanded) representation
(define (type=? τ1 τ2)
; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
@@ -37,16 +47,16 @@
[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
[_ #f]))
+ (define current-type=? (make-parameter type=?))
+ (current-typecheck-relation type=?)
+
+ ;; convenience fns for current-type=?
(define (types=? τs1 τs2)
(and (stx-length=? τs1 τs2)
- (stx-andmap (current-type=?) τs1 τs2)))
+ (stx-andmap (current-type=?) τs1 τs2))))
- (define current-type=? (make-parameter type=?))
- (current-typecheck-relation type=?))
-
(define-syntax-category type)
-;(define-basic-checked-stx → : #%type #:arity >= 1)
(define-type-constructor → #:arity >= 1)
(define-syntax (λ/tc stx)
@@ -58,12 +68,7 @@
(define-syntax (app/tc stx)
(syntax-parse stx
[(_ e_fn e_arg ...)
- ;; 2015-08-06: there are currently three alternative tycon matching syntaxes
-; #:with [e_fn- (~→* τ_in ... τ_out)] (infer→+erase #'e_fn) ; #1 (external) pattern expander
- ;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander
- ;#:with (τ_in ...) (→-get τ_in from #'τ_fn)
- ;#:with τ_out (→-get τ_out from #'τ_fn)
- #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →) ; #3 work directly on term -- better err msg
+ #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(string-append
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -1,13 +1,11 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "stlc+lit.rkt" #%app λ type=?)
+(require (except-in "stlc+lit.rkt" #%app λ)
(prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ))
- (only-in "stlc+rec-iso.rkt" type=?))
+ (only-in "stlc+rec-iso.rkt")) ; want type=? from here
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ)
- (all-from-out "stlc+rec-iso.rkt")) ; type=?
-(provide ∀ Λ inst)
-
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ))
+(provide Λ inst)
;; System F
;; Type relation:
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -7,7 +7,8 @@
[(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
[(_ e : τ-expected)
#:with τ (typeof (expand/df #'e))
- #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
+ #:fail-unless
+ (typecheck? #'τ ((current-type-eval) #'τ-expected))
(format
"Expression ~a [loc ~a:~a] has type ~a, expected ~a"
(syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -18,7 +19,8 @@
(syntax-parse stx #:datum-literals (:)
[(_ e : not-τ)
#:with τ (typeof (expand/df #'e))
- #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ))
+ #:fail-when
+ (typecheck? #'τ ((current-type-eval) #'not-τ))
(format
"(~a:~a) Expression ~a should not have type ~a"
(syntax-line stx) (syntax-column stx)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -24,13 +24,11 @@
;; is easily inserted into each #%- form
;; - A base type is just a Racket identifier, so type equality, even with
;; aliasing, is just free-identifier=?
-
-;; Types are represented as fully expanded syntax
-;; - base types are identifiers
;; - type constructors are prefix
(struct exn:fail:type:runtime exn:fail:user ())
+;; require macro
;; need options for
;; - pass through
;; - use (generated) prefix to avoid conflicts
@@ -55,19 +53,20 @@
(regexp-replace pre-pat name ""))))
(all-from-out base-lang))))]))
-
-
;; type assignment
(begin-for-syntax
- ;; macro for nicer syntax
+ ;; Type assignment macro for nicer syntax
(define-syntax (⊢ stx)
(syntax-parse stx #:datum-literals (:)
[(_ e : τ) #'(assign-type #`e #`τ)]
[(_ e τ) #'(⊢ e : τ)]))
-
+
+ ;; Actual type assignment function.
;; assign-type Type -> Syntax
;; Attaches type τ to (expanded) expression e.
- ;; must eval here, to catch unbound types
+ ;; - eval here so all types are stored in canonical form
+ ;; - syntax-local-introduce fixes marks on types
+ ;; which didnt get marked bc they were syntax properties
(define (assign-type e τ #:tag [tag 'type])
(syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
@@ -75,6 +74,11 @@
;; Retrieves type of given stx, or #f if input has not been assigned a type.
(define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
+ ;; - infers type of e
+ ;; - checks that type of e matches the specified type
+ ;; - erases types in e
+ ;; - returns e- and its type
+ ;; - does not return type if it's base type
(define-syntax (⇑ stx)
(syntax-parse stx #:datum-literals (as)
[(_ e as tycon)
@@ -89,7 +93,6 @@
"~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
(syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
(syntax->datum #'e) 'tycon (type->str #'τ_e))
- ;#:with args (τ-get #'τ_e)
(if (stx-pair? #'τ_e)
(syntax-parse #'τ_e
[(τ-expander . args) #'(e- args)])
@@ -121,6 +124,8 @@
#'(e- (... ...))
#'(τ_e (... ...)))
#'res])]))
+
+ ;; basic infer function with no context:
;; infers the type and erases types in an expression
(define (infer+erase e #:expand [expand-fn expand/df])
(define e+ (expand-fn e))
@@ -131,10 +136,10 @@
;; This is the main "infer" function. All others are defined in terms of this.
;; It should be named infer+erase but leaving it for now for backward compat.
- ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
- ;; expanded before wrapping in lambda
- ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
- ;; the types before typechecking, which is acceptable
+ ;; ctx = vars and their types
+ ;; tvctx = tyvars and their kinds
+ ;; octx + tag = some other context (and an associated tag)
+ ;; eg bounded quantification in Fsub
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
#:octx [octx tvctx] #:tag [tag 'unused]
#:expand [expand-fn expand/df])
@@ -160,14 +165,16 @@
((~literal #%expression) e+) ... (~literal void))))))))
(expand-fn
#`(λ (tv ...)
- (let-syntax ([tv (make-rename-transformer (assign-type (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...)
+ (let-syntax ([tv (make-rename-transformer
+ (assign-type
+ (assign-type #'tv #'k)
+ #'ok #:tag '#,tag))] ...)
(λ (x ...)
- (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ))] ...)
+ (let-syntax ([x (make-rename-transformer
+ (assign-type #'x #'τ))] ...)
(#%expression e) ... void)))))
-; #:when (stx-map displayln #'(e+ ...))
-; #:when (displayln (stx-map typeof #'(e+ ...)))
(list #'tvs+ #'xs+ #'(e+ ...)
- (stx-map ; check is when trying to combine #%type and kinds
+ (stx-map ; need this check when combining #%type and kinds
(λ (t) (or (false? t) (syntax-local-introduce t)))
(stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
@@ -187,25 +194,15 @@
(define (infer/tyctx+erase ctx e)
(syntax-parse (infer (list e) #:tvctx ctx)
[(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
-
- ;; infers type and erases types in a single expression,
- ;; in the context of the given bindings and their types
- (define (infer/type-ctxt+erase x+τs e)
- (syntax-parse (infer (list e) #:ctx x+τs)
- [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
- ;; infers type and erases types in multiple expressions,
- ;; in the context of (one set of) given bindings and their tpyes
- (define (infers/type-ctxt+erase ctxt es)
- (stx-cdr (infer es #:ctx ctxt)))
- ;; infers and erases types in an expression, in the context of given type vars
- #;(define (infer/tvs+erase e tvs)
- (syntax-parse (infer (list e) #:tvs tvs)
- [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
- ; type parameters, for type checker aspects that require extension
+ ; extra indirection, enables easily overriding type=? with sub?
+ ; to add subtyping, without changing any other definitions
+ ; - must be here (instead of stlc) due to rackunit-typechecking
(define current-typecheck-relation (make-parameter #f))
+
+ ;; convenience fns for current-typecheck-relation
(define (typecheck? t1 t2)
- ((current-typecheck-relation) t1 t2)) ;((current-type-eval) t1) ((current-type-eval) t2)))
+ ((current-typecheck-relation) t1 t2))
(define (typechecks? τs1 τs2)
(and (= (stx-length τs1) (stx-length τs2))
(stx-andmap typecheck? τs1 τs2)))
@@ -241,18 +238,8 @@
(current-continuation-marks)))))
(begin-for-syntax
- ;; type validation
- ;; only check outer wrapper; tycons are responsible for verifying their own args
- #;(define (#%type? t) (typecheck? t #'#%type))
- #;(define (is-type? τ)
- (or (plain-type? τ)
- ; partial expand to reveal #%type wrapper
- (syntax-parse (local-expand τ 'expression (list #'#%type))
- [((~literal #%type) _) #t] [_ #f])))
- (define (expanded-type? τ)
- (and (typeof τ) #;(typecheck? (typeof τ) #'#%type) τ))
-
; surface type syntax is saved as the value of the 'orig property
+ ; used to report error msgs
(define (add-orig stx orig)
(define origs (or (syntax-property orig 'orig) null))
(syntax-property stx 'orig (cons orig origs)))
@@ -265,112 +252,20 @@
[(stx-pair? τ) (string-join (stx-map type->str τ)
#:before-first "("
#:after-last ")")]
- [else (format "~a" (syntax->datum τ))]))
-
- ;; consumes:
- ;; - type
- ;; - type constructor identifier
- ;; - syntax-class representing shape of arguments to tycon
- #;(define-syntax (match-type stx)
- (syntax-parse stx
- [(_ ty tycon cls)
- #'(syntax-parse ((current-type-eval) ty)
- [((~literal #%plain-type)
- ((~literal #%plain-lambda) (tv:id (... ...))
- ((~literal let-values) () ((~literal let-values) ()
- ((~literal #%plain-app) t . args)))))
- #:declare args cls ; check shape of arguments
- #:fail-unless (typecheck? #'t #'tycon) ; check tycons match
- (format "Type error: expected ~a type, got ~a"
- (type->str #'τ) (type->str ty))
- #'args]
- [_ #f])]))
-)
-
-(begin-for-syntax
- (define (bracket? stx)
- (define paren-shape/#f (syntax-property stx 'paren-shape))
- (and paren-shape/#f (char=? paren-shape/#f #\[)))
- #;(define-syntax-class bound-vars
- (pattern
- (~and stx [[x:id ...]]
- #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
- #:when (and (bracket? #'stx)
- (bracket? (stx-car #'stx)))))
- (begin-for-syntax
- (define (bracket? stx)
- (define paren-shape/#f (syntax-property stx 'paren-shape))
- (and paren-shape/#f (char=? paren-shape/#f #\[)))
- #;(define-syntax-class bound-vars
- (pattern
- (~and stx [[x:id ...]]
- #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
- #:when (and (bracket? #'stx)
- (bracket? (stx-car #'stx)))))))
+ [else (format "~a" (syntax->datum τ))])))
(begin-for-syntax
(define (mk-? id) (format-id id "~a?" id))
- (define-for-syntax (mk-? id) (format-id id "~a?" id)))
-
-#;(define #%type void)
-#;(define-for-syntax (mk-type t) (assign-type t #'#%type))
-
-;#;(define-syntax (define-base-type stx)
-; (syntax-parse stx
-; [(_ τ:id)
-; #:with τ? (format-id #'τ "~a?" #'τ)
-; #:with τ-internal (generate-temporary #'τ)
-; #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
-; #:with τ-cls (generate-temporary #'τ)
-; #:with τ-expander (format-id #'τ "~~~a" #'τ)
-; #'(begin
-; (provide τ (for-syntax τ? inferτ+erase τ-expander))
-; (define τ-internal
-; (λ () (raise (exn:fail:type:runtime
-; (format "~a: Cannot use type at run time" 'τ)
-; (current-continuation-marks)))))
-; (define-syntax (τ stx)
-; (syntax-parse stx
-; [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
-; (begin-for-syntax
-; ; expanded form of τ
-; (define-syntax-class τ-cls
-; (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
-; (define (τ? t)
-; (syntax-parse ((current-type-eval) t)
-; [expanded-type
-; #:declare expanded-type τ-cls
-; (typecheck? #'expanded-type.ty #'τ-internal)]))
-; ; base type pattern expanders should be identifier macros but
-; ; parsing them is ambiguous, so handle and pass through other args
-; (define-syntax τ-expander
-; (pattern-expander
-; (syntax-parser
-; [ty:id #'((~literal #%plain-type)
-; ((~literal #%plain-app)
-; (~literal τ-internal)))]
-; [(_ . rst)
-; #'(((~literal #%plain-type)
-; ((~literal #%plain-app)
-; (~literal τ-internal))) . rst)])))
-; (define (inferτ+erase e)
-; (syntax-parse (infer+erase e) #:context e
-; [(e- expanded-type)
-; #:declare expanded-type τ-cls
-; #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
-; (format
-; "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
-; (syntax-source e) (syntax-line e) (syntax-column e)
-; (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
-; #'e-]))))]))
+ (define-for-syntax (mk-? id) (format-id id "~a?" id))
+ (define (brace? stx)
+ (define paren-shape/#f (syntax-property stx 'paren-shape))
+ (and paren-shape/#f (char=? paren-shape/#f #\{))))
(define-syntax define-basic-checked-id-stx
(syntax-parser #:datum-literals (:)
[(_ τ:id : kind)
#:with τ? (mk-? #'τ)
#:with τ-internal (generate-temporary #'τ)
- ;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
- ;#:with τ-cls (generate-temporary #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#'(begin
(provide τ (for-syntax τ? τ-expander))
@@ -399,8 +294,6 @@
(syntax-parser
[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
-#;(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
-
; I use identifiers "τ" and "kind" but this form is not restricted to them.
; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
(define-syntax (define-basic-checked-stx stx)
@@ -413,13 +306,10 @@
(~seq #:bvs (~and has-bvs? bvs-op) bvs-n:exact-nonnegative-integer)
#:defaults ([bvs-op #'>=][bvs-n #'0])))
#:with #%kind (format-id #'kind "#%~a" #'kind)
- ;#:with kind+ ((current-type-eval) #'kind)
#:with τ-internal (generate-temporary #'τ)
#:with τ? (mk-? #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
#:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
- ;#:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
- ;#:with τ-get (format-id #'τ "~a-get" #'τ)
#`(begin
(provide τ (for-syntax τ-expander τ-expander* τ? #;inferτ+erase))
(begin-for-syntax
@@ -441,7 +331,6 @@
(syntax-parser
[(_ . pat)
#'(~or
- ;((~literal #%plain-app) (~literal τ-internal) . pat)
(τ-expander . pat)
(~and
any
@@ -453,32 +342,13 @@
(define (τ? t)
(and (stx-pair? t)
(syntax-parse t
- [((~literal #%plain-lambda) bvs ((~literal #%plain-app) tycon . _))
- (typecheck? #'tycon #'τ-internal)]
+ [((~literal #%plain-lambda) bvs ((~literal #%plain-app) (~literal τ-internal) . _))
+ #t #;(typecheck? #'tycon #'τ-internal)]
[_ #f]))))
-; #;(define (τ-get t)
-; (syntax-parse t
-; [(τ-expander . pat) #'pat]))
-; #;(define (inferτ+erase e)
-; (syntax-parse (infer+erase e) #:context e
-; [(e- τ_e)
-; #:fail-unless (stx-pair? #'τ_e)
-; (format
-; "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
-; (syntax-source e) (syntax-line e) (syntax-column e)
-; (syntax->datum e) 'τ (type->str #'τ_e))
-; #:with ((~literal #%plain-app) tycon . args) #'τ_e
-; #:fail-unless (typecheck? #'tycon #'τ-internal)
-; (format
-; "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
-; (syntax-source e) (syntax-line e) (syntax-column e)
-; (syntax->datum e) 'τ (type->str #'τ_e))
-; #`(e- args)])))
(define τ-internal
(λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use type at run time" 'τ)
(current-continuation-marks)))))
- ;(define (τ? ty) (syntax-parser ty [((~literal τ) . pat) #t][_ #f]))
;; ; this is the actual constructor
(define-syntax (τ stx)
(syntax-parse stx
@@ -493,15 +363,7 @@
#:with (bvs- τs- _)
(infers/ctx+erase #'([bv : #%kind] (... ...)) #'args
#:expand (current-type-eval))
-; #:when (stx-andmap
-; (λ (t k)
-; (or (typecheck? k #'kind+)
-; (type-error #:src t
-; #:msg "not a valid type: ~a" t)))
-; #'args #'ks)
#:with (~! (~var _ kind) (... ...)) #'τs-
-; #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
-; #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
(assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind)]
;; else fail with err msg
[_
@@ -509,394 +371,6 @@
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
#'τ stx #'op #'n)])))]))
-; #;[(_ #:cat cat
-; (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
-; #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
-; . pat)
-; ; lits must have ~ prefix (for syntax-parse compat) for now
-; (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
-; decls ...
-; #;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
-; #:defaults ([(tvar 1) null][(cls 1) null])))
-; #:with τ-match (format-id #'τ "~a-match" #'τ)
-; #:with τ? (format-id #'τ "~a?" #'τ)
-; #:with τ-get (format-id #'τ "~a-get" #'τ)
-; #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
-; #:with τ-expander (format-id #'τ "~~~a" #'τ)
-; #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
-; #:with pat-class (generate-temporary #'τ) ; syntax-class name
-; #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
-; #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
-; #`(begin
-; ;; list can't be function, ow it will use typed #%app
-; ;; define lit as macro that expands into #%app,
-; ;; so it will use the #%app here (racket's #%app)
-; (define lit-tmp void) ...
-; (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
-; (provide lit ...)
-; (provide τ (for-syntax τ-expander τ-expander*))
-; (begin-for-syntax
-; #;(define-syntax lit
-; (pattern-expander
-; (syntax-parser
-; [(_ . xs)
-; #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
-; ; the ~τ pattern backtracks normally;
-; ; the ~τ* version errors immediately for a non-match
-; (define-syntax τ-expander
-; (pattern-expander
-; (syntax-parser
-; [(_ (~optional
-; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
-; . match-pat)
-; ;; manually replace literals with expanded form, to get around ~ restriction
-; #:with new-match-pat
-; #`#,(subst-datum-lits
-; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
-; #'(lit ...)
-; #'match-pat)
-; #'((~literal #%plain-type)
-; ((~literal #%plain-lambda) (bvs.x (... ...))
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
-; (define-syntax τ-expander*
-; (pattern-expander
-; (syntax-parser
-; [(_ (~optional
-; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
-; . match-pat)
-; #:with pat-from-constructor
-; #,(if (attribute bvs-test)
-; #'(quote-syntax (τ bvs-pat.stx . pat))
-; #'(quote-syntax (τ . pat)))
-; ;; manually replace literals with expanded form, to get around ~ restriction
-; #:with new-match-pat
-; #`#,(subst-datum-lits
-; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
-; #'(lit ...)
-; #'match-pat)
-; #'(~and
-; (~or
-; ((~literal #%plain-type)
-; ((~literal #%plain-lambda) (bvs.x (... ...))
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
-; (~and any
-; (~do
-; (type-error #:src #'any
-; #:msg
-; "Expected type of expression to match pattern ~a, got: ~a"
-; (quote-syntax pat-from-constructor) #'any))))
-; ~!)])))
-; (define-syntax-class pat-class
-; ;; dont check is-type? here; should already be types
-; ;; only check is-type? for user-entered types, eg tycon call
-; ;; thus, dont include decls here, only want shape
-; ; uses "lit" pattern expander
-; (pattern pat))
-; (define (τ-match ty)
-; (or (match-type ty tycon pat-class)
-; ;; error msg should go in specific macro def?
-; (type-error #:src ty
-; #:msg "Expected type with pattern: ~a, got: ~a"
-; (quote-syntax (τ . pat)) ty)))
-; ; predicate version of τ-match
-; (define (τ? ty) (match-type ty tycon pat-class))
-; ;; expression version of τ-match
-; (define (τ-match+erase e)
-; (syntax-parse (infer+erase e)
-; [(e- ty)
-; #:with τ_matched/#f (match-type #'ty tycon pat-class)
-; #:fail-unless (syntax-e #'τ_matched/#f)
-; (format
-; "~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
-; (syntax-source e) (syntax-line e) (syntax-column e)
-; (syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
-; #'(e- τ_matched/#f)]))
-; ;; get syntax bound to specific pat var (as declared in def-tycon)
-; (define-syntax (τ-get stx)
-; (syntax-parse stx #:datum-literals (from)
-; [(_ attr from ty)
-; #:with args (generate-temporary)
-; #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
-; #:with the-pat (quote-syntax (τ . pat))
-; #'(syntax-parse #'ty ;((current-type-eval) #'ty)
-; [typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
-; #:fail-unless (τ? #'typ)
-; (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
-; (syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ)
-; (type->str (quote-syntax the-pat)) (type->str #'typ))
-; #:with ((~literal #%plain-type)
-; ((~literal #%plain-lambda) tvs
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) f . args)))))
-; ((current-type-eval) #'typ)
-; #:declare args pat-class ; check shape of arguments
-;; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match
-;; (format "Type error: expected ~a type, got ~a"
-;; (type->str #'τ) (type->str #'ty))
-; (attribute args.attr)])])))
-; (define tycon (λ _ (raise (exn:fail:type:runtime
-; (format "~a: Cannot use type at run time" 'τ)
-; (current-continuation-marks)))))
-; (define-syntax (τ stx)
-; (syntax-parse stx #:literals (lit ...)
-; [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
-; (~seq #:bind (~and bvs (bvs-pat.x ...)))))
-; . (~and pat ~! args)) ; first check shape
-; #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
-; [(attribute bvs) #'bvs]
-; [else null])
-; ; this inner syntax-parse gets the ~! to register
-; ; otherwise, apparently #:declare's get subst into pat (before ~!)
-; (syntax-parse #'args #:literals (lit ...)
-; [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
-; #'(#%type
-; (λ (tv (... ...)) ;(bvs.x (... ...))
-;; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
-; (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
-; (tycon . args))))])]
-; [_
-; #:with expected-pat
-; #,(if (attribute bvs-test)
-; #'(quote-syntax (τ bvs-pat.stx . pat))
-; #'(quote-syntax (τ . pat)))
-; (type-error #:src stx
-; #:msg (string-append
-; "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
-; #;(format
-; "where: ~a"
-; (string-join
-; (stx-map
-; (λ (typ clss) (format "~a is a ~a" typ clss))
-; #'(ty (... ...)) #'(cls (... ...)))
-; ", ")))
-; #'τ stx #'expected-pat)])))]))
-
-; define-type-constructor, archied 2015-08-12
-;(define-syntax define-type-constructor
-; (syntax-parser
-; [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
-; #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
-; . pat)
-; ; lits must have ~ prefix (for syntax-parse compat) for now
-; (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
-; decls ...
-; #;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
-; #:defaults ([(tvar 1) null][(cls 1) null])))
-; #:with τ-match (format-id #'τ "~a-match" #'τ)
-; #:with τ? (format-id #'τ "~a?" #'τ)
-; #:with τ-get (format-id #'τ "~a-get" #'τ)
-; #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
-; #:with τ-expander (format-id #'τ "~~~a" #'τ)
-; #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
-; #:with pat-class (generate-temporary #'τ) ; syntax-class name
-; #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
-; #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
-; #`(begin
-; ;; list can't be function, ow it will use typed #%app
-; ;; define lit as macro that expands into #%app,
-; ;; so it will use the #%app here (racket's #%app)
-; (define lit-tmp void) ...
-; (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
-; (provide lit ...)
-; (provide τ (for-syntax τ-expander τ-expander*))
-; (begin-for-syntax
-; #;(define-syntax lit
-; (pattern-expander
-; (syntax-parser
-; [(_ . xs)
-; #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
-; ; the ~τ pattern backtracks normally;
-; ; the ~τ* version errors immediately for a non-match
-; (define-syntax τ-expander
-; (pattern-expander
-; (syntax-parser
-; [(_ (~optional
-; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
-; . match-pat)
-; ;; manually replace literals with expanded form, to get around ~ restriction
-; #:with new-match-pat
-; #`#,(subst-datum-lits
-; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
-; #'(lit ...)
-; #'match-pat)
-; #'((~literal #%plain-type)
-; ((~literal #%plain-lambda) (bvs.x (... ...))
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
-; (define-syntax τ-expander*
-; (pattern-expander
-; (syntax-parser
-; [(_ (~optional
-; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
-; . match-pat)
-; #:with pat-from-constructor
-; #,(if (attribute bvs-test)
-; #'(quote-syntax (τ bvs-pat.stx . pat))
-; #'(quote-syntax (τ . pat)))
-; ;; manually replace literals with expanded form, to get around ~ restriction
-; #:with new-match-pat
-; #`#,(subst-datum-lits
-; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
-; #'(lit ...)
-; #'match-pat)
-; #'(~and
-; (~or
-; ((~literal #%plain-type)
-; ((~literal #%plain-lambda) (bvs.x (... ...))
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
-; (~and any
-; (~do
-; (type-error #:src #'any
-; #:msg
-; "Expected type of expression to match pattern ~a, got: ~a"
-; (quote-syntax pat-from-constructor) #'any))))
-; ~!)])))
-; (define-syntax-class pat-class
-; ;; dont check is-type? here; should already be types
-; ;; only check is-type? for user-entered types, eg tycon call
-; ;; thus, dont include decls here, only want shape
-; ; uses "lit" pattern expander
-; (pattern pat))
-; (define (τ-match ty)
-; (or (match-type ty tycon pat-class)
-; ;; error msg should go in specific macro def?
-; (type-error #:src ty
-; #:msg "Expected type with pattern: ~a, got: ~a"
-; (quote-syntax (τ . pat)) ty)))
-; ; predicate version of τ-match
-; (define (τ? ty) (match-type ty tycon pat-class))
-; ;; expression version of τ-match
-; (define (τ-match+erase e)
-; (syntax-parse (infer+erase e)
-; [(e- ty)
-; #:with τ_matched/#f (match-type #'ty tycon pat-class)
-; #:fail-unless (syntax-e #'τ_matched/#f)
-; (format
-; "~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
-; (syntax-source e) (syntax-line e) (syntax-column e)
-; (syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
-; #'(e- τ_matched/#f)]))
-; ;; get syntax bound to specific pat var (as declared in def-tycon)
-; (define-syntax (τ-get stx)
-; (syntax-parse stx #:datum-literals (from)
-; [(_ attr from ty)
-; #:with args (generate-temporary)
-; #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
-; #:with the-pat (quote-syntax (τ . pat))
-; #'(syntax-parse #'ty ;((current-type-eval) #'ty)
-; [typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
-; #:fail-unless (τ? #'typ)
-; (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
-; (syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ)
-; (type->str (quote-syntax the-pat)) (type->str #'typ))
-; #:with ((~literal #%plain-type)
-; ((~literal #%plain-lambda) tvs
-; ((~literal let-values) () ((~literal let-values) ()
-; ((~literal #%plain-app) f . args)))))
-; ((current-type-eval) #'typ)
-; #:declare args pat-class ; check shape of arguments
-;; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match
-;; (format "Type error: expected ~a type, got ~a"
-;; (type->str #'τ) (type->str #'ty))
-; (attribute args.attr)])])))
-; (define tycon (λ _ (raise (exn:fail:type:runtime
-; (format "~a: Cannot use type at run time" 'τ)
-; (current-continuation-marks)))))
-; (define-syntax (τ stx)
-; (syntax-parse stx #:literals (lit ...)
-; [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
-; (~seq #:bind (~and bvs (bvs-pat.x ...)))))
-; . (~and pat ~! args)) ; first check shape
-; #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
-; [(attribute bvs) #'bvs]
-; [else null])
-; ; this inner syntax-parse gets the ~! to register
-; ; otherwise, apparently #:declare's get subst into pat (before ~!)
-; (syntax-parse #'args #:literals (lit ...)
-; [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
-; #'(#%type
-; (λ (tv (... ...)) ;(bvs.x (... ...))
-;; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
-; (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
-; (tycon . args))))])]
-; [_
-; #:with expected-pat
-; #,(if (attribute bvs-test)
-; #'(quote-syntax (τ bvs-pat.stx . pat))
-; #'(quote-syntax (τ . pat)))
-; (type-error #:src stx
-; #:msg (string-append
-; "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
-; #;(format
-; "where: ~a"
-; (string-join
-; (stx-map
-; (λ (typ clss) (format "~a is a ~a" typ clss))
-; #'(ty (... ...)) #'(cls (... ...)))
-; ", ")))
-; #'τ stx #'expected-pat)])))]))
-
-
-;; TODO: refine this to enable specifying arity information
-;; type constructors currently must have 1+ arguments
-;#;(define-syntax (define-type-constructor stx)
-; (syntax-parse stx
-; [(_ τ:id (~optional (~seq #:arity n:exact-positive-integer)))
-; #:with τ? (format-id #'τ "~a?" #'τ)
-; #:with τ-ref (format-id #'τ "~a-ref" #'τ)
-; #:with τ-num-args (format-id #'τ "~a-num-args" #'τ)
-; #:with τ-args (format-id #'τ "~a-args" #'τ)
-; #:with τ-match (format-id #'τ "~a-match" #'τ)
-; #:with tmp (generate-temporary #'τ)
-; #`(begin
-; ;; TODO: define syntax class instead of these separate tycon fns
-; (provide τ (for-syntax τ? τ-ref τ-num-args τ-args))
-; (define tmp (λ _ (raise (exn:fail:type:runtime
-; (format "~a: Cannot use type at run time" 'τ)
-; (current-continuation-marks)))))
-; (define-syntax (τ stx)
-; (syntax-parse stx
-; [x:id
-; (type-error #:src #'x
-; #:msg "Cannot use type constructor ~a in non-application position"
-; #'τ)]
-; [(_) ; default tycon requires 1+ args
-; #:when (not #,(attribute n))
-; (type-error #:src stx
-; #:msg "Type constructor must have at least 1 argument.")]
-; [(_ x (... ...))
-; #:when #,(and (attribute n)
-; #'(not (= n (stx-length #'(x (... ...))))))
-; #:with m #,(and (attribute n) #'n)
-; (type-error #:src stx
-; #:msg "Type constructor ~a expected ~a argument(s), given: ~a"
-; #'τ #'m #'(x (... ...)))]
-; ; this is racket's #%app
-; [(_ x (... ...)) #'(tmp x (... ...))]))
-; ; TODO: ok to assume type in canonical (ie, fully expanded) form?
-; ;; yes for now
-; (define-for-syntax (τ? stx)
-; (syntax-parse ((current-promote) stx)
-; [((~literal #%plain-app) tycon τ_arg (... ...)) (typecheck? #'tycon #'tmp)]
-; [_ #f]))
-; (define-for-syntax (τ-ref stx m)
-; (syntax-parse stx
-; [((~literal #%plain-app) tycon τ_arg (... ...))
-; #:when (typecheck? #'tycon #'tmp)
-; (stx-list-ref #'(τ_arg (... ...)) m)]))
-; (define-for-syntax (τ-args stx)
-; (syntax-parse ((current-promote) stx)
-; [((~literal #%plain-app) tycon τ_arg (... ...))
-; #:when (typecheck? #'tycon #'tmp)
-; #'(τ_arg (... ...))]))
-; (define-for-syntax (τ-num-args stx)
-; (syntax-parse stx
-; [((~literal #%plain-app) tycon τ_arg (... ...))
-; #:when (typecheck? #'tycon #'tmp)
-; (stx-length #'(τ_arg (... ...)))])))]))
; examples:
; (define-syntax-category type)
@@ -929,7 +403,6 @@
(pattern τ
#:with norm ((current-type-eval) #'τ)
#:with k (typeof #'norm)
- ;#:fail-unless (#%tag? #'k)
#:fail-unless ((current-is-name?) #'norm)
(format "~a (~a:~a) not a valid ~a: ~a"
(syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
@@ -971,75 +444,8 @@
(define-syntax define-name-cons
(syntax-parser
[(_ (~var x id) . rst) #'(define-basic-checked-stx x : name . rst)])))]))
-;; syntax classes
-(begin-for-syntax
- #;(define-syntax-class type
- ;; τ = surface syntax, as written
- ;; norm = canonical form for the type, ie expanded
- ;; -dont bother to check if type is already expanded, because this class
- ;; typically annotates user-written types
- (pattern τ
-; #:with [norm k] (infer+erase #'τ)
- #:with norm ((current-type-eval) #'τ)
- #:with k (typeof #'norm)
- #:fail-unless (#%type? #'k)
- (format "~a (~a:~a) not a valid type: ~a"
- (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
- (type->str #'τ))))
-
- #;(define-syntax-class typed-binding #:datum-literals (:)
- #:attributes (x τ)
- (pattern [x:id : ~! ty:type] #:attr τ #'ty.norm)
- (pattern any
- #:fail-when #t
- (format
- (string-append
- "Improperly formatted type annotation: ~a; should have shape [x : τ], "
- "where τ is a valid type.")
- (type->str #'any))
- #:attr x #f #:attr τ #f))
-
- (define (brace? stx)
- (define paren-shape/#f (syntax-property stx 'paren-shape))
- (and paren-shape/#f (char=? paren-shape/#f #\{)))
- #;(define-syntax-class ann ; type instantiation
- #:attributes (τ norm)
- (pattern stx
- #:when (stx-pair? #'stx)
- #:when (brace? #'stx)
- #:with (τ:type) #'stx
- #:attr norm (delay #'τ.norm))
- (pattern any
- #:fail-when #t
- (format
- (string-append
- "Improperly formatted type annotation: ~a; should have shape {τ}, "
- "where τ is a valid type.")
- (type->str #'any))
- #:attr τ #f #:attr norm #f)))
-
-
-
-#;(define-syntax (define-primop stx)
- (syntax-parse stx #:datum-literals (:)
- [(_ op:id : τ (~optional (~seq : k) #:defaults ([k #'#%type])))
- #:with kind ((current-type-eval) #'k)
- #:with τ+ ((current-type-eval) #'τ)
- #:with k_τ (typeof #'τ+)
- #:when (typecheck? #'k_τ #'kind)
- #:with op/tc (generate-temporary #'op)
- #`(begin
- (provide (rename-out [op/tc op]))
- (define-syntax (op/tc stx)
- (syntax-parse stx
- [f:id (assign-type (syntax/loc stx op) #'τ)] ; HO case
- [(_ x (... ...))
- #:with app (datum->syntax stx '#%app)
- #:with op (format-id stx "~a" #'op)
- (syntax/loc stx (app op x (... ...)))])))]))
-
-;(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
+; substitution
(begin-for-syntax
; subst τ for y in e, if (bound-id=? x y)
(define (subst τ x e)
@@ -1051,56 +457,4 @@
[_ e]))
(define (substs τs xs e)
- (stx-fold subst e τs xs))
-
- ; subst τ for y in e, if (equal? (syntax-e x) (syntax-e y))
- #;(define-for-syntax (subst-datum-lit τ x e)
- (syntax-parse e
- [y:id #:when (equal? (syntax-e e) (syntax-e x)) τ]
- [(esub ...)
- #:with (esub_subst ...) (stx-map (λ (e1) (subst-datum-lit τ x e1)) #'(esub ...))
- (syntax-track-origin #'(esub_subst ...) e x)]
- [_ e]))
-
- #;(define-for-syntax (subst-datum-lits τs xs e)
- (stx-fold subst-datum-lit e τs xs)))
-
-
-;; type environment -----------------------------------------------------------
-#;(begin-for-syntax
-
- ;; A Variable is a Symbol
- ;; A TypeEnv is a [HashOf Variable => Type]
-
- ;; base-type-env : TypeEnv
- ;; Γ : [ParameterOf TypeEnv]
- ;; The keys represent variables and the values are their types.
- ;; NOTE: I can't use a free-id-table because a variable must be in the table
- ;; before expanding (ie type checking) a λ body, so the vars in the body won't
- ;; be free-id=? to the ones in the table.
- ;; Using symbols instead of ids should be fine because I'm manually managing
- ;; the entire environment, and the surface language has no macros so I know
- ;; all the binding forms ahead of time.
- (define base-type-env (hash))
- (define Γ (make-parameter base-type-env))
-
- ;; type-env-lookup : Syntax -> Type
- ;; Returns the type of the input identifier, according to Γ.
- (define (type-env-lookup x)
- (hash-ref (Γ) (syntax->datum x)
- (λ () (type-error #:src x
- #:msg "Could not find type for variable ~a" x))))
-
- ;; type-env-extend : #'((x τ) ...) -> TypeEnv
- ;; Returns a TypeEnv 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)))
-
- ;; with-extended-type-env : #'((x τ) ...) Syntax ->
- ;; Must be macro because type env must be extended before expanding the body e.
- (define-syntax (with-extended-type-env stx)
- (syntax-parse stx
- [(_ x-τs e)
- #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
+ (stx-fold subst e τs xs)))
