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

Merge branch 'issue-24'; closes #24

Browse Source
This commit is contained in:
William J. Bowman 2015-10-02 18:29:14 -04:00
commit e58d59d56b
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
2 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
curnel/redex-lang.rkt
View File

@ -121,12 +121,15 @@
[exprs (second (bind-subst))])
(bind-subst (list (cons x vars) (cons t exprs)))))
(define (subst-bindings t)
(term (subst-all ,t ,(first (bind-subst)) ,(second (bind-subst)))))
(define (type-infer/term t)
(let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,t t_0) t_0)])
(let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,(subst-bindings t) t_0) t_0)])
(and (pair? t) (car t))))
(define (type-check/term? e t)
(and (judgment-holds (type-check ,(sigma) ,(gamma) ,e ,t)) #t))
(and (judgment-holds (type-check ,(sigma) ,(gamma) ,(subst-bindings e) ,(subst-bindings t))) #t))
;; TODO: Blanket disarming is probably a bad idea.
(define orig-insp (variable-reference->module-declaration-inspector (#%variable-reference)))
@ -215,11 +218,12 @@
#,(datum->syntax syn t))]))
(define (eval-cur syn)
(term (reduce ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst))))))
(term (reduce ,(sigma) ,(subst-bindings (cur->datum syn)))))
(define (syntax->curnel-syntax syn)
(quasisyntax/loc
syn
;; TODO: this subst-all should be #,(subst-bindings (cur->datum syn)), but doesn't work
(term (reduce #,(sigma) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
;; Reflection tools
@ -232,7 +236,7 @@
(define (step/syn syn)
(datum->cur
syn
(term (step ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
(term (step ,(sigma) ,(subst-bindings (cur->datum syn))))))
;; Are these two terms equivalent in type-systems internal equational reasoning?
(define (cur-equal? e1 e2)

14
stdlib/prop.rkt
View File

@ -94,4 +94,16 @@
true
true
(refl Bool true))
z))
z)
(define (id (A : Type) (x : A)) x)
(check-equal?
((id (== True T T))
(refl True (run (id True T))))
(refl True T))
(check-equal?
((id (== True T T))
(refl True (id True T)))
(refl True T)))