Examples should be formatted and typechecked

.github/workflows/ci.yml

@@ -21,40 +21,15 @@ concurrency:
   group: "${{ github.workflow }}-${{ github.head_ref || github.run_id }}"
   cancel-in-progress: true
 env:
-  SKIP: ormolu
+  SKIP: ormolu format-juvix-examples
 
 jobs:
-<<<<<<< HEAD
-
   pre-commit:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - uses: actions/setup-python@v4
         with:
-          python-version: '3.11'
-      - uses: pre-commit/[email protected]
-
-  clang-format:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - uses: jidicula/[email protected]
-        with:
-          clang-format-version: '15'
-          check-path: runtime/src
-
-  ormolu:
-=======
-  pre-commit:
->>>>>>> 9606ba98 (w.i.p)
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-      - uses: mrkkrp/ormolu-action@v11
-        with:
-<<<<<<< HEAD
-=======
           python-version: "3.11"
       - uses: pre-commit/[email protected]
 
@@ -64,7 +39,6 @@ jobs:
       - uses: actions/checkout@v3
       - uses: mrkkrp/ormolu-action@v11
         with:
->>>>>>> 9606ba98 (w.i.p)
           version: 0.5.2.0
           extra-args: >-
             --ghc-opt -XDerivingStrategies --ghc-opt -XImportQualifiedPost
@@ -136,6 +110,12 @@ jobs:
           cd main
           make test
 
+      - name: Typecheck and format Juvix examples
+        if: ${{ success() }}
+        run: |
+          cd main
+          make -s juvix-format
+
       - name: Add ~/.local/bin to PATH
         run: |
           echo "$HOME/.local/bin" >> $GITHUB_PATH
@@ -243,11 +223,7 @@ jobs:
       - name: Deploy HTML to github pages
         uses: peaceiris/actions-gh-pages@v3
         with:
-<<<<<<< HEAD
-          github_token: '${{ secrets.GITHUB_TOKEN }}'
-=======
           github_token: "${{ secrets.GITHUB_TOKEN }}"
->>>>>>> 9606ba98 (w.i.p)
           publish_dir: main/book/html
           enable_jekyll: false
           cname: docs.juvix.org
@@ -270,10 +246,6 @@ jobs:
         run: |
           brew install icu4c
           brew link icu4c --force
-<<<<<<< HEAD
-
-=======
->>>>>>> 9606ba98 (w.i.p)
 
       - name: Download and extract wasi-sysroot
         run: >
@@ -322,6 +294,12 @@ jobs:
           make CC=$CC LIBTOOL=$LIBTOOL test
           make CC=$CC LIBTOOL=$LIBTOOL install
 
+      - name: Typecheck and format Juvix examples
+        if: ${{ success() }}
+        run: |
+          cd main
+          make -s juvix-format
+
       - name: Add ~/.local/bin to PATH
         run: |
           echo "$HOME/.local/bin" >> $GITHUB_PATH

.pre-commit-config.yaml

@@ -43,7 +43,13 @@ repos:
   - repo: local
     hooks:
       - id: ormolu
-        name: format Haskell code with ormolu
-        entry: make -s ormolu
+        name: check Haskell formatting with ormolu
+        entry: make -s check-ormolu
         language: system
         pass_filenames: false
+      - id: juvix-examples
+        name: typecheck and format Juvix examples
+        entry: make -s juvix-format
+        language: system
+        verbose: false
+        pass_filenames: false

examples/demo/Demo.juvix

@@ -1,59 +1,59 @@
 module Demo;
