{-# 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        ( void )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
import Control.Monad.State  ( MonadState, StateT, runStateT )

import qualified Control.Monad.Fail as Fail

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

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

import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Irrelevance (workOnTypes, isPropM)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad hiding (constructorForm)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive.Cubical

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
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.Impossible


-- | Monad for non-linear matching.
newtype NLM a = NLM { NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a }
  deriving ( a -> NLM b -> NLM a
(a -> b) -> NLM a -> NLM b
(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
<$ :: a -> NLM b -> NLM a
$c<$ :: forall a b. a -> NLM b -> NLM a
fmap :: (a -> b) -> NLM a -> NLM b
$cfmap :: forall a b. (a -> b) -> NLM a -> NLM b
Functor, Functor NLM
a -> NLM a
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
NLM a -> NLM b -> NLM b
NLM a -> NLM b -> NLM a
NLM (a -> b) -> NLM a -> NLM b
(a -> b -> c) -> NLM a -> NLM b -> NLM c
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
<* :: NLM a -> NLM b -> NLM a
$c<* :: forall a b. NLM a -> NLM b -> NLM a
*> :: NLM a -> NLM b -> NLM b
$c*> :: forall a b. NLM a -> NLM b -> NLM b
liftA2 :: (a -> b -> c) -> NLM a -> NLM b -> NLM c
$cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
<*> :: NLM (a -> b) -> NLM a -> NLM b
$c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
pure :: a -> NLM a
$cpure :: forall a. a -> NLM a
$cp1Applicative :: Functor NLM
Applicative, Applicative NLM
a -> NLM a
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
NLM a -> (a -> NLM b) -> NLM b
NLM a -> NLM b -> NLM b
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
return :: a -> NLM a
$creturn :: forall a. a -> NLM a
>> :: NLM a -> NLM b -> NLM b
$c>> :: forall a b. NLM a -> NLM b -> NLM b
>>= :: NLM a -> (a -> NLM b) -> NLM b
$c>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
$cp1Monad :: Applicative NLM
Monad, Monad NLM
Monad NLM -> (forall a. String -> NLM a) -> MonadFail NLM
String -> NLM a
forall a. String -> NLM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> NLM a
$cfail :: forall a. String -> NLM a
$cp1MonadFail :: Monad NLM
Fail.MonadFail
           , Applicative NLM
NLM a
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
NLM a -> NLM a -> NLM a
NLM a -> NLM [a]
NLM a -> NLM [a]
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
many :: NLM a -> NLM [a]
$cmany :: forall a. NLM a -> NLM [a]
some :: NLM a -> NLM [a]
$csome :: forall a. NLM a -> NLM [a]
<|> :: NLM a -> NLM a -> NLM a
$c<|> :: forall a. NLM a -> NLM a -> NLM a
empty :: NLM a
$cempty :: forall a. NLM a
$cp1Alternative :: Applicative NLM
Alternative, Monad NLM
Alternative NLM
NLM a
Alternative NLM
-> Monad NLM
-> (forall a. NLM a)
-> (forall a. NLM a -> NLM a -> NLM a)
-> MonadPlus NLM
NLM a -> NLM a -> NLM a
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
mplus :: NLM a -> NLM a -> NLM a
$cmplus :: forall a. NLM a -> NLM a -> NLM a
mzero :: NLM a
$cmzero :: forall a. NLM a
$cp2MonadPlus :: Monad NLM
$cp1MonadPlus :: Alternative NLM
MonadPlus
           , MonadError Blocked_, MonadState NLMState
           , Functor NLM
MonadFail NLM
Applicative NLM
Functor NLM
-> Applicative NLM
-> MonadFail NLM
-> (String -> NLM (Maybe (Builtin PrimFun)))
-> HasBuiltins NLM
String -> NLM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> (String -> m (Maybe (Builtin PrimFun)))
-> HasBuiltins m
getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
$cgetBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
$cp3HasBuiltins :: MonadFail NLM
$cp2HasBuiltins :: Applicative NLM
$cp1HasBuiltins :: Functor NLM
HasBuiltins, Functor NLM
MonadFail NLM
Applicative NLM
MonadDebug NLM
HasOptions NLM
MonadTCEnv NLM
Functor NLM
-> Applicative NLM
-> MonadFail NLM
-> HasOptions NLM
-> MonadDebug NLM
-> MonadTCEnv NLM
-> (QName -> NLM Definition)
-> (QName -> NLM (Either SigError Definition))
-> (QName -> NLM RewriteRules)
-> HasConstInfo NLM
QName -> NLM RewriteRules
QName -> NLM (Either SigError Definition)
QName -> NLM Definition
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> HasOptions m
-> MonadDebug m
-> MonadTCEnv m
-> (QName -> m Definition)
-> (QName -> m (Either SigError Definition))
-> (QName -> m RewriteRules)
-> HasConstInfo m
getRewriteRulesFor :: QName -> NLM RewriteRules
$cgetRewriteRulesFor :: QName -> NLM RewriteRules
getConstInfo' :: QName -> NLM (Either SigError Definition)
$cgetConstInfo' :: QName -> NLM (Either SigError Definition)
getConstInfo :: QName -> NLM Definition
$cgetConstInfo :: QName -> NLM Definition
$cp6HasConstInfo :: MonadTCEnv NLM
$cp5HasConstInfo :: MonadDebug NLM
$cp4HasConstInfo :: HasOptions NLM
$cp3HasConstInfo :: MonadFail NLM
$cp2HasConstInfo :: Applicative NLM
$cp1HasConstInfo :: Functor NLM
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
commandLineOptions :: NLM CommandLineOptions
$ccommandLineOptions :: NLM CommandLineOptions
pragmaOptions :: NLM PragmaOptions
$cpragmaOptions :: NLM PragmaOptions
$cp3HasOptions :: Monad NLM
$cp2HasOptions :: Applicative NLM
$cp1HasOptions :: Functor NLM
HasOptions, Monad NLM
NLM TCState
Monad NLM
-> NLM TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b)
-> (forall a. (TCState -> TCState) -> NLM a -> NLM a)
-> ReadTCState NLM
(TCState -> TCState) -> NLM a -> NLM a
Lens' a TCState -> (a -> a) -> NLM b -> NLM b
forall a. (TCState -> TCState) -> NLM a -> NLM a
forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: (TCState -> TCState) -> NLM a -> NLM a
$cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
locallyTCState :: Lens' a TCState -> (a -> a) -> NLM b -> NLM b
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
getTCState :: NLM TCState
$cgetTCState :: NLM TCState
$cp1ReadTCState :: Monad NLM
ReadTCState
           , Monad NLM
NLM TCEnv
Monad NLM
-> NLM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a)
-> MonadTCEnv NLM
(TCEnv -> TCEnv) -> NLM a -> NLM a
forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: (TCEnv -> TCEnv) -> NLM a -> NLM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
askTC :: NLM TCEnv
$caskTC :: NLM TCEnv
$cp1MonadTCEnv :: Monad NLM
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
ReduceM a -> NLM a
forall a. ReduceM a -> NLM a
forall (m :: * -> *).
Applicative m
-> MonadTCEnv m
-> ReadTCState m
-> HasOptions m
-> (forall a. ReduceM a -> m a)
-> MonadReduce m
liftReduce :: ReduceM a -> NLM a
$cliftReduce :: forall a. ReduceM a -> NLM a
$cp4MonadReduce :: HasOptions NLM
$cp3MonadReduce :: ReadTCState NLM
$cp2MonadReduce :: MonadTCEnv NLM
$cp1MonadReduce :: Applicative NLM
MonadReduce, MonadTCEnv NLM
Range -> String -> (Name -> NLM a) -> NLM a
Name -> Term -> Dom Type -> NLM a -> NLM a
Name -> Dom Type -> NLM a -> NLM a
Substitution -> (Context -> Context) -> NLM a -> NLM a
MonadTCEnv NLM
-> (forall a. Name -> Dom Type -> NLM a -> NLM a)
-> (forall a. Name -> Term -> Dom Type -> NLM a -> NLM a)
-> (forall a.
    Substitution -> (Context -> Context) -> 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 -> Term -> Dom Type -> NLM a -> NLM a
forall a. Name -> Dom Type -> NLM a -> NLM a
forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
withFreshName :: Range -> String -> (Name -> NLM a) -> NLM a
$cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
updateContext :: Substitution -> (Context -> Context) -> NLM a -> NLM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
addLetBinding' :: Name -> Term -> Dom Type -> NLM a -> NLM a
$caddLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
addCtx :: Name -> Dom Type -> NLM a -> NLM a
$caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
$cp1MonadAddContext :: MonadTCEnv NLM
MonadAddContext, Monad NLM
Functor NLM
Applicative NLM
NLM Bool
NLM Verbosity
Functor NLM
-> Applicative NLM
-> Monad NLM
-> (String -> VerboseLevel -> TCM Doc -> NLM String)
-> (forall a. String -> VerboseLevel -> String -> NLM a -> NLM a)
-> (forall a. String -> VerboseLevel -> String -> NLM a -> NLM a)
-> NLM Verbosity
-> NLM Bool
-> (forall a. NLM a -> NLM a)
-> MonadDebug NLM
String -> VerboseLevel -> String -> NLM a -> NLM a
String -> VerboseLevel -> String -> NLM a -> NLM a
String -> VerboseLevel -> TCM Doc -> NLM String
NLM a -> NLM a
forall a. String -> VerboseLevel -> String -> NLM a -> NLM a
forall a. NLM a -> NLM a
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> (String -> VerboseLevel -> TCM Doc -> m String)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> (forall a. String -> VerboseLevel -> String -> m a -> m a)
-> m Verbosity
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
nowDebugPrinting :: NLM a -> NLM a
$cnowDebugPrinting :: forall a. NLM a -> NLM a
isDebugPrinting :: NLM Bool
$cisDebugPrinting :: NLM Bool
getVerbosity :: NLM Verbosity
$cgetVerbosity :: NLM Verbosity
verboseBracket :: String -> VerboseLevel -> String -> NLM a -> NLM a
$cverboseBracket :: forall a. String -> VerboseLevel -> String -> NLM a -> NLM a
traceDebugMessage :: String -> VerboseLevel -> String -> NLM a -> NLM a
$ctraceDebugMessage :: forall a. String -> VerboseLevel -> String -> NLM a -> NLM a
formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NLM String
$cformatDebugMessage :: String -> VerboseLevel -> TCM Doc -> NLM String
$cp3MonadDebug :: Monad NLM
$cp2MonadDebug :: Applicative NLM
$cp1MonadDebug :: Functor NLM
MonadDebug
           , MonadDebug NLM
MonadTCEnv NLM
MonadReduce NLM
ReadTCState NLM
MonadAddContext NLM
HasBuiltins NLM
HasConstInfo NLM
HasBuiltins NLM
-> HasConstInfo NLM
-> MonadAddContext NLM
-> MonadDebug NLM
-> MonadReduce NLM
-> MonadTCEnv NLM
-> ReadTCState NLM
-> PureTCM NLM
forall (m :: * -> *).
HasBuiltins m
-> HasConstInfo m
-> MonadAddContext m
-> MonadDebug m
-> MonadReduce m
-> MonadTCEnv m
-> ReadTCState m
-> PureTCM m
$cp7PureTCM :: ReadTCState NLM
$cp6PureTCM :: MonadTCEnv NLM
$cp5PureTCM :: MonadReduce NLM
$cp4PureTCM :: MonadDebug NLM
$cp3PureTCM :: MonadAddContext NLM
$cp2PureTCM :: HasConstInfo NLM
$cp1PureTCM :: HasBuiltins NLM
PureTCM
           )

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

data NLMState = NLMState
  { NLMState -> Sub
_nlmSub   :: Sub
  , NLMState -> PostponedEquations
_nlmEqs   :: PostponedEquations
  }

instance Null NLMState where
  empty :: NLMState
empty  = NLMState :: Sub -> PostponedEquations -> NLMState
NLMState { _nlmSub :: Sub
_nlmSub = Sub
forall a. Null a => a
empty , _nlmEqs :: PostponedEquations
_nlmEqs = PostponedEquations
forall a. Null a => a
empty }
  null :: NLMState -> Bool
null NLMState
s = Sub -> Bool
forall a. Null a => a -> Bool
null (NLMState
sNLMState -> Lens' Sub NLMState -> Sub
forall o i. o -> Lens' i o -> i
^.Lens' Sub NLMState
nlmSub) Bool -> Bool -> Bool
&& PostponedEquations -> Bool
forall a. Null a => a -> Bool
null (NLMState
sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
forall o i. o -> Lens' i o -> i
^.Lens' PostponedEquations NLMState
nlmEqs)

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

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

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

matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked = Blocked_ -> NLM ()
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 -> VerboseLevel -> Type -> Term -> NLM ()
tellSub Relevance
r VerboseLevel
i Type
a Term
v = do
  Maybe (Relevance, Term)
old <- VerboseLevel -> Sub -> Maybe (Relevance, Term)
forall a. VerboseLevel -> IntMap a -> Maybe a
IntMap.lookup VerboseLevel
i (Sub -> Maybe (Relevance, Term))
-> NLM Sub -> NLM (Maybe (Relevance, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Sub NLMState -> NLM Sub
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Sub NLMState
nlmSub
  case Maybe (Relevance, Term)
old of
    Maybe (Relevance, Term)
Nothing -> Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= VerboseLevel -> (Relevance, Term) -> Sub -> Sub
forall a. VerboseLevel -> a -> IntMap a -> IntMap a
IntMap.insert VerboseLevel
i (Relevance
r,Term
v)
    Just (Relevance
r',Term
v')
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r  -> () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r' -> Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= VerboseLevel -> (Relevance, Term) -> Sub -> Sub
forall a. VerboseLevel -> a -> IntMap a -> IntMap a
IntMap.insert VerboseLevel
i (Relevance
r,Term
v)
      | Bool
otherwise       -> NLM (Maybe Blocked_) -> (Blocked_ -> NLM ()) -> NLM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (Type -> Term -> Term -> NLM (Maybe Blocked_)
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Maybe Blocked_)
equal Type
a Term
v Term
v') Blocked_ -> NLM ()
matchingBlocked

tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Telescope
k Type
a Term
u Term
v = do
  String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
               [ TCM Doc
"adding equality between" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)
               , TCM Doc
" and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
  Lens' PostponedEquations NLMState
nlmEqs Lens' PostponedEquations NLMState
-> (PostponedEquations -> PostponedEquations) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= (Telescope -> Type -> Term -> Term -> PostponedEquation
PostponedEquation Telescope
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 -> Telescope
eqFreeVars :: Telescope -- ^ Telescope 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 t a b where
  match :: Relevance  -- ^ Are we currently matching in an irrelevant context?
        -> Telescope  -- ^ The telescope of pattern variables
        -> Telescope  -- ^ The telescope of lambda-bound variables
        -> t          -- ^ The type of the pattern
        -> a          -- ^ The pattern to match
        -> b          -- ^ The term to be matched against the pattern
        -> NLM ()

instance Match t a b => Match (Dom t) (Arg a) (Arg b) where
  match :: Relevance
-> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k Dom t
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 -> Telescope -> Telescope -> t -> a -> b -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r' Telescope
gamma Telescope
k (Dom t -> t
forall t e. Dom' t e -> e
unDom Dom t
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 (Type, Elims -> Term) [Elim' NLPat] Elims where
  match :: Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t, Elims -> Term
hd) [] [] = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Elims -> Term
hd) [] Elims
_  = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Elims -> Term
hd) [Elim' NLPat]
_  [] = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Elims -> Term
hd) (Elim' NLPat
p:[Elim' NLPat]
ps) (Elim
v:Elims
vs) =
   String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
50 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
     [ TCM Doc
"matching elimination " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Elim' NLPat -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim' NLPat
p)
     , TCM Doc
"  with               " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Elim -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
v)
     , TCM Doc
"  eliminating head   " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd []) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t)]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
   case (Elim' NLPat
p,Elim
v) of
    (Apply Arg NLPat
p, Apply Arg Term
v) -> (Telescope -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
forall a b. (a -> b) -> a -> b
$ 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Pi Dom Type
a Abs Type
b -> do
        Relevance
-> Telescope
-> Telescope
-> Dom Type
-> Arg NLPat
-> Arg Term
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k 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
forall a. Arg a -> Elim' a
Apply Arg Term
vElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t',Elims -> Term
hd') [Elim' NLPat]
ps Elims
vs
      Term
t -> String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
20
        (TCM Doc
"application at non-pi type (possible non-confluence?) " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t) NLM ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (IApply NLPat
x NLPat
y NLPat
p , IApply Term
u Term
v Term
i) -> (Telescope -> NLM PathView -> NLM PathView
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM PathView -> NLM PathView) -> NLM PathView -> NLM PathView
forall a b. (a -> b) -> a -> b
$ 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 (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
        Right Type
interval <- 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
        Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k Type
interval NLPat
p Term
i
        let t' :: Type
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
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
u Term
v Term
iElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t',Elims -> Term
hd') [Elim' NLPat]
ps Elims
vs
      PathView
t -> String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
20
        (TCM Doc
"interval application at non-pi type (possible non-confluence?) " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (PathView -> Type
pathUnview PathView
t)) NLM ()
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
      ~(Just (El Sort
_ (Pi Dom Type
a Abs Type
b))) <- Telescope -> NLM (Maybe Type) -> NLM (Maybe Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM (Maybe Type) -> NLM (Maybe Type))
-> NLM (Maybe Type) -> NLM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ 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
      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
      Elims -> Term
hd' <- Telescope -> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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)
      Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t',Elims -> Term
hd') [Elim' NLPat]
ps Elims
vs

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

    (Apply{}, Proj{} ) -> NLM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Proj{} , Apply{}) -> NLM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

