packages feed

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

------------------------------------------------------------------------
-- A memoising variant of the standard backtracking parser combinators
------------------------------------------------------------------------

-- Following Frost/Szydlowski and Frost/Hafiz/Callaghan (but without
-- the left recursion fix). An improvement has been made: The user
-- does not have to insert memoisation annotations manually. Instead
-- all grammar non-terminals are memoised. This is perhaps a bit less
-- flexible, but less error-prone, since there is no need to guarantee
-- that all "keys" (arguments to the memoise combinator) are unique.

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}

module Memoised where

import Control.Monad.State.Strict
import Control.Applicative
import qualified IndexedMap as IMap
import Control.Arrow
import IndexedOrd
import qualified Parser

-- | Positions.

type Pos = Integer

-- | Lists annotated with positions.

type AnnList tok = [ (Pos, tok) ]

-- | Keys used by the memoisation code. 'Nothing' is used to indicate
-- the end of the input.

data Key nt r = Key (nt r) (Maybe Pos)

instance IndexedEq nt => IndexedEq (Key nt) where
  iEq (Key x1 y1) (Key x2 y2) = case (y1 == y2, iEq x1 x2) of
    (True, Just eq) -> Just eq
    _               -> Nothing

instance IndexedOrd nt => IndexedOrd (Key nt) where
  iCompare (Key x1 y1) (Key x2 y2) = case compare y1 y2 of
    LT -> LT
    EQ -> iCompare x1 x2
    GT -> GT

-- | Memoised values.

newtype Value tok r = Value [(r, AnnList tok)]

-- | The parser type.

-- I did not replace the first function space with a reader monad
-- since the type checker had trouble handling the rank-2 argument
-- type (Parser.Grammar ...).

newtype Parser nt tok r =
  P { unP :: Parser.Grammar (Parser nt tok) nt ->
             AnnList tok ->
             State (IMap.Map (Key nt) (Value tok)) [(r, AnnList tok)] }

instance Functor (Parser nt tok) where
  fmap f (P p) = P $ \g input -> fmap (map (f *** id)) (p g input)

instance Monad (Parser nt tok) where
  return x  = P $ \_ input -> return [(x, input)]
  P p >>= f = P $ \g input -> do
    rs <- p g input
    fmap concat $ mapM (\(x, toks) -> unP (f x) g toks) rs

instance Applicative (Parser nt tok) where
  pure      = return
  p1 <*> p2 = p1 >>= \f -> fmap f p2

instance Alternative (Parser nt tok) where
  empty         = P $ \_ _     -> return empty
  P p1 <|> P p2 = P $ \g input -> liftM2 (<|>) (p1 g input) (p2 g input)

parse :: Parser.Grammar (Parser nt tok) nt ->
         Parser nt tok r -> [tok] -> [r]
parse g p toks =
  map fst .
  filter (null . snd) .
  flip evalState IMap.empty $
  unP p g (zip [1 ..] toks)

instance Parser.Parser (Parser nt tok) tok where
  symbol = P $ \_ input -> return $
    case input of
      (_, c) : cs -> return (c, cs)
      _           -> empty

  parse = parse (const empty)

-- | Non-terminals are memoised.

instance Parser.NTParser (Parser nt tok) nt tok where
  nonTerm x = P $ \grammar input -> do
    let key = Key x (case input of
                       (pos, _) : _ -> Just pos
                       []           -> Nothing)
    res' <- lookupTable key
    case res' of
      Just (Value v) -> return v
      Nothing        -> do
        rs <- unP (grammar x) grammar input
        modifyTable (IMap.insert key (Value rs))
        return rs
    where
    lookupTable k = fmap (IMap.lookup k) get
    modifyTable f = modify f

  parseWithGrammar = parse