diff options
Diffstat (limited to 'src/full/Agda/TypeChecking/Injectivity.hs')
| -rw-r--r-- | src/full/Agda/TypeChecking/Injectivity.hs | 36 |
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__ |