instance Match t a b => Match t (Dom a) (Dom b) where
  match :: Relevance
-> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k t
t Dom a
p Dom b
v = Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k t
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
-> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()
match Relevance
r Telescope
gamma Telescope
k ()
_ (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
-> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPSort
sp Sort
s
    Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Sort -> Type
sort Sort
s) NLPat
p Term
a

instance Match () NLPSort Sort where
  match :: Relevance
-> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
match Relevance
r Telescope
gamma Telescope
k ()
_ NLPSort
p Sort
s = do
    Blocked Sort
bs <- Telescope -> NLM (Blocked Sort) -> NLM (Blocked Sort)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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_
b = Blocked Sort -> Blocked_
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked Sort
bs
        s :: Sort
s = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
bs
        yes :: NLM ()
yes = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: NLM ()
no  = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()
    String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"matching pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (NLPSort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPSort
p)
      , TCM Doc
"  with sort      " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    case (NLPSort
p , Sort
s) of
      (PType NLPat
lp  , Type Level' Term
l  ) -> Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPat
lp Level' Term
l
      (PProp NLPat
lp  , Prop Level' Term
l  ) -> Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPat
lp Level' Term
l
      (PInf IsFibrant
fp Integer
np , Inf IsFibrant
f Integer
n)
        | IsFibrant
