Use Juvix formatter

Makefile

@@ -12,3 +12,16 @@ html:
 PHONY: clean
 clean:
 	rm -rf docs
+
+TOFORMATJUVIXFILES = ./Stdlib
+TOFORMAT = $(shell find ${TOFORMATJUVIXFILES} -name "*.juvix" -print)
+
+.PHONY: $(TOFORMAT)
+juvix-format: $(TOFORMAT)
+$(TOFORMAT): %:
+	@echo "Formatting $@"
+	@juvix dev scope $@ --with-comments > $@.tmp
+	@echo "" >> $@.tmp
+	@mv $@.tmp $@
+	@echo "Typechecking formatted $@"
+	@juvix typecheck $@ --only-errors

Stdlib/Data/Bool.juvix

@@ -1,14 +1,18 @@
 module Stdlib.Data.Bool;
+  builtin bool type Bool :=
+    | true : Bool
+    | false : Bool;
 
-builtin bool
-type Bool :=
-  true : Bool |
-  false : Bool;
+  not : Bool → Bool;
+  not true := false;
+  not false := true;
 
-not : Bool → Bool;
-not true := false;
-not false := true;
+  infixr 2 ||;
+  || : Bool → Bool → Bool;
+  || false a := a;
+  || true _ := true;
 
+<<<<<<< HEAD
 infixr 2 ||;
 builtin bool-or
 || : Bool → Bool → Bool;
@@ -32,4 +36,14 @@ or a b := a || b;
 and : Bool → Bool → Bool;
 and a b := a && b;
 
+=======
+  infixr 2 &&;
+  && : Bool → Bool → Bool;
+  && false _ := false;
+  && true a := a;
+
+  builtin bool-if if : {A : Type} → Bool → A → A → A;
+  if true a _ := a;
+  if false _ b := b;
+>>>>>>> 4b965cb (Use Juvix formatter)
 end;

Stdlib/Data/List.juvix

@@ -1,103 +1,115 @@
 module Stdlib.Data.List;
-
-open import Stdlib.Data.Bool;
-open import Stdlib.Function;
-open import Stdlib.Data.Nat;
-open import Stdlib.Data.Ord;
-open import Stdlib.Data.Product;
-
-infixr 5 ::;
-type List (a : Type) :=
-    nil : List a
-  | :: : a → List a → List a;
-
-elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
-elem _ _ nil := false;
-elem eq s (x :: xs) := eq s x || elem eq s xs;
-
-foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
-foldr _ z nil := z;
-foldr f z (h :: hs) := f h (foldr f z hs);
-
-foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl f z nil := z ;
-foldl f z (h :: hs) := foldl f (f z h) hs;
-
-map : {A : Type} → {B : Type} → (A → B) → List A → List B;
-map f nil := nil;
-map f (h :: hs) := f h :: map f hs;
-
-filter : {A : Type} → (A → Bool) → List A → List A;
-filter _ nil := nil;
-filter f (h :: hs) := if (f h)
-   (h :: filter f hs)
-   (filter f hs);
-
-length : {A : Type} → List A → Nat;
-length nil := zero;
-length (_ :: l) := suc (length l);
-
-reverse : {A : Type} → List A → List A;
-reverse := foldl (flip (::)) nil;
-
-replicate : {A : Type} → Nat → A → List A;
-replicate zero _ := nil;
-replicate (suc n) x :=  x :: replicate n x;
-
-take : {A : Type} → Nat → List A → List A;
-take (suc n) (x :: xs) := x :: take n xs;
-take _ _ := nil;
-
-splitAt : {A : Type} → Nat → List A → List A × List A;
-splitAt _ nil := nil , nil ;
-splitAt zero xs :=  nil , xs;
-splitAt (suc zero) (x :: xs) := x :: nil , xs;
-splitAt (suc (suc m)) (x :: xs) := first ((::) x) (splitAt m xs);
-
-merge : {A : Type} → (A → A → Ordering) → List A → List A → List A;
-merge cmp (x :: xs) (y :: ys) :=
-   if (isLT (cmp x y))
+  open import Stdlib.Data.Bool;
+  open import Stdlib.Function;
+  open import Stdlib.Data.Nat;
+  open import Stdlib.Data.Ord;
+  open import Stdlib.Data.Product;
+
+  infixr 5 ::;
+  type List (a : Type) :=
+    | nil : List a
+    | :: : a → List a → List a;
+
+  elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
+  elem _ _ nil := false;
+  elem eq s (x :: xs) := eq s x || elem eq s xs;
+
+  foldr : {A : Type} → {B : Type} → (A → B → B) → B → List
+    A → B;
+  foldr _ z nil := z;
+  foldr f z (h :: hs) := f h (foldr f z hs);
+
+  foldl : {A : Type} → {B : Type} → (B → A → B) → B → List
+    A → B;
+  foldl f z nil := z;
+  foldl f z (h :: hs) := foldl f (f z h) hs;
+
+  map : {A : Type} → {B : Type} → (A → B) → List A → List B;
+  map f nil := nil;
+  map f (h :: hs) := f h :: map f hs;
+
+  filter : {A : Type} → (A → Bool) → List A → List A;
+  filter _ nil := nil;
+  filter f (h :: hs) := if
+    (f h)
+    (h :: filter f hs)
+    (filter f hs);
+
+  length : {A : Type} → List A → Nat;
+  length nil := zero;
+  length (_ :: l) := suc (length l);
+
+  reverse : {A : Type} → List A → List A;
+  reverse := foldl (flip (::)) nil;
+
+  replicate : {A : Type} → Nat → A → List A;
+  replicate zero _ := nil;
+  replicate (suc n) x := x :: replicate n x;
+
+  take : {A : Type} → Nat → List A → List A;
+  take (suc n) (x :: xs) := x :: take n xs;
+  take _ _ := nil;
+
+  splitAt : {A : Type} → Nat → List A → List A × List A;
+  splitAt _ nil := nil , nil;
+  splitAt zero xs := nil , xs;
+  splitAt (suc zero) (x :: xs) := x :: nil , xs;
+  splitAt (suc (suc m)) (x :: xs) := first
+    ((::) x)
+    (splitAt m xs);
+
+  merge : {A : Type} → (A → A → Ordering) → List A → List
+    A → List A;
+  merge cmp (x :: xs) (y :: ys) := if
+    (isLT (cmp x y))
     (x :: merge cmp xs (y :: ys))
     (y :: merge cmp (x :: xs) ys);
