Parsec.fm

Parsec.Error.Fancy.custom: <E: Type> -> (e: E) -> Parsec.Error.Fancy(E)
  <E> (e)
  <P> () (custom) custom(e)

Parsec.Error.Fancy.fail: <E: Type> -> String -> Parsec.Error.Fancy(E)
  <E> (msg)
  <P> (fail) () fail(msg)

// A fancy error is where the parser author preempts the internal error system
// and instead returns a failure message or a value of custom error type E

Parsec.Error.Fancy : Type -> Type
  (E)
  parser.error.fancy<P: Parsec.Error.Fancy(E) -> Type> ->
  (fail:   (msg: String) -> P(Parsec.Error.Fancy.fail<E>(msg))) ->
  (custom: (err: E) -> P(Parsec.Error.Fancy.custom<E>(err))) ->
  P(parser.error.fancy)

Parsec.Error.Item.end_of_input: Parsec.Error.Item
  <P> () () (end_of_input) end_of_input

// Error items are the possible things that at a given position in the input
// a parser might expect to see, or alternatively might *not* expect to see.
//
// They are:
// - tokens or characters such as "a", "b", "&", "ϝ", "\ACK"
// - labels or tags used by some parsers (e.g. Parsec.tokens) to describe
//   abstract input conditions like "is a capital letter" or the string "foobar"
//   (custom labels can also be attached to a parser using Parsec.label)
// - the end of the input stream

Parsec.Error.Item : Type
  parser.error.tokens<P: Parsec.Error.Item -> Type> ->
  (tokens:       (xs: String) -> P(Parsec.Error.Item.tokens(xs))) ->
  (label:        (xs: String) -> P(Parsec.Error.Item.label(xs))) ->
  (end_of_input: P(Parsec.Error.Item.end_of_input)) ->
  P(parser.error.tokens)

Parsec.Error.Item.label: String -> Parsec.Error.Item
  (xs)
  <P> () (label) () label(xs)

Parsec.Error.Item.show : Parsec.Error.Item -> String
  (e) e<() String>
  | (xs) String.quote(xs);
  | (xs) String.concat("label ")(xs);
  | "end of input";


Parsec.Error.Item.tokens: String -> Parsec.Error.Item
  (xs)
  <P> (tokens) () () tokens(xs)

// A parser error can be one of two things:
// - a trivial or internal error with
//   - the index at which the error occured
//   - possibly the unexpected input the parser didn't know how to process
//   - a list of things the parser did expect to see at that that index
// - a fancy, or user specified, errror with
//  - the index at which the error occured
//  - a list of custom messages (eihter type String or type E) at that index
Parsec.Error : Type -> Type
  (E)
  parser.error<P: Parsec.Error(E) -> Type> ->
  (trivial:
    (position: Nat) ->
    (unexpect: Maybe(Parsec.Error.Item)) ->
    (expected: List(Parsec.Error.Item))  ->
    P(Parsec.Error.make_trivial<E>(position)(unexpect)(expected))
  ) ->
  (fancy:
    (position: Nat) ->
    (messages: List(Parsec.Error.Fancy(E))) ->
    P(Parsec.Error.make_fancy<E>(position)(messages))
  ) ->
  P(parser.error)


Parsec.Error.index:
  <E: Type> ->
  Parsec.Error(E) ->
  Nat

  <E> (x)

  x<() Nat>
  | (x.pos) (x.unx) (x.exp) x.pos;
  | (x.pos) (x.msg) x.pos;

Parsec.Error.make_fancy:
  <E: Type> ->
  Nat ->
  List(Parsec.Error.Fancy(E)) ->
  Parsec.Error(E)

  <E> (position) (messages)
  <P> () (fancy) fancy(position)(messages)

Parsec.Error.make_trivial:
  <E: Type> ->
  Nat ->
  Maybe(Parsec.Error.Item) ->
  List(Parsec.Error.Item) ->
  Parsec.Error(E)

  <E> (position) (unexpect) (expected)
  <P> (trivial) () trivial(position)(unexpect)(expected)

