module Agda.Syntax.Concrete.Operators
( parseApplication
, parseModuleApplication
, parseLHS
, parsePattern
, parsePatternSyn
) where
import Control.DeepSeq
import Control.Applicative
import Control.Monad
import Data.Either (partitionEithers)
import Data.Function
import Data.List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
import qualified Data.Traversable as Trav
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Concrete hiding (appView)
import Agda.Syntax.Concrete.Operators.Parser
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.TypeChecking.Monad.Base (typeError, TypeError(..), LHSOrPatSyn(..))
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.State (getScope)
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Either
import Agda.Utils.ReadP
#if MIN_VERSION_base(4,8,0)
import Agda.Utils.List hiding ( uncons )
#else
import Agda.Utils.List
#endif
#include "undefined.h"
import Agda.Utils.Impossible
billToParser :: ScopeM a -> ScopeM a
billToParser = Bench.billTo [Bench.Parsing, Bench.Operators]
type FlatScope = Map QName [AbstractName]
getDefinedNames :: [KindOfName] -> FlatScope -> [[NewNotation]]
getDefinedNames kinds names =
[ mergeNotations $
map (\d -> namesToNotation x (A.qnameName $ anameName d)) ds
| (x, ds) <- Map.toList names
, any ((`elem` kinds) . anameKind) ds
, not (null ds)
]
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames flat = do
let defs = getDefinedNames allKindsOfNames flat
locals <- notShadowedLocals <$> getLocalVars
reportSLn "scope.operators" 50 $ unlines
[ "flat = " ++ show flat
, "defs = " ++ show defs
, "locals= " ++ show locals
]
let localNots = map localOp locals
localNames = Set.fromList $ map notaName localNots
otherNots = filter (\n -> not (Set.member (notaName n) localNames))
(concat defs)
return $ split $ localNots ++ otherNots
where
localOp (x, y) = namesToNotation (QName x) y
split ops = partitionEithers $ concatMap opOrNot ops
opOrNot n = Left (notaName n) :
if null (notation n) then [] else [Right n]
data Parsers e = Parsers
{ pTop :: ReadP e e
, pApp :: ReadP e e
, pArgs :: ReadP e [NamedArg e]
, pNonfix :: ReadP e e
, pAtom :: ReadP e e
}
data UseBoundNames = UseBoundNames | DontUseBoundNames
buildParsers :: forall e. IsExpr e => Range -> FlatScope -> UseBoundNames -> ScopeM (Parsers e)
buildParsers r flat use = do
(names, ops) <- localNames flat
let cons = getDefinedNames [ConName, PatternSynName] flat
reportSLn "scope.operators" 50 $ unlines
[ "names = " ++ show names
, "ops = " ++ show ops
, "cons = " ++ show cons ]
let conparts = Set.fromList $ concatMap notationNames $ concat cons
opsparts = Set.fromList $ concatMap notationNames ops
allParts = Set.union conparts opsparts
connames = Set.fromList $ map (notaName . head) cons
(non, fix) = partition nonfix ops
set = Set.fromList names
isAtom x = case use of
UseBoundNames -> not (Set.member x allParts) || Set.member x set
DontUseBoundNames -> not (Set.member x conparts) || Set.member x connames
let chain = foldr ( $ )
return $ Data.Function.fix $ \p -> Parsers
{ pTop = chain (pApp p) (concatMap (mkP (pTop p)) (order fix))
, pApp = appP (pNonfix p) (pArgs p)
, pArgs = argsP (pNonfix p)
, pNonfix = chain (pAtom p) (map (nonfixP . opP (pTop p)) non)
, pAtom = atomP isAtom
}
where
level :: NewNotation -> Integer
level = fixityLevel . notaFixity
nonfix, isprefix, ispostfix :: NewNotation -> Bool
nonfix = (== NonfixNotation) . notationKind . notation
isprefix = (== PrefixNotation) . notationKind . notation
ispostfix = (== PostfixNotation) . notationKind . notation
isinfix :: Associativity -> NewNotation -> Bool
isinfix ass syn =
notationKind (notation syn) == InfixNotation
&&
fixityAssoc (notaFixity syn) == ass
order :: [NewNotation] -> [[NewNotation]]
order = groupBy ((==) `on` level) . sortBy (compare `on` level)
mkP :: ReadP e e -> [NewNotation] -> [ReadP e e -> ReadP e e]
mkP p0 ops = case concat [infx, inlfx, inrfx, prefx, postfx] of
[] -> [id]
fs -> fs
where
inlfx = fixP infixlP (isinfix LeftAssoc)
inrfx = fixP infixrP (isinfix RightAssoc)
infx = fixP infixP (isinfix NonAssoc)
prefx = fixP prefixP isprefix
postfx = fixP postfixP ispostfix
fixP :: (ReadP e (NewNotation,Range,[e]) -> ReadP e e -> ReadP e e) -> (NewNotation -> Bool) -> [ReadP e e -> ReadP e e]
fixP f g =
case filter g ops of
[] -> []
ops -> [ f $ choice $ map (opP p0) ops ]
patternAppView :: Pattern -> [NamedArg Pattern]
patternAppView p = case p of
AppP p arg -> patternAppView p ++ [arg]
OpAppP _ x _ ps -> defaultNamedArg (IdentP x) : ps
ParenP _ p -> patternAppView p
RawAppP _ _ -> __IMPOSSIBLE__
_ -> [ defaultNamedArg p ]
parsePat :: ReadP Pattern Pattern -> Pattern -> [Pattern]
parsePat prs p = case p of
AppP p (Common.Arg info q) ->
fullParen' <$> (AppP <$> parsePat prs p <*> (Common.Arg info <$> traverse (parsePat prs) q))
RawAppP _ ps -> fullParen' <$> (parsePat prs =<< parse prs ps)
OpAppP r d ns ps -> fullParen' . OpAppP r d ns <$> (mapM . traverse . traverse) (parsePat prs) ps
HiddenP _ _ -> fail "bad hidden argument"
InstanceP _ _ -> fail "bad instance argument"
AsP r x p -> AsP r x <$> parsePat prs p
DotP r e -> return $ DotP r e
ParenP r p -> fullParen' <$> parsePat prs p
WildP _ -> return p
AbsurdP _ -> return p
LitP _ -> return p
QuoteP _ -> return p
IdentP _ -> return p
type ParseLHS = Either Pattern (Name, LHSCore)
parseLHS' :: LHSOrPatSyn -> Maybe Name -> Pattern -> ScopeM ParseLHS
parseLHS' lhsOrPatSyn top p = do
let ms = qualifierModules $ patternQNames p
flat <- flattenScope ms <$> getScope
parsers <- buildParsers (getRange p) flat DontUseBoundNames
let patP = pTop parsers
let cons = getNames [ConName, PatternSynName] flat
let flds = getNames [FldName] flat
case [ res | p' <- force $ parsePat patP p
, res <- validPattern (PatternCheckConfig top cons flds) p' ] of
[(p,lhs)] -> return lhs
[] -> typeError $ NoParseForLHS lhsOrPatSyn p
rs -> typeError $ AmbiguousParseForLHS lhsOrPatSyn p $
map (fullParen . fst) rs
where
getNames kinds flat =
map (notaName . head) $ getDefinedNames kinds flat
validPattern :: PatternCheckConfig -> Pattern -> [(Pattern, ParseLHS)]
validPattern conf p = case (classifyPattern conf p, top) of
(Just r@(Left _), Nothing) -> [(p, r)]
(Just r@(Right _), Just{}) -> [(p, r)]
_ -> []
data PatternCheckConfig = PatternCheckConfig
{ topName :: Maybe Name
, conNames :: [QName]
, fldNames :: [QName]
}
classifyPattern :: PatternCheckConfig -> Pattern -> Maybe ParseLHS
classifyPattern conf p =
case patternAppView p of
Common.Arg _ (Named _ (IdentP x@(QName f))) : ps | Just f == topName conf -> do
guard $ all validPat ps
return $ Right (f, LHSHead f ps)
Common.Arg _ (Named _ (IdentP x)) : ps | x `elem` fldNames conf -> do
ps0 <- mapM classPat ps
let (ps1, rest) = span (isLeft . namedArg) ps0
(p2, ps3) <- uncons rest
guard $ all (isLeft . namedArg) ps3
let (f, lhs) = fromR p2
(ps', _:ps'') = splitAt (length ps1) ps
return $ Right (f, LHSProj x ps' lhs ps'')
_ -> do
guard $ validConPattern (conNames conf) p
return $ Left p
where
validPat = validConPattern (conNames conf) . namedArg
classPat :: NamedArg Pattern -> Maybe (NamedArg ParseLHS)
classPat = Trav.mapM (Trav.mapM (classifyPattern conf))
fromR :: NamedArg (Either a (b, c)) -> (b, NamedArg c)
fromR (Common.Arg info (Named n (Right (b, c)))) = (b, Common.Arg info (Named n c))
fromR (Common.Arg info (Named n (Left a ))) = __IMPOSSIBLE__
parseLHS :: Name -> Pattern -> ScopeM LHSCore
parseLHS top p = billToParser $ do
res <- parseLHS' IsLHS (Just top) p
case res of
Right (f, lhs) -> return lhs
_ -> typeError $ NoParseForLHS IsLHS p
parsePattern :: Pattern -> ScopeM Pattern
parsePattern = parsePatternOrSyn IsLHS
parsePatternSyn :: Pattern -> ScopeM Pattern
parsePatternSyn = parsePatternOrSyn IsPatSyn
parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
parsePatternOrSyn lhsOrPatSyn p = billToParser $ do
res <- parseLHS' lhsOrPatSyn Nothing p
case res of
Left p -> return p
_ -> typeError $ NoParseForLHS lhsOrPatSyn p
validConPattern :: [QName] -> Pattern -> Bool
validConPattern cons p = case appView p of
[_] -> True
IdentP x : ps -> elem x cons && all (validConPattern cons) ps
[QuoteP _, _] -> True
_ -> False
appView :: Pattern -> [Pattern]
appView p = case p of
AppP p a -> appView p ++ [namedArg a]
OpAppP _ op _ ps -> IdentP op : map namedArg ps
ParenP _ p -> appView p
RawAppP _ _ -> __IMPOSSIBLE__
HiddenP _ _ -> __IMPOSSIBLE__
InstanceP _ _ -> __IMPOSSIBLE__
_ -> [p]
qualifierModules :: [QName] -> [[Name]]
qualifierModules qs =
nub $ filter (not . null) $ map (init . qnameParts) qs
parseApplication :: [Expr] -> ScopeM Expr
parseApplication [e] = return e
parseApplication es = billToParser $ do
let ms = qualifierModules [ q | Ident q <- es ]
flat <- flattenScope ms <$> getScope
p <- buildParsers (getRange es) flat UseBoundNames
case force $ parse (pTop p) es of
[e] -> return e
[] -> typeError $ NoParseForApplication es
es' -> typeError $ AmbiguousParseForApplication es $ map fullParen es'
parseModuleIdentifier :: Expr -> ScopeM QName
parseModuleIdentifier (Ident m) = return m
parseModuleIdentifier e = typeError $ NotAModuleExpr e
parseRawModuleApplication :: [Expr] -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication es = billToParser $ do
let e : es_args = es
m <- parseModuleIdentifier e
let ms = qualifierModules [ q | Ident q <- es_args ]
flat <- flattenScope ms <$> getScope
p <- buildParsers (getRange es_args) flat UseBoundNames
case parse (pArgs p) es_args of
[as] -> return (m, as)
[] -> typeError $ NoParseForApplication es
ass -> do
let f = fullParen . foldl (App noRange) (Ident m)
typeError $ AmbiguousParseForApplication es
$ map f ass
parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])
parseModuleApplication (RawApp _ es) = parseRawModuleApplication es
parseModuleApplication (App r e1 e2) = do
(m, args) <- parseModuleApplication e1
return (m, args ++ [e2])
parseModuleApplication e = do
m <- parseModuleIdentifier e
return (m, [])
fullParen :: IsExpr e => e -> e
fullParen e = case exprView $ fullParen' e of
ParenV e -> e
e' -> unExprView e'
fullParen' :: IsExpr e => e -> e
fullParen' e = case exprView e of
LocalV _ -> e
WildV _ -> e
OtherV _ -> e
HiddenArgV _ -> e
InstanceArgV _ -> e
ParenV _ -> e
AppV e1 (Common.Arg info e2) -> par $ unExprView $ AppV (fullParen' e1) (Common.Arg info e2')
where
e2' = case argInfoHiding info of
Hidden -> e2
Instance -> e2
NotHidden -> fullParen' <$> e2
OpAppV x ns es -> par $ unExprView $ OpAppV x ns $ (map . fmap . fmap . fmap) fullParen' es
LamV bs e -> par $ unExprView $ LamV bs (fullParen e)
where
par = unExprView . ParenV