diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt index 7cf1d36..7a666e3 100644 --- a/macrotypes/examples/fomega.rkt +++ b/macrotypes/examples/fomega.rkt @@ -1,54 +1,31 @@ #lang s-exp macrotypes/typecheck -(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst) -(reuse String #%datum #:from "stlc+reco+var.rkt") +(reuse λ #%app Int → + #:from "sysf.rkt") +(reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt") ;; System F_omega -;; Type relation: ;; Types: -;; - types from sysf.rkt -;; - String from stlc+reco+var +;; - redefine ∀ +;; - extend kind? and kind=? to include #%type +;; - extend sysf with tyλ and tyapp ;; Terms: -;; - extend ∀ Λ inst from sysf -;; - add tyλ and tyapp -;; - #%datum from stlc+reco+var +;; - extend sysf with Λ inst -(provide (for-syntax current-kind?) - define-type-alias - (type-out ★ ⇒ ∀★ ∀) - Λ inst tyλ tyapp) +(provide (type-out ∀) (kind-out ★ ⇒ ∀★ ∀) Λ inst tyλ tyapp) (define-syntax-category :: kind) -; want #%type to be equiv to★ -; => edit current-kind? so existing #%type annotations (with no #%kind tag) -; are treated as kinds -; <= define ★ as rename-transformer expanding to #%type +;; want #%type to be equiv to ★ +;; => extend current-kind? to recognize #%type +;; <= define ★ as rename-transformer expanding to #%type (begin-for-syntax (current-kind? (λ (k) (or (#%type? k) (kind? 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)) + ;; well-formed types, ie not types with ⇒ kind (current-type? (λ (t) (define k (kindof t)) - #;(or (type? t) (★? (typeof t)) (∀★? (typeof t))) (and k ((current-kind?) k) (not (⇒? k))))) - ;; o.w., a valid type is one with any valid kind + ;; any valid type (includes ⇒-kinded types) (current-any-type? (λ (t) (define k (kindof t)) (and k ((current-kind?) k))))) - -; must override, to handle kinds -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ) - #:with (τ- k_τ) (infer+erase #'τ #:tag '::) - #:fail-unless ((current-kind?) #'k_τ) - (format "not a valid type: ~a\n" (type->str #'τ)) - #'(define-syntax alias - (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) - (begin-for-syntax (define ★? #%type?) (define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder @@ -59,7 +36,7 @@ (define-binding-type ∀ #:arr ∀★) ;; alternative: normalize before type=? -; but then also need to normalize in current-promote +;; but then also need to normalize in current-promote? (begin-for-syntax (define (normalize τ) (syntax-parse τ #:literals (#%plain-app #%plain-lambda) @@ -82,7 +59,6 @@ (define old-eval (current-type-eval)) (define (type-eval τ) (normalize (old-eval τ))) (current-type-eval type-eval) - (current-ev type-eval) (define old-type=? (current-type=?)) ; ty=? == syntax eq and syntax prop eq @@ -91,9 +67,7 @@ (and (or (and (not k1) (not k2)) (and k1 k2 ((current-kind=?) k1 k2))) (old-type=? t1 t2)))) - (current-type=? type=?) - (current-typecheck-relation type=?) - (current-check-relation type=?)) + (current-typecheck-relation type=?)) (define-typed-syntax Λ [(_ bvs:kind-ctx e) @@ -120,7 +94,7 @@ #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:tag '::) #:fail-unless ((current-kind?) #'k_body) (format "not a valid type: ~a\n" (type->str #'τ_body)) - (⊢ (λ- tvs- τ_body-) :: (⇒ bvs.kind ... k_body))]) + (assign-kind #'(λ- tvs- τ_body-) #'(⇒ bvs.kind ... k_body))]) (define-typed-syntax tyapp [(_ τ_fn τ_arg ...) @@ -142,4 +116,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)]) + (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)]) diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt index 88341c9..12f017c 100644 --- a/macrotypes/examples/fomega2.rkt +++ b/macrotypes/examples/fomega2.rkt @@ -1,8 +1,10 @@ #lang s-exp macrotypes/typecheck -(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst λ #%app →) -(reuse String #%datum #:from "stlc+reco+var.rkt") +(reuse Int + #:from "sysf.rkt") +(require (prefix-in sysf: (only-in "sysf.rkt" →- → #%app λ)) + (only-in "sysf.rkt" ~→ →?)) +(reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt") -; same as fomega.rkt except here λ and #%app works as both type and terms +; same as fomega.rkt except λ and #%app works as both type and terms, ; - uses definition from stlc, but tweaks type? and kind? predicates ;; → is also both type and kind @@ -15,9 +17,7 @@ ;; - extend ∀ Λ inst from sysf ;; - #%datum from stlc+reco+var -(provide define-type-alias - ★ ∀★ ∀ → - λ #%app Λ inst +(provide (kind-out ★ ∀★) (type-out ∀) → λ #%app Λ inst (for-syntax current-kind-eval kindcheck?)) (define-syntax-category :: kind) @@ -36,14 +36,6 @@ (current-any-type? (λ (t) (define k (kindof t)) (and k ((current-kind?) k))))) -; must override -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ) - #:with (τ- _) (infer+erase #'τ #:tag '::) - #'(define-syntax alias - (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) - ;; extend → to serve as both type and kind (define-syntax (→ stx) (syntax-parse stx @@ -78,20 +70,17 @@ (define old-eval (current-type-eval)) (define (type-eval τ) (normalize (old-eval τ))) (current-type-eval type-eval) - (current-ev type-eval) - (define old-type=? (current-type=?)) - (define (type=? t1 t2) + (define old-typecheck? (current-typecheck-relation)) + (define (new-typecheck? t1 t2) (syntax-parse (list t1 t2) #:datum-literals (:) [((~∀ ([tv1 : k1]) tbody1) (~∀ ([tv2 : k2]) tbody2)) - ((current-kind=?) #'k1 #'k2)] - [_ (old-type=? t1 t2)])) - (current-type=? type=?) - (current=? type=?) - (current-typecheck-relation type=?) - (current-check-relation type=?) + (and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))] + [_ (old-typecheck? t1 t2)])) + (current-typecheck-relation new-typecheck?) + ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind= (define old-kind=? (current-kind=?)) (define (new-kind=? k1 k2) (or (and (★? k1) (#%type? k2)) @@ -102,8 +91,7 @@ (define-typed-syntax Λ [(_ bvs:kind-ctx e) - #:with ((tv- ...) e- τ_e) - (infer/ctx+erase #'bvs #'e) + #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))]) (define-typed-syntax inst @@ -124,7 +112,7 @@ (define-typed-syntax λ [(_ bvs:kind-ctx τ) ; type #:with (Xs- τ- k_res) (infer/ctx+erase #'bvs #'τ #:tag '::) - (⊢ (λ- Xs- τ-) :: (→ bvs.kind ... k_res))] + (assign-kind #'(λ- Xs- τ-) #'(→ bvs.kind ... k_res))] [(_ . rst) #'(sysf:λ . rst)]) ; term ;; extend #%app to also work as a type @@ -150,5 +138,5 @@ (format "Expected: ~a arguments with type(s): " (stx-length #'(k_in ...))) (string-join (stx-map type->str #'(k_in ...)) ", ")) - (⊢ (#%app- τ_fn- τ_arg- ...) :: k_out)] + (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)] [(_ . rst) #'(sysf:#%app . rst)]) ; term diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt index 0108259..9e9324e 100644 --- a/macrotypes/examples/mlish+adhoc.rkt +++ b/macrotypes/examples/mlish+adhoc.rkt @@ -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 (mk-type #'X))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt index 8e9232b..6eb1b34 100644 --- a/macrotypes/examples/mlish.rkt +++ b/macrotypes/examples/mlish.rkt @@ -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 (mk-type #'X))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map diff --git a/macrotypes/examples/stlc+occurrence.rkt b/macrotypes/examples/stlc+occurrence.rkt index 4e9adff..298262c 100644 --- a/macrotypes/examples/stlc+occurrence.rkt +++ b/macrotypes/examples/stlc+occurrence.rkt @@ -135,8 +135,7 @@ (τ-eval τ)] [_ (τ-eval τ-stx)])))) - (current-type-eval ∪-eval) - (current-ev ∪-eval)) + (current-type-eval ∪-eval)) ;; ----------------------------------------------------------------------------- ;; --- Subtyping diff --git a/macrotypes/info.rkt b/macrotypes/info.rkt index 4b479dd..3b22751 100644 --- a/macrotypes/info.rkt +++ b/macrotypes/info.rkt @@ -9,7 +9,7 @@ (define test-omit-paths '("examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp - "examples/tests/fomega3.rkt" + "examples/fomega3.rkt" "examples/tests/fomega3-tests.rkt" "examples/tests/mlish/bg/README.md")) diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt index 2a4624c..9666663 100644 --- a/macrotypes/stx-utils.rkt +++ b/macrotypes/stx-utils.rkt @@ -88,6 +88,27 @@ (define (generate-temporariesss stx) (stx-map generate-temporariess stx)) +;; stx prop helpers + +;; ca*r : Any -> Any +(define (ca*r v) + (if (cons? v) (ca*r (car v)) v)) +;; cd*r : Any -> Any +(define (cd*r v) + (if (cons? v) (cd*r (cdr v)) v)) + +;; get-stx-prop/ca*r : Syntax Key -> Val +;; Retrieves Val at Key stx prop on Stx. +;; If Val is a non-empty list, continue down head until non-list. +(define (get-stx-prop/ca*r stx tag) + (ca*r (syntax-property stx tag))) + +;; get-stx-prop/cd*r : Syntax Key -> Val +(define (get-stx-prop/cd*r stx tag) + (cd*r (syntax-property stx tag))) + + + ;; transfers properties and src loc from orig to new (define (transfer-stx-props new orig #:ctx [ctx new]) (datum->syntax ctx (syntax-e new) orig orig)) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 3b31555..1d22d43 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -42,10 +42,11 @@ ;; - To typecheck a surface form, it local-expands each subterm in order to get ;; their types. ;; - With this typechecking strategy, the typechecking implementation machinery -;; is easily inserted into each #%- form +;; is easily inserted into each #%XYZ form ;; - A base type is just a Racket identifier, so type equality, even with ;; aliasing, is just free-identifier=? ;; - type constructors are prefix +;; - use different stx prop keys for different metadata, eg ':: for kinds ;; redefine #%module-begin to add some provides (provide (rename-out [mb #%module-begin])) @@ -54,7 +55,7 @@ [(_ . stuff) (syntax/loc this-syntax (#%module-begin - ; provide some useful racket forms + ; auto-provide some useful racket forms (provide #%module-begin #%top-interaction #%top require only-in) . stuff))])) @@ -77,7 +78,9 @@ (path->string (path-replace-suffix (file-name-from-path f) ""))) (define-syntax-parameter stx (syntax-rules ()))) -;; non-turnstile +;; non-Turnstile define-typed-syntax +;; TODO: potentially confusing? get rid of this? +;; - but it will be annoying since the `stx` stx-param is used everywhere (define-syntax (define-typed-syntax stx) (syntax-parse stx [(_ name:id stx-parse-clause ...+) @@ -190,38 +193,31 @@ (begin-for-syntax ;; Helper functions for attaching/detaching types, kinds, etc. - ;; get-stx-prop/car : Stx Key -> Val - ;; Retrieves Val at Key stx prop on Stx. - ;; 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)) - (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. - ;; Define new kinds of metadata with `define-syntax-category` + ;; Define new metadata via `define-syntax-category` ;; attach : Stx Tag Val -> Stx ;; Adds Tag+Val to Stx as stx prop, returns new Stx. ;; e.g., Stx = expression, Tag = ':, Val = Type stx - (define (attach stx tag v #:eval [eval (λ (x) x)]) - (set-stx-prop/preserved stx tag (eval v))) + (define (attach stx tag v) + (set-stx-prop/preserved stx tag v)) ;; detach : Stx Tag -> Val ;; Retrieves Val at Tag stx prop on Stx. ;; If Val is a non-empty list, return first element, otherwise return Val. ;; e.g., Stx = expression, Tag = ':, Val = Type stx (define (detach stx tag) -; (or - (get-stx-prop/car stx tag) -; (error 'detach "~a has no ~a prop" (stx->datum stx) tag)) - )) + (get-stx-prop/ca*r stx tag))) ;; ---------------------------------------------------------------------------- -;; define-syntax-category ------------------------------------------------------ +;; ---------------------------------------------------------------------------- +;; define-syntax-category ----------------------------------------------------- +;; ---------------------------------------------------------------------------- +;; ---------------------------------------------------------------------------- -;; Defines a new type of metadata on syntax, e.g. types, as well as functions -;; and macros for manipulating the metadata. +;; This is a huge macro. +;; Defines a new type of metadata on syntax, e.g. types, and functions +;; and macros for manipulating the metadata, e.g. define-base-type, type=?, etc ;; A syntax category requires a name and two keys, ;; - one to use when attaching values of this category (eg ': for types) @@ -229,7 +225,7 @@ ;; If key1 is unspecified, the default is ': ;; If key2 is unspecified, the default is "twice" key1 (ie '::) ;; -;; examples uses: +;; example uses: ;; (define-syntax-category type) ;; (define-syntax-category : type) ;; (define-syntax-category : type ::) @@ -237,8 +233,8 @@ ;; ;; CODE NOTE: ;; To make this large macros-defining macro easier to read, -;; I define a `type` patvar corresponding to the category name, -;; and a `kind` patvar for its "type". +;; I use a `type` pat var corresponding to the category name, +;; and a `kind` pat var for its "type". ;; But `name` could correspond to any kind of metadata, ;; e.g., kinds, src locs, polymorphic bounds (define-syntax (define-syntax-category stx) @@ -249,7 +245,7 @@ #`(define-syntax-category key name #,(mkx2 #'key))] [(_ key1:id name:id key2:id) ;; syntax classes - #:with type #'name ; dangerous, check `type` not used in binding pos below + #:with type #'name ; dangerous? check `type` not used in binding pos below #:with any-type (format-id #'name "any-~a" #'name) #:with type-ctx (format-id #'name "~a-ctx" #'name) #:with type-bind (format-id #'name "~a-bind" #'name) @@ -305,7 +301,7 @@ (define (type-key2) 'key2) (define (typeof stx) (detach stx 'key1)) (define (tagoftype stx) (detach stx 'key2)) ; = kindof if kind stx-cat defined - (define (fast-assign-type e τ) + (define (fast-assign-type e τ) ; TODO: does this actually help? (attach e 'key1 (syntax-local-introduce τ))) (define (assign-type e τ) (fast-assign-type e ((current-type-eval) τ))) @@ -357,8 +353,8 @@ #:attr norm #f)) ;; checking types (define (type=? t1 t2) - ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1)) - ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2)) + ;; (printf "(τ=) t1 = ~a\n" #;τ1 (stx->datum t1)) + ;; (printf "(τ=) t2 = ~a\n" #;τ2 (stx->datum t2)) (or (and (id? t1) (id? t2) (free-id=? t1 t2)) (and (stx-null? t1) (stx-null? t2)) (syntax-parse (list t1 t2) ; handle binding types @@ -376,7 +372,7 @@ (define (types=? τs1 τs2) (and (stx-length=? τs1 τs2) (stx-andmap (current-type=?) τs1 τs2))) - ; extra indirection, enables easily overriding type=? with sub? + ; extra indirection, enables easily overriding type=? with eg sub? ; to add subtyping, without changing any other definitions (define current-typecheck-relation (make-parameter type=?)) ;; convenience fns for current-typecheck-relation @@ -399,8 +395,9 @@ ;; and type application (define (default-type-eval τ) ; TODO: optimization: don't expand if expanded - ; currently, this causes problems when - ; combining unexpanded and expanded types to create new types + ; - but this causes problems when combining unexpanded and + ; expanded types to create new types + ; - alternative: use syntax-local-expand-expression? (add-orig (expand/df τ) τ)) (define current-type-eval (make-parameter default-type-eval)) (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))) @@ -454,7 +451,7 @@ (add-orig (attach (syntax/loc this-syntax (τ-internal)) - 'new-key2 ((current-type-eval) #'new-#%tag)) + 'new-key2 (expand/df #'new-#%tag)) #'τ)])))])) (define-syntax define-base-types (syntax-parser @@ -698,7 +695,7 @@ #'(kindcon k_arg (... (... ...))) #'#%tag) (add-orig - (attach #'(τ- bvs- . τs-) 'key2 ((current-type-eval) #'k_result)) + (attach #'(τ- bvs- . τs-) 'key2 (default-type-eval #'k_result)) stx)] [_ (type-error #:src stx @@ -707,15 +704,17 @@ "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") #'τ stx #'op #'n)])))])))])) -;; end define-syntax-category ------------------------------------------------- +;; ---------------------------------------------------------------------------- +;; ---------------------------------------------------------------------------- +;; end of define-syntax-category ---------------------------------------------- +;; ---------------------------------------------------------------------------- ;; ---------------------------------------------------------------------------- ;; pre-declare all type-related functions and forms (define-syntax-category type) ;; generic, type-agnostic parameters -;; Use these for code that is generic over types and kinds -;; TODO: need an easier way to update all relevant params at once +;; Use in code that is generic over types and kinds, e.g., in #lang Turnstile (begin-for-syntax (define current=? (make-parameter (current-type=?))) (define (=s? xs1 xs2) ; map current=? pairwise over lists @@ -734,14 +733,14 @@ ;; type assignment utilities -------------------------------------------------- (begin-for-syntax - ;; Type assignment macro for nicer syntax + ;; Type assignment macro (ie assign-type) for nicer syntax (define-syntax (⊢ stx) (syntax-parse stx - [(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))] + [(_ e tag τ) #'(assign-type #`e #`τ)] [(_ e τ) #'(⊢ e : τ)])) (define-syntax (⊢/no-teval stx) (syntax-parse stx - [(_ e tag τ) #'(attach #`e 'tag ((current-ev) #`τ))] + [(_ e tag τ) #'(fast-assign-type #`e #`τ)] [(_ e τ) #'(⊢/no-teval e : τ)])) ;; Actual type assignment function. @@ -774,14 +773,7 @@ (define v (syntax-property stx tag)) (if (cons? v) (car v) v)) - ;; get-stx-prop/cd*r : Syntax Any -> Any - (define (get-stx-prop/cd*r stx tag) - (cd*r (syntax-property stx tag))) - - ;; cd*r : Any -> Any - (define (cd*r v) - (if (cons? v) (cd*r (cdr v)) v)) - + (define (mk-tyvar X) (attach X 'tyvar #t)) (define (tyvar? X) (syntax-property X 'tyvar)) (define type-pat "[A-Za-z]+") @@ -859,8 +851,8 @@ ;; basic infer function with no context: ;; infers the type and erases types in an expression - (define (infer+erase e #:tag [tag (current-tag)]) - (define e+ (expand/df e)) + (define (infer+erase e #:tag [tag (current-tag)] #:expa [expa expand/df]) + (define e+ (expa e)) (list e+ (detach e+ tag))) ;; infers the types and erases types in multiple expressions (define (infers+erase es #:tag [tag (current-tag)]) @@ -870,7 +862,15 @@ ;; It should be named infer+erase but leaving it for now for backward compat. ;; ctx = vars and their types (or other props, denoted with "sep") ;; tvctx = tyvars and their kinds - (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag (current-tag)]) + ;; TODO: infer currently tries to be generic over types and kinds + ;; but I'm not sure it properly generalizes + ;; eg, what if I need separate type-eval and kind-eval fns? + ;; - should infer be moved into define-syntax-category? + (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] + #:tag [tag (current-tag)] ; the "type" to return from es + #:expa [expa expand/df] ; used to expand e + #:tev [tev #'(current-type-eval)] ; type-eval (τ in ctx) + #:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx) (syntax-parse ctx [([x sep τ] ...) ; dont expand yet bc τ may have references to tvs #:with ([tv (~seq tvsep:id tvk) ...] ...) tvctx @@ -890,19 +890,18 @@ ((~literal #%plain-lambda) xs+ ((~literal let-values) () ((~literal let-values) () ((~literal #%expression) e+) ... (~literal void)))))))) - (expand/df + (expa #`(λ (tv ...) (let-syntax ([tv (make-rename-transformer - (attach + (mk-tyvar (for/fold ([tv-id #'tv]) - ([s (in-list (list 'tvsep ...))] - [k (in-list (list #'tvk ...))]) - (attach tv-id s ((current-ev) k))) - 'tyvar #t))] ...) + ([s (in-list '(tvsep ...))] + [k (in-stx-list #'(tvk ...))]) + (attach tv-id s (#,kev k)))))] ...) (λ (x ...) - (let-syntax - ([x (make-variable-like-transformer (attach #'x 'sep ((current-ev) #'τ)))] ...) - (#%expression e) ... void))))) + (let-syntax ([x (make-variable-like-transformer + (attach #'x 'sep (#,tev #'τ)))] ...) + (#%expression e) ... void))))) (list #'tvs+ #'xs+ #'(e+ ...) (stx-map (λ (e) (detach e tag)) #'(e+ ...)))] diff --git a/turnstile/examples/fomega-no-reuse-old.rkt b/turnstile/examples/fomega-no-reuse-old.rkt index 218f590..62bb896 100644 --- a/turnstile/examples/fomega-no-reuse-old.rkt +++ b/turnstile/examples/fomega-no-reuse-old.rkt @@ -9,6 +9,8 @@ ;; this version still uses ': key for kinds +;; tyλ and λ are separate forms + (provide define-type-alias ★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp (typed-out [+ : (→ Int Int Int)]) @@ -49,7 +51,6 @@ [_ τ])) (define old-eval (current-type-eval)) (current-type-eval (lambda (τ) (normalize (old-eval τ)))) - (current-ev (current-type-eval)) (define old-type=? (current-type=?)) ; ty=? == syntax eq and syntax prop eq @@ -61,9 +62,7 @@ (and k1 k2 ((current-kind=?) k1 k2))) (old-type=? t1 t2)))) (current-type=? type=?) - (current-typecheck-relation type=?) - (current=? type=?) - (current-check-relation type=?)) + (current-typecheck-relation type=?)) ;; kinds ---------------------------------------------------------------------- (define-internal-kind-constructor ★) ; defines ★- diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt index 5378c35..46cf2e1 100644 --- a/turnstile/examples/fomega-no-reuse.rkt +++ b/turnstile/examples/fomega-no-reuse.rkt @@ -27,7 +27,8 @@ ;; (need this for define-primop, which still uses type stx-class) (current-type? (λ (t) (★? (kindof t)))) ;; o.w., a valid type is one with any valid kind - (current-any-type? (λ (t) ((current-kind?) (kindof t)))) + (current-any-type? (λ (t) (define k (kindof t)) + (and k ((current-kind?) k)))) ;; TODO: I think this can be simplified (define (normalize τ) @@ -49,21 +50,29 @@ [_ τ])) (define old-eval (current-type-eval)) (current-type-eval (lambda (τ) (normalize (old-eval τ)))) - (current-ev (current-type-eval)) - (define old-type=? (current-type=?)) + ;; (define old-type=? (current-type=?)) + ;; ; ty=? == syntax eq and syntax prop eq + ;; (define (type=? t1 t2) + ;; (let ([k1 (kindof t1)][k2 (kindof t2)]) + ;; ; the extra `and` and `or` clauses are bc type=? is a structural + ;; ; traversal on stx objs, so not all sub stx objs will have a "type"-stx + ;; (and (or (and (not k1) (not k2)) + ;; (and k1 k2 ((current-kind=?) k1 k2))) + ;; (old-type=? t1 t2)))) + ;; (current-type=? type=?) + ;; (current-typecheck-relation type=?)) + (define old-typecheck? (current-typecheck-relation)) ; ty=? == syntax eq and syntax prop eq - (define (type=? t1 t2) + (define (new-typecheck? t1 t2) (let ([k1 (kindof t1)][k2 (kindof t2)]) ; the extra `and` and `or` clauses are bc type=? is a structural ; traversal on stx objs, so not all sub stx objs will have a "type"-stx (and (or (and (not k1) (not k2)) - (and k1 k2 ((current-kind=?) k1 k2))) - (old-type=? t1 t2)))) - (current-type=? type=?) - (current-typecheck-relation type=?) - (current=? type=?) - (current-check-relation type=?)) + (and k1 k2 (kindcheck? k1 k2))) + (old-typecheck? t1 t2)))) +; (current-type=? type=?) + (current-typecheck-relation new-typecheck?)) ;; kinds ---------------------------------------------------------------------- (define-internal-kind-constructor ★) ; defines ★- @@ -166,16 +175,12 @@ ;; TODO: what to do when a def-typed-stx needs both ;; current-typecheck-relation and current-kindcheck-relation -(define-typed-syntax (inst e τ ...) ≫ +(define-typed-syntax (inst e τ:any-type ...) ≫ [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~★ k ...))] - ;; switch to kindcheck? instead of typecheck? - #:do[(define old-check (current-check-relation)) - (current-check-relation (current-kindcheck-relation))] - [⊢ τ ≫ τ- ⇐ :: k] ... - #:do[(current-check-relation old-check)] - ;; #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) - ;; (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) - #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body) +; [⊢ τ ≫ τ- ⇐ :: k] ... ; doesnt work since def-typed-s ⇐ not using kindcheck? + #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) + #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) + (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) -------- - [⊢ e- ⇒ τ-inst]) + [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body)]) diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt index 32f268a..f582d61 100644 --- a/turnstile/examples/fomega.rkt +++ b/turnstile/examples/fomega.rkt @@ -58,7 +58,6 @@ (define old-eval (current-type-eval)) (define (new-type-eval τ) (normalize (old-eval τ))) (current-type-eval new-type-eval) - (current-ev new-type-eval) (define old-type=? (current-type=?)) ;; need to also compare kinds of types @@ -69,20 +68,20 @@ (and (or (and (not k1) (not k2)) (and k1 k2 ((current-kind=?) k1 k2))) (old-type=? t1 t2)))) - (current-type=? new-type=?) - (current-typecheck-relation new-type=?) - (current-check-relation new-type=?)) + (current-typecheck-relation new-type=?)) (define-typed-syntax (Λ bvs:kind-ctx e) ≫ [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e] -------- [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)]) +;; τ.norm invokes current-type-eval while "≫ τ-" uses only local-expand +;; (via infer fn) (define-typed-syntax (inst e τ:any-type ...) ≫ [⊢ e ≫ e- ⇒ (~∀ tvs τ_body) (⇒ :: (~∀★ k ...))] [⊢ τ ≫ τ- ⇐ :: k] ... -------- - [⊢ e- ⇒ #,(substs #'(τ- ...) #'tvs #'τ_body)]) + [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]) ;; - see fomega2.rkt for example with no explicit tyλ and tyapp (define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫ diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt index a107a37..5d9d33b 100644 --- a/turnstile/examples/fomega2.rkt +++ b/turnstile/examples/fomega2.rkt @@ -80,28 +80,24 @@ (define old-eval (current-type-eval)) (define (type-eval τ) (normalize (old-eval τ))) (current-type-eval type-eval) - (current-ev type-eval) - (define old-type=? (current-type=?)) - (define (type=? t1 t2) - (syntax-parse (list t1 t2) #:datum-literals (:) - ;; TODO: compare tbody1 and tbody2 - [((~∀ ([tv1 : k1]) tbody1) - (~∀ ([tv2 : k2]) tbody2)) - ((current-kind=?) #'k1 #'k2)] - [_ (old-type=? t1 t2)])) - (current-type=? type=?) - (current=? type=?) - (current-typecheck-relation type=?) - (current-check-relation type=?) - + ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind= (define old-kind=? (current-kind=?)) (define (new-kind=? k1 k2) (or (and (★? k1) (#%type? k2)) ; enables use of existing type defs (and (#%type? k1) (★? k2)) (old-kind=? k1 k2))) (current-kind=? new-kind=?) - (current-kindcheck-relation new-kind=?)) + (current-kindcheck-relation new-kind=?) + + (define old-typecheck? (current-typecheck-relation)) + (define (new-typecheck? t1 t2) + (syntax-parse (list t1 t2) #:datum-literals (:) + [((~∀ ([tv1 : k1]) tbody1) + (~∀ ([tv2 : k2]) tbody2)) + (and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))] + [_ (old-typecheck? t1 t2)])) + (current-typecheck-relation new-typecheck?)) (define-typed-syntax (Λ bvs:kind-ctx e) ≫ [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e] @@ -110,36 +106,28 @@ (define-typed-syntax (inst e τ:any-type ...) ≫ [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))] - #:do[(define old-check (current-check-relation)) - (current-check-relation new-kind=?)] - [⊢ τ ≫ τ- ⇐ :: k] ... - #:do[(current-check-relation old-check)] - #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body) +; [⊢ τ ≫ τ- ⇐ :: k] ... ; doesnt work since def-typed-s ⇐ not using kindcheck? + #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) + #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) + (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) -------- - [⊢ e- ⇒ τ-inst]) + [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body)]) ;; extend λ to also work as a type -;; must be define-typed-syntax because of default case -;; so use explicit tag in first case -(define-typed-syntax λ - [(_ bvs:kind-ctx τ) ≫ ; type - [[bvs.x ≫ X- :: bvs.kind] ... ⊢ τ ≫ τ- ⇒ :: k_res] +(define-kinded-syntax λ + [(_ bvs:kind-ctx τ) ≫ ; type + [[bvs.x ≫ X- :: bvs.kind] ... ⊢ τ ≫ τ- ⇒ k_res] ------------ - [⊢ (λ- (X- ...) τ-) ⇒ :: (→ bvs.kind ... k_res)]] - [(_ . rst) ≫ - --- [≻ (sysf:λ . rst)]]) ; term + [⊢ (λ- (X- ...) τ-) ⇒ (→ bvs.kind ... k_res)]] + [(_ . rst) ≫ --- [≻ (sysf:λ . rst)]]) ; term ;; extend #%app to also work as a type -(define-typed-syntax #%app - [(_ τ_fn τ_arg ...) ≫ ; type - [⊢ τ_fn ≫ τ_fn- ⇒ :: (~→ k_in ... k_out)] +(define-kinded-syntax #%app + [(_ τ_fn τ_arg ...) ≫ ; type + [⊢ τ_fn ≫ τ_fn- ⇒ (~→ k_in ... k_out)] #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...]) (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...]) - #:do[(define old-check (current-check-relation)) - (current-check-relation new-kind=?)] - [⊢ τ_arg ≫ τ_arg- ⇐ :: k_in] ... - #:do[(current-check-relation old-check)] + [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ... ------------- - [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ :: k_out]] - [(_ . rst) ≫ - --- [≻ (sysf:#%app . rst)]]) ; term + [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out]] + [(_ . rst) ≫ --- [≻ (sysf:#%app . rst)]]) ; term diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index 08d5887..393b76c 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -34,8 +34,7 @@ (define (sub? t1 t2) (stlc:sub? ((current-promote) t1) t2)) (current-sub? sub?) - (current-typecheck-relation sub?) - (current-check-relation sub?)) + (current-typecheck-relation sub?)) ; quasi-kind, but must be type constructor because its arguments are types (define-type-constructor <: #:arity >= 0) diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt index 0d48e54..03d172b 100644 --- a/turnstile/examples/mlish+adhoc.rkt +++ b/turnstile/examples/mlish+adhoc.rkt @@ -338,7 +338,7 @@ -------- [≻ (begin- (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected))) - #,(quasisyntax/loc stx + #,(quasisyntax/loc this-syntax (define- g ;(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]) (liftedλ {Y ...} ([x : τ] ... #:where TC ...) @@ -387,7 +387,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 (mk-type #'X))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map @@ -658,10 +658,10 @@ [⊢ e ≫ e- ⇒ τ_e] #:with ([(~seq p ...) (~datum ->) e_body] ...) #'clauses #:with (pat ...) (stx-map ; use brace to indicate root pattern - (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})])) + (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc this-syntax {pp ...})])) #'((p ...) ...)) #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e) - #:with ty-expected (get-expected-type stx) + #:with ty-expected (get-expected-type this-syntax) [[x ≫ x- : ty] ... ⊢ [(add-expected e_body ty-expected) ≫ e_body- ⇒ ty_body]] ... #:when (check-exhaust #'(pat- ...) #'τ_e) ---- @@ -671,7 +671,7 @@ [(_ e with . clauses) ≫ #:fail-when (null? (syntax->list #'clauses)) "no clauses" [⊢ e ≫ e- ⇒ τ_e] - #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type + #:with t_expect (syntax-property this-syntax 'expected-type) ; propagate inferred type #:with out (cond [(×? #'τ_e) ;; e is tuple @@ -730,7 +730,7 @@ #:with (_ (_ (_ ConsAll) . _) ...) #'info-body #:fail-unless (set=? (syntax->datum #'(Clause ...)) (syntax->datum #'(ConsAll ...))) - (type-error #:src stx + (type-error #:src this-syntax #:msg (string-append "match: clauses not exhaustive; missing: " (string-join @@ -896,7 +896,7 @@ ⇒ (∀ Xs+ (=> TC+ ... (ext-stlc:→ ty+ ... ty-out)))]] [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC #:with (X ...) (compute-tyvars #'(ty ...)) - #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type stx) + #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type this-syntax) -------- [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) (add-expected body body-ty)))]] [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC, ignoring expected-type @@ -904,12 +904,12 @@ -------- [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) body))]] [(_ (x:id ...+) body) ≫ - #:with (~?∀ Xs expected) (get-expected-type stx) + #:with (~?∀ Xs expected) (get-expected-type this-syntax) #:do [(unless (→? #'expected) - (type-error #:src stx #:msg "λ parameters must have type annotations"))] + (type-error #:src this-syntax #:msg "λ parameters must have type annotations"))] #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...]) - (type-error #:src stx #:msg + (type-error #:src this-syntax #:msg (format "expected a function of ~a arguments, got one with ~a arguments" (stx-length #'[arg-ty ...] #'[x ...]))))] -------- @@ -922,10 +922,9 @@ ;; TODO is there a way to have λs that refer to ids defined after them? #'(Λ Xs (ext-stlc:λ x+tys . body))]) - ;; #%app -------------------------------------------------- (define-typed-syntax mlish:#%app #:export-as #%app - [(_ e_fn . e_args) ≫ + [(~and this-app (_ e_fn . e_args)) ≫ ; #:when (printf "app: ~a\n" (syntax->datum #'(e_fn . e_args))) ;; ) compute fn type (ie ∀ and →) [⊢ e_fn ≫ e_fn- ⇒ (~and ty_fn (~∀ Xs ty_fnX))] @@ -939,7 +938,7 @@ (syntax-parse #'(e_args tyX_args) [((e_arg ...) (τ_inX ... _)) #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...)) - (mk-app-err-msg stx #:expected #'(τ_inX ...) + (mk-app-err-msg #'this-app #:expected #'(τ_inX ...) #:note "Wrong number of arguments.") #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args)) #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])] @@ -949,13 +948,13 @@ ;; no typeclasses, duplicate code for now -------------------------------- [(~ext-stlc:→ . tyX_args) ;; ) solve for type variables Xs - (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx)) + (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app)) ;; ) instantiate polymorphic function type (syntax-parse (inst-types/cs #'Xs #'cs #'tyX_args) [(τ_in ... τ_out) ; concrete types ;; ) arity check #:fail-unless (stx-length=? #'(τ_in ...) #'e_args) - (mk-app-err-msg stx #:expected #'(τ_in ...) + (mk-app-err-msg #'this-app #:expected #'(τ_in ...) #:note "Wrong number of arguments.") ;; ) compute argument types; re-use args expanded during solve #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))]) @@ -967,7 +966,7 @@ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...) ;; ) typecheck args #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) - (mk-app-err-msg stx + (mk-app-err-msg #'this-app #:given #'(τ_arg ...) #:expected (stx-map @@ -986,13 +985,13 @@ (syntax-parse #'τ_out [(~?∀ (Y ...) τ_out) (unless (→? #'τ_out) - (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)) + (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn)) #'(∀ (unsolved-X ... Y ...) τ_out)])) (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])] ;; handle type class constraints ---------------------------------------- [(~=> TCX ... (~ext-stlc:→ . tyX_args)) ;; ) solve for type variables Xs - (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx)) + (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app)) ;; ) instantiate polymorphic function type (syntax-parse (inst-types/cs #'Xs #'cs #'((TCX ...) tyX_args)) [((TC ...) (τ_in ... τ_out)) ; concrete types @@ -1005,7 +1004,7 @@ (with-handlers ([exn:fail:syntax:unbound? (lambda (e) - (type-error #:src stx + (type-error #:src #'this-app #:msg (format (string-append @@ -1028,9 +1027,12 @@ (stx-map (lambda (X ty-solved) (string-append (type->str X) " : " (type->str ty-solved))) - #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))]) + #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))] + [(lambda _ #t) + (lambda (e) (displayln "other exn")(displayln e) + (error 'lookup))]) (lookup-op o tys))) - (stx-map (lambda (o) (format-id stx "~a" o #:source stx)) gen-ops) + (stx-map (lambda (o) (format-id #'this-app "~a" o #:source #'this-app)) gen-ops) (stx-map (syntax-parser [(~∀ _ (~ext-stlc:→ ty_in ... _)) #'(ty_in ...)]) @@ -1038,7 +1040,7 @@ #'((generic-op ...) ...) #'((ty-concrete-op ...) ...) #'(TC ...)) ;; ) arity check #:fail-unless (stx-length=? #'(τ_in ...) #'e_args) - (mk-app-err-msg stx #:expected #'(τ_in ...) + (mk-app-err-msg #'this-app #:expected #'(τ_in ...) #:note "Wrong number of arguments.") ;; ) compute argument types; re-use args expanded during solve #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))]) @@ -1050,7 +1052,7 @@ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...) ;; ) typecheck args #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) - (mk-app-err-msg stx + (mk-app-err-msg #'this-app #:given #'(τ_arg ...) #:expected (stx-map @@ -1069,14 +1071,14 @@ (syntax-parse #'τ_out [(~?∀ (Y ...) τ_out) (unless (→? #'τ_out) - (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)) + (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn)) #'(∀ (unsolved-X ... Y ...) τ_out)])) (⊢ ((#%app- e_fn- op ...) e_arg- ...) : τ_out*)])])])]] [(_ e_fn . e_args) ≫ ; err case; e_fn is not a function [⊢ e_fn ≫ e_fn- ⇒ τ_fn] -------- [#:error - (type-error #:src stx + (type-error #:src #'this-app #:msg (format "Expected expression ~a to have → type, got: ~a" (syntax->datum #'e_fn) (type->str #'τ_fn)))]]) @@ -1658,10 +1660,10 @@ [(_ (Name ty ...) [generic-op concrete-op] ...) ≫ [⊢ (Name ty ...) ≫ (~=> TC ... (~TC [generic-op-expected ty-concrete-op-expected] ...)) ⇒ _] - #:when (TCs-exist? #'(TC ...) #:ctx stx) + #:when (TCs-exist? #'(TC ...) #:ctx this-syntax) #:fail-unless (set=? (syntax->datum #'(generic-op ...)) (syntax->datum #'(generic-op-expected ...))) - (type-error #:src stx + (type-error #:src this-syntax #:msg (format "Type class instance ~a incomplete, missing: ~a" (syntax->datum #'(Name ty ...)) (string-join @@ -1719,7 +1721,7 @@ ;; (~TC [generic-op-expected ty-concrete-op-expected] ...))) ;; ⇒ _] ;; #:with Xs+ #'(X- ...) - #:when (TCs-exist? #'(TCsub ...) #:ctx stx) + #:when (TCs-exist? #'(TCsub ...) #:ctx this-syntax) ;; simulate as if the declared concrete-op* has TC ... predicates ;; TODO: fix this manual deconstruction and assembly #:with ((app fa (lam _ ei ty_fn)) ...) #'(ty-concrete-op-expected ...) @@ -1727,7 +1729,7 @@ (stx-map (current-type-eval) #'((app fa (lam Xs+ ei (=> TC+ ... ty_fn))) ...)) #:fail-unless (set=? (syntax->datum #'(generic-op ...)) (syntax->datum #'(generic-op-expected ...))) - (type-error #:src stx + (type-error #:src this-syntax #:msg (format "Type class instance ~a incomplete, missing: ~a" (syntax->datum #'(Name ty ...)) (string-join diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index 9e5a502..bfb4464 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -421,7 +421,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 (mk-type #'X))] ...) (void ty_flat ...))))) #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) (stx-map @@ -700,10 +700,10 @@ [⊢ e ≫ e- ⇒ τ_e] #:with ([(~seq p ...) -> e_body] ...) #'clauses #:with (pat ...) (stx-map ; use brace to indicate root pattern - (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})])) + (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc this-syntax {pp ...})])) #'((p ...) ...)) #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e) - #:with ty-expected (get-expected-type stx) + #:with ty-expected (get-expected-type this-syntax) [[x ≫ x- : ty] ... ⊢ (add-expected e_body ty-expected) ≫ e_body- ⇒ ty_body] ... #:when (check-exhaust #'(pat- ...) #'τ_e) -------- @@ -715,7 +715,7 @@ #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses" [⊢ e ≫ e- ⇒ τ_e] #:when (×? #'τ_e) - #:with t_expect (get-expected-type stx) ; propagate inferred type + #:with t_expect (get-expected-type this-syntax) ; propagate inferred type #:with ([x ... -> e_body]) #'clauses #:with (~× ty ...) #'τ_e #:fail-unless (stx-length=? #'(ty ...) #'(x ...)) @@ -732,7 +732,7 @@ #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses" [⊢ e ≫ e- ⇒ τ_e] #:when (List? #'τ_e) - #:with t_expect (get-expected-type stx) ; propagate inferred type + #:with t_expect (get-expected-type this-syntax) ; propagate inferred type #:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary))) (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'()))) -> e_body] ...+) @@ -769,7 +769,7 @@ #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses" [⊢ e ≫ e- ⇒ τ_e] #:when (and (not (×? #'τ_e)) (not (List? #'τ_e))) - #:with t_expect (get-expected-type stx) ; propagate inferred type + #:with t_expect (get-expected-type this-syntax) ; propagate inferred type #:with ([Clause:id x:id ... (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)])) -> e_c_un] ...+) ; un = unannotated with expected ty @@ -779,7 +779,7 @@ #:with (_ (_ (_ ConsAll) . _) ...) #'info-body #:fail-unless (set=? (syntax->datum #'(Clause ...)) (syntax->datum #'(ConsAll ...))) - (type-error #:src stx + (type-error #:src this-syntax #:msg (string-append "match: clauses not exhaustive; missing: " (string-join @@ -879,7 +879,7 @@ ;; compute fn type (ie ∀ and →) [⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))] ;; solve for type variables Xs - #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx) + #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax) ;; instantiate polymorphic function type #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) @@ -895,13 +895,13 @@ (syntax-parse #'τ_out [(~?∀ (Y ...) τ_out) #:fail-unless (→? #'τ_out) - (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn) + (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) (for ([X (in-list (syntax->list #'(unsolved-X ...)))]) (unless (covariant-X? X #'τ_out) (raise-syntax-error #f - (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn) - stx))) + (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) + this-syntax))) #'(∀ (unsolved-X ... Y ...) τ_out)])) -------- [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out*]]) diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt index 405ba84..622ca8a 100644 --- a/turnstile/examples/stlc+effect.rkt +++ b/turnstile/examples/stlc+effect.rkt @@ -80,7 +80,7 @@ -------- [⊢ (#%app- box- e-) (⇒ : (Ref τ)) - (⇒ ν (locs #,(syntax-position stx) ns ...)) + (⇒ ν (locs #,(syntax-position this-syntax) ns ...)) (⇒ := (locs as ...)) (⇒ ! (locs ds ...))]]) (define-typed-syntax deref @@ -95,7 +95,7 @@ (⇒ : ty) (⇒ ν (locs ns ...)) (⇒ := (locs as ...)) - (⇒ ! (locs #,(syntax-position stx) ds ...))]]) + (⇒ ! (locs #,(syntax-position this-syntax) ds ...))]]) (define-typed-syntax := #:literals (:=) [(_ e_ref e) ≫ [⊢ e_ref ≫ e_ref- @@ -112,6 +112,6 @@ [⊢ (#%app- set-box!- e_ref- e-) (⇒ : Unit) (⇒ ν (locs ns1 ... ns2 ...)) - (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...)) + (⇒ := (locs #,(syntax-position this-syntax) as1 ... as2 ...)) (⇒ ! (locs ds1 ... ds2 ...))]]) diff --git a/turnstile/examples/stlc+reco+sub.rkt b/turnstile/examples/stlc+reco+sub.rkt index efdc9a6..a5645a9 100644 --- a/turnstile/examples/stlc+reco+sub.rkt +++ b/turnstile/examples/stlc+reco+sub.rkt @@ -49,5 +49,4 @@ #'([l τl] ...))] [_ #f]))) (current-sub? sub?) - (current-typecheck-relation sub?) - (current-check-relation sub?)) + (current-typecheck-relation sub?)) diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt index ca86aee..0660a1a 100644 --- a/turnstile/examples/stlc+reco+var.rkt +++ b/turnstile/examples/stlc+reco+var.rkt @@ -122,7 +122,7 @@ (∨-ref #'τ #'l #:else (λ () (raise-syntax-error #f (format "~a field does not exist" (syntax->datum #'l)) - stx))) + this-syntax))) [⊢ e ≫ e- ⇐ τ_e] -------- [⊢ (list- 'l e)]]) diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt index 2e32c4f..f4aae33 100644 --- a/turnstile/examples/stlc+sub.rkt +++ b/turnstile/examples/stlc+sub.rkt @@ -52,7 +52,6 @@ (Top? τ2))) (define current-sub? (make-parameter sub?)) (current-typecheck-relation sub?) - (current-check-relation sub?) (define (subs? τs1 τs2) (and (stx-length=? τs1 τs2) @@ -75,8 +74,7 @@ [(τ τ2-expander) ((current-sub?) #'τ #'τ1)] [_ #f])) (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) - (current-typecheck-relation (current-sub?)) - (current-check-relation (current-sub?)))] + (current-typecheck-relation (current-sub?)))] [(_ (~seq τ1:id <: τ2:id (~and (~literal ...) ddd)) (~seq τ3:id <: τ4:id) => @@ -96,8 +94,7 @@ ((current-sub?) #'τ3 #'τ4))] [_ #f])) (current-sub? (λ (t1 t2) (or (old-sub? t1 t2) (fn t1 t2)))) - (current-typecheck-relation (current-sub?)) - (current-check-relation (current-sub?)))])) + (current-typecheck-relation (current-sub?)))])) (define-sub-relation Nat <: Int) (define-sub-relation Int <: Num) diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt index 964080a..7558b71 100644 --- a/turnstile/examples/stlc+union+case.rkt +++ b/turnstile/examples/stlc+union+case.rkt @@ -97,7 +97,6 @@ [_ #f]))) (current-sub? sub?) (current-typecheck-relation sub?) - (current-check-relation sub?) (define (subs? τs1 τs2) (and (stx-length=? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2)))) diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt index f23d0c8..c30d7ca 100644 --- a/turnstile/examples/stlc+union.rkt +++ b/turnstile/examples/stlc+union.rkt @@ -124,7 +124,6 @@ [_ #f]))) (define current-sub? (make-parameter sub?)) (current-typecheck-relation sub?) - (current-check-relation sub?) (define (subs? τs1 τs2) (and (stx-length=? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2))) diff --git a/turnstile/examples/tests/fomega-no-reuse-tests.rkt b/turnstile/examples/tests/fomega-no-reuse-tests.rkt index d2c2918..b95e7f2 100644 --- a/turnstile/examples/tests/fomega-no-reuse-tests.rkt +++ b/turnstile/examples/tests/fomega-no-reuse-tests.rkt @@ -54,7 +54,7 @@ : (→ (→ Int String) (→ Int String))) (typecheck-fail ; TODO: fix err msg: "given an invalid expression" (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1) - #:with-msg "inst: type mismatch: expected ★") + #:with-msg "inst:.*not a valid type: 1") (typecheck-fail (Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1))) diff --git a/turnstile/examples/tests/rackunit-typechecking.rkt b/turnstile/examples/tests/rackunit-typechecking.rkt index 7830c2d..6925b18 100644 --- a/turnstile/examples/tests/rackunit-typechecking.rkt +++ b/turnstile/examples/tests/rackunit-typechecking.rkt @@ -4,7 +4,6 @@ check-equal/rand (rename-out [typecheck-fail check-stx-err])) - (begin-for-syntax (define (add-esc s) (string-append "\\" s)) (define escs (map add-esc '("(" ")" "[" "]"))) diff --git a/turnstile/examples/trivial.rkt b/turnstile/examples/trivial.rkt index 7ef6585..e6be01e 100644 --- a/turnstile/examples/trivial.rkt +++ b/turnstile/examples/trivial.rkt @@ -121,7 +121,6 @@ [_ #f]))) (current-type=? new-type=?) (current-typecheck-relation new-type=?) - (current-check-relation new-type=?) ;; current-type? ;; TODO: disabling type validation for now @@ -147,7 +146,6 @@ ((current-type-eval) #'(CCs- a b c (Int (#%datum- . e-)))))] [_ t+])) (current-type-eval new-teval) - (current-ev new-teval) ;; type inference helpers --------------------------------------------------- ;; A "B" is a type binding, eg (X ty) or (ty X) @@ -346,7 +344,7 @@ #:with Bs** (prune-Bs #'Bs*) ; #:when (begin (displayln "checking Cs:") ; (pretty-print (syntax->datum #'Cs*))) - #:with remaining-Cs (check-Cs #'Cs* stx) + #:with remaining-Cs (check-Cs #'Cs* this-syntax) ; #:when (printf "remaining Cs: ~a\n" ; (syntax->datum #'remaining-Cs)) #:with ty-out** diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index b9a84cb..5502a10 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -5,9 +5,9 @@ define-typed-syntax define-syntax-category (rename-out [define-typed-syntax define-typerule] [define-typed-syntax define-syntax/typecheck]) - (for-syntax syntax-parse/typed-syntax + (for-syntax syntax-parse/typecheck (rename-out - [syntax-parse/typed-syntax syntax-parse/typecheck]))) + [syntax-parse/typecheck syntax-parse/typed-syntax]))) (require (except-in (rename-in macrotypes/typecheck @@ -201,9 +201,9 @@ (define max-d (apply max 0 ds))] #:with depth (add1 max-d) #:with [[es-stx* es-stx-orig* es-pat*] ...] - (for/list ([tc-es-stx (in-list (syntax->list #'[tc.es-stx ...]))] - [tc-es-stx-orig (in-list (syntax->list #'[tc.es-stx-orig ...]))] - [tc-es-pat (in-list (syntax->list #'[tc.es-pat ...]))] + (for/list ([tc-es-stx (in-stx-list #'[tc.es-stx ...])] + [tc-es-stx-orig (in-stx-list #'[tc.es-stx-orig ...])] + [tc-es-pat (in-stx-list #'[tc.es-pat ...])] [d (in-list ds)]) (list (add-lists tc-es-stx (- max-d d)) @@ -311,7 +311,7 @@ ([k (in-stx-list #'[props.tag ...])] [v (in-stx-list #'[props.tag-expr ...])]) (with-syntax ([body body] [k k] [v v]) - #'(attach body `k ((current-ev) v))))] + #`(attach body `k ((current-ev) v))))] ;; ⇒ conclusion, implicit pat [pattern (~or [⊢ e-stx props:⇒-props/conclusion] [⊢ [e-stx props:⇒-props/conclusion]]) @@ -338,7 +338,7 @@ (~parse τ-pat #'τ)) #:with [stuff ...] #'[] #:with body:expr - #'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)] + #'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)] ;; macro invocations [pattern [≻ e-stx] #:with :last-clause #'[_ ≻ e-stx]] @@ -396,80 +396,59 @@ (require (for-meta 1 'syntax-classes) (for-meta 2 'syntax-classes)) -(define-syntax define-typed-syntax - (lambda (stx) - (syntax-parse stx - ;; single-clause def - [(def (name:id . pats) . rst) - ;; cannot always bind name as pat var, eg #%app, so replace with _ - #:with r:rule #'[(_ . pats) . rst] - #'(-define-typed-syntax name r.norm)] - ;; multi-clause def - [(def name:id - (~and (~seq kw-stuff ...) :stxparse-kws) - rule:rule - ...+) - #'(-define-typed-syntax - name - kw-stuff ... - rule.norm - ...)]))) - (begin-for-syntax - (define-syntax syntax-parse/typed-syntax - (lambda (stx) - (syntax-parse stx - [(stxparse - stx-expr + (define-syntax syntax-parse/typecheck + (syntax-parser + [(_ stx-expr (~and (~seq kw-stuff ...) :stxparse-kws) - rule:rule - ...) - #'(syntax-parse - stx-expr - kw-stuff ... - rule.norm - ...)])))) + rule:rule ...) + #'(syntax-parse stx-expr kw-stuff ... rule.norm ...)]))) + +;; macrotypes/typecheck.rkt already defines (-define-syntax-category type); +;; - just add the "def-named-syntax" part of the def-stx-cat macro below +;; TODO: eliminate code dup with def-named-stx in define-stx-cat below? +(define-syntax define-typed-syntax + (syntax-parser + ;; single-clause def + [(_ (rulename:id . pats) . rst) + ;; using #'rulename as patvar may cause problems, eg #%app, so use _ + #'(define-typed-syntax rulename [(_ . pats) . rst])] + ;; multi-clause def + ;; - let stx-parse/tychk match :rule (dont double-match) + [(_ rulename:id + (~and (~seq kw-stuff ...) :stxparse-kws) + rule ...+) + #'(define-syntax (rulename stx) + (parameterize ([current-check-relation (current-typecheck-relation)] + [current-ev (current-type-eval)] + [current-tag (type-key1)]) + (syntax-parse/typecheck stx kw-stuff ... rule ...)))])) (define-syntax define-syntax-category - (lambda (stx) - (syntax-parse stx + (syntax-parser [(_ name:id) ; default key1 = ': for types #'(define-syntax-category : name)] [(_ key:id name:id) ; default key2 = ':: for kinds #`(define-syntax-category key name #,(mkx2 #'key))] [(_ key1:id name:id key2:id) #:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name) - #:with new-check-relation (format-id #'name "current-~acheck-relation" #'name) - ;; #:with new-attach (format-id #'name "assign-~a" #'name) - ;; #:with new-detach (format-id #'name "~aof" #'name) + #:with new-check-rel (format-id #'name "current-~acheck-relation" #'name) #:with new-eval (format-id #'name "current-~a-eval" #'name) #'(begin (-define-syntax-category key1 name key2) - (define-syntax (def-named-syntax stx) - (syntax-parse stx + (define-syntax def-named-syntax + (syntax-parser ;; single-clause def - #;[(_ (rulename:id . pats) . rst) - ;; cannot bind name as pat var, eg #%app, so replace with _ - #:with r #'[(_ . pats) . rst] - #'(define-syntax (rulename stxx) - (parameterize ([current-check-relation (new-check-relation)] - [current-attach new-attach] - [current-detach new-detach] - [current-tag 'key1]) - (syntax-parse/typed-syntax stxx r)))] [(_ (rulename:id . pats) . rst) - ;; cannot bind name as pat var, eg #%app, so replace with _ - #:with r #'[(_ . pats) . rst] - #'(def-named-syntax rulename r)] - ;; multi-clause def - [(_ rulename:id + ;; #'rulename as a pat var may cause problems, eg #%app, so use _ + #'(def-named-syntax rulename [(_ . pats) . rst])] + ;; multi-clause def + [(_ rulename:id (~and (~seq kw-stuff (... ...)) :stxparse-kws) - rule:rule (... ...+)) - #'(define-syntax (rulename stxx) - (parameterize ([current-check-relation (new-check-relation)] - ;; [current-attach new-attach] - ;; [current-detach new-detach] + rule (... ...+)) ; let stx-parse/tychk match :rule stxcls + #'(define-syntax (rulename stx) + (parameterize ([current-check-relation (new-check-rel)] [current-ev (new-eval)] [current-tag 'key1]) - (syntax-parse/typed-syntax stxx kw-stuff (... ...) - rule (... ...))))])))]))) + (syntax-parse/typecheck stx kw-stuff (... ...) + rule (... ...))))])))]))