{-# LANGUAGE UndecidableInstances #-}  -- for Arg a => Elim' a

-- | Tools for 'DisplayTerm' and 'DisplayForm'.

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

-- | Get the arities of all display forms for a name.
displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
displayFormArities :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Nat]
displayFormArities QName
q = (Open DisplayForm -> Nat) -> [Open DisplayForm] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map ([Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length ([Elim] -> Nat)
-> (Open DisplayForm -> [Elim]) -> Open DisplayForm -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForm -> [Elim]
dfPats (DisplayForm -> [Elim])
-> (Open DisplayForm -> DisplayForm) -> Open DisplayForm -> [Elim]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Open DisplayForm -> DisplayForm
forall (t :: * -> *) a. Decoration t => t a -> a
dget) ([Open DisplayForm] -> [Nat]) -> m [Open DisplayForm] -> m [Nat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m [Open DisplayForm]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Open DisplayForm]
getDisplayForms QName
q

-- | Lift a local display form to an outer context. The substitution goes from the parent context to
--   the context of the local display form (see Issue 958). Current only handles pure extensions of
--   the parent context.
liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
liftLocalDisplayForm Substitution
IdS DisplayForm
df = DisplayForm -> Maybe DisplayForm
forall a. a -> Maybe a
Just DisplayForm
df
liftLocalDisplayForm (Wk Nat
n Substitution
IdS) (Display Nat
m [Elim]
lhs DisplayTerm
rhs) =
  -- We lift a display form by turning matches on free variables into pattern variables, which can
  -- be done by simply adding to the dfPatternVars field.
  DisplayForm -> Maybe DisplayForm
forall a. a -> Maybe a
Just (DisplayForm -> Maybe DisplayForm)
-> DisplayForm -> Maybe DisplayForm
forall a b. (a -> b) -> a -> b
$ Nat -> [Elim] -> DisplayTerm -> DisplayForm
Display (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m) [Elim]
lhs DisplayTerm
rhs
liftLocalDisplayForm Substitution
_ DisplayForm
_ = Maybe DisplayForm
forall a. Maybe a
Nothing

type MonadDisplayForm m =
  ( MonadReduce m
  , ReadTCState m
  , HasConstInfo m
  , HasBuiltins m
  , MonadDebug m
  )

-- | Find a matching display form for @q es@.
--   In essence this tries to rewrite @q es@ with any
--   display form @q ps --> dt@ and returns the instantiated
--   @dt@ if successful.  First match wins.
displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
displayForm :: forall (m :: * -> *).
MonadDisplayForm m =>
QName -> [Elim] -> m (Maybe DisplayTerm)
displayForm QName
q [Elim]
es = do
  -- Get display forms for name q.
  [Open DisplayForm]
odfs  <- QName -> m [Open DisplayForm]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Open DisplayForm]
getDisplayForms QName
q
  if ([Open DisplayForm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Open DisplayForm]
odfs) then do
    [Char] -> Nat -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.display.top" Nat
101 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"no displayForm for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q
    Maybe DisplayTerm -> m (Maybe DisplayTerm)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DisplayTerm
forall a. Maybe a
Nothing
  else do
    -- Display debug info about the @Open@s.
    m () -> m ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> TCM (Doc Aspects) -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.display.top" Nat
100 (TCM (Doc Aspects) -> m ()) -> TCM (Doc Aspects) -> m ()
forall a b. (a -> b) -> a -> b
$ do
      Map CheckpointId Substitution
cps <- Lens' TCEnv (Map CheckpointId Substitution)
-> TCMT IO (Map CheckpointId Substitution)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map CheckpointId Substitution
 -> f (Map CheckpointId Substitution))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId Substitution)
eCheckpoints
      Telescope
cxt <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
        [ Doc Aspects
"displayForm for" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q
        , Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"cxt =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Telescope -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Telescope
cxt
        , Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"cps =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat (((CheckpointId, Substitution) -> Doc Aspects)
-> [(CheckpointId, Substitution)] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (CheckpointId, Substitution) -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Map CheckpointId Substitution -> [(CheckpointId, Substitution)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
cps))
        , Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"dfs =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ((Open DisplayForm -> Doc Aspects)
