diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index 018ed4c..735aea7 100644 --- a/tapl/mlish.rkt +++ b/tapl/mlish.rkt @@ -1,7 +1,7 @@ #lang s-exp "typecheck.rkt" (require (for-syntax syntax/id-set)) -(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and +(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and #%datum #:rename [~→ ~ext-stlc:→]) (reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt") (require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias) @@ -12,7 +12,7 @@ ;(provide hd tl nil?) (provide →) (provide define-type match) -(provide (rename-out [ext-stlc:let let] [ext-stlc:and and])) +(provide (rename-out [ext-stlc:let let] [ext-stlc:and and] [ext-stlc:#%datum #%datum])) ;; ML-like language ;; - top level recursive functions @@ -231,15 +231,22 @@ (syntax-parse stx #:datum-literals (with ->) [(_ e with . clauses) #:fail-when (null? (syntax->list #'clauses)) "no clauses" - #:with ([Clause:id x ... - (~optional (~seq #:when e_guard) #:defaults ([e_guard #'#t])) - -> e_c_un] ...) ; un = unannotated with expected ty - (stx-sort #'clauses symbol 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 (stx-length=? #'(Clause ...) #'(Cons ...)) "wrong number of case clauses" + ;; #:fail-unless #;(free-id-set=? (immutable-free-id-set (syntax->list #'(Clause ...))) + ;; (immutable-free-id-set (syntax->list #'(Cons ...)))) + ;; ;; (id-set-size=? #'(Clause ...) #'(Cons ...)) + ;; "wrong number of case clauses" +; #:fail-unless (typechecks? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive" + #: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)) @@ -248,17 +255,23 @@ #: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_c- τ_ec) ...) - (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ] ...) ...) #'(e_c ...)) + #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...) + (stx-map + (λ (bs eg+ec) (infers/ctx+erase bs eg+ec)) + #'(([x : τ] ...) ...) #'((e_guard e_c) ...)) + #: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" ;; #:with C (syntax-property #'τ_e 'constructor) ; check if variant is known statically ;; #:with (acc ...) (syntax-property #'τ_e 'accessors) ;; #:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...)) #:with τ_out (stx-car #'(τ_ec ...)) + #:with z (generate-temporary) ; dont duplicate eval of test expr (⊢ (let ([z e-]) (cond [(and (Cons? z) - (let ([x- (acc z)] ...) e_guard)) + (let ([x- (acc z)] ...) e_guard-)) (let ([x- (acc z)] ...) e_c-)] ...)) : τ_out)])) @@ -319,8 +332,8 @@ (format "Expected expression ~a to have → type, got: ~a" (syntax->datum #'e_fn) (type->str #'τ_fn)) #:with (~∀ Xs (~ext-stlc:→ τ_inX ... τ_outX)) #'τ_fn - #:with (τ_solved ...) (solve #'Xs #'(τ_inX ...) (syntax/loc stx (e_fn e_arg ...))) ;; ) instantiate polymorphic fn type + #:with (τ_solved ...) (solve #'Xs #'(τ_inX ...) (syntax/loc stx (e_fn e_arg ...))) ;; #:with cs (compute-constraints #'((τ_inX τ_arg) ...)) ;; #:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))) ;; #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...)) @@ -329,36 +342,14 @@ #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'Xs t)) #'(τ_inX ... τ_outX)) + ;; ) arity check #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) (mk-app-err-msg stx #:expected #'(τ_inX ...) ; #:given #'(τ_arg ...) #:note "Wrong number of arguments.") ;; ) compute argument types; (possibly) double-expand args (for now) #:with ([e_arg- τ_arg] ...) (infers+erase (stx-map add-expected-ty #'(e_arg ...) #'(τ_in ...))) - ;; ) arity check - #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) - (mk-app-err-msg stx #:expected #'(τ_inX ...) - #:given #'(τ_arg ...) - #:note "Wrong number of arguments.") ;; ) typecheck args #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) (mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...)) (⊢ (#%app e_fn- e_arg- ...) : τ_out)]) - - - ;; ;; 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 ...) τ ...)) - ;; (let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)] - ;; [τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)] - ;; [old-cs #'()]) - ;; (define/with-syntax [a- τ_a] (infer+erase a)) - ;; (define cs (stx-append old-cs (compute-constraints (list (list τ+ #'τ_a))))) - ;; (define maybe-solved (filter syntax-e (stx-map (λ (y) (lookup y cs)) #'Ys))) - ;; (if (stx-length=? maybe-solved #'Ys) - ;; #`(C #,(syntax-property #`{#,@maybe-solved} 'paren-shape #\{) . args) ; loses 'paren-shape - ;; (if (or (stx-null? a-rst) (stx-null? τ+rst)) - ;; (type-error #:src stx - ;; #:msg "could not infer types for constructor ~a; add annotations" #'(C . args)) - ;; (loop (stx-car a-rst) (stx-cdr a-rst) (stx-car τ+rst) (stx-cdr τ+rst) cs))))])) - diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt index bb1b5c4..9ef6e02 100644 --- a/tapl/tests/mlish-tests.rkt +++ b/tapl/tests/mlish-tests.rkt @@ -92,6 +92,11 @@ [Cons x xs -> (if (p? x) (Cons x (filter p? xs)) (filter p? xs))])) +(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X)) + (match lst with + [Nil -> Nil] + [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))] + [Cons x xs -> (filter p? xs)])) (check-type (filter zero? Nil) : (List Int) ⇒ (Nil {Int})) (check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) : (List Int) ⇒ (Nil {Int})) @@ -99,6 +104,14 @@ : (List Int) ⇒ (Cons 0 Nil)) (check-type (filter (λ ([x : Int]) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) +(check-type (filter/guard zero? Nil) : (List Int) ⇒ (Nil {Int})) +(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List Int) ⇒ (Nil {Int})) +(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 0 Nil)) +(check-type + (filter/guard (λ ([x : Int]) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) ; doesnt work yet: all lambdas need annotations ;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 9a106f4..369ecc9 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -2,7 +2,7 @@ (require (for-syntax (except-in racket extends) syntax/parse racket/syntax syntax/stx racket/stxparam - syntax/parse/debug + syntax/parse/debug syntax/id-set "stx-utils.rkt") (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt") (for-meta 3 racket/base syntax/parse racket/syntax) @@ -12,7 +12,7 @@ (except-out (all-from-out racket/base) #%module-begin) (for-syntax (all-defined-out)) (all-defined-out) (for-syntax - (all-from-out racket syntax/parse racket/syntax syntax/stx + (all-from-out racket syntax/parse racket/syntax syntax/stx syntax/id-set "stx-utils.rkt")) (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax))) @@ -157,6 +157,11 @@ (define (typeof stx #:tag [tag 'type]) (define ty (syntax-property stx tag)) (if (cons? ty) (car ty) ty)) + + ;; fns for working with id sets + (define (id-set=? ids1 ids2) + (free-id-set=? (immutable-free-id-set (syntax->list ids1)) + (immutable-free-id-set (syntax->list ids2)))) (define type-pat "[A-Za-z]+")