This PR adds a builtin integer type to the surface language that is
compiled to the backend integer type.
## Inductive definition
The `Int` type is defined in the standard library as:
```
builtin int
type Int :=
| --- ofNat n represents the integer n
ofNat : Nat -> Int
| --- negSuc n represents the integer -(n + 1)
negSuc : Nat -> Int;
```
## New builtin functions defined in the standard library
```
intToString : Int -> String;
+ : Int -> Int -> Int;
neg : Int -> Int;
* : Int -> Int -> Int;
- : Int -> Int -> Int;
div : Int -> Int -> Int;
mod : Int -> Int -> Int;
== : Int -> Int -> Bool;
<= : Int -> Int -> Bool;
< : Int -> Int -> Bool;
```
Additional builtins required in the definition of the other builtins:
```
negNat : Nat -> Int;
intSubNat : Nat -> Nat -> Int;
nonNeg : Int -> Bool;
```
## REPL types of literals
In the REPL, non-negative integer literals have the inferred type `Nat`,
negative integer literals have the inferred type `Int`.
```
Stdlib.Prelude> :t 1
Nat
Stdlib.Prelude> :t -1
Int
:t let x : Int := 1 in x
Int
```
## The standard library Prelude
The definitions of `*`, `+`, `div` and `mod` are not exported from the
standard library prelude as these would conflict with the definitions
from `Stdlib.Data.Nat`.
Stdlib.Prelude
```
open import Stdlib.Data.Int hiding {+;*;div;mod} public;
```
* Closes https://github.com/anoma/juvix/issues/1679
* Closes https://github.com/anoma/juvix/issues/1984
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Depends on PR #1832
* Closes#1799
* Removes Backend.C.Translation.FromInternal
* Removes `foreign` and `compile` blocks
* Removes unused test files
* Removes the old C runtime
* Removes other dead code
- Closes#1637.
A function type signature is now allowed to have a body. This is valid
for both top level and let definitions.
```
not : Bool -> Bool := λ {
| true := false
| false := true
};
```
* 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
* add a simple positive test
* add lambda expressions to microjuvix language
* add basic normalization of type aliases
* fix test name
* normalize only functions on types
* normalize when matching
* fix type of inductive names
* improve detection of normalizing functions
* remove obsolete comment
* match constructor return type
* add test for issue 1333
* fix existing tests
* use lambda case
* add strong normalization
* Add test cases for type aliases and another fix
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* w.i.p
* Added strict positivity condition for datatypes w.i.p
* Add negative test for str.postivity check
* Add some revisions
* the branch is back to feet
* w.i.p add lots of traces to check alg.
* Add more test and revisions
* Add negative and positive test to the new flag and the keyword
* Fix shell tests.
* Make pre-commit happy
* Fix rebase conflicts
* Make pre-commit happy
* Add shell test, rename keyword, fix error msg
* Revert change
* Necessary changes
* Remove wrong unless
* Move the positivity checker to its own folder
* Add missing juvix.yaml
* Add a negative test thanks to jan
* make some style changes
* Make ormolu happy
* Remove unnecessary instance of Show
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* keep qualified names
* add comment
* add pretty field to Abstract Name
* add test
* Add shell test
* Add another test
* fix shell test
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* Implement error message for double braces
* Implement error message for implicit pattern on the left of an application
* Implement error message for constructor expected on the left of an application
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Renaming MiniJuvix to Juvix
* Make Ormolu happy
* Make Hlint happy
* Remove redundant imports
* Fix shell tests and add target ci to our Makefile
* Make pre-commit happy
* Throw error when reading a file that conflicts with stdlib
The Files effect first tries to read a file from the embedded stdlib. If
this succeeds and the file also exists in the project then an error is
thrown.
This error can be thrown either at the parsing stage, if the entrypoint
file conflicts with the standard library, or at the scoping stage if an
imported file conflicts.
* Fix module name in test file
* work in progress towards implicit arguments
* Wip towards implicit types
* improve arity checker
* Add version of SimpleFungibleToken with implicit arguments
* guess arity of body before checking the lhs of a clause
* add ArityUnknown and fix some tests
* wip: proper errors in arity checker
* fix bugs, improve errors and add tests
* format
* set hlint version to 3.4 in the ci
* update pre-commit version to 3.0.0
* minor changes
* added more revisions
* minor
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* [WIP] EntryPoint now has options. --no-termination is a new global opt.
* Add TerminationChecking to the pipeline
* Add TerminationChecking to the pipeline
* Keep GlobalOptions in App
* Fix reviewer's comments
* delete unnecessary parens
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* add face and handling of not in scope symbol error
* small fix
* generic errors wip
* add App effect
* format
* add flycheck-minijuvix
* use absolute paths and refactor
* fix dir0
* add generic error instances and improve some errors
* format
* qualify strings
* use AnsiText
* add ToGenericError instances for the type checker errors
* improve error message
* improve handling of parsing errors
* Parsing terminating keyword
* cosmetics
* Add support for `terminating` keyword to function decl.
* Minor replacement
* Fix .mjuxix to .mjuvix and the module name
* Add support for compile (by Jonathan)
* Remove error related to unsopported backend
Co-authored-by: Jonathan Prieto-Cubides <jonathan.cubides@uib.no>
In the following case:
```
module WrongConstructorArity;
inductive T {
A : T;
};
f : T → T;
f (A i) ≔ i;
end;
```
The typechecker fails when checking the clause `f (A i) := i` because of
the extra constructor argument. However if typechecking continues then
the variable `i` on the rhs does not have a type so we must short-circuit.
* [ format ] AbstractToMicroJuvix
* [ CI ] fixes
* [ CI ] fixes
* [ CI ] Using GHC 9.0 for Hlint
* [ CI ] Use static-checks for Dev as well
* [test] Add positive test for typechecker
* [test] Improve positive typechecker error output
* [typecheck] Restore correct handling of TypeAny
I mistakenly removed the matchTypes function in
https://github.com/heliaxdev/minijuvix/pull/22. This caused the handling
of TypeAny to break.
Literals have type TypeAny and so should be valid when matching against
any other type. The tests have been updated to reflect this.
* [test] Add positive MicroJuvix typecheck tests
* [ ormolu ] fixes
Co-authored-by: Jonathan Prieto-Cubides <jonathan.cubides@uib.no>
