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

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

module Mikan.TypeChecking.DisplayForm (displayForm) where

import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe
import Control.Applicative hiding (asum)

import Data.Strict.Tuple qualified as Pair
import Data.Monoid (All(..))
import Data.IntMap (IntMap)
import Data.IntMap qualified as IntMap
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set

import Mikan.Syntax.Common
import Mikan.Syntax.Internal
import Mikan.Syntax.Internal.Names
import Mikan.Syntax.Scope.Base (inverseScopeLookupName, isNameInScope)

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Level
import Mikan.TypeChecking.Reduce (instantiate)

import Mikan.Utils.StrictState
import Mikan.Utils.StrictReader
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.List1 (List1)
import Mikan.Utils.Maybe
import Mikan.Syntax.Common.Pretty

import Mikan.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
  )

type MatchResult = IntMap (WithOrigin Term)

-- | A monad for linear matching of display forms.
newtype MatchM a = MatchM { forall a.
MatchM a
-> IntMap (WithOrigin Term)
-> Origin
-> ReduceM (Pair (Maybe a) (IntMap (WithOrigin Term)))
unMatchM :: MatchResult -> Origin -> ReduceM (Pair.Pair (Maybe a) MatchResult) }
  deriving
    ( (forall a b. (a -> b) -> MatchM a -> MatchM b)
-> (forall a b. a -> MatchM b -> MatchM a) -> Functor MatchM
forall a b. a -> MatchM b -> MatchM a
forall a b. (a -> b) -> MatchM a -> MatchM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> MatchM a -> MatchM b
fmap :: forall a b. (a -> b) -> MatchM a -> MatchM b
$c<$ :: forall a b. a -> MatchM b -> MatchM a
<$ :: forall a b. a -> MatchM b -> MatchM a
Functor, Functor MatchM
Functor MatchM =>
(forall a. a -> MatchM a)
-> (forall a b. MatchM (a -> b) -> MatchM a -> MatchM b)
-> (forall a b c.
    (a -> b -> c) -> MatchM a -> MatchM b -> MatchM c)
-> (forall a b. MatchM a -> MatchM b -> MatchM b)
-> (forall a b. MatchM a -> MatchM b -> MatchM a)
-> Applicative MatchM
forall a. a -> MatchM a
forall a b. MatchM a -> MatchM b -> MatchM a
forall a b. MatchM a -> MatchM b -> MatchM b
forall a b. MatchM (a -> b) -> MatchM a -> MatchM b
forall a b c. (a -> b -> c) -> MatchM a -> MatchM b -> MatchM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> MatchM a
pure :: forall a. a -> MatchM a
$c<*> :: forall a b. MatchM (a -> b) -> MatchM a -> MatchM b
<*> :: forall a b. MatchM (a -> b) -> MatchM a -> MatchM b
$cliftA2 :: forall a b c. (a -> b -> c) -> MatchM a -> MatchM b -> MatchM c
liftA2 :: forall a b c. (a -> b -> c) -> MatchM a -> MatchM b -> MatchM c
$c*> :: forall a b. MatchM a -> MatchM b -> MatchM b
*> :: forall a b. MatchM a -> MatchM b -> MatchM b
$c<* :: forall a b. MatchM a -> MatchM b -> MatchM a
<* :: forall a b. MatchM a -> MatchM b -> MatchM a
Applicative, Applicative MatchM
Applicative MatchM =>
(forall a b. MatchM a -> (a -> MatchM b) -> MatchM b)
-> (forall a b. MatchM a -> MatchM b -> MatchM b)
-> (forall a. a -> MatchM a)
-> Monad MatchM
forall a. a -> MatchM a
forall a b. MatchM a -> MatchM b -> MatchM b
forall a b. MatchM a -> (a -> MatchM b) -> MatchM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. MatchM a -> (a -> MatchM b) -> MatchM b
>>= :: forall a b. MatchM a -> (a -> MatchM b) -> MatchM b
$c>> :: forall a b. MatchM a -> MatchM b -> MatchM b
>> :: forall a b. MatchM a -> MatchM b -> MatchM b
$creturn :: forall a. a -> MatchM a
return :: forall a. a -> MatchM a
Monad, MonadReader Origin, MonadState MatchResult, Monad MatchM
Monad MatchM => (forall a. String -> MatchM a) -> MonadFail MatchM
forall a. String -> MatchM a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> MatchM a
fail :: forall a. String -> MatchM a
MonadFail, Applicative MatchM
Applicative MatchM =>
(forall a. MatchM a)
-> (forall a. MatchM a -> MatchM a -> MatchM a)
-> (forall a. MatchM a -> MatchM [a])
-> (forall a. MatchM a -> MatchM [a])
-> Alternative MatchM
forall a. MatchM a
forall a. MatchM a -> MatchM [a]
forall a. MatchM a -> MatchM a -> MatchM a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
$cempty :: forall a. MatchM a
empty :: forall a. MatchM a
$c<|> :: forall a. MatchM a -> MatchM a -> MatchM a
<|> :: forall a. MatchM a -> MatchM a -> MatchM a
$csome :: forall a. MatchM a -> MatchM [a]
some :: forall a. MatchM a -> MatchM [a]
$cmany :: forall a. MatchM a -> MatchM [a]
many :: forall a. MatchM a -> MatchM [a]
Alternative
    , Monad MatchM
Functor MatchM
Applicative MatchM
MatchM CommandLineOptions
MatchM PragmaOptions
(Functor MatchM, Applicative MatchM, Monad MatchM) =>
MatchM PragmaOptions
-> MatchM CommandLineOptions -> HasOptions MatchM
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
m PragmaOptions -> m CommandLineOptions -> HasOptions m
$cpragmaOptions :: MatchM PragmaOptions
pragmaOptions :: MatchM PragmaOptions
$ccommandLineOptions :: MatchM CommandLineOptions
commandLineOptions :: MatchM CommandLineOptions
HasOptions, Monad MatchM
MatchM TCEnv
Monad MatchM =>
MatchM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> MatchM a -> MatchM a)
-> MonadTCEnv MatchM
forall a. (TCEnv -> TCEnv) -> MatchM a -> MatchM a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
$caskTC :: MatchM TCEnv
askTC :: MatchM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> MatchM a -> MatchM a
localTC :: forall a. (TCEnv -> TCEnv) -> MatchM a -> MatchM a
MonadTCEnv, Monad MatchM
MatchM SessionState
MatchM TCState
Monad MatchM =>
MatchM TCState
-> (forall a b.
    Lens' TCState a -> (a -> a) -> MatchM b -> MatchM b)
-> MatchM SessionState
-> (forall a. (TCState -> TCState) -> MatchM a -> MatchM a)
-> ReadTCState MatchM
forall a. (TCState -> TCState) -> MatchM a -> MatchM a
forall a b. Lens' TCState a -> (a -> a) -> MatchM b -> MatchM b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
-> m SessionState
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
$cgetTCState :: MatchM TCState
getTCState :: MatchM TCState
$clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> MatchM b -> MatchM b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> MatchM b -> MatchM b
$cgetSessionState :: MatchM SessionState
getSessionState :: MatchM SessionState
$cwithTCState :: forall a. (TCState -> TCState) -> MatchM a -> MatchM a
withTCState :: forall a. (TCState -> TCState) -> MatchM a -> MatchM a
ReadTCState, Applicative MatchM
HasOptions MatchM
MonadTCEnv MatchM
ReadTCState MatchM
(Applicative MatchM, MonadTCEnv MatchM, ReadTCState MatchM,
 HasOptions MatchM) =>
(forall a. ReduceM a -> MatchM a) -> MonadReduce MatchM
forall a. ReduceM a -> MatchM a
forall (m :: * -> *).
(Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
(forall a. ReduceM a -> m a) -> MonadReduce m
$cliftReduce :: forall a. ReduceM a -> MatchM a
liftReduce :: forall a. ReduceM a -> MatchM a
MonadReduce, Monad MatchM
Functor MatchM
Applicative MatchM
(Functor MatchM, Applicative MatchM, Monad MatchM) =>
(SomeBuiltin -> MatchM (Maybe (Builtin PrimFun)))
-> HasBuiltins MatchM
SomeBuiltin -> MatchM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
$cgetBuiltinThing :: SomeBuiltin -> MatchM (Maybe (Builtin PrimFun))
getBuiltinThing :: SomeBuiltin -> MatchM (Maybe (Builtin PrimFun))
HasBuiltins, Monad MatchM
Functor MatchM
Applicative MatchM
MatchM Bool
MatchM Verbosity
MatchM ProfileOptions
(Functor MatchM, Applicative MatchM, Monad MatchM) =>
(String -> Nat -> TCM Doc -> MatchM Doc)
-> (forall a. String -> Nat -> Doc -> MatchM a -> MatchM a)
-> (forall a. String -> Nat -> String -> MatchM a -> MatchM a)
-> MatchM Verbosity
-> MatchM ProfileOptions
-> MatchM Bool
-> (forall a. MatchM a -> MatchM a)
-> MonadDebug MatchM
String -> Nat -> TCM Doc -> MatchM Doc
forall a. String -> Nat -> String -> MatchM a -> MatchM a
forall a. String -> Nat -> Doc -> MatchM a -> MatchM a
forall a. MatchM a -> MatchM a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(String -> Nat -> TCM Doc -> m Doc)
-> (forall a. String -> Nat -> Doc -> m a -> m a)
-> (forall a. String -> Nat -> String -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
$cformatDebugMessage :: String -> Nat -> TCM Doc -> MatchM Doc
formatDebugMessage :: String -> Nat -> TCM Doc -> MatchM Doc
$ctraceDebugMessage :: forall a. String -> Nat -> Doc -> MatchM a -> MatchM a
traceDebugMessage :: forall a. String -> Nat -> Doc -> MatchM a -> MatchM a
$cverboseBracket :: forall a. String -> Nat -> String -> MatchM a -> MatchM a
verboseBracket :: forall a. String -> Nat -> String -> MatchM a -> MatchM a
$cgetVerbosity :: MatchM Verbosity
getVerbosity :: MatchM Verbosity
$cgetProfileOptions :: MatchM ProfileOptions
getProfileOptions :: MatchM ProfileOptions
$cisDebugPrinting :: MatchM Bool
isDebugPrinting :: MatchM Bool
$cnowDebugPrinting :: forall a. MatchM a -> MatchM a
nowDebugPrinting :: forall a. MatchM a -> MatchM a
MonadDebug
    )
    via MaybeT (StateT MatchResult (ReaderT Origin ReduceM))

-- | Assign the given variable to the term, failing if the variable has
-- already been assigned.
assignMatch :: Int -> Term -> MatchM ()
assignMatch :: Nat -> Term -> MatchM ()
assignMatch Nat
m Term
t = (IntMap (WithOrigin Term) -> Bool) -> MatchM Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Nat -> IntMap (WithOrigin Term) -> Bool
forall a. Nat -> IntMap a -> Bool
IntMap.member Nat
m) MatchM Bool -> (Bool -> MatchM ()) -> MatchM ()
forall a b. MatchM a -> (a -> MatchM b) -> MatchM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
True  -> MatchM ()
forall a. MatchM a
forall (f :: * -> *) a. Alternative f => f a
empty -- non-linear display forms are not supported yet.
  Bool
False -> do
    o <- MatchM Origin
forall r (m :: * -> *). MonadReader r m => m r
ask
    modify $ IntMap.insert m (WithOrigin o t)

runMatch :: MonadDisplayForm m => MatchM a -> m (Maybe a)
runMatch :: forall (m :: * -> *) a.
MonadDisplayForm m =>
MatchM a -> m (Maybe a)
runMatch MatchM a
k = ReduceM (Maybe a) -> m (Maybe a)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Maybe a) -> m (Maybe a))
-> ReduceM (Maybe a) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ MatchM a
-> IntMap (WithOrigin Term)
-> Origin
-> ReduceM (Pair (Maybe a) (IntMap (WithOrigin Term)))
forall a.
MatchM a
-> IntMap (WithOrigin Term)
-> Origin
-> ReduceM (Pair (Maybe a) (IntMap (WithOrigin Term)))
unMatchM MatchM a
k IntMap (WithOrigin Term)
forall a. Monoid a => a
mempty Origin
Inserted ReduceM (Pair (Maybe a) (IntMap (WithOrigin Term)))
-> (Pair (Maybe a) (IntMap (WithOrigin Term)) -> Maybe a)
-> ReduceM (Maybe a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Pair (Maybe a) (IntMap (WithOrigin Term)) -> Maybe a
forall a b. Pair a b -> a
Pair.fst

-- | Find a matching display form for @q es@.
--
-- In essence this tries to rewrite @q es@ with any of the display forms
-- @q ps --> dt@, returning the first instantiated @dt@.

displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
displayForm :: forall (m :: * -> *).
MonadDisplayForm m =>
QName -> [Elim] -> m (Maybe DisplayTerm)
displayForm QName
q [Elim]
es = MaybeT m DisplayTerm -> m (Maybe DisplayTerm)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
  -- Get display forms for name q.
  odfs <- QName -> MaybeT m [Open DisplayForm]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Open DisplayForm]
