From 3bc035fde1e0a17129152e8e65ba316bd4615ddd Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Mon, 20 Jun 2016 15:05:25 -0400
Subject: [PATCH] start on typed-lang-builder

with stlc and stlc+lit
---
 tapl/tests/stlc+lit-tests.rkt                 |  11 +-
 tapl/tests/stlc-tests.rkt                     |   2 +-
 tapl/typed-lang-builder/lang/reader.rkt       |   2 +
 tapl/typed-lang-builder/stlc+lit.rkt          |  40 +++
 tapl/typed-lang-builder/stlc.rkt              |  54 ++++
 .../typed-lang-builder/typed-lang-builder.rkt | 291 ++++++++++++++++++
 6 files changed, 393 insertions(+), 7 deletions(-)
 create mode 100644 tapl/typed-lang-builder/lang/reader.rkt
 create mode 100644 tapl/typed-lang-builder/stlc+lit.rkt
 create mode 100644 tapl/typed-lang-builder/stlc.rkt
 create mode 100644 tapl/typed-lang-builder/typed-lang-builder.rkt

diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index 95f6bc7..c289a27 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/tapl/tests/stlc+lit-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+lit.rkt"
+#lang s-exp "../typed-lang-builder/stlc+lit.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; thunk
@@ -36,7 +36,7 @@
 (typecheck-fail
  (λ ([f : Int]) (f 1 2))
  #:with-msg
- "Expected expression f to have → type, got: Int")
+ "Expected → type, got: Int")
 
 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
             : (→ (→ Int Int Int) Int Int Int))
