From e9290629daff4d3e1846cda8b9aae0866807df83 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 30 Mar 2016 16:12:11 -0400 Subject: [PATCH] fix a few err msg issues - add working monad example - closes #7 --- tapl/ext-stlc.rkt | 2 +- tapl/mlish.rkt | 26 ++++++-- tapl/stlc.rkt | 2 +- tapl/tests/mlish/bg/monad.mlish | 112 ++++++++++++++++++++++++++++++++ tapl/tests/mlish/match2.mlish | 3 +- tapl/tests/run-mlish-tests3.rkt | 1 + tapl/typecheck.rkt | 10 +-- 7 files changed, 143 insertions(+), 13 deletions(-) create mode 100644 tapl/tests/mlish/bg/monad.mlish diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index 89c7abe..600c765 100644 --- 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 index 8aafbb0..32ffb5c 100644 --- 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 index 4547a39..9ffafbd 100644 --- 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 new file mode 100644 index 0000000..aed6d48 --- /dev/null +++ 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 index bfd6398..eba59c0 100644 --- 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 index 9978cfe..4e2c28a 100644 --- 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 index 3c3a24d..36ac6be 100644 --- 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