{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Substitute
( module Agda.TypeChecking.Substitute
, module Agda.TypeChecking.Substitute.Class
, module Agda.TypeChecking.Substitute.DeBruijn
, Substitution'(..), Substitution
) where
import Control.Arrow (second)
import Control.Monad (guard)
import Data.Coerce
import Data.Function
import qualified Data.List as List
import Data.Map (Map)
import Data.Maybe
import Data.HashMap.Strict (HashMap)
import Debug.Trace (trace)
import Language.Haskell.TH.Syntax (thenCmp)
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options (typeInType)
import Agda.TypeChecking.Free as Free
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence as Occ
import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Substitute.DeBruijn
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-}
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-}
applyTermE :: forall t. (Coercible Term t, Apply t, Subst t t)
=> (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE :: (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE err' :: Empty -> Term -> Elims -> Term
err' m :: t
m [] = t
m
applyTermE err' :: Empty -> Term -> Elims -> Term
err' m :: t
m es :: 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 i :: Int
i es' :: Elims
es' -> Int -> Elims -> Term
Var Int
i (Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)
Def f :: QName
f es' :: Elims
es' -> QName -> Elims -> Elims -> Term
defApp QName
f Elims
es' Elims
es
Con c :: ConHead
c ci :: ConInfo
ci args :: Elims
args -> (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
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 _ b :: Abs Term
b ->
case Elims
es of
Apply a :: Arg Term
a : es0 :: Elims
es0 -> Abs t -> t -> t
forall t a. Subst t a => Abs a -> t -> 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 -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) t -> Elims -> Term
forall x. Coercible t x => x -> Elims -> Term
`app` Elims
es0
IApply _ _ a :: Term
a : es0 :: Elims
es0 -> Abs t -> t -> t
forall t a. Subst t a => Abs a -> t -> 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 x. Coercible t x => x -> Elims -> Term
`app` Elims
es0
_ -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
MetaV x :: MetaId
x es' :: Elims
es' -> MetaId -> Elims -> Term
MetaV MetaId
x (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 _ _ -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
Sort s :: Sort
s -> Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Sort
s Sort -> Elims -> Sort
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
Dummy s :: String
s es' :: Elims
es' -> String -> Elims -> Term
Dummy String
s (Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)
DontCare mv :: Term
mv -> Term -> Term
dontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
mv Term -> Elims -> Term
forall x. Coercible t x => x -> Elims -> Term
`app` Elims
es
where
app :: Coercible t x => x -> Elims -> Term
app :: x -> Elims -> Term
app t :: x
t es :: Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ (x -> t
forall a b. Coercible a b => a -> b
coerce x
t :: t) t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
err :: Empty -> Term
err e :: 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, Subst t 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, Subst t t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE (\ _ t :: Term
t es :: Elims
es -> String -> Elims -> Term
Dummy "applyE" (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
t) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es))
canProject :: QName -> Term -> Maybe (Arg Term)
canProject :: QName -> Term -> Maybe (Arg Term)
canProject f :: QName
f v :: Term
v =
case Term
v of
(Con (ConHead _ _ fs :: [Arg QName]
fs) _ vs :: Elims
vs) -> do
(fld :: Arg QName
fld, i :: Int
i) <- (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fQName -> 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
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
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)
_ -> Maybe (Arg Term)
forall a. Maybe a
Nothing
conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp :: (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch ci :: ConInfo
ci args :: Elims
args [] = ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args
conApp fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch ci :: ConInfo
ci args :: Elims
args (a :: Elim' Term
a@Apply{} : es :: Elims
es) = (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fk ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch ci :: ConInfo
ci args :: Elims
args (a :: Elim' Term
a@IApply{} : es :: Elims
es) = (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fk ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch@(ConHead c :: QName
c _ fs :: [Arg QName]
fs) ci :: ConInfo
ci args :: Elims
args ees :: Elims
ees@(Proj o :: ProjOrigin
o f :: QName
f : es :: Elims
es) =
let failure :: c -> c
failure err :: c
err = (String -> c -> c) -> c -> String -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> c -> c
forall a. String -> a -> a
trace c
err (String -> c) -> String -> c
forall a b. (a -> b) -> a -> b
$
"conApp: constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c String -> String -> String
forall a. [a] -> [a] -> [a]
++
" with fields\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Arg QName -> String) -> [Arg QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((" " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Arg QName -> String) -> Arg QName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> String
forall a. Show a => a -> String
show) [Arg QName]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++
" and args\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Elim' Term -> String) -> Elims -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((" " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (Elim' Term -> String) -> Elim' Term -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> String
forall a. Pretty a => a -> String
prettyShow) Elims
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++
" projected by " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
f
isApply :: Elim' a -> Arg a
isApply e :: Elim' a
e = Arg a -> Maybe (Arg a) -> Arg a
forall a. a -> Maybe a -> a
fromMaybe (Arg a -> Arg a
forall c. c -> c
failure Arg a
forall a. HasCallStack => a
__IMPOSSIBLE__) (Maybe (Arg a) -> Arg a) -> Maybe (Arg a) -> Arg a
forall a b. (a -> b) -> a -> b
$ Elim' a -> Maybe (Arg a)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
e
stuck :: Empty -> Term
stuck err :: Empty
err = Empty -> Term -> Elims -> Term
fk Empty
err (ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args) [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]
app :: Term -> Elims -> Term
app :: Term -> Elims -> Term
app v :: Term
v es :: Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ 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
in
case (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fQName -> 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 of
Nothing -> Term -> Term
forall c. c -> c
failure (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Elims -> Term
`app` Elims
es
Just (fld :: Arg QName
fld, i :: Int
i) -> let
v :: Term
v = Term -> (Elim' Term -> Term) -> Maybe (Elim' Term) -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Term -> Term
forall c. c -> c
failure (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__) (Arg QName -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare Arg QName
fld (Term -> Term) -> (Elim' Term -> Term) -> Elim' Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
argToDontCare (Arg Term -> Term)
-> (Elim' Term -> Arg Term) -> Elim' Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Arg Term
forall a. Elim' a -> Arg a
isApply) (Maybe (Elim' Term) -> Term) -> Maybe (Elim' Term) -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe (Elim' Term)
forall a. [a] -> Maybe a
listToMaybe (Elims -> Maybe (Elim' Term)) -> Elims -> Maybe (Elim' Term)
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop Int
i Elims
args
in Term
v Term -> Elims -> Term
`app` Elims
es
defApp :: QName -> Elims -> Elims -> Term
defApp :: QName -> Elims -> Elims -> Term
defApp f :: QName
f [] (Apply a :: Arg Term
a : es :: Elims
es) | Just v :: 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 f :: QName
f es0 :: Elims
es0 es :: 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 ai :: ArgInfo
ai v :: Term
v) = ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai Term
v
relToDontCare :: LensRelevance a => a -> Term -> Term
relToDontCare :: a -> Term -> Term
relToDontCare ai :: a
ai v :: Term
v
| Relevance
Irrelevant <- a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance a
ai = Term -> Term
dontCare Term
v
| Bool
otherwise = Term
v
instance Apply Sort where
applyE :: Sort -> Elims -> Sort
applyE s :: Sort
s [] = Sort
s
applyE s :: Sort
s es :: Elims
es = case Sort
s of
MetaS x :: MetaId
x es' :: Elims
es' -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> Elims -> Sort
forall a b. (a -> b) -> a -> b
$ Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es
DefS d :: QName
d es' :: Elims
es' -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d (Elims -> Sort) -> Elims -> Sort
forall a b. (a -> b) -> a -> b
$ Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es
_ -> Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Subst Term a => Apply (Tele a) where
apply :: Tele a -> Args -> Tele a
apply tel :: Tele a
tel [] = Tele a
tel
apply EmptyTel _ = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
apply (ExtendTel _ tel :: Abs (Tele a)
tel) (t :: Arg Term
t : ts :: Args
ts) = Abs (Tele a) -> Term -> Tele a
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp Abs (Tele a)
tel (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) Tele a -> Args -> Tele a
forall t. Apply t => t -> Args -> t
`apply` Args
ts
applyE :: Tele a -> Elims -> Tele a
applyE t :: Tele a
t es :: Elims
es = Tele a -> Args -> Tele a
forall t. Apply t => t -> Args -> t
apply Tele a
t (Args -> Tele a) -> Args -> Tele a
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply Definition where
apply :: Definition -> Args -> Definition
apply (Defn info :: ArgInfo
info x :: QName
x t :: Type
t pol :: [Polarity]
pol occ :: [Occurrence]
occ gens :: NumGeneralizableArgs
gens gpars :: [Maybe Name]
gpars df :: [LocalDisplayForm]
df m :: MutualId
m c :: CompiledRepresentation
c inst :: Maybe QName
inst copy :: Bool
copy ma :: Set QName
ma nc :: Bool
nc inj :: Bool
inj copat :: Bool
copat blk :: Blocked_
blk d :: Defn
d) args :: Args
args =
ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Type -> Args -> Type
piApply Type
t Args
args) ([Polarity] -> Args -> [Polarity]
forall t. Apply t => t -> Args -> t
apply [Polarity]
pol Args
args) ([Occurrence] -> Args -> [Occurrence]
forall t. Apply t => t -> Args -> t
apply [Occurrence]
occ Args
args) (NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
apply NumGeneralizableArgs
gens Args
args) (Int -> [Maybe Name] -> [Maybe Name]
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Maybe Name]
gpars) [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk (Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
d Args
args)
applyE :: Definition -> Elims -> Definition
applyE t :: Definition
t es :: Elims
es = Definition -> Args -> Definition
forall t. Apply t => t -> Args -> t
apply Definition
t (Args -> Definition) -> Args -> Definition
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply RewriteRule where
apply :: RewriteRule -> Args -> RewriteRule
apply r :: RewriteRule
r args :: Args
args =
let newContext :: Telescope
newContext = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply (RewriteRule -> Telescope
rewContext RewriteRule
r) Args
args
sub :: Substitution' NLPat
sub = Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
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) -> Args -> [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) Args
args
in RewriteRule :: QName
-> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule
RewriteRule
{ rewName :: QName
rewName = RewriteRule -> QName
rewName RewriteRule
r
, rewContext :: Telescope
rewContext = Telescope
newContext
, rewHead :: QName
rewHead = RewriteRule -> QName
rewHead RewriteRule
r
, rewPats :: PElims
rewPats = Substitution' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
sub (RewriteRule -> PElims
rewPats RewriteRule
r)
, rewRHS :: Term
rewRHS = Substitution' NLPat -> Term -> Term
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Term
rewRHS RewriteRule
r)
, rewType :: Type
rewType = Substitution' NLPat -> Type -> Type
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Type
rewType RewriteRule
r)
}
applyE :: RewriteRule -> Elims -> RewriteRule
applyE t :: RewriteRule
t es :: Elims
es = RewriteRule -> Args -> RewriteRule
forall t. Apply t => t -> Args -> t
apply RewriteRule
t (Args -> RewriteRule) -> Args -> RewriteRule
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
apply :: [Occurrence] -> Args -> [Occurrence]
apply occ :: [Occurrence]
occ args :: Args
args = Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Occurrence]
occ
applyE :: [Occurrence] -> Elims -> [Occurrence]
applyE t :: [Occurrence]
t es :: Elims
es = [Occurrence] -> Args -> [Occurrence]
forall t. Apply t => t -> Args -> t
apply [Occurrence]
t (Args -> [Occurrence]) -> Args -> [Occurrence]
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [Polarity] where
apply :: [Polarity] -> Args -> [Polarity]
apply pol :: [Polarity]
pol args :: Args
args = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Polarity]
pol
applyE :: [Polarity] -> Elims -> [Polarity]
applyE t :: [Polarity]
t es :: Elims
es = [Polarity] -> Args -> [Polarity]
forall t. Apply t => t -> Args -> t
apply [Polarity]
t (Args -> [Polarity]) -> Args -> [Polarity]
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply NumGeneralizableArgs where
apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs
apply NoGeneralizableArgs args :: Args
args = NumGeneralizableArgs
NoGeneralizableArgs
apply (SomeGeneralizableArgs n :: Int
n) args :: Args
args = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args)
applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs
applyE t :: NumGeneralizableArgs
t es :: Elims
es = NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
apply NumGeneralizableArgs
t (Args -> NumGeneralizableArgs) -> Args -> NumGeneralizableArgs
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
apply ps :: [NamedArg (Pattern' a)]
ps args :: Args
args = Int -> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a x.
(Eq a, Num a) =>
a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [NamedArg (Pattern' a)]
ps
where
loop :: a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop 0 ps :: [NamedArg (Pattern' x)]
ps = [NamedArg (Pattern' x)]
ps
loop n :: a
n [] = [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
loop n :: a
n (p :: NamedArg (Pattern' x)
p : ps :: [NamedArg (Pattern' x)]
ps) =
let recurse :: [NamedArg (Pattern' x)]
recurse = a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) [NamedArg (Pattern' x)]
ps
in case NamedArg (Pattern' x) -> Pattern' x
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' x)
p of
VarP{} -> [NamedArg (Pattern' x)]
recurse
DotP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
LitP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
ConP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
DefP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP{} -> [NamedArg (Pattern' x)]
recurse
applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]
applyE t :: [NamedArg (Pattern' a)]
t es :: Elims
es = [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
forall t. Apply t => t -> Args -> t
apply [NamedArg (Pattern' a)]
t (Args -> [NamedArg (Pattern' a)])
-> Args -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply Projection where
apply :: Projection -> Args -> Projection
apply p :: Projection
p args :: Args
args = Projection
p
{ projIndex :: Int
projIndex = Projection -> Int
projIndex Projection
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
, projLams :: ProjLams
projLams = Projection -> ProjLams
projLams Projection
p ProjLams -> Args -> ProjLams
forall t. Apply t => t -> Args -> t
`apply` Args
args
}
applyE :: Projection -> Elims -> Projection
applyE t :: Projection
t es :: Elims
es = Projection -> Args -> Projection
forall t. Apply t => t -> Args -> t
apply Projection
t (Args -> Projection) -> Args -> Projection
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply ProjLams where
apply :: ProjLams -> Args -> ProjLams
apply (ProjLams lams :: [Arg String]
lams) args :: Args
args = [Arg String] -> ProjLams
ProjLams ([Arg String] -> ProjLams) -> [Arg String] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Int -> [Arg String] -> [Arg String]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Arg String]
lams
applyE :: ProjLams -> Elims -> ProjLams
applyE t :: ProjLams
t es :: Elims
es = ProjLams -> Args -> ProjLams
forall t. Apply t => t -> Args -> t
apply ProjLams
t (Args -> ProjLams) -> Args -> ProjLams
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply Defn where
apply :: Defn -> Args -> Defn
apply d :: Defn
d [] = Defn
d
apply d :: Defn
d args :: Args
args = case Defn
d of
Axiom{} -> Defn
d
DataOrRecSig n :: Int
n -> Int -> Defn
DataOrRecSig (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args)
GeneralizableVar{} -> Defn
d
AbstractDefn d :: Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
d Args
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
funInv = FunctionInverse
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
Nothing } ->
Defn
d { funClauses :: [Clause]
funClauses = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args
, funCompiled :: Maybe CompiledClauses
funCompiled = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
forall t. Apply t => t -> Args -> t
apply Maybe CompiledClauses
cc Args
args
, funCovering :: [Clause]
funCovering = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cov Args
args
, funInv :: FunctionInverse
funInv = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
inv Args
args
, funExtLam :: Maybe ExtLamInfo
funExtLam = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (System -> Args -> System
forall t. Apply t => t -> Args -> t
`apply` Args
args) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
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
funInv = FunctionInverse
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Maybe Projection
funProjection = Just p0 :: Projection
p0} ->
case Projection
p0 Projection -> Args -> Projection
forall t. Apply t => t -> Args -> t
`apply` Args
args of
p :: Projection
p@Projection{ projIndex :: Projection -> Int
projIndex = Int
n }
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 -> Defn
d { funProjection :: Maybe Projection
funProjection = Maybe Projection
forall a. HasCallStack => a
__IMPOSSIBLE__ }
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Defn
d { funProjection :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
p }
| Bool
otherwise ->
Defn
d { funClauses :: [Clause]
funClauses = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args'
, funCompiled :: Maybe CompiledClauses
funCompiled = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
forall t. Apply t => t -> Args -> t
apply Maybe CompiledClauses
cc Args
args'
, funCovering :: [Clause]
funCovering = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cov Args
args'
, funInv :: FunctionInverse
funInv = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
inv Args
args'
, funProjection :: Maybe Projection
funProjection = if Bool
isVar0 then Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
p{ projIndex :: Int
projIndex = 0 } else Maybe Projection
forall a. Maybe a
Nothing
, funExtLam :: Maybe ExtLamInfo
funExtLam = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ _ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extLam
}
where
larg :: Arg Term
larg = Args -> Arg Term
forall a. [a] -> a
last Args
args
args' :: Args
args' = [Arg Term
larg]
isVar0 :: Bool
isVar0 = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
larg of Var 0 [] -> Bool
True; _ -> Bool
False
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
Defn
d { dataPars :: Int
dataPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
, dataClause :: Maybe Clause
dataClause = Maybe Clause -> Args -> Maybe Clause
forall t. Apply t => t -> Args -> t
apply Maybe Clause
cl Args
args
}
Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Telescope
recTel = Telescope
tel
} ->
Defn
d { recPars :: Int
recPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
, recClause :: Maybe Clause
recClause = Maybe Clause -> Args -> Maybe Clause
forall t. Apply t => t -> Args -> t
apply Maybe Clause
cl Args
args, recTel :: Telescope
recTel = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
args
}
Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
Defn
d { conPars :: Int
conPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args }
Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
Defn
d { primClauses :: [Clause]
primClauses = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args }
applyE :: Defn -> Elims -> Defn
applyE t :: Defn
t es :: Elims
es = Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
t (Args -> Defn) -> Args -> Defn
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply PrimFun where
apply :: PrimFun -> Args -> PrimFun
apply (PrimFun x :: QName
x ar :: Int
ar def :: Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) args :: Args
args = QName
-> Int
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun)
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \ vs :: Args
vs -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def (Args
args Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
vs)
applyE :: PrimFun -> Elims -> PrimFun
applyE t :: PrimFun
t es :: Elims
es = PrimFun -> Args -> PrimFun
forall t. Apply t => t -> Args -> t
apply PrimFun
t (Args -> PrimFun) -> Args -> PrimFun
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply Clause where
apply :: Clause -> Args -> Clause
apply cls :: Clause
cls@(Clause rl :: Range
rl rf :: Range
rf tel :: Telescope
tel ps :: NAPs
ps b :: Maybe Term
b t :: Maybe (Arg Type)
t catchall :: Bool
catchall recursive :: Maybe Bool
recursive unreachable :: Maybe Bool
unreachable ell :: ExpandedEllipsis
ell) args :: Args
args
| Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> NAPs -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise =
Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
rl Range
rf
Telescope
tel'
(Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rhoP (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) NAPs
ps)
(Substitution' Term -> Maybe Term -> Maybe Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Maybe Term
b)
(Substitution' Term -> Maybe (Arg Type) -> Maybe (Arg Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Maybe (Arg Type)
t)
Bool
catchall
Maybe Bool
recursive
Maybe Bool
unreachable
ExpandedEllipsis
ell
where
rargs :: [Term]
rargs = (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> Args -> [Term]
forall a b. (a -> b) -> a -> b
$ Args -> Args
forall a. [a] -> [a]
reverse Args
args
rps :: NAPs
rps = NAPs -> NAPs
forall a. [a] -> [a]
reverse (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
take (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) NAPs
ps
n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
tel' :: Telescope
tel' = Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel NAPs
rps [Term]
rargs
rhoP :: PatternSubstitution
rhoP :: Substitution' DeBruijnPattern
rhoP = (Term -> DeBruijnPattern)
-> Int -> NAPs -> [Term] -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Int
n NAPs
rps [Term]
rargs
rho :: Substitution' Term
rho = (Term -> Term) -> Int -> NAPs -> [Term] -> Substitution' Term
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> Term
forall c. c -> c
id Int
n NAPs
rps [Term]
rargs
substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP :: Int -> Term -> NAPs -> NAPs
substP i :: Int
i v :: Term
v = Int -> DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Int -> t -> a -> a
subst Int
i (Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
v)
mkSub :: Subst a a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub :: (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub _ _ [] [] = Substitution' a
forall a. Substitution' a
idS
mkSub tm :: Term -> a
tm n :: Int
n (p :: NamedArg DeBruijnPattern
p : ps :: NAPs
ps) (v :: Term
v : vs :: [Term]
vs) =
case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
VarP _ (DBPatVar _ i :: Int
i) -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Int -> Term -> NAPs -> NAPs
substP Int
i Term
v' NAPs
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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 t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Term
v
DotP{} -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n NAPs
ps [Term]
vs
ConP c :: ConHead
c _ ps' :: NAPs
ps' -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs)
DefP o :: PatternInfo
o q :: QName
q ps' :: NAPs
ps' -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) [Term]
vs
LitP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP _ _ _ (DBPatVar _ i :: Int
i) -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Int -> Term -> NAPs -> NAPs
substP Int
i Term
v' NAPs
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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 t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Term
v
mkSub _ _ _ _ = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel :: Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel n :: Int
n tel :: Telescope
tel [] [] = Telescope
tel
newTel n :: Int
n tel :: Telescope
tel (p :: NamedArg DeBruijnPattern
p : ps :: NAPs
ps) (v :: Term
v : vs :: [Term]
vs) =
case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
VarP _ (DBPatVar _ i :: Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Int -> Term -> Telescope -> Telescope
forall t t a t.
(Eq t, Num t, Subst t a, Subst t t) =>
t -> t -> Tele a -> Tele a
subTel (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
v Telescope
tel) (Int -> Term -> NAPs -> NAPs
substP Int
i (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Term
v) NAPs
ps) [Term]
vs
DotP{} -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel NAPs
ps [Term]
vs
ConP c :: ConHead
c _ ps' :: NAPs
ps' -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs)
DefP _ q :: QName
q ps' :: NAPs
ps' -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) [Term]
vs
LitP{} -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP _ _ _ (DBPatVar _ i :: Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Int -> Term -> Telescope -> Telescope
forall t t a t.
(Eq t, Num t, Subst t a, Subst t t) =>
t -> t -> Tele a -> Tele a
subTel (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
v Telescope
tel) (Int -> Term -> NAPs -> NAPs
substP Int
i (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Term
v) NAPs
ps) [Term]
vs
newTel _ tel :: Telescope
tel _ _ = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
projections :: ConHead -> Term -> [Term]
projections c :: ConHead
c v :: 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
$ 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 ai :: ArgInfo
ai f :: QName
f <- ConHead -> [Arg QName]
conFields ConHead
c ]
subTel :: t -> t -> Tele a -> Tele a
subTel i :: t
i v :: t
v EmptyTel = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
subTel 0 v :: t
v (ExtendTel _ tel :: Abs (Tele a)
tel) = Abs (Tele a) -> t -> Tele a
forall t a. Subst t a => Abs a -> t -> a
absApp Abs (Tele a)
tel t
v
subTel i :: t
i v :: t
v (ExtendTel a :: a
a tel :: 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 -> t -> Tele a -> Tele a
subTel (t
i t -> t -> t
forall a. Num a => a -> a -> a
- 1) (Int -> t -> t
forall t a. Subst t a => Int -> a -> a
raise 1 t
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 t :: Clause
t es :: Elims
es = Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
apply Clause
t (Args -> Clause) -> Args -> Clause
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply CompiledClauses where
apply :: CompiledClauses -> Args -> CompiledClauses
apply cc :: CompiledClauses
cc args :: Args
args = case CompiledClauses
cc of
Fail -> CompiledClauses
forall a. CompiledClauses' a
Fail
Done hs :: [Arg String]
hs t :: Term
t
| [Arg String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg String]
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 [0..[Arg String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg String]
hs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1] [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args
in [Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
Done (Int -> [Arg String] -> [Arg String]
forall a. Int -> [a] -> [a]
List.drop Int
len [Arg String]
hs) (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sub Term
t
| Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
Case n :: Arg Int
n bs :: 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ m :: Int
m -> Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len) (Case CompiledClauses -> Args -> Case CompiledClauses
forall t. Apply t => t -> Args -> t
apply Case CompiledClauses
bs Args
args)
| Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
where
len :: Int
len = Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args
applyE :: CompiledClauses -> Elims -> CompiledClauses
applyE t :: CompiledClauses
t es :: Elims
es = CompiledClauses -> Args -> CompiledClauses
forall t. Apply t => t -> Args -> t
apply CompiledClauses
t (Args -> CompiledClauses) -> Args -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply ExtLamInfo where
apply :: ExtLamInfo -> Args -> ExtLamInfo
apply (ExtLamInfo m :: ModuleName
m sys :: Maybe System
sys) args :: Args
args = ModuleName -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
m (Maybe System -> Args -> Maybe System
forall t. Apply t => t -> Args -> t
apply Maybe System
sys Args
args)
applyE :: ExtLamInfo -> Elims -> ExtLamInfo
applyE t :: ExtLamInfo
t es :: Elims
es = ExtLamInfo -> Args -> ExtLamInfo
forall t. Apply t => t -> Args -> t
apply ExtLamInfo
t (Args -> ExtLamInfo) -> Args -> ExtLamInfo
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply System where
apply :: System -> Args -> System
apply (System tel :: Telescope
tel sys :: [(Face, Term)]
sys) args :: Args
args
= if Int
nargs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
ntel then System
forall a. HasCallStack => a
__IMPOSSIBLE__
else Telescope -> [(Face, Term)] -> System
System Telescope
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 a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- Bool -> Bool
forall c. c -> c
id) (Face -> Face) -> (Term -> Term) -> (Face, Term) -> (Face, Term)
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- Term -> Term
f) [(Face, Term)]
sys)
where
f :: Term -> Term
f = Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sigma
nargs :: Int
nargs = Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args
ntel :: Int
ntel = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
newTel :: Telescope
newTel = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
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) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args))
applyE :: System -> Elims -> System
applyE t :: System
t es :: Elims
es = System -> Args -> System
forall t. Apply t => t -> Args -> t
apply System
t (Args -> System) -> Args -> System
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply a => Apply (WithArity a) where
apply :: WithArity a -> Args -> WithArity a
apply (WithArity n :: Int
n a :: a
a) args :: Args
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 -> Args -> a
forall t. Apply t => t -> Args -> t
apply a
a Args
args
applyE :: WithArity a -> Elims -> WithArity a
applyE (WithArity n :: Int
n a :: a
a) es :: 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 -> Args -> Case a
apply (Branches cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: Bool
lz) args :: Args
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) -> Args -> Map QName (WithArity a)
forall t. Apply t => t -> Args -> t
apply Map QName (WithArity a)
cs Args
args) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (WithArity a -> Args -> WithArity a
forall t. Apply t => t -> Args -> t
`apply` Args
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 -> Args -> Map Literal a
forall t. Apply t => t -> Args -> t
apply Map Literal a
ls Args
args) (Maybe a -> Args -> Maybe a
forall t. Apply t => t -> Args -> t
apply Maybe a
m Args
args) Maybe Bool
b Bool
lz
applyE :: Case a -> Elims -> Case a
applyE (Branches cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: Bool
lz) es :: 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 (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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 -> Args -> FunctionInverse
apply NotInjective args :: Args
args = FunctionInverse
forall c. FunctionInverse' c
NotInjective
apply (Inverse inv :: InversionMap Clause
inv) args :: Args
args = InversionMap Clause -> FunctionInverse
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse)
-> InversionMap Clause -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ InversionMap Clause -> Args -> InversionMap Clause
forall t. Apply t => t -> Args -> t
apply InversionMap Clause
inv Args
args
applyE :: FunctionInverse -> Elims -> FunctionInverse
applyE t :: FunctionInverse
t es :: Elims
es = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
t (Args -> FunctionInverse) -> Args -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Apply DisplayTerm where
apply :: DisplayTerm -> Args -> DisplayTerm
apply (DTerm v :: Term
v) args :: Args
args = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
v Args
args
apply (DDot v :: Term
v) args :: Args
args = Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
v Args
args
apply (DCon c :: ConHead
c ci :: ConInfo
ci vs :: [Arg DisplayTerm]
vs) args :: Args
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) -> Args -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
args
apply (DDef c :: QName
c es :: [Elim' DisplayTerm]
es) args :: Args
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) -> Args -> [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
args
apply (DWithApp v :: DisplayTerm
v ws :: [DisplayTerm]
ws es :: Elims
es) args :: Args
args = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
v [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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
applyE :: DisplayTerm -> Elims -> DisplayTerm
applyE (DTerm v :: Term
v) es :: Elims
es = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v Elims
es
applyE (DDot v :: Term
v) es :: Elims
es = Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v Elims
es
applyE (DCon c :: ConHead
c ci :: ConInfo
ci vs :: [Arg DisplayTerm]
vs) es :: 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) -> Args -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
ws
where ws :: Args
ws = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
applyE (DDef c :: QName
c es' :: [Elim' DisplayTerm]
es') 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es
applyE (DWithApp v :: DisplayTerm
v ws :: [DisplayTerm]
ws es' :: Elims
es') es :: Elims
es = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
v [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] -> Args -> [t]
apply ts :: [t]
ts args :: Args
args = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) [t]
ts
applyE :: [t] -> Elims -> [t]
applyE ts :: [t]
ts es :: 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 -> Args -> Blocked t
apply b :: Blocked t
b args :: Args
args = (t -> t) -> Blocked t -> Blocked t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Blocked t
b
applyE :: Blocked t -> Elims -> Blocked t
applyE b :: Blocked t
b es :: Elims
es = (t -> t) -> Blocked t -> Blocked t
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 -> Args -> Maybe t
apply x :: Maybe t
x args :: Args
args = (t -> t) -> Maybe t -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Maybe t
x
applyE :: Maybe t -> Elims -> Maybe t
applyE x :: Maybe t
x es :: Elims
es = (t -> t) -> Maybe t -> Maybe t
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 -> Args -> Maybe t
apply x :: Maybe t
x args :: Args
args = (t -> t) -> Maybe t -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Maybe t
x
applyE :: Maybe t -> Elims -> Maybe t
applyE x :: Maybe t
x es :: Elims
es = (t -> t) -> Maybe t -> Maybe t
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 -> Args -> Map k v
apply x :: Map k v
x args :: Args
args = (v -> v) -> Map k v -> Map k v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Args -> v
forall t. Apply t => t -> Args -> t
`apply` Args
args) Map k v
x
applyE :: Map k v -> Elims -> Map k v
applyE x :: Map k v
x es :: Elims
es = (v -> v) -> Map k v -> Map k v
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 -> Args -> HashMap k v
apply x :: HashMap k v
x args :: Args
args = (v -> v) -> HashMap k v -> HashMap k v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Args -> v
forall t. Apply t => t -> Args -> t
`apply` Args
args) HashMap k v
x
applyE :: HashMap k v -> Elims -> HashMap k v
applyE x :: HashMap k v
x es :: Elims
es = (v -> v) -> HashMap k v -> HashMap k v
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) -> Args -> (a, b)
apply (x :: a
x,y :: b
y) args :: Args
args = (a -> Args -> a
forall t. Apply t => t -> Args -> t
apply a
x Args
args, b -> Args -> b
forall t. Apply t => t -> Args -> t
apply b
y Args
args)
applyE :: (a, b) -> Elims -> (a, b)
applyE (x :: a
x,y :: b
y) es :: 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) -> Args -> (a, b, c)
apply (x :: a
x,y :: b
y,z :: c
z) args :: Args
args = (a -> Args -> a
forall t. Apply t => t -> Args -> t
apply a
x Args
args, b -> Args -> b
forall t. Apply t => t -> Args -> t
apply b
y Args
args, c -> Args -> c
forall t. Apply t => t -> Args -> t
apply c
z Args
args)
applyE :: (a, b, c) -> Elims -> (a, b, c)
applyE (x :: a
x,y :: b
y,z :: c
z) es :: 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 -> Args -> Drop a
apply x :: Drop a
x args :: Args
args = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
dropMore (Args -> Int
forall a. Sized a => a -> Int
size Args
args) Drop a
x
applyE :: Drop a -> Elims -> Drop a
applyE t :: Drop a
t es :: Elims
es = Drop a -> Args -> Drop a
forall t. Apply t => t -> Args -> t
apply Drop a
t (Args -> Drop a) -> Args -> Drop a
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance DoDrop a => Abstract (Drop a) where
abstract :: Telescope -> Drop a -> Drop a
abstract tel :: Telescope
tel x :: Drop a
x = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
unDrop (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Drop a
x
instance Apply Permutation where
apply :: Permutation -> Args -> Permutation
apply (Perm n :: Int
n xs :: [Int]
xs) args :: Args
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 = Args -> Int
forall a. Sized a => a -> Int
size Args
args
applyE :: Permutation -> Elims -> Permutation
applyE t :: Permutation
t es :: Elims
es = Permutation -> Args -> Permutation
forall t. Apply t => t -> Args -> t
apply Permutation
t (Args -> Permutation) -> Args -> Permutation
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
instance Abstract Permutation where
abstract :: Telescope -> Permutation -> Permutation
abstract tel :: Telescope
tel (Perm n :: Int
n xs :: [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
$ [0..Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
piApply :: Type -> Args -> Type
piApply :: Type -> Args -> Type
piApply t :: Type
t [] = Type
t
piApply (El _ (Pi _ b :: Abs Type
b)) (a :: Arg Term
a:args :: Args
args) = Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Type -> Args -> Type
`piApply` Args
args
piApply t :: Type
t args :: Args
args =
String -> Type -> Type
forall a. String -> a -> a
trace ("piApply t = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n args = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Args -> String
forall a. Show a => a -> String
show Args
args) Type
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Abstract Term where
abstract :: Telescope -> Term -> Term
abstract = Telescope -> Term -> Term
teleLam
instance Abstract Type where
abstract :: Telescope -> Type -> Type
abstract = Telescope -> Type -> Type
telePi_
instance Abstract Sort where
abstract :: Telescope -> Sort -> Sort
abstract EmptyTel s :: Sort
s = Sort
s
abstract _ s :: Sort
s = Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Abstract Telescope where
EmptyTel abstract :: Telescope -> Telescope -> Telescope
`abstract` tel :: Telescope
tel = Telescope
tel
ExtendTel arg :: Dom Type
arg xtel :: Abs Telescope
xtel `abstract` tel :: Telescope
tel = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
arg (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Abs Telescope
xtel Abs Telescope -> (Telescope -> Telescope) -> Abs Telescope
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
tel)
instance Abstract Definition where
abstract :: Telescope -> Definition -> Definition
abstract tel :: Telescope
tel (Defn info :: ArgInfo
info x :: QName
x t :: Type
t pol :: [Polarity]
pol occ :: [Occurrence]
occ gens :: NumGeneralizableArgs
gens gpars :: [Maybe Name]
gpars df :: [LocalDisplayForm]
df m :: MutualId
m c :: CompiledRepresentation
c inst :: Maybe QName
inst copy :: Bool
copy ma :: Set QName
ma nc :: Bool
nc inj :: Bool
inj copat :: Bool
copat blk :: Blocked_
blk d :: Defn
d) =
ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Type
t) (Telescope -> [Polarity] -> [Polarity]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Polarity]
pol) (Telescope -> [Occurrence] -> [Occurrence]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Occurrence]
occ) (Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel NumGeneralizableArgs
gens)
(Int -> Maybe Name -> [Maybe Name]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
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 QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk (Telescope -> Defn -> Defn
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Defn
d)
instance Abstract RewriteRule where
abstract :: Telescope -> RewriteRule -> RewriteRule
abstract tel :: Telescope
tel (RewriteRule q :: QName
q gamma :: Telescope
gamma f :: QName
f ps :: PElims
ps rhs :: Term
rhs t :: Type
t) =
QName
-> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule
RewriteRule QName
q (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
gamma) QName
f PElims
ps Term
rhs Type
t
instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
abstract :: Telescope -> [Occurrence] -> [Occurrence]
abstract tel :: Telescope
tel [] = []
abstract tel :: Telescope
tel occ :: [Occurrence]
occ = Int -> Occurrence -> [Occurrence]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Occurrence
Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++ [Occurrence]
occ
instance {-# OVERLAPPING #-} Abstract [Polarity] where
abstract :: Telescope -> [Polarity] -> [Polarity]
abstract tel :: Telescope
tel [] = []
abstract tel :: Telescope
tel pol :: [Polarity]
pol = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Polarity
Invariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++ [Polarity]
pol
instance Abstract NumGeneralizableArgs where
abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
abstract tel :: Telescope
tel NoGeneralizableArgs = NumGeneralizableArgs
NoGeneralizableArgs
abstract tel :: Telescope
tel (SomeGeneralizableArgs n :: Int
n) = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
instance Abstract Projection where
abstract :: Telescope -> Projection -> Projection
abstract tel :: Telescope
tel p :: Projection
p = Projection
p
{ projIndex :: Int
projIndex = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Projection -> Int
projIndex Projection
p
, projLams :: ProjLams
projLams = Telescope -> ProjLams -> ProjLams
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (ProjLams -> ProjLams) -> ProjLams -> ProjLams
forall a b. (a -> b) -> a -> b
$ Projection -> ProjLams
projLams Projection
p
}
instance Abstract ProjLams where
abstract :: Telescope -> ProjLams -> ProjLams
abstract tel :: Telescope
tel (ProjLams lams :: [Arg String]
lams) = [Arg String] -> ProjLams
ProjLams ([Arg String] -> ProjLams) -> [Arg String] -> ProjLams
forall a b. (a -> b) -> a -> b
$
(Dom' Term (String, Type) -> Arg String)
-> [Dom' Term (String, Type)] -> [Arg String]
forall a b. (a -> b) -> [a] -> [b]
map (\ !Dom' Term (String, Type)
dom -> Dom' Term String -> Arg String
forall t a. Dom' t a -> Arg a
argFromDom ((String, Type) -> String
forall a b. (a, b) -> a
fst ((String, Type) -> String)
-> Dom' Term (String, Type) -> Dom' Term String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
dom)) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel) [Arg String] -> [Arg String] -> [Arg String]
forall a. [a] -> [a] -> [a]
++ [Arg String]
lams
instance Abstract System where
abstract :: Telescope -> System -> System
abstract tel :: Telescope
tel (System tel1 :: Telescope
tel1 sys :: [(Face, Term)]
sys) = Telescope -> [(Face, Term)] -> System
System (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel1) [(Face, Term)]
sys
instance Abstract Defn where
abstract :: Telescope -> Defn -> Defn
abstract tel :: Telescope
tel d :: Defn
d = case Defn
d of
Axiom{} -> Defn
d
DataOrRecSig n :: Int
n -> Int -> Defn
DataOrRecSig (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
GeneralizableVar{} -> Defn
d
AbstractDefn d :: Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Telescope -> Defn -> Defn
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
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
funInv = FunctionInverse
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
Nothing } ->
Defn
d { funClauses :: [Clause]
funClauses = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cs
, funCompiled :: Maybe CompiledClauses
funCompiled = Telescope -> Maybe CompiledClauses -> Maybe CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe CompiledClauses
cc
, funCovering :: [Clause]
funCovering = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cov
, funInv :: FunctionInverse
funInv = Telescope -> FunctionInverse -> FunctionInverse
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel FunctionInverse
inv
, funExtLam :: Maybe ExtLamInfo
funExtLam = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (Telescope -> System -> System
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
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
funInv = FunctionInverse
inv
, funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
, funProjection :: Defn -> Maybe Projection
funProjection = Just p :: Projection
p } ->
if Projection -> Int
projIndex Projection
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Defn
d' else
Defn
d' { funClauses :: [Clause]
funClauses = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 [Clause]
cs
, funCompiled :: Maybe CompiledClauses
funCompiled = Telescope -> Maybe CompiledClauses -> Maybe CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 Maybe CompiledClauses
cc
, funCovering :: [Clause]
funCovering = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 [Clause]
cov
, funInv :: FunctionInverse
funInv = Telescope -> FunctionInverse -> FunctionInverse
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 FunctionInverse
inv
, funExtLam :: Maybe ExtLamInfo
funExtLam = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ _ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extLam
}
where
d' :: Defn
d' = Defn
d { funProjection :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Telescope -> Projection -> Projection
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Projection
p }
tel1 :: Telescope
tel1 = [Dom' Term (String, Type)] -> Telescope
telFromList ([Dom' Term (String, Type)] -> Telescope)
-> [Dom' Term (String, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a. Int -> [a] -> [a]
drop (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
-> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
Defn
d { dataPars :: Int
dataPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
, dataClause :: Maybe Clause
dataClause = Telescope -> Maybe Clause -> Maybe Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe Clause
cl
}
Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Telescope
recTel = Telescope
tel' } ->
Defn
d { recPars :: Int
recPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
, recClause :: Maybe Clause
recClause = Telescope -> Maybe Clause -> Maybe Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe Clause
cl
, recTel :: Telescope
recTel = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel'
}
Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
Defn
d { conPars :: Int
conPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel }
Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
Defn
d { primClauses :: [Clause]
primClauses = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cs }
instance Abstract PrimFun where
abstract :: Telescope -> PrimFun -> PrimFun
abstract tel :: Telescope
tel (PrimFun x :: QName
x ar :: Int
ar def :: Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) = QName
-> Int
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun)
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \ts :: Args
ts -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop Int
n Args
ts
where n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
instance Abstract Clause where
abstract :: Telescope -> Clause -> Clause
abstract tel :: Telescope
tel (Clause rl :: Range
rl rf :: Range
rf tel' :: Telescope
tel' ps :: NAPs
ps b :: Maybe Term
b t :: Maybe (Arg Type)
t catchall :: Bool
catchall recursive :: Maybe Bool
recursive unreachable :: Maybe Bool
unreachable ell :: ExpandedEllipsis
ell) =
Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
rl Range
rf (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel')
(Int -> Telescope -> NAPs
namedTelVars Int
m Telescope
tel NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps)
Maybe Term
b
Maybe (Arg Type)
t
Bool
catchall
Maybe Bool
recursive
Maybe Bool
unreachable
ExpandedEllipsis
ell
where m :: Int
m = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel'
instance Abstract CompiledClauses where
abstract :: Telescope -> CompiledClauses -> CompiledClauses
abstract tel :: Telescope
tel Fail = CompiledClauses
forall a. CompiledClauses' a
Fail
abstract tel :: Telescope
tel (Done xs :: [Arg String]
xs t :: Term
t) = [Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
Done ((Dom' Term (String, Type) -> Arg String)
-> [Dom' Term (String, Type)] -> [Arg String]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term String -> Arg String
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term String -> Arg String)
-> (Dom' Term (String, Type) -> Dom' Term String)
-> Dom' Term (String, Type)
-> Arg String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type) -> String)
-> Dom' Term (String, Type) -> Dom' Term String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, Type) -> String
forall a b. (a, b) -> a
fst) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel) [Arg String] -> [Arg String] -> [Arg String]
forall a. [a] -> [a] -> [a]
++ [Arg String]
xs) Term
t
abstract tel :: Telescope
tel (Case n :: Arg Int
n bs :: 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ i :: Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Telescope -> Case CompiledClauses -> Case CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Case CompiledClauses
bs)
instance Abstract a => Abstract (WithArity a) where
abstract :: Telescope -> WithArity a -> WithArity a
abstract tel :: Telescope
tel (WithArity n :: Int
n a :: 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
$ Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel a
a
instance Abstract a => Abstract (Case a) where
abstract :: Telescope -> Case a -> Case a
abstract tel :: Telescope
tel (Branches cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: 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 (Telescope -> Map QName (WithArity a) -> Map QName (WithArity a)
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Map QName (WithArity a)
cs) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Telescope -> WithArity a -> WithArity a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
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)
(Telescope -> Map Literal a -> Map Literal a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Map Literal a
ls) (Telescope -> Maybe a -> Maybe a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe a
m) Maybe Bool
b Bool
lz
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars m :: Int
m = (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NAPs -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
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) (NAPs -> [Arg DeBruijnPattern])
-> (Telescope -> NAPs) -> Telescope -> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Telescope -> NAPs
namedTelVars Int
m)
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars :: Int -> Telescope -> NAPs
namedTelVars m :: Int
m EmptyTel = []
namedTelVars m :: Int
m (ExtendTel !Dom Type
dom tel :: Abs Telescope
tel) =
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) (Int -> String -> Named NamedName DeBruijnPattern
namedDBVarP (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (String -> Named NamedName DeBruijnPattern)
-> String -> Named NamedName DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> String
forall a. Abs a -> String
absName Abs Telescope
tel) NamedArg DeBruijnPattern -> NAPs -> NAPs
forall a. a -> [a] -> [a]
:
Int -> Telescope -> NAPs
namedTelVars (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel)
instance Abstract FunctionInverse where
abstract :: Telescope -> FunctionInverse -> FunctionInverse
abstract tel :: Telescope
tel NotInjective = FunctionInverse
forall c. FunctionInverse' c
NotInjective
abstract tel :: Telescope
tel (Inverse inv :: InversionMap Clause
inv) = InversionMap Clause -> FunctionInverse
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse)
-> InversionMap Clause -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Telescope -> InversionMap Clause -> InversionMap Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel InversionMap Clause
inv
instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where
abstract :: Telescope -> [t] -> [t]
abstract tel :: Telescope
tel = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (Telescope -> t -> t
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel)
instance Abstract t => Abstract (Maybe t) where
abstract :: Telescope -> Maybe t -> Maybe t
abstract tel :: Telescope
tel x :: Maybe t
x = (t -> t) -> Maybe t -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> t -> t
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) Maybe t
x
instance Abstract v => Abstract (Map k v) where
abstract :: Telescope -> Map k v -> Map k v
abstract tel :: Telescope
tel m :: Map k v
m = (v -> v) -> Map k v -> Map k v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> v -> v
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) Map k v
m
instance Abstract v => Abstract (HashMap k v) where
abstract :: Telescope -> HashMap k v -> HashMap k v
abstract tel :: Telescope
tel m :: HashMap k v
m = (v -> v) -> HashMap k v -> HashMap k v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> v -> v
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) HashMap k v
m
abstractArgs :: Abstract a => Args -> a -> a
abstractArgs :: Args -> a -> a
abstractArgs args :: Args
args x :: a
x = Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel a
x
where
tel :: Telescope
tel = (Arg String -> Telescope -> Telescope)
-> Telescope -> [Arg String] -> Telescope
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\arg :: Arg String
arg@(Arg info :: ArgInfo
info x :: String
x) -> Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
HasCallStack => Type
__DUMMY_TYPE__ Type -> Dom' Term String -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg String -> Dom' Term String
forall a. Arg a -> Dom a
domFromArg Arg String
arg) (Abs Telescope -> Telescope)
-> (Telescope -> Abs Telescope) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
x)
Telescope
forall a. Tele a
EmptyTel
([Arg String] -> Telescope) -> [Arg String] -> Telescope
forall a b. (a -> b) -> a -> b
$ (String -> Arg Term -> Arg String)
-> [String] -> Args -> [Arg String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> Arg Term -> Arg String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [String]
names Args
args
names :: [String]
names = [String] -> [String]
forall a. [a] -> [a]
cycle ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
stringToArgName (String -> String) -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String -> String
forall a. a -> [a] -> [a]
:[])) ['a'..'z']
renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming :: Empty -> Permutation -> Substitution' a
renaming err :: Empty
err p :: Permutation
p = Empty -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Empty
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 :: Permutation -> Substitution' a
renamingR p :: Permutation
p@(Perm n :: Int
n _) = Permutation -> [a] -> [a]
forall a. Permutation -> [a] -> [a]
permute (Permutation -> Permutation
reverseP Permutation
p) ((Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar [0..]) [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
renameP :: Subst t a => Empty -> Permutation -> a -> a
renameP :: Empty -> Permutation -> a -> a
renameP err :: Empty
err p :: Permutation
p = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> Permutation -> Substitution' t
forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming Empty
err Permutation
p)
instance Subst a a => Subst a (Substitution' a) where
applySubst :: Substitution' a -> Substitution' a -> Substitution' a
applySubst rho :: Substitution' a
rho sgm :: Substitution' a
sgm = Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho Substitution' a
sgm
{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
applySubstTerm :: forall t. (Coercible t Term, Subst t t, Apply t) => Substitution' t -> t -> t
applySubstTerm :: Substitution' t -> t -> t
applySubstTerm IdS t :: t
t = t
t
applySubstTerm rho :: Substitution' t
rho t :: 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 i :: Int
i es :: Elims
es -> t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' t -> Int -> t
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' t
rho Int
i t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims -> Elims
subE Elims
es
Lam h :: ArgInfo
h m :: Abs Term
m -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Abs Term -> Abs Term
forall a b. (Coercible b a, Subst t a) => b -> b
sub @(Abs t) Abs Term
m
Def f :: QName
f es :: Elims
es -> QName -> Elims -> Elims -> Term
defApp QName
f [] (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE Elims
es
Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE Elims
vs
MetaV x :: MetaId
x es :: Elims
es -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE Elims
es
Lit l :: Literal
l -> Literal -> Term
Lit Literal
l
Level l :: Level
l -> Level -> Term
levelTm (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall a b. (Coercible b a, Subst t a) => b -> b
sub @(Level' t) Level
l
Pi a :: Dom Type
a b :: Abs Type
b -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi ((Dom Type, Abs Type) -> Term) -> (Dom Type, Abs Type) -> Term
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi (Dom Type
a,Abs Type
b)
Sort s :: Sort
s -> Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall a b. (Coercible b a, Subst t a) => b -> b
sub @(Sort' t) Sort
s
DontCare mv :: Term
mv -> Term -> Term
dontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall a b. (Coercible b a, Subst t a) => b -> b
sub @t Term
mv
Dummy s :: String
s es :: Elims
es -> String -> Elims -> Term
Dummy String
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE Elims
es
where
sub :: forall a b. (Coercible b a, Subst t a) => b -> b
sub :: b -> b
sub t :: b
t = a -> b
forall a b. Coercible a b => a -> b
coerce (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (b -> a
forall a b. Coercible a b => a -> b
coerce b
t :: a)
subE :: Elims -> Elims
subE :: Elims -> Elims
subE = forall b. (Coercible b [Elim' t], Subst t [Elim' t]) => b -> b
forall a b. (Coercible b a, Subst t a) => b -> b
sub @[Elim' t]
subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi = forall b.
(Coercible b (Dom' t (Type'' t t), Abs (Type'' t t)),
Subst t (Dom' t (Type'' t t), Abs (Type'' t t))) =>
b -> b
forall a b. (Coercible b a, Subst t a) => b -> b
sub @(Dom' t (Type'' t t), Abs (Type'' t t))
instance Subst Term Term where
applySubst :: Substitution' Term -> Term -> Term
applySubst = Substitution' Term -> Term -> Term
forall t.
(Coercible t Term, Subst t t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm
instance Subst BraveTerm BraveTerm where
applySubst :: Substitution' BraveTerm -> BraveTerm -> BraveTerm
applySubst = Substitution' BraveTerm -> BraveTerm -> BraveTerm
forall t.
(Coercible t Term, Subst t t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm
instance (Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) where
applySubst :: Substitution' t -> Type'' a b -> Type'' a b
applySubst rho :: Substitution' t
rho (El s :: Sort' a
s t :: b
t) = Substitution' t -> Sort' a -> Sort' a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho Sort' a
s Sort' a -> b -> Type'' a b
forall t a. Sort' t -> a -> Type'' t a
`El` Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho b
t
instance (Coercible a Term, Subst t a) => Subst t (Sort' a) where
applySubst :: Substitution' t -> Sort' a -> Sort' a
applySubst rho :: Substitution' t
rho s :: Sort' a
s = case Sort' a
s of
Type n :: Level' a
n -> Level' a -> Sort' a
forall t. Level' t -> Sort' t
Type (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Level' a -> Level' a
forall a. Subst t a => a -> a
sub Level' a
n
Prop n :: Level' a
n -> Level' a -> Sort' a
forall t. Level' t -> Sort' t
Prop (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Level' a -> Level' a
forall a. Subst t a => a -> a
sub Level' a
n
Inf -> Sort' a
forall t. Sort' t
Inf
SizeUniv -> Sort' a
forall t. Sort' t
SizeUniv
PiSort a :: Dom' a (Type'' a a)
a s2 :: Abs (Sort' a)
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort (Dom' a (Type'' a a) -> Dom Type
forall a b. Coercible a b => a -> b
coerce (Dom' a (Type'' a a) -> Dom Type)
-> Dom' a (Type'' a a) -> Dom Type
forall a b. (a -> b) -> a -> b
$ Dom' a (Type'' a a) -> Dom' a (Type'' a a)
forall a. Subst t a => a -> a
sub Dom' a (Type'' a a)
a) (Abs (Sort' a) -> Abs Sort
forall a b. Coercible a b => a -> b
coerce (Abs (Sort' a) -> Abs Sort) -> Abs (Sort' a) -> Abs Sort
forall a b. (a -> b) -> a -> b
$ Abs (Sort' a) -> Abs (Sort' a)
forall a. Subst t a => a -> a
sub Abs (Sort' a)
s2)
FunSort s1 :: Sort' a
s1 s2 :: Sort' a
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s1) (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s2)
UnivSort s :: Sort' a
s -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Maybe Sort -> Sort -> Sort
univSort Maybe Sort
forall a. Maybe a
Nothing (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s
MetaS x :: MetaId
x es :: [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
$ [Elim' a] -> [Elim' a]
forall a. Subst t a => a -> a
sub [Elim' a]
es
DefS d :: QName
d es :: [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
$ [Elim' a] -> [Elim' a]
forall a. Subst t a => a -> a
sub [Elim' a]
es
DummyS{} -> Sort' a
s
where sub :: a -> a
sub x :: a
x = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x
instance Subst t a => Subst t (Level' a) where
applySubst :: Substitution' t -> Level' a -> Level' a
applySubst rho :: Substitution' t
rho (Max n :: Integer
n as :: [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' t -> [PlusLevel' a] -> [PlusLevel' a]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho [PlusLevel' a]
as
instance Subst t a => Subst t (PlusLevel' a) where
applySubst :: Substitution' t -> PlusLevel' a -> PlusLevel' a
applySubst rho :: Substitution' t
rho (Plus n :: Integer
n l :: LevelAtom' a
l) = Integer -> LevelAtom' a -> PlusLevel' a
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
n (LevelAtom' a -> PlusLevel' a) -> LevelAtom' a -> PlusLevel' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> LevelAtom' a -> LevelAtom' a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho LevelAtom' a
l
instance Subst t a => Subst t (LevelAtom' a) where
applySubst :: Substitution' t -> LevelAtom' a -> LevelAtom' a
applySubst rho :: Substitution' t
rho (MetaLevel m :: MetaId
m vs :: [Elim' a]
vs) = MetaId -> [Elim' a] -> LevelAtom' a
forall t. MetaId -> [Elim' t] -> LevelAtom' t
MetaLevel MetaId
m ([Elim' a] -> LevelAtom' a) -> [Elim' a] -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> [Elim' a] -> [Elim' a]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho [Elim' a]
vs
applySubst rho :: Substitution' t
rho (BlockedLevel m :: MetaId
m v :: a
v) = MetaId -> a -> LevelAtom' a
forall t. MetaId -> t -> LevelAtom' t
BlockedLevel MetaId
m (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v
applySubst rho :: Substitution' t
rho (NeutralLevel _ v :: a
v) = a -> LevelAtom' a
forall t. t -> LevelAtom' t
UnreducedLevel (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v
applySubst rho :: Substitution' t
rho (UnreducedLevel v :: a
v) = a -> LevelAtom' a
forall t. t -> LevelAtom' t
UnreducedLevel (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v
instance Subst Term Name where
applySubst :: Substitution' Term -> Name -> Name
applySubst rho :: Substitution' Term
rho = Name -> Name
forall c. c -> c
id
instance {-# OVERLAPPING #-} Subst Term String where
applySubst :: Substitution' Term -> String -> String
applySubst rho :: Substitution' Term
rho = String -> String
forall c. c -> c
id
instance Subst Term ConPatternInfo where
applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo
applySubst rho :: Substitution' Term
rho i :: ConPatternInfo
i = ConPatternInfo
i{ conPType :: Maybe (Arg Type)
conPType = Substitution' Term -> Maybe (Arg Type) -> Maybe (Arg Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho (Maybe (Arg Type) -> Maybe (Arg Type))
-> Maybe (Arg Type) -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i }
instance Subst Term Pattern where
applySubst :: Substitution' Term -> Pattern -> Pattern
applySubst rho :: Substitution' Term
rho p :: Pattern
p = case Pattern
p of
ConP c :: ConHead
c mt :: ConPatternInfo
mt ps :: [NamedArg Pattern]
ps -> ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (Substitution' Term -> ConPatternInfo -> ConPatternInfo
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho ConPatternInfo
mt) ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> [NamedArg Pattern] -> [NamedArg Pattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [NamedArg Pattern]
ps
DefP o :: PatternInfo
o q :: QName
q ps :: [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' Term -> [NamedArg Pattern] -> [NamedArg Pattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [NamedArg Pattern]
ps
DotP o :: PatternInfo
o t :: 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' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
t
VarP o :: PatternInfo
o s :: String
s -> Pattern
p
LitP o :: PatternInfo
o l :: Literal
l -> Pattern
p
ProjP{} -> Pattern
p
IApplyP o :: PatternInfo
o t :: Term
t u :: Term
u x :: String
x -> PatternInfo -> Term -> Term -> String -> Pattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
t) (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
u) String
x
instance Subst Term A.ProblemEq where
applySubst :: Substitution' Term -> ProblemEq -> ProblemEq
applySubst rho :: Substitution' Term
rho (A.ProblemEq p :: Pattern
p v :: Term
v a :: 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' Term -> (Term, Dom Type) -> (Term, Dom Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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 i :: Int
i = Int -> [Arg Int] -> NLPat
PVar Int
i []
deBruijnView :: NLPat -> Maybe Int
deBruijnView p :: NLPat
p = case NLPat
p of
PVar i :: 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{} -> Maybe Int
forall a. Maybe a
Nothing
PTerm{} -> Maybe Int
forall a. Maybe a
Nothing
applyNLPatSubst :: (Subst Term a) => Substitution' NLPat -> a -> a
applyNLPatSubst :: Substitution' NLPat -> a -> a
applyNLPatSubst = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NLPat -> Term
nlPatToTerm
where
nlPatToTerm :: NLPat -> Term
nlPatToTerm :: NLPat -> Term
nlPatToTerm p :: NLPat
p = case NLPat
p of
PVar i :: Int
i xs :: [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
xs
PTerm u :: Term
u -> Term
u
PDef f :: QName
f es :: PElims
es -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PLam i :: ArgInfo
i u :: Abs NLPat
u -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PPi a :: Dom NLPType
a b :: Abs NLPType
b -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PSort s :: NLPSort
s -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
PBoundVar i :: Int
i es :: PElims
es -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
applyNLSubstToDom :: Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom :: Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom rho :: Substitution' NLPat
rho dom :: Dom a
dom = Substitution' NLPat -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho (a -> a) -> Dom a -> Dom a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom a
dom{ domTactic :: Maybe Term
domTactic = Substitution' NLPat -> Maybe Term -> Maybe Term
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
rho (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Dom a -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom a
dom }
instance Subst NLPat NLPat where
applySubst :: Substitution' NLPat -> NLPat -> NLPat
applySubst rho :: Substitution' NLPat
rho p :: NLPat
p = case NLPat
p of
PVar i :: Int
i bvs :: [Arg Int]
bvs -> Substitution' NLPat -> Int -> NLPat
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' NLPat
rho Int
i NLPat -> [Arg Int] -> NLPat
`applyBV` [Arg Int]
bvs
PDef f :: QName
f es :: PElims
es -> QName -> PElims -> NLPat
PDef QName
f (PElims -> NLPat) -> PElims -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho PElims
es
PLam i :: ArgInfo
i u :: Abs NLPat
u -> ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
i (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> Abs NLPat -> Abs NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho Abs NLPat
u
PPi a :: Dom NLPType
a b :: Abs NLPType
b -> Dom NLPType -> Abs NLPType -> NLPat
PPi (Substitution' NLPat -> Dom NLPType -> Dom NLPType
forall a. Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
rho Dom NLPType
a) (Substitution' NLPat -> Abs NLPType -> Abs NLPType
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho Abs NLPType
b)
PSort s :: NLPSort
s -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> NLPSort -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPSort -> NLPSort
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPSort
s
PBoundVar i :: Int
i es :: PElims
es -> Int -> PElims -> NLPat
PBoundVar Int
i (PElims -> NLPat) -> PElims -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho PElims
es
PTerm u :: Term
u -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> Term -> Term
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
rho Term
u
where
applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV p :: NLPat
p ys :: [Arg Int]
ys = case NLPat
p of
PVar i :: Int
i xs :: [Arg Int]
xs -> Int -> [Arg Int] -> NLPat
PVar Int
i ([Arg Int]
xs [Arg Int] -> [Arg Int] -> [Arg Int]
forall a. [a] -> [a] -> [a]
++ [Arg Int]
ys)
PTerm u :: Term
u -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Term
u Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Arg Int -> Arg Term) -> [Arg Int] -> Args
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Term) -> Arg Int -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
ys
PDef f :: QName
f es :: PElims
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PLam i :: ArgInfo
i u :: Abs NLPat
u -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PPi a :: Dom NLPType
a b :: Abs NLPType
b -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PSort s :: NLPSort
s -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
PBoundVar i :: Int
i es :: PElims
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Subst NLPat NLPType where
applySubst :: Substitution' NLPat -> NLPType -> NLPType
applySubst rho :: Substitution' NLPat
rho (NLPType s :: NLPSort
s a :: NLPat
a) = NLPSort -> NLPat -> NLPType
NLPType (Substitution' NLPat -> NLPSort -> NLPSort
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPSort
s) (Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
a)
instance Subst NLPat NLPSort where
applySubst :: Substitution' NLPat -> NLPSort -> NLPSort
applySubst rho :: Substitution' NLPat
rho = \case
PType l :: NLPat
l -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
l
PProp l :: NLPat
l -> NLPat -> NLPSort
PProp (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
l
PInf -> NLPSort
PInf
PSizeUniv -> NLPSort
PSizeUniv
instance Subst NLPat RewriteRule where
applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule
applySubst rho :: Substitution' NLPat
rho (RewriteRule q :: QName
q gamma :: Telescope
gamma f :: QName
f ps :: PElims
ps rhs :: Term
rhs t :: Type
t) =
QName
-> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule
RewriteRule QName
q (Substitution' NLPat -> Telescope -> Telescope
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
rho Telescope
gamma)
QName
f (Substitution' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
rho) PElims
ps)
(Substitution' NLPat -> Term -> Term
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
rho) Term
rhs)
(Substitution' NLPat -> Type -> Type
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' NLPat
rho) Type
t)
where n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma
instance Subst t a => Subst t (Blocked a) where
applySubst :: Substitution' t -> Blocked a -> Blocked a
applySubst rho :: Substitution' t
rho b :: Blocked a
b = (a -> a) -> Blocked a -> Blocked a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho) Blocked a
b
instance Subst Term DisplayForm where
applySubst :: Substitution' Term -> DisplayForm -> DisplayForm
applySubst rho :: Substitution' Term
rho (Display n :: Int
n ps :: Elims
ps v :: DisplayTerm
v) =
Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n (Substitution' Term -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS 1 Substitution' Term
rho) Elims
ps)
(Substitution' Term -> DisplayTerm -> DisplayTerm
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
rho) DisplayTerm
v)
instance Subst Term DisplayTerm where
applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm
applySubst rho :: Substitution' Term
rho (DTerm v :: Term
v) = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
v
applySubst rho :: Substitution' Term
rho (DDot v :: Term
v) = Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
v
applySubst rho :: Substitution' Term
rho (DCon c :: ConHead
c ci :: ConInfo
ci vs :: [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' Term -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [Arg DisplayTerm]
vs
applySubst rho :: Substitution' Term
rho (DDef c :: QName
c es :: [Elim' DisplayTerm]
es) = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [Elim' DisplayTerm]
es
applySubst rho :: Substitution' Term
rho (DWithApp v :: DisplayTerm
v vs :: [DisplayTerm]
vs es :: Elims
es) = (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp ((DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm)
-> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term
-> (DisplayTerm, [DisplayTerm], Elims)
-> (DisplayTerm, [DisplayTerm], Elims)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho (DisplayTerm
v, [DisplayTerm]
vs, Elims
es)
instance Subst t a => Subst t (Tele a) where
applySubst :: Substitution' t -> Tele a -> Tele a
applySubst rho :: Substitution' t
rho EmptyTel = Tele a
forall a. Tele a
EmptyTel
applySubst rho :: Substitution' t
rho (ExtendTel t :: a
t tel :: Abs (Tele a)
tel) = (a -> Abs (Tele a) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel ((a, Abs (Tele a)) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> (a, Abs (Tele a)) -> (a, Abs (Tele a))
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (a
t, Abs (Tele a)
tel)
instance Subst Term Constraint where
applySubst :: Substitution' Term -> Constraint -> Constraint
applySubst rho :: Substitution' Term
rho c :: Constraint
c = case Constraint
c of
ValueCmp cmp :: Comparison
cmp a :: CompareAs
a u :: Term
u v :: Term
v -> Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp (CompareAs -> CompareAs
forall a. Subst Term a => a -> a
rf CompareAs
a) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
u) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
v)
ValueCmpOnFace cmp :: Comparison
cmp p :: Term
p t :: Type
t u :: Term
u v :: Term
v -> Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
cmp (Term -> Term
forall a. Subst Term a => a -> a
rf Term
p) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
t) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
u) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
v)
ElimCmp ps :: [Polarity]
ps fs :: [IsForced]
fs a :: Type
a v :: Term
v e1 :: Elims
e1 e2 :: Elims
e2 -> [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
ps [IsForced]
fs (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
v) (Elims -> Elims
forall a. Subst Term a => a -> a
rf Elims
e1) (Elims -> Elims
forall a. Subst Term a => a -> a
rf Elims
e2)
TelCmp a :: Type
a b :: Type
b cmp :: Comparison
cmp tel1 :: Telescope
tel1 tel2 :: Telescope
tel2 -> Type -> Type -> Comparison -> Telescope -> Telescope -> Constraint
TelCmp (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
b) Comparison
cmp (Telescope -> Telescope
forall a. Subst Term a => a -> a
rf Telescope
tel1) (Telescope -> Telescope
forall a. Subst Term a => a -> a
rf Telescope
tel2)
SortCmp cmp :: Comparison
cmp s1 :: Sort
s1 s2 :: Sort
s2 -> Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s1) (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s2)
LevelCmp cmp :: Comparison
cmp l1 :: Level
l1 l2 :: Level
l2 -> Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp (Level -> Level
forall a. Subst Term a => a -> a
rf Level
l1) (Level -> Level
forall a. Subst Term a => a -> a
rf Level
l2)
Guarded c :: Constraint
c cs :: ProblemId
cs -> Constraint -> ProblemId -> Constraint
Guarded (Constraint -> Constraint
forall a. Subst Term a => a -> a
rf Constraint
c) ProblemId
cs
IsEmpty r :: Range
r a :: Type
a -> Range -> Type -> Constraint
IsEmpty Range
r (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a)
CheckSizeLtSat t :: Term
t -> Term -> Constraint
CheckSizeLtSat (Term -> Term
forall a. Subst Term a => a -> a
rf Term
t)
FindInstance m :: MetaId
m b :: Maybe MetaId
b cands :: Maybe [Candidate]
cands -> MetaId -> Maybe MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m Maybe MetaId
b (Maybe [Candidate] -> Maybe [Candidate]
forall a. Subst Term a => a -> a
rf Maybe [Candidate]
cands)
UnBlock{} -> Constraint
c
CheckFunDef{} -> Constraint
c
HasBiggerSort s :: Sort
s -> Sort -> Constraint
HasBiggerSort (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s)
HasPTSRule a :: Dom Type
a s :: Abs Sort
s -> Dom Type -> Abs Sort -> Constraint
HasPTSRule (Dom Type -> Dom Type
forall a. Subst Term a => a -> a
rf Dom Type
a) (Abs Sort -> Abs Sort
forall a. Subst Term a => a -> a
rf Abs Sort
s)
UnquoteTactic m :: Maybe MetaId
m t :: Term
t h :: Term
h g :: Type
g -> Maybe MetaId -> Term -> Term -> Type -> Constraint
UnquoteTactic Maybe MetaId
m (Term -> Term
forall a. Subst Term a => a -> a
rf Term
t) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
h) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
g)
CheckMetaInst m :: MetaId
m -> MetaId -> Constraint
CheckMetaInst MetaId
m
where
rf :: a -> a
rf x :: a
x = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho a
x
instance Subst Term CompareAs where
applySubst :: Substitution' Term -> CompareAs -> CompareAs
applySubst rho :: Substitution' Term
rho (AsTermsOf a :: Type
a) = Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> Type -> CompareAs
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Type
a
applySubst rho :: Substitution' Term
rho AsSizes = CompareAs
AsSizes
applySubst rho :: Substitution' Term
rho AsTypes = CompareAs
AsTypes
instance Subst t a => Subst t (Elim' a) where
applySubst :: Substitution' t -> Elim' a -> Elim' a
applySubst rho :: Substitution' t
rho e :: Elim' a
e = case Elim' a
e of
Apply v :: Arg a
v -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a) -> Arg a -> Elim' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> Arg a -> Arg a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho Arg a
v
IApply x :: a
x y :: a
y r :: a
r -> a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x) (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
y) (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
r)
Proj{} -> Elim' a
e
instance Subst t a => Subst t (Abs a) where
applySubst :: Substitution' t -> Abs a -> Abs a
applySubst rho :: Substitution' t
rho (Abs x :: String
x a :: a
a) = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' t -> Substitution' t
forall a. Int -> Substitution' a -> Substitution' a
liftS 1 Substitution' t
rho) a
a
applySubst rho :: Substitution' t
rho (NoAbs x :: String
x a :: a
a) = String -> a -> Abs a
forall a. String -> a -> Abs a
NoAbs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
a
instance Subst t a => Subst t (Arg a) where
applySubst :: Substitution' t -> Arg a -> Arg a
applySubst IdS arg :: Arg a
arg = Arg a
arg
applySubst rho :: Substitution' t
rho arg :: Arg a
arg = FreeVariables -> Arg a -> Arg a
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables (Arg a -> Arg a) -> Arg a -> Arg a
forall a b. (a -> b) -> a -> b
$ (a -> a) -> Arg a -> Arg a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho) Arg a
arg
instance Subst t a => Subst t (Named name a) where
applySubst :: Substitution' t -> Named name a -> Named name a
applySubst rho :: Substitution' t
rho = (a -> a) -> Named name a -> Named name a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho)
instance (Subst t a, Subst t b) => Subst t (Dom' a b) where
applySubst :: Substitution' t -> Dom' a b -> Dom' a b
applySubst IdS dom :: Dom' a b
dom = Dom' a b
dom
applySubst rho :: Substitution' t
rho dom :: Dom' a b
dom = FreeVariables -> Dom' a b -> Dom' a b
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables (Dom' a b -> Dom' a b) -> Dom' a b -> Dom' a b
forall a b. (a -> b) -> a -> b
$
(b -> b) -> Dom' a b -> Dom' a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho) Dom' a b
dom{ domTactic :: Maybe a
domTactic = Substitution' t -> Maybe a -> Maybe a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (Dom' a b -> Maybe a
forall t e. Dom' t e -> Maybe t
domTactic Dom' a b
dom) }
instance Subst t a => Subst t (Maybe a) where
instance Subst t a => Subst t [a] where
instance (Ord k, Subst t a) => Subst t (Map k a) where
instance Subst t a => Subst t (WithHiding a) where
instance Subst Term () where
applySubst :: Substitution' Term -> () -> ()
applySubst _ _ = ()
instance (Subst t a, Subst t b) => Subst t (a, b) where
applySubst :: Substitution' t -> (a, b) -> (a, b)
applySubst rho :: Substitution' t
rho (x :: a
x,y :: b
y) = (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x, Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho b
y)
instance (Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) where
applySubst :: Substitution' t -> (a, b, c) -> (a, b, c)
applySubst rho :: Substitution' t
rho (x :: a
x,y :: b
y,z :: c
z) = (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x, Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho b
y, Substitution' t -> c -> c
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho c
z)
instance (Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) where
applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d)
applySubst rho :: Substitution' t
rho (x :: a
x,y :: b
y,z :: c
z,u :: d
u) = (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x, Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho b
y, Substitution' t -> c -> c
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho c
z, Substitution' t -> d -> d
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho d
u)
instance Subst Term Candidate where
applySubst :: Substitution' Term -> Candidate -> Candidate
applySubst rho :: Substitution' Term
rho (Candidate u :: Term
u t :: Type
t ov :: Bool
ov) = Term -> Type -> Bool -> Candidate
Candidate (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
u) (Substitution' Term -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Type
t) Bool
ov
instance Subst Term EqualityView where
applySubst :: Substitution' Term -> EqualityView -> EqualityView
applySubst rho :: Substitution' Term
rho (OtherType t :: Type
t) = Type -> EqualityView
OtherType
(Substitution' Term -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Type
t)
applySubst rho :: Substitution' Term
rho (EqualityType s :: Sort
s eq :: QName
eq l :: Args
l t :: Arg Term
t a :: Arg Term
a b :: Arg Term
b) = Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType
(Substitution' Term -> Sort -> Sort
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Sort
s)
QName
eq
((Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Substitution' Term -> Arg Term -> Arg Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho) Args
l)
(Substitution' Term -> Arg Term -> Arg Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Arg Term
t)
(Substitution' Term -> Arg Term -> Arg Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Arg Term
a)
(Substitution' Term -> Arg Term -> Arg Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Arg Term
b)
instance DeBruijn a => DeBruijn (Pattern' a) where
debruijnNamedVar :: String -> Int -> Pattern' a
debruijnNamedVar n :: String
n i :: Int
i = a -> Pattern' a
forall a. a -> Pattern' a
varP (a -> Pattern' a) -> a -> Pattern' a
forall a b. (a -> b) -> a -> b
$ String -> Int -> a
forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar String
n Int
i
deBruijnView :: Pattern' a -> Maybe Int
deBruijnView _ = Maybe Int
forall a. Maybe a
Nothing
fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution :: Substitution' DeBruijnPattern -> Substitution' Term
fromPatternSubstitution = (DeBruijnPattern -> Term)
-> Substitution' DeBruijnPattern -> Substitution' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm
applyPatSubst :: (Subst Term a) => PatternSubstitution -> a -> a
applyPatSubst :: Substitution' DeBruijnPattern -> a -> a
applyPatSubst = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Substitution' Term -> a -> a)
-> (Substitution' DeBruijnPattern -> Substitution' Term)
-> Substitution' DeBruijnPattern
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' DeBruijnPattern -> Substitution' Term
fromPatternSubstitution
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin o :: PatOrigin
o p :: Pattern' a
p = case Pattern' a -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo Pattern' a
p of
Nothing -> Pattern' a
p
Just i :: PatternInfo
i -> PatternInfo -> Pattern' a -> Pattern' a
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo (PatternInfo
i { patOrigin :: PatOrigin
patOrigin = PatOrigin
o }) Pattern' a
p
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo i :: PatternInfo
i p :: Pattern' a
p = case Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p of
Nothing -> Pattern' a
p
Just PatOSplit -> Pattern' a
p
Just PatOAbsurd -> Pattern' a
p
Just _ -> case Pattern' a
p of
(VarP _ x :: a
x) -> PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
i a
x
(DotP _ u :: Term
u) -> PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i Term
u
(ConP c :: ConHead
c (ConPatternInfo _ r :: Bool
r ft :: Bool
ft b :: Maybe (Arg Type)
b l :: Bool
l) ps :: [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 _ q :: QName
q ps :: [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 _ l :: 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 _ t :: Term
t u :: Term
u x :: 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 DeBruijnPattern where
applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern
applySubst IdS p :: DeBruijnPattern
p = DeBruijnPattern
p
applySubst rho :: Substitution' DeBruijnPattern
rho p :: DeBruijnPattern
p = case DeBruijnPattern
p of
VarP i :: PatternInfo
i x :: 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
$
String -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> String
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
Substitution' DeBruijnPattern -> Int -> DeBruijnPattern
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' DeBruijnPattern
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
DotP i :: PatternInfo
i u :: 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
$ Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u
ConP c :: ConHead
c ci :: ConPatternInfo
ci ps :: NAPs
ps -> ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci (NAPs -> DeBruijnPattern) -> NAPs -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho NAPs
ps
DefP i :: PatternInfo
i q :: QName
q ps :: NAPs
ps -> PatternInfo -> QName -> NAPs -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q (NAPs -> DeBruijnPattern) -> NAPs -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho NAPs
ps
LitP i :: PatternInfo
i x :: Literal
x -> DeBruijnPattern
p
ProjP{} -> DeBruijnPattern
p
IApplyP i :: PatternInfo
i t :: Term
t u :: Term
u x :: DBPatVar
x -> case String -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> String
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> Int -> DeBruijnPattern
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' DeBruijnPattern
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x of
IApplyP _ _ _ y :: DBPatVar
y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
t) (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u) DBPatVar
y
VarP _ y :: DBPatVar
y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
t) (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u) DBPatVar
y
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
where
useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
useName :: String -> DeBruijnPattern -> DeBruijnPattern
useName n :: String
n (VarP o :: PatternInfo
o x :: DBPatVar
x)
| String -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (DBPatVar -> String
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 :: String
dbPatVarName = String
n }
useName _ x :: DeBruijnPattern
x = DeBruijnPattern
x
instance Subst Term Range where
applySubst :: Substitution' Term -> Range -> Range
applySubst _ = Range -> Range
forall c. c -> c
id
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply (Projection prop :: Maybe QName
prop d :: QName
d r :: Arg QName
r _ lams :: ProjLams
lams) o :: ProjOrigin
o rel :: Relevance
rel args :: Args
args =
case [Arg String] -> Maybe ([Arg String], Arg String)
forall a. [a] -> Maybe ([a], a)
initLast ([Arg String] -> Maybe ([Arg String], Arg String))
-> [Arg String] -> Maybe ([Arg String], Arg String)
forall a b. (a -> b) -> a -> b
$ ProjLams -> [Arg String]
getProjLams ProjLams
lams of
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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args else Term
forall a. HasCallStack => a
__IMPOSSIBLE__
Just (pars :: [Arg String]
pars, Arg i :: ArgInfo
i y :: String
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
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
y (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var 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
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
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 0 [] Term -> Arg QName -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg QName
r]
(pars' :: [Arg String]
pars', args' :: Args
args') = [Arg String] -> Args -> ([Arg String], Args)
forall a b. [a] -> [b] -> ([a], [b])
dropCommon [Arg String]
pars Args
args
in (Arg String -> Term -> Term) -> Term -> [Arg String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr (\ (Arg ai :: ArgInfo
ai x :: String
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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
x) (Term
core Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
args') [Arg String]
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 { TelV a -> Tele (Dom a)
theTel :: Tele (Dom a), TelV a -> a
theCore :: a }
deriving (Int -> TelV a -> String -> String
[TelV a] -> String -> String
TelV a -> String
(Int -> TelV a -> String -> String)
-> (TelV a -> String)
-> ([TelV a] -> String -> String)
-> Show (TelV a)
forall a. Show a => Int -> TelV a -> String -> String
forall a. Show a => [TelV a] -> String -> String
forall a. Show a => TelV a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TelV a] -> String -> String
$cshowList :: forall a. Show a => [TelV a] -> String -> String
show :: TelV a -> String
$cshow :: forall a. Show a => TelV a -> String
showsPrec :: Int -> TelV a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> TelV a -> String -> String
Show, a -> TelV b -> TelV a
(a -> b) -> TelV a -> TelV b
(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
<$ :: a -> TelV b -> TelV a
$c<$ :: forall a b. a -> TelV b -> TelV a
fmap :: (a -> b) -> TelV a -> TelV b
$cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
Functor)
deriving instance (Subst Term a, Eq a) => Eq (TelV a)
deriving instance (Subst Term a, Ord a) => Ord (TelV a)
telView' :: Type -> TelView
telView' :: Type -> TelView
telView' = Int -> Type -> TelView
telView'UpTo (-1)
telView'UpTo :: Int -> Type -> TelView
telView'UpTo :: Int -> Type -> TelView
telView'UpTo 0 t :: Type
t = Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telView'UpTo n :: Int
n t :: Type
t = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Pi a :: Dom Type
a b :: Abs Type
b -> Dom Type -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> String
forall a. Abs a -> String
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
- 1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
_ -> Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
where
absV :: Dom a -> String -> TelV a -> TelV a
absV a :: Dom a
a x :: String
x (TelV tel :: Tele (Dom a)
tel t :: 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 (String -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. String -> a -> Abs a
Abs String
x Tele (Dom a)
tel)) a
t
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' f :: Name -> a
f [] t :: Dom Type
t = []
bindsToTel' f :: Name -> a
f (x :: Name
x:xs :: [Name]
xs) t :: Dom Type
t = (Type -> (a, Type)) -> Dom Type -> Dom' Term (a, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> a
f Name
x,) Dom Type
t Dom' Term (a, Type) -> ListTel' a -> ListTel' a
forall a. a -> [a] -> [a]
: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f [Name]
xs (Int -> Dom Type -> Dom Type
forall t a. Subst t a => Int -> a -> a
raise 1 Dom Type
t)
bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel :: [Name] -> Dom Type -> [Dom' Term (String, Type)]
bindsToTel = (Name -> String)
-> [Name] -> Dom Type -> [Dom' Term (String, Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> String
nameToArgName
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel [] t :: Type
t = Telescope
forall a. Tele a
EmptyTel
namedBindsToTel (x :: NamedArg Name
x : xs :: [NamedArg Name]
xs) t :: Type
t =
Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
t Type -> Dom' Term () -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Name -> String
nameToArgName (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ [NamedArg Name] -> Type -> Telescope
namedBindsToTel [NamedArg Name]
xs (Int -> Type -> Type
forall t a. Subst t a => Int -> a -> a
raise 1 Type
t)
domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom' Term ()
domFromNamedArgName x :: NamedArg Name
x = () () -> Dom' Term Name -> Dom' Term ()
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 (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 Nothing x :: 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 String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> String -> Ranged String
forall a. Range -> a -> Ranged a
Ranged (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x) (String -> Ranged String) -> String -> Ranged String
forall a b. (a -> b) -> a -> b
$ Name -> String
nameToArgName Name
x) Name
x
forceName x :: Named NamedName Name
x = Named NamedName Name
x
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi :: Dom' Term (String, Type) -> Type -> Type
mkPi !Dom' Term (String, Type)
dom b :: Type
b = Term -> Type
forall a. a -> Type'' Term a
el (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a (String -> Type -> Abs Type
forall t a. (Subst t a, Free a) => String -> a -> Abs a
mkAbs String
x Type
b)
where
x :: String
x = (String, Type) -> String
forall a b. (a, b) -> a
fst ((String, Type) -> String) -> (String, Type) -> String
forall a b. (a -> b) -> a -> b
$ Dom' Term (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (String, Type)
dom
a :: Dom Type
a = (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
dom
el :: a -> Type'' Term a
el = Sort -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> a -> Type'' Term a) -> Sort -> a -> Type'' Term a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort Dom Type
a (String -> Sort -> Abs Sort
forall a. String -> a -> Abs a
Abs String
x (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
b))
mkLam :: Arg ArgName -> Term -> Term
mkLam :: Arg String -> Term -> Term
mkLam a :: Arg String
a v :: Term
v = ArgInfo -> Abs Term -> Term
Lam (Arg String -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg String
a) (String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs (Arg String -> String
forall e. Arg e -> e
unArg Arg String
a) Term
v)
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' reAbs :: Abs Type -> Abs Type
reAbs = Telescope -> Type -> Type
telePi where
telePi :: Telescope -> Type -> Type
telePi EmptyTel t :: Type
t = Type
t
telePi (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: Type
t = Term -> Type
forall a. a -> Type'' Term a
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 = (Telescope -> Type -> Type
`telePi` Type
t) (Telescope -> Type) -> Abs Telescope -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel
el :: a -> Type'' Term a
el = Sort -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> a -> Type'' Term a) -> Sort -> a -> Type'' Term a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort Dom Type
u (Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Abs Type -> Abs Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
telePi :: Telescope -> Type -> Type
telePi :: Telescope -> Type -> Type
telePi = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' Abs Type -> Abs Type
forall t a. (Subst t a, Free a) => Abs a -> Abs a
reAbs
telePi_ :: Telescope -> Type -> Type
telePi_ :: Telescope -> Type -> Type
telePi_ = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' Abs Type -> Abs Type
forall c. c -> c
id
telePiVisible :: Telescope -> Type -> Type
telePiVisible :: Telescope -> Type -> Type
telePiVisible EmptyTel t :: Type
t = Type
t
telePiVisible (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: Type
t
| Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Dom Type
u, NoAbs x :: String
x t' :: Type
t' <- Abs Type
b' = Type
t'
| Bool
otherwise = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Sort -> Sort
piSort Dom Type
u (Abs Sort -> Sort) -> Abs Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Abs Type -> Abs Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Telescope
tel Abs Telescope -> (Telescope -> Type) -> Abs Type
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Telescope -> Type -> Type
`telePiVisible` Type
t)
b' :: Abs Type
b' = Abs Type -> Abs Type
forall t a. (Subst t a, Free a) => Abs a -> Abs a
reAbs Abs Type
b
teleLam :: Telescope -> Term -> Term
teleLam :: Telescope -> Term -> Term
teleLam EmptyTel t :: Term
t = Term
t
teleLam (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: 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
$ (Telescope -> Term -> Term) -> Term -> Telescope -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope -> Term -> Term
teleLam Term
t (Telescope -> Term) -> Abs Telescope -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel
class TeleNoAbs a where
teleNoAbs :: a -> Term -> Term
instance TeleNoAbs ListTel where
teleNoAbs :: [Dom' Term (String, Type)] -> Term -> Term
teleNoAbs tel :: [Dom' Term (String, Type)]
tel t :: Term
t = (Dom' Term (String, Type) -> Term -> Term)
-> Term -> [Dom' Term (String, Type)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (x :: String
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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
x) Term
t [Dom' Term (String, Type)]
tel
instance TeleNoAbs Telescope where
teleNoAbs :: Telescope -> Term -> Term
teleNoAbs tel :: Telescope
tel = [Dom' Term (String, Type)] -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs ([Dom' Term (String, Type)] -> Term -> Term)
-> [Dom' Term (String, Type)] -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel _ [] = [Dom Type] -> Maybe [Dom Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeArgsWithTel (ExtendTel dom :: Dom Type
dom tel :: Abs Telescope
tel) (v :: Term
v : vs :: [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
<$> Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel (Abs Telescope -> Term -> Telescope
forall t a. Subst t a => Abs a -> t -> a
absApp Abs Telescope
tel Term
v) [Term]
vs
typeArgsWithTel EmptyTel{} (_:_) = Maybe [Dom Type]
forall a. Maybe a
Nothing
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody cl :: Clause
cl = Substitution' Term -> Maybe Term -> Maybe Term
forall t a. Subst t a => Substitution' t -> 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 Candidate
deriving instance (Subst t a, Eq a) => Eq (Tele a)
deriving instance (Subst t a, Ord a) => Ord (Tele a)
deriving instance Eq CompareAs
deriving instance Eq Section
instance Ord PlusLevel where
compare :: PlusLevel' Term -> PlusLevel' Term -> Ordering
compare (Plus n :: Integer
n a :: LevelAtom' Term
a) (Plus m :: Integer
m b :: LevelAtom' Term
b) = (LevelAtom' Term, Integer)
-> (LevelAtom' Term, Integer) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LevelAtom' Term
a,Integer
n) (LevelAtom' Term
b,Integer
m)
instance Eq LevelAtom where
== :: LevelAtom' Term -> LevelAtom' Term -> Bool
(==) = Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Term -> Term -> Bool)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> LevelAtom' Term
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LevelAtom' Term -> Term
unLevelAtom
instance Ord LevelAtom where
compare :: LevelAtom' Term -> LevelAtom' Term -> Ordering
compare = Term -> Term -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term -> Term -> Ordering)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> LevelAtom' Term
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LevelAtom' Term -> Term
unLevelAtom
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 x :: Int
x vs :: Elims
vs == :: Term -> Term -> Bool
== Var x' :: Int
x' vs' :: 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 h :: ArgInfo
h v :: Abs Term
v == Lam h' :: ArgInfo
h' v' :: 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 l :: Literal
l == Lit l' :: Literal
l' = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
Def x :: QName
x vs :: Elims
vs == Def x' :: QName
x' vs' :: 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 x :: ConHead
x _ vs :: Elims
vs == Con x' :: ConHead
x' _ vs' :: 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 a :: Dom Type
a b :: Abs Type
b == Pi a' :: Dom Type
a' b' :: 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 s :: Sort
s == Sort s' :: Sort
s' = Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s'
Level l :: Level
l == Level l' :: Level
l' = Level
l Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
l'
MetaV m :: MetaId
m vs :: Elims
vs == MetaV m' :: MetaId
m' vs' :: 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 _ == DontCare _ = Bool
True
Dummy{} == Dummy{} = Bool
True
_ == _ = Bool
False
instance Eq a => Eq (Pattern' a) where
VarP _ x :: a
x == :: Pattern' a -> Pattern' a -> Bool
== VarP _ y :: a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
DotP _ u :: Term
u == DotP _ v :: Term
v = Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v
ConP c :: ConHead
c _ ps :: [NamedArg (Pattern' a)]
ps == ConP c' :: ConHead
c' _ qs :: [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 _ l :: Literal
l == LitP _ l' :: Literal
l' = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
ProjP _ f :: QName
f == ProjP _ g :: QName
g = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g
IApplyP _ u :: Term
u v :: Term
v x :: a
x == IApplyP _ u' :: Term
u' v' :: Term
v' y :: 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 _ f :: QName
f ps :: [NamedArg (Pattern' a)]
ps == DefP _ g :: QName
g qs :: [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
_ == _ = Bool
False
instance Ord Term where
Var a :: Int
a b :: Elims
b compare :: Term -> Term -> Ordering
`compare` Var x :: Int
x y :: Elims
y = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
x Int
a Ordering -> Ordering -> Ordering
`thenCmp` Elims -> Elims -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Elims
b Elims
y
Var{} `compare` _ = Ordering
LT
_ `compare` Var{} = Ordering
GT
Def a :: QName
a b :: Elims
b `compare` Def x :: QName
x y :: 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` _ = Ordering
LT
_ `compare` Def{} = Ordering
GT
Con a :: ConHead
a _ b :: Elims
b `compare` Con x :: ConHead
x _ y :: 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` _ = Ordering
LT
_ `compare` Con{} = Ordering
GT
Lit a :: Literal
a `compare` Lit x :: Literal
x = Literal -> Literal -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Literal
a Literal
x
Lit{} `compare` _ = Ordering
LT
_ `compare` Lit{} = Ordering
GT
Lam a :: ArgInfo
a b :: Abs Term
b `compare` Lam x :: ArgInfo
x y :: 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` _ = Ordering
LT
_ `compare` Lam{} = Ordering
GT
Pi a :: Dom Type
a b :: Abs Type
b `compare` Pi x :: Dom Type
x y :: 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` _ = Ordering
LT
_ `compare` Pi{} = Ordering
GT
Sort a :: Sort
a `compare` Sort x :: Sort
x = Sort -> Sort -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Sort
a Sort
x
Sort{} `compare` _ = Ordering
LT
_ `compare` Sort{} = Ordering
GT
Level a :: Level
a `compare` Level x :: Level
x = Level -> Level -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Level
a Level
x
Level{} `compare` _ = Ordering
LT
_ `compare` Level{} = Ordering
GT
MetaV a :: MetaId
a b :: Elims
b `compare` MetaV x :: MetaId
x y :: 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` _ = Ordering
LT
_ `compare` MetaV{} = Ordering
GT
DontCare{} `compare` DontCare{} = Ordering
EQ
DontCare{} `compare` _ = Ordering
LT
_ `compare` DontCare{} = Ordering
GT
Dummy{} `compare` Dummy{} = Ordering
EQ
instance (Subst t a, Eq a) => Eq (Abs a) where
NoAbs _ a :: a
a == :: Abs a -> Abs a -> Bool
== NoAbs _ b :: a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
a :: Abs a
a == b :: Abs a
b = Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
b
instance (Subst t a, Ord a) => Ord (Abs a) where
NoAbs _ a :: a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs _ b :: a
b = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
a :: Abs a
a `compare` b :: Abs a
b = Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
b
deriving instance Ord a => Ord (Dom a)
instance (Subst t a, Eq a) => Eq (Elim' a) where
Apply a :: Arg a
a == :: Elim' a -> Elim' a -> Bool
== Apply b :: Arg a
b = Arg a
a Arg a -> Arg a -> Bool
forall a. Eq a => a -> a -> Bool
== Arg a
b
Proj _ x :: QName
x == Proj _ y :: QName
y = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
IApply x :: a
x y :: a
y r :: a
r == IApply x' :: a
x' y' :: a
y' r' :: 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'
_ == _ = Bool
False
instance (Subst t a, Ord a) => Ord (Elim' a) where
Apply a :: Arg a
a compare :: Elim' a -> Elim' a -> Ordering
`compare` Apply b :: Arg a
b = Arg a
a Arg a -> Arg a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Arg a
b
Proj _ x :: QName
x `compare` Proj _ y :: QName
y = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
IApply x :: a
x y :: a
y r :: a
r `compare` IApply x' :: a
x' y' :: a
y' r' :: 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` _ = Ordering
LT
_ `compare` Apply{} = Ordering
GT
Proj{} `compare` _ = Ordering
LT
_ `compare` Proj{} = Ordering
GT
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' univInf :: Maybe Sort
univInf (Type l :: Level
l) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' univInf :: Maybe Sort
univInf (Prop l :: Level
l) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' univInf :: Maybe Sort
univInf Inf = Maybe Sort
univInf
univSort' univInf :: Maybe Sort
univInf s :: Sort
s = Maybe Sort
forall a. Maybe a
Nothing
univSort :: Maybe Sort -> Sort -> Sort
univSort :: Maybe Sort -> Sort -> Sort
univSort univInf :: Maybe Sort
univInf s :: Sort
s = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Maybe Sort -> Sort -> Maybe Sort
univSort' Maybe Sort
univInf Sort
s
univInf :: (HasOptions m) => m (Maybe Sort)
univInf :: m (Maybe Sort)
univInf =
m Bool -> m (Maybe Sort) -> m (Maybe Sort) -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((PragmaOptions -> Bool
optOmegaInOmega (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType)
(Maybe Sort -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Sort -> m (Maybe Sort)) -> Maybe Sort -> m (Maybe Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf)
(Maybe Sort -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Sort
forall a. Maybe a
Nothing)
funSort' :: Sort -> Sort -> Maybe Sort
funSort' :: Sort -> Sort -> Maybe Sort
funSort' a :: Sort
a b :: Sort
b = case (Sort
a, Sort
b) of
(Inf , _ ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
(_ , Inf ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
(Type a :: Level
a , Type b :: Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
(SizeUniv , b :: Sort
b ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
b
(_ , SizeUniv ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
SizeUniv
(Prop a :: Level
a , Type b :: Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
(Type a :: Level
a , Prop b :: Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
(Prop a :: Level
a , Prop b :: Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
(a :: Sort
a , b :: Sort
b ) -> Maybe Sort
forall a. Maybe a
Nothing
funSort :: Sort -> Sort -> Sort
funSort :: Sort -> Sort -> Sort
funSort a :: Sort
a b :: Sort
b = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
a Sort
b) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Maybe Sort
funSort' Sort
a Sort
b
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' a :: Dom Type
a (NoAbs _ b :: Sort
b) = Sort -> Sort -> Maybe Sort
funSort' (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) Sort
b
piSort' a :: Dom Type
a bAbs :: Abs Sort
bAbs@(Abs _ b :: Sort
b) = case Int -> Sort -> Maybe (FlexRig' ())
forall a. Free a => Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn 0 Sort
b of
Nothing -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Empty -> Abs Sort -> Sort
forall t a. Subst t a => Empty -> Abs a -> a
noabsApp Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Sort
bAbs
Just o :: FlexRig' ()
o -> case FlexRig' ()
o of
StronglyRigid -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
Unguarded -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
WeaklyRigid -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
Flexible _ -> Maybe Sort
forall a. Maybe a
Nothing
piSort :: Dom Type -> Abs Sort -> Sort
piSort :: Dom Type -> Abs Sort -> Sort
piSort a :: Dom Type
a b :: Abs Sort
b = case Dom Type -> Abs Sort -> Maybe Sort
piSort' Dom Type
a Abs Sort
b of
Just s :: Sort
s -> Sort
s
Nothing | NoAbs _ b' :: Sort
b' <- Abs Sort
b -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) Sort
b'
| Bool
otherwise -> Dom Type -> Abs Sort -> Sort
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort Dom Type
a Abs Sort
b
levelMax :: Integer -> [PlusLevel] -> Level
levelMax :: Integer -> [PlusLevel' Term] -> Level
levelMax n0 :: Integer
n0 as0 :: [PlusLevel' Term]
as0 = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n [PlusLevel' Term]
as
where
Max n1 :: Integer
n1 as1 :: [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
as2 :: [PlusLevel' Term]
as2 = [PlusLevel' Term] -> [PlusLevel' Term]
forall t. Eq (LevelAtom' t) => [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [PlusLevel' Term]
as1
as :: [PlusLevel' Term]
as = [PlusLevel' Term] -> [PlusLevel' Term]
forall a. Ord a => [a] -> [a]
List.sort [PlusLevel' Term]
as2
greatestB :: Integer
greatestB = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ 0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [ Integer
n | Plus n :: Integer
n _ <- [PlusLevel' Term]
as ]
n :: Integer
n | Integer
n1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
greatestB = Integer
n1
| Bool
otherwise = 0
lmax :: Integer -> [PlusLevel] -> [Level] -> Level
lmax :: Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax m :: Integer
m as :: [PlusLevel' Term]
as [] = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m [PlusLevel' Term]
as
lmax m :: Integer
m as :: [PlusLevel' Term]
as (Max n :: Integer
n bs :: [PlusLevel' Term]
bs : ls :: [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 m :: Integer
m as :: [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 m :: Integer
m l :: LevelAtom' Term
l) = Integer -> Level -> Level
levelPlus Integer
m (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ LevelAtom' Term -> Level
expandAtom LevelAtom' Term
l
expandAtom :: LevelAtom -> Level
expandAtom :: LevelAtom' Term -> Level
expandAtom l :: LevelAtom' Term
l = case LevelAtom' Term
l of
BlockedLevel _ v :: Term
v -> Term -> Level
expandTm Term
v
NeutralLevel _ v :: Term
v -> Term -> Level
expandTm Term
v
UnreducedLevel v :: Term
v -> Term -> Level
expandTm Term
v
MetaLevel{} -> Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max 0 [Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus 0 LevelAtom' Term
l]
where
expandTm :: Term -> Level
expandTm (Level l :: Level
l) = Level -> Level
expandLevel Level
l
expandTm (Sort (Type l :: Level
l)) = Level -> Level
expandLevel Level
l
expandTm v :: Term
v = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max 0 [Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus 0 LevelAtom' Term
l]
removeSubsumed :: [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [] = []
removeSubsumed (Plus n :: Integer
n a :: LevelAtom' t
a : bs :: [PlusLevel' t]
bs)
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
ns = [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [PlusLevel' t]
bs
| Bool
otherwise = Integer -> LevelAtom' t -> PlusLevel' t
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
n LevelAtom' t
a PlusLevel' t -> [PlusLevel' t] -> [PlusLevel' t]
forall a. a -> [a] -> [a]
: [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [ PlusLevel' t
b | b :: PlusLevel' t
b@(Plus _ a' :: LevelAtom' t
a') <- [PlusLevel' t]
bs, LevelAtom' t
a LevelAtom' t -> LevelAtom' t -> Bool
forall a. Eq a => a -> a -> Bool
/= LevelAtom' t
a' ]
where
ns :: [Integer]
ns = [ Integer
m | Plus m :: Integer
m a' :: LevelAtom' t
a' <- [PlusLevel' t]
bs, LevelAtom' t
a LevelAtom' t -> LevelAtom' t -> Bool
forall a. Eq a => a -> a -> Bool
== LevelAtom' t
a', Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n ]
levelLub :: Level -> Level -> Level
levelLub :: Level -> Level -> Level
levelLub (Max m :: Integer
m as :: [PlusLevel' Term]
as) (Max n :: Integer
n bs :: [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 l :: Level
l =
case Level
l of
Max 0 [Plus 0 l :: LevelAtom' Term
l] -> LevelAtom' Term -> Term
unLevelAtom LevelAtom' Term
l
_ -> Level -> Term
Level Level
l
unLevelAtom :: LevelAtom -> Term
unLevelAtom :: LevelAtom' Term -> Term
unLevelAtom (MetaLevel x :: MetaId
x es :: Elims
es) = MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
unLevelAtom (NeutralLevel _ v :: Term
v) = Term
v
unLevelAtom (UnreducedLevel v :: Term
v) = Term
v
unLevelAtom (BlockedLevel _ v :: Term
v) = Term
v