packages feed

Agda-2.3.2.2: src/prototyping/mixfix/benchmarks/PrecedenceGraph.hs

------------------------------------------------------------------------
-- Precedence graphs
------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts, Rank2Types #-}

module PrecedenceGraph
    -- * Precedence graphs.
  ( Name
  , Assoc(..)
  , Fixity(..)
  , Node
  , PrecedenceGraph
    -- * Constructing precedence graphs.
  , empty
  , bindsAs
  , bindsBetween
  , unrelated
    -- * Parsing expressions.
  , Token(..)
  , Expr(..)
  , expressionParser
    -- * Testing.
  , tests
  ) where

import Parser
import qualified Data.List as List
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Graph.Inductive as G
import Data.Graph.Inductive ((&))
import Control.Applicative hiding (empty)
import Control.Monad
import qualified Control.Applicative as A
import qualified Control.Monad.State as S
import qualified Control.Monad.Identity as I
import Data.Function
import Test.QuickCheck

------------------------------------------------------------------------
-- Some helper functions

-- | Converts a set to a list and maps over it.

mapM' :: Monad m => (a -> m b) -> Set a -> m [b]
mapM' f = mapM f . Set.toList

-- | An efficient variant of 'List.nub'.

efficientNub :: Ord a => [a] -> [a]
efficientNub = removeDups . List.sort
  where removeDups = map head . List.group

-- Code used to test efficientNub.

data IgnoreSnd a b = Pair a b
  deriving Show

fst' :: IgnoreSnd a b -> a
fst' (Pair x y) = x

instance (Eq a, Eq b) => Eq (IgnoreSnd a b) where
  (==) = (==) `on` fst'

instance (Ord a, Eq b) => Ord (IgnoreSnd a b) where
  compare = compare `on` fst'

instance (Arbitrary a, Arbitrary b) => Arbitrary (IgnoreSnd a b) where
  arbitrary = liftM2 Pair arbitrary arbitrary

-- | This property tests that 'efficientNub' is equivalent to 'nub',
-- up to a permutation of the output. Note that the property checks
-- that the two functions choose the same representative from every
-- equivalence class.

prop_efficientNub :: [IgnoreSnd Integer Int] -> Property
prop_efficientNub xs =
  classify nonTriv "with non-trivial equivalence classes" $
    efficientNub xs =*= List.sort (List.nub xs)
  where
  xs =*= ys = length xs == length ys && and (zipWith reallyEqual xs ys)
  reallyEqual (Pair x y) (Pair u v) = x == u && y == v

  nonTriv = any ((> 1) . length) $
            map (List.nubBy reallyEqual) $
            List.group $ List.sort xs

------------------------------------------------------------------------
-- Types

-- | A name is a /non-empty/ list of /non-empty/ name parts.

type Name = [String]

-- | Associativity.

data Assoc = Non | L | R
             deriving (Eq, Ord, Show)

-- | Fixity.

data Fixity = Prefix | Postfix | Infix Assoc
              deriving (Eq, Ord, Show)

-- | Precedence graph node labels.

type Node = Int

-- | Precedence graphs.

-- Invariant: Has to be acyclic.

newtype PrecedenceGraph =
  PG { unPG :: G.Gr (Map Fixity (Set Name)) () }
     deriving Show

------------------------------------------------------------------------
-- Inspecting precedence graphs

-- | The successors of a node.

successors :: PrecedenceGraph -> Node -> Set Node
successors g n = Set.fromList $ G.suc (unPG g) n

-- | A node's annotation.

annotation :: PrecedenceGraph -> Node -> Map Fixity (Set Name)
annotation g n = case G.lab (unPG g) n of
  Nothing  -> Map.empty
  Just ann -> ann

-- | The nodes in the graph.

nodes :: PrecedenceGraph -> Set Node
nodes = Set.fromList . G.nodes . unPG

-- | Is the graph acyclic?

-- Check this by ensuring that the graph is simple (no loops) and all
-- strongly connected components have size 1.

acyclic :: PrecedenceGraph -> Bool
acyclic (PG g) = G.isSimple g && all (\c -> length c == 1) (G.scc g)

------------------------------------------------------------------------
-- Constructing precedence graphs

-- An empty precedence graph.

empty :: PrecedenceGraph
empty = PG G.empty

-- @bindsAs op fix n g@ adds @op@ (with fixity @fix@) to node @n@.
--
-- Precondition: @n@ has to exist in @g@, and @n@ should not already
-- be annotated with @op@. (The second precondition is not checked.)

