@@ -152,12 +152,16 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
152152 (val : ty) -> (more : List tok) ->
153153 ParseResult (x :: xs ++ more) c ty
154154
155+-- Take the result of an alternative branch, reset the commit flag to
156+-- the commit flag from the outer alternative, and weaken the 'consumes'
157+-- flag to take both alternatives into account
155158weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
156− ParseResult xs c ty -> ParseResult xs (whatever && c) ty
157−weakenRes (Failure com msg ts) = Failure com msg ts
158−weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
159−weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
160−weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
159+ (com' : Bool) ->
160+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
161+weakenRes com' (Failure com msg ts) = Failure com' msg ts
162+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
163+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
164+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
161165
162166shorter : (more : List tok) -> .(ys : List tok) ->
163167 LTE (S (length more)) (S (length (ys ++ more)))
@@ -192,7 +196,7 @@ doParse com xs act with (sizeAccessible xs)
192196 = if com' -- If the alternative had committed, don't try the
193197 -- other branch (and reset commit flag)
194198 then Failure com msg ts
195− else weakenRes (doParse False xs y | sml)
199+ else weakenRes com (doParse False xs y | sml)
196200 -- Successfully parsed the first option, so use the outer commit flag
197201 doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
198202 = EmptyRes com val xs