support more atomic rewriting

[pnwamk]

make it easy to rewrite other atoms in redex models (e.g. a language might want to use #t and #f because it is convenient, but render them as true and false or similar)

[pnwamk]

NOTE: these changes haven't been tested yet (although they seem relatively simple/harmless).

[pnwamk]

This doesn't seem to work - I don't think the rewriting code is called on non-symbols at the moment. More digging required!

[rfindler]

Yes, that won't work, I believe.

[pnwamk]

Okay, the approach I think is now more-or-less correct. i.e. to rewrite a non-symbol atom, you have to rewrite its string representation.

I've tested this manually but haven't added anything to the test suite.

[rfindler]

Why not just change redex to have rewriters for non-symbol atoms?

[pnwamk]

Okay, now this PR let's users provide a rewriter for any reasonable redex-recognized literal value (i.e. a symbol, string, number, or boolean) and internally redex will worry about which symbol or string(s) to watch out for within the implementation when deciding when to apply the rewriters (since internally everything is represented as strings by the time the rewriters get to them).

This seems to work okay in a few simple hand tests I've done:

#lang racket/base
(require redex)

(define-language L
  (b ::= 1 0)
  (n ::= natural)
  [blah ::= #true #false 42 43 "hi" "hello"])

(with-atomic-rewriters
    ([#t "truthy"]
     [42 "forty-two"]
     ["hi" "high"])
  (render-language L))

produces

[rfindler]

Ok, I had a look at the code now. The to-lw is the one doing the conversion from various atoms to their string form. So there is no way to do rewriting based on the original datum at this layer. And if we change how to-lw works, well, it would be backward incompatible, but also I think that it would not be desirable, as that code is doing things like trying to figure out if the original input was #true or #t for example.

So now I think I'm going to backtrack a bit here (sorry!) and say that I think it makes sense to include a rewriter for things that are already stringified and not separate out the rewriters based on a guess on what the original datum was. Lets just consider that information gone.

I'm thinking of something where we can add another class of atomic rewriters that is called on things that are already stringified. I'm of two minds on whether it should be called on the string tokens that are the parens. Maybe it should optionally be called on them.

Also, this change is definitely one that warrants a change to bitmap-test.rkt.

[pnwamk]

Okay. Thanks for the detailed comments! I'll probably come back to this sometime next week and try to see how to tweak things to make it more in line with your most recent comments.

[rfindler]

Thanks!

[pnwamk]

Oh and when you have sec, if you did not see most recent edits if you could glance at them (commit 2b9af0c43adfd27e28bae4455c5207b4e4a392ac) and comment on if that approach is close to what you are describing when you say a "rewriter for things that are already stringified". In that most recent approach I tried to completely abstract away from the user redex's internal stringifying and just let them specify the literal values (and then we internally worry about how we might have stringified those values).

Sorry for the mess -- the edits have probably been difficult or impossible to follow (I force pushed since I radically changed what I was doing).

[rfindler]

I looked at that code. I am thinking that a single rewriter, applied to all string values (or something like the current atomic rewriters where the strings are specified outside) is the way to go. Then we might want to add some convenience things like that rw functions that you mentioned from the unstable library to easily and conveniently drop in common ones. But that stuff probably doesn't need to be in the guts of the pict construction stuff.

[rfindler]

@pnwamk do you still have interest in this? If so, I can try implementing the approach I outlined above (I have to say I have no memory of any of this, however!)

[pnwamk]

I don't have time I would plan to spend on implementing or trying this in the near future, no. If it's convenient to close this PR for now and/or indefinitely I won't be offended in the slightest :+1:

[rfindler]

If it existed, would you use it?

[pnwamk]

I don't have any immediate needs I would use it for, but in the longer term I could easily see using it, yes. I personally liked the idea of added flexibility between what's rendered and what's used under the hood to actually implement the redex model, and redex still holds a sweet spot in my mind for "runnable math".