CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

w1 ₃₂→₁₆ w2 #713

Open mn200 opened 4 years ago

mn200 commented 4 years ago

Make it so. Depends on #499

mn200 commented 4 years ago

Actually, casts are unary, so perhaps we could have this as a suffix, so that

     w1 ₃₂→₁₆

would be the 16 bit value corresponding to w1.

Alternatively, and this is the one that Magnus prefers, have

        ₃₂←₁₆ w2

which would be the 32 bit version of (16 bit value) w2.

konrad-slind commented 4 years ago

Possibly naive question. Why not have a general operation

width(w,n)

which maps word w to its corresponding n-width version? Being binary, the "width" operation could even be an infix, although I am not sure that you are even considering concrete syntax.

On Tue, Jan 7, 2020 at 10:01 PM Michael Norrish notifications@github.com wrote:

Actually, casts are unary, so perhaps we could have this as a suffix, so that

 w1 ₃₂→₁₆

would be the 16 bit value corresponding to w1.

Alternatively, and this is the one that Magnus prefers, have

    ₃₂←₁₆ w2

which would be the 32 bit version of (16 bit value) w2.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/CakeML/cakeml/issues/713?email_source=notifications&email_token=AAIOAD6PZIBZS2EGLIVUL73Q4VF2BA5CNFSM4KC7NCGKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEILDSNI#issuecomment-571881781, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD7OZ3DDVTOO3LB57W3Q4VF2BANCNFSM4KC7NCGA .

mn200 commented 4 years ago

You actually need to know both source and destination sizes, so in some sense it's a ternary operation. Moreover, the source and dest numbers have to be literals; they're not really arguments in the way that the w is.

(This is all supposing that we have words of arbitrary widths floating around (as per issue #499).)

konrad-slind commented 4 years ago

Right. I was operating under the assumption that w would have a type from which its size could be calculated. (I did this in a language we worked on at Collins. Yes, the target width was a literal.)

On Tue, Jan 7, 2020 at 11:22 PM Michael Norrish notifications@github.com wrote:

You actually need to know both source and destination sizes, so in some sense it's a ternary operation. Moreover, the source and dest numbers have to be literals; they're not really arguments in the way that the w is.

(This is all supposing that we have words of arbitrary widths floating around (as per issue #499 https://github.com/CakeML/cakeml/issues/499 ).)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/CakeML/cakeml/issues/713?email_source=notifications&email_token=AAIOAD6R3YAAI4ABUWZ6GHDQ4VPJ5A5CNFSM4KC7NCGKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEILHBLI#issuecomment-571895981, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD7S5N6ZGSGMAWS3Q7DQ4VPJ5ANCNFSM4KC7NCGA .