getDisplayForms QName
q
  guard (not (null odfs))

  -- Display debug info about the @Open@s.
  unlessDebugPrinting $ reportSDoc "tc.display.top" 100 $ do
    cps <- viewTC eCheckpoints
    cxt <- getContextTelescope
    ofs <- catMaybes <$> traverse (tryGetOpen liftLocalDisplayForm) odfs
    return $ vcat
      [ "displayForm for" <+> pretty q
      , nest 2 $ "cxt =" <+> pretty cxt
      , nest 2 $ "cps =" <+> vcat (map pretty (Map.toList cps))
      , nest 2 $ "dfs =" <+> vcat (map pretty odfs)
      , nest 2 $ "ofs =" <+> vcat (map pretty ofs)
      , nest 2 $ " es =" <+> pretty (map (fmap unSpine) es)
      ]

  scope <- getScope

  let
    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
. (QName -> ScopeInfo -> Bool) -> ScopeInfo -> QName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> ScopeInfo -> Bool
isNameInScope ScopeInfo
scope) DisplayTerm
d

    isWithDisplay DWithApp{} = Bool
True
    isWithDisplay DisplayTerm
_          = Bool
False

  asum $ odfs <&> \Open DisplayForm
odf -> Maybe DisplayTerm -> MaybeT m DisplayTerm
forall (f :: * -> *) a. Alternative f => Maybe a -> f a
liftMaybe (Maybe DisplayTerm -> MaybeT m DisplayTerm)
-> MaybeT m (Maybe DisplayTerm) -> MaybeT m DisplayTerm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MatchM DisplayTerm -> MaybeT m (Maybe DisplayTerm)
forall (m :: * -> *) a.
MonadDisplayForm m =>
MatchM a -> m (Maybe a)
runMatch do
    -- Use only the display forms that can be opened in the current
    -- context.
    df <- Maybe DisplayForm -> MatchM DisplayForm
