{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE UndecidableInstances     #-}

{- |  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.Monad.State

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.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.Utils.Either
import Agda.Utils.Except
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.
type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)

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

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

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

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

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

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

-- | Add substitution @i |-> v : a@ to result of matching.
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellSub Relevance
r Int
i Type
a Term
v = do
  Maybe (Relevance, Term)
old <- Int -> Sub -> Maybe (Relevance, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i (Sub -> Maybe (Relevance, Term))
-> ExceptT Blocked_ (StateT NLMState ReduceM) Sub
-> ExceptT
     Blocked_ (StateT NLMState ReduceM) (Maybe (Relevance, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Sub NLMState
-> ExceptT Blocked_ (StateT NLMState ReduceM) Sub
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Sub NLMState
nlmSub
  case Maybe (Relevance, Term)
old of
    Maybe (Relevance, Term)
Nothing -> Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= Int -> (Relevance, Term) -> Sub -> Sub
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Relevance
r,Term
v)
    Just (Relevance
r',Term
v')
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r  -> () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r' -> Lens' Sub NLMState
nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= Int -> (Relevance, Term) -> Sub -> Sub
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Relevance
r,Term
v)
      | Bool
otherwise       -> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Blocked_)
-> (Blocked_ -> NLM ()) -> NLM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (Type
-> Term
-> Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Blocked_)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m,
 HasBuiltins 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
  VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
               [ TCM Doc
"adding equality between" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)
               , TCM Doc
" and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
  Lens' PostponedEquations NLMState
nlmEqs Lens' PostponedEquations NLMState
-> (PostponedEquations -> PostponedEquations) -> NLM ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= (Telescope -> Type -> Term -> Term -> PostponedEquation
PostponedEquation Telescope
k Type
a Term
u Term
vPostponedEquation -> PostponedEquations -> PostponedEquations
forall a. a -> [a] -> [a]
:)

type Sub = IntMap (Relevance, Term)

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

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

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

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

instance Match (Type, Term) [Elim' NLPat] Elims where
  match :: Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t, Term
hd) [] [] = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Term
hd) [] Elims
_  = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
ReallyNotBlocked ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Term
hd) [Elim' NLPat]
_  [] = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
ReallyNotBlocked ()
  match Relevance
r Telescope
gamma Telescope
k (Type
t, Term
hd) (Elim' NLPat
p:[Elim' NLPat]
ps) (Elim
v:Elims
vs) = case (Elim' NLPat
p,Elim
v) of
    (Apply Arg NLPat
p, Apply Arg Term
v) -> do
      ~(Pi Dom Type
a Abs Type
b) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
      Relevance
-> Telescope
-> Telescope
-> Dom Type
-> Arg NLPat
-> Arg Term
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k Dom Type
a Arg NLPat
p Arg Term
v
      Type
t' <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Type
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Type)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall a b. (a -> b) -> a -> b
$ Type
t Type -> Arg Term -> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Arg Term
v
      let hd' :: Term
hd' = Term
hd Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Arg Term
v ]
      Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t',Term
hd') [Elim' NLPat]
ps Elims
vs

    (Proj ProjOrigin
o QName
f, Proj ProjOrigin
o' QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> do
      ~(Just (El Sort' Term
_ (Pi Dom Type
a Abs Type
b))) <- QName
-> Type -> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Type))
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
      let t' :: Type
t' = Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
hd
      Term
hd' <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Term
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Term)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall a b. (a -> b) -> a -> b
$ ProjOrigin
-> QName
-> Arg Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) 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
hd)
      Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
t',Term
hd') [Elim' NLPat]
ps Elims
vs

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

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

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

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

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

instance Match () NLPSort Sort where
  match :: Relevance
