agda - Agda：用数字解析字符串

Answer 1

Answer 2

I had a go at it trying not to be clever and using simple recursive functions rather than stdlib magic. parse xs m ns parses xs by recording the (possibly empty) prefix already read in m while keeping the list of numbers already parsed in the accumulator ns.

If a parsing failure happens (non recognized character, two consecutive ,, etc.) everything is thrown away and we return nothing.

module parseList where

open import Data.Nat
open import Data.List
open import Data.Maybe
open import Data.Char
open import Data.String

isDigit : Char → Maybe ℕ
isDigit '0' = just 0
isDigit '1' = just 1
isDigit '2' = just 2
isDigit '3' = just 3
isDigit _   = nothing

attach : Maybe ℕ → ℕ → ℕ
attach nothing  n = n
attach (just m) n = 10 * m + n

Quote : List Char → Maybe (List ℕ)
Quote xs = parse xs nothing []
  where
    parse : List Char → Maybe ℕ → List ℕ → Maybe (List ℕ)
    parse []         nothing  ns = just ns
    parse []         (just n) ns = just (n ∷ ns)
    parse (',' ∷ tl) (just n) ns = parse tl nothing (n ∷ ns)
    parse (hd ∷ tl)  m        ns with isDigit hd
    ... | nothing = nothing
    ... | just n  = parse tl (just (attach m n)) ns

stringListToℕ : String → Maybe (List ℕ)
stringListToℕ xs with Quote (toList xs)
... | nothing = nothing
... | just ns = just (reverse ns)

open import Relation.Binary.PropositionalEquality

test : stringListToℕ ("12,3") ≡ just (12 ∷ 3 ∷ [])
test = refl

Answer 3

Here is the Code from Vitus as a running example that uses the Agda Prelude

module Parse where

open import Prelude

-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude

-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory 



open import Data.Product using (uncurry′)
open import Data.Maybe using ()
open import Data.List using (sequence)

splitBy : ∀ {a} {A : Set a} → (A → Bool) → List A → List (List A)
splitBy {A = A} p = uncurry′ _∷_ ∘ foldr step ([] , [])
  where
    step : A → List A × List (List A) → List A × List (List A)
    step x (cur , acc) with p x
    ... | true  = x ∷ cur , acc
    ... | false = []      , cur ∷ acc


charsToℕ : List Char → Maybe ℕ
charsToℕ []   = nothing
charsToℕ list = stringToℕ (fromList list)

notComma : Char → Bool
notComma c = not (c == ',')

-- Finally:

charListToℕ : List Char → Maybe (List ℕ)
charListToℕ = Data.List.sequence Data.Maybe.monad ∘ map charsToℕ ∘ splitBy     notComma

stringListToℕ : String → Maybe (List ℕ)
stringListToℕ = charListToℕ ∘ toList


-- Test

test1 : charListToℕ ('1' ∷ '2' ∷ ',' ∷ '3' ∷ []) ≡ just (12 ∷ 3 ∷ [])
test1 = refl

test2 : stringListToℕ "12,33" ≡ just (12 ∷ 33 ∷ [])
test2 = refl

test3 : stringListToℕ ",,," ≡ nothing
test3 = refl

test4 : stringListToℕ "abc,def" ≡ nothing
test4 = refl