{-# 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.Utils.Pretty

import Agda.Utils.Impossible

-- | Convert a 'DisplayTerm' into a 'Term'.
dtermToTerm :: DisplayTerm -> Term
dtermToTerm :: DisplayTerm -> Term
dtermToTerm DisplayTerm
dt = case DisplayTerm
dt of
  DWithApp DisplayTerm
d [DisplayTerm]
ds Elims
es ->
    DisplayTerm -> Term
dtermToTerm DisplayTerm
d forall t. Apply t => t -> Args -> t
`apply` forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Arg a
defaultArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayTerm -> Term
dtermToTerm) [DisplayTerm]
ds forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
  DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
args   -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DisplayTerm -> Term
dtermToTerm) [Arg DisplayTerm]
args
  DDef QName
f [Elim' DisplayTerm]
es        -> QName -> Elims -> Term
Def QName
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DisplayTerm -> Term
dtermToTerm) [Elim' DisplayTerm]
es
  DDot Term
v           -> Term
v
  DTerm Term
v          -> Term
v

-- | 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 = 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 -> Elims
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

-- | 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 = forall a. a -> Maybe a
Just DisplayForm
df
liftLocalDisplayForm (Wk Nat
n Substitution
IdS) (Display Nat
m Elims
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.
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Elims -> DisplayTerm -> DisplayForm
Display (Nat
n forall a. Num a => a -> a -> a
+ Nat
m) Elims
lhs DisplayTerm
rhs
liftLocalDisplayForm Substitution
_ 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 -> Elims -> m (Maybe DisplayTerm)
displayForm QName
q Elims
es = do
  -- Get display forms for name q.
  [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
    -- Display debug info about the @Open@s.
    forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM Doc -> 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' a TCEnv -> m a
viewTC Lens' (Map CheckpointId Substitution) TCEnv
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 -> Doc
vcat
        [ Doc
"displayForm for" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
q
        , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"cxt =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Telescope
cxt
        , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"cps =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty (forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
cps))
        , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"dfs =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Open DisplayForm]
odfs) ]
    -- Use only the display forms that can be opened in the current context.
    [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
    -- Keep the display forms that match the application @q es@.
    [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 -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
`matchDisplayForm` Elims
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 ]
    -- Not safe when printing non-terminating terms.
    -- (nfdfs, us) <- normalise (dfs, es)
    forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM Doc -> 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 -> Doc
vcat
      [ Doc
"name        :" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
q
      , Doc
"displayForms:" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty [DisplayForm]
dfs
      , Doc
"arguments   :" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Elims
es
      , Doc
"matches     :" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty [DisplayTerm]
ms
      , Doc
"result      :" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms)
      ]
    -- Return the first display form that matches.
    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
    -- 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
_ Elims
_ 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  -- all names in d should be in scope

    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

-- | 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 -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
matchDisplayForm d :: DisplayForm
d@(Display Nat
n Elims
ps DisplayTerm
v) Elims
es
  | forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
ps forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  | Bool
otherwise             = do
      let (Elims
es0, Elims
es1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
ps) Elims
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) Elims
ps Elims
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
              -- #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 <- 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 -> Elims -> t
`applyE` Elims
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  -- Non-linear pattern, fail for now.

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@ 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 = 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'
      -- we do not care to differentiate between Apply and IApply for
      -- printing.
      (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
_:Elims
_), Term
v) | Just{} <- Window -> Nat -> Maybe Nat
inWindow Window
w Nat
i -> forall (m :: * -> *) a. MonadPlus m => m a
mzero  -- Higher-order pattern, fail for now.
    (Var Nat
i Elims
ps, Var Nat
j Elims
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 Elims
ps Elims
vs
    (Def QName
c Elims
ps, Def QName
d Elims
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 Elims
ps Elims
vs
    (Con ConHead
c ConInfo
_ Elims
ps, Con ConHead
d ConInfo
_ Elims
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 Elims
ps Elims
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  -- TODO: this is wrong (this is why we lifted the rhs before)
    (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

-- | 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 = 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
      -- pattern variable: replace origin if better
      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 -- Issue #2717, not __IMPOSSIBLE__
      -- constructor: recurse
      Con ConHead
c ConInfo
ci Elims
args -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> 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 Elims
args
      -- def: recurse
      Def QName
q Elims
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ QName -> Elims -> 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 Elims
es
      -- otherwise: fall back to ordinary substitution
      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
      -- constructor: recurse
      Con ConHead
c ConInfo
ci Elims
args -> ConHead -> ConInfo -> Elims -> 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 Elims
args
      -- def: recurse
      Def QName
q Elims
es -> QName -> Elims -> 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 Elims
es
      -- otherwise: fall back to oridinary substitution
      Term
_ -> forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
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 DisplayTerm
dt =
    case DisplayTerm
dt of
      DTerm Term
v        -> Term -> DisplayTerm
DTerm     forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v
      DDot  Term
v        -> Term -> DisplayTerm
DDot      forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v
      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 Elims
es -> DisplayTerm -> [DisplayTerm] -> Elims -> 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 Elims
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        -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm forall a b. (a -> b) -> a -> b
$ forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v
      DDot  Term
v        -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term -> DisplayTerm
DDot      forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho Term
v
      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 Elims
es -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ DisplayTerm -> [DisplayTerm] -> Elims -> 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 Elims
es)