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

module Agda.Syntax.Translation.ReflectedToAbstract where

import Control.Arrow ( (***) )
import Control.Monad.Except
import Control.Monad.Reader

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

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

import Agda.Interaction.Options (optUseUnicode, UnicodeOrAscii(..))
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.Syntax.Scope.Monad (getCurrentModule)

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

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

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

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

withVar :: MonadReflectedToAbstract m => String -> R.Type -> (Name -> m a) -> m a
withVar :: forall (m :: * -> *) a.
MonadReflectedToAbstract m =>
String -> Type -> (Name -> m a) -> m a
withVar String
s Type
t Name -> m a
f = do
  Name
name <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
  [Name]
ctx  <- ([(Name, Type)] -> [Name]) -> m [Name]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (([(Name, Type)] -> [Name]) -> m [Name])
-> ([(Name, Type)] -> [Name]) -> m [Name]
forall a b. (a -> b) -> a -> b
$ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (((Name, Type) -> Name) -> [(Name, Type)] -> [Name])
-> ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete (Name -> Name) -> ((Name, Type) -> Name) -> (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst
  UnicodeOrAscii
glyphMode <- PragmaOptions -> UnicodeOrAscii
optUseUnicode (PragmaOptions -> UnicodeOrAscii)
-> m PragmaOptions -> m UnicodeOrAscii
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
M.pragmaOptions
  let freshNameMode :: FreshNameMode
freshNameMode = case UnicodeOrAscii
glyphMode of
        UnicodeOrAscii
UnicodeOk -> FreshNameMode
A.UnicodeSubscript
        UnicodeOrAscii
AsciiOnly -> FreshNameMode
A.AsciiCounter
  let name' :: Name
name' = [Name] -> Name
forall a. [a] -> a
head ([Name] -> Name) -> [Name] -> Name
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Name] -> Name -> Bool
forall {t :: * -> *}. Foldable t => t Name -> Name -> Bool
notTaken [Name]
ctx) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> Name -> [Name]
forall a. (a -> a) -> a -> [a]
iterate (FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode) Name
name
  ([(Name, Type)] -> [(Name, Type)]) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Name
name,Type
t)(Name, Type) -> [(Name, Type)] -> [(Name, Type)]
forall a. a -> [a] -> [a]
:) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Name -> m a
f Name
name'
  where
    notTaken :: t Name -> Name -> Bool
notTaken t Name
xs Name
x = Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x Bool -> Bool -> Bool
|| Name -> Name
nameConcrete Name
x Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
xs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance ToAbstract Literal where
  type AbsOfRef Literal = Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Literal -> m (AbsOfRef Literal)
toAbstract Literal
l = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty Literal
l

instance ToAbstract Term where
  type AbsOfRef Term = Expr
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Type -> m (AbsOfRef Type)
toAbstract = \case
    R.Var Int
i Elims
es -> do
      Name
name <- Int -> m Name
forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
mkVarName Int
i
      (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (Name -> Expr
A.Var Name
name, Elims
es)
    R.Con QName
c Elims
es -> (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
c), Elims
es)
    R.Def QName
f Elims
es -> do
      Expr
af <- QName -> m Expr
forall (m :: * -> *). HasConstInfo m => QName -> m Expr
mkDef (KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
f)
      (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (Expr
af, Elims
es)
    R.Lam Hiding
h Abs Type
t  -> do
      (Expr
e, Name
name) <- Abs Type -> m (AbsOfRef (Abs Type))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Abs Type
t
      let info :: ArgInfo
info  = Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Reflected ArgInfo
defaultArgInfo
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
name) Expr
e
    R.ExtLam List1 Clause
cs Elims
es -> do
      Name
name <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
extendedLambdaName
      ModuleName
m    <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
      let qname :: QName
qname   = ModuleName -> Name -> QName
qualify ModuleName
m Name
name
          cname :: Name
cname   = Name -> Name
nameConcrete Name
name
          defInfo :: DefInfo' Expr
defInfo = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cname Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef Range
forall a. Range' a
noRange
      List1 Clause
cs <- NonEmpty (QNamed Clause) -> m (AbsOfRef (NonEmpty (QNamed Clause)))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (NonEmpty (QNamed Clause)
 -> m (AbsOfRef (NonEmpty (QNamed Clause))))
-> NonEmpty (QNamed Clause)
-> m (AbsOfRef (NonEmpty (QNamed Clause)))
forall a b. (a -> b) -> a -> b
$ (Clause -> QNamed Clause)
-> List1 Clause -> NonEmpty (QNamed Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
qname) List1 Clause
cs
      (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract
        (ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
defInfo Erased
defaultErased QName
qname List1 Clause
cs, Elims
es)
    R.Pi Dom Type
a Abs Type
b   -> do
      (Expr
b, Name
name) <- Abs Type -> m (AbsOfRef (Abs Type))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Abs Type
b
      TypedBinding
a         <- (Dom Type, Name) -> m (AbsOfRef (Dom Type, Name))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (Dom Type
a, Name
name)
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
exprNoRange (TypedBinding -> Telescope1
forall el coll. Singleton el coll => el -> coll
singleton TypedBinding
a) Expr
b
    R.Sort Sort
s   -> Sort -> m (AbsOfRef Sort)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Sort
s
    R.Lit Literal
l    -> Literal -> m (AbsOfRef Literal)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Literal
l
    R.Meta MetaId
x Elims
es    -> (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract (MetaInfo -> Expr
A.Underscore MetaInfo
info, Elims
es)
      where info :: MetaInfo
info = MetaInfo
emptyMetaInfo{ metaNumber :: Maybe MetaId
metaNumber = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x }
    Type
R.Unknown      -> Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo

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

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


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

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

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

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

instance ToAbstract R.Pattern where
  type AbsOfRef R.Pattern = A.Pattern
  toAbstract :: forall (m :: * -> *).
MonadReflectedToAbstract m =>
Pattern -> m (AbsOfRef Pattern)
toAbstract Pattern
pat = case Pattern
pat of
    R.ConP QName
c [Arg Pattern]
args -> do
      NAPs Expr
args <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract [Arg Pattern]
args
      Pattern -> m Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConOrigin
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ KillRangeT QName
forall a. KillRange a => KillRangeT a
killRange QName
c) NAPs Expr
args
    R.DotP Type
t -> PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Pattern) -> m Expr -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
t
    R.VarP Int
i -> do
      (Name
x, Type
t) <- Int -> m (Name, Type)
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> m (Name, Type)
mkVar Int
i
      Int -> Type -> Pattern -> m Pattern
forall (m :: * -> *).
MonadReflectedToAbstract m =>
Int -> Type -> Pattern -> m Pattern
annotatePattern Int
i Type
t (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
    R.LitP Literal
l  -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
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 (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 (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)
toAbstract [Arg Pattern]
pats
    Expr
rhs  <- Type -> m (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadReflectedToAbstract m) =>
r -> m (AbsOfRef r)
toAbstract Type
rhs
    let lhs :: LHS
lhs = SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> NAPs Expr -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> m Clause) -> Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] (Expr -> Maybe Expr -> RHS
RHS Expr
rhs Maybe Expr
forall a. Maybe a
Nothing) WhereDeclarations
noWhereDecls Bool
False
  toAbstract (QNamed QName
name (R.AbsurdClause [(Text, Arg Type)]
tel [Arg Pattern]
pats)) = [(String, Type)]
-> ([Name] -> m (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 (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)
toAbstract [Arg Pattern]
pats
    let lhs :: LHS
lhs = SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> NAPs Expr -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
name NAPs Expr
pats
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> m Clause) -> Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] RHS
AbsurdRHS WhereDeclarations
noWhereDecls Bool
False

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

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

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

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