{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE NondecreasingIndentation #-}

-- | Checking confluence of rewrite rules.
--
-- Given a rewrite rule @f ps ↦ v@, we construct critical pairs
-- involving this as the main rule by searching for:
--
-- 1. *Different* rules @f ps' ↦ v'@ where @ps@ and @ps'@ can be
--    unified@.
--
-- 2. Subpatterns @g qs@ of @ps@ and rewrite rules @g qs' ↦ w@ where
--    @qs@ and @qs'@ can be unified.
--
-- Each of these leads to a *critical pair* @v₁ <-- u --> v₂@, which
-- should satisfy @v₁ = v₂@.

module Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules , checkConfluenceOfClause ) where

import Control.Applicative
import Control.Monad
import Control.Monad.Reader

import Data.Function ( on )
import Data.Functor ( ($>) )
import Data.List ( elemIndex , tails )
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars

import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance ( workOnTypes )
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Warning
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting.Clause
import Agda.TypeChecking.Rewriting.NonLinPattern
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

import Agda.Utils.Except
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Singleton
import Agda.Utils.Size


-- ^ Check confluence of the given rewrite rules wrt all other rewrite
--   rules (also amongst themselves).
checkConfluenceOfRules :: [RewriteRule] -> TCM ()
checkConfluenceOfRules :: [RewriteRule] -> TCM ()
checkConfluenceOfRules = Bool -> [RewriteRule] -> TCM ()
checkConfluenceOfRules' Bool
False

-- ^ Check confluence of the given clause wrt rewrite rules of the
-- constructors it matches against
checkConfluenceOfClause :: QName -> Int -> Clause -> TCM ()
checkConfluenceOfClause :: QName -> Int -> Clause -> TCM ()
checkConfluenceOfClause QName
f Int
i Clause
cl = do
  QName