forall (f :: * -> *) a. Alternative f => Maybe a -> f a
liftMaybe (Maybe DisplayForm -> MatchM DisplayForm)
-> MatchM (Maybe DisplayForm) -> MatchM DisplayForm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Substitution -> DisplayForm -> Maybe DisplayForm)
-> Open DisplayForm -> MatchM (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
odf

    -- All names in the display form should be in scope. 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.
    guard (wellScoped scope df)

    -- Keep the display forms that match the application @q es@.
    r <- matchDisplayForm df es
    r <$ unlessDebugPrinting do
      reportS "tc.display.top" 100 $ "result:" <+> pretty r

{-# SPECIALIZE displayForm :: QName -> Elims -> TCM (Maybe DisplayTerm) #-}

-- | 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 :: DisplayForm -> Elims -> MatchM DisplayTerm
matchDisplayForm :: DisplayForm -> [Elim] -> MatchM DisplayTerm
matchDisplayForm (Display Nat
n [Elim]
ps DisplayTerm
v) [Elim]
es = do
  es1 <- Window -> [Elim] -> [Elim] -> MatchM [Elim]
matchElims (Nat -> Nat -> Window
Window Nat
0 Nat
n) [Elim]
ps [Elim]
es
  us <- forM [0 .. n - 1] $ \ Nat
i ->
    -- #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.
    Maybe (WithOrigin Term) -> MatchM (WithOrigin Term)
forall (f :: * -> *) a. Alternative f => Maybe a -> f a
liftMaybe (Maybe (WithOrigin Term) -> MatchM (WithOrigin Term))
-> MatchM (Maybe (WithOrigin Term)) -> MatchM (WithOrigin Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (IntMap (WithOrigin Term) -> Maybe (WithOrigin Term))
-> MatchM (Maybe (WithOrigin Term))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Nat -> IntMap (WithOrigin Term) -> Maybe (WithOrigin Term)
forall a. Nat -> IntMap a -> Maybe a
IntMap.lookup Nat
i)
  return (substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)

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)

-- | Compare variables in a 'Window'.
--
-- The 'Display' constructor acts as though it binds the pattern
-- pattern variables up to 'n', so a match like
--
-- Display 1 [@1 @0] x =? [@0 _]
--
-- should work (it didn't; see LiftDisplayIntermediate). In effect,
-- this is because the LHS patterns are in some context "Γ . @0", but
-- the RHS term is only in context Γ.
--
-- Therefore, this function raises variables appearing in the RHS so
-- that they live inside the given 'Window' before comparing with
-- variables in the patterns. This avoids having to weaken and
-- strengthen the arguments to a display form.
sameVar :: Window -> Nat -> Nat -> Bool
sameVar :: Window -> Nat -> Nat -> Bool
sameVar (Window Nat
lo Nat
hi) Nat
i Nat
j = Nat -> Term
var Nat
i Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Nat -> Substitution
forall a. Nat -> Nat -> Substitution' a
raiseFromS Nat
lo Nat
hi) (Nat -> Term
var Nat
j)

-- @'matchElims' rho n ps es@ matches some display patterns against the
-- eliminations of a term, inserting implicit arguments where necessary,
-- and returning whatever eliminations were left over.
matchElims
  :: Window
  -> Elims -- ^ The patterns to match against.
  -> Elims -- ^ The eliminations.
  -> MatchM Elims
matchElims :: Window -> [Elim] -> [Elim] -> MatchM [Elim]
matchElims Window
n = [Elim] -> [Elim] -> MatchM [Elim]
go where

  -- match one elimination pattern against the head of the list,
  -- returning the remaining eliminations.
  unconsArg :: Elim -> Elims -> MatchM Elims
  -- not enough arguments:
  unconsArg :: Elim -> [Elim] -> MatchM [Elim]
unconsArg Elim
_ [] = MatchM [Elim]
forall a. MatchM a
forall (f :: * -> *) a. Alternative f => f a
empty

  -- projections only match themselves, no implicit insertion applies,
  -- and note that origin does not matter:
  unconsArg (Proj ProjOrigin
_ QName
f) [Elim]
es = case [Elim]
es of
    Proj ProjOrigin
_ QName
f':[Elim]
es -> [Elim]
es [Elim] -> MatchM () -> MatchM [Elim]
forall a b. a -> MatchM b -> MatchM a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f')
    [Elim]
_            -> MatchM [Elim]
forall a. MatchM a
forall (f :: * -> *) a. Alternative f => f a
empty

  -- both Apply and IApply count as application for the purposes of
  -- matching. if the pattern is invisible but the argument is visible,
  -- we match the pattern against a dummy (necessary if the pattern has
  -- simple pattern variables) and keep the argument in the result list
  -- for the next pattern.
  unconsArg Elim
p (Elim
e:[Elim]
es) | Arg Term
p' <- Elim -> Arg Term
forall a. Elim' a -> Arg a
mustApplyElim Elim
p = do
    e' <- Maybe (Arg Term) -> MatchM (Arg Term)
forall (f :: * -> *) a. Alternative f => Maybe a -> f a
liftMaybe (Maybe (Arg Term) -> MatchM (Arg Term))
-> Maybe (Arg Term) -> MatchM (Arg Term)
forall a b. (a -> b) -> a -> b
$ Elim -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim
e
    if not (visible p') && visible e'
      then (e:es) <$ match n p' (Dummy DummyDisplay [] <$ p')
      else es     <$ match n p' e'

  go :: Elims -> Elims -> MatchM Elims
  go :: [Elim] -> [Elim] -> MatchM [Elim]
go (Elim
p:[Elim]
ps) [Elim]
es = do
    es <- Elim -> [Elim] -> MatchM [Elim]
unconsArg Elim
p [Elim]
es
    go ps es
  go [] [Elim]
es = [Elim] -> MatchM [Elim]
forall a. a -> MatchM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Elim]
es

