{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fwarn-missing-signatures #-}

module Agda.Syntax.Translation.ReflectedToAbstract where

import Control.Monad.Reader

import Agda.Syntax.Fixity
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Info
import Agda.Syntax.Common
import Agda.Syntax.Abstract as A hiding (Apply)
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Reflected as R
import Agda.Syntax.Internal (Dom,Dom'(..))

import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.Syntax.Scope.Monad (getCurrentModule)

import Agda.Utils.Except
import Agda.Utils.Monad
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Functor
import Agda.Utils.Size

type Names = [Name]

type MonadReflectedToAbstract m =
  ( MonadReader Names m
  , MonadFresh NameId m
  , MonadError TCErr m
  , MonadTCEnv m
  , ReadTCState m
  , HasOptions m
  , HasConstInfo m
  )

-- | Adds a new unique name to the current context.
withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a
withName :: String -> (Name -> m a) -> m a
withName String
s Name -> m a
f = do
  Name
name <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
  [Name]
ctx  <- ([Name] -> [Name]) -> m [Name]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (([Name] -> [Name]) -> m [Name]) -> ([Name] -> [Name]) -> m [Name]
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameConcrete
  let name' :: Name
name' = [Name] -> Name
forall a. [a] -> a
head ([Name] -> Name) -> [Name] -> Name
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Name] -> Name -> Bool
forall (t :: * -> *). Foldable t => t Name -> Name -> Bool
notTaken [Name]
ctx) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> Name -> [Name]
forall a. (a -> a) -> a -> [a]
iterate Name -> Name
nextName Name
name
  ([Name] -> [Name]) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Name
nameName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Name -> m a
f Name
name'
  where
    notTaken :: t Name -> Name -> Bool
notTaken t Name
xs Name
x = Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x Bool -> Bool -> Bool
|| Name -> Name
nameConcrete Name
x Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
xs

-- | Returns the name of the variable with the given de Bruijn index.
askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
askName :: Int -> m (Maybe Name)
askName Int
i = ([Name] -> Maybe Name) -> m (Maybe Name)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ([Name] -> Int -> Maybe Name
forall a. [a] -> Int -> Maybe a
!!! Int
i)

class ToAbstract r a | r -> a where
  toAbstract :: MonadReflectedToAbstract m => r -> m a

-- | Translate reflected syntax to abstract, using the names from the current typechecking context.
toAbstract_ ::
  (ToAbstract r a
  , MonadFresh NameId m
  , MonadError TCErr m
  , MonadTCEnv m
  , ReadTCState m
  , HasOptions m
  , HasConstInfo m
  ) => r -> m a
toAbstract_ :: r -> m a
toAbstract_ = m a -> m a
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (m a -> m a) -> (r -> m a) -> r -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> m a
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstractWithoutImplicit

-- | Drop implicit arguments unless --show-implicit is on.
toAbstractWithoutImplicit ::
  (ToAbstract r a
  , MonadFresh NameId m
  , MonadError TCErr m
  , MonadTCEnv m
  , ReadTCState m
  , HasOptions m
  , HasConstInfo m
  ) => r -> m a
toAbstractWithoutImplicit :: r -> m a
toAbstractWithoutImplicit r
x = ReaderT [Name] m a -> [Name] -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (r -> ReaderT [Name] m a
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract r
x) ([Name] -> m a) -> m [Name] -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames

instance ToAbstract r a => ToAbstract (Named name r) (Named name a) where
  toAbstract :: Named name r -> m (Named name a)
