From 43bd556e3fe1354721b46fa124e6bdeed9f4afda Mon Sep 17 00:00:00 2001
From: raoxiaojia <raoxiaojia@gmail.com>
Date: Fri, 20 Mar 2026 09:22:51 -0700
Subject: [PATCH] implementations of error reporting, positions, and branch
 committing

---
 _RocqProject      |  3 +++
 src/Category.v    | 25 ++++++++++++++++++
 src/Char.v        |  1 +
 src/Combinators.v | 21 ++++++++++++++-
 src/Examples.v    | 62 +++++++++++++++++++++++++++++++++++++++++--
 src/Monad.v       | 61 ++++++++++++++++++++++++++++++++++++++++++
 src/Numbers.v     |  1 +
 src/Parseque.v    |  2 +-
 src/Position.v    | 58 ++++++++++++++++++++++++++++++++++++++++
 src/Result.v      | 67 +++++++++++++++++++++++++++++++++++++++++++++++
 src/Running.v     | 27 ++++++++++++++++++-
 11 files changed, 323 insertions(+), 5 deletions(-)
 create mode 100644 src/Monad.v
 create mode 100644 src/Position.v
 create mode 100644 src/Result.v

diff --git a/_RocqProject b/_RocqProject
index 5633f80..7a0b5a9 100644
--- a/_RocqProject
+++ b/_RocqProject
@@ -7,9 +7,12 @@ src/EqDec.v
 src/Examples.v
 src/Indexed.v
 src/Induction.v
+src/Monad.v
 src/NEList.v
 src/Numbers.v
 src/Parseque.v
+src/Position.v
+src/Result.v
 src/Running.v
 src/Sized.v
 src/StringAsList.v
diff --git a/src/Category.v b/src/Category.v
index 537323f..2449fe0 100644
--- a/src/Category.v
+++ b/src/Category.v
@@ -40,6 +40,31 @@ end.
 
 Arguments MkRawAlternative {_} {_} {_}.
 
+Class RecordToken (M : Type -> Type) (Tok : Type) :=
+  MkRecordToken { _recordToken : Tok -> M unit }.
+
+Definition recordToken {M : Type -> Type} {Tok : Type} `{RecordToken M Tok} : Tok -> M unit :=
+  _recordToken.
+
+Arguments MkRecordToken {_} {_}.
+
+#[global]
+Instance defaultRecordToken (M : Type -> Type) `{RawApplicative M} (Tok : Type)
+  : RecordToken M Tok | 100 :=
+  MkRecordToken (fun _ => pure tt).
+
+Class RawCommit (M : Type -> Type) :=
+  MkRawCommit { _commit : forall A, M A -> M A }.
+
+Definition commit {M : Type -> Type} `{RawCommit M} {A : Type} : M A -> M A :=
+  _commit _.
+
+Arguments MkRawCommit {_}.
+
+#[global]
+Instance defaultRawCommit (M : Type -> Type) : RawCommit M | 100 :=
+  MkRawCommit (fun _ x => x).
+
 Class RawMonad (F : Type -> Type) `{RawApplicative F} :=
   MkRawMonad { _bind : forall A B, F A -> (A -> F B) -> F B }.
 
diff --git a/src/Char.v b/src/Char.v
index 1691935..db588cf 100644
--- a/src/Char.v
+++ b/src/Char.v
@@ -9,6 +9,7 @@ Section Char.
 Context
   {Chars : nat -> Type} `{Sized Chars ascii}
   {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
+  `{RecordToken M ascii}
   {A : Type} {n : nat}.
 
 Definition char (c : ascii) : Parser Chars ascii M ascii n := exact c.
