@@ -40,18 +40,72 @@ inf False t = t
40||| consumed and therefore the input is smaller)
40||| consumed and therefore the input is smaller)
41export %inline
41export %inline
42(>>=) : {c1 : Bool} ->
42(>>=) : {c1 : Bool} ->
43− Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
44+ inf c1 (a -> Grammar tok c2 b) ->
44 Grammar tok (c1 || c2) b
45 Grammar tok (c1 || c2) b
45(>>=) {c1 = False} = SeqEmpty
46(>>=) {c1 = False} = SeqEmpty
46(>>=) {c1 = True} = SeqEat
47(>>=) {c1 = True} = SeqEat
49+||| Sequence a grammar followed by the grammar it returns.
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
48||| Give two alternative grammars. If both consume, the combination is
57||| Give two alternative grammars. If both consume, the combination is
49||| guaranteed to consume.
58||| guaranteed to consume.
51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
60+(<|>) : Grammar tok c1 ty ->
52 Grammar tok (c1 && c2) ty
62 Grammar tok (c1 && c2) ty
53(<|>) = Alt
63(<|>) = Alt
65+||| Allows the result of a grammar to be mapped to a different value.
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)
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.
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)
92+||| Sequence two grammars. If both succeed, use the value of the first one.
93+||| Guaranteed to consume if either grammar consumes.
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
100+||| Sequence two grammars. If both succeed, use the value of the second one.
101+||| Guaranteed to consume if either grammar consumes.
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
108+||| Always succeed with the given value.
56pure : (val : ty) -> Grammar tok False ty
110pure : (val : ty) -> Grammar tok False ty
57pure = Empty
111pure = Empty
@@ -226,6 +280,9 @@ optional : Grammar tok True a -> (ifNothing : a) ->
226 Grammar tok False a
280 Grammar tok False a
227optional p def = p <|> pure def
281optional p def = p <|> pure def
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
230||| Parse an instance of `p` that is between `left` and `right`.
287||| Parse an instance of `p` that is between `left` and `right`.