* Support inductive type and universe expressions
* Support function type expressions
* Add type information to Core function and constructor nodes
* Remove unused do
* Add shelltests for `juvix repl`
* repl: Compute entrypoint root when loading a file
Previously the REPL would use app root (which could be the current
directory or the project root of the initially loaded file). Thus files
in a different project could not be loaded.
The entrypoint root must be computed each time a new file is `:load`ed.
Adds shell-tests for REPL commands
* Move preludePath to Juvix.Extra.Paths
* Adds a major mode for juvix-repl
* juvix-mode: C-c C-l loads file into REPL, if the REPL is running
* Detect ANSI support in Emacs REPL / shell by using hSupportsANSIColor API
* Disable comint echo handling. Juvix REPL does not echo
* repl: whitespace strip input to compile/eval/infer commands
`juvix` CLI invocations now read/write/delete the standard library in
the project's `.juvix-build/stdlib` directory.
When shelltest runs in threaded mode, two tests may run conflicting IO
operations on the same `.juvix-build/stdlib` directory.
* REPL support reloading
* Reformat :help and add :version command
* repl: Display the currently loaded module in the banner
* repl: Load the Prelude at launch unless --no-prelude or --no-stdlib are set
* Remove ParserParams
ParserParams is only used to record the root of the project, which is
used to prefix source file paths. However source file paths are always
absolute so this is not required.
* Add GetAbsPath to Files effect
The Files effect is not responsible for resolving a relative module
path into an absolute path on disk. This will allow us to resolve
relative module paths to alternative paths, for example to point to the
standard library on disk.
* Files effect getAbsPath returns paths within the registered standard
library
This means that the standard library can exist on disk at a different
location to the Juvix project.
A command line flag --stdlib-path can be specified to point to a
standard library, otherwise the embedded standard library is written to
disk at $PROJ_DIR/.juvix-build/stdlib and this is used instead.
* Recreate stdlib dir only when juvix version changes
* Add UpdateStdlib to the Files effect
* Add comment for stdlibOrFile
* Remove spurious import
```
builtin boolean-if
if : {A : Type} → Bool → A → A → A;
if true x _ := x;
if false _ x := x;
```
This allows a backend to translate if directly, so that only one branch
is evalutated.
An example compilation of if is given for the legacy backend for testing.
builtin boolean
inductive MyBool {
myTrue : Bool;
myFalse : Bool;
};
The first constructor is mapped to primitive true and the second
constructor is mapped to primitive false.
This also adds compilation of builtin boolean in the legacy backend as
this was trivial to implement.
* remove ≔ from the language and replace it by :=
* revert accidental changes in juvix input mode
* update stdlib submodule
* rename ℕ by Nat in the tests and examples
* fix shell tests
