{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.DisplayForm (displayForm) where
import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe
import Data.Monoid (All(..))
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
import Agda.Syntax.Scope.Base (inverseScopeLookupName)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Level
import Agda.TypeChecking.Reduce (instantiate)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Syntax.Common.Pretty
import Agda.Utils.Impossible
displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
displayFormArities :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Nat]
displayFormArities QName
q = forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForm -> [Elim]
dfPats forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Decoration t => t a -> a
dget) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Open DisplayForm]
getDisplayForms QName
q
liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
liftLocalDisplayForm Substitution
IdS DisplayForm
df = forall a. a -> Maybe a
Just DisplayForm
df
liftLocalDisplayForm (Wk Nat
n Substitution
IdS) (Display Nat
m [Elim]
lhs DisplayTerm
rhs) =
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> [Elim] -> DisplayTerm -> DisplayForm
Display (Nat
n forall a. Num a => a -> a -> a
+ Nat
m) [Elim]
lhs DisplayTerm
rhs
liftLocalDisplayForm Substitution
_ DisplayForm
_ = forall a. Maybe a
Nothing
type MonadDisplayForm m =
( MonadReduce m
, ReadTCState m
, HasConstInfo m
, HasBuiltins m
, MonadDebug m
)
displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
displayForm :: forall (m :: * -> *).
MonadDisplayForm m =>
QName -> [Elim] -> m (Maybe DisplayTerm)
displayForm QName
q [Elim]
es = do
[Open DisplayForm]
odfs <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Open DisplayForm]
getDisplayForms QName
q
if (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Open DisplayForm]
odfs) then do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.display.top" Nat
101 forall a b. (a -> b) -> a -> b
$ [Char]
"no displayForm for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
q
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
else do
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.display.top" Nat
100 forall a b. (a -> b) -> a -> b
$ do
Map CheckpointId Substitution
cps <- forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC Lens' TCEnv (Map CheckpointId Substitution)
eCheckpoints
Telescope
cxt <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
[ Doc Aspects
"displayForm for" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty QName
q
, forall a. Nat -> Doc a -> Doc a
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc Aspects
"cxt =" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty Telescope
cxt
, forall a. Nat -> Doc a -> Doc a
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc Aspects
"cps =" forall a. Doc a -> Doc a -> Doc a
<+> forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc Aspects
pretty (forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
cps))
, forall a. Nat -> Doc a -> Doc a
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc Aspects
"dfs =" forall a. Doc a -> Doc a -> Doc a
<+> forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc Aspects
pretty [Open DisplayForm]
odfs) ]
[DisplayForm]
dfs <- forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a (m :: * -> *).
(TermSubst a, ReadTCState m, MonadTCEnv m) =>
(Substitution -> a -> Maybe a) -> Open a -> m (Maybe a)
tryGetOpen Substitution -> DisplayForm -> Maybe DisplayForm
liftLocalDisplayForm) [Open DisplayForm]
odfs
ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
[DisplayTerm]
ms <- do
[Maybe (DisplayForm, DisplayTerm)]
ms <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *).
MonadDisplayForm m =>
DisplayForm -> [Elim] -> MaybeT m (DisplayForm, DisplayTerm)
`matchDisplayForm` [Elim]
es)) [DisplayForm]
dfs
forall (m :: * -> *) a. Monad m => a -> m a
return [ DisplayTerm
m | Just (DisplayForm
d, DisplayTerm
m) <- [Maybe (DisplayForm, DisplayTerm)]
ms, ScopeInfo -> DisplayForm -> Bool
wellScoped ScopeInfo
scope DisplayForm
d ]
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.display.top" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
[ Doc Aspects
"name :" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty QName
q
, Doc Aspects
"displayForms:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty [DisplayForm]
dfs
, Doc Aspects
"arguments :" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty [Elim]
es
, Doc Aspects
"matches :" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty [DisplayTerm]
ms
, Doc Aspects
"result :" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty (forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms)
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms
where
wellScoped :: ScopeInfo -> DisplayForm -> Bool
wellScoped ScopeInfo
scope (Display Nat
_ [Elim]
_ DisplayTerm
d)
| DisplayTerm -> Bool
isWithDisplay DisplayTerm
d = Bool
True
| Bool
otherwise = All -> Bool
getAll forall a b. (a -> b) -> a -> b
$ forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> QName -> Bool
inScope ScopeInfo
scope) DisplayTerm
d
inScope :: ScopeInfo -> QName -> Bool
inScope ScopeInfo
scope QName
x = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ QName -> ScopeInfo -> [QName]
inverseScopeLookupName QName
x ScopeInfo
scope
isWithDisplay :: DisplayTerm -> Bool
isWithDisplay DWithApp{} = Bool
True
isWithDisplay DisplayTerm
_ = Bool
False
matchDisplayForm :: MonadDisplayForm m
=> DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
matchDisplayForm :: forall (m :: * -> *).
MonadDisplayForm m =>
DisplayForm -> [Elim] -> MaybeT m (DisplayForm, DisplayTerm)
matchDisplayForm d :: DisplayForm
d@(Display Nat
n [Elim]
ps DisplayTerm
v) [Elim]
es
| forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
ps forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
es = forall (m :: * -> *) a. MonadPlus m => m a
mzero
| Bool
otherwise = do
let ([Elim]
es0, [Elim]
es1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
ps) [Elim]
es
MatchResult
mm <- forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match (Nat -> Nat -> Window
Window Nat
0 Nat
n) [Elim]
ps [Elim]
es0
[WithOrigin Term]
us <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Nat
0 .. Nat
n forall a. Num a => a -> a -> a
- Nat
1] forall a b. (a -> b) -> a -> b
$ \ Nat
i -> do
Just WithOrigin Term
u <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nat
i MatchResult
mm
forall (m :: * -> *) a. Monad m => a -> m a
return WithOrigin Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForm
d, forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin (forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. WithOrigin a -> a
woThing [WithOrigin Term]
us) [WithOrigin Term]
us DisplayTerm
v forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es1)
type MatchResult = Map Int (WithOrigin Term)
unionMatch :: Monad m => MatchResult -> MatchResult -> MaybeT m MatchResult
unionMatch :: forall (m :: * -> *).
Monad m =>
MatchResult -> MatchResult -> MaybeT m MatchResult
unionMatch MatchResult
m1 MatchResult
m2
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection MatchResult
m1 MatchResult
m2) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union MatchResult
m1 MatchResult
m2
| Bool
otherwise = forall (m :: * -> *) a. MonadPlus m => m a
mzero
unionsMatch :: Monad m => [MatchResult] -> MaybeT m MatchResult
unionsMatch :: forall (m :: * -> *).
Monad m =>
[MatchResult] -> MaybeT m MatchResult
unionsMatch = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *).
Monad m =>
MatchResult -> MatchResult -> MaybeT m MatchResult
unionMatch forall k a. Map k a
Map.empty
data Window = Window {Window -> Nat
dbLo, Window -> Nat
dbHi :: Nat}
inWindow :: Window -> Nat -> Maybe Nat
inWindow :: Window -> Nat -> Maybe Nat
inWindow (Window Nat
lo Nat
hi) Nat
n | Nat
lo forall a. Ord a => a -> a -> Bool
<= Nat
n, Nat
n forall a. Ord a => a -> a -> Bool
< Nat
hi = forall a. a -> Maybe a
Just (Nat
n forall a. Num a => a -> a -> a
- Nat
lo)
| Bool
otherwise = forall a. Maybe a
Nothing
shiftWindow :: Window -> Window
shiftWindow :: Window -> Window
shiftWindow (Window Nat
lo Nat
hi) = Nat -> Nat -> Window
Window (Nat
lo forall a. Num a => a -> a -> a
+ Nat
1) (Nat
hi forall a. Num a => a -> a -> a
+ Nat
1)
class Match a where
match :: MonadDisplayForm m => Window -> a -> a -> MaybeT m MatchResult
instance Match a => Match [a] where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> [a] -> [a] -> MaybeT m MatchResult
match Window
n [a]
xs [a]
ys = forall (m :: * -> *).
Monad m =>
[MatchResult] -> MaybeT m MatchResult
unionsMatch forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
n) [a]
xs [a]
ys
instance Match a => Match (Arg a) where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Arg a -> Arg a -> MaybeT m MatchResult
match Window
n Arg a
p Arg a
v = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. LensOrigin a => Origin -> a -> a
setOrigin (forall a. LensOrigin a => a -> Origin
getOrigin Arg a
v)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
n (forall e. Arg e -> e
unArg Arg a
p) (forall e. Arg e -> e
unArg Arg a
v)
instance Match a => Match (Elim' a) where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Elim' a -> Elim' a -> MaybeT m MatchResult
match Window
n Elim' a
p Elim' a
v =
case (Elim' a
p, Elim' a
v) of
(Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') | QName
f forall a. Eq a => a -> a -> Bool
== QName
f' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty
(Elim' a, Elim' a)
_ | Just Arg a
a <- forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
p
, Just Arg a
a' <- forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
v -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
n Arg a
a Arg a
a'
(Elim' a, Elim' a)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
instance Match Term where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Term -> Term -> MaybeT m MatchResult
match Window
w Term
p Term
v = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Term
v -> case (Term -> Term
unSpine Term
p, Term -> Term
unSpine Term
v) of
(Var Nat
i [], Term
v) | Just Nat
j <- Window -> Nat -> Maybe Nat
inWindow Window
w Nat
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Nat
j (forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted Term
v)
(Var Nat
i (Elim
_:[Elim]
_), Term
v) | Just{} <- Window -> Nat -> Maybe Nat
inWindow Window
w Nat
i -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
(Var Nat
i [Elim]
ps, Var Nat
j [Elim]
vs) | Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
(Def QName
c [Elim]
ps, Def QName
d [Elim]
vs) | QName
c forall a. Eq a => a -> a -> Bool
== QName
d -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
(Con ConHead
c ConInfo
_ [Elim]
ps, Con ConHead
d ConInfo
_ [Elim]
vs) | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
d -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
(Lit Literal
l, Lit Literal
l') | Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty
(Lam ArgInfo
h Abs Term
p, Lam ArgInfo
h' Abs Term
v) | ArgInfo
h forall a. Eq a => a -> a -> Bool
== ArgInfo
h' -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match (Window -> Window
shiftWindow Window
w) (forall a. Abs a -> a
unAbs Abs Term
p) (forall a. Abs a -> a
unAbs Abs Term
v)
(Term
p, Term
v) | Term
p forall a. Eq a => a -> a -> Bool
== Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty
(Term
p, Level Level
l) -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w Term
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
(Sort Sort
ps, Sort Sort
pv) -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w Sort
ps Sort
pv
(Term
p, Sort (Type Level
v)) -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w Term
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
(Term, Term)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
instance Match Sort where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Sort -> Sort -> MaybeT m MatchResult
match Window
w Sort
p Sort
v = case (Sort
p, Sort
v) of
(Type Level
pl, Type Level
vl) -> forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w Level
pl Level
vl
(Sort, Sort)
_ | Sort
p forall a. Eq a => a -> a -> Bool
== Sort
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty
(Sort, Sort)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
instance Match Level where
match :: forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Level -> Level -> MaybeT m MatchResult
match Window
w Level
p Level
v = do
Term
p <- forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
p
Term
v <- forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
match Window
w Term
p Term
v
class SubstWithOrigin a where
substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a
instance SubstWithOrigin a => SubstWithOrigin [a] where
substWithOrigin :: Substitution -> [WithOrigin Term] -> [a] -> [a]
substWithOrigin Substitution
rho [WithOrigin Term]
ots = forall a b. (a -> b) -> [a] -> [b]
map (forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots)
instance (SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) where
substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a
substWithOrigin Substitution
rho [WithOrigin Term]
ots (Apply Arg a
arg) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Arg a
arg
substWithOrigin Substitution
rho [WithOrigin Term]
ots e :: Elim' a
e@Proj{} = Elim' a
e
substWithOrigin Substitution
rho [WithOrigin Term]
ots (IApply a
u a
v a
w) = forall a. a -> a -> a -> Elim' a
IApply
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots a
u)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots a
v)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots a
w)
instance SubstWithOrigin (Arg Term) where
substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
substWithOrigin Substitution
rho [WithOrigin Term]
ots (Arg ArgInfo
ai Term
v) =
case Term
v of
Var Nat
x [] -> case [WithOrigin Term]
ots forall a. [a] -> Nat -> Maybe a
!!! Nat
x of
Just (WithOrigin Origin
o Term
u) -> forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensOrigin a => (Origin -> Origin) -> a -> a
mapOrigin (Origin -> Origin -> Origin
replaceOrigin Origin
o) ArgInfo
ai) Term
u
Maybe (WithOrigin Term)
Nothing -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v
Con ConHead
c ConInfo
ci [Elim]
args -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
args
Def QName
q [Elim]
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
Term
_ -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v
where
replaceOrigin :: Origin -> Origin -> Origin
replaceOrigin Origin
_ Origin
UserWritten = Origin
UserWritten
replaceOrigin Origin
o Origin
_ = Origin
o
instance SubstWithOrigin Term where
substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v =
case Term
v of
Con ConHead
c ConInfo
ci [Elim]
args -> ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
args
Def QName
q [Elim]
es -> QName -> [Elim] -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
Term
_ -> forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v
instance SubstWithOrigin DisplayTerm where
substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
substWithOrigin Substitution
rho [WithOrigin Term]
ots =
\case
DTerm' Term
v [Elim]
es -> Term -> [Elim] -> DisplayTerm
DTerm' (forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v) forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
DDot' Term
v [Elim]
es -> Term -> [Elim] -> DisplayTerm
DDot' (forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v) forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
DDef QName
q [Elim' DisplayTerm]
es -> QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
q forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim' DisplayTerm]
es
DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
args -> ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Arg DisplayTerm]
args
DWithApp DisplayTerm
t [DisplayTerm]
ts [Elim]
es -> DisplayTerm -> [DisplayTerm] -> [Elim] -> DisplayTerm
DWithApp
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots DisplayTerm
t)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [DisplayTerm]
ts)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)
instance SubstWithOrigin (Arg DisplayTerm) where
substWithOrigin :: Substitution
-> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm
substWithOrigin Substitution
rho [WithOrigin Term]
ots (Arg ArgInfo
ai DisplayTerm
dt) =
case DisplayTerm
dt of
DTerm' Term
v [Elim]
es -> forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Term -> [Elim] -> DisplayTerm
`DTerm'` forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)
DDot' Term
v [Elim]
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term -> [Elim] -> DisplayTerm
DDot' (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v) forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
DDef QName
q [Elim' DisplayTerm]
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
q forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim' DisplayTerm]
es
DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
args -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Arg DisplayTerm]
args
DWithApp DisplayTerm
t [DisplayTerm]
ts [Elim]
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ DisplayTerm -> [DisplayTerm] -> [Elim] -> DisplayTerm
DWithApp
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots DisplayTerm
t)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [DisplayTerm]
ts)
(forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)