{-# 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.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 = 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 <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
  [Name]
ctx  <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
  UnicodeOrAscii
glyphMode <- PragmaOptions -> UnicodeOrAscii
optUseUnicode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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' = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall {t :: * -> *}. Foldable t => t Name -> Name -> Bool
notTaken [Name]
ctx) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> a -> [a]
iterate (FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode) Name
name
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Name
name,Type
t)forall a. a -> [a] -> [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 = forall a. IsNoName a => a -> Bool
isNoName Name
x Bool -> Bool -> Bool
|| Name -> Name
nameConcrete Name
x 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 = forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
[(String, Type)] -> ([Name] -> m a) -> m a
withVars forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [String]
ss forall a b. (a -> b) -> a -> b
$ 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) -> forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> Type -> (Name -> m a) -> m a
withVar String
s Type
t forall a b. (a -> b) -> a -> b
$ \Name
n -> forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
[(String, Type)] -> ([Name] -> m a) -> m a
withVars [(String, Type)]
ss forall a b. (a -> b) -> a -> b
$ \[Name]
ns -> [Name] -> m a
f (Name
nforall 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 = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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_ = forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 <- forall a. KillRange a => KillRangeT a
killRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  let ctx :: [(Name, Type)]
ctx = forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat Type
R.Unknown
  forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (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) = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (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
    Expr
dom <- forall r (m :: * -> *).
(ToAbstract r, 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!
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
A.TBind forall a. Range' a
noRange
      (TacticAttr -> Bool -> TypedBindingInfo
A.TypedBindingInfo forall a. Maybe a
Nothing Bool
isfin)
      (forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
i forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
name)
      Expr
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 (Named_ Expr)
arg     <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Arg Type
arg
    Bool
showImp <- forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
showImp Bool -> Bool -> Bool
|| forall a. LensHiding a => a -> Bool
visible Arg (Named_ Expr)
arg
             then AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected AppInfo
defaultAppInfo_) Expr
f Arg (Named_ Expr)
arg
             else Expr
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) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. ((a, b) -> c) -> a -> b -> c
curry 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) = forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> (Name -> m a) -> m a
withName String
s' forall a b. (a -> b) -> a -> b
$ \Name
name -> (,Name
name) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract r
x
    where s' :: String
s' = if (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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit 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
name <- forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
mkVarName Int
i
      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 -> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange QName
c), Elims
es)
    R.Def QName
f Elims
es -> do
      Expr
af <- forall (m :: * -> *). HasConstInfo m => QName -> m Expr
mkDef (forall a. KillRange a => KillRangeT a
killRange QName
f)
      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) <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Abs Type
t
      let info :: ArgInfo
info  = forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h forall a b. (a -> b) -> a -> b
$ forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected ArgInfo
defaultArgInfo
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
A.mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
name) Expr
e
    R.ExtLam List1 Clause
cs Elims
es -> do
      Name
name <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
extendedLambdaName
      ModuleName
m    <- 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 = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cname Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef forall a. Range' a
noRange
      List1 Clause
cs <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. QName -> a -> QNamed a
QNamed QName
qname) List1 Clause
cs
      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) <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Abs Type
b
      TypedBinding
a         <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (Dom Type
a, Name
name)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
exprNoRange (forall el coll. Singleton el coll => el -> coll
singleton TypedBinding
a) Expr
b
    R.Sort Sort
s   -> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Sort
s
    R.Lit Literal
l    -> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Literal
l
    R.Meta MetaId
x Elims
es    -> do
      MetaInfo
info <- forall (m :: * -> *). ReadTCState m => m MetaInfo
mkMetaInfo
      let info' :: MetaInfo
info' = MetaInfo
info{ metaNumber :: Maybe MetaId
metaNumber = forall a. a -> Maybe a
Just MetaId
x }
      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
A.Underscore forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m MetaInfo
mkMetaInfo

mkMetaInfo :: ReadTCState m => m MetaInfo
mkMetaInfo :: forall (m :: * -> *). ReadTCState m => m MetaInfo
mkMetaInfo = do
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case

  Constructor{}
    -> AmbiguousQName -> Expr
A.Con 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 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 (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected AppInfo
defaultAppInfo_) Expr
e1 forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM (forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Maybe (Name, Type))
askVar Int
i) forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
  Telescope
cxt   <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  [Name]
names <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (forall a. Sized a => a -> Int
size Telescope
cxt) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
  forall (m :: * -> *) a. ReadTCState m => Bool -> m a -> m a
withShowAllArguments' Bool
False forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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 = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
annotatePattern Int
i Type
t Pattern
p = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a. Int -> [a] -> [a]
drop forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ do
  Expr
