search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

Elimnators and lambda not resugared properly? #132

Open wilbowma opened 4 years ago

wilbowma commented 4 years ago 
#lang cur
(require
 (only-in cur [new-elim elim]))

(define-datatype Nat : Type
  (z : Nat)
  (s : (-> Nat Nat)))

(begin-for-syntax
  (displayln (cur-reflect
              (cur-expand
               #`(lambda (x : Nat)
                   (elim
                    x
                    (lambda (x : Nat) Nat)
                    z
                    (lambda (n : Nat) (IH : Nat) n)))))))

> #<syntax (λ (x) (elim-Nat x (λ (X10) Nat) (z) (λ (X1) (λ (X11) X1))))>
> #<syntax (λ (x) (elim-Nat x (λ (X1) Nat) (z) (λ (X1) (λ (X2) X1))))>
> 
> #<syntax (λ (x) (elim-Nat x (λ (X10) Nat) (z) (λ (X1) (λ (X11) X1))))>
> #<syntax (λ (x) (elim-Nat x (λ (X1) Nat) (z) (λ (X1) (λ (X2) X1))))>

I expected elim to resugar to elim, rather than elim-Nat. This isn't a huge deal. But also, the lambdas inside the elim ought to have type annotations. That one does reduce readability.

stchang commented 4 years ago

Yes, right now a term expanded from a general elim is indistinguishable from a type specific one.

Same with expanded lambda, it doesnt know if the original term had an annotation or not. A quick fix would be to just add more stx props. But a better way would be to have terms also implement the "type info" that types have (which includes a resugar method for each term).

We'd have to modify Turnstile to have define-typed-syntax do everything that define-type does which could be a substantial change though. I'll need to think about what the syntax of that new define-typed-syntax would look like though.