delete old directory
This commit is contained in:
AlexKnauth
parent
8a24117188
commit
4c5b8ae2e5
|
|
@ -1,53 +0,0 @@
|
|||
***** 2014-08-21 *****
|
||||
|
||||
Language hierarchy + accompanying test file:
|
||||
(each language extension should run all the previous langs' test files)
|
||||
|
||||
stlc.rkt
|
||||
stlc+mod-begin.rkt
|
||||
stlc+define.rkt
|
||||
sysf.rkt
|
||||
|
||||
***** 2014-08-20 *****
|
||||
- still trying to solve the issue with the impl of forall instantiation
|
||||
- summary below of failures so far
|
||||
|
||||
#### Attempt #1:
|
||||
|
||||
naive substitution during instantiation (ie redex's "subst-vars")
|
||||
|
||||
# Extended Description / Why I Thought It Would Work:
|
||||
- instantiation is just substitution, so why not re-use the built-in
|
||||
substitution of pattern variables/templates?
|
||||
- this does naive substitution, ie renames everything, even binders
|
||||
- I thought it would be ok since, types are just names
|
||||
eg (forall (X) (-> X (forall (X) (-> X X)))) applied to Int becomes
|
||||
(-> Int (forall (Int) (-> Int Int))), which is valid
|
||||
|
||||
# Failed Because:
|
||||
- if you apply a forall to a non-identifier type, ie (-> Int Int),
|
||||
the result is an invalid type
|
||||
|
||||
##### Attempt #2:
|
||||
|
||||
Define forall as a macro that when it expands, renames binders and refs to
|
||||
something unique (ala gensym).
|
||||
|
||||
# Extended Description:
|
||||
- requires manual expansion since I took over the expansion of the program
|
||||
via local-expand
|
||||
|
||||
# Failed Because:
|
||||
- every type must get expanded before use, which means that every type
|
||||
constructor must get redefined to expand its subtypes
|
||||
- not sure how to do this for user-defined types
|
||||
|
||||
# Other Notes:
|
||||
- I think this means I can't expect to do any preprocessing
|
||||
|
||||
##### Attempt #3:
|
||||
|
||||
Just manually substitute, checking for the binding forms (ie forall) to avoid
|
||||
capture.
|
||||
|
||||
Working so far.
|
||||
|
|
@ -1,341 +0,0 @@
|
|||
#lang racket
|
||||
(require
|
||||
racket/stxparam
|
||||
(for-syntax
|
||||
;racket/base
|
||||
syntax/parse syntax/parse/experimental/template
|
||||
racket/syntax syntax/stx;racket/stxparam syntax/id-table
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse))
|
||||
(require "typecheck.rkt")
|
||||
(provide (except-out (all-from-out racket) #%module-begin))
|
||||
|
||||
;; Extension of Racket for implementing typed languages
|
||||
|
||||
(provide define-typed-syntax ;define-typed-top-level-syntax
|
||||
define-primop ;define-syntax/type-rule
|
||||
declare-base-type declare-base-types)
|
||||
;$this (for-syntax extends))
|
||||
(provide (rename-out [mb/ext #%module-begin]))
|
||||
;; provide syntax-classes
|
||||
(provide (for-syntax integer str boolean))
|
||||
|
||||
;; lit-set : [Listof identifier]
|
||||
(define-for-syntax lit-set null)
|
||||
(define-syntax (declare-base-type stx)
|
||||
(syntax-parse stx
|
||||
[(_ τ)
|
||||
(set! lit-set (cons #'τ lit-set))
|
||||
#'(begin (define τ #f) (provide τ))]))
|
||||
(define-syntax-rule (declare-base-types τ ...)
|
||||
(begin (declare-base-type τ) ...))
|
||||
|
||||
;(begin-for-syntax
|
||||
; (define defined-names (make-free-id-table)))
|
||||
;(define-syntax-parameter
|
||||
; $this
|
||||
; (λ (stx)
|
||||
; (syntax-parse stx
|
||||
; [(_ x)
|
||||
; #:when (printf "~a\n" (free-id-table-ref defined-names #'λ))
|
||||
; (free-id-table-ref defined-names #'x)])))
|
||||
|
||||
(begin-for-syntax
|
||||
;; concrete-τ? : determines if a type is a concrete type or has pattern vars
|
||||
;; result is used to determine whether to insert ellipses in the output pattern
|
||||
(define (concrete-τ? τ)
|
||||
(or (and (identifier? τ) (member τ lit-set free-identifier=?))
|
||||
(and (not (identifier? τ)) (stx-andmap concrete-τ? τ))))
|
||||
;; ** syntax-class: type ----------------------------------------
|
||||
(define-syntax-class type
|
||||
(pattern any))
|
||||
;; **syntax-class: meta-term ----------------------------------------
|
||||
;; - is the term pattern in meta-language
|
||||
;; (ie where the type rules are declared)
|
||||
;; - matches type vars
|
||||
(define-syntax-class meta-term #:datum-literals (:)
|
||||
;; cases
|
||||
(pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+ (~optional (~and ldots (~literal ...))))
|
||||
#:with (~datum cases) #'name
|
||||
#:attr args-pat/notypes (template (e_test [Cons (x ...) body ...] ... (?? ldots)))
|
||||
#:attr typevars-pat #'())
|
||||
;; define-type
|
||||
(pattern (name:id τ_name:id τ_body)
|
||||
#:attr args-pat/notypes #'()
|
||||
#:attr typevars-pat #'(τ_name τ_body))
|
||||
;; define-like binding form
|
||||
(pattern (name:id (f:id [x:id : τ] ... (~optional (~and ldots (~literal ...)))) : τ_result e ...)
|
||||
#:attr args-pat/notypes (template ((f x ... (?? ldots)) e ...))
|
||||
#:attr typevars-pat (template (τ_result τ ... (?? ldots))))
|
||||
;; lambda-like binding form
|
||||
(pattern (name:id ([x:id : τ] ... (~optional (~and ldots (~literal ...)))) e ...)
|
||||
#:attr args-pat/notypes (template ((x ... (?? ldots)) e ...))
|
||||
#:attr typevars-pat (template (τ ... (?? ldots))))
|
||||
;; let-like binding form
|
||||
(pattern (name:id ([x:id ex] ... (~optional (~and ldots (~literal ...)))) e ...)
|
||||
#:attr args-pat/notypes (template (([x ex] ... (?? ldots)) e ...))
|
||||
#:attr typevars-pat #'())
|
||||
;; the list of ids after the name is in curly parens and represents a type declaration
|
||||
;; for the arguments (which can be any type)
|
||||
;; example: cons
|
||||
(pattern (name:id τs e ...)
|
||||
#:when (curly-parens? #'τs)
|
||||
#:attr args-pat/notypes #'(e ...)
|
||||
#:attr typevars-pat #'τs)
|
||||
(pattern (name:id e ...)
|
||||
#:attr args-pat/notypes #'(e ...)
|
||||
#:attr typevars-pat #'()))
|
||||
;; **syntax-class: term ----------------------------------------
|
||||
;; - matches concrete terms in the actual (typed) language
|
||||
;; - matches concrete types
|
||||
;; name identifier is the extended form
|
||||
(define-syntax-class term #:datum-literals (:)
|
||||
;; cases
|
||||
(pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+)
|
||||
#:with (~datum cases) #'name
|
||||
#:with e_test+ (expand/df #'e_test)
|
||||
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
|
||||
#:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
|
||||
#:with ((lam (x+ ...) body+ ... body_result+) ...)
|
||||
(stx-map (λ (bods xs τs)
|
||||
(with-extended-type-env
|
||||
(stx-map list xs τs)
|
||||
(expand/df #`(λ #,xs #,@bods))))
|
||||
#'((body ...) ...)
|
||||
#'((x ...) ...)
|
||||
#'((τ ...) ...))
|
||||
#:attr expanded-args #'(e_test+ [Cons+ (x+ ...) body+ ... body_result+] ...)
|
||||
#:attr types #'())
|
||||
;; define-type
|
||||
(pattern (name:id τ_name:id τ_body)
|
||||
;;don't expand
|
||||
#:attr expanded-args #'()
|
||||
#:attr types #'(τ_name τ_body))
|
||||
;; define-like binding form
|
||||
(pattern (name:id (f:id [x:id : τ] ...) : τ_result e ...)
|
||||
; #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
|
||||
; (expand/df #'(λ (f x ...) e ...)))
|
||||
; ;; identifiers didnt get a type bc racket has no %#var form
|
||||
; #:with es++ (with-extended-type-env #'([x τ] ...)
|
||||
; (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
|
||||
; #:attr expanded-args #'(xs+ . es++)
|
||||
;; don't expand
|
||||
#:attr expanded-args #'((f x ...) e ...)
|
||||
#:attr types #'(τ_result τ ...))
|
||||
;; lambda-like binding form
|
||||
(pattern (name:id ([x:id : τ] ...) e ...)
|
||||
#:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e ...)))
|
||||
;; identifiers didnt get a type bc racket has no %#var form
|
||||
#:with es++ (with-extended-type-env #'([x τ] ...)
|
||||
(stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
|
||||
#:attr expanded-args #'(xs+ . es++)
|
||||
#:attr types #'(τ ...))
|
||||
;;let-like binding form
|
||||
(pattern (name:id ([x:id ex] ...) e ...)
|
||||
#:with (ex+ ...) (stx-map expand/df #'(ex ...))
|
||||
#:with (τ ...) (stx-map typeof #'(ex+ ...))
|
||||
#:with (lam (x+ ...) . es+) (with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e ...)))
|
||||
;; identifiers didnt get a type bc racket has no %#var form
|
||||
#:with es++ (with-extended-type-env #'([x τ] ...)
|
||||
(stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
|
||||
#:attr expanded-args #'(([x+ ex+] ...) . es++)
|
||||
#:attr types #'())
|
||||
;; the list of ids after the name is in curly parens and represents a type declaration
|
||||
;; for the arguments (which can be any type)
|
||||
;; example: cons
|
||||
(pattern (name:id τs e ...)
|
||||
#:when (curly-parens? #'τs)
|
||||
#:with (e+ ...) (stx-map expand/df #'(e ...))
|
||||
#:attr expanded-args #'(e+ ...)
|
||||
#:attr types #'τs)
|
||||
(pattern (name:id e ...)
|
||||
#:with (e+ ...) (stx-map expand/df #'(e ...))
|
||||
#:attr expanded-args #'(e+ ...)
|
||||
#:attr types #'()))
|
||||
;; **syntax-class: τ-constraint ----------------------------------------
|
||||
(define-splicing-syntax-class
|
||||
τ-constraint
|
||||
#:datum-literals (:= : let typeof == Γ-extend with when:)
|
||||
(pattern (when: e)
|
||||
#:attr pattern-directive #'(#:when e))
|
||||
(pattern (with pat e)
|
||||
#:attr pattern-directive #'(#:with pat e))
|
||||
(pattern (let τ := (typeof e))
|
||||
#:attr pattern-directive #'(#:with τ (typeof #'e)))
|
||||
(pattern (e : τ)
|
||||
#:attr pattern-directive #'(#:when (assert-type #'e #'τ)))
|
||||
(pattern (τ1 == τ2)
|
||||
#:attr pattern-directive #'(#:fail-unless (type=? #'τ1 #'τ2)
|
||||
(format "type ~a and ~a should be equal"
|
||||
(syntax->datum #'τ1) (syntax->datum #'τ2))))
|
||||
(pattern (Γ-extend [f : τ] ... (~optional (~and ldots (~literal ...))))
|
||||
#:attr pattern-directive
|
||||
#`(#:when (Γ (type-env-extend #'([f τ] ... #,@(template ((?? ldots))))))))
|
||||
(pattern (~seq (let τ := (typeof e)) (~literal ...))
|
||||
#:attr pattern-directive #'(#:with (τ (... ...)) (stx-map typeof #'(e (... ...)))))
|
||||
(pattern (~seq (e0 : τ0) (~and ldots (~literal ...)))
|
||||
#:when (concrete-τ? #'τ0)
|
||||
#:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 ldots))))
|
||||
;; not concrete-τ
|
||||
(pattern (~seq (e0 : τ0) (~and ldots (~literal ...)))
|
||||
#:attr pattern-directive #'(#:when (stx-andmap assert-type #'(e0 ldots) #'(τ0 ldots))))))
|
||||
|
||||
|
||||
;; define-typed-syntax
|
||||
(define-syntax (define-typed-syntax stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ meta-e:meta-term : meta-τ
|
||||
(~optional (~seq #:where
|
||||
c:τ-constraint ...))
|
||||
(~optional (~seq #:expanded expanded-e)))
|
||||
#:with fresh-name (generate-temporary #'meta-e.name)
|
||||
; #:when (free-id-table-set! defined-names #'meta-e.name #'fresh-name)
|
||||
#:with lits lit-set
|
||||
#`(begin
|
||||
(provide (rename-out [fresh-name meta-e.name]))
|
||||
(define-syntax (fresh-name stx)
|
||||
(syntax-parse stx #:literals lits
|
||||
[e:term
|
||||
;; shadow pattern vars representing subterms with its expansion
|
||||
;; - except for the name of the form, since result must use base form
|
||||
#:with meta-e.args-pat/notypes #'e.expanded-args
|
||||
#:with meta-e.typevars-pat #'e.types
|
||||
#,@(template ((?? (?@ . ((?@ . c.pattern-directive) ...)))))
|
||||
(⊢ (syntax/loc
|
||||
stx
|
||||
#,@(template ((?? expanded-e
|
||||
(meta-e.name . meta-e.args-pat/notypes)))))
|
||||
#'meta-τ)]
|
||||
[_ #:when (type-error #:src stx #:msg "type error") #'(void)]
|
||||
)))]))
|
||||
|
||||
|
||||
;; overload mod-begin to check for define-literal-type-rule and other top-level forms
|
||||
(begin-for-syntax
|
||||
(define-syntax-class def #:datum-literals (define-literal-type-rule extends inherit-types)
|
||||
(pattern (extends m f ...)
|
||||
; #:when (stx-map
|
||||
; (λ (f)
|
||||
; (free-id-table-set!
|
||||
; defined-names
|
||||
; f
|
||||
; (format-id #'m "ext:~a" f)))
|
||||
; #'(f ...))
|
||||
#:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr inherited-τs #'()
|
||||
#:attr base-mod #'(m) #:attr ext-fs #'(f ...))
|
||||
(pattern (inherit-types τ ...)
|
||||
#:attr inherited-τs #'(τ ...)
|
||||
#:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'())
|
||||
(pattern (define-literal-type-rule stx-class : τ)
|
||||
#:attr other #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'()
|
||||
#:attr stxc #'(stx-class)
|
||||
#:attr lit-τ #'(τ))
|
||||
(pattern any
|
||||
#:attr other #'(any)
|
||||
#:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'())))
|
||||
|
||||
(define-syntax (mb/ext stx)
|
||||
(syntax-parse stx
|
||||
[(_ d:def ...)
|
||||
#:with (stxc ...) (template ((?@ . d.stxc) ...))
|
||||
#:with (lit-τ ...) (template ((?@ . d.lit-τ) ...))
|
||||
#:with (base-mod ...) (template ((?@ . d.base-mod) ...))
|
||||
#:with (inherited-τ ...) (template ((?@ . d.inherited-τs) ...))
|
||||
#:when (set! lit-set (append (syntax->list #'(inherited-τ ...)) lit-set))
|
||||
;; check that
|
||||
#:fail-unless (let ([len (stx-length #'(base-mod ...))]) (or (zero? len) (= len 1)))
|
||||
(format "Supply either 0 or 1 base modules. Given ~a"
|
||||
(syntax->datum #'(base-mod ...)))
|
||||
#:with m (if (zero? (stx-length #'(base-mod ...)))
|
||||
#'()
|
||||
(car (syntax->list #'(base-mod ...))))
|
||||
#:with (f ...) (template ((?@ . d.ext-fs) ...))
|
||||
#:with (ext-f ...) (stx-map (λ (f) (format-id #'m "ext:~a" f)) #'(f ...))
|
||||
; (template ((?@ . d.ext-fs) ...)))
|
||||
#:with my-datum (generate-temporary)
|
||||
#:with datum-def
|
||||
#`(define-syntax (my-datum stx)
|
||||
(syntax-parse stx
|
||||
[(_ . x) #:declare x stxc (⊢ (syntax/loc stx (r:#%datum . x)) #'lit-τ)]
|
||||
...
|
||||
;; try previous version of #%datum, if it exists, ie if we are extending
|
||||
#,@(if (stx-null? #'m)
|
||||
#'()
|
||||
#`([(_ . x)
|
||||
(syntax/loc stx (#,(datum->syntax #'m 'ext:#%datum) . x))]))
|
||||
[(_ . x)
|
||||
#:when (type-error #:src stx #:msg "Don't know the type for literal: ~a" #'x)
|
||||
(syntax/loc stx (r:#%datum . x))]))
|
||||
#:with my-mb (generate-temporary)
|
||||
#:with mb-def
|
||||
#'(define-syntax (my-mb stx)
|
||||
(syntax-parse stx
|
||||
[(_ def (... ...))
|
||||
#:with mb-let (expand/df #'(r:let () def (... ...) (r:void)))
|
||||
#'(r:#%module-begin mb-let)]))
|
||||
#`(#%module-begin
|
||||
; (require (for-syntax syntax/id-table))
|
||||
; (begin-for-syntax
|
||||
; (define defined-names (make-free-id-table)))
|
||||
#,@(if (stx-null? #'m)
|
||||
#'()
|
||||
#`((require (only-in m inherited-τ ...))
|
||||
(provide inherited-τ ...)
|
||||
(require racket/provide)
|
||||
(require (prefix-in ext: (except-in m inherited-τ ...)))
|
||||
(provide
|
||||
(filtered-out
|
||||
(lambda (name)
|
||||
#;(printf "inheriting from ~a: ~a\n"
|
||||
#,(syntax->datum #'m)
|
||||
(and (regexp-match? #rx"^ext:.+$" name)
|
||||
(regexp-replace #rx"ext:" name "")))
|
||||
(and (regexp-match? #rx"^ext:.+$" name)
|
||||
(regexp-replace #rx"ext:" name "")))
|
||||
(except-out (all-from-out m)
|
||||
ext-f ...
|
||||
#,(datum->syntax #'m 'ext:#%datum)
|
||||
#,(datum->syntax #'m 'ext:#%module-begin)
|
||||
#,(datum->syntax #'m 'ext:check-type-error)
|
||||
#,(datum->syntax #'m 'ext:check-type)
|
||||
#,(datum->syntax #'m 'ext:check-not-type)
|
||||
#,(datum->syntax #'m 'ext:check-type-and-result))))))
|
||||
(require (prefix-in r: racket/base))
|
||||
(provide (rename-out [r:#%top-interaction #%top-interaction]))
|
||||
(provide (rename-out [my-datum #%datum]))
|
||||
datum-def
|
||||
(provide (rename-out [my-mb #%module-begin]))
|
||||
mb-def
|
||||
#,@(template ((?@ . d.other) ...))
|
||||
;; testing forms --------------------
|
||||
(require (for-syntax rackunit))
|
||||
(require rackunit)
|
||||
(provide check-equal?)
|
||||
(provide check-type-error check-type check-not-type check-type-and-result)
|
||||
(define-syntax (check-type-error stx)
|
||||
(syntax-parse stx
|
||||
[(_ e)
|
||||
#:when (check-exn exn:fail? (λ () (expand/df #'e)))
|
||||
#'(void)]))
|
||||
(define-syntax (check-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-true (assert-type #'e+ #'τ)
|
||||
(format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
(define-syntax (check-not-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-false (type=? (typeof #'e+) #'τ)
|
||||
(format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
(define-syntax (check-type-and-result stx)
|
||||
(syntax-parse stx #:datum-literals (: =>)
|
||||
[(_ e : τ => v)
|
||||
#'(begin (check-type e : τ)
|
||||
(check-equal? e v))]))
|
||||
)]))
|
||||
|
|
@ -1,180 +0,0 @@
|
|||
#lang s-exp "stlc+define+cons.rkt"
|
||||
|
||||
(check-type-error ((λ ([x : Int]) (+ x 1)) "10"))
|
||||
(check-type ((λ ([x : Int]) (+ x 1)) 10) : Int)
|
||||
(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11) ; identifier used out of context
|
||||
(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
|
||||
|
||||
; check fns with literal or id bodies
|
||||
(check-type (λ ([x : Int]) x) : (Int → Int))
|
||||
(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
|
||||
|
||||
;; check fns with multi-expr body
|
||||
(check-type (λ ([x : Int]) (void) x) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) 1 x))
|
||||
(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
|
||||
|
||||
(check-type (λ ([x : Int]) (printf {Int} "~a\n" x) x) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) (printf {String} "~a\n" x) x))
|
||||
(check-type-error (λ ([x : Int]) (printf {Int} 1 x) x))
|
||||
(check-type (λ ([x : Int]) (printf "one") x) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) (printf "~a" x) x))
|
||||
(check-type-and-result (printf "Testing printf (expecting 100): ") : Unit => (void))
|
||||
(check-type-and-result ((λ ([x : Int]) (printf {Int} "~a\n" x) (+ x 1)) 100) : Int => 101)
|
||||
|
||||
;; multi arity primops
|
||||
(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
|
||||
(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
|
||||
(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
|
||||
(check-type-error (λ ([y : Int] [z : Int]) (= y)))
|
||||
(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
|
||||
(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
|
||||
(check-type-error (λ ([y : Int] [z : Int]) (< y)))
|
||||
(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
|
||||
(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
|
||||
(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
|
||||
;; the following still fails bc varargs not handled
|
||||
;; fixed: 2014-09-04
|
||||
(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
|
||||
(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
|
||||
(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
|
||||
(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
|
||||
|
||||
; HO fn
|
||||
(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
|
||||
(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
|
||||
(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
|
||||
(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
|
||||
|
||||
;; shadowed var
|
||||
(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
|
||||
(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
|
||||
|
||||
;; let
|
||||
(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
|
||||
(check-type-error (let ([x 1] [y "two"]) (+ x y)))
|
||||
(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
|
||||
|
||||
;; lists
|
||||
(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
|
||||
(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
|
||||
(check-type-error (cons {Int} 1 (null {String})))
|
||||
(check-type-error (cons {Int} "one" (null {Int})))
|
||||
(check-type-error (cons {String} 1 (null {Int})))
|
||||
(check-type-error (cons {String} 1 (null {Int})))
|
||||
(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
|
||||
(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
|
||||
: String => "one")
|
||||
(check-type-and-result (null? {String} (null {String})) : Bool => #t)
|
||||
(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
|
||||
(check-type-error (null? {String} (null {Int})))
|
||||
(check-type-error (null? {Int} (null {String})))
|
||||
(check-type-error (null? {Int} 1))
|
||||
(check-type-error (null? {Int} "one"))
|
||||
(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
|
||||
|
||||
; begin and void
|
||||
(check-type (void) : Unit)
|
||||
(check-type-and-result (begin (void) 1) : Int => 1)
|
||||
(check-type-and-result (begin (void) (void) 1) : Int => 1)
|
||||
(check-type-and-result (begin (void) (void) (void)) : Unit => (void))
|
||||
(check-type-and-result (begin (+ 1 2)) : Int => 3)
|
||||
(check-type-error (begin 1 2))
|
||||
|
||||
(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) 1 1))
|
||||
(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
|
||||
(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
|
||||
: Int => 6)
|
||||
|
||||
; define
|
||||
(define (g [y : Int]) : Int
|
||||
(+ (f y) 1))
|
||||
(define (f [x : Int]) : Int
|
||||
(+ x 1))
|
||||
(check-type-and-result (f 10) : Int => 11)
|
||||
(check-type-and-result (g 100) : Int => 102)
|
||||
(check-not-type (f 10) : String)
|
||||
(check-not-type (g 100) : String)
|
||||
|
||||
;; if
|
||||
(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
|
||||
(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
|
||||
(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
|
||||
(check-type-error (if (null? {Int} (null {Int})) "one" 1))
|
||||
(check-type-error (if 1 2 3))
|
||||
|
||||
;;; recursive fn
|
||||
(define (add1 [x : Int]) : Int
|
||||
(+ x 1))
|
||||
(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
|
||||
(if (null? {Int} lst)
|
||||
(null {Int})
|
||||
(cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
|
||||
(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
|
||||
: (Listof Int)
|
||||
=> (cons {Int} 2 (cons {Int} 3 (null {Int}))))
|
||||
(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
|
||||
: (Listof String))
|
||||
|
||||
;; recursive types
|
||||
(define (a [x : Int]) : Int (b x))
|
||||
(define (b [x : Int]) : Int (a x))
|
||||
(define (ff [x : Int]) : Int (ff x))
|
||||
|
||||
;; define-type (non parametric)
|
||||
(define-type MaybeInt (variant (None) (Just Int)))
|
||||
(check-type (None) : MaybeInt)
|
||||
(check-type (Just 10) : MaybeInt)
|
||||
(check-type-error (Just "ten"))
|
||||
(check-type-error (Just (None)))
|
||||
(define (maybeint->bool [maybint : MaybeInt]) : Bool
|
||||
(cases maybint
|
||||
[None () #f]
|
||||
[Just (x) #t]))
|
||||
(check-type-and-result (maybeint->bool (None)) : Bool => #f)
|
||||
(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
|
||||
(check-type-error (maybeint->bool 25))
|
||||
(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
|
||||
(cases maybint
|
||||
[None () #f]
|
||||
[Just (x) x])))
|
||||
|
||||
(define-type IntList (variant (Null) (Cons Int IntList)))
|
||||
(check-type-and-result (Null) : IntList => (Null))
|
||||
(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
|
||||
(check-type-error (Cons "one" (Null)))
|
||||
(check-type-error (Cons 1 2))
|
||||
(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
|
||||
(cases lst
|
||||
[Null () (Null)]
|
||||
[Cons (x xs) (Cons (f x) (map/IntList f xs))]))
|
||||
(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
|
||||
(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
|
||||
(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null))))
|
||||
: IntList => (Cons 3 (Cons 2 (Null))))
|
||||
(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
|
||||
(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
|
||||
(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
|
||||
(cases lst
|
||||
[BoolNull () (Null)]
|
||||
[BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
|
||||
(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
|
||||
(check-type-and-result
|
||||
(map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
|
||||
: IntList => (Cons 1 (Null)))
|
||||
(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
|
||||
;; check typename is available
|
||||
(check-type (λ ([lst : IntList])
|
||||
(cases lst
|
||||
[Null () (None)]
|
||||
[Cons (x xs) (Just x)]))
|
||||
: (IntList → MaybeInt))
|
||||
(check-type ((λ ([lst : IntList])
|
||||
(cases lst
|
||||
[Null () (None)]
|
||||
[Cons (x xs) (Just x)]))
|
||||
(Null)) : MaybeInt)
|
||||
|
|
@ -1,183 +0,0 @@
|
|||
#lang s-exp "stlc+define+cons-via-racket-extended.rkt"
|
||||
|
||||
(check-type-error ((λ ([x : Int]) (+ x 1)) "10"))
|
||||
(check-type ((λ ([x : Int]) (+ x 1)) 10) : Int)
|
||||
(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11)
|
||||
(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
|
||||
|
||||
;; check fns with literal or id bodies
|
||||
(check-type (λ ([x : Int]) x) : (Int → Int))
|
||||
(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
|
||||
|
||||
;; check fns with multi-expr body
|
||||
(check-type (λ ([x : Int]) (void) x) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) 1 x))
|
||||
(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
|
||||
|
||||
; printf
|
||||
;(check-type (λ ([x : Int]) (printf {Int} "~a\n" x) x) : (Int → Int))
|
||||
;(check-type-error (λ ([x : Int]) (printf {String} "~a\n" x) x))
|
||||
;(check-type-error (λ ([x : Int]) (printf {Int} 1 x) x))
|
||||
;(check-type (λ ([x : Int]) (printf "one") x) : (Int → Int))
|
||||
;(check-type-error (λ ([x : Int]) (printf "~a" x) x))
|
||||
;(check-type-and-result ((λ ([x : Int]) (printf {Int} "~a\n" x) (+ x 1)) 100) : Int => 101)
|
||||
|
||||
;; multi arity primops
|
||||
(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
|
||||
(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
|
||||
(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
|
||||
(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
|
||||
(check-type-error (λ ([y : Int] [z : Int]) (= y)))
|
||||
(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
|
||||
(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
|
||||
(check-type-error (λ ([y : Int] [z : Int]) (< y)))
|
||||
(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
|
||||
(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
|
||||
(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
|
||||
;; the following HO example still fails bc varargs not handled
|
||||
;; fixed: 2014-09-04
|
||||
(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
|
||||
(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
|
||||
(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
|
||||
(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
|
||||
|
||||
;; HO fn
|
||||
(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
|
||||
(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
|
||||
(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
|
||||
(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
|
||||
|
||||
;; shadowed var
|
||||
(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
|
||||
(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
|
||||
|
||||
;; let
|
||||
(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
|
||||
(check-type-error (let ([x 1] [y "two"]) (+ x y)))
|
||||
(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
|
||||
|
||||
;;; lists
|
||||
(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
|
||||
(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
|
||||
(check-type-error (cons {Int} 1 (null {String})))
|
||||
(check-type-error (cons {Int} "one" (null {Int})))
|
||||
(check-type-error (cons {String} 1 (null {Int})))
|
||||
(check-type-error (cons {String} 1 (null {Int})))
|
||||
(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
|
||||
(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
|
||||
: String => "one")
|
||||
(check-type-and-result (null? {String} (null {String})) : Bool => #t)
|
||||
(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
|
||||
(check-type-error (null? {String} (null {Int})))
|
||||
(check-type-error (null? {Int} (null {String})))
|
||||
(check-type-error (null? {Int} 1))
|
||||
(check-type-error (null? {Int} "one"))
|
||||
(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
|
||||
|
||||
;; begin and void
|
||||
(check-type (void) : Unit)
|
||||
(check-type-and-result (begin (void) 1) : Int => 1)
|
||||
(check-type-and-result (begin (void) (void) 1) : Int => 1)
|
||||
(check-type-and-result (begin (void) (void) (void)) : Unit => (void))
|
||||
(check-type-and-result (begin (+ 1 2)) : Int => 3)
|
||||
(check-type-error (begin 1 2))
|
||||
|
||||
(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
|
||||
(check-type-error (λ ([x : Int]) 1 1))
|
||||
(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
|
||||
(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
|
||||
: Int => 6)
|
||||
|
||||
;; define
|
||||
(define (g [y : Int]) : Int
|
||||
(+ (f y) 1))
|
||||
(define (f [x : Int]) : Int
|
||||
(+ x 1))
|
||||
(check-type-and-result (f 10) : Int => 11)
|
||||
(check-type-and-result (g 100) : Int => 102)
|
||||
(check-not-type (f 10) : String)
|
||||
(check-not-type (g 100) : String)
|
||||
|
||||
;; if
|
||||
(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
|
||||
(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
|
||||
(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
|
||||
(check-type-error (if (null? {Int} (null {Int})) "one" 1))
|
||||
(check-type-error (if 1 2 3))
|
||||
(check-type-and-result (if #t 1 2) : Int => 1)
|
||||
(check-type-and-result (if #f 1 2) : Int => 2)
|
||||
(check-type-error (if #t 1 #f))
|
||||
|
||||
;;; recursive fn
|
||||
(define (add1 [x : Int]) : Int
|
||||
(+ x 1))
|
||||
(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
|
||||
(if (null? {Int} lst)
|
||||
(null {Int})
|
||||
(cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
|
||||
(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
|
||||
: (Listof Int)
|
||||
=> (cons {Int} 2 (cons {Int} 3 (null {Int}))))
|
||||
(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
|
||||
: (Listof String))
|
||||
|
||||
;; recursive types
|
||||
(define (a [x : Int]) : Int (b x))
|
||||
(define (b [x : Int]) : Int (a x))
|
||||
(define (ff [x : Int]) : Int (ff x))
|
||||
|
||||
;; define-type (non parametric)
|
||||
(define-type MaybeInt (variant (None) (Just Int)))
|
||||
(check-type (None) : MaybeInt)
|
||||
(check-type (Just 10) : MaybeInt)
|
||||
(check-type-error (Just "ten"))
|
||||
(check-type-error (Just (None)))
|
||||
(define (maybeint->bool [maybint : MaybeInt]) : Bool
|
||||
(cases maybint
|
||||
[None () #f]
|
||||
[Just (x) #t]))
|
||||
(check-type-and-result (maybeint->bool (None)) : Bool => #f)
|
||||
(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
|
||||
(check-type-error (maybeint->bool 25))
|
||||
(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
|
||||
(cases maybint
|
||||
[None () #f]
|
||||
[Just (x) x])))
|
||||
|
||||
(define-type IntList (variant (Null) (Cons Int IntList)))
|
||||
(check-type-and-result (Null) : IntList => (Null))
|
||||
(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
|
||||
(check-type-error (Cons "one" (Null)))
|
||||
(check-type-error (Cons 1 2))
|
||||
(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
|
||||
(cases lst
|
||||
[Null () (Null)]
|
||||
[Cons (x xs) (Cons (f x) (map/IntList f xs))]))
|
||||
(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
|
||||
(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
|
||||
(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null))))
|
||||
: IntList => (Cons 3 (Cons 2 (Null))))
|
||||
(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
|
||||
(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
|
||||
(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
|
||||
(cases lst
|
||||
[BoolNull () (Null)]
|
||||
[BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
|
||||
(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
|
||||
(check-type-and-result
|
||||
(map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
|
||||
: IntList => (Cons 1 (Null)))
|
||||
(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
|
||||
;; check typename is available
|
||||
(check-type (λ ([lst : IntList])
|
||||
(cases lst
|
||||
[Null () (None)]
|
||||
[Cons (x xs) (Just x)]))
|
||||
: (IntList → MaybeInt))
|
||||
(check-type ((λ ([lst : IntList])
|
||||
(cases lst
|
||||
[Null () (None)]
|
||||
[Cons (x xs) (Just x)]))
|
||||
(Null)) : MaybeInt)
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
#lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
|
||||
(extends "stlc-via-racket-extended.rkt" λ +)
|
||||
(inherit-types Int →)
|
||||
(require (for-syntax syntax/stx "stx-utils.rkt") "typecheck.rkt")
|
||||
|
||||
;; Simply-Typed Lambda Calculus+
|
||||
;; - stlc extended with practical language feature
|
||||
;; - implemented in racket-extended lang
|
||||
;; Features:
|
||||
;; - stlc
|
||||
;; - multi-expr lam bodies
|
||||
;; - printing
|
||||
;; - cons + listops
|
||||
;; - more prim types (bool, string)
|
||||
;; - more prim ops
|
||||
;; - user (recursive) function definitions
|
||||
;; - user (recursive) (variant) type-definitions + cases
|
||||
;; - var args: TODO: primops can handle multiple args but not general application
|
||||
|
||||
(declare-base-types String Bool Listof Unit)
|
||||
(define-for-syntax (assert-Unit-type e) (assert-type e #'Unit))
|
||||
|
||||
(define-literal-type-rule boolean : Bool)
|
||||
(define-literal-type-rule str : String)
|
||||
|
||||
;; define-type ----------------------------------------------------------------
|
||||
(define-typed-syntax
|
||||
(define-type τ (variant (Cons τ_fld ...) ...)) : Unit
|
||||
#:where
|
||||
(Γ-extend [Cons : (τ_fld ... → τ)] ...)
|
||||
(with (flds ...) (stx-map generate-temporaries #'((τ_fld ...) ...)))
|
||||
#:expanded
|
||||
(begin (struct Cons flds #:transparent) ...))
|
||||
|
||||
(define-typed-syntax
|
||||
(cases e_test [Cons (x ...) e_body ... e_result] ...) : τ_res
|
||||
#:where
|
||||
(when: (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((e_body ...) ...)))
|
||||
(let (τ ... → τ_Cons) := (typeof Cons)) ...
|
||||
(when: (or (null? (syntax->list #'(τ_Cons ...)))
|
||||
(andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_Cons ...)))))
|
||||
(cdr (syntax->list #'(τ_Cons ...))))))
|
||||
(when: (assert-type #'e_test (stx-car #'(τ_Cons ...))))
|
||||
(let τ_result := (typeof e_result)) ...
|
||||
(when: (or (null? (syntax->list #'(τ_result ...)))
|
||||
(andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
|
||||
(cdr (syntax->list #'(τ_result ...))))))
|
||||
(with τ_res (stx-car #'(τ_result ...)))
|
||||
#:expanded
|
||||
(match e_test [(Cons x ...) e_body ... e_result] ...))
|
||||
|
||||
;; typed forms ----------------------------------------------------------------
|
||||
(define-typed-syntax
|
||||
(begin e ... e_result) : τ_result
|
||||
#:where
|
||||
(e : Unit) ...
|
||||
(let τ_result := (typeof e_result)))
|
||||
|
||||
#;(define-syntax (printf/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ τs str . args)
|
||||
#:when (curly-parens? #'τs)
|
||||
#:with str+ (expand/df #'str)
|
||||
#:when (assert-String-type #'str+)
|
||||
#:with args+ (stx-map expand/df #'args)
|
||||
#:when (stx-andmap assert-type #'args+ #'τs)
|
||||
(⊢ (syntax/loc stx (printf str+ . args+)) #'Unit)]
|
||||
[(_ str . args)
|
||||
#:fail-unless (null? (syntax->list #'args)) "Please provide type annotations for arguments"
|
||||
#:with str+ (expand/df #'str)
|
||||
#:when (assert-String-type #'str+)
|
||||
(⊢ (syntax/loc stx (printf str+)) #'Unit)]))
|
||||
|
||||
(define-primop + : (Int ... → Int))
|
||||
(define-primop - : (Int Int ... → Int))
|
||||
(define-primop = : (Int Int Int ... → Bool))
|
||||
(define-primop < : (Int Int Int ... → Bool))
|
||||
(define-primop or : (Bool ... → Bool))
|
||||
(define-primop and : (Bool ... → Bool))
|
||||
(define-primop not : (Bool → Bool))
|
||||
(define-primop abs : (Int → Int))
|
||||
(define-primop void : (→ Unit))
|
||||
|
||||
(define-typed-syntax
|
||||
(λ ([x : τ] ...) e ... e_result) : (τ ... → τ_body)
|
||||
#:where
|
||||
(e : Unit) ...
|
||||
(let τ_body := (typeof e_result)))
|
||||
|
||||
(define-typed-syntax
|
||||
(let ([x ex] ...) e ... e_result) : τ_result
|
||||
#:where
|
||||
(e : Unit) ...
|
||||
(let τ_result := (typeof e_result)))
|
||||
|
||||
(define-typed-syntax
|
||||
(if e_test e1 e2) : τ2
|
||||
#:where
|
||||
(e_test : Bool)
|
||||
(let τ1 := (typeof e1))
|
||||
(let τ2 := (typeof e2))
|
||||
(τ1 == τ2))
|
||||
|
||||
;; lists ----------------------------------------------------------------------
|
||||
(define-typed-syntax
|
||||
(cons {τ} e1 e2) : (Listof τ)
|
||||
#:where
|
||||
(e1 : τ)
|
||||
(e2 : (Listof τ)))
|
||||
(define-typed-syntax
|
||||
(null {τ}) : (Listof τ)
|
||||
#:expanded
|
||||
null)
|
||||
(define-typed-syntax
|
||||
(null? {τ} e) : Bool
|
||||
#:where
|
||||
(e : (Listof τ)))
|
||||
(define-typed-syntax
|
||||
(first {τ} e) : τ
|
||||
#:where
|
||||
(e : (Listof τ)))
|
||||
(define-typed-syntax
|
||||
(rest {τ} e) : (Listof τ)
|
||||
#:where
|
||||
(e : (Listof τ)))
|
||||
|
||||
;; define ---------------------------------------------------------------------
|
||||
(define-typed-syntax
|
||||
(define (f [x : τ] ...) : τ_result e ...) : Unit
|
||||
#:where
|
||||
(Γ-extend [f : (τ ... → τ_result)])
|
||||
#:expanded
|
||||
(define f (ext:λ ([x : τ] ...) e ...)))
|
||||
|
|
@ -1,363 +0,0 @@
|
|||
#lang racket/base
|
||||
(require
|
||||
racket/match
|
||||
(for-syntax racket/base syntax/parse syntax/parse/experimental/template
|
||||
racket/set syntax/stx racket/syntax
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse)
|
||||
"typecheck.rkt")
|
||||
|
||||
(require (except-in "stlc.rkt" #%app #%datum λ #%module-begin +))
|
||||
(require (prefix-in stlc: "stlc.rkt"))
|
||||
(provide (all-from-out "stlc.rkt"))
|
||||
|
||||
(provide
|
||||
define-type cases
|
||||
(rename-out
|
||||
[datum/tc #%datum]
|
||||
#;[void/tc void] [printf/tc printf]
|
||||
[λ/tc λ] [let/tc let]
|
||||
; for #%app, must prefix and re-provide because this file needs to use racket's #%app
|
||||
[stlc:#%app #%app]
|
||||
; [app/tc #%app]
|
||||
[define/tc define]
|
||||
[begin/tc begin]
|
||||
[if/tc if]
|
||||
[datum/tc #%datum] [module-begin/tc #%module-begin]
|
||||
[cons/tc cons] [null/tc null] [null?/tc null?] [first/tc first] [rest/tc rest] [list/tc list]))
|
||||
|
||||
;; Simply-Typed Lambda Calculus+
|
||||
;; - stlc extended with practical language feature
|
||||
;; - implemented in racket
|
||||
;; Features:
|
||||
;; - stlc
|
||||
;; - multi-expr lam bodies
|
||||
;; - printing
|
||||
;; - cons + listops
|
||||
;; - more prim types (bool, string)
|
||||
;; - more prim ops
|
||||
;; - user (recursive) function definitions
|
||||
;; - user (recursive) (variant) type-definitions + cases
|
||||
;; - var args: TODO: primops can handle multiple args but not general application
|
||||
|
||||
(define-and-provide-builtin-types String Bool Listof Unit)
|
||||
(provide (for-syntax assert-Unit-type assert-String-type))
|
||||
(define-for-syntax (assert-Unit-type e) (assert-type e #'Unit))
|
||||
(define-for-syntax (assert-String-type e) (assert-type e #'String))
|
||||
|
||||
;; define-type ----------------------------------------------------------------
|
||||
(define-syntax (define-type stx)
|
||||
(syntax-parse stx #:datum-literals (variant)
|
||||
[(_ τ:id (variant (Cons:id τ_fld ...) ...))
|
||||
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
|
||||
#:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)] ...)))
|
||||
#'(begin
|
||||
(struct Cons (x ...) #:transparent) ...)]
|
||||
[(_ τ:id (Cons:id τ_fld ...))
|
||||
#:with (x ...) (generate-temporaries #'(τ_fld ...))
|
||||
#:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
|
||||
#'(begin
|
||||
(struct Cons (x ...) #:transparent))]))
|
||||
(define-syntax (cases stx)
|
||||
(syntax-parse stx #:literals (→)
|
||||
[(_ e [Cons (x ...) body ... body_result] ...)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
|
||||
#:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
|
||||
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
|
||||
#:with ((lam (x+ ...) body+ ... body_result+) ...)
|
||||
(stx-map (λ (bods xs τs)
|
||||
(with-extended-type-env
|
||||
(stx-map list xs τs)
|
||||
(expand/df #`(λ #,xs #,@bods))))
|
||||
#'((body ... body_result) ...)
|
||||
#'((x ...) ...)
|
||||
#'((τ ...) ...))
|
||||
#:when (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((body+ ...) ...))
|
||||
#:with (τ_result ...) (stx-map typeof #'(body_result+ ...))
|
||||
#:when (or (null? (syntax->list #'(τ_result ...)))
|
||||
(andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
|
||||
(cdr (syntax->list #'(τ_result ...)))))
|
||||
(⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
|
||||
(car (syntax->list #'(τ_result ...))))]))
|
||||
|
||||
;; typed forms ----------------------------------------------------------------
|
||||
(define-syntax (datum/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
|
||||
[(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)]
|
||||
[(_ . x) #'(stlc:#%datum . x)]))
|
||||
|
||||
(define-syntax (begin/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ e ... e_result)
|
||||
#:with (e+ ... e_result+) (stx-map expand/df #'(e ... e_result))
|
||||
#:when (stx-andmap assert-Unit-type #'(e+ ...))
|
||||
(⊢ (syntax/loc stx (begin e+ ... e_result+)) (typeof #'e_result+))]))
|
||||
|
||||
#;(define-syntax (void/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
|
||||
|
||||
(define-syntax (printf/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ τs str . args)
|
||||
#:when (curly-parens? #'τs)
|
||||
#:with str+ (expand/df #'str)
|
||||
#:when (assert-String-type #'str+)
|
||||
#:with args+ (stx-map expand/df #'args)
|
||||
#:when (stx-andmap assert-type #'args+ #'τs)
|
||||
(⊢ (syntax/loc stx (printf str+ . args+)) #'Unit)]
|
||||
[(_ str . args)
|
||||
#:fail-unless (null? (syntax->list #'args)) "Please provide type annotations for arguments"
|
||||
#:with str+ (expand/df #'str)
|
||||
#:when (assert-String-type #'str+)
|
||||
(⊢ (syntax/loc stx (printf str+)) #'Unit)]))
|
||||
|
||||
(define-primop + : (Int ... → Int))
|
||||
(define-primop - : (Int Int ... → Int))
|
||||
(define-primop = : (Int Int Int ... → Bool))
|
||||
(define-primop < : (Int Int Int ... → Bool))
|
||||
(define-primop or : (Bool ... → Bool))
|
||||
(define-primop and : (Bool ... → Bool))
|
||||
(define-primop not : (Bool → Bool))
|
||||
(define-primop abs : (Int → Int))
|
||||
(define-primop void : (→ Unit))
|
||||
|
||||
|
||||
(define-syntax (λ/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ ([x:id : τ] ...) e ... e_result)
|
||||
;; the with-extended-type-env must be outside the expand/df (instead of
|
||||
;; around just the body) bc ow the parameter will get restored to the old
|
||||
;; value before the local-expand happens
|
||||
#:with (lam xs . es+) (with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e ... e_result)))
|
||||
;; manually handle identifiers here
|
||||
;; - since Racket has no #%var hook, ids didn't get "expanded" in the previous line
|
||||
;; and thus didn't get a type
|
||||
;; TODO: can I put this somewhere else where it's more elegant?
|
||||
#:with (e++ ... e_result++) (with-extended-type-env #'([x τ] ...)
|
||||
(stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
|
||||
;; manually handle the implicit begin
|
||||
#:when (stx-map assert-Unit-type #'(e++ ...))
|
||||
#:with τ_body (typeof #'e_result++)
|
||||
(⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(τ ... → τ_body))]))
|
||||
|
||||
;; #%app
|
||||
#;(define-syntax (app/tc stx)
|
||||
(syntax-parse stx #:literals (→)
|
||||
[(_ e_fn e_arg ...)
|
||||
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
|
||||
|
||||
#:with (τ ... → τ_res) (typeof #'e_fn+)
|
||||
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
|
||||
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
|
||||
[(_ e ...) #'(stlc:#%app e ...)]))
|
||||
|
||||
(define-syntax (let/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ ([x:id e_x] ...) e ... e_result)
|
||||
#:with (e_x+ ...) (stx-map expand/df #'(e_x ...))
|
||||
#:with (τ ...) (stx-map typeof #'(e_x+ ...))
|
||||
#:with (lam (x+ ...) e+ ... e_result+)
|
||||
(with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e ... e_result)))
|
||||
#:when (stx-andmap assert-Unit-type #'(e+ ...))
|
||||
(⊢ (syntax/loc stx (let ([x+ e_x+] ...) e+ ... e_result+)) (typeof #'e_result+))]))
|
||||
|
||||
(define-syntax (if/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ e_test e1 e2)
|
||||
#:with e_test+ (expand/df #'e_test)
|
||||
#:when (assert-type #'e_test+ #'Bool)
|
||||
#:with e1+ (expand/df #'e1)
|
||||
#:with e2+ (expand/df #'e2)
|
||||
#:when (or (type=? (typeof #'e1+) (typeof #'e2+))
|
||||
(type-error #:src stx
|
||||
#:msg "IF branches have differing types: branch ~a has type ~a and branch ~a has type ~a"
|
||||
#'e1 (typeof #'e1+)
|
||||
#'e2 (typeof #'e2+)))
|
||||
(⊢ (syntax/loc stx (if e_test+ e1+ e2+)) (typeof #'e1+))]))
|
||||
|
||||
;; lists ----------------------------------------------------------------------
|
||||
(define-syntax (cons/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {T} e1 e2)
|
||||
#:with e1+ (expand/df #'e1)
|
||||
#:with e2+ (expand/df #'e2)
|
||||
#:when (assert-type #'e1+ #'T)
|
||||
#:when (assert-type #'e2+ #'(Listof T))
|
||||
(⊢ (syntax/loc stx (cons e1+ e2+)) #'(Listof T))]))
|
||||
(define-syntax (null/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {T}) (⊢ (syntax/loc stx null) #'(Listof T))]))
|
||||
(define-syntax (list/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {τ}) #'(null/tc {τ})]
|
||||
[(_ {τ} x . rst) #'(cons/tc {τ} x (list/tc {τ} . rst))]))
|
||||
(define-syntax (null?/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {T} e)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (assert-type #'e+ #'(Listof T))
|
||||
(⊢ (syntax/loc stx (null? e+)) #'Bool)]))
|
||||
(define-syntax (first/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {T} e)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (assert-type #'e+ #'(Listof T))
|
||||
(⊢ (syntax/loc stx (car e+)) #'T)]))
|
||||
(define-syntax (rest/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ {T} e)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (assert-type #'e+ #'(Listof T))
|
||||
(⊢ (syntax/loc stx (cdr e+)) #'(Listof T))]))
|
||||
|
||||
;; define, module-begin -------------------------------------------------------
|
||||
(define-syntax (define/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ (f:id [x:id : τ] ...) : τ_result e ...)
|
||||
#:when (Γ (type-env-extend #'([f (τ ... → τ_result)])))
|
||||
;; If I use the (commented-out) copied-from-λ impl below,
|
||||
;; get "f unbound identifier error" for example:
|
||||
;; (define (g [y : Int]) : Int
|
||||
;; (+ (f y) 1))
|
||||
;; (define (f [x : Int]) : Int
|
||||
;; (+ x 1))
|
||||
;; But if I define define/tc interms of λ/tc, the example works.
|
||||
;; I'm guessing it's because the call to expand/df is deferred
|
||||
;; in the latter case to until after the racket internal def code first
|
||||
;; does its peek-expand to get all the λ/tcs, and thus all the f's have
|
||||
;; been added to the internal def ctxt
|
||||
; #:with (lam xs . es+) (with-extended-type-env #'([x τ] ...)
|
||||
; (expand/df #'(λ (f x ...) e ... e_result)))
|
||||
; #:with (e++ ... e_result++) (with-extended-type-env #'([x τ] ...)
|
||||
; (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
|
||||
; #:when (stx-map assert-Unit-type #'(e++ ...))
|
||||
; #:with τ_body (typeof #'e_result++)
|
||||
; (⊢ (syntax/loc stx (define xs+ e++ ... e_result++)) #'(τ ... → τ_body))]
|
||||
#'(define f (λ/tc ([x : τ] ...) e ...))]
|
||||
[(_ x:id e) #'(define x e)]))
|
||||
|
||||
|
||||
(begin-for-syntax
|
||||
;; EXTENSIBILITY NOTE:
|
||||
;; Originally, define-type was a #:literal instead of a #:datum-literal, but
|
||||
;; this became a problem when sysf extended define-type (but not modul-begin).
|
||||
;; Putting define-type in the #:literals list makes it always expect the stlc
|
||||
;; version of define-type, so it wasnt getting properly parsed in sysf.
|
||||
;;
|
||||
;; Similarly, I had to define the define-type pattern below to avoid explicitly
|
||||
;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
|
||||
;; version of define-type.
|
||||
(define-syntax-class maybe-def #:datum-literals (define variant define-type)
|
||||
(pattern define-fn
|
||||
#:with (define (f x ...) body ...) #'define-fn
|
||||
#:attr fndef #'(define-fn)
|
||||
#:attr e #'() #:attr tydecl #'())
|
||||
(pattern define-variant-type-decl
|
||||
#:with (define-type TypeName (variant (Cons fieldτ ...) ...))
|
||||
#'define-variant-type-decl
|
||||
#:attr tydecl #'(define-variant-type-decl)
|
||||
#:attr fndef #'() #:attr e #'())
|
||||
(pattern define-type-decl
|
||||
#:with (define-type TypeName:id (Cons:id fieldτ ...) ...)
|
||||
#'define-type-decl
|
||||
#:attr tydecl #'(define-type-decl)
|
||||
#:attr fndef #'() #:attr e #'())
|
||||
(pattern exp:expr
|
||||
#:attr tydecl #'() #:attr fndef #'()
|
||||
#:attr e #'(exp)))
|
||||
(define-syntax-class strct #:literals (begin define-values define-syntaxes)
|
||||
(pattern
|
||||
(begin
|
||||
(define-values (x ...) mk-strct-type-def)
|
||||
(define-syntaxes (y) strct-info-def))
|
||||
#:attr def-val #'(define-values (x ...) mk-strct-type-def)
|
||||
#:attr def-syn #'(define-syntaxes (y) strct-info-def)))
|
||||
(define-syntax-class def-val #:literals (define-values)
|
||||
(pattern (define-values (x ...) vals)
|
||||
#:attr lhs #'(x ...)
|
||||
#:attr rhs #'vals))
|
||||
(define-syntax-class def-syn #:literals (define-syntaxes)
|
||||
(pattern (define-syntaxes (x) stxs)
|
||||
#:attr lhs #'x
|
||||
#:attr rhs #'stxs))
|
||||
)
|
||||
|
||||
(define-syntax (module-begin/tc stx)
|
||||
(syntax-parse stx #:literals (begin)
|
||||
[(_ mb-form:maybe-def ...)
|
||||
;; handle define-type
|
||||
#:with (deftype ...) (template ((?@ . mb-form.tydecl) ...))
|
||||
; #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
|
||||
; #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
|
||||
; #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
|
||||
; #:with (def-val:def-val ...) #'(structdef+.def-val ...)
|
||||
; #:with (def-val-lhs ...) #'(def-val.lhs ...)
|
||||
; #:with (def-val-rhs ...) #'(def-val.rhs ...)
|
||||
; #:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
|
||||
; #:with (def-syn-lhs ...) #'(def-syn.lhs ...)
|
||||
; #:with (def-syn-rhs ...) #'(def-syn.rhs ...)
|
||||
;; handle defines
|
||||
#:with (deffn ...) (template ((?@ . mb-form.fndef) ...))
|
||||
; #:with (deffn+:def-val ...) (stx-map expand/df/module-ctx #'(deffn ...))
|
||||
; #:with (f ...) #'(deffn+.lhs ...)
|
||||
; #:with (v ...) #'(deffn+.rhs ...)
|
||||
#:with (e ...) (template ((?@ . mb-form.e) ...))
|
||||
;; base type env
|
||||
; #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
|
||||
;; NOTE: for struct def, define-values *must* come before define-syntaxes
|
||||
;; ow, error, eg: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
|
||||
(quasisyntax/loc stx
|
||||
(#%module-begin
|
||||
#,(expand/df #'(let ()
|
||||
deftype ...
|
||||
;structdef ...
|
||||
deffn ...
|
||||
e ...
|
||||
(void)))
|
||||
; #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
|
||||
; (let-syntax ([def-syn-lhs def-syn-rhs] ...)
|
||||
; (letrec-values ([f v] ...) e ... (void)))))
|
||||
(define #,(datum->syntax stx 'runtime-env)
|
||||
(for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
|
||||
(hash->list (Γ)))])
|
||||
(values (car x:τ) (cdr x:τ))))
|
||||
))]))
|
||||
|
||||
;; type checking testing: -----------------------------------------------------
|
||||
(require rackunit)
|
||||
(require (for-syntax rackunit "typecheck.rkt"))
|
||||
(provide check-equal?)
|
||||
(provide check-type-error check-type check-type-and-result check-not-type)
|
||||
|
||||
(define-syntax (check-type-error stx)
|
||||
(syntax-parse stx
|
||||
[(_ e)
|
||||
#:when (check-exn exn:fail? (λ () (expand/df #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-true (assert-type #'e+ #'τ)
|
||||
(format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-not-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-false (type=? (typeof #'e+) #'τ)
|
||||
(format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-type-and-result stx)
|
||||
(syntax-parse stx #:datum-literals (: =>)
|
||||
[(_ e : τ => v)
|
||||
#'(begin (check-type e : τ)
|
||||
(check-equal? e v))]))
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang s-exp "stlc-via-racket-extended.rkt"
|
||||
((λ ([f : (Int → Int)] [x : Int])
|
||||
(f x))
|
||||
(λ ([x : Int]) (+ x x))
|
||||
10)
|
||||
((λ ([x : Int]) (+ x 1)) 100)
|
||||
((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
|
||||
+
|
||||
100
|
||||
200)
|
||||
|
||||
;; extra tests
|
||||
; test #%datum extension
|
||||
|
||||
; when lang is stlc: should fail with: "dont know type for literal" (but not inf loop)
|
||||
; when lang is stlc+define+cons: should be ok
|
||||
;#f
|
||||
;"dsfa"
|
||||
|
||||
;; lang: stlc: fail
|
||||
;; lang: stlc+define: fail
|
||||
;1.2
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
#lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
|
||||
;(provide #%top-interaction)
|
||||
;(require (prefix-in r: racket/base))
|
||||
;(provide (rename-out [r:#%module-begin #%module-begin]))
|
||||
|
||||
;; Simply-Typed Lambda Calculus
|
||||
;; - implemented with racket-extended language
|
||||
;; - lam, app, var, +, and int literals only
|
||||
|
||||
(declare-base-types → Int)
|
||||
|
||||
;; typed forms ----------------------------------------------------------------
|
||||
|
||||
(define-literal-type-rule integer : Int)
|
||||
|
||||
(define-primop + : (Int Int → Int))
|
||||
#;(define-simple-syntax/type-rule
|
||||
(+ e ...) : Int
|
||||
#:where
|
||||
(e : Int) ...)
|
||||
|
||||
(define-typed-syntax
|
||||
(λ ([x : τ] ...) e) : (τ ... → τ_body)
|
||||
#:where
|
||||
(let τ_body := (typeof e)))
|
||||
|
||||
(define-typed-syntax
|
||||
(#%app f e ...) : τ2
|
||||
#:where
|
||||
(let (τ1 ... → τ2) := (typeof f))
|
||||
(e : τ1) ...)
|
||||
57
old/stlc.rkt
57
old/stlc.rkt
|
|
@ -1,57 +0,0 @@
|
|||
#lang racket/base
|
||||
(require
|
||||
(for-syntax racket/base syntax/parse syntax/parse/experimental/template
|
||||
syntax/stx racket/syntax
|
||||
"stx-utils.rkt")
|
||||
"typecheck.rkt")
|
||||
(provide (rename-out [λ/tc λ] [app/tc #%app] [datum/tc #%datum]))
|
||||
(provide #%module-begin #%top-interaction)
|
||||
|
||||
;; Simply-Typed Lambda Calculus
|
||||
;; - lam, app, var, +, and int literals only
|
||||
;; - implemented in racket
|
||||
|
||||
(define-and-provide-builtin-types → Int)
|
||||
(provide (for-syntax assert-Int-type))
|
||||
(define-for-syntax (assert-Int-type e) (assert-type e #'Int))
|
||||
|
||||
;; typed forms ----------------------------------------------------------------
|
||||
|
||||
;; datum
|
||||
(define-syntax (datum/tc stx)
|
||||
(syntax-parse stx
|
||||
[(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
|
||||
[(_ . x)
|
||||
#:when (type-error #:src #'x #:msg "Literal ~a has unknown type." #'x)
|
||||
(syntax/loc stx (#%datum . x))]))
|
||||
|
||||
;; op
|
||||
(define-primop + : (Int Int → Int))
|
||||
|
||||
;; lambda
|
||||
(define-syntax (λ/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ ([x:id : τ] ...) e)
|
||||
;; the with-extended-type-env must be outside the expand/df (instead of
|
||||
;; around just the body) bc ow the parameter will get restored to the old
|
||||
;; value before the local-expand happens
|
||||
#:with (lam xs+ e+) (with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e)))
|
||||
;; manually handle identifiers here
|
||||
;; - since Racket has no #%var hook, ids didn't get "expanded" in the previous line
|
||||
;; and thus didn't get a type
|
||||
;; TODO: can I put this somewhere else where it's more elegant?
|
||||
#:with e++ (if (identifier? #'e+)
|
||||
(with-extended-type-env #'([x τ] ...) (expand/df #'e+))
|
||||
#'e+)
|
||||
#:with τ_body (typeof #'e++)
|
||||
(⊢ (syntax/loc stx (lam xs+ e++)) #'(τ ... → τ_body))]))
|
||||
|
||||
;; #%app
|
||||
(define-syntax (app/tc stx)
|
||||
(syntax-parse stx #:literals (→)
|
||||
[(_ e_fn e_arg ...)
|
||||
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
|
||||
#:with (τ ... → τ_res) (typeof #'e_fn+)
|
||||
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
|
||||
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang racket/base
|
||||
(require syntax/stx racket/list)
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (stx-cadr stx) (car (stx-cdr stx)))
|
||||
|
||||
(define (stx-andmap f . stx-lsts)
|
||||
(apply andmap f (map syntax->list stx-lsts)))
|
||||
|
||||
(define (stx-flatten stxs)
|
||||
(apply append (stx-map syntax->list stxs)))
|
||||
|
||||
(define (curly-parens? stx)
|
||||
(define paren-prop (syntax-property stx 'paren-shape))
|
||||
(and paren-prop (char=? #\{ paren-prop)))
|
||||
|
||||
(define (stx-member v stx)
|
||||
(member v (syntax->list stx) free-identifier=?))
|
||||
|
||||
(define (stx-length stx) (length (syntax->list stx)))
|
||||
|
||||
(define (stx-last stx) (last (syntax->list stx)))
|
||||
|
|
@ -1,197 +0,0 @@
|
|||
#lang s-exp "sysf.rkt"
|
||||
|
||||
;; polymorphic tests
|
||||
(define-type (Maybe X) (variant (None) (Just X)))
|
||||
(check-type (None {Int}) : (Maybe Int))
|
||||
(check-type (Just {Int} 1) : (Maybe Int))
|
||||
(check-type-error (Just {Int} #f))
|
||||
(check-not-type (Just {Int} 1) : (Maybe Bool))
|
||||
(check-type (λ {X} ([x : X]) x) : (∀ (X) (X → X)))
|
||||
(check-type-error ((λ ([x : X]) x) 1))
|
||||
|
||||
;; lists
|
||||
(define-type (MyList X) (variant (Null) (Cons X (MyList X))))
|
||||
(check-type (Null {Int}) : (MyList Int))
|
||||
(check-type (Cons {Int} 1 (Null {Int})) : (MyList Int))
|
||||
(define (map/List {A B} [f : (A → B)] [lst : (MyList A)]) : (MyList B)
|
||||
(cases {A} lst
|
||||
[Null () (Null {B})]
|
||||
[Cons (x xs) (Cons {B} (f {A B} x) (map/List {A B} f xs))]))
|
||||
(define (add1 [x : Int]) : Int (+ x 1))
|
||||
(check-type-and-result
|
||||
(map/List {Int Int} add1 (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
|
||||
: (MyList Int) => (Cons {Int} 2 (Cons {Int} 3 (Null {Int}))))
|
||||
(check-type-and-result
|
||||
(map/List {Int Bool} (λ ([x : Int]) #f) (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
|
||||
: (MyList Bool) => (Cons {Bool} #f (Cons {Bool} #f (Null {Bool}))))
|
||||
;; fails without inst (2014-08-18)
|
||||
;; - Typed Racket also requires inst
|
||||
;; - OCaml does not require inst
|
||||
(check-type-and-result
|
||||
(map/List {Int Bool} (inst (λ {X} {[x : X]} #f) Int) (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
|
||||
: (MyList Bool) => (Cons {Bool} #f (Cons {Bool} #f (Null {Bool}))))
|
||||
|
||||
(check-type-and-result (list {Int} 1 2 3)
|
||||
: (Listof Int) => (cons {Int} 1 (cons {Int} 2 (cons {Int} 3 (null {Int})))))
|
||||
(check-type-error (list {Int} 1 2 #f))
|
||||
(check-type-error (list {Bool} 1 2 3))
|
||||
;; map
|
||||
(define (map {A B} [f : (A → B)] [lst : (Listof A)]) : (Listof B)
|
||||
(if (null? {A} lst)
|
||||
(null {B})
|
||||
(cons {B} (f {A B} (first {A} lst)) (map {A B} f (rest {A} lst)))))
|
||||
(check-type-and-result (map {Int Int} add1 (list {Int} 1 2 3))
|
||||
: (Listof Int) => (list {Int} 2 3 4))
|
||||
(check-type-error (map {Int Bool} add1 (list {Int} 1 2 3)))
|
||||
(check-type-error (map {Bool Int} add1 (list {Int} 1 2 3)))
|
||||
(check-type-error (map {Int Int} add1 (list {Bool} 1 2 3)))
|
||||
|
||||
;; Queen type
|
||||
(define-type Queen (Q Int Int))
|
||||
|
||||
;; filter
|
||||
(define (filter {A} [p? : (A → Bool)] [lst : (Listof A)]) : (Listof A)
|
||||
(if (null? {A} lst)
|
||||
(null {A})
|
||||
(let ([x (first {A} lst)])
|
||||
(if (p? x)
|
||||
(cons {A} x (filter {A} p? (rest {A} lst)))
|
||||
(filter {A} p? (rest {A} lst))))))
|
||||
|
||||
(check-type-and-result
|
||||
(filter {Int} (λ ([n : Int]) (if (= n 5) #f #t)) (list {Int} 1 2 3 4 5 5 6 7))
|
||||
: (Listof Int) => (list {Int} 1 2 3 4 6 7))
|
||||
|
||||
;; foldr
|
||||
(define (foldr {A B} [f : (A B → B)] [base : B] [lst : (Listof A)]) : B
|
||||
(if (null? {A} lst)
|
||||
base
|
||||
(f (first {A} lst) (foldr {A B} f base (rest {A} lst)))))
|
||||
|
||||
(check-type-and-result (foldr {Int Int} + 0 (build-list {Int} add1 4)) : Int => 10)
|
||||
|
||||
;; foldl
|
||||
(define (foldl {A B} [f : (A B → B)] [acc : B] [lst : (Listof A)]) : B
|
||||
(if (null? {A} lst)
|
||||
acc
|
||||
(foldl {A B} f (f (first {A} lst) acc) (rest {A} lst))))
|
||||
|
||||
(check-type-and-result (foldl {Int Int} + 0 (build-list {Int} add1 4)) : Int => 10)
|
||||
|
||||
;; tails
|
||||
(define (tails {A} [lst : (Listof A)]) : (Listof (Listof A))
|
||||
(if (null? {A} lst)
|
||||
(list {(Listof A)} (null {A}))
|
||||
(cons {(Listof A)} lst (tails {A} (rest {A} lst)))))
|
||||
(check-type-and-result (tails {Int} (list {Int} 1 2 3))
|
||||
: (Listof (Listof Int))
|
||||
=> (list {(Listof Int)} (list {Int} 1 2 3) (list {Int} 2 3) (list {Int} 3) (null {Int})))
|
||||
(check-type-error (tails {Bool} (list {Int} 1 2 3)))
|
||||
(check-type-error (tails {Int} (list {Bool} 1 2 3)))
|
||||
(check-not-type (tails {Int} (list {Int} 1 2 3)) : (Listof Int))
|
||||
|
||||
(define (andmap {A} [f : (A → Bool)] [lst : (Listof A)]) : Bool
|
||||
(if (null? {A} lst)
|
||||
#t
|
||||
(and (f (first {A} lst)) (andmap {A} f (rest {A} lst)))))
|
||||
|
||||
(define (safe? [q1 : Queen] [q2 : Queen]) : Bool
|
||||
(cases q1
|
||||
[Q (x1 y1)
|
||||
(cases q2
|
||||
[Q (x2 y2) (not (or (or (= x1 x2) (= y1 y2))
|
||||
(= (abs (- x1 x2)) (abs (- y1 y2)))))])]))
|
||||
(check-type-and-result (safe? (Q 1 1) (Q 1 2)) : Bool => #f)
|
||||
(check-type-and-result (safe? (Q 1 1) (Q 2 1)) : Bool => #f)
|
||||
(check-type-and-result (safe? (Q 1 1) (Q 2 2)) : Bool => #f)
|
||||
(check-type-and-result (safe? (Q 1 1) (Q 2 3)) : Bool => #t)
|
||||
|
||||
(define (safe/list? [lst : (Listof Queen)]) : Bool
|
||||
(if (null? {Queen} lst)
|
||||
#t
|
||||
(let ([q1 (first {Queen} lst)])
|
||||
(andmap {Queen} (λ ([q2 : Queen]) (safe? q1 q2)) (rest {Queen} lst)))))
|
||||
|
||||
(check-type safe/list? : ((Listof Queen) → Bool))
|
||||
|
||||
(define (valid? [lst : (Listof Queen)]) : Bool
|
||||
(andmap {(Listof Queen)} safe/list? (tails {Queen} lst)))
|
||||
|
||||
(define (build-list-help {A} [f : (Int → A)] [n : Int] [m : Int]) : (Listof A)
|
||||
(if (= n m)
|
||||
(null {A})
|
||||
(cons {A} (f {A} n) (build-list-help {A} f (add1 n) m))))
|
||||
(define (build-list {A} [f : (Int → A)] [n : Int]) : (Listof A)
|
||||
(build-list-help {A} f 0 n))
|
||||
|
||||
(check-type-and-result (build-list {Int} add1 8)
|
||||
: (Listof Int) => (list {Int} 1 2 3 4 5 6 7 8))
|
||||
|
||||
(define (append {A} [lst1 : (Listof A)] [lst2 : (Listof A)]) : (Listof A)
|
||||
(if (null? {A} lst1)
|
||||
lst2
|
||||
(cons {A} (first {A} lst1) (append {A} (rest {A} lst1) lst2))))
|
||||
|
||||
(define (nqueens [n : Int]) : (Listof (Listof Queen))
|
||||
(let ([process-row
|
||||
(λ ([row : Int] [all-possible-so-far : (Listof (Listof Queen))])
|
||||
(foldr {(Listof Queen) (Listof (Listof Queen))}
|
||||
(λ ([qs : (Listof Queen)] [new-qss : (Listof (Listof Queen))])
|
||||
(append
|
||||
{(Listof Queen)}
|
||||
(map
|
||||
{Int (Listof Queen)}
|
||||
(λ ([col : Int]) (cons {Queen} (Q row col) qs))
|
||||
(build-list {Int} add1 n))
|
||||
new-qss))
|
||||
(null {(Listof Queen)})
|
||||
all-possible-so-far))])
|
||||
(let ([all-possible
|
||||
(foldl
|
||||
{Int (Listof (Listof Queen))}
|
||||
process-row
|
||||
(list {(Listof Queen)} (null {Queen}))
|
||||
(build-list {Int} add1 n))])
|
||||
(let ([solns (filter {(Listof Queen)} valid? all-possible)])
|
||||
(if (null? {(Listof Queen)} solns)
|
||||
(null {Queen})
|
||||
(first {(Listof Queen)} solns))))))
|
||||
|
||||
(check-type-and-result (nqueens 4)
|
||||
: (Listof (Listof Queen))
|
||||
=> (list {Queen} (Q 4 3) (Q 3 1) (Q 2 4) (Q 1 2)))
|
||||
|
||||
;; testing for variable capture
|
||||
(define (polyf {X} [x : X]) : X x)
|
||||
(check-type polyf : (∀ (X) (X → X)))
|
||||
(define (polyf2 {X} [x : X]) : (∀ (X) (X → X)) polyf)
|
||||
(check-type polyf2 : (∀ (X) (X → (∀ (X) (X → X)))))
|
||||
|
||||
;; the following test fails bc X gets captured (2014-08-18)
|
||||
;; - 2014-08-20: fixed
|
||||
;; - 2014-08-20: backed out fix, so renamer is equiv to redex's "subst-vars"
|
||||
;; Capture is actually ok because the binder gets renamed as well.
|
||||
;; Since types are names anyways, it's ok.
|
||||
;; Eg, the following example has type (→ Int (∀ (Int) (→ Int Int))), which is ok
|
||||
; - 2014-08-20: changed my mind again,
|
||||
;; capture is not ok when forall is applied to non-base types, ie →
|
||||
;; (see test below)
|
||||
;; - 2014-08-20: fixed by implementing manual subst
|
||||
(check-type (inst polyf2 Int) : (Int → (∀ (X) (X → X))))
|
||||
;; the following test "fails" bc forall is nested
|
||||
;; - Typed Racket has same behavior, so ok
|
||||
(check-type-error (inst (inst polyf2 Int) Bool))
|
||||
(check-type-error ((inst polyf2 Int) #f))
|
||||
;; again, the following example has type (∀ (Int) (→ Int Int)), which is ok
|
||||
;; - 2014-08-20: fixed by impl manual subst
|
||||
(check-type ((inst polyf2 Int) 1) : (∀ (X) (X → X)))
|
||||
(check-type (inst ((inst polyf2 Int) 1) Bool) : (Bool → Bool))
|
||||
;; test same example with type-instantiating apply instead of inst
|
||||
(check-type (polyf2 {Int} 1) : (∀ (Y) (Y → Y)))
|
||||
(check-type-error (polyf2 {Int} #f))
|
||||
(check-type-and-result ((polyf2 {Int} 1) {Bool} #f) : Bool => #f)
|
||||
(check-type-error ((polyf2 {Int} 1) {Bool} 2))
|
||||
|
||||
(check-type (inst polyf (Int → Int)) : ((Int → Int) → (Int → Int)))
|
||||
;; the follow test fails because the binder is renamed to (→ Int Int)
|
||||
(check-type (inst polyf2 (Int → Int)) : ((Int → Int) → (∀ (X) (X → X))))
|
||||
199
old/sysf.rkt
199
old/sysf.rkt
|
|
@ -1,199 +0,0 @@
|
|||
#lang racket/base
|
||||
(require
|
||||
racket/match
|
||||
(for-syntax
|
||||
racket/base syntax/parse syntax/parse/experimental/template
|
||||
syntax/stx racket/syntax racket/set
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse)
|
||||
"typecheck.rkt")
|
||||
(require
|
||||
(except-in
|
||||
"stlc.rkt"
|
||||
define-type cases begin #%app λ define
|
||||
check-type-error check-type check-type-and-result check-not-type check-equal?))
|
||||
(require
|
||||
(prefix-in stlc:
|
||||
(only-in
|
||||
"stlc.rkt"
|
||||
define-type cases begin #%app λ define)))
|
||||
(provide (all-from-out "stlc.rkt"))
|
||||
(provide
|
||||
define-type cases inst
|
||||
(rename-out
|
||||
[stlc:begin begin]
|
||||
[app/tc #%app]
|
||||
[λ/tc λ] [define/tc define]))
|
||||
|
||||
(define-and-provide-builtin-types ∀)
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class ∀τ #:literals (∀)
|
||||
(pattern (∀ tvs:tyvars/no-brace τbody)))
|
||||
;; a list of types, for type instantiation
|
||||
(define-syntax-class inst-τs
|
||||
(pattern τs
|
||||
#:when (curly-parens? #'τs)
|
||||
#:fail-unless (stx-pair? #'τs) "Must provide a list of types"
|
||||
#:with (τ ...) #'τs))
|
||||
(define-syntax-class tyvars
|
||||
(pattern tvs
|
||||
#:when (curly-parens? #'tvs)
|
||||
#:fail-unless (stx-pair? #'tvs) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'tvs))
|
||||
"Given duplicate binders in type variable list."))
|
||||
(define-syntax-class tyvars/no-brace
|
||||
(pattern tvs
|
||||
#:fail-unless (stx-pair? #'tvs) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'tvs))
|
||||
"Given duplicate binders in type variable list.")))
|
||||
|
||||
|
||||
;; define-type ----------------------------------------------------------------
|
||||
(define-syntax (define-type stx)
|
||||
(syntax-parse stx #:datum-literals (variant)
|
||||
[(_ (Tycon:id X:id ...) (variant (Cons:id τ_fld ...) ...))
|
||||
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
|
||||
#:when (Γ (type-env-extend #'([Cons (∀ (X ...) (τ_fld ... → (Tycon X ...)))] ...)))
|
||||
#'(begin ; should be racket begin
|
||||
(struct Cons (x ...) #:transparent) ...)]
|
||||
[(_ any ...) #'(stlc:define-type any ...)]))
|
||||
|
||||
(define-syntax (inst stx)
|
||||
(syntax-parse stx #:literals (∀)
|
||||
[(_ e τ ...)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:with τ_e:∀τ (typeof #'e+)
|
||||
(⊢ #'e+ (apply-forall #'τ_e #'(τ ...)))]
|
||||
[(_ e τ ...) ; error if not ∀ type
|
||||
#:with τ_e (typeof (expand/df #'e))
|
||||
#:when
|
||||
(type-error
|
||||
#:src #'e
|
||||
#:msg "Could not instantiate expression ~a with non-polymorphic type ~a"
|
||||
#'e #'τ_e)
|
||||
#f]))
|
||||
|
||||
;; cases ----------------------------------------------------------------------
|
||||
(define-syntax (cases stx)
|
||||
(syntax-parse stx #:literals (∀ →)
|
||||
[(_ τs:inst-τs e [Cons (x ...) body ... body_result] ...)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
|
||||
#:with (τ_Cons:∀τ ...) (stx-map typeof #'(Cons+ ...))
|
||||
#:with ((τ ... → τ_res) ...)
|
||||
(stx-map (λ (∀τ) (apply-forall ∀τ #'τs)) #'(τ_Cons ...))
|
||||
;; check constructor type in every branch matches expr being matched
|
||||
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_res ...))
|
||||
#:with ((lam (x+ ...) body+ ... body_result+) ...)
|
||||
(stx-map (λ (bods xs τs)
|
||||
(with-extended-type-env
|
||||
(stx-map list xs τs)
|
||||
(expand/df #`(λ #,xs #,@bods))))
|
||||
#'((body ... body_result) ...)
|
||||
#'((x ...) ...)
|
||||
#'((τ ...) ...))
|
||||
#:when (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((body+ ...) ...))
|
||||
#:with (τ_result ...) (stx-map typeof #'(body_result+ ...))
|
||||
#:when (or (null? (syntax->list #'(τ_result ...)))
|
||||
(andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
|
||||
(cdr (syntax->list #'(τ_result ...)))))
|
||||
(⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
|
||||
(car (syntax->list #'(τ_result ...))))]
|
||||
[(_ any ...) #:when (displayln "stlc:cases") #'(stlc:cases any ...)]))
|
||||
|
||||
;; lambda ---------------------------------------------------------------------
|
||||
(define-syntax (λ/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
;; most of the code from this case, except for the curly? check,
|
||||
;; is copied from stlc:λ
|
||||
[(_ tvs:tyvars ([x:id : τ] ...) e ... e_result)
|
||||
;; the with-extended-type-env must be outside the expand/df (instead of
|
||||
;; around just the body) bc ow the parameter will get restored to the old
|
||||
;; value before the local-expand happens
|
||||
#:with (lam xs e+ ... e_result+) (with-extended-type-env #'([x τ] ...)
|
||||
(expand/df #'(λ (x ...) e ... e_result)))
|
||||
;; manually handle identifiers here
|
||||
;; - since Racket has no #%var hook, ids didn't get "expanded" in the previous line
|
||||
;; and thus didn't get a type
|
||||
;; TODO: can I put this somewhere else where it's more elegant?
|
||||
#:with (e++ ... e_result++) (with-extended-type-env #'([x τ] ...)
|
||||
(stx-map
|
||||
(λ (e) (if (identifier? e) (expand/df e) e))
|
||||
#'(e+ ... e_result+)))
|
||||
;; manually typecheck the implicit begin
|
||||
#:when (stx-map assert-Unit-type #'(e++ ...))
|
||||
#:with τ_body (typeof #'e_result++)
|
||||
(⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (τ ... → τ_body)))]
|
||||
[(_ any ...) #'(stlc:λ any ...)]))
|
||||
|
||||
; define ----------------------------------------------------------------------
|
||||
(define-syntax (define/tc stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
;; most of the code from this case, except for the curly? check,
|
||||
;; is copied from stlc:define
|
||||
[(_ (f:id tvs:tyvars [x:id : τ] ...) : τ_result e ...)
|
||||
#:when (Γ (type-env-extend #'([f (∀ tvs (τ ... → τ_result))])))
|
||||
#'(define f (λ/tc tvs ([x : τ] ...) e ...))]
|
||||
[(_ any ...) #'(stlc:define any ...)]))
|
||||
|
||||
; #%app -----------------------------------------------------------------------
|
||||
(define-syntax (app/tc stx)
|
||||
(syntax-parse stx #:literals (→ void ∀)
|
||||
; this case only triggered by testing forms, eg check-type
|
||||
; more specifically, types should never get expanded, except when testing
|
||||
; [(_ → arg ...) #'(→ arg ...)]
|
||||
[(_ e_fn τs:inst-τs e_arg ...)
|
||||
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
|
||||
#:with τ_fn:∀τ (typeof #'e_fn+)
|
||||
#:with (τ_arg ... → τ_res) (apply-forall #'τ_fn #'τs)
|
||||
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
|
||||
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
|
||||
;; handle type apply of non-poly fn here; just pass through
|
||||
[(_ e_fn τs:inst-τs e_arg ...)
|
||||
#'(stlc:#%app e_fn e_arg ...)]
|
||||
;; error when e_fn has ∀ type but in instantiation vars
|
||||
[(_ e_fn e_arg ...)
|
||||
#:with e_fn+ (expand/df #'e_fn)
|
||||
#:with τ_fn:∀τ (typeof #'e_fn+)
|
||||
#:when (type-error #:src #'stx
|
||||
#:msg "Missing type instantiation(s) in application: ~a"
|
||||
#'(e_fn e_arg ...))
|
||||
#'#f]
|
||||
[(_ any ...) #'(stlc:#%app any ...)]))
|
||||
|
||||
;; testing fns ----------------------------------------------------------------
|
||||
;; for now, these are duplicated from stlc.rkt: 2014-08-14
|
||||
;; type checking testing: -----------------------------------------------------
|
||||
(require rackunit)
|
||||
(require (for-syntax rackunit "typecheck.rkt"))
|
||||
(provide check-equal?)
|
||||
(provide check-type-error check-type check-type-and-result check-not-type)
|
||||
|
||||
(define-syntax (check-type-error stx)
|
||||
(syntax-parse stx
|
||||
[(_ e)
|
||||
#:when (check-exn exn:fail? (λ () (expand/df #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-true (assert-type #'e+ #'τ)
|
||||
(format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-not-type stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-false (type=? (typeof #'e+) #'τ)
|
||||
(format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
(define-syntax (check-type-and-result stx)
|
||||
(syntax-parse stx #:datum-literals (: =>)
|
||||
[(_ e : τ => v)
|
||||
#'(begin (check-type e : τ)
|
||||
(check-equal? e v))]))
|
||||
|
|
@ -1,250 +0,0 @@
|
|||
#lang racket/base
|
||||
(require (for-syntax racket/base syntax/parse syntax/stx racket/syntax
|
||||
racket/set racket/list racket/function
|
||||
"stx-utils.rkt")
|
||||
(for-meta 2 racket/base syntax/parse))
|
||||
(provide (all-defined-out)
|
||||
(for-syntax (all-defined-out)))
|
||||
|
||||
(begin-for-syntax
|
||||
;; usage:
|
||||
;; type-error #:src src-stx
|
||||
;; #:msg msg-string msg-args ...
|
||||
;; msg-args should be syntax
|
||||
(define-syntax-rule (type-error #:src stx-src #:msg msg args ...)
|
||||
(raise-user-error
|
||||
'TYPE-ERROR
|
||||
(format (string-append "~a (~a:~a): " msg)
|
||||
(syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
|
||||
(syntax->datum args) ...))))
|
||||
|
||||
;; for types, just need the identifier bound
|
||||
(define-syntax-rule (define-and-provide-builtin-type τ)
|
||||
(begin (define τ #f) (provide τ)))
|
||||
(define-syntax-rule (define-and-provide-builtin-types τ ...)
|
||||
(begin (define-and-provide-builtin-type τ) ...))
|
||||
|
||||
(define-syntax (define-primop stx)
|
||||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ op:id : ((~and τ_arg (~not (~literal ...))) ... (~optional (~and ldots (~literal ...)))
|
||||
(~and arr (~datum →))
|
||||
τ_result))
|
||||
; #:with lit-→ (datum->syntax stx '→)
|
||||
#:with (~datum →) #'arr
|
||||
#:with op/tc (format-id #'op "~a/tc" #'op)
|
||||
#`(begin
|
||||
(provide (rename-out [op/tc op]))
|
||||
(define-syntax (op/tc stx)
|
||||
(syntax-parse stx
|
||||
[f:id ; HO case
|
||||
(⊢ (syntax/loc stx op)
|
||||
#,(if (attribute ldots)
|
||||
#'#'(τ_arg ... (... (... ...)) arr τ_result)
|
||||
#'#'(τ_arg ... arr τ_result)))]
|
||||
;; TODO: for now, just drop the ...
|
||||
; #'(τ_arg ... arr τ_result))]
|
||||
[(_ e (... ...))
|
||||
#:with es+ (stx-map expand/df #'(e (... ...)))
|
||||
#:with τs #'(τ_arg ...)
|
||||
#:fail-unless (let ([es-len (stx-length #'es+)]
|
||||
[τs-len (stx-length #'τs)])
|
||||
(or (and #,(if (attribute ldots) #t #f)
|
||||
(>= (- es-len (sub1 τs-len)) 0))
|
||||
(= es-len τs-len)))
|
||||
#,(if (attribute ldots)
|
||||
#'(format "Wrong number of arguments, given ~a, expected at least ~a"
|
||||
(stx-length #'es+) (sub1 (stx-length #'τs)))
|
||||
#'(format "Wrong number of arguments, given ~a, expected ~a"
|
||||
(stx-length #'es+) (stx-length #'τs)))
|
||||
#:with τs-ext #,(if (attribute ldots)
|
||||
#'(let* ([diff (- (stx-length #'es+) (sub1 (stx-length #'τs)))]
|
||||
[last-τ (stx-last #'τs)]
|
||||
[last-τs (build-list diff (λ _ last-τ))])
|
||||
(append (drop-right (syntax->list #'τs) 1) last-τs))
|
||||
#'#'τs)
|
||||
#:when (stx-andmap assert-type #'es+ #'τs-ext)
|
||||
(⊢ (syntax/loc stx (op . es+)) #'τ_result)])))]))
|
||||
|
||||
;; general type-checking functions
|
||||
|
||||
(define-for-syntax (type=? τ1 τ2)
|
||||
; (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
|
||||
(syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀ →)
|
||||
[(x:id y:id) (free-identifier=? τ1 τ2)]
|
||||
[(∀τ1 ∀τ2)
|
||||
#:with (∀ τvars1 τ_body1) #'∀τ1
|
||||
#:fail-unless (stx-pair? #'τvars1) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'τvars1)) "Given duplicate identifiers"
|
||||
#:with (∀ τvars2 τ_body2) #'∀τ2
|
||||
#:fail-unless (stx-pair? #'τvars2) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'τvars2)) "Given duplicate identifiers"
|
||||
#:with fresh-τvars (generate-temporaries #'τvars1)
|
||||
;; to handle α-equiv, for apply-forall with same vars
|
||||
(and (= (length (syntax->list #'τvars1))
|
||||
(length (syntax->list #'τvars2)))
|
||||
(type=? (apply-forall #'∀τ1 #'fresh-τvars) (apply-forall #'∀τ2 #'fresh-τvars)))]
|
||||
;; ldots on lhs
|
||||
[(((~and τ_arg1 (~not (~literal ...))) ... τ_repeat (~and ldots (~literal ...)) → τ_result1)
|
||||
((~and τ_arg2 (~not (~literal ...))) ... → τ_result2))
|
||||
(let ([num-arg1 (stx-length #'(τ_arg1 ...))]
|
||||
[num-arg2 (stx-length #'(τ_arg2 ...))])
|
||||
(define diff (- num-arg2 num-arg1))
|
||||
(define extra-τs (build-list diff (λ _ #'τ_repeat)))
|
||||
(with-syntax ([(τ_arg1/ext ...) (append (syntax->list #'(τ_arg1 ...)) extra-τs)])
|
||||
(and (= (length (syntax->list #'(τ_arg1/ext ...))) (length (syntax->list #'(τ_arg2 ...))))
|
||||
(stx-andmap type=? #'(τ_arg1/ext ...) #'(τ_arg2 ...))
|
||||
(type=? #'τ_result1 #'τ_result2))))]
|
||||
;; ldots on rhs
|
||||
[(((~and τ_arg2 (~not (~literal ...))) ... → τ_result2)
|
||||
((~and τ_arg1 (~not (~literal ...))) ... τ_repeat (~and ldots (~literal ...)) → τ_result1))
|
||||
(let ([num-arg1 (stx-length #'(τ_arg1 ...))]
|
||||
[num-arg2 (stx-length #'(τ_arg2 ...))])
|
||||
(define diff (- num-arg2 num-arg1))
|
||||
(define extra-τs (build-list diff (λ _ #'τ_repeat)))
|
||||
(with-syntax ([(τ_arg1/ext ...) (append (syntax->list #'(τ_arg1 ...)) extra-τs)])
|
||||
(and (= (length (syntax->list #'(τ_arg1/ext ...))) (length (syntax->list #'(τ_arg2 ...))))
|
||||
(stx-andmap type=? #'(τ_arg1/ext ...) #'(τ_arg2 ...))
|
||||
(type=? #'τ_result1 #'τ_result2))))]
|
||||
;; ldots on both lhs and rhs
|
||||
[(((~and τ_arg1 (~not (~literal ...))) ... τ_repeat1 (~and ldots1 (~literal ...)) → τ_result1)
|
||||
((~and τ_arg2 (~not (~literal ...))) ... τ_repeat2 (~and ldots2 (~literal ...)) → τ_result2))
|
||||
(let ([num-arg1 (stx-length #'(τ_arg1 ...))]
|
||||
[num-arg2 (stx-length #'(τ_arg2 ...))])
|
||||
(cond [(> num-arg2 num-arg1)
|
||||
(define diff (- num-arg2 num-arg1))
|
||||
(define extra-τs (build-list diff (λ _ #'τ_repeat1)))
|
||||
(with-syntax ([(τ_arg1/ext ...) (append (syntax->list #'(τ_arg1 ...)) extra-τs)])
|
||||
(and (= (length (syntax->list #'(τ_arg1/ext ...))) (length (syntax->list #'(τ_arg2 ...))))
|
||||
(stx-andmap type=? #'(τ_arg1/ext ...) #'(τ_arg2 ...))
|
||||
(type=? #'τ_result1 #'τ_result2)))]
|
||||
[else
|
||||
(define diff (- num-arg1 num-arg2))
|
||||
(define extra-τs (build-list diff (λ _ #'τ_repeat2)))
|
||||
(with-syntax ([(τ_arg2/ext ...) (append (syntax->list #'(τ_arg2 ...)) extra-τs)])
|
||||
(and (= (length (syntax->list #'(τ_arg2/ext ...))) (length (syntax->list #'(τ_arg1 ...))))
|
||||
(stx-andmap type=? #'(τ_arg2/ext ...) #'(τ_arg1 ...))
|
||||
(type=? #'τ_result1 #'τ_result2)))]))]
|
||||
[((τ_arg1 ... → τ_result1) (τ_arg2 ... → τ_result2))
|
||||
(and (= (length (syntax->list #'(τ_arg1 ...))) (length (syntax->list #'(τ_arg2 ...))))
|
||||
(stx-andmap type=? #'(τ_arg1 ...) #'(τ_arg2 ...))
|
||||
(type=? #'τ_result1 #'τ_result2))]
|
||||
[((tycon1:id τ1 ...) (tycon2:id τ2 ...))
|
||||
(and (free-identifier=? #'tycon1 #'tycon2)
|
||||
(= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
|
||||
(stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
|
||||
[_ #f]))
|
||||
|
||||
;; return #t if (typeof e)=τ, else type error
|
||||
(define-for-syntax (assert-type e τ)
|
||||
; (printf "~a has type " (syntax->datum e))
|
||||
; (printf "~a; expected: " (syntax->datum (typeof e)))
|
||||
; (printf "~a\n" (syntax->datum τ))
|
||||
(or (type=? (typeof e) τ)
|
||||
(type-error #:src e
|
||||
#:msg "~a has type ~a, but should have type ~a" e (typeof e) τ)))
|
||||
|
||||
;; attaches type τ to e (as syntax property)
|
||||
(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
|
||||
|
||||
;; retrieves type of τ (from syntax property)
|
||||
(define-for-syntax (typeof stx) (syntax-property stx 'type))
|
||||
(define-for-syntax has-type? typeof)
|
||||
|
||||
;; type environment -----------------------------------------------------------
|
||||
(begin-for-syntax
|
||||
(define base-type-env (hash))
|
||||
;; Γ : [Hashof var-symbol => type-stx]
|
||||
;; - can't use free-identifier=? for the hash table (or free-id-table)
|
||||
;; because env must be set before expanding λ body (ie before going under λ)
|
||||
;; so x's in the body won't be free-id=? to the one in the table
|
||||
;; use symbols instead of identifiers for now --- should be fine because
|
||||
;; I'm manually managing the environment, and surface language has no macros
|
||||
;; so I know all the binding forms
|
||||
(define Γ (make-parameter base-type-env))
|
||||
|
||||
(define (type-env-lookup x)
|
||||
(hash-ref (Γ) (syntax->datum x)
|
||||
(λ ()
|
||||
(type-error #:src x
|
||||
#:msg "Could not find type for variable ~a" x))))
|
||||
|
||||
;; returns a new hash table extended with type associations x:τs
|
||||
(define (type-env-extend x:τs)
|
||||
(define xs (stx-map stx-car x:τs))
|
||||
(define τs (stx-map stx-cadr x:τs))
|
||||
(apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
|
||||
|
||||
;; must be macro because type env must be extended first, before expandinb body
|
||||
(define-syntax (with-extended-type-env stx)
|
||||
(syntax-parse stx
|
||||
[(_ x-τs e)
|
||||
#'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
|
||||
|
||||
;; apply-forall ---------------------------------------------------------------
|
||||
(define-for-syntax (subst x τ mainτ)
|
||||
(syntax-parse mainτ #:datum-literals (∀ →)
|
||||
[y:id
|
||||
#:when (free-identifier=? #'y x)
|
||||
τ]
|
||||
[y:id #'y]
|
||||
[∀τ
|
||||
#:with (∀ tyvars τbody) #'∀τ
|
||||
#:when (stx-member x #'tyvars)
|
||||
#'∀τ]
|
||||
[∀τ
|
||||
#:with (∀ tyvars τbody) #'∀τ
|
||||
#:when (not (stx-member x #'tyvars))
|
||||
#`(∀ tyvars #,(subst x τ #'τbody))]
|
||||
;; need the ~and because for the result, I need to use the → literal
|
||||
;; from the context of the input, and not the context here
|
||||
[(τ_arg ... (~and (~datum →) arrow) τ_result)
|
||||
#:with (τ_arg/subst ... τ_result/subst)
|
||||
(stx-map (curry subst x τ) #'(τ_arg ... τ_result))
|
||||
#'(τ_arg/subst ... arrow τ_result/subst)]
|
||||
[(tycon:id τarg ...)
|
||||
#:with (τarg/subst ...) (stx-map (curry subst x τ) #'(τarg ...))
|
||||
#'(tycon τarg/subst ...)]))
|
||||
(define-for-syntax (apply-forall ∀τ τs)
|
||||
(syntax-parse ∀τ #:datum-literals (∀)
|
||||
[(∀ (X ...) body)
|
||||
(foldl subst #'body (syntax->list #'(X ...)) (syntax->list τs))]))
|
||||
#;(define-for-syntax (apply-forall ∀τ τs)
|
||||
; (printf "applying ∀:~a to ~a\n" (syntax->datum ∀τ) (syntax->datum τs))
|
||||
(define ctx (syntax-local-make-definition-context))
|
||||
(define id (generate-temporary))
|
||||
(syntax-local-bind-syntaxes
|
||||
(list id)
|
||||
(syntax-parse ∀τ #:datum-literals (∀/internal)
|
||||
[(∀/internal (X ...) τbody)
|
||||
#'(λ (stx)
|
||||
(syntax-parse stx
|
||||
[(_ (τ (... ...)))
|
||||
#:with (X ...) #'(τ (... ...))
|
||||
#'τbody]))])
|
||||
ctx)
|
||||
(local-expand #`(#,id #,τs) 'expression (list #'#%app) ctx))
|
||||
|
||||
;; expand/df ------------------------------------------------------------------
|
||||
;; depth-first expand
|
||||
(define-for-syntax (expand/df e [ctx #f])
|
||||
; (printf "expanding: ~a\n" (syntax->datum e))
|
||||
; (printf "typeenv: ~a\n" (Γ))
|
||||
(cond
|
||||
;; 1st case handles struct constructors that are not the same name as struct
|
||||
;; (should always be an identifier)
|
||||
[(syntax-property e 'constructor-for) => (λ (Cons)
|
||||
(⊢ e (type-env-lookup Cons)))]
|
||||
;; 2nd case handles identifiers that are not struct constructors
|
||||
[(identifier? e)
|
||||
; handle this here bc there's no #%var form
|
||||
; but some ids, like primops, may already have type
|
||||
(define e+ (local-expand e 'expression null ctx))
|
||||
(if (has-type? e+) e+ (⊢ e (type-env-lookup e)))]
|
||||
;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
|
||||
;; ow forms like lambda and app won't get properly assigned types
|
||||
[else (local-expand e 'expression null ctx)]))
|
||||
(define-for-syntax (expand/df/module-ctx def)
|
||||
(local-expand def 'module #f))
|
||||
(define-for-syntax (expand/df/mb-ctx def)
|
||||
(local-expand def 'module-begin #f))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user