fix external names

[gizemcaylak]

This PR fixes external names in file-ext.mc since it causes a conflict in Miking CorePPL with readFile built-in due to how externals are handled. There is an intrinsic called readLines so the external 'readLine' shadows that intrinsic and causes the external's name to change in Miking CorePPL. @br4sco suggested the best option is that before printing, we could go through all externals and add their symbols to the pretty print environment before we start pretty printing (though not sure how to integrate that in the CorePPL compiler currently). A temporary solution Oscar suggested for now is to rename externals to prevent this.

[marten-voorberg]

Could you elaborate a bit more on the conflict? It seems a little undesirable to me to add such a verbose prefix to every external.

[gizemcaylak]

Could you elaborate a bit more on the conflict? It seems a little undesirable to me to add such a verbose prefix to every external.

In Miking CorePPL compiler, when I use readLine, I get this error: ERROR </tmp/miking-tmp.Si3PRRixQk0 5216:0-5230:2>: No implementation for external readLine1.

external readLine1! : ReadChannel -> ([Char], Bool)
in
let readLine2: ReadChannel -> Option [Char] =
  lam rc.
    match
      readLine1 rc
    with
      (s51, false)
    then
      Some
        s51
    else
      None
        {}
in

There is an intrinsic called readLines so the external shadows that intrinsic and get a name suffixed with a 1. @br4sco suggested the best option is that before printing, we could go through all externals and add their symbols to the pretty print environment before we start pretty printing (though not sure how to integrate that in the CorePPL compiler currently). A temporary solution Oscar suggested for now is to rename externals to prevent this.

[br4sco]

Could you elaborate a bit more on the conflict? It seems a little undesirable to me to add such a verbose prefix to every external.

In short, readLine is intrinsic, and because we do not have any namespacing and includes are transitive, It is hard to control what gets pulled into scope when you include a file (which may, as in this case, shadow an intrinsic). @gizemcaylak issue is a combination of these unexpected includes and a bug in the pretty printer, which currently can't handle the case when an external name collides with an intrinsic name. This name change makes sense because of how includes works regardless of this pretty printer bug and solves the issue for @gizemcaylak

I would go a step further and change the name of readLine in

let readLine : ReadChannel -> Option String =
  lam rc. match externalReadLine rc with (s, false) then Some s else None ()

to a name that does not clash with the intrinsic readLine to avoid unexpected shadowing. I think that we, in general, should disallow shadowing of intrinsics in the standard library as long as includes works as they do now.

We can discuss how and who should address the pretty printer bug at the next Miking meeting.