{-# LANGUAGE BangPatterns #-}
{-# 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.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Position
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.Monad.Options (typeInType)
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.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
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
IApply _ _ a : es0 -> lazyAbsApp b a `applyE` es0
_ -> __IMPOSSIBLE__
MetaV x es' -> MetaV x (es' ++ es)
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
Pi _ _ -> __IMPOSSIBLE__
Sort s -> Sort $ s `applyE` es
Dummy{} -> __IMPOSSIBLE__
DontCare mv -> dontCare $ mv `applyE` es
canProject :: QName -> Term -> Maybe (Arg Term)
canProject f v =
case v of
(Con (ConHead _ _ fs) _ vs) -> do
(fld, i) <- findWithIndex ((f==) . unArg) fs
setArgInfo (getArgInfo fld) <.> 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 ci args (a@IApply{} : es) = conApp ch ci (args ++ [a]) es
conApp ch@(ConHead c _ fs) ci args (Proj o f : es) =
let failure err = flip trace err $
"conApp: constructor " ++ show c ++
" with fields\n" ++ unlines (map ((" " ++) . show) fs) ++
" and args\n" ++ unlines (map ((" " ++) . prettyShow) args) ++
" projected by " ++ show f
isApply e = fromMaybe (failure __IMPOSSIBLE__) $ isApplyElim e
(fld, i) = fromMaybe (failure __IMPOSSIBLE__) $ findWithIndex ((f==) . unArg) fs
v = maybe (failure __IMPOSSIBLE__) (relToDontCare fld . 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) = relToDontCare ai v
relToDontCare :: LensRelevance a => a -> Term -> Term
relToDontCare ai v
| Irrelevant <- getRelevance ai = dontCare v
| otherwise = v
instance Apply Sort where
applyE s [] = s
applyE s es = case s of
MetaS x es' -> MetaS x $ es' ++ es
DefS d es' -> DefS d $ es' ++ es
_ -> __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
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply Definition where
apply (Defn info x t pol occ gens gpars df m c inst copy ma nc inj d) args =
Defn info x (piApply t args) (apply pol args) (apply occ args) (apply gens args) (drop (length args) gpars) df m c inst copy ma nc inj (apply d args)
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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)
}
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
apply occ args = List.drop (length args) occ
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance {-# OVERLAPPING #-} Apply [Polarity] where
apply pol args = List.drop (length args) pol
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply NumGeneralizableArgs where
apply NoGeneralizableArgs args = NoGeneralizableArgs
apply (SomeGeneralizableArgs n) args = SomeGeneralizableArgs (n - length args)
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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__
DefP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
IApplyP{} -> recurse
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply Projection where
apply p args = p
{ projIndex = projIndex p - size args
, projLams = projLams p `apply` args
}
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply ProjLams where
apply (ProjLams lams) args = ProjLams $ List.drop (length args) lams
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply Defn where
apply d [] = d
apply d args = case d of
Axiom{} -> d
DataOrRecSig n -> DataOrRecSig (n - length args)
GeneralizableVar{} -> d
AbstractDefn d -> AbstractDefn $ apply d args
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funExtLam = extLam
, funProjection = Nothing } ->
d { funClauses = apply cs args
, funCompiled = apply cc args
, funInv = apply inv args
, funExtLam = modifySystem (`apply` args) <$> extLam
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funExtLam = extLam
, funProjection = Just p0} ->
case p0 `apply` args of
p@Projection{ projIndex = n }
| n < 0 -> d { funProjection = __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
, funExtLam = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam
}
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 }
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply PrimFun where
apply (PrimFun x ar def) args = PrimFun x (ar - size args) $ \ vs -> def (args ++ vs)
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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)
DefP o q ps' -> mkSub tm n (ps' ++ ps) vs
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
IApplyP _ _ _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v')
where v' = raise (n - 1) v
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)
DefP _ q ps' -> newTel n tel (ps' ++ ps) vs
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
IApplyP _ _ _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs
newTel _ tel _ _ = __IMPOSSIBLE__
projections c v = [ relToDontCare ai $ applyE v [Proj ProjSystem f] | Arg ai 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
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply ExtLamInfo where
apply (ExtLamInfo m sys) args = ExtLamInfo m (apply sys args)
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
instance Apply System where
apply (System tel sys) args
= if nargs > ntel then __IMPOSSIBLE__
else System newTel (map (map (f -*- id) -*- f) sys)
where
f = applySubst sigma
nargs = length args
ntel = size tel
newTel = apply tel args
sigma = liftS (ntel - nargs) (parallelS (reverse $ map unArg args))
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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 b lz) args =
Branches cop (apply cs args) (second (`apply` args) <$> eta) (apply ls args) (apply m args) b lz
applyE (Branches cop cs eta ls m b lz) es =
Branches cop (applyE cs es) (second (`applyE` es) <$> eta)(applyE ls es) (applyE m es) b lz
instance Apply FunctionInverse where
apply NotInjective args = NotInjective
apply (Inverse inv) args = Inverse $ apply inv args
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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
applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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 gens gpars df m c inst copy ma nc inj d) =
Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) (abstract tel gens)
(replicate (size tel) Nothing ++ gpars) df m c inst copy ma nc 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 NumGeneralizableArgs where
abstract tel NoGeneralizableArgs = NoGeneralizableArgs
abstract tel (SomeGeneralizableArgs n) = SomeGeneralizableArgs (size tel + n)
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 -> argFromDom (fst <$> dom)) (telToList tel) ++ lams
instance Abstract System where
abstract tel (System tel1 sys) = System (abstract tel tel1) sys
instance Abstract Defn where
abstract tel d = case d of
Axiom{} -> d
DataOrRecSig n -> DataOrRecSig (size tel + n)
GeneralizableVar{} -> d
AbstractDefn d -> AbstractDefn $ abstract tel d
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funExtLam = extLam
, funProjection = Nothing } ->
d { funClauses = abstract tel cs
, funCompiled = abstract tel cc
, funInv = abstract tel inv
, funExtLam = modifySystem (abstract tel) <$> extLam
}
Function{ funClauses = cs, funCompiled = cc, funInv = inv
, funExtLam = extLam
, funProjection = Just p } ->
if projIndex p > 0 then d' else
d' { funClauses = abstract tel1 cs
, funCompiled = abstract tel1 cc
, funInv = abstract tel1 inv
, funExtLam = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam
}
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 b lz) =
Branches cop (abstract tel cs) (second (abstract tel) <$> eta)
(abstract tel ls) (abstract tel m) b 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 tel) =
Arg (domInfo dom) (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@(Arg info x) -> ExtendTel (__DUMMY_TYPE__ <$ domFromArg arg) . 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
Dummy{} -> t
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 n -> Prop $ sub n
Inf -> Inf
SizeUniv -> SizeUniv
PiSort s1 s2 -> piSort (sub s1) (sub s2)
UnivSort s -> univSort Nothing $ sub s
MetaS x es -> MetaS x $ sub es
DefS d es -> DefS d $ sub es
DummyS{} -> s
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
DefP o q ps -> DefP o q $ applySubst rho ps
DotP o t -> DotP o $ applySubst rho t
VarP o s -> p
LitP l -> p
ProjP{} -> p
IApplyP o t u x -> IApplyP o (applySubst rho t) (applySubst rho u) x
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)
ValueCmpOnFace cmp p t u v -> ValueCmpOnFace cmp (rf p) (rf t) (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)
FindInstance m b cands -> FindInstance m b (rf cands)
UnBlock{} -> c
CheckFunDef{} -> c
HasBiggerSort s -> HasBiggerSort (rf s)
HasPTSRule s1 s2 -> HasPTSRule (rf s1) (rf s2)
UnquoteTactic m t h g -> UnquoteTactic m (rf t) (rf h) (rf g)
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
IApply x y r -> IApply (applySubst rho x) (applySubst rho y) (applySubst rho r)
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 ov) = Candidate (applySubst rho u) (applySubst rho t) 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 _) ft b l) ps)
-> ConP c (ConPatternInfo (Just o) ft b l) ps
DefP _ q ps -> DefP o q ps
ConP{} -> __IMPOSSIBLE__
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
(IApplyP _ t u x) -> IApplyP o t u x
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
DefP o q ps -> DefP o q $ applySubst rho ps
LitP x -> p
ProjP{} -> p
IApplyP o t u x -> case useName (dbPatVarName x) $ lookupS rho $ dbPatVarIndex x of
IApplyP _ _ _ y -> IApplyP o (applyPatSubst rho t) (applyPatSubst rho u) y
VarP _ y -> IApplyP o (applyPatSubst rho t) (applyPatSubst rho u) y
_ -> __IMPOSSIBLE__
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
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel [] t = EmptyTel
namedBindsToTel (x : xs) t =
ExtendTel (t <$ domFromNamedArgName x) $ Abs (nameToArgName $ namedArg x) $ namedBindsToTel xs (raise 1 t)
domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName x = () <$ domFromNamedArg (fmap forceName x)
where
forceName (Named Nothing x) = Named (Just $ Ranged (getRange x) $ nameToArgName x) x
forceName x = x
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi !dom b = el $ Pi a (mkAbs x b)
where
x = fst $ unDom dom
a = snd <$> dom
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{domInfo = ai, unDom = (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
Dummy{} == Dummy{} = True
_ == _ = False
instance Eq a => Eq (Pattern' a) where
VarP _ x == VarP _ y = x == y
DotP _ u == DotP _ v = u == v
ConP c _ ps == ConP c' _ qs = c == c && ps == qs
LitP l == LitP l' = l == l'
ProjP _ f == ProjP _ g = f == g
IApplyP _ u v x == IApplyP _ u' v' y = u == u' && v == v' && x == y
DefP _ f ps == DefP _ g qs = f == g && ps == qs
_ == _ = 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
DontCare{} `compare` _ = LT
_ `compare` DontCare{} = GT
Dummy{} `compare` Dummy{} = 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
IApply x y r == IApply x' y' r' = x == x' && y == y' && r == r'
_ == _ = 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
IApply x y r `compare` IApply x' y' r' = compare x x' `mappend` compare y y' `mappend` compare r r'
Apply{} `compare` _ = LT
_ `compare` Apply{} = GT
Proj{} `compare` _ = LT
_ `compare` Proj{} = GT
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' univInf (Type l) = Just $ Type $ levelSuc l
univSort' univInf (Prop l) = Just $ Type $ levelSuc l
univSort' univInf Inf = univInf
univSort' univInf s = Nothing
univSort :: Maybe Sort -> Sort -> Sort
univSort univInf s = fromMaybe (UnivSort s) $ univSort' univInf s
univInf :: (HasOptions m) => m (Maybe Sort)
univInf =
ifM ((optOmegaInOmega <$> pragmaOptions) `or2M` typeInType)
(return $ Just Inf)
(return Nothing)
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
(Prop (Max as) , Type (Max bs)) -> Just $ Type $ levelMax $ as ++ bs
(Type (Max as) , Prop (Max bs)) -> Just $ Prop $ levelMax $ as ++ bs
(Prop (Max as) , Prop (Max bs)) -> Just $ Prop $ levelMax $ as ++ bs
(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 -> Just $ 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