{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.Records where

import Prelude hiding (null)

import Control.Applicative        ( (<|>) )
import Control.Monad.Except       ( MonadError )
import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )
import Control.Monad.Writer       ( Writer, runWriter, tell )

import Data.Bifunctor
import Data.List qualified as List
import Data.Maybe
import Data.Set (Set)
import Data.Set qualified as Set
import Data.HashMap.Strict qualified as HMap
import Data.Text.Short qualified as TS

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

import Mikan.TypeChecking.Irrelevance
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Base.Warning qualified as W
import Mikan.TypeChecking.Pretty as TCM
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Reduce.Monad () --instance only
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Warnings
import {-# SOURCE #-} Mikan.TypeChecking.Primitive.Cubical.Base (isCubicalSubtype)
import {-# SOURCE #-} Mikan.TypeChecking.ProjectionLike (eligibleForProjectionLike)

import Mikan.Utils.CallStack ( HasCallStack )
import Mikan.Utils.Empty
import Mikan.Utils.Function (applyWhen)
import Mikan.Utils.Functor (($>), (<&>))
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Utils.Singleton
import Mikan.Utils.Size

import Mikan.Utils.Impossible

---------------------------------------------------------------------------
-- * Tools to build record values

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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args

-- | Order the fields of a record construction.
orderFields
  :: forall a . HasRange a
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields ConInfo
orig 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)
  --   ]
  Bool
-> WriterT [RecordFieldWarning] Identity ()
-> WriterT [RecordFieldWarning] Identity ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ConInfo
orig ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConORecWhere) (WriterT [RecordFieldWarning] Identity ()
 -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$
    [(Name, a)]
-> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [(Name, a)]
alien     ((List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
 -> WriterT [RecordFieldWarning] Identity ())
-> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ (NonEmpty (Name, Range) -> RecordFieldWarning)
-> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ()
forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {f :: * -> *}
       {a}.
(MonadWriter b m, Singleton b b, Bifunctor p, HasRange b,
 Functor f) =>
(f (p a Range) -> b) -> f (p a b) -> m ()
warn ((NonEmpty (Name, Range) -> RecordFieldWarning)
 -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> (NonEmpty (Name, Range) -> RecordFieldWarning)
-> List1 (Name, a)
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> NonEmpty (Name, Range) -> RecordFieldWarning
W.TooManyFields QName
r [Name]
missing

  [(Name, a)]
-> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [(Name, a)]
duplicate ((List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
 -> WriterT [RecordFieldWarning] Identity ())
-> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ (NonEmpty (Name, Range) -> RecordFieldWarning)
-> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ()
forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {f :: * -> *}
       {a}.
(MonadWriter b m, Singleton b b, Bifunctor p, HasRange b,
 Functor f) =>
(f (p a Range) -> b) -> f (p a b) -> m ()
warn ((NonEmpty (Name, Range) -> RecordFieldWarning)
 -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
-> (NonEmpty (Name, Range) -> RecordFieldWarning)
-> List1 (Name, a)
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ List1 (Name, List1 Range) -> RecordFieldWarning
W.DuplicateFields (List1 (Name, List1 Range) -> RecordFieldWarning)
-> (NonEmpty (Name, Range) -> List1 (Name, List1 Range))
-> NonEmpty (Name, Range)
-> RecordFieldWarning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Range) -> (Name, List1 Range))
-> NonEmpty (Name, Range) -> List1 (Name, List1 Range)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Range -> List1 Range) -> (Name, Range) -> (Name, List1 Range)
forall a b. (a -> b) -> (Name, a) -> (Name, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Range -> List1 Range
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
  [a] -> WriterT [RecordFieldWarning] Identity [a]
forall a. a -> WriterT [RecordFieldWarning] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> WriterT [RecordFieldWarning] Identity [a])
-> [a] -> WriterT [RecordFieldWarning] Identity [a]
forall a b. (a -> b) -> a -> b
$ [Arg Name]
axs [Arg Name] -> (Arg Name -> a) -> [a]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 :: (f (p a Range) -> b) -> f (p a b) -> m ()
warn f (p a Range) -> b
w    = b -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (b -> m ()) -> (f (p a b) -> b) -> f (p a b) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
forall el coll. Singleton el coll => el -> coll
singleton (b -> b) -> (f (p a b) -> b) -> f (p a b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (p a Range) -> b
w (f (p a Range) -> b)
-> (f (p a b) -> f (p a Range)) -> f (p a b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p a b -> p a Range) -> f (p a b) -> f (p a Range)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> Range) -> p a b -> p a Range
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> Range
forall a. HasRange a => a -> Range
getRange)

-- | Raise generated 'RecordFieldWarning's as warnings.
warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings :: forall a. 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 :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> 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 -> TCMT IO a
forall a. a -> TCMT IO 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 :: forall a. 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 (ZonkAny 0))
-> [RecordFieldWarning] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TypeError -> TCMT IO (ZonkAny 0)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCMT IO (ZonkAny 0))
-> (RecordFieldWarning -> TypeError)
-> RecordFieldWarning
-> TCMT IO (ZonkAny 0)
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 -> TCMT IO a
forall a. a -> TCMT IO 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
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn ConInfo
o 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
$ ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields ConInfo
o 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
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsFail ConInfo
o 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
$ ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields ConInfo
o 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
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields ConInfo
o 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 NamedName a
forall c. Arg Name -> c -> Named_ c
nameIfHidden Arg Name
a a
e Named NamedName a -> Arg Name -> NamedArg a
forall a b. a -> Arg b -> Arg 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)]
-> WriterT [RecordFieldWarning] Identity [NamedArg a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConInfo
-> QName
-> (Arg Name -> Maybe (NamedArg a))
-> [Arg Name]
-> [(Name, Maybe (NamedArg a))]
-> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
forall a.
HasRange a =>
ConInfo
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields ConInfo
o 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 NamedName a
forall a name. a -> Named name a
unnamed (a -> Named NamedName a)
-> (Name -> a) -> Name -> Named NamedName a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> a
placeholder (Name -> Named NamedName 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 :: forall c. Arg Name -> c -> Named_ c
nameIfHidden Arg Name
ax
      | Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
ax = c -> Named NamedName c
forall a name. a -> Named name a
unnamed
      | Bool
otherwise  = NamedName -> c -> Named NamedName c
forall name a. name -> a -> Named name a
named (NamedName -> c -> Named NamedName c)
-> NamedName -> c -> Named NamedName c
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged RawName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged RawName -> NamedName) -> Ranged RawName -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> RawName -> Ranged RawName
forall a. Range -> a -> Ranged a
Ranged (Arg Name -> Range
forall a. HasRange a => a -> Range
getRange Arg Name
ax) (RawName -> Ranged RawName) -> RawName -> Ranged RawName
forall a b. (a -> b) -> a -> b
$ Name -> RawName
C.nameToRawName (Name -> RawName) -> Name -> RawName
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
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn ConInfo
o 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
$ ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields ConInfo
o 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
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> 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 :: forall a.
HasRange a =>
ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail ConInfo
o 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
$ ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
ConInfo
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields ConInfo
o QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs

---------------------------------------------------------------------------
-- * Query information about records from signature

-- | Check if a name refers to a record.
--   If yes, return record definition.
{-# INLINE isRecord #-}
isRecord :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe RecordData)
isRecord :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r = do
  QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
r m Definition -> (Definition -> Defn) -> m Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef m Defn -> (Defn -> Maybe RecordData) -> m (Maybe RecordData)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    RecordDefn RecordData
rd -> RecordData -> Maybe RecordData
forall a. a -> Maybe a
Just RecordData
rd
    Defn
_ -> Maybe RecordData
forall a. Maybe a
Nothing

-- | Get the definition for a record. Throws an exception if the name
--   does not refer to a record or the record is abstract.
getRecordDef :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m RecordData
getRecordDef :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r = m RecordData -> m (Maybe RecordData) -> m RecordData
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m RecordData
err (m (Maybe RecordData) -> m RecordData)
-> m (Maybe RecordData) -> m RecordData
forall a b. (a -> b) -> a -> b
$ QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r
  where err :: m RecordData
err = TypeError -> m RecordData
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m RecordData) -> TypeError -> m RecordData
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a b. a -> Maybe b -> Maybe a
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 :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m)
  => QName
  -> m [Dom C.Name]
