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

Restricted elim curnel syntax

Browse Source 
The curnel was documented as having a restricted syntax, but this was
not actually enforced. Now it is.
This commit is contained in:
William J. Bowman 2015-09-25 17:50:27 -04:00
parent b64d20319f
commit 9681fbd9e0
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
3 changed files with 12 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
curnel/redex-lang.rkt
View File

@ -174,14 +174,10 @@
[e (parameterize ([gamma (extend-Γ/term gamma x t)])
(cur->datum #'e))])
(term (,(syntax->datum #'b) (,x : ,t) ,e)))]
[(elim t e P m ...)
(let* ([t (cur->datum #'t)]
[e (cur->datum #'e)]
[P (cur->datum #'P)]
[e (term (((elim ,t) ,e) ,P))])
(for/fold ([e e])
([m (syntax->list #'(m ...))])
(term (,e ,(cur->datum m)))))]
[(elim t1 t2)
(let* ([t1 (cur->datum #'t1)]
[t2 (cur->datum #'t2)])
(term ((elim ,t1) ,t2)))]
[(#%app e1 e2)
(term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
(unless (and inner-expand? (type-infer/term reified-term))
@ -414,10 +410,10 @@
#'(void))]))
(define-syntax (dep-elim syn)
(syntax-case syn (:)
[(_ D e P method ...)
(syntax-case syn ()
[(_ D T)
(syntax->curnel-syntax
(quasisyntax/loc syn (elim D e P method ...)))]))
(quasisyntax/loc syn (elim D T)))]))
;; TODO: Not sure if this is the correct behavior for #%top
(define-syntax (dep-top syn)

6
stdlib/nat.rkt
View File

@ -33,12 +33,12 @@
;; Credit to this function goes to Max
(define nat-equal?
(elim Nat Type (lambda (x : Nat) (-> Nat Bool))
(elim Nat Type (lambda (x : Nat) Bool)
((elim Nat Type) (lambda (x : Nat) (-> Nat Bool))
((elim Nat Type) (lambda (x : Nat) Bool)
true
(lambda* (x : Nat) (ih-n2 : Bool) false))
(lambda* (x : Nat) (ih : (-> Nat Bool))
(elim Nat Type (lambda (x : Nat) Bool)
((elim Nat Type) (lambda (x : Nat) Bool)
false
(lambda* (x : Nat) (ih-bla : Bool)
(ih x))))))

4
stdlib/sugar.rkt
View File

@ -88,13 +88,13 @@
(let* ([D (type-infer/syn #'e)]
[M (type-infer/syn (clause-body #'(clause* ...)))]
[U (type-infer/syn M)])
#`(elim #,D U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
#`((elim #,D #,U) (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
e))]))
(define-syntax (case* syn)
(syntax-case syn ()
[(_ D U e (p ...) P clause* ...)
#`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
#`((elim D U) P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
(define-syntax-rule (define-theorem name prop)
(define name prop))