-> Telescope -> Telescope -> () -> NLPSort -> Sort' Term -> NLM ()
match Relevance
r Telescope
gamma Telescope
k ()
_ NLPSort
p Sort' Term
s = do
    Blocked (Sort' Term)
bs <- Sort' Term
-> ExceptT
     Blocked_ (StateT NLMState ReduceM) (Blocked (Sort' Term))
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort' Term
s
    let b :: Blocked_
b = Blocked (Sort' Term) -> Blocked_
forall (f :: * -> *) a. Functor f => f a -> f ()
void Blocked (Sort' Term)
bs
        s :: Sort' Term
s = Blocked (Sort' Term) -> Sort' Term
forall t. Blocked t -> t
ignoreBlocking Blocked (Sort' Term)
bs
        yes :: NLM ()
yes = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        no :: NLM ()
no  = Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
ReallyNotBlocked ()
    VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ TCM Doc
"matching pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (NLPSort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPSort
p)
      , TCM Doc
"  with sort      " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Sort' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
    case (NLPSort
p , Sort' Term
s) of
      (PType NLPat
lp  , Type Level' Term
l  ) -> Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPat
lp Level' Term
l
      (PProp NLPat
lp  , Prop Level' Term
l  ) -> Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPat
lp Level' Term
l
      (NLPSort
PInf      , Sort' Term
Inf     ) -> NLM ()
yes
      (NLPSort
PSizeUniv , Sort' Term
SizeUniv) -> 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 -> t -> Blocked t
Blocked MetaId
m ()

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

instance Match () NLPat Level where
  match :: Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
match Relevance
r Telescope
gamma Telescope
k ()
_ NLPat
p Level' Term
l = do
    Type
t <- Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
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)
-> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Term)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey
-> ExceptT Blocked_ (StateT NLMState ReduceM) (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getBuiltin' VerboseKey
builtinLevel
    Term
v <- Level' Term -> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
    Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k Type
t NLPat
p Term
v

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

      PDef QName
f [Elim' NLPat]
ps -> VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
60 (TCM Doc
"matching a PDef: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$ do
        Term
v <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Term
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Term)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall a b. (a -> b) -> a -> b
$ Term -> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (Term -> ExceptT Blocked_ (StateT NLMState ReduceM) Term)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
-> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> ExceptT Blocked_ (StateT NLMState ReduceM) Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
        case Term
v of
          Def QName
f' Elims
es
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'   -> do
                Type
ft <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Type
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Type)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType (Definition -> Type)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
-> ExceptT Blocked_ (StateT NLMState ReduceM) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
                Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ft , QName -> Elims -> Term
Def QName
f []) [Elim' NLPat]
ps Elims
es
          Con ConHead
c ConInfo
ci Elims
vs
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c -> do
                ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT
   Blocked_
   (StateT NLMState ReduceM)
   (Maybe ((QName, Type, Args), Type))
 -> ExceptT
      Blocked_
      (StateT NLMState ReduceM)
      (Maybe ((QName, Type, Args), Type)))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ ConHead
-> Type
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t
                Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) [Elim' NLPat]
ps Elims
vs
          Term
_ | Pi Dom Type
a Abs Type
b <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
t -> do
            let ai :: ArgInfo
ai    = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a
                pbody :: NLPat
pbody = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' NLPat] -> [Elim' NLPat]
forall t a. Subst t a => Int -> a -> a
raise Int
1 [Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++ [ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NLPat -> Arg NLPat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
                body :: Term
body  = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
                k' :: Telescope
k'    = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b) Telescope
k)
            Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) NLPat
pbody Term
body
          Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          -- If v is not of record constructor form but we are matching at record
          -- type, e.g., we eta-expand both v to (c vs) and
          -- the pattern (p = PDef f ps) to @c (p .f1) ... (p .fn)@.
            Defn
def <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Defn
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Defn)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef (Definition -> Defn)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
            (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- Telescope
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT
   Blocked_
   (StateT NLMState ReduceM)
   (Telescope, ConHead, ConInfo, Args)
 -> ExceptT
      Blocked_
      (StateT NLMState ReduceM)
      (Telescope, ConHead, ConInfo, Args))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall a b. (a -> b) -> a -> b
$ QName
-> Args
-> Defn
-> Term
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
            ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT
   Blocked_
   (StateT NLMState ReduceM)
   (Maybe ((QName, Type, Args), Type))
 -> ExceptT
      Blocked_
      (StateT NLMState ReduceM)
      (Maybe ((QName, Type, Args), Type)))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ ConHead
-> Type
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t
            let flds :: [Arg QName]
flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
def
                mkField :: QName -> NLPat
mkField QName
fld = QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++ [ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])
                -- Issue #3335: when matching against the record constructor,
                -- don't add projections but take record field directly.
                ps' :: [Elim' NLPat]
