{-# LANGUAGE CPP #-}
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.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
#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
{-# SPECIALIZE projView :: Term -> TCM ProjectionView #-}
projView :: HasConstInfo m => Term -> m ProjectionView
projView v = do
let fallback = return $ NoProjection v
case 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__
IApply{} : _ -> __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 $ "elimView of " <+> prettyTCM v
reportSLn "tc.conv.elim" 50 $ "v = " ++ show v
v <- reduceProjectionLike v
reportSDoc "tc.conv.elim" 40 $
"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 :: (HasConstInfo m) => QName -> m Bool
eligibleForProjectionLike d = eligible . theDef <$> getConstInfo d
where
eligible = \case
Datatype{} -> True
Record{} -> True
Axiom{} -> True
DataOrRecSig{} -> True
GeneralizableVar{} -> False
Function{} -> False
Primitive{} -> False
Constructor{} -> __IMPOSSIBLE__
AbstractDefn d -> eligible d
makeProjection :: QName -> TCM ()
makeProjection x =
inTopContext $ do
reportSLn "tc.proj.like" 70 $ "Considering " ++ prettyShow x ++ " for projection likeness"
defn <- getConstInfo x
let t = defType defn
reportSDoc "tc.proj.like" 20 $ sep
[ "Checking for projection likeness "
, prettyTCM x <+> " : " <+> 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,
funSplitTree = st0, funCompiled = cc0, funInv = NotInjective,
funMutual = Just [],
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
case lastMaybe (filter (checkOccurs cls . snd) ps0) of
Nothing -> reportSDoc "tc.proj.like" 50 $ nest 2 $ vcat
[ "occurs check failed"
, nest 2 $ "clauses =" <?> vcat (map pretty cls) ]
Just (d, n) -> do
reportSDoc "tc.proj.like" 10 $ sep
[ prettyTCM x <+> " : " <+> prettyTCM t
, text $ " is projection like in argument " ++ show n ++ " for type " ++ show d
]
__CRASH_WHEN__ "tc.proj.like.crash" 1000
let cls' = map (dropArgs n) cls
cc = dropArgs n cc0
st = dropArgs n st0
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 = Nothing
, projOrig = x
, projFromType = d
, projIndex = pIndex
, projLams = ProjLams $ map (argFromDom . fmap fst) tel
}
let newDef = def
{ funProjection = Just projection
, funClauses = cls'
, funSplitTree = st
, 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"
Function{funMutual = Just (_:_)} ->
reportSLn "tc.proj.like" 30 $ " mutual functions can't be projections"
Function{funMutual = Nothing} ->
reportSLn "tc.proj.like" 30 $ " mutuality check has not run yet"
Axiom -> reportSLn "tc.proj.like" 30 $ " not a function, but Axiom"
DataOrRecSig{} -> reportSLn "tc.proj.like" 30 $ " not a function, but DataOrRecSig"
GeneralizableVar{} -> reportSLn "tc.proj.like" 30 $ " not a function, but GeneralizableVar"
AbstractDefn{} -> reportSLn "tc.proj.like" 30 $ " not a function, but AbstractDefn"
Constructor{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Constructor"
Datatype{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Datatype"
Primitive{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Primitive"
Record{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Record"
where
validProj :: (Arg QName, Int) -> TCM Bool
validProj (_, 0) = return False
validProj (d, _) = eligibleForProjectionLike (unArg d)
recursive = do
occs <- computeOccurrences x
case Map.lookup (ADef x) occs of
Just n | n >= 1 -> 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 ps
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 DefP{} = False
noMatch LitP{} = False
noMatch ProjP{}= False
noMatch VarP{} = True
noMatch DotP{} = True
noMatch IApplyP{} = True
checkBody m n b = not . getAny $ runFree badVar IgnoreNot b
where badVar x = Any $ m - n <= x && x < m
candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
candidateArgs vs t =
case unEl t of
Pi a b
| Def d es <- 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