@@ -44,14 +44,13 @@
 
 (typecheck-fail
  (+ 1 (λ ([x : Int]) x))
- #:with-msg (expected "Int, Int" #:given "Int, (→ Int Int)"))
+ #:with-msg "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)")
 (typecheck-fail
  (λ ([x : (→ Int Int)]) (+ x x))
-  #:with-msg (expected "Int, Int" #:given "(→ Int Int), (→ Int Int)"))
+  #:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)")
 (typecheck-fail
  ((λ ([x : Int] [y : Int]) y) 1)
- #:with-msg (expected "Int, Int" #:given "Int"
-                      #:note "Wrong number of arguments"))
+ #:with-msg "wrong number of arguments: expected 2, given 1")
 
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
 
diff --git a/tapl/tests/stlc-tests.rkt b/tapl/tests/stlc-tests.rkt
index 2502b9e..ebdd1ca 100644
--- a/tapl/tests/stlc-tests.rkt
+++ b/tapl/tests/stlc-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../stlc.rkt"
+#lang s-exp "../typed-lang-builder/stlc.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; cannot write any terms without base types, but can check some errors
diff --git a/tapl/typed-lang-builder/lang/reader.rkt b/tapl/typed-lang-builder/lang/reader.rkt
new file mode 100644
index 0000000..0deb76e
--- /dev/null
+++ b/tapl/typed-lang-builder/lang/reader.rkt
@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+macrotypes/tapl/typed-lang-builder/typed-lang-builder
diff --git a/tapl/typed-lang-builder/stlc+lit.rkt b/tapl/typed-lang-builder/stlc+lit.rkt
new file mode 100644
index 0000000..d5d92b7
--- /dev/null
+++ b/tapl/typed-lang-builder/stlc+lit.rkt
@@ -0,0 +1,40 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc.rkt")
+(provide define-primop)
+
+;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
+;; Types:
+;; - types from stlc.rkt
+;; - Int
+;; Terms:
+;; - terms from stlc.rkt
+;; - numeric literals
+;; - prim +
+;; Typechecking forms:
+;; - define-primop
+
+(define-base-type Int)
+
+(define-syntax define-primop
+  (syntax-parser #:datum-literals (:)
+    [(define-primop op:id : τ:type)
+     #:with op/tc (generate-temporary #'op)
+     #'(begin-
+         (provide- (rename-out- [op/tc op]))
+         (define-primop op/tc op : τ))]
+    [(define-primop op/tc op : τ)
+     #'(begin-
+         ; rename transformer doesnt seem to expand at the right time
+         ; - op still has no type in #%app
+         (define-syntax op/tc
+           (make-variable-like-transformer (assign-type #'op #'τ))))]))
+
+(define-primop + : (→ Int Int Int))
+
+(define-typed-syntax #%datum
+  [(#%datum . n:integer) ▶
+   --------
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Int)]]]
+  [(_ . x) ▶
+   --------
+   [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
diff --git a/tapl/typed-lang-builder/stlc.rkt b/tapl/typed-lang-builder/stlc.rkt
new file mode 100644
index 0000000..d059701
--- /dev/null
+++ b/tapl/typed-lang-builder/stlc.rkt
@@ -0,0 +1,54 @@
+#lang macrotypes/tapl/typed-lang-builder
+(provide (for-syntax current-type=? types=?))
+
+(begin-for-syntax
+  ;; type eval
+  ;; - type-eval == full expansion == canonical type representation
+  ;; - must expand because:
+  ;;   - checks for unbound identifiers (ie, undefined types)
+  ;;   - checks for valid types, ow can't distinguish types and terms
+  ;;     - could parse types but separate parser leads to duplicate code
+  ;;   - later, expanding enables reuse of same mechanisms for kind checking
+  ;;     and type application
+  (define (type-eval τ)
+    ; TODO: optimization: don't expand if expanded
+    ; currently, this causes problems when
+    ; combining unexpanded and expanded types to create new types
+    (add-orig (expand/df τ) τ))
+
+  (current-type-eval type-eval))
+
+(define-syntax-category type)
+(define-type-constructor → #:arity >= 1
+  #:arg-variances (λ (stx)
+                    (syntax-parse stx
+                      [(_ τ_in ... τ_out)
+                       (append
+                        (make-list (stx-length #'[τ_in ...]) contravariant)
+                        (list covariant))])))
+
+(define-typed-syntax λ #:datum-literals (:)
+  [(λ ([x:id : τ_in:type] ...) e) ▶
+   [() ([x : τ_in.norm ≫ x-] ...) ⊢ [[e ≫ e-] ⇒ (: τ_out)]]
+   --------
+   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇒ (: (→ τ_in.norm ... τ_out))]]]
+  [(λ (x:id ...) e) ⇐ (: (~→ τ_in ... τ_out)) ▶
+   [() ([x : τ_in ≫ x-] ...) ⊢ [[e ≫ e-] ⇐ (: τ_out)]]
+   --------
+   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇐ (: _)]]])
+
+(define-typed-syntax #%app
+  [(_ e_fn e_arg ...) ▶
+   [⊢ [[e_fn ≫ e_fn-] ⇒ (: (~→ τ_in ... τ_out))]]
+   [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+    (format "wrong number of arguments: expected ~a, given ~a"
+            (stx-length #'[τ_in ...]) (stx-length #'[e_arg ...]))] 
+   [⊢ [[e_arg ≫ e_arg-] ⇐ (: τ_in)] ...]
+   --------
+   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ (: τ_out)]]])
+
+(define-typed-syntax ann #:datum-literals (:)
+  [(_ e : τ:type) ▶
+   [⊢ [[e ≫ e-] ⇐ (: τ.norm)]]
+   --------
+   [⊢ [[_ ≫ e-] ⇒ (: τ.norm)]]])
diff --git a/tapl/typed-lang-builder/typed-lang-builder.rkt b/tapl/typed-lang-builder/typed-lang-builder.rkt
new file mode 100644
index 0000000..9bb4435
--- /dev/null
+++ b/tapl/typed-lang-builder/typed-lang-builder.rkt
@@ -0,0 +1,291 @@
+#lang racket/base
+
+(provide (except-out (all-from-out "../typecheck.rkt") -define-typed-syntax)
+         define-typed-syntax
+         (for-syntax syntax-parse/typed-syntax))
+
+(require (rename-in
+          "../typecheck.rkt"
+          [define-typed-syntax -define-typed-syntax]
+          ))
+
+(module syntax-classes racket/base
+  (provide (all-defined-out))
+  (require (for-meta -1 (except-in "../typecheck.rkt" #%module-begin))
+           (for-meta -2 (except-in "../typecheck.rkt" #%module-begin)))
+  (define-syntax-class ---
+    [pattern (~datum --------)])
+  (define-syntax-class elipsis
+    [pattern (~literal ...)])
+  (define-splicing-syntax-class props
+    [pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))])
+  (define-splicing-syntax-class id+props+≫
+    #:datum-literals (≫)
+    #:attributes ([x- 1] [ctx 1])
+    [pattern (~seq [x:id props:props ≫ x--:id])
+             #:with [x- ...] #'[x--]
+             #:with [ctx ...] #'[[x props.stuff ...]]]
+    [pattern (~seq [x:id props:props ≫ x--:id] ooo:elipsis)
+             #:with [x- ...] #'[x-- ooo]
+             #:with [ctx ...] #'[[x props.stuff ...] ooo]])
+  (define-splicing-syntax-class id-props+≫*
+    #:attributes ([x- 1] [ctx 1])
+    [pattern (~seq ctx1:id+props+≫ ...)
+             #:with [x- ...] #'[ctx1.x- ... ...]
+             #:with [ctx ...] #'[ctx1.ctx ... ...]])
+  (define-splicing-syntax-class inf
+    #:datum-literals (⊢ ⇒ ⇐ ≫ :)
+    #:attributes ([pre 1] [e-stx 1] [e-pat 1] τ-tagss [τ-pats 1] k-tagss [k-pats 1] [post 1])
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*])
+             #:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()]]]
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*] ooo:elipsis)
+             #:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()] ooo]]
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)])
+             #:with [pre ...] #'[]
+             #:with [e-stx ...] #'[e-stx*]
+             #:with [e-pat ...] #'[e-pat*]
+             #:with τ-tagss #'(list (list 'τ-props.k ...))
+             #:with [τ-pats ...] #'[[τ-props.v ...]]
+             #:with k-tagss #'(list (list 'k-props.k ...))
+             #:with [k-pats ...] #'[[k-props.v ...]]
+             #:with [post ...] #'[]]
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)] ooo:elipsis)
+             #:with [pre ...] #'[]
+             #:with [e-stx ...] #'[e-stx* ooo]
+             #:with [e-pat ...] #'[e-pat* ooo]
+             
+             #:with τ-tagss #'(map cdr (syntax->datum #'[[e-stx* τ-props.k ...] ooo]))
+             #:with [τ-pats ...] #'[[τ-props.v ...] ooo]
+             #:with k-tagss #'(map cdr (syntax->datum #'[[e-stx* k-props.k ...] ooo]))
+             #:with [k-pats ...] #'[[k-props.v ...] ooo]
+             #:with [post ...] #'[]]
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)])
+             #:with τ-tmp (generate-temporary 'τ)
+             #:with τ-stx-tmp (generate-temporary #'τ-stx*)
+             #:with [pre ...] #'[#:with τ-stx-tmp ((current-type-eval) #'τ-stx*)]
+             #:with [e-stx ...] #'[(add-expected e-stx* τ-stx-tmp)]
+             #:with [e-pat ...] #'[e-pat*]
+             #:with τ-tagss #'(list (list ':))
+             #:with [τ-pats ...] #'[[τ-tmp]]
+             #:with k-tagss #'(list (list))
+             #:with [k-pats ...] #'[[]]
+             #:with [post ...]
+             #'[#:with
+                (~and _
+                  (~post
+                   (~post
+                    (~fail
+                     #:unless (typecheck? #'τ-tmp #'τ-stx-tmp)
+                     (format "type mismatch: expected ~a, given ~a\n  expression: ~s"
+                             (type->str #'τ-stx-tmp)
+                             (type->str #'τ-tmp)
+                             (syntax->datum #'e-stx*))))))
+                this-syntax]]
+    [pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)] ooo:elipsis)
+             #:with τ-tmp (generate-temporary 'τ)
+             #:with τ-stx-tmp (generate-temporary #'τ-stx*)
+             #:with [pre ...] #'[#:with [τ-stx-tmp ooo]
+                                 (stx-map (current-type-eval) #'[τ-stx* ooo])]
+             #:with [e-stx ...] #'[(add-expected e-stx* τ-stx-tmp) ooo]
+             #:with [e-pat ...] #'[e-pat* ooo]
+             #:with τ-tagss #'(map cdr (syntax->datum #'[[τ-stx-tmp :] ooo]))
+             #:with [τ-pats ...] #'[[τ-tmp] ooo]
+             #:with k-tagss #'(list)
+             #:with [k-pats ...] #'[]
+             #:with [post ...]
+             #'[#:with
+                (~and _
+                  (~post
+                   (~post
+                    (~fail
+                     #:unless (typechecks? #'[τ-tmp ooo] #'[τ-stx-tmp ooo])
+                     (format (string-append "type mismatch\n"
+                                            "  expected:    ~a\n"
+                                            "  given:       ~a\n"
+                                            "  expressions: ~a")
+                             (string-join (stx-map type->str #'[τ-stx-tmp ooo]) ", ")
+                             (string-join (stx-map type->str #'[τ-tmp ooo]) ", ")
+                             (string-join (map ~s (stx-map syntax->datum #'[e-stx* ooo])) ", "))))))
+                this-syntax]]
+    )
+  (define-splicing-syntax-class inf*
+    [pattern (~seq inf:inf ...)
+             #:with [pre ...] #'[inf.pre ... ...]
+             #:with [e-stx ...] #'[inf.e-stx ... ...]
+             #:with [e-pat ...] #'[inf.e-pat ... ...]
+             #:with τ-tagss #'(append inf.τ-tagss ...)
+             #:with [τ-pats ...] #'[inf.τ-pats ... ...]
+             #:with k-tagss #'(append inf.k-tagss ...)
+             #:with [k-pats ...] #'[inf.k-pats ... ...]
+             #:with [post ...] #'[inf.post ... ...]])
+  (define-splicing-syntax-class clause
+    #:attributes ([stuff 1])
+    #:datum-literals (⊢ ⇒ ⇐ ≫ τ⊑ :)
+    [pattern [⊢ (~and (~seq inf-stuff ...) (~seq inf:inf ...))]
+             #:with [:clause] #'[[() () ⊢ inf-stuff ...]]]
+    [pattern (~seq [⊢ (~and (~seq inf-stuff ...) (~seq inf:inf ...))] ooo:elipsis)
+             #:with [:clause] #'[[() () ⊢ inf-stuff ...] ooo]]
+    [pattern [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*]
+             #:with e:id (generate-temporary)
+             #:with τ:id (generate-temporary)
+             #:with ooo (quote-syntax ...)
+             #:with [stuff ...]
+             #'[inf.pre ...
+                #:with [(tvctx.x- ...) (ctx.x- ...) (e ooo) (τ ooo)]
+                (infer #:tvctx #'(tvctx.ctx ...) #:ctx #'(ctx.ctx ...) #'(inf.e-stx ...))
+                #:with [inf.e-pat ...] #'[e ooo]
+                #:with [inf.τ-pats ...]
+                (for/list ([e (in-list (syntax->list #'[e ooo]))]
+                           [tags (in-list inf.τ-tagss)])
+                  (for/list ([tag (in-list tags)])
+                    (typeof e #:tag tag)))
+                #:with [inf.k-pats ...]
+                (for/list ([τ (in-list (syntax->list #'[τ ooo]))]
+                           [tags (in-list inf.k-tagss)])
+                  (for/list ([tag (in-list tags)])
+                    (typeof τ #:tag tag)))
+                inf.post ...]]
+    [pattern (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis)
+             #:with e:id (generate-temporary)
+             #:with τ:id (generate-temporary)
+             ;TODO: What should these do?
+             #:fail-unless (stx-null? #'[inf.pre ...]) "this type of clause does not support elipses"
+             #:fail-unless (stx-null? #'[inf.post ...]) "this type of clause does not support elipses"
+             #:with tvctxss (cond [(stx-null? #'[tvctx.ctx ...]) #'(in-cycle (in-value '()))]
+                                  [else #'(in-list (syntax->list #'[(tvctx.ctx ...) ooo]))])
+             #:with ctxss (cond [(stx-null? #'[ctx.ctx ...]) #'(in-cycle (in-value '()))]
+                                [else #'(in-list (syntax->list #'[(ctx.ctx ...) ooo]))])
+             #:with [stuff ...]
+             #'[#:with [[(tvctx.x- ...) (ctx.x- ...) (e ooo) (τ ooo)] ooo]
+                (for/list ([tvctxs tvctxss]
+                           [ctxs ctxss]
+                           [es (in-list (syntax->list #'[(inf.e-stx ...) ooo]))])
+                  (infer #:tvctx tvctxs #:ctx ctxs es))
+                #:with [(inf.e-pat ...) ooo] #'[(e ooo) ooo]
+                #:with [(inf.τ-pats ...) ooo]
+                (for/list ([es (in-list (syntax->list #'[(e ooo) ooo]))])
+                  (for/list ([e (in-list (syntax->list es))]
+                             [tags (in-list inf.τ-tagss)])
+                    (for/list ([tag (in-list tags)])
+                      (typeof e #:tag tag))))
+                #:with [(inf.k-pats ...) ooo]
+                (for/list ([τs (in-list (syntax->list #'[(τ ooo) ooo]))])
+                  (for/list ([τ (in-list (syntax->list τs))]
+                             [tags (in-list inf.k-tagss)])
+                    (for/list ([tag (in-list tags)])
+                      (typeof τ #:tag tag))))]]
+    [pattern [a τ⊑ b]
+             #:with [stuff ...]
+             #'[#:fail-unless (typecheck? #'a #'b)
+                (format "type mismatch: expected ~a, given ~a"
+                        (type->str #'b)
+                        (type->str #'a))]]
+    [pattern (~seq [a τ⊑ b] ooo:elipsis)
+             #:with [stuff ...]
+             #'[#:fail-unless (typechecks? #'[a ooo] #'[b ooo])
+                (format (string-append "type mismatch\n"
+                                       "  expected:    ~a\n"
+                                       "  given:       ~a")
+                        (string-join (stx-map type->str #'[b ooo]) ", ")
+                        (string-join (stx-map type->str #'[a ooo]) ", "))]]
+    [pattern [#:when condition:expr]
+             #:with [stuff ...]
+             #'[#:when condition]]
+    [pattern [#:with pat:expr expr:expr]
+             #:with [stuff ...]
+             #'[#:with pat expr]]
+    [pattern [#:fail-unless condition:expr message:expr]
+             #:with [stuff ...]
+             #'[#:fail-unless condition message]]
+    )
+  (define-syntax-class last-clause
+    #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
+    [pattern [⊢ [[pat ≫ e-stx] ⇒ (τ-props:props)]]
+             #:with [pre ...]
+             #'[]
+             #:with [stuff ...]
+             #'[(for/fold ([result (quasisyntax/loc this-syntax e-stx)])
+                          ([tag (in-list (list 'τ-props.k ...))]
+                           [τ (in-list (list #`τ-props.v ...))])
+                  (assign-type result τ #:tag tag))]]
+    [pattern [⊢ [[pat ≫ e-stx] ⇐ (: τ-pat)]]
+             #:with τ
+             (generate-temporary #'τ-pat)
+             #:with [pre ...]
+             #'[#:with τ (get-expected-type this-syntax)
+                #:with (~and _ (~post (~fail #:unless (syntax-e #'τ)
+                                             "no expected type, add annotations")))
+                this-syntax
+                #:with τ-pat #'τ]
+             #:with [stuff ...]
+             #'[(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]]
+    [pattern [pat ≻ e-stx]
+             #:with [pre ...]
+             #'[]
+             #:with [stuff ...]
+             #'[(quasisyntax/loc this-syntax e-stx)]]
+    [pattern [pat #:error msg:expr]
+             #:with [pre ...]
+             #'[]
+             #:with [stuff ...]
+             #'[#:fail-unless #f msg
+                ;; should never get here
+                (error msg)]])
+  (define-splicing-syntax-class pat #:datum-literals (⇐ :)
+    [pattern (~seq pat)
+             #:with [stuff ...] #'[]]
+    [pattern (~seq pat ⇐ (: τ-pat))
+             #:with τ (generate-temporary #'τ-pat)
+             #:with [stuff ...]
+             #'[#:with τ (get-expected-type this-syntax)
+                #:with (~and _ (~post (~fail #:unless (syntax-e #'τ)
+                                             "no expected type, add annotations")))
+                this-syntax
+                #:with τ-pat #'τ]])
+  (define-syntax-class rule #:datum-literals (▶)
+    [pattern [pat:pat ▶
+              clause:clause ...
+              :---
+              last-clause:last-clause]
+             #:with norm
+             #'[(~and pat.pat last-clause.pat)
+                pat.stuff ...
+                last-clause.pre ...
+                clause.stuff ... ...
+                last-clause.stuff ...]])
+  )
+(require (for-meta 1 'syntax-classes)
+         (for-meta 2 'syntax-classes))
+
+(define-syntax define-typed-syntax
+  (lambda (stx)
+    (syntax-parse stx
+      [(def name:id
+         (~and (~seq stuff ...) (~or (~seq :keyword _)
+                                     (~seq :keyword)))
+         ...
+         rule:rule
+         ...)
+       #'(-define-typed-syntax
+          name
+          stuff ... ...
+          rule.norm
+          ...)])))
+
+(begin-for-syntax
+  (define-syntax syntax-parse/typed-syntax
+    (lambda (stx)
+      (syntax-parse stx
+        [(stxparse
+          stx-id:id
+          (~and (~seq stuff ...) (~or (~seq :keyword _)
+                                      (~seq :keyword)))
+          ...
+          rule:rule
+          ...)
+         #'(syntax-parse
+               stx-id
+             stuff ... ...
+             rule.norm
+             ...)]))))
+