ps'
                  | ConHead -> QName
conName ConHead
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f = [Elim' NLPat]
ps
                  | Bool
otherwise      = (Arg QName -> Elim' NLPat) -> [Arg QName] -> [Elim' NLPat]
forall a b. (a -> b) -> [a] -> [b]
map (Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat)
-> (Arg QName -> Arg NLPat) -> Arg QName -> Elim' NLPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> NLPat) -> Arg QName -> Arg NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> NLPat
mkField) [Arg QName]
flds
            Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ct, ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) [Elim' NLPat]
ps' ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs)
          MetaV MetaId
m Elims
es -> do
            Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ()
          Term
v -> Term -> NLM ()
maybeBlock Term
v
      PLam ArgInfo
i Abs NLPat
p' -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Pi Dom Type
a Abs Type
b -> do
          let body :: Term
body = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Int -> Term
var Int
0)]
              k' :: Telescope
k'   = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) (Abs NLPat -> NLPat
forall t a. Subst t a => Abs a -> a
absBody Abs NLPat
p') Term
body
        MetaV MetaId
m Elims
es -> Blocked_ -> NLM ()
matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ()
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PPi Dom NLPType
pa Abs NLPType
pb -> case Term
v of
        Pi Dom Type
a Abs Type
b -> do
          Relevance
-> Telescope
-> Telescope
-> ()
-> Dom NLPType
-> Dom Type
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () Dom NLPType
pa Dom Type
a
          let k' :: Telescope
k' = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' () (Abs NLPType -> NLPType
forall t a. Subst t a => Abs a -> a
absBody Abs NLPType
pb) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PSort NLPSort
ps -> case Term
v of
        Sort Sort' Term
s -> Relevance
-> Telescope -> Telescope -> () -> NLPSort -> Sort' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPSort
ps Sort' Term
s
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PBoundVar Int
i [Elim' NLPat]
ps -> case Term
v of
        Var Int
i' Elims
es | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' -> do
          let ti :: Type
ti = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> Dom Type -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
k) Int
i
          Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ti , Int -> Term
var Int
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 = Int -> [Elim' NLPat] -> NLPat
PBoundVar (Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' NLPat] -> [Elim' NLPat]
forall t a. Subst t a => Int -> a -> a
raise Int
1 [Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++ [ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NLPat -> Arg NLPat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
              body :: Term
body  = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
              k' :: Telescope
k'    = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b) Telescope
k)
          Relevance
-> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k' (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) NLPat
pbody Term
body
        Term
_ | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
          Defn
def <- Telescope
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT Blocked_ (StateT NLMState ReduceM) Defn
 -> ExceptT Blocked_ (StateT NLMState ReduceM) Defn)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef (Definition -> Defn)
-> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
-> ExceptT Blocked_ (StateT NLMState ReduceM) Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExceptT Blocked_ (StateT NLMState ReduceM) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          (Telescope
tel, ConHead
c, ConInfo
ci, Args
vs) <- Telescope
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT
   Blocked_
   (StateT NLMState ReduceM)
   (Telescope, ConHead, ConInfo, Args)
 -> ExceptT
      Blocked_
      (StateT NLMState ReduceM)
      (Telescope, ConHead, ConInfo, Args))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall a b. (a -> b) -> a -> b
$ QName
-> Args
-> Defn
-> Term
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
          ~(Just ((QName, Type, Args)
_ , Type
ct)) <- Telescope
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (ExceptT
   Blocked_
   (StateT NLMState ReduceM)
   (Maybe ((QName, Type, Args), Type))
 -> ExceptT
      Blocked_
      (StateT NLMState ReduceM)
      (Maybe ((QName, Type, Args), Type)))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ ConHead
-> Type
-> ExceptT
     Blocked_
     (StateT NLMState ReduceM)
     (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t
          let flds :: [Arg QName]
flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term QName]
recFields Defn
def
              ps' :: [Arg NLPat]
ps'  = (Arg QName -> Arg NLPat) -> [Arg QName] -> [Arg NLPat]
forall a b. (a -> b) -> [a] -> [b]
map ((QName -> NLPat) -> Arg QName -> Arg NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
-> (QName -> NLPat) -> Arg QName -> Arg NLPat
forall a b. (a -> b) -> a -> b
$ \QName
fld -> Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i ([Elim' NLPat]
ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
forall a. [a] -> [a] -> [a]
++ [ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld])) [Arg QName]
flds
          Relevance
-> Telescope
-> Telescope
-> (Type, Term)
-> [Elim' NLPat]
-> Elims
-> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k (Type
ct, ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) ((Arg NLPat -> Elim' NLPat) -> [Arg NLPat] -> [Elim' NLPat]
forall a b. (a -> b) -> [a] -> [b]
map Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply [Arg NLPat]
ps') ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs)
        Term
v -> Term -> NLM ()
maybeBlock Term
v
      PTerm Term
u -> VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
60 (TCM Doc
"matching a PTerm" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
gamma Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
k) (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
forall a b. (a -> b) -> a -> b
$
        Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
tellEq Telescope
gamma Telescope
k Type
t Term
u Term
v

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

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


makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution Telescope
gamma Sub
sub =
  Empty -> [Maybe Term] -> Substitution -> Substitution
forall a.
DeBruijn a =>
Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Int -> Maybe Term) -> [Int] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Term
val [Int
0 .. Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gammaInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]) Substitution
forall a. Substitution' a
IdS
    where
      val :: Int -> Maybe Term
val Int
i = case Int -> Sub -> Maybe (Relevance, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i Sub
sub of
                Just (Relevance
Irrelevant, Term
v) -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
dontCare Term
v
                Just (Relevance
_         , Term
v) -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v
                Maybe (Relevance, Term)
Nothing              -> Maybe Term
forall a. Maybe a
Nothing

checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m)
                        => Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations :: Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs = PostponedEquations
-> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' PostponedEquations
eqs ((PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_))
-> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$
  \ (PostponedEquation Telescope
k Type
a Term
lhs Term
rhs) -> do
      let lhs' :: Term
lhs' = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
k) Substitution
sub) Term
lhs
      VerboseKey
-> Int -> TCM Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ TCM Doc
"checking postponed equality between" , Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs')
        , TCM Doc
" and " , Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs) ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ do
      Telescope -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
k (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> m (Maybe Blocked_)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m,
 HasBuiltins m) =>
Type -> Term -> Term -> m (Maybe Blocked_)
equal Type
a Term
lhs' Term
rhs

-- main function
nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m, Match t a b)
            => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch :: Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
gamma t
t a
p b
v = do
  let no :: VerboseKey -> a -> m (Either a b)
no VerboseKey
msg a
b = VerboseKey -> Int -> TCM Doc -> m (Either a b) -> m (Either a b)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
                   [ TCM Doc
"matching failed during" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text VerboseKey
msg
                   , TCM Doc
"blocking: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (a -> VerboseKey
forall a. Show a => a -> VerboseKey
show a
b) ]) (m (Either a b) -> m (Either a b))
-> m (Either a b) -> m (Either a b)
forall a b. (a -> b) -> a -> b
$ Either a b -> m (Either a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either a b
forall a b. a -> Either a b
Left a
b)
  m (Either Blocked_ NLMState)
