mirror of
https://github.com/anoma/juvix.git
synced 2024-08-17 12:10:21 +03:00
Make juvix format
line width 100 with ribbon width 100 (#2883)
This PR increases the ribbon width of `juvix format` from 60 to 100
characters.
Reasons for the compromise to a fixed 100 chars ribbon width:
* It is clear that the ribbon width of 60 characters was too small.
* A ribbon width of 100 is an acceptable compromise between formatting
code for display and editing code in multiple buffers on the same
screen.
* We would like to avoid making the formatter configurable so that Juvix
code has a consistent look and to save future Juvix users from
discussions about formatting. Maxim: "juvix format's style is no one's
favourite, yet juvix format is everyone's favourite" (thanks go fmt).
## Definition of ribbon width from the
[docs](https://hackage.haskell.org/package/prettyprinter-1.7.1/docs/Prettyprinter.html)
> The page has a certain maximum width, which the layouter tries to not
exceed, by inserting line breaks where possible. The functions given in
this module make it fairly straightforward to specify where, and under
what circumstances, such a line break may be inserted by the layouter,
for example via the
[sep](https://hackage.haskell.org/package/prettyprinter-1.7.1/docs/Prettyprinter.html#v:sep)
function.
>
> There is also the concept of ribbon width. The ribbon is the part of a
line that is printed, i.e. the line length without the leading
indentation. The layouters take a ribbon fraction argument, which
specifies how much of a line should be filled before trying to break it
up. A ribbon width of 0.5 in a document of width 80 will result in the
layouter to try to not exceed 0.5*80 = 40 (ignoring current indentation
depth).
Examples from
[`anoma-app-patterns:/Token/Transaction.juvix`](8d7e892de3/Token/Transaction.juvix
).
NB: The file in the repo is unformatted so will not match the layout in
the left column below.
| Current (line width 150, ribbon width 60) | This PR (line width 100,
ribbon width 100) |
| --- | --- |
| <img width="1000" alt="Screenshot 2024-07-10 at 12 22 46"
src="https://github.com/anoma/juvix/assets/92877/108b59bc-4b3d-4b83-a148-bb7069d7bc13">
| <img width="1000" alt="Screenshot 2024-07-10 at 14 41 33"
src="https://github.com/anoma/juvix/assets/92877/c3cc2c11-bd45-4a07-84ba-3de3d960e542">
|
| <img width="1000" alt="Screenshot 2024-07-10 at 12 23 10"
src="https://github.com/anoma/juvix/assets/92877/9f3e2d47-bcac-409a-8b09-12dde5079ec5">
| <img width="1000" alt="Screenshot 2024-07-10 at 14 42 01"
src="https://github.com/anoma/juvix/assets/92877/3e20db90-5f62-48e0-ac38-ec357d5baec0">
|
| <img width="1000" alt="Screenshot 2024-07-10 at 12 23 21"
src="https://github.com/anoma/juvix/assets/92877/995d01a9-d19d-429e-aee4-114a4a40c899">
| <img width="1075" alt="Screenshot 2024-07-10 at 14 42 14"
src="https://github.com/anoma/juvix/assets/92877/3cfd1663-75d2-48a3-9e93-c7938cc62a47">
|
| <img width="1000" alt="Screenshot 2024-07-10 at 12 23 34"
src="https://github.com/anoma/juvix/assets/92877/1623afe4-89a6-4633-86e0-8d4d39e49e93">
| <img width="1000" alt="Screenshot 2024-07-10 at 14 42 29"
src="https://github.com/anoma/juvix/assets/92877/813f602f-04b4-4ed5-a21e-4435a58d8515">
|
| <img width="1086" alt="Screenshot 2024-07-10 at 12 23 50"
src="https://github.com/anoma/juvix/assets/92877/a04d0664-b9d4-46f3-8ea0-72e5ae0660e1">
| <img width="1093" alt="Screenshot 2024-07-10 at 14 42 40"
src="https://github.com/anoma/juvix/assets/92877/5cf2328d-b911-4ad9-bcc8-3611f4f89465">
|
| <img width="1000" alt="Screenshot 2024-07-10 at 12 24 13"
src="https://github.com/anoma/juvix/assets/92877/53053e7a-32e1-440e-9060-1ab15133a934">
| <img width="1058" alt="Screenshot 2024-07-10 at 14 42 57"
src="https://github.com/anoma/juvix/assets/92877/7263732e-a2cf-43f3-9d49-0599175a160d">
|
This commit is contained in:
parent
597824e89d
commit
4e227436ce
@ -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!"
|
||||
|
@ -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;
|
||||
|
@ -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;
|
||||
|
||||
|
@ -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;
|
||||
|
@ -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)};
|
||||
|
@ -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);
|
||||
|
@ -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)));
|
||||
|
@ -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)));
|
||||
|
@ -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;
|
||||
|
@ -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));
|
||||
|
@ -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);
|
||||
|
@ -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;
|
||||
|
@ -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));
|
||||
|
@ -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
|
||||
|
@ -28,8 +28,7 @@ axiom f : String → String;
|
||||
|
||||
x : String := "" + ("" ++ "");
|
||||
|
||||
axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String
|
||||
→ String;
|
||||
axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String → String;
|
||||
|
||||
nesting : String :=
|
||||
wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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) :=
|
||||
|
@ -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
|
||||
|
@ -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"
|
||||
]};
|
||||
|
@ -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
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user