On Sat, Apr 4, 2020 at 3:14 AM Olivier Binda <[email protected]> wrote:
> I guess that the restriction on id is this way so that we can do nice
> stuff with notations (mostly with numbers).
>
> For example, at some point, I plan to allow users to write 1283 and to
> have that (maybe in a preprocessing step) turned into (; ; ; 1 2 8 3 )
> because normal users will want to use numbers the way they are used to
>
I haven't quite got there yet, but I plan to do something like this in MM1.
Inside a math expression, you can use antiquotation (denoted by a prefix
comma) to interpolate a lisp expression, like $ 2 + 2 = ,(->string {2 + 2})
$ would call the ->string function on the result of evaluating {2+2},
resulting in "4" getting placed in the math expression. (Actually in this
case you would have to do a bit more to make it typecheck; you need to
prepend "c" to the string and then convert the string to an atom 'c4, and
return that.) The resulting expression, '(eq (add c2 c2) c4), is just as if
you had typed $ 2 + 2 = 4 $ to begin with.
That part works already today, but I want to extend this with a hook for
the to-expr function to allow "malformed" expressions which are not just
s-expressions of atoms but also include numbers and strings directly,
calling a user defined callback to convert the number into a term. That
way, you could write $ 2 + 2 = ,4 $ and the 4 would get elaborated into 'c4
by a user hook, and this would work just as well for larger terms and
computations like $ ,11111 * ,11111 = ,{11111 * 11111} $. Similarly, you
will be able to write $ ,"hello world" $ instead of the current much uglier
$ _h :' _e :' _l :' _l :' _o :' __ :' _w :' _o :' _r :' _l :' _d :' s0 $.
but now, I'll try to do something hard :
>>> - either replace the term for logical or with a definition (which means
>>> refactoring lots of proofs)
>>> - or replacing the co usage for +, with using a term (which probably
>>> means more refactoring)
>>>
>>
>> The MM0 pretty printer already knows how to print notations, so all you
>> would have to do is to add a notation for wo. But it would have to happen
>> between reading the incoming .mm file and producing the output, that is,
>> inside mm0-hs, so that is on me to some extent. It needs to somehow accept
>> configuration information to guide the process, and passing that by the
>> command line would be very clunky. The internal metamath parser already
>> knows how to read $j commands, so one option would be to add a new $j
>> command declaring the notation.
>>
>
> You hint that it could be done with mm0-hs. Ok.
> Still, I don't want to rely on that. I need to be able to do that myself,
> because Mephistolus needs it.
> So, I will only rely on mm0-hs to translate mm stuff into basic mm0-stuff
>
If you already have it parsed and ready to analyze, then it shouldn't be
too hard to add notations on your end, but you will have to write a pretty
printer for mm0 if you want to produce notation-upgraded mm0 files. This
isn't very hard though, especially if you don't worry about things like
proper indentation. You won't be able to acquire information about
notations through $j directives this way, unless you intend to also parse
the source .mm file (in which case you may as well write the mm->mm0
translator yourself), and the set.mm0 output file loses most metadata so
you will have to supply this in some other way, perhaps a configuration
file of your own devising.
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSt6o2yAzta4rvznwZFfqfUgKMQ1K%2B--X63rWQFeGJe8Tg%40mail.gmail.com.
