From e6beb22d1b6c931594d551c803bb09001d0f6b2f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 10 Oct 2024 18:04:31 +0200 Subject: [PATCH] fix formatting --- examples/milestone/Hanoi/Hanoi.juvix | 4 +- tests/positive/265/M.juvix | 3 +- .../Internal/Positivity/RoseTree.juvix | 3 +- .../positive/Internal/Positivity2/main.juvix | 7 +- tests/positive/Isabelle/Program.juvix | 125 ++++++++++++------ tests/positive/MarkdownImport/B.juvix.md | 4 +- tests/positive/MarkdownImport/C.juvix.md | 8 -- tests/positive/Termination/Data/List.juvix | 9 +- tests/positive/issue1693/M.juvix | 9 +- tests/positive/issue1731/builtinFail.juvix | 5 +- tests/positive/issue3048/Other.juvix | 2 + tests/positive/issue3048/main.juvix | 10 +- 12 files changed, 99 insertions(+), 90 deletions(-) diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix index 54ea6bc9de..c641593b4d 100644 --- a/examples/milestone/Hanoi/Hanoi.juvix +++ b/examples/milestone/Hanoi/Hanoi.juvix @@ -44,8 +44,8 @@ type Move := to : Peg }; -showMove (move : Move) : String - := showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move); +showMove (move : Move) : String := + showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move); --- Produce a list of ;Move;s that solves the towers of Hanoi game hanoi : Nat -> Peg -> Peg -> Peg -> List Move diff --git a/tests/positive/265/M.juvix b/tests/positive/265/M.juvix index 5f1dbc1a45..590437d7b4 100644 --- a/tests/positive/265/M.juvix +++ b/tests/positive/265/M.juvix @@ -4,8 +4,7 @@ type Bool := | true : Bool | false : Bool; -type Pair (A : Type) (B : Type) := - mkPair : A → B → Pair A B; +type Pair (A : Type) (B : Type) := mkPair : A → B → Pair A B; f : _ → _ | (mkPair false true) := true diff --git a/tests/positive/Internal/Positivity/RoseTree.juvix b/tests/positive/Internal/Positivity/RoseTree.juvix index c8de6ff5ec..3b88717db1 100644 --- a/tests/positive/Internal/Positivity/RoseTree.juvix +++ b/tests/positive/Internal/Positivity/RoseTree.juvix @@ -4,5 +4,4 @@ type List (A : Type) : Type := | nil : List A | cons : A -> List A -> List A; -type RoseTree (A : Type) : Type := - node : A -> List (RoseTree A) -> RoseTree A; +type RoseTree (A : Type) : Type := node : A -> List (RoseTree A) -> RoseTree A; diff --git a/tests/positive/Internal/Positivity2/main.juvix b/tests/positive/Internal/Positivity2/main.juvix index d46d62baec..84f4f584f9 100644 --- a/tests/positive/Internal/Positivity2/main.juvix +++ b/tests/positive/Internal/Positivity2/main.juvix @@ -10,6 +10,7 @@ type Box (A : Type) := box A; module M1; type T1 (x y : Type) := mkT1 y (x -> x) x; + type T2 (x : (Type -> Type) -> Type) := mkT2 (x (T1 T)); end; @@ -18,7 +19,7 @@ module M2; type T2 (x : Type) := mkT2 (x -> T); - -- type T3 := mkT3 (T1 T3); +-- type T3 := mkT3 (T1 T3); end; module M3; @@ -40,11 +41,11 @@ module E3; end; module E5; - type Ghost1 (A : Type) := ghost1 (Ghost2 ((Ghost1 (A -> A)) -> Ghost2 A)); + type Ghost1 (A : Type) := ghost1 (Ghost2 (Ghost1 (A -> A) -> Ghost2 A)); type Ghost2 (B : Type) := ghost2 Ok (Ghost1 B); - type Ok := mkOk (Ghost1 (Ok -> Ok)); + type Ok := mkOk (Ghost1 (Ok -> Ok)); end; module E6; diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 7e7db6324b..24d5ca0457 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -12,7 +12,7 @@ id2 {A : Type} : A -> A := id; add_one : List Nat -> List Nat | [] := [] -- hello! - | (x :: xs) := (x + 1) :: add_one xs; + | (x :: xs) := x + 1 :: add_one xs; sum : List Nat -> Nat | [] := 0 @@ -37,14 +37,20 @@ dec : Nat -> Nat dec' (x : Nat) : Nat := -- Do case switch -- pattern match on x - case x of {- the zero case -} zero := {- return zero -} zero | {- the suc case -} suc y := y; + case x of + | {- the zero case -} + zero := + {- return zero -} + zero + | {- the suc case -} + suc y := y; optmap {A} (f : A -> A) : Maybe A -> Maybe A | nothing := nothing | (just x) := just (f x); pboth {A B A' B'} (f : A -> A') (g : B -> B') : Pair A B -> Pair A' B' - | (x, y) := (f x, g y); + | (x, y) := f x, g y; bool_fun (x y z : Bool) : Bool := x && y || z; @@ -62,26 +68,26 @@ qsnd : {A : Type} → Queue A → List A | (queue _ v) := v; pop_front {A} (q : Queue A) : Queue A := - let - q' : Queue A := queue (tail (qfst q)) (qsnd q); - in case qfst q' of - | nil := queue (reverse (qsnd q')) nil - | _ := q'; + let + q' : Queue A := queue (tail (qfst q)) (qsnd q); + in case qfst q' of + | nil := queue (reverse (qsnd q')) nil + | _ := q'; push_back {A} (q : Queue A) (x : A) : Queue A := - case qfst q of - | nil := queue (x :: nil) (qsnd q) - | q' := queue q' (x :: qsnd q); + case qfst q of + | nil := queue (x :: nil) (qsnd q) + | q' := queue q' (x :: qsnd q); --- Checks if the queue is empty is_empty {A} (q : Queue A) : Bool := - case qfst q of - | nil := - case qsnd q of { - | nil := true - | _ := false - } - | _ := false; + case qfst q of + | nil := + case qsnd q of { + | nil := true + | _ := false + } + | _ := false; empty : {A : Type} → Queue A := queue nil nil; @@ -96,52 +102,85 @@ funkcja (n : Nat) : Nat := --- An Either' type type Either' A B := - --- Left constructor - Left' A -| --- Right constructor - Right' B; + | --- Left constructor + Left' A + | --- Right constructor + Right' B; -- Records {-# isabelle-ignore: true #-} -type R' := mkR' { - r1' : Nat; - r2' : Nat; -}; - -type R := mkR { - r1 : Nat; - r2 : Nat; -}; +type R' := + mkR' { + r1' : Nat; + r2' : Nat + }; + +type R := + mkR { + r1 : Nat; + r2 : Nat + }; r : R := mkR 0 1; + v : Nat := 0; -funR (r : R) : R := - case r of - | mkR@{r1; r2} := r@R{r1 := r1 + r2}; +funR (r : R) : R := case r of mkR@{r1; r2} := r@R{r1 := r1 + r2}; funRR : R -> R | r@mkR@{r1; r2} := r@R{r1 := r1 + r2}; funR' : R -> R - | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2}; + | mkR@{r1 := rr1; r2 := rr2} := + mkR@{ + r1 := rr1 + rr2; + r2 := rr2 + }; funR1 : R -> R - | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} - | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}; + | mkR@{r1 := zero; r2} := + mkR@{ + r1 := r2; + r2 + } + | mkR@{r1 := rr1; r2 := rr2} := + mkR@{ + r1 := rr2; + r2 := rr1 + }; funR2 (r : R) : R := case r of - | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} - | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}; + | mkR@{r1 := zero; r2} := + mkR@{ + r1 := r2; + r2 + } + | mkR@{r1 := rr1; r2 := rr2} := + mkR@{ + r1 := rr2; + r2 := rr1 + }; funR3 (er : Either' R R) : R := case er of - | Left' mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} - | Left' mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1} - | Right' mkR@{r1; r2 := zero} := mkR@{r1 := 7; r2 := r1} - | Right' r@(mkR@{r1; r2}) := r@R{r1 := r2 + 2; r2 := r1 + 3}; + | Left' mkR@{r1 := zero; r2} := + mkR@{ + r1 := r2; + r2 + } + | Left' mkR@{r1 := rr1; r2 := rr2} := + mkR@{ + r1 := rr2; + r2 := rr1 + } + | Right' mkR@{r1; r2 := zero} := + mkR@{ + r1 := 7; + r2 := r1 + } + | Right' r@mkR@{r1; r2} := r@R{ r1 := r2 + 2; r2 := r1 + 3 }; funR4 : R -> R | r@mkR@{r1} := r@R{r2 := r1}; diff --git a/tests/positive/MarkdownImport/B.juvix.md b/tests/positive/MarkdownImport/B.juvix.md index 6d596fc858..2c40326ba1 100644 --- a/tests/positive/MarkdownImport/B.juvix.md +++ b/tests/positive/MarkdownImport/B.juvix.md @@ -1,5 +1,3 @@ -```juvix module B; -axiom D : Type; -``` \ No newline at end of file +axiom D : Type; diff --git a/tests/positive/MarkdownImport/C.juvix.md b/tests/positive/MarkdownImport/C.juvix.md index 2d8d4f0b09..44e6f3bd07 100644 --- a/tests/positive/MarkdownImport/C.juvix.md +++ b/tests/positive/MarkdownImport/C.juvix.md @@ -1,15 +1,7 @@ -# This is a Juvix code block - -```juvix module C; import B open; axiom aa : D; -``` - -Text in between code blocks -```juvix axiom b : D; -``` \ No newline at end of file diff --git a/tests/positive/Termination/Data/List.juvix b/tests/positive/Termination/Data/List.juvix index 2d9e8f1a66..2bde073fe8 100644 --- a/tests/positive/Termination/Data/List.juvix +++ b/tests/positive/Termination/Data/List.juvix @@ -11,13 +11,11 @@ type List (A : Type) := | cons : A → List A → List A; -- Do not remove implicit arguments. Useful for testing. -foldr - : {A : Type} → {B : Type} → (A → B → B) → B → List A → B +foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B | _ z nil := z | f z (cons h hs) := f h (foldr {_} f z hs); -foldl - : {A : Type} → {B : Type} → (B → A → B) → B → List A → B +foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B | f z nil := z | {_} {_} f z (cons h hs) := foldl {_} f (f z h) hs; @@ -27,8 +25,7 @@ map : {A : Type} → {B : Type} → (A → B) → List A → List B filter : {A : Type} → (A → Bool) → List A → List A | f nil := nil - | f (cons h hs) := - ite (f h) (cons h (filter {_} f hs)) (filter f hs); + | f (cons h hs) := ite (f h) (cons h (filter {_} f hs)) (filter f hs); length : {A : Type} → List A → ℕ | nil := zero diff --git a/tests/positive/issue1693/M.juvix b/tests/positive/issue1693/M.juvix index 68bb4ffd77..10b95c16c1 100644 --- a/tests/positive/issue1693/M.juvix +++ b/tests/positive/issue1693/M.juvix @@ -2,14 +2,7 @@ module M; import Stdlib.Prelude open; -S - : {A : Type} - → {B : Type} - → {C : Type} - → (A → B → C) - → (A → B) - → A - → C +S : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → (A → B) → A → C | x y z := x z (y z); K : {A : Type} → {B : Type} → A → B → A diff --git a/tests/positive/issue1731/builtinFail.juvix b/tests/positive/issue1731/builtinFail.juvix index a665df7900..4ea27d9e1f 100644 --- a/tests/positive/issue1731/builtinFail.juvix +++ b/tests/positive/issue1731/builtinFail.juvix @@ -6,7 +6,4 @@ import Stdlib.System.IO open; builtin fail axiom fail : {A : Type} → String → A; -main : IO := - printStringLn "Get" - >>> fail "Enough" - >>> printStringLn "Sleep"; +main : IO := printStringLn "Get" >>> fail "Enough" >>> printStringLn "Sleep"; diff --git a/tests/positive/issue3048/Other.juvix b/tests/positive/issue3048/Other.juvix index e947739e98..d4d31a8fb5 100644 --- a/tests/positive/issue3048/Other.juvix +++ b/tests/positive/issue3048/Other.juvix @@ -1,5 +1,7 @@ module Other; type T1 := mkT1; + type T2 := mkT2; + type T3 := mkT3; diff --git a/tests/positive/issue3048/main.juvix b/tests/positive/issue3048/main.juvix index 5e06bf76b6..12fe495c39 100644 --- a/tests/positive/issue3048/main.juvix +++ b/tests/positive/issue3048/main.juvix @@ -3,14 +3,6 @@ module main; import Other; type Tree (A : Type) := - node (Tree A) - (Tree A) - (Tree A) - (Tree A) - (Tree A) - (Tree A) - (Tree A) - (Tree A) - (Tree A); + node (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A); type Foo := mkFoo (Tree Foo);