{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Telescope where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad (unless, guard)
import Data.Foldable (forM_)
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
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
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 info (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 info (name,_)) <- zip xs l ]
where l = telToList tel
teleNamedArgs :: (DeBruijn a) => Telescope -> [NamedArg a]
teleNamedArgs tel =
[ Arg info (Named (Just $ Ranged noRange $ argNameToString name) (deBruijnVar i))
| (i, Dom info (name,_)) <- 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 info (argName,_), Dom _ (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 $ 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 $ 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'
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 = ConPatternInfo
{ 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
mustBePi :: MonadTCM tcm => Type -> tcm (Dom Type, Abs Type)
mustBePi t = ifNotPiType t __IMPOSSIBLE__ $ \ a b -> return (a,b)
ifPi :: MonadTCM tcm => Term -> (Dom Type -> Abs Type -> tcm a) -> (Term -> tcm a) -> tcm a
ifPi t yes no = do
t <- liftTCM $ reduce t
case t of
Pi a b -> yes a b
_ -> no t
ifPiType :: MonadTCM tcm => Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a
ifPiType (El s t) yes no = ifPi t yes (no . El s)
ifNotPi :: MonadTCM tcm => Term -> (Term -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPi = flip . ifPi
ifNotPiType :: MonadTCM tcm => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiType = flip . ifPiType
piApplyM :: Type -> Args -> TCM Type
piApplyM t [] = return t
piApplyM t (arg : args) = do
(_, b) <- mustBePi t
absApp b (unArg arg) `piApplyM` args
piApply1 :: MonadTCM tcm => Type -> Term -> tcm Type
piApply1 t v = do
(_, b) <- mustBePi t
return $ absApp b v
typeArity :: Type -> TCM Nat
typeArity t = do
TelV tel _ <- telView t
return (size tel)
data OutputTypeName
= OutputTypeName QName
| OutputTypeVar
| OutputTypeNameNotYetKnown
| NoOutputTypeName
getOutputTypeName :: Type -> TCM OutputTypeName
getOutputTypeName t = do
TelV tel t' <- telView t
ifBlocked (unEl t') (\ _ _ -> return OutputTypeNameNotYetKnown) $ \ _ v ->
case v of
Def n _ -> return $ OutputTypeName n
Sort{} -> return NoOutputTypeName
Var n _ -> return OutputTypeVar
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
Pi{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance x t = do
n <- getOutputTypeName t
case n of
OutputTypeName n -> addNamedInstance x n
OutputTypeNameNotYetKnown -> addUnknownInstance x
NoOutputTypeName -> typeError $ WrongInstanceDeclaration
OutputTypeVar -> typeError $ WrongInstanceDeclaration
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