From 52f99936f6d298c23439349a7aef0aa8e97066c7 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 11 Jan 2023 14:56:42 +0100 Subject: [PATCH 1/9] restructure documentation --- README.org | 144 +----------------- docs/org/SUMMARY.org | 64 ++++---- .../{introduction => }/about/community.org | 0 docs/org/{introduction => }/about/team.org | 0 docs/org/backends/README.org | 1 - docs/org/backends/minic.org | 1 - .../language/abstract.org | 1 - .../language/concrete.org | 1 - .../language/microjuvix.org | 1 - docs/org/compiler-architecture/languages.org | 7 - docs/org/compiler-architecture/pipeline.org | 1 - docs/org/examples/README.org | 0 .../totality/termination.org} | 0 docs/org/getting-started/README.org | 2 - docs/org/getting-started/dependencies.org | 38 ----- docs/org/getting-started/quick-start.org | 58 ------- docs/org/howto/installing.org | 119 +++++++++++++++ docs/org/language-reference/README.org | 8 - docs/org/notes/lsp.org | 12 ++ docs/org/quick-start.org | 90 +++++++++++ docs/org/reference/examples.org | 9 ++ docs/org/reference/language/README.org | 7 + .../language}/axiom.org | 0 .../language}/builtins.org | 0 .../language}/comments.org | 2 +- .../language/compileblocks.org} | 0 .../language/datatypes.org} | 0 .../language/foreign.org} | 0 .../language}/functions.org | 0 .../language}/modules.org | 0 docs/org/reference/stdlib.org | 2 + docs/org/{ => reference}/tooling/CLI.org | 0 docs/org/{ => reference}/tooling/README.org | 2 +- docs/org/{ => reference}/tooling/doctor.org | 0 .../tooling/emacs.org} | 0 docs/org/{ => reference}/tooling/testing.org | 0 docs/org/tutorials/emacs.org | 0 docs/org/tutorials/learn.org | 0 docs/org/tutorials/structure.org | 0 docs/org/tutorials/vscode.org | 0 40 files changed, 280 insertions(+), 290 deletions(-) mode change 100755 => 100644 docs/org/SUMMARY.org rename docs/org/{introduction => }/about/community.org (100%) rename docs/org/{introduction => }/about/team.org (100%) delete mode 100644 docs/org/backends/README.org delete mode 100644 docs/org/backends/minic.org delete mode 100644 docs/org/compiler-architecture/language/abstract.org delete mode 100644 docs/org/compiler-architecture/language/concrete.org delete mode 100644 docs/org/compiler-architecture/language/microjuvix.org delete mode 100644 docs/org/compiler-architecture/languages.org delete mode 100644 docs/org/compiler-architecture/pipeline.org mode change 100755 => 100644 docs/org/examples/README.org rename docs/org/{language-reference/termination-checking.org => explanations/totality/termination.org} (100%) delete mode 100644 docs/org/getting-started/README.org delete mode 100755 docs/org/getting-started/dependencies.org delete mode 100644 docs/org/getting-started/quick-start.org create mode 100644 docs/org/howto/installing.org delete mode 100644 docs/org/language-reference/README.org create mode 100644 docs/org/notes/lsp.org create mode 100644 docs/org/quick-start.org create mode 100644 docs/org/reference/examples.org create mode 100644 docs/org/reference/language/README.org rename docs/org/{language-reference => reference/language}/axiom.org (100%) rename docs/org/{language-reference => reference/language}/builtins.org (100%) mode change 100755 => 100644 rename docs/org/{language-reference => reference/language}/comments.org (67%) rename docs/org/{language-reference/compile-blocks.org => reference/language/compileblocks.org} (100%) mode change 100755 => 100644 rename docs/org/{language-reference/inductive-data-types.org => reference/language/datatypes.org} (100%) mode change 100755 => 100644 rename docs/org/{language-reference/foreign-blocks.org => reference/language/foreign.org} (100%) rename docs/org/{language-reference => reference/language}/functions.org (100%) rename docs/org/{language-reference => reference/language}/modules.org (100%) mode change 100755 => 100644 create mode 100644 docs/org/reference/stdlib.org rename docs/org/{ => reference}/tooling/CLI.org (100%) rename docs/org/{ => reference}/tooling/README.org (60%) rename docs/org/{ => reference}/tooling/doctor.org (100%) rename docs/org/{tooling/emacs-mode.org => reference/tooling/emacs.org} (100%) rename docs/org/{ => reference}/tooling/testing.org (100%) create mode 100644 docs/org/tutorials/emacs.org create mode 100644 docs/org/tutorials/learn.org create mode 100644 docs/org/tutorials/structure.org create mode 100644 docs/org/tutorials/vscode.org diff --git a/README.org b/README.org index adc5fada4f..bbddca73ae 100644 --- a/README.org +++ b/README.org @@ -46,149 +46,9 @@ 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 diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org old mode 100755 new mode 100644 index cfbac70168..961aa2699b --- a/docs/org/SUMMARY.org +++ b/docs/org/SUMMARY.org @@ -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 X 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/comments.md][Comments]] + - [[./reference/language/axiom.md][Axiom]] + - [[./reference/language/compileblocks.md][Compile block]] + - [[./reference/language/modules.md][Module]] + - [[./reference/language/datatypes.md][Data types]] + - [[./reference/languages/functions.md][Function]] + - [[./reference/language/foreign.md][Foreign block]] +- [[./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]] diff --git a/docs/org/introduction/about/community.org b/docs/org/about/community.org similarity index 100% rename from docs/org/introduction/about/community.org rename to docs/org/about/community.org diff --git a/docs/org/introduction/about/team.org b/docs/org/about/team.org similarity index 100% rename from docs/org/introduction/about/team.org rename to docs/org/about/team.org diff --git a/docs/org/backends/README.org b/docs/org/backends/README.org deleted file mode 100644 index f2f31863c8..0000000000 --- a/docs/org/backends/README.org +++ /dev/null @@ -1 +0,0 @@ -- [[./minic.md][MiniC backend]] diff --git a/docs/org/backends/minic.org b/docs/org/backends/minic.org deleted file mode 100644 index 4568fd182d..0000000000 --- a/docs/org/backends/minic.org +++ /dev/null @@ -1 +0,0 @@ -* MiniC Backend diff --git a/docs/org/compiler-architecture/language/abstract.org b/docs/org/compiler-architecture/language/abstract.org deleted file mode 100644 index 7066085297..0000000000 --- a/docs/org/compiler-architecture/language/abstract.org +++ /dev/null @@ -1 +0,0 @@ -* Abstract Internal Language diff --git a/docs/org/compiler-architecture/language/concrete.org b/docs/org/compiler-architecture/language/concrete.org deleted file mode 100644 index 7b5a5bee95..0000000000 --- a/docs/org/compiler-architecture/language/concrete.org +++ /dev/null @@ -1 +0,0 @@ -* Concrete Internal Language diff --git a/docs/org/compiler-architecture/language/microjuvix.org b/docs/org/compiler-architecture/language/microjuvix.org deleted file mode 100644 index b4f8ed2ea2..0000000000 --- a/docs/org/compiler-architecture/language/microjuvix.org +++ /dev/null @@ -1 +0,0 @@ -* MicroJuvix Internal Language diff --git a/docs/org/compiler-architecture/languages.org b/docs/org/compiler-architecture/languages.org deleted file mode 100644 index afb2022832..0000000000 --- a/docs/org/compiler-architecture/languages.org +++ /dev/null @@ -1,7 +0,0 @@ -* Internal Juvix languages - -** Languages - -- [[./language/abstract.md][Abstract Language]] -- [[./language/concrete.md][Concrete language]] -- [[./language/microjuvix.md][MicroJuvix Language]] diff --git a/docs/org/compiler-architecture/pipeline.org b/docs/org/compiler-architecture/pipeline.org deleted file mode 100644 index b2a4d09a8b..0000000000 --- a/docs/org/compiler-architecture/pipeline.org +++ /dev/null @@ -1 +0,0 @@ -* Pipeline diff --git a/docs/org/examples/README.org b/docs/org/examples/README.org old mode 100755 new mode 100644 diff --git a/docs/org/language-reference/termination-checking.org b/docs/org/explanations/totality/termination.org similarity index 100% rename from docs/org/language-reference/termination-checking.org rename to docs/org/explanations/totality/termination.org diff --git a/docs/org/getting-started/README.org b/docs/org/getting-started/README.org deleted file mode 100644 index 50a2a941e0..0000000000 --- a/docs/org/getting-started/README.org +++ /dev/null @@ -1,2 +0,0 @@ -- [[./quick-start.md][Quick start]] -- [[./dependencies.md][Installing dependencies]] diff --git a/docs/org/getting-started/dependencies.org b/docs/org/getting-started/dependencies.org deleted file mode 100755 index b5b8a368e8..0000000000 --- a/docs/org/getting-started/dependencies.org +++ /dev/null @@ -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 diff --git a/docs/org/getting-started/quick-start.org b/docs/org/getting-started/quick-start.org deleted file mode 100644 index b05e032daa..0000000000 --- a/docs/org/getting-started/quick-start.org +++ /dev/null @@ -1,58 +0,0 @@ -* Quick Start - -#+begin_html - -Juvix Mascot - -#+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 diff --git a/docs/org/howto/installing.org b/docs/org/howto/installing.org new file mode 100644 index 0000000000..029aa67ddf --- /dev/null +++ b/docs/org/howto/installing.org @@ -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 instruction 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 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]] 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 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=. + +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 diff --git a/docs/org/language-reference/README.org b/docs/org/language-reference/README.org deleted file mode 100644 index 81b2d326b3..0000000000 --- a/docs/org/language-reference/README.org +++ /dev/null @@ -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]] diff --git a/docs/org/notes/lsp.org b/docs/org/notes/lsp.org new file mode 100644 index 0000000000..fb51333e52 --- /dev/null +++ b/docs/org/notes/lsp.org @@ -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 diff --git a/docs/org/quick-start.org b/docs/org/quick-start.org new file mode 100644 index 0000000000..41039d09fc --- /dev/null +++ b/docs/org/quick-start.org @@ -0,0 +1,90 @@ +* Quick Start + +#+begin_html + +Juvix Mascot + +#+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 available. See +[[./quick-start.md#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 + +** 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 := 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 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 diff --git a/docs/org/reference/examples.org b/docs/org/reference/examples.org new file mode 100644 index 0000000000..87d522bd1e --- /dev/null +++ b/docs/org/reference/examples.org @@ -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]] diff --git a/docs/org/reference/language/README.org b/docs/org/reference/language/README.org new file mode 100644 index 0000000000..9e334ca228 --- /dev/null +++ b/docs/org/reference/language/README.org @@ -0,0 +1,7 @@ + - [[./comments.md][Comments]] + - [[./axiom.md][Axiom]] + - [[./functions.md][Function]] + - [[./modules.md][Module System]] + - [[./datatypes.md][Inductive data types]] + - [[./compileblocks.md][Compile blocks]] + - [[./foreign.md][Foreign blocks]] diff --git a/docs/org/language-reference/axiom.org b/docs/org/reference/language/axiom.org similarity index 100% rename from docs/org/language-reference/axiom.org rename to docs/org/reference/language/axiom.org diff --git a/docs/org/language-reference/builtins.org b/docs/org/reference/language/builtins.org old mode 100755 new mode 100644 similarity index 100% rename from docs/org/language-reference/builtins.org rename to docs/org/reference/language/builtins.org diff --git a/docs/org/language-reference/comments.org b/docs/org/reference/language/comments.org similarity index 67% rename from docs/org/language-reference/comments.org rename to docs/org/reference/language/comments.org index d201074b98..0160eb7b6b 100644 --- a/docs/org/language-reference/comments.org +++ b/docs/org/reference/language/comments.org @@ -1,6 +1,6 @@ * Comments -A comment is introduced in the same fashion as in =Haskell=/=Agda=. +A comment is introduced in the same fashion as in =Haskell= or =Agda=. - Inline Comment #+begin_src diff --git a/docs/org/language-reference/compile-blocks.org b/docs/org/reference/language/compileblocks.org old mode 100755 new mode 100644 similarity index 100% rename from docs/org/language-reference/compile-blocks.org rename to docs/org/reference/language/compileblocks.org diff --git a/docs/org/language-reference/inductive-data-types.org b/docs/org/reference/language/datatypes.org old mode 100755 new mode 100644 similarity index 100% rename from docs/org/language-reference/inductive-data-types.org rename to docs/org/reference/language/datatypes.org diff --git a/docs/org/language-reference/foreign-blocks.org b/docs/org/reference/language/foreign.org similarity index 100% rename from docs/org/language-reference/foreign-blocks.org rename to docs/org/reference/language/foreign.org diff --git a/docs/org/language-reference/functions.org b/docs/org/reference/language/functions.org similarity index 100% rename from docs/org/language-reference/functions.org rename to docs/org/reference/language/functions.org diff --git a/docs/org/language-reference/modules.org b/docs/org/reference/language/modules.org old mode 100755 new mode 100644 similarity index 100% rename from docs/org/language-reference/modules.org rename to docs/org/reference/language/modules.org diff --git a/docs/org/reference/stdlib.org b/docs/org/reference/stdlib.org new file mode 100644 index 0000000000..a266b3abbb --- /dev/null +++ b/docs/org/reference/stdlib.org @@ -0,0 +1,2 @@ + +The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains common functions that can be used in Juvix programs. diff --git a/docs/org/tooling/CLI.org b/docs/org/reference/tooling/CLI.org similarity index 100% rename from docs/org/tooling/CLI.org rename to docs/org/reference/tooling/CLI.org diff --git a/docs/org/tooling/README.org b/docs/org/reference/tooling/README.org similarity index 60% rename from docs/org/tooling/README.org rename to docs/org/reference/tooling/README.org index 8ebb95e630..dd57f660b2 100644 --- a/docs/org/tooling/README.org +++ b/docs/org/reference/tooling/README.org @@ -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]] diff --git a/docs/org/tooling/doctor.org b/docs/org/reference/tooling/doctor.org similarity index 100% rename from docs/org/tooling/doctor.org rename to docs/org/reference/tooling/doctor.org diff --git a/docs/org/tooling/emacs-mode.org b/docs/org/reference/tooling/emacs.org similarity index 100% rename from docs/org/tooling/emacs-mode.org rename to docs/org/reference/tooling/emacs.org diff --git a/docs/org/tooling/testing.org b/docs/org/reference/tooling/testing.org similarity index 100% rename from docs/org/tooling/testing.org rename to docs/org/reference/tooling/testing.org diff --git a/docs/org/tutorials/emacs.org b/docs/org/tutorials/emacs.org new file mode 100644 index 0000000000..e69de29bb2 diff --git a/docs/org/tutorials/learn.org b/docs/org/tutorials/learn.org new file mode 100644 index 0000000000..e69de29bb2 diff --git a/docs/org/tutorials/structure.org b/docs/org/tutorials/structure.org new file mode 100644 index 0000000000..e69de29bb2 diff --git a/docs/org/tutorials/vscode.org b/docs/org/tutorials/vscode.org new file mode 100644 index 0000000000..e69de29bb2 From 0973d5e8b6cc0b47431112cc96b5998bd3bde34a Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 11 Jan 2023 16:01:45 +0100 Subject: [PATCH 2/9] minor change --- docs/org/quick-start.org | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/org/quick-start.org b/docs/org/quick-start.org index 41039d09fc..5676da95da 100644 --- a/docs/org/quick-start.org +++ b/docs/org/quick-start.org @@ -8,8 +8,7 @@ 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 available. See -[[./quick-start.md#cli-usage-examples][CLI usage examples]] for descriptions of common tasks. +After installation, run =juvix --help= to see the list of commands available. Run Juvix doctor to check your system setup: From 8147a5146adc3cdf2c05e8d0c63996c1c594b102 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 11 Jan 2023 16:54:03 +0100 Subject: [PATCH 3/9] improve documentation --- docs/org/SUMMARY.org | 12 +++--- docs/org/howto/installing.org | 14 +++---- docs/org/quick-start.org | 2 +- docs/org/reference/language/README.org | 8 ++-- .../language/{axiom.org => axioms.org} | 0 docs/org/reference/language/datatypes.org | 38 ++++++++----------- docs/org/reference/language/functions.org | 11 +++--- 7 files changed, 39 insertions(+), 46 deletions(-) rename docs/org/reference/language/{axiom.org => axioms.org} (100%) diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org index 961aa2699b..1c0d2c341b 100644 --- a/docs/org/SUMMARY.org +++ b/docs/org/SUMMARY.org @@ -25,13 +25,13 @@ * Reference - [[./reference/stdlib.md][Standard library]] - [[./reference/language/README.md][Language reference]] - - [[./reference/language/comments.md][Comments]] - - [[./reference/language/axiom.md][Axiom]] - - [[./reference/language/compileblocks.md][Compile block]] - - [[./reference/language/modules.md][Module]] + - [[./reference/language/functions.md][Functions]] - [[./reference/language/datatypes.md][Data types]] - - [[./reference/languages/functions.md][Function]] - - [[./reference/language/foreign.md][Foreign block]] + - [[./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]] diff --git a/docs/org/howto/installing.org b/docs/org/howto/installing.org index 029aa67ddf..2c07c7db15 100644 --- a/docs/org/howto/installing.org +++ b/docs/org/howto/installing.org @@ -9,7 +9,7 @@ If you want to compile to WebAssembly, you also need: - [[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 instruction on how to install the dependencies. +See [[./installing.md#installing-dependencies][below]] for instructions on how to install the dependencies. * Installing Juvix @@ -30,7 +30,7 @@ brew install juvix #+end_src -Helpful information on the shell can also be obtained by running: +Helpful information can also be obtained by running: #+begin_src shell brew info juvix @@ -40,10 +40,10 @@ brew info juvix 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 install this executable, downlaod 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 +For example if =~/.local/bin= is on your shell's =PATH=, you can install Juvix as follows: #+begin_src shell @@ -68,8 +68,8 @@ The C compiler and linker paths can be specified as options to the =make install 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 +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 @@ -80,7 +80,7 @@ brew install --build-from-source --HEAD juvix --verbose We recommend to use the =stack= build tool with this project. -If you would prefer to use the =cabal= build tool instead then you must generate +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: diff --git a/docs/org/quick-start.org b/docs/org/quick-start.org index 5676da95da..bb5e22305e 100644 --- a/docs/org/quick-start.org +++ b/docs/org/quick-start.org @@ -8,7 +8,7 @@ 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 available. +After installation, run =juvix --help= to see the list of commands. Run Juvix doctor to check your system setup: diff --git a/docs/org/reference/language/README.org b/docs/org/reference/language/README.org index 9e334ca228..a3219dc7d3 100644 --- a/docs/org/reference/language/README.org +++ b/docs/org/reference/language/README.org @@ -1,7 +1,7 @@ + - [[./functions.md][Functions]] + - [[./datatypes.md][Data types]] + - [[./modules.md][Modules]] - [[./comments.md][Comments]] - - [[./axiom.md][Axiom]] - - [[./functions.md][Function]] - - [[./modules.md][Module System]] - - [[./datatypes.md][Inductive data types]] + - [[./axioms.md][Axioms]] - [[./compileblocks.md][Compile blocks]] - [[./foreign.md][Foreign blocks]] diff --git a/docs/org/reference/language/axiom.org b/docs/org/reference/language/axioms.org similarity index 100% rename from docs/org/reference/language/axiom.org rename to docs/org/reference/language/axioms.org diff --git a/docs/org/reference/language/datatypes.org b/docs/org/reference/language/datatypes.org index 893b379cb9..d320ddadaa 100644 --- a/docs/org/reference/language/datatypes.org +++ b/docs/org/reference/language/datatypes.org @@ -1,22 +1,20 @@ -* Inductive data types +* 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. +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 inductive type is the =Unit= type with one constructor called =unit=. +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 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. +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 := @@ -24,8 +22,7 @@ type 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. +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 inifl 6 +; @@ -34,12 +31,9 @@ inifl 6 +; + (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: +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 ::; @@ -52,5 +46,5 @@ 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]] +For more examples of inductive types and how to use them, see +[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]]. diff --git a/docs/org/reference/language/functions.org b/docs/org/reference/language/functions.org index 5d97905aa4..c84c6c83e0 100644 --- a/docs/org/reference/language/functions.org +++ b/docs/org/reference/language/functions.org @@ -1,9 +1,8 @@ * Function declaration -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; From 1cdf80b9f64fbb4838ead1af5498e6aa44a25c0d Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 16 Jan 2023 18:52:07 +0100 Subject: [PATCH 4/9] tutorial wip --- Makefile | 3 +- README.org | 26 +- docs/org/SUMMARY.org | 2 +- docs/org/quick-start.org | 2 +- docs/org/reference/language/functions.org | 2 +- docs/org/tutorials/learn.org | 455 +++++++++++++++++++++ examples/milestone/Tutorial/Tutorial.juvix | 24 ++ 7 files changed, 495 insertions(+), 19 deletions(-) create mode 100644 examples/milestone/Tutorial/Tutorial.juvix diff --git a/Makefile b/Makefile index b99b143683..e29c598136 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,8 @@ EXAMPLES= HelloWorld/HelloWorld.juvix \ Hanoi/Hanoi.juvix \ PascalsTriangle/PascalsTriangle.juvix \ TicTacToe/CLI/TicTacToe.juvix \ - ValidityPredicates/SimpleFungibleToken.juvix + ValidityPredicates/SimpleFungibleToken.juvix \ + Tutorial/Tutorial.juvix EXAMPLE_WEBAPP_OUTPUT=_docs/examples/webapp WEBAPP_EXAMPLES=TicTacToe/Web/TicTacToe.juvix diff --git a/README.org b/README.org index bbddca73ae..61c0186463 100644 --- a/README.org +++ b/README.org @@ -52,12 +52,12 @@ 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: @@ -69,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 diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org index 1c0d2c341b..85c8bd73c2 100644 --- a/docs/org/SUMMARY.org +++ b/docs/org/SUMMARY.org @@ -5,7 +5,7 @@ - [[./quick-start.md][Quick start]] * Tutorials -- [[./tutorials/learn.md][Learn Juvix in X minutes]] +- [[./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]] diff --git a/docs/org/quick-start.org b/docs/org/quick-start.org index bb5e22305e..5fa774900b 100644 --- a/docs/org/quick-start.org +++ b/docs/org/quick-start.org @@ -65,7 +65,7 @@ module HelloWorld; open import Stdlib.Prelude; main : IO; -main := putStrLn "hello world!"; +main := printStringLn "hello world!"; end; #+end_src diff --git a/docs/org/reference/language/functions.org b/docs/org/reference/language/functions.org index c84c6c83e0..ca3c6a1f3e 100644 --- a/docs/org/reference/language/functions.org +++ b/docs/org/reference/language/functions.org @@ -1,4 +1,4 @@ -* Function declaration +* Function declarations A function declaration consists of a type signature and a group of /function clauses/. diff --git a/docs/org/tutorials/learn.org b/docs/org/tutorials/learn.org index e69de29bb2..ebb7044702 100644 --- a/docs/org/tutorials/learn.org +++ b/docs/org/tutorials/learn.org @@ -0,0 +1,455 @@ +* Juvix tutorial + +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= and so on 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 condiditional =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 implict 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 recusively 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 is possible to /partially apply/ it to a smaller number of arguments than specified in its definition. The result is an approriate 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 can be inferred in a function application. However, sometimes this is not possible and then they need to be provided manually by enclosing them in braces: =f {implArg1} .. {implArgK} arg1 .. argN=. For example, =nil {Nat}= has type =List Nat= while =nil= by itself has type ={A : Type} -> List A=. + +** Tail recursion + +Any recursive call whose result is further processed by the calling function needs to create a new stack frame to save the calling function environment. This means that each such call will use a constant amount of memory. For example, a function =sum= implemented as follows will use an additional amount of memory proportional to the length of the processed list: +#+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. + +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. + +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)@\{ } +#+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 following =plusOne= function 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. +#+begin_example +plusOne : NList -> NList; +plusOne nnil := nnil; +plusOne (ncons x xs) := ncons (x + 1) (plusOne xs); +#+end_example + +** Totality checking + +By default, the Juvix compiler requires all functions to be total. Totality checking consists of: + * termination checking, + * coverage checking. + +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 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, this is not possible. Then one can use the =terminating= keyword to forgoe the termination check. +#+begin_example +log2 : Nat -> Nat; +log2 n := if (n <= 1) 0 (1 + log2 (div n 2)); +#+end_example + +Coverage checking ensures that there are no unhandles 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]]. + +TODO diff --git a/examples/milestone/Tutorial/Tutorial.juvix b/examples/milestone/Tutorial/Tutorial.juvix new file mode 100644 index 0000000000..1ac3a1fe76 --- /dev/null +++ b/examples/milestone/Tutorial/Tutorial.juvix @@ -0,0 +1,24 @@ +module Tutorial; + +{- + +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. + +-} + +-- 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; + +-- A monomorphic list of natural numbers. +type NatList := +| NatNil : NatList +| NatCons : Nat → NatList → NatList; + +main : IO; +main := printStringLn "Hello world!"; + +end; From cba2b97a7bcc6400a89e293fee5550ff44b00269 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 18 Jan 2023 11:15:13 +0100 Subject: [PATCH 5/9] Tutorial finished --- docs/org/tutorials/learn.org | 97 ++++++++++++++++++++++++++++-------- 1 file changed, 77 insertions(+), 20 deletions(-) diff --git a/docs/org/tutorials/learn.org b/docs/org/tutorials/learn.org index ebb7044702..b632f366a4 100644 --- a/docs/org/tutorials/learn.org +++ b/docs/org/tutorials/learn.org @@ -1,6 +1,25 @@ * Juvix tutorial -After [[./howto/installing.md][installing Juvix]], launch the Juvix REPL: +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 @@ -133,7 +152,7 @@ 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= and so on are just shorthands for appropriate expressions built using =suc= and =zero=. +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 @@ -296,7 +315,7 @@ The definition of =mirror= follows the definition of =Tree=. There are two recur 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 is possible to /partially apply/ it to a smaller number of arguments than specified in its definition. The result is an approriate 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. +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 approriate 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 @@ -336,7 +355,11 @@ This function has two /implicit type arguments/ =A= and =B=. These arguments are 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 can be inferred in a function application. However, sometimes this is not possible and then they need to be provided manually by enclosing them in braces: =f {implArg1} .. {implArgK} arg1 .. argN=. For example, =nil {Nat}= has type =List Nat= while =nil= by itself has type ={A : Type} -> List A=. +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 @@ -355,9 +378,9 @@ while (lst /= nnil) { }; 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. +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: +The following implementation of =sum= uses tail recursion. #+begin_example sum : NList -> Nat; sum lst := let { @@ -367,7 +390,7 @@ sum lst := let { } 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 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 @@ -411,34 +434,31 @@ 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 following =plusOne= function 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. -#+begin_example -plusOne : NList -> NList; -plusOne nnil := nnil; -plusOne (ncons x xs) := ncons (x + 1) (plusOne xs); -#+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 checking consists of: - * termination checking, - * coverage 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 pattern matched on in the clause. One can reformulate this definition so that it is accepted by the termination checker: +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, this is not possible. Then one can use the =terminating= keyword to forgoe the termination check. +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 (1 + log2 (div n 2)); +log2 n := if (n <= 1) 0 (suc (log2 (div n 2))); #+end_example Coverage checking ensures that there are no unhandles patterns in function clauses or =case= expressions. For example, the following definition is rejected because the case =suc zero= is not handled: @@ -452,4 +472,41 @@ even (suc (suc n)) := even n; 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]]. -TODO +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=. From 63e24703d9d09a2423140a46679cfbbb9ee497a4 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 18 Jan 2023 11:22:11 +0100 Subject: [PATCH 6/9] fix images --- docs/org/quick-start.org | 4 ++-- examples/milestone/Tutorial/Tutorial.juvix | 7 ++----- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/docs/org/quick-start.org b/docs/org/quick-start.org index 5fa774900b..96b3f4573d 100644 --- a/docs/org/quick-start.org +++ b/docs/org/quick-start.org @@ -2,11 +2,11 @@ #+begin_html -Juvix Mascot +Juvix Mascot #+end_html -To install Juvix, follow the instruction in the [[./howto/installing.md][Installation How-to]]. +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. diff --git a/examples/milestone/Tutorial/Tutorial.juvix b/examples/milestone/Tutorial/Tutorial.juvix index 1ac3a1fe76..0f5c6cd9dd 100644 --- a/examples/milestone/Tutorial/Tutorial.juvix +++ b/examples/milestone/Tutorial/Tutorial.juvix @@ -6,6 +6,8 @@ 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. +COMING SOON + -} -- import the standard library prelude and bring it into scope @@ -13,11 +15,6 @@ open import Stdlib.Prelude; -- bring comparison operators on Nat into scope open import Stdlib.Data.Nat.Ord; --- A monomorphic list of natural numbers. -type NatList := -| NatNil : NatList -| NatCons : Nat → NatList → NatList; - main : IO; main := printStringLn "Hello world!"; From 6a254ef2494a43b6e7453660ff6cdd0b8f1f2959 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Thu, 19 Jan 2023 11:33:59 +0100 Subject: [PATCH 7/9] Fixed some typos and add missing yaml file --- docs/org/howto/installing.org | 2 +- docs/org/reference/language/axioms.org | 2 +- docs/org/reference/language/builtins.org | 2 +- docs/org/reference/language/comments.org | 2 +- docs/org/reference/language/compileblocks.org | 4 ++-- docs/org/reference/language/datatypes.org | 2 +- docs/org/reference/language/foreign.org | 5 ----- docs/org/reference/language/modules.org | 4 ++-- docs/org/reference/tooling/CLI.org | 6 +----- docs/org/reference/tooling/doctor.org | 2 +- docs/org/tutorials/learn.org | 10 +++++----- examples/milestone/Tutorial/Tutorial.juvix | 13 ++++--------- examples/milestone/Tutorial/juvix.yaml | 2 ++ examples/milestone/ValidityPredicates/juvix.yaml | 2 ++ 14 files changed, 24 insertions(+), 34 deletions(-) create mode 100644 examples/milestone/Tutorial/juvix.yaml diff --git a/docs/org/howto/installing.org b/docs/org/howto/installing.org index 2c07c7db15..09a6b2a09c 100644 --- a/docs/org/howto/installing.org +++ b/docs/org/howto/installing.org @@ -40,7 +40,7 @@ brew info juvix 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 move it +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 diff --git a/docs/org/reference/language/axioms.org b/docs/org/reference/language/axioms.org index 98107591c9..aaf4bf98ad 100644 --- a/docs/org/reference/language/axioms.org +++ b/docs/org/reference/language/axioms.org @@ -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 diff --git a/docs/org/reference/language/builtins.org b/docs/org/reference/language/builtins.org index 40470ab516..29a65ee398 100644 --- a/docs/org/reference/language/builtins.org +++ b/docs/org/reference/language/builtins.org @@ -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; diff --git a/docs/org/reference/language/comments.org b/docs/org/reference/language/comments.org index 0160eb7b6b..f379953ed3 100644 --- a/docs/org/reference/language/comments.org +++ b/docs/org/reference/language/comments.org @@ -1,6 +1,6 @@ * Comments -A comment is introduced in the same fashion as in =Haskell= or =Agda=. +Comments follow the same syntax as in =Haskell= and =Agda=. Be aware, Juvix has no support for nested comments. - Inline Comment #+begin_src diff --git a/docs/org/reference/language/compileblocks.org b/docs/org/reference/language/compileblocks.org index 8b834a4c60..9450d073cc 100644 --- a/docs/org/reference/language/compileblocks.org +++ b/docs/org/reference/language/compileblocks.org @@ -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"; diff --git a/docs/org/reference/language/datatypes.org b/docs/org/reference/language/datatypes.org index d320ddadaa..54a4ba3dd8 100644 --- a/docs/org/reference/language/datatypes.org +++ b/docs/org/reference/language/datatypes.org @@ -25,7 +25,7 @@ type 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: #+begin_src text -inifl 6 +; +infixl 6 +; + : Nat -> Nat -> Nat; + zero b := b; + (suc a) b := suc (a + b); diff --git a/docs/org/reference/language/foreign.org b/docs/org/reference/language/foreign.org index 5cbe4edb68..3dffab2f0d 100644 --- a/docs/org/reference/language/foreign.org +++ b/docs/org/reference/language/foreign.org @@ -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 diff --git a/docs/org/reference/language/modules.org b/docs/org/reference/language/modules.org index b06e59e11a..d6e57e2af7 100644 --- a/docs/org/reference/language/modules.org +++ b/docs/org/reference/language/modules.org @@ -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. diff --git a/docs/org/reference/tooling/CLI.org b/docs/org/reference/tooling/CLI.org index ffc04ed500..d540b05843 100644 --- a/docs/org/reference/tooling/CLI.org +++ b/docs/org/reference/tooling/CLI.org @@ -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 diff --git a/docs/org/reference/tooling/doctor.org b/docs/org/reference/tooling/doctor.org index f9e79d6c79..6557693c5c 100644 --- a/docs/org/reference/tooling/doctor.org +++ b/docs/org/reference/tooling/doctor.org @@ -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 diff --git a/docs/org/tutorials/learn.org b/docs/org/tutorials/learn.org index b632f366a4..f92f6ca781 100644 --- a/docs/org/tutorials/learn.org +++ b/docs/org/tutorials/learn.org @@ -231,7 +231,7 @@ 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 condiditional =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. +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). @@ -267,7 +267,7 @@ 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 implict state are possible, because the state is always explicit. +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 @@ -283,7 +283,7 @@ 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 recusively call =nlength= on =xs= and add =1= to the result. +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 @@ -315,7 +315,7 @@ The definition of =mirror= follows the definition of =Tree=. There are two recur 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 approriate 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. +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 @@ -461,7 +461,7 @@ log2 : Nat -> Nat; log2 n := if (n <= 1) 0 (suc (log2 (div n 2))); #+end_example -Coverage checking ensures that there are no unhandles patterns in function clauses or =case= expressions. For example, the following definition is rejected because the case =suc zero= is not handled: +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; diff --git a/examples/milestone/Tutorial/Tutorial.juvix b/examples/milestone/Tutorial/Tutorial.juvix index 0f5c6cd9dd..2707c4b6fd 100644 --- a/examples/milestone/Tutorial/Tutorial.juvix +++ b/examples/milestone/Tutorial/Tutorial.juvix @@ -1,14 +1,9 @@ -module Tutorial; - -{- +--- 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. -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. - -COMING SOON +module Tutorial; --} -- import the standard library prelude and bring it into scope open import Stdlib.Prelude; diff --git a/examples/milestone/Tutorial/juvix.yaml b/examples/milestone/Tutorial/juvix.yaml new file mode 100644 index 0000000000..e61f4a5823 --- /dev/null +++ b/examples/milestone/Tutorial/juvix.yaml @@ -0,0 +1,2 @@ +name: Tutorial +version: 0.0.1 diff --git a/examples/milestone/ValidityPredicates/juvix.yaml b/examples/milestone/ValidityPredicates/juvix.yaml index e69de29bb2..a75e487d2f 100644 --- a/examples/milestone/ValidityPredicates/juvix.yaml +++ b/examples/milestone/ValidityPredicates/juvix.yaml @@ -0,0 +1,2 @@ +name: ValidityPredicates +version: 0.1.0 \ No newline at end of file From 634dee71c3dc7763855a5a21e3da868be374aac9 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Thu, 19 Jan 2023 11:39:34 +0100 Subject: [PATCH 8/9] Add missing yaml files --- examples/demo/juvix.yaml | 2 ++ examples/milestone/Collatz/juvix.yaml | 2 ++ examples/milestone/Fibonacci/juvix.yaml | 2 ++ examples/milestone/Hanoi/juvix.yaml | 2 ++ examples/milestone/HelloWorld/juvix.yaml | 2 ++ examples/milestone/PascalsTriangle/juvix.yaml | 2 ++ examples/milestone/TicTacToe/juvix.yaml | 4 ++-- examples/milestone/Tutorial/juvix.yaml | 2 +- examples/milestone/ValidityPredicates/juvix.yaml | 2 +- 9 files changed, 16 insertions(+), 4 deletions(-) diff --git a/examples/demo/juvix.yaml b/examples/demo/juvix.yaml index e69de29bb2..d28f81e92f 100644 --- a/examples/demo/juvix.yaml +++ b/examples/demo/juvix.yaml @@ -0,0 +1,2 @@ +name: Demo +version: 0.1.0 diff --git a/examples/milestone/Collatz/juvix.yaml b/examples/milestone/Collatz/juvix.yaml index e69de29bb2..e42822a936 100644 --- a/examples/milestone/Collatz/juvix.yaml +++ b/examples/milestone/Collatz/juvix.yaml @@ -0,0 +1,2 @@ +name: Collatz +version: 0.1.0 diff --git a/examples/milestone/Fibonacci/juvix.yaml b/examples/milestone/Fibonacci/juvix.yaml index e69de29bb2..80c88144a6 100644 --- a/examples/milestone/Fibonacci/juvix.yaml +++ b/examples/milestone/Fibonacci/juvix.yaml @@ -0,0 +1,2 @@ +name: Fibonacci +version: 0.1.0 diff --git a/examples/milestone/Hanoi/juvix.yaml b/examples/milestone/Hanoi/juvix.yaml index e69de29bb2..9de3cb6dac 100644 --- a/examples/milestone/Hanoi/juvix.yaml +++ b/examples/milestone/Hanoi/juvix.yaml @@ -0,0 +1,2 @@ +name: Hanoi +version: 0.1.0 diff --git a/examples/milestone/HelloWorld/juvix.yaml b/examples/milestone/HelloWorld/juvix.yaml index e69de29bb2..454325b4fe 100644 --- a/examples/milestone/HelloWorld/juvix.yaml +++ b/examples/milestone/HelloWorld/juvix.yaml @@ -0,0 +1,2 @@ +name: HelloWorld +version: 0.1.0 diff --git a/examples/milestone/PascalsTriangle/juvix.yaml b/examples/milestone/PascalsTriangle/juvix.yaml index e69de29bb2..e516228c15 100644 --- a/examples/milestone/PascalsTriangle/juvix.yaml +++ b/examples/milestone/PascalsTriangle/juvix.yaml @@ -0,0 +1,2 @@ +name: PascalsTriangle +version: 0.1.0 diff --git a/examples/milestone/TicTacToe/juvix.yaml b/examples/milestone/TicTacToe/juvix.yaml index 3d1e2d60be..723a49718e 100644 --- a/examples/milestone/TicTacToe/juvix.yaml +++ b/examples/milestone/TicTacToe/juvix.yaml @@ -1,2 +1,2 @@ -name: tic-tac-toe -version: 1.0.0 +name: TicTacToe +version: 0.1.0 diff --git a/examples/milestone/Tutorial/juvix.yaml b/examples/milestone/Tutorial/juvix.yaml index e61f4a5823..03bcb02a8f 100644 --- a/examples/milestone/Tutorial/juvix.yaml +++ b/examples/milestone/Tutorial/juvix.yaml @@ -1,2 +1,2 @@ name: Tutorial -version: 0.0.1 +version: 0.1.0 diff --git a/examples/milestone/ValidityPredicates/juvix.yaml b/examples/milestone/ValidityPredicates/juvix.yaml index a75e487d2f..67134a4998 100644 --- a/examples/milestone/ValidityPredicates/juvix.yaml +++ b/examples/milestone/ValidityPredicates/juvix.yaml @@ -1,2 +1,2 @@ name: ValidityPredicates -version: 0.1.0 \ No newline at end of file +version: 0.1.0 From 3e7a19c49f45fed8215330d71b0f3549aeda29a7 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Thu, 19 Jan 2023 11:44:30 +0100 Subject: [PATCH 9/9] Update Makefile --- Makefile | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Makefile b/Makefile index e29c598136..a36c282f8d 100644 --- a/Makefile +++ b/Makefile @@ -11,14 +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 \ - Tutorial/Tutorial.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 @@ -68,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)