{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

Given a lhs

  Δ ⊢ lhs : B

and a candidate term

  Γ ⊢ t : A

we seek a substitution Γ ⊢ σ : Δ such that

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

-}

module Agda.TypeChecking.Rewriting.NonLinMatch where

import Prelude hiding (null, sequence)

import Control.Applicative  ( Alternative )
import Control.Monad        ( 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 Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Irrelevance (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) =>
(SomeBuiltin -> NLM (Maybe (Builtin PrimFun))) -> HasBuiltins NLM
SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
(Functor m, Applicative m, MonadFail m) =>
(SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
$cgetBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
getBuiltinThing :: SomeBuiltin -> 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' TCState a -> (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' TCState a -> (a -> a) -> NLM b -> NLM b
forall (m :: * -> *).
Monad m =>
m TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
$cgetTCState :: NLM TCState
getTCState :: NLM TCState
$clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
$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. Origin -> 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. Origin -> 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. Origin -> 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. Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
addLetBinding' :: forall a. Origin -> 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
s NLMState -> Lens' NLMState Sub -> Sub
forall o i. o -> Lens' o i -> i
^. (Sub -> f Sub) -> NLMState -> f NLMState
Lens' NLMState Sub
nlmSub) Bool -> Bool -> Bool
&& PostponedEquations -> Bool
forall a. Null a => a -> Bool
null (NLMState
s NLMState -> Lens' NLMState PostponedEquations -> PostponedEquations
forall o i. o -> Lens' o i -> i
^. (PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
Lens' NLMState PostponedEquations
nlmEqs)

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

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

runNLM :: (MonadReduce m) => NLM () -> m (Either Blocked_ NLMState)
runNLM :: forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either Blocked_ NLMState)
runNLM NLM ()
nlm = do
  (ok,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 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
  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' NLMState Sub -> NLM Sub
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Sub -> f Sub) -> NLMState -> f NLMState
Lens' NLMState Sub
nlmSub
  case old of
    Maybe (Relevance, Term)
Nothing -> (Sub -> f Sub) -> NLMState -> f NLMState
Lens' NLMState Sub
nlmSub Lens' NLMState Sub -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (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' NLMState Sub
nlmSub Lens' NLMState Sub -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (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 -> Context -> Type -> Term -> Term -> NLM ()
tellEq :: Telescope -> Context -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Context
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 (Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)
               , TCMT IO Doc
" and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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' NLMState PostponedEquations
nlmEqs Lens' NLMState PostponedEquations
-> (PostponedEquations -> PostponedEquations) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (i -> i) -> m ()
%= (Context -> Type -> Term -> Term -> PostponedEquation
PostponedEquation Context
k Type
a Term
u Term
vPostponedEquation -> PostponedEquations -> PostponedEquations
forall a. a -> [a] -> [a]
:)

type Sub = IntMap (Relevance, Term)

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

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

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

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

instance Match [Elim' NLPat] Elims where
  match :: Relevance
-> Telescope
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
match Relevance
r Telescope
gamma Context
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 Context
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 Context
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 Context
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 (Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Elim' NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM Elim' NLPat
p)
     , TCMT IO Doc
"  with               " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
<+> Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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) -> Context -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> NLM Type -> NLM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM Term -> (Term -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Pi Dom Type
a Abs Type
b -> do
        Relevance
-> Telescope
-> Context
-> TypeOf (Arg Term)
-> Arg NLPat
-> Arg Term
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
k TypeOf (Arg Term)
Dom Type
a Arg NLPat
p Arg Term
v
        let t' :: Type
t'  = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v)
            hd' :: Elims -> Term
hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
vElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        Relevance
-> Telescope
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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) -> Context -> NLM PathView -> NLM PathView
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (Type -> NLM PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView (Type -> NLM PathView) -> NLM Type -> NLM PathView
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM PathView -> (PathView -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
_u Arg Term
_v -> do
        Right 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
        match r gamma k interval p i
        let t' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
i ]
        let hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
u Term
v Term
iElim -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        match r gamma k (t',hd') ps 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
      Context -> NLM (Maybe Type) -> NLM (Maybe Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (QName -> Type -> NLM (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> NLM (Maybe Type)) -> NLM Type -> NLM (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> NLM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) NLM (Maybe Type) -> (Maybe Type -> NLM ()) -> NLM ()
forall a b. NLM a -> (a -> NLM b) -> NLM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> do
          let u :: Term
u = Elims -> Term
hd []
              t' :: Type
t' = Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
          hd' <- Context -> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (NLM (Elims -> Term) -> NLM (Elims -> Term))
-> NLM (Elims -> Term) -> NLM (Elims -> Term)
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Term -> Elims -> Term) -> NLM Term -> NLM (Elims -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProjOrigin -> QName -> Arg Term -> NLM Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
u)
          match r gamma k (t',hd') ps vs
        Maybe Type
_ -> NLM ()
no

    (Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') | Bool
otherwise -> do
      String -> 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 a b => Match (Dom a) (Dom b) where
  match :: Relevance
-> Telescope
-> Context
-> TypeOf (Dom b)
-> Dom a
-> Dom b
-> NLM ()
match Relevance
r Telescope
gamma Context
k TypeOf (Dom b)
t Dom a
p Dom b
v = Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
k TypeOf b
TypeOf (Dom b)
t (Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
p) (Dom b -> b
forall t e. Dom' t e -> e
unDom Dom b
v)

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

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

      -- blocked cases
      (NLPSort
_ , UnivSort{}) -> Blocked_ -> 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
-> Context
-> TypeOf (Level' Term)
-> NLPat
-> Level' Term
-> NLM ()
match Relevance
r Telescope
gamma Context
k TypeOf (Level' Term)
_ NLPat
p Level' Term
l = do
    t <- Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Type) -> NLM (Maybe Term) -> NLM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> NLM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevel
    v <- reallyUnLevelView l
    match r gamma k t p v

instance Match NLPat Term where
  match :: Relevance  -- Are we currently matching in an irrelevant context?
        -> Telescope  -- The telescope of pattern variables
        -> Context    -- The context of lambda-bound variables
        -> Type       -- The type of the pattern
        -> NLPat      -- The pattern to match
        -> Term       -- The term to be matched against the pattern
        -> NLM ()
  match :: Relevance
-> Telescope -> Context -> Type -> NLPat -> Term -> NLM ()
match Relevance
r0 Telescope
gamma Context
k Type
t NLPat
p Term
v = do
    vbt <- Context -> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type)))
-> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
forall a b. (a -> b) -> a -> b
$ (Term, Type) -> NLM (Blocked (Term, Type))
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB (Term
v,Type
t)
    let n = Context -> Key
forall a. Sized a => a -> Key
size Context
k
        b = Blocked (Term, Type) -> Blocked_
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked (Term, Type)
vbt
        (v,t) = ignoreBlocking vbt
        prettyPat  = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ 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 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NLPat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
p
        prettyTerm = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
        prettyType = TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    etaRecord <- addContext k $ isEtaRecordType t
    pview <- pathViewAsPi'whnf
    prop <- fromRight __IMPOSSIBLE__ <.> runBlocked . addContext k $ isPropM t
    let r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
    traceSDoc "rewriting.match" 30 (sep
      [ "matching pattern " <+> prettyPat
      , "  with term      " <+> prettyTerm
      , "  of type        " <+> prettyType ]) $ do
    traceSDoc "rewriting.match" 80 (vcat
      [ "  raw pattern:  " <+> text (show p)
      , "  raw term:     " <+> text (show v)
      , "  raw type:     " <+> text (show t) ]) $ do
    traceSDoc "rewriting.match" 70 (vcat
      [ "pattern vars:   " <+> prettyTCM gamma
      , "bound vars:     " <+> prettyTCM k ]) $ do
    let yes = () -> NLM ()
forall a. a -> NLM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no TCMT IO Doc
msg = if Relevance
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_
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 = \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 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 vars :: [Key]
vars = (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
        let allowedVars :: IntSet
            allowedVars :: IntSet
allowedVars = [Key] -> IntSet
IntSet.fromList [Key]
vars
            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]
vars
            tel :: Telescope
            tel :: Telescope
tel = Permutation -> Context -> Telescope
permuteContext Permutation
perm Context
k
        ok <- Context
-> 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 => Context -> m a -> m a
addContext Context
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 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
        v <- Context -> NLM Term -> NLM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
forall a b. (a -> b) -> a -> b
$ Term -> NLM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Term -> NLM Term) -> NLM Term -> NLM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> NLM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
        case v of
          Def QName
f' Elims
es
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'   -> do
                ft <- Context -> NLM Type -> NLM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
                match r gamma k (ft , Def f) ps es
          Con ConHead
c ConInfo
ci Elims
vs
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c -> do
                Context
-> NLM (Maybe ((QName, Type, Args), Type))
-> NLM (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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' <- Context -> String -> Dom Type -> NLM Context
forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
            match r gamma k' (absBody b) pbody body
          Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          -- If v is not of record constructor form but we are matching at record
          -- type, e.g., we eta-expand both v to (c vs) and
          -- the pattern (p = PDef f ps) to @c (p .f1) ... (p .fn)@.
            RecordDefn def <- Context -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
            (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
            addContext k (getFullyAppliedConType c t) >>= \case
              Just ((QName, Type, Args)
_ , Type
ct) -> do
                let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
def
                    mkField :: QName -> NLPat
mkField QName
fld = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++ [ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])
                    -- Issue #3335: when matching against the record constructor,
                    -- don't add projections but take record field directly.
                    ps' :: [Elim' NLPat]
ps'
                      | ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f = [Elim' NLPat]
ps
                      | Bool
otherwise      = (Arg QName -> Elim' NLPat) -> [Arg QName] -> [Elim' NLPat]
forall a b. (a -> b) -> [a] -> [b]
map (Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat)
-> (Arg QName -> Arg NLPat) -> Arg QName -> Elim' NLPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
                Relevance
-> Telescope
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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' <- Context -> String -> Dom Type -> NLM Context
forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' (absBody b) (absBody p') body
        Term
_ | Left ((Dom Type
a,Abs Type
b),(Term
x,Term
y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview Type
t -> do
          let body :: Term
body = 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' <- Context -> String -> Dom Type -> NLM Context
forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
k String
"i" Dom Type
a
          match r gamma k' (absBody b) (absBody p') 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
-> Context
-> TypeOf (Dom Type)
-> Dom NLPType
-> Dom Type
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
k () Dom NLPType
pa Dom Type
a
          k' <- Context -> String -> Dom Type -> NLM Context
forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' () (absBody pb) (absBody b)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PSort NLPSort
ps -> case Term
v of
        Sort Sort
s -> Relevance
-> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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 = Type
-> (Dom' Term (Name, Type) -> Type)
-> Maybe (Dom' Term (Name, Type))
-> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) (Maybe (Dom' Term (Name, Type)) -> Type)
-> Maybe (Dom' Term (Name, Type)) -> Type
forall a b. (a -> b) -> a -> b
$ Key -> Context -> Maybe (Dom' Term (Name, Type))
lookupBV_ Key
i Context
k
          Relevance
-> Telescope
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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
1 Key -> 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' <- Context -> String -> Dom Type -> NLM Context
forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
k (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) Dom Type
a
          match r gamma k' (absBody b) pbody body
        Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          RecordDefn def <- Context -> NLM Defn -> NLM Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
          (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
          addContext k (getFullyAppliedConType c t) >>= \case
            Just ((QName, Type, Args)
_ , Type
ct) -> do
              let flds :: [Arg QName]
flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
def
                  ps' :: [Arg NLPat]
ps'  = (Arg QName -> Arg NLPat) -> [Arg QName] -> [Arg NLPat]
forall a b. (a -> b) -> [a] -> [b]
map ((QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
-> (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ \QName
fld -> 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
-> Context
-> TypeOf Elims
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Context
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 (Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$
        Telescope -> Context -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Context
k Type
t Term
u Term
v

extendContext :: MonadAddContext m => Context -> ArgName -> Dom Type -> m Context
extendContext :: forall (m :: * -> *).
MonadAddContext m =>
Context -> String -> Dom Type -> m Context
extendContext Context
cxt String
x Dom Type
a = Range -> String -> (Name -> m Context) -> m Context
forall a. Range -> String -> (Name -> m a) -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Range -> String -> (Name -> m a) -> m a
withFreshName Range
forall a. Null a => a
empty String
x \ Name
y -> Context -> m Context
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> m Context) -> Context -> m Context
forall a b. (a -> b) -> a -> b
$ (Type -> (Name, Type)) -> Dom Type -> Dom' Term (Name, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name
y,) Dom Type
a Dom' Term (Name, Type) -> Context -> Context
forall a. a -> [a] -> [a]
: Context
cxt


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

{-# SPECIALIZE checkPostponedEquations :: Substitution -> PostponedEquations -> TCM (Maybe Blocked_) #-}
checkPostponedEquations :: PureTCM m
                        => Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations :: forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe Blocked_)
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 Context
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 (Context -> Key
forall a. Sized a => a -> Key
size Context
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" , Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
k (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs')
        , TCMT IO Doc
" and " , Context -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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
      Context -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
addContext Context
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 a b)
            => Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch :: forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
gamma TypeOf b
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 -> Context -> TypeOf b -> a -> b -> NLM ()
forall a b.
Match a b =>
Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
match Relevance
Relevant Telescope
gamma Context
forall a. Null a => a
empty TypeOf b
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
s NLMState -> Lens' NLMState Sub -> Sub
forall o i. o -> Lens' o i -> i
^. (Sub -> f Sub) -> NLMState -> f NLMState
Lens' NLMState Sub
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
s NLMState -> Lens' NLMState PostponedEquations -> PostponedEquations
forall o i. o -> Lens' o i -> i
^. (PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
Lens' NLMState PostponedEquations
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
        ok <- Substitution -> PostponedEquations -> m (Maybe Blocked_)
forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs
        case 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
    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
    getNumberOfParameters c >>= \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__
        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
        t <- t0 `piApplyM` (vs ++ ws)
        return $ Just (c , 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