{-# 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 <- forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getClausesAsRewriteRules QName
f
  let noMetasInPats :: RewriteRule -> TCMT IO Bool
noMetasInPats RewriteRule
rew
        | forall a. AllMetas a => a -> Bool
noMetas (RewriteRule -> PElims
rewPats RewriteRule
rew) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        | Bool
otherwise             = do
            forall (m :: * -> *). MonadWarning m => Doc -> m ()
genericWarning forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
              forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Confluence checking incomplete because the definition of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text String
"contains unsolved metavariables."
            forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  [RewriteRule]
rews <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM RewriteRule -> TCMT IO Bool
noMetasInPats [RewriteRule]
rews
  let matchables :: [[QName]]
matchables = forall a b. (a -> b) -> [a] -> [b]
map forall a. GetMatchables a => a -> [QName]
getMatchables [RewriteRule]
rews
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Function" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has matchable symbols" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [[QName]]
matchables)
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[QName]]
matchables
  let hasRules :: QName -> f Bool
hasRules QName
g = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
g
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [RewriteRule]
rews [[QName]]
matchables) forall a b. (a -> b) -> a -> b
$ \(RewriteRule
rew,[QName]
ms) ->
    forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall {f :: * -> *}. HasConstInfo f => QName -> f Bool
hasRules [QName]
ms) 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 = forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode 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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConfluenceCheck
confChk forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) 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
         (forall a. Ord a => a -> Set a -> Set a
Set.insert QName
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Set QName
defMatchable forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
    [QName]
allSymbols <- forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {f :: * -> *}.
HasConstInfo f =>
RewriteRule -> f (Set QName)
getSymbols [RewriteRule]
rews
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [QName]
allSymbols forall a b. (a -> b) -> a -> b
$ \QName
f -> do
      [RewriteRule]
rewsf <- forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RewriteRule]
rewsf forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.triangle" Nat
10 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"(re)checking triangle property for rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
        RewriteRule -> TCM ()
checkTrianglePropertyForRule RewriteRule
rew

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

  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
10 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Checking confluence of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Checking confluence of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
  (Type
fa , Elims -> Term
hdf) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def (RewriteRule -> Type
rewType RewriteRule
rew)

  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Head symbol" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hdf []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of rewrite rule has type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
  forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f) forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') (RewriteRule
rewforall a. a -> [a] -> [a]
:[RewriteRule]
rewsRest) Bool -> Bool -> Bool
||
            (RewriteRule -> Bool
rewFromClause RewriteRule
rew Bool -> Bool -> Bool
&& RewriteRule -> Bool
rewFromClause RewriteRule
rew')) forall a b. (a -> b) -> a -> b
$
      (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hdf RewriteRule
rew RewriteRule
rew'
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 1 of confluence check of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 <- forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm PElims
qs
  forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
fa, Elims -> Term
hdf) Elims
es) forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole -> do
    let g :: QName
g   = forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
        hdg :: Elims -> Term
hdg = forall a. OneHole a -> Elims -> Term
ohHead OneHole Elims
hole
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
40 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Found hole with head symbol" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
g
    [RewriteRule]
rews' <- forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RewriteRule]
rews' forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew' -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) 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
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 2 of confluence check of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Definition -> Set QName
defMatchable Definition
def) forall a b. (a -> b) -> a -> b
$ \ QName
g -> do
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
40 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Symbol" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
g forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has rules that match on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g) forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) forall a b. (a -> b) -> a -> b
$ do
        Elims
es' <- 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' <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
g
        (Type
ga , Elims -> Term
hdg) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def' (RewriteRule -> Type
rewType RewriteRule
rew')
        forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
PType p -> p -> m [OneHole p]
allHolesList (Type
ga , Elims -> Term
hdg) Elims
es') forall a b. (a -> b) -> a -> b
$ \ OneHole Elims
hole -> do
          let f' :: QName
f' = forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QName
f forall a. Eq a => a -> a -> Bool
== QName
f') 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
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Finished step 3 of confluence check of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 =
      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)) forall a b. (a -> b) -> a -> b
$
      forall a. TCM a -> TCM a
