anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-03 13:03:25 +03:00
Code Issues Projects Releases Wiki Activity

Add new README and md files (#1904)

Browse Source 
In this PR, I have updated the README file to reflect the new goals of
the project and highlight related products to Juvix. The ORG files have
been replaced with Markdown for better readability and maintainability.
Additionally, I have added a couple of files to fine-tune the mdbook
settings. These changes, I believe, will make it easier for users to
understand and contribute to the project.🤞

- Closes #1878
- New pre-commit hook to format md, yaml, js, CSS files.

To check the website generation, I have deployed the result here:
Work in progress.

- https://jonaprieto.github.io/juvix
- https://github.com/jonaprieto/juvix

---------

Co-authored-by: Paul Cadman <pcadman@gmail.com>
Co-authored-by: Christopher Goes <cwgoes@pluranimity.org>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This commit is contained in:
Jonathan Cubides 2023-03-21 20:01:48 +01:00 committed by GitHub
parent 6a538029e1
commit 22ba8f15fd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
99 changed files with 6526 additions and 4250 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
.github/ISSUE_TEMPLATE/bug_report.md vendored
View File

@ -1,21 +1,22 @@
---
name: Bug report
about: Create a report to help us improve
title: ''
title: ""
labels: bug, pending-review
assignees: ''
assignees: ""
---
**Describe the bug**
A clear and concise description of what the bug is.
**Desktop (please complete the following information):**
- OS: [e.g. iOS]
- Juvix Version [e.g. 22]
**To Reproduce**
Steps to reproduce the behavior:
1. Go to '...'
2. Click on '....'
3. Scroll down to '....'

5
.github/ISSUE_TEMPLATE/feature_request.md vendored
View File

@ -1,10 +1,9 @@
---
name: Feature request
about: Suggest an idea for this project
title: ''
title: ""
labels: enhancement, pending-review
assignees: ''
assignees: ""
---
**Is your feature request related to a problem? Please describe.**

23
.github/workflows/ci.yml vendored
View File

@ -1,5 +1,5 @@
name: The Juvix compiler CI
'on':
"on":
workflow_dispatch:
inputs:
ref:
@ -18,20 +18,19 @@ name: The Juvix compiler CI
- synchronize
- ready_for_review
concurrency:
group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}'
group: "${{ github.workflow }}-${{ github.head_ref || github.run_id }}"
cancel-in-progress: true
env:
SKIP: ormolu
jobs:
pre-commit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: actions/setup-python@v4
with:
python-version: '3.11'
python-version: "3.11"
- uses: pre-commit/action@v3.0.0
clang-format:
@ -40,7 +39,7 @@ jobs:
- uses: actions/checkout@v3
- uses: jidicula/clang-format-action@v4.10.1
with:
clang-format-version: '15'
clang-format-version: "15"
check-path: runtime/src
ormolu:
@ -71,13 +70,13 @@ jobs:
path: |
C:/Program Files/LLVM
./llvm
key: '${{ runner.os }}-llvm-13'
key: "${{ runner.os }}-llvm-13"
- name: Install LLVM and Clang
uses: KyleMayes/install-llvm-action@v1
with:
version: '13.0'
cached: '${{ steps.cache-llvm.outputs.cache-hit }}'
version: "13.0"
cached: "${{ steps.cache-llvm.outputs.cache-hit }}"
- name: Download and extract wasi-sysroot
run: >
@ -191,13 +190,13 @@ jobs:
path: |
C:/Program Files/LLVM
./llvm
key: '${{ runner.os }}-llvm-13'
key: "${{ runner.os }}-llvm-13"
- name: Install LLVM and Clang
uses: KyleMayes/install-llvm-action@v1
with:
version: '13.0'
cached: '${{ steps.cache-llvm.outputs.cache-hit }}'
version: "13.0"
cached: "${{ steps.cache-llvm.outputs.cache-hit }}"
- name: Build the mdbook
run: |
@ -227,7 +226,7 @@ jobs:
- name: Deploy HTML to github pages
uses: peaceiris/actions-gh-pages@v3
with:
github_token: '${{ secrets.GITHUB_TOKEN }}'
github_token: "${{ secrets.GITHUB_TOKEN }}"
publish_dir: main/book/html
enable_jekyll: false
cname: docs.juvix.org

4
.github/workflows/linux-static-binary.yaml vendored
View File

@ -4,9 +4,9 @@ on:
workflow_dispatch:
inputs:
ref:
description: 'the repository ref to build'
description: "the repository ref to build"
required: true
default: 'main'
default: "main"
jobs:
build:

11
.gitignore vendored
View File

