mirror of
https://github.com/anoma/juvix.git
synced 2024-09-11 16:26:33 +03:00
* Add initial docs generation website (#119) * Add docs generation * [makefile] add serve-docs target * Fixed rebase conflicts * Update pre-commit rev * Added changelog
This commit is contained in:
parent
7e20e5083b
commit
7e309eccdb
64
.github/workflows/ci.yml
vendored
64
.github/workflows/ci.yml
vendored
@ -24,6 +24,33 @@ jobs:
|
||||
ready to review.
|
||||
run: exit 1
|
||||
|
||||
docs:
|
||||
runs-on: ubuntu-latest
|
||||
if: ${{ github.ref == 'refs/heads/master' }}
|
||||
steps:
|
||||
- name: Checkout our repository
|
||||
uses: actions/checkout@v2
|
||||
|
||||
- uses: r-lib/actions/setup-pandoc@v1
|
||||
with:
|
||||
pandoc-version: '2.13'
|
||||
|
||||
- name: MDBook setup
|
||||
uses: peaceiris/actions-mdbook@v1
|
||||
with:
|
||||
mdbook-version: 'latest'
|
||||
|
||||
- name: Generate Markdown files for each Org file
|
||||
run: make markdown-docs
|
||||
|
||||
- name: Deploy HTML to github pages
|
||||
uses: peaceiris/actions-gh-pages@v3
|
||||
with:
|
||||
github_token: ${{ secrets.GITHUB_TOKEN }}
|
||||
publish_dir: _docs
|
||||
enable_jekyll: false
|
||||
|
||||
|
||||
ormolu:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
@ -116,17 +143,13 @@ jobs:
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
path: main
|
||||
submodules: true
|
||||
|
||||
- name: Build Haskell Project
|
||||
run: |
|
||||
cd main
|
||||
make ci-build
|
||||
|
||||
- name: Download MiniJuvix-stdlib
|
||||
run: |
|
||||
cd main
|
||||
make minijuvix-stdlib
|
||||
|
||||
test:
|
||||
needs: build
|
||||
runs-on: ${{ matrix.os }}
|
||||
@ -179,34 +202,3 @@ jobs:
|
||||
run: |
|
||||
cd main
|
||||
make ci-test
|
||||
|
||||
docs:
|
||||
runs-on: ubuntu-latest
|
||||
if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
|
||||
steps:
|
||||
- name: Checkout our repository
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
path: main
|
||||
|
||||
- uses: r-lib/actions/setup-pandoc@v1
|
||||
with:
|
||||
pandoc-version: '2.13'
|
||||
|
||||
- name: Setup mdBook
|
||||
uses: peaceiris/actions-mdbook@v1
|
||||
with:
|
||||
mdbook-version: 'latest'
|
||||
|
||||
- name: Generate Markdown files for each Org file
|
||||
run: |
|
||||
cd main
|
||||
make markdown-docs
|
||||
|
||||
- name: Deploy
|
||||
uses: peaceiris/actions-gh-pages@v3
|
||||
if: ${{ github.ref == 'refs/heads/main' }}
|
||||
with:
|
||||
github_token: ${{ secrets.GITHUB_TOKEN }}
|
||||
publish_dir: main/_docs/
|
||||
enable_jekyll: false
|
||||
|
2
.gitignore
vendored
2
.gitignore
vendored
@ -69,5 +69,5 @@ UPDATES-FOR-CHANGELOG.org
|
||||
|
||||
# C Code generation
|
||||
*.wasm
|
||||
docs/**/*.md
|
||||
docs/md/
|
||||
_docs
|
||||
|
@ -15,7 +15,7 @@ repos:
|
||||
- id: mixed-line-ending
|
||||
|
||||
- repo: https://github.com/heliaxdev/minijuvix
|
||||
rev: f987ef1c13e75e6ed60e8e85c8afecb3f485e224
|
||||
rev: 6f5c3fc2bc70cf65594d3b74fb62e75e8fcfac5b
|
||||
hooks:
|
||||
- id: ormolu
|
||||
- id: hlint
|
||||
|
@ -7,5 +7,5 @@
|
||||
- id: ormolu
|
||||
name: ormolu
|
||||
description: Run Ormolu linter
|
||||
entry: make check-format
|
||||
entry: make check-ormolu
|
||||
language: system
|
||||
|
18
Makefile
18
Makefile
@ -3,11 +3,11 @@ PREFIX="$(PWD)/.stack-work/prefix"
|
||||
UNAME := $(shell uname)
|
||||
HLINTQUIET :=
|
||||
|
||||
ORGFILES = $(shell find docs/ -type f -name '*.org')
|
||||
MDFILES:=$(ORGFILES:.org=.md)
|
||||
ORGFILES = $(shell find docs/org -type f -name '*.org')
|
||||
MDFILES:=$(patsubst docs/org/%,docs/md/%,$(ORGFILES:.org=.md))
|
||||
|
||||
ORGTOMDPRG ?=pandoc
|
||||
ORGOPTS=--from org --to markdown --standalone -o $@
|
||||
ORGOPTS=--from org --to markdown_strict -s -o $@
|
||||
|
||||
# ORGTOMDPRG ?=emacs
|
||||
# ORGOPTS=--batch -f org-html-export-to-markdown
|
||||
@ -23,19 +23,19 @@ endif
|
||||
all:
|
||||
make pre-commit
|
||||
|
||||
docs/md/%.md : docs/org/%.org
|
||||
@echo "Processing ... $@"
|
||||
@mkdir -p $(dir $@)
|
||||
${ORGTOMDPRG} $? ${ORGOPTS}
|
||||
|
||||
.PHONY: markdown-docs
|
||||
markdown-docs: $(MDFILES)
|
||||
mdbook build
|
||||
|
||||
.PHONY: serve-docs
|
||||
serve-docs:
|
||||
make markdown-docs
|
||||
serve-docs: $(MDFILES)
|
||||
mdbook serve --open
|
||||
|
||||
%.md: %.org
|
||||
@echo "Processing ... $@"
|
||||
${ORGTOMDPRG} $? ${ORGOPTS}
|
||||
|
||||
.PHONY : checklines
|
||||
checklines :
|
||||
@grep '.\{81,\}' \
|
||||
|
51
README.org
51
README.org
@ -53,57 +53,6 @@ If the installation succeeds, you must be able to run the =minijuvix=
|
||||
command from any location. To get the complete list of commands, please
|
||||
run =minijuvix --help=.
|
||||
|
||||
** Testing
|
||||
|
||||
*** Dependencies
|
||||
|
||||
The following dependencies are required for the WASM compiler tests.
|
||||
|
||||
- [[https://wasmer.io][wasmer]]
|
||||
- [[https://releases.llvm.org/download.html][Clang / LLVM]] (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
|
||||
|
||||
*** Running
|
||||
|
||||
Run tests using:
|
||||
|
||||
#+begin_src shell
|
||||
stack test
|
||||
#+end_src
|
||||
|
||||
To run tests, ignoring all the WASM tests:
|
||||
|
||||
#+begin_src shell
|
||||
stack test --ta '-p "! /slow tests/"'
|
||||
#+end_src
|
||||
|
||||
|
||||
** Usage Example
|
||||
|
@ -1,9 +1,9 @@
|
||||
[book]
|
||||
title = "MiniJuvix"
|
||||
title = "The MiniJuvix Book"
|
||||
authors = [ "Jonathan Prieto-Cubides" , "Jan Mas Rovira" , "Paul Cadman" ]
|
||||
language = "en"
|
||||
multilingual = false
|
||||
src = "docs"
|
||||
src = "docs/md/"
|
||||
|
||||
[build]
|
||||
build-dir = "_docs"
|
||||
|
@ -1,3 +0,0 @@
|
||||
* Summary
|
||||
|
||||
- [[./developer-tooling.md][Developer Tooling 1]]
|
@ -1,55 +0,0 @@
|
||||
#+TITLE: Developer Tooling
|
||||
|
||||
** Emacs mode
|
||||
|
||||
There is an Emacs mode available for MiniJuvix. Currently, it
|
||||
supports syntax highlighting for well-scoped modules.
|
||||
|
||||
To install it add the following lines to your Emacs configuration file:
|
||||
|
||||
#+begin_src elisp
|
||||
(push "/path/to/minijuvix/minijuvix-mode/" load-path)
|
||||
(require 'minijuvix-mode)
|
||||
#+end_src
|
||||
|
||||
Make sure that =minijuvix= is installed in your =PATH=.
|
||||
|
||||
The MiniJuvix major mode will be activated automatically for =.mjuvix= files.
|
||||
|
||||
*** Keybindings
|
||||
|
||||
| Key | Function Name | Description |
|
||||
|-----------+------------------+-------------------------------------------------------|
|
||||
| =C-c C-l= | =minijuvix-load= | Runs the scoper and adds semantic syntax highlighting |
|
||||
|
||||
** CLI Auto-completion Scripts
|
||||
|
||||
The MiniJuvix CLI can generate auto-completion scripts. Follow the instructions below for your shell.
|
||||
|
||||
NB: You may need to restart your shell after installing the completion script.
|
||||
|
||||
*** Bash
|
||||
|
||||
Add the following line to your bash init script (for example =~/.bashrc=).
|
||||
|
||||
#+begin_src shell
|
||||
eval "$(minijuvix --bash-completion-script minijuvix)"
|
||||
#+end_src
|
||||
|
||||
*** Fish
|
||||
|
||||
Run the following command in your shell:
|
||||
|
||||
#+begin_src shell
|
||||
minijuvix --fish-completion-script minijuvix > ~/.config/fish/completions/minijuvix.fish
|
||||
#+end_src
|
||||
|
||||
*** ZSH
|
||||
|
||||
Run the following command in your shell:
|
||||
|
||||
#+begin_src shell
|
||||
minijuvix --zsh-completion-script minijuvix > $DIR_IN_FPATH/_minijuvix
|
||||
#+end_src
|
||||
|
||||
where =$DIR_IN_FPATH= is a directory that is present on the [[https://zsh.sourceforge.io/Doc/Release/Functions.html][ZSH FPATH variable]] (which you can inspect by running =echo $FPATH= in the shell).
|
36
docs/org/SUMMARY.org
Normal file
36
docs/org/SUMMARY.org
Normal file
@ -0,0 +1,36 @@
|
||||
* Summary
|
||||
|
||||
- [[./introduction/about/what-is.md][MiniJuvix]]
|
||||
- [[./introduction/changelog.md][Changelog]]
|
||||
- [[./introduction/getting-started.md][Getting started]]
|
||||
- [[./examples/README.md][Examples]]
|
||||
- [[./examples/backend-specific/minic-hello-world.md][Hello world]]
|
||||
- [[./examples/validity-predicates/PolyFungibleToken.md][Fungible Token]]
|
||||
|
||||
- [[./language-reference/README.md][Language reference]]
|
||||
- [[./language-reference/comments.md][Comments]]
|
||||
- [[./language-reference/axiom.md][Axiom]]
|
||||
- [[./language-reference/functions.md][Function]]
|
||||
- [[./language-reference/modules.md][Module System]]
|
||||
- [[./language-reference/inductive-data-types.md][Inductive data type]]
|
||||
- [[./language-reference/termination-checking.md][Termination checking]]
|
||||
- [[./language-reference/compile-blocks.md][Compile block]]
|
||||
- [[./language-reference/foreign-blocks.md][Foreign block]]
|
||||
- [[./backends/README.md][Backends]]
|
||||
- [[./backends/minic.md][MiniC backend]]
|
||||
- [[./backends/minihaskell.md][MiniHaskell backend]]
|
||||
- [[./compiler-architecture/README][Compiler architecture]]
|
||||
- [[./compiler-architecture/pipeline.md][Pipeline]]
|
||||
- [[./compiler-architecture/languages.md][Internal languages]]
|
||||
- [[./compiler-architecture/language/abstract.md][Abstract Language]]
|
||||
- [[./compiler-architecture/language/concrete.md][Concrete language]]
|
||||
- [[./compiler-architecture/language/microjuvix.md][MicroJuvix Language]]
|
||||
|
||||
- [[./tooling/README.md][Tooling]]
|
||||
- [[./tools/CLI.md][Command line Interface]]
|
||||
- [[./tools/emacs-mode.md][Writting MiniJuvix programs with Emacs Mode]]
|
||||
- [[./tools/testing.md][Test Suite]]
|
||||
|
||||
- [[./introduction/about/what-is.md][About]]
|
||||
- [[./introduction/about/team.md][The Dev Team]]
|
||||
- [[./introduction/about/community.md][Community]]
|
2
docs/org/backends/README.org
Normal file
2
docs/org/backends/README.org
Normal file
@ -0,0 +1,2 @@
|
||||
- [[./backends/minic.md][MiniC backend]]
|
||||
- [[./backends/minihaskell.md][MiniHaskell backend]]
|
1
docs/org/backends/minic.org
Normal file
1
docs/org/backends/minic.org
Normal file
@ -0,0 +1 @@
|
||||
* MiniC Backend
|
1
docs/org/backends/minihaskell.org
Normal file
1
docs/org/backends/minihaskell.org
Normal file
@ -0,0 +1 @@
|
||||
* MiniHaskell Backend
|
1
docs/org/compiler-architecture/language/abstract.org
Normal file
1
docs/org/compiler-architecture/language/abstract.org
Normal file
@ -0,0 +1 @@
|
||||
* Abstract Internal Language
|
1
docs/org/compiler-architecture/language/concrete.org
Normal file
1
docs/org/compiler-architecture/language/concrete.org
Normal file
@ -0,0 +1 @@
|
||||
* Concrete Internal Language
|
1
docs/org/compiler-architecture/language/microjuvix.org
Normal file
1
docs/org/compiler-architecture/language/microjuvix.org
Normal file
@ -0,0 +1 @@
|
||||
* MicroJuvix Internal Language
|
7
docs/org/compiler-architecture/languages.org
Normal file
7
docs/org/compiler-architecture/languages.org
Normal file
@ -0,0 +1,7 @@
|
||||
* Internal MiniJuvix languages
|
||||
|
||||
** Languages
|
||||
|
||||
- [[./compiler-architecture/language/abstract.md][Abstract Language]]
|
||||
- [[./compiler-architecture/language/concrete.md][Concrete language]]
|
||||
- [[./compiler-architecture/language/microjuvix.md][MicroJuvix Language]]
|
1
docs/org/compiler-architecture/pipeline.org
Normal file
1
docs/org/compiler-architecture/pipeline.org
Normal file
@ -0,0 +1 @@
|
||||
* Pipeline
|
2
docs/org/examples/README.org
Normal file
2
docs/org/examples/README.org
Normal file
@ -0,0 +1,2 @@
|
||||
- [[./examples/backend-specific/minic-hello-world.md][Hello world]]
|
||||
- [[./examples/validity-predicates/PolyFungibleToken.md][Fungible Token]]
|
44
docs/org/examples/backend-specific/minic-hello-world.org
Normal file
44
docs/org/examples/backend-specific/minic-hello-world.org
Normal file
@ -0,0 +1,44 @@
|
||||
* Mini C Hello World
|
||||
|
||||
In the following example a MiniJuvix file is compiled using the C backend.
|
||||
|
||||
#+begin_src
|
||||
-- tests/positive/MiniC/HelloWorld/Input.mjuvix
|
||||
module Input;
|
||||
|
||||
axiom String : Type;
|
||||
|
||||
compile String {
|
||||
c ↦ "char*";
|
||||
};
|
||||
|
||||
axiom Action : Type;
|
||||
|
||||
compile Action {
|
||||
c ↦ "int";
|
||||
};
|
||||
|
||||
axiom put-str-ln : String → Action;
|
||||
|
||||
compile put-str-ln {
|
||||
c ↦ "putStrLn";
|
||||
};
|
||||
|
||||
main : Action;
|
||||
main ≔ put-str-ln "hello world!";
|
||||
|
||||
end;
|
||||
#+end_src
|
||||
|
||||
|
||||
The result is compiled to WASM using [[https://llvm.org][Clang]] and then executed using [[https://wasmer.io][wasmer]].
|
||||
|
||||
NB: Set the =WASI_SYSROOT_PATH= environment variable to the root of the WASI sysroot. See [[#Dependencies][Dependencies]] for instructions on how to install the sysroot.
|
||||
|
||||
#+begin_src shell
|
||||
cd tests/positive/MiniC/HelloWorld
|
||||
minijuvix minic Input.mjuvix | clang --target=wasm32-wasi -nodefaultlibs -lc --sysroot $WASI_SYSROOT_PATH -I../../../../minic-runtime/libc -x c - -o out.wasm && wasmer out.wasm
|
||||
#+end_src
|
||||
|
||||
#+RESULTS:
|
||||
: hello world!
|
334
docs/org/examples/validity-predicates/PolyFungibleToken.org
Normal file
334
docs/org/examples/validity-predicates/PolyFungibleToken.org
Normal file
@ -0,0 +1,334 @@
|
||||
# Polymorphic simple fungible token
|
||||
|
||||
#+begin_src
|
||||
-- tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix
|
||||
module PolySimpleFungibleToken;
|
||||
|
||||
foreign ghc {
|
||||
import Anoma
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Booleans
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Bool {
|
||||
true : Bool;
|
||||
false : Bool;
|
||||
};
|
||||
|
||||
infixr 2 ||;
|
||||
|| : Bool → Bool → Bool;
|
||||
|| false a ≔ a;
|
||||
|| true _ ≔ true;
|
||||
|
||||
infixr 3 &&;
|
||||
&& : Bool → Bool → Bool;
|
||||
&& false _ ≔ false;
|
||||
&& true a ≔ a;
|
||||
|
||||
if : (A : Type) → Bool → A → A → A;
|
||||
if _ true a _ ≔ a;
|
||||
if _ false _ b ≔ b;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Backend Booleans
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom BackendBool : Type;
|
||||
|
||||
compile BackendBool {
|
||||
ghc ↦ "Bool";
|
||||
};
|
||||
|
||||
axiom backend-true : BackendBool;
|
||||
compile backend-true {
|
||||
ghc ↦ "True";
|
||||
};
|
||||
|
||||
axiom backend-false : BackendBool;
|
||||
compile backend-false {
|
||||
ghc ↦ "False";
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Backend Bridge
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
foreign ghc {
|
||||
bool :: Bool -> a -> a -> a
|
||||
bool True x _ = x
|
||||
bool False _ y = y
|
||||
};
|
||||
|
||||
axiom bool : BackendBool → Bool → Bool → Bool;
|
||||
compile bool {
|
||||
ghc ↦ "bool";
|
||||
};
|
||||
|
||||
from-backend-bool : BackendBool → Bool;
|
||||
from-backend-bool bb ≔ bool bb true false;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
const : (A : Type) → (B : Type) → A → B → A;
|
||||
const _ _ a _ ≔ a;
|
||||
|
||||
id : (A : Type) → A → A;
|
||||
id _ a ≔ a;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Integers
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom Int : Type;
|
||||
compile Int {
|
||||
ghc ↦ "Int";
|
||||
};
|
||||
|
||||
infix 4 <';
|
||||
axiom <' : Int → Int → BackendBool;
|
||||
compile <' {
|
||||
ghc ↦ "(<)";
|
||||
};
|
||||
|
||||
infix 4 <;
|
||||
< : Int → Int → Bool;
|
||||
< i1 i2 ≔ from-backend-bool (i1 <' i2);
|
||||
|
||||
axiom eqInt : Int → Int → BackendBool;
|
||||
compile eqInt {
|
||||
ghc ↦ "(==)";
|
||||
};
|
||||
|
||||
infix 4 ==Int;
|
||||
==Int : Int → Int → Bool;
|
||||
==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
|
||||
|
||||
infixl 6 -;
|
||||
axiom - : Int -> Int -> Int;
|
||||
compile - {
|
||||
ghc ↦ "(-)";
|
||||
};
|
||||
|
||||
infixl 6 +;
|
||||
axiom + : Int -> Int -> Int;
|
||||
compile + {
|
||||
ghc ↦ "(+)";
|
||||
};
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Strings
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom String : Type;
|
||||
compile String {
|
||||
ghc ↦ "[Char]";
|
||||
};
|
||||
|
||||
axiom eqString : String → String → BackendBool;
|
||||
compile eqString {
|
||||
ghc ↦ "(==)";
|
||||
};
|
||||
|
||||
infix 4 ==String;
|
||||
==String : String → String → Bool;
|
||||
==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Lists
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive List (A : Type) {
|
||||
nil : List A;
|
||||
cons : A → List A → List A;
|
||||
};
|
||||
|
||||
elemGen : (A : Type) → (A → A → Bool) → A → List A → Bool;
|
||||
elemGen _ _ _ nil ≔ false;
|
||||
elemGen A eq s (cons x xs) ≔ eq s x || elemGen A eq s xs;
|
||||
|
||||
elem : String → List String → Bool;
|
||||
elem s l ≔ elemGen String (==String) s l;
|
||||
|
||||
foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
|
||||
foldl _ _ f z nil ≔ z;
|
||||
foldl A B f z (cons h hs) ≔ foldl A B f (f z h) hs;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Pair
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- inductive PairIntBool {
|
||||
-- MakePair : Int → Bool → PairIntBool;
|
||||
-- };
|
||||
|
||||
inductive Pair (A : Type) (B : Type) {
|
||||
mkPair : A → B → Pair A B;
|
||||
};
|
||||
|
||||
if-pairIntBool : Bool → Pair Int Bool → Pair Int Bool → Pair Int Bool;
|
||||
if-pairIntBool ≔ if (Pair Int Bool);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Maybe
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
inductive Maybe (A : Type) {
|
||||
nothing : Maybe A;
|
||||
just : A → Maybe A;
|
||||
};
|
||||
|
||||
if-optionInt : Bool → Maybe Int → Maybe Int → Maybe Int;
|
||||
if-optionInt ≔ if (Maybe Int);
|
||||
|
||||
from-int : Int → Maybe Int;
|
||||
from-int i ≔ if-optionInt (i < 0) (nothing Int) (just Int i);
|
||||
|
||||
maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
|
||||
maybe _ _ b _ nothing ≔ b;
|
||||
maybe _ _ _ f (just x) ≔ f x;
|
||||
|
||||
maybe-int : Int → Maybe Int → Int;
|
||||
maybe-int d ≔ maybe Int Int d (id Int);
|
||||
|
||||
if-optionString : Bool → Maybe String → Maybe String → Maybe String;
|
||||
if-optionString ≔ if (Maybe String);
|
||||
|
||||
from-string : String → Maybe String;
|
||||
from-string s ≔ if-optionString (s ==String "") (nothing String) (just String s);
|
||||
|
||||
pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
|
||||
pair-from-optionString ≔ maybe String (Pair Int Bool) (mkPair Int Bool 0 false);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- foldl
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
foldl' : (Pair Int Bool → String → Pair Int Bool) → Pair Int Bool → List String → Pair Int Bool;
|
||||
foldl' ≔ foldl String (Pair Int Bool) ;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Anoma
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom readPre : String → Int;
|
||||
compile readPre {
|
||||
ghc ↦ "readPre";
|
||||
};
|
||||
|
||||
axiom readPost : String → Int;
|
||||
compile readPost {
|
||||
ghc ↦ "readPost";
|
||||
};
|
||||
|
||||
axiom isBalanceKey : String → String → String;
|
||||
compile isBalanceKey {
|
||||
ghc ↦ "isBalanceKey";
|
||||
};
|
||||
|
||||
read-pre : String → Maybe Int;
|
||||
read-pre s ≔ from-int (readPre s);
|
||||
|
||||
read-post : String → Maybe Int;
|
||||
read-post s ≔ from-int (readPost s);
|
||||
|
||||
is-balance-key : String → String → Maybe String;
|
||||
is-balance-key token key ≔ from-string (isBalanceKey token key);
|
||||
|
||||
unwrap-default : Maybe Int → Int;
|
||||
unwrap-default o ≔ maybe-int 0 o;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Validity Predicate
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
change-from-key : String → Int;
|
||||
change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
|
||||
|
||||
check-vp : List String → String → Int → String → Pair Int Bool;
|
||||
check-vp verifiers key change owner ≔
|
||||
if-pairIntBool
|
||||
(change-from-key key < 0)
|
||||
-- make sure the spender approved the transaction
|
||||
(mkPair Int Bool (change + (change-from-key key)) (elem owner verifiers))
|
||||
(mkPair Int Bool (change + (change-from-key key)) true);
|
||||
|
||||
check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
|
||||
check-keys token verifiers (mkPair change is-success) key ≔
|
||||
if-pairIntBool
|
||||
is-success
|
||||
(pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
|
||||
(mkPair Int Bool 0 false);
|
||||
|
||||
check-result : Pair Int Bool → Bool;
|
||||
check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
|
||||
|
||||
vp : String → List String → List String → Bool;
|
||||
vp token keys-changed verifiers ≔
|
||||
check-result
|
||||
(foldl'
|
||||
(check-keys token verifiers)
|
||||
(mkPair Int Bool 0 true)
|
||||
keys-changed);
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- IO
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
axiom Action : Type;
|
||||
compile Action {
|
||||
ghc ↦ "IO ()";
|
||||
};
|
||||
|
||||
axiom putStr : String → Action;
|
||||
compile putStr {
|
||||
ghc ↦ "putStr";
|
||||
};
|
||||
|
||||
axiom putStrLn : String → Action;
|
||||
compile putStrLn {
|
||||
ghc ↦ "putStrLn";
|
||||
};
|
||||
|
||||
infixl 1 >>;
|
||||
axiom >> : Action → Action → Action;
|
||||
compile >> {
|
||||
ghc ↦ "(>>)";
|
||||
};
|
||||
|
||||
show-result : Bool → String;
|
||||
show-result true ≔ "OK";
|
||||
show-result false ≔ "FAIL";
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Testing VP
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
token : String;
|
||||
token ≔ "owner-token";
|
||||
|
||||
owner-address : String;
|
||||
owner-address ≔ "owner-address";
|
||||
|
||||
change1-key : String;
|
||||
change1-key ≔ "change1-key";
|
||||
|
||||
change2-key : String;
|
||||
change2-key ≔ "change2-key";
|
||||
|
||||
verifiers : List String;
|
||||
verifiers ≔ cons String owner-address (nil String);
|
||||
|
||||
keys-changed : List String;
|
||||
keys-changed ≔ cons String change1-key (cons String change2-key (nil String));
|
||||
|
||||
main : Action;
|
||||
main ≔
|
||||
(putStr "VP Status: ")
|
||||
>> (putStrLn (show-result (vp token keys-changed verifiers)));
|
||||
|
||||
end;
|
||||
#+end_src
|
8
docs/org/introduction/about/community.org
Normal file
8
docs/org/introduction/about/community.org
Normal file
@ -0,0 +1,8 @@
|
||||
* MiniJuvix community
|
||||
|
||||
We would love to hear what you think of MiniJuvix! Join us on
|
||||
[[https://discord.gg/nsGaCZzJ][Discord]]
|
||||
|
||||
This project is part of a bigger effort called [[https://anoma.net/][Anoma]].
|
||||
Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination.
|
||||
Join the [[https://anoma.net/community][Anoma project]].
|
1
docs/org/introduction/about/team.org
Normal file
1
docs/org/introduction/about/team.org
Normal file
@ -0,0 +1 @@
|
||||
* The MiniJuvix Dev Team
|
47
docs/org/introduction/about/what-is.org
Normal file
47
docs/org/introduction/about/what-is.org
Normal file
@ -0,0 +1,47 @@
|
||||
* MiniJuvix
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/minijuvix/blob/main/LICENSE">
|
||||
<img alt="LICENSE" src="https://img.shields.io/badge/license-GPL--3.0--only-blue.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml">
|
||||
<img alt="CI status" src="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/minijuvix/tags">
|
||||
<img alt="" src="https://img.shields.io/github/v/release/heliaxdev/minijuvix?include_prereleases" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/minijuvix/issues">
|
||||
<img alt="" src="https://img.shields.io/github/issues/heliaxdev/minijuvix" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/MiniJuvix">
|
||||
<img align="right" width="300" height="300" alt="MiniJuvix Mascot" src="https://juvix.org/_nuxt/img/seating-mascot.051c86a.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
|
||||
MiniJuvix is a pre-alpha programming language for writing efficient formally-verified
|
||||
[[https://anoma.network/blog/validity-predicates/][validity predicates]], which can be
|
||||
deployed to various distributed ledgers. MiniJuvix is part of the Anoma's Juvix Toolkit.
|
||||
At the moment, this is software released for experimentation and research purposes only as
|
||||
no warranty is provided or implied yet.
|
||||
|
||||
MiniJuvix aims to address many issues that we have experienced while trying to
|
||||
write and deploy decentralized applications present in the ecosystem of
|
||||
smart-contracts:
|
||||
|
||||
- the difficulty of adequate program verification,
|
||||
- the ceiling of compositional complexity,
|
||||
- the illegibility of execution costs, and
|
||||
- the lock-in to particular backends.
|
@ -1,8 +1,10 @@
|
||||
* The MiniJuvix Changelog
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: the-minijuvix-changelog
|
||||
:END:
|
||||
* Changelog
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/MiniJuvix">
|
||||
<img align="right" width="300" height="300" alt="MiniJuvix Mascot" src="https://juvix.org/_nuxt/img/greeting-mascot.ad540a1.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
** [[https://github.com/heliaxdev/minijuvix/tree/v0.1.3][v0.1.3]]
|
||||
(2022-05-05)
|
28
docs/org/introduction/getting-started.org
Normal file
28
docs/org/introduction/getting-started.org
Normal file
@ -0,0 +1,28 @@
|
||||
* Getting started
|
||||
|
||||
** Quick Start
|
||||
|
||||
#+begin_html
|
||||
<a href="https://github.com/heliaxdev/MiniJuvix">
|
||||
<img align="left" width="200" height="200" alt="MiniJuvix Mascot" src="https://juvix.org/_nuxt/img/teaching-mascot.f828959.svg" />
|
||||
</a>
|
||||
#+end_html
|
||||
|
||||
|
||||
To install MiniJuvix, you can download its sources using
|
||||
[[http://git-scm.com/][Git]] from the
|
||||
[[https://github.com/heliaxdev/minijuvix.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 https://github.com/heliaxdev/minijuvix.git
|
||||
cd minijuvix
|
||||
stack install
|
||||
#+end_src
|
||||
|
||||
If the installation succeeds, you must be able to run the =minijuvix=
|
||||
command from any location.
|
||||
|
||||
|
||||
To get the complete list of commands, please run =minijuvix --help=.
|
8
docs/org/language-reference/README.org
Normal file
8
docs/org/language-reference/README.org
Normal file
@ -0,0 +1,8 @@
|
||||
- [[./language-reference/comments.md][Comments]]
|
||||
- [[./language-reference/axiom.md][Axiom]]
|
||||
- [[./language-reference/functions.md][Function]]
|
||||
- [[./language-reference/modules.md][Module System]]
|
||||
- [[./language-reference/inductive-data-types.md][Inductive data type]]
|
||||
- [[./language-reference/termination-checking.md][Termination checking]]
|
||||
- [[./language-reference/compile-blocks.md][Compile block]]
|
||||
- [[./language-reference/foreign-blocks.md][Foreign block]]
|
18
docs/org/language-reference/axiom.org
Normal file
18
docs/org/language-reference/axiom.org
Normal file
@ -0,0 +1,18 @@
|
||||
* Axiom
|
||||
|
||||
An axiom/postulate can be introduced by using the =axiom= keyword.
|
||||
For example, let us imagine one wants to write a program that assumes
|
||||
$A$ is a type and there exist a term $x$ that inhabits $A$. Then the program would
|
||||
like like the following.
|
||||
|
||||
#+begin_src
|
||||
-- Example.mjuvix
|
||||
module Example;
|
||||
axiom A : Type;
|
||||
axom x : A;
|
||||
end;
|
||||
#+end_src
|
||||
|
||||
Terms introduced by the =axiom= keyword lack of any computational content. However,
|
||||
it is possible to attach a computational content to an axiom by giving compilation rules,
|
||||
see [[./language-reference/compile-blocks.md][Compile blocks]].
|
17
docs/org/language-reference/comments.org
Normal file
17
docs/org/language-reference/comments.org
Normal file
@ -0,0 +1,17 @@
|
||||
* Comments
|
||||
|
||||
A comment is introduced in the same fashion as in Haskell/Agda.
|
||||
|
||||
- Inline Comment
|
||||
#+begin_src
|
||||
-- This is a comment!
|
||||
#+end_src
|
||||
|
||||
- Region comment
|
||||
|
||||
#+begin_src
|
||||
{-
|
||||
This is a comment!
|
||||
|
||||
-}
|
||||
#+end_src
|
1
docs/org/language-reference/compile-blocks.org
Normal file
1
docs/org/language-reference/compile-blocks.org
Normal file
@ -0,0 +1 @@
|
||||
# Compile blocks
|
1
docs/org/language-reference/foreign-blocks.org
Normal file
1
docs/org/language-reference/foreign-blocks.org
Normal file
@ -0,0 +1 @@
|
||||
# Foreign blocks
|
22
docs/org/language-reference/functions.org
Normal file
22
docs/org/language-reference/functions.org
Normal file
@ -0,0 +1,22 @@
|
||||
* Function declaration
|
||||
|
||||
In MiniJuvix, a function declaration is a type signature /and/ a group
|
||||
of definitions called /function clauses/.
|
||||
|
||||
#+begin_example
|
||||
fun : A → B;
|
||||
fun case1 := ...;
|
||||
fun case2 := ...;
|
||||
fun case3 := ...;
|
||||
#+end_example
|
||||
|
||||
** Mutual recursive functions
|
||||
|
||||
#+begin_example
|
||||
|
||||
f : A -> A -> A;
|
||||
g : A -> A -> A;
|
||||
|
||||
g x y := f x x;
|
||||
f x y := g x (f x x);
|
||||
#+end_example
|
1
docs/org/language-reference/inductive-data-types.org
Normal file
1
docs/org/language-reference/inductive-data-types.org
Normal file
@ -0,0 +1 @@
|
||||
# Inductive data types
|
1
docs/org/language-reference/modules.org
Normal file
1
docs/org/language-reference/modules.org
Normal file
@ -0,0 +1 @@
|
||||
* Module system
|
26
docs/org/language-reference/termination-checking.org
Normal file
26
docs/org/language-reference/termination-checking.org
Normal file
@ -0,0 +1,26 @@
|
||||
* Termination checking
|
||||
|
||||
To not bring inconsistencies by function declarations, MiniJuvix
|
||||
requires that all function pass the termination checker.
|
||||
This check is called before the typechecking in the compilation pipeline.
|
||||
|
||||
|
||||
Since the former requirement is vital but often tricky to fulfill for programs
|
||||
in a total language like MiniJuvix. It is convenient to have
|
||||
a way to bypass the termination checking. The user may be certain their
|
||||
programs are terminating even when our termination checker algorithm can not
|
||||
see it. The termination checker is limited as it only accepts a subset
|
||||
of recursion functions. Our termination checker algorithm is a slightly modification
|
||||
of the algorithm for checking terminationg of the Foetus's language.
|
||||
|
||||
|
||||
To skip the termination checker, we introduced the =terminating= keyword
|
||||
to annotate a type signature as terminating. The syntax is the following.
|
||||
|
||||
#+begin_example
|
||||
terminating fun : A → B;
|
||||
#+end_example
|
||||
|
||||
Annotating a function as =terminating= means that /all/ its function clauses pass the termination
|
||||
checker's criterion. To skip the termination checker for mutual recursive functions, all the functions
|
||||
involved must be annotated as =terminating=, otherwise, the checker will complain.
|
83
docs/org/tooling/CLI.org
Normal file
83
docs/org/tooling/CLI.org
Normal file
@ -0,0 +1,83 @@
|
||||
* CLI
|
||||
|
||||
** Usage
|
||||
|
||||
#+begin_src shell
|
||||
minijuvix [Global options] ((-v|--version) | --show-root | COMMAND)
|
||||
#+end_src
|
||||
|
||||
** Informative options
|
||||
|
||||
- =-v,--version=
|
||||
Print the version and exit
|
||||
- =--show-root=
|
||||
Print the detected root of the project
|
||||
- =-h,--help=
|
||||
Show this help text
|
||||
|
||||
|
||||
** Global Command flags
|
||||
|
||||
- =--no-colors=
|
||||
Disable globally ANSI formatting
|
||||
- =--show-name-ids=
|
||||
Show the unique number of each identifier when pretty
|
||||
printing
|
||||
- =--only-errors=
|
||||
Only print errors in a uniform format (used by
|
||||
minijuvix-mode)
|
||||
|
||||
** Commands
|
||||
|
||||
- =parse=
|
||||
Parse a MiniJuvix file
|
||||
- =scope=
|
||||
Parse and scope a MiniJuvix file
|
||||
- =html=
|
||||
Generate HTML for a MiniJuvix file
|
||||
- =termination=
|
||||
Subcommands related to termination checking
|
||||
- =monojuvix=
|
||||
Translate a MiniJuvix file to MonoJuvix
|
||||
- =microjuvix=
|
||||
Subcommands related to MicroJuvix
|
||||
- =minihaskell=
|
||||
Translate a MiniJuvix file to MiniHaskell
|
||||
- =minic=
|
||||
Translate a MiniJuvix file to MiniC
|
||||
- =highlight=
|
||||
Highlight a MiniJuvix file
|
||||
|
||||
|
||||
** CLI Auto-completion Scripts
|
||||
|
||||
The MiniJuvix CLI can generate auto-completion scripts. Follow the instructions below for your shell.
|
||||
|
||||
NB: You may need to restart your shell after installing the completion script.
|
||||
|
||||
*** Bash
|
||||
|
||||
Add the following line to your bash init script (for example =~/.bashrc=).
|
||||
|
||||
#+begin_src shell
|
||||
eval "$(minijuvix --bash-completion-script minijuvix)"
|
||||
#+end_src
|
||||
|
||||
*** Fish
|
||||
|
||||
Run the following command in your shell:
|
||||
|
||||
#+begin_src shell
|
||||
minijuvix --fish-completion-script minijuvix
|
||||
> ~/.config/fish/completions/minijuvix.fish
|
||||
#+end_src
|
||||
|
||||
*** ZSH
|
||||
|
||||
Run the following command in your shell:
|
||||
|
||||
#+begin_src shell
|
||||
minijuvix --zsh-completion-script minijuvix > $DIR_IN_FPATH/_minijuvix
|
||||
#+end_src
|
||||
|
||||
where =$DIR_IN_FPATH= is a directory that is present on the [[https://zsh.sourceforge.io/Doc/Release/Functions.html][ZSH FPATH variable]] (which you can inspect by running =echo $FPATH= in the shell).
|
3
docs/org/tooling/README.org
Normal file
3
docs/org/tooling/README.org
Normal file
@ -0,0 +1,3 @@
|
||||
- [[./tools/CLI.md][Command line Interface]]
|
||||
- [[./tools/emacs-mode.md][Writting MiniJuvix programs with Emacs Mode]]
|
||||
- [[./tools/testing.md][Test Suite]]
|
22
docs/org/tooling/emacs-mode.org
Normal file
22
docs/org/tooling/emacs-mode.org
Normal file
@ -0,0 +1,22 @@
|
||||
** Emacs Mode
|
||||
|
||||
|
||||
There is an Emacs mode available for MiniJuvix. Currently, it
|
||||
supports syntax highlighting for well-scoped modules.
|
||||
|
||||
To install it add the following lines to your Emacs configuration file:
|
||||
|
||||
#+begin_src elisp
|
||||
(push "/path/to/minijuvix/minijuvix-mode/" load-path)
|
||||
(require 'minijuvix-mode)
|
||||
#+end_src
|
||||
|
||||
Make sure that =minijuvix= is installed in your =PATH=.
|
||||
|
||||
The MiniJuvix major mode will be activated automatically for =.mjuvix= files.
|
||||
|
||||
*** Keybindings
|
||||
|
||||
| Key | Function Name | Description |
|
||||
|-----------+------------------+-------------------------------------------------------|
|
||||
| =C-c C-l= | =minijuvix-load= | Runs the scoper and adds semantic syntax highlighting |
|
51
docs/org/tooling/testing.org
Normal file
51
docs/org/tooling/testing.org
Normal file
@ -0,0 +1,51 @@
|
||||
* Testing
|
||||
|
||||
*** Dependencies
|
||||
|
||||
The following dependencies are required for the WASM compiler tests.
|
||||
|
||||
- [[https://wasmer.io][wasmer]]
|
||||
- [[https://releases.llvm.org/download.html][Clang / LLVM]] (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
|
||||
|
||||
*** Running
|
||||
|
||||
Run tests using:
|
||||
|
||||
#+begin_src shell
|
||||
stack test
|
||||
#+end_src
|
||||
|
||||
To run tests, ignoring all the WASM tests:
|
||||
|
||||
#+begin_src shell
|
||||
stack test --ta '-p "! /slow tests/"'
|
||||
#+end_src
|
@ -1,4 +1,4 @@
|
||||
module NoLexOrde;
|
||||
module Loop;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user