@@ -152,12 +152,16 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
152 (val : ty) -> (more : List tok) ->
152 (val : ty) -> (more : List tok) ->
153 ParseResult (x :: xs ++ more) c ty
153 ParseResult (x :: xs ++ more) c ty
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
155weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
158weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
156− ParseResult xs c ty -> ParseResult xs (whatever && c) ty
160+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
157−weakenRes (Failure com msg ts) = Failure com msg ts
161+weakenRes com' (Failure com msg ts) = Failure com' msg ts
158−weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
162+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
159−weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
163+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
160−weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
164+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
162shorter : (more : List tok) -> .(ys : List tok) ->
166shorter : (more : List tok) -> .(ys : List tok) ->
163 LTE (S (length more)) (S (length (ys ++ more)))
167 LTE (S (length more)) (S (length (ys ++ more)))
@@ -192,7 +196,7 @@ doParse com xs act with (sizeAccessible xs)
192 = if com' -- If the alternative had committed, don't try the
196 = if com' -- If the alternative had committed, don't try the
193 -- other branch (and reset commit flag)
197 -- other branch (and reset commit flag)
194 then Failure com msg ts
198 then Failure com msg ts
195− else weakenRes (doParse False xs y | sml)
199+ else weakenRes com (doParse False xs y | sml)
196 -- Successfully parsed the first option, so use the outer commit flag
200 -- Successfully parsed the first option, so use the outer commit flag
197 doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
201 doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
198 = EmptyRes com val xs
202 = EmptyRes com val xs