module Agda.Syntax.IdiomBrackets (parseIdiomBracketsSeq) where import Control.Monad import Agda.Syntax.Common import Agda.Syntax.Position import Agda.Syntax.Concrete import Agda.Syntax.Concrete.Operators import Agda.Syntax.Concrete.Pretty ( leftIdiomBrkt, rightIdiomBrkt ) import Agda.Syntax.Scope.Base import Agda.Syntax.Scope.Monad import Agda.TypeChecking.Monad import Agda.Utils.List1 ( List1, pattern (:|), (<|) ) import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.Utils.Singleton parseIdiomBracketsSeq :: Range -> [Expr] -> ScopeM Expr parseIdiomBracketsSeq :: Range -> [Expr] -> ScopeM Expr parseIdiomBracketsSeq Range r [Expr] es = do let qEmpty :: QName qEmpty = Name -> QName QName (Name -> QName) -> Name -> QName forall a b. (a -> b) -> a -> b $ [Char] -> Name simpleName [Char] "empty" qPlus :: QName qPlus = Name -> QName QName (Name -> QName) -> Name -> QName forall a b. (a -> b) -> a -> b $ [Char] -> Name simpleBinaryOperator [Char] "<|>" ePlus :: Expr -> Expr -> Expr ePlus Expr a Expr b = Range -> Expr -> NamedArg Expr -> Expr App Range r (Range -> Expr -> NamedArg Expr -> Expr App Range r (QName -> Expr Ident QName qPlus) (Expr -> NamedArg Expr forall a. a -> NamedArg a defaultNamedArg Expr a)) (Expr -> NamedArg Expr forall a. a -> NamedArg a defaultNamedArg Expr b) case [Expr] es of [] -> QName -> ScopeM () ensureInScope QName qEmpty ScopeM () -> ScopeM Expr -> ScopeM Expr forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> Expr -> ScopeM Expr forall a. a -> TCMT IO a forall (m :: * -> *) a. Monad m => a -> m a return (QName -> Expr Ident QName qEmpty) [Expr e] -> Range -> Expr -> ScopeM Expr parseIdiomBrackets Range r Expr e es :: [Expr] es@(Expr _:[Expr] _) -> do QName -> ScopeM () ensureInScope QName qPlus es' <- (Expr -> ScopeM Expr) -> [Expr] -> TCMT IO [Expr] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b] mapM (Range -> Expr -> ScopeM Expr parseIdiomBrackets Range r) [Expr] es return $ foldr1 ePlus es' parseIdiomBrackets :: Range -> Expr -> ScopeM Expr parseIdiomBrackets :: Range -> Expr -> ScopeM Expr parseIdiomBrackets Range r Expr e = do let qPure :: QName qPure = Name -> QName QName (Name -> QName) -> Name -> QName forall a b. (a -> b) -> a -> b $ [Char] -> Name simpleName [Char] "pure" qAp :: QName qAp = Name -> QName QName (Name -> QName) -> Name -> QName forall a b. (a -> b) -> a -> b $ [Char] -> Name simpleBinaryOperator [Char] "<*>" ePure :: Expr -> Expr ePure = Range -> Expr -> NamedArg Expr -> Expr App Range r (QName -> Expr Ident QName qPure) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr forall b c a. (b -> c) -> (a -> b) -> a -> c . Expr -> NamedArg Expr forall a. a -> NamedArg a defaultNamedArg eAp :: Expr -> Expr -> Expr eAp Expr a Expr b = Range -> Expr -> NamedArg Expr -> Expr App Range r (Range -> Expr -> NamedArg Expr -> Expr App Range r (QName -> Expr Ident QName qAp) (Expr -> NamedArg Expr forall a. a -> NamedArg a defaultNamedArg Expr a)) (Expr -> NamedArg Expr forall a. a -> NamedArg a defaultNamedArg Expr b) (QName -> ScopeM ()) -> [QName] -> ScopeM () forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => (a -> m b) -> t a -> m () mapM_ QName -> ScopeM () ensureInScope [QName qPure, QName qAp] case Expr e of RawApp Range _ List2 Expr es -> do e :| es <- Expr -> ScopeM (List1 Expr) appViewM (Expr -> ScopeM (List1 Expr)) -> ScopeM Expr -> ScopeM (List1 Expr) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b =<< List2 Expr -> ScopeM Expr parseApplication List2 Expr es return $ foldl eAp (ePure e) es Expr _ -> Expr -> ScopeM Expr forall a. a -> TCMT IO a forall (m :: * -> *) a. Monad m => a -> m a return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr forall a b. (a -> b) -> a -> b $ Expr -> Expr ePure Expr e appViewM :: Expr -> ScopeM (List1 Expr) appViewM :: Expr -> ScopeM (List1 Expr) appViewM = \case e :: Expr e@App{} -> let AppView Expr e' [NamedArg Expr] es = Expr -> AppView appView Expr e in (Expr e' Expr -> [Expr] -> List1 Expr forall a. a -> [a] -> NonEmpty a :|) ([Expr] -> List1 Expr) -> TCMT IO [Expr] -> ScopeM (List1 Expr) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (NamedArg Expr -> ScopeM Expr) -> [NamedArg Expr] -> TCMT IO [Expr] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b] mapM NamedArg Expr -> ScopeM Expr forall {m :: * -> *} {a}. (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Arg (Named NamedName a) -> m a onlyVisible [NamedArg Expr] es OpApp Range _ QName op Set Name _ OpAppArgs es -> (QName -> Expr Ident QName op Expr -> [Expr] -> List1 Expr forall a. a -> [a] -> NonEmpty a :|) ([Expr] -> List1 Expr) -> TCMT IO [Expr] -> ScopeM (List1 Expr) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> ScopeM Expr) -> OpAppArgs -> TCMT IO [Expr] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b] mapM (OpApp Expr -> ScopeM Expr forall {m :: * -> *} {a}. (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => OpApp a -> m a ordinary (OpApp Expr -> ScopeM Expr) -> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> TCMT IO (OpApp Expr)) -> Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> ScopeM Expr forall (m :: * -> *) b c a. Monad m => (b -> m c) -> (a -> m b) -> a -> m c <=< MaybePlaceholder (OpApp Expr) -> TCMT IO (OpApp Expr) forall {m :: * -> *} {a}. (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => MaybePlaceholder a -> m a noPlaceholder (MaybePlaceholder (OpApp Expr) -> TCMT IO (OpApp Expr)) -> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> TCMT IO (MaybePlaceholder (OpApp Expr))) -> Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> TCMT IO (OpApp Expr) forall (m :: * -> *) b c a. Monad m => (b -> m c) -> (a -> m b) -> a -> m c <=< Arg (Named NamedName (MaybePlaceholder (OpApp Expr))) -> TCMT IO (MaybePlaceholder (OpApp Expr)) forall {m :: * -> *} {a}. (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Arg (Named NamedName a) -> m a onlyVisible) OpAppArgs es Expr e -> List1 Expr -> ScopeM (List1 Expr) forall a. a -> TCMT IO a forall (m :: * -> *) a. Monad m => a -> m a return (List1 Expr -> ScopeM (List1 Expr)) -> List1 Expr -> ScopeM (List1 Expr) forall a b. (a -> b) -> a -> b $ Expr -> List1 Expr forall el coll. Singleton el coll => el -> coll singleton Expr e where onlyVisible :: Arg (Named NamedName a) -> m a onlyVisible Arg (Named NamedName a) a | () -> NamedArg () forall a. a -> NamedArg a defaultNamedArg () NamedArg () -> NamedArg () -> Bool forall a. Eq a => a -> a -> Bool == (Named NamedName a -> Named NamedName ()) -> Arg (Named NamedName a) -> NamedArg () forall a b. (a -> b) -> Arg a -> Arg b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (() () -> Named NamedName a -> Named NamedName () forall a b. a -> Named NamedName b -> Named NamedName a forall (f :: * -> *) a b. Functor f => a -> f b -> f a <$) Arg (Named NamedName a) a = a -> m a forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (a -> m a) -> a -> m a forall a b. (a -> b) -> a -> b $ Arg (Named NamedName a) -> a forall a. NamedArg a -> a namedArg Arg (Named NamedName a) a | Bool otherwise = [Char] -> m a forall (m :: * -> *) a. (HasCallStack, MonadTCError m) => [Char] -> m a genericError [Char] "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)" noPlaceholder :: MaybePlaceholder a -> m a noPlaceholder Placeholder{} = [Char] -> m a forall (m :: * -> *) a. (HasCallStack, MonadTCError m) => [Char] -> m a genericError [Char] "Naked sections are not allowed in idiom brackets" noPlaceholder (NoPlaceholder Maybe PositionInName _ a x) = a -> m a forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return a x ordinary :: OpApp a -> m a ordinary (Ordinary a a) = a -> m a forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return a a ordinary OpApp a _ = [Char] -> m a forall (m :: * -> *) a. (HasCallStack, MonadTCError m) => [Char] -> m a genericError [Char] "Binding syntax is not allowed in idiom brackets" ensureInScope :: QName -> ScopeM () ensureInScope :: QName -> ScopeM () ensureInScope QName q = do r <- QName -> ScopeM ResolvedName resolveName QName q case r of ResolvedName UnknownName -> [Char] -> ScopeM () forall (m :: * -> *) a. (HasCallStack, MonadTCError m) => [Char] -> m a genericError ([Char] -> ScopeM ()) -> [Char] -> ScopeM () forall a b. (a -> b) -> a -> b $ QName -> [Char] forall a. Pretty a => a -> [Char] prettyShow QName q [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ [Char] " needs to be in scope to use idiom brackets " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Doc -> [Char] forall a. Pretty a => a -> [Char] prettyShow Doc leftIdiomBrkt [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ [Char] " ... " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Doc -> [Char] forall a. Pretty a => a -> [Char] prettyShow Doc rightIdiomBrkt ResolvedName _ -> () -> ScopeM () forall a. a -> TCMT IO a forall (m :: * -> *) a. Monad m => a -> m a return ()