From 6cb15a06da533e6efc2d918df38c91b1b482e891 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 13 Apr 2016 15:14:57 -0400 Subject: [PATCH] code cleanup --- tapl/mlish.rkt | 176 ++++++-------------------------- tapl/notes.txt | 58 +++++++++++ tapl/tests/run-mlish-tests1.rkt | 2 +- tapl/tests/run-mlish-tests2.rkt | 2 +- tapl/typecheck.rkt | 156 +++++++--------------------- 5 files changed, 129 insertions(+), 265 deletions(-) diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index 91c89ff..9a177fe 100644 --- a/tapl/mlish.rkt +++ b/tapl/mlish.rkt @@ -43,9 +43,8 @@ ; should only be monomorphic? [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...))) (compute-constraints #'((τ1 τ2) ...))] - [_ #:when #t #;(printf "shouldnt get here. could not unify: ~a\n" τ1-τ2) #'()])) - (define (compute-constraints τs) - ;(printf "constraints: ~a\n" (syntax->datum τs)) + [_ #'()])) + (define (compute-constraints τs) (stx-appendmap compute-constraint τs)) (define (solve-constraint x-τ) @@ -136,24 +135,10 @@ ;; top-lvl fns, since they can call each other #:with (~and ty_fn_expected (~∀ _ (~ext-stlc:→ _ ... out_expected))) ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...))) - ;; #:with [_ _ (~and ty_fn_actual (~∀ _ (~ext-stlc:→ _ ... out_actual)))] - ;; (infer/ctx+erase #'([f : ty_fn_expected]) ; need to handle recursive fn calls - ;; #'(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))) - ;; #:fail-unless (typecheck? #'ty_fn_actual #'ty_fn_expected) - ;; (format - ;; "Function ~a's body ~a has type ~a, which does not match given type ~a." - ;; (syntax->datum #'f) (syntax->datum #'e) - ;; (type->str #'out_actual) (type->str #'τ_out)) #`(begin - (define-syntax f - (make-rename-transformer - ;(⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out))))) - (⊢ g : ty_fn_expected #;(∀ Ys (ext-stlc:→ τ+orig ...))))) + (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected))) (define g (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))] - #;(begin - (define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out))))) - (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann)))) [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) #'(define/tc (f [x : ty] ... -> ty_out) . b)] [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e) @@ -179,19 +164,8 @@ ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...))) 'orig (list #'(→ τ+orig ...))) - ;; #:with [_ _ (~and ty_fn_actual (~∀ _ (~ext-stlc:→ _ ... out_actual)))] - ;; (infer/ctx+erase #'([f : ty_fn_expected]) ; need to handle recursive fn calls - ;; #'(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))) - ;; #:fail-unless (typecheck? #'ty_fn_actual #'ty_fn_expected) - ;; (format - ;; "Function ~a's body ~a has type ~a, which does not match given type ~a." - ;; (syntax->datum #'f) (syntax->datum #'e) - ;; (type->str #'out_actual) (type->str #'τ_out)) #`(begin - (define-syntax f - (make-rename-transformer - ;(⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out))))) - (⊢ g : ty_fn_expected #;(∀ Ys (ext-stlc:→ τ+orig ...))))) + (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected))) (define g (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]) @@ -214,12 +188,8 @@ (Cons [fld (~datum :) τ] ...) (~and (Cons τ ...) (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...) - #:with RecName (generate-temporary #'Name) #:with NameExpander (format-id #'Name "~~~a" #'Name) #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name) - #:with NameDelayed (format-id #'Name "~a-delayed" #'Name) - #:with NameForced (format-id #'NameDelayed "~a-force" #'NameDelayed) - #:with NameForcedExpander (format-id #'NameForced "~~~a" #'NameForced) #:with (StructName ...) (generate-temporaries #'(Cons ...)) #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) @@ -227,47 +197,13 @@ #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs)) #'(StructName ...) #'((fld ...) ...)) #:with (Cons? ...) (stx-map mk-? #'(StructName ...)) - #:with (Y ...) (generate-temporaries #'(X ...)) - ;; types, but using RecName instead of Name - #:with ((τ/rec ...) ...) (subst #'RecName #'Name #'((τ ...) ...)) #`(begin -; (define NameDelayed (lambda () (error "types not allowed at runtime"))) - ; TODO: use define-type-constructor for delayed form as well, - ;; to get proper pattern expanders, etc - ;; (define-syntax (Name stx) - ;; (syntax-parse stx - ;; [(_ Y ...) (add-orig (mk-type #'(delay NameDelayed Y ...)) stx)])) (define-syntax (NameExtraInfo stx) (syntax-parse stx [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)])) (define-type-constructor Name #:arity = #,(stx-length #'(X ...)) #:extra-info 'NameExtraInfo -; #:extra-info (X ...) (('Cons 'StructName Cons? [acc τ] ...) ...) - #:no-provide) - #;(define-type-constructor Name - #:arity = #,(stx-length #'(X ...)) - #:extra-info (X ...) - (λ (RecName) - (let-syntax - ([RecName - (syntax-parser - [(_ Y ...) - ;; - this is a placeholder to break the recursion - ;; - clients, like match, must manually unfold by - ;; replacing the entire (#%plain-app RecName ...) stx - ;; - to preserve polymorphic recursion, the entire stx - ;; should be replaced but with X ... as the args - ;; in place of args in the input type - ;; (see subst-special in typecheck.rkt) - (assign-type #'(#%plain-app RecName Y ...) #'#%type)] - [(~and err (_ . rst)) - (type-error #:src #'err - #:msg (format "type constructor ~a expects ~a args, given ~a: ~a" - (syntax->datum #'Name) (stx-length #'(X ...)) - (stx-length #'rst) (string-join (stx-map type->str #'rst) ", ")))] - )]) - ('Cons 'StructName Cons? [acc τ/rec] ...) ...)) #:no-provide) (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ... (define-syntax (Cons stx) @@ -280,7 +216,6 @@ #:with τ-expected (syntax-property #'C 'expected-type) #:fail-unless (syntax-e #'τ-expected) (type-error #:src stx #:msg "cannot infer type of ~a; add annotations" #'C) -; #:with (_ (~datum delay) (_ () _ τ-expected-arg (... ...))) ((current-type-eval) #'τ-expected) #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected) #'(C {τ-expected-arg (... ...)})] [_:id @@ -334,14 +269,9 @@ [{(~datum _)} #'()] [{(~literal stlc+cons:nil)} #'()] [{A:id} ; disambiguate 0-arity constructors (that don't need parens) - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . info-body))) #:when (get-extra-info #'ty) #'()] ;; comma tup syntax always has parens -; [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))} [{(~and ps (p1 (unq p) ...))} #:when (not (stx-null? #'(p ...))) #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) @@ -351,12 +281,7 @@ [((~datum _) ty) #'()] [((~or (~literal stlc+cons:nil)) ty) #'()] [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens) - #:with (_ (_ ((~literal quote) C) . _) ...) - ;; ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . (((~literal #%plain-app) ((~literal quote) C) . rst) ...)))) - (get-extra-info #'ty) + #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty) #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) #'()] [(x:id ty) #'((x ty))] @@ -379,21 +304,15 @@ #:with (~List t) #'ty (unifys #'([p t] [ps ty]))] [((Name p ...) ty) - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . info-body))) - ;; (get-extra-info #'ty) -; #:with (_ (_ ((~literal quote) ConsAll) . _) ...) (get-extra-info #'ty) -; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body) - #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...) - (stx-findf - (syntax-parser - [(_ 'C . rst) - (equal? (syntax->datum #'Name) (syntax->datum #'C))]) - (stx-cdr (get-extra-info #'ty))) - (unifys #'([p τ] ...))] - [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) #'()])) + #:with (_ (_ Cons) _ _ [_ _ τ] ...) + (stx-findf + (syntax-parser + [(_ 'C . rst) + (equal? (syntax->datum #'Name) (syntax->datum #'C))]) + (stx-cdr (get-extra-info #'ty))) + (unifys #'([p τ] ...))] + [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) + #'()])) (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys)) (define (compile-pat p ty) @@ -403,15 +322,9 @@ [{(~datum _)} #'_] [{(~literal stlc+cons:nil)} (syntax/loc p (list))] [{A:id} ; disambiguate 0-arity constructors (that don't need parens) - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . info-body))) #:when (get-extra-info ty) (compile-pat #'(A) ty)] ;; comma tup stx always has parens - ;; comma tup syntax always has parens -; [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))} [{(~and ps (p1 (unq p) ...))} #:when (not (stx-null? #'(p ...))) #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) @@ -421,12 +334,8 @@ [(~literal stlc+cons:nil) ; nil #'(list)] [A:id ; disambiguate 0-arity constructors (that don't need parens) - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . (((~literal #%plain-app) ((~literal quote) C) . rst) ...)))) - #:with (_ (_ ((~literal quote) C) . _) ...) (get-extra-info ty) - #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) + #:with (_ (_ (_ C) . _) ...) (get-extra-info ty) + #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) (compile-pat #'(A) ty)] [x:id p] [(p1 (unq p) ...) ; comma tup stx @@ -454,14 +363,7 @@ #:with ps- (compile-pat #'ps ty) #'(cons p- ps-)] [(Name . pats) - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . info-body))) - ;; (get-extra-info ty) - ;; #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body - ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body) - #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...) + #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...) (stx-findf (syntax-parser [(_ 'C . rst) @@ -513,14 +415,7 @@ (syntax->list #'((p ...) ...)))])])] [else ; algebraic datatypes (syntax-parse (get-extra-info ty) - [#;((~literal #%plain-lambda) (RecName) - ((~literal let-values) () - ((~literal let-values) () - . (((~literal #%plain-app) - ((~literal quote) C) - ((~literal quote) Cstruct) - . rst) ...)))) - (_ (_ ((~literal quote) C) ((~literal quote) Cstruct) . rst) ...) + [(_ (_ (_ C) (_ Cstruct) . rst) ...) (syntax-parse pats [((Cpat _ ...) ...) (define Cs (syntax->datum #'(C ...))) @@ -538,6 +433,7 @@ #t])] [_ #t])])) + ;; TODO: do get-ctx and compile-pat in one pass (define (compile-pats pats ty) (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats)) ) @@ -553,13 +449,11 @@ (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})])) #'((p ...) ...)) #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e) - ;; #:with ((~and ctx ([x ty] ...)) ...) (stx-map (lambda (p) (get-ctx p #'τ_e)) #'(pat ...)) #:with ty-expected (get-expected-type stx) #:with ([(x- ...) e_body- ty_body] ...) (stx-map infer/ctx+erase #'(ctx ...) #'((add-expected e_body ty-expected) ...)) - ;; #:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...)) #:fail-unless (same-types? #'(ty_body ...)) (string-append "branches have different types, given: " (string-join (stx-map type->str #'(ty_body ...)) ", ")) @@ -569,7 +463,6 @@ ])])) (define-typed-syntax match #:datum-literals (with) -; (syntax-parse stx #:datum-literals (with) [(_ e with . clauses) #:fail-when (null? (syntax->list #'clauses)) "no clauses" #:with [e- τ_e] (infer+erase #'e) @@ -594,7 +487,9 @@ [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary))) (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'()))) -> e_body] ...) - #:fail-unless (stx-ormap (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) #'(xs ...)) + #:fail-unless (stx-ormap + (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) + #'(xs ...)) "match: missing empty list case" #:fail-when (and (stx-andmap brack? #'(xs ...)) (= 1 (stx-length #'(xs ...)))) @@ -625,16 +520,9 @@ [([Clause:id x:id ... (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)])) -> e_c_un] ...) ; un = unannotated with expected ty - ;; len #'clauses maybe > len #'info, due to guards - ;; #:with ((~literal #%plain-lambda) (RecName) - ;; ((~literal let-values) () - ;; ((~literal let-values) () - ;; . info-body))) - ;; (get-extra-info #'τ_e) - ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body) + ;; length #'clauses may be > length #'info, due to guards #:with info-body (get-extra-info #'τ_e) - #:with info-unfolded #'info-body - #:with (_ (_ ((~literal quote) ConsAll) . _) ...) #'info-body + #:with (_ (_ (_ ConsAll) . _) ...) #'info-body #:fail-unless (set=? (syntax->datum #'(Clause ...)) (syntax->datum #'(ConsAll ...))) (type-error #:src stx @@ -646,14 +534,13 @@ (syntax->datum #'(ConsAll ...)) (syntax->datum #'(Clause ...)))) ", "))) - #:with ((_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...) ...) + #:with ((_ _ _ Cons? [_ acc τ] ...) ...) (map ; ok to compare symbols since clause names can't be rebound (lambda (Cl) (stx-findf (syntax-parser - [((~literal #%plain-app) 'C . rst) - (equal? Cl (syntax->datum #'C))]) - (stx-cdr #'info-unfolded))) ; drop leading #%app + [(_ 'C . rst) (equal? Cl (syntax->datum #'C))]) + (stx-cdr #'info-body))) ; drop leading #%app (syntax->datum #'(Clause ...))) ;; this commented block experiments with expanding to unsafe ops ;; #:with ((acc ...) ...) (stx-map @@ -781,8 +668,10 @@ (define old-orig (get-orig tyin)) (define new-orig (and old-orig - (substs (stx-map get-orig #'tys-solved) #'Xs old-orig - (lambda (x y) (equal? (syntax->datum x) (syntax->datum y)))))) + (substs + (stx-map get-orig #'tys-solved) #'Xs old-orig + (lambda (x y) + (equal? (syntax->datum x) (syntax->datum y)))))) (syntax-property tyin 'orig (list new-orig))) #'(τ_in ...))) (⊢ (#%app e_fn- e_arg- ...) : τ_out)])])] @@ -931,8 +820,7 @@ [(_ start) #:with start- (⇑ start as Int) (⊢ (in-naturals start-) : (Sequence Int))]) - - + (define-typed-syntax in-vector [(_ e) diff --git a/tapl/notes.txt b/tapl/notes.txt index 977bc5f..88854ba 100644 --- a/tapl/notes.txt +++ b/tapl/notes.txt @@ -1,3 +1,61 @@ +2016-04-13: +Summary of the extra-info problem. +Problem: datatypes need to know all constructors and argument types +- to properly do matching +- but storing this info as part of the type leads to looping for recursive + and mutually recursive types, since the canonical form of all types is + full expansion +Current solution: +- for each type TY, define: + - standard TY macro via define-type-constructor + - with extra-info = name of additional macro + - additional "extra-info" macro that expands into needed datatype clause info +- this solution addresses many issues: + - breaks the recursion (ie inf looping) in type macros + - is much faster, since it avoids the type traversals I was doing to manually + unroll recursive types (see subst-special and subst-expr) + - allows for substing of quantified tyvars to occur naturally, + since the types are passed into the extra-info macro + +What didnt work: +- quoting the extra-info (or parts of it) to avoid infinite expansion + - summary: + - must be exposed to expansion: + - struct accessors + - any type vars + - cannot be exposed to expansion: + - call to recursive and mutually recursive type constructors + - tried a complicated solution where I used "sentinel" stxs + to accumulate the context that the quoted parts were missing + - was complicated when needing to instantiate forall types + - and didnt fully work for nested datatypes + +- manually subst out recursive calls + - essentially, this required me to manually manage the recursive types, + including, a la tapl, including unrolling in match + - was very performance costly (see subst-special and subst-expr) + - this solution does work with mutually recursive types (still inf loops) + +- store extra-info as stx-property + - figured out how to use make-syntax-delta-introducer to sync up unexpanded + props, so that it may be instantiated properly + - but something doesnt work (specifically match) when types are provided + - works if everything is defined in the same file + - ie, inline basics-general in basics2 + - doesnt work if (provide (struct-out ...)) is inserted directly in mlish.rkt + - couldnt get it to work if Cons? is assigned different contexts in match + - eg context of e-, or τ_e + - direct match on constructor is fine (see Bool use in bg/basics2.mlish) + - but doesnt work when passed through fn call (see bool-id in basics2) + - essentially, struct accessors and predicates must be exposed to expansion + error is: + ; require: namespace mismatch; + ; reference to a module that is not available + ; reference phase: 0 + ; referenced module: 'basics-general + ; referenced phase level: 0 + ; in: True26? + 2016-02-29 Problem: storing variant info as properties - when instantiating polymorphic type, need to instantiate properties as well diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt index c486d39..e59e76f 100644 --- a/tapl/tests/run-mlish-tests1.rkt +++ b/tapl/tests/run-mlish-tests1.rkt @@ -1,6 +1,6 @@ #lang racket/base (require "mlish-tests.rkt") -;(require "mlish/queens.mlish") +(require "mlish/queens.mlish") (require "mlish/listpats.mlish") (require "mlish/match2.mlish") (require "mlish/polyrecur.mlish") diff --git a/tapl/tests/run-mlish-tests2.rkt b/tapl/tests/run-mlish-tests2.rkt index 7cc65dd..92e8e14 100644 --- a/tapl/tests/run-mlish-tests2.rkt +++ b/tapl/tests/run-mlish-tests2.rkt @@ -1,6 +1,6 @@ #lang racket/base -(require "mlish/queens.mlish") +;(require "mlish/queens.mlish") ;; shootout tests (require "mlish/trees-tests.mlish") diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index c0b602f..659ff2d 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -134,12 +134,10 @@ (define-syntax add-expected (syntax-parser - [(_ e τ) -; #:when (printf "adding expected type ~a to expression ~a\n" -; (syntax->datum #'τ) (syntax->datum #'e)) - (syntax-property #'e 'expected-type #'τ)])) + [(_ e τ) (syntax-property #'e 'expected-type #'τ)])) (define-for-syntax (add-expected-ty e ty) - (or (and (syntax-e ty) (syntax-property e 'expected-type ((current-type-eval) ty))) + (or (and (syntax-e ty) + (syntax-property e 'expected-type ((current-type-eval) ty))) e)) ;; type assignment @@ -213,10 +211,6 @@ ['x (syntax-e #'x)] [_ (syntax->datum #'e-)]) 'tycon (type->str #'τ_e)) - #;(if (stx-pair? #'τ_e) - (syntax-parse #'τ_e - [(τ-expander . args) #'(e- args)]) - #'e-) (syntax-parse #'τ_e [(τ-expander . args) #'(e- args)] [_ #'e-])])])) @@ -243,10 +237,6 @@ ;#:with args (τ-get #'τ_e) #:with res (stx-map (λ (e t) - #;(if (stx-pair? t) - (syntax-parse t - [(τ-expander . args) #`(#,e #'args)]) - e) (syntax-parse t [(τ-expander . args) #`(#,e args)] [_ e])) @@ -298,44 +288,37 @@ (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...) (λ (x ...) - (let-syntax ([x (syntax-parser [i:id -; #:when (or (not (and (identifier? #'τ) (free-identifier=? #'x #'τ))) -; (printf "~a has type = itself\n" #'i)) -; #:when (or (not (get-expected-type #'i)) -; (printf "expected type of ~a: ~a\n" -; #'i (and (get-expected-type #'i) -; (syntax->datum (get-expected-type #'i))))) -; #:when (or (not (get-expected-type #'i)) -; (printf "assigned type of ~a: ~a\n" -; (syntax->datum #'i) (syntax->datum #'τ))) - (if (and (identifier? #'τ) (free-identifier=? #'x #'τ)) - (if (get-expected-type #'i) - (add-env (assign-type #'x (get-expected-type #'i)) #`((x #,(get-expected-type #'i)))) - (raise (exn:fail:type:infer - (format "~a (~a:~a): could not infer type of ~a; add annotation(s)" - (syntax-source #'x) (syntax-line #'x) (syntax-column #'x) - (syntax->datum #'x)) - (current-continuation-marks)))) - (assign-type #'x #'τ))] - [(o . rst) ; handle if x used in fn position - #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ)) - (raise (exn:fail:type:infer - (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)" - (syntax-source #'o) (syntax-line #'o) (syntax-column #'o) - (syntax->datum #'o)) - (current-continuation-marks))) - #:with app (datum->syntax #'o '#%app) - #`(app #,(assign-type #'x #'τ) . rst)] - #;[(_ . rst) #`(#,(assign-type #'x #'τ) . rst)]) - #;(make-rename-transformer (assign-type #'x #'τ))] ...) + (let-syntax + ([x + (syntax-parser + [i:id + (if (and (identifier? #'τ) (free-identifier=? #'x #'τ)) + (if (get-expected-type #'i) + (add-env + (assign-type #'x (get-expected-type #'i)) + #`((x #,(get-expected-type #'i)))) + (raise + (exn:fail:type:infer + (format "~a (~a:~a): could not infer type of ~a; add annotation(s)" + (syntax-source #'x) (syntax-line #'x) (syntax-column #'x) + (syntax->datum #'x)) + (current-continuation-marks)))) + (assign-type #'x #'τ))] + [(o . rst) ; handle if x used in fn position + #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ)) + (raise (exn:fail:type:infer + (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)" + (syntax-source #'o) (syntax-line #'o) (syntax-column #'o) + (syntax->datum #'o)) + (current-continuation-marks))) + #:with app (datum->syntax #'o '#%app) + #`(app #,(assign-type #'x #'τ) . rst)] + #;[(_ . rst) #`(#,(assign-type #'x #'τ) . rst)]) + #;(make-rename-transformer (assign-type #'x #'τ))] ...) (#%expression e) ... void))))) (list #'tvs+ #'xs+ #'(e+ ...) (stx-map ; need this check when combining #%type and kinds (λ (t) (or (false? t) - ; TODO: why does this happen? - ; happens when propagating 'env up in λ - #;(and (pair? t) - (syntax-local-introduce (car t))) (syntax-local-introduce t))) (stx-map typeof #'(e+ ...))))] [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)])) @@ -433,13 +416,7 @@ ((~literal #%plain-lambda) bvs ((~literal #%expression) ((~literal quote) extra-info-macro)) . tys)) (expand/df #'(extra-info-macro . tys))] - [_ #f])) - (define (get-tyargs ty) - (syntax-parse ty - [((~literal #%plain-app) internal-id - ((~literal #%plain-lambda) bvs - xtra-info . rst)) - #'rst]))) + [_ #f]))) (define-syntax define-basic-checked-id-stx @@ -488,17 +465,14 @@ (~optional (~seq #:arity op n:exact-nonnegative-integer) #:defaults ([op #'=] [n #'1])) - (~optional - (~seq #:bvs (~and (~parse has-bvs? #'#t) bvs-op) bvs-n:exact-nonnegative-integer) + (~optional (~seq #:bvs (~and (~parse has-bvs? #'#t) bvs-op) + bvs-n:exact-nonnegative-integer) #:defaults ([bvs-op #'=][bvs-n #'0])) (~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon)) #:defaults ([tycon #'void])) - #;(~optional (~seq #:extra-info extra-bvs extra-info) - #:defaults ([extra-bvs #'()] - [extra-info #'void])) - (~optional (~seq #:extra-info extra-info) #:defaults ([extra-info #'void])) - (~optional (~and #:no-provide (~parse no-provide? #'#t))) - ) + (~optional (~seq #:extra-info extra-info) + #:defaults ([extra-info #'void])) + (~optional (~and #:no-provide (~parse no-provide? #'#t)))) #:with #%kind (format-id #'kind "#%~a" #'kind) #:with τ-internal (generate-temporary #'τ) #:with τ? (mk-? #'τ) @@ -549,8 +523,6 @@ (define (τ? t) (and (stx-pair? t) (syntax-parse t - #;[((~literal #%plain-lambda) bvs ((~literal #%plain-app) (~literal τ-internal) . _)) - #t] [((~literal #%plain-app) (~literal τ-internal) . _) #t] [_ #f])))) @@ -581,10 +553,6 @@ #:with k_result (if #,(attribute has-annotations?) #'(tycon k_arg (... ...)) #'#%kind) - ;; #:with extra-info-inst - ;; (if (stx-null? #'extra-bvs) - ;; #'extra-info - ;; (substs #'τs- #'extra-bvs #'extra-info)) (add-orig (assign-type (syntax/loc stx @@ -720,54 +688,4 @@ [_ e])) (define (substs τs xs e [cmp bound-identifier=?]) - (stx-fold (lambda (ty x res) (subst ty x res cmp)) e τs xs)) - - ;; subst-expr: - ;; - like subst except the target can be any stx, rather than just an id - ;; - used for implementing polymorphic recursive types - (define (stx-lam? s) - (syntax-parse s - [((~literal #%plain-lambda) . rst) #t] [_ #f])) - (define (stx-lam=? s1 s2) - (syntax-parse (list s1 s2) - [(((~literal #%plain-lambda) xs . bs1) - ((~literal #%plain-lambda) ys . bs2)) - #:with zs (generate-temporaries #'xs) - (and (stx-length=? #'xs #'ys) - (stx=? (substs #'zs #'xs #'bs1) - (substs #'zs #'ys #'bs2)))])) - (define (stx=? s1 s2) - (or (and (identifier? s1) (identifier? s2) (free-identifier=? s1 s2)) - (and (stx-null? s1) (stx-null? s2)) - (and (stx-lam? s1) (stx-lam? s2) (stx-lam=? s1 s2)) - (and (stx-pair? s1) (stx-pair? s2) (stx-length=? s1 s2) - (stx-andmap stx=? s1 s2)))) - ;; subst e1 for e2 in e3 - (define (subst-expr e1 e2 e3) - (cond - [(stx=? e2 e3) e1] - [(identifier? e3) e3] - [else ; stx-pair - (with-syntax ([result (stx-map (lambda (e) (subst-expr e1 e2 e)) e3)]) - (syntax-track-origin #'result e3 #'here))])) - (define (subst-exprs τs xs e) - (stx-fold subst-expr e τs xs)) - ;; subst-special: - ;; - used for unfolding polymorphic recursive type - ;; subst ty1 for x in ty2 - ;; where ty1 is an applied type constructor type - ;; x is a placeholder for an applied tycons type in ty2 - ;; - subst special first replaces the args of ty1 with that of x - ;; before replacing applications of tycons x with this modified ty1 - (define (subst-special ty1 x ty2) - (cond - [(identifier? ty2) ty2] - [(syntax-parse ty2 [((~literal #%plain-app) tycons:id . _) (free-identifier=? #'tycons x)] [_ #f]) - (syntax-parse ty2 - [((~literal #%plain-app) tycons:id . newargs) -; #:with oldargs (get-tyargs ty1) - (subst-exprs #'newargs (get-tyargs ty1) ty1)])] - [else ; stx-pair - (with-syntax ([result (stx-map (lambda (e) (subst-special ty1 x e)) ty2)]) - (syntax-track-origin #'result ty2 #'here))])) - ) + (stx-fold (lambda (ty x res) (subst ty x res cmp)) e τs xs)))