module Agda.TypeChecking.ProjectionLike where
import Control.Monad
import qualified Data.Map as Map
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free (isBinderUsed)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce)
import Agda.TypeChecking.DropArgs
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Permutation
#include "../undefined.h"
import Agda.Utils.Impossible
data ProjectionView
= ProjectionView
{ projViewProj :: QName
, projViewSelf :: I.Arg Term
, projViewSpine :: Elims
}
| LoneProjectionLike QName I.ArgInfo
| NoProjection Term
unProjView :: ProjectionView -> Term
unProjView pv =
case pv of
ProjectionView f a es -> Def f (Apply a : es)
LoneProjectionLike f ai -> Def f []
NoProjection v -> v
projView :: Term -> TCM ProjectionView
projView v = do
let fallback = return $ NoProjection v
case ignoreSharing v of
Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do
case es of
[] -> return $ LoneProjectionLike f $ projArgInfo isP
Apply a : es -> return $ ProjectionView f a es
Proj{} : _ -> __IMPOSSIBLE__
_ -> fallback
reduceProjectionLike :: Term -> TCM Term
reduceProjectionLike v = do
pv <- projView v
case pv of
ProjectionView{} -> onlyReduceProjections $ reduce v
_ -> return v
elimView :: Bool -> Term -> TCM Term
elimView loneProjToLambda v = do
reportSDoc "tc.conv.elim" 30 $ text "elimView of " <+> prettyTCM v
reportSLn "tc.conv.elim" 50 $ "v = " ++ show v
v <- reduceProjectionLike v
reportSDoc "tc.conv.elim" 40 $
text "elimView (projections reduced) of " <+> prettyTCM v
pv <- projView v
case pv of
NoProjection{} -> return v
LoneProjectionLike f ai
| loneProjToLambda -> return $ Lam ai $ Abs "r" $ Var 0 [Proj f]
| otherwise -> return v
ProjectionView f a es -> (`applyE` (Proj f : es)) <$> elimView loneProjToLambda (unArg a)
eligibleForProjectionLike :: QName -> TCM Bool
eligibleForProjectionLike d = do
defn <- theDef <$> getConstInfo d
return $ case defn of
Datatype{} -> True
Record{} -> True
Axiom{} -> True
_ -> False
makeProjection :: QName -> TCM ()
makeProjection x = inTopContext $ do
defn <- getConstInfo x
let t = defType defn
reportSDoc "tc.proj.like" 20 $ sep
[ text "Checking for projection likeness "
, prettyTCM x <+> text " : " <+> prettyTCM t
]
case theDef defn of
Function{funClauses = cls}
| any (isNothing . getBodyUnraised) cls ->
reportSLn "tc.proj.like" 30 $ " projection-like functions cannot have absurd clauses"
def@Function{funProjection = Nothing, funClauses = cls, funCompiled = cc0, funInv = NotInjective,
funMutual = [],
funAbstr = ConcreteDef} -> do
ps0 <- filterM validProj $ candidateArgs [] t
reportSLn "tc.proj.like" 30 $ if null ps0 then " no candidates found"
else " candidates: " ++ show ps0
unless (null ps0) $ do
ifM recursive (reportSLn "tc.proj.like" 30 $ " recursive functions are not considered for projection-likeness") $ do
ps <- return $ filter (checkOccurs cls . snd) ps0
when (null ps) $
reportSLn "tc.proj.like" 50 $
" occurs check failed\n clauses = " ++ show cls
case reverse ps of
[] -> return ()
(d, n) : _ -> do
reportSDoc "tc.proj.like" 10 $ sep
[ prettyTCM x <+> text " : " <+> prettyTCM t
, text $ " is projection like in argument " ++ show n ++ " for type " ++ show d
]
let cls' = map (dropArgs n) cls
cc = dropArgs n cc0
reportSLn "tc.proj.like" 60 $ " rewrote clauses to\n " ++ show cc
let (ptel, Dom ai _ : _) = splitAt n $ telToList $ theTel $ telView' t
proj = teleNoAbs ptel $ Def x []
let projection = Projection
{ projProper = Nothing
, projFromType = d
, projIndex = n + 1
, projDropPars = proj
, projArgInfo = ai
}
let newDef = def
{ funProjection = Just projection
, funClauses = cls'
, funCompiled = cc
, funInv = dropArgs n $ funInv def
}
addConstant x $ defn { defPolarity = drop n $ defPolarity defn
, defArgOccurrences = drop n $ defArgOccurrences defn
, defDisplay = []
, theDef = newDef
}
Function{funInv = Inverse{}} ->
reportSLn "tc.proj.like" 30 $ " injective functions can't be projections"
Function{funAbstr = AbstractDef} ->
reportSLn "tc.proj.like" 30 $ " abstract functions can't be projections"
Function{funProjection = Just{}} ->
reportSLn "tc.proj.like" 30 $ " already projection like"
_ -> reportSLn "tc.proj.like" 30 $ " not a function"
where
validProj :: (QName, Int) -> TCM Bool
validProj (_, 0) = return False
validProj (d, _) = eligibleForProjectionLike d
recursive = do
occs <- computeOccurrences x
let xocc = Map.lookup (ADef x) occs
case xocc of
Just (_ : _) -> return True
_ -> return False
checkOccurs cls n = all (nonOccur n) cls
nonOccur n cl =
and [ take n p == [0..n 1]
, onlyMatch n ps
, checkBody n b ]
where
Perm _ p = clausePerm cl
ps = namedClausePats cl
b = clauseBody cl
onlyMatch n ps = all (shallowMatch . namedArg) (take 1 ps1) &&
noMatches (ps0 ++ drop 1 ps1)
where
(ps0, ps1) = splitAt n ps
shallowMatch (ConP _ _ ps) = noMatches ps
shallowMatch _ = True
noMatches = all (noMatch . namedArg)
noMatch ConP{} = False
noMatch LitP{} = False
noMatch ProjP{}= False
noMatch VarP{} = True
noMatch DotP{} = True
checkBody 0 _ = True
checkBody _ NoBody = __IMPOSSIBLE__
checkBody n (Bind b) = not (isBinderUsed b) && checkBody (n 1) (unAbs b)
checkBody _ Body{} = __IMPOSSIBLE__
candidateArgs :: [Term] -> Type -> [(QName,Int)]
candidateArgs vs t =
case ignoreSharing $ unEl t of
Pi a b
| Def d es <- ignoreSharing $ unEl $ unDom a,
Just us <- allApplyElims es,
vs == map unArg us -> (d, length vs) : candidateRec b
| otherwise -> candidateRec b
_ -> []
where
candidateRec NoAbs{} = []
candidateRec (Abs x t) = candidateArgs (var (size vs) : vs) t