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

    module Agda.Syntax.Translation.ReflectedToAbstract where

    import Control.Arrow        ( (***) )
    import Control.Monad        ( foldM )
    import Control.Monad.Except ( MonadError )
    import Control.Monad.Reader ( MonadReader(..), asks, reader, runReaderT )

    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Text (Text)
    import qualified Data.Text as Text

    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.Interaction.Options (optUseUnicode, UnicodeOrAscii(..))
    import Agda.TypeChecking.Monad as M hiding (MetaInfo)
    import Agda.Syntax.Scope.Monad (getCurrentModule)

    import Agda.Utils.Impossible
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Utils.Pretty
    import Agda.Utils.Functor
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    type Vars = [(Name,R.Type)]

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

    -- | Adds a new unique name to the current context.
    --   NOTE: See @chooseName@ in @Agda.Syntax.Translation.AbstractToConcrete@ for similar logic.
    --   NOTE: See @freshConcreteName@ in @Agda.Syntax.Scope.Monad@ also for similar logic.
    withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a
    withName :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> (Name -> m a) -> m a
    withName String
    s = String -> Type -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    R.Unknown

    withVar :: MonadReflectedToAbstract m => String -> R.Type -> (Name -> m a) -> m a
    withVar :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    t 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, Type)] -> [Name]) -> m [Name]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (([(Name, Type)] -> [Name]) -> m [Name])
    -> ([(Name, Type)] -> [Name]) -> m [Name]
    forall a b. (a -> b) -> a -> b
    $ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Name, Type) -> Name) -> [(Name, Type)] -> [Name])
    -> ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete (Name -> Name) -> ((Name, Type) -> Name) -> (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst
      UnicodeOrAscii
    glyphMode <- PragmaOptions -> UnicodeOrAscii
    optUseUnicode (PragmaOptions -> UnicodeOrAscii)
    -> m PragmaOptions -> m UnicodeOrAscii
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    M.pragmaOptions
      let freshNameMode :: FreshNameMode
    freshNameMode = case UnicodeOrAscii
    glyphMode of
            UnicodeOrAscii
    UnicodeOk -> FreshNameMode
    A.UnicodeSubscript
            UnicodeOrAscii
    AsciiOnly -> FreshNameMode
    A.AsciiCounter
      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 (FreshNameMode -> Name -> Name
    nextName FreshNameMode
    freshNameMode) Name
    name
      ([(Name, Type)] -> [(Name, Type)]) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((Name
    name,Type
    t)(Name, Type) -> [(Name, Type)] -> [(Name, Type)]
    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

    withNames :: MonadReflectedToAbstract m => [String] -> ([Name] -> m a) -> m a
    withNames :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [String] -> ([Name] -> m a) -> m a
    withNames [String]
    ss = [(String, Type)] -> ([Name] -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars ([(String, Type)] -> ([Name] -> m a) -> m a)
    -> [(String, Type)] -> ([Name] -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> [Type] -> [(String, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    ss ([Type] -> [(String, Type)]) -> [Type] -> [(String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Type]
    forall a. a -> [a]
    repeat Type
    R.Unknown

    withVars :: MonadReflectedToAbstract m => [(String, R.Type)] -> ([Name] -> m a) -> m a
    withVars :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars [(String, Type)]
    ss [Name] -> m a
    f = case [(String, Type)]
    ss of
      []     -> [Name] -> m a
    f []
      ((String
    s,Type
    t):[(String, Type)]
    ss) -> String -> Type -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    t ((Name -> m a) -> m a) -> (Name -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \Name
    n -> [(String, Type)] -> ([Name] -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars [(String, Type)]
    ss (([Name] -> m a) -> m a) -> ([Name] -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    ns -> [Name] -> m a
    f (Name
    nName -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :[Name]
    ns)

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

    askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
    askName :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe Name)
    askName Int
    i = ((Name, Type) -> Name) -> Maybe (Name, Type) -> Maybe Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst (Maybe (Name, Type) -> Maybe Name)
    -> m (Maybe (Name, Type)) -> m (Maybe Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Maybe (Name, Type))
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe (Name, Type))
    askVar Int
    i

    class ToAbstract r where
      type AbsOfRef r
      toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r)

      default toAbstract
        :: (Traversable t, ToAbstract s, t s ~ r, t (AbsOfRef s) ~ (AbsOfRef r))
        => MonadReflectedToAbstract m => r -> m (AbsOfRef r)
      toAbstract = (s -> m (AbsOfRef s)) -> t s -> m (t (AbsOfRef s))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse s -> m (AbsOfRef s)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract

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

    -- | Drop implicit arguments unless --show-implicit is on.
    toAbstractWithoutImplicit ::
      (ToAbstract r
      , MonadFresh NameId m
      , MonadError TCErr m
      , MonadTCEnv m
      , ReadTCState m
      , HasOptions m
      , HasBuiltins m
      , HasConstInfo m
      ) => r -> m (AbsOfRef r)
    toAbstractWithoutImplicit :: forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit r
    x = do
      [Name]
    xs <- [Name] -> [Name]
    forall a. KillRange a => KillRangeT a
    killRange ([Name] -> [Name]) -> m [Name] -> m [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [Name]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
    getContextNames
      let ctx :: [(Name, Type)]
    ctx = [Name] -> [Type] -> [(Name, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    xs ([Type] -> [(Name, Type)]) -> [Type] -> [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Type]
    forall a. a -> [a]
    repeat Type
    R.Unknown
      ReaderT [(Name, Type)] m (AbsOfRef r)
    -> [(Name, Type)] -> m (AbsOfRef r)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (r -> ReaderT [(Name, Type)] m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract r
    x) [(Name, Type)]
    ctx

    instance ToAbstract r => ToAbstract (Named name r) where
      type AbsOfRef (Named name r) = Named name (AbsOfRef r)

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

    instance ToAbstract r => ToAbstract [Arg r] where
      type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]

    -- instance ToAbstract r Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where
    instance (ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) where
      type AbsOfRef (Dom r, Name) = A.TypedBinding
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Dom r, Name) -> m (AbsOfRef (Dom r, Name))
    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 (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    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 -> List1 (NamedArg Binder) -> Expr -> TypedBinding
    mkTBind Range
    forall a. Range' a
    noRange (NamedArg Binder -> List1 (NamedArg Binder)
    forall el coll. Singleton el coll => el -> coll
    singleton (NamedArg Binder -> List1 (NamedArg Binder))
    -> NamedArg Binder -> List1 (NamedArg Binder)
    forall a b. (a -> b) -> a -> b
    $ 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) where
      type AbsOfRef (Expr, Elim) = Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elim) -> m (AbsOfRef (Expr, Elim))
    toAbstract (Expr
    f, Apply Arg Type
    arg) = do
        NamedArg Expr
    arg     <- Arg Type -> m (AbsOfRef (Arg Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Arg Type
    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) where
      type AbsOfRef (Expr, Elims) = Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    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 (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract) Expr
    f Elims
    elims

    instance ToAbstract r => ToAbstract (R.Abs r) where
      type AbsOfRef (R.Abs r) = (AbsOfRef r, Name)
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Abs r -> m (AbsOfRef (Abs r))
    toAbstract (Abs String
    s r
    x) = String -> (Name -> m (AbsOfRef r, Name)) -> m (AbsOfRef r, Name)
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> (Name -> m a) -> m a
    withName String
    s' ((Name -> m (AbsOfRef r, Name)) -> m (AbsOfRef r, Name))
    -> (Name -> m (AbsOfRef r, Name)) -> m (AbsOfRef r, Name)
    forall a b. (a -> b) -> a -> b
    $ \Name
    name -> (,) (AbsOfRef r -> Name -> (AbsOfRef r, Name))
    -> m (AbsOfRef r) -> m (Name -> (AbsOfRef r, Name))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> r -> m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract r
    x m (Name -> (AbsOfRef r, Name)) -> m Name -> m (AbsOfRef r, 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 where
      type AbsOfRef Literal = Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Literal -> m (AbsOfRef Literal)
    toAbstract Literal
    l = 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 -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty Literal
    l

    instance ToAbstract Term where
      type AbsOfRef Term = Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Type -> m (AbsOfRef Type)
    toAbstract = \case
        R.Var Int
    i Elims
    es -> do
          Name
    name <- Int -> m Name
    forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
    mkVarName Int
    i
          (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract (Name -> Expr
    A.Var Name
    name, Elims
    es)
        R.Con QName
    c Elims
    es -> (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    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 (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract (Expr
    af, Elims
    es)
        R.Lam Hiding
    h Abs Type
    t  -> do
          (Expr
    e, Name
    name) <- Abs Type -> m (AbsOfRef (Abs Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Abs Type
    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 List1 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' Expr
    defInfo = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo Name
    cname Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ConcreteDef Range
    forall a. Range' a
    noRange
          List1 Clause
    cs <- NonEmpty (QNamed Clause) -> m (AbsOfRef (NonEmpty (QNamed Clause)))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract (NonEmpty (QNamed Clause)
     -> m (AbsOfRef (NonEmpty (QNamed Clause))))
    -> NonEmpty (QNamed Clause)
    -> m (AbsOfRef (NonEmpty (QNamed Clause)))
    forall a b. (a -> b) -> a -> b
    $ (Clause -> QNamed Clause)
    -> List1 Clause -> NonEmpty (QNamed Clause)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    qname) List1 Clause
    cs
          (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract
            (ExprInfo
    -> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
    A.ExtendedLam ExprInfo
    exprNoRange DefInfo' Expr
    defInfo Erased
    defaultErased QName
    qname List1 Clause
    cs, Elims
    es)
        R.Pi Dom Type
    a Abs Type
    b   -> do
          (Expr
    b, Name
    name) <- Abs Type -> m (AbsOfRef (Abs Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Abs Type
    b
          TypedBinding
    a         <- (Dom Type, Name) -> m (AbsOfRef (Dom Type, Name))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract (Dom Type
    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 -> Telescope1 -> Expr -> Expr
    A.Pi ExprInfo
    exprNoRange (TypedBinding -> Telescope1
    forall el coll. Singleton el coll => el -> coll
    singleton TypedBinding
    a) Expr
    b
        R.Sort Sort
    s   -> Sort -> m (AbsOfRef Sort)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Sort
    s
        R.Lit Literal
    l    -> Literal -> m (AbsOfRef Literal)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Literal
    l
        R.Meta MetaId
    x Elims
    es    -> do
          MetaInfo
    info <- m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo
          let info' :: MetaInfo
    info' = MetaInfo
    info{ metaNumber :: Maybe MetaId
    metaNumber = MetaId -> Maybe MetaId
    forall a. a -> Maybe a
    Just MetaId
    x }
          (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract (MetaInfo -> Expr
    A.Underscore MetaInfo
    info', Elims
    es)
        Type
    R.Unknown      -> MetaInfo -> Expr
    Underscore (MetaInfo -> Expr) -> m MetaInfo -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo

    mkMetaInfo :: ReadTCState m => m MetaInfo
    mkMetaInfo :: forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo = do
      ScopeInfo
    scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      MetaInfo -> m MetaInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaInfo -> m MetaInfo) -> MetaInfo -> m MetaInfo
    forall a b. (a -> b) -> a -> b
    $ MetaInfo
    emptyMetaInfo { metaScope :: ScopeInfo
    metaScope = ScopeInfo
    scope }

    mkDef :: HasConstInfo m => QName -> m A.Expr
    mkDef :: forall (m :: * -> *). HasConstInfo m => 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)

    mkApp :: Expr -> Expr -> Expr
    mkApp :: Expr -> Expr -> Expr
    mkApp Expr
    e1 Expr
    e2 = AppInfo -> Expr -> NamedArg Expr -> Expr
    App (Origin -> AppInfo -> AppInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Reflected AppInfo
    defaultAppInfo_) Expr
    e1 (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    e2

    mkVar :: MonadReflectedToAbstract m => Int -> m (Name, R.Type)
    mkVar :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i = m (Maybe (Name, Type))
    -> ((Name, Type) -> m (Name, Type))
    -> m (Name, Type)
    -> m (Name, Type)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> (a -> m b) -> m b -> m b
    ifJustM (Int -> m (Maybe (Name, Type))
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe (Name, Type))
    askVar Int
    i) (Name, Type) -> m (Name, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (m (Name, Type) -> m (Name, Type))
    -> m (Name, Type) -> m (Name, Type)
    forall a b. (a -> b) -> a -> b
    $ do
      Telescope
    cxt   <- m Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      [Name]
    names <- ([(Name, Type)] -> [Name]) -> m [Name]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (([(Name, Type)] -> [Name]) -> m [Name])
    -> ([(Name, Type)] -> [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, Type)] -> [Name]) -> [(Name, Type)] -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> [Name]
    forall a. [a] -> [a]
    reverse ([Name] -> [Name])
    -> ([(Name, Type)] -> [Name]) -> [(Name, Type)] -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst
      Bool -> m (Name, Type) -> m (Name, Type)
    forall (m :: * -> *) a. ReadTCState m => Bool -> m a -> m a
    withShowAllArguments' Bool
    False (m (Name, Type) -> m (Name, Type))
    -> m (Name, Type) -> m (Name, Type)
    forall a b. (a -> b) -> a -> b
    $ TypeError -> m (Name, Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Name, Type)) -> TypeError -> m (Name, Type)
    forall a b. (a -> b) -> a -> b
    $ Int -> Telescope -> [Name] -> TypeError
    DeBruijnIndexOutOfScope Int
    i Telescope
    cxt [Name]
    names

    mkVarName :: MonadReflectedToAbstract m => Int -> m Name
    mkVarName :: forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
    mkVarName Int
    i = (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name) -> m (Name, Type) -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Name, Type)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i

    annotatePattern :: MonadReflectedToAbstract m => Int -> R.Type -> A.Pattern -> m A.Pattern
    annotatePattern :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> Type -> Pattern -> m Pattern
    annotatePattern Int
    _ Type
    R.Unknown Pattern
    p = Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
    annotatePattern Int
    i Type
    t Pattern
    p = ([(Name, Type)] -> [(Name, Type)]) -> m Pattern -> m Pattern
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (Int -> [(Name, Type)] -> [(Name, Type)]
    forall a. Int -> [a] -> [a]
    drop (Int -> [(Name, Type)] -> [(Name, Type)])
    -> Int -> [(Name, Type)] -> [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ do
      Expr
    t <- Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Type
    t  -- go into the right context for translating the type
      Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Expr -> Pattern -> Pattern
    forall e. PatInfo -> e -> Pattern' e -> Pattern' e
    A.AnnP PatInfo
    patNoRange Expr
    t Pattern
    p

    instance ToAbstract Sort where
      type AbsOfRef Sort = Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Sort -> m (AbsOfRef Sort)
    toAbstract Sort
    s = do
        QName
    setName <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinSet
        QName
    propName <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinProp
        QName
    infName <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinSetOmega
        case Sort
    s of
          SetS Type
    x -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    setName) (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Type
    x
          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
    $ QName -> Suffix -> Expr
    A.Def' QName
    setName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          PropS Type
    x -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    propName) (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Type
    x
          PropLitS 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
    $ QName -> Suffix -> Expr
    A.Def' QName
    propName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          InfS 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
    $ QName -> Suffix -> Expr
    A.Def' QName
    infName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          Sort
    UnknownS -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    setName) (Expr -> Expr) -> (MetaInfo -> Expr) -> MetaInfo -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaInfo -> Expr
    Underscore (MetaInfo -> Expr) -> m MetaInfo -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo

    instance ToAbstract R.Pattern where
      type AbsOfRef R.Pattern = A.Pattern
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Pattern -> m (AbsOfRef Pattern)
    toAbstract Pattern
    pat = case Pattern
    pat of
        R.ConP QName
    c [Arg Pattern]
    args -> do
          NAPs Expr
    args <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract [Arg Pattern]
    args
          Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ ConPatInfo -> AmbiguousQName -> NAPs Expr -> 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) NAPs Expr
    args
        R.DotP Type
    t -> PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    patNoRange (Expr -> Pattern) -> m Expr -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Type
    t
        R.VarP Int
    i -> do
          (Name
    x, Type
    t) <- Int -> m (Name, Type)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i
          Int -> Type -> Pattern -> m Pattern
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> Type -> Pattern -> m Pattern
    annotatePattern Int
    i Type
    t (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern) -> BindName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    mkBindName Name
    x
        R.LitP Literal
    l  -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    patNoRange Literal
    l
        R.AbsurdP Int
    i -> do
          (Name
    _, Type
    t) <- Int -> m (Name, Type)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i
          Int -> Type -> Pattern -> m Pattern
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> Type -> Pattern -> m Pattern
    annotatePattern Int
    i Type
    t (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
        R.ProjP QName
    d -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ 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

    instance ToAbstract (QNamed R.Clause) where
      type AbsOfRef (QNamed R.Clause) = A.Clause

      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    toAbstract (QNamed QName
    name (R.Clause [(Text, Arg Type)]
    tel [Arg Pattern]
    pats Type
    rhs)) = [(String, Type)] -> ([Name] -> m Clause) -> m Clause
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars (((Text, Arg Type) -> (String, Type))
    -> [(Text, Arg Type)] -> [(String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> String
    Text.unpack (Text -> String)
    -> (Arg Type -> Type) -> (Text, Arg Type) -> (String, Type)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Arg Type -> Type
    forall e. Arg e -> e
    unArg) [(Text, Arg Type)]
    tel) (([Name] -> m Clause) -> m Clause)
    -> ([Name] -> m Clause) -> m Clause
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    _ -> do
        [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats
        NAPs Expr
    pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract [Arg Pattern]
    pats
        Expr
    rhs  <- Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract Type
    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 -> NAPs Expr -> SpineLHS
    SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    name NAPs Expr
    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 [(Text, Arg Type)]
    tel [Arg Pattern]
    pats)) = [(String, Type)] -> ([Name] -> m Clause) -> m Clause
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars (((Text, Arg Type) -> (String, Type))
    -> [(Text, Arg Type)] -> [(String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> String
    Text.unpack (Text -> String)
    -> (Arg Type -> Type) -> (Text, Arg Type) -> (String, Type)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Arg Type -> Type
    forall e. Arg e -> e
    unArg) [(Text, Arg Type)]
    tel) (([Name] -> m Clause) -> m Clause)
    -> ([Name] -> m Clause) -> m Clause
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    _ -> do
        [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats
        NAPs Expr
    pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract [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 -> NAPs Expr -> SpineLHS
    SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    name NAPs Expr
    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] where
      type AbsOfRef [QNamed R.Clause] = [A.Clause]
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [QNamed Clause] -> m (AbsOfRef [QNamed 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 (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract

    instance ToAbstract (List1 (QNamed R.Clause)) where
      type AbsOfRef (List1 (QNamed R.Clause)) = List1 A.Clause
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    NonEmpty (QNamed Clause) -> m (AbsOfRef (NonEmpty (QNamed Clause)))
    toAbstract = (QNamed Clause -> m Clause)
    -> NonEmpty (QNamed Clause) -> m (List1 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 (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    toAbstract

    -- | Check that all variables in the telescope are bound in the left-hand side. Since we check the
    --   telescope by attaching type annotations to the pattern variables there needs to be somewhere to
    --   put the annotation. Also, since the lhs is where the variables are actually bound, missing a
    --   binding for a variable that's used later in the telescope causes unbound variable panic
    --   (see #5044).
    checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg R.Type)] -> [Arg R.Pattern] -> m ()
    checkClauseTelescopeBindings :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats =
      case [Text] -> [Text]
    forall a. [a] -> [a]
    reverse [ Text
    x | ((Text
    x, Arg Type
    _), Int
    i) <- [(Text, Arg Type)] -> [Int] -> [((Text, Arg Type), Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ([(Text, Arg Type)] -> [(Text, Arg Type)]
    forall a. [a] -> [a]
    reverse [(Text, Arg Type)]
    tel) [Int
    0..], Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Int
    i Set Int
    bs ] of
        [] -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        [Text]
    xs -> Doc -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> m ()) -> Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Doc
    "Missing bindings for telescope variable" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    s) Doc -> Doc -> Doc
    <?>
                                  ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    ", " ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Text -> Doc) -> [Text] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Doc
    text (String -> Doc) -> (Text -> String) -> Text -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> String
    Text.unpack) [Text]
    xs) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ".") Doc -> Doc -> Doc
    $$
                                 Doc
    "All variables in the clause telescope must be bound in the left-hand side."
          where s :: Doc
    s | [Text] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Text]
    xs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = Doc
    forall a. Null a => a
    empty
                  | Bool
    otherwise      = Doc
    "s"
      where
        bs :: Set Int
    bs = [Arg Pattern] -> Set Int
    boundVars [Arg Pattern]
    pats

        boundVars :: [Arg Pattern] -> Set Int
    boundVars = [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Int] -> Set Int)
    -> ([Arg Pattern] -> [Set Int]) -> [Arg Pattern] -> Set Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Pattern -> Set Int) -> [Arg Pattern] -> [Set Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Set Int
    bound (Pattern -> Set Int)
    -> (Arg Pattern -> Pattern) -> Arg Pattern -> Set Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Pattern -> Pattern
    forall e. Arg e -> e
    unArg)
        bound :: Pattern -> Set Int
    bound (R.VarP Int
    i)    = Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    i
        bound (R.ConP QName
    _ [Arg Pattern]
    ps) = [Arg Pattern] -> Set Int
    boundVars [Arg Pattern]
    ps
        bound R.DotP{}      = Set Int
    forall a. Set a
    Set.empty
        bound R.LitP{}      = Set Int
    forall a. Set a
    Set.empty
        bound (R.AbsurdP Int
    i) = Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    i
        bound R.ProjP{}     = Set Int
    forall a. Set a
    Set.empty