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

Massive clean up of Redex core

Browse Source 
* Renamed languages and reorganized languages
* Various fixes to fresh name generating
* Fixed to testing infrastructure; now tests modulo equivelance
* Renamed and reorganized many metafunctions, particularly those to do
  with Σ and Γ
* Reorganized sections of code to improve readability and reduce
  dependencies
* Reimplemented eliminator typing and reduction
* Various stylistic changes
This commit is contained in:
William J. Bowman 2015-09-30 16:16:03 -04:00
parent a3c3b0fca7
commit 04405758ff
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
2 changed files with 590 additions and 517 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1096
curnel/redex-core.rkt
View File

File diff suppressed because it is too large Load Diff

11
curnel/redex-lang.rkt
View File

@ -11,7 +11,7 @@
racket/syntax racket/syntax
(except-in racket/provide-transform export) (except-in racket/provide-transform export)
racket/require-transform racket/require-transform
(except-in "redex-core.rkt" remove) "redex-core.rkt"
redex/reduction-semantics)) redex/reduction-semantics))
(provide (provide
;; Basic syntax ;; Basic syntax
@ -86,6 +86,7 @@
(error 'core-error "We built a bad sigma ~s" x)) (error 'core-error "We built a bad sigma ~s" x))
x))) x)))
;; These should be provided by core, so details of envs can be hidden.
(define (extend-Γ/term env x t) (define (extend-Γ/term env x t)
(term (,(env) ,x : ,t))) (term (,(env) ,x : ,t)))
@ -269,8 +270,8 @@
(define (cur-identifier-bound? id) (define (cur-identifier-bound? id)
(let ([x (syntax->datum id)]) (let ([x (syntax->datum id)])
(and (x? x) (and (x? x)
(or (term (lookup-Γ ,(gamma) ,x)) (or (term (Γ-ref ,(gamma) ,x))
(term (lookup-Σ ,(sigma) ,x)))))) (term (Σ-ref-type ,(sigma) ,x))))))
(define (filter-cur-exports syn modes) (define (filter-cur-exports syn modes)
(partition (compose cur-identifier-bound? export-local-id) (partition (compose cur-identifier-bound? export-local-id)
@ -336,7 +337,7 @@
;; TODO: Do not DIY gensym ;; TODO: Do not DIY gensym
(set! gn (add1 gn)) (set! gn (add1 gn))
(set! out-gammas (set! out-gammas
#`(#,@out-gammas (gamma (term (append-Γ #`(#,@out-gammas (gamma (term (Γ-union
,(gamma) ,(gamma)
,#,new-id))))) ,#,new-id)))))
(cons (struct-copy import imp [local-id new-id]) (cons (struct-copy import imp [local-id new-id])
@ -349,7 +350,7 @@
;; TODO: Do not DIY gensym ;; TODO: Do not DIY gensym
(set! sn (add1 sn)) (set! sn (add1 sn))
(set! out-sigmas (set! out-sigmas
#`(#,@out-sigmas (sigma (term (append-Σ #`(#,@out-sigmas (sigma (term (Σ-union
,(sigma) ,(sigma)
,#,new-id))))) ,#,new-id)))))
(cons (struct-copy import imp [local-id new-id]) (cons (struct-copy import imp [local-id new-id])