define definitions recomputed on every call

[wilbowma]

I think this is because we implement define with a variable transformer instead of actually expanding to a variable de-reference. It surprised me in my attempt at a staged programming example. This has to do with how we implement normalization; we'd need a way to delta reduce variables at compile-time.

#lang cur

(require cur/stdlib/nat)
(require racket/trace)
(require cur/debug/syntax-trace)

(trace-define-syntax run
                     (lambda (stx)
                       (syntax-parse stx
                         [(_ expr)
                          (cur-normalize #'expr)])))

(define one (run (plus 1 0)))
one

Should print

> (run '(run (plus 1 0)))
<'(s z)
(s z)

But actually

> (run '(run (plus 1 0)))
<'(s z)
> (run '(run (plus 1 0)))
<'(s z)
'(s z)

and we see run executed on every call use of one.

[stchang]

Yes, it's a problem.

We can't get rid of the variable-transformer (because then ids wont have types), but define in coc.rkt should be using the expanded e. It doesnt right now as a workaround to the old stxprop + modules problem.

As a start, I've submitted #135, which fixes your problem, but breaks many tests, which I'm still working through.

(If your demo works ok with #135 then feel free to use it.)

[wilbowma]

Thanks! I just cut that part of the demo. I can do with out it.

[stchang]

dupe of #37 and #90?

[wilbowma]

I wouldn't say dupe, but it is related. #37 and #90 are dupes. I consider that related to implementing things like Coq's cbn and cbv tactics, which let the user control evaluation.

[wilbowma]

Partially addressed, but the issue is we need lazy (by-need) \delta-reduction, I think.