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

Removed implementation of case & case*

Browse Source
This commit is contained in:
William J. Bowman 2016-01-18 14:03:33 -05:00
parent 2fcba80950
commit c3f5719b30
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 0 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
cur-lib/cur/stdlib/sugar.rkt
View File

@ -120,35 +120,6 @@
(define-syntax-rule (elim t1 t2 e ...) (define-syntax-rule (elim t1 t2 e ...)
((real-elim t1 t2) e ...)) ((real-elim t1 t2) e ...))
(begin-for-syntax
(define (rewrite-clause clause)
(syntax-case clause (: IH:)
[((con (a : A) ...) IH: ((x : t) ...) body)
#'(lambda (a : A) ... (x : t) ... body)]
[(e body) #'body])))
;; TODO: Expects clauses in same order as constructors as specified when
;; TODO: inductive D is defined.
;; TODO: Assumes D has no parameters
(define-syntax (case syn)
;; duplicated code
(define (clause-body syn)
(syntax-case (car (syntax->list syn)) (: IH:)
[((con (a : A) ...) IH: ((x : t) ...) body) #'body]
[(e body) #'body]))
(syntax-case syn (=>)
[(_ e clause* ...)
(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* ...)))
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)]))
;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive" ;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
(begin-for-syntax (begin-for-syntax
(define ih-dict (make-hash)) (define ih-dict (make-hash))