t <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
t  -- go into the right context for translating the type
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
patNoRange Expr
t Pattern
p

instance ToAbstract Sort where
  type AbsOfRef Sort = A.Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Sort -> m (AbsOfRef Sort)
toAbstract Sort
s = do
    QName
setName <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinSet
    QName
propName <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinProp
    QName
infName <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
x
      LitS Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
setName 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
x
      PropLitS Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
propName forall a b. (a -> b) -> a -> b
$ Integer -> Suffix
A.Suffix Integer
x
      InfS Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
infName 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Expr
A.Underscore forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract [Arg Pattern]
args
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConOrigin
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange QName
c) NAPs Expr
args
    R.DotP Type
t -> forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
t
    R.VarP Int
i -> do
      (Name
x, Type
t) <- forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Name, Type)
mkVar Int
i
      forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> Type -> Pattern -> m Pattern
annotatePattern Int
i Type
t forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName Name
x
    R.LitP Literal
l  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
patNoRange Literal
l
    R.AbsurdP Int
i -> do
      (Name
_, Type
t) <- forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Name, Type)
mkVar Int
i
      forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> Type -> Pattern -> m Pattern
annotatePattern Int
i Type
t forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
    R.ProjP QName
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous forall a b. (a -> b) -> a -> b
$ 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)) = forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
[(String, Type)] -> ([Name] -> m a) -> m a
withVars (forall a b. (a -> b) -> [a] -> [b]
map (Text -> String
Text.unpack forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall e. Arg e -> e
unArg) [(Text, Arg Type)]
tel) forall a b. (a -> b) -> a -> b
$ \[Name]
_ -> do
    forall (m :: * -> *).
MonadReflectedToAbstract m =>
[(Text, Arg Type)] -> [Arg Pattern] -> m ()
checkClauseTelescopeBindings [(Text, Arg Type)]
tel [Arg Pattern]
pats
    NAPs Expr
pats <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract [Arg Pattern]
pats
    Expr
rhs  <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
rhs
    let lhs :: LHS
lhs = forall a b. LHSToSpine a b => b -> a
spineToLhs forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> NAPs Expr -> SpineLHS
A.SpineLHS forall a. Null a => a
empty QName
name NAPs Expr
pats
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] (Expr -> Maybe Expr -> RHS
A.RHS Expr
rhs forall a. Maybe a
Nothing) WhereDeclarations
A.noWhereDecls Bool
False
  toAbstract (QNamed QName
name (R.AbsurdClause [(Text, Arg Type)]
tel [Arg Pattern]
pats)) = forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
[(String, Type)] -> ([Name] -> m a) -> m a
withVars (forall a b. (a -> b) -> [a] -> [b]
map (Text -> String
Text.unpack forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall e. Arg e -> e
unArg) [(Text, Arg Type)]
tel) forall a b. (a -> b) -> a -> b
$ \[Name]
_ -> do
    forall (m :: * -> *).
MonadReflectedToAbstract m =>
[(Text, Arg Type)] -> [Arg Pattern] -> m ()
checkClauseTelescopeBindings [(Text, Arg Type)]
tel [Arg Pattern]
pats
    NAPs Expr
pats <- forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract [Arg Pattern]
pats
    let lhs :: LHS
lhs = forall a b. LHSToSpine a b => b -> a
spineToLhs forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> NAPs Expr -> SpineLHS
A.SpineLHS forall a. Null a => a
empty QName
name NAPs Expr
pats
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] RHS
A.AbsurdRHS WhereDeclarations
A.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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 forall a. [a] -> [a]
reverse [ Text
x | ((Text
x, Arg Type
_), Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. [a] -> [a]
reverse [(Text, Arg Type)]
tel) [Int
0..], Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Bool
Set.member Int
i Set Int
bs ] of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Text]
xs -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall a b. (a -> b) -> a -> b
$ (Doc
"Missing bindings for telescope variable" forall a. Semigroup a => a -> a -> a
<> Doc
s) Doc -> Doc -> Doc
<?>
                              (forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack) [Text]
xs) 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 | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
xs forall a. Eq a => a -> a -> Bool
== Int
1 = 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 = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Set Int
bound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg)
    bound :: Pattern -> Set Int
bound (R.VarP Int
i)    = 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{}      = forall a. Set a
Set.empty
    bound R.LitP{}      = forall a. Set a
Set.empty
    bound (R.AbsurdP Int
i) = forall a. a -> Set a
Set.singleton Int
i
    bound R.ProjP{}     = forall a. Set a
Set.empty