module Agda.TypeChecking.Telescope where
import Control.Applicative
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as Set
#include "../undefined.h"
import Agda.Utils.Impossible
renameP :: Subst t => Permutation -> t -> t
renameP p = applySubst (renaming p)
renaming :: Permutation -> Substitution
renaming p = gamma'
where
n = size p
gamma = permute (reverseP $ invertP $ reverseP p) $ map var [0..]
gamma' = gamma ++# raiseS n
renamingR :: Permutation -> Substitution
renamingR p@(Perm n _) = permute (reverseP p) (map var [0..]) ++# raiseS n
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 :: [String] -> [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 -> [String]
teleNames = map (fst . unDom) . telToList
teleArgNames :: Telescope -> [Arg String]
teleArgNames = map (argFromDom . fmap fst) . telToList
teleArgs :: Telescope -> Args
teleArgs tel = [ Arg h r (var i) | (i, Dom h r _) <- zip (downFrom $ size l) l ]
where l = telToList tel
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 = map (n 1 ) $ filter (< n) $ reverse $ Set.toList fv
isC = [0..n 1] \\ is
perm0 = Perm n $ is ++ isC
permuteTel p ts = renameP (reverseP p) (permute p ts)
ts1 = permuteTel perm0 ts0
perm1 = reorderTel_ ts1
ts2 = permuteTel perm1 ts1
perm = composeP perm1 perm0
tel' = unflattenTel (permute perm names) ts2
Perm _ js = perm
m = genericLength $ takeWhile (`notElem` is) (reverse js)
(tel1, tel2) = telFromList -*- telFromList $ genericSplitAt (n m) $ telToList tel'
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 ignoreSharing $ 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
piApplyM :: Type -> Args -> TCM Type
piApplyM t [] = return t
piApplyM t (arg : args) = do
t <- reduce t
case ignoreSharing $ unEl t of
Pi _ b -> absApp b (unArg arg) `piApplyM` args
_ -> __IMPOSSIBLE__