summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Injectivity.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Injectivity.hs')
-rw-r--r--src/full/Agda/TypeChecking/Injectivity.hs36
1 files changed, 19 insertions, 17 deletions
diff --git a/src/full/Agda/TypeChecking/Injectivity.hs b/src/full/Agda/TypeChecking/Injectivity.hs
index a53b7b3..f447db1 100644
--- a/src/full/Agda/TypeChecking/Injectivity.hs
+++ b/src/full/Agda/TypeChecking/Injectivity.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE TupleSections #-}
module Agda.TypeChecking.Injectivity where
@@ -31,8 +30,9 @@ 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.List
+import Agda.Utils.Maybe
import Agda.Utils.Permutation
#include "undefined.h"
@@ -45,26 +45,28 @@ headSymbol v = do -- ignoreAbstractMode $ do
v <- ignoreBlocking <$> reduceHead v
case ignoreSharing v of
Def f _ -> do
+ let yes = return $ Just $ ConsHead f
+ no = return $ Nothing
def <- theDef <$> do ignoreAbstractMode $ getConstInfo f
-- Andreas, 2013-02-18
-- if we do not ignoreAbstractMode here, abstract Functions get turned
-- into Axioms, but we want to distinguish these.
case def of
- Datatype{} -> return (Just $ ConsHead f)
- Record{} -> return (Just $ ConsHead f)
+ Datatype{} -> yes
+ Record{} -> yes
Axiom{} -> do
reportSLn "tc.inj.axiom" 50 $ "headSymbol: " ++ show f ++ " is an Axiom."
-- Don't treat axioms in the current mutual block
-- as constructors (they might have definitions we
-- don't know about yet).
- fs <- lookupMutualBlock =<< currentOrFreshMutualBlock
- if Set.member f fs
- then return Nothing
- else return (Just $ ConsHead f)
- Function{} -> return Nothing
- Primitive{} -> return Nothing
+ caseMaybeM (asks envMutualBlock) yes $ \ mb -> do
+ fs <- mutualNames <$> lookupMutualBlock mb
+ if Set.member f fs then no else yes
+ Function{} -> no
+ Primitive{} -> no
Constructor{} -> __IMPOSSIBLE__
- Con c _ -> return (Just $ ConsHead $ conName c)
+ AbstractDefn -> __IMPOSSIBLE__
+ Con c _ _ -> return (Just $ ConsHead $ conName c)
Sort _ -> return (Just SortHead)
Pi _ _ -> return (Just PiHead)
Lit _ -> return Nothing -- handle literal heads as well? can't think of
@@ -86,7 +88,7 @@ checkInjectivity f cs
-- Is it pointless to use injectivity for this function?
pointLess [] = True
pointLess (_:_:_) = False
- pointLess [cl] = not $ any (properlyMatching . unArg) $ clausePats cl
+ pointLess [cl] = not $ any (properlyMatching . namedArg) $ namedClausePats cl
-- Andreas, 2014-06-12
-- If we only have record patterns, it is also pointless.
-- We need at least one proper match.
@@ -95,7 +97,7 @@ checkInjectivity f cs = do
-- Extract the head symbol of the rhs of each clause (skip absurd clauses)
es <- catMaybes <$> do
forM cs $ \ c -> do -- produces a list ...
- mapM ((,c) <.> headSymbol) $ getBodyUnraised c -- ... of maybes
+ mapM ((,c) <.> headSymbol) $ clauseBody c -- ... of maybes
let (hs, ps) = unzip es
reportSLn "tc.inj.check" 40 $ " right hand sides: " ++ show hs
if all isJust hs && distinct hs
@@ -105,7 +107,7 @@ checkInjectivity f cs = do
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)
+ fsep (punctuate comma $ map (prettyTCM . namedArg) $ namedClausePats c)
return $ Inverse inv
else return NotInjective
@@ -183,7 +185,7 @@ useInjectivity cmp a u v = do
Nothing -> typeError $ UnequalTerms cmp u v a
Just cl@Clause{ clauseTel = tel } -> maybeAbort $ do
let ps = clausePats cl
- perm = clausePerm cl
+ perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl
-- These are what dot patterns should be instantiated at
ms <- map unArg <$> newTelMeta tel
reportSDoc "tc.inj.invert" 20 $ vcat
@@ -249,13 +251,13 @@ useInjectivity cmp a u v = do
sub <- ask
return $ applySubst sub v
- metaElim (Arg _ (ProjP p)) = return $ Proj p
+ metaElim (Arg _ (ProjP o p)) = lift $ lift $ Proj o <$> getOriginalProjection 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 (ConP c mt args) = Con c (fromConPatternInfo mt) <$> metaArgs args
metaPat (LitP l) = return $ Lit l
metaPat ProjP{} = __IMPOSSIBLE__