From 9d635d4d15b7eb9123e46e781c5fdf8fd5c53277 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 5 Aug 2024 14:03:49 +0200
Subject: [PATCH 1/7] syntax

---
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 113 ++++++++++++++++++
 src/Juvix/Compiler/Concrete/Print/Base.hs     |  33 ++++-
 .../FromParsed/Analysis/Scoping.hs            |   8 ++
 3 files changed, 153 insertions(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index bf233a2418..79d0df3425 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -55,6 +55,11 @@ type family FieldArgIxType s = res | res -> s where
   FieldArgIxType 'Parsed = ()
   FieldArgIxType 'Scoped = Int
 
+type DoBindIdenType :: Stage -> GHCType
+type family DoBindIdenType s = res | res -> s where
+  DoBindIdenType 'Parsed = ()
+  DoBindIdenType 'Scoped = ScopedIden
+
 type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHCType
 type family SideIfBranchConditionType s k = res where
   SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
@@ -1706,6 +1711,32 @@ deriving stock instance Ord (LetStatement 'Parsed)
 
 deriving stock instance Ord (LetStatement 'Scoped)
 
+data DoLet (s :: Stage) = DoLet
+  { _doLetKw :: KeywordRef,
+    _doLetFunDefs :: NonEmpty (LetStatement s)
+  }
+  deriving stock (Generic)
+
+instance Serialize (DoLet 'Scoped)
+
+instance NFData (DoLet 'Scoped)
+
+instance Serialize (DoLet 'Parsed)
+
+instance NFData (DoLet 'Parsed)
+
+deriving stock instance Show (DoLet 'Parsed)
+
+deriving stock instance Show (DoLet 'Scoped)
+
+deriving stock instance Eq (DoLet 'Parsed)
+
+deriving stock instance Eq (DoLet 'Scoped)
+
+deriving stock instance Ord (DoLet 'Parsed)
+
+deriving stock instance Ord (DoLet 'Scoped)
+
 data Let (s :: Stage) = Let
   { _letKw :: KeywordRef,
     _letInKw :: Irrelevant KeywordRef,
@@ -2454,6 +2485,87 @@ deriving stock instance Ord (RecordStatement 'Parsed)
 
 deriving stock instance Ord (RecordStatement 'Scoped)
 
+data Do (s :: Stage) = Do
+  { _doKeyword :: Irrelevant KeywordRef,
+    _doDelims :: Irrelevant (KeywordRef, KeywordRef),
+    _doBindIden :: DoBindIdenType s,
+    _doStatements :: [DoStatement s]
+  }
+  deriving stock (Generic)
+
+instance Serialize (Do 'Parsed)
+
+instance Serialize (Do 'Scoped)
+
+instance NFData (Do 'Scoped)
+
+instance NFData (Do 'Parsed)
+
+deriving stock instance Show (Do 'Parsed)
+
+deriving stock instance Show (Do 'Scoped)
+
+deriving stock instance Eq (Do 'Parsed)
+
+deriving stock instance Eq (Do 'Scoped)
+
+deriving stock instance Ord (Do 'Parsed)
+
+deriving stock instance Ord (Do 'Scoped)
+
+data DoBind (s :: Stage) = DoBind
+  { _doBindPattern :: PatternParensType s,
+    _doBindArrowKw :: Irrelevant KeywordRef,
+    _doBindExpression :: ExpressionType s
+  }
+  deriving stock (Generic)
+
+instance Serialize (DoBind 'Scoped)
+
+instance Serialize (DoBind 'Parsed)
+
+instance NFData (DoBind 'Scoped)
+
+instance NFData (DoBind 'Parsed)
+
+deriving stock instance Show (DoBind 'Parsed)
+
+deriving stock instance Show (DoBind 'Scoped)
+
+deriving stock instance Eq (DoBind 'Parsed)
+
+deriving stock instance Eq (DoBind 'Scoped)
+
+deriving stock instance Ord (DoBind 'Parsed)
+
+deriving stock instance Ord (DoBind 'Scoped)
+
+data DoStatement (s :: Stage)
+  = DoStatementBind (DoBind s)
+  | DoStatementLet (DoLet s)
+  | DoStatementExpression (ExpressionType s)
+  deriving stock (Generic)
+
+instance Serialize (DoStatement 'Scoped)
+
+instance Serialize (DoStatement 'Parsed)
+
+instance NFData (DoStatement 'Scoped)
+
+instance NFData (DoStatement 'Parsed)
+
+deriving stock instance Show (DoStatement 'Parsed)
+
+deriving stock instance Show (DoStatement 'Scoped)
+
+deriving stock instance Eq (DoStatement 'Parsed)
+
+deriving stock instance Eq (DoStatement 'Scoped)
+
+deriving stock instance Ord (DoStatement 'Parsed)
+
+deriving stock instance Ord (DoStatement 'Scoped)
+
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
   = AtomIdentifier (IdentifierType s)
@@ -2465,6 +2577,7 @@ data ExpressionAtom (s :: Stage)
   | AtomInstanceHole (HoleType s)
   | AtomDoubleBraces (DoubleBracesExpression s)
   | AtomBraces (WithLoc (ExpressionType s))
+  | AtomDo (Do s)
   | AtomLet (Let s)
   | AtomRecordUpdate (RecordUpdate s)
   | AtomUniverse Universe
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index a50648774a..0e2fe505a4 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -42,7 +42,9 @@ import Juvix.Prelude.Pretty qualified as P
 --- * the body of a `Top` iterator,
 --- * the else branch body of a `Top` if expression,
 --- * the last branch body of a `Top` case expresssion.
-data IsTop = Top | NotTop
+data IsTop
+  = Top
+  | NotTop
 
 type PrettyPrintingMaybe a = forall r. (Members '[ExactPrint, Reader Options] r) => a -> Maybe (Sem r ())
 
@@ -396,10 +398,39 @@ instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where
     let (l, r) = _doubleBracesDelims ^. unIrrelevant
     ppCode l <> ppTopExpressionType _doubleBracesExpression <> ppCode r
 
+instance (SingI s) => PrettyPrint (DoLet s) where
+  ppCode DoLet {..} = do
+    let letFunDefs' = blockIndent (ppBlock _doLetFunDefs)
+    ppCode _doLetKw
+      <+> letFunDefs'
+
+instance (SingI s) => PrettyPrint (DoBind s) where
+  ppCode DoBind {..} = do
+    ppPatternParensType _doBindPattern
+      <+> ppCode _doBindArrowKw
+      <+> ppTopExpressionType _doBindExpression
+
+instance (SingI s) => PrettyPrint (DoStatement s) where
+  ppCode = \case
+    DoStatementExpression e -> ppExpressionType e
+    DoStatementLet l -> ppCode l
+    DoStatementBind l -> ppCode l
+
+instance (SingI s) => PrettyPrint (Do s) where
+  ppCode Do {..} = do
+    let dokw = ppCode _doKeyword
+        (openbr, closebr) = over both ppCode (_doDelims ^. unIrrelevant)
+        statements' = ppBlock _doStatements
+    dokw
+      <+> openbr
+      <+> statements'
+      <+> closebr
+
 instance (SingI s) => PrettyPrint (ExpressionAtom s) where
   ppCode = \case
     AtomIdentifier n -> ppIdentifierType n
     AtomLambda l -> ppCode l
+    AtomDo l -> ppCode l
     AtomLet lb -> ppLet NotTop lb
     AtomCase c -> ppCase NotTop c
     AtomIf c -> ppIf NotTop c
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 7ccf1414f3..41327ab0fd 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -2366,6 +2366,13 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do
         ..
       }
 
+checkDo ::
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  Do 'Parsed ->
+  Sem r (Do 'Scoped)
+checkDo Do {..} = do
+  undefined
+
 checkCase ::
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
   Case 'Parsed ->
@@ -2622,6 +2629,7 @@ checkExpressionAtom ::
 checkExpressionAtom e = case e of
   AtomIdentifier n -> pure . AtomIdentifier <$> checkScopedIden n
   AtomLambda lam -> pure . AtomLambda <$> checkLambda lam
+  AtomDo a -> pure . AtomDo <$> checkDo a
   AtomCase c -> pure . AtomCase <$> checkCase c
   AtomIf c -> pure . AtomIf <$> checkIf c
   AtomLet letBlock -> pure . AtomLet <$> checkLet letBlock

From d25d37c5b5cf3b6d7cae8e10ff58f9de6f276251 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 5 Aug 2024 17:43:15 +0200
Subject: [PATCH 2/7] scoping

---
 .../FromParsed/Analysis/Scoping.hs            | 51 ++++++++++++++++++-
 src/Juvix/Compiler/Core/Keywords.hs           |  4 +-
 .../Compiler/Core/Translation/FromSource.hs   |  2 +-
 src/Juvix/Data/Keyword/All.hs                 |  4 +-
 src/Juvix/Extra/Strings.hs                    |  4 +-
 5 files changed, 57 insertions(+), 8 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 41327ab0fd..f25ff00cb1 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -20,6 +20,7 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra (recordNameSignatureByIndex)
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Gen qualified as G
+import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Pretty (ppTrace)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
@@ -28,6 +29,7 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Compiler.Store.Scoped.Language as Store
 import Juvix.Data.FixityInfo qualified as FI
+import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude
 
 scopeCheck ::
@@ -2366,12 +2368,59 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do
         ..
       }
 
+checkDoBind ::
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  DoBind 'Parsed ->
+  Sem r (DoBind 'Scoped)
+checkDoBind DoBind {..} = do
+  expr' <- checkParseExpressionAtoms _doBindExpression
+  pat' <- checkParsePatternAtoms _doBindPattern
+  return
+    DoBind
+      { _doBindArrowKw,
+        _doBindPattern = pat',
+        _doBindExpression = expr'
+      }
+
+checkDoLet ::
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  DoLet 'Parsed ->
+  Sem r (DoLet 'Scoped)
+checkDoLet DoLet {..} = do
+  defs' <- checkLetStatements _doLetFunDefs
+  return
+    DoLet
+      { _doLetKw,
+        _doLetFunDefs = defs'
+      }
+
+checkDoStatement ::
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  DoStatement 'Parsed ->
+  Sem r (DoStatement 'Scoped)
+checkDoStatement = \case
+  DoStatementExpression e -> DoStatementExpression <$> checkParseExpressionAtoms e
+  DoStatementBind b -> DoStatementBind <$> checkDoBind b
+  DoStatementLet b -> DoStatementLet <$> checkDoLet b
+
 checkDo ::
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
   Do 'Parsed ->
   Sem r (Do 'Scoped)
 checkDo Do {..} = do
-  undefined
+  let bindSym :: Symbol =
+        run
+          . runReader (getLoc _doKeyword)
+          $ Gen.symbol Str.bindOperator
+  bindIden <- checkScopedIden (NameUnqualified bindSym)
+  stmts' <- mapM checkDoStatement _doStatements
+  return
+    Do
+      { _doStatements = stmts',
+        _doBindIden = bindIden,
+        _doKeyword,
+        _doDelims
+      }
 
 checkCase ::
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs
index 6f1d8eac29..3f5a522cdc 100644
--- a/src/Juvix/Compiler/Core/Keywords.hs
+++ b/src/Juvix/Compiler/Core/Keywords.hs
@@ -16,7 +16,7 @@ import Juvix.Data.Keyword.All
     kwAnomaVerifyWithMessage,
     kwAny,
     kwAssign,
-    kwBind,
+    kwBindOperator,
     kwBottom,
     kwBuiltin,
     kwByteArrayFromListByte,
@@ -105,7 +105,7 @@ allKeywords =
     kwLe,
     kwGt,
     kwGe,
-    kwBind,
+    kwBindOperator,
     kwSeq,
     kwSeqq,
     kwTrace,
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 26c8633064..acc1f98a21 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -353,7 +353,7 @@ bindExpr' ::
   Node ->
   ParsecS r Node
 bindExpr' varsNum vars node = do
-  kw kwBind
+  kw kwBindOperator
   node' <- cmpExpr varsNum vars
   ioExpr' varsNum vars (mkConstr Info.empty (BuiltinTag TagBind) [node, node'])
 
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index e8697ff61e..806f103d32 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -250,8 +250,8 @@ kwAtoi = asciiKw Str.instrStrToInt
 kwStrcat :: Keyword
 kwStrcat = asciiKw Str.instrStrConcat
 
-kwBind :: Keyword
-kwBind = asciiKw Str.bind
+kwBindOperator :: Keyword
+kwBindOperator = asciiKw Str.bindOperator
 
 kwSeq :: Keyword
 kwSeq = asciiKw Str.seq_
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 7fe7156802..6d0acb0300 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -461,8 +461,8 @@ greater = ">"
 greaterEqual :: (IsString s) => s
 greaterEqual = ">="
 
-bind :: (IsString s) => s
-bind = ">>="
+bindOperator :: (IsString s) => s
+bindOperator = ">>="
 
 seq_ :: (IsString s) => s
 seq_ = ">>"

From cd0349f9756ccd303dd4d89823ed7ead4314d392 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 6 Aug 2024 10:56:04 +0200
Subject: [PATCH 3/7] parsing and desugaring

---
 src/Juvix/Compiler/Concrete/Keywords.hs       |  4 +
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 38 +++++++-
 .../Concrete/Language/IsApeInstances.hs       |  1 +
 src/Juvix/Compiler/Concrete/Print/Base.hs     |  3 +-
 .../FromParsed/Analysis/Scoping.hs            | 15 +++-
 .../FromParsed/Analysis/Scoping/Error.hs      |  2 +
 .../Analysis/Scoping/Error/Types.hs           | 20 +++++
 .../Concrete/Translation/FromSource.hs        | 37 ++++++++
 src/Juvix/Compiler/Internal/Extra/Base.hs     | 14 +++
 .../Internal/Translation/FromConcrete.hs      | 87 ++++++++++++++++---
 src/Juvix/Data/Keyword/All.hs                 |  6 ++
 src/Juvix/Extra/Strings.hs                    |  9 ++
 12 files changed, 218 insertions(+), 18 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs
index b60bd2c9ad..a254061802 100644
--- a/src/Juvix/Compiler/Concrete/Keywords.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 79d0df3425..7497502869 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -1470,6 +1470,7 @@ data Expression
   | ExpressionIf (If 'Scoped)
   | ExpressionLambda (Lambda 'Scoped)
   | ExpressionLet (Let 'Scoped)
+  | ExpressionDo (Do 'Scoped)
   | ExpressionUniverse Universe
   | ExpressionLiteral LiteralLoc
   | ExpressionFunction (Function 'Scoped)
@@ -1712,8 +1713,8 @@ deriving stock instance Ord (LetStatement 'Parsed)
 deriving stock instance Ord (LetStatement 'Scoped)
 
 data DoLet (s :: Stage) = DoLet
-  { _doLetKw :: KeywordRef,
-    _doLetFunDefs :: NonEmpty (LetStatement s)
+  { _doLetKw :: Irrelevant KeywordRef,
+    _doLetStatements :: NonEmpty (LetStatement s)
   }
   deriving stock (Generic)
 
@@ -2489,7 +2490,7 @@ data Do (s :: Stage) = Do
   { _doKeyword :: Irrelevant KeywordRef,
     _doDelims :: Irrelevant (KeywordRef, KeywordRef),
     _doBindIden :: DoBindIdenType s,
-    _doStatements :: [DoStatement s]
+    _doStatements :: NonEmpty (DoStatement s)
   }
   deriving stock (Generic)
 
@@ -2910,6 +2911,28 @@ fixityPrecAbove = fixityFieldHelper fixityFieldsPrecAbove
 fixityPrecBelow :: SimpleGetter (ParsedFixityInfo s) (Maybe [SymbolType s])
 fixityPrecBelow = fixityFieldHelper fixityFieldsPrecBelow
 
+instance (SingI s) => HasLoc (LetStatement s) where
+  getLoc = \case
+    LetOpen o -> getLoc o
+    LetAliasDef d -> getLoc d
+    LetFunctionDef d -> getLoc d
+
+instance (SingI s) => HasLoc (DoBind s) where
+  getLoc DoBind {..} =
+    getLocPatternParensType _doBindPattern
+      <> getLocExpressionType _doBindExpression
+
+instance (SingI s) => HasLoc (DoLet s) where
+  getLoc DoLet {..} =
+    getLoc _doLetKw
+      <> getLoc (last _doLetStatements)
+
+instance (SingI s) => HasLoc (DoStatement s) where
+  getLoc = \case
+    DoStatementExpression e -> getLocExpressionType e
+    DoStatementBind b -> getLoc b
+    DoStatementLet b -> getLoc b
+
 instance (SingI s) => HasLoc (AliasDef s) where
   getLoc AliasDef {..} = getLoc _aliasDefSyntaxKw <> getLocIdentifierType _aliasDefAsName
 
@@ -2950,10 +2973,14 @@ instance HasAtomicity (NamedApplication s) where
 instance HasAtomicity (NamedApplicationNew s) where
   atomicity = const (Aggregate updateFixity)
 
+instance HasAtomicity (Do s) where
+  atomicity = const Atom
+
 instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIdentifier {} -> Atom
     ExpressionHole {} -> Atom
+    ExpressionDo d -> atomicity d
     ExpressionInstanceHole {} -> Atom
     ExpressionParensIdentifier {} -> Atom
     ExpressionApplication {} -> Aggregate appFixity
@@ -3147,6 +3174,10 @@ instance HasLoc (DoubleBracesExpression s) where
 instance HasAtomicity (DoubleBracesExpression s) where
   atomicity = const Atom
 
+instance HasLoc (Do s) where
+  getLoc Do {..} =
+    getLoc _doKeyword <> getLoc (_doDelims ^. unIrrelevant . _2)
+
 instance HasLoc Expression where
   getLoc = \case
     ExpressionIdentifier i -> getLoc i
@@ -3159,6 +3190,7 @@ instance HasLoc Expression where
     ExpressionCase i -> getLoc i
     ExpressionIf x -> getLoc x
     ExpressionLet i -> getLoc i
+    ExpressionDo i -> getLoc i
     ExpressionUniverse i -> getLoc i
     ExpressionLiteral i -> getLoc i
     ExpressionFunction i -> getLoc i
diff --git a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
index 3cd65514e6..cb7a551f20 100644
--- a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
+++ b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
@@ -157,6 +157,7 @@ instance IsApe Expression ApeLeaf where
     ExpressionParensIdentifier {} -> leaf
     ExpressionIdentifier {} -> leaf
     ExpressionList {} -> leaf
+    ExpressionDo {} -> leaf
     ExpressionCase {} -> leaf
     ExpressionIf {} -> leaf
     ExpressionLambda {} -> leaf
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 0e2fe505a4..4bf607efce 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -400,7 +400,7 @@ instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where
 
 instance (SingI s) => PrettyPrint (DoLet s) where
   ppCode DoLet {..} = do
-    let letFunDefs' = blockIndent (ppBlock _doLetFunDefs)
+    let letFunDefs' = blockIndent (ppBlock _doLetStatements)
     ppCode _doLetKw
       <+> letFunDefs'
 
@@ -957,6 +957,7 @@ instance PrettyPrint Expression where
     ExpressionPostfixApplication a -> ppCode a
     ExpressionLambda l -> ppCode l
     ExpressionLet lb -> ppLet NotTop lb
+    ExpressionDo d -> ppCode d
     ExpressionUniverse u -> ppCode u
     ExpressionLiteral l -> ppCode l
     ExpressionFunction f -> ppCode f
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index f25ff00cb1..77ad466eeb 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -2375,6 +2375,7 @@ checkDoBind ::
 checkDoBind DoBind {..} = do
   expr' <- checkParseExpressionAtoms _doBindExpression
   pat' <- checkParsePatternAtoms _doBindPattern
+  -- TODO check no implicit pattern
   return
     DoBind
       { _doBindArrowKw,
@@ -2387,11 +2388,11 @@ checkDoLet ::
   DoLet 'Parsed ->
   Sem r (DoLet 'Scoped)
 checkDoLet DoLet {..} = do
-  defs' <- checkLetStatements _doLetFunDefs
+  defs' <- checkLetStatements _doLetStatements
   return
     DoLet
       { _doLetKw,
-        _doLetFunDefs = defs'
+        _doLetStatements = defs'
       }
 
 checkDoStatement ::
@@ -3280,6 +3281,7 @@ parseTerm =
     <|> parseList
     <|> parseLiteral
     <|> parseLet
+    <|> parseDo
     <|> parseIterator
     <|> parseDoubleBraces
     <|> parseBraces
@@ -3373,6 +3375,7 @@ parseTerm =
         namedApp s = case s of
           AtomNamedApplicationNew u -> Just u
           _ -> Nothing
+
     parseLet :: Parse Expression
     parseLet = ExpressionLet <$> P.token letBlock mempty
       where
@@ -3381,6 +3384,14 @@ parseTerm =
           AtomLet u -> Just u
           _ -> Nothing
 
+    parseDo :: Parse Expression
+    parseDo = ExpressionDo <$> P.token letBlock mempty
+      where
+        letBlock :: ExpressionAtom 'Scoped -> Maybe (Do 'Scoped)
+        letBlock s = case s of
+          AtomDo u -> Just u
+          _ -> Nothing
+
     parseIterator :: Parse Expression
     parseIterator = ExpressionIterator <$> P.token iterator mempty
       where
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
index 3dcd846058..81cfab60b7 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
@@ -59,6 +59,7 @@ data ScoperError
   | ErrBuiltinAlreadyDefined BuiltinAlreadyDefined
   | ErrBuiltinNotDefined BuiltinNotDefined
   | ErrBuiltinErrorMessage BuiltinErrorMessage
+  | ErrDoLastStatement DoLastStatement
   deriving stock (Generic)
 
 instance ToGenericError ScoperError where
@@ -109,6 +110,7 @@ instance ToGenericError ScoperError where
     ErrBuiltinAlreadyDefined e -> genericError e
     ErrBuiltinNotDefined e -> genericError e
     ErrBuiltinErrorMessage e -> genericError e
+    ErrDoLastStatement e -> genericError e
 
 builtinsErrorMsg :: (Members '[Error ScoperError] r) => Interval -> AnsiText -> Sem r a
 builtinsErrorMsg loc msg =
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
index 380d4b0bde..cc6635bcf6 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
@@ -46,6 +46,26 @@ instance ToGenericError MultipleDeclarations where
             <> line
             <> itemize (map pretty [i1, i2])
 
+newtype DoLastStatement = DoLastStatement
+  { _doLastStatement :: DoStatement 'Scoped
+  }
+
+instance ToGenericError DoLastStatement where
+  genericError DoLastStatement {..} = generr
+    where
+      generr =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = prettyError msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          i = getLoc _doLastStatement
+          msg :: Doc Ann
+          msg =
+            "The last statement of a do block must be an expression"
+
 -- | megaparsec error while resolving infixities.
 newtype InfixError = InfixError
   { _infixErrorAtoms :: ExpressionAtoms 'Scoped
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 8d0c583663..a04bec1062 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -832,6 +832,7 @@ expressionAtom =
       <|> AtomCase <$> case_
       <|> AtomFunction <$> function
       <|> AtomLet <$> letBlock
+      <|> AtomDo <$> doBlock
       <|> AtomFunArrow <$> kw kwRightArrow
       <|> AtomHole <$> hole
       <|> AtomParens <$> parens parseExpressionAtoms
@@ -1164,6 +1165,42 @@ letStatement =
     <|> LetAliasDef <$> (kw kwSyntax >>= aliasDef)
     <|> LetOpen <$> openModule
 
+doBind :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoBind 'Parsed)
+doBind = do
+  (_doBindPattern, _doBindArrowKw) <- P.try $ do
+    pat <- parsePatternAtoms
+    arrowkw <- Irrelevant <$> kw kwLeftArrow
+    return (pat, arrowkw)
+  _doBindExpression <- parseExpressionAtoms
+  return DoBind {..}
+
+doLet :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoLet 'Parsed)
+doLet = do
+  _doLetKw <- Irrelevant <$> kw kwLet
+  -- TODO think about this P.try
+  _doLetStatements <- P.sepEndBy1 (P.try letStatement) semicolon
+  return DoLet {..}
+
+doStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoStatement 'Parsed)
+doStatement =
+  DoStatementLet <$> doLet
+    <|> DoStatementBind <$> doBind
+    <|> DoStatementExpression <$> parseExpressionAtoms
+
+doBlock :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Do 'Parsed)
+doBlock = do
+  _doKeyword <- Irrelevant <$> kw kwDo
+  lbr <- kw delimBraceL
+  _doStatements <- P.sepEndBy1 doStatement semicolon
+  rbr <- kw delimBraceR
+  let
+  return
+    Do
+      { _doBindIden = (),
+        _doDelims = Irrelevant (lbr, rbr),
+        ..
+      }
+
 letBlock :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Let 'Parsed)
 letBlock = do
   _letKw <- kw kwLet
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index 2d65b21405..dfef064e61 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -618,6 +618,20 @@ infixl 9 @@
 (@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression
 a @@ b = toExpression (Application (toExpression a) (toExpression b) Explicit)
 
+-- | \{p := b}
+(==>) :: (IsExpression a) => PatternArg -> a -> Expression
+p ==> b =
+  ExpressionLambda
+    Lambda
+      { _lambdaClauses =
+          pure
+            LambdaClause
+              { _lambdaPatterns = pure p,
+                _lambdaBody = toExpression b
+              },
+        _lambdaType = Nothing
+      }
+
 freshFunVar :: (Member NameIdGen r) => Interval -> Text -> Sem r VarName
 freshFunVar i n = set nameKind KNameFunction <$> freshVar i n
 
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index b2edf6ea9b..f7a4b01851 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -810,6 +810,7 @@ goExpression = \case
   ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b))
   ExpressionDoubleBraces b -> throw (ErrDanglingDoubleBrace (DanglingDoubleBrace b))
   ExpressionLet l -> goLet l
+  ExpressionDo l -> goDo l
   ExpressionList l -> goList l
   ExpressionUniverse uni -> return (Internal.ExpressionUniverse (goUniverse uni))
   ExpressionFunction func -> Internal.ExpressionFunction <$> goFunction func
@@ -1027,18 +1028,6 @@ goExpression = \case
         Just _letClauses -> Internal.ExpressionLet Internal.Let {..}
         Nothing -> _letExpression
 
-    goLetFunDefs :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.LetClause]
-    goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetStatements clauses
-      where
-        preLetStatements :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.PreLetStatement]
-        preLetStatements cl = mapMaybeM preLetStatement (toList cl)
-          where
-            preLetStatement :: LetStatement 'Scoped -> Sem r (Maybe Internal.PreLetStatement)
-            preLetStatement = \case
-              LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goFunctionDef f
-              LetAliasDef {} -> return Nothing
-              LetOpen {} -> return Nothing
-
     goApplicationArg :: Expression -> Sem r Internal.ApplicationArg
     goApplicationArg arg =
       let (e, i) = case arg of
@@ -1109,6 +1098,80 @@ goExpression = \case
         mkApp :: Internal.Expression -> Internal.Expression -> Internal.Expression
         mkApp a1 a2 = Internal.ExpressionApplication $ Internal.Application a1 a2 Explicit
 
+goLetFunDefs ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  NonEmpty (LetStatement 'Scoped) ->
+  Sem r [Internal.LetClause]
+goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetStatements clauses
+  where
+    preLetStatements :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.PreLetStatement]
+    preLetStatements cl = mapMaybeM preLetStatement (toList cl)
+      where
+        preLetStatement :: LetStatement 'Scoped -> Sem r (Maybe Internal.PreLetStatement)
+        preLetStatement = \case
+          LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goFunctionDef f
+          LetAliasDef {} -> return Nothing
+          LetOpen {} -> return Nothing
+
+goDo ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  Do 'Scoped ->
+  Sem r Internal.Expression
+goDo Do {..} = goStatements _doStatements
+  where
+    goStatements :: NonEmpty (DoStatement 'Scoped) -> Sem r Internal.Expression
+    goStatements (l :| ss) = case nonEmpty ss of
+      Nothing -> goLastStatement l
+      Just ss1 -> do
+        ss1' <- goStatements ss1
+        case l of
+          DoStatementExpression e -> goDoExpression e ss1'
+          DoStatementBind b -> goDoBind b ss1'
+          DoStatementLet b -> goDoLet b ss1'
+
+    -- l >>= \{_ := r}
+    goDoExpression :: Expression -> Internal.Expression -> Sem r Internal.Expression
+    goDoExpression l r = do
+      let p =
+            PatternArg
+              { _patternArgIsImplicit = Explicit,
+                _patternArgName = Nothing,
+                _patternArgPattern = PatternWildcard (Wildcard (getLoc l <> getLoc r))
+              }
+      goDoBindHelper p l r
+
+    goDoLet :: DoLet 'Scoped -> Internal.Expression -> Sem r Internal.Expression
+    goDoLet DoLet {..} r = do
+      defs <- goLetFunDefs _doLetStatements
+      return $ case nonEmpty defs of
+        Nothing -> r
+        Just defs1 ->
+          Internal.ExpressionLet
+            Internal.Let
+              { _letClauses = defs1,
+                _letExpression = r
+              }
+
+    goDoBind :: DoBind 'Scoped -> Internal.Expression -> Sem r Internal.Expression
+    goDoBind DoBind {..} r = goDoBindHelper _doBindPattern _doBindExpression r
+
+    bindIden :: Internal.Expression
+    bindIden = Internal.toExpression (goName (_doBindIden ^. scopedIdenFinal))
+
+    -- l >>= \{p := r}
+    goDoBindHelper :: PatternArg -> Expression -> Internal.Expression -> Sem r Internal.Expression
+    goDoBindHelper p l r = do
+      p' <- goPatternArg p
+      l' <- goExpression l
+      return (bindIden Internal.@@ l' Internal.@@ (p' Internal.==> r))
+
+    goLastStatement :: DoStatement 'Scoped -> Sem r Internal.Expression
+    goLastStatement = \case
+      DoStatementExpression e -> goExpression e
+      d -> throw (ErrDoLastStatement (DoLastStatement d))
+
 goCase :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Case 'Scoped -> Sem r Internal.Case
 goCase c = do
   _caseExpression <- goExpression (c ^. caseExpression)
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index 806f103d32..9f1d31e6de 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -88,6 +88,9 @@ kwPublic = asciiKw Str.public
 kwRightArrow :: Keyword
 kwRightArrow = unicodeKw Str.toAscii Str.toUnicode
 
+kwLeftArrow :: Keyword
+kwLeftArrow = unicodeKw Str.leftArrowAscii Str.leftArrowUnicode
+
 kwSyntax :: Keyword
 kwSyntax = asciiKw Str.syntax
 
@@ -268,6 +271,9 @@ kwTrace = asciiKw Str.trace_
 kwFail :: Keyword
 kwFail = asciiKw Str.fail_
 
+kwDo :: Keyword
+kwDo = asciiKw Str.do_
+
 kwDump :: Keyword
 kwDump = asciiKw Str.dump
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 6d0acb0300..99906da31f 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -5,6 +5,9 @@ import Juvix.Prelude.Base
 auto :: (IsString s) => s
 auto = "auto"
 
+do_ :: (IsString s) => s
+do_ = "do"
+
 binaryPrefix :: (IsString s) => s
 binaryPrefix = "0b"
 
@@ -536,9 +539,15 @@ lambdaAscii = "\\"
 toUnicode :: (IsString s) => s
 toUnicode = "→"
 
+leftArrowUnicode :: (IsString s) => s
+leftArrowUnicode = "←"
+
 toAscii :: (IsString s) => s
 toAscii = "->"
 
+leftArrowAscii :: (IsString s) => s
+leftArrowAscii = "<-"
+
 mapstoUnicode :: (IsString s) => s
 mapstoUnicode = "↦"
 

From f646743b5224ea79d640b9e7c613fd32571af173 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 6 Aug 2024 17:21:02 +0200
Subject: [PATCH 4/7] builtin

---
 src/Juvix/Compiler/Builtins.hs                |   2 +
 src/Juvix/Compiler/Builtins/Monad.hs          |   8 ++
 src/Juvix/Compiler/Concrete/Data/Builtins.hs  | 117 +++++++++++++++++-
 src/Juvix/Compiler/Concrete/Language/Base.hs  |   6 -
 src/Juvix/Compiler/Concrete/Print/Base.hs     |   8 +-
 .../FromParsed/Analysis/Scoping.hs            |   8 --
 .../Concrete/Translation/FromSource.hs        |   3 +-
 .../Compiler/Core/Data/InfoTableBuilder.hs    |   5 +-
 .../Compiler/Core/Translation/FromInternal.hs |  16 +--
 .../Core/Translation/Stripped/FromCore.hs     |   1 +
 .../Internal/Translation/FromConcrete.hs      |  88 ++++++-------
 src/Juvix/Extra/Strings.hs                    |   6 +
 tests/Compilation/positive/test080.juvix      |  74 +++++++++++
 13 files changed, 265 insertions(+), 77 deletions(-)
 create mode 100644 src/Juvix/Compiler/Builtins/Monad.hs
 create mode 100644 tests/Compilation/positive/test080.juvix

diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
index fbd9ec0226..d47c5a6e0f 100644
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Builtins/Monad.hs b/src/Juvix/Compiler/Builtins/Monad.hs
new file mode 100644
index 0000000000..c1855a3562
--- /dev/null
+++ b/src/Juvix/Compiler/Builtins/Monad.hs
@@ -0,0 +1,8 @@
+module Juvix.Compiler.Builtins.Monad where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerMonadBind :: forall r. (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
+registerMonadBind f = registerBuiltin BuiltinMonadBind (f ^. funDefName)
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index e10b8e78a8..4499e82219 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 7497502869..fa9ad5a696 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -55,11 +55,6 @@ type family FieldArgIxType s = res | res -> s where
   FieldArgIxType 'Parsed = ()
   FieldArgIxType 'Scoped = Int
 
-type DoBindIdenType :: Stage -> GHCType
-type family DoBindIdenType s = res | res -> s where
-  DoBindIdenType 'Parsed = ()
-  DoBindIdenType 'Scoped = ScopedIden
-
 type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHCType
 type family SideIfBranchConditionType s k = res where
   SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
@@ -2489,7 +2484,6 @@ deriving stock instance Ord (RecordStatement 'Scoped)
 data Do (s :: Stage) = Do
   { _doKeyword :: Irrelevant KeywordRef,
     _doDelims :: Irrelevant (KeywordRef, KeywordRef),
-    _doBindIden :: DoBindIdenType s,
     _doStatements :: NonEmpty (DoStatement s)
   }
   deriving stock (Generic)
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 4bf607efce..15119ada9c 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -423,8 +423,10 @@ instance (SingI s) => PrettyPrint (Do s) where
         statements' = ppBlock _doStatements
     dokw
       <+> openbr
-      <+> statements'
-      <+> closebr
+        <> hardline
+        <> indent statements'
+        <> hardline
+        <> closebr
 
 instance (SingI s) => PrettyPrint (ExpressionAtom s) where
   ppCode = \case
@@ -828,7 +830,7 @@ ppLRExpression associates fixlr e =
     (ppCode e)
 
 ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
-ppBlock items = vsep (sepEndSemicolon (fmap ppCode items))
+ppBlock items = vsepHard (sepEndSemicolon (fmap ppCode items))
 
 instance (SingI s) => PrettyPrint (Lambda s) where
   ppCode Lambda {..} = do
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 77ad466eeb..1828694c2c 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -20,7 +20,6 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra (recordNameSignatureByIndex)
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Gen qualified as G
-import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Pretty (ppTrace)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
@@ -29,7 +28,6 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Compiler.Store.Scoped.Language as Store
 import Juvix.Data.FixityInfo qualified as FI
-import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude
 
 scopeCheck ::
@@ -2409,16 +2407,10 @@ checkDo ::
   Do 'Parsed ->
   Sem r (Do 'Scoped)
 checkDo Do {..} = do
-  let bindSym :: Symbol =
-        run
-          . runReader (getLoc _doKeyword)
-          $ Gen.symbol Str.bindOperator
-  bindIden <- checkScopedIden (NameUnqualified bindSym)
   stmts' <- mapM checkDoStatement _doStatements
   return
     Do
       { _doStatements = stmts',
-        _doBindIden = bindIden,
         _doKeyword,
         _doDelims
       }
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index a04bec1062..f5c499b5e1 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1196,8 +1196,7 @@ doBlock = do
   let
   return
     Do
-      { _doBindIden = (),
-        _doDelims = Irrelevant (lbr, rbr),
+      { _doDelims = Irrelevant (lbr, rbr),
         ..
       }
 
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index 9648fc97d2..605bb1b969 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@@ -156,8 +156,9 @@ runInfoTableBuilder' st = reinterpret (runState st) interp
         modify' (over (builderStateModule . moduleInfoTable . infoIdentifiers) (HashMap.adjust (over identifierType (expandType args)) sym))
       GetIdent txt -> do
         s <- get
-        let r1 = HashMap.lookup txt (s ^. builderStateModule . moduleInfoTable . identMap)
-            r2 = HashMap.lookup txt (s ^. builderStateModule . moduleImportsTable . identMap)
+        let modSt = s ^. builderStateModule
+            r1 = modSt ^. moduleInfoTable . identMap . at txt
+            r2 = modSt ^. moduleImportsTable . identMap . at txt
         return (r1 <|> r2)
       GetModule ->
         (^. builderStateModule) <$> get
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 819ccf009f..ffaa4be376 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -326,7 +326,8 @@ preFunctionDef f = do
 
     normalizeBuiltinName :: Maybe BuiltinFunction -> Text -> Text
     normalizeBuiltinName blt name = case blt of
-      Just b | isNatBuiltin b -> show (pretty b)
+      Just b
+        | isNatBuiltin b -> show (pretty b)
       _ -> case name of
         ">" -> Str.natGt
         ">=" -> Str.natGe
@@ -955,13 +956,12 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of
           Just (IdentConstr tag) ->
             return $
               PatConstr
-                ( PatternConstr
-                    { _patternConstrInfo = setInfoName (ctrName ^. nameText) mempty,
-                      _patternConstrBinder = binder ctorTy,
-                      _patternConstrTag = tag,
-                      _patternConstrArgs = args
-                    }
-                )
+                PatternConstr
+                  { _patternConstrInfo = setInfoName (ctrName ^. nameText) mempty,
+                    _patternConstrBinder = binder ctorTy,
+                    _patternConstrTag = tag,
+                    _patternConstrArgs = args
+                  }
           Just _ -> error ("internal to core: not a constructor " <> txt)
           Nothing -> error ("internal to core: undeclared identifier: " <> txt)
         where
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index e87799c5af..af84cbfefb 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -53,6 +53,7 @@ fromCore fsize tab =
       BuiltinIntLe -> False
       BuiltinIntLt -> False
       BuiltinSeq -> False
+      BuiltinMonadBind -> True -- TODO revise
       BuiltinFromNat -> True
       BuiltinFromInt -> True
 
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index f7a4b01851..f0c941d8ad 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -548,6 +548,7 @@ checkBuiltinFunction d f = localBuiltins $ case f of
   BuiltinFromNat -> checkFromNat d
   BuiltinFromInt -> checkFromInt d
   BuiltinSeq -> checkSeq d
+  BuiltinMonadBind -> checkMonadBind d
 
 checkBuiltinAxiom ::
   (Members '[Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>
@@ -1119,58 +1120,57 @@ goDo ::
   (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
   Do 'Scoped ->
   Sem r Internal.Expression
-goDo Do {..} = goStatements _doStatements
+goDo Do {..} = do
+  goStatements _doStatements
   where
     goStatements :: NonEmpty (DoStatement 'Scoped) -> Sem r Internal.Expression
-    goStatements (l :| ss) = case nonEmpty ss of
-      Nothing -> goLastStatement l
+    goStatements (s :| ss) = case nonEmpty ss of
+      Nothing -> goLastStatement s
       Just ss1 -> do
         ss1' <- goStatements ss1
-        case l of
+        case s of
           DoStatementExpression e -> goDoExpression e ss1'
           DoStatementBind b -> goDoBind b ss1'
           DoStatementLet b -> goDoLet b ss1'
+      where
+        -- l >>= \{_ := r}
+        goDoExpression :: Expression -> Internal.Expression -> Sem r Internal.Expression
+        goDoExpression l r = do
+          let p =
+                PatternArg
+                  { _patternArgIsImplicit = Explicit,
+                    _patternArgName = Nothing,
+                    _patternArgPattern = PatternWildcard (Wildcard (getLoc l <> getLoc r))
+                  }
+          goDoBindHelper p l r
+
+        goDoLet :: DoLet 'Scoped -> Internal.Expression -> Sem r Internal.Expression
+        goDoLet DoLet {..} r = do
+          defs <- goLetFunDefs _doLetStatements
+          return $ case nonEmpty defs of
+            Nothing -> r
+            Just defs1 ->
+              Internal.ExpressionLet
+                Internal.Let
+                  { _letClauses = defs1,
+                    _letExpression = r
+                  }
 
-    -- l >>= \{_ := r}
-    goDoExpression :: Expression -> Internal.Expression -> Sem r Internal.Expression
-    goDoExpression l r = do
-      let p =
-            PatternArg
-              { _patternArgIsImplicit = Explicit,
-                _patternArgName = Nothing,
-                _patternArgPattern = PatternWildcard (Wildcard (getLoc l <> getLoc r))
-              }
-      goDoBindHelper p l r
-
-    goDoLet :: DoLet 'Scoped -> Internal.Expression -> Sem r Internal.Expression
-    goDoLet DoLet {..} r = do
-      defs <- goLetFunDefs _doLetStatements
-      return $ case nonEmpty defs of
-        Nothing -> r
-        Just defs1 ->
-          Internal.ExpressionLet
-            Internal.Let
-              { _letClauses = defs1,
-                _letExpression = r
-              }
-
-    goDoBind :: DoBind 'Scoped -> Internal.Expression -> Sem r Internal.Expression
-    goDoBind DoBind {..} r = goDoBindHelper _doBindPattern _doBindExpression r
-
-    bindIden :: Internal.Expression
-    bindIden = Internal.toExpression (goName (_doBindIden ^. scopedIdenFinal))
-
-    -- l >>= \{p := r}
-    goDoBindHelper :: PatternArg -> Expression -> Internal.Expression -> Sem r Internal.Expression
-    goDoBindHelper p l r = do
-      p' <- goPatternArg p
-      l' <- goExpression l
-      return (bindIden Internal.@@ l' Internal.@@ (p' Internal.==> r))
-
-    goLastStatement :: DoStatement 'Scoped -> Sem r Internal.Expression
-    goLastStatement = \case
-      DoStatementExpression e -> goExpression e
-      d -> throw (ErrDoLastStatement (DoLastStatement d))
+        goDoBind :: DoBind 'Scoped -> Internal.Expression -> Sem r Internal.Expression
+        goDoBind DoBind {..} r = goDoBindHelper _doBindPattern _doBindExpression r
+
+        -- l >>= \{p := r}
+        goDoBindHelper :: PatternArg -> Expression -> Internal.Expression -> Sem r Internal.Expression
+        goDoBindHelper p l r = do
+          p' <- goPatternArg p
+          l' <- goExpression l
+          bindIden <- getBuiltinName (getLoc _doKeyword) BuiltinMonadBind
+          return (bindIden Internal.@@ l' Internal.@@ (p' Internal.==> r))
+
+        goLastStatement :: DoStatement 'Scoped -> Sem r Internal.Expression
+        goLastStatement = \case
+          DoStatementExpression e -> goExpression e
+          d -> throw (ErrDoLastStatement (DoLastStatement d))
 
 goCase :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Case 'Scoped -> Sem r Internal.Case
 goCase c = do
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 99906da31f..b9a3698a68 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -371,6 +371,9 @@ anomaVerifyDetached = "anoma-verify-detached"
 anomaSign :: (IsString s) => s
 anomaSign = "anoma-sign"
 
+builtinMonadBind :: (IsString s) => s
+builtinMonadBind = "monad-bind"
+
 anomaSignDetached :: (IsString s) => s
 anomaSignDetached = "anoma-sign-detached"
 
@@ -968,6 +971,9 @@ nothing = "nothing"
 just :: (IsString s) => s
 just = "just"
 
+monad :: (IsString s) => s
+monad = "monad"
+
 pair :: (IsString s) => s
 pair = "pair"
 
diff --git a/tests/Compilation/positive/test080.juvix b/tests/Compilation/positive/test080.juvix
new file mode 100644
index 0000000000..de86ef48c8
--- /dev/null
+++ b/tests/Compilation/positive/test080.juvix
@@ -0,0 +1,74 @@
+-- Do notation
+module test080;
+
+import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Fixity open;
+import Stdlib.System.IO open;
+import Stdlib.Data.Maybe open;
+
+trait
+type Functor (f : Type -> Type) := mkFunctor {map : {A B : Type} -> (A -> B) -> f A -> f B};
+
+trait
+type Applicative (f : Type -> Type) :=
+  mkApplicative {
+    {{ApplicativeFunctor}} : Functor f;
+    pure : {A : Type} -> A -> f A;
+    ap : {A B : Type} -> f (A -> B) -> f A -> f B
+  };
+
+trait
+type Monad (f : Type -> Type) :=
+  mkMonad {
+    {{MonadApplicative}} : Applicative f;
+
+    bind : {A B : Type} -> f A -> (A -> f B) -> f B
+  };
+
+open Functor;
+open Applicative;
+open Monad;
+
+syntax operator >>= seq;
+builtin monad-bind
+>>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g;
+
+monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x;
+
+instance
+maybeFunctor : Functor Maybe :=
+  mkFunctor@{
+    map {A B} (f : A -> B) : Maybe A -> Maybe B
+      | nothing := nothing
+      | (just x) := just (f x)
+  };
+
+instance
+maybeApplicative : Applicative Maybe :=
+  mkApplicative@{
+    pure := just;
+    ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
+      | (just f) (just x) := just (f x)
+      | _ _ := nothing
+  };
+
+instance
+maybeMonad : Monad Maybe :=
+  mkMonad@{
+    bind {A B} : Maybe A -> (A -> Maybe B) -> Maybe B
+      | nothing _ := nothing
+      | (just a) f := f a
+  };
+
+minusOne : Nat -> Maybe Nat
+  | zero := nothing
+  | (suc n) := just n;
+
+minusThree (n : Nat) : Maybe Nat :=
+  do {
+    x1 <- minusOne n;
+    x2 <- minusOne x1;
+    pure x2;
+  };
+
+main : IO := printLn (minusThree 1) >>> printLn (minusThree 4);

From 07d6c627d32398956139123861163a4738a21505 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 7 Aug 2024 13:51:28 +0200
Subject: [PATCH 5/7] new syntax

---
 src/Juvix/Compiler/Concrete/Language/Base.hs  |  3 +-
 src/Juvix/Compiler/Concrete/Print/Base.hs     | 22 ++++++++----
 .../FromParsed/Analysis/Scoping.hs            |  1 +
 .../Concrete/Translation/FromSource.hs        | 34 ++++++++++++++-----
 4 files changed, 45 insertions(+), 15 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index fa9ad5a696..109e9e6847 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -1709,7 +1709,8 @@ deriving stock instance Ord (LetStatement 'Scoped)
 
 data DoLet (s :: Stage) = DoLet
   { _doLetKw :: Irrelevant KeywordRef,
-    _doLetStatements :: NonEmpty (LetStatement s)
+    _doLetStatements :: NonEmpty (LetStatement s),
+    _doLetInKw :: Irrelevant KeywordRef
   }
   deriving stock (Generic)
 
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 15119ada9c..581dfb12b3 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -401,8 +401,10 @@ instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where
 instance (SingI s) => PrettyPrint (DoLet s) where
   ppCode DoLet {..} = do
     let letFunDefs' = blockIndent (ppBlock _doLetStatements)
+    -- blockIndent d = hardline <> indent d <> line
     ppCode _doLetKw
-      <+> letFunDefs'
+      <> letFunDefs'
+      <> ppCode _doLetInKw
 
 instance (SingI s) => PrettyPrint (DoBind s) where
   ppCode DoBind {..} = do
@@ -410,6 +412,16 @@ instance (SingI s) => PrettyPrint (DoBind s) where
       <+> ppCode _doBindArrowKw
       <+> ppTopExpressionType _doBindExpression
 
+instance (Foldable l, SingI s) => PrettyPrint (l (DoStatement s)) where
+  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => l (DoStatement s) -> Sem r ()
+  ppCode = vsepHard . map go . toList
+    where
+      go :: DoStatement s -> Sem r ()
+      go = \case
+        DoStatementBind b -> ppCode b >> semicolon
+        DoStatementExpression b -> ppExpressionType b >> semicolon
+        DoStatementLet b -> ppCode b
+
 instance (SingI s) => PrettyPrint (DoStatement s) where
   ppCode = \case
     DoStatementExpression e -> ppExpressionType e
@@ -418,13 +430,11 @@ instance (SingI s) => PrettyPrint (DoStatement s) where
 
 instance (SingI s) => PrettyPrint (Do s) where
   ppCode Do {..} = do
-    let dokw = ppCode _doKeyword
-        (openbr, closebr) = over both ppCode (_doDelims ^. unIrrelevant)
-        statements' = ppBlock _doStatements
-    dokw
+    let (openbr, closebr) = over both ppCode (_doDelims ^. unIrrelevant)
+    ppCode _doKeyword
       <+> openbr
         <> hardline
-        <> indent statements'
+        <> indent (ppCode _doStatements)
         <> hardline
         <> closebr
 
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 1828694c2c..7120a43eb9 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -2390,6 +2390,7 @@ checkDoLet DoLet {..} = do
   return
     DoLet
       { _doLetKw,
+        _doLetInKw,
         _doLetStatements = defs'
       }
 
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index f5c499b5e1..5f6da993b8 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1177,21 +1177,39 @@ doBind = do
 doLet :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoLet 'Parsed)
 doLet = do
   _doLetKw <- Irrelevant <$> kw kwLet
-  -- TODO think about this P.try
-  _doLetStatements <- P.sepEndBy1 (P.try letStatement) semicolon
+  _doLetStatements <- P.sepEndBy1 letStatement semicolon
+  _doLetInKw <- Irrelevant <$> kw kwIn
   return DoLet {..}
 
-doStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoStatement 'Parsed)
-doStatement =
-  DoStatementLet <$> doLet
-    <|> DoStatementBind <$> doBind
-    <|> DoStatementExpression <$> parseExpressionAtoms
+doStatements :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (NonEmpty (DoStatement 'Parsed))
+doStatements =
+  P.label "<do statement>" $
+    plet
+      <|> pother
+  where
+    plet :: ParsecS r (NonEmpty (DoStatement 'Parsed))
+    plet = do
+      s <- DoStatementLet <$> doLet
+      ss <- doStatements
+      return (s :| toList ss)
+
+    pother :: ParsecS r (NonEmpty (DoStatement 'Parsed))
+    pother = do
+      s <-
+        DoStatementBind <$> doBind
+          <|> DoStatementExpression <$> parseExpressionAtoms
+      semi <- isJust <$> optional semicolon
+      if
+          | semi -> do
+              ss <- maybe [] toList <$> optional doStatements
+              return (s :| ss)
+          | otherwise -> return (pure s)
 
 doBlock :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Do 'Parsed)
 doBlock = do
   _doKeyword <- Irrelevant <$> kw kwDo
   lbr <- kw delimBraceL
-  _doStatements <- P.sepEndBy1 doStatement semicolon
+  _doStatements <- doStatements
   rbr <- kw delimBraceR
   let
   return

From 45f4410dddd2f3d8bb3c37792e517cd98ef9784d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 7 Aug 2024 15:45:38 +0200
Subject: [PATCH 6/7] implicit pattern error

---
 .../FromParsed/Analysis/Scoping.hs            |  3 ++-
 .../FromParsed/Analysis/Scoping/Error.hs      |  2 ++
 .../Analysis/Scoping/Error/Types.hs           | 27 +++++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 7120a43eb9..c6f2b9f1b1 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -2373,7 +2373,8 @@ checkDoBind ::
 checkDoBind DoBind {..} = do
   expr' <- checkParseExpressionAtoms _doBindExpression
   pat' <- checkParsePatternAtoms _doBindPattern
-  -- TODO check no implicit pattern
+  unless (Explicit == pat' ^. patternArgIsImplicit) $
+    throw (ErrDoBindImplicitPattern (DoBindImplicitPattern pat'))
   return
     DoBind
       { _doBindArrowKw,
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
index 81cfab60b7..850e219461 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
@@ -60,6 +60,7 @@ data ScoperError
   | ErrBuiltinNotDefined BuiltinNotDefined
   | ErrBuiltinErrorMessage BuiltinErrorMessage
   | ErrDoLastStatement DoLastStatement
+  | ErrDoBindImplicitPattern DoBindImplicitPattern
   deriving stock (Generic)
 
 instance ToGenericError ScoperError where
@@ -111,6 +112,7 @@ instance ToGenericError ScoperError where
     ErrBuiltinNotDefined e -> genericError e
     ErrBuiltinErrorMessage e -> genericError e
     ErrDoLastStatement e -> genericError e
+    ErrDoBindImplicitPattern e -> genericError e
 
 builtinsErrorMsg :: (Members '[Error ScoperError] r) => Interval -> AnsiText -> Sem r a
 builtinsErrorMsg loc msg =
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
index cc6635bcf6..97a3d2e953 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
@@ -618,6 +618,33 @@ instance ToGenericError AliasBinderPattern where
             "As-Patterns cannot be used to alias pattern variables:"
               <+> code (ppCode opts' pat)
 
+newtype DoBindImplicitPattern = DoBindImplicitPattern
+  { _doBindImplicitPattern :: PatternArg
+  }
+  deriving stock (Show)
+
+makeLenses ''DoBindImplicitPattern
+
+instance ToGenericError DoBindImplicitPattern where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = prettyError msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          pat :: PatternArg
+          pat = e ^. doBindImplicitPattern
+          i = getLoc pat
+          msg =
+            "Illegal pattern "
+              <> ppCode opts' pat
+              <> "\nImplicit patterns are not allowed on the left hand side of a bind arrow inside a do block"
+
 newtype ImplicitPatternLeftApplication = ImplicitPatternLeftApplication
   { _implicitPatternLeftApplication :: PatternApp
   }

From 19fa9917ff62bb3f86ebc244783654dca06287e8 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 14 Aug 2024 23:18:21 +0200
Subject: [PATCH 7/7] fix rebase

---
 src/Juvix/Compiler/Builtins/Monad.hs                   |  5 ++---
 .../Compiler/Internal/Translation/FromConcrete.hs      |  6 +++---
 tests/Compilation/positive/test080.juvix               | 10 ++++++++--
 3 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/Juvix/Compiler/Builtins/Monad.hs b/src/Juvix/Compiler/Builtins/Monad.hs
index c1855a3562..a7208751ae 100644
--- a/src/Juvix/Compiler/Builtins/Monad.hs
+++ b/src/Juvix/Compiler/Builtins/Monad.hs
@@ -1,8 +1,7 @@
 module Juvix.Compiler.Builtins.Monad where
 
-import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-registerMonadBind :: forall r. (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
-registerMonadBind f = registerBuiltin BuiltinMonadBind (f ^. funDefName)
+checkMonadBind :: forall r. FunctionDef -> Sem r ()
+checkMonadBind _ = return ()
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index f0c941d8ad..8db74604f0 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -1101,7 +1101,7 @@ goExpression = \case
 
 goLetFunDefs ::
   forall r.
-  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
   NonEmpty (LetStatement 'Scoped) ->
   Sem r [Internal.LetClause]
 goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetStatements clauses
@@ -1117,7 +1117,7 @@ goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetSta
 
 goDo ::
   forall r.
-  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
   Do 'Scoped ->
   Sem r Internal.Expression
 goDo Do {..} = do
@@ -1164,7 +1164,7 @@ goDo Do {..} = do
         goDoBindHelper p l r = do
           p' <- goPatternArg p
           l' <- goExpression l
-          bindIden <- getBuiltinName (getLoc _doKeyword) BuiltinMonadBind
+          bindIden <- localBuiltins (getBuiltinNameScoper (getLoc _doKeyword) BuiltinMonadBind)
           return (bindIden Internal.@@ l' Internal.@@ (p' Internal.==> r))
 
         goLastStatement :: DoStatement 'Scoped -> Sem r Internal.Expression
diff --git a/tests/Compilation/positive/test080.juvix b/tests/Compilation/positive/test080.juvix
index de86ef48c8..edfb423813 100644
--- a/tests/Compilation/positive/test080.juvix
+++ b/tests/Compilation/positive/test080.juvix
@@ -22,6 +22,7 @@ type Monad (f : Type -> Type) :=
   mkMonad {
     {{MonadApplicative}} : Applicative f;
 
+    builtin monad-bind
     bind : {A B : Type} -> f A -> (A -> f B) -> f B
   };
 
@@ -30,7 +31,6 @@ open Applicative;
 open Monad;
 
 syntax operator >>= seq;
-builtin monad-bind
 >>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g;
 
 monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x;
@@ -68,7 +68,13 @@ minusThree (n : Nat) : Maybe Nat :=
   do {
     x1 <- minusOne n;
     x2 <- minusOne x1;
-    pure x2;
+    let
+      x2' : Nat := x2;
+      num := 3;
+      num1 := 4;
+    in
+    x3 <- minusOne x2';
+    pure x3;
   };
 
 main : IO := printLn (minusThree 1) >>> printLn (minusThree 4);