toAbstract = (r -> m a) -> Named name r -> m (Named name a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse r -> m a
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract

instance ToAbstract r a => ToAbstract (Arg r) (NamedArg a) where
  toAbstract :: Arg r -> m (NamedArg a)
toAbstract (Arg ArgInfo
i r
x) = ArgInfo -> Named_ a -> NamedArg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Named_ a -> NamedArg a) -> m (Named_ a) -> m (NamedArg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Named NamedName r -> m (Named_ a)
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (r -> Named NamedName r
forall a name. a -> Named name a
unnamed r
x)

instance ToAbstract [Arg Term] [NamedArg Expr] where
  toAbstract :: [Arg Term] -> m [NamedArg Expr]
toAbstract = (Arg Term -> m (NamedArg Expr)) -> [Arg Term] -> m [NamedArg Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Arg Term -> m (NamedArg Expr)
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract

instance ToAbstract r Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where
  toAbstract :: (Dom r, Name) -> m TypedBinding
toAbstract (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i,unDom :: forall t e. Dom' t e -> e
unDom = r
x, domTactic :: forall t e. Dom' t e -> Maybe t
domTactic = Maybe Term
tac}, Name
name) = do
    Expr
dom <- r -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract r
x
    TypedBinding -> m TypedBinding
forall (m :: * -> *) a. Monad m => a -> m a
return (TypedBinding -> m TypedBinding) -> TypedBinding -> m TypedBinding
forall a b. (a -> b) -> a -> b
$ Range -> [NamedArg Binder] -> Expr -> TypedBinding
mkTBind Range
forall a. Range' a
noRange [ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
i (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
name] Expr
dom

instance ToAbstract (Expr, Elim) Expr where
  toAbstract :: (Expr, Elim) -> m Expr
toAbstract (Expr
f, Apply Arg Term
arg) = do
    NamedArg Expr
arg     <- Arg Term -> m (NamedArg Expr)
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Arg Term
arg
    Bool
showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
    Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ if Bool
showImp Bool -> Bool -> Bool
|| NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg
             then AppInfo -> Expr -> NamedArg Expr -> Expr
App (Origin -> AppInfo -> AppInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected AppInfo
defaultAppInfo_) Expr
f NamedArg Expr
arg
             else Expr
f

instance ToAbstract (Expr, Elims) Expr where
  toAbstract :: (Expr, Elims) -> m Expr
toAbstract (Expr
f, Elims
elims) = (Expr -> Elim -> m Expr) -> Expr -> Elims -> m Expr
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (((Expr, Elim) -> m Expr) -> Expr -> Elim -> m Expr
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Expr, Elim) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract) Expr
f Elims
elims

instance ToAbstract r a => ToAbstract (R.Abs r) (a, Name) where
  toAbstract :: Abs r -> m (a, Name)
toAbstract (Abs String
s r
x) = String -> (Name -> m (a, Name)) -> m (a, Name)
forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> (Name -> m a) -> m a
withName String
s' ((Name -> m (a, Name)) -> m (a, Name))
-> (Name -> m (a, Name)) -> m (a, Name)
forall a b. (a -> b) -> a -> b
$ \Name
name -> (,) (a -> Name -> (a, Name)) -> m a -> m (Name -> (a, Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> r -> m a
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract r
x m (Name -> (a, Name)) -> m Name -> m (a, Name)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> m Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
name
    where s' :: String
s' = if (String -> Bool
forall a. IsNoName a => a -> Bool
isNoName String
s) then String
"z" else String
s -- TODO: only do this when var is free

instance ToAbstract Literal Expr where
  toAbstract :: Literal -> m Expr
toAbstract Literal
l = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> Expr
A.Lit Literal
l)

instance ToAbstract Term Expr where
  toAbstract :: Term -> m Expr
toAbstract Term
t = case Term
t of
    R.Var Int
i Elims
es -> do
      Maybe Name
mname <- Int -> m (Maybe Name)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Maybe Name)
askName Int
i
      case Maybe Name
mname of
        Maybe Name
Nothing -> do
          Telescope
cxt   <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          [Name]
names <- ([Name] -> [Name]) -> m [Name]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (([Name] -> [Name]) -> m [Name]) -> ([Name] -> [Name]) -> m [Name]
forall a b. (a -> b) -> a -> b
$ Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
cxt) ([Name] -> [Name]) -> ([Name] -> [Name]) -> [Name] -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Name]
forall a. [a] -> [a]
reverse
          Bool -> m Expr -> m Expr
forall (m :: * -> *) a. ReadTCState m => Bool -> m a -> m a
withShowAllArguments' Bool
False (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ TypeError -> m Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m Expr) -> TypeError -> m Expr
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> [Name] -> TypeError
DeBruijnIndexOutOfScope Int
i Telescope
cxt [Name]
names
        Just Name
name -> (Expr, Elims) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (Name -> Expr
A.Var Name
name, Elims
es)
    R.Con QName
c Elims
es -> (Expr, Elims) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
c), Elims
es)
    R.Def QName
f Elims
es -> do
      Expr
af <- QName -> m Expr
forall (m :: * -> *). HasConstInfo m => QName -> m Expr
mkDef (KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
f)
      (Expr, Elims) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (Expr
af, Elims
es)
    R.Lam Hiding
h Abs Term
t  -> do
      (Expr
e, Name
name) <- Abs Term -> m (Expr, Name)
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Abs Term
t
      let info :: ArgInfo
info  = Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected ArgInfo
defaultArgInfo
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
name) Expr
e
    R.ExtLam [Clause]