fp IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
f, 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

      -- blocked cases
      (NLPSort
_ , UnivSort{}) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (NLPSort
_ , PiSort{}  ) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (NLPSort
_ , FunSort{} ) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (NLPSort
_ , MetaS MetaId
m Elims
_ ) -> Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocked_
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
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
match Relevance
r Telescope
gamma Telescope
k ()
_ NLPat
p Level' Term
l = do
    Type
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
<$> String -> NLM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    Term
v <- Level' Term -> NLM Term
forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
    Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k Type
t NLPat
p Term
v

instance Match Type NLPat Term where
  match :: Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
match Relevance
r0 Telescope
gamma Telescope
k Type
t NLPat
p Term
v = do
    Blocked (Term, Type)
vbt <- Telescope
-> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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 :: VerboseLevel
n = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
k
        b :: Blocked_
b = Blocked (Term, Type) -> Blocked_
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked (Term, Type)
vbt
        (Term
v,Type
t) = Blocked (Term, Type) -> (Term, Type)
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Term, Type)
vbt
        prettyPat :: TCM Doc
prettyPat  = TCM Doc -> TCM Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (NLPat -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
p)
        prettyTerm :: TCM Doc
prettyTerm = TCM Doc -> TCM Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        prettyType :: TCM Doc
prettyType = TCM Doc -> TCM Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    Maybe (QName, Args)
etaRecord <- Telescope -> NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args)))
-> NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args))
forall a b. (a -> b) -> a -> b
$ Type -> NLM (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t
    Bool
prop <- (Blocker -> Bool) -> Either Blocker Bool -> Bool
forall a b. (a -> b) -> Either a b -> b
fromRight Blocker -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ (Either Blocker Bool -> Bool)
-> (BlockT NLM Bool -> NLM (Either Blocker Bool))
-> BlockT NLM Bool
-> NLM Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BlockT NLM Bool -> NLM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT NLM Bool -> NLM (Either Blocker Bool))
-> (BlockT NLM Bool -> BlockT NLM Bool)
-> BlockT NLM Bool
-> NLM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> BlockT NLM Bool -> BlockT NLM Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (BlockT NLM Bool -> NLM Bool) -> BlockT NLM Bool -> NLM Bool
forall a b. (a -> b) -> a -> b
$ Type -> BlockT NLM Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
t
    let r :: Relevance
