From 3a97efcb24aa3b89af45cd3941d22d2c351c925e Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 20 Jun 2016 15:09:39 -0400 Subject: [PATCH] implement stlc+reco-var and stlc+cons with typed-lang-builder --- tapl/tests/stlc+cons-tests.rkt | 10 +- tapl/tests/stlc+reco+var-tests.rkt | 12 +- tapl/typed-lang-builder/stlc+cons.rkt | 81 ++++++++++ tapl/typed-lang-builder/stlc+reco+var.rkt | 175 ++++++++++++++++++++++ 4 files changed, 267 insertions(+), 11 deletions(-) create mode 100644 tapl/typed-lang-builder/stlc+cons.rkt create mode 100644 tapl/typed-lang-builder/stlc+reco+var.rkt diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt index 00857f1..7c40cb0 100644 --- a/tapl/tests/stlc+cons-tests.rkt +++ b/tapl/tests/stlc+cons-tests.rkt @@ -1,13 +1,13 @@ -#lang s-exp "../stlc+cons.rkt" +#lang s-exp "../typed-lang-builder/stlc+cons.rkt" (require "rackunit-typechecking.rkt") (typecheck-fail (cons 1 2) - #:with-msg "Expected expression 2 to have List type, got: Int") + #:with-msg "expected \\(List Int\\), given Int\n *expression: 2") ;(typecheck-fail (cons 1 nil) ; #:with-msg "nil: requires type annotation") (check-type (cons 1 nil) : (List Int)) (check-type (cons 1 (nil {Int})) : (List Int)) -(typecheck-fail nil #:with-msg "nil requires type annotation") +(typecheck-fail nil #:with-msg "nil: no expected type, add annotations") (typecheck-fail (nil Int) #:with-msg @@ -35,7 +35,7 @@ (typecheck-fail (isnil (head fn-lst)) #:with-msg - "Expected expression \\(head fn-lst\\) to have List type, got: \\(→ Int Int\\)") + "Expected List type, got: \\(→ Int Int\\)") (check-type (isnil (tail fn-lst)) : Bool ⇒ #t) (check-type (head fn-lst) : (→ Int Int)) (check-type ((head fn-lst) 25) : Int ⇒ 35) @@ -45,7 +45,7 @@ (typecheck-fail (cons 1 1) #:with-msg - "Expected expression 1 to have List type, got: Int") + "expected \\(List Int\\), given Int\n *expression: 1") ;; previous tests: ------------------------------------------------------------ ;; define-type-alias diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt index 7d07f44..c84e03c 100644 --- a/tapl/tests/stlc+reco+var-tests.rkt +++ b/tapl/tests/stlc+reco+var-tests.rkt @@ -1,4 +1,4 @@ -#lang s-exp "../stlc+reco+var.rkt" +#lang s-exp "../typed-lang-builder/stlc+reco+var.rkt" (require "rackunit-typechecking.rkt") ;; define-type-alias @@ -49,8 +49,8 @@ (check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit])) (typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x) (var coffee = (void) as (∨ [coffee : Unit]))) - #:with-msg (expected "(∨ [coffee : Unit] [tea : Unit])" - #:given "(∨ [coffee : Unit])")) + #:with-msg (string-append "expected: +\\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\)\n" + " *given: +\\(∨ \\(coffee : Unit\\)\\)")) (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit])) (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) @@ -75,7 +75,7 @@ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) [coffee x => "1"] [tea x => 2]) - #:with-msg "branches have different types") + #:with-msg "branches have incompatible types: String and Int") (check-type (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit])) [coffee x => x] @@ -102,11 +102,11 @@ (typecheck-fail (var name = "Steve" as Int) #:with-msg - "Expected ∨ type, got: Int") + "Expected the expected type to be a ∨ type, got: Int") (typecheck-fail (case 1 [racket x => 1]) #:with-msg - "Expected expression 1 to have ∨ type, got: Int") + "Expected ∨ type, got: Int") (typecheck-fail (λ ([x : (∨)]) x) #:with-msg "Improper usage of type constructor ∨: \\(∨\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)") diff --git a/tapl/typed-lang-builder/stlc+cons.rkt b/tapl/typed-lang-builder/stlc+cons.rkt new file mode 100644 index 0000000..5c6fa0f --- /dev/null +++ b/tapl/typed-lang-builder/stlc+cons.rkt @@ -0,0 +1,81 @@ +#lang macrotypes/tapl/typed-lang-builder +(extends "stlc+reco+var.rkt") + +;; Simply-Typed Lambda Calculus, plus cons +;; Types: +;; - types from stlc+reco+var.rkt +;; - List constructor +;; Terms: +;; - terms from stlc+reco+var.rkt + +;; TODO: enable HO use of list primitives + +(define-type-constructor List) + +(define-typed-syntax nil + [(nil ~! τi:type-ann) ▶ + -------- + [⊢ [[_ ≫ null-] ⇒ (: (List τi.norm))]]] + ; minimal type inference + [nil:id ⇐ (: (~List τ)) ▶ + -------- + [⊢ [[_ ≫ null-] ⇐ (: _)]]]) +(define-typed-syntax cons + [(cons e1 e2) ▶ + [⊢ [[e1 ≫ e1-] ⇒ (: τ1)]] + [⊢ [[e2 ≫ e2-] ⇐ (: (List τ1))]] + -------- + [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ (: (List τ1))]]]) +(define-typed-syntax isnil + [(isnil e) ▶ + [⊢ [[e ≫ e-] ⇒ (: (~List _))]] + -------- + [⊢ [[_ ≫ (null?- e-)] ⇒ (: Bool)]]]) +(define-typed-syntax head + [(head e) ▶ + [⊢ [[e ≫ e-] ⇒ (: (~List τ))]] + -------- + [⊢ [[_ ≫ (car- e-)] ⇒ (: τ)]]]) +(define-typed-syntax tail + [(tail e) ▶ + [⊢ [[e ≫ e-] ⇒ (: τ-lst)]] + [#:fail-unless (List? #'τ-lst) + (format "Expected a list type, got: ~a" (type->str #'τ-lst))] + -------- + [⊢ [[_ ≫ (cdr- e-)] ⇒ (: τ-lst)]]]) +(define-typed-syntax list + [(list) ▶ + -------- + [_ ≻ nil]] + [(list x . rst) ⇐ (: (~List τ)) ▶ ; has expected type + -------- + [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ (: _)]]] + [(list x . rst) ▶ ; no expected type + -------- + [_ ≻ (cons x (list . rst))]]) +(define-typed-syntax reverse + [(reverse e) ▶ + [⊢ [[e ≫ e-] ⇒ (: τ-lst)]] + [#:fail-unless (List? #'τ-lst) + (format "Expected a list type, got: ~a" (type->str #'τ-lst))] + -------- + [⊢ [[_ ≫ (reverse- e-)] ⇒ (: τ-lst)]]]) +(define-typed-syntax length + [(length e) ▶ + [⊢ [[e ≫ e-] ⇒ (: τ-lst)]] + [#:fail-unless (List? #'τ-lst) + (format "Expected a list type, got: ~a" (type->str #'τ-lst))] + -------- + [⊢ [[_ ≫ (length- e-)] ⇒ (: Int)]]]) +(define-typed-syntax list-ref + [(list-ref e n) ▶ + [⊢ [[e ≫ e-] ⇒ (: (~List τ))]] + [⊢ [[n ≫ n-] ⇐ (: Int)]] + -------- + [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ (: τ)]]]) +(define-typed-syntax member + [(member v e) ▶ + [⊢ [[e ≫ e-] ⇒ (: (~List τ))]] + [⊢ [[v ≫ v-] ⇐ (: τ)]] + -------- + [⊢ [[_ ≫ (member- v- e-)] ⇒ (: Bool)]]]) diff --git a/tapl/typed-lang-builder/stlc+reco+var.rkt b/tapl/typed-lang-builder/stlc+reco+var.rkt new file mode 100644 index 0000000..88084d6 --- /dev/null +++ b/tapl/typed-lang-builder/stlc+reco+var.rkt @@ -0,0 +1,175 @@ +#lang macrotypes/tapl/typed-lang-builder +(extends "stlc+tup.rkt" #:except × ×? tup proj + #:rename [~× ~stlc:×]) +(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*)) + + +;; Simply-Typed Lambda Calculus, plus records and variants +;; Types: +;; - types from stlc+tup.rkt +;; - redefine tuple type × to records +;; - sum type constructor ∨ +;; Terms: +;; - terms from stlc+tup.rkt +;; - redefine tup to records +;; - sums (var) +;; TopLevel: +;; - define (values only) +;; - define-type-alias + +(provide define-type-alias) +(define-syntax define-type-alias + (syntax-parser + [(define-type-alias alias:id τ:type) + #'(define-syntax alias (make-variable-like-transformer #'τ.norm))] + [(define-type-alias (f:id x:id ...) ty) + #'(define-syntax (f stx) + (syntax-parse stx + [(_ x ...) #'ty]))])) + +(define-typed-syntax define + [(define x:id : τ:type e:expr) ▶ + ;This wouldn't work with mutually recursive definitions + ;[⊢ [[e ≫ e-] ⇐ τ.norm]] + ;So expand to an ann form instead. + -------- + [_ ≻ (begin- + (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) + (define- y (ann e : τ.norm)))]] + [(define x:id e) ▶ + [⊢ [[e ≫ e-] ⇒ (: τ)]] + [#:with y (generate-temporary #'x)] + -------- + [_ ≻ (begin- + (define-syntax x (make-rename-transformer (⊢ y : τ))) + (define- y e-))]]) + + +; re-define tuples as records +; dont use define-type-constructor because I want the : literal syntax +(define-syntax × + (syntax-parser #:datum-literals (:) + [(_ [label:id : τ:type] ...) + #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...)) + #`(stlc+tup:× valid-τ ...)])) +(begin-for-syntax + (define-syntax ~× + (pattern-expander + (syntax-parser #:datum-literals (:) + [(_ [l : τ_l] (~and ddd (~literal ...))) + #'(~stlc:× ((~literal #%plain-app) (quote l) τ_l) ddd)] + [(_ . args) + #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...)) + (~parse args #'((l τ_l) (... ...))))]))) + (define ×? stlc+tup:×?) + (define-syntax ~×* + (pattern-expander + (syntax-parser #:datum-literals (:) + [(_ [l : τ_l] (~and ddd (~literal ...))) + #'(~or (~× [l : τ_l] ddd) + (~and any (~do (type-error + #:src #'any + #:msg "Expected × type, got: ~a" #'any))))])))) + +(begin-for-syntax + (define (stx-assoc-ref stx-lst lookup-k #:else [fail (λ () #f)]) + (define match_res (stx-assoc lookup-k stx-lst)) + (cond [match_res + (stx-cadr match_res)] + [else + (fail)])) + (define (×-ref ×-type l) + (syntax-parse ×-type + [(~× [l_τ : τ] ...) + (define res + (stx-assoc-ref #'([l_τ τ] ...) l #:else (λ () (error 'X-ref "bad!")))) + (add-orig res (get-orig res))]))) + +;; records +(define-typed-syntax tup #:datum-literals (=) + [(tup [l:id = e] ...) ▶ + [⊢ [[e ≫ e-] ⇒ (: τ)] ...] + -------- + [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ (: (× [l : τ] ...))]]]) +(define-typed-syntax proj #:literals (quote) + [(proj e_rec l:id) ▶ + [⊢ [[e_rec ≫ e_rec-] ⇒ (: τ_e)]] + [#:fail-unless (×? #'τ_e) + (format "Expected expression ~s to have × type, got: ~a" + (syntax->datum #'e_rec) (type->str #'τ_e))] + [#:with τ_l (×-ref #'τ_e #'l)] + -------- + [⊢ [[_ ≫ (cadr- (assoc- 'l e_rec-))] ⇒ (: τ_l)]]]) + +(define-type-constructor ∨/internal #:arity >= 0) + +;; variants +(define-syntax ∨ + (syntax-parser #:datum-literals (:) + [(∨ (~and [label:id : τ:type] x) ...) + #:when (> (stx-length #'(x ...)) 0) + #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...)) + #'(∨/internal valid-τ ...)] + [any + (type-error #:src #'any + #:msg (string-append + "Improper usage of type constructor ∨: ~a, " + "expected (∨ [label:id : τ:type] ...+)") + #'any)])) +(begin-for-syntax + (define ∨? ∨/internal?) + (define-syntax ~∨ + (pattern-expander + (syntax-parser #:datum-literals (:) + [(_ [l : τ_l] (~and ddd (~literal ...))) + #'(~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)] + [(_ . args) + #'(~and (~∨/internal ((~literal #%plain-app) (quote l) τ_l) (... ...)) + (~parse args #'((l τ_l) (... ...))))]))) + (define-syntax ~∨* + (pattern-expander + (syntax-parser #:datum-literals (:) + [(_ [l : τ_l] (~and ddd (~literal ...))) + #'(~and (~or (~∨ [l : τ_l] ddd) + (~and any (~do (type-error + #:src #'any + #:msg "Expected ∨ type, got: ~a" #'any)))) + ~!)])))) ; dont backtrack here + +(begin-for-syntax + (define (∨-ref ∨-type l #:else [fail (λ () #f)]) + (syntax-parse ∨-type + [(~∨ [l_τ : τ] ...) + (define res + (stx-assoc-ref #'([l_τ τ] ...) l #:else fail)) + (add-orig res (get-orig res))]))) + +(define-typed-syntax var #:datum-literals (as =) + [(var l:id = e as τ:type) ▶ + -------- + [_ ≻ (ann (var l = e) : τ.norm)]] + [(var l:id = e) ⇐ (: τ) ▶ + [#:fail-unless (∨? #'τ) + (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))] + [#:with τ_e + (∨-ref #'τ #'l #:else + (λ () (raise-syntax-error #f + (format "~a field does not exist" (syntax->datum #'l)) + stx)))] + [⊢ [[e ≫ e-] ⇐ (: τ_e)]] + -------- + [⊢ [[_ ≫ (list- 'l e)] ⇐ (: _)]]]) + +(define-typed-syntax case + #:datum-literals (of =>) + [(case e [l:id x:id => e_l] ...) ▶ + [#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"] + [⊢ [[e ≫ e-] ⇒ (: (~∨* [l_x : τ_x] ...))]] + [#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"] + [#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"] + [() ([x : τ_x ≫ x-]) ⊢ [[e_l ≫ e_l-] ⇒ (: τ_el)]] ... + -------- + [⊢ [[_ ≫ + (let- ([l_e (car- e-)]) + (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))] + ⇒ (: (⊔ τ_el ...))]]])