search

Barnard-PL-Labs / tsltools

Library and tools for the TSL specification format
Other
7 stars 4 forks source link

fix preprocess real encoding bug (issue 41) #42

Closed leoqiao18 closed 2 years ago

leoqiao18 commented 2 years ago

Fix issue #41 .

The preprocessor uses read and show to process and encode real/float, which causes the encoding to be wrong. For example, a real like 0.01 gets turned into 1.0e-2. Therefore, the encoding after the preprocessing becomes real1.0e-2(), which becomes invalid syntax for TSL synthesis.

Instead of storing Int and Float in the Value ADT, just store the string representations.

leoqiao18 commented 2 years ago

@santolucito The reason was that reading a string to a float would lose precision in a lot of cases, and become impossible to write a show function that recovers the same decimal string representation.

If we still want an internal type representation, maybe we can store both the string and the float (i.e. TSLReal String Float), so that we have the original string to be used in encoding and the float to be used as the internal representation.

santolucito commented 2 years ago

But if we lose any precision (I'm not really sure when this would happen anyway), then that lost precision value would be what we use the TSL-MT computation anyway. Although we only need the string for the preprocessor, we're going to be using the Float representation for any modulo theories reasoning. Certainly having two representations seems too complicated as well. @wonhyukchoi can you chime in on how this change would impact TSL-MT downstream?

On Thu, Nov 3, 2022, 8:04 PM Leo Qiao @.***> wrote:

@santolucito https://github.com/santolucito The reason was that reading a string to a float would lose precision in a lot of cases, and become impossible to write a show function that recovers the same decimal string representation.

If we still want an internal type representation, maybe we can store both the string and the float (i.e. TSLReal String Float), so that we have the original string to be used in encoding and the float to be used as the internal representation.

— Reply to this email directly, view it on GitHub https://github.com/Barnard-PL-Labs/tsltools/pull/42#issuecomment-1302807592, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIJAPFS3TFGBVVBDFHAORTWGRHHVANCNFSM6AAAAAARWUILZ4 . You are receiving this because you were mentioned.Message ID: @.***>

santolucito commented 2 years ago

Actually, maybe this value only stays within the preprocessor, in which case I would agree it makes sense to just keep it as a String. Wonhyuk will know more about where this value is used again, if at all, since I think he is literally writing that code right now haha

On Thu, Nov 3, 2022, 8:58 PM Mark Santolucito @.***> wrote:

But if we lose any precision (I'm not really sure when this would happen anyway), then that lost precision value would be what we use the TSL-MT computation anyway. Although we only need the string for the preprocessor, we're going to be using the Float representation for any modulo theories reasoning. Certainly having two representations seems too complicated as well. @wonhyukchoi can you chime in on how this change would impact TSL-MT downstream?

On Thu, Nov 3, 2022, 8:04 PM Leo Qiao @.***> wrote:

@santolucito https://github.com/santolucito The reason was that reading a string to a float would lose precision in a lot of cases, and become impossible to write a show function that recovers the same decimal string representation.

If we still want an internal type representation, maybe we can store both the string and the float (i.e. TSLReal String Float), so that we have the original string to be used in encoding and the float to be used as the internal representation.

— Reply to this email directly, view it on GitHub https://github.com/Barnard-PL-Labs/tsltools/pull/42#issuecomment-1302807592, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIJAPFS3TFGBVVBDFHAORTWGRHHVANCNFSM6AAAAAARWUILZ4 . You are receiving this because you were mentioned.Message ID: @.***>

wonhyukchoi commented 2 years ago

The preprocessor is separate from anything TSL-MT related. No need to store the Real value. We can just keep it as a string. Changes lgtm, feel free to merge it.

The parser for the preprocessor is super hacky though, and not sure if spending more time is worth it. I'm planning to do a rewrite of the preprocessor by implementing a full-blown TSL parser later.

leoqiao18 commented 2 years ago

Added a small fix for issue #40, where the preprocessor parses / as a Mult.