r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
    String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"matching pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyPat
      , TCM Doc
"  with term      " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyTerm
      , TCM Doc
"  of type        " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyType ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
80 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"  raw pattern:  " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (NLPat -> String
forall a. Show a => a -> String
show NLPat
p)
      , TCM Doc
"  raw term:     " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Term -> String
forall a. Show a => a -> String
show Term
v)
      , TCM Doc
"  raw type:     " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Type -> String
forall a. Show a => a -> String
show Type
t) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
70 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"pattern vars:   " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
      , TCM Doc
"bound vars:     " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
k ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    let yes :: NLM ()
yes = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: TCM Doc -> NLM ()
no TCM Doc
msg = if Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant then NLM ()
yes else do
          String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCM Doc
"mismatch between" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyPat
            , TCM Doc
" and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyTerm
            , TCM Doc
" of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyType
            , TCM Doc
msg ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCM Doc
"blocking tag from reduction: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> String
forall a. Show a => a -> String
show Blocked_
b) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          Blocked_ -> NLM ()
matchingBlocked Blocked_
b
        block :: Blocked_ -> NLM ()
block Blocked_
b' = if Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant then NLM ()
yes else do
          String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCM Doc
"matching blocked on meta"
            , String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> String
forall a. Show a => a -> String
show Blocked_
b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCM Doc
"blocking tag from reduction: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> String
forall a. Show a => a -> String
show Blocked_
b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          Blocked_ -> NLM ()
matchingBlocked (Blocked_
b Blocked_ -> Blocked_ -> Blocked_
forall a. Monoid a => a -> a -> a
`mappend` Blocked_
b')
        maybeBlock :: Term -> NLM ()
maybeBlock = \case
          MetaV MetaId
m Elims
es -> Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocked_
forall t. MetaId -> Blocked' t ()
blocked_ MetaId
m
          Term
_          -> TCM Doc -> NLM ()
no TCM Doc
""
    case NLPat
p of
      PVar VerboseLevel
i [Arg VerboseLevel]
bvs -> String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
60 (TCM Doc
"matching a PVar: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (VerboseLevel -> String
forall a. Show a => a -> String
show VerboseLevel
i)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        let allowedVars :: IntSet
            allowedVars :: IntSet
allowedVars = [VerboseLevel] -> IntSet
IntSet.fromList ((Arg VerboseLevel -> VerboseLevel)
-> [Arg VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg [Arg VerboseLevel]
bvs)
            badVars :: IntSet
            badVars :: IntSet
badVars = IntSet -> IntSet -> IntSet
IntSet.difference ([VerboseLevel] -> IntSet
IntSet.fromList (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
n)) IntSet
allowedVars
            perm :: Permutation
            perm :: Permutation
perm = VerboseLevel -> [VerboseLevel] -> Permutation
Perm VerboseLevel
n ([VerboseLevel] -> Permutation) -> [VerboseLevel] -> Permutation
forall a b. (a -> b) -> a -> b
$ [VerboseLevel] -> [VerboseLevel]
forall a. [a] -> [a]
reverse ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ (Arg VerboseLevel -> VerboseLevel)
-> [Arg VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg ([Arg VerboseLevel] -> [VerboseLevel])
-> [Arg VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ [Arg VerboseLevel]
bvs
            tel :: Telescope
            tel :: Telescope
tel = Permutation -> Telescope -> Telescope
permuteTel Permutation
perm Telescope
k
        Either Blocked_ (Maybe Term)
ok <- Telescope
-> NLM (Either Blocked_ (Maybe Term))
-> NLM (Either Blocked_ (Maybe Term))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM (Either Blocked_ (Maybe Term))
 -> NLM (Either Blocked_ (Maybe Term)))
-> NLM (Either Blocked_ (Maybe Term))
-> NLM (Either Blocked_ (Maybe Term))
forall a b. (a -> b) -> a -> b
$ IntSet -> Term -> NLM (Either Blocked_ (Maybe Term))
forall (m :: * -> *) a.
(MonadReduce m, Reduce a, ForceNotFree a) =>
IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree IntSet
badVars Term
v
        case Either Blocked_ (Maybe Term)
ok of
          Left Blocked_
b         -> Blocked_ -> NLM ()
block Blocked_
b
          Right Maybe Term
Nothing  -> TCM Doc -> NLM ()
no TCM Doc
""
          Right (Just Term
v) ->
            let t' :: Type
t' = Telescope -> Type -> Type
telePi  Telescope
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' = Telescope -> Term -> Term
teleLam Telescope
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 -> VerboseLevel -> Type -> Term -> NLM ()
tellSub Relevance
r (VerboseLevel
iVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
n) Type
t' Term
v'

      PDef QName
f [Elim' NLPat]
ps -> String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
60 (TCM Doc
"matching a PDef: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        Term
v <- Telescope -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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 Term
v of
          Def QName
f' Elims
es
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'   -> do
                Type
ft <- Telescope -> NLM Type -> NLM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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 => QName -> m Definition
getConstInfo QName
f
                Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ft , QName -> Elims -> Term
Def QName
f) [Elim' NLPat]
ps Elims
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
                ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> 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
addContext Telescope
k (NLM (Maybe ((QName, Type, Args), Type))
 -> NLM (Maybe ((QName, Type, Args), Type)))
-> NLM (Maybe ((QName, Type, Args), Type))
-> NLM (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ 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
                Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) [Elim' NLPat]
ps Elims
vs
          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
$ VerboseLevel -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
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
$ VerboseLevel -> Term
var VerboseLevel
0 ]
                body :: Term
body  = VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
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
$ VerboseLevel -> Term
var VerboseLevel
0 ]
                k' :: Telescope
k'    = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
            Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) NLPat
pbody Term
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)@.
            Defn
def <- Telescope -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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 => QName -> m Definition
getConstInfo QName
d
            (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- Telescope
-> NLM (Telescope, ConHead, ConInfo, Args)
-> NLM (Telescope, ConHead, ConInfo, Args)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM (Telescope, ConHead, ConInfo, Args)
 -> NLM (Telescope, ConHead, ConInfo, Args))
-> NLM (Telescope, ConHead, ConInfo, Args)
-> NLM (Telescope, ConHead, ConInfo, Args)
forall a b. (a -> b) -> a -> b
$ QName
-> Args -> Defn -> Term -> NLM (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
            ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> 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
addContext Telescope
k (NLM (Maybe ((QName, Type, Args), Type))
 -> NLM (Maybe ((QName, Type, Args), Type)))
-> NLM (Maybe ((QName, Type, Args), Type))
-> NLM (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ 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
            let flds :: [Arg QName]
flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
            Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ct, ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) [Elim' NLPat]
ps' ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs)
          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 = VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
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 (VerboseLevel -> Term
var VerboseLevel
0)]
              k' :: Telescope
k'   = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) (Abs NLPat -> NLPat
forall a. Subst a => Abs a -> a
absBody Abs NLPat
p') Term
body
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PPi Dom NLPType
pa Abs NLPType
pb -> case Term
v of
        Pi Dom Type
a Abs Type
b -> do
          Relevance
-> Telescope
-> Telescope
-> ()
-> Dom NLPType
-> Dom Type
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () Dom NLPType
pa Dom Type
a
          let k' :: Telescope
k' = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' () (Abs NLPType -> NLPType
forall a. Subst a => Abs a -> a
absBody Abs NLPType
pb) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PSort NLPSort
ps -> case Term
v of
        Sort Sort
s -> Relevance
-> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPSort
ps Sort
s
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PBoundVar VerboseLevel
i [Elim' NLPat]
ps -> case Term
v of
        Var VerboseLevel
i' Elims
es | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
i' -> do
          let ti :: Type
ti = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> Dom Type -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> [Dom Type] -> VerboseLevel -> Dom Type
forall a. a -> [a] -> VerboseLevel -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
k) VerboseLevel
i
          Relevance
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ti , VerboseLevel -> Elims -> Term
Var VerboseLevel
i) [Elim' NLPat]
ps Elims
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 = VerboseLevel -> [Elim' NLPat] -> NLPat
PBoundVar (VerboseLevel
1VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
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
$ VerboseLevel -> Term
var VerboseLevel
0 ]
              body :: Term
body  = VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
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
$ VerboseLevel -> Term
var VerboseLevel
0 ]
              k' :: Telescope
k'    = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) NLPat
pbody Term
body
        Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          Defn
def <- Telescope -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
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 => QName -> m Definition
getConstInfo QName
d
          (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- Telescope
-> NLM (Telescope, ConHead, ConInfo, Args)
-> NLM (Telescope, ConHead, ConInfo, Args)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (NLM (Telescope, ConHead, ConInfo, Args)
 -> NLM (Telescope, ConHead, ConInfo, Args))
-> NLM (Telescope, ConHead, ConInfo, Args)
-> NLM (Telescope, ConHead, ConInfo, Args)
forall a b. (a -> b) -> a -> b
$ QName
-> Args -> Defn -> Term -> NLM (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
          ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> 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
addContext Telescope
k (NLM (Maybe ((QName, Type, Args), Type))
 -> NLM (Maybe ((QName, Type, Args), Type)))
-> NLM (Maybe ((QName, Type, Args), Type))
-> NLM (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ 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
          let flds :: [Arg QName]
flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
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 (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 -> VerboseLevel -> [Elim' NLPat] -> NLPat
PBoundVar VerboseLevel
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
-> Telescope
-> Telescope
-> (Type, Elims -> Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PTerm Term
u -> String -> VerboseLevel -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
60 (TCM Doc
"matching a PTerm" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$
        Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Telescope
k Type
t Term
u Term
v

-- Checks if the given term contains any free variables that satisfy the
-- given condition on their DBI, possibly reducing the term in the process.
-- Returns `Right Nothing` if there are such variables, `Right (Just v')`
-- if there are none (where v' is the possibly reduced version of the given
-- term) or `Left b` if the problem is blocked on a meta.
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a)
           => IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree :: IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree IntSet
xs a
v = do
  (IntMap IsFree
mxs , a
v') <- IntSet -> a -> m (IntMap IsFree, a)
forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree IntSet
xs a
v
  case (IsFree -> IsFree -> IsFree) -> IsFree -> IntMap IsFree -> IsFree
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IntMap.foldr IsFree -> IsFree -> IsFree
pickFree IsFree
NotFree IntMap IsFree
mxs of
    MaybeFree MetaSet
ms
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms   -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right Maybe a
forall a. Maybe a
Nothing
      | Bool
otherwise -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Either Blocked_ (Maybe a)
forall a b. a -> Either a b
Left (Blocked_ -> Either Blocked_ (Maybe a))
-> Blocked_ -> Either Blocked_ (Maybe a)
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
      where blocker :: Blocker
blocker = Set Blocker -> Blocker
unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set Blocker -> Set Blocker)
-> Set Blocker -> MetaSet -> Set Blocker
forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet (Blocker -> Set Blocker -> Set Blocker
forall a. Ord a => a -> Set a -> Set a
Set.insert (Blocker -> Set Blocker -> Set Blocker)
-> (MetaId -> Blocker) -> MetaId -> Set Blocker -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Blocker
unblockOnMeta) Set Blocker
forall a. Set a
Set.empty MetaSet
ms
    IsFree
NotFree -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right (a -> Maybe a
forall a. a -> Maybe a
Just a
v')

  where
    -- Check if any of the variables occur freely.
    -- Prefer occurrences that do not depend on any metas.
    pickFree :: IsFree -> IsFree -> IsFree
    pickFree :: IsFree -> IsFree -> IsFree
pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
f2
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms1  = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) f2 :: IsFree
f2@(MaybeFree MetaSet
ms2)
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms2  = IsFree
f2
      | Bool
otherwise = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
NotFree = IsFree
f1
    pickFree IsFree
NotFree IsFree
f2 = IsFree
f2


makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution Telescope
gamma Sub
sub =
  [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> Term) -> [VerboseLevel] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
HasCallStack => Term
__DUMMY_TERM__ (Maybe Term -> Term)
-> (VerboseLevel -> Maybe Term) -> VerboseLevel -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Maybe Term
val) [VerboseLevel
0 .. Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
gammaVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]
    where
      val :: VerboseLevel -> Maybe Term
val VerboseLevel
i = case VerboseLevel -> Sub -> Maybe (Relevance, Term)
forall a. VerboseLevel -> IntMap a -> Maybe a
IntMap.lookup VerboseLevel
i Sub
sub of
                Just (Relevance
Irrelevant, Term
v) -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
dontCare Term
v
                Just (Relevance
_         , Term
v) -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v
                Maybe (Relevance, Term)
Nothing              -> Maybe Term
forall a. Maybe a
Nothing

checkPostponedEquations :: PureTCM m
                        => Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations :: Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs = PostponedEquations
-> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
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_)) -> m (Maybe Blocked_))
-> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$
  \ (PostponedEquation Telescope
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 (VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
k) Substitution
sub) Term
lhs
      String
-> VerboseLevel
-> TCM Doc
-> m (Maybe Blocked_)
-> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCM Doc
"checking postponed equality between" , Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs')
        , TCM Doc
" and " , Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs) ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ do
      Telescope -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> m (Maybe Blocked_)
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Maybe Blocked_)
equal Type
a Term
lhs' Term
rhs

-- main function
nonLinMatch :: (PureTCM m, Match t a b)
            => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch :: Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
gamma t
t a
p b
v = do
  let no :: String -> a -> m (Either a b)
no String
msg a
b = String
-> VerboseLevel -> TCM Doc -> m (Either a b) -> m (Either a b)
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                   [ TCM Doc
"matching failed during" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
msg
                   , TCM Doc
"blocking: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCM 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 (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_ NLMState)
-> (Blocked_ -> m (Either Blocked_ Substitution))
-> (NLMState -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ 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_ NLMState)
forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either Blocked_ NLMState)
runNLM (NLM () -> m (Either Blocked_ NLMState))
-> NLM () -> m (Either Blocked_ NLMState)
forall a b. (a -> b) -> a -> b
$ Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
Relevant Telescope
gamma Telescope
forall a. Tele a
EmptyTel t
t a
p b
v) (String -> Blocked_ -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"matching") ((NLMState -> m (Either Blocked_ Substitution))
 -> m (Either Blocked_ Substitution))
-> (NLMState -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ \ NLMState
s -> do
    let sub :: Substitution
sub = Telescope -> Sub -> Substitution
makeSubstitution Telescope
gamma (Sub -> Substitution) -> Sub -> Substitution
forall a b. (a -> b) -> a -> b
$ NLMState
sNLMState -> Lens' Sub NLMState -> Sub
forall o i. o -> Lens' i o -> i
^.Lens' Sub NLMState
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
forall o i. o -> Lens' i o -> i
^.Lens' PostponedEquations NLMState
nlmEqs
    String
-> VerboseLevel
-> TCM Doc
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
90 (String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"sub = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Substitution -> String
forall a. Show a => a -> String
show Substitution
sub) (m (Either Blocked_ Substitution)
 -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ do
    Maybe Blocked_
ok <- Substitution -> PostponedEquations -> m (Maybe Blocked_)
forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs
    case Maybe Blocked_
ok of
      Maybe Blocked_
Nothing -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ Substitution -> m (Either Blocked_ Substitution))
-> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ Substitution -> Either Blocked_ Substitution
forall a b. b -> Either a b
Right Substitution
sub
      Just Blocked_
b  -> String -> Blocked_ -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"checking of postponed equations" Blocked_
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 :: Type -> Term -> Term -> m (Maybe Blocked_)
equal Type
a Term
u Term
v = BlockT m Bool -> m (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Type -> Term -> Term -> BlockT m Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v) m (Either Blocker Bool)
-> (Either Blocker Bool -> m (Maybe Blocked_))
-> m (Maybe Blocked_)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left Blocker
b      -> Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocked_ -> m (Maybe Blocked_))
-> Maybe Blocked_ -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Maybe Blocked_
forall a. a -> Maybe a
Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()
  Right Bool
True  -> Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Blocked_
forall a. Maybe a
Nothing
  Right Bool
False -> String
-> VerboseLevel
-> TCM Doc
-> m (Maybe Blocked_)
-> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc String
"rewriting.match" VerboseLevel
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCM Doc
"mismatch between " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , TCM Doc
" and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ do
    Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocked_ -> m (Maybe Blocked_))
-> Maybe Blocked_ -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Maybe Blocked_
forall a. a -> Maybe a
Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked_
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)
getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead :: Term -> m (Maybe (QName, Type))
getTypedHead = \case
  Def QName
