{-# LANGUAGE NondecreasingIndentation #-}

-- | Checking local or global confluence of rewrite rules.
--
-- For checking LOCAL CONFLUENCE of a given rewrite rule @f ps ↦ v@,
-- we construct critical pairs involving this as the main rule by
-- searching for:
--
-- 1. *Different* rules @f ps' ↦ ...@ where @ps@ and @ps'@ can be
--    unified.
--
-- 2. Subpatterns @g qs@ of @ps@ and rewrite rules @g qs' ↦ ...@ where
--    @qs@ and @qs'@ can be unified.
--
-- Each of these leads to a *critical pair* @v₁ <-- f us --> v₂@, which
-- should satisfy @v₁ = v₂@.
--
-- For checking GLOBAL CONFLUENCE, we check the following two
-- properties:
--
-- 1. For any two left-hand sides of the rewrite rules that overlap
--    (either at the root position or at a subterm), the most general
--    unifier of the two left-hand sides is again a left-hand side of
--    a rewrite rule. For example, if there are two rules @suc m + n =
--    suc (m + n)@ and @m + suc n = suc (m + n)@, then there should
--    also be a rule @suc m + suc n = suc (suc (m + n))@.
--
-- 2. Each rewrite rule should satisfy the *triangle property*: For
--    any rewrite rule @u ↦ w@ and any single-step parallel unfolding
--    @u => v@, we should have another single-step parallel unfolding
--    @v => w@.


module Agda.TypeChecking.Rewriting.Confluence
  ( checkConfluenceOfRules
  , checkConfluenceOfClauses
  , sortRulesOfSymbol
  ) where

import Control.Applicative
import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Reader ( MonadReader(..), asks, runReaderT )

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

import Agda.Interaction.Options ( ConfluenceCheck(..) )

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

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

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (unlessNullM)
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple ((***))

-- | Check confluence of the clauses of the given function wrt rewrite rules of the
-- constructors they match against
checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses ConfluenceCheck
confChk QName
f = do
  rews <- QName -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getClausesAsRewriteRules QName
f
  let noMetasInPats GlobalRewriteRule
rew
        | [Elim' NLPat] -> Bool
forall a. AllMetas a => a -> Bool
noMetas (GlobalRewriteRule -> [Elim' NLPat]
grPats GlobalRewriteRule
rew) = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        | Bool
otherwise             = Bool
False Bool -> TCM () -> TCMT IO Bool
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Warning
ConfluenceCheckingIncompleteBecauseOfMeta QName
f
  rews <- filterM noMetasInPats rews
  let matchables = (GlobalRewriteRule -> [QName]) -> [GlobalRewriteRule] -> [[QName]]
forall a b. (a -> b) -> [a] -> [b]
map' GlobalRewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [GlobalRewriteRule]
rews
  reportSDoc "rewriting.confluence" 30 $
    "Function" <+> prettyTCM f <+> "has matchable symbols" <+> prettyList_ (map' prettyTCM matchables)
  modifySignature $ setMatchableSymbols f $ concat matchables

  let hasRules QName
g = Bool -> Bool
not (Bool -> Bool)
-> ([GlobalRewriteRule] -> Bool) -> [GlobalRewriteRule] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GlobalRewriteRule] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([GlobalRewriteRule] -> Bool) -> f [GlobalRewriteRule] -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f [GlobalRewriteRule]
forall (m :: * -> *).
HasConstInfo m =>
QName -> m [GlobalRewriteRule]
getGlobalRewriteRulesFor QName
g
  forM_ (zip' rews matchables) \(GlobalRewriteRule
rew,[QName]
ms) ->
    TCMT IO [QName] -> ([QName] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM ((QName -> TCMT IO Bool) -> [QName] -> TCMT IO [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM QName -> TCMT IO Bool
forall {f :: * -> *}. HasConstInfo f => QName -> f Bool
hasRules [QName]
ms) \[QName]
_ -> do
      ConfluenceCheck -> [GlobalRewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [GlobalRewriteRule
rew]

-- | Check confluence of the given rewrite rules wrt all other rewrite
--   rules (also amongst themselves).
checkConfluenceOfRules :: ConfluenceCheck -> [GlobalRewriteRule] -> TCM ()
checkConfluenceOfRules :: ConfluenceCheck -> [GlobalRewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [GlobalRewriteRule]
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

  -- Global confluence: we need to check the triangle property for each rewrite
  -- rule of each head symbol as well as rules that match on them
  Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ConfluenceCheck
confChk ConfluenceCheck -> ConfluenceCheck -> Bool
forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let getSymbols :: GlobalRewriteRule -> f (Set QName)
getSymbols GlobalRewriteRule
rew = let f :: QName
f = GlobalRewriteRule -> QName
grHead GlobalRewriteRule
rew in
         (QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
f) (Set QName -> Set QName)
-> (Definition -> Set QName) -> Definition -> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Set QName
defMatchable (Definition -> Set QName) -> f Definition -> f (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
    allSymbols <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Set QName -> [QName])
-> ([Set QName] -> Set QName) -> [Set QName] -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set QName] -> Set QName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set QName] -> [QName]) -> TCMT IO [Set QName] -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GlobalRewriteRule -> TCMT IO (Set QName))
-> [GlobalRewriteRule] -> TCMT IO [Set QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse GlobalRewriteRule -> TCMT IO (Set QName)
forall {f :: * -> *}.
HasConstInfo f =>
GlobalRewriteRule -> f (Set QName)
getSymbols [GlobalRewriteRule]
rews
    forM_ allSymbols $ \QName
f -> do
      rewsf <- QName -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getAllRulesFor QName
f
      forM_ rewsf $ \GlobalRewriteRule
rew -> do
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.triangle" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"(re)checking triangle property for rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew)
        GlobalRewriteRule -> TCM ()
checkTrianglePropertyForRule GlobalRewriteRule
rew

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

  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew)
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> GlobalRewriteRule -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => GlobalRewriteRule -> m Doc
prettyTCM GlobalRewriteRule
rew

  let f :: QName
f   = GlobalRewriteRule -> QName
grHead GlobalRewriteRule
rew
      qs :: [Elim' NLPat]
qs  = GlobalRewriteRule -> [Elim' NLPat]
grPats GlobalRewriteRule
rew
      tel :: Tele (Dom Type)
tel = GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
rew
  def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
  (fa , hdf) <- addContext tel $ makeHead def (grType rew)

  reportSDoc "rewriting.confluence" 30 $ addContext tel $
    "Head symbol" <+> prettyTCM (hdf []) <+> "of rewrite rule has type" <+> prettyTCM fa

  -- Step 1: check other rewrite rules that overlap at top position
  forMM_ (getAllRulesFor f) $ \ GlobalRewriteRule
rew' -> do
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((GlobalRewriteRule -> Bool) -> [GlobalRewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName GlobalRewriteRule
rew') (GlobalRewriteRule
rewGlobalRewriteRule -> [GlobalRewriteRule] -> [GlobalRewriteRule]
forall a. a -> [a] -> [a]
:[GlobalRewriteRule]
rewsRest) Bool -> Bool -> Bool
||
            (GlobalRewriteRule -> Bool
grFromClause GlobalRewriteRule
rew Bool -> Bool -> Bool
&& GlobalRewriteRule -> Bool
grFromClause GlobalRewriteRule
rew')) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      ([Elim] -> Term)
-> GlobalRewriteRule -> GlobalRewriteRule -> TCM ()
checkConfluenceTop [Elim] -> Term
hdf GlobalRewriteRule
rew GlobalRewriteRule
rew'
  reportSDoc "rewriting.confluence" 30 $
    "Finished step 1 of confluence check of rule" <+> prettyTCM (grName rew)

  -- Step 2: check other rewrite rules that overlap with a subpattern
  -- of this rewrite rule
  es <- nlPatToTerm qs
  forMM_ (addContext tel $ allHolesList (fa, hdf) es) $ \ OneHole [Elim]
hole -> do
    let g :: QName
g   = OneHole [Elim] -> QName
forall a. OneHole a -> QName
ohHeadName OneHole [Elim]
hole
        hdg :: [Elim] -> Term
hdg = OneHole [Elim] -> [Elim] -> Term
forall a. OneHole a -> [Elim] -> Term
ohHead OneHole [Elim]
hole
    VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Found hole with head symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
g
    rews' <- QName -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getAllRulesFor QName
g
    forM_ rews' $ \GlobalRewriteRule
rew' -> do
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((GlobalRewriteRule -> Bool) -> [GlobalRewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName GlobalRewriteRule
rew') [GlobalRewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        ([Elim] -> Term)
-> ([Elim] -> Term)
-> GlobalRewriteRule
-> GlobalRewriteRule
-> OneHole [Elim]
-> TCM ()
checkConfluenceSub [Elim] -> Term
hdf [Elim] -> Term
hdg GlobalRewriteRule
rew GlobalRewriteRule
rew' OneHole [Elim]
hole
  reportSDoc "rewriting.confluence" 30 $
    "Finished step 2 of confluence check of rule" <+> prettyTCM (grName rew)

  -- Step 3: check other rewrite rules that have a subpattern which
  -- overlaps with this rewrite rule
  forM_ (defMatchable def) $ \ QName
g -> do
    VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
g TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has rules that match on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
    TCMT IO [GlobalRewriteRule]
-> (GlobalRewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getAllRulesFor QName
g) ((GlobalRewriteRule -> TCM ()) -> TCM ())
-> (GlobalRewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ GlobalRewriteRule
rew' -> do
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((GlobalRewriteRule -> Bool) -> [GlobalRewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName GlobalRewriteRule
rew') [GlobalRewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        es' <- [Elim' NLPat] -> TCMT IO [Elim]
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m [Elim]
nlPatToTerm (GlobalRewriteRule -> [Elim' NLPat]
grPats GlobalRewriteRule
rew')
        let tel' = GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
rew'
        def' <- getConstInfo g
        (ga , hdg) <- addContext tel' $ makeHead def' (grType rew')
        forMM_ (addContext tel' $ allHolesList (ga , hdg) es') $ \ OneHole [Elim]
hole -> do
          let f' :: QName
f' = OneHole [Elim] -> QName
forall a. OneHole a -> QName
ohHeadName OneHole [Elim]
hole
          Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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
$ ([Elim] -> Term)
-> ([Elim] -> Term)
-> GlobalRewriteRule
-> GlobalRewriteRule
-> OneHole [Elim]
-> TCM ()
checkConfluenceSub [Elim] -> Term
hdg [Elim] -> Term
hdf GlobalRewriteRule
rew' GlobalRewriteRule
rew OneHole [Elim]
hole
  reportSDoc "rewriting.confluence" 30 $
    "Finished step 3 of confluence check of rule" <+> prettyTCM (grName rew)

  where

    -- Check confluence of two rewrite rules that have the same head symbol,
    -- e.g. @f ps --> a@ and @f ps' --> b@.
    checkConfluenceTop ::
      (Elims -> Term) -> GlobalRewriteRule -> GlobalRewriteRule -> TCM ()
    checkConfluenceTop :: ([Elim] -> Term)
-> GlobalRewriteRule -> GlobalRewriteRule -> TCM ()
checkConfluenceTop [Elim] -> Term
hd GlobalRewriteRule
rew1 GlobalRewriteRule
rew2 =
      Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew1) (GlobalRewriteRule -> QName
grName GlobalRewriteRule
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

        sub1 <- Tele (Dom Type) -> TCM Substitution
makeMetaSubst (Tele (Dom Type) -> TCM Substitution)
-> Tele (Dom Type) -> TCM Substitution
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
rew1
        sub2 <- makeMetaSubst $ grContext rew2

        let f    = GlobalRewriteRule -> QName
grHead GlobalRewriteRule
rew1 -- == grHead rew2
            a1   = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> Type
grType GlobalRewriteRule
rew1
            a2   = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> Type
grType GlobalRewriteRule
rew2

        es1 <- applySubst sub1 <$> nlPatToTerm (grPats rew1)
        es2 <- applySubst sub2 <$> nlPatToTerm (grPats rew2)

        reportSDoc "rewriting.confluence" 30 $ vcat
          [ "checkConfluenceTop" <+> prettyTCM (grName rew1) <+> prettyTCM (grName rew2)
          , "  f    = " <+> prettyTCM f
          , "  ctx1 = " <+> prettyTCM (grContext rew1)
          , "  ctx2 = " <+> prettyTCM (grContext rew2)
          , "  es1  = " <+> prettyTCM es1
          , "  es2  = " <+> prettyTCM es2
          ]

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

            lhs1 = [Elim] -> Term
hd ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim]
es1' [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
esr
            lhs2 = [Elim] -> Term
hd ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim]
es2' [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
esr

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

        reportSDoc "rewriting.confluence" 20 $ sep
          [ "Considering potential critical pair at top-level: "
          , nest 2 $ prettyTCM $ lhs1, " =?= "
          , nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
          ]

        maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
          -- Unify the left-hand sides of both rewrite rules
          fa   <- defType <$> getConstInfo f
          fpol <- getPolarity' CmpEq f
          onlyReduceTypes $
            compareElims fpol [] fa (hd []) es1' 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 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (GlobalRewriteRule -> Term
grRHS GlobalRewriteRule
rew1) Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es2r
              rhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub2 (GlobalRewriteRule -> Term
grRHS GlobalRewriteRule
rew2) Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es1r

          return (rhs1 , rhs2)

        whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hd (es1' ++! esr))

    -- 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)
      -> GlobalRewriteRule -> GlobalRewriteRule -> OneHole Elims -> TCM ()
    checkConfluenceSub :: ([Elim] -> Term)
-> ([Elim] -> Term)
-> GlobalRewriteRule
-> GlobalRewriteRule
-> OneHole [Elim]
-> TCM ()
checkConfluenceSub [Elim] -> Term
hdf [Elim] -> Term
hdg GlobalRewriteRule
rew1 GlobalRewriteRule
rew2 OneHole [Elim]
hole0 = do
      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"foo 2" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew2)
      Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew1) (GlobalRewriteRule -> QName
grName GlobalRewriteRule
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

        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Checking confluence of rules" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCMT IO Doc
"and" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (GlobalRewriteRule -> QName
grName GlobalRewriteRule
rew2) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"at subpattern position"

        sub1 <- Tele (Dom Type) -> TCM Substitution
makeMetaSubst (Tele (Dom Type) -> TCM Substitution)
-> Tele (Dom Type) -> TCM Substitution
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
rew1

        let bvTel0     = OneHole [Elim] -> Tele (Dom Type)
forall a. OneHole a -> Tele (Dom Type)
ohBoundVars OneHole [Elim]
hole0
            k          = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
bvTel0
            b0         = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> 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 [Elim] -> Type
forall a. OneHole a -> Type
ohType OneHole [Elim]
hole0
            g          = OneHole [Elim] -> QName
forall a. OneHole a -> QName
ohHeadName OneHole [Elim]
hole0
            es0        = Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
k Substitution
sub1) ([Elim] -> [Elim]) -> [Elim] -> [Elim]
forall a b. (a -> b) -> a -> b
$ OneHole [Elim] -> [Elim]
forall a. OneHole a -> [Elim]
ohElims OneHole [Elim]
hole0
            qs2        = GlobalRewriteRule -> [Elim' NLPat]
grPats GlobalRewriteRule
rew2

        -- TODO: support IApply in forceEtaExpansion
        let isIApply IApply{} = Bool
True
            isIApply Elim' a
_        = Bool
False
        unless (any isIApply $ drop (size es0) qs2) $ do

        -- 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.
        hole1 <- addContext bvTel0 $
          forceEtaExpansion b0 (hdg es0) $ drop (size es0) qs2

        verboseS "rewriting.confluence.eta" 30 $
          unless (size es0 == size qs2) $
          addContext bvTel0 $
          reportSDoc "rewriting.confluence.eta" 30 $ vcat
            [ "forceEtaExpansion result:"
            , nest 2 $ "bound vars: " <+> prettyTCM (ohBoundVars hole1)
            , nest 2 $ "hole contents: " <+> addContext (ohBoundVars hole1) (prettyTCM $ ohContents hole1)
            ]

        let hole      = OneHole Term
hole1 OneHole Term -> OneHole [Elim] -> OneHole [Elim]
forall a. OneHole Term -> OneHole a -> OneHole a
`composeHole` OneHole [Elim]
hole0
            g         = OneHole [Elim] -> QName
forall a. OneHole a -> QName
ohHeadName OneHole [Elim]
hole -- == grHead rew2
            es'       = OneHole [Elim] -> [Elim]
forall a. OneHole a -> [Elim]
ohElims OneHole [Elim]
hole
            bvTel     = OneHole [Elim] -> Tele (Dom Type)
forall a. OneHole a -> Tele (Dom Type)
ohBoundVars OneHole [Elim]
hole
            plug      = OneHole [Elim] -> Term -> [Elim]
forall a. OneHole a -> Term -> a
ohPlugHole OneHole [Elim]
hole

        sub2 <- addContext bvTel $ makeMetaSubst $ grContext rew2

        let es1 = Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
bvTel) Substitution
sub1) [Elim]
es'
        es2 <- applySubst sub2 <$> nlPatToTerm (grPats 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.
        when (size es1 < size es2) __IMPOSSIBLE__
        let n = [Elim] -> Int
forall a. Sized a => a -> Int
size [Elim]
es2
            (es1' , es1r) = splitAt n es1

        let lhs1 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
hdf ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Elim]
plug (Term -> [Elim]) -> Term -> [Elim]
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
hdg [Elim]
es1
            lhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
hdf ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Elim]
plug (Term -> [Elim]) -> Term -> [Elim]
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
hdg ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim]
es2 [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
es1r
            a    = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> Type
grType GlobalRewriteRule
rew1

        reportSDoc "rewriting.confluence" 20 $ sep
          [ "Considering potential critical pair at subpattern: "
          , nest 2 $ prettyTCM $ lhs1 , " =?= "
          , nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
          ]

        maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
          -- Unify the subpattern of the first rewrite rule with the lhs
          -- of the second one
          ga   <- defType <$> getConstInfo g
          gpol <- getPolarity' CmpEq g
          onlyReduceTypes $ addContext bvTel $
            compareElims gpol [] ga (hdg []) es1' es2

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

          -- Left-hand side of first rewrite rule, with subpattern
          -- rewritten by the second rewrite rule
          let w = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub2 (GlobalRewriteRule -> Term
grRHS GlobalRewriteRule
rew2) Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es1r
          reportSDoc "rewriting.confluence" 30 $ sep
            [ "Plugging hole with w = "
            , nest 2 $ addContext bvTel $ prettyTCM w
            ]
          let rhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
hdf ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Elim]
plug Term
w

          return (rhs1 , rhs2)

        whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hdf (applySubst sub1 $ plug $ hdg es1))

    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 -> ([Elim] -> Term) -> [Elim] -> Term -> Term -> TCM ()
checkCriticalPair Type
a [Elim] -> Term
hd [Elim]
es Term
rhs1 Term
rhs2 = do

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

      let 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, [Elim], Term, Term) -> Set MetaId
forall m.
Monoid m =>
(MetaId -> m) -> (Type, [Elim], Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton ((Type, [Elim], Term, Term) -> Set MetaId)
-> (Type, [Elim], Term, Term) -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (Type
a,[Elim]
es,Term
rhs1,Term
rhs2)

      reportSDoc "rewriting.confluence" 30 $ sep
        [ "Abstracting over metas: "
        , prettyList_ (map' (text . show) ms)
        ]
      (gamma , (a,es,rhs1,rhs2)) <- fromMaybe __IMPOSSIBLE__ <$>
        abstractOverMetas ms (a,es,rhs1,rhs2)

      addContext gamma $ reportSDoc "rewriting.confluence" 10 $ sep
        [ "Found critical pair: "
        , nest 2 $ prettyTCM (hd es)
        , " ---> " , nest 2 $ prettyTCM rhs1
        , " =?= " , nest 2 $ prettyTCM rhs2
        , " : " , nest 2 $ prettyTCM a ]
      reportSDoc "rewriting.confluence" 30 $ do
        gamma <- instantiateFull gamma
        sep [ "Context of critical pair: "
            , nest 2 $ prettyTCM gamma ]

      addContext gamma $ case confChk of

        -- Local confluence check: check that critical pair has a
        -- common reduct.
        ConfluenceCheck
LocalConfluenceCheck -> do
            TCM () -> TCM ()
forall (m :: * -> *) a. (MonadTCEnv 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, MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCM ()
equalTerm Type
a Term
rhs1 Term
rhs2
          TCM () -> (TCErr -> TCM ()) -> TCM ()
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
            TypeError CallStack
_ TCState
s Closure TypeError
err -> do
              prettyErr <- (TCState -> TCState) -> TCMT IO Doc -> TCMT IO Doc
forall a. (TCState -> TCState) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure TypeError -> m Doc
prettyTCM Closure TypeError
err
              warning $ RewriteNonConfluent (hd es) rhs1 rhs2 prettyErr
            TCErr
err           -> TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

        -- Global confluence check: enforce that MGU is again the LHS
        -- of a rewrite rule (actual global confluence then follows
        -- from the triangle property which was checked before).
        ConfluenceCheck
GlobalConfluenceCheck -> do
          (f, t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
forall a. a -> Maybe a -> a
fromMaybe (QName, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
-> TCMT IO (Maybe (QName, Type)) -> TCMT IO (QName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe (QName, Type))
forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead ([Elim] -> Term
hd [])

          let checkEqualLHS :: GlobalRewriteRule -> TCM Bool
              checkEqualLHS (GlobalRewriteRule QName
q Tele (Dom Type)
delta QName
_ [Elim' NLPat]
ps Term
_ Type
_ Bool
_ TopLevelModuleName
_) = do
                TCMT IO (Either Blocked_ Substitution)
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (Tele (Dom Type)
-> TypeOf [Elim]
-> [Elim' NLPat]
-> [Elim]
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Tele (Dom Type)
-> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Tele (Dom Type)
delta (Type
t , [Elim] -> Term
hd) [Elim' NLPat]
ps [Elim]
es) TCMT IO (Either Blocked_ Substitution)
-> (Either Blocked_ Substitution -> TCMT IO Bool) -> TCMT IO Bool
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Left Blocked_
_    -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                  Right Substitution
sub -> do
                    let us :: [Term]
us = Substitution' (SubstArg [Term]) -> [Term] -> [Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Term])
sub ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta
                        as :: [Dom Type]
as = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom Type])
sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
delta
                    VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                      Bool -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless ([Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
us) (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc
"with instantiation" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM [Term]
us))) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
                        Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd [Elim]
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is an instance of the LHS of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
                    ok <- [(Term, Dom Type)] -> TCMT IO Bool
allDistinctVars ([(Term, Dom Type)] -> TCMT IO Bool)
-> [(Term, Dom Type)] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ [Term] -> [Dom Type] -> [(Term, Dom Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip' [Term]
us [Dom Type]
as
                    when ok $ reportSDoc "rewriting.confluence.global" 30 $
                      "It is equal to the LHS of rewrite rule" <+> prettyTCM q
                    return ok
              allDistinctVars :: [(Term,Dom Type)] -> TCM Bool
              allDistinctVars [(Term, Dom Type)]
us = do
                us' <- ((Term, Dom Type) -> TCMT IO Bool)
-> [(Term, Dom Type)] -> TCMT IO [(Term, Dom Type)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not (Bool -> Bool)
-> ((Term, Dom Type) -> TCMT IO Bool)
-> (Term, Dom Type)
-> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Dom Type -> TCMT IO Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM (Dom Type -> TCMT IO Bool)
-> ((Term, Dom Type) -> Dom Type)
-> (Term, Dom Type)
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Dom Type) -> Dom Type
forall a b. (a, b) -> b
snd) [(Term, Dom Type)]
us
                mis <- traverse (\(Term
u,Dom Type
a) -> Term -> Type -> TCMT IO (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
u (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) $ us'
                case sequence mis of
                  Just [Int]
is -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Int]
is
                  Maybe [Int]
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

          rews <- getAllRulesFor f
          let sameRHS = TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO Bool
pureEqualTerm Type
a Term
rhs1 Term
rhs2
          unlessM (sameRHS `or2M` anyM checkEqualLHS rews) $ addContext gamma $
            warning $ RewriteAmbiguousRules (hd es) rhs1 rhs2

    checkTrianglePropertyForRule :: GlobalRewriteRule -> TCM ()
    checkTrianglePropertyForRule :: GlobalRewriteRule -> TCM ()
checkTrianglePropertyForRule (GlobalRewriteRule QName
q Tele (Dom Type)
gamma QName
f [Elim' NLPat]
ps Term
rhs Type
b Bool
c TopLevelModuleName
_) =
      Tele (Dom Type) -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

      u  <- NLPat -> TCMT IO Term
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm (NLPat -> TCMT IO Term) -> NLPat -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' NLPat] -> NLPat
PDef QName
f [Elim' NLPat]
ps
      -- First element in the list is the "best reduct" @ρ(u)@
      (rhou,vs) <- fromMaybe __IMPOSSIBLE__ . uncons <$> allParallelReductions u

      reportSDoc "rewriting.confluence" 40 $ ("rho(" <> prettyTCM u <> ") =") <+> prettyTCM rhou
      reportSDoc "rewriting.confluence" 40 $ ("S(" <> prettyTCM u <> ") =") <+> prettyList_ (map' prettyTCM vs)

      -- If present, last element is always equal to u
      caseMaybe (initLast vs) (return ()) $ \([Term]
vs',Term
u') -> do
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
u') TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        [Term] -> (Term -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term]
vs' ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Term
v -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> Term -> Term -> TCMT IO Bool
checkParallelReductionStep Type
b Term
v Term
rhou) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Warning
RewriteMissingRule Term
u Term
v Term
rhou

    checkParallelReductionStep :: Type -> Term -> Term -> TCM Bool
    checkParallelReductionStep :: Type -> Term -> Term -> TCMT IO Bool
checkParallelReductionStep Type
a Term
u Term
w = do
      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ TCMT IO Doc
"Global confluence: checking if" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
        , TCMT IO Doc
"reduces to" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
w , TCMT IO Doc
"in one parallel step." ]
      ListT (TCMT IO) Term -> (Term -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) a.
Monad m =>
ListT m a -> (a -> m Bool) -> m Bool
anyListT (Term -> ListT (TCMT IO) Term
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Term -> m Term
parReduce Term
u) ((Term -> TCMT IO Bool) -> TCMT IO Bool)
-> (Term -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \Term
v -> do
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u , TCMT IO Doc
" reduces to " , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
          ]
        eq <- TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO Bool
pureEqualTerm Type
a Term
v Term
w
        when eq $ reportSDoc "rewriting.confluence.global" 30 $ fsep
          [ "  which is equal to" , prettyTCM w
          ]
        return eq


sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol QName
f = do
    -- Andreas, 2025-06-28, PR #7934:
    -- By getting all rewrite rules regardless of scope,
    -- we replicate the old (unhygienic) approach to rewrite rule scoping
    -- here to avoid a regression.
    -- See also #7969 for a reason why the code below is questionable.
    rules <- [GlobalRewriteRule] -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
PureTCM m =>
[GlobalRewriteRule] -> m [GlobalRewriteRule]
sortRules ([GlobalRewriteRule] -> TCMT IO [GlobalRewriteRule])
-> TCMT IO [GlobalRewriteRule] -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> QName -> TCMT IO [GlobalRewriteRule]
forall (m :: * -> *).
ReadTCState m =>
Bool -> QName -> m [GlobalRewriteRule]
getFilteredGlobalRewriteRulesFor Bool
False QName
f
    modifySignature $ over sigRewriteRules $ HMap.insert f rules
  where
    sortRules :: PureTCM m => [GlobalRewriteRule] -> m [GlobalRewriteRule]
    sortRules :: forall (m :: * -> *).
PureTCM m =>
[GlobalRewriteRule] -> m [GlobalRewriteRule]
sortRules [GlobalRewriteRule]
rs = do
      ordPairs <- Set (QName, QName) -> Set (QName, QName)
forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops (Set (QName, QName) -> Set (QName, QName))
-> ([(GlobalRewriteRule, GlobalRewriteRule)] -> Set (QName, QName))
-> [(GlobalRewriteRule, GlobalRewriteRule)]
-> Set (QName, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(QName, QName)] -> Set (QName, QName)
forall a. Ord a => [a] -> Set a
Set.fromList ([(QName, QName)] -> Set (QName, QName))
-> ([(GlobalRewriteRule, GlobalRewriteRule)] -> [(QName, QName)])
-> [(GlobalRewriteRule, GlobalRewriteRule)]
-> Set (QName, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((GlobalRewriteRule, GlobalRewriteRule) -> (QName, QName))
-> [(GlobalRewriteRule, GlobalRewriteRule)] -> [(QName, QName)]
forall a b. (a -> b) -> [a] -> [b]
map' (GlobalRewriteRule -> QName
grName (GlobalRewriteRule -> QName)
-> (GlobalRewriteRule -> QName)
-> (GlobalRewriteRule, GlobalRewriteRule)
-> (QName, QName)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** GlobalRewriteRule -> QName
grName) ([(GlobalRewriteRule, GlobalRewriteRule)] -> Set (QName, QName))
-> m [(GlobalRewriteRule, GlobalRewriteRule)]
-> m (Set (QName, QName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((GlobalRewriteRule, GlobalRewriteRule) -> m Bool)
-> [(GlobalRewriteRule, GlobalRewriteRule)]
-> m [(GlobalRewriteRule, GlobalRewriteRule)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((GlobalRewriteRule -> GlobalRewriteRule -> m Bool)
-> (GlobalRewriteRule, GlobalRewriteRule) -> m Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((GlobalRewriteRule -> GlobalRewriteRule -> m Bool)
 -> (GlobalRewriteRule, GlobalRewriteRule) -> m Bool)
-> (GlobalRewriteRule -> GlobalRewriteRule -> m Bool)
-> (GlobalRewriteRule, GlobalRewriteRule)
-> m Bool
forall a b. (a -> b) -> a -> b
$ (GlobalRewriteRule -> GlobalRewriteRule -> m Bool)
-> GlobalRewriteRule -> GlobalRewriteRule -> m Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip GlobalRewriteRule -> GlobalRewriteRule -> m Bool
forall (m :: * -> *).
PureTCM m =>
GlobalRewriteRule -> GlobalRewriteRule -> m Bool
moreGeneralLHS) [(GlobalRewriteRule
r1,GlobalRewriteRule
r2) | GlobalRewriteRule
r1 <- [GlobalRewriteRule]
rs, GlobalRewriteRule
r2 <- [GlobalRewriteRule]
rs]
      let perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$
                   (GlobalRewriteRule -> GlobalRewriteRule -> Bool)
-> [GlobalRewriteRule] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (\GlobalRewriteRule
r1 GlobalRewriteRule
r2 -> (GlobalRewriteRule -> QName
grName GlobalRewriteRule
r1,GlobalRewriteRule -> QName
grName GlobalRewriteRule
r2) (QName, QName) -> Set (QName, QName) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (QName, QName)
ordPairs) [GlobalRewriteRule]
rs
      reportSDoc "rewriting.confluence.sort" 50 $ "sorted rules: " <+>
        prettyList_ (map' (prettyTCM . grName) $ permute perm rs)
      return $! permute perm rs

    moreGeneralLHS :: PureTCM m
      => GlobalRewriteRule -> GlobalRewriteRule -> m Bool
    moreGeneralLHS :: forall (m :: * -> *).
PureTCM m =>
GlobalRewriteRule -> GlobalRewriteRule -> m Bool
moreGeneralLHS GlobalRewriteRule
r1 GlobalRewriteRule
r2
      | GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName GlobalRewriteRule
r1 GlobalRewriteRule
r2     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | GlobalRewriteRule -> QName
grHead GlobalRewriteRule
r1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= GlobalRewriteRule -> QName
grHead GlobalRewriteRule
r2 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | Bool
otherwise              = Tele (Dom Type) -> m Bool -> m Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (GlobalRewriteRule -> Tele (Dom Type)
grContext GlobalRewriteRule
r2) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
          def <- QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo (QName -> m Definition) -> QName -> m Definition
forall a b. (a -> b) -> a -> b
$ GlobalRewriteRule -> QName
grHead GlobalRewriteRule
r1
          (t, hd) <- makeHead def (grType r2)
          (vs :: Elims) <- nlPatToTerm $ grPats r2
          res <- isRight <$> onlyReduceTypes
            (nonLinMatch (grContext r1) (t, hd) (grPats r1) vs)
          when res $ reportSDoc "rewriting.confluence.sort" 55 $
            "the lhs of " <+> prettyTCM (grName r1) <+>
            "is more general than the lhs of" <+> prettyTCM (grName r2)
          return res

    deleteLoops :: Ord a => Set (a,a) -> Set (a,a)
    deleteLoops :: forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops Set (a, a)
xs = ((a, a) -> Bool) -> Set (a, a) -> Set (a, a)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(a
x,a
y) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (a
y,a
x) (a, a) -> Set (a, a) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (a, a)
xs) Set (a, a)
xs

makeHead :: PureTCM m => Definition -> Type -> m (Type , Elims -> Term)
makeHead :: forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, [Elim] -> Term)
makeHead Definition
def Type
a = case Definition -> Defn
theDef Definition
def of
  Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
ch } -> do
    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
<$> ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
ch Type
a
    return (ca , Con ch 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right 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
    rtype <- 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
r
    TelV ptel _ <- telView rtype
    n <- getContextSize
    let pars :: Args
        pars = Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
ptel) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
ptel
    ftype <- defType def `piApplyM` pars
    return (ftype , Def f)
  Defn
_ -> (Type, [Elim] -> Term) -> m (Type, [Elim] -> Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> Type
defType Definition
def , QName -> [Elim] -> Term
Def (QName -> [Elim] -> Term) -> QName -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)

sameRuleName :: GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName :: GlobalRewriteRule -> GlobalRewriteRule -> Bool
sameRuleName = QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) (QName -> QName -> Bool)
-> (GlobalRewriteRule -> QName)
-> GlobalRewriteRule
-> GlobalRewriteRule
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` GlobalRewriteRule -> QName
grName

-- | Get both clauses and rewrite rules for the given symbol
getAllRulesFor :: (HasConstInfo m, ReadTCState m, MonadFresh NameId m)
  => QName -> m [GlobalRewriteRule]
getAllRulesFor :: forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getAllRulesFor QName
f = [GlobalRewriteRule] -> [GlobalRewriteRule] -> [GlobalRewriteRule]
forall a. [a] -> [a] -> [a]
(++!) ([GlobalRewriteRule] -> [GlobalRewriteRule] -> [GlobalRewriteRule])
-> m [GlobalRewriteRule]
-> m ([GlobalRewriteRule] -> [GlobalRewriteRule])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m [GlobalRewriteRule]
forall (m :: * -> *).
HasConstInfo m =>
QName -> m [GlobalRewriteRule]
getGlobalRewriteRulesFor QName
f m ([GlobalRewriteRule] -> [GlobalRewriteRule])
-> m [GlobalRewriteRule] -> m [GlobalRewriteRule]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> m [GlobalRewriteRule]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
QName -> m [GlobalRewriteRule]
getClausesAsRewriteRules QName
f

-- | Build a substitution that replaces all variables in the given
--   telescope by fresh metavariables.
makeMetaSubst :: Telescope -> TCM Substitution
makeMetaSubst :: Tele (Dom Type) -> TCM Substitution
makeMetaSubst Tele (Dom Type)
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) -> TCMT IO Args -> TCM Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type) -> TCMT IO Args
newTelMeta Tele (Dom Type)
gamma

computingOverlap :: (MonadTCEnv m) => m a -> m a
computingOverlap :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap = Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eConflComputingOverlap ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True

-- | 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 :: forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 TCM a
f = TCMT IO (Maybe a) -> TCMT IO (Maybe a)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> TCM a -> TCMT IO (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f)
  TCMT IO (Maybe a)
-> (TCErr -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    err :: TCErr
err@TypeError{} -> do
      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Unification failed with error: "
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
        ]
      Maybe a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
    TCErr
err -> TCErr -> TCMT IO (Maybe a)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  TCMT IO (Maybe a)
-> (Maybe a -> TCMT IO (Maybe a))
-> (ProblemId -> Maybe a -> TCMT IO (Maybe a))
-> TCMT IO (Maybe a)
forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
`ifNoConstraints` Maybe a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a))
-> (ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ \ProblemId
pid Maybe a
_ -> do
    cs <- ProblemId -> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
    prettyCs <- prettyInterestingConstraints cs
    warning $ RewriteMaybeNonConfluent lhs1 lhs2 prettyCs
    return Nothing


type MonadParallelReduce m =
  ( PureTCM m
  , MonadFresh NameId m
  )

-- | List all possible single-step parallel reductions of the given term.
allParallelReductions :: (MonadParallelReduce m, ParallelReduce a) => a -> m [a]
allParallelReductions :: forall (m :: * -> *) a.
(MonadParallelReduce m, ParallelReduce a) =>
a -> m [a]
allParallelReductions = ListT m a -> m [a]
forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT (ListT m a -> m [a]) -> (a -> ListT m a) -> a -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ListT m a
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce

-- | Single-step parallel reduction of a given term.
--   The monad 'm' can be instantiated in multiple ways:
--   * Use 'MaybeT TCM' to get the "optimal reduct" obtained by
--     applying rewrite rules eagerly.
--   * Use 'ListT TCM' to obtain all possible one-step parallel
--     reductions.
class ParallelReduce a where
  parReduce :: (MonadParallelReduce m, MonadPlus m) => a -> m a

  default parReduce
    :: ( MonadParallelReduce m, MonadPlus m
       , Traversable f, a ~ f b, ParallelReduce b)
    => a -> m a
  parReduce = (b -> m b) -> f b -> m (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse b -> m b
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
b -> m b
parReduce

-- | Compute possible one-step reductions by applying a rewrite rule
--   at the top-level and reducing all subterms in the position of a
--   variable of the rewrite rule in parallel.
topLevelReductions :: (MonadParallelReduce m, MonadPlus m) => (Elims -> Term) -> Elims -> m Term
topLevelReductions :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
([Elim] -> Term) -> [Elim] -> m Term
topLevelReductions [Elim] -> Term
hd [Elim]
es = do
  VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd [Elim]
es)
  -- Get type of head symbol
  (f , t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
forall a. a -> Maybe a -> a
fromMaybe (QName, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
-> m (Maybe (QName, Type)) -> m (QName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (Maybe (QName, Type))
forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead ([Elim] -> Term
hd [])
  reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: head symbol" <+> prettyTCM (hd []) <+> ":" <+> prettyTCM t
  GlobalRewriteRule q gamma _ ps rhs b c _ <- scatterMP (getAllRulesFor f)
  reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: trying rule" <+> prettyTCM q
  -- Don't reduce if underapplied
  guard $ length es >= length ps
  let (es0 , es1) = splitAt (length ps) es
  onlyReduceTypes (nonLinMatch gamma (t,hd) ps es0) >>= \case
    -- Matching failed: no reduction
    Left Blocked_
block -> m Term
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    -- Matching succeeded
    Right Substitution
sub -> do
      let vs :: [Term]
vs = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' (Substitution -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution
sub) ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Int
0..(Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gammaInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
      sub' <- [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> m [Term] -> m Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> m [Term]
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
[Term] -> m [Term]
parReduce [Term]
vs
      es1' <- parReduce es1
      let w = (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub' Term
rhs) Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim]
es1'
      reportSDoc "rewriting.parreduce" 50 $ "topLevelReductions: rewrote" <+> prettyTCM (hd es) <+> "to" <+> prettyTCM w
      return w

instance ParallelReduce Term where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Term -> m Term
parReduce = \case
    -- Interesting cases
    (Def QName
f [Elim]
es) -> (([Elim] -> Term) -> [Elim] -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
([Elim] -> Term) -> [Elim] -> m Term
topLevelReductions (QName -> [Elim] -> Term
Def QName
f) [Elim]
es) m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (QName -> [Elim] -> Term
Def QName
f ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
[Elim] -> m [Elim]
parReduce [Elim]
es)
    (Con ConHead
c ConInfo
ci [Elim]
es) -> (([Elim] -> Term) -> [Elim] -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
([Elim] -> Term) -> [Elim] -> m Term
topLevelReductions (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci) [Elim]
es) m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
[Elim] -> m [Elim]
parReduce [Elim]
es)

    -- Congruence cases
    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 :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs Term -> m (Abs Term)
parReduce Abs Term
u
    Var Int
x [Elim]
es -> Int -> [Elim] -> Term
Var Int
x ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
[Elim] -> m [Elim]
parReduce [Elim]
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 :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Dom Type -> m (Dom Type)
parReduce Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs Type -> m (Abs Type)
parReduce Abs Type
b
    Sort Sort' Term
s   -> Sort' Term -> Term
Sort  (Sort' Term -> Term) -> m (Sort' Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Sort' Term -> m (Sort' Term)
parReduce Sort' Term
s

    -- Base cases
    u :: Term
u@Lit{}      -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Level{}    -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u -- TODO: is this fine?
    u :: Term
u@DontCare{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Dummy{}    -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u -- not __IMPOSSIBLE__ because of presence of Dummy
                             -- parameters for rewrite rules on constructors.

    -- Impossible cases
    MetaV{}    -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ParallelReduce Sort where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Sort' Term -> m (Sort' Term)
parReduce = Sort' Term -> m (Sort' Term)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure -- TODO: is this fine?

instance ParallelReduce a => ParallelReduce (Arg a) where
instance ParallelReduce a => ParallelReduce (Dom a) where
instance ParallelReduce a => ParallelReduce (Type' a) where
instance ParallelReduce a => ParallelReduce [a] where

instance ParallelReduce a => ParallelReduce (Elim' a) where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Elim' a -> m (Elim' a)
parReduce (Apply Arg a
u)  = Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a) -> m (Arg a) -> m (Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg a -> m (Arg a)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Arg a -> m (Arg a)
parReduce Arg a
u
  parReduce e :: Elim' a
e@Proj{}   = Elim' a -> m (Elim' a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
  parReduce e :: Elim' a
e@IApply{} = Elim' a -> m (Elim' a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e -- TODO

instance (Subst a, ParallelReduce a) => ParallelReduce (Abs a) where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs a -> m (Abs a)
parReduce = Dom Type -> (a -> m a) -> Abs a -> m (Abs a)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ a -> m a
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce


-- | 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 :: forall a.
MetasToVars a =>
[MetaId] -> a -> TCM (Maybe (Tele (Dom Type), a))
abstractOverMetas [MetaId]
ms a
x = do

  -- Sort metas in dependency order
  TCMT IO (Maybe [MetaId])
-> ([MetaId] -> TCMT IO (Tele (Dom Type), a))
-> TCMT IO (Maybe (Tele (Dom Type), 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 (Tele (Dom Type), a))
 -> TCMT IO (Maybe (Tele (Dom Type), a)))
-> ([MetaId] -> TCMT IO (Tele (Dom Type), a))
-> TCMT IO (Maybe (Tele (Dom Type), a))
forall a b. (a -> b) -> a -> b
$ \[MetaId]
ms' -> do

    -- Get types and suggested names of metas
    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 :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType
    ns <- forM ms' getMetaNameSuggestion

    -- Construct telescope (still containing the metas)
    let n     = [MetaId] -> Int
forall a. Sized a => a -> Int
size [MetaId]
ms'
        gamma = Int -> [VerboseKey] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' Int
n [VerboseKey]
ns ([Dom Type] -> Tele (Dom Type)) -> [Dom Type] -> Tele (Dom Type)
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 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'
    runReaderT (metasToVars (gamma, x)) metaIndex

-- | A @OneHole p@ is a @p@ with a subpattern @f ps@ singled out.
data OneHole a = OneHole
  { forall a. OneHole a -> Tele (Dom Type)
ohBoundVars :: Telescope     -- Telescope of bound variables at the hole
  , forall a. OneHole a -> Type
ohType      :: Type          -- Type of the term in the hole
  , forall a. OneHole a -> Term -> a
ohPlugHole  :: Term -> a     -- Plug the hole with some term
  , forall a. OneHole a -> [Elim] -> Term
ohHead      :: Elims -> Term -- The head symbol of the term in the hole
  , forall a. OneHole a -> [Elim]
ohElims     :: Elims         -- The eliminations of the term in the hole
  } deriving ((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
$cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
fmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
$c<$ :: forall a b. a -> OneHole b -> OneHole a
<$ :: forall a b. a -> OneHole b -> OneHole a
Functor)

ohHeadName :: OneHole a -> QName
ohHeadName :: forall a. OneHole a -> QName
ohHeadName OneHole a
oh = case OneHole a -> [Elim] -> Term
forall a. OneHole a -> [Elim] -> Term
ohHead OneHole a
oh [] of
  Def QName
f [Elim]
_   -> QName
f
  Con ConHead
c ConInfo
_ [Elim]
_ -> ConHead -> QName
conName ConHead
c
  Term
_         -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__

ohContents :: OneHole a -> Term
ohContents :: forall a. OneHole a -> Term
ohContents OneHole a
oh = OneHole a -> [Elim] -> Term
forall a. OneHole a -> [Elim] -> Term
ohHead OneHole a
oh ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ OneHole a -> [Elim]
forall a. OneHole a -> [Elim]
ohElims OneHole a
oh

-- | The trivial hole
idHole :: Type -> Term -> OneHole Term
idHole :: Type -> Term -> OneHole Term
idHole Type
a = \case
  Def QName
f [Elim]
es    -> Tele (Dom Type)
-> Type
-> (Term -> Term)
-> ([Elim] -> Term)
-> [Elim]
-> OneHole Term
forall a.
Tele (Dom Type)
-> Type -> (Term -> a) -> ([Elim] -> Term) -> [Elim] -> OneHole a
OneHole Tele (Dom Type)
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (QName -> [Elim] -> Term
Def QName
f) [Elim]
es
  Con ConHead
c ConInfo
ci [Elim]
es -> Tele (Dom Type)
-> Type
-> (Term -> Term)
-> ([Elim] -> Term)
-> [Elim]
-> OneHole Term
forall a.
Tele (Dom Type)
-> Type -> (Term -> a) -> ([Elim] -> Term) -> [Elim] -> OneHole a
OneHole Tele (Dom Type)
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci) [Elim]
es
  Term
_           -> OneHole Term
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Plug a hole with another hole
composeHole :: OneHole Term -> OneHole a -> OneHole a
composeHole :: forall a. OneHole Term -> OneHole a -> OneHole a
composeHole OneHole Term
inner OneHole a
outer = OneHole
  { ohBoundVars :: Tele (Dom Type)
ohBoundVars = OneHole a -> Tele (Dom Type)
forall a. OneHole a -> Tele (Dom Type)
ohBoundVars OneHole a
outer Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` OneHole Term -> Tele (Dom Type)
forall a. OneHole a -> Tele (Dom Type)
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
  , ohHead :: [Elim] -> Term
ohHead      = OneHole Term -> [Elim] -> Term
forall a. OneHole a -> [Elim] -> Term
ohHead OneHole Term
inner
  , ohElims :: [Elim]
ohElims     = OneHole Term -> [Elim]
forall a. OneHole a -> [Elim]
ohElims OneHole Term
inner
  }

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

-- | Given a @p : a@, @allHoles p@ lists all the possible
--   decompositions @p = p'[(f ps)/x]@.
class (TermSubst p, Free p) => AllHoles p where
  allHoles :: (Alternative m, PureTCM m) => TypeOf p -> p -> m (OneHole p)

allHoles_
  :: ( Alternative m , PureTCM m , AllHoles p , TypeOf p ~ () )
  => p -> m (OneHole p)
allHoles_ :: forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ = TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles ()

allHolesList
  :: ( PureTCM m , AllHoles p)
  => TypeOf p -> p -> m [OneHole p]
allHolesList :: forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
TypeOf p -> p -> m [OneHole p]
allHolesList TypeOf 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
. TypeOf p -> p -> ListT m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles TypeOf 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 :: forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
a Term
v [] = OneHole Term -> TCMT IO (OneHole Term)
forall a. a -> TCMT IO a
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 -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Forcing" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a , TCMT IO Doc
"to take one more argument" ]
    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_
    cod <- addContext dom $ newTypeMeta_
    equalType a $ mkPi (("x",) <$> dom) cod

    -- Construct body of eta-expansion
    let body = Int -> Term -> Term
forall a. Subst 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
    addContext dom $ ohAddBV "x" dom . fmap (Lam i . mkAbs "x") <$>
      forceEtaExpansion cod body es

  Proj ProjOrigin
o QName
f -> do

    -- Force a to be the right record type for projection by f
    VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Forcing" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a , TCMT IO Doc
"to be projectible by" , QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f ]
    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) -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe QName)
getRecordOfField QName
f
    Defn{ defType = ra, theDef = RecordDefn rdef } <- getConstInfo r
    pars <- newArgsMeta ra
    s <- ra `piApplyM` pars >>= \Type
s -> Type
-> (Sort' Term -> TCMT IO (Sort' Term))
-> TCMT IO (Sort' Term)
-> TCMT IO (Sort' Term)
forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort' Term -> m a) -> m a -> m a
ifIsSort Type
s Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TCMT IO (Sort' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
    equalType a $ El s (Def r $ map' Apply pars)

    -- Eta-expand v at record type r, and get field corresponding to f
    (_ , c , ci , fields) <- etaExpandRecord_ r pars rdef v
    let fs        = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
rdef
        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  = 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
w = ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> [Elim]) -> Args -> [Elim]
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 a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Args
fields

    -- Get type of field corresponding to f
    ~(Just (El _ (Pi b c))) <- getDefType f =<< reduce a
    let fa = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v

    -- Continue with remaining eliminations
    fmap fUpdate <$> forceEtaExpansion fa fContent es

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

-- Instances for @AllHoles@

instance AllHoles p => AllHoles (Arg p) where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Arg p) -> Arg p -> m (OneHole (Arg p))
allHoles TypeOf (Arg p)
a Arg p
x = (p -> Arg p) -> OneHole p -> OneHole (Arg p)
forall a b. (a -> b) -> OneHole a -> OneHole b
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
<$> TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles (Dom' Term (TypeOf p) -> TypeOf p
forall t e. Dom' t e -> e
unDom TypeOf (Arg p)
Dom' Term (TypeOf p)
a) (Arg p -> p
forall e. Arg e -> e
unArg Arg p
x)

instance AllHoles p => AllHoles (Dom p) where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Dom p) -> Dom p -> m (OneHole (Dom p))
allHoles TypeOf (Dom p)
a Dom p
x = (p -> Dom p) -> OneHole p -> OneHole (Dom p)
forall a b. (a -> b) -> OneHole a -> OneHole b
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
<$> TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles TypeOf p
TypeOf (Dom p)
a (Dom p -> p
forall t e. Dom' t e -> e
unDom Dom p
x)

instance AllHoles (Abs Term) where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Abs Term) -> Abs Term -> m (OneHole (Abs Term))
allHoles (Dom Type
dom , Abs Type
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
forall (m :: * -> *) a.
MonadAddContext m =>
(VerboseKey, Dom Type) -> 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 a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Term -> Abs Term
forall a. (Subst 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
<$>
      TypeOf Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Term -> Term -> m (OneHole Term)
allHoles (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
a) (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
x)

instance AllHoles (Abs Type) where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
allHoles TypeOf (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
forall (m :: * -> *) a.
MonadAddContext m =>
(VerboseKey, Dom Type) -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a , TypeOf (Abs Type)
Dom 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) TypeOf (Abs Type)
Dom 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 a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Type -> Abs Type
forall a. (Subst 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, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
a)

instance AllHoles Elims where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf [Elim] -> [Elim] -> m (OneHole [Elim])
allHoles (Type
a,[Elim] -> Term
hd) [] = m (OneHole [Elim])
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles (Type
a,[Elim] -> Term
hd) (Elim
e:[Elim]
es) = do
    VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.hole" Int
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Head symbol" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
hd []) , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
      , TCMT IO Doc
"is eliminated by" , Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
e
      ]
    case Elim
e of
      Apply Arg Term
x -> do
        ~(Pi b 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'  = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
            hd' = [Elim] -> Term
hd ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim
eElim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:)
        (fmap ((:es) . Apply) <$> allHoles b x)
         <|> (fmap (e:) <$> allHoles (a' , hd') es)
      Proj ProjOrigin
o QName
f -> do
        ~(Just (El _ (Pi b c))) <- QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM 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' = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` [Elim] -> Term
hd []
        hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
        fmap (e:) <$> allHoles (a' , hd') es
      IApply Term
x Term
y Term
u -> m (OneHole [Elim])
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty -- TODO: support --confluence-check + --cubical

instance AllHoles Type where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Type -> Type -> m (OneHole Type)
allHoles TypeOf Type
_ (El Sort' Term
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 a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s) (OneHole Term -> OneHole Type)
-> m (OneHole Term) -> m (OneHole Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeOf Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Term -> Term -> m (OneHole Term)
allHoles (Sort' Term -> Type
sort Sort' Term
s) Term
a

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

instance AllHoles Sort where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Sort' Term) -> Sort' Term -> m (OneHole (Sort' Term))
allHoles TypeOf (Sort' Term)
_ = \case
    Univ Univ
u Level' Term
l     -> (Level' Term -> Sort' Term)
-> OneHole (Level' Term) -> OneHole (Sort' Term)
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Univ -> Level' Term -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u) (OneHole (Level' Term) -> OneHole (Sort' Term))
-> m (OneHole (Level' Term)) -> m (OneHole (Sort' Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level' Term -> m (OneHole (Level' Term))
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level' Term
l
    Inf Univ
_ Integer
_      -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    Sort' Term
SizeUniv     -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    Sort' Term
LockUniv     -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    Sort' Term
LevelUniv    -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    Sort' Term
IntervalUniv -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
    PiSort{}     -> m (OneHole (Sort' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    FunSort{}    -> m (OneHole (Sort' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    UnivSort{}   -> m (OneHole (Sort' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaS{}      -> m (OneHole (Sort' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
    DefS QName
f [Elim]
es    -> do
      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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      fmap (DefS f) <$> allHoles (fa , Def f) es
    DummyS{}     -> m (OneHole (Sort' Term))
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty

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

instance AllHoles [PlusLevel] where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf [PlusLevel' Term]
-> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
allHoles TypeOf [PlusLevel' Term]
_ []     = m (OneHole [PlusLevel' Term])
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles TypeOf [PlusLevel' Term]
_ (PlusLevel' Term
l:[PlusLevel' Term]
ls) =
    ((PlusLevel' Term -> [PlusLevel' Term])
-> OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term]
forall a b. (a -> b) -> OneHole a -> OneHole b
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, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ PlusLevel' Term
l)
    m (OneHole [PlusLevel' Term])
-> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (([PlusLevel' Term] -> [PlusLevel' Term])
-> OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term]
forall a b. (a -> b) -> OneHole a -> OneHole b
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, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ [PlusLevel' Term]
ls)

instance AllHoles PlusLevel where
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (PlusLevel' Term)
-> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
allHoles TypeOf (PlusLevel' Term)
_ (Plus Integer
n Term
l) = do
    la <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType'
    fmap (Plus n) <$> allHoles la l


-- | 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> m a'
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(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 :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
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 a.
((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 a b. (a -> b) -> Maybe a -> Maybe b
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
forall (m :: * -> *).
(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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x

instance MetasToVars Term where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars = \case
    Var Int
i [Elim]
es   -> Int -> [Elim] -> Term
Var Int
i    ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs Term -> m (Abs Term)
metasToVars Abs Term
u
    Lit Literal
l      -> Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Literal -> Term
Lit Literal
l)
    Def QName
f [Elim]
es   -> QName -> [Elim] -> Term
Def QName
f    ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
es
    Con ConHead
c ConInfo
i [Elim]
es -> ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
i  ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Dom Type -> m (Dom Type)
metasToVars Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs Type -> m (Abs Type)
metasToVars Abs Type
b
    Sort Sort' Term
s     -> Sort' Term -> Term
Sort     (Sort' Term -> Term) -> m (Sort' Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort' Term -> m (Sort' Term)
metasToVars Sort' Term
s
    Level Level' Term
l    -> Level' Term -> Term
Level    (Level' Term -> Term) -> m (Level' Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level' Term -> m (Level' Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Level' Term -> m (Level' Term)
metasToVars Level' Term
l
    MetaV MetaId
x [Elim]
es -> ((MetaId -> Maybe Int) -> Maybe Int) -> m (Maybe Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((MetaId -> Maybe Int) -> MetaId -> Maybe Int
forall a b. (a -> b) -> a -> b
$ MetaId
x) m (Maybe Int) -> (Maybe Int -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Int
i   -> Int -> [Elim] -> Term
Var Int
i    ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
es
      Maybe Int
Nothing  -> MetaId -> [Elim] -> Term
MetaV MetaId
x  ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars Term
u
    Dummy DummyTermKind
s [Elim]
es -> DummyTermKind -> [Elim] -> Term
Dummy DummyTermKind
s  ([Elim] -> Term) -> m [Elim] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim] -> m [Elim]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
 HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[Elim] -> m [Elim]
metasToVars [Elim]
es

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

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

instance MetasToVars Level where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Level' Term -> m (Level' Term)
metasToVars (Max Integer
n [PlusLevel' Term]
ls) = Integer -> [PlusLevel' Term] -> Level' Term
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level' Term)
-> m [PlusLevel' Term] -> m (Level' Term)
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[PlusLevel' Term] -> m [PlusLevel' Term]
metasToVars [PlusLevel' Term]
ls

instance MetasToVars PlusLevel where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
PlusLevel' Term -> m (PlusLevel' Term)
metasToVars (Plus Integer
n Term
x) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' 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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars Term
x

instance MetasToVars a => MetasToVars (Tele a) where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Tele a -> m (Tele a)
metasToVars Tele a
EmptyTel = Tele a -> m (Tele a)
forall a. a -> m 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
forall (m :: * -> *).
(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 a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs (Tele a) -> m (Abs (Tele a))
metasToVars Abs (Tele a)
tel

instance (MetasToVars a, MetasToVars b) => MetasToVars (a,b) where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y

instance (MetasToVars a, MetasToVars b, MetasToVars c) => MetasToVars (a,b,c) where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(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
forall (m :: * -> *).
(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 a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
c -> m c
metasToVars c
z

instance (MetasToVars a, MetasToVars b, MetasToVars c, MetasToVars d) => MetasToVars (a,b,c,d) where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(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
forall (m :: * -> *).
(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 a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
c -> m c
metasToVars c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
d -> m d
metasToVars d
w