// When a parser branches and tries different possible options on its input
// we need some way to combine the errors that each branch generates.
// Because branches that consume more input are better than those that do less
// the errors from farther along the input are more useful.
// Thus to merge errors we compare positions and throw away the earlier error.
// If both errors occur at the same place though, we prefer fancy errors.
// If both errors are fancy at the same place, we merge the messages.
// If both errors are trivial at the same place, we merge the expected items.
// (We also try to prefer the presence of an unexpected token over its absence)

Parsec.Error.merge:
  <E: Type> ->
  Parsec.Error(E) ->
  Parsec.Error(E) ->
  Parsec.Error(E)

  <E> (x) (y)
  let x.index = Parsec.Error.index<E>(x)
  let y.index = Parsec.Error.index<E>(y)
  Nat.cmp(x.index)(y.index)<() Parsec.Error(E)>
  | y;
  | x<() Parsec.Error(E)> 
    |#trivial# (x.pos) (x.unx) (x.exp)
      y<() Parsec.Error(E)>
      |#trivial# (y.pos) (y.unx) (y.exp)
        Parsec.Error.make_trivial<E>(x.pos)
        | x.unx<() Maybe(Parsec.Error.Item)> | y.unx; | () x.unx;; // TODO: Ord
        | List.concat<Parsec.Error.Item>(x.exp)(y.exp);;
      |#fancy#   (y.pos) (y.msg) y;;
    |#fancy# (x.pos) (x.msg)
      y<() Parsec.Error(E)>
      |#trivial# (y.pos) (y.unx) (y.exp) x;
      |#fancy#   (y.pos) (y.msg)
        Parsec.Error.make_fancy<E>(x.pos)
        | List.concat<Parsec.Error.Fancy(E)>(x.msg)(y.msg);;;;
  | x;


Parsec.Error.show: <E : Type> -> (E -> String) -> Parsec.Error(E) -> String
  <E> (f) (e)
  e<() String>
  | (position) (unexpect) (expected) "trivial";
  | (position) (messages) "fancy";

Parsec.Reply.eaten_error :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.State(S)(E) ->
  Parsec.Error(E) ->
  Parsec.Reply(S)(E)(A)

  <S> <E> <A> (state) (error)
  <P> () () () (eaten_error) eaten_error(state)(error)

Parsec.Reply.eaten_value :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.State(S)(E) ->
  A ->
  Parsec.Reply(S)(E)(A)

  <S> <E> <A> (state) (value)
  <P> () () (eaten_value) () eaten_value(state)(value)

Parsec.Reply.empty_error :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.State(S)(E) ->
  Parsec.Error(E) ->
  Parsec.Reply(S)(E)(A)

  <S> <E> <A> (state) (error)
  <P> () (empty_error) () () empty_error(state)(error)

Parsec.Reply.empty_value :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.State(S)(E) ->
  A ->
  Parsec.Reply(S)(E)(A)

  <S> <E> <A> (state) (value)
  <P> (empty_value) () () () empty_value(state)(value)

// A parser reply represents the four possible outputs for a parser
// - empty_value when the parser returns a value and input was not consumed
// - empty_error when the parser throws an error and input was not consumed
// - eaten_value when the parser returns a value and input was consumed
// - eaten_error when the parser throws an error and input was consumed

Parsec.Reply : Type -> Type -> Type -> Type
  (S) (E) (A)
  parser_reply<P: Parsec.Reply(S)(E)(A) -> Type> ->
  (empty_value:
    (state: Parsec.State(S)(E)) ->
    (value: A)    ->
    P(Parsec.Reply.empty_value<S><E><A>(state)(value))
  ) ->
  (empty_error:
    (state: Parsec.State(S)(E)) ->
    (error: Parsec.Error(E))    ->
    P(Parsec.Reply.empty_error<S><E><A>(state)(error))
  ) ->
  (eaten_value:
    (state: Parsec.State(S)(E)) ->
    (value: A)    ->
    P(Parsec.Reply.eaten_value<S><E><A>(state)(value))
  ) ->
  (eaten_error:
    (state: Parsec.State(S)(E)) ->
    (error: Parsec.Error(E))    ->
    P(Parsec.Reply.eaten_error<S><E><A>(state)(error))
  ) ->
  P(parser_reply)

// We can collapse a parser reply to an Either by throwing away consumption info

Parsec.Reply.to_either:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.Reply(S)(E)(A) ->
  Either(Parsec.Error(E))(A)

  <S> <E> <A> (reply)
  reply<() Either(Parsec.Error(E))(A)>
  | () (a) Either.right<Parsec.Error(E)><A>(a);
  | () (e) Either.left<Parsec.Error(E)><A>(e);
  | () (a) Either.right<Parsec.Error(E)><A>(a);
  | () (e) Either.left<Parsec.Error(E)><A>(e);


// by default, a parser state has its index at zero and no errors
Parsec.State.default:
  <S: Type> ->
  <E: Type> ->
  String ->
  S ->
  Parsec.State(S)(E)

  <S> <E> (input) (state)
  <P> (make) make(input)(Nat.zero)(List.nil<Parsec.Error(E)>)(state)

// A parser state contains 5 things
// - the remaining string input to parse
// - the index that the remaining input began at when we started parsing
// - a list of errors we've accumulated at our current index
// - a custom state value that the user can embed into the parser if they like

Parsec.State: Type -> Type -> Type
  (S) (E)
  parser_state<P: Parsec.State(S)(E) -> Type> ->
  (make: (input: String) ->
         (index: Nat)    ->
         (error: List(Parsec.Error(E))) ->
         (state: S)      ->
         P(Parsec.State.make<S><E>(input)(index)(error)(state))
  ) ->
  P(parser_state)


// We compare two states and return the one farthest from the start of the input

Parsec.State.longest_match:
  <S: Type> ->
  <E: Type> ->
  Parsec.State(S)(E) ->
  Parsec.State(S)(E) ->
  Parsec.State(S)(E)

  <S> <E> (x) (y)
  x<() Parsec.State(S)(E)> | (x.input) (x.index) (x.error) (x.state)
  y<() Parsec.State(S)(E)> | (y.input) (y.index) (y.error) (y.state)
  Nat.cmp(x.index)(y.index)<() Parsec.State(S)(E)>
  | y;
  | x;
  | x;;;


Parsec.State.make:
  <S: Type> ->
  <E: Type> ->
  String ->
  Nat ->
  List(Parsec.Error(E)) ->
  S ->
  Parsec.State(S)(E)

  <S> <E> (input) (index) (error) (state)
  <P> (make) make(input)(index)(error)(state)

Parsec.any_char : <S: Type> -> <E: Type> -> Parsec(S)(E)(Char)
  <S> <E>
  Parsec.token<S><E><Char>(Maybe.some<Char>)
  | List.single<Parsec.Error.Item>(Parsec.Error.Item.label("any char"));

// a parser is an applicative
Parsec.ap:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  <B: Type> ->
  Parsec(S)(E)(A -> B) ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(B)

  <S> <E> <A> <B> (pf) (pa)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  pf<X>(s1)
  | (s2) (f) pa<X>(s2)
    | (s3) (a) empty_value(s3)(f(a));
    | empty_error;
    | (s3) (a) eaten_value(s3)(f(a));
    | eaten_error;;
  | empty_error;
  | (s2) (f) pa<X>(s2)
    | (s3) (a) eaten_value(s3)(f(a));
    | eaten_error;
    | (s3) (a) eaten_value(s3)(f(a));
    | eaten_error;;
  | eaten_error;

// a parser is a monad
Parsec.bind:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  <B: Type> ->
  Parsec(S)(E)(A) ->
  (A -> Parsec(S)(E)(B)) ->
  Parsec(S)(E)(B)

  <S> <E> <A> <B> (pa) (pf)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  pa<X>(s1)
  | (s2) (a) pf(a)<X>(s2)
    | (s3) (b) empty_value(s3)(b);
    | empty_error;
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;;
  | empty_error;
  | (s2) (a) pf(a)<X>(s2)
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;;
  | eaten_error;

Parsec.char : <S: Type> -> <E: Type> -> Char -> Parsec(S)(E)(Char)
  <S> <E> (c)
  Parsec.token<S><E><Char>
  | (x) U16.eql(c)(x)<() Maybe(Char)>
    | Maybe.some<Char>(c);
    | Maybe.none<Char>;;
  | List.single<Parsec.Error.Item>
    | Parsec.Error.Item.tokens(String.single(c));;

// take a list of parsers and try them until one consumes input or succeeds
Parsec.choice:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  List(Parsec(S)(E)(A)) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (ps)
  ps<() Parsec(S)(E)(A)>
  | Parsec.zero<S><E><A>;
  | (head) (tail) Parsec.plus<S><E><A>(head)(Parsec.choice<S><E><A>(tail));

// parse the end of the input
Parsec.eof : <S: Type> -> <E: Type> -> Parsec(S)(E)(Unit)
  <S> <E>

  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  s1<() X> | (input) (index) (error) (state)
  input<() X>
  | empty_value(s1)(Unit.new);
  | (head) ()
    empty_error(s1) | Parsec.Error.make_trivial<E>
    | index;
    | Maybe.some<Parsec.Error.Item>
      | Parsec.Error.Item.tokens(String.single(head));;
    | List.single<Parsec.Error.Item>(Parsec.Error.Item.end_of_input);;;;

// Throw a custom error message

Parsec.fail:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  String ->
  Parsec(S)(E)(A)

  <S> <E> <A> (msg)
  <X> (s) () (empty_error) () ()
  s<() X>
  | () (index) () ()
    let e = List.single<Parsec.Error.Fancy(E)>(Parsec.Error.Fancy.fail<E>(msg))
    empty_error(s)(Parsec.Error.make_fancy<E>(index)(e));

// A parser is a continuation that says
// For custom State type S, custom Error type E, and return type A,
// For all possible continuation types B (i.e. all possible parser compositions)
// We take a Parsec.State with custom state and errors 
// and run one of four possible continuation functions on it
// - empty_value (EOK) processes a state and a  value when no input was consumed
// - empty_error (EER) processes a state and an error when no input was consumed
// - eaten_value (COK) processes a state and a  value when input was consumed
// - eaten_error (CER) processes a state and an error when input was consumed

Parsec : (S : Type) -> (E : Type) -> (A: Type) -> Type
  (S) (E) (A)
    <B : Type> ->
    Parsec.State(S)(E) ->
    (Parsec.State(S)(E) -> A -> B) ->
    (Parsec.State(S)(E) -> Parsec.Error(E) -> B) ->
    (Parsec.State(S)(E) -> A -> B) ->
    (Parsec.State(S)(E) -> Parsec.Error(E) -> B) ->
    B





Parsec.get_state: <S: Type> -> <E: Type> -> Parsec(S)(E)(Parsec.State(S)(E))
  <S> <E>
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  empty_value(s1)(s1)

// attach a label to a parser that shows in the un/expected error items

Parsec.label :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  String ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (label) (p)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  p<X>(s1)
  | empty_value;
  | (s2) (e)
    e<() X>
    | (pos) (us) ()
      empty_error(s2)
      | let es = List.single<Parsec.Error.Item>(Parsec.Error.Item.label(label))
        Parsec.Error.make_trivial<E>(pos)(us)(es);;
    | () () empty_error(s2)(e);;
  | eaten_value;
  | eaten_error;


// We can make a parser from any generic function
// that can process parser states into parser replies

Parsec.make:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  (Parsec.State(S)(E) -> Parsec.Reply(S)(E)(A)) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (f)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  f(s1)<() X>
  | (s2) (a) empty_value(s2)(a);
  | empty_error;
  | (s2) (a) eaten_value(s2)(a);
  | eaten_error;

Parsec.many:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(List(A))
  <S> <E> <A> (p)
  Parsec.bind<S><E><Maybe(A)><List(A)>
  | Parsec.optional<S><E><A>(p);
  | (x) x<() Parsec(S)(E)(List(A))>
    | Parsec.pure<S><E><List(A)>(List.nil<A>);
    | (a) Parsec.map<S><E><List(A)><List(A)>
      | List.cons<A>(a);
      | Parsec.many<S><E><A>(p);;;



Parsec.many_till:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  <B: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(B) ->
  Parsec(S)(E)(List(A))
  <S> <E> <A> <B> (p) (q)
  Parsec.plus<S><E><List(A)>
  | Parsec.then<S><E><B><List(A)>(q)(Parsec.pure<S><E><List(A)>(List.nil<A>));
  | Parsec.bind<S><E><A><List(A)>(p) | (x)
    Parsec.bind<S><E><List(A)><List(A)>(Parsec.many_till<S><E><A><B>(p)(q))
    | (xs) Parsec.pure<S><E><List(A)>(List.cons<A>(x)(xs));;;


// A parser is a functor
Parsec.map:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  <B: Type> ->
  (A -> B) ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(B)

  <S> <E> <A> <B> (f) (p)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  p<X>(s1)
  | (s2) (a) empty_value(s2)(f(a));
  | empty_error;
  | (s2) (a) eaten_value(s2)(f(a));
  | eaten_error;

// We can observe an error so that we can try to handle it
Parsec.observing:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(Either(Parsec.Error(E))(A))

  <S> <E> <A> (p)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  p<X>(s1)
  | (s2) (x) empty_value(s2)(Either.right<Parsec.Error(E)><A>(x));
  | (s2) (e) empty_value(s2)(Either.left<Parsec.Error(E)><A>(e));
  | (s2) (x) eaten_value(s2)(Either.right<Parsec.Error(E)><A>(x));
  | (s2) (e) eaten_value(s2)(Either.left<Parsec.Error(E)><A>(e));

Parsec.optional:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(Maybe(A))

  <S> <E> <A> (p)
  Parsec.plus<S><E><Maybe(A)>
  | Parsec.map<S><E><A><Maybe(A)>(Maybe.some<A>)(p);
  | Parsec.pure<S><E><Maybe(A)>(Maybe.none<A>);


// with dependent types, we can reason that a successful parser returns an A
// and an unsuccessful parser returns a lifted Parsec.Error(E) value
// (`The` lifts the Parsec.Error into a type so we can see it at compile time)

Parsec.parse:
  <S : Type> ->
  <E : Type> ->
  <A: Type> ->
  (p: Parsec(S)(E)(A)) ->
  (s: Parsec.State(S)(E)) ->
  Parsec.type(S)(E)(A)(Parsec.run<S><E><A>(p)(s))

  <S> <E> <A> (p) (s)
  Parsec.run<S><E><A>(p)(s)<(t) Parsec.type(S)(E)(A)(t)>
  | () (x) x;
  | () (e) e;
  | () (x) x;
  | () (e) e;



// we can look ahead in the input stream and not consume any input
// if the parser succeeds

Parsec.peek:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (p)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  p<X>(s1)
  | (s2) (a) empty_value(s1)(a);
  | empty_error;
  | (s2) (a) empty_value(s1)(a);
  | eaten_error;

// We can combine two parsers by trying to apply the first one and,
// if it fails consuming no input, we apply the second one.
// If the second one fails, we merge the states and errors
// (merging always favors the state and error farthest along the input).
Parsec.plus:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (p) (q)

  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  p<X>(s1)
  | empty_value;
  | (s2) (p.err) q<X>(s1)
    | empty_value;
    | (s3) (q.err) empty_error
      | Parsec.State.longest_match<S><E>(s2)(s3);
      | Parsec.Error.merge<E>(p.err)(q.err);;
    | eaten_value;
    | (s3) (q.err) empty_error
      | Parsec.State.longest_match<S><E>(s2)(s3);
      | Parsec.Error.merge<E>(p.err)(q.err);;;
  | eaten_value;
  | eaten_error;


// We can turn any value into a parser that returns that value
// without consuming any input.

Parsec.pure:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  (a: A) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (a)
  <X> (s) (empty_value) () () () empty_value(s)(a)

// Running a parser is applying it to a Parsec.State and
// the four possible Parsec.Reply constructors
// This sets `B` from the `Parsec` definition as Parsec.Reply
// which terminates the chain of continuations

Parsec.run :
  <S : Type> ->
  <E : Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec.State(S)(E) ->
  Parsec.Reply(S)(E)(A)

  <S> <E> <A> (p) (s)
  p<Parsec.Reply(S)(E)(A)>(s)
  | Parsec.Reply.empty_value<S><E><A>;
  | Parsec.Reply.empty_error<S><E><A>;
  | Parsec.Reply.eaten_value<S><E><A>;
  | Parsec.Reply.eaten_error<S><E><A>;


// we can run a parser on a default state and either get an error or a value
Parsec.run_default:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  String ->
  S ->
  Either(Parsec.Error(E))(A)

  <S> <E> <A> (p) (str) (s)
  Parsec.Reply.to_either<S><E><A>
  | Parsec.run<S><E><A>(p)(Parsec.State.default<S><E>(str)(s));



Parsec.skip_many:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(Unit)
  <S> <E> <A> (p)
  Parsec.plus<S><E><Unit>
  | Parsec.then<S><E><A><Unit>(p)(Parsec.skip_many<S><E><A>(p));
  | Parsec.pure<S><E><Unit>(Unit.new);


// Take a number of characters, error with a custom label if we hit end of input

Parsec.take:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  String    ->
  Nat ->
  Parsec(S)(E)(String)

  <S> <E> <A> (err) (n)
  <X> (s1) (empty_value) (empty_error) (eaten_value) ()
  s1<() X> | (input) (index) (error) (state)
  String.take_n(n)(input)<() X> 
  | empty_error(s1) | Parsec.Error.make_trivial<E>
    | index;
    | Maybe.some<Parsec.Error.Item>(Parsec.Error.Item.end_of_input);
    | List.single<Parsec.Error.Item>(Parsec.Error.Item.label(err));;;
  | (p) p<() X> | (took) (rest)
    let s2  = Parsec.State.make<S><E>(rest)(Nat.add(index)(n))(error)(state)
    eaten_value(s2)(took);;;



// take characters while a condition is true (can return no characters)
Parsec.take_while:
  <S: Type> ->
  <E: Type> ->
  (Char -> Bool) ->
  Parsec(S)(E)(String)

  <S> <E> (f)
  <X> (s1) (empty_value) (empty_error) (eaten_value) ()
  s1<() X> | (input) (index) (error) (state)
  String.take_while(f)(input)<() X> | (took) (rest)
  let len = String.length(took)
  let s2  = Parsec.State.make<S><E>(rest)(Nat.add(index)(len))(error)(state)
  took<() X>
  | empty_value(s2)(took);
  | () () eaten_value(s2)(took);;;


// take at least one character while a condition is true

Parsec.take_while1:
  <S: Type> ->
  <E: Type> ->
  String    ->
  (Char -> Bool) ->
  Parsec(S)(E)(String)

  <S> <E> (err) (f)
  <X> (s1) (empty_value) (empty_error) (eaten_value) ()
  s1<() X> | (input) (index) (error) (state)
  String.take_while(f)(input)<() X> | (took) (rest)
  let len = String.length(took)
  let s2  = Parsec.State.make<S><E>(rest)(Nat.add(index)(len))(error)(state)
  took<() X>
  | input<() X>
    | empty_error(s2) | Parsec.Error.make_trivial<E>
      | index;
      | Maybe.some<Parsec.Error.Item>(Parsec.Error.Item.end_of_input);
      | List.single<Parsec.Error.Item>(Parsec.Error.Item.label(err));;;
    | (head) ()
      empty_error(s2) | Parsec.Error.make_trivial<E>
      | index;
      | Maybe.some<Parsec.Error.Item>
        | Parsec.Error.Item.tokens(String.single(head));;
      | List.single<Parsec.Error.Item>(Parsec.Error.Item.label(err));;;;
  | () () eaten_value(s2)(took);;;



// an example of how to use a dependently typed parser

Parsec.test1 : String
  Parsec.parse<Unit><Unit><String>
//    | Unit.show;
    | Parsec.tokens<Unit><Unit>("a");
    | Parsec.State.default<Unit><Unit>
      | "a";
      | Unit.new;;




// a parser is a monad
Parsec.then:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  <B: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(B) ->
  Parsec(S)(E)(B)

  <S> <E> <A> <B> (pa) (pb)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  pa<X>(s1)
  | (s2) (a) pb<X>(s2)
    | (s3) (b) empty_value(s3)(b);
    | empty_error;
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;;
  | empty_error;
  | (s2) (a) pb<X>(s2)
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;
    | (s3) (b) eaten_value(s3)(b);
    | eaten_error;;
  | eaten_error;

// throw a parse error while consuming no input

Parsec.throw :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec.Error(E) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (e)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  empty_error(s1)(e)


// parse a single character with a validator function 
// and a list of expected tokens

Parsec.token:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  (Char -> Maybe(A)) ->
  List(Parsec.Error.Item) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (f) (es)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  s1<() X> | (input) (index) (error) (state)
  input<() X>
  | let unex = Maybe.some<Parsec.Error.Item>(Parsec.Error.Item.end_of_input)
    empty_error(s1)(Parsec.Error.make_trivial<E>(Nat.zero)(unex)(es));
  | (c) (cs)
    f(c)<() X>
    | let item = Parsec.Error.Item.tokens(String.single(c))
      let unex = Maybe.some<Parsec.Error.Item>(item)
      empty_error(s1)(Parsec.Error.make_trivial<E>(index)(unex)(es));
    | (x)
      let s2 = Parsec.State.make<S><E>(cs)(Nat.succ(index))(error)(state)
      eaten_value(s2)(x);;;


// match a literal string
Parsec.tokens:
  <S: Type> ->
  <E: Type> ->
  String    ->
  Parsec(S)(E)(String)

  <S> <E> (str)
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  s1<() X> | (input) (index) (error) (state)
  let len = String.length(str)
  String.take_n(len)(input)<() X>
  | let unex = Maybe.some<Parsec.Error.Item>(Parsec.Error.Item.end_of_input)
    let expe = List.single<Parsec.Error.Item>
      | Parsec.Error.Item.label(String.quote(str));
    empty_error(s1)(Parsec.Error.make_trivial<E>(Nat.zero)(unex)(expe));
  | (p) p<() X> | (took) (rest)
    let s2 = Parsec.State.make<S><E>(rest)(Nat.add(index)(len))(error)(state)
    String.eql(str)(took)<() X>
    | str<() X>
      | empty_value(s2)(str);
      | () () eaten_value(s2)(str);;
    | let expe_label = Parsec.Error.Item.label(String.quote(str))
      let unex = took<() Maybe(Parsec.Error.Item)>
        | Maybe.none<Parsec.Error.Item>;
        | () () Maybe.some<Parsec.Error.Item>(Parsec.Error.Item.tokens(took));
      let expe = List.single<Parsec.Error.Item>(expe_label)
      empty_error(s1)(Parsec.Error.make_trivial<E>(index)(unex)(expe));;;;


// try to apply a parser, if it fails, it consumes no input

Parsec.try :
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A) ->
  Parsec(S)(E)(A)

  <S> <E> <A> (p)
  <X> (s1) (empty_value) (empty_error) (eaten_value) ()
  p<X>(s1)
  | empty_value;
  | (s2) (e) empty_error(s1)(e);
  | eaten_value;
  | (s2) (e) empty_error(s1)(e);

// A dependent type of parser reply for use by Parsec.parse

Parsec.type: (S: Type) -> (E: Type) -> (A: Type) -> Parsec.Reply(S)(E)(A) -> Type
  (S) (E) (A) (reply)
  reply<() Type>
  | () () A;
  | () (e) Parsec.Error(E);
  | () () A;
  | () (e) Parsec.Error(E);

// an empty parser that always fails consuming no input and showing no error
Parsec.zero:
  <S: Type> ->
  <E: Type> ->
  <A: Type> ->
  Parsec(S)(E)(A)

  <S> <E> <A>
  <X> (s1) (empty_value) (empty_error) (eaten_value) (eaten_error)
  s1<() X> | () (index) () ()
  let e = Parsec.Error.make_trivial<E>
          | index;
          | Maybe.none<Parsec.Error.Item>;
          | List.nil<Parsec.Error.Item>;
  empty_error(s1)(e);