Juvix
CI Status |
---|
Codebase |
|
|
Juvix is an open-source, constantly evolving functional programming language designed for writing privacy-preserving decentralized applications. Using Juvix, developers can write high-level programs which can be compiled to WASM directly, or through VampIR to circuits for private execution with Taiga on Anoma or Ethereum.
Getting Started
To get started with Juvix, head over to the documentation website to learn more about the language and its features. You can also find installation instructions and tutorials to help you get started with writing Juvix programs. You can download the latest release from the Juvix GitHub repository or use the web-based development environment, Juvix Github Codespace, which provides a pre-configured workspace ready to use with Juvix and the Haskell toolchain installed.
Language features
Juvix is designed with a focus on safety. The Juvix compiler runs several static analyses which guarantee the absence of runtime errors. Analyses performed include termination and type checking. As a result, functional programs, especially validity predicates, can be written with greater confidence in their correctness.
Some language features in Juvix include:
- Haskell/Agda-like syntax with support for Unicode
- Type inference
- Parametric polymorphism
- User defined inductive data types
- Higher-order functions
- Referential transparency
The Juvix module system allows developers to break down their programs into smaller, reusable modules that can be compiled separately and combined to create larger programs. These modules can be used to build libraries, which can then be documented using Juvix's built-in documentation generation tool, see for example, the Juvix standard library's website. For further details, please refer to the Juvix book which includes our latest updates.
Related projects
If you're interested in Juvix, you may also want to explore the following related projects:
Project | Description |
---|---|
GEB | Intermediate language for writing compilers and one of the Juvix backends. |
VampIR | Proof-system-agnostic language for writing arithmetic circuit and one of the GEB backends. |
Taiga | A framework for generalized shielded state transitions. |
Resources
Here is a summary of resources to help you learn more about Juvix:
Documentation
Resource | Description |
---|---|
Official website | The official website of Juvix, where you can find documentation, changelog, tutorials, and community resources. |
GitHub repository | The official GitHub repository of Juvix, where you can find the source code and contribute to the project. |
Community
Resource | Description |
---|---|
Discord community | The Juvix community on Discord is a space where you can connect with the developers behind Juvix and other members of the community who are passionate about privacy-preserving decentralized applications. It's a place where you can ask for help with using Juvix, discuss the latest features and updates, and get involved in the project. |
The official Twitter account of Juvix, where you can stay up-to-date with the latest news and announcements. |
Libraries
Resource | Description |
---|---|
Standard library | The Juvix standard library is a collection of pre-written functions and modules that come bundled with the Juvix programming language. It provides developers with a set of common and useful tools that they can use to build their Juvix programs without having to write everything from scratch. |
IDE support
Resource | Description |
---|---|
VSCode extension | Support for the Juvix programming language with features such as syntax highlighting, error checking and many more directly in the VSCode editor. |
Emacs Juvix mode | A major mode for Emacs that provides support for writing Juvix programs. |
Development environments
Resource | Description |
---|---|
Juvix Standard Lib Codespace | A web-based development environment for the Juvix standard library on GitHub. It provides a pre-configured workspace with the Juvix standard library installed and ready to use, so you can start using the library in your projects. Some examples of Juvix programs are also loaded in this environment. |
Juvix Github Codespace | This codespace provides a pre-configured workspace with Juvix and the Haskell toolchain installed. Everything is ready to use, so you can start developing/inspecting the Juvix compiler right away. |
Installation
Resource | Description |
---|---|
Homebrew Juvix formula | A formula for Homebrew, a package manager for macOS and Linux, that allows you to easily install Juvix on your system. |
Juvix Nightly builds | Users can download and use these nightly builds to experiment with the latest changes to the Juvix Compiler. Nightly builds may contain new features, bug fixes, and other improvements to Juvix that are still in development and have not yet been released in an official version. |
Contributing
If you're interested in contributing to Juvix, please see the contributing guidelines for more information. We welcome contributions of all kinds, from bug reports and feature requests to code contributions and documentation improvements.
License
Juvix is open-source software released under the GNU General Public License v3.0. See the LICENSE file for more information.
Changelog
v0.3.0 (2023-03-15)
Implemented enhancements:
- Avoid line breaks in applications within a type signature #1850 (paulcadman)
- Respect user's spacing decisions in the formatter #1837 (janmasrovira)
- Formatter should not transform ASCII symbols to unicode by default #1827 (janmasrovira)
- Enable match-to-case, nat-to-int and convert-builtins by default in REPL #1825 (lukaszcz)
- The Juvix formatter works poorly with multi-line ifs #1793 (janmasrovira)
- Add a lazy IO sequencing function (#1772) #1773 (lukaszcz)
- Support LetRec in the GEB backend #1756 (janmasrovira)
- Support integers in the GEB backend #1753 (lukaszcz)
- GEB evaluator #1751 (jonaprieto)
- Add debugging builtin functions #1731 (jonaprieto)
- Non-judoc comments are removed when generating HTML output #1723 (janmasrovira)
- Special syntax for
case
#1716 (janmasrovira) - Make || and && lazy #1701 (lukaszcz)
- It should be possible to specify multiple implicit type arguments at once #1692 (janmasrovira)
- Naive compilation of complex pattern matches with match-expressions to decision trees with case-expressions #1531 (paulcadman)
- New compilation pipeline #1832 (lukaszcz)
- Add internal core-eval option to evaluate named function identifier #1819 (paulcadman)
- Short syntax for sequences of function and datatype parameters #1809 (lukaszcz)
- Add Geb Backend Evaluator with some extra subcommands #1808 (jonaprieto)
- Add REPL option to apply Core transformations #1796 (paulcadman)
- String builtins #1784 (lukaszcz)
- Use restore/save github action to speed up the CI testing #1783 (jonaprieto)
- Fix minor issue with ==% for type equality #1780 (jonaprieto)
- Add debugging builtin functions
trace
andfail
#1771 (jonaprieto) - Keep regular comments in html output #1766 (janmasrovira)
- Lazy boolean operators #1743 (lukaszcz)
- Refactor
html
command with extra options #1725 (jonaprieto) - Add initial setup for codespaces #1713 (jonaprieto)
- Typecheck let expressions #1712 (janmasrovira)
- Use Smoke instead of shelltestrunner #1710 (jonaprieto)
- Replace –output-dir flag by –internal-build-dir #1707 (jonaprieto)
- Compiler output #1705 (jonaprieto)
- Allow optional pipe before the first constructor for inductive type declarations #1699 (jonaprieto)
- Nat builtins #1686 (lukaszcz)
Merged pull requests:
- Remove dead code in
Internal
#1891 (janmasrovira) - Remove missing Juvix examples and webapp example from docs build #1890 (paulcadman)
- Fix type synonym in let #1880 (janmasrovira)
- Update stack resolver to lts-20.12 #1873 (paulcadman)
- Use Ape to format patterns #1870 (janmasrovira)
- Fix Core-To-Geb translation #1863 (jonaprieto)
- Remove the old C backend #1862 (lukaszcz)
- Move
substEnv
to its own module #1861 (janmasrovira) - Add
_caseTypeWholeExpression
to Internal #1860 (janmasrovira) - remove old minihaskell files #1859 (jonaprieto)
- Fix bugs in the Case translation in Core-to-Geb #1858 (lukaszcz)
- Format examples #1856 (janmasrovira)
- Sort the identifiers topologically in the Core-to-GEB translation #1854 (lukaszcz)
- Add type info to the mid-square hashing function #1853 (lukaszcz)
- Use APE mechanism to format Function expressions #1852 (paulcadman)
- Preserve single wildcards pretty printing function parameters #1851 (paulcadman)
- Add type annotation to case expression #1849 (janmasrovira)
- Remove module parameters #1848 (janmasrovira)
- Allow shadowing local variables with let function definitions #1847 (janmasrovira)
- Add lambda type info #1845 (janmasrovira)
- Improve comma formatting #1842 (janmasrovira)
- Improve formatter #1840 (janmasrovira)
- Respect lambda Ascii/Unicode #1838 (janmasrovira)
- Fix
juvix init
#1835 (janmasrovira) - The formatter respects the ascii function arrow #1834 (janmasrovira)
- Add
dev core from-concrete
command #1833 (janmasrovira) - Give proper errors for incorrect application of lazy builtins #1830 (lukaszcz)
- Documentation: update language reference #1829 (lukaszcz)
- Add compilation of complex pattern matching to case #1824 (paulcadman)
- Apply CI ghcup workaround to docs build #1823 (paulcadman)
- Update the Juvix tutorial for 0.3 #1822 (lukaszcz)
- Workaround ghcup issue on CI runner #1821 (paulcadman)
- Respect the
juvix dev highlight --format
flag when outputting errors #1820 (janmasrovira) - Comments about the usage of the JuvixCore recursors #1818 (lukaszcz)
- Emacs mode and VSCode extension tutorials #1815 (lukaszcz)
- Documentation: how to compile Juvix programs #1813 (lukaszcz)
- Make '>>' lazy #1812 (lukaszcz)
- Output proper GEB Lisp programs #1810 (lukaszcz)
- Remove the usage annotation syntax #1805 (lukaszcz)
- Mid-square hashing implemented in JuvixCore #1804 (lukaszcz)
- Autocompletion for
dev core compilation --target
#1803 (janmasrovira) - Special syntax for case #1800 (janmasrovira)
- Adapt benchmarks to the new pipeline #1795 (lukaszcz)
- Support letrec lifting without lambda lifting #1794 (janmasrovira)
- Use the reader effect #1791 (janmasrovira)
- Remove braces from let expressions #1790 (janmasrovira)
- Translate as-pattern binders to Core PatternBinders #1789 (paulcadman)
- Fix termination with as-patterns #1787 (janmasrovira)
- Allow type signatures to have a body #1785 (janmasrovira)
- Track builtins in the Core InfoTable #1782 (paulcadman)
- Pipes for lambda clauses #1781 (janmasrovira)
- Support integers in the GEB backend #1778 (lukaszcz)
- Add builtin nat and bool types as start nodes in reachability analysis #1775 (paulcadman)
- Update pre-commit #1772 (jonaprieto)
- Parse JuvixCore with absolute paths #1770 (paulcadman)
- Use absolute path in Core Evaluator to generate source file location #1769 (paulcadman)
- Install wasmer binary from Github releases #1765 (jonaprieto)
- Run the new Juvix formatter for all the Juvix examples #1764 (jonaprieto)
- Fix let expressions in the repl #1763 (janmasrovira)
- Improve arity inference for repl expressions #1762 (janmasrovira)
- Fix broken links and other improvements #1761 (jonaprieto)
- Translate Nat builtins to the correct Core Ops #1760 (paulcadman)
- Remove hlint from the CI and pre-commit config #1759 (jonaprieto)
- Fix demo example build #1757 (paulcadman)
- Basic Geb integration #1748 (lukaszcz)
- Fix macOS CI build #1747 (paulcadman)
- Adapt Juvix programs to the new pipeline #1746 (lukaszcz)
- Fix link in README for the new docs #1745 (lukaszcz)
- Move juvix-mode to a separate repository #1744 (jonaprieto)
- Print comments when pretty printing concrete syntax #1737 (janmasrovira)
- Demo #1736 (lukaszcz)
- Update CI to install Smoke, Github actions, and Makefile fixes #1735 (jonaprieto)
- Update stack.yaml #1734 (jonaprieto)
- Fix Nat builtins #1733 (lukaszcz)
- Script to count LOC #1732 (lukaszcz)
- Give a proper type to literal Strings #1730 (paulcadman)
- Do not filter implicit args in internal to core translation #1728 (paulcadman)
- Fix de Brujin indexing of lambda arguments #1727 (paulcadman)
- Fix inference loop #1726 (janmasrovira)
- Remove wildcard patterns from Internal #1724 (janmasrovira)
- Restructure the documentation and add a tutorial #1718 (lukaszcz)
- Improve error message for confusing ':=' with '=' #1715 (lukaszcz)
- Fix #1704 #1711 (janmasrovira)
- Fix #1693 #1708 (janmasrovira)
- Tests for the new compilation pipeline #1703 (lukaszcz)
- Add printString and printBool support to legacy C backend #1698 (paulcadman)
- Add –show-de-bruijn option to
juvix repl
#1694 (lukaszcz) - Allow 'terminating' keyword with builtins #1688 (lukaszcz)
- Remove unicode cons symbol #1687 (lukaszcz)
- Change syntax for ind. data types and forbid the empty data type #1684 (jonaprieto)
- Convert Nat literals to Core integers #1681 (lukaszcz)
- Less verbose output from running
make check
#1675 (jonaprieto) - Remove where syntax #1674 (jonaprieto)
- Benchmarks #1673 (janmasrovira)
- JuvixCore to JuvixAsm translation #1665 (lukaszcz)
v0.2.9 (2023-01-18)
Implemented enhancements:
- Refactor
html
command with extra options #1725 (jonaprieto) - Add initial setup for codespaces #1713 (jonaprieto)
- Typecheck let expressions #1712 (janmasrovira)
- Use Smoke instead of shelltestrunner #1710 (jonaprieto)
- Replace –output-dir flag by –internal-build-dir #1707 (jonaprieto)
- Compiler output #1705 (jonaprieto)
- Allow optional pipe before the first constructor for inductive type declarations #1699 (jonaprieto)
- Nat builtins #1686 (lukaszcz)
Merged pull requests:
- Demo #1736 (lukaszcz)
- Update stack.yaml #1734 (jonaprieto)
- Fix Nat builtins #1733 (lukaszcz)
- Script to count LOC #1732 (lukaszcz)
- Give a proper type to literal Strings #1730 (paulcadman)
- Do not filter implicit args in internal to core translation #1728 (paulcadman)
- Fix de Brujin indexing of lambda arguments #1727 (paulcadman)
- Fix inference loop #1726 (janmasrovira)
- Remove wildcard patterns from Internal #1724 (janmasrovira)
- Restructure the documentation and add a tutorial #1718 (lukaszcz)
- Improve error message for confusing ':=' with '=' #1715 (lukaszcz)
- Fix #1704 #1711 (janmasrovira)
- Fix #1693 #1708 (janmasrovira)
- Tests for the new compilation pipeline #1703 (lukaszcz)
- Add printString and printBool support to legacy C backend #1698 (paulcadman)
- Add –show-de-bruijn option to
juvix repl
#1694 (lukaszcz) - Allow 'terminating' keyword with builtins #1688 (lukaszcz)
- Remove unicode cons symbol #1687 (lukaszcz)
- Change syntax for ind. data types and forbid the empty data type #1684 (jonaprieto)
- Convert Nat literals to Core integers #1681 (lukaszcz)
- Less verbose output from running
make check
#1675 (jonaprieto) - Remove where syntax #1674 (jonaprieto)
- Benchmarks #1673 (janmasrovira)
- JuvixCore to JuvixAsm translation #1665 (lukaszcz)
v0.2.8 (2022-12-20)
Implemented enhancements:
- Support basic dependencies #1622 (janmasrovira)
Merged pull requests:
- Refactor hie.yaml and add entry in the readme #1672 (janmasrovira)
- Fix inline monospace formatted text in README #1671 (paulcadman)
- Pin mdbook to version 0.4.22 in docs build #1670 (paulcadman)
- Add option to specify Core transformations to
dev internal core-eval
#1669 (paulcadman) - Revert "Ignore binaries generated by running some tests" #1668 (jonaprieto)
- Add configuration files so the project can be built with cabal #1667 (paulcadman)
- Add documentation for compiling/running the TicTacToe example #1664 (paulcadman)
- Ignore binaries generated by running some tests #1663 (jonaprieto)
- Conversion of Nat representation to JuvixCore integers #1661 (lukaszcz)
- Move applications inside Lets and Cases #1659 (lukaszcz)
- Run shelltests on macOS build #1658 (paulcadman)
- Restore macOS CI build/test #1657 (paulcadman)
- Remove type arguments and type abstractions from Nodes #1655 (lukaszcz)
- Pretty printing of JuvixAsm code #1650 (lukaszcz)
- Remove NameId from Core #1649 (lukaszcz)
- Translation from JuvixAsm to C #1619 (lukaszcz)
v0.2.7 (2022-12-05)
Implemented enhancements:
- Add juvix-repl-mode for emacs #1612 (paulcadman)
- Make lambda lifting correct when free variables occur in the types of binders #1609 (janmasrovira)
Merged pull requests:
- Files pure refactor #1652 (janmasrovira)
- Use the same stack version in all CI jobs and remove
stack setup
step #1651 (paulcadman) - Fix 'not a primitive type' error message #1648 (lukaszcz)
- Upgrade stack snapshot to use ghc-9.2.5 #1621 (janmasrovira)
- Add an emacs function to restart the REPL #1618 (paulcadman)
- Add types to Core functions and constructors when translating from Internal #1617 (paulcadman)
- Auto complete argument of 'dev core read -t' #1616 (janmasrovira)
- Compute new entrypoint root when loading a file in the REPL #1615 (paulcadman)
- Compute maximum runtime stack height in JuvixReg #1613 (lukaszcz)
- Remove shelltest threading #1611 (paulcadman)
- Use StackInfo and recurseS in the JuvixAsm to JuvixReg translation. #1610 (lukaszcz)
- Precompute maximum heap allocation #1608 (lukaszcz)
- Improvements to Juvix REPL #1607 (paulcadman)
- Fix discrepancy between Juvix and WASM pages #1605 (lukaszcz)
- Compute JuvixAsm stack usage info #1604 (lukaszcz)
- Improve As-Pattern parsing #1603 (ii8)
- Juvix core recursors should descend into nodes stored in infos #1600 (janmasrovira)
- Add docs for installing the linux binary #1599 (paulcadman)
- Binder refactor #1598 (janmasrovira)
- Juvix C runtime #1580 (lukaszcz)
- As-patterns #1576 (ii8)
- Eta expansion at the top of each core function definition (#1481) #1571 (janmasrovira)
- Add translation from Internal to Core #1567 (paulcadman)
v0.2.6 (2022-10-26)
Implemented enhancements:
- Support go to definition for the standard library #1592 (paulcadman)
- Add builtin if #1585 (paulcadman)
- Add builtin boolean #1582 (paulcadman)
- Add lambda expressions to internal and add typechecking support #1538 (janmasrovira)
Fixed bugs:
- Fix arity checker bug #1546 (janmasrovira)
- Look in patterns when building the dependency graph #1536 (janmasrovira)
Merged pull requests:
- Update language reference to match current state of Juvix #1594 (paulcadman)
- Fix letrec printing #1591 (janmasrovira)
- Update stdlib submodule with builtin changes #1589 (paulcadman)
- Rename builtin natural to nat and boolean to bool #1588 (paulcadman)
- Improve the test for eta-expansion of constructors and builtins #1583 (lukaszcz)
- Properly newline expressions in the pretty printer #1581 (janmasrovira)
- Letrec lifting #1579 (janmasrovira)
- Add softlines between applications and hang definitions #1578 (janmasrovira)
- Parse optional type info in JVC files #1575 (lukaszcz)
- Fix symbol numbering bug #1574 (lukaszcz)
- 1569 rewrite the test for lambda lifting to use evaluation #1572 (janmasrovira)
- Remove lambda from reservedSymbols #1568 (lukaszcz)
- Keywords refactor #1566 (janmasrovira)
- remove ≔ from the language and replace it by := #1563 (janmasrovira)
- JuvixReg #1551 (lukaszcz)
- Remove duplicate function in concrete analysis #1550 (ii8)
- Evaluator minor style refactor #1547 (janmasrovira)
- Properly handle top lambdas in the termination checker #1544 (janmasrovira)
- Mutual inference #1543 (janmasrovira)
- Autocomplete ".jvc" input files for core {eval, read} commands #1542 (paulcadman)
- Add –show-de-bruijn to
core eval
command #1540 (paulcadman) - Inductive types should depend on the types of their constructors #1537 (lukaszcz)
- Parser labels #1535 (janmasrovira)
- JuvixAsm #1432 (lukaszcz)
v0.2.5 (2022-09-14)
Fixed bugs:
- Properly type check patterns that need normalization #1472 (janmasrovira)
- Detect nested patterns as smaller in the termination checker #1524
- Fix developBeta in Core/Extra.hs #1487 (lukaszcz)
- Core/Extra/Recursors/Collector bugfix #1510 (lukaszcz)
Merged pull requests:
- Replace -> by := in lambda syntax #1533 (janmasrovira)
- 'Match' with complex patterns in Core #1530 (lukaszcz)
- Refactor CLI #1527 (janmasrovira)
- Add CanonicalProjection #1526 (janmasrovira)
- Make comma a delimiter #1525 (lukaszcz)
- Detect nested patterns as smaller in the termination checker #1524 (janmasrovira)
- Disallow tab characters as spaces #1523 (janmasrovira)
- Refactor
destruct
in Core/Extra/Base #1522 (lukaszcz) - JuvixCore primitive types #1521 (lukaszcz)
- Enable autocompletion for the –theme flag #1519 (janmasrovira)
- Stripped version of Core Node datatype #1518 (lukaszcz)
- Add
internal core read
command #1517 (janmasrovira) - Implement some instances for BinderList #1515 (janmasrovira)
- Back recursor types with type families #1514 (janmasrovira)
- Eager evaluation of Constr arguments #1513 (lukaszcz)
- Dynamic type in Core #1508 (lukaszcz)
- LetRec in Core #1507 (lukaszcz)
- Add Haddock and Agda licenses #1506 (janmasrovira)
- Fix docs webapp examples CI build #1505 (paulcadman)
- Add CLI usage examples doc and integrate with README #1504 (paulcadman)
- Refactor BinderInfo #1503 (lukaszcz)
- Make
juvix compile
default to native target #1502 (paulcadman) - Refactor Node datatype #1501 (lukaszcz)
- Clean up import list in Pipeline #1499 (jonaprieto)
- Remove mono #1497 (jonaprieto)
- Remove Haskell support #1496 (jonaprieto)
- Implement lambda lifting #1494 (janmasrovira)
- Document Emacs installation and the 'exec-path' problem #1493 (lukaszcz)
- Add –allow-different-user to workflow stack command #1492 (paulcadman)
- Stack with github actions permissions workaround #1490 (paulcadman)
- Restructure recursors and add some lens interfaces #1489 (janmasrovira)
- Add a github action to build a static linux binary #1488 (paulcadman)
- Fix developBeta in Core/Extra.hs #1487 (lukaszcz)
- Add an option to show name ids in errors #1486 (lukaszcz)
v0.2.4 (2022-08-19)
(Special version for Heliax's retreat in Italy)
Implemented enhancements:
- Add –stdin flag #1459 (janmasrovira)
Fixed bugs:
- Fix typechecker #1458 (janmasrovira)
Merged pull requests:
- use –stdin in flycheck mode #1460 (janmasrovira)
- Add a native compile target for demos #1457 (paulcadman)
- Small changes for the presentation #1456 (jonaprieto)
- Fixes TicTacToe Web example #1454 (paulcadman)
- Upgrade to ghc-9.2.4 #1451 (janmasrovira)
v0.2.3 (2022-08-15)
Implemented enhancements:
- add
name
andversion
tojuvix.yaml
#1422 (janmasrovira)
Fixed bugs:
- Properly handle paragraphs in judoc #1447 (janmasrovira)
Merged pull requests:
- Give a proper type to literal natural numbers #1453 (janmasrovira)
- Add the option to output json in the
juvix internal highlight
command #1450 (janmasrovira) for supporting the new Juvix Mode for Visual Studio Code (jonaprieto) - Allow _ in Wasm exported names to support Anoma signature #1449 (paulcadman)
- Add Towers of Hanoi and Pascal triangle examples #1446 (paulcadman)
- Add
juvix init
command #1445 (janmasrovira) - Refactor pretty to reduce duplication #1443 (janmasrovira)
- Add initial support for examples in Html documentation #1442 (janmasrovira)
- Add revisions to README #1440 (jonaprieto)
- CI: Run build on push to main #1437 (paulcadman)
- Add doctor subcommand #1436 (paulcadman)
- CI checkout repo before cache and use recommended cache strategy #1435 (paulcadman)
- Various documentation adjustments #1434 (paulcadman)
- Setup Clang before building docs in CI #1433 (paulcadman)
- Major revisions to Makefile #1431 (jonaprieto)
- Do not add
-src
suffix to links in HTML when runningjuvix html
#1429 (paulcadman) - Add a Web version of TicTacToe #1427 (paulcadman)
- WASM import all non-compile axioms with alphanum names in entrypoint #1426 (paulcadman)
- Export all functions with alpha numeric names from entrypoint module #1425 (paulcadman)
- Refactor #1420 (jonaprieto)
- Permit axiom without a compile block #1418 (paulcadman)
- Implement an html documentation generator similar to haddock (#1413) #1416 (janmasrovira)
- Fix version shell test for 0.2.2 #1415 (paulcadman)
- Remove Int from stdlib and update SimpleFungibleToken example #1414 (paulcadman)
v0.2.2 (2022-07-25)
Implemented enhancements:
- Compute name dependency graph and filter unreachable definitions #1408 (lukaszcz)
- Support type aliases #1404 (janmasrovira)
- Add debugging custom function to Prelude #1401 (jonaprieto)
- Add positivity check for data types #1393 (jonaprieto)
- Keep qualified names #1392 (janmasrovira)
- Direct translation from MicroJuvix to MiniC #1386 (lukaszcz)
- Widens the accepted symbol list #1385 (mariari)
- Check all the type parameter names are different when declaring an inductive type #1377 (jonaprieto)
Fixed bugs:
- Curly braces are allowed nested in patterns #1380 (janmasrovira)
Merged pull requests:
- Add
Fail
effect (#1409) #1411 (janmasrovira) - Refactor of typechecking and other checking processes #1410 (jonaprieto)
- Use bold for code in scoper error messages #1403 (janmasrovira)
- Replace ppSimple by text #1402 (jonaprieto)
- Implement some error messages (#1396) #1400 (lukaszcz)
- Refactor childs of pattern parentheses and braces #1398 (janmasrovira)
- Update Juvix standard-library #1389 (jonaprieto)
- Fix documentation generation #1387 (jonaprieto)
- Adds Collatz sequence generator example #1384 (paulcadman)
- html-examples #1381 (jonaprieto)
- Refine hole in type signature to function type #1379 (janmasrovira)
- Type checking fails when the type of a pattern is not given by the signature #1378 (janmasrovira)
- Set cname for gh-pages action #1376 (paulcadman)
- Add fibonacci sequence example program #1375 (paulcadman)
- Fix Changelog links and minors #1371 (jonaprieto)
- Add Version number to the emacs mode #1320 (mariari)
New name: Juvix
Since version 0.2.2, the project has been renamed from "Mini Juvix" to "Juvix". The new name reflects the fact that the project is no longer just a compiler for a subset of Juvix, but a full implementation of the language. Affected by this change are:
- Github repository moved from the Heliax organization to the Anoma organization. "anoma/juvix" is the new repository name.
- All references to "Mini Juvix" have been replaced with "Juvix". Unfortunetly,
due to the move, the old links to the Mini Juvix repository are broken and will not be fixed.
v0.2.1 (2022-07-12)
Implemented enhancements:
- Specialize commands of/for internal use MiniJuvix-#270 (jonaprieto)
- Improve handling of location information for different objs MiniJuvix-#263 (jonaprieto)
- Add issues and PR templates MiniJuvix-#261 (jonaprieto)
- Throw error when reading a file that conflicts with embedded stdlib MiniJuvix-#243 (paulcadman)
- Embed standard library in the minijuvix binary MiniJuvix-#210 (paulcadman)
Fixed bugs:
- Fixed a bug with the path to walloc.c MiniJuvix-#237 (lukaszcz)
- Perform ScopedToAbstract exactly once for each module MiniJuvix-#223 (paulcadman)
Merged pull requests:
- Label renaming MiniJuvix-#275 (jonaprieto)
- Update link to discord MiniJuvix-#264 (Romainua)
- Include
open import
statements when generating HTML MiniJuvix-#260 (paulcadman) - Renaming MiniJuvix to Juvix MiniJuvix-#259 (jonaprieto)
- Updates tests to use the updated standard library MiniJuvix-#253 (paulcadman)
- Enforce C99 standard in the generated C files MiniJuvix-#252 (lukaszcz)
- Restore mascot images to the minijuvix book MiniJuvix-#250 (paulcadman)
- Allow jumping to another module in emacs MiniJuvix-#249 (janmasrovira)
- Restore Juvix mascot image to README MiniJuvix-#248 (paulcadman)
- Add emacs option
minijuvix-disable-embedded-stdlib
MiniJuvix-#247 (paulcadman) - Deprecate GHC backend MiniJuvix-#244 (lukaszcz)
- Removed 'eval' and 'print' keywords (#214) MiniJuvix-#242 (lukaszcz)
- Add option to disable minijuvix input method MiniJuvix-#239 (janmasrovira)
- Remove the 'match' keyword MiniJuvix-#238 (lukaszcz)
- Removed tests/positive/HelloWorld.mjuvix and specified clang version in the documentation MiniJuvix-#236 (lukaszcz)
- Filter symbol entries properly in the scoper MiniJuvix-#234 (janmasrovira)
- Use the ModulesCache for
open
statements in ScopedToAbstract pass MiniJuvix-#224 (paulcadman) - README: Include
--recursive
in git clone command to fetch stdlib MiniJuvix-#211 (paulcadman) - Update project description v0.2.0 MiniJuvix-#209 (jonaprieto)
- Unify AST representation of types and expressions in MicroJuvix MiniJuvix-#188 (janmasrovira)
v0.2.0 (2022-06-28)
Implemented enhancements:
- Support built in types MiniJuvix-#192 (janmasrovira)
- Support partial application and closure passing in C backend MiniJuvix-#190 (paulcadman)
- Allow
open import
statements MiniJuvix-#175 (janmasrovira) - Remove TypeAny and adapt typechecking for literals MiniJuvix-#173 (janmasrovira)
- Allow holes to be refined into function types MiniJuvix-#165 (janmasrovira)
- Support implicit arguments MiniJuvix-#144 (janmasrovira)
- Add support for holes in type signatures MiniJuvix-#141 (janmasrovira)
- Support function closures with no environment in minic MiniJuvix-#137 (paulcadman)
- Add holes for expressions in function clauses and inference support MiniJuvix-#136 (janmasrovira)
- Add "-Oz" optimization flag to clang args MiniJuvix-#133 (paulcadman)
- Add version and help option and root command to the CLI MiniJuvix-#131 (jonaprieto)
Fixed bugs:
- Fix: Ignore implicit patterns and arguments in termination checking MiniJuvix-#172 (janmasrovira)
- Fix: pretty printing for terminating keyword MiniJuvix-#145 (jonaprieto)
Merged pull requests:
- Fix: proper error handling for typechecker errors MiniJuvix-#189 (jonaprieto)
- Add juvix version info and date to HTML output MiniJuvix-#186 (jonaprieto)
- Fix: Add check for constructor return types MiniJuvix-#182 (jonaprieto)
- Use Abstract name in Abstract syntax and Micro/MonoJuvix MiniJuvix-#181 (janmasrovira)
- Add an option to specify the path where to put the HTML output MiniJuvix-#179 (jonaprieto)
- Upgrade to ghc-9.2.3 MiniJuvix-#178 (janmasrovira)
- Replace dead link in README with a link to the Juvix book MiniJuvix-#177 (paulcadman)
- Embed HTML assets in the juvix binary MiniJuvix-#176 (paulcadman)
- Fix: identifiers with a keyword prefix cannot be parsed MiniJuvix-#171 (janmasrovira)
- Improve filepath equality MiniJuvix-#170 (janmasrovira)
- Update validity predicate milestone example to 0.2 syntax MiniJuvix-#167 (paulcadman)
- Fix links in documentation and update to new syntax MiniJuvix-#163 (paulcadman)
- Update stdlib to work with version 0.2 MiniJuvix-#160 (janmasrovira)
- Update README usage example to use the compile command MiniJuvix-#158 (paulcadman)
- Remove dead code related to the pipeline MiniJuvix-#156 (janmasrovira)
- Add negative test for AppLeftImplicit MiniJuvix-#154 (janmasrovira)
- Add positive test designed for implicit arguments MiniJuvix-#153 (janmasrovira)
- Remove ExpressionTyped from MicroJuvix MiniJuvix-#143 (janmasrovira)
- Revision for package.yaml and minor deletions MiniJuvix-#135 (jonaprieto)
v0.1.4 (2022-05-30)
Merged pull requests:
- Generic Errors and refactoring MiniJuvix-#123 (jonaprieto)
- Only generates docs if the pull request merges MiniJuvix-#121 (jonaprieto)
- Add initial docs generation website MiniJuvix-#119 (jonaprieto)
- Fix internal link in README MiniJuvix-#116 (paulcadman)
- Add minic-runtime for linking without libc MiniJuvix-#113 (paulcadman)
- Add termination checking to the pipeline MiniJuvix-#111 (jonaprieto)
- Support uncurried higher order functions MiniJuvix-#110 (paulcadman)
- Improve error generation and handling MiniJuvix-#108 (janmasrovira)
- Add MiniC tests with clang+wasi-sdk MiniJuvix-#105 (paulcadman)
- Add usage example and move developer docs MiniJuvix-#96 (paulcadman)
- Refactor warning related stuff MiniJuvix-#91 (janmasrovira)
- Remove Agda backend MiniJuvix-#86 (paulcadman)
Implemented enhancements:
- Add
compile
subcommand to generate binaries MiniJuvix-#128 - Add intervals to flycheck errors MiniJuvix-#124
- Improve error handling in juvix-mode MiniJuvix-#107
- Support multiple modules in compilation MiniJuvix-#93
- Add compile command to CLI MiniJuvix-#130 (paulcadman)
- Use Interval in GenericErrors MiniJuvix-#125 (janmasrovira)
- Remove dev in the CI and other tweaks MiniJuvix-#118 (jonaprieto)
- Highlight comments correctly MiniJuvix-#106 (janmasrovira)
- Support multiple modules in compilation MiniJuvix-#100 (janmasrovira)
- New target syntax and modular VP examples MiniJuvix-#92 (jonaprieto)
Fixed bugs:
- Missing error messages when using throw/error MiniJuvix-#117
- Fix highlight of comments MiniJuvix-#104
- Fix juvix-mode coloring for projects with multiple modules MiniJuvix-#101
- Fix
highlight
command for modules with import statements MiniJuvix-#102 (janmasrovira)
Closed issues:
- Deprecate the class JuvixError MiniJuvix-#115
- Add ToGenericError instance for the infix parsing errors MiniJuvix-#114
- Compile to WASM without linking libc MiniJuvix-#112
- Add the termination checker to the pipeline MiniJuvix-#109
- Use clang + wasi-sdk instead of emcc to compile to WASM MiniJuvix-#103
- Move developer tooling docs out of README MiniJuvix-#95
- Add pre-commit checks to CI checks MiniJuvix-#94
- Support higher order functions in C backend MiniJuvix-#90
- Remove dev from the list of branches in the CI MiniJuvix-#89
- Refactor warning related stuff MiniJuvix-#87
- The Juvix website MiniJuvix-#51
v0.1.3 (2022-05-05)
Closed issues:
- Monomorphisation naming inconsistency MiniJuvix-#84
- Remove BackendAgda MiniJuvix-#83
- Change terminating keyword behavior MiniJuvix-#81
- MonoJuvix
ExpressionTyped
is never used MiniJuvix-#79 - Bump stackage nightly and delete
allow-newer: true
fromstack.yaml
MiniJuvix-#75 - Generate automatically CHANGELOG and Github Release Notes MiniJuvix-#73
- Make flag –show-name-ids global MiniJuvix-#61
- Add C code generation backend MiniJuvix-#60
- Add polymorphism MiniJuvix-#59
- Add the compile keyword to the frontend syntax (support up to Scoping) MiniJuvix-#58
- Error with undefined or underscores MiniJuvix-#54
- Add support for other GHC and Stack stable version MiniJuvix-#52
- Autodetect output ANSI support when prettyprinting MiniJuvix-#38
- Terminating for type signatures MiniJuvix-#11
Merged pull requests:
- Remove agda backend MiniJuvix-#86 (paulcadman)
- 84 monomorphisation naming inconsistency MiniJuvix-#85 (janmasrovira)
- Change terminating keyword behavior MiniJuvix-#82 (jonaprieto)
- Remove unused constructor ExpressionTyped in Monojuvix MiniJuvix-#80 (janmasrovira)
- Stricter stack builds and pedantic mode for CI MiniJuvix-#78 (jonaprieto)
- Bump stackage version and remove allow-newer MiniJuvix-#76 (janmasrovira)
- Add automatically updates/issues/merged PRs to the changelog MiniJuvix-#74 (jonaprieto)
- Add terminating keyword MiniJuvix-#71 (jonaprieto)
- Monomorphization MiniJuvix-#70 (janmasrovira)
- Remove StatementCompile in AST after scoping MiniJuvix-#69 (paulcadman)
- Add C code generation backend MiniJuvix-#68 (paulcadman)
- Check if stderr supports ANSI and print accordingly MiniJuvix-#67 (janmasrovira)
- Add support for compile (by Jonathan) MiniJuvix-#66 (paulcadman)
- Add NameIdGen effect to the pipeline MiniJuvix-#64 (janmasrovira)
- Make the
--show-name-ids
flag global MiniJuvix-#63 (janmasrovira) - Implement type checker with polymorphism MiniJuvix-#62 (janmasrovira)
v0.1.2 (2022-04-11)
Closed issues:
- Add en emacs mode with support for scoped highlighting MiniJuvix-#25
- Add support for project root detection through a juvix.yaml file MiniJuvix-#24
- Add CLI cmd to generate juvix autocompletion files for fish and zsh MiniJuvix-#23
- Add pretty and typecheck subcommands to the microjuvix CLI MiniJuvix-#21
- Translate identifiers from MicroJuvix to MiniHaskell (valid Haskell) MiniJuvix-#19
- Implement the MiniHaskell to Haskell translation (prettyprinter) MiniJuvix-#18
- Implementation of a typechecker for MicroJuvix MiniJuvix-#16
- Add references to the Abstract AST to update compilation to MiniHaskell MiniJuvix-#12
- Order in the house MiniJuvix-#10
Merged pull requests:
- The Juvix project now follows the same goals as the original Juvix project. MiniJuvix-#7 (jonaprieto)
- Dev→main MiniJuvix-#6 (jonaprieto)
- Big update including termination checking MiniJuvix-#5 (janmasrovira)
- Parser and scoper MiniJuvix-#3 (jonaprieto)
- Upgrade to ghc9 and use hpack MiniJuvix-#2 (janmasrovira)
- Merge MiniJuvix-#1 (jonaprieto)
v0.1.1 (2022-03-25)
- Add support in the parser/scoper for Axiom backends
- Add support for
foreign
keyword - Add flag
--no-colors
for the scope command - Upgrade to GHC 9.2.2
- Improve resolution of local symbols in the scoper
- Several new tests related to ambiguous symbols
- Add
--version
flag - Add InfoTableBuilder effect for the scoper
Closed issues:
- Add diff output to the test suite MiniJuvix-#9
- Improve scoper ambiguity error messages MiniJuvix-#8
Quick Start
To install Juvix, follow the instructions in the Installation How-to.
After installation, run juvix --help
to see the list of commands.
Run Juvix doctor to check your system setup:
juvix doctor
CLI Usage Examples
Create a new package:
juvix init
Compile a source file into an executable:
juvix compile path/to/source.juvix
Compile a source file into a WebAssembly binary:
juvix compile -t wasm path/to/source.juvix
Launch the REPL:
juvix repl
Typecheck a source file:
juvix typecheck path/to/source.juvix
Generate HTML representations of a source file and its imports:
juvix html --recursive path/to/source.juvix
The Hello World example
This is the Juvix source code of the traditional Hello World program.
-- HelloWorld.juvix
module HelloWorld;
open import Stdlib.Prelude;
main : IO;
main := printStringLn "hello world!";
end;
To compile and run a binary generated by Juvix, save the source code to
a file called HelloWorld.juvix
and run the following command from the
directory containing it:
juvix compile HelloWorld.juvix
./HelloWorld
You should see the output: hello world!
The source code can also be compiled to a WebAssembly binary. This
requires some additional setup. See the Installation
How-to for more
information. You can also run juvix doctor
to check your setup.
juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasm
Juvix tutorial
NOTE: This is a tutorial for Juvix version 0.3. Earlier versions do not support all the syntax described here.
- Juvix REPL
- Basic expressions
- Files, modules and compilation
- Output
- Data types and functions
- Pattern matching
- Comparisons and conditionals
- Local definitions
- Recursion
- Partial application and higher-order functions
- Polymorphism
- Tail recursion
- Totality checking
- Exercises
Juvix REPL
After installing Juvix, launch the Juvix REPL:
juvix repl
The response should be similar to:
Juvix REPL version 0.3: https://juvix.org. Run :help for help
OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
Stdlib.Prelude>
Currently, the REPL supports evaluating expressions but it does not yet
support adding new definitions. To see the list of available REPL
commands type :help
.
Basic expressions
You can try evaluating simple arithmetic expressions in the REPL:
Stdlib.Prelude> 3 + 4
7
Stdlib.Prelude> 1 + 3 * 7
22
Stdlib.Prelude> div 35 4
8
Stdlib.Prelude> mod 35 4
3
Stdlib.Prelude> sub 35 4
31
Stdlib.Prelude> sub 4 35
0
By default, Juvix operates on non-negative natural numbers. Natural number
subtraction is implemented by the function sub
. Subtracting a bigger
natural number from a smaller one yields 0
.
You can also try boolean expressions
Stdlib.Prelude> true
true
Stdlib.Prelude> not true
false
Stdlib.Prelude> true && false
false
Stdlib.Prelude> true || false
true
Stdlib.Prelude> if true 1 0
1
and strings, pairs and lists:
Stdlib.Prelude> "Hello world!"
"Hello world!"
Stdlib.Prelude> (1, 2)
(1, 2)
Stdlib.Prelude> 1 :: 2 :: nil
1 :: 2 :: nil
In fact, you can use all functions and types from the Stdlib.Prelude module of the standard library, which is preloaded by default.
Stdlib.Prelude> length (1 :: 2 :: nil)
3
Stdlib.Prelude> null (1 :: 2 :: nil)
false
Stdlib.Prelude> swap (1, 2)
(2, 1)
Files, modules and compilation
Currently, the REPL does not support adding new definitions. To define
new functions or data types, you need to put them in a separate file and
either load the file in the REPL with :load file.juvix
or compile the
file to a binary executable with the shell command
juvix compile file.juvix
.
To conveniently edit Juvix files, an Emacs mode and a VSCode extension are available.
A Juvix file must declare a module whose name corresponds exactly to the
name of the file. For example, a file Hello.juvix
must declare a
module Hello
:
-- Hello world example. This is a comment.
module Hello;
-- Import the standard library prelude, including the function 'printStringLn'
open import Stdlib.Prelude;
main : IO;
main := printStringLn "Hello world!";
end;
A file compiled to an executable must define the zero-argument function
main
of type IO
which is evaluated when running the program.
Output
In addition to printStringLn
, the standard library includes the
functions printString
, printNat
, printNatLn
, printBool
,
printBoolLn
. The IO
computations can be sequenced with >>
, e.g.,
printNat 3 >> printString " + " >> printNatLn 4
has type IO
and when executed prints 3 + 4
followed by a newline.
The type IO
is the type of IO actions, i.e., of data structures
representing IO computations. The functions printString
, printNat
,
etc., do not immediately print their arguments, but rather create a data
structure representing an appropriate IO action. The IO actions created
by the main
function are executed only after the program has been
evaluated.
Data types and functions
To see the type of an expression, use the :type
REPL command:
Stdlib.Prelude> :type 1
Nat
Stdlib.Prelude> :type true
Bool
The types Nat
and Bool
are defined in the standard library.
The type Bool
has two constructors true
and false
.
type Bool :=
| true : Bool
| false : Bool;
The constructors of a data type can be used to build elements of the
type. They can also appear as patterns in function definitions. For
example, the not
function is defined in the standard library by:
not : Bool -> Bool;
not true := false;
not false := true;
The first line is the signature which specifies the type of the
definition. In this case, not
is a function from Bool
to Bool
. The
signature is followed by two function clauses which specify the
function result depending on the shape of the arguments. When a function
call is evaluated, the first clause that matches the arguments is used.
In contrast to languages like Python, Java or C/C++, Juvix doesn't
require parentheses for function calls. All the arguments are just
listed after the function. The general pattern for function application
is: func arg1 arg2 arg3 ...
A more complex example of a data type is the Nat
type from the
standard library:
type Nat :=
| zero : Nat
| suc : Nat -> Nat;
The constructor zero
represents 0
and suc
represents the successor
function – suc n
is the successor of n
, i.e., n+1
. For example,
suc zero
represents 1
. The number literals 0
, 1
, 2
, etc., are
just shorthands for appropriate expressions built using suc
and
zero
.
The constructors of a data type specify how the elements of the type can
be constructed. For instance, the above definition specifies that an
element of Nat
is either:
zero
, orsuc n
wheren
is an element ofNat
, i.e., it is constructed by applyingsuc
to appropriate arguments (in this case the argument ofsuc
has typeNat
).
Any element of Nat
can be built with the constructors in this way –
there are no other elements. Mathematically, this is an inductive
definition, which is why the data type is called inductive.
If implemented directly, the above unary representation of natural
numbers would be extremely inefficient. The Juvix compiler uses a binary
number representation under the hood and implements arithmetic
operations using corresponding machine instructions, so the performance
of natural number arithmetic is similar to other programming languages.
The Nat
type is a high-level presentation of natural numbers as seen
by the user who does not need to worry about low-level arithmetic
implementation details.
One can use zero
and suc
in pattern matching, like any other
constructors:
infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
The infixl 6 +
declares +
to be an infix left-associative operator
with priority 6. The +
is an ordinary function, except that function
application for +
is written in infix notation. The definitions of the
clauses of +
still need the prefix notation on the left-hand sides.
The a
and b
in the patterns on the left-hand sides of the clauses
are variables which match arbitrary values of the corresponding type.
They can be used on the right-hand side to refer to the values matched.
For example, when evaluating
(suc (suc zero)) + zero
the second clause of +
matches, assigning suc zero
to a
and zero
to b
. Then the right-hand side of the clause is evaluated with a
and
b
substituted by these values:
suc (suc zero + zero)
Again, the second clause matches, now with both a
and b
being
zero
. After replacing with the right-hand side, we obtain:
suc (suc (zero + zero))
Now the first clause matches and finally we obtain the result
suc (suc zero)
which is just 2
.
The function +
is defined like above in the standard library, but the
Juvix compiler treats it specially and generates efficient code using
appropriate CPU instructions.
Pattern matching
The patterns in function clauses do not have to match on a single constructor – they may be arbitrarily deep. For example, here is an (inefficient) implementation of a function which checks whether a natural number is even:
even : Nat -> Bool;
even zero := true;
even (suc zero) := false;
even (suc (suc n)) := even n;
This definition states that a natural number n
is even if either n
is zero
or, recursively, n-2
is even.
If a subpattern is to be ignored, then one can use a wildcard _
instead of naming the subpattern.
isPositive : Nat -> Bool;
isPositive zero := false;
isPositive (suc _) := true;
The above function could also be written as:
isPositive : Nat -> Bool;
isPositive zero := false;
isPositive _ := true;
It is not necessary to define a separate function to perform pattern
matching. One can use the case
syntax to pattern match an expression
directly.
Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
1
Comparisons and conditionals
To use the comparison operators on natural numbers, one needs to import
the Stdlib.Data.Nat.Ord
module. The comparison operators are not in
Stdlib.Prelude
to avoid clashes with user-defined operators for other
data types. The functions available in Stdlib.Data.Nat.Org
include:
<
, <=
, >
, >=
, ==
, /=
, min
, max
.
For example, one may define the function max3
by:
open import Stdlib.Data.Nat.Ord;
max3 : Nat -> Nat -> Nat -> Nat;
max3 x y z := if (x > y) (max x z) (max y z);
The conditional if
is a special function which is evaluated lazily,
i.e., first the condition (the first argument) is evaluated, and then
depending on its truth-value one of the branches (the second or the
third argument) is evaluated and returned.
By default, evaluation in Juvix is eager (or strict), meaning that
the arguments to a function are fully evaluated before applying the
function. Only if
, ||
and &&
are treated specially and evaluated
lazily. These special functions cannot be partially applied (see
Partial application and higher-order
functions
below).
Local definitions
Juvix supports local definitions with let-expressions.
f : Nat -> Nat;
f a := let x : Nat := a + 5;
y : Nat := a * 7 + x
in
x * y;
The variables x
and y
are not visible outside f
.
One can also use multi-clause definitions in let
-expressions, with the
same syntax as definitions inside a module. For example:
even' : Nat -> Bool;
even' :=
let
even : Nat -> Bool;
odd : Nat -> Bool;
even zero := true;
even (suc n) := odd n;
odd zero := false;
odd (suc n) := even n;
in
even
The functions even
and odd
are not visible outside even'
.
Recursion
Juvix is a purely functional language, which means that functions have no side effects and all variables are immutable. An advantage of functional programming is that all expressions are referentially transparent – any expression can be replaced by its value without changing the meaning of the program. This makes it easier to reason about programs, in particular to prove their correctness. No errors involving implicit state are possible, because the state is always explicit.
In a functional language, there are no imperative loops. Repetition is expressed using recursion. In many cases, the recursive definition of a function follows the inductive definition of a data structure the function analyses. For example, consider the following inductive type of lists of natural numbers:
type NList :=
| nnil : NList
| ncons : Nat -> NList -> NList;
An element of NList
is either nnil
(empty) or ncons x xs
where
x : Nat
and xs : NList
(a list with head x
and tail xs
).
A function computing the length of a list may be defined by:
nlength : NList -> Nat;
nlength nnil := 0;
nlength (ncons _ xs) := nlength xs + 1;
The definition follows the inductive definition of NList
. There are
two function clauses for the two constructors. The case for nnil
is
easy – the constructor has no arguments and the length of the empty list
is 0
. For a constructor with some arguments, one typically needs to
express the result of the function in terms of the constructor
arguments, usually calling the function recursively on the constructor's
inductive arguments (for ncons
this is the second argument). In the
case of ncons _ xs
, we recursively call nlength
on xs
and add 1
to the result.
Let's consider another example – a function which returns the maximum of the numbers in a list or 0 for the empty list.
open import Stdlib.Data.Nat.Ord; -- for `max`
nmaximum : NList -> Nat;
nmaximum nnil := 0;
nmaximum (ncons x xs) := max x (nmaximum xs);
Again, there is a clause for each constructor. In the case for ncons
,
we recursively call the function on the list tail and take the maximum
of the result and the list head.
For an example of a constructor with more than one inductive argument, consider binary trees with natural numbers in nodes.
type Tree :=
| leaf : Nat -> Tree
| node : Nat -> Tree -> Tree -> Tree;
The constructor node
has two inductive arguments (the second and the
third) which represent the left and the right subtree.
A function which produces the mirror image of a tree may be defined by:
mirror : Tree -> Tree;
mirror (leaf x) := leaf x;
mirror (node x l r) := node x (mirror r) (mirror l);
The definition of mirror
follows the definition of Tree
. There are
two recursive calls for the two inductive constructors of node
(the
subtrees).
Partial application and higher-order functions
Strictly speaking, all Juvix functions have only one argument.
Multi-argument functions are really functions which return a function
which takes the next argument and returns a function taking another
argument, and so on for all arguments. The function type former ->
(the arrow) is right-associative. Hence, the type, e.g.,
Nat -> Nat -> Nat
when fully parenthesised becomes
Nat -> (Nat -> Nat)
. It is the type of functions which given an
argument of type Nat
return a function of type Nat -> Nat
which
itself takes an argument of type Nat
and produces a result of type
Nat
. Function application is left-associative. For example, f a b
when fully parenthesised becomes (f a) b
. So it is an application to
b
of the function obtained by applying f
to a
.
Since a multi-argument function is just a one-argument function
returning a function, it can be partially applied to a smaller number
of arguments than specified in its definition. The result is an
appropriate function. For example, sub 10
is a function which
subtracts its argument from 10
, and (+) 1
is a function which adds
1
to its argument. If the function has been declared as an infix
operator (like +
), then for partial application one needs to enclose
it in parentheses.
A function which takes a function as an argument is a higher-order
function. An example is the nmap
function which applies a given
function to each element in a list of natural numbers.
nmap : (Nat -> Nat) -> NList -> NList;
nmap _ nnil := nnil;
nmap f (ncons x xs) := ncons (f x) (nmap f xs);
The application
nmap \{ x := div x 2 } lst
divides every element of lst
by 2
, rounding down the result. The
expression
\{ x := div x 1 }
is an unnamed function, or a lambda, which divides its argument by
2
.
Polymorphism
The type NList
we have been working with above requires the list
elements to be natural numbers. It is possible to define lists
polymorphically, parameterising them by the element type. This is
analogous to generics in languages like Java, C++ or Rust. Here is the
polymorphic definition of lists from the standard library:
infixr 5 ::;
type List (A : Type) :=
| nil : List A
| :: : A -> List A -> List A;
The constructor ::
is declared as a right-associative infix operator
with priority 5. The definition has a parameter A
which is the element
type.
Now one can define the map
function polymorphically:
map : {A B : Type} -> (A -> B) -> List A -> List B;
map f nil := nil;
map f (h :: hs) := f h :: map f hs;
This function has two implicit type arguments A
and B
. These
arguments are normally omitted in function application – they are
inferred automatically during type checking. The curly braces indicate
that the argument is implicit and should be inferred.
In fact, the constructors nil
and ::
also have an implicit argument:
the type of list elements. All type parameters of a data type definition
become implicit arguments of the constructors.
Usually, the implicit arguments in a function application can be inferred. However, sometimes this is not possible and then the implicit arguments need to be provided explicitly by enclosing them in braces:
f {implArg1} .. {implArgK} arg1 .. argN
For example, nil {Nat}
has type List Nat
while nil
by itself has
type {A : Type} -> List A
.
Tail recursion
Any recursive call whose result is further processed by the calling
function needs to create a new stack frame to save the calling function
environment. This means that each such call will use a constant amount
of memory. For example, a function sum
implemented as follows will use
an additional amount of memory proportional to the length of the
processed list:
sum : NList -> Nat;
sum nnil := 0;
sum (ncons x xs) := x + sum xs;
This is not acceptable if you care about performance. In an imperative language, one would use a simple loop going over the list without any memory allocation. In pseudocode:
var sum : Nat := 0;
while (lst /= nnil) {
sum := sum + head lst;
lst := tail lst;
};
return sum;
Fortunately, it is possible to rewrite this function to use tail recursion. A recursive call is tail recursive if its result is also the result of the calling function, i.e., the calling function returns immediately after it without further processing. The Juvix compiler guarantees that all tail calls will be eliminated, i.e., that they will be compiled to simple jumps without extra memory allocation. In a tail recursive call, instead of creating a new stack frame, the old one is reused.
The following implementation of sum
uses tail recursion.
sum : NList -> Nat;
sum lst :=
let
go : Nat -> NList -> Nat;
go acc nnil := acc;
go acc (ncons x xs) := go (acc + x) xs;
in
go 0 lst;
The first argument of go
is an accumulator which holds the sum
computed so far. It is analogous to the sum
variable in the imperative
loop above. The initial value of the accumulator is 0. The function go
uses only constant additional memory overall. The code generated for it
by the Juvix compiler is equivalent to an imperative loop.
Most imperative loops may be translated into tail recursive functional
programs by converting the locally modified variables into accumulators
and the loop condition into pattern matching. For example, here is an
imperative pseudocode for computing the nth Fibonacci number in linear
time. The variables cur
and next
hold the last two computed
Fibonacci numbers.
var cur : Nat := 0;
var next : Nat := 1;
while (n /= 0) {
var tmp := next;
next := cur + next;
cur := tmp;
n := n - 1;
};
return cur;
An equivalent functional program is:
fib : Nat -> Nat;
fib :=
let go : Nat -> Nat -> Nat -> Nat;
go cur _ zero := cur;
go cur next (suc n) := go next (cur + next) n;
in
go 0 1;
A naive definition of the Fibonacci function runs in exponential time:
fib : Nat -> Nat;
fib zero := 0;
fib (suc zero) := 1;
fib (suc (suc n)) := fib n + fib (suc n);
Tail recursion is less useful when the function needs to allocate memory
anyway. For example, one could make the map
function from the previous
section tail recursive, but the time and memory use would still be
proportional to the length of the input because of the need to allocate
the result list.
Totality checking
By default, the Juvix compiler requires all functions to be total. Totality consists of:
The termination check ensures that all functions are structurally recursive, i.e., all recursive call are on structurally smaller value – subpatterns of the matched pattern. For example, the termination checker rejects the definition
fact : Nat -> Nat;
fact x := if (x == 0) 1 (x * fact (sub x 1));
because the recursive call is not on a subpattern of a pattern matched on in the clause. One can reformulate this definition so that it is accepted by the termination checker:
fact : Nat -> Nat;
fact zero := 1;
fact [email protected](suc n) := x * fact n;
Sometimes, such a reformulation is not possible. Then one can use the
terminating
keyword to forgoe the termination check.
terminating
log2 : Nat -> Nat;
log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
Coverage checking ensures that there are no unhandled patterns in
function clauses or case
expressions. For example, the following
definition is rejected because the case suc zero
is not handled:
even : Nat -> Bool;
even zero := true;
even (suc (suc n)) := even n;
NOTE: Coverage checking will be implemented only in Juvix version 0.4. Earlier versions of Juvix accept non-exhaustive patterns.
Exercises
You have now learnt the very basics of Juvix. To consolidate your understanding of Juvix and functional programming, try doing some of the following exercises. To learn how to write more complex Juvix programs, see the advanced tutorial and the Juvix program examples.
-
Define a function
prime : Nat -> Nat
which checks if a given natural number is prime. -
What is wrong with the following definition?
half : Nat -> Nat; half n := if (n < 2) 0 (half (n - 2) + 1);
How can you reformulate this definition so that it is accepted by Juvix?
-
Define a polymorphic function which computes the last element of a list. What is the result of your function on the empty list?
-
A suffix of a list
l
is any list which can be obtained froml
by removing some initial elements. For example, the suffixes of1 :: 2 :: 3 :: nil
are:1 :: 2 :: 3 :: nil
,2 :: 3 :: nil
,3 :: nil
andnil
.Define a function which computes the list of all suffixes of a given list in the order of decreasing length.
-
Recall the
Tree
type from above.type Tree := | leaf : Nat -> Tree | node : Nat -> Tree -> Tree -> Tree;
Analogously to the
map
function for lists, define a functiontmap : (Nat -> Nat) -> Tree -> Tree
which applies a function to all natural numbers stored in a tree.
-
Make the
Tree
type polymorphic in the element type and repeat the previous exercise. -
Write a tail recursive function which reverses a list.
-
Write a tail recursive function which computes the factorial of a natural number.
-
Define a function
comp : {A : Type} -> List (A -> A) -> A -> A
which composes all functions in a list. For example,comp (suc :: (*) 2 :: \{x := sub x 1} :: nil)
should be a function which given
x
computes2(x - 1) + 1
.
Juvix Emacs mode tutorial
First, follow the instructions in the Emacs Mode
Reference to install the Juvix Emacs
mode. Once you've successfully set it up, create a file Hello.juvix
with the following content.
module Hello;
open import Stdlib.Prelude;
main : IO;
main := printStringLn "Hello world!";
end;
Type C-c C-l
to run the scoper and highlight the syntax.
If you make a mistake in your program, it is automatically underlined in red with the error message popping up when you hover the mouse pointer over the underlined part.
For example, in the following program the identifier printStringLna
should be underlined with the error message "Symbol not in scope".
module Hello;
open import Stdlib.Prelude;
main : IO;
main := printStringLna "Hello world!";
end;
If error underlining doesn't work, make sure you have the flycheck
mode turned on. It should be turned on automatically when loading
juvix-mode
, but in case this doesn't work you can enable it with
M-x flycheck-mode
.
Let's extend our program with another definition.
module Hello;
open import Stdlib.Prelude;
print : IO;
print := printStringLn "Hello world!";
main : IO;
main := print;
end;
Place the cursor on the print
call in the function clause of main
and press M-.
. The cursor will jump to the definition of print
above. This also works across files and for definitions from the
standard library. You can try using M-.
to jump to the definition of
printStringLn
.
One more feature of the Juvix Emacs mode is code formatting. To format
the content of the current buffer, type C-c C-f
. Here is the result.
module Hello;
open import Stdlib.Prelude;
print : IO;
print := printStringLn "Hello world!";
main : IO;
main := print;
end;
Juvix VSCode extension tutorial
To install the Juvix VSCode extension, click on the "Extensions" button in the left panel and search for the "Juvix" extension by Heliax.
Once you've installed the Juvix extension, you can open a Juvix file.
For example, create a Hello.juvix
file with the following content.
module Hello;
open import Stdlib.Prelude;
main : IO;
main := printStringLn "Hello world!";
end;
Syntax should be automatically highlighted for any file with .juvix
extension. You can jump to the definition of an identifier by pressing
F12 or control-clicking it. To apply the Juvix code formatter to the
current file, use Shift+Ctrl+I.
In the top right-hand corner of the editor window you should see several buttons. Hover the mouse pointer over a button to see its description. The functions of the buttons are as follows.
- Load file in REPL (Shift+Alt+R). Launches the Juvix REPL in a separate window and loads the current file into it. You can then evaluate any definition from the loaded file.
- Typecheck (Shift+Alt+T). Type-checks the current file.
- Compile (Shift+Alt+C). Compiles the current file. The resulting native executable will be left in the directory of the file.
- Run (Shift+Alt+X). Compiles and runs the current file. The output of the executable run is displayed in a separate window.
- Html preview. Generates HTML documentation for the current file and displays it in a separate window.
Dependencies
You need Clang / LLVM version
13 or later. Note that on macOS the preinstalled clang does not support
the wasm target, so use e.g. brew install llvm
instead.
If you want to compile to WebAssembly, you also need:
- wasmer
- wasi-sdk
- wasm-ld - the LLVM linker for WASM (NB: On
Linux you may need to install the
lld
package; on macOS this is installed as part ofllvm
).
See below for instructions on how to install the dependencies.
Installing Juvix
MacOS
The easiest way to install Juvix on MacOS is by using Homebrew.
To install the homebrew-juvix tap, run:
brew tap anoma/juvix
To install Juvix, run:
brew install juvix
Helpful information can also be obtained by running:
brew info juvix
Linux x8664
A Juvix compiler binary executable for Linux x8664 is available on the Juvix release page.
To install this executable, download and unzip the linked file and move
it to a directory on your shell's PATH
.
For example if ~/.local/bin
is on your shell's PATH
, you can install
Juvix as follows:
cd /tmp
curl -OL https://github.com/anoma/juvix/releases/download/v0.3.0/juvix-linux_x86_64-v0.3.0.zip
unzip juvix-linux_x86_64-v0.3.0.zip
mv juvix-linux_x86_64-v0.3.0 ~/.local/bin/juvix
Building Juvix from source
To install Juvix from source you must clone the Github repository. Then Juvix can be installed with the following commands. We assume you have Stack and GNU Make installed.
git clone --recursive https://github.com/anoma/juvix.git
cd juvix
make install
The C compiler and linker paths can be specified as options to the
make install
command, e.g.
make install CC=path/to/clang LIBTOOL=path/to/llvm-ar
On MacOS, you can alternatively run the following command for Homebrew.
The flag --HEAD
used below is optional – use it to build the latest
version of Juvix in the main
branch on Github.
brew install --build-from-source --HEAD juvix --verbose
Building the project with cabal
We recommend to use the stack
build tool with this project.
If you prefer the cabal
build tool instead, then you need to generate
the juvix.cabal
file using hpack
before running cabal build
.
You also need to compile the runtime first:
make runtime
cabal build
Installing dependencies
To install wasi-sdk
you need to download libclang_rt
and
wasi-sysroot
precompiled archives from the wasi-sdk release
page and:
-
Extract the
libclang_rt.builtins-wasm32-wasi-*.tar.gz
archive in theclang
installation root (for example/usr/lib/clang/13
on Ubuntu or`brew --prefix llvm`
on macos).For example on macos with homebrew clang:
cd `brew --prefix llvm` curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/libclang_rt.builtins-wasm32-wasi-15.0.tar.gz -OL tar xf libclang_rt.builtins-wasm32-wasi-15.0.tar.gz
-
Extract the
wasi-sysroot-*.tar.gz
archive on your local system and setWASI_SYSROOT_PATH
to its path.For example:
cd ~ curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/wasi-sysroot-15.0.tar.gz -OL tar xf wasi-sysroot-15.0.tar.gz export WASI_SYSROOT_PATH=~/wasi-sysroot
Compiling simple programs
A Juvix file must declare a module whose name corresponds exactly to the
name of the file. For example, a file Hello.juvix
must declare a
module Hello
:
-- Hello world example. This is a comment.
module Hello;
-- Import the standard library prelude, including the function 'printStringLn'
open import Stdlib.Prelude;
main : IO;
main := printStringLn "Hello world!";
end;
A file compiled to an executable must define the zero-argument function
main
of type IO
which is evaluated when running the program.
To compile the file Hello.juvix
type juvix compile Hello.juvix
.
Typing juvix compile --help
will list all options to the compile
command.
Compilation targets
Since version 0.3 Juvix supports three compilation targets. The targets
are specified with the -t
option:
juvix compile -t target file.juvix
.
native
. This is the default. Produces a native 64bit executable for your machine.wasm32-wasi
. Produces a WebAssembly binary which uses the WASI runtime.geb
. Produces a GEB input file.
Juvix projects
A Juvix project is a collection of Juvix modules inside one main
project directory containing a juvix.yaml
metadata file. The name of
each module must coincide with the path of the file it is defined in,
relative to the project's root directory. For example, if the file is
root/Data/List.juvix
then the module must be called Data.List
,
assuming root
is the project's directory.
To check that Juvix is correctly detecting your project's root, you can
run the command juvix dev root File.juvix
.
See also: Modules Reference.
Documenting Juvix programs with Judoc
Type theory
Totality checking
Termination
To not bring inconsistencies by function declarations, Juvix requires that every function passes its termination checker. However, since this is a strong requirement, often tricky to fulfil, we give the user the possibility to skip this check in two different ways:
- Using the
terminating
keyword to annotate function type signatures as terminating. The syntax is the following.
terminating fun : A → B;
Note that annotating a function as terminating
means that all its
function clauses pass the termination checker's criterion. To skip the
termination checker for mutual recursive functions, all the functions
involved must be annotated as terminating
.
- Using the CLI global flag
--no-termination
.
juvix typecheck --no-termination MyProgram.juvix
In any case, be aware that our termination checker is limited as it only accepts a subset of recursion functions. The termination checker algorithm is a slight modification of the algorithm for checking termination in the Foetus's language.
Strictly positive data types
Coverage checking
The Juvix standard library contains common functions that can be used in Juvix programs.
Function declarations
A function declaration consists of a type signature and a group of function clauses.
In the following example, we define a function multiplyByTwo
. The
first line multiplyByTwo : Nat -> Nat;
is the type signature and the
second line multiplyByTwo n := 2 * n;
is a function clause.
open import Stdlib.Prelude;
multiplyByTwo : Nat -> Nat;
multiplyByTwo n := 2 * n;
A function may have more than one function clause. When a function is called, the first clause that matches the arguments is used.
The following function has two clauses.
open import Stdlib.Prelude;
neg : Bool -> Bool;
neg true := false;
neg false := true;
When neg
is called with true
, the first clause is used and the
function returns false
. Similarly, when neg
is called with false
,
the second clause is used and the function returns true
.
Mutually recursive functions
Function declarations can depend on each other recursively. In the
following example, we define a function that checks if a number is
even
by calling a function that checks if a number is odd
.
open import Stdlib.Prelude;
odd : Nat -> Bool;
even : Nat -> Bool;
odd zero := false;
odd (suc n) := even n;
even zero := true;
even (suc n) := odd n;
Anonymous functions
Anonymous functions, or lambdas, are introduced with the syntax:
\{| pat1 .. patN_1 := clause1
| ..
| pat1 .. patN_M := clauseM}
The first pipe |
is optional. Instead of \
one can also use λ
.
An anonymous function just lists all clauses of a function without naming it. Any function declaration can be converted to use anonymous functions:
open import Stdlib.Prelude;
odd : Nat -> Bool;
even : Nat -> Bool;
odd := \{
| zero := false
| (suc n) := even n
};
even := \{
| zero := true
| (suc n) := odd n
};
Short definitions
A function definition can be written in one line, with the body immediately following the signature:
multiplyByTwo : Nat -> Nat := \{n := 2 * n};
Data types
A data type declaration consists of:
- The
type
keyword, - a unique name for the type,
- the
:=
symbol, and - a non-empty list of constructor declarations (functions for building the elements of the data type).
The simplest data type is the Unit
type with one constructor called
unit
.
type Unit := unit : Unit;
In the following example, we declare the type Nat
– the unary
representation of natural numbers. This type comes with two
constructors: zero
and suc
. Example elements of type Nat
are the
number one represented by suc zero
, the number two represented by
suc (suc zero)
, etc.
type Nat :=
zero : Nat
| suc : Nat -> Nat;
Constructors can be used like normal functions or in patterns when defining functions by pattern matching. For example, here is a function adding two natural numbers:
infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
A data type may have type parameters. A data type with a type parameter
A
is called polymorphic in A
. A canonical example is the type
List
polymorphic in the type of list elements.
infixr 5 ::;
type List (A : Type) :=
nil : List A
| :: : A -> List A -> List A;
elem : {A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
elem _ _ nil := false;
elem eq s (x :: xs) := eq s x || elem eq s xs;
For more examples of inductive types and how to use them, see the Juvix standard library.
Module system
Defining a module
The module
keyword stars the declaration of a module followed by its
name and body. The module declaration ends with the end
keyword.
-- ModuleName.juvix
module ModuleName;
end;
A Juvix project is a collection of Juvix modules inside one main
project folder containing a metadata file named juvix.yaml
. Each Juvix
file has to define a module of the same name. The name of the
module must coincide with the path of the its file relative to its
project's root directory. For example, if the file is
root/Data/List.juvix
then the module must be called Data.List
,
assuming root
is the project's folder.
To check that Juvix is correctly detecting your project's root, one can
run the command juvix dev root File.juvix
.
Importing modules
To bring into the current scope all module definitions from other
external modules, one can use the import
keyword along with the
corresponding module name. This way, one gets all the imported names
qualified.
-- A.juvix
module A;
axiom Nat : Type;
axiom zero : Nat;
end;
-- B.juvix
module B;
import A;
x : A.Nat;
x := A.zero;
Additionally, one can open an imported module making available all its names by their unqualified name.
-- A.juvix
module A;
axiom Nat : Type;
axiom zero : Nat;
end;
-- B.juvix
module B;
import A;
open A;
x : Nat;
x := zero;
However, opening modules may create name collisions if you already have
the imported names as definitions in the current module. In this case,
Juvix will complain with an error, letting you know which symbols are
ambiguous. For example, in module B
below, the name a
is ambiguous.
-- A.juvix
module A;
axiom A : Type;
axiom a : A;
end;
-- B.juvix
module B;
import A;
open A;
axiom a : A;
x := a;
end;
One alternative here is hiding the name a
as follows.
-- B.juvix
module B;
import A;
open A hiding {a};
axiom a : A;
x := a;
end;
Now, we can use the open import
syntax to simplify the import-open
statements.
Instead of having:
import Prelude;
open Prelude;
We simplify it by the expression:
open import Prelude;
The hiding
keyword can be used within an open-import
statement.
-- B.juvix
module A;
open import A hiding {a};
axiom a : A;
x := a;
end;
Exporting symbols
The module C
below does not typecheck. Both symbols, originally
defined in module A
, are not visible in module C
after importing
B
. The symbols A
and a
are not exported by the module B
. To
export symbols from an imported module, one can use the public
keyword
at the end of the corresponding open
statement. For example, the
module C
typechecks after marking the import of A
as public
in
module B
.
-- A.juvix
module A;
axiom A : Type;
axiom a : A;
end;
-- B.juvix
module B;
open import A;
end;
-- C.juvix
module C;
open import B;
x : A;
x := a;
end;
Fix:
-- B.juvix
module B;
open import A public;
end;
Local definitions
Local definitions are introduced with the let
construct.
sum : NList -> Nat;
sum lst :=
let
go : Nat -> NList -> Nat;
go acc nnil := acc;
go acc (ncons x xs) := go (acc + x) xs;
in
go 0 lst;
The declaractions in a let
have the same syntax as declarations inside
a module, but they are visible only in the expression following the in
keyword.
Control structures
Case
A case expression has the following syntax:
case value
| pat1 := branch1
..
| patN := branchN
For example, one can evaluate the following expression in the REPL:
Stdlib.Prelude> case 2 | zero := 0 | suc x := x | _ := 19
1
Lazy builtins
The standard library provides several builtin functions which are treated specially and evaluated lazily. These builtins must always be fully applied.
if condition branch1 branch2
. First evaluatescondition
, if true evaluates and returnsbranch1
, otherwise evaluates and returnsbranch2
.a || b
. Lazy disjunction. First evaluatesa
, if true returns true, otherwise evaluates and returnsb
.a && b
. Lazy conjunction. First evaluatesa
, if false returns false, otherwise evaluates and returnsb
.a >> b
. Sequences two IO actions. Lazy in the second argument.
Comments
Comments follow the same syntax as in Haskell
and Agda
. Be aware,
Juvix has no support for nested comments.
- Inline Comment
-- This is a comment!
- Region comment
{-
This is a comment!
-}
Axiom
Axioms or postulates can be introduced by using the axiom
keyword. For
example, let us imagine one wants to write a program that assumes A is
a type, and there exists a term x that inhabits A. Then the program
would look like the following.
-- Example.juvix
module Example;
axiom A : Type;
axiom x : A;
end;
Terms introduced by the axiom
keyword lack any computational content.
Programs containing axioms not marked as builtins cannot be compiled to
most targets.
The following links are clickable versions of their corresponding Juvix
programs. The HTML output is generated by running
juvix html --recursive FileName.juvix
.
Benchmarks
CLI
Usage
juvix [Global options] ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CMD)
Informative options
-v,--version
Print the version and exit-h,--help
Show this help text
Global Command flags
--no-colors
Disable globally ANSI formatting--show-name-ids
Show the unique number of each identifier when pretty printing--only-errors
Only print errors in a uniform format (used by juvix-mode)--no-termination
Disable termination checking--no-positivity
Disable positivity checking for inductive types--no-stdlib
Do not use the standard library
Main Commands
html
Generate HTML output from a Juvix filetypecheck
Typecheck a Juvix filecompile
Compile a Juvix file
Utility Commands
doctor
Perform checks on your Juvix development environmentinit
Interactively initialize a juvix project in the current directory
Dev Commands
juvix dev COMMAND
parse
Parse a Juvix filescope
Parse and scope a Juvix filehighlight
Highlight a Juvix filecore
Subcommands related to JuvixCoreasm
Subcommands related to JuvixAsmroot
Show the root path for a Juvix projecttermination
Subcommands related to termination checkinginternal
Subcommands related to Internalminic
Translate a Juvix file to a subset of C
CLI Auto-completion Scripts
The Juvix CLI can generate auto-completion scripts. Follow the instructions below for your shell.
NB: You may need to restart your shell after installing the completion script.
Bash
Add the following line to your bash init script (for example
~/.bashrc
).
eval "$(juvix --bash-completion-script juvix)"
Fish
Run the following command in your shell:
juvix --fish-completion-script juvix
> ~/.config/fish/completions/juvix.fish
ZSH
Run the following command in your shell:
juvix --zsh-completion-script juvix > $DIR_IN_FPATH/_juvix
where $DIR_IN_FPATH
is a directory that is present on the ZSH FPATH
variable (which
you can inspect by running echo $FPATH
in the shell).
Juvix Doctor
The juvix doctor
command can help you to troubleshoot problems with
your development environment. For each problem the doctor finds they'll
be a link to a section on this page to help you fix it.
Could not find the clang command
The Juvix compiler uses the Clang compiler
version 13 or later to generate binaries. You need to have Clang
available on your system $PATH
.
Recommended installation method:
MacOS
Use Homebrew:
brew install llvm
NB: The distribution of Clang that comes with XCode does not support the
Wasm
target so you must install the standard Clang distribution.
Debian / Ubuntu Linux
sudo apt install clang lldb lld
Arch Linux
sudo pacman -S llvm lld
Could not find the wasm-ld command
The Juvix compiler required wasm-ld
(the Wasm linker) to produce
Wasm
binaries.
Recommended installation method:
MacOS
wasm-ld
is included in the Homebrew llvm
distribution:
brew install llvm
Debian / Ubuntu Linux
sudo apt install lldb lld
Arch Linux
sudo pacman -S lld
Newer Clang version required
Juvix requires Clang version 13 or above. See the documentation on installing Clang.
Clang does not support the wasm32 target
Juvix requires Clang version 13 or above. See the documentation on installing Clang.
Clang does not support the wasm32-wasi target
Juvix uses WASI - The Wasm System Interface to
produce binaries that can be executed using a Wasm runtime. The files
necessary to setup Clang with wasm32-wasi
support are available at
wasi-sdk.
To install the wasm32-wasi
target for Clang you need to do two things:
Install libclang_rt.builtins-wasm32.a
into your Clang distribution
-
Obtain
libclang_rt.builtins-wasm32-wasi-16.0.tar.gz
from the wasi-sdk releases page. -
Untar the file and place the file
lib/wasi/libclang_rt.builtins-wasm32.a
into your Clang distribution directory.On MacOS, if you installed llvm using homebrew you can find the Clang distribution directory using
brew --prefix llvm
. You should then place the builtins file at`brew --prefix llvm`/lib/wasi/libclang_rt.builtins-wasm32.a
.On Linux the Clang distribution directory will be something like
/usr/lib/clang/13.0.1
where13.0.1
is the version of Clang that you have installed. You should then place the builtins file at/usr/lib/clang/13.0.1/lib/wasi/libclang_rt.builtins-wasm32
.
Download the WASI sysroot and set WASI_SYSROOT_PATH
- Obtain
wasi-sysroot-16.0.tar.gz
from the wasi-sdk releases page. - Untar the file and set the environment variable
WASI_SYSROOT_PATH
to that location.
Environment variable WASI_SYSROOT_PATH
is not set
Set the WASI_SYSROOT_PATH
to the directory where you installed the
wasi-sdk
sysroot files. See installing the WASI
sysroot.
Could not find the wasmer command
The Juvix test suite uses Wasmer as a Wasm runtime to execute compiled Wasm binaries. See the Wasmer documentation to see how to install it.
Emacs Mode
There is an Emacs mode available for Juvix. Currently, it supports syntax highlighting for well-scoped modules.
To get started, clone the Juvix Emacs mode repository:
git clone https://github.com/anoma/juvix-mode.git
To install it add the following lines to your Emacs configuration file:
(push "/path/to/juvix-mode/" load-path)
(require 'juvix-mode)
Make sure that Juvix is installed in your PATH
.
The Juvix major mode will be activated automatically for .juvix
files.
Keybindings
Key | Function Name | Description |
---|---|---|
C-c C-l | juvix-load | Runs the scoper and adds semantic syntax highlighting |
M-. | juvix-goto-definition | Go to the definition of symbol at point |
C-c C-f | juvix-format-buffer | Format the current buffer |
Emacs installation
Most Linux distributions contain an Emacs package which can be installed
with your package manager (sudo apt install emacs
on Ubuntu). On
macOS, it is recommended to install Emacs Plus via Homebrew:
brew install emacs-plus
. Using the Emacs Homebrew casks is not
recommended.
Common problems
-
Error "Symbol's value as variable is void: sh:1:"
Make sure the juvix executable is on the Emacs'
exec-path
. Note thatexec-path
may be different from your shell'sPATH
. This is particularly common on macOS with Emacs launched from GUI instead of the terminal.The easiest way to resolve this issue is to install the exec-path-from-shell package (available on MELPA). Alternatively, one may set
exec-path
to match shellPATH
by following the instructions from EmacsWiki.
Testing
Dependencies
See Installing dependencies for instructions on how to setup the testing environment for the WASM compiler tests.
Running
Run tests using:
stack test
To run tests, ignoring all the WASM tests:
stack test --ta '-p "! /slow tests/"'
Judoc syntax reference
Judoc is used to document parts of your code. You can attach Judoc blocks to the following entities:
- A module.
- A type definition.
- A constructor definition.
- A type signature of a function.
- An axiom definition.
In order to attach documentation to any of these entities, write blocks of documentation before them:
-
For modules:
--- This module is cool module Cool; ..
-
For type definitions:
--- Unary representation of natural numbers type Nat : Type := | --- Nullary constructor representing number 0 zero : Nat | --- Unary constructor representing the successor of a natural number suc : Nat -> Nat;
-
For type signatures (and likewise for axioms):
--- The polymorphic identity function id : {A : Type} -> A -> A;
Next we define the syntax of Judoc blocks.
Block
A block can be one of these:
- A paragraph.
- An example.
Blocks are separated by a line with only ---
.
For instance, this is a sequence of two blocks:
--- First block
---
--- Second block
Note that the following is a single block since it lacks the ---
separator:
--- First block
--- Still first block
Paragraph
A paragraph is a non-empty sequence of lines.
For instance, the following is a paragraph with two lines:
--- First line
--- Second line
Note that a rendered paragraph will have have no line breaks. If you want to have line breaks, you will need to split the paragraph. Hence, the paragraph above will be rendered as
First line Second line
line
A line starts with ---
and is followed by a non-empty sequence of
atoms.
For instance, the following is a valid line:
--- A ;Pair Int Bool; contains an ;Int; and a ;Bool;
Atom
An atom is either:
- A string of text (including spaces but not line breaks).
- An inline Juvix expression surrounded by
;
.
For instance, the following are valid atoms:
I am some text.
;Pair Int Bool;
Example
An example is of the following form
--- >>> someExpression ;
The someExpression
can span multiple lines and it must be ended with a ;
.
For instance:
--- >>> 1
+ 2
+ 3;
Juvix community
Join us on our Discord server
This project is part of a bigger effort called Anoma. Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination. Join the Anoma project.
Contributing to Juvix
Thank you for considering contributing to Juvix! We welcome all contributions, big or small, of any kind. We appreciate any help/feedback we can get.
Getting Started
Make sure you have followed the installation instructions and have a working Juvix installation. You can also use the web-based development environment ready to the Juvix development, Juvix Github Codespace
- Fork the repository.
- Clone your forked repository to your local machine.
- Install Stack if you haven't already.
- Build the project by running
stack build
. To build the project with optimizations, runstack build --fast
. To install the binaries to your local~/.local/bin
, runstack install
. - Run the tests by running
stack test
. - Make sure to install the pre-commit binary, so you
can run the pre-commit hooks by running
make precommit
in the root directory of the project. All the Pull Requests will be checked by the pre-commit hooks.
Making Changes
- Create a new branch for your changes:
git checkout -b my-branch-name
. In case you are working on an issue, please name your branch after the issue number, e.g.issue-123
. - Make your changes and commit them with a descriptive message.
- Push your changes to your forked repository:
git push origin my-branch-name
. - Submit a pull request to the main repository with a concise description of your changes.
- Make sure that your pull request passes all the tests and pre-commit hooks.
Haskell Code Style
We value readability and maintainability over saving lines of code. The best source of truth for the Juvix code style is the existing codebase. We strongly encourage you to look at the existing code and follow the same style. Open an issue if you have any questions, or better yet, join our Discord and ask there!
Some basic guidelines when writing code:
- Use clear and descriptive names for variables, functions, and types.
- Keep functions short and focused on a single task. Separate functions when they start to get too long.
- Use comments to explain complex or non-obvious code.
- Run
make format
to format your code withormolu
.
Testing
Please include tests for any new functionality or bug fixes. The tests are
located in the test
directory, the tests are written in Haskell and use the
tasty framework. To run the tests, run stack test
. If you are changing the
CLI, please also update the smoke tests in the tests/smoke
directory.
Code Review
All pull requests will be reviewed by at least one member of the development team. Feedback may be provided on the code itself, as well as on the tests and documentation.
Thank you for contributing to Juvix!
GNU GENERAL PUBLIC LICENSE
Version 3, 29 June 2007
Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.
Preamble
The GNU General Public License is a free, copyleft license for
software and other kinds of works.
The licenses for most software and other practical works are designed
to take away your freedom to share and change the works. By contrast,
the GNU General Public License is intended to guarantee your freedom to
share and change all versions of a program--to make sure it remains free
software for all its users. We, the Free Software Foundation, use the
GNU General Public License for most of our software; it applies also to
any other work released this way by its authors. You can apply it to
your programs, too.
When we speak of free software, we are referring to freedom, not
price. Our General Public Licenses are designed to make sure that you
have the freedom to distribute copies of free software (and charge for
them if you wish), that you receive source code or can get it if you
want it, that you can change the software or use pieces of it in new
free programs, and that you know you can do these things.
To protect your rights, we need to prevent others from denying you
these rights or asking you to surrender the rights. Therefore, you have
certain responsibilities if you distribute copies of the software, or if
you modify it: responsibilities to respect the freedom of others.
For example, if you distribute copies of such a program, whether
gratis or for a fee, you must pass on to the recipients the same
freedoms that you received. You must make sure that they, too, receive
or can get the source code. And you must show them these terms so they
know their rights.
Developers that use the GNU GPL protect your rights with two steps:
(1) assert copyright on the software, and (2) offer you this License
giving you legal permission to copy, distribute and/or modify it.
For the developers' and authors' protection, the GPL clearly explains
that there is no warranty for this free software. For both users' and
authors' sake, the GPL requires that modified versions be marked as
changed, so that their problems will not be attributed erroneously to
authors of previous versions.
Some devices are designed to deny users access to install or run
modified versions of the software inside them, although the manufacturer
can do so. This is fundamentally incompatible with the aim of
protecting users' freedom to change the software. The systematic
pattern of such abuse occurs in the area of products for individuals to
use, which is precisely where it is most unacceptable. Therefore, we
have designed this version of the GPL to prohibit the practice for those
products. If such problems arise substantially in other domains, we
stand ready to extend this provision to those domains in future versions
of the GPL, as needed to protect the freedom of users.
Finally, every program is threatened constantly by software patents.
States should not allow patents to restrict development and use of
software on general-purpose computers, but in those that do, we wish to
avoid the special danger that patents applied to a free program could
make it effectively proprietary. To prevent this, the GPL assures that
patents cannot be used to render the program non-free.
The precise terms and conditions for copying, distribution and
modification follow.
TERMS AND CONDITIONS
0. Definitions.
"This License" refers to version 3 of the GNU General Public License.
"Copyright" also means copyright-like laws that apply to other kinds of
works, such as semiconductor masks.
"The Program" refers to any copyrightable work licensed under this
License. Each licensee is addressed as "you". "Licensees" and
"recipients" may be individuals or organizations.
To "modify" a work means to copy from or adapt all or part of the work
in a fashion requiring copyright permission, other than the making of an
exact copy. The resulting work is called a "modified version" of the
earlier work or a work "based on" the earlier work.
A "covered work" means either the unmodified Program or a work based
on the Program.
To "propagate" a work means to do anything with it that, without
permission, would make you directly or secondarily liable for
infringement under applicable copyright law, except executing it on a
computer or modifying a private copy. Propagation includes copying,
distribution (with or without modification), making available to the
public, and in some countries other activities as well.
To "convey" a work means any kind of propagation that enables other
parties to make or receive copies. Mere interaction with a user through
a computer network, with no transfer of a copy, is not conveying.
An interactive user interface displays "Appropriate Legal Notices"
to the extent that it includes a convenient and prominently visible
feature that (1) displays an appropriate copyright notice, and (2)
tells the user that there is no warranty for the work (except to the
extent that warranties are provided), that licensees may convey the
work under this License, and how to view a copy of this License. If
the interface presents a list of user commands or options, such as a
menu, a prominent item in the list meets this criterion.
1. Source Code.
The "source code" for a work means the preferred form of the work
for making modifications to it. "Object code" means any non-source
form of a work.
A "Standard Interface" means an interface that either is an official
standard defined by a recognized standards body, or, in the case of
interfaces specified for a particular programming language, one that
is widely used among developers working in that language.
The "System Libraries" of an executable work include anything, other
than the work as a whole, that (a) is included in the normal form of
packaging a Major Component, but which is not part of that Major
Component, and (b) serves only to enable use of the work with that
Major Component, or to implement a Standard Interface for which an
implementation is available to the public in source code form. A
"Major Component", in this context, means a major essential component
(kernel, window system, and so on) of the specific operating system
(if any) on which the executable work runs, or a compiler used to
produce the work, or an object code interpreter used to run it.
The "Corresponding Source" for a work in object code form means all
the source code needed to generate, install, and (for an executable
work) run the object code and to modify the work, including scripts to
control those activities. However, it does not include the work's
System Libraries, or general-purpose tools or generally available free
programs which are used unmodified in performing those activities but
which are not part of the work. For example, Corresponding Source
includes interface definition files associated with source files for
the work, and the source code for shared libraries and dynamically
linked subprograms that the work is specifically designed to require,
such as by intimate data communication or control flow between those
subprograms and other parts of the work.
The Corresponding Source need not include anything that users
can regenerate automatically from other parts of the Corresponding
Source.
The Corresponding Source for a work in source code form is that
same work.
2. Basic Permissions.
All rights granted under this License are granted for the term of
copyright on the Program, and are irrevocable provided the stated
conditions are met. This License explicitly affirms your unlimited
permission to run the unmodified Program. The output from running a
covered work is covered by this License only if the output, given its
content, constitutes a covered work. This License acknowledges your
rights of fair use or other equivalent, as provided by copyright law.
You may make, run and propagate covered works that you do not
convey, without conditions so long as your license otherwise remains
in force. You may convey covered works to others for the sole purpose
of having them make modifications exclusively for you, or provide you
with facilities for running those works, provided that you comply with
the terms of this License in conveying all material for which you do
not control copyright. Those thus making or running the covered works
for you must do so exclusively on your behalf, under your direction
and control, on terms that prohibit them from making any copies of
your copyrighted material outside their relationship with you.
Conveying under any other circumstances is permitted solely under
the conditions stated below. Sublicensing is not allowed; section 10
makes it unnecessary.
3. Protecting Users' Legal Rights From Anti-Circumvention Law.
No covered work shall be deemed part of an effective technological
measure under any applicable law fulfilling obligations under article
11 of the WIPO copyright treaty adopted on 20 December 1996, or
similar laws prohibiting or restricting circumvention of such
measures.
When you convey a covered work, you waive any legal power to forbid
circumvention of technological measures to the extent such circumvention
is effected by exercising rights under this License with respect to
the covered work, and you disclaim any intention to limit operation or
modification of the work as a means of enforcing, against the work's
users, your or third parties' legal rights to forbid circumvention of
technological measures.
4. Conveying Verbatim Copies.
You may convey verbatim copies of the Program's source code as you
receive it, in any medium, provided that you conspicuously and
appropriately publish on each copy an appropriate copyright notice;
keep intact all notices stating that this License and any
non-permissive terms added in accord with section 7 apply to the code;
keep intact all notices of the absence of any warranty; and give all
recipients a copy of this License along with the Program.
You may charge any price or no price for each copy that you convey,
and you may offer support or warranty protection for a fee.
5. Conveying Modified Source Versions.
You may convey a work based on the Program, or the modifications to
produce it from the Program, in the form of source code under the
terms of section 4, provided that you also meet all of these conditions:
a) The work must carry prominent notices stating that you modified
it, and giving a relevant date.
b) The work must carry prominent notices stating that it is
released under this License and any conditions added under section
7. This requirement modifies the requirement in section 4 to
"keep intact all notices".
c) You must license the entire work, as a whole, under this
License to anyone who comes into possession of a copy. This
License will therefore apply, along with any applicable section 7
additional terms, to the whole of the work, and all its parts,
regardless of how they are packaged. This License gives no
permission to license the work in any other way, but it does not
invalidate such permission if you have separately received it.
d) If the work has interactive user interfaces, each must display
Appropriate Legal Notices; however, if the Program has interactive
interfaces that do not display Appropriate Legal Notices, your
work need not make them do so.
A compilation of a covered work with other separate and independent
works, which are not by their nature extensions of the covered work,
and which are not combined with it such as to form a larger program,
in or on a volume of a storage or distribution medium, is called an
"aggregate" if the compilation and its resulting copyright are not
used to limit the access or legal rights of the compilation's users
beyond what the individual works permit. Inclusion of a covered work
in an aggregate does not cause this License to apply to the other
parts of the aggregate.
6. Conveying Non-Source Forms.
You may convey a covered work in object code form under the terms
of sections 4 and 5, provided that you also convey the
machine-readable Corresponding Source under the terms of this License,
in one of these ways:
a) Convey the object code in, or embodied in, a physical product
(including a physical distribution medium), accompanied by the
Corresponding Source fixed on a durable physical medium
customarily used for software interchange.
b) Convey the object code in, or embodied in, a physical product
(including a physical distribution medium), accompanied by a
written offer, valid for at least three years and valid for as
long as you offer spare parts or customer support for that product
model, to give anyone who possesses the object code either (1) a
copy of the Corresponding Source for all the software in the
product that is covered by this License, on a durable physical
medium customarily used for software interchange, for a price no
more than your reasonable cost of physically performing this
conveying of source, or (2) access to copy the
Corresponding Source from a network server at no charge.
c) Convey individual copies of the object code with a copy of the
written offer to provide the Corresponding Source. This
alternative is allowed only occasionally and noncommercially, and
only if you received the object code with such an offer, in accord
with subsection 6b.
d) Convey the object code by offering access from a designated
place (gratis or for a charge), and offer equivalent access to the
Corresponding Source in the same way through the same place at no
further charge. You need not require recipients to copy the
Corresponding Source along with the object code. If the place to
copy the object code is a network server, the Corresponding Source
may be on a different server (operated by you or a third party)
that supports equivalent copying facilities, provided you maintain
clear directions next to the object code saying where to find the
Corresponding Source. Regardless of what server hosts the
Corresponding Source, you remain obligated to ensure that it is
available for as long as needed to satisfy these requirements.
e) Convey the object code using peer-to-peer transmission, provided
you inform other peers where the object code and Corresponding
Source of the work are being offered to the general public at no
charge under subsection 6d.
A separable portion of the object code, whose source code is excluded
from the Corresponding Source as a System Library, need not be
included in conveying the object code work.
A "User Product" is either (1) a "consumer product", which means any
tangible personal property which is normally used for personal, family,
or household purposes, or (2) anything designed or sold for incorporation
into a dwelling. In determining whether a product is a consumer product,
doubtful cases shall be resolved in favor of coverage. For a particular
product received by a particular user, "normally used" refers to a
typical or common use of that class of product, regardless of the status
of the particular user or of the way in which the particular user
actually uses, or expects or is expected to use, the product. A product
is a consumer product regardless of whether the product has substantial
commercial, industrial or non-consumer uses, unless such uses represent
the only significant mode of use of the product.
"Installation Information" for a User Product means any methods,
procedures, authorization keys, or other information required to install
and execute modified versions of a covered work in that User Product from
a modified version of its Corresponding Source. The information must
suffice to ensure that the continued functioning of the modified object
code is in no case prevented or interfered with solely because
modification has been made.
If you convey an object code work under this section in, or with, or
specifically for use in, a User Product, and the conveying occurs as
part of a transaction in which the right of possession and use of the
User Product is transferred to the recipient in perpetuity or for a
fixed term (regardless of how the transaction is characterized), the
Corresponding Source conveyed under this section must be accompanied
by the Installation Information. But this requirement does not apply
if neither you nor any third party retains the ability to install
modified object code on the User Product (for example, the work has
been installed in ROM).
The requirement to provide Installation Information does not include a
requirement to continue to provide support service, warranty, or updates
for a work that has been modified or installed by the recipient, or for
the User Product in which it has been modified or installed. Access to a
network may be denied when the modification itself materially and
adversely affects the operation of the network or violates the rules and
protocols for communication across the network.
Corresponding Source conveyed, and Installation Information provided,
in accord with this section must be in a format that is publicly
documented (and with an implementation available to the public in
source code form), and must require no special password or key for
unpacking, reading or copying.
7. Additional Terms.
"Additional permissions" are terms that supplement the terms of this
License by making exceptions from one or more of its conditions.
Additional permissions that are applicable to the entire Program shall
be treated as though they were included in this License, to the extent
that they are valid under applicable law. If additional permissions
apply only to part of the Program, that part may be used separately
under those permissions, but the entire Program remains governed by
this License without regard to the additional permissions.
When you convey a copy of a covered work, you may at your option
remove any additional permissions from that copy, or from any part of
it. (Additional permissions may be written to require their own
removal in certain cases when you modify the work.) You may place
additional permissions on material, added by you to a covered work,
for which you have or can give appropriate copyright permission.
Notwithstanding any other provision of this License, for material you
add to a covered work, you may (if authorized by the copyright holders of
that material) supplement the terms of this License with terms:
a) Disclaiming warranty or limiting liability differently from the
terms of sections 15 and 16 of this License; or
b) Requiring preservation of specified reasonable legal notices or
author attributions in that material or in the Appropriate Legal
Notices displayed by works containing it; or
c) Prohibiting misrepresentation of the origin of that material, or
requiring that modified versions of such material be marked in
reasonable ways as different from the original version; or
d) Limiting the use for publicity purposes of names of licensors or
authors of the material; or
e) Declining to grant rights under trademark law for use of some
trade names, trademarks, or service marks; or
f) Requiring indemnification of licensors and authors of that
material by anyone who conveys the material (or modified versions of
it) with contractual assumptions of liability to the recipient, for
any liability that these contractual assumptions directly impose on
those licensors and authors.
All other non-permissive additional terms are considered "further
restrictions" within the meaning of section 10. If the Program as you
received it, or any part of it, contains a notice stating that it is
governed by this License along with a term that is a further
restriction, you may remove that term. If a license document contains
a further restriction but permits relicensing or conveying under this
License, you may add to a covered work material governed by the terms
of that license document, provided that the further restriction does
not survive such relicensing or conveying.
If you add terms to a covered work in accord with this section, you
must place, in the relevant source files, a statement of the
additional terms that apply to those files, or a notice indicating
where to find the applicable terms.
Additional terms, permissive or non-permissive, may be stated in the
form of a separately written license, or stated as exceptions;
the above requirements apply either way.
8. Termination.
You may not propagate or modify a covered work except as expressly
provided under this License. Any attempt otherwise to propagate or
modify it is void, and will automatically terminate your rights under
this License (including any patent licenses granted under the third
paragraph of section 11).
However, if you cease all violation of this License, then your
license from a particular copyright holder is reinstated (a)
provisionally, unless and until the copyright holder explicitly and
finally terminates your license, and (b) permanently, if the copyright
holder fails to notify you of the violation by some reasonable means
prior to 60 days after the cessation.
Moreover, your license from a particular copyright holder is
reinstated permanently if the copyright holder notifies you of the
violation by some reasonable means, this is the first time you have
received notice of violation of this License (for any work) from that
copyright holder, and you cure the violation prior to 30 days after
your receipt of the notice.
Termination of your rights under this section does not terminate the
licenses of parties who have received copies or rights from you under
this License. If your rights have been terminated and not permanently
reinstated, you do not qualify to receive new licenses for the same
material under section 10.
9. Acceptance Not Required for Having Copies.
You are not required to accept this License in order to receive or
run a copy of the Program. Ancillary propagation of a covered work
occurring solely as a consequence of using peer-to-peer transmission
to receive a copy likewise does not require acceptance. However,
nothing other than this License grants you permission to propagate or
modify any covered work. These actions infringe copyright if you do
not accept this License. Therefore, by modifying or propagating a
covered work, you indicate your acceptance of this License to do so.
10. Automatic Licensing of Downstream Recipients.
Each time you convey a covered work, the recipient automatically
receives a license from the original licensors, to run, modify and
propagate that work, subject to this License. You are not responsible
for enforcing compliance by third parties with this License.
An "entity transaction" is a transaction transferring control of an
organization, or substantially all assets of one, or subdividing an
organization, or merging organizations. If propagation of a covered
work results from an entity transaction, each party to that
transaction who receives a copy of the work also receives whatever
licenses to the work the party's predecessor in interest had or could
give under the previous paragraph, plus a right to possession of the
Corresponding Source of the work from the predecessor in interest, if
the predecessor has it or can get it with reasonable efforts.
You may not impose any further restrictions on the exercise of the
rights granted or affirmed under this License. For example, you may
not impose a license fee, royalty, or other charge for exercise of
rights granted under this License, and you may not initiate litigation
(including a cross-claim or counterclaim in a lawsuit) alleging that
any patent claim is infringed by making, using, selling, offering for
sale, or importing the Program or any portion of it.
11. Patents.
A "contributor" is a copyright holder who authorizes use under this
License of the Program or a work on which the Program is based. The
work thus licensed is called the contributor's "contributor version".
A contributor's "essential patent claims" are all patent claims
owned or controlled by the contributor, whether already acquired or
hereafter acquired, that would be infringed by some manner, permitted
by this License, of making, using, or selling its contributor version,
but do not include claims that would be infringed only as a
consequence of further modification of the contributor version. For
purposes of this definition, "control" includes the right to grant
patent sublicenses in a manner consistent with the requirements of
this License.
Each contributor grants you a non-exclusive, worldwide, royalty-free
patent license under the contributor's essential patent claims, to
make, use, sell, offer for sale, import and otherwise run, modify and
propagate the contents of its contributor version.
In the following three paragraphs, a "patent license" is any express
agreement or commitment, however denominated, not to enforce a patent
(such as an express permission to practice a patent or covenant not to
sue for patent infringement). To "grant" such a patent license to a
party means to make such an agreement or commitment not to enforce a
patent against the party.
If you convey a covered work, knowingly relying on a patent license,
and the Corresponding Source of the work is not available for anyone
to copy, free of charge and under the terms of this License, through a
publicly available network server or other readily accessible means,
then you must either (1) cause the Corresponding Source to be so
available, or (2) arrange to deprive yourself of the benefit of the
patent license for this particular work, or (3) arrange, in a manner
consistent with the requirements of this License, to extend the patent
license to downstream recipients. "Knowingly relying" means you have
actual knowledge that, but for the patent license, your conveying the
covered work in a country, or your recipient's use of the covered work
in a country, would infringe one or more identifiable patents in that
country that you have reason to believe are valid.
If, pursuant to or in connection with a single transaction or
arrangement, you convey, or propagate by procuring conveyance of, a
covered work, and grant a patent license to some of the parties
receiving the covered work authorizing them to use, propagate, modify
or convey a specific copy of the covered work, then the patent license
you grant is automatically extended to all recipients of the covered
work and works based on it.
A patent license is "discriminatory" if it does not include within
the scope of its coverage, prohibits the exercise of, or is
conditioned on the non-exercise of one or more of the rights that are
specifically granted under this License. You may not convey a covered
work if you are a party to an arrangement with a third party that is
in the business of distributing software, under which you make payment
to the third party based on the extent of your activity of conveying
the work, and under which the third party grants, to any of the
parties who would receive the covered work from you, a discriminatory
patent license (a) in connection with copies of the covered work
conveyed by you (or copies made from those copies), or (b) primarily
for and in connection with specific products or compilations that
contain the covered work, unless you entered into that arrangement,
or that patent license was granted, prior to 28 March 2007.
Nothing in this License shall be construed as excluding or limiting
any implied license or other defenses to infringement that may
otherwise be available to you under applicable patent law.
12. No Surrender of Others' Freedom.
If conditions are imposed on you (whether by court order, agreement or
otherwise) that contradict the conditions of this License, they do not
excuse you from the conditions of this License. If you cannot convey a
covered work so as to satisfy simultaneously your obligations under this
License and any other pertinent obligations, then as a consequence you may
not convey it at all. For example, if you agree to terms that obligate you
to collect a royalty for further conveying from those to whom you convey
the Program, the only way you could satisfy both those terms and this
License would be to refrain entirely from conveying the Program.
13. Use with the GNU Affero General Public License.
Notwithstanding any other provision of this License, you have
permission to link or combine any covered work with a work licensed
under version 3 of the GNU Affero General Public License into a single
combined work, and to convey the resulting work. The terms of this
License will continue to apply to the part which is the covered work,
but the special requirements of the GNU Affero General Public License,
section 13, concerning interaction through a network will apply to the
combination as such.
14. Revised Versions of this License.
The Free Software Foundation may publish revised and/or new versions of
the GNU General Public License from time to time. Such new versions will
be similar in spirit to the present version, but may differ in detail to
address new problems or concerns.
Each version is given a distinguishing version number. If the
Program specifies that a certain numbered version of the GNU General
Public License "or any later version" applies to it, you have the
option of following the terms and conditions either of that numbered
version or of any later version published by the Free Software
Foundation. If the Program does not specify a version number of the
GNU General Public License, you may choose any version ever published
by the Free Software Foundation.
If the Program specifies that a proxy can decide which future
versions of the GNU General Public License can be used, that proxy's
public statement of acceptance of a version permanently authorizes you
to choose that version for the Program.
Later license versions may give you additional or different
permissions. However, no additional obligations are imposed on any
author or copyright holder as a result of your choosing to follow a
later version.
15. Disclaimer of Warranty.
THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
16. Limitation of Liability.
IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
SUCH DAMAGES.
17. Interpretation of Sections 15 and 16.
If the disclaimer of warranty and limitation of liability provided
above cannot be given local legal effect according to their terms,
reviewing courts shall apply local law that most closely approximates
an absolute waiver of all civil liability in connection with the
Program, unless a warranty or assumption of liability accompanies a
copy of the Program in return for a fee.
END OF TERMS AND CONDITIONS
How to Apply These Terms to Your New Programs
If you develop a new program, and you want it to be of the greatest
possible use to the public, the best way to achieve this is to make it
free software which everyone can redistribute and change under these terms.
To do so, attach the following notices to the program. It is safest
to attach them to the start of each source file to most effectively
state the exclusion of warranty; and each file should have at least
the "copyright" line and a pointer to where the full notice is found.
<one line to give the program's name and a brief idea of what it does.>
Copyright (C) <year> <name of author>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
Also add information on how to contact you by electronic and paper mail.
If the program does terminal interaction, make it output a short
notice like this when it starts in an interactive mode:
<program> Copyright (C) <year> <name of author>
This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
This is free software, and you are welcome to redistribute it
under certain conditions; type `show c' for details.
The hypothetical commands `show w' and `show c' should show the appropriate
parts of the General Public License. Of course, your program's commands
might be different; for a GUI interface, you would use an "about box".
You should also get your employer (if you work as a programmer) or school,
if any, to sign a "copyright disclaimer" for the program, if necessary.
For more information on this, and how to apply and follow the GNU GPL, see
<https://www.gnu.org/licenses/>.
The GNU General Public License does not permit incorporating your program
into proprietary programs. If your program is a subroutine library, you
may consider it more useful to permit linking proprietary applications with
the library. If this is what you want to do, use the GNU Lesser General
Public License instead of this License. But first, please read
<https://www.gnu.org/licenses/why-not-lgpl.html>.