From b8cd84170b6d70117a1fc54c35e69e1cab617471 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 26 Jun 2024 09:23:35 +0100 Subject: [PATCH] Update juvix-stdlib to remove non-ASCII indentifiers (#2857) This PR updates the juvix-stdlib to the current main commit which includes: * https://github.com/anoma/juvix-stdlib/issues/59 * https://github.com/anoma/juvix-stdlib/issues/101 All the Juvix test suite files and examples in this repo have been updated to be compatible with the new stdlib. --- examples/demo/Demo.juvix | 10 ++-- examples/milestone/Bank/Bank.juvix | 2 +- examples/milestone/Collatz/Collatz.juvix | 8 +-- examples/milestone/Fibonacci/Fibonacci.juvix | 3 +- .../milestone/TicTacToe/CLI/TicTacToe.juvix | 9 +-- juvix-stdlib | 2 +- test/Compilation/Positive.hs | 2 +- .../Anoma/Compilation/positive/test003.juvix | 8 +-- .../Anoma/Compilation/positive/test006.juvix | 4 +- .../Anoma/Compilation/positive/test007.juvix | 14 ++--- .../Anoma/Compilation/positive/test009.juvix | 6 +- .../Anoma/Compilation/positive/test011.juvix | 4 +- .../Anoma/Compilation/positive/test012.juvix | 8 +-- .../Anoma/Compilation/positive/test013.juvix | 6 +- .../Anoma/Compilation/positive/test014.juvix | 6 +- .../Anoma/Compilation/positive/test015.juvix | 10 ++-- .../Anoma/Compilation/positive/test020.juvix | 16 ++--- .../Anoma/Compilation/positive/test021.juvix | 2 +- .../Anoma/Compilation/positive/test022.juvix | 12 ++-- .../Anoma/Compilation/positive/test023.juvix | 2 +- .../Anoma/Compilation/positive/test025.juvix | 8 +-- .../Anoma/Compilation/positive/test026.juvix | 2 +- .../Anoma/Compilation/positive/test027.juvix | 10 ++-- .../Anoma/Compilation/positive/test028.juvix | 2 +- .../Anoma/Compilation/positive/test029.juvix | 8 +-- .../Anoma/Compilation/positive/test030.juvix | 8 +-- .../Anoma/Compilation/positive/test032.juvix | 6 +- .../Anoma/Compilation/positive/test033.juvix | 18 +++--- .../Anoma/Compilation/positive/test034.juvix | 8 +-- .../Anoma/Compilation/positive/test035.juvix | 10 ++-- .../Anoma/Compilation/positive/test036.juvix | 6 +- .../Anoma/Compilation/positive/test039.juvix | 2 +- .../Anoma/Compilation/positive/test049.juvix | 32 +++++----- .../Anoma/Compilation/positive/test054.juvix | 4 +- .../Anoma/Compilation/positive/test055.juvix | 6 +- .../Anoma/Compilation/positive/test060.juvix | 4 +- .../Anoma/Compilation/positive/test061.juvix | 24 ++++---- .../Anoma/Compilation/positive/test063.juvix | 14 ++--- .../Anoma/Compilation/positive/test069.juvix | 2 +- .../Anoma/Compilation/positive/test071.juvix | 2 +- .../Compilation/positive/test072/Monad.juvix | 4 +- .../Compilation/positive/test072/Reader.juvix | 2 +- .../positive/test072/ReaderT.juvix | 8 +-- .../Compilation/positive/test072/State.juvix | 2 +- .../Compilation/positive/test072/StateT.juvix | 6 +- .../Anoma/Compilation/positive/test074.juvix | 2 +- .../Anoma/Compilation/positive/test075.juvix | 6 +- .../Anoma/Compilation/positive/test076.juvix | 6 +- tests/Casm/Compilation/positive/test030.juvix | 2 +- tests/Casm/Compilation/positive/test032.juvix | 4 +- tests/Casm/Compilation/positive/test033.juvix | 8 +-- tests/Casm/Compilation/positive/test035.juvix | 2 +- tests/Casm/Compilation/positive/test036.juvix | 6 +- tests/Casm/Compilation/positive/test054.juvix | 4 +- tests/Casm/Compilation/positive/test060.juvix | 6 +- tests/Casm/Compilation/positive/test069.juvix | 2 +- tests/Casm/Compilation/positive/test071.juvix | 2 +- .../Compilation/positive/test072/Monad.juvix | 4 +- .../Compilation/positive/test072/Reader.juvix | 2 +- .../positive/test072/ReaderT.juvix | 8 +-- .../Compilation/positive/test072/State.juvix | 2 +- .../Compilation/positive/test072/StateT.juvix | 6 +- tests/Casm/Compilation/positive/test077.juvix | 6 +- tests/Compilation/positive/test003.juvix | 8 +-- tests/Compilation/positive/test004.juvix | 10 ++-- tests/Compilation/positive/test006.juvix | 4 +- tests/Compilation/positive/test007.juvix | 18 +++--- tests/Compilation/positive/test009.juvix | 6 +- tests/Compilation/positive/test011.juvix | 4 +- tests/Compilation/positive/test012.juvix | 24 ++++---- tests/Compilation/positive/test013.juvix | 6 +- tests/Compilation/positive/test014.juvix | 6 +- tests/Compilation/positive/test015.juvix | 10 ++-- tests/Compilation/positive/test020.juvix | 16 ++--- tests/Compilation/positive/test021.juvix | 4 +- tests/Compilation/positive/test022.juvix | 12 ++-- tests/Compilation/positive/test023.juvix | 4 +- tests/Compilation/positive/test025.juvix | 8 +-- tests/Compilation/positive/test026.juvix | 2 +- tests/Compilation/positive/test027.juvix | 10 ++-- tests/Compilation/positive/test028.juvix | 6 +- tests/Compilation/positive/test029.juvix | 10 ++-- tests/Compilation/positive/test030.juvix | 8 +-- tests/Compilation/positive/test031.juvix | 2 +- tests/Compilation/positive/test032.juvix | 8 +-- tests/Compilation/positive/test033.juvix | 27 ++++----- tests/Compilation/positive/test034.juvix | 8 +-- tests/Compilation/positive/test035.juvix | 18 +++--- tests/Compilation/positive/test036.juvix | 6 +- tests/Compilation/positive/test039.juvix | 2 +- tests/Compilation/positive/test049.juvix | 60 +++++++++---------- tests/Compilation/positive/test051.juvix | 4 +- tests/Compilation/positive/test054.juvix | 4 +- tests/Compilation/positive/test055.juvix | 6 +- tests/Compilation/positive/test060.juvix | 4 +- tests/Compilation/positive/test061.juvix | 32 +++++----- tests/Compilation/positive/test063.juvix | 14 ++--- tests/Compilation/positive/test069.juvix | 2 +- tests/Compilation/positive/test071.juvix | 2 +- .../Compilation/positive/test072/Monad.juvix | 4 +- .../Compilation/positive/test072/Reader.juvix | 2 +- .../positive/test072/ReaderT.juvix | 8 +-- .../Compilation/positive/test072/State.juvix | 4 +- .../Compilation/positive/test072/StateT.juvix | 6 +- tests/Geb/positive/Compilation/test011.juvix | 6 +- tests/Geb/positive/Compilation/test027.juvix | 5 +- tests/Internal/positive/AsPatterns.juvix | 10 ++-- tests/Internal/positive/Case.juvix | 2 +- tests/Internal/positive/Church.juvix | 2 +- tests/Internal/positive/Lambda.juvix | 16 ++--- tests/Internal/positive/LitIntegerToNat.juvix | 2 +- tests/Internal/positive/QuickSort.juvix | 4 +- tests/Rust/Compilation/positive/test030.juvix | 2 +- tests/Rust/Compilation/positive/test032.juvix | 4 +- tests/Rust/Compilation/positive/test033.juvix | 8 +-- tests/Rust/Compilation/positive/test035.juvix | 2 +- tests/Rust/Compilation/positive/test036.juvix | 6 +- tests/Rust/Compilation/positive/test054.juvix | 4 +- tests/Rust/Compilation/positive/test060.juvix | 6 +- tests/Rust/Compilation/positive/test069.juvix | 2 +- tests/Rust/Compilation/positive/test071.juvix | 2 +- .../Compilation/positive/test072/Monad.juvix | 4 +- .../Compilation/positive/test072/Reader.juvix | 2 +- .../positive/test072/ReaderT.juvix | 8 +-- .../Compilation/positive/test072/State.juvix | 2 +- .../Compilation/positive/test072/StateT.juvix | 6 +- .../VampIR/positive/Compilation/test002.juvix | 2 +- .../VampIR/positive/Compilation/test003.juvix | 2 +- .../VampIR/positive/Compilation/test006.juvix | 2 +- .../VampIR/positive/Compilation/test009.juvix | 2 +- .../VampIR/positive/Compilation/test020.juvix | 2 +- .../benchmark/ackermann/juvix/ackermann.juvix | 2 +- .../benchmark/mergesort/juvix/mergesort.juvix | 6 +- tests/negative/issue2771/Main.juvix | 7 +-- tests/positive/Ape.juvix | 18 +++--- tests/positive/Internal/AsPattern.juvix | 8 +-- tests/positive/Internal/Implicit.juvix | 4 +- tests/positive/Internal/Lambda.juvix | 4 +- tests/positive/Internal/Synonyms.juvix | 2 +- tests/positive/Markdown/Test.juvix.md | 2 +- tests/positive/Markdown/markdown/Test.md | 2 +- tests/positive/Traits2.juvix | 17 +++--- tests/positive/issue1693/M.juvix | 2 +- tests/positive/issue1731/builtinFail.juvix | 4 +- tests/positive/issue1731/builtinTrace.juvix | 14 ++--- ...pile-dependencies-package-juvix.smoke.yaml | 6 +- .../Commands/compile-dependencies.smoke.yaml | 6 +- tests/smoke/Commands/dev/repl.smoke.yaml | 2 +- tests/smoke/Commands/repl.smoke.yaml | 10 ++-- 149 files changed, 520 insertions(+), 520 deletions(-) diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix index 30c07d167..11de93e94 100644 --- a/examples/demo/Demo.juvix +++ b/examples/demo/Demo.juvix @@ -43,11 +43,11 @@ sort {A} {{Ord A}} : List A → List A printNatListLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printNatListLn xs; + printNat x >>> printString " :: " >>> printNatListLn xs; main : IO := printStringLn "Hello!" - >> printNatListLn (preorder (mirror tree)) - >> printNatListLn (sort (preorder (mirror tree))) - >> printNatLn (log2 3) - >> printNatLn (log2 130); + >>> printNatListLn (preorder (mirror tree)) + >>> printNatListLn (sort (preorder (mirror tree))) + >>> printNatLn (log2 3) + >>> printNatLn (log2 130); diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix index e7b26d9ae..378139252 100644 --- a/examples/milestone/Bank/Bank.juvix +++ b/examples/milestone/Bank/Bank.juvix @@ -34,7 +34,7 @@ open Token; --- This module defines the type for balances and its associated operations. module Balances; - Balances : Type := List (Field × Nat); + Balances : Type := List (Pair Field Nat); --- Increments the amount associated with a certain ;Field;. increment : Field -> Nat -> Balances -> Balances diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix index 6cb4a4e01..e697b1b5c 100644 --- a/examples/milestone/Collatz/Collatz.juvix +++ b/examples/milestone/Collatz/Collatz.juvix @@ -12,8 +12,8 @@ collatz : Nat → Nat terminating run (f : Nat → Nat) : Nat → IO - | (suc zero) := printNatLn 1 >> printStringLn "Finished!" - | n := printNatLn n >> run f (f n); + | (suc zero) := printNatLn 1 >>> printStringLn "Finished!" + | n := printNatLn n >>> run f (f n); welcome : String := "Collatz calculator\n------------------\n\nType a number then ENTER"; @@ -22,7 +22,7 @@ resultHeading : String := "Collatz sequence:"; main : IO := printStringLn welcome - >> readLn + >>> readLn λ {s := printStringLn resultHeading - >> run collatz (stringToNat s)}; + >>> run collatz (stringToNat s)}; diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix index 56f23c251..631e41bb7 100644 --- a/examples/milestone/Fibonacci/Fibonacci.juvix +++ b/examples/milestone/Fibonacci/Fibonacci.juvix @@ -8,4 +8,5 @@ fib : Nat → Nat → Nat → Nat fibonacci (n : Nat) : Nat := fib n 0 1; -main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat); +main : IO := + readLn (stringToNat >> fibonacci >> printNatLn); diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix index c7ec9c37a..0cea3e91f 100644 --- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix @@ -17,7 +17,7 @@ prompt (x : GameState) : String := ++str ": "; nextMove (s : GameState) : String → GameState := - flip playMove s ∘ validMove ∘ stringToNat; + stringToNat >> validMove >> flip playMove s; --- Main loop terminating @@ -30,12 +30,13 @@ run : GameState → IO ++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); + >>> readLn (run << nextMove (state b p noError)) + | 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"; --- The entry point of the program -main : IO := printStringLn welcome >> run beginState; +main : IO := printStringLn welcome >>> run beginState; diff --git a/juvix-stdlib b/juvix-stdlib index 73ecbc577..00f6f503d 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 73ecbc57738f4bde6f4f39636436ba38504b33f6 +Subproject commit 00f6f503dbc2cfa72bd469fb8ce7edd0e9730639 diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 4a746c019..735851008 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -327,7 +327,7 @@ tests = $(mkRelFile "test050.juvix") $(mkRelFile "out/test050.out"), posTest - "Test051: Local recursive function using IO >>" + "Test051: Local recursive function using IO >>>" $(mkRelDir ".") $(mkRelFile "test051.juvix") $(mkRelFile "out/test051.out"), diff --git a/tests/Anoma/Compilation/positive/test003.juvix b/tests/Anoma/Compilation/positive/test003.juvix index 9cbc58fef..8e0005ad5 100644 --- a/tests/Anoma/Compilation/positive/test003.juvix +++ b/tests/Anoma/Compilation/positive/test003.juvix @@ -14,7 +14,7 @@ import Stdlib.Debug.Trace open; main : Nat := trace (mod 3 2) - >>> trace (div 18 4) - >>> trace (mod 18 4) - >>> trace (div 16 4) - >>> mod 16 4; + >-> trace (div 18 4) + >-> trace (mod 18 4) + >-> trace (div 16 4) + >-> mod 16 4; diff --git a/tests/Anoma/Compilation/positive/test006.juvix b/tests/Anoma/Compilation/positive/test006.juvix index 3828f0655..2d6d99732 100644 --- a/tests/Anoma/Compilation/positive/test006.juvix +++ b/tests/Anoma/Compilation/positive/test006.juvix @@ -10,5 +10,5 @@ loop : Nat := loop; main : Bool := trace (if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1)) - >>> trace (2 > 0 || loop == 0) - >>> 2 < 0 && loop == 0; + >-> trace (2 > 0 || loop == 0) + >-> 2 < 0 && loop == 0; diff --git a/tests/Anoma/Compilation/positive/test007.juvix b/tests/Anoma/Compilation/positive/test007.juvix index cd6d7ab6c..6c68d86ec 100644 --- a/tests/Anoma/Compilation/positive/test007.juvix +++ b/tests/Anoma/Compilation/positive/test007.juvix @@ -20,11 +20,11 @@ lst : List Nat := 0 :: 1 :: nil; main : List Nat := trace (null lst) - >>> trace (null (nil {Nat})) - >>> trace (head 1 lst) - >>> trace (tail lst) - >>> trace (head 0 (tail lst)) - >>> trace (map ((+) 1) lst) - >>> map' ((+) 1) lst + >-> trace (null (nil {Nat})) + >-> trace (head 1 lst) + >-> trace (tail lst) + >-> trace (head 0 (tail lst)) + >-> trace (map ((+) 1) lst) + >-> map' ((+) 1) lst -- TODO: Restore when anoma backend supports strings - -- >>> runPartial λ {{{_}} := map'' ((+) 1) lst}; + -- >-> runPartial λ {{{_}} := map'' ((+) 1) lst}; diff --git a/tests/Anoma/Compilation/positive/test009.juvix b/tests/Anoma/Compilation/positive/test009.juvix index f77b2af05..051f7be47 100644 --- a/tests/Anoma/Compilation/positive/test009.juvix +++ b/tests/Anoma/Compilation/positive/test009.juvix @@ -18,6 +18,6 @@ fact : Nat → Nat := fact' 1; main (n : Nat) : Nat := trace (sum n) - >>> trace (fact 5) - >>> trace (fact 10) - >>> fact 12; + >-> trace (fact 5) + >-> trace (fact 10) + >-> fact 12; diff --git a/tests/Anoma/Compilation/positive/test011.juvix b/tests/Anoma/Compilation/positive/test011.juvix index 6b7f5a75a..03459c723 100644 --- a/tests/Anoma/Compilation/positive/test011.juvix +++ b/tests/Anoma/Compilation/positive/test011.juvix @@ -12,5 +12,5 @@ fib : Nat → Nat := fib' 0 1; main : Nat := trace (fib 10) - >>> trace (fib 100) - >>> fib 1000; + >-> trace (fib 100) + >-> fib 1000; diff --git a/tests/Anoma/Compilation/positive/test012.juvix b/tests/Anoma/Compilation/positive/test012.juvix index 6f600a2e2..17818374a 100644 --- a/tests/Anoma/Compilation/positive/test012.juvix +++ b/tests/Anoma/Compilation/positive/test012.juvix @@ -32,7 +32,7 @@ combineDigits (xs : List Nat) : Nat := for (acc := 0) (x in xs) acc * 10 + x; main : Nat := trace (combineDigits (preorder (gen 3))) - >>> trace (combineDigits (preorder (gen 4))) - >>> trace (combineDigits (preorder (gen 5))) - >>> trace (combineDigits (preorder (gen 6))) - >>> combineDigits (preorder (gen 7)); + >-> trace (combineDigits (preorder (gen 4))) + >-> trace (combineDigits (preorder (gen 5))) + >-> trace (combineDigits (preorder (gen 6))) + >-> combineDigits (preorder (gen 7)); diff --git a/tests/Anoma/Compilation/positive/test013.juvix b/tests/Anoma/Compilation/positive/test013.juvix index ffe7eeafb..9b0574404 100644 --- a/tests/Anoma/Compilation/positive/test013.juvix +++ b/tests/Anoma/Compilation/positive/test013.juvix @@ -16,6 +16,6 @@ f : Nat → Nat → Nat main : Nat := trace (f 5 6) - >>> trace (f 6 5) - >>> trace (f 10 5) - >>> f 11 5; + >-> trace (f 6 5) + >-> trace (f 10 5) + >-> f 11 5; diff --git a/tests/Anoma/Compilation/positive/test014.juvix b/tests/Anoma/Compilation/positive/test014.juvix index d965d1f54..d6060ec6c 100644 --- a/tests/Anoma/Compilation/positive/test014.juvix +++ b/tests/Anoma/Compilation/positive/test014.juvix @@ -24,13 +24,13 @@ vy : Nat := 7; main : Nat := trace (func (div y x)) - >>> -- 17 div 5 + 4 = 7 + >-> -- 17 div 5 + 4 = 7 trace (y + x * z) - >>> -- 17 + >-> -- 17 trace (vx + vy * (z + 1)) - >>> -- 37 + >-> -- 37 f (h g 2 3) 4; diff --git a/tests/Anoma/Compilation/positive/test015.juvix b/tests/Anoma/Compilation/positive/test015.juvix index e2195e8d9..eb93c97b6 100644 --- a/tests/Anoma/Compilation/positive/test015.juvix +++ b/tests/Anoma/Compilation/positive/test015.juvix @@ -23,19 +23,19 @@ h : Nat → Nat main : Nat := trace (f 100 500) - >>> -- 600 + >-> -- 600 trace (f 5 0) - >>> -- 25 + >-> -- 25 trace (f 5 5) - >>> -- 30 + >-> -- 30 trace (h 10) - >>> -- 45 + >-> -- 45 trace (g 10 h) - >>> -- 55 + >-> -- 55 g 3 (f 10); diff --git a/tests/Anoma/Compilation/positive/test020.juvix b/tests/Anoma/Compilation/positive/test020.juvix index d0b41a2e1..6f516f29c 100644 --- a/tests/Anoma/Compilation/positive/test020.juvix +++ b/tests/Anoma/Compilation/positive/test020.juvix @@ -16,11 +16,11 @@ subp : Nat → Nat → Nat main : Nat := trace (f91 101) - >>> trace (f91 95) - >>> trace (f91 16) - >>> trace (f91 5) - >>> trace (subp 101 1) - >>> trace (subp 11 5) - >>> trace (subp 10 4) - >>> trace (subp 1000 600) - >>> subp 10000 6000; + >-> trace (f91 95) + >-> trace (f91 16) + >-> trace (f91 5) + >-> trace (subp 101 1) + >-> trace (subp 11 5) + >-> trace (subp 10 4) + >-> trace (subp 1000 600) + >-> subp 10000 6000; diff --git a/tests/Anoma/Compilation/positive/test021.juvix b/tests/Anoma/Compilation/positive/test021.juvix index 0b1fa205f..2130e3ef0 100644 --- a/tests/Anoma/Compilation/positive/test021.juvix +++ b/tests/Anoma/Compilation/positive/test021.juvix @@ -18,4 +18,4 @@ power' : Nat → Nat → Nat → Nat power : Nat → Nat → Nat := power' 1; main : Nat := - trace (power 2 3) >>> trace (power 3 7) >>> power 5 11; + trace (power 2 3) >-> trace (power 3 7) >-> power 5 11; diff --git a/tests/Anoma/Compilation/positive/test022.juvix b/tests/Anoma/Compilation/positive/test022.juvix index b896ee59f..5deab316a 100644 --- a/tests/Anoma/Compilation/positive/test022.juvix +++ b/tests/Anoma/Compilation/positive/test022.juvix @@ -17,12 +17,12 @@ sum' : Nat → Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (h :: t) := - printNat h >> printString " :: " >> printListNatLn t; + printNat h >>> printString " :: " >>> printListNatLn t; main (n : Nat) : Nat := trace (gen 10) - >>> trace (reverse (gen 10)) - >>> trace (filter ((<) 5) (gen 10)) - >>> trace (reverse (map (flip sub 1) (gen 10))) - >>> trace (sum n) - >>> sum' n; + >-> trace (reverse (gen 10)) + >-> trace (filter ((<) 5) (gen 10)) + >-> trace (reverse (map (flip sub 1) (gen 10))) + >-> trace (sum n) + >-> sum' n; diff --git a/tests/Anoma/Compilation/positive/test023.juvix b/tests/Anoma/Compilation/positive/test023.juvix index c5d19fa8a..706408b22 100644 --- a/tests/Anoma/Compilation/positive/test023.juvix +++ b/tests/Anoma/Compilation/positive/test023.juvix @@ -17,4 +17,4 @@ terminating h : Nat → Nat | x := if (x < 1) 1 (x * f (sub x 1)); -main : Nat := trace (f 5) >>> trace (f 10) >>> f 20; +main : Nat := trace (f 5) >-> trace (f 10) >-> f 20; diff --git a/tests/Anoma/Compilation/positive/test025.juvix b/tests/Anoma/Compilation/positive/test025.juvix index b7b744376..bd2b1cfef 100644 --- a/tests/Anoma/Compilation/positive/test025.juvix +++ b/tests/Anoma/Compilation/positive/test025.juvix @@ -11,7 +11,7 @@ gcd : Nat → Nat → Nat main : Nat := trace (gcd (3 * 7 * 2) (7 * 2 * 11)) - >>> trace (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5)) - >>> trace (gcd 3 7) - >>> trace (gcd 7 3) - >>> gcd (11 * 7 * 3) (2 * 5 * 13); + >-> trace (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5)) + >-> trace (gcd 3 7) + >-> trace (gcd 7 3) + >-> gcd (11 * 7 * 3) (2 * 5 * 13); diff --git a/tests/Anoma/Compilation/positive/test026.juvix b/tests/Anoma/Compilation/positive/test026.juvix index ceedf68a1..22a241e07 100644 --- a/tests/Anoma/Compilation/positive/test026.juvix +++ b/tests/Anoma/Compilation/positive/test026.juvix @@ -30,7 +30,7 @@ drop_front : {A : Type} → Queue A → Queue A | nil := queue (reverse (qsnd q')) nil | _ := q'; -pop_front {A} : Queue A -> Maybe (A × Queue A) +pop_front {A} : Queue A -> Maybe (Pair A (Queue A)) | (queue xs ys) := case xs of | h :: t := just (h, queue t ys) diff --git a/tests/Anoma/Compilation/positive/test027.juvix b/tests/Anoma/Compilation/positive/test027.juvix index 32ab466ec..93dd4bac4 100644 --- a/tests/Anoma/Compilation/positive/test027.juvix +++ b/tests/Anoma/Compilation/positive/test027.juvix @@ -10,17 +10,17 @@ czero : Num | {_} f x := x; csuc : Num → Num - | n {_} f := f ∘ n {_} f; + | n {_} f := f << n {_} f; num : Nat → Num | zero := czero | (suc n) := csuc (num n); add : Num → Num → Num - | n m {_} f := n {_} f ∘ m {_} f; + | n m {_} f := n {_} f << m {_} f; mul : Num → Num → Num - | n m {_} := n {_} ∘ m {_}; + | n m {_} := n {_} << m {_}; isZero : Num → Bool | n := n {_} (const false) true; @@ -30,5 +30,5 @@ toNat : Num → Nat main : Nat := trace (toNat (num 7)) - >>> trace (toNat (add (num 7) (num 3))) - >>> toNat (mul (num 7) (num 3)); + >-> trace (toNat (add (num 7) (num 3))) + >-> toNat (mul (num 7) (num 3)); diff --git a/tests/Anoma/Compilation/positive/test028.juvix b/tests/Anoma/Compilation/positive/test028.juvix index 51478ac54..e5b34db0c 100644 --- a/tests/Anoma/Compilation/positive/test028.juvix +++ b/tests/Anoma/Compilation/positive/test028.juvix @@ -45,4 +45,4 @@ primes : Unit → Stream := eratostenes (numbers 2); main (n1 n2 : Nat) : Nat := trace (snth n1 primes) - >>> snth n2 primes; + >-> snth n2 primes; diff --git a/tests/Anoma/Compilation/positive/test029.juvix b/tests/Anoma/Compilation/positive/test029.juvix index d5fbfa783..82bc305d5 100644 --- a/tests/Anoma/Compilation/positive/test029.juvix +++ b/tests/Anoma/Compilation/positive/test029.juvix @@ -11,7 +11,7 @@ ack : Nat → Nat → Nat main : Nat := trace (ack 0 7) - >>> trace (ack 1 7) - >>> trace (ack 1 13) - >>> trace (ack 2 7) - >>> ack 2 13; + >-> trace (ack 1 7) + >-> trace (ack 1 13) + >-> trace (ack 2 7) + >-> ack 2 13; diff --git a/tests/Anoma/Compilation/positive/test030.juvix b/tests/Anoma/Compilation/positive/test030.juvix index 3999b2477..f928889f1 100644 --- a/tests/Anoma/Compilation/positive/test030.juvix +++ b/tests/Anoma/Compilation/positive/test030.juvix @@ -8,7 +8,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A -- clauses with differing number of patterns not yet supported -- iterate f zero x := x; | f zero := id - | f (suc n) := f ∘ iterate f n; + | f (suc n) := f << iterate f n; plus : Nat → Nat → Nat := iterate suc; @@ -23,6 +23,6 @@ ackermann : Nat → Nat → Nat main : Nat := trace (plus 3 7) - >>> trace (mult 3 7) - >>> trace (exp 3 7) - >>> ackermann 1 13; + >-> trace (mult 3 7) + >-> trace (exp 3 7) + >-> ackermann 1 13; diff --git a/tests/Anoma/Compilation/positive/test032.juvix b/tests/Anoma/Compilation/positive/test032.juvix index 2a67798b7..732989dfe 100644 --- a/tests/Anoma/Compilation/positive/test032.juvix +++ b/tests/Anoma/Compilation/positive/test032.juvix @@ -4,7 +4,7 @@ module test032; import Stdlib.Prelude open; import Stdlib.Debug.Trace open; -split : {A : Type} → Nat → List A → List A × List A +split : {A : Type} → Nat → List A → Pair (List A) (List A) | zero xs := nil, xs | (suc n) nil := nil, nil | (suc n) (x :: xs) := @@ -46,5 +46,5 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat) main : List Nat := trace (take 10 (uniq (sort (flatten (gen2 nil 6 10))))) - >>> trace (take 10 (uniq (sort (flatten (gen2 nil 7 10))))) - >>> take 10 (uniq (sort (flatten (gen2 nil 6 20)))); + >-> trace (take 10 (uniq (sort (flatten (gen2 nil 7 10))))) + >-> take 10 (uniq (sort (flatten (gen2 nil 6 20)))); diff --git a/tests/Anoma/Compilation/positive/test033.juvix b/tests/Anoma/Compilation/positive/test033.juvix index e6d4f2935..e5f121296 100644 --- a/tests/Anoma/Compilation/positive/test033.juvix +++ b/tests/Anoma/Compilation/positive/test033.juvix @@ -10,24 +10,24 @@ f : (Nat → Nat) → Nat f' : Nat → Nat | x := f ((+) x); -g : (Nat → Nat × Nat) → Nat × Nat +g : (Nat → Pair Nat Nat) → Pair Nat Nat | f := f 2; -g' : Nat → Nat × Nat +g' : Nat → Pair Nat Nat | x := g ((,) x); f1' : Nat → Nat → Nat | x y := f ((+) (div x y)); -g1' : Nat → Nat → Nat × Nat +g1' : Nat → Nat → Pair Nat Nat | x y := g ((,) (div x y)); -h : (Nat → Nat → Nat × Nat) → Nat × Nat +h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat | f := f 1 2; -main : Nat × Nat := +main : Pair Nat Nat := trace (f' 7) - >>> trace (g' 7) - >>> trace (f1' 7 2) - >>> trace (g1' 7 2) - >>> h (,); + >-> trace (g' 7) + >-> trace (f1' 7 2) + >-> trace (g1' 7 2) + >-> h (,); diff --git a/tests/Anoma/Compilation/positive/test034.juvix b/tests/Anoma/Compilation/positive/test034.juvix index 18bec55f8..99ac0798b 100644 --- a/tests/Anoma/Compilation/positive/test034.juvix +++ b/tests/Anoma/Compilation/positive/test034.juvix @@ -22,8 +22,8 @@ mutrec : Nat := terminating h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1)); in trace (f 5) - >>> trace (f 10) - >>> trace (g 5) - >>> h 5; + >-> trace (f 10) + >-> trace (g 5) + >-> h 5; -main : Nat := trace (sum 1000) >>> mutrec; +main : Nat := trace (sum 1000) >-> mutrec; diff --git a/tests/Anoma/Compilation/positive/test035.juvix b/tests/Anoma/Compilation/positive/test035.juvix index a73e30b63..9276ffd3a 100644 --- a/tests/Anoma/Compilation/positive/test035.juvix +++ b/tests/Anoma/Compilation/positive/test035.juvix @@ -43,8 +43,8 @@ h : Nat -> Nat main : Nat := trace (sum2 (lgen 5)) - >>> trace (f (gen 10)) - >>> trace (f (gen 15)) - >>> trace (f (gen 16)) - >>> trace (h 5) - >>> h 3; + >-> trace (f (gen 10)) + >-> trace (f (gen 15)) + >-> trace (f (gen 16)) + >-> trace (h 5) + >-> h 3; diff --git a/tests/Anoma/Compilation/positive/test036.juvix b/tests/Anoma/Compilation/positive/test036.juvix index 6a64c5f61..77c982774 100644 --- a/tests/Anoma/Compilation/positive/test036.juvix +++ b/tests/Anoma/Compilation/positive/test036.juvix @@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A f : Nat → Nat := suc; g : Nat → Nat → Nat - | z := f ∘ flip sub z; + | z := f << flip sub z; g' : Nat → Nat → Nat - | z := f ∘ λ {x := sub x z}; + | z := f << λ {x := sub x z}; -h : Nat → Nat := f ∘ g 3; +h : Nat → Nat := f << g 3; j : Nat → Nat → Nat := g'; diff --git a/tests/Anoma/Compilation/positive/test039.juvix b/tests/Anoma/Compilation/positive/test039.juvix index 5687cd62b..6f4841e61 100644 --- a/tests/Anoma/Compilation/positive/test039.juvix +++ b/tests/Anoma/Compilation/positive/test039.juvix @@ -15,4 +15,4 @@ main : Bool := | zero := true | (suc n) := not (odd n); plusOne (n : Ty) : Ty := n + 1; - in trace (odd (plusOne 13)) >>> even (plusOne 12); + in trace (odd (plusOne 13)) >-> even (plusOne 12); diff --git a/tests/Anoma/Compilation/positive/test049.juvix b/tests/Anoma/Compilation/positive/test049.juvix index 88406a6cb..8cef7b132 100644 --- a/tests/Anoma/Compilation/positive/test049.juvix +++ b/tests/Anoma/Compilation/positive/test049.juvix @@ -10,22 +10,22 @@ f : Int -> Nat main : Int := trace (ofNat 1) - >>> trace (ofNat (suc zero)) - >>> trace (f -1) - >>> trace (f (ofNat (suc zero))) - >>> trace (f (negSuc (suc zero))) - >>> trace (1 == -1) - >>> trace (neg -1) - >>> trace + >-> trace (ofNat (suc zero)) + >-> trace (f -1) + >-> trace (f (ofNat (suc zero))) + >-> trace (f (negSuc (suc zero))) + >-> trace (1 == -1) + >-> trace (neg -1) + >-> trace (let g : Int -> Int := neg; in g -1) - >>> trace (-2 * -2) - >>> trace (nonNeg 0) - >>> trace (nonNeg -1) - >>> trace (0 < 0) - >>> trace (0 <= 0) - >>> trace (0 < 1) - >>> trace (-1 <= 0) - >>> trace (mod 4 -3) - >>> div -6 -3; + >-> trace (-2 * -2) + >-> trace (nonNeg 0) + >-> trace (nonNeg -1) + >-> trace (0 < 0) + >-> trace (0 <= 0) + >-> trace (0 < 1) + >-> trace (-1 <= 0) + >-> trace (mod 4 -3) + >-> div -6 -3; diff --git a/tests/Anoma/Compilation/positive/test054.juvix b/tests/Anoma/Compilation/positive/test054.juvix index aae917428..2b1a49c55 100644 --- a/tests/Anoma/Compilation/positive/test054.juvix +++ b/tests/Anoma/Compilation/positive/test054.juvix @@ -36,12 +36,12 @@ myfor2 syntax iterator myzip2 {init := 2; range := 2}; myzip2 : {A A' B C : Type} - → (A → A' → B → C → A × A') + → (A → A' → B → C → Pair A A') → A → A' → List B → List C - → A × A' + → Pair A A' | f a b xs ys := myfor (acc, acc' := a, b) (x, y in zip xs ys) f acc acc' x y; diff --git a/tests/Anoma/Compilation/positive/test055.juvix b/tests/Anoma/Compilation/positive/test055.juvix index a95219117..120fb8a31 100644 --- a/tests/Anoma/Compilation/positive/test055.juvix +++ b/tests/Anoma/Compilation/positive/test055.juvix @@ -3,9 +3,9 @@ module test055; import Stdlib.Prelude open; -type Pair := - | pair : Nat -> Nat -> Pair; +type Pair' := + | pair : Nat -> Nat -> Pair'; -main : List (Pair × Nat) × List Pair := +main : Pair (List (Pair Pair' Nat)) (List Pair') := (pair 1 2, 3) :: (pair 2 3, 4) :: nil , pair 1 2 :: pair 2 3 :: nil; diff --git a/tests/Anoma/Compilation/positive/test060.juvix b/tests/Anoma/Compilation/positive/test060.juvix index 20edd30f7..abc464316 100644 --- a/tests/Anoma/Compilation/positive/test060.juvix +++ b/tests/Anoma/Compilation/positive/test060.juvix @@ -10,13 +10,13 @@ type Triple (A B C : Type) := thd : C }; -type Pair (A B : Type) := +type Pair' (A B : Type) := mkPair { fst : A; snd : B }; -mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool +mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool | mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst | x := case x of {_ := false}; diff --git a/tests/Anoma/Compilation/positive/test061.juvix b/tests/Anoma/Compilation/positive/test061.juvix index 7d741e2af..bb26cc849 100644 --- a/tests/Anoma/Compilation/positive/test061.juvix +++ b/tests/Anoma/Compilation/positive/test061.juvix @@ -60,18 +60,18 @@ f5 {A} {{T A}} (n : Nat) (a : A) : Nat := n + T.toNat a; main : Nat := trace (T.toNat true) - >>> trace (f false) - >>> trace (T.toNat 3) - >>> trace (T.toNat (g {Nat})) - >>> trace (T.toNat [true; false]) - >>> trace (T.toNat [1; 2; 3]) - >>> trace + >-> trace (f false) + >-> trace (T.toNat 3) + >-> trace (T.toNat (g {Nat})) + >-> trace (T.toNat [true; false]) + >-> trace (T.toNat [1; 2; 3]) + >-> trace (let f (_ : Unit) : Nat := 5; in T.toNat f) - >>> trace (f' [1; 2]) - >>> trace (f'' [true; false]) - >>> trace (f'3 [just true; nothing; just false]) - >>> trace (f'4 [just [1]; nothing; just [2; 3]]) - >>> trace (f'3 true) - >>> f5 1 [0; 1; 1]; + >-> trace (f' [1; 2]) + >-> trace (f'' [true; false]) + >-> trace (f'3 [just true; nothing; just false]) + >-> trace (f'4 [just [1]; nothing; just [2; 3]]) + >-> trace (f'3 true) + >-> f5 1 [0; 1; 1]; diff --git a/tests/Anoma/Compilation/positive/test063.juvix b/tests/Anoma/Compilation/positive/test063.juvix index f5cf3f49e..0672bf84f 100644 --- a/tests/Anoma/Compilation/positive/test063.juvix +++ b/tests/Anoma/Compilation/positive/test063.juvix @@ -78,10 +78,10 @@ h {A} {{U2 A}} : A -> A := f; main : Nat := trace (T1.pp 0) - >>> trace (T2.pp 1) - >>> trace (T3.pp 2) - >>> trace (T4.pp 3) - >>> trace (U.pp 4) - >>> trace (f 5) - >>> trace (g {{mkU1 id}} 6) - >>> h 7; + >-> trace (T2.pp 1) + >-> trace (T3.pp 2) + >-> trace (T4.pp 3) + >-> trace (U.pp 4) + >-> trace (f 5) + >-> trace (g {{mkU1 id}} 6) + >-> h 7; diff --git a/tests/Anoma/Compilation/positive/test069.juvix b/tests/Anoma/Compilation/positive/test069.juvix index 58dc77089..8e31e48d9 100644 --- a/tests/Anoma/Compilation/positive/test069.juvix +++ b/tests/Anoma/Compilation/positive/test069.juvix @@ -3,7 +3,7 @@ module test069; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Anoma/Compilation/positive/test071.juvix b/tests/Anoma/Compilation/positive/test071.juvix index 84f4d5100..d552c6682 100644 --- a/tests/Anoma/Compilation/positive/test071.juvix +++ b/tests/Anoma/Compilation/positive/test071.juvix @@ -3,7 +3,7 @@ module test071; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Anoma/Compilation/positive/test072/Monad.juvix b/tests/Anoma/Compilation/positive/test072/Monad.juvix index 81a4dfb96..e96aa763e 100644 --- a/tests/Anoma/Compilation/positive/test072/Monad.juvix +++ b/tests/Anoma/Compilation/positive/test072/Monad.juvix @@ -16,6 +16,6 @@ type Monad (f : Type -> Type) := open Monad public; -syntax operator >> bind; ->> {M : Type → Type} {A B : Type} {{Monad M}} (x : M +syntax operator >>> bind; +>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/Anoma/Compilation/positive/test072/Reader.juvix b/tests/Anoma/Compilation/positive/test072/Reader.juvix index 7e89040ff..8de25df4a 100644 --- a/tests/Anoma/Compilation/positive/test072/Reader.juvix +++ b/tests/Anoma/Compilation/positive/test072/Reader.juvix @@ -10,7 +10,7 @@ instance Reader-Functor {R : Type} : Functor (Reader R) := mkFunctor@{ <$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra) + | (mkReader ra) := mkReader (f << ra) }; instance diff --git a/tests/Anoma/Compilation/positive/test072/ReaderT.juvix b/tests/Anoma/Compilation/positive/test072/ReaderT.juvix index 95d4d7d3d..c9e7ee662 100644 --- a/tests/Anoma/Compilation/positive/test072/ReaderT.juvix +++ b/tests/Anoma/Compilation/positive/test072/ReaderT.juvix @@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} monad := ReaderT-Monad; ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s}; reader {A : Type} (f : S → A) : ReaderT S M A := - mkReaderT (MMonad.return ∘ f) + mkReaderT (MMonad.return << f) }; import MonadState open; import StateT open; import Identity open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; liftReaderT {R A : Type} {M : Type → Type} (m : M A) : ReaderT R M A := mkReaderT (const m); @@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := monadic : ReaderT Nat (StateT Nat Identity) Nat := askNat >>= λ {n := - liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + liftReaderT (modify λ {m := m * n}) >>> liftReaderT get}; main : Nat := runIdentity (evalState 2 (runReader 5 monadic)); @@ -87,6 +87,6 @@ main : Nat := -- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) := -- mkMonadReader@{ -- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}}; --- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader; +-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader; -- ask : StateT S M R := liftStateT MonadReader.ask; -- }; diff --git a/tests/Anoma/Compilation/positive/test072/State.juvix b/tests/Anoma/Compilation/positive/test072/State.juvix index 2e7fadc12..df7e8d486 100644 --- a/tests/Anoma/Compilation/positive/test072/State.juvix +++ b/tests/Anoma/Compilation/positive/test072/State.juvix @@ -2,7 +2,7 @@ module State; import Monad open; import Functor open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type State (S A : Type) := mkState {runState : S -> A × S}; diff --git a/tests/Anoma/Compilation/positive/test072/StateT.juvix b/tests/Anoma/Compilation/positive/test072/StateT.juvix index f804233f3..3ea027ccf 100644 --- a/tests/Anoma/Compilation/positive/test072/StateT.juvix +++ b/tests/Anoma/Compilation/positive/test072/StateT.juvix @@ -4,15 +4,15 @@ import Monad open; import Monad open using {module Monad as MMonad}; import Functor open; import Functor open using {module Functor as MFunctor}; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type StateT (S : Type) (M : Type → Type) (A : Type) := - mkStateT {runStateT : S → M (A × S)}; + mkStateT {runStateT : S → M (Pair A S)}; runState {S A : Type} {M : Type → Type} (s : S) (m : StateT S M - A) : M (A × S) := StateT.runStateT m s; + A) : M (Pair A S) := StateT.runStateT m s; evalState {S A : Type} {M : Type → Type} {{Functor M}} (s : S) (m : StateT S M A) : M A := diff --git a/tests/Anoma/Compilation/positive/test074.juvix b/tests/Anoma/Compilation/positive/test074.juvix index a70294efe..7ce14271e 100644 --- a/tests/Anoma/Compilation/positive/test074.juvix +++ b/tests/Anoma/Compilation/positive/test074.juvix @@ -7,4 +7,4 @@ builtin anoma-get axiom anomaGet : {Value Key : Type} -> Key -> Value; main (k1 : Nat) (k2 : List Nat) : List Nat := - trace (anomaGet {Nat} k1) >>> anomaGet k2; + trace (anomaGet {Nat} k1) >-> anomaGet k2; diff --git a/tests/Anoma/Compilation/positive/test075.juvix b/tests/Anoma/Compilation/positive/test075.juvix index cfad65e7b..2e95bf972 100644 --- a/tests/Anoma/Compilation/positive/test075.juvix +++ b/tests/Anoma/Compilation/positive/test075.juvix @@ -10,8 +10,8 @@ main : Nat := -- jam 0 == 2 trace (anomaEncode 0) -- jam [1 2 0] == 84081 - >>> trace (anomaEncode [1;2]) + >-> trace (anomaEncode [1;2]) -- jam [1 2] == 4657 - >>> trace (anomaEncode (1 , 2)) + >-> trace (anomaEncode (1 , 2)) -- jam 1 == 12 - >>> anomaEncode false; + >-> anomaEncode false; diff --git a/tests/Anoma/Compilation/positive/test076.juvix b/tests/Anoma/Compilation/positive/test076.juvix index cb3c7bf5f..a7bede845 100644 --- a/tests/Anoma/Compilation/positive/test076.juvix +++ b/tests/Anoma/Compilation/positive/test076.juvix @@ -10,8 +10,8 @@ main : Bool := -- cue 2 == 0 trace (anomaDecode {Nat} 2) -- cue 84081 == [1 2 0] - >>> trace (anomaDecode {List Nat} 84081) + >-> trace (anomaDecode {List Nat} 84081) -- cue 4657 == [1 2] - >>> trace (anomaDecode {Nat × Nat} 4657) + >-> trace (anomaDecode {Pair Nat Nat} 4657) -- cue 12 == 1 - >>> anomaDecode {Bool} 12; + >-> anomaDecode {Bool} 12; diff --git a/tests/Casm/Compilation/positive/test030.juvix b/tests/Casm/Compilation/positive/test030.juvix index b5434b9b2..0f5f54db4 100644 --- a/tests/Casm/Compilation/positive/test030.juvix +++ b/tests/Casm/Compilation/positive/test030.juvix @@ -7,7 +7,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A -- clauses with differing number of patterns not yet supported -- iterate f zero x := x; | f zero := id - | f (suc n) := f ∘ iterate f n; + | f (suc n) := f << iterate f n; plus : Nat → Nat → Nat := iterate suc; diff --git a/tests/Casm/Compilation/positive/test032.juvix b/tests/Casm/Compilation/positive/test032.juvix index eb6fe5259..b6932d7ac 100644 --- a/tests/Casm/Compilation/positive/test032.juvix +++ b/tests/Casm/Compilation/positive/test032.juvix @@ -3,7 +3,7 @@ module test032; import Stdlib.Prelude open; -split : {A : Type} → Nat → List A → List A × List A +split : {A : Type} → Nat → List A → Pair (List A) (List A) | zero xs := nil, xs | (suc n) nil := nil, nil | (suc n) (x :: xs) := @@ -46,7 +46,7 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat) printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; sum : List Nat → Nat | nil := 0 diff --git a/tests/Casm/Compilation/positive/test033.juvix b/tests/Casm/Compilation/positive/test033.juvix index e2be0043f..27ce2e8d8 100644 --- a/tests/Casm/Compilation/positive/test033.juvix +++ b/tests/Casm/Compilation/positive/test033.juvix @@ -9,19 +9,19 @@ f : (Nat → Nat) → Nat f' : Nat → Nat | x := f ((+) x); -g : (Nat → Nat × Nat) → Nat × Nat +g : (Nat → Pair Nat Nat) → Pair Nat Nat | f := f 2; -g' : Nat → Nat × Nat +g' : Nat → Pair Nat Nat | x := g ((,) x); f1' : Nat → Nat → Nat | x y := f ((+) (div x y)); -g1' : Nat → Nat → Nat × Nat +g1' : Nat → Nat → Pair Nat Nat | x y := g ((,) (div x y)); -h : (Nat → Nat → Nat × Nat) → Nat × Nat +h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat | f := f 1 2; main : Nat := diff --git a/tests/Casm/Compilation/positive/test035.juvix b/tests/Casm/Compilation/positive/test035.juvix index 75a9d3ffe..9386150d3 100644 --- a/tests/Casm/Compilation/positive/test035.juvix +++ b/tests/Casm/Compilation/positive/test035.juvix @@ -44,7 +44,7 @@ h : Nat -> Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; main : Nat := head 0 (sum2 (lgen 5)) diff --git a/tests/Casm/Compilation/positive/test036.juvix b/tests/Casm/Compilation/positive/test036.juvix index 540f26bed..5af459d39 100644 --- a/tests/Casm/Compilation/positive/test036.juvix +++ b/tests/Casm/Compilation/positive/test036.juvix @@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A f : Nat → Nat := suc; g : Nat → Nat → Nat - | z := f ∘ flip sub z; + | z := f << flip sub z; g' : Nat → Nat → Nat - | z := f ∘ λ {x := sub x z}; + | z := f << λ {x := sub x z}; -h : Nat → Nat := f ∘ g 3; +h : Nat → Nat := f << g 3; j : Nat → Nat → Nat := g'; diff --git a/tests/Casm/Compilation/positive/test054.juvix b/tests/Casm/Compilation/positive/test054.juvix index aae917428..2b1a49c55 100644 --- a/tests/Casm/Compilation/positive/test054.juvix +++ b/tests/Casm/Compilation/positive/test054.juvix @@ -36,12 +36,12 @@ myfor2 syntax iterator myzip2 {init := 2; range := 2}; myzip2 : {A A' B C : Type} - → (A → A' → B → C → A × A') + → (A → A' → B → C → Pair A A') → A → A' → List B → List C - → A × A' + → Pair A A' | f a b xs ys := myfor (acc, acc' := a, b) (x, y in zip xs ys) f acc acc' x y; diff --git a/tests/Casm/Compilation/positive/test060.juvix b/tests/Casm/Compilation/positive/test060.juvix index 6e306a394..7e352001f 100644 --- a/tests/Casm/Compilation/positive/test060.juvix +++ b/tests/Casm/Compilation/positive/test060.juvix @@ -10,7 +10,7 @@ type Triple (A B C : Type) := thd : C }; -type Pair (A B : Type) := +type Pair' (A B : Type) := mkPair { fst : A; snd : B @@ -19,7 +19,7 @@ type Pair (A B : Type) := sum : Triple Nat Nat Nat → Nat | mkTriple@{fst; snd; thd} := fst + snd + thd; -mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool +mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool | mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst | x := case x of {_ := false}; @@ -34,7 +34,7 @@ main : Nat := }; f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10}); - in sum $ if + in sum <| if (mf mkPair@{ fst := mkPair true nil; diff --git a/tests/Casm/Compilation/positive/test069.juvix b/tests/Casm/Compilation/positive/test069.juvix index ac9dda3ab..0484d600d 100644 --- a/tests/Casm/Compilation/positive/test069.juvix +++ b/tests/Casm/Compilation/positive/test069.juvix @@ -3,7 +3,7 @@ module test069; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Casm/Compilation/positive/test071.juvix b/tests/Casm/Compilation/positive/test071.juvix index 84f4d5100..d552c6682 100644 --- a/tests/Casm/Compilation/positive/test071.juvix +++ b/tests/Casm/Compilation/positive/test071.juvix @@ -3,7 +3,7 @@ module test071; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Casm/Compilation/positive/test072/Monad.juvix b/tests/Casm/Compilation/positive/test072/Monad.juvix index 81a4dfb96..e96aa763e 100644 --- a/tests/Casm/Compilation/positive/test072/Monad.juvix +++ b/tests/Casm/Compilation/positive/test072/Monad.juvix @@ -16,6 +16,6 @@ type Monad (f : Type -> Type) := open Monad public; -syntax operator >> bind; ->> {M : Type → Type} {A B : Type} {{Monad M}} (x : M +syntax operator >>> bind; +>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/Casm/Compilation/positive/test072/Reader.juvix b/tests/Casm/Compilation/positive/test072/Reader.juvix index 7e89040ff..8de25df4a 100644 --- a/tests/Casm/Compilation/positive/test072/Reader.juvix +++ b/tests/Casm/Compilation/positive/test072/Reader.juvix @@ -10,7 +10,7 @@ instance Reader-Functor {R : Type} : Functor (Reader R) := mkFunctor@{ <$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra) + | (mkReader ra) := mkReader (f << ra) }; instance diff --git a/tests/Casm/Compilation/positive/test072/ReaderT.juvix b/tests/Casm/Compilation/positive/test072/ReaderT.juvix index 95d4d7d3d..c9e7ee662 100644 --- a/tests/Casm/Compilation/positive/test072/ReaderT.juvix +++ b/tests/Casm/Compilation/positive/test072/ReaderT.juvix @@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} monad := ReaderT-Monad; ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s}; reader {A : Type} (f : S → A) : ReaderT S M A := - mkReaderT (MMonad.return ∘ f) + mkReaderT (MMonad.return << f) }; import MonadState open; import StateT open; import Identity open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; liftReaderT {R A : Type} {M : Type → Type} (m : M A) : ReaderT R M A := mkReaderT (const m); @@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := monadic : ReaderT Nat (StateT Nat Identity) Nat := askNat >>= λ {n := - liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + liftReaderT (modify λ {m := m * n}) >>> liftReaderT get}; main : Nat := runIdentity (evalState 2 (runReader 5 monadic)); @@ -87,6 +87,6 @@ main : Nat := -- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) := -- mkMonadReader@{ -- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}}; --- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader; +-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader; -- ask : StateT S M R := liftStateT MonadReader.ask; -- }; diff --git a/tests/Casm/Compilation/positive/test072/State.juvix b/tests/Casm/Compilation/positive/test072/State.juvix index 2e7fadc12..df7e8d486 100644 --- a/tests/Casm/Compilation/positive/test072/State.juvix +++ b/tests/Casm/Compilation/positive/test072/State.juvix @@ -2,7 +2,7 @@ module State; import Monad open; import Functor open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type State (S A : Type) := mkState {runState : S -> A × S}; diff --git a/tests/Casm/Compilation/positive/test072/StateT.juvix b/tests/Casm/Compilation/positive/test072/StateT.juvix index f804233f3..3ea027ccf 100644 --- a/tests/Casm/Compilation/positive/test072/StateT.juvix +++ b/tests/Casm/Compilation/positive/test072/StateT.juvix @@ -4,15 +4,15 @@ import Monad open; import Monad open using {module Monad as MMonad}; import Functor open; import Functor open using {module Functor as MFunctor}; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type StateT (S : Type) (M : Type → Type) (A : Type) := - mkStateT {runStateT : S → M (A × S)}; + mkStateT {runStateT : S → M (Pair A S)}; runState {S A : Type} {M : Type → Type} (s : S) (m : StateT S M - A) : M (A × S) := StateT.runStateT m s; + A) : M (Pair A S) := StateT.runStateT m s; evalState {S A : Type} {M : Type → Type} {{Functor M}} (s : S) (m : StateT S M A) : M A := diff --git a/tests/Casm/Compilation/positive/test077.juvix b/tests/Casm/Compilation/positive/test077.juvix index 448fdde0f..0e29998d9 100644 --- a/tests/Casm/Compilation/positive/test077.juvix +++ b/tests/Casm/Compilation/positive/test077.juvix @@ -23,13 +23,13 @@ type ComplianceResult := y : Field }; -count : List (Field × Bool) -> Field +count : List (Pair Field Bool) -> Field | [] := 0 | ((h, b) :: t) := if b (h + count t) (count t); main (input : Resource) - (path : List (Field × Bool)) + (path : List (Pair Field Bool)) : ComplianceResult := mkResult@{ cnt := count path; @@ -44,7 +44,7 @@ main {- main (input : Resource) - (path : List (Field × Bool)) + (path : List (Pair Field Bool)) : Field := count path; -} diff --git a/tests/Compilation/positive/test003.juvix b/tests/Compilation/positive/test003.juvix index fbf6be4cc..015fc6aa6 100644 --- a/tests/Compilation/positive/test003.juvix +++ b/tests/Compilation/positive/test003.juvix @@ -13,7 +13,7 @@ import Stdlib.Prelude open; main : IO := printNatLn (mod 3 2) - >> printNatLn (div 18 4) - >> printNatLn (mod 18 4) - >> printNatLn (div 16 4) - >> printNatLn (mod 16 4); + >>> printNatLn (div 18 4) + >>> printNatLn (mod 18 4) + >>> printNatLn (div 16 4) + >>> printNatLn (mod 16 4); diff --git a/tests/Compilation/positive/test004.juvix b/tests/Compilation/positive/test004.juvix index a95f83e6d..e6fd83d1e 100644 --- a/tests/Compilation/positive/test004.juvix +++ b/tests/Compilation/positive/test004.juvix @@ -5,8 +5,8 @@ import Stdlib.Prelude open; main : IO := printNat 1 - >> printNat 2 - >> printNat 3 - >> printNat 4 - >> printNat 5 - >> printString "\n"; + >>> printNat 2 + >>> printNat 3 + >>> printNat 4 + >>> printNat 5 + >>> printString "\n"; diff --git a/tests/Compilation/positive/test006.juvix b/tests/Compilation/positive/test006.juvix index 0aa53d89d..1e81893a2 100644 --- a/tests/Compilation/positive/test006.juvix +++ b/tests/Compilation/positive/test006.juvix @@ -9,5 +9,5 @@ loop : Nat := loop; main : IO := printNatLn (if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1)) - >> printBoolLn (2 > 0 || loop == 0) - >> printBoolLn (2 < 0 && loop == 0); + >>> printBoolLn (2 > 0 || loop == 0) + >>> printBoolLn (2 < 0 && loop == 0); diff --git a/tests/Compilation/positive/test007.juvix b/tests/Compilation/positive/test007.juvix index 7caf74433..2f222eb07 100644 --- a/tests/Compilation/positive/test007.juvix +++ b/tests/Compilation/positive/test007.juvix @@ -18,17 +18,17 @@ lst : List Nat := 0 :: 1 :: nil; printNatList : List Nat → IO | nil := printString "nil" | (h :: t) := - printNat h >> printString " :: " >> printNatList t; + printNat h >>> printString " :: " >>> printNatList t; printNatListLn (lst : List Nat) : IO := - printNatList lst >> printString "\n"; + printNatList lst >>> printString "\n"; main : IO := printBoolLn (null lst) - >> printBoolLn (null (nil {Nat})) - >> printNatLn (head 1 lst) - >> printNatListLn (tail lst) - >> printNatLn (head 0 (tail lst)) - >> printNatListLn (map ((+) 1) lst) - >> printNatListLn (map' ((+) 1) lst) - >> printNatListLn (runPartial (λ{{{_}} := map'' ((+) 1) lst})); + >>> printBoolLn (null (nil {Nat})) + >>> printNatLn (head 1 lst) + >>> printNatListLn (tail lst) + >>> printNatLn (head 0 (tail lst)) + >>> printNatListLn (map ((+) 1) lst) + >>> printNatListLn (map' ((+) 1) lst) + >>> printNatListLn (runPartial (λ{{{_}} := map'' ((+) 1) lst})); diff --git a/tests/Compilation/positive/test009.juvix b/tests/Compilation/positive/test009.juvix index 139ebd00a..76f32d512 100644 --- a/tests/Compilation/positive/test009.juvix +++ b/tests/Compilation/positive/test009.juvix @@ -17,6 +17,6 @@ fact : Nat → Nat := fact' 1; main : IO := printNatLn (sum 10000) - >> printNatLn (fact 5) - >> printNatLn (fact 10) - >> printNatLn (fact 12); + >>> printNatLn (fact 5) + >>> printNatLn (fact 10) + >>> printNatLn (fact 12); diff --git a/tests/Compilation/positive/test011.juvix b/tests/Compilation/positive/test011.juvix index e1d098605..160d01b65 100644 --- a/tests/Compilation/positive/test011.juvix +++ b/tests/Compilation/positive/test011.juvix @@ -11,5 +11,5 @@ fib : Nat → Nat := fib' 0 1; main : IO := printNatLn (fib 10) - >> printNatLn (fib 100) - >> printNatLn (fib 1000); + >>> printNatLn (fib 100) + >>> printNatLn (fib 1000); diff --git a/tests/Compilation/positive/test012.juvix b/tests/Compilation/positive/test012.juvix index 2d00b616c..529cfe7b6 100644 --- a/tests/Compilation/positive/test012.juvix +++ b/tests/Compilation/positive/test012.juvix @@ -20,19 +20,19 @@ gen : Nat → Tree preorder : Tree → IO | leaf := printNat 0 - | (node1 c) := printNat 1 >> preorder c - | (node2 l r) := printNat 2 >> preorder l >> preorder r + | (node1 c) := printNat 1 >>> preorder c + | (node2 l r) := printNat 2 >>> preorder l >>> preorder r | (node3 l m r) := - printNat 3 >> preorder l >> preorder m >> preorder r; + printNat 3 >>> preorder l >>> preorder m >>> preorder r; main : IO := preorder (gen 3) - >> printString "\n" - >> preorder (gen 4) - >> printString "\n" - >> preorder (gen 5) - >> printString "\n" - >> preorder (gen 6) - >> printString "\n" - >> preorder (gen 7) - >> printString "\n"; + >>> printString "\n" + >>> preorder (gen 4) + >>> printString "\n" + >>> preorder (gen 5) + >>> printString "\n" + >>> preorder (gen 6) + >>> printString "\n" + >>> preorder (gen 7) + >>> printString "\n"; diff --git a/tests/Compilation/positive/test013.juvix b/tests/Compilation/positive/test013.juvix index 97a7fa90e..5c3f7fe73 100644 --- a/tests/Compilation/positive/test013.juvix +++ b/tests/Compilation/positive/test013.juvix @@ -15,6 +15,6 @@ f : Nat → Nat → Nat main : IO := printNatLn (f 5 6) - >> printNatLn (f 6 5) - >> printNatLn (f 10 5) - >> printNatLn (f 11 5); + >>> printNatLn (f 6 5) + >>> printNatLn (f 10 5) + >>> printNatLn (f 11 5); diff --git a/tests/Compilation/positive/test014.juvix b/tests/Compilation/positive/test014.juvix index e20d99f22..4c3b04c5c 100644 --- a/tests/Compilation/positive/test014.juvix +++ b/tests/Compilation/positive/test014.juvix @@ -23,13 +23,13 @@ vy : Nat := 7; main : IO := printNatLn (func (div y x)) - >> -- 17 div 5 + 4 = 7 + >>> -- 17 div 5 + 4 = 7 printNatLn (y + x * z) - >> -- 17 + >>> -- 17 printNatLn (vx + vy * (z + 1)) - >> -- 37 + >>> -- 37 f (h g 2 3) 4; diff --git a/tests/Compilation/positive/test015.juvix b/tests/Compilation/positive/test015.juvix index eb6efcd27..adac4cdc9 100644 --- a/tests/Compilation/positive/test015.juvix +++ b/tests/Compilation/positive/test015.juvix @@ -21,18 +21,18 @@ h : Nat → Nat main : IO := printNatLn (f 100 500) - >> -- 600 + >>> -- 600 printNatLn (f 5 0) - >> -- 25 + >>> -- 25 printNatLn (f 5 5) - >> -- 30 + >>> -- 30 printNatLn (h 10) - >> -- 45 + >>> -- 45 printNatLn (g 10 h) - >> -- 55 + >>> -- 55 printNatLn (g 3 (f 10)); diff --git a/tests/Compilation/positive/test020.juvix b/tests/Compilation/positive/test020.juvix index 339977e2a..32243daca 100644 --- a/tests/Compilation/positive/test020.juvix +++ b/tests/Compilation/positive/test020.juvix @@ -15,11 +15,11 @@ subp : Nat → Nat → Nat main : IO := printNatLn (f91 101) - >> printNatLn (f91 95) - >> printNatLn (f91 16) - >> printNatLn (f91 5) - >> printNatLn (subp 101 1) - >> printNatLn (subp 11 5) - >> printNatLn (subp 10 4) - >> printNatLn (subp 1000 600) - >> printNatLn (subp 10000 6000); + >>> printNatLn (f91 95) + >>> printNatLn (f91 16) + >>> printNatLn (f91 5) + >>> printNatLn (subp 101 1) + >>> printNatLn (subp 11 5) + >>> printNatLn (subp 10 4) + >>> printNatLn (subp 1000 600) + >>> printNatLn (subp 10000 6000); diff --git a/tests/Compilation/positive/test021.juvix b/tests/Compilation/positive/test021.juvix index f99c34873..59ecd7d6f 100644 --- a/tests/Compilation/positive/test021.juvix +++ b/tests/Compilation/positive/test021.juvix @@ -15,5 +15,5 @@ power : Nat → Nat → Nat := power' 1; main : IO := printNatLn (power 2 3) - >> printNatLn (power 3 7) - >> printNatLn (power 5 11); + >>> printNatLn (power 3 7) + >>> printNatLn (power 5 11); diff --git a/tests/Compilation/positive/test022.juvix b/tests/Compilation/positive/test022.juvix index a2f69854f..209802296 100644 --- a/tests/Compilation/positive/test022.juvix +++ b/tests/Compilation/positive/test022.juvix @@ -16,13 +16,13 @@ sum' : Nat → Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (h :: t) := - printNat h >> printString " :: " >> printListNatLn t; + printNat h >>> printString " :: " >>> printListNatLn t; main : IO := printListNatLn (gen 10) - >> printListNatLn (reverse (gen 10)) - >> printListNatLn (filter ((<) 5) (gen 10)) - >> printListNatLn (reverse (map (flip sub 1) (gen 10))) - >> printNatLn (sum 10000) - >> printNatLn (sum' 10000); + >>> printListNatLn (reverse (gen 10)) + >>> printListNatLn (filter ((<) 5) (gen 10)) + >>> printListNatLn (reverse (map (flip sub 1) (gen 10))) + >>> printNatLn (sum 10000) + >>> printNatLn (sum' 10000); diff --git a/tests/Compilation/positive/test023.juvix b/tests/Compilation/positive/test023.juvix index 63a6ba24f..2a0946bfe 100644 --- a/tests/Compilation/positive/test023.juvix +++ b/tests/Compilation/positive/test023.juvix @@ -18,6 +18,6 @@ h : Nat → Nat main : IO := printNatLn (f 5) - >> printNatLn (f 10) - >> printNatLn (f 20); + >>> printNatLn (f 10) + >>> printNatLn (f 20); diff --git a/tests/Compilation/positive/test025.juvix b/tests/Compilation/positive/test025.juvix index d8adaa989..0176bc860 100644 --- a/tests/Compilation/positive/test025.juvix +++ b/tests/Compilation/positive/test025.juvix @@ -13,8 +13,8 @@ gcd : Nat → Nat → Nat main : IO := printNatLn (gcd (3 * 7 * 2) (7 * 2 * 11)) - >> printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5)) - >> printNatLn (gcd 3 7) - >> printNatLn (gcd 7 3) - >> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13)); + >>> printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5)) + >>> printNatLn (gcd 3 7) + >>> printNatLn (gcd 7 3) + >>> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13)); diff --git a/tests/Compilation/positive/test026.juvix b/tests/Compilation/positive/test026.juvix index 4be4c2510..6b254281d 100644 --- a/tests/Compilation/positive/test026.juvix +++ b/tests/Compilation/positive/test026.juvix @@ -52,7 +52,7 @@ f {{Partial}} : Nat → Queue Nat → List Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (h :: t) := - printNat h >> printString " :: " >> printListNatLn t; + printNat h >>> printString " :: " >>> printListNatLn t; main : IO := printListNatLn (runPartial λ {{{_}} := f 100 empty}); diff --git a/tests/Compilation/positive/test027.juvix b/tests/Compilation/positive/test027.juvix index e5bda901d..011f94af0 100644 --- a/tests/Compilation/positive/test027.juvix +++ b/tests/Compilation/positive/test027.juvix @@ -9,17 +9,17 @@ czero : Num | {_} f x := x; csuc : Num → Num - | n {_} f := f ∘ n {_} f; + | n {_} f := f << n {_} f; num : Nat → Num | zero := czero | (suc n) := csuc (num n); add : Num → Num → Num - | n m {_} f := n {_} f ∘ m {_} f; + | n m {_} f := n {_} f << m {_} f; mul : Num → Num → Num - | n m {_} := n {_} ∘ m {_}; + | n m {_} := n {_} << m {_}; isZero : Num → Bool | n := n {_} (const false) true; @@ -29,5 +29,5 @@ toNat : Num → Nat main : IO := printNatLn (toNat (num 7)) - >> printNatLn (toNat (add (num 7) (num 3))) - >> printNatLn (toNat (mul (num 7) (num 3))); + >>> printNatLn (toNat (add (num 7) (num 3))) + >>> printNatLn (toNat (mul (num 7) (num 3))); diff --git a/tests/Compilation/positive/test028.juvix b/tests/Compilation/positive/test028.juvix index 438e38d7d..64adbfcff 100644 --- a/tests/Compilation/positive/test028.juvix +++ b/tests/Compilation/positive/test028.juvix @@ -43,6 +43,6 @@ primes : Unit → Stream := eratostenes (numbers 2); main : IO := printNatLn (snth 10 primes) - >> printNatLn (snth 50 primes) - >> printNatLn (snth 100 primes) - >> printNatLn (snth 200 primes); + >>> printNatLn (snth 50 primes) + >>> printNatLn (snth 100 primes) + >>> printNatLn (snth 200 primes); diff --git a/tests/Compilation/positive/test029.juvix b/tests/Compilation/positive/test029.juvix index 2ff65fe36..bbd4eb5eb 100644 --- a/tests/Compilation/positive/test029.juvix +++ b/tests/Compilation/positive/test029.juvix @@ -10,8 +10,8 @@ ack : Nat → Nat → Nat main : IO := printNatLn (ack 0 7) - >> printNatLn (ack 1 7) - >> printNatLn (ack 1 13) - >> printNatLn (ack 2 7) - >> printNatLn (ack 2 13) - >> printNatLn (ack 3 7); + >>> printNatLn (ack 1 7) + >>> printNatLn (ack 1 13) + >>> printNatLn (ack 2 7) + >>> printNatLn (ack 2 13) + >>> printNatLn (ack 3 7); diff --git a/tests/Compilation/positive/test030.juvix b/tests/Compilation/positive/test030.juvix index 8db307a63..06d31084b 100644 --- a/tests/Compilation/positive/test030.juvix +++ b/tests/Compilation/positive/test030.juvix @@ -7,7 +7,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A -- clauses with differing number of patterns not yet supported -- iterate f zero x := x; | f zero := id - | f (suc n) := f ∘ iterate f n; + | f (suc n) := f << iterate f n; plus : Nat → Nat → Nat := iterate suc; @@ -22,7 +22,7 @@ ackermann : Nat → Nat → Nat main : IO := printNatLn (plus 3 7) - >> printNatLn (mult 3 7) - >> printNatLn (exp 3 7) - >> printNatLn (ackermann 3 7); + >>> printNatLn (mult 3 7) + >>> printNatLn (exp 3 7) + >>> printNatLn (ackermann 3 7); diff --git a/tests/Compilation/positive/test031.juvix b/tests/Compilation/positive/test031.juvix index 8718f7ef7..7240e76a6 100644 --- a/tests/Compilation/positive/test031.juvix +++ b/tests/Compilation/positive/test031.juvix @@ -14,6 +14,6 @@ mklst2 : Nat → List (List Nat) printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; main : IO := printListNatLn (flatten (mklst2 4)); diff --git a/tests/Compilation/positive/test032.juvix b/tests/Compilation/positive/test032.juvix index 5a7e12b3f..155be3211 100644 --- a/tests/Compilation/positive/test032.juvix +++ b/tests/Compilation/positive/test032.juvix @@ -3,7 +3,7 @@ module test032; import Stdlib.Prelude open; -split : {A : Type} → Nat → List A → List A × List A +split : {A : Type} → Nat → List A → Pair (List A) (List A) | zero xs := nil, xs | (suc n) nil := nil, nil | (suc n) (x :: xs) := @@ -46,12 +46,12 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat) printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; main : IO := printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 40))))) - >> printListNatLn + >>> printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 9 80))))) - >> printListNatLn + >>> printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 80))))); diff --git a/tests/Compilation/positive/test033.juvix b/tests/Compilation/positive/test033.juvix index 391dc1c60..24792b4b5 100644 --- a/tests/Compilation/positive/test033.juvix +++ b/tests/Compilation/positive/test033.juvix @@ -9,33 +9,32 @@ f : (Nat → Nat) → Nat f' : Nat → Nat | x := f ((+) x); -g : (Nat → Nat × Nat) → Nat × Nat +g : (Nat → Pair Nat Nat) → Pair Nat Nat | f := f 2; -g' : Nat → Nat × Nat +g' : Nat → Pair Nat Nat | x := g ((,) x); f1' : Nat → Nat → Nat | x y := f ((+) (div x y)); -g1' : Nat → Nat → Nat × Nat +g1' : Nat → Nat → Pair Nat Nat | x y := g ((,) (div x y)); -h : (Nat → Nat → Nat × Nat) → Nat × Nat +h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat | f := f 1 2; -printPairNatLn : Nat × Nat → IO +printPairNatLn : Pair Nat Nat → IO | (x, y) := printString "(" - >> printNat x - >> printString ", " - >> printNat y - >> printStringLn ")"; + >>> printNat x + >>> printString ", " + >>> printNat y + >>> printStringLn ")"; main : IO := printNatLn (f' 7) - >> printPairNatLn (g' 7) - >> printNatLn (f1' 7 2) - >> printPairNatLn (g1' 7 2) - >> printPairNatLn (h (,)); - + >>> printPairNatLn (g' 7) + >>> printNatLn (f1' 7 2) + >>> printPairNatLn (g1' 7 2) + >>> printPairNatLn (h (,)); diff --git a/tests/Compilation/positive/test034.juvix b/tests/Compilation/positive/test034.juvix index 6658f44e2..c5fe93a86 100644 --- a/tests/Compilation/positive/test034.juvix +++ b/tests/Compilation/positive/test034.juvix @@ -21,8 +21,8 @@ mutrec : IO := terminating h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1)); in printNatLn (f 5) - >> printNatLn (f 10) - >> printNatLn (g 5) - >> printNatLn (h 5); + >>> printNatLn (f 10) + >>> printNatLn (g 5) + >>> printNatLn (h 5); -main : IO := printNatLn (sum 10000) >> mutrec; +main : IO := printNatLn (sum 10000) >>> mutrec; diff --git a/tests/Compilation/positive/test035.juvix b/tests/Compilation/positive/test035.juvix index 6796b5725..2d168a1c0 100644 --- a/tests/Compilation/positive/test035.juvix +++ b/tests/Compilation/positive/test035.juvix @@ -43,16 +43,16 @@ h : Nat -> Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; main : IO := printListNatLn (sum2 (lgen 5)) - >> printNatLn (f (gen 10)) - >> printNatLn (f (gen 15)) - >> printNatLn (f (gen 16)) - >> printNatLn (f (gen 17)) - >> printNatLn (f (gen 18)) - >> printNatLn (f (gen 20)) - >> printNatLn (h 5) - >> printNatLn (h 3); + >>> printNatLn (f (gen 10)) + >>> printNatLn (f (gen 15)) + >>> printNatLn (f (gen 16)) + >>> printNatLn (f (gen 17)) + >>> printNatLn (f (gen 18)) + >>> printNatLn (f (gen 20)) + >>> printNatLn (h 5) + >>> printNatLn (h 3); diff --git a/tests/Compilation/positive/test036.juvix b/tests/Compilation/positive/test036.juvix index 14ea641d9..68e57d7a0 100644 --- a/tests/Compilation/positive/test036.juvix +++ b/tests/Compilation/positive/test036.juvix @@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A f : Nat → Nat := suc; g : Nat → Nat → Nat - | z := f ∘ flip sub z; + | z := f << flip sub z; g' : Nat → Nat → Nat - | z := f ∘ λ {x := sub x z}; + | z := f << λ {x := sub x z}; -h : Nat → Nat := f ∘ g 3; +h : Nat → Nat := f << g 3; j : Nat → Nat → Nat := g'; diff --git a/tests/Compilation/positive/test039.juvix b/tests/Compilation/positive/test039.juvix index e3b49a366..3799b5394 100644 --- a/tests/Compilation/positive/test039.juvix +++ b/tests/Compilation/positive/test039.juvix @@ -15,4 +15,4 @@ main : IO := | (suc n) := not (odd n); plusOne (n : Ty) : Ty := n + 1; in printBoolLn (odd (plusOne 13)) - >> printBoolLn (even (plusOne 12)); + >>> printBoolLn (even (plusOne 12)); diff --git a/tests/Compilation/positive/test049.juvix b/tests/Compilation/positive/test049.juvix index bb81bf4c5..dae19d4e0 100644 --- a/tests/Compilation/positive/test049.juvix +++ b/tests/Compilation/positive/test049.juvix @@ -9,39 +9,39 @@ f : Int -> Nat main : IO := printStringLn (intToString 1) - >> printStringLn (intToString -1) - >> printIntLn (ofNat 1) - >> printIntLn (negSuc 0) - >> printIntLn (ofNat (suc zero)) - >> printIntLn (negSuc zero) - >> printStringLn (natToString (f 1)) - >> printNatLn (f -1) - >> printNatLn (f (ofNat (suc zero))) - >> printNatLn (f (negSuc (suc zero))) - >> printBoolLn (-1 == -2) - >> printBoolLn (-1 == -1) - >> printBoolLn (1 == 1) - >> printBoolLn (-1 == 1) - >> printIntLn (-1 + 1) - >> printIntLn (negNat (suc zero)) - >> printIntLn + >>> printStringLn (intToString -1) + >>> printIntLn (ofNat 1) + >>> printIntLn (negSuc 0) + >>> printIntLn (ofNat (suc zero)) + >>> printIntLn (negSuc zero) + >>> printStringLn (natToString (f 1)) + >>> printNatLn (f -1) + >>> printNatLn (f (ofNat (suc zero))) + >>> printNatLn (f (negSuc (suc zero))) + >>> printBoolLn (-1 == -2) + >>> printBoolLn (-1 == -1) + >>> printBoolLn (1 == 1) + >>> printBoolLn (-1 == 1) + >>> printIntLn (-1 + 1) + >>> printIntLn (negNat (suc zero)) + >>> printIntLn (let g : Nat -> Int := negNat; in g (suc zero)) - >> printIntLn (neg -1) - >> printIntLn + >>> printIntLn (neg -1) + >>> printIntLn (let g : Int -> Int := neg; in g -1) - >> printIntLn (-2 * 2) - >> printIntLn (div 4 -2) - >> printIntLn (2 - 2) - >> printBoolLn (nonNeg 0) - >> printBoolLn (nonNeg -1) - >> printIntLn (mod -5 -2) - >> printBoolLn (0 < 0) - >> printBoolLn (0 <= 0) - >> printBoolLn (0 < 1) - >> printBoolLn (1 <= 0) - >> printIntLn (mod 5 -3) - >> printIntLn (div 5 -3); + >>> printIntLn (-2 * 2) + >>> printIntLn (div 4 -2) + >>> printIntLn (2 - 2) + >>> printBoolLn (nonNeg 0) + >>> printBoolLn (nonNeg -1) + >>> printIntLn (mod -5 -2) + >>> printBoolLn (0 < 0) + >>> printBoolLn (0 <= 0) + >>> printBoolLn (0 < 1) + >>> printBoolLn (1 <= 0) + >>> printIntLn (mod 5 -3) + >>> printIntLn (div 5 -3); diff --git a/tests/Compilation/positive/test051.juvix b/tests/Compilation/positive/test051.juvix index d7bf153fe..e55e75b4a 100644 --- a/tests/Compilation/positive/test051.juvix +++ b/tests/Compilation/positive/test051.juvix @@ -1,4 +1,4 @@ --- local recursive function using IO >> +-- local recursive function using IO >>> module test051; import Stdlib.Prelude open; @@ -7,5 +7,5 @@ main : IO := let f : Nat -> IO | zero := printStringLn "" - | (suc n) := printString "*" >> f n; + | (suc n) := printString "*" >>> f n; in f 3; diff --git a/tests/Compilation/positive/test054.juvix b/tests/Compilation/positive/test054.juvix index aae917428..2b1a49c55 100644 --- a/tests/Compilation/positive/test054.juvix +++ b/tests/Compilation/positive/test054.juvix @@ -36,12 +36,12 @@ myfor2 syntax iterator myzip2 {init := 2; range := 2}; myzip2 : {A A' B C : Type} - → (A → A' → B → C → A × A') + → (A → A' → B → C → Pair A A') → A → A' → List B → List C - → A × A' + → Pair A A' | f a b xs ys := myfor (acc, acc' := a, b) (x, y in zip xs ys) f acc acc' x y; diff --git a/tests/Compilation/positive/test055.juvix b/tests/Compilation/positive/test055.juvix index a95219117..120fb8a31 100644 --- a/tests/Compilation/positive/test055.juvix +++ b/tests/Compilation/positive/test055.juvix @@ -3,9 +3,9 @@ module test055; import Stdlib.Prelude open; -type Pair := - | pair : Nat -> Nat -> Pair; +type Pair' := + | pair : Nat -> Nat -> Pair'; -main : List (Pair × Nat) × List Pair := +main : Pair (List (Pair Pair' Nat)) (List Pair') := (pair 1 2, 3) :: (pair 2 3, 4) :: nil , pair 1 2 :: pair 2 3 :: nil; diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix index a03b09664..fe2fce252 100644 --- a/tests/Compilation/positive/test060.juvix +++ b/tests/Compilation/positive/test060.juvix @@ -10,13 +10,13 @@ type Triple (A B C : Type) := thd : C }; -type Pair (A B : Type) := +type Pair' (A B : Type) := mkPair { fst : A; snd : B }; -mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool +mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool | mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst | x := case x of _ := false; diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix index a99ef36e0..089fe32ed 100644 --- a/tests/Compilation/positive/test061.juvix +++ b/tests/Compilation/positive/test061.juvix @@ -66,7 +66,7 @@ showBoolFunI : Show (Bool → Bool) := mkShow@{ }; instance -showPairI {A B} {{Show A}} {{Show' B}} : Show' (A × B) := +showPairI {A B} {{Show A}} {{Show' B}} : Show' (Pair A B) := mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y}; trait @@ -79,19 +79,19 @@ instance tFunI {A} {{T A}} : T (A -> A) := mkT \ { a := a }; main : IO := - printStringLn (Show.show true) >> - printStringLn (f false) >> - printStringLn (Show.show 3) >> - printStringLn (Show.show (g {Nat})) >> - printStringLn (Show.show [true; false]) >> - printStringLn (Show.show [1; 2; 3]) >> - printStringLn (f' [1; 2]) >> - printStringLn (f'' [true; false]) >> - printStringLn (f'3 [just true; nothing; just false]) >> - printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >> - printStringLn (f'3 "abba") >> - printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >> - printStringLn (f5 "abba" 3) >> - printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >> - printStringLn (Show.show (λ{x := not x})) >> + printStringLn (Show.show true) >>> + printStringLn (f false) >>> + printStringLn (Show.show 3) >>> + printStringLn (Show.show (g {Nat})) >>> + printStringLn (Show.show [true; false]) >>> + printStringLn (Show.show [1; 2; 3]) >>> + printStringLn (f' [1; 2]) >>> + printStringLn (f'' [true; false]) >>> + printStringLn (f'3 [just true; nothing; just false]) >>> + printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>> + printStringLn (f'3 "abba") >>> + printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>> + printStringLn (f5 "abba" 3) >>> + printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >>> + printStringLn (Show.show (λ{x := not x})) >>> printStringLn (Show.show (3, [1; 2 + T.a 0])); diff --git a/tests/Compilation/positive/test063.juvix b/tests/Compilation/positive/test063.juvix index ee1c50c52..0ede701e3 100644 --- a/tests/Compilation/positive/test063.juvix +++ b/tests/Compilation/positive/test063.juvix @@ -77,10 +77,10 @@ h {A} {{U2 A}} : A -> A := f; main : IO := printStringLn (T1.pp "a") - >> printStringLn (T2.pp "b") - >> printStringLn (T3.pp "c") - >> printStringLn (T4.pp "d") - >> printStringLn (U.pp "e") - >> printStringLn (f "f") - >> printStringLn (g {{mkU1 id}} "g") - >> printStringLn (h "h"); + >>> printStringLn (T2.pp "b") + >>> printStringLn (T3.pp "c") + >>> printStringLn (T4.pp "d") + >>> printStringLn (U.pp "e") + >>> printStringLn (f "f") + >>> printStringLn (g {{mkU1 id}} "g") + >>> printStringLn (h "h"); diff --git a/tests/Compilation/positive/test069.juvix b/tests/Compilation/positive/test069.juvix index 58dc77089..8e31e48d9 100644 --- a/tests/Compilation/positive/test069.juvix +++ b/tests/Compilation/positive/test069.juvix @@ -3,7 +3,7 @@ module test069; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Compilation/positive/test071.juvix b/tests/Compilation/positive/test071.juvix index 84f4d5100..d552c6682 100644 --- a/tests/Compilation/positive/test071.juvix +++ b/tests/Compilation/positive/test071.juvix @@ -3,7 +3,7 @@ module test071; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Compilation/positive/test072/Monad.juvix b/tests/Compilation/positive/test072/Monad.juvix index 81a4dfb96..e96aa763e 100644 --- a/tests/Compilation/positive/test072/Monad.juvix +++ b/tests/Compilation/positive/test072/Monad.juvix @@ -16,6 +16,6 @@ type Monad (f : Type -> Type) := open Monad public; -syntax operator >> bind; ->> {M : Type → Type} {A B : Type} {{Monad M}} (x : M +syntax operator >>> bind; +>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/Compilation/positive/test072/Reader.juvix b/tests/Compilation/positive/test072/Reader.juvix index 7e89040ff..8de25df4a 100644 --- a/tests/Compilation/positive/test072/Reader.juvix +++ b/tests/Compilation/positive/test072/Reader.juvix @@ -10,7 +10,7 @@ instance Reader-Functor {R : Type} : Functor (Reader R) := mkFunctor@{ <$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra) + | (mkReader ra) := mkReader (f << ra) }; instance diff --git a/tests/Compilation/positive/test072/ReaderT.juvix b/tests/Compilation/positive/test072/ReaderT.juvix index 95d4d7d3d..c9e7ee662 100644 --- a/tests/Compilation/positive/test072/ReaderT.juvix +++ b/tests/Compilation/positive/test072/ReaderT.juvix @@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} monad := ReaderT-Monad; ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s}; reader {A : Type} (f : S → A) : ReaderT S M A := - mkReaderT (MMonad.return ∘ f) + mkReaderT (MMonad.return << f) }; import MonadState open; import StateT open; import Identity open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; liftReaderT {R A : Type} {M : Type → Type} (m : M A) : ReaderT R M A := mkReaderT (const m); @@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := monadic : ReaderT Nat (StateT Nat Identity) Nat := askNat >>= λ {n := - liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + liftReaderT (modify λ {m := m * n}) >>> liftReaderT get}; main : Nat := runIdentity (evalState 2 (runReader 5 monadic)); @@ -87,6 +87,6 @@ main : Nat := -- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) := -- mkMonadReader@{ -- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}}; --- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader; +-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader; -- ask : StateT S M R := liftStateT MonadReader.ask; -- }; diff --git a/tests/Compilation/positive/test072/State.juvix b/tests/Compilation/positive/test072/State.juvix index 2e7fadc12..939ebbe48 100644 --- a/tests/Compilation/positive/test072/State.juvix +++ b/tests/Compilation/positive/test072/State.juvix @@ -2,9 +2,9 @@ module State; import Monad open; import Functor open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; -type State (S A : Type) := mkState {runState : S -> A × S}; +type State (S A : Type) := mkState {runState : S -> Pair A S}; instance State-Functor {S : Type} : Functor (State S) := diff --git a/tests/Compilation/positive/test072/StateT.juvix b/tests/Compilation/positive/test072/StateT.juvix index f804233f3..3ea027ccf 100644 --- a/tests/Compilation/positive/test072/StateT.juvix +++ b/tests/Compilation/positive/test072/StateT.juvix @@ -4,15 +4,15 @@ import Monad open; import Monad open using {module Monad as MMonad}; import Functor open; import Functor open using {module Functor as MFunctor}; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type StateT (S : Type) (M : Type → Type) (A : Type) := - mkStateT {runStateT : S → M (A × S)}; + mkStateT {runStateT : S → M (Pair A S)}; runState {S A : Type} {M : Type → Type} (s : S) (m : StateT S M - A) : M (A × S) := StateT.runStateT m s; + A) : M (Pair A S) := StateT.runStateT m s; evalState {S A : Type} {M : Type → Type} {{Functor M}} (s : S) (m : StateT S M A) : M A := diff --git a/tests/Geb/positive/Compilation/test011.juvix b/tests/Geb/positive/Compilation/test011.juvix index 87444c4d5..c5b35eb9f 100644 --- a/tests/Geb/positive/Compilation/test011.juvix +++ b/tests/Geb/positive/Compilation/test011.juvix @@ -3,8 +3,8 @@ module test011; import Stdlib.Prelude open; -type Pair := - | pair : ((Nat → Nat) → Nat → Nat) → Nat → Pair; +type Pair' := + | pair : ((Nat → Nat) → Nat → Nat) → Nat → Pair'; id' : Nat → Nat | x := x; @@ -15,7 +15,7 @@ id'' : (Nat → Nat) → Nat → Nat id''' : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat | x := x; -f : Pair → Nat +f : Pair' → Nat | l := (case l of | pair x zero := x diff --git a/tests/Geb/positive/Compilation/test027.juvix b/tests/Geb/positive/Compilation/test027.juvix index dcf7f49b5..9dd9a6457 100644 --- a/tests/Geb/positive/Compilation/test027.juvix +++ b/tests/Geb/positive/Compilation/test027.juvix @@ -3,12 +3,11 @@ module test027; import Stdlib.Prelude open; -type Pair := - | pair : Nat -> Nat -> Pair; +type Pair' := + | pair : Nat -> Nat -> Pair'; main : Nat := case pair 1 2 of | pair (suc _) zero := 0 | pair (suc _) (suc x) := x | _ := 19; - diff --git a/tests/Internal/positive/AsPatterns.juvix b/tests/Internal/positive/AsPatterns.juvix index 793fd9d73..7837d930e 100644 --- a/tests/Internal/positive/AsPatterns.juvix +++ b/tests/Internal/positive/AsPatterns.juvix @@ -5,7 +5,7 @@ import Stdlib.Prelude open; printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; f1 : List Nat -> List Nat | a@(x :: x' :: xs) := a @@ -38,8 +38,8 @@ l2 : List Nat := main : IO := printListNatLn (f1 l1) - >> printListNatLn (f2 l1) - >> printListNatLn (f3 zero l1) - >> printNatLn (f4 zero l1) - >> printListNatLn (f5 l1 l2); + >>> printListNatLn (f2 l1) + >>> printListNatLn (f3 zero l1) + >>> printNatLn (f4 zero l1) + >>> printListNatLn (f5 l1 l2); diff --git a/tests/Internal/positive/Case.juvix b/tests/Internal/positive/Case.juvix index 71f839a61..1dfd3ab42 100644 --- a/tests/Internal/positive/Case.juvix +++ b/tests/Internal/positive/Case.juvix @@ -17,4 +17,4 @@ andList : List Bool → Bool main : IO := printBoolLn (not' false) - >> printBoolLn (andList (true :: false :: nil)); + >>> printBoolLn (andList (true :: false :: nil)); diff --git a/tests/Internal/positive/Church.juvix b/tests/Internal/positive/Church.juvix index b3fb29c40..ecb3e2b0a 100644 --- a/tests/Internal/positive/Church.juvix +++ b/tests/Internal/positive/Church.juvix @@ -8,7 +8,7 @@ czero : Num | {_} f x := x; csuc : Num → Num - | n {_} f := f ∘ n {_} f; + | n {_} f := f << n {_} f; toNat : Num → Nat | n := n {_} ((+) (suc zero)) zero; diff --git a/tests/Internal/positive/Lambda.juvix b/tests/Internal/positive/Lambda.juvix index b9dfc8fa9..73b84cc2e 100644 --- a/tests/Internal/positive/Lambda.juvix +++ b/tests/Internal/positive/Lambda.juvix @@ -9,10 +9,10 @@ uncurry' → {B : Type} → {C : Type} → (A → B → C) - → A × B + → Pair A B → C := λ {| f (a, b) := f a b}; -fst' : {A : Type} → {B : Type} → A × B → A +fst' : {A : Type} → {B : Type} → Pair A B → A | {_} := λ {| (a, _) := a}; first' @@ -20,8 +20,8 @@ first' → {B : Type} → {A' : Type} → (A → A') - → A × B - → A' × B := λ {| f (a, b) := f a, b}; + → Pair A B + → Pair A' B := λ {| f (a, b) := f a, b}; foldr' : {A : Type} @@ -37,7 +37,7 @@ foldr' main : IO := printNatLn (id' zero) - >> printNatLn (uncurry' (+) (1, 1)) - >> printNatLn (fst' (zero, 1)) - >> printNatLn (fst (first' ((+) 1) (1, zero))) - >> printNatLn (foldr' (+) zero (1 :: 2 :: 3 :: nil)); + >>> printNatLn (uncurry' (+) (1, 1)) + >>> printNatLn (fst' (zero, 1)) + >>> printNatLn (fst (first' ((+) 1) (1, zero))) + >>> printNatLn (foldr' (+) zero (1 :: 2 :: 3 :: nil)); diff --git a/tests/Internal/positive/LitIntegerToNat.juvix b/tests/Internal/positive/LitIntegerToNat.juvix index beeb15012..671c300c0 100644 --- a/tests/Internal/positive/LitIntegerToNat.juvix +++ b/tests/Internal/positive/LitIntegerToNat.juvix @@ -6,5 +6,5 @@ f : Nat -> Nat | (suc x) := x | zero := 0; -main : IO := printNatLn (f 3) >> printNatLn (f 0); +main : IO := printNatLn (f 3) >>> printNatLn (f 0); diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix index 65c6318b9..c19a9c1d7 100644 --- a/tests/Internal/positive/QuickSort.juvix +++ b/tests/Internal/positive/QuickSort.juvix @@ -2,7 +2,7 @@ module QuickSort; import Stdlib.Prelude open hiding {quickSort}; -qsHelper : {A : Type} → A → List A × List A → List A +qsHelper : {A : Type} → A → Pair (List A) (List A) → List A | a (l, r) := l ++ (a :: nil) ++ r; terminating @@ -13,7 +13,7 @@ quickSort | cmp (x :: xs) := qsHelper x - (both (quickSort cmp) (partition (isGT ∘ cmp x) xs)); + (both (quickSort cmp) (partition (isGT << cmp x) xs)); uniq : {A : Type} -> (A -> A -> Ordering) -> List A -> List A diff --git a/tests/Rust/Compilation/positive/test030.juvix b/tests/Rust/Compilation/positive/test030.juvix index b5434b9b2..0f5f54db4 100644 --- a/tests/Rust/Compilation/positive/test030.juvix +++ b/tests/Rust/Compilation/positive/test030.juvix @@ -7,7 +7,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A -- clauses with differing number of patterns not yet supported -- iterate f zero x := x; | f zero := id - | f (suc n) := f ∘ iterate f n; + | f (suc n) := f << iterate f n; plus : Nat → Nat → Nat := iterate suc; diff --git a/tests/Rust/Compilation/positive/test032.juvix b/tests/Rust/Compilation/positive/test032.juvix index eb6fe5259..b6932d7ac 100644 --- a/tests/Rust/Compilation/positive/test032.juvix +++ b/tests/Rust/Compilation/positive/test032.juvix @@ -3,7 +3,7 @@ module test032; import Stdlib.Prelude open; -split : {A : Type} → Nat → List A → List A × List A +split : {A : Type} → Nat → List A → Pair (List A) (List A) | zero xs := nil, xs | (suc n) nil := nil, nil | (suc n) (x :: xs) := @@ -46,7 +46,7 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat) printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; sum : List Nat → Nat | nil := 0 diff --git a/tests/Rust/Compilation/positive/test033.juvix b/tests/Rust/Compilation/positive/test033.juvix index e2be0043f..27ce2e8d8 100644 --- a/tests/Rust/Compilation/positive/test033.juvix +++ b/tests/Rust/Compilation/positive/test033.juvix @@ -9,19 +9,19 @@ f : (Nat → Nat) → Nat f' : Nat → Nat | x := f ((+) x); -g : (Nat → Nat × Nat) → Nat × Nat +g : (Nat → Pair Nat Nat) → Pair Nat Nat | f := f 2; -g' : Nat → Nat × Nat +g' : Nat → Pair Nat Nat | x := g ((,) x); f1' : Nat → Nat → Nat | x y := f ((+) (div x y)); -g1' : Nat → Nat → Nat × Nat +g1' : Nat → Nat → Pair Nat Nat | x y := g ((,) (div x y)); -h : (Nat → Nat → Nat × Nat) → Nat × Nat +h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat | f := f 1 2; main : Nat := diff --git a/tests/Rust/Compilation/positive/test035.juvix b/tests/Rust/Compilation/positive/test035.juvix index 75a9d3ffe..9386150d3 100644 --- a/tests/Rust/Compilation/positive/test035.juvix +++ b/tests/Rust/Compilation/positive/test035.juvix @@ -44,7 +44,7 @@ h : Nat -> Nat printListNatLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := - printNat x >> printString " :: " >> printListNatLn xs; + printNat x >>> printString " :: " >>> printListNatLn xs; main : Nat := head 0 (sum2 (lgen 5)) diff --git a/tests/Rust/Compilation/positive/test036.juvix b/tests/Rust/Compilation/positive/test036.juvix index 540f26bed..5af459d39 100644 --- a/tests/Rust/Compilation/positive/test036.juvix +++ b/tests/Rust/Compilation/positive/test036.juvix @@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A f : Nat → Nat := suc; g : Nat → Nat → Nat - | z := f ∘ flip sub z; + | z := f << flip sub z; g' : Nat → Nat → Nat - | z := f ∘ λ {x := sub x z}; + | z := f << λ {x := sub x z}; -h : Nat → Nat := f ∘ g 3; +h : Nat → Nat := f << g 3; j : Nat → Nat → Nat := g'; diff --git a/tests/Rust/Compilation/positive/test054.juvix b/tests/Rust/Compilation/positive/test054.juvix index aae917428..2b1a49c55 100644 --- a/tests/Rust/Compilation/positive/test054.juvix +++ b/tests/Rust/Compilation/positive/test054.juvix @@ -36,12 +36,12 @@ myfor2 syntax iterator myzip2 {init := 2; range := 2}; myzip2 : {A A' B C : Type} - → (A → A' → B → C → A × A') + → (A → A' → B → C → Pair A A') → A → A' → List B → List C - → A × A' + → Pair A A' | f a b xs ys := myfor (acc, acc' := a, b) (x, y in zip xs ys) f acc acc' x y; diff --git a/tests/Rust/Compilation/positive/test060.juvix b/tests/Rust/Compilation/positive/test060.juvix index 6e306a394..7e352001f 100644 --- a/tests/Rust/Compilation/positive/test060.juvix +++ b/tests/Rust/Compilation/positive/test060.juvix @@ -10,7 +10,7 @@ type Triple (A B C : Type) := thd : C }; -type Pair (A B : Type) := +type Pair' (A B : Type) := mkPair { fst : A; snd : B @@ -19,7 +19,7 @@ type Pair (A B : Type) := sum : Triple Nat Nat Nat → Nat | mkTriple@{fst; snd; thd} := fst + snd + thd; -mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool +mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool | mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst | x := case x of {_ := false}; @@ -34,7 +34,7 @@ main : Nat := }; f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10}); - in sum $ if + in sum <| if (mf mkPair@{ fst := mkPair true nil; diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix index ac9dda3ab..0484d600d 100644 --- a/tests/Rust/Compilation/positive/test069.juvix +++ b/tests/Rust/Compilation/positive/test069.juvix @@ -3,7 +3,7 @@ module test069; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix index 84f4d5100..d552c6682 100644 --- a/tests/Rust/Compilation/positive/test071.juvix +++ b/tests/Rust/Compilation/positive/test071.juvix @@ -3,7 +3,7 @@ module test071; import Stdlib.Data.Nat open hiding {Ord; mkOrd}; import Stdlib.Data.Nat.Ord as Ord; -import Stdlib.Data.Product as Ord; +import Stdlib.Data.Pair as Ord; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; diff --git a/tests/Rust/Compilation/positive/test072/Monad.juvix b/tests/Rust/Compilation/positive/test072/Monad.juvix index 81a4dfb96..e96aa763e 100644 --- a/tests/Rust/Compilation/positive/test072/Monad.juvix +++ b/tests/Rust/Compilation/positive/test072/Monad.juvix @@ -16,6 +16,6 @@ type Monad (f : Type -> Type) := open Monad public; -syntax operator >> bind; ->> {M : Type → Type} {A B : Type} {{Monad M}} (x : M +syntax operator >>> bind; +>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/Rust/Compilation/positive/test072/Reader.juvix b/tests/Rust/Compilation/positive/test072/Reader.juvix index 7e89040ff..8de25df4a 100644 --- a/tests/Rust/Compilation/positive/test072/Reader.juvix +++ b/tests/Rust/Compilation/positive/test072/Reader.juvix @@ -10,7 +10,7 @@ instance Reader-Functor {R : Type} : Functor (Reader R) := mkFunctor@{ <$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra) + | (mkReader ra) := mkReader (f << ra) }; instance diff --git a/tests/Rust/Compilation/positive/test072/ReaderT.juvix b/tests/Rust/Compilation/positive/test072/ReaderT.juvix index 95d4d7d3d..c9e7ee662 100644 --- a/tests/Rust/Compilation/positive/test072/ReaderT.juvix +++ b/tests/Rust/Compilation/positive/test072/ReaderT.juvix @@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} monad := ReaderT-Monad; ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s}; reader {A : Type} (f : S → A) : ReaderT S M A := - mkReaderT (MMonad.return ∘ f) + mkReaderT (MMonad.return << f) }; import MonadState open; import StateT open; import Identity open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; liftReaderT {R A : Type} {M : Type → Type} (m : M A) : ReaderT R M A := mkReaderT (const m); @@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := monadic : ReaderT Nat (StateT Nat Identity) Nat := askNat >>= λ {n := - liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + liftReaderT (modify λ {m := m * n}) >>> liftReaderT get}; main : Nat := runIdentity (evalState 2 (runReader 5 monadic)); @@ -87,6 +87,6 @@ main : Nat := -- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) := -- mkMonadReader@{ -- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}}; --- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader; +-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader; -- ask : StateT S M R := liftStateT MonadReader.ask; -- }; diff --git a/tests/Rust/Compilation/positive/test072/State.juvix b/tests/Rust/Compilation/positive/test072/State.juvix index 2e7fadc12..df7e8d486 100644 --- a/tests/Rust/Compilation/positive/test072/State.juvix +++ b/tests/Rust/Compilation/positive/test072/State.juvix @@ -2,7 +2,7 @@ module State; import Monad open; import Functor open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type State (S A : Type) := mkState {runState : S -> A × S}; diff --git a/tests/Rust/Compilation/positive/test072/StateT.juvix b/tests/Rust/Compilation/positive/test072/StateT.juvix index f804233f3..3ea027ccf 100644 --- a/tests/Rust/Compilation/positive/test072/StateT.juvix +++ b/tests/Rust/Compilation/positive/test072/StateT.juvix @@ -4,15 +4,15 @@ import Monad open; import Monad open using {module Monad as MMonad}; import Functor open; import Functor open using {module Functor as MFunctor}; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; type StateT (S : Type) (M : Type → Type) (A : Type) := - mkStateT {runStateT : S → M (A × S)}; + mkStateT {runStateT : S → M (Pair A S)}; runState {S A : Type} {M : Type → Type} (s : S) (m : StateT S M - A) : M (A × S) := StateT.runStateT m s; + A) : M (Pair A S) := StateT.runStateT m s; evalState {S A : Type} {M : Type → Type} {{Functor M}} (s : S) (m : StateT S M A) : M A := diff --git a/tests/VampIR/positive/Compilation/test002.juvix b/tests/VampIR/positive/Compilation/test002.juvix index b925d7c76..19c1718bf 100644 --- a/tests/VampIR/positive/Compilation/test002.juvix +++ b/tests/VampIR/positive/Compilation/test002.juvix @@ -17,7 +17,7 @@ boolToNat : Bool -> Nat main : Nat -> Nat -> Nat | a b := boolToNat - $ λ { + <| λ { | x (Just b) := if x false b | _ Nothing := false } diff --git a/tests/VampIR/positive/Compilation/test003.juvix b/tests/VampIR/positive/Compilation/test003.juvix index c41e34aba..f6a914075 100644 --- a/tests/VampIR/positive/Compilation/test003.juvix +++ b/tests/VampIR/positive/Compilation/test003.juvix @@ -17,7 +17,7 @@ boolToNat : Bool -> Nat main : Nat -> Nat -> Nat | x y := boolToNat - $ λ { + <| λ { | opt0 := false | (opt1 b) := b | (opt2 b c) := if b b c diff --git a/tests/VampIR/positive/Compilation/test006.juvix b/tests/VampIR/positive/Compilation/test006.juvix index bcf541d58..e60168c19 100644 --- a/tests/VampIR/positive/Compilation/test006.juvix +++ b/tests/VampIR/positive/Compilation/test006.juvix @@ -18,7 +18,7 @@ boolToNat : Bool -> Nat main : Nat -> Nat -> Nat | x y := boolToNat - $ case + <| case opt3 (natToBool x) λ {x y := if y false x} (natToBool y) of { | opt0 := false diff --git a/tests/VampIR/positive/Compilation/test009.juvix b/tests/VampIR/positive/Compilation/test009.juvix index 6ef11eeb9..cd0523c4a 100644 --- a/tests/VampIR/positive/Compilation/test009.juvix +++ b/tests/VampIR/positive/Compilation/test009.juvix @@ -3,7 +3,7 @@ module test009; import Stdlib.Prelude open; -f : Nat -> ((Nat -> Nat) -> Nat -> Nat) × Nat → Nat +f : Nat -> Pair ((Nat -> Nat) -> Nat -> Nat) Nat → Nat | a l := case l of { | x, zero := x diff --git a/tests/VampIR/positive/Compilation/test020.juvix b/tests/VampIR/positive/Compilation/test020.juvix index 877a305e7..a0a881ba8 100644 --- a/tests/VampIR/positive/Compilation/test020.juvix +++ b/tests/VampIR/positive/Compilation/test020.juvix @@ -6,7 +6,7 @@ import Stdlib.Prelude open; {-# unroll: 10 #-} compose : {A : Type} → Nat → (A → A) → A → A | zero _ := id - | (suc n) f := f ∘ compose n f; + | (suc n) f := f << compose n f; main : Nat → Bool → Bool | n b := compose n not b; diff --git a/tests/benchmark/ackermann/juvix/ackermann.juvix b/tests/benchmark/ackermann/juvix/ackermann.juvix index 3f6258829..a4b1d13b3 100644 --- a/tests/benchmark/ackermann/juvix/ackermann.juvix +++ b/tests/benchmark/ackermann/juvix/ackermann.juvix @@ -5,7 +5,7 @@ import Stdlib.Prelude open; iter : {A : Type} → (A → A) → Nat → A → A | f zero := id - | f (suc n) := f ∘ iter f n; + | f (suc n) := f << iter f n; step : (Nat → Nat) → Nat → Nat | f n := iter f (suc n) 1; diff --git a/tests/benchmark/mergesort/juvix/mergesort.juvix b/tests/benchmark/mergesort/juvix/mergesort.juvix index b1126319c..05afda83d 100644 --- a/tests/benchmark/mergesort/juvix/mergesort.juvix +++ b/tests/benchmark/mergesort/juvix/mergesort.juvix @@ -4,11 +4,11 @@ module mergesort; import Stdlib.Prelude open; split_go - : {A : Type} → List A → List A → List A → List A × List A + : {A : Type} → List A → List A → List A → Pair (List A) (List A) | nil ys zs := ys, zs | (x :: xs') ys zs := split_go xs' zs (x :: ys); -split : {A : Type} → List A → List A × List A +split : {A : Type} → List A → Pair (List A) (List A) | xs := split_go xs nil nil; revappend : {A : Type} → List A → List A → List A @@ -25,7 +25,7 @@ merget : List Nat → List Nat → List Nat → List Nat (merget (x :: xs') ys' (y :: acc)); terminating -sort' : List Nat × List Nat → List Nat +sort' : Pair (List Nat) (List Nat) → List Nat | (l1, l2) := merget (sort l1) (sort l2) nil; terminating diff --git a/tests/negative/issue2771/Main.juvix b/tests/negative/issue2771/Main.juvix index d579fd2b5..829f0e48d 100644 --- a/tests/negative/issue2771/Main.juvix +++ b/tests/negative/issue2771/Main.juvix @@ -2,11 +2,8 @@ module Main; type T := t; -type Box := mkBox { unbox : T }; +type Box := mkBox {unbox : T}; -f (b : Box) : Box := - case b of { - mkBox _ := mkBox t - }; +f (b : Box) : Box := case b of mkBox _ := mkBox t; main : T := f (mkBox t); diff --git a/tests/positive/Ape.juvix b/tests/positive/Ape.juvix index 9b268ca71..2a1b592c2 100644 --- a/tests/positive/Ape.juvix +++ b/tests/positive/Ape.juvix @@ -15,8 +15,8 @@ axiom * : String → String → String; syntax operator - sub; axiom - : String → String → String; -syntax operator >> seq; -axiom >> : String → String → String; +syntax operator >>> seq; +axiom >>> : String → String → String; syntax operator + ladd; axiom + : String → String → String; @@ -56,13 +56,13 @@ nesting : String := t : String := "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" - >> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + >>> "Hellooooooooo" + "Hellooooooooo" + "Hellooooooooo" + ("Hellooooooooo" diff --git a/tests/positive/Internal/AsPattern.juvix b/tests/positive/Internal/AsPattern.juvix index 253ff1c39..76434bca1 100644 --- a/tests/positive/Internal/AsPattern.juvix +++ b/tests/positive/Internal/AsPattern.juvix @@ -2,9 +2,9 @@ module AsPattern; import Stdlib.Data.Fixity open; -syntax operator ∘ composition; +syntax operator << composition; -∘ +<< : {A : Type} → {B : Type} → {C : Type} @@ -48,5 +48,5 @@ a : {A : Type} → A × Nat → Nat | p@(x, s@_) := snd p + suc zero; b : {A : Type} → A × Nat → ({B : Type} → B → B) → A - | p@(_, zero) f := (f ∘ fst) p - | p@(_, _) f := (f ∘ fst) p; + | p@(_, zero) f := (f << fst) p + | p@(_, _) f := (f << fst) p; diff --git a/tests/positive/Internal/Implicit.juvix b/tests/positive/Internal/Implicit.juvix index 17b9cfd79..6fd601145 100644 --- a/tests/positive/Internal/Implicit.juvix +++ b/tests/positive/Internal/Implicit.juvix @@ -2,9 +2,9 @@ module Implicit; import Stdlib.Data.Fixity open; -syntax operator ∘ composition; +syntax operator << composition; -∘ +<< : {A : Type} → {B : Type} → {C : Type} diff --git a/tests/positive/Internal/Lambda.juvix b/tests/positive/Internal/Lambda.juvix index cc96c3824..208f9b0f6 100644 --- a/tests/positive/Internal/Lambda.juvix +++ b/tests/positive/Internal/Lambda.juvix @@ -10,9 +10,9 @@ syntax operator × functor; syntax operator , pair; type × (A : Type) (B : Type) := , : A → B → A × B; -syntax operator ∘ composition; +syntax operator << composition; -∘ +<< : {A : Type} → {B : Type} → {C : Type} diff --git a/tests/positive/Internal/Synonyms.juvix b/tests/positive/Internal/Synonyms.juvix index 3d579ad34..2b2c77e2b 100644 --- a/tests/positive/Internal/Synonyms.juvix +++ b/tests/positive/Internal/Synonyms.juvix @@ -23,4 +23,4 @@ czero : Num | {_} f x := x; csuc : idTy2 Num → idTy Num - | n {_} f := f ∘ n {_} f; + | n {_} f := f << n {_} f; diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md index 7146c7971..12698dd12 100644 --- a/tests/positive/Markdown/Test.juvix.md +++ b/tests/positive/Markdown/Test.juvix.md @@ -42,7 +42,7 @@ end; Commands like `typecheck` and `compile` can be used with Juvix Markdown files. ```juvix -main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat); +main : IO := readLn (printNatLn << fibonacci << stringToNat); ``` Other code blocks are not touched, e.g: diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md index ad7c67399..d4c15f200 100644 --- a/tests/positive/Markdown/markdown/Test.md +++ b/tests/positive/Markdown/markdown/Test.md @@ -21,7 +21,7 @@ You can pass a number to the `extract-module-statements` attribute to drop that Commands like `typecheck` and `compile` can be used with Juvix Markdown files. -
main : IO := readLn (printNatLn  fibonacci  stringToNat);
+
main : IO := readLn (printNatLn << fibonacci << stringToNat);
Other code blocks are not touched, e.g: diff --git a/tests/positive/Traits2.juvix b/tests/positive/Traits2.juvix index 75adc5202..22f60252a 100644 --- a/tests/positive/Traits2.juvix +++ b/tests/positive/Traits2.juvix @@ -66,24 +66,27 @@ Maybe-Monad : Monad Maybe := import Stdlib.Data.Bool open; import Stdlib.Function open; -import Stdlib.Data.Product open; +import Stdlib.Data.Pair open; -×-fmap {A B C : Type} (f : B -> C) : A × B -> A × C +×-fmap {A B C : Type} (f : B -> C) : Pair A B -> Pair A C | (a, b) := a, f b; -×-Functor : {A : Type} -> Functor ((×) A) := +×-Functor : {A : Type} -> Functor (Pair A) := mkFunctor ×-fmap; ×-bind {A : Type} {{Semigroup A}} {B C : Type} - : A × B -> (B -> A × C) -> A × C + : Pair A B -> (B -> Pair A C) -> Pair A C | (a, b) f := case f b of a', b' := a <> a', b'; instance ×-Monad - {A : Type} {{Semigroup A}} {{Monoid A}} : Monad ((×) A) := + {A : Type} + {{Semigroup A}} + {{Monoid A}} + : Monad (Pair A) := mkMonad@{ bind := ×-bind; return := λ {b := Monoid.mempty, b}; @@ -94,7 +97,7 @@ type Reader (r a : Type) := mkReader {runReader : r -> a}; Reader-fmap {R A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra); + | (mkReader ra) := mkReader (f << ra); Reader-Functor-NoNamed {R : Type} : Functor (Reader R) := mkFunctor Reader-fmap; @@ -103,7 +106,7 @@ instance Reader-Functor {R : Type} : Functor (Reader R) := mkFunctor@{ fmap {A B : Type} (f : A -> B) : Reader R A -> Reader R B - | (mkReader ra) := mkReader (f ∘ ra) + | (mkReader ra) := mkReader (f << ra) }; instance diff --git a/tests/positive/issue1693/M.juvix b/tests/positive/issue1693/M.juvix index cf7c6ca0b..68bb4ffd7 100644 --- a/tests/positive/issue1693/M.juvix +++ b/tests/positive/issue1693/M.juvix @@ -19,7 +19,7 @@ I : {A : Type} → A → A := S K (K {_} {Bool}); main : IO := printNatLn - $ I {Nat} 1 + <| I {Nat} 1 + I I 1 + I (I 1) + I 1 diff --git a/tests/positive/issue1731/builtinFail.juvix b/tests/positive/issue1731/builtinFail.juvix index 144b242b1..a665df790 100644 --- a/tests/positive/issue1731/builtinFail.juvix +++ b/tests/positive/issue1731/builtinFail.juvix @@ -8,5 +8,5 @@ axiom fail : {A : Type} → String → A; main : IO := printStringLn "Get" - >> fail "Enough" - >> printStringLn "Sleep"; + >>> fail "Enough" + >>> printStringLn "Sleep"; diff --git a/tests/positive/issue1731/builtinTrace.juvix b/tests/positive/issue1731/builtinTrace.juvix index 66882db66..e6234a03d 100644 --- a/tests/positive/issue1731/builtinTrace.juvix +++ b/tests/positive/issue1731/builtinTrace.juvix @@ -7,15 +7,15 @@ axiom trace : {A : Type} → A → A; terminating f : Nat → Nat → Nat - | x y := if (x == 0) y (trace x >>> f (sub x 1) y); + | x y := if (x == 0) y (trace x >-> f (sub x 1) y); {- f 4 0 = -trace 4 >>> f 3 0 -=> trace 4 >>> trace 3 >>> f 2 0 -=> trace 4 >>> trace 3 >>> trace 2 >>> f 1 0 -=> trace 4 >>> trace 3 >>> trace 2 >>> trace 1 (f 0 0) -=> trace 4 >>> trace 3 >>> trace 2 >>> trace 1 0 +trace 4 >-> f 3 0 +=> trace 4 >-> trace 3 >-> f 2 0 +=> trace 4 >-> trace 3 >-> trace 2 >-> f 1 0 +=> trace 4 >-> trace 3 >-> trace 2 >-> trace 1 (f 0 0) +=> trace 4 >-> trace 3 >-> trace 2 >-> trace 1 0 = 0 -} -main : IO := printNatLn $ f 4 0; +main : IO := printNatLn <| f 4 0; diff --git a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml index 57308873e..50821a38e 100644 --- a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml +++ b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml @@ -268,7 +268,7 @@ tests: module HelloDep; import Stdlib.Prelude open; import HelloDep2 open; - main : IO := printStringLn "Hello from dep1" >> printStringLn hello; + main : IO := printStringLn "Hello from dep1" >>> printStringLn hello; EOF cat <<-EOF > Package.juvix @@ -352,7 +352,7 @@ tests: module HelloDep; import HelloDep2 open; import Stdlib.Prelude open; - main : IO := printStringLn "This is from the second commit" >> printStringLn hello; + main : IO := printStringLn "This is from the second commit" >>> printStringLn hello; EOF git add -A @@ -607,7 +607,7 @@ tests: module HelloDep; import Stdlib.Prelude open; import HelloDep2 open; - main : IO := printStringLn "Hello from dep1" >> printStringLn hello; + main : IO := printStringLn "Hello from dep1" >>> printStringLn hello; EOF cat <<-EOF > Package.juvix diff --git a/tests/smoke/Commands/compile-dependencies.smoke.yaml b/tests/smoke/Commands/compile-dependencies.smoke.yaml index 0979a36bf..d61a8f987 100644 --- a/tests/smoke/Commands/compile-dependencies.smoke.yaml +++ b/tests/smoke/Commands/compile-dependencies.smoke.yaml @@ -252,7 +252,7 @@ tests: module HelloDep; import Stdlib.Prelude open; import HelloDep2 open; - main : IO := printStringLn "Hello from dep1" >> printStringLn hello; + main : IO := printStringLn "Hello from dep1" >>> printStringLn hello; EOF cat <<-EOF > juvix.yaml @@ -328,7 +328,7 @@ tests: module HelloDep; import HelloDep2 open; import Stdlib.Prelude open; - main : IO := printStringLn "This is from the second commit" >> printStringLn hello; + main : IO := printStringLn "This is from the second commit" >>> printStringLn hello; EOF git add -A @@ -571,7 +571,7 @@ tests: module HelloDep; import Stdlib.Prelude open; import HelloDep2 open; - main : IO := printStringLn "Hello from dep1" >> printStringLn hello; + main : IO := printStringLn "Hello from dep1" >>> printStringLn hello; EOF cat <<-EOF > juvix.yaml diff --git a/tests/smoke/Commands/dev/repl.smoke.yaml b/tests/smoke/Commands/dev/repl.smoke.yaml index a72369ec4..da65c9617 100644 --- a/tests/smoke/Commands/dev/repl.smoke.yaml +++ b/tests/smoke/Commands/dev/repl.smoke.yaml @@ -243,7 +243,7 @@ tests: - repl args: - positive/issue1731/builtinTrace.juvix - stdin: trace 2 >>> printNatLn 3 + stdin: trace 2 >-> printNatLn 3 stdout: contains: | 3 diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml index c5d519bd8..cb930c5f2 100644 --- a/tests/smoke/Commands/repl.smoke.yaml +++ b/tests/smoke/Commands/repl.smoke.yaml @@ -71,11 +71,11 @@ tests: - juvix - repl - ../examples/milestone/HelloWorld/HelloWorld.juvix - stdin: ":def >> (>>) (((>>)))" + stdin: ":def >>> (>>>) (((>>>)))" stdout: contains: | builtin IO-sequence - axiom >> : IO → IO → IO + axiom >>> : IO → IO → IO exit-status: 0 - name: repl-def-infix @@ -83,11 +83,11 @@ tests: - juvix - repl - ../examples/milestone/HelloWorld/HelloWorld.juvix - stdin: ":def >>" + stdin: ":def >>>" stdout: contains: | builtin IO-sequence - axiom >> : IO → IO → IO + axiom >>> : IO → IO → IO exit-status: 0 - name: open @@ -295,7 +295,7 @@ tests: - repl args: - positive/issue1731/builtinTrace.juvix - stdin: trace 2 >>> printNatLn 3 + stdin: trace 2 >-> printNatLn 3 stdout: contains: | 3