commit 487c8fedc5b8d27ee3fc6d71dd5cc7ea54416486
parent 3839ea51c44efc296bf76088d1e959b7d50d20c5
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 2 Mar 2016 15:34:51 -0500
mlish: fix define-type and match
- resolves #1
- define-type-constructor accepts arbitrary extra "info" that is stored
with the type
- get-extra-info extras this info
- define type stores extra info that is essentially a mu type
containing all variant info
- match must manually "unfold" this info, ie iso-recursive
- all tests passing
- mlish tests implements full nqueens example
- no explicit instantiation of polymorphic functions
- some polymorphic constructors require annotations when no inference possible
- a lone nil with no other information
- lambda params require annotations
- top lvl fns require full signature
Diffstat:
5 files changed, 244 insertions(+), 48 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -81,7 +81,13 @@
#:note (format "Could not infer instantiation of polymorphic function ~a."
(syntax->datum (stx-car stx)))))
(loop (stx-car args-rst) (stx-cdr args-rst)
- (stx-car tys-rst) (stx-cdr tys-rst) cs))))])))
+ (stx-car tys-rst) (stx-cdr tys-rst) cs))))]))
+ ;; instantiate polymorphic types
+ (define (inst-type ty-solved Xs ty)
+ (substs ty-solved Xs ty))
+ (define (inst-types ty-solved Xs tys)
+ (stx-map (lambda (t) (inst-type ty-solved Xs t)) tys))
+ )
;; define --------------------------------------------------
(define-typed-syntax define
@@ -114,6 +120,7 @@
#:with g (add-orig (generate-temporary #'f) #'f)
#:with e_ann #'(add-expected e τ_out)
#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ #:with (~∀ Xs (~ext-stlc:→ in ...)) ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
#`(begin
(define-syntax f
(make-rename-transformer
@@ -140,6 +147,7 @@
;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
(~and (~or (~and IdCons:id (~parse (Cons τ ...) #'(IdCons)))
(Cons τ ...))) ...)
+ #:with RecName (generate-temporary #'Name)
#:with NameExpander (format-id #'Name "~~~a" #'Name)
#:with (StructName ...) (generate-temporaries #'(Cons ...))
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
@@ -148,10 +156,33 @@
#:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#: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 get-Name-info (format-id #'Name "get-~a-info" #'Name)
+ ;; types, but using RecName instead of Name
+ #:with ((τ/rec ...) ...) (subst-expr #'RecName #'(Name X ...) #'((τ ...) ...))
#`(begin
(define-type-constructor Name
#:arity = #,(stx-length #'(X ...))
- #:other-prop variants #'(X ...) #'((Cons StructName [fld : τ] ...) ...))
+; #:other-prop variants #'(X ...) #'((Cons StructName [fld : τ] ...) ...))
+ #:extra-info (X ...) (λ (RecName) ('Cons Cons? [acc τ/rec] ...) ...))
+ ;; cant use define-type-constructor because I want expansion to contain all
+ ;; variant info (including possibly recursive references)
+ ;; (define-syntax (Name stx)
+ ;; (syntax-parse stx
+ ;; [(_ Y ...)
+ ;; #'(InternalName Y ... (λ (RecName) ('Cons StructName [fld τ/rec] ...) ...))]))
+ ;; (begin-for-syntax
+ ;; (define-syntax NameExpander
+ ;; (pattern-expander
+ ;; (syntax-parser
+ ;; [(_ . pat)
+ ;; #:with expanded-ty (generate-temporary)
+ ;; #'(~and expanded-ty
+ ;; (~parse
+ ;; ((literal #%plain-app) (~literal InternalName)
+ ;; arg ... ((~literal #%plain-lambda) _ variant-info))
+ ;; #'expanded-ty)
+ ;; (~parse pat #'(arg ...)))]))))
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
(define-syntax (Cons stx)
(syntax-parse stx
@@ -199,8 +230,13 @@
[(C . args) ; no type annotations, must infer instantiation
;; infer instantiation types from args left-to-right,
;; short-circuit if done early, and use result to help infer remaining args
- #:with (~Tmp Ys . τs+) ((current-type-eval) #'(Tmp (X ...) τ ...))
- #:with (τ_solved (... ...)) (solve #'Ys #'τs+ stx)
+ #:with (~Tmp Ys . τs+) ((current-type-eval) #'(Tmp (X ...) (Name X ...) τ ...))
+ #:with ty-expected (get-expected-type stx) ; first attempt to instantiate using expected-ty
+ #:with dummy-e (if (syntax-e #'ty-expected) ; to use solve, need to attach expected-ty to expr
+ (assign-type #'"dummy" #'ty-expected)
+ (assign-type #'"dummy" #'Int)) ; Int is another dummy
+ #:with (new-app (... ...)) #'(C dummy-e . args)
+ #:with (τ_solved (... ...)) (solve #'Ys #'τs+ #'(new-app (... ...)))
;; (let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)]
;; [τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)]
;; [old-cs #'()])
@@ -231,16 +267,26 @@
-> e_c_un] ...) ; un = unannotated with expected ty
#'clauses ; clauses must stay in same order
;; len #'clauses maybe > len #'info, due to guards
- #:with info (syntax-property #'τ_e 'variants)
- #:with (~and cons-info ((Cons Cons2 [fld (~datum :) τ] ...) ...))
- (stx-map (lambda (C) (stx-assoc C #'info)) #'(Clause ...))
- #:fail-unless (id-set=? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
- #:with ((acc ...) ...) (stx-map
- (lambda (C fs)
- (stx-map (lambda (f) (format-id C "~a-~a" C f)) fs))
- #'(Cons2 ...)
- #'((fld ...) ...))
- #:with (Cons? ...) (stx-map (lambda (C) (format-id C "~a?" C)) #'(Cons2 ...))
+; #:with info (syntax-property #'τ_e 'variants)
+ #:with ((~literal #%plain-lambda) (RecName) . info-body)
+ (get-extra-info #'τ_e)
+ #:with info-unfolded (subst #'τ_e #'RecName #'info-body)
+ #: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))])
+ #'info-unfolded))
+ (syntax->datum #'(Clause ...)))
+;; #:fail-unless (id-set=? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
+ ;; #:with ((acc ...) ...) (stx-map
+ ;; (lambda (C fs)
+ ;; (stx-map (lambda (f) (format-id C "~a-~a" C f)) fs))
+ ;; #'(Cons2 ...)
+ ;; #'((fld ...) ...))
+;; #:with (Cons? ...) (stx-map (lambda (C) (format-id C "~a?" C)) #'(Cons2 ...))
#:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
#:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
#:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
@@ -250,7 +296,9 @@
#:fail-unless (and (same-types? #'(τ_guard ...))
(Bool? (stx-car #'(τ_guard ...))))
"guard expression(s) must have type bool"
- #:fail-unless (same-types? #'(τ_ec ...)) "branches have different types"
+ #:fail-unless (same-types? #'(τ_ec ...))
+ (string-append "branches have different types, given: "
+ (string-join (stx-map type->str #'(τ_ec ...)) ", "))
#:with τ_out (stx-car #'(τ_ec ...))
#:with z (generate-temporary) ; dont duplicate eval of test expr
(⊢ (let ([z e-])
@@ -293,7 +341,9 @@
; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns
-(define-typed-syntax liftedλ #:export-as λ #:datum-literals (:)
+(define-typed-syntax liftedλ #:export-as λ
+ [(_ (x:id ...) . body)
+ (type-error #:src stx #:msg "λ parameters must have type annotations")]
[(_ . rst)
#'(Λ () (ext-stlc:λ . rst))])
@@ -324,7 +374,8 @@
;; #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
;; (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
;; #:note "Could not infer instantiation of polymorphic function.")
- #:with (τ_in ... τ_out) (stx-map
+ #:with (τ_in ... τ_out) (inst-types #'(τ_solved ...) #'Xs #'(τ_inX ... τ_outX))
+ #;(stx-map
(λ (t) (substs #'(τ_solved ...) #'Xs t))
#'(τ_inX ... τ_outX))
;; ) arity check
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,19 @@
+2016-02-29
+Problem: storing variant info as properties
+- when instantiating polymorphic type, need to instantiate properties as well
+Alternate Solution: store variant syntactically in (expanded) type
+- benefit is instantiation "just works"
+- drawbacks:
+ - recursive types will expand infinitely
+ - quoting the variant stops infinite expansion but breaks the subst
+ - ie ids in the quote no longer correspond to the bound id
+ - can manually stop expansion but then types will no longer always be
+ fully expanded forms
+ - tried this a few times previously - can get VERY messy - avoid if possible
+- to make this alternate work, can manually fold/unfold recursive types
+ - cant use \mu from stlc+rec-iso bc each type is more than the mu
+ so folding/unfolding is a little different
+
2016-02-19
Implementing algebraic data types
- macro cannot define type-alias and constructor functions that produce
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -1,7 +1,13 @@
#lang racket/base
(require syntax/stx racket/list)
-(provide (all-defined-out))
+(require (prefix-in r: (only-in racket/base syntax->list)))
+(provide (except-out (all-defined-out) syntax->list))
+(define (syntax->list stx)
+ (if (syntax? stx)
+ (r:syntax->list stx)
+ stx))
+
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
@@ -24,8 +30,10 @@
(member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
(define (str-stx-assoc v stx)
(assoc v (map syntax->list (syntax->list stx)) stx-str=?))
-(define (stx-assoc v stx) ; v = id
- (assoc v (map syntax->list (syntax->list stx)) free-identifier=?))
+(define (stx-assoc v stx [cmp free-identifier=?]) ; v = id
+ (assoc v (map syntax->list (syntax->list stx)) cmp))
+(define (stx-findf f stx)
+ (findf f (syntax->list stx)))
(define (stx-length stx) (length (if (syntax? stx) (syntax->list stx) stx)))
(define (stx-length=? stx1 stx2)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -2,6 +2,8 @@
(require "rackunit-typechecking.rkt")
;; tests more or less copied from infer-tests.rkt ------------------------------
+(typecheck-fail (λ (x) x) #:with-msg "parameters must have type annotations")
+
;; top-level defines
(define (f [x : Int] → Int) x)
(typecheck-fail (f 1 2) #:with-msg "Wrong number of arguments")
@@ -12,22 +14,22 @@
(define (g [x : X] → X) x)
(check-type g : (→ X X))
-; (inferred) polymorpic instantiation
+;; (inferred) polymorpic instantiation
(check-type (g 1) : Int ⇒ 1)
(check-type (g #f) : Bool ⇒ #f) ; different instantiation
(check-type (g add1) : (→ Int Int))
(check-type (g +) : (→ Int Int Int))
-; function polymorphic in list element
+;; function polymorphic in list element
(define-type (List X)
- (Nil)
+ Nil
(Cons X (List X)))
-(define (g2 [lst : (List X)] → (List X)) lst)
-(check-type g2 : (→ (List X) (List X)))
+(define (g2 [lst : (List Y)] → (List Y)) lst)
+(check-type g2 : (→ (List Y) (List Y)))
(typecheck-fail (g2 1)
#:with-msg
- (expected "(List X)" #:given "Int"
+ (expected "(List Y)" #:given "Int"
#:note "Could not infer instantiation of polymorphic function"))
;; todo? allow polymorphic nil?
@@ -38,15 +40,16 @@
(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
-;(define (g3 [lst : (List X)] → X) (hd lst)) ; cant type this fn (what to put for nil case)
-;(check-type g3 : (→ {X} (List X) X))
-;(check-type g3 : (→ {A} (List A) A))
-;(check-not-type g3 : (→ {A B} (List A) B))
-;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
-;(check-type (g3 (nil {Int})) : Int) ; runtime fail
-;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
-;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
-;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
+;; ;; mlish cant type this fn (ie, incomplete cases on variant --- what to put for Nil case?)
+;; ;(define (g3 [lst : (List X)] → X) (hd lst))
+;; ;(check-type g3 : (→ {X} (List X) X))
+;; ;(check-type g3 : (→ {A} (List A) A))
+;; ;(check-not-type g3 : (→ {A B} (List A) B))
+;; ;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+;; ;(check-type (g3 (nil {Int})) : Int) ; runtime fail
+;; ;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
+;; ;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
+;; ;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
;; recursive fn
(define (recf [x : Int] → Int) (recf x))
@@ -62,7 +65,6 @@
;; list fns ----------
-
; map: tests whether match and define properly propagate 'expected-type
(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
(match lst with
@@ -74,13 +76,13 @@
(check-not-type map : (→ (→ A B) (List B) (List A)))
(check-not-type map : (→ (→ X X) (List X) (List X))) ; only 1 bound tyvar
-; nil without annotation tests fn-first, left-to-right arg inference
+; nil without annotation; tests fn-first, left-to-right arg inference
; does work yet, need to add left-to-right inference in #%app
(check-type (map add1 Nil) : (List Int) ⇒ (Nil {Int}))
(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil))))
: (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
-(typecheck-fail (map add1 (Cons "1" Nil)))
- ;#:with-msg (expected "Int" #:given "String")) ; TODO: fix err msg
+(typecheck-fail (map add1 (Cons "1" Nil))
+ #:with-msg (expected "Int, (List Int)" #:given "String, (List Int)"))
(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))
: (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
;; ; doesnt work yet: all lambdas need annotations
@@ -115,6 +117,85 @@
; doesnt work yet: all lambdas need annotations
;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> base]
+ [Cons x xs -> (f x (foldr f base xs))]))
+(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> acc]
+ [Cons x xs -> (foldr f (f x acc) xs)]))
+
+(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
+ (match lst with
+ [Nil -> #t]
+ [Cons x xs #:when (p? x) -> (all? p? xs)]
+ [Cons x xs -> #f]))
+
+(define (tails [lst : (List X)] → (List (List X)))
+ (match lst with
+ [Nil -> (Cons Nil Nil)]
+ [Cons x xs -> (Cons lst (tails xs))]))
+
+(define (build-list [n : Int] [f : (→ Int X)] → (List X))
+ (if (zero? (sub1 n))
+ (Cons (f 0) Nil)
+ (Cons (f (sub1 n)) (build-list (sub1 n) f))))
+(check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil))))
+(check-type (build-list 5 sub1)
+ : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil))))))
+
+(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X))
+ (match lst1 with
+ [Nil -> lst2]
+ [Cons x xs -> (Cons x (append xs lst2))]))
+
+;; n-queens --------------------
+(define-type Queen (Q Int Int))
+
+(define (safe? [q1 : Queen] [q2 : Queen] → Bool)
+ (match q1 with
+ [Q x1 y1 ->
+ (match q2 with
+ [Q x2 y2 ->
+ (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2)))))])]))
+(define (safe/list? [qs : (List Queen)] → Bool)
+ (match qs with
+ [Nil -> #t]
+ [Cons q1 rst -> (all? (λ ([q2 : Queen]) (safe? q1 q2)) rst)]))
+(define (valid? [lst : (List Queen)] → Bool)
+ (all? safe/list? (tails lst)))
+
+(define (nqueens [n : Int] → (List Queen))
+ (let* ([process-row
+ (λ ([r : Int] [all-possible-so-far : (List (List Queen))])
+ (foldr
+ (λ ([qs : (List Queen)] [new-qss : (List (List Queen))])
+ (append
+ (map (λ ([c : Int]) (Cons (Q r c) qs)) (build-list n add1))
+ new-qss))
+ Nil
+ all-possible-so-far))]
+ [all-possible (foldl process-row (Cons Nil Nil) (build-list n add1))])
+ (let ([solns (filter valid? all-possible)])
+ (match solns with
+ [Nil -> Nil]
+ [Cons x xs -> x]))))
+
+(check-type nqueens : (→ Int (List Queen)))
+(check-type (nqueens 1)
+ : (List Queen) ⇒ (Cons (Q 1 1) Nil))
+(check-type (nqueens 2) : (List Queen) ⇒ (Nil {Queen}))
+(check-type (nqueens 3) : (List Queen) ⇒ (Nil {Queen}))
+(check-type (nqueens 4)
+ : (List Queen)
+ ⇒ (Cons (Q 3 1) (Cons (Q 2 4) (Cons (Q 1 2) (Cons (Q 4 3) Nil)))))
+(check-type (nqueens 5)
+ : (List Queen)
+ ⇒ (Cons (Q 4 2) (Cons (Q 3 4) (Cons (Q 2 1) (Cons (Q 1 3) (Cons (Q 5 5) Nil))))))
+
+
;; end infer.rkt tests --------------------------------------------------
;; algebraic data types
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -412,7 +412,14 @@
(define-for-syntax (mk-? id) (format-id id "~a?" id))
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
- (and paren-shape/#f (char=? paren-shape/#f #\{))))
+ (and paren-shape/#f (char=? paren-shape/#f #\{)))
+ (define (get-extra-info t)
+ (syntax-parse t
+ [((~literal #%plain-app) internal-id
+ ((~literal #%plain-lambda) bvs
+ ((~literal #%expression) extra-info-to-extract) . rst))
+ #'extra-info-to-extract]
+ [_ #'void])))
(define-syntax define-basic-checked-id-stx
(syntax-parser #:datum-literals (:)
@@ -467,6 +474,9 @@
#:defaults ([tycon #'void]))
(~optional (~seq #:other-prop other-key other-bvs other-val)
#:defaults ([other-key #'#f]))
+ (~optional (~seq #:extra-info extra-bvs extra-info)
+ #:defaults ([extra-bvs #'()]
+ [extra-info #'void]))
)
#:with #%kind (format-id #'kind "#%~a" #'kind)
#:with τ-internal (generate-temporary #'τ)
@@ -485,7 +495,8 @@
#'(~and expanded-τ
(~parse
((~literal #%plain-app) (~literal τ-internal)
- ((~literal #%plain-lambda) (~and bvs (tv (... (... ...)))) (~literal void) . rst))
+ ((~literal #%plain-lambda) (~and bvs (tv (... (... ...))))
+ skipped-extra-info . rst))
#'expanded-τ)
#,(if (attribute has-bvs?)
(if (attribute has-annotations?)
@@ -497,7 +508,8 @@
[(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) bvs-pat)
#:defaults ([bvs-pat #'()])) . pat)
#'((~literal #%plain-app) (~literal τ-internal)
- ((~literal #%plain-lambda) bvs-pat (~literal void) . pat))])))
+ ((~literal #%plain-lambda) bvs-pat
+ skipped-extra-info . pat))])))
(define-syntax τ-expander*
(pattern-expander
(syntax-parser
@@ -546,11 +558,17 @@
#: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))
+ ;; #:with extra-info-inst (substs #'args #,#'extra-bvs #,#'extra-info)
#:with result
- (assign-type (syntax/loc stx (τ-internal (λ bvs- void . τs-))) #'k_result)
- #,(if (syntax-e #'other-key)
- #`(syntax-property #'result 'other-key (substs #'args #,#'other-bvs #,#'other-val))
- #'#'result)]
+ (assign-type (syntax/loc stx (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) #'k_result)
+ #'result]
+ ;; #,(if (syntax-e #'other-key)
+ ;; #`(syntax-property #'result 'other-key (substs #'args #,#'other-bvs #,#'other-val))
+ ;; #'#'result)]
;; else fail with err msg
[_
(type-error #:src stx
@@ -658,7 +676,8 @@
(syntax-parser
[(_ tycons x ...)
#'((~literal #%plain-app) tycons
- ((~literal #%plain-lambda) bvs (~literal void) x ...))])))
+ ((~literal #%plain-lambda) bvs
+ skipped-extra-info x ...))])))
(define (merge-type-tags stx)
(define t (syntax-property stx 'type))
(or (and (pair? t)
@@ -668,8 +687,13 @@
stx))
; subst τ for y in e, if (bound-id=? x y)
(define (subst τ x e)
+ #'(printf "subst ~a for ~a in ~a\n"
+ (syntax->datum τ)
+ x
+ (syntax->datum e))
(syntax-parse e
[y:id #:when (bound-identifier=? e x)
+ ; #:when (printf "~a = ~a\n" #'y x)
; #:when
; (displayln (syntax-property (syntax-track-origin τ #'y #'y) 'type))
; #:when (displayln (syntax-property (syntax-property (syntax-track-origin τ #'y #'y) 'type #'#%type) 'type))
@@ -682,4 +706,20 @@
[_ e]))
(define (substs τs xs e)
- (stx-fold subst e τs xs)))
+ (stx-fold subst e τs xs))
+
+ ;; subst-expr
+ ;; used for inferring recursive types
+ (define (stx=? s1 s2)
+ (or (and (identifier? s1) (identifier? s2) (free-identifier=? s1 s2))
+ (and (stx-null? s1) (stx-null? 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
+ (stx-map (lambda (e) (subst-expr e1 e2 e)) e3)]))
+ )
