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

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

module Agda.TypeChecking.DisplayForm where

import Prelude hiding (all)
import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe
import Data.Foldable (all)
import qualified Data.Map as Map

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.Monad.Builtin (HasBuiltins(..))
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 Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (DisplayTerm -> Arg Term) -> [DisplayTerm] -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term)
-> (DisplayTerm -> Term) -> DisplayTerm -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayTerm -> Term
dtermToTerm) [DisplayTerm]
ds Term -> Elims -> Term
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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg DisplayTerm -> Elim' Term) -> [Arg DisplayTerm] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Arg DisplayTerm -> Arg Term) -> Arg DisplayTerm -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DisplayTerm -> Term) -> Arg DisplayTerm -> Arg Term
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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Elim' DisplayTerm -> Elim' Term) -> [Elim' DisplayTerm] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map ((DisplayTerm -> Term) -> Elim' DisplayTerm -> Elim' Term
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 :: QName -> m [Int]
displayFormArities QName
q = (Open DisplayForm -> Int) -> [Open DisplayForm] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Elims -> Int)
-> (Open DisplayForm -> Elims) -> Open DisplayForm -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForm -> Elims
dfPats (DisplayForm -> Elims)
-> (Open DisplayForm -> DisplayForm) -> Open DisplayForm -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Open DisplayForm -> DisplayForm
forall (t :: * -> *) a. Decoration t => t a -> a
dget) ([Open DisplayForm] -> [Int]) -> m [Open DisplayForm] -> m [Int]
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

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 :: QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
q Elims
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 (t :: * -> *) a. Foldable t => t a -> Bool
null [Open DisplayForm]
odfs) then do
    VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.display.top" Int
101 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"no displayForm for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q
    Maybe DisplayTerm -> m (Maybe DisplayTerm)
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.
    VerboseKey -> Int -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> m () -> m ()
verboseS VerboseKey
"tc.display.top" Int
100 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      Map CheckpointId Substitution
cps <- Lens' (Map CheckpointId Substitution) TCEnv
-> m (Map CheckpointId Substitution)
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Map CheckpointId Substitution) TCEnv
eCheckpoints
      Telescope
