{-# 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.Base

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 { forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a }
  deriving ( (forall a b. (a -> b) -> NLM a -> NLM b)
-> (forall a b. a -> NLM b -> NLM a) -> Functor NLM
forall a b. a -> NLM b -> NLM a
forall a b. (a -> b) -> NLM a -> NLM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> NLM a -> NLM b
fmap :: forall a b. (a -> b) -> NLM a -> NLM b
$c<$ :: forall a b. a -> NLM b -> NLM a
<$ :: forall a b. a -> NLM b -> NLM a
Functor, Functor NLM
Functor NLM
-> (forall a. a -> NLM a)
-> (forall a b. NLM (a -> b) -> NLM a -> NLM b)
-> (forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c)
-> (forall a b. NLM a -> NLM b -> NLM b)
-> (forall a b. NLM a -> NLM b -> NLM a)
-> Applicative NLM
forall a. a -> NLM a
forall a b. NLM a -> NLM b -> NLM a
forall a b. NLM a -> NLM b -> NLM b
forall a b. NLM (a -> b) -> NLM a -> NLM b
forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> NLM a
pure :: forall a. a -> NLM a
$c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
$cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
liftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
$c*> :: forall a b. NLM a -> NLM b -> NLM b
*> :: forall a b. NLM a -> NLM b -> NLM b
$c<* :: forall a b. NLM a -> NLM b -> NLM a
<* :: forall a b. NLM a -> NLM b -> NLM a
Applicative, Applicative NLM
Applicative NLM
-> (forall a b. NLM a -> (a -> NLM b) -> NLM b)
-> (forall a b. NLM a -> NLM b -> NLM b)
-> (forall a. a -> NLM a)
-> Monad NLM
forall a. a -> NLM a
forall a b. NLM a -> NLM b -> NLM b
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
$c>> :: forall a b. NLM a -> NLM b -> NLM b
>> :: forall a b. NLM a -> NLM b -> NLM b
$creturn :: forall a. a -> NLM a
return :: forall a. a -> NLM a
Monad, Monad NLM
Monad NLM -> (forall a. String -> NLM a) -> MonadFail NLM
forall a. String -> NLM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> NLM a
fail :: forall a. String -> NLM a
Fail.MonadFail
           , Applicative NLM
Applicative NLM
-> (forall a. NLM a)
-> (forall a. NLM a -> NLM a -> NLM a)
-> (forall a. NLM a -> NLM [a])
-> (forall a. NLM a -> NLM [a])
-> Alternative NLM
forall a. NLM a
forall a. NLM a -> NLM [a]
forall a. NLM a -> NLM a -> NLM a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
$cempty :: forall a. NLM a
empty :: forall a. NLM a
$c<|> :: forall a. NLM a -> NLM a -> NLM a
<|> :: forall a. NLM a -> NLM a -> NLM a
$csome :: forall a. NLM a -> NLM [a]
some :: forall a. NLM a -> NLM [a]
$cmany :: forall a. NLM a -> NLM [a]
many :: forall a. NLM a -> NLM [a]
Alternative, Monad NLM
Alternative NLM
Alternative NLM
-> Monad NLM
-> (forall a. NLM a)
-> (forall a. NLM a -> NLM a -> NLM a)
-> MonadPlus NLM
forall a. NLM a
forall a. NLM a -> NLM a -> NLM a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
$cmzero :: forall a. NLM a
mzero :: forall a. NLM a
$cmplus :: forall a. NLM a -> NLM a -> NLM a
mplus :: forall a. NLM a -> NLM a -> NLM a
MonadPlus
           , MonadError Blocked_, MonadState NLMState
           , 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
$cgetBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
HasBuiltins, Functor NLM
MonadFail NLM
Applicative NLM
HasOptions NLM
MonadTCEnv NLM
MonadDebug 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
$cgetConstInfo :: QName -> NLM Definition
getConstInfo :: QName -> NLM Definition
$cgetConstInfo' :: QName -> NLM (Either SigError Definition)
getConstInfo' :: QName -> NLM (Either SigError Definition)
$cgetRewriteRulesFor :: QName -> NLM RewriteRules
getRewriteRulesFor :: QName -> NLM RewriteRules
HasConstInfo, Monad NLM
Functor NLM
Applicative NLM
NLM PragmaOptions
NLM CommandLineOptions
Functor NLM
-> Applicative NLM
-> Monad NLM
-> NLM PragmaOptions
-> NLM CommandLineOptions
-> HasOptions NLM
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
$cpragmaOptions :: NLM PragmaOptions
pragmaOptions :: NLM PragmaOptions
$ccommandLineOptions :: NLM CommandLineOptions
commandLineOptions :: NLM CommandLineOptions
HasOptions, Monad NLM
NLM 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
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
$cgetTCState :: NLM TCState
getTCState :: NLM TCState
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
$cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
withTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
ReadTCState
           , Monad NLM
NLM TCEnv
Monad NLM
-> NLM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a)
-> MonadTCEnv NLM
forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
$caskTC :: NLM TCEnv
askTC :: NLM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
localTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
MonadTCEnv, Applicative NLM
HasOptions NLM
MonadTCEnv NLM
ReadTCState NLM
Applicative NLM
-> MonadTCEnv NLM
-> ReadTCState NLM
-> HasOptions NLM
-> (forall a. ReduceM a -> NLM a)
-> MonadReduce NLM
forall a. ReduceM a -> NLM a
forall (m :: * -> *).
Applicative m
-> MonadTCEnv m
-> ReadTCState m
-> HasOptions m
-> (forall a. ReduceM a -> m a)
-> MonadReduce m
$cliftReduce :: forall a. ReduceM a -> NLM a
liftReduce :: forall a. ReduceM a -> NLM a
MonadReduce, MonadTCEnv NLM
MonadTCEnv NLM
-> (forall a. Name -> Dom Type -> NLM a -> NLM a)
-> (forall a. 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
$caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
addCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
$caddLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
addLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
updateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
$cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
withFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
MonadAddContext, Monad NLM
Functor NLM
Applicative NLM
NLM Bool
NLM Verbosity
NLM ProfileOptions
Functor NLM
-> Applicative NLM
-> Monad NLM
-> (String -> Key -> TCMT IO Doc -> NLM String)
-> (forall a. String -> Key -> String -> NLM a -> NLM a)
-> (forall a. String -> Key -> String -> NLM a -> NLM a)
-> NLM Verbosity
-> NLM ProfileOptions
-> NLM Bool
-> (forall a. NLM a -> NLM a)
-> MonadDebug NLM
String -> Key -> TCMT IO Doc -> NLM String
forall a. String -> Key -> String -> NLM a -> NLM a
forall a. NLM a -> NLM a
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> (String -> Key -> TCMT IO Doc -> m String)
-> (forall a. String -> Key -> String -> m a -> m a)
-> (forall a. String -> Key -> String -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
$cformatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
formatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
$ctraceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
traceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
$cverboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
verboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
$cgetVerbosity :: NLM Verbosity
getVerbosity :: NLM Verbosity
$cgetProfileOptions :: NLM ProfileOptions
getProfileOptions :: NLM ProfileOptions
$cisDebugPrinting :: NLM Bool
isDebugPrinting :: NLM Bool
$cnowDebugPrinting :: forall a. NLM a -> NLM a
nowDebugPrinting :: forall a. NLM a -> NLM a
MonadDebug
           , MonadTCEnv NLM
MonadReduce NLM
ReadTCState NLM
HasBuiltins NLM
MonadAddContext NLM
MonadDebug 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
PureTCM
           )

instance MonadBlock NLM where
  patternViolation :: forall a. Blocker -> NLM a
patternViolation Blocker
b = Blocked_ -> NLM a
forall a. 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 :: forall a. (Blocker -> NLM a) -> NLM a -> NLM a
catchPatternErr Blocker -> NLM a
h NLM a
f = NLM a -> (Blocked_ -> NLM a) -> NLM a
forall a. 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 a. 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 { _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
^.(Sub -> f Sub) -> NLMState -> f NLMState
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
^.(PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
Lens' PostponedEquations NLMState
nlmEqs)

nlmSub :: Lens' Sub NLMState
nlmSub :: Lens' Sub 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 :: Lens' PostponedEquations 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 :: forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either Blocked_ NLMState)
runNLM NLM ()
nlm = do
  (Either Blocked_ ()
ok,NLMState
out) <- ReduceM (Either Blocked_ (), NLMState)
-> m (Either Blocked_ (), NLMState)
forall a. ReduceM a -> m a
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 a. a -> m a
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 a. a -> m a
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 a. Blocked_ -> NLM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError

-- | Add substitution @i |-> v : a@ to result of matching.
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellSub :: Relevance -> Key -> Type -> Term -> NLM ()
tellSub Relevance
r Key
i Type
a Term
v = do
  Maybe (Relevance, Term)
old <- Key -> Sub -> Maybe (Relevance, Term)
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
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 (Sub -> f Sub) -> NLMState -> f NLMState
Lens' Sub NLMState
nlmSub
  case Maybe (Relevance, Term)
old of
    Maybe (Relevance, Term)
Nothing -> (Sub -> f Sub) -> NLMState -> f NLMState
Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= Key -> (Relevance, Term) -> Sub -> Sub
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
i (Relevance
r,Term
v)
    Just (Relevance
r',Term
v')
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r  -> () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r' -> (Sub -> f Sub) -> NLMState -> f NLMState
Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= Key -> (Relevance, Term) -> Sub -> Sub
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
               [ TCMT IO Doc
"adding equality between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)
               , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
  (PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
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 a. a -> NLM a
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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
50 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
     [ TCMT IO Doc
"matching elimination " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Elim' NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM Elim' NLPat
p)
     , TCMT IO Doc
"  with               " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
v)
     , TCMT IO Doc
"  eliminating head   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t)]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do

   let no :: NLM ()
no  = Blocked_ -> 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 ()
   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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Pi Dom Type
a Abs Type
b -> do
        Relevance
-> 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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
20
        (TCMT IO Doc
"application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t) NLM ()
forall a. NLM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (IApply NLPat
x NLPat
y NLPat
p , IApply Term
u Term
v Term
i) -> (Telescope -> NLM PathView -> NLM PathView
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
_u Arg Term
_v -> do
        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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
20
        (TCMT IO Doc
"interval application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (PathView -> Type
pathUnview PathView
t)) NLM ()
forall a. NLM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (Proj ProjOrigin
o QName
f, Proj ProjOrigin
o' QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> do
      Telescope -> NLM (Maybe Type) -> NLM (Maybe Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (QName -> Type -> NLM (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> NLM (Maybe Type)) -> NLM Type -> NLM (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM (Maybe Type) -> (Maybe Type -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> do
          let u :: Term
u = Elims -> Term
hd []
              t' :: Type
t' = Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
          Elims -> Term
hd' <- Telescope -> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
        Maybe Type
_ -> NLM ()
no

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

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

    (IApply{} , Elim
_    ) -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 a. a -> NLM a
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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"matching pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (NLPSort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
prettyTCM NLPSort
p)
      , TCMT IO Doc
"  with sort      " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> 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
      (PSSet NLPat
lp  , SSet 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
      (NLPSort
PIntervalUniv , Sort
IntervalUniv) -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: Key
n = Telescope -> Key
forall a. Sized a => a -> Key
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 :: TCMT IO Doc
prettyPat  = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
p)
        prettyTerm :: TCMT IO Doc
prettyTerm = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
        prettyType :: TCMT IO Doc
prettyType = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
    Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview <- NLM (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
    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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"matching pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyPat
      , TCMT IO Doc
"  with term      " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyTerm
      , TCMT IO Doc
"  of type        " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyType ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
80 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"  raw pattern:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (NLPat -> String
forall a. Show a => a -> String
show NLPat
p)
      , TCMT IO Doc
"  raw term:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Term -> String
forall a. Show a => a -> String
show Term
v)
      , TCMT IO Doc
"  raw type:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Type -> String
forall a. Show a => a -> String
show Type
t) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
70 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"pattern vars:   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
gamma
      , TCMT IO Doc
"bound vars:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
k ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    let yes :: NLM ()
yes = () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: TCMT IO Doc -> NLM ()
no TCMT IO Doc
msg = if Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant then NLM ()
yes else do
          String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"mismatch between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyPat
            , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyTerm
            , TCMT IO Doc
" of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyType
            , TCMT IO Doc
msg ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> 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 -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"matching blocked on meta"
            , String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> String
forall a. Show a => a -> String
show Blocked_
b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocked_ -> 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
_          -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
    case NLPat
p of
      PVar Key
i [Arg Key]
bvs -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
60 (TCMT IO Doc
"matching a PVar: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Key -> String
forall a. Show a => a -> String
show Key
i)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        let allowedVars :: IntSet
            allowedVars :: IntSet
allowedVars = [Key] -> IntSet
IntSet.fromList ((Arg Key -> Key) -> [Arg Key] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Arg Key -> Key
forall e. Arg e -> e
unArg [Arg Key]
bvs)
            badVars :: IntSet
            badVars :: IntSet
badVars = IntSet -> IntSet -> IntSet
IntSet.difference ([Key] -> IntSet
IntSet.fromList (Key -> [Key]
forall a. Integral a => a -> [a]
downFrom Key
n)) IntSet
allowedVars
            perm :: Permutation
            perm :: Permutation
perm = Key -> [Key] -> Permutation
Perm Key
n ([Key] -> Permutation) -> [Key] -> Permutation
forall a b. (a -> b) -> a -> b
$ [Key] -> [Key]
forall a. [a] -> [a]
reverse ([Key] -> [Key]) -> [Key] -> [Key]
forall a b. (a -> b) -> a -> b
$ (Arg Key -> Key) -> [Arg Key] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Arg Key -> Key
forall e. Arg e -> e
unArg ([Arg Key] -> [Key]) -> [Arg Key] -> [Key]
forall a b. (a -> b) -> a -> b
$ [Arg Key]
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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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  -> TCMT IO Doc -> NLM ()
no TCMT IO 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 -> Key -> Type -> Term -> NLM ()
tellSub Relevance
r (Key
iKey -> Key -> Key
forall a. Num a => a -> a -> a
-Key
n) Type
t' Term
v'

      PDef QName
f [Elim' NLPat]
ps -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
60 (TCMT IO Doc
"matching a PDef: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        Term
v <- Telescope -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
                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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) NLM (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Just ((QName, Type, Args)
_ , Type
ct) -> Relevance
-> 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
                  Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
          Term
_ | Pi Dom Type
a Abs Type
b <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
t -> do
            let ai :: ArgInfo
ai    = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
                pbody :: NLPat
pbody = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Key -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Key -> a -> a
raise Key
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
$ Key -> Term
var Key
0 ]
                body :: Term
body  = Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
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
$ Key -> Term
var Key
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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
            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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) NLM (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Just ((QName, Type, Args)
_ , Type
ct) -> do
                let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom 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 a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
                Relevance
-> 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)
              Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
          Term
v -> Term -> NLM ()
maybeBlock Term
v
      PLam ArgInfo
i Abs NLPat
p' -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b -> do
          let body :: Term
body = Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
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 (Key -> Term
var Key
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
_ | Left ((Dom Type
a,Abs Type
b),(Term
x,Term
y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview Type
t -> do
          let body :: Term
body = Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
1 Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply (Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
1 Term
x) (Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
1 Term
y) (Term -> Elim) -> Term -> Elim
forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
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 String
"i" 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 Key
i [Elim' NLPat]
ps -> case Term
v of
        Var Key
i' Elims
es | Key
i Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
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] -> Key -> Dom Type
forall a. a -> [a] -> Key -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
k) Key
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 , Key -> Elims -> Term
Var Key
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 = Key -> [Elim' NLPat] -> NLPat
PBoundVar (Key
1Key -> Key -> Key
forall a. Num a => a -> a -> a
+Key
i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Key -> [Elim' NLPat] -> [Elim' NLPat]
forall a. Subst a => Key -> a -> a
raise Key
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
$ Key -> Term
var Key
0 ]
              body :: Term
body  = Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
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
$ Key -> Term
var Key
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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
          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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) NLM (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just ((QName, Type, Args)
_ , Type
ct) -> do
              let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom 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 a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
-> (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ \QName
fld -> Key -> [Elim' NLPat] -> NLPat
PBoundVar Key
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)
            Maybe ((QName, Type, Args), Type)
Nothing -> TCMT IO Doc -> NLM ()
no TCMT IO Doc
""
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PTerm Term
u -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
60 (TCMT IO Doc
"matching a PTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$
        Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Telescope
k Type
t Term
u Term
v

makeSubstitution :: Telescope -> Sub -> Maybe Substitution
makeSubstitution :: Telescope -> Sub -> Maybe Substitution
makeSubstitution Telescope
gamma Sub
sub =
  [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> Maybe [Term] -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Key -> Maybe Term) -> [Key] -> Maybe [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Key -> Maybe Term
val [Key
0 .. Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
gammaKey -> Key -> Key
forall a. Num a => a -> a -> a
-Key
1]
    where
      val :: Key -> Maybe Term
val Key
i = case Key -> Sub -> Maybe (Relevance, Term)
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
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 :: forall (m :: * -> *).
PureTCM m =>
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 (Key -> Substitution -> Substitution
forall a. Key -> Substitution' a -> Substitution' a
liftS (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
k) Substitution
sub) Term
lhs
      String
-> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking postponed equality between" , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs')
        , TCMT IO Doc
" and " , Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs) ]) (m (Maybe Blocked_) -> 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
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 -> Key -> TCMT IO Doc -> m (Either a b) -> m (Either a b)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                   [ TCMT IO Doc
"matching failed during" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
msg
                   , TCMT IO Doc
"blocking: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Show a => a -> String
show a
b) ]) (m (Either a b) -> m (Either a b))
-> m (Either a b) -> m (Either a b)
forall a b. (a -> b) -> a -> b
$ Either a b -> m (Either a b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either a b
forall a b. a -> Either a b
Left a
b)
  m (Either Blocked_ 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 msub :: Maybe Substitution
msub = Telescope -> Sub -> Maybe Substitution
makeSubstitution Telescope
gamma (Sub -> Maybe Substitution) -> Sub -> Maybe Substitution
forall a b. (a -> b) -> a -> b
$ NLMState
sNLMState -> Lens' Sub NLMState -> Sub
forall o i. o -> Lens' i o -> i
^.(Sub -> f Sub) -> NLMState -> f NLMState
Lens' Sub NLMState
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
forall o i. o -> Lens' i o -> i
^.(PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
Lens' PostponedEquations NLMState
nlmEqs
    String
-> Key
-> TCMT IO Doc
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
90 (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"msub = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe Substitution -> String
forall a. Show a => a -> String
show Maybe Substitution
msub) (m (Either Blocked_ Substitution)
 -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ case Maybe Substitution
msub of
      Maybe Substitution
Nothing -> String -> Blocked_ -> m (Either Blocked_ Substitution)
forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"checking that all variables are bound" Blocked_
forall t. Blocked' t ()
notBlocked_
      Just Substitution
sub -> 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 a. a -> m a
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 :: forall (m :: * -> *).
PureTCM m =>
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 a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left Blocker
b      -> Maybe Blocked_ -> m (Maybe Blocked_)
forall a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Blocked_
forall a. Maybe a
Nothing
  Right Bool
False -> String
-> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"mismatch between " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
      , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ do
    Maybe Blocked_ -> m (Maybe Blocked_)
forall a. a -> m a
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 :: forall (m :: * -> *). PureTCM m => 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
    QName -> m (Maybe Key)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Key)
getNumberOfParameters QName
c m (Maybe Key)
-> (Maybe Key -> m (Maybe (QName, Type)))
-> m (Maybe (QName, Type))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Key
npars -> do
        let ws :: Args
ws = Key -> Arg Term -> Args
forall a. Key -> a -> [a]
replicate (Key
npars Key -> Key -> Key
forall a. Num a => a -> a -> a
- Args -> Key
forall a. Sized a => a -> Key
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
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
`piApplyM` (Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
ws)
        Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
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)
      Maybe Key
Nothing -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Type)
forall a. Maybe a
Nothing
  Term
_ -> Maybe (QName, Type) -> m (Maybe (QName, Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Type)
forall a. Maybe a
Nothing