{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Records where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans.Maybe
import Control.Monad.Writer

import Data.Bifunctor
import qualified Data.List as List
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap

import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base (isNameInScope)

import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty as TCM
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad () --instance only
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike (eligibleForProjectionLike)

import Agda.Utils.Either
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon ConHead
h ConInfo
info Args
args = ConHead -> ConInfo -> Elims -> Term
Con ConHead
h ConInfo
info ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)

-- | Order the fields of a record construction.
orderFields
  :: forall a . HasRange a
  => QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> Writer [RecordFieldWarning] [a]           -- ^ Content arranged in official order.
orderFields :: QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = do
  -- reportSDoc "tc.record" 30 $ vcat
  --   [ "orderFields"
  --   , "  official fields: " <+> sep (map pretty xs)
  --   , "  provided fields: " <+> sep (map pretty ys)
  --   ]
  [(Name, a)]
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
alien     (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
 -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
forall w (m :: * -> *) el (p :: * -> * -> *) a a.
(MonadWriter w m, Singleton el w, Bifunctor p, HasRange a) =>
([p a Range] -> el) -> [p a a] -> m ()
warn (([(Name, Range)] -> RecordFieldWarning)
 -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)]
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> [(Name, Range)] -> RecordFieldWarning
TooManyFieldsWarning QName
r [Name]
missing
  [(Name, a)]
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
duplicate (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
 -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
forall w (m :: * -> *) el (p :: * -> * -> *) a a.
(MonadWriter w m, Singleton el w, Bifunctor p, HasRange a) =>
([p a Range] -> el) -> [p a a] -> m ()
warn (([(Name, Range)] -> RecordFieldWarning)
 -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)]
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> RecordFieldWarning
DuplicateFieldsWarning
  [a] -> Writer [RecordFieldWarning] [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> Writer [RecordFieldWarning] [a])
-> [a] -> Writer [RecordFieldWarning] [a]
forall a b. (a -> b) -> a -> b
$ [Arg Name] -> (Arg Name -> a) -> [a]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg Name]
axs ((Arg Name -> a) -> [a]) -> (Arg Name -> a) -> [a]
forall a b. (a -> b) -> a -> b
$ \ Arg Name
ax -> a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (Arg Name -> a
fill Arg Name
ax) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ Name -> [(Name, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
ax) [(Name, a)]
uniq
  where
    ([(Name, a)]
uniq, [(Name, a)]
duplicate) = ((Name, a) -> Name) -> [(Name, a)] -> ([(Name, a)], [(Name, a)])
forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
nubAndDuplicatesOn (Name, a) -> Name
forall a b. (a, b) -> a
fst [(Name, a)]
fs   -- separating duplicate fields
    xs :: [Name]
xs        = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
axs                       -- official fields (accord. record type)
    missing :: [Name]
missing   = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem (((Name, a) -> Name) -> [(Name, a)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, a) -> Name
forall a b. (a, b) -> a
fst [(Name, a)]
fs)) [Name]
xs  -- missing  fields
    alien :: [(Name, a)]
alien     = ((Name, a) -> Bool) -> [(Name, a)] -> [(Name, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Name, a) -> Bool) -> (Name, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs (Name -> Bool) -> ((Name, a) -> Name) -> (Name, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, a) -> Name
forall a b. (a, b) -> a
fst) [(Name, a)]
fs      -- spurious fields
    warn :: ([p a Range] -> el) -> [p a a] -> m ()
warn [p a Range] -> el
w    = w -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (w -> m ()) -> ([p a a] -> w) -> [p a a] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. el -> w
forall el coll. Singleton el coll => el -> coll
singleton (el -> w) -> ([p a a] -> el) -> [p a a] -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [p a Range] -> el
w ([p a Range] -> el) -> ([p a a] -> [p a Range]) -> [p a a] -> el
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p a a -> p a Range) -> [p a a] -> [p a Range]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Range) -> p a a -> p a Range
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second a -> Range
forall a. HasRange a => a -> Range
getRange)

-- | Raise generated 'RecordFieldWarning's as warnings.
warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings Writer [RecordFieldWarning] a
comp = do
  let (a
res, [RecordFieldWarning]
ws) = Writer [RecordFieldWarning] a -> (a, [RecordFieldWarning])
forall w a. Writer w a -> (a, w)
runWriter Writer [RecordFieldWarning] a
comp
  (RecordFieldWarning -> TCMT IO ())
-> [RecordFieldWarning] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> (RecordFieldWarning -> Warning)
-> RecordFieldWarning
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> Warning
RecordFieldWarning) [RecordFieldWarning]
ws
  a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- | Raise generated 'RecordFieldWarning's as errors.
failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings Writer [RecordFieldWarning] a
comp = do
  let (a
res, [RecordFieldWarning]
ws) = Writer [RecordFieldWarning] a -> (a, [RecordFieldWarning])
forall w a. Writer w a -> (a, w)
runWriter Writer [RecordFieldWarning] a
comp
  (RecordFieldWarning -> TCMT IO Any)
-> [RecordFieldWarning] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TypeError -> TCMT IO Any
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Any)
-> (RecordFieldWarning -> TypeError)
-> RecordFieldWarning
-> TCMT IO Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> TypeError
recordFieldWarningToError) [RecordFieldWarning]
ws
    -- This will raise the first warning (if any) as error.
  a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- | Order the fields of a record construction.
--   Raise generated 'RecordFieldWarning's as warnings.
orderFieldsWarn
  :: forall a . HasRange a
  => QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> TCM [a]           -- ^ Content arranged in official order.
orderFieldsWarn :: QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = Writer [RecordFieldWarning] [a] -> TCM [a]
forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
-> Writer [RecordFieldWarning] [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs

-- | Order the fields of a record construction.
--   Raise generated 'RecordFieldWarning's as errors.
orderFieldsFail
  :: forall a . HasRange a
  => QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> TCM [a]           -- ^ Content arranged in official order.
orderFieldsFail :: QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsFail QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = Writer [RecordFieldWarning] [a] -> TCM [a]
forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
-> Writer [RecordFieldWarning] [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFields
  :: forall a . HasRange a
  => QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> Writer [RecordFieldWarning] [NamedArg a]
       -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFields :: QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs = do
  -- Compute the list of given fields, decorated with the ArgInfo from the record def.
  let arg :: Name -> a -> NamedArg a
arg Name
x a
e = Maybe (Arg Name)
-> NamedArg a -> (Arg Name -> NamedArg a) -> NamedArg a
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((Arg Name -> Bool) -> [Arg Name] -> Maybe (Arg Name)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool) -> (Arg Name -> Name) -> Arg Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Name -> Name
forall e. Arg e -> e
unArg) [Arg Name]
axs) (a -> NamedArg a
forall a. a -> NamedArg a
defaultNamedArg a
e) ((Arg Name -> NamedArg a) -> NamedArg a)
-> (Arg Name -> NamedArg a) -> NamedArg a
forall a b. (a -> b) -> a -> b
$ \ Arg Name
a ->
        Arg Name -> a -> Named_ a
forall c. Arg Name -> c -> Named_ c
nameIfHidden Arg Name
a a
e Named_ a -> Arg Name -> NamedArg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Name
a
      givenFields :: [(Name, Maybe (NamedArg a))]
givenFields = [ (Name
x, NamedArg a -> Maybe (NamedArg a)
forall a. a -> Maybe a
Just (NamedArg a -> Maybe (NamedArg a))
-> NamedArg a -> Maybe (NamedArg a)
forall a b. (a -> b) -> a -> b
$ Name -> a -> NamedArg a
arg Name
x a
e) | FieldAssignment Name
x a
e <- [FieldAssignment' a]
fs ]

  -- Omitted explicit fields are filled in with placeholders.
  -- Omitted implicit or instance fields
  -- are still left out and inserted later by checkArguments_.
  [Maybe (NamedArg a)] -> [NamedArg a]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (NamedArg a)] -> [NamedArg a])
-> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
-> Writer [RecordFieldWarning] [NamedArg a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> (Arg Name -> Maybe (NamedArg a))
-> [Arg Name]
-> [(Name, Maybe (NamedArg a))]
-> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> Maybe (NamedArg a)
fill [Arg Name]
axs [(Name, Maybe (NamedArg a))]
givenFields
  where
    fill :: Arg C.Name -> Maybe (NamedArg a)
    fill :: Arg Name -> Maybe (NamedArg a)
fill Arg Name
ax
      | Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
ax = NamedArg a -> Maybe (NamedArg a)
forall a. a -> Maybe a
Just (NamedArg a -> Maybe (NamedArg a))
-> NamedArg a -> Maybe (NamedArg a)
forall a b. (a -> b) -> a -> b
$ Origin -> NamedArg a -> NamedArg a
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (NamedArg a -> NamedArg a) -> NamedArg a -> NamedArg a
forall a b. (a -> b) -> a -> b
$ a -> Named_ a
forall a name. a -> Named name a
unnamed (a -> Named_ a) -> (Name -> a) -> Name -> Named_ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> a
placeholder (Name -> Named_ a) -> Arg Name -> NamedArg a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Name
ax
      | Bool
otherwise  = Maybe (NamedArg a)
forall a. Maybe a
Nothing
    -- Andreas, 2017-04-13, issue #2494
    -- We need to put the field names as argument names for hidden arguments.
    -- Otherwise, insertImplicit does not do the right thing.
    nameIfHidden :: Arg C.Name -> c -> Named_ c
    nameIfHidden :: Arg Name -> c -> Named_ c
nameIfHidden Arg Name
ax
      | Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
ax = c -> Named_ c
forall a name. a -> Named name a
unnamed
      | Bool
otherwise  = WithOrigin (Ranged String) -> c -> Named_ c
forall name a. name -> a -> Named name a
named (WithOrigin (Ranged String) -> c -> Named_ c)
-> WithOrigin (Ranged String) -> c -> Named_ c
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged String -> WithOrigin (Ranged String)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> WithOrigin (Ranged String))
-> Ranged String -> WithOrigin (Ranged String)
forall a b. (a -> b) -> a -> b
$ Range -> String -> Ranged String
forall a. Range -> a -> Ranged a
Ranged (Arg Name -> Range
forall a. HasRange a => a -> Range
getRange Arg Name
ax) (String -> Ranged String) -> String -> Ranged String
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
ax

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFieldsWarn
  :: forall a . HasRange a
  => QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFieldsWarn :: QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs =
  Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
-> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFieldsFail
  :: forall a . HasRange a
  => QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFieldsFail :: QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs =
  Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
-> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs

-- | Get the definition for a record. Throws an exception if the name
--   does not refer to a record or the record is abstract.
getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn
getRecordDef :: QName -> m Defn
getRecordDef QName
r = m Defn -> (Defn -> m Defn) -> Maybe Defn -> m Defn
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Defn
err Defn -> m Defn
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Defn -> m Defn) -> m (Maybe Defn) -> m Defn
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
  where err :: m Defn
err = TypeError -> m Defn
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m Defn) -> TypeError -> m Defn
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
r [])

-- | Get the record name belonging to a field name.
getRecordOfField :: QName -> TCM (Maybe QName)
getRecordOfField :: QName -> TCM (Maybe QName)
getRecordOfField QName
d = TCMT IO (Maybe Projection)
-> TCM (Maybe QName)
-> (Projection -> TCM (Maybe QName))
-> TCM (Maybe QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
d) (Maybe QName -> TCM (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) ((Projection -> TCM (Maybe QName)) -> TCM (Maybe QName))
-> (Projection -> TCM (Maybe QName)) -> TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$
  \ Projection{ projProper :: Projection -> Maybe QName
projProper = Maybe QName
proper, projFromType :: Projection -> Arg QName
projFromType = Arg QName
r} ->
    Maybe QName -> TCM (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCM (Maybe QName))
-> Maybe QName -> TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
r QName -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe QName
proper -- if proper then Just (unArg r) else Nothing

-- | Get the field names of a record.
getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m)
                    => QName -> m [Dom C.Name]
getRecordFieldNames :: QName -> m [Dom Name]
getRecordFieldNames QName
r = Defn -> [Dom Name]
recordFieldNames (Defn -> [Dom Name]) -> m Defn -> m [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Defn
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r

getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m)
                     => QName -> m (Maybe [Dom C.Name])
getRecordFieldNames_ :: QName -> m (Maybe [Dom Name])
getRecordFieldNames_ QName
r = (Defn -> [Dom Name]) -> Maybe Defn -> Maybe [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Defn -> [Dom Name]
recordFieldNames (Maybe Defn -> Maybe [Dom Name])
-> m (Maybe Defn) -> m (Maybe [Dom Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r

recordFieldNames :: Defn -> [Dom C.Name]
recordFieldNames :: Defn -> [Dom Name]
recordFieldNames = (Dom' Term QName -> Dom Name) -> [Dom' Term QName] -> [Dom Name]
forall a b. (a -> b) -> [a] -> [b]
map ((QName -> Name) -> Dom' Term QName -> Dom Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Name
nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)) ([Dom' Term QName] -> [Dom Name])
-> (Defn -> [Dom' Term QName]) -> Defn -> [Dom Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields

-- | Find all records with at least the given fields.
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords :: [Name] -> TCM [QName]
findPossibleRecords [Name]
fields = do
  [Definition]
defs  <- HashMap QName Definition -> [Definition]
forall k v. HashMap k v -> [v]
HMap.elems (HashMap QName Definition -> [Definition])
-> TCMT IO (HashMap QName Definition) -> TCMT IO [Definition]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions)
  [Definition]
idefs <- HashMap QName Definition -> [Definition]
forall k v. HashMap k v -> [v]
HMap.elems (HashMap QName Definition -> [Definition])
-> TCMT IO (HashMap QName Definition) -> TCMT IO [Definition]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stImports   ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions)
  ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  [QName] -> TCM [QName]
forall (m :: * -> *) a. Monad m => a -> m a
return ([QName] -> TCM [QName]) -> [QName] -> TCM [QName]
forall a b. (a -> b) -> a -> b
$ (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> ScopeInfo -> Bool
`isNameInScope` ScopeInfo
scope) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ [Definition] -> [QName]
cands [Definition]
defs [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ [Definition] -> [QName]
cands [Definition]
idefs
  where
    cands :: [Definition] -> [QName]
cands [Definition]
defs = [ Definition -> QName
defName Definition
d | Definition
d <- [Definition]
defs, Definition -> Bool
possible Definition
d ]
    possible :: Definition -> Bool
possible Definition
def =
      -- Check whether the given fields are contained
      -- in the fields of record @def@ (if it is a record).
      case Definition -> Defn
theDef Definition
def of
        Record{ recFields :: Defn -> [Dom' Term QName]
recFields = [Dom' Term QName]
fs } -> Set Name -> Set Name -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Name
given (Set Name -> Bool) -> Set Name -> Bool
forall a b. (a -> b) -> a -> b
$
          [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ([Name] -> Set Name) -> [Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ (Dom' Term QName -> Name) -> [Dom' Term QName] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete (Name -> Name)
-> (Dom' Term QName -> Name) -> Dom' Term QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name)
-> (Dom' Term QName -> QName) -> Dom' Term QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom' Term QName]
fs
        Defn
_ -> Bool
False
    given :: Set Name
given = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name]
fields

-- | Get the field types of a record.
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes QName
r = Defn -> Telescope
recTel (Defn -> Telescope) -> TCMT IO Defn -> TCM Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Defn
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r

-- | Get the field names belonging to a record type.
getRecordTypeFields
  :: Type  -- ^ Record type.  Need not be reduced.
  -> TCM [Dom QName]
getRecordTypeFields :: Type -> TCM [Dom' Term QName]
getRecordTypeFields Type
t = do
  Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t  -- Andreas, 2018-03-03, fix for #2989.
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
r Elims
_ -> do
      Defn
rDef <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
      case Defn
rDef of
        Record { recFields :: Defn -> [Dom' Term QName]
recFields = [Dom' Term QName]
fields } -> [Dom' Term QName] -> TCM [Dom' Term QName]
forall (m :: * -> *) a. Monad m => a -> m a
return [Dom' Term QName]
fields
        Defn
_ -> TCM [Dom' Term QName]
forall a. HasCallStack => a
__IMPOSSIBLE__
    Term
_ -> TCM [Dom' Term QName]
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Returns the given record type's constructor name (with an empty
-- range).
getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
getRecordConstructor :: QName -> m ConHead
getRecordConstructor QName
r = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> (Defn -> ConHead) -> Defn -> ConHead
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> ConHead
recConHead (Defn -> ConHead) -> m Defn -> m ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Defn
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r

-- | Check if a name refers to a record.
--   If yes, return record definition.
{-# SPECIALIZE isRecord :: QName -> TCM (Maybe Defn) #-}
{-# SPECIALIZE isRecord :: QName -> ReduceM (Maybe Defn) #-}
isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
isRecord :: QName -> m (Maybe Defn)
isRecord QName
r = do
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
  Maybe Defn -> m (Maybe Defn)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Defn -> m (Maybe Defn)) -> Maybe Defn -> m (Maybe Defn)
forall a b. (a -> b) -> a -> b
$ case Defn
def of
    Record{} -> Defn -> Maybe Defn
forall a. a -> Maybe a
Just Defn
def
    Defn
_        -> Maybe Defn
forall a. Maybe a
Nothing

-- | Reduce a type and check whether it is a record type.
--   Succeeds only if type is not blocked by a meta var.
--   If yes, return its name, parameters, and definition.
isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, Defn))
isRecordType :: Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t = (Blocked Type -> Maybe (QName, Args, Defn))
-> ((QName, Args, Defn) -> Maybe (QName, Args, Defn))
-> Either (Blocked Type) (QName, Args, Defn)
-> Maybe (QName, Args, Defn)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (QName, Args, Defn)
-> Blocked Type -> Maybe (QName, Args, Defn)
forall a b. a -> b -> a
const Maybe (QName, Args, Defn)
forall a. Maybe a
Nothing) (QName, Args, Defn) -> Maybe (QName, Args, Defn)
forall a. a -> Maybe a
Just (Either (Blocked Type) (QName, Args, Defn)
 -> Maybe (QName, Args, Defn))
-> m (Either (Blocked Type) (QName, Args, Defn))
-> m (Maybe (QName, Args, Defn))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType Type
t

-- | Reduce a type and check whether it is a record type.
--   Succeeds only if type is not blocked by a meta var.
--   If yes, return its name, parameters, and definition.
--   If no, return the reduced type (unless it is blocked).
tryRecordType :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType :: Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType Type
t = Type
-> (Blocker
    -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
-> (NotBlocked
    -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
-> m (Either (Blocked Type) (QName, Args, Defn))
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
m Type
a -> Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, Defn)
 -> m (Either (Blocked Type) (QName, Args, Defn)))
-> Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall a b. (a -> b) -> a -> b
$ Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
forall a b. a -> Either a b
Left (Blocked Type -> Either (Blocked Type) (QName, Args, Defn))
-> Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
forall a b. (a -> b) -> a -> b
$ Blocker -> Type -> Blocked Type
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
m Type
a) ((NotBlocked
  -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
 -> m (Either (Blocked Type) (QName, Args, Defn)))
-> (NotBlocked
    -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
-> m (Either (Blocked Type) (QName, Args, Defn))
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
nb Type
t -> do
  let no :: m (Either (Blocked Type) (QName, Args, Defn))
no = Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, Defn)
 -> m (Either (Blocked Type) (QName, Args, Defn)))
-> Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall a b. (a -> b) -> a -> b
$ Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
forall a b. a -> Either a b
Left (Blocked Type -> Either (Blocked Type) (QName, Args, Defn))
-> Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
forall a b. (a -> b) -> a -> b
$ NotBlocked -> Type -> Blocked Type
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
nb Type
t
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
r Elims
es -> do
      let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      m (Maybe Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
-> (Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
-> m (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) m (Either (Blocked Type) (QName, Args, Defn))
no ((Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
 -> m (Either (Blocked Type) (QName, Args, Defn)))
-> (Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
-> m (Either (Blocked Type) (QName, Args, Defn))
forall a b. (a -> b) -> a -> b
$ \ Defn
def -> Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, Defn)
 -> m (Either (Blocked Type) (QName, Args, Defn)))
-> Either (Blocked Type) (QName, Args, Defn)
-> m (Either (Blocked Type) (QName, Args, Defn))
forall a b. (a -> b) -> a -> b
$ (QName, Args, Defn) -> Either (Blocked Type) (QName, Args, Defn)
forall a b. b -> Either a b
Right (QName
r,Args
vs,Defn
def)
    Term
_ -> m (Either (Blocked Type) (QName, Args, Defn))
no

-- | Get the original projection info for name.
{-# SPECIALIZE origProjection :: QName -> TCM (QName, Definition, Maybe Projection) #-}
origProjection ::  HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
origProjection :: QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f = do
  Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  let proj :: Maybe Projection
proj     = Defn -> Maybe Projection
isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def
      fallback :: m (QName, Definition, Maybe Projection)
fallback = (QName, Definition, Maybe Projection)
-> m (QName, Definition, Maybe Projection)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Definition
def, Maybe Projection
proj)
  Maybe Projection
-> m (QName, Definition, Maybe Projection)
-> (Projection -> m (QName, Definition, Maybe Projection))
-> m (QName, Definition, Maybe Projection)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
proj m (QName, Definition, Maybe Projection)
fallback ((Projection -> m (QName, Definition, Maybe Projection))
 -> m (QName, Definition, Maybe Projection))
-> (Projection -> m (QName, Definition, Maybe Projection))
-> m (QName, Definition, Maybe Projection)
forall a b. (a -> b) -> a -> b
$
    \ p :: Projection
p@Projection{ projProper :: Projection -> Maybe QName
projProper = Maybe QName
proper, projOrig :: Projection -> QName
projOrig = QName
f' } ->
      if Maybe QName -> Bool
forall a. Maybe a -> Bool
isNothing Maybe QName
proper Bool -> Bool -> Bool
|| QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' then m (QName, Definition, Maybe Projection)
fallback else do
        Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f'
        (QName, Definition, Maybe Projection)
-> m (QName, Definition, Maybe Projection)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f', Definition
def, Defn -> Maybe Projection
isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def)

-- | @getDefType f t@ computes the type of (possibly projection-(like))
--   function @f@ whose first argument has type @t@.
--   The `parameters' for @f@ are extracted from @t@.
--   @Nothing@ if @f@ is projection(like) but
--   @t@ is not a data/record/axiom type.
--
--   Precondition: @t@ is reduced.
--
--   See also: 'Agda.TypeChecking.Datatypes.getConType'
getDefType :: PureTCM m => QName -> Type -> m (Maybe Type)
getDefType :: QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t = do
  -- Andreas, Issue #1973: we need to take the original projection
  -- since the parameters from the reduced type t are correct for
  -- the original projection only.
  -- Due to module application, the given (non-original) projection f
  -- may expect less parameters, those corresponding to a unreduced
  -- version of t (which we cannot obtain here).
  (QName
f, Definition
def, Maybe Projection
mp) <- QName -> m (QName, Definition, Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f
  let a :: Type
a = Definition -> Type
defType Definition
def
  -- if @f@ is not a projection (like) function, @a@ is the correct type
      fallback :: m (Maybe Type)
fallback = Maybe Type -> m (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> m (Maybe Type)) -> Maybe Type -> m (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
a
  String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.deftype" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"definition f =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"  -- raw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
f)
    , TCM Doc
"has type   a =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    , TCM Doc
"principal  t =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  Maybe Projection
-> m (Maybe Type)
-> (Projection -> m (Maybe Type))
-> m (Maybe Type)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
mp m (Maybe Type)
fallback ((Projection -> m (Maybe Type)) -> m (Maybe Type))
-> (Projection -> m (Maybe Type)) -> m (Maybe Type)
forall a b. (a -> b) -> a -> b
$
    \ (Projection{ projIndex :: Projection -> VerboseLevel
projIndex = VerboseLevel
n }) -> if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0 then m (Maybe Type)
fallback else do
      -- otherwise, we have to instantiate @a@ to the "parameters" of @f@
      let npars :: VerboseLevel
npars | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0    = VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__
                | Bool
otherwise = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1
      String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.deftype" VerboseLevel
20 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"projIndex    = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> String
forall a. Show a => a -> String
show VerboseLevel
n
      -- we get the parameters from type @t@
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Def QName
d Elims
es -> do
          -- Andreas, 2013-10-22
          -- we need to check this @Def@ is fully reduced.
          -- If it is stuck due to disabled reductions
          -- (because of failed termination check),
          -- we will produce garbage parameters.
          m Bool -> m (Maybe Type) -> m (Maybe Type) -> m (Maybe Type)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike QName
d) m (Maybe Type)
failNotElig (m (Maybe Type) -> m (Maybe Type))
-> m (Maybe Type) -> m (Maybe Type)
forall a b. (a -> b) -> a -> b
$ {- else -} do
            -- now we know it is reduced, we can safely take the parameters
            let pars :: Args
pars = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe Args) -> Elims -> Maybe Args
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
npars Elims
es
            String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.deftype" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"head d     = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
d
              , TCM Doc
"parameters =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars)
              ]
            String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.deftype" VerboseLevel
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"parameters = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Args -> String
forall a. Show a => a -> String
show Args
pars
            if Args -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
pars VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
npars then String -> m (Maybe Type)
failure String
"does not supply enough parameters"
            else Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
a Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
        Term
_ -> m (Maybe Type)
failNotDef
  where
    failNotElig :: m (Maybe Type)
failNotElig = String -> m (Maybe Type)
failure String
"is not eligible for projection-likeness"
    failNotDef :: m (Maybe Type)
failNotDef  = String -> m (Maybe Type)
failure String
"is not a Def."
    failure :: String -> m (Maybe Type)
failure String
reason = do
      String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.deftype" VerboseLevel
25 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCM Doc
"Def. " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" is projection(like)"
        , TCM Doc
"but the type "
        , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"of its argument " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reason
        ]
      Maybe Type -> m (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing

-- | The analogue of 'piApply'.  If @v@ is a value of record type @t@
--   with field @f@, then @projectTyped v t f@ returns the type of @f v@.
--   And also the record type (as first result).
--
--   Works also for projection-like definitions @f@.
--   In this case, the first result is not a record type.
--
--   Precondition: @t@ is reduced.
--
projectTyped
  :: PureTCM m
  => Term        -- ^ Head (record value).
  -> Type        -- ^ Its type.
  -> ProjOrigin
  -> QName       -- ^ Projection.
  -> m (Maybe (Dom Type, Term, Type))
projectTyped :: Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
v Type
t ProjOrigin
o QName
f = m (Maybe Type)
-> m (Maybe (Dom Type, Term, Type))
-> (Type -> m (Maybe (Dom Type, Term, Type)))
-> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t) (Maybe (Dom Type, Term, Type) -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom Type, Term, Type)
forall a. Maybe a
Nothing) ((Type -> m (Maybe (Dom Type, Term, Type)))
 -> m (Maybe (Dom Type, Term, Type)))
-> (Type -> m (Maybe (Dom Type, Term, Type)))
-> m (Maybe (Dom Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ \ Type
tf -> do
  Type
-> (Type -> m (Maybe (Dom Type, Term, Type)))
-> (Dom Type -> Abs Type -> m (Maybe (Dom Type, Term, Type)))
-> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
tf (m (Maybe (Dom Type, Term, Type))
-> Type -> m (Maybe (Dom Type, Term, Type))
forall a b. a -> b -> a
const (m (Maybe (Dom Type, Term, Type))
 -> Type -> m (Maybe (Dom Type, Term, Type)))
-> m (Maybe (Dom Type, Term, Type))
-> Type
-> m (Maybe (Dom Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ Maybe (Dom Type, Term, Type) -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom Type, Term, Type)
forall a. Maybe a
Nothing) {- else -} ((Dom Type -> Abs Type -> m (Maybe (Dom Type, Term, Type)))
 -> m (Maybe (Dom Type, Term, Type)))
-> (Dom Type -> Abs Type -> m (Maybe (Dom Type, Term, Type)))
-> m (Maybe (Dom Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ \ Dom Type
dom Abs Type
b -> do
  Term
u <- ProjOrigin -> QName -> Arg Term -> m Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v)
  Maybe (Dom Type, Term, Type) -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Dom Type, Term, Type) -> m (Maybe (Dom Type, Term, Type)))
-> Maybe (Dom Type, Term, Type) -> m (Maybe (Dom Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ (Dom Type, Term, Type) -> Maybe (Dom Type, Term, Type)
forall a. a -> Maybe a
Just (Dom Type
dom, Term
u, Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v)

-- | Typing of an elimination.

data ElimType
  = ArgT (Dom Type)           -- ^ Type of the argument.
  | ProjT
    { ElimType -> Dom Type
projTRec   :: Dom Type  -- ^ The type of the record which is eliminated.
    , ElimType -> Type
projTField :: Type      -- ^ The type of the field.
    }

instance PrettyTCM ElimType where
  prettyTCM :: ElimType -> m Doc
prettyTCM (ArgT Dom Type
a)    = Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
  prettyTCM (ProjT Dom Type
a Type
b) =
    m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
TCM.<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"->" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)

-- | Given a head and its type, compute the types of the eliminations.

typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims Type
a Term
_ [] = [ElimType] -> TCM [ElimType]
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeElims Type
a Term
self (Elim' Term
e : Elims
es) = do
  case Elim' Term
e of
    -- Andrea 02/08/2017: when going from patterns to elims we
    -- generate an Apply elim even for Path types, because we use VarP
    -- for both, so we have to allow for a Path type here.
    Apply Arg Term
v -> Type
-> (Type -> TCM [ElimType])
-> (Dom Type -> Abs Type -> TCM [ElimType])
-> TCM [ElimType]
forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType Type
a Type -> TCM [ElimType]
forall a. HasCallStack => a
__IMPOSSIBLE__ {- else -} ((Dom Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType])
-> (Dom Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType]
forall a b. (a -> b) -> a -> b
$ \ Dom Type
a Abs Type
b -> do
      (Dom Type -> ElimType
ArgT Dom Type
a ElimType -> [ElimType] -> [ElimType]
forall a. a -> [a] -> [a]
:) ([ElimType] -> [ElimType]) -> TCM [ElimType] -> TCM [ElimType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> TCM [ElimType]
typeElims (Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (SubstArg Type -> Type) -> SubstArg Type -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim' Term
e]) Elims
es
    Proj ProjOrigin
o QName
f -> do
      Type
a <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
      (Dom Type
dom, Term
self, Type
a) <- (Dom Type, Term, Type)
-> Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type)
forall a. a -> Maybe a -> a
fromMaybe (Dom Type, Term, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type))
-> TCMT IO (Maybe (Dom Type, Term, Type))
-> TCMT IO (Dom Type, Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> Type
-> ProjOrigin
-> QName
-> TCMT IO (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
self Type
a ProjOrigin
o QName
f
      (Dom Type -> Type -> ElimType
ProjT Dom Type
dom Type
a ElimType -> [ElimType] -> [ElimType]
forall a. a -> [a] -> [a]
:) ([ElimType] -> [ElimType]) -> TCM [ElimType] -> TCM [ElimType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> TCM [ElimType]
typeElims Type
a Term
self Elims
es
    IApply{} -> TCM [ElimType]
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Check if a name refers to an eta expandable record.
{-# SPECIALIZE isEtaRecord :: QName -> TCM Bool #-}
{-# SPECIALIZE isEtaRecord :: QName -> ReduceM Bool #-}
isEtaRecord :: HasConstInfo m => QName -> m Bool
isEtaRecord :: QName -> m Bool
isEtaRecord QName
r = Bool -> (Defn -> Bool) -> Maybe Defn -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
forall a. Eq a => a -> a -> Bool
==) (HasEta' PatternOrCopattern -> Bool)
-> (Defn -> HasEta' PatternOrCopattern) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> HasEta' PatternOrCopattern
recEtaEquality) (Maybe Defn -> Bool) -> m (Maybe Defn) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r

isEtaCon :: HasConstInfo m => QName -> m Bool
isEtaCon :: QName -> m Bool
isEtaCon QName
c = QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c m (Either SigError Definition)
-> (Either SigError Definition -> m Bool) -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left (SigUnknown String
err) -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  Left SigError
SigAbstract -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  Right Definition
def -> case Definition -> Defn
theDef Definition
def of
    Constructor {conData :: Defn -> QName
conData = QName
r} -> QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r
    Defn
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Going under one of these does not count as a decrease in size for the termination checker.
isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor :: QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c =
  m (Maybe (QName, Defn))
-> m Bool -> ((QName, Defn) -> m Bool) -> m Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (((QName, Defn) -> m Bool) -> m Bool)
-> ((QName, Defn) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ (QName
_, Defn
def) -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$
    Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta Bool -> Bool -> Bool
|| Defn -> Maybe Induction
recInduction Defn
def Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
Inductive
      -- If in doubt about coinductivity, then yes.

-- | Check if a name refers to a record which is not coinductive.  (Projections are then size-preserving)
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord QName
r = Bool -> (Defn -> Bool) -> Maybe Defn -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Maybe Induction -> Bool)
-> (Defn -> Maybe Induction) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe Induction
recInduction) (Maybe Defn -> Bool) -> TCMT IO (Maybe Defn) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r

-- | Check if a type is an eta expandable record and return the record identifier and the parameters.
isEtaRecordType :: (HasConstInfo m)
                => Type -> m (Maybe (QName, Args))
isEtaRecordType :: Type -> m (Maybe (QName, Args))
isEtaRecordType Type
a = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
  Def QName
d Elims
es -> do
    let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
    m Bool
-> m (Maybe (QName, Args))
-> m (Maybe (QName, Args))
-> m (Maybe (QName, Args))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d) (Maybe (QName, Args) -> m (Maybe (QName, Args))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (QName, Args) -> m (Maybe (QName, Args)))
-> Maybe (QName, Args) -> m (Maybe (QName, Args))
forall a b. (a -> b) -> a -> b
$ (QName, Args) -> Maybe (QName, Args)
forall a. a -> Maybe a
Just (QName
d, Args
vs)) (Maybe (QName, Args) -> m (Maybe (QName, Args))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
forall a. Maybe a
Nothing)
  Term
_        -> Maybe (QName, Args) -> m (Maybe (QName, Args))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args)
forall a. Maybe a
Nothing

-- | Check if a name refers to a record constructor.
--   If yes, return record definition.
isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
isRecordConstructor :: QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c = QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c m (Either SigError Definition)
-> (Either SigError Definition -> m (Maybe (QName, Defn)))
-> m (Maybe (QName, Defn))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left (SigUnknown String
err)        -> m (Maybe (QName, Defn))
forall a. HasCallStack => a
__IMPOSSIBLE__
  Left SigError
SigAbstract             -> Maybe (QName, Defn) -> m (Maybe (QName, Defn))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Defn)
forall a. Maybe a
Nothing
  Right Definition
def -> case Definition -> Defn
theDef (Definition -> Defn) -> Definition -> Defn
forall a b. (a -> b) -> a -> b
$ Definition
def of
    Constructor{ conData :: Defn -> QName
conData = QName
r } -> (Defn -> (QName, Defn)) -> Maybe Defn -> Maybe (QName, Defn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName
r,) (Maybe Defn -> Maybe (QName, Defn))
-> m (Maybe Defn) -> m (Maybe (QName, Defn))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
    Defn
_                          -> Maybe (QName, Defn) -> m (Maybe (QName, Defn))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Defn)
forall a. Maybe a
Nothing

-- | Check if a constructor name is the internally generated record constructor.
--
--   Works also for abstract constructors.
isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m)
                             => QName -> m Bool
isGeneratedRecordConstructor :: QName -> m Bool
isGeneratedRecordConstructor QName
c = m Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
  m (Maybe (QName, Defn))
-> m Bool -> ((QName, Defn) -> m Bool) -> m Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (((QName, Defn) -> m Bool) -> m Bool)
-> ((QName, Defn) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ (QName
_, Defn
def) ->
    case Defn
def of
      Record{ recNamedCon :: Defn -> Bool
recNamedCon = Bool
False } -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Defn
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False


-- | Turn off eta for unguarded recursive records.
--   Projections do not preserve guardedness.
unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
unguardedRecord :: QName -> PatternOrCopattern -> TCMT IO ()
unguardedRecord QName
q PatternOrCopattern
pat = (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
  r :: Defn
r@Record{} -> Defn
r { recEtaEquality' :: EtaEquality
recEtaEquality' = EtaEquality -> HasEta' PatternOrCopattern -> EtaEquality
setEtaEquality (Defn -> EtaEquality
recEtaEquality' Defn
r) (HasEta' PatternOrCopattern -> EtaEquality)
-> HasEta' PatternOrCopattern -> EtaEquality
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta' PatternOrCopattern
forall a. a -> HasEta' a
NoEta PatternOrCopattern
pat }
  Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Turn on eta for inductive guarded recursive records.
--   Projections do not preserve guardedness.
recursiveRecord :: QName -> TCM ()
recursiveRecord :: QName -> TCMT IO ()
recursiveRecord QName
q = do
  Bool
ok <- TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
etaEnabled
  (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    r :: Defn
r@Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality
eta } ->
      Defn
r { recEtaEquality' :: EtaEquality
recEtaEquality' = EtaEquality
eta' }
      where
      eta' :: EtaEquality
eta' | Bool
ok, Inferred NoEta{} <- EtaEquality
eta, Maybe Induction
ind Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive = HasEta' PatternOrCopattern -> EtaEquality
Inferred HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta
           | Bool
otherwise = EtaEquality
eta
    Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Turn on eta for non-recursive record, unless user declared otherwise.
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord :: QName -> TCMT IO ()
nonRecursiveRecord QName
q = TCM Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
etaEnabled (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
  -- Do nothing if eta is disabled by option.
  (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
    r :: Defn
r@Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = Inferred (NoEta PatternOrCopattern
_) }
      | Maybe Induction
ind Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive ->
      Defn
r { recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta' PatternOrCopattern -> EtaEquality
Inferred HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta }
    r :: Defn
r@Record{} -> Defn
r
    Defn
_          -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | Check whether record type is marked as recursive.
--
--   Precondition: record type identifier exists in signature.
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord QName
q = Defn -> Bool
recRecursive (Defn -> Bool) -> (Signature -> Defn) -> Signature -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Defn)
-> (Signature -> Definition) -> Signature -> Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe Definition -> Definition
forall a. a -> Maybe a -> a
fromMaybe Definition
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Definition -> Definition)
-> (Signature -> Maybe Definition) -> Signature -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Signature -> Maybe Definition
lookupDefinition QName
q (Signature -> Bool) -> TCMT IO Signature -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature

{- | @etaExpandBoundVar i = (Δ, σ, τ)@

Precondition: The current context is @Γ = Γ₁, x:R pars, Γ₂@ where
  @|Γ₂| = i@ and @R@ is a eta-expandable record type
  with constructor @c@ and fields @Γ'@.

Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.
-}
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar :: VerboseLevel -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar VerboseLevel
i = ((Telescope, Substitution, Substitution, Telescope)
 -> (Telescope, Substitution, Substitution))
-> Maybe (Telescope, Substitution, Substitution, Telescope)
-> Maybe (Telescope, Substitution, Substitution)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Telescope
delta, Substitution
sigma, Substitution
tau, Telescope
_) -> (Telescope
delta, Substitution
sigma, Substitution
tau)) (Maybe (Telescope, Substitution, Substitution, Telescope)
 -> Maybe (Telescope, Substitution, Substitution))
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
-> TCM (Maybe (Telescope, Substitution, Substitution))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  VerboseLevel
-> Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar VerboseLevel
i (Telescope
 -> TCMT
      IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> TCM Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope

-- | @expandRecordVar i Γ = (Δ, σ, τ, Γ')@
--
--   Precondition: @Γ = Γ₁, x:R pars, Γ₂@ where
--     @|Γ₂| = i@ and @R@ is a eta-expandable record type
--     with constructor @c@ and fields @Γ'@.
--
--   Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.

expandRecordVar :: Int -> Telescope -> TCM (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar :: VerboseLevel
-> Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar VerboseLevel
i Telescope
gamma0 = do
  -- Get the context with last variable added last in list.
  let gamma :: [Dom (String, Type)]
gamma = Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
gamma0
  -- Convert the de Bruijn index i to a de Bruijn level
      l :: VerboseLevel
l     = [Dom (String, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (String, Type)]
gamma VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
i
  -- Extract type of @i@th de Bruijn index.
  -- Γ = Γ₁, x:a, Γ₂
  let ([Dom (String, Type)]
gamma1, dom :: Dom (String, Type)
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (String
x, Type
a)}) : [Dom (String, Type)]
gamma2) = VerboseLevel
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
l [Dom (String, Type)]
gamma -- TODO:: Defined but not used dom, ai
  -- This must be a eta-expandable record type.
  let failure :: TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
failure = do
        String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.meta.assign.proj" VerboseLevel
25 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          TCM Doc
"failed to eta-expand variable " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty String
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCM Doc
" since its type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCM Doc
" is not a record type"
        Maybe (Telescope, Substitution, Substitution, Telescope)
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. Maybe a
Nothing
  TCMT IO (Maybe (QName, Args, Defn))
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
-> ((QName, Args, Defn)
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCMT IO (Maybe (QName, Args, Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
a) TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
failure (((QName, Args, Defn)
  -> TCMT
       IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
 -> TCMT
      IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> ((QName, Args, Defn)
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars, Defn
def) -> case Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def of
    NoEta{} -> Maybe (Telescope, Substitution, Substitution, Telescope)
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. Maybe a
Nothing
    HasEta' PatternOrCopattern
YesEta  -> (Telescope, Substitution, Substitution, Telescope)
-> Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. a -> Maybe a
Just ((Telescope, Substitution, Substitution, Telescope)
 -> Maybe (Telescope, Substitution, Substitution, Telescope))
-> TCMT IO (Telescope, Substitution, Substitution, Telescope)
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      -- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).
      -- TODO: compose argInfo ai with tel.
      let tel :: Telescope
tel = Defn -> Telescope
recTel Defn
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
          m :: VerboseLevel
m   = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel
          fs :: [Arg QName]
fs  = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
def
      -- Construct the record pattern @Γ₁, Γ' ⊢ u := c ys@.
          ys :: Args
ys  = (Arg QName -> VerboseLevel -> Arg Term)
-> [Arg QName] -> [VerboseLevel] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg QName
f VerboseLevel
i -> Arg QName
f Arg QName -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
i) [Arg QName]
fs ([VerboseLevel] -> Args) -> [VerboseLevel] -> Args
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
m
          u :: Term
u   = ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem Args
ys
      -- @Γ₁, Γ' ⊢ τ₀ : Γ₁, x:_@
          tau0 :: Substitution
tau0 = Term -> Substitution -> Substitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
u (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Substitution
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
m
      -- @Γ₁, Γ', Γ₂ ⊢ τ₀ : Γ₁, x:_, Γ₂@
          tau :: Substitution
tau  = VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS ([Dom (String, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (String, Type)]
gamma2) Substitution
tau0

      --  Fields are in order first-first.
          zs :: Args
zs  = [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
f -> VerboseLevel -> Elims -> Term
Var VerboseLevel
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
      --  We need to reverse the field sequence to build the substitution.
      -- @Γ₁, x:_ ⊢ σ₀ : Γ₁, Γ'@
          sigma0 :: Substitution
sigma0 = [Term] -> [Term]
forall a. [a] -> [a]
reverse ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
zs) [Term] -> Substitution -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# VerboseLevel -> Substitution
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
1
      -- @Γ₁, x:_, Γ₂ ⊢ σ₀ : Γ₁, Γ', Γ₂@
          sigma :: Substitution
sigma  = VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS ([Dom (String, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (String, Type)]
gamma2) Substitution
sigma0

      -- Construct @Δ@ as telescope.
      -- Note @Γ₁, x:_ ⊢ Γ₂@, thus, @Γ₁, Γ' ⊢ [τ₀]Γ₂@

          -- Use "f(x)" as variable name for the projection f(x).
          s :: String
s     = String -> String
forall a. Pretty a => a -> String
prettyShow String
x
          tel' :: Telescope
tel'  = (String -> String) -> Telescope -> Telescope
forall a. (String -> String) -> Tele a -> Tele a
mapAbsNames (\ String
f -> String -> String
stringToArgName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
argNameToString String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") Telescope
tel
          delta :: Telescope
delta = [Dom (String, Type)] -> Telescope
telFromList ([Dom (String, Type)] -> Telescope)
-> [Dom (String, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ [Dom (String, Type)]
gamma1 [Dom (String, Type)]
-> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. [a] -> [a] -> [a]
++ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel' [Dom (String, Type)]
-> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. [a] -> [a] -> [a]
++
                    Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Substitution' (SubstArg Telescope) -> Telescope -> Telescope
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Telescope)
tau0 (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ [Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
gamma2)
                    -- Andreas, 2017-07-29, issue #2644
                    -- We cannot substitute directly into a ListTel like gamma2,
                    -- we have to convert it to a telescope first, otherwise we get garbage.

      (Telescope, Substitution, Substitution, Telescope)
-> TCMT IO (Telescope, Substitution, Substitution, Telescope)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
delta, Substitution
sigma, Substitution
tau, Telescope
tel)

-- | Precondition: variable list is ordered descendingly.  Can be empty.
expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively :: [VerboseLevel]
-> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [] Telescope
gamma = (Telescope, Substitution, Substitution)
-> TCM (Telescope, Substitution, Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma, Substitution
forall a. Substitution' a
idS, Substitution
forall a. Substitution' a
idS)
expandRecordVarsRecursively (VerboseLevel
i : [VerboseLevel]
is) Telescope
gamma = do
  TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
-> TCM (Telescope, Substitution, Substitution)
-> ((Telescope, Substitution, Substitution, Telescope)
    -> TCM (Telescope, Substitution, Substitution))
-> TCM (Telescope, Substitution, Substitution)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (VerboseLevel
-> Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar VerboseLevel
i Telescope
gamma) ([VerboseLevel]
-> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [VerboseLevel]
is Telescope
gamma)
  (((Telescope, Substitution, Substitution, Telescope)
  -> TCM (Telescope, Substitution, Substitution))
 -> TCM (Telescope, Substitution, Substitution))
-> ((Telescope, Substitution, Substitution, Telescope)
    -> TCM (Telescope, Substitution, Substitution))
-> TCM (Telescope, Substitution, Substitution)
forall a b. (a -> b) -> a -> b
$ \ (Telescope
gamma1, Substitution
sigma1, Substitution
tau1, Telescope
tel) -> do
    -- Γ ⊢ σ₁ : Γ₁  and  Γ₁ ⊢ τ₁ : Γ
    let n :: VerboseLevel
n = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel
        newis :: [VerboseLevel]
newis = VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
n ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom (VerboseLevel -> [VerboseLevel]) -> VerboseLevel -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
n
    (Telescope
gamma2, Substitution
sigma2, Substitution
tau2) <- [VerboseLevel]
-> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively ([VerboseLevel]
newis [VerboseLevel] -> [VerboseLevel] -> [VerboseLevel]
forall a. [a] -> [a] -> [a]
++ [VerboseLevel]
is) Telescope
gamma1
    -- Γ₁ ⊢ σ₂ : Γ₂  and  Γ₂ ⊢ τ₂ : Γ₁
    (Telescope, Substitution, Substitution)
-> TCM (Telescope, Substitution, Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma2, Substitution' (SubstArg Substitution)
-> Substitution -> Substitution
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Substitution)
sigma1 Substitution
sigma2, Substitution' (SubstArg Substitution)
-> Substitution -> Substitution
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Substitution)
tau2 Substitution
tau1)

-- | @curryAt v (Γ (y : R pars) -> B) n =
--     ( \ v -> λ Γ ys → v Γ (c ys)            {- curry   -}
--     , \ v -> λ Γ y → v Γ (p1 y) ... (pm y)  {- uncurry -}
--     , Γ (ys : As) → B[c ys / y]
--     )@
--
--   where @n = size Γ@.
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt :: Type -> VerboseLevel -> TCM (Term -> Term, Term -> Term, Type)
curryAt Type
t VerboseLevel
n = do
  -- first, strip the leading n domains (which remain unchanged)
  TelV Telescope
gamma Type
core <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpTo VerboseLevel
n Type
t
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
core of
    -- There should be at least one domain left
    Pi (dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b -> do
      -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
      -- For now, we only eta-expand once.
      -- This might trigger another call to @etaExpandProjectedVar@ later.
      -- A more efficient version does all the eta-expansions at once here.
      (QName
r, Args
pars, Defn
def) <- (QName, Args, Defn)
-> Maybe (QName, Args, Defn) -> (QName, Args, Defn)
forall a. a -> Maybe a -> a
fromMaybe (QName, Args, Defn)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Args, Defn) -> (QName, Args, Defn))
-> TCMT IO (Maybe (QName, Args, Defn))
-> TCMT IO (QName, Args, Defn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe (QName, Args, Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
a
      if | NoEta PatternOrCopattern
_ <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def -> TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
         | Bool
otherwise -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- TODO: compose argInfo ai with tel.
      let tel :: Telescope
tel = Defn -> Telescope
recTel Defn
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
          m :: VerboseLevel
m   = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel
          fs :: [Arg QName]
fs  = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
def
          ys :: Args
ys  = (Arg QName -> VerboseLevel -> Arg Term)
-> [Arg QName] -> [VerboseLevel] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg QName
f VerboseLevel
i -> Arg QName
f Arg QName -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
i) [Arg QName]
fs ([VerboseLevel] -> Args) -> [VerboseLevel] -> Args
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
m
          u :: Term
u   = ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem Args
ys
          b' :: Type
b'  = VerboseLevel -> Abs Type -> Abs Type
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
m Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
          t' :: Type
t'  = Telescope
gamma Telescope -> Type -> Type
`telePi` (Telescope
tel Telescope -> Type -> Type
`telePi` Type
b')
          gammai :: [ArgInfo]
gammai = (Dom (String, Type) -> ArgInfo)
-> [Dom (String, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom (String, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo ([Dom (String, Type)] -> [ArgInfo])
-> [Dom (String, Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
gamma
          xs :: Args
xs  = Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> VerboseLevel -> Arg Term)
-> [ArgInfo] -> [VerboseLevel] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ ArgInfo
ai VerboseLevel
i -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i) [ArgInfo]
gammai [VerboseLevel
m..]
          curry :: Term -> Term
curry Term
v = Telescope -> Term -> Term
teleLam Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
tel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                      VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise (VerboseLevel
nVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
m) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Args
xs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
u])
          zs :: Args
zs  = [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
f -> VerboseLevel -> Elims -> Term
Var VerboseLevel
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
          atel :: Telescope
atel = Dom (String, Type) -> Telescope
forall a. SgTel a => a -> Telescope
sgTel (Dom (String, Type) -> Telescope)
-> Dom (String, Type) -> Telescope
forall a b. (a -> b) -> a -> b
$ (,) (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) (Type -> (String, Type)) -> Dom Type -> Dom (String, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom
          uncurry :: Term -> Term
uncurry Term
v = Telescope -> Term -> Term
teleLam Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
atel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                        VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Args
xs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
zs)
      (Term -> Term, Term -> Term, Type)
-> TCM (Term -> Term, Term -> Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
curry, Term -> Term
uncurry, Type
t')
    Term
_ -> TCM (Term -> Term, Term -> Term, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__

{-| @etaExpand r pars u@ computes the eta expansion of record value @u@
    at record type @r pars@.

    The first argument @r@ should be the name of an eta-expandable record type.
    Given

      @record R : Set where field x : A; y : B; .z : C@

    and @r : R@,

      @etaExpand R [] r = (tel, [R.x r, R.y r, R.z r])@

    where @tel@ is the record telescope instantiated at the parameters @pars@.
-}
etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m)
                => QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord :: QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m) =>
Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' Bool
False

-- | Eta expand a record regardless of whether it's an eta-record or not.
forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
                     => QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord :: QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m) =>
Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' Bool
True

etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m)
                 => Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' :: Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' Bool
forceEta QName
r Args
pars Term
u = do
  Defn
def <- Defn -> Maybe Defn -> Defn
forall a. a -> Maybe a -> a
fromMaybe Defn
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Defn -> Defn) -> m (Maybe Defn) -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
  (Telescope
tel, ConHead
_, ConInfo
_, Args
args) <- Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
forceEta QName
r Args
pars Defn
def Term
u
  (Telescope, Args) -> m (Telescope, Args)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel, Args
args)

etaExpandRecord_ :: HasConstInfo m
                 => QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ :: QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ = Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
False

etaExpandRecord'_ :: HasConstInfo m
                  => Bool -> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ :: Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
forceEta QName
r Args
pars Defn
def Term
u = do
  let Record{ recConHead :: Defn -> ConHead
recConHead     = ConHead
con
            , recFields :: Defn -> [Dom' Term QName]
recFields      = [Dom' Term QName]
xs
            , recTel :: Defn -> Telescope
recTel         = Telescope
tel
            } = Defn
def
      tel' :: Telescope
tel' = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
pars
  -- Make sure we do not expand non-eta records (unless forced to):
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta Bool -> Bool -> Bool
|| Bool
forceEta) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  case Term
u of

    -- Already expanded.
    Con ConHead
con_ ConInfo
ci Elims
es -> do
      let args :: Args
args = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      -- Andreas, 2019-10-21, issue #4148
      -- @con == con_@ might fail, but their normal forms should be equal.
      m (Maybe QName) -> m () -> m ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (ConHead -> QName
conName ConHead
con QName -> QName -> m (Maybe QName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
`sameDef` ConHead -> QName
conName ConHead
con_) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"impossible" VerboseLevel
10 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"etaExpandRecord_: the following two constructors should be identical"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"con  = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ConHead -> String
forall a. Pretty a => a -> String
prettyShow ConHead
con
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"con_ = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ConHead -> String
forall a. Pretty a => a -> String
prettyShow ConHead
con_
          ]
        m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Telescope, ConHead, ConInfo, Args)
-> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel', ConHead
con, ConInfo
ci, Args
args)

    -- Not yet expanded.
    Term
_ -> do
      -- Andreas, < 2016-01-18: Note: recFields are always the original projections,
      -- thus, we can use them in Proj directly.
      let xs' :: Args
xs' = [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for ((Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
xs) ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
x -> Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]
      String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.record.eta" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"eta expanding" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"tel' =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
          , TCM Doc
"args =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
xs'
          ]
        ]
      (Telescope, ConHead, ConInfo, Args)
-> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel', ConHead
con, ConInfo
ConOSystem, Args
xs')

etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType Type
t Term
u = do
  (QName
r, Args
pars, Defn
def) <- (QName, Args, Defn)
-> Maybe (QName, Args, Defn) -> (QName, Args, Defn)
forall a. a -> Maybe a -> a
fromMaybe (QName, Args, Defn)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Args, Defn) -> (QName, Args, Defn))
-> TCMT IO (Maybe (QName, Args, Defn))
-> TCMT IO (QName, Args, Defn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe (QName, Args, Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t
  (Telescope
tel, ConHead
con, ConInfo
ci, Args
args) <- QName
-> Args
-> Defn
-> Term
-> TCMT IO (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
r Args
pars Defn
def Term
u
  (Telescope, Term) -> TCM (Telescope, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel, ConHead -> ConInfo -> Args -> Term
mkCon ConHead
con ConInfo
ci Args
args)

-- | The fields should be eta contracted already.
--
--   We can eta contract if all fields @f = ...@ are irrelevant
--   or all fields @f@ are the projection @f v@ of the same value @v@,
--   but we need at least one relevant field to find the value @v@.
--
--   If all fields are erased, we cannot eta-contract.

--   Andreas, 2019-11-06, issue #4168: eta-contraction all-erased record
--   lead to compilation error.

--   TODO: this can be moved out of TCM.
--   Andreas, 2018-01-28: attempted just that, but Auto does not
--   put the conFields there (it does not run in TCM).
--   If we get rid of Auto, we can do this.  (Tests not involving Auto pass.)

{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> TCM Term #-}
{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> ReduceM Term #-}
etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord QName
r ConHead
c ConInfo
ci Args
args = if (Arg Term -> Bool) -> Args -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Arg Term -> Bool) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Bool
forall a. LensModality a => a -> Bool
usableModality) Args
args then m Term
fallBack else do
  Just Record{ recFields :: Defn -> [Dom' Term QName]
recFields = [Dom' Term QName]
xs } <- QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
  String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.record.eta.contract" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"eta contracting record"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"record type r  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
      , TCM Doc
"constructor c  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
      , TCM Doc
"field names xs =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Dom' Term QName] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty    [Dom' Term QName]
xs
      , TCM Doc
"fields    args =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
args
      ]
    ]
  case VerboseLevel -> VerboseLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Args -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
args) ([Dom' Term QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Dom' Term QName]
xs) of
    Ordering
LT -> m Term
fallBack       -- Not fully applied
    Ordering
GT -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Too many arguments. Impossible.
    Ordering
EQ -> do
      case (Arg Term -> Dom' Term QName -> Maybe (Maybe Term))
-> Args -> [Dom' Term QName] -> Maybe [Maybe Term]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Arg Term -> Dom' Term QName -> Maybe (Maybe Term)
check Args
args [Dom' Term QName]
xs of
        Just [Maybe Term]
as -> case [Maybe Term] -> [Term]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Term]
as of
          (Term
a:[Term]
as) ->
            if (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term
a Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
==) [Term]
as
              then Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
a
              else m Term
fallBack
          [Term]
_ -> m Term
fallBack -- just irrelevant terms
        Maybe [Maybe Term]
_ -> m Term
fallBack  -- a Nothing
  where
  fallBack :: m Term
fallBack = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> ConInfo -> Args -> Term
mkCon ConHead
c ConInfo
ci Args
args)
  check :: Arg Term -> Dom QName -> Maybe (Maybe Term)
  check :: Arg Term -> Dom' Term QName -> Maybe (Maybe Term)
check Arg Term
a Dom' Term QName
ax = do
  -- @a@ is the constructor argument, @ax@ the corr. record field name
    -- skip irrelevant record fields by returning DontCare
    case (Arg Term -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg Term
a, Term -> Maybe (Elims -> Term, Elims)
hasElims (Term -> Maybe (Elims -> Term, Elims))
-> Term -> Maybe (Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) of
      (Relevance
Irrelevant, Maybe (Elims -> Term, Elims)
_)   -> Maybe Term -> Maybe (Maybe Term)
forall a. a -> Maybe a
Just Maybe Term
forall a. Maybe a
Nothing
      -- if @a@ is the record field name applied to a single argument
      -- then it passes the check
      (Relevance
_, Just (Elims -> Term
_, [])) -> Maybe (Maybe Term)
forall a. Maybe a
Nothing  -- not a projection
      (Relevance
_, Just (Elims -> Term
h, Elim' Term
e0:Elims
es0))
        | (Elims
es, Proj ProjOrigin
_o QName
f) <- Elim' Term -> Elims -> (Elims, Elim' Term)
forall a. a -> [a] -> ([a], a)
initLast1 Elim' Term
e0 Elims
es0
        , Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom Dom' Term QName
ax QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f -> Maybe Term -> Maybe (Maybe Term)
forall a. a -> Maybe a
Just (Maybe Term -> Maybe (Maybe Term))
-> Maybe Term -> Maybe (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
h Elims
es
      (Relevance, Maybe (Elims -> Term, Elims))
_                 -> Maybe (Maybe Term)
forall a. Maybe a
Nothing

-- | Is the type a hereditarily singleton record type? May return a
-- blocking metavariable.
--
-- Precondition: The name should refer to a record type, and the
-- arguments should be the parameters to the type.
isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
isSingletonRecord :: QName -> Args -> m Bool
isSingletonRecord QName
r Args
ps = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> QName -> Args -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> m (Maybe Term)
isSingletonRecord' Bool
False QName
r Args
ps

isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m)
                                 => QName -> Args -> m Bool
isSingletonRecordModuloRelevance :: QName -> Args -> m Bool
isSingletonRecordModuloRelevance QName
r Args
ps = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> QName -> Args -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> m (Maybe Term)
isSingletonRecord' Bool
True QName
r Args
ps

-- | Return the unique (closed) inhabitant if exists.
--   In case of counting irrelevance in, the returned inhabitant
--   contains dummy terms.
isSingletonRecord' :: forall m. (PureTCM m, MonadBlock m)
                   => Bool -> QName -> Args -> m (Maybe Term)
isSingletonRecord' :: Bool -> QName -> Args -> m (Maybe Term)
isSingletonRecord' Bool
regardIrrelevance QName
r Args
ps = do
  String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.meta.eta" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Is" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
ps) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"a singleton record type?"
  QName -> m (Maybe Defn)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r m (Maybe Defn) -> (Maybe Defn -> m (Maybe Term)) -> m (Maybe Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Defn
Nothing  -> Maybe Term -> m (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
    Just Defn
def -> do
      (Args -> Term) -> Maybe Args -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem) (Maybe Args -> Maybe Term) -> m (Maybe Args) -> m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m (Maybe Args)
check (Defn -> Telescope
recTel Defn
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
ps)
  where
  check :: Telescope -> m (Maybe [Arg Term])
  check :: Telescope -> m (Maybe Args)
check Telescope
tel = do
    String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.meta.eta" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"isSingletonRecord' checking telescope " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
    case Telescope
tel of
      Telescope
EmptyTel -> Maybe Args -> m (Maybe Args)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Args -> m (Maybe Args)) -> Maybe Args -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args
forall a. a -> Maybe a
Just []
      ExtendTel Dom Type
dom Abs Telescope
tel -> m Bool -> m (Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
regardIrrelevance m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Dom Type -> m Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom Type
dom)
        {-then-}
          (Dom Type
-> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Telescope
tel ((Telescope -> m (Maybe Args)) -> m (Maybe Args))
-> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ (Maybe Args -> Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Args -> Args) -> Maybe Args -> Maybe Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) Term
HasCallStack => Term
__DUMMY_TERM__ Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
:)) (m (Maybe Args) -> m (Maybe Args))
-> (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> m (Maybe Args)
check)
        {-else-} (m (Maybe Args) -> m (Maybe Args))
-> m (Maybe Args) -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ do
          Maybe Term
isSing <- Bool -> Type -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> m (Maybe Term)
isSingletonType' Bool
regardIrrelevance (Type -> m (Maybe Term)) -> Type -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
          case Maybe Term
isSing of
            Maybe Term
Nothing  -> Maybe Args -> m (Maybe Args)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Args
forall a. Maybe a
Nothing
            (Just Term
v) -> Dom Type
-> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Telescope
tel ((Telescope -> m (Maybe Args)) -> m (Maybe Args))
-> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ (Maybe Args -> Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Args -> Args) -> Maybe Args -> Maybe Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) Term
v Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
:)) (m (Maybe Args) -> m (Maybe Args))
-> (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> m (Maybe Args)
check

-- | Check whether a type has a unique inhabitant and return it.
--   Can be blocked by a metavar.
isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)
isSingletonType :: Type -> m (Maybe Term)
isSingletonType = Bool -> Type -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> m (Maybe Term)
isSingletonType' Bool
False

-- | Check whether a type has a unique inhabitant (irrelevant parts ignored).
--   Can be blocked by a metavar.
isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance :: Type -> m Bool
isSingletonTypeModuloRelevance Type
t = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> m (Maybe Term)
isSingletonType' Bool
True Type
t

isSingletonType' :: (PureTCM m, MonadBlock m) => Bool -> Type -> m (Maybe Term)
isSingletonType' :: Bool -> Type -> m (Maybe Term)
isSingletonType' Bool
regardIrrelevance Type
t = do
    TelV Telescope
tel Type
t <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
    Type
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
    Telescope -> m (Maybe Term) -> m (Maybe Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m (Maybe Term) -> m (Maybe Term))
-> m (Maybe Term) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
      Maybe (QName, Args, Defn)
res <- Type -> m (Maybe (QName, Args, Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t
      case Maybe (QName, Args, Defn)
res of
        Just (QName
r, Args
ps, Defn
def) | HasEta' PatternOrCopattern
YesEta <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def -> do
          (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) (Maybe Term -> Maybe Term) -> m (Maybe Term) -> m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> QName -> Args -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> m (Maybe Term)
isSingletonRecord' Bool
regardIrrelevance QName
r Args
ps
        Maybe (QName, Args, Defn)
_ -> Maybe Term -> m (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing

-- | Checks whether the given term (of the given type) is beta-eta-equivalent
--   to a variable. Returns just the de Bruijn-index of the variable if it is,
--   or nothing otherwise.
isEtaVar :: forall m. PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar :: Term -> Type -> m (Maybe VerboseLevel)
isEtaVar Term
u Type
a = MaybeT m VerboseLevel -> m (Maybe VerboseLevel)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m VerboseLevel -> m (Maybe VerboseLevel))
-> MaybeT m VerboseLevel -> m (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ Term
-> Type
-> Maybe VerboseLevel
-> [Elim' VerboseLevel]
-> MaybeT m VerboseLevel
isEtaVarG Term
u Type
a Maybe VerboseLevel
forall a. Maybe a
Nothing []
  where
    -- Checks whether the term u (of type a) is beta-eta-equivalent to
    -- `Var i es`, and returns i if it is. If the argument mi is `Just i'`,
    -- then i and i' are also required to be equal (else Nothing is returned).
    isEtaVarG :: Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG :: Term
-> Type
-> Maybe VerboseLevel
-> [Elim' VerboseLevel]
-> MaybeT m VerboseLevel
isEtaVarG Term
u Type
a Maybe VerboseLevel
mi [Elim' VerboseLevel]
es = do
      (Term
u, Type
a) <- (Term, Type) -> MaybeT m (Term, Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Type
a)
      String -> VerboseLevel -> TCM Doc -> MaybeT m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.lhs" VerboseLevel
80 (TCM Doc -> MaybeT m ()) -> TCM Doc -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"isEtaVarG" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"u  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
        , TCM Doc
"a  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        , TCM Doc
"mi = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Maybe VerboseLevel -> String
forall a. Show a => a -> String
show Maybe VerboseLevel
mi)
        , TCM Doc
"es = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Elim' VerboseLevel -> TCM Doc)
-> [Elim' VerboseLevel] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Elim' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elim' Term -> TCM Doc)
-> (Elim' VerboseLevel -> Elim' Term)
-> Elim' VerboseLevel
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseLevel -> Term) -> Elim' VerboseLevel -> Elim' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VerboseLevel -> Term
var) [Elim' VerboseLevel]
es)
        ])
      case (Term
u, Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) of
        (Var VerboseLevel
i' Elims
es', Term
_) -> do
          Bool -> MaybeT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ Maybe VerboseLevel
mi Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== (VerboseLevel
i' VerboseLevel -> Maybe VerboseLevel -> Maybe VerboseLevel
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe VerboseLevel
mi)
          Type
b <- VerboseLevel -> MaybeT m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i'
          Term -> Type -> Elims -> [Elim' VerboseLevel] -> MaybeT m ()
areEtaVarElims (VerboseLevel -> Term
var VerboseLevel
i') Type
b Elims
es' [Elim' VerboseLevel]
es
          VerboseLevel -> MaybeT m VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
i'
        (Term
_, Def QName
d Elims
pars) -> do
          Bool -> MaybeT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT m ()) -> MaybeT m Bool -> MaybeT m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do QName -> MaybeT m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d
          [QName]
fs <- (Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom ([Dom' Term QName] -> [QName])
-> (Definition -> [Dom' Term QName]) -> Definition -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields (Defn -> [Dom' Term QName])
-> (Definition -> Defn) -> Definition -> [Dom' Term QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> [QName]) -> MaybeT m Definition -> MaybeT m [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> MaybeT m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          [VerboseLevel]
is <- [QName]
-> (QName -> MaybeT m VerboseLevel) -> MaybeT m [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [QName]
fs ((QName -> MaybeT m VerboseLevel) -> MaybeT m [VerboseLevel])
-> (QName -> MaybeT m VerboseLevel) -> MaybeT m [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ \QName
f -> do
            let o :: ProjOrigin
o = ProjOrigin
ProjSystem
            (Dom Type
_, Term
_, Type
fa) <- m (Maybe (Dom Type, Term, Type)) -> MaybeT m (Dom Type, Term, Type)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (Dom Type, Term, Type))
 -> MaybeT m (Dom Type, Term, Type))
-> m (Maybe (Dom Type, Term, Type))
-> MaybeT m (Dom Type, Term, Type)
forall a b. (a -> b) -> a -> b
$ Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
u Type
a ProjOrigin
o QName
f
            Term
-> Type
-> Maybe VerboseLevel
-> [Elim' VerboseLevel]
-> MaybeT m VerboseLevel
isEtaVarG (Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]) Type
fa Maybe VerboseLevel
mi ([Elim' VerboseLevel]
es [Elim' VerboseLevel]
-> [Elim' VerboseLevel] -> [Elim' VerboseLevel]
forall a. [a] -> [a] -> [a]
++ [ProjOrigin -> QName -> Elim' VerboseLevel
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f])
          case (Maybe VerboseLevel
mi, [VerboseLevel]
is) of
            (Just VerboseLevel
i, [VerboseLevel]
_)     -> VerboseLevel -> MaybeT m VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
i
            (Maybe VerboseLevel
Nothing, [])   -> MaybeT m VerboseLevel
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (Maybe VerboseLevel
Nothing, VerboseLevel
i:[VerboseLevel]
is) -> Bool -> MaybeT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((VerboseLevel -> Bool) -> [VerboseLevel] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
i) [VerboseLevel]
is) MaybeT m () -> MaybeT m VerboseLevel -> MaybeT m VerboseLevel
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> VerboseLevel -> MaybeT m VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
i
        (Term
_, Pi Dom Type
dom Abs Type
cod) -> Dom Type -> MaybeT m VerboseLevel -> MaybeT m VerboseLevel
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
dom (MaybeT m VerboseLevel -> MaybeT m VerboseLevel)
-> MaybeT m VerboseLevel -> MaybeT m VerboseLevel
forall a b. (a -> b) -> a -> b
$ do
          let u' :: Term
u'  = VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
1 Term
u Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
0]
              a' :: Type
a'  = Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
cod
              mi' :: Maybe VerboseLevel
mi' = (VerboseLevel -> VerboseLevel)
-> Maybe VerboseLevel -> Maybe VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1) Maybe VerboseLevel
mi
              es' :: [Elim' VerboseLevel]
es' = ((Elim' VerboseLevel -> Elim' VerboseLevel)
-> [Elim' VerboseLevel] -> [Elim' VerboseLevel]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Elim' VerboseLevel -> Elim' VerboseLevel)
 -> [Elim' VerboseLevel] -> [Elim' VerboseLevel])
-> ((VerboseLevel -> VerboseLevel)
    -> Elim' VerboseLevel -> Elim' VerboseLevel)
-> (VerboseLevel -> VerboseLevel)
-> [Elim' VerboseLevel]
-> [Elim' VerboseLevel]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseLevel -> VerboseLevel)
-> Elim' VerboseLevel -> Elim' VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1) [Elim' VerboseLevel]
es [Elim' VerboseLevel]
-> [Elim' VerboseLevel] -> [Elim' VerboseLevel]
forall a. [a] -> [a] -> [a]
++ [Arg VerboseLevel -> Elim' VerboseLevel
forall a. Arg a -> Elim' a
Apply (Arg VerboseLevel -> Elim' VerboseLevel)
-> Arg VerboseLevel -> Elim' VerboseLevel
forall a b. (a -> b) -> a -> b
$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom Arg Type -> VerboseLevel -> Arg VerboseLevel
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel
0]
          (-VerboseLevel
1VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+) (VerboseLevel -> VerboseLevel)
-> MaybeT m VerboseLevel -> MaybeT m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> Type
-> Maybe VerboseLevel
-> [Elim' VerboseLevel]
-> MaybeT m VerboseLevel
isEtaVarG Term
u' Type
a' Maybe VerboseLevel
mi' [Elim' VerboseLevel]
es'
        (Term, Term)
_ -> MaybeT m VerboseLevel
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    -- `areEtaVarElims u a es es'` checks whether the given elims es (as applied
    -- to the term u of type a) are beta-eta-equal to either projections or
    -- variables with de Bruijn indices given by es'.
    areEtaVarElims :: Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims :: Term -> Type -> Elims -> [Elim' VerboseLevel] -> MaybeT m ()
areEtaVarElims Term
u Type
a []    []    = () -> MaybeT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    areEtaVarElims Term
u Type
a []    (Elim' VerboseLevel
_:[Elim' VerboseLevel]
_) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Elim' Term
_:Elims
_) []    = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Proj ProjOrigin
o QName
f : Elims
es) (Proj ProjOrigin
_ QName
f' : [Elim' VerboseLevel]
es') = do
      Bool -> MaybeT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'
      Type
a       <- Type -> MaybeT m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
      (Dom Type
_, Term
_, Type
fa) <- m (Maybe (Dom Type, Term, Type)) -> MaybeT m (Dom Type, Term, Type)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (Dom Type, Term, Type))
 -> MaybeT m (Dom Type, Term, Type))
-> m (Maybe (Dom Type, Term, Type))
-> MaybeT m (Dom Type, Term, Type)
forall a b. (a -> b) -> a -> b
$ Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
u Type
a ProjOrigin
o QName
f
      Term -> Type -> Elims -> [Elim' VerboseLevel] -> MaybeT m ()
areEtaVarElims (Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]) Type
fa Elims
es [Elim' VerboseLevel]
es'
    -- These two cases can occur only when we're looking at two different
    -- variables (i.e. one of function type and the other of record type) so
    -- it's definitely not the variable we're looking for (or someone is playing
    -- Jedi mind tricks on us)
    areEtaVarElims Term
u Type
a (Proj{}  : Elims
_ ) (Apply Arg VerboseLevel
_ : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Apply Arg Term
_ : Elims
_ ) (Proj{}  : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Proj{} : Elims
_ ) (IApply{} : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Proj{} : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Apply  Arg Term
_ : Elims
_ ) (IApply{} : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Apply  Arg VerboseLevel
_ : [Elim' VerboseLevel]
_  ) = MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_) (IApply{} : [Elim' VerboseLevel]
_) = MaybeT m ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- TODO Andrea: not actually impossible, should be done like Apply
    areEtaVarElims Term
u Type
a (Apply Arg Term
v : Elims
es) (Apply Arg VerboseLevel
i : [Elim' VerboseLevel]
es') = do
      Type
-> (Type -> MaybeT m ())
-> (Dom Type -> Abs Type -> MaybeT m ())
-> MaybeT m ()
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
a (MaybeT m () -> Type -> MaybeT m ()
forall a b. a -> b -> a
const MaybeT m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero) ((Dom Type -> Abs Type -> MaybeT m ()) -> MaybeT m ())
-> (Dom Type -> Abs Type -> MaybeT m ()) -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ \Dom Type
dom Abs Type
cod -> do
      VerboseLevel
_ <- Term
-> Type
-> Maybe VerboseLevel
-> [Elim' VerboseLevel]
-> MaybeT m VerboseLevel
isEtaVarG (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) (VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just (VerboseLevel -> Maybe VerboseLevel)
-> VerboseLevel -> Maybe VerboseLevel
forall a b. (a -> b) -> a -> b
$ Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg Arg VerboseLevel
i) []
      Term -> Type -> Elims -> [Elim' VerboseLevel] -> MaybeT m ()
areEtaVarElims (Term
u Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [(VerboseLevel -> Term) -> Arg VerboseLevel -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VerboseLevel -> Term
var Arg VerboseLevel
i]) (Abs Type
cod Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` VerboseLevel -> Term
var (Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg Arg VerboseLevel
i)) Elims
es [Elim' VerboseLevel]
es'


-- | Replace projection patterns by the original projections.
--
class NormaliseProjP a where
  normaliseProjP :: HasConstInfo m => a -> m a

instance NormaliseProjP Clause where
  normaliseProjP :: Clause -> m Clause
normaliseProjP Clause
cl = do
    NAPs
ps <- NAPs -> m NAPs
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP (NAPs -> m NAPs) -> NAPs -> m NAPs
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl
    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
$ Clause
cl { namedClausePats :: NAPs
namedClausePats = NAPs
ps }

instance NormaliseProjP a => NormaliseProjP [a] where
  normaliseProjP :: [a] -> m [a]
normaliseProjP = (a -> m a) -> [a] -> m [a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Arg a) where
  normaliseProjP :: Arg a -> m (Arg a)
normaliseProjP = (a -> m a) -> Arg a -> m (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Named_ a) where
  normaliseProjP :: Named_ a -> m (Named_ a)
normaliseProjP = (a -> m a) -> Named_ a -> m (Named_ a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP

instance NormaliseProjP (Pattern' x) where
  normaliseProjP :: Pattern' x -> m (Pattern' x)
normaliseProjP p :: Pattern' x
p@VarP{}        = Pattern' x -> m (Pattern' x)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
  normaliseProjP p :: Pattern' x
p@DotP{}        = Pattern' x -> m (Pattern' x)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
  normaliseProjP (ConP ConHead
c ConPatternInfo
cpi [NamedArg (Pattern' x)]
ps) = ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi ([NamedArg (Pattern' x)] -> Pattern' x)
-> m [NamedArg (Pattern' x)] -> m (Pattern' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [NamedArg (Pattern' x)]
ps
  normaliseProjP (DefP PatternInfo
o QName
q [NamedArg (Pattern' x)]
ps) = PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' x)] -> Pattern' x)
-> m [NamedArg (Pattern' x)] -> m (Pattern' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [NamedArg (Pattern' x)]
ps
  normaliseProjP p :: Pattern' x
p@LitP{}        = Pattern' x -> m (Pattern' x)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
  normaliseProjP (ProjP ProjOrigin
o QName
d0)    = ProjOrigin -> QName -> Pattern' x
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o (QName -> Pattern' x) -> m QName -> m (Pattern' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d0
  normaliseProjP p :: Pattern' x
p@IApplyP{}     = Pattern' x -> m (Pattern' x)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p