Support for Agda 2.6.2 & stdlib 2.0 (#32)

Co-authored-by: Pavel Turyansky <pavel.turyansky@kaspersky.com>

.gitignore

@@ -1,3 +1,4 @@
+Everything.agda
 *.agdai
 *~
 *.pdf

Makefile

@@ -0,0 +1,17 @@
+.PHONY: test Everything.agda clean
+
+OTHEROPTS = --auto-inline -Werror
+
+RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
+
+test: Everything.agda
+	agda ${RTSARGS} -i. Everything.agda
+
+html: Everything.agda
+	agda ${RTSARGS} --html -i. Everything.agda
+
+Everything.agda:
+	git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
+
+clean:
+	find . -name '*.agdai' -exec rm \{\} \;

agdarsec.agda-lib

@@ -1,3 +1,4 @@
 name: agdarsec
 include: src
-depend: standard-library
+depend: standard-library-2.0
+flags: --guardedness

src/Data/Text.agda

@@ -1,7 +1,7 @@
 module Data.Text where
 
 open import Data.Char.Base
-open import Data.String.Base
+open import Data.String.Base hiding (uncons)
 open import Data.Maybe.Base
 open import Data.List.Base hiding (uncons)
 open import Data.Pair
@@ -12,7 +12,6 @@ postulate uncons : String → Maybe (Pair Char String)
 {-# FOREIGN GHC import qualified Data.Text #-}
 {-# COMPILE GHC uncons = Data.Text.uncons #-}
 
-
 postulate
   uncons-list : (s : String) →
                 toList s ≡ maybe (λ p → fst p ∷ toList (snd p)) [] (uncons s)

src/Text/Parser.agda

@@ -14,9 +14,10 @@ module Text.Parser where
 
 open import Level using (0ℓ)
 open import Level.Bounded as Level≤ using ([_])
-open import Category.Monad using (RawMonad; RawMonadZero; RawMonadPlus)
+open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus)
+open import Effect.Monad.State.Transformer.Base using (runStateT)
 open import Function.Base using (const; _∘′_; case_of_)
-open import Function.Identity.Categorical as Identity
+open import Function.Identity.Effectful as Identity
 open import Data.Bool.Base using (Bool; T; not; if_then_else_)
 open import Data.Char.Base using (Char)
 open import Data.Empty using (⊥)
@@ -81,8 +82,8 @@ runParser : ∀[ Parser A ] → String → Position ⊎ A
 runParser p str =
   let init  = Level≤.lift (start , [])
       input = Level≤.lift (mkText str refl)
-  in case Result.toSum (Types.Parser.runParser p (ℕₚ.n≤1+n _) input init) of λ where
-        (inj₂ (res , p)) → if Success.size res ≡ᵇ 0
+  in case Result.toSum (runStateT (Types.Parser.runParser p (ℕₚ.n≤1+n _) input) init) of λ where
+        (inj₂ (p , res)) → if Success.size res ≡ᵇ 0
                            then inj₂ (Level≤.lower (Success.value res))
                            else inj₁ (proj₁ (Level≤.lower p))
         (inj₁ p) → inj₁ (Level≤.lower p)

src/Text/Parser/Combinators.agda

@@ -25,7 +25,7 @@ open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable using (⌊_⌋)
 open import Relation.Binary.PropositionalEquality.Decidable.Core using (DecidableEquality; decide)
 
-open import Category.Monad using (RawMonadPlus)
+open import Effect.Monad using (RawMonadPlus)
 open import Data.List.Sized.Interface using (Sized)
 
 open import Function.Base using (const; _$_; _∘_; _∘′_; flip; case_of_)
@@ -50,7 +50,7 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
 
   guardM : theSet (A ⟶ Maybe B) → ∀[ Parser A ⇒ Parser B ]
   runParser (guardM p A) m≤n s =
-    runParser A m≤n s 𝕄.>>= maybe 𝕄.return 𝕄.∅ ∘′ S.guardM p
+    runParser A m≤n s 𝕄.>>= maybe 𝕄.pure 𝕄.∅ ∘′ S.guardM p
 
  module _ {A : Set≤ l} where
 
@@ -98,16 +98,16 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
     runParser A m≤n s 𝕄.>>= λ rA →
     let (a ^ p<m , s′) = rA in
     (runParser (Box.call (B (lower a)) (≤-trans p<m m≤n)) ≤-refl s′ 𝕄.>>= λ rB →
-    𝕄.return (S.and rA (S.map just rB)))
-    𝕄.∣ 𝕄.return ((lift (lower a , nothing)) ^ p<m , s′)
+    𝕄.pure (S.and rA (S.map just rB)))
+    𝕄.∣ 𝕄.pure ((lift (lower a , nothing)) ^ p<m , s′)
 
   _&>>=_ : ∀ {n} → Parser A n → ((a : theSet A) → (□ Parser (mkSet≤ (B a))) n) →
            Parser (Σ A B) n
   runParser (A &>>= B) m≤n s =
     runParser A m≤n s 𝕄.>>= λ rA →
     let (a ^ p<m , s′) = rA in
     (runParser (Box.call (B (lower a)) (≤-trans p<m m≤n)) ≤-refl s′ 𝕄.>>= λ rB →
-     𝕄.return (S.and rA rB))
+     𝕄.pure (S.and rA rB))
 
  module _ {A B : Set≤ l} where
 