-- | 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 :: Window -> a -> a -> MatchM ()

instance Match a => Match (Arg a) where
  match :: Window -> Arg a -> Arg a -> MatchM ()
match Window
n (Arg ArgInfo
i a
p) (Arg ArgInfo
i' a
v) = (Origin -> Origin) -> MatchM () -> MatchM ()
forall a. (Origin -> Origin) -> MatchM a -> MatchM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Origin -> Origin -> Origin
forall a b. a -> b -> a
const (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
i')) do
    Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ArgInfo
i ArgInfo -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
`sameHiding` ArgInfo
i')
    Window -> a -> a -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
n a
p a
v

instance Match a => Match (Dom a) where
  match :: Window -> Dom a -> Dom a -> MatchM ()
match Window
n Dom a
p Dom a
v = Window -> Arg a -> Arg a -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
n (Dom a -> Arg a
forall t a. Dom' t a -> Arg a
argFromDom Dom a
p) (Dom a -> Arg a
forall t a. Dom' t a -> Arg a
argFromDom Dom a
v)

instance a ~ Elim => Match [a] where
  match :: Window -> [a] -> [a] -> MatchM ()
match Window
n [a]
ps [a]
as = do
    [] <- Window -> [Elim] -> [Elim] -> MatchM [Elim]
matchElims Window
n [a]
[Elim]
ps [a]
[Elim]
as
    pure ()

instance Match Term where
  match :: Window -> Term -> Term -> MatchM ()
match Window
w Term
p Term
v = ReduceM Term -> MatchM Term
forall a. ReduceM a -> MatchM a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (Term -> ReduceM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v) MatchM Term -> (Term -> MatchM ()) -> MatchM ()
forall a b. MatchM a -> (a -> MatchM b) -> MatchM 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 [Elim]
es, Term
_) | Just Nat
j <- Window -> Nat -> Maybe Nat
inWindow Window
w Nat
i ->
      -- fail to match if the pattern variable is applied because we
      -- don't support higher-order display patterns yet.
      -- note that the binding is to the spined form of v.
      Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Elim] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Elim]
es) MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Nat -> Term -> MatchM ()
assignMatch Nat
j Term
v

    -- only the display dummy should appear here; it matches any
    -- pattern.
    (Term
_, Dummy DummyTermKind
r [Elim]
_) -> case DummyTermKind
r of
      DummyTermKind
DummyDisplay -> () -> MatchM ()
forall a. a -> MatchM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      DummyBrave{} -> MatchM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      DummyNamed{} -> MatchM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    (Lit Literal
l      , Lit Literal
m     ) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
m)
    (Var Nat
i [Elim]
ps   , Var Nat
j [Elim]
vs  ) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Window -> Nat -> Nat -> Bool
sameVar Window
w Nat
i Nat
j) MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> [Elim] -> [Elim] -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w [Elim]
ps [Elim]
vs
    (Def QName
c [Elim]
ps   , Def QName
d [Elim]
vs  ) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d)        MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> [Elim] -> [Elim] -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w [Elim]
ps [Elim]
vs
    (Con ConHead
c ConInfo
_ [Elim]
ps , Con ConHead
d ConInfo
_ [Elim]
vs) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
d)        MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> [Elim] -> [Elim] -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w [Elim]
ps [Elim]
vs
    (Lam ArgInfo
h Abs Term
p    , Lam ArgInfo
i Abs Term
v   ) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ArgInfo
h ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
i) MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> Term -> Term -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
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)
    (Pi  Dom' Term Type
d Abs Type
r    , Pi Dom' Term Type
e Abs Type
s    ) -> Window -> Dom' Term Type -> Dom' Term Type -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w Dom' Term Type
d Dom' Term Type
e    MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> Type -> Type -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match (Window -> Window
shiftWindow Window
w) (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
r) (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
s)
    (Sort Sort
ps    , Sort Sort
pv   ) -> Window -> Sort -> Sort -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w Sort
ps Sort
pv
    (Term
p, Level Level
l)              -> Window -> Term -> Term -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w Term
p (Term -> MatchM ()) -> MatchM Term -> MatchM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> MatchM Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l

    (Term, Term)
