From cb394d3cc2ff85373a3307bf11bca6b44ad2f7f6 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sun, 29 Mar 2026 09:44:50 -0700
Subject: [PATCH] change record update syntax

---
 src/Lib/Parser.newt | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt
index b37aa18..7b3700a 100644
--- a/src/Lib/Parser.newt
+++ b/src/Lib/Parser.newt
@@ -28,7 +28,7 @@ parenWrap pa = do
   pure t
 
 braces : ∀ a. Parser a -> Parser a
-braces pa = do
+braces pa = try $ do
   symbol "{"
   t <- pa
   symbol "}"
@@ -107,8 +107,9 @@ asAtom = do
     Just exp => pure $ RAs fc nm exp
     Nothing  => pure $ RVar fc nm
 
--- the inside of Raw
+
 recordUpdate : Parser Raw
+recordUpdate' : Parser Raw
 
 parenTypeExp : Parser Raw
 parenTypeExp = do
@@ -126,6 +127,7 @@ atom : Parser Raw
 atom = do
   pure MkUnit
   RU <$> getPos <* keyword "U"
+    <|> recordUpdate'
     -- <|> RVar <$> getPos <*> ident
     <|> asAtom
     <|> RVar <$> getPos <*> uident
@@ -155,6 +157,15 @@ recordUpdate = do
   tm <- optional atom
   pure $ RUpdateRec fc clauses tm
 
+recordUpdate' = do
+  fc <- getPos
+  symbol "{"
+  clauses <- sepBy (symbol ";") updateClause
+  symbol "}"
+  tm <- optional atom
+  pure $ RUpdateRec fc clauses tm
+
+
 -- Argument to a Spine
 pArg : Parser (Icit × FC × Raw)
 pArg = do
@@ -454,11 +465,14 @@ ebind = do
 
 ibind : Parser Telescope
 ibind = do
-  -- I've gone back and forth on this, but I think {m a b} is more useful than {Int}
-  symbol "{"
-  quant <- quantity
-  names <- (some (addPos varname))
-  ty <- symbol ":" *> typeExpr
+  -- we don't know if it's an ibind or record update until we hit the `:`
+  (quant, names) <- try $ do
+    symbol "{"
+    quant <- quantity
+    names <- (some (addPos varname))
+    symbol ":"
+    pure (quant, names)
+  ty <- typeExpr
   symbol "}"
   pure $ map (makeBind quant (Just ty)) names
   where