module Agda.TypeChecking.Substitute where
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Arrow ((***))
import Data.Generics (Typeable, Data)
import Data.List hiding (sort)
import qualified Data.List as List
import Data.Function
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Free
import Agda.TypeChecking.CompiledClause
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Permutation
#include "../undefined.h"
import Agda.Utils.Impossible
class Apply t where
apply :: t -> Args -> t
instance Apply Term where
apply m [] = m
apply m args@(a:args0) =
case m of
Var i args' -> Var i (args' ++ args)
Def c args' -> Def c (args' ++ args)
Con c args' -> Con c (args' ++ args)
Lam _ u -> absApp u (unArg a) `apply` args0
MetaV x args' -> MetaV x (args' ++ args)
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
Pi _ _ -> __IMPOSSIBLE__
Sort _ -> __IMPOSSIBLE__
DontCare mv -> DontCare $ mv `apply` args
instance Apply Type where
apply = piApply
instance Apply Sort where
apply s [] = s
apply s _ = __IMPOSSIBLE__
instance Subst a => Apply (Tele a) where
apply tel [] = tel
apply EmptyTel _ = __IMPOSSIBLE__
apply (ExtendTel _ tel) (t : ts) = absApp tel (unArg t) `apply` ts
instance Apply Definition where
apply (Defn rel x t df m c d) args = Defn rel x (piApply t args) df m c (apply d args)
instance Apply Defn where
apply d [] = d
apply d args = case d of
Axiom{} -> d
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Nothing, funArgOccurrences = occ } ->
d { funClauses = apply cs args
, funCompiled = apply cc args
, funInv = apply inv args
, funArgOccurrences = drop (length args) occ
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Just (r, n), funArgOccurrences = occ }
| m < n -> d { funProjection = Just (r, n m) }
| otherwise ->
d { funClauses = apply cs args'
, funCompiled = apply cc args'
, funInv = apply inv args'
, funProjection = Just (r, 0)
, funArgOccurrences = drop 1 occ
}
where args' = [last args]
m = size args
Datatype{ dataPars = np, dataClause = cl
, dataArgOccurrences = occ } ->
d { dataPars = np size args, dataClause = apply cl args
, dataArgOccurrences = drop (length args) occ
}
Record{ recPars = np, recConType = t, recClause = cl, recTel = tel
, recArgOccurrences = occ } ->
d { recPars = np size args, recConType = apply t args
, recClause = apply cl args, recTel = apply tel args
, recArgOccurrences = drop (length args) occ
}
Constructor{ conPars = np } ->
d { conPars = np size args }
Primitive{ primClauses = cs } ->
d { primClauses = apply cs args }
instance Apply PrimFun where
apply (PrimFun x ar def) args = PrimFun x (ar size args) $ \vs -> def (args ++ vs)
instance Apply Clause where
apply (Clause r tel perm ps b) args =
Clause r (apply tel args) (apply perm args)
(drop (size args) ps) (apply b args)
instance Apply CompiledClauses where
apply cc args = case cc of
Fail -> Fail
Done hs t
| length hs >= len -> Done (drop len hs)
(substs ([ Var (fromIntegral i) []
| i <- [0..length hs len 1]] ++
map unArg args) t)
| otherwise -> __IMPOSSIBLE__
Case n bs
| n >= len -> Case (n len) (apply bs args)
| otherwise -> __IMPOSSIBLE__
where
len = length args
instance Apply a => Apply (Case a) where
apply (Branches cs ls m) args =
Branches (apply cs args) (apply ls args) (apply m args)
instance Apply FunctionInverse where
apply NotInjective args = NotInjective
apply (Inverse inv) args = Inverse $ apply inv args
instance Apply ClauseBody where
apply b [] = b
apply (Bind (Abs _ b)) (a:args) = subst (unArg a) b `apply` args
apply (Bind (NoAbs _ b)) (_:args) = b `apply` args
apply (Body _) (_:_) = __IMPOSSIBLE__
apply NoBody _ = NoBody
instance Apply DisplayTerm where
apply (DTerm v) args = DTerm $ apply v args
apply (DDot v) args = DDot $ apply v args
apply (DCon c vs) args = DCon c $ vs ++ map (fmap DTerm) args
apply (DDef c vs) args = DDef c $ vs ++ map (fmap DTerm) args
apply (DWithApp v args') args = DWithApp v $ args' ++ args
instance Apply t => Apply [t] where
apply ts args = map (`apply` args) ts
instance Apply t => Apply (Blocked t) where
apply b args = fmap (`apply` args) b
instance Apply t => Apply (Maybe t) where
apply x args = fmap (`apply` args) x
instance Apply v => Apply (Map k v) where
apply x args = fmap (`apply` args) x
instance (Apply a, Apply b) => Apply (a,b) where
apply (x,y) args = (apply x args, apply y args)
instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
apply (x,y,z) args = (apply x args, apply y args, apply z args)
instance Apply Permutation where
apply (Perm n xs) args = Perm (n m) $ map (flip () m) $ genericDrop m xs
where
m = size args
instance Abstract Permutation where
abstract tel (Perm n xs) = Perm (n + m) $ [0..m 1] ++ map (+ m) xs
where
m = size tel
piApply :: Type -> Args -> Type
piApply t [] = t
piApply (El _ (Pi _ b)) (a:args) = absApp b (unArg a) `piApply` args
piApply _ _ = __IMPOSSIBLE__
class Abstract t where
abstract :: Telescope -> t -> t
instance Abstract Term where
abstract = teleLam
instance Abstract Type where
abstract = telePi_
instance Abstract Sort where
abstract EmptyTel s = s
abstract _ s = __IMPOSSIBLE__
instance Abstract Telescope where
abstract EmptyTel tel = tel
abstract (ExtendTel arg tel') tel = ExtendTel arg $ fmap (`abstract` tel) tel'
instance Abstract Definition where
abstract tel (Defn rel x t df m c d) = Defn rel x (abstract tel t) df m c (abstract tel d)
instance Abstract Defn where
abstract tel d = case d of
Axiom{} -> d
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Nothing, funArgOccurrences = occ } ->
d { funClauses = abstract tel cs, funCompiled = abstract tel cc
, funInv = abstract tel inv
, funArgOccurrences = replicate (size tel) Negative ++ occ
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Just (r, n), funArgOccurrences = occ } ->
d { funProjection = Just (r, n + size tel) }
Datatype{ dataPars = np, dataClause = cl, dataArgOccurrences = occ } ->
d { dataPars = np + size tel, dataClause = abstract tel cl
, dataArgOccurrences = replicate (size tel) Negative ++ occ
}
Record{ recPars = np, recConType = t, recClause = cl, recTel = tel'
, recArgOccurrences = occ } ->
d { recPars = np + size tel, recConType = abstract tel t
, recClause = abstract tel cl, recTel = abstract tel tel'
, recArgOccurrences = replicate (size tel) Negative ++ occ
}
Constructor{ conPars = np } ->
d { conPars = np + size tel }
Primitive{ primClauses = cs } ->
d { primClauses = abstract tel cs }
instance Abstract PrimFun where
abstract tel (PrimFun x ar def) = PrimFun x (ar + n) $ \ts -> def $ genericDrop n ts
where n = size tel
instance Abstract Clause where
abstract tel (Clause r tel' perm ps b) =
Clause r (abstract tel tel') (abstract tel perm)
(telVars tel ++ ps) (abstract tel b)
instance Abstract CompiledClauses where
abstract tel Fail = Fail
abstract tel (Done xs t) = Done (map (fmap fst) (telToList tel) ++ xs) t
abstract tel (Case n bs) =
Case (n + fromIntegral (size tel)) (abstract tel bs)
instance Abstract a => Abstract (Case a) where
abstract tel (Branches cs ls m) =
Branches (abstract tel cs) (abstract tel ls) (abstract tel m)
telVars EmptyTel = []
telVars (ExtendTel arg tel) = fmap (const $ VarP $ absName tel) arg : telVars (unAbs tel)
instance Abstract FunctionInverse where
abstract tel NotInjective = NotInjective
abstract tel (Inverse inv) = Inverse $ abstract tel inv
instance Abstract ClauseBody where
abstract EmptyTel b = b
abstract (ExtendTel _ tel) b = Bind $ fmap (`abstract` b) tel
instance Abstract t => Abstract [t] where
abstract tel = map (abstract tel)
instance Abstract t => Abstract (Maybe t) where
abstract tel x = fmap (abstract tel) x
instance Abstract v => Abstract (Map k v) where
abstract tel m = fmap (abstract tel) m
abstractArgs :: Abstract a => Args -> a -> a
abstractArgs args x = abstract tel x
where
tel = foldr (\(Arg h r x) -> ExtendTel (Arg h r $ sort Prop) . Abs x) EmptyTel
$ zipWith (fmap . const) names args
names = cycle $ map (:[]) ['a'..'z']
type Substitution = [Term]
class Subst t where
substs :: Substitution -> t -> t
substUnder :: Nat -> Term -> t -> t
idSub :: Telescope -> Substitution
idSub tel = [ Var i [] | i <- [0..size tel 1] ]
subst :: Subst t => Term -> t -> t
subst u t = substUnder 0 u t
instance Subst Term where
substs us t =
case t of
Var i vs -> (us !!! i) `apply` substs us vs
Lam h m -> Lam h $ substs us m
Def c vs -> Def c $ substs us vs
Con c vs -> Con c $ substs us vs
MetaV x vs -> MetaV x $ substs us vs
Lit l -> Lit l
Level l -> levelTm $ substs us l
Pi a b -> uncurry Pi $ substs us (a,b)
Sort s -> sortTm $ substs us s
DontCare mv -> DontCare $ substs us mv
where
[] !!! n = __IMPOSSIBLE__
(x:xs) !!! 0 = x
(_:xs) !!! n = xs !!! (n 1)
substUnder n u t =
case t of
Var i vs
| i == n -> raise n u `apply` substUnder n u vs
| i < n -> Var i $ substUnder n u vs
| otherwise -> Var (i 1) $ substUnder n u vs
Lam h m -> Lam h $ substUnder n u m
Def c vs -> Def c $ substUnder n u vs
Con c vs -> Con c $ substUnder n u vs
MetaV x vs -> MetaV x $ substUnder n u vs
Level l -> levelTm $ substUnder n u l
Lit l -> Lit l
Pi a b -> uncurry Pi $ substUnder n u (a,b)
Sort s -> sortTm $ substUnder n u s
DontCare mv -> DontCare $ substUnder n u mv
instance Subst Type where
substs us (El s t) = substs us s `El` substs us t
substUnder n u (El s t) = substUnder n u s `El` substUnder n u t
instance Subst Sort where
substs us s = case s of
Type n -> levelSort $ sub n
Prop -> Prop
Inf -> Inf
DLub s1 s2 -> DLub (sub s1) (sub s2)
where sub x = substs us x
substUnder n u s = case s of
Type n -> levelSort $ sub n
Prop -> Prop
Inf -> Inf
DLub s1 s2 -> DLub (sub s1) (sub s2)
where sub x = substUnder n u x
instance Subst Level where
substs us (Max as) = Max $ substs us as
substUnder n u (Max as) = Max $ substUnder n u as
instance Subst PlusLevel where
substs us l@ClosedLevel{} = l
substs us (Plus n l) = Plus n $ substs us l
substUnder n u l@ClosedLevel{} = l
substUnder n u (Plus m l) = Plus m $ substUnder n u l
instance Subst LevelAtom where
substs us (MetaLevel m vs) = MetaLevel m $ substs us vs
substs us (BlockedLevel m v) = BlockedLevel m $ substs us v
substs us (NeutralLevel v) = UnreducedLevel $ substs us v
substs us (UnreducedLevel v) = UnreducedLevel $ substs us v
substUnder n u (MetaLevel m vs) = MetaLevel m $ substUnder n u vs
substUnder n u (BlockedLevel m v) = BlockedLevel m $ substUnder n u v
substUnder n u (NeutralLevel v) = UnreducedLevel $ substUnder n u v
substUnder n u (UnreducedLevel v) = UnreducedLevel $ substUnder n u v
instance Subst Pattern where
substs us p = case p of
VarP s -> VarP s
LitP l -> LitP l
ConP c mt ps -> ConP c (substs us mt) $ substs us ps
DotP t -> DotP $ substs us t
substUnder n u p = case p of
VarP s -> VarP s
LitP l -> LitP l
ConP c mt ps -> ConP c (substUnder n u mt) $ substUnder n u ps
DotP t -> DotP $ substUnder n u t
instance Subst t => Subst (Blocked t) where
substs us b = fmap (substs us) b
substUnder n u b = fmap (substUnder n u) b
instance Subst DisplayTerm where
substs us (DTerm v) = DTerm $ substs us v
substs us (DDot v) = DDot $ substs us v
substs us (DCon c vs) = DCon c $ substs us vs
substs us (DDef c vs) = DDef c $ substs us vs
substs us (DWithApp vs ws) = uncurry DWithApp $ substs us (vs, ws)
substUnder n u (DTerm v) = DTerm $ substUnder n u v
substUnder n u (DDot v) = DDot $ substUnder n u v
substUnder n u (DCon c vs) = DCon c $ substUnder n u vs
substUnder n u (DDef c vs) = DDef c $ substUnder n u vs
substUnder n u (DWithApp vs ws) = uncurry DWithApp $ substUnder n u (vs, ws)
instance Subst a => Subst (Tele a) where
substs us EmptyTel = EmptyTel
substs us (ExtendTel t tel) = uncurry ExtendTel $ substs us (t, tel)
substUnder n u EmptyTel = EmptyTel
substUnder n u (ExtendTel t tel) = uncurry ExtendTel $ substUnder n u (t, tel)
instance Subst a => Subst (Abs a) where
substs us (Abs x t) = Abs x $ substs (Var 0 [] : raise 1 us) t
substs us (NoAbs x t) = NoAbs x $ substs us t
substUnder n u (Abs x t) = Abs x $ substUnder (n + 1) u t
substUnder n u (NoAbs x t) = NoAbs x $ substUnder n u t
instance Subst a => Subst (Arg a) where
substs us = fmap (substs us)
substUnder n u = fmap (substUnder n u)
instance Subst a => Subst (Maybe a) where
substs us = fmap (substs us)
substUnder n u = fmap (substUnder n u)
instance Subst a => Subst [a] where
substs us = map (substs us)
substUnder n u = map (substUnder n u)
instance (Subst a, Subst b) => Subst (a,b) where
substs us (x,y) = (substs us x, substs us y)
substUnder n u (x,y) = (substUnder n u x, substUnder n u y)
instance Subst ClauseBody where
substs us (Body t) = Body $ substs us t
substs us (Bind b) = Bind $ substs us b
substs _ NoBody = NoBody
substUnder n u (Body t) = Body $ substUnder n u t
substUnder n u (Bind b) = Bind $ substUnder n u b
substUnder _ _ NoBody = NoBody
class Raise t where
raiseFrom :: Nat -> Nat -> t -> t
renameFrom :: Nat -> (Nat -> Nat) -> t -> t
instance Raise () where
raiseFrom _ _ _ = ()
renameFrom _ _ _ = ()
instance Raise Term where
raiseFrom m k v =
case v of
Var i vs
| i < m -> Var i $ rf vs
| otherwise -> Var (i + k) $ rf vs
Lam h m -> Lam h $ rf m
Def c vs -> Def c $ rf vs
Con c vs -> Con c $ rf vs
MetaV x vs -> MetaV x $ rf vs
Level l -> Level $ rf l
Lit l -> Lit l
Pi a b -> uncurry Pi $ rf (a,b)
Sort s -> Sort $ rf s
DontCare mv -> DontCare $ rf mv
where
rf x = raiseFrom m k x
renameFrom m k v =
case v of
Var i vs
| i < m -> Var i $ rf vs
| otherwise -> Var (k (i m) + m) $ rf vs
Lam h m -> Lam h $ rf m
Def c vs -> Def c $ rf vs
Con c vs -> Con c $ rf vs
MetaV x vs -> MetaV x $ rf vs
Level l -> Level $ rf l
Lit l -> Lit l
Pi a b -> uncurry Pi $ rf (a,b)
Sort s -> Sort $ rf s
DontCare mv -> DontCare $ rf mv
where
rf x = renameFrom m k x
instance Raise Type where
raiseFrom m k (El s t) = raiseFrom m k s `El` raiseFrom m k t
renameFrom m k (El s t) = renameFrom m k s `El` renameFrom m k t
instance Raise Sort where
raiseFrom m k s = case s of
Type n -> Type $ rf n
Prop -> Prop
Inf -> Inf
DLub s1 s2 -> DLub (rf s1) (rf s2)
where rf x = raiseFrom m k x
renameFrom m k s = case s of
Type n -> Type $ rf n
Prop -> Prop
Inf -> Inf
DLub s1 s2 -> DLub (rf s1) (rf s2)
where rf x = renameFrom m k x
instance Raise Level where
raiseFrom m k (Max as) = Max $ raiseFrom m k as
renameFrom m k (Max as) = Max $ renameFrom m k as
instance Raise PlusLevel where
raiseFrom m k l@ClosedLevel{} = l
raiseFrom m k (Plus n l) = Plus n $ raiseFrom m k l
renameFrom m k l@ClosedLevel{} = l
renameFrom m k (Plus n l) = Plus n $ renameFrom m k l
instance Raise LevelAtom where
raiseFrom m k l = case l of
MetaLevel n vs -> MetaLevel n $ raiseFrom m k vs
NeutralLevel v -> NeutralLevel $ raiseFrom m k v
BlockedLevel n v -> BlockedLevel n $ raiseFrom m k v
UnreducedLevel v -> UnreducedLevel $ raiseFrom m k v
renameFrom m k l = case l of
MetaLevel n vs -> MetaLevel n $ renameFrom m k vs
NeutralLevel v -> NeutralLevel $ renameFrom m k v
BlockedLevel n v -> BlockedLevel n $ renameFrom m k v
UnreducedLevel v -> UnreducedLevel $ renameFrom m k v
instance Raise Constraint where
raiseFrom m k c = case c of
ValueCmp cmp a u v -> ValueCmp cmp (rf a) (rf u) (rf v)
ElimCmp ps a v e1 e2 -> ElimCmp ps (rf a) (rf v) (rf e1) (rf e2)
TypeCmp cmp a b -> TypeCmp cmp (rf a) (rf b)
TelCmp a b cmp tel1 tel2 -> TelCmp (rf a) (rf b) cmp (rf tel1) (rf tel2)
SortCmp cmp s1 s2 -> SortCmp cmp (rf s1) (rf s2)
LevelCmp cmp l1 l2 -> LevelCmp cmp (rf l1) (rf l2)
Guarded c cs -> Guarded (rf c) cs
IsEmpty a -> IsEmpty (rf a)
FindInScope{} -> c
UnBlock{} -> c
where
rf x = raiseFrom m k x
renameFrom m k c = case c of
ValueCmp cmp a u v -> ValueCmp cmp (rf a) (rf u) (rf v)
ElimCmp ps a v e1 e2 -> ElimCmp ps (rf a) (rf v) (rf e1) (rf e2)
TypeCmp cmp a b -> TypeCmp cmp (rf a) (rf b)
TelCmp a b cmp tel1 tel2 -> TelCmp (rf a) (rf b) cmp (rf tel1) (rf tel2)
SortCmp cmp s1 s2 -> SortCmp cmp (rf s1) (rf s2)
LevelCmp cmp l1 l2 -> LevelCmp cmp (rf l1) (rf l2)
Guarded c cs -> Guarded (rf c) cs
IsEmpty a -> IsEmpty (rf a)
FindInScope{} -> c
UnBlock{} -> c
where
rf x = renameFrom m k x
instance Raise Elim where
raiseFrom m k e = case e of
Apply v -> Apply (raiseFrom m k v)
Proj{} -> e
renameFrom m k e = case e of
Apply v -> Apply (renameFrom m k v)
Proj{} -> e
instance Raise ClauseBody where
raiseFrom m k b = case b of
Body v -> Body $ rf v
NoBody -> NoBody
Bind b -> Bind $ rf b
where rf x = raiseFrom m k x
renameFrom m k b = case b of
Body v -> Body $ rf v
NoBody -> NoBody
Bind b -> Bind $ rf b
where rf x = renameFrom m k x
instance Raise Pattern where
raiseFrom m k p = case p of
DotP t -> DotP $ raiseFrom m k t
ConP c mt ps -> ConP c (raiseFrom m k mt) (raiseFrom m k ps)
VarP x -> p
LitP l -> p
renameFrom m k p = case p of
DotP t -> DotP $ renameFrom m k t
ConP c mt ps -> ConP c (renameFrom m k mt) (renameFrom m k ps)
VarP x -> p
LitP l -> p
instance Raise a => Raise (Tele a) where
raiseFrom m k EmptyTel = EmptyTel
raiseFrom m k (ExtendTel a tel) = uncurry ExtendTel $ raiseFrom m k (a, tel)
renameFrom m k EmptyTel = EmptyTel
renameFrom m k (ExtendTel a tel) = uncurry ExtendTel $ renameFrom m k (a, tel)
instance Raise DisplayForm where
raiseFrom m k (Display n ps v) = Display n (raiseFrom (m + 1) k ps)
(raiseFrom (m + n) k v)
renameFrom m k (Display n ps v) = Display n (renameFrom (m + 1) k ps)
(renameFrom (m + n) k v)
instance Raise DisplayTerm where
raiseFrom m k (DWithApp xs ys) = uncurry DWithApp $ raiseFrom m k (xs, ys)
raiseFrom m k (DTerm v) = DTerm $ raiseFrom m k v
raiseFrom m k (DDot v) = DDot $ raiseFrom m k v
raiseFrom m k (DCon c vs) = DCon c $ raiseFrom m k vs
raiseFrom m k (DDef c vs) = DDef c $ raiseFrom m k vs
renameFrom m k (DWithApp xs ys) = uncurry DWithApp $ renameFrom m k (xs, ys)
renameFrom m k (DTerm v) = DTerm $ renameFrom m k v
renameFrom m k (DDot v) = DDot $ renameFrom m k v
renameFrom m k (DCon c vs) = DCon c $ renameFrom m k vs
renameFrom m k (DDef c vs) = DDef c $ renameFrom m k vs
instance Raise t => Raise (Abs t) where
raiseFrom m k (Abs x v) = Abs x $ raiseFrom (m + 1) k v
raiseFrom m k (NoAbs x v) = NoAbs x $ raiseFrom m k v
renameFrom m k (Abs x v) = Abs x $ renameFrom (m + 1) k v
renameFrom m k (NoAbs x v) = NoAbs x $ renameFrom m k v
instance Raise t => Raise (Arg t) where
raiseFrom m k = fmap (raiseFrom m k)
renameFrom m k = fmap (renameFrom m k)
instance Raise t => Raise (Blocked t) where
raiseFrom m k = fmap (raiseFrom m k)
renameFrom m k = fmap (renameFrom m k)
instance Raise t => Raise [t] where
raiseFrom m k = fmap (raiseFrom m k)
renameFrom m k = fmap (renameFrom m k)
instance Raise t => Raise (Maybe t) where
raiseFrom m k = fmap (raiseFrom m k)
renameFrom m k = fmap (renameFrom m k)
instance Raise v => Raise (Map k v) where
raiseFrom m k = fmap (raiseFrom m k)
renameFrom m k = fmap (renameFrom m k)
instance (Raise a, Raise b) => Raise (a,b) where
raiseFrom m k (x,y) = (raiseFrom m k x, raiseFrom m k y)
renameFrom m k (x,y) = (renameFrom m k x, renameFrom m k y)
raise :: Raise t => Nat -> t -> t
raise = raiseFrom 0
rename :: Raise t => (Nat -> Nat) -> t -> t
rename = renameFrom 0
data TelV a = TelV (Tele (Arg a)) a
deriving (Typeable, Data, Show, Eq, Ord, Functor)
type TelView = TelV Type
telFromList :: [Arg (String, Type)] -> Telescope
telFromList = foldr (\(Arg h r (x, a)) -> ExtendTel (Arg h r a) . Abs x) EmptyTel
telToList :: Telescope -> [Arg (String, Type)]
telToList EmptyTel = []
telToList (ExtendTel arg tel) = fmap ((,) $ absName tel) arg : telToList (absBody tel)
telView' :: Type -> TelView
telView' t = case unEl t of
Pi a b -> absV a (absName b) $ telView' (absBody b)
_ -> TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
telePi :: Telescope -> Type -> Type
telePi EmptyTel t = t
telePi (ExtendTel u tel) t = el $ Pi u (reAbs b)
where
el = El (dLub s1 s2)
b = fmap (flip telePi t) tel
s1 = getSort $ unArg u
s2 = fmap getSort b
telePi_ :: Telescope -> Type -> Type
telePi_ EmptyTel t = t
telePi_ (ExtendTel u tel) t = el $ Pi u b
where
el = El (dLub s1 s2)
b = fmap (flip telePi_ t) tel
s1 = getSort $ unArg u
s2 = fmap getSort b
teleLam :: Telescope -> Term -> Term
teleLam EmptyTel t = t
teleLam (ExtendTel u tel) t = Lam (argHiding u) $ flip teleLam t <$> tel
dLub :: Sort -> Abs Sort -> Sort
dLub s1 (NoAbs _ s2) = sLub s1 s2
dLub s1 b@(Abs _ s2) = case occurrence 0 $ freeVars s2 of
Flexible -> DLub s1 b
NoOccurrence -> sLub s1 (absApp b __IMPOSSIBLE__)
StronglyRigid -> Inf
WeaklyRigid -> Inf
absApp :: Subst t => Abs t -> Term -> t
absApp (Abs _ v) u = subst u v
absApp (NoAbs _ v) _ = v
absBody :: Raise t => Abs t -> t
absBody (Abs _ v) = v
absBody (NoAbs _ v) = raise 1 v
mkAbs :: (Raise a, Free a) => String -> a -> Abs a
mkAbs x v | 0 `freeIn` v = Abs x v
| otherwise = NoAbs x (raise (1) v)
reAbs :: (Raise a, Free a) => Abs a -> Abs a
reAbs (NoAbs x v) = NoAbs x v
reAbs (Abs x v) = mkAbs x v
deriving instance (Raise a, Eq a) => Eq (Tele a)
deriving instance (Raise a, Ord a) => Ord (Tele a)
deriving instance Eq Sort
deriving instance Ord Sort
deriving instance Eq Type
deriving instance Ord Type
deriving instance Ord Term
deriving instance Eq Level
deriving instance Ord Level
deriving instance Eq PlusLevel
deriving instance Ord LevelAtom
deriving instance Eq Elim
deriving instance Ord Elim
deriving instance Eq Constraint
instance Ord PlusLevel where
compare ClosedLevel{} Plus{} = LT
compare Plus{} ClosedLevel{} = GT
compare (ClosedLevel n) (ClosedLevel m) = compare n m
compare (Plus n a) (Plus m b) = compare (a,n) (b,m)
instance Eq LevelAtom where
(==) = (==) `on` unLevelAtom
instance Eq Term where
Var x vs == Var x' vs' = x == x' && vs == vs'
Lam h v == Lam h' v' = h == h' && v == v'
Lit l == Lit l' = l == l'
Def x vs == Def x' vs' = x == x' && vs == vs'
Con x vs == Con x' vs' = x == x' && vs == vs'
Pi a b == Pi a' b' = a == a' && b == b'
Sort s == Sort s' = s == s'
Level l == Level l' = l == l'
MetaV m vs == MetaV m' vs' = m == m' && vs == vs'
DontCare _ == DontCare _ = True
_ == _ = False
instance (Raise a, Eq a) => Eq (Abs a) where
NoAbs _ a == NoAbs _ b = a == b
Abs _ a == Abs _ b = a == b
a == b = absBody a == absBody b
instance (Raise a, Ord a) => Ord (Abs a) where
NoAbs _ a `compare` NoAbs _ b = a `compare` b
Abs _ a `compare` Abs _ b = a `compare` b
a `compare` b = absBody a `compare` absBody b
sLub :: Sort -> Sort -> Sort
sLub s Prop = s
sLub Prop s = s
sLub Inf _ = Inf
sLub _ Inf = Inf
sLub (Type (Max as)) (Type (Max bs)) = Type $ levelMax (as ++ bs)
sLub (DLub a b) c = DLub (sLub a c) b
sLub a (DLub b c) = DLub (sLub a b) c
lvlView :: Term -> Level
lvlView (Level l) = l
lvlView (Sort (Type l)) = l
lvlView v = Max [Plus 0 $ UnreducedLevel v]
levelMax :: [PlusLevel] -> Level
levelMax as0 = Max $ ns ++ List.sort bs
where
as = Prelude.concatMap expand as0
ns = case [ n | ClosedLevel n <- as, n > 0 ] of
[] -> []
ns -> [ ClosedLevel n | n <- [Prelude.maximum ns], n > leastB ]
bs = subsume [ b | b@Plus{} <- as ]
leastB | null bs = 0
| otherwise = Prelude.minimum [ n | Plus n _ <- bs ]
expand l@ClosedLevel{} = [l]
expand (Plus n l) = map (plus n) $ expand0 $ expandAtom l
expand0 [] = [ClosedLevel 0]
expand0 as = as
expandAtom (BlockedLevel _ (Level (Max as))) = as
expandAtom (NeutralLevel (Level (Max as))) = as
expandAtom (UnreducedLevel (Level (Max as))) = as
expandAtom (BlockedLevel _ (Sort (Type (Max as)))) = as
expandAtom (NeutralLevel (Sort (Type (Max as)))) = as
expandAtom (UnreducedLevel (Sort (Type (Max as)))) = as
expandAtom l = [Plus 0 l]
plus n (ClosedLevel m) = ClosedLevel (n + m)
plus n (Plus m l) = Plus (n + m) l
subsume (ClosedLevel{} : _) = __IMPOSSIBLE__
subsume [] = []
subsume (Plus n a : bs)
| not $ null ns = subsume bs
| otherwise = Plus n a : subsume [ b | b@(Plus _ a') <- bs, a /= a' ]
where
ns = [ m | Plus m a' <- bs, a == a', m > n ]
sortTm :: Sort -> Term
sortTm (Type l) = Sort $ levelSort l
sortTm s = Sort s
levelSort :: Level -> Sort
levelSort (Max as)
| List.any isInf as = Inf
where
isInf ClosedLevel{} = False
isInf (Plus _ l) = infAtom l
infAtom (NeutralLevel a) = infTm a
infAtom (UnreducedLevel a) = infTm a
infAtom MetaLevel{} = False
infAtom BlockedLevel{} = False
infTm (Sort Inf) = True
infTm _ = False
levelSort l =
case levelTm l of
Sort s -> s
_ -> Type l
levelTm :: Level -> Term
levelTm l =
case l of
Max [Plus 0 l] -> unLevelAtom l
_ -> Level l
unLevelAtom (MetaLevel x vs) = MetaV x vs
unLevelAtom (NeutralLevel v) = v
unLevelAtom (UnreducedLevel v) = v
unLevelAtom (BlockedLevel _ v) = v