{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Records where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans.Maybe
import Control.Monad.Writer
import Control.Applicative
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 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 ()
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 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
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)
orderFields
:: forall a . HasRange a
=> QName
-> (Arg C.Name -> a)
-> [Arg C.Name]
-> [(C.Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields :: forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = do
[(Name, a)]
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
alien (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {a}.
(MonadWriter b m, Singleton b b, Bifunctor p, HasRange b) =>
([p a Range] -> b) -> [p a b] -> m ()
warn (([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)]
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> [(Name, Range)] -> RecordFieldWarning
W.TooManyFields QName
r [Name]
missing
[(Name, a)]
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
duplicate (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {a}.
(MonadWriter b m, Singleton b b, Bifunctor p, HasRange b) =>
([p a Range] -> b) -> [p a b] -> m ()
warn (([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
-> ([(Name, Range)] -> RecordFieldWarning)
-> [(Name, a)]
-> WriterT [RecordFieldWarning] Identity ()
forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> RecordFieldWarning
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
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
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
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
warn :: ([p a Range] -> b) -> [p a b] -> m ()
warn [p a Range] -> b
w = b -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (b -> m ()) -> ([p a b] -> b) -> [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) -> ([p a b] -> b) -> [p a b] -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [p a Range] -> b
w ([p a Range] -> b) -> ([p a b] -> [p a Range]) -> [p a b] -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p a b -> p a Range) -> [p a b] -> [p a Range]
forall a b. (a -> b) -> [a] -> [b]
map ((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)
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
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
a -> TCMT IO a
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res
orderFieldsWarn
:: forall a . HasRange a
=> QName
-> (Arg C.Name -> a)
-> [Arg C.Name]
-> [(C.Name, a)]
-> TCM [a]
orderFieldsWarn :: forall a.
HasRange a =>
QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = Writer [RecordFieldWarning] [a] -> TCM [a]
forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
-> Writer [RecordFieldWarning] [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs
orderFieldsFail
:: forall a . HasRange a
=> QName
-> (Arg C.Name -> a)
-> [Arg C.Name]
-> [(C.Name, a)]
-> TCM [a]
orderFieldsFail :: forall a.
HasRange a =>
QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsFail QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs = Writer [RecordFieldWarning] [a] -> TCM [a]
forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
-> Writer [RecordFieldWarning] [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> a
fill [Arg Name]
axs [(Name, a)]
fs
insertMissingFields
:: forall a . HasRange a
=> QName
-> (C.Name -> a)
-> [FieldAssignment' a]
-> [Arg C.Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields :: forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs = do
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 ]
[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
<$> QName
-> (Arg Name -> Maybe (NamedArg a))
-> [Arg Name]
-> [(Name, Maybe (NamedArg a))]
-> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
forall a.
HasRange a =>
QName
-> (Arg Name -> a)
-> [Arg Name]
-> [(Name, a)]
-> Writer [RecordFieldWarning] [a]
orderFields QName
r Arg Name -> Maybe (NamedArg a)
fill [Arg Name]
axs [(Name, Maybe (NamedArg a))]
givenFields
where
fill :: Arg C.Name -> Maybe (NamedArg a)
fill :: Arg Name -> Maybe (NamedArg a)
fill Arg Name
ax
| Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
ax = NamedArg a -> Maybe (NamedArg a)
forall a. a -> Maybe a
Just (NamedArg a -> Maybe (NamedArg a))
-> NamedArg a -> Maybe (NamedArg a)
forall a b. (a -> b) -> a -> b
$ Origin -> NamedArg a -> NamedArg a
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (NamedArg a -> NamedArg a) -> NamedArg a -> NamedArg a
forall a b. (a -> b) -> a -> b
$ a -> Named 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
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
insertMissingFieldsWarn
:: forall a . HasRange a
=> QName
-> (C.Name -> a)
-> [FieldAssignment' a]
-> [Arg C.Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn :: forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs =
Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
-> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs
insertMissingFieldsFail
:: forall a . HasRange a
=> QName
-> (C.Name -> a)
-> [FieldAssignment' a]
-> [Arg C.Name]
-> TCM [NamedArg a]
insertMissingFieldsFail :: forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs =
Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
-> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> Writer [RecordFieldWarning] [NamedArg a]
insertMissingFields QName
r Name -> a
placeholder [FieldAssignment' a]
fs [Arg Name]
axs
{-# 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
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 [])
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
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
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 =
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
getRecordTypeFields
:: Type
-> 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
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__
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
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
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
{-# 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 :: PureTCM m => QName -> Type -> m (Maybe Type)
getDefType :: forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t = do
(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
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
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
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Def QName
d Elims
es -> do
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
$ do
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
shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m)
=> Term -> Type -> ProjOrigin -> QName -> m Type
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
projectTyped
:: PureTCM m
=> Term
-> Type
-> ProjOrigin
-> QName
-> 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) ((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)
data ElimType
= ArgT (Dom Type)
| ProjT
{ ElimType -> Dom' Term Type
projTRec :: Dom Type
, ElimType -> Type
projTField :: Type
}
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
TCM.<> 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)
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
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__ ((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__
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
{-# 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
Maybe RecordData
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just RecordData
r -> RecordData -> m Bool
forall (m :: * -> *). HasConstInfo m => RecordData -> m Bool
isEtaRecordDef RecordData
r
isEtaRecordDef :: HasConstInfo m => RecordData -> m Bool
isEtaRecordDef :: forall (m :: * -> *). HasConstInfo m => RecordData -> m 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 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise = 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
{-# 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
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) ->
RecordData -> m Bool
forall (m :: * -> *). HasConstInfo m => RecordData -> m 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)
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
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
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) -> m Bool
-> m (Maybe (QName, RecordData))
-> m (Maybe (QName, RecordData))
-> m (Maybe (QName, RecordData))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (RecordData -> m Bool
forall (m :: * -> *). HasConstInfo m => RecordData -> m Bool
isEtaRecordDef RecordData
def) (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)) (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)
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
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
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
recursiveRecord :: QName -> TCM ()
recursiveRecord :: QName -> TCMT IO ()
recursiveRecord = QName -> TCMT IO ()
updateEtaForRecord
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord :: QName -> TCMT IO ()
nonRecursiveRecord = QName -> TCMT IO ()
updateEtaForRecord
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 :: 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 :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
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
let gamma :: [Dom' Term (ArgName, Type)]
gamma = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma0
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
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
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) -> RecordData -> m Bool
forall (m :: * -> *). HasConstInfo m => RecordData -> m Bool
isEtaRecordDef RecordData
def m Bool
-> (Bool
-> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
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
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
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
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
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
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]
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
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
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)
(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)
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
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
return (gamma2, applySubst sigma1 sigma2, applySubst tau2 tau1)
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt Type
t Int
n = do
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
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
(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 ()
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__
etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m)
=> QName
-> Args
-> Term
-> m (Telescope, Args)
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
forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
=> QName
-> Args
-> Term
-> m (Telescope, Args)
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
etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m)
=> Bool
-> QName
-> Args
-> Term
-> m (Telescope, Args)
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)
etaExpandRecord_ :: HasConstInfo m
=> QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
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
etaExpandRecord'_ :: HasConstInfo m
=> Bool
-> QName
-> Args
-> RecordData
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
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
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
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)
Term
_ -> do
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)
{-# 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
Just RecordData{ _recFields = xs } <- 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
Ordering
GT -> m Term
forall a. HasCallStack => a
__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
Maybe [Maybe Term]
_ -> m Term
fallBack
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
case (Arg Term -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg Term
a, Term -> Maybe (Elims -> Term, Elims)
hasElims (Term -> Maybe (Elims -> Term, Elims))
-> Term -> Maybe (Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) of
(Relevance
Irrelevant, Maybe (Elims -> Term, Elims)
_) -> Maybe Term -> Maybe (Maybe Term)
forall a. a -> Maybe a
Just Maybe Term
forall a. Maybe a
Nothing
(Relevance
_, Just (Elims -> Term
_, [])) -> Maybe (Maybe Term)
forall a. Maybe a
Nothing
(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 #-}
isSingletonRecord :: (PureTCM m, MonadBlock m)
=> QName
-> Args
-> 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
-> Args
-> 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
isSingletonRecord'
:: forall m. (PureTCM m, MonadBlock m)
=> Bool
-> QName
-> Args
-> Set QName
-> m (Maybe Term)
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)
]
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
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
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 :: 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)
(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)
(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 []
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
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
-> Type
-> Set QName
-> m (Maybe Term)
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
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
guardM $ isEtaRecordDef def
abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)
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
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])
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')
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) #-}
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
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 (f :: * -> *). Alternative f => Bool -> f ()
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 :: * -> *).
(Applicative m, MonadFail 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 (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT m ()) -> MaybeT m Bool -> MaybeT m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do QName -> MaybeT m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d
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 (f :: * -> *). Alternative f => Bool -> f ()
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 :: 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 (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
forall a b. (a -> b) -> a -> b
$ QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'
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'
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__
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'
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