{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Telescope where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Data.Foldable (forM_, find)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Warnings
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
#include "undefined.h"
import Agda.Utils.Impossible
flattenTel :: Telescope -> [Dom Type]
flattenTel EmptyTel = []
flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
reorderTel :: [Dom Type] -> Maybe Permutation
reorderTel tel = topoSort comesBefore tel'
where
tel' = zip (downFrom $ size tel) tel
(i, _) `comesBefore` (_, a) = i `freeIn` unEl (unDom a)
reorderTel_ :: [Dom Type] -> Permutation
reorderTel_ tel = case reorderTel tel of
Nothing -> __IMPOSSIBLE__
Just p -> p
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
unflattenTel [] [] = EmptyTel
unflattenTel (x : xs) (a : tel) = ExtendTel a' (Abs x tel')
where
tel' = unflattenTel xs tel
a' = applySubst rho a
rho = parallelS (replicate (size tel + 1) __IMPOSSIBLE_TERM__)
unflattenTel [] (_ : _) = __IMPOSSIBLE__
unflattenTel (_ : _) [] = __IMPOSSIBLE__
teleNames :: Telescope -> [ArgName]
teleNames = map (fst . unDom) . telToList
teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames = map (argFromDom . fmap fst) . telToList
teleArgs :: (DeBruijn a) => Telescope -> [Arg a]
teleArgs tel =
[ Arg info (deBruijnVar i)
| (i, Dom {domInfo = info, unDom = (n,_)}) <- zip (downFrom $ size l) l ]
where l = telToList tel
withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
xs `withNamedArgsFromTel` tel =
[ Arg info (Named (Just $ Ranged noRange $ argNameToString name) x)
| (x, Dom {domInfo = info, unDom = (name,_)}) <- zip xs l ]
where l = telToList tel
teleNamedArgs :: (DeBruijn a) => Telescope -> [NamedArg a]
teleNamedArgs tel =
[ fmap (deBruijnVar i <$) $ namedArgFromDom dom
| (i, dom) <- zip (downFrom $ size l) l ]
where l = telToList tel
tele2NamedArgs :: (DeBruijn a) => Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs tel0 tel =
[ Arg info (Named (Just $ Ranged noRange $ argNameToString argName) (debruijnNamedVar varName i))
| (i, Dom{domInfo = info, unDom = (argName,_)}, Dom{unDom = (varName,_)}) <- zip3 (downFrom $ size l) l0 l ]
where
l = telToList tel
l0 = telToList tel0
splitTelescopeAt :: Int -> Telescope -> (Telescope,Telescope)
splitTelescopeAt n tel
| n <= 0 = (EmptyTel, tel)
| otherwise = splitTelescopeAt' n tel
where
splitTelescopeAt' _ EmptyTel = (EmptyTel,EmptyTel)
splitTelescopeAt' 1 (ExtendTel a tel) = (ExtendTel a (tel $> EmptyTel), absBody tel)
splitTelescopeAt' m (ExtendTel a tel) = (ExtendTel a (tel $> tel'), tel'')
where
(tel', tel'') = splitTelescopeAt (m - 1) $ absBody tel
permuteTel :: Permutation -> Telescope -> Telescope
permuteTel perm tel =
let names = permute perm $ teleNames tel
types = permute perm $ renameP __IMPOSSIBLE__ (flipP perm) $ flattenTel tel
in unflattenTel names types
varDependencies :: Telescope -> IntSet -> IntSet
varDependencies tel = allDependencies IntSet.empty
where
n = size tel
ts = flattenTel tel
directDependencies :: Int -> IntSet
directDependencies i = allFreeVars $ indexWithDefault __IMPOSSIBLE__ ts (n-1-i)
allDependencies :: IntSet -> IntSet -> IntSet
allDependencies =
IntSet.foldr $ \j soFar ->
if j >= n || j `IntSet.member` soFar
then soFar
else IntSet.insert j $ allDependencies soFar $ directDependencies j
data SplitTel = SplitTel
{ firstPart :: Telescope
, secondPart :: Telescope
, splitPerm :: Permutation
}
splitTelescope
:: VarSet
-> Telescope
-> SplitTel
splitTelescope fv tel = SplitTel tel1 tel2 perm
where
names = teleNames tel
ts0 = flattenTel tel
n = size tel
is = varDependencies tel fv
isC = IntSet.fromList [0..(n-1)] `IntSet.difference` is
perm = Perm n $ map (n-1-) $ VarSet.toDescList is ++ VarSet.toDescList isC
ts1 = renameP __IMPOSSIBLE__ (reverseP perm) (permute perm ts0)
tel' = unflattenTel (permute perm names) ts1
m = size is
(tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
splitTelescopeExact
:: [Int]
-> Telescope
-> Maybe SplitTel
splitTelescopeExact is tel = guard ok $> SplitTel tel1 tel2 perm
where
names = teleNames tel
ts0 = flattenTel tel
n = size tel
checkDependencies :: IntSet -> [Int] -> Bool
checkDependencies soFar [] = True
checkDependencies soFar (j:js) = ok && checkDependencies (IntSet.insert j soFar) js
where
fv' = allFreeVars $
indexWithDefault __IMPOSSIBLE__ ts0 (n-1-j)
fv = fv' `IntSet.intersection` IntSet.fromAscList [ 0 .. n-1 ]
ok = fv `IntSet.isSubsetOf` soFar
ok = all (<n) is && checkDependencies IntSet.empty is
isC = downFrom n List.\\ is
perm = Perm n $ map (n-1-) $ is ++ isC
ts1 = renameP __IMPOSSIBLE__ (reverseP perm) (permute perm ts0)
tel' = unflattenTel (permute perm names) ts1
m = size is
(tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
instantiateTelescopeN
:: Telescope
-> [(Int,Term)]
-> Maybe (Telescope,
Substitution)
instantiateTelescopeN tel [] = return (tel, IdS)
instantiateTelescopeN tel ((k,t):xs) = do
(tel', sigma, _) <- instantiateTelescope tel k t
(tel'', sigma') <- instantiateTelescopeN tel' (map (subtract 1 -*- applyPatSubst sigma) xs)
return (tel'', applyPatSubst sigma sigma')
instantiateTelescope
:: Telescope
-> Int
-> Term
-> Maybe (Telescope,
PatternSubstitution,
Permutation)
instantiateTelescope tel k u = guard ok $> (tel', sigma, rho)
where
names = teleNames tel
ts0 = flattenTel tel
n = size tel
j = n-1-k
is0 = varDependencies tel $ allFreeVars u
is1 = IntSet.delete j $
IntSet.fromAscList [ 0 .. n-1 ] `IntSet.difference` is0
is = IntSet.toAscList is1 ++ IntSet.toAscList is0
ok = not $ j `IntSet.member` is0
perm = Perm n $ is
rho = reverseP perm
u1 = renameP __IMPOSSIBLE__ perm u
us = map (\i -> fromMaybe (dotP u1) (deBruijnVar <$> List.findIndex (i ==) is)) [ 0 .. n-1 ]
sigma = us ++# raiseS (n-1)
ts1 = permute rho $ applyPatSubst sigma ts0
tel' = unflattenTel (permute rho names) ts1
expandTelescopeVar
:: Telescope
-> Int
-> Telescope
-> ConHead
-> ( Telescope
, PatternSubstitution)
expandTelescopeVar gamma k delta c = (tel', rho)
where
(ts1,a:ts2) = fromMaybe __IMPOSSIBLE__ $
splitExactlyAt k $ telToList gamma
cpi = noConPatternInfo
{ conPRecord = Just PatOSystem
, conPType = Just $ snd <$> argFromDom a
, conPLazy = True
}
cargs = map (setOrigin Inserted) $ teleNamedArgs delta
cdelta = ConP c cpi cargs
rho0 = consS cdelta $ raiseS (size delta)
rho = liftS (size ts2) rho0
gamma1 = telFromList ts1
gamma2' = applyPatSubst rho0 $ telFromList ts2
tel' = gamma1 `abstract` (delta `abstract` gamma2')
telView :: Type -> TCM TelView
telView = telViewUpTo (-1)
telViewUpTo :: Int -> Type -> TCM TelView
telViewUpTo n t = telViewUpTo' n (const True) t
telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView
telViewUpTo' 0 p t = return $ TelV EmptyTel t
telViewUpTo' n p t = do
t <- reduce t
case unEl t of
Pi a b | p a -> absV a (absName b) <$> telViewUpTo' (n - 1) p (absBody b)
_ -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
telViewPath :: Type -> TCM TelView
telViewPath = telViewUpToPath (-1)
telViewUpToPath :: Int -> Type -> TCM TelView
telViewUpToPath 0 t = return $ TelV EmptyTel t
telViewUpToPath n t = do
vt <- pathViewAsPi $ t
case vt of
Left (a,b) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
Right (El _ t) | Pi a b <- t
-> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
Right t -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
type Boundary = Boundary' (Term,Term)
type Boundary' a = [(Term,a)]
telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView,Boundary)
telViewUpToPathBoundary' 0 t = return $ (TelV EmptyTel t,[])
telViewUpToPathBoundary' n t = do
vt <- pathViewAsPi' $ t
case vt of
Left ((a,b),xy) -> addEndPoints xy . absV a (absName b) <$> telViewUpToPathBoundary' (n - 1) (absBody b)
Right (El _ t) | Pi a b <- t
-> absV a (absName b) <$> telViewUpToPathBoundary' (n - 1) (absBody b)
Right t -> return $ (TelV EmptyTel t,[])
where
absV a x (TelV tel t, cs) = (TelV (ExtendTel a (Abs x tel)) t, cs)
addEndPoints xy (telv@(TelV tel _),cs) = (telv, (var $ size tel - 1, xyInTel):cs)
where
xyInTel = raise (size tel) xy
fullBoundary :: Telescope -> Boundary -> Boundary
fullBoundary tel bs =
let es = teleElims tel bs
l = size tel
in map (\ (t@(Var i []), xy) -> (t, xy `applyE` (drop (l - i) es))) bs
telViewUpToPathBoundary :: Int -> Type -> TCM (TelView,Boundary)
telViewUpToPathBoundary i a = do
(telv@(TelV tel b), bs) <- telViewUpToPathBoundary' i a
return $ (telv, fullBoundary tel bs)
telViewUpToPathBoundaryP :: Int -> Type -> TCM (TelView,Boundary)
telViewUpToPathBoundaryP = telViewUpToPathBoundary'
telViewPathBoundaryP :: Type -> TCM (TelView,Boundary)
telViewPathBoundaryP = telViewUpToPathBoundaryP (-1)
teleElims :: DeBruijn a => Telescope -> Boundary' (a,a) -> [Elim' a]
teleElims tel [] = map Apply $ teleArgs tel
teleElims tel boundary = recurse (teleArgs tel)
where
recurse = fmap updateArg
matchVar x =
snd <$> flip find boundary (\case
(Var i [],_) -> i == x
_ -> __IMPOSSIBLE__)
updateArg a@(Arg info p) =
case deBruijnView p of
Just i | Just (t,u) <- matchVar i -> IApply t u p
_ -> Apply a
pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type)
pathViewAsPi t = either (Left . fst) Right <$> pathViewAsPi' t
pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi' t = do
pathViewAsPi'whnf <*> reduce t
pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi'whnf = do
view <- pathView'
minterval <- getBuiltin' builtinInterval
return $ \ t -> case view t of
PathType s l p a x y | Just interval <- minterval ->
let name | Lam _ (Abs n _) <- unArg a = n
| otherwise = "i"
i = El Inf interval
in
Left $ ((defaultDom $ i, Abs name $ El (raise 1 s) $ raise 1 (unArg a) `apply` [defaultArg $ var 0]), (unArg x, unArg y))
_ -> Right t
piOrPath :: Type -> TCM (Either (Dom Type, Abs Type) Type)
piOrPath t = do
t <- pathViewAsPi'whnf <*> pure t
case t of
Left (p,_) -> return $ Left p
Right (El _ (Pi a b)) -> return $ Left (a,b)
Right t -> return $ Right t
telView'UpToPath :: Int -> Type -> TCM TelView
telView'UpToPath 0 t = return $ TelV EmptyTel t
telView'UpToPath n t = do
vt <- pathViewAsPi'whnf <*> pure t
case vt of
Left ((a,b),_) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
Right (El _ t) | Pi a b <- t
-> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
Right t -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
telView'Path :: Type -> TCM TelView
telView'Path = telView'UpToPath (-1)
isPath :: Type -> TCM (Maybe (Dom Type, Abs Type))
isPath t = either Just (const Nothing) <$> pathViewAsPi t
telePatterns :: (DeBruijn a, DeBruijn (Pattern' a)) =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns = telePatterns' teleNamedArgs
telePatterns' :: (DeBruijn a, DeBruijn (Pattern' a)) =>
(forall a. (DeBruijn a) => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' f tel [] = f tel
telePatterns' f tel boundary = recurse $ f tel
where
recurse = (fmap . fmap . fmap) updateVar
matchVar x =
snd <$> flip find boundary (\case
(Var i [],_) -> i == x
_ -> __IMPOSSIBLE__)
o = PatOSystem
updateVar x =
case deBruijnView x of
Just i | Just (t,u) <- matchVar i -> IApplyP o t u x
_ -> VarP o x
mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type)
mustBePi t = ifNotPiType t __IMPOSSIBLE__ $ \ a b -> return (a,b)
ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
ifPi t yes no = do
t <- reduce t
case t of
Pi a b -> yes a b
_ -> no t
ifPiType :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType (El s t) yes no = ifPi t yes (no . El s)
ifNotPi :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPi = flip . ifPi
ifNotPiType :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType = flip . ifPiType
ifNotPiOrPathType :: (MonadReduce tcm, MonadTCM tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType t no yes = do
ifPiType t yes (\ t -> either (uncurry yes . fst) (const $ no t) =<< (liftTCM pathViewAsPi'whnf <*> pure t))
class PiApplyM a where
piApplyM :: MonadReduce m => Type -> a -> m Type
instance PiApplyM Term where
piApplyM t v = ifNotPiType t __IMPOSSIBLE__ $ \ _ b -> return $ absApp b v
instance PiApplyM a => PiApplyM (Arg a) where
piApplyM t = piApplyM t . unArg
instance PiApplyM a => PiApplyM (Named n a) where
piApplyM t = piApplyM t . namedThing
instance PiApplyM a => PiApplyM [a] where
piApplyM t = foldl (\ mt v -> mt >>= (`piApplyM` v)) (return t)
typeArity :: Type -> TCM Nat
typeArity t = do
TelV tel _ <- telView t
return (size tel)
data OutputTypeName
= OutputTypeName QName
| OutputTypeVar
| OutputTypeVisiblePi
| OutputTypeNameNotYetKnown
| NoOutputTypeName
getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName t = do
TelV tel t' <- telViewUpTo' (-1) notVisible t
ifBlocked (unEl t') (\ _ _ -> return (tel , OutputTypeNameNotYetKnown)) $ \ _ v ->
case v of
Def n _ -> return (tel , OutputTypeName n)
Sort{} -> return (tel , NoOutputTypeName)
Var n _ -> return (tel , OutputTypeVar)
Pi{} -> return (tel , OutputTypeVisiblePi)
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance x t = do
(tel , n) <- getOutputTypeName t
case n of
OutputTypeName n -> addNamedInstance x n
OutputTypeNameNotYetKnown -> addUnknownInstance x
NoOutputTypeName -> warning $ WrongInstanceDeclaration
OutputTypeVar -> warning $ WrongInstanceDeclaration
OutputTypeVisiblePi -> warning $ InstanceWithExplicitArg x
resolveUnknownInstanceDefs :: TCM ()
resolveUnknownInstanceDefs = do
anonInstanceDefs <- getAnonInstanceDefs
clearAnonInstanceDefs
forM_ anonInstanceDefs $ \ n -> addTypedInstance n =<< typeOfConst n
getInstanceDefs :: TCM InstanceTable
getInstanceDefs = do
resolveUnknownInstanceDefs
insts <- getAllInstanceDefs
unless (null $ snd insts) $
typeError $ GenericError $ "There are instances whose type is still unsolved"
return $ fst insts