commit e9290629daff4d3e1846cda8b9aae0866807df83
parent d881d988c2d6189a9b32dd2725beaab156a455c8
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 30 Mar 2016 16:12:11 -0400
fix a few err msg issues
- add working monad example
- closes #7
Diffstat:
7 files changed, 143 insertions(+), 13 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -80,7 +80,7 @@
(define-typed-syntax ann
#:datum-literals (:)
[(_ e : ascribed-τ:type)
- #:with (e- τ) (infer+erase #'e)
+ #:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
#:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
(format "~a does not have type ~a\n"
(syntax->datum #'e) (syntax->datum #'ascribed-τ))
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -159,7 +159,10 @@
;; - currently cannot do it here; to do the check here, need all types of
;; 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 ...)))
+ (syntax-property
+ ((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))))
@@ -267,7 +270,7 @@
(infer+erase (syntax-property e 'expected-type τ_e)))
#'(e_arg ...) #'(τ_in.norm (... ...)))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
- (mk-app-err-msg #'(C e_arg ...)
+ (mk-app-err-msg (syntax/loc stx (C e_arg ...))
#:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
#:name (format "constructor ~a" 'Cons))
(⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
@@ -298,7 +301,7 @@
;; ; #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
;; ; #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
;; ; #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
- #'(C {τ_solved (... ...)} . args)]))
+ (syntax/loc stx (C {τ_solved (... ...)} . args))]))
...)]))
;; match --------------------------------------------------
@@ -573,7 +576,7 @@
(define-syntax → ; wrapping →
(syntax-parser
- [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+ [(_ . rst) (syntax-property #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))]))
; special arrow that computes free vars; for use with tests
; (because we can't write explicit forall
(provide →/test)
@@ -671,7 +674,20 @@
#:with ([e_arg- τ_arg] ...) (infers+erase (stx-map add-expected-ty #'(e_arg ...) #'(τ_in ...)))
;; ) typecheck args
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...))
+ (mk-app-err-msg stx
+ #:given #'(τ_arg ...)
+ #:expected
+ (stx-map
+ (lambda (tyin)
+ (define old-orig (get-orig tyin))
+ (displayln old-orig)
+ (define new-orig
+ (and old-orig
+ (substs (stx-map get-orig #'(τ_solved ...)) #'Xs old-orig
+ (lambda (x y) (equal? (syntax->datum x) (syntax->datum y))))))
+ (displayln new-orig)
+ (syntax-property tyin 'orig (list new-orig)))
+ #'(τ_in ...)))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
;; cond and other conditionals
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -80,7 +80,7 @@
(syntax-parse stx
[(app . rst)
#:when (not (equal? '#%app (syntax->datum #'app)))
- (mk-app-err-msg #'(#%app app . rst)
+ (mk-app-err-msg (syntax/loc stx (#%app app . rst))
#:expected expected-τs
#:given given-τs
#:note note
diff --git a/tapl/tests/mlish/bg/monad.mlish b/tapl/tests/mlish/bg/monad.mlish
@@ -0,0 +1,112 @@
+#lang s-exp "../../../mlish.rkt"
+(require "../../rackunit-typechecking.rkt")
+
+(define-type (Option A)
+ [None]
+ [Some A])
+
+;; -----------------------------------------------------------------------------
+
+(define-type (List a)
+ [Nil]
+ [∷ a (List a)])
+
+(define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A)
+ (match x* with
+ [Nil -> acc]
+ [∷ h t -> (foldl f (f acc h) t)]))
+
+(define (reverse [x* : (List A)] → (List A))
+ (foldl (λ ([acc : (List A)] [x : A]) (∷ x acc)) Nil x*))
+
+;; =============================================================================
+;; === BatchedQueue
+
+(define-type (BatchedQueue A)
+ [BQ (List A) (List A)])
+
+(define (bq-check [f : (List A)] [r : (List A)] → (BatchedQueue A))
+ (match f with
+ [Nil -> (BQ (reverse r) Nil)]
+ [∷ h t -> (BQ f r)]))
+
+(define (bq-empty → (BatchedQueue A))
+ (BQ Nil Nil))
+
+(define (bq-isEmpty [bq : (BatchedQueue A)] → Bool)
+ (match bq with
+ [BQ f r ->
+ (match f with
+ [Nil -> #t]
+ [∷ h t -> #f])]))
+
+(define (bq-snoc [bq : (BatchedQueue A)] [x : A] → (BatchedQueue A))
+ (match bq with
+ [BQ f r -> (bq-check f (∷ x r))]))
+
+(define (bq-head [bq : (BatchedQueue A)] → (Option A))
+ (match bq with
+ [BQ f r ->
+ (match f with
+ [Nil -> None]
+ [∷ h t -> (Some h)])]))
+
+(define (bq-tail [bq : (BatchedQueue A)] → (Option (BatchedQueue A)))
+ (match bq with
+ [BQ f* r* ->
+ (match f* with
+ [Nil -> None]
+ [∷ x f* ->
+ (Some (bq-check f* r*))])]))
+
+(define (list->bq [x* : (List A)] → (BatchedQueue A))
+ (foldl
+ (λ ([q : (BatchedQueue A)] [x : A]) (bq-snoc q x))
+ (bq-empty) x*))
+
+;; -----------------------------------------------------------------------------
+
+(define digit*
+ (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil))))))))))
+
+(check-type digit* : (List Int))
+
+(define sample-bq
+ (list->bq digit*))
+
+(check-type sample-bq : (BatchedQueue Int))
+
+(check-type (Some sample-bq) : (Option (BatchedQueue Int)))
+
+(define (>> [f : (→ A (Option B))] [x : (Option A)] → (Option B))
+ (match x with
+ [None -> None]
+ [Some y -> (f y)]))
+
+(check-type >> : (→/test (→ X (Option Y)) (Option X) (Option Y)))
+
+(check-type (bq-tail sample-bq) : (Option (BatchedQueue Int)))
+
+;; can't pass polymorphic fn? need to inst first
+(check-type (>> (inst bq-tail Int) (Some sample-bq))
+ : (Option (BatchedQueue Int)))
+
+;(ann (>> bq-tail (Some sample-bq)) : (Option (BatchedQueue Int)))
+
+(define intbq-tail (inst bq-tail Int))
+
+(check-type intbq-tail :
+ (→/test (BatchedQueue Int) (Option (BatchedQueue Int))))
+
+(check-type (>> intbq-tail (Some sample-bq))
+ : (Option (BatchedQueue Int)))
+
+(check-type (inst bq-head Int) : (→/test (BatchedQueue Int) (Option Int)))
+
+(define bq-tails-result
+ (>> intbq-tail (>> intbq-tail (>> intbq-tail (Some sample-bq)))))
+
+(check-type bq-tails-result : (Option (BatchedQueue Int))
+ ⇒ (Some (BQ (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))) Nil)))
+
+(check-type (>> (inst bq-head Int) bq-tails-result) : (Option Int) -> (Some 4))
diff --git a/tapl/tests/mlish/match2.mlish b/tapl/tests/mlish/match2.mlish
@@ -113,7 +113,8 @@
(check-type
(match2 (list 1 2) with
[nil -> -1]
- [x :: xs -> x]) : Int -> 1)
+ [x :: xs -> x])
+ : Int -> 1)
(check-type
(match2 (list 1 2) with
diff --git a/tapl/tests/run-mlish-tests3.rkt b/tapl/tests/run-mlish-tests3.rkt
@@ -2,3 +2,4 @@
;; bg
(require "mlish/bg/huffman.mlish")
(require "mlish/bg/lambda.mlish")
+(require "mlish/bg/monad.mlish")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -704,19 +704,19 @@
(syntax-property stx 'type (car t)))
stx))
; subst τ for y in e, if (bound-id=? x y)
- (define (subst τ x e)
+ (define (subst τ x e [cmp bound-identifier=?])
(syntax-parse e
- [y:id #:when (bound-identifier=? e x)
+ [y:id #:when (cmp e x)
; use syntax-track-origin to transfer 'orig
; but may transfer multiple #%type tags, so merge
(merge-type-tags (syntax-track-origin τ #'y #'y))]
[(esub ...)
- #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
+ #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1 cmp)) #'(esub ...))
(syntax-track-origin #'(esub_subst ...) e x)]
[_ e]))
- (define (substs τs xs e)
- (stx-fold subst e τs xs))
+ (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