localTCStateSavingWarnings forall a b. (a -> b) -> a -> b
$ do

        Substitution
sub1 <- forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew1
        Substitution
sub2 <- forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst 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   = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub1 forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew1
            a2 :: Type
a2   = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub2 forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew2

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

        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"checkConfluenceTop" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew1) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2)
          , TCMT IO Doc
"  f    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
          , TCMT IO Doc
"  ctx1 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> Telescope
rewContext RewriteRule
rew1)
          , TCMT IO Doc
"  ctx2 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> Telescope
rewContext RewriteRule
rew2)
          , TCMT IO Doc
"  es1  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es1
          , TCMT IO Doc
"  es2  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 = forall a. Ord a => a -> a -> a
min (forall a. Sized a => a -> Nat
size Elims
es1) (forall a. Sized a => a -> Nat
size Elims
es2)
            (Elims
es1' , Elims
es1r) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Elims
es1
            (Elims
es2' , Elims
es2r) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Elims
es2
            esr :: Elims
esr           = Elims
es1r forall a. [a] -> [a] -> [a]
++ Elims
es2r

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

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

        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"Considering potential critical pair at top-level: "
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Term
lhs1, TCMT IO Doc
" =?= "
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Term
lhs2 , TCMT IO Doc
" : " , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
          ]

        Maybe (Term, Term)
maybeCriticalPair <- forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 forall a b. (a -> b) -> a -> b
$ do
          -- Unify the left-hand sides of both rewrite rules
          Type
fa   <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          [Polarity]
fpol <- forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
f
          forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes forall a b. (a -> b) -> a -> b
$
            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 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub1 (RewriteRule -> Term
rewRHS RewriteRule
rew1) forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2r
              rhs2 :: Term
rhs2 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r

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

        forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Term, Term)
maybeCriticalPair forall a b. (a -> b) -> a -> b
$ 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' 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
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
100 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"foo 2" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew1) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2)
      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)) forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
localTCStateSavingWarnings forall a b. (a -> b) -> a -> b
$ do

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

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

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

        -- TODO: support IApply in forceEtaExpansion
        let isIApply :: Elim' a -> Bool
isIApply IApply{} = Bool
True
            isIApply Elim' a
_        = Bool
False
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {a}. Elim' a -> Bool
isIApply forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
drop (forall a. Sized a => a -> Nat
size Elims
es0) PElims
qs2) forall a b. (a -> b) -> a -> b
$ do

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

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

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

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

        let es1 :: Elims
es1 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Telescope
bvTel) Substitution
sub1) Elims
es'
        Elims
es2 <- forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Sized a => a -> Nat
size Elims
es1 forall a. Ord a => a -> a -> Bool
< forall a. Sized a => a -> Nat
size Elims
es2) forall a. HasCallStack => a
__IMPOSSIBLE__
        let n :: Nat
n = forall a. Sized a => a -> Nat
size Elims
es2
            (Elims
es1' , Elims
es1r) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Elims
es1

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

        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"Considering potential critical pair at subpattern: "
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Term
lhs1 , TCMT IO Doc
" =?= "
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Term
lhs2 , TCMT IO Doc
" : " , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
          ]

        Maybe (Term, Term)
maybeCriticalPair <- forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
g
          [Polarity]
gpol <- forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
g
          forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel forall a b. (a -> b) -> a -> b
$
            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 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub1 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 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r
          forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"Plugging hole with w = "
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
bvTel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
w
            ]
          let rhs2 :: Term
rhs2 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub1 forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug Term
w

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

        forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Term, Term)
maybeCriticalPair forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hdf (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub1 forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug 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) <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type
a,Elims
es,Term
rhs1,Term
rhs2)

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

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

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

      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma 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
            forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
rhs1 Term
rhs2
          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 <- forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (forall a b. a -> b -> a
const TCState
s) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure TypeError
err
              forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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           -> 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) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
                forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (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) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Left Blocked_
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                  Right Substitution
sub -> do
                    let us :: [Term]
us = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Telescope
delta
                        as :: [Dom Type]
as = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
                    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.global" Nat