fi <- QName -> Int -> TCM QName
clauseQName QName
f Int
i
  Maybe RewriteRule -> (RewriteRule -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (QName -> QName -> Clause -> Maybe RewriteRule
clauseToRewriteRule QName
f QName
fi Clause
cl) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
    Bool -> [RewriteRule] -> TCM ()
checkConfluenceOfRules' Bool
True [RewriteRule
rew]
    let matchables :: [QName]
matchables = RewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables RewriteRule
rew
    VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"Function" 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 -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"has matchable symbols" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
matchables)
    (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f [QName]
matchables

checkConfluenceOfRules' :: Bool -> [RewriteRule] -> TCM ()
checkConfluenceOfRules' :: Bool -> [RewriteRule] -> TCM ()
checkConfluenceOfRules' Bool
isClause [RewriteRule]
rews = TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

  [[RewriteRule]] -> ([RewriteRule] -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([RewriteRule] -> [[RewriteRule]]
forall a. [a] -> [[a]]
tails [RewriteRule]
rews) (([RewriteRule] -> TCM ()) -> TCM ())
-> ([RewriteRule] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
-> (RewriteRule -> [RewriteRule] -> TCM ())
-> [RewriteRule]
-> TCM ()
forall b a. b -> (a -> [a] -> b) -> [a] -> b
listCase (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((RewriteRule -> [RewriteRule] -> TCM ())
 -> [RewriteRule] -> TCM ())
-> (RewriteRule -> [RewriteRule] -> TCM ())
-> [RewriteRule]
-> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew [RewriteRule]
rewsRest -> do

  VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"Checking confluence of rule" 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 (RewriteRule -> QName
rewName RewriteRule
rew)

  let f :: QName
f   = RewriteRule -> QName
rewHead RewriteRule
rew
      qs :: PElims
qs  = RewriteRule -> PElims
rewPats RewriteRule
rew
      tel :: Telescope
tel = RewriteRule -> Telescope
rewContext RewriteRule
rew
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  (Type
fa , Elims -> Term
hdf) <- Telescope
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term))
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall a b. (a -> b) -> a -> b
$ Definition -> Type -> TCMT IO (Type, Elims -> Term)
makeHead Definition
def (RewriteRule -> Type
rewType RewriteRule
rew)

  -- Step 1: check other rewrite rules that overlap at top position
  TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> Bool -> TCMT IO [RewriteRule]
getRulesFor QName
f Bool
isClause) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' ->
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameName RewriteRule
rew') ([RewriteRule] -> Bool) -> [RewriteRule] -> Bool
forall a b. (a -> b) -> a -> b
$ RewriteRule
rewRewriteRule -> [RewriteRule] -> [RewriteRule]
forall a. a -> [a] -> [a]
:[RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hdf RewriteRule
rew RewriteRule
rew'

  -- Step 2: check other rewrite rules that overlap with a subpattern
  -- of this rewrite rule
  Elims
es <- PElims -> TCMT IO Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm PElims
qs
  TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
-> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall a b. (a -> b) -> a -> b
$ PType Elims -> Elims -> TCMT IO [OneHole Elims]
forall (m :: * -> *) p.
(MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m,
 AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
fa, Elims -> Term
hdf) Elims
es) ((OneHole Elims -> TCM ()) -> TCM ())
-> (OneHole Elims -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole ->
    Maybe (QName, Elims -> Term, Elims)
-> TCM () -> ((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe (QName, Elims -> Term, Elims)
headView (Term -> Maybe (QName, Elims -> Term, Elims))
-> Term -> Maybe (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Term
forall a. OneHole a -> Term
ohContents OneHole Elims
hole) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ (((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ())
-> ((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (QName
g , Elims -> Term
hdg , Elims
_) -> do
      TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> Bool -> TCMT IO [RewriteRule]
getRulesFor QName
g Bool
isClause) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew' ->
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew RewriteRule
rew' OneHole Elims
hole

  -- Step 3: check other rewrite rules that have a subpattern which
  -- overlaps with this rewrite rule
  Set QName -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Definition -> Set QName
defMatchable Definition
def) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
g -> do
    TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> TCMT IO [RewriteRule]
getClausesAndRewriteRulesFor QName
g) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Elims
es' <- PElims -> TCMT IO Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew')
        let tel' :: Telescope
tel' = RewriteRule -> Telescope
rewContext RewriteRule
rew'
        Definition
def' <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
g
        (Type
ga , Elims -> Term
hdg) <- Telescope
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term))
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall a b. (a -> b) -> a -> b
$ Definition -> Type -> TCMT IO (Type, Elims -> Term)
makeHead Definition
def' (RewriteRule -> Type
rewType RewriteRule
rew')
        TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
-> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall a b. (a -> b) -> a -> b
$ PType Elims -> Elims -> TCMT IO [OneHole Elims]
forall (m :: * -> *) p.
(MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m,
 AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
ga , Elims -> Term
hdg) Elims
es') ((OneHole Elims -> TCM ()) -> TCM ())
-> (OneHole Elims -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole ->
          Maybe (QName, Elims -> Term, Elims)
-> TCM () -> ((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe (QName, Elims -> Term, Elims)
headView (Term -> Maybe (QName, Elims -> Term, Elims))
-> Term -> Maybe (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Term
forall a. OneHole a -> Term
ohContents OneHole Elims
hole) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ (((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ())
-> ((QName, Elims -> Term, Elims) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (QName
f' , Elims -> Term
_ , Elims
_) ->
            Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdg Elims -> Term
hdf RewriteRule
rew' RewriteRule
rew OneHole Elims
hole

  where

    sameName :: RewriteRule -> RewriteRule -> Bool
sameName = QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) (QName -> QName -> Bool)
-> (RewriteRule -> QName) -> RewriteRule -> RewriteRule -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RewriteRule -> QName
rewName

    -- Check confluence of two rewrite rules that have the same head symbol,
    -- e.g. @f ps --> a@ and @f ps' --> b@.
    checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
    checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hd RewriteRule
rew1 RewriteRule
rew2 =
      Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        Substitution
sub1 <- Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew1
        Substitution
sub2 <- Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew2

        let f :: QName
f    = RewriteRule -> QName
rewHead RewriteRule
rew1 -- == rewHead rew2
            a1 :: Type
a1   = Substitution -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew1
            a2 :: Type
a2   = Substitution -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew2

        Elims
es1 <- Substitution -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> TCMT IO Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew1)
        Elims
es2 <- Substitution -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub2 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> TCMT IO Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew2)

        -- Make sure we are comparing eliminations with the same arity
        -- (see #3810).
        let n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es1) (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es2)
            (Elims
es1' , Elims
es1r) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es1
            (Elims
es2' , Elims
es2r) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es2

            lhs1 :: Term
lhs1 = Elims -> Term
hd (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es1' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es2r
            lhs2 :: Term
lhs2 = Elims -> Term
hd (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es2' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1r

            -- Use type of rewrite rule with the most eliminations
            a :: Type
a | Elims -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Elims
es1r = Type
a2
              | Bool
otherwise = Type
a1

        VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"Considering potential critical pair at top-level: "
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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 -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term
lhs1, TCM Doc
" =?= "
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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 -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term
lhs2 , TCM Doc
" : " , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
a
          ]

        Maybe (Term, Term)
maybeCriticalPair <- Term -> Term -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 (TCM (Term, Term) -> TCM (Maybe (Term, Term)))
-> TCM (Term, Term) -> TCM (Maybe (Term, Term))
forall a b. (a -> b) -> a -> b
$ do
          -- Unify the left-hand sides of both rewrite rules
          Type
fa   <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          [Polarity]
fpol <- Comparison -> QName -> TCMT IO [Polarity]
forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
f
          TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
fpol [] Type
fa (Elims -> Term
hd []) Elims
es1' Elims
es2'

          -- Get the rhs of both rewrite rules (after unification). In
          -- case of different arities, add additional arguments from
          -- one side to the other side.
          let rhs1 :: Term
rhs1 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (RewriteRule -> Term
rewRHS RewriteRule
rew1) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2r
              rhs2 :: Term
rhs2 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r

          (Term, Term) -> TCM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
rhs1 , Term
rhs2)

        Maybe (Term, Term) -> ((Term, Term) -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Term, Term)
maybeCriticalPair (((Term, Term) -> TCM ()) -> TCM ())
-> ((Term, Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
rhs1 , Term
rhs2) ->
          Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hd (Elims
es1' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es2r) Term
rhs1 Term
rhs2

    -- Check confluence between two rules that overlap at a subpattern,
    -- e.g. @f ps[g qs] --> a@ and @g qs' --> b@.
    checkConfluenceSub :: (Elims -> Term) -> (Elims -> Term) -> RewriteRule -> RewriteRule -> OneHole Elims -> TCM ()
    checkConfluenceSub :: (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew1 RewriteRule
rew2 OneHole Elims
hole0 =
      Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        Substitution
sub1 <- Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew1

        let f :: QName
f          = RewriteRule -> QName
rewHead RewriteRule
rew1
            bvTel0 :: Telescope
bvTel0     = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole0
            k :: Int
k          = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
bvTel0
            b0 :: Type
b0         = Substitution -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
k Substitution
sub1) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Type
forall a. OneHole a -> Type
ohType OneHole Elims
hole0
            (QName
g,Elims -> Term
_,Elims
es0)  = (QName, Elims -> Term, Elims)
-> Maybe (QName, Elims -> Term, Elims)
-> (QName, Elims -> Term, Elims)
forall a. a -> Maybe a -> a
fromMaybe (QName, Elims -> Term, Elims)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Elims -> Term, Elims)
 -> (QName, Elims -> Term, Elims))
-> Maybe (QName, Elims -> Term, Elims)
-> (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe (QName, Elims -> Term, Elims)
headView (Term -> Maybe (QName, Elims -> Term, Elims))
-> Term -> Maybe (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$
                           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 Int
k Substitution
sub1) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Term
forall a. OneHole a -> Term
ohContents OneHole Elims
hole0
            qs2 :: PElims
qs2        = RewriteRule -> PElims
rewPats RewriteRule
rew2

        -- If the second rewrite rule has more eliminations than the
        -- subpattern of the first rule, the only chance of overlap is
        -- by eta-expanding the subpattern of the first rule.
        OneHole Term
hole1 <- Telescope -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel0 (TCMT IO (OneHole Term) -> TCMT IO (OneHole Term))
-> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall a b. (a -> b) -> a -> b
$
          Type -> Term -> PElims -> TCMT IO (OneHole Term)
forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
b0 (Elims -> Term
hdg Elims
es0) (PElims -> TCMT IO (OneHole Term))
-> PElims -> TCMT IO (OneHole Term)
forall a b. (a -> b) -> a -> b
$ Int -> PElims -> PElims
forall a. Int -> [a] -> [a]
drop (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es0) PElims
qs2

        VerboseKey -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> m () -> m ()
verboseS VerboseKey
"rewriting.confluence.eta" Int
30 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PElims -> Int
forall a. Sized a => a -> Int
size PElims
qs2) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel0 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ TCM Doc
"forceEtaExpansion result:"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ 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 (OneHole Term -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Term
hole1)
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"hole contents: " 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 (OneHole Term -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Term
hole1) (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ OneHole Term -> Term
forall a. OneHole a -> Term
ohContents OneHole Term
hole1)
            ]

        let hole :: OneHole Elims
hole      = OneHole Term
hole1 OneHole Term -> OneHole Elims -> OneHole Elims
forall a. OneHole Term -> OneHole a -> OneHole a
`composeHole` OneHole Elims
hole0
            (QName
g,Elims -> Term
_,Elims
es') = (QName, Elims -> Term, Elims)
-> Maybe (QName, Elims -> Term, Elims)
-> (QName, Elims -> Term, Elims)
forall a. a -> Maybe a -> a
fromMaybe (QName, Elims -> Term, Elims)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Elims -> Term, Elims)
 -> (QName, Elims -> Term, Elims))
-> Maybe (QName, Elims -> Term, Elims)
-> (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe (QName, Elims -> Term, Elims)
headView (Term -> Maybe (QName, Elims -> Term, Elims))
-> Term -> Maybe (QName, Elims -> Term, Elims)
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Term
forall a. OneHole a -> Term
ohContents OneHole Elims
hole -- g == rewHead rew2
            bvTel :: Telescope
bvTel     = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole
            plug :: Term -> Elims
plug      = OneHole Elims -> Term -> Elims
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Elims
hole

        Substitution
sub2 <- Telescope -> TCMT IO Substitution -> TCMT IO Substitution
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel (TCMT IO Substitution -> TCMT IO Substitution)
-> TCMT IO Substitution -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew2

        let es1 :: Elims
es1 = Substitution -> Elims -> Elims
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
bvTel) Substitution
sub1) Elims
es'
        Elims
es2 <- Substitution -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub2 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> TCMT IO Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew2)

        -- Make sure we are comparing eliminations with the same arity
        -- (see #3810). Because we forced eta-expansion of es1, we
        -- know that it is at least as long as es2.
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Elims -> Int
forall a. Sized a => a -> Int
size Elims
es2) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        let n :: Int
n = Elims -> Int
forall a. Sized a => a -> Int
size Elims
es2
            (Elims
es1' , Elims
es1r) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es1

        let lhs1 :: Term
lhs1 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg Elims
es1
            lhs2 :: Term
lhs2 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es2 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1r
            a :: Type
a    = Substitution -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew1

        VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"Considering potential critical pair at subpattern: "
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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 -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term
lhs1 , TCM Doc
" =?= "
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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 -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term
lhs2 , TCM Doc
" : " , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
a
          ]

        Maybe (Term, Term)
