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 Agda.TypeChecking.Monad.Benchmark (billSub)
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
import Agda.Utils.List
#include "undefined.h"
import Agda.Utils.Impossible
partsInScope :: FlatScope -> ScopeM (Set QName)
partsInScope flat = do
(names, ops) <- localNames flat
let xs = concatMap parts names ++ concatMap notationNames ops
return $ Set.fromList xs
where
qual xs x = foldr Qual (QName x) xs
parts q = parts' (init $ qnameParts q) (unqualify q)
parts' ms (NoName _ _) = []
parts' ms x@(Name _ [_]) = [qual ms x]
parts' ms x@(Name _ xs) = qual ms x : qual ms (Name noRange [first]) : [ QName $ Name noRange [i] | i <- iparts ]
where
first:iparts = [ i | i@(Id {}) <- xs ]
type FlatScope = Map QName [AbstractName]
getDefinedNames :: [KindOfName] -> FlatScope -> [(QName, Fixity')]
getDefinedNames kinds names =
[ (x, chooseFixity fixs)
| (x, ds) <- Map.toList names
, any ((`elem` kinds) . anameKind) ds
, let fixs = map (A.nameFixity . A.qnameName . anameName) ds
, not (null fixs)
]
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
]
return $ split $ uniqOn fst $ map localOp locals ++ defs
where
localOp (x, y) = (QName x, A.nameFixity y)
split ops = partitionEithers $ concatMap opOrNot ops
opOrNot (q, Fixity' fx syn) = Left q : map Right (notaFromName ++ nota)
where
notaFromName = case unqualify q of
Name _ [_] -> []
x -> [NewNotation q fx $ syntaxOf x]
nota = if null syn then [] else [NewNotation q fx syn]
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 $ map oldToNewNotation cons
opsparts = Set.fromList $ concatMap notationNames $ ops
allParts = Set.union conparts opsparts
connames = Set.fromList $ map fst 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
isinfixl, isinfixr, isinfix, nonfix, isprefix, ispostfix :: NewNotation -> Bool
isinfixl (NewNotation _ (LeftAssoc _ _) syn) = isInfix syn
isinfixl _ = False
isinfixr (NewNotation _ (RightAssoc _ _) syn) = isInfix syn
isinfixr _ = False
isinfix (NewNotation _ (NonAssoc _ _) syn) = isInfix syn
isinfix _ = False
nonfix (NewNotation _ _ syn) = notationKind syn == NonfixNotation
isprefix (NewNotation _ _ syn) = notationKind syn == PrefixNotation
ispostfix (NewNotation _ _ syn) = notationKind syn == PostfixNotation
isInfix :: Notation -> Bool
isInfix syn = notationKind syn == InfixNotation
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 isinfixl
inrfx = fixP infixrP isinfixr
infx = fixP infixP isinfix
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 ]
instance IsExpr Expr where
exprView e = case e of
Ident x -> LocalV x
App _ e1 e2 -> AppV e1 e2
OpApp r d es -> OpAppV d es
HiddenArg _ e -> HiddenArgV e
InstanceArg _ e -> InstanceArgV e
Paren _ e -> ParenV e
Lam _ bs e -> LamV bs e
Underscore{} -> WildV e
_ -> OtherV e
unExprView e = case e of
LocalV x -> Ident x
AppV e1 e2 -> App (fuseRange e1 e2) e1 e2
OpAppV d es -> OpApp (fuseRange d es) d es
HiddenArgV e -> HiddenArg (getRange e) e
InstanceArgV e -> InstanceArg (getRange e) e
ParenV e -> Paren (getRange e) e
LamV bs e -> Lam (fuseRange bs e) bs e
WildV e -> e
OtherV e -> e
instance IsExpr Pattern where
exprView e = case e of
IdentP x -> LocalV x
AppP e1 e2 -> AppV e1 e2
OpAppP r d es -> OpAppV d ((map . fmap . fmap) Ordinary es)
HiddenP _ e -> HiddenArgV e
InstanceP _ e -> InstanceArgV e
ParenP _ e -> ParenV e
WildP{} -> WildV e
_ -> OtherV e
unExprView e = case e of
LocalV x -> IdentP x
AppV e1 e2 -> AppP e1 e2
OpAppV d es -> let ess :: [NamedArg Pattern]
ess = (map . fmap . fmap) (fromOrdinary __IMPOSSIBLE__) es
in OpAppP (fuseRange d es) d ess
HiddenArgV e -> HiddenP (getRange e) e
InstanceArgV e -> InstanceP (getRange e) e
ParenV e -> ParenP (getRange e) e
LamV _ _ -> __IMPOSSIBLE__
WildV e -> e
OtherV e -> e
lhsArgs :: Pattern -> (Name, [NamedArg Pattern])
lhsArgs p = case lhsArgs' p of
Just (x, args) -> (x, args)
Nothing -> __IMPOSSIBLE__
lhsArgs' :: Pattern -> Maybe (Name, [NamedArg Pattern])
lhsArgs' p = case patternAppView p of
Common.Arg _ (Named _ (IdentP (QName x))) : ps -> Just (x, ps)
_ -> Nothing
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 ps -> fullParen' . OpAppP r d <$> (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 fst $ 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 = 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 = 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]
patternQNames :: Pattern -> [QName]
patternQNames p = case p of
RawAppP _ ps -> concatMap patternQNames ps
IdentP q -> [q]
ParenP _ p -> patternQNames p
HiddenP _ p -> patternQNames (namedThing p)
InstanceP _ p -> patternQNames (namedThing p)
OpAppP r d ps -> __IMPOSSIBLE__
AppP{} -> __IMPOSSIBLE__
AsP r x p -> patternQNames p
AbsurdP{} -> []
WildP{} -> []
DotP{} -> []
LitP{} -> []
QuoteP{} -> []
qualifierModules :: [QName] -> [[Name]]
qualifierModules qs =
nub $ filter (not . null) $ map (init . qnameParts) qs
parseApplication :: [Expr] -> ScopeM Expr
parseApplication [e] = return e
parseApplication es = 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
[] -> do
inScope <- partsInScope flat
case [ x | Ident x <- es, not (Set.member x inScope) ] of
[] -> typeError $ NoParseForApplication es
xs -> typeError $ NotInScope xs
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 = 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)
[] -> do
inScope <- partsInScope flat
case [ x | Ident x <- es_args, not (Set.member x inScope) ] of
[] -> typeError $ NoParseForApplication es
xs -> typeError $ NotInScope xs
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 es -> par $ unExprView $ OpAppV x $ (map . fmap . fmap . fmap) fullParen' es
LamV bs e -> par $ unExprView $ LamV bs (fullParen e)
where
par = unExprView . ParenV