Agda-2.3.2.2: src/prototyping/mixfix/ExpressionParser.hs
------------------------------------------------------------------------
-- Turning graphs into expression parsers
------------------------------------------------------------------------
{-# LANGUAGE FlexibleContexts, GADTs #-}
module ExpressionParser
( NT
, parse
) where
import qualified Parser
import Parser hiding (parse)
import PrecedenceGraph
import Utilities
import IndexedOrd
import Name
import Token
import Expression
import qualified MemoisedCPS
import Control.Applicative as A
import Data.Foldable (asum)
import qualified Data.List as List
import qualified Data.Set as Set
import Data.Set (Set)
-- | Looks up all names of the given fixity, regardless of the
-- annotation.
(!*) :: Annotation -> Fixity -> Set Name
m !* k = Set.unions [m ! (k, ass) | ass <- [Non, L, R]]
-- | Operator applications.
type Op = (Name, [Maybe Expr])
-- | Functions for applying 'Op'erator applications to 'Expr'essions.
appLeft :: Maybe Expr -> Op -> Op
appLeft e (u, es) = (u, e : es)
appRight :: Op -> Maybe Expr -> Op
appRight (u, es) e = (u, es ++ [e])
appBoth :: Maybe Expr -> Op -> Maybe Expr -> Op
appBoth e1 o e2 = appLeft e1 (appRight o e2)
-- | Converts an 'Op'erator application to an 'Expr'ession.
toE :: Op -> Expr
toE (u, es) = Op u es
-- | Nonterminals used by the expression grammar.
data NT r where
ExprN :: Set Node -> NT Expr
OpN :: Set Name -> NT Op
NodeN :: Node -> NT Expr
PostLeftsN :: Node -> NT Expr
AtomN :: NT Expr
-- | Non-terminal for an expression.
expression :: PrecedenceGraph -> NT Expr
expression g = ExprN (nodes g)
-- | A placeholder of the given kind.
placeholder :: NTParser p NT Token => Pos -> p (Maybe Expr)
placeholder p = Nothing <$ sym (Placeholder p)
-- | Parses the given name part (possibly with a shorter module
-- prefix).
namePart :: NTParser p NT Token
=> [String]
-- ^ Module name.
-> String
-- ^ Name part.
-> p ()
namePart ms n = symbol >>= \s -> case s of
QualifiedName ms' n' -> if ms' `List.isSuffixOf` ms && n' == n
then return () else A.empty
_ -> A.empty
-- | The expression grammar.
grammar :: NTParser p NT Token =>
PrecedenceGraph ->
-- ^ The precedence graph.
(Name -> Set Name) ->
-- ^ A function giving all qualified names matching the
-- given qualified name (which might be given with an
-- incomplete module name prefix).
Set Name ->
-- ^ Closed mixfix operators.
NT r -> p r
-- Note that parentheses should not be treated here. The top-level
-- parser should take care of let, lambda, parentheses, hidden
-- argument braces, and pattern dots. (And perhaps something else as
-- well.)
-- Note also that an operator which is sectioned in the right way
-- becomes closed.
grammar g lookupName closed AtomN =
Fun <$> (asum =<< map return . filter (not . isOperator) .
Set.toList . lookupName <$> parseName)
<|> WildcardE <$ sym Wildcard
<|> sym LParen *> nonTerm (expression g) <* sym RParen
<|> toE <$> ( nonTerm (OpN closed)
<|> appRight <$> nonTerm (OpN prefix) <*> placeholder End
<|> appLeft <$> placeholder Beg <*> nonTerm (OpN postfix)
<|> appBoth <$> placeholder Beg <*> nonTerm (OpN infx) <*>
placeholder End)
where
allOps = allOperators g
prefix = allOps !* Prefix
postfix = allOps !* Postfix
infx = allOps !* Infix
-- Production for a subset of the expressions. Only the nodes
-- reachable from the given set of nodes are recognised.
grammar _ _ _ (ExprN ns)
= app <$> nonTerm AtomN <*> many (nonTerm AtomN)
<|> asum (map (nonTerm . NodeN) $ Set.toList ns)
-- Production for operators (just the internal, mixfix parts; not the
-- "outer" arguments).
grammar g _ _ (OpN ops) = asum $ map op (Set.toList ops)
where
op n = (,) n <$>
(Just <$> nonTerm (expression g) <|> placeholder Mid)
`between`
map (namePart (moduleName n)) (nameParts n)
-- Production for a graph node.
grammar g _ _ (NodeN n) =
nonAssoc <|> preRights <|> nonTerm (PostLeftsN n)
where
-- Applications of non-associative operators.
nonAssoc = appBoth' <$>
higher g n <*> internal g n Infix Non <*> higher g n
-- Sequences of prefix/infix right-associative operators.
preRights = preRight <*> (preRights <|> higher g n)
where
preRight = appRight' <$> internal g n Prefix Non
<|> appBoth' <$> higher g n <*> internal g n Infix R
appRight' o e2 = toE $ appRight o (Just e2)
appBoth' e1 o e2 = toE $ appBoth (Just e1) o (Just e2)
-- Sequences of postfix/infix left-associative operators. (This
-- non-terminal needs to be memoised: it is left recursive.)
grammar g _ _ (PostLeftsN n) = flip ($) <$>
(nonTerm (PostLeftsN n) <|> higher g n) <*> postLeft
where
postLeft = appLeft' <$> internal g n Postfix Non
<|> appBoth' <$> internal g n Infix L <*> higher g n
appLeft' o e1 = toE $ appLeft (Just e1) o
appBoth' o e2 e1 = toE $ appBoth (Just e1) o (Just e2)
-- | Production for the internal parts of operators of the given
-- fixity (in this node). Includes certain sections; for instance, a
-- left-sectioned infix operator becomes a prefix operator.
internal :: NTParser p NT Token =>
PrecedenceGraph -> Node -> Fixity -> Assoc -> p Op
internal g n f ass =
nonTerm (OpN (ann ! (f, ass)))
<|> case f of
Prefix -> appLeft <$> placeholder Beg <*> infx
Postfix -> appRight <$> infx <*> placeholder End
Infix -> A.empty
where
ann = annotation g n
infx = nonTerm (OpN (ann !* Infix))
-- | Production for expressions of higher precedence or atoms.
higher :: NTParser p NT Token =>
PrecedenceGraph -> Node -> p Expr
higher g n = nonTerm (ExprN (successors g n))
-- | Parses an expression.
parse :: PrecedenceGraph ->
-- ^ The precedence graph.
(Name -> Set Name) ->
-- ^ A function giving all qualified names matching the
-- given qualified name (which might be given with an
-- incomplete module name prefix).
Set Name ->
-- ^ Closed mixfix operators.
[Token] ->
-- ^ Input tokens.
[Expr]
parse g lookupName closed =
MemoisedCPS.parse (grammar g lookupName closed)
(nonTerm $ expression g)
------------------------------------------------------------------------
-- Boring instances
instance IndexedEq NT where
iEq (ExprN ns1) (ExprN ns2) = boolToEq $ ns1 == ns2
iEq (OpN ns1) (OpN ns2) = boolToEq $ ns1 == ns2
iEq (NodeN n1) (NodeN n2) = boolToEq $ n1 == n2
iEq (PostLeftsN n1) (PostLeftsN n2) = boolToEq $ n1 == n2
iEq AtomN AtomN = Just Refl
iEq _ _ = Nothing
instance IndexedOrd NT where
iCompare (ExprN ns1) (ExprN ns2) = compare ns1 ns2
iCompare (OpN ns1) (OpN ns2) = compare ns1 ns2
iCompare (NodeN n1) (NodeN n2) = compare n1 n2
iCompare (PostLeftsN n1) (PostLeftsN n2) = compare n1 n2
iCompare AtomN AtomN = EQ
iCompare (ExprN _) _ = LT
iCompare (OpN _) (ExprN _) = GT
iCompare (OpN _) _ = LT
iCompare (NodeN _) (ExprN _) = GT
iCompare (NodeN _) (OpN _) = GT
iCompare (NodeN _) _ = LT
iCompare (PostLeftsN _) AtomN = LT
iCompare (PostLeftsN _) _ = GT
iCompare AtomN _ = GT