Finish updating to stdlib 2.0

.github/workflows/ci-ubuntu.yml

@@ -45,8 +45,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_COMMIT: tags/v2.6.2
-  STDLIB_VERSION: 1.7
+  AGDA_COMMIT: tags/v2.6.4.3
+  STDLIB_VERSION: '2.0'
 
   GHC_VERSION: 8.6.5
   CABAL_VERSION: 3.2.0.0
@@ -83,7 +83,7 @@ jobs:
       # i.e. if we change either the version of Agda, ghc, or cabal that we want
       # to use for the build.
       - name: Cache cabal packages
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         id: cache-cabal
         with:
           path: |
@@ -134,7 +134,7 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout agdarsec
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       # Generate a fresh Everything.agda & index.agda and start building!
       - name: Test agdarsec

Makefile

@@ -1,12 +1,13 @@
 AGDA_EXEC?=agda
 .PHONY: test Everything.agda clean
 
-OTHEROPTS = --auto-inline -Werror
+OTHEROPTS = -Werror
 
 RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
 
 test: Everything.agda
 	${AGDA_EXEC} ${RTSARGS} -i. Everything.agda
+	${AGDA_EXEC} ${RTSARGS} -i. -i src/ -iexamples index.agda
 
 html: Everything.agda
 	${AGDA_EXEC} ${RTSARGS} --html -i. Everything.agda

README.md

@@ -7,12 +7,10 @@ The motivation and design decisions behind agdarsec are detailed in:
 
 ## Compilation
 
