blob: ec1b6a5ac8966493266ef16a46951fb64023ec95 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
{-# OPTIONS --without-K --guardedness --safe #-}
open import Text.Parser.Types.Core using (Parameters)
module Data.SExp.Parser {l} {P : Parameters l} where
import Data.String.Base as String
open import Data.List as List using (List)
open import Data.Char.Base using (Char)
open import Data.List.Sized.Interface using (Sized)
open import Data.List.NonEmpty as List⁺ using (List⁺) renaming (map to map⁺)
open import Data.Subset using (Subset; into)
open import Effect.Monad using (RawMonadPlus)
open import Function.Base using (_∘_; _$_)
open import Induction.Nat.Strong using (fix; map; □_)
open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality)
open import Relation.Unary using (IUniversal; _⇒_)
open import Level.Bounded using (theSet; [_])
open import Text.Parser.Types P using (Parser)
open import Text.Parser.Combinators {P = P} using (_<$>_; list⁺; _<|>_; _<$_; _<&_; _<&?_; box)
open import Text.Parser.Combinators.Char {P = P} using (alpha; parens; withSpaces; spaces; char)
open import Text.Parser.Combinators.Numbers {P = P} using (decimalℕ)
open import Data.SExp using (SExp)
open SExp
open Parameters P using (M; Tok; Toks)
module _
{{𝕄 : RawMonadPlus M}}
{{𝕊 : Sized Tok Toks}}
{{𝔻 : DecidableEquality (theSet Tok)}}
{{ℂ : Subset Char (theSet Tok)}}
{{ℂ⁻ : Subset (theSet Tok) Char}}
where
-- An atom is just a non-empty list of alphabetical characters.
-- We use `<$>` to turn that back into a string and apply the `Atom` constructor.
atom : ∀[ Parser [ SExp ] ]
atom = Atom ∘ String.fromList⁺ ∘ map⁺ (into ℂ⁻) <$> list⁺ alpha
-- Natural number parser
nat : ∀[ Parser [ SExp ] ]
nat = Nat <$> decimalℕ
-- Empty list parser
nil : ∀[ Parser [ SExp ] ]
nil = SExps List.[] <$ char '(' <&? box spaces <& box (char ')')
-- Parser for a list of S-Expressions
list : ∀[ Parser [ SExp ] ⇒ Parser [ List SExp ] ]
list sexp = List⁺.toList <$> list⁺ (withSpaces sexp)
-- Compound S-Expression parser
compound : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
compound rec = nil <|> SExps <$> parens (map list rec)
-- S-Expression parser
sexp : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
sexp rec = atom <|> nat <|> compound rec
-- Build the parser as a fixpoint since SExp is an inductive type
sexp-top : ∀[ Parser [ SExp ] ]
sexp-top = fix (Parser [ SExp ]) sexp
-- Top-level parser for list of S-Expressions
LIST : ∀[ Parser [ SExp ] ]
LIST = SExps <$> list sexp-top
-- Top-level S-Expression parser
SEXP : ∀[ Parser [ SExp ] ]
SEXP = withSpaces sexp-top
|