-> (Blocked_ -> m (Either Blocked_ Substitution))
-> (NLMState -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (NLM () -> m (Either Blocked_ NLMState)
forall (m :: * -> *).
MonadReduce m =>
NLM () -> m (Either Blocked_ NLMState)
runNLM (NLM () -> m (Either Blocked_ NLMState))
-> NLM () -> m (Either Blocked_ NLMState)
forall a b. (a -> b) -> a -> b
$ Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
Relevant Telescope
gamma Telescope
forall a. Tele a
EmptyTel t
t a
p b
v) (VerboseKey -> Blocked_ -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(MonadDebug m, Show a) =>
VerboseKey -> a -> m (Either a b)
no VerboseKey
"matching") ((NLMState -> m (Either Blocked_ Substitution))
 -> m (Either Blocked_ Substitution))
-> (NLMState -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ \ NLMState
s -> do
    let sub :: Substitution
sub = Telescope -> Sub -> Substitution
makeSubstitution Telescope
gamma (Sub -> Substitution) -> Sub -> Substitution
forall a b. (a -> b) -> a -> b
$ NLMState
sNLMState -> Lens' Sub NLMState -> Sub
forall o i. o -> Lens' i o -> i
^.Lens' Sub NLMState
nlmSub
        eqs :: PostponedEquations
eqs = NLMState
sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
forall o i. o -> Lens' i o -> i
^.Lens' PostponedEquations NLMState
nlmEqs
    VerboseKey
-> Int
-> TCM Doc
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
90 (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"sub = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Substitution -> VerboseKey
forall a. Show a => a -> VerboseKey
show Substitution
sub) (m (Either Blocked_ Substitution)
 -> m (Either Blocked_ Substitution))
-> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ do
    Maybe Blocked_
ok <- Substitution -> PostponedEquations -> m (Maybe Blocked_)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m,
 MonadDebug m) =>
Substitution -> PostponedEquations -> m (Maybe Blocked_)
checkPostponedEquations Substitution
sub PostponedEquations
eqs
    case Maybe Blocked_
ok of
      Maybe Blocked_
Nothing -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocked_ Substitution -> m (Either Blocked_ Substitution))
-> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
forall a b. (a -> b) -> a -> b
$ Substitution -> Either Blocked_ Substitution
forall a b. b -> Either a b
Right Substitution
sub
      Just Blocked_
b  -> VerboseKey -> Blocked_ -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(MonadDebug m, Show a) =>
VerboseKey -> a -> m (Either a b)
no VerboseKey
"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 :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m)
      => Type -> Term -> Term -> m (Maybe Blocked_)
equal :: Type -> Term -> Term -> m (Maybe Blocked_)
equal Type
a Term
u Term
v = Type -> Term -> Term -> m Bool
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v m Bool -> (Bool -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
True -> Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Blocked_
forall a. Maybe a
Nothing
  Bool
False -> VerboseKey
-> Int -> TCM Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"rewriting.match" Int
10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ TCM Doc
"mismatch between " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
      , TCM Doc
" and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
-> m (Maybe Blocked_) -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ do
    Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocked_ -> m (Maybe Blocked_))
-> Maybe Blocked_ -> m (Maybe Blocked_)
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Maybe Blocked_
forall a. a -> Maybe a
Just Blocked_
block

  where
    block :: Blocked_
block = Maybe MetaId -> Blocked_ -> (MetaId -> Blocked_) -> Blocked_
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((Term, Term) -> Maybe MetaId
forall a. TermLike a => a -> Maybe MetaId
firstMeta (Term
u, Term
v))
              (NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
ReallyNotBlocked ())
              (\MetaId
m -> MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ())