module Agda.TypeChecking.ProjectionLike where
import Control.Monad
import qualified Data.Map as Map
import Data.Monoid (Any(..), getAny)
import Agda.Interaction.Options
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free (runFree, IgnoreSorts(..))
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce)
import Agda.TypeChecking.DropArgs
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Impossible
data ProjectionView
= ProjectionView
{ ProjectionView -> QName
projViewProj :: QName
, ProjectionView -> Arg Term
projViewSelf :: Arg Term
, ProjectionView -> Elims
projViewSpine :: Elims
}
| LoneProjectionLike QName ArgInfo
| NoProjection Term
unProjView :: ProjectionView -> Term
unProjView :: ProjectionView -> Term
unProjView pv :: ProjectionView
pv =
case ProjectionView
pv of
ProjectionView f :: QName
f a :: Arg Term
a es :: Elims
es -> QName -> Elims -> Term
Def QName
f (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
a Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es)
LoneProjectionLike f :: QName
f ai :: ArgInfo
ai -> QName -> Elims -> Term
Def QName
f []
NoProjection v :: Term
v -> Term
v
{-# SPECIALIZE projView :: Term -> TCM ProjectionView #-}
projView :: HasConstInfo m => Term -> m ProjectionView
projView :: Term -> m ProjectionView
projView v :: Term
v = do
let fallback :: m ProjectionView
fallback = ProjectionView -> m ProjectionView
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ Term -> ProjectionView
NoProjection Term
v
case Term
v of
Def f :: QName
f es :: Elims
es -> m (Maybe Projection)
-> m ProjectionView
-> (Projection -> m ProjectionView)
-> m ProjectionView
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
f) m ProjectionView
fallback ((Projection -> m ProjectionView) -> m ProjectionView)
-> (Projection -> m ProjectionView) -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ \ isP :: Projection
isP -> do
if Projection -> Int
projIndex Projection
isP Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 then m ProjectionView
fallback else do
case Elims
es of
[] -> ProjectionView -> m ProjectionView
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ QName -> ArgInfo -> ProjectionView
LoneProjectionLike QName
f (ArgInfo -> ProjectionView) -> ArgInfo -> ProjectionView
forall a b. (a -> b) -> a -> b
$ Projection -> ArgInfo
projArgInfo Projection
isP
Apply a :: Arg Term
a : es :: Elims
es -> ProjectionView -> m ProjectionView
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjectionView -> m ProjectionView)
-> ProjectionView -> m ProjectionView
forall a b. (a -> b) -> a -> b
$ QName -> Arg Term -> Elims -> ProjectionView
ProjectionView QName
f Arg Term
a Elims
es
Proj{} : _ -> m ProjectionView
forall a. HasCallStack => a
__IMPOSSIBLE__
IApply{} : _ -> m ProjectionView
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> m ProjectionView
fallback
reduceProjectionLike :: (MonadReduce m, MonadTCEnv m, HasConstInfo m) => Term -> m Term
reduceProjectionLike :: Term -> m Term
reduceProjectionLike v :: Term
v = do
ProjectionView
pv <- Term -> m ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
case ProjectionView
pv of
ProjectionView{} -> m Term -> m Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceProjections (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
_ -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
elimView
:: (MonadReduce m, MonadTCEnv m, HasConstInfo m)
=> Bool -> Term -> m Term
elimView :: Bool -> Term -> m Term
elimView loneProjToLambda :: Bool
loneProjToLambda v :: Term
v = do
VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.conv.elim" 30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ "elimView of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
Term
v <- Term -> m Term
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasConstInfo m) =>
Term -> m Term
reduceProjectionLike Term
v
VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.conv.elim" 40 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
"elimView (projections reduced) of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
ProjectionView
pv <- Term -> m ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v
case ProjectionView
pv of
NoProjection{} -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
LoneProjectionLike f :: QName
f ai :: ArgInfo
ai
| Bool
loneProjToLambda -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs "r" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var 0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f]
| Bool
otherwise -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
ProjectionView f :: QName
f a :: Arg Term
a es :: Elims
es -> (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` (ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjPrefix QName
f Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es)) (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Term -> m Term
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasConstInfo m) =>
Bool -> Term -> m Term
elimView Bool
loneProjToLambda (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
eligibleForProjectionLike :: (HasConstInfo m) => QName -> m Bool
eligibleForProjectionLike :: QName -> m Bool
eligibleForProjectionLike d :: QName
d = Defn -> Bool
eligible (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> m Definition -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
where
eligible :: Defn -> Bool
eligible = \case
Datatype{} -> Bool
True
Record{} -> Bool
True
Axiom{} -> Bool
True
DataOrRecSig{} -> Bool
True
GeneralizableVar{} -> Bool
False
Function{} -> Bool
False
Primitive{} -> Bool
False
Constructor{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
AbstractDefn d :: Defn
d -> Defn -> Bool
eligible Defn
d
makeProjection :: QName -> TCM ()
makeProjection :: QName -> TCM ()
makeProjection x :: QName
x = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optProjectionLike (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
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
$ do
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 70 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Considering " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
x VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ " for projection likeness"
Definition
defn <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
let t :: Type
t = Definition -> Type
defType Definition
defn
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.proj.like" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "Checking for projection likeness "
, QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> " : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
]
case Definition -> Defn
theDef Definition
defn of
Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls}
| (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " projection-like functions cannot have absurd clauses"
| (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> (Term -> Bool) -> Maybe Term -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Bool
isRecordExpression (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cls ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " projection-like functions cannot have record rhss"
def :: Defn
def@Function{funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
Nothing, funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls,
funSplitTree :: Defn -> Maybe SplitTree
funSplitTree = Maybe SplitTree
st0, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc0, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
NotInjective,
funMutual :: Defn -> Maybe [QName]
funMutual = Just [],
funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
ConcreteDef} -> do
[(Arg QName, Int)]
ps0 <- ((Arg QName, Int) -> TCMT IO Bool)
-> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Arg QName, Int) -> TCMT IO Bool
validProj ([(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)])
-> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
forall a b. (a -> b) -> a -> b
$ [Term] -> Type -> [(Arg QName, Int)]
candidateArgs [] Type
t
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ if [(Arg QName, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0 then " no candidates found"
else " candidates: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(Arg QName, Int)] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [(Arg QName, Int)]
ps0
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Arg QName, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Arg QName, Int)]
ps0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCMT IO Bool
recursive (VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " recursive functions are not considered for projection-likeness") (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
case [(Arg QName, Int)] -> Maybe (Arg QName, Int)
forall a. [a] -> Maybe a
lastMaybe (((Arg QName, Int) -> Bool)
-> [(Arg QName, Int)] -> [(Arg QName, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Clause] -> Int -> Bool
forall (t :: * -> *). Foldable t => t Clause -> Int -> Bool
checkOccurs [Clause]
cls (Int -> Bool)
-> ((Arg QName, Int) -> Int) -> (Arg QName, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg QName, Int) -> Int
forall a b. (a, b) -> b
snd) [(Arg QName, Int)]
ps0) of
Nothing -> VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.proj.like" 50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "occurs check failed"
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "clauses =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ((Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty [Clause]
cls) ]
Just (d :: Arg QName
d, n :: Int
n) -> do
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "tc.proj.like" 10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> " : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "is projection like in argument", Int -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
n, "for type", QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
d) ]
]
VerboseKey -> Int -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> Int -> m ()
__CRASH_WHEN__ "tc.proj.like.crash" 1000
let cls' :: [Clause]
cls' = (Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Clause -> Clause
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n) [Clause]
cls
cc :: Maybe CompiledClauses
cc = Int -> Maybe CompiledClauses -> Maybe CompiledClauses
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n Maybe CompiledClauses
cc0
st :: Maybe SplitTree
st = Int -> Maybe SplitTree -> Maybe SplitTree
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n Maybe SplitTree
st0
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> VerboseKey
unlines
[ " rewrote clauses to"
, " " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> VerboseKey
forall a. Show a => a -> VerboseKey
show Maybe CompiledClauses
cc
]
let pIndex :: Int
pIndex = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
tel :: [Dom (VerboseKey, Type)]
tel = Int -> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. Int -> [a] -> [a]
take Int
pIndex ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)])
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList (Tele (Dom Type) -> [Dom (VerboseKey, Type)])
-> Tele (Dom Type) -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ TelV Type -> Tele (Dom Type)
forall a. TelV a -> Tele (Dom a)
theTel (TelV Type -> Tele (Dom Type)) -> TelV Type -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Type -> TelV Type
telView' Type
t
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Dom (VerboseKey, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom (VerboseKey, Type)]
tel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
pIndex) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let projection :: Projection
projection = Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection
{ projProper :: Maybe QName
projProper = Maybe QName
forall a. Maybe a
Nothing
, projOrig :: QName
projOrig = QName
x
, projFromType :: Arg QName
projFromType = Arg QName
d
, projIndex :: Int
projIndex = Int
pIndex
, projLams :: ProjLams
projLams = [Arg VerboseKey] -> ProjLams
ProjLams ([Arg VerboseKey] -> ProjLams) -> [Arg VerboseKey] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom (VerboseKey, Type) -> Arg VerboseKey)
-> [Dom (VerboseKey, Type)] -> [Arg VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term VerboseKey -> Arg VerboseKey
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term VerboseKey -> Arg VerboseKey)
-> (Dom (VerboseKey, Type) -> Dom' Term VerboseKey)
-> Dom (VerboseKey, Type)
-> Arg VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VerboseKey, Type) -> VerboseKey)
-> Dom (VerboseKey, Type) -> Dom' Term VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst) [Dom (VerboseKey, Type)]
tel
}
let newDef :: Defn
newDef = Defn
def
{ funProjection :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
projection
, funClauses :: [Clause]
funClauses = [Clause]
cls'
, funSplitTree :: Maybe SplitTree
funSplitTree = Maybe SplitTree
st
, funCompiled :: Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc
, funInv :: FunctionInverse
funInv = Int -> FunctionInverse -> FunctionInverse
forall a. DropArgs a => Int -> a -> a
dropArgs Int
n (FunctionInverse -> FunctionInverse)
-> FunctionInverse -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Defn -> FunctionInverse
funInv Defn
def
}
QName -> Definition -> TCM ()
addConstant QName
x (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ Definition
defn { defPolarity :: [Polarity]
defPolarity = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
drop Int
n ([Polarity] -> [Polarity]) -> [Polarity] -> [Polarity]
forall a b. (a -> b) -> a -> b
$ Definition -> [Polarity]
defPolarity Definition
defn
, defArgOccurrences :: [Occurrence]
defArgOccurrences = Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
drop Int
n ([Occurrence] -> [Occurrence]) -> [Occurrence] -> [Occurrence]
forall a b. (a -> b) -> a -> b
$ Definition -> [Occurrence]
defArgOccurrences Definition
defn
, defDisplay :: [LocalDisplayForm]
defDisplay = []
, theDef :: Defn
theDef = Defn
newDef
}
Function{funInv :: Defn -> FunctionInverse
funInv = Inverse{}} ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " injective functions can't be projections"
Function{funAbstr :: Defn -> IsAbstract
funAbstr = IsAbstract
AbstractDef} ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " abstract functions can't be projections"
Function{funProjection :: Defn -> Maybe Projection
funProjection = Just{}} ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " already projection like"
Function{funMutual :: Defn -> Maybe [QName]
funMutual = Just (_:_)} ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " mutual functions can't be projections"
Function{funMutual :: Defn -> Maybe [QName]
funMutual = Maybe [QName]
Nothing} ->
VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " mutuality check has not run yet"
Axiom -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but Axiom"
DataOrRecSig{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but DataOrRecSig"
GeneralizableVar{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but GeneralizableVar"
AbstractDefn{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but AbstractDefn"
Constructor{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but Constructor"
Datatype{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but Datatype"
Primitive{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but Primitive"
Record{} -> VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn "tc.proj.like" 30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " not a function, but Record"
where
isRecordExpression :: Term -> Bool
isRecordExpression :: Term -> Bool
isRecordExpression = \case
Con _ ConORec _ -> Bool
True
_ -> Bool
False
validProj :: (Arg QName, Int) -> TCM Bool
validProj :: (Arg QName, Int) -> TCMT IO Bool
validProj (_, 0) = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
validProj (d :: Arg QName
d, _) = QName -> TCMT IO Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
eligibleForProjectionLike (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
d)
recursive :: TCMT IO Bool
recursive = do
Map Item Integer
occs <- QName -> TCM (Map Item Integer)
computeOccurrences QName
x
case Item -> Map Item Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (QName -> Item
ADef QName
x) Map Item Integer
occs of
Just n :: Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
checkOccurs :: t Clause -> Int -> Bool
checkOccurs cls :: t Clause
cls n :: Int
n = (Clause -> Bool) -> t Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Clause -> Bool
nonOccur Int
n) t Clause
cls
nonOccur :: Int -> Clause -> Bool
nonOccur n :: Int
n cl :: Clause
cl =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n [Int]
p [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
, Int -> [NamedArg (Pattern' DBPatVar)] -> Bool
forall x. Int -> [NamedArg (Pattern' x)] -> Bool
onlyMatch Int
n [NamedArg (Pattern' DBPatVar)]
ps
, Int -> Int -> Maybe Term -> Bool
forall t. Free t => Int -> Int -> t -> Bool
checkBody Int
m Int
n Maybe Term
b ]
where
Perm _ p :: [Int]
p = 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
$ Clause -> Maybe Permutation
clausePerm Clause
cl
ps :: [NamedArg (Pattern' DBPatVar)]
ps = Clause -> [NamedArg (Pattern' DBPatVar)]
namedClausePats Clause
cl
b :: Maybe Term
b = Clause -> Maybe Term
compiledClauseBody Clause
cl
m :: Int
m = [Arg (Either DBPatVar Term)] -> Int
forall a. Sized a => a -> Int
size ([Arg (Either DBPatVar Term)] -> Int)
-> [Arg (Either DBPatVar Term)] -> Int
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' DBPatVar) -> [Arg (Either DBPatVar Term)])
-> [NamedArg (Pattern' DBPatVar)] -> [Arg (Either DBPatVar Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NamedArg (Pattern' DBPatVar) -> [Arg (Either DBPatVar Term)]
forall a b. PatternVars a b => b -> [Arg (Either a Term)]
patternVars [NamedArg (Pattern' DBPatVar)]
ps
onlyMatch :: Int -> [NamedArg (Pattern' x)] -> Bool
onlyMatch n :: Int
n ps :: [NamedArg (Pattern' x)]
ps = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (Pattern' x)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
forall x. Pattern' x -> Bool
shallowMatch (Pattern' x -> Bool)
-> (NamedArg (Pattern' x) -> Pattern' x)
-> NamedArg (Pattern' x)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' x) -> Pattern' x
forall a. NamedArg a -> a
namedArg) (Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. Int -> [a] -> [a]
take 1 [NamedArg (Pattern' x)]
ps1) Bool -> Bool -> Bool
&&
[NamedArg (Pattern' x)] -> Bool
forall x. [NamedArg (Pattern' x)] -> Bool
noMatches ([NamedArg (Pattern' x)]
ps0 [NamedArg (Pattern' x)]
-> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. [a] -> [a] -> [a]
++ Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
forall a. Int -> [a] -> [a]
drop 1 [NamedArg (Pattern' x)]
ps1)
where
(ps0 :: [NamedArg (Pattern' x)]
ps0, ps1 :: [NamedArg (Pattern' x)]
ps1) = Int
-> [NamedArg (Pattern' x)]
-> ([NamedArg (Pattern' x)], [NamedArg (Pattern' x)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg (Pattern' x)]
ps
shallowMatch :: Pattern' x -> Bool
shallowMatch (ConP _ _ ps :: [NamedArg (Pattern' x)]
ps) = [NamedArg (Pattern' x)] -> Bool
forall x. [NamedArg (Pattern' x)] -> Bool
noMatches [NamedArg (Pattern' x)]
ps
shallowMatch _ = Bool
True
noMatches :: [NamedArg (Pattern' x)] -> Bool
noMatches = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (Pattern' x)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' x -> Bool
forall x. Pattern' x -> Bool
noMatch (Pattern' x -> Bool)
-> (NamedArg (Pattern' x) -> Pattern' x)
-> NamedArg (Pattern' x)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' x) -> Pattern' x
forall a. NamedArg a -> a
namedArg)
noMatch :: Pattern' x -> Bool
noMatch ConP{} = Bool
False
noMatch DefP{} = Bool
False
noMatch LitP{} = Bool
False
noMatch ProjP{}= Bool
False
noMatch VarP{} = Bool
True
noMatch DotP{} = Bool
True
noMatch IApplyP{} = Bool
True
checkBody :: Int -> Int -> t -> Bool
checkBody m :: Int
m n :: Int
n b :: t
b = Bool -> Bool
not (Bool -> Bool) -> (Any -> Bool) -> Any -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar Any -> IgnoreSorts -> t -> Any
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar Any
badVar IgnoreSorts
IgnoreNot t
b
where badVar :: SingleVar Any
badVar x :: Int
x = Bool -> Any
Any (Bool -> Any) -> Bool -> Any
forall a b. (a -> b) -> a -> b
$ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m
candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
candidateArgs vs :: [Term]
vs t :: Type
t =
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Pi a :: Dom Type
a b :: Abs Type
b
| Def d :: QName
d es :: Elims
es <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a,
Just us :: [Arg Term]
us <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es,
[Term]
vs [Term] -> [Term] -> Bool
forall a. Eq a => a -> a -> Bool
== (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
us -> (QName
d QName -> Arg Type -> Arg QName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs) (Arg QName, Int) -> [(Arg QName, Int)] -> [(Arg QName, Int)]
forall a. a -> [a] -> [a]
: Abs Type -> [(Arg QName, Int)]
candidateRec Abs Type
b
| Bool
otherwise -> Abs Type -> [(Arg QName, Int)]
candidateRec Abs Type
b
_ -> []
where
candidateRec :: Abs Type -> [(Arg QName, Int)]
candidateRec NoAbs{} = []
candidateRec (Abs x :: VerboseKey
x t :: Type
t) = [Term] -> Type -> [(Arg QName, Int)]
candidateArgs (Int -> Term
var ([Term] -> Int
forall a. Sized a => a -> Int
size [Term]
vs) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs) Type
t