diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt
index 34dbcd7..36ce469 100644
--- a/cur-lib/cur/curnel/redex-lang.rkt
+++ b/cur-lib/cur/curnel/redex-lang.rkt
@@ -2,7 +2,7 @@
;; This module just provide module language sugar over the redex model.
(require
- "redex-core.rkt"
+ (except-in "redex-core.rkt" apply)
redex/reduction-semantics
racket/provide-syntax
(for-syntax
@@ -11,7 +11,7 @@
racket/syntax
(except-in racket/provide-transform export)
racket/require-transform
- "redex-core.rkt"
+ (except-in "redex-core.rkt" apply)
redex/reduction-semantics))
(provide
;; Basic syntax
@@ -177,10 +177,11 @@
[e (parameterize ([gamma (extend-Γ/term gamma x t)])
(cur->datum #'e))])
(term (,(syntax->datum #'b) (,x : ,t) ,e)))]
- [(elim t1 t2)
- (let* ([t1 (cur->datum #'t1)]
- [t2 (cur->datum #'t2)])
- (term (elim ,t1 ,t2)))]
+ [(elim D motive (i ...) (m ...) d)
+ (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
+ ,(map cur->datum (syntax->list #'(i ...)))
+ ,(map cur->datum (syntax->list #'(m ...)))
+ ,(cur->datum #'d)))]
[(#%app e1 e2)
(term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
(unless (or (inner-expand?) (type-infer/term reified-term))
@@ -446,9 +447,9 @@
(define-syntax (dep-elim syn)
(syntax-parse syn
- [(_ D:id T)
+ [(_ D:id motive (i ...) (m ...) e)
(syntax->curnel-syntax
- (quasisyntax/loc syn (elim D T)))]))
+ (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
(define-syntax-rule (dep-void) (void))
diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index ff4fe25..5db151b 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -95,8 +95,18 @@
(cur->coq #'t))]))))
"")]
[(Type i) "Type"]
- [(real-elim var t)
- (format "~a_rect" (cur->coq #'var))]
+ [(real-elim var:id motive (i ...) (m ...) d)
+ (format
+ "(~a_rect ~a~a~a ~a)"
+ (cur->coq #'var)
+ (cur->coq #'motive)
+ (for/fold ([strs ""])
+ ([m (syntax->list #'(m ...))])
+ (format "~a ~a" strs (cur->coq m)))
+ (for/fold ([strs ""])
+ ([i (syntax->list #'(i ...))])
+ (format "~a ~a" strs (cur->coq i)))
+ (cur->coq #'d))]
[(real-app e1 e2)
(format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
diff --git a/cur-lib/cur/stdlib/prop.rkt b/cur-lib/cur/stdlib/prop.rkt
index a61bc52..3c3a191 100644
--- a/cur-lib/cur/stdlib/prop.rkt
+++ b/cur-lib/cur/stdlib/prop.rkt
@@ -71,11 +71,12 @@
(define proof:A-or-A
(lambda (A : Type) (c : (Or A A))
;; TODO: What should the motive be?
- (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
- (lambda (A : Type) (B : Type) (a : A) a)
- ;; TODO: How do we know B is A?
- (lambda (A : Type) (B : Type) (b : B) b)
- A A c)))
+ (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+ (A A)
+ ((lambda (A : Type) (B : Type) (a : A) a)
+ ;; TODO: How do we know B is A?
+ (lambda (A : Type) (B : Type) (b : B) b))
+ c)))
(qed thm:A-or-A proof:A-or-A)
|#
diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
index 71654b5..fb7ba99 100644
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -12,7 +12,6 @@
#%app
define
:
- elim
define-type
match
recur
@@ -29,7 +28,6 @@
(require
(only-in "../main.rkt"
- [elim real-elim]
[#%app real-app]
[λ real-lambda]
[Π real-Π]
@@ -163,8 +161,67 @@
(quasisyntax/loc syn
(real-define id body))]))
-(define-syntax-rule (elim t1 t2 e ...)
- ((real-elim t1 t2) e ...))
+#|
+(begin-for-syntax
+ (define (type->telescope syn)
+ (syntax-parse (cur-expand syn)
+ #:literals (real-Π)
+ #:datum-literals (:)
+ [(real-Π (x:id : t) body)
+ (cons #'(x : t) (type->telescope #'body))]
+ [_ '()]))
+
+ (define (type->body syn)
+ (syntax-parse syn
+ #:literals (real-Π)
+ #:datum-literals (:)
+ [(real-Π (x:id : t) body)
+ (type->body #'body)]
+ [e #'e]))
+
+ (define (constructor-indices D syn)
+ (let loop ([syn syn]
+ [args '()])
+ (syntax-parse (cur-expand syn)
+ #:literals (real-app)
+ [D:id args]
+ [(real-app e1 e2)
+ (loop #'e1 (cons #'e2 args))])))
+
+ (define (inductive-index-telescope D)
+ (type->telescope (cur-type-infer D)))
+
+ (define (inductive-method-telescope D motive)
+ (for/list ([syn (cur-constructor-map D)])
+ (with-syntax ([(c : t) syn]
+ [name (gensym (format-symbol "~a-~a" #'c 'method))]
+ [((arg : arg-type) ...) (type->telescope #'t)]
+ [((rarg : rarg-type) ...) (constructor-recursive-args D #'((arg : arg-type) ...))]
+ [((ih : ih-type) ...) (constructor-inductive-hypotheses #'((rarg : rarg-type) ...) motive)]
+ [(iarg ...) (constructor-indices D (type->body #'t))]
+ )
+ #`(name : (forall (arg : arg-type) ...
+ (ih : ih-type) ...
+ (motive iarg ...)))))))
+
+(define-syntax (elim syn)
+ (syntax-parse syn
+ [(elim D:id U e ...)
+ (with-syntax ([((x : t) ...) (inductive-index-telescope #'D)]
+ [motive (gensym 'motive)]
+ [y (gensym 'y)]
+ [disc (gensym 'disc)]
+ [((method : method-type) ...) (inductive-method-telescope #'D #'motive)])
+ #`((lambda
+ (motive : (forall (x : t) ... (y : (D x ...)) U))
+ (method : ) ...
+ (x : t) ...
+ (disc : (D x ...)) ...
+ (real-elim D motive (x ...) (method ...) disc))
+ e ...)
+ )
+ ]))
+|#
;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
(begin-for-syntax
@@ -366,15 +423,9 @@
(quasisyntax/loc syn
(elim
D.inductive-name
- #,(or
- (cur-type-infer (attribute return-type))
- (raise-syntax-error
- 'match
- "Could not infer type of motive. Sorry, you'll have to use elim."
- syn))
motive
- c.method ...
- #,@(attribute D.indices)
+ #,(attribute D.indices)
+ (c.method ...)
d))]))
(begin-for-syntax
diff --git a/cur-lib/info.rkt b/cur-lib/info.rkt
index 916ccf0..0369661 100644
--- a/cur-lib/info.rkt
+++ b/cur-lib/info.rkt
@@ -3,5 +3,5 @@
(define deps '("base" ("redex-lib" #:version "1.11")))
(define build-deps '())
(define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
-(define version "0.3")
+(define version "0.4")
(define pkg-authors '(wilbowma))
diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt
index a2cda7b..e40c5cd 100644
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@@ -41,11 +41,12 @@
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n"))))
(let ([t (cur->coq
- #'(elim nat Type (lambda (x : nat) nat) z
- (lambda (x : nat) (ih-x : nat) ih-x)
+ #'(elim nat (lambda (x : nat) nat)
+ ()
+ (z (lambda (x : nat) (ih-x : nat) ih-x))
e))])
(check-regexp-match
- "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+ "\\(nat_rect \\(fun x : nat => nat\\) z \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\) e\\)"
t))
(check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
diff --git a/cur-test/cur/tests/stdlib/list.rkt b/cur-test/cur/tests/stdlib/list.rkt
index afda5a8..f560ece 100644
--- a/cur-test/cur/tests/stdlib/list.rkt
+++ b/cur-test/cur/tests/stdlib/list.rkt
@@ -32,11 +32,11 @@
(:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
(check-equal?
(void)
- (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
- (lambda (A : Type) z)
- (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
- z)
- Bool
+ (:: (elim List (lambda (A : Type) (ls : (List A)) Nat)
+ (Bool)
+ ((lambda (A : Type) z)
+ (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
+ z))
(nil Bool))
Nat))
diff --git a/cur-test/cur/tests/stdlib/prop.rkt b/cur-test/cur/tests/stdlib/prop.rkt
index ec90b0c..0d8222e 100644
--- a/cur-test/cur/tests/stdlib/prop.rkt
+++ b/cur-test/cur/tests/stdlib/prop.rkt
@@ -11,11 +11,11 @@
(:: pf:proj1 thm:proj1)
(:: pf:proj2 thm:proj2)
(check-equal?
- (elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
- (λ (A : Type) (x : A) z)
- Bool
- true
- true
+ (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+ (Bool
+ true
+ true)
+ ((λ (A : Type) (x : A) z))
(refl Bool true))
z)
diff --git a/cur-test/cur/tests/stdlib/typeclass.rkt b/cur-test/cur/tests/stdlib/typeclass.rkt
index 9f6ce6c..fb8bb27 100644
--- a/cur-test/cur/tests/stdlib/typeclass.rkt
+++ b/cur-test/cur/tests/stdlib/typeclass.rkt
@@ -11,9 +11,7 @@
(equal? : (forall (a : A) (b : A) Bool)))
(impl (Eqv Bool)
(define (equal? (a : Bool) (b : Bool))
- (if a
- (if b true false)
- (if b false true))))
+ (if a b (not b))))
(impl (Eqv Nat)
(define equal? nat-equal?))
(check-equal?
diff --git a/cur-test/info.rkt b/cur-test/info.rkt
index 37c408b..bc46632 100644
--- a/cur-test/info.rkt
+++ b/cur-test/info.rkt
@@ -1,7 +1,7 @@
#lang info
(define collection 'multi)
(define deps '())
-(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2") "sweet-exp"))
+(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.4") "sweet-exp"))
(define update-implies '("cur-lib"))
(define pkg-desc "Tests for \"cur\".")
(define pkg-authors '(wilbowma))