-
Notifications
You must be signed in to change notification settings - Fork 90
Open
Labels
Description
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;
EndThis 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.