@@ -40,18 +40,72 @@ inf False t = t
4040||| consumed and therefore the input is smaller)
4141export %inline
4242(>>=) : {c1 : Bool} ->
43− Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
43+ Grammar tok c1 a ->
44+ inf c1 (a -> Grammar tok c2 b) ->
4445 Grammar tok (c1 || c2) b
4546(>>=) {c1 = False} = SeqEmpty
4647(>>=) {c1 = True} = SeqEat
4748
49+||| Sequence a grammar followed by the grammar it returns.
50+export
51+join : {c1 : Bool} ->
52+ Grammar tok c1 (Grammar tok c2 a) ->
53+ Grammar tok (c1 || c2) a
54+join {c1 = False} p = SeqEmpty p id
55+join {c1 = True} p = SeqEat p id
56+
4857||| Give two alternative grammars. If both consume, the combination is
4958||| guaranteed to consume.
5059export
51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
60+(<|>) : Grammar tok c1 ty ->
61+ Grammar tok c2 ty ->
5262 Grammar tok (c1 && c2) ty
5363(<|>) = Alt
5464
65+||| Allows the result of a grammar to be mapped to a different value.
66+export
67+Functor (Grammar tok c) where
68+ map f (Empty val) = Empty (f val)
69+ map f (Fail msg) = Fail msg
70+ map f (Terminal g) = Terminal (\t => map f (g t))
71+ map f (Alt x y) = Alt (map f x) (map f y)
72+ map f (SeqEat act next)
73+ = SeqEat act (\val => map f (next val))
74+ map f (SeqEmpty act next)
75+ = SeqEmpty act (\val => map f (next val))
76+ -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
77+ -- so a sequence must be used.
78+ map {c = False} f p = SeqEmpty p (Empty . f)
79+
80+||| Sequence a grammar with value type `a -> b` and a grammar
81+||| with value type `a`. If both succeed, apply the function
82+||| from the first grammar to the value from the second grammar.
83+||| Guaranteed to consume if either grammar consumes.
84+export
85+(<*>) : {c1 : Bool} ->
86+ Grammar tok c1 (a -> b) ->
87+ inf c1 (Grammar tok c2 a) ->
88+ Grammar tok (c1 || c2) b
89+(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
90+(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
91+
92+||| Sequence two grammars. If both succeed, use the value of the first one.
93+||| Guaranteed to consume if either grammar consumes.
94+export
95+(<*) : Grammar tok c1 a ->
96+ inf c1 (Grammar tok c2 b) ->
97+ Grammar tok (c1 || c2) a
98+(<*) x y = map const x <*> y
99+
100+||| Sequence two grammars. If both succeed, use the value of the second one.
101+||| Guaranteed to consume if either grammar consumes.
102+export
103+(*>) : Grammar tok c1 a ->
104+ inf c1 (Grammar tok c2 b) ->
105+ Grammar tok (c1 || c2) b
106+(*>) x y = map (const id) x <*> y
107+
108+||| Always succeed with the given value.
55109export
56110pure : (val : ty) -> Grammar tok False ty
57111pure = Empty
@@ -226,6 +280,9 @@ optional : Grammar tok True a -> (ifNothing : a) ->
226280 Grammar tok False a
227281optional p def = p <|> pure def
228282
283+||| Fold over a list of grammars until the first one succeeds.
284+choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
285+choice xs = foldr Alt (Fail "No more options") xs
229286
230287||| Parse an instance of `p` that is between `left` and `right`.
231288export