{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Substitute
( module Agda.TypeChecking.Substitute
, module Agda.TypeChecking.Substitute.Class
, module Agda.TypeChecking.Substitute.DeBruijn
, Substitution'(..), Substitution
) where
import Control.Arrow (first, second)
import Data.Function
import Data.Functor
import qualified Data.List as List
import Data.Map (Map)
import Data.Maybe
import Data.Monoid
import Debug.Trace (trace)
import Language.Haskell.TH.Syntax (thenCmp)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Position (Range)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Free as Free
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence as Occ
import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Substitute.DeBruijn
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.HashMap (HashMap)
#include "undefined.h"
import Agda.Utils.Impossible
instance Apply Term where
applyE m [] = m
applyE m es =
case m of
Var i es' -> Var i (es' ++ es)
Def f es' -> defApp f es' es
Con c ci args -> conApp c ci args es
Lam _ b ->
case es of
Apply a : es0 -> lazyAbsApp b (unArg a) `applyE` es0
_ -> __IMPOSSIBLE__
MetaV x es' -> MetaV x (es' ++ es)
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
Pi _ _ -> __IMPOSSIBLE__
Sort _ -> __IMPOSSIBLE__
DontCare mv -> dontCare $ mv `applyE` es
canProject :: QName -> Term -> Maybe (Arg Term)
canProject f v =
case v of
(Con (ConHead _ _ fs) _ vs) -> do
i <- List.elemIndex f fs
isApplyElim =<< headMaybe (drop i vs)
_ -> Nothing
conApp :: ConHead -> ConInfo -> Elims -> Elims -> Term
conApp ch ci args [] = Con ch ci args
conApp ch ci args (a@Apply{} : es) = conApp ch ci (args ++ [a]) es
conApp ch@(ConHead c _ fs) ci args (Proj o f : es) =
let failure = flip trace __IMPOSSIBLE__ $
"conApp: constructor " ++ show c ++
" with fields " ++ show fs ++
" projected by " ++ show f
isApply e = fromMaybe __IMPOSSIBLE__ $ isApplyElim e
i = maybe failure id $ List.elemIndex f fs
v = maybe failure (argToDontCare . isApply) $ headMaybe $ drop i args
in applyE v es
defApp :: QName -> Elims -> Elims -> Term
defApp f [] (Apply a : es) | Just v <- canProject f (unArg a)
= argToDontCare v `applyE` es
defApp f es0 es = Def f $ es0 ++ es
argToDontCare :: Arg Term -> Term
argToDontCare (Arg ai v)
| Irrelevant <- getRelevance ai = dontCare v
| otherwise = v
instance Apply Sort where
applyE s [] = s
applyE s _ = __IMPOSSIBLE__
instance Subst Term a => Apply (Tele a) where
apply tel [] = tel
apply EmptyTel _ = __IMPOSSIBLE__
apply (ExtendTel _ tel) (t : ts) = lazyAbsApp tel (unArg t) `apply` ts
instance Apply Definition where
apply (Defn info x t pol occ df m c inst copy ma inj d) args =
Defn info x (piApply t args) (apply pol args) (apply occ args) df m c inst copy ma inj (apply d args)
instance Apply RewriteRule where
apply r args =
let newContext = apply (rewContext r) args
sub = liftS (size newContext) $ parallelS $
reverse $ map (PTerm . unArg) args
in RewriteRule
{ rewName = rewName r
, rewContext = newContext
, rewHead = rewHead r
, rewPats = applySubst sub (rewPats r)
, rewRHS = applyNLPatSubst sub (rewRHS r)
, rewType = applyNLPatSubst sub (rewType r)
}
instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
apply occ args = List.drop (length args) occ
instance {-# OVERLAPPING #-} Apply [Polarity] where
apply pol args = List.drop (length args) pol
instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
apply ps args = loop (length args) ps
where
loop 0 ps = ps
loop n [] = __IMPOSSIBLE__
loop n (p : ps) =
let recurse = loop (n - 1) ps
in case namedArg p of
VarP{} -> recurse
DotP{} -> __IMPOSSIBLE__
LitP{} -> __IMPOSSIBLE__
ConP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
instance Apply Projection where
apply p args = p
{ projIndex = projIndex p - size args
, projLams = projLams p `apply` args
}
instance Apply ProjLams where
apply (ProjLams lams) args = ProjLams $ List.drop (length args) lams
instance Apply Defn where
apply d [] = d
apply d args = case d of
Axiom{} -> d
AbstractDefn d -> AbstractDefn $ apply d args
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Nothing } ->
d { funClauses = apply cs args
, funCompiled = apply cc args
, funInv = apply inv args
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Just p0} ->
case p0 `apply` args of
p@Projection{ projIndex = n }
| n < 0 -> __IMPOSSIBLE__
| n > 0 -> d { funProjection = Just p }
| otherwise ->
d { funClauses = apply cs args'
, funCompiled = apply cc args'
, funInv = apply inv args'
, funProjection = if isVar0 then Just p{ projIndex = 0 } else Nothing
}
where
larg = last args
args' = [larg]
isVar0 = case unArg larg of Var 0 [] -> True; _ -> False
Datatype{ dataPars = np, dataClause = cl } ->
d { dataPars = np - size args
, dataClause = apply cl args
}
Record{ recPars = np, recClause = cl, recTel = tel
} ->
d { recPars = np - size args
, recClause = apply cl args, recTel = apply tel args
}
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 cls@(Clause rl rf tel ps b t catchall unreachable) args
| length args > length ps = __IMPOSSIBLE__
| otherwise =
Clause rl rf
tel'
(applySubst rhoP $ drop (length args) ps)
(applySubst rho b)
(applySubst rho t)
catchall
unreachable
where
rargs = map unArg $ reverse args
rps = reverse $ take (length args) ps
n = size tel
tel' = newTel n tel rps rargs
rhoP :: PatternSubstitution
rhoP = mkSub dotP n rps rargs
rho = mkSub id n rps rargs
substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP i v = subst i (dotP v)
mkSub :: Subst a a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub _ _ [] [] = idS
mkSub tm n (p : ps) (v : vs) =
case namedArg p of
VarP _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v')
where v' = raise (n - 1) v
DotP{} -> mkSub tm n ps vs
ConP c _ ps' -> mkSub tm n (ps' ++ ps) (projections c v ++ vs)
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
mkSub _ _ _ _ = __IMPOSSIBLE__
newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel n tel [] [] = tel
newTel n tel (p : ps) (v : vs) =
case namedArg p of
VarP _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs
DotP{} -> newTel n tel ps vs
ConP c _ ps' -> newTel n tel (ps' ++ ps) (projections c v ++ vs)
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
newTel _ tel _ _ = __IMPOSSIBLE__
projections c v = [ applyE v [Proj ProjSystem f] | f <- conFields c ]
subTel i v EmptyTel = __IMPOSSIBLE__
subTel 0 v (ExtendTel _ tel) = absApp tel v
subTel i v (ExtendTel a tel) = ExtendTel a $ subTel (i - 1) (raise 1 v) <$> tel
instance Apply CompiledClauses where
apply cc args = case cc of
Fail -> Fail
Done hs t
| length hs >= len ->
let sub = parallelS $ map var [0..length hs - len - 1] ++ map unArg args
in Done (List.drop len hs) $ applySubst sub t
| otherwise -> __IMPOSSIBLE__
Case n bs
| unArg n >= len -> Case (n <&> \ m -> m - len) (apply bs args)
| otherwise -> __IMPOSSIBLE__
where
len = length args
instance Apply a => Apply (WithArity a) where
apply (WithArity n a) args = WithArity n $ apply a args
applyE (WithArity n a) es = WithArity n $ applyE a es
instance Apply a => Apply (Case a) where
apply (Branches cop cs eta ls m lz) args =
Branches cop (apply cs args) (second (`apply` args) <$> eta) (apply ls args) (apply m args) lz
applyE (Branches cop cs eta ls m lz) es =
Branches cop (applyE cs es) (second (`applyE` es) <$> eta)(applyE ls es) (applyE m es) lz
instance Apply FunctionInverse where
apply NotInjective args = NotInjective
apply (Inverse inv) args = Inverse $ apply inv args
instance Apply DisplayTerm where
apply (DTerm v) args = DTerm $ apply v args
apply (DDot v) args = DDot $ apply v args
apply (DCon c ci vs) args = DCon c ci $ vs ++ map (fmap DTerm) args
apply (DDef c es) args = DDef c $ es ++ map (Apply . fmap DTerm) args
apply (DWithApp v ws es) args = DWithApp v ws $ es ++ map Apply args
applyE (DTerm v) es = DTerm $ applyE v es
applyE (DDot v) es = DDot $ applyE v es
applyE (DCon c ci vs) es = DCon c ci $ vs ++ map (fmap DTerm) ws
where ws = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
applyE (DDef c es') es = DDef c $ es' ++ map (fmap DTerm) es
applyE (DWithApp v ws es') es = DWithApp v ws $ es' ++ es
instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where
apply ts args = map (`apply` args) ts
applyE ts es = map (`applyE` es) ts
instance Apply t => Apply (Blocked t) where
apply b args = fmap (`apply` args) b
applyE b es = fmap (`applyE` es) b
instance Apply t => Apply (Maybe t) where
apply x args = fmap (`apply` args) x
applyE x es = fmap (`applyE` es) x
instance Apply v => Apply (Map k v) where
apply x args = fmap (`apply` args) x
applyE x es = fmap (`applyE` es) x
instance Apply v => Apply (HashMap k v) where
apply x args = fmap (`apply` args) x
applyE x es = fmap (`applyE` es) x
instance (Apply a, Apply b) => Apply (a,b) where
apply (x,y) args = (apply x args, apply y args)
applyE (x,y) es = (applyE x es , applyE y es )
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)
applyE (x,y,z) es = (applyE x es , applyE y es , applyE z es )
instance DoDrop a => Apply (Drop a) where
apply x args = dropMore (size args) x
instance DoDrop a => Abstract (Drop a) where
abstract tel x = unDrop (size tel) x
instance Apply Permutation where
apply (Perm n xs) args = Perm (n - m) $ map (flip (-) m) $ drop 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) = lazyAbsApp b (unArg a) `piApply` args
piApply t args =
trace ("piApply t = " ++ show t ++ "\n args = " ++ show args) __IMPOSSIBLE__
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
EmptyTel `abstract` tel = tel
ExtendTel arg xtel `abstract` tel = ExtendTel arg $ xtel <&> (`abstract` tel)
instance Abstract Definition where
abstract tel (Defn info x t pol occ df m c inst copy ma inj d) =
Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) df m c inst copy ma inj (abstract tel d)
instance Abstract RewriteRule where
abstract tel (RewriteRule q gamma f ps rhs t) =
RewriteRule q (abstract tel gamma) f ps rhs t
instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
abstract tel [] = []
abstract tel occ = replicate (size tel) Mixed ++ occ
instance {-# OVERLAPPING #-} Abstract [Polarity] where
abstract tel [] = []
abstract tel pol = replicate (size tel) Invariant ++ pol
instance Abstract Projection where
abstract tel p = p
{ projIndex = size tel + projIndex p
, projLams = abstract tel $ projLams p
}
instance Abstract ProjLams where
abstract tel (ProjLams lams) = ProjLams $
map (\ (Dom ai (x, _)) -> Arg ai x) (telToList tel) ++ lams
instance Abstract Defn where
abstract tel d = case d of
Axiom{} -> d
AbstractDefn d -> AbstractDefn $ abstract tel d
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Nothing } ->
d { funClauses = abstract tel cs
, funCompiled = abstract tel cc
, funInv = abstract tel inv
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funProjection = Just p } ->
if projIndex p > 0 then d' else
d' { funClauses = abstract tel1 cs
, funCompiled = abstract tel1 cc
, funInv = abstract tel1 inv
}
where
d' = d { funProjection = Just $ abstract tel p }
tel1 = telFromList $ drop (size tel - 1) $ telToList tel
Datatype{ dataPars = np, dataClause = cl } ->
d { dataPars = np + size tel
, dataClause = abstract tel cl
}
Record{ recPars = np, recClause = cl, recTel = tel' } ->
d { recPars = np + size tel
, recClause = abstract tel cl
, recTel = abstract tel tel'
}
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 $ drop n ts
where n = size tel
instance Abstract Clause where
abstract tel (Clause rl rf tel' ps b t catchall unreachable) =
Clause rl rf (abstract tel tel')
(namedTelVars m tel ++ ps)
b
t
catchall
unreachable
where m = size tel + size tel'
instance Abstract CompiledClauses where
abstract tel Fail = Fail
abstract tel (Done xs t) = Done (map (argFromDom . fmap fst) (telToList tel) ++ xs) t
abstract tel (Case n bs) =
Case (n <&> \ i -> i + size tel) (abstract tel bs)
instance Abstract a => Abstract (WithArity a) where
abstract tel (WithArity n a) = WithArity n $ abstract tel a
instance Abstract a => Abstract (Case a) where
abstract tel (Branches cop cs eta ls m lz) =
Branches cop (abstract tel cs) (second (abstract tel) <$> eta)
(abstract tel ls) (abstract tel m) lz
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars m = map (fmap namedThing) . (namedTelVars m)
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars m EmptyTel = []
namedTelVars m (ExtendTel (Dom info a) tel) =
Arg info (namedDBVarP (m-1) $ absName tel) :
namedTelVars (m-1) (unAbs tel)
instance Abstract FunctionInverse where
abstract tel NotInjective = NotInjective
abstract tel (Inverse inv) = Inverse $ abstract tel inv
instance {-# OVERLAPPABLE #-} 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
instance Abstract v => Abstract (HashMap 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 info x) -> ExtendTel (Dom info $ sort Prop) . Abs x)
EmptyTel
$ zipWith (<$) names args
names = cycle $ map (stringToArgName . (:[])) ['a'..'z']
renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming err p = prependS err gamma $ raiseS $ size p
where
gamma :: [Maybe a]
gamma = inversePermute p (deBruijnVar :: Int -> a)
renamingR :: DeBruijn a => Permutation -> Substitution' a
renamingR p@(Perm n _) = permute (reverseP p) (map deBruijnVar [0..]) ++# raiseS n
renameP :: Subst t a => Empty -> Permutation -> a -> a
renameP err p = applySubst (renaming err p)
instance Subst a a => Subst a (Substitution' a) where
applySubst rho sgm = composeS rho sgm
instance Subst Term Term where
applySubst IdS t = t
applySubst rho t = case t of
Var i es -> lookupS rho i `applyE` applySubst rho es
Lam h m -> Lam h $ applySubst rho m
Def f es -> defApp f [] $ applySubst rho es
Con c ci vs -> Con c ci $ applySubst rho vs
MetaV x es -> MetaV x $ applySubst rho es
Lit l -> Lit l
Level l -> levelTm $ applySubst rho l
Pi a b -> uncurry Pi $ applySubst rho (a,b)
Sort s -> Sort $ applySubst rho s
DontCare mv -> dontCare $ applySubst rho mv
instance Subst Term a => Subst Term (Type' a) where
applySubst rho (El s t) = applySubst rho s `El` applySubst rho t
instance Subst Term Sort where
applySubst rho s = case s of
Type n -> Type $ sub n
Prop -> Prop
Inf -> Inf
SizeUniv -> SizeUniv
PiSort s1 s2 -> piSort (sub s1) (sub s2)
UnivSort s -> univSort $ sub s
MetaS x es -> MetaS x $ sub es
where sub x = applySubst rho x
instance Subst Term Level where
applySubst rho (Max as) = Max $ applySubst rho as
instance Subst Term PlusLevel where
applySubst rho l@ClosedLevel{} = l
applySubst rho (Plus n l) = Plus n $ applySubst rho l
instance Subst Term LevelAtom where
applySubst rho (MetaLevel m vs) = MetaLevel m $ applySubst rho vs
applySubst rho (BlockedLevel m v) = BlockedLevel m $ applySubst rho v
applySubst rho (NeutralLevel _ v) = UnreducedLevel $ applySubst rho v
applySubst rho (UnreducedLevel v) = UnreducedLevel $ applySubst rho v
instance Subst Term Name where
applySubst rho = id
instance {-# OVERLAPPING #-} Subst Term String where
applySubst rho = id
instance Subst Term ConPatternInfo where
applySubst rho i = i{ conPType = applySubst rho $ conPType i }
instance Subst Term Pattern where
applySubst rho p = case p of
ConP c mt ps -> ConP c (applySubst rho mt) $ applySubst rho ps
DotP o t -> DotP o $ applySubst rho t
VarP o s -> p
LitP l -> p
ProjP{} -> p
instance Subst Term A.ProblemEq where
applySubst rho (A.ProblemEq p v a) =
uncurry (A.ProblemEq p) $ applySubst rho (v,a)
instance DeBruijn NLPat where
deBruijnVar i = PVar i []
deBruijnView p = case p of
PVar i [] -> Just i
PVar{} -> Nothing
PWild{} -> Nothing
PDef{} -> Nothing
PLam{} -> Nothing
PPi{} -> Nothing
PBoundVar{} -> Nothing
PTerm{} -> Nothing
applyNLPatSubst :: (Subst Term a) => Substitution' NLPat -> a -> a
applyNLPatSubst = applySubst . fmap nlPatToTerm
where
nlPatToTerm :: NLPat -> Term
nlPatToTerm p = case p of
PVar i xs -> Var i $ map (Apply . fmap var) xs
PTerm u -> u
PWild -> __IMPOSSIBLE__
PDef f es -> __IMPOSSIBLE__
PLam i u -> __IMPOSSIBLE__
PPi a b -> __IMPOSSIBLE__
PBoundVar i es -> __IMPOSSIBLE__
instance Subst NLPat NLPat where
applySubst rho p = case p of
PVar i bvs -> lookupS rho i `applyBV` bvs
PWild -> p
PDef f es -> PDef f $ applySubst rho es
PLam i u -> PLam i $ applySubst rho u
PPi a b -> PPi (applySubst rho a) (applySubst rho b)
PBoundVar i es -> PBoundVar i $ applySubst rho es
PTerm u -> PTerm $ applyNLPatSubst rho u
where
applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV p ys = case p of
PVar i xs -> PVar i (xs ++ ys)
PTerm u -> PTerm $ u `apply` map (fmap var) ys
PWild -> __IMPOSSIBLE__
PDef f es -> __IMPOSSIBLE__
PLam i u -> __IMPOSSIBLE__
PPi a b -> __IMPOSSIBLE__
PBoundVar i es -> __IMPOSSIBLE__
instance Subst NLPat NLPType where
applySubst rho (NLPType s a) = NLPType (applySubst rho s) (applySubst rho a)
instance Subst NLPat RewriteRule where
applySubst rho (RewriteRule q gamma f ps rhs t) =
RewriteRule q (applyNLPatSubst rho gamma)
f (applySubst (liftS n rho) ps)
(applyNLPatSubst (liftS n rho) rhs)
(applyNLPatSubst (liftS n rho) t)
where n = size gamma
instance Subst t a => Subst t (Blocked a) where
applySubst rho b = fmap (applySubst rho) b
instance Subst Term DisplayForm where
applySubst rho (Display n ps v) =
Display n (applySubst (liftS 1 rho) ps)
(applySubst (liftS n rho) v)
instance Subst Term DisplayTerm where
applySubst rho (DTerm v) = DTerm $ applySubst rho v
applySubst rho (DDot v) = DDot $ applySubst rho v
applySubst rho (DCon c ci vs) = DCon c ci $ applySubst rho vs
applySubst rho (DDef c es) = DDef c $ applySubst rho es
applySubst rho (DWithApp v vs es) = uncurry3 DWithApp $ applySubst rho (v, vs, es)
instance Subst t a => Subst t (Tele a) where
applySubst rho EmptyTel = EmptyTel
applySubst rho (ExtendTel t tel) = uncurry ExtendTel $ applySubst rho (t, tel)
instance Subst Term Constraint where
applySubst rho c = case c of
ValueCmp cmp a u v -> ValueCmp cmp (rf a) (rf u) (rf v)
ElimCmp ps fs a v e1 e2 -> ElimCmp ps fs (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 r a -> IsEmpty r (rf a)
CheckSizeLtSat t -> CheckSizeLtSat (rf t)
FindInScope m b cands -> FindInScope m b (rf cands)
UnBlock{} -> c
CheckFunDef{} -> c
HasBiggerSort s -> HasBiggerSort (rf s)
HasPTSRule s1 s2 -> HasPTSRule (rf s1) (rf s2)
where
rf x = applySubst rho x
instance Subst t a => Subst t (Elim' a) where
applySubst rho e = case e of
Apply v -> Apply $ applySubst rho v
Proj{} -> e
instance Subst t a => Subst t (Abs a) where
applySubst rho (Abs x a) = Abs x $ applySubst (liftS 1 rho) a
applySubst rho (NoAbs x a) = NoAbs x $ applySubst rho a
instance Subst t a => Subst t (Arg a) where
applySubst IdS arg = arg
applySubst rho arg = setFreeVariables unknownFreeVariables $ fmap (applySubst rho) arg
instance Subst t a => Subst t (Named name a) where
applySubst rho = fmap (applySubst rho)
instance Subst t a => Subst t (Dom a) where
applySubst IdS dom = dom
applySubst rho dom = setFreeVariables unknownFreeVariables $ fmap (applySubst rho) dom
instance Subst t a => Subst t (Maybe a) where
applySubst rho = fmap (applySubst rho)
instance Subst t a => Subst t [a] where
applySubst rho = map (applySubst rho)
instance (Ord k, Subst t a) => Subst t (Map k a) where
applySubst rho = fmap (applySubst rho)
instance Subst Term () where
applySubst _ _ = ()
instance (Subst t a, Subst t b) => Subst t (a, b) where
applySubst rho (x,y) = (applySubst rho x, applySubst rho y)
instance (Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) where
applySubst rho (x,y,z) = (applySubst rho x, applySubst rho y, applySubst rho z)
instance (Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) where
applySubst rho (x,y,z,u) = (applySubst rho x, applySubst rho y, applySubst rho z, applySubst rho u)
instance Subst Term Candidate where
applySubst rho (Candidate u t eti ov) = Candidate (applySubst rho u) (applySubst rho t) eti ov
instance Subst Term EqualityView where
applySubst rho (OtherType t) = OtherType
(applySubst rho t)
applySubst rho (EqualityType s eq l t a b) = EqualityType
(applySubst rho s)
eq
(map (applySubst rho) l)
(applySubst rho t)
(applySubst rho a)
(applySubst rho b)
instance DeBruijn DeBruijnPattern where
debruijnNamedVar n i = varP $ DBPatVar n i
deBruijnView _ = Nothing
fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution = fmap patternToTerm
applyPatSubst :: (Subst Term a) => PatternSubstitution -> a -> a
applyPatSubst = applySubst . fromPatternSubstitution
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin o p = case patternOrigin p of
Nothing -> p
Just PatOSplit -> p
Just PatOAbsurd -> p
Just _ -> case p of
(VarP _ x) -> VarP o x
(DotP _ u) -> DotP o u
(ConP c (ConPatternInfo (Just _) b l) ps)
-> ConP c (ConPatternInfo (Just o) b l) ps
ConP{} -> __IMPOSSIBLE__
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
instance Subst DeBruijnPattern DeBruijnPattern where
applySubst IdS p = p
applySubst rho p = case p of
VarP o x ->
usePatOrigin o $
useName (dbPatVarName x) $
lookupS rho $ dbPatVarIndex x
DotP o u -> DotP o $ applyPatSubst rho u
ConP c ci ps -> ConP c ci $ applySubst rho ps
LitP x -> p
ProjP{} -> p
where
useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
useName n (VarP o x)
| isUnderscore (dbPatVarName x)
= VarP o $ x { dbPatVarName = n }
useName _ x = x
instance Subst Term Range where
applySubst _ = id
projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
projDropParsApply (Projection prop d r _ lams) o args =
case initLast $ getProjLams lams of
Nothing -> if proper then Def d $ map Apply args else __IMPOSSIBLE__
Just (pars, Arg i y) ->
let core = if proper then Lam i $ Abs y $ Var 0 [Proj o d]
else Lam i $ Abs y $ Def d [Apply $ Var 0 [] <$ r]
(pars', args') = dropCommon pars args
in List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (core `apply` args') pars'
where proper = isJust prop
type TelView = TelV Type
data TelV a = TelV { theTel :: Tele (Dom a), theCore :: a }
deriving (Show, Functor)
deriving instance (Subst t a, Eq a) => Eq (TelV a)
deriving instance (Subst t a, Ord a) => Ord (TelV a)
telView' :: Type -> TelView
telView' = telView'UpTo (-1)
telView'UpTo :: Int -> Type -> TelView
telView'UpTo 0 t = TelV EmptyTel t
telView'UpTo n t = case unEl t of
Pi a b -> absV a (absName b) $ telView'UpTo (n - 1) (absBody b)
_ -> TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' f [] t = []
bindsToTel' f (x:xs) t = fmap (f x,) t : bindsToTel' f xs (raise 1 t)
bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel = bindsToTel' nameToArgName
bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a
bindsWithHidingToTel' f [] t = []
bindsWithHidingToTel' f (WithHiding h x : xs) t =
fmap (f x,) (mapHiding (mappend h) t) : bindsWithHidingToTel' f xs (raise 1 t)
bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel
bindsWithHidingToTel = bindsWithHidingToTel' nameToArgName
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi (Dom info (x, a)) b = el $ Pi (Dom info a) (mkAbs x b)
where
el = El $ piSort (getSort a) (Abs x (getSort b))
mkLam :: Arg ArgName -> Term -> Term
mkLam a v = Lam (argInfo a) (Abs (unArg a) v)
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' reAbs = telePi where
telePi EmptyTel t = t
telePi (ExtendTel u tel) t = el $ Pi u $ reAbs b
where
b = (`telePi` t) <$> tel
el = El $ piSort (getSort u) (getSort <$> b)
telePi :: Telescope -> Type -> Type
telePi = telePi' reAbs
telePi_ :: Telescope -> Type -> Type
telePi_ = telePi' id
teleLam :: Telescope -> Term -> Term
teleLam EmptyTel t = t
teleLam (ExtendTel u tel) t = Lam (domInfo u) $ flip teleLam t <$> tel
class TeleNoAbs a where
teleNoAbs :: a -> Term -> Term
instance TeleNoAbs ListTel where
teleNoAbs tel t = foldr (\ (Dom ai (x, _)) -> Lam ai . NoAbs x) t tel
instance TeleNoAbs Telescope where
teleNoAbs tel = teleNoAbs $ telToList tel
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel _ [] = return []
typeArgsWithTel (ExtendTel dom tel) (v : vs) = (dom :) <$> typeArgsWithTel (absApp tel v) vs
typeArgsWithTel EmptyTel{} (_:_) = Nothing
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody cl = applySubst (renamingR perm) $ clauseBody cl
where perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl
deriving instance Eq Substitution
deriving instance Ord Substitution
deriving instance Eq Sort
deriving instance Ord Sort
deriving instance Eq Level
deriving instance Ord Level
deriving instance Eq PlusLevel
deriving instance Eq NotBlocked
deriving instance Eq t => Eq (Blocked t)
deriving instance Eq Candidate
deriving instance (Subst t a, Eq a) => Eq (Tele a)
deriving instance (Subst t a, Ord a) => Ord (Tele a)
deriving instance Eq Constraint
deriving instance Eq Section
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 Ord LevelAtom where
compare = compare `on` unLevelAtom
instance Eq a => Eq (Type' a) where
(==) = (==) `on` unEl
instance Ord a => Ord (Type' a) where
compare = compare `on` unEl
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 Ord Term where
Var a b `compare` Var x y = compare x a `thenCmp` compare b y
Var{} `compare` _ = LT
_ `compare` Var{} = GT
Def a b `compare` Def x y = compare (a, b) (x, y)
Def{} `compare` _ = LT
_ `compare` Def{} = GT
Con a _ b `compare` Con x _ y = compare (a, b) (x, y)
Con{} `compare` _ = LT
_ `compare` Con{} = GT
Lit a `compare` Lit x = compare a x
Lit{} `compare` _ = LT
_ `compare` Lit{} = GT
Lam a b `compare` Lam x y = compare (a, b) (x, y)
Lam{} `compare` _ = LT
_ `compare` Lam{} = GT
Pi a b `compare` Pi x y = compare (a, b) (x, y)
Pi{} `compare` _ = LT
_ `compare` Pi{} = GT
Sort a `compare` Sort x = compare a x
Sort{} `compare` _ = LT
_ `compare` Sort{} = GT
Level a `compare` Level x = compare a x
Level{} `compare` _ = LT
_ `compare` Level{} = GT
MetaV a b `compare` MetaV x y = compare (a, b) (x, y)
MetaV{} `compare` _ = LT
_ `compare` MetaV{} = GT
DontCare{} `compare` DontCare{} = EQ
instance (Subst t 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 (Subst t 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
instance (Subst t a, Eq a) => Eq (Elim' a) where
Apply a == Apply b = a == b
Proj _ x == Proj _ y = x == y
_ == _ = False
instance (Subst t a, Ord a) => Ord (Elim' a) where
Apply a `compare` Apply b = a `compare` b
Proj _ x `compare` Proj _ y = x `compare` y
Apply{} `compare` Proj{} = LT
Proj{} `compare` Apply{} = GT
univSort' :: Sort -> Maybe Sort
univSort' (Type l) = Just $ Type $ levelSuc l
univSort' s = Nothing
univSort :: Sort -> Sort
univSort s = fromMaybe (UnivSort s) $ univSort' s
funSort' :: Sort -> Sort -> Maybe Sort
funSort' a b = case (a, b) of
(Inf , _ ) -> Just Inf
(_ , Inf ) -> Just Inf
(Type (Max as) , Type (Max bs)) -> Just $ Type $ levelMax $ as ++ bs
(SizeUniv , b ) -> Just b
(_ , SizeUniv ) -> Just SizeUniv
(a , b ) -> Nothing
funSort :: Sort -> Sort -> Sort
funSort a b = fromMaybe (PiSort a (NoAbs underscore b)) $ funSort' a b
piSort' :: Sort -> Abs Sort -> Maybe Sort
piSort' a (NoAbs _ b) = funSort' a b
piSort' a bAbs@(Abs _ b) = case occurrence 0 b of
NoOccurrence -> funSort' a $ noabsApp __IMPOSSIBLE__ bAbs
Irrelevantly -> Just Inf
StronglyRigid -> Just Inf
Unguarded -> Just Inf
WeaklyRigid -> Just Inf
Flexible _ -> Nothing
piSort :: Sort -> Abs Sort -> Sort
piSort a b = fromMaybe (PiSort a b) $ piSort' a b
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 | let n = Prelude.maximum ns, n > greatestB ]
bs = subsume [ b | b@Plus{} <- as ]
greatestB | null bs = 0
| otherwise = Prelude.maximum [ 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 l = case l of
BlockedLevel _ v -> expandTm v
NeutralLevel _ v -> expandTm v
UnreducedLevel v -> expandTm v
MetaLevel{} -> [Plus 0 l]
where
expandTm v = case v of
Level (Max as) -> as
Sort (Type (Max as)) -> as
_ -> [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 ]
levelTm :: Level -> Term
levelTm l =
case l of
Max [Plus 0 l] -> unLevelAtom l
_ -> Level l
unLevelAtom :: LevelAtom -> Term
unLevelAtom (MetaLevel x es) = MetaV x es
unLevelAtom (NeutralLevel _ v) = v
unLevelAtom (UnreducedLevel v) = v
unLevelAtom (BlockedLevel _ v) = v
levelSucView :: Level -> Maybe Level
levelSucView (Max []) = Nothing
levelSucView (Max as) = Max <$> traverse atomPred as
where
atomPred :: PlusLevel -> Maybe PlusLevel
atomPred (ClosedLevel n)
| n > 0 = Just $ ClosedLevel (n-1)
| otherwise = Nothing
atomPred (Plus n l)
| n > 0 = Just $ Plus (n-1) l
| otherwise = Nothing