-  -- standard library prelude
-  open import Stdlib.Prelude;
-  -- for comparisons on natural numbers
-  open import Stdlib.Data.Nat.Ord;
-  -- for Ordering
-  open import Stdlib.Data.Ord;
-
-  even : Nat → Bool;
-  even zero := true;
-  even (suc zero) := false;
-  even (suc (suc n)) := even n;
-
-  even' : Nat → Bool;
-  even' n := mod n 2 == 0;
-
-  -- base 2 logarithm rounded down
-  terminating
-  log2 : Nat → Nat;
-  log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
-
-  type Tree (A : Type) :=
-    | leaf : A → Tree A
-    | node : A → Tree A → Tree A → Tree A;
-
-  mirror : {A : Type} → Tree A → Tree A;
-  mirror t@(leaf _) := t;
-  mirror (node x l r) := node x (mirror r) (mirror l);
-
-  tree : Tree Nat;
-  tree := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
-
-  preorder : {A : Type} → Tree A → List A;
-  preorder (leaf x) := x :: nil;
-  preorder (node x l r) :=
-    x :: nil ++ preorder l ++ preorder r;
-
-  terminating
-  sort : {A : Type} → (A → A → Ordering) → List A → List A;
-  sort _ nil := nil;
-  sort _ xs@(_ :: nil) := xs;
-  sort cmp xs :=
-    uncurry
-      (merge cmp)
-      (both (sort cmp) (splitAt (div (length xs) 2) xs));
-
-  printNatListLn : List Nat → IO;
-  printNatListLn nil := printStringLn "nil";
-  printNatListLn (x :: xs) :=
-    printNat x >> printString " :: " >> printNatListLn xs;
-
-  main : IO;
-  main :=
-    printStringLn "Hello!"
-      >> printNatListLn (preorder (mirror tree))
-      >> printNatListLn (sort compare (preorder (mirror tree)))
-      >> printNatLn (log2 3)
-      >> printNatLn (log2 130);
-end;
+
+-- standard library prelude
+open import Stdlib.Prelude;
+-- for comparisons on natural numbers
+open import Stdlib.Data.Nat.Ord;
+-- for Ordering
+open import Stdlib.Data.Ord;
+
+even : Nat → Bool;
+even zero := true;
+even (suc zero) := false;
+even (suc (suc n)) := even n;
+
+even' : Nat → Bool;
+even' n := mod n 2 == 0;
+
+-- base 2 logarithm rounded down
+terminating
+log2 : Nat → Nat;
+log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
+
+type Tree (A : Type) :=
+  | leaf : A → Tree A
+  | node : A → Tree A → Tree A → Tree A;
+
+mirror : {A : Type} → Tree A → Tree A;
+mirror t@(leaf _) := t;
+mirror (node x l r) := node x (mirror r) (mirror l);
+
+tree : Tree Nat;
+tree := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
+
+preorder : {A : Type} → Tree A → List A;
+preorder (leaf x) := x :: nil;
+preorder (node x l r) :=
+  x :: nil ++ preorder l ++ preorder r;
+
+terminating
+sort : {A : Type} → (A → A → Ordering) → List A → List A;
+sort _ nil := nil;
+sort _ xs@(_ :: nil) := xs;
+sort cmp xs :=
+  uncurry
+    (merge cmp)
+    (both (sort cmp) (splitAt (div (length xs) 2) xs));
+
+printNatListLn : List Nat → IO;
+printNatListLn nil := printStringLn "nil";
+printNatListLn (x :: xs) :=
+  printNat x >> printString " :: " >> printNatListLn xs;
+
+main : IO;
+main :=
+  printStringLn "Hello!"
+    >> printNatListLn (preorder (mirror tree))
+    >> printNatListLn (sort compare (preorder (mirror tree)))
+    >> printNatLn (log2 3)
+    >> printNatLn (log2 130);

examples/midsquare/MidSquareHash.juvix

@@ -1,35 +1,54 @@
 --- This file implements the mid-square hashing function in Juvix. See:
+
 --- https://research.cs.vt.edu/AVresearch/hashing/midsquare.php
----
+
 --- The implementation is for hashing natural numbers with maximum 16 bits into 6
+
 --- bits. In order to facilitate the translation to the current version of the
+
 --- GEB backend, no recursion is used (it is manually unrolled).
----
 module MidSquareHash;
 
 open import Stdlib.Prelude;
 open import Stdlib.Data.Nat.Ord;
 
 --- `powN` is 2 ^ N
 pow0 : Nat := 1;
+
 pow1 : Nat := 2 * pow0;
+
 pow2 : Nat := 2 * pow1;
+
 pow3 : Nat := 2 * pow2;
+
 pow4 : Nat := 2 * pow3;
+
 pow5 : Nat := 2 * pow4;
+
 pow6 : Nat := 2 * pow5;
+
 pow7 : Nat := 2 * pow6;
+
 pow8 : Nat := 2 * pow7;
+
 pow9 : Nat := 2 * pow8;
+
 pow10 : Nat := 2 * pow9;
+
 pow11 : Nat := 2 * pow10;
+
 pow12 : Nat := 2 * pow11;
+
 pow13 : Nat := 2 * pow12;
+
 pow14 : Nat := 2 * pow13;
+
 pow15 : Nat := 2 * pow14;
+
 pow16 : Nat := 2 * pow15;
 
 --- `hashN` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
+
 --- (i.e. smaller than 64) using the mid-square algorithm.
 hash0 : Nat -> Nat;
 hash0 x := 0;
@@ -44,48 +63,59 @@ hash3 : Nat -> Nat;
 hash3 x := x * x;
 
 hash4 : Nat -> Nat;
-hash4 x := if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+hash4 x :=
+  if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat;
-hash5 x := if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+hash5 x :=
+  if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat;
-hash6 x := if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+hash6 x :=
+  if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat;
-hash7 x := if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+hash7 x :=
+  if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat;
-hash8 x := if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+hash8 x :=
+  if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat;
-hash9 x := if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+hash9 x :=
+  if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat;
-hash10 x := if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+hash10 x :=
+  if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat;
-hash11 x := if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+hash11 x :=
+  if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat;
-hash12 x := if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+hash12 x :=
+  if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat;
-hash13 x := if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+hash13 x :=
+  if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat;
-hash14 x := if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+hash14 x :=
+  if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat;
-hash15 x := if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+hash15 x :=
+  if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat;
-hash16 x := if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash16 x :=
+  if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
 main : Nat;
 main := hash 1367;
 -- result: 3
-
-end;