Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge if -> ite renaming from stdlib #2869

Merged
merged 2 commits into from
Jul 2, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion examples/demo/Demo.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ even' : Nat → Bool
-- base 2 logarithm rounded down
terminating
log2 : Nat → Nat
| n := if (n <= 1) 0 (suc (log2 (div n 2)));
| n := ite (n <= 1) 0 (suc (log2 (div n 2)));

type Tree (A : Type) :=
| leaf : A → Tree A
Expand Down
2 changes: 1 addition & 1 deletion examples/midsquare/MidSquareHash.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ pow : Nat -> Nat
--- (i.e. smaller than 64) using the mid-square algorithm.
hash' : Nat -> Nat -> Nat
| (suc n@(suc (suc m))) x :=
if
ite
(x < pow n)
(hash' n x)
(mod (div (x * x) (pow m)) (pow 6))
Expand Down
26 changes: 13 additions & 13 deletions examples/midsquare/MidSquareHashUnrolled.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -58,55 +58,55 @@ hash3 : Nat -> Nat

hash4 : Nat -> Nat
| x :=
if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);

hash5 : Nat -> Nat
| x :=
if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);

hash6 : Nat -> Nat
| x :=
if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);

hash7 : Nat -> Nat
| x :=
if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);

hash8 : Nat -> Nat
| x :=
if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);

hash9 : Nat -> Nat
| x :=
if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);

hash10 : Nat -> Nat
| x :=
if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);

hash11 : Nat -> Nat
| x :=
if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);

hash12 : Nat -> Nat
| x :=
if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);

hash13 : Nat -> Nat
| x :=
if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);

hash14 : Nat -> Nat
| x :=
if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);

hash15 : Nat -> Nat
| x :=
if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);

hash16 : Nat -> Nat
| x :=
if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);

hash : Nat -> Nat := hash16;

Expand Down
6 changes: 3 additions & 3 deletions examples/milestone/Bank/Bank.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ module Balances;
increment : Field -> Nat -> Balances -> Balances
| f n nil := (f, n) :: nil
| f n ((b, bn) :: bs) :=
if
ite
(f == b)
((b, bn + n) :: bs)
((b, bn) :: increment f n bs);
Expand All @@ -51,7 +51,7 @@ module Balances;
decrement : Field -> Nat -> Balances -> Balances
| _ _ nil := nil
| f n ((b, bn) :: bs) :=
if
ite
(f == b)
((b, sub bn n) :: bs)
((b, bn) :: decrement f n bs);
Expand Down Expand Up @@ -80,7 +80,7 @@ calculateInterest : Nat -> Nat -> Nat -> Nat

--- Asserts some ;Bool; condition.
assert : {A : Type} -> Bool -> A -> A
| c a := if c a (failwith "assertion failed");
| c a := ite c a (failwith "assertion failed");

--- Returns a new ;Token;. Arguments are:
---
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/Collatz/Collatz.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module Collatz;
import Stdlib.Prelude open;

collatzNext (n : Nat) : Nat :=
if (mod n 2 == 0) (div n 2) (3 * n + 1);
ite (mod n 2 == 0) (div n 2) (3 * n + 1);

