* [cbackend] Adds an AST for C
This should cover enough C to implement the microjuvix backend.
* [cbackend] Add C serializer using language-c library
We may decide to write our own serializer for the C AST but this
demonstrates that the C AST is sufficient at least.
* [cbackend] Declarations will always be typed
* [cbackend] Add CPP support to AST
* [cbackend] Rename some names for clarity
* [cbackend] Add translation of InductiveDef to C
* [cbackend] Add CLI for C backend
* [cbackend] Add stdbool.h to file header
* [cbackend] Allow Cpp and Verbatim code inline
* [cbackend] Add a newline after printing C
* [cbackend] Support foreign blocks
* [cbackend] Add support for axioms
* [cbackend] Remove code examples
* [cbackend] wip FunctionDef including Expressions
* [parser] Support esacping '}' inside a foreign block
* [cbackend] Add support for patterns in functions
* [cbackend] Add foreign C support to HelloWorld.mjuvix
* hlint fixes
* More hlint fixes not picked up by pre-commit
* [cbackend] Remove CompileStatement from MonoJuvix
* [cbackend] Add support for compile blocks
* [cbackend] Move compileInfo extraction to MonoJuvixResult
* [minihaskell] Fix compile block support
* [chore] Remove ununsed isBackendSupported function
* [chore] Remove unused imports
* [cbackend] Use a Reader for pattern bindings
* [cbackend] Fix compiler warnings
* [cbackend] Add support for nested patterns
* [cbackend] Use functions to instantiate argument names
* [cbackend] Add non-exhaustive pattern error message
* [cbackend] Adds test for c to WASM compile and execution
* [cbackend] Add links to test dependencies in quickstart
* [cbackend] Add test with inductive types and patterns
* [cbackend] Fix indentation
* [cbackend] Remove ExpressionTyped case
https://github.com/heliaxdev/minijuvix/issues/79
* [lexer] Fix lexing of \ inside a foreign block
* [cbackend] PR review fixes
* [chore] Remove unused import
* [cbackend] Rename CJuvix to MiniC
* [cbackend] Rename MonoJuvixToC to MonoJuvixToMiniC
* [cbackend] Add test for polymorphic function
* [cbackend] Add module for string literals
* add TypeCallsBuilder and others
* implement propagation of type calls
* improve type propagation
* polymorphize fungible token
* sort type calls map pretty output
* use HashSet in TypeCallsMap
* renaming
* rename module
* improve indexing in type propagation
* draft monomorphization generation algorithm
* fix draft
* wip mono code generation
* wip code generation
* finish first candidate for code generation
* add monojuvix command
* fix MonoJuvix pretty printer to properly display name ids
* [monojuvix] improve clause pretty printing
* add support for function types in expressions
* properly translate function expressions
* ormolu
* add a basic positive test for monomorphization
* cleanup effect constraints
* collect type applications in axiom types
* apply some style improvements
* fix PolySimpleFungibleToken and add it to the test suite
* ignore polymorphic inductive definitions that are never used
* 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>
* add references to the syntax and cleanup code
* [make] add .PHONY to Makefile targets
* [parser] add parser / pretty for axiom backends
* Pairing progress
* [scoper] Add support for Axiom backends
* [parser] Fix foreign block parsing
* [ app ] adds --no-colors flag for the scope command
* [ghc] upgrade to ghc 9.2.2
* use GHC2021
* [doc] Remove out-of-date comment
* [test] Add ambiguity tests
* [scoper] Improve resolution of local symbols
* [error] WIP improving ambiguity error messages
* [ clean-up ] new lab folder for experimentation
* [ app ] ixes the lint warning
* [ Termination ] removes Alga dependency
* [error] Add message for ambiguous symbol error
* [error] Add ambiguous module message
* [scoper] Remove ErrGeneric
* [test] Add test to suite
* [test] show diff when ast's are different
* [ lab ] folder organization
* [ Makefile ] add targets with --watch option (stack cmds) and remove unused things
* [ app ] add --version flag and fixed warnings and formatting
* [test] remove fromRightIO to fix ambiguity error
* [test] Add test of shadowing public open
* [scoper] Add visibility annotation for Name
* prepare buildIntoTable
* [ Concrete ] add instance of hashable for refs.
* add InfoTableBuilder effect
* [ scoper ] add InfoTableBuilder effect
* [ CHANGELOG ] updated v0.1.1
* [ README ] org version now
* fix package.yaml
* fix readme
* [microjuvix] implement basic typechecker
* add simple test for MicroJuvix type checker
* fix checking for constructors apps in patterns
* [scope] Move InfoTable to a new module
* [abstract] Make Iden use references instead of Name
* [abstract] Add InfoTable for abstract syntax
* [scoper] Add function clauses to scoped InfoTable
* [abstract] Add InfoTableBuilder for scoped to abstract
* [main] Fix callsites of translateModule
* [doc] Remove empty docs
* [scoper] Update emptyInfoTable with missing field
* rename some functions
* [minihaskell] add compilation to MiniHaskell
* [microjuvix] improve wrong type message
* Add a validity predicate example written in MiniJuvix
* [typecheck] Add error infrastructure for type errors
Add a pretty error for mismatched constructor type in a pattern match
* [test] Adds negative typecheck test for constructor
* [app] Adds microjuvix subcommands for printing / typechecking
* [typecheck] Add error message for ctor match args mistmatch
* [typecheck] Add descriptive messages for remainng errors
* [typecheck] Updates to error message copy
* [typecheck] fix merge conflicts:
* [highlight] add basic support for highlighting symbols
* [minijuvix-mode] add minijuvix-mode and basic description in the readme
* [readme] improve formatting
* automatically detect the root of the project and add --show-root flag
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Paul Cadman <pcadman@gmail.com>
