commit 27d7f33b4a62da0193ba682fcecb5f41c591a899
parent 2d2d278b8e7e91171d8d64fdc2db198d1ee028ae
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 26 Aug 2014 16:53:48 -0400
add parallel implementation what uses racket-extended instead of racket
- currently stlc (core) only
Diffstat:
3 files changed, 171 insertions(+), 0 deletions(-)
diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
@@ -0,0 +1,133 @@
+#lang racket/base
+(require
+ (for-syntax
+ racket/base syntax/parse syntax/parse/experimental/template
+ racket/syntax syntax/stx
+ "stx-utils.rkt")
+ (for-meta 2 racket/base syntax/parse))
+(require "typecheck.rkt")
+(provide (except-out (all-from-out racket/base) #%module-begin))
+
+;; Extension of Racket for implementing typed languages
+
+(provide define-term/type-rule
+ declare-built-in-type declare-built-in-types)
+(provide (rename-out [mb/ext #%module-begin]))
+;; provide syntax-classes
+(provide (for-syntax integer str))
+
+;; lit-set : [Listof identifier]
+(define-for-syntax lit-set null)
+(define-syntax (declare-built-in-type stx)
+ (syntax-parse stx
+ [(_ τ)
+ (set! lit-set (cons #'τ lit-set))
+ #'(begin (define τ #f) (provide τ))]))
+(define-syntax-rule (declare-built-in-types τ ...)
+ (begin (declare-built-in-type τ) ...))
+
+(begin-for-syntax
+ ;; concrete-τ? : determines if a type is a concrete type or has pattern vars
+ ;; result is used to determine whether to insert ellipses in the output pattern
+ (define (concrete-τ? τ)
+ (or (and (identifier? τ) (member τ lit-set free-identifier=?))
+ (and (not (identifier? τ)) (stx-andmap concrete-τ? τ))))
+ (define-syntax-class type
+ (pattern any))
+ ;; meta-term is the term pattern in meta-language
+ ;; (ie where the type rules are declared)
+ ;; - matches type vars
+ (define-syntax-class meta-term #:datum-literals (:)
+ (pattern (name:id ([x:id : τ] ... (~optional (~and ldots (~literal ...)))) e ...)
+ #:attr args/notypes (template ((x ... (?? ldots)) e ...))
+ #:attr typevars (template (τ ... (?? ldots))))
+ (pattern (name:id e ...)
+ #:attr args/notypes #'(e ...)
+ #:attr typevars #'())
+ #;(pattern (name:id . n)
+ #:attr args/notypes #'n
+ #:attr typevars #'()))
+ ;; term matches concrete terms in the actual (typed) language
+ ;; - matches concrete types
+ ;; name identifier is the extended form
+ (define-syntax-class term
+ (pattern (name:id ([x:id : τ] ...) e ...)
+ #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
+ (expand/df #'(λ (x ...) e ...)))
+ ;; identifiers didnt get a type bc racket has no %#var form
+ #:with es++ (with-extended-type-env #'([x τ] ...)
+ (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+ #:attr expanded-args #'(xs+ . es++)
+ #:attr types #'(τ ...))
+ (pattern (name:id e ...)
+ #:with (e+ ...) (stx-map expand/df #'(e ...))
+ #:attr expanded-args #'(e+ ...)
+ #:attr types #'())
+ #;(pattern (name:id . n)
+ #:attr expanded-args #'n
+ #:attr types #'()))
+ (define-splicing-syntax-class τ-constraint #:datum-literals (:= : let typeof)
+ (pattern (let τ := (typeof e))
+ #:attr pattern-directive #'(#:with τ (typeof #'e)))
+ (pattern (e : τ)
+ #:attr pattern-directive #'(#:when (assert-type #'e #'τ)))
+ (pattern (~seq (e0 : τ0) (~literal ...))
+ #:when (concrete-τ? #'τ0)
+ #:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 (... ...)))))
+ ;; not concrete-τ
+ (pattern (~seq (e0 : τ0) (~literal ...))
+ #:attr pattern-directive #'(#:when (stx-andmap assert-type #'(e0 (... ...)) #'(τ0 (... ...)))))))
+
+
+
+;; define-term/type-rule
+(define-syntax (define-term/type-rule stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ meta-e:meta-term : meta-τ
+ (~optional (~seq #:where
+ c:τ-constraint ...)))
+ #:with fresh-name (generate-temporary #'meta-e.name)
+ #:with lits lit-set
+ (template
+ (begin
+ (provide (rename-out [fresh-name meta-e.name]))
+ (define-syntax (fresh-name stx)
+ (syntax-parse stx #:literals lits
+ [e:term
+ ;; shadow pattern vars representing subterms with its expansion
+ ;; - except for the name of the form, since result must use base form
+ #:with meta-e.args/notypes #'e.expanded-args
+ #:with meta-e.typevars #'e.types
+ (?? (?@ . ((?@ . c.pattern-directive) ...)))
+ (⊢ (syntax/loc stx (meta-e.name . meta-e.args/notypes)) #'meta-τ)]
+ [_ #:when (type-error #:src stx #:msg "type error") #'(void)]
+ ))))]))
+
+;; overload mod-begin to check for define-literal-type-rule
+(begin-for-syntax
+ (define-syntax-class def #:datum-literals (define-literal-type-rule)
+ (pattern (define-literal-type-rule stx-class : τ)
+ #:attr other #'()
+ #:attr stxc #'(stx-class)
+ #:attr lit-τ #'(τ))
+ (pattern any #:attr other #'(any) #:attr stxc #'() #:attr lit-τ #'())))
+
+(define-syntax (mb/ext stx)
+ (syntax-parse stx
+ [(_ d:def ...)
+ #:with (stxc ...) (template ((?@ . d.stxc) ...))
+ #:with (lit-τ ...) (template ((?@ . d.lit-τ) ...))
+ #:with my-datum (generate-temporary)
+ #:with datum-def
+ #'(define-syntax (my-datum stx)
+ (syntax-parse stx
+ [(_ . x) #:declare x stxc (⊢ (syntax/loc stx (#%datum . x)) #'lit-τ)]
+ ...
+ [(_ . x)
+ #:when (type-error #:src stx #:msg "Don't know the type for literal: ~a" #'x)
+ stx]))
+ (template
+ (#%module-begin
+ (provide (rename-out [my-datum #%datum]))
+ datum-def
+ (?@ . d.other) ...))]))
+\ No newline at end of file
diff --git a/stlc-test.rkt b/stlc-test.rkt
@@ -0,0 +1,5 @@
+#lang s-exp "stlc-via-racket-extended.rkt"
+((λ ([f : (Int → Int)] [x : Int]) (f x))
+ (λ ([x : Int]) (+ x x 2))
+ 10)
+((λ ([x : Int]) (+ x 1 3)) 100)
+\ No newline at end of file
diff --git a/stlc-via-racket-extended.rkt b/stlc-via-racket-extended.rkt
@@ -0,0 +1,31 @@
+#lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
+(provide #%top-interaction)
+(require (prefix-in r: racket/base))
+(provide (rename-out [r:#%module-begin #%module-begin]))
+
+;; Simply-Typed Lambda Calculus
+;; - implemented with racket-extended language
+;; - lam, app, and var only
+
+(declare-built-in-types → Int)
+
+;; typed forms ----------------------------------------------------------------
+
+(define-literal-type-rule integer : Int)
+(define-literal-type-rule str : String)
+
+(define-term/type-rule
+ (+ e ...) : Int
+ #:where
+ (e : Int) ...)
+
+(define-term/type-rule
+ (λ ([x : τ] ...) e) : (τ ... → τ_body)
+ #:where
+ (let τ_body := (typeof e)))
+
+(define-term/type-rule
+ (#%app f e ...) : τ2
+ #:where
+ (let (τ1 ... → τ2) := (typeof f))
+ (e : τ1) ...)
