cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Use Quote syntax instead of process_topdecs + append_prog

Open dnezam opened this issue 1 month ago • 0 comments

Files such as cakeml/basis/basisProgScript.sml already use modern syntax for quotes. Ideally, we would be using it more extensively where it makes sense.

For example, in readerProgScript.sml,

val _ = (append_prog o process_topdecs) ‘
  fun l2c_aux acc ins =
    case TextIO.inputLine ins of
      None => List.rev acc
    | Some ln => l2c_aux (tokenize (str_prefix ln)::acc) ins;
  ’;

would become

Quote add_cakeml:
  fun l2c_aux acc ins =
    case TextIO.inputLine ins of
      None => List.rev acc
    | Some ln => l2c_aux (tokenize (str_prefix ln)::acc) ins;
End

This should also be applied to patterns such as

val _ = process_topdecs `
  fun pureLoop x = pureLoop x;
  ` |> append_prog;

Before updating files, it would be good to ask whether there are any major reworks going on to avoid merge conflicts.

dnezam avatar Nov 12 '25 10:11 dnezam