cs Elims
es -> do
      Name
name <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
extendedLambdaName
      ModuleName
m    <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
      let qname :: QName
qname   = ModuleName -> Name -> QName
qualify ModuleName
m Name
name
          cname :: Name
cname   = Name -> Name
nameConcrete Name
name
          defInfo :: DefInfo' t
defInfo = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cname Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef Range
forall a. Range' a
noRange
      [Clause]
cs <- [QNamed Clause] -> m [Clause]
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract ([QNamed Clause] -> m [Clause]) -> [QNamed Clause] -> m [Clause]
forall a b. (a -> b) -> a -> b
$ (Clause -> QNamed Clause) -> [Clause] -> [QNamed Clause]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
qname) [Clause]
cs
      (Expr, Elims) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (ExprInfo -> DefInfo -> QName -> [Clause] -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo
forall t. DefInfo' t
defInfo QName
qname [Clause]
cs, Elims
es)
    R.Pi Dom Term
a Abs Term
b   -> do
      (Expr
b, Name
name) <- Abs Term -> m (Expr, Name)
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Abs Term
b
      TypedBinding
a         <- (Dom Term, Name) -> m TypedBinding
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (Dom Term
a, Name
name)
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope -> Expr -> Expr
A.Pi ExprInfo
exprNoRange [TypedBinding
a] Expr
b
    R.Sort Sort
s   -> Sort -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Sort
s
    R.Lit Literal
l    -> Literal -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Literal
l
    R.Meta MetaId
x Elims
es    -> (Expr, Elims) -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract (MetaInfo -> Expr
A.Underscore MetaInfo
info, Elims
es)
      where info :: MetaInfo
info = MetaInfo
emptyMetaInfo{ metaNumber :: Maybe MetaId
metaNumber = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x }
    Term
R.Unknown      -> Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo

mkDef :: HasConstInfo m => QName -> m A.Expr
mkDef :: QName -> m Expr
mkDef QName
f =
  m Bool -> m Expr -> m Expr -> m Expr
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> m Definition -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f)
      (Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Macro QName
f)
      (Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
f)

mkSet :: Expr -> Expr
mkSet :: Expr -> Expr
mkSet Expr
e = AppInfo -> Expr -> NamedArg Expr -> Expr
App (Origin -> AppInfo -> AppInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected AppInfo
defaultAppInfo_) (ExprInfo -> Integer -> Expr
A.Set ExprInfo
exprNoRange Integer
0) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e

instance ToAbstract Sort Expr where
  toAbstract :: Sort -> m Expr
toAbstract (SetS Term
x) = Expr -> Expr
mkSet (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Term
x
  toAbstract (LitS Integer
x) = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Integer -> Expr
A.Set ExprInfo
exprNoRange Integer
x
  toAbstract Sort
UnknownS = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
mkSet (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo

instance ToAbstract R.Pattern (Names, A.Pattern) where
  toAbstract :: Pattern -> m ([Name], Pattern)
toAbstract Pattern
pat = case Pattern
pat of
    R.ConP QName
c [Arg Pattern]
args -> do
      ([Name]
names, [NamedArg Pattern]
args) <- [Arg Pattern] -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m ([Name], [NamedArg Pattern])
toAbstractPats [Arg Pattern]
args
      ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
names, ConPatInfo -> AmbiguousQName -> [NamedArg Pattern] -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConOrigin
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
c) [NamedArg Pattern]
args)
    Pattern
R.DotP    -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange)
    R.VarP String
s | String -> Bool
forall a. IsNoName a => a -> Bool
isNoName String
s -> String -> (Name -> m ([Name], Pattern)) -> m ([Name], Pattern)
forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> (Name -> m a) -> m a
withName String
"z" ((Name -> m ([Name], Pattern)) -> m ([Name], Pattern))
-> (Name -> m ([Name], Pattern)) -> m ([Name], Pattern)
forall a b. (a -> b) -> a -> b
$ \ Name
name -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
name], BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
name)
        -- Ulf, 2016-08-09: Also bind noNames (#2129). This to make the
        -- behaviour consistent with lambda and pi.
        -- return ([], A.WildP patNoRange)
    R.VarP String
s  -> String -> (Name -> m ([Name], Pattern)) -> m ([Name], Pattern)
forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> (Name -> m a) -> m a
withName String
s ((Name -> m ([Name], Pattern)) -> m ([Name], Pattern))
-> (Name -> m ([Name], Pattern)) -> m ([Name], Pattern)
forall a b. (a -> b) -> a -> b
$ \ Name
name -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
name], BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
name)
    R.LitP Literal
