@@ -43,6 +43,15 @@ export %inline
4343(>>=) {c1 = False} = SeqEmpty
4444(>>=) {c1 = True} = SeqEat
4545
46+||| Sequence two grammars. If either consumes some input, the sequence is
47+||| guaranteed to consume input. This is an explicitly non-infinite version
48+||| of `>>=`.
49+export
50+seq : Grammar tok c1 a ->
51+ (a -> Grammar tok c2 b) ->
52+ Grammar tok (c1 || c2) b
53+seq = SeqEmpty
54+
4655||| Sequence a grammar followed by the grammar it returns.
4756export
4857join : {c1 : Bool} ->
@@ -79,18 +88,16 @@ Functor (Grammar tok c) where
7988||| from the first grammar to the value from the second grammar.
8089||| Guaranteed to consume if either grammar consumes.
8190export
82−(<*>) : {c1 : Bool} ->
83− Grammar tok c1 (a -> b) ->
84− inf c1 (Grammar tok c2 a) ->
91+(<*>) : Grammar tok c1 (a -> b) ->
92+ Grammar tok c2 a ->
8593 Grammar tok (c1 || c2) b
86−(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
87−(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
94+(<*>) x y = SeqEmpty x (\f => map f y)
8895
8996||| Sequence two grammars. If both succeed, use the value of the first one.
9097||| Guaranteed to consume if either grammar consumes.
9198export
9299(<*) : Grammar tok c1 a ->
93− inf c1 (Grammar tok c2 b) ->
100+ Grammar tok c2 b ->
94101 Grammar tok (c1 || c2) a
95102(<*) x y = map const x <*> y
96103
@@ -98,7 +105,7 @@ export
98105||| Guaranteed to consume if either grammar consumes.
99106export
100107(*>) : Grammar tok c1 a ->
101− inf c1 (Grammar tok c2 b) ->
108+ Grammar tok c2 b ->
102109 Grammar tok (c1 || c2) b
103110(*>) x y = map (const id) x <*> y
104111