Agda-2.3.2.2: src/prototyping/mixfix/benchmarks/SlowParser.hs
------------------------------------------------------------------------
-- An elegant but very slow variant of AmbTrie
------------------------------------------------------------------------
-- I think that the code below would be accepted directly by Coq's
-- termination and productivity checkers (if written in Coq style,
-- with Parser declared as being coinductive).
-- Note that this parser does not do any on-the-fly left
-- factorisation.
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module SlowParser where
import Control.Monad
import qualified Parser
import Control.Applicative
infix 4 :&:
data Parser k r' tok r = [ r ] :&: (tok -> Parser k r' tok r)
-- Note that empty and (<|>) are productive. (If we assume a total language.)
instance Alternative (Parser k r' tok) where
empty = [] :&: const empty
xs1 :&: f1 <|> xs2 :&: f2 = xs1 ++ xs2 :&: (\c -> f1 c <|> f2 c)
-- Note that bind is productive.
instance Monad (Parser k r' tok) where
return x = [x] :&: const empty
xs :&: f >>= g = foldr (<|>) ([] :&: (\c -> f c >>= g)) (map g xs)
instance Applicative (Parser k r' tok) where
pure = return
p1 <*> p2 = p1 >>= \f -> p2 >>= \x -> return (f x)
instance Functor (Parser k r' tok) where
fmap = liftM
-- Note that parse is structurally recursive.
parse :: Parser k r' tok r -> [ tok ] -> [ r ]
parse (xs :&: f) [] = xs
parse (xs :&: f) (c : s) = parse (f c) s
instance Parser.Parser (Parser k r' tok) k r' tok where
sym c = [] :&: \c' -> if c == c' then return c' else empty