Nat.toString and Nat.fromString

[xrchz]

• Define variants of the toString and fromString functions in basis/pure/mlintTheory that work on natural numbers rather than integers. (They should call the existing helper functions.)
• Prove them correct and add them to the basis library (either in Int or perhaps better in a new module Nator Num).
• Use these throughout the compiler and examples, in favour of any other number conversion functions.

[agomezl]

I finish writing basis/pure/mlnumTheory and now I'm fiddling with basis/NumProgTheory but am not quite sure how to get it right.

I am currently "copying" what is in IntProgTheory but dont know what to do with:

(* What is this BTW? *)
val _ = ml_prog_update (add_dec ``Dtabbrev unknown_loc [] "num" (Tapp [] TC_num)`` I);

val _ = trans "+" `(+):num->num->num`
val _ = trans "-" `(-):num->num->num`
val _ = trans "*" `($*):num->num->num `

(* Should I try to these? *)
(* val _ = trans "div" `(/):num->num->num` *)
(* val _ = trans "mod" `(%):num->num->num` *)
(* val _ = trans "<" `(<):num->num->bool` *)
(* val _ = trans ">" `(>):num->num->bool` *)
(* val _ = trans "<=" `(<=):num->num->bool` *)
(* val _ = trans ">=" `(>=):num->num->bool` *)

is this necessary for Num? for the most part I understand what is happening but don't really know if this should be (or is already) done somewhere else.

Additionally, when translating toString fromString and fromString_unsafe I get some inconsistent naming from the translator.

(* Gives me tostring_v_thm *)
val result = translate (toString_def |> REWRITE_RULE [mlintTheory.maxSmall_DEC_def]);
(*
> Translating tostring
val result =
   |- (NUM --> STRING_TYPE) toString tostring_v:
   thm
*)

(* Gives me fromstring_unsafe_1_v_thm *)
val result = translate fromString_unsafe_def;
(*
> Translating fromstring_unsafe_1

WARNING: fromstring_unsafe_1 has a precondition.

val result =
    [.]
|- (Eq STRING_TYPE v1 --> NUM) fromString_unsafe fromstring_unsafe_1_v:
   thm
*)

(* Gives me fromstring_v_thm *)
val result = translate fromString_def;
(*
Translating fromstring

WARNING: fromstring has a precondition.

val result =
    [.] |- (Eq STRING_TYPE v1 --> OPTION_TYPE NUM) fromString fromstring_v:
   thm
*)

This theory opens IntProgTheory hence toString fromString and fromString_unsafe are all "duplicated" but the translator only reflect this in fromString_unsafe, why?

[xrchz]

The naming thing (second part of your comment) might be because of capital letters. You should use next_ml_names to ensure the right name is given to the function in CakeML.

There's no num type in CakeML (and no TC_num). nums in HOL should target CakeML ints. But you should probably add all the operators to the Num module.. For div and mod they are called DIV and MOD, not / and %. I think trans is just adding a function to a module, assuming it has already been translated (as should be the case for all these operators).

Edit: maybe it's not so important to add the operators that are the same on ints. The question is whether we want to have a Num.num type (abbreviating int, but maybe opaque) in CakeML, or just have the Num module operating on ints (but with natural number semantics).

[xrchz]

You shouldn't copy the definitions of the to/from string functions. You should just call them.

[agomezl]

The definitions of the to/from string functions are in basis/pure/mlnumTheory and are pretty minimal since they mostly reuse stuff from mlintTheory

val toString_def = Define`
  toString n =
    if n < 10n then
      str (toChar n)
    else
      implode (toChars (n MOD maxSmall_DEC) (n DIV maxSmall_DEC) "")`;

val fromString_unsafe_def = Define`
  fromString_unsafe str =
    if strlen str = 0
    then 0n
    else fromChars_unsafe (strlen str) str`;

val fromString_def = Define`
  fromString str =
    if strlen str = 0
    then SOME 0n
    else fromChars (strlen str) str`;

The whole theory is just 55 lines long

[agomezl]

@xrchz Even after doing:

val _ = next_ml_names := ["toString"];
val result = translate
               (toString_def |> REWRITE_RULE [mlintTheory.maxSmall_DEC_def]);

val _ = next_ml_names := ["fromString_unsafe"];
val result = translate fromString_unsafe_def;

val _ = next_ml_names := ["fromString"];
val result = translate fromString_def;

I still get the same results (fromstring_unsafe_1_v_thm instead of fromstring_unsafe_v_thm)

[myreen]

Does it matter what the _v thms are called? Surely, the ML names are what matters.

[myreen]

Regarding minimal definitions. It would be neater if the definitions were directly referring to the other ones, e.g.

val toString_def = Define`
  toString n = mlint$toString (& n)`;

[agomezl]

@myreen mlint$toString is actually already turning it's int argument into a num since it uses mlint$toChars (which uses nums). mlnum$toString is just a simplified version of mlint$toString without all the conversion. (this is also true for fromString)

[myreen]

I still think it would be nicer to have smaller definitions, i.e. avoid the if etc.

[xrchz]

@myreen The v names matter a little bit because they are also the side condition names, which you have to refer to when you're proving them.

[agomezl]

@xrchz what is the purpose of reg_alloc.sml? and Is this code:

fun  num_to_dec v1 =
    if  (v1 < 10)
    then  [Char.chr (48 + v1)]
    else  (Char.chr (48 + (v1 mod 10))::(num_to_dec (v1 div 10)));

  fun  num_to_dec_string v1 =  reverse (num_to_dec v1);

  fun  alookup v5 v6 =
    case  v5
    of  []  =>  NONE
    |   v4::v3 =>  (case  v4
                    of  (v2,v1) =>  (if  (v2 = v6)
                                     then  (SOME(v1))
                                     else  (alookup v3 v6)));

Still necessary?

[xrchz]

Ask @tanyongkiam. I think it's not necessary if a new version can be generated from the translator.

[agomezl]

I just pushed some refactoring for mlnum$toString and mlnum$fromString couldn't find many uses of num_to_dec_string or num_from_dec_string so this is mostly simple rewrites. I'm currently running a full bootstrap to see if something breaks.

[xrchz]

Feel free to reopen the pull request. Then the regression test infrastructure can find what breaks for you instead :)

[tanyongkiam]

It is used for compilation in the logic to provide the oracle coloring functions.

Those lines are still needed, because this unverified allocator runs inside HOL4 and not CakeML.

I suppose you could make it generated by translation automatically, but then you would have to build all the way up to the translation of the allocator everytime you want to compile in the logic.