{-# 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 Prelude hiding ( zip, zipWith )
import Data.Coerce
import Data.Function (on)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map.Strict as MapS
import Data.Maybe
import Data.HashMap.Strict (HashMap)
import Debug.Trace (trace)
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
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
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.Either
import Agda.Utils.Empty
import Agda.Utils.Function (applyWhen, applyUnless, ($$!))
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.ListInf as ListInf
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Zip
{-# INLINE applyTermE #-}
applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t)
=> (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE :: forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE Empty -> Term -> Elims -> Term
err' = \t
m Elims
es -> case Elims
es of
[] -> t
m
Elims
es -> Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$
case t -> Term
forall a b. Coercible a b => a -> b
coerce t
m of
Var Int
i Elims
es' -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
Def QName
f Elims
es' -> QName -> Elims -> Elims -> Term
defApp QName
f Elims
es' Elims
es
Con ConHead
c ConInfo
ci Elims
args -> forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
err' ConHead
c ConInfo
ci Elims
args Elims
es
Lam ArgInfo
_ Abs Term
b ->
case Elims
es of
Apply Arg Term
a : Elims
es0 -> Abs t -> SubstArg t -> t
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> SubstArg t
forall a b. Coercible a b => a -> b
coerce (Term -> SubstArg t) -> Term -> SubstArg t
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) t -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es0
IApply Term
_ Term
_ Term
a : Elims
es0 -> Abs t -> SubstArg t -> t
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
a) t -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es0
Elims
_ -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
MetaV MetaId
x Elims
es' -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
Lit{} -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
Level{} -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
Pi Dom Type
_ Abs Type
_ -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
Sort Sort' Term
s -> Sort' Term -> Term
Sort (Sort' Term -> Term) -> Sort' Term -> Term
forall a b. (a -> b) -> a -> b
$ Sort' Term
s Sort' Term -> Elims -> Sort' Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
Dummy DummyTermKind
s Elims
es' -> DummyTermKind -> Elims -> Term
Dummy DummyTermKind
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
DontCare Term
mv -> Term -> Term
dontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
mv Term -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es
where
{-# INLINE app #-}
app :: Coercible t a => a -> Elims -> Term
app :: forall a. Coercible t a => a -> Elims -> Term
app a
u Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ (a -> t
forall a b. Coercible a b => a -> b
coerce a
u :: t) t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
err :: Empty -> Term
err Empty
e = Empty -> Term -> Elims -> Term
err' Empty
e (t -> Term
forall a b. Coercible a b => a -> b
coerce t
m) Elims
es
instance Apply Term where
applyE :: Term -> Elims -> Term
applyE = (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term
forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE Empty -> Term -> Elims -> Term
forall a. Empty -> a
absurd
instance Apply BraveTerm where
applyE :: BraveTerm -> Elims -> BraveTerm
applyE = (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm
forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE (\ Empty
_ Term
t Elims
es -> DummyTermKind -> Elims -> Term
Dummy (Term -> DummyTermKind
DummyBrave Term
t) Elims
es)
{-# INLINE canProject #-}
canProject :: QName -> Term -> Maybe (Arg Term)
canProject :: QName -> Term -> Maybe (Arg Term)
canProject QName
f Term
v =
case Term
v of
(Con (ConHead QName
_ DataOrRecord
_ Induction
_ [Arg QName]
fs) ConInfo
_ Elims
vs) ->
(Arg QName -> Bool)
-> [Arg QName]
-> Maybe (Arg Term)
-> (Arg QName -> Int -> Maybe (Arg Term))
-> Maybe (Arg Term)
forall a b. (a -> Bool) -> [a] -> b -> (a -> Int -> b) -> b
findWithIndex' ((QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> QName
forall e. Arg e -> e
unArg) [Arg QName]
fs Maybe (Arg Term)
forall a. Maybe a
Nothing \Arg QName
fld Int
i -> do
Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Arg QName -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg QName
fld
ArgInfo -> Arg Term -> Arg Term
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (Arg QName -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg QName
fld) (Arg Term -> Arg Term)
-> (Elim' Term -> Maybe (Arg Term))
-> Elim' Term
-> Maybe (Arg Term)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim (Elim' Term -> Maybe (Arg Term))
-> Maybe (Elim' Term) -> Maybe (Arg Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> Maybe (Elim' Term)
forall a. [a] -> Maybe a
listToMaybe (Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop Int
i Elims
vs)
Term
_ -> Maybe (Arg Term)
forall a. Maybe a
Nothing
{-# INLINE conApp #-}
conApp :: forall t. (Coercible t Term, Apply t)
=> (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp :: forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp Empty -> Term -> Elims -> Term
fallback ch :: ConHead
ch@(ConHead QName
c DataOrRecord
_ Induction
_ [Arg QName]
fs) ConInfo
ci Elims
args Elims
topEs = Elims -> Term
go Elims
topEs where
{-# INLINE traceProjFailure #-}
traceProjFailure :: forall a. QName -> a -> a
traceProjFailure :: forall a. QName -> a -> a
traceProjFailure QName
f a
err = QName -> QName -> [Arg QName] -> Elims -> Elims -> a -> a
forall {a} {a} {a} {a} {a}.
(Pretty a, Pretty a, Pretty a, Pretty a) =>
a -> a -> [a] -> [Elim' a] -> [Elim' a] -> a -> a
go QName
c QName
f [Arg QName]
fs Elims
args Elims
topEs a
err where
{-# NOINLINE go #-}
go :: a -> a -> [a] -> [Elim' a] -> [Elim' a] -> a -> a
go a
c a
f [a]
fs [Elim' a]
args [Elim' a]
es a
err =
let argsBeforeProj :: [Elim' a]
argsBeforeProj = (Elim' a -> Bool) -> [Elim' a] -> [Elim' a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile' (\case Proj{} -> Bool
False; Elim' a
_ -> Bool
True) ([Elim' a]
args [Elim' a] -> [Elim' a] -> [Elim' a]
forall a. [a] -> [a] -> [a]
++! [Elim' a]
es)
in [Char] -> a -> a
forall a. [Char] -> a -> a
trace ([[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char]
"conApp: constructor ", a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
c
, [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
" with fields" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (a -> [Char]) -> [a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++!) ([Char] -> [Char]) -> (a -> [Char]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [a]
fs
, [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
" and args" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Elim' a -> [Char]) -> [Elim' a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++!) ([Char] -> [Char]) -> (Elim' a -> [Char]) -> Elim' a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [Elim' a]
argsBeforeProj
, [Char]
" projected by ", a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
f
]) a
err
stuck :: Empty -> Term
stuck :: Empty -> Term
stuck Empty
err = Empty -> Term -> Elims -> Term
fallback Empty
err (ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args) Elims
topEs
go :: Elims -> Term
go :: Elims -> Term
go = \case
[] -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
topEs
Apply{} : Elims
es -> Elims -> Term
go Elims
es
IApply{} : Elims
es -> Elims -> Term
go Elims
es
Proj ProjOrigin
o QName
f : Elims
es -> [Arg QName] -> Elims -> Term
lookupProj [Arg QName]
fs Elims
args where
fieldNotFound :: Term
fieldNotFound :: Term
fieldNotFound = QName -> Term -> Term
forall a. QName -> a -> a
traceProjFailure QName
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
project :: Arg QName -> Arg Term -> Term
project :: Arg QName -> Arg Term -> Term
project Arg QName
fld Arg Term
a =
let !v :: Term
v = Arg QName -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare Arg QName
fld (Arg Term -> Term
argToDontCare Arg Term
a) in t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
applyE (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
v :: t) Elims
es)
lookupProj :: [Arg QName] -> Elims -> Term
lookupProj :: [Arg QName] -> Elims -> Term
lookupProj (Arg QName
fld:[Arg QName]
fs) (Elim' Term
a:Elims
args)
| QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fld = case Elim' Term
a of
Proj{} -> QName -> Term -> Term
forall a. QName -> a -> a
traceProjFailure QName
f Term
forall a. HasCallStack => a
__IMPOSSIBLE__
Apply Arg Term
a -> Arg QName -> Arg Term -> Term
project Arg QName
fld Arg Term
a
IApply Term
_ Term
_ Term
a -> Arg QName -> Arg Term -> Term
project Arg QName
fld (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
a)
| Bool
otherwise = [Arg QName] -> Elims -> Term
lookupProj [Arg QName]
fs Elims
args
lookupProj [Arg QName]
fs [] = [Arg QName] -> Elims -> Term
lookupFromElims [Arg QName]
fs Elims
topEs
lookupProj [] Elims
_ = Term
fieldNotFound
lookupFromElims :: [Arg QName] -> Elims -> Term
lookupFromElims :: [Arg QName] -> Elims -> Term
lookupFromElims (Arg QName
fld:[Arg QName]
fs) (Elim' Term
a:Elims
es)
| QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fld = case Elim' Term
a of
Proj{} -> Term
fieldNotFound
Apply Arg Term
a -> Arg QName -> Arg Term -> Term
project Arg QName
fld Arg Term
a
IApply Term
_ Term
_ Term
a -> Arg QName -> Arg Term -> Term
project Arg QName
fld (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
a)
| Bool
otherwise = [Arg QName] -> Elims -> Term
lookupFromElims [Arg QName]
fs Elims
es
lookupFromElims [Arg QName]
_ Elims
_ = Term
fieldNotFound
defApp :: QName -> Elims -> Elims -> Term
defApp :: QName -> Elims -> Elims -> Term
defApp QName
f [] (Apply Arg Term
a : Elims
es) | Just Arg Term
v <- QName -> Term -> Maybe (Arg Term)
canProject QName
f (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
= Arg Term -> Term
argToDontCare Arg Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
defApp QName
f Elims
es0 Elims
es = QName -> Elims -> Term
Def QName
f (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
argToDontCare :: Arg Term -> Term
argToDontCare :: Arg Term -> Term
argToDontCare (Arg ArgInfo
ai Term
v) = ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai Term
v
relToDontCare :: LensRelevance a => a -> Term -> Term
relToDontCare :: forall a. LensRelevance a => a -> Term -> Term
relToDontCare a
ai = Bool -> (Term -> Term) -> Term -> Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (a -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant a
ai) Term -> Term
dontCare
instance Apply Sort where
applyE :: Sort' Term -> Elims -> Sort' Term
applyE Sort' Term
s [] = Sort' Term
s
applyE Sort' Term
s Elims
es = case Sort' Term
s of
MetaS MetaId
x Elims
es' -> MetaId -> Elims -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort' Term) -> Elims -> Sort' Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
DefS QName
d Elims
es' -> QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d (Elims -> Sort' Term) -> Elims -> Sort' Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
Sort' Term
_ -> Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__
instance TermSubst a => Apply (Tele a) where
apply :: Tele a -> [Arg Term] -> Tele a
apply Tele a
tel [] = Tele a
tel
apply Tele a
EmptyTel [Arg Term]
_ = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
apply (ExtendTel a
_ Abs (Tele a)
tel) (Arg Term
t : [Arg Term]
ts) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs (Tele a)
tel (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) Tele a -> [Arg Term] -> Tele a
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts
applyE :: Tele a -> Elims -> Tele a
applyE Tele a
t Elims
es = Tele a -> [Arg Term] -> Tele a
forall t. Apply t => t -> [Arg Term] -> t
apply Tele a
t ([Arg Term] -> Tele a) -> [Arg Term] -> Tele a
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply Definition where
apply :: Definition -> [Arg Term] -> Definition
apply (Defn ArgInfo
info QName
x Type
t [Polarity]
pol [Occurrence]
occ [Maybe Name]
gpars [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Bool
hasm Defn
d) [Arg Term]
args =
ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe InstanceInfo
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Bool
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Type -> [Arg Term] -> Type
piApply Type
t [Arg Term]
args) ([Polarity] -> [Arg Term] -> [Polarity]
forall t. Apply t => t -> [Arg Term] -> t
apply [Polarity]
pol [Arg Term]
args) ([Occurrence] -> [Arg Term] -> [Occurrence]
forall t. Apply t => t -> [Arg Term] -> t
apply [Occurrence]
occ [Arg Term]
args) (Int -> [Maybe Name] -> [Maybe Name]
forall a. Int -> [a] -> [a]
drop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [Maybe Name]
gpars)
[LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Bool
hasm (Defn -> [Arg Term] -> Defn
forall t. Apply t => t -> [Arg Term] -> t
apply Defn
d [Arg Term]
args)
applyE :: Definition -> Elims -> Definition
applyE Definition
t Elims
es = Definition -> [Arg Term] -> Definition
forall t. Apply t => t -> [Arg Term] -> t
apply Definition
t ([Arg Term] -> Definition) -> [Arg Term] -> Definition
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply GlobalRewriteRule where
apply :: GlobalRewriteRule -> [Arg Term] -> GlobalRewriteRule
apply GlobalRewriteRule
r [Arg Term]
args =
let newContext :: Tele (Dom Type)
newContext = Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
forall t. Apply t => t -> [Arg Term] -> t
apply (GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
r) [Arg Term]
args
sub :: Substitution' NLPat
sub = Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
newContext) (Substitution' NLPat -> Substitution' NLPat)
-> Substitution' NLPat -> Substitution' NLPat
forall a b. (a -> b) -> a -> b
$ [NLPat] -> Substitution' NLPat
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([NLPat] -> Substitution' NLPat) -> [NLPat] -> Substitution' NLPat
forall a b. (a -> b) -> a -> b
$ [NLPat] -> [NLPat]
forall a. [a] -> [a]
reverse ([NLPat] -> [NLPat]) -> [NLPat] -> [NLPat]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> NLPat) -> [Arg Term] -> [NLPat]
forall a b. (a -> b) -> [a] -> [b]
map' (Term -> NLPat
PTerm (Term -> NLPat) -> (Arg Term -> Term) -> Arg Term -> NLPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
args
in GlobalRewriteRule
{ grName :: QName
grName = GlobalRewriteRule -> QName
grName GlobalRewriteRule
r
, grContext :: Tele (Dom Type)
grContext = Tele (Dom Type)
newContext
, grHead :: QName
grHead = GlobalRewriteRule -> QName
grHead GlobalRewriteRule
r
, grPats :: [Elim' NLPat]
grPats = Substitution' (SubstArg [Elim' NLPat])
-> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' NLPat
Substitution' (SubstArg [Elim' NLPat])
sub (GlobalRewriteRule -> [Elim' NLPat]
grPats GlobalRewriteRule
r)
, grRHS :: Term
grRHS = Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (GlobalRewriteRule -> Term
grRHS GlobalRewriteRule
r)
, grType :: Type
grType = Substitution' NLPat -> Type -> Type
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (GlobalRewriteRule -> Type
grType GlobalRewriteRule
r)
, grFromClause :: Bool
grFromClause = GlobalRewriteRule -> Bool
grFromClause GlobalRewriteRule
r
, grTopModule :: TopLevelModuleName
grTopModule = GlobalRewriteRule -> TopLevelModuleName
grTopModule GlobalRewriteRule
r
}
applyE :: GlobalRewriteRule -> Elims -> GlobalRewriteRule
applyE GlobalRewriteRule
t Elims
es = GlobalRewriteRule -> [Arg Term] -> GlobalRewriteRule
forall t. Apply t => t -> [Arg Term] -> t
apply GlobalRewriteRule
t ([Arg Term] -> GlobalRewriteRule)
-> [Arg Term] -> GlobalRewriteRule
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
apply :: [Occurrence] -> [Arg Term] -> [Occurrence]
apply [Occurrence]
occ [Arg Term]
args = Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
List.drop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [Occurrence]
occ
applyE :: [Occurrence] -> Elims -> [Occurrence]
applyE [Occurrence]
t Elims
es = [Occurrence] -> [Arg Term] -> [Occurrence]
forall t. Apply t => t -> [Arg Term] -> t
apply [Occurrence]
t ([Arg Term] -> [Occurrence]) -> [Arg Term] -> [Occurrence]
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [Polarity] where
apply :: [Polarity] -> [Arg Term] -> [Polarity]
apply [Polarity]
pol [Arg Term]
args = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
List.drop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [Polarity]
pol
applyE :: [Polarity] -> Elims -> [Polarity]
applyE [Polarity]
t Elims
es = [Polarity] -> [Arg Term] -> [Polarity]
forall t. Apply t => t -> [Arg Term] -> t
apply [Polarity]
t ([Arg Term] -> [Polarity]) -> [Arg Term] -> [Polarity]
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply NumGeneralizableArgs where
apply :: NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
apply NumGeneralizableArgs
NoGeneralizableArgs [Arg Term]
args = NumGeneralizableArgs
NoGeneralizableArgs
apply (SomeGeneralizableArgs Int
n) [Arg Term]
args = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args)
applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs
applyE NumGeneralizableArgs
t Elims
es = NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
forall t. Apply t => t -> [Arg Term] -> t
apply NumGeneralizableArgs
t ([Arg Term] -> NumGeneralizableArgs)
-> [Arg Term] -> NumGeneralizableArgs
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
apply :: [NamedArg (Pattern' a)] -> [Arg Term] -> [NamedArg (Pattern' a)]
apply [NamedArg (Pattern' a)]
ps [Arg Term]
args = Int -> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall {t} {x}.
(Eq t, Num t) =>
t -> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
loop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [NamedArg (Pattern' a)]
ps
where
loop :: t -> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
loop t
0 [Arg (Named_ (Pattern' x))]
ps = [Arg (Named_ (Pattern' x))]
ps
loop t
n [] = [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
loop t
n (Arg (Named_ (Pattern' x))
p : [Arg (Named_ (Pattern' x))]
ps) =
let recurse :: [Arg (Named_ (Pattern' x))]
recurse = t -> [Arg (Named_ (Pattern' x))] -> [Arg (Named_ (Pattern' x))]
loop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [Arg (Named_ (Pattern' x))]
ps
in case Arg (Named_ (Pattern' x)) -> Pattern' x
forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' x))
p of
VarP{} -> [Arg (Named_ (Pattern' x))]
recurse
DotP{} -> [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
LitP{} -> [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
ConP{} -> [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
DefP{} -> [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> [Arg (Named_ (Pattern' x))]
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP{} -> [Arg (Named_ (Pattern' x))]
recurse
applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]
applyE [NamedArg (Pattern' a)]
t Elims
es = [NamedArg (Pattern' a)] -> [Arg Term] -> [NamedArg (Pattern' a)]
forall t. Apply t => t -> [Arg Term] -> t
apply [NamedArg (Pattern' a)]
t ([Arg Term] -> [NamedArg (Pattern' a)])
-> [Arg Term] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply Projection where
apply :: Projection -> [Arg Term] -> Projection
apply Projection
p [Arg Term]
args = Projection
p
{ projIndex = projIndex p - size args
, projLams = projLams p `apply` args
}
applyE :: Projection -> Elims -> Projection
applyE Projection
t Elims
es = Projection -> [Arg Term] -> Projection
forall t. Apply t => t -> [Arg Term] -> t
apply Projection
t ([Arg Term] -> Projection) -> [Arg Term] -> Projection
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply ProjLams where
apply :: ProjLams -> [Arg Term] -> ProjLams
apply (ProjLams [Arg [Char]]
lams) [Arg Term]
args = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
List.drop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [Arg [Char]]
lams
applyE :: ProjLams -> Elims -> ProjLams
applyE ProjLams
t Elims
es = ProjLams -> [Arg Term] -> ProjLams
forall t. Apply t => t -> [Arg Term] -> t
apply ProjLams
t ([Arg Term] -> ProjLams) -> [Arg Term] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply Defn where
apply :: Defn -> [Arg Term] -> Defn
apply Defn
d [] = Defn
d
apply Defn
d [Arg Term]
args = case Defn
d of
Axiom{} -> Defn
d
DataOrRecSig Int
n DataOrRecord_
eta -> Int -> DataOrRecord_ -> Defn
DataOrRecSig (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) DataOrRecord_
eta
GeneralizableVar NumGeneralizableArgs
gv -> NumGeneralizableArgs -> Defn
GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
forall a b. (a -> b) -> a -> b
$ NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
forall t. Apply t => t -> [Arg Term] -> t
apply NumGeneralizableArgs
gv [Arg Term]
args
AbstractDefn Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Defn -> [Arg Term] -> Defn
forall t. Apply t => t -> [Arg Term] -> t
apply Defn
d [Arg Term]
args
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse' Clause
funInv = FunctionInverse' Clause
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
_ } ->
Defn
d { funClauses = apply cs args
, funCompiled = apply cc args
, funCovering = apply cov args
, funInv = apply inv args
, funExtLam = modifySystem (`apply` args) <$> extLam
}
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse' Clause
funInv = FunctionInverse' Clause
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right p0 :: Projection
p0@Projection{ projIndex :: Projection -> Int
projIndex = Int
n0 } } ->
case Projection
p0 Projection -> [Arg Term] -> Projection
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args of
p :: Projection
p@Projection{ projIndex :: Projection -> Int
projIndex = Int
n }
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Defn
d { funProjection = Right p }
| Bool
otherwise ->
Defn
d { funClauses = apply cs args'
, funCompiled = apply cc args'
, funCovering = apply cov args'
, funInv = apply inv args'
, funProjection = if n == 0 && isVar0 then Right p else Left MaybeProjection
, funExtLam = modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) <$> extLam
}
where
args' :: [Arg Term]
args' = Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop Int
n0 [Arg Term]
args
isVar0 :: Bool
isVar0 = case (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop (Int
n0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Arg Term]
args of [Var Int
0 []] -> Bool
True; [Term]
_ -> Bool
False
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
Defn
d { dataPars = np - size args
, dataClause = apply cl args
}
Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel
} ->
Defn
d { recPars = np - size args
, recClause = apply cl args, recTel = apply tel args
}
Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
Defn
d { conPars = np - size args }
Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
Defn
d { primClauses = apply cs args }
PrimitiveSort{} -> Defn
d
applyE :: Defn -> Elims -> Defn
applyE Defn
t Elims
es = Defn -> [Arg Term] -> Defn
forall t. Apply t => t -> [Arg Term] -> t
apply Defn
t ([Arg Term] -> Defn) -> [Arg Term] -> Defn
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply PrimFun where
apply :: PrimFun -> [Arg Term] -> PrimFun
apply (PrimFun QName
x Int
ar [Occurrence]
occs [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) [Arg Term]
args =
QName
-> Int
-> [Occurrence]
-> ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) (Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
drop Int
n [Occurrence]
occs) (([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun)
-> ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
vs -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$! [Arg Term]
args [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++! [Arg Term]
vs
where
n :: Int
n = [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
args
applyE :: PrimFun -> Elims -> PrimFun
applyE PrimFun
t Elims
es = PrimFun -> [Arg Term] -> PrimFun
forall t. Apply t => t -> [Arg Term] -> t
apply PrimFun
t ([Arg Term] -> PrimFun) -> [Arg Term] -> PrimFun
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply Clause where
apply :: Clause -> [Arg Term] -> Clause
apply cls :: Clause
cls@(Clause Range
rl Range
rf Tele (Dom Type)
tel [NamedArg DeBruijnPattern]
ps Maybe Term
b Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) [Arg Term]
args
| [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg DeBruijnPattern]
ps = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise =
Range
-> Range
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf
Tele (Dom Type)
tel'
(Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg [NamedArg DeBruijnPattern])
rhoP ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [NamedArg DeBruijnPattern]
ps)
(Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Maybe Term))
rho Maybe Term
b)
(Substitution' (SubstArg (Maybe (Arg Type)))
-> Maybe (Arg Type) -> Maybe (Arg Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Maybe (Arg Type)))
rho Maybe (Arg Type)
t)
Catchall
catchall
ClauseRecursive
recursive
Maybe Bool
unreachable
ExpandedEllipsis
ell
Maybe ModuleName
wm
where
rargs :: [Term]
rargs = (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> [Arg Term]
forall a. [a] -> [a]
reverse [Arg Term]
args
rps :: [NamedArg DeBruijnPattern]
rps = [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a]
reverse ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
take' ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) [NamedArg DeBruijnPattern]
ps
n :: Int
n = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
tel' :: Tele (Dom Type)
tel' = Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel Int
n Tele (Dom Type)
tel [NamedArg DeBruijnPattern]
rps [Term]
rargs
rhoP :: PatternSubstitution
rhoP :: PatternSubstitution
rhoP = (Term -> DeBruijnPattern)
-> Int
-> [NamedArg DeBruijnPattern]
-> [Term]
-> PatternSubstitution
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Int
n [NamedArg DeBruijnPattern]
rps [Term]
rargs
rho :: Substitution' Term
rho = (Term -> Term)
-> Int
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Substitution' Term
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> Term
forall a. a -> a
id Int
n [NamedArg DeBruijnPattern]
rps [Term]
rargs
substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP :: Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v = Int
-> SubstArg [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
i (Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
v)
mkSub :: EndoSubst a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub :: forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
_ Int
_ [] [] = Substitution' a
forall a. Substitution' a
idS
mkSub Term -> a
tm Int
n (NamedArg DeBruijnPattern
p : [NamedArg DeBruijnPattern]
ps) (Term
v : [Term]
vs) =
case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
VarP PatternInfo
_ (DBPatVar [Char]
_ Int
i) -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v' [NamedArg DeBruijnPattern]
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> a -> Substitution' a
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
i (Term -> a
tm Term
v')
where v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v
DotP{} -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n [NamedArg DeBruijnPattern]
ps [Term]
vs
ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps' -> ((Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n ([NamedArg DeBruijnPattern] -> [Term] -> Substitution' a)
-> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a b. (a -> b) -> a -> b
$! ([NamedArg DeBruijnPattern]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps)) ([Term] -> Substitution' a) -> [Term] -> Substitution' a
forall a b. (a -> b) -> a -> b
$! (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
vs)
DefP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
LitP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar [Char]
_ Int
i) -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v' [NamedArg DeBruijnPattern]
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> a -> Substitution' a
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
i (Term -> a
tm Term
v')
where v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v
mkSub Term -> a
_ Int
_ [NamedArg DeBruijnPattern]
_ [Term]
_ = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel :: Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel Int
n Tele (Dom Type)
tel [] [] = Tele (Dom Type)
tel
newTel Int
n Tele (Dom Type)
tel (NamedArg DeBruijnPattern
p : [NamedArg DeBruijnPattern]
ps) (Term
v : [Term]
vs) =
case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
VarP PatternInfo
_ (DBPatVar [Char]
_ Int
i) -> Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> SubstArg (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall {t} {a}.
(Eq t, Num t, Subst a, Subst (SubstArg a)) =>
t -> SubstArg a -> Tele a -> Tele a
subTel (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
SubstArg (Dom Type)
v Tele (Dom Type)
tel) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) [NamedArg DeBruijnPattern]
ps) [Term]
vs
DotP{} -> Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel Int
n Tele (Dom Type)
tel [NamedArg DeBruijnPattern]
ps [Term]
vs
ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps' -> (Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel Int
n Tele (Dom Type)
tel ([NamedArg DeBruijnPattern] -> [Term] -> Tele (Dom Type))
-> [NamedArg DeBruijnPattern] -> [Term] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$! [NamedArg DeBruijnPattern]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps) ([Term] -> Tele (Dom Type)) -> [Term] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$! (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
vs)
DefP{} -> Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
LitP{} -> Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar [Char]
_ Int
i) -> Int
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Tele (Dom Type)
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> SubstArg (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall {t} {a}.
(Eq t, Num t, Subst a, Subst (SubstArg a)) =>
t -> SubstArg a -> Tele a -> Tele a
subTel (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
SubstArg (Dom Type)
v Tele (Dom Type)
tel) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) [NamedArg DeBruijnPattern]
ps) [Term]
vs
newTel Int
_ Tele (Dom Type)
tel [NamedArg DeBruijnPattern]
_ [Term]
_ = Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
projections :: ConHead -> Term -> [Term]
projections :: ConHead -> Term -> [Term]
projections ConHead
c Term
v = [ ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
case ConHead -> DataOrRecord
conDataRecord ConHead
c of
DataOrRecord
IsData -> QName -> Elims -> Elims -> Term
defApp QName
f [] [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v)]
IsRecord{} -> Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
| Arg ArgInfo
ai QName
f <- ConHead -> [Arg QName]
conFields ConHead
c ]
subTel :: t -> SubstArg a -> Tele a -> Tele a
subTel t
i SubstArg a
v Tele a
EmptyTel = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
subTel t
0 SubstArg a
v (ExtendTel a
_ Abs (Tele a)
tel) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Tele a)
tel SubstArg a
SubstArg (Tele a)
v
subTel t
i SubstArg a
v (ExtendTel a
a Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> Abs (Tele a) -> Tele a
forall a b. (a -> b) -> a -> b
$ t -> SubstArg a -> Tele a -> Tele a
subTel (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Int -> SubstArg a -> SubstArg a
forall a. Subst a => Int -> a -> a
raise Int
1 SubstArg a
v) (Tele a -> Tele a) -> Abs (Tele a) -> Abs (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele a)
tel
applyE :: Clause -> Elims -> Clause
applyE Clause
t Elims
es = Clause -> [Arg Term] -> Clause
forall t. Apply t => t -> [Arg Term] -> t
apply Clause
t ([Arg Term] -> Clause) -> [Arg Term] -> Clause
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply CompiledClauses where
apply :: CompiledClauses -> [Arg Term] -> CompiledClauses
apply CompiledClauses
cc [Arg Term]
args = case CompiledClauses
cc of
Fail [Arg [Char]]
hs -> [Arg [Char]] -> CompiledClauses
forall a. [Arg [Char]] -> CompiledClauses' a
Fail (Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
drop Int
len [Arg [Char]]
hs)
Done Int
no ClauseRecursive
mr [Arg [Char]]
hs Term
t
| [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
hs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len ->
let sub :: Substitution' Term
sub = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$! ((Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var [Int
0..[Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
hs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
args)
in Int -> ClauseRecursive -> [Arg [Char]] -> Term -> CompiledClauses
forall a.
Int -> ClauseRecursive -> [Arg [Char]] -> a -> CompiledClauses' a
Done Int
no ClauseRecursive
mr (Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
List.drop Int
len [Arg [Char]]
hs) (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sub Term
t
| Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
Case Arg Int
n Case CompiledClauses
bs
| Arg Int -> Int
forall e. Arg e -> e
unArg Arg Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Arg Int
n Arg Int -> (Int -> Int) -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int
m -> Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len) (Case CompiledClauses -> [Arg Term] -> Case CompiledClauses
forall t. Apply t => t -> [Arg Term] -> t
apply Case CompiledClauses
bs [Arg Term]
args)
| Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
where
len :: Int
len = [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args
applyE :: CompiledClauses -> Elims -> CompiledClauses
applyE CompiledClauses
t Elims
es = CompiledClauses -> [Arg Term] -> CompiledClauses
forall t. Apply t => t -> [Arg Term] -> t
apply CompiledClauses
t ([Arg Term] -> CompiledClauses) -> [Arg Term] -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply ExtLamInfo where
apply :: ExtLamInfo -> [Arg Term] -> ExtLamInfo
apply (ExtLamInfo ModuleName
m Bool
b Maybe System
sys) [Arg Term]
args = ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
m Bool
b (Maybe System -> [Arg Term] -> Maybe System
forall t. Apply t => t -> [Arg Term] -> t
apply Maybe System
sys [Arg Term]
args)
applyE :: ExtLamInfo -> Elims -> ExtLamInfo
applyE ExtLamInfo
t Elims
es = ExtLamInfo -> [Arg Term] -> ExtLamInfo
forall t. Apply t => t -> [Arg Term] -> t
apply ExtLamInfo
t ([Arg Term] -> ExtLamInfo) -> [Arg Term] -> ExtLamInfo
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply System where
apply :: System -> [Arg Term] -> System
apply (System Tele (Dom Type)
tel [(Face, Term)]
sys) [Arg Term]
args
= if Int
nargs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
ntel then System
forall a. HasCallStack => a
__IMPOSSIBLE__
else Tele (Dom Type) -> [(Face, Term)] -> System
System Tele (Dom Type)
newTel (((Face, Term) -> (Face, Term)) -> [(Face, Term)] -> [(Face, Term)]
forall a b. (a -> b) -> [a] -> [b]
map'' (((Term, Bool) -> (Term, Bool)) -> Face -> Face
forall a b. (a -> b) -> [a] -> [b]
map'' (Term -> Term
f (Term -> Term) -> (Bool -> Bool) -> (Term, Bool) -> (Term, Bool)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Bool -> Bool
forall a. a -> a
id) (Face -> Face) -> (Term -> Term) -> (Face, Term) -> (Face, Term)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Term -> Term
f) [(Face, Term)]
sys)
where
f :: Term -> Term
f = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sigma
nargs :: Int
nargs = [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args
ntel :: Int
ntel = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
newTel :: Tele (Dom Type)
newTel = Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
forall t. Apply t => t -> [Arg Term] -> t
apply Tele (Dom Type)
tel [Arg Term]
args
sigma :: Substitution' Term
sigma = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
ntel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nargs) ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
args))
applyE :: System -> Elims -> System
applyE System
t Elims
es = System -> [Arg Term] -> System
forall t. Apply t => t -> [Arg Term] -> t
apply System
t ([Arg Term] -> System) -> [Arg Term] -> System
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply a => Apply (WithArity a) where
apply :: WithArity a -> [Arg Term] -> WithArity a
apply (WithArity Int
n a
a) [Arg Term]
args = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ a -> [Arg Term] -> a
forall t. Apply t => t -> [Arg Term] -> t
apply a
a [Arg Term]
args
applyE :: WithArity a -> Elims -> WithArity a
applyE (WithArity Int
n a
a) Elims
es = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
a Elims
es
instance Apply a => Apply (Case a) where
apply :: Case a -> [Arg Term] -> Case a
apply (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) [Arg Term]
args =
Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Map QName (WithArity a) -> [Arg Term] -> Map QName (WithArity a)
forall t. Apply t => t -> [Arg Term] -> t
apply Map QName (WithArity a)
cs [Arg Term]
args) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (WithArity a -> [Arg Term] -> WithArity a
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta) (Map Literal a -> [Arg Term] -> Map Literal a
forall t. Apply t => t -> [Arg Term] -> t
apply Map Literal a
ls [Arg Term]
args) (Maybe a -> [Arg Term] -> Maybe a
forall t. Apply t => t -> [Arg Term] -> t
apply Maybe a
m [Arg Term]
args) Maybe Bool
b Bool
lz
applyE :: Case a -> Elims -> Case a
applyE (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) Elims
es =
Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Map QName (WithArity a) -> Elims -> Map QName (WithArity a)
forall t. Apply t => t -> Elims -> t
applyE Map QName (WithArity a)
cs Elims
es) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (WithArity a -> Elims -> WithArity a
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta)(Map Literal a -> Elims -> Map Literal a
forall t. Apply t => t -> Elims -> t
applyE Map Literal a
ls Elims
es) (Maybe a -> Elims -> Maybe a
forall t. Apply t => t -> Elims -> t
applyE Maybe a
m Elims
es) Maybe Bool
b Bool
lz
instance Apply FunctionInverse where
apply :: FunctionInverse' Clause -> [Arg Term] -> FunctionInverse' Clause
apply FunctionInverse' Clause
NotInjective [Arg Term]
args = FunctionInverse' Clause
forall c. FunctionInverse' c
NotInjective
apply (Inverse InversionMap Clause
inv) [Arg Term]
args = InversionMap Clause -> FunctionInverse' Clause
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse' Clause)
-> InversionMap Clause -> FunctionInverse' Clause
forall a b. (a -> b) -> a -> b
$ InversionMap Clause -> [Arg Term] -> InversionMap Clause
forall t. Apply t => t -> [Arg Term] -> t
apply InversionMap Clause
inv [Arg Term]
args
applyE :: FunctionInverse' Clause -> Elims -> FunctionInverse' Clause
applyE FunctionInverse' Clause
t Elims
es = FunctionInverse' Clause -> [Arg Term] -> FunctionInverse' Clause
forall t. Apply t => t -> [Arg Term] -> t
apply FunctionInverse' Clause
t ([Arg Term] -> FunctionInverse' Clause)
-> [Arg Term] -> FunctionInverse' Clause
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Apply DisplayTerm where
apply :: DisplayTerm -> [Arg Term] -> DisplayTerm
apply (DTerm' Term
v Elims
es) [Arg Term]
args = Term -> Elims -> DisplayTerm
DTerm' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
apply (DDot' Term
v Elims
es) [Arg Term]
args = Term -> Elims -> DisplayTerm
DDot' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
apply (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs) [Arg Term]
args = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Arg DisplayTerm]
vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Arg DisplayTerm) -> [Arg Term] -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) [Arg Term]
args)
apply (DDef QName
c [Elim' DisplayTerm]
es) [Arg Term]
args = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Elim' DisplayTerm]
es [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' DisplayTerm)
-> [Arg Term] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) [Arg Term]
args)
apply (DWithApp DisplayTerm
v List1 DisplayTerm
ws Elims
es) [Arg Term]
args = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp DisplayTerm
v List1 DisplayTerm
ws (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
applyE :: DisplayTerm -> Elims -> DisplayTerm
applyE (DTerm' Term
v Elims
es') Elims
es = Term -> Elims -> DisplayTerm
DTerm' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
applyE (DDot' Term
v Elims
es') Elims
es = Term -> Elims -> DisplayTerm
DDot' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
applyE (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs) Elims
es = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Arg DisplayTerm]
vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. [a] -> [a] -> [a]
++! (Arg Term -> Arg DisplayTerm) -> [Arg Term] -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) [Arg Term]
ws
where ws :: [Arg Term]
ws = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
applyE (DDef QName
c [Elim' DisplayTerm]
es') Elims
es = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Elim' DisplayTerm]
es' [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++! (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es
applyE (DWithApp DisplayTerm
v List1 DisplayTerm
ws Elims
es') Elims
es = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp DisplayTerm
v List1 DisplayTerm
ws (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where
apply :: [t] -> [Arg Term] -> [t]
apply [t]
ts [Arg Term]
args = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (t -> [Arg Term] -> t
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) [t]
ts
applyE :: [t] -> Elims -> [t]
applyE [t]
ts Elims
es = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) [t]
ts
instance Apply t => Apply (Blocked t) where
apply :: Blocked t -> [Arg Term] -> Blocked t
apply Blocked t
b [Arg Term]
args = (t -> t) -> Blocked t -> Blocked t
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> [Arg Term] -> t
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) Blocked t
b
applyE :: Blocked t -> Elims -> Blocked t
applyE Blocked t
b Elims
es = (t -> t) -> Blocked t -> Blocked t
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Blocked t
b
instance Apply t => Apply (Maybe t) where
apply :: Maybe t -> [Arg Term] -> Maybe t
apply Maybe t
x [Arg Term]
args = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> [Arg Term] -> t
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) Maybe t
x
applyE :: Maybe t -> Elims -> Maybe t
applyE Maybe t
x Elims
es = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Maybe t
x
instance Apply t => Apply (Strict.Maybe t) where
apply :: Maybe t -> [Arg Term] -> Maybe t
apply Maybe t
x [Arg Term]
args = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> [Arg Term] -> t
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) Maybe t
x
applyE :: Maybe t -> Elims -> Maybe t
applyE Maybe t
x Elims
es = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Maybe t
x
instance Apply v => Apply (Map k v) where
apply :: Map k v -> [Arg Term] -> Map k v
apply Map k v
x [Arg Term]
args = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> [Arg Term] -> v
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) Map k v
x
applyE :: Map k v -> Elims -> Map k v
applyE Map k v
x Elims
es = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Elims -> v
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Map k v
x
instance Apply v => Apply (HashMap k v) where
apply :: HashMap k v -> [Arg Term] -> HashMap k v
apply HashMap k v
x [Arg Term]
args = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> [Arg Term] -> v
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args) HashMap k v
x
applyE :: HashMap k v -> Elims -> HashMap k v
applyE HashMap k v
x Elims
es = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Elims -> v
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) HashMap k v
x
instance (Apply a, Apply b) => Apply (a,b) where
apply :: (a, b) -> [Arg Term] -> (a, b)
apply (a
x,b
y) [Arg Term]
args = (a -> [Arg Term] -> a
forall t. Apply t => t -> [Arg Term] -> t
apply a
x [Arg Term]
args, b -> [Arg Term] -> b
forall t. Apply t => t -> [Arg Term] -> t
apply b
y [Arg Term]
args)
applyE :: (a, b) -> Elims -> (a, b)
applyE (a
x,b
y) Elims
es = (a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
x Elims
es , b -> Elims -> b
forall t. Apply t => t -> Elims -> t
applyE b
y Elims
es )
instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
apply :: (a, b, c) -> [Arg Term] -> (a, b, c)
apply (a
x,b
y,c
z) [Arg Term]
args = (a -> [Arg Term] -> a
forall t. Apply t => t -> [Arg Term] -> t
apply a
x [Arg Term]
args, b -> [Arg Term] -> b
forall t. Apply t => t -> [Arg Term] -> t
apply b
y [Arg Term]
args, c -> [Arg Term] -> c
forall t. Apply t => t -> [Arg Term] -> t
apply c
z [Arg Term]
args)
applyE :: (a, b, c) -> Elims -> (a, b, c)
applyE (a
x,b
y,c
z) Elims
es = (a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
x Elims
es , b -> Elims -> b
forall t. Apply t => t -> Elims -> t
applyE b
y Elims
es , c -> Elims -> c
forall t. Apply t => t -> Elims -> t
applyE c
z Elims
es )
instance DoDrop a => Apply (Drop a) where
apply :: Drop a -> [Arg Term] -> Drop a
apply Drop a
x [Arg Term]
args = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
dropMore ([Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
args) Drop a
x
applyE :: Drop a -> Elims -> Drop a
applyE Drop a
t Elims
es = Drop a -> [Arg Term] -> Drop a
forall t. Apply t => t -> [Arg Term] -> t
apply Drop a
t ([Arg Term] -> Drop a) -> [Arg Term] -> Drop a
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance DoDrop a => Abstract (Drop a) where
abstract :: Tele (Dom Type) -> Drop a -> Drop a
abstract Tele (Dom Type)
tel Drop a
x = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
unDrop (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Drop a
x
instance Apply Permutation where
apply :: Permutation -> [Arg Term] -> Permutation
apply (Perm Int
n [Int]
xs) [Arg Term]
args = Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$! (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' ((Int -> Int -> Int) -> Int -> Int -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip (-) Int
m) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop Int
m [Int]
xs
where
m :: Int
m = [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
args
applyE :: Permutation -> Elims -> Permutation
applyE Permutation
t Elims
es = Permutation -> [Arg Term] -> Permutation
forall t. Apply t => t -> [Arg Term] -> t
apply Permutation
t ([Arg Term] -> Permutation) -> [Arg Term] -> Permutation
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
instance Abstract Permutation where
abstract :: Tele (Dom Type) -> Permutation -> Permutation
abstract Tele (Dom Type)
tel (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$! [Int
0..Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! ((Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) [Int]
xs)
where
m :: Int
m = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
piApply :: Type -> Args -> Type
piApply :: Type -> [Arg Term] -> Type
piApply Type
t [] = Type
t
piApply (El Sort' Term
_ (Pi Dom Type
_ Abs Type
b)) (Arg Term
a:[Arg Term]
args) = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Type -> [Arg Term] -> Type
`piApply` [Arg Term]
args
piApply Type
t [Arg Term]
args =
[Char] -> Type -> Type
forall a. [Char] -> a -> a
trace ([Char]
"piApply t = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
"\n args = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Arg Term] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Arg Term]
args) Type
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Abstract Term where
abstract :: Tele (Dom Type) -> Term -> Term
abstract = Tele (Dom Type) -> Term -> Term
teleLam
instance Abstract Type where
abstract :: Tele (Dom Type) -> Type -> Type
abstract = Tele (Dom Type) -> Type -> Type
telePi_
instance Abstract Sort where
abstract :: Tele (Dom Type) -> Sort' Term -> Sort' Term
abstract Tele (Dom Type)
EmptyTel Sort' Term
s = Sort' Term
s
abstract Tele (Dom Type)
_ Sort' Term
s = Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Abstract Telescope where
Tele (Dom Type)
EmptyTel abstract :: Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
`abstract` Tele (Dom Type)
tel = Tele (Dom Type)
tel
ExtendTel Dom Type
arg Abs (Tele (Dom Type))
xtel `abstract` Tele (Dom Type)
tel = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
arg (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Abs (Tele (Dom Type))
xtel Abs (Tele (Dom Type))
-> (Tele (Dom Type) -> Tele (Dom Type)) -> Abs (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
tel)
instance Abstract Definition where
abstract :: Tele (Dom Type) -> Definition -> Definition
abstract Tele (Dom Type)
tel (Defn ArgInfo
info QName
x Type
t [Polarity]
pol [Occurrence]
occ [Maybe Name]
gpars [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Bool
hasm Defn
d) =
ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe InstanceInfo
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Bool
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Type
t) (Tele (Dom Type) -> [Polarity] -> [Polarity]
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel [Polarity]
pol) (Tele (Dom Type) -> [Occurrence] -> [Occurrence]
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel [Occurrence]
occ)
(Int -> Maybe Name -> [Maybe Name]
forall a. Int -> a -> [a]
replicate' (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Maybe Name
forall a. Maybe a
Nothing [Maybe Name] -> [Maybe Name] -> [Maybe Name]
forall a. [a] -> [a] -> [a]
++! [Maybe Name]
gpars)
[LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Bool
hasm (Tele (Dom Type) -> Defn -> Defn
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Defn
d)
instance Abstract GlobalRewriteRule where
abstract :: Tele (Dom Type) -> GlobalRewriteRule -> GlobalRewriteRule
abstract Tele (Dom Type)
tel (GlobalRewriteRule QName
q Tele (Dom Type)
gamma QName
f [Elim' NLPat]
ps Term
rhs Type
t Bool
c TopLevelModuleName
top) =
QName
-> Tele (Dom Type)
-> QName
-> [Elim' NLPat]
-> Term
-> Type
-> Bool
-> TopLevelModuleName
-> GlobalRewriteRule
GlobalRewriteRule QName
q (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Tele (Dom Type)
gamma) QName
f [Elim' NLPat]
ps Term
rhs Type
t Bool
c TopLevelModuleName
top
instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
abstract :: Tele (Dom Type) -> [Occurrence] -> [Occurrence]
abstract Tele (Dom Type)
tel [] = []
abstract Tele (Dom Type)
tel [Occurrence]
occ = Int -> Occurrence -> [Occurrence]
forall a. Int -> a -> [a]
replicate' (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Occurrence
Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++! [Occurrence]
occ
instance {-# OVERLAPPING #-} Abstract [Polarity] where
abstract :: Tele (Dom Type) -> [Polarity] -> [Polarity]
abstract Tele (Dom Type)
tel [] = []
abstract Tele (Dom Type)
tel [Polarity]
pol = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate' (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Polarity
Invariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++! [Polarity]
pol
instance Abstract NumGeneralizableArgs where
abstract :: Tele (Dom Type) -> NumGeneralizableArgs -> NumGeneralizableArgs
abstract Tele (Dom Type)
tel NumGeneralizableArgs
NoGeneralizableArgs = NumGeneralizableArgs
NoGeneralizableArgs
abstract Tele (Dom Type)
tel (SomeGeneralizableArgs Int
n) = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
instance Abstract Projection where
abstract :: Tele (Dom Type) -> Projection -> Projection
abstract Tele (Dom Type)
tel Projection
p = Projection
p
{ projIndex = size tel + projIndex p
, projLams = abstract tel $ projLams p
}
instance Abstract ProjLams where
abstract :: Tele (Dom Type) -> ProjLams -> ProjLams
abstract Tele (Dom Type)
tel (ProjLams [Arg [Char]]
lams) = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$!
((Dom' Term ([Char], Type) -> Arg [Char])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (\ !Dom' Term ([Char], Type)
dom -> Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char])
-> Dom' Term ([Char], Type) -> Dom' Term [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term ([Char], Type)
dom)) (Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel)) [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++! [Arg [Char]]
lams
instance Abstract System where
abstract :: Tele (Dom Type) -> System -> System
abstract Tele (Dom Type)
tel (System Tele (Dom Type)
tel1 [(Face, Term)]
sys) = Tele (Dom Type) -> [(Face, Term)] -> System
System (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Tele (Dom Type)
tel1) [(Face, Term)]
sys
instance Abstract Defn where
abstract :: Tele (Dom Type) -> Defn -> Defn
abstract Tele (Dom Type)
tel Defn
d = case Defn
d of
Axiom{} -> Defn
d
DataOrRecSig Int
n DataOrRecord_
eta -> Int -> DataOrRecord_ -> Defn
DataOrRecSig (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) DataOrRecord_
eta
GeneralizableVar NumGeneralizableArgs
gv -> NumGeneralizableArgs -> Defn
GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> NumGeneralizableArgs -> NumGeneralizableArgs
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel NumGeneralizableArgs
gv
AbstractDefn Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Defn -> Defn
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Defn
d
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse' Clause
funInv = FunctionInverse' Clause
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
_ } ->
Defn
d { funClauses = abstract tel cs
, funCompiled = abstract tel cc
, funCovering = abstract tel cov
, funInv = abstract tel inv
, funExtLam = modifySystem (abstract tel) <$> extLam
}
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse' Clause
funInv = FunctionInverse' Clause
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p } ->
if Projection -> Int
projIndex Projection
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then
Defn
d { funProjection = Right $ abstract tel p
, funClauses = map' (abstractClause EmptyTel) cs
}
else
Defn
d { funProjection = Right $ abstract tel p
, funClauses = map' (abstractClause tel1) cs
, funCompiled = abstract tel1 cc
, funCovering = abstract tel1 cov
, funInv = abstract tel1 inv
, funExtLam = modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) <$> extLam
}
where
tel1 :: Tele (Dom Type)
tel1 = [Dom' Term ([Char], Type)] -> Tele (Dom Type)
telFromList ([Dom' Term ([Char], Type)] -> Tele (Dom Type))
-> [Dom' Term ([Char], Type)] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. Int -> [a] -> [a]
drop (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
abstractClause :: Tele (Dom Type) -> Clause -> Clause
abstractClause Tele (Dom Type)
tel1 Clause
c = (Tele (Dom Type) -> Clause -> Clause
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel1 Clause
c) { clauseTel = abstract tel $ clauseTel c }
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
Defn
d { dataPars = np + size tel
, dataClause = abstract tel cl
}
Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Tele (Dom Type)
recTel = Tele (Dom Type)
tel' } ->
Defn
d { recPars = np + size tel
, recClause = abstract tel cl
, recTel = abstract tel tel'
}
Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
Defn
d { conPars = np + size tel }
Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
Defn
d { primClauses = abstract tel cs }
PrimitiveSort{} -> Defn
d
instance Abstract PrimFun where
abstract :: Tele (Dom Type) -> PrimFun -> PrimFun
abstract Tele (Dom Type)
tel (PrimFun QName
x Int
ar [Occurrence]
occs [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) =
QName
-> Int
-> [Occurrence]
-> ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (Int -> Occurrence -> [Occurrence]
forall a. Int -> a -> [a]
replicate' Int
n Occurrence
Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++! [Occurrence]
occs) (([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun)
-> ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \[Arg Term]
ts ->
[Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop Int
n [Arg Term]
ts
where n :: Int
n = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
instance Abstract Clause where
abstract :: Tele (Dom Type) -> Clause -> Clause
abstract Tele (Dom Type)
tel (Clause Range
rl Range
rf Tele (Dom Type)
tel' [NamedArg DeBruijnPattern]
ps Maybe Term
b Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
Range
-> Range
-> Tele (Dom Type)
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Tele (Dom Type)
tel')
(Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
namedTelVars Int
m Tele (Dom Type)
tel [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps)
Maybe Term
b
Maybe (Arg Type)
t
Catchall
catchall
ClauseRecursive
recursive
Maybe Bool
unreachable
ExpandedEllipsis
ell
Maybe ModuleName
wm
where m :: Int
m = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel'
instance Abstract CompiledClauses where
abstract :: Tele (Dom Type) -> CompiledClauses -> CompiledClauses
abstract Tele (Dom Type)
tel CompiledClauses
cc = case CompiledClauses
cc of
Fail [Arg [Char]]
xs -> [Arg [Char]] -> CompiledClauses
forall a. [Arg [Char]] -> CompiledClauses' a
Fail ([Arg [Char]]
hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++! [Arg [Char]]
xs)
Done Int
no ClauseRecursive
mr [Arg [Char]]
xs Term
t -> Int -> ClauseRecursive -> [Arg [Char]] -> Term -> CompiledClauses
forall a.
Int -> ClauseRecursive -> [Arg [Char]] -> a -> CompiledClauses' a
Done Int
no ClauseRecursive
mr ([Arg [Char]]
hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++! [Arg [Char]]
xs) Term
t
Case Arg Int
n Case CompiledClauses
bs -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Arg Int
n Arg Int -> (Int -> Int) -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) (Tele (Dom Type) -> Case CompiledClauses -> Case CompiledClauses
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Case CompiledClauses
bs)
where
hs :: [Arg [Char]]
hs = (Dom' Term ([Char], Type) -> Arg [Char])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term [Char] -> Arg [Char])
-> (Dom' Term ([Char], Type) -> Dom' Term [Char])
-> Dom' Term ([Char], Type)
-> Arg [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Type) -> [Char])
-> Dom' Term ([Char], Type) -> Dom' Term [Char]
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst) ([Dom' Term ([Char], Type)] -> [Arg [Char]])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
instance Abstract a => Abstract (WithArity a) where
abstract :: Tele (Dom Type) -> WithArity a -> WithArity a
abstract Tele (Dom Type)
tel (WithArity Int
n a
a) = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> a -> a
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel a
a
instance Abstract a => Abstract (Case a) where
abstract :: Tele (Dom Type) -> Case a -> Case a
abstract Tele (Dom Type)
tel (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) =
Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Tele (Dom Type)
-> Map QName (WithArity a) -> Map QName (WithArity a)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Map QName (WithArity a)
cs) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Tele (Dom Type) -> WithArity a -> WithArity a
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta)
(Tele (Dom Type) -> Map Literal a -> Map Literal a
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Map Literal a
ls) (Tele (Dom Type) -> Maybe a -> Maybe a
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Maybe a
m) Maybe Bool
b Bool
lz
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars :: Int -> Tele (Dom Type) -> [Arg DeBruijnPattern]
telVars Int
m = (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) ([NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
-> (Tele (Dom Type) -> [NamedArg DeBruijnPattern])
-> Tele (Dom Type)
-> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
namedTelVars Int
m)
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars :: Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
namedTelVars Int
m Tele (Dom Type)
EmptyTel = []
namedTelVars Int
m (ExtendTel !Dom Type
dom Abs (Tele (Dom Type))
tel) =
let !rest :: [NamedArg DeBruijnPattern]
rest = Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
namedTelVars (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Abs a -> a
unAbs Abs (Tele (Dom Type))
tel) in
let !this :: NamedArg DeBruijnPattern
this = ArgInfo
-> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern)
-> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! (Int -> [Char] -> Named NamedName DeBruijnPattern
namedDBVarP (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([Char] -> Named NamedName DeBruijnPattern)
-> [Char] -> Named NamedName DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Abs (Tele (Dom Type)) -> [Char]
forall a. Abs a -> [Char]
absName Abs (Tele (Dom Type))
tel) in
NamedArg DeBruijnPattern
this NamedArg DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. a -> [a] -> [a]
: [NamedArg DeBruijnPattern]
rest
instance Abstract FunctionInverse where
abstract :: Tele (Dom Type)
-> FunctionInverse' Clause -> FunctionInverse' Clause
abstract Tele (Dom Type)
tel FunctionInverse' Clause
NotInjective = FunctionInverse' Clause
forall c. FunctionInverse' c
NotInjective
abstract Tele (Dom Type)
tel (Inverse InversionMap Clause
inv) = InversionMap Clause -> FunctionInverse' Clause
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse' Clause)
-> InversionMap Clause -> FunctionInverse' Clause
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> InversionMap Clause -> InversionMap Clause
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel InversionMap Clause
inv
instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where
abstract :: Tele (Dom Type) -> [t] -> [t]
abstract Tele (Dom Type)
tel = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (Tele (Dom Type) -> t -> t
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel)
instance Abstract t => Abstract (Maybe t) where
abstract :: Tele (Dom Type) -> Maybe t -> Maybe t
abstract Tele (Dom Type)
tel Maybe t
x = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> t -> t
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel) Maybe t
x
instance Abstract v => Abstract (Map k v) where
abstract :: Tele (Dom Type) -> Map k v -> Map k v
abstract Tele (Dom Type)
tel Map k v
m = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> v -> v
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel) Map k v
m
instance Abstract v => Abstract (HashMap k v) where
abstract :: Tele (Dom Type) -> HashMap k v -> HashMap k v
abstract Tele (Dom Type)
tel HashMap k v
m = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> v -> v
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel) HashMap k v
m
abstractArgs :: Abstract a => Args -> a -> a
abstractArgs :: forall a. Abstract a => [Arg Term] -> a -> a
abstractArgs [Arg Term]
args a
x = Tele (Dom Type) -> a -> a
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel a
x
where
tel :: Tele (Dom Type)
tel = (Arg [Char] -> Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type) -> [Arg [Char]] -> Tele (Dom Type)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\arg :: Arg [Char]
arg@(Arg ArgInfo
info [Char]
x) -> Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
HasCallStack => Type
__DUMMY_TYPE__ Type -> Dom' Term [Char] -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char] -> Dom' Term [Char]
forall a. Arg a -> Dom a
domFromArg Arg [Char]
arg) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type)
-> Tele (Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs [Char]
x)
Tele (Dom Type)
forall a. Tele a
EmptyTel
([Arg [Char]] -> Tele (Dom Type))
-> [Arg [Char]] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ([Char] -> Arg Term -> Arg [Char])
-> Infinite [Char] -> [Arg Term] -> [Arg [Char]]
forall a b c. (a -> b -> c) -> Infinite a -> [b] -> [c]
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a b c.
Zip f g h =>
(a -> b -> c) -> f a -> g b -> h c
zipWith [Char] -> Arg Term -> Arg [Char]
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) Infinite [Char]
names [Arg Term]
args
names :: Infinite [Char]
names = NonEmpty [Char] -> Infinite [Char]
forall a. NonEmpty a -> Infinite a
ListInf.cycle (NonEmpty [Char] -> Infinite [Char])
-> NonEmpty [Char] -> Infinite [Char]
forall a b. (a -> b) -> a -> b
$ (Char -> [Char]) -> NonEmpty Char -> NonEmpty [Char]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> [Char]
stringToArgName ([Char] -> [Char]) -> (Char -> [Char]) -> Char -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> [Char]
forall el coll. Singleton el coll => el -> coll
singleton) (Char
'a' Char -> [Char] -> NonEmpty Char
forall a. a -> [a] -> NonEmpty a
:| [Char
'b'..Char
'z'])
renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a
renaming :: forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
err Permutation
p = Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
err [Maybe a]
gamma (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS (Int -> Substitution' a) -> Int -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Permutation -> Int
forall a. Sized a => a -> Int
size Permutation
p
where
gamma :: [Maybe a]
gamma :: [Maybe a]
gamma = Permutation -> (Int -> a) -> [Maybe a]
forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p (Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar :: Int -> a)
renamingR :: DeBruijn a => Permutation -> Substitution' a
renamingR :: forall a. DeBruijn a => Permutation -> Substitution' a
renamingR p :: Permutation
p@(Perm Int
n [Int]
is) = [a]
xs [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS Int
n
where
xs :: [a]
xs = (Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map' (\Int
i -> Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)) ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
is)
renameP :: Subst a => Impossible -> Permutation -> a -> a
renameP :: forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
err Permutation
p = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> Permutation -> Substitution' (SubstArg a)
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
err Permutation
p)
data AnySubstitution = AnySub
{ AnySubstitution -> forall a. DeBruijn a => Substitution' a
getSub :: forall a. DeBruijn a => Substitution' a }
toRenOn :: DeBruijn a => VarSet -> Substitution' a -> Maybe AnySubstitution
toRenOn :: forall a.
DeBruijn a =>
VarSet -> Substitution' a -> Maybe AnySubstitution
toRenOn VarSet
vars Substitution' a
rho = Int -> Substitution' a -> Maybe AnySubstitution
go Int
0 Substitution' a
rho
where
go :: Int -> Substitution' a -> Maybe AnySubstitution
go Int
x Substitution' a
IdS = AnySubstitution -> Maybe AnySubstitution
forall a. a -> Maybe a
Just (AnySubstitution -> Maybe AnySubstitution)
-> AnySubstitution -> Maybe AnySubstitution
forall a b. (a -> b) -> a -> b
$ (forall a. DeBruijn a => Substitution' a) -> AnySubstitution
AnySub ((forall a. DeBruijn a => Substitution' a) -> AnySubstitution)
-> (forall a. DeBruijn a => Substitution' a) -> AnySubstitution
forall a b. (a -> b) -> a -> b
$ Substitution' a
forall a. Substitution' a
forall a. DeBruijn a => Substitution' a
IdS
go Int
x (EmptyS Impossible
i) = AnySubstitution -> Maybe AnySubstitution
forall a. a -> Maybe a
Just (AnySubstitution -> Maybe AnySubstitution)
-> AnySubstitution -> Maybe AnySubstitution
forall a b. (a -> b) -> a -> b
$ (forall a. DeBruijn a => Substitution' a) -> AnySubstitution
AnySub ((forall a. DeBruijn a => Substitution' a) -> AnySubstitution)
-> (forall a. DeBruijn a => Substitution' a) -> AnySubstitution
forall a b. (a -> b) -> a -> b
$ Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
i
go Int
x (a
t :# Substitution' a
rho) = do
AnySub rho' <- Int -> Substitution' a -> Maybe AnySubstitution
go (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Substitution' a
rho
if x `VarSet.member` vars
then do
y <- deBruijnView t
Just $ AnySub $ deBruijnVar y :# rho'
else Just $ AnySub $ Strengthen __IMPOSSIBLE__ 1 rho'
go Int
x (Strengthen Impossible
i Int
n Substitution' a
rho) = do
AnySub rho' <- Int -> Substitution' a -> Maybe AnySubstitution
go (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Substitution' a
rho
Just $ AnySub $ Strengthen i n rho'
go Int
x (Wk Int
n Substitution' a
rho) = do
AnySub rho' <- Int -> Substitution' a -> Maybe AnySubstitution
go Int
x Substitution' a
rho
Just $ AnySub $ Wk n rho'
go Int
x (Lift Int
n Substitution' a
rho) = do
AnySub rho' <- Int -> Substitution' a -> Maybe AnySubstitution
go (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Substitution' a
rho
Just $ AnySub $ Lift n rho'
instance EndoSubst a => Subst (Substitution' a) where
type SubstArg (Substitution' a) = a
applySubst :: Substitution' (SubstArg (Substitution' a))
-> Substitution' a -> Substitution' a
applySubst Substitution' (SubstArg (Substitution' a))
rho Substitution' a
sgm = Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
Substitution' (SubstArg (Substitution' a))
rho Substitution' a
sgm
{-# INLINE applySubstTerm #-}
applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
applySubstTerm :: forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm Substitution' t
IdS t
t = t
t
applySubstTerm Substitution' t
rho t
t = Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ case t -> Term
forall a b. Coercible a b => a -> b
coerce t
t of
Var Int
i Elims
es -> let !t :: t
t = Substitution' t -> Int -> t
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' t
rho Int
i in t -> Term
forall a b. Coercible a b => a -> b
coerce (t
t t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es)
Lam ArgInfo
h Abs Term
m -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$! forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Abs t) Substitution' t
rho Abs Term
m
Def QName
f Elims
es -> QName -> Elims -> Elims -> Term
defApp QName
f [] (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
vs
MetaV MetaId
x Elims
es -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
Lit Literal
l -> Literal -> Term
Lit Literal
l
Level Level
l -> Level -> Term
levelTm (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Level' t) Substitution' t
rho Level
l
Pi Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> Term
Pi (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Dom' t (Type'' t t)) Substitution' t
rho Dom Type
a) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Abs (Type'' t t)) Substitution' t
rho Abs Type
b)
Sort Sort' Term
s -> Sort' Term -> Term
Sort (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Sort' t) Substitution' t
rho Sort' Term
s)
DontCare Term
mv -> Term -> Term
dontCare (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
mv)
Dummy DummyTermKind
s Elims
es -> DummyTermKind -> Elims -> Term
Dummy DummyTermKind
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
where
sub :: forall a b. (Coercible b a, SubstWith t a) => Substitution' t -> b -> b
sub :: forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub Substitution' t
rho b
t = a -> b
forall a b. Coercible a b => a -> b
coerce (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' t
Substitution' (SubstArg a)
rho (b -> a
forall a b. Coercible a b => a -> b
coerce b
t :: a)); {-# INLINE sub #-}
subE :: Substitution' t -> Elims -> Elims
subE :: Substitution' t -> Elims -> Elims
subE Substitution' t
rho [] = []
subE Substitution' t
rho (Elim' Term
a:Elims
as) = case Elim' Term
a of
Apply (Arg ArgInfo
i Term
t) ->
let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
| Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
in (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
t))Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as
p :: Elim' Term
p@Proj{} -> (Elim' Term
p Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as
IApply Term
l Term
r Term
t -> (Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
l) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
r) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
t)Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as
instance Subst Term where
type SubstArg Term = Term
applySubst :: Substitution' (SubstArg Term) -> Term -> Term
applySubst = Substitution' Term -> Term -> Term
Substitution' (SubstArg Term) -> Term -> Term
forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm
{-# SPECIALIZE lookupS :: Substitution' Term -> Nat -> Term #-}
{-# SPECIALIZE isNoAbs :: Abs Term -> Maybe Term #-}
instance Subst BraveTerm where
type SubstArg BraveTerm = BraveTerm
applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
applySubst = Substitution' BraveTerm -> BraveTerm -> BraveTerm
Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm
instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) where
type SubstArg (Type'' a b) = SubstArg a
applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b
applySubst Substitution' (SubstArg (Type'' a b))
rho (El Sort' a
s b
t) = Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
Substitution' (SubstArg (Type'' a b))
rho Sort' a
s Sort' a -> b -> Type'' a b
forall t a. Sort' t -> a -> Type'' t a
`El` Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Type'' a b))
rho b
t
instance Subst a => Subst (Sort' a) where
type SubstArg (Sort' a) = SubstArg a
applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
applySubst Substitution' (SubstArg (Sort' a))
rho = \case
Univ Univ
u Level' a
n -> Univ -> Level' a -> Sort' a
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Level' a))
Substitution' (SubstArg (Sort' a))
rho Level' a
n
Inf Univ
u Integer
n -> Univ -> Integer -> Sort' a
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
Sort' a
SizeUniv -> Sort' a
forall t. Sort' t
SizeUniv
Sort' a
LockUniv -> Sort' a
forall t. Sort' t
LockUniv
Sort' a
LevelUniv -> Sort' a
forall t. Sort' t
LevelUniv
Sort' a
IntervalUniv -> Sort' a
forall t. Sort' t
IntervalUniv
PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2 -> ((Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a)
-> Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Dom' a a)) -> Dom' a a -> Dom' a a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
Substitution' (SubstArg (Dom' a a))
rho Dom' a a
a) (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s1)) (Abs (Sort' a) -> Sort' a) -> Abs (Sort' a) -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Abs (Sort' a)))
-> Abs (Sort' a) -> Abs (Sort' a)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
Substitution' (SubstArg (Abs (Sort' a)))
rho Abs (Sort' a)
s2
FunSort Sort' a
s1 Sort' a
s2 -> Sort' a -> Sort' a -> Sort' a
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s1) (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s2)
UnivSort Sort' a
s -> Sort' a -> Sort' a
forall t. Sort' t -> Sort' t
UnivSort (Sort' a -> Sort' a) -> Sort' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s
MetaS MetaId
x [Elim' a]
es -> MetaId -> [Elim' a] -> Sort' a
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
Substitution' (SubstArg (Sort' a))
rho [Elim' a]
es
DefS QName
d [Elim' a]
es -> QName -> [Elim' a] -> Sort' a
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
Substitution' (SubstArg (Sort' a))
rho [Elim' a]
es
s :: Sort' a
s@DummyS{} -> Sort' a
s
where
subE :: Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE :: Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [] = []
subE Substitution' (SubstArg a)
rho (Elim' a
a:[Elim' a]
as) = case Elim' a
a of
Apply (Arg ArgInfo
i a
t) ->
let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
| Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
in (Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
t))Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:) ([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as
p :: Elim' a
p@Proj{} -> (Elim' a
p Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:) ([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as
IApply a
l a
r a
t -> (a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
l) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
r) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
t)Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:)
([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as
instance Subst a => Subst (Level' a) where
type SubstArg (Level' a) = SubstArg a
applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a
applySubst Substitution' (SubstArg (Level' a))
rho (Max Integer
n [PlusLevel' a]
as) = Integer -> [PlusLevel' a] -> Level' a
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' a] -> Level' a) -> [PlusLevel' a] -> Level' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [PlusLevel' a] -> [PlusLevel' a]
forall {t}.
Subst t =>
Substitution' (SubstArg t) -> [PlusLevel' t] -> [PlusLevel' t]
go Substitution' (SubstArg a)
Substitution' (SubstArg (Level' a))
rho [PlusLevel' a]
as where
go :: Substitution' (SubstArg t) -> [PlusLevel' t] -> [PlusLevel' t]
go Substitution' (SubstArg t)
rho [] = []
go Substitution' (SubstArg t)
rho (Plus Integer
x t
y : [PlusLevel' t]
as) = (:) (PlusLevel' t -> [PlusLevel' t] -> [PlusLevel' t])
-> PlusLevel' t -> [PlusLevel' t] -> [PlusLevel' t]
forall a b. (a -> b) -> a -> b
$$! (Integer -> t -> PlusLevel' t
forall t. Integer -> t -> PlusLevel' t
Plus Integer
x (t -> PlusLevel' t) -> t -> PlusLevel' t
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg t) -> t -> t
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg t)
rho t
y) ([PlusLevel' t] -> [PlusLevel' t])
-> [PlusLevel' t] -> [PlusLevel' t]
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg t) -> [PlusLevel' t] -> [PlusLevel' t]
go Substitution' (SubstArg t)
rho [PlusLevel' t]
as
instance Subst a => Subst (PlusLevel' a) where
type SubstArg (PlusLevel' a) = SubstArg a
applySubst :: Substitution' (SubstArg (PlusLevel' a))
-> PlusLevel' a -> PlusLevel' a
applySubst Substitution' (SubstArg (PlusLevel' a))
rho (Plus Integer
n a
l) = Integer -> a -> PlusLevel' a
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (a -> PlusLevel' a) -> a -> PlusLevel' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (PlusLevel' a))
rho a
l
instance Subst Name where
type SubstArg Name = Term
applySubst :: Substitution' (SubstArg Name) -> Name -> Name
applySubst Substitution' (SubstArg Name)
rho = Name -> Name
forall a. a -> a
id
instance Subst ConPatternInfo where
type SubstArg ConPatternInfo = Term
applySubst :: Substitution' (SubstArg ConPatternInfo)
-> ConPatternInfo -> ConPatternInfo
applySubst Substitution' (SubstArg ConPatternInfo)
rho ConPatternInfo
i = ConPatternInfo
i{ conPType = applySubst rho $ conPType i }
instance Subst Pattern where
type SubstArg Pattern = Term
applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern
applySubst Substitution' (SubstArg Pattern)
rho = \case
ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
ps -> ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (Substitution' (SubstArg ConPatternInfo)
-> ConPatternInfo -> ConPatternInfo
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg ConPatternInfo)
Substitution' (SubstArg Pattern)
rho ConPatternInfo
mt) ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg Pattern])
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg Pattern])
Substitution' (SubstArg Pattern)
rho [NamedArg Pattern]
ps
DefP PatternInfo
o QName
q [NamedArg Pattern]
ps -> PatternInfo -> QName -> [NamedArg Pattern] -> Pattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg Pattern])
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg Pattern])
Substitution' (SubstArg Pattern)
rho [NamedArg Pattern]
ps
DotP PatternInfo
o Term
t -> PatternInfo -> Term -> Pattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o (Term -> Pattern) -> Term -> Pattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Pattern)
Substitution' (SubstArg Term)
rho Term
t
p :: Pattern
p@(VarP PatternInfo
_o [Char]
_x) -> Pattern
p
p :: Pattern
p@(LitP PatternInfo
_o Literal
_l) -> Pattern
p
p :: Pattern
p@(ProjP ProjOrigin
_o QName
_x) -> Pattern
p
IApplyP PatternInfo
o Term
t Term
u [Char]
x -> PatternInfo -> Term -> Term -> [Char] -> Pattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Pattern)
Substitution' (SubstArg Term)
rho Term
t) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Pattern)
Substitution' (SubstArg Term)
rho Term
u) [Char]
x
instance Subst A.ProblemEq where
type SubstArg A.ProblemEq = Term
applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq
applySubst Substitution' (SubstArg ProblemEq)
rho (A.ProblemEq Pattern
p Term
v Dom Type
a) =
(Term -> Dom Type -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Pattern -> Term -> Dom Type -> ProblemEq
A.ProblemEq Pattern
p) ((Term, Dom Type) -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Term, Dom Type))
-> (Term, Dom Type) -> (Term, Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Term, Dom Type))
Substitution' (SubstArg ProblemEq)
rho (Term
v,Dom Type
a)
instance DeBruijn BraveTerm where
deBruijnVar :: Int -> BraveTerm
deBruijnVar = Term -> BraveTerm
BraveTerm (Term -> BraveTerm) -> (Int -> Term) -> Int -> BraveTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
forall a. DeBruijn a => Int -> a
deBruijnVar
deBruijnView :: BraveTerm -> Maybe Int
deBruijnView = Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (Term -> Maybe Int)
-> (BraveTerm -> Term) -> BraveTerm -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BraveTerm -> Term
unBrave
instance DeBruijn NLPat where
deBruijnVar :: Int -> NLPat
deBruijnVar Int
i = DefSing -> Int -> [Arg Int] -> NLPat
PVar DefSing
MaybeSing Int
i []
deBruijnView :: NLPat -> Maybe Int
deBruijnView = \case
PVar DefSing
s Int
i [] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
PVar{} -> Maybe Int
forall a. Maybe a
Nothing
PDef{} -> Maybe Int
forall a. Maybe a
Nothing
PLam{} -> Maybe Int
forall a. Maybe a
Nothing
PPi{} -> Maybe Int
forall a. Maybe a
Nothing
PSort{} -> Maybe Int
forall a. Maybe a
Nothing
PBoundVar Int
i [] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
PBoundVar{} -> Maybe Int
forall a. Maybe a
Nothing
PTerm{} -> Maybe Int
forall a. Maybe a
Nothing
applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst :: forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst = Substitution' Term -> a -> a
Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' Term -> a -> a)
-> (Substitution' NLPat -> Substitution' Term)
-> Substitution' NLPat
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NLPat -> Term) -> Substitution' NLPat -> Substitution' Term
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NLPat -> Term
nlPatToTerm
where
nlPatToTerm :: NLPat -> Term
nlPatToTerm :: NLPat -> Term
nlPatToTerm = \case
PVar DefSing
s Int
i [Arg Int]
xs -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Int -> Elim' Term) -> [Arg Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Arg Int -> Arg Term) -> Arg Int -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Term) -> Arg Int -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
xs
PTerm Term
u -> Term
u
PDef QName
f [Elim' NLPat]
es -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PLam ArgInfo
i Abs NLPat
u -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PPi Dom NLPType
a Abs NLPType
b -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PSort NLPSort
s -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PBoundVar Int
i [Elim' NLPat]
es -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom :: forall a.
SubstWith NLPat a =>
Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
rho Dom a
dom =
Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' NLPat
Substitution' (SubstArg a)
rho (a -> a) -> Dom a -> Dom a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom a
dom Dom a -> (Dom a -> Dom a) -> Dom a
forall a b. a -> (a -> b) -> b
& (Maybe Term -> Identity (Maybe Term)) -> Dom a -> Identity (Dom a)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic ((Maybe Term -> Identity (Maybe Term))
-> Dom a -> Identity (Dom a))
-> (Maybe Term -> Maybe Term) -> Dom a -> Dom a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Substitution' NLPat -> Maybe Term -> Maybe Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
rho)
lookupSVar :: EndoSubst a => Substitution' a -> Nat -> Maybe Nat
lookupSVar :: forall a. EndoSubst a => Substitution' a -> Int -> Maybe Int
lookupSVar Substitution' a
sub Int
x = a -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (a -> Maybe Int) -> a -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Substitution' a -> Int -> a
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' a
sub Int
x
instance Subst NLPat where
type SubstArg NLPat = NLPat
applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat
applySubst Substitution' (SubstArg NLPat)
rho = \case
PVar DefSing
s Int
i [Arg Int]
bvs -> Substitution' NLPat -> Int -> NLPat
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' NLPat
Substitution' (SubstArg NLPat)
rho Int
i NLPat -> [Arg Int] -> NLPat
`applyBV` [Arg Int]
bvs
PDef QName
f [Elim' NLPat]
es -> QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Elim' NLPat])
-> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Elim' NLPat])
Substitution' (SubstArg NLPat)
rho [Elim' NLPat]
es
PLam ArgInfo
i Abs NLPat
u -> ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
i (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Abs NLPat)) -> Abs NLPat -> Abs NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPat)
Substitution' (SubstArg (Abs NLPat))
rho Abs NLPat
u
PPi Dom NLPType
a Abs NLPType
b -> Dom NLPType -> Abs NLPType -> NLPat
PPi (Substitution' NLPat -> Dom NLPType -> Dom NLPType
forall a.
SubstWith NLPat a =>
Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
Substitution' (SubstArg NLPat)
rho Dom NLPType
a) (Substitution' (SubstArg (Abs NLPType))
-> Abs NLPType -> Abs NLPType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPat)
Substitution' (SubstArg (Abs NLPType))
rho Abs NLPType
b)
PSort NLPSort
s -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> NLPSort -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPSort
s
PBoundVar Int
i [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> NLPat
PBoundVar (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> Int -> Maybe Int
forall a. EndoSubst a => Substitution' a -> Int -> Maybe Int
lookupSVar Substitution' NLPat
Substitution' (SubstArg NLPat)
rho Int
i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Elim' NLPat])
-> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Elim' NLPat])
Substitution' (SubstArg NLPat)
rho [Elim' NLPat]
es
PTerm Term
u -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
Substitution' (SubstArg NLPat)
rho Term
u
where
applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV NLPat
p [Arg Int]
ys = case NLPat
p of
PVar DefSing
s Int
i [Arg Int]
xs -> DefSing -> Int -> [Arg Int] -> NLPat
PVar DefSing
s Int
i ([Arg Int] -> NLPat) -> [Arg Int] -> NLPat
forall a b. (a -> b) -> a -> b
$! [Arg Int]
xs [Arg Int] -> [Arg Int] -> [Arg Int]
forall a. [a] -> [a] -> [a]
++! [Arg Int]
ys
PTerm Term
u -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Term
u Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` (Arg Int -> Arg Term) -> [Arg Int] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map' ((Int -> Term) -> Arg Int -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
ys
PDef QName
f [Elim' NLPat]
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PLam ArgInfo
i Abs NLPat
u -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PPi Dom NLPType
a Abs NLPType
b -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PSort NLPSort
s -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PBoundVar Int
i [Elim' NLPat]
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Subst NLPType where
type SubstArg NLPType = NLPat
applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType
applySubst Substitution' (SubstArg NLPType)
rho (NLPType NLPSort
s NLPat
a) = NLPSort -> NLPat -> NLPType
NLPType (Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPType)
rho NLPSort
s) (Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPType)
Substitution' (SubstArg NLPat)
rho NLPat
a)
instance Subst NLPSort where
type SubstArg NLPSort = NLPat
applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
applySubst Substitution' (SubstArg NLPSort)
rho = \case
PUniv Univ
u NLPat
l -> Univ -> NLPat -> NLPSort
PUniv Univ
u (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPat
l
PInf Univ
f Integer
n -> Univ -> Integer -> NLPSort
PInf Univ
f Integer
n
NLPSort
PSizeUniv -> NLPSort
PSizeUniv
NLPSort
PLockUniv -> NLPSort
PLockUniv
NLPSort
PLevelUniv -> NLPSort
PLevelUniv
NLPSort
PIntervalUniv -> NLPSort
PIntervalUniv
instance Subst GlobalRewriteRule where
type SubstArg GlobalRewriteRule = NLPat
applySubst :: Substitution' (SubstArg GlobalRewriteRule)
-> GlobalRewriteRule -> GlobalRewriteRule
applySubst Substitution' (SubstArg GlobalRewriteRule)
rho (GlobalRewriteRule QName
q Tele (Dom Type)
gamma QName
f [Elim' NLPat]
ps Term
rhs Type
t Bool
c TopLevelModuleName
top) =
QName
-> Tele (Dom Type)
-> QName
-> [Elim' NLPat]
-> Term
-> Type
-> Bool
-> TopLevelModuleName
-> GlobalRewriteRule
GlobalRewriteRule QName
q (Substitution' NLPat -> Tele (Dom Type) -> Tele (Dom Type)
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
Substitution' (SubstArg GlobalRewriteRule)
rho Tele (Dom Type)
gamma)
QName
f (Substitution' (SubstArg [Elim' NLPat])
-> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
Substitution' (SubstArg GlobalRewriteRule)
rho) [Elim' NLPat]
ps)
(Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
Substitution' (SubstArg GlobalRewriteRule)
rho) Term
rhs)
(Substitution' NLPat -> Type -> Type
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
Substitution' (SubstArg GlobalRewriteRule)
rho) Type
t)
Bool
c TopLevelModuleName
top
where n :: Int
n = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma
instance Subst a => Subst (LocalEquation' a) where
type SubstArg (LocalEquation' a) = SubstArg a
applySubst :: Substitution' (SubstArg (LocalEquation' a))
-> LocalEquation' a -> LocalEquation' a
applySubst Substitution' (SubstArg (LocalEquation' a))
rho (LocalEquation Tele (Dom' a (Type'' a a))
gamma a
lhs a
rhs Type'' a a
t) =
Tele (Dom' a (Type'' a a))
-> a -> a -> Type'' a a -> LocalEquation' a
forall t.
Tele (Dom' t (Type'' t t))
-> t -> t -> Type'' t t -> LocalEquation' t
LocalEquation (Substitution' (SubstArg (Tele (Dom' a (Type'' a a))))
-> Tele (Dom' a (Type'' a a)) -> Tele (Dom' a (Type'' a a))
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (LocalEquation' a))
Substitution' (SubstArg (Tele (Dom' a (Type'' a a))))
rho Tele (Dom' a (Type'' a a))
gamma)
(Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho' a
lhs)
(Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho' a
rhs)
(Substitution' (SubstArg (Type'' a a)) -> Type'' a a -> Type'' a a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Type'' a a))
rho' Type'' a a
t)
where rho' :: Substitution' (SubstArg a)
rho' = Int -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom' a (Type'' a a)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' a (Type'' a a))
gamma) Substitution' (SubstArg a)
Substitution' (SubstArg (LocalEquation' a))
rho
instance Subst RewriteHead where
type SubstArg RewriteHead = Term
applySubst :: Substitution' (SubstArg RewriteHead) -> RewriteHead -> RewriteHead
applySubst Substitution' (SubstArg RewriteHead)
rho (RewDefHead QName
f) = QName -> RewriteHead
RewDefHead QName
f
applySubst Substitution' (SubstArg RewriteHead)
rho (RewVarHead Int
x) = Int -> RewriteHead
RewVarHead (Int -> RewriteHead) -> Int -> RewriteHead
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$
Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (Term -> Maybe Int) -> Term -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
Substitution' (SubstArg RewriteHead)
rho Int
x
applySubstLocalRewrite :: DeBruijn a
=> Substitution' a -> RewriteRule -> Maybe RewriteRule
applySubstLocalRewrite :: forall a.
DeBruijn a =>
Substitution' a -> RewriteRule -> Maybe RewriteRule
applySubstLocalRewrite Substitution' a
rho rew :: RewriteRule
rew@(RewriteRule Tele (Dom Type)
gamma RewriteHead
f [Elim' NLPat]
ps Term
rhs Type
b) =
case VarSet -> Substitution' a -> Maybe AnySubstitution
forall a.
DeBruijn a =>
VarSet -> Substitution' a -> Maybe AnySubstitution
toRenOn (RewriteRule -> VarSet
forall t. Free t => t -> VarSet
freeVarSet RewriteRule
rew) Substitution' a
rho of
Just (AnySub forall a. DeBruijn a => Substitution' a
rho') -> do
let rho'' :: DeBruijn a => Substitution' a
rho'' :: forall a. DeBruijn a => Substitution' a
rho'' = Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma) Substitution' a
forall a. DeBruijn a => Substitution' a
rho'
RewriteRule -> Maybe RewriteRule
forall a. a -> Maybe a
Just (RewriteRule -> Maybe RewriteRule)
-> RewriteRule -> Maybe RewriteRule
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> RewriteHead -> [Elim' NLPat] -> Term -> Type -> RewriteRule
RewriteRule (Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
forall a. DeBruijn a => Substitution' a
rho' Tele (Dom Type)
gamma)
(Substitution' (SubstArg RewriteHead) -> RewriteHead -> RewriteHead
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg RewriteHead)
forall a. DeBruijn a => Substitution' a
rho' RewriteHead
f)
(Substitution' (SubstArg [Elim' NLPat])
-> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' NLPat
Substitution' (SubstArg [Elim' NLPat])
forall a. DeBruijn a => Substitution' a
rho'' [Elim' NLPat]
ps)
(Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
forall a. DeBruijn a => Substitution' a
rho'' Term
rhs)
(Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
forall a. DeBruijn a => Substitution' a
rho'' Type
b)
Maybe AnySubstitution
Nothing -> Maybe RewriteRule
forall a. Maybe a
Nothing
instance Subst a => Subst (RewDom' a) where
type SubstArg (RewDom' a) = SubstArg a
applySubst :: Substitution' (SubstArg (RewDom' a)) -> RewDom' a -> RewDom' a
applySubst Substitution' (SubstArg (RewDom' a))
rho (RewDom LocalEquation' a
eq Maybe RewriteRule
rew) =
LocalEquation' a -> Maybe RewriteRule -> RewDom' a
forall t. LocalEquation' t -> Maybe RewriteRule -> RewDom' t
RewDom (Substitution' (SubstArg (LocalEquation' a))
-> LocalEquation' a -> LocalEquation' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (LocalEquation' a))
Substitution' (SubstArg (RewDom' a))
rho LocalEquation' a
eq)
(Substitution' (SubstArg a) -> RewriteRule -> Maybe RewriteRule
forall a.
DeBruijn a =>
Substitution' a -> RewriteRule -> Maybe RewriteRule
applySubstLocalRewrite Substitution' (SubstArg a)
Substitution' (SubstArg (RewDom' a))
rho (RewriteRule -> Maybe RewriteRule)
-> Maybe RewriteRule -> Maybe RewriteRule
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe RewriteRule
rew)
instance Subst a => Subst (Blocked a) where
type SubstArg (Blocked a) = SubstArg a
applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a
applySubst Substitution' (SubstArg (Blocked a))
rho Blocked a
b = (a -> a) -> Blocked a -> Blocked a
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Blocked a))
rho) Blocked a
b
instance Subst DisplayForm where
type SubstArg DisplayForm = Term
applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm
applySubst Substitution' (SubstArg DisplayForm)
rho (Display Int
n Elims
ps DisplayTerm
v) =
let rho' :: Substitution' Term
rho' = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
Substitution' (SubstArg DisplayForm)
rho
!ps' :: Elims
ps' = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Elims)
rho' Elims
ps in
Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n Elims
ps' (Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg DisplayTerm)
rho' DisplayTerm
v)
instance Subst DisplayTerm where
type SubstArg DisplayTerm = Term
applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
applySubst Substitution' (SubstArg DisplayTerm)
rho (DTerm' Term
v Elims
es) = Term -> Elims -> DisplayTerm
DTerm' (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg DisplayTerm)
rho Term
v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Elims)
Substitution' (SubstArg DisplayTerm)
rho Elims
es
applySubst Substitution' (SubstArg DisplayTerm)
rho (DDot' Term
v Elims
es) = Term -> Elims -> DisplayTerm
DDot' (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg DisplayTerm)
rho Term
v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Elims)
Substitution' (SubstArg DisplayTerm)
rho Elims
es
applySubst Substitution' (SubstArg DisplayTerm)
rho (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs) = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Arg DisplayTerm])
-> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Arg DisplayTerm])
Substitution' (SubstArg DisplayTerm)
rho [Arg DisplayTerm]
vs
applySubst Substitution' (SubstArg DisplayTerm)
rho (DDef QName
c [Elim' DisplayTerm]
es) = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Elim' DisplayTerm])
-> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Elim' DisplayTerm])
Substitution' (SubstArg DisplayTerm)
rho [Elim' DisplayTerm]
es
applySubst Substitution' (SubstArg DisplayTerm)
rho (DWithApp DisplayTerm
v List1 DisplayTerm
vs Elims
es) = (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)
-> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp ((DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm)
-> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
-> (DisplayTerm, List1 DisplayTerm, Elims)
-> (DisplayTerm, List1 DisplayTerm, Elims)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
Substitution' (SubstArg DisplayTerm)
rho (DisplayTerm
v, List1 DisplayTerm
vs, Elims
es)
instance Subst a => Subst (Tele a) where
type SubstArg (Tele a) = SubstArg a
applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a
applySubst Substitution' (SubstArg (Tele a))
rho Tele a
EmptyTel = Tele a
forall a. Tele a
EmptyTel
applySubst Substitution' (SubstArg (Tele a))
rho (ExtendTel a
t Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Tele a))
rho a
t) (Abs (Tele a) -> Tele a) -> Abs (Tele a) -> Tele a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Abs (Tele a)))
-> Abs (Tele a) -> Abs (Tele a)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Tele a))
Substitution' (SubstArg (Abs (Tele a)))
rho Abs (Tele a)
tel
instance Subst Constraint where
type SubstArg Constraint = Term
applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint
applySubst Substitution' (SubstArg Constraint)
rho = \case
ValueCmp Comparison
cmp CompareAs
a Term
u Term
v -> Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp (CompareAs -> CompareAs
forall a. TermSubst a => a -> a
rf CompareAs
a) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
u) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v)
ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v -> Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
cmp (Term -> Term
forall a. TermSubst a => a -> a
rf Term
p) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
t) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
u) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v)
ElimCmp [Polarity]
ps [IsForced]
fs Type
a Term
v Elims
e1 Elims
e2 -> [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
ps [IsForced]
fs (Type -> Type
forall a. TermSubst a => a -> a
rf Type
a) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v) (Elims -> Elims
forall a. TermSubst a => a -> a
rf Elims
e1) (Elims -> Elims
forall a. TermSubst a => a -> a
rf Elims
e2)
SortCmp Comparison
cmp Sort' Term
s1 Sort' Term
s2 -> Comparison -> Sort' Term -> Sort' Term -> Constraint
SortCmp Comparison
cmp (Sort' Term -> Sort' Term
forall a. TermSubst a => a -> a
rf Sort' Term
s1) (Sort' Term -> Sort' Term
forall a. TermSubst a => a -> a
rf Sort' Term
s2)
LevelCmp Comparison
cmp Level
l1 Level
l2 -> Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp (Level -> Level
forall a. TermSubst a => a -> a
rf Level
l1) (Level -> Level
forall a. TermSubst a => a -> a
rf Level
l2)
IsEmpty Range
r Type
a -> Range -> Type -> Constraint
IsEmpty Range
r (Type -> Type
forall a. TermSubst a => a -> a
rf Type
a)
CheckSizeLtSat Term
t -> Term -> Constraint
CheckSizeLtSat (Term -> Term
forall a. TermSubst a => a -> a
rf Term
t)
FindInstance Range
r MetaId
m Maybe [Candidate]
cands -> Range -> MetaId -> Maybe [Candidate] -> Constraint
FindInstance Range
r MetaId
m (Maybe [Candidate] -> Maybe [Candidate]
forall a. TermSubst a => a -> a
rf Maybe [Candidate]
cands)
ResolveInstanceHead KwRange
kwr QName
q -> KwRange -> QName -> Constraint
ResolveInstanceHead KwRange
kwr (QName -> QName
forall a. TermSubst a => a -> a
rf QName
q)
c :: Constraint
c@UnBlock{} -> Constraint
c
c :: Constraint
c@CheckFunDef{} -> Constraint
c
HasBiggerSort Sort' Term
s -> Sort' Term -> Constraint
HasBiggerSort (Sort' Term -> Sort' Term
forall a. TermSubst a => a -> a
rf Sort' Term
s)
HasPTSRule Dom Type
a Abs (Sort' Term)
s -> Dom Type -> Abs (Sort' Term) -> Constraint
HasPTSRule (Dom Type -> Dom Type
forall a. TermSubst a => a -> a
rf Dom Type
a) (Abs (Sort' Term) -> Abs (Sort' Term)
forall a. TermSubst a => a -> a
rf Abs (Sort' Term)
s)
CheckLockedVars Term
a Type
b Arg Term
c Type
d -> Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Term -> Term
forall a. TermSubst a => a -> a
rf Term
a) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
b) (Arg Term -> Arg Term
forall a. TermSubst a => a -> a
rf Arg Term
c) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
d)
UnquoteTactic Term
t Term
h Type
g -> Term -> Term -> Type -> Constraint
UnquoteTactic (Term -> Term
forall a. TermSubst a => a -> a
rf Term
t) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
h) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
g)
CheckDataSort QName
q Sort' Term
s -> QName -> Sort' Term -> Constraint
CheckDataSort QName
q (Sort' Term -> Sort' Term
forall a. TermSubst a => a -> a
rf Sort' Term
s)
CheckMetaInst MetaId
m -> MetaId -> Constraint
CheckMetaInst MetaId
m
CheckType Type
t -> Type -> Constraint
CheckType (Type -> Type
forall a. TermSubst a => a -> a
rf Type
t)
UsableAtModality WhyCheckModality
cc Maybe (Sort' Term)
ms Modality
mod Term
m -> WhyCheckModality
-> Maybe (Sort' Term) -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc (Maybe (Sort' Term) -> Maybe (Sort' Term)
forall a. TermSubst a => a -> a
rf Maybe (Sort' Term)
ms) Modality
mod (Term -> Term
forall a. TermSubst a => a -> a
rf Term
m)
RewConstraint LocalEquation' Term
e -> LocalEquation' Term -> Constraint
RewConstraint (LocalEquation' Term -> LocalEquation' Term
forall a. TermSubst a => a -> a
rf LocalEquation' Term
e)
where
{-# INLINE rf #-}
rf :: forall a. TermSubst a => a -> a
rf :: forall a. TermSubst a => a -> a
rf a
x = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg Constraint)
rho a
x
instance Subst CompareAs where
type SubstArg CompareAs = Term
applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs
applySubst Substitution' (SubstArg CompareAs)
rho (AsTermsOf Type
a) = Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> Type -> CompareAs
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg CompareAs)
rho Type
a
applySubst Substitution' (SubstArg CompareAs)
rho CompareAs
AsSizes = CompareAs
AsSizes
applySubst Substitution' (SubstArg CompareAs)
rho CompareAs
AsTypes = CompareAs
AsTypes
instance Subst a => Subst (Elim' a) where
type SubstArg (Elim' a) = SubstArg a
applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a
applySubst Substitution' (SubstArg (Elim' a))
rho = \case
Apply Arg a
v -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg a))
Substitution' (SubstArg (Elim' a))
rho Arg a
v)
IApply a
x a
y a
r -> a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
x) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
y) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
r)
e :: Elim' a
e@Proj{} -> Elim' a
e
instance Subst a => Subst (Abs a) where
type SubstArg (Abs a) = SubstArg a
applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a
applySubst Substitution' (SubstArg (Abs a))
rho (Abs [Char]
x a
a) = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
Abs [Char]
x (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' (SubstArg a)
Substitution' (SubstArg (Abs a))
rho) a
a)
applySubst Substitution' (SubstArg (Abs a))
rho (NoAbs [Char]
x a
a) = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Abs a))
rho a
a)
instance Subst a => Subst (Arg a) where
{-# INLINE applySubst #-}
type SubstArg (Arg a) = SubstArg a
applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
applySubst Substitution' (SubstArg (Arg a))
IdS Arg a
arg = Arg a
arg
applySubst Substitution' (SubstArg (Arg a))
rho (Arg ArgInfo
i a
t) =
let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
| Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
in ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (a -> Arg a) -> a -> Arg a
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Arg a))
rho a
t
instance Subst a => Subst (Named name a) where
type SubstArg (Named name a) = SubstArg a
{-# INLINE applySubst #-}
applySubst :: Substitution' (SubstArg (Named name a))
-> Named name a -> Named name a
applySubst Substitution' (SubstArg (Named name a))
rho = (a -> a) -> Named name a -> Named name a
forall a b. (a -> b) -> Named name a -> Named name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Named name a))
rho)
instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) where
type SubstArg (Dom' a b) = SubstArg a
{-# INLINE applySubst #-}
applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b
applySubst Substitution' (SubstArg (Dom' a b))
IdS Dom' a b
dom = Dom' a b
dom
applySubst Substitution' (SubstArg (Dom' a b))
rho (Dom' inf :: DomInfo a
inf@(DomInfo ArgInfo
i Maybe NamedName
n Bool
f Maybe a
t Maybe (RewDom' a)
rw) b
e) =
let i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
| Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i in
let inf' :: DomInfo a
inf' | Maybe a
Nothing <- Maybe a
t, Maybe (RewDom' a)
Nothing <- Maybe (RewDom' a)
rw = DomInfo a
inf
| Bool
otherwise = ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe a
-> Maybe (RewDom' a)
-> DomInfo a
forall t.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> DomInfo t
DomInfo ArgInfo
i' Maybe NamedName
n Bool
f (Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Maybe a))
Substitution' (SubstArg (Dom' a b))
rho Maybe a
t) (Substitution' (SubstArg (Maybe (RewDom' a)))
-> Maybe (RewDom' a) -> Maybe (RewDom' a)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Maybe (RewDom' a)))
Substitution' (SubstArg (Dom' a b))
rho Maybe (RewDom' a)
rw) in
DomInfo a -> b -> Dom' a b
forall t e. DomInfo t -> e -> Dom' t e
Dom' DomInfo a
inf' (b -> Dom' a b) -> b -> Dom' a b
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Dom' a b))
rho b
e
instance Subst LetBinding where
type SubstArg LetBinding = Term
applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding
applySubst Substitution' (SubstArg LetBinding)
rho (LetBinding IsAxiom
isAxiom Origin
o Term
v Dom Type
t) = IsAxiom -> Origin -> Term -> Dom Type -> LetBinding
LetBinding IsAxiom
isAxiom Origin
o (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg LetBinding)
rho Term
v) (Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom Type))
Substitution' (SubstArg LetBinding)
rho Dom Type
t)
instance Subst ContextEntry where
type SubstArg ContextEntry = Term
applySubst :: Substitution' (SubstArg ContextEntry)
-> ContextEntry -> ContextEntry
applySubst Substitution' (SubstArg ContextEntry)
rho (CtxVar Name
x Dom Type
a) = Name -> Dom Type -> ContextEntry
CtxVar Name
x (Dom Type -> ContextEntry) -> Dom Type -> ContextEntry
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom Type))
Substitution' (SubstArg ContextEntry)
rho Dom Type
a
instance Subst a => Subst (Maybe a) where
type SubstArg (Maybe a) = SubstArg a
applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a
applySubst Substitution' (SubstArg (Maybe a))
rho Maybe a
ma = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Maybe a))
rho (a -> a) -> Maybe a -> Maybe a
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Maybe a
ma
instance Subst a => Subst [a] where
type SubstArg [a] = SubstArg a
applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a]
applySubst Substitution' (SubstArg [a])
rho [] = []
applySubst Substitution' (SubstArg [a])
rho (a
a:[a]
as) = let !as' :: [a]
as' = Substitution' (SubstArg [a]) -> [a] -> [a]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [a])
rho [a]
as in Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg [a])
rho a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as'
instance Subst a => Subst (List1 a) where
type SubstArg (List1 a) = SubstArg a
applySubst :: Substitution' (SubstArg (List1 a)) -> List1 a -> List1 a
applySubst Substitution' (SubstArg (List1 a))
rho (a
a :| [a]
as) = let !as' :: [a]
as' = Substitution' (SubstArg [a]) -> [a] -> [a]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [a])
Substitution' (SubstArg (List1 a))
rho [a]
as in Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (List1 a))
rho a
a a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
as'
instance (Ord k, Subst a) => Subst (Map k a) where
type SubstArg (Map k a) = SubstArg a
instance Subst a => Subst (Ranged a) where
type SubstArg (Ranged a) = SubstArg a
instance Subst a => Subst (WithHiding a) where
type SubstArg (WithHiding a) = SubstArg a
instance Subst () where
type SubstArg () = Term
applySubst :: Substitution' (SubstArg ()) -> () -> ()
applySubst Substitution' (SubstArg ())
_ ()
_ = ()
instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) where
type SubstArg (a, b) = SubstArg a
{-# INLINE applySubst #-}
applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b)
applySubst Substitution' (SubstArg (a, b))
rho (a
x,b
y) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b))
rho b
y)
instance (Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) where
type SubstArg (a, b, c) = SubstArg a
applySubst :: Substitution' (SubstArg (a, b, c)) -> (a, b, c) -> (a, b, c)
applySubst Substitution' (SubstArg (a, b, c))
rho (a
x,b
y,c
z) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b, c))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b, c))
rho b
y, Substitution' (SubstArg c) -> c -> c
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg c)
Substitution' (SubstArg (a, b, c))
rho c
z)
instance
( Subst a, Subst b, Subst c, Subst d
, SubstArg a ~ SubstArg b
, SubstArg b ~ SubstArg c
, SubstArg c ~ SubstArg d
) => Subst (a, b, c, d) where
type SubstArg (a, b, c, d) = SubstArg a
applySubst :: Substitution' (SubstArg (a, b, c, d))
-> (a, b, c, d) -> (a, b, c, d)
applySubst Substitution' (SubstArg (a, b, c, d))
rho (a
x,b
y,c
z,d
u) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b, c, d))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b, c, d))
rho b
y, Substitution' (SubstArg c) -> c -> c
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg c)
Substitution' (SubstArg (a, b, c, d))
rho c
z, Substitution' (SubstArg d) -> d -> d
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg d)
Substitution' (SubstArg (a, b, c, d))
rho d
u)
instance Subst Candidate where
type SubstArg Candidate = Term
applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate
applySubst Substitution' (SubstArg Candidate)
rho (Candidate CandidateKind
q Term
u Type
t OverlapMode
ov) = CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
q (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg Candidate)
rho Term
u) (Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg Candidate)
rho Type
t) OverlapMode
ov
instance Subst EqualityView where
type SubstArg EqualityView = Term
applySubst :: Substitution' (SubstArg EqualityView)
-> EqualityView -> EqualityView
applySubst Substitution' (SubstArg EqualityView)
rho = \case
OtherType Type
t -> Type -> EqualityView
OtherType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityView)
Substitution' (SubstArg Type)
rho Type
t
IdiomType Type
t -> Type -> EqualityView
IdiomType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityView)
Substitution' (SubstArg Type)
rho Type
t
EqualityViewType EqualityTypeData
eqt -> EqualityTypeData -> EqualityView
EqualityViewType (EqualityTypeData -> EqualityView)
-> EqualityTypeData -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityTypeData)
Substitution' (SubstArg EqualityView)
rho EqualityTypeData
eqt
instance Subst EqualityTypeData where
type SubstArg EqualityTypeData = Term
applySubst :: Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
applySubst Substitution' (SubstArg EqualityTypeData)
rho (EqualityTypeData Range
r Sort' Term
s QName
eq [Arg Term]
l Arg Term
t Arg Term
a Arg Term
b) = Range
-> Sort' Term
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityTypeData
EqualityTypeData Range
r
(Substitution' (SubstArg (Sort' Term)) -> Sort' Term -> Sort' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityTypeData)
Substitution' (SubstArg (Sort' Term))
rho Sort' Term
s)
QName
eq
((Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho) [Arg Term]
l)
(Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
t)
(Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
a)
(Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
b)
instance DeBruijn a => DeBruijn (Pattern' a) where
deBruijnNamedVar :: [Char] -> Int -> Pattern' a
deBruijnNamedVar [Char]
n Int
i = a -> Pattern' a
forall a. a -> Pattern' a
varP (a -> Pattern' a) -> a -> Pattern' a
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> a
forall a. DeBruijn a => [Char] -> Int -> a
deBruijnNamedVar [Char]
n Int
i
deBruijnView :: Pattern' a -> Maybe Int
deBruijnView Pattern' a
_ = Maybe Int
forall a. Maybe a
Nothing
fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution :: PatternSubstitution -> Substitution' Term
fromPatternSubstitution = (DeBruijnPattern -> Term)
-> PatternSubstitution -> Substitution' Term
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm
applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
applyPatSubst :: forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst = Substitution' Term -> a -> a
Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' Term -> a -> a)
-> (PatternSubstitution -> Substitution' Term)
-> PatternSubstitution
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternSubstitution -> Substitution' Term
fromPatternSubstitution
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin :: forall a. PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin PatOrigin
o Pattern' a
p = case Pattern' a -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo Pattern' a
p of
Maybe PatternInfo
Nothing -> Pattern' a
p
Just PatternInfo
i -> PatternInfo -> Pattern' a -> Pattern' a
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo (PatternInfo
i { patOrigin = o }) Pattern' a
p
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo :: forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i Pattern' a
p = case Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p of
Maybe PatOrigin
Nothing -> Pattern' a
p
Just PatOrigin
PatOSplit -> Pattern' a
p
Just PatOrigin
PatOAbsurd -> Pattern' a
p
Just PatOrigin
_ -> case Pattern' a
p of
(VarP PatternInfo
_ a
x) -> PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
i a
x
(DotP PatternInfo
_ Term
u) -> PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i Term
u
(ConP ConHead
c (ConPatternInfo PatternInfo
_ Bool
r Bool
ft Maybe (Arg Type)
b Bool
l) [NamedArg (Pattern' a)]
ps)
-> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
i Bool
r Bool
ft Maybe (Arg Type)
b Bool
l) [NamedArg (Pattern' a)]
ps
DefP PatternInfo
_ QName
q [NamedArg (Pattern' a)]
ps -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q [NamedArg (Pattern' a)]
ps
(LitP PatternInfo
_ Literal
l) -> PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
i Literal
l
ProjP{} -> Pattern' a
forall a. HasCallStack => a
__IMPOSSIBLE__
(IApplyP PatternInfo
_ Term
t Term
u a
x) -> PatternInfo -> Term -> Term -> a -> Pattern' a
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i Term
t Term
u a
x
instance Subst DeBruijnPattern where
type SubstArg DeBruijnPattern = DeBruijnPattern
applySubst :: Substitution' (SubstArg DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
applySubst Substitution' (SubstArg DeBruijnPattern)
IdS = DeBruijnPattern -> DeBruijnPattern
forall a. a -> a
id
applySubst Substitution' (SubstArg DeBruijnPattern)
rho = \case
VarP PatternInfo
i DBPatVar
x ->
PatternInfo -> DeBruijnPattern -> DeBruijnPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
[Char] -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> [Char]
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
PatternSubstitution -> Int -> DeBruijnPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
DotP PatternInfo
i Term
u -> PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i (Term -> DeBruijnPattern) -> Term -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u
ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
ps -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci {conPType = applyPatSubst rho (conPType ci)} ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
Substitution' (SubstArg DeBruijnPattern)
rho [NamedArg DeBruijnPattern]
ps
DefP PatternInfo
i QName
q [NamedArg DeBruijnPattern]
ps -> PatternInfo
-> QName -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
Substitution' (SubstArg DeBruijnPattern)
rho [NamedArg DeBruijnPattern]
ps
p :: DeBruijnPattern
p@(LitP PatternInfo
_ Literal
_) -> DeBruijnPattern
p
p :: DeBruijnPattern
p@ProjP{} -> DeBruijnPattern
p
IApplyP PatternInfo
i Term
t Term
u DBPatVar
x ->
case [Char] -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> [Char]
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Int -> DeBruijnPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x of
IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
t) (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u) DBPatVar
y
VarP PatternInfo
_ DBPatVar
y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
t) (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u) DBPatVar
y
DeBruijnPattern
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
where
useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
useName :: [Char] -> DeBruijnPattern -> DeBruijnPattern
useName [Char]
n (VarP PatternInfo
o DBPatVar
x)
| [Char] -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (DBPatVar -> [Char]
dbPatVarName DBPatVar
x)
= PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar
x { dbPatVarName = n }
useName [Char]
_ DeBruijnPattern
x = DeBruijnPattern
x
instance Subst Range where
type SubstArg Range = Term
applySubst :: Substitution' (SubstArg Range) -> Range -> Range
applySubst Substitution' (SubstArg Range)
_ = Range -> Range
forall a. a -> a
id
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> [Arg Term] -> Term
projDropParsApply (Projection Maybe QName
prop QName
d Arg QName
r Int
_ ProjLams
lams) ProjOrigin
o Relevance
rel [Arg Term]
args =
case [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
forall a. [a] -> Maybe ([a], a)
initLast ([Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char]))
-> [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
forall a b. (a -> b) -> a -> b
$ ProjLams -> [Arg [Char]]
getProjLams ProjLams
lams of
Maybe ([Arg [Char]], Arg [Char])
Nothing -> if Bool
proper then QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args else Term
forall a. HasCallStack => a
__IMPOSSIBLE__
Just ([Arg [Char]]
pars, Arg ArgInfo
i [Char]
y) ->
let irr :: Bool
irr = Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel
core :: Term
core
| Bool
proper Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
irr = ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
y (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
d]
| Bool
otherwise = ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
y (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [] Term -> Arg QName -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg QName
r]
([Arg [Char]]
pars', [Arg Term]
args') = [Arg [Char]] -> [Arg Term] -> ([Arg [Char]], [Arg Term])
forall a b. [a] -> [b] -> ([a], [b])
dropCommon [Arg [Char]]
pars [Arg Term]
args
in (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr (\ (Arg ArgInfo
ai [Char]
x) -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x) (Term
core Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args') [Arg [Char]]
pars'
where proper :: Bool
proper = Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust Maybe QName
prop
type TelView = TelV Type
data TelV a = TelV { forall a. TelV a -> Tele (Dom a)
theTel :: Tele (Dom a), forall a. TelV a -> a
theCore :: a }
deriving (Int -> TelV a -> [Char] -> [Char]
[TelV a] -> [Char] -> [Char]
TelV a -> [Char]
(Int -> TelV a -> [Char] -> [Char])
-> (TelV a -> [Char])
-> ([TelV a] -> [Char] -> [Char])
-> Show (TelV a)
forall a. Show a => Int -> TelV a -> [Char] -> [Char]
forall a. Show a => [TelV a] -> [Char] -> [Char]
forall a. Show a => TelV a -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => Int -> TelV a -> [Char] -> [Char]
showsPrec :: Int -> TelV a -> [Char] -> [Char]
$cshow :: forall a. Show a => TelV a -> [Char]
show :: TelV a -> [Char]
$cshowList :: forall a. Show a => [TelV a] -> [Char] -> [Char]
showList :: [TelV a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> TelV a -> TelV b)
-> (forall a b. a -> TelV b -> TelV a) -> Functor TelV
forall a b. a -> TelV b -> TelV a
forall a b. (a -> b) -> TelV a -> TelV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
fmap :: forall a b. (a -> b) -> TelV a -> TelV b
$c<$ :: forall a b. a -> TelV b -> TelV a
<$ :: forall a b. a -> TelV b -> TelV a
Functor)
deriving instance (TermSubst a, Eq a) => Eq (TelV a)
deriving instance (TermSubst a, Ord a) => Ord (TelV a)
telView' :: Type -> TelView
telView' :: Type -> TelView
telView' = Int -> Type -> TelView
telView'UpTo (-Int
1)
telView'UpTo :: Int -> Type -> TelView
telView'UpTo :: Int -> Type -> TelView
telView'UpTo Int
0 Type
t = Tele (Dom Type) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t
telView'UpTo Int
n Type
t = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom Type
a Abs Type
b -> Dom Type -> [Char] -> TelView -> TelView
forall a. Dom a -> [Char] -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> [Char]
forall a. Abs a -> [Char]
absName Abs Type
b) (TelView -> TelView) -> TelView -> TelView
forall a b. (a -> b) -> a -> b
$ Int -> Type -> TelView
telView'UpTo (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
Term
_ -> Tele (Dom Type) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t
absV :: Dom a -> ArgName -> TelV a -> TelV a
absV :: forall a. Dom a -> [Char] -> TelV a -> TelV a
absV Dom a
a [Char]
x (TelV Tele (Dom a)
tel a
t) = Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a ([Char] -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. [Char] -> a -> Abs a
Abs [Char]
x Tele (Dom a)
tel)) a
t
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' :: forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f [] Dom Type
t = []
bindsToTel' Name -> a
f (Name
x:[Name]
xs) Dom Type
t = let !rest :: [Dom (a, Type)]
rest = (Name -> a) -> [Name] -> Dom Type -> [Dom (a, Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f [Name]
xs (Int -> Dom Type -> Dom Type
forall a. Subst a => Int -> a -> a
raise Int
1 Dom Type
t) in (Type -> (a, Type)) -> Dom Type -> Dom (a, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> a
f Name
x,) Dom Type
t Dom (a, Type) -> [Dom (a, Type)] -> [Dom (a, Type)]
forall a. a -> [a] -> [a]
: [Dom (a, Type)]
rest
bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel :: [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
bindsToTel = (Name -> [Char])
-> [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> [Char]
nameToArgName
bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 :: forall a. (Name -> a) -> NonEmpty Name -> Dom Type -> ListTel' a
bindsToTel'1 Name -> a
f = (Name -> a) -> [Name] -> Dom Type -> ListTel' a
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f ([Name] -> Dom Type -> ListTel' a)
-> (NonEmpty Name -> [Name])
-> NonEmpty Name
-> Dom Type
-> ListTel' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Name -> [Item (NonEmpty Name)]
NonEmpty Name -> [Name]
forall l. IsList l => l -> [Item l]
List1.toList
bindsToTel1 :: List1 Name -> Dom Type -> ListTel
bindsToTel1 :: NonEmpty Name -> Dom Type -> [Dom' Term ([Char], Type)]
bindsToTel1 = [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
bindsToTel ([Name] -> Dom Type -> [Dom' Term ([Char], Type)])
-> (NonEmpty Name -> [Name])
-> NonEmpty Name
-> Dom Type
-> [Dom' Term ([Char], Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Name -> [Item (NonEmpty Name)]
NonEmpty Name -> [Name]
forall l. IsList l => l -> [Item l]
List1.toList
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel :: [NamedArg Name] -> Type -> Tele (Dom Type)
namedBindsToTel [] Type
t = Tele (Dom Type)
forall a. Tele a
EmptyTel
namedBindsToTel (NamedArg Name
x : [NamedArg Name]
xs) Type
t =
let !rest :: Tele (Dom Type)
rest = [NamedArg Name] -> Type -> Tele (Dom Type)
namedBindsToTel [NamedArg Name]
xs (Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
t) in
Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
t Type -> Dom' Term () -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x) ([Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs (Name -> [Char]
nameToArgName (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) Tele (Dom Type)
rest)
namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 :: NonEmpty (NamedArg Name) -> Type -> Tele (Dom Type)
namedBindsToTel1 = [NamedArg Name] -> Type -> Tele (Dom Type)
namedBindsToTel ([NamedArg Name] -> Type -> Tele (Dom Type))
-> (NonEmpty (NamedArg Name) -> [NamedArg Name])
-> NonEmpty (NamedArg Name)
-> Type
-> Tele (Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (NamedArg Name) -> [Item (NonEmpty (NamedArg Name))]
NonEmpty (NamedArg Name) -> [NamedArg Name]
forall l. IsList l => l -> [Item l]
List1.toList
domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x = () () -> Dom' Term Name -> Dom' Term ()
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term Name
forall a. NamedArg a -> Dom a
domFromNamedArg ((Named NamedName Name -> Named NamedName Name)
-> NamedArg Name -> NamedArg Name
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Name -> Named NamedName Name
forceName NamedArg Name
x)
where
forceName :: Named NamedName Name -> Named NamedName Name
forceName (Named Maybe NamedName
Nothing Name
x) = Maybe NamedName -> Name -> Named NamedName Name
forall name a. Maybe name -> a -> Named name a
Named (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged [Char] -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged [Char] -> NamedName) -> Ranged [Char] -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> [Char] -> Ranged [Char]
forall a. Range -> a -> Ranged a
Ranged (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) ([Char] -> Ranged [Char]) -> [Char] -> Ranged [Char]
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
nameToArgName Name
x) Name
x
forceName Named NamedName Name
x = Named NamedName Name
x
domNameFromNamedArgName :: NamedArg Name -> Dom Name
domNameFromNamedArgName :: NamedArg Name -> Dom' Term Name
domNameFromNamedArgName NamedArg Name
x = NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x Name -> Dom' Term () -> Dom' Term Name
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x
mkPiSort :: Dom Type -> Abs Type -> Sort
mkPiSort :: Dom Type -> Abs Type -> Sort' Term
mkPiSort Dom Type
a Abs Type
b = Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort (Type -> Sort' Term) -> Type -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort (Type -> Sort' Term) -> Abs Type -> Abs (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi :: Dom' Term ([Char], Type) -> Type -> Type
mkPi !Dom' Term ([Char], Type)
dom Type
b = Term -> Type
el (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a ([Char] -> Type -> Abs Type
forall a. (Subst a, Free a) => [Char] -> a -> Abs a
mkAbs [Char]
x Type
b)
where
x :: [Char]
x = ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
forall a b. (a -> b) -> a -> b
$ Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom Dom' Term ([Char], Type)
dom
a :: Dom Type
a = ([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term ([Char], Type)
dom
el :: Term -> Type
el = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> Sort' Term -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Sort' Term
mkPiSort Dom Type
a ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
Abs [Char]
x Type
b)
mkLam :: Arg ArgName -> Term -> Term
mkLam :: Arg [Char] -> Term -> Term
mkLam Arg [Char]
a Term
v = ArgInfo -> Abs Term -> Term
Lam (Arg [Char] -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg [Char]
a) ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs (Arg [Char] -> [Char]
forall e. Arg e -> e
unArg Arg [Char]
a) Term
v)
lamView :: Term -> ([Arg ArgName], Term)
lamView :: Term -> ([Arg [Char]], Term)
lamView (Lam ArgInfo
h (Abs [Char]
x Term
b)) = ([Arg [Char]] -> [Arg [Char]])
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> [Char] -> Arg [Char]
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
forall a. a -> [a] -> [a]
:) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
lamView Term
b
lamView (Lam ArgInfo
h (NoAbs [Char]
x Term
b)) = ([Arg [Char]] -> [Arg [Char]])
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> [Char] -> Arg [Char]
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
forall a. a -> [a] -> [a]
:) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
lamView (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
b)
lamView Term
t = ([], Term
t)
unlamView :: [Arg ArgName] -> Term -> Term
unlamView :: [Arg [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs Term
b = (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
mkLam Term
b [Arg [Char]]
xs
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' :: (Abs Type -> Abs Type) -> Tele (Dom Type) -> Type -> Type
telePi' Abs Type -> Abs Type
reAbs = Tele (Dom Type) -> Type -> Type
telePi where
telePi :: Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
EmptyTel Type
t = Type
t
telePi (ExtendTel Dom Type
u Abs (Tele (Dom Type))
tel) Type
t = Term -> Type
el (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
u (Abs Type -> Term) -> Abs Type -> Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Abs Type
reAbs Abs Type
b
where
b :: Abs Type
b = (Tele (Dom Type) -> Type -> Type
`telePi` Type
t) (Tele (Dom Type) -> Type) -> Abs (Tele (Dom Type)) -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom Type))
tel
el :: Term -> Type
el = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> Sort' Term -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Sort' Term
mkPiSort Dom Type
u Abs Type
b
telePi :: Telescope -> Type -> Type
telePi :: Tele (Dom Type) -> Type -> Type
telePi = (Abs Type -> Abs Type) -> Tele (Dom Type) -> Type -> Type
telePi' Abs Type -> Abs Type
forall a. (Subst a, Free a) => Abs a -> Abs a
reAbs
telePi_ :: Telescope -> Type -> Type
telePi_ :: Tele (Dom Type) -> Type -> Type
telePi_ = (Abs Type -> Abs Type) -> Tele (Dom Type) -> Type -> Type
telePi' Abs Type -> Abs Type
forall a. a -> a
id
telePiVisible :: Telescope -> Type -> Type
telePiVisible :: Tele (Dom Type) -> Type -> Type
telePiVisible Tele (Dom Type)
EmptyTel Type
t = Type
t
telePiVisible (ExtendTel Dom Type
u Abs (Tele (Dom Type))
tel) Type
t
| Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Dom Type
u, NoAbs [Char]
x Type
t' <- Abs Type
b' = Type
t'
| Bool
otherwise = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort' Term
mkPiSort Dom Type
u Abs Type
b) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
u Abs Type
b
where
b :: Abs Type
b = Abs (Tele (Dom Type))
tel Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> Type) -> Abs Type
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tele (Dom Type) -> Type -> Type
`telePiVisible` Type
t)
b' :: Abs Type
b' = Abs Type -> Abs Type
forall a. (Subst a, Free a) => Abs a -> Abs a
reAbs Abs Type
b
teleLam :: Telescope -> Term -> Term
teleLam :: Tele (Dom Type) -> Term -> Term
teleLam Tele (Dom Type)
EmptyTel Term
t = Term
t
teleLam (ExtendTel Dom Type
u Abs (Tele (Dom Type))
tel) Term
t = ArgInfo -> Abs Term -> Term
Lam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
u) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ (Tele (Dom Type) -> Term -> Term)
-> Term -> Tele (Dom Type) -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Tele (Dom Type) -> Term -> Term
teleLam Term
t (Tele (Dom Type) -> Term) -> Abs (Tele (Dom Type)) -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom Type))
tel
class TeleNoAbs a where
teleNoAbs :: a -> Term -> Term
instance TeleNoAbs ListTel where
teleNoAbs :: [Dom' Term ([Char], Type)] -> Term -> Term
teleNoAbs [Dom' Term ([Char], Type)]
tel Term
t = (Dom' Term ([Char], Type) -> Term -> Term)
-> Term -> [Dom' Term ([Char], Type)] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Dom' Term ([Char], Type)
d -> ArgInfo -> Abs Term -> Term
Lam (Dom' Term ([Char], Type)
d Dom' Term ([Char], Type)
-> Getting ArgInfo (Dom' Term ([Char], Type)) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term ([Char], Type)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom Dom' Term ([Char], Type)
d))) Term
t [Dom' Term ([Char], Type)]
tel
instance TeleNoAbs Telescope where
teleNoAbs :: Tele (Dom Type) -> Term -> Term
teleNoAbs Tele (Dom Type)
tel = [Dom' Term ([Char], Type)] -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs ([Dom' Term ([Char], Type)] -> Term -> Term)
-> [Dom' Term ([Char], Type)] -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel :: Tele (Dom Type) -> [Term] -> Maybe [Dom Type]
typeArgsWithTel Tele (Dom Type)
_ [] = [Dom Type] -> Maybe [Dom Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeArgsWithTel (ExtendTel Dom Type
dom Abs (Tele (Dom Type))
tel) (Term
v : [Term]
vs) = (Dom Type
dom Dom Type -> [Dom Type] -> [Dom Type]
forall a. a -> [a] -> [a]
:) ([Dom Type] -> [Dom Type]) -> Maybe [Dom Type] -> Maybe [Dom Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type) -> [Term] -> Maybe [Dom Type]
typeArgsWithTel (Abs (Tele (Dom Type))
-> SubstArg (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Tele (Dom Type))
tel Term
SubstArg (Tele (Dom Type))
v) [Term]
vs
typeArgsWithTel EmptyTel{} (Term
_:[Term]
_) = Maybe [Dom Type]
forall a. Maybe a
Nothing
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody Clause
cl = Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Permutation -> Substitution' Term
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR Permutation
perm) (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl
where perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
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 CandidateKind
deriving instance Eq Candidate
deriving instance Ord CandidateKind
deriving instance Ord Candidate
deriving instance (Subst a, Eq a) => Eq (Tele a)
deriving instance (Subst a, Ord a) => Ord (Tele a)
deriving instance Eq Section
instance Ord PlusLevel where
compare :: PlusLevel' Term -> PlusLevel' Term -> Ordering
compare (Plus Integer
n Term
a) (Plus Integer
m Term
b) = (Term, Integer) -> (Term, Integer) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term
a,Integer
n) (Term
b,Integer
m)
instance Eq a => Eq (Type' a) where
== :: Type' a -> Type' a -> Bool
(==) = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool) -> (Type' a -> a) -> Type' a -> Type' a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Type' a -> a
forall t a. Type'' t a -> a
unEl
instance Ord a => Ord (Type' a) where
compare :: Type' a -> Type' a -> Ordering
compare = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering)
-> (Type' a -> a) -> Type' a -> Type' a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Type' a -> a
forall t a. Type'' t a -> a
unEl
instance Eq Term where
Var Int
x Elims
vs == :: Term -> Term -> Bool
== Var Int
x' Elims
vs' = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
Lam ArgInfo
h Abs Term
v == Lam ArgInfo
h' Abs Term
v' = ArgInfo
h ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
h' Bool -> Bool -> Bool
&& Abs Term
v Abs Term -> Abs Term -> Bool
forall a. Eq a => a -> a -> Bool
== Abs Term
v'
Lit Literal
l == Lit Literal
l' = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
Def QName
x Elims
vs == Def QName
x' Elims
vs' = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
Con ConHead
x ConInfo
_ Elims
vs == Con ConHead
x' ConInfo
_ Elims
vs' = ConHead
x ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
Pi Dom Type
a Abs Type
b == Pi Dom Type
a' Abs Type
b' = Dom Type
a Dom Type -> Dom Type -> Bool
forall a. Eq a => a -> a -> Bool
== Dom Type
a' Bool -> Bool -> Bool
&& Abs Type
b Abs Type -> Abs Type -> Bool
forall a. Eq a => a -> a -> Bool
== Abs Type
b'
Sort Sort' Term
s == Sort Sort' Term
s' = Sort' Term
s Sort' Term -> Sort' Term -> Bool
forall a. Eq a => a -> a -> Bool
== Sort' Term
s'
Level Level
l == Level Level
l' = Level
l Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
l'
MetaV MetaId
m Elims
vs == MetaV MetaId
m' Elims
vs' = MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
DontCare Term
_ == DontCare Term
_ = Bool
True
Dummy{} == Dummy{} = Bool
True
Term
_ == Term
_ = Bool
False
instance Eq a => Eq (Pattern' a) where
VarP PatternInfo
_ a
x == :: Pattern' a -> Pattern' a -> Bool
== VarP PatternInfo
_ a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
DotP PatternInfo
_ Term
u == DotP PatternInfo
_ Term
v = Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v
ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
ps == ConP ConHead
c' ConPatternInfo
_ [NamedArg (Pattern' a)]
qs = ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c Bool -> Bool -> Bool
&& [NamedArg (Pattern' a)]
ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg (Pattern' a)]
qs
LitP PatternInfo
_ Literal
l == LitP PatternInfo
_ Literal
l' = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
ProjP ProjOrigin
_ QName
f == ProjP ProjOrigin
_ QName
g = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g
IApplyP PatternInfo
_ Term
u Term
v a
x == IApplyP PatternInfo
_ Term
u' Term
v' a
y = Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
u' Bool -> Bool -> Bool
&& Term
v Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v' Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
DefP PatternInfo
_ QName
f [NamedArg (Pattern' a)]
ps == DefP PatternInfo
_ QName
g [NamedArg (Pattern' a)]
qs = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g Bool -> Bool -> Bool
&& [NamedArg (Pattern' a)]
ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg (Pattern' a)]
qs
Pattern' a
_ == Pattern' a
_ = Bool
False
instance Ord Term where
Var Int
a Elims
b compare :: Term -> Term -> Ordering
`compare` Var Int
x Elims
y = (Int, Elims) -> (Int, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int
x, Elims
b) (Int
a, Elims
y)
Var{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Var{} = Ordering
GT
Def QName
a Elims
b `compare` Def QName
x Elims
y = (QName, Elims) -> (QName, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (QName
a, Elims
b) (QName
x, Elims
y)
Def{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Def{} = Ordering
GT
Con ConHead
a ConInfo
_ Elims
b `compare` Con ConHead
x ConInfo
_ Elims
y = (ConHead, Elims) -> (ConHead, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ConHead
a, Elims
b) (ConHead
x, Elims
y)
Con{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Con{} = Ordering
GT
Lit Literal
a `compare` Lit Literal
x = Literal -> Literal -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Literal
a Literal
x
Lit{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Lit{} = Ordering
GT
Lam ArgInfo
a Abs Term
b `compare` Lam ArgInfo
x Abs Term
y = (ArgInfo, Abs Term) -> (ArgInfo, Abs Term) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ArgInfo
a, Abs Term
b) (ArgInfo
x, Abs Term
y)
Lam{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Lam{} = Ordering
GT
Pi Dom Type
a Abs Type
b `compare` Pi Dom Type
x Abs Type
y = (Dom Type, Abs Type) -> (Dom Type, Abs Type) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Dom Type
a, Abs Type
b) (Dom Type
x, Abs Type
y)
Pi{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Pi{} = Ordering
GT
Sort Sort' Term
a `compare` Sort Sort' Term
x = Sort' Term -> Sort' Term -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Sort' Term
a Sort' Term
x
Sort{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Sort{} = Ordering
GT
Level Level
a `compare` Level Level
x = Level -> Level -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Level
a Level
x
Level{} `compare` Term
_ = Ordering
LT
Term
_ `compare` Level{} = Ordering
GT
MetaV MetaId
a Elims
b `compare` MetaV MetaId
x Elims
y = (MetaId, Elims) -> (MetaId, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MetaId
a, Elims
b) (MetaId
x, Elims
y)
MetaV{} `compare` Term
_ = Ordering
LT
Term
_ `compare` MetaV{} = Ordering
GT
DontCare{} `compare` DontCare{} = Ordering
EQ
DontCare{} `compare` Term
_ = Ordering
LT
Term
_ `compare` DontCare{} = Ordering
GT
Dummy{} `compare` Dummy{} = Ordering
EQ
instance (Subst a, Eq a) => Eq (Abs a) where
NoAbs [Char]
_ a
a == :: Abs a -> Abs a -> Bool
== NoAbs [Char]
_ a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
Abs a
a == Abs a
b = Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
b
instance (Subst a, Ord a) => Ord (Abs a) where
NoAbs [Char]
_ a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs [Char]
_ a
b = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
Abs a
a `compare` Abs a
b = Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
b
deriving instance Ord a => Ord (Dom a)
instance (Eq a) => Eq (Elim' a) where
Apply Arg a
a == :: Elim' a -> Elim' a -> Bool
== Apply Arg a
b = Arg a
a Arg a -> Arg a -> Bool
forall a. Eq a => a -> a -> Bool
== Arg a
b
Proj ProjOrigin
_ QName
x == Proj ProjOrigin
_ QName
y = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
IApply a
x a
y a
r == IApply a
x' a
y' a
r' = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' Bool -> Bool -> Bool
&& a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y' Bool -> Bool -> Bool
&& a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
r'
Elim' a
_ == Elim' a
_ = Bool
False
instance (Ord a) => Ord (Elim' a) where
Apply Arg a
a compare :: Elim' a -> Elim' a -> Ordering
`compare` Apply Arg a
b = Arg a
a Arg a -> Arg a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Arg a
b
Proj ProjOrigin
_ QName
x `compare` Proj ProjOrigin
_ QName
y = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
IApply a
x a
y a
r `compare` IApply a
x' a
y' a
r' = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
x' Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
y a
y' Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
r a
r'
Apply{} `compare` Elim' a
_ = Ordering
LT
Elim' a
_ `compare` Apply{} = Ordering
GT
Proj{} `compare` Elim' a
_ = Ordering
LT
Elim' a
_ `compare` Proj{} = Ordering
GT
deriving instance Eq DefSing
deriving instance Eq NLPat
deriving instance Eq NLPType
deriving instance Eq NLPSort
deriving instance Eq LocalEquation
deriving instance Eq RewriteRule
deriving instance Eq RewDom
deriving instance Eq (DomInfo Term)
deriving instance Ord DefSing
deriving instance Ord NLPSort
deriving instance Ord NLPType
deriving instance Ord NLPat
deriving instance Ord LocalEquation
deriving instance Ord RewriteHead
deriving instance Ord RewriteRule
deriving instance Ord RewDom
deriving instance Ord (DomInfo Term)
univSort' :: Sort -> Either Blocker Sort
univSort' :: Sort' Term -> Either Blocker (Sort' Term)
univSort' (Univ Univ
u Level
l) = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ (Univ -> Univ
univUniv Univ
u) (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' (Inf Univ
u Integer
n) = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ
univUniv Univ
u) (Integer -> Sort' Term) -> Integer -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n
univSort' Sort' Term
SizeUniv = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0
univSort' Sort' Term
LockUniv = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' Sort' Term
LevelUniv = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' Sort' Term
IntervalUniv = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' (MetaS MetaId
m Elims
_) = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' FunSort{} = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' PiSort{} = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' UnivSort{} = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' DefS{} = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' DummyS{} = Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort :: Sort -> Sort
univSort :: Sort' Term -> Sort' Term
univSort Sort' Term
s = (Blocker -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort' Term -> Blocker -> Sort' Term
forall a b. a -> b -> a
const (Sort' Term -> Blocker -> Sort' Term)
-> Sort' Term -> Blocker -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort Sort' Term
s) (Either Blocker (Sort' Term) -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Either Blocker (Sort' Term)
univSort' Sort' Term
s
sort :: Sort -> Type
sort :: Sort' Term -> Type
sort Sort' Term
s = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Sort' Term
univSort Sort' Term
s) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
Sort Sort' Term
s
ssort :: Level -> Type
ssort :: Level -> Type
ssort Level
l = Sort' Term -> Type
sort (Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet Level
l)
data SizeOfSort = SizeOfSort
{ SizeOfSort -> Univ
szSortUniv :: Univ
, SizeOfSort -> Integer
szSortSize :: Integer
}
pattern SmallSort :: Univ -> SizeOfSort
pattern $mSmallSort :: forall {r}. SizeOfSort -> (Univ -> r) -> ((# #) -> r) -> r
$bSmallSort :: Univ -> SizeOfSort
SmallSort u = SizeOfSort u (-1)
pattern LargeSort :: Univ -> Integer -> SizeOfSort
pattern $mLargeSort :: forall {r}.
SizeOfSort -> (Univ -> Integer -> r) -> ((# #) -> r) -> r
$bLargeSort :: Univ -> Integer -> SizeOfSort
LargeSort u n <- ((\ x :: SizeOfSort
x@(SizeOfSort Univ
u Integer
n) -> Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) Maybe () -> SizeOfSort -> Maybe SizeOfSort
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SizeOfSort
x) -> Just (SizeOfSort u n))
where LargeSort Univ
u Integer
n = Univ -> Integer -> SizeOfSort
SizeOfSort Univ
u Integer
n
{-# COMPLETE SmallSort, LargeSort #-}
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sizeOfSort :: Sort' Term -> Either Blocker SizeOfSort
sizeOfSort = \case
Univ Univ
u Level
_ -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
u
Sort' Term
SizeUniv -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
UType
Sort' Term
LockUniv -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
UType
Sort' Term
LevelUniv -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
UType
Sort' Term
IntervalUniv -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
USSet
Inf Univ
u Integer
n -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> SizeOfSort
LargeSort Univ
u Integer
n
MetaS MetaId
m Elims
_ -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker SizeOfSort)
-> Blocker -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
FunSort{} -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
PiSort{} -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
UnivSort{} -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
DefS{} -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
DummyS{} -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
isSmallSort :: Sort -> Bool
isSmallSort :: Sort' Term -> Bool
isSmallSort Sort' Term
s = case Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
s of
Right SmallSort{} -> Bool
True
Either Blocker SizeOfSort
_ -> Bool
False
funSort' :: Bool -> Sort -> Sort -> Either Blocker Sort
funSort' :: Bool -> Sort' Term -> Sort' Term -> Either Blocker (Sort' Term)
funSort' Bool
hasLevelUniv Sort' Term
a Sort' Term
b = case (Sort' Term -> Sort' Term
normLU Sort' Term
a, Sort' Term -> Sort' Term
normLU Sort' Term
b) of
(Univ Univ
u Level
a , Univ Univ
u' Level
b ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ (Univ -> Univ -> Univ
funUniv Univ
u Univ
u') (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
(Inf Univ
ua Integer
m , Sort' Term
b ) -> Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
b Either Blocker SizeOfSort
-> (SizeOfSort -> Sort' Term) -> Either Blocker (Sort' Term)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (SizeOfSort Univ
ub Integer
n) -> Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ -> Univ
funUniv Univ
ua Univ
ub) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n)
(Sort' Term
a , Inf Univ
ub Integer
n ) -> Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
a Either Blocker SizeOfSort
-> (SizeOfSort -> Sort' Term) -> Either Blocker (Sort' Term)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (SizeOfSort Univ
ua Integer
m) -> Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ -> Univ
funUniv Univ
ua Univ
ub) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n)
(Sort' Term
LockUniv , Sort' Term
LevelUniv ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
LockUniv , Sort' Term
b ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right Sort' Term
b
(Sort' Term
a , Sort' Term
LockUniv ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
IntervalUniv , Sort' Term
IntervalUniv ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
(Sort' Term
IntervalUniv , Univ Univ
u Level
b ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u Level
b
(Sort' Term
IntervalUniv , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Univ Univ
u Level
a , Sort' Term
IntervalUniv ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level
a
(Sort' Term
_ , Sort' Term
IntervalUniv ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
SizeUniv , Sort' Term
b ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right Sort' Term
b
(Sort' Term
a , Sort' Term
SizeUniv ) -> Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
a Either Blocker SizeOfSort
-> (SizeOfSort -> Either Blocker (Sort' Term))
-> Either Blocker (Sort' Term)
forall a b.
Either Blocker a -> (a -> Either Blocker b) -> Either Blocker b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SmallSort{} -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right Sort' Term
forall t. Sort' t
SizeUniv
LargeSort{} -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
LevelUniv , Sort' Term
LevelUniv ) -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right Sort' Term
forall t. Sort' t
LevelUniv
(Sort' Term
_ , Sort' Term
LevelUniv ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
LevelUniv , Sort' Term
b ) -> Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
b Either Blocker SizeOfSort
-> (SizeOfSort -> Sort' Term) -> Either Blocker (Sort' Term)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
SmallSort Univ
ub -> Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
ub Integer
0
LargeSort{} -> Sort' Term
b
(MetaS MetaId
m Elims
_ , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left (Blocker -> Either Blocker (Sort' Term))
-> Blocker -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
(Sort' Term
_ , MetaS MetaId
m Elims
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left (Blocker -> Either Blocker (Sort' Term))
-> Blocker -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
(FunSort{} , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
_ , FunSort{} ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(PiSort{} , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
_ , PiSort{} ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(UnivSort{} , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
_ , UnivSort{} ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(DefS{} , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
_ , DefS{} ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(DummyS{} , Sort' Term
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
(Sort' Term
_ , DummyS{} ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
neverUnblock
where
normLU :: Sort' Term -> Sort' Term
normLU = Bool -> (Sort' Term -> Sort' Term) -> Sort' Term -> Sort' Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
hasLevelUniv \case
Sort' Term
LevelUniv -> Integer -> Sort' Term
mkType Integer
0
Sort' Term
s -> Sort' Term
s
funSort :: Bool -> Sort -> Sort -> Sort
funSort :: Bool -> Sort' Term -> Sort' Term -> Sort' Term
funSort Bool
hasLevelUniv Sort' Term
a Sort' Term
b = (Blocker -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort' Term -> Blocker -> Sort' Term
forall a b. a -> b -> a
const (Sort' Term -> Blocker -> Sort' Term)
-> Sort' Term -> Blocker -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
a Sort' Term
b) (Either Blocker (Sort' Term) -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Bool -> Sort' Term -> Sort' Term -> Either Blocker (Sort' Term)
funSort' Bool
hasLevelUniv Sort' Term
a Sort' Term
b
{-# SPECIALISE funSortM' :: Sort -> Sort -> TCM (Either Blocker Sort) #-}
funSortM' :: HasOptions m => Sort -> Sort -> m (Either Blocker Sort)
funSortM' :: forall (m :: * -> *).
HasOptions m =>
Sort' Term -> Sort' Term -> m (Either Blocker (Sort' Term))
funSortM' Sort' Term
a Sort' Term
b = do
hasLevelUniv <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
return $ funSort' hasLevelUniv a b
{-# SPECIALISE funSortM :: Sort -> Sort -> TCM Sort #-}
funSortM :: HasOptions m => Sort -> Sort -> m Sort
funSortM :: forall (m :: * -> *).
HasOptions m =>
Sort' Term -> Sort' Term -> m (Sort' Term)
funSortM Sort' Term
a Sort' Term
b = do
hasLevelUniv <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
return $ funSort hasLevelUniv a b
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' :: Dom Term
-> Sort' Term -> Abs (Sort' Term) -> Either Blocker (Sort' Term)
piSort' Dom Term
a Sort' Term
s1 (NoAbs [Char]
_ Sort' Term
s2) = Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
s1 Sort' Term
s2
piSort' Dom Term
a Sort' Term
s1 s2Abs :: Abs (Sort' Term)
s2Abs@(Abs [Char]
_ Sort' Term
s2) = case Int -> Sort' Term -> Maybe FlexRig
forall a. Free a => Int -> a -> Maybe FlexRig
flexRigOccurrenceIn Int
0 Sort' Term
s2 of
Maybe FlexRig
Nothing -> Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Sort' Term -> Either Blocker (Sort' Term))
-> Sort' Term -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
s1 (Sort' Term -> Sort' Term) -> Sort' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Impossible -> Abs (Sort' Term) -> Sort' Term
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ Abs (Sort' Term)
s2Abs
Just FlexRig
o -> Dom Term
-> Sort' Term
-> Abs (Sort' Term)
-> FlexRig
-> IsCodomainNormalised
-> Either Blocker (Sort' Term)
piSortAbs Dom Term
a Sort' Term
s1 Abs (Sort' Term)
s2Abs FlexRig
o IsCodomainNormalised
CodomainNotNormalised
data IsCodomainNormalised = CodomainNormalised | CodomainNotNormalised
piSortAbs
:: Dom Term
-> Sort
-> Abs Sort
-> FlexRig
-> IsCodomainNormalised
-> Either Blocker Sort
piSortAbs :: Dom Term
-> Sort' Term
-> Abs (Sort' Term)
-> FlexRig
-> IsCodomainNormalised
-> Either Blocker (Sort' Term)
piSortAbs Dom Term
a Sort' Term
s1 NoAbs{} FlexRig
_ IsCodomainNormalised
_ = Either Blocker (Sort' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
piSortAbs Dom Term
a Sort' Term
s1 (Abs [Char]
x Sort' Term
s2) FlexRig
occ IsCodomainNormalised
norm = case (Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
s1 , Sort' Term -> Either Blocker SizeOfSort
sizeOfSort Sort' Term
s2) of
(Right (SmallSort Univ
u1) , Right (SmallSort Univ
u2)) -> case FlexRig
occ of
FlexRig
StronglyRigid -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
FlexRig
Unguarded -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
FlexRig
WeaklyRigid -> case IsCodomainNormalised
norm of
IsCodomainNormalised
CodomainNormalised -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
IsCodomainNormalised
CodomainNotNormalised -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
alwaysUnblock
Flexible MetaSet
ms -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left (Blocker -> Either Blocker (Sort' Term))
-> Blocker -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$! MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
(Right (LargeSort Univ
u1 Integer
n) , Right (SmallSort Univ
u2)) -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort' Term -> Either Blocker (Sort' Term)
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n)
(Either Blocker SizeOfSort
_ , Right LargeSort{}) -> Either Blocker (Sort' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Left Blocker
blocker , Right SizeOfSort
_ ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
blocker
(Right SizeOfSort
_ , Left Blocker
blocker ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left Blocker
blocker
(Left Blocker
blocker1 , Left Blocker
blocker2 ) -> Blocker -> Either Blocker (Sort' Term)
forall a b. a -> Either a b
Left (Blocker -> Either Blocker (Sort' Term))
-> Blocker -> Either Blocker (Sort' Term)
forall a b. (a -> b) -> a -> b
$! Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
blocker1 Blocker
blocker2
piSort :: Dom Term -> Sort -> Abs Sort -> Sort
piSort :: Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
piSort Dom Term
a Sort' Term
s1 Abs (Sort' Term)
s2 = (Blocker -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort' Term -> Blocker -> Sort' Term
forall a b. a -> b -> a
const (Sort' Term -> Blocker -> Sort' Term)
-> Sort' Term -> Blocker -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom Term
a Sort' Term
s1 Abs (Sort' Term)
s2) (Either Blocker (Sort' Term) -> Sort' Term)
-> Either Blocker (Sort' Term) -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Dom Term
-> Sort' Term -> Abs (Sort' Term) -> Either Blocker (Sort' Term)
piSort' Dom Term
a Sort' Term
s1 Abs (Sort' Term)
s2
{-# SPECIALISE piSortM :: Dom Term -> Sort -> Abs Sort -> TCM Sort #-}
piSortM :: HasOptions m => Dom Term -> Sort -> Abs Sort -> m Sort
piSortM :: forall (m :: * -> *).
HasOptions m =>
Dom Term -> Sort' Term -> Abs (Sort' Term) -> m (Sort' Term)
piSortM Dom Term
va Sort' Term
s1 Abs (Sort' Term)
s2 = case Dom Term
-> Sort' Term -> Abs (Sort' Term) -> Either Blocker (Sort' Term)
piSort' Dom Term
va Sort' Term
s1 Abs (Sort' Term)
s2 of
Left Blocker
_ -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort' Term -> m (Sort' Term)) -> Sort' Term -> m (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom Term
va Sort' Term
s1 Abs (Sort' Term)
s2
Right (FunSort Sort' Term
s1' Sort' Term
s2') -> Sort' Term -> Sort' Term -> m (Sort' Term)
forall (m :: * -> *).
HasOptions m =>
Sort' Term -> Sort' Term -> m (Sort' Term)
funSortM Sort' Term
s1' Sort' Term
s2'
Right Sort' Term
s' -> Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s'
levelMax :: Integer -> [PlusLevel] -> Level
levelMax :: Integer -> [PlusLevel' Term] -> Level
levelMax !Integer
n0 [PlusLevel' Term]
as0 = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n [PlusLevel' Term]
as
where
Max Integer
n1 [PlusLevel' Term]
as1 = Level -> Level
expandLevel (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n0 [PlusLevel' Term]
as0
as :: [PlusLevel' Term]
as = [PlusLevel' Term] -> [PlusLevel' Term]
removeSubsumed [PlusLevel' Term]
as1
greatestB :: Integer
greatestB = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [ Integer
n | Plus Integer
n Term
_ <- [PlusLevel' Term]
as ]
n :: Integer
n | Integer
n1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
greatestB = Integer
n1
| Bool
otherwise = Integer
0
lmax :: Integer -> [PlusLevel] -> [Level] -> Level
lmax :: Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax Integer
m [PlusLevel' Term]
as [] = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m [PlusLevel' Term]
as
lmax Integer
m [PlusLevel' Term]
as (Max Integer
n [PlusLevel' Term]
bs : [Level]
ls) = Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel' Term]
bs [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. [a] -> [a] -> [a]
++! [PlusLevel' Term]
as) [Level]
ls
expandLevel :: Level -> Level
expandLevel :: Level -> Level
expandLevel (Max Integer
m [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax Integer
m [] ([Level] -> Level) -> [Level] -> Level
forall a b. (a -> b) -> a -> b
$ (PlusLevel' Term -> Level) -> [PlusLevel' Term] -> [Level]
forall a b. (a -> b) -> [a] -> [b]
map'' PlusLevel' Term -> Level
expandPlus [PlusLevel' Term]
as
expandPlus :: PlusLevel -> Level
expandPlus :: PlusLevel' Term -> Level
expandPlus (Plus Integer
m Term
l) = Integer -> Level -> Level
levelPlus Integer
m (Term -> Level
expandTm Term
l)
expandTm :: Term -> Level
expandTm (Level Level
l) = Level -> Level
expandLevel Level
l
expandTm Term
l = Term -> Level
forall t. t -> Level' t
atomicLevel Term
l
removeSubsumed :: [PlusLevel' Term] -> [PlusLevel' Term]
removeSubsumed =
((Term, Integer) -> PlusLevel' Term)
-> [(Term, Integer)] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Term
a, Integer
n) -> Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n Term
a) ([(Term, Integer)] -> [PlusLevel' Term])
-> ([PlusLevel' Term] -> [(Term, Integer)])
-> [PlusLevel' Term]
-> [PlusLevel' Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Map Term Integer -> [(Term, Integer)]
forall k a. Map k a -> [(k, a)]
MapS.toAscList (Map Term Integer -> [(Term, Integer)])
-> ([PlusLevel' Term] -> Map Term Integer)
-> [PlusLevel' Term]
-> [(Term, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Integer -> Integer -> Integer)
-> [(Term, Integer)] -> Map Term Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
MapS.fromListWith Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max ([(Term, Integer)] -> Map Term Integer)
-> ([PlusLevel' Term] -> [(Term, Integer)])
-> [PlusLevel' Term]
-> Map Term Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(PlusLevel' Term -> (Term, Integer))
-> [PlusLevel' Term] -> [(Term, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Plus Integer
n Term
a) -> (Term
a, Integer
n))
levelLub :: Level -> Level -> Level
levelLub :: Level -> Level -> Level
levelLub (Max Integer
m [PlusLevel' Term]
as) (Max Integer
n [PlusLevel' Term]
bs) = Integer -> [PlusLevel' Term] -> Level
levelMax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$! [PlusLevel' Term]
as [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. [a] -> [a] -> [a]
++! [PlusLevel' Term]
bs
levelTm :: Level -> Term
levelTm :: Level -> Term
levelTm Level
l =
case Level
l of
Max Integer
0 [Plus Integer
0 Term
l] -> Term
l
Level
_ -> Level -> Term
Level Level
l