From a4d7483f2558fbf23f20684222c1839dc4200349 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 20 May 2015 15:26:02 -0400 Subject: [PATCH] stlc+lit: cleanup and comment --- tapl/stlc+lit.rkt | 10 +++++++--- tapl/stlc.rkt | 7 +++---- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt index 466fcdf..8936a2f 100644 --- a/tapl/stlc+lit.rkt +++ b/tapl/stlc+lit.rkt @@ -10,9 +10,13 @@ (provide (all-from-out "stlc.rkt")) ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives -;; forms from stlc.rkt -;; numeric literals -;; prim + +;; Types: +;; - types from stlc.rkt +;; - Int +;; Terms: +;; - terms from stlc.rkt +;; - numeric literals +;; - prim + (define-base-type Int) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index 2fa8183..8ccc1cc 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -6,6 +6,9 @@ (provide #%module-begin #%top-interaction #%top require) ;; Simply-Typed Lambda Calculus +;; - no base type so cannot write any terms +;; Types: → +;; Terms: ;; - var ;; - multi-arg lambda ;; - multi-arg app @@ -27,10 +30,6 @@ (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 (types=? #'(τ ...) #'(τ_arg ...)) (string-append (format