use add-constraints in infer.rkt
This commit is contained in:
AlexKnauth
parent
20015aa39a
commit
34f969efba
|
|
@ -6,6 +6,7 @@
|
|||
(require (only-in "stlc+cons.rkt" ~List))
|
||||
(reuse tup × proj #:from "stlc+tup.rkt")
|
||||
(reuse define-type-alias #:from "stlc+reco+var.rkt")
|
||||
(require (for-syntax "type-constraints.rkt"))
|
||||
(provide hd tl nil?)
|
||||
(provide →)
|
||||
|
||||
|
|
@ -15,8 +16,8 @@
|
|||
(syntax-parser
|
||||
[(_ (~and Xs {X:id ...}) . rst)
|
||||
#:when (brace? #'Xs)
|
||||
#'(∀ (X ...) (ext-stlc:→ . rst))]
|
||||
[(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
|
||||
(add-orig #'(∀ (X ...) (ext-stlc:→ . rst)) (get-orig this-syntax))]
|
||||
[(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
|
||||
|
||||
(define-primop + : (→ Int Int Int))
|
||||
(define-primop - : (→ Int Int Int))
|
||||
|
|
@ -28,34 +29,6 @@
|
|||
(define-primop not : (→ Bool Bool))
|
||||
(define-primop abs : (→ Int Int))
|
||||
|
||||
(begin-for-syntax
|
||||
(define (compute-constraint τ1-τ2)
|
||||
(syntax-parse τ1-τ2
|
||||
[(X:id τ) #'((X τ))]
|
||||
[((~List τ1) (~List τ2)) (compute-constraint #'(τ1 τ2))]
|
||||
; should only be monomorphic?
|
||||
[((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
|
||||
(compute-constraints #'((τ1 τ2) ...))]
|
||||
[_ #'()]))
|
||||
(define (compute-constraints τs)
|
||||
;(printf "constraints: ~a\n" (syntax->datum τs))
|
||||
(stx-appendmap compute-constraint τs))
|
||||
|
||||
(define (solve-constraint x-τ)
|
||||
(syntax-parse x-τ
|
||||
[(X:id τ) #'((X τ))]
|
||||
[_ #'()]))
|
||||
(define (solve-constraints cs)
|
||||
(stx-appendmap compute-constraint cs))
|
||||
|
||||
(define (lookup x substs)
|
||||
(syntax-parse substs
|
||||
[((y:id τ) . rst)
|
||||
#:when (free-identifier=? #'y x)
|
||||
#'τ]
|
||||
[(_ . rst) (lookup x #'rst)]
|
||||
[() false])))
|
||||
|
||||
(define-typed-syntax define
|
||||
[(_ x:id e)
|
||||
#:with (e- τ) (infer+erase #'e)
|
||||
|
|
@ -68,7 +41,9 @@
|
|||
#:with g (generate-temporary #'f)
|
||||
#:with e_ann #'(add-expected e τ_out)
|
||||
#'(begin
|
||||
(define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
|
||||
(define-syntax f (make-rename-transformer
|
||||
(⊢ g : #,(add-orig #'(∀ (X ...) (ext-stlc:→ τ ... τ_out))
|
||||
#'(→ τ ... τ_out)))))
|
||||
(define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
|
||||
[(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
|
||||
#:with g (generate-temporary #'f)
|
||||
|
|
@ -86,7 +61,7 @@
|
|||
(syntax->datum #'fn))
|
||||
#:with (τ_arg ...) #'given-τ-args
|
||||
#:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
|
||||
(⊢ λ- : (∀ () τ_λ))]
|
||||
(⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))]
|
||||
[(~and fn (_ (x:id ...) e) ~!) ; no annotations, couldnt infer from ctx (eg, unapplied lam), try to infer from body
|
||||
#:with (xs- e- τ_res) (infer/ctx+erase #'([x : x] ...) #'e)
|
||||
#:with env (get-env #'e-)
|
||||
|
|
@ -100,11 +75,12 @@
|
|||
;; propagate up inferred types of variables
|
||||
#:with res (add-env #'(λ xs- e-) #'env)
|
||||
; #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : x] ...) e))
|
||||
(⊢ res : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
|
||||
(⊢ res : #,(add-orig #'(∀ () (ext-stlc:→ τ_arg ... τ_res))
|
||||
#`(→ #,@(stx-map get-orig #'(τ_arg ... τ_res)))))]
|
||||
;(⊢ (λ xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
|
||||
[(_ . rst)
|
||||
#:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ . rst))
|
||||
(⊢ λ- : (∀ () τ_λ))])
|
||||
(⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))])
|
||||
|
||||
(define-typed-syntax #%app
|
||||
[(_ e_fn e_arg ...) ; infer args first
|
||||
|
|
@ -131,9 +107,8 @@
|
|||
(syntax->datum #'(e_arg ...))
|
||||
(stx-map type->str #'(τ_arg ...)))
|
||||
"\n")))
|
||||
#:with cs (compute-constraints #'((τ_inX τ_arg) ...))
|
||||
#:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
|
||||
#:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
|
||||
#:with cs (add-constraints #'(X ...) '() #'([τ_inX τ_arg] ...))
|
||||
#:with (τ_in ... τ_out) (inst-types/cs #'(X ...) #'cs #'(τ_inX ... τ_outX))
|
||||
; some code duplication
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(type-error #:src stx
|
||||
|
|
@ -186,14 +161,12 @@
|
|||
[else
|
||||
(define/with-syntax [e τ] (infer+erase e_arg))
|
||||
; (displayln #'(e τ))
|
||||
(define/with-syntax (c ...) cs)
|
||||
(define/with-syntax (new-c ...) (compute-constraint #`(#,τ_inX τ)))
|
||||
(values #'(new-c ... c ...) (cons #'[e τ] e+τs))]))])
|
||||
(define cs* (add-constraints #'(X ...) cs #`([#,τ_inX τ])))
|
||||
(values cs* (cons #'[e τ] e+τs))]))])
|
||||
(define/with-syntax e+τs/stx e+τs)
|
||||
(list cs (reverse (syntax->list #'e+τs/stx))))
|
||||
#:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e_arg- ...))))
|
||||
#:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
|
||||
#:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
|
||||
#:with (τ_in ... τ_out) (inst-types/cs #'(X ...) #'cs #'(τ_inX ... τ_outX))
|
||||
; some code duplication
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(string-append
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@
|
|||
; function polymorphic in list element
|
||||
(define {X} (g2 [lst : (List X)] → (List X)) lst)
|
||||
(check-type g2 : (→ {X} (List X) (List X)))
|
||||
(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
|
||||
(typecheck-fail (g2 1) #:with-msg "expected: \\(List X\\)\n *given: Int") ; TODO: more precise err msg
|
||||
(check-type (g2 (nil {Int})) : (List Int) ⇒ (nil {Int}))
|
||||
(check-type (g2 (nil {Bool})) : (List Bool) ⇒ (nil {Bool}))
|
||||
(check-type (g2 (nil {(List Int)})) : (List (List Int)) ⇒ (nil {(List Int)}))
|
||||
|
|
@ -64,7 +64,7 @@
|
|||
(countdown (sub1 x))))
|
||||
(check-type (countdown 0) : Int ⇒ 0)
|
||||
(check-type (countdown 10) : Int ⇒ 0)
|
||||
(typecheck-fail (countdown "10") #:with-msg "Arguments.+have wrong type")
|
||||
(typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String")
|
||||
|
||||
; list abbrv
|
||||
(check-type (list 1 2 3) : (List Int))
|
||||
|
|
@ -88,7 +88,11 @@
|
|||
(check-type (map add1 nil) : (List Int) ⇒ (nil {Int}))
|
||||
(check-type (map add1 (list)) : (List Int) ⇒ (nil {Int}))
|
||||
(check-type (map add1 (list 1 2 3)) : (List Int) ⇒ (list 2 3 4))
|
||||
(typecheck-fail (map add1 (list "1")) #:with-msg "Arguments.+have wrong type")
|
||||
(typecheck-fail (map add1 (list "1")) #:with-msg
|
||||
(string-append
|
||||
"couldn't unify Int and String\n"
|
||||
" *expected: \\(→ X Y\\), \\(List X\\)\n"
|
||||
" *given: \\(→ Int Int\\), \\(List String\\)"))
|
||||
(check-type (map (λ ([x : Int]) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
|
||||
; doesnt work yet
|
||||
;; 2015-12-18: dont need annotations on lambdas with concrete type
|
||||
|
|
@ -209,11 +213,11 @@
|
|||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) 2)
|
||||
#:with-msg
|
||||
"Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
|
||||
"expected: Unit\n *given: Int")
|
||||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) void)
|
||||
#:with-msg
|
||||
"Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
|
||||
"expected: Unit\n *given: \\(→ Unit\\)")
|
||||
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
|
|
@ -251,7 +255,7 @@
|
|||
(typecheck-fail
|
||||
(let ([x #f]) (+ x 1))
|
||||
#:with-msg
|
||||
"Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
|
||||
"expected: Int, Int\n *given: Bool, Int")
|
||||
(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
|
||||
#:with-msg "x: unbound identifier")
|
||||
|
||||
|
|
@ -259,7 +263,7 @@
|
|||
(typecheck-fail
|
||||
(let* ([x #t] [y (+ x 1)]) 1)
|
||||
#:with-msg
|
||||
"Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
|
||||
"expected: Int, Int\n *given: Bool, Int")
|
||||
|
||||
; letrec
|
||||
(typecheck-fail
|
||||
|
|
@ -332,7 +336,7 @@
|
|||
(typecheck-fail
|
||||
((λ ([x : Bool]) x) 1)
|
||||
#:with-msg
|
||||
"Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
|
||||
"expected: Bool\n *given: Int")
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
|
||||
(typecheck-fail
|
||||
(λ ([f : Int]) (f 1 2))
|
||||
|
|
@ -347,11 +351,11 @@
|
|||
(typecheck-fail
|
||||
(+ 1 (λ ([x : Int]) x))
|
||||
#:with-msg
|
||||
"Arguments to function \\+ have wrong type.+Given:\n 1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
|
||||
"expected: Int, Int\n *given: Int, \\(→ Int Int\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg
|
||||
"Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
|
||||
"expected: Int, Int\n *given: \\(→ Int Int\\), \\(→ Int Int\\)")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "Wrong number of arguments")
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user