35 forall a b. (a -> b) -> a -> b
$
                      forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is an instance of the LHS of rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with instantiation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
us)
                    Bool
ok <- [(Term, Dom Type)] -> TCMT IO Bool
allDistinctVars forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
us [Dom Type]
as
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.global" Nat
30 forall a b. (a -> b) -> a -> b
$
                      TCMT IO Doc
"It is equal to the LHS of rewrite rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
                    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' <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Term, Dom Type)]
us
                [Maybe Nat]
mis <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\(Term
u,Dom Type
a) -> forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Nat)
isEtaVar Term
u (forall t e. Dom' t e -> e
unDom Dom Type
a)) forall a b. (a -> b) -> a -> b
$ [(Term, Dom Type)]
us'
                case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe Nat]
mis of
                  Just [Nat]
is -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Bool
fastDistinct [Nat]
is
                  Maybe [Nat]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

          [RewriteRule]
rews <- forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f
          let sameRHS :: TCMT IO Bool
sameRHS = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
rhs1 Term
rhs2
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (TCMT IO Bool
sameRHS forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM [RewriteRule]
rews RewriteRule -> TCMT IO Bool
checkEqualLHS) forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$ do
      Term
u  <- forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm 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) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (a, [a])
uncons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadParallelReduce m, ParallelReduce a) =>
a -> m [a]
allParallelReductions Term
u
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
40 forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"rho(" forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
") =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhou
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
40 forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"S(" forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
") =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs)
      -- If present, last element is always equal to u
      forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall a. [a] -> Maybe ([a], a)
initLast [Term]
vs) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \([Term]
vs',Term
u') -> do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term
u forall a. Eq a => a -> a -> Bool
== Term
u') forall a. HasCallStack => a
__IMPOSSIBLE__
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term]
vs' forall a b. (a -> b) -> a -> b
$ \Term
v -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> Term -> Term -> TCMT IO Bool
checkParallelReductionStep Type
b Term
v Term
rhou) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.global" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ TCMT IO Doc
"Global confluence: checking if" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
        , TCMT IO Doc
"reduces to" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
w , TCMT IO Doc
"in one parallel step." ]
      forall (m :: * -> *) a.
Monad m =>
ListT m a -> (a -> m Bool) -> m Bool
anyListT (forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Term
u) forall a b. (a -> b) -> a -> b
$ \Term
v -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.global" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u , TCMT IO Doc
" reduces to " , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
          ]
        Bool
eq <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
v Term
w
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
eq forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.global" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
          [ TCMT IO Doc
"  which is equal to" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
w
          ]
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
eq


sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol QName
f = do
    [RewriteRule]
rules <- forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over Lens' RewriteRuleMap Signature
sigRewriteRules forall a b. (a -> b) -> a -> b
$ 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 <- forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (RewriteRule -> QName
rewName forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** RewriteRule -> QName
rewName) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
                   forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (\RewriteRule
r1 RewriteRule
r2 -> (RewriteRule -> QName
rewName RewriteRule
r1,RewriteRule -> QName
rewName RewriteRule
r2) forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (QName, QName)
ordPairs) [RewriteRule]
rs
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.sort" Nat
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sorted rules: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute Permutation
perm [RewriteRule]
rs)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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       = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | RewriteRule -> QName
rewHead RewriteRule
r1 forall a. Eq a => a -> a -> Bool
/= RewriteRule -> QName
rewHead RewriteRule
r2 = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | Bool
otherwise                = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (RewriteRule -> Telescope
rewContext RewriteRule
r2) forall a b. (a -> b) -> a -> b
$ do
          Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewHead RewriteRule
r1
          (Type
t, Elims -> Term
hd) <- forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def (RewriteRule -> Type
rewType RewriteRule
r2)
          (Elims
vs :: Elims) <- forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm forall a b. (a -> b) -> a -> b
$ RewriteRule -> PElims
rewPats RewriteRule
r2
          Bool
res <- forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (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)
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
res forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.sort" Nat
55 forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"the lhs of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
r1) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            TCMT IO Doc
"is more general than the lhs of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
r2)
          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 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(a
x,a
y) -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ (a
y,a
x) 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 <- forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
ch Type
a
    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 -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
