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