Make the parser commit to the choices it makes.

1 files changed, 12 insertions, 12 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 7008950..fbd1252 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -122,48 +122,48 @@ ident = bounds $ match OTIdent
 
 var : Grammar state ObsToken True Syntax
 var = do
-  id <- ident
+  id <- ident <* commit
   pure (Var id.bounds id.val)
 
 prop : Grammar state ObsToken True Syntax
 prop = do
-  prop <- bounds $ match OTProp
+  prop <- bounds $ match OTProp <* commit
   pure (Sort prop.bounds Prop)
 
 set0 : Grammar state ObsToken True Syntax
 set0 = do
-  set <- bounds $ match OTSet
+  set <- bounds $ match OTSet <* commit
   pure (Sort set.bounds (Set 0))
 
 top : Grammar state ObsToken True Syntax
 top = do
-  unit <- bounds $ match OTUnit
+  unit <- bounds $ match OTUnit <* commit
   pure (Top unit.bounds)
 
 point : Grammar state ObsToken True Syntax
 point = do
-  point <- bounds $ match OTPoint
+  point <- bounds $ match OTPoint <* commit
   pure (Point point.bounds)
 
 bottom : Grammar state ObsToken True Syntax
 bottom = do
-  void <- bounds $ match OTVoid
+  void <- bounds $ match OTVoid <* commit
   pure (Bottom void.bounds)
 
 atomicNoSet : Grammar state ObsToken True Syntax
-atomicNoSet = var <|> prop <|> top <|> point <|> bottom
+atomicNoSet = (var <|> prop <|> top <|> point <|> bottom) <* commit
 
 atomic : Grammar state ObsToken True Syntax
-atomic = atomicNoSet <|> set0
+atomic = (atomicNoSet <|> set0) <* commit
 
 set : Grammar state ObsToken True Syntax
 set = do
-  i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |]
+  i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |] <* commit
   pure (Sort i.bounds i.val)
 
 botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
 botElim = do
-  absurd <- bounds $ match OTAbsurd
+  absurd <- bounds $ match OTAbsurd <* commit
   pure (Absurd absurd.bounds)
 
 -- NOTE: these functions are all total.
@@ -182,7 +182,7 @@ exp = precGteApp <|> (botElim <*> term <*> term)
 
 partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
-decl = [| MkPair ident (match OTColon *> exp) |]
+decl = [| MkPair ident (commit *> match OTColon *> exp) |]
 
 partial
 def : Grammar state ObsToken True (WithBounds String, Syntax)
@@ -200,7 +200,7 @@ fullDef =
 
 partial
 file : Grammar state ObsToken False (List Definition)
-file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef
+file = many (match OTNewline) *> sepBy (some (match OTNewline)) fullDef <* many (match OTNewline) <* eof
 
 postprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
 postprocess [] = []