{-# 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 -> 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
<$ :: forall a b. a -> NLM b -> NLM a
$c<$ :: forall a b. a -> NLM b -> NLM a
fmap :: forall a b. (a -> b) -> NLM a -> NLM b
$cfmap :: forall a b. (a -> b) -> NLM a -> NLM b
Functor, Functor 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
<* :: forall a b. NLM a -> NLM b -> NLM a
$c<* :: forall a b. NLM a -> NLM b -> NLM a
*> :: forall a b. NLM a -> NLM b -> NLM b
$c*> :: forall a b. NLM a -> NLM b -> NLM b
liftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
$cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
$c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
pure :: forall a. a -> NLM a
$cpure :: forall a. a -> NLM a
Applicative, Applicative 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
return :: forall a. a -> NLM a
$creturn :: forall a. a -> NLM a
>> :: forall a b. NLM a -> NLM b -> NLM b
$c>> :: forall a b. NLM a -> NLM b -> NLM b
>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
$c>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
Monad, Monad NLM
forall a. String -> NLM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: forall a. String -> NLM a
$cfail :: forall a. String -> NLM a
Fail.MonadFail
           , Applicative 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
many :: forall a. NLM a -> NLM [a]
$cmany :: forall a. NLM a -> NLM [a]
some :: forall a. NLM a -> NLM [a]
$csome :: forall a. NLM a -> NLM [a]
<|> :: forall a. NLM a -> NLM a -> NLM a
$c<|> :: forall a. NLM a -> NLM a -> NLM a
empty :: forall a. NLM a
$cempty :: forall a. NLM a
Alternative, Monad NLM
Alternative 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
mplus :: forall a. NLM a -> NLM a -> NLM a
$cmplus :: forall a. NLM a -> NLM a -> NLM a
mzero :: forall a. NLM a
$cmzero :: forall a. NLM a
MonadPlus
           , MonadError Blocked_, MonadState NLMState
           , Functor NLM
MonadFail NLM
Applicative NLM
String -> NLM (Maybe (Builtin PrimFun))
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> (String -> m (Maybe (Builtin PrimFun)))
-> HasBuiltins m
getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
$cgetBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
HasBuiltins, Functor NLM
MonadFail NLM
Applicative NLM
MonadDebug NLM
HasOptions NLM
MonadTCEnv NLM
QName -> NLM RewriteRules
QName -> NLM (Either SigError Definition)
QName -> NLM Definition
forall (m :: * -> *).
Functor m
-> Applicative m
-> MonadFail m
-> HasOptions m
-> MonadDebug m
-> MonadTCEnv m
-> (QName -> m Definition)
-> (QName -> m (Either SigError Definition))
-> (QName -> m RewriteRules)
-> HasConstInfo m
getRewriteRulesFor :: QName -> NLM RewriteRules
$cgetRewriteRulesFor :: QName -> NLM RewriteRules
getConstInfo' :: QName -> NLM (Either SigError Definition)
$cgetConstInfo' :: QName -> NLM (Either SigError Definition)
getConstInfo :: QName -> NLM Definition
$cgetConstInfo :: QName -> NLM Definition
HasConstInfo, Monad NLM
Functor NLM
Applicative NLM
NLM PragmaOptions
NLM CommandLineOptions
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
commandLineOptions :: NLM CommandLineOptions
$ccommandLineOptions :: NLM CommandLineOptions
pragmaOptions :: NLM PragmaOptions
$cpragmaOptions :: NLM PragmaOptions
HasOptions, Monad NLM
NLM TCState
forall a. (TCState -> TCState) -> NLM a -> NLM a
forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
$cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
$clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
getTCState :: NLM TCState
$cgetTCState :: NLM TCState
ReadTCState
           , Monad NLM
NLM TCEnv
forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
askTC :: NLM TCEnv
$caskTC :: NLM TCEnv
MonadTCEnv, Applicative NLM
HasOptions NLM
MonadTCEnv NLM
ReadTCState 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
liftReduce :: forall a. ReduceM a -> NLM a
$cliftReduce :: forall a. ReduceM a -> NLM a
MonadReduce, MonadTCEnv NLM
forall a. Range -> String -> (Name -> NLM a) -> NLM a
forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
forall a. Name -> Dom Type -> NLM a -> NLM a
forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
forall (m :: * -> *).
MonadTCEnv m
-> (forall a. Name -> Dom Type -> m a -> m a)
-> (forall a. Name -> Term -> Dom Type -> m a -> m a)
-> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
-> (forall a. Range -> String -> (Name -> m a) -> m a)
-> MonadAddContext m
withFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
$cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
updateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
$cupdateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
addLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
$caddLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
addCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
$caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
MonadAddContext, Monad NLM
Functor NLM
Applicative NLM
NLM Bool
NLM Verbosity
NLM ProfileOptions
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
nowDebugPrinting :: forall a. NLM a -> NLM a
$cnowDebugPrinting :: forall a. NLM a -> NLM a
isDebugPrinting :: NLM Bool
$cisDebugPrinting :: NLM Bool
getProfileOptions :: NLM ProfileOptions
$cgetProfileOptions :: NLM ProfileOptions
getVerbosity :: NLM Verbosity
$cgetVerbosity :: NLM Verbosity
verboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
$cverboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
traceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
$ctraceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
formatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
$cformatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
MonadDebug
           , MonadDebug NLM
MonadTCEnv NLM
MonadReduce NLM
ReadTCState NLM
MonadAddContext NLM
HasBuiltins NLM
HasConstInfo 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 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError NLM a
f forall a b. (a -> b) -> a -> b
$ \case
    Blocked Blocker
b ()
_      -> Blocker -> NLM a
h Blocker
b
    err :: Blocked_
err@NotBlocked{} -> 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 = forall a. Null a => a
empty , _nlmEqs :: PostponedEquations
_nlmEqs = forall a. Null a => a
empty }
  null :: NLMState -> Bool