proj } -> do
    let f :: QName
f          = Projection -> QName
projOrig Projection
proj
        r :: QName
r          = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ Projection -> Arg QName
projFromType Projection
proj
    Type
rtype <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
    TelV Telescope
ptel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
rtype
    Nat
n <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
    let pars :: Args
        pars :: Args
pars = forall a. Subst a => Nat -> a -> a
raise (Nat
n forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Telescope
ptel) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
ptel
    Type
ftype <- Definition -> Type
defType Definition
def forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
    forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ftype , QName -> Elims -> Term
Def QName
f)
  Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> Type
defType Definition
def , QName -> Elims -> Term
Def forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)

sameRuleName :: RewriteRule -> RewriteRule -> Bool
sameRuleName :: RewriteRule -> RewriteRule -> Bool
sameRuleName = forall a. Eq a => a -> a -> 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 = forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eConflComputingOverlap forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f)
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    err :: TCErr
err@TypeError{} -> do
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Unification failed with error: "
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    TCErr
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
`ifNoConstraints` forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ProblemId
pid Maybe a
_ -> do
    Constraints
cs <- forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
    [Doc]
prettyCs <- forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
    forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Doc] -> Warning
RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
prettyCs
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.parreduce" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead (Elims -> Term
hd [])
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.parreduce" Nat
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: head symbol" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 <- forall (m :: * -> *) (t :: * -> *) a.
(MonadPlus m, Foldable t) =>
m (t a) -> m a
scatterMP (forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f)
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.parreduce" Nat
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: trying rule" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
  -- Don't reduce if underapplied
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es forall a. Ord a => a -> a -> Bool
>= forall (t :: * -> *) a. Foldable t => t a -> Nat
length PElims
ps
  let (Elims
es0 , Elims
es1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length PElims
ps) Elims
es
  forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (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) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Matching failed: no reduction
    Left Blocked_
block -> forall (f :: * -> *) a. Alternative f => f a
empty
    -- Matching succeeded
    Right Substitution
sub -> do
      let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution
sub) forall a b. (a -> b) -> a -> b
$ [Nat
0..(forall a. Sized a => a -> Nat
size Telescope
gammaforall a. Num a => a -> a -> a
-Nat
1)]
      Substitution
sub' <- forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce [Term]
vs
      Elims
es1' <- forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
es1
      let w :: Term
w = (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub' Term
rhs) forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1'
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.parreduce" Nat
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions: rewrote" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd Elims
es) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
w
      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) -> (forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (QName -> Elims -> Term
Def QName
f) Elims
es) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (QName -> Elims -> Term
Def QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Elims
es)
    (Con ConHead
c ConInfo
ci Elims
es) -> (forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
es) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Dom Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Abs Type
b
    Sort Sort
s   -> Sort -> Term
Sort  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce Sort
s

    -- Base cases
    u :: Term
