projects
/
scheme.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Fix total pattern match verification
[scheme.git]
/
typecheck.scm
diff --git
a/typecheck.scm
b/typecheck.scm
index b3466751fdf7f4161963d3904c13f970b8798a76..b2b001f1d27220211e5f67e651d641c9895f5b5c 100644
(file)
--- a/
typecheck.scm
+++ b/
typecheck.scm
@@
-1,4
+1,5
@@
(load "ast.scm")
(load "ast.scm")
+(load "stdlib.scm")
(define (abs? t)
(and (list? t) (eq? (car t) 'abs)))
(define (abs? t)
(and (list? t) (eq? (car t) 'abs)))
@@
-194,10
+195,14
@@
(define (get-bindings product-types pattern)
(define (go product-type product)
(define (get-bindings product-types pattern)
(define (go product-type product)
-
(case (ast-type x
)
+
(case (ast-type product
)
['var (list (cons product product-type))]
; an inner pattern match
['var (list (cons product product-type))]
; an inner pattern match
- ['app (get-bindings product-type product)]))
+ ['app (let* ([inner-sum (car product)]
+ [inner-sums (cdr (assoc product-type dls))]
+ [inner-product-types (cdr (assoc inner-sum inner-sums))])
+ (get-bindings inner-product-types product))]
+ [else '()]))
(flat-map go product-types (cdr pattern)))
(flat-map go product-types (cdr pattern)))
@@
-211,6
+216,7
@@
(let* ([names (cdr pattern)]
[product-types (cdr sum)]
[new-env (append (get-bindings product-types pattern) env)])
(let* ([names (cdr pattern)]
[product-types (cdr sum)]
[new-env (append (get-bindings product-types pattern) env)])
+
(check dls new-env expr)))]
; pattern match with binding and no constructor
['var (check dls (env-insert env pattern switch-type) expr)]
(check dls new-env expr)))]
; pattern match with binding and no constructor
['var (check dls (env-insert env pattern switch-type) expr)]
@@
-253,7
+259,6
@@
((res
(case (ast-type x)
('int-literal (make-result '() 'Int))
((res
(case (ast-type x)
('int-literal (make-result '() 'Int))
- ('bool-literal (make-result '() 'Bool))
('string-literal (make-result '() 'String))
('builtin (make-result '() (builtin-type x)))
('string-literal (make-result '() 'String))
('builtin (make-result '() (builtin-type x)))
@@
-313,8
+318,9
@@
(flat-map data-tors-type-env (program-data-layouts prog)))
; we typecheck the lambda calculus only (only single arg lambdas)
(flat-map data-tors-type-env (program-data-layouts prog)))
; we typecheck the lambda calculus only (only single arg lambdas)
-(define (typecheck prog)
- (let ([expanded (expand-pattern-matches prog)])
+(define (typecheck prog-without-stdlib)
+ (let* ([prog (append stdlib prog-without-stdlib)]
+ [expanded (expand-pattern-matches prog)])
(cadr (check (program-data-layouts prog)
(init-adts-env expanded)
(normalize (program-body expanded))))))
(cadr (check (program-data-layouts prog)
(init-adts-env expanded)
(normalize (program-body expanded))))))