diff --git a/src/Combinators.v b/src/Combinators.v
index 6255954..9a82fc7 100644
--- a/src/Combinators.v
+++ b/src/Combinators.v
@@ -33,10 +33,15 @@ Section Combinators1.
 Context
   {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
   {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
+  `{RecordToken M Tok}
   {A B : Type} {n : nat}.
 
 Definition anyTok : Parser Toks Tok M Tok n :=
- MkParser (fun m mlen ts => fromOption (getTok ts)).
+ MkParser (fun m mlen ts =>
+   match getTok ts with
+   | None   => fail
+   | Some s => fmap (fun _ => s) (recordToken (value s))
+   end).
 
 Definition guardM (f : A -> option B) (p : Parser Toks Tok M A n) :
   Parser Toks Tok M B n :=
@@ -91,6 +96,7 @@ Section Combinators2.
 Context
   {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
   {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
+  `{RecordToken M Tok}
   {A B : Type} {n : nat}.
 
 Definition ands (ps : NEList (Parser Toks Tok M A n)) : Parser Toks Tok M (NEList A) n :=
@@ -138,6 +144,7 @@ Section Combinators3.
 Context
   {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok} `{EqDec Tok}
   {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
+  `{RecordToken M Tok}
   {A B C : Type} {n : nat}.
 
 Definition app (p : Parser Toks Tok M (A -> B) n)
@@ -162,6 +169,18 @@ Definition betweenm (open : Parser Toks Tok M A n) (close : Box (Parser Toks Tok
 
 End Combinators3.
 
+Section Commit.
+
+Context
+  {Toks : nat -> Type} {Tok : Type}
+  {M : Type -> Type} `{RawCommit M}
+  {A : Type} {n : nat}.
+
+Definition commitP (p : Parser Toks Tok M A n) : Parser Toks Tok M A n :=
+  MkParser (fun _ mlen toks => commit (runParser p mlen toks)).
+
+End Commit.
+
 Section HChainl.
 
 Context
diff --git a/src/Examples.v b/src/Examples.v
index 1f3839c..f113522 100644
--- a/src/Examples.v
+++ b/src/Examples.v
@@ -1,5 +1,5 @@
-From parseque Require Import Running Parseque.
-From Stdlib Require Import Ascii String.
+From parseque Require Import Running Parseque Result Position Monad.
+From Stdlib Require Import Ascii String NArith.
 
 Section ArithmeticLanguage.
 
@@ -52,3 +52,61 @@ Definition test2 : check "1+(2*31-4)" expr := MkSingleton
  (EAdd (EEmb (TEmb (FLit 1)))
              (TEmb (FEmb (ESub (EEmb (TMul (TEmb (FLit 2)) (FLit 31)))
                                            (TEmb (FLit 4)))))).
+
+(* Error reporting examples using ParsequeT *)
+
+Section ErrorReporting.
+
+Local Instance altInst : RawAlternative (ParsequeT Position) :=
+  parsequeTRawAlternative id.
+
+Context
+  {Toks : nat -> Type} `{Sized Toks ascii}
+  {n : nat}.
+
+Definition binary_digit : Parser Toks ascii (ParsequeT Position) nat n :=
+  0 <$ exact "0"%char <|> 1 <$ exact "1"%char.
+
+Definition hex_digit : Parser Toks ascii (ParsequeT Position) nat n :=
+  alts ( (0  <$ exact "0"%char) :: (1  <$ exact "1"%char)
+      :: (2  <$ exact "2"%char) :: (3  <$ exact "3"%char)
+      :: (4  <$ exact "4"%char) :: (5  <$ exact "5"%char)
+      :: (6  <$ exact "6"%char) :: (7  <$ exact "7"%char)
+      :: (8  <$ exact "8"%char) :: (9  <$ exact "9"%char)
+      :: (10 <$ exact "a"%char) :: (11 <$ exact "b"%char)
+      :: (12 <$ exact "c"%char) :: (13 <$ exact "d"%char)
+      :: (14 <$ exact "e"%char) :: (15 <$ exact "f"%char)
+      :: nil).
+
+Definition digits (base : nat) (digit : Parser Toks ascii (ParsequeT Position) nat n) :
+  Parser Toks ascii (ParsequeT Position) nat n :=
+  let convert ds := NEList.foldl (fun ih d => base * ih + d) ds 0
+  in Combinators.map convert (nelist digit).
+
+(* Binary: "0b" prefix, then committed to binary digits *)
+Definition binary : Parser Toks ascii (ParsequeT Position) nat n :=
+  exact "0"%char &> exact "b"%char &>
+    commitP (digits 2 binary_digit).
+
+(* Hexadecimal: "0x" prefix, then committed to hex digits *)
+Definition hexadecimal : Parser Toks ascii (ParsequeT Position) nat n :=
+  exact "0"%char &> exact "x"%char &>
+    commitP (digits 16 hex_digit).
+
+(* Try binary, then hex *)
+Definition number : Parser Toks ascii (ParsequeT Position) nat n :=
+  binary <|> hexadecimal.
+
+End ErrorReporting.
+
+(* "0b101" parses as binary 5 *)
+Definition test3 : checkResult id "0b101" (fun n => number) =
+  inr 5 := eq_refl.
+
+(* "0xff" parses as hex 255 *)
+Definition test4 : checkResult id "0xff" (fun n => number) =
+  inr 255 := eq_refl.
+
+(* "0b0000002": error at "2" (col 8), not at "b" (col 1) *)
+Definition test5 : checkResult id "0b0000002" (fun n => number) =
+  inl (MkPosition 0%N 8%N) := eq_refl.
diff --git a/src/Monad.v b/src/Monad.v
new file mode 100644
index 0000000..5e43346
--- /dev/null
+++ b/src/Monad.v
@@ -0,0 +1,61 @@
+From parseque Require Import Category Result Position.
+From Stdlib Require Import Ascii.
+
+Definition ParsequeT (E A : Type) : Type :=
+  Position -> Result E (A * Position).
+
+Section ParsequeTInstances.
+
+Context {E : Type}.
+
+#[global]
+Instance parsequeTRawFunctor : RawFunctor (ParsequeT E) :=
+  MkRawFunctor (fun _ _ f ma pos =>
+    fmap (fun '(a, pos') => (f a, pos')) (ma pos)).
+
+#[global]
+Instance parsequeTRawApplicative : RawApplicative (ParsequeT E) :=
+  MkRawApplicative
+    (fun _ a pos => Value (a, pos))
+    (fun _ _ mf ma pos =>
+      bind (mf pos) (fun '(f, pos') =>
+      fmap (fun '(a, pos'') => (f a, pos'')) (ma pos'))).
+
+#[global]
+Instance parsequeTRawMonad : RawMonad (ParsequeT E) :=
+  MkRawMonad (fun _ _ ma f pos =>
+    bind (ma pos) (fun '(a, pos') => f a pos')).
+
+Definition getPosition : ParsequeT E Position :=
+  fun pos => Value (pos, pos).
+
+Definition commitT {A : Type} (ma : ParsequeT E A) : ParsequeT E A :=
+  fun pos => commitResult (ma pos).
+
+#[global]
+Instance parsequeTRawCommit : RawCommit (ParsequeT E) :=
+  MkRawCommit (fun _ => commitT).
+
+#[global]
+Instance parsequeTRecordToken : RecordToken (ParsequeT E) ascii :=
+  MkRecordToken (fun c pos => Value (tt, update c pos)).
+
+End ParsequeTInstances.
+
+Section ParsequeTAlternative.
+
+Context {E : Type} (toError : Position -> E).
+
+#[global]
+Instance parsequeTRawAlternative : RawAlternative (ParsequeT E) :=
+  MkRawAlternative
+    (fun _ pos => SoftFail (toError pos))
+    (fun _ ma mb pos =>
+      choice (ma pos) (fun _ => mb tt pos)).
+
+End ParsequeTAlternative.
+
+Arguments parsequeTRawAlternative {_} _.
+
+Definition runParsequeT {E A : Type} (ma : ParsequeT E A) : Result E (A * Position) :=
+  ma start.
diff --git a/src/Numbers.v b/src/Numbers.v
index 70f0a9c..28b8bc5 100644
--- a/src/Numbers.v
+++ b/src/Numbers.v
@@ -9,6 +9,7 @@ Section Numbers.
 
 Context
   {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
+  `{RecordToken M ascii}
   {Chars : nat -> Type} `{Sized Chars ascii}
   {n : nat}.
 
diff --git a/src/Parseque.v b/src/Parseque.v
index 2c4a052..e4439ba 100644
--- a/src/Parseque.v
+++ b/src/Parseque.v
@@ -1 +1 @@
-From parseque Require Export Indexed Category Induction Combinators Sized Char Numbers.
+From parseque Require Export Indexed Category Induction Combinators Sized Char Numbers Result Position Monad.
diff --git a/src/Position.v b/src/Position.v
new file mode 100644
index 0000000..9e4824d
--- /dev/null
+++ b/src/Position.v
@@ -0,0 +1,58 @@
+From Stdlib Require Import Ascii String NArith Lia.
+From Stdlib Require Import List.
+Import ListNotations.
+From Stdlib Require Import Program.Wf Program.Utils.
+From parseque Require Import StringAsList.
+Local Open Scope N_scope.
+
+Record Position : Type :=
+  MkPosition { line : N ; col : N }.
+
+Definition start : Position := MkPosition 0 0.
+
+Definition update (c : ascii) (p : Position) : Position :=
+  if (c =? "010")%char then MkPosition (N.succ (line p)) 0
+  else MkPosition (line p) (N.succ (col p)).
+
+Definition updates (cs : list ascii) (p : Position) : Position :=
+  List.fold_left (fun pos c => update c pos) cs p.
+
+Definition digit_to_ascii (n : N) : ascii :=
+  ascii_of_N (48 + n).
+
+Lemma pos_lt_wf : well_founded Pos.lt.
+Proof.
+  intro p. induction p using Pos.peano_ind.
+  - constructor. intros y Hy. lia.
+  - constructor. intros y Hy.
+    assert (H: (y < p \/ y = p)%positive) by lia.
+    destruct H.
+    + apply IHp. assumption.
+    + subst. exact IHp.
+Qed.
+
+Program Fixpoint pos_to_string_aux (p : positive) (acc : String)
+  {wf Pos.lt p} : String :=
+  let qr := N.pos_div_eucl p 10 in
+  let acc' := digit_to_ascii (snd qr) :: acc in
+  match fst qr with
+  | N0     => acc'
+  | Npos q' => pos_to_string_aux q' acc'
+  end.
+Next Obligation.
+  pose proof (N.pos_div_eucl_spec p 10) as H.
+  destruct (N.pos_div_eucl p 10) as [q r].
+  simpl in *. lia.
+Qed.
+Next Obligation.
+  apply measure_wf. exact pos_lt_wf.
+Defined.
+
+Definition N_to_string (n : N) : String :=
+  match n with
+  | N0     => ["0"]%char
+  | Npos p => pos_to_string_aux p nil
+  end.
+
+Definition show (p : Position) : String :=
+  N_to_string (line p) ++ [":"]%char ++ N_to_string (col p).
diff --git a/src/Result.v b/src/Result.v
new file mode 100644
index 0000000..cd282b7
--- /dev/null
+++ b/src/Result.v
@@ -0,0 +1,67 @@
+From parseque Require Import Category.
+
+Inductive Result (E A : Type) : Type :=
+  | SoftFail : E -> Result E A
+  | HardFail : E -> Result E A
+  | Value    : A -> Result E A.
+
+Arguments SoftFail {_} {_}.
+Arguments HardFail {_} {_}.
+Arguments Value    {_} {_}.
+
+Definition result {E A B : Type} (soft hard : E -> B) (val : A -> B)
+  (r : Result E A) : B :=
+  match r with
+  | SoftFail e => soft e
+  | HardFail e => hard e
+  | Value a    => val a
+  end.
+
+Section Instances.
+
+Context {E : Type}.
+
+#[global]
+Instance resultRawFunctor : RawFunctor (Result E) :=
+  MkRawFunctor (fun _ _ f r =>
+    match r with
+    | SoftFail e => SoftFail e
+    | HardFail e => HardFail e
+    | Value a    => Value (f a)
+    end).
+
+#[global]
+Instance resultRawApplicative : RawApplicative (Result E) :=
+  MkRawApplicative
+    (fun _ a => Value a)
+    (fun _ _ rf ra =>
+      match rf with
+      | SoftFail e => SoftFail e
+      | HardFail e => HardFail e
+      | Value f    => fmap f ra
+      end).
+
+#[global]
+Instance resultRawMonad : RawMonad (Result E) :=
+  MkRawMonad (fun _ _ ra f =>
+    match ra with
+    | SoftFail e => SoftFail e
+    | HardFail e => HardFail e
+    | Value a    => f a
+    end).
+
+Definition choice {A : Type} (ra : Result E A) (fb : unit -> Result E A) : Result E A :=
+  match ra with
+  | SoftFail _ => fb tt
+  | HardFail e => HardFail e
+  | Value a    => Value a
+  end.
+
+End Instances.
+
+Definition commitResult {E A : Type} (r : Result E A) : Result E A :=
+  match r with
+  | SoftFail e => HardFail e
+  | HardFail e => HardFail e
+  | Value a    => Value a
+  end.
\ No newline at end of file
diff --git a/src/Running.v b/src/Running.v
index 6c599ea..de48dca 100644
--- a/src/Running.v
+++ b/src/Running.v
@@ -1,4 +1,4 @@
-From parseque Require Import Category Combinators Sized Numbers Indexed StringAsList Success.
+From parseque Require Import Category Combinators Sized Numbers Indexed StringAsList Success Result Position Monad.
 From Stdlib Require Import String Ascii PeanoNat.
 
 Inductive Singleton (A : Type) : A -> Type :=
@@ -39,3 +39,28 @@ Definition check : string -> [ Parser (SizedList Tok) Tok M A ] -> Type := fun s
   end.
 
 End Check.
+
+Section CheckResult.
+
+Context
+  {Tok : Type} `{Tokenizer Tok}
+  {E : Type} (toError : Position -> E)
+  {A : Type}.
+
+Definition checkResult : string -> [ Parser (SizedList Tok) Tok (ParsequeT E) A ] -> E + A :=
+  fun s p =>
+  let tokens := (fromText s : list Tok) in
+  let n      := List.length tokens in
+  let input  := mkSizedList tokens in
+  let mr     := runParser (p n) (Nat.le_refl n) input in
+  match runParsequeT mr with
+  | SoftFail e => inl e
+  | HardFail e => inl e
+  | Value (s, pos) =>
+    match Success.size s with
+    | O => inr (Success.value s)
+    | _ => inl (toError pos)
+    end
+  end.
+
+End CheckResult.