cxt <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.display.top" Int
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
        [ Doc
"displayForm for" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
        , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"cxt =" Doc -> Doc -> Doc
<+> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
cxt
        , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"cps =" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (((CheckpointId, Substitution) -> Doc)
-> [(CheckpointId, Substitution)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (CheckpointId, Substitution) -> Doc
forall a. Pretty a => a -> Doc
pretty (Map CheckpointId Substitution -> [(CheckpointId, Substitution)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
cps))
        , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"dfs =" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat ((Open DisplayForm -> Doc) -> [Open DisplayForm] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Open DisplayForm -> Doc
forall a. Show a => a -> Doc
pshow [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)
mapM Open DisplayForm -> m (Maybe DisplayForm)
forall a (m :: * -> *).
(Subst Term a, MonadTCEnv m) =>
Open a -> m (Maybe a)
tryGetOpen [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)
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 -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
`matchDisplayForm` Elims
es)) [DisplayForm]
dfs
      [DisplayTerm] -> m [DisplayTerm]
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
$ VerboseKey -> Int -> [VerboseKey] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> Int -> a -> m ()
reportS VerboseKey
"tc.display.top" Int
100
      [ VerboseKey
"name        : " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
q
      , VerboseKey
"displayForms: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [DisplayForm] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [DisplayForm]
dfs
      , VerboseKey
"arguments   : " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Elims -> VerboseKey
forall a. Show a => a -> VerboseKey
show Elims
es
      , VerboseKey
"matches     : " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [DisplayTerm] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [DisplayTerm]
ms
      , VerboseKey
"result      : " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe DisplayTerm -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([DisplayTerm] -> Maybe DisplayTerm
forall a. [a] -> Maybe a
listToMaybe [DisplayTerm]
ms)
      ]
    -- Return the first display form that matches.
    Maybe DisplayTerm -> m (Maybe DisplayTerm)
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 Int
_ Elims
_ DisplayTerm
d)
      | DisplayTerm -> Bool
isWithDisplay DisplayTerm
d = Bool
True
      | Bool
otherwise       = (QName -> Bool) -> Set QName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ScopeInfo -> QName -> Bool
inScope ScopeInfo
scope) (Set QName -> Bool) -> Set QName -> Bool
forall a b. (a -> b) -> a -> b
$ DisplayTerm -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn DisplayTerm
d

    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 (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 :: DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
matchDisplayForm d :: DisplayForm
d@(Display Int
_ Elims
ps DisplayTerm
v) Elims
es
  | Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es = MaybeT m (DisplayForm, DisplayTerm)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  | Bool
otherwise             = do
      let (Elims
es0, Elims
es1) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt (Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
ps) Elims
es
      [WithOrigin Term]
us <- [WithOrigin Term] -> [WithOrigin Term]
forall a. [a] -> [a]
reverse ([WithOrigin Term] -> [WithOrigin Term])
-> MaybeT m [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Elims -> Elims -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Elims
ps (Elims -> MaybeT m [WithOrigin Term])
-> Elims -> MaybeT m [WithOrigin Term]
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall t a. Subst t a => Int -> a -> a
raise Int
1 Elims
es0
      (DisplayForm, DisplayTerm) -> MaybeT m (DisplayForm, DisplayTerm)
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 -> Elims -> DisplayTerm
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1)

-- | Class @Match@ for matching a term @p@ in the role of a pattern
--   against a term @v@.
--
--   The 0th variable in @p@ plays the role
--   of a place holder (pattern variable).  Each occurrence of
--   @var 0@ in @p@ stands for a different pattern variable.
--
--   The result of matching, if successful, is a list of solutions for the
--   pattern variables, in left-to-right order.
--
--   The 0th variable is in scope in the input @v@, but should not
--   actually occur!
--   In the output solution, the @0th@ variable is no longer in scope.
--   (It has been substituted by __IMPOSSIBLE__ which corresponds to
--   a raise by -1).
class Match a where
  match :: MonadDisplayForm m => a -> a -> MaybeT m [WithOrigin Term]

instance Match a => Match [a] where
  match :: [a] -> [a] -> MaybeT m [WithOrigin Term]
match [a]
xs [a]
ys = [[WithOrigin Term]] -> [WithOrigin Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[WithOrigin Term]] -> [WithOrigin Term])
-> MaybeT m [[WithOrigin Term]] -> MaybeT m [WithOrigin Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> a -> MaybeT m [WithOrigin Term])
-> [a] -> [a] -> MaybeT m [[WithOrigin Term]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM a -> a -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match [a]
xs [a]
ys

instance Match a => Match (Arg a) where
  match :: Arg a -> Arg a -> MaybeT m [WithOrigin Term]
match Arg a
p Arg a
v = (WithOrigin Term -> WithOrigin Term)
-> [WithOrigin Term] -> [WithOrigin Term]
forall a b. (a -> b) -> [a] -> [b]
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)) ([WithOrigin Term] -> [WithOrigin Term])
-> MaybeT m [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match (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 :: Elim' a -> Elim' a -> MaybeT m [WithOrigin Term]
match 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' -> [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      (Apply Arg a
a, Apply Arg a
a')         -> Arg a -> Arg a -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Arg a
a Arg a
a'
      (Elim' a, Elim' a)
_                           -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance Match Term where
  match :: Term -> Term -> MaybeT m [WithOrigin Term]
match Term
p Term
v = m Term -> MaybeT m Term
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 [WithOrigin Term])
-> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Term
v -> case (Term
p, Term
v) of
    (Var Int
0 [], Term
v) -> [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Origin -> Term -> WithOrigin Term
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Term -> WithOrigin Term) -> Term -> WithOrigin Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term -> Term
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
v ]
    (Var Int
i Elims
ps, Var Int
j Elims
vs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j  -> Elims -> Elims -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Elims
ps Elims
vs
    (Def QName
c Elims
ps, Def QName
d Elims
vs) | QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d  -> Elims -> Elims -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Elims
ps Elims
vs
    (Con ConHead
c ConInfo
_ Elims
ps, Con ConHead
d ConInfo
_ Elims
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
d -> Elims -> Elims -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Elims
ps Elims
vs
    (Lit Literal
l, Lit Literal
l')      | Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l' -> [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Term
p, Term
v)               | Term
p Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v  -> [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Term
p, Level Level
l)                   -> Term -> Term -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Term
p (Term -> MaybeT m [WithOrigin Term])
-> MaybeT m Term -> MaybeT m [WithOrigin Term]
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)             -> Sort -> Sort -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Sort
ps Sort
pv
    (Term
p, Sort (Type Level
v))             -> Term -> Term -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Term
p (Term -> MaybeT m [WithOrigin Term])
-> MaybeT m Term -> MaybeT m [WithOrigin Term]
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 [WithOrigin Term]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance Match Sort where
  match :: Sort -> Sort -> MaybeT m [WithOrigin Term]
match Sort
p Sort
v = case (Sort
p, Sort
v) of
    (Type Level
pl, Type Level
vl) -> Level -> Level -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match Level
pl Level
vl
    (Sort, Sort)
_ | Sort
p Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
v -> [WithOrigin Term] -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Sort, Sort)
_          -> MaybeT m [WithOrigin Term]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance Match Level where
  match :: Level -> Level -> MaybeT m [WithOrigin Term]
match 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
    Term -> Term -> MaybeT m [WithOrigin Term]
forall a (m :: * -> *).
(Match a, MonadDisplayForm m) =>
a -> a -> MaybeT m [WithOrigin Term]
match 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 Int
x [] -> case [WithOrigin Term]
ots [WithOrigin Term] -> Int -> Maybe (WithOrigin Term)
forall a. [a] -> Int -> Maybe a
!!! Int
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 -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
rho Term
v -- Issue #2717, not __IMPOSSIBLE__
      -- constructor: recurse
      Con ConHead
c ConInfo
ci Elims
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 -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Elims -> Elims
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Elims
args
      -- def: recurse
      Def QName
q Elims
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 -> Elims -> Term
Def QName
q (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Elims -> Elims
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Elims
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 -> Term -> Term
forall t a. Subst t a => Substitution' t -> 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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Elims -> Elims
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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Elims -> Elims
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Elims
es
      -- otherwise: fall back to oridinary substitution
      Term
_ -> Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> 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     (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Term -> Term
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Term
v
      DDot  Term
v        -> Term -> DisplayTerm
DDot      (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
rho Term
v
      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 Elims
es -> DisplayTerm -> [DisplayTerm] -> Elims -> 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] -> Elims -> Elims
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        -> (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm (Arg Term -> Arg DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v
      DDot  Term
v        -> 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 -> DisplayTerm
DDot      (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
rho Term
v
      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 Elims
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] -> Elims -> 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] -> Elims -> Elims
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots Elims
es)