maybeCriticalPair <- Term -> Term -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 (TCM (Term, Term) -> TCM (Maybe (Term, Term)))
-> TCM (Term, Term) -> TCM (Maybe (Term, Term))
forall a b. (a -> b) -> a -> b
$ do
          -- Unify the subpattern of the first rewrite rule with the lhs
          -- of the second one
          Type
ga   <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
g
          [Polarity]
gpol <- Comparison -> QName -> TCMT IO [Polarity]
forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
g
          TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
gpol [] Type
ga (Elims -> Term
hdg []) Elims
es1' Elims
es2

          -- Right-hand side of first rewrite rule (after unification)
          let rhs1 :: Term
rhs1 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Term
rewRHS RewriteRule
rew1

          -- Left-hand side of first rewrite rule, with subpattern
          -- rewritten by the second rewrite rule
          let w :: Term
w = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r
          VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ TCM Doc
"Plugging hole with w = "
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
bvTel (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
w
            ]
          let rhs2 :: Term
rhs2 = Substitution -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug Term
w

          (Term, Term) -> TCM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
rhs1 , Term
rhs2)

        Maybe (Term, Term) -> ((Term, Term) -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Term, Term)
maybeCriticalPair (((Term, Term) -> TCM ()) -> TCM ())
-> ((Term, Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
rhs1 , Term
rhs2) ->
          Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hdf (Substitution -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub1 (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg Elims
es1) Term
rhs1 Term
rhs2

    headView :: Term -> Maybe (QName, Elims -> Term, Elims)
    headView :: Term -> Maybe (QName, Elims -> Term, Elims)
headView (Def QName
f Elims
es) = (QName, Elims -> Term, Elims)
-> Maybe (QName, Elims -> Term, Elims)
forall a. a -> Maybe a
Just (QName
f , QName -> Elims -> Term
Def QName
f , Elims
es)
    headView (Con ConHead
c ConInfo
ci Elims
es) = (QName, Elims -> Term, Elims)
-> Maybe (QName, Elims -> Term, Elims)
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
c , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci , Elims
es)
    headView Term
_ = Maybe (QName, Elims -> Term, Elims)
forall a. Maybe a
Nothing

    makeHead :: Definition -> Type -> TCM (Type , Elims -> Term)
    makeHead :: Definition -> Type -> TCMT IO (Type, Elims -> Term)
makeHead Definition
def Type
a = case Definition -> Defn
theDef Definition
def of
      Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
ch } -> do
        Type
ca <- ((QName, Type, Args), Type) -> Type
forall a b. (a, b) -> b
snd (((QName, Type, Args), Type) -> Type)
-> (Maybe ((QName, Type, Args), Type)
    -> ((QName, Type, Args), Type))
-> Maybe ((QName, Type, Args), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
forall a. a -> Maybe a -> a
fromMaybe ((QName, Type, Args), Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
-> TCMT IO (Maybe ((QName, Type, Args), Type)) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
ch Type
a
        (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ca , ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ConOSystem)
      -- For record projections @f : R Δ → A@, we rely on the invariant
      -- that any clause is fully general in the parameters, i.e. it
      -- is quantified over the parameter telescope @Δ@
      Function { funProjection :: Defn -> Maybe Projection
funProjection = Just Projection
proj } -> do
        let f :: QName
f          = Projection -> QName
projOrig Projection
proj
            r :: QName
r          = Arg QName -> QName
forall e. Arg e -> e
unArg (Arg QName -> QName) -> Arg QName -> QName
forall a b. (a -> b) -> a -> b
$ Projection -> Arg QName
projFromType Projection
proj
        Type
rtype <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
        TelV Telescope
ptel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
rtype
        Int
n <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
        let pars :: Args
            pars :: Args
pars = Int -> Args -> Args
forall t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ptel) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
ptel
        Type
ftype <- Definition -> Type
defType Definition
def Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Args
pars
        (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ftype , QName -> Elims -> Term
Def QName
f)
      Defn
_ -> (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> Type
defType Definition
def , QName -> Elims -> Term
Def (QName -> Elims -> Term) -> QName -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)

    getClausesAndRewriteRulesFor :: QName -> TCM [RewriteRule]
    getClausesAndRewriteRulesFor :: QName -> TCMT IO [RewriteRule]
getClausesAndRewriteRulesFor QName
f =
      [RewriteRule] -> [RewriteRule] -> [RewriteRule]
forall a. [a] -> [a] -> [a]
(++) ([RewriteRule] -> [RewriteRule] -> [RewriteRule])
-> TCMT IO [RewriteRule]
-> TCMT IO ([RewriteRule] -> [RewriteRule])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [RewriteRule]
getClausesAsRewriteRules QName
f TCMT IO ([RewriteRule] -> [RewriteRule])
-> TCMT IO [RewriteRule] -> TCMT IO [RewriteRule]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> TCMT IO [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f

    getRulesFor :: QName -> Bool -> TCM [RewriteRule]
    getRulesFor :: QName -> Bool -> TCMT IO [RewriteRule]
getRulesFor QName
f Bool
isClause
      | Bool
isClause  = QName -> TCMT IO [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
      | Bool
otherwise = QName -> TCMT IO [RewriteRule]
getClausesAndRewriteRulesFor QName
f

    -- Build a substitution that replaces all variables in the given
    -- telescope by fresh metavariables.
    makeMetaSubst :: (MonadMetaSolver m) => Telescope -> m Substitution
    makeMetaSubst :: Telescope -> m Substitution
makeMetaSubst Telescope
gamma = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution)
-> (Args -> [Term]) -> Args -> Substitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> (Args -> [Term]) -> Args -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> Substitution) -> m Args -> m Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Args
forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
newTelMeta Telescope
gamma

    -- Try to run the TCM action, return @Just x@ if it succeeds with
    -- result @x@ or @Nothing@ if it throws a type error. Abort if
    -- there are any constraints.
    tryUnification :: Term -> Term -> TCM a -> TCM (Maybe a)
    tryUnification :: Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 TCM a
f = (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> TCM a -> TCM (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f)
      TCM (Maybe a) -> (TCErr -> TCM (Maybe a)) -> TCM (Maybe a)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
        err :: TCErr
err@TypeError{} -> do
          VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ TCM Doc
"Unification failed with error: "
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err
            ]
          Maybe a -> TCM (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        TCErr
err -> TCErr -> TCM (Maybe a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
      TCM (Maybe a)
-> (Maybe a -> TCM (Maybe a))
-> (ProblemId -> Maybe a -> TCM (Maybe a))
-> TCM (Maybe a)
forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
`ifNoConstraints` Maybe a -> TCM (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ProblemId -> Maybe a -> TCM (Maybe a)) -> TCM (Maybe a))
-> (ProblemId -> Maybe a -> TCM (Maybe a)) -> TCM (Maybe a)
forall a b. (a -> b) -> a -> b
$ \ProblemId
pid Maybe a
_ -> do
        Constraints
cs <- ProblemId -> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
        [Doc]
prettyCs <- Constraints -> TCMT IO [Doc]
forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
        Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Doc] -> Warning
RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
prettyCs
        Maybe a -> TCM (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

    checkCriticalPair
      :: Type     -- Type of the critical pair
      -> (Elims -> Term)  -- Head of lhs
      -> Elims            -- Eliminations of lhs
      -> Term     -- First reduct
      -> Term     -- Second reduct
      -> TCM ()
    checkCriticalPair :: Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hd Elims
es Term
rhs1 Term
rhs2 = do

      (Type
a,Elims
es,Term
rhs1,Term
rhs2) <- (Type, Elims, Term, Term) -> TCMT IO (Type, Elims, Term, Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type
a,Elims
es,Term
rhs1,Term
rhs2)

      let ms :: [MetaId]
ms = Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Type, Elims, Term, Term) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton ((Type, Elims, Term, Term) -> Set MetaId)
-> (Type, Elims, Term, Term) -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (Type
a,Elims
es,Term
rhs1,Term
rhs2)

      VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ TCM Doc
"Abstracting over metas: "
        , [TCM Doc] -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((MetaId -> TCM Doc) -> [MetaId] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (MetaId -> VerboseKey) -> MetaId -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> VerboseKey
forall a. Show a => a -> VerboseKey
show) [MetaId]
ms)
        ]
      (Telescope
gamma , (Type
a,Elims
es,Term
rhs1,Term
rhs2)) <- (Telescope, (Type, Elims, Term, Term))
-> Maybe (Telescope, (Type, Elims, Term, Term))
-> (Telescope, (Type, Elims, Term, Term))
forall a. a -> Maybe a -> a
fromMaybe (Telescope, (Type, Elims, Term, Term))
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Telescope, (Type, Elims, Term, Term))
 -> (Telescope, (Type, Elims, Term, Term)))