collatz : Nat → Nat
| zero := zero
Expand Down
8 changes: 4 additions & 4 deletions examples/milestone/TicTacToe/Logic/Game.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,14 @@ import Logic.GameState open public;
--- Checks if we reached the end of the game.
checkState : GameState → GameState
| (state b p e) :=
if
ite
(won (state b p e))
(state
b
p
(terminate
("Player " ++str showSymbol (switch p) ++str " wins!")))
(if
(ite
(draw (state b p e))
(state b p (terminate "It's a draw!"))
(state b p e));
Expand All @@ -29,7 +29,7 @@ playMove : Maybe Nat → GameState → GameState
| nothing (state b p _) :=
state b p (continue "\nInvalid number, try again\n")
| (just k) (state (board s) player e) :=
if
ite
(not (elem (==) k (possibleMoves (flatten s))))
(state
(board s)
Expand All @@ -43,4 +43,4 @@ playMove : Maybe Nat → GameState → GameState

--- Returns ;just; if the given ;Nat; is in range of 1..9
validMove (n : Nat) : Maybe Nat :=
if (n <= 9 && n >= 1) (just n) nothing;
ite (n <= 9 && n >= 1) (just n) nothing;
2 changes: 1 addition & 1 deletion examples/milestone/TicTacToe/Logic/Square.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -23,5 +23,5 @@ showSquare : Square → String
| (occupied s) := " " ++str showSymbol s ++str " ";

replace (player : Symbol) (k : Nat) : Square → Square
| (empty n) := if (n == k) (occupied player) (empty n)
| (empty n) := ite (n == k) (occupied player) (empty n)
| s := s;
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test006.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,6 @@ loop : Nat := loop;

main : Bool :=
trace
(if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
(ite (3 > 0) 1 loop + ite (2 < 1) loop (ite (7 >= 8) loop 1))
>-> trace (2 > 0 || loop == 0)
>-> 2 < 0 && loop == 0;
4 changes: 2 additions & 2 deletions tests/Anoma/Compilation/positive/test012.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,10 @@ terminating
gen : Nat → Tree
| zero := leaf
| n :=
if
ite
(mod n 3 == 0)
(node1 (gen (sub n 1)))
(if
(ite
(mod n 3 == 1)
(node2 (gen (sub n 1)) (gen (sub n 1)))
(node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1))));
Expand Down
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test013.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@ import Stdlib.Debug.Trace open;

f : Nat → Nat → Nat
| x :=
if
ite
(x == 6)
λ {_ := 0}
(if
(ite
(x == 5)
λ {_ := 1}
(if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
(ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));

main : Nat :=
trace (f 5 6)
Expand Down
4 changes: 2 additions & 2 deletions tests/Anoma/Compilation/positive/test015.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@ f : Nat → Nat → Nat
| x :=
let
g (y : Nat) : Nat := x + y;
in if
in ite
(x == 0)
(f 10)
(if (x < 10) λ {y := g (f (sub x 1) y)} g);
(ite (x < 10) λ {y := g (f (sub x 1) y)} g);

g (x : Nat) (h : Nat → Nat) : Nat := x + h x;

Expand Down
4 changes: 2 additions & 2 deletions tests/Anoma/Compilation/positive/test020.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@ import Stdlib.Debug.Trace open;
-- McCarthy's 91 function
terminating
f91 : Nat → Nat
| n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
| n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));

-- subtraction by increments
terminating
subp : Nat → Nat → Nat
| i j := if (i == j) 0 (subp i (j + 1) + 1);
| i j := ite (i == j) 0 (subp i (j + 1) + 1);

main : Nat :=
trace (f91 101)
Expand Down
4 changes: 2 additions & 2 deletions tests/Anoma/Compilation/positive/test021.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@ import Stdlib.Debug.Trace open;
terminating
power' : Nat → Nat → Nat → Nat
| acc a b :=
if
ite
(b == 0)
acc
(if
(ite
(mod b 2 == 0)
(power' acc (a * a) (div b 2))
(power' (acc * a) (a * a) (div b 2)));
Expand Down
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test023.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,14 @@ import Stdlib.Debug.Trace open;
terminating
f : Nat → Nat

| x := if (x < 1) 1 (2 * x + g (sub x 1));
| x := ite (x < 1) 1 (2 * x + g (sub x 1));

terminating
g : Nat → Nat
| x := if (x < 1) 1 (x + h (sub x 1));
| x := ite (x < 1) 1 (x + h (sub x 1));

terminating
h : Nat → Nat
| x := if (x < 1) 1 (x * f (sub x 1));
| x := ite (x < 1) 1 (x * f (sub x 1));

main : Nat := trace (f 5) >-> trace (f 10) >-> f 20;
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test024.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ gen : Nat → Tree
g : Tree → Tree

| leaf := leaf
| (node l r) := if (isNode l) r (node r l);
| (node l r) := ite (isNode l) r (node r l);

terminating
f : Tree → Nat
Expand Down
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test025.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import Stdlib.Debug.Trace open;
terminating
gcd : Nat → Nat → Nat
| a b :=
if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
ite (a > b) (gcd b a) (ite (a == 0) b (gcd (mod b a) a));

main : Nat :=
trace (gcd (3 * 7 * 2) (7 * 2 * 11))
Expand Down
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test028.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
| p s unit :=
case force s of
cons h t :=
if (p h) (cons h (sfilter p t)) (force (sfilter p t));
ite (p h) (cons h (sfilter p t)) (force (sfilter p t));

shead : Stream → Nat
| (cons h _) := h;
Expand Down
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test032.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,14 @@ merge' : List Nat → List Nat → List Nat
| nil ys := ys
| xs nil := xs
| xs@(x :: xs') ys@(y :: ys') :=
if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
ite (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');

terminating
sort : List Nat → List Nat
| xs :=
let
n : Nat := length xs;
in if
in ite
(n <= 1)
xs
case split (div n 2) xs of {l1, l2 :=
Expand All @@ -33,7 +33,7 @@ uniq : List Nat → List Nat
| nil := nil
| (x :: nil) := x :: nil
| (x :: xs@(x' :: _)) :=
if (x == x') (uniq xs) (x :: uniq xs);
ite (x == x') (uniq xs) (x :: uniq xs);

gen : List Nat → Nat → (Nat → Nat) → List Nat
| acc zero f := acc
Expand Down
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test034.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@ sum : Nat → Nat :=
mutrec : Nat :=
let
terminating
f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
terminating
g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
terminating
h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
in trace (f 5)
>-> trace (f 10)
>-> trace (g 5)
Expand Down
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test060.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ main : Triple Nat Nat Nat :=
};
f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
(@Triple{fst := fst * 10});
in if
in ite
(mf
mkPair@{
fst := mkPair true nil;
Expand Down
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test064.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@ f (x y : Nat) : Nat := x + y;

-- TODO: Replace loop with failwith when anoma backend supports strings
{-# inline: false #-}
g (x : Bool) : Bool := if x loop true;
g (x : Bool) : Bool := ite x loop true;

{-# inline: false #-}
h (x : Bool) : Bool := if (g x) false true;
h (x : Bool) : Bool := ite (g x) false true;

{-# inline: false, eval: false #-}
j (x : Nat) : Nat := x + 0;
Expand All @@ -38,6 +38,6 @@ even' : Nat -> Bool := even;
main : Nat :=
sum 3
+ case even' 6 || g true || h true of {
| true := if (g false) (f 1 2 + sum 7 + j 0) 0
| true := ite (g false) (f 1 2 + sum 7 + j 0) 0
| false := f (3 + 4) (f 0 8) + loop
};
2 changes: 1 addition & 1 deletion tests/Anoma/Compilation/positive/test071.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;

main : Nat :=
fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
h@?{b := 4} 1;
8 changes: 4 additions & 4 deletions tests/Casm/Compilation/positive/test006.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ terminating
loop : Nat := loop;

main : Nat :=
if (3 > 0) 1 loop
+ if (2 < 1) loop (if (7 >= 8) loop 1)
+ if (2 > 0 || loop == 0) 1 0
+ if (2 < 0 && loop == 0) 1 0;
ite (3 > 0) 1 loop
+ ite (2 < 1) loop (ite (7 >= 8) loop 1)
+ ite (2 > 0 || loop == 0) 1 0
+ ite (2 < 0 && loop == 0) 1 0;
4 changes: 2 additions & 2 deletions tests/Casm/Compilation/positive/test007.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
lst : List Nat := 0 :: 1 :: nil;

main : Nat :=
if (null lst) 1 0
+ if (null (nil {Nat})) 1 0
ite (null lst) 1 0
+ ite (null (nil {Nat})) 1 0
+ head 1 lst
+ head 0 (tail lst)
+ head 0 (tail (map ((+) 1) lst))
Expand Down
Loading
Loading