null NLMState
s = forall a. Null a => a -> Bool
null (NLMState
sforall o i. o -> Lens' i o -> i
^.Lens' Sub NLMState
nlmSub) Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null (NLMState
sforall o i. o -> Lens' i o -> i
^.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) 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) 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) <- forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
unNLM NLM ()
nlm) forall a. Null a => a
empty
  case Either Blocked_ ()
ok of
    Left Blocked_
block -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Blocked_
block
    Right ()
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right NLMState
out

matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked :: Blocked_ -> NLM ()
matchingBlocked = 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 <- forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Sub NLMState
nlmSub
  case Maybe (Relevance, Term)
old of
    Maybe (Relevance, Term)
Nothing -> Lens' Sub NLMState
nlmSub forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
i (Relevance
r,Term
v)
    Just (Relevance
r',Term
v')
      | forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r' -> Lens' Sub NLMState
nlmSub forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
i (Relevance
r,Term
v)
      | Bool
otherwise       -> forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (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
  forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
               [ TCMT IO Doc
"adding equality between" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)
               , TCMT IO Doc
" and " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v) ]) forall a b. (a -> b) -> a -> b
$ do
  Lens' PostponedEquations NLMState
nlmEqs 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
vforall 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` forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
p
                          in  forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r' Telescope
gamma Telescope
k (forall t e. Dom' t e -> e
unDom Dom t
t) (forall e. Arg e -> e
unArg Arg a
p) (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) [] [] = 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 forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Elims -> Term
hd) [Elim' NLPat]
_  [] = Blocked_ -> NLM ()
matchingBlocked forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked 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) =
   forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
50 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
     [ TCMT IO Doc
"matching elimination " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim' NLPat
p)
     , TCMT IO Doc
"  with               " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim
v)
     , TCMT IO Doc
"  eliminating head   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t)]) forall a b. (a -> b) -> a -> b
$ do

   let no :: NLM ()
no  = Blocked_ -> NLM ()
matchingBlocked forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()
   case (Elim' NLPat
p,Elim
v) of
    (Apply Arg NLPat
p, Apply Arg Term
v) -> (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Pi Dom Type
a Abs Type
b -> do
        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'  = forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (forall e. Arg e -> e
unArg Arg Term
v)
            hd' :: Elims -> Term
hd' = Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply Arg Term
vforall a. a -> [a] -> [a]
:)
        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 -> 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?) " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t) forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (IApply NLPat
x NLPat
y NLPat
p , IApply Term
u Term
v Term
i) -> (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) 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 <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
        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' = forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
b forall t. Apply t => t -> Args -> t
`apply` [ forall a. a -> Arg a
defaultArg Term
i ]
        let hd' :: Elims -> Term
hd' = Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> a -> a -> Elim' a
IApply Term
u Term
v Term
iforall a. a -> [a] -> [a]
:)
        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 -> 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?) " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (PathView -> Type
pathUnview PathView
t)) forall (m :: * -> *) a. MonadPlus m => m a
mzero

    (Proj ProjOrigin
o QName
f, Proj ProjOrigin
o' QName
f') | QName
f forall a. Eq a => a -> a -> Bool
== QName
f' -> do
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t) 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 forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
u
          Elims -> Term
hd' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> Elims -> t
applyE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
u)
          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
      forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
20 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"mismatch between projections " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
        , TCMT IO Doc
" and " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f' ]) forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

    (IApply{} , Elim
_    ) -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- TODO
    (Elim' NLPat
_ , IApply{}    ) -> 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 = forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k t
t (forall t e. Dom' t e -> e
unDom Dom a
p) (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) = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ do
    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
    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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s
    let b :: Blocked_
b = forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked Sort
bs
        s :: Sort
s = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
bs
        yes :: NLM ()
yes = forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: NLM ()
no  = Blocked_ -> NLM ()
matchingBlocked forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()
    forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"matching pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPSort
p)
      , TCMT IO Doc
"  with sort      " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s) ]) forall a b. (a -> b) -> a -> b
$ do
    case (NLPSort
p , Sort
s) of
      (PType NLPat
lp  , Type Level' Term
l  ) -> 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  ) -> 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  ) -> 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 forall a. Eq a => a -> a -> Bool
== IsFibrant
f, Integer
np 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 forall a b. (a -> b) -> a -> b
$ 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 <- forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    Term
v <- forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
    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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB (Term
v,Type
t)
    let n :: Key
n = forall a. Sized a => a -> Key
size Telescope
k
        b :: Blocked_
b = forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked (Term, Type)
vbt
        (Term
v,Type
t) = forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Term, Type)
vbt
        prettyPat :: TCMT IO Doc
prettyPat  = forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
p)
        prettyTerm :: TCMT IO Doc
prettyTerm = forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        prettyType :: TCMT IO Doc
prettyType = forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    Maybe (QName, Args)
etaRecord <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t
    Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview <- forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
    Bool
prop <- forall a b. (a -> b) -> Either a b -> b
fromRight forall a. HasCallStack => a
__IMPOSSIBLE__ forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ 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
    forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"matching pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyPat
      , TCMT IO Doc
"  with term      " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyTerm
      , TCMT IO Doc
"  of type        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyType ]) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
80 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"  raw pattern:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show NLPat
p)
      , TCMT IO Doc
"  raw term:     " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Term
v)
      , TCMT IO Doc
"  raw type:     " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Type
t) ]) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
70 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"pattern vars:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
      , TCMT IO Doc
"bound vars:     " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
k ]) forall a b. (a -> b) -> a -> b
$ do
    let yes :: NLM ()
yes = forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: TCMT IO Doc -> NLM ()
no TCMT IO Doc
msg = if Relevance
r forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant then NLM ()
yes else do
          forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"mismatch between" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyPat
            , TCMT IO Doc
" and " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyTerm
            , TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
prettyType
            , TCMT IO Doc
msg ]) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Blocked_
b) ]) forall a b. (a -> b) -> a -> b
$ do
          Blocked_ -> NLM ()
matchingBlocked Blocked_
b
        block :: Blocked_ -> NLM ()
block Blocked_
b' = if Relevance
r forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant then NLM ()
yes else do
          forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"matching blocked on meta"
            , forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Blocked_
b') ]) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"blocking tag from reduction: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Blocked_
b') ]) forall a b. (a -> b) -> a -> b
$ do
          Blocked_ -> NLM ()
matchingBlocked (Blocked_
b forall a. Monoid a => a -> a -> a
`mappend` Blocked_
b')
        maybeBlock :: Term -> NLM ()
maybeBlock = \case
          MetaV MetaId
m Elims
es -> Blocked_ -> NLM ()
matchingBlocked forall a b. (a -> b) -> a -> b
$ 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 -> 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: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Key
i)) forall a b. (a -> b) -> a -> b
$ do
        let allowedVars :: IntSet
            allowedVars :: IntSet
allowedVars = [Key] -> IntSet
IntSet.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Key]
bvs)
            badVars :: IntSet
            badVars :: IntSet
badVars = IntSet -> IntSet -> IntSet
IntSet.difference ([Key] -> IntSet
IntSet.fromList (forall a. Integral a => a -> [a]
downFrom Key
n)) IntSet
allowedVars
            perm :: Permutation
            perm :: Permutation
perm = Key -> [Key] -> Permutation
Perm Key
n forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg 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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Impossible -> Permutation -> a -> a
renameP HasCallStack => Impossible
impossible Permutation
perm Type
t
                v' :: Term
v' = Telescope -> Term -> Term
teleLam Telescope
tel forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Impossible -> Permutation -> a -> a
renameP HasCallStack => Impossible
impossible Permutation
perm Term
v
            in Relevance -> Key -> Type -> Term -> NLM ()
tellSub Relevance
r (Key
iforall a. Num a => a -> a -> a
-Key
n) Type
t' Term
v'

      PDef QName
f [Elim' NLPat]
ps -> 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: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f) forall a b. (a -> b) -> a -> b
$ do
        Term
v <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
        case Term
v of
          Def QName
f' Elims
es
            | QName
f forall a. Eq a => a -> a -> Bool
== QName
f'   -> do
                Type
ft <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
                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 forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c -> do
                forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Just ((QName, Type, Args)
_ , Type
ct) -> 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 <- forall t a. Type'' t a -> a
unEl Type
t -> do
            let ai :: ArgInfo
ai    = forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
                pbody :: NLPat
pbody = QName -> [Elim' NLPat] -> NLPat
PDef QName
f forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Key -> a -> a
raise Key
1 [Elim' NLPat]
ps forall a. [a] -> [a] -> [a]
++ [ forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
0 ]
                body :: Term
body  = forall a. Subst a => Key -> a -> a
raise Key
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [ forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
0 ]
                k' :: Telescope
k'    = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
            forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
            (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
            forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) 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 = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom 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 forall a. [a] -> [a] -> [a]
++ [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 forall a. Eq a => a -> a -> Bool
== QName
f = [Elim' NLPat]
ps
                      | Bool
otherwise      = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
                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' (forall a b. (a -> b) -> [a] -> [b]
map 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 forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b -> do
          let body :: Term
body = forall a. Subst a => Key -> a -> a
raise Key
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Key -> Term
var Key
0)]
              k' :: Telescope
k'   = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (forall a. Subst a => Abs a -> a
absBody Abs Type
b) (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 = forall a. Subst a => Key -> a -> a
raise Key
1 Term
v forall t. Apply t => t -> Elims -> t
`applyE` [ forall a. a -> a -> a -> Elim' a
IApply (forall a. Subst a => Key -> a -> a
raise Key
1 Term
x) (forall a. Subst a => Key -> a -> a
raise Key
1 Term
y) forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
0 ]
              k' :: Telescope
k'   = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (forall a. String -> a -> Abs a
Abs String
"i" Telescope
k)
          forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (forall a. Subst a => Abs a -> a
absBody Abs Type
b) (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
          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' = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' () (forall a. Subst a => Abs a -> a
absBody Abs NLPType
pb) (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 -> 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 forall a. Eq a => a -> a -> Bool
== Key
i' -> do
          let ti :: Type
ti = forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Key -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
k) Key
i
          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 <- forall t a. Type'' t a -> a
unEl Type
t -> do
          let ai :: ArgInfo
ai    = forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
              pbody :: NLPat
pbody = Key -> [Elim' NLPat] -> NLPat
PBoundVar (Key
1forall a. Num a => a -> a -> a
+Key
i) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Key -> a -> a
raise Key
1 [Elim' NLPat]
ps forall a. [a] -> [a] -> [a]
++ [ forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
0 ]
              body :: Term
body  = forall a. Subst a => Key -> a -> a
raise Key
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Key -> Term
var Key
0 ]
              k' :: Telescope
k'    = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) Telescope
k)
          forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) 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 = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
def
                  ps' :: [Arg NLPat]
ps'  = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \QName
fld -> Key -> [Elim' NLPat] -> NLPat
PBoundVar Key
i ([Elim' NLPat]
ps forall a. [a] -> [a] -> [a]
++ [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])) [Arg QName]
flds
              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) (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg NLPat]
ps') (forall a b. (a -> b) -> [a] -> [b]
map 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 -> 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)) 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 =
  forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Key -> Maybe Term
val [Key
0 .. forall a. Sized a => a -> Key
size Telescope
gammaforall a. Num a => a -> a -> a
-Key
1]
    where
      val :: Key -> Maybe Term
val Key
i = case forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
i Sub
sub of
                Just (Relevance
Irrelevant, Term
v) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Term
dontCare Term
v
                Just (Relevance
_         , Term
v) -> forall a. a -> Maybe a
Just Term
v
                Maybe (Relevance, Term)
Nothing              -> 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 = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' PostponedEquations
eqs forall a b. (a -> b) -> a -> b
$
  \ (PostponedEquation Telescope
k Type
a Term
lhs Term
rhs) -> do
      let lhs' :: Term
lhs' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Key -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Key
size Telescope
k) Substitution
sub) Term
lhs
      forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
30 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking postponed equality between" , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs')
        , TCMT IO Doc
" and " , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs) ]) forall a b. (a -> b) -> a -> b
$ do
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                   [ TCMT IO Doc
"matching failed during" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text String
msg
                   , TCMT IO Doc
"blocking: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show a
b) ]) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left a
b)
  forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either Blocked_ NLMState)
runNLM forall a b. (a -> b) -> a -> b
$ forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
Relevant Telescope
gamma forall a. Tele a
EmptyTel t
t a
p b
v) (forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"matching") forall a b. (a -> b) -> a -> b
$ \ NLMState
s -> do
    let msub :: Maybe Substitution
msub = Telescope -> Sub -> Maybe Substitution
makeSubstitution Telescope
gamma forall a b. (a -> b) -> a -> b
$ NLMState
sforall o i. o -> Lens' i o -> i
^.Lens' Sub NLMState
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
sforall o i. o -> Lens' i o -> i
^.Lens' PostponedEquations NLMState
nlmEqs
    forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
90 (forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"msub = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Maybe Substitution
msub) forall a b. (a -> b) -> a -> b
$ case Maybe Substitution
msub of
      Maybe Substitution
Nothing -> forall {m :: * -> *} {a} {b}.
(MonadDebug m, Show a) =>
String -> a -> m (Either a b)
no String
"checking that all variables are bound" forall t. Blocked' t ()
notBlocked_
      Just Substitution
sub -> do
        Maybe Blocked_
ok <- forall (m :: * -> *).
PureTCM m =>
Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs
        case Maybe Blocked_
ok of
          Maybe Blocked_
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Substitution
sub
          Just Blocked_
b  -> 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 = forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left Blocker
b      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()
  Right Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  Right Bool
False -> forall (m :: * -> *) a.
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m a -> m a
traceSDoc String
"rewriting.match" Key
10 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"mismatch between " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , TCMT IO Doc
" and " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ]) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked 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 []   -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName
f,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- 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
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Key)
getNumberOfParameters QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Key
npars -> do
        let ws :: Args
ws = forall a. Key -> a -> [a]
replicate (Key
npars forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Key
size Args
vs) forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg HasCallStack => Term
__DUMMY_TERM__
        Type
t0 <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
        Type
t <- Type
t0 forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` (Args
vs forall a. [a] -> [a] -> [a]
++ Args
ws)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
c , Type
t)
      Maybe Key
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing