From 69c97a55124d618c9c3b4607c49cba6b524dc05a Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 11 Nov 2014 18:21:43 -0500 Subject: [PATCH] start tapl/ dir --- tapl/stlc-tests.rkt | 1 + tapl/stlc.rkt | 17 +++++++++++++++++ tapl/typecheck.rkt | 3 +++ 3 files changed, 21 insertions(+) create mode 100644 tapl/stlc-tests.rkt create mode 100644 tapl/stlc.rkt create mode 100644 tapl/typecheck.rkt diff --git a/tapl/stlc-tests.rkt b/tapl/stlc-tests.rkt new file mode 100644 index 0000000..5bc0523 --- /dev/null +++ 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 new file mode 100644 index 0000000..0797d60 --- /dev/null +++ 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 new file mode 100644 index 0000000..832066e --- /dev/null +++ b/tapl/typecheck.rkt @@ -0,0 +1,3 @@ +#lang racket/base + +;; general type checking utility functions \ No newline at end of file