{-# LANGUAGE NondecreasingIndentation #-}

module Agda.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 qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap

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

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

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

import Agda.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 ((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
  => A.RecStyle        -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields RecStyle
style 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 (RecStyle
style RecStyle -> RecStyle -> Bool
forall a. Eq a => a -> a -> Bool
== RecStyle
A.RecStyleWhere) (WriterT [RecordFieldWarning] Identity ()
 -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$   -- Don't warn about unknown fields for `record where`
    [(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
$ NonEmpty (Name, Range) -> RecordFieldWarning
W.DuplicateFields
  [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] -> (Arg Name -> a) -> [a]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg Name]
axs ((Arg Name -> a) -> [a]) -> (Arg Name -> a) -> [a]
forall a b. (a -> b) -> a -> b
$ \ Arg Name
ax -> a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (Arg Name -> a
fill Arg Name
ax) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ Name -> [(Name, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
ax) [(Name, a)]
uniq
  where
    ([(Name, a)]
uniq, [(Name, a)]
duplicate) = ((Name, a) -> Name) -> [(Name, a)] -> ([(Name, a)], [(Name, a)])
forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
nubAndDuplicatesOn (Name, a) -> Name
forall a b. (a, b) -> a
fst [(Name, a)]
fs   -- separating duplicate fields
    xs :: [Name]
xs        = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
axs                       -- official fields (accord. record type)
    missing :: [Name]
missing   = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem (((Name, a) -> Name) -> [(Name, a)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, a) -> Name
forall a b. (a, b) -> a
fst [(Name, a)]
fs)) [Name]
xs  -- missing  fields
    alien :: [(Name, a)]
alien     = ((Name, a) -> Bool) -> [(Name, a)] -> [(Name, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Name, a) -> Bool) -> (Name, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs (Name -> Bool) -> ((Name, a) -> Name) -> (Name, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, a) -> Name
forall a b. (a, b) -> a
fst) [(Name, a)]
fs      -- spurious fields
    warn :: (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 :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> (RecordFieldWarning -> Warning)
-> RecordFieldWarning
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> Warning
RecordFieldWarning) [RecordFieldWarning]
ws
  a -> 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 Any)
-> [RecordFieldWarning] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TypeError -> TCMT IO Any
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Any)
-> (RecordFieldWarning -> TypeError)
-> RecordFieldWarning
-> TCMT IO Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> TypeError
recordFieldWarningToError) [RecordFieldWarning]
ws
    -- This will raise the first warning (if any) as error.
  a -> 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
  => A.RecStyle        -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn RecStyle
style 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
$ RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields RecStyle
style 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
  => A.RecStyle        -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsFail RecStyle
style 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
$ RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields RecStyle
style 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
  => A.RecStyle           -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields RecStyle
style 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
<$> RecStyle
-> QName
-> (Arg Name -> Maybe (NamedArg a))
-> [Arg Name]
-> [(Name, Maybe (NamedArg a))]
-> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
forall a.
HasRange a =>
RecStyle
-> QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields RecStyle
style 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 ArgName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> ArgName -> Ranged ArgName
forall a. Range -> a -> Ranged a
Ranged (Arg Name -> Range
forall a. HasRange a => a -> Range
getRange Arg Name
ax) (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
forall a b. (a -> b) -> a -> b
$ Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> ArgName) -> Name -> ArgName
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
  => A.RecStyle           -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn RecStyle
style 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
$ RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields RecStyle
style 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
  => A.RecStyle           -- ^ Braces or where
  -> 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 =>
RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail RecStyle
style 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
$ RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
RecStyle
-> QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields RecStyle
style 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.
{-# SPECIALIZE isRecord :: QName -> TCM (Maybe RecordData) #-}
{-# SPECIALIZE isRecord :: QName -> ReduceM (Maybe RecordData) #-}
isRecord :: HasConstInfo m => QName -> m (Maybe RecordData)
isRecord :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
r = do
  QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r m Definition -> (Definition -> Defn) -> m Defn
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef m Defn -> (Defn -> Maybe RecordData) -> m (Maybe RecordData)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m RecordData
getRecordDef :: forall (m :: * -> *).
(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 :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
r
  where err :: m RecordData
err = TypeError -> m RecordData
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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 :: (HasConstInfo m, ReadTCState m, MonadError TCErr m)
  => QName
  -> m [Dom C.Name]
getRecordFieldNames :: forall (m :: * -> *).
(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 :: * -> *).
(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
<$> Lens' TCState (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' 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
  :: Type  -- ^ Record type.  Need not be reduced.
  -> TCM [Dom QName]
getRecordTypeFields :: 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 => 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 :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
getRecordConstructor :: forall (m :: * -> *).
(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 :: * -> *).
(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 :: PureTCM m => Type -> m (Maybe (QName, Args, RecordData))
isRecordType :: forall (m :: * -> *).
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 :: * -> *).
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 :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, RecordData))
tryRecordType :: forall (m :: * -> *).
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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      m (Maybe 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 :: * -> *).
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 :: QName -> TCM (QName, Definition, Maybe Projection) #-}
origProjection ::  HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
origProjection :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f = do
  def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  let proj     = Defn -> Maybe Projection
isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef 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 => QName -> m Definition
getConstInfo QName
f'
        return (f', def, isProjection_ $ theDef 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 :: * -> *).
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
    ]
  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
      ArgName -> Int -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.deftype" Int
20 (ArgName -> m ()) -> ArgName -> m ()
forall a b. (a -> b) -> a -> b
$ ArgName
"projIndex    = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Int -> ArgName
forall a. Show a => a -> ArgName
show Int
n
      -- we get the parameters from type @t@
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Def QName
d Elims
es -> do
          -- Andreas, 2013-10-22
          -- we need to check this @Def@ is fully reduced.
          -- If it is stuck due to disabled reductions
          -- (because of failed termination check),
          -- we will produce garbage parameters.
          m Bool -> m (Maybe Type) -> m (Maybe Type) -> m (Maybe Type)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike QName
d) m (Maybe Type)
failNotElig (m (Maybe Type) -> m (Maybe Type))
-> m (Maybe Type) -> m (Maybe Type)
forall a b. (a -> b) -> a -> b
$ {- else -} do
            -- now we know it is reduced, we can safely take the parameters
            let pars :: Args
pars = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe Args) -> Elims -> Maybe Args
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
take Int
npars Elims
es
            ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
              [ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"head d     = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
pars)
              ]
            ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 ArgName -> m (Maybe Type)
failure ArgName
"does not supply enough parameters"
            else Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
a Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
`piApplyM` Args
pars
        Term
_ -> m (Maybe Type)
failNotDef
  where
    failNotElig :: m (Maybe Type)
failNotElig = ArgName -> m (Maybe Type)
failure ArgName
"is not eligible for projection-likeness"
    failNotDef :: m (Maybe Type)
failNotDef  = ArgName -> m (Maybe Type)
failure ArgName
"is not a Def."
    failure :: ArgName -> m (Maybe Type)
failure ArgName
reason = do
      ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
        , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"of its argument " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
reason
        ]
      ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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 Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) (Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Elim
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 a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Arg Term -> 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 a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Term -> 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.
--
-- The answer is no for a record type with an erased constructor
-- unless the current quantity is \"erased\".
{-# SPECIALIZE isEtaRecord :: QName -> TCM Bool #-}
{-# SPECIALIZE isEtaRecord :: QName -> ReduceM Bool #-}
isEtaRecord :: HasConstInfo m => QName -> m Bool
isEtaRecord :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r = do
  QName -> m (Maybe RecordData)
forall (m :: * -> *).
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 -> do
     constructorQ <- Definition -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> Quantity) -> m Definition -> m Quantity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName (RecordData -> ConHead
_recConHead RecordData
r))
     currentQ     <- viewTC eQuantity
     return $ constructorQ `moreQuantity` currentQ
    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

{-# SPECIALIZE isEtaCon :: QName -> TCM Bool #-}
isEtaCon :: HasConstInfo m => QName -> m Bool
isEtaCon :: forall (m :: * -> *). 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 :: * -> *).
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 :: HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor :: forall (m :: * -> *). 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 :: * -> *).
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 :: HasConstInfo m => QName -> m Bool
isInductiveRecord :: forall (m :: * -> *). 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 :: * -> *).
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 :: (HasConstInfo m)
  => Type
  -> m (Maybe (QName, Args))