-merge _ nil ys := ys;
-merge _ xs nil := xs;
-
-partition : {A : Type} → (A → Bool) → List A → List A × List A;
-partition _ nil := nil , nil ;
-partition f (x :: xs) := (if (f x) first second) ((::) x) (partition f xs);
-
-infixr 5 ++;
-++ : {A : Type} → List A → List A → List A;
-++ nil ys := ys;
-++ (x :: xs) ys := x :: (xs ++ ys);
-
-flatten : {A : Type} → List (List A) → List A;
-flatten := foldl (++) nil;
-
-prependToAll : {A : Type} → A → List A → List A;
-prependToAll _ nil := nil;
-prependToAll sep (x :: xs) := sep :: x :: prependToAll sep xs;
-
-intersperse : {A : Type} → A → List A → List A;
-intersperse _ nil := nil;
-intersperse sep (x :: xs) := x :: prependToAll sep xs;
-
-head : {A : Type} → List A → A;
-head (x :: _) := x;
-
-tail : {A : Type} → List A → List A;
-tail (_ :: xs) := xs;
-
-terminating
-transpose : {A : Type} → List (List A) → List (List A);
-transpose (nil :: _) := nil;
-transpose xss := (map head xss) :: (transpose (map tail xss));
-
-any : {A : Type} → (A → Bool) → List A → Bool;
-any f xs := foldl (||) false (map f xs);
-
-null : {A : Type} → List A → Bool;
-null nil := true;
-null _ := false;
-
+  merge _ nil ys := ys;
+  merge _ xs nil := xs;
+
+  partition : {A : Type} → (A → Bool) → List A → List A
+    × List A;
+  partition _ nil := nil , nil;
+  partition f (x :: xs) := if
+    (f x)
+    first
+    second
+    ((::) x)
+    (partition f xs);
+
+  infixr 5 ++;
+  ++ : {A : Type} → List A → List A → List A;
+  ++ nil ys := ys;
+  ++ (x :: xs) ys := x :: xs ++ ys;
+
+  flatten : {A : Type} → List (List A) → List A;
+  flatten := foldl (++) nil;
+
+  prependToAll : {A : Type} → A → List A → List A;
+  prependToAll _ nil := nil;
+  prependToAll sep (x :: xs) := sep
+    :: x
+    :: prependToAll sep xs;
+
+  intersperse : {A : Type} → A → List A → List A;
+  intersperse _ nil := nil;
+  intersperse sep (x :: xs) := x :: prependToAll sep xs;
+
+  head : {A : Type} → List A → A;
+  head (x :: _) := x;
+
+  tail : {A : Type} → List A → List A;
+  tail (_ :: xs) := xs;
+
+  terminating
+  transpose : {A : Type} → List (List A) → List (List A);
+  transpose (nil :: _) := nil;
+  transpose xss := map head xss :: transpose (map tail xss);
+
+  any : {A : Type} → (A → Bool) → List A → Bool;
+  any f xs := foldl (||) false (map f xs);
+
+  null : {A : Type} → List A → Bool;
+  null nil := true;
+  null _ := false;
 end;

Stdlib/Data/List/Ord.juvix

@@ -1,15 +1,15 @@
 module Stdlib.Data.List.Ord;
+  open import Stdlib.Data.Ord;
+  open import Stdlib.Data.List;
 
-open import Stdlib.Data.Ord;
-open import Stdlib.Data.List;
-
-compare : {A : Type} → (A → A → Ordering) → List A → List A → Ordering;
-compare _ nil nil := EQ;
-compare _ nil (_ :: _) := LT;
-compare _ (_ :: _) nil := GT;
-compare cmp (x :: xs) (y :: ys) := ifOrd (cmp x y)
-  LT
-  (compare cmp xs ys)
-  GT;
-
+  compare : {A : Type} → (A → A → Ordering) → List A → List
+    A → Ordering;
+  compare _ nil nil := EQ;
+  compare _ nil (_ :: _) := LT;
+  compare _ (_ :: _) nil := GT;
+  compare cmp (x :: xs) (y :: ys) := ifOrd
+    (cmp x y)
+    LT
+    (compare cmp xs ys)
+    GT;
 end;

Stdlib/Data/Maybe.juvix

@@ -1,16 +1,13 @@
 module Stdlib.Data.Maybe;
+  type Maybe (A : Type) :=
+    | nothing : Maybe A
+    | just : A → Maybe A;
 
-type Maybe (A : Type) :=
-    nothing : Maybe A
-  | just : A → Maybe A;
-
-
-fromMaybe : {A : Type} → A → Maybe A → A;
-fromMaybe a nothing := a;
-fromMaybe _ (just a) := a;
-
-maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
-maybe b _ nothing := b;
-maybe _ f (just a) := f a;
+  fromMaybe : {A : Type} → A → Maybe A → A;
+  fromMaybe a nothing := a;
+  fromMaybe _ (just a) := a;
 
+  maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
+  maybe b _ nothing := b;
+  maybe _ f (just a) := f a;
 end;