{-# 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
  ( Name, QName, QNamed(QNamed)
  , isNoName, nameConcrete, nextName, qualify, unambiguous
  )
import qualified Agda.Syntax.Abstract as A
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.Syntax.Common.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 <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ String
s
  ctx  <- asks $ map $ nameConcrete . fst
  glyphMode <- optUseUnicode <$> M.pragmaOptions
  let freshNameMode = case UnicodeOrAscii
glyphMode of
        UnicodeOrAscii
UnicodeOk -> FreshNameMode
A.UnicodeSubscript
        UnicodeOrAscii
AsciiOnly -> FreshNameMode
A.AsciiCounter
  let name' = Name -> [Name] -> Name
forall a. a -> [a] -> a
headWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ ([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
  local ((name,t):) $ f 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 a. ([(Name, Type)] -> a) -> m a
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 a b. (a -> b) -> Maybe a -> Maybe b
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)
forall (f :: * -> *) a b.
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
s -> m (AbsOfRef s)
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
  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] -> [(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
  runReaderT (toAbstract x) 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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Named NamedName r -> m (AbsOfRef (Named NamedName 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 A.Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where
instance (ToAbstract r, AbsOfRef r ~ A.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, domIsFinite :: forall t e. Dom' t e -> Bool
domIsFinite = Bool
isfin, 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
    dom <- r -> m (AbsOfRef r)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
r -> m (AbsOfRef r)
toAbstract r
x
    -- TODO(Amy): Anyone know why this discards the tactic? It was like
    -- that when I got here!
    return $ A.TBind noRange
      (A.TypedBindingInfo empty isfin)
      (singleton $ unnamedArg i $ A.mkBinder_ name)
      dom

instance ToAbstract (A.Expr, Elim) where
  type AbsOfRef (A.Expr, Elim) = A.Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elim) -> m (AbsOfRef (Expr, Elim))
toAbstract (Expr
f, Apply Arg Type
arg) = do
    arg     <- Arg Type -> m (AbsOfRef (Arg Type))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Arg Type -> m (AbsOfRef (Arg Type))
toAbstract Arg Type
arg
    showImp <- showImplicitArguments
    return $ if showImp || visible arg
             then A.App (setOrigin Reflected defaultAppInfo_) f arg
             else f

instance ToAbstract (A.Expr, Elims) where
  type AbsOfRef (A.Expr, Elims) = A.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
(Expr, Elim) -> m (AbsOfRef (Expr, Elim))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elim) -> m (AbsOfRef (Expr, Elim))
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 (Abs r))) -> m (AbsOfRef (Abs r))
forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> (Name -> m a) -> m a
withName String
s' ((Name -> m (AbsOfRef (Abs r))) -> m (AbsOfRef (Abs r)))
-> (Name -> m (AbsOfRef (Abs r))) -> m (AbsOfRef (Abs r))
forall a b. (a -> b) -> a -> b
$ \Name
name -> (,Name
name) (AbsOfRef r -> (AbsOfRef r, Name))
-> m (AbsOfRef r) -> m (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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
r -> m (AbsOfRef r)
toAbstract r
x
    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 = A.Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Literal -> m (AbsOfRef Literal)
toAbstract Literal
l = Expr -> m Expr
forall a. a -> m a
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 = A.Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract = \case
    R.Var Int
i Elims
es -> do
      name <- Int -> m Name
forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
mkVarName Int
i
      toAbstract (A.Var name, es)
    R.Con QName
c Elims
es -> (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elims) -> m (AbsOfRef (Expr, Elims))
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
      af <- QName -> m Expr
forall (m :: * -> *). HasConstInfo m => QName -> m Expr
mkDef (KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
f)
      toAbstract (af, es)
    R.Lam Hiding
h Abs Type
t  -> do
      (e, name) <- Abs Type -> m (AbsOfRef (Abs Type))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Abs Type -> m (AbsOfRef (Abs Type))
toAbstract Abs Type
t
      let 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
      return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg info $ A.mkBinder_ name) e
    R.ExtLam List1 Clause
cs Elims
es -> do
      name <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ String
extendedLambdaName
      m    <- getCurrentModule
      let qname   = ModuleName -> Name -> QName
qualify ModuleName
m Name
name
          cname   = Name -> Name
nameConcrete Name
name
          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
      cs <- toAbstract $ fmap (QNamed qname) cs
      toAbstract
        (A.ExtendedLam exprNoRange defInfo defaultErased qname cs, es)
    R.Pi Dom Type
a Abs Type
b   -> do
      (b, name) <- Abs Type -> m (AbsOfRef (Abs Type))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Abs Type -> m (AbsOfRef (Abs Type))
toAbstract Abs Type
b
      a         <- toAbstract (a, name)
      return $ A.Pi exprNoRange (singleton a) b
    R.Sort Sort
s   -> Sort -> m (AbsOfRef Sort)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Sort -> m (AbsOfRef Sort)
toAbstract Sort
s
    R.Lit Literal
l    -> Literal -> m (AbsOfRef Literal)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Literal -> m (AbsOfRef Literal)
toAbstract Literal
l
    R.Meta MetaId
x Elims
es    -> do
      info <- m MetaInfo
forall (m :: * -> *). ReadTCState m => m MetaInfo
mkMetaInfo
      let info' = MetaInfo
info{ metaNumber = Just x }
      toAbstract (A.Underscore info', es)
    Type
R.Unknown      -> MetaInfo -> Expr
A.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
  scope <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  return $ emptyMetaInfo { metaScope = scope }

mkDef :: HasConstInfo m => QName -> m A.Expr
mkDef :: forall (m :: * -> *). HasConstInfo m => QName -> m Expr
mkDef QName
f = QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f m Definition -> (Definition -> Defn) -> m Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef m Defn -> (Defn -> Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case

  Constructor{}
    -> AmbiguousQName -> Expr
A.Con (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
f

  Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projProper :: Projection -> Maybe QName
projProper = Just{} } }
    -> ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjSystem (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
f

  d :: Defn
d@Function{} | Defn -> Bool
isMacro Defn
d
    -> QName -> Expr
A.Macro QName
f

  Defn
_ -> QName -> Expr
A.Def QName
f

mkApp :: A.Expr -> A.Expr -> A.Expr
mkApp :: Expr -> Expr -> Expr
mkApp Expr
e1 Expr
e2 = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (Origin -> AppInfo -> AppInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected AppInfo
defaultAppInfo_) Expr
e1 (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Arg (Named_ 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 a. a -> m a
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
  cxt   <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  names <- asks $ drop (size cxt) . reverse . map fst
  withShowAllArguments' False $ typeError $ DeBruijnIndexOutOfScope i cxt 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


instance ToAbstract Sort where
  type AbsOfRef Sort = A.Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Sort -> m (AbsOfRef Sort)
toAbstract Sort
s = do
    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
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinSet
    propName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinProp
    infName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega
    case 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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract Type
x
      LitS Integer
x -> Expr -> m Expr
forall a. a -> m a
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract Type
x
      PropLitS Integer
x -> Expr -> m Expr
forall a. a -> m a
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 a. a -> m a
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
A.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
      args <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m (AbsOfRef [Arg Pattern])
toAbstract [Arg Pattern]
args
      return $ A.ConP (ConPatInfo ConOCon patNoRange ConPatEager) (unambiguous $ killRange c) args
    R.DotP Type
t -> PatInfo -> Expr -> Pattern' Expr
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Pattern' Expr) -> m Expr -> m (Pattern' 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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract Type
t
    R.VarP Int
i -> do
      (x, _t) <- Int -> m (Name, Type)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Name, Type)
mkVar Int
i
      return $ A.VarP $ A.mkBindName x
    R.LitP Literal
l  -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
-> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern' Expr
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
patNoRange Literal
l
    R.AbsurdP Int
_i -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
-> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
    R.ProjP QName
d -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
-> AbsOfRef Pattern -> m (AbsOfRef Pattern)
forall a b. (a -> b) -> a -> b
$ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' Expr
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
ProjSystem (AmbiguousQName -> Pattern' Expr)
-> AmbiguousQName -> Pattern' Expr
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 (AbsOfRef (QNamed Clause)))
-> m (AbsOfRef (QNamed 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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 (AbsOfRef (QNamed Clause)))
 -> m (AbsOfRef (QNamed Clause)))
-> ([Name] -> m (AbsOfRef (QNamed Clause)))
-> m (AbsOfRef (QNamed 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
    pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m (AbsOfRef [Arg Pattern])
toAbstract [Arg Pattern]
pats
    rhs  <- toAbstract rhs
    let 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
A.SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    return $ A.Clause lhs [] (A.RHS rhs Nothing) A.noWhereDecls False
  toAbstract (QNamed QName
name (R.AbsurdClause [(Text, Arg Type)]
tel [Arg Pattern]
pats)) = [(String, Type)]
-> ([Name] -> m (AbsOfRef (QNamed Clause)))
-> m (AbsOfRef (QNamed 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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 (AbsOfRef (QNamed Clause)))
 -> m (AbsOfRef (QNamed Clause)))
-> ([Name] -> m (AbsOfRef (QNamed Clause)))
-> m (AbsOfRef (QNamed 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
    pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
[Arg Pattern] -> m (AbsOfRef [Arg Pattern])
toAbstract [Arg Pattern]
pats
    let 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
A.SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    return $ A.Clause lhs [] A.AbsurdRHS A.noWhereDecls 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse QNamed Clause -> m Clause
QNamed Clause -> m (AbsOfRef (QNamed Clause))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
QNamed Clause -> m (AbsOfRef (QNamed Clause))
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse QNamed Clause -> m Clause
QNamed Clause -> m (AbsOfRef (QNamed Clause))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
QNamed Clause -> m (AbsOfRef (QNamed Clause))
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 a. a -> m a
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] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (String -> [Doc]
pwords String
"Missing bindings for telescope" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ [Text] -> Doc -> Doc
forall a. Sized a => a -> Doc -> Doc
pluralS [Text]
xs Doc
"variable" ])
        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
forall a. String -> Doc a
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
"All variables in the clause telescope must be bound in the left-hand side."
      ]
  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