Add do notation (#2937)

- Closes #2355
- Depends on #2943 

Example:
```
minusOne : Nat -> Maybe Nat
  | zero := nothing
  | (suc n) := just n;


minusThree (n : Nat) : Maybe Nat :=
  do {
    x1 <- minusOne n;
    x2 <- minusOne x1;
    let
      x2' : Nat := x2;
    in
    x3 <- minusOne x2';
    pure x3;
  };
```

src/Juvix/Compiler/Builtins.hs

@@ -13,6 +13,7 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Cairo,
     module Juvix.Compiler.Builtins.Byte,
     module Juvix.Compiler.Builtins.ByteArray,
+    module Juvix.Compiler.Builtins.Monad,
   )
 where
 
@@ -28,5 +29,6 @@ import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int
 import Juvix.Compiler.Builtins.List
 import Juvix.Compiler.Builtins.Maybe
+import Juvix.Compiler.Builtins.Monad
 import Juvix.Compiler.Builtins.Nat
 import Juvix.Compiler.Builtins.String

src/Juvix/Compiler/Builtins/Monad.hs

@@ -0,0 +1,7 @@
+module Juvix.Compiler.Builtins.Monad where
+
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkMonadBind :: forall r. FunctionDef -> Sem r ()
+checkMonadBind _ = return ()

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

@@ -152,6 +152,7 @@ data BuiltinFunction
   | BuiltinFromNat
   | BuiltinFromInt
   | BuiltinSeq
+  | BuiltinMonadBind
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinFunction
@@ -189,6 +190,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
+    BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
   = BuiltinNatPrint
@@ -365,7 +367,26 @@ isNatBuiltin = \case
   BuiltinNatLe -> True
   BuiltinNatLt -> True
   BuiltinNatEq -> True
-  _ -> False
+  --
+  BuiltinBoolIf -> False
+  BuiltinBoolOr -> False
+  BuiltinBoolAnd -> False
+  BuiltinIntEq -> False
+  BuiltinIntPlus -> False
+  BuiltinIntSubNat -> False
+  BuiltinIntNegNat -> False
+  BuiltinIntNeg -> False
+  BuiltinIntMul -> False
+  BuiltinIntDiv -> False
+  BuiltinIntMod -> False
+  BuiltinIntSub -> False
+  BuiltinIntNonNeg -> False
+  BuiltinIntLe -> False
+  BuiltinIntLt -> False
+  BuiltinFromNat -> False
+  BuiltinFromInt -> False
+  BuiltinSeq -> False
+  BuiltinMonadBind -> False
 
 isIntBuiltin :: BuiltinFunction -> Bool
 isIntBuiltin = \case
@@ -381,13 +402,101 @@ isIntBuiltin = \case
   BuiltinIntNonNeg -> True
   BuiltinIntLe -> True
   BuiltinIntLt -> True
-  _ -> False
+  --
+  BuiltinNatPlus -> False
+  BuiltinNatSub -> False
+  BuiltinNatMul -> False
+  BuiltinNatUDiv -> False
+  BuiltinNatDiv -> False
+  BuiltinNatMod -> False
+  BuiltinNatLe -> False
+  BuiltinNatLt -> False
+  BuiltinNatEq -> False
+  BuiltinBoolIf -> False
+  BuiltinBoolOr -> False
+  BuiltinBoolAnd -> False
+  BuiltinFromNat -> False
+  BuiltinFromInt -> False
+  BuiltinSeq -> False
+  BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
-  _ -> False
+  --
+  BuiltinIntEq -> False
+  BuiltinIntPlus -> False
+  BuiltinIntSubNat -> False
+  BuiltinIntNegNat -> False
+  BuiltinIntNeg -> False
+  BuiltinIntMul -> False
+  BuiltinIntDiv -> False
+  BuiltinIntMod -> False
+  BuiltinIntSub -> False
+  BuiltinIntNonNeg -> False
+  BuiltinIntLe -> False
+  BuiltinIntLt -> False
+  BuiltinNatPlus -> False
+  BuiltinNatSub -> False
+  BuiltinNatMul -> False
+  BuiltinNatUDiv -> False
+  BuiltinNatDiv -> False
+  BuiltinNatMod -> False
+  BuiltinNatLe -> False
+  BuiltinNatLt -> False
+  BuiltinNatEq -> False
+  BuiltinBoolIf -> False
+  BuiltinBoolOr -> False
+  BuiltinBoolAnd -> False
+  BuiltinSeq -> False
+  BuiltinMonadBind -> False
 
 isIgnoredBuiltin :: BuiltinFunction -> Bool
-isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f) && not (isCastBuiltin f)
+isIgnoredBuiltin f
+  | spec == explicit = spec
+  | otherwise = impossible
+  where
+    spec :: Bool
+    spec =
+      (not . isNatBuiltin)
+        .&&. (not . isIntBuiltin)
+        .&&. (not . isCastBuiltin)
+        .&&. (/= BuiltinMonadBind)
+        $ f
+
+    explicit :: Bool
+    explicit = case f of
+      -- Cast
+      BuiltinFromNat -> False
+      BuiltinFromInt -> False
+      -- Int
+      BuiltinIntEq -> False
+      BuiltinIntPlus -> False
+      BuiltinIntSubNat -> False
+      BuiltinIntNegNat -> False
+      BuiltinIntNeg -> False
+      BuiltinIntMul -> False
+      BuiltinIntDiv -> False
+      BuiltinIntMod -> False
+      BuiltinIntSub -> False
+      BuiltinIntNonNeg -> False
+      BuiltinIntLe -> False
+      BuiltinIntLt -> False
+      -- Nat
+      BuiltinNatPlus -> False
+      BuiltinNatSub -> False
+      BuiltinNatMul -> False
+      BuiltinNatUDiv -> False
+      BuiltinNatDiv -> False
+      BuiltinNatMod -> False
+      BuiltinNatLe -> False
+      BuiltinNatLt -> False
+      BuiltinNatEq -> False
+      -- Monad
+      BuiltinMonadBind -> False
+      -- Ignored
+      BuiltinBoolIf -> True
+      BuiltinBoolOr -> True
+      BuiltinBoolAnd -> True
+      BuiltinSeq -> True

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All
     kwCase,
     kwCoercion,
     kwColon,
+    kwDo,
     kwElse,
     kwEnd,
     kwEq,
@@ -51,6 +52,7 @@ import Juvix.Data.Keyword.All
     kwIterator,
     kwLambda,
     kwLeft,
+    kwLeftArrow,
     kwLet,
     kwMapsTo,
     kwModule,
@@ -88,6 +90,7 @@ reservedKeywords =
     kwAxiom,
     kwCase,
     kwColon,
+    kwDo,
     kwElse,
     kwEnd,
     kwHiding,
@@ -97,6 +100,7 @@ reservedKeywords =
     kwIn,
     kwInductive,
     kwLambda,
+    kwLeftArrow,
     kwLet,
     kwModule,
     kwOf,