Context: Inspired by Lean's #guard commands, I'd like to implement "static unit tests" in Racket, where tests give the same interactive feedback as types.
Currently, what I'm doing is creating a sub-module using module*, then requiring the enclosing module at for-syntax time. But the enclosing module may not necessarily export the function in general (e.g. it may just be a helper). So what I'm doing is whenever the programmer writes (with-examples (name) _ ...), I generate a throwaway alias name* and provide it to the sub-module instead, which it renames back to name.
What I don't like about this approach is that there will be no arrow in DrRacket if I place the cursor on factorial in the sub-module.
My question: Is there a better way to do this in Racket, to provide only specifically to a sub-module, and not necessarily everyone?
The typical way for a submodule to require the "public interface" of its outer module would be something like (module* name (submod "..") ___).
#lang racket/base
(define public 42)
(define private 43)
(provide (all-from-out racket/base)
public)
(module* m (submod "..")
(println public)) ;works, but using `private` would be an error
Not only does this limit m to exports, it goes through any contracts that might be attached at the module boundary (sometimes you might care).
This approach avoids needing to make aliases. However it doesn't seem to help with the main thing you didn't like about your approach:
The arrows aren't better -- there's just an arrow from public to (submod "..").
I see thanks!! So even in the expanded code, the arrow points to the module. That's why in the macro one, there's no arrow pointing back to the original
One thing you might try is to generate binders and references that have the right syntax locations, but are in dead code. You could use the factorial that's written at the top of with-examples both in the enclosing module (as a reference) and in the newly created module (as a binder) to get at least some arrows. Check Syntax doesn't care if you use an identifier with the same source location in multiple different unrelated scopes. It does it's best with what it finds.
I tried to write an example to illustrate but ran into trouble with the submodule. Are you doing some kind of hygiene bending operations on the generated submodule?
Thanks Robby!! So actually I get two arrows now pointing to both binding positions, which is reasonable. I don't know how it happened and what I did differently
Unreasonable question: We don't need to do anything for a submodule defined by module* to access the enclosing module's definitions if it's in the same phase:
#lang racket/base
(define x 42)
(module* test #f
(println x))
Is it possible to have the submodule access the enclosing module during the submodule's for-syntax phase without explicitly providing/requiring anything?
(begin
(provide (rename-out [x x*])) ; so `x` isn't exposed to public in general
(module* anon #f
(require (for-syntax racket/base
(rename-in (submod "..") [x* x])))
(begin-for-syntax
(check-equal? x 42))))
I think the reason I finally get 2 arrows now (one pointing to the original x) is because I'm declaring #f instead of (submod "..") like I used to do. So as far as arrow is concerned, I'm good now
My possibly unreasonable question is, if it is possible to not have to explicitly provide/require private bindings from the enclosing module and have it available in the for-syntax phase of the submodule, something hypothetically like below ?
(module* anon (for-syntax #f) ; (not a thing)
(begin-for-syntax
(check-equal? x 42)))
I probably should rename with-examples to static-module+ or something to mirror module+. But a name starting with with naturally has the indentation I want
Oh! I thought you were asking for a change to check syntax that might make more arrows appear automatically without needing to make up binders and whatnot.
I'm revisiting this question, trying not to make users explicitly provide all the names to the sub-module, potentially giving up the arrows if that's infeasible.
The macro with-examples then would be used like this:
#lang racket/base
(define n 42)
(with-examples
(displayln n) ; prints 42 at compile time
)
It would expand to something like this:
#lang racket/base
(define n 42)
(module* all-defns #f
(provide (all-from-out (submod "..")))
(module* compile-time-exec #f
(require (for-syntax racket/base
(submod "..")))
(begin-for-syntax
(displayln n))))
; Still printing 42 at compile time
But at the moment, I don't know where to get the context to assign to the body ... of the macro, so that I can both preserve the original source locations (for precise error reporting), and get the bindings from (submod ".."):
(define-syntax-parser with-examples
[(with-examples body ...)
#:with racket/base (datum->syntax #'with-examples 'racket/base)
#'(module* all-defns #f
(provide (all-from-out (submod "..")))
(module* compile-time-exec #f
(require (for-syntax racket/base
(submod "..")))
(begin-for-syntax
body ... ; Won't see bindings from (submod "..")
)))])
(with-examples
(displayln n) ; ERROR: n undefined
)
How can I get body ... to see the bindings from the (submod ..) in the generated (module* compile-time-exec ...)?
The scope “on the parentheses” of the (submod "..") form is used for the imported bindings. This distinction is important so that the binding for submod still comes from the macro definition site, in case the usual binding isn't available at the use site.
I also changed to use this-syntax instead of binding and using #'with-examples: that would allow some other macro that would expand to with-examples to work like the (submod "..") case.
I'm not sure if there's a way to do this or not, and I've only skimmed the rest of this thread (so I'm likewise not getting into whether it should check syntax-local-context or syntax-local-lift-module-end-declaration or something to work multiple times).
But one thing to note is that (require (submod "..")) imports the identifiers exported by the parent module, potentially shadowing un-exported identifiers with the same names. The most common example is contracts:
?