module Agda.TypeChecking.Telescope where
import Control.Applicative
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.Reduce
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 r (Var i []) | (i, Arg h r _) <- 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'
telView :: MonadTCM tcm => Type -> tcm TelView
telView t = do
t <- reduce t
case unEl t of
Pi a (Abs x b) -> absV a x <$> telView b
Fun a b -> absV a "_" <$> telView (raise 1 b)
_ -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
piApplyM :: MonadTCM tcm => Type -> Args -> tcm Type
piApplyM t [] = return t
piApplyM t (arg : args) = do
t <- reduce t
case (t, arg) of
(El _ (Pi _ b), arg) -> absApp b (unArg arg) `piApplyM` args
(El _ (Fun _ b), _ ) -> b `piApplyM` args
_ -> __IMPOSSIBLE__