@@ -43,6 +43,15 @@ export %inline
43(>>=) {c1 = False} = SeqEmpty
43(>>=) {c1 = False} = SeqEmpty
44(>>=) {c1 = True} = SeqEat
44(>>=) {c1 = True} = SeqEat
46+||| Sequence two grammars. If either consumes some input, the sequence is
47+||| guaranteed to consume input. This is an explicitly non-infinite version
50+seq : Grammar tok c1 a ->
51+ (a -> Grammar tok c2 b) ->
52+ Grammar tok (c1 || c2) b
46||| Sequence a grammar followed by the grammar it returns.
55||| Sequence a grammar followed by the grammar it returns.
48join : {c1 : Bool} ->
57join : {c1 : Bool} ->
@@ -79,18 +88,16 @@ Functor (Grammar tok c) where
79||| from the first grammar to the value from the second grammar.
88||| from the first grammar to the value from the second grammar.
80||| Guaranteed to consume if either grammar consumes.
89||| Guaranteed to consume if either grammar consumes.
82−(<*>) : {c1 : Bool} ->
83− Grammar tok c1 (a -> b) ->
91+(<*>) : Grammar tok c1 (a -> b) ->
84− inf c1 (Grammar tok c2 a) ->
92+ Grammar tok c2 a ->
85 Grammar tok (c1 || c2) b
93 Grammar tok (c1 || c2) b
86−(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
94+(<*>) x y = SeqEmpty x (\f => map f y)
87−(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
89||| Sequence two grammars. If both succeed, use the value of the first one.
96||| Sequence two grammars. If both succeed, use the value of the first one.
90||| Guaranteed to consume if either grammar consumes.
97||| Guaranteed to consume if either grammar consumes.
92(<*) : Grammar tok c1 a ->
99(<*) : Grammar tok c1 a ->
93− inf c1 (Grammar tok c2 b) ->
100+ Grammar tok c2 b ->
94 Grammar tok (c1 || c2) a
101 Grammar tok (c1 || c2) a
95(<*) x y = map const x <*> y
102(<*) x y = map const x <*> y
@@ -98,7 +105,7 @@ export
98||| Guaranteed to consume if either grammar consumes.
105||| Guaranteed to consume if either grammar consumes.
100(*>) : Grammar tok c1 a ->
107(*>) : Grammar tok c1 a ->
101− inf c1 (Grammar tok c2 b) ->
108+ Grammar tok c2 b ->
102 Grammar tok (c1 || c2) b
109 Grammar tok (c1 || c2) b
103(*>) x y = map (const id) x <*> y
110(*>) x y = map (const id) x <*> y