-> TCMT IO (Maybe (Telescope, (Type, Elims, Term, Term)))
-> TCMT IO (Telescope, (Type, Elims, Term, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        [MetaId]
-> (Type, Elims, Term, Term)
-> TCMT IO (Maybe (Telescope, (Type, Elims, Term, Term)))
forall a.
MetasToVars a =>
[MetaId] -> a -> TCM (Maybe (Telescope, a))
abstractOverMetas [MetaId]
ms (Type
a,Elims
es,Term
rhs1,Term
rhs2)

      Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ TCM Doc
"Found critical pair: " , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
rhs1
        , TCM Doc
" =?= " , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
rhs2
        , TCM Doc
" : " , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (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
a ]

      Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
rhs1 Term
rhs2
        TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
          TypeError TCState
s Closure TypeError
err -> do
            Doc
prettyErr <- (TCState -> TCState) -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure TypeError
err
            Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Doc -> Warning
RewriteNonConfluent (Elims -> Term
hd Elims
es) Term
rhs1 Term
rhs2 Doc
prettyErr
          TCErr
err           -> TCErr -> TCM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

-- | Given metavariables ms and some x, construct a telescope Γ and
--   replace all occurrences of the given metavariables in @x@ by
--   normal variables from Γ. Returns @Nothing@ if metas have cyclic
--   dependencies.
abstractOverMetas :: (MetasToVars a) => [MetaId] -> a -> TCM (Maybe (Telescope, a))
abstractOverMetas :: [MetaId] -> a -> TCM (Maybe (Telescope, a))
abstractOverMetas [MetaId]
ms a
x = do

  -- Sort metas in dependency order
  TCMT IO (Maybe [MetaId])
-> ([MetaId] -> TCMT IO (Telescope, a))
-> TCM (Maybe (Telescope, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM ([MetaId] -> TCMT IO (Maybe [MetaId])
dependencySortMetas [MetaId]
ms) (([MetaId] -> TCMT IO (Telescope, a))
 -> TCM (Maybe (Telescope, a)))
-> ([MetaId] -> TCMT IO (Telescope, a))
-> TCM (Maybe (Telescope, a))
forall a b. (a -> b) -> a -> b
$ \[MetaId]
ms' -> do

    -- Get types and suggested names of metas
    [Type]
as <- [MetaId] -> (MetaId -> TCMT IO Type) -> TCMT IO [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
ms' MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType
    [VerboseKey]
ns <- [MetaId] -> (MetaId -> TCMT IO VerboseKey) -> TCMT IO [VerboseKey]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
ms' MetaId -> TCMT IO VerboseKey
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m VerboseKey
getMetaNameSuggestion

    -- Construct telescope (still containing the metas)
    let gamma :: Telescope
gamma = [VerboseKey] -> [Dom Type] -> Telescope
unflattenTel [VerboseKey]
ns ([Dom Type] -> Telescope) -> [Dom Type] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Type -> Dom Type) -> [Type] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Dom Type
forall a. a -> Dom a
defaultDom [Type]
as

    -- Replace metas by variables
    let n :: Int
n           = [MetaId] -> Int
forall a. Sized a => a -> Int
size [MetaId]
ms'
        metaIndex :: MetaId -> Maybe Int
metaIndex MetaId
x = (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> [MetaId] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex MetaId
x [MetaId]
ms'
    ReaderT (MetaId -> Maybe Int) (TCMT IO) (Telescope, a)
-> (MetaId -> Maybe Int) -> TCMT IO (Telescope, a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ((Telescope, a)
-> ReaderT (MetaId -> Maybe Int) (TCMT IO) (Telescope, a)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars (Telescope
gamma, a
x)) MetaId -> Maybe Int
metaIndex

-- ^ A @OneHole p@ is a @p@ with a subpattern @f ps@ singled out.
data OneHole a = OneHole
  { OneHole a -> Telescope
ohBoundVars :: Telescope     -- Telescope of bound variables at the hole
  , OneHole a -> Type
ohType      :: Type          -- Type of the term in the hole
  , OneHole a -> Term -> a
ohPlugHole  :: Term -> a     -- Plug the hole with some term
  , OneHole a -> Term
ohContents  :: Term          -- The term in the hole
  } deriving (a -> OneHole b -> OneHole a
(a -> b) -> OneHole a -> OneHole b
(forall a b. (a -> b) -> OneHole a -> OneHole b)
-> (forall a b. a -> OneHole b -> OneHole a) -> Functor OneHole
forall a b. a -> OneHole b -> OneHole a
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> OneHole b -> OneHole a
$c<$ :: forall a b. a -> OneHole b -> OneHole a
fmap :: (a -> b) -> OneHole a -> OneHole b
$cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
Functor)

-- | The trivial hole
idHole :: Type -> Term -> OneHole Term
idHole :: Type -> Term -> OneHole Term
idHole Type
a Term
v = Telescope -> Type -> (Term -> Term) -> Term -> OneHole Term
forall a. Telescope -> Type -> (Term -> a) -> Term -> OneHole a
OneHole Telescope
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id Term
v

-- | Plug a hole with another hole
composeHole :: OneHole Term -> OneHole a -> OneHole a
composeHole :: OneHole Term -> OneHole a -> OneHole a
composeHole OneHole Term
inner OneHole a
outer = OneHole :: forall a. Telescope -> Type -> (Term -> a) -> Term -> OneHole a
OneHole
  { ohBoundVars :: Telescope
ohBoundVars = OneHole a -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole a
outer Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` OneHole Term -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Term
inner
  , ohType :: Type
ohType      = OneHole Term -> Type
forall a. OneHole a -> Type
ohType OneHole Term
inner
  , ohPlugHole :: Term -> a
ohPlugHole  = OneHole a -> Term -> a
forall a. OneHole a -> Term -> a
ohPlugHole OneHole a
outer (Term -> a) -> (Term -> Term) -> Term -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneHole Term -> Term -> Term
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Term
inner
  , ohContents :: Term
ohContents  = OneHole Term -> Term
forall a. OneHole a -> Term
ohContents OneHole Term
inner
  }

ohAddBV :: ArgName -> Dom Type -> OneHole a -> OneHole a
ohAddBV :: VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV VerboseKey
x Dom Type
a OneHole a
oh = OneHole a
oh { ohBoundVars :: Telescope
ohBoundVars = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
x (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ OneHole a -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole a
oh }

-- ^ Given a @p : a@, @allHoles p@ lists all the possible
--   decompositions @p = p'[(f ps)/x]@.
class (Subst Term p , Free p) => AllHoles p where
  type PType p
  allHoles :: (Alternative m , MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m)
           => PType p -> p -> m (OneHole p)

allHoles_
  :: ( Alternative m , MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m, MonadDebug m
     , AllHoles p , PType p ~ () )
  => p -> m (OneHole p)
allHoles_ :: p -> m (OneHole p)
allHoles_ = PType p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles ()

allHolesList
  :: ( MonadReduce m, MonadAddContext m, HasBuiltins m, HasConstInfo m , AllHoles p)
  => PType p -> p -> m [OneHole p]
allHolesList :: PType p -> p -> m [OneHole p]
allHolesList PType p
a = ListT m (OneHole p) -> m [OneHole p]
forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT (ListT m (OneHole p) -> m [OneHole p])
-> (p -> ListT m (OneHole p)) -> p -> m [OneHole p]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PType p -> p -> ListT m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles PType p
a

-- | Given a term @v : a@ and eliminations @es@, force eta-expansion
--   of @v@ to match the structure (Apply/Proj) of the eliminations.
--
--   Examples:
--
--   1. @v : _A@ and @es = [$ w]@: this will instantiate
--      @_A := (x : _A1) → _A2@ and return the @OneHole Term@
--      @λ x → [v x]@.
--
--   2. @v : _A@ and @es = [.fst]@: this will instantiate
--      @_A := _A1 × _A2@ and return the @OneHole Term@
--      @([v .fst]) , (v .snd)@.
forceEtaExpansion :: Type -> Term -> [Elim' a] -> TCM (OneHole Term)
forceEtaExpansion :: Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
a Term
v [] = OneHole Term -> TCMT IO (OneHole Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (OneHole Term -> TCMT IO (OneHole Term))
-> OneHole Term -> TCMT IO (OneHole Term)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> OneHole Term
idHole Type
a Term
v
forceEtaExpansion Type
a Term
v (Elim' a
e:[Elim' a]
es) = case Elim' a
e of

  Apply (Arg ArgInfo
i a
w) -> do

    -- Force a to be a pi type
    VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
      [ TCM Doc
"Forcing" , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v , TCM Doc
":" , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a , TCM Doc
"to take one more argument" ]
    Dom Type
dom <- ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
i (Type -> Dom Type) -> TCMT IO Type -> TCMT IO (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Type
newTypeMeta_
    Type
cod <- Dom Type -> TCMT IO Type -> TCMT IO Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
dom (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Type
newTypeMeta_
    Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a (Type -> TCM ()) -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ Dom (VerboseKey, Type) -> Type -> Type
mkPi ((VerboseKey
"x",) (Type -> (VerboseKey, Type)) -> Dom Type -> Dom (VerboseKey, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) Type
cod

    -- Construct body of eta-expansion
    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 (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]

    -- Continue with remaining eliminations
    Dom Type -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
dom (TCMT IO (OneHole Term) -> TCMT IO (OneHole Term))
-> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Dom Type -> OneHole Term -> OneHole Term
forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV VerboseKey
"x" Dom Type
dom (OneHole Term -> OneHole Term)
-> (OneHole Term -> OneHole Term) -> OneHole Term -> OneHole Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term) -> OneHole Term -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Term -> Abs Term
forall t a. (Subst t a, Free a) => VerboseKey -> a -> Abs a
mkAbs VerboseKey
"x") (OneHole Term -> OneHole Term)
-> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
cod Term
body [Elim' a]
es

  Proj ProjOrigin
o QName
f -> do

    -- Force a to be the right record type for projection by f
    VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
      [ TCM Doc
"Forcing" , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v , TCM Doc
":" , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a , TCM Doc
"to be projectible by" , QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f ]
    QName
r <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe QName)
getRecordOfField QName
f
    Definition
rdef <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
    let ra :: Type
ra = Definition -> Type
defType Definition
rdef
    Args
pars <- Type -> TCMT IO Args
forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta Type
ra
    Sort
s <- Type
ra Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Args
pars TCMT IO Type -> (Type -> TCMT IO Sort) -> TCMT IO Sort
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
s -> Type -> (Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
s Sort -> TCMT IO Sort
forall (m :: * -> *) a. Monad m => a -> m a
return TCMT IO Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
    Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a (Type -> TCM ()) -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
pars)

    -- Eta-expand v at record type r, and get field corresponding to f
    (Telescope
_ , ConHead
c , ConInfo
ci , Args
fields) <- QName
-> Args
-> Defn
-> Term
-> TCMT IO (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
r Args
pars (Definition -> Defn
theDef Definition
rdef) Term
v
    let fs :: [Arg QName]
fs        = (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 -> [Dom' Term QName]) -> Defn -> [Dom' Term QName]
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
rdef
        i :: Int
i         = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex QName
f ([QName] -> Maybe Int) -> [QName] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Arg QName -> QName) -> [Arg QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Arg QName -> QName
forall e. Arg e -> e
unArg [Arg QName]
fs
        fContent :: Term
fContent  = Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term) -> Maybe (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Args
fields Args -> Int -> Maybe (Arg Term)
forall a. [a] -> Int -> Maybe a
!!! Int
i
        fUpdate :: Term -> Term
fUpdate Term
w = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> (Arg Term -> Arg Term) -> Args -> Args
forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
i (Term
w Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Args
fields

    -- Get type of field corresponding to f
    ~(Just (El Sort
_ (Pi Dom Type
b Abs Type
c))) <- QName -> Type -> TCMT IO (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> TCMT IO (Maybe Type))
-> TCMT IO Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
    let fa :: Type
fa = Abs Type
c Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
v

    -- Continue with remaining eliminations
    (Term -> Term) -> OneHole Term -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
fUpdate (OneHole Term -> OneHole Term)
-> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
fa Term
fContent [Elim' a]
es

  IApply{} -> TCMT IO (OneHole Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Not yet implemented

-- ^ Instances for @AllHoles@

instance AllHoles p => AllHoles (Arg p) where
  type PType (Arg p) = Dom (PType p)
  allHoles :: PType (Arg p) -> Arg p -> m (OneHole (Arg p))
allHoles PType (Arg p)
a Arg p
x = (p -> Arg p) -> OneHole p -> OneHole (Arg p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg p
x Arg p -> p -> Arg p
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (OneHole p -> OneHole (Arg p))
-> m (OneHole p) -> m (OneHole (Arg p))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Dom' Term (PType p) -> PType p
forall t e. Dom' t e -> e
unDom Dom' Term (PType p)
PType (Arg p)
a) (Arg p -> p
forall e. Arg e -> e
unArg Arg p
x)

instance AllHoles p => AllHoles (Dom p) where
  type PType (Dom p) = PType p
  allHoles :: PType (Dom p) -> Dom p -> m (OneHole (Dom p))
allHoles PType (Dom p)
a Dom p
x = (p -> Dom p) -> OneHole p -> OneHole (Dom p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Dom p
x Dom p -> p -> Dom p
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (OneHole p -> OneHole (Dom p))
-> m (OneHole p) -> m (OneHole (Dom p))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles PType p
PType (Dom p)
a (Dom p -> p
forall t e. Dom' t e -> e
unDom Dom p
x)

instance AllHoles (Abs Term) where
  type PType (Abs Term) = (Dom Type , Abs Type)
  allHoles :: PType (Abs Term) -> Abs Term -> m (OneHole (Abs Term))
allHoles (dom , a) Abs Term
x = (VerboseKey, Dom Type)
-> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Term -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Term
x , Dom Type
dom) (m (OneHole (Abs Term)) -> m (OneHole (Abs Term)))
-> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
forall a b. (a -> b) -> a -> b
$
    VerboseKey -> Dom Type -> OneHole (Abs Term) -> OneHole (Abs Term)
forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) Dom Type
dom (OneHole (Abs Term) -> OneHole (Abs Term))
-> (OneHole Term -> OneHole (Abs Term))
-> OneHole Term
-> OneHole (Abs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Abs Term) -> OneHole Term -> OneHole (Abs Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Term -> Abs Term
forall t a. (Subst t a, Free a) => VerboseKey -> a -> Abs a
mkAbs (VerboseKey -> Term -> Abs Term) -> VerboseKey -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Abs Term -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Term
x) (OneHole Term -> OneHole (Abs Term))
-> m (OneHole Term) -> m (OneHole (Abs Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      PType Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
a) (Abs Term -> Term
forall t a. Subst t a => Abs a -> a
absBody Abs Term
x)

instance AllHoles (Abs Type) where
  type PType (Abs Type) = Dom Type
  allHoles :: PType (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
allHoles PType (Abs Type)
dom Abs Type
a = (VerboseKey, Dom Type)
-> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a , Dom Type
PType (Abs Type)
dom) (m (OneHole (Abs Type)) -> m (OneHole (Abs Type)))
-> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
forall a b. (a -> b) -> a -> b
$
    VerboseKey -> Dom Type -> OneHole (Abs Type) -> OneHole (Abs Type)
forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) Dom Type
PType (Abs Type)
dom (OneHole (Abs Type) -> OneHole (Abs Type))
-> (OneHole Type -> OneHole (Abs Type))
-> OneHole Type
-> OneHole (Abs Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Abs Type) -> OneHole Type -> OneHole (Abs Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Type -> Abs Type
forall t a. (Subst t a, Free a) => VerboseKey -> a -> Abs a
mkAbs (VerboseKey -> Type -> Abs Type) -> VerboseKey -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) (OneHole Type -> OneHole (Abs Type))
-> m (OneHole Type) -> m (OneHole (Abs Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      Type -> m (OneHole Type)
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
a)

instance AllHoles Elims where
  type PType Elims = (Type , Elims -> Term)
  allHoles :: PType Elims -> Elims -> m (OneHole Elims)
allHoles (a,hd) [] = m (OneHole Elims)
forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles (a,hd) (Elim' Term
e:Elims
es) = do
    VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.hole" Int
65 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
      [ TCM Doc
"Head symbol" , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) , TCM Doc
":" , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , TCM Doc
"is eliminated by" , Elim' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elim' Term
e
      ]
    case Elim' Term
e of
      Apply Arg Term
x -> do
        ~(Pi Dom Type
b Abs Type
c) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> m Type -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        let a' :: Type
a'  = Abs Type
c Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
            hd' :: Elims -> Term
hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term
eElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
        ((Arg Term -> Elims) -> OneHole (Arg Term) -> OneHole Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:Elims
es) (Elim' Term -> Elims)
-> (Arg Term -> Elim' Term) -> Arg Term -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply) (OneHole (Arg Term) -> OneHole Elims)
-> m (OneHole (Arg Term)) -> m (OneHole Elims)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType (Arg Term) -> Arg Term -> m (OneHole (Arg Term))
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles Dom Type
PType (Arg Term)
b Arg Term
x)
         m (OneHole Elims) -> m (OneHole Elims) -> m (OneHole Elims)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Elims -> Elims) -> OneHole Elims -> OneHole Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Elim' Term
eElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (OneHole Elims -> OneHole Elims)
-> m (OneHole Elims) -> m (OneHole Elims)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
a' , Elims -> Term
hd') Elims
es)
      Proj ProjOrigin
o QName
f -> do
        ~(Just (El Sort
_ (Pi Dom Type
b Abs Type
c))) <- QName -> Type -> m (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> m (Maybe Type)) -> m Type -> m (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        let a' :: Type
a' = Abs Type
c Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Elims -> Term
hd []
        Elims -> Term
hd' <- Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Term -> Elims -> Term) -> m Term -> m (Elims -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProjOrigin -> QName -> Arg Term -> m 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
b Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd [])
        (Elims -> Elims) -> OneHole Elims -> OneHole Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Elim' Term
eElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (OneHole Elims -> OneHole Elims)
-> m (OneHole Elims) -> m (OneHole Elims)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
a' , Elims -> Term
hd') Elims
es
      IApply Term
x Term
y Term
u -> m (OneHole Elims)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Not yet implemented

instance AllHoles Type where
  type PType Type = ()
  allHoles :: PType Type -> Type -> m (OneHole Type)
allHoles PType Type
_ (El Sort
s Term
a) = m (OneHole Type) -> m (OneHole Type)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (m (OneHole Type) -> m (OneHole Type))
-> m (OneHole Type) -> m (OneHole Type)
forall a b. (a -> b) -> a -> b
$
    (Term -> Type) -> OneHole Term -> OneHole Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s) (OneHole Term -> OneHole Type)
-> m (OneHole Term) -> m (OneHole Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Sort -> Type
sort Sort
s) Term
a

instance AllHoles Term where
  type PType Term = Type
  allHoles :: PType Term -> Term -> m (OneHole Term)
allHoles PType Term
a Term
u = do
    VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.hole" Int
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep
      [ TCM Doc
"Getting holes of term" , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u , TCM Doc
":" , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
PType Term
a ]
    case Term
u of
      Var Int
i Elims
es       -> do
        Type
ai <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
        (Elims -> Term) -> OneHole Elims -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Elims -> Term
Var Int
i) (OneHole Elims -> OneHole Term)
-> m (OneHole Elims) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
ai , Int -> Elims -> Term
Var Int
i) Elims
es
      Lam ArgInfo
i Abs Term
u        -> do
        ~(Pi Dom Type
b Abs Type
c) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> m Type -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
PType Term
a
        (Abs Term -> Term) -> OneHole (Abs Term) -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Abs Term -> Term
Lam ArgInfo
i) (OneHole (Abs Term) -> OneHole Term)
-> m (OneHole (Abs Term)) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType (Abs Term) -> Abs Term -> m (OneHole (Abs Term))
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Dom Type
b,Abs Type
c) Abs Term
u
      Lit Literal
l          -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a
empty
      v :: Term
v@(Def QName
f Elims
es)   -> do
        Type
fa <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
        OneHole Term -> m (OneHole Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term -> OneHole Term
idHole Type
PType Term
a Term
v)
         m (OneHole Term) -> m (OneHole Term) -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Elims -> Term) -> OneHole Elims -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Elims -> Term
Def QName
f) (OneHole Elims -> OneHole Term)
-> m (OneHole Elims) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
fa , QName -> Elims -> Term
Def QName
f) Elims
es)
      v :: Term
v@(Con ConHead
c ConInfo
ci Elims
es) -> do
        Type
ca <- ((QName, Type, Args), Type) -> Type
forall a b. (a, b) -> b
snd (((QName, Type, Args), Type) -> Type)
-> (Maybe ((QName, Type, Args), Type)
    -> ((QName, Type, Args), Type))
-> Maybe ((QName, Type, Args), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
forall a. a -> Maybe a -> a
fromMaybe ((QName, Type, Args), Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
-> m (Maybe ((QName, Type, Args), Type)) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          ConHead -> Type -> m (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 -> m (Maybe ((QName, Type, Args), Type)))
-> m Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
PType Term
a
        OneHole Term -> m (OneHole Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term -> OneHole Term
idHole Type
PType Term
a Term
v)
         m (OneHole Term) -> m (OneHole Term) -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Elims -> Term) -> OneHole Elims -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) (OneHole Elims -> OneHole Term)
-> m (OneHole Elims) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
ca , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
es)
      Pi Dom Type
a Abs Type
b         ->
        ((Dom Type -> Term) -> OneHole (Dom Type) -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Dom Type
a -> Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b) (OneHole (Dom Type) -> OneHole Term)
-> m (OneHole (Dom Type)) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (OneHole (Dom Type))
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Dom Type
a) m (OneHole Term) -> m (OneHole Term) -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        ((Abs Type -> Term) -> OneHole (Abs Type) -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Abs Type
b -> Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b) (OneHole (Abs Type) -> OneHole Term)
-> m (OneHole (Abs Type)) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles Dom Type
PType (Abs Type)
a Abs Type
b)
      Sort Sort
s         -> (Sort -> Term) -> OneHole Sort -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort (OneHole Sort -> OneHole Term)
-> m (OneHole Sort) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (OneHole Sort)
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Sort
s
      Level Level
l        -> (Level -> Term) -> OneHole Level -> OneHole Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Term
Level (OneHole Level -> OneHole Term)
-> m (OneHole Level) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (OneHole Level)
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
      MetaV{}        -> m (OneHole Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
      DontCare{}     -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a
empty
      Dummy{}        -> m (OneHole Term)
forall (f :: * -> *) a. Alternative f => f a
empty

instance AllHoles Sort where
  type PType Sort = ()
  allHoles :: PType Sort -> Sort -> m (OneHole Sort)
allHoles PType Sort
_ = \case
    Type Level
l       -> (Level -> Sort) -> OneHole Level -> OneHole Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Sort
forall t. Level' t -> Sort' t
Type (OneHole Level -> OneHole Sort)
-> m (OneHole Level) -> m (OneHole Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (OneHole Level)
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
    Prop Level
l       -> (Level -> Sort) -> OneHole Level -> OneHole Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Sort
forall t. Level' t -> Sort' t
Prop (OneHole Level -> OneHole Sort)
-> m (OneHole Level) -> m (OneHole Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (OneHole Level)
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
    Sort
Inf          -> m (OneHole Sort)
forall (f :: * -> *) a. Alternative f => f a
empty
    Sort
SizeUniv     -> m (OneHole Sort)
forall (f :: * -> *) a. Alternative f => f a
empty
    PiSort{}     -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
    FunSort{}    -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
    UnivSort{}   -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaS{}      -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
    DefS QName
f Elims
es    -> do
      Type
fa <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      (Elims -> Sort) -> OneHole Elims -> OneHole Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f) (OneHole Elims -> OneHole Sort)
-> m (OneHole Elims) -> m (OneHole Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Elims -> Elims -> m (OneHole Elims)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles (Type
fa , QName -> Elims -> Term
Def QName
f) Elims
es
    DummyS{}     -> m (OneHole Sort)
forall (f :: * -> *) a. Alternative f => f a
empty

instance AllHoles Level where
  type PType Level = ()
  allHoles :: PType Level -> Level -> m (OneHole Level)
allHoles PType Level
_ (Max Integer
n [PlusLevel' Term]
ls) = ([PlusLevel' Term] -> Level)
-> OneHole [PlusLevel' Term] -> OneHole Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) (OneHole [PlusLevel' Term] -> OneHole Level)
-> m (OneHole [PlusLevel' Term]) -> m (OneHole Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ [PlusLevel' Term]
ls

instance AllHoles [PlusLevel] where
  type PType [PlusLevel] = ()
  allHoles :: PType [PlusLevel' Term]
-> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
allHoles PType [PlusLevel' Term]
_ []     = m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles PType [PlusLevel' Term]
_ (PlusLevel' Term
l:[PlusLevel' Term]
ls) =
    ((PlusLevel' Term -> [PlusLevel' Term])
-> OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:[PlusLevel' Term]
ls) (OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term])
-> m (OneHole (PlusLevel' Term)) -> m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ PlusLevel' Term
l)
    m (OneHole [PlusLevel' Term])
-> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (([PlusLevel' Term] -> [PlusLevel' Term])
-> OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlusLevel' Term
lPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:) (OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term])
-> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ [PlusLevel' Term]
ls)

instance AllHoles PlusLevel where
  type PType PlusLevel = ()
  allHoles :: PType (PlusLevel' Term)
-> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
allHoles PType (PlusLevel' Term)
_ (Plus Integer
n LevelAtom' Term
l) = (LevelAtom' Term -> PlusLevel' Term)
-> OneHole (LevelAtom' Term) -> OneHole (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
n) (OneHole (LevelAtom' Term) -> OneHole (PlusLevel' Term))
-> m (OneHole (LevelAtom' Term)) -> m (OneHole (PlusLevel' Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LevelAtom' Term -> m (OneHole (LevelAtom' Term))
forall (m :: * -> *) p.
(Alternative m, MonadReduce m, MonadAddContext m, HasBuiltins m,
 HasConstInfo m, MonadDebug m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ LevelAtom' Term
l

instance AllHoles LevelAtom where
  type PType LevelAtom = ()
  allHoles :: PType (LevelAtom' Term)
-> LevelAtom' Term -> m (OneHole (LevelAtom' Term))
allHoles PType (LevelAtom' Term)
_ LevelAtom' Term
l = do
    Type
la <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
    case LevelAtom' Term
l of
      MetaLevel{}      -> m (OneHole (LevelAtom' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
      BlockedLevel{}   -> m (OneHole (LevelAtom' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
      NeutralLevel NotBlocked
b Term
u -> (Term -> LevelAtom' Term)
-> OneHole Term -> OneHole (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
b) (OneHole Term -> OneHole (LevelAtom' Term))
-> m (OneHole Term) -> m (OneHole (LevelAtom' Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles Type
PType Term
la Term
u
      UnreducedLevel Term
u -> (Term -> LevelAtom' Term)
-> OneHole Term -> OneHole (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (OneHole Term -> OneHole (LevelAtom' Term))
-> m (OneHole Term) -> m (OneHole (LevelAtom' Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, MonadReduce m, MonadAddContext m,
 HasBuiltins m, HasConstInfo m) =>
PType p -> p -> m (OneHole p)
allHoles Type
PType Term
la Term
u


-- | Convert metavariables to normal variables. Warning: doesn't
--   convert sort metas.
class MetasToVars a where
  metasToVars
    :: (MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
    => a -> m a

  default metasToVars
    :: ( MetasToVars a', Traversable f, a ~ f a'
       , MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
    => a -> m a
  metasToVars = (a' -> m a') -> f a' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a' -> m a'
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars

instance MetasToVars a => MetasToVars [a] where
instance MetasToVars a => MetasToVars (Arg a) where
instance MetasToVars a => MetasToVars (Dom a) where
instance MetasToVars a => MetasToVars (Elim' a) where

instance MetasToVars a => MetasToVars (Abs a) where
  metasToVars :: Abs a -> m (Abs a)
metasToVars (Abs   VerboseKey
i a
x) = VerboseKey -> a -> Abs a
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
i   (a -> Abs a) -> m a -> m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((MetaId -> Maybe Int) -> MetaId -> Maybe Int) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Int
forall a. Enum a => a -> a
succ (Maybe Int -> Maybe Int)
-> (MetaId -> Maybe Int) -> MetaId -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x)
  metasToVars (NoAbs VerboseKey
i a
x) = VerboseKey -> a -> Abs a
forall a. VerboseKey -> a -> Abs a
NoAbs VerboseKey
i (a -> Abs a) -> m a -> m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x

instance MetasToVars Term where
  metasToVars :: Term -> m Term
metasToVars = \case
    Var Int
i Elims
es   -> Int -> Elims -> Term
Var Int
i    (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    Lam ArgInfo
i Abs Term
u    -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i    (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> m (Abs Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Term
u
    Lit Literal
l      -> Literal -> Term
Lit      (Literal -> Term) -> m Literal -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> m Literal
forall (f :: * -> *) a. Applicative f => a -> f a
pure Literal
l
    Def QName
f Elims
es   -> QName -> Elims -> Term
Def QName
f    (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    Con ConHead
c ConInfo
i Elims
es -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
i  (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
Pi       (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Type
b
    Sort Sort
s     -> Sort -> Term
Sort     (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s
    Level Level
l    -> Level -> Term
Level    (Level -> Term) -> m Level -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    MetaV MetaId
x Elims
es -> ((MetaId -> Maybe Int) -> MetaId -> Maybe Int
forall a b. (a -> b) -> a -> b
$ MetaId
x) ((MetaId -> Maybe Int) -> Maybe Int)
-> m (MetaId -> Maybe Int) -> m (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (MetaId -> Maybe Int)
forall r (m :: * -> *). MonadReader r m => m r
ask m (Maybe Int) -> (Maybe Int -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Int
i   -> Int -> Elims -> Term
Var Int
i    (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
      Maybe Int
Nothing  -> MetaId -> Elims -> Term
MetaV MetaId
x  (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DontCare Term
u -> Term -> Term
DontCare (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
u
    Dummy VerboseKey
s Elims
es -> VerboseKey -> Elims -> Term
Dummy VerboseKey
s  (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es

instance MetasToVars Type where
  metasToVars :: Type -> m Type
metasToVars (El Sort
s Term
t) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
t

instance MetasToVars Sort where
  metasToVars :: Sort -> m Sort
metasToVars = \case
    Type Level
l     -> Level -> Sort
forall t. Level' t -> Sort' t
Type     (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Prop Level
l     -> Level -> Sort
forall t. Level' t -> Sort' t
Prop     (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Sort
Inf        -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
Inf
    Sort
SizeUniv   -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
SizeUniv
    PiSort Dom Type
s Abs Sort
t -> Dom Type -> Abs Sort -> Sort
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort   (Dom Type -> Abs Sort -> Sort)
-> m (Dom Type) -> m (Abs Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Dom Type
s m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Sort -> m (Abs Sort)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Sort
t
    FunSort Sort
s Sort
t -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort) -> m Sort -> m (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s m (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
t
    UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s
    MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DefS QName
f Elims
es  -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f   (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DummyS VerboseKey
s   -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Sort
forall t. VerboseKey -> Sort' t
DummyS VerboseKey
s

instance MetasToVars Level where
  metasToVars :: Level -> m Level
metasToVars (Max Integer
n [PlusLevel' Term]
ls) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m [PlusLevel' Term]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars [PlusLevel' Term]
ls

instance MetasToVars PlusLevel where
  metasToVars :: PlusLevel' Term -> m (PlusLevel' Term)
metasToVars (Plus Integer
n LevelAtom' Term
x) = Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
n (LevelAtom' Term -> PlusLevel' Term)
-> m (LevelAtom' Term) -> m (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LevelAtom' Term -> m (LevelAtom' Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars LevelAtom' Term
x

instance MetasToVars LevelAtom where
  metasToVars :: LevelAtom' Term -> m (LevelAtom' Term)
metasToVars = \case
    MetaLevel MetaId
m Elims
es    -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
forall a. Monoid a => a
mempty (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars (MetaId -> Elims -> Term
MetaV MetaId
m Elims
es)
    BlockedLevel MetaId
_ Term
u  -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel      (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
u
    NeutralLevel NotBlocked
nb Term
u -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
nb     (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
u
    UnreducedLevel Term
u  -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel      (Term -> LevelAtom' Term) -> m Term -> m (LevelAtom' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
u

instance MetasToVars a => MetasToVars (Tele a) where
  metasToVars :: Tele a -> m (Tele a)
metasToVars Tele a
EmptyTel = Tele a -> m (Tele a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele a
forall a. Tele a
EmptyTel
  metasToVars (ExtendTel a
a Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (a -> Abs (Tele a) -> Tele a) -> m a -> m (Abs (Tele a) -> Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
a m (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs (Tele a) -> m (Abs (Tele a))
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs (Tele a)
tel

instance (MetasToVars a, MetasToVars b) => MetasToVars (a,b) where
  metasToVars :: (a, b) -> m (a, b)
metasToVars (a
x,b
y) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> (a, b)) -> m b -> m (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars b
y

instance (MetasToVars a, MetasToVars b, MetasToVars c) => MetasToVars (a,b,c) where
  metasToVars :: (a, b, c) -> m (a, b, c)
metasToVars (a
x,b
y,c
z) = (,,) (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> m c
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars c
z

instance (MetasToVars a, MetasToVars b, MetasToVars c, MetasToVars d) => MetasToVars (a,b,c,d) where
  metasToVars :: (a, b, c, d) -> m (a, b, c, d)
metasToVars (a
x,b
y,c
z,d
w) = (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> m a -> m (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> c -> d -> (a, b, c, d))
-> m b -> m (c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> m c
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> d -> m d
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
metasToVars d
w