module Agda.TypeChecking.Injectivity where
import Prelude hiding (mapM)
import Control.Applicative
import Control.Monad.State hiding (mapM, forM)
import Control.Monad.Reader hiding (mapM, forM)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.Traversable hiding (for)
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Polarity
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.List
import Agda.Utils.Functor
import Agda.Utils.Permutation
#include "undefined.h"
import Agda.Utils.Impossible
headSymbol :: Term -> TCM (Maybe TermHead)
headSymbol v = do
v <- ignoreBlocking <$> reduceHead v
case ignoreSharing v of
Def f _ -> do
def <- theDef <$> do ignoreAbstractMode $ getConstInfo f
case def of
Datatype{} -> return (Just $ ConsHead f)
Record{} -> return (Just $ ConsHead f)
Axiom{} -> do
reportSLn "tc.inj.axiom" 50 $ "headSymbol: " ++ show f ++ " is an Axiom."
fs <- lookupMutualBlock =<< currentOrFreshMutualBlock
if Set.member f fs
then return Nothing
else return (Just $ ConsHead f)
Function{} -> return Nothing
Primitive{} -> return Nothing
Constructor{} -> __IMPOSSIBLE__
Con c _ -> return (Just $ ConsHead $ conName c)
Sort _ -> return (Just SortHead)
Pi _ _ -> return (Just PiHead)
Lit _ -> return Nothing
Lam{} -> return Nothing
Var{} -> return Nothing
Level{} -> return Nothing
MetaV{} -> return Nothing
DontCare{} -> return Nothing
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
checkInjectivity f cs
| pointLess cs = do
reportSLn "tc.inj.check.pointless" 20 $
"Injectivity of " ++ show (A.qnameToConcrete f) ++ " would be pointless."
return NotInjective
where
pointLess [] = True
pointLess (_:_:_) = False
pointLess [cl] = not $ any (properlyMatching . unArg) $ clausePats cl
checkInjectivity f cs = do
reportSLn "tc.inj.check" 40 $ "Checking injectivity of " ++ show f
es <- catMaybes <$> do
forM cs $ \ c -> do
mapM ((,c) <.> headSymbol) $ getBodyUnraised c
let (hs, ps) = unzip es
reportSLn "tc.inj.check" 40 $ " right hand sides: " ++ show hs
if all isJust hs && distinct hs
then do
let inv = Map.fromList (map fromJust hs `zip` ps)
reportSLn "tc.inj.check" 20 $ show f ++ " is injective."
reportSDoc "tc.inj.check" 30 $ nest 2 $ vcat $
for (Map.toList inv) $ \ (h, c) ->
text (show h) <+> text "-->" <+>
fsep (punctuate comma $ map (prettyTCM . unArg) $ clausePats c)
return $ Inverse inv
else return NotInjective
functionInverse :: Term -> TCM InvView
functionInverse v = case ignoreSharing v of
Def f es -> do
d <- theDef <$> getConstInfo f
case d of
Function{ funInv = inv } -> case inv of
NotInjective -> return NoInv
Inverse m -> return $ Inv f es m
_ -> return NoInv
_ -> return NoInv
data InvView = Inv QName [Elim] (Map TermHead Clause)
| NoInv
data MaybeAbort = Abort | KeepGoing
useInjectivity :: Comparison -> Type -> Term -> Term -> TCM ()
useInjectivity cmp a u v = do
reportSDoc "tc.inj.use" 30 $ fsep $
pwords "useInjectivity on" ++
[ prettyTCM u, prettyTCM cmp, prettyTCM v, text ":", prettyTCM a
]
uinv <- functionInverse u
vinv <- functionInverse v
case (uinv, vinv) of
(Inv f fArgs _, Inv g gArgs _)
| f == g -> do
a <- defType <$> getConstInfo f
reportSDoc "tc.inj.use" 20 $ vcat
[ fsep (pwords "comparing application of injective function" ++ [prettyTCM f] ++
pwords "at")
, nest 2 $ fsep $ punctuate comma $ map prettyTCM fArgs
, nest 2 $ fsep $ punctuate comma $ map prettyTCM gArgs
, nest 2 $ text "and type" <+> prettyTCM a
]
pol <- getPolarity' cmp f
compareElims pol a (Def f []) fArgs gArgs
| otherwise -> fallBack
(Inv f args inv, NoInv) -> do
a <- defType <$> getConstInfo f
reportSDoc "tc.inj.use" 20 $ fsep $
pwords "inverting injective function" ++
[ prettyTCM f, text ":", prettyTCM a, text "for", prettyTCM v
, parens $ text "args =" <+> prettyList (map prettyTCM args)
]
invert u f a inv args =<< headSymbol v
(NoInv, Inv g args inv) -> do
a <- defType <$> getConstInfo g
reportSDoc "tc.inj.use" 20 $ fsep $
pwords "inverting injective function" ++
[ prettyTCM g, text ":", prettyTCM a, text "for", prettyTCM u
, parens $ text "args =" <+> prettyList (map prettyTCM args)
]
invert v g a inv args =<< headSymbol u
(NoInv, NoInv) -> fallBack
where
fallBack = addConstraint $ ValueCmp cmp a u v
invert :: Term -> QName -> Type -> Map TermHead Clause -> [Elim] -> Maybe TermHead -> TCM ()
invert _ _ a inv args Nothing = fallBack
invert org f ftype inv args (Just h) = case Map.lookup h inv of
Nothing -> typeError $ UnequalTerms cmp u v a
Just cl@Clause{ clauseTel = tel
, clausePerm = perm } -> maybeAbort $ do
let ps = clausePats cl
ms <- map unArg <$> newTelMeta tel
reportSDoc "tc.inj.invert" 20 $ vcat
[ text "meta patterns" <+> prettyList (map prettyTCM ms)
, text " perm =" <+> text (show perm)
, text " tel =" <+> prettyTCM tel
, text " ps =" <+> prettyList (map (text . show) ps)
]
let ms' = permute (invertP __IMPOSSIBLE__ $ compactP perm) ms
let sub = parallelS (reverse ms)
margs <- runReaderT (evalStateT (mapM metaElim ps) ms') sub
reportSDoc "tc.inj.invert" 20 $ vcat
[ text "inversion"
, nest 2 $ vcat
[ text "lhs =" <+> prettyTCM margs
, text "rhs =" <+> prettyTCM args
, text "type =" <+> prettyTCM ftype
]
]
pol <- purgeNonvariant <$> getPolarity' cmp f
let args' = take (length margs) args
compareElims pol ftype org margs args'
org <- reduce org
h <- headSymbol org
case h of
Just h -> KeepGoing <$ compareTerm cmp a u v
Nothing -> do
reportSDoc "tc.inj.invert" 30 $ vcat
[ text "aborting inversion;" <+> prettyTCM org
, text "plainly," <+> text (show org)
, text "has TermHead" <+> text (show h)
, text "which does not expose a constructor"
]
return Abort
maybeAbort m = do
(a, s) <- localTCStateSaving m
case a of
KeepGoing -> put s
Abort -> fallBack
nextMeta = do
m : ms <- get
put ms
return m
dotP :: Monad m => Term -> StateT [Term] (ReaderT Substitution m) Term
dotP v = do
sub <- ask
return $ applySubst sub v
metaElim (Arg _ (ProjP p)) = return $ Proj p
metaElim (Arg info p) = Apply . Arg info <$> metaPat p
metaArgs args = mapM (traverse $ metaPat . namedThing) args
metaPat (DotP v) = dotP v
metaPat (VarP _) = nextMeta
metaPat (ConP c mt args) = Con c <$> metaArgs args
metaPat (LitP l) = return $ Lit l
metaPat ProjP{} = __IMPOSSIBLE__