getRecordFieldNames :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m [Dom Name]
getRecordFieldNames QName
r = RecordData -> [Dom Name]
recordFieldNames (RecordData -> [Dom Name]) -> m RecordData -> m [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m RecordData
forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r

recordFieldNames :: RecordData -> [Dom C.Name]
recordFieldNames :: RecordData -> [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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
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])
-> (RecordData -> [Dom' Term QName]) -> RecordData -> [Dom Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordData -> [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
  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
<$> Getter TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
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' Signature (HashMap QName Definition)
sigDefinitions)
  idefs <- HMap.elems <$> useTC (stImports   . sigDefinitions)
  scope <- getScope
  return $ filter (`isNameInScope` scope) $ cands defs ++ cands 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 names belonging to a record type.
getRecordTypeFields :: HasCallStack
  => Type  -- ^ Record type.  Need not be reduced.
  -> TCM [Dom QName]
getRecordTypeFields :: HasCallStack => Type -> TCM [Dom' Term QName]
getRecordTypeFields Type
t = do
  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 unEl t of
    Def QName
r Elims
_ -> do
      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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
r
      case rDef of
        Record { recFields :: Defn -> [Dom' Term QName]
recFields = [Dom' Term QName]
fields } -> [Dom' Term QName] -> TCM [Dom' Term QName]
forall a. a -> TCMT IO a
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 :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
getRecordConstructor :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
r = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead
-> (RecordData -> ConHead) -> RecordData -> ConHead
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordData -> ConHead
_recConHead (RecordData -> ConHead) -> m RecordData -> m ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m RecordData
forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r

-- | 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 :: (HasCallStack, PureTCM m) => Type -> m (Maybe (QName, Args, RecordData))
isRecordType :: forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType Type
t = (Blocked Type -> Maybe (QName, Args, RecordData))
-> ((QName, Args, RecordData) -> Maybe (QName, Args, RecordData))
-> Either (Blocked Type) (QName, Args, RecordData)
-> Maybe (QName, Args, RecordData)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (QName, Args, RecordData)
-> Blocked Type -> Maybe (QName, Args, RecordData)
forall a b. a -> b -> a
const Maybe (QName, Args, RecordData)
forall a. Maybe a
Nothing) (QName, Args, RecordData) -> Maybe (QName, Args, RecordData)
forall a. a -> Maybe a
Just (Either (Blocked Type) (QName, Args, RecordData)
 -> Maybe (QName, Args, RecordData))
-> m (Either (Blocked Type) (QName, Args, RecordData))
-> m (Maybe (QName, Args, RecordData))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Either (Blocked Type) (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Either (Blocked Type) (QName, Args, RecordData))
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 :: (HasCallStack, PureTCM m) => Type -> m (Either (Blocked Type) (QName, Args, RecordData))
tryRecordType :: forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Either (Blocked Type) (QName, Args, RecordData))
tryRecordType Type
t = Type
-> (Blocker
    -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> (NotBlocked
    -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> m (Either (Blocked Type) (QName, Args, RecordData))
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, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, RecordData)
 -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> Either (Blocked Type) (QName, Args, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
forall a b. a -> Either a b
Left (Blocked Type -> Either (Blocked Type) (QName, Args, RecordData))
-> Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
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, RecordData)))
 -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> (NotBlocked
    -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
nb Type
t -> do
  let no :: m (Either (Blocked Type) (QName, Args, RecordData))
no = Either (Blocked Type) (QName, Args, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, RecordData)
 -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> Either (Blocked Type) (QName, Args, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
forall a b. a -> Either a b
Left (Blocked Type -> Either (Blocked Type) (QName, Args, RecordData))
-> Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
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 = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
      m (Maybe RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
-> (RecordData
    -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r) m (Either (Blocked Type) (QName, Args, RecordData))
no ((RecordData
  -> m (Either (Blocked Type) (QName, Args, RecordData)))
 -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> (RecordData
    -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ \ RecordData
def -> Either (Blocked Type) (QName, Args, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked Type) (QName, Args, RecordData)
 -> m (Either (Blocked Type) (QName, Args, RecordData)))
-> Either (Blocked Type) (QName, Args, RecordData)
-> m (Either (Blocked Type) (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ (QName, Args, RecordData)
-> Either (Blocked Type) (QName, Args, RecordData)
forall a b. b -> Either a b
Right (QName
r,Args
vs,RecordData
def)
    Term
_ -> m (Either (Blocked Type) (QName, Args, RecordData))
no

-- | Get the original projection info for name.
{-# SPECIALIZE origProjection :: HasCallStack => QName -> TCM (QName, Definition, Maybe Projection) #-}
origProjection ::  (HasCallStack, HasConstInfo m) => QName -> m (QName, Definition, Maybe Projection)
origProjection :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f = do
  def <- QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
  let proj     = Definition -> Maybe Projection
isProjectionDefinition Definition
def
      fallback = (QName, Definition, Maybe Projection)
-> m (QName, Definition, Maybe Projection)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Definition
def, Maybe Projection
proj)
  caseMaybe proj fallback $
    \ 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
        def <- QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f'
        return (f', def, isProjectionDefinition 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 :: forall (m :: * -> *). PureTCM m => 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).
  (f, def, mp) <- QName -> m (QName, Definition, Maybe Projection)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f
  let a = Definition -> Type
defType Definition
def
  -- if @f@ is not a projection (like) function, @a@ is the correct type
      fallback = Maybe Type -> m (Maybe Type)
forall a. a -> m a
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
  reportSDoc "tc.deftype" 20 $ vcat
    [ "definition   f =" <+> prettyTCM f <+> text ("  -- raw: " ++ prettyShow f)
    , "has type     a =" <+> prettyTCM a
    , "principal    t =" <+> prettyTCM t <+> "-- raw:" <+> pretty t
    , "instantiated t =" <+> (pretty =<< instantiate t)
    , "reduced      t =" <+> (pretty =<< reduce t)
    ]
  caseMaybe mp fallback $
    \ (Projection{ projIndex :: Projection -> Int
projIndex = Int
n }) -> if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then m (Maybe Type)
fallback else do
      -- otherwise, we have to instantiate @a@ to the "parameters" of @f@
      let npars :: Int
npars | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Int
forall a. HasCallStack => a
__IMPOSSIBLE__
                | Bool
otherwise = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
      [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.deftype" Int
20 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"projIndex    = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
      -- we get the parameters from type @t@
      Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) m Term -> (Term -> m (Maybe Type)) -> m (Maybe Type)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        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 = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims (Elims -> Args) -> Elims -> Args
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
take Int
npars Elims
es
            [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.deftype" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"head d     = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
d
              , TCMT IO Doc
"parameters =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
pars)
              ]
            [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.deftype" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"parameters = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
pars
            if Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
pars Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
npars then [Char] -> m (Maybe Type)
failure [Char]
"does not supply enough parameters"
            else do
              t <- Type
a Type -> Args -> m Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
Type -> a -> m Type
`piApplyM` Args
pars
              reportSDoc "tc.deftype" 20 $ "t = " <+> pretty t
              pure $ Just t
        Term
_ -> m (Maybe Type)
failNotDef
  where
    failNotElig :: m (Maybe Type)
failNotElig = [Char] -> m (Maybe Type)
failure [Char]
"is not eligible for projection-likeness"
    failNotDef :: m (Maybe Type)
failNotDef  = [Char] -> m (Maybe Type)
failure [Char]
"is not a Def."
    failure :: [Char] -> m (Maybe Type)
failure [Char]
reason = do
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.deftype" Int
25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"Def. " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is projection(like)"
        , TCMT IO Doc
"but the type "
        , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"of its argument " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
reason
        ]
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.deftype" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
      Maybe Type -> m (Maybe Type)
forall a. a -> m a
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
$ case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Dummy{} -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
HasCallStack => Type
__DUMMY_TYPE__
        Term
_       -> Maybe Type
forall a. Maybe a
Nothing

-- | Apply a projection to an expression with a known type, returning
--   the type of the projected value.
--   The given type should either be a record type or a type eligible for
--   the principal argument of a projection-like function.
shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m)
                    => Term -> Type -> ProjOrigin -> QName -> m Type
-- shouldBeProjectible t f = maybe failure return =<< projectionType t f
shouldBeProjectible :: forall (m :: * -> *).
(PureTCM m, MonadTCError m, MonadBlock m) =>
Term -> Type -> ProjOrigin -> QName -> m Type
shouldBeProjectible Term
v Type
t ProjOrigin
o QName
f = do
  t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  projectTyped v t o f >>= \case
    Just (Dom' Term Type
_ , Term
_ , Type
ft) -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ft
    Maybe (Dom' Term Type, Term, Type)
Nothing -> case Type
t of
      El Sort' Term
_ Dummy{} -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
HasCallStack => Type
__DUMMY_TYPE__
      Type
_ -> TypeError -> m Type
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m Type) -> TypeError -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
    -- TODO: more accurate error that makes sense also for proj.-like funs.

-- | 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 :: forall (m :: * -> *).
PureTCM m =>
Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
projectTyped Term
v Type
t ProjOrigin
o QName
f = m (Maybe Type)
-> m (Maybe (Dom' Term Type, Term, Type))
-> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> m (Maybe (Dom' Term 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' Term Type, Term, Type)
-> m (Maybe (Dom' Term Type, Term, Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom' Term Type, Term, Type)
forall a. Maybe a
Nothing) ((Type -> m (Maybe (Dom' Term Type, Term, Type)))
 -> m (Maybe (Dom' Term Type, Term, Type)))
-> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> m (Maybe (Dom' Term Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ \ Type
tf -> do
  Type
-> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> (Dom' Term Type
    -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> m (Maybe (Dom' Term Type, Term, Type))
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
ifNotPiType Type
tf (m (Maybe (Dom' Term Type, Term, Type))
-> Type -> m (Maybe (Dom' Term Type, Term, Type))
forall a b. a -> b -> a
const (m (Maybe (Dom' Term Type, Term, Type))
 -> Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> m (Maybe (Dom' Term Type, Term, Type))
-> Type
-> m (Maybe (Dom' Term Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ Maybe (Dom' Term Type, Term, Type)
-> m (Maybe (Dom' Term Type, Term, Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom' Term Type, Term, Type)
forall a. Maybe a
Nothing) {- else -} ((Dom' Term Type
  -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
 -> m (Maybe (Dom' Term Type, Term, Type)))
-> (Dom' Term Type
    -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
-> m (Maybe (Dom' Term Type, Term, Type))
forall a b. (a -> b) -> a -> b
$ \ Dom' Term Type
dom Abs Type
b -> do
  u <- ProjOrigin -> QName -> Arg Term -> m Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v)
  return $ Just (dom, u, b `absApp` v)

-- | Typing of an elimination.

data ElimType
  = ArgT (Dom Type)           -- ^ Type of the argument.
  | ProjT
    { ElimType -> Dom' Term 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 :: forall (m :: * -> *). MonadPretty m => ElimType -> m Doc
prettyTCM (ArgT Dom' Term Type
a)    = Dom' Term Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
prettyTCM Dom' Term Type
a
  prettyTCM (ProjT Dom' Term Type
a Type
b) =
    m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Dom' Term Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
prettyTCM Dom' Term 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
forall (m :: * -> *). MonadPretty m => Type -> 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeElims Type
a Term
self (Elim
e : Elims
es) = do
  case Elim
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' Term Type -> Abs Type -> TCM [ElimType])
-> TCM [ElimType]
forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type
-> (Type -> tcm a)
-> (Dom' Term Type -> Abs Type -> tcm a)
-> tcm a
ifNotPiOrPathType Type
a Type -> TCM [ElimType]
forall a. HasCallStack => a
__IMPOSSIBLE__ {- else -} ((Dom' Term Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType])
-> (Dom' Term Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType]
forall a b. (a -> b) -> a -> b
$ \ Dom' Term Type
a Abs Type
b -> do
      (Dom' Term Type -> ElimType
ArgT Dom' Term 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 (SubstArg Type) -> SubstArg Type
forall e. Arg e -> e
unArg Arg Term
Arg (SubstArg Type)
v) (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) Elims
es
    Proj ProjOrigin
o QName
f -> do
      a <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
      (dom, self, a) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self a o f
      (ProjT dom a :) <$> typeElims a self es
    IApply{} -> TCM [ElimType]
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Given a term with a given type and a list of eliminations, returning the
--   type of the term applied to the eliminations.
eliminateType :: (PureTCM m) => m Empty -> Term -> Type -> Elims -> m Type
eliminateType :: forall (m :: * -> *).
PureTCM m =>
m Empty -> Term -> Type -> Elims -> m Type
eliminateType m Empty
err = m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
forall (m :: * -> *).
PureTCM m =>
m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
eliminateType' m Empty
err ((Elims -> Term) -> Type -> Elims -> m Type)
-> (Term -> Elims -> Term) -> Term -> Type -> Elims -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE

eliminateType' :: (PureTCM m) => m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
eliminateType' :: forall (m :: * -> *).
PureTCM m =>
m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
eliminateType' m Empty
err Elims -> Term
hd Type
t [] = Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
eliminateType' m Empty
err Elims -> Term
hd Type
t (Elim
e : Elims
es) = case Elim
e of
  Apply Arg Term
v -> do
    t' <- m Empty -> Type -> Arg Term -> m Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t Arg Term
v
    eliminateType' err (hd . (e:)) t' es
  Proj ProjOrigin
o QName
f -> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t m Type -> (Type -> m (Maybe Type)) -> m (Maybe Type)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f m (Maybe Type) -> (Maybe Type -> m Type) -> m Type
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Type
a -> Type
-> (Type -> m Type)
-> (Dom' Term Type -> Abs Type -> m Type)
-> m Type
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
ifNotPiType Type
a (\Type
_ -> Empty -> Type
forall a. Empty -> a
absurd (Empty -> Type) -> m Empty -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Empty
err) ((Dom' Term Type -> Abs Type -> m Type) -> m Type)
-> (Dom' Term Type -> Abs Type -> m Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Dom' Term Type
_ Abs Type
c ->
      m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
forall (m :: * -> *).
PureTCM m =>
m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
eliminateType' m Empty
err (Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) (Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` (Elims -> Term
hd [])) Elims
es
    Maybe Type
Nothing -> Empty -> Type
forall a. Empty -> a
absurd (Empty -> Type) -> m Empty -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Empty
err
  IApply Term
_ Term
_ Term
r -> do
    t' <- m Empty -> Type -> Term -> m Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t Term
r
    eliminateType' err (hd . (e:)) t' es

-- | Check if a name refers to an eta expandable record.
{-# SPECIALIZE isEtaRecord :: HasCallStack => QName -> TCM Bool #-}
{-# SPECIALIZE isEtaRecord :: HasCallStack => QName -> ReduceM Bool #-}
isEtaRecord :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaRecord :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaRecord QName
r = do
  QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r m (Maybe RecordData) -> (Maybe RecordData -> m Bool) -> m Bool
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just RecordData
r | RecordData -> Bool
isEtaRecordDef RecordData
r -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Maybe RecordData
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

isEtaRecordDef :: RecordData -> Bool
isEtaRecordDef :: RecordData -> Bool
isEtaRecordDef RecordData
r = RecordData -> HasEta
_recEtaEquality RecordData
r HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
forall a. HasEta' a
YesEta

{-# INLINE isEtaCon #-}
isEtaCon :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaCon :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaCon QName
c = Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, RecordData) -> Bool)
-> m (Maybe (QName, RecordData)) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor QName
c

-- | Going under one of these does not count as a decrease in size for the termination checker.
isEtaOrCoinductiveRecordConstructor :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaOrCoinductiveRecordConstructor :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c =
  m (Maybe (QName, RecordData))
-> m Bool -> ((QName, RecordData) -> 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, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c) (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (((QName, RecordData) -> m Bool) -> m Bool)
-> ((QName, RecordData) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ (QName
_, RecordData
def) ->
    Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordData -> Bool
isEtaRecordDef RecordData
def) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M`
      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordData -> Maybe Induction
_recInduction RecordData
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 :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isInductiveRecord :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isInductiveRecord QName
r = Bool -> (RecordData -> Bool) -> Maybe RecordData -> 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)
-> (RecordData -> Maybe Induction) -> RecordData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordData -> Maybe Induction
_recInduction) (Maybe RecordData -> Bool) -> m (Maybe RecordData) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r

-- | Check if a type is an eta expandable record and return the record identifier and the parameters.
isEtaRecordType :: (HasCallStack, HasConstInfo m)
  => Type
  -> m (Maybe (QName, Args))
isEtaRecordType :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
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 = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims 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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaRecord QName
d) (Maybe (QName, Args) -> m (Maybe (QName, Args))
forall a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe (QName, RecordData))
isRecordConstructor :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c = QName -> m (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c m (Either SigError Definition)
-> (Either SigError Definition -> m (Maybe (QName, RecordData)))
-> m (Maybe (QName, RecordData))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left (SigUnknown [Char]
err)     -> [Char] -> m (Maybe (QName, RecordData))
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
err
  Left SigError
SigAbstract          -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, RecordData)
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 } -> (RecordData -> (QName, RecordData))
-> Maybe RecordData -> Maybe (QName, RecordData)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName
r,) (Maybe RecordData -> Maybe (QName, RecordData))
-> m (Maybe RecordData) -> m (Maybe (QName, RecordData))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r
    Defn
_                          -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, RecordData)
forall a. Maybe a
Nothing

isEtaRecordConstructor :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor :: forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor QName
c = QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c m (Maybe (QName, RecordData))
-> (Maybe (QName, RecordData) -> m (Maybe (QName, RecordData)))
-> m (Maybe (QName, RecordData))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Maybe (QName, RecordData)
Nothing -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, RecordData)
forall a. Maybe a
Nothing
  Just (QName
d, RecordData
def) -> if RecordData -> Bool
isEtaRecordDef RecordData
def then Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (QName, RecordData) -> m (Maybe (QName, RecordData)))
-> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a b. (a -> b) -> a -> b
$ (QName, RecordData) -> Maybe (QName, RecordData)
forall a. a -> Maybe a
Just (QName
d, RecordData
def) else Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, RecordData)
forall a. Maybe a
Nothing

-- | 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 = QName -> (EtaEquality -> EtaEquality) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta QName
q \ EtaEquality
eta -> EtaEquality -> HasEta -> EtaEquality
setEtaEquality EtaEquality
eta (HasEta -> EtaEquality) -> HasEta -> EtaEquality
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta
forall a. a -> HasEta' a
NoEta PatternOrCopattern
pat

-- | Turn on eta for non-recursive and inductive guarded recursive records,
--   unless user declared otherwise.
--   Projections do not preserve guardedness.
updateEtaForRecord :: QName -> TCM ()
updateEtaForRecord :: QName -> TCMT IO ()
updateEtaForRecord QName
q = TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO 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 we need to switch on eta for record q?
  switchEta <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef TCMT IO Defn -> (Defn -> Bool) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Record{ recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality
eta }
      | 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 -> Bool
True
      | Bool
otherwise -> Bool
False
    Defn
_ -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

  when switchEta $ modifyRecEta q $ const $ Inferred YesEta

-- | Turn on eta for inductive guarded recursive records.
--   Projections do not preserve guardedness.
recursiveRecord :: QName -> TCM ()
recursiveRecord :: QName -> TCMT IO ()
recursiveRecord = QName -> TCMT IO ()
updateEtaForRecord

-- | Turn on eta for non-recursive record, unless user declared otherwise.
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord :: QName -> TCMT IO ()
nonRecursiveRecord = QName -> TCMT IO ()
updateEtaForRecord

-- | Check whether record type is marked as recursive.
--
--   Precondition: record type identifier exists in signature.
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord :: QName -> TCMT IO Bool
isRecursiveRecord QName
q =
  Getter TCState (Maybe Definition) -> TCMT IO (Maybe Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Maybe Definition -> f (Maybe Definition))
    -> Signature -> f Signature)
-> (Maybe Definition -> f (Maybe Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Lens' Signature (Maybe (IxValue Signature))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Signature
QName
q) TCMT IO (Maybe Definition)
-> (Maybe Definition -> Maybe Defn) -> TCMT IO (Maybe Defn)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Definition -> Defn) -> Maybe Definition -> Maybe Defn
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Definition -> Defn
theDef TCMT IO (Maybe Defn) -> (Maybe Defn -> Bool) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Just (RecordDefn RecordData
r) -> RecordData -> Bool
recRecursive_ RecordData
r
    Maybe Defn
_ -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

{- | @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 :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar Int
i = ((Telescope, Substitution, Substitution, Telescope)
 -> (Telescope, Substitution, Substitution))
-> Maybe (Telescope, Substitution, Substitution, Telescope)
-> Maybe (Telescope, Substitution, Substitution)
forall a b. (a -> b) -> Maybe a -> Maybe b
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
  Int
-> Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar Int
i (Telescope
 -> TCMT
      IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> TCMT IO Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (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 :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar :: forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar Int
i Telescope
gamma0 = do
  -- Get the context with last variable added last in list.
  let gamma :: [Dom (RawName, Type)]
gamma = Telescope -> [Dom (RawName, Type)]
forall t. Tele (Dom t) -> [Dom (RawName, t)]
telToList Telescope
gamma0
  -- Convert the de Bruijn index i to a de Bruijn level
      l :: Int
l     = [Dom (RawName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (RawName, Type)]
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i
  -- Extract type of @i@th de Bruijn index.
  -- Γ = Γ₁, x:a, Γ₂
  let ([Dom (RawName, Type)]
gamma1, dom :: Dom (RawName, Type)
dom@(Dom (RawName, Type) -> (RawName, Type)
forall t e. Dom' t e -> e
unDom -> (RawName
x, Type
a)) : [Dom (RawName, Type)]
gamma2) = Int
-> [Dom (RawName, Type)]
-> ([Dom (RawName, Type)], [Dom (RawName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
l [Dom (RawName, Type)]
gamma -- TODO:: Defined but not used dom
  -- This must be a eta-expandable record type.
  let failure :: m (Maybe (Telescope, Substitution, Substitution, Telescope))
failure = do
        [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"failed to eta-expand variable " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> RawName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RawName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCMT IO Doc
" since its type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCMT IO Doc
" is not a record type"
        Maybe (Telescope, Substitution, Substitution, Telescope)
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. Maybe a
Nothing
  m (Maybe (QName, Args, RecordData))
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
-> ((QName, Args, RecordData)
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> m (Maybe (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType Type
a) m (Maybe (Telescope, Substitution, Substitution, Telescope))
failure (((QName, Args, RecordData)
  -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
 -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> ((QName, Args, RecordData)
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars, RecordData
def) -> case RecordData -> Bool
isEtaRecordDef RecordData
def of
    Bool
False -> Maybe (Telescope, Substitution, Substitution, Telescope)
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. Maybe a
Nothing
    Bool
True  -> (Telescope, Substitution, Substitution, Telescope)
-> Maybe (Telescope, Substitution, Substitution, Telescope)
forall a. a -> Maybe a
Just ((Telescope, Substitution, Substitution, Telescope)
 -> Maybe (Telescope, Substitution, Substitution, Telescope))
-> m (Telescope, Substitution, Substitution, Telescope)
-> m (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 = RecordData -> Telescope
_recTel RecordData
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
          m :: Int
m   = Telescope -> Int
forall a. Sized a => a -> Int
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
$ RecordData -> [Dom' Term QName]
_recFields RecordData
def
      -- Construct the record pattern @Γ₁, Γ' ⊢ u := c ys@.
          ys :: Args
ys  = (Arg QName -> Int -> Arg Term) -> [Arg QName] -> [Int] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\ Arg QName
f Int
i -> Arg QName
f Arg QName -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [Arg QName]
fs ([Int] -> Args) -> [Int] -> Args
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
m
          u :: Term
u   = ConHead -> ConInfo -> Args -> Term
mkCon (RecordData -> ConHead
_recConHead RecordData
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
$ Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
m
      -- @Γ₁, Γ', Γ₂ ⊢ τ₀ : Γ₁, x:_, Γ₂@
          tau :: Substitution
tau  = Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS ([Dom (RawName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (RawName, Type)]
gamma2) Substitution
tau0

      --  Fields are in order first-first.
          zs :: Args
zs  = [Arg QName]
fs [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap \ QName
f -> Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim
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
++# Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1
      -- @Γ₁, x:_, Γ₂ ⊢ σ₀ : Γ₁, Γ', Γ₂@
          sigma :: Substitution
sigma  = Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS ([Dom (RawName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (RawName, Type)]
gamma2) Substitution
sigma0

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

          -- Use "f(x)" as variable name for the projection f(x).
          s :: RawName
s     = [Char] -> RawName
TS.pack ([Char] -> RawName) -> [Char] -> RawName
forall a b. (a -> b) -> a -> b
$ RawName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow RawName
x
          tel' :: Telescope
tel'  = (RawName -> RawName) -> Telescope -> Telescope
forall a. (RawName -> RawName) -> Tele a -> Tele a
mapAbsNames (\ RawName
f -> RawName -> RawName
stringToArgName (RawName -> RawName) -> RawName -> RawName
forall a b. (a -> b) -> a -> b
$ RawName -> RawName
argNameToString RawName
f RawName -> RawName -> RawName
forall a. Semigroup a => a -> a -> a
<> RawName
"(" RawName -> RawName -> RawName
forall a. Semigroup a => a -> a -> a
<> RawName
s RawName -> RawName -> RawName
forall a. Semigroup a => a -> a -> a
<> RawName
")") Telescope
tel
          delta :: Telescope
delta = [Dom (RawName, Type)] -> Telescope
telFromList ([Dom (RawName, Type)] -> Telescope)
-> [Dom (RawName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ [Dom (RawName, Type)]
gamma1 [Dom (RawName, Type)]
-> [Dom (RawName, Type)] -> [Dom (RawName, Type)]
forall a. [a] -> [a] -> [a]
++ Telescope -> [Dom (RawName, Type)]
forall t. Tele (Dom t) -> [Dom (RawName, t)]
telToList Telescope
tel' [Dom (RawName, Type)]
-> [Dom (RawName, Type)] -> [Dom (RawName, Type)]
forall a. [a] -> [a] -> [a]
++
                    Telescope -> [Dom (RawName, Type)]
forall t. Tele (Dom t) -> [Dom (RawName, 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 (RawName, Type)] -> Telescope
telFromList [Dom (RawName, 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)
-> m (Telescope, Substitution, Substitution, Telescope)
forall a. a -> m a
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 :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [] Telescope
gamma = (Telescope, Substitution, Substitution)
-> TCM (Telescope, Substitution, Substitution)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma, Substitution
forall a. Substitution' a
idS, Substitution
forall a. Substitution' a
idS)
expandRecordVarsRecursively (Int
i : [Int]
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 (Int
-> Telescope
-> TCMT
     IO (Maybe (Telescope, Substitution, Substitution, Telescope))
forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar Int
i Telescope
gamma) ([Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [Int]
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 :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
        newis :: [Int]
newis = Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
    (gamma2, sigma2, tau2) <- [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively ([Int]
newis [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
is) Telescope
gamma1
    -- Γ₁ ⊢ σ₂ : Γ₂  and  Γ₂ ⊢ τ₂ : Γ₁
    return (gamma2, applySubst sigma1 sigma2, applySubst tau2 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 -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt Type
t Int
n = do
  -- first, strip the leading n domains (which remain unchanged)
  TelV gamma core <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
n Type
t
  case unEl core of
    -- There should be at least one domain left
    Pi Dom' Term Type
dom Abs Type
b -> do
      let ai :: ArgInfo
ai = Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
          a :: Type
a = Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom
      -- 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.
      (r, pars, def) <- (QName, Args, RecordData)
-> Maybe (QName, Args, RecordData) -> (QName, Args, RecordData)
forall a. a -> Maybe a -> a
fromMaybe (QName, Args, RecordData)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Args, RecordData) -> (QName, Args, RecordData))
-> TCMT IO (Maybe (QName, Args, RecordData))
-> TCMT IO (QName, Args, RecordData)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType Type
a
      if | NoEta _ <- _recEtaEquality def -> __IMPOSSIBLE__
         | otherwise -> return ()
      -- TODO: compose argInfo ai with tel.
      let tel = RecordData -> Telescope
_recTel RecordData
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars
          m   = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
          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
$ RecordData -> [Dom' Term QName]
_recFields RecordData
def
          ys  = (Arg QName -> Int -> Arg Term) -> [Arg QName] -> [Int] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg QName
f Int
i -> Arg QName
f Arg QName -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [Arg QName]
fs ([Int] -> Args) -> [Int] -> Args
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
m
          u   = ConHead -> ConInfo -> Args -> Term
mkCon (KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ RecordData -> ConHead
_recConHead RecordData
def) ConInfo
ConOSystem Args
ys
          b'  = Int -> Abs Type -> Abs Type
forall a. Subst a => Int -> a -> a
raise Int
m Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
          t'  = Telescope
gamma Telescope -> Type -> Type
`telePi` (Telescope
tel Telescope -> Type -> Type
`telePi` Type
b')
          gammai = (Dom (RawName, Type) -> ArgInfo)
-> [Dom (RawName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map' Dom (RawName, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo ([Dom (RawName, Type)] -> [ArgInfo])
-> [Dom (RawName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (RawName, Type)]
forall t. Tele (Dom t) -> [Dom (RawName, t)]
telToList Telescope
gamma
          xs  = Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Int -> Arg Term) -> [ArgInfo] -> [Int] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ ArgInfo
ai Int
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
$! Int -> Term
var Int
i) [ArgInfo]
gammai [Int
m..]
          curry Term
v = Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                      Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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  = [Arg QName]
fs [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap \ QName
f -> Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
          uncurry Term
v = Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam (Dom' Term Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
dom) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ RawName -> Term -> Abs Term
forall a. RawName -> a -> Abs a
Abs (Abs Type -> RawName
forall a. Abs a -> RawName
absName Abs Type
b) (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
                        Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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)
      return (curry, uncurry, 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 : Type 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)
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
etaExpandRecord :: forall (m :: * -> *).
HasConstInfo m =>
QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
forall (m :: * -> *).
HasConstInfo 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)
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
forceEtaExpandRecord :: forall (m :: * -> *).
HasConstInfo m =>
QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
forall (m :: * -> *).
HasConstInfo m =>
Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' Bool
True

-- | Eta-expand a value at the given record type (must match).
etaExpandRecord' :: (HasConstInfo m)
  => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
  -> QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
etaExpandRecord' :: forall (m :: * -> *).
HasConstInfo m =>
Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' Bool
forceEta QName
r Args
pars Term
u = do
  def <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> m (Maybe RecordData) -> m RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r
  (tel, _, _, args) <- etaExpandRecord'_ forceEta r pars def u
  return (tel, args)

-- | Eta-expand a value at the given eta record type (must match).
etaExpandRecord_ :: HasConstInfo m
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> RecordData  -- ^ Definition of record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, ConHead, ConInfo, Args)
     -- ^ Field types instantiated to parameters, disassembled constructor term.
etaExpandRecord_ :: forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ = Bool
-> QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
False

-- | Eta-expand a value at the given record type (must match).
etaExpandRecord'_ :: HasConstInfo m
  => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
  -> QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> RecordData  -- ^ Definition of record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, ConHead, ConInfo, Args)
     -- ^ Field types instantiated to parameters, disassembled constructor term.
etaExpandRecord'_ :: forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
forceEta QName
r Args
pars
    def :: RecordData
def@RecordData{ _recConHead :: RecordData -> ConHead
_recConHead = ConHead
con, _recFields :: RecordData -> [Dom' Term QName]
_recFields = [Dom' Term QName]
xs, _recTel :: RecordData -> Telescope
_recTel = Telescope
tel }
    Term
u = do
  let 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (RecordData -> HasEta
_recEtaEquality RecordData
def HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
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 = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims 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
        [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"etaExpandRecord_: the following two constructors should be identical"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"r    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
r
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"con  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ConHead
con
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"con_ =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ConHead
con_
          ]
        m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Telescope, ConHead, ConInfo, Args)
-> m (Telescope, ConHead, ConInfo, Args)
forall a. a -> m a
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' = [Dom' Term QName]
xs [Dom' Term QName] -> (Dom' Term QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Monad m => m a -> (a -> b) -> m b
<&!> \Dom' Term QName
dom ->
            Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term QName
dom Arg QName -> (QName -> Term) -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \QName
x -> Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.record.eta" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"eta expanding" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"tel' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel'
          , TCMT IO Doc
"args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
xs'
          ]
        ]
      (Telescope, ConHead, ConInfo, Args)
-> m (Telescope, ConHead, ConInfo, Args)
forall a. a -> m a
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
  (r, pars, def) <- (QName, Args, RecordData)
-> Maybe (QName, Args, RecordData) -> (QName, Args, RecordData)
forall a. a -> Maybe a -> a
fromMaybe (QName, Args, RecordData)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Args, RecordData) -> (QName, Args, RecordData))
-> TCMT IO (Maybe (QName, Args, RecordData))
-> TCMT IO (QName, Args, RecordData)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType Type
t
  (tel, con, ci, args) <- etaExpandRecord_ r pars def u
  return (tel, mkCon con ci 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@.

--   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 :: forall (m :: * -> *).
HasConstInfo m =>
QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord QName
r ConHead
c ConInfo
ci Args
args = do
  RecordData{ _recFields = xs } <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> m (Maybe RecordData) -> m RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r
  reportSDoc "tc.record.eta.contract" 20 $ vcat
    [ "eta contracting record"
    , nest 2 $ vcat
      [ "record type r  =" <+> prettyTCM r
      , "constructor c  =" <+> prettyTCM c
      , "field names xs =" <+> pretty    xs
      , "fields    args =" <+> prettyTCM args
      ]
    ]
  case compare (length args) (length 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 -- András 2026-03-17: TODO optimize
        Just [Maybe Term]
as -> case [Maybe Term] -> [Term]
forall a. [Maybe a] -> [a]
catMaybe' [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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$! 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
    case Term -> Maybe (Elims -> Term, Elims)
hasElims (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) of
      -- if @a@ is the record field name applied to a single argument
      -- then it passes the check
      Just (Elims -> Term
_, []) -> Maybe (Maybe Term)
forall a. Maybe a
Nothing  -- not a projection
      Just (Elims -> Term
h, Elim
e0:Elims
es0)
        | (Elims
es, Proj ProjOrigin
_o QName
f) <- Elim -> Elims -> (Elims, Elim)
forall a. a -> [a] -> ([a], a)
initLast1' Elim
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
      Maybe (Elims -> Term, Elims)
_                 -> Maybe (Maybe Term)
forall a. Maybe a
Nothing

{-# SPECIALIZE isSingletonRecord :: QName -> Args -> TCM Bool #-}
-- | 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   -- ^ Name of record type to check.
  -> Args    -- ^ Parameters given to the record type.
  -> m Bool
isSingletonRecord :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
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 -> Set QName -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
False QName
r Args
ps Set QName
forall a. Monoid a => a
mempty

isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m)
  => QName   -- ^ Name of record type to check.
  -> Args    -- ^ Parameters given to the record type.
  -> m Bool
isSingletonRecordModuloRelevance :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
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 -> Set QName -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
True QName
r Args
ps Set QName
forall a. Monoid a => a
mempty

-- | 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            -- ^ Should disregard irrelevant fields?
  -> QName           -- ^ Name of record type to check.
  -> Args            -- ^ Parameters given to the record type.
  -> Set QName       -- ^ Non-terminating record types we already encountered.
                     --   These are considered as non-singletons,
                     --   otherwise we would construct an infinite inhabitant (in an infinite time...).
  -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
isSingletonRecord' :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
regardIrrelevance QName
r Args
ps Set QName
rs = do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Is" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
ps) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"a singleton record type?"
    , TCMT IO Doc
"  already visited:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM ([QName] -> [TCMT IO Doc]) -> [QName] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
rs)
    ]
  -- Andreas, 2022-03-10, issue #5823
  -- We need to make sure we are not infinitely unfolding records, so we only expand each once,
  -- and keep track of the recursive ones we have already seen.
  if QName
r QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
rs then m (Maybe Term)
forall {a}. m (Maybe a)
no else do
    m (Maybe RecordData)
-> m (Maybe Term)
-> (RecordData -> m (Maybe Term))
-> m (Maybe Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
r) m (Maybe Term)
forall {a}. m (Maybe a)
no ((RecordData -> m (Maybe Term)) -> m (Maybe Term))
-> (RecordData -> m (Maybe Term)) -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ \ RecordData
def -> do
      -- We might not know yet whether a record type is recursive because the positivity checker hasn't run yet.
      -- In this case, we pessimistically consider the record type to be recursive (@True@).
      let recursive :: Bool
recursive = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Bool -> Bool
not (Bool -> Bool) -> ([QName] -> Bool) -> [QName] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> Bool
forall a. Null a => a -> Bool
null) (Maybe [QName] -> Bool) -> Maybe [QName] -> Bool
forall a b. (a -> b) -> a -> b
$ RecordData -> Maybe [QName]
_recMutual RecordData
def
      -- Andreas, 2022-03-23, issue #5823
      -- We may pass through terminating record types as often as we want.
      -- If the termination checker has not run yet, we pessimistically consider the record type
      -- to be non-terminating.
      let nonTerminating :: Bool
nonTerminating = Bool -> (Bool -> Bool) -> Maybe Bool -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Bool -> Bool
not (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ RecordData -> Maybe Bool
_recTerminates RecordData
def
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r, TCMT IO Doc
"is recursive      :", Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
recursive      ]
        , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r, TCMT IO Doc
"is non-terminating:", Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
nonTerminating ]
        ]
      (Args -> Term) -> Maybe Args -> Maybe Term
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ConHead -> ConInfo -> Args -> Term
mkCon (RecordData -> ConHead
_recConHead RecordData
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
<$> do
        Set QName -> Telescope -> m (Maybe Args)
check (Bool -> (Set QName -> Set QName) -> Set QName -> Set QName
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Bool
recursive Bool -> Bool -> Bool
&& Bool
nonTerminating) (QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
r) Set QName
rs) (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ RecordData -> Telescope
_recTel RecordData
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
ps
  where
  -- Check that all entries of the constructor telescope are singletons.
  check :: Set QName -> Telescope -> m (Maybe [Arg Term])
  check :: Set QName -> Telescope -> m (Maybe Args)
check Set QName
rs Telescope
tel = do
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"isSingletonRecord' checking telescope " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
    case Telescope
tel of
      Telescope
EmptyTel -> m (Maybe Args)
forall {a}. m (Maybe [a])
yes
      ExtendTel Dom' Term 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 a. a -> m a
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' Term Type -> m Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Dom' Term Type
dom)
        {-then-}
          (Dom' Term Type
-> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term 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 a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Args -> Args) -> Maybe Args -> Maybe Args
forall a b. (a -> b) -> Maybe a -> Maybe b
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' Term Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term 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
. Set QName -> Telescope -> m (Maybe Args)
check Set QName
rs)
        {-else-} (m (Maybe Args) -> m (Maybe Args))
-> m (Maybe Args) -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ do
          m (Maybe Term)
-> m (Maybe Args) -> (Term -> m (Maybe Args)) -> m (Maybe Args)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Bool -> Type -> Set QName -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
regardIrrelevance (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom) Set QName
rs) m (Maybe Args)
forall {a}. m (Maybe a)
no ((Term -> m (Maybe Args)) -> m (Maybe Args))
-> (Term -> m (Maybe Args)) -> m (Maybe Args)
forall a b. (a -> b) -> a -> b
$ \ Term
v -> do
            Dom' Term Type
-> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term 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 a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Args -> Args) -> Maybe Args -> Maybe Args
forall a b. (a -> b) -> Maybe a -> Maybe b
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' Term Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term 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
. Set QName -> Telescope -> m (Maybe Args)
check Set QName
rs
  no :: m (Maybe a)
no  = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  yes :: m (Maybe [a])
yes = Maybe [a] -> m (Maybe [a])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [a] -> m (Maybe [a])) -> Maybe [a] -> m (Maybe [a])
forall a b. (a -> b) -> a -> b
$ [a] -> Maybe [a]
forall a. a -> Maybe a
Just []

-- | 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 :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> m (Maybe Term)
isSingletonType Type
t = Bool -> Type -> Set QName -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
False Type
t Set QName
forall a. Monoid a => a
mempty

-- | 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 :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance Type
t = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Bool -> Type -> Set QName -> m (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
True Type
t Set QName
forall a. Monoid a => a
mempty

isSingletonType'
  :: forall m. (PureTCM m, MonadBlock m)
  => Bool            -- ^ Should disregard irrelevant fields?
  -> Type            -- ^ Type to check.
  -> Set QName       -- ^ Non-terminating record typess we already encountered.
                     --   These are considered as non-singletons,
                     --   otherwise we would construct an infinite inhabitant (in an infinite time...).
  -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
isSingletonType' :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
regardIrrelevance Type
t Set QName
rs = do
    TelV tel t <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
    t <- abortIfBlocked t
    addContext tel $ do
      let
        -- Easy case: η for records.
        record :: m (Maybe Term)
        record = MaybeT m Term -> m (Maybe Term)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m Term -> m (Maybe Term))
-> MaybeT m Term -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
          (r, ps, def) <- m (Maybe (QName, Args, RecordData))
-> MaybeT m (QName, Args, RecordData)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (QName, Args, RecordData))
 -> MaybeT m (QName, Args, RecordData))
-> m (Maybe (QName, Args, RecordData))
-> MaybeT m (QName, Args, RecordData)
forall a b. (a -> b) -> a -> b
$ Type -> m (Maybe (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType Type
t
          guard $ isEtaRecordDef def
          abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)

        -- Slightly harder case: η for Sub {level} tA phi elt.
        -- tA : Type level, phi : I, elt : Partial phi tA.
        subtype :: m (Maybe Term)
        subtype = MaybeT m Term -> m (Maybe Term)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m Term -> m (Maybe Term))
-> MaybeT m Term -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
          (level, tA, phi, elt) <- m (Maybe (Term, Term, Term, Term))
-> MaybeT m (Term, Term, Term, Term)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (Term, Term, Term, Term))
 -> MaybeT m (Term, Term, Term, Term))
-> m (Maybe (Term, Term, Term, Term))
-> MaybeT m (Term, Term, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type -> m (Maybe (Term, Term, Term, Term))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Term, Term, Term, Term))
isCubicalSubtype Type
t
          subin <- MaybeT $ getBuiltinName' builtinSubIn
          itIsOne <- MaybeT $ getBuiltinName' builtinIsOne
          phiV <- intervalView phi
          case phiV of
            -- If phi = i1, then inS (elt 1=1) is the only inhabitant.
            IntervalView
IOne -> do
              let
                argH :: e -> Arg e
argH = ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> e -> Arg e) -> ArgInfo -> e -> Arg e
forall a b. (a -> b) -> a -> b
$! Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo
                it :: Term
it = Term
elt Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Term
DontCare (QName -> Elims -> Term
Def QName
itIsOne []))]
              Term -> MaybeT m Term
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
subin [] Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argH Term
level, Term -> Arg Term
forall a. a -> Arg a
argH Term
tA, Term -> Arg Term
forall a. a -> Arg a
argH Term
phi, Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
it])
            -- Otherwise we're blocked
            OTerm Term
phi' -> Blocker -> MaybeT m Term
forall a. Blocker -> MaybeT m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
phi')
            -- This fails the MaybeT: we're not looking at a
            -- definitional singleton.
            IntervalView
_ -> MaybeT m Term
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

      (<|>) <$!> record <*!> subtype

{-# SPECIALIZE isEtaVar :: Term -> Type -> TCM (Maybe Int) #-}
-- | 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 :: forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
u Type
a = MaybeT m Int -> m (Maybe Int)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m Int -> m (Maybe Int)) -> MaybeT m Int -> m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG Term
u Type
a Maybe Int
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 Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG Term
u Type
a !Maybe Int
mi [Elim' Int]
es = do
      (u, a) <- (Term, Type) -> MaybeT m (Term, Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Type
a)
      reportSDoc "tc.lhs" 80 $ "isEtaVarG" <+> nest 2 (vcat
        [ "u  = " <+> prettyTCM u
        , "a  = " <+> prettyTCM a
        , "mi = " <+> text (show mi)
        , "es = " <+> prettyList_ (map' (prettyTCM . fmap var) es)
        ])
      case (u, unEl a) of
        (Var Int
i' Elims
es', Term
_) -> do
          Bool -> MaybeT m ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ Maybe Int
mi Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
i' Int -> Maybe Int -> Maybe Int
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Int
mi)
          b <- Int -> MaybeT m Type
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
typeOfBV Int
i'
          areEtaVarElims (var i') b es' es
          return i'
        (Term
_, Def QName
d Elims
pars) -> do
          Bool -> MaybeT m ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaRecord QName
d
          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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
          is <- forM fs $ \QName
f -> do
            let o :: ProjOrigin
o = ProjOrigin
ProjSystem
            (_, _, fa) <- m (Maybe (Dom' Term Type, Term, Type))
-> MaybeT m (Dom' Term Type, Term, Type)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (Dom' Term Type, Term, Type))
 -> MaybeT m (Dom' Term Type, Term, Type))
-> m (Maybe (Dom' Term Type, Term, Type))
-> MaybeT m (Dom' Term Type, Term, Type)
forall a b. (a -> b) -> a -> b
$ Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
projectTyped Term
u Type
a ProjOrigin
o QName
f
            isEtaVarG (u `applyE` [Proj o f]) fa mi (es ++! [Proj o f])
          case (mi, is) of
            (Just Int
i, [Int]
_)     -> Int -> MaybeT m Int
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
            (Maybe Int
Nothing, [])   -> MaybeT m Int
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (Maybe Int
Nothing, Int
i:[Int]
is) -> Bool -> MaybeT m ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i) [Int]
is) MaybeT m () -> MaybeT m Int -> MaybeT m Int
forall a b. MaybeT m a -> MaybeT m b -> MaybeT m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> MaybeT m Int
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
        (Term
_, Pi Dom' Term Type
dom Abs Type
cod) -> Dom' Term Type -> MaybeT m Int -> MaybeT m Int
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Dom' Term Type -> m a -> m a
addContext Dom' Term Type
dom (MaybeT m Int -> MaybeT m Int) -> MaybeT m Int -> MaybeT m Int
forall a b. (a -> b) -> a -> b
$ do
          let u' :: Term
u'  = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
u Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
0]
              a' :: Type
a'  = Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
cod
              mi' :: Maybe Int
mi' = (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Int) -> Maybe Int -> Maybe Int
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Maybe Int
mi
              es' :: [Elim' Int]
es' = ((Elim' Int -> Elim' Int) -> [Elim' Int] -> [Elim' Int]
forall a b. (a -> b) -> [a] -> [b]
map' ((Elim' Int -> Elim' Int) -> [Elim' Int] -> [Elim' Int])
-> ((Int -> Int) -> Elim' Int -> Elim' Int)
-> (Int -> Int)
-> [Elim' Int]
-> [Elim' Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int) -> Elim' Int -> Elim' Int
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Elim' Int]
es [Elim' Int] -> [Elim' Int] -> [Elim' Int]
forall a. [a] -> [a] -> [a]
++! [Arg Int -> Elim' Int
forall a. Arg a -> Elim' a
Apply (Arg Int -> Elim' Int) -> Arg Int -> Elim' Int
forall a b. (a -> b) -> a -> b
$! Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom Arg Type -> Int -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
0]
          (-Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> MaybeT m Int -> MaybeT m Int
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG Term
u' Type
a' Maybe Int
mi' [Elim' Int]
es'
        (Term, Term)
_ -> MaybeT m Int
forall a. MaybeT m a
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' Int] -> MaybeT m ()
areEtaVarElims Term
u Type
a []    []    = () -> MaybeT m ()
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    areEtaVarElims Term
u Type
a []    (Elim' Int
_:[Elim' Int]
_) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Elim
_:Elims
_) []    = MaybeT m ()
forall a. MaybeT m a
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' Int]
es') = do
      Bool -> MaybeT m ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
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'
      a       <- Type -> MaybeT m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
      (_, _, fa) <- MaybeT $ projectTyped u a o f
      areEtaVarElims (u `applyE` [Proj o f]) fa es 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 Int
_ : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Apply Arg Term
_ : Elims
_ ) (Proj{}  : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Proj{} : Elims
_ ) (IApply{} : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Proj{} : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (Apply  Arg Term
_ : Elims
_ ) (IApply{} : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Apply  Arg Int
_ : [Elim' Int]
_  ) = MaybeT m ()
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    areEtaVarElims Term
u Type
a (IApply{} : Elims
_) (IApply{} : [Elim' Int]
_) = 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 Int
i : [Elim' Int]
es') = do
      Type
-> (Type -> MaybeT m ())
-> (Dom' Term Type -> Abs Type -> MaybeT m ())
-> MaybeT m ()
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term 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 a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero) ((Dom' Term Type -> Abs Type -> MaybeT m ()) -> MaybeT m ())
-> (Dom' Term Type -> Abs Type -> MaybeT m ()) -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ \Dom' Term Type
dom Abs Type
cod -> do
      _ <- Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom) (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Arg Int -> Int
forall e. Arg e -> e
unArg Arg Int
i) []
      areEtaVarElims (u `apply` [fmap var i]) (cod `absApp` var (unArg i)) es es'


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

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

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

instance NormaliseProjP a => NormaliseProjP [a] where
  normaliseProjP :: forall (m :: * -> *). HasConstInfo m => [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
forall (m :: * -> *). HasConstInfo m => a -> m a
normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Arg a) where
  normaliseProjP :: forall (m :: * -> *). HasConstInfo m => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
forall (m :: * -> *). HasConstInfo m => a -> m a
normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Named_ a) where
  normaliseProjP :: forall (m :: * -> *). HasConstInfo m => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse a -> m a
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
forall (m :: * -> *). HasConstInfo m => a -> m a
normaliseProjP

instance NormaliseProjP (Pattern' x) where
  normaliseProjP :: forall (m :: * -> *).
HasConstInfo m =>
Pattern' x -> m (Pattern' x)
normaliseProjP p :: Pattern' x
p@VarP{}        = Pattern' x -> m (Pattern' x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
  normaliseProjP p :: Pattern' x
p@DotP{}        = Pattern' x -> m (Pattern' x)
forall a. a -> m a
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
forall (m :: * -> *).
HasConstInfo m =>
[NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
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
forall (m :: * -> *).
HasConstInfo m =>
[NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
normaliseProjP [NamedArg (Pattern' x)]
ps
  normaliseProjP p :: Pattern' x
p@LitP{}        = Pattern' x -> m (Pattern' x)
forall a. a -> m a
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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m QName
getOriginalProjection QName
d0
  normaliseProjP p :: Pattern' x
p@IApplyP{}     = Pattern' x -> m (Pattern' x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
  normaliseProjP (MaskP Pattern' x
p)       = Pattern' x -> Pattern' x
forall x. Pattern' x -> Pattern' x
MaskP (Pattern' x -> Pattern' x) -> m (Pattern' x) -> m (Pattern' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' x -> m (Pattern' x)
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
forall (m :: * -> *).
HasConstInfo m =>
Pattern' x -> m (Pattern' x)
normaliseProjP Pattern' x
p