f []   -> (QName, Type) -> Maybe (QName, Type)
forall a. a -> Maybe a
Just ((QName, Type) -> Maybe (QName, Type))
-> (Definition -> (QName, Type))
-> Definition
-> Maybe (QName, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName
f,) (Type -> (QName, Type))
-> (Definition -> Type) -> Definition -> (QName, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> Maybe (QName, Type))
-> m Definition -> m (Maybe (QName, Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => 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
    Args
vs <- QName -> m Args
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply QName
c
    -- Jesper, 2020-06-17, issue #4755: add dummy arguments in
    -- case we don't have enough parameters
    VerboseLevel
npars <- VerboseLevel -> Maybe VerboseLevel -> VerboseLevel
forall a. a -> Maybe a -> a
fromMaybe VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe VerboseLevel -> VerboseLevel)
-> m (Maybe VerboseLevel) -> m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe VerboseLevel)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
c
    let ws :: Args
ws = VerboseLevel -> Arg Term -> Args
forall a. VerboseLevel -> a -> [a]
replicate (VerboseLevel
npars VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
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__
    Type
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 => QName -> m Definition
getConstInfo QName
c
    Type
t <- Type
t0 Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` (Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
ws)
    Maybe (QName, Type) -> m (Maybe (QName, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (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
c , Type
t)
  Term
_ -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Type)
forall a. Maybe a
Nothing