[ elab ] Support limited file operations in elab scripts, e.g. enable type providers

[buzden]

Description

Idris 1 used to have type providers, facilities that allowed pretty arbitrary code to be additionally executed at the compile time allowing to provide particular values based on whatever stuff. But this approach is very fragile and unsafe, since arbitrary effects can break a lot and generally seems to be undesired.

Seemingly, most important feature was a file access. This allowed to implement the principle of a single source of truth in a higher level and typesafe manner. Say, your code interacts with some other code with some well-defined typed interface and if you can generate a type declaration from this description automatically during compile time, you've solved a problem of synchronisation: each time the common description updates, your types update too. If the change was incompatible, you code stopped compiling.

The vice-versa situation is possible -- one may want to define types in Idris but to be able to export some data in a well-defined format to couterparties and to have them be synchonised well automatically.

What I propose is to make elaborator scripts to be able to access files in the project dir with a simple interface allowing type providers stuff without allowing arbitrary IO at compile time. You can see an example of primitive limited type provider in the added test.

An additional action called idrisDir is also proposed to be added. It allows returning paths of project dirs. This can be useful for nicer error messages (see the test for example). Also, I have at least one more nice use case for it, it is not trivial, but I'll explain it if there is a need.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).