l  -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Literal -> Pattern
forall e. Literal -> Pattern' e
A.LitP Literal
l)
    Pattern
R.AbsurdP -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange)
    R.ProjP QName
d -> ([Name], Pattern) -> m ([Name], Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
ProjSystem (AmbiguousQName -> Pattern) -> AmbiguousQName -> Pattern
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
d)

toAbstractPats :: MonadReflectedToAbstract m => [Arg R.Pattern] -> m (Names, [NamedArg A.Pattern])
toAbstractPats :: [Arg Pattern] -> m ([Name], [NamedArg Pattern])
toAbstractPats [Arg Pattern]
pats = case [Arg Pattern]
pats of
    []   -> ([Name], [NamedArg Pattern]) -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    Arg Pattern
p:[Arg Pattern]
ps -> do
      ([Name]
names,  NamedArg Pattern
p)  <- (Arg ([Name], Named NamedName Pattern) -> ([Name], NamedArg Pattern)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
distributeF (Arg ([Name], Named NamedName Pattern)
 -> ([Name], NamedArg Pattern))
-> (Arg (Named NamedName ([Name], Pattern))
    -> Arg ([Name], Named NamedName Pattern))
-> Arg (Named NamedName ([Name], Pattern))
-> ([Name], NamedArg Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName ([Name], Pattern)
 -> ([Name], Named NamedName Pattern))
-> Arg (Named NamedName ([Name], Pattern))
-> Arg ([Name], Named NamedName Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName ([Name], Pattern)
-> ([Name], Named NamedName Pattern)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
distributeF) (Arg (Named NamedName ([Name], Pattern))
 -> ([Name], NamedArg Pattern))
-> m (Arg (Named NamedName ([Name], Pattern)))
-> m ([Name], NamedArg Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Pattern -> m (Arg (Named NamedName ([Name], Pattern)))
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Arg Pattern
p
      ([Name]
namess, [NamedArg Pattern]
ps) <- ([Name] -> [Name])
-> m ([Name], [NamedArg Pattern]) -> m ([Name], [NamedArg Pattern])
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ([Name]
names[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++) (m ([Name], [NamedArg Pattern]) -> m ([Name], [NamedArg Pattern]))
-> m ([Name], [NamedArg Pattern]) -> m ([Name], [NamedArg Pattern])
forall a b. (a -> b) -> a -> b
$ [Arg Pattern] -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m ([Name], [NamedArg Pattern])
toAbstractPats [Arg Pattern]
ps
      ([Name], [NamedArg Pattern]) -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
namess[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++[Name]
names, NamedArg Pattern
pNamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:[NamedArg Pattern]
ps)

instance ToAbstract (QNamed R.Clause) A.Clause where
  toAbstract :: QNamed Clause -> m Clause
toAbstract (QNamed QName
name (R.Clause [Arg Pattern]
pats Term
rhs)) = do
    ([Name]
names, [NamedArg Pattern]
pats) <- [Arg Pattern] -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m ([Name], [NamedArg Pattern])
toAbstractPats [Arg Pattern]
pats
    Expr
rhs           <- ([Name] -> [Name]) -> m Expr -> m Expr
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ([Name]
names[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Term -> m Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract Term
rhs
    let lhs :: LHS
lhs = SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
name [NamedArg Pattern]
pats
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> m Clause) -> Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] (Expr -> Maybe Expr -> RHS
RHS Expr
rhs Maybe Expr
forall a. Maybe a
Nothing) WhereDeclarations
noWhereDecls Bool
False
  toAbstract (QNamed QName
name (R.AbsurdClause [Arg Pattern]
pats)) = do
    ([Name]
_, [NamedArg Pattern]
pats) <- [Arg Pattern] -> m ([Name], [NamedArg Pattern])
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m ([Name], [NamedArg Pattern])
toAbstractPats [Arg Pattern]
pats
    let lhs :: LHS
lhs = SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
name [NamedArg Pattern]
pats
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> m Clause) -> Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] RHS
AbsurdRHS WhereDeclarations
noWhereDecls Bool
False

instance ToAbstract [QNamed R.Clause] [A.Clause] where
  toAbstract :: [QNamed Clause] -> m [Clause]
toAbstract = (QNamed Clause -> m Clause) -> [QNamed Clause] -> m [Clause]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QNamed Clause -> m Clause
forall r a (m :: * -> *).
(ToAbstract r a, MonadReflectedToAbstract m) =>
r -> m a
toAbstract