{-# 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
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
  [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] -> 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
  ([(Name, Type)] -> [(Name, Type)]) -> m a -> m a
forall a. ([(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 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
  [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)
forall (m :: * -> *).
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)
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
    Expr
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!
    TypedBinding -> m TypedBinding
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypedBinding -> m TypedBinding) -> TypedBinding -> m TypedBinding
forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
A.TBind Range
forall a. Range' a
noRange
      (TacticAttribute -> Bool -> TypedBindingInfo
A.TypedBindingInfo TacticAttribute
forall a. Null a => a
empty Bool
isfin)
      (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
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     <- 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
    Bool
showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
    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
$ if Bool
showImp Bool -> Bool -> Bool
|| Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ Expr)
arg
             then AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (Origin -> AppInfo -> AppInfo
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) = (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
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elims) -> m (AbsOfRef (Expr, Elims))
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)
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
      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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elims) -> m (AbsOfRef (Expr, Elims))
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Abs Type -> m (AbsOfRef (Abs Type))
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 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 -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
A.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
A.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
forall (m :: * -> *). MonadFresh NameId m => String -> 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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
NonEmpty (QNamed Clause) -> m (AbsOfRef (NonEmpty (QNamed Clause)))
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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Expr, Elims) -> m (AbsOfRef (Expr, Elims))
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Abs Type -> m (AbsOfRef (Abs Type))
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
(Dom Type, Name) -> m (AbsOfRef (Dom Type, Name))
toAbstract (Dom Type
a, Name
name)
      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 -> 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)
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
      MetaInfo
info <- m MetaInfo
forall (m :: * -> *). ReadTCState m => m MetaInfo
mkMetaInfo
      let info' :: MetaInfo
info' = MetaInfo
info{ metaNumber = Just x }
      (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 (MetaInfo -> Expr
A.Underscore MetaInfo
info', Elims
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
  ScopeInfo
scope <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  MetaInfo -> m MetaInfo
forall a. a -> m a
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 = 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
  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 a. a -> m a
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 a. ([(Name, Type)] -> [(Name, Type)]) -> m a -> m a
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract Type
t  -- go into the right context for translating the type
  Pattern -> m Pattern
forall a. a -> m a
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 = A.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
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
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
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
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
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
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)
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
      NAPs Expr
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
      Pattern -> m Pattern
forall a. a -> m a
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)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
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
A.mkBindName Name
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
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 -> 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
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 (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
    NAPs Expr
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
    Expr
rhs  <- 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
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
A.SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    Clause -> m Clause
forall a. a -> m a
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
A.RHS Expr
rhs Maybe Expr
forall a. Maybe a
Nothing) WhereDeclarations
A.noWhereDecls Bool
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
    NAPs Expr
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 :: 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
A.SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    Clause -> m Clause
forall a. a -> m a
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
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 = (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
$ ([Text] -> (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall a c. Sized a => a -> c -> c -> c
singPlural [Text]
xs Doc -> Doc
forall a. a -> a
id (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"s") Doc
"Missing bindings for telescope 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 -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$
                             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