From ee413b96a2d06ba31c7adfd02231590eb7d9832d Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 May 2015 15:01:49 -0400
Subject: [PATCH] add define-primop

---
 tapl/stlc+lit.rkt             |  9 ++--
 tapl/stlc.rkt                 | 32 ++++++++-----
 tapl/tests/stlc+lit-tests.rkt |  9 +++-
 tapl/typecheck.rkt            | 85 ++++++++++++++++++++++++++++-------
 4 files changed, 103 insertions(+), 32 deletions(-)

diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index 0b09e74..466fcdf 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -2,13 +2,12 @@
 (require
   (for-syntax racket/base syntax/parse)
   "typecheck.rkt")
-(require (prefix-in stlc: "stlc.rkt"))
+(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
+         (except-in "stlc.rkt" #%app λ))
 (provide (rename-out [datum/tc #%datum]
                      [stlc:#%app #%app]
                      [stlc:λ λ]))
-(provide Int
-         (rename-out [stlc:→ →]))
-(provide #%module-begin #%top-interaction #%top require)
+(provide (all-from-out "stlc.rkt"))
  
 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
 ;; forms from stlc.rkt
@@ -17,6 +16,8 @@
 
 (define-base-type Int)
 
+(define-primop + : (Int Int → Int))
+
 (define-syntax (datum/tc stx)
   (syntax-parse stx
     [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index e77b256..2fa8183 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -1,9 +1,8 @@
 #lang racket/base
 (require
-  (for-syntax racket/base syntax/parse syntax/stx "stx-utils.rkt")
+  (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
   "typecheck.rkt")
-(provide (rename-out [λ/tc λ] [app/tc #%app])
-         →)
+(provide (rename-out [λ/tc λ] [app/tc #%app]))
 (provide #%module-begin #%top-interaction #%top require)
  
 ;; Simply-Typed Lambda Calculus
@@ -22,13 +21,26 @@
 (define-syntax (app/tc stx)
   (syntax-parse stx #:literals (→)
     [(_ e_fn e_arg ...)
-     #:with (e_fn- (τ ... → τ_res)) (infer+erase #'e_fn)
+     #:with (e_fn- τ_fn) (infer+erase #'e_fn)
+     #:fail-unless (→? #'τ_fn)
+                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+     #:with (τ ... → τ_res) #'τ_fn
      #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
-     #:fail-unless (= (stx-length #'(τ ...))
-                      (stx-length #'(τ_arg ...)))
-                   (format "Wrong number of arguments: given ~a, expected ~a\n"
-                           (stx-length #'(τ_arg ...)) (stx-length #'(τ ...)))
+;     #:fail-unless (= (stx-length #'(τ ...))
+;                      (stx-length #'(τ_arg ...)))
+;                   (format "Wrong number of arguments: given ~a, expected ~a\n"
+;                           (stx-length #'(τ_arg ...)) (stx-length #'(τ ...)))
      #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
-                   (format "Arguments have wrong type: given ~a, expected ~a\n"
-                           (syntax->datum #'(τ_arg ...)) (syntax->datum #'(τ ...)))
+                   (string-append
+                    (format
+                     "Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
+                     (syntax->datum #'e_fn))
+                    (string-join
+                     (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
+                     ", ")
+                    "\nexpect arguments with type: "
+                    (string-join
+                     (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
+                     ", "))
      (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index dd6faf1..253dc3e 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/tapl/tests/stlc+lit-tests.rkt
@@ -11,4 +11,11 @@
 (check-type (λ ([f : (Int → Int)]) 1) : ((Int → Int) → Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 ;((λ ([x : Bool]) x) 1)
-;(λ ([x : Bool]) x)
\ No newline at end of file
+;(λ ([x : Bool]) x)
+(typecheck-fail (λ ([f : Int]) (f 1 2)))
+(check-type (λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
+            : ((Int Int → Int) Int Int → Int))
+(check-type ((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x)))
+(typecheck-fail (λ ([x : (Int → Int)]) (+ x x)))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 4bd86c4..31ef5cd 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -1,6 +1,6 @@
 #lang racket/base
 (require
-  (for-syntax racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt")
+  (for-syntax racket/base syntax/parse racket/list racket/syntax syntax/stx "stx-utils.rkt")
   (for-meta 2 racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt"))
 (provide 
  (for-syntax (all-defined-out))
@@ -23,15 +23,27 @@
 (define-syntax (define-base-type stx)
   (syntax-parse stx
     [(_ τ:id)
-     #'(define-syntax (τ stx)
-         (syntax-parse stx
-           [_ (error 'Int "Cannot use type at run time.")]))]))
+     #'(begin
+         (provide τ)
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [_ (error 'Int "Cannot use type at run time.")])))]))
 (define-syntax (define-type-constructor stx)
   (syntax-parse stx
     [(_ τ:id)
-     #'(define-syntax (τ stx)
-         (syntax-parse stx
-           [_ (error 'Int "Cannot use type at run time.")]))]))
+     #:with τ? (format-id #'τ "~a?" #'τ)
+     #'(begin
+         (provide τ)
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [_ (error 'Int "Cannot use type at run time.")]))
+         (define-for-syntax (τ? stx)
+           (syntax-parse stx
+             [(τ_arg (... ...))
+              (for/or ([id (syntax->list #'(τ_arg (... ...)))])
+                (type=? #'τ id))]
+             [_ #f]))
+         )]))
 
 ;; type classes
 (begin-for-syntax
@@ -56,21 +68,21 @@
       [(b:typed-binding ...)
        #:with (x ...) #'(b.x ...)
        #:with (τ ...) #'(b.τ ...)
-;       #:with arr (datum->syntax e '→)
        #:with
        (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
        (expand/df
         #`(λ (x ...)
             (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
-;       (list #'(lam xs+ e+) #`(τ ... arr #,(typeof #'e+)))]))
        (list #'xs+ #'e+ (typeof #'e+))]))
 
   (define (infer+erase e)
     (define e+ (expand/df e))
     (list e+ (typeof e+)))
-  (define (infers+erase es) (stx-map infer+erase es))
+  (define (infers+erase es)
+    (stx-map infer+erase es))
   (define (types=? τs1 τs2)
-    (stx-andmap type=? τs1 τs2))
+    (and (= (stx-length τs1) (stx-length τs2))
+         (stx-andmap type=? τs1 τs2)))
   
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
@@ -81,14 +93,14 @@
 
   ;; assert-type : Syntax Type -> Boolean
   ;; Returns #t if (typeof e)==τ, else type error
-  (define (assert-type e τ)
+  #;(define (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) τ)))
-  (define (assert-types es τs)
+  #;(define (assert-types es τs)
     (stx-andmap assert-type es τs))
 
   ;; type=? : Type Type -> Boolean
@@ -97,9 +109,11 @@
     (syntax-parse #`(#,τ1 #,τ2)
       ; → should not be datum literal;
       ; adding a type constructor should extend type equality
-      #:datum-literals (→)
+;      #:datum-literals (→)
       [(x:id y:id) (free-identifier=? τ1 τ2)]
-      [((x ... → x_out) (y ... → y_out))
+      [((τ1 ...) (τ2 ...))
+       (types=? #'(τ1 ...) #'(τ2 ...))]
+      #;[((x ... → x_out) (y ... → y_out))
        (and (type=? #'x_out #'y_out)
             (stx-andmap type=? #'(x ...) #'(y ...)))]
       [_ #f]))
@@ -134,10 +148,47 @@
      'TYPE-ERROR
      (format (string-append "~a (~a:~a): " msg) 
              (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src) 
-             (syntax->datum args) ...))))
+             (syntax->datum args) ...)))
+
+  )
+
+(define-syntax (define-primop stx)
+    (syntax-parse stx #:datum-literals (:)
+      [(_ op:id : τ)
+       #:with op/tc (generate-temporary #'op)
+       #`(begin
+           (provide (rename-out [op/tc op]))
+           (define-syntax (op/tc stx)
+             (syntax-parse stx
+               [f:id (⊢ (syntax/loc stx op) #'τ)] ; HO case
+               [(_ x (... ...))
+                #:with app (datum->syntax stx '#%app)
+                #:with op (format-id stx "~a" #'op)
+                #'(app op x (... ...))]
+               #;[(_ 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)])))]))
 
 ;; type environment -----------------------------------------------------------
-(begin-for-syntax
+#;(begin-for-syntax
   
   ;; A Variable is a Symbol
   ;; A TypeEnv is a [HashOf Variable => Type]