Merge if -> ite renaming from stdlib (#2869)

examples/demo/Demo.juvix

@@ -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

examples/midsquare/MidSquareHash.juvix

@@ -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))

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -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;
 

examples/milestone/Bank/Bank.juvix

@@ -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);
@@ -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);
@@ -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:
 ---

examples/milestone/Collatz/Collatz.juvix

@@ -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

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -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));
@@ -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)
@@ -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;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -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;

tests/Anoma/Compilation/positive/test006.juvix

@@ -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;

tests/Anoma/Compilation/positive/test012.juvix

@@ -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))));

tests/Anoma/Compilation/positive/test013.juvix

@@ -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)

tests/Anoma/Compilation/positive/test015.juvix

@@ -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;
 

tests/Anoma/Compilation/positive/test020.juvix

@@ -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)

tests/Anoma/Compilation/positive/test021.juvix

@@ -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)));

tests/Anoma/Compilation/positive/test023.juvix

@@ -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;

tests/Anoma/Compilation/positive/test024.juvix

@@ -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

tests/Anoma/Compilation/positive/test025.juvix

@@ -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))

tests/Anoma/Compilation/positive/test028.juvix

@@ -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;

tests/Anoma/Compilation/positive/test032.juvix

@@ -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 :=
@@ -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

tests/Anoma/Compilation/positive/test034.juvix

@@ -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)

tests/Anoma/Compilation/positive/test060.juvix

@@ -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;

tests/Anoma/Compilation/positive/test064.juvix

@@ -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;
@@ -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
       };

tests/Anoma/Compilation/positive/test071.juvix

@@ -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;

tests/Casm/Compilation/positive/test006.juvix

@@ -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;

tests/Casm/Compilation/positive/test007.juvix

@@ -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))