search

wilbowma / cur

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

Printable data types #124

Open wilbowma opened 4 years ago

wilbowma commented 4 years ago

I want support for making numbers print like numbers. I can redefine #%datum to get numbers to read like numbers, but want vice versa. Some kind of interface to gen:printable?

stchang commented 4 years ago

gen:printable would work for runtime. During typechecking, we're printing stx objects, which do not work with gen:printable. That's why we have the generic type methods. Overloading the resugar-type method might work. Do you have an example in mind?

wilbowma commented 4 years ago

I'd probably want both. I'm working through my demo, and after I define #%datum for the naturals, I type 0 in the REPL and (z) get printed. This is .. okay. Might even be good most of the time. But I'd like to be able to make it print 0.

stchang commented 4 years ago

Ok, gen:print is fine for the repl. Though define-type currently doesnt let you get at the internal struct definition. We should probably open a separate ticket for Turnstile to do that.