@ -65,8 +65,10 @@ agda2hs/
docs/*.html
*.cabal
/src/Juvix/Utils/OldParser.hs
CHANGELOG.md
UPDATES-FOR-CHANGELOG.org
docs/CHANGELOG.md
docs/CONTRIBUTING.md
docs/LICENSE.md
docs/README.md
.juvix-build
# C Code generation
@ -74,16 +76,13 @@ UPDATES-FOR-CHANGELOG.org
*.s
*.wasm
*.exe
docs/md/
_docs
docs/**/*.md
book/*
**/html/*
*.cmi
*.cmx
*.cmo
.history
docs/org/README.org
# Binary files (produced by `make check`)
examples/milestone/HelloWorld/HelloWorld
hie.yaml

6
.hlint.yaml
View File

@ -67,7 +67,11 @@
- error: { lhs: occNameString (occName (unLoc x)), rhs: rdrNameStr x }
- error: { lhs: occNameString (occName x), rhs: occNameStr x }
- error: {lhs: noLoc (HsVar noExtField (noLoc (mkRdrUnqual (mkVarOcc x)))), rhs: strToVar x}
- error:
{
lhs: noLoc (HsVar noExtField (noLoc (mkRdrUnqual (mkVarOcc x)))),
rhs: strToVar x,
}
# ------------------------------------------------------------------------------
# IGNORES

7
.pre-commit-config.yaml
View File

@ -17,6 +17,13 @@ repos:
- id: mixed-line-ending
exclude: tests/
- repo: https://github.com/pre-commit/mirrors-prettier
rev: v3.0.0-alpha.6
hooks:
- id: prettier
types_or: [css, javascript, markdown, yaml, toml]
exclude: examples/|tests/|assets/
- repo: https://github.com/anoma/juvix
rev: v0.2.9
hooks:

1388
CHANGELOG.md Normal file
View File

File diff suppressed because it is too large Load Diff

64
CONTRIBUTING.md Normal file
View File

@ -0,0 +1,64 @@
# 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][installation] and have a working Juvix installation. You can also use the web-based development environment ready to the Juvix development, [Juvix Github Codespace][juvix-codespace]
1. Fork the repository.
2. Clone your forked repository to your local machine.
3. Install [Stack][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][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][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!
[installation]: https://docs.juvix.org/howto/installing.html
[juvix-codespace]: https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope
[stack]: https://docs.haskellstack.org/en/stable/README/
[pre-commit]: https://pre-commit.com/
[discord]: https://discord.gg/PfaaFVErHt

2
LICENSE → LICENSE.md
View File

@ -1,3 +1,4 @@
```
GNU GENERAL PUBLIC LICENSE
Version 3, 29 June 2007
@ -672,3 +673,4 @@ 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>.
```

64
Makefile
View File

@ -2,11 +2,6 @@ PWD=$(CURDIR)
PREFIX="$(PWD)/.stack-work/prefix"
UNAME := $(shell uname)
IMAGES = $(shell find assets/images -type f)
ORGFILES = $(shell find docs/org -type f -name '*.org')
MDFILES:=$(patsubst docs/org/%,docs/md/%,$(ORGFILES:.org=.md))
EXAMPLEMILESTONE=examples/milestone
EXAMPLEHTMLOUTPUT=_docs/examples/html
EXAMPLES= Collatz/Collatz.juvix \
@ -21,9 +16,10 @@ DEMO_EXAMPLE=examples/demo/Demo.juvix
MAKEAUXFLAGS?=-s
MAKE=make ${MAKEAUXFLAGS}
ORGTOMDPRG ?=pandoc
ORGOPTS=--from org --to markdown_strict -s -o $@
METAFILES:=README.md \
CHANGELOG.md \
CONTRIBUTING.md \
LICENSE.md
ifeq ($(UNAME), Darwin)
THREADS := $(shell sysctl -n hw.logicalcpu)
@ -33,16 +29,10 @@ else
THREADS := $(shell echo %NUMBER_OF_PROCESSORS%)
endif
images:
echo $(IMAGES)
all: install
clean: clean-runtime
@stack clean --full
@rm -rf .hie
@rm -rf book
@rm -rf docs/md
.PHONY: clean-hard
clean-hard: clean
@ -81,39 +71,20 @@ demo-example:
# -- MDBook
docs/md/README.md : README.org
@mkdir -p docs/md
@${ORGTOMDPRG} README.org ${ORGOPTS}
docs/md/changelog.md : changelog.org
@mkdir -p docs/md
@${ORGTOMDPRG} changelog.org ${ORGOPTS}
docs/md/%.md : docs/org/%.org
@echo "Processing ... $@"
@mkdir -p $(dir $@)
${ORGTOMDPRG} $? ${ORGOPTS}
.PHONY: markdown-files
markdown-files: docs/md/README.md docs/md/changelog.md $(MDFILES)
.PHONY: markdown-docs
markdown-docs: cargo-dependencies markdown-files
@echo "copying assets ..."
@mkdir -p docs/md/assets/images
@cp -v $(IMAGES) docs/md/assets/images/
.PHONY: docs
docs:
@cp $(METAFILES) docs/
@mdbook build
.PHONY: serve-docs
serve-docs: markdown-files
serve-docs: docs
@mdbook serve --open
cargo-dependencies:
@cargo install mdbook \
mdbook-katex \
mdbook-linkcheck \
mdbook-toc
mdbook-pagetoc
# -- Codebase Documentation
@ -130,8 +101,8 @@ ORMOLUFILES = $(shell git ls-files '*.hs' '*.hs-boot' | grep -v '^contrib/')
ORMOLUFLAGS?=--no-cabal
ORMOLUMODE?=inplace
.PHONY: format
format: clang-format
.PHONY: ormolu
ormolu:
@${ORMOLU} ${ORMOLUFLAGS} \
--ghc-opt -XStandaloneDeriving \
--ghc-opt -XUnicodeSyntax \
@ -142,6 +113,11 @@ format: clang-format
--mode ${ORMOLUMODE} \
$(ORMOLUFILES)
.PHONY: format
format:
@${MAKE} clang-format
@${MAKE} ormolu
.PHONY: clang-format
clang-format:
@cd runtime && ${MAKE} format
@ -149,8 +125,6 @@ clang-format:
TOFORMATJUVIXFILES = ./examples
TOFORMAT = $(shell find ${TOFORMATJUVIXFILES} -name "*.juvix" -print)
.PHONY: $(TOFORMAT)
juvix-format: $(TOFORMAT)
$(TOFORMAT): %:
@echo "Formatting $@"
@juvix dev scope $@ --with-comments > $@.tmp
@ -158,10 +132,14 @@ $(TOFORMAT): %:
@echo "Typechecking formatted $@"
@juvix typecheck $@ --only-errors
.PHONY: $(TOFORMAT)
juvix-format:
@${MAKE} $(TOFORMAT)
.PHONY: check-ormolu
check-ormolu: export ORMOLUMODE = check
check-ormolu:
@${MAKE} format
@${MAKE} ormolu
HLINT?=stack exec -- hlint
HLINTFLAGS?=

144
README.md Normal file
View File

@ -0,0 +1,144 @@
# Juvix
<a href="https://github.com/anoma/juvix"><img align="right" width="300" alt="Tara the Juvix mascot" src="assets/images/tara-seating.svg" /></a>
<!-- prettier-ignore -->
| CI Status |
| --------- |
|<a href="https://github.com/anoma/juvix/actions/workflows/ci.yml"><img alt="CI status" src="https://github.com/anoma/juvix/actions/workflows/ci.yml/badge.svg" /> </a> |
|<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg" alt="pages-build-deployment" /></a>|
<!-- prettier-ignore -->
| Codebase |
| -------- |
|<a href="https://github.com/anoma/juvix/tags"><img src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases"/></a>|
|<a href="https://github.com/anoma/juvix/blob/main/LICENSE"><img src="https://img.shields.io/badge/license-GPL--3.0--only-blue.svg"/></a> |
|<a href="https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope"><img height="20pt" alt="Open the Juvix Standard Lib in Github Codespace" src="https://github.com/codespaces/badge.svg"/> </a>|
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][vampir] to circuits for private execution with [Taiga][taiga] on [Anoma][anoma] or Ethereum.
## Getting Started
To get started with Juvix, head over to the [documentation website][juvix-book]
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][latest-release] from the
Juvix GitHub repository or use the web-based development environment, [Juvix
Github Codespace][repo-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][stdlib]. For further details,
please refer to [the Juvix book][juvix-book] which includes
our [latest updates][changelog].
## Related projects
If you're interested in Juvix, you may also want to explore the following related projects:
<!-- prettier-ignore -->
| Project | Description |
| ------- | ----------- |
| [GEB][geb] | Intermediate language for writing compilers and one of the Juvix backends. |
| [VampIR][vampir] | Proof-system-agnostic language for writing arithmetic circuit and one of the GEB backends.|
| [Taiga][taiga] | A framework for generalized shielded state transitions. |
## Resources
Here is a summary of resources to help you learn more about Juvix:
### Documentation
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [Official website][website] | The official website of Juvix, where you can find documentation, changelog, tutorials, and community resources. |
| [GitHub repository][repo] | The official GitHub repository of Juvix, where you can find the source code and contribute to the project. |
### Community
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [Discord community][discord] | The Juvix community on Discord is a space where you can connect with the developers behind Juvix and other members of the community who are passionate about privacy-preserving decentralized applications. It's a place where you can ask for help with using Juvix, discuss the latest features and updates, and get involved in the project. |
| [Twitter][twitter] | The official Twitter account of Juvix, where you can stay up-to-date with the latest news and announcements. |
### Libraries
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [Standard library][stdlib] | The Juvix standard library is a collection of pre-written functions and modules that come bundled with the Juvix programming language. It provides developers with a set of common and useful tools that they can use to build their Juvix programs without having to write everything from scratch. |
### IDE support
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [VSCode extension][vscode-plugin] | Support for the Juvix programming language with features such as syntax highlighting, error checking and many more directly in the VSCode editor.
| [Emacs Juvix mode][juvix-mode] | A major mode for Emacs that provides support for writing Juvix programs. |
### Development environments
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [Juvix Standard Lib Codespace][stdlib-codespace] | A web-based development environment for the Juvix standard library on GitHub. It provides a pre-configured workspace with the Juvix standard library installed and ready to use, so you can start using the library in your projects. Some examples of Juvix programs are also loaded in this environment. |
| [Juvix Github Codespace][repo-codespace] | This codespace provides a pre-configured workspace with Juvix and the Haskell toolchain installed. Everything is ready to use, so you can start developing/inspecting the Juvix compiler right away. |
### Installation
<!-- prettier-ignore -->
| Resource | Description |
| -------- | ----------- |
| [Homebrew Juvix formula][juvix-formula] | A formula for [Homebrew][homebrew], a package manager for macOS and Linux, that allows you to easily install Juvix on your system. |
| [Juvix Nightly builds][nightly-builds] | Users can download and use these nightly builds to experiment with the latest changes to the Juvix Compiler. Nightly builds may contain new features, bug fixes, and other improvements to Juvix that are still in development and have not yet been released in an official version.|
## Contributing
If you're interested in contributing to Juvix, please see the [contributing guidelines](CONTRIBUTING.md) 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](LICENSE.md) file for more information.
[anoma]: https://anoma.net
[changelog]: https://anoma.github.io/juvix/changelog.html
[discord]: https://discord.gg/PfaaFVErHt
[geb]: https://github.com/anoma/geb
[homebrew]: https://brew.sh
[juvix-book]: https://docs.juvix.org
[juvix-formula]: https://github.com/anoma/homebrew-juvix
[juvix-mode]: https://github.com/anoma/juvix-mode
[latest-release]: https://github.com/anoma/juvix/releases/latest
[nightly-builds]: https://github.com/anoma/nightly-juvix-builds
[repo-codespace]: https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope
[repo]: https://github.com/anoma/juvix
[stdlib-codespace]: https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope
[stdlib]: https://github.com/anoma/juvix-stdlib
[taiga]: https://github.com/anoma/taiga
[twitter]: https://twitter.com/juvixlang
[vampir]: https://github.com/anoma/vamp-ir
[vscode-plugin]: https://github.com/anoma/vscode-juvix
[website]: https://juvix.org

84
README.org
View File

@ -1,84 +0,0 @@
* Juvix
#+begin_html
<a href="https://github.com/anoma/juvix/actions/workflows/ci.yml">
<img alt="CI status" src="https://github.com/anoma/juvix/actions/workflows/ci.yml/badge.svg" />
</a>
#+end_html
#+begin_html
<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img
src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg"
alt="pages-build-deployment" /></a>
#+end_html
#+begin_html
<a href="https://github.com/anoma/juvix/tags">
<img alt="" src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases" />
</a>
#+end_html
#+begin_html
<a href="https://github.com/anoma/juvix/blob/main/LICENSE">
<img alt="LICENSE" src="https://img.shields.io/badge/license-GPL--3.0--only-blue.svg" />
</a>
#+end_html
#+begin_html
<a href="https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=455254004">
<img height="20pt" alt="Open the Juvix Standard Lib in Github Codespace" src="https://github.com/codespaces/badge.svg" />
</a>
#+end_html
#+begin_html
<a href="https://github.com/anoma/juvix">
<img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/images/tara-seating.svg" />
</a>
#+end_html
** Description
Juvix is a research programming language created by [[https://heliax.dev/][Heliax]] as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling [[https://anoma.network/blog/validity-predicates/][validity predicates]] to [[https://webassembly.org/][WebAssembly]], which can be deployed to various distributed ledgers including [[https://anoma.net/][Anoma]].
The Juvix language and related tools are documented in [[https://anoma.github.io/juvix/][the Juvix book]]. To write
and test Juvix programs, you can use your favorite text editor, the =juvix=
command line tool, the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Github Codespace]], and the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Standard Lib Codespace]]. However, we recommend using the =juvix-mode= in [[https://docs.juvix.org/reference/tooling/emacs.html][Emacs]] or the
plugin in [[https://github.com/anoma/vscode-juvix][VSCode]].
** Quick start
See [[https://docs.juvix.org/quick-start.html][Quick start]] to start with Juvix.
** The Juvix programming language
Juvix provides a high degree of assurance. The Juvix compiler runs
several static analyses which guarantee the absence of runtime
errors. Analyses performed include termination, arity, and type
checking. As a result, functional programs, especially validity
predicates, can be written with greater confidence in their
correctness.
Some of the language features in Juvix include:
- unicode syntax
- parametric polymorphism
- inductive and parametric data types
- higher-order functions
- implicit arguments
- holes in expressions
- axioms for non-computable terms
The Juvix module system further permits splitting programs into
several modules to build libraries which can be later documented by
generating HTML files based on the codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the
Juvix standard library's website]]. For further details, please refer to
[[https://anoma.github.io/juvix/][the Juvix book]] which includes our [[https://anoma.github.io/juvix/changelog.html][latest updates]].
** Community
Join us on our [[https://discord.gg/PfaaFVErHt][Discord server]]!
Juvix is part of a bigger effort called [[https://anoma.net/][Anoma]].
Anoma is an intent-centric, privacy-preserving protocol for decentralized counterparty discovery, solving, and multi-chain atomic settlement.
Join the [[https://anoma.net/community][Anoma project]].

57
book.toml
View File

@ -3,15 +3,58 @@ title = "The Juvix Book"
authors = [ "Jonathan Prieto-Cubides" , "Jan Mas Rovira" , "Paul Cadman" , "Lukasz Czajka" ]
language = "en"
multilingual = false
src = "docs/md/"
src = "docs"
[build]
build-dir = "_docs"
create-missing = true
[output.html]
mathjax-support = true
[preprocessor.index]
[preprocessor.toc]
command = "mdbook-toc"
renderer = ["html"]
[preprocessor.links]
[preprocessor.pagetoc]
[preprocessor.katex]
renderers = ["html"]
static-css = false
include-src = false
block-delimiter = {left = "$$", right = "$$"}
inline-delimiter = {left = "$", right = "$"}
macros = "theme/latex-macros.txt"
[output.katex]
[output.html]
default-theme = "light"
preferred-dark-theme = "Ayu"
copy-fonts = true
additional-css = ["theme/pagetoc.css"]
additional-js = ["theme/pagetoc.js","assets/images/tara-magicien.png", "assets/images/tara-seating.svg", "assets/images/tara-smiling.png", "assets/images/tara-smiling.svg", "assets/images/tara-teaching.png", "assets/images/tara-teaching.svg", "assets/js/highlight.js", "assets/js/tex-chtml.js" ]
no-section-label = false
git-repository-url = "https://github.com/anoma/juvix"
git-repository-icon = "fa-github"
[output.html.fold]
enable = true # whether or not to enable section folding
level = 0 # the depth to start folding
[output.html.search]
enable = true # enables the search feature
limit-results = 15 # maximum number of search results
teaser-word-count = 30 # number of words used for a search result teaser
use-boolean-and = true # multiple search terms must all match
boost-title = 2 # ranking boost factor for matches in headers
boost-hierarchy = 1 # ranking boost factor for matches in page names
boost-paragraph = 1 # ranking boost factor for matches in text
expand = true # partial words will match longer terms
heading-split-level = 2 # link results to heading levels
copy-js = true # include Javascript code for search
[output.linkcheck]
follow-web-links = false
traverse-parent-directories = false
exclude = [ ]
user-agent = "mdbook-linkcheck-0.4.0"
cache-timeout = 43200
[output.linkcheck.http-headers]
'crates\.io' = ["Accept: text/html"]

1528
changelog.org
View File

File diff suppressed because it is too large Load Diff

53
docs/SUMMARY.md Normal file
View File

@ -0,0 +1,53 @@
# Summary
- [The Juvix project](./README.md)
- [Changelog](./CHANGELOG.md)
- [Quick start](./quick-start.md)
# Tutorials
- [Learn Juvix in minutes](./tutorials/learn.md)
- [Structuring Juvix projects](./tutorials/structure.md)
- [Juvix Emacs mode](./tutorials/emacs.md)
- [Juvix VSCode extension](./tutorials/vscode.md)
# How-to guides
- [Installing Juvix](./howto/installing.md)
- [Compiling Juvix programs](./howto/compilation.md)
- [Judoc: Juvix documentation tool](./howto/judoc.md)
# Explanations
- [Type theory](./explanations/typetheory.md)
- [Totality checking](./explanations/totality/README.md)
- [Termination](./explanations/totality/termination.md)
- [Strictly positive data
types](./explanations/totality/positive.md)
- [Coverage checking](./explanations/totality/coverage.md)
# Reference
- [Standard library](./reference/stdlib.md)
- [Language reference](./reference/language/README.md)
- [Functions](./reference/language/functions.md)
- [Data types](./reference/language/datatypes.md)
- [Modules](./reference/language/modules.md)
- [Local definitions](./reference/language/let.md)
- [Control structures](./reference/language/control.md)
- [Comments](./reference/language/comments.md)
- [Axioms](./reference/language/axioms.md)
- [Example programs](./reference/examples.md)
- [Benchmarks](./reference/benchmarks.md)
- [Tooling](./reference/tooling/README.md)
- [Command line interface](./reference/tooling/CLI.md)
- [Doctor](./reference/tooling/doctor.md)
- [Emacs mode](./reference/tooling/emacs.md)
- [Haskell test suite](./reference/tooling/testing.md)
- [Judoc reference](./reference/judoc.md)
# About
- [Community](./about/community.md)
- [Contributing](./CONTRIBUTING.md)
- [License](./LICENSE.md)

8
docs/about/community.md Normal file
View File

@ -0,0 +1,8 @@
# Juvix community
Join us on our [Discord server](https://discord.gg/waYhQ2Qr)
This project is part of a bigger effort called
[Anoma](https://anoma.net/). Anoma is a suite of protocols and
mechanisms for self-contained, self-sovereign coordination. Join the
[Anoma project](https://anoma.net/community).

1
docs/about/team.md Normal file
View File

@ -0,0 +1 @@
# The Juvix Dev Team

1388
docs/changelog.md Normal file
View File

File diff suppressed because it is too large Load Diff

15
docs/examples/README.md Normal file
View File

@ -0,0 +1,15 @@
## [Examples of programs written in Juvix](https://github.com/anoma/juvix/tree/main/examples/milestone)
The following links are clickable versions of their corresponding Juvix
programs. The HTML output can be generated by running
`juvix html --recursive FileName.juvix`.
- [HelloWorld.juvix](https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html)
- [Fibonacci.juvix](https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html)
- [Hanoi.juvix](https://docs.juvix.org/examples/html/Hanoi/Hanoi.html)
- [PascalsTriangle.juvix](https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html)
- [Collatz.juvix](https://docs.juvix.org/examples/html/Collatz/Collatz.html)
- [TicTacToe.juvix](https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html)
The [Juvix standard library](https://anoma.github.io/juvix-stdlib/)
contains common functions that can be used in Juvix programs.

1
docs/explanations/totality/README.md Normal file
View File

@ -0,0 +1 @@
# Totality checking

1
docs/explanations/totality/coverage.md Normal file
View File

@ -0,0 +1 @@
# Coverage checking

1
docs/explanations/totality/positive.md Normal file
View File

@ -0,0 +1 @@
# Strictly positive data types

29
docs/explanations/totality/termination.md Normal file
View File

@ -0,0 +1,29 @@
# 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.
```juvix
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
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.

1
docs/explanations/typetheory.md Normal file
View File

@ -0,0 +1 @@
# Type theory

51
docs/howto/compilation.md Normal file
View File

@ -0,0 +1,51 @@
# 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`:
```juvix
-- 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](https://anoma.github.io/geb/) input file.
# Juvix projects
A <u>Juvix project</u> 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](../reference/language/modules.md).

135
docs/howto/installing.md Normal file
View File

@ -0,0 +1,135 @@
# Dependencies
You need [Clang / LLVM](https://releases.llvm.org/download.html) 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](https://wasmer.io)
- [wasi-sdk](https://github.com/WebAssembly/wasi-sdk/releases)
- [wasm-ld](https://lld.llvm.org) - 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](./installing.md#installing-dependencies) for instructions on
how to install the dependencies.
# Installing Juvix
### MacOS
The easiest way to install Juvix on MacOS is by using
[Homebrew](https://brew.sh).
To install the [homebrew-juvix
tap](https://github.com/anoma/homebrew-juvix), run:
```shell
brew tap anoma/juvix
```
To install Juvix, run:
```shell
brew install juvix
```
Helpful information can also be obtained by running:
```shell
brew info juvix
```
### Linux x86<sub>64</sub>
A Juvix compiler binary executable for Linux x86<sub>64</sub> is
available on the [Juvix release
page](https://github.com/anoma/juvix/releases/latest).
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:
```shell
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](https://github.com/anoma/juvix.git). Then Juvix can be
installed with the following commands. We assume you have
[Stack](https://haskellstack.org) and [GNU
Make](https://www.gnu.org/software/make/) installed.
```shell
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.
```shell
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.
```shell
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](https://github.com/sol/hpack)
before running `cabal build`.
You also need to compile the runtime first:
```shell
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](https://github.com/WebAssembly/wasi-sdk/releases/) 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:
```shell
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:
```shell
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
```

1
docs/howto/judoc.md Normal file
View File

@ -0,0 +1 @@
# Documenting Juvix programs with Judoc

0
docs/org/notes/README.org → docs/notes/README.md
View File

82
docs/notes/builtins.md Normal file
View File

@ -0,0 +1,82 @@
---
author: Jan Mas Rovira
title: Builtins
---
# Overview
The goal is to support builtin types and functions that get compiled to
efficient primitives. We plan on supporting primitives for the following
types of definitions:
1. Builtin inductive definitions. For example:
```juvix
builtin nat
type Nat :=
zero : Nat |
suc : Nat → Nat;
```
We will call this the canonical definition of natural numbers.
2. Builtin function definitions. For example:
```juvix
inifl 6 +;
builtin nat-plus
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
```
3. Builtin axiom definitions. For example:
```juvix
builtin nat-print
axiom printNat : Nat → Action;
```
## Collecting builtin information
The idea is that builtin definitions are treated normally throughout the
pipeline except in the backend part. There is one exception to that. We
need to collect information about the builtins that have been included
in the code and what are the terms that refer to them. For instance,
imagine that we find this definitions in a juvix module:
```juvix
builtin nat
type MyNat :=
z : MyNat |
s : MyNat → MyNat;
```
We need to take care of the following:
1. Check that the definition `MyInt` is up to renaming equal to the
canonical definition that we provide in the compiler.
2. Rember a map from concrete to canonical names: {MyNat ↦ Nat; z ↦
zero; s ↦ suc};
3. Rembember that we have a definition for builtin natural numbers.
This is necessary if later we attempt to define a builtin function
or axiom that depends on natural numbers.
In the compiler we need to know the following:
1. For inductives:
1. What is the primitive type that we will target in the backend:
E.g. {Nat ↦ int}.
2. For constructors:
1. What is the primitive constructor function: E.g. {zero ↦ 0;
suc ↦ plus<sub>one</sub>};
2. How to test if a term matches a pattern with that
constructor. E.g. {zero ↦ is<sub>zero</sub>; suc ↦
is<sub>notzero</sub>};
3. How to deconstruct/project each of the constructor
arguments. E.g. {zero ↦ ∅; suc ↦ minus<sub>one</sub>}}. Note
that if a constructor takes multiple arguments we will need
to have a projection function for each argument.
2. For functions and axioms:
1. What is the primitive function that we will target in the
backend: E.g. {+ ↦ add}.

16
docs/notes/lsp.md Normal file
View File

@ -0,0 +1,16 @@
# LSP support
We provide a sample `hie.yaml` configuration file for both `cabal` and
`stack`.
If you prefer `stack`, run:
```shell
cp stack.hie.yaml hie.yaml
```
If you prefer `cabal`, run:
```shell
cp cabal.hie.yaml hie.yaml
```

228
docs/notes/monomorphization.md Normal file
View File

@ -0,0 +1,228 @@
---
author: Jan Mas Rovira
---
# Monomorphization
(Removed in v0.2.5)
Monomorphization refers to the process of converting polymorphic code to
monomorphic code (no type variables) through static analysis.
Example:
```juvix
id : (A : Type) → A → A;
id _ a := a;
b : Bool;
b := id Bool true;
n : Nat;
n := id Nat zero;
```
Is translated into:
```juvix
id_Bool : Bool → Bool;
id_Bool a := a;
id_Nat : Nat → Nat;
id_Nat a := a;
```
# More examples
## Mutual recursion
```juvix
type List (A : Type) :=
nil : List A |
cons : A → List A → List A;
even : (A : Type) → List A → Bool;
even A nil := true ;
even A (cons _ xs) := not (odd A xs) ;
odd : (A : Type) → List A → Bool;
odd A nil := false ;
odd A (cons _ xs) := not (even A xs) ;
-- main := even Bool .. odd Nat;
```
# Collection algorithm
This section describes the algorithm to collect the list of all concrete
functions and inductive definitions that need to be generated.
## Assumptions:
1. Type abstractions only appear at the leftmost part of a type
signature.
2. All functions and constructors are fully type-applied: i.e. currying
for types is not supported.
3. There is at least one function with a concrete type signature.
4. All axioms are monomorphic.
5. No module parameters.
## Definitions
1. **Application**. An application is an expression of the form
`t₁ t₂ … tₙ` with n > 0.
2. **Sub application**. If `t₁ t₂ … tₙ` is an application then for
every `0<i<n` `t₁ t₂ … tᵢ` is a sub application.
Fix a juvix program `P`. Let `𝒲` be the set of all applications that
appear in `P`.
1. **Maximal application**. A maximal application is an application
`A∈𝒲` such that for every `A'∈𝒲` we have that `A` is **not** a sub
application of `A'`.
2. **Type application**. If
1. `t a₁ a₂ … aₙ` is a maximal application; and
2. `t` is either a function or an inductive type; and
3. `a₁, …, aₘ` are types; and
4. `aₘ₊₁` is not a type or `m = n`.
Then `t a₁, …, aₘ` is a type application.
3. **Concrete type**. A type is concrete if it involves no type
variables.
4. **Concrete type application**. A type application `t a₁ a₂ … aₙ` if
`a₁, a₂, …,
aₙ` are concrete types.
## Option 1
Let `S₀` be the set of functions with a concrete type signature. Gather
all type applications (both in the type and in the body) in each of the
functions in `S₀`. Clearly the collected type applications are all
concrete. We now have a stack `c₁, c₂, …, cₙ` of concrete type
applications.
1. If the stack is empty, we are done.
2. Otherwise pop `c₁` from the stack. It will be of the form
`t a₁ … aₘ`, where `t` is either an inductive or a function and
`a₁, …, aₘ` are concrete types.
3. If the instantiation `t a₁ … aₘ` has already been registered go to
step 1. Otherwise continue to the next step.
4. Register the instantiation `t a₁ … aₘ`.
5. If `t` is a function, then it has type variables `v₁, …, vₘ`.
Consider the substitution `σ = {v₁ ↦ a₁, …, vₘ ↦ aₘ}`. Consider the
list of type applications in the body of `t`: `d₁, …, dᵣ`. Add
`σ(d₁), …, σ(dᵣ)` to the stack and continue to step 1. It is easy to
see that for any `i`, `σ(dᵢ)` is a concrete type application.
6. If `t` is an inductive type, let `d₁, …, dᵣ` be the type
applications that appear in the type of its constructors, then
proceed as before.
### Correctness
It should be clear that the algorithm terminates and registers all
instantiations of constructors and functions.
# Generation algorithm
The input of this algorithm is the list of concrete type applications,
name it `ℒ`, produced by the collection algorithm. Example:
```juvix
List String
Pair Int Bool
Maybe String
Maybe Int
if (Maybe String)
if (Maybe Int)
if (Pair Int Bool)
```
## Name generation
Let `f â` be an arbitrary element of `ℒ`, where `â` is a list of
concrete types.
- If `f` is a function, assign a fresh name to `f â`, call it
`⋆(f â)`.
- If `f` is an inductive type, assign a fresh name to `f â`, call it
`⋆(f â)`. Then, for each constructor `cᵢ` of `f`, where `i` is the
index of the constructor, assign a fresh name to it and call it
`⋆ᵢ(f â)`.
## Function generation
Consider an arbitrary function `f` in the original program. Then
consider the list of concrete type applications involving `f`:
`f â₁, …, f âₙ`.
- If `n = 0`, then either:
1. `f` has a concrete type signature, in that case we proceed as
expected.
2. `f` is never called from the functions with a concrete type. In
this case we can safely ignore it.
- If `n > 1`. For each `âᵢ` we proceed as follows in the next
sections. Fix `m` to be the lenght of `âᵢ` with `m > 0`.
### Function name
The name of the monomorphized function is `⋆(f âᵢ)`.
### Type signature
Let `𝒮` be the type signature of `f`. Then `𝒮` has to be of the form
`(A₁ :
Type) → … → (Aₘ : Type) → Π`, where `Π` is a type with no type
abstractions. Now consider the substitution
`σ = {A₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]}`. Since `âᵢ` is a list of concrete
types, it is clear that `σ(Π)` is a concrete type. Then proceed as
described in <span class="spurious-link" target="Types">_Types_</span>.
### Function clause
Let `𝒞` be a function clause of `f`. Let `p₁ … pₖ` with `k ≥ m` be the
list of patterns in `𝒞`. Clearly the first `m` patterns must be either
variables or wildcards. Wlog assume that the first `m` patterns are all
variables, namely `v₁, …, vₘ`. Let `σ = {v₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]}` be
a substitution. Let `e` be the body of `𝒞`, then clearly `σ(e)` has no
type variables in it. Now, since each name id must be bound at most
once, we need to generate new ones for the local variables bound in the
patterns `pₘ₊₁, …, pₖ`. Let `w₁, …, wₛ` be the variables bound in
`pₘ₊₁, …, pₖ`. Let `w'₁, …, w'ₛ` be fresh variables. Then let
`δ = {w₁ ↦ w'₁, …, wₛ ↦ w'ₛ}`.
Now let `𝒞'` have patterns `δ(pₘ₊₁), …, δ(pₖ)` and let `e' :` (σ ∪
δ)(e)=. It should be clear that `e'` has no type variables in it and
that all local variable references in `e'` are among `w'₁, …, w'ₛ`. Note
that `e'` is not yet monomorphized. Proceed to the next step to achieve
that.
### Expressions
The input is an expression `e` that has no type variables in it. The
goal is to replace the concrete type applications by the corresponding
monomorphized expression.
The only interesting case is when we find an application. Consider the
unfolded view of the application: `f a₁ … aₘ`. Then, if `f` is either a
constructor, or a function, let `A₁, …, Aₖ` with `k ≤ m` be the list of
type parameters of `f`.
- If `f` is a function and `f a₁ … aₖ ∉ ℒ` then recurse normally,
otherwise, let `â :` a₁ … aₖ= and replace the original expression
`f a₁ … aₘ`, by `⋆(f â)
aₖ₊₁' … aₘ'` where `aₖ₊₁' … aₘ'` are the monomorphization of
`aₖ₊₁ … aₘ` respectively.
- If `f` is a constructor, let `d` be its inductive type. Then check
`d a₁ … aₖ
∈ ℒ`. Proceed analogously as before.
### Types
The input is a type `t` that has no type variables in it. The goal is to
replace the concrete type applications by the corresponding
monomorphized type. Proceed analogously to the previous section.

343
docs/notes/runtime-benchmark-results.md Normal file
View File

@ -0,0 +1,343 @@
# Benchmarks of the new Juvix runtime
Benchmarked version: commit 148ececb4d4259eacbb980f5992073a3ac611d82
from 31.10.2022
## Summary
We benchmark several programs manually compiled into the primitives of
the new Juvix runtime. The code corresponds closely to the code that
will be generated by the new compilation process, with basic low-level
optimisations (unboxing, untagging, etc.) but without any high-level
optimisations on JuvixCore (inlining, specialisation, constant folding,
fusion, etc.). This corresponds to the compilation process planned for
the 0.4 milestone.
We compare the running time and memory usage with analogous programs
written in Haskell, OCaml, JuvixCore (using the evaluator), current
Juvix (with the "direct" transpilation to C) and C.
The results suggest that for most first-order programs the new
compilation process will produce code with running time comparable to
the code produced by the native OCaml compiler. For higher-order
programs heavy on closure manipulation, the results are acceptable but
noticeably worse, especially with third-order functions (i.e. functions
which take functions taking functions). This could, however, be
alleviated by implementing the specialisation optimisation (see the
"specialised" column in the \`ackermann\` and \`mapfun\` benchmarks).
Besides, functional programs of order higher than two are rare.
The comparisons with OCaml and Haskell were not entirely fair because
the new Juvix runtime does not perform garbage collection. The overhead
of garbage collection is particularly visible on the \`mergesort\`
benchmark which creates many intermediate data structures that are
quickly discarded. With proper memory management, the running time
results on first-order programs for the new Juvix runtime are expected
to become slightly worse than for the native OCaml compiler.
For simple programs operating on integers which don't require any heap
memory allocation (\`fibonacci\` and \`combinations\` benchmarks), the
direct transpilation to C in the current Juvix seems to perform best
(behind only C). The reason is that for very simple programs \`clang\`
can better optimise the output of such a direct transpiler. The main
problem with the transpilation to C approach is that it cannot scale to
reliably work for more complex programs, as evidenced by the segfaults,
longer running time and higher memory use on other benchmarks.
In addition to the \`fibonacci\` and \`combinations\` benchmarks, the
advantage of direct transpilation for very simple programs is also
visible on the \`fold\` benchmark where a simple loop over a list
dominates the running time. However, this is partly because the
compilation of closures in current Juvix is incorrect allowing it to be
more efficient.
## Benchmark programs
# fibonacci: compute the Nth Fibonacci number modulo 2<sup>28</sup> (N = 100’000’000)
The Nth Fibonacci number is computed in O(N). Needs only constant stack
space and no heap memory. This benchmark tests the efficiency of tail
recursion and arithmetic operations.
# combinations: count combinations of numbers 1 to N having sum N (N = 100)
This benchmark tests the efficiency of general recursion. No heap memory
needs to be allocated. Uses stack space proportional to N. The running
time is exponential in N.
# prime: compute the Nth prime (N = 16384)
The Nth prime number is computed via the Eratosthenes sieve. A list of N
primes is created. No intermediate lists are discarded (garbage
collection not needed). This benchmark tests the efficiency of tail
recursion, arithmetic operations, list cell allocation and access.
# mergesort: merge sort a list of N integers (N = 2’000’000)
At each level of merge sort intermediate lists are created and
discarded. The running time for this benchmark largely depends on the
efficiency of memory management. Here one may observe the overhead of
garbage collection or the memory blow-up if no garbage collection is
used.
# maybe: optionally sum N integers from a binary tree K times (N = 2<sup>20</sup>, K = 100)
If a fixed number k is encountered in the tree then the result is
\`Nothing\`, otherwise it is \`Just sum\`. The computation is repeated
for values of k from 0 to K. This tests the efficiency of handling
optional values and data structure access.
# fold: fold a list of N integers K times (N = 100’000, K = 1000)
The sum of N natural numbers is computed via fold<sub>left</sub>
(tail-recursive). The computation is repeated K times. The list is
created only once, so that allocation time does not dominate. This
benchmark tests the efficiency of closure call and list cell access.
# cps: compute the Nth Fibonacci number modulo 2<sup>28</sup> with CPS (N = 100’000’000)
The function computing the Nth Fibonacci number is written in
continuation-passing style, tail-recursively calling a continuation
supplied as an argument. This benchmark tests the efficiency of closure
call and allocation.
# mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
This benchmark tests the efficiency of standard higher-order functions
on lists, closure call and memory management. The program allocates O(K)
intermediate lists of length N which are quickly discarded.
# ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
The higher-order Ackermann function definition iterates an iteration of
function compositions. Hence, it uses a third-order invocation of an
iteration function. This benchmark tests the efficiency of creating and
calling second-order closures, and of partial application.
# mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
The benchmark stores K second-order closures in a list, maps them
successively to a list of K closures, and then successively maps the K
closures from the result to a list of N integers. This benchmark tests
the efficiency of manipulating closures and storing them in data
structures.
The benchmark programs can be found in \`tests/benchmark\` in the Juvix
source directory.
## Methodology
For each program the total running time (elapsed real time) and memory
use (maximum resident set size) were measured on an M1 iMac with no
significant background activity. Averages of several runs were taken.
The variance was negligible, unless indicated otherwise by providing a
range.
## Results
# fibonacci: compute the Nth Fibonacci number modulo 2<sup>28</sup> (N = 100’000’000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.26 | 0.35 | 0.35 | 0.23 | 13.15 | 10.03 | 0.39 | 0.35 | 0.94 | 0.16 | 0.22 |
| Memory use (MB, max RSS) | 1.5 | 3.8 | 1.3 | 8.8 | 21.3 | 8067.7 | 9.7 | 1.7 | 1.8 | 1.3 | 4.0 |
# combinations: count all combinations of numbers 1 to N having sum N (N = 1000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 6.67 | 11.25 | 3.22 | 5.1 | 441.71 | 5.48 | 5.48 | 6.53 | 41.08 | 2.69 | 4.80 |
| Memory use (MB, max RSS) | 1.5 | 3.9 | 1.3 | 8.9 | 22.3 | 9.6 | 9.6 | 1.7 | 1.9 | 1.3 | 4.0 |
# prime: compute the Nth prime (N = 16384)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 1.52 | 1.91 | segfault | 3.09 | 167.04 | 3.85 | 3.85 | 1.68 | 14.82 | 0.12 | 0.13 |
| Memory use (MB, max RSS) | 1.7 | 4.0 | segfault | 9.3 | 24.4 | 9.8 | 9.6 | 2.2 | 2.2 | 1.4 | 4.0 |
# mergesort: merge sort a list of N integers (N = 2’000’000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.40 | 0.31 | 3.55 | 1.32 | 22.45 | 2.86 | 2.90 | 1.95 | 3.52 | 0.15 | 0.15 |
| Memory use (MB, max RSS) | 1973.7 | 720.4 | 5046.7 | 2729.8 | 1728.9 | 253.6 | 253.6 | 172.6 | 343.1 | 24.4 | 26.8 |
# maybe: optionally sum N non-zero integers from a binary tree K times (N = 2<sup>20</sup>, K = 100)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.45 | 0.64 | 3.29 | 1.57 | 22.75 | 5.58 | 0.59 | 0.30 | 3.57 | 0.27 | 0.50 |
| Memory use (MB, max RSS) | 1.6 | 3.8 | 2646.1 | 1320.9 | 22.4 | 5560.7 | 9.7 | 3.9 | 4.0 | 1.3 | 4.1 |
# fold: fold a list of N integers K times (N = 100’000, K = 1000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.45 | 0.54 | 0.35 | 0.23 | 15.27 | 0.58 | 0.58 | 0.36 | 1.80 | NA | NA |
| Memory use (MB, max RSS) | 3.1 | 4.6 | 4.4 | 10.6 | 43.4 | 12.7 | 12.7 | 5.9 | 5.9 | NA | NA |
# cps: compute the Nth Fibonacci number modulo 2<sup>28</sup> with CPS (N = 100’000’000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.43 | 0.52 | 1.56 | stack overflow | 20.22 | 10.04 | 0.39 | 0.35 | 1.60 | 0.16 | 0.25 |
| Memory use (MB, max RSS) | 1.5 | 3.9 | 1539.3 | stack overflow | 21.3 | 8067.7 | 9.7 | 1.7 | 1.8 | 1.3 | 4.0 |
# mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 1.01 | 1.59 | 2.74 | 1.81 | 38.24 | 1.29 | 2.42 | 1.43 | 4.22 | NA | NA |
| Memory use (MB, max RSS) | 2154.5 | 893.0 | 3059.1 | 1542.0 | 26.4 | 10.6 | 10.7 | 7.5 | 10-20 | NA | NA |
# ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | New Juvix runtime (specialised, native) | New Juvix runtime (specialised, wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | --------------------------------------- | ----------------------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 0.92 | 1.21 | 0.30 | 0.65 | segfault | runtime error | 11.71 | 0.87 | 0.47 | 0.54 | 1.35 | 0.00 | 0.14 |
| Memory use (MB, max RSS) | 2.6 | 4.1 | 2.3 | 3.9 | segfault | runtime error | 23.3 | 13.6 | 9.6 | 2.0 | 3.6 | 1.3 | 4.0 |
# mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | New Juvix runtime (specialised, native) | New Juvix runtime (specialised, wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
| ------------------------ | -------------------------- | ---------------------------------- | --------------------------------------- | ----------------------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
| Time (seconds, real) | 1.27 | 1.04 | 0.39 | 0.46 | segfault | runtime error | 4.18 | 1.85 | 0.95 | 0.19 | 0.68 | NA | NA |
| Memory use (MB, max RSS) | 3209.8 | 1229.7 | 21.8 | 13.2 | segfault | runtime error | 33.0 | 13.6 | 11.6 | 5.3 | 7.9 | NA | NA |
Comments
---
# "New Juvix runtime" denotes C programs written using the primitives
of the new Juvix runtime. These programs were "manually" compiled from
the corresponding Juvix/JuvixCore programs, according to the new Juvix
compilation concept. They correspond closely to the code that will be
generated by the basic version of the new compilation process, without
any high-level optimisations (inlining, specialisation, fusion, constant
folding) but with basic low-level memory representation optimisations
(unboxing, untagging, etc). This version of the new compilation process
should be finished with the 0.4 milestone.
# The "specialised" column for "New Juvix runtime" denotes a version
of the corresponding "New Juvix runtime" benchmark program for which
specialisation of higher-order functions was manually performed (to
simulate the effects of the high-level specialisation optimisation).
# "Current Juvix" denotes Juvix programs compiled with the current
compilation process via a "direct" translation to C. For a fair
comparison, all number operations were implemented using native binary C
integers (exposed via \`foreign\` and \`compile\` blocks) without
overflow check, instead of using the unary Nat from the standard
library. For Haskell, we use the fixed-precision Int instead of the
arbitrary-precision Integer.
# For the simplest benchmark programs without heap memory allocation
(e.g. \`fibonacci\`, \`combinations\`), the performance of "Current
Juvix" is comparable to or better than that of "New Juvix runtime". This
is because \`clang\` managed to eliminate (tail) recursion and optimise
the code to essentially the same or better thing. The main problem with
the current "direct" transpilation to C approach is that it cannot scale
to reliably work for more complex programs. By "more complex" I mean
larger program size, more functions, more complex patterns of recursion
and/or the use of more functional programming features (including
functional data structures). I don't mean higher computational
complexity or more resource use.
# The segfaults and runtime errors for "Current Juvix" are
consequences of incorrectly generated code (current compilation of
partial application is not entirely correct) or stack overflows (when
\`clang\` didn't figure out how to eliminate tail recursion).
# The comparison with "Current Juvix" is not entirely fair for
benchmarks that test the manipulation and calling of closures (e.g.
\`fold\`). Current Juvix achieves good performance (when it doesn't
segfault) at the expense of correctness: partial application is not
compiled correctly and fixing this would require a fundamental change in
closure representation.
# The comparison with Haskell and OCaml compilers is not entirely
fair, because the new Juvix runtime does not perform garbage collection.
With the GC overhead, I would expect the Juvix runtime results for
native compilation of first-order programs to become a bit worse than
the native OCaml versions. The GC overhead is particularly noticeable
for the \`mergesort\` benchmark which creates many large intermediate
lists. The memory usage of the Juvix runtime is much higher on this
benchmark than the memory usage of OCaml or Haskell versions. The
relatively small time difference between the OCaml native and bytecode
versions of \`mergesort\` also indicates that GC accounts for a
significant part of the running time.
# Another small overhead will be introduced by bounds checking for
integer operations. Currently, the new Juvix runtime operates on unboxed
31-bit (or 63-bit) integers without checking for integer overflow.
# If we decide to default to transparent arbitrary-precision integers,
then another small overhead will be introduced by the need to check the
integer representation with each arithmetic operation.
# Admittedly, the programs were deliberately written in a way to make
high-level optimisations unnecessary, except specialisation for
higher-order functions (mostly in \`ackermann\` and \`mapfun\`). This
also explains the good performance of the OCaml native compiler which
doesn't do much high-level optimisation.
# In the "Current Juvix" and OCaml version of \`mergesort\`, to avoid
stack overflow the \`merge\` function was written tail-recursively with
accumulator reversal at the end. This is not necessary for the new Juvix
runtime, because the stack is dynamically extended when needed.
# As evidenced by the \`combinations\` benchmark, for non-tail-recursive
direct calls our code performs worse than the code which uses the C /
WebAssembly stack and function call mechanisms. However, in general it
is impossible to directly use the C / WebAssembly stack and call
mechanisms for a purely functional language. Since we dynamically
allocate the stack segments when needed, stack overflow is impossible.
This is convenient in an eager functional language. Otherwise, one needs
to rewrite all functions operating on large data to use tail recursion.
We pay for this convenience with a small overhead, which is the main
reason for poorer performance on \`combinations\` where stack
manipulation cost dominates.
# Haskell's laziness seems to introduce more overhead than I
expected. This would explain the comparatively better performance of the
native OCaml compiler. The problem is particularly stark when Haskell's
strictness analysis fails for some reason, as in the \`fibonacci\`
benchmark. The second "Haskell" column with the "-XStrict" flag for GHC
indicates the version of the benchmark compiled with strictness as the
default.
# The C versions of the programs were written to take advantage of C's
imperative features, e.g., using arrays instead of lists, loops instead
of recursion. No C versions are provided for some benchmarks designed to
test specifically functional language features.
# With the new Juvix runtime, the 32-bit WebAssembly version of
\`mergesort\` is faster than the 64-bit native version because it needs
roughly half as much memory (the word size is 4 bytes instead of 8). The
difference is even starker between the WebAssembly and native versions
of \`mergesort\` for "Current Juvix".
# There seems to be a memory leak in the JuvixCore evaluator. This is
what happens too often when one uses a lazy language.
# Haskell also leaks memory in the Fibonacci benchmark, despite it
being a simple tail-recursive program. It seems strictness analysis
didn't work.

77
docs/notes/strictly-positive-data-types.md Normal file
View File

@ -0,0 +1,77 @@
# Strictly positive data types
We follow a syntactic description of strictly positive inductive data
types.
An inductive type is said to be <u>strictly positive</u> if it does not
occur or occurs strictly positively in the types of the arguments of its
constructors. A name qualified as strictly positive for an inductive
type if it never occurs at a negative position in the types of the
arguments of its constructors. We refer to a negative position as those
occurrences on the left of an arrow in a type constructor argument.
In the example below, the type `X` occurs strictly positive in `c0` and
negatively at the constructor `c1`. Therefore, `X` is not strictly
positive.
```minijuvix
axiom B : Type;
type X :=
c0 : (B -> X) -> X
| c1 : (X -> X) -> X;
```
We could also refer to positive parameters as such parameters occurring
in no negative positions. For example, the type `B` in the `c0`
constructor above is on the left of the arrow `B->X`. Then, `B` is at a
negative position. Negative parameters need to be considered when
checking strictly positive data types as they may allow defining
non-strictly positive data types.
In the example below, the type `T0` is strictly positive. However, the
type `T1` is not. Only after unfolding the type application `T0 (T1 A)`
in the data constructor `c1`, we can find out that `T1` occurs at a
negative position because of `T0`. More precisely, the type parameter
`A` of `T0` is negative.
```minijuvix
type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
type T1 := c1 : T0 T1 -> T1;
```
## Bypass the strict positivity condition
To bypass the positivity check, a data type declaration can be annotated
with the keyword `positive`. Another way is to use the CLI global flag
`--no-positivity` when type checking a `Juvix` File.
```juvix
$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
module E5;
positive
type T0 (A : Type) :=
c0 : (T0 A -> A) -> T0 A;
end;
```
## Examples of non-strictly data types
- `Bad` is not strictly positive because of the negative parameter
`A` of `Tree`.
```juvix
type Tree (A : Type) :=
leaf : Tree A
| node : (A -> Tree A) -> Tree A;
type Bad :=
bad : Tree Bad -> Bad;
```
- `A` is a negative parameter.
```juvix
type B (A : Type) :=
b : (A -> B (B A -> A)) -> B A;
```

45
docs/org/SUMMARY.org
View File

@ -1,45 +0,0 @@
* Summary
- [[./README.md][The Juvix project]]
- [[./changelog.md][Changelog]]
- [[./quick-start.md][Quick start]]
* Tutorials
- [[./tutorials/learn.md][Learn Juvix in minutes]]
- [[./tutorials/structure.md][Structuring Juvix projects]]
- [[./tutorials/emacs.md][Juvix Emacs mode]]
- [[./tutorials/vscode.md][Juvix VSCode extension]]
* How-to guides
- [[./howto/installing.md][Installing Juvix]]
- [[./howto/compilation.md][Compiling Juvix programs]]
- [[./howto/judoc.md][Judoc: Juvix documentation tool]]
* Explanations
- [[./explanations/typetheory.md][Type theory]]
- [[./explanations/totality/README.md][Totality checking]]
- [[./explanations/totality/termination.md][Termination]]
- [[./explanations/totality/positive.md][Strictly positive data types]]
- [[./explanations/totality/coverage.md][Coverage checking]]
* Reference
- [[./reference/stdlib.md][Standard library]]
- [[./reference/language/README.md][Language reference]]
- [[./reference/language/functions.md][Functions]]
- [[./reference/language/datatypes.md][Data types]]
- [[./reference/language/modules.md][Modules]]
- [[./reference/language/let.md][Local definitions]]
- [[./reference/language/control.md][Control structures]]
- [[./reference/language/comments.md][Comments]]
- [[./reference/language/axioms.md][Axioms]]
- [[./reference/examples.md][Example programs]]
- [[./reference/benchmarks.md][Benchmarks]]
- [[./reference/tooling/README.md][Tooling]]
- [[./reference/tooling/CLI.md][Command line interface]]
- [[./reference/tooling/doctor.md][Doctor]]
- [[./reference/tooling/emacs.md][Emacs mode]]
- [[./reference/tooling/testing.md][Haskell test suite]]
- [[./reference/judoc.md][Judoc reference]]
* About
- [[./about/community.md][Community]]

7
docs/org/about/community.org
View File

@ -1,7 +0,0 @@
* Juvix community
Join us on our [[https://discord.gg/waYhQ2Qr][Discord server]]
This project is part of a bigger effort called [[https://anoma.net/][Anoma]].
Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination.
Join the [[https://anoma.net/community][Anoma project]].

1
docs/org/about/team.org
View File

@ -1 +0,0 @@
* The Juvix Dev Team

13
docs/org/examples/README.org
View File

@ -1,13 +0,0 @@
** [[https://github.com/anoma/juvix/tree/main/examples/milestone][Examples of programs written in Juvix]]
The following links are clickable versions of their corresponding Juvix programs. The HTML output can be generated by running =juvix html --recursive FileName.juvix=.
- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains
common functions that can be used in Juvix programs.

26
docs/org/explanations/totality/termination.org
View File

@ -1,26 +0,0 @@
* 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 fulfill,
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.
#+begin_example
terminating fun : A → B;
#+end_example
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=.
#+begin_example
juvix typecheck --no-termination MyProgram.juvix
#+end_example
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 slightly modification of the algorithm for checking termination in the Foetus's language.

41
docs/org/howto/compilation.org
View File

@ -1,41 +0,0 @@
* 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=:
#+begin_example
-- 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;
#+end_example
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 [[https://anoma.github.io/geb/][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: [[../reference/language/modules.md][Modules Reference]].

119
docs/org/howto/installing.org
View File

@ -1,119 +0,0 @@
* Dependencies
You need [[https://releases.llvm.org/download.html][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:
- [[https://wasmer.io][wasmer]]
- [[https://github.com/WebAssembly/wasi-sdk/releases][wasi-sdk]]
- [[https://lld.llvm.org][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 [[./installing.md#installing-dependencies][below]] for instructions on how to install the dependencies.
* Installing Juvix
*** MacOS
The easiest way to install Juvix on MacOS is by using [[https://brew.sh][Homebrew]].
To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:
#+begin_src shell
brew tap anoma/juvix
#+end_src
To install Juvix, run:
#+begin_src shell
brew install juvix
#+end_src
Helpful information can also be obtained by running:
#+begin_src shell
brew info juvix
#+end_src
*** Linux x86_64
A Juvix compiler binary executable for Linux x86_64 is available on the [[https://github.com/anoma/juvix/releases/latest][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:
#+begin_src shell
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
#+end_src
*** Building Juvix from source
To install Juvix from source you must clone the [[https://github.com/anoma/juvix.git][Github repository]]. Then Juvix can be installed with the following commands. We assume you have [[https://haskellstack.org][Stack]] and [[https://www.gnu.org/software/make/][GNU Make]] installed.
#+begin_src shell
git clone --recursive https://github.com/anoma/juvix.git
cd juvix
make install
#+end_src
The C compiler and linker paths can be specified as options to the =make install= command, e.g.
#+begin_src shell
make install CC=path/to/clang LIBTOOL=path/to/llvm-ar
#+end_src
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.
#+begin_src shell
brew install --build-from-source --HEAD juvix --verbose
#+end_src
*** 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 [[https://github.com/sol/hpack][hpack]] before running =cabal build=.
You also need to compile the runtime first:
#+begin_src shell
make runtime
cabal build
#+end_src
* Installing dependencies
To install =wasi-sdk= you need to download =libclang_rt= and =wasi-sysroot=
precompiled archives from the [[https://github.com/WebAssembly/wasi-sdk/releases/][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:
#+begin_src shell
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
#+end_src
2. Extract the =wasi-sysroot-*.tar.gz= archive on your local system and set
=WASI_SYSROOT_PATH= to its path.
For example:
#+begin_src shell
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
#+end_src

68
docs/org/notes/builtins.org
View File

@ -1,68 +0,0 @@
#+title: Builtins
#+author: Jan Mas Rovira
* Overview
The goal is to support builtin types and functions that get compiled to
efficient primitives. We plan on supporting primitives for the following types
of definitions:
1. Builtin inductive definitions. For example:
#+begin_example
builtin nat
type Nat :=
zero : Nat |
suc : Nat → Nat;
#+end_example
We will call this the canonical definition of natural numbers.
2. Builtin function definitions. For example:
#+begin_src text
inifl 6 +;
builtin nat-plus
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
#+end_src
3. Builtin axiom definitions. For example:
#+begin_src text
builtin nat-print
axiom printNat : Nat → Action;
#+end_src
** Collecting builtin information
The idea is that builtin definitions are treated normally throughout the
pipeline except in the backend part. There is one exception to that. We need to
collect information about the builtins that have been included in the code and
what are the terms that refer to them. For instance, imagine that we find this
definitions in a juvix module:
#+begin_src text
builtin nat
type MyNat :=
z : MyNat |
s : MyNat → MyNat;
#+end_src
We need to take care of the following:
1. Check that the definition =MyInt= is up to renaming equal to the canonical
definition that we provide in the compiler.
2. Rember a map from concrete to canonical names: {MyNat ↦ Nat; z ↦ zero; s ↦ suc};
3. Rembember that we have a definition for builtin natural numbers. This is
necessary if later we attempt to define a builtin function or axiom that
depends on natural numbers.
In the compiler we need to know the following:
1. For inductives:
1. What is the primitive type that we will target in the backend: E.g. {Nat ↦ int}.
2. For constructors:
1. What is the primitive constructor function: E.g. {zero ↦ 0; suc ↦ plus_one};
2. How to test if a term matches a pattern with that constructor.
E.g. {zero ↦ is_zero; suc ↦ is_not_zero};
3. How to deconstruct/project each of the constructor arguments. E.g. {zero ↦
∅; suc ↦ minus_one}}. Note that if a constructor takes multiple arguments
we will need to have a projection function for each argument.
2. For functions and axioms:
1. What is the primitive function that we will target in the backend: E.g. {+
↦ add}.

12
docs/org/notes/lsp.org
View File

@ -1,12 +0,0 @@
* LSP support
We provide a sample =hie.yaml= configuration file for both =cabal= and =stack=.
If you prefer =stack=, run:
#+begin_src shell
cp stack.hie.yaml hie.yaml
#+end_src
If you prefer =cabal=, run:
#+begin_src shell
cp cabal.hie.yaml hie.yaml
#+end_src

183
docs/org/notes/monomorphization.org
View File

@ -1,183 +0,0 @@
#+author: Jan Mas Rovira
* Monomorphization
(Removed in v0.2.5)
Monomorphization refers to the process of converting polymorphic code to
monomorphic code (no type variables) through static analysis.
Example:
#+begin_src juvix
id : (A : Type) → A → A;
id _ a := a;
b : Bool;
b := id Bool true;
n : Nat;
n := id Nat zero;
#+end_src
Is translated into:
#+begin_src juvix
id_Bool : Bool → Bool;
id_Bool a := a;
id_Nat : Nat → Nat;
id_Nat a := a;
#+end_src
* More examples
** Mutual recursion
#+begin_src juvix
type List (A : Type) :=
nil : List A |
cons : A → List A → List A;
even : (A : Type) → List A → Bool;
even A nil := true ;
even A (cons _ xs) := not (odd A xs) ;
odd : (A : Type) → List A → Bool;
odd A nil := false ;
odd A (cons _ xs) := not (even A xs) ;
-- main := even Bool .. odd Nat;
#+end_src
* Collection algorithm
This section describes the algorithm to collect the list of all concrete
functions and inductive definitions that need to be generated.
** Assumptions:
1. Type abstractions only appear at the leftmost part of a type signature.
2. All functions and constructors are fully type-applied: i.e. currying for
types is not supported.
3. There is at least one function with a concrete type signature.
4. All axioms are monomorphic.
5. No module parameters.
** Definitions
1. *Application*. An application is an expression of the form =t₁ t₂ … tₙ= with n > 0.
2. *Sub application*. If =t₁ t₂ … tₙ= is an application then for every =0<i<n=
=t₁ t₂ … tᵢ= is a sub application.
Fix a juvix program =P=. Let =𝒲= be the set of all applications that appear in =P=.
1. *Maximal application*. A maximal application is an application =A∈𝒲= such that
for every =A'∈𝒲= we have that =A= is *not* a sub application of =A'=.
2. *Type application*. If
1. =t a₁ a₂ … aₙ= is a maximal application; and
1. =t= is either a function or an inductive type; and
2. =a₁, …, aₘ= are types; and
3. =aₘ₊₁= is not a type or =m = n=.
Then =t a₁, …, aₘ= is a type application.
3. *Concrete type*. A type is concrete if it involves no type variables.
4. *Concrete type application*. A type application =t a₁ a₂ … aₙ= if =a₁, a₂, …,
aₙ= are concrete types.
** Option 1
Let =S₀= be the set of functions with a concrete type signature. Gather all
type applications (both in the type and in the body) in each of the functions
in =S₀=. Clearly the collected type applications are all concrete. We now have
a stack =c₁, c₂, …, cₙ= of concrete type applications.
1. If the stack is empty, we are done.
2. Otherwise pop =c₁= from the stack. It will be of the form =t a₁ … aₘ=,
where =t= is either an inductive or a function and =a₁, …, aₘ= are
concrete types.
3. If the instantiation =t a₁ … aₘ= has already been registered go to step 1.
Otherwise continue to the next step.
4. Register the instantiation =t a₁ … aₘ=.
5. If =t= is a function, then it has type variables =v₁, …, vₘ=.
Consider the substitution =σ = {v₁ ↦ a₁, …, vₘ ↦ aₘ}=.
Consider the list of type applications in the body of =t=: =d₁, …, dᵣ=.
Add =σ(d₁), …, σ(dᵣ)= to the stack and continue to step 1.
It is easy to see that for any =i=, =σ(dᵢ)= is a concrete type application.
6. If =t= is an inductive type, let =d₁, …, dᵣ= be the type applications that
appear in the type of its constructors, then proceed as before.
*** Correctness
It should be clear that the algorithm terminates and registers all
instantiations of constructors and functions.
* Generation algorithm
The input of this algorithm is the list of concrete type applications, name it
=ℒ=, produced by the collection algorithm. Example:
#+begin_example
List String
Pair Int Bool
Maybe String
Maybe Int
if (Maybe String)
if (Maybe Int)
if (Pair Int Bool)
#+end_example
** Name generation
Let =f â= be an arbitrary element of =ℒ=, where =â= is a list of concrete types.
- If =f= is a function, assign a fresh name to =f â=, call it =⋆(f â)=.
- If =f= is an inductive type, assign a fresh name to =f â=, call it
=⋆(f â)=. Then, for each constructor =cᵢ= of =f=, where =i= is the index of
the constructor, assign a fresh name to it and call it =⋆ᵢ(f â)=.
** Function generation
Consider an arbitrary function =f= in the original program. Then consider the
list of concrete type applications involving =f=: =f â₁, …, f âₙ=.
- If =n = 0=, then either:
1. =f= has a concrete type signature, in that case we proceed as expected.
2. =f= is never called from the functions with a concrete type. In this case we
can safely ignore it.
- If =n > 1=. For each =âᵢ= we proceed as follows in the next sections. Fix =m= to be
the lenght of =âᵢ= with =m > 0=.
*** Function name
The name of the monomorphized function is =⋆(f âᵢ)=.
*** Type signature
Let =𝒮= be the type signature of =f=. Then =𝒮= has to be of the form =(A₁ :
Type) → … → (Aₘ : Type) → Π=, where =Π= is a type with no type abstractions.
Now consider the substitution =σ = {A₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]}=. Since =âᵢ= is
a list of concrete types, it is clear that =σ(Π)= is a concrete type.
Then proceed as described in [[Types]].
*** Function clause
Let =𝒞= be a function clause of =f=. Let =p₁ … pₖ= with =k ≥ m= be the list of
patterns in =𝒞=. Clearly the first =m= patterns must be either variables or
wildcards. Wlog assume that the first =m= patterns are all variables, namely
=v₁, …, vₘ=. Let =σ = {v₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]}= be a substitution. Let =e=
be the body of =𝒞=, then clearly =σ(e)= has no type variables in it. Now, since
each name id must be bound at most once, we need to generate new ones for the
local variables bound in the patterns =pₘ₊₁, …, pₖ=. Let =w₁, …, wₛ=
be the variables bound in =pₘ₊₁, …, pₖ=. Let =w'₁, …, w'ₛ= be fresh variables.
Then let =δ = {w₁ ↦ w'₁, …, wₛ ↦ w'ₛ}=.
Now let =𝒞'= have patterns =δ(pₘ₊₁), …, δ(pₖ)= and let =e' := (σ ∪ δ)(e)=. It
should be clear that =e'= has no type variables in it and that all local
variable references in =e'= are among =w'₁, …, w'ₛ=. Note that =e'= is not yet
monomorphized. Proceed to the next step to achieve that.
*** Expressions
The input is an expression =e= that has no type variables in it. The goal is to
replace the concrete type applications by the corresponding monomorphized
expression.
The only interesting case is when we find an application. Consider the unfolded
view of the application: =f a₁ … aₘ=. Then, if =f= is either a constructor, or
a function, let =A₁, …, Aₖ= with =k ≤ m= be the list of type parameters of =f=.
- If =f= is a function and =f a₁ … aₖ ∉ ℒ= then recurse normally, otherwise,
let =â := a₁ … aₖ= and replace the original expression =f a₁ … aₘ=, by =⋆(f â)
aₖ₊₁' … aₘ'= where =aₖ₊₁' … aₘ'= are the monomorphization of =aₖ₊₁ … aₘ=
respectively.
- If =f= is a constructor, let =d= be its inductive type. Then check =d a₁ … aₖ
∈ ℒ=. Proceed analogously as before.
*** Types
The input is a type =t= that has no type variables in it. The goal is to
replace the concrete type applications by the corresponding monomorphized
type. Proceed analogously to the previous section.

326
docs/org/notes/runtime-benchmark-results.org
View File

@ -1,326 +0,0 @@
Benchmarks of the new Juvix runtime
====================================
Benchmarked version: commit 148ececb4d4259eacbb980f5992073a3ac611d82 from 31.10.2022
Summary
-------
We benchmark several programs manually compiled into the primitives of
the new Juvix runtime. The code corresponds closely to the code that
will be generated by the new compilation process, with basic low-level
optimisations (unboxing, untagging, etc.) but without any high-level
optimisations on JuvixCore (inlining, specialisation, constant
folding, fusion, etc.). This corresponds to the compilation process
planned for the 0.4 milestone.
We compare the running time and memory usage with analogous programs
written in Haskell, OCaml, JuvixCore (using the evaluator), current
Juvix (with the "direct" transpilation to C) and C.
The results suggest that for most first-order programs the new
compilation process will produce code with running time comparable to
the code produced by the native OCaml compiler. For higher-order
programs heavy on closure manipulation, the results are acceptable but
noticeably worse, especially with third-order functions
(i.e. functions which take functions taking functions). This could,
however, be alleviated by implementing the specialisation optimisation
(see the "specialised" column in the `ackermann` and `mapfun`
benchmarks). Besides, functional programs of order higher than two are
rare.
The comparisons with OCaml and Haskell were not entirely fair because
the new Juvix runtime does not perform garbage collection. The
overhead of garbage collection is particularly visible on the
`mergesort` benchmark which creates many intermediate data structures
that are quickly discarded. With proper memory management, the running
time results on first-order programs for the new Juvix runtime are
expected to become slightly worse than for the native OCaml compiler.
For simple programs operating on integers which don't require any heap
memory allocation (`fibonacci` and `combinations` benchmarks), the
direct transpilation to C in the current Juvix seems to perform best
(behind only C). The reason is that for very simple programs `clang`
can better optimise the output of such a direct transpiler. The main
problem with the transpilation to C approach is that it cannot scale
to reliably work for more complex programs, as evidenced by the
segfaults, longer running time and higher memory use on other
benchmarks.
In addition to the `fibonacci` and `combinations` benchmarks, the
advantage of direct transpilation for very simple programs is also
visible on the `fold` benchmark where a simple loop over a list
dominates the running time. However, this is partly because the
compilation of closures in current Juvix is incorrect allowing it
to be more efficient.
Benchmark programs
------------------
* fibonacci: compute the Nth Fibonacci number modulo 2^28 (N = 100’000’000)
The Nth Fibonacci number is computed in O(N). Needs only constant
stack space and no heap memory. This benchmark tests the
efficiency of tail recursion and arithmetic operations.
* combinations: count combinations of numbers 1 to N having sum N (N = 100)
This benchmark tests the efficiency of general recursion. No heap
memory needs to be allocated. Uses stack space proportional to
N. The running time is exponential in N.
* prime: compute the Nth prime (N = 16384)
The Nth prime number is computed via the Eratosthenes sieve. A
list of N primes is created. No intermediate lists are discarded
(garbage collection not needed). This benchmark tests the
efficiency of tail recursion, arithmetic operations, list cell
allocation and access.
* mergesort: merge sort a list of N integers (N = 2’000’000)
At each level of merge sort intermediate lists are created and
discarded. The running time for this benchmark largely depends on
the efficiency of memory management. Here one may observe the
overhead of garbage collection or the memory blow-up if no garbage
collection is used.
* maybe: optionally sum N integers from a binary tree K times (N = 2^20, K = 100)
If a fixed number k is encountered in the tree then the result is
`Nothing`, otherwise it is `Just sum`. The computation is repeated
for values of k from 0 to K. This tests the efficiency of handling
optional values and data structure access.
* fold: fold a list of N integers K times (N = 100’000, K = 1000)
The sum of N natural numbers is computed via fold_left
(tail-recursive). The computation is repeated K times. The list is
created only once, so that allocation time does not dominate. This
benchmark tests the efficiency of closure call and list cell
access.
* cps: compute the Nth Fibonacci number modulo 2^28 with CPS (N = 100’000’000)
The function computing the Nth Fibonacci number is written in
continuation-passing style, tail-recursively calling a
continuation supplied as an argument. This benchmark tests the
efficiency of closure call and allocation.
* mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
This benchmark tests the efficiency of standard higher-order
functions on lists, closure call and memory management. The
program allocates O(K) intermediate lists of length N which are
quickly discarded.
* ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
The higher-order Ackermann function definition iterates an
iteration of function compositions. Hence, it uses a third-order
invocation of an iteration function. This benchmark tests the
efficiency of creating and calling second-order closures, and of
partial application.
* mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
The benchmark stores K second-order closures in a list, maps them
successively to a list of K closures, and then successively maps
the K closures from the result to a list of N integers. This
benchmark tests the efficiency of manipulating closures and
storing them in data structures.
The benchmark programs can be found in `tests/benchmark` in the Juvix
source directory.
Methodology
-----------
For each program the total running time (elapsed real time) and memory
use (maximum resident set size) were measured on an M1 iMac with no
significant background activity. Averages of several runs were taken.
The variance was negligible, unless indicated otherwise by providing a
range.
Results
-------
* fibonacci: compute the Nth Fibonacci number modulo 2^28 (N = 100’000’000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.26 |0.35 |0.35 |0.23 |13.15 |10.03 |0.39 |0.35 |0.94 |0.16 |0.22 |
|Memory use (MB, max RSS)|1.5 |3.8 |1.3 |8.8 |21.3 |8067.7 |9.7 |1.7 |1.8 |1.3 |4.0 |
* combinations: count all combinations of numbers 1 to N having sum N (N = 1000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |6.67 |11.25 |3.22 |5.1 |441.71 |5.48 |5.48 |6.53 |41.08 |2.69 |4.80 |
|Memory use (MB, max RSS)|1.5 |3.9 |1.3 |8.9 |22.3 |9.6 |9.6 |1.7 |1.9 |1.3 |4.0 |
* prime: compute the Nth prime (N = 16384)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |1.52 |1.91 |segfault |3.09 |167.04 |3.85 |3.85 |1.68 |14.82 |0.12 |0.13 |
|Memory use (MB, max RSS)|1.7 |4.0 |segfault |9.3 |24.4 |9.8 |9.6 |2.2 |2.2 |1.4 |4.0 |
* mergesort: merge sort a list of N integers (N = 2’000’000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.40 |0.31 |3.55 |1.32 |22.45 |2.86 |2.90 |1.95 |3.52 |0.15 |0.15 |
|Memory use (MB, max RSS)|1973.7 |720.4 |5046.7 |2729.8 |1728.9 |253.6 |253.6 |172.6 |343.1 |24.4 |26.8 |
* maybe: optionally sum N non-zero integers from a binary tree K times (N = 2^20, K = 100)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.45 |0.64 |3.29 |1.57 |22.75 |5.58 |0.59 |0.30 |3.57 |0.27 |0.50 |
|Memory use (MB, max RSS)|1.6 |3.8 |2646.1 |1320.9 |22.4 |5560.7 |9.7 |3.9 |4.0 |1.3 |4.1 |
* fold: fold a list of N integers K times (N = 100’000, K = 1000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.45 |0.54 |0.35 |0.23 |15.27 |0.58 |0.58 |0.36 |1.80 |NA |NA |
|Memory use (MB, max RSS)|3.1 |4.6 |4.4 |10.6 |43.4 |12.7 |12.7 |5.9 |5.9 |NA |NA |
* cps: compute the Nth Fibonacci number modulo 2^28 with CPS (N = 100’000’000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.43 |0.52 |1.56 |stack overflow |20.22 |10.04 |0.39 |0.35 |1.60 |0.16 |0.25 |
|Memory use (MB, max RSS)|1.5 |3.9 |1539.3 |stack overflow |21.3 |8067.7 |9.7 |1.7 |1.8 |1.3 |4.0 |
* mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |1.01 |1.59 |2.74 |1.81 |38.24 |1.29 |2.42 |1.43 |4.22 |NA |NA |
|Memory use (MB, max RSS)|2154.5 |893.0 |3059.1 |1542.0 |26.4 |10.6 |10.7 |7.5 |10-20 |NA |NA |
* ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|New Juvix runtime (specialised, native)|New Juvix runtime (specialised, wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|---------------------------------------|-----------------------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |0.92 |1.21 |0.30 |0.65 |segfault |runtime error |11.71 |0.87 |0.47 |0.54 |1.35 |0.00 |0.14 |
|Memory use (MB, max RSS)|2.6 |4.1 |2.3 |3.9 |segfault |runtime error |23.3 |13.6 |9.6 |2.0 |3.6 |1.3 |4.0 |
* mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
| |New Juvix runtime (native)|New Juvix runtime (wasm32, wasmer)|New Juvix runtime (specialised, native)|New Juvix runtime (specialised, wasm32, wasmer)|Current Juvix (native)|Current Juvix (wasm32, wasmer)|JuvixCore evaluator|Haskell (native, ghc -O2)|Haskell (native, ghc -XStrict -O2)|OCaml (native, ocamlopt -O2)|OCaml (bytecode)|C (native, clang -O3)|C (wasm32, clang -Os, wasmer)|
|------------------------|--------------------------|----------------------------------|---------------------------------------|-----------------------------------------------|----------------------|------------------------------|-------------------|-------------------------|----------------------------------|----------------------------|----------------|---------------------|-----------------------------|
|Time (seconds, real) |1.27 |1.04 |0.39 |0.46 |segfault |runtime error |4.18 |1.85 |0.95 |0.19 |0.68 |NA |NA |
|Memory use (MB, max RSS)|3209.8 |1229.7 |21.8 |13.2 |segfault |runtime error |33.0 |13.6 |11.6 |5.3 |7.9 |NA |NA |
Comments
--------
* "New Juvix runtime" denotes C programs written using the primitives
of the new Juvix runtime. These programs were "manually" compiled
from the corresponding Juvix/JuvixCore programs, according to the
new Juvix compilation concept. They correspond closely to the code
that will be generated by the basic version of the new compilation
process, without any high-level optimisations (inlining,
specialisation, fusion, constant folding) but with basic low-level
memory representation optimisations (unboxing, untagging, etc). This
version of the new compilation process should be finished with the
0.4 milestone.
* The "specialised" column for "New Juvix runtime" denotes a version
of the corresponding "New Juvix runtime" benchmark program for which
specialisation of higher-order functions was manually performed (to
simulate the effects of the high-level specialisation optimisation).
* "Current Juvix" denotes Juvix programs compiled with the current
compilation process via a "direct" translation to C. For a fair
comparison, all number operations were implemented using native
binary C integers (exposed via `foreign` and `compile` blocks)
without overflow check, instead of using the unary Nat from the
standard library. For Haskell, we use the fixed-precision Int
instead of the arbitrary-precision Integer.
* For the simplest benchmark programs without heap memory allocation
(e.g. `fibonacci`, `combinations`), the performance of "Current
Juvix" is comparable to or better than that of "New Juvix
runtime". This is because `clang` managed to eliminate (tail)
recursion and optimise the code to essentially the same or better
thing. The main problem with the current "direct" transpilation to C
approach is that it cannot scale to reliably work for more complex
programs. By "more complex" I mean larger program size, more
functions, more complex patterns of recursion and/or the use of more
functional programming features (including functional data
structures). I don't mean higher computational complexity or more
resource use.
* The segfaults and runtime errors for "Current Juvix" are
consequences of incorrectly generated code (current compilation of
partial application is not entirely correct) or stack overflows
(when `clang` didn't figure out how to eliminate tail recursion).
* The comparison with "Current Juvix" is not entirely fair for
benchmarks that test the manipulation and calling of closures
(e.g. `fold`). Current Juvix achieves good performance (when it
doesn't segfault) at the expense of correctness: partial application
is not compiled correctly and fixing this would require a
fundamental change in closure representation.
* The comparison with Haskell and OCaml compilers is not entirely
fair, because the new Juvix runtime does not perform garbage
collection. With the GC overhead, I would expect the Juvix runtime
results for native compilation of first-order programs to become a
bit worse than the native OCaml versions. The GC overhead is
particularly noticeable for the `mergesort` benchmark which creates
many large intermediate lists. The memory usage of the Juvix runtime
is much higher on this benchmark than the memory usage of OCaml or
Haskell versions. The relatively small time difference between the
OCaml native and bytecode versions of `mergesort` also indicates
that GC accounts for a significant part of the running time.
* Another small overhead will be introduced by bounds checking for
integer operations. Currently, the new Juvix runtime operates on
unboxed 31-bit (or 63-bit) integers without checking for integer
overflow.
* If we decide to default to transparent arbitrary-precision integers,
then another small overhead will be introduced by the need to check
the integer representation with each arithmetic operation.
* Admittedly, the programs were deliberately written in a way to make
high-level optimisations unnecessary, except specialisation for
higher-order functions (mostly in `ackermann` and `mapfun`). This
also explains the good performance of the OCaml native compiler
which doesn't do much high-level optimisation.
* In the "Current Juvix" and OCaml version of `mergesort`, to avoid
stack overflow the `merge` function was written tail-recursively
with accumulator reversal at the end. This is not necessary for the
new Juvix runtime, because the stack is dynamically extended when
needed.
* As evidenced by the `combinations` benchmark, for non-tail-recursive
direct calls our code performs worse than the code which uses the C
/ WebAssembly stack and function call mechanisms. However, in
general it is impossible to directly use the C / WebAssembly stack
and call mechanisms for a purely functional language. Since we
dynamically allocate the stack segments when needed, stack overflow
is impossible. This is convenient in an eager functional
language. Otherwise, one needs to rewrite all functions operating on
large data to use tail recursion. We pay for this convenience with a
small overhead, which is the main reason for poorer performance on
`combinations` where stack manipulation cost dominates.
* Haskell's laziness seems to introduce more overhead than I
expected. This would explain the comparatively better performance of
the native OCaml compiler. The problem is particularly stark when
Haskell's strictness analysis fails for some reason, as in the
`fibonacci` benchmark. The second "Haskell" column with the
"-XStrict" flag for GHC indicates the version of the benchmark
compiled with strictness as the default.
* The C versions of the programs were written to take advantage of C's
imperative features, e.g., using arrays instead of lists, loops
instead of recursion. No C versions are provided for some benchmarks
designed to test specifically functional language features.
* With the new Juvix runtime, the 32-bit WebAssembly version of
`mergesort` is faster than the 64-bit native version because it
needs roughly half as much memory (the word size is 4 bytes instead
of 8). The difference is even starker between the WebAssembly and
native versions of `mergesort` for "Current Juvix".
* There seems to be a memory leak in the JuvixCore evaluator. This is
what happens too often when one uses a lazy language.
* Haskell also leaks memory in the Fibonacci benchmark, despite it
being a simple tail-recursive program. It seems strictness analysis
didn't work.

71
docs/org/notes/strictly-positive-data-types.org
View File

@ -1,71 +0,0 @@
* Strictly positive data types
We follow a syntactic description of strictly positive inductive data types.
An inductive type is said to be _strictly positive_ if it does not occur or
occurs strictly positively in the types of the arguments of its constructors. A
name qualified as strictly positive for an inductive type if it never occurs at
a negative position in the types of the arguments of its constructors. We refer
to a negative position as those occurrences on the left of an arrow in a type
constructor argument.
In the example below, the type =X= occurs strictly positive in =c0= and
negatively at the constructor =c1=. Therefore, =X= is not strictly positive.
#+begin_src minijuvix
axiom B : Type;
type X :=
c0 : (B -> X) -> X
| c1 : (X -> X) -> X;
#+end_src
We could also refer to positive parameters as such parameters occurring in no
negative positions. For example, the type =B= in the =c0= constructor above is
on the left of the arrow =B->X=. Then, =B= is at a negative position. Negative
parameters need to be considered when checking strictly positive data types as
they may allow to define non-strictly positive data types.
In the example below, the type =T0= is strictly positive. However, the type =T1= is not.
Only after unfolding the type application =T0 (T1 A)= in the data constructor =c1=, we can
find out that =T1= occurs at a negative position because of =T0=. More precisely,
the type parameter =A= of =T0= is negative.
#+begin_src minijuvix
type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
type T1 := c1 : T0 T1 -> T1;
#+end_src
** Bypass the strict positivity condition
To bypass the positivity check, a data type declaration can be annotated
with the keyword =positive=. Another way is to use the CLI global flag =--no-positivity=
when typechecking a =Juvix= File.
#+begin_example
$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
module E5;
positive
type T0 (A : Type) :=
c0 : (T0 A -> A) -> T0 A;
end;
#+end_example
** Examples of non-strictly data types
- =Bad= is not strictly positive beceause of the negative parameter =A= of =Tree=.
#+begin_src minijuvix
type Tree (A : Type) :=
leaf : Tree A
| node : (A -> Tree A) -> Tree A;
type Bad :=
bad : Tree Bad -> Bad;
#+end_src
- =A= is a negative parameter.
#+begin_src minijuvix
type B (A : Type) :=
b : (A -> B (B A -> A)) -> B A;
#+end_src

8
docs/org/reference/examples.org
View File

@ -1,8 +0,0 @@
The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running =juvix html --recursive FileName.juvix=.
- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]

7
docs/org/reference/language/README.org
View File

@ -1,7 +0,0 @@
- [[./functions.md][Functions]]
- [[./datatypes.md][Data types]]
- [[./modules.md][Modules]]
- [[./let.md][Local definitions]]
- [[./control.md][Control structures]]
- [[./comments.md][Comments]]
- [[./axioms.md][Axioms]]

15
docs/org/reference/language/axioms.org
View File

@ -1,15 +0,0 @@
* 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.
#+begin_src
-- Example.juvix
module Example;
axiom A : Type;
axiom x : A;
end;
#+end_src
Terms introduced by the =axiom= keyword lack any computational content. Programs containing axioms not marked as builtins cannot be compiled to most targets.

30
docs/org/reference/language/builtins.org
View File

@ -1,30 +0,0 @@
* Built-ins
Juvix has support for the built-in natural type and a few functions that are compiled to efficient primitives.
1. Built-in inductive definitions.
#+begin_example
builtin nat
type Nat :=
zero : Nat |
suc : Nat → Nat;
#+end_example
2. Builtin function definitions.
#+begin_example
infixl 6 +;
builtin nat-plus
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
#+end_example
3. Builtin axiom definitions.
#+begin_example
builtin nat-print
axiom printNat : Nat → Action;
#+end_example

17
docs/org/reference/language/comments.org
View File

@ -1,17 +0,0 @@
* Comments
Comments follow the same syntax as in =Haskell= and =Agda=. Be aware, Juvix has no support for nested comments.
- Inline Comment
#+begin_src
-- This is a comment!
#+end_src
- Region comment
#+begin_src
{-
This is a comment!
-}
#+end_src

27
docs/org/reference/language/control.org
View File

@ -1,27 +0,0 @@
* Control structures
** Case
A case expression has the following syntax:
#+begin_example
case value
| pat1 := branch1
..
| patN := branchN
#+end_example
For example, one can evaluate the following expression in the REPL:
#+begin_example
Stdlib.Prelude> case 2 | zero := 0 | suc x := x | _ := 19
1
#+end_example
** 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.

50
docs/org/reference/language/datatypes.org
View File

@ -1,50 +0,0 @@
* Data types
A data type declaration consists of:
- the =type= keyword,
- a unique name for the type,
- the =:== symbol,
- 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=.
#+begin_example
type Unit := unit : Unit;
#+end_example
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.
#+begin_example
type Nat :=
zero : Nat
| suc : Nat -> Nat;
#+end_example
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:
#+begin_src text
infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
#+end_src
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.
#+begin_example
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;
#+end_example
For more examples of inductive types and how to use them, see
[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]].

88
docs/org/reference/language/functions.org
View File

@ -1,88 +0,0 @@
* 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.
#+begin_example
open import Stdlib.Prelude;
multiplyByTwo : Nat -> Nat;
multiplyByTwo n := 2 * n;
#+end_example
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.
#+begin_example
open import Stdlib.Prelude;
neg : Bool -> Bool;
neg true := false;
neg false := true;
#+end_example
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=.
#+begin_example
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;
#+end_example
** Anonymous functions
Anonymous functions, or /lambdas/, are introduced with the syntax:
#+begin_example
\{| pat1 .. patN_1 := clause1
| ..
| pat1 .. patN_M := clauseM}
#+end_example
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:
#+begin_example
open import Stdlib.Prelude;
odd : Nat -> Bool;
even : Nat -> Bool;
odd := \{
| zero := false
| (suc n) := even n
};
even := \{
| zero := true
| (suc n) := odd n
};
#+end_example
** Short definitions
A function definition can be written in one line, with the body immediately following the signature:
#+begin_example
multiplyByTwo : Nat -> Nat := \{n := 2 * n};
#+end_example

16
docs/org/reference/language/let.org
View File

@ -1,16 +0,0 @@
* Local definitions
Local definitions are introduced with the =let= construct.
#+begin_example
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;
#+end_example
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.

173
docs/org/reference/language/modules.org
View File

@ -1,173 +0,0 @@
* 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.
#+begin_example
-- ModuleName.juvix
module ModuleName;
end;
#+end_example
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=.
# - Inside a module, other (sub) modules can be declared.
# #+begin_example
# -- Example.juvix
# module Example;
# module A;
# end;
# end;
# #+end_example
** 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.
#+begin_example
-- A.juvix
module A;
axiom Nat : Type;
axiom zero : Nat;
end;
-- B.juvix
module B;
import A;
x : A.Nat;
x := A.zero;
#+end_example
Additionally, one can _open_ an imported module making available all its
names by their unqualified name.
#+begin_example
-- A.juvix
module A;
axiom Nat : Type;
axiom zero : Nat;
end;
-- B.juvix
module B;
import A;
open A;
x : Nat;
x := zero;
#+end_example
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.
#+begin_example
-- 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;
#+end_example
One alternative here is hiding the name =a= as follows.
#+begin_example
-- B.juvix
module B;
import A;
open A hiding {a};
axiom a : A;
x := a;
end;
#+end_example
Now, we can use the =open import= syntax to simplify the =import-open= statements.
Instead of having:
#+begin_example
import Prelude;
open Prelude;
#+end_example
We simplify it by the expression:
#+begin_example
open import Prelude;
#+end_example
The =hiding= keyword can be used within an =open-import= statement.
#+begin_example
-- B.juvix
module A;
open import A hiding {a};
axiom a : A;
x := a;
end;
#+end_example
** 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=.
#+begin_example
-- 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;
#+end_example
Fix:
#+begin_example
-- B.juvix
module B;
open import A public;
end;
#+end_example

2
docs/org/reference/stdlib.org
View File

@ -1,2 +0,0 @@
The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains common functions that can be used in Juvix programs.

106
docs/org/reference/tooling/CLI.org
View File

@ -1,106 +0,0 @@
* CLI
** Usage
#+begin_src shell
juvix [Global options] ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CMD)
#+end_src
** 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
#+begin_src shell
juvix dev COMMAND
#+end_src
- =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=).
#+begin_src shell
eval "$(juvix --bash-completion-script juvix)"
#+end_src
*** Fish
Run the following command in your shell:
#+begin_src shell
juvix --fish-completion-script juvix
> ~/.config/fish/completions/juvix.fish
#+end_src
*** ZSH
Run the following command in your shell:
#+begin_src shell
juvix --zsh-completion-script juvix > $DIR_IN_FPATH/_juvix
#+end_src
where =$DIR_IN_FPATH= is a directory that is present on the [[https://zsh.sourceforge.io/Doc/Release/Functions.html][ZSH FPATH variable]] (which you can inspect by running =echo $FPATH= in the shell).

4
docs/org/reference/tooling/README.org
View File

@ -1,4 +0,0 @@
- [[./CLI.md][Command line Interface]]
- [[./emacs.md][Emacs Mode]]
- [[./testing.md][Test Suite]]
- [[./doctor.md][Doctor]]

93
docs/org/reference/tooling/doctor.org
View File

@ -1,93 +0,0 @@
* 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 [[https://clang.llvm.org][Clang compiler]] version 13 or later to generate binaries. You need to have Clang available on your system =$PATH=.
Recommended installation method:
*** MacOS
Use [[https://brew.sh][Homebrew]]:
#+begin_src shell
brew install llvm
#+end_src
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
#+begin_src shell
sudo apt install clang lldb lld
#+end_src
*** Arch Linux
#+begin_src shell
sudo pacman -S llvm lld
#+end_src
** 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 [[https://brew.sh][Homebrew]] llvm distribution:
#+begin_src shell
brew install llvm
#+end_src
*** Debian / Ubuntu Linux
#+begin_src shell
sudo apt install lldb lld
#+end_src
*** Arch Linux
#+begin_src shell
sudo pacman -S lld
#+end_src
** Newer Clang version required
Juvix requires Clang version 13 or above. See the documentation on [[./doctor.md#could-not-find-the-clang-command][installing Clang]].
** Clang does not support the wasm32 target
Juvix requires Clang version 13 or above. See the documentation on [[./doctor.md#could-not-find-the-clang-command][installing Clang]].
** Clang does not support the wasm32-wasi target
Juvix uses [[https://wasi.dev][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 [[https://github.com/WebAssembly/wasi-sdk/releases][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 [[https://github.com/WebAssembly/wasi-sdk/releases][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 [[https://github.com/WebAssembly/wasi-sdk/releases][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 [[./doctor.md#download-the-wasi-sysroot-and-set-wasi_sysroot_path][installing the WASI sysroot]].
** Could not find the wasmer command
The Juvix test suite uses [[https://wasmer.io][Wasmer]] as a Wasm runtime to execute compiled Wasm binaries. See [[https://docs.wasmer.io/ecosystem/wasmer/getting-started][the Wasmer documentation]] to see how to install it.

52
docs/org/reference/tooling/emacs.org
View File

@ -1,52 +0,0 @@
** 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:
#+begin_src sh
git clone https://github.com/anoma/juvix-mode.git
#+end_src
To install it add the following lines to your
Emacs configuration file:
#+begin_src elisp
(push "/path/to/juvix-mode/" load-path)
(require 'juvix-mode)
#+end_src
Make sure that Juvix is installed in your =PATH=.
The Juvix major mode will be activated automatically for =.juvix= files.
*** Keybindings
| Key | Function Name | Description |
|-----------+-------------------------+-------------------------------------------------------|
| =C-c C-l= | =juvix-load= | Runs the scoper and adds semantic syntax highlighting |
| =M-.= | =juvix-goto-definition= | Go to the definition of symbol at point |
| =C-c C-f= | =juvix-format-buffer= | Format the current buffer |
*** Emacs installation
Most Linux distributions contain an Emacs package which can be
installed with your package manager (=sudo apt install emacs= on
Ubuntu). On macOS, it is recommended to install Emacs Plus via
Homebrew: =brew install emacs-plus=. Using the Emacs Homebrew casks is
not recommended.
*** Common problems
- Error "Symbol's value as variable is void: sh:1:"
Make sure the juvix executable is on the Emacs' =exec-path=. Note
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
[[https://github.com/purcell/exec-path-from-shell][exec-path-from-shell]] package (available on MELPA). Alternatively,
one may set =exec-path= to match shell =PATH= by following the
instructions from [[https://www.emacswiki.org/emacs/ExecPath][EmacsWiki]].

20
docs/org/reference/tooling/testing.org
View File

@ -1,20 +0,0 @@
* Testing
*** Dependencies
See [[./doctor.html][Installing dependencies]] for instructions on how to setup the testing
environment for the WASM compiler tests.
*** Running
Run tests using:
#+begin_src shell
stack test
#+end_src
To run tests, ignoring all the WASM tests:
#+begin_src shell
stack test --ta '-p "! /slow tests/"'
#+end_src

1
docs/org/tutorials/README.org
View File

@ -1 +0,0 @@
- [[./nodejs-interop.md][NodeJS Interop]]

78
docs/org/tutorials/emacs.org
View File

@ -1,78 +0,0 @@
* Juvix Emacs mode tutorial
First, follow the instructions in the [[../reference/tooling/emacs.md][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.
#+begin_example
module Hello;
open import Stdlib.Prelude;
main : IO;
main := printStringLn "Hello world!";
end;
#+end_example
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".
#+begin_example
module Hello;
open import Stdlib.Prelude;
main : IO;
main := printStringLna "Hello world!";
end;
#+end_example
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.
#+begin_example
module Hello;
open import Stdlib.Prelude;
print : IO;
print := printStringLn "Hello world!";
main : IO;
main := print;
end;
#+end_example
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.
#+begin_example
module Hello;
open import Stdlib.Prelude;
print : IO;
print := printStringLn "Hello world!";
main : IO;
main := print;
end;
#+end_example

517
docs/org/tutorials/learn.org
View File

@ -1,517 +0,0 @@
* Juvix tutorial
NOTE: This is a tutorial for Juvix version 0.3. Earlier versions do not support all of the syntax described here.
* [[./learn.md#juvix-repl][Juvix REPL]]
* [[./learn.md#basic-expressions][Basic expressions]]
* [[./learn.md#files-modules-and-compilation][Files, modules and compilation]]
* [[./learn.md#output][Output]]
* [[./learn.md#data-types-and-functions][Data types and functions]]
* [[./learn.md#pattern-matching][Pattern matching]]
* [[./learn.md#comparisons-and-conditionals][Comparisons and conditionals]]
* [[./learn.md#local-definitions][Local definitions]]
* [[./learn.md#recursion][Recursion]]
* [[./learn.md#partial-application-and-higher-order-functions][Partial application and higher-order functions]]
* [[./learn.md#polymorphism][Polymorphism]]
* [[./learn.md#tail-recursion][Tail recursion]]
* [[./learn.md#totality-checking][Totality checking]]
* [[./learn.md#exercises][Exercises]]
** Juvix REPL
After [[../howto/installing.md][installing Juvix]], launch the Juvix REPL:
#+begin_src shell
juvix repl
#+end_src
The response should be similar to:
#+begin_example
Juvix REPL version 0.3: https://juvix.org. Run :help for help
OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
Stdlib.Prelude>
#+end_example
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:
#+begin_example
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
#+end_example
By default Juvix operates on nonnegative 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
#+begin_example
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
#+end_example
and strings, pairs and lists:
#+begin_example
Stdlib.Prelude> "Hello world!"
"Hello world!"
Stdlib.Prelude> (1, 2)
(1, 2)
Stdlib.Prelude> 1 :: 2 :: nil
1 :: 2 :: nil
#+end_example
In fact, you can use all functions and types from the [[https://anoma.github.io/juvix-stdlib/Stdlib.Prelude.html][Stdlib.Prelude]] module of the [[https://anoma.github.io/juvix-stdlib][standard library]], which is preloaded by default.
#+begin_example
Stdlib.Prelude> length (1 :: 2 :: nil)
3
Stdlib.Prelude> null (1 :: 2 :: nil)
false
Stdlib.Prelude> swap (1, 2)
(2, 1)
#+end_example
** 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.md][Emacs mode]] and a [[./vscode.md][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=:
#+begin_example
-- 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;
#+end_example
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.,
#+begin_example
printNat 3 >> printString " + " >> printNatLn 4
#+end_example
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:
#+begin_example
Stdlib.Prelude> :type 1
Nat
Stdlib.Prelude> :type true
Bool
#+end_example
The types =Nat= and =Bool= are defined in the standard library.
The type =Bool= has two constructors =true= and =false=.
#+begin_example
type Bool :=
| true : Bool
| false : Bool;
#+end_example
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:
#+begin_example
not : Bool -> Bool;
not true := false;
not false := true;
#+end_example
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:
#+begin_example
type Nat :=
| zero : Nat
| suc : Nat -> Nat;
#+end_example
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:
#+begin_example
infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
#+end_example
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
#+begin_example
(suc (suc zero)) + zero
#+end_example
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:
#+begin_example
suc (suc zero + zero)
#+end_example
Again, the second clause matches, now with both =a= and =b= being =zero=. After replacing with the right-hand side, we obtain:
#+begin_example
suc (suc (zero + zero))
#+end_example
Now the first clause matches and finally we obtain the result
#+begin_example
suc (suc zero)
#+end_example
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:
#+begin_example
even : Nat -> Bool;
even zero := true;
even (suc zero) := false;
even (suc (suc n)) := even n;
#+end_example
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.
#+begin_example
isPositive : Nat -> Bool;
isPositive zero := false;
isPositive (suc _) := true;
#+end_example
The above function could also be written as:
#+begin_example
isPositive : Nat -> Bool;
isPositive zero := false;
isPositive _ := true;
#+end_example
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.
#+begin_example
Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
1
#+end_example
** 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:
#+begin_example
open import Stdlib.Data.Nat.Ord;
max3 : Nat -> Nat -> Nat -> Nat;
max3 x y z := if (x > y) (max x z) (max y z);
#+end_example
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 [[./learn.md#partial-application-and-higher-order-functions][Partial application and higher-order functions]] below).
** Local definitions
Juvix supports local definitions with let-expressions.
#+begin_example
f : Nat -> Nat;
f a := let x : Nat := a + 5;
y : Nat := a * 7 + x
in
x * y;
#+end_example
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:
#+begin_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
#+end_example
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:
#+begin_example
type NList :=
| nnil : NList
| ncons : Nat -> NList -> NList;
#+end_example
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:
#+begin_example
nlength : NList -> Nat;
nlength nnil := 0;
nlength (ncons _ xs) := nlength xs + 1;
#+end_example
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.
#+begin_example
open import Stdlib.Data.Nat.Ord; -- for `max`
nmaximum : NList -> Nat;
nmaximum nnil := 0;
nmaximum (ncons x xs) := max x (nmaximum xs);
#+end_example
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.
#+begin_example
type Tree :=
| leaf : Nat -> Tree
| node : Nat -> Tree -> Tree -> Tree;
#+end_example
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:
#+begin_example
mirror : Tree -> Tree;
mirror (leaf x) := leaf x;
mirror (node x l r) := node x (mirror r) (mirror l);
#+end_example
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.
#+begin_example
nmap : (Nat -> Nat) -> NList -> NList;
nmap _ nnil := nnil;
nmap f (ncons x xs) := ncons (f x) (nmap f xs);
#+end_example
The application
#+begin_example
nmap \{ x := div x 2 } lst
#+end_example
divides every element of =lst= by =2=, rounding down the result. The expression
#+begin_example
\{ x := div x 1 }
#+end_example
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:
#+begin_example
infixr 5 ::;
type List (A : Type) :=
| nil : List A
| :: : A -> List A -> List A;
#+end_example
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:
#+begin_example
map : {A B : Type} -> (A -> B) -> List A -> List B;
map f nil := nil;
map f (h :: hs) := f h :: map f hs;
#+end_example
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:
#+begin_example
f {implArg1} .. {implArgK} arg1 .. argN
#+end_example
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:
#+begin_example
sum : NList -> Nat;
sum nnil := 0;
sum (ncons x xs) := x + sum xs;
#+end_example
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:
#+begin_example
var sum : Nat := 0;
while (lst /= nnil) {
sum := sum + head lst;
lst := tail lst;
};
return sum;
#+end_example
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.
#+begin_example
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;
#+end_example
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.
# A shorter way of writing the above =sum= function is to use a /named lambda/:
# #+begin_example
# sum : NList -> Nat;
# sum := go(acc := 0)@\{
# acc nnil := acc;
# acc (ncons x xs) := go (acc + x) xs;
# };
# #+end_example
# The syntax
# #+begin_example
# go(acc1 := v1= ... accn := vn)@\{ <clauses> }
# #+end_example
# introduces a recursive function =go= with =n= accumulators =acc1=, ..., =accn= and further =k= arguments of the lambda expression (above =n = k = 1=). The value of the entire expression is =go v1 ... vn=. The scope of =go= is the lambda expression, i.e., it is not visible outside of it.
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.
#+begin_example
var cur : Nat := 0;
var next : Nat := 1;
while (n /= 0) {
var tmp := next;
next := cur + next;
cur := tmp;
n := n - 1;
};
return cur;
#+end_example
An equivalent functional program is:
#+begin_example
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;
#+end_example
A naive definition of the Fibonacci function runs in exponential time:
#+begin_example
fib : Nat -> Nat;
fib zero := 0;
fib (suc zero) := 1;
fib (suc (suc n)) := fib n + fib (suc n);
#+end_example
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:
* [[../explanations/totality/termination.md][termination]],
* [[../explanations/totality/coverage.md][coverage]],
* [[../explanations/totality/positive.md][strict positivity]].
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
#+begin_example
fact : Nat -> Nat;
fact x := if (x == 0) 1 (x * fact (sub x 1));
#+end_example
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:
#+begin_example
fact : Nat -> Nat;
fact zero := 1;
fact x@(suc n) := x * fact n;
#+end_example
Sometimes, such a reformulation is not possible. Then one can use the =terminating= keyword to forgoe the termination check.
#+begin_example
terminating
log2 : Nat -> Nat;
log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
#+end_example
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:
#+begin_example
even : Nat -> Bool;
even zero := true;
even (suc (suc n)) := even n;
#+end_example
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 [[https://docs.juvix.org/examples/html/Tutorial/Tutorial.html][advanced tutorial]] and the [[../reference/examples.md][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?
#+begin_example
half : Nat -> Nat;
half n := if (n < 2) 0 (half (n - 2) + 1);
#+end_example
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.
#+begin_example
type Tree :=
| leaf : Nat -> Tree
| node : Nat -> Tree -> Tree -> Tree;
#+end_example
Analogously to the =map= function for lists, define a function
#+begin_example
tmap : (Nat -> Nat) -> Tree -> Tree
#+end_example
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,
#+begin_example
comp (suc :: (*) 2 :: \{x := sub x 1} :: nil)
#+end_example
should be a function which given =x= computes =2(x - 1) + 1=.

108
docs/org/tutorials/nodejs-interop.org
View File

@ -1,108 +0,0 @@
* NodeJS Interop
A Juvix module can be compiled to a Wasm module. When a Wasm module is
instantiated by a host, functions from the host can be injected into a Wasm
module and functions from the Wasm module can be called by the host.
In this tutorial you will see how to call host functions in Juvix and call Juvix
functions from the host using the Wasm mechanism.
** The Juvix module
The following Juvix module has two functions.
The function =hostDisplayString= is an =axiom= with no corresponding =compile=
block that implements it. We will inject an implementation for this function
when we instantiate the module from NodeJS.
The function =juvixRender= is a normal Juvix function. We will call this from
NodeJS.
#+begin_src
-- NodeJsInterop.juvix
module NodeJsInterop;
open import Stdlib.Prelude;
axiom hostDisplayString : String → IO;
juvixRender : IO;
juvixRender := hostDisplayString "Hello World from Juvix!";
end;
#+end_src
** Compiling the Juvix module
The Juvix module can be compiled using the following command:
#+begin_src
juvix compile -t wasm -r standalone NodeJsInterop.juvix
#+end_src
This will create a file containing a Wasm module called =NodeJsInterop.wasm=.
** The NodeJS module
The following NodeJS module demonstrates both calling a Juvix function from
NodeJS and injecting a NodeJS function into a Juvix module.
The NodeJS function =hostDisplayString= is passed to the Wasm module
=NodeJSInterop.wasm= when it is instantiated. After instantiation the Juvix
function =juvixRender= is called.
The functions =ptrToCstr= and =cstrlen= are necessary to convert the =char=
pointer passed from Juvix to a JS =String=.
#+begin_src
// NodeJSInterop.js
const fs = require('fs');
let wasmModule = null;
function cstrlen(mem, ptr) {
let len = 0;
while (mem[ptr] != 0) {
len++;
ptr++;
}
return len;
}
function ptrToCstr(ptr) {
const wasmMemory = wasmModule.instance.exports.memory.buffer;
const mem = new Uint8Array(wasmMemory);
const len = cstrlen(mem, ptr);
const bytes = new Uint8Array(wasmMemory, ptr, len);
return new TextDecoder().decode(bytes);
}
function hostDisplayString(strPtr) {
const text = ptrToCstr(strPtr);
console.log(text);
}
const wasmBuffer = fs.readFileSync("NodeJsInterop.wasm");
WebAssembly.instantiate(wasmBuffer, {
env: {
hostDisplayString,
}
}).then((w) => {
wasmModule = w;
wasmModule.instance.exports.juvixRender();
});
#+end_src
** Running the Wasm module
Now you should have the files =NodeJsInterop.wasm= and =NodeJsInterop.js= in the
same directory. Run the following command to execute the module:
#+begin_src
node NodeJsInterop.js
#+end_src
You should see the following output:
#+begin_src
Hello World from Juvix!
#+end_src

66
docs/org/quick-start.org → docs/quick-start.md
View File

@ -1,64 +1,63 @@
* Quick Start
# Quick Start
#+begin_html
<a href="https://github.com/anoma/juvix">
<img align="left" width="200" height="200" alt="Juvix Mascot" src="assets/images/tara-teaching.svg" />
</a>
#+end_html
To install Juvix, follow the instructions in the [[./howto/installing.md][Installation How-to]].
To install Juvix, follow the instructions in the [Installation
How-to](./howto/installing.md).
After installation, run =juvix --help= to see the list of commands.
After installation, run `juvix --help` to see the list of commands.
Run Juvix doctor to check your system setup:
#+begin_src shell
```shell
juvix doctor
#+end_src
```
** CLI Usage Examples
## CLI Usage Examples
Create a new package:
#+begin_src shell
```shell
juvix init
#+end_src
```
Compile a source file into an executable:
#+begin_src shell
```shell
juvix compile path/to/source.juvix
#+end_src
```
Compile a source file into a WebAssembly binary:
#+begin_src shell
```shell
juvix compile -t wasm path/to/source.juvix
#+end_src
```
Launch the REPL:
#+begin_src shell
```shell
juvix repl
#+end_src
```
Typecheck a source file:
#+begin_src shell
```shell
juvix typecheck path/to/source.juvix
#+end_src
```
Generate HTML representations of a source file and its imports:
#+begin_src shell
```shell
juvix html --recursive path/to/source.juvix
#+end_src
```
** The Hello World example
## The Hello World example
This is the Juvix source code of the traditional Hello World program.
#+begin_src shell
```shell
-- HelloWorld.juvix
module HelloWorld;
@ -68,22 +67,25 @@ main : IO;
main := printStringLn "hello world!";
end;
#+end_src
```
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:
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:
#+begin_src shell
```shell
juvix compile HelloWorld.juvix
./HelloWorld
#+end_src
```
You should see the output: =hello world!=
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 [[https://anoma.github.io/juvix/howto/installing.html][Installation How-to]] for more information. You can also run =juvix doctor= to check your setup.
The source code can also be compiled to a WebAssembly binary. This
requires some additional setup. See the [Installation
How-to](https://anoma.github.io/juvix/howto/installing.html) for more
information. You can also run `juvix doctor` to check your setup.
#+begin_src shell
```shell
juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasm
#+end_src
```

1
docs/reference/benchmarks.md Normal file
View File

@ -0,0 +1 @@
# Benchmarks

10
docs/reference/examples.md Normal file
View File

@ -0,0 +1,10 @@
The following links are clickable versions of their corresponding Juvix
programs. The HTML output is generated by running
`juvix html --recursive FileName.juvix`.
- [HelloWorld.juvix](https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html)
- [Fibonacci.juvix](https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html)
- [Hanoi.juvix](https://docs.juvix.org/examples/html/Hanoi/Hanoi.html)
- [PascalsTriangle.juvix](https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html)
- [Collatz.juvix](https://docs.juvix.org/examples/html/Collatz/Collatz.html)
- [TicTacToe.juvix](https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html)

1
docs/reference/judoc.md Normal file
View File

@ -0,0 +1 @@
# Judoc reference

7
docs/reference/language/README.md Normal file
View File

@ -0,0 +1,7 @@
- [Functions](./functions.md)
- [Data types](./datatypes.md)
- [Modules](./modules.md)
- [Local definitions](./let.md)
- [Control structures](./control.md)
- [Comments](./comments.md)
- [Axioms](./axioms.md)

16
docs/reference/language/axioms.md Normal file
View File

@ -0,0 +1,16 @@
# 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.

30
docs/reference/language/builtins.md Normal file
View File

@ -0,0 +1,30 @@
# Built-ins
Juvix has support for the built-in natural type and a few functions that
are compiled to efficient primitives.
1. Built-in inductive definitions.
```juvix
builtin nat
type Nat :=
zero : Nat |
suc : Nat → Nat;
```
2. Builtin function definitions.
```juvix
infixl 6 +;
builtin nat-plus
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
```
3. Builtin axiom definitions.
```juvix
builtin nat-print
axiom printNat : Nat → Action;
```

19
docs/reference/language/comments.md Normal file
View File

@ -0,0 +1,19 @@
# 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!
-}

34
docs/reference/language/control.md Normal file
View File

@ -0,0 +1,34 @@
# Control structures
## Case
A case expression has the following syntax:
```juvix
case value
| pat1 := branch1
..
| patN := branchN
```
For example, one can evaluate the following expression in the REPL:
```juvix
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.

57
docs/reference/language/datatypes.md Normal file
View File

@ -0,0 +1,57 @@
# 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`.
```juvix
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.
```juvix
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:
```juvix
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.
```juvix
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](https://anoma.github.io/juvix-stdlib/).

93
docs/reference/language/functions.md Normal file
View File

@ -0,0 +1,93 @@
# 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.
```juvix
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.
```juvix
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`.
```juvix
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:
```juvix
\{| 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:
```juvix
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:
```juvix
multiplyByTwo : Nat -> Nat := \{n := 2 * n};
```

18
docs/reference/language/let.md Normal file
View File

@ -0,0 +1,18 @@
# Local definitions
Local definitions are introduced with the `let` construct.
```juvix
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.

166
docs/reference/language/modules.md Normal file
View File

@ -0,0 +1,166 @@
# 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.
```juvix
-- ModuleName.juvix
module ModuleName;
end;
```
A <u>Juvix project</u> 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 <u>module</u> 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.
```juvix
-- 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 <u>open</u> an imported module making available
all its names by their unqualified name.
```juvix
-- 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.
```juvix
-- 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.
```juvix
-- 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:
```juvix
import Prelude;
open Prelude;
```
We simplify it by the expression:
```juvix
open import Prelude;
```
The `hiding` keyword can be used within an `open-import` statement.
```juvix
-- 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`.
```juvix
-- 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:
```juvix
-- B.juvix
module B;
open import A public;
end;
```

2
docs/reference/stdlib.md Normal file
View File

@ -0,0 +1,2 @@
The [Juvix standard library](https://anoma.github.io/juvix-stdlib/)
contains common functions that can be used in Juvix programs.

89
docs/reference/tooling/CLI.md Normal file
View File

@ -0,0 +1,89 @@
# CLI
## Usage
```shell
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
```shell
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`).
```shell
eval "$(juvix --bash-completion-script juvix)"
```
### Fish
Run the following command in your shell:
```shell
juvix --fish-completion-script juvix
> ~/.config/fish/completions/juvix.fish
```
### ZSH
Run the following command in your shell:
```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](https://zsh.sourceforge.io/Doc/Release/Functions.html) (which
you can inspect by running `echo $FPATH` in the shell).

4
docs/reference/tooling/README.md Normal file
View File

@ -0,0 +1,4 @@
- [Command line Interface](./CLI.md)
- [Emacs Mode](./emacs.md)
- [Test Suite](./testing.md)
- [Doctor](./doctor.md)

123
docs/reference/tooling/doctor.md Normal file
View File

@ -0,0 +1,123 @@
# 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](https://clang.llvm.org)
version 13 or later to generate binaries. You need to have Clang
available on your system `$PATH`.
Recommended installation method:
### MacOS
Use [Homebrew](https://brew.sh):
```shell
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
```shell
sudo apt install clang lldb lld
```
### Arch Linux
```shell
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](https://brew.sh) llvm
distribution:
```shell
brew install llvm
```
### Debian / Ubuntu Linux
```shell
sudo apt install lldb lld
```
### Arch Linux
```shell
sudo pacman -S lld
```
## Newer Clang version required
Juvix requires Clang version 13 or above. See the documentation on
[installing Clang](./doctor.md#could-not-find-the-clang-command).
## Clang does not support the wasm32 target
Juvix requires Clang version 13 or above. See the documentation on
[installing Clang](./doctor.md#could-not-find-the-clang-command).
## Clang does not support the wasm32-wasi target
Juvix uses [WASI - The Wasm System Interface](https://wasi.dev) 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](https://github.com/WebAssembly/wasi-sdk/releases).
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](https://github.com/WebAssembly/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](https://github.com/WebAssembly/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](./doctor.md#download-the-wasi-sysroot-and-set-wasi_sysroot_path).
## Could not find the wasmer command
The Juvix test suite uses [Wasmer](https://wasmer.io) as a Wasm runtime
to execute compiled Wasm binaries. See [the Wasmer
documentation](https://docs.wasmer.io/ecosystem/wasmer/getting-started)
to see how to install it.

52
docs/reference/tooling/emacs.md Normal file
View File

@ -0,0 +1,52 @@
## 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:
```bash
git clone https://github.com/anoma/juvix-mode.git
```
To install it add the following lines to your Emacs configuration file:
```elisp
(push "/path/to/juvix-mode/" load-path)
(require 'juvix-mode)
```
Make sure that Juvix is installed in your `PATH`.
The Juvix major mode will be activated automatically for `.juvix` files.
### Keybindings
| Key | Function Name | Description |
| --------- | ----------------------- | ----------------------------------------------------- |
| `C-c C-l` | `juvix-load` | Runs the scoper and adds semantic syntax highlighting |
| `M-.` | `juvix-goto-definition` | Go to the definition of symbol at point |
| `C-c C-f` | `juvix-format-buffer` | Format the current buffer |
### Emacs installation
Most Linux distributions contain an Emacs package which can be installed
with your package manager (`sudo apt install emacs` on Ubuntu). On
macOS, it is recommended to install Emacs Plus via Homebrew:
`brew install emacs-plus`. Using the Emacs Homebrew casks is not
recommended.
### Common problems
- Error "Symbol's value as variable is void: sh:1:"
Make sure the juvix executable is on the Emacs' `exec-path`. Note
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](https://github.com/purcell/exec-path-from-shell)
package (available on MELPA). Alternatively, one may set `exec-path`
to match shell `PATH` by following the instructions from
[EmacsWiki](https://www.emacswiki.org/emacs/ExecPath).

20
docs/reference/tooling/testing.md Normal file
View File

@ -0,0 +1,20 @@
# Testing
### Dependencies
See [Installing dependencies](./doctor.html) for instructions on how to
setup the testing environment for the WASM compiler tests.
### Running
Run tests using:
```shell
stack test
```
To run tests, ignoring all the WASM tests:
```shell
stack test --ta '-p "! /slow tests/"'
```

1
docs/tutorials/README.md Normal file
View File

@ -0,0 +1 @@
- [NodeJS Interop](./nodejs-interop.md)

79
docs/tutorials/emacs.md Normal file
View File

@ -0,0 +1,79 @@
# Juvix Emacs mode tutorial
First, follow the instructions in the [Emacs Mode
Reference](../reference/tooling/emacs.md) to install the Juvix Emacs
mode. Once you've successfully set it up, create a file `Hello.juvix`
with the following content.
```juvix
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".
```juvix
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.
```juvix
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.
```juvix
module Hello;
open import Stdlib.Prelude;
print : IO;
print := printStringLn "Hello world!";
main : IO;
main := print;
end;
```

792
docs/tutorials/learn.md Normal file
View File

@ -0,0 +1,792 @@
# Juvix tutorial
NOTE: This is a tutorial for Juvix version 0.3. Earlier versions do not
support all the syntax described here.
- [Juvix REPL](./learn.md#juvix-repl)
- [Basic expressions](./learn.md#basic-expressions)
- [Files, modules and
compilation](./learn.md#files-modules-and-compilation)
- [Output](./learn.md#output)
- [Data types and functions](./learn.md#data-types-and-functions)
- [Pattern matching](./learn.md#pattern-matching)
- [Comparisons and
conditionals](./learn.md#comparisons-and-conditionals)
- [Local definitions](./learn.md#local-definitions)
- [Recursion](./learn.md#recursion)
- [Partial application and higher-order
functions](./learn.md#partial-application-and-higher-order-functions)
- [Polymorphism](./learn.md#polymorphism)
- [Tail recursion](./learn.md#tail-recursion)
- [Totality checking](./learn.md#totality-checking)
- [Exercises](./learn.md#exercises)
## Juvix REPL
After [installing Juvix](../howto/installing.md), launch the Juvix REPL:
```shell
juvix repl
```
The response should be similar to:
```juvix
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:
```juvix
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
```juvix
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:
```juvix
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](https://anoma.github.io/juvix-stdlib/Stdlib.Prelude.html)
module of the [standard library](https://anoma.github.io/juvix-stdlib),
which is preloaded by default.
```juvix
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](./emacs.md) and a
[VSCode extension](./vscode.md) 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`:
```juvix
-- 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.,
```juvix
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:
```juvix
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`.
```juvix
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:
```juvix
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:
```juvix
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:
```juvix
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
```juvix
(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:
```juvix
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:
```juvix
suc (suc (zero + zero))
```
Now the first clause matches and finally we obtain the result
```juvix
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:
```juvix
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.
```juvix
isPositive : Nat -> Bool;
isPositive zero := false;
isPositive (suc _) := true;
```
The above function could also be written as:
```juvix
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.
```juvix
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:
```juvix
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](./learn.md#partial-application-and-higher-order-functions)
below).
## Local definitions
Juvix supports local definitions with let-expressions.
```juvix
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:
```juvix
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:
```juvix
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:
```juvix
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.
```juvix
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.
```juvix
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:
```juvix
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.
```juvix
nmap : (Nat -> Nat) -> NList -> NList;
nmap _ nnil := nnil;
nmap f (ncons x xs) := ncons (f x) (nmap f xs);
```
The application
```juvix
nmap \{ x := div x 2 } lst
```
divides every element of `lst` by `2`, rounding down the result. The
expression
```juvix
\{ 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:
```juvix
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:
```juvix
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:
```juvix
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:
```juvix
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:
```juvix
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.
```juvix
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.
```juvix
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:
```juvix
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:
```juvix
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:
- [termination](../explanations/totality/termination.md),
- [coverage](../explanations/totality/coverage.md),
- [strict positivity](../explanations/totality/positive.md).
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
```juvix
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:
```juvix
fact : Nat -> Nat;
fact zero := 1;
fact x@(suc n) := x * fact n;
```
Sometimes, such a reformulation is not possible. Then one can use the
`terminating` keyword to forgoe the termination check.
```juvix
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:
```juvix
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](https://docs.juvix.org/examples/html/Tutorial/Tutorial.html)
and the [Juvix program examples](../reference/examples.md).
1. Define a function `prime : Nat -> Nat` which checks if a given
natural number is prime.
2. What is wrong with the following definition?
```juvix
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.
```juvix
type Tree :=
| leaf : Nat -> Tree
| node : Nat -> Tree -> Tree -> Tree;
```
Analogously to the `map` function for lists, define a function
```juvix
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,
```juvix
comp (suc :: (*) 2 :: \{x := sub x 1} :: nil)
```
should be a function which given `x` computes `2(x - 1) + 1`.

101
docs/tutorials/nodejs-interop.md Normal file
View File

@ -0,0 +1,101 @@
# NodeJS Interop
A Juvix module can be compiled to a Wasm module. When a Wasm module is
instantiated by a host, functions from the host can be injected into a
Wasm module and functions from the Wasm module can be called by the
host.
In this tutorial you will see how to call host functions in Juvix and
call Juvix functions from the host using the Wasm mechanism.
## The Juvix module
The following Juvix module has two functions.
The function `hostDisplayString` is an `axiom` with no corresponding
`compile` block that implements it. We will inject an implementation for
this function when we instantiate the module from NodeJS.
The function `juvixRender` is a normal Juvix function. We will call this
from NodeJS.
-- NodeJsInterop.juvix
module NodeJsInterop;
open import Stdlib.Prelude;
axiom hostDisplayString : String → IO;
juvixRender : IO;
juvixRender := hostDisplayString "Hello World from Juvix!";
end;
## Compiling the Juvix module
The Juvix module can be compiled using the following command:
juvix compile -t wasm -r standalone NodeJsInterop.juvix
This will create a file containing a Wasm module called
`NodeJsInterop.wasm`.
## The NodeJS module
The following NodeJS module demonstrates both calling a Juvix function
from NodeJS and injecting a NodeJS function into a Juvix module.
The NodeJS function `hostDisplayString` is passed to the Wasm module
`NodeJSInterop.wasm` when it is instantiated. After instantiation the
Juvix function `juvixRender` is called.
The functions `ptrToCstr` and `cstrlen` are necessary to convert the
`char` pointer passed from Juvix to a JS `String`.
// NodeJSInterop.js
const fs = require('fs');
let wasmModule = null;
function cstrlen(mem, ptr) {
let len = 0;
while (mem[ptr] != 0) {
len++;
ptr++;
}
return len;
}
function ptrToCstr(ptr) {
const wasmMemory = wasmModule.instance.exports.memory.buffer;
const mem = new Uint8Array(wasmMemory);
const len = cstrlen(mem, ptr);
const bytes = new Uint8Array(wasmMemory, ptr, len);
return new TextDecoder().decode(bytes);
}
function hostDisplayString(strPtr) {
const text = ptrToCstr(strPtr);
console.log(text);
}
const wasmBuffer = fs.readFileSync("NodeJsInterop.wasm");
WebAssembly.instantiate(wasmBuffer, {
env: {
hostDisplayString,
}
}).then((w) => {
wasmModule = w;
wasmModule.instance.exports.juvixRender();
});
## Running the Wasm module
Now you should have the files `NodeJsInterop.wasm` and
`NodeJsInterop.js` in the same directory. Run the following command to
execute the module:
node NodeJsInterop.js
You should see the following output:
Hello World from Juvix!

0
docs/org/tutorials/structure.org → docs/tutorials/structure.md
View File

24
docs/org/tutorials/vscode.org → docs/tutorials/vscode.md
View File

@ -1,14 +1,12 @@
* Juvix VSCode extension tutorial
# 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.
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.
Once you've installed the Juvix extension, you can open a Juvix file.
For example, create a `Hello.juvix` file with the following content.
#+begin_example
```juvix
module Hello;
open import Stdlib.Prelude;
@ -17,16 +15,16 @@ main : IO;
main := printStringLn "Hello world!";
end;
#+end_example
```
Syntax should be automatically highlighted for any file with =.juvix=
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.
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

1
examples/milestone/TicTacToe/TicTacToe.juvix
View File

@ -1,4 +1,3 @@
module TicTacToe;
import CLI.TicTacToe;
import Web.TicTacToe;
end;

13
package.yaml
View File

@ -1,10 +1,17 @@
name: juvix
version: 0.3.0
license: GPL-3.0-only
license-file: LICENSE
license-file: LICENSE.md
copyright: (c) 2022- Heliax AG.
maintainer: The PLT Team at Heliax AG <hello@heliax.dev>
author: [ Jonathan Prieto-Cubides , Jan Mas Rovira , Paul Cadman , Lukasz Czajka , Github's contributors ]
author:
[
Jonathan Prieto-Cubides,
Jan Mas Rovira,
Paul Cadman,
Lukasz Czajka,
Github's contributors,
]
tested-with: ghc == 9.2.6
homepage: https://juvix.org
bug-reports: https://github.com/anoma/juvix/issues
@ -13,7 +20,7 @@ category: Compilers/Interpreters
github: anoma/juvix
extra-source-files:
- README.org
- README.md
- assets/css/*.css
- assets/js/*.js
- assets/images/*.svg

317
theme/index.hbs Normal file
View File

@ -0,0 +1,317 @@
<!DOCTYPE HTML>
<html lang="{{ language }}" class="sidebar-visible no-js {{ default_theme }}">
<head>
<!-- Book generated using mdBook -->
<meta charset="UTF-8">
<title>{{ title }}</title>
{{#if is_print }}
<meta name="robots" content="noindex" />
{{/if}}
{{#if base_url}}
<base href="{{ base_url }}">
{{/if}}
<!-- Custom HTML head -->
{{> head}}
<meta name="description" content="{{ description }}">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#ffffff" />
{{#if favicon_svg}}
<link rel="icon" href="{{ path_to_root }}favicon.svg">
{{/if}}
{{#if favicon_png}}
<link rel="shortcut icon" href="{{ path_to_root }}favicon.png">
{{/if}}
<link rel="stylesheet" href="{{ path_to_root }}css/variables.css">
<link rel="stylesheet" href="{{ path_to_root }}css/general.css">
<link rel="stylesheet" href="{{ path_to_root }}css/chrome.css">
{{#if print_enable}}
<link rel="stylesheet" href="{{ path_to_root }}css/print.css" media="print">
{{/if}}
<!-- Fonts -->
<link rel="stylesheet" href="{{ path_to_root }}FontAwesome/css/font-awesome.css">
{{#if copy_fonts}}
<link rel="stylesheet" href="{{ path_to_root }}fonts/fonts.css">
{{/if}}
<!-- Highlight.js Stylesheets -->
<link rel="stylesheet" href="{{ path_to_root }}highlight.css">
<link rel="stylesheet" href="{{ path_to_root }}tomorrow-night.css">
<link rel="stylesheet" href="{{ path_to_root }}ayu-highlight.css">
<!-- Custom theme stylesheets -->
{{#each additional_css}}
<link rel="stylesheet" href="{{ ../path_to_root }}{{ this }}">
{{/each}}
{{#if mathjax_support}}
<!-- MathJax -->
<script async src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
{{/if}}
</head>
<body>
<div id="body-container">
<!-- Provide site root to javascript -->
<script>
var path_to_root = "{{ path_to_root }}";
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "{{ preferred_dark_theme }}" : "{{ default_theme }}";
</script>
<!-- Work around some values being stored in localStorage wrapped in quotes -->
<script>
try {
var theme = localStorage.getItem('mdbook-theme');
var sidebar = localStorage.getItem('mdbook-sidebar');
if (theme.startsWith('"') && theme.endsWith('"')) {
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
}
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
}
} catch (e) { }
</script>
<!-- Set the theme before any content is loaded, prevents flash -->
<script>
var theme;
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
var html = document.querySelector('html');
html.classList.remove('no-js')
html.classList.remove('{{ default_theme }}')
html.classList.add(theme);
html.classList.add('js');
</script>
<!-- Hide / unhide sidebar before it is displayed -->
<script>
var html = document.querySelector('html');
var sidebar = null;
if (document.body.clientWidth >= 1080) {
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
sidebar = sidebar || 'visible';
} else {
sidebar = 'hidden';
}
html.classList.remove('sidebar-visible');
html.classList.add("sidebar-" + sidebar);
</script>
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
{{#toc}}{{/toc}}
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
<div id="page-wrapper" class="page-wrapper">
<div class="page">
{{> header}}
<div id="menu-bar-hover-placeholder"></div>
<div id="menu-bar" class="menu-bar sticky bordered">
<div class="left-buttons">
<button id="sidebar-toggle" class="icon-button" type="button" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
<i class="fa fa-bars"></i>
</button>
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
<i class="fa fa-paint-brush"></i>
</button>
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
</ul>
{{#if search_enabled}}
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
<i class="fa fa-search"></i>
</button>
{{/if}}
</div>
<h1 class="menu-title">{{ book_title }}</h1>
<div class="right-buttons">
{{#if print_enable}}
<a href="{{ path_to_root }}print.html" title="Print this book" aria-label="Print this book">
<i id="print-button" class="fa fa-print"></i>
</a>
{{/if}}
{{#if git_repository_url}}
<a href="{{git_repository_url}}" title="Git repository" aria-label="Git repository">
<i id="git-repository-button" class="fa {{git_repository_icon}}"></i>
</a>
{{/if}}
{{#if git_repository_edit_url}}
<a href="{{git_repository_edit_url}}" title="Suggest an edit" aria-label="Suggest an edit">
<i id="git-edit-button" class="fa fa-edit"></i>
</a>
{{/if}}
</div>
</div>
{{#if search_enabled}}
<div id="search-wrapper" class="hidden">
<form id="searchbar-outer" class="searchbar-outer">
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
</form>
<div id="searchresults-outer" class="searchresults-outer hidden">
<div id="searchresults-header" class="searchresults-header"></div>
<ul id="searchresults">
</ul>
</div>
</div>
{{/if}}
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
<script>
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
});
</script>
<div id="content" class="content">
<main><div class="sidetoc"><nav class="pagetoc"></nav></div>
{{{ content }}}
</main>
<nav class="nav-wrapper" aria-label="Page navigation">
<!-- Mobile navigation buttons -->
{{#previous}}
<a rel="prev" href="{{ path_to_root }}{{link}}" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
{{/previous}}
{{#next}}
<a rel="next" href="{{ path_to_root }}{{link}}" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
{{/next}}
<div style="clear: both"></div>
</nav>
</div>
</div>
<nav class="nav-wide-wrapper" aria-label="Page navigation">
{{#previous}}
<a rel="prev" href="{{ path_to_root }}{{link}}" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
{{/previous}}
{{#next}}
<a rel="next" href="{{ path_to_root }}{{link}}" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
{{/next}}
</nav>
</div>
{{#if live_reload_endpoint}}
<!-- Livereload script (if served using the cli tool) -->
<script>
const wsProtocol = location.protocol === 'https:' ? 'wss:' : 'ws:';
const wsAddress = wsProtocol + "//" + location.host + "/" + "{{{live_reload_endpoint}}}";
const socket = new WebSocket(wsAddress);
socket.onmessage = function (event) {
if (event.data === "reload") {
socket.close();
location.reload();
}
};
window.onbeforeunload = function() {
socket.close();
}
</script>
{{/if}}
{{#if google_analytics}}
<!-- Google Analytics Tag -->
<script>
var localAddrs = ["localhost", "127.0.0.1", ""];
// make sure we don't activate google analytics if the developer is
// inspecting the book locally...
if (localAddrs.indexOf(document.location.hostname) === -1) {
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
(i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
})(window,document,'script','https://www.google-analytics.com/analytics.js','ga');
ga('create', '{{google_analytics}}', 'auto');
ga('send', 'pageview');
}
</script>
{{/if}}
{{#if playground_line_numbers}}
<script>
window.playground_line_numbers = true;
</script>
{{/if}}
{{#if playground_copyable}}
<script>
window.playground_copyable = true;
</script>
{{/if}}
{{#if playground_js}}
<script src="{{ path_to_root }}ace.js"></script>
<script src="{{ path_to_root }}editor.js"></script>
<script src="{{ path_to_root }}mode-rust.js"></script>
<script src="{{ path_to_root }}theme-dawn.js"></script>
<script src="{{ path_to_root }}theme-tomorrow_night.js"></script>
{{/if}}
{{#if search_js}}
<script src="{{ path_to_root }}elasticlunr.min.js"></script>
<script src="{{ path_to_root }}mark.min.js"></script>
<script src="{{ path_to_root }}searcher.js"></script>
{{/if}}
<script src="{{ path_to_root }}clipboard.min.js"></script>
<script src="{{ path_to_root }}highlight.js"></script>
<script src="{{ path_to_root }}book.js"></script>
<!-- Custom JS scripts -->
{{#each additional_js}}
<script src="{{ ../path_to_root }}{{this}}"></script>
{{/each}}
{{#if is_print}}
{{#if mathjax_support}}
<script>
window.addEventListener('load', function() {
MathJax.Hub.Register.StartupHook('End', function() {
window.setTimeout(window.print, 100);
});
});
</script>
{{else}}
<script>
window.addEventListener('load', function() {
window.setTimeout(window.print, 100);
});
</script>
{{/if}}
{{/if}}
</div>
</body>
</html>

0
theme/latex-macros.txt Normal file
View File

57
theme/pagetoc.css Normal file
View File

@ -0,0 +1,57 @@
@media only screen and (max-width: 1439px) {
.sidetoc {
display: none;
}
}
@media only screen and (min-width: 1440px) {
main {
position: relative;
}
.sidetoc {
margin-left: auto;
margin-right: auto;
left: calc(100% + (var(--content-max-width)) / 4 - 140px);
position: absolute;
}
.pagetoc {
position: fixed;
width: 200px;
height: calc(100vh - var(--menu-bar-height) - 0.67em * 4);
overflow: auto;
}
.pagetoc a {
border-left: 1px solid var(--sidebar-bg);
color: var(--fg) !important;
display: block;
padding-bottom: 5px;
padding-top: 5px;
padding-left: 10px;
text-align: left;
text-decoration: none;
}
.pagetoc a:hover,
.pagetoc a.active {
background: var(--sidebar-bg);
color: var(--sidebar-fg) !important;
}
.pagetoc .active {
background: var(--sidebar-bg);
color: var(--sidebar-fg);
}
.pagetoc .pagetoc-H2 {
padding-left: 20px;
}
.pagetoc .pagetoc-H3 {
padding-left: 40px;
}
.pagetoc .pagetoc-H4 {
padding-left: 60px;
}
.pagetoc .pagetoc-H5 {
display: none;
}
.pagetoc .pagetoc-H6 {
display: none;
}
}

58
theme/pagetoc.js Normal file
View File

@ -0,0 +1,58 @@
// Un-active everything when you click it
Array.prototype.forEach.call(
document.getElementsByClassName("pagetoc")[0].children,
function (el) {
el.addEventHandler("click", function () {
Array.prototype.forEach.call(
document.getElementsByClassName("pagetoc")[0].children,
function (el) {
el.classList.remove("active");
},
);
el.classList.add("active");
});
},
);
var updateFunction = function () {
var id;
var elements = document.getElementsByClassName("header");
Array.prototype.forEach.call(elements, function (el) {
if (window.pageYOffset >= el.offsetTop) {
id = el;
}
});
Array.prototype.forEach.call(
document.getElementsByClassName("pagetoc")[0].children,
function (el) {
el.classList.remove("active");
},
);
if (!id) return;
Array.prototype.forEach.call(
document.getElementsByClassName("pagetoc")[0].children,
function (el) {
if (id.href.localeCompare(el.href) == 0) {
el.classList.add("active");
}
},
);
};
// Populate sidebar on load
window.addEventListener("load", function () {
var pagetoc = document.getElementsByClassName("pagetoc")[0];
var elements = document.getElementsByClassName("header");
Array.prototype.forEach.call(elements, function (el) {
var link = document.createElement("a");
link.appendChild(document.createTextNode(el.text));
link.href = el.href;
link.classList.add("pagetoc-" + el.parentElement.tagName);
pagetoc.appendChild(link);
});
updateFunction.call();
});
// Handle active elements on scroll
window.addEventListener("scroll", updateFunction);