{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

{- |  Non-linear matching of the lhs of a rewrite rule against a
      neutral term.

Given a lhs

  Δ ⊢ lhs : B

and a candidate term

  Γ ⊢ t : A

we seek a substitution Γ ⊢ σ : Δ such that

  Γ ⊢ B[σ] = A   and
  Γ ⊢ lhs[σ] = t : A

-}

module Agda.TypeChecking.Rewriting.NonLinMatch where

import Prelude hiding (null, sequence)

import Control.Applicative  ( Alternative )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )

import Data.Maybe
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Conversion.Pure (pureBlockOrEqualTermPureTCM)
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Irrelevance (isPropM)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive.Cubical.Base

import Agda.Utils.Either
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.VarSet (VarSet)
import Agda.Utils.VarSet qualified as VarSet
import Agda.Utils.StrictState

import Agda.Utils.Impossible


-- | Monad for non-linear matching.
newtype NLM a = NLM { forall a.
NLM a -> ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) a
unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a }
  deriving ( (forall a b. (a -> b) -> NLM a -> NLM b)
-> (forall a b. a -> NLM b -> NLM a) -> Functor NLM
forall a b. a -> NLM b -> NLM a
forall a b. (a -> b) -> NLM a -> NLM 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) -> NLM a -> NLM b
fmap :: forall a b. (a -> b) -> NLM a -> NLM b
$c<$ :: forall a b. a -> NLM b -> NLM a
<$ :: forall a b. a -> NLM b -> NLM a
Functor, Functor NLM
Functor NLM =>
(forall a. a -> NLM a)
-> (forall a b. NLM (a -> b) -> NLM a -> NLM b)
-> (forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c)
-> (forall a b. NLM a -> NLM b -> NLM b)
-> (forall a b. NLM a -> NLM b -> NLM a)
-> Applicative NLM
forall a. a -> NLM a
forall a b. NLM a -> NLM b -> NLM a
forall a b. NLM a -> NLM b -> NLM b
forall a b. NLM (a -> b) -> NLM a -> NLM b
forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM 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 -> NLM a
pure :: forall a. a -> NLM a
$c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
$cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
liftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
$c*> :: forall a b. NLM a -> NLM b -> NLM b
*> :: forall a b. NLM a -> NLM b -> NLM b
$c<* :: forall a b. NLM a -> NLM b -> NLM a
<* :: forall a b. NLM a -> NLM b -> NLM a
Applicative, Applicative NLM
Applicative NLM =>
(forall a b. NLM a -> (a -> NLM b) -> NLM b)
-> (forall a b. NLM a -> NLM b -> NLM b)
-> (forall a. a -> NLM a)
-> Monad NLM
forall a. a -> NLM a
forall a b. NLM a -> NLM b -> NLM b
forall a b. NLM a -> (a -> NLM b) -> NLM 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. NLM a -> (a -> NLM b) -> NLM b
>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
$c>> :: forall a b. NLM a -> NLM b -> NLM b
>> :: forall a b. NLM a -> NLM b -> NLM b
$creturn :: forall a. a -> NLM a
return :: forall a. a -> NLM a
Monad, Monad NLM
Monad NLM =>
(forall a. HasCallStack => String -> NLM a) -> MonadFail NLM
forall a. HasCallStack => String -> NLM a
forall (m :: * -> *).
Monad m =>
(forall a. HasCallStack => String -> m a) -> MonadFail m
$cfail :: forall a. HasCallStack => String -> NLM a
fail :: forall a. HasCallStack => String -> NLM a
MonadFail
           , Applicative NLM
Applicative NLM =>
(forall a. NLM a)
-> (forall a. NLM a -> NLM a -> NLM a)
-> (forall a. NLM a -> NLM [a])
-> (forall a. NLM a -> NLM [a])
-> Alternative NLM
forall a. NLM a
forall a. NLM a -> NLM [a]
forall a. NLM a -> NLM a -> NLM 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. NLM a
empty :: forall a. NLM a
$c<|> :: forall a. NLM a -> NLM a -> NLM a
<|> :: forall a. NLM a -> NLM a -> NLM a
$csome :: forall a. NLM a -> NLM [a]
some :: forall a. NLM a -> NLM [a]
$cmany :: forall a. NLM a -> NLM [a]
many :: forall a. NLM a -> NLM [a]
Alternative, Monad NLM
Alternative NLM
(Alternative NLM, Monad NLM) =>
(forall a. NLM a)
-> (forall a. NLM a -> NLM a -> NLM a) -> MonadPlus NLM
forall a. NLM a
forall a. NLM a -> NLM a -> NLM a
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
$cmzero :: forall a. NLM a
mzero :: forall a. NLM a
$cmplus :: forall a. NLM a -> NLM a -> NLM a
mplus :: forall a. NLM a -> NLM a -> NLM a
MonadPlus
           , MonadError Blocked_, MonadState NLMState
           , Monad NLM
Functor NLM
Applicative NLM
(Functor NLM, Applicative NLM, Monad NLM) =>
(SomeBuiltin -> NLM (Maybe (Builtin PrimFun))) -> HasBuiltins NLM
SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
$cgetBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
getBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
HasBuiltins, Functor NLM
Applicative NLM
HasOptions NLM
MonadTCEnv NLM
MonadDebug NLM
(Functor NLM, Applicative NLM, HasOptions NLM, MonadDebug NLM,
 MonadTCEnv NLM) =>
(HasCallStack => QName -> NLM Definition)
-> (HasCallStack => QName -> NLM (Either SigError Definition))
-> (QName -> NLM GlobalRewriteRules)
-> (RewriteHead -> NLM RewriteRules)
-> HasConstInfo NLM
HasCallStack => QName -> NLM (Either SigError Definition)
HasCallStack => QName -> NLM Definition
QName -> NLM GlobalRewriteRules
RewriteHead -> NLM RewriteRules
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadDebug m,
 MonadTCEnv m) =>
(HasCallStack => QName -> m Definition)
-> (HasCallStack => QName -> m (Either SigError Definition))
-> (QName -> m GlobalRewriteRules)
-> (RewriteHead -> m RewriteRules)
-> HasConstInfo m
$cgetConstInfo :: HasCallStack => QName -> NLM Definition
getConstInfo :: HasCallStack => QName -> NLM Definition
$cgetConstInfo' :: HasCallStack => QName -> NLM (Either SigError Definition)
getConstInfo' :: HasCallStack => QName -> NLM (Either SigError Definition)
$cgetGlobalRewriteRulesFor :: QName -> NLM GlobalRewriteRules
getGlobalRewriteRulesFor :: QName -> NLM GlobalRewriteRules
$cgetLocalRewriteRulesFor :: RewriteHead -> NLM RewriteRules
getLocalRewriteRulesFor :: RewriteHead -> NLM RewriteRules
HasConstInfo, Monad NLM
Functor NLM
Applicative NLM
NLM PragmaOptions
NLM CommandLineOptions
(Functor NLM, Applicative NLM, Monad NLM) =>
NLM PragmaOptions -> NLM CommandLineOptions -> HasOptions NLM
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
m PragmaOptions -> m CommandLineOptions -> HasOptions m
$cpragmaOptions :: NLM PragmaOptions
pragmaOptions :: NLM PragmaOptions
$ccommandLineOptions :: NLM CommandLineOptions
commandLineOptions :: NLM CommandLineOptions
HasOptions, Monad NLM
NLM SessionState
NLM TCState
Monad NLM =>
NLM TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b)
-> NLM SessionState
-> (forall a. (TCState -> TCState) -> NLM a -> NLM a)
-> ReadTCState NLM
forall a. (TCState -> TCState) -> NLM a -> NLM a
forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM 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 :: NLM TCState
getTCState :: NLM TCState
$clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
$cgetSessionState :: NLM SessionState
getSessionState :: NLM SessionState
$cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
withTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
ReadTCState
           , Monad NLM
