{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Records where
import Control.Monad
import Control.Monad.Trans.Maybe
import qualified Data.List as List
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Data.Traversable (traverse)
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base (isNameInScope)
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad ()
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike (eligibleForProjectionLike)
import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Impossible
mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon h info args = Con h info (map Apply args)
orderFields
:: forall a
. QName
-> (Arg C.Name -> a)
-> [Arg C.Name]
-> [(C.Name, a)]
-> TCM [a]
orderFields r fill axs fs = do
reportSDoc "tc.record" 30 $ vcat
[ "orderFields"
, " official fields: " <+> sep (map pretty xs)
, " provided fields: " <+> sep (map pretty ys)
]
unlessNull duplicate $ typeError . DuplicateFields . nubOn id
unlessNull alien $ typeError . TooManyFields r missing
return $ for axs $ \ ax -> fromMaybe (fill ax) $ lookup (unArg ax) fs
where
xs = map unArg axs
ys = map fst fs
duplicate = duplicates ys
alien = ys List.\\ xs
missing = xs List.\\ ys
insertMissingFields
:: forall a
. QName
-> (C.Name -> a)
-> [FieldAssignment' a]
-> [Arg C.Name]
-> TCM [NamedArg a]
insertMissingFields r placeholder fs axs = do
let arg x e = caseMaybe (List.find ((x ==) . unArg) axs) (defaultNamedArg e) $ \ a ->
nameIfHidden a e <$ a
givenFields = [ (x, Just $ arg x e) | FieldAssignment x e <- fs ]
catMaybes <$> orderFields r fill axs givenFields
where
fill :: Arg C.Name -> Maybe (NamedArg a)
fill ax
| visible ax = Just $ setOrigin Inserted $ unnamed . placeholder <$> ax
| otherwise = Nothing
nameIfHidden :: Arg C.Name -> c -> Named_ c
nameIfHidden ax
| visible ax = unnamed
| otherwise = named $ WithOrigin Inserted $ Ranged (getRange ax) $ prettyShow $ unArg ax
recordModule :: QName -> ModuleName
recordModule = mnameFromList . qnameToList
getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn
getRecordDef r = maybe err return =<< isRecord r
where err = typeError $ ShouldBeRecordType (El __DUMMY_SORT__ $ Def r [])
getRecordOfField :: QName -> TCM (Maybe QName)
getRecordOfField d = caseMaybeM (isProjection d) (return Nothing) $
\ Projection{ projProper = proper, projFromType = r} ->
return $ unArg r <$ proper
getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m)
=> QName -> m [Dom C.Name]
getRecordFieldNames r = recordFieldNames <$> getRecordDef r
getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m)
=> QName -> m (Maybe [Dom C.Name])
getRecordFieldNames_ r = fmap recordFieldNames <$> isRecord r
recordFieldNames :: Defn -> [Dom C.Name]
recordFieldNames = map (fmap (nameConcrete . qnameName)) . recFields
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords fields = do
defs <- HMap.elems <$> useTC (stSignature . sigDefinitions)
idefs <- HMap.elems <$> useTC (stImports . sigDefinitions)
scope <- getScope
return $ filter (`isNameInScope` scope) $ cands defs ++ cands idefs
where
cands defs = [ defName d | d <- defs, possible d ]
possible def =
case theDef def of
Record{ recFields = fs } -> Set.isSubsetOf given $
Set.fromList $ map (nameConcrete . qnameName . unDom) fs
_ -> False
given = Set.fromList fields
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes r = recTel <$> getRecordDef r
getRecordTypeFields
:: Type
-> TCM [Dom QName]
getRecordTypeFields t = do
t <- reduce t
case unEl t of
Def r _ -> do
rDef <- theDef <$> getConstInfo r
case rDef of
Record { recFields = fields } -> return fields
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
getRecordConstructor r = killRange <$> recConHead <$> getRecordDef r
{-# SPECIALIZE isRecord :: QName -> TCM (Maybe Defn) #-}
{-# SPECIALIZE isRecord :: QName -> ReduceM (Maybe Defn) #-}
isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
isRecord r = do
def <- theDef <$> getConstInfo r
return $ case def of
Record{} -> Just def
_ -> Nothing
isRecordType :: (MonadReduce m, HasConstInfo m, HasBuiltins m)
=> Type -> m (Maybe (QName, Args, Defn))
isRecordType t = either (const Nothing) Just <$> tryRecordType t
tryRecordType :: (MonadReduce m, HasConstInfo m, HasBuiltins m)
=> Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType t = ifBlocked t (\ m a -> return $ Left $ Blocked m a) $ \ nb t -> do
let no = return $ Left $ NotBlocked nb t
case unEl t of
Def r es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
caseMaybeM (isRecord r) no $ \ def -> return $ Right (r,vs,def)
_ -> no
{-# SPECIALIZE origProjection :: QName -> TCM (QName, Definition, Maybe Projection) #-}
origProjection :: HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
origProjection f = do
def <- getConstInfo f
let proj = isProjection_ $ theDef def
fallback = return (f, def, proj)
caseMaybe proj fallback $
\ p@Projection{ projProper = proper, projOrig = f' } ->
if isNothing proper || f == f' then fallback else do
def <- getConstInfo f'
return (f', def, isProjection_ $ theDef def)
getDefType :: (HasConstInfo m, MonadReduce m, MonadDebug m)
=> QName -> Type -> m (Maybe Type)
getDefType f t = do
(f, def, mp) <- origProjection f
let a = defType def
fallback = return $ Just 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 = n }) -> if n <= 0 then fallback else do
let npars | n == 0 = __IMPOSSIBLE__
| otherwise = n - 1
reportSLn "tc.deftype" 20 $ "projIndex = " ++ show n
case unEl t of
Def d es -> do
ifNotM (eligibleForProjectionLike d) failNotElig $ do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take npars es
reportSDoc "tc.deftype" 20 $ vcat
[ text $ "head d = " ++ prettyShow d
, "parameters =" <+> sep (map prettyTCM pars)
]
reportSLn "tc.deftype" 60 $ "parameters = " ++ show pars
if length pars < npars then failure "does not supply enough parameters"
else Just <$> a `piApplyM` pars
_ -> failNotDef
where
failNotElig = failure "is not eligible for projection-likeness"
failNotDef = failure "is not a Def."
failure reason = do
reportSDoc "tc.deftype" 25 $ sep
[ "Def. " <+> prettyTCM f <+> " is projection(like)"
, "but the type "
, prettyTCM t
, text $ "of its argument " ++ reason
]
return Nothing
projectTyped
:: (HasConstInfo m, MonadReduce m, MonadDebug m)
=> Term
-> Type
-> ProjOrigin
-> QName
-> m (Maybe (Dom Type, Term, Type))
projectTyped v t o f = caseMaybeM (getDefType f t) (return Nothing) $ \ tf -> do
ifNotPiType tf (const $ return Nothing) $ \ dom b -> do
u <- applyDef o f (argFromDom dom $> v)
return $ Just (dom, u, b `absApp` v)
data ElimType
= ArgT (Dom Type)
| ProjT
{ projTRec :: Dom Type
, projTField :: Type
}
instance PrettyTCM ElimType where
prettyTCM (ArgT a) = prettyTCM a
prettyTCM (ProjT a b) =
"." <> parens (prettyTCM a <+> "->" <+> prettyTCM b)
typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims a _ [] = return []
typeElims a self (e : es) = do
case e of
Apply v -> ifNotPiOrPathType a __IMPOSSIBLE__ $ \ a b -> do
(ArgT a :) <$> typeElims (absApp b $ unArg v) (self `applyE` [e]) es
Proj o f -> do
a <- reduce a
(dom, self, a) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self a o f
(ProjT dom a :) <$> typeElims a self es
IApply{} -> __IMPOSSIBLE__
{-# SPECIALIZE isEtaRecord :: QName -> TCM Bool #-}
{-# SPECIALIZE isEtaRecord :: QName -> ReduceM Bool #-}
isEtaRecord :: HasConstInfo m => QName -> m Bool
isEtaRecord r = maybe False ((YesEta ==) . recEtaEquality) <$> isRecord r
isEtaCon :: HasConstInfo m => QName -> m Bool
isEtaCon c = getConstInfo' c >>= \case
Left (SigUnknown err) -> __IMPOSSIBLE__
Left SigAbstract -> return False
Right def -> case theDef def of
Constructor {conData = r} -> isEtaRecord r
_ -> return False
isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
isEtaOrCoinductiveRecordConstructor c =
caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->
return $ (Just Inductive, NoEta) /= (recInduction def, recEtaEquality def)
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord r = maybe False (\ d -> recInduction d /= Just CoInductive) <$> isRecord r
isEtaRecordType :: (HasConstInfo m)
=> Type -> m (Maybe (QName, Args))
isEtaRecordType a = case unEl a of
Def d es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
ifM (isEtaRecord d) (return $ Just (d, vs)) (return Nothing)
_ -> return Nothing
isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
isRecordConstructor c = getConstInfo' c >>= \case
Left (SigUnknown err) -> __IMPOSSIBLE__
Left SigAbstract -> return Nothing
Right def -> case theDef $ def of
Constructor{ conData = r } -> fmap (r,) <$> isRecord r
_ -> return Nothing
isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m)
=> QName -> m Bool
isGeneratedRecordConstructor c = ignoreAbstractMode $ do
caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->
case def of
Record{ recNamedCon = False } -> return True
_ -> return False
unguardedRecord :: QName -> TCM ()
unguardedRecord q = modifySignature $ updateDefinition q $ updateTheDef $ \case
r@Record{} -> r { recEtaEquality' = setEtaEquality (recEtaEquality' r) NoEta }
_ -> __IMPOSSIBLE__
recursiveRecord :: QName -> TCM ()
recursiveRecord q = do
ok <- etaEnabled
modifySignature $ updateDefinition q $ updateTheDef $ \case
r@Record{ recInduction = ind, recEtaEquality' = eta } ->
r { recEtaEquality' = eta' }
where
eta' | ok, eta == Inferred NoEta, ind /= Just CoInductive = Inferred YesEta
| otherwise = eta
_ -> __IMPOSSIBLE__
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord q = whenM etaEnabled $ do
modifySignature $ updateDefinition q $ updateTheDef $ \case
r@Record{ recInduction = ind, recEtaEquality' = Inferred NoEta }
| ind /= Just CoInductive ->
r { recEtaEquality' = Inferred YesEta }
r@Record{} -> r
_ -> __IMPOSSIBLE__
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord q = recRecursive . theDef . fromMaybe __IMPOSSIBLE__ . lookupDefinition q <$> getSignature
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar i = fmap (\ (delta, sigma, tau, _) -> (delta, sigma, tau)) <$> do
expandRecordVar i =<< getContextTelescope
expandRecordVar :: Int -> Telescope -> TCM (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar i gamma0 = do
let gamma = telToList gamma0
l = size gamma - 1 - i
let (gamma1, dom@(Dom{domInfo = ai, unDom = (x, a)}) : gamma2) = splitAt l gamma
let failure = do
reportSDoc "tc.meta.assign.proj" 25 $
"failed to eta-expand variable " <+> pretty x <+>
" since its type " <+> prettyTCM a <+>
" is not a record type"
return Nothing
caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> do
if recEtaEquality def == NoEta then return Nothing else Just <$> do
let tel = recTel def `apply` pars
m = size tel
fs = map argFromDom $ recFields def
ys = zipWith (\ f i -> f $> var i) fs $ downFrom m
u = mkCon (recConHead def) ConOSystem ys
tau0 = consS u $ raiseS m
tau = liftS (size gamma2) tau0
zs = for fs $ fmap $ \ f -> Var 0 [Proj ProjSystem f]
sigma0 = reverse (map unArg zs) ++# raiseS 1
sigma = liftS (size gamma2) sigma0
s = prettyShow x
tel' = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel
delta = telFromList $ gamma1 ++ telToList tel' ++
telToList (applySubst tau0 $ telFromList gamma2)
return (delta, sigma, tau, tel)
expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [] gamma = return (gamma, idS, idS)
expandRecordVarsRecursively (i : is) gamma = do
caseMaybeM (expandRecordVar i gamma) (expandRecordVarsRecursively is gamma)
$ \ (gamma1, sigma1, tau1, tel) -> do
let n = size tel
newis = take n $ downFrom $ i + n
(gamma2, sigma2, tau2) <- expandRecordVarsRecursively (newis ++ is) gamma1
return (gamma2, applySubst sigma1 sigma2, applySubst tau2 tau1)
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt t n = do
TelV gamma core <- telViewUpTo n t
case unEl core of
Pi (dom@Dom{domInfo = ai, unDom = a}) b -> do
(r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
when (recEtaEquality def == NoEta) __IMPOSSIBLE__
let tel = recTel def `apply` pars
m = size tel
fs = map argFromDom $ recFields def
ys = zipWith (\ f i -> f $> var i) fs $ downFrom m
u = mkCon (recConHead def) ConOSystem ys
b' = raise m b `absApp` u
t' = gamma `telePi` (tel `telePi` b')
gammai = map domInfo $ telToList gamma
xs = reverse $ zipWith (\ ai i -> Arg ai $ var i) gammai [m..]
curry v = teleLam gamma $ teleLam tel $
raise (n+m) v `apply` (xs ++ [Arg ai u])
zs = for fs $ fmap $ \ f -> Var 0 [Proj ProjSystem f]
atel = sgTel $ (,) (absName b) <$> dom
uncurry v = teleLam gamma $ teleLam atel $
raise (n + 1) v `apply` (xs ++ zs)
return (curry, uncurry, t')
_ -> __IMPOSSIBLE__
etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
=> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord = etaExpandRecord' False
forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
=> QName -> Args -> Term -> m (Telescope, Args)
forceEtaExpandRecord = etaExpandRecord' True
etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
=> Bool -> QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord' forceEta r pars u = do
def <- getRecordDef r
(tel, _, _, args) <- etaExpandRecord'_ forceEta r pars def u
return (tel, args)
etaExpandRecord_ :: HasConstInfo m
=> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ = etaExpandRecord'_ False
etaExpandRecord'_ :: HasConstInfo m
=> Bool -> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ forceEta r pars def u = do
let Record{ recConHead = con
, recFields = xs
, recTel = tel
} = def
tel' = apply tel pars
unless (recEtaEquality def == YesEta || forceEta) __IMPOSSIBLE__
case u of
Con con_ ci es -> do
let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
whenNothingM (conName con `sameDef` conName con_) $ do
reportSDoc "impossible" 10 $ vcat
[ "etaExpandRecord_: the following two constructors should be identical"
, nest 2 $ text $ "con = " ++ prettyShow con
, nest 2 $ text $ "con_ = " ++ prettyShow con_
]
__IMPOSSIBLE__
return (tel', con, ci, args)
_ -> do
let xs' = for (map argFromDom xs) $ fmap $ \ x -> u `applyE` [Proj ProjSystem x]
reportSDoc "tc.record.eta" 20 $ vcat
[ "eta expanding" <+> prettyTCM u <+> ":" <+> prettyTCM r
, nest 2 $ vcat
[ "tel' =" <+> prettyTCM tel'
, "args =" <+> prettyTCM xs'
]
]
return (tel', con, ConOSystem, xs')
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType t u = do
(r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType 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 r c ci args = if all (not . usableModality) args then fallBack else do
Just Record{ recFields = xs } <- isRecord r
let check :: Arg Term -> Dom QName -> Maybe (Maybe Term)
check a ax = do
case (getRelevance a, hasElims $ unArg a) of
(Irrelevant, _) -> Just Nothing
(_, Just (_, [])) -> Nothing
(_, Just (h, es)) | Proj _o f <- last es, unDom ax == f
-> Just $ Just $ h $ init es
_ -> Nothing
case compare (length args) (length xs) of
LT -> fallBack
GT -> __IMPOSSIBLE__
EQ -> do
case zipWithM check args xs of
Just as -> case [ a | Just a <- as ] of
(a:as) ->
if all (a ==) as
then return a
else fallBack
_ -> fallBack
_ -> fallBack
where
fallBack = return (mkCon c ci args)
isSingletonRecord :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> QName -> Args -> m (Either MetaId Bool)
isSingletonRecord r ps = mapRight isJust <$> isSingletonRecord' False r ps
isSingletonRecordModuloRelevance :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> QName -> Args -> m (Either MetaId Bool)
isSingletonRecordModuloRelevance r ps = mapRight isJust <$> isSingletonRecord' True r ps
isSingletonRecord' :: forall m. (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> Bool -> QName -> Args -> m (Either MetaId (Maybe Term))
isSingletonRecord' regardIrrelevance r ps = do
reportSDoc "tc.meta.eta" 30 $ "Is" <+> prettyTCM (Def r $ map Apply ps) <+> "a singleton record type?"
isRecord r >>= \case
Nothing -> return $ Right Nothing
Just def -> do
emap (mkCon (recConHead def) ConOSystem) <$> check (recTel def `apply` ps)
where
check :: Telescope -> m (Either MetaId (Maybe [Arg Term]))
check tel = do
reportSDoc "tc.meta.eta" 30 $
"isSingletonRecord' checking telescope " <+> prettyTCM tel
case tel of
EmptyTel -> return $ Right $ Just []
ExtendTel dom tel -> ifM (return regardIrrelevance `and2M` isIrrelevantOrPropM dom)
(underAbstraction dom tel $ \ tel ->
emap (Arg (domInfo dom) __DUMMY_TERM__ :) <$> check tel)
$ do
isSing <- isSingletonType' regardIrrelevance $ unDom dom
case isSing of
Left mid -> return $ Left mid
Right Nothing -> return $ Right Nothing
Right (Just v) -> underAbstraction dom tel $ \ tel ->
emap (Arg (domInfo dom) v :) <$> check tel
isSingletonType :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> Type -> m (Either MetaId (Maybe Term))
isSingletonType = isSingletonType' False
isSingletonTypeModuloRelevance :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> Type -> m (Either MetaId Bool)
isSingletonTypeModuloRelevance t = mapRight isJust <$> isSingletonType' True t
isSingletonType' :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m)
=> Bool -> Type -> m (Either MetaId (Maybe Term))
isSingletonType' regardIrrelevance t = do
TelV tel t <- telView t
ifBlocked t (\ m _ -> return $ Left m) $ \ _ t -> addContext tel $ do
res <- isRecordType t
case res of
Just (r, ps, def) | YesEta <- recEtaEquality def -> do
emap (abstract tel) <$> isSingletonRecord' regardIrrelevance r ps
_ -> return $ Right Nothing
isEtaVar :: Term -> Type -> TCM (Maybe Int)
isEtaVar u a = runMaybeT $ isEtaVarG u a Nothing []
where
isEtaVarG :: Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT TCM Int
isEtaVarG u a mi es = do
(u, a) <- liftTCM $ reduce (u, a)
liftTCM $ reportSDoc "tc.lhs" 80 $ "isEtaVarG" <+> nest 2 (vcat
[ "u = " <+> text (show u)
, "a = " <+> prettyTCM a
, "mi = " <+> text (show mi)
, "es = " <+> prettyList (map (text . show) es)
])
case (u, unEl a) of
(Var i' es', _) -> do
guard $ mi == (i' <$ mi)
b <- liftTCM $ typeOfBV i'
areEtaVarElims (var i') b es' es
return i'
(_, Def d pars) -> do
guard =<< do liftTCM $ isEtaRecord d
fs <- liftTCM $ map unDom . recFields . theDef <$> getConstInfo d
is <- forM fs $ \f -> do
let o = ProjSystem
(_, _, fa) <- MaybeT $ projectTyped u a o f
isEtaVarG (u `applyE` [Proj o f]) fa mi (es ++ [Proj o f])
case (mi, is) of
(Just i, _) -> return i
(Nothing, []) -> mzero
(Nothing, i:is) -> guard (all (==i) is) >> return i
(_, Pi dom cod) -> addContext dom $ do
let u' = raise 1 u `apply` [argFromDom dom $> var 0]
a' = absBody cod
mi' = fmap (+1) mi
es' = (fmap . fmap) (+1) es ++ [Apply $ argFromDom dom $> 0]
(-1+) <$> isEtaVarG u' a' mi' es'
_ -> mzero
areEtaVarElims :: Term -> Type -> Elims -> [Elim' Int] -> MaybeT TCM ()
areEtaVarElims u a [] [] = return ()
areEtaVarElims u a [] (_:_) = mzero
areEtaVarElims u a (_:_) [] = mzero
areEtaVarElims u a (Proj o f : es) (Proj _ f' : es') = do
guard $ f == f'
a <- liftTCM $ reduce a
(_, _, fa) <- MaybeT $ projectTyped u a o f
areEtaVarElims (u `applyE` [Proj o f]) fa es es'
areEtaVarElims u a (Proj{} : _ ) (Apply _ : _ ) = mzero
areEtaVarElims u a (Apply _ : _ ) (Proj{} : _ ) = mzero
areEtaVarElims u a (Proj{} : _ ) (IApply{} : _ ) = mzero
areEtaVarElims u a (IApply{} : _ ) (Proj{} : _ ) = mzero
areEtaVarElims u a (Apply _ : _ ) (IApply{} : _ ) = mzero
areEtaVarElims u a (IApply{} : _ ) (Apply _ : _ ) = mzero
areEtaVarElims u a (IApply{} : _) (IApply{} : _) = __IMPOSSIBLE__
areEtaVarElims u a (Apply v : es) (Apply i : es') = do
ifNotPiType a (const mzero) $ \dom cod -> do
_ <- isEtaVarG (unArg v) (unDom dom) (Just $ unArg i) []
areEtaVarElims (u `apply` [fmap var i]) (cod `absApp` var (unArg i)) es es'
emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)
emap = mapRight . fmap
class NormaliseProjP a where
normaliseProjP :: HasConstInfo m => a -> m a
instance NormaliseProjP Clause where
normaliseProjP cl = do
ps <- normaliseProjP $ namedClausePats cl
return $ cl { namedClausePats = ps }
instance NormaliseProjP a => NormaliseProjP [a] where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Arg a) where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Named_ a) where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP (Pattern' x) where
normaliseProjP p@VarP{} = return p
normaliseProjP p@DotP{} = return p
normaliseProjP (ConP c cpi ps) = ConP c cpi <$> normaliseProjP ps
normaliseProjP (DefP o q ps) = DefP o q <$> normaliseProjP ps
normaliseProjP p@LitP{} = return p
normaliseProjP (ProjP o d0) = ProjP o <$> getOriginalProjection d0
normaliseProjP p@IApplyP{} = return p