diff --git a/.github/PULL_REQUEST_TEMPLATE/pull_request_template.md b/.github/pull_request_template.md similarity index 100% rename from .github/PULL_REQUEST_TEMPLATE/pull_request_template.md rename to .github/pull_request_template.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 158d762fc..626ebe230 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,4 +1,4 @@ -name: The Juvix compiler CI +name: Juvix Compiler CI "on": workflow_dispatch: inputs: @@ -148,105 +148,6 @@ jobs: cd main make smoke - docs-linux: - needs: build-and-test-linux - runs-on: ubuntu-20.04 - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - # Grant GITHUB_TOKEN the permissions required to make a Pages deployment - permissions: - pages: write # to deploy to Pages - id-token: write # to verify the deployment originates from an appropriate source - - steps: - - name: Checkout our repository - uses: actions/checkout@v3 - with: - path: main - submodules: recursive - - - name: Install mdbook-pagetoc - uses: baptiste0928/cargo-install@v1 - with: - crate: mdbook-pagetoc - - - name: Install mdbook-katex - uses: baptiste0928/cargo-install@v1 - with: - crate: mdbook-katex - - - name: Install mdbook-linkcheck - uses: baptiste0928/cargo-install@v1 - with: - crate: mdbook-linkcheck - - - name: MDBook setup - uses: peaceiris/actions-mdbook@v1 - with: - mdbook-version: "latest" - - - name: Cache LLVM and Clang - id: cache-llvm - uses: actions/cache@v3 - with: - path: | - C:/Program Files/LLVM - ./llvm - 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 }}" - - - name: Make runtime - run: | - cd main - make runtime - - - name: Stack setup - id: stack - uses: freckle/stack-action@v4 - with: - working-directory: main - test: false - - - name: Generate HTML files from examples - run: | - cd main - echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH - make install - make html-examples - make demo-example - - - name: Build the mdbook - run: | - cd main - make docs - - - name: Setup Pages - uses: actions/configure-pages@v3 - if: >- - github.ref == 'refs/heads/main' || github.event_name == - 'workflow_dispatch' - - - name: Upload artifact - uses: actions/upload-pages-artifact@v1 - if: >- - github.ref == 'refs/heads/main' || github.event_name == - 'workflow_dispatch' - with: - path: main/book/html - - - name: Deploy to GitHub Pages - uses: actions/deploy-pages@v1 - id: deployment - if: >- - github.ref == 'refs/heads/main' || github.event_name == - 'workflow_dispatch' - build-and-test-macos: runs-on: macos-12 steps: diff --git a/Makefile b/Makefile index 046c78a7e..f4a67f491 100644 --- a/Makefile +++ b/Makefile @@ -56,11 +56,7 @@ clean-juvix-build: repl: @${STACK} ghci Juvix:lib ${STACKFLAGS} -# ------------------------------------------------------------------------------ -# -- The Juvix Book -# ------------------------------------------------------------------------------ - -# -- EXAMPLES +# -- EXAMPLES HTML OUTPUT .PHONY: html-examples html-examples: $(EXAMPLES) @@ -76,26 +72,6 @@ demo-example: @mkdir -p ${OUTPUTDIR} @${JUVIXBIN} html $(DEMO_EXAMPLE) --output-dir=$(CURDIR)/${OUTPUTDIR} -# -- MDBook - -.PHONY: docs -docs: html-examples - @cp $(METAFILES) docs/ - @cp -r assets/ docs/ - @mdbook build - -.PHONY: serve-docs -serve-docs: docs - @mdbook serve --open - -cargo-dependencies: - @cargo install mdbook \ - mdbook-katex \ - mdbook-linkcheck \ - mdbook-pagetoc - -# -- Codebase Documentation - .PHONY : haddock haddock : @cabal --docdir=docs/ --htmldir=docs/ haddock --enable-documentation diff --git a/docs/SUMMARY.md b/docs/SUMMARY.md deleted file mode 100644 index f425c6b9a..000000000 --- a/docs/SUMMARY.md +++ /dev/null @@ -1,56 +0,0 @@ -# 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) - - [Project](./reference/language/project.md) - - [Functions](./reference/language/functions.md) - - [Infix operators](./reference/language/infix.md) - - [Data types](./reference/language/datatypes.md) - - [Modules](./reference/language/modules.md) - - [Statements](./reference/language/statement.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) diff --git a/docs/about/community.md b/docs/about/community.md deleted file mode 100644 index 1f78b47bc..000000000 --- a/docs/about/community.md +++ /dev/null @@ -1,8 +0,0 @@ -# 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). diff --git a/docs/about/team.md b/docs/about/team.md deleted file mode 100644 index cae719f0f..000000000 --- a/docs/about/team.md +++ /dev/null @@ -1 +0,0 @@ -# The Juvix Dev Team diff --git a/docs/changelog.md b/docs/changelog.md deleted file mode 100644 index 1903c7698..000000000 --- a/docs/changelog.md +++ /dev/null @@ -1,1547 +0,0 @@ -# Changelog - - -Juvix Mascot - - -## [v0.3.1](https://github.com/anoma/juvix/tree/v0.3.1) (2023-03-31) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.3.0...v0.3.1) - -**Implemented enhancements:** - -- Option `--show-args-num` [\#1946](https://github.com/anoma/juvix/pull/1946) - ([lukaszcz](https://github.com/lukaszcz)) -- Preserve the target type in letrec lifting - [\#1945](https://github.com/anoma/juvix/pull/1945) - ([janmasrovira](https://github.com/janmasrovira)) -- Add syntax highlighting to Core error messages - [\#1938](https://github.com/anoma/juvix/pull/1938) - ([lukaszcz](https://github.com/lukaszcz)) -- Add the `--unroll` option - [\#1935](https://github.com/anoma/juvix/pull/1935) - ([lukaszcz](https://github.com/lukaszcz)) -- Preserve name and location information in Internal-to-Core - [\#1933](https://github.com/anoma/juvix/pull/1933) - ([lukaszcz](https://github.com/lukaszcz)) -- Polymorphic type inference in Core - [\#1931](https://github.com/anoma/juvix/pull/1931) - ([lukaszcz](https://github.com/lukaszcz)) -- Update README.md with Juvix nightly builds badge - [\#1923](https://github.com/anoma/juvix/pull/1923) - ([jonaprieto](https://github.com/jonaprieto)) -- Create clean-up-cache.yaml - [\#1915](https://github.com/anoma/juvix/pull/1915) - ([jonaprieto](https://github.com/jonaprieto)) -- Update GitHub pages deployment using deploy-pages action - [\#1910](https://github.com/anoma/juvix/pull/1910) - ([jonaprieto](https://github.com/jonaprieto)) -- Check for recursive inductive types in the GEB pipeline - [\#1909](https://github.com/anoma/juvix/pull/1909) - ([lukaszcz](https://github.com/lukaszcz)) -- CI pre-commit maintenance - [\#1905](https://github.com/anoma/juvix/pull/1905) - ([jonaprieto](https://github.com/jonaprieto)) -- Add new README and md files - [\#1904](https://github.com/anoma/juvix/pull/1904) - ([jonaprieto](https://github.com/jonaprieto)) -- Print JuvixCore correctly - [\#1875](https://github.com/anoma/juvix/pull/1875) - ([lukaszcz](https://github.com/lukaszcz)) -- Pattern matching compilation - [\#1874](https://github.com/anoma/juvix/pull/1874) - ([lukaszcz](https://github.com/lukaszcz)) -- CI Haskell maintenance - [\#1797](https://github.com/anoma/juvix/pull/1797) - ([jonaprieto](https://github.com/jonaprieto)) - -**Merged pull requests:** - -- Let-folding after lifting - [\#1955](https://github.com/anoma/juvix/pull/1955) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix removal of polymorphic type arguments - [\#1954](https://github.com/anoma/juvix/pull/1954) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix a bug in closure traversal - [\#1953](https://github.com/anoma/juvix/pull/1953) - ([lukaszcz](https://github.com/lukaszcz)) -- Update typecheck command to check for coverage - [\#1952](https://github.com/anoma/juvix/pull/1952) - ([janmasrovira](https://github.com/janmasrovira)) -- CI: Ignore errors linux typecheck / format examples step - [\#1950](https://github.com/anoma/juvix/pull/1950) - ([paulcadman](https://github.com/paulcadman)) -- Filter out type synonyms in RemoveTypeArgs - [\#1949](https://github.com/anoma/juvix/pull/1949) - ([lukaszcz](https://github.com/lukaszcz)) -- Add fail nodes to Geb - [\#1947](https://github.com/anoma/juvix/pull/1947) - ([lukaszcz](https://github.com/lukaszcz)) -- End-to-end Geb compilation tests - [\#1942](https://github.com/anoma/juvix/pull/1942) - ([lukaszcz](https://github.com/lukaszcz)) -- Add juvix dev repl command - [\#1941](https://github.com/anoma/juvix/pull/1941) - ([paulcadman](https://github.com/paulcadman)) -- Refactor Geb values - [\#1940](https://github.com/anoma/juvix/pull/1940) - ([lukaszcz](https://github.com/lukaszcz)) -- Avoid capturing the same free variable multiple times in letrec lifting - [\#1939](https://github.com/anoma/juvix/pull/1939) - ([janmasrovira](https://github.com/janmasrovira)) -- Add Judoc syntax reference - [\#1934](https://github.com/anoma/juvix/pull/1934) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix spacing of judoc in the formatter - [\#1932](https://github.com/anoma/juvix/pull/1932) - ([janmasrovira](https://github.com/janmasrovira)) -- bench: Fix juvix compile flag for wasm - [\#1925](https://github.com/anoma/juvix/pull/1925) - ([paulcadman](https://github.com/paulcadman)) -- Fix memory count for string operations - [\#1924](https://github.com/anoma/juvix/pull/1924) - ([lukaszcz](https://github.com/lukaszcz)) -- Let folding - [\#1921](https://github.com/anoma/juvix/pull/1921) - ([lukaszcz](https://github.com/lukaszcz)) -- Add a test suite for milestone examples - [\#1920](https://github.com/anoma/juvix/pull/1920) - ([paulcadman](https://github.com/paulcadman)) -- Add --numeric-version flag - [\#1918](https://github.com/anoma/juvix/pull/1918) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix bug with unregistered builtin bool - [\#1917](https://github.com/anoma/juvix/pull/1917) - ([lukaszcz](https://github.com/lukaszcz)) -- Recursion unrolling for functions - [\#1912](https://github.com/anoma/juvix/pull/1912) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix REPL state to include enough information to rerun the pipeline - [\#1911](https://github.com/anoma/juvix/pull/1911) - ([janmasrovira](https://github.com/janmasrovira)) -- CI Haskell fix for macOS build - [\#1908](https://github.com/anoma/juvix/pull/1908) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix bug in IO runtime - [\#1906](https://github.com/anoma/juvix/pull/1906) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix JuvixAsm validation - [\#1903](https://github.com/anoma/juvix/pull/1903) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix registration of builtin inductive axioms - [\#1901](https://github.com/anoma/juvix/pull/1901) - ([paulcadman](https://github.com/paulcadman)) -- internal-to-core: Fix index shifting of pattern arguments - [\#1900](https://github.com/anoma/juvix/pull/1900) - ([paulcadman](https://github.com/paulcadman)) -- Fix de Bruijn indices in rmap - [\#1898](https://github.com/anoma/juvix/pull/1898) - ([lukaszcz](https://github.com/lukaszcz)) -- Normalize types in repl - [\#1897](https://github.com/anoma/juvix/pull/1897) - ([janmasrovira](https://github.com/janmasrovira)) -- Add MidSquareHash.juvix and fix types in MidSquareHash.jvc - [\#1896](https://github.com/anoma/juvix/pull/1896) - ([lukaszcz](https://github.com/lukaszcz)) -- Automatically detect and split mutually recursive blocks in let expressions - [\#1894](https://github.com/anoma/juvix/pull/1894) - ([janmasrovira](https://github.com/janmasrovira)) -- The `rmap` recursor - [\#1893](https://github.com/anoma/juvix/pull/1893) - ([lukaszcz](https://github.com/lukaszcz)) -- Add `juvix format` command - [\#1886](https://github.com/anoma/juvix/pull/1886) - ([paulcadman](https://github.com/paulcadman)) -- Make keyword `end` optional for top modules - [\#1883](https://github.com/anoma/juvix/pull/1883) - ([janmasrovira](https://github.com/janmasrovira)) -- Add errors to the Core pipeline and check GEB prerequisites - [\#1871](https://github.com/anoma/juvix/pull/1871) - ([lukaszcz](https://github.com/lukaszcz)) -- Test core to geb translation - [\#1865](https://github.com/anoma/juvix/pull/1865) - ([jonaprieto](https://github.com/jonaprieto)) - -## [v0.3.0](https://github.com/anoma/juvix/tree/v0.3.0) (2023-03-15) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.9...v0.3.0) - -**Implemented enhancements:** - -- Avoid line breaks in applications within a type signature - [#1850](https://github.com/anoma/juvix/issues/1850) - ([paulcadman](https://github.com/paulcadman)) -- Respect user's spacing decisions in the formatter - [#1837](https://github.com/anoma/juvix/issues/1837) - ([janmasrovira](https://github.com/janmasrovira)) -- Formatter should not transform ASCII symbols to unicode by default - [#1827](https://github.com/anoma/juvix/issues/1827) - ([janmasrovira](https://github.com/janmasrovira)) -- Enable match-to-case, nat-to-int and convert-builtins by default in - REPL [#1825](https://github.com/anoma/juvix/issues/1825) - ([lukaszcz](https://github.com/lukaszcz)) -- The Juvix formatter works poorly with multi-line ifs - [#1793](https://github.com/anoma/juvix/issues/1793) - ([janmasrovira](https://github.com/janmasrovira)) -- Add a lazy IO sequencing function (#1772) - [#1773](https://github.com/anoma/juvix/issues/1773) - ([lukaszcz](https://github.com/lukaszcz)) -- Support LetRec in the GEB backend - [#1756](https://github.com/anoma/juvix/issues/1756) - ([janmasrovira](https://github.com/janmasrovira)) -- Support integers in the GEB backend - [#1753](https://github.com/anoma/juvix/issues/1753) - ([lukaszcz](https://github.com/lukaszcz)) -- GEB evaluator [#1751](https://github.com/anoma/juvix/issues/1751) - ([jonaprieto](https://github.com/jonaprieto)) -- Add debugging builtin functions - [#1731](https://github.com/anoma/juvix/issues/1731) - ([jonaprieto](https://github.com/jonaprieto)) -- Non-judoc comments are removed when generating HTML output - [#1723](https://github.com/anoma/juvix/issues/1723) - ([janmasrovira](https://github.com/janmasrovira)) -- Special syntax for `case` - [#1716](https://github.com/anoma/juvix/issues/1716) - ([janmasrovira](https://github.com/janmasrovira)) -- Make \|\| and && lazy - [#1701](https://github.com/anoma/juvix/issues/1701) - ([lukaszcz](https://github.com/lukaszcz)) -- It should be possible to specify multiple implicit type arguments at - once [#1692](https://github.com/anoma/juvix/issues/1692) - ([janmasrovira](https://github.com/janmasrovira)) -- Naive compilation of complex pattern matches with match-expressions - to decision trees with case-expressions - [#1531](https://github.com/anoma/juvix/issues/1531) - ([paulcadman](https://github.com/paulcadman)) -- New compilation pipeline - [#1832](https://github.com/anoma/juvix/pull/1832) - ([lukaszcz](https://github.com/lukaszcz)) -- Add internal core-eval option to evaluate named function identifier - [#1819](https://github.com/anoma/juvix/pull/1819) - ([paulcadman](https://github.com/paulcadman)) -- Short syntax for sequences of function and datatype parameters - [#1809](https://github.com/anoma/juvix/pull/1809) - ([lukaszcz](https://github.com/lukaszcz)) -- Add Geb Backend Evaluator with some extra subcommands - [#1808](https://github.com/anoma/juvix/pull/1808) - ([jonaprieto](https://github.com/jonaprieto)) -- Add REPL option to apply Core transformations - [#1796](https://github.com/anoma/juvix/pull/1796) - ([paulcadman](https://github.com/paulcadman)) -- String builtins [#1784](https://github.com/anoma/juvix/pull/1784) - ([lukaszcz](https://github.com/lukaszcz)) -- Use restore/save github action to speed up the CI testing - [#1783](https://github.com/anoma/juvix/pull/1783) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix minor issue with ==% for type equality - [#1780](https://github.com/anoma/juvix/pull/1780) - ([jonaprieto](https://github.com/jonaprieto)) -- Add debugging builtin functions `trace` and `fail` - [#1771](https://github.com/anoma/juvix/pull/1771) - ([jonaprieto](https://github.com/jonaprieto)) -- Keep regular comments in html output - [#1766](https://github.com/anoma/juvix/pull/1766) - ([janmasrovira](https://github.com/janmasrovira)) -- Lazy boolean operators - [#1743](https://github.com/anoma/juvix/pull/1743) - ([lukaszcz](https://github.com/lukaszcz)) -- Refactor `html` command with extra options - [#1725](https://github.com/anoma/juvix/pull/1725) - ([jonaprieto](https://github.com/jonaprieto)) -- Add initial setup for codespaces - [#1713](https://github.com/anoma/juvix/pull/1713) - ([jonaprieto](https://github.com/jonaprieto)) -- Typecheck let expressions - [#1712](https://github.com/anoma/juvix/pull/1712) - ([janmasrovira](https://github.com/janmasrovira)) -- Use Smoke instead of shelltestrunner - [#1710](https://github.com/anoma/juvix/pull/1710) - ([jonaprieto](https://github.com/jonaprieto)) -- Replace –output-dir flag by –internal-build-dir - [#1707](https://github.com/anoma/juvix/pull/1707) - ([jonaprieto](https://github.com/jonaprieto)) -- Compiler output [#1705](https://github.com/anoma/juvix/pull/1705) - ([jonaprieto](https://github.com/jonaprieto)) -- Allow optional pipe before the first constructor for inductive type - declarations [#1699](https://github.com/anoma/juvix/pull/1699) - ([jonaprieto](https://github.com/jonaprieto)) -- Nat builtins [#1686](https://github.com/anoma/juvix/pull/1686) - ([lukaszcz](https://github.com/lukaszcz)) - -**Merged pull requests:** - -- Remove dead code in `Internal` - [#1891](https://github.com/anoma/juvix/pull/1891) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove missing Juvix examples and webapp example from docs build - [#1890](https://github.com/anoma/juvix/pull/1890) - ([paulcadman](https://github.com/paulcadman)) -- Fix type synonym in let - [#1880](https://github.com/anoma/juvix/pull/1880) - ([janmasrovira](https://github.com/janmasrovira)) -- Update stack resolver to lts-20.12 - [#1873](https://github.com/anoma/juvix/pull/1873) - ([paulcadman](https://github.com/paulcadman)) -- Use Ape to format patterns - [#1870](https://github.com/anoma/juvix/pull/1870) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix Core-To-Geb translation - [#1863](https://github.com/anoma/juvix/pull/1863) - ([jonaprieto](https://github.com/jonaprieto)) -- Remove the old C backend - [#1862](https://github.com/anoma/juvix/pull/1862) - ([lukaszcz](https://github.com/lukaszcz)) -- Move `substEnv` to its own module - [#1861](https://github.com/anoma/juvix/pull/1861) - ([janmasrovira](https://github.com/janmasrovira)) -- Add `_caseTypeWholeExpression` to Internal - [#1860](https://github.com/anoma/juvix/pull/1860) - ([janmasrovira](https://github.com/janmasrovira)) -- remove old minihaskell files - [#1859](https://github.com/anoma/juvix/pull/1859) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix bugs in the Case translation in Core-to-Geb - [#1858](https://github.com/anoma/juvix/pull/1858) - ([lukaszcz](https://github.com/lukaszcz)) -- Format examples [#1856](https://github.com/anoma/juvix/pull/1856) - ([janmasrovira](https://github.com/janmasrovira)) -- Sort the identifiers topologically in the Core-to-GEB translation - [#1854](https://github.com/anoma/juvix/pull/1854) - ([lukaszcz](https://github.com/lukaszcz)) -- Add type info to the mid-square hashing function - [#1853](https://github.com/anoma/juvix/pull/1853) - ([lukaszcz](https://github.com/lukaszcz)) -- Use APE mechanism to format Function expressions - [#1852](https://github.com/anoma/juvix/pull/1852) - ([paulcadman](https://github.com/paulcadman)) -- Preserve single wildcards pretty printing function parameters - [#1851](https://github.com/anoma/juvix/pull/1851) - ([paulcadman](https://github.com/paulcadman)) -- Add type annotation to case expression - [#1849](https://github.com/anoma/juvix/pull/1849) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove module parameters - [#1848](https://github.com/anoma/juvix/pull/1848) - ([janmasrovira](https://github.com/janmasrovira)) -- Allow shadowing local variables with let function definitions - [#1847](https://github.com/anoma/juvix/pull/1847) - ([janmasrovira](https://github.com/janmasrovira)) -- Add lambda type info - [#1845](https://github.com/anoma/juvix/pull/1845) - ([janmasrovira](https://github.com/janmasrovira)) -- Improve comma formatting - [#1842](https://github.com/anoma/juvix/pull/1842) - ([janmasrovira](https://github.com/janmasrovira)) -- Improve formatter [#1840](https://github.com/anoma/juvix/pull/1840) - ([janmasrovira](https://github.com/janmasrovira)) -- Respect lambda Ascii/Unicode - [#1838](https://github.com/anoma/juvix/pull/1838) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix `juvix init` [#1835](https://github.com/anoma/juvix/pull/1835) - ([janmasrovira](https://github.com/janmasrovira)) -- The formatter respects the ascii function arrow - [#1834](https://github.com/anoma/juvix/pull/1834) - ([janmasrovira](https://github.com/janmasrovira)) -- Add `dev core from-concrete` command - [#1833](https://github.com/anoma/juvix/pull/1833) - ([janmasrovira](https://github.com/janmasrovira)) -- Give proper errors for incorrect application of lazy builtins - [#1830](https://github.com/anoma/juvix/pull/1830) - ([lukaszcz](https://github.com/lukaszcz)) -- Documentation: update language reference - [#1829](https://github.com/anoma/juvix/pull/1829) - ([lukaszcz](https://github.com/lukaszcz)) -- Add compilation of complex pattern matching to case - [#1824](https://github.com/anoma/juvix/pull/1824) - ([paulcadman](https://github.com/paulcadman)) -- Apply CI ghcup workaround to docs build - [#1823](https://github.com/anoma/juvix/pull/1823) - ([paulcadman](https://github.com/paulcadman)) -- Update the Juvix tutorial for 0.3 - [#1822](https://github.com/anoma/juvix/pull/1822) - ([lukaszcz](https://github.com/lukaszcz)) -- Workaround ghcup issue on CI runner - [#1821](https://github.com/anoma/juvix/pull/1821) - ([paulcadman](https://github.com/paulcadman)) -- Respect the `juvix dev highlight --format` flag when outputting - errors [#1820](https://github.com/anoma/juvix/pull/1820) - ([janmasrovira](https://github.com/janmasrovira)) -- Comments about the usage of the JuvixCore recursors - [#1818](https://github.com/anoma/juvix/pull/1818) - ([lukaszcz](https://github.com/lukaszcz)) -- Emacs mode and VSCode extension tutorials - [#1815](https://github.com/anoma/juvix/pull/1815) - ([lukaszcz](https://github.com/lukaszcz)) -- Documentation: how to compile Juvix programs - [#1813](https://github.com/anoma/juvix/pull/1813) - ([lukaszcz](https://github.com/lukaszcz)) -- Make '\>\>' lazy [#1812](https://github.com/anoma/juvix/pull/1812) - ([lukaszcz](https://github.com/lukaszcz)) -- Output proper GEB Lisp programs - [#1810](https://github.com/anoma/juvix/pull/1810) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove the usage annotation syntax - [#1805](https://github.com/anoma/juvix/pull/1805) - ([lukaszcz](https://github.com/lukaszcz)) -- Mid-square hashing implemented in JuvixCore - [#1804](https://github.com/anoma/juvix/pull/1804) - ([lukaszcz](https://github.com/lukaszcz)) -- Autocompletion for `dev core compilation --target` - [#1803](https://github.com/anoma/juvix/pull/1803) - ([janmasrovira](https://github.com/janmasrovira)) -- Special syntax for case - [#1800](https://github.com/anoma/juvix/pull/1800) - ([janmasrovira](https://github.com/janmasrovira)) -- Adapt benchmarks to the new pipeline - [#1795](https://github.com/anoma/juvix/pull/1795) - ([lukaszcz](https://github.com/lukaszcz)) -- Support letrec lifting without lambda lifting - [#1794](https://github.com/anoma/juvix/pull/1794) - ([janmasrovira](https://github.com/janmasrovira)) -- Use the reader effect - [#1791](https://github.com/anoma/juvix/pull/1791) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove braces from let expressions - [#1790](https://github.com/anoma/juvix/pull/1790) - ([janmasrovira](https://github.com/janmasrovira)) -- Translate as-pattern binders to Core PatternBinders - [#1789](https://github.com/anoma/juvix/pull/1789) - ([paulcadman](https://github.com/paulcadman)) -- Fix termination with as-patterns - [#1787](https://github.com/anoma/juvix/pull/1787) - ([janmasrovira](https://github.com/janmasrovira)) -- Allow type signatures to have a body - [#1785](https://github.com/anoma/juvix/pull/1785) - ([janmasrovira](https://github.com/janmasrovira)) -- Track builtins in the Core InfoTable - [#1782](https://github.com/anoma/juvix/pull/1782) - ([paulcadman](https://github.com/paulcadman)) -- Pipes for lambda clauses - [#1781](https://github.com/anoma/juvix/pull/1781) - ([janmasrovira](https://github.com/janmasrovira)) -- Support integers in the GEB backend - [#1778](https://github.com/anoma/juvix/pull/1778) - ([lukaszcz](https://github.com/lukaszcz)) -- Add builtin nat and bool types as start nodes in reachability - analysis [#1775](https://github.com/anoma/juvix/pull/1775) - ([paulcadman](https://github.com/paulcadman)) -- Update pre-commit [#1772](https://github.com/anoma/juvix/pull/1772) - ([jonaprieto](https://github.com/jonaprieto)) -- Parse JuvixCore with absolute paths - [#1770](https://github.com/anoma/juvix/pull/1770) - ([paulcadman](https://github.com/paulcadman)) -- Use absolute path in Core Evaluator to generate source file location - [#1769](https://github.com/anoma/juvix/pull/1769) - ([paulcadman](https://github.com/paulcadman)) -- Install wasmer binary from Github releases - [#1765](https://github.com/anoma/juvix/pull/1765) - ([jonaprieto](https://github.com/jonaprieto)) -- Run the new Juvix formatter for all the Juvix examples - [#1764](https://github.com/anoma/juvix/pull/1764) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix let expressions in the repl - [#1763](https://github.com/anoma/juvix/pull/1763) - ([janmasrovira](https://github.com/janmasrovira)) -- Improve arity inference for repl expressions - [#1762](https://github.com/anoma/juvix/pull/1762) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix broken links and other improvements - [#1761](https://github.com/anoma/juvix/pull/1761) - ([jonaprieto](https://github.com/jonaprieto)) -- Translate Nat builtins to the correct Core Ops - [#1760](https://github.com/anoma/juvix/pull/1760) - ([paulcadman](https://github.com/paulcadman)) -- Remove hlint from the CI and pre-commit config - [#1759](https://github.com/anoma/juvix/pull/1759) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix demo example build - [#1757](https://github.com/anoma/juvix/pull/1757) - ([paulcadman](https://github.com/paulcadman)) -- Basic Geb integration - [#1748](https://github.com/anoma/juvix/pull/1748) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix macOS CI build [#1747](https://github.com/anoma/juvix/pull/1747) - ([paulcadman](https://github.com/paulcadman)) -- Adapt Juvix programs to the new pipeline - [#1746](https://github.com/anoma/juvix/pull/1746) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix link in README for the new docs - [#1745](https://github.com/anoma/juvix/pull/1745) - ([lukaszcz](https://github.com/lukaszcz)) -- Move juvix-mode to a separate repository - [#1744](https://github.com/anoma/juvix/pull/1744) - ([jonaprieto](https://github.com/jonaprieto)) -- Print comments when pretty printing concrete syntax - [#1737](https://github.com/anoma/juvix/pull/1737) - ([janmasrovira](https://github.com/janmasrovira)) -- Demo [#1736](https://github.com/anoma/juvix/pull/1736) - ([lukaszcz](https://github.com/lukaszcz)) -- Update CI to install Smoke, Github actions, and Makefile fixes - [#1735](https://github.com/anoma/juvix/pull/1735) - ([jonaprieto](https://github.com/jonaprieto)) -- Update stack.yaml [#1734](https://github.com/anoma/juvix/pull/1734) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix Nat builtins [#1733](https://github.com/anoma/juvix/pull/1733) - ([lukaszcz](https://github.com/lukaszcz)) -- Script to count LOC - [#1732](https://github.com/anoma/juvix/pull/1732) - ([lukaszcz](https://github.com/lukaszcz)) -- Give a proper type to literal Strings - [#1730](https://github.com/anoma/juvix/pull/1730) - ([paulcadman](https://github.com/paulcadman)) -- Do not filter implicit args in internal to core translation - [#1728](https://github.com/anoma/juvix/pull/1728) - ([paulcadman](https://github.com/paulcadman)) -- Fix de Brujin indexing of lambda arguments - [#1727](https://github.com/anoma/juvix/pull/1727) - ([paulcadman](https://github.com/paulcadman)) -- Fix inference loop [#1726](https://github.com/anoma/juvix/pull/1726) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove wildcard patterns from Internal - [#1724](https://github.com/anoma/juvix/pull/1724) - ([janmasrovira](https://github.com/janmasrovira)) -- Restructure the documentation and add a tutorial - [#1718](https://github.com/anoma/juvix/pull/1718) - ([lukaszcz](https://github.com/lukaszcz)) -- Improve error message for confusing ':=' with '=' - [#1715](https://github.com/anoma/juvix/pull/1715) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix #1704 [#1711](https://github.com/anoma/juvix/pull/1711) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix #1693 [#1708](https://github.com/anoma/juvix/pull/1708) - ([janmasrovira](https://github.com/janmasrovira)) -- Tests for the new compilation pipeline - [#1703](https://github.com/anoma/juvix/pull/1703) - ([lukaszcz](https://github.com/lukaszcz)) -- Add printString and printBool support to legacy C backend - [#1698](https://github.com/anoma/juvix/pull/1698) - ([paulcadman](https://github.com/paulcadman)) -- Add –show-de-bruijn option to `juvix repl` - [#1694](https://github.com/anoma/juvix/pull/1694) - ([lukaszcz](https://github.com/lukaszcz)) -- Allow 'terminating' keyword with builtins - [#1688](https://github.com/anoma/juvix/pull/1688) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove unicode cons symbol - [#1687](https://github.com/anoma/juvix/pull/1687) - ([lukaszcz](https://github.com/lukaszcz)) -- Change syntax for ind. data types and forbid the empty data type - [#1684](https://github.com/anoma/juvix/pull/1684) - ([jonaprieto](https://github.com/jonaprieto)) -- Convert Nat literals to Core integers - [#1681](https://github.com/anoma/juvix/pull/1681) - ([lukaszcz](https://github.com/lukaszcz)) -- Less verbose output from running `make check` - [#1675](https://github.com/anoma/juvix/pull/1675) - ([jonaprieto](https://github.com/jonaprieto)) -- Remove where syntax - [#1674](https://github.com/anoma/juvix/pull/1674) - ([jonaprieto](https://github.com/jonaprieto)) -- Benchmarks [#1673](https://github.com/anoma/juvix/pull/1673) - ([janmasrovira](https://github.com/janmasrovira)) -- JuvixCore to JuvixAsm translation - [#1665](https://github.com/anoma/juvix/pull/1665) - ([lukaszcz](https://github.com/lukaszcz)) - -## [v0.2.9](https://github.com/anoma/juvix/tree/v0.2.9) (2023-01-18) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.8...v0.2.9) - -**Implemented enhancements:** - -- Refactor `html` command with extra options - [#1725](https://github.com/anoma/juvix/pull/1725) - ([jonaprieto](https://github.com/jonaprieto)) -- Add initial setup for codespaces - [#1713](https://github.com/anoma/juvix/pull/1713) - ([jonaprieto](https://github.com/jonaprieto)) -- Typecheck let expressions - [#1712](https://github.com/anoma/juvix/pull/1712) - ([janmasrovira](https://github.com/janmasrovira)) -- Use Smoke instead of shelltestrunner - [#1710](https://github.com/anoma/juvix/pull/1710) - ([jonaprieto](https://github.com/jonaprieto)) -- Replace –output-dir flag by –internal-build-dir - [#1707](https://github.com/anoma/juvix/pull/1707) - ([jonaprieto](https://github.com/jonaprieto)) -- Compiler output [#1705](https://github.com/anoma/juvix/pull/1705) - ([jonaprieto](https://github.com/jonaprieto)) -- Allow optional pipe before the first constructor for inductive type - declarations [#1699](https://github.com/anoma/juvix/pull/1699) - ([jonaprieto](https://github.com/jonaprieto)) -- Nat builtins [#1686](https://github.com/anoma/juvix/pull/1686) - ([lukaszcz](https://github.com/lukaszcz)) - -**Merged pull requests:** - -- Demo [#1736](https://github.com/anoma/juvix/pull/1736) - ([lukaszcz](https://github.com/lukaszcz)) -- Update stack.yaml [#1734](https://github.com/anoma/juvix/pull/1734) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix Nat builtins [#1733](https://github.com/anoma/juvix/pull/1733) - ([lukaszcz](https://github.com/lukaszcz)) -- Script to count LOC - [#1732](https://github.com/anoma/juvix/pull/1732) - ([lukaszcz](https://github.com/lukaszcz)) -- Give a proper type to literal Strings - [#1730](https://github.com/anoma/juvix/pull/1730) - ([paulcadman](https://github.com/paulcadman)) -- Do not filter implicit args in internal to core translation - [#1728](https://github.com/anoma/juvix/pull/1728) - ([paulcadman](https://github.com/paulcadman)) -- Fix de Brujin indexing of lambda arguments - [#1727](https://github.com/anoma/juvix/pull/1727) - ([paulcadman](https://github.com/paulcadman)) -- Fix inference loop [#1726](https://github.com/anoma/juvix/pull/1726) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove wildcard patterns from Internal - [#1724](https://github.com/anoma/juvix/pull/1724) - ([janmasrovira](https://github.com/janmasrovira)) -- Restructure the documentation and add a tutorial - [#1718](https://github.com/anoma/juvix/pull/1718) - ([lukaszcz](https://github.com/lukaszcz)) -- Improve error message for confusing ':=' with '=' - [#1715](https://github.com/anoma/juvix/pull/1715) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix #1704 [#1711](https://github.com/anoma/juvix/pull/1711) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix #1693 [#1708](https://github.com/anoma/juvix/pull/1708) - ([janmasrovira](https://github.com/janmasrovira)) -- Tests for the new compilation pipeline - [#1703](https://github.com/anoma/juvix/pull/1703) - ([lukaszcz](https://github.com/lukaszcz)) -- Add printString and printBool support to legacy C backend - [#1698](https://github.com/anoma/juvix/pull/1698) - ([paulcadman](https://github.com/paulcadman)) -- Add –show-de-bruijn option to `juvix repl` - [#1694](https://github.com/anoma/juvix/pull/1694) - ([lukaszcz](https://github.com/lukaszcz)) -- Allow 'terminating' keyword with builtins - [#1688](https://github.com/anoma/juvix/pull/1688) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove unicode cons symbol - [#1687](https://github.com/anoma/juvix/pull/1687) - ([lukaszcz](https://github.com/lukaszcz)) -- Change syntax for ind. data types and forbid the empty data type - [#1684](https://github.com/anoma/juvix/pull/1684) - ([jonaprieto](https://github.com/jonaprieto)) -- Convert Nat literals to Core integers - [#1681](https://github.com/anoma/juvix/pull/1681) - ([lukaszcz](https://github.com/lukaszcz)) -- Less verbose output from running `make check` - [#1675](https://github.com/anoma/juvix/pull/1675) - ([jonaprieto](https://github.com/jonaprieto)) -- Remove where syntax - [#1674](https://github.com/anoma/juvix/pull/1674) - ([jonaprieto](https://github.com/jonaprieto)) -- Benchmarks [#1673](https://github.com/anoma/juvix/pull/1673) - ([janmasrovira](https://github.com/janmasrovira)) -- JuvixCore to JuvixAsm translation - [#1665](https://github.com/anoma/juvix/pull/1665) - ([lukaszcz](https://github.com/lukaszcz)) - -## [v0.2.8](https://github.com/anoma/juvix/tree/v0.2.8) (2022-12-20) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.7...v0.2.8) - -**Implemented enhancements:** - -- Support basic dependencies - [#1622](https://github.com/anoma/juvix/pull/1622) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- Refactor hie.yaml and add entry in the readme - [#1672](https://github.com/anoma/juvix/pull/1672) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix inline monospace formatted text in README - [#1671](https://github.com/anoma/juvix/pull/1671) - ([paulcadman](https://github.com/paulcadman)) -- Pin mdbook to version 0.4.22 in docs build - [#1670](https://github.com/anoma/juvix/pull/1670) - ([paulcadman](https://github.com/paulcadman)) -- Add option to specify Core transformations to - `dev internal core-eval` - [#1669](https://github.com/anoma/juvix/pull/1669) - ([paulcadman](https://github.com/paulcadman)) -- Revert "Ignore binaries generated by running some tests" - [#1668](https://github.com/anoma/juvix/pull/1668) - ([jonaprieto](https://github.com/jonaprieto)) -- Add configuration files so the project can be built with cabal - [#1667](https://github.com/anoma/juvix/pull/1667) - ([paulcadman](https://github.com/paulcadman)) -- Add documentation for compiling/running the TicTacToe example - [#1664](https://github.com/anoma/juvix/pull/1664) - ([paulcadman](https://github.com/paulcadman)) -- Ignore binaries generated by running some tests - [#1663](https://github.com/anoma/juvix/pull/1663) - ([jonaprieto](https://github.com/jonaprieto)) -- Conversion of Nat representation to JuvixCore integers - [#1661](https://github.com/anoma/juvix/pull/1661) - ([lukaszcz](https://github.com/lukaszcz)) -- Move applications inside Lets and Cases - [#1659](https://github.com/anoma/juvix/pull/1659) - ([lukaszcz](https://github.com/lukaszcz)) -- Run shelltests on macOS build - [#1658](https://github.com/anoma/juvix/pull/1658) - ([paulcadman](https://github.com/paulcadman)) -- Restore macOS CI build/test - [#1657](https://github.com/anoma/juvix/pull/1657) - ([paulcadman](https://github.com/paulcadman)) -- Remove type arguments and type abstractions from Nodes - [#1655](https://github.com/anoma/juvix/pull/1655) - ([lukaszcz](https://github.com/lukaszcz)) -- Pretty printing of JuvixAsm code - [#1650](https://github.com/anoma/juvix/pull/1650) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove NameId from Core - [#1649](https://github.com/anoma/juvix/pull/1649) - ([lukaszcz](https://github.com/lukaszcz)) -- Translation from JuvixAsm to C - [#1619](https://github.com/anoma/juvix/pull/1619) - ([lukaszcz](https://github.com/lukaszcz)) - -## [v0.2.7](https://github.com/anoma/juvix/tree/v0.2.7) (2022-12-05) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.6...v0.2.7) - -**Implemented enhancements:** - -- Add juvix-repl-mode for emacs - [#1612](https://github.com/anoma/juvix/pull/1612) - ([paulcadman](https://github.com/paulcadman)) -- Make lambda lifting correct when free variables occur in the types - of binders [#1609](https://github.com/anoma/juvix/pull/1609) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- Files pure refactor - [#1652](https://github.com/anoma/juvix/pull/1652) - ([janmasrovira](https://github.com/janmasrovira)) -- Use the same stack version in all CI jobs and remove `stack setup` - step [#1651](https://github.com/anoma/juvix/pull/1651) - ([paulcadman](https://github.com/paulcadman)) -- Fix 'not a primitive type' error message - [#1648](https://github.com/anoma/juvix/pull/1648) - ([lukaszcz](https://github.com/lukaszcz)) -- Upgrade stack snapshot to use ghc-9.2.5 - [#1621](https://github.com/anoma/juvix/pull/1621) - ([janmasrovira](https://github.com/janmasrovira)) -- Add an emacs function to restart the REPL - [#1618](https://github.com/anoma/juvix/pull/1618) - ([paulcadman](https://github.com/paulcadman)) -- Add types to Core functions and constructors when translating from - Internal [#1617](https://github.com/anoma/juvix/pull/1617) - ([paulcadman](https://github.com/paulcadman)) -- Auto complete argument of 'dev core read -t' - [#1616](https://github.com/anoma/juvix/pull/1616) - ([janmasrovira](https://github.com/janmasrovira)) -- Compute new entrypoint root when loading a file in the REPL - [#1615](https://github.com/anoma/juvix/pull/1615) - ([paulcadman](https://github.com/paulcadman)) -- Compute maximum runtime stack height in JuvixReg - [#1613](https://github.com/anoma/juvix/pull/1613) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove shelltest threading - [#1611](https://github.com/anoma/juvix/pull/1611) - ([paulcadman](https://github.com/paulcadman)) -- Use StackInfo and recurseS in the JuvixAsm to JuvixReg translation. - [#1610](https://github.com/anoma/juvix/pull/1610) - ([lukaszcz](https://github.com/lukaszcz)) -- Precompute maximum heap allocation - [#1608](https://github.com/anoma/juvix/pull/1608) - ([lukaszcz](https://github.com/lukaszcz)) -- Improvements to Juvix REPL - [#1607](https://github.com/anoma/juvix/pull/1607) - ([paulcadman](https://github.com/paulcadman)) -- Fix discrepancy between Juvix and WASM pages - [#1605](https://github.com/anoma/juvix/pull/1605) - ([lukaszcz](https://github.com/lukaszcz)) -- Compute JuvixAsm stack usage info - [#1604](https://github.com/anoma/juvix/pull/1604) - ([lukaszcz](https://github.com/lukaszcz)) -- Improve As-Pattern parsing - [#1603](https://github.com/anoma/juvix/pull/1603) - ([ii8](https://github.com/ii8)) -- Juvix core recursors should descend into nodes stored in infos - [#1600](https://github.com/anoma/juvix/pull/1600) - ([janmasrovira](https://github.com/janmasrovira)) -- Add docs for installing the linux binary - [#1599](https://github.com/anoma/juvix/pull/1599) - ([paulcadman](https://github.com/paulcadman)) -- Binder refactor [#1598](https://github.com/anoma/juvix/pull/1598) - ([janmasrovira](https://github.com/janmasrovira)) -- Juvix C runtime [#1580](https://github.com/anoma/juvix/pull/1580) - ([lukaszcz](https://github.com/lukaszcz)) -- As-patterns [#1576](https://github.com/anoma/juvix/pull/1576) - ([ii8](https://github.com/ii8)) -- Eta expansion at the top of each core function definition (#1481) - [#1571](https://github.com/anoma/juvix/pull/1571) - ([janmasrovira](https://github.com/janmasrovira)) -- Add translation from Internal to Core - [#1567](https://github.com/anoma/juvix/pull/1567) - ([paulcadman](https://github.com/paulcadman)) - -## [v0.2.6](https://github.com/anoma/juvix/tree/v0.2.6) (2022-10-26) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.5...v0.2.6) - -**Implemented enhancements:** - -- Support go to definition for the standard library - [#1592](https://github.com/anoma/juvix/pull/1592) - ([paulcadman](https://github.com/paulcadman)) -- Add builtin if [#1585](https://github.com/anoma/juvix/pull/1585) - ([paulcadman](https://github.com/paulcadman)) -- Add builtin boolean - [#1582](https://github.com/anoma/juvix/pull/1582) - ([paulcadman](https://github.com/paulcadman)) -- Add lambda expressions to internal and add typechecking support - [#1538](https://github.com/anoma/juvix/pull/1538) - ([janmasrovira](https://github.com/janmasrovira)) - -**Fixed bugs:** - -- Fix arity checker bug - [#1546](https://github.com/anoma/juvix/pull/1546) - ([janmasrovira](https://github.com/janmasrovira)) -- Look in patterns when building the dependency graph - [#1536](https://github.com/anoma/juvix/pull/1536) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- Update language reference to match current state of Juvix - [#1594](https://github.com/anoma/juvix/pull/1594) - ([paulcadman](https://github.com/paulcadman)) -- Fix letrec printing - [#1591](https://github.com/anoma/juvix/pull/1591) - ([janmasrovira](https://github.com/janmasrovira)) -- Update stdlib submodule with builtin changes - [#1589](https://github.com/anoma/juvix/pull/1589) - ([paulcadman](https://github.com/paulcadman)) -- Rename builtin natural to nat and boolean to bool - [#1588](https://github.com/anoma/juvix/pull/1588) - ([paulcadman](https://github.com/paulcadman)) -- Improve the test for eta-expansion of constructors and builtins - [#1583](https://github.com/anoma/juvix/pull/1583) - ([lukaszcz](https://github.com/lukaszcz)) -- Properly newline expressions in the pretty printer - [#1581](https://github.com/anoma/juvix/pull/1581) - ([janmasrovira](https://github.com/janmasrovira)) -- Letrec lifting [#1579](https://github.com/anoma/juvix/pull/1579) - ([janmasrovira](https://github.com/janmasrovira)) -- Add softlines between applications and hang definitions - [#1578](https://github.com/anoma/juvix/pull/1578) - ([janmasrovira](https://github.com/janmasrovira)) -- Parse optional type info in JVC files - [#1575](https://github.com/anoma/juvix/pull/1575) - ([lukaszcz](https://github.com/lukaszcz)) -- Fix symbol numbering bug - [#1574](https://github.com/anoma/juvix/pull/1574) - ([lukaszcz](https://github.com/lukaszcz)) -- 1569 rewrite the test for lambda lifting to use evaluation - [#1572](https://github.com/anoma/juvix/pull/1572) - ([janmasrovira](https://github.com/janmasrovira)) -- Remove lambda from reservedSymbols - [#1568](https://github.com/anoma/juvix/pull/1568) - ([lukaszcz](https://github.com/lukaszcz)) -- Keywords refactor [#1566](https://github.com/anoma/juvix/pull/1566) - ([janmasrovira](https://github.com/janmasrovira)) -- remove ≔ from the language and replace it by := - [#1563](https://github.com/anoma/juvix/pull/1563) - ([janmasrovira](https://github.com/janmasrovira)) -- JuvixReg [#1551](https://github.com/anoma/juvix/pull/1551) - ([lukaszcz](https://github.com/lukaszcz)) -- Remove duplicate function in concrete analysis - [#1550](https://github.com/anoma/juvix/pull/1550) - ([ii8](https://github.com/ii8)) -- Evaluator minor style refactor - [#1547](https://github.com/anoma/juvix/pull/1547) - ([janmasrovira](https://github.com/janmasrovira)) -- Properly handle top lambdas in the termination checker - [#1544](https://github.com/anoma/juvix/pull/1544) - ([janmasrovira](https://github.com/janmasrovira)) -- Mutual inference [#1543](https://github.com/anoma/juvix/pull/1543) - ([janmasrovira](https://github.com/janmasrovira)) -- Autocomplete ".jvc" input files for core {eval, read} commands - [#1542](https://github.com/anoma/juvix/pull/1542) - ([paulcadman](https://github.com/paulcadman)) -- Add –show-de-bruijn to `core eval` command - [#1540](https://github.com/anoma/juvix/pull/1540) - ([paulcadman](https://github.com/paulcadman)) -- Inductive types should depend on the types of their constructors - [#1537](https://github.com/anoma/juvix/pull/1537) - ([lukaszcz](https://github.com/lukaszcz)) -- Parser labels [#1535](https://github.com/anoma/juvix/pull/1535) - ([janmasrovira](https://github.com/janmasrovira)) -- JuvixAsm [#1432](https://github.com/anoma/juvix/pull/1432) - ([lukaszcz](https://github.com/lukaszcz)) - -## [v0.2.5](https://github.com/anoma/juvix/tree/v0.2.5) (2022-09-14) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.4...v0.2.5) - -**Fixed bugs:** - -- Properly type check patterns that need normalization - [#1472](https://github.com/anoma/juvix/pull/1472) - ([janmasrovira](https://github.com/janmasrovira)) -- Detect nested patterns as smaller in the termination checker - [#1524](https://github.com/anoma/juvix/pull/1524) -- Fix developBeta in Core/Extra.hs - [#1487](https://github.com/anoma/juvix/pull/1487) - ([lukaszcz](https://github.com/lukaszcz)) -- Core/Extra/Recursors/Collector bugfix - [#1510](https://github.com/anoma/juvix/pull/1510) - ([lukaszcz](https://github.com/lukaszcz)) - -**Merged pull requests:** - -- Replace -\> by := in lambda syntax - [#1533](https://github.com/anoma/juvix/pull/1533) - ([janmasrovira](https://github.com/janmasrovira)) -- 'Match' with complex patterns in Core - [#1530](https://github.com/anoma/juvix/pull/1530) - ([lukaszcz](https://github.com/lukaszcz)) -- Refactor CLI [#1527](https://github.com/anoma/juvix/pull/1527) - ([janmasrovira](https://github.com/janmasrovira)) -- Add CanonicalProjection - [#1526](https://github.com/anoma/juvix/pull/1526) - ([janmasrovira](https://github.com/janmasrovira)) -- Make comma a delimiter - [#1525](https://github.com/anoma/juvix/pull/1525) - ([lukaszcz](https://github.com/lukaszcz)) -- Detect nested patterns as smaller in the termination checker - [#1524](https://github.com/anoma/juvix/pull/1524) - ([janmasrovira](https://github.com/janmasrovira)) -- Disallow tab characters as spaces - [#1523](https://github.com/anoma/juvix/pull/1523) - ([janmasrovira](https://github.com/janmasrovira)) -- Refactor `destruct` in Core/Extra/Base - [#1522](https://github.com/anoma/juvix/pull/1522) - ([lukaszcz](https://github.com/lukaszcz)) -- JuvixCore primitive types - [#1521](https://github.com/anoma/juvix/pull/1521) - ([lukaszcz](https://github.com/lukaszcz)) -- Enable autocompletion for the –theme flag - [#1519](https://github.com/anoma/juvix/pull/1519) - ([janmasrovira](https://github.com/janmasrovira)) -- Stripped version of Core Node datatype - [#1518](https://github.com/anoma/juvix/pull/1518) - ([lukaszcz](https://github.com/lukaszcz)) -- Add `internal core read` command - [#1517](https://github.com/anoma/juvix/pull/1517) - ([janmasrovira](https://github.com/janmasrovira)) -- Implement some instances for BinderList - [#1515](https://github.com/anoma/juvix/pull/1515) - ([janmasrovira](https://github.com/janmasrovira)) -- Back recursor types with type families - [#1514](https://github.com/anoma/juvix/pull/1514) - ([janmasrovira](https://github.com/janmasrovira)) -- Eager evaluation of Constr arguments - [#1513](https://github.com/anoma/juvix/pull/1513) - ([lukaszcz](https://github.com/lukaszcz)) -- Dynamic type in Core - [#1508](https://github.com/anoma/juvix/pull/1508) - ([lukaszcz](https://github.com/lukaszcz)) -- LetRec in Core [#1507](https://github.com/anoma/juvix/pull/1507) - ([lukaszcz](https://github.com/lukaszcz)) -- Add Haddock and Agda licenses - [#1506](https://github.com/anoma/juvix/pull/1506) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix docs webapp examples CI build - [#1505](https://github.com/anoma/juvix/pull/1505) - ([paulcadman](https://github.com/paulcadman)) -- Add CLI usage examples doc and integrate with README - [#1504](https://github.com/anoma/juvix/pull/1504) - ([paulcadman](https://github.com/paulcadman)) -- Refactor BinderInfo - [#1503](https://github.com/anoma/juvix/pull/1503) - ([lukaszcz](https://github.com/lukaszcz)) -- Make `juvix compile` default to native target - [#1502](https://github.com/anoma/juvix/pull/1502) - ([paulcadman](https://github.com/paulcadman)) -- Refactor Node datatype - [#1501](https://github.com/anoma/juvix/pull/1501) - ([lukaszcz](https://github.com/lukaszcz)) -- Clean up import list in Pipeline - [#1499](https://github.com/anoma/juvix/pull/1499) - ([jonaprieto](https://github.com/jonaprieto)) -- Remove mono [#1497](https://github.com/anoma/juvix/pull/1497) - ([jonaprieto](https://github.com/jonaprieto)) -- Remove Haskell support - [#1496](https://github.com/anoma/juvix/pull/1496) - ([jonaprieto](https://github.com/jonaprieto)) -- Implement lambda lifting - [#1494](https://github.com/anoma/juvix/pull/1494) - ([janmasrovira](https://github.com/janmasrovira)) -- Document Emacs installation and the 'exec-path' problem - [#1493](https://github.com/anoma/juvix/pull/1493) - ([lukaszcz](https://github.com/lukaszcz)) -- Add –allow-different-user to workflow stack command - [#1492](https://github.com/anoma/juvix/pull/1492) - ([paulcadman](https://github.com/paulcadman)) -- Stack with github actions permissions workaround - [#1490](https://github.com/anoma/juvix/pull/1490) - ([paulcadman](https://github.com/paulcadman)) -- Restructure recursors and add some lens interfaces - [#1489](https://github.com/anoma/juvix/pull/1489) - ([janmasrovira](https://github.com/janmasrovira)) -- Add a github action to build a static linux binary - [#1488](https://github.com/anoma/juvix/pull/1488) - ([paulcadman](https://github.com/paulcadman)) -- Fix developBeta in Core/Extra.hs - [#1487](https://github.com/anoma/juvix/pull/1487) - ([lukaszcz](https://github.com/lukaszcz)) -- Add an option to show name ids in errors - [#1486](https://github.com/anoma/juvix/pull/1486) - ([lukaszcz](https://github.com/lukaszcz)) - -## [v0.2.4](https://github.com/anoma/juvix/tree/v0.2.4) (2022-08-19) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.3...v0.2.4) - -(Special version for Heliax's retreat in Italy) - -**Implemented enhancements:** - -- Add –stdin flag [#1459](https://github.com/anoma/juvix/pull/1459) - ([janmasrovira](https://github.com/janmasrovira)) - -**Fixed bugs:** - -- Fix typechecker [#1458](https://github.com/anoma/juvix/pull/1458) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- use –stdin in flycheck mode - [#1460](https://github.com/anoma/juvix/pull/1460) - ([janmasrovira](https://github.com/janmasrovira)) -- Add a native compile target for demos - [#1457](https://github.com/anoma/juvix/pull/1457) - ([paulcadman](https://github.com/paulcadman)) -- Small changes for the presentation - [#1456](https://github.com/anoma/juvix/pull/1456) - ([jonaprieto](https://github.com/jonaprieto)) -- Fixes TicTacToe Web example - [#1454](https://github.com/anoma/juvix/pull/1454) - ([paulcadman](https://github.com/paulcadman)) -- Upgrade to ghc-9.2.4 - [#1451](https://github.com/anoma/juvix/pull/1451) - ([janmasrovira](https://github.com/janmasrovira)) - -## [v0.2.3](https://github.com/anoma/juvix/tree/v0.2.3) (2022-08-15) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.2...v0.2.3) - -**Implemented enhancements:** - -- add `name` and `version` to `juvix.yaml` - [#1422](https://github.com/anoma/juvix/pull/1422) - ([janmasrovira](https://github.com/janmasrovira)) - -**Fixed bugs:** - -- Properly handle paragraphs in judoc - [#1447](https://github.com/anoma/juvix/pull/1447) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- Give a proper type to literal natural numbers - [#1453](https://github.com/anoma/juvix/pull/1453) - ([janmasrovira](https://github.com/janmasrovira)) -- Add the option to output json in the `juvix internal highlight` - command [#1450](https://github.com/anoma/juvix/pull/1450) - ([janmasrovira](https://github.com/janmasrovira)) for supporting the - new Juvix Mode for Visual Studio Code - ([jonaprieto](https://github.com/anoma/vscode-juvix)) -- Allow \_ in Wasm exported names to support Anoma signature - [#1449](https://github.com/anoma/juvix/pull/1449) - ([paulcadman](https://github.com/paulcadman)) -- Add Towers of Hanoi and Pascal triangle examples - [#1446](https://github.com/anoma/juvix/pull/1446) - ([paulcadman](https://github.com/paulcadman)) -- Add `juvix init` command - [#1445](https://github.com/anoma/juvix/pull/1445) - ([janmasrovira](https://github.com/janmasrovira)) -- Refactor pretty to reduce duplication - [#1443](https://github.com/anoma/juvix/pull/1443) - ([janmasrovira](https://github.com/janmasrovira)) -- Add initial support for examples in Html documentation - [#1442](https://github.com/anoma/juvix/pull/1442) - ([janmasrovira](https://github.com/janmasrovira)) -- Add revisions to README - [#1440](https://github.com/anoma/juvix/pull/1440) - ([jonaprieto](https://github.com/jonaprieto)) -- CI: Run build on push to main - [#1437](https://github.com/anoma/juvix/pull/1437) - ([paulcadman](https://github.com/paulcadman)) -- Add doctor subcommand - [#1436](https://github.com/anoma/juvix/pull/1436) - ([paulcadman](https://github.com/paulcadman)) -- CI checkout repo before cache and use recommended cache strategy - [#1435](https://github.com/anoma/juvix/pull/1435) - ([paulcadman](https://github.com/paulcadman)) -- Various documentation adjustments - [#1434](https://github.com/anoma/juvix/pull/1434) - ([paulcadman](https://github.com/paulcadman)) -- Setup Clang before building docs in CI - [#1433](https://github.com/anoma/juvix/pull/1433) - ([paulcadman](https://github.com/paulcadman)) -- Major revisions to Makefile - [#1431](https://github.com/anoma/juvix/pull/1431) - ([jonaprieto](https://github.com/jonaprieto)) -- Do not add `-src` suffix to links in HTML when running `juvix html` - [#1429](https://github.com/anoma/juvix/pull/1429) - ([paulcadman](https://github.com/paulcadman)) -- Add a Web version of TicTacToe - [#1427](https://github.com/anoma/juvix/pull/1427) - ([paulcadman](https://github.com/paulcadman)) -- WASM import all non-compile axioms with alphanum names in entrypoint - [#1426](https://github.com/anoma/juvix/pull/1426) - ([paulcadman](https://github.com/paulcadman)) -- Export all functions with alpha numeric names from entrypoint module - [#1425](https://github.com/anoma/juvix/pull/1425) - ([paulcadman](https://github.com/paulcadman)) -- Refactor [#1420](https://github.com/anoma/juvix/pull/1420) - ([jonaprieto](https://github.com/jonaprieto)) -- Permit axiom without a compile block - [#1418](https://github.com/anoma/juvix/pull/1418) - ([paulcadman](https://github.com/paulcadman)) -- Implement an html documentation generator similar to haddock (#1413) - [#1416](https://github.com/anoma/juvix/pull/1416) - ([janmasrovira](https://github.com/janmasrovira)) -- Fix version shell test for 0.2.2 - [#1415](https://github.com/anoma/juvix/pull/1415) - ([paulcadman](https://github.com/paulcadman)) -- Remove Int from stdlib and update SimpleFungibleToken example - [#1414](https://github.com/anoma/juvix/pull/1414) - ([paulcadman](https://github.com/paulcadman)) - -## [v0.2.2](https://github.com/anoma/juvix/tree/v0.2.2) (2022-07-25) - -[Full Changelog](https://github.com/anoma/juvix/compare/v0.2.1...v0.2.2) - -**Implemented enhancements:** - -- Compute name dependency graph and filter unreachable definitions - [#1408](https://github.com/anoma/juvix/pull/1408) - ([lukaszcz](https://github.com/lukaszcz)) -- Support type aliases - [#1404](https://github.com/anoma/juvix/pull/1404) - ([janmasrovira](https://github.com/janmasrovira)) -- Add debugging custom function to Prelude - [#1401](https://github.com/anoma/juvix/pull/1401) - ([jonaprieto](https://github.com/jonaprieto)) -- Add positivity check for data types - [#1393](https://github.com/anoma/juvix/pull/1393) - ([jonaprieto](https://github.com/jonaprieto)) -- Keep qualified names - [#1392](https://github.com/anoma/juvix/pull/1392) - ([janmasrovira](https://github.com/janmasrovira)) -- Direct translation from MicroJuvix to MiniC - [#1386](https://github.com/anoma/juvix/pull/1386) - ([lukaszcz](https://github.com/lukaszcz)) -- Widens the accepted symbol list - [#1385](https://github.com/anoma/juvix/pull/1385) - ([mariari](https://github.com/mariari)) -- Check all the type parameter names are different when declaring an - inductive type [#1377](https://github.com/anoma/juvix/pull/1377) - ([jonaprieto](https://github.com/jonaprieto)) - -**Fixed bugs:** - -- Curly braces are allowed nested in patterns - [#1380](https://github.com/anoma/juvix/pull/1380) - ([janmasrovira](https://github.com/janmasrovira)) - -**Merged pull requests:** - -- Add `Fail` effect (#1409) - [#1411](https://github.com/anoma/juvix/pull/1411) - ([janmasrovira](https://github.com/janmasrovira)) -- Refactor of typechecking and other checking processes - [#1410](https://github.com/anoma/juvix/pull/1410) - ([jonaprieto](https://github.com/jonaprieto)) -- Use bold for code in scoper error messages - [#1403](https://github.com/anoma/juvix/pull/1403) - ([janmasrovira](https://github.com/janmasrovira)) -- Replace ppSimple by text - [#1402](https://github.com/anoma/juvix/pull/1402) - ([jonaprieto](https://github.com/jonaprieto)) -- Implement some error messages (#1396) - [#1400](https://github.com/anoma/juvix/pull/1400) - ([lukaszcz](https://github.com/lukaszcz)) -- Refactor childs of pattern parentheses and braces - [#1398](https://github.com/anoma/juvix/pull/1398) - ([janmasrovira](https://github.com/janmasrovira)) -- Update Juvix standard-library - [#1389](https://github.com/anoma/juvix/pull/1389) - ([jonaprieto](https://github.com/jonaprieto)) -- Fix documentation generation - [#1387](https://github.com/anoma/juvix/pull/1387) - ([jonaprieto](https://github.com/jonaprieto)) -- Adds Collatz sequence generator example - [#1384](https://github.com/anoma/juvix/pull/1384) - ([paulcadman](https://github.com/paulcadman)) -- html-examples [#1381](https://github.com/anoma/juvix/pull/1381) - ([jonaprieto](https://github.com/jonaprieto)) -- Refine hole in type signature to function type - [#1379](https://github.com/anoma/juvix/pull/1379) - ([janmasrovira](https://github.com/janmasrovira)) -- Type checking fails when the type of a pattern is not given by the - signature [#1378](https://github.com/anoma/juvix/pull/1378) - ([janmasrovira](https://github.com/janmasrovira)) -- Set cname for gh-pages action - [#1376](https://github.com/anoma/juvix/pull/1376) - ([paulcadman](https://github.com/paulcadman)) -- Add fibonacci sequence example program - [#1375](https://github.com/anoma/juvix/pull/1375) - ([paulcadman](https://github.com/paulcadman)) -- Fix Changelog links and minors - [#1371](https://github.com/anoma/juvix/pull/1371) - ([jonaprieto](https://github.com/jonaprieto)) -- Add Version number to the emacs mode - [#1320](https://github.com/anoma/juvix/pull/1320) - ([mariari](https://github.com/mariari)) - -## New name: Juvix - -Since version 0.2.2, the project has been renamed from "Mini Juvix" to -"Juvix". The new name reflects the fact that the project is no longer -just a compiler for a subset of Juvix, but a full implementation of the -language. Affected by this change are: - -- Github repository moved from the Heliax organization to the Anoma - organization. "anoma/juvix" is the new repository name. -- All references to "Mini Juvix" have been replaced with "Juvix". - Unfortunetly, - -due to the move, the old links to the Mini Juvix repository are broken -and will not be fixed. - -## v0.2.1 (2022-07-12) - -**Implemented enhancements:** - -- Specialize commands of/for internal use MiniJuvix-#270 - ([jonaprieto](https://github.com/jonaprieto)) -- Improve handling of location information for different objs - MiniJuvix-#263 ([jonaprieto](https://github.com/jonaprieto)) -- Add issues and PR templates MiniJuvix-#261 - ([jonaprieto](https://github.com/jonaprieto)) -- Throw error when reading a file that conflicts with embedded stdlib - MiniJuvix-#243 ([paulcadman](https://github.com/paulcadman)) -- Embed standard library in the minijuvix binary MiniJuvix-#210 - ([paulcadman](https://github.com/paulcadman)) - -**Fixed bugs:** - -- Fixed a bug with the path to walloc.c MiniJuvix-#237 - ([lukaszcz](https://github.com/lukaszcz)) -- Perform ScopedToAbstract exactly once for each module MiniJuvix-#223 - ([paulcadman](https://github.com/paulcadman)) - -**Merged pull requests:** - -- Label renaming MiniJuvix-#275 - ([jonaprieto](https://github.com/jonaprieto)) -- Update link to discord MiniJuvix-#264 - ([Romainua](https://github.com/Romainua)) -- Include `open import` statements when generating HTML MiniJuvix-#260 - ([paulcadman](https://github.com/paulcadman)) -- Renaming MiniJuvix to Juvix MiniJuvix-#259 - ([jonaprieto](https://github.com/jonaprieto)) -- Updates tests to use the updated standard library MiniJuvix-#253 - ([paulcadman](https://github.com/paulcadman)) -- Enforce C99 standard in the generated C files MiniJuvix-#252 - ([lukaszcz](https://github.com/lukaszcz)) -- Restore mascot images to the minijuvix book MiniJuvix-#250 - ([paulcadman](https://github.com/paulcadman)) -- Allow jumping to another module in emacs MiniJuvix-#249 - ([janmasrovira](https://github.com/janmasrovira)) -- Restore Juvix mascot image to README MiniJuvix-#248 - ([paulcadman](https://github.com/paulcadman)) -- Add emacs option `minijuvix-disable-embedded-stdlib` MiniJuvix-#247 - ([paulcadman](https://github.com/paulcadman)) -- Deprecate GHC backend MiniJuvix-#244 - ([lukaszcz](https://github.com/lukaszcz)) -- Removed 'eval' and 'print' keywords (#214) MiniJuvix-#242 - ([lukaszcz](https://github.com/lukaszcz)) -- Add option to disable minijuvix input method MiniJuvix-#239 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove the 'match' keyword MiniJuvix-#238 - ([lukaszcz](https://github.com/lukaszcz)) -- Removed tests/positive/HelloWorld.mjuvix and specified clang version - in the documentation MiniJuvix-#236 - ([lukaszcz](https://github.com/lukaszcz)) -- Filter symbol entries properly in the scoper MiniJuvix-#234 - ([janmasrovira](https://github.com/janmasrovira)) -- Use the ModulesCache for `open` statements in ScopedToAbstract pass - MiniJuvix-#224 ([paulcadman](https://github.com/paulcadman)) -- README: Include `--recursive` in git clone command to fetch stdlib - MiniJuvix-#211 ([paulcadman](https://github.com/paulcadman)) -- Update project description v0.2.0 MiniJuvix-#209 - ([jonaprieto](https://github.com/jonaprieto)) -- Unify AST representation of types and expressions in MicroJuvix - MiniJuvix-#188 ([janmasrovira](https://github.com/janmasrovira)) - -## v0.2.0 (2022-06-28) - -**Implemented enhancements:** - -- Support built in types MiniJuvix-#192 - ([janmasrovira](https://github.com/janmasrovira)) -- Support partial application and closure passing in C backend - MiniJuvix-#190 ([paulcadman](https://github.com/paulcadman)) -- Allow `open import` statements MiniJuvix-#175 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove TypeAny and adapt typechecking for literals MiniJuvix-#173 - ([janmasrovira](https://github.com/janmasrovira)) -- Allow holes to be refined into function types MiniJuvix-#165 - ([janmasrovira](https://github.com/janmasrovira)) -- Support implicit arguments MiniJuvix-#144 - ([janmasrovira](https://github.com/janmasrovira)) -- Add support for holes in type signatures MiniJuvix-#141 - ([janmasrovira](https://github.com/janmasrovira)) -- Support function closures with no environment in minic - MiniJuvix-#137 ([paulcadman](https://github.com/paulcadman)) -- Add holes for expressions in function clauses and inference support - MiniJuvix-#136 ([janmasrovira](https://github.com/janmasrovira)) -- Add "-Oz" optimization flag to clang args MiniJuvix-#133 - ([paulcadman](https://github.com/paulcadman)) -- Add version and help option and root command to the CLI - MiniJuvix-#131 ([jonaprieto](https://github.com/jonaprieto)) - -**Fixed bugs:** - -- Fix: Ignore implicit patterns and arguments in termination checking - MiniJuvix-#172 ([janmasrovira](https://github.com/janmasrovira)) -- Fix: pretty printing for terminating keyword MiniJuvix-#145 - ([jonaprieto](https://github.com/jonaprieto)) - -**Merged pull requests:** - -- Fix: proper error handling for typechecker errors MiniJuvix-#189 - ([jonaprieto](https://github.com/jonaprieto)) -- Add juvix version info and date to HTML output MiniJuvix-#186 - ([jonaprieto](https://github.com/jonaprieto)) -- Fix: Add check for constructor return types MiniJuvix-#182 - ([jonaprieto](https://github.com/jonaprieto)) -- Use Abstract name in Abstract syntax and Micro/MonoJuvix - MiniJuvix-#181 ([janmasrovira](https://github.com/janmasrovira)) -- Add an option to specify the path where to put the HTML output - MiniJuvix-#179 ([jonaprieto](https://github.com/jonaprieto)) -- Upgrade to ghc-9.2.3 MiniJuvix-#178 - ([janmasrovira](https://github.com/janmasrovira)) -- Replace dead link in README with a link to the Juvix book - MiniJuvix-#177 ([paulcadman](https://github.com/paulcadman)) -- Embed HTML assets in the juvix binary MiniJuvix-#176 - ([paulcadman](https://github.com/paulcadman)) -- Fix: identifiers with a keyword prefix cannot be parsed - MiniJuvix-#171 ([janmasrovira](https://github.com/janmasrovira)) -- Improve filepath equality MiniJuvix-#170 - ([janmasrovira](https://github.com/janmasrovira)) -- Update validity predicate milestone example to 0.2 syntax - MiniJuvix-#167 ([paulcadman](https://github.com/paulcadman)) -- Fix links in documentation and update to new syntax MiniJuvix-#163 - ([paulcadman](https://github.com/paulcadman)) -- Update stdlib to work with version 0.2 MiniJuvix-#160 - ([janmasrovira](https://github.com/janmasrovira)) -- Update README usage example to use the compile command - MiniJuvix-#158 ([paulcadman](https://github.com/paulcadman)) -- Remove dead code related to the pipeline MiniJuvix-#156 - ([janmasrovira](https://github.com/janmasrovira)) -- Add negative test for AppLeftImplicit MiniJuvix-#154 - ([janmasrovira](https://github.com/janmasrovira)) -- Add positive test designed for implicit arguments MiniJuvix-#153 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove ExpressionTyped from MicroJuvix MiniJuvix-#143 - ([janmasrovira](https://github.com/janmasrovira)) -- Revision for package.yaml and minor deletions MiniJuvix-#135 - ([jonaprieto](https://github.com/jonaprieto)) - -## v0.1.4 (2022-05-30) - -**Merged pull requests:** - -- Generic Errors and refactoring MiniJuvix-#123 - ([jonaprieto](https://github.com/jonaprieto)) -- Only generates docs if the pull request merges MiniJuvix-#121 - ([jonaprieto](https://github.com/jonaprieto)) -- Add initial docs generation website MiniJuvix-#119 - ([jonaprieto](https://github.com/jonaprieto)) -- Fix internal link in README MiniJuvix-#116 - ([paulcadman](https://github.com/paulcadman)) -- Add minic-runtime for linking without libc MiniJuvix-#113 - ([paulcadman](https://github.com/paulcadman)) -- Add termination checking to the pipeline MiniJuvix-#111 - ([jonaprieto](https://github.com/jonaprieto)) -- Support uncurried higher order functions MiniJuvix-#110 - ([paulcadman](https://github.com/paulcadman)) -- Improve error generation and handling MiniJuvix-#108 - ([janmasrovira](https://github.com/janmasrovira)) -- Add MiniC tests with clang+wasi-sdk MiniJuvix-#105 - ([paulcadman](https://github.com/paulcadman)) -- Add usage example and move developer docs MiniJuvix-#96 - ([paulcadman](https://github.com/paulcadman)) -- Refactor warning related stuff MiniJuvix-#91 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove Agda backend MiniJuvix-#86 - ([paulcadman](https://github.com/paulcadman)) - -**Implemented enhancements:** - -- Add `compile` subcommand to generate binaries MiniJuvix-#128 -- Add intervals to flycheck errors MiniJuvix-#124 -- Improve error handling in juvix-mode MiniJuvix-#107 -- Support multiple modules in compilation MiniJuvix-#93 -- Add compile command to CLI MiniJuvix-#130 - ([paulcadman](https://github.com/paulcadman)) -- Use Interval in GenericErrors MiniJuvix-#125 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove dev in the CI and other tweaks MiniJuvix-#118 - ([jonaprieto](https://github.com/jonaprieto)) -- Highlight comments correctly MiniJuvix-#106 - ([janmasrovira](https://github.com/janmasrovira)) -- Support multiple modules in compilation MiniJuvix-#100 - ([janmasrovira](https://github.com/janmasrovira)) -- New target syntax and modular VP examples MiniJuvix-#92 - ([jonaprieto](https://github.com/jonaprieto)) - -**Fixed bugs:** - -- Missing error messages when using throw/error MiniJuvix-#117 -- Fix highlight of comments MiniJuvix-#104 -- Fix juvix-mode coloring for projects with multiple modules - MiniJuvix-#101 -- Fix `highlight` command for modules with import statements - MiniJuvix-#102 ([janmasrovira](https://github.com/janmasrovira)) - -**Closed issues:** - -- Deprecate the class JuvixError MiniJuvix-#115 -- Add ToGenericError instance for the infix parsing errors - MiniJuvix-#114 -- Compile to WASM without linking libc MiniJuvix-#112 -- Add the termination checker to the pipeline MiniJuvix-#109 -- Use clang + wasi-sdk instead of emcc to compile to WASM - MiniJuvix-#103 -- Move developer tooling docs out of README MiniJuvix-#95 -- Add pre-commit checks to CI checks MiniJuvix-#94 -- Support higher order functions in C backend MiniJuvix-#90 -- Remove dev from the list of branches in the CI MiniJuvix-#89 -- Refactor warning related stuff MiniJuvix-#87 -- The Juvix website MiniJuvix-#51 - -## v0.1.3 (2022-05-05) - -**Closed issues:** - -- Monomorphisation naming inconsistency MiniJuvix-#84 -- Remove BackendAgda MiniJuvix-#83 -- Change terminating keyword behavior MiniJuvix-#81 -- MonoJuvix `ExpressionTyped` is never used MiniJuvix-#79 -- Bump stackage nightly and delete `allow-newer: true` from - `stack.yaml` MiniJuvix-#75 -- Generate automatically CHANGELOG and Github Release Notes - MiniJuvix-#73 -- Make flag –show-name-ids global MiniJuvix-#61 -- Add C code generation backend MiniJuvix-#60 -- Add polymorphism MiniJuvix-#59 -- Add the compile keyword to the frontend syntax (support up to - Scoping) MiniJuvix-#58 -- Error with undefined or underscores MiniJuvix-#54 -- Add support for other GHC and Stack stable version MiniJuvix-#52 -- Autodetect output ANSI support when prettyprinting MiniJuvix-#38 -- Terminating for type signatures MiniJuvix-#11 - -**Merged pull requests:** - -- Remove agda backend MiniJuvix-#86 - ([paulcadman](https://github.com/paulcadman)) -- 84 monomorphisation naming inconsistency MiniJuvix-#85 - ([janmasrovira](https://github.com/janmasrovira)) -- Change terminating keyword behavior MiniJuvix-#82 - ([jonaprieto](https://github.com/jonaprieto)) -- Remove unused constructor ExpressionTyped in Monojuvix MiniJuvix-#80 - ([janmasrovira](https://github.com/janmasrovira)) -- Stricter stack builds and pedantic mode for CI MiniJuvix-#78 - ([jonaprieto](https://github.com/jonaprieto)) -- Bump stackage version and remove allow-newer MiniJuvix-#76 - ([janmasrovira](https://github.com/janmasrovira)) -- Add automatically updates/issues/merged PRs to the changelog - MiniJuvix-#74 ([jonaprieto](https://github.com/jonaprieto)) -- Add terminating keyword MiniJuvix-#71 - ([jonaprieto](https://github.com/jonaprieto)) -- Monomorphization MiniJuvix-#70 - ([janmasrovira](https://github.com/janmasrovira)) -- Remove StatementCompile in AST after scoping MiniJuvix-#69 - ([paulcadman](https://github.com/paulcadman)) -- Add C code generation backend MiniJuvix-#68 - ([paulcadman](https://github.com/paulcadman)) -- Check if stderr supports ANSI and print accordingly MiniJuvix-#67 - ([janmasrovira](https://github.com/janmasrovira)) -- Add support for compile (by Jonathan) MiniJuvix-#66 - ([paulcadman](https://github.com/paulcadman)) -- Add NameIdGen effect to the pipeline MiniJuvix-#64 - ([janmasrovira](https://github.com/janmasrovira)) -- Make the `--show-name-ids` flag global MiniJuvix-#63 - ([janmasrovira](https://github.com/janmasrovira)) -- Implement type checker with polymorphism MiniJuvix-#62 - ([janmasrovira](https://github.com/janmasrovira)) - -## v0.1.2 (2022-04-11) - -**Closed issues:** - -- Add en emacs mode with support for scoped highlighting MiniJuvix-#25 -- Add support for project root detection through a juvix.yaml file - MiniJuvix-#24 -- Add CLI cmd to generate juvix autocompletion files for fish and zsh - MiniJuvix-#23 -- Add pretty and typecheck subcommands to the microjuvix CLI - MiniJuvix-#21 -- Translate identifiers from MicroJuvix to MiniHaskell (valid Haskell) - MiniJuvix-#19 -- Implement the MiniHaskell to Haskell translation (prettyprinter) - MiniJuvix-#18 -- Implementation of a typechecker for MicroJuvix MiniJuvix-#16 -- Add references to the Abstract AST to update compilation to - MiniHaskell MiniJuvix-#12 -- Order in the house MiniJuvix-#10 - -**Merged pull requests:** - -- The Juvix project now follows the same goals as the original Juvix - project. MiniJuvix-#7 ([jonaprieto](https://github.com/jonaprieto)) -- Dev→main MiniJuvix-#6 ([jonaprieto](https://github.com/jonaprieto)) -- Big update including termination checking MiniJuvix-#5 - ([janmasrovira](https://github.com/janmasrovira)) -- Parser and scoper MiniJuvix-#3 - ([jonaprieto](https://github.com/jonaprieto)) -- Upgrade to ghc9 and use hpack MiniJuvix-#2 - ([janmasrovira](https://github.com/janmasrovira)) -- Merge MiniJuvix-#1 ([jonaprieto](https://github.com/jonaprieto)) - -## v0.1.1 (2022-03-25) - -- Add support in the parser/scoper for Axiom backends -- Add support for `foreign` keyword -- Add flag `--no-colors` for the scope command -- Upgrade to GHC 9.2.2 -- Improve resolution of local symbols in the scoper -- Several new tests related to ambiguous symbols -- Add `--version` flag -- Add InfoTableBuilder effect for the scoper - -**Closed issues:** - -- Add diff output to the test suite MiniJuvix-#9 -- Improve scoper ambiguity error messages MiniJuvix-#8 diff --git a/docs/examples/README.md b/docs/examples/README.md deleted file mode 100644 index 75e44c6d9..000000000 --- a/docs/examples/README.md +++ /dev/null @@ -1,15 +0,0 @@ -## [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](./html/examples/html/HelloWorld/HelloWorld.html) -- [Fibonacci.juvix](./html/examples/html/Fibonacci/Fibonacci.html) -- [Hanoi.juvix](./html/examples/html/Hanoi/Hanoi.html) -- [PascalsTriangle.juvix](./html/examples/html/PascalsTriangle/PascalsTriangle.html) -- [Collatz.juvix](./html/examples/html/Collatz/Collatz.html) -- [TicTacToe.juvix](./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. diff --git a/docs/explanations/totality/README.md b/docs/explanations/totality/README.md deleted file mode 100644 index d68a6db08..000000000 --- a/docs/explanations/totality/README.md +++ /dev/null @@ -1 +0,0 @@ -# Totality checking diff --git a/docs/explanations/totality/coverage.md b/docs/explanations/totality/coverage.md deleted file mode 100644 index ba2cdb89b..000000000 --- a/docs/explanations/totality/coverage.md +++ /dev/null @@ -1 +0,0 @@ -# Coverage checking diff --git a/docs/explanations/totality/positive.md b/docs/explanations/totality/positive.md deleted file mode 100644 index ca0db59f7..000000000 --- a/docs/explanations/totality/positive.md +++ /dev/null @@ -1 +0,0 @@ -# Strictly positive data types diff --git a/docs/explanations/totality/termination.md b/docs/explanations/totality/termination.md deleted file mode 100644 index 2d9fb9457..000000000 --- a/docs/explanations/totality/termination.md +++ /dev/null @@ -1,29 +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 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. diff --git a/docs/explanations/typetheory.md b/docs/explanations/typetheory.md deleted file mode 100644 index 4fdafc3f4..000000000 --- a/docs/explanations/typetheory.md +++ /dev/null @@ -1 +0,0 @@ -# Type theory diff --git a/docs/howto/compilation.md b/docs/howto/compilation.md deleted file mode 100644 index c0e50cfeb..000000000 --- a/docs/howto/compilation.md +++ /dev/null @@ -1,61 +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`: - -```juvix --- Hello world example. This is a comment. -module Hello; - --- Import the standard library prelude, including the 'String' type -open import Stdlib.Prelude; - -main : String; -main := "Hello world!"; -``` - -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. - -# Compilation options - -To see all compilation options type `juvix compile --help`. The most -commonly used options are: - -- `-t target`: specify the target, -- `-g`: generate debug information and runtime assertions, -- `-o file`: specify the output 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 interactively initialize a Juvix project in the current directory, -use `juvix init`. - -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). diff --git a/docs/howto/installing.md b/docs/howto/installing.md deleted file mode 100644 index df57614f1..000000000 --- a/docs/howto/installing.md +++ /dev/null @@ -1,135 +0,0 @@ -# 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 x8664 - -A Juvix compiler binary executable for Linux x8664 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.2/juvix-linux_x86_64-v0.3.2.zip -unzip juvix-linux_x86_64-v0.3.2.zip -mv juvix-linux_x86_64-v0.3.2 ~/.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 - ``` diff --git a/docs/howto/judoc.md b/docs/howto/judoc.md deleted file mode 100644 index e9211df66..000000000 --- a/docs/howto/judoc.md +++ /dev/null @@ -1 +0,0 @@ -# Documenting Juvix programs with Judoc diff --git a/docs/notes/README.md b/docs/notes/README.md deleted file mode 100644 index e69de29bb..000000000 diff --git a/docs/notes/builtins.md b/docs/notes/builtins.md deleted file mode 100644 index 4ce8ad30c..000000000 --- a/docs/notes/builtins.md +++ /dev/null @@ -1,82 +0,0 @@ ---- -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 ↦ plusone}; - 2. How to test if a term matches a pattern with that - constructor. E.g. {zero ↦ iszero; suc ↦ - isnotzero}; - 3. How to deconstruct/project each of the constructor - arguments. E.g. {zero ↦ ∅; suc ↦ minusone}}. 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}. diff --git a/docs/notes/lsp.md b/docs/notes/lsp.md deleted file mode 100644 index 10197fb3b..000000000 --- a/docs/notes/lsp.md +++ /dev/null @@ -1,16 +0,0 @@ -# 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 -``` diff --git a/docs/notes/monomorphization.md b/docs/notes/monomorphization.md deleted file mode 100644 index 3df563e18..000000000 --- a/docs/notes/monomorphization.md +++ /dev/null @@ -1,228 +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: - -```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 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. diff --git a/docs/notes/runtime-benchmark-results.md b/docs/notes/runtime-benchmark-results.md deleted file mode 100644 index 7a2e4a458..000000000 --- a/docs/notes/runtime-benchmark-results.md +++ /dev/null @@ -1,343 +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 228 (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 = 220, 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 foldleft -(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 228 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 228 (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 = 220, 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 228 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. diff --git a/docs/notes/strictly-positive-data-types.md b/docs/notes/strictly-positive-data-types.md deleted file mode 100644 index f845a6d67..000000000 --- a/docs/notes/strictly-positive-data-types.md +++ /dev/null @@ -1,77 +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. - -```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; - ``` diff --git a/docs/quick-start.md b/docs/quick-start.md deleted file mode 100644 index ad4eaa793..000000000 --- a/docs/quick-start.md +++ /dev/null @@ -1,91 +0,0 @@ -# Quick Start - - -Juvix Mascot - - -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. - -Run Juvix doctor to check your system setup: - -```shell -juvix doctor -``` - -## CLI Usage Examples - -Create a new package: - -```shell -juvix init -``` - -Compile a source file into an executable: - -```shell -juvix compile path/to/source.juvix -``` - -Compile a source file into a WebAssembly binary: - -```shell -juvix compile -t wasm path/to/source.juvix -``` - -Launch the REPL: - -```shell -juvix repl -``` - -Typecheck a source file: - -```shell -juvix typecheck path/to/source.juvix -``` - -Generate HTML representations of a source file and its imports: - -```shell -juvix html --recursive path/to/source.juvix -``` - -## The Hello World example - -This is the Juvix source code of the traditional Hello World program. - -```shell --- HelloWorld.juvix -module HelloWorld; - -open import Stdlib.Prelude; - -main : IO; -main := printStringLn "hello world!"; - -end; -``` - -To compile and run a binary generated by Juvix, save the source code to -a file called `HelloWorld.juvix` and run the following command from the -directory containing it: - -```shell -juvix compile HelloWorld.juvix -./HelloWorld -``` - -You should see the output: `hello world!` - -The source code can also be compiled to a WebAssembly binary. This -requires some additional setup. See the [Installation -How-to](https://anoma.github.io/juvix/howto/installing.html) for more -information. You can also run `juvix doctor` to check your setup. - -```shell -juvix compile --target wasm HelloWorld.juvix -wasmer HelloWorld.wasm -``` diff --git a/docs/reference/benchmarks.md b/docs/reference/benchmarks.md deleted file mode 100644 index 680d5655b..000000000 --- a/docs/reference/benchmarks.md +++ /dev/null @@ -1 +0,0 @@ -# Benchmarks diff --git a/docs/reference/examples.md b/docs/reference/examples.md deleted file mode 100644 index 88613be6f..000000000 --- a/docs/reference/examples.md +++ /dev/null @@ -1,10 +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`. - -- [HelloWorld.juvix](./../examples/html/HelloWorld/HelloWorld.html) -- [Fibonacci.juvix](./../examples/html/Fibonacci/Fibonacci.html) -- [Hanoi.juvix](./../examples/html/Hanoi/Hanoi.html) -- [PascalsTriangle.juvix](./../examples/html/PascalsTriangle/PascalsTriangle.html) -- [Collatz.juvix](./../examples/html/Collatz/Collatz.html) -- [TicTacToe.juvix](./../examples/html/TicTacToe/CLI/CLI.TicTacToe.html) diff --git a/docs/reference/judoc.md b/docs/reference/judoc.md deleted file mode 100644 index f65045f7b..000000000 --- a/docs/reference/judoc.md +++ /dev/null @@ -1,120 +0,0 @@ -# Judoc syntax reference - -Judoc is used to document parts of your code. You can attach _Judoc -blocks_ to the following entities: - -1. A module. -2. A type definition. -3. A constructor definition. -4. A type signature of a function. -5. An axiom definition. - -In order to attach documentation to any of these entities, write _blocks_ of -documentation before them: - -1. For modules: - ``` - --- This module is cool - module Cool; - .. - ``` -2. For type definitions: - ``` - --- Unary representation of natural numbers - type Nat : Type := - | --- Nullary constructor representing number 0 - zero : Nat - | --- Unary constructor representing the successor of a natural number - suc : Nat -> Nat; - ``` -3. For type signatures (and likewise for axioms): - - ``` - --- The polymorphic identity function - id : {A : Type} -> A -> A; - ``` - - Next we define the syntax of Judoc _blocks_. - -## Block - -A _block_ can be one of these: - -1. A _paragraph_. -2. An _example_. - -_Blocks_ are separated by a line with only `---`. -For instance, this is a sequence of two _blocks_: - -``` ---- First block ---- ---- Second block -``` - -Note that the following is a single block since it lacks the `---` separator: - -``` ---- First block - ---- Still first block -``` - -### Paragraph - -A _paragraph_ is a non-empty sequence of _lines_. - -For instance, the following is a paragraph with two _lines_: - -``` ---- First line ---- Second line -``` - -Note that a rendered paragraph will have have no line breaks. If you want to -have line breaks, you will need to split the paragraph. Hence, the paragraph -above will be rendered as - -``` -First line Second line -``` - -##### line - -A _line_ starts with `---` and is followed by a non-empty sequence of -_atoms_. - -For instance, the following is a valid _line_: - -``` ---- A ;Pair Int Bool; contains an ;Int; and a ;Bool; -``` - -##### Atom - -An _atom_ is either: - -1. A string of text (including spaces but not line breaks). -2. An inline Juvix expression surrounded by `;`. - -For instance, the following are valid _atoms_: - -1. `I am some text.` -2. `;Pair Int Bool;` - -### Example - -An example is of the following form - -``` ---- >>> someExpression ; -``` - -The `someExpression` can span multiple lines and it must be ended with a `;`. -For instance: - -``` ---- >>> 1 - + 2 - + 3; -``` diff --git a/docs/reference/language/README.md b/docs/reference/language/README.md deleted file mode 100644 index 668612de5..000000000 --- a/docs/reference/language/README.md +++ /dev/null @@ -1,7 +0,0 @@ -- [Functions](./functions.md) -- [Data types](./datatypes.md) -- [Modules](./modules.md) -- [Local definitions](./let.md) -- [Control structures](./control.md) -- [Comments](./comments.md) -- [Axioms](./axioms.md) diff --git a/docs/reference/language/axioms.md b/docs/reference/language/axioms.md deleted file mode 100644 index 332f6a21f..000000000 --- a/docs/reference/language/axioms.md +++ /dev/null @@ -1,20 +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. - -```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. diff --git a/docs/reference/language/builtins.md b/docs/reference/language/builtins.md deleted file mode 100644 index ebe4c7333..000000000 --- a/docs/reference/language/builtins.md +++ /dev/null @@ -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. - - ```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; - ``` diff --git a/docs/reference/language/comments.md b/docs/reference/language/comments.md deleted file mode 100644 index 5479aff78..000000000 --- a/docs/reference/language/comments.md +++ /dev/null @@ -1,18 +0,0 @@ -# Comments - -Comments follow the same syntax as in `Haskell` and `Agda`. Be aware, -Juvix has no support for nested comments. - -- Inline Comment - -```juvix - -- This is a comment! -``` - -- Region comment - -```juvix - {- - This is a comment! - -} -``` diff --git a/docs/reference/language/control.md b/docs/reference/language/control.md deleted file mode 100644 index 943c381db..000000000 --- a/docs/reference/language/control.md +++ /dev/null @@ -1,34 +0,0 @@ -# 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. diff --git a/docs/reference/language/datatypes.md b/docs/reference/language/datatypes.md deleted file mode 100644 index 972e89913..000000000 --- a/docs/reference/language/datatypes.md +++ /dev/null @@ -1,57 +0,0 @@ -# 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/). diff --git a/docs/reference/language/functions.md b/docs/reference/language/functions.md deleted file mode 100644 index d40dfa07a..000000000 --- a/docs/reference/language/functions.md +++ /dev/null @@ -1,93 +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. - -```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}; -``` diff --git a/docs/reference/language/infix.md b/docs/reference/language/infix.md deleted file mode 100644 index 0d93696db..000000000 --- a/docs/reference/language/infix.md +++ /dev/null @@ -1,3 +0,0 @@ -# Infix operators - -TODO diff --git a/docs/reference/language/let.md b/docs/reference/language/let.md deleted file mode 100644 index 841a90c06..000000000 --- a/docs/reference/language/let.md +++ /dev/null @@ -1,18 +0,0 @@ -# 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. diff --git a/docs/reference/language/modules.md b/docs/reference/language/modules.md deleted file mode 100644 index 6c81f3404..000000000 --- a/docs/reference/language/modules.md +++ /dev/null @@ -1,140 +0,0 @@ -# Module system - -Modules are the way in which we split our programs in separate files. Juvix also -supports local modules, which provide a way to better organize different scopes -within a file. - -We call top modules those who are defined at the top of a file. -We call local modules those who are defined inside another module. - -## Top modules - -A module has a name and a body, which comprises a sequence of -[statements](statement.md). - -In order to define a module named `Data.List` we will use the following syntax: - -```juvix -module Data.List; - - -``` - -### Top module naming convention - -Top modules that belong to a [project](project.md) must follow a naming -convention. That is, if `dir` is the root of a project, then the module in -`dir/Data/List.juvix` must be named `Data.List`. - -## _Import_ and _open_ statements - -In order to access the definitions from another modules we use an -_import_ statement. To import some module named `Data.List` we will write - -```juvix -import Data.List; -``` - -Now, we can access the definitions in the imported module using _qualified -names_. E.g., `Data.List.sort`. - -It is possible to import modules and give them a more convinent way thus: - -```juvix -import Data.List as List; -``` - -If we want to access the contents of a module without the need to qualify the -names, we use an _open statement_. The syntax is as follows: - -```juvix -open Data.List; -``` - -Now we can simply write `sort`. It is important to remember that when we open a -module, that module must be in scope, i.e., it must either be imported -or defined as a local module - -Since importing and opening a module is done often, there is special syntax for -that. The following statement: - -```juvix -open import Data.List; -``` - -Is equivalent to this: - -```juvix -import Data.List; -open Data.List; -``` - -When opening a module, if we want to open an explicit subset of its definitions, -we must use the `using` keyword thus: - -```juvix -open Data.List using {List; sort; reverse} -``` - -If we want to open all definitions of a module minus a subset, we -must use the `hiding` keyword thus: - -```juvix -open Data.List hiding {head; tail} -``` - -All opened definitions are available under the current module, but -they are not exported by default. Meaning that if another module imports the current -module, it will only be able to access the definitions defined there but not -those which have been opened. If we want opened definitions to be exported, we -must use the `public` keyword thus: - -``` -module Prelude; - -open import Data.List public; -``` - -Now, from another module we can access definitions in `Data.List` through the -`Prelude` module. - -``` -module MyModule; - -open import Prelude; - --- List, sort, reverse, etc. are now in scope -``` - -## Local modules - -Juvix modules have a hierarchical structure. So far we have discussed top level -modules, which have a one-to-one correspondence with files in the filesystem. On -the other hand, local modules are defined within another module. They can be -useful to group definitions within a file. - -The syntax for local modules is as follows: - -``` -module Path.To.TopModule; - -module Loc; - -end; -``` - -After the definition of a local module, we can access its definitions by using -qualified names. Local modules can be opened by open statements in the same way -as top modules. - -Local modules inherit the scope of the parent module. Some shadowing rules -apply, and they probably follow your intuition: - -1. Opening or defining a symbol shadows inherited instances of that symbol. -2. Opening a symbol does _not_ shadow a defined instanance of that symbol in the - current module. -3. Conversely, defining a symbol in the current module does _not_ shadow an - opened instance of that symbol. - -As a consequence of 2 and 3, using a symbol that is both defined and opened -locally will result in an ambiguity error. diff --git a/docs/reference/language/modules_old.md b/docs/reference/language/modules_old.md deleted file mode 100644 index 28a2ced79..000000000 --- a/docs/reference/language/modules_old.md +++ /dev/null @@ -1,166 +0,0 @@ -# Module system - -## Defining a module - -The `module` keyword starts 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 Juvix project is a collection of Juvix modules inside one main -project folder containing a metadata file named `juvix.yaml`. Each Juvix -file has to define a module of the same name. The name of the -module must coincide with the path of the its file relative to its -project's root directory. For example, if the file is -`root/Data/List.juvix` then the module must be called `Data.List`, -assuming `root` is the project's folder. - -To check that Juvix is correctly detecting your project's root, one can -run the command `juvix dev root File.juvix`. - -## Importing modules - -To bring into the current scope all module definitions from other -external modules, one can use the `import` keyword along with the -corresponding module name. This way, one gets all the imported names -qualified. - -```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 open 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; -``` diff --git a/docs/reference/language/project.md b/docs/reference/language/project.md deleted file mode 100644 index 50d11b81b..000000000 --- a/docs/reference/language/project.md +++ /dev/null @@ -1,37 +0,0 @@ -# Juvix project - -A _juvix project_ is a collection of juvix modules plus some extra metadata -gathered in a `juvix.yaml` file. The most convenient way to create a juvix -project is to run the command `juvix init`. - -A project is rooted in a directory. The root is set by creating a `juvix.yaml`, -which contains the following fields: - -1. **name**: The name of the project. The name must not be empty and cannot - exceed 100 characters. Lower case letters, digits and hyphen `-` are - acceptable characters. The first letter must not be a hyphen. Summarizing, it - must match the following regexp: `[a-z0-9][a-z0-9-]{0,99}`. -2. **version** (_optional_): The version of the project. It must follow the - [SemVer](https://semver.org/) specification. If ommited the version will be - assumed to be _0.0.0_. -3. **dependencies** (_optional_): The dependencies of the project given as a - list. Each dependency is given as relative (or absolute) path to the root of - another juvix project. If the field is ommited, it will be assumed to contain - the juvix standard library as a dependency. - -As intuition would tell, a juvix module belongs to a juvix project if it is -placed in the subtree hanging from the root directory. This rule has two -exceptions: - -1. Modules in a hidden (or hanging from a hidden) directory are not part of the - project. E.g., if the root of a project is `dir`, then the module - `dir/.d/Lib.juvix` does not belong to the project rooted in `dir`. -1. A `juvix.yaml` file shadows other `juvix.yaml` files in parent - directories. E.g. if the root of a project is `dir` and the files - `dir/juvix.yaml` and `dir/nested/juvix.yaml` exist, then the module - `dir/nested/Lib.juvix` would belong to the project in `dir/nested`. - -## Module naming convention - -Modules that belong to a project must follow a naming convention. -See the documentation for [modules](modules.md). diff --git a/docs/reference/language/statement.md b/docs/reference/language/statement.md deleted file mode 100644 index 31ca5b024..000000000 --- a/docs/reference/language/statement.md +++ /dev/null @@ -1,13 +0,0 @@ -# Statement - -A juvix statement is each of the components of a module. -All statements are listed below: - -1. [type definition](datatypes.md). -2. [function definition](functions.md). -3. [axiom definition](axioms.md). -4. [fixity declaration](infix.md). -5. [function definition](functions.md). -6. [open](modules.md). -7. [import](modules.md). -8. [local module](modules.md). diff --git a/docs/reference/stdlib.md b/docs/reference/stdlib.md deleted file mode 100644 index 6199e89e4..000000000 --- a/docs/reference/stdlib.md +++ /dev/null @@ -1,2 +0,0 @@ -The [Juvix standard library](https://anoma.github.io/juvix-stdlib/) -contains common functions that can be used in Juvix programs. diff --git a/docs/reference/tooling/CLI.md b/docs/reference/tooling/CLI.md deleted file mode 100644 index 58612267b..000000000 --- a/docs/reference/tooling/CLI.md +++ /dev/null @@ -1,89 +0,0 @@ -# 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). diff --git a/docs/reference/tooling/README.md b/docs/reference/tooling/README.md deleted file mode 100644 index a9f186a5f..000000000 --- a/docs/reference/tooling/README.md +++ /dev/null @@ -1,4 +0,0 @@ -- [Command line Interface](./CLI.md) -- [Emacs Mode](./emacs.md) -- [Test Suite](./testing.md) -- [Doctor](./doctor.md) diff --git a/docs/reference/tooling/doctor.md b/docs/reference/tooling/doctor.md deleted file mode 100644 index 5c0650729..000000000 --- a/docs/reference/tooling/doctor.md +++ /dev/null @@ -1,123 +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 [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. diff --git a/docs/reference/tooling/emacs.md b/docs/reference/tooling/emacs.md deleted file mode 100644 index 0d90615a5..000000000 --- a/docs/reference/tooling/emacs.md +++ /dev/null @@ -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: - -```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). diff --git a/docs/reference/tooling/testing.md b/docs/reference/tooling/testing.md deleted file mode 100644 index f3b6faeb0..000000000 --- a/docs/reference/tooling/testing.md +++ /dev/null @@ -1,20 +0,0 @@ -# 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/"' -``` diff --git a/docs/tutorials/README.md b/docs/tutorials/README.md deleted file mode 100644 index dbacce882..000000000 --- a/docs/tutorials/README.md +++ /dev/null @@ -1 +0,0 @@ -- [NodeJS Interop](./nodejs-interop.md) diff --git a/docs/tutorials/emacs.md b/docs/tutorials/emacs.md deleted file mode 100644 index ae5bdcb3b..000000000 --- a/docs/tutorials/emacs.md +++ /dev/null @@ -1,79 +0,0 @@ -# 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; -``` diff --git a/docs/tutorials/learn.md b/docs/tutorials/learn.md deleted file mode 100644 index c250a3666..000000000 --- a/docs/tutorials/learn.md +++ /dev/null @@ -1,805 +0,0 @@ -# Juvix tutorial - -- [Juvix REPL](./learn.md#juvix-repl) -- [Basic expressions](./learn.md#basic-expressions) -- [Files, modules and - compilation](./learn.md#files-modules-and-compilation) -- [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: - -```jrepl -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: - -```jrepl -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 - -```jrepl -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: - -```jrepl -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. - -```jrepl -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 'String' type -open import Stdlib.Prelude; - -main : String; -main := "Hello world!"; -``` - -A file compiled to an executable must define the zero-argument -function `main` which is evaluated when running the program. The -definition of `main` can have any non-function type, e.g., `String`, -`Bool` or `Nat`. The generated executable prints the result of -evaluating `main`. - -## Data types and functions - -To see the type of an expression, use the `:type` REPL command: - -```jrepl -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. - -```jrepl -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 2 } -``` - -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 -similar 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: - -```pascal -sum : Nat := 0; - -while (lst /= nil) do -begin - sum := sum + head lst; - lst := tail lst; -end; - -result := 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. - -```pascal -cur : Nat := 0; -next : Nat := 1; - -while (n /= 0) do -begin - tmp := next; - next := cur + next; - cur := tmp; - n := n - 1; -end; - -result := 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 values – -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; -``` - -Since coverage checking forces the user to specify the function for all input values, it may be unclear how to implement functions which are typically partial. For example, the `tail` function on lists is often left undefined for the empty list. One solution is to return a default value. In the Juvix standard library, `tail` is implemented as follows, returning the empty list when the argument is empty. - -```juvix -tail : {A : Type} -> List A -> List A; -tail (_ :: xs) := xs; -tail nil := nil; -``` - -Another solution is to wrap the result in the `Maybe` type from the standard library, which allows to represent optional values. An element of `Maybe A` is either `nothing` or `just x` with `x : A`. - -```juvix -type Maybe (A : Type) := - | nothing : Maybe A - | just : A -> Maybe A; -``` - -For example, one could define the tail function as: - -```juvix -tail' : {A : Type} -> List A -> Maybe (List A) -tail' (_ :: xs) := just xs; -tail' nil := nothing; -``` - -Then the user needs to explicitly check if the result of the function contains a value or not: - -```juvix -case tail' lst -| just x := ... -| nothing := ... -``` - -## 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](./../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`. diff --git a/docs/tutorials/nodejs-interop.md b/docs/tutorials/nodejs-interop.md deleted file mode 100644 index af1f259b4..000000000 --- a/docs/tutorials/nodejs-interop.md +++ /dev/null @@ -1,101 +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. - - -- 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! diff --git a/docs/tutorials/structure.md b/docs/tutorials/structure.md deleted file mode 100644 index e69de29bb..000000000 diff --git a/docs/tutorials/vscode.md b/docs/tutorials/vscode.md deleted file mode 100644 index 4eabac674..000000000 --- a/docs/tutorials/vscode.md +++ /dev/null @@ -1,40 +0,0 @@ -# Juvix VSCode extension tutorial - -To install the [Juvix VSCode extension][vscode-marketplace], 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. - -```juvix -module Hello; - -open import Stdlib.Prelude; - -main : IO; -main := printStringLn "Hello world!"; - -end; -``` - -Syntax should be automatically highlighted for any file with `.juvix` -extension. You can jump to the definition of an identifier by pressing -F12 or control-clicking it. To apply the Juvix code formatter to the -current file, use Shift+Ctrl+I. - -In the top right-hand corner of the editor window you should see several -buttons. Hover the mouse pointer over a button to see its description. -The functions of the buttons are as follows. - -- Load file in REPL (Shift+Alt+R). Launches the Juvix REPL in a - separate window and loads the current file into it. You can then - evaluate any definition from the loaded file. -- Typecheck (Shift+Alt+T). Type-checks the current file. -- Compile (Shift+Alt+C). Compiles the current file. The resulting - native executable will be left in the directory of the file. -- Run (Shift+Alt+X). Compiles and runs the current file. The output of - the executable run is displayed in a separate window. -- Html preview. Generates HTML documentation for the current file and - displays it in a separate window. - -[vscode-marketplace]: https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode