Problem with bind and contexts

[jwiegley]

I have the following code right now:

Require Import Category.
Require Import Sized.
Require Import Combinators.
Require Import Numbers.
Require Import NEList.

Require Import Coq.NArith.NArith.
Require Import Coq.QArith.QArith.

Require Import Ascii.
Local Open Scope char.

Require Import Coq.Lists.List.
Import ListNotations.

Section Helpers.

Context
  {M : Type -> Type}
  `{RF : RawFunctor M}
  `{RA : RawApplicative M}
  `{RM : RawMonad M}
  `{RT : RawAlternative M}
  {Chars : nat -> Type} `{Sized Chars ascii}
  {n : nat}.

Definition decimal_digit_N : Parser Chars ascii M N n :=
  alts ((0 <$ exact "0")%N
     :: (1 <$ exact "1")%N
     :: (2 <$ exact "2")%N
     :: (3 <$ exact "3")%N
     :: (4 <$ exact "4")%N
     :: (5 <$ exact "5")%N
     :: (6 <$ exact "6")%N
     :: (7 <$ exact "7")%N
     :: (8 <$ exact "8")%N
     :: (9 <$ exact "9")%N
     :: nil).

Definition decimal_N : Parser Chars ascii M N n :=
  let convert ds := foldl (fun ih d => 10 * ih + d)%N ds 0%N
  in Combinators.map convert (nelist decimal_digit_N).

Definition float_Q : Parser Chars ascii M Q n :=
  decimal_N >>= fun x : N =>
    match x return Parser Chars ascii M Q n with
    | N0 => (Qmake <$> decimal_int) <*> pure 1%positive
    | Npos p => (Qmake <$> decimal_int) <*> pure p
    end.

End Helpers.

When I tried to type check float_Q, I get:

Error:
Unable to satisfy the following constraints:
In environment:
M : Type -> Type
RF, H : RawFunctor M
RA : RawApplicative M
H0 : RawFunctor M
H1 : RawApplicative M
RM : RawMonad M
H2 : RawFunctor M
H3 : RawApplicative M
RT : RawAlternative M
Chars : nat -> Type
H4 : Sized Chars ascii
n : nat
x : N

?F : "Type -> Type"

?H : "RawFunctor ?F"

?H0 : "RawApplicative ?F"

As you can see, there are somehow three RawFunctor M instances in scope, which I don't quite understand. I've tried various combinations of explicit arguments, but I was wondering if you could help me understand what I'm doing wrong here?

[gallais]

One of the design decisions of this library is that all the Parsers you can define have to consume some of their input. This makes deciding whether it is safe to perform a recursive call trivial (if you have already run a first parser, then you can go ahead).

As a consequence it is not possible to write pure : A -> Parser Toks Tok M A. Here Coq looks for an instance of Applicative (Parser Toks Tok M) because you used pure but can't find one because there isn't any (the instances in context are for the underlying monad M, there are 3 instances for RawFunctor M because there's the one you declared but also the ones that appear as constraints of RawApplicative M and RawMonad M).

You can define this parser like so: instead of using f <$> a <*> pure b, you can write (fun x => f x b) <$> a.

Definition float_Q : Parser Chars ascii M Q n :=
  decimal_N >>= fun x : N =>
    match x with
    | N0     => (fun x => Qmake x 1%positive) <$> decimal_int
    | Npos p => (fun x => Qmake x p)          <$> decimal_int
    end.

[gallais]

Alternatively, because there is no real control flow dependency between the value of x and the parser that gets run afterwards, you could have:

Definition float_Q_cast (x : N) (y : Z) : Q :=
  Qmake y (match x with
   | N0     => 1
   | Npos p => p end).

Definition float_Q' : Parser Chars ascii M Q n :=
  (float_Q_cast <$> decimal_N) <*> decimal_int.

[jwiegley]

Well, look at that. Thanks for the fast response! I'm getting closer and closer to something that works... :)

[jwiegley]

@gallais Success! I still have a bit of math to do inside float_Q, but that's the trivial part:

Require Import Category.
Require Import Sized.
Require Import Combinators.
Require Import Numbers.
Require Import NEList.
Require Import Char.
Require Import Running.
Require Import Indexed.

Require Import Coq.NArith.NArith.
Require Import Coq.QArith.QArith.
Require Import Coq.Strings.String.

Require Import Ascii.
Local Open Scope char.

Require Import Coq.Lists.List.

Section Helpers.

Context
  {M : Type -> Type}
  `{RF : RawFunctor M}
  `{RA : RawApplicative M}
  `{RM : RawMonad M}
  `{RT : RawAlternative M}
  {Chars : nat -> Type} `{Sized Chars ascii}
  {n : nat}.

Definition decimal_digit_N : Parser Chars ascii M N n :=
  alts ((0 <$ exact "0")%N
     :: (1 <$ exact "1")%N
     :: (2 <$ exact "2")%N
     :: (3 <$ exact "3")%N
     :: (4 <$ exact "4")%N
     :: (5 <$ exact "5")%N
     :: (6 <$ exact "6")%N
     :: (7 <$ exact "7")%N
     :: (8 <$ exact "8")%N
     :: (9 <$ exact "9")%N
     :: nil).

Definition decimal_N : Parser Chars ascii M N n :=
  let convert ds := foldl (fun ih d => 10 * ih + d)%N ds 0%N
  in Combinators.map convert (nelist decimal_digit_N).

Definition float_Q : Parser Chars ascii M Q n :=
  ((fun x '(y, z) =>
      Qmake x (match z with
               | N0 => 1
               | Npos x => x
               end))
    <$> (decimal_int <& exact "."))
    <*> ((((fun x y => (length (toList x), y))
             <$> nelist (0 <$ exact "0")%N)
            <*> decimal_N)
           <|> ((fun x => (0%nat, x))
                  <$> decimal_N)).

End Helpers.

Section ArithmeticLanguage.

Context
  {Toks : nat -> Type} `{Sized Toks ascii}
  {M : Type -> Type} `{RawMonad M} `{RawAlternative M}.

Record Coords := {
  coordTime      : N;
  coordLatitude  : Q;
  coordLongitude : Q
}.

Record Language (n : nat) : Type := MkLanguage
  { _expr : Parser Toks ascii M (NEList Coords) n
  }.

Arguments MkLanguage {_}.

Definition language (n : nat) : Language n :=
  MkLanguage
    (nelist
       (((Build_Coords
            <$> (decimal_N <& spaces))
           <*> (float_Q <& spaces))
          <*> (float_Q <& space))).

Definition expr : [ Parser Toks ascii M (NEList Coords) ] :=
  fun n => _expr n (language n).

Definition float_expr : [ Parser Toks ascii M Q ] :=
  fun n => @float_Q _ _ _ _ _ _ _ _ _ n.

End ArithmeticLanguage.

Lemma test_float_Q : check "10.2" float_expr.
Proof.
  vm_compute; constructor.
Qed.

Definition newline := String "013"%char EmptyString.

Lemma test_expr : check ("10 10.2 10.2" ++ newline ++
                         "10 10.2 10.2" ++ newline)%string expr.
Proof.
  vm_compute; constructor.
Qed.

[jwiegley]

The float_Q_cast is much cleaner, but I still need to track how many zeroes occurred after the decimal point, so I know what to multiply the numerator by. And it needs to parse the period. :)

[gallais]

Nice! This is what I'd do:

Definition float_Q_cast : (Z * option (NEList ascii) * N) -> Q :=
  fun '((x , zeros) , z) =>
  Qmake x (match z with | N0 => 1 | Npos p => p end).

Definition float_Q : Parser Chars ascii M Q n :=
  float_Q_cast
  <$> decimal_int
  <&> (char "." &?> nelist (char "0"))
  <&> decimal_N.

The idea is that a parser for a (potentially empty) list is a parser for a NEList which is allowed to fail. Hence the use of the <&?> conjunction which doesn't mind having an unsuccessful second component.

My strategy in general is to collect all the data by using various <&> variants and then have a function putting the subparts together.

Btw: I didn't know about fun '(x , y) => ... to pattern-match on the fly on pairs and had been using fun p => let (x , y) := p in .... Thanks for the tip!