NLM TCEnv
Monad NLM =>
NLM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a) -> MonadTCEnv NLM
forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
$caskTC :: NLM TCEnv
askTC :: NLM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
localTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
MonadTCEnv, Applicative NLM
HasOptions NLM
MonadTCEnv NLM
ReadTCState NLM
(Applicative NLM, MonadTCEnv NLM, ReadTCState NLM,
 HasOptions NLM) =>
(forall a. ReduceM a -> NLM a) -> MonadReduce NLM
forall a. ReduceM a -> NLM a
forall (m :: * -> *).
(Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
(forall a. ReduceM a -> m a) -> MonadReduce m
$cliftReduce :: forall a. ReduceM a -> NLM a
liftReduce :: forall a. ReduceM a -> NLM a
MonadReduce, MonadTCEnv NLM
MonadTCEnv NLM =>
(forall a. Name -> Dom Type -> NLM a -> NLM a)
-> (forall a.
    IsAxiom -> Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a)
-> (forall a. RewriteRule -> NLM a -> NLM a)
-> (forall a.
    Substitution
    -> (Context' ContextEntry -> Context' ContextEntry)
    -> NLM a
    -> NLM a)
-> (forall a. Range -> String -> (Name -> NLM a) -> NLM a)
-> MonadAddContext NLM
forall a. Range -> String -> (Name -> NLM a) -> NLM a
forall a. Name -> Dom Type -> NLM a -> NLM a
forall a. RewriteRule -> NLM a -> NLM a
forall a.
Substitution
-> (Context' ContextEntry -> Context' ContextEntry)
-> NLM a
-> NLM a
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
forall (m :: * -> *).
MonadTCEnv m =>
(forall a. Name -> Dom Type -> m a -> m a)
-> (forall a.
    IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. RewriteRule -> m a -> m a)
-> (forall a.
    Substitution
    -> (Context' ContextEntry -> Context' ContextEntry) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
$caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
addCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
$caddLetBinding' :: forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
addLetBinding' :: forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
$caddLocalRewrite :: forall a. RewriteRule -> NLM a -> NLM a
addLocalRewrite :: forall a. RewriteRule -> NLM a -> NLM a
$cupdateContext :: forall a.
Substitution
-> (Context' ContextEntry -> Context' ContextEntry)
-> NLM a
-> NLM a
updateContext :: forall a.
Substitution
-> (Context' ContextEntry -> Context' ContextEntry)
-> NLM a
-> NLM a
$cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
withFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
MonadAddContext, Monad NLM
Functor NLM
Applicative NLM
NLM Bool
NLM Verbosity
NLM ProfileOptions
(Functor NLM, Applicative NLM, Monad NLM) =>
(String -> Int -> TCMT IO Doc -> NLM Doc)
-> (forall a. String -> Int -> Doc -> NLM a -> NLM a)
-> (forall a. String -> Int -> String -> NLM a -> NLM a)
-> NLM Verbosity
-> NLM ProfileOptions
-> NLM Bool
-> (forall a. NLM a -> NLM a)
-> MonadDebug NLM
String -> Int -> TCMT IO Doc -> NLM Doc
forall a. String -> Int -> String -> NLM a -> NLM a
forall a. String -> Int -> Doc -> NLM a -> NLM a
forall a. NLM a -> NLM a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
(String -> Int -> TCMT IO Doc -> m Doc)
-> (forall a. String -> Int -> Doc -> m a -> m a)
-> (forall a. String -> Int -> String -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
$cformatDebugMessage :: String -> Int -> TCMT IO Doc -> NLM Doc
formatDebugMessage :: String -> Int -> TCMT IO Doc -> NLM Doc
$ctraceDebugMessage :: forall a. String -> Int -> Doc -> NLM a -> NLM a
traceDebugMessage :: forall a. String -> Int -> Doc -> NLM a -> NLM a
$cverboseBracket :: forall a. String -> Int -> String -> NLM a -> NLM a
verboseBracket :: forall a. String -> Int -> String -> NLM a -> NLM a
$cgetVerbosity :: NLM Verbosity
getVerbosity :: NLM Verbosity
$cgetProfileOptions :: NLM ProfileOptions
getProfileOptions :: NLM ProfileOptions
$cisDebugPrinting :: NLM Bool
isDebugPrinting :: NLM Bool
$cnowDebugPrinting :: forall a. NLM a -> NLM a
nowDebugPrinting :: forall a. NLM a -> NLM a
MonadDebug
           , Monad NLM
Monad NLM =>
(HasCallStack => FileId -> NLM File)
-> (File -> NLM FileId) -> MonadFileId NLM
HasCallStack => FileId -> NLM File
File -> NLM FileId
forall (m :: * -> *).
Monad m =>
(HasCallStack => FileId -> m File)
-> (File -> m FileId) -> MonadFileId m
$cfileFromId :: HasCallStack => FileId -> NLM File
fileFromId :: HasCallStack => FileId -> NLM File
$cidFromFile :: File -> NLM FileId
idFromFile :: File -> NLM FileId
MonadFileId
           , MonadFileId NLM
MonadTCEnv NLM
MonadReduce NLM
ReadTCState NLM
HasBuiltins NLM
MonadAddContext NLM
MonadDebug NLM
HasConstInfo NLM
(HasBuiltins NLM, HasConstInfo NLM, MonadAddContext NLM,
 MonadDebug NLM, MonadFileId NLM, MonadReduce NLM, MonadTCEnv NLM,
 ReadTCState NLM) =>
PureTCM NLM
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
 MonadFileId m, MonadReduce m, MonadTCEnv m, ReadTCState m) =>
PureTCM m
PureTCM
           )

instance MonadBlock NLM where
  patternViolation :: forall a. Blocker -> NLM a
patternViolation Blocker
b = Blocked' Term () -> NLM a
forall a. Blocked' Term () -> NLM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Blocked' Term () -> NLM a) -> Blocked' Term () -> NLM a
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked' Term ()
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()
  catchPatternErr :: forall a. (Blocker -> NLM a) -> NLM a -> NLM a