@@ -139,15 +139,15 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
     runParser A m≤n s 𝕄.>>= λ rA →
     let (a ^ p<m , s′) = rA in
     (runParser (Box.call (B (lower a)) (≤-trans p<m m≤n)) ≤-refl s′ 𝕄.>>= λ rB →
-     𝕄.return (S.and′ rA (S.map just rB)))
-    𝕄.∣ 𝕄.return (lift (lower a , nothing) ^ p<m , s′)
+     𝕄.pure (S.and′ rA (S.map just rB)))
+    𝕄.∣ 𝕄.pure (lift (lower a , nothing) ^ p<m , s′)
 
   _&>>=′_ : ∀[ Parser A ⇒ (const (theSet A) ⇒ □ Parser B) ⇒ Parser (A × B) ]
   runParser (A &>>=′ B) m≤n s =
     runParser A m≤n s 𝕄.>>= λ rA →
     let (a ^ p<m , s′) = rA in
     (runParser (Box.call (B (lower a)) (≤-trans p<m m≤n)) ≤-refl s′ 𝕄.>>= λ rB →
-     𝕄.return (S.and′ rA rB))
+     𝕄.pure (S.and′ rA rB))
 
  module _ {A B : Set≤ l} where
 
@@ -189,7 +189,7 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
   _<&M>_ : ∀[ Parser A ⇒ const (M (Lift B)) ⇒ Parser (A × B) ]
   runParser (A <&M> B) m≤n s =
     runParser A m≤n s 𝕄.>>= λ rA → B 𝕄.>>= λ b →
-    𝕄.return (S.map (_, lower b) rA)
+    𝕄.pure (S.map (_, lower b) rA)
 
   _<&M_ : ∀[ Parser A ⇒ const (M (Lift B)) ⇒ Parser A ]
   A <&M B = proj₁ <$> (A <&M> B)
@@ -218,7 +218,7 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
   runParser (<[ f , k ]> A⊎B) m≤n s =
     runParser A⊎B m≤n s 𝕄.>>= λ rA⊎B → let (v ^ p<m , s′) = rA⊎B in
     case lower v of λ where
-      (inj₁ a) → 𝕄.return (lift (f a) ^ p<m , s′)
+      (inj₁ a) → 𝕄.pure (lift (f a) ^ p<m , s′)
       (inj₂ b) → <-lift p<m 𝕄.<$> runParser (Box.call (k b) (≤-trans p<m m≤n)) ≤-refl s′
 
  module _ {A B : Set≤ l} where
@@ -274,14 +274,14 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
  module _ {A : Set≤ l} where
 
   schainl : ∀[ Success Toks A ⇒ □ Parser (A ⟶ A) ⇒ M ∘′ Success Toks A ]
-  schainl = Box.fix goal $ λ rec sA op → rest rec sA op 𝕄.∣ 𝕄.return sA where
+  schainl = Box.fix goal $ λ rec sA op → rest rec sA op 𝕄.∣ 𝕄.pure sA where
 
     goal = Success Toks A ⇒ □ Parser (A ⟶ A) ⇒ M ∘′ Success Toks A
 
     rest : ∀[ □ goal ⇒ goal ]
     rest rec (a ^ p<m , s) op = runParser (Box.call op p<m) ≤-refl s 𝕄.>>= λ sOp →
           Box.call rec p<m (S.map (_$ lower a) sOp) (Box.<-lower p<m op) 𝕄.>>=
-          𝕄.return ∘′ <-lift p<m
+          𝕄.pure ∘′ <-lift p<m
 
   iterate : ∀[ Parser A ⇒ □ Parser (A ⟶ A) ⇒ Parser A ]
   runParser (iterate {n} a op) m≤n s =
@@ -302,7 +302,7 @@ module _ {{𝕊 : Sized Tok Toks}} {{𝕄 : RawMonadPlus M}}
   chainr1 = Box.fix goal $ λ rec A op → mkParser λ m≤n s →
             runParser A m≤n s 𝕄.>>= λ sA →
             rest (Box.≤-lower m≤n rec) (≤-lower m≤n A) (Box.≤-lower m≤n op) sA
-            𝕄.∣  𝕄.return sA where
+            𝕄.∣  𝕄.pure sA where
 
     goal = Parser A ⇒ □ Parser (A ⟶ A ⟶ A) ⇒ Parser A
 

src/Text/Parser/Combinators/Char.agda

@@ -16,7 +16,7 @@ open import Data.Product using (_,_)
 open import Data.String.Base as String using (String)
 open import Data.Vec.Base as Vec using (toList)
 
-open import Category.Monad using (RawMonadPlus)
+open import Effect.Monad using (RawMonadPlus)
 open import Function.Base using (_∘′_; _$′_; _$_)
 
 open import Relation.Nullary using (does)

src/Text/Parser/Combinators/Numbers.agda

@@ -18,7 +18,7 @@ open import Data.Sign.Base using (Sign)
 open import Data.Sum.Base using ([_,_]′)
 
 open import Function.Base using (const; id; _$_; _∘′_; case_of_)
-open import Category.Monad using (RawMonadPlus)
+open import Effect.Monad using (RawMonadPlus)
 
 open import Relation.Unary
 open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality)

src/Text/Parser/JSON.agda

@@ -6,7 +6,7 @@ open import Text.Parser.Types.Core using (Parameters)
 
 module Text.Parser.JSON {l} {P : Parameters l} where
 
-open import Category.Monad using (RawMonadPlus)
+open import Effect.Monad using (RawMonadPlus)
 
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base using (Char)

src/Text/Parser/Monad.agda

@@ -13,12 +13,15 @@ open import Data.Text.Sized using (Text)
 open import Data.Subset using (Subset; into)
 open import Function.Base using (_∘′_; _$′_)
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+open import Effect.Empty
+open import Effect.Choice
 
-open import Function.Identity.Categorical as Id using (Identity)
-open import Category.Monad.State
+open import Function.Identity.Effectful as Id using (Identity)
+open import Effect.Monad.State.Transformer as StateT
+  using (StateT; mkStateT; runStateT; RawMonadState)
 
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
 
@@ -53,41 +56,50 @@ module AgdarsecT
   private module 𝕄 = RawMonad 𝕄
 
   monadT : RawMonad (AgdarsecT E Ann M)
-  monadT = StateTMonad _ (Result-monadT E 𝕄)
+  monadT = StateT.monad (Result-monadT E 𝕄)
 
   applicative : RawApplicative (AgdarsecT E Ann M)
-  applicative = RawMonad.rawIApplicative monadT
+  applicative = RawMonad.rawApplicative monadT
+
+  empty : RawEmpty (AgdarsecT E Ann M)
+  empty = record
+    { empty = mkStateT (𝕄.pure ∘′ SoftFail ∘′ Level≤.map (into 𝕊))
+    }
 
   applicativeZero : RawApplicativeZero (AgdarsecT E Ann M)
   applicativeZero = record
-    { applicative = applicative
-    ; ∅           = 𝕄.pure ∘′ SoftFail ∘′ Level≤.map (into 𝕊)
+    { rawApplicative = applicative
+    ; rawEmpty = empty
     }
 
   monadZero : RawMonadZero (AgdarsecT E Ann M)
   monadZero = record
-    { monad           = monadT
-    ; applicativeZero = applicativeZero
+    { rawMonad = monadT
+    ; rawEmpty = empty
     }
 
+  choice : RawChoice (AgdarsecT E Ann M)
+  choice = StateT.choice (ResultT-choice E 𝕄)
+
   alternative : RawAlternative (AgdarsecT E Ann M)
   alternative = record
-    { applicativeZero = applicativeZero
-    ; _∣_             = λ ma₁ ma₂ s → ma₁ s 𝕄.>>= λ where
-        (SoftFail _) → ma₂ s
-        r            → 𝕄.pure r
+    { rawApplicativeZero = applicativeZero
+    ; rawChoice = choice
     }
 
   monadPlus : RawMonadPlus (AgdarsecT E Ann M)
   monadPlus = record
-    { monad       = monadT
-    ; alternative = alternative
+    { rawMonadZero = monadZero
+    ; rawChoice = choice
     }
 
   monadState : RawMonadState (Lift ([ Position ] × List Ann)) (AgdarsecT E Ann M)
-  monadState = StateTMonadState _ (Result-monadT E 𝕄)
+  monadState = StateT.monadState (Result-monadT E 𝕄)
 
-  private module ST = RawMonadState monadState
+  private
+    module ST where
+      open RawMonad monadT public
+      open RawMonadState monadState public
 
   getPosition : AgdarsecT E Ann M (Lift [ Position ])
   getPosition = Level≤.map proj₁ ST.<$> ST.get
@@ -97,18 +109,18 @@ module AgdarsecT
 
   withAnnotation : ∀ {A} → theSet Ann → AgdarsecT E Ann M A → AgdarsecT E Ann M A
   withAnnotation c ma = let open ST in do
-    ST.modify (Level≤.map $′ map₂ (c ∷_))
+    modify (Level≤.map $′ map₂ (c ∷_))
     a ← ma
-    ST.modify (Level≤.map $′ map₂ (drop 1))
-    ST.pure a
+    modify (Level≤.map $′ map₂ (drop 1))
+    pure a
 
   recordChar : Char → AgdarsecT E Ann M (Lift ⊤)
   recordChar c = _ ST.<$ ST.modify (Level≤.map $′ map₁ (update c))
 
   -- Commiting to a branch makes all the failures in that branch hard failures
   -- that we cannot recover from
   commit : ∀ {A} → AgdarsecT E Ann M A → AgdarsecT E Ann M A
-  commit m s = result HardFail HardFail Value 𝕄.<$> m s
+  commit m = mkStateT λ s → result HardFail HardFail Value 𝕄.<$> runStateT m s
 
   param : ∀ Tok Toks recTok → Parameters l
   param Tok Toks recTok = record

src/Text/Parser/Monad/Result.agda

@@ -2,11 +2,13 @@ module Text.Parser.Monad.Result where
 
 open import Level using (Level)
 open import Level.Bounded using (Set≤; Lift)
-open import Category.Monad using (RawMonad)
+open import Effect.Monad using (RawMonad; mkRawMonad)
+open import Effect.Empty
+open import Effect.Choice
 open import Data.Maybe.Base using (Maybe; maybe′)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘′_)
-import Function.Identity.Categorical as Id
+import Function.Identity.Effectful as Id
 
 private
   variable
@@ -43,10 +45,20 @@ ResultT : Set≤ l →          -- Error
 ResultT E M A = M (Result (Lift E) A)
 
 Result-monadT : ∀ (E : Set≤ l) {M} → RawMonad M → RawMonad (ResultT E M)
-Result-monadT E M = record
-  { return = M.pure ∘′ Value
-  ; _>>=_  = λ m f → m M.>>= result (M.pure ∘′ SoftFail) (M.pure ∘′ HardFail) f
-  } where module M = RawMonad M
+Result-monadT E {M} monad-M = mkRawMonad (ResultT E M) pure _>>=_
+  where
+    module M = RawMonad monad-M
+    pure : ∀ {A} → A → ResultT E M A
+    pure = M.pure ∘′ Value
+    _>>=_ : ∀ {A B} → ResultT E M A → (A → ResultT E M B) → ResultT E M B
+    _>>=_ = λ m f → m M.>>= result (M.pure ∘′ SoftFail) (M.pure ∘′ HardFail) f
 
 Result-monad : (E : Set≤ l) → RawMonad (Result (Lift E))
 Result-monad E = Result-monadT E Id.monad
+
+ResultT-choice : ∀ (E : Set≤ l) {M} → RawMonad M → RawChoice {ℓ = l} (ResultT E M)
+ResultT-choice E M = record
+  { _<|>_ = λ m₁ m₂ → m₁ >>= λ where
+      (SoftFail _) → m₂
+      r → pure r
+  } where open RawMonad M

src/Text/Parser/Polymorphic.agda

@@ -2,8 +2,8 @@ open import Level using (Level)
 
 module Text.Parser.Polymorphic (l : Level) where
 
-open import Function.Identity.Categorical using (Identity)
-open import Category.Monad
+open import Function.Identity.Effectful using (Identity)
+open import Effect.Monad
 open import Data.Char.Base using (Char)
 open import Data.Product using (proj₁)
 open import Level.Bounded as Level≤ using (Set≤; theSet; [_]; lift; lower)