commit 69c97a55124d618c9c3b4607c49cba6b524dc05a parent d29aed64b8c31adf1208e0aebe32d27154f64b89 Author: Stephen Chang <stchang@ccs.neu.edu> Date: Tue, 11 Nov 2014 18:21:43 -0500 start tapl/ dir Diffstat:
| A | tapl/stlc-tests.rkt | | | 2 | ++ |
| A | tapl/stlc.rkt | | | 18 | ++++++++++++++++++ |
| A | tapl/typecheck.rkt | | | 4 | ++++ |
3 files changed, 24 insertions(+), 0 deletions(-)
diff --git a/tapl/stlc-tests.rkt b/tapl/stlc-tests.rkt @@ -0,0 +1 @@ +#lang s-exp "stlc.rkt" +\ No newline at end of file diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt @@ -0,0 +1,17 @@ +#lang racket/base +(require + (for-syntax racket/base syntax/parse)) + +;; Simply-Typed Lambda Calculus +;; - one arg lambda +;; - var +;; - binary app +;; - binary + +;; - integers + +(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))])) +\ No newline at end of file diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt @@ -0,0 +1,3 @@ +#lang racket/base + +;; general type checking utility functions +\ No newline at end of file