The second parameter is the word length.  For example:

wordsSyntax.mk_word (Arbnum.fromInt 0xA, Arbnum.fromInt 32)

For convenience, there is also

wordsSyntax.mk_wordi (Arbnum.fromInt 0xA, 32)

and

wordsSyntax.mk_wordii (0xA, 32)

Be aware that Mosml integers are 31 bits wide.  For example:

- mk_wordii (0xFFFFFFFF, 32);
! Toplevel input:
! mk_wordii (0xFFFFFFFF, 32);
!            ^^^^^^^^^^
! Lexical error: integer constant is too large.

However this is okay with PolyML:

 > mk_wordii (0xFFFFFFFF, 32);
val it = ``4294967295w`` : Abbrev.term

Anthony.

for the cases when the word length and value are integers.

On 15 Apr 2009, at 20:46, Lu Zhao wrote:

> Hey,
>
> Suppose there is a variable in SML:
>
> val v = 0xA
>
> How can I get a term which has the value of "v" in word32? I found
> mk_word in wordsSyntax, but I have no idea what the second parameter
> should be (I guess the first might be v)?
>
> Thanks.
> Lu


------------------------------------------------------------------------------
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to