isEtaRecordType :: forall (m :: * -> *).
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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
    m Bool
-> m (Maybe (QName, Args))
-> m (Maybe (QName, Args))
-> m (Maybe (QName, Args))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d) (Maybe (QName, Args) -> m (Maybe (QName, Args))
forall 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 :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
isRecordConstructor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c = QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c m (Either SigError Definition)
-> (Either SigError Definition -> m (Maybe (QName, 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 ArgName
err)     -> m (Maybe (QName, RecordData))
forall a. HasCallStack => a
__IMPOSSIBLE__
  Left SigError
SigCubicalNotErasure -> m (Maybe (QName, RecordData))
forall a. HasCallStack => a
__IMPOSSIBLE__
  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 :: * -> *).
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 :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor QName
c = QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
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 => QName -> m Definition
getConstInfo QName
q TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef TCMT IO Defn -> (Defn -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 =
  TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature TCMT IO Signature
-> (Signature -> Maybe Definition) -> TCMT IO (Maybe Definition)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> QName -> Signature -> Maybe Definition
lookupDefinition QName
q TCMT IO (Maybe Definition)
-> (Maybe Definition -> Maybe Defn) -> TCMT IO (Maybe Defn)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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' Term (ArgName, Type)]
gamma = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma0
  -- Convert the de Bruijn index i to a de Bruijn level
      l :: Int
l     = [Dom' Term (ArgName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom' Term (ArgName, 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' Term (ArgName, Type)]
gamma1, dom :: Dom' Term (ArgName, Type)
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
x, Type
a)}) : [Dom' Term (ArgName, Type)]
gamma2) = Int
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
l [Dom' Term (ArgName, Type)]
gamma -- TODO:: Defined but not used dom, ai
  -- This must be a eta-expandable record type.
  let failure :: m (Maybe (Telescope, Substitution, Substitution, Telescope))
failure = do
        ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ArgName
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 :: * -> *).
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' Term (ArgName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom' Term (ArgName, Type)]
gamma2) Substitution
tau0

      --  Fields are in order first-first.
          zs :: Args
zs  = [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
f -> 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' Term (ArgName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom' Term (ArgName, Type)]
gamma2) Substitution
sigma0

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

          -- Use "f(x)" as variable name for the projection f(x).
          s :: ArgName
s     = ArgName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow ArgName
x
          tel' :: Telescope
tel'  = (ArgName -> ArgName) -> Telescope -> Telescope
forall a. (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames (\ ArgName
f -> ArgName -> ArgName
stringToArgName (ArgName -> ArgName) -> ArgName -> ArgName
forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName
argNameToString ArgName
f ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"(" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
")") Telescope
tel
          delta :: Telescope
delta = [Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> [Dom' Term (ArgName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)]
gamma1 [Dom' Term (ArgName, Type)]
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a] -> [a]
++ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel' [Dom' Term (ArgName, Type)]
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a] -> [a]
++
                    Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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' Term (ArgName, Type)] -> Telescope
telFromList [Dom' Term (ArgName, 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 :: Dom' Term Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b -> do
      -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
      -- For now, we only eta-expand once.
      -- This might trigger another call to @etaExpandProjectedVar@ later.
      -- A more efficient version does all the eta-expansions at once here.
      (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 :: * -> *).
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' Term (ArgName, Type) -> ArgInfo)
-> [Dom' Term (ArgName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (ArgName, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo ([Dom' Term (ArgName, Type)] -> [ArgInfo])
-> [Dom' Term (ArgName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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
teleLam Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
tel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                      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] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
f -> Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
          atel = Dom' Term (ArgName, Type) -> Telescope
forall a. SgTel a => a -> Telescope
sgTel (Dom' Term (ArgName, Type) -> Telescope)
-> Dom' Term (ArgName, Type) -> Telescope
forall a b. (a -> b) -> a -> b
$ (,) (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) (Type -> (ArgName, Type))
-> Dom' Term Type -> Dom' Term (ArgName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Type
dom
          uncurry Term
v = Telescope -> Term -> Term
teleLam Telescope
gamma (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
atel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                        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 : Set where field x : A; y : B; .z : C@

    and @r : R@,

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

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

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

-- | Eta-expand a value at the given record type (must match).
etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState 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, MonadDebug m, ReadTCState 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 :: * -> *).
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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      -- Andreas, 2019-10-21, issue #4148
      -- @con == con_@ might fail, but their normal forms should be equal.
      m (Maybe QName) -> m () -> m ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (ConHead -> QName
conName ConHead
con QName -> QName -> m (Maybe QName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
`sameDef` ConHead -> QName
conName ConHead
con_) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"con  = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ConHead -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow 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
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"con_ = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ConHead -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow 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' = [Arg QName] -> (Arg QName -> Arg Term) -> Args
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for ((Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
xs) ((Arg QName -> Arg Term) -> Args)
-> (Arg QName -> Arg Term) -> Args
forall a b. (a -> b) -> a -> b
$ (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> Term) -> Arg QName -> Arg Term)
-> (QName -> Term) -> Arg QName -> Arg Term
forall a b. (a -> b) -> a -> b
$ \ QName
x -> Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]
      ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 :: * -> *).
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@.
--
--   If all fields are erased, we cannot eta-contract.

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

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

{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> TCM Term #-}
{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> ReduceM Term #-}
etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord :: forall (m :: * -> *).
HasConstInfo m =>
QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord QName
r ConHead
c ConInfo
ci Args
args = if (Arg Term -> Bool) -> Args -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Arg Term -> Bool) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Bool
forall a. LensModality a => a -> Bool
usableModality) Args
args then m Term
fallBack else do
  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 :: * -> *).
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
        Just [Maybe Term]
as -> case [Maybe Term] -> [Term]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Term]
as of
          (Term
a:[Term]
as) ->
            if (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term
a Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
==) [Term]
as
              then Term -> m Term
forall 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 (ConHead -> ConInfo -> Args -> Term
mkCon ConHead
c ConInfo
ci Args
args)
  check :: Arg Term -> Dom QName -> Maybe (Maybe Term)
  check :: Arg Term -> Dom' Term QName -> Maybe (Maybe Term)
check Arg Term
a Dom' Term QName
ax = do
  -- @a@ is the constructor argument, @ax@ the corr. record field name
    -- skip irrelevant record fields by returning DontCare
    case (Arg Term -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg Term
a, Term -> Maybe (Elims -> Term, Elims)
hasElims (Term -> Maybe (Elims -> Term, Elims))
-> Term -> Maybe (Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) of
      (Irrelevant{}, Maybe (Elims -> Term, Elims)
_)   -> Maybe Term -> Maybe (Maybe Term)
forall a. a -> Maybe a
Just Maybe Term
forall a. Maybe a
Nothing
      -- if @a@ is the record field name applied to a single argument
      -- then it passes the check
      (Relevance
_, Just (Elims -> Term
_, [])) -> Maybe (Maybe Term)
forall a. Maybe a
Nothing  -- not a projection
      (Relevance
_, Just (Elims -> Term
h, Elim
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
      (Relevance, 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
  ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 :: * -> *).
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
      ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
    ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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 :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 :: * -> *).
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 (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
_ -> ArgName -> MaybeT m Term
forall a. ArgName -> MaybeT m a
forall (m :: * -> *) a. MonadFail m => ArgName -> m a
fail ArgName
""

      (<|>) <$> 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 :: * -> *). 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 => 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) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe 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) Maybe Int
mi
              es' :: [Elim' Int]
es' = ((Elim' Int -> Elim' Int) -> [Elim' Int] -> [Elim' Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 [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 :: * -> *). 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