module Agda.TypeChecking.Telescope where
import Data.Set (Set)
import qualified Data.Set as Set
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "../undefined.h"
import Agda.Utils.Impossible
rename :: Subst t => Permutation -> t -> t
rename p = substs (renaming p)
renaming :: Permutation -> [Term]
renaming p = gamma'
where
n = size p
gamma = permute (reverseP $ invertP $ reverseP p) $ map var [0..]
gamma' = gamma ++ map var [n..]
var i = Var i []
renamingR :: Permutation -> [Term]
renamingR p@(Perm n _) = permute (reverseP p) (map var [0..]) ++ map var [n..]
where
var i = Var (fromIntegral i) []
flattenTel :: Telescope -> [Arg Type]
flattenTel EmptyTel = []
flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
reorderTel :: [Arg Type] -> Permutation
reorderTel tel = case topoSort comesBefore tel' of
Nothing -> __IMPOSSIBLE__
Just p -> p
where
tel' = reverse $ zip [0..] $ reverse tel
(i, _) `comesBefore` (_, a) = i `freeIn` unEl (unArg a)
unflattenTel :: [String] -> [Arg Type] -> Telescope
unflattenTel [] [] = EmptyTel
unflattenTel (x : xs) (a : tel) = ExtendTel a' (Abs x tel')
where
tel' = unflattenTel xs tel
a' = substs rho a
rho = replicate (size tel + 1) __IMPOSSIBLE_TERM__ ++ map var [0..]
where var i = Var i []
unflattenTel [] (_ : _) = __IMPOSSIBLE__
unflattenTel (_ : _) [] = __IMPOSSIBLE__
teleNames :: Telescope -> [String]
teleNames = map (fst . unArg) . telToList
teleArgNames :: Telescope -> [Arg String]
teleArgNames = map (fmap fst) . telToList
teleArgs :: Telescope -> Args
teleArgs tel =
reverse [ Arg h (Var i []) | (i, Arg h _) <- zip [0..] $ reverse (telToList tel) ]
data SplitTel = SplitTel
{ firstPart :: Telescope
, secondPart :: Telescope
, splitPerm :: Permutation
}
splitTelescope :: Set Nat -> 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 = rename (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'