{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# 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 (second)
import Control.Monad (guard)
import Data.Coerce
import Data.Function
import qualified Data.List as List
import Data.Map (Map)
import Data.Maybe
import Data.HashMap.Strict (HashMap)
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.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 qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-}
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-}
applyTermE :: forall t. (Coercible Term t, Apply t, Subst t t)
=> (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE err' m [] = m
applyTermE err' m es = coerce $
case coerce m of
Var i es' -> Var i (es' ++ es)
Def f es' -> defApp f es' es
Con c ci args -> conApp @t err' c ci args es
Lam _ b ->
case es of
Apply a : es0 -> lazyAbsApp (coerce b :: Abs t) (coerce $ unArg a) `app` es0
IApply _ _ a : es0 -> lazyAbsApp (coerce b :: Abs t) (coerce a) `app` es0
_ -> err __IMPOSSIBLE__
MetaV x es' -> MetaV x (es' ++ es)
Lit{} -> err __IMPOSSIBLE__
Level{} -> err __IMPOSSIBLE__
Pi _ _ -> err __IMPOSSIBLE__
Sort s -> Sort $ s `applyE` es
Dummy s es' -> Dummy s (es' ++ es)
DontCare mv -> dontCare $ mv `app` es
where
app :: Coercible t x => x -> Elims -> Term
app t es = coerce $ (coerce t :: t) `applyE` es
err e = err' e (coerce m) es
instance Apply Term where
applyE = applyTermE absurd
instance Apply BraveTerm where
applyE = applyTermE (\ _ t es -> Dummy "applyE" (Apply (defaultArg t) : es))
canProject :: QName -> Term -> Maybe (Arg Term)
canProject f v =
case v of
(Con (ConHead _ _ fs) _ vs) -> do
(fld, i) <- findWithIndex ((f==) . unArg) fs
guard $ not $ isIrrelevant fld
setArgInfo (getArgInfo fld) <.> isApplyElim =<< listToMaybe (drop i vs)
_ -> Nothing
conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp fk ch ci args [] = Con ch ci args
conApp fk ch ci args (a@Apply{} : es) = conApp @t fk ch ci (args ++ [a]) es
conApp fk ch ci args (a@IApply{} : es) = conApp @t fk ch ci (args ++ [a]) es
conApp fk ch@(ConHead c _ fs) ci args ees@(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
stuck err = fk err (Con ch ci args) [Proj o f]
app :: Term -> Elims -> Term
app v es = coerce $ applyE (coerce v :: t) es
in
case findWithIndex ((f==) . unArg) fs of
Nothing -> failure $ stuck __IMPOSSIBLE__ `app` es
Just (fld, i) -> let
v = maybe (failure $ stuck __IMPOSSIBLE__) (relToDontCare fld . argToDontCare . isApply) $ listToMaybe $ drop i args
in v `app` 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 copat blk 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 copat blk (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, funCovering = cov, funInv = inv
, funExtLam = extLam
, funProjection = Nothing } ->
d { funClauses = apply cs args
, funCompiled = apply cc args
, funCovering = apply cov args
, funInv = apply inv args
, funExtLam = modifySystem (`apply` args) <$> extLam
}
Function{ funClauses = cs, funCompiled = cc, funCovering = cov, 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'
, funCovering = apply cov 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 recursive unreachable ell) args
| length args > length ps = __IMPOSSIBLE__
| otherwise =
Clause rl rf
tel'
(applySubst rhoP $ drop (length args) ps)
(applySubst rho b)
(applySubst rho t)
catchall
recursive
unreachable
ell
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 t => Apply (Strict.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 copat blk 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 copat blk (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, funCovering = cov, funInv = inv
, funExtLam = extLam
, funProjection = Nothing } ->
d { funClauses = abstract tel cs
, funCompiled = abstract tel cc
, funCovering = abstract tel cov
, funInv = abstract tel inv
, funExtLam = modifySystem (abstract tel) <$> extLam
}
Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv
, funExtLam = extLam
, funProjection = Just p } ->
if projIndex p > 0 then d' else
d' { funClauses = abstract tel1 cs
, funCompiled = abstract tel1 cc
, funCovering = abstract tel1 cov
, 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 recursive unreachable ell) =
Clause rl rf (abstract tel tel')
(namedTelVars m tel ++ ps)
b
t
catchall
recursive
unreachable
ell
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
{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
applySubstTerm :: forall t. (Coercible t Term, Subst t t, Apply t) => Substitution' t -> t -> t
applySubstTerm IdS t = t
applySubstTerm rho t = coerce $ case coerce t of
Var i es -> coerce $ lookupS rho i `applyE` subE es
Lam h m -> Lam h $ sub @(Abs t) m
Def f es -> defApp f [] $ subE es
Con c ci vs -> Con c ci $ subE vs
MetaV x es -> MetaV x $ subE es
Lit l -> Lit l
Level l -> levelTm $ sub @(Level' t) l
Pi a b -> uncurry Pi $ subPi (a,b)
Sort s -> Sort $ sub @(Sort' t) s
DontCare mv -> dontCare $ sub @t mv
Dummy s es -> Dummy s $ subE es
where
sub :: forall a b. (Coercible b a, Subst t a) => b -> b
sub t = coerce $ applySubst rho (coerce t :: a)
subE :: Elims -> Elims
subE = sub @[Elim' t]
subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi = sub @(Dom' t (Type'' t t), Abs (Type'' t t))
instance Subst Term Term where
applySubst = applySubstTerm
instance Subst BraveTerm BraveTerm where
applySubst = applySubstTerm
instance (Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) where
applySubst rho (El s t) = applySubst rho s `El` applySubst rho t
instance (Coercible a Term, Subst t a) => Subst t (Sort' a) where
applySubst rho s = case s of
Type n -> Type $ sub n
Prop n -> Prop $ sub n
Inf -> Inf
SizeUniv -> SizeUniv
PiSort a s2 -> coerce $ piSort (coerce $ sub a) (coerce $ sub s2)
FunSort s1 s2 -> coerce $ funSort (coerce $ sub s1) (coerce $ sub s2)
UnivSort s -> coerce $ univSort Nothing $ coerce $ 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 t a => Subst t (Level' a) where
applySubst rho (Max n as) = Max n $ applySubst rho as
instance Subst t a => Subst t (PlusLevel' a) where
applySubst rho (Plus n l) = Plus n $ applySubst rho l
instance Subst t a => Subst t (LevelAtom' a) 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 o 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 BraveTerm where
deBruijnVar = BraveTerm . deBruijnVar
deBruijnView = deBruijnView . unBrave
instance DeBruijn NLPat where
deBruijnVar i = PVar i []
deBruijnView p = case p of
PVar i [] -> Just i
PVar{} -> Nothing
PDef{} -> Nothing
PLam{} -> Nothing
PPi{} -> Nothing
PSort{} -> 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
PDef f es -> __IMPOSSIBLE__
PLam i u -> __IMPOSSIBLE__
PPi a b -> __IMPOSSIBLE__
PSort s -> __IMPOSSIBLE__
PBoundVar i es -> __IMPOSSIBLE__
applyNLSubstToDom :: Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom rho dom = applySubst rho <$> dom{ domTactic = applyNLPatSubst rho $ domTactic dom }
instance Subst NLPat NLPat where
applySubst rho p = case p of
PVar i bvs -> lookupS rho i `applyBV` bvs
PDef f es -> PDef f $ applySubst rho es
PLam i u -> PLam i $ applySubst rho u
PPi a b -> PPi (applyNLSubstToDom rho a) (applySubst rho b)
PSort s -> PSort $ applySubst rho s
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
PDef f es -> __IMPOSSIBLE__
PLam i u -> __IMPOSSIBLE__
PPi a b -> __IMPOSSIBLE__
PSort s -> __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 NLPSort where
applySubst rho = \case
PType l -> PType $ applySubst rho l
PProp l -> PProp $ applySubst rho l
PInf -> PInf
PSizeUniv -> PSizeUniv
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)
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 a s -> HasPTSRule (rf a) (rf s)
UnquoteTactic m t h g -> UnquoteTactic m (rf t) (rf h) (rf g)
CheckMetaInst m -> CheckMetaInst m
where
rf x = applySubst rho x
instance Subst Term CompareAs where
applySubst rho (AsTermsOf a) = AsTermsOf $ applySubst rho a
applySubst rho AsSizes = AsSizes
applySubst rho AsTypes = AsTypes
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 b) => Subst t (Dom' a b) where
applySubst IdS dom = dom
applySubst rho dom = setFreeVariables unknownFreeVariables $
fmap (applySubst rho) dom{ domTactic = applySubst rho (domTactic dom) }
instance Subst t a => Subst t (Maybe a) where
instance Subst t a => Subst t [a] where
instance (Ord k, Subst t a) => Subst t (Map k a) where
instance Subst t a => Subst t (WithHiding a) where
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 a => DeBruijn (Pattern' a) where
debruijnNamedVar n i = varP $ debruijnNamedVar 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 patternInfo p of
Nothing -> p
Just i -> usePatternInfo (i { patOrigin = o }) p
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo i p = case patternOrigin p of
Nothing -> p
Just PatOSplit -> p
Just PatOAbsurd -> p
Just _ -> case p of
(VarP _ x) -> VarP i x
(DotP _ u) -> DotP i u
(ConP c (ConPatternInfo _ r ft b l) ps)
-> ConP c (ConPatternInfo i r ft b l) ps
DefP _ q ps -> DefP i q ps
(LitP _ l) -> LitP i l
ProjP{} -> __IMPOSSIBLE__
(IApplyP _ t u x) -> IApplyP i t u x
instance Subst DeBruijnPattern DeBruijnPattern where
applySubst IdS p = p
applySubst rho p = case p of
VarP i x ->
usePatternInfo i $
useName (dbPatVarName x) $
lookupS rho $ dbPatVarIndex x
DotP i u -> DotP i $ applyPatSubst rho u
ConP c ci ps -> ConP c ci $ applySubst rho ps
DefP i q ps -> DefP i q $ applySubst rho ps
LitP i x -> p
ProjP{} -> p
IApplyP i t u x -> case useName (dbPatVarName x) $ lookupS rho $ dbPatVarIndex x of
IApplyP _ _ _ y -> IApplyP i (applyPatSubst rho t) (applyPatSubst rho u) y
VarP _ y -> IApplyP i (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 -> Relevance -> Args -> Term
projDropParsApply (Projection prop d r _ lams) o rel args =
case initLast $ getProjLams lams of
Nothing -> if proper then Def d $ map Apply args else __IMPOSSIBLE__
Just (pars, Arg i y) ->
let irr = isIrrelevant rel
core
| proper && not irr = Lam i $ Abs y $ Var 0 [Proj o d]
| otherwise = 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 Term a, Eq a) => Eq (TelV a)
deriving instance (Subst Term 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 $ WithOrigin Inserted $ 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 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 u (getSort <$> b)
telePi :: Telescope -> Type -> Type
telePi = telePi' reAbs
telePi_ :: Telescope -> Type -> Type
telePi_ = telePi' id
telePiVisible :: Telescope -> Type -> Type
telePiVisible EmptyTel t = t
telePiVisible (ExtendTel u tel) t
| notVisible u, NoAbs x t' <- b' = t'
| otherwise = El (piSort u $ getSort <$> b) $ Pi u b
where
b = tel <&> (`telePiVisible` t)
b' = reAbs b
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 CompareAs
deriving instance Eq Section
instance Ord PlusLevel where
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
a == b = absBody a == absBody b
instance (Subst t a, Ord a) => Ord (Abs a) where
NoAbs _ a `compare` NoAbs _ b = a `compare` b
a `compare` b = absBody a `compare` absBody b
deriving instance Ord a => Ord (Dom a)
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 a , Type b) -> Just $ Type $ levelLub a b
(SizeUniv , b ) -> Just b
(_ , SizeUniv ) -> Just SizeUniv
(Prop a , Type b) -> Just $ Type $ levelLub a b
(Type a , Prop b) -> Just $ Prop $ levelLub a b
(Prop a , Prop b) -> Just $ Prop $ levelLub a b
(a , b ) -> Nothing
funSort :: Sort -> Sort -> Sort
funSort a b = fromMaybe (FunSort a b) $ funSort' a b
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' a (NoAbs _ b) = funSort' (getSort a) b
piSort' a bAbs@(Abs _ b) = case flexRigOccurrenceIn 0 b of
Nothing -> Just $ funSort (getSort a) $ noabsApp __IMPOSSIBLE__ bAbs
Just o -> case o of
StronglyRigid -> Just Inf
Unguarded -> Just Inf
WeaklyRigid -> Just Inf
Flexible _ -> Nothing
piSort :: Dom Type -> Abs Sort -> Sort
piSort a b = case piSort' a b of
Just s -> s
Nothing | NoAbs _ b' <- b -> FunSort (getSort a) b'
| otherwise -> PiSort a b
levelMax :: Integer -> [PlusLevel] -> Level
levelMax n0 as0 = Max n as
where
Max n1 as1 = expandLevel $ Max n0 as0
as2 = removeSubsumed as1
as = List.sort as2
greatestB = Prelude.maximum $ 0 : [ n | Plus n _ <- as ]
n | n1 > greatestB = n1
| otherwise = 0
lmax :: Integer -> [PlusLevel] -> [Level] -> Level
lmax m as [] = Max m as
lmax m as (Max n bs : ls) = lmax (max m n) (bs ++ as) ls
expandLevel :: Level -> Level
expandLevel (Max m as) = lmax m [] $ map expandPlus as
expandPlus :: PlusLevel -> Level
expandPlus (Plus m l) = levelPlus m $ expandAtom l
expandAtom :: LevelAtom -> Level
expandAtom l = case l of
BlockedLevel _ v -> expandTm v
NeutralLevel _ v -> expandTm v
UnreducedLevel v -> expandTm v
MetaLevel{} -> Max 0 [Plus 0 l]
where
expandTm (Level l) = expandLevel l
expandTm (Sort (Type l)) = expandLevel l
expandTm v = Max 0 [Plus 0 l]
removeSubsumed [] = []
removeSubsumed (Plus n a : bs)
| not $ null ns = removeSubsumed bs
| otherwise = Plus n a : removeSubsumed [ b | b@(Plus _ a') <- bs, a /= a' ]
where
ns = [ m | Plus m a' <- bs, a == a', m > n ]
levelLub :: Level -> Level -> Level
levelLub (Max m as) (Max n bs) = levelMax (max m n) $ as ++ bs
levelTm :: Level -> Term
levelTm l =
case l of
Max 0 [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