{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NondecreasingIndentation #-}
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 ( 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.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
checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses ConfluenceCheck
confChk QName
f = do
rews <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getClausesAsRewriteRules QName
f
let noMetasInPats RewriteRule
rew
| PElims -> Bool
forall a. AllMetas a => a -> Bool
noMetas (RewriteRule -> PElims
rewPats RewriteRule
rew) = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| Bool
otherwise = Bool
False Bool -> TCM () -> TCMT IO Bool
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Warning
ConfluenceCheckingIncompleteBecauseOfMeta QName
f
rews <- filterM noMetasInPats rews
let matchables = (RewriteRule -> [QName]) -> [RewriteRule] -> [[QName]]
forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [RewriteRule]
rews
reportSDoc "rewriting.confluence" 30 $
"Function" <+> prettyTCM f <+> "has matchable symbols" <+> prettyList_ (map prettyTCM matchables)
modifySignature $ setMatchableSymbols f $ concat matchables
let hasRules QName
g = Bool -> Bool
not (Bool -> Bool) -> ([RewriteRule] -> Bool) -> [RewriteRule] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RewriteRule] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([RewriteRule] -> Bool) -> f [RewriteRule] -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
g
forM_ (zip rews matchables) $ \(RewriteRule
rew,[QName]
ms) ->
TCMT IO [QName] -> ([QName] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM ((QName -> TCMT IO Bool) -> [QName] -> TCMT IO [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM QName -> TCMT IO Bool
forall {f :: * -> *}. HasConstInfo f => QName -> f Bool
hasRules [QName]
ms) (([QName] -> TCM ()) -> TCM ()) -> ([QName] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \[QName]
_ -> do
ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [RewriteRule
rew]
checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [RewriteRule]
rews = TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConfluenceCheck
confChk ConfluenceCheck -> ConfluenceCheck -> Bool
forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
let getSymbols :: RewriteRule -> f (Set QName)
getSymbols RewriteRule
rew = let f :: QName
f = RewriteRule -> QName
rewHead RewriteRule
rew in
(QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
f) (Set QName -> Set QName)
-> (Definition -> Set QName) -> Definition -> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Set QName
defMatchable (Definition -> Set QName) -> f Definition -> f (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
allSymbols <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Set QName -> [QName])
-> ([Set QName] -> Set QName) -> [Set QName] -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set QName] -> Set QName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set QName] -> [QName]) -> TCMT IO [Set QName] -> TCMT IO [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RewriteRule -> TCMT IO (Set QName))
-> [RewriteRule] -> TCMT IO [Set QName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse RewriteRule -> TCMT IO (Set QName)
forall {f :: * -> *}.
HasConstInfo f =>
RewriteRule -> f (Set QName)
getSymbols [RewriteRule]
rews
forM_ allSymbols $ \QName
f -> do
rewsf <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f
forM_ rewsf $ \RewriteRule
rew -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.triangle" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"(re)checking triangle property for rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
RewriteRule -> TCM ()
checkTrianglePropertyForRule RewriteRule
rew
[[RewriteRule]] -> ([RewriteRule] -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([RewriteRule] -> [[RewriteRule]]
forall a. [a] -> [[a]]
tails [RewriteRule]
rews) (([RewriteRule] -> TCM ()) -> TCM ())
-> ([RewriteRule] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
-> (RewriteRule -> [RewriteRule] -> TCM ())
-> [RewriteRule]
-> TCM ()
forall b a. b -> (a -> [a] -> b) -> [a] -> b
listCase (() -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((RewriteRule -> [RewriteRule] -> TCM ())
-> [RewriteRule] -> TCM ())
-> (RewriteRule -> [RewriteRule] -> TCM ())
-> [RewriteRule]
-> TCM ()
forall a b. (a -> b) -> a -> b
$ \RewriteRule
rew [RewriteRule]
rewsRest -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew)
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> RewriteRule -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => RewriteRule -> 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
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
(fa , hdf) <- addContext tel $ makeHead def (rewType rew)
reportSDoc "rewriting.confluence" 30 $ addContext tel $
"Head symbol" <+> prettyTCM (hdf []) <+> "of rewrite rule has type" <+> prettyTCM fa
forMM_ (getAllRulesFor f) $ \ RewriteRule
rew' -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') (RewriteRule
rewRewriteRule -> [RewriteRule] -> [RewriteRule]
forall a. a -> [a] -> [a]
:[RewriteRule]
rewsRest) Bool -> Bool -> Bool
||
(RewriteRule -> Bool
rewFromClause RewriteRule
rew Bool -> Bool -> Bool
&& RewriteRule -> Bool
rewFromClause RewriteRule
rew')) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
(Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hdf RewriteRule
rew RewriteRule
rew'
reportSDoc "rewriting.confluence" 30 $ "Finished step 1 of confluence check of rule" <+> prettyTCM (rewName rew)
es <- nlPatToTerm qs
forMM_ (addContext tel $ allHolesList (fa, hdf) es) $ \ OneHole Elims
hole -> do
let g :: QName
g = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
hdg :: Elims -> Term
hdg = OneHole Elims -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole Elims
hole
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Found hole with head symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
g
rews' <- QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g
forM_ rews' $ \RewriteRule
rew' -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
(Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew RewriteRule
rew' OneHole Elims
hole
reportSDoc "rewriting.confluence" 30 $ "Finished step 2 of confluence check of rule" <+> prettyTCM (rewName rew)
forM_ (defMatchable def) $ \ QName
g -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
g TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"has rules that match on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ (QName -> TCMT IO [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
g) ((RewriteRule -> TCM ()) -> TCM ())
-> (RewriteRule -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ RewriteRule
rew' -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
rew') [RewriteRule]
rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
es' <- PElims -> TCMT IO Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm (RewriteRule -> PElims
rewPats RewriteRule
rew')
let tel' = RewriteRule -> Telescope
rewContext RewriteRule
rew'
def' <- getConstInfo g
(ga , hdg) <- addContext tel' $ makeHead def' (rewType rew')
forMM_ (addContext tel' $ allHolesList (ga , hdg) es') $ \ OneHole Elims
hole -> do
let f' :: QName
f' = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdg Elims -> Term
hdf RewriteRule
rew' RewriteRule
rew OneHole Elims
hole
reportSDoc "rewriting.confluence" 30 $ "Finished step 3 of confluence check of rule" <+> prettyTCM (rewName rew)
where
checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
checkConfluenceTop Elims -> Term
hd RewriteRule
rew1 RewriteRule
rew2 =
Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
sub1 <- Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew1
sub2 <- makeMetaSubst $ rewContext rew2
let f = RewriteRule -> QName
rewHead RewriteRule
rew1
a1 = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew1
a2 = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew2
es1 <- applySubst sub1 <$> nlPatToTerm (rewPats rew1)
es2 <- applySubst sub2 <$> nlPatToTerm (rewPats rew2)
reportSDoc "rewriting.confluence" 30 $ vcat
[ "checkConfluenceTop" <+> prettyTCM (rewName rew1) <+> prettyTCM (rewName rew2)
, " f = " <+> prettyTCM f
, " ctx1 = " <+> prettyTCM (rewContext rew1)
, " ctx2 = " <+> prettyTCM (rewContext rew2)
, " es1 = " <+> prettyTCM es1
, " es2 = " <+> prettyTCM es2
]
let n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es1) (Elims -> Int
forall a. Sized a => a -> Int
size Elims
es2)
(es1' , es1r) = splitAt n es1
(es2' , es2r) = splitAt n es2
esr = Elims
es1r Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es2r
lhs1 = Elims -> Term
hd (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es1' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
esr
lhs2 = Elims -> Term
hd (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es2' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
esr
a | Elims -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Elims
es1r = Type
a2
| Bool
otherwise = Type
a1
reportSDoc "rewriting.confluence" 20 $ sep
[ "Considering potential critical pair at top-level: "
, nest 2 $ prettyTCM $ lhs1, " =?= "
, nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
]
maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
fa <- defType <$> getConstInfo f
fpol <- getPolarity' CmpEq f
onlyReduceTypes $
compareElims fpol [] fa (hd []) es1' es2'
let rhs1 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (RewriteRule -> Term
rewRHS RewriteRule
rew1) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es2r
rhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r
return (rhs1 , rhs2)
whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hd (es1' ++ esr))
checkConfluenceSub :: (Elims -> Term) -> (Elims -> Term) -> RewriteRule -> RewriteRule -> OneHole Elims -> TCM ()
checkConfluenceSub :: (Elims -> Term)
-> (Elims -> Term)
-> RewriteRule
-> RewriteRule
-> OneHole Elims
-> TCM ()
checkConfluenceSub Elims -> Term
hdf Elims -> Term
hdg RewriteRule
rew1 RewriteRule
rew2 OneHole Elims
hole0 = do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"foo 2" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2)
Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> QName -> Call
CheckConfluence (RewriteRule -> QName
rewName RewriteRule
rew1) (RewriteRule -> QName
rewName RewriteRule
rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Checking confluence of rules" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
"and" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (RewriteRule -> QName
rewName RewriteRule
rew2) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"at subpattern position"
sub1 <- Telescope -> TCMT IO Substitution
forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst (Telescope -> TCMT IO Substitution)
-> Telescope -> TCMT IO Substitution
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Telescope
rewContext RewriteRule
rew1
let bvTel0 = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole0
k = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
bvTel0
b0 = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
k Substitution
sub1) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Type
forall a. OneHole a -> Type
ohType OneHole Elims
hole0
g = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole0
es0 = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
k Substitution
sub1) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ OneHole Elims -> Elims
forall a. OneHole a -> Elims
ohElims OneHole Elims
hole0
qs2 = RewriteRule -> PElims
rewPats RewriteRule
rew2
let isIApply IApply{} = Bool
True
isIApply Elim' a
_ = Bool
False
unless (any isIApply $ drop (size es0) qs2) $ do
hole1 <- addContext bvTel0 $
forceEtaExpansion b0 (hdg es0) $ drop (size es0) qs2
verboseS "rewriting.confluence.eta" 30 $
unless (size es0 == size qs2) $
addContext bvTel0 $
reportSDoc "rewriting.confluence.eta" 30 $ vcat
[ "forceEtaExpansion result:"
, nest 2 $ "bound vars: " <+> prettyTCM (ohBoundVars hole1)
, nest 2 $ "hole contents: " <+> addContext (ohBoundVars hole1) (prettyTCM $ ohContents hole1)
]
let hole = OneHole Term
hole1 OneHole Term -> OneHole Elims -> OneHole Elims
forall a. OneHole Term -> OneHole a -> OneHole a
`composeHole` OneHole Elims
hole0
g = OneHole Elims -> QName
forall a. OneHole a -> QName
ohHeadName OneHole Elims
hole
es' = OneHole Elims -> Elims
forall a. OneHole a -> Elims
ohElims OneHole Elims
hole
bvTel = OneHole Elims -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Elims
hole
plug = OneHole Elims -> Term -> Elims
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Elims
hole
sub2 <- addContext bvTel $ makeMetaSubst $ rewContext rew2
let es1 = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
bvTel) Substitution
sub1) Elims
es'
es2 <- applySubst sub2 <$> nlPatToTerm (rewPats rew2)
when (size es1 < size es2) __IMPOSSIBLE__
let n = Elims -> Int
forall a. Sized a => a -> Int
size Elims
es2
(es1' , es1r) = splitAt n es1
let lhs1 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg Elims
es1
lhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug (Term -> Elims) -> Term -> Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdg (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims
es2 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1r
a = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sub1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Type
rewType RewriteRule
rew1
reportSDoc "rewriting.confluence" 20 $ sep
[ "Considering potential critical pair at subpattern: "
, nest 2 $ prettyTCM $ lhs1 , " =?= "
, nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
]
maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
ga <- defType <$> getConstInfo g
gpol <- getPolarity' CmpEq g
onlyReduceTypes $ addContext bvTel $
compareElims gpol [] ga (hdg []) es1' es2
let rhs1 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ RewriteRule -> Term
rewRHS RewriteRule
rew1
let w = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub2 (RewriteRule -> Term
rewRHS RewriteRule
rew2) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1r
reportSDoc "rewriting.confluence" 30 $ sep
[ "Plugging hole with w = "
, nest 2 $ addContext bvTel $ prettyTCM w
]
let rhs2 = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
hdf (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Elims
plug Term
w
return (rhs1 , rhs2)
whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hdf (applySubst sub1 $ plug $ hdg es1))
checkCriticalPair
:: Type
-> (Elims -> Term)
-> Elims
-> Term
-> Term
-> TCM ()
checkCriticalPair :: Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
checkCriticalPair Type
a Elims -> Term
hd Elims
es Term
rhs1 Term
rhs2 = do
(a,es,rhs1,rhs2) <- (Type, Elims, Term, Term) -> TCMT IO (Type, Elims, Term, Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type
a,Elims
es,Term
rhs1,Term
rhs2)
let ms = Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Type, Elims, Term, Term) -> Set MetaId
forall m.
Monoid m =>
(MetaId -> m) -> (Type, Elims, Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton ((Type, Elims, Term, Term) -> Set MetaId)
-> (Type, Elims, Term, Term) -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (Type
a,Elims
es,Term
rhs1,Term
rhs2)
reportSDoc "rewriting.confluence" 30 $ sep
[ "Abstracting over metas: "
, prettyList_ (map (text . show) ms)
]
(gamma , (a,es,rhs1,rhs2)) <- fromMaybe __IMPOSSIBLE__ <$>
abstractOverMetas ms (a,es,rhs1,rhs2)
addContext gamma $ reportSDoc "rewriting.confluence" 10 $ sep
[ "Found critical pair: "
, nest 2 $ prettyTCM (hd es)
, " ---> " , nest 2 $ prettyTCM rhs1
, " =?= " , nest 2 $ prettyTCM rhs2
, " : " , nest 2 $ prettyTCM a ]
reportSDoc "rewriting.confluence" 30 $ do
gamma <- instantiateFull gamma
sep [ "Context of critical pair: "
, nest 2 $ prettyTCM gamma ]
addContext gamma $ case confChk of
ConfluenceCheck
LocalConfluenceCheck -> do
TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
rhs1 Term
rhs2
TCM () -> (TCErr -> TCM ()) -> TCM ()
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
TypeError CallStack
_ TCState
s Closure TypeError
err -> do
prettyErr <- (TCState -> TCState) -> TCMT IO Doc -> TCMT IO Doc
forall a. (TCState -> TCState) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure TypeError -> m Doc
prettyTCM Closure TypeError
err
warning $ RewriteNonConfluent (hd es) rhs1 rhs2 prettyErr
TCErr
err -> TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
ConfluenceCheck
GlobalConfluenceCheck -> do
(f, t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
forall a. a -> Maybe a -> a
fromMaybe (QName, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
-> TCMT IO (Maybe (QName, Type)) -> TCMT IO (QName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe (QName, Type))
forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead (Elims -> Term
hd [])
let checkEqualLHS :: RewriteRule -> TCM Bool
checkEqualLHS (RewriteRule QName
q Telescope
delta QName
_ PElims
ps Term
_ Type
_ Bool
_) = do
TCMT IO (Either Blocked_ Substitution)
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (Telescope
-> TypeOf Elims
-> PElims
-> Elims
-> TCMT IO (Either Blocked_ Substitution)
forall (m :: * -> *) a b.
(PureTCM m, Match a b) =>
Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
nonLinMatch Telescope
delta (Type
t , Elims -> Term
hd) PElims
ps Elims
es) TCMT IO (Either Blocked_ Substitution)
-> (Either Blocked_ Substitution -> TCMT IO Bool) -> TCMT IO Bool
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left Blocked_
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Right Substitution
sub -> do
let us :: [Term]
us = Substitution' (SubstArg [Term]) -> [Term] -> [Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Term])
sub ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta
as :: [Dom Type]
as = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom Type])
sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Elims -> Term
hd Elims
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is an instance of the LHS of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with instantiation" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM [Term]
us)
ok <- [(Term, Dom Type)] -> TCMT IO Bool
allDistinctVars ([(Term, Dom Type)] -> TCMT IO Bool)
-> [(Term, Dom Type)] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ [Term] -> [Dom Type] -> [(Term, Dom Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
us [Dom Type]
as
when ok $ reportSDoc "rewriting.confluence.global" 30 $
"It is equal to the LHS of rewrite rule" <+> prettyTCM q
return ok
allDistinctVars :: [(Term,Dom Type)] -> TCM Bool
allDistinctVars [(Term, Dom Type)]
us = do
us' <- ((Term, Dom Type) -> TCMT IO Bool)
-> [(Term, Dom Type)] -> TCMT IO [(Term, Dom Type)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not (Bool -> Bool)
-> ((Term, Dom Type) -> TCMT IO Bool)
-> (Term, Dom Type)
-> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Dom Type -> TCMT IO Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM (Dom Type -> TCMT IO Bool)
-> ((Term, Dom Type) -> Dom Type)
-> (Term, Dom Type)
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Dom Type) -> Dom Type
forall a b. (a, b) -> b
snd) [(Term, Dom Type)]
us
mis <- traverse (\(Term
u,Dom Type
a) -> Term -> Type -> TCMT IO (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
u (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) $ us'
case sequence mis of
Just [Int]
is -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Int]
is
Maybe [Int]
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
rews <- getAllRulesFor f
let sameRHS = TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
rhs1 Term
rhs2
unlessM (sameRHS `or2M` anyM rews checkEqualLHS) $ addContext gamma $
warning $ RewriteAmbiguousRules (hd es) rhs1 rhs2
checkTrianglePropertyForRule :: RewriteRule -> TCM ()
checkTrianglePropertyForRule :: RewriteRule -> TCM ()
checkTrianglePropertyForRule (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
b Bool
c) = Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
u <- NLPat -> TCMT IO Term
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm (NLPat -> TCMT IO Term) -> NLPat -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> PElims -> NLPat
PDef QName
f PElims
ps
(rhou,vs) <- fromMaybe __IMPOSSIBLE__ . uncons <$> allParallelReductions u
reportSDoc "rewriting.confluence" 40 $ ("rho(" <> prettyTCM u <> ") =") <+> prettyTCM rhou
reportSDoc "rewriting.confluence" 40 $ ("S(" <> prettyTCM u <> ") =") <+> prettyList_ (map prettyTCM vs)
caseMaybe (initLast vs) (return ()) $ \([Term]
vs',Term
u') -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
u') TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
[Term] -> (Term -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term]
vs' ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Term
v -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> Term -> Term -> TCMT IO Bool
checkParallelReductionStep Type
b Term
v Term
rhou) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Warning
RewriteMissingRule Term
u Term
v Term
rhou
checkParallelReductionStep :: Type -> Term -> Term -> TCM Bool
checkParallelReductionStep :: Type -> Term -> Term -> TCMT IO Bool
checkParallelReductionStep Type
a Term
u Term
w = do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"Global confluence: checking if" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
, TCMT IO Doc
"reduces to" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
w , TCMT IO Doc
"in one parallel step." ]
ListT (TCMT IO) Term -> (Term -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) a.
Monad m =>
ListT m a -> (a -> m Bool) -> m Bool
anyListT (Term -> ListT (TCMT IO) Term
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Term -> m Term
parReduce Term
u) ((Term -> TCMT IO Bool) -> TCMT IO Bool)
-> (Term -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \Term
v -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.global" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u , TCMT IO Doc
" reduces to " , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
]
eq <- TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
v Term
w
when eq $ reportSDoc "rewriting.confluence.global" 30 $ fsep
[ " which is equal to" , prettyTCM w
]
return eq
sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol :: QName -> TCM ()
sortRulesOfSymbol QName
f = do
rules <- [RewriteRule] -> TCMT IO [RewriteRule]
forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules ([RewriteRule] -> TCMT IO [RewriteRule])
-> TCMT IO [RewriteRule] -> TCMT IO [RewriteRule]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f
modifySignature $ over sigRewriteRules $ HMap.insert f rules
where
sortRules :: PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules :: forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
sortRules [RewriteRule]
rs = do
ordPairs <- Set (QName, QName) -> Set (QName, QName)
forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops (Set (QName, QName) -> Set (QName, QName))
-> ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
-> [(RewriteRule, RewriteRule)]
-> Set (QName, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(QName, QName)] -> Set (QName, QName)
forall a. Ord a => [a] -> Set a
Set.fromList ([(QName, QName)] -> Set (QName, QName))
-> ([(RewriteRule, RewriteRule)] -> [(QName, QName)])
-> [(RewriteRule, RewriteRule)]
-> Set (QName, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RewriteRule, RewriteRule) -> (QName, QName))
-> [(RewriteRule, RewriteRule)] -> [(QName, QName)]
forall a b. (a -> b) -> [a] -> [b]
map (RewriteRule -> QName
rewName (RewriteRule -> QName)
-> (RewriteRule -> QName)
-> (RewriteRule, RewriteRule)
-> (QName, QName)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** RewriteRule -> QName
rewName) ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
-> m [(RewriteRule, RewriteRule)] -> m (Set (QName, QName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
((RewriteRule, RewriteRule) -> m Bool)
-> [(RewriteRule, RewriteRule)] -> m [(RewriteRule, RewriteRule)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((RewriteRule -> RewriteRule -> m Bool)
-> (RewriteRule, RewriteRule) -> m Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((RewriteRule -> RewriteRule -> m Bool)
-> (RewriteRule, RewriteRule) -> m Bool)
-> (RewriteRule -> RewriteRule -> m Bool)
-> (RewriteRule, RewriteRule)
-> m Bool
forall a b. (a -> b) -> a -> b
$ (RewriteRule -> RewriteRule -> m Bool)
-> RewriteRule -> RewriteRule -> m Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip RewriteRule -> RewriteRule -> m Bool
forall (m :: * -> *).
PureTCM m =>
RewriteRule -> RewriteRule -> m Bool
moreGeneralLHS) [(RewriteRule
r1,RewriteRule
r2) | RewriteRule
r1 <- [RewriteRule]
rs, RewriteRule
r2 <- [RewriteRule]
rs]
let perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$
(RewriteRule -> RewriteRule -> Bool)
-> [RewriteRule] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (\RewriteRule
r1 RewriteRule
r2 -> (RewriteRule -> QName
rewName RewriteRule
r1,RewriteRule -> QName
rewName RewriteRule
r2) (QName, QName) -> Set (QName, QName) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (QName, QName)
ordPairs) [RewriteRule]
rs
reportSDoc "rewriting.confluence.sort" 50 $ "sorted rules: " <+>
prettyList_ (map (prettyTCM . rewName) $ permute perm rs)
return $ permute perm rs
moreGeneralLHS :: PureTCM m => RewriteRule -> RewriteRule -> m Bool
moreGeneralLHS :: forall (m :: * -> *).
PureTCM m =>
RewriteRule -> RewriteRule -> m Bool
moreGeneralLHS RewriteRule
r1 RewriteRule
r2
| RewriteRule -> RewriteRule -> Bool
sameRuleName RewriteRule
r1 RewriteRule
r2 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| RewriteRule -> QName
rewHead RewriteRule
r1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= RewriteRule -> QName
rewHead RewriteRule
r2 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise = Telescope -> m Bool -> m Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (RewriteRule -> Telescope
rewContext RewriteRule
r2) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (QName -> m Definition) -> QName -> m Definition
forall a b. (a -> b) -> a -> b
$ RewriteRule -> QName
rewHead RewriteRule
r1
(t, hd) <- makeHead def (rewType r2)
(vs :: Elims) <- nlPatToTerm $ rewPats r2
res <- isRight <$> onlyReduceTypes (nonLinMatch (rewContext r1) (t, hd) (rewPats r1) vs)
when res $ reportSDoc "rewriting.confluence.sort" 55 $
"the lhs of " <+> prettyTCM (rewName r1) <+>
"is more general than the lhs of" <+> prettyTCM (rewName r2)
return res
deleteLoops :: Ord a => Set (a,a) -> Set (a,a)
deleteLoops :: forall a. Ord a => Set (a, a) -> Set (a, a)
deleteLoops Set (a, a)
xs = ((a, a) -> Bool) -> Set (a, a) -> Set (a, a)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(a
x,a
y) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (a
y,a
x) (a, a) -> Set (a, a) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (a, a)
xs) Set (a, a)
xs
makeHead :: PureTCM m => Definition -> Type -> m (Type , Elims -> Term)
makeHead :: forall (m :: * -> *).
PureTCM m =>
Definition -> Type -> m (Type, Elims -> Term)
makeHead Definition
def Type
a = case Definition -> Defn
theDef Definition
def of
Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
ch } -> do
ca <- ((QName, Type, Args), Type) -> Type
forall a b. (a, b) -> b
snd (((QName, Type, Args), Type) -> Type)
-> (Maybe ((QName, Type, Args), Type)
-> ((QName, Type, Args), Type))
-> Maybe ((QName, Type, Args), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
forall a. a -> Maybe a -> a
fromMaybe ((QName, Type, Args), Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
-> m (Maybe ((QName, Type, Args), Type)) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
ch Type
a
return (ca , Con ch ConOSystem)
Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
proj } -> do
let f :: QName
f = Projection -> QName
projOrig Projection
proj
r :: QName
r = Arg QName -> QName
forall e. Arg e -> e
unArg (Arg QName -> QName) -> Arg QName -> QName
forall a b. (a -> b) -> a -> b
$ Projection -> Arg QName
projFromType Projection
proj
rtype <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
TelV ptel _ <- telView rtype
n <- getContextSize
let pars :: Args
pars = Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ptel) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
ptel
ftype <- defType def `piApplyM` pars
return (ftype , Def f)
Defn
_ -> (Type, Elims -> Term) -> m (Type, Elims -> Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> Type
defType Definition
def , QName -> Elims -> Term
Def (QName -> Elims -> Term) -> QName -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
def)
sameRuleName :: RewriteRule -> RewriteRule -> Bool
sameRuleName :: RewriteRule -> RewriteRule -> Bool
sameRuleName = QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) (QName -> QName -> Bool)
-> (RewriteRule -> QName) -> RewriteRule -> RewriteRule -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RewriteRule -> QName
rewName
getAllRulesFor :: (HasConstInfo m, MonadFresh NameId m) => QName -> m [RewriteRule]
getAllRulesFor :: forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getAllRulesFor QName
f = [RewriteRule] -> [RewriteRule] -> [RewriteRule]
forall a. [a] -> [a] -> [a]
(++) ([RewriteRule] -> [RewriteRule] -> [RewriteRule])
-> m [RewriteRule] -> m ([RewriteRule] -> [RewriteRule])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m [RewriteRule]
forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
getRewriteRulesFor QName
f m ([RewriteRule] -> [RewriteRule])
-> m [RewriteRule] -> m [RewriteRule]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> m [RewriteRule]
forall (m :: * -> *).
(HasConstInfo m, MonadFresh NameId m) =>
QName -> m [RewriteRule]
getClausesAsRewriteRules QName
f
makeMetaSubst :: (MonadMetaSolver m) => Telescope -> m Substitution
makeMetaSubst :: forall (m :: * -> *).
MonadMetaSolver m =>
Telescope -> m Substitution
makeMetaSubst Telescope
gamma = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution)
-> (Args -> [Term]) -> Args -> Substitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> (Args -> [Term]) -> Args -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> Substitution) -> m Args -> m Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Args
forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
newTelMeta Telescope
gamma
computingOverlap :: (MonadTCEnv m) => m a -> m a
computingOverlap :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap = Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eConflComputingOverlap ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True
tryUnification :: Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification :: forall a. Term -> Term -> TCM a -> TCM (Maybe a)
tryUnification Term
lhs1 Term
lhs2 TCM a
f = TCMT IO (Maybe a) -> TCMT IO (Maybe a)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
computingOverlap (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> TCM a -> TCMT IO (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f)
TCMT IO (Maybe a)
-> (TCErr -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
err :: TCErr
err@TypeError{} -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Unification failed with error: "
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
]
Maybe a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
TCErr
err -> TCErr -> TCMT IO (Maybe a)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
TCMT IO (Maybe a)
-> (Maybe a -> TCMT IO (Maybe a))
-> (ProblemId -> Maybe a -> TCMT IO (Maybe a))
-> TCMT IO (Maybe a)
forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
`ifNoConstraints` Maybe a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a))
-> (ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ \ProblemId
pid Maybe a
_ -> do
cs <- ProblemId -> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
prettyCs <- prettyInterestingConstraints cs
warning $ RewriteMaybeNonConfluent lhs1 lhs2 prettyCs
return Nothing
type MonadParallelReduce m =
( PureTCM m
, MonadFresh NameId m
)
allParallelReductions :: (MonadParallelReduce m, ParallelReduce a) => a -> m [a]
allParallelReductions :: forall (m :: * -> *) a.
(MonadParallelReduce m, ParallelReduce a) =>
a -> m [a]
allParallelReductions = ListT m a -> m [a]
forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT (ListT m a -> m [a]) -> (a -> ListT m a) -> a -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ListT m a
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce
class ParallelReduce a where
parReduce :: (MonadParallelReduce m, MonadPlus m) => a -> m a
default parReduce
:: ( MonadParallelReduce m, MonadPlus m
, Traversable f, a ~ f b, ParallelReduce b)
=> a -> m a
parReduce = (b -> m b) -> f b -> m (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse b -> m b
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
b -> m b
parReduce
topLevelReductions :: (MonadParallelReduce m, MonadPlus m) => (Elims -> Term) -> Elims -> m Term
topLevelReductions :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions Elims -> Term
hd Elims
es = do
VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.parreduce" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"topLevelReductions" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Elims -> Term
hd Elims
es)
(f , t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
forall a. a -> Maybe a -> a
fromMaybe (QName, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
-> m (Maybe (QName, Type)) -> m (QName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (Maybe (QName, Type))
forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
getTypedHead (Elims -> Term
hd [])
reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: head symbol" <+> prettyTCM (hd []) <+> ":" <+> prettyTCM t
RewriteRule q gamma _ ps rhs b c <- scatterMP (getAllRulesFor f)
reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: trying rule" <+> prettyTCM q
guard $ length es >= length ps
let (es0 , es1) = splitAt (length ps) es
onlyReduceTypes (nonLinMatch gamma (t,hd) ps es0) >>= \case
Left Blocked_
block -> m Term
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Right Substitution
sub -> do
let vs :: [Term]
vs = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution
sub) ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Int
0..(Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gammaInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
sub' <- [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> m [Term] -> m Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> m [Term]
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
[Term] -> m [Term]
parReduce [Term]
vs
es1' <- parReduce es1
let w = (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sub' Term
rhs) Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es1'
reportSDoc "rewriting.parreduce" 50 $ "topLevelReductions: rewrote" <+> prettyTCM (hd es) <+> "to" <+> prettyTCM w
return w
instance ParallelReduce Term where
parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Term -> m Term
parReduce = \case
(Def QName
f Elims
es) -> ((Elims -> Term) -> Elims -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (QName -> Elims -> Term
Def QName
f) Elims
es) m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (QName -> Elims -> Term
Def QName
f (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Elims -> m Elims
parReduce Elims
es)
(Con ConHead
c ConInfo
ci Elims
es) -> ((Elims -> Term) -> Elims -> m Term
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
(Elims -> Term) -> Elims -> m Term
topLevelReductions (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
es) m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Elims -> m Elims
parReduce Elims
es)
Lam ArgInfo
i Abs Term
u -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> m (Abs Term)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs Term -> m (Abs Term)
parReduce Abs Term
u
Var Int
x Elims
es -> Int -> Elims -> Term
Var Int
x (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Elims -> m Elims
parReduce Elims
es
Pi Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> Term
Pi (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Dom Type -> m (Dom Type)
parReduce Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs Type -> m (Abs Type)
parReduce Abs Type
b
Sort Sort
s -> Sort -> Term
Sort (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Sort -> m Sort
parReduce Sort
s
u :: Term
u@Lit{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
u :: Term
u@Level{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
u :: Term
u@DontCare{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
u :: Term
u@Dummy{} -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
MetaV{} -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__
instance ParallelReduce Sort where
parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Sort -> m Sort
parReduce = Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance ParallelReduce a => ParallelReduce (Arg a) where
instance ParallelReduce a => ParallelReduce (Dom a) where
instance ParallelReduce a => ParallelReduce (Type' a) where
instance ParallelReduce a => ParallelReduce [a] where
instance ParallelReduce a => ParallelReduce (Elim' a) where
parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Elim' a -> m (Elim' a)
parReduce (Apply Arg a
u) = Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a) -> m (Arg a) -> m (Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg a -> m (Arg a)
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Arg a -> m (Arg a)
parReduce Arg a
u
parReduce e :: Elim' a
e@Proj{} = Elim' a -> m (Elim' a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
parReduce e :: Elim' a
e@IApply{} = Elim' a -> m (Elim' a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
instance (Free a, Subst a, ParallelReduce a) => ParallelReduce (Abs a) where
parReduce :: forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
Abs a -> m (Abs a)
parReduce = Dom Type -> (a -> m a) -> Abs a -> m (Abs a)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ a -> m a
forall a (m :: * -> *).
(ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
a -> m a
forall (m :: * -> *).
(MonadParallelReduce m, MonadPlus m) =>
a -> m a
parReduce
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
TCMT IO (Maybe [MetaId])
-> ([MetaId] -> TCMT IO (Telescope, a))
-> TCMT IO (Maybe (Telescope, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM ([MetaId] -> TCMT IO (Maybe [MetaId])
dependencySortMetas [MetaId]
ms) (([MetaId] -> TCMT IO (Telescope, a))
-> TCMT IO (Maybe (Telescope, a)))
-> ([MetaId] -> TCMT IO (Telescope, a))
-> TCMT IO (Maybe (Telescope, a))
forall a b. (a -> b) -> a -> b
$ \[MetaId]
ms' -> do
as <- [MetaId] -> (MetaId -> TCMT IO Type) -> TCMT IO [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
ms' MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType
ns <- forM ms' getMetaNameSuggestion
let n = [MetaId] -> Int
forall a. Sized a => a -> Int
size [MetaId]
ms'
gamma = Int -> [VerboseKey] -> [Dom Type] -> Telescope
unflattenTel' Int
n [VerboseKey]
ns ([Dom Type] -> Telescope) -> [Dom Type] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Type -> Dom Type) -> [Type] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Dom Type
forall a. a -> Dom a
defaultDom [Type]
as
let metaIndex MetaId
x = (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> [MetaId] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex MetaId
x [MetaId]
ms'
runReaderT (metasToVars (gamma, x)) metaIndex
data OneHole a = OneHole
{ forall a. OneHole a -> Telescope
ohBoundVars :: Telescope
, forall a. OneHole a -> Type
ohType :: Type
, forall a. OneHole a -> Term -> a
ohPlugHole :: Term -> a
, forall a. OneHole a -> Elims -> Term
ohHead :: Elims -> Term
, forall a. OneHole a -> Elims
ohElims :: Elims
} deriving ((forall a b. (a -> b) -> OneHole a -> OneHole b)
-> (forall a b. a -> OneHole b -> OneHole a) -> Functor OneHole
forall a b. a -> OneHole b -> OneHole a
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
fmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
$c<$ :: forall a b. a -> OneHole b -> OneHole a
<$ :: forall a b. a -> OneHole b -> OneHole a
Functor)
ohHeadName :: OneHole a -> QName
ohHeadName :: forall a. OneHole a -> QName
ohHeadName OneHole a
oh = case OneHole a -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole a
oh [] of
Def QName
f Elims
_ -> QName
f
Con ConHead
c ConInfo
_ Elims
_ -> ConHead -> QName
conName ConHead
c
Term
_ -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__
ohContents :: OneHole a -> Term
ohContents :: forall a. OneHole a -> Term
ohContents OneHole a
oh = OneHole a -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole a
oh (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ OneHole a -> Elims
forall a. OneHole a -> Elims
ohElims OneHole a
oh
idHole :: Type -> Term -> OneHole Term
idHole :: Type -> Term -> OneHole Term
idHole Type
a = \case
Def QName
f Elims
es -> Telescope
-> Type
-> (Term -> Term)
-> (Elims -> Term)
-> Elims
-> OneHole Term
forall a.
Telescope
-> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
OneHole Telescope
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (QName -> Elims -> Term
Def QName
f) Elims
es
Con ConHead
c ConInfo
ci Elims
es -> Telescope
-> Type
-> (Term -> Term)
-> (Elims -> Term)
-> Elims
-> OneHole Term
forall a.
Telescope
-> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
OneHole Telescope
forall a. Tele a
EmptyTel Type
a Term -> Term
forall a. a -> a
id (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
es
Term
_ -> OneHole Term
forall a. HasCallStack => a
__IMPOSSIBLE__
composeHole :: OneHole Term -> OneHole a -> OneHole a
composeHole :: forall a. OneHole Term -> OneHole a -> OneHole a
composeHole OneHole Term
inner OneHole a
outer = OneHole
{ ohBoundVars :: Telescope
ohBoundVars = OneHole a -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole a
outer Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` OneHole Term -> Telescope
forall a. OneHole a -> Telescope
ohBoundVars OneHole Term
inner
, ohType :: Type
ohType = OneHole Term -> Type
forall a. OneHole a -> Type
ohType OneHole Term
inner
, ohPlugHole :: Term -> a
ohPlugHole = OneHole a -> Term -> a
forall a. OneHole a -> Term -> a
ohPlugHole OneHole a
outer (Term -> a) -> (Term -> Term) -> Term -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneHole Term -> Term -> Term
forall a. OneHole a -> Term -> a
ohPlugHole OneHole Term
inner
, ohHead :: Elims -> Term
ohHead = OneHole Term -> Elims -> Term
forall a. OneHole a -> Elims -> Term
ohHead OneHole Term
inner
, ohElims :: Elims
ohElims = OneHole Term -> Elims
forall a. OneHole a -> Elims
ohElims OneHole Term
inner
}
ohAddBV :: ArgName -> Dom Type -> OneHole a -> OneHole a
ohAddBV :: forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV VerboseKey
x Dom Type
a OneHole a
oh = OneHole a
oh { ohBoundVars = ExtendTel a $ Abs x $ ohBoundVars oh }
class (TermSubst p, Free p) => AllHoles p where
allHoles :: (Alternative m, PureTCM m) => TypeOf p -> p -> m (OneHole p)
allHoles_
:: ( Alternative m , PureTCM m , AllHoles p , TypeOf p ~ () )
=> p -> m (OneHole p)
allHoles_ :: forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ = TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles ()
allHolesList
:: ( PureTCM m , AllHoles p)
=> TypeOf p -> p -> m [OneHole p]
allHolesList :: forall (m :: * -> *) p.
(PureTCM m, AllHoles p) =>
TypeOf p -> p -> m [OneHole p]
allHolesList TypeOf p
a = ListT m (OneHole p) -> m [OneHole p]
forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
sequenceListT (ListT m (OneHole p) -> m [OneHole p])
-> (p -> ListT m (OneHole p)) -> p -> m [OneHole p]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOf p -> p -> ListT m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles TypeOf p
a
forceEtaExpansion :: Type -> Term -> [Elim' a] -> TCM (OneHole Term)
forceEtaExpansion :: forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
forceEtaExpansion Type
a Term
v [] = OneHole Term -> TCMT IO (OneHole Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneHole Term -> TCMT IO (OneHole Term))
-> OneHole Term -> TCMT IO (OneHole Term)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> OneHole Term
idHole Type
a Term
v
forceEtaExpansion Type
a Term
v (Elim' a
e:[Elim' a]
es) = case Elim' a
e of
Apply (Arg ArgInfo
i a
w) -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"Forcing" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a , TCMT IO Doc
"to take one more argument" ]
dom <- ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
i (Type -> Dom Type) -> TCMT IO Type -> TCMT IO (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Type
newTypeMeta_
cod <- addContext dom $ newTypeMeta_
equalType a $ mkPi (("x",) <$> dom) cod
let body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]
addContext dom $ ohAddBV "x" dom . fmap (Lam i . mkAbs "x") <$>
forceEtaExpansion cod body es
Proj ProjOrigin
o QName
f -> do
VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.eta" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"Forcing" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a , TCMT IO Doc
"to be projectible by" , QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f ]
r <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe QName)
getRecordOfField QName
f
Defn{ defType = ra, theDef = RecordDefn rdef } <- getConstInfo r
pars <- newArgsMeta ra
s <- ra `piApplyM` pars >>= \Type
s -> Type -> (Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> (Sort -> m a) -> m a -> m a
ifIsSort Type
s Sort -> TCMT IO Sort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TCMT IO Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
equalType a $ El s (Def r $ map Apply pars)
(_ , c , ci , fields) <- etaExpandRecord_ r pars rdef v
let fs = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
rdef
i = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex QName
f ([QName] -> Maybe Int) -> [QName] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Arg QName -> QName) -> [Arg QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Arg QName -> QName
forall e. Arg e -> e
unArg [Arg QName]
fs
fContent = Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term) -> Maybe (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Args
fields Args -> Int -> Maybe (Arg Term)
forall a. [a] -> Int -> Maybe a
!!! Int
i
fUpdate Term
w = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> (Arg Term -> Arg Term) -> Args -> Args
forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
i (Term
w Term -> Arg Term -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Args
fields
~(Just (El _ (Pi b c))) <- getDefType f =<< reduce a
let fa = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v
fmap fUpdate <$> forceEtaExpansion fa fContent es
IApply{} -> TCMT IO (OneHole Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
instance AllHoles p => AllHoles (Arg p) where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Arg p) -> Arg p -> m (OneHole (Arg p))
allHoles TypeOf (Arg p)
a Arg p
x = (p -> Arg p) -> OneHole p -> OneHole (Arg p)
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg p
x Arg p -> p -> Arg p
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (OneHole p -> OneHole (Arg p))
-> m (OneHole p) -> m (OneHole (Arg p))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles (Dom' Term (TypeOf p) -> TypeOf p
forall t e. Dom' t e -> e
unDom TypeOf (Arg p)
Dom' Term (TypeOf p)
a) (Arg p -> p
forall e. Arg e -> e
unArg Arg p
x)
instance AllHoles p => AllHoles (Dom p) where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Dom p) -> Dom p -> m (OneHole (Dom p))
allHoles TypeOf (Dom p)
a Dom p
x = (p -> Dom p) -> OneHole p -> OneHole (Dom p)
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Dom p
x Dom p -> p -> Dom p
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (OneHole p -> OneHole (Dom p))
-> m (OneHole p) -> m (OneHole (Dom p))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeOf p -> p -> m (OneHole p)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
allHoles TypeOf p
TypeOf (Dom p)
a (Dom p -> p
forall t e. Dom' t e -> e
unDom Dom p
x)
instance AllHoles (Abs Term) where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Abs Term) -> Abs Term -> m (OneHole (Abs Term))
allHoles (Dom Type
dom , Abs Type
a) Abs Term
x = (VerboseKey, Dom Type)
-> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(VerboseKey, Dom Type) -> m a -> m a
addContext (Abs Term -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Term
x , Dom Type
dom) (m (OneHole (Abs Term)) -> m (OneHole (Abs Term)))
-> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
forall a b. (a -> b) -> a -> b
$
VerboseKey -> Dom Type -> OneHole (Abs Term) -> OneHole (Abs Term)
forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) Dom Type
dom (OneHole (Abs Term) -> OneHole (Abs Term))
-> (OneHole Term -> OneHole (Abs Term))
-> OneHole Term
-> OneHole (Abs Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Abs Term) -> OneHole Term -> OneHole (Abs Term)
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Term -> Abs Term
forall a. (Subst a, Free a) => VerboseKey -> a -> Abs a
mkAbs (VerboseKey -> Term -> Abs Term) -> VerboseKey -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Abs Term -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Term
x) (OneHole Term -> OneHole (Abs Term))
-> m (OneHole Term) -> m (OneHole (Abs Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
TypeOf Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Term -> Term -> m (OneHole Term)
allHoles (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
a) (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
x)
instance AllHoles (Abs Type) where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
allHoles TypeOf (Abs Type)
dom Abs Type
a = (VerboseKey, Dom Type)
-> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(VerboseKey, Dom Type) -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a , TypeOf (Abs Type)
Dom Type
dom) (m (OneHole (Abs Type)) -> m (OneHole (Abs Type)))
-> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
forall a b. (a -> b) -> a -> b
$
VerboseKey -> Dom Type -> OneHole (Abs Type) -> OneHole (Abs Type)
forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
ohAddBV (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) TypeOf (Abs Type)
Dom Type
dom (OneHole (Abs Type) -> OneHole (Abs Type))
-> (OneHole Type -> OneHole (Abs Type))
-> OneHole Type
-> OneHole (Abs Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Abs Type) -> OneHole Type -> OneHole (Abs Type)
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey -> Type -> Abs Type
forall a. (Subst a, Free a) => VerboseKey -> a -> Abs a
mkAbs (VerboseKey -> Type -> Abs Type) -> VerboseKey -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
a) (OneHole Type -> OneHole (Abs Type))
-> m (OneHole Type) -> m (OneHole (Abs Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Type -> m (OneHole Type)
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
a)
instance AllHoles Elims where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Elims -> Elims -> m (OneHole Elims)
allHoles (Type
a,Elims -> Term
hd) [] = m (OneHole Elims)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
allHoles (Type
a,Elims -> Term
hd) (Elim' Term
e:Elims
es) = do
VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.hole" Int
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"Head symbol" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Elims -> Term
hd []) , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"is eliminated by" , Elim' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM Elim' Term
e
]
case Elim' Term
e of
Apply Arg Term
x -> do
~(Pi b c) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> m Type -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
let a' = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term
eElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
(fmap ((:es) . Apply) <$> allHoles b x)
<|> (fmap (e:) <$> allHoles (a' , hd') es)
Proj ProjOrigin
o QName
f -> do
~(Just (El _ (Pi b c))) <- QName -> Type -> m (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> m (Maybe Type)) -> m Type -> m (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
let a' = Abs Type
c Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Elims -> Term
hd []
hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
fmap (e:) <$> allHoles (a' , hd') es
IApply Term
x Term
y Term
u -> m (OneHole Elims)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
instance AllHoles Type where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Type -> Type -> m (OneHole Type)
allHoles TypeOf Type
_ (El Sort
s Term
a) = m (OneHole Type) -> m (OneHole Type)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (m (OneHole Type) -> m (OneHole Type))
-> m (OneHole Type) -> m (OneHole Type)
forall a b. (a -> b) -> a -> b
$
(Term -> Type) -> OneHole Term -> OneHole Type
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s) (OneHole Term -> OneHole Type)
-> m (OneHole Term) -> m (OneHole Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeOf Term -> Term -> m (OneHole Term)
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Term -> Term -> m (OneHole Term)
allHoles (Sort -> Type
sort Sort
s) Term
a
instance AllHoles Term where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Term -> Term -> m (OneHole Term)
allHoles TypeOf Term
a Term
u = do
VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"rewriting.confluence.hole" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"Getting holes of term" , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u , TCMT IO Doc
":" , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM TypeOf Term
Type
a ]
case Term
u of
Var Int
i Elims
es -> do
ai <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
fmap (Var i) <$> allHoles (ai , Var i) es
Lam ArgInfo
i Abs Term
u -> do
~(Pi b c) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> m Type -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce TypeOf Term
Type
a
fmap (Lam i) <$> allHoles (b,c) u
Lit Literal
l -> m (OneHole Term)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
v :: Term
v@(Def QName
f Elims
es) -> do
fa <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
pure (idHole a v)
<|> (fmap (Def f) <$> allHoles (fa , Def f) es)
v :: Term
v@(Con ConHead
c ConInfo
ci Elims
es) -> do
ca <- ((QName, Type, Args), Type) -> Type
forall a b. (a, b) -> b
snd (((QName, Type, Args), Type) -> Type)
-> (Maybe ((QName, Type, Args), Type)
-> ((QName, Type, Args), Type))
-> Maybe ((QName, Type, Args), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
forall a. a -> Maybe a -> a
fromMaybe ((QName, Type, Args), Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
-> m (Maybe ((QName, Type, Args), Type)) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c (Type -> m (Maybe ((QName, Type, Args), Type)))
-> m Type -> m (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce TypeOf Term
Type
a
pure (idHole a v)
<|> (fmap (Con c ci) <$> allHoles (ca , Con c ci) es)
Pi Dom Type
a Abs Type
b ->
((Dom Type -> Term) -> OneHole (Dom Type) -> OneHole Term
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Dom Type
a -> Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b) (OneHole (Dom Type) -> OneHole Term)
-> m (OneHole (Dom Type)) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (OneHole (Dom Type))
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ Dom Type
a) m (OneHole Term) -> m (OneHole Term) -> m (OneHole Term)
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
((Abs Type -> Term) -> OneHole (Abs Type) -> OneHole Term
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Abs Type
b -> Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b) (OneHole (Abs Type) -> OneHole Term)
-> m (OneHole (Abs Type)) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
forall p (m :: * -> *).
(AllHoles p, Alternative m, PureTCM m) =>
TypeOf p -> p -> m (OneHole p)
forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
allHoles TypeOf (Abs Type)
Dom Type
a Abs Type
b)
Sort Sort
s -> (Sort -> Term) -> OneHole Sort -> OneHole Term
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort (OneHole Sort -> OneHole Term)
-> m (OneHole Sort) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (OneHole Sort)
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ Sort
s
Level Level
l -> (Level -> Term) -> OneHole Level -> OneHole Term
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level -> Term
Level (OneHole Level -> OneHole Term)
-> m (OneHole Level) -> m (OneHole Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (OneHole Level)
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
MetaV{} -> m (OneHole Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
DontCare{} -> m (OneHole Term)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Dummy{} -> m (OneHole Term)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
instance AllHoles Sort where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Sort -> Sort -> m (OneHole Sort)
allHoles TypeOf Sort
_ = \case
Univ Univ
u Level
l -> (Level -> Sort) -> OneHole Level -> OneHole Sort
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u) (OneHole Level -> OneHole Sort)
-> m (OneHole Level) -> m (OneHole Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (OneHole Level)
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ Level
l
Inf Univ
_ Integer
_ -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Sort
SizeUniv -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Sort
LockUniv -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Sort
LevelUniv -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
Sort
IntervalUniv -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
PiSort{} -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
FunSort{} -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
UnivSort{} -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
MetaS{} -> m (OneHole Sort)
forall a. HasCallStack => a
__IMPOSSIBLE__
DefS QName
f Elims
es -> do
fa <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
fmap (DefS f) <$> allHoles (fa , Def f) es
DummyS{} -> m (OneHole Sort)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
instance AllHoles Level where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf Level -> Level -> m (OneHole Level)
allHoles TypeOf Level
_ (Max Integer
n [PlusLevel' Term]
ls) = ([PlusLevel' Term] -> Level)
-> OneHole [PlusLevel' Term] -> OneHole Level
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) (OneHole [PlusLevel' Term] -> OneHole Level)
-> m (OneHole [PlusLevel' Term]) -> m (OneHole Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ [PlusLevel' Term]
ls
instance AllHoles [PlusLevel] where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf [PlusLevel' Term]
-> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
allHoles TypeOf [PlusLevel' Term]
_ [] = m (OneHole [PlusLevel' Term])
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
allHoles TypeOf [PlusLevel' Term]
_ (PlusLevel' Term
l:[PlusLevel' Term]
ls) =
((PlusLevel' Term -> [PlusLevel' Term])
-> OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term]
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:[PlusLevel' Term]
ls) (OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term])
-> m (OneHole (PlusLevel' Term)) -> m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ PlusLevel' Term
l)
m (OneHole [PlusLevel' Term])
-> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (([PlusLevel' Term] -> [PlusLevel' Term])
-> OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term]
forall a b. (a -> b) -> OneHole a -> OneHole b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlusLevel' Term
lPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:) (OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term])
-> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
forall (m :: * -> *) p.
(Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
p -> m (OneHole p)
allHoles_ [PlusLevel' Term]
ls)
instance AllHoles PlusLevel where
allHoles :: forall (m :: * -> *).
(Alternative m, PureTCM m) =>
TypeOf (PlusLevel' Term)
-> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
allHoles TypeOf (PlusLevel' Term)
_ (Plus Integer
n Term
l) = do
la <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType'
fmap (Plus n) <$> allHoles la l
class MetasToVars a where
metasToVars
:: (MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
=> a -> m a
default metasToVars
:: ( MetasToVars a', Traversable f, a ~ f a'
, MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
=> a -> m a
metasToVars = (a' -> m a') -> f a' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> m a'
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a' -> m a'
metasToVars
instance MetasToVars a => MetasToVars [a] where
instance MetasToVars a => MetasToVars (Arg a) where
instance MetasToVars a => MetasToVars (Dom a) where
instance MetasToVars a => MetasToVars (Elim' a) where
instance MetasToVars a => MetasToVars (Abs a) where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs a -> m (Abs a)
metasToVars (Abs VerboseKey
i a
x) = VerboseKey -> a -> Abs a
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
i (a -> Abs a) -> m a -> m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((MetaId -> Maybe Int) -> MetaId -> Maybe Int) -> m a -> m a
forall a.
((MetaId -> Maybe Int) -> MetaId -> Maybe Int) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Int -> Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Int
forall a. Enum a => a -> a
succ (Maybe Int -> Maybe Int)
-> (MetaId -> Maybe Int) -> MetaId -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x)
metasToVars (NoAbs VerboseKey
i a
x) = VerboseKey -> a -> Abs a
forall a. VerboseKey -> a -> Abs a
NoAbs VerboseKey
i (a -> Abs a) -> m a -> m (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x
instance MetasToVars Term where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars = \case
Var Int
i Elims
es -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
Lam ArgInfo
i Abs Term
u -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> m (Abs Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs Term -> m (Abs Term)
metasToVars Abs Term
u
Lit Literal
l -> Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Literal -> Term
Lit Literal
l)
Def QName
f Elims
es -> QName -> Elims -> Term
Def QName
f (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
Con ConHead
c ConInfo
i Elims
es -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
i (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
Pi Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> Term
Pi (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m (Dom Type)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Dom Type -> m (Dom Type)
metasToVars Dom Type
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> m (Abs Type)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs Type -> m (Abs Type)
metasToVars Abs Type
b
Sort Sort
s -> Sort -> Term
Sort (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
s
Level Level
l -> Level -> Term
Level (Level -> Term) -> m Level -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Level -> m Level
metasToVars Level
l
MetaV MetaId
x Elims
es -> ((MetaId -> Maybe Int) -> Maybe Int) -> m (Maybe Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((MetaId -> Maybe Int) -> MetaId -> Maybe Int
forall a b. (a -> b) -> a -> b
$ MetaId
x) m (Maybe Int) -> (Maybe Int -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Int
i -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
Maybe Int
Nothing -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
DontCare Term
u -> Term -> Term
DontCare (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars Term
u
Dummy VerboseKey
s Elims
es -> VerboseKey -> Elims -> Term
Dummy VerboseKey
s (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
instance MetasToVars Type where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Type -> m Type
metasToVars (El Sort
s Term
t) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
s m (Term -> Type) -> m Term -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars Term
t
instance MetasToVars Sort where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars = \case
Univ Univ
u Level
l -> Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Sort) -> m Level -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Level
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Level -> m Level
metasToVars Level
l
Inf Univ
u Integer
n -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
Sort
SizeUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
SizeUniv
Sort
LockUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
LockUniv
Sort
LevelUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
LevelUniv
Sort
IntervalUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
forall t. Sort' t
IntervalUniv
PiSort Dom' Term Term
s Sort
t Abs Sort
u -> Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> m (Dom' Term Term) -> m (Sort -> Abs Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term -> m (Dom' Term Term)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Dom' Term Term -> m (Dom' Term Term)
metasToVars Dom' Term Term
s m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
t m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Sort -> m (Abs Sort)
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs Sort -> m (Abs Sort)
metasToVars Abs Sort
u
FunSort Sort
s Sort
t -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort) -> m Sort -> m (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
s m (Sort -> Sort) -> m Sort -> m Sort
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
t
UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort) -> m Sort -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Sort -> m Sort
metasToVars Sort
s
MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
DefS QName
f Elims
es -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
f (Elims -> Sort) -> m Elims -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> m Elims
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Elims -> m Elims
metasToVars Elims
es
DummyS VerboseKey
s -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Sort
forall t. VerboseKey -> Sort' t
DummyS VerboseKey
s
instance MetasToVars Level where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Level -> m Level
metasToVars (Max Integer
n [PlusLevel' Term]
ls) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> m [PlusLevel' Term]
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
[PlusLevel' Term] -> m [PlusLevel' Term]
metasToVars [PlusLevel' Term]
ls
instance MetasToVars PlusLevel where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
PlusLevel' Term -> m (PlusLevel' Term)
metasToVars (Plus Integer
n Term
x) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Term -> m Term
metasToVars Term
x
instance MetasToVars a => MetasToVars (Tele a) where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Tele a -> m (Tele a)
metasToVars Tele a
EmptyTel = Tele a -> m (Tele a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele a
forall a. Tele a
EmptyTel
metasToVars (ExtendTel a
a Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (a -> Abs (Tele a) -> Tele a) -> m a -> m (Abs (Tele a) -> Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
a m (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs (Tele a) -> m (Abs (Tele a))
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
Abs (Tele a) -> m (Abs (Tele a))
metasToVars Abs (Tele a)
tel
instance (MetasToVars a, MetasToVars b) => MetasToVars (a,b) where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(a, b) -> m (a, b)
metasToVars (a
x,b
y) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y
instance (MetasToVars a, MetasToVars b, MetasToVars c) => MetasToVars (a,b,c) where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(a, b, c) -> m (a, b, c)
metasToVars (a
x,b
y,c
z) = (,,) (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> m c
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
c -> m c
metasToVars c
z
instance (MetasToVars a, MetasToVars b, MetasToVars c, MetasToVars d) => MetasToVars (a,b,c,d) where
metasToVars :: forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
(a, b, c, d) -> m (a, b, c, d)
metasToVars (a
x,b
y,c
z,d
w) = (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> m a -> m (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
a -> m a
metasToVars a
x m (b -> c -> d -> (a, b, c, d))
-> m b -> m (c -> d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m b
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
b -> m b
metasToVars b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> m c
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
c -> m c
metasToVars c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> d -> m d
forall a (m :: * -> *).
(MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
HasBuiltins m) =>
a -> m a
forall (m :: * -> *).
(MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
d -> m d
metasToVars d
w