Fixed hygeine issues in define-language

* Now data gets properly defined!
* Export begin from redex-core.
* Added nat, needed by pltools.
This commit is contained in:
William J. Bowman 2015-01-23 01:09:06 -05:00
parent 69711620db
commit 0a5568b78c
3 changed files with 35 additions and 14 deletions

6
nat.rkt Normal file
View File

@ -0,0 +1,6 @@
#lang s-exp "redex-core.rkt"
(require "sugar.rkt")
(data nat : Type
(z : nat)
(s : (-> nat nat)))

View File

@ -1,6 +1,9 @@
#lang s-exp "redex-core.rkt" #lang s-exp "redex-core.rkt"
(require "sugar.rkt") (require "sugar.rkt" "nat.rkt")
(provide define-relation) ;; TODO: Can't export var, avar because technically these aren't
;; defined....
;; REALLY NEED TO FIX THAT
(provide define-relation define-language)
(begin-for-syntax (begin-for-syntax
(define-syntax-class dash (define-syntax-class dash
@ -33,10 +36,10 @@
(begin-for-syntax (begin-for-syntax
(require racket/syntax) (require racket/syntax)
(define (new-name . id*) (define (new-name name . id*)
(apply format-id #f (for/fold ([str "~a"]) (apply format-id name (for/fold ([str "~a"])
([_ (cdr id*)]) ([_ id*])
(string-append str "-~a")) (map syntax->datum id*))) (string-append str "-~a")) name (map syntax->datum id*)))
(define (fresh-name id) (define (fresh-name id)
(datum->syntax id (gensym (syntax->datum id))))) (datum->syntax id (gensym (syntax->datum id)))))
@ -122,6 +125,7 @@
(define-syntax (define-language syn) (define-syntax (define-language syn)
(syntax-parse syn (syntax-parse syn
#:literals (var)
[(_ name:id (~do (lang-name #'name)) [(_ name:id (~do (lang-name #'name))
(~do (nts (hash-set (make-immutable-hash) 'var #'var))) (~do (nts (hash-set (make-immutable-hash) 'var #'var)))
(~optional (~seq #:vars (x*:id ...) (~optional (~seq #:vars (x*:id ...)
@ -129,17 +133,27 @@
([v (syntax->datum #'(x* ...))]) ([v (syntax->datum #'(x* ...))])
(hash-set ht v (hash-ref ht 'var))))))) (hash-set ht v (hash-ref ht 'var)))))))
. clause*:nt-clauses) . clause*:nt-clauses)
(let ([var (hash-ref (nts) 'var)]) #`(begin . clause*.defs)]))
#`(begin
#,@(if (attribute x*)
#`((data #,var : Type (avar : (-> nat #,var))))
#'())
. clause*.defs))]))
; TODO: Not quite working yet. I think it has something to do with (data var : Type (avar : (-> nat var)))
; begin.
#|
(define-language stlc (define-language stlc
#:vars (x) #:vars (x)
(val (v) ::= true false) (val (v) ::= true false)
(type (A B) ::= bool (-> A B)) (type (A B) ::= bool (-> A B))
(term (e) ::= var v (e e) (lambda x A e))) (term (e) ::= var v (e e) (lambda x A e)))
(begin
(data stlc-val : Type
(stlc-true : stlc-val)
(stlc-false : stlc-val))
(data stlc-type : Type
(stlc-bool : stlc-type)
(stlc--> : (->* stlc-type stlc-type stlc-type)))
(data stlc-term : Type
(var-->-stlc-term : (-> var stlc-term))
(stlc-val-->-stlc-term : (-> stlc-val stlc-term))
(stlc-term2151 : (->* stlc-term stlc-term stlc-term))
(stlc-lambda : (->* var stlc-type stlc-term stlc-term))))
|#

View File

@ -616,6 +616,7 @@
provide provide
for-syntax for-syntax
module+ module+
begin
(rename-out (rename-out
[dep-lambda lambda] [dep-lambda lambda]
[dep-lambda λ] [dep-lambda λ]