module Agda.TypeChecking.ProjectionLike where
import Control.Monad
import qualified Data.Map as Map
import Data.Monoid (Any(..), getAny)
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.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 :: Arg Term
, projViewSpine :: Elims
}
| LoneProjectionLike QName 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 :: HasConstInfo m => Term -> m ProjectionView
projView v = do
let fallback = return $ NoProjection v
case ignoreSharing v of
Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do
if projIndex isP <= 0 then fallback else 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 ProjPrefix f]
| otherwise -> return v
ProjectionView f a es -> (`applyE` (Proj ProjPrefix 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
Function{} -> False
Primitive{} -> False
Constructor{} -> __IMPOSSIBLE__
AbstractDefn -> 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 . clauseBody) 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 pIndex = n + 1
tel = take pIndex $ telToList $ theTel $ telView' t
unless (length tel == pIndex) __IMPOSSIBLE__
let projection = Projection
{ projProper = False
, projOrig = x
, projFromType = d
, projIndex = pIndex
, projLams = ProjLams $ map (\ (Dom ai (y, _)) -> Arg ai y) tel
}
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 :: (Arg QName, Int) -> TCM Bool
validProj (_, 0) = return False
validProj (d, _) = eligibleForProjectionLike (unArg 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 m n b ]
where
Perm _ p = fromMaybe __IMPOSSIBLE__ $ clausePerm cl
ps = namedClausePats cl
b = compiledClauseBody cl
m = size $ concatMap patternVars $ clausePats 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 m n b = not . getAny $ runFree badVar IgnoreNot b
where badVar (x,_) = Any $ m1n < x && x < m
candidateArgs :: [Term] -> Type -> [(Arg 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 <$ argFromDom a, length vs) : candidateRec b
| otherwise -> candidateRec b
_ -> []
where
candidateRec NoAbs{} = []
candidateRec (Abs x t) = candidateArgs (var (size vs) : vs) t