all tests passing
- fixed current-ev problem
- forgot to update default define-typed-syntax in turnstile.rkt
with parameterize
This commit is contained in:
Stephen Chang
parent
ae5d160c05
commit
1a3f208903
|
|
@ -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)])
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -135,8 +135,7 @@
|
|||
(τ-eval τ)]
|
||||
[_
|
||||
(τ-eval τ-stx)]))))
|
||||
(current-type-eval ∪-eval)
|
||||
(current-ev ∪-eval))
|
||||
(current-type-eval ∪-eval))
|
||||
|
||||
;; -----------------------------------------------------------------------------
|
||||
;; --- Subtyping
|
||||
|
|
|
|||
|
|
@ -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"))
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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+ ...)))]
|
||||
|
|
|
|||
|
|
@ -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 ★-
|
||||
|
|
|
|||
|
|
@ -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)])
|
||||
|
||||
|
|
|
|||
|
|
@ -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) ≫
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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*]])
|
||||
|
|
|
|||
|
|
@ -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 ...))]])
|
||||
|
||||
|
|
|
|||
|
|
@ -49,5 +49,4 @@
|
|||
#'([l τl] ...))]
|
||||
[_ #f])))
|
||||
(current-sub? sub?)
|
||||
(current-typecheck-relation sub?)
|
||||
(current-check-relation sub?))
|
||||
(current-typecheck-relation sub?))
|
||||
|
|
|
|||
|
|
@ -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)]])
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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))))
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
|
|||
|
|
@ -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 '("(" ")" "[" "]")))
|
||||
|
|
|
|||
|
|
@ -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**
|
||||
|
|
|
|||
|
|
@ -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 (... ...))))])))]))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user