packages feed

Agda-2.3.2.2: src/prototyping/mixfix/Parser.hs

------------------------------------------------------------------------
-- A parser interface
------------------------------------------------------------------------

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
             Rank2Types #-}

module Parser where

import Control.Applicative

import IndexedOrd

class (Alternative p, Monad p) => Parser p tok | p -> tok where
  symbol :: p tok

  parse :: p r -> [ tok ] -> [ r ]

sat :: Parser p tok => (tok -> Bool) -> p tok
sat p = do
  c <- symbol
  if p c then return c else empty

sym :: Eq tok => Parser p tok => tok -> p tok
sym c = sat (== c)

sepBy :: Parser p tok => p r -> p sep -> p [r]
p `sepBy` sep = (:) <$> p <*> many (sep *> p)

chainr1 :: Parser p tok => p a -> p (a -> a -> a) -> p a
chainr1 p op = c
  where c = (\x f -> f x) <$> p <*>
            (pure id <|> flip <$> op <*> c)

chainl1 :: Parser p tok => p a -> p (a -> a -> a) -> p a
chainl1 p op = (\x f -> f x) <$> p <*> c
  where
  c =   pure (\x -> x)
    <|> (\f y g x -> g (f x y)) <$> op <*> p <*> c

chainr3 :: Parser p tok => p a -> p (a -> a -> a) -> p a
chainr3 p op = (\x f y -> f x y) <$> p <*> op <*> chainr1 p op

chainl3 :: Parser p tok => p a -> p (a -> a -> a) -> p a
chainl3 p op = (\x f y -> f x y) <$> chainl1 p op <*> op <*> p

-- | • `between` [x, y, z] ≈ x • y • z.

between :: Parser p tok => p a -> [p b] -> p [a]
p `between` []       = empty
p `between` [x]      = [] <$ x
p `between` (x : xs) = (:) <$> (x *> p) <*> (p `between` xs)

class Parser p tok => NTParser p nt tok | p -> tok nt where
  -- | Parser for the given non-terminal.
  nonTerm :: IndexedOrd nt => nt r -> p r

  parseWithGrammar :: Grammar p nt -> p r -> [ tok ] -> [ r ]

-- | A \"grammar\": a mapping from non-terminals to right-hand sides
-- (parsers).

type Grammar p nt = forall r. nt r -> p r