catchPatternErr Blocker -> NLM a
h NLM a
f = NLM a -> (Blocked' Term () -> NLM a) -> NLM a
forall a. NLM a -> (Blocked' Term () -> NLM a) -> NLM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError NLM a
f ((Blocked' Term () -> NLM a) -> NLM a)
-> (Blocked' Term () -> NLM a) -> NLM a
forall a b. (a -> b) -> a -> b
$ \case
    Blocked Blocker
b ()
_      -> Blocker -> NLM a
h Blocker
b
    err :: Blocked' Term ()
err@NotBlocked{} -> Blocked' Term () -> NLM a
forall a. Blocked' Term () -> NLM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Blocked' Term ()
err

data NLMState = NLMState
  { NLMState -> IntMap (Relevance, Term)
_nlmSub   :: Sub
  , NLMState -> PostponedEquations
_nlmEqs   :: PostponedEquations
  }

instance Null NLMState where
  empty :: NLMState
empty  = NLMState { _nlmSub :: IntMap (Relevance, Term)
_nlmSub = IntMap (Relevance, Term)
forall a. Null a => a
empty , _nlmEqs :: PostponedEquations
_nlmEqs = PostponedEquations
forall a. Null a => a
empty }
  null :: NLMState -> Bool
null NLMState
s = IntMap (Relevance, Term) -> Bool
forall a. Null a => a -> Bool
null (NLMState
s NLMState
-> Getting
     (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
-> IntMap (Relevance, Term)
forall s a. s -> Getting a s a -> a
^. Getting
  (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
Lens' NLMState (IntMap (Relevance, Term))
nlmSub) Bool -> Bool -> Bool
&& PostponedEquations -> Bool
forall a. Null a => a -> Bool
null (NLMState
s NLMState
-> Getting PostponedEquations NLMState PostponedEquations
-> PostponedEquations
forall s a. s -> Getting a s a -> a
^. Getting PostponedEquations NLMState PostponedEquations
Lens' NLMState PostponedEquations
nlmEqs)

nlmSub :: Lens' NLMState Sub
nlmSub :: Lens' NLMState (IntMap (Relevance, Term))
nlmSub IntMap (Relevance, Term) -> f (IntMap (Relevance, Term))
f NLMState
s = IntMap (Relevance, Term) -> f (IntMap (Relevance, Term))
f (NLMState -> IntMap (Relevance, Term)
_nlmSub NLMState
s) f (IntMap (Relevance, Term))
-> (IntMap (Relevance, Term) -> NLMState) -> f NLMState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \IntMap (Relevance, Term)
x -> NLMState
s {_nlmSub = x}

nlmEqs :: Lens' NLMState PostponedEquations
nlmEqs :: Lens' NLMState PostponedEquations
nlmEqs PostponedEquations -> f PostponedEquations
f NLMState
s = PostponedEquations -> f PostponedEquations
f (NLMState -> PostponedEquations
_nlmEqs NLMState
s) f PostponedEquations
-> (PostponedEquations -> NLMState) -> f NLMState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \PostponedEquations
x -> NLMState
s {_nlmEqs = x}

runNLM :: (MonadReduce m) => NLM () -> m (Either Blocked_ NLMState)
runNLM :: forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either (Blocked' Term ()) NLMState)
runNLM NLM ()
nlm = do
  (ok,out) <- ReduceM (Either (Blocked' Term ()) (), NLMState)
-> m (Either (Blocked' Term ()) (), NLMState)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Either (Blocked' Term ()) (), NLMState)
 -> m (Either (Blocked' Term ()) (), NLMState))
-> ReduceM (Either (Blocked' Term ()) (), NLMState)
-> m (Either (Blocked' Term ()) (), NLMState)
forall a b. (a -> b) -> a -> b
$ StateT NLMState ReduceM (Either (Blocked' Term ()) ())
-> NLMState -> ReduceM (Either (Blocked' Term ()) (), NLMState)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m (a, s)
runStateT (ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) ()
-> StateT NLMState ReduceM (Either (Blocked' Term ()) ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) ()
 -> StateT NLMState ReduceM (Either (Blocked' Term ()) ()))
-> ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) ()
-> StateT NLMState ReduceM (Either (Blocked' Term ()) ())
forall a b. (a -> b) -> a -> b
$ NLM () -> ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) ()
forall a.
NLM a -> ExceptT (Blocked' Term ()) (StateT NLMState ReduceM) a
unNLM NLM ()
nlm) NLMState
forall a. Null a => a
empty
  case ok of
    Left Blocked' Term ()
block -> Either (Blocked' Term ()) NLMState
-> m (Either (Blocked' Term ()) NLMState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked' Term ()) NLMState
 -> m (Either (Blocked' Term ()) NLMState))
-> Either (Blocked' Term ()) NLMState
-> m (Either (Blocked' Term ()) NLMState)
forall a b. (a -> b) -> a -> b
$ Blocked' Term () -> Either (Blocked' Term ()) NLMState
forall a b. a -> Either a b
Left Blocked' Term ()
block
    Right ()
_    -> Either (Blocked' Term ()) NLMState
-> m (Either (Blocked' Term ()) NLMState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked' Term ()) NLMState
 -> m (Either (Blocked' Term ()) NLMState))
-> Either (Blocked' Term ()) NLMState
-> m (Either (Blocked' Term ()) NLMState)
forall a b. (a -> b) -> a -> b
$ NLMState -> Either (Blocked' Term ()) NLMState
forall a b. b -> Either a b
Right NLMState
out

matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked :: Blocked' Term () -> NLM ()
matchingBlocked = Blocked' Term () -> NLM ()
forall a. Blocked' Term () -> NLM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError

-- | Add substitution @i |-> v : a@ to result of matching.
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellSub Relevance
r Int
i Type
a Term
v = do
  old <- Int -> IntMap (Relevance, Term) -> Maybe (Relevance, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i (IntMap (Relevance, Term) -> Maybe (Relevance, Term))
-> NLM (IntMap (Relevance, Term)) -> NLM (Maybe (Relevance, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
-> NLM (IntMap (Relevance, Term))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
Lens' NLMState (IntMap (Relevance, Term))
nlmSub
  case old of
    Maybe (Relevance, Term)
Nothing -> (IntMap (Relevance, Term) -> Identity (IntMap (Relevance, Term)))
-> NLMState -> Identity NLMState
Lens' NLMState (IntMap (Relevance, Term))
nlmSub ((IntMap (Relevance, Term) -> Identity (IntMap (Relevance, Term)))
 -> NLMState -> Identity NLMState)
-> (IntMap (Relevance, Term) -> IntMap (Relevance, Term)) -> NLM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Int
-> (Relevance, Term)
-> IntMap (Relevance, Term)
-> IntMap (Relevance, Term)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Relevance
r,Term
v)
    Just (Relevance
r',Term
v')
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r  -> () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r' -> (IntMap (Relevance, Term) -> Identity (IntMap (Relevance, Term)))
-> NLMState -> Identity NLMState
Lens' NLMState (IntMap (Relevance, Term))
nlmSub ((IntMap (Relevance, Term) -> Identity (IntMap (Relevance, Term)))
 -> NLMState -> Identity NLMState)
-> (IntMap (Relevance, Term) -> IntMap (Relevance, Term)) -> NLM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Int
-> (Relevance, Term)
-> IntMap (Relevance, Term)
-> IntMap (Relevance, Term)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Relevance
r,Term
v)
      | Bool
otherwise       -> NLM (Maybe (Blocked' Term ()))
-> (Blocked' Term () -> NLM ()) -> NLM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (Type -> Term -> Term -> NLM (Maybe (Blocked' Term ()))
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Maybe (Blocked' Term ()))
equal Type
a Term
v Term
v') Blocked' Term () -> NLM ()
matchingBlocked

tellEq :: Telescope -> Context -> Type -> Term -> Term -> NLM ()
tellEq :: Tele (Dom Type)
-> Context' ContextEntry -> Type -> Term -> Term -> NLM ()
tellEq Tele (Dom Type)
gamma Context' ContextEntry
k Type
a Term
u Term
v = do
  String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
               [ TCMT IO Doc
"adding equality between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)
               , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
  (PostponedEquations -> Identity PostponedEquations)
-> NLMState -> Identity NLMState
Lens' NLMState PostponedEquations
nlmEqs ((PostponedEquations -> Identity PostponedEquations)
 -> NLMState -> Identity NLMState)
-> (PostponedEquations -> PostponedEquations) -> NLM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (Context' ContextEntry -> Type -> Term -> Term -> PostponedEquation
PostponedEquation Context' ContextEntry
k Type
a Term
u Term
vPostponedEquation -> PostponedEquations -> PostponedEquations
forall a. a -> [a] -> [a]
:)

type Sub = IntMap (Relevance, Term)

-- | Matching against a term produces a constraint
--   which we have to verify after applying
--   the substitution computed by matching.
data PostponedEquation = PostponedEquation
  { PostponedEquation -> Context' ContextEntry
eqFreeVars :: Context -- ^ Context of free variables in the equation
  , PostponedEquation -> Type
eqType :: Type    -- ^ Type of the equation, living in same context as the rhs.
  , PostponedEquation -> Term
eqLhs :: Term     -- ^ Term from pattern, living in pattern context.
  , PostponedEquation -> Term
eqRhs :: Term     -- ^ Term from scrutinee, living in context where matching was invoked.
  }
type PostponedEquations = [PostponedEquation]

-- | Match a non-linear pattern against a neutral term,
--   returning a substitution.

class Match a b where
  match :: Relevance  -- ^ Are we currently matching in an irrelevant context?
        -> Telescope  -- ^ The telescope of pattern variables
        -> Context    -- ^ The context of lambda-bound variables
        -> TypeOf b   -- ^ The type of the pattern
        -> a          -- ^ The pattern to match
        -> b          -- ^ The term to be matched against the pattern
        -> NLM ()

instance Match a b => Match (Arg a) (Arg b) where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Arg b)
-> Arg a
-> Arg b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf (Arg b)
t Arg a
p Arg b
v = let r' :: Relevance
r' = Relevance
r Relevance -> Relevance -> Relevance
`composeRelevance` Arg a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
p
                          in  Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r' Tele (Dom Type)
gamma Context' ContextEntry
k (Dom' Term (TypeOf b) -> TypeOf b
forall t e. Dom' t e -> e
unDom TypeOf (Arg b)
Dom' Term (TypeOf b)
t) (Arg a -> a
forall e. Arg e -> e
unArg Arg a
p) (Arg b -> b
forall e. Arg e -> e
unArg Arg b
v)

instance Match [Elim' NLPat] Elims where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
t, Elims -> Term
hd) [] [] = () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
t, Elims -> Term
hd) [] Elims
_  = Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
  match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
t, Elims -> Term
hd) [Elim' NLPat]
_  [] = Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
  match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
t, Elims -> Term
hd) (Elim' NLPat
p:[Elim' NLPat]
ps) (Elim' Term
v:Elims
vs) =
   String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
50 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
     [ TCMT IO Doc
"matching elimination " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Elim' NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM Elim' NLPat
p)
     , TCMT IO Doc
"  with               " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Elim' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM Elim' Term
v)
     , TCMT IO Doc
"  eliminating head   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t)]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do

   let no :: NLM ()
no  = Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
   case (Elim' NLPat
p,Elim' Term
v) of
    (Apply Arg NLPat
p, Apply Arg Term
v) -> Context' ContextEntry -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> NLM Type -> NLM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM Term -> (Term -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Pi Dom Type
a Abs Type
b -> do
        Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Arg Term)
-> Arg NLPat
-> Arg Term
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf (Arg Term)
Dom Type
a Arg NLPat
p Arg Term
v
        let t' :: Type
t'  = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v)
            hd' :: Elims -> Term
hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
vElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
t',Elims -> Term
hd') [Elim' NLPat]
ps Elims
vs
      Term
t -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
20
        (TCMT IO Doc
"application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t) NLM ()
forall a. NLM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (IApply NLPat
x NLPat
y NLPat
p , IApply Term
u Term
v Term
i) -> Context' ContextEntry -> NLM PathView -> NLM PathView
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Type -> NLM PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView (Type -> NLM PathView) -> NLM Type -> NLM PathView
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM PathView -> (PathView -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
_u Arg Term
_v -> do
        interval <- (TCErr -> Type) -> Either TCErr Type -> Type
forall a b. (a -> b) -> Either a b -> b
fromRight TCErr -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Either TCErr Type -> Type) -> NLM (Either TCErr Type) -> NLM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT TCErr NLM Type -> NLM (Either TCErr Type)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT TCErr NLM Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
        match r gamma k interval p i
        let t' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
i ]
        let hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
u Term
v Term
iElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        match r gamma k (t',hd') ps vs
      PathView
t -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
20
        (TCMT IO Doc
"interval application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (PathView -> Type
pathUnview PathView
t)) NLM ()
forall a. NLM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (Proj ProjOrigin
o QName
f, Proj ProjOrigin
o' QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> do
      Context' ContextEntry -> NLM (Maybe Type) -> NLM (Maybe Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (QName -> Type -> NLM (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> NLM (Maybe Type)) -> NLM Type -> NLM (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM (Maybe Type) -> (Maybe Type -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> do
          let u :: Term
u = Elims -> Term
hd []
              t' :: Type
t' = Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
          hd' <- Context' ContextEntry -> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM (Elims -> Term) -> NLM (Elims -> Term))
-> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Term -> Elims -> Term) -> NLM Term -> NLM (Elims -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProjOrigin -> QName -> Arg Term -> NLM Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
u)
          match r gamma k (t',hd') ps vs
        Maybe Type
_ -> NLM ()
no

    (Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') | Bool
otherwise -> do
      String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
20 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"mismatch between projections " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
        , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f' ]) NLM ()
forall a. NLM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (Apply{}, Proj{} ) -> NLM ()
no
    (Proj{} , Apply{}) -> NLM ()
no

    (IApply{} , Elim' Term
_    ) -> NLM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- TODO
    (Elim' NLPat
_ , IApply{}    ) -> NLM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- TODO

instance Match a b => Match (Dom a) (Dom b) where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Dom b)
-> Dom a
-> Dom b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf (Dom b)
t Dom a
p Dom b
v = Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf b
TypeOf (Dom b)
t (Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
p) (Dom b -> b
forall t e. Dom' t e -> e
unDom Dom b
v)

instance Match NLPType Type where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Type
-> NLPType
-> Type
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf Type
_ (NLPType NLPSort
sp NLPat
p) (El Sort
s Term
a) = NLM () -> NLM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Sort
-> NLPSort
-> Sort
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k () NLPSort
sp Sort
s
    Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Term
-> NLPat
-> Term
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Sort -> Type
sort Sort
s) NLPat
p Term
a

instance Match NLPSort Sort where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Sort
-> NLPSort
-> Sort
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf Sort
_ NLPSort
p Sort
s = do
    bs <- Context' ContextEntry -> NLM (Blocked Sort) -> NLM (Blocked Sort)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM (Blocked Sort) -> NLM (Blocked Sort))
-> NLM (Blocked Sort) -> NLM (Blocked Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> NLM (Blocked Sort)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s
    let b = Blocked Sort -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked Sort
bs
        s = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
bs
        yes = () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no  = Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
    traceSDoc "rewriting.match" 30 (sep
      [ "matching pattern " <+> addContext gamma (addContext k $ prettyTCM p)
      , "  with sort      " <+> addContext k (prettyTCM s) ]) $ do
    case (p , s) of
      (PUniv Univ
u NLPat
lp    , Univ Univ
u' Level' Term
l) | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u'          -> Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Level' Term)
-> NLPat
-> Level' Term
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k () NLPat
lp Level' Term
l
      (PInf Univ
up Integer
np    , Inf Univ
u Integer
n)   | Univ
up Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u, Integer
np Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n -> NLM ()
yes
      (NLPSort
PSizeUniv     , Sort
SizeUniv)                     -> NLM ()
yes
      (NLPSort
PLockUniv     , Sort
LockUniv)                     -> NLM ()
yes
      (NLPSort
PLevelUniv    , Sort
LevelUniv)                    -> NLM ()
yes
      (NLPSort
PIntervalUniv , Sort
IntervalUniv)                 -> NLM ()
yes

      -- blocked cases
      (NLPSort
_ , UnivSort{}) -> Blocked' Term () -> NLM ()
matchingBlocked Blocked' Term ()
b
      (NLPSort
_ , PiSort{}  ) -> Blocked' Term () -> NLM ()
matchingBlocked Blocked' Term ()
b
      (NLPSort
_ , FunSort{} ) -> Blocked' Term () -> NLM ()
matchingBlocked Blocked' Term ()
b
      (NLPSort
_ , MetaS MetaId
m Elims
_ ) -> Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocked' Term ()
forall t. MetaId -> Blocked' t ()
blocked_ MetaId
m

      -- all other cases do not match
      (NLPSort
_ , Sort
_) -> NLM ()
no

instance Match NLPat Level where
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Level' Term)
-> NLPat
-> Level' Term
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k TypeOf (Level' Term)
_ NLPat
p Level' Term
l = do
    t <- Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Type) -> NLM (Maybe Term) -> NLM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> NLM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevel
    v <- reallyUnLevelView l
    match r gamma k t p v

instance Match NLPat Term where
  match :: Relevance  -- Are we currently matching in an irrelevant context?
        -> Telescope  -- The telescope of pattern variables
        -> Context    -- The context of lambda-bound variables
        -> Type       -- The type of the pattern
        -> NLPat      -- The pattern to match
        -> Term       -- The term to be matched against the pattern
        -> NLM ()
  match :: Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> Type
-> NLPat
-> Term
-> NLM ()
match Relevance
r0 Tele (Dom Type)
gamma Context' ContextEntry
k Type
t NLPat
p Term
v = do
    vbt <- Context' ContextEntry
-> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type)))
-> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
forall a b. (a -> b) -> a -> b
$ (Term, Type) -> NLM (Blocked (Term, Type))
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB (Term
v,Type
t)
    let n = Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
k
        b = Blocked (Term, Type) -> Blocked' Term ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked (Term, Type)
vbt
        (v,t) = ignoreBlocking vbt
        prettyPat  = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
p
        prettyTerm = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
        prettyType = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    etaRecord <- addContext k $ isEtaRecordType t
    pview <- pathViewAsPi'whnf
    prop <- fromRight __IMPOSSIBLE__ <.> runBlocked . addContext k $ isPropM t
    let r = if Bool
prop then Relevance
irrelevant else Relevance
r0
    traceSDoc "rewriting.match" 30 (sep
      [ "matching pattern " <+> prettyPat
      , "  with term      " <+> prettyTerm
      , "  of type        " <+> prettyType ]) $ do
    traceSDoc "rewriting.match" 80 (vcat
      [ "  raw pattern:  " <+> text (show p)
      , "  raw term:     " <+> text (show v)
      , "  raw type:     " <+> text (show t) ]) $ do
    traceSDoc "rewriting.match" 70 (vcat
      [ "pattern vars:   " <+> prettyTCM gamma
      , "bound vars:     " <+> prettyTCM k ]) $ do
    let yes = () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no TCMT IO Doc
msg = if Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r then NLM ()
yes else do
          String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"mismatch between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyPat
            , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyTerm
            , TCMT IO Doc
" of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyType
            , TCMT IO Doc
msg ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked' Term () -> String
forall a. Show a => a -> String
show Blocked' Term ()
b) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          Blocked' Term () -> NLM ()
matchingBlocked Blocked' Term ()
b
        block Blocked' Term ()
b' = if Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r then NLM ()
yes else do
          String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"matching blocked on meta"
            , String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked' Term () -> String
forall a. Show a => a -> String
show Blocked' Term ()
b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked' Term () -> String
forall a. Show a => a -> String
show Blocked' Term ()
b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term ()
b Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Monoid a => a -> a -> a
`mappend` Blocked' Term ()
b')
        maybeBlock = \case
          MetaV MetaId
m Elims
es -> Blocked' Term () -> NLM ()
matchingBlocked (Blocked' Term () -> NLM ()) -> Blocked' Term () -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocked' Term ()
forall t. MetaId -> Blocked' t ()
blocked_ MetaId
m
          Term
_          -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
    case p of
      PVar DefSing
s Int
i [Arg Int]
bvs -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
60 (TCMT IO Doc
"matching a PVar: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        case Int
n of
          Int
0 -> Relevance -> Int -> Type -> Term -> NLM ()
tellSub Relevance
r (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) Type
t Term
v
          Int
_ -> do
            let vars :: [Int]
vars = (Arg Int -> Int) -> [Arg Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Int -> Int
forall e. Arg e -> e
unArg [Arg Int]
bvs
            let allowedVars :: VarSet
                allowedVars :: VarSet
allowedVars = [Int] -> VarSet
VarSet.fromList [Int]
vars
                badVars :: VarSet
                badVars :: VarSet
badVars = Int -> VarSet -> VarSet
VarSet.complement Int
n VarSet
allowedVars
                perm :: Permutation
                perm :: Permutation
perm = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
vars
                tel :: Telescope
                tel :: Tele (Dom Type)
tel = Permutation -> Context' ContextEntry -> Tele (Dom Type)
permuteContext Permutation
perm Context' ContextEntry
k
            ok <- Context' ContextEntry
-> NLM (Either (Blocked' Term ()) (Maybe Term))
-> NLM (Either (Blocked' Term ()) (Maybe Term))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM (Either (Blocked' Term ()) (Maybe Term))
 -> NLM (Either (Blocked' Term ()) (Maybe Term)))
-> NLM (Either (Blocked' Term ()) (Maybe Term))
-> NLM (Either (Blocked' Term ()) (Maybe Term))
forall a b. (a -> b) -> a -> b
$ ReduceM (Either (Blocked' Term ()) (Maybe Term))
-> NLM (Either (Blocked' Term ()) (Maybe Term))
forall a. ReduceM a -> NLM a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Either (Blocked' Term ()) (Maybe Term))
 -> NLM (Either (Blocked' Term ()) (Maybe Term)))
-> ReduceM (Either (Blocked' Term ()) (Maybe Term))
-> NLM (Either (Blocked' Term ()) (Maybe Term))
forall a b. (a -> b) -> a -> b
$ VarSet -> Term -> ReduceM (Either (Blocked' Term ()) (Maybe Term))
forall a.
(Reduce a, ForceNotFree a) =>
VarSet -> a -> ReduceM (Either (Blocked' Term ()) (Maybe a))
reallyFree VarSet
badVars Term
v
            case ok of
              Left Blocked' Term ()
b         -> Blocked' Term () -> NLM ()
block Blocked' Term ()
b
              Right Maybe Term
Nothing  -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
              Right (Just Term
v) ->
                let t' :: Type
t' = Tele (Dom Type) -> Type -> Type
telePi  Tele (Dom Type)
tel (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Impossible -> Permutation -> Type -> Type
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible Permutation
perm Type
t
                    v' :: Term
v' = Tele (Dom Type) -> Term -> Term
teleLam Tele (Dom Type)
tel (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Impossible -> Permutation -> Term -> Term
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible Permutation
perm Term
v
                in Relevance -> Int -> Type -> Term -> NLM ()
tellSub Relevance
r (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) Type
t' Term
v'

      PDef QName
f [Elim' NLPat]
ps -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
60 (TCMT IO Doc
"matching a PDef: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        v <- Context' ContextEntry -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
forall a b. (a -> b) -> a -> b
$ Term -> NLM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Term -> NLM Term) -> NLM Term -> NLM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> NLM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
        case v of
          Def QName
f' Elims
es
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'   -> do
                ft <- Context' ContextEntry -> NLM Type -> NLM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM Type -> NLM Type) -> NLM Type -> NLM Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType (Definition -> Type) -> NLM Definition -> NLM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> NLM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
                match r gamma k (ft , Def f) ps es
          Con ConHead
c ConInfo
ci Elims
vs
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c -> do
                Context' ContextEntry
-> NLM (Maybe ((QName, Type, Args), Type))
-> NLM (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) NLM (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Just ((QName, Type, Args)
_ , Type
ct) -> Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) [Elim' NLPat]
ps Elims
vs
                  Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
          Term
_ | Pi Dom Type
a Abs Type
b <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
t -> do
            let ai :: ArgInfo
ai    = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
                pbody :: NLPat
pbody = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Int -> a -> a
raise Int
1 [Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++! [ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NLPat -> Arg NLPat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
                body :: Term
body  = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
            k' <- Context' ContextEntry
-> String -> Dom Type -> NLM (Context' ContextEntry)
forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
            match r gamma k' (absBody b) pbody body
          Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          -- If v is not of record constructor form but we are matching at record
          -- type, e.g., we eta-expand both v to (c vs) and
          -- the pattern (p = PDef f ps) to @c (p .f1) ... (p .fn)@.
            RecordDefn def <- Context' ContextEntry -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> NLM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
            (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
            addContext k (getFullyAppliedConType c t) >>= \case
              Just ((QName, Type, Args)
_ , Type
ct) -> do
                let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
def
                    mkField :: QName -> NLPat
mkField QName
fld = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++! [ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])
                    -- Issue #3335: when matching against the record constructor,
                    -- don't add projections but take record field directly.
                    ps' :: [Elim' NLPat]
ps'
                      | ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f = [Elim' NLPat]
ps
                      | Bool
otherwise      = (Arg QName -> Elim' NLPat) -> [Arg QName] -> [Elim' NLPat]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat)
-> (Arg QName -> Arg NLPat) -> Arg QName -> Elim' NLPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
                Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
ct, ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) [Elim' NLPat]
ps' ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs)
              Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
          Term
v -> Term -> NLM ()
maybeBlock Term
v
      PLam ArgInfo
i Abs NLPat
p' -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b -> do
          let body :: Term
body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Int -> Term
var Int
0)]
          k' <- Context' ContextEntry
-> String -> Dom Type -> NLM (Context' ContextEntry)
forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' (absBody b) (absBody p') body
        Term
_ | Left ((Dom Type
a,Abs Type
b),(Term
x,Term
y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview Type
t -> do
          let body :: Term
body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
x) (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
y) (Term -> Elim' Term) -> Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
          k' <- Context' ContextEntry
-> String -> Dom Type -> NLM (Context' ContextEntry)
forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
k String
"i" Dom Type
a
          match r gamma k' (absBody b) (absBody p') body
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PPi Dom' Term NLPType
pa Abs NLPType
pb -> case Term
v of
        Pi Dom Type
a Abs Type
b -> do
          Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf (Dom Type)
-> Dom' Term NLPType
-> Dom Type
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k () Dom' Term NLPType
pa Dom Type
a
          k' <- Context' ContextEntry
-> String -> Dom Type -> NLM (Context' ContextEntry)
forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' () (absBody pb) (absBody b)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PSort NLPSort
ps -> case Term
v of
        Sort Sort
s -> Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Sort
-> NLPSort
-> Sort
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k () NLPSort
ps Sort
s
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PBoundVar Int
i [Elim' NLPat]
ps -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
60
          (TCMT IO Doc
"Matching a PBoundVar" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (NLPat -> TCMT IO Doc) -> NLPat -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i [Elim' NLPat]
ps) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            (Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ case Term
v of
        -- Either we are matching a higher order bound variable in k or we
        -- are matching a locally bound variable outside gamma
        -- (gamma is the rewrite telescope - i.e. the telescope of pattern
        -- variables which are in scope in the pattern but not in the term we
        -- matching against)
        Var Int
i' Elims
es |  (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
k Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i')
                  Bool -> Bool -> Bool
|| (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
k Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma) -> do
          ti <- Tele (Dom Type) -> NLM Type -> NLM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (NLM Type -> NLM Type) -> NLM Type -> NLM Type
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> NLM Type -> NLM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM Type -> NLM Type) -> NLM Type -> NLM Type
forall a b. (a -> b) -> a -> b
$ Int -> NLM Type
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
typeOfBV Int
i
          match r gamma k (ti , Var i) ps es
        Term
_ | Pi Dom Type
a Abs Type
b <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
t -> do
          let ai :: ArgInfo
ai    = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
              pbody :: NLPat
pbody = Int -> [Elim' NLPat] -> NLPat
PBoundVar (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Int -> a -> a
raise Int
1 [Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++! [ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NLPat -> Arg NLPat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
              body :: Term
body  = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ 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
$ Int -> Term
var Int
0 ]
          k' <- Context' ContextEntry
-> String -> Dom Type -> NLM (Context' ContextEntry)
forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' (absBody b) pbody body
        Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          RecordDefn def <- Context' ContextEntry -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> NLM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
          (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
          addContext k (getFullyAppliedConType c t) >>= \case
            Just ((QName, Type, Args)
_ , Type
ct) -> do
              let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
def
                  ps' :: [Arg NLPat]
ps'  = (Arg QName -> Arg NLPat) -> [Arg QName] -> [Arg NLPat]
forall a b. (a -> b) -> [a] -> [b]
map' ((QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
-> (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ \QName
fld -> Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i ([Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++! [ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])) [Arg QName]
flds
              Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
r Tele (Dom Type)
gamma Context' ContextEntry
k (Type
ct, ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) ((Arg NLPat -> Elim' NLPat) -> [Arg NLPat] -> [Elim' NLPat]
forall a b. (a -> b) -> [a] -> [b]
map' Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply [Arg NLPat]
ps') ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs)
            Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PTerm Term
u -> String -> Int -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
60 (TCMT IO Doc
"matching a PTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$
        -- #8231: We need to skip testing conversion if we are matching at
        -- at irrelevant relevance
        Bool -> NLM () -> NLM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> Context' ContextEntry -> Type -> Term -> Term -> NLM ()
tellEq Tele (Dom Type)
gamma Context' ContextEntry
k Type
t Term
u Term
v

extendContext :: MonadAddContext m => Context -> ArgName -> Dom Type -> m Context
extendContext :: forall (m :: * -> *).
MonadAddContext m =>
Context' ContextEntry
-> String -> Dom Type -> m (Context' ContextEntry)
extendContext Context' ContextEntry
cxt String
x Dom Type
a = Range
-> String
-> (Name -> m (Context' ContextEntry))
-> m (Context' ContextEntry)
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Null a => a
empty String
x \Name
y -> Context' ContextEntry -> m (Context' ContextEntry)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Context' ContextEntry -> m (Context' ContextEntry))
-> Context' ContextEntry -> m (Context' ContextEntry)
forall a b. (a -> b) -> a -> b
$ Name -> Dom Type -> Context' ContextEntry -> Context' ContextEntry
CxExtendVar Name
y Dom Type
a Context' ContextEntry
cxt


makeSubstitution :: Telescope -> Sub -> Maybe Substitution
makeSubstitution :: Tele (Dom Type) -> IntMap (Relevance, Term) -> Maybe Substitution
makeSubstitution Tele (Dom Type)
gamma IntMap (Relevance, Term)
sub =
  [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> Maybe [Term] -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Maybe Term) -> [Int] -> Maybe [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Int -> Maybe Term
val [Int
0 .. Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gammaInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
    where
      val :: Int -> Maybe Term
val Int
i = Int -> IntMap (Relevance, Term) -> Maybe (Relevance, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap (Relevance, Term)
sub Maybe (Relevance, Term)
-> ((Relevance, Term) -> Term) -> Maybe Term
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (Relevance
rel, Term
v) -> Bool -> (Term -> Term) -> Term -> Term
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel) Term -> Term
dontCare Term
v

{-# SPECIALIZE checkPostponedEquations :: Substitution -> PostponedEquations -> TCM (Maybe Blocked_) #-}
checkPostponedEquations :: PureTCM m
                        => Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations :: forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe (Blocked' Term ()))
checkPostponedEquations Substitution
sub PostponedEquations
eqs = PostponedEquations
-> (PostponedEquation -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ()))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' PostponedEquations
eqs ((PostponedEquation -> m (Maybe (Blocked' Term ())))
 -> m (Maybe (Blocked' Term ())))
-> (PostponedEquation -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$
  \ (PostponedEquation Context' ContextEntry
k Type
a Term
lhs Term
rhs) -> do
      let lhs' :: Term
lhs' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
k) Substitution
sub) Term
lhs
      String
-> Int
-> TCMT IO Doc
-> m (Maybe (Blocked' Term ()))
-> m (Maybe (Blocked' Term ()))
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking postponed equality between" , Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs')
        , TCMT IO Doc
" and " , Context' ContextEntry -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs) ]) (m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$ do
      Context' ContextEntry
-> m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ()))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Context' ContextEntry -> m a -> m a
addContext Context' ContextEntry
k (m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> m (Maybe (Blocked' Term ()))
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Maybe (Blocked' Term ()))
equal Type
a Term
lhs' Term
rhs

-- main function
nonLinMatch :: (PureTCM m, Match a b)
            => Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch :: forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Tele (Dom Type)
-> TypeOf b -> a -> b -> m (Either (Blocked' Term ()) Substitution)
nonLinMatch Tele (Dom Type)
gamma TypeOf b
t a
p b
v = do
  let no :: String -> a -> m (Either a b)
no String
msg a
b = String -> Int -> TCMT IO Doc -> m (Either a b) -> m (Either a b)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                   [ TCMT IO Doc
"matching failed during" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
msg
                   , TCMT IO Doc
"blocking: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Show a => a -> String
show a
b) ]) (m (Either a b) -> m (Either a b))
-> m (Either a b) -> m (Either a b)
forall a b. (a -> b) -> a -> b
$ Either a b -> m (Either a b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either a b
forall a b. a -> Either a b
Left a
b)
  m (Either (Blocked' Term ()) NLMState)
-> (Blocked' Term () -> m (Either (Blocked' Term ()) Substitution))
-> (NLMState -> m (Either (Blocked' Term ()) Substitution))
-> m (Either (Blocked' Term ()) Substitution)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (NLM () -> m (Either (Blocked' Term ()) NLMState)
forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either (Blocked' Term ()) NLMState)
runNLM (NLM () -> m (Either (Blocked' Term ()) NLMState))
-> NLM () -> m (Either (Blocked' Term ()) NLMState)
forall a b. (a -> b) -> a -> b
$ Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
forall a b.
Match a b =>
Relevance
-> Tele (Dom Type)
-> Context' ContextEntry
-> TypeOf b
-> a
-> b
-> NLM ()
match Relevance
relevant Tele (Dom Type)
gamma Context' ContextEntry
forall a. Null a => a
empty TypeOf b
t a
p b
v) (String
-> Blocked' Term () -> m (Either (Blocked' Term ()) Substitution)
forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"matching") ((NLMState -> m (Either (Blocked' Term ()) Substitution))
 -> m (Either (Blocked' Term ()) Substitution))
-> (NLMState -> m (Either (Blocked' Term ()) Substitution))
-> m (Either (Blocked' Term ()) Substitution)
forall a b. (a -> b) -> a -> b
$ \ NLMState
s -> do
    let msub :: Maybe Substitution
msub = Tele (Dom Type) -> IntMap (Relevance, Term) -> Maybe Substitution
makeSubstitution Tele (Dom Type)
gamma (IntMap (Relevance, Term) -> Maybe Substitution)
-> IntMap (Relevance, Term) -> Maybe Substitution
forall a b. (a -> b) -> a -> b
$ NLMState
s NLMState
-> Getting
     (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
-> IntMap (Relevance, Term)
forall s a. s -> Getting a s a -> a
^. Getting
  (IntMap (Relevance, Term)) NLMState (IntMap (Relevance, Term))
Lens' NLMState (IntMap (Relevance, Term))
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
s NLMState
-> Getting PostponedEquations NLMState PostponedEquations
-> PostponedEquations
forall s a. s -> Getting a s a -> a
^. Getting PostponedEquations NLMState PostponedEquations
Lens' NLMState PostponedEquations
nlmEqs
    String
-> Int
-> TCMT IO Doc
-> m (Either (Blocked' Term ()) Substitution)
-> m (Either (Blocked' Term ()) Substitution)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
90 (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"msub = " String -> String -> String
forall a. [a] -> [a] -> [a]
++! Maybe Substitution -> String
forall a. Show a => a -> String
show Maybe Substitution
msub) (m (Either (Blocked' Term ()) Substitution)
 -> m (Either (Blocked' Term ()) Substitution))
-> m (Either (Blocked' Term ()) Substitution)
-> m (Either (Blocked' Term ()) Substitution)
forall a b. (a -> b) -> a -> b
$ case Maybe Substitution
msub of
      Maybe Substitution
Nothing -> String
-> Blocked' Term () -> m (Either (Blocked' Term ()) Substitution)
forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"checking that all variables are bound" Blocked' Term ()
forall t. Blocked' t ()
notBlocked_
      Just Substitution
sub -> do
        ok <- Substitution -> PostponedEquations -> m (Maybe (Blocked' Term ()))
forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe (Blocked' Term ()))
checkPostponedEquations Substitution
sub PostponedEquations
eqs
        case ok of
          Maybe (Blocked' Term ())
Nothing -> Either (Blocked' Term ()) Substitution
-> m (Either (Blocked' Term ()) Substitution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocked' Term ()) Substitution
 -> m (Either (Blocked' Term ()) Substitution))
-> Either (Blocked' Term ()) Substitution
-> m (Either (Blocked' Term ()) Substitution)
forall a b. (a -> b) -> a -> b
$ Substitution -> Either (Blocked' Term ()) Substitution
forall a b. b -> Either a b
Right Substitution
sub
          Just Blocked' Term ()
b  -> String
-> Blocked' Term () -> m (Either (Blocked' Term ()) Substitution)
forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"checking of postponed equations" Blocked' Term ()
b

-- | Typed βη-equality, also handles empty record types.
--   Returns `Nothing` if the terms are equal, or `Just b` if the terms are not
--   (where b contains information about possible metas blocking the comparison)
equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)
equal :: forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Maybe (Blocked' Term ()))
equal Type
a Term
u Term
v = Type -> Term -> Term -> m (Either Blocker Bool)
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Either Blocker Bool)
pureBlockOrEqualTermPureTCM Type
a Term
u Term
v m (Either Blocker Bool)
-> (Either Blocker Bool -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ()))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left Blocker
b      -> Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ()))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ())))
-> Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$ Blocked' Term () -> Maybe (Blocked' Term ())
forall a. a -> Maybe a
Just (Blocked' Term () -> Maybe (Blocked' Term ()))
-> Blocked' Term () -> Maybe (Blocked' Term ())
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked' Term ()
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()
  Right Bool
True  -> Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ()))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Blocked' Term ())
forall a. Maybe a
Nothing
  Right Bool
False -> String
-> Int
-> TCMT IO Doc
-> m (Maybe (Blocked' Term ()))
-> m (Maybe (Blocked' Term ()))
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Int
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"mismatch between " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ]) (m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ())))
-> m (Maybe (Blocked' Term ())) -> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$ do
    Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ()))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ())))
-> Maybe (Blocked' Term ()) -> m (Maybe (Blocked' Term ()))
forall a b. (a -> b) -> a -> b
$ Blocked' Term () -> Maybe (Blocked' Term ())
forall a. a -> Maybe a
Just (Blocked' Term () -> Maybe (Blocked' Term ()))
-> Blocked' Term () -> Maybe (Blocked' Term ())
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()

-- | Utility function for getting the name and type of a head term (i.e. a
--   `Def` or `Con` with no arguments)
--   Fails on variable heads
getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead :: forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead Term
x = do
  t <- Term -> m (Maybe (Maybe QName, Type))
forall (m :: * -> *).
PureTCM m =>
Term -> m (Maybe (Maybe QName, Type))
getLocalHeadType Term
x
  case t of
    Just (Just QName
f,  Type
t) -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (QName, Type) -> m (Maybe (QName, Type)))
-> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a b. (a -> b) -> a -> b
$ (QName, Type) -> Maybe (QName, Type)
forall a. a -> Maybe a
Just (QName
f, Type
t)
    Just (Maybe QName
Nothing, Type
t) -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, Type)
forall a. Maybe a
Nothing
    Maybe (Maybe QName, Type)
Nothing           -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, Type)
forall a. Maybe a
Nothing

-- | Utility function for getting the type of a head term. Includes a case
--   for variables (which are valid heads of local rewrite rules)
getLocalHeadType :: PureTCM m => Term -> m (Maybe (Maybe QName, Type))
getLocalHeadType :: forall (m :: * -> *).
PureTCM m =>
Term -> m (Maybe (Maybe QName, Type))
getLocalHeadType =  \case
  Def QName
f []   -> (Maybe QName, Type) -> Maybe (Maybe QName, Type)
forall a. a -> Maybe a
Just ((Maybe QName, Type) -> Maybe (Maybe QName, Type))
-> (Definition -> (Maybe QName, Type))
-> Definition
-> Maybe (Maybe QName, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f,) (Type -> (Maybe QName, Type))
-> (Definition -> Type) -> Definition -> (Maybe QName, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> Maybe (Maybe QName, Type))
-> m Definition -> m (Maybe (Maybe QName, Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
  Con (ConHead { conName :: ConHead -> QName
conName = QName
c }) ConInfo
_ [] -> do
    -- Andreas, 2018-09-08, issue #3211:
    -- discount module parameters for constructor heads
    vs <- QName -> m Args
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Args
freeVarsToApply QName
c
    -- Jesper, 2020-06-17, issue #4755: add dummy arguments in
    -- case we don't have enough parameters
    getNumberOfParameters c >>= \case
      Just Int
npars -> do
        let ws :: Args
ws = Int -> Arg Term -> Args
forall a. Int -> a -> [a]
replicate' (Int
npars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
vs) (Arg Term -> Args) -> Arg Term -> Args
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
HasCallStack => Term
__DUMMY_TERM__
        t0 <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
c
        t <- t0 `piApplyM` (vs ++! ws)
        return $ Just (Just c , t)
      Maybe Int
Nothing -> Maybe (Maybe QName, Type) -> m (Maybe (Maybe QName, Type))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Maybe QName, Type)
forall a. Maybe a
Nothing
  Var Int
x [] -> do
    t <- Int -> m (Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
x
    pure $ Just (Nothing, unDom t)
  Term
_ -> Maybe (Maybe QName, Type) -> m (Maybe (Maybe QName, Type))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Maybe QName, Type)
forall a. Maybe a
Nothing