u@Lit{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Level{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
u -- TODO: is this fine?
    u :: Term
u@DontCare{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    u :: Term
u@Dummy{}    -> 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{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

instance (Free a, Subst a, ParallelReduce a) => ParallelReduce (Abs a) where
  parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs a -> m (Abs a)
parReduce = forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction HasCallStack => Dom Type
__DUMMY_DOM__ 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
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM ([MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas [MetaId]
ms) forall a b. (a -> b) -> a -> b
$ \[MetaId]
ms' -> do

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

    -- Construct telescope (still containing the metas)
    let n :: Nat
n     = forall a. Sized a => a -> Nat
size [MetaId]
ms'
        gamma :: Telescope
gamma = Nat -> [String] -> [Dom Type] -> Telescope
unflattenTel' Nat
n [String]
ns forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Dom a
defaultDom [Type]
as

    -- Replace metas by variables
    let metaIndex :: MetaId -> Maybe Nat
metaIndex MetaId
x = (Nat
nforall a. Num a => a -> a -> a
-Nat
1forall a. Num a => a -> a -> a
-) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => a -> [a] -> Maybe Nat
elemIndex MetaId
x [MetaId]
ms'
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (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 -> 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 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
_         -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

ohAddBV :: ArgName -> Dom Type -> OneHole a -> OneHole a
ohAddBV :: forall a. String -> Dom Type -> OneHole a -> OneHole a
ohAddBV String
x Dom Type
a OneHole a
oh = OneHole a
oh { ohBoundVars :: Telescope
ohBoundVars = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs String
x forall a b. (a -> b) -> a -> b
$ 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_ = 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 = forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return 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
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.eta" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Forcing" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v , 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 <- forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Type
newTypeMeta_
    Type
cod <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
dom forall a b. (a -> b) -> a -> b
$ TCMT IO Type
newTypeMeta_
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi ((String
"x",) 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 = forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0]

    -- Continue with remaining eliminations
    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
dom forall a b. (a -> b) -> a -> b
$ forall a. String -> Dom Type -> OneHole a -> OneHole a
ohAddBV String
"x" Dom Type
dom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Abs Term -> Term
Lam ArgInfo
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs String
"x") forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      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
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.eta" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Forcing" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v , TCMT IO Doc
":" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a , TCMT IO Doc
"to be projectible by" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f ]
    QName
r <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe QName)
getRecordOfField QName
f
    Definition
rdef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
    let ra :: Type
ra = Definition -> Type
defType Definition
rdef
    Args
pars <- forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta Type
ra
    Sort
s <- Type
ra forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
s -> forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
s forall (m :: * -> *) a. Monad m => a -> m a
return forall a. HasCallStack => a
__IMPOSSIBLE__
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort
s (QName -> Elims -> Term
Def QName
r forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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) <- 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        = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
rdef
        i :: Nat
i         = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Eq a => a -> [a] -> Maybe Nat
elemIndex QName
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg QName]
fs
        fContent :: Term
fContent  = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Args
fields forall a. [a] -> Nat -> Maybe a
!!! Nat
i
        fUpdate :: Term -> Term
fUpdate Term
w = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. Nat -> (a -> a) -> [a] -> [a]
updateAt Nat
i (Term
w 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))) <- forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
    let fa :: Type
fa = Abs Type
c forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
v

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

  IApply{} -> 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg p
x forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles (forall t e. Dom' t e -> e
unDom PType (Arg p)
a) (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Dom p
x forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles PType (Dom p)
a (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 = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> String
absName Abs Term
x , Dom Type
dom) forall a b. (a -> b) -> a -> b
$
    forall a. String -> Dom Type -> OneHole a -> OneHole a
ohAddBV (forall a. Abs a -> String
absName Abs Type
a) Dom Type
dom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> String
absName Abs Term
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles (forall a. Subst a => Abs a -> a
absBody Abs Type
a) (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 = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> String
absName Abs Type
a , PType (Abs Type)
dom) forall a b. (a -> b) -> a -> b
$
    forall a. String -> Dom Type -> OneHole a -> OneHole a
ohAddBV (forall a. Abs a -> String
absName Abs Type
a) PType (Abs Type)
dom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> String
absName Abs Type
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ (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) [] = forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles (Type
a,Elims -> Term
hd) (Elim' Term
e:Elims
es) = do
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.hole" Nat
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Head symbol" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Elims -> Term
hd []) , TCMT IO Doc
":" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
      , TCMT IO Doc
"is eliminated by" , 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) <- forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        let a' :: Type
a'  = Abs Type
c forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` forall e. Arg e -> e
unArg Arg Term
x
            hd' :: Elims -> Term
hd' = Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term
eforall a. a -> [a] -> [a]
:)
        (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. a -> [a] -> [a]
:Elims
es) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Arg a -> Elim' a
Apply) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles Dom Type
b Arg Term
x)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Elim' Term
eforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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))) <- forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        let a' :: Type
a' = Abs Type
c forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Elims -> Term
hd []
        Elims -> Term
hd' <- forall t. Apply t => t -> Elims -> t
applyE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (forall t a. Dom' t a -> Arg a
argFromDom Dom Type
b forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Elims -> Term
hd [])
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Elim' Term
eforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> forall (f :: * -> *) a. Alternative f => f a
empty -- TODO: support --confluence-check + --cubical

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) = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t a. Sort' t -> a -> Type'' t a
El Sort
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.confluence.hole" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ TCMT IO Doc
"Getting holes of term" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u , TCMT IO Doc
":" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PType Term
a ]
    case Term
u of
      Var Nat
i Elims
es       -> do
        Type
ai <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Nat -> Elims -> Term
Var Nat
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) <- forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce PType Term
a
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Abs Term -> Term
Lam ArgInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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          -> forall (f :: * -> *) a. Alternative f => f a
empty
      v :: Term
v@(Def QName
f Elims
es)   -> do
        Type
fa <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term -> OneHole Term
idHole PType Term
a Term
v)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Elims -> Term
Def QName
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce PType Term
a
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term -> OneHole Term
idHole PType Term
a Term
v)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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         ->
        (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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Dom Type
a) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        (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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles Dom Type
a Abs Type
b)
      Sort Sort
s         -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Sort
s
      Level Level
l        -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Term
Level forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
      MetaV{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
      DontCare{}     -> forall (f :: * -> *) a. Alternative f => f a
empty
      Dummy{}        -> 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       -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
    Prop Level
l       -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
    Inf IsFibrant
f Integer
n      -> forall (f :: * -> *) a. Alternative f => f a
empty
    SSet Level
l       -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
    Sort
SizeUniv     -> forall (f :: * -> *) a. Alternative f => f a
empty
    Sort
LockUniv     -> forall (f :: * -> *) a. Alternative f => f a
empty
    Sort
IntervalUniv -> forall (f :: * -> *) a. Alternative f => f a
empty
    PiSort{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    FunSort{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    UnivSort{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaS{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    DefS QName
f Elims
es    -> do
      Type
fa <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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{}     -> 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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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]
_ []     = forall (f :: * -> *) a. Alternative f => f a
empty
  allHoles PType [PlusLevel' Term]
_ (PlusLevel' Term
l:[PlusLevel' Term]
ls) =
    (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> [a] -> [a]
:[PlusLevel' Term]
ls) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, PType p ~ ()) =>
p -> m (OneHole p)
allHoles_ PlusLevel' Term
l)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlusLevel' Term
lforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (m :: * -> *). HasBuiltins m => m Type
levelType'
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
PType p -> p -> m (OneHole p)
allHoles Type
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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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   String
i a
x) = forall a. String -> a -> Abs a
Abs String
i   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x)
  metasToVars (NoAbs String
i a
x) = forall a. String -> a -> Abs a
NoAbs String
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Term
u
    Lit Literal
l      -> 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    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Dom Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s
    Level Level
l    -> Level -> Term
Level    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    MetaV MetaId
x Elims
es -> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall a b. (a -> b) -> a -> b
$ MetaId
x) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Nat
i   -> Nat -> Elims -> Term
Var Nat
i    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DontCare Term
u -> Term -> Term
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Term
u
    Dummy String
s Elims
es -> String -> Elims -> Term
Dummy String
s  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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     -> forall t. Level' t -> Sort' t
Type     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Prop Level
l     -> forall t. Level' t -> Sort' t
Prop     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Inf IsFibrant
f Integer
n    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    SSet Level
l     -> forall t. Level' t -> Sort' t
SSet     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Level
l
    Sort
SizeUniv   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall t. Sort' t
SizeUniv
    Sort
LockUniv   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall t. Sort' t
LockUniv
    Sort
IntervalUniv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall t. Sort' t
IntervalUniv
    PiSort Dom' Term Term
s Sort
t Abs Sort
u -> forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Dom' Term Term
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Abs Sort
u
    FunSort Sort
s Sort
t -> forall t. Sort' t -> Sort' t -> Sort' t
FunSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
t
    UnivSort Sort
s -> forall t. Sort' t -> Sort' t
UnivSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Sort
s
    MetaS MetaId
x Elims
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DefS QName
f Elims
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars Elims
es
    DummyS String
s   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall t. String -> Sort' t
DummyS String
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) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Tele a
EmptyTel
  metasToVars (ExtendTel a
a Abs (Tele a)
tel) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = (,,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars c
z forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
 HasBuiltins m) =>
a -> m a
metasToVars d
w