{-# 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 s :: 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 f :: Sub -> f Sub
f s :: 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
<&> \x :: Sub
x -> NLMState
s {_nlmSub :: Sub
_nlmSub = Sub
x}

nlmEqs :: Lens' PostponedEquations NLMState
nlmEqs :: (PostponedEquations -> f PostponedEquations)
-> NLMState -> f NLMState
nlmEqs f :: PostponedEquations -> f PostponedEquations
f s :: 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
<&> \x :: 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 ()
nlm = do
  (ok :: Either Blocked_ ()
ok,out :: 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 block :: 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 r :: Relevance
r i :: Int
i a :: Type
a v :: 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
    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 (r' :: Relevance
r',v' :: 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 gamma :: Telescope
gamma k :: Telescope
k a :: Type
a u :: Term
u v :: Term
v = do
  VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
               [ "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)
               , " 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k t :: Dom t
t p :: Arg a
p v :: 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k (t :: Type
t, hd :: Term
hd) [] [] = () -> NLM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  match r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k (t :: Type
t, hd :: Term
hd) [] _  = 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k (t :: Type
t, hd :: Term
hd) _  [] = 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k (t :: Type
t, hd :: Term
hd) (p :: Elim' NLPat
p:ps :: [Elim' NLPat]
ps) (v :: Elim
v:vs :: Elims
vs) = case (Elim' NLPat
p,Elim
v) of
    (Apply p :: Arg NLPat
p, Apply v :: Arg Term
v) -> do
      ~(Pi a :: Dom Type
a b :: 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 o :: ProjOrigin
o f :: QName
f, Proj o' :: ProjOrigin
o' f' :: QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> do
      ~(Just (El _ (Pi a :: Dom Type
a b :: 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 _ f :: QName
f, Proj _ f' :: 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 "rewriting.match" 20 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ "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
        , " 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{} , _    ) -> NLM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- TODO
    (_ , 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k t :: t
t p :: Dom a
p v :: 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k _ (NLPType sp :: NLPSort
sp p :: NLPat
p) (El s :: Sort' Term
s a :: 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 r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k _ p :: NLPSort
p s :: 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 "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ "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)
      , "  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 lp :: NLPat
lp  , Type l :: 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 lp :: NLPat
lp  , Prop l :: Level' Term
l  ) -> Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
forall t a b.
Match t a b =>
Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
match Relevance
r Telescope
gamma Telescope
k () NLPat
lp Level' Term
l
      (PInf      , Inf     ) -> NLM ()
yes
      (PSizeUniv , SizeUniv) -> NLM ()
yes

      -- blocked cases
      (_ , UnivSort{}) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (_ , PiSort{}  ) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (_ , FunSort{} ) -> Blocked_ -> NLM ()
matchingBlocked Blocked_
b
      (_ , MetaS m :: MetaId
m _ ) -> 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
      (_ , _) -> NLM ()
no

instance Match () NLPat Level where
  match :: Relevance
-> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
match r :: Relevance
r gamma :: Telescope
gamma k :: Telescope
k _ p :: NLPat
p l :: Level' Term
l = do
    Type
t <- Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType 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 r0 :: Relevance
r0 gamma :: Telescope
gamma k :: Telescope
k t :: Type
t p :: NLPat
p v :: 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
        (v :: Term
v,t :: 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 "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ "matching pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyPat
      , "  with term      " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyTerm
      , "  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 "rewriting.match" 80 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ "  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)
      , "  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)
      , "  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 "rewriting.match" 70 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ "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
      , "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 msg :: 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 "rewriting.match" 10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ "mismatch between" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyPat
            , " and " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
prettyTerm
            , " 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 "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ "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 b' :: 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 "rewriting.match" 10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ "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 "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ "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 w :: Term
w = case Term
w of
          MetaV m :: MetaId
m es :: 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 ()
          _          -> TCM Doc -> NLM ()
no ""
    case NLPat
p of
      PVar i :: Int
i bvs :: [Arg Int]
bvs -> VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "rewriting.match" 60 ("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 b :: Blocked_
b         -> Blocked_ -> NLM ()
block Blocked_
b
          Right Nothing  -> TCM Doc -> NLM ()
no ""
          Right (Just v :: 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 f :: QName
f ps :: [Elim' NLPat]
ps -> VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "rewriting.match" 60 ("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 f' :: QName
f' es :: 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 c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs
            | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead -> QName
conName ConHead
c -> do
                ~(Just (_ , ct :: 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
          _ | Pi a :: Dom Type
a b :: 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 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 0 ]
                body :: Term
body  = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise 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 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
          _ | Just (d :: QName
d, pars :: 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
            (tel :: Telescope
tel, c :: ConHead
c, ci :: ConInfo
ci, vs :: 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 (_ , ct :: 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 fld :: 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 m :: MetaId
m es :: 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 ()
          v :: Term
v -> Term -> NLM ()
maybeBlock Term
v
      PLam i :: ArgInfo
i p' :: Abs NLPat
p' -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
        Pi a :: Dom Type
a b :: Abs Type
b -> do
          let body :: Term
body = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise 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 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 m :: MetaId
m es :: 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 ()
        v :: Term
v -> Term -> NLM ()
maybeBlock Term
v
      PPi pa :: Dom NLPType
pa pb :: Abs NLPType
pb -> case Term
v of
        Pi a :: Dom Type
a b :: 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)
        v :: Term
v -> Term -> NLM ()
maybeBlock Term
v
      PSort ps :: NLPSort
ps -> case Term
v of
        Sort s :: 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
        v :: Term
v -> Term -> NLM ()
maybeBlock Term
v
      PBoundVar i :: Int
i ps :: [Elim' NLPat]
ps -> case Term
v of
        Var i' :: Int
i' es :: 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
        _ | Pi a :: Dom Type
a b :: 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 (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 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 0 ]
              body :: Term
body  = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise 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 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
        _ | Just (d :: QName
d, pars :: 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
          (tel :: Telescope
tel, c :: ConHead
c, ci :: ConInfo
ci, vs :: 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 (_ , ct :: 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
$ \fld :: 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)
        v :: Term
v -> Term -> NLM ()
maybeBlock Term
v
      PTerm u :: Term
u -> VerboseKey -> Int -> TCM Doc -> NLM () -> NLM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc "rewriting.match" 60 ("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 xs :: IntSet
xs v :: a
v = do
  (mxs :: IntMap IsFree
mxs , v' :: 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 ms :: 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 (\ m :: 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
    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 ms1 :: MetaSet
ms1) f2 :: IsFree
f2
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms1  = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree ms1 :: MetaSet
ms1) f2 :: IsFree
f2@(MaybeFree ms2 :: MetaSet
ms2)
      | MetaSet -> Bool
forall a. Null a => a -> Bool
null MetaSet
ms2  = IsFree
f2
      | Bool
otherwise = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree ms1 :: MetaSet
ms1) NotFree = IsFree
f1
    pickFree NotFree f2 :: IsFree
f2 = IsFree
f2


makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution :: Telescope -> Sub -> Substitution
makeSubstitution gamma :: Telescope
gamma sub :: 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 [0 .. Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gammaInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]) Substitution
forall a. Substitution' a
IdS
    where
      val :: Int -> Maybe Term
val i :: Int
i = case Int -> Sub -> Maybe (Relevance, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i Sub
sub of
                Just (Irrelevant, v :: 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 (_         , v :: Term
v) -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v
                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 sub :: Substitution
sub eqs :: 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 k :: Telescope
k a :: Type
a lhs :: Term
lhs rhs :: 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 "rewriting.match" 30 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ "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')
        , " 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 gamma :: Telescope
gamma t :: t
t p :: a
p v :: b
v = do
  let no :: VerboseKey -> a -> m (Either a b)
no msg :: VerboseKey
msg b :: 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 "rewriting.match" 10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
                   [ "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
                   , "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 "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
$ \ s :: 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 "rewriting.match" 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
$ "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
      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 b :: Blocked_
b  -> VerboseKey -> Blocked_ -> m (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(MonadDebug m, Show a) =>
VerboseKey -> a -> m (Either a b)
no "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 a :: Type
a u :: Term
u v :: 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
  True -> Maybe Blocked_ -> m (Maybe Blocked_)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Blocked_
forall a. Maybe a
Nothing
  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 "rewriting.match" 10 ([TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ "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
      , " 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 ())
              (\m :: MetaId
m -> MetaId -> () -> Blocked_
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m ())