bindsAs :: Name -> Fixity -> Node -> PrecedenceGraph -> PrecedenceGraph
bindsAs op fix n (PG g) = case G.match n g of
  (Nothing, g') -> error "bindsAs: The node does not exist."
  (Just (pre, n, a, suc), g') ->
    PG ((pre, n, Map.adjust (Set.insert op) fix a, suc) & g')

-- @bindsBetween op fix tighterThan looserThan n g@ adds a new node to
-- @g@, annotated with @op@ (with fixity @fix@). Edges are added from
-- all nodes in @tighterThan@, and their predecessors. Edges are also
-- added to all nodes in @looserThan@, and their successors. The new
-- node label is returned along with the new graph.
--
-- Precondition: The resulting graph has to be acyclic.

bindsBetween :: Name -> Fixity -> [Node] -> [Node] ->
                PrecedenceGraph -> (Node, PrecedenceGraph)
bindsBetween op fixity tighterThan looserThan (PG g)
  -- The test for acyclicity is rather slow.
  | True {- acyclic g' -} = (new, g')
  | otherwise             = error "bindsBetween: Cyclic result."
  where
  [new]          = G.newNodes 1 g
  allLooserThan  = looserThan  : map (G.suc g) looserThan
  allTighterThan = tighterThan : map (G.pre g) tighterThan
  fix            = map ((,) ()) . efficientNub . concat
  ctxt           = ( fix allTighterThan
                   , new
                   , Map.singleton fixity (Set.singleton op)
                   , fix allLooserThan
                   )
  g'             = PG (ctxt & g)

-- @unrelated op fix g@ add a fresh node to @g@, annotated with @op@
-- (with fixity @fix@). No new edges are added.

unrelated :: Name -> Fixity -> PrecedenceGraph ->
             (Node, PrecedenceGraph)
unrelated op fix = bindsBetween op fix [] []

------------------------------------------------------------------------
-- Turning graphs into expression parsers

-- | Tokens.

data Token = Atom | Name String
  deriving (Eq, Ord, Show)

-- | Expressions.

data Expr = AtomE | Op String [Expr]
  deriving (Eq, Ord, Show)

-- | The internal, mixfix part of an operator (the name, excluding outer
-- '_', plus the internal expressions).

type Op = (String, [Expr])

-- | The parser type used below. The state component is used to
-- memoise the computation of node parsers.

type P r = forall p. Parser p Node Expr Token =>
           S.State (Map Node (p Expr)) (p r)

-- | Expression parser. Parameterised on a graph describing the
-- operators.

expressionParser :: Parser p Node Expr Token =>
                    PrecedenceGraph -> p Expr
expressionParser g = S.evalState (expr g (nodes g)) Map.empty

-- | Parses a subset of the expressions. Only the nodes reachable from
-- the given list of nodes are recognised by the parser.

-- Note that Atom stands for applications of one or more identifiers,
-- parenthesised expressions, or mixfix operators that are not prefix,
-- postfix or infix. Hence the atom parser will probably be
-- implemented using expressionParser.

expr :: PrecedenceGraph -> Set Node -> P Expr
expr g ns = do
  ns <- mapM' (node g) ns
  return $ (AtomE <$ sym Atom) <|> choice ns

-- | Parser for one operator (just the internal, mixfix part).

-- Note that this function uses the non-memoised (expressionParser g)
-- instead of the memoised (expr g (nodes g)). The reason is that
-- otherwise the memoisation is not sufficiently productive. This
-- could be fixed by inserting the parsers into the memo table
-- _before_ computing them, by using recursive do in "node" below.
-- However, I think recursive do is too complicated. The current
-- solution is easier to understand and gives roughly the same
-- performance.

opProd :: PrecedenceGraph -> Name -> P Op
opProd g nameParts =
  return $ (,) (List.intercalate "_" nameParts) <$>
           (expressionParser g `between` map Name nameParts)

-- | Parser for several operators.

opProds :: PrecedenceGraph -> Set Name -> P Op
opProds g ops = fmap choice (mapM' (opProd g) ops)

appLeft :: Expr -> Op -> Expr
appLeft e (n, es) = Op ('_' : n) (e : es)

appRight :: Op -> Expr -> Expr
appRight (n, es) e = Op (n ++ "_") (es ++ [e])

appBoth :: Op -> Expr -> Expr -> Expr
appBoth (n, es) l r = Op ('_' : n ++ "_") (l : es ++ [r])

-- | Parser for a node.
--
-- The graph typically has lots of sharing (many pointers to the same
-- node), so this function is memoised. In two ways, actually:
--
-- 1) The construction of the parsers is memoised.
--
-- 2) If a memoising parser is used the results of parsing a given
--    node at a specific position are also memoised.
--
-- Note that the second memoisation is potentially unsafe, if this
-- parser is combined with another memoised parser. The memoisation
-- keys have to be unique.

node :: PrecedenceGraph -> Node -> P Expr
node g n = do
  memoisedP <- fmap (Map.lookup n) S.get
  case memoisedP of
    Just p  -> return p
    Nothing -> do
      -- Parser for operators of higher precedence.
      h <- expr g (successors g n)
      p <- fmap (memoise n . choice) $ sequence (opParsers h)
      S.modify (Map.insert n p)
      return p
  where
  m ! k = case Map.lookup k m of
    Nothing -> Set.empty
    Just ns -> ns

  ops fixity f = fmap f (opProds g (annotation g n ! fixity))
                        -- Parser for the internal parts of operators
                        -- of the given fixity (in this node).

  opParsers h =
    [ ops Prefix      (\o -> flip (foldr appRight) <$> many1 o <*> h)
    , ops Postfix     (\o -> foldl appLeft         <$> h <*> many1 o)
    , ops (Infix Non) (\o -> flip appBoth <$> h <*> o <*> h)
    , ops (Infix L)   (\o -> chainl3 h (appBoth <$> o))
    , ops (Infix R)   (\o -> chainr3 h (appBoth <$> o))
    ]

------------------------------------------------------------------------
-- All test cases

-- | All tests from this module.

tests = do
  quickCheck prop_efficientNub