mirror of
https://github.com/anoma/juvix.git
synced 2024-12-01 00:04:58 +03:00
Restructure the documentation and add a tutorial (#1718)
* Closes #1597 * Closes #1624 * Closes #1633 The tutorial uses syntax which has not been implemented yet: it depends on - #1637, - #1716, - #1639, - #1638. The tutorial also assumes the following issues are done: - #1720, and - #1701. Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This commit is contained in:
Łukasz Czajka
GitHub
parent
ecac5e07c7
commit
b95abeaada
18
Makefile
18
Makefile
@ -11,13 +11,15 @@ MDFILES:=$(patsubst docs/org/%,docs/md/%,$(ORGFILES:.org=.md))
|
||||
|
||||
EXAMPLEMILESTONE=examples/milestone
|
||||
EXAMPLEHTMLOUTPUT=_docs/examples/html
|
||||
EXAMPLES= HelloWorld/HelloWorld.juvix \
|
||||
Collatz/Collatz.juvix \
|
||||
Fibonacci/Fibonacci.juvix \
|
||||
Hanoi/Hanoi.juvix \
|
||||
PascalsTriangle/PascalsTriangle.juvix \
|
||||
TicTacToe/CLI/TicTacToe.juvix \
|
||||
ValidityPredicates/SimpleFungibleToken.juvix
|
||||
EXAMPLES= Collatz/Collatz.juvix \
|
||||
Demo/Demo.juvix \
|
||||
Fibonacci/Fibonacci.juvix \
|
||||
Hanoi/Hanoi.juvix \
|
||||
HelloWorld/HelloWorld.juvix \
|
||||
PascalsTriangle/PascalsTriangle.juvix \
|
||||
TicTacToe/CLI/TicTacToe.juvix \
|
||||
Tutorial/Tutorial.juvix \
|
||||
ValidityPredicates/SimpleFungibleToken.juvix
|
||||
|
||||
EXAMPLE_WEBAPP_OUTPUT=_docs/examples/webapp
|
||||
WEBAPP_EXAMPLES=TicTacToe/Web/TicTacToe.juvix
|
||||
@ -67,7 +69,7 @@ html-examples: $(EXAMPLES)
|
||||
$(EXAMPLES):
|
||||
$(eval OUTPUTDIR=$(EXAMPLEHTMLOUTPUT)/$(dir $@))
|
||||
@mkdir -p ${OUTPUTDIR}
|
||||
@juvix html $(EXAMPLEMILESTONE)/$@ --recursive --output-dir=$(CURDIR)/${OUTPUTDIR} --print-metadata
|
||||
@juvix html $(EXAMPLEMILESTONE)/$@ --output-dir=$(CURDIR)/${OUTPUTDIR}
|
||||
|
||||
.PHONY: webapp-examples
|
||||
webapp-examples: $(WEBAPP_EXAMPLES)
|
||||
|
||||
170
README.org
170
README.org
@ -46,158 +46,18 @@ and test Juvix programs, you can use your favorite text editor, the =juvix=
|
||||
command line tool, the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Github Codespace]], and the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Standard Lib Codespace]]. However, we recommend using the =juvix-mode= in [[https://docs.juvix.org/tooling/emacs-mode.html][Emacs]] or the
|
||||
plugin in [[https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode][VSCode]].
|
||||
|
||||
** [[https://github.com/anoma/juvix/tree/main/examples/milestone][First examples of programs written in Juvix]]
|
||||
** Quick start
|
||||
|
||||
The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running =juvix html --recursive FileName.juvix=.
|
||||
|
||||
- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
|
||||
|
||||
The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains
|
||||
common functions that can be used in Juvix programs.
|
||||
|
||||
** Installation
|
||||
|
||||
*** MacOS
|
||||
|
||||
The easiest way to install Juvix on MacOS is by using [[https://brew.sh][Homebrew]].
|
||||
|
||||
To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:
|
||||
|
||||
#+begin_src shell
|
||||
brew tap anoma/juvix
|
||||
#+end_src
|
||||
|
||||
To install Juvix, run:
|
||||
|
||||
#+begin_src shell
|
||||
brew install juvix
|
||||
#+end_src
|
||||
|
||||
|
||||
Helpful information on the shell can also be obtained by running:
|
||||
|
||||
#+begin_src shell
|
||||
brew info juvix
|
||||
#+end_src
|
||||
|
||||
*** Linux x86_64
|
||||
|
||||
A Juvix compiler binary executable for Linux x86_64 is available on the [[https://github.com/anoma/juvix/releases/latest][Juvix release page]].
|
||||
|
||||
To install this executable, downlaod and unzip the linked file and add move it
|
||||
to a directory on your shell's =PATH=.
|
||||
|
||||
For example if =~/.local/bin= is on your shell's =PATH= you can install Juvix as
|
||||
follows:
|
||||
|
||||
#+begin_src shell
|
||||
cd /tmp
|
||||
curl -OL https://github.com/anoma/juvix/releases/download/v0.2.8/juvix-linux_x86_64-v0.2.8.zip
|
||||
unzip juvix-linux_x86_64-v0.2.8.zip
|
||||
mv juvix-linux_x86_64-v0.2.8 ~/.local/bin/juvix
|
||||
#+end_src
|
||||
|
||||
*** Building Juvix from source
|
||||
|
||||
To install Juvix from source you must clone the [[https://github.com/anoma/juvix.git][Github repository]]. Then Juvix
|
||||
can be installed with the following commands. We assume you have [[https://haskellstack.org][Stack]]
|
||||
installed.
|
||||
|
||||
#+begin_src shell
|
||||
git clone --recursive https://github.com/anoma/juvix.git
|
||||
cd juvix
|
||||
stack install
|
||||
#+end_src
|
||||
|
||||
On MacOS you can alternatively run the following command for Homebrew. The flag
|
||||
=--HEAD= used below is optional, use it to build the latest version of Juvix in
|
||||
the =main= branch on Github.
|
||||
|
||||
#+begin_src shell
|
||||
brew install --build-from-source --HEAD juvix --verbose
|
||||
#+end_src
|
||||
|
||||
** Quick Start
|
||||
|
||||
After installation run =juvix --help= to see the list of commands available. See
|
||||
[[https://docs.juvix.org/getting-started/quick-start.html#cli-usage-examples][CLI usage examples]] for descriptions of common tasks.
|
||||
|
||||
Run Juvix doctor to check your system setup:
|
||||
|
||||
#+begin_src shell
|
||||
juvix doctor
|
||||
#+end_src
|
||||
|
||||
*** The Hello World example
|
||||
|
||||
This is the Juvix source code of the traditional Hello World program.
|
||||
|
||||
#+begin_src shell
|
||||
-- HelloWorld.juvix
|
||||
module HelloWorld;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
main : IO;
|
||||
main := putStrLn "hello world!";
|
||||
|
||||
end;
|
||||
#+end_src
|
||||
|
||||
To compile and run a binary generated by Juvix, save the source code to a file
|
||||
called =HelloWorld.juvix= and run the following command from the directory
|
||||
containing it:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile HelloWorld.juvix
|
||||
./HelloWorld
|
||||
#+end_src
|
||||
|
||||
You should see the output: =hello world!=
|
||||
|
||||
The source code can also be compiled to a WebAssembly binary. This requires some
|
||||
additional setup. See [[https://anoma.github.io/juvix/getting-started/dependencies.html][Installing dependencies]] in the documentation for more
|
||||
information. You can also run =juvix doctor= to check your setup.
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile --target wasm HelloWorld.juvix
|
||||
wasmer HelloWorld.wasm
|
||||
#+end_src
|
||||
|
||||
** LSP support
|
||||
|
||||
We provide a sammple =hie.yaml= configuration file for both =cabal= and =stack=.
|
||||
|
||||
If you prefer =stack=, run:
|
||||
#+begin_src shell
|
||||
cp stack.hie.yaml hie.yaml
|
||||
#+end_src
|
||||
If you prefer =cabal=, run:
|
||||
#+begin_src shell
|
||||
cp cabal.hie.yaml hie.yaml
|
||||
#+end_src
|
||||
|
||||
** Building the project with =cabal=
|
||||
|
||||
We recommend that contributors use the =stack= build tool with this project.
|
||||
|
||||
If you would prefer to use the =cabal= build tool instead then you must generate
|
||||
the =juvix.cabal= file using [[https://github.com/sol/hpack][hpack]] before running =cabal build=.
|
||||
See [[./quick-start.md][Quick start]] to start with Juvix.
|
||||
|
||||
** The Juvix programming language
|
||||
|
||||
Juvix allows us to write programs with a high degree of assurance. The Juvix
|
||||
compiler runs several static analyses during the compilation phase to guarantee
|
||||
no runtime errors. Analyses permormed during this phase include scope,
|
||||
termination, arity, and type checkiqng. As a result, functional programs,
|
||||
especially validity predicates, can be written with greater confidence that they
|
||||
will be free of runtime errors.
|
||||
Juvix provides a high degree of assurance. The Juvix compiler runs
|
||||
several static analyses which guarantee the absence of runtime
|
||||
errors. Analyses performed include termination, arity, and type
|
||||
checking. As a result, functional programs, especially validity
|
||||
predicates, can be written with greater confidence in their
|
||||
correctness.
|
||||
|
||||
Some of the language features in Juvix include:
|
||||
|
||||
@ -209,15 +69,11 @@ Some of the language features in Juvix include:
|
||||
- holes in expressions
|
||||
- axioms for non-computable terms
|
||||
|
||||
Additionally, the foreign and compile blocks syntax enable developers to compile
|
||||
a program to different backends including the =C= language. The Juvix module
|
||||
system further permits splitting programs into several modules to build
|
||||
libraries which can be later documented by generating HTML files based on the
|
||||
codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the Juvix
|
||||
standard library's website]]. For futher details, please refer to
|
||||
[[https://anoma.github.io/juvix/][the Juvix book]] which includes our
|
||||
[[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].
|
||||
|
||||
The Juvix module system further permits splitting programs into
|
||||
several modules to build libraries which can be later documented by
|
||||
generating HTML files based on the codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the
|
||||
Juvix standard library's website]]. For further details, please refer to
|
||||
[[https://anoma.github.io/juvix/][the Juvix book]] which includes our [[https://anoma.github.io/juvix/changelog.html][latest updates]].
|
||||
|
||||
** Community
|
||||
|
||||
|
||||
64
docs/org/SUMMARY.org
Executable file → Normal file
64
docs/org/SUMMARY.org
Executable file → Normal file
@ -2,34 +2,44 @@
|
||||
|
||||
- [[./README.md][The Juvix project]]
|
||||
- [[./changelog.md][Changelog]]
|
||||
- [[./getting-started/README.md][Getting started]]
|
||||
- [[./getting-started/quick-start.md][Quick start]]
|
||||
- [[./getting-started/dependencies.md][Installing dependencies]]
|
||||
- [[./examples/README.md][Juvix Examples]]
|
||||
- [[./tutorials/README.md][Tutorials]]
|
||||
- [[./tutorials/nodejs-interop.md][NodeJS Interop]]
|
||||
- [[./quick-start.md][Quick start]]
|
||||
|
||||
- [[./language-reference/README.md][Language reference]]
|
||||
- [[./language-reference/comments.md][Comments]]
|
||||
- [[./language-reference/axiom.md][Axiom]]
|
||||
- [[./language-reference/compile-blocks.md][Compile block]]
|
||||
- [[./language-reference/modules.md][Module]]
|
||||
- [[./language-reference/inductive-data-types.md][Data type]]
|
||||
- [[./language-reference/functions.md][Function]]
|
||||
- [[./language-reference/foreign-blocks.md][Foreign block]]
|
||||
- [[./language-reference/termination-checking.md][Termination]]
|
||||
* Tutorials
|
||||
- [[./tutorials/learn.md][Learn Juvix in minutes]]
|
||||
- [[./tutorials/structure.md][Structuring Juvix projects]]
|
||||
- [[./tutorials/emacs.md][Juvix Emacs mode]]
|
||||
- [[./tutorials/vscode.md][Juvix VSCode extension]]
|
||||
|
||||
- [[./tooling/README.md][Tooling]]
|
||||
- [[./tooling/CLI.md][Command line interface]]
|
||||
- [[./tooling/doctor.md][Doctor]]
|
||||
- [[./tooling/emacs-mode.md][Emacs mode]]
|
||||
- [[./tooling/testing.md][Haskell test suite]]
|
||||
* How-to guides
|
||||
- [[./howto/installing.md][Installing Juvix]]
|
||||
- [[./howto/compilation.md][Compiling Juvix programs]]
|
||||
- [[./howto/judoc.md][Judoc: Juvix documentation tool]]
|
||||
|
||||
- [[./notes/README.md][Notes]]
|
||||
- [[./notes/runtime-benchmark-results.md][Runtime benchmark results]]
|
||||
- [[./notes/monomorphization.md][Monomorphization]]
|
||||
- [[./examples/validity-predicates/README.md][Validity predicates]]
|
||||
- [[./notes/strictly-positive-data-types.md][Strictly positive data types]]
|
||||
* Explanations
|
||||
- [[./explanations/typetheory.md][Type theory]]
|
||||
- [[./explanations/totality/README.md][Totality checking]]
|
||||
- [[./explanations/totality/termination.md][Termination]]
|
||||
- [[./explanations/totality/positive.md][Strictly positive data types]]
|
||||
- [[./explanations/totality/coverage.md][Coverage checking]]
|
||||
|
||||
- [[./README.md][About]]
|
||||
- [[./introduction/about/community.md][Community]]
|
||||
* Reference
|
||||
- [[./reference/stdlib.md][Standard library]]
|
||||
- [[./reference/language/README.md][Language reference]]
|
||||
- [[./reference/language/functions.md][Functions]]
|
||||
- [[./reference/language/datatypes.md][Data types]]
|
||||
- [[./reference/language/modules.md][Modules]]
|
||||
- [[./reference/language/comments.md][Comments]]
|
||||
- [[./reference/language/axioms.md][Axioms]]
|
||||
- [[./reference/language/compileblocks.md][Compile blocks]]
|
||||
- [[./reference/language/foreign.md][Foreign blocks]]
|
||||
- [[./reference/examples.md][Example programs]]
|
||||
- [[./reference/benchmarks.md][Benchmarks]]
|
||||
- [[./reference/tooling/README.md][Tooling]]
|
||||
- [[./reference/tooling/CLI.md][Command line interface]]
|
||||
- [[./reference/tooling/doctor.md][Doctor]]
|
||||
- [[./reference/tooling/emacs.md][Emacs mode]]
|
||||
- [[./reference/tooling/testing.md][Haskell test suite]]
|
||||
- [[./reference/judoc.md][Judoc reference]]
|
||||
|
||||
* About
|
||||
- [[./about/community.md][Community]]
|
||||
|
||||
@ -1 +0,0 @@
|
||||
- [[./minic.md][MiniC backend]]
|
||||
@ -1 +0,0 @@
|
||||
* MiniC Backend
|
||||
@ -1 +0,0 @@
|
||||
* Abstract Internal Language
|
||||
@ -1 +0,0 @@
|
||||
* Concrete Internal Language
|
||||
@ -1 +0,0 @@
|
||||
* MicroJuvix Internal Language
|
||||
@ -1,7 +0,0 @@
|
||||
* Internal Juvix languages
|
||||
|
||||
** Languages
|
||||
|
||||
- [[./language/abstract.md][Abstract Language]]
|
||||
- [[./language/concrete.md][Concrete language]]
|
||||
- [[./language/microjuvix.md][MicroJuvix Language]]
|
||||
@ -1 +0,0 @@
|
||||
* Pipeline
|
||||
0
docs/org/examples/README.org
Executable file → Normal file
0
docs/org/examples/README.org
Executable file → Normal file
@ -1,2 +0,0 @@
|
||||
- [[./quick-start.md][Quick start]]
|
||||
- [[./dependencies.md][Installing dependencies]]
|
||||
@ -1,38 +0,0 @@
|
||||
|
||||
* Installing dependencies
|
||||
|
||||
The following dependencies are only required for compiling to WASM.
|
||||
|
||||
- [[https://wasmer.io][wasmer]]
|
||||
- [[https://releases.llvm.org/download.html][Clang / LLVM]] version 13 or later (NB: On macOS the preinstalled clang does not support the wasm
|
||||
target so use =brew install llvm= instead for example)
|
||||
- [[https://github.com/WebAssembly/wasi-sdk/releases][wasi-sdk]]
|
||||
- [[https://lld.llvm.org][wasm-ld]] - the LLVM linker for WASM (NB: On linux you may need to install the
|
||||
=lld= package, on macOS this is installed as part of =llvm=).
|
||||
|
||||
To install =wasi-sdk= you need to download =libclang_rt= and =wasi-sysroot=
|
||||
precompiled archives from the [[https://github.com/WebAssembly/wasi-sdk/releases/][wasi-sdk release page]] and:
|
||||
|
||||
1. Extract the =libclang_rt.builtins-wasm32-wasi-*.tar.gz= archive in the
|
||||
=clang= installation root (for example =/usr/lib/clang/13= on Ubuntu or
|
||||
=`brew --prefix llvm`= on macos).
|
||||
|
||||
For example on macos with homebrew clang:
|
||||
|
||||
#+begin_src shell
|
||||
cd `brew --prefix llvm`
|
||||
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/libclang_rt.builtins-wasm32-wasi-15.0.tar.gz -OL
|
||||
tar xf libclang_rt.builtins-wasm32-wasi-15.0.tar.gz
|
||||
#+end_src
|
||||
|
||||
2. Extract the =wasi-sysroot-*.tar.gz= archive on your local system and set
|
||||
=WASI_SYSROOT_PATH= to its path.
|
||||
|
||||
For example:
|
||||
|
||||
#+begin_src shell
|
||||
cd ~
|
||||
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/wasi-sysroot-15.0.tar.gz -OL
|
||||
tar xf wasi-sysroot-15.0.tar.gz
|
||||
export WASI_SYSROOT_PATH=~/wasi-sysroot
|
||||
#+end_src
|
||||
@ -1,58 +0,0 @@
|
||||
* Quick Start
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/anoma/juvix">
|
||||
<img align="left" width="200" height="200" alt="Juvix Mascot" src="../assets/images/tara-teaching.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
|
||||
To install Juvix, you can download its sources using
|
||||
[[http://git-scm.com/][Git]] from the
|
||||
[[https://github.com/anoma/juvix.git][Github repository]]. Then, the
|
||||
program can be downloaded and installed with the following commands. You
|
||||
will need to have [[https://haskellstack.org][Stack]] installed.
|
||||
|
||||
#+begin_src shell
|
||||
git clone --recursive https://github.com/anoma/juvix.git
|
||||
cd juvix
|
||||
stack install
|
||||
#+end_src
|
||||
|
||||
If the installation succeeds, you must be able to run the Juvix
|
||||
command from any location.
|
||||
|
||||
|
||||
To get the complete list of commands, please run =juvix --help=.
|
||||
|
||||
** CLI Usage Examples
|
||||
|
||||
Create a new package:
|
||||
|
||||
#+begin_src shell
|
||||
juvix init
|
||||
#+end_src
|
||||
|
||||
Compile a source file into an executable:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Compile a source file into a WebAssembly binary:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile -t wasm path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Typecheck a source file:
|
||||
|
||||
#+begin_src shell
|
||||
juvix typecheck path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Generate HTML representations of a source file and its imports:
|
||||
|
||||
#+begin_src shell
|
||||
juvix html --recursive path/to/source.juvix
|
||||
#+end_src
|
||||
119
docs/org/howto/installing.org
Normal file
119
docs/org/howto/installing.org
Normal file
@ -0,0 +1,119 @@
|
||||
|
||||
* Dependencies
|
||||
|
||||
You need [[https://releases.llvm.org/download.html][Clang / LLVM]] version 13 or later. Note that on macOS the preinstalled clang does not support the wasm target, so use e.g. =brew install llvm= instead.
|
||||
|
||||
If you want to compile to WebAssembly, you also need:
|
||||
- [[https://wasmer.io][wasmer]]
|
||||
- [[https://github.com/WebAssembly/wasi-sdk/releases][wasi-sdk]]
|
||||
- [[https://lld.llvm.org][wasm-ld]] - the LLVM linker for WASM (NB: On Linux you may need to install the
|
||||
=lld= package; on macOS this is installed as part of =llvm=).
|
||||
|
||||
See [[./installing.md#installing-dependencies][below]] for instructions on how to install the dependencies.
|
||||
|
||||
* Installing Juvix
|
||||
|
||||
*** MacOS
|
||||
|
||||
The easiest way to install Juvix on MacOS is by using [[https://brew.sh][Homebrew]].
|
||||
|
||||
To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:
|
||||
|
||||
#+begin_src shell
|
||||
brew tap anoma/juvix
|
||||
#+end_src
|
||||
|
||||
To install Juvix, run:
|
||||
|
||||
#+begin_src shell
|
||||
brew install juvix
|
||||
#+end_src
|
||||
|
||||
|
||||
Helpful information can also be obtained by running:
|
||||
|
||||
#+begin_src shell
|
||||
brew info juvix
|
||||
#+end_src
|
||||
|
||||
*** Linux x86_64
|
||||
|
||||
A Juvix compiler binary executable for Linux x86_64 is available on the [[https://github.com/anoma/juvix/releases/latest][Juvix release page]].
|
||||
|
||||
To install this executable, download and unzip the linked file and move it
|
||||
to a directory on your shell's =PATH=.
|
||||
|
||||
For example if =~/.local/bin= is on your shell's =PATH=, you can install Juvix as
|
||||
follows:
|
||||
|
||||
#+begin_src shell
|
||||
cd /tmp
|
||||
curl -OL https://github.com/anoma/juvix/releases/download/v0.2.8/juvix-linux_x86_64-v0.2.8.zip
|
||||
unzip juvix-linux_x86_64-v0.2.8.zip
|
||||
mv juvix-linux_x86_64-v0.2.8 ~/.local/bin/juvix
|
||||
#+end_src
|
||||
|
||||
*** Building Juvix from source
|
||||
|
||||
To install Juvix from source you must clone the [[https://github.com/anoma/juvix.git][Github repository]]. Then Juvix can be installed with the following commands. We assume you have [[https://haskellstack.org][Stack]] and [[https://www.gnu.org/software/make/][GNU Make]] installed.
|
||||
|
||||
#+begin_src shell
|
||||
git clone --recursive https://github.com/anoma/juvix.git
|
||||
cd juvix
|
||||
make install
|
||||
#+end_src
|
||||
|
||||
The C compiler and linker paths can be specified as options to the =make install= command, e.g.
|
||||
#+begin_src shell
|
||||
make install CC=path/to/clang LIBTOOL=path/to/llvm-ar
|
||||
#+end_src
|
||||
|
||||
On MacOS, you can alternatively run the following command for Homebrew. The flag
|
||||
=--HEAD= used below is optional -- use it to build the latest version of Juvix in
|
||||
the =main= branch on Github.
|
||||
|
||||
#+begin_src shell
|
||||
brew install --build-from-source --HEAD juvix --verbose
|
||||
#+end_src
|
||||
|
||||
*** Building the project with =cabal=
|
||||
|
||||
We recommend to use the =stack= build tool with this project.
|
||||
|
||||
If you prefer the =cabal= build tool instead, then you need to generate
|
||||
the =juvix.cabal= file using [[https://github.com/sol/hpack][hpack]] before running =cabal build=.
|
||||
|
||||
You also need to compile the runtime first:
|
||||
#+begin_src shell
|
||||
make runtime
|
||||
cabal build
|
||||
#+end_src
|
||||
|
||||
* Installing dependencies
|
||||
|
||||
To install =wasi-sdk= you need to download =libclang_rt= and =wasi-sysroot=
|
||||
precompiled archives from the [[https://github.com/WebAssembly/wasi-sdk/releases/][wasi-sdk release page]] and:
|
||||
|
||||
1. Extract the =libclang_rt.builtins-wasm32-wasi-*.tar.gz= archive in the
|
||||
=clang= installation root (for example =/usr/lib/clang/13= on Ubuntu or
|
||||
=`brew --prefix llvm`= on macos).
|
||||
|
||||
For example on macos with homebrew clang:
|
||||
|
||||
#+begin_src shell
|
||||
cd `brew --prefix llvm`
|
||||
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/libclang_rt.builtins-wasm32-wasi-15.0.tar.gz -OL
|
||||
tar xf libclang_rt.builtins-wasm32-wasi-15.0.tar.gz
|
||||
#+end_src
|
||||
|
||||
2. Extract the =wasi-sysroot-*.tar.gz= archive on your local system and set
|
||||
=WASI_SYSROOT_PATH= to its path.
|
||||
|
||||
For example:
|
||||
|
||||
#+begin_src shell
|
||||
cd ~
|
||||
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/wasi-sysroot-15.0.tar.gz -OL
|
||||
tar xf wasi-sysroot-15.0.tar.gz
|
||||
export WASI_SYSROOT_PATH=~/wasi-sysroot
|
||||
#+end_src
|
||||
@ -1,8 +0,0 @@
|
||||
- [[./comments.md][Comments]]
|
||||
- [[./axiom.md][Axiom]]
|
||||
- [[./functions.md][Function]]
|
||||
- [[./modules.md][Module System]]
|
||||
- [[./inductive-data-types.md][Inductive data type]]
|
||||
- [[./termination-checking.md][Termination checking]]
|
||||
- [[./compile-blocks.md][Compile block]]
|
||||
- [[./foreign-blocks.md][Foreign block]]
|
||||
@ -1,56 +0,0 @@
|
||||
* Inductive data types
|
||||
|
||||
The =inductive= keyword is reserved for declaring inductive data types. An
|
||||
inductive type declaration requires a unique name for its type and a non-empty
|
||||
list of constructor declarations, functions for building the terms of the
|
||||
inductive data type. Constructors can be used as normal identifiers and also in
|
||||
patterns. As shown later, one can also provide type parameters to widen the
|
||||
family of inductive types one can define in Juvix.
|
||||
|
||||
The simplest inductive type is the =Unit= type with one constructor called =unit=.
|
||||
|
||||
#+begin_example
|
||||
type Unit := unit : Unit;
|
||||
#+end_example
|
||||
|
||||
In the following example, we declare the inductive type =Nat=, the unary
|
||||
representation of natural numbers. This type comes with two data constructors,
|
||||
namely =zero= and =suc=. A term of the type =Nat= is the number one, represented
|
||||
by =suc zero= or the number two represented by =suc (suc zero)=, etc.
|
||||
|
||||
#+begin_example
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| suc : Nat -> Nat;
|
||||
#+end_example
|
||||
|
||||
The way to use inductive types is by declaring functions by pattern matching.
|
||||
Let us define, for example, the function for adding two natural numbers.
|
||||
|
||||
#+begin_src text
|
||||
inifl 6 +;
|
||||
+ : Nat -> Nat -> Nat;
|
||||
+ zero b := b;
|
||||
+ (suc a) b := suc (a + b);
|
||||
#+end_src
|
||||
|
||||
As mentioned earlier, an inductive type may have type parameters. The canonical
|
||||
example is the polymorphic type =List=. The type =List= is the inductive type that
|
||||
considers the type of the elements in the list as a parameter. A constructor to
|
||||
build the empty list, that is the base case, and another constructor to enlarge
|
||||
the list, we usually called it =cons=. One possible definition for this type is
|
||||
the following type taken from the Juvix standard library:
|
||||
|
||||
#+begin_example
|
||||
infixr 5 ::;
|
||||
type List (A : Type) :=
|
||||
nil : List A
|
||||
| :: : A -> List A -> List A;
|
||||
|
||||
elem : {A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
|
||||
elem _ _ nil := false;
|
||||
elem eq s (x :: xs) := eq s x || elem eq s xs;
|
||||
#+end_example
|
||||
|
||||
To see more examples of inductive types and how to use them, please check out
|
||||
[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]]
|
||||
12
docs/org/notes/lsp.org
Normal file
12
docs/org/notes/lsp.org
Normal file
@ -0,0 +1,12 @@
|
||||
* LSP support
|
||||
|
||||
We provide a sample =hie.yaml= configuration file for both =cabal= and =stack=.
|
||||
|
||||
If you prefer =stack=, run:
|
||||
#+begin_src shell
|
||||
cp stack.hie.yaml hie.yaml
|
||||
#+end_src
|
||||
If you prefer =cabal=, run:
|
||||
#+begin_src shell
|
||||
cp cabal.hie.yaml hie.yaml
|
||||
#+end_src
|
||||
89
docs/org/quick-start.org
Normal file
89
docs/org/quick-start.org
Normal file
@ -0,0 +1,89 @@
|
||||
* Quick Start
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/anoma/juvix">
|
||||
<img align="left" width="200" height="200" alt="Juvix Mascot" src="assets/images/tara-teaching.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
To install Juvix, follow the instruction in the [[./howto/installing.md][Installation How-to]].
|
||||
|
||||
After installation, run =juvix --help= to see the list of commands.
|
||||
|
||||
Run Juvix doctor to check your system setup:
|
||||
|
||||
#+begin_src shell
|
||||
juvix doctor
|
||||
#+end_src
|
||||
|
||||
** CLI Usage Examples
|
||||
|
||||
Create a new package:
|
||||
|
||||
#+begin_src shell
|
||||
juvix init
|
||||
#+end_src
|
||||
|
||||
Compile a source file into an executable:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Compile a source file into a WebAssembly binary:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile -t wasm path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Launch the REPL:
|
||||
|
||||
#+begin_src shell
|
||||
juvix repl
|
||||
#+end_src
|
||||
|
||||
Typecheck a source file:
|
||||
|
||||
#+begin_src shell
|
||||
juvix typecheck path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
Generate HTML representations of a source file and its imports:
|
||||
|
||||
#+begin_src shell
|
||||
juvix html --recursive path/to/source.juvix
|
||||
#+end_src
|
||||
|
||||
** The Hello World example
|
||||
|
||||
This is the Juvix source code of the traditional Hello World program.
|
||||
|
||||
#+begin_src shell
|
||||
-- HelloWorld.juvix
|
||||
module HelloWorld;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
main : IO;
|
||||
main := printStringLn "hello world!";
|
||||
|
||||
end;
|
||||
#+end_src
|
||||
|
||||
To compile and run a binary generated by Juvix, save the source code to a file
|
||||
called =HelloWorld.juvix= and run the following command from the directory
|
||||
containing it:
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile HelloWorld.juvix
|
||||
./HelloWorld
|
||||
#+end_src
|
||||
|
||||
You should see the output: =hello world!=
|
||||
|
||||
The source code can also be compiled to a WebAssembly binary. This requires some additional setup. See the [[https://anoma.github.io/juvix/howto/installing.html][Installation How-to]] for more information. You can also run =juvix doctor= to check your setup.
|
||||
|
||||
#+begin_src shell
|
||||
juvix compile --target wasm HelloWorld.juvix
|
||||
wasmer HelloWorld.wasm
|
||||
#+end_src
|
||||
9
docs/org/reference/examples.org
Normal file
9
docs/org/reference/examples.org
Normal file
@ -0,0 +1,9 @@
|
||||
The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running =juvix html --recursive FileName.juvix=.
|
||||
|
||||
- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
|
||||
- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
|
||||
7
docs/org/reference/language/README.org
Normal file
7
docs/org/reference/language/README.org
Normal file
@ -0,0 +1,7 @@
|
||||
- [[./functions.md][Functions]]
|
||||
- [[./datatypes.md][Data types]]
|
||||
- [[./modules.md][Modules]]
|
||||
- [[./comments.md][Comments]]
|
||||
- [[./axioms.md][Axioms]]
|
||||
- [[./compileblocks.md][Compile blocks]]
|
||||
- [[./foreign.md][Foreign blocks]]
|
||||
@ -8,7 +8,7 @@ $A$ is a type, and there exists a term $x$ that inhabits $A$. Then the program w
|
||||
-- Example.juvix
|
||||
module Example;
|
||||
axiom A : Type;
|
||||
axom x : A;
|
||||
axiom x : A;
|
||||
end;
|
||||
#+end_src
|
||||
|
||||
2
docs/org/language-reference/builtins.org → docs/org/reference/language/builtins.org
Executable file → Normal file
2
docs/org/language-reference/builtins.org → docs/org/reference/language/builtins.org
Executable file → Normal file
@ -15,7 +15,7 @@ Juvix has support for the built-in natural type and a few functions that are com
|
||||
2. Builtin function definitions.
|
||||
|
||||
#+begin_example
|
||||
inifl 6 +;
|
||||
infixl 6 +;
|
||||
builtin nat-plus
|
||||
+ : Nat → Nat → Nat;
|
||||
+ zero b := b;
|
||||
@ -1,6 +1,6 @@
|
||||
* Comments
|
||||
|
||||
A comment is introduced in the same fashion as in =Haskell=/=Agda=.
|
||||
Comments follow the same syntax as in =Haskell= and =Agda=. Be aware, Juvix has no support for nested comments.
|
||||
|
||||
- Inline Comment
|
||||
#+begin_src
|
||||
4
docs/org/language-reference/compile-blocks.org → docs/org/reference/language/compileblocks.org
Executable file → Normal file
4
docs/org/language-reference/compile-blocks.org → docs/org/reference/language/compileblocks.org
Executable file → Normal file
@ -49,14 +49,14 @@ compile Action {
|
||||
- A compile block must be in the same module as their name definition.
|
||||
|
||||
#+begin_src haskell
|
||||
$ cat A.mjuvix
|
||||
$ cat A.juvix
|
||||
...
|
||||
axiom Action : Type;
|
||||
...
|
||||
#+end_src
|
||||
|
||||
#+begin_src haskell
|
||||
$ cat B.mjuvix
|
||||
$ cat B.juvix
|
||||
...
|
||||
compile Action {
|
||||
c -> "int";
|
||||
50
docs/org/reference/language/datatypes.org
Normal file
50
docs/org/reference/language/datatypes.org
Normal file
@ -0,0 +1,50 @@
|
||||
* Data types
|
||||
|
||||
A data type declaration consists of:
|
||||
- the =type= keyword,
|
||||
- a unique name for the type,
|
||||
- the =:== symbol,
|
||||
- a non-empty list of constructor declarations -- functions for building the elements of the data type.
|
||||
|
||||
The simplest data type is the =Unit= type with one constructor called =unit=.
|
||||
|
||||
#+begin_example
|
||||
type Unit := unit : Unit;
|
||||
#+end_example
|
||||
|
||||
In the following example, we declare the type =Nat= -- the unary
|
||||
representation of natural numbers. This type comes with two constructors: =zero= and =suc=. Example elements of type =Nat= are the number one represented
|
||||
by =suc zero=, the number two represented by =suc (suc zero)=, etc.
|
||||
|
||||
#+begin_example
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| suc : Nat -> Nat;
|
||||
#+end_example
|
||||
|
||||
Constructors can be used like normal functions or in patterns when defining functions by pattern matching. For example, here is a function adding two natural numbers:
|
||||
|
||||
#+begin_src text
|
||||
infixl 6 +;
|
||||
+ : Nat -> Nat -> Nat;
|
||||
+ zero b := b;
|
||||
+ (suc a) b := suc (a + b);
|
||||
#+end_src
|
||||
|
||||
A data type may have type parameters. A data type with a type
|
||||
parameter =A= is called /polymorphic in/ =A=. A canonical example is
|
||||
the type =List= polymorphic in the type of list elements.
|
||||
|
||||
#+begin_example
|
||||
infixr 5 ::;
|
||||
type List (A : Type) :=
|
||||
nil : List A
|
||||
| :: : A -> List A -> List A;
|
||||
|
||||
elem : {A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
|
||||
elem _ _ nil := false;
|
||||
elem eq s (x :: xs) := eq s x || elem eq s xs;
|
||||
#+end_example
|
||||
|
||||
For more examples of inductive types and how to use them, see
|
||||
[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]].
|
||||
@ -9,7 +9,6 @@ The following is an example taken from the Juvix standard library.
|
||||
|
||||
#+begin_example
|
||||
module Integers;
|
||||
|
||||
axiom Int : Type;
|
||||
compile Int { c -> "int" };
|
||||
|
||||
@ -28,8 +27,4 @@ axiom <' : Int -> Int -> Bool;
|
||||
compile <' {
|
||||
c -> "lessThan";
|
||||
};
|
||||
|
||||
infix 4 <;
|
||||
< : Int -> Int -> Bool;
|
||||
< a b := from-backend-bool (a <' b);
|
||||
#+end_example
|
||||
@ -1,9 +1,8 @@
|
||||
* Function declaration
|
||||
* Function declarations
|
||||
|
||||
A function declaration is a type signature /and/ a group of definitions called
|
||||
/function clauses/.
|
||||
A function declaration consists of a type signature and a group of /function clauses/.
|
||||
|
||||
In the following example we define a function called =multiplyByTwo=. The first
|
||||
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.
|
||||
|
||||
@ -27,13 +26,13 @@ neg true := false;
|
||||
neg false := true;
|
||||
#+end_example
|
||||
|
||||
When =neg= is called with =true= the first clause is used and the function
|
||||
returns =false=. Similarly, when =neg= is called with =false= the second clause
|
||||
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 others 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=.
|
||||
Function declarations can depend on each other recursively. In the following example, we define a function that checks if a number is =even= by calling a function that checks if a number is =odd=.
|
||||
|
||||
#+begin_example
|
||||
open import Stdlib.Prelude;
|
||||
4
docs/org/language-reference/modules.org → docs/org/reference/language/modules.org
Executable file → Normal file
4
docs/org/language-reference/modules.org → docs/org/reference/language/modules.org
Executable file → Normal file
@ -17,7 +17,7 @@ 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 respect to its project. For example, if the file is
|
||||
=root/Data/List.juvix= then the module must be called =Data.List=, assumming
|
||||
=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
|
||||
@ -138,7 +138,7 @@ end;
|
||||
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 corresponing =open=
|
||||
module, one can use the =public= keyword at the end of the corresponding =open=
|
||||
statement. For example, in module =B=, after marking the import of =A= as
|
||||
=public=, the module =C= typechecks.
|
||||
|
||||
2
docs/org/reference/stdlib.org
Normal file
2
docs/org/reference/stdlib.org
Normal file
@ -0,0 +1,2 @@
|
||||
|
||||
The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains common functions that can be used in Juvix programs.
|
||||
@ -10,8 +10,6 @@ juvix [Global options] ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CM
|
||||
|
||||
- =-v,--version=
|
||||
Print the version and exit
|
||||
- =--show-root=
|
||||
Print the detected root of the project
|
||||
- =-h,--help=
|
||||
Show this help text
|
||||
|
||||
@ -65,8 +63,6 @@ juvix dev COMMAND
|
||||
Subcommands related to JuvixCore
|
||||
- =asm=
|
||||
Subcommands related to JuvixAsm
|
||||
- =doc=
|
||||
Generate documentation
|
||||
- =root=
|
||||
Show the root path for a Juvix project
|
||||
- =termination=
|
||||
@ -74,7 +70,7 @@ juvix dev COMMAND
|
||||
- =internal=
|
||||
Subcommands related to Internal
|
||||
- =minic=
|
||||
Translate a Juvix file to MiniC
|
||||
Translate a Juvix file to a subset of C
|
||||
|
||||
** CLI Auto-completion Scripts
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
- [[./CLI.md][Command line Interface]]
|
||||
- [[./emacs-mode.md][Writting Juvix programs with Emacs Mode]]
|
||||
- [[./emacs.md][Emacs Mode]]
|
||||
- [[./testing.md][Test Suite]]
|
||||
- [[./doctor.md][Doctor]]
|
||||
@ -34,7 +34,7 @@ sudo pacman -S llvm lld
|
||||
|
||||
The Juvix compiler required =wasm-ld= (the Wasm linker) to produce =Wasm= binaries.
|
||||
|
||||
Recommened installation method:
|
||||
Recommended installation method:
|
||||
|
||||
*** MacOS
|
||||
|
||||
0
docs/org/tutorials/emacs.org
Normal file
0
docs/org/tutorials/emacs.org
Normal file
512
docs/org/tutorials/learn.org
Normal file
512
docs/org/tutorials/learn.org
Normal file
@ -0,0 +1,512 @@
|
||||
* Juvix tutorial
|
||||
|
||||
NOTE: This is a tutorial for Juvix version 0.3. Earlier versions do not support all of the syntax described here.
|
||||
|
||||
* [[./learn.md#juvix-repl][Juvix REPL]]
|
||||
* [[./learn.md#basic-expressions][Basic expressions]]
|
||||
* [[./learn.md#files-modules-and-compilation][Files, modules and compilation]]
|
||||
* [[./learn.md#output][Output]]
|
||||
* [[./learn.md#data-types-and-functions][Data types and functions]]
|
||||
* [[./learn.md#pattern-matching][Pattern matching]]
|
||||
* [[./learn.md#comparisons-and-conditionals][Comparisons and conditionals]]
|
||||
* [[./learn.md#local-definitions][Local definitions]]
|
||||
* [[./learn.md#recursion][Recursion]]
|
||||
* [[./learn.md#partial-application-and-higher-order-functions][Partial application and higher-order functions]]
|
||||
* [[./learn.md#polymorphism][Polymorphism]]
|
||||
* [[./learn.md#tail-recursion][Tail recursion]]
|
||||
* [[./learn.md#totality-checking][Totality checking]]
|
||||
* [[./learn.md#exercises][Exercises]]
|
||||
|
||||
** Juvix REPL
|
||||
|
||||
After [[../howto/installing.md][installing Juvix]], launch the Juvix REPL:
|
||||
|
||||
#+begin_src shell
|
||||
juvix repl
|
||||
#+end_src
|
||||
|
||||
The response should be similar to:
|
||||
#+begin_example
|
||||
Juvix REPL version 0.3: https://juvix.org. Run :help for help
|
||||
OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
|
||||
Stdlib.Prelude>
|
||||
#+end_example
|
||||
|
||||
Currently, the REPL supports evaluating expressions but it does not yet support adding new definitions. To see the list of available REPL commands type =:help=.
|
||||
|
||||
** Basic expressions
|
||||
|
||||
You can try evaluating simple arithmetic expressions in the REPL:
|
||||
#+begin_example
|
||||
Stdlib.Prelude> 3 + 4
|
||||
7
|
||||
Stdlib.Prelude> 1 + 3 * 7
|
||||
22
|
||||
Stdlib.Prelude> div 35 4
|
||||
8
|
||||
Stdlib.Prelude> mod 35 4
|
||||
3
|
||||
Stdlib.Prelude> sub 35 4
|
||||
31
|
||||
Stdlib.Prelude> sub 4 35
|
||||
0
|
||||
#+end_example
|
||||
By default Juvix operates on nonnegative natural numbers. Natural number subtraction is implemented by the function =sub=. Subtracting a bigger natural number from a smaller one yields =0=.
|
||||
|
||||
You can also try boolean expressions
|
||||
#+begin_example
|
||||
Stdlib.Prelude> true
|
||||
true
|
||||
Stdlib.Prelude> not true
|
||||
false
|
||||
Stdlib.Prelude> true && false
|
||||
false
|
||||
Stdlib.Prelude> true || false
|
||||
true
|
||||
Stdlib.Prelude> if true 1 0
|
||||
1
|
||||
#+end_example
|
||||
and strings, pairs and lists:
|
||||
#+begin_example
|
||||
Stdlib.Prelude> "Hello world!"
|
||||
"Hello world!"
|
||||
Stdlib.Prelude> (1, 2)
|
||||
(1, 2)
|
||||
Stdlib.Prelude> 1 :: 2 :: nil
|
||||
1 :: 2 :: nil
|
||||
#+end_example
|
||||
|
||||
In fact, you can use all functions and types from the [[https://anoma.github.io/juvix-stdlib/Stdlib.Prelude.html][Stdlib.Prelude]] module of the [[https://anoma.github.io/juvix-stdlib][standard library]], which is preloaded by default.
|
||||
|
||||
#+begin_example
|
||||
Stdlib.Prelude> length (1 :: 2 :: nil)
|
||||
3
|
||||
Stdlib.Prelude> null (1 :: 2 :: nil)
|
||||
false
|
||||
Stdlib.Prelude> swap (1, 2)
|
||||
(2, 1)
|
||||
#+end_example
|
||||
|
||||
** Files, modules and compilation
|
||||
|
||||
Currently, the REPL does not support adding new definitions. To define new functions or data types, you need to put them in a separate file and either load the file in the REPL with =:load file.juvix= or compile the file to a binary executable with the shell command =juvix compile file.juvix=.
|
||||
|
||||
To conveniently edit Juvix files, an [[./emacs.md][Emacs mode]] and a [[./vscode.md][VSCode extension]] are available.
|
||||
|
||||
A Juvix file must declare a module whose name corresponds exactly to the name of the file. For example, a file =Hello.juvix= must declare a module =Hello=:
|
||||
#+begin_example
|
||||
-- Hello world example. This is a comment.
|
||||
module Hello;
|
||||
|
||||
-- Import the standard library prelude, including the function 'printStringLn'
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
main : IO;
|
||||
main := printStringLn "Hello world!";
|
||||
|
||||
end;
|
||||
#+end_example
|
||||
A file compiled to an executable must define the zero-argument function =main= of type =IO= which is evaluated when running the program.
|
||||
|
||||
** Output
|
||||
|
||||
In addition to =printStringLn=, the standard library includes the functions =printString=, =printNat=, =printNatLn=, =printBool=, =printBoolLn=. The =IO= computations can be sequenced with =>>=, e.g.,
|
||||
#+begin_example
|
||||
printNat 3 >> printString " + " >> printNatLn 4
|
||||
#+end_example
|
||||
has type =IO= and when executed prints =3 + 4= followed by a newline.
|
||||
|
||||
The type =IO= is the type of IO actions, i.e., of data structures representing IO computations. The functions =printString=, =printNat=, etc., do not immediately print their arguments, but rather create a data structure representing an appropriate IO action. The IO actions created by the =main= function are executed only after the program has been evaluated.
|
||||
|
||||
** Data types and functions
|
||||
|
||||
To see the type of an expression, use the =:type= REPL command:
|
||||
#+begin_example
|
||||
Stdlib.Prelude> :type 1
|
||||
Nat
|
||||
Stdlib.Prelude> :type true
|
||||
Bool
|
||||
#+end_example
|
||||
|
||||
The types =Nat= and =Bool= are defined in the standard library.
|
||||
|
||||
The type =Bool= has two constructors =true= and =false=.
|
||||
#+begin_example
|
||||
type Bool :=
|
||||
| true : Bool
|
||||
| false : Bool;
|
||||
#+end_example
|
||||
The constructors of a data type can be used to build elements of the type. They can also appear as patterns in function definitions. For example, the =not= function is defined in the standard library by:
|
||||
#+begin_example
|
||||
not : Bool -> Bool;
|
||||
not true := false;
|
||||
not false := true;
|
||||
#+end_example
|
||||
The first line is the /signature/ which specifies the type of the definition. In this case, =not= is a function from =Bool= to =Bool=. The signature is followed by two /function clauses/ which specify the function result depending on the shape of the arguments. When a function call is evaluated, the first clause that matches the arguments is used.
|
||||
|
||||
In contrast to languages like Python, Java or C/C++, Juvix doesn't require parentheses for function calls. All the arguments are just listed after the function. The general pattern for function application is: =func arg1 arg2 arg3 ...=
|
||||
|
||||
A more complex example of a data type is the =Nat= type from the standard library:
|
||||
#+begin_example
|
||||
type Nat :=
|
||||
| zero : Nat
|
||||
| suc : Nat -> Nat;
|
||||
#+end_example
|
||||
The constructor =zero= represents =0= and =suc= represents the successor function -- =suc n= is the successor of =n=, i.e., =n+1=. For example, =suc zero= represents =1=. The number literals =0=, =1=, =2=, etc., are just shorthands for appropriate expressions built using =suc= and =zero=.
|
||||
|
||||
The constructors of a data type specify how the elements of the type can be constructed. For instance, the above definition specifies that an element of =Nat= is either:
|
||||
* =zero=, or
|
||||
* =suc n= where =n= is an element of =Nat=, i.e., it is constructed by applying =suc= to appropriate arguments (in this case the argument of =suc= has type =Nat=).
|
||||
Any element of =Nat= can be built with the constructors in this way -- there are no other elements. Mathematically, this is an inductive definition, which is why the data type is called /inductive/.
|
||||
|
||||
If implemented directly, the above unary representation of natural numbers would be extremely inefficient. The Juvix compiler uses a binary number representation under the hood and implements arithmetic operations using corresponding machine instructions, so the performance of natural number arithmetic is similar to other programming languages. The =Nat= type is a high-level presentation of natural numbers as seen by the user who does not need to worry about low-level arithmetic implementation details.
|
||||
|
||||
One can use =zero= and =suc= in pattern matching, like any other constructors:
|
||||
#+begin_example
|
||||
infixl 6 +;
|
||||
+ : Nat -> Nat -> Nat;
|
||||
+ zero b := b;
|
||||
+ (suc a) b := suc (a + b);
|
||||
#+end_example
|
||||
The =infixl 6 += declares =+= to be an infix left-associative operator with priority 6. The =+= is an ordinary function, except that function application for =+= is written in infix notation. The definitions of the clauses of =+= still need the prefix notation on the left-hand sides.
|
||||
|
||||
The =a= and =b= in the patterns on the left-hand sides of the clauses are /variables/ which match arbitrary values of the corresponding type. They can be used on the right-hand side to refer to the values matched. For example, when evaluating
|
||||
#+begin_example
|
||||
(suc (suc zero)) + zero
|
||||
#+end_example
|
||||
the second clause of =+= matches, assigning =suc zero= to =a= and =zero= to =b=. Then the right-hand side of the clause is evaluated with =a= and =b= substituted by these values:
|
||||
#+begin_example
|
||||
suc (suc zero + zero)
|
||||
#+end_example
|
||||
Again, the second clause matches, now with both =a= and =b= being =zero=. After replacing with the right-hand side, we obtain:
|
||||
#+begin_example
|
||||
suc (suc (zero + zero))
|
||||
#+end_example
|
||||
Now the first clause matches and finally we obtain the result
|
||||
#+begin_example
|
||||
suc (suc zero)
|
||||
#+end_example
|
||||
which is just =2=.
|
||||
|
||||
The function =+= is defined like above in the standard library, but the Juvix compiler treats it specially and generates efficient code using appropriate CPU instructions.
|
||||
|
||||
** Pattern matching
|
||||
|
||||
The patterns in function clauses do not have to match on a single constructor -- they may be arbitrarily deep. For example, here is an (inefficient) implementation of a function which checks whether a natural number is even:
|
||||
#+begin_example
|
||||
even : Nat -> Bool;
|
||||
even zero := true;
|
||||
even (suc zero) := false;
|
||||
even (suc (suc n)) := even n;
|
||||
#+end_example
|
||||
This definition states that a natural number =n= is even if either =n= is =zero= or, recursively, =n-2= is even.
|
||||
|
||||
If a subpattern is to be ignored, then one can use a wildcard =_= instead of naming the subpattern.
|
||||
#+begin_example
|
||||
isPositive : Nat -> Bool;
|
||||
isPositive zero := false;
|
||||
isPositive (suc _) := true;
|
||||
#+end_example
|
||||
The above function could also be written as:
|
||||
#+begin_example
|
||||
isPositive : Nat -> Bool;
|
||||
isPositive zero := false;
|
||||
isPositive _ := true;
|
||||
#+end_example
|
||||
|
||||
It is not necessary to define a separate function to perform pattern matching. One can use the =case= syntax to pattern match an expression directly.
|
||||
#+begin_example
|
||||
Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
|
||||
1
|
||||
#+end_example
|
||||
|
||||
** Comparisons and conditionals
|
||||
|
||||
To use the comparison operators on natural numbers, one needs to import the =Stdlib.Data.Nat.Ord= module. The comparison operators are not in =Stdlib.Prelude= to avoid clashes with user-defined operators for other data types. The functions available in =Stdlib.Data.Nat.Org= include: =<=, =<==, =>=, =>==, ====, =/==, =min=, =max=.
|
||||
|
||||
For example, one may define the function =max3= by:
|
||||
#+begin_example
|
||||
open import Stdlib.Data.Nat.Ord;
|
||||
|
||||
max3 : Nat -> Nat -> Nat -> Nat;
|
||||
max3 x y z := if (x > y) (max x z) (max y z);
|
||||
#+end_example
|
||||
The conditional =if= is a special function which is evaluated lazily, i.e., first the condition (the first argument) is evaluated, and then depending on its truth-value one of the branches (the second or the third argument) is evaluated and returned.
|
||||
|
||||
By default, evaluation in Juvix is /eager/ (or /strict/), meaning that the arguments to a function are fully evaluated before applying the function. Only =if=, =||= and =&&= are treated specially and evaluated lazily. These special functions cannot be partially applied (see [[./learn.md#partial-application-and-higher-order-functions][Partial application and higher-order functions]] below).
|
||||
|
||||
** Local definitions
|
||||
|
||||
Juvix supports local definitions with let-expressions.
|
||||
#+begin_example
|
||||
f : Nat -> Nat;
|
||||
f a := let x : Nat := a + 5;
|
||||
y : Nat := a * 7 + x
|
||||
in
|
||||
x * y;
|
||||
#+end_example
|
||||
The variables =x= and =y= are not visible outside =f=.
|
||||
|
||||
One can also use multi-clause definitions in =let=-expressions, with the same syntax as definitions inside a module. Complex definitions need to be enclosed in braces. For example:
|
||||
#+begin_example
|
||||
even' : Nat -> Bool;
|
||||
even' :=
|
||||
let {
|
||||
even : Nat -> Bool;
|
||||
odd : Nat -> Bool;
|
||||
|
||||
even zero := true;
|
||||
even (suc n) := odd n;
|
||||
|
||||
odd zero := false;
|
||||
odd (suc n) := even n;
|
||||
} in
|
||||
even
|
||||
#+end_example
|
||||
The functions =even= and =odd= are not visible outside =even'=.
|
||||
|
||||
** Recursion
|
||||
|
||||
Juvix is a purely functional language, which means that functions have no side effects and all variables are immutable. An advantage of functional programming is that all expressions are /referentially transparent/ -- any expression can be replaced by its value without changing the meaning of the program. This makes it easier to reason about programs, in particular to prove their correctness. No errors involving implicit state are possible, because the state is always explicit.
|
||||
|
||||
In a functional language, there are no imperative loops. Repetition is expressed using recursion. In many cases, the recursive definition of a function follows the inductive definition of a data structure the function analyses. For example, consider the following inductive type of lists of natural numbers:
|
||||
#+begin_example
|
||||
type NList :=
|
||||
| nnil : NList
|
||||
| ncons : Nat -> NList -> NList;
|
||||
#+end_example
|
||||
An element of =NList= is either =nnil= (empty) or =ncons x xs= where =x : Nat= and =xs : NList= (a list with head =x= and tail =xs=).
|
||||
|
||||
A function computing the length of a list may be defined by:
|
||||
#+begin_example
|
||||
nlength : NList -> Nat;
|
||||
nlength nnil := 0;
|
||||
nlength (ncons _ xs) := nlength xs + 1;
|
||||
#+end_example
|
||||
The definition follows the inductive definition of =NList=. There are two function clauses for the two constructors. The case for =nnil= is easy -- the constructor has no arguments and the length of the empty list is =0=. For a constructor with some arguments, one typically needs to express the result of the function in terms of the constructor arguments, usually calling the function recursively on the constructor's inductive arguments (for =ncons= this is the second argument). In the case of =ncons _ xs=, we recursively call =nlength= on =xs= and add =1= to the result.
|
||||
|
||||
Let's consider another example -- a function which returns the maximum of the numbers in a list or 0 for the empty list.
|
||||
#+begin_example
|
||||
open import Stdlib.Data.Nat.Ord; -- for `max`
|
||||
|
||||
nmaximum : NList -> Nat;
|
||||
nmaximum nnil := 0;
|
||||
nmaximum (ncons x xs) := max x (nmaximum xs);
|
||||
#+end_example
|
||||
Again, there is a clause for each constructor. In the case for =ncons=, we recursively call the function on the list tail and take the maximum of the result and the list head.
|
||||
|
||||
For an example of a constructor with more than one inductive argument, consider binary trees with natural numbers in nodes.
|
||||
#+begin_example
|
||||
type Tree :=
|
||||
| leaf : Nat -> Tree
|
||||
| node : Nat -> Tree -> Tree -> Tree;
|
||||
#+end_example
|
||||
The constructor =node= has two inductive arguments (the second and the third) which represent the left and the right subtree.
|
||||
|
||||
A function which produces the mirror image of a tree may be defined by:
|
||||
#+begin_example
|
||||
mirror : Tree -> Tree;
|
||||
mirror (leaf x) := leaf x;
|
||||
mirror (node x l r) := node x (mirror r) (mirror l);
|
||||
#+end_example
|
||||
The definition of =mirror= follows the definition of =Tree=. There are two recursive calls for the two inductive constructors of =node= (the subtrees).
|
||||
|
||||
** Partial application and higher-order functions
|
||||
|
||||
Strictly speaking, all Juvix functions have only one argument. Multi-argument functions are really functions which return a function which takes the next argument and returns a function taking another argument, and so on for all arguments. The function type former =->= (the arrow) is right-associative. Hence, the type, e.g., =Nat -> Nat -> Nat= when fully parenthesised becomes =Nat -> (Nat -> Nat)=. It is the type of functions which given an argument of type =Nat= return a function of type =Nat -> Nat= which itself takes an argument of type =Nat= and produces a result of type =Nat=. Function application is left-associative. For example, =f a b= when fully parenthesised becomes =(f a) b=. So it is an application to =b= of the function obtained by applying =f= to =a=.
|
||||
|
||||
Since a multi-argument function is just a one-argument function returning a function, it can be /partially applied/ to a smaller number of arguments than specified in its definition. The result is an appropriate function. For example, =sub 10= is a function which subtracts its argument from =10=, and =(+) 1= is a function which adds =1= to its argument. If the function has been declared as an infix operator (like =+=), then for partial application one needs to enclose it in parentheses.
|
||||
|
||||
A function which takes a function as an argument is a /higher-order function/. An example is the =nmap= function which applies a given function to each element in a list of natural numbers.
|
||||
#+begin_example
|
||||
nmap : (Nat -> Nat) -> NList -> NList;
|
||||
nmap _ nnil := nnil;
|
||||
nmap f (ncons x xs) := ncons (f x) (nmap f xs);
|
||||
#+end_example
|
||||
|
||||
The application
|
||||
#+begin_example
|
||||
nmap \{ x := div x 2 } lst
|
||||
#+end_example
|
||||
divides every element of =lst= by =2=, rounding down the result. The expression
|
||||
#+begin_example
|
||||
\{ x := div x 1 }
|
||||
#+end_example
|
||||
is an unnamed function, or a /lambda/, which divides its argument by =2=.
|
||||
|
||||
** Polymorphism
|
||||
|
||||
The type =NList= we have been working with above requires the list elements to be natural numbers. It is possible to define lists /polymorphically/, parameterising them by the element type. This is analogous to generics in languages like Java, C++ or Rust. Here is the polymorphic definition of lists from the standard library:
|
||||
#+begin_example
|
||||
infixr 5 ::;
|
||||
type List (A : Type) :=
|
||||
| nil : List A
|
||||
| :: : A -> List A -> List A;
|
||||
#+end_example
|
||||
The constructor =::= is declared as a right-associative infix operator with priority 5. The definition has a parameter =A= which is the element type.
|
||||
|
||||
Now one can define the =map= function polymorphically:
|
||||
#+begin_example
|
||||
map : {A : Type} -> {B : Type} -> (A -> B) -> List A -> List B;
|
||||
map f nil := nil;
|
||||
map f (h :: hs) := f h :: map f hs;
|
||||
#+end_example
|
||||
This function has two /implicit type arguments/ =A= and =B=. These arguments are normally omitted in function application -- they are inferred automatically during type checking. The curly braces indicate that the argument is implicit and should be inferred.
|
||||
|
||||
In fact, the constructors =nil= and =::= also have an implicit argument: the type of list elements. All type parameters of a data type definition become implicit arguments of the constructors.
|
||||
|
||||
Usually, the implicit arguments in a function application can be inferred. However, sometimes this is not possible and then the implicit arguments need to be provided explicitly by enclosing them in braces:
|
||||
#+begin_example
|
||||
f {implArg1} .. {implArgK} arg1 .. argN
|
||||
#+end_example
|
||||
For example, =nil {Nat}= has type =List Nat= while =nil= by itself has type ={A : Type} -> List A=.
|
||||
|
||||
** Tail recursion
|
||||
|
||||
Any recursive call whose result is further processed by the calling function needs to create a new stack frame to save the calling function environment. This means that each such call will use a constant amount of memory. For example, a function =sum= implemented as follows will use an additional amount of memory proportional to the length of the processed list:
|
||||
#+begin_example
|
||||
sum : NList -> Nat;
|
||||
sum nnil := 0;
|
||||
sum (ncons x xs) := x + sum xs;
|
||||
#+end_example
|
||||
This is not acceptable if you care about performance. In an imperative language, one would use a simple loop going over the list without any memory allocation. In pseudocode:
|
||||
#+begin_example
|
||||
var sum : Nat := 0;
|
||||
while (lst /= nnil) {
|
||||
sum := sum + head lst;
|
||||
lst := tail lst;
|
||||
};
|
||||
return sum;
|
||||
#+end_example
|
||||
Fortunately, it is possible to rewrite this function to use /tail recursion/. A recursive call is /tail recursive/ if its result is also the result of the calling function, i.e., the calling function returns immediately after it without further processing. The Juvix compiler /guarantees/ that all tail calls will be eliminated, i.e., that they will be compiled to simple jumps without extra memory allocation. In a tail recursive call, instead of creating a new stack frame, the old one is reused.
|
||||
|
||||
The following implementation of =sum= uses tail recursion.
|
||||
#+begin_example
|
||||
sum : NList -> Nat;
|
||||
sum lst := let {
|
||||
go : Nat -> NList -> Nat;
|
||||
go acc nnil := acc;
|
||||
go acc (ncons x xs) := go (acc + x) xs;
|
||||
} in
|
||||
go 0 lst;
|
||||
#+end_example
|
||||
The first argument of =go= is an /accumulator/ which holds the sum computed so far. It is analogous to the =sum= variable in the imperative loop above. The initial value of the accumulator is 0. The function =go= uses only constant additional memory overall. The code generated for it by the Juvix compiler is equivalent to an imperative loop.
|
||||
|
||||
A shorter way of writing the above =sum= function is to use a /named lambda/:
|
||||
#+begin_example
|
||||
sum : NList -> Nat;
|
||||
sum := go(acc := 0)@\{
|
||||
acc nnil := acc;
|
||||
acc (ncons x xs) := go (acc + x) xs;
|
||||
};
|
||||
#+end_example
|
||||
The syntax
|
||||
#+begin_example
|
||||
go(acc1 := v1= ... accn := vn)@\{ <clauses> }
|
||||
#+end_example
|
||||
introduces a recursive function =go= with =n= accumulators =acc1=, ..., =accn= and further =k= arguments of the lambda expression (above =n = k = 1=). The value of the entire expression is =go v1 ... vn=. The scope of =go= is the lambda expression, i.e., it is not visible outside of it.
|
||||
|
||||
Most imperative loops may be translated into tail recursive functional programs by converting the locally modified variables into accumulators and the loop condition into pattern matching. For example, here is a pseudocode for computing the nth Fibonacci number in linear time. The variables =cur= and =next= hold the last two computed Fibonacci numbers.
|
||||
#+begin_example
|
||||
var cur : Nat := 0;
|
||||
var next : Nat := 1;
|
||||
while (n /= 0) {
|
||||
var tmp := next;
|
||||
next := cur + next;
|
||||
cur := tmp;
|
||||
n := n - 1;
|
||||
};
|
||||
return cur;
|
||||
#+end_example
|
||||
An equivalent functional program is:
|
||||
#+begin_example
|
||||
fib : Nat -> Nat;
|
||||
fib := go(cur := 0; next := 1)@\{
|
||||
cur _ zero := cur;
|
||||
cur next (suc n) := go next (cur + next) n;
|
||||
};
|
||||
#+end_example
|
||||
A naive definition of the Fibonacci function runs in exponential time:
|
||||
#+begin_example
|
||||
fib : Nat -> Nat;
|
||||
fib zero := 0;
|
||||
fib (suc zero) := 1;
|
||||
fib (suc (suc n)) := fib n + fib (suc n);
|
||||
#+end_example
|
||||
|
||||
Tail recursion is less useful when the function needs to allocate memory anyway. For example, one could make the =map= function from the previous section tail recursive, but the time and memory use would still be proportional to the length of the input because of the need to allocate the result list.
|
||||
|
||||
** Totality checking
|
||||
|
||||
By default, the Juvix compiler requires all functions to be total. Totality consists of:
|
||||
* [[../explanations/totality/termination.md][termination]],
|
||||
* [[../explanations/totality/coverage.md][coverage]],
|
||||
* [[../explanations/totality/positive.md][strict positivity]].
|
||||
|
||||
The termination check ensures that all functions are structurally recursive, i.e., all recursive call are on structurally smaller value -- subpatterns of the matched pattern. For example, the termination checker rejects the definition
|
||||
#+begin_example
|
||||
fact : Nat -> Nat;
|
||||
fact x := if (x == 0) 1 (x * fact (sub x 1));
|
||||
#+end_example
|
||||
because the recursive call is not on a subpattern of a pattern matched on in the clause. One can reformulate this definition so that it is accepted by the termination checker:
|
||||
#+begin_example
|
||||
fact : Nat -> Nat;
|
||||
fact zero := 1;
|
||||
fact x@(suc n) := x * fact n;
|
||||
#+end_example
|
||||
Sometimes, such a reformulation is not possible. Then one can use the =terminating= keyword to forgoe the termination check.
|
||||
#+begin_example
|
||||
terminating
|
||||
log2 : Nat -> Nat;
|
||||
log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
|
||||
#+end_example
|
||||
|
||||
Coverage checking ensures that there are no unhandled patterns in function clauses or =case= expressions. For example, the following definition is rejected because the case =suc zero= is not handled:
|
||||
#+begin_example
|
||||
even : Nat -> Bool;
|
||||
even zero := true;
|
||||
even (suc (suc n)) := even n;
|
||||
#+end_example
|
||||
|
||||
** Exercises
|
||||
|
||||
You have now learnt the very basics of Juvix. To consolidate your understanding of Juvix and functional programming, try doing some of the following exercises. To learn how to write more complex Juvix programs, see the [[https://docs.juvix.org/examples/html/Tutorial/Tutorial.html][advanced tutorial]] and the [[../reference/examples.md][Juvix program examples]].
|
||||
|
||||
1. Define a function =prime : Nat -> Nat= which checks if a given natural number is prime.
|
||||
|
||||
2. What is wrong with the following definition?
|
||||
#+begin_example
|
||||
half : Nat -> Nat;
|
||||
half n := if (n < 2) 0 (half (n - 2) + 1);
|
||||
#+end_example
|
||||
How can you reformulate this definition so that it is accepted by Juvix?
|
||||
|
||||
3. Define a polymorphic function which computes the last element of a list. What is the result of your function on the empty list?
|
||||
|
||||
4. A /suffix/ of a list =l= is any list which can be obtained from =l= by removing some initial elements. For example, the suffixes of =1 :: 2 :: 3 :: nil= are: =1 :: 2 :: 3 :: nil=, =2 :: 3 :: nil=, =3 :: nil= and =nil=.
|
||||
|
||||
Define a function which computes the list of all suffixes of a given list in the order of decreasing length.
|
||||
|
||||
5. Recall the =Tree= type from above.
|
||||
#+begin_example
|
||||
type Tree :=
|
||||
| leaf : Nat -> Tree
|
||||
| node : Nat -> Tree -> Tree -> Tree;
|
||||
#+end_example
|
||||
Analogously to the =map= function for lists, define a function
|
||||
#+begin_example
|
||||
tmap : (Nat -> Nat) -> Tree -> Tree
|
||||
#+end_example
|
||||
which applies a function to all natural numbers stored in a tree.
|
||||
|
||||
6. Make the =Tree= type polymorphic in the element type and repeat the previous exercise.
|
||||
|
||||
7. Write a tail recursive function which reverses a list.
|
||||
|
||||
8. Write a tail recursive function which computes the factorial of a natural number.
|
||||
|
||||
9. Define a function =comp : {A : Type} -> List (A -> A) -> A -> A= which composes all functions in a list. For example,
|
||||
#+begin_example
|
||||
comp (suc :: (*) 2 :: \{x := sub x 1} :: nil)
|
||||
#+end_example
|
||||
should be a function which given =x= computes =2(x - 1) + 1=.
|
||||
0
docs/org/tutorials/structure.org
Normal file
0
docs/org/tutorials/structure.org
Normal file
0
docs/org/tutorials/vscode.org
Normal file
0
docs/org/tutorials/vscode.org
Normal file
@ -0,0 +1,2 @@
|
||||
name: Demo
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: Collatz
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: Fibonacci
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: Hanoi
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: HelloWorld
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: PascalsTriangle
|
||||
version: 0.1.0
|
||||
@ -1,2 +1,2 @@
|
||||
name: tic-tac-toe
|
||||
version: 1.0.0
|
||||
name: TicTacToe
|
||||
version: 0.1.0
|
||||
|
||||
16
examples/milestone/Tutorial/Tutorial.juvix
Normal file
16
examples/milestone/Tutorial/Tutorial.juvix
Normal file
@ -0,0 +1,16 @@
|
||||
--- This is an advanced tutorial for the Juvix programming language. You should read
|
||||
--- the "Quick start" and the "Learn Juvix in minutes" pages in the documentation
|
||||
--- first.
|
||||
|
||||
module Tutorial;
|
||||
|
||||
|
||||
-- import the standard library prelude and bring it into scope
|
||||
open import Stdlib.Prelude;
|
||||
-- bring comparison operators on Nat into scope
|
||||
open import Stdlib.Data.Nat.Ord;
|
||||
|
||||
main : IO;
|
||||
main := printStringLn "Hello world!";
|
||||
|
||||
end;
|
||||
2
examples/milestone/Tutorial/juvix.yaml
Normal file
2
examples/milestone/Tutorial/juvix.yaml
Normal file
@ -0,0 +1,2 @@
|
||||
name: Tutorial
|
||||
version: 0.1.0
|
||||
@ -0,0 +1,2 @@
|
||||
name: ValidityPredicates
|
||||
version: 0.1.0
|
||||
Loading…
Reference in New Issue
Block a user