{-# LANGUAGE CPP #-}
module Agda.Utils.Parser.MemoisedCPS
( ParserClass(..)
, sat, token, tok, doc
, DocP, bindP, choiceP, seqP, starP, atomP
, Parser
, ParserWithGrammar
) where
import Control.Applicative ( Alternative((<|>), empty, many, some) )
import Control.Monad (ap, liftM2)
import Control.Monad.State.Strict (State, evalState, runState, get, put, modify')
import Data.Array
import Data.Hashable
import qualified Data.HashMap.Strict as Map
import Data.HashMap.Strict (HashMap)
import qualified Data.HashSet as Set
import Data.HashSet (HashSet)
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap.Strict (IntMap)
import qualified Data.List as List
import Data.Maybe
import Text.PrettyPrint.HughesPJ hiding (empty)
import qualified Text.PrettyPrint.HughesPJ as PP
import Agda.Utils.Pretty ( mparens )
#include "undefined.h"
import Agda.Utils.Impossible
type Pos = Int
type M k r tok b = State (IntMap (HashMap k (Value k r tok b)))
type Cont k r tok b a = Pos -> a -> M k r tok b [b]
data Value k r tok b = Value
{ results :: !(IntMap [r])
, continuations :: [Cont k r tok b r]
}
newtype Parser k r tok a =
P { unP :: forall b.
Array Pos tok ->
Pos ->
Cont k r tok b a ->
M k r tok b [b]
}
instance Monad (Parser k r tok) where
return = pure
P p >>= f = P $ \input i k ->
p input i $ \j x -> unP (f x) input j k
instance Functor (Parser k r tok) where
fmap f (P p) = P $ \input i k ->
p input i $ \i -> k i . f
instance Applicative (Parser k r tok) where
pure x = P $ \_ i k -> k i x
P p1 <*> P p2 = P $ \input i k ->
p1 input i $ \i f ->
p2 input i $ \i x ->
k i (f x)
instance Alternative (Parser k r tok) where
empty = P $ \_ _ _ -> return []
P p1 <|> P p2 = P $ \input i k ->
liftM2 (++) (p1 input i k) (p2 input i k)
class (Functor p, Applicative p, Alternative p, Monad p) =>
ParserClass p k r tok | p -> k, p -> r, p -> tok where
parse :: p a -> [tok] -> [a]
grammar :: Show k => p a -> Doc
sat' :: (tok -> Maybe a) -> p a
annotate :: (DocP -> DocP) -> p a -> p a
memoise :: (Eq k, Hashable k, Show k) => k -> p r -> p r
memoiseIfPrinting :: (Eq k, Hashable k, Show k) => k -> p r -> p r
doc :: ParserClass p k r tok => Doc -> p a -> p a
doc d = annotate (\_ -> (d, atomP))
sat :: ParserClass p k r tok => (tok -> Bool) -> p tok
sat p = sat' (\t -> if p t then Just t else Nothing)
token :: ParserClass p k r tok => p tok
token = doc (text "·") (sat' Just)
tok :: (ParserClass p k r tok, Eq tok, Show tok) => tok -> p tok
tok t = doc (text (show t)) (sat (t ==))
instance ParserClass (Parser k r tok) k r tok where
parse p toks =
flip evalState IntMap.empty $
unP p (listArray (0, n - 1) toks) 0 $ \j x ->
if j == n then return [x] else return []
where n = List.genericLength toks
grammar _ = PP.empty
sat' p = P $ \input i k ->
if inRange (bounds input) i then
case p (input ! i) of
Nothing -> return []
Just x -> (k $! (i + 1)) $! x
else
return []
annotate _ p = p
memoiseIfPrinting _ p = p
memoise key p = P $ \input i k -> do
let alter j zero f m =
IntMap.alter (Just . f . fromMaybe zero) j m
lookupTable = fmap (\m -> Map.lookup key =<<
IntMap.lookup i m) get
insertTable v = modify' $ alter i Map.empty (Map.insert key v)
v <- lookupTable
case v of
Nothing -> do
insertTable (Value IntMap.empty [k])
unP p input i $ \j r -> do
Just (Value rs ks) <- lookupTable
insertTable (Value (alter j [] (r :) rs) ks)
concat <$> mapM (\k -> k j r) ks
Just (Value rs ks) -> do
insertTable (Value rs (k : ks))
concat . concat <$>
mapM (\(i, rs) -> mapM (k i) rs) (IntMap.toList rs)
data ParserWithGrammar k r tok a =
PG (Bool -> Either (Parser k r tok a) (Docs k))
type DocP = (Doc, Int)
bindP :: Int
bindP = 10
choiceP :: Int
choiceP = 20
seqP :: Int
seqP = 30
starP :: Int
starP = 40
atomP :: Int
atomP = 50
type Docs k = State (HashMap k (Maybe DocP)) DocP
pg :: Parser k r tok a -> Docs k -> ParserWithGrammar k r tok a
pg p d = PG $ \b -> if b then Left p else Right d
parser :: ParserWithGrammar k r tok a -> Parser k r tok a
parser (PG p) = either id __IMPOSSIBLE__ (p True)
docs :: ParserWithGrammar k r tok a -> Docs k
docs (PG p) = either __IMPOSSIBLE__ id (p False)
instance Monad (ParserWithGrammar k r tok) where
return = pure
p >>= f =
pg (parser p >>= parser . f)
((\(d, p) -> (mparens (p < bindP) d <+> text ">>= ?", bindP))
<$> docs p)
instance Functor (ParserWithGrammar k r tok) where
fmap f p = pg (fmap f (parser p)) (docs p)
instance Applicative (ParserWithGrammar k r tok) where
pure x = pg (pure x) (return (text "ε", atomP))
p1 <*> p2 =
pg (parser p1 <*> parser p2)
(liftM2 (\(d1, p1) (d2, p2) ->
(sep [ mparens (p1 < seqP) d1
, mparens (p2 < seqP) d2
], seqP))
(docs p1) (docs p2))
starDocs :: String -> ParserWithGrammar k r tok a -> Docs k
starDocs s p =
(\(d, p) -> (mparens (p < starP) d <+> text s, starP)) <$> docs p
instance Alternative (ParserWithGrammar k r tok) where
empty = pg empty (return (text "∅", atomP))
p1 <|> p2 =
pg (parser p1 <|> parser p2)
(liftM2 (\(d1, p1) (d2, p2) ->
(sep [ mparens (p1 < choiceP) d1
, text "|"
, mparens (p2 < choiceP) d2
], choiceP))
(docs p1) (docs p2))
many p = pg (many (parser p)) (starDocs "⋆" p)
some p = pg (some (parser p)) (starDocs "+" p)
prettyKey :: Show k => k -> DocP
prettyKey key = (text ("<" ++ show key ++ ">"), atomP)
memoiseDocs ::
(Eq k, Hashable k, Show k) =>
k -> ParserWithGrammar k r tok r -> Docs k
memoiseDocs key p = do
r <- Map.lookup key <$> get
case r of
Just _ -> return ()
Nothing -> do
modify' (Map.insert key Nothing)
d <- docs p
modify' (Map.insert key (Just d))
return (prettyKey key)
instance ParserClass (ParserWithGrammar k r tok) k r tok where
parse p = parse (parser p)
sat' p = pg (sat' p) (return (text "<sat ?>", atomP))
annotate f p = pg (parser p) (f <$> docs p)
memoise key p = pg (memoise key (parser p))
(memoiseDocs key p)
memoiseIfPrinting key p = pg (parser p) (memoiseDocs key p)
grammar p =
d
$+$
nest 2 (foldr1 ($+$) $
text "where" :
map (\(k, d) -> fst (prettyKey k) <+> text "∷=" <+>
maybe __IMPOSSIBLE__ fst d)
(Map.toList ds))
where
((d, _), ds) = runState (docs p) Map.empty