A refactored Parsec

Arcsec.fmc

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);;;