Juvix

Tara the Juvix mascot

CI Status

The Juvix compiler CI

Nightly build, release and benchmark
Codebase
Open the Juvix Standard Lib in Github Codespace

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.

If you're interested in Juvix, you may also want to explore the following related projects:

ProjectDescription
GEBIntermediate language for writing compilers and one of the Juvix backends.
VampIRProof-system-agnostic language for writing arithmetic circuit and one of the GEB backends.
TaigaA framework for generalized shielded state transitions.

Resources

Here is a summary of resources to help you learn more about Juvix:

Documentation

ResourceDescription
Official websiteThe official website of Juvix, where you can find documentation, changelog, tutorials, and community resources.
GitHub repositoryThe official GitHub repository of Juvix, where you can find the source code and contribute to the project.

Community

ResourceDescription
Discord communityThe 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.
TwitterThe official Twitter account of Juvix, where you can stay up-to-date with the latest news and announcements.

Libraries

ResourceDescription
Standard libraryThe 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

ResourceDescription
VSCode extensionSupport for the Juvix programming language with features such as syntax highlighting, error checking and many more directly in the VSCode editor.
Emacs Juvix modeA major mode for Emacs that provides support for writing Juvix programs.

Development environments

ResourceDescription
Juvix Standard Lib CodespaceA 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 CodespaceThis 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

ResourceDescription
Homebrew Juvix formulaA formula for Homebrew, a package manager for macOS and Linux, that allows you to easily install Juvix on your system.
Juvix Nightly buildsUsers 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

Juvix Mascot

v0.3.0 (2023-03-15)

Full Changelog

Implemented enhancements:

Merged pull requests:

v0.2.9 (2023-01-18)

Full Changelog

Implemented enhancements:

Merged pull requests:

v0.2.8 (2022-12-20)

Full Changelog

Implemented enhancements:

Merged pull requests:

v0.2.7 (2022-12-05)

Full Changelog

Implemented enhancements:

Merged pull requests:

v0.2.6 (2022-10-26)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.5 (2022-09-14)

Full Changelog

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:

v0.2.4 (2022-08-19)

Full Changelog

(Special version for Heliax's retreat in Italy)

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.3 (2022-08-15)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.2 (2022-07-25)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

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 from stack.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

Juvix Mascot

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

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, or
  • suc n where n is an element of Nat, i.e., it is constructed by applying suc to appropriate arguments (in this case the argument of suc has type Nat).

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.

  1. Define a function prime : Nat -> Nat which checks if a given natural number is prime.

  2. 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?

  3. Define a polymorphic function which computes the last element of a list. What is the result of your function on the empty list?

  4. A suffix of a list l is any list which can be obtained from l by removing some initial elements. For example, the suffixes of 1 :: 2 :: 3 :: nil are: 1 :: 2 :: 3 :: nil, 2 :: 3 :: nil, 3 :: nil and nil.

    Define a function which computes the list of all suffixes of a given list in the order of decreasing length.

  5. 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 function

    tmap : (Nat -> Nat) -> Tree -> Tree

    which applies a function to all natural numbers stored in a tree.

  6. Make the Tree type polymorphic in the element type and repeat the previous exercise.

  7. Write a tail recursive function which reverses a list.

  8. Write a tail recursive function which computes the factorial of a natural number.

  9. 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 computes 2(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 of llvm).

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:

  1. Extract the libclang_rt.builtins-wasm32-wasi-*.tar.gz archive in the clang 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

  2. Extract the wasi-sysroot-*.tar.gz archive on your local system and set WASI_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.

  1. native. This is the default. Produces a native 64bit executable for your machine.
  2. wasm32-wasi. Produces a WebAssembly binary which uses the WASI runtime.
  3. 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 evaluates condition, if true evaluates and returns branch1, otherwise evaluates and returns branch2.
  • a || b. Lazy disjunction. First evaluates a, if true returns true, otherwise evaluates and returns b.
  • a && b. Lazy conjunction. First evaluates a, if false returns false, otherwise evaluates and returns b.
  • 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 file
  • typecheck Typecheck a Juvix file
  • compile Compile a Juvix file

Utility Commands

  • doctor Perform checks on your Juvix development environment
  • init Interactively initialize a juvix project in the current directory

Dev Commands

juvix dev COMMAND
  • parse Parse a Juvix file
  • scope Parse and scope a Juvix file
  • highlight Highlight a Juvix file
  • core Subcommands related to JuvixCore
  • asm Subcommands related to JuvixAsm
  • root Show the root path for a Juvix project
  • termination Subcommands related to termination checking
  • internal Subcommands related to Internal
  • minic 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

  1. Obtain libclang_rt.builtins-wasm32-wasi-16.0.tar.gz from the wasi-sdk releases page.

  2. 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 where 13.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

  1. Obtain wasi-sysroot-16.0.tar.gz from the wasi-sdk releases page.
  2. 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

KeyFunction NameDescription
C-c C-ljuvix-loadRuns the scoper and adds semantic syntax highlighting
M-.juvix-goto-definitionGo to the definition of symbol at point
C-c C-fjuvix-format-bufferFormat 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 that exec-path may be different from your shell's PATH. 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 shell PATH 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:

  1. A module.
  2. A type definition.
  3. A constructor definition.
  4. A type signature of a function.
  5. An axiom definition.

In order to attach documentation to any of these entities, write blocks of documentation before them:

  1. For modules:

    --- This module is cool
module Cool;
..

  2. 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;

  3. 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:

  1. A paragraph.
  2. 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:

  1. A string of text (including spaces but not line breaks).
  2. An inline Juvix expression surrounded by ;.

For instance, the following are valid atoms:

  1. I am some text.
  2. ;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

  1. Fork the repository.
  2. Clone your forked repository to your local machine.
  3. Install Stack if you haven't already.
  4. Build the project by running stack build. To build the project with optimizations, run stack build --fast. To install the binaries to your local ~/.local/bin, run stack install.
  5. Run the tests by running stack test.
  6. 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

  1. 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.
  2. Make your changes and commit them with a descriptive message.
  3. Push your changes to your forked repository: git push origin my-branch-name.
  4. Submit a pull request to the main repository with a concise description of your changes.
  5. 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 with ormolu.

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>.