Add builtin if

```
builtin boolean-if
if : {A : Type} → Bool → A → A → A;
if true x _ := x;
if false _ x := x;
```

This allows a backend to translate if directly, so that only one branch
is evalutated.

An example compilation of if is given for the legacy backend for testing.

c-runtime/builtins/bool.h

@@ -16,4 +16,6 @@ bool is_prim_false(prim_bool b) {
     return b == prim_false;
 }
 
+#define prim_if(b, ifThen, ifElse) (b ? ifThen : ifElse)
+
 #endif // BOOL_H_

src/Juvix/Compiler/Abstract/Extra/Functions.hs

@@ -237,28 +237,45 @@ toApplicationArg p =
       PatternVariable v -> ApplicationArg Explicit (toExpression v)
       PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
       PatternEmpty -> impossible
-      PatternWildcard _ -> error "TODO"
+      PatternWildcard _ ->
+        ApplicationArg
+          Explicit
+          ( ExpressionHole
+              ( Hole
+                  { _holeId = error "hole with no id",
+                    _holeLoc = error "hole with no location"
+                  }
+              )
+          )
 
 clauseLhsAsExpression :: FunctionClause -> Expression
 clauseLhsAsExpression cl =
   foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
 
-infixr 0 -->
-
-(-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
-(-->) a b =
+expressionArrow :: (IsExpression a, IsExpression b) => IsImplicit -> a -> b -> Expression
+expressionArrow isImplicit a b =
   ExpressionFunction
     ( Function
         ( FunctionParameter
             { _paramName = Nothing,
               _paramUsage = UsageOmega,
-              _paramImplicit = Explicit,
+              _paramImplicit = isImplicit,
               _paramType = toExpression a
             }
         )
         (toExpression b)
     )
 
+infixr 0 <>-->
+
+(<>-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+(<>-->) = expressionArrow Implicit
+
+infixr 0 -->
+
+(-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+(-->) = expressionArrow Explicit
+
 infix 4 ===
 
 (===) :: (IsExpression a, IsExpression b) => a -> b -> Bool
@@ -291,3 +308,14 @@ freshVar n = do
         _namePretty = n,
         _nameLoc = error "freshVar with no location"
       }
+
+freshHole :: Member NameIdGen r => Sem r Expression
+freshHole = do
+  uid <- freshNameId
+  return $
+    ExpressionHole
+      ( Hole
+          { _holeId = uid,
+            _holeLoc = error "freshHole with no location"
+          }
+      )

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -253,6 +253,7 @@ registerBuiltinFunction ::
   Sem r ()
 registerBuiltinFunction d = \case
   BuiltinNaturalPlus -> registerNaturalPlus d
+  BuiltinBooleanIf -> registerIf d
 
 registerBuiltinAxiom ::
   Members '[InfoTableBuilder, Error ScoperError, Builtins] r =>

src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs

@@ -25,6 +25,7 @@ builtinAxiomName = \case
 builtinFunctionName :: BuiltinFunction -> Maybe Text
 builtinFunctionName = \case
   BuiltinNaturalPlus -> Just natplus
+  BuiltinBooleanIf -> Just boolif
 
 builtinName :: BuiltinPrim -> Maybe Text
 builtinName = \case

src/Juvix/Compiler/Backend/C/Data/CNames.hs

@@ -38,6 +38,9 @@ ioseq = primPrefix "sequence"
 natplus :: Text
 natplus = primPrefix "natplus"
 
+boolif :: Text
+boolif = primPrefix "if"
+
 funField :: Text
 funField = "fun"
 

src/Juvix/Compiler/Builtins/Boolean.hs

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Builtins.Boolean where
 
+import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Abstract.Extra
 import Juvix.Compiler.Abstract.Pretty
 import Juvix.Compiler.Builtins.Effect
@@ -29,3 +30,37 @@ registerFalse d@InductiveConstructorDef {..} = do
   boolTy <- getBuiltinName (getLoc d) BuiltinBoolean
   unless (ctorTy === boolTy) (error $ "false has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
   registerBuiltin BuiltinBooleanFalse ctorFalse
+
+registerIf :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIf f = do
+  boolean <- getBuiltinName (getLoc f) BuiltinBoolean
+  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBooleanTrue
+  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBooleanFalse
+  vart <- freshVar "t"
+  let if_ = f ^. funDefName
+      ty = f ^. funDefTypeSig
+      freeTVars = HashSet.fromList [vart]
+      u = ExpressionUniverse (Universe {_universeLevel = Nothing, _universeLoc = error "Universe with no location"})
+  unless (((u <>--> boolean --> vart --> vart --> vart) ==% ty) freeTVars) (error "Boolean if has the wrong type signature")
+  registerBuiltin BuiltinBooleanIf if_
+  vare <- freshVar "e"
+  hole <- freshHole
+  let e = toExpression vare
+      freeVars = HashSet.fromList [vare]
+      (=%) :: (IsExpression a, IsExpression b) => a -> b -> Bool
+      a =% b = (a ==% b) freeVars
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (if_ @@ true_ @@ e @@ hole, e),
+          (if_ @@ false_ @@ hole @@ e, e)
+        ]
+      clauses :: [(Expression, Expression)]
+      clauses =
+        [ (clauseLhsAsExpression c, c ^. clauseBody)
+          | c <- toList (f ^. funDefClauses)
+        ]
+  case zipExactMay exClauses clauses of
+    Nothing -> error "Boolean if has the wrong number of clauses"
+    Just z -> forM_ z $ \((exLhs, exBody), (lhs, body)) -> do
+      unless (exLhs =% lhs) (error "clause lhs does not match")
+      unless (exBody =% body) (error $ "clause body does not match " <> ppTrace exBody <> " | " <> ppTrace body)

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -63,13 +63,15 @@ instance Hashable BuiltinConstructor
 
 data BuiltinFunction
   = BuiltinNaturalPlus
+  | BuiltinBooleanIf
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
 
 instance Hashable BuiltinFunction
 
 instance Pretty BuiltinFunction where
   pretty = \case
     BuiltinNaturalPlus -> Str.naturalPlus
+    BuiltinBooleanIf -> Str.booleanIf
 
 data BuiltinAxiom
   = BuiltinNaturalPrint

src/Juvix/Extra/Strings.hs

@@ -107,6 +107,9 @@ naturalPrint = "natural-print"
 naturalPlus :: IsString s => s
 naturalPlus = "natural-plus"
 
+booleanIf :: IsString s => s
+booleanIf = "boolean-if"
+
 builtin :: IsString s => s
 builtin = "builtin"
 

tests/positive/BuiltinsBool.juvix

@@ -6,4 +6,9 @@ inductive Bool {
   false : Bool;
 };
 
+builtin boolean-if
+if : {A : Type} → Bool → A → A → A;
+if true t _ := t;
+if false _ e := e;
+
 end;

tests/positive/MiniC/Builtins/Input.juvix

@@ -6,6 +6,11 @@ inductive Bool {
   false : Bool;
 };
 
+builtin boolean-if
+if : {A : Type} → Bool → A → A → A;
+if true t _ := t;
+if false _ e := e;
+
 builtin natural
 inductive ℕ {
  zero : ℕ;
@@ -32,6 +37,12 @@ plusOne := suc;
 someLiteral : _;
 someLiteral := 123;
 
+infix 4 ==;
+== : ℕ → ℕ → Bool;
+== zero zero := true;
+== (suc n) (suc m) := n == m;
+== _ _ := false;
+
 builtin IO axiom IO : Type;
 
 infixl 1 >>;
@@ -42,6 +53,10 @@ main : IO;
 main := printNat (boolToNat true)
      >> printNat (boolToNat false)
      >> printNat (mult 3 (2 + 2))
-     >> printNat 2;
+     >> printNat 2
+     >> printNat (if (1 == 2) 100 200)
+     >> printNat (if (1 == 1) 300 400)
+     >> if (1 == 2) (printNat 500) (printNat 600)
+     >> if (1 == 1) (printNat 700) (printNat 800);
 
 end;

tests/positive/MiniC/Builtins/expected.golden

@@ -2,3 +2,7 @@
 0
 12
 2
+200
+300
+600
+700