Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* v0.1.1 (#15) * 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 Co-authored-by: Jan Mas Rovira <[email protected]> Co-authored-by: Paul Cadman <[email protected]> * [ package.yaml ] update version * 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 * Adds many new features (w.i.p v0.1.2) (#28) * 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 <[email protected]> Co-authored-by: Paul Cadman <[email protected]> Co-authored-by: Paul Cadman <[email protected]> * [ CI ] Add Haskell Github Action with Stack test and ormolu check * [typecheck] Return all errors encountered during typechecking Any expression that fails typechecking is assigned TypeAny so typechecking can proceed. * [typecheck] Wrap type errors in NonEmpty * [typechecker] throw in expressions, collect in clauses * [typecheck] Add the definition loc to microjuvix names This is used in type errors * [concrete] Adds location info to Literal * [typecheck] Add function name to pattern type errors * [typecheck] Add concrete name location to type error messages for expression * [test] Add test for multiple type errors Add test for literals * [prelude] Remove Control.Monad from export Control.Monad is already exported by Control.Monad.Extra * [concrete] Add HasLoc for LiteralLoc * [ pre-commit ] Add support and hooks * [ hlint ] fix some hints * [ CI ] Add hlint check * [doc] Add docs for enabling CLI autocompletion (#31) * Remove missused import * setup InfoTable for parser * define ParserResult and refactor * [minijuvix-mode] save buffer and clear annotation before loading * [ CI ] New jobs: ormolu and hlint * Add action hints for autocompletion (#35) * [ format ] AbstractToMicroJuvix * [ CI ] fixes * [ CI ] fixes * [ CI ] Using GHC 9.0 for Hlint * [ CI ] Use static-checks for Dev as well * [app] Add action hints for autocompletion Using `action "file"` means that the autocompletion for that part of the command will prompt the user with a list of files. Without these action hints the user would have to type out the whole path to the file without autocompletion assistance. Co-authored-by: Jonathan Prieto-Cubides <[email protected]> * Restore correct handling of TypeAny and add positive typecheck tests (#34) * [ 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 anoma/minijuvix#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 <[email protected]> * wip * add evil kbds * fix * Fix typo * [emacs] Add load and goto def keybindings * [emacs] Remove extra evil-define-key * [emacs] Use 'evil hook instead of 'evil-maps * [emacs] Add message if no goto information is found * Better to use kbd * wip * w.i.p * Fix compilation * Make Ormolu happy and Hlint * w.i.p Fixing test suite * Fix test suite * [minihaskell] Do not add id suffix to top-level modules and main For minihaskell the name of the output file needs to match the module name. So we must not add the usual '_<nameid>' suffix to top level names. Additionally the main function in a haskell file is the entry-point to the haskell program. So the suffix must not be added in this case also. * [minihaskell] Output ANSI codes only if handle supports it This adds `ansi-terminal` dependency to the Main target but this is already a transitive dependency of `prettyprinter-ansi-terminal`. We want to add this support globally which we will do in https://github.com/heliaxdev/minijuvix/issues/38. * [typecheck] Shortcircuit clause pattern check errors 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. * [ README ] Add badges and grammar * w.i.p Add global option --no-color * emacs mode: keep buffer saved after highlighting * add generic pretty utilities * w.i.p refactoring ansi/text pretty printer * [test] Update VP example * [test] Add Anoma Haskell backend for VP * fix #29 * emacs mode: keep buffer saved after highlighting * [test] Update VP example * [test] Add Anoma Haskell backend for VP * make my friends hlint and ormolu happy * run ormolu 4 * remove undefined (#56) * [emacs] Add copy of agda-input to minijuvix-mode (#57) This provides agda-input method (under the name `minijuvix`) to minijuvix-mode. Co-authored-by: Jan Mas Rovira <[email protected]> Co-authored-by: Paul Cadman <[email protected]> Co-authored-by: Paul Cadman <[email protected]> Co-authored-by: caryoscelus <[email protected]>
- Loading branch information
5 people
authored
Apr 11, 2022
1 parent
eee91cb
commit f55112f