_                         -> MatchM ()
forall a. MatchM a
forall (f :: * -> *) a. Alternative f => f a
empty

instance Match Type where
  match :: Window -> Type -> Type -> MatchM ()
match Window
w (El Sort
p Term
_) (El Sort
v Term
_) = Window -> Sort -> Sort -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w Sort
p Sort
v

instance Match Sort where
  match :: Window -> Sort -> Sort -> MatchM ()
match Window
w Sort
p Sort
v = case (Sort
p, Sort
v) of
    (Univ Univ
u Level
pl, Univ Univ
u' Level
vl) -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u') MatchM () -> MatchM () -> MatchM ()
forall a b. MatchM a -> MatchM b -> MatchM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Window -> Level -> Level -> MatchM ()
forall a. Match a => Window -> a -> a -> MatchM ()
match Window
w Level
pl Level
vl
    (Sort, Sort)
_                       -> Bool -> MatchM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Sort
p Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
v)

instance Match Level where
  match :: Window -> Level -> Level -> MatchM ()
match Window
w Level
p Level
v = do
    p <- Level -> MatchM Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
p
    v <- reallyUnLevelView v
    match w p 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 (List1 a) where
  substWithOrigin :: Substitution -> [WithOrigin Term] -> List1 a -> List1 a
substWithOrigin Substitution
rho [WithOrigin Term]
ots = (a -> a) -> List1 a -> List1 a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 List1 DisplayTerm
ts [Elim]
es -> DisplayTerm -> List1 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] -> List1 DisplayTerm -> List1 DisplayTerm
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots List1 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 List1 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 -> List1 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] -> List1 DisplayTerm -> List1 DisplayTerm
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots List1 DisplayTerm
ts)
        (Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
forall a.
SubstWithOrigin a =>
Substitution -> [WithOrigin Term] -> a -> a
substWithOrigin Substitution
rho [WithOrigin Term]
ots [Elim]
es)