-> [Open DisplayForm] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map Open DisplayForm -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [Open DisplayForm]
odfs) ]
    -- Use only the display forms that can be opened in the current context.
    [DisplayForm]
dfs   <- [Maybe DisplayForm] -> [DisplayForm]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe DisplayForm] -> [DisplayForm])
-> m [Maybe DisplayForm] -> m [DisplayForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Open DisplayForm -> m (Maybe DisplayForm))
-> [Open DisplayForm] -> m [Maybe DisplayForm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Substitution -> DisplayForm -> Maybe DisplayForm)
-> Open DisplayForm -> m (Maybe DisplayForm)
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 <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    -- Keep the display forms that match the application @q es@.
    [DisplayTerm]
ms <- do
      [Maybe (DisplayForm, DisplayTerm)]
ms <- (DisplayForm -> m (Maybe (DisplayForm, DisplayTerm)))
-> [DisplayForm] -> m [Maybe (DisplayForm, DisplayTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (MaybeT m (DisplayForm, DisplayTerm)
-> m (Maybe (DisplayForm, DisplayTerm))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (DisplayForm, DisplayTerm)
 -> m (Maybe (DisplayForm, DisplayTerm)))
-> (DisplayForm -> MaybeT m (DisplayForm, DisplayTerm))
-> DisplayForm
-> m (Maybe (DisplayForm, DisplayTerm))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DisplayForm -> [Elim] -> MaybeT m (DisplayForm, DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
DisplayForm -> [Elim] -> MaybeT m (DisplayForm, DisplayTerm)
`matchDisplayForm` [Elim]
es)) [DisplayForm]
dfs
      [DisplayTerm] -> m [DisplayTerm]
forall a. a -> m a
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 ]
    -- Not safe when printing non-terminating terms.
    -- (nfdfs, us) <- normalise (dfs, es)
    m () -> m ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> TCM (Doc Aspects) -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.display.top" Nat
100 (TCM (Doc Aspects) -> m ()) -> TCM (Doc Aspects) -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCM (Doc Aspects))
-> Doc Aspects -> TCM (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Doc Aspects
"name        :" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q
      , Doc Aspects
"displayForms:" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [DisplayForm] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [DisplayForm]
dfs
      , Doc Aspects
"arguments   :" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Elim] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [Elim]
es
      , Doc Aspects
"matches     :" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [DisplayTerm] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [DisplayTerm]
ms
      , Doc Aspects
"result      :" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Maybe DisplayTerm -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty ([DisplayTerm] -> Maybe DisplayTerm
forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms)
      ]
    -- Return the first display form that matches.
    Maybe DisplayTerm -> m (Maybe DisplayTerm)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DisplayTerm -> m (Maybe DisplayTerm))
-> Maybe DisplayTerm -> m (Maybe DisplayTerm)
forall a b. (a -> b) -> a -> b
$ [DisplayTerm] -> Maybe DisplayTerm
forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms
  where
    -- Look at the original display form, not the instantiated result when
    -- checking if it's well-scoped. Otherwise we might pick up out of scope
    -- identifiers coming from the source term.
    wellScoped :: ScopeInfo -> DisplayForm -> Bool
wellScoped ScopeInfo
scope (Display Nat
_ [Elim]
_ DisplayTerm
d)
      | DisplayTerm -> Bool
isWithDisplay DisplayTerm
d = Bool
True
      | Bool
otherwise       = All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ (QName -> All) -> DisplayTerm -> All
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All (Bool -> All) -> (QName -> Bool) -> QName -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> QName -> Bool
inScope ScopeInfo
scope) DisplayTerm
d  -- all names in d should be in scope

    inScope :: ScopeInfo -> QName -> Bool
inScope ScopeInfo
scope QName
x = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([QName] -> Bool) -> [QName] -> Bool
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

