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

Fixing redex-lang to aid in debugging

Browse Source
This commit is contained in:
William J. Bowman 2016-01-17 17:28:57 -05:00
parent ceb2a1aefc
commit 09f47481ab
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 25 additions and 31 deletions

56
cur-lib/cur/curnel/redex-lang.rkt
View File

@ -189,35 +189,29 @@
reified-term) reified-term)
(define (datum->cur syn t) (define (datum->cur syn t)
(match t (let datum->cur ([t t])
[(list (quote term) e) (match t
(quasisyntax/loc [(list (quote term) e)
syn (quasisyntax/loc syn
(datum->cur syn e))] (datum->cur e))]
[(list (quote Unv) i) [(list (quote Unv) i)
(quasisyntax/loc (quasisyntax/loc syn
syn (Type #,i))]
(Type #,i))] [(list (quote Π) (list x (quote :) t) body)
[(list (quote Π) (list x (quote :) t) body) (quasisyntax/loc syn
(quasisyntax/loc (dep-forall (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
syn [(list (quote λ) (list x (quote :) t) body)
(dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))] (quasisyntax/loc syn
[(list (quote λ) (list x (quote :) t) body) (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
(quasisyntax/loc [(list (list (quote elim) t1) t2)
syn (quasisyntax/loc syn
(dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))] (dep-elim #,(datum->cur t1) #,(datum->cur t2)))]
[(list (list (quote elim) t1) t2) [(list e1 e2)
(quasisyntax/loc (quasisyntax/loc syn
syn (dep-app #,(datum->cur e1) #,(datum->cur e2)))]
(dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))] [_
[(list e1 e2) (quasisyntax/loc syn
(quasisyntax/loc #,(datum->syntax syn t))])))
syn
(dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
[_
(quasisyntax/loc
syn
#,(datum->syntax syn t))]))
(define (eval-cur syn) (define (eval-cur syn)
(term (reduce ,(delta) ,(subst-bindings (cur->datum syn))))) (term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
@ -422,8 +416,8 @@
(quasisyntax/loc syn (λ (x : t) e)))])) (quasisyntax/loc syn (λ (x : t) e)))]))
(define-syntax (dep-app syn) (define-syntax (dep-app syn)
(syntax-case syn () (syntax-parse syn
[(_ e1 e2) [(_ e1:expr e2:expr)
(syntax->curnel-syntax (syntax->curnel-syntax
(quasisyntax/loc syn (#%app e1 e2)))])) (quasisyntax/loc syn (#%app e1 e2)))]))