diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix index 9c9c542e8..0a0dcff0f 100644 --- a/examples/demo/Demo.juvix +++ b/examples/demo/Demo.juvix @@ -24,8 +24,7 @@ mirror : {A : Type} → Tree A → Tree A | t@(leaf _) := t | (node x l r) := node x (mirror r) (mirror l); -tree : Tree Nat := - node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7); +tree : Tree Nat := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7); preorder : {A : Type} → Tree A → List A | (leaf x) := x :: nil @@ -35,15 +34,11 @@ terminating sort {A} {{Ord A}} : List A → List A | nil := nil | xs@(_ :: nil) := xs - | xs := - uncurry - merge - (both sort (splitAt (div (length xs) 2) xs)); + | xs := uncurry merge (both sort (splitAt (div (length xs) 2) xs)); printNatListLn : List Nat → IO | nil := printStringLn "nil" - | (x :: xs) := - printNat x >>> printString " :: " >>> printNatListLn xs; + | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs; main : IO := printStringLn "Hello!" diff --git a/examples/midsquare/MidSquareHash.juvix b/examples/midsquare/MidSquareHash.juvix index 731b548b9..1a50f54f2 100644 --- a/examples/midsquare/MidSquareHash.juvix +++ b/examples/midsquare/MidSquareHash.juvix @@ -14,11 +14,7 @@ pow : Nat -> Nat --- `hash' N` 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. hash' : Nat -> Nat -> Nat - | (suc n@(suc (suc m))) x := - ite - (x < pow n) - (hash' n x) - (mod (div (x * x) (pow m)) (pow 6)) + | (suc n@(suc (suc m))) x := ite (x < pow n) (hash' n x) (mod (div (x * x) (pow m)) (pow 6)) | _ x := x * x; hash : Nat -> Nat := hash' 16; diff --git a/examples/midsquare/MidSquareHashUnrolled.juvix b/examples/midsquare/MidSquareHashUnrolled.juvix index 80468695d..0f7927ac0 100644 --- a/examples/midsquare/MidSquareHashUnrolled.juvix +++ b/examples/midsquare/MidSquareHashUnrolled.juvix @@ -57,56 +57,43 @@ hash3 : Nat -> Nat | x := x * x; hash4 : Nat -> Nat - | x := - ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); + | x := ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6); hash5 : Nat -> Nat - | x := - ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); + | x := ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6); hash6 : Nat -> Nat - | x := - ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); + | x := ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6); hash7 : Nat -> Nat - | x := - ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); + | x := ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6); hash8 : Nat -> Nat - | x := - ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); + | x := ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6); hash9 : Nat -> Nat - | x := - ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); + | x := ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6); hash10 : Nat -> Nat - | x := - ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); + | x := ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6); hash11 : Nat -> Nat - | x := - ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); + | x := ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6); hash12 : Nat -> Nat - | x := - ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); + | x := ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6); hash13 : Nat -> Nat - | x := - ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); + | x := ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6); hash14 : Nat -> Nat - | x := - ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); + | x := ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6); hash15 : Nat -> Nat - | x := - ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); + | x := ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6); hash16 : Nat -> Nat - | x := - ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); + | x := ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6); hash : Nat -> Nat := hash16; diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix index 01550e94c..d7d088dfa 100644 --- a/examples/milestone/Bank/Bank.juvix +++ b/examples/milestone/Bank/Bank.juvix @@ -39,22 +39,14 @@ module Balances; --- Increments the amount associated with a certain ;Field;. increment : Field -> Nat -> Balances -> Balances | f n nil := (f, n) :: nil - | f n ((b, bn) :: bs) := - ite - (f == b) - ((b, bn + n) :: bs) - ((b, bn) :: increment f n bs); + | f n ((b, bn) :: bs) := ite (f == b) ((b, bn + n) :: bs) ((b, bn) :: increment f n bs); --- Decrements the amount associated with a certain ;Field;. --- If the ;Field; is not found, it does nothing. --- Subtraction is truncated to ;zero;. decrement : Field -> Nat -> Balances -> Balances | _ _ nil := nil - | f n ((b, bn) :: bs) := - ite - (f == b) - ((b, sub bn n) :: bs) - ((b, bn) :: decrement f n bs); + | f n ((b, bn) :: bs) := ite (f == b) ((b, sub bn n) :: bs) ((b, bn) :: decrement f n bs); emtpyBalances : Balances := nil; @@ -90,16 +82,13 @@ assert : {A : Type} -> Bool -> A -> A --- --- `caller`: Who is creating the transaction. It must be the bank. issue : Address -> Address -> Nat -> Token - | caller owner amount := - assert (caller == bankAddress) (mkToken owner 0 amount); + | caller owner amount := assert (caller == bankAddress) (mkToken owner 0 amount); --- Deposits some amount of money into the bank. -deposit - (bal : Balances) (token : Token) (amount : Nat) : Token := +deposit (bal : Balances) (token : Token) (amount : Nat) : Token := let difference : Nat := sub (getAmount token) amount; - remaining : Token := - mkToken (getOwner token) (getGates token) difference; + remaining : Token := mkToken (getOwner token) (getGates token) difference; hash : Field := hashAddress (getOwner token); bal' : Balances := increment hash amount bal; in runOnChain (commitBalances bal') remaining; diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix index 71663a9d2..eed4d4ba1 100644 --- a/examples/milestone/Collatz/Collatz.juvix +++ b/examples/milestone/Collatz/Collatz.juvix @@ -2,8 +2,7 @@ module Collatz; import Stdlib.Prelude open; -collatzNext (n : Nat) : Nat := - ite (mod n 2 == 0) (div n 2) (3 * n + 1); +collatzNext (n : Nat) : Nat := ite (mod n 2 == 0) (div n 2) (3 * n + 1); collatz : Nat → Nat | zero := zero @@ -15,14 +14,10 @@ run (f : Nat → Nat) : Nat → IO | (suc zero) := printNatLn 1 >>> printStringLn "Finished!" | n := printNatLn n >>> run f (f n); -welcome : String := - "Collatz calculator\n------------------\n\nType a number then ENTER"; +welcome : String := "Collatz calculator\n------------------\n\nType a number then ENTER"; resultHeading : String := "Collatz sequence:"; main : IO := printStringLn welcome - >>> readLn - λ {s := - printStringLn resultHeading - >>> run collatz (stringToNat s)}; + >>> readLn λ {s := printStringLn resultHeading >>> run collatz (stringToNat s)}; diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix index 631e41bb7..3b5ebbd78 100644 --- a/examples/milestone/Fibonacci/Fibonacci.juvix +++ b/examples/milestone/Fibonacci/Fibonacci.juvix @@ -8,5 +8,4 @@ fib : Nat → Nat → Nat → Nat fibonacci (n : Nat) : Nat := fib n 0 1; -main : IO := - readLn (stringToNat >> fibonacci >> printNatLn); +main : IO := readLn (stringToNat >> fibonacci >> printNatLn); diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix index e61f8c50e..355c64f1e 100644 --- a/examples/milestone/Hanoi/Hanoi.juvix +++ b/examples/milestone/Hanoi/Hanoi.juvix @@ -15,9 +15,7 @@ module Hanoi; import Stdlib.Prelude open; --- Concatenates a list of strings ---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" - :: "b" - :: nil; +--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil; concat : List String → String := foldl (++str) ""; intercalate : String → List String → String @@ -29,8 +27,7 @@ singleton : {A : Type} → A → List A --- Produce a ;String; representation of a ;List Nat; showList : List Nat → String - | xs := - "[" ++str intercalate "," (map natToString xs) ++str "]"; + | xs := "[" ++str intercalate "," (map natToString xs) ++str "]"; --- A Peg represents a peg in the towers of Hanoi game type Peg := @@ -47,17 +44,11 @@ showPeg : Peg → String type Move := move : Peg → Peg → Move; showMove : Move → String - | (move from to) := - showPeg from ++str " -> " ++str showPeg to; + | (move from to) := showPeg from ++str " -> " ++str showPeg to; --- Produce a list of ;Move;s that solves the towers of Hanoi game hanoi : Nat → Peg → Peg → Peg → List Move | zero _ _ _ := nil - | (suc n) p1 p2 p3 := - hanoi n p1 p3 p2 - ++ singleton (move p1 p2) - ++ hanoi n p3 p2 p1; + | (suc n) p1 p2 p3 := hanoi n p1 p3 p2 ++ singleton (move p1 p2) ++ hanoi n p3 p2 p1; -main : IO := - printStringLn - (unlines (map showMove (hanoi 5 left middle right))); +main : IO := printStringLn (unlines (map showMove (hanoi 5 left middle right))); diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix index c6f7c9daa..a940b4df6 100644 --- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix +++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix @@ -15,27 +15,18 @@ scanIterate {A} : Nat → (A → A) → A → List A singleton {A} (a : A) : List A := a :: nil; --- Concatenates a list of strings ---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" - :: "b" - :: nil; +--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil; concat : List String → String := foldl (++str) ""; -intercalate (sep : String) (xs : List String) : String := - concat (intersperse sep xs); +intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs); -showList (xs : List Nat) : String := - "[" ++str intercalate "," (map natToString xs) ++str "]"; +showList (xs : List Nat) : String := "[" ++str intercalate "," (map natToString xs) ++str "]"; --- Compute the next row of Pascal's triangle pascalNextRow (row : List Nat) : List Nat := - zipWith - (+) - (singleton zero ++ row) - (row ++ singleton zero); + zipWith (+) (singleton zero ++ row) (row ++ singleton zero); --- Produce Pascal's triangle to a given depth -pascal (rows : Nat) : List (List Nat) := - scanIterate rows pascalNextRow (singleton 1); +pascal (rows : Nat) : List (List Nat) := scanIterate rows pascalNextRow (singleton 1); -main : IO := - printStringLn (unlines (map showList (pascal 10))); +main : IO := printStringLn (unlines (map showList (pascal 10))); diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix index 0cea3e91f..ca208bb7d 100644 --- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix @@ -10,33 +10,22 @@ import Logic.Game open; --- A ;String; that prompts the user for their input prompt (x : GameState) : String := - "\n" - ++str showGameState x - ++str "\nPlayer " - ++str showSymbol (player x) - ++str ": "; + "\n" ++str showGameState x ++str "\nPlayer " ++str showSymbol (player x) ++str ": "; -nextMove (s : GameState) : String → GameState := - stringToNat >> validMove >> flip playMove s; +nextMove (s : GameState) : String → GameState := stringToNat >> validMove >> flip playMove s; --- Main loop terminating run : GameState → IO | (state b p (terminate msg)) := - printStringLn - ("\n" - ++str showGameState (state b p noError) - ++str "\n" - ++str msg) + printStringLn ("\n" ++str showGameState (state b p noError) ++str "\n" ++str msg) | (state b p (continue msg)) := printString (msg ++str prompt (state b p noError)) >>> readLn (run << nextMove (state b p noError)) - | x := - printString (prompt x) >>> readLn (run << nextMove x); + | x := printString (prompt x) >>> readLn (run << nextMove x); --- The welcome message -welcome : String := - "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move"; +welcome : String := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move"; --- The entry point of the program main : IO := printStringLn welcome >>> run beginState; diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix index 21b22c854..5f269f483 100644 --- a/examples/milestone/TicTacToe/Logic/Board.juvix +++ b/examples/milestone/TicTacToe/Logic/Board.juvix @@ -21,22 +21,16 @@ full : List Square → Bool | _ := failwith "full"; diagonals : List (List Square) → List (List Square) - | ((a1 :: _ :: b1 :: nil) - :: (_ :: c :: _ :: nil) - :: (b2 :: _ :: a2 :: nil) - :: nil) := + | ((a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil) := (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil | _ := failwith "diagonals"; -columns : List (List Square) → List (List Square) := - transpose; +columns : List (List Square) → List (List Square) := transpose; rows : List (List Square) → List (List Square) := id; --- Textual representation of a ;List Square; -showRow (xs : List Square) : String := - concat (surround "|" (map showSquare xs)); +showRow (xs : List Square) : String := concat (surround "|" (map showSquare xs)); showBoard : Board → String - | (board squares) := - unlines (surround "+---+---+---+" (map showRow squares)); + | (board squares) := unlines (surround "+---+---+---+" (map showRow squares)); diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix index 7d42d7ca2..daa07ccd3 100644 --- a/examples/milestone/TicTacToe/Logic/Extra.juvix +++ b/examples/milestone/TicTacToe/Logic/Extra.juvix @@ -4,15 +4,11 @@ module Logic.Extra; import Stdlib.Prelude open; --- Concatenates a list of strings ---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" - :: "b" - :: nil; +--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil; concat : List String → String := foldl (++str) ""; --- It inserts the first ;String; at the beginning, in between, and at the end of the second list -surround (x : String) (xs : List String) : List String := - (x :: intersperse x xs) ++ x :: nil; +surround (x : String) (xs : List String) : List String := (x :: intersperse x xs) ++ x :: nil; --- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result -intercalate (sep : String) (xs : List String) : String := - concat (intersperse sep xs); +intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs); diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix index 37a454f7e..3e7c8d42c 100644 --- a/examples/milestone/TicTacToe/Logic/Game.juvix +++ b/examples/milestone/TicTacToe/Logic/Game.juvix @@ -14,33 +14,17 @@ checkState : GameState → GameState | (state b p e) := ite (won (state b p e)) - (state - b - p - (terminate - ("Player " ++str showSymbol (switch p) ++str " wins!"))) - (ite - (draw (state b p e)) - (state b p (terminate "It's a draw!")) - (state b p e)); + (state b p (terminate ("Player " ++str showSymbol (switch p) ++str " wins!"))) + (ite (draw (state b p e)) (state b p (terminate "It's a draw!")) (state b p e)); --- Given a player attempted move, updates the state accordingly. playMove : Maybe Nat → GameState → GameState - | nothing (state b p _) := - state b p (continue "\nInvalid number, try again\n") + | nothing (state b p _) := state b p (continue "\nInvalid number, try again\n") | (just k) (state (board s) player e) := ite (not (elem (==) k (possibleMoves (flatten s)))) - (state - (board s) - player - (continue "\nThe square is already occupied, try again\n")) - (checkState - (state - (board (map (map (replace player k)) s)) - (switch player) - noError)); + (state (board s) player (continue "\nThe square is already occupied, try again\n")) + (checkState (state (board (map (map (replace player k)) s)) (switch player) noError)); --- Returns ;just; if the given ;Nat; is in range of 1..9 -validMove (n : Nat) : Maybe Nat := - ite (n <= 9 && n >= 1) (just n) nothing; +validMove (n : Nat) : Maybe Nat := ite (n <= 9 && n >= 1) (just n) nothing; diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix index c24ef1985..4009c8ebb 100644 --- a/examples/milestone/TicTacToe/Logic/GameState.juvix +++ b/examples/milestone/TicTacToe/Logic/GameState.juvix @@ -12,8 +12,7 @@ type Error := | --- a fatal occurred terminate : String → Error; -type GameState := - state : Board → Symbol → Error → GameState; +type GameState := state : Board → Symbol → Error → GameState; --- Textual representation of a ;GameState; showGameState : GameState → String @@ -29,21 +28,14 @@ beginState : GameState := (board (map (map empty) - ((1 :: 2 :: 3 :: nil) - :: (4 :: 5 :: 6 :: nil) - :: (7 :: 8 :: 9 :: nil) - :: nil))) + ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil))) X noError; --- ;true; if some player has won the game won : GameState → Bool - | (state (board squares) _ _) := - any - full - (diagonals squares ++ rows squares ++ columns squares); + | (state (board squares) _ _) := any full (diagonals squares ++ rows squares ++ columns squares); --- ;true; if there is a draw draw : GameState → Bool - | (state (board squares) _ _) := - null (possibleMoves (flatten squares)); + | (state (board squares) _ _) := null (possibleMoves (flatten squares)); diff --git a/src/Juvix/Prelude/Pretty.hs b/src/Juvix/Prelude/Pretty.hs index eccc18681..29e98871b 100644 --- a/src/Juvix/Prelude/Pretty.hs +++ b/src/Juvix/Prelude/Pretty.hs @@ -19,12 +19,12 @@ import Prettyprinter.Render.Text qualified as Text import Prettyprinter.Util (reflow) import Prelude --- | The page width is 150 with the desired length (not counting indent spaces) --- being 150*0.4 = 60 +-- | The page width is 100 with the desired length (not counting indent spaces) +-- being 100*1.0 = 100 defaultLayoutOptions :: LayoutOptions defaultLayoutOptions = LayoutOptions - { layoutPageWidth = AvailablePerLine 150 0.4 + { layoutPageWidth = AvailablePerLine 100 1.0 } class HasAnsiBackend a where diff --git a/tests/positive/Ape.juvix b/tests/positive/Ape.juvix index 2a1b592c2..a182adf29 100644 --- a/tests/positive/Ape.juvix +++ b/tests/positive/Ape.juvix @@ -28,8 +28,7 @@ axiom f : String → String; x : String := "" + ("" ++ ""); -axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String - → String; +axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String → String; nesting : String := wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index abe8bfd1e..57567ec4c 100644 --- a/tests/positive/Format.juvix +++ b/tests/positive/Format.juvix @@ -16,11 +16,7 @@ Bool; true; false; mkShow; module Show}; terminating -- Comment between terminating and type sig go : Nat → Nat → Nat - | n s := - ite - (s < n) - (go (sub n 1) s) - (go n (sub s n) + go (sub n 1) s); + | n s := ite (s < n) (go (sub n 1) s) (go n (sub s n) + go (sub n 1) s); module {- local module -} M; @@ -77,6 +73,13 @@ t3 : String := , "i" , "j" , "k" + , "1234" + , "1234" + , "1234" + , "1234" + , "1234" + , "1234" + , "1234" , "1234"; -- escaping in String literals @@ -121,14 +124,9 @@ t : String := +l1 "Hellooooooooo" +l1 "Hellooooooooo" +l6 "Hellooooooooo" - +l6 ("Hellooooooooo" - +r6 "Hellooooooooo" - +r6 "Hellooooooooo") + +l6 ("Hellooooooooo" +r6 "Hellooooooooo" +r6 "Hellooooooooo") +l6 "Hellooooooooo" - +l6 "Hellooooooooo" - +l7 "Hellooooooooo" - +l7 "Hellooooooooo" - +l7 "Hellooooooooo" + +l6 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo" , "hi" , "hi"; @@ -146,8 +144,11 @@ exampleFunction1 -> List A -> List A -> List A + -> List A + -> List A + -> List A -> Nat - | _ _ _ _ _ _ _ := 1; + | _ _ _ _ _ _ _ _ _ _ := 1; axiom undefined : {A : Type} -> A; @@ -162,8 +163,11 @@ exampleFunction2 -> List A -> List A -> List A + -> List A + -> List A + -> List A -> Nat := - λ {_ _ _ _ _ _ _ := + λ {_ _ _ _ _ _ _ _ _ _ := undefined -- comment after first + undefined @@ -296,8 +300,7 @@ module Traits; showStringI : Show String := mkShow (show := id); instance - showBoolI : Show Bool := - mkShow (show := λ {x := ite x "true" "false"}); + showBoolI : Show Bool := mkShow (show := λ {x := ite x "true" "false"}); instance showNatI : Show Nat := mkShow (show := natToString); @@ -309,16 +312,14 @@ module Traits; g : {A : Type} → {{Show A}} → Nat := 5; instance - showListI {A} {{Show A}} : Show (List A) := - mkShow (show := showList); + showListI {A} {{Show A}} : Show (List A) := mkShow (show := showList); showMaybe {A} {{Show A}} : Maybe A → String | (just x) := "just (" ++str Show.show x ++str ")" | nothing := "nothing"; instance - showMaybeI {A} {{Show A}} : Show (Maybe A) := - mkShow (show := showMaybe); + showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow (show := showMaybe); f {A} {{Show A}} : A → String | x := Show.show x; @@ -376,6 +377,8 @@ l1 : List Int := ; longLongLongArg ; longLongLongArg ; longLongLongArg + ; longLongLongArg + ; longLongLongArg ]; l2 : List Int := [1; 2; 3]; @@ -385,12 +388,16 @@ l3 : List (List Int) := ; longLongLongListArg ; longLongLongListArg ; longLongLongListArg + ; longLongLongListArg + ; longLongLongListArg ]; l4 : List (List Int) := [ [1; 2; 3] ; longLongLongListArg ; [ longLongLongArg + ; longLongLongArg + ; longLongLongArg ; longLongLongArg ; longLongLongArg ; longLongLongArg @@ -411,7 +418,7 @@ i2479' : {_ : Nat} -> Nat | {_} := zero; -- formatting arguments that do not fit in a line -fffffffffffffffffffffffffffffffffffffffffffffffff +fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff {f : List Nat} : Nat := zero; -- formatting arguments that do not fit in a line diff --git a/tests/positive/Iterators.juvix b/tests/positive/Iterators.juvix index 8a3729a48..49b83808d 100644 --- a/tests/positive/Iterators.juvix +++ b/tests/positive/Iterators.juvix @@ -1,12 +1,10 @@ module Iterators; syntax iterator for {init := 1; range := 1}; -for {A B : Type} (f : A → B → A) (x : A) (y : B) : A := - f x y; +for {A B : Type} (f : A → B → A) (x : A) (y : B) : A := f x y; syntax iterator itconst {init := 2; range := 2}; -itconst - : {A B C : Type} → (A → A → B → C → A) → A → A → B → C → A +itconst : {A B C : Type} → (A → A → B → C → A) → A → A → B → C → A | f := f; builtin bool diff --git a/tests/positive/Judoc.juvix b/tests/positive/Judoc.juvix index 816a7fe50..98cb2e029 100644 --- a/tests/positive/Judoc.juvix +++ b/tests/positive/Judoc.juvix @@ -9,9 +9,7 @@ type T := --- document constructor t : T; ---- blah ;id A; and ;A A id T A id; this is another ;id - id - id; example +--- blah ;id A; and ;A A id T A id; this is another ;id id id; example --- hahahah --- and another one ;T; id : {A : Type} → A → A diff --git a/tests/positive/StdlibList/Data/List.juvix b/tests/positive/StdlibList/Data/List.juvix index 75ba0de7f..c5607fb44 100644 --- a/tests/positive/StdlibList/Data/List.juvix +++ b/tests/positive/StdlibList/Data/List.juvix @@ -10,13 +10,11 @@ type List (A : Type) := match : {A : Type} → {B : Type} → A → (A → B) → B | x f := f x; -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 | a b f z (:: h hs) := f h (foldr a b 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 | a b f z nil := z | a b f z (:: h hs) := foldl a b f (f z h) hs; @@ -67,18 +65,10 @@ splitAt : (a : Type) → ℕ → List a → List a × List a | a _ nil := , nil nil | a zero xs := , nil xs | a (suc zero) (:: x xs) := , (:: x nil) xs - | a (suc (suc m)) (:: x xs) := - match - (splitAt a m xs) - λ {(, xs' xs'') := , (:: x xs') xs''}; + | a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ {(, xs' xs'') := , (:: x xs') xs''}; terminating -merge - : (a : Type) - → (a → a → Ordering) - → List a - → List a - → List a +merge : (a : Type) → (a → a → Ordering) → List a → List a → List a | a cmp (:: x xs) (:: y ys) := match (cmp x y) @@ -94,8 +84,7 @@ merge | a (:: x xs) ys := :: x (++ a xs ys); terminating -quickSort - : (a : Type) → (a → a → Ordering) → List a → List a +quickSort : (a : Type) → (a → a → Ordering) → List a → List a | a _ nil := nil | a _ (:: x nil) := :: x nil | a cmp (:: x ys) := diff --git a/tests/positive/Syntax.juvix b/tests/positive/Syntax.juvix index 6aa76c2f8..064b0f22b 100644 --- a/tests/positive/Syntax.juvix +++ b/tests/positive/Syntax.juvix @@ -1,8 +1,6 @@ module Syntax; -compose - {A B C : Type} (f : B -> C) (g : A -> B) (x : A) : C := - f (g x); +compose {A B C : Type} (f : B -> C) (g : A -> B) (x : A) : C := f (g x); compose' {A B C : Type} (f : B -> C) (g : A -> B) : A -> C | x := f (g x); @@ -41,8 +39,7 @@ syntax operator ==2 cmp; | _ _ := false; module MutualTypes; - isNotEmpty {a : Type} (t : Tree a) : Bool := - not (isEmpty t); + isNotEmpty {a : Type} (t : Tree a) : Bool := not (isEmpty t); isEmpty {a : Type} : (t : Tree a) -> Bool | empty := true diff --git a/tests/positive/package/Package.juvix b/tests/positive/package/Package.juvix index 599444d14..796cb1b33 100644 --- a/tests/positive/package/Package.juvix +++ b/tests/positive/package/Package.juvix @@ -6,9 +6,6 @@ package : Package := defaultPackage {name := "foo"; version := mkVersion 0 1 0; - dependencies := [ github - "anoma" - "juvix-stdlib" - "adf58a7180b361a022fb53c22ad9e5274ebf6f66" + dependencies := [ github "anoma" "juvix-stdlib" "adf58a7180b361a022fb53c22ad9e5274ebf6f66" ; github "anoma" "juvix-containers" "v0.7.1" ]}; diff --git a/tests/smoke/Commands/dev/highlight.smoke.yaml b/tests/smoke/Commands/dev/highlight.smoke.yaml index 168b79480..2d228fb79 100644 --- a/tests/smoke/Commands/dev/highlight.smoke.yaml +++ b/tests/smoke/Commands/dev/highlight.smoke.yaml @@ -10,7 +10,7 @@ tests: - positive/Internal/LiteralInt.juvix stdout: - contains: | + contains: |- add-text-properties exit-status: 0 @@ -23,7 +23,7 @@ tests: - negative/InfixError.juvix stdout: - contains: | + contains: |- juvix-goto exit-status: 0