{-# LANGUAGE ScopedTypeVariables #-}
{-# 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' ↦ v'@ where @ps@ and @ps'@ can be
--    unified@.
--
-- 2. Subpatterns @g qs@ of @ps@ and rewrite rules @g qs' ↦ w@ where
--    @qs@ and @qs'@ can be unified.
--
-- Each of these leads to a *critical pair* @v₁ <-- u --> v₂@, which
-- should satisfy @v₁ = v₂@.
--
-- 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.Arrow ((***))
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader

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 ( workOnTypes , 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.Applicative
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

-- ^ 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
  [RewriteRule]
rews <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getClausesAsRewriteRules QName
f
  let matchables :: [[QName]]
matchables = (RewriteRule -> [QName]) -> [RewriteRule] -> [[QName]]
forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [RewriteRule]
rews
  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Function" 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
prettyTCM QName
f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has matchable symbols" 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_ (([QName] -> TCMT IO Doc) -> [[QName]] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [[QName]]
matchables)
  (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f ([QName] -> Signature -> Signature)
-> [QName] -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ [[QName]] -> [QName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[QName]]
matchables
  let hasRules :: QName -> f Bool
hasRules QName
g = Bool -> Bool
not (Bool -> Bool) -> ([RewriteRule] -> Bool) -> [RewriteRule] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([RewriteRule] -> Bool) -> f [RewriteRule] -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
g
  [(RewriteRule, [QName])]
-> ((RewriteRule, [QName]) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([RewriteRule] -> [[QName]] -> [(RewriteRule, [QName])]
forall a b. [a] -> [b] -> [(a, b)]
zip [RewriteRule]
rews [[QName]]
matchables) (((RewriteRule, [QName]) -> TCM ()) -> TCM ())
-> ((RewriteRule, [QName]) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \(RewriteRule
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] -> TCM ()) -> TCM ()) -> ([QName] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \[QName]
_ -> do
      ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [RewriteRule
rew]

-- ^ Check confluence of the given rewrite rules wrt all other rewrite
--   rules (also amongst themselves).
checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [RewriteRule]
rews = TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

  -- 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
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 :: RewriteRule -> f (Set QName)
getSymbols RewriteRule
rew = let f :: QName
f = RewriteRule -> QName
rewHead RewriteRule
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 => QName -> m Definition
getConstInfo QName
f
    [QName]
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
<$> (RewriteRule -> TCMT IO (Set QName))
-> [RewriteRule] -> TCMT IO [Set QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse RewriteRule -> TCMT IO (Set QName)
forall {f :: * -> *}.
HasConstInfo f =>
RewriteRule -> f (Set QName)
getSymbols [RewriteRule]
rews
    [QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
allSymbols ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \QName
f -> do
      [RewriteRule]
rewsf <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f
      [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RewriteRule]
rewsf ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.triangle" Nat
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
        RewriteRule -> TCM ()
checkTrianglePropertyForRule RewriteRule
rew

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

  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
<+> RewriteRule -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM RewriteRule
rew

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

  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Head symbol" 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
prettyTCM (Elims -> Term
hdf []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of rewrite rule has type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fa

  -- Step 1: check other rewrite rules that overlap at top position
  TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') (RewriteRule
rewRewriteRule -> [RewriteRule] -> [RewriteRule]
forall a. a -> [a] -> [a]
:[RewriteRule]
rewsRest) Bool -> Bool -> Bool
||
            (RewriteRule -> Bool
rewFromClause RewriteRule
rew Bool -> Bool -> Bool
&& RewriteRule -> Bool
rewFromClause RewriteRule
rew')) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hdf RewriteRule
rew RewriteRule
rew'
  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 1 of confluence check 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)

  -- Step 2: check other rewrite rules that overlap with a subpattern
  -- of this rewrite rule
  Elims
es <- PElims -> TCMT IO Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm PElims
qs
  TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
-> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall a b. (a -> b) -> a -> b
$ PType Elims -> Elims -> TCMT IO [OneHole Elims]
forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
fa, Elims -> Term
hdf) Elims
es) ((OneHole Elims -> TCM ()) -> TCM ())
-> (OneHole Elims -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole -> do
    let g :: QName
g   = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
        hdg :: Elims -> Term
hdg = OneHole Elims -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole Elims
hole
    VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
prettyTCM QName
g
    [RewriteRule]
rews' <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g
    [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RewriteRule]
rews' ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew' -> do
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew RewriteRule
rew' OneHole Elims
hole
  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 2 of confluence check 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)

  -- Step 3: check other rewrite rules that have a subpattern which
  -- overlaps with this rewrite rule
  Set QName -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Definition -> Set QName
defMatchable Definition
def) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
g -> do
    VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
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
prettyTCM QName
f
    TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Elims
es' <- PElims -> TCMT IO Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew')
        let tel' :: Telescope
tel' = RewriteRule -> Telescope
rewContext RewriteRule
rew'
        Definition
def' <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
g
        (Type
ga , Elims -> Term
hdg) <- Telescope
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term))
-> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
forall a b. (a -> b) -> a -> b
$ Definition -> Type -> TCMT IO (Type, Elims -> Term)
forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def' (RewriteRule -> Type
rewType RewriteRule
rew')
        TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
-> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
forall a b. (a -> b) -> a -> b
$ PType Elims -> Elims -> TCMT IO [OneHole Elims]
forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
ga , Elims -> Term
hdg) Elims
es') ((OneHole Elims -> TCM ()) -> TCM ())
-> (OneHole Elims -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole -> do
          let f' :: QName
f' = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdg Elims -> Term
hdf RewriteRule
rew' RewriteRule
rew OneHole Elims
hole
  VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 3 of confluence check 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
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) -> RewriteRule -> RewriteRule -> TCM ()
    checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hd RewriteRule
rew1 RewriteRule
rew2 =
      Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

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

        let f :: QName
f    = RewriteRule -> QName
rewHead RewriteRule
rew1 -- == rewHead rew2
            a1 :: Type
a1   = Substitution' (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
$ RewriteRule -> Type
rewType RewriteRule
rew1
            a2 :: Type
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
$ RewriteRule -> Type
rewType RewriteRule
rew2

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

        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
vcat
          [ TCMT IO Doc
"checkConfluenceTop" 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2)
          , TCMT IO Doc
"  f    = " 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
prettyTCM QName
f
          , TCMT IO Doc
"  ctx1 = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> Telescope
rewContext RewriteRule
rew1)
          , TCMT IO Doc
"  ctx2 = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> Telescope
rewContext RewriteRule
rew2)
          , TCMT IO Doc
"  es1  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es1
          , TCMT IO Doc
"  es2  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es2
          ]

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

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

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

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

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

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

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

        Maybe (Term, Term) -> ((Term, Term) -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Term, Term)
maybeCriticalPair (((Term, Term) -> TCM ()) -> TCM ())
-> ((Term, Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> TCM ()) -> (Term, Term) -> TCM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hd (Elims
es1' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
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) -> RewriteRule -> RewriteRule -> OneHole Elims -> TCM ()
    checkConfluenceSub :: (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew1 RewriteRule
rew2 OneHole Elims
hole0 = do
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2)
      Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
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"

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

        let bvTel0 :: Telescope
bvTel0     = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole0
            k :: Nat
k          = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
bvTel0
            b0 :: Type
b0         = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Substitution -> Substitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
k Substitution
sub1) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Type
forall a. OneHole a -> Type
ohType OneHole Elims
hole0
            g :: QName
g          = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole0
            es0 :: Elims
es0        = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Substitution -> Substitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
k Substitution
sub1) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Elims
forall a. OneHole a -> Elims
ohElims OneHole Elims
hole0
            qs2 :: PElims
qs2        = RewriteRule -> PElims
rewPats RewriteRule
rew2

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

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

        let hole :: OneHole Elims
hole      = OneHole Term
hole1 OneHole Term -> OneHole Elims -> OneHole Elims
forall a. OneHole Term -> OneHole a -> OneHole a
`composeHole` OneHole Elims
hole0
            g :: QName
g         = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole -- == rewHead rew2
            es' :: Elims
es'       = OneHole Elims -> Elims
forall a. OneHole a -> Elims
ohElims OneHole Elims
hole
            bvTel :: Telescope
bvTel     = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole
            plug :: Term -> Elims
plug      = OneHole Elims -> Term -> Elims
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Elims
hole

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

        let es1 :: Elims
es1 = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Substitution -> Substitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
bvTel) Substitution
sub1) Elims
es'
        Elims
es2 <- Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Elims)
sub2 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> TCMT IO Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew2)

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

        let lhs1 :: Term
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
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg Elims
es1
            lhs2 :: Term
lhs2 = Substitution' (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
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es2 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1r
            a :: Type
a    = Substitution' (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
$ RewriteRule -> Type
rewType RewriteRule
rew1

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

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

          -- Right-hand side of first rewrite rule (after unification)
          let rhs1 :: Term
rhs1 = Substitution' (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
$ RewriteRule -> Term
rewRHS RewriteRule
rew1

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

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

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

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

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

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

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

      Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
10 (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
sep
        [ TCMT IO Doc
"Found critical pair: "
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (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
prettyTCM (Elims -> Term
hd Elims
es)
        , TCMT IO Doc
" ---> " , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (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
prettyTCM Term
rhs1
        , TCMT IO Doc
" =?= " , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (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
prettyTCM Term
rhs2
        , TCMT IO Doc
" : " , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Telescope
gamma <- Telescope -> TCMT IO Telescope
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Telescope
gamma
        [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Context of critical pair: "
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma ]

      Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case ConfluenceCheck
confChk of

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

        -- 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
          (QName
f, Type
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 (Elims -> Term
hd [])

          let checkEqualLHS :: RewriteRule -> TCM Bool
              checkEqualLHS :: RewriteRule -> TCMT IO Bool
checkEqualLHS (RewriteRule QName
q Telescope
delta QName
_ PElims
ps Term
_ Type
_ Bool
_) = do
                TCMT IO (Either Blocked_ Substitution)
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (Telescope
-> (Type, Elims -> Term)
-> PElims
-> Elims
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
delta (Type
t , Elims -> Term
hd) PElims
ps Elims
es) TCMT IO (Either Blocked_ Substitution)
-> (Either Blocked_ Substitution -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Left Blocked_
_    -> Bool -> TCMT IO Bool
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
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var ([Nat] -> [Term]) -> [Nat] -> [Term]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Nat]) -> Nat -> [Nat]
forall a b. (a -> b) -> a -> b
$ Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
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
$ Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
                    VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Nat
35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                      Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
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
prettyTCM QName
q 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
prettyTCM [Term]
us)
                    Bool
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
                    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                      TCMT IO Doc
"It is equal to the LHS of rewrite 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
prettyTCM QName
q
                    Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok
              allDistinctVars :: [(Term,Dom Type)] -> TCM Bool
              allDistinctVars :: [(Term, Dom Type)] -> TCMT IO Bool
allDistinctVars [(Term, Dom Type)]
us = do
                [(Term, Dom Type)]
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
                [Maybe Nat]
mis <- ((Term, Dom Type) -> TCMT IO (Maybe Nat))
-> [(Term, Dom Type)] -> TCMT IO [Maybe Nat]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\(Term
u,Dom Type
a) -> Term -> Type -> TCMT IO (Maybe Nat)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Nat)
isEtaVar Term
u (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) ([(Term, Dom Type)] -> TCMT IO [Maybe Nat])
-> [(Term, Dom Type)] -> TCMT IO [Maybe Nat]
forall a b. (a -> b) -> a -> b
$ [(Term, Dom Type)]
us'
                case [Maybe Nat] -> Maybe [Nat]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe Nat]
mis of
                  Just [Nat]
is -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ [Nat] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Nat]
is
                  Maybe [Nat]
Nothing -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

          [RewriteRule]
rews <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f
          let sameRHS :: TCMT IO Bool
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
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
rhs1 Term
rhs2
          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (TCMT IO Bool
sameRHS TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` [RewriteRule] -> (RewriteRule -> TCMT IO Bool) -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM [RewriteRule]
rews RewriteRule -> TCMT IO Bool
checkEqualLHS) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (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
RewriteAmbiguousRules (Elims -> Term
hd Elims
es) Term
rhs1 Term
rhs2

    checkTrianglePropertyForRule :: RewriteRule -> TCM ()
    checkTrianglePropertyForRule :: RewriteRule -> TCM ()
checkTrianglePropertyForRule (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
b Bool
c) = Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Term
u  <- NLPat -> TCMT IO Term
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm (NLPat -> TCMT IO Term) -> NLPat -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> PElims -> NLPat
PDef QName
f PElims
ps
      -- First element in the list is the "best reduct" @ρ(u)@
      (Term
rhou,[Term]
vs) <- (Term, [Term]) -> Maybe (Term, [Term]) -> (Term, [Term])
forall a. a -> Maybe a -> a
fromMaybe (Term, [Term])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Term, [Term]) -> (Term, [Term]))
-> ([Term] -> Maybe (Term, [Term])) -> [Term] -> (Term, [Term])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Maybe (Term, [Term])
forall a. [a] -> Maybe (a, [a])
uncons ([Term] -> (Term, [Term]))
-> TCMT IO [Term] -> TCMT IO (Term, [Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO [Term]
forall (m :: * -> *) a.
(MonadParallelReduce m, ParallelReduce a) =>
a -> m [a]
allParallelReductions Term
u
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"rho(" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
") =") 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
prettyTCM Term
rhou
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"S(" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
") =") 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
prettyTCM [Term]
vs)
      -- If present, last element is always equal to u
      Maybe ([Term], Term)
-> TCM () -> (([Term], Term) -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ([Term] -> Maybe ([Term], Term)
forall a. [a] -> Maybe ([a], a)
initLast [Term]
vs) (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((([Term], Term) -> TCM ()) -> TCM ())
-> (([Term], Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \([Term]
vs',Term
u') -> do
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
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 -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Nat
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
prettyTCM Term
u
        , TCMT IO Doc
"reduces to" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
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 -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Nat
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
prettyTCM Term
u , TCMT IO Doc
" reduces to " , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
          ]
        Bool
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
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
v Term
w
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
eq (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Nat
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
"  which is equal to" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
w
          ]
        Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
eq


sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol QName
f = do
    [RewriteRule]
rules <- [RewriteRule] -> TCMT IO [RewriteRule]
forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules ([RewriteRule] -> TCMT IO [RewriteRule])
-> TCMT IO [RewriteRule] -> TCMT IO [RewriteRule]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Lens' (HashMap QName [RewriteRule]) Signature
-> LensMap (HashMap QName [RewriteRule]) Signature
forall i o. Lens' i o -> LensMap i o
over Lens' (HashMap QName [RewriteRule]) Signature
sigRewriteRules LensMap (HashMap QName [RewriteRule]) Signature
-> LensMap (HashMap QName [RewriteRule]) Signature
forall a b. (a -> b) -> a -> b
$ QName
-> [RewriteRule]
-> HashMap QName [RewriteRule]
-> HashMap QName [RewriteRule]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert QName
f [RewriteRule]
rules
  where
    sortRules :: PureTCM m => [RewriteRule] -> m [RewriteRule]
    sortRules :: forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules [RewriteRule]
rs = do
      Set (QName, QName)
ordPairs <- Set (QName, QName) -> Set (QName, QName)
forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops (Set (QName, QName) -> Set (QName, QName))
-> ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
-> [(RewriteRule, RewriteRule)]
-> 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))
-> ([(RewriteRule, RewriteRule)] -> [(QName, QName)])
-> [(RewriteRule, RewriteRule)]
-> Set (QName, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RewriteRule, RewriteRule) -> (QName, QName))
-> [(RewriteRule, RewriteRule)] -> [(QName, QName)]
forall a b. (a -> b) -> [a] -> [b]
map (RewriteRule -> QName
rewName (RewriteRule -> QName)
-> (RewriteRule -> QName)
-> (RewriteRule, RewriteRule)
-> (QName, QName)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** RewriteRule -> QName
rewName) ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
-> m [(RewriteRule, RewriteRule)] -> m (Set (QName, QName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((RewriteRule, RewriteRule) -> m Bool)
-> [(RewriteRule, RewriteRule)] -> m [(RewriteRule, RewriteRule)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((RewriteRule -> RewriteRule -> m Bool)
-> (RewriteRule, RewriteRule) -> m Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((RewriteRule -> RewriteRule -> m Bool)
 -> (RewriteRule, RewriteRule) -> m Bool)
-> (RewriteRule -> RewriteRule -> m Bool)
-> (RewriteRule, RewriteRule)
-> m Bool
forall a b. (a -> b) -> a -> b
$ (RewriteRule -> RewriteRule -> m Bool)
-> RewriteRule -> RewriteRule -> m Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip RewriteRule -> RewriteRule -> m Bool
forall (m :: * -> *).
PureTCM m =>
RewriteRule -> RewriteRule -> m Bool
moreGeneralLHS) [(RewriteRule
r1,RewriteRule
r2) | RewriteRule
r1 <- [RewriteRule]
rs, RewriteRule
r2 <- [RewriteRule]
rs]
      let perm :: Permutation
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
$
                   (RewriteRule -> RewriteRule -> Bool)
-> [RewriteRule] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (\RewriteRule
r1 RewriteRule
r2 -> (RewriteRule -> QName
rewName RewriteRule
r1,RewriteRule -> QName
rewName RewriteRule
r2) (QName, QName) -> Set (QName, QName) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (QName, QName)
ordPairs) [RewriteRule]
rs
      VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.sort" Nat
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sorted rules: " 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_ ((RewriteRule -> TCMT IO Doc) -> [RewriteRule] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> TCMT IO Doc)
-> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) ([RewriteRule] -> [TCMT IO Doc]) -> [RewriteRule] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Permutation -> [RewriteRule] -> [RewriteRule]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [RewriteRule]
rs)
      [RewriteRule] -> m [RewriteRule]
forall (m :: * -> *) a. Monad m => a -> m a
return ([RewriteRule] -> m [RewriteRule])
-> [RewriteRule] -> m [RewriteRule]
forall a b. (a -> b) -> a -> b
$ Permutation -> [RewriteRule] -> [RewriteRule]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [RewriteRule]
rs

    moreGeneralLHS :: PureTCM m => RewriteRule -> RewriteRule -> m Bool
    moreGeneralLHS :: forall (m :: * -> *).
PureTCM m =>
RewriteRule -> RewriteRule -> m Bool
moreGeneralLHS RewriteRule
r1 RewriteRule
r2
      | RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
r1 RewriteRule
r2       = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | RewriteRule -> QName
rewHead RewriteRule
r1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= RewriteRule -> QName
rewHead RewriteRule
r2 = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | Bool
otherwise                = Telescope -> m Bool -> m Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (RewriteRule -> Telescope
rewContext RewriteRule
r2) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
          Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (QName -> m Definition) -> QName -> m Definition
forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewHead RewriteRule
r1
          (Type
t, Elims -> Term
hd) <- Definition -> Type -> m (Type, Elims -> Term)
forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def (RewriteRule -> Type
rewType RewriteRule
r2)
          (Elims
vs :: Elims) <- PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm (PElims -> m Elims) -> PElims -> m Elims
forall a b. (a -> b) -> a -> b
$ RewriteRule -> PElims
rewPats RewriteRule
r2
          Bool
res <- Either Blocked_ Substitution -> Bool
forall a b. Either a b -> Bool
isRight (Either Blocked_ Substitution -> Bool)
-> m (Either Blocked_ Substitution) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (Telescope
-> (Type, Elims -> Term)
-> PElims
-> Elims
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch (RewriteRule -> Telescope
rewContext RewriteRule
r1) (Type
t, Elims -> Term
hd) (RewriteRule -> PElims
rewPats RewriteRule
r1) Elims
vs)
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
res (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.sort" Nat
55 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"the lhs of " 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
r1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            TCMT IO Doc
"is more general than the lhs of" 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
prettyTCM (RewriteRule -> QName
rewName RewriteRule
r2)
          Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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, Elims -> Term)
makeHead Definition
def Type
a = case Definition -> Defn
theDef Definition
def of
  Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
ch } -> do
    Type
ca <- ((QName, Type, Args), Type) -> Type
forall a b. (a, b) -> b
snd (((QName, Type, Args), Type) -> Type)
-> (Maybe ((QName, Type, Args), Type)
    -> ((QName, Type, Args), Type))
-> Maybe ((QName, Type, Args), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
forall a. a -> Maybe a -> a
fromMaybe ((QName, Type, Args), Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
-> 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
    (Type, Elims -> Term) -> m (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ca , ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ConOSystem)
  -- For record projections @f : R Δ → A@, we rely on the invariant
  -- that any clause is fully general in the parameters, i.e. it
  -- is quantified over the parameter telescope @Δ@
  Function { funProjection :: Defn -> Maybe Projection
funProjection = Just Projection
proj } -> do
    let f :: QName
f          = Projection -> QName
projOrig Projection
proj
        r :: QName
r          = Arg QName -> QName
forall e. Arg e -> e
unArg (Arg QName -> QName) -> Arg QName -> QName
forall a b. (a -> b) -> a -> b
$ Projection -> Arg QName
projFromType Projection
proj
    Type
rtype <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
    TelV Telescope
ptel Type
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
rtype
    Nat
n <- m Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
    let pars :: Args
        pars :: Args
pars = Nat -> Args -> Args
forall a. Subst a => Nat -> a -> a
raise (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ptel) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
ptel
    Type
ftype <- Definition -> Type
defType Definition
def Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
    (Type, Elims -> Term) -> m (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ftype , QName -> Elims -> Term
Def QName
f)
  Defn
_ -> (Type, Elims -> Term) -> m (Type, Elims -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> Type
defType Definition
def , QName -> Elims -> Term
Def (QName -> Elims -> Term) -> QName -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)

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

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

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

computingOverlap :: (MonadTCEnv m) => m a -> m a
computingOverlap :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap = Lens' Bool TCEnv -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
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 e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    err :: TCErr
err@TypeError{} -> do
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Nat
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: "
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
prettyTCM TCErr
err
        ]
      Maybe a -> TCMT IO (Maybe 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 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 (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
    Constraints
cs <- ProblemId -> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
    [Doc]
prettyCs <- Constraints -> TCMT IO [Doc]
forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
    Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Doc] -> Warning
RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
prettyCs
    Maybe a -> TCMT IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
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
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)
traverse b -> m b
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
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) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions Elims -> Term
hd Elims
es = do
  VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Nat
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
prettyTCM (Elims -> Term
hd Elims
es)
  -- Get type of head symbol
  (QName
f , Type
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 (Elims -> Term
hd [])
  VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Nat
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: head symbol" 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
prettyTCM (Elims -> Term
hd []) 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
  RewriteRule QName
q Telescope
gamma QName
_ PElims
ps Term
rhs Type
b Bool
c <- m [RewriteRule] -> m RewriteRule
forall (m :: * -> *) (t :: * -> *) a.
(MonadPlus m, Foldable t) =>
m (t a) -> m a
scatterMP (QName -> m [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f)
  VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Nat
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: trying 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
prettyTCM QName
q
  -- Don't reduce if underapplied
  Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Elims -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= PElims -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length PElims
ps
  let (Elims
es0 , Elims
es1) = Nat -> Elims -> (Elims, Elims)
forall a. Nat -> [a] -> ([a], [a])
splitAt (PElims -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length PElims
ps) Elims
es
  m (Either Blocked_ Substitution)
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (Telescope
-> (Type, Elims -> Term)
-> PElims
-> Elims
-> m (Either Blocked_ Substitution)
forall (m :: * -> *) t a b.
(PureTCM m, Match t a b) =>
Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
gamma (Type
t,Elims -> Term
hd) PElims
ps Elims
es0) m (Either Blocked_ Substitution)
-> (Either Blocked_ Substitution -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Matching failed: no reduction
    Left Blocked_
block -> m Term
forall (f :: * -> *) a. Alternative f => f a
empty
    -- Matching succeeded
    Right Substitution
sub -> do
      let vs :: [Term]
vs = (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> Nat -> Term
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution
sub) ([Nat] -> [Term]) -> [Nat] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Nat
0..(Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
gammaNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1)]
      Substitution
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
parReduce [Term]
vs
      Elims
es1' <- Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
es1
      let w :: Term
w = (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub' Term
rhs) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1'
      VerboseKey -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Nat -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Nat
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: rewrote" 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
prettyTCM (Elims -> Term
hd Elims
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to" 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
prettyTCM Term
w
      Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
w

instance ParallelReduce Term where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Term -> m Term
parReduce = \case
    -- Interesting cases
    (Def QName
f Elims
es) -> ((Elims -> Term) -> Elims -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (QName -> Elims -> Term
Def QName
f) Elims
es) m Term -> m Term -> m Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (QName -> Elims -> Term
Def QName
f (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
es)
    (Con ConHead
c ConInfo
ci Elims
es) -> ((Elims -> Term) -> Elims -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
es) m Term -> m Term -> m Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
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
parReduce Abs Term
u
    Var Nat
x Elims
es -> Nat -> Elims -> Term
Var Nat
x (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
es
    Pi Dom Type
a Abs Type
b   -> Dom Type -> Abs Type -> Term
Pi    (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Abs Type
b
    Sort Sort
s   -> Sort -> Term
Sort  (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Sort
s

    -- Base cases
    u :: Term
u@Lit{}      -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Level{}    -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u -- TODO: is this fine?
    u :: Term
u@DontCare{} -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Dummy{}    -> Term -> m Term
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 -> m Sort
parReduce = Sort -> m Sort
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
parReduce Arg a
u
  parReduce e :: Elim' a
e@Proj{}   = Elim' a -> m (Elim' a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
  parReduce IApply{}   = m (Elim' a)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- not yet supported

instance (Free a, 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 b (m :: * -> *).
(Subst a, Subst b, 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
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 (Telescope, a))
abstractOverMetas [MetaId]
ms a
x = do

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

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

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

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

-- ^ A @OneHole p@ is a @p@ with a subpattern @f ps@ singled out.
data OneHole a = OneHole
  { forall a. OneHole a -> Telescope
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 -> Elims -> Term
ohHead      :: Elims -> Term -- The head symbol of the term in the hole
  , forall a. OneHole a -> Elims
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
<$ :: forall a b. a -> OneHole b -> OneHole a
$c<$ :: forall a b. a -> OneHole b -> OneHole a
fmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
$cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
Functor)

ohHeadName :: OneHole a -> QName
ohHeadName :: forall a. OneHole a -> QName
ohHeadName OneHole a
oh = case OneHole a -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole a
oh [] of
  Def QName
f Elims
_   -> QName
f
  Con ConHead
c ConInfo
_ Elims
_ -> 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 -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole a
oh (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ OneHole a -> Elims
forall a. OneHole a -> Elims
ohElims OneHole a
oh

-- | The trivial hole
idHole :: Type -> Term -> OneHole Term
idHole :: Type -> Term -> OneHole Term
idHole Type
a = \case
  Def QName
f Elims
es    -> Telescope
-> Type
-> (Term -> Term)
-> (Elims -> Term)
-> Elims
-> OneHole Term
forall a.
Telescope
-> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
OneHole Telescope
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (QName -> Elims -> Term
Def QName
f) Elims
es
  Con ConHead
c ConInfo
ci Elims
es -> Telescope
-> Type
-> (Term -> Term)
-> (Elims -> Term)
-> Elims
-> OneHole Term
forall a.
Telescope
-> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
OneHole Telescope
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
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 :: Telescope
ohBoundVars = OneHole a -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole a
outer Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` OneHole Term -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Term
inner
  , ohType :: Type
ohType      = OneHole Term -> Type
forall a. OneHole a -> Type
ohType OneHole Term
inner
  , ohPlugHole :: Term -> a
ohPlugHole  = OneHole a -> Term -> a
forall a. OneHole a -> Term -> a
ohPlugHole OneHole a
outer (Term -> a) -> (Term -> Term) -> Term -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneHole Term -> Term -> Term
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Term
inner
  , ohHead :: Elims -> Term
ohHead      = OneHole Term -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole Term
inner
  , ohElims :: Elims
ohElims     = OneHole Term -> Elims
forall a. OneHole a -> Elims
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 :: Telescope
ohBoundVars = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
x (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ OneHole a -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole a
oh }

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

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

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

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

  Apply (Arg ArgInfo
i a
w) -> do

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

    -- Construct body of eta-expansion
    let body :: Term
body = Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
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
$ Nat -> Term
var Nat
0]

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

  Proj ProjOrigin
o QName
f -> do

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

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

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

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

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

-- ^ Instances for @AllHoles@

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

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

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

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

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

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

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

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

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

instance AllHoles PlusLevel where
  type PType PlusLevel = ()
  allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
PType (PlusLevel' Term)
-> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
allHoles PType (PlusLevel' Term)
_ (Plus Integer
n Term
l) = do
    Type
la <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
    (Term -> PlusLevel' Term)
-> OneHole Term -> OneHole (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) (OneHole Term -> OneHole (PlusLevel' Term))
-> m (OneHole Term) -> m (OneHole (PlusLevel' Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PType Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles Type
PType Term
la Term
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)
traverse a' -> m a'
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) 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 Nat) 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 Nat) -> MetaId -> Maybe Nat) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Nat -> Nat) -> Maybe Nat -> Maybe Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Nat -> Nat
forall a. Enum a => a -> a
succ (Maybe Nat -> Maybe Nat)
-> (MetaId -> Maybe Nat) -> MetaId -> Maybe Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x

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

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

instance MetasToVars Sort where
  metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Nat) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars = \case
    Type Level
l     -> Level -> Sort
forall t. Level' t -> Sort' t
Type     (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Prop Level
l     -> Level -> Sort
forall t. Level' t -> Sort' t
Prop     (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Inf IsFibrant
f Integer
n    -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    SSet Level
l     -> Level -> Sort
forall t. Level' t -> Sort' t
SSet     (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Sort
SizeUniv   -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
SizeUniv
    Sort
LockUniv   -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
LockUniv
    PiSort Dom' Term Term
s Sort
t Abs Sort
u -> Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort   (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> m (Dom' Term Term) -> m (Sort -> Abs Sort -> Sort)
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 Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Dom' Term Term
s m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
t m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Sort -> m (Abs Sort)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Sort
u
    FunSort Sort
s Sort
t -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort) -> m Sort -> m (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s m (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
t
    UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s
    MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DefS QName
f Elims
es  -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f   (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DummyS VerboseKey
s   -> Sort -> m Sort
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Sort
forall t. VerboseKey -> Sort' t
DummyS VerboseKey
s

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

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

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

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

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

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