agda - Agda: 数字で文字列をパースする

Answer 1

Answer 2

私は賢くならず、標準ライブラリの魔法ではなく単純な再帰関数を使用しようと試みました。parse xs m nsaccumulator で既に解析された数値のリストを保持しながら、xs既に読み込まれた (おそらく空の) プレフィックスを記録することによって解析します。mns

解析エラーが発生した場合 (文字が認識されない、 が 2 つ連続,するなど)、すべてが破棄され、 が返され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

Agda Prelude を使用する実行例としての Vitus のコードを次に示します。

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