Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham
Created April 30, 2020 00:11
Show Gist options
  • Save johnchandlerburnham/56cb8ae845f7e6ef2b3be9ae853ec232 to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/56cb8ae845f7e6ef2b3be9ae853ec232 to your computer and use it in GitHub Desktop.
A refactored Parsec
Arcsec : (S : Type) -> (E : Type) -> (A: Type) -> Type
(S) (E) (A)
<B : Type> ->
Parsec.State(S)(E) ->
(Bool -> Parsec.State(S)(E) -> Either(Parsec.Error(E))(A) -> B) ->
B
Arcsec.Reply : Type -> Type -> Type -> Type
(S) (E) (A)
arcsec_reply<P: Arcsec.Reply(S)(E)(A) -> Type> ->
(new :
(eaten: Bool) ->
(state: Parsec.State(S)(E)) ->
(value: Either(Parsec.Error(E))(A)) ->
P(Arcsec.Reply.new<S><E><A>(eaten)(state)(value))
) ->
P(arcsec_reply)
Arcsec.Reply.new :
<S: Type> ->
<E: Type> ->
<A: Type> ->
Bool ->
Parsec.State(S)(E) ->
Either(Parsec.Error(E))(A) ->
Arcsec.Reply(S)(E)(A)
<S> <E> <A> (eaten) (state) (value)
<P> (new) new(eaten)(state)(value)
Arcsec.run :
<S : Type> ->
<E : Type> ->
<A: Type> ->
Arcsec(S)(E)(A) ->
Parsec.State(S)(E) ->
Arcsec.Reply(S)(E)(A)
<S> <E> <A> (p) (s)
p<Arcsec.Reply(S)(E)(A)>(s)
| Arcsec.Reply.new<S><E><A>;
Arcsec.try :
<S: Type> ->
<E: Type> ->
<A: Type> ->
Arcsec(S)(E)(A) ->
Arcsec(S)(E)(A)
<S> <E> <A> (p)
<X> (s1) (new_reply)
p<X>(s1)
| (eaten) (s2) (value)
value<() X>
| (x) new_reply(Bool.false)(s1)(value);
| (x) eaten<() X>
| new_reply(Bool.true)(s2)(value);
| new_reply(Bool.false)(s2)(value);;;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment