{-# 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 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.Either
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.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Impossible
mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon ConHead
h ConInfo
info Args
args = ConHead -> ConInfo -> Elims -> Term
Con ConHead
h ConInfo
info (forall a b. (a -> b) -> [a] -> [b]
map 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
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
alien forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> [(Name, Range)] -> RecordFieldWarning
TooManyFieldsWarning QName
r [Name]
missing
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, a)]
duplicate forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> RecordFieldWarning
DuplicateFieldsWarning
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg Name]
axs forall a b. (a -> b) -> a -> b
$ \ Arg Name
ax -> forall a. a -> Maybe a -> a
fromMaybe (Arg Name -> a
fill Arg Name
ax) forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall e. Arg e -> e
unArg Arg Name
ax) [(Name, a)]
uniq
where
([(Name, a)]
uniq, [(Name, a)]
duplicate) = forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
nubAndDuplicatesOn forall a b. (a, b) -> a
fst [(Name, a)]
fs
xs :: [Name]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
axs
missing :: [Name]
missing = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> a -> Bool
hasElem (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, a)]
fs)) [Name]
xs
alien :: [(Name, a)]
alien = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. [p a Range] -> b
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second 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) = forall w a. Writer w a -> (a, w)
runWriter Writer [RecordFieldWarning] a
comp
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> Warning
RecordFieldWarning) [RecordFieldWarning]
ws
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) = forall w a. Writer w a -> (a, w)
runWriter Writer [RecordFieldWarning] a
comp
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordFieldWarning -> TypeError
recordFieldWarningToError) [RecordFieldWarning]
ws
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 = forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings forall a b. (a -> b) -> a -> b
$ 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 = forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings forall a b. (a -> b) -> a -> b
$ 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 = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
x forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Name]
axs) (forall a. a -> NamedArg a
defaultNamedArg a
e) forall a b. (a -> b) -> a -> b
$ \ Arg Name
a ->
forall c. Arg Name -> c -> Named_ c
nameIfHidden Arg Name
a a
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Name
a
givenFields :: [(Name, Maybe (NamedArg a))]
givenFields = [ (Name
x, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Name -> a -> NamedArg a
arg Name
x a
e) | FieldAssignment Name
x a
e <- [FieldAssignment' a]
fs ]
forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
| forall a. LensHiding a => a -> Bool
visible Arg Name
ax = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> a
placeholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Name
ax
| Bool
otherwise = forall a. Maybe a
Nothing
nameIfHidden :: Arg C.Name -> c -> Named_ c
nameIfHidden :: forall c. Arg Name -> c -> Named_ c
nameIfHidden Arg Name
ax
| forall a. LensHiding a => a -> Bool
visible Arg Name
ax = forall a name. a -> Named name a
unnamed
| Bool
otherwise = forall name a. name -> a -> Named name a
named forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange Arg Name
ax) forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> ArgName
prettyShow forall a b. (a -> b) -> a -> b
$ 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 =
forall a. Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings forall a b. (a -> b) -> a -> b
$ 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 =
forall a. Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings forall a b. (a -> b) -> a -> b
$ 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
getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn
getRecordDef :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r = forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Defn
err forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
where err :: m Defn
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType (forall t a. Sort' t -> a -> Type'' t a
El HasCallStack => Sort
__DUMMY_SORT__ 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 = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
d) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
\ Projection{ projProper :: Projection -> Maybe QName
projProper = Maybe QName
proper, projFromType :: Projection -> Arg QName
projFromType = Arg QName
r} ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg QName
r 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 = Defn -> [Dom Name]
recordFieldNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r
getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m)
=> QName -> m (Maybe [Dom C.Name])
getRecordFieldNames_ :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom Name])
getRecordFieldNames_ QName
r = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Defn -> [Dom Name]
recordFieldNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
recordFieldNames :: Defn -> [Dom C.Name]
recordFieldNames :: Defn -> [Dom Name]
recordFieldNames = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom QName]
recFields
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords :: [Name] -> TCM [QName]
findPossibleRecords [Name]
fields = do
[Definition]
defs <- forall k v. HashMap k v -> [v]
HMap.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' Signature TCState
stSignature forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (HashMap QName Definition) Signature
sigDefinitions)
[Definition]
idefs <- forall k v. HashMap k v -> [v]
HMap.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' Signature TCState
stImports forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (HashMap QName Definition) Signature
sigDefinitions)
ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> ScopeInfo -> Bool
`isNameInScope` ScopeInfo
scope) forall a b. (a -> b) -> a -> b
$ [Definition] -> [QName]
cands [Definition]
defs forall a. [a] -> [a] -> [a]
++ [Definition] -> [QName]
cands [Definition]
idefs
where
cands :: [Definition] -> [QName]
cands [Definition]
defs = [ Definition -> QName
defName Definition
d | Definition
d <- [Definition]
defs, Definition -> Bool
possible Definition
d ]
possible :: Definition -> Bool
possible Definition
def =
case Definition -> Defn
theDef Definition
def of
Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Name
given forall a b. (a -> b) -> a -> b
$
forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
Defn
_ -> Bool
False
given :: Set Name
given = forall a. Ord a => [a] -> Set a
Set.fromList [Name]
fields
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes QName
r = Defn -> Telescope
recTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r
getRecordTypeFields
:: Type
-> TCM [Dom QName]
getRecordTypeFields :: Type -> TCM [Dom QName]
getRecordTypeFields Type
t = do
Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
case forall t a. Type'' t a -> a
unEl Type
t of
Def QName
r Elims
_ -> do
Defn
rDef <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
case Defn
rDef of
Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fields } -> forall (m :: * -> *) a. Monad m => a -> m a
return [Dom QName]
fields
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Term
_ -> 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 = forall a. KillRange a => KillRangeT a
killRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> ConHead
recConHead forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r
{-# SPECIALIZE isRecord :: QName -> TCM (Maybe Defn) #-}
{-# SPECIALIZE isRecord :: QName -> ReduceM (Maybe Defn) #-}
isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
isRecord :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r = do
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Defn
def of
Record{} -> forall a. a -> Maybe a
Just Defn
def
Defn
_ -> forall a. Maybe a
Nothing
isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, Defn))
isRecordType :: forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType Type
t
tryRecordType :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType :: forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType Type
t = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
m Type
a) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
nb Type
t -> do
let no :: m (Either (Blocked Type) (QName, Args, Defn))
no = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
nb Type
t
case forall t a. Type'' t a -> a
unEl Type
t of
Def QName
r Elims
es -> do
let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) m (Either (Blocked Type) (QName, Args, Defn))
no forall a b. (a -> b) -> a -> b
$ \ Defn
def -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (QName
r,Args
vs,Defn
def)
Term
_ -> m (Either (Blocked Type) (QName, Args, Defn))
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
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
let proj :: Maybe Projection
proj = Defn -> Maybe Projection
isProjection_ forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def
fallback :: m (QName, Definition, Maybe Projection)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Definition
def, Maybe Projection
proj)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
proj m (QName, Definition, Maybe Projection)
fallback forall a b. (a -> b) -> a -> b
$
\ p :: Projection
p@Projection{ projProper :: Projection -> Maybe QName
projProper = Maybe QName
proper, projOrig :: Projection -> QName
projOrig = QName
f' } ->
if forall a. Maybe a -> Bool
isNothing Maybe QName
proper Bool -> Bool -> Bool
|| QName
f forall a. Eq a => a -> a -> Bool
== QName
f' then m (QName, Definition, Maybe Projection)
fallback else do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f'
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f', Definition
def, Defn -> Maybe Projection
isProjection_ forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
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
(QName
f, Definition
def, Maybe Projection
mp) <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (QName, Definition, Maybe Projection)
origProjection QName
f
let a :: Type
a = Definition -> Type
defType Definition
def
fallback :: m (Maybe Type)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Type
a
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.deftype" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"definition f =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
" -- raw: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
f)
, TCMT IO Doc
"has type a =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"principal t =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
mp m (Maybe Type)
fallback forall a b. (a -> b) -> a -> b
$
\ (Projection{ projIndex :: Projection -> Int
projIndex = Int
n }) -> if Int
n forall a. Ord a => a -> a -> Bool
<= Int
0 then m (Maybe Type)
fallback else do
let npars :: Int
npars | Int
n forall a. Eq a => a -> a -> Bool
== Int
0 = forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise = Int
n forall a. Num a => a -> a -> a
- Int
1
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.deftype" Int
20 forall a b. (a -> b) -> a -> b
$ ArgName
"projIndex = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n
case forall t a. Type'' t a -> a
unEl Type
t of
Def QName
d Elims
es -> do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike QName
d) m (Maybe Type)
failNotElig forall a b. (a -> b) -> a -> b
$ do
let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
npars Elims
es
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.deftype" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"head d = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
d
, TCMT IO Doc
"parameters =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars)
]
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.deftype" Int
60 forall a b. (a -> b) -> a -> b
$ ArgName
"parameters = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Args
pars
if forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
pars forall a. Ord a => a -> a -> Bool
< Int
npars then ArgName -> m (Maybe Type)
failure ArgName
"does not supply enough parameters"
else forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
a forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
Term
_ -> m (Maybe Type)
failNotDef
where
failNotElig :: m (Maybe Type)
failNotElig = 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
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.deftype" Int
25 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"Def. " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is projection(like)"
, TCMT IO Doc
"but the type "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"of its argument " forall a. [a] -> [a] -> [a]
++ ArgName
reason
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
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 = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Type
tf -> do
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
ifNotPiType Type
tf (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Dom' Term Type
dom Abs Type
b -> do
Term
u <- forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
v)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Dom' Term Type
dom, Term
u, Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
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) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom' Term Type
a
prettyTCM (ProjT Dom' Term Type
a Type
b) =
m Doc
"." forall a. Semigroup a => a -> a -> a
TCM.<> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom' Term Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims Type
a Term
_ [] = 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 -> forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type
-> (Type -> tcm a)
-> (Dom' Term Type -> Abs Type -> tcm a)
-> tcm a
ifNotPiOrPathType Type
a forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ Dom' Term Type
a Abs Type
b -> do
(Dom' Term Type -> ElimType
ArgT Dom' Term Type
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> TCM [ElimType]
typeElims (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
v) (Term
self forall t. Apply t => t -> Elims -> t
`applyE` [Elim
e]) Elims
es
Proj ProjOrigin
o QName
f -> do
Type
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
(Dom' Term Type
dom, Term
self, Type
a) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
projectTyped Term
self Type
a ProjOrigin
o QName
f
(Dom' Term Type -> Type -> ElimType
ProjT Dom' Term Type
dom Type
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Elims -> TCM [ElimType]
typeElims Type
a Term
self Elims
es
IApply{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
{-# 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
Maybe Defn
isRec <- forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
case Maybe Defn
isRec of
Maybe Defn
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just Defn
r
| Defn -> HasEta
recEtaEquality Defn
r forall a. Eq a => a -> a -> Bool
/= forall a. HasEta' a
YesEta -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise -> do
Quantity
constructorQ <- forall a. LensQuantity a => a -> Quantity
getQuantity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName (Defn -> ConHead
recConHead Defn
r))
Quantity
currentQ <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Quantity TCEnv
eQuantity
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantity
constructorQ Quantity -> Quantity -> Bool
`moreQuantity` Quantity
currentQ
isEtaCon :: HasConstInfo m => QName -> m Bool
isEtaCon :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaCon QName
c = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left (SigUnknown ArgName
err) -> forall a. HasCallStack => a
__IMPOSSIBLE__
Left SigError
SigAbstract -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Right Definition
def -> case Definition -> Defn
theDef Definition
def of
Constructor {conData :: Defn -> QName
conData = QName
r} -> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor QName
c =
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall a b. (a -> b) -> a -> b
$ \ (QName
_, Defn
def) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
Defn -> HasEta
recEtaEquality Defn
def forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta Bool -> Bool -> Bool
|| Defn -> Maybe Induction
recInduction Defn
def forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Induction
Inductive
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord QName
r = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. a -> Maybe a
Just Induction
CoInductive forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Maybe Induction
recInduction) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
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 forall t a. Type'' t a -> a
unEl Type
a of
Def QName
d Elims
es -> do
let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
d, Args
vs)) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
isRecordConstructor :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left (SigUnknown ArgName
err) -> forall a. HasCallStack => a
__IMPOSSIBLE__
Left SigError
SigAbstract -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Right Definition
def -> case Definition -> Defn
theDef forall a b. (a -> b) -> a -> b
$ Definition
def of
Constructor{ conData :: Defn -> QName
conData = QName
r } -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName
r,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m)
=> QName -> m Bool
isGeneratedRecordConstructor :: forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
isGeneratedRecordConstructor QName
c = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall a b. (a -> b) -> a -> b
$ \ (QName
_, Defn
def) ->
case Defn
def of
Record{ recNamedCon :: Defn -> Bool
recNamedCon = Bool
False } -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
unguardedRecord :: QName -> PatternOrCopattern -> TCMT IO ()
unguardedRecord QName
q PatternOrCopattern
pat = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
r :: Defn
r@Record{} -> Defn
r { recEtaEquality' :: EtaEquality
recEtaEquality' = EtaEquality -> HasEta -> EtaEquality
setEtaEquality (Defn -> EtaEquality
recEtaEquality' Defn
r) forall a b. (a -> b) -> a -> b
$ forall a. a -> HasEta' a
NoEta PatternOrCopattern
pat }
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
updateEtaForRecord :: QName -> TCM ()
updateEtaForRecord :: QName -> TCMT IO ()
updateEtaForRecord QName
q = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
etaEnabled forall a b. (a -> b) -> a -> b
$ do
Bool
switchEta <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef 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 forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Induction
CoInductive -> Bool
True
| Bool
otherwise -> Bool
False
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
switchEta forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over (Lens' Defn Definition
lensTheDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' RecordData Defn
lensRecord) forall a b. (a -> b) -> a -> b
$ \ RecordData
d ->
RecordData
d{ _recEtaEquality' :: EtaEquality
_recEtaEquality' = HasEta -> EtaEquality
Inferred forall a. HasEta' a
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 -> TCM Bool
isRecursiveRecord QName
q = Defn -> Bool
recRecursive forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Signature -> Maybe Definition
lookupDefinition QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Signature
getSignature
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar Int
i = 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)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
forall (m :: * -> *).
PureTCM m =>
Int
-> Telescope
-> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar Int
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma0
l :: Int
l = forall a. Sized a => a -> Int
size [Dom' Term (ArgName, Type)]
gamma forall a. Num a => a -> a -> a
- Int
1 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) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
l [Dom' Term (ArgName, Type)]
gamma
let failure :: m (Maybe (Telescope, Substitution, Substitution, Telescope))
failure = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
25 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"failed to eta-expand variable " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ArgName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
" since its type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
" is not a record type"
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
a) m (Maybe (Telescope, Substitution, Substitution, Telescope))
failure forall a b. (a -> b) -> a -> b
$ \ (QName
r, Args
pars, Defn
def) -> case Defn -> HasEta
recEtaEquality Defn
def of
NoEta{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
HasEta
YesEta -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
let tel :: Telescope
tel = Defn -> Telescope
recTel Defn
def forall t. Apply t => t -> Args -> t
`apply` Args
pars
m :: Int
m = forall a. Sized a => a -> Int
size Telescope
tel
fs :: [Arg QName]
fs = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
def
ys :: Args
ys = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg QName
f Int
i -> Arg QName
f forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [Arg QName]
fs forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
m
u :: Term
u = ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem Args
ys
tau0 :: Substitution
tau0 = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
u forall a b. (a -> b) -> a -> b
$ forall a. Int -> Substitution' a
raiseS Int
m
tau :: Substitution
tau = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size [Dom' Term (ArgName, Type)]
gamma2) Substitution
tau0
zs :: Args
zs = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \ QName
f -> Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
sigma0 :: Substitution
sigma0 = forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
zs) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Int -> Substitution' a
raiseS Int
1
sigma :: Substitution
sigma = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size [Dom' Term (ArgName, Type)]
gamma2) Substitution
sigma0
s :: ArgName
s = forall a. Pretty a => a -> ArgName
prettyShow ArgName
x
tel' :: Telescope
tel' = forall a. (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames (\ ArgName
f -> ArgName -> ArgName
stringToArgName forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName
argNameToString ArgName
f forall a. [a] -> [a] -> [a]
++ ArgName
"(" forall a. [a] -> [a] -> [a]
++ ArgName
s forall a. [a] -> [a] -> [a]
++ ArgName
")") Telescope
tel
delta :: Telescope
delta = [Dom' Term (ArgName, Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)]
gamma1 forall a. [a] -> [a] -> [a]
++ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel' forall a. [a] -> [a] -> [a]
++
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
tau0 forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)] -> Telescope
telFromList [Dom' Term (ArgName, Type)]
gamma2)
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 = forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma, forall a. Substitution' a
idS, forall a. Substitution' a
idS)
expandRecordVarsRecursively (Int
i : [Int]
is) Telescope
gamma = do
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (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)
forall a b. (a -> b) -> a -> b
$ \ (Telescope
gamma1, Substitution
sigma1, Substitution
tau1, Telescope
tel) -> do
let n :: Int
n = forall a. Sized a => a -> Int
size Telescope
tel
newis :: [Int]
newis = forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
n
(Telescope
gamma2, Substitution
sigma2, Substitution
tau2) <- [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively ([Int]
newis forall a. [a] -> [a] -> [a]
++ [Int]
is) Telescope
gamma1
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma2, forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sigma1 Substitution
sigma2, forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
tau2 Substitution
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 Telescope
gamma Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
n Type
t
case forall t a. Type'' t a -> a
unEl Type
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
(QName
r, Args
pars, Defn
def) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
a
if | NoEta PatternOrCopattern
_ <- Defn -> HasEta
recEtaEquality Defn
def -> forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
let tel :: Telescope
tel = Defn -> Telescope
recTel Defn
def forall t. Apply t => t -> Args -> t
`apply` Args
pars
m :: Int
m = forall a. Sized a => a -> Int
size Telescope
tel
fs :: [Arg QName]
fs = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
def
ys :: Args
ys = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg QName
f Int
i -> Arg QName
f forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [Arg QName]
fs forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
m
u :: Term
u = ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem Args
ys
b' :: Type
b' = forall a. Subst a => Int -> a -> a
raise Int
m Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
u
t' :: Type
t' = Telescope
gamma Telescope -> Type -> Type
`telePi` (Telescope
tel Telescope -> Type -> Type
`telePi` Type
b')
gammai :: [ArgInfo]
gammai = forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> ArgInfo
domInfo forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma
xs :: Args
xs = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ ArgInfo
ai Int
i -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i) [ArgInfo]
gammai [Int
m..]
curry :: Term -> Term
curry Term
v = Telescope -> Term -> Term
teleLam Telescope
gamma forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
tel forall a b. (a -> b) -> a -> b
$
forall a. Subst a => Int -> a -> a
raise (Int
nforall a. Num a => a -> a -> a
+Int
m) Term
v forall t. Apply t => t -> Args -> t
`apply` (Args
xs forall a. [a] -> [a] -> [a]
++ [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
u])
zs :: Args
zs = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \ QName
f -> Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
atel :: Telescope
atel = forall a. SgTel a => a -> Telescope
sgTel forall a b. (a -> b) -> a -> b
$ (,) (forall a. Abs a -> ArgName
absName Abs Type
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Type
dom
uncurry :: Term -> Term
uncurry Term
v = Telescope -> Term -> Term
teleLam Telescope
gamma forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term
teleLam Telescope
atel forall a b. (a -> b) -> a -> b
$
forall a. Subst a => Int -> a -> a
raise (Int
n forall a. Num a => a -> a -> a
+ Int
1) Term
v forall t. Apply t => t -> Args -> t
`apply` (Args
xs forall a. [a] -> [a] -> [a]
++ Args
zs)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
curry, Term -> Term
uncurry, Type
t')
Term
_ -> 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 = 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 = 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
Defn
def <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
(Telescope
tel, ConHead
_, ConInfo
_, Args
args) <- forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
forceEta QName
r Args
pars Defn
def Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel, Args
args)
etaExpandRecord_ :: HasConstInfo m
=> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ :: forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ = forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
False
etaExpandRecord'_ :: HasConstInfo m
=> Bool -> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ :: forall (m :: * -> *).
HasConstInfo m =>
Bool
-> QName
-> Args
-> Defn
-> Term
-> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ Bool
forceEta QName
r Args
pars Defn
def Term
u = do
let Record{ recConHead :: Defn -> ConHead
recConHead = ConHead
con
, recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
xs
, recTel :: Defn -> Telescope
recTel = Telescope
tel
} = Defn
def
tel' :: Telescope
tel' = forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
pars
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Defn -> HasEta
recEtaEquality Defn
def forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta Bool -> Bool -> Bool
|| Bool
forceEta) forall a. HasCallStack => a
__IMPOSSIBLE__
case Term
u of
Con ConHead
con_ ConInfo
ci Elims
es -> do
let args :: Args
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (ConHead -> QName
conName ConHead
con forall (m :: * -> *).
HasConstInfo m =>
QName -> QName -> m (Maybe QName)
`sameDef` ConHead -> QName
conName ConHead
con_) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"etaExpandRecord_: the following two constructors should be identical"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"con = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow ConHead
con
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"con_ = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow ConHead
con_
]
forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel', ConHead
con, ConInfo
ci, Args
args)
Term
_ -> do
let xs' :: Args
xs' = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
xs) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \ QName
x -> Term
u forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.record.eta" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"eta expanding" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"tel' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
, TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
xs'
]
]
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel', ConHead
con, ConInfo
ConOSystem, Args
xs')
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType Type
t Term
u = do
(QName
r, Args
pars, Defn
def) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t
(Telescope
tel, ConHead
con, ConInfo
ci, Args
args) <- forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
r Args
pars Defn
def Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel, ConHead -> ConInfo -> Args -> Term
mkCon ConHead
con ConInfo
ci Args
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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => a -> Bool
usableModality) Args
args then m Term
fallBack else do
Just Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
xs } <- forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.record.eta.contract" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"eta contracting record"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"record type r =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
, TCMT IO Doc
"constructor c =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
, TCMT IO Doc
"field names xs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Dom QName]
xs
, TCMT IO Doc
"fields args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
args
]
]
case forall a. Ord a => a -> a -> Ordering
compare (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
xs) of
Ordering
LT -> m Term
fallBack
Ordering
GT -> forall a. HasCallStack => a
__IMPOSSIBLE__
Ordering
EQ -> do
case forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Arg Term -> Dom QName -> Maybe (Maybe Term)
check Args
args [Dom QName]
xs of
Just [Maybe Term]
as -> case forall a. [Maybe a] -> [a]
catMaybes [Maybe Term]
as of
(Term
a:[Term]
as) ->
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term
a forall a. Eq a => a -> a -> Bool
==) [Term]
as
then 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 = 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 QName -> Maybe (Maybe Term)
check Arg Term
a Dom QName
ax = do
case (forall a. LensRelevance a => a -> Relevance
getRelevance Arg Term
a, Term -> Maybe (Elims -> Term, Elims)
hasElims forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a) of
(Relevance
Irrelevant, Maybe (Elims -> Term, Elims)
_) -> forall a. a -> Maybe a
Just forall a. Maybe a
Nothing
(Relevance
_, Just (Elims -> Term
_, [])) -> forall a. Maybe a
Nothing
(Relevance
_, Just (Elims -> Term
h, Elim
e0:Elims
es0))
| (Elims
es, Proj ProjOrigin
_o QName
f) <- forall a. a -> [a] -> ([a], a)
initLast1 Elim
e0 Elims
es0
, forall t e. Dom' t e -> e
unDom Dom QName
ax forall a. Eq a => a -> a -> Bool
== QName
f -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Elims -> Term
h Elims
es
(Relevance, Maybe (Elims -> Term, Elims))
_ -> forall a. Maybe a
Nothing
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 = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
False QName
r Args
ps 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 = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
True QName
r Args
ps 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
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Is" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
r forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
ps) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"a singleton record type?"
, TCMT IO Doc
" already visited:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set QName
rs)
]
if QName
r forall a. Ord a => a -> Set a -> Bool
`Set.member` Set QName
rs then forall {a}. m (Maybe a)
no else do
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
r) forall {a}. m (Maybe a)
no forall a b. (a -> b) -> a -> b
$ \ Defn
def -> do
let recursive :: Bool
recursive = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null) forall a b. (a -> b) -> a -> b
$ Defn -> Maybe [QName]
recMutual Defn
def
let nonTerminating :: Bool
nonTerminating = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Defn -> Maybe Bool
recTerminates Defn
def
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r, TCMT IO Doc
"is recursive :", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
recursive ]
, forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r, TCMT IO Doc
"is non-terminating:", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
nonTerminating ]
]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ConHead -> ConInfo -> Args -> Term
mkCon (Defn -> ConHead
recConHead Defn
def) ConInfo
ConOSystem) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Set QName -> Telescope -> m (Maybe Args)
check (forall a. Bool -> (a -> a) -> a -> a
applyWhen (Bool
recursive Bool -> Bool -> Bool
&& Bool
nonTerminating) (forall a. Ord a => a -> Set a -> Set a
Set.insert QName
r) Set QName
rs) forall a b. (a -> b) -> a -> b
$ Defn -> Telescope
recTel Defn
def 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
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
30 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"isSingletonRecord' checking telescope " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
case Telescope
tel of
Telescope
EmptyTel -> forall {a}. m (Maybe [a])
yes
ExtendTel Dom' Term Type
dom Abs Telescope
tel -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
regardIrrelevance forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom' Term Type
dom)
(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 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
dom) HasCallStack => Term
__DUMMY_TERM__ forall a. a -> [a] -> [a]
:)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set QName -> Telescope -> m (Maybe Args)
check Set QName
rs)
forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
regardIrrelevance (forall t e. Dom' t e -> e
unDom Dom' Term Type
dom) Set QName
rs) forall {a}. m (Maybe a)
no forall a b. (a -> b) -> a -> b
$ \ Term
v -> do
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 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
dom) Term
v forall a. a -> [a] -> [a]
:)) 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
yes :: m (Maybe [a])
yes = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
False Type
t 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 = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> Type -> Set QName -> m (Maybe Term)
isSingletonType' Bool
True Type
t 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 Telescope
tel Type
t <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
let
record :: m (Maybe Term)
record :: m (Maybe Term)
record = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
(QName
r, Args
ps, Defn
def) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. HasEta' a
YesEta forall a. Eq a => a -> a -> Bool
== Defn -> HasEta
recEtaEquality Defn
def)
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Bool -> QName -> Args -> Set QName -> m (Maybe Term)
isSingletonRecord' Bool
regardIrrelevance QName
r Args
ps Set QName
rs)
subtype :: m (Maybe Term)
subtype :: m (Maybe Term)
subtype = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
(Term
level, Term
tA, Term
phi, Term
elt) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Term, Term, Term, Term))
isCubicalSubtype Type
t
QName
subin <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getBuiltinName' ArgName
builtinSubIn
QName
itIsOne <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getBuiltinName' ArgName
builtinIsOne
IntervalView
phiV <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView Term
phi
case IntervalView
phiV of
IntervalView
IOne -> do
let
argH :: e -> Arg e
argH = forall e. ArgInfo -> e -> Arg e
Arg forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo
it :: Term
it = Term
elt forall t. Apply t => t -> Args -> t
`apply` [forall a. a -> Arg a
defaultArg (QName -> Elims -> Term
Def QName
itIsOne [])]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
subin [] forall t. Apply t => t -> Args -> t
`apply` [forall a. a -> Arg a
argH Term
level, forall a. a -> Arg a
argH Term
tA, forall a. a -> Arg a
argH Term
phi, forall a. a -> Arg a
defaultArg Term
it])
OTerm Term
phi' -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
phi')
IntervalView
_ -> forall (m :: * -> *) a. MonadFail m => ArgName -> m a
fail ArgName
""
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe Term)
record forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Maybe Term)
subtype
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 = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG Term
u Type
a 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
(Term
u, Type
a) <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Type
a)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs" Int
80 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"isEtaVarG" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"u = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
, TCMT IO Doc
"a = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"mi = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Maybe Int
mi)
, TCMT IO Doc
"es = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Elim' Int]
es)
])
case (Term
u, forall t a. Type'' t a -> a
unEl Type
a) of
(Var Int
i' Elims
es', Term
_) -> do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Maybe Int
mi forall a. Eq a => a -> a -> Bool
== (Int
i' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Int
mi)
Type
b <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i'
Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
areEtaVarElims (Int -> Term
var Int
i') Type
b Elims
es' [Elim' Int]
es
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i'
(Term
_, Def QName
d Elims
pars) -> do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d
[QName]
fs <- forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom QName]
recFields forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
[Int]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [QName]
fs forall a b. (a -> b) -> a -> b
$ \QName
f -> do
let o :: ProjOrigin
o = ProjOrigin
ProjSystem
(Dom' Term Type
_, Term
_, Type
fa) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
projectTyped Term
u Type
a ProjOrigin
o QName
f
Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG (Term
u forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]) Type
fa Maybe Int
mi ([Elim' Int]
es forall a. [a] -> [a] -> [a]
++ [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f])
case (Maybe Int
mi, [Int]
is) of
(Just Int
i, [Int]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
(Maybe Int
Nothing, []) -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
(Maybe Int
Nothing, Int
i:[Int]
is) -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
==Int
i) [Int]
is) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
(Term
_, Pi Dom' Term Type
dom Abs Type
cod) -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom' Term Type
dom forall a b. (a -> b) -> a -> b
$ do
let u' :: Term
u' = forall a. Subst a => Int -> a -> a
raise Int
1 Term
u forall t. Apply t => t -> Args -> t
`apply` [forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
0]
a' :: Type
a' = forall a. Subst a => Abs a -> a
absBody Abs Type
cod
mi' :: Maybe Int
mi' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Num a => a -> a -> a
+Int
1) Maybe Int
mi
es' :: [Elim' Int]
es' = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a. Num a => a -> a -> a
+Int
1) [Elim' Int]
es forall a. [a] -> [a] -> [a]
++ [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
0]
(-Int
1forall a. Num a => a -> a -> a
+) 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)
_ -> 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 [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
areEtaVarElims Term
u Type
a [] (Elim' Int
_:[Elim' Int]
_) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (Elim
_:Elims
_) [] = 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
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ QName
f forall a. Eq a => a -> a -> Bool
== QName
f'
Type
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
(Dom' Term Type
_, Term
_, Type
fa) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom' Term Type, Term, Type))
projectTyped Term
u Type
a ProjOrigin
o QName
f
Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
areEtaVarElims (Term
u forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]) Type
fa Elims
es [Elim' Int]
es'
areEtaVarElims Term
u Type
a (Proj{} : Elims
_ ) (Apply Arg Int
_ : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (Apply Arg Term
_ : Elims
_ ) (Proj{} : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (Proj{} : Elims
_ ) (IApply{} : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Proj{} : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (Apply Arg Term
_ : Elims
_ ) (IApply{} : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (IApply{} : Elims
_ ) (Apply Arg Int
_ : [Elim' Int]
_ ) = forall (m :: * -> *) a. MonadPlus m => m a
mzero
areEtaVarElims Term
u Type
a (IApply{} : Elims
_) (IApply{} : [Elim' Int]
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
areEtaVarElims Term
u Type
a (Apply Arg Term
v : Elims
es) (Apply Arg Int
i : [Elim' Int]
es') = do
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
ifNotPiType Type
a (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero) forall a b. (a -> b) -> a -> b
$ \Dom' Term Type
dom Abs Type
cod -> do
Int
_ <- Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
isEtaVarG (forall e. Arg e -> e
unArg Arg Term
v) (forall t e. Dom' t e -> e
unDom Dom' Term Type
dom) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Int
i) []
Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
areEtaVarElims (Term
u forall t. Apply t => t -> Args -> t
`apply` [forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var Arg Int
i]) (Abs Type
cod forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Int -> Term
var (forall e. Arg e -> e
unArg Arg Int
i)) Elims
es [Elim' Int]
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
NAPs
ps <- forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Clause
cl { namedClausePats :: NAPs
namedClausePats = NAPs
ps }
instance NormaliseProjP a => NormaliseProjP [a] where
normaliseProjP :: forall (m :: * -> *). HasConstInfo m => [a] -> m [a]
normaliseProjP = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Arg a) where
normaliseProjP :: forall (m :: * -> *). HasConstInfo m => Arg a -> m (Arg a)
normaliseProjP = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Named_ a) where
normaliseProjP :: forall (m :: * -> *). HasConstInfo m => Named_ a -> m (Named_ a)
normaliseProjP = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(NormaliseProjP a, 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{} = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
normaliseProjP p :: Pattern' x
p@DotP{} = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
normaliseProjP (ConP ConHead
c ConPatternInfo
cpi [NamedArg (Pattern' x)]
ps) = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [NamedArg (Pattern' x)]
ps
normaliseProjP (DefP PatternInfo
o QName
q [NamedArg (Pattern' x)]
ps) = forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [NamedArg (Pattern' x)]
ps
normaliseProjP p :: Pattern' x
p@LitP{} = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p
normaliseProjP (ProjP ProjOrigin
o QName
d0) = forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d0
normaliseProjP p :: Pattern' x
p@IApplyP{} = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' x
p