-[![Travis Status](https://api.travis-ci.org/gallais/agdarsec.svg?branch=master)](https://travis-ci.org/gallais/agdarsec)
-
 To typecheck and compile this project you will need:
 
-* Agda version 2.6.2
-* Agda's standard library (version 1.7)
+* Agda version 2.6.4.3
+* Agda's standard library (version 2.0)
 
 ## Ports
 

examples/Base.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 open import Level using (Level)
 
 module Base (l : Level) where
@@ -8,21 +10,21 @@ import Data.Nat as Nat
 open import Data.Nat.Properties
 open import Data.Char.Base as Char using (Char)
 import Data.Empty as Empty
-open import Data.Product as Product using (_,_; proj₁)
+open import Data.Product as Product using (_,_; proj₂)
 
 open import Data.List.Base as List using ([]; _∷_)
-open import Data.List.Categorical as List
+open import Data.List.Effectful as List
 open import Data.List.Sized.Interface
 
 open import Data.String as String
 open import Data.Vec as Vec using ()
 open import Data.Bool
 open import Data.Maybe as Maybe using (nothing; just; maybe′)
-open import Data.Maybe.Categorical as MaybeCat
+open import Data.Maybe.Effectful as MaybeCat
 open import Data.Sum
 open import Function
-open import Category.Monad
-open import Category.Monad.State
+open import Effect.Monad
+open import Effect.Monad.State.Transformer as StateT using (StateT)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
@@ -81,9 +83,10 @@ instance
 
   runStateT : ∀ {M A} {{𝕄 : RawMonadRun M}} → RawMonadRun (StateT (Lift ([ Position ] × List A)) M)
   runStateT {{𝕄}} .RawMonadRun.runM =
-    List.map proj₁
+    List.map proj₂
     ∘′ runM 𝕄
     ∘′ (_$ lift (start , []))
+    ∘′ StateT.runStateT
 
   monadMaybe : RawMonad {l} Maybe.Maybe
   monadMaybe = MaybeCat.monad

examples/Expr.agda

@@ -1,6 +1,8 @@
 -- Example taken from parsec's documentation
 -- https://hackage.haskell.org/package/parsec-3.1.11/docs/Text-Parsec-Combinator.html#v:chainl1
 
+{-# OPTIONS --guardedness #-}
+
 module Expr where
 
 

examples/Identifier.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Identifier where
 
 import Level

examples/Large.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Large where
 
 import Level

examples/Matrix.agda

@@ -1,8 +1,10 @@
+{-# OPTIONS --guardedness #-}
+
 module Matrix where
 
 open import Data.Maybe.Base as Maybe
-open import Data.Nat.Base
-open import Data.Product as Product
+open import Data.Nat.Base hiding (_!)
+open import Data.Product.Base as Product
 open import Data.Sum.Base
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Function.Base
@@ -26,7 +28,7 @@ indices = f <$> (decimalℕ <& box space <&> box decimalℕ) where
   f (suc m , suc n) = inj₂ (suc m , suc n , _)
 
 matrix : ∀[ Parser (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Matrix ℕ m n) ]
-matrix = <[ ((λ (m , n , p) → [ (λ _ → 0 , n , []) , (λ _ → m , 0 , Vec.replicate []) ] p))
+matrix = <[ ((λ (m , n , p) → [ (λ _ → 0 , n , []) , (λ _ → m , 0 , Vec.replicate _ []) ] p))
           , (λ (m , n , p , q) → box $ (m ,_) ∘ (n ,_) <$> replicate m {{p}} (replicate n {{q}} (space &> box decimalℕ)))
           ]> indices
 

examples/NList.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 -- Challenge taken from stackoverflow:
 -- http://stackoverflow.com/questions/12380239/agda-parsing-nested-lists
 

examples/Parentheses.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Parentheses where
 
 import Level

examples/RegExp.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module RegExp where
 
 import Level

examples/SExp.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module SExp where
 
 open import Level using (0ℓ)
@@ -9,7 +11,7 @@ data SExp : Set where
   Atom : String → SExp
   Pair : SExp → SExp → SExp
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.List.Sized.Interface
 open import Data.List.NonEmpty as List⁺ using (List⁺)
 open import Data.Maybe

examples/STLC.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module STLC where
 
 open import Level.Bounded using ([_])
@@ -15,6 +17,7 @@ open import Data.Vec.Base as Vec using (Vec)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.List.Sized.Interface
 open import Data.Product using (_×_; _,_; uncurry; ∃; proj₁)
+import Effect.Monad.State.Transformer as StateT
 open import Function.Base
 
 open import Relation.Nullary
@@ -115,7 +118,9 @@ instance
   _ = ParserM.monadPlus
   _ = ParserM.monad
 
-P = ParserM.param [ Token ] (λ n → [ Vec Token n ]) λ where (p , _) _ → Value (_ , lift (p , []))
+P = ParserM.param [ Token ] (λ n → [ Vec Token n ]) λ
+  where (p , _) .StateT.runStateT _ → Value (lift (p , []) , _)
+
 
 theTok : Tok → ∀[ Parser P [ Token ] ]
 theTok t = maybeTok $ λ where

examples/Vec.agda

@@ -1,11 +1,13 @@
+{-# OPTIONS --guardedness #-}
+
 module Vec where
 
 open import Text.Parser
 open import Data.Unit.Base
 open import Data.Vec hiding (replicate)
-open import Data.Maybe
-open import Data.Nat
-open import Data.Product
+open import Data.Maybe.Base
+open import Data.Nat.Base hiding (_!)
+open import Data.Product.Base
 
 n-times : {A : Set} → ∀[ Parser A ⇒ Parser (∃[ n ] Vec A (suc n)) ]
 n-times p = decimalℕ &>>= λ n → box (replicate (suc n) p)

index.agda

@@ -5,6 +5,10 @@ module index where
 -- The core design decisions behind agdarsec are detailed in
 -- https://gallais.github.io/pdf/agdarsec18.pdf
 
+-- The most general version of the library is in
+
+import Text.Parser.Polymorphic
+
 -- We have a simplified frontend with ready made default choices:
 
 import Text.Parser

src/Text/Parser/Polymorphic.agda

@@ -59,6 +59,7 @@ open import Data.Nat.Base using (_≡ᵇ_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_,_)
 open import Data.String as String using (String)
+open import Effect.Monad.State.Transformer using (runStateT)
 open import Function.Base using (case_of_)
 
 import Text.Parser.Monad.Result as Result
@@ -68,8 +69,8 @@ runParser : {A : Set≤ l} → ∀[ Parser A ] → String → Position ⊎ theSe
 runParser p str =
   let init  = lift (start , [])
       input = lift (String.toVec str)
-  in case Result.toSum (Parser.runParser p (ℕₚ.n≤1+n _) input init) of λ where
-        (inj₂ (res , p)) → let open Success in
+  in case Result.toSum (runStateT (Parser.runParser p (ℕₚ.n≤1+n _) input) init) of λ where
+        (inj₂ (p , res)) → let open Success in
                            if size res ≡ᵇ 0
                            then inj₂ (lower (value res))
                            else inj₁ (proj₁ (lower p))