summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/ProjectionLike.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/ProjectionLike.hs')
-rw-r--r--src/full/Agda/TypeChecking/ProjectionLike.hs44
1 files changed, 12 insertions, 32 deletions
diff --git a/src/full/Agda/TypeChecking/ProjectionLike.hs b/src/full/Agda/TypeChecking/ProjectionLike.hs
index 8269586..f86bee9 100644
--- a/src/full/Agda/TypeChecking/ProjectionLike.hs
+++ b/src/full/Agda/TypeChecking/ProjectionLike.hs
@@ -1,7 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ FlexibleInstances,
+ PatternGuards #-}
+
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
module Agda.TypeChecking.ProjectionLike where
@@ -55,11 +59,13 @@ unProjView pv =
NoProjection v -> v
-- | Top-level 'ProjectionView' (no reduction).
-projView :: Term -> TCM ProjectionView
+{-# SPECIALIZE projView :: Term -> TCM ProjectionView #-}
+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
@@ -85,7 +91,7 @@ reduceProjectionLike v = do
-- This does just one layer, such that the top spine contains
-- the projection-like functions as projections.
-- Used in 'compareElims' in @TypeChecking.Conversion@
--- and in 'Agda.TypeChecking.CheckInternal'.
+-- and in "Agda.TypeChecking.CheckInternal".
--
-- If the 'Bool' is 'True', a lone projection like function will be
-- turned into a lambda-abstraction, expecting the principal argument.
@@ -109,18 +115,6 @@ elimView loneProjToLambda v = do
| otherwise -> return v
ProjectionView f a es -> (`applyE` (Proj f : es)) <$> elimView loneProjToLambda (unArg a)
-{- Andreas, 2013-11-01: Use of unLevel no longer necessary, since we do not reduce!
- case ignoreSharing v of
- Def f (Apply (Arg _ rv) : es) -> do
- flip (maybeM (return v)) (isProjection f) $ \ _ -> do
- (`applyE` (Proj f : es)) <$> do elimView =<< unLevel =<< reduce rv
- -- domi 2012-7-24: Add unLevel to handle neutral levels.
- -- The problem is that reduce turns @suc (neutral)@
- -- into @Level (Max [Plus 1 (NeutralLevel neutral)])@
- -- which the below pattern match does not handle.
- _ -> return v
--}
-
-- | Which @Def@types are eligible for the principle argument
-- of a projection-like function?
eligibleForProjectionLike :: QName -> TCM Bool
@@ -282,17 +276,3 @@ makeProjection x = inTopContext $ do
where
candidateRec NoAbs{} = []
candidateRec (Abs x t) = candidateArgs (var (size vs) : vs) t
-
-{-
- candidateArgs :: [Term] -> Term -> [(QName,Int)]
- candidateArgs vs (Shared p) = candidateArgs vs $ derefPtr p
- candidateArgs vs (Pi (Dom info (El _ def)) b)
- | Def d es <- ignoreSharing def,
- Just us <- allApplyElims es,
- vs == map unArg us = (d, length vs) : candidateRec vs b
- candidateArgs vs (Pi _ b) = candidateRec vs b
- candidateArgs _ _ = []
-
- candidateRec vs NoAbs{} = []
- candidateRec vs b = candidateArgs (var (size vs) : vs) (unEl $ absBody b)
--}