suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

move define to stlc+var.rkt; cleanup

Browse Source
This commit is contained in:
Stephen Chang 2015-07-08 17:15:08 -04:00
parent dafa992176
commit 46598499d1
3 changed files with 24 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
tapl/stlc+box.rkt
View File

@ -1,9 +1,9 @@
#lang racket/base
(require "typecheck.rkt")
(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app λ))
(except-in "stlc+cons.rkt" #%app λ))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
(provide (except-out (all-from-out "stlc+cons.rkt") stlc:#%app stlc:λ))
(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app))
(except-in "stlc+cons.rkt" #%app))
(provide (rename-out [stlc:#%app #%app]))
(provide (except-out (all-from-out "stlc+cons.rkt") stlc:#%app))
(provide ref deref :=)
;; Simply-Typed Lambda Calculus, plus mutable references

20
tapl/stlc+cons.rkt
View File

@ -1,10 +1,9 @@
#lang racket/base
(require "typecheck.rkt")
(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app λ let begin))
(except-in "stlc+var.rkt" #%app λ let begin))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let] [stlc:begin begin]
[cons/tc cons] [define/tc define]))
(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app stlc:λ stlc:let stlc:begin))
(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app))
(except-in "stlc+var.rkt" #%app))
(provide (rename-out [stlc:#%app #%app] [cons/tc cons]))
(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app))
(provide nil isnil head tail)
;; Simply-Typed Lambda Calculus, plus cons
@ -13,20 +12,9 @@
;; - List constructor
;; Terms:
;; - terms from stlc+var.rkt
;; - define, constants only
;; TODO: enable HO use of list primitives
;; constants only
(define-syntax (define/tc stx)
(syntax-parse stx
[(_ x:id e)
#:with (e- τ) (infer+erase #'e)
#:with y (generate-temporary)
#'(begin
(define-syntax x (make-rename-transformer (⊢ #'y #'τ)))
(define y e-))]))
(define-type-constructor List #:arity 1)
(define-syntax (nil stx)

21
tapl/stlc+var.rkt
View File

@ -1,10 +1,11 @@
#lang racket/base
(require "typecheck.rkt")
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?))
(except-in "stlc+tup.rkt" #%app λ tup proj let type=?))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?))
(except-in "stlc+tup.rkt" #%app begin tup proj let type=?))
(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
[define/tc define]))
(provide (except-out (all-from-out "stlc+tup.rkt")
stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj
stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
(for-syntax stlc:type=?)))
(provide tup proj var case)
(provide (for-syntax type=?))
@ -22,6 +23,8 @@
;; - terms from stlc+tup.rkt
;; - extend tup to include records
;; - sums (var)
;; TopLevel:
;; - define (values only)
(begin-for-syntax
; extend to:
@ -88,4 +91,12 @@
(⊢ #'(let ([l_e (car e-)])
(cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
(stx-car #'(τ_el ...)))]))
(define-syntax (define/tc stx)
(syntax-parse stx
[(_ x:id e)
#:with (e- τ) (infer+erase #'e)
#:with y (generate-temporary)
#'(begin
(define-syntax x (make-rename-transformer (⊢ #'y #'τ)))
(define y e-))]))