-- | Match a 'DisplayForm' @q ps = v@ against @q es@.
--   Return the 'DisplayTerm' @v[us]@ if the match was successful,
--   i.e., @es / ps = Just us@.
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
  | [Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
ps Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> [Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
es = MaybeT m (DisplayForm, DisplayTerm)
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  | Bool
otherwise             = do
      let ([Elim]
es0, [Elim]
es1) = Nat -> [Elim] -> ([Elim], [Elim])
forall a. Nat -> [a] -> ([a], [a])
splitAt ([Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
ps) [Elim]
es
      MatchResult
mm <- Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
match (Nat -> Nat -> Window
Window Nat
0 Nat
n) [Elim]
ps [Elim]
es0
      [WithOrigin Term]
us <- [Nat]
-> (Nat -> MaybeT m (WithOrigin Term))
-> MaybeT m [WithOrigin Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Nat
0 .. Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1] ((Nat -> MaybeT m (WithOrigin Term)) -> MaybeT m [WithOrigin Term])
-> (Nat -> MaybeT m (WithOrigin Term))
-> MaybeT m [WithOrigin Term]
forall a b. (a -> b) -> a -> b
$ \ Nat
i -> do
              -- #5294: Fail if we don't have bindings for all variables. This can
              --        happen outside parameterised modules when some of the parameters
              --        are not used in the lhs.
              Just WithOrigin Term
u <- Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term)))
-> Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
forall a b. (a -> b) -> a -> b
$ Nat -> MatchResult -> Maybe (WithOrigin Term)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nat
i MatchResult
mm
              WithOrigin Term -> MaybeT m (WithOrigin Term)
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return WithOrigin Term
u
      (DisplayForm, DisplayTerm) -> MaybeT m (DisplayForm, DisplayTerm)
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForm
d, Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin ([Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ (WithOrigin Term -> Term) -> [WithOrigin Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map WithOrigin Term -> Term
forall a. WithOrigin a -> a
woThing [WithOrigin Term]
us) [WithOrigin Term]
us DisplayTerm
v DisplayTerm -> [Elim] -> DisplayTerm
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
  | MatchResult -> Bool
forall a. Map Nat a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (MatchResult -> MatchResult -> MatchResult
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection MatchResult
m1 MatchResult
m2) = MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchResult -> MaybeT m MatchResult)
-> MatchResult -> MaybeT m MatchResult
forall a b. (a -> b) -> a -> b
$ MatchResult -> MatchResult -> MatchResult
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union MatchResult
m1 MatchResult
m2
  | Bool
otherwise = MaybeT m MatchResult
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero  -- Non-linear pattern, fail for now.

unionsMatch :: Monad m => [MatchResult] -> MaybeT m MatchResult
unionsMatch :: forall (m :: * -> *).
Monad m =>
[MatchResult] -> MaybeT m MatchResult
unionsMatch = (MatchResult -> MatchResult -> MaybeT m MatchResult)
-> MatchResult -> [MatchResult] -> MaybeT m MatchResult
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM MatchResult -> MatchResult -> MaybeT m MatchResult
forall (m :: * -> *).
Monad m =>
MatchResult -> MatchResult -> MaybeT m MatchResult
unionMatch MatchResult
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 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
n, Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
hi = Nat -> Maybe Nat
forall a. a -> Maybe a
Just (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
lo)
                          | Bool
otherwise       = Maybe Nat
forall a. Maybe a
Nothing

shiftWindow :: Window -> Window
shiftWindow :: Window -> Window
shiftWindow (Window Nat
lo Nat
hi) = Nat -> Nat -> Window
Window (Nat
lo Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (Nat
hi Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)

-- | Class @Match@ for matching a term @p@ in the role of a pattern
--   against a term @v@.
--
--   Free variables inside the window in @p@ are pattern variables and
--   the result of matching is a map from pattern variables (shifted down to start at 0) to subterms
--   of @v@.
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 = [MatchResult] -> MaybeT m MatchResult
forall (m :: * -> *).
Monad m =>
[MatchResult] -> MaybeT m MatchResult
unionsMatch ([MatchResult] -> MaybeT m MatchResult)
-> MaybeT m [MatchResult] -> MaybeT m MatchResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> a -> MaybeT m MatchResult)
-> [a] -> [a] -> MaybeT m [MatchResult]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Window -> a -> a -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
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 = (WithOrigin Term -> WithOrigin Term) -> MatchResult -> MatchResult
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Origin -> WithOrigin Term -> WithOrigin Term
forall a. LensOrigin a => Origin -> a -> a
setOrigin (Arg a -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin Arg a
v)) (MatchResult -> MatchResult)
-> MaybeT m MatchResult -> MaybeT m MatchResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Window -> a -> a -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> a -> a -> MaybeT m MatchResult
match Window
n (Arg a -> a
forall e. Arg e -> e
unArg Arg a
p) (Arg a -> a
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 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return MatchResult
forall k a. Map k a
Map.empty
      (Elim' a, Elim' a)
_ | Just Arg a
a  <- Elim' a -> Maybe (Arg a)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
p
        , Just Arg a
a' <- Elim' a -> Maybe (Arg a)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
v    -> Window -> Arg a -> Arg a -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Arg a -> Arg a -> MaybeT m MatchResult
match Window
n Arg a
a Arg a
a'
      -- we do not care to differentiate between Apply and IApply for
      -- printing.
      (Elim' a, Elim' a)
_                               -> MaybeT m MatchResult
forall a. MaybeT m 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 = m Term -> MaybeT m Term
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v) MaybeT m Term
-> (Term -> MaybeT m MatchResult) -> MaybeT m MatchResult
forall a b. MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
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 -> MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchResult -> MaybeT m MatchResult)
-> MatchResult -> MaybeT m MatchResult
forall a b. (a -> b) -> a -> b
$ Nat -> WithOrigin Term -> MatchResult
forall k a. k -> a -> Map k a
Map.singleton Nat
j (Origin -> Term -> WithOrigin Term
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 -> MaybeT m MatchResult
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero  -- Higher-order pattern, fail for now.
    (Var Nat
i [Elim]
ps, Var Nat
j [Elim]
vs) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j  -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
    (Def QName
c [Elim]
ps, Def QName
d [Elim]
vs) | QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d  -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
    (Con ConHead
c ConInfo
_ [Elim]
ps, Con ConHead
d ConInfo
_ [Elim]
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
d -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
match Window
w [Elim]
ps [Elim]
vs
    (Lit Literal
l, Lit Literal
l')      | Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l' -> MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return MatchResult
forall k a. Map k a
Map.empty
    (Lam ArgInfo
h Abs Term
p, Lam ArgInfo
h' Abs Term
v)  | ArgInfo
h ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
h' -> Window -> Term -> Term -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Term -> Term -> MaybeT m MatchResult
match (Window -> Window
shiftWindow Window
w) (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
p) (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
v)
    (Term
p, Term
v)               | Term
p Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v  -> MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return MatchResult
forall k a. Map k a
Map.empty  -- TODO: this is wrong (this is why we lifted the rhs before)
    (Term
p, Level Level
l)                   -> Window -> Term -> Term -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Term -> Term -> MaybeT m MatchResult
match Window
w Term
p (Term -> MaybeT m MatchResult)
-> MaybeT m Term -> MaybeT m MatchResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> MaybeT m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
    (Sort Sort
ps, Sort Sort
pv)             -> Window -> Sort -> Sort -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Sort -> Sort -> MaybeT m MatchResult
match Window
w Sort
ps Sort
pv
    (Term
p, Sort (Type Level
v))             -> Window -> Term -> Term -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Term -> Term -> MaybeT m MatchResult
match Window
w Term
p (Term -> MaybeT m MatchResult)
-> MaybeT m Term -> MaybeT m MatchResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> MaybeT m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
    (Term, Term)
_                              -> MaybeT m MatchResult
forall a. MaybeT m a
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) -> Window -> Level -> Level -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Level -> Level -> MaybeT m MatchResult
match Window
w Level
pl Level
vl
    (Sort, Sort)
_ | Sort
p Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
v -> MatchResult -> MaybeT m MatchResult
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return MatchResult
forall k a. Map k a
Map.empty
    (Sort, Sort)
_          -> MaybeT m MatchResult
forall a. MaybeT m a
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 <- Level -> MaybeT m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
p
    Term
v <- Level -> MaybeT m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
v
    Window -> Term -> Term -> MaybeT m MatchResult
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
Window -> a -> a -> MaybeT m MatchResult
forall (m :: * -> *).
MonadDisplayForm m =>
Window -> Term -> Term -> MaybeT m MatchResult
match Window
w Term
p Term
v

-- | Substitute terms with origin into display terms,
--   replacing variables along with their origins.
--
--   The purpose is to replace the pattern variables in a with-display form,
--   and only on the top level of the lhs.  Thus, we are happy to fall back
--   to ordinary substitution where it does not matter.
--   This fixes issue #2590.

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 = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> [WithOrigin Term] -> a -> a
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) = 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 -> [WithOrigin Term] -> Arg a -> Arg a
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) = a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply
    (Substitution -> [WithOrigin Term] -> a -> a
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots a
u)
    (Substitution -> [WithOrigin Term] -> a -> a
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots a
v)
    (Substitution -> [WithOrigin Term] -> a -> a
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
      -- pattern variable: replace origin if better
      Var Nat
x [] -> case [WithOrigin Term]
ots [WithOrigin Term] -> Nat -> Maybe (WithOrigin Term)
forall a. [a] -> Nat -> Maybe a
!!! Nat
x of
        Just (WithOrigin Origin
o Term
u) -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ((Origin -> Origin) -> ArgInfo -> ArgInfo
forall a. LensOrigin a => (Origin -> Origin) -> a -> a
mapOrigin (Origin -> Origin -> Origin
replaceOrigin Origin
o) ArgInfo
ai) Term
u
        Maybe (WithOrigin Term)
Nothing -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v -- Issue #2717, not __IMPOSSIBLE__
      -- constructor: recurse
      Con ConHead
c ConInfo
ci [Elim]
args -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
args
      -- def: recurse
      Def QName
q [Elim]
es -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
q ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
      -- otherwise: fall back to ordinary substitution
      Term
_ -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
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
      -- constructor: recurse
      Con ConHead
c ConInfo
ci [Elim]
args -> ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
args
      -- def: recurse
      Def QName
q [Elim]
es -> QName -> [Elim] -> Term
Def QName
q ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
      -- otherwise: fall back to oridinary substitution
      Term
_ -> Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v

-- Do not go into dot pattern, otherwise interaction test #231 fails
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' (Substitution -> [WithOrigin Term] -> Term -> Term
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v) ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
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'  (Substitution -> [WithOrigin Term] -> Term -> Term
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v) ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
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    ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution
-> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
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 ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution
-> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
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
        (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots DisplayTerm
t)
        (Substitution -> [WithOrigin Term] -> [DisplayTerm] -> [DisplayTerm]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [DisplayTerm]
ts)
        (Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)

-- Do not go into dot pattern, otherwise interaction test #231 fails
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    -> Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v) Arg Term -> (Term -> DisplayTerm) -> Arg DisplayTerm
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Term -> [Elim] -> DisplayTerm
`DTerm'` Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)
      DDot'  Term
v [Elim]
es    -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> [Elim] -> DisplayTerm
DDot' (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v)  ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es
      DDef QName
q [Elim' DisplayTerm]
es      -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
q    ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution
-> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
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 -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution
-> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
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 -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ DisplayTerm -> [DisplayTerm] -> [Elim] -> DisplayTerm
DWithApp
        (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots DisplayTerm
t)
        (Substitution -> [WithOrigin Term] -> [DisplayTerm] -> [DisplayTerm]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [DisplayTerm]
ts)
        (Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)