1 2-- | Dropping initial arguments (``parameters'') from a function which can be 3-- easily reconstructed from its principal argument. 4-- 5-- A function which has such parameters is called ``projection-like''. 6-- 7-- The motivation for this optimization comes from the use of nested records. 8-- 9-- First, let us look why proper projections need not store the parameters: 10-- The type of a projection @f@ is of the form 11-- @ 12-- f : Γ → R Γ → C 13-- @ 14-- where @R@ is the record type and @C@ is the type of the field @f@. 15-- Given a projection application 16-- @ 17-- p pars u 18-- @ 19-- we know that the type of the principal argument @u@ is 20-- @ 21-- u : R pars 22-- @ 23-- thus, the parameters @pars@ are redundant in the projection application 24-- if we can always infer the type of @u@. 25-- For projections, this is case, because the principal argument @u@ must be 26-- neutral; otherwise, if it was a record value, we would have a redex, 27-- yet Agda maintains a β-normal form. 28-- 29-- The situation for projections can be generalized to ``projection-like'' 30-- functions @f@. Conditions: 31-- 32-- 1. The type of @f@ is of the form @f : Γ → D Γ → ...@ for some 33-- type constructor @D@ which can never reduce. 34-- 35-- 2. For every reduced welltyped application @f pars u ...@, 36-- the type of @u@ is inferable. 37-- 38-- This then allows @pars@ to be dropped always. 39-- 40-- Condition 2 is approximated by a bunch of criteria, for details see function 41-- 'makeProjection'. 42-- 43-- Typical projection-like functions are compositions of projections 44-- which arise from nested records. 45-- 46-- Notes: 47-- 48-- 1. This analysis could be dualized to ``constructor-like'' functions 49-- whose parameters are reconstructable from the target type. 50-- But such functions would need to be fully applied. 51-- 52-- 2. A more general analysis of which arguments are reconstructible 53-- can be found in 54-- 55-- Jason C. Reed, Redundancy elimination for LF 56-- LFTMP 2004. 57 58module Agda.TypeChecking.ProjectionLike where 59 60import Control.Monad 61 62import qualified Data.Map as Map 63import Data.Monoid (Any(..), getAny) 64 65import Agda.Interaction.Options 66 67import Agda.Syntax.Abstract.Name 68import Agda.Syntax.Common 69import Agda.Syntax.Internal 70import Agda.Syntax.Internal.Pattern 71 72import Agda.TypeChecking.Monad 73import Agda.TypeChecking.Free (runFree, IgnoreSorts(..)) 74import Agda.TypeChecking.Substitute 75import Agda.TypeChecking.Positivity 76import Agda.TypeChecking.Pretty 77import Agda.TypeChecking.Reduce (reduce) 78 79import Agda.TypeChecking.DropArgs 80 81import Agda.Utils.List 82import Agda.Utils.Maybe 83import Agda.Utils.Monad 84import Agda.Utils.Permutation 85import Agda.Utils.Pretty ( prettyShow ) 86import Agda.Utils.Size 87 88import Agda.Utils.Impossible 89 90-- | View for a @Def f (Apply a : es)@ where @isProjection f@. 91-- Used for projection-like @f@s. 92data ProjectionView 93 = ProjectionView 94 { projViewProj :: QName 95 , projViewSelf :: Arg Term 96 , projViewSpine :: Elims 97 } 98 -- ^ A projection or projection-like function, applied to its 99 -- principal argument 100 | LoneProjectionLike QName ArgInfo 101 -- ^ Just a lone projection-like function, missing its principal 102 -- argument (from which we could infer the parameters). 103 | NoProjection Term 104 -- ^ Not a projection or projection-like thing. 105 106-- | Semantics of 'ProjectionView'. 107unProjView :: ProjectionView -> Term 108unProjView pv = 109 case pv of 110 ProjectionView f a es -> Def f (Apply a : es) 111 LoneProjectionLike f ai -> Def f [] 112 NoProjection v -> v 113 114-- | Top-level 'ProjectionView' (no reduction). 115{-# SPECIALIZE projView :: Term -> TCM ProjectionView #-} 116projView :: HasConstInfo m => Term -> m ProjectionView 117projView v = do 118 let fallback = return $ NoProjection v 119 case v of 120 Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do 121 if projIndex isP <= 0 then fallback else do 122 case es of 123 [] -> return $ LoneProjectionLike f $ projArgInfo isP 124 Apply a : es -> return $ ProjectionView f a es 125 -- Since a projection is a function, it cannot be projected itself. 126 Proj{} : _ -> __IMPOSSIBLE__ 127 -- The principal argument of a projection-like cannot be the interval? 128 IApply{} : _ -> __IMPOSSIBLE__ 129 130 _ -> fallback 131 132-- | Reduce away top-level projection like functions. 133-- (Also reduces projections, but they should not be there, 134-- since Internal is in lambda- and projection-beta-normal form.) 135-- 136reduceProjectionLike :: PureTCM m => Term -> m Term 137reduceProjectionLike v = do 138 -- Andreas, 2013-11-01 make sure we do not reduce a constructor 139 -- because that could be folded back into a literal by reduce. 140 pv <- projView v 141 case pv of 142 ProjectionView{} -> onlyReduceProjections $ reduce v 143 -- ordinary reduce, only different for Def's 144 _ -> return v 145 146data ProjEliminator = EvenLone | ButLone | NoPostfix 147 deriving Eq 148 149-- | Turn prefix projection-like function application into postfix ones. 150-- This does just one layer, such that the top spine contains 151-- the projection-like functions as projections. 152-- Used in 'compareElims' in @TypeChecking.Conversion@ 153-- and in "Agda.TypeChecking.CheckInternal". 154-- 155-- If the 'Bool' is 'True', a lone projection like function will be 156-- turned into a lambda-abstraction, expecting the principal argument. 157-- If the 'Bool' is 'False', it will be returned unaltered. 158-- 159-- No precondition. 160-- Preserves constructorForm, since it really does only something 161-- on (applications of) projection-like functions. 162elimView :: PureTCM m => ProjEliminator -> Term -> m Term 163elimView pe v = do 164 reportSDoc "tc.conv.elim" 30 $ "elimView of " <+> prettyTCM v 165 v <- reduceProjectionLike v 166 reportSDoc "tc.conv.elim" 40 $ 167 "elimView (projections reduced) of " <+> prettyTCM v 168 case pe of 169 NoPostfix -> return v 170 _ -> do 171 pv <- projView v 172 case pv of 173 NoProjection{} -> return v 174 LoneProjectionLike f ai 175 | pe==EvenLone -> return $ Lam ai $ Abs "r" $ Var 0 [Proj ProjPrefix f] 176 | otherwise -> return v 177 ProjectionView f a es -> (`applyE` (Proj ProjPrefix f : es)) <$> elimView pe (unArg a) 178 179-- | Which @Def@types are eligible for the principle argument 180-- of a projection-like function? 181eligibleForProjectionLike :: (HasConstInfo m) => QName -> m Bool 182eligibleForProjectionLike d = eligible . theDef <$> getConstInfo d 183 where 184 eligible = \case 185 Datatype{} -> True 186 Record{} -> True 187 Axiom{} -> True 188 DataOrRecSig{} -> True 189 GeneralizableVar{} -> False 190 Function{} -> False 191 Primitive{} -> False 192 PrimitiveSort{} -> False 193 Constructor{} -> __IMPOSSIBLE__ 194 AbstractDefn d -> eligible d 195 -- Andreas, 2017-08-14, issue #2682: 196 -- Abstract records still export the projections. 197 -- Andreas, 2016-10-11 AIM XXIV 198 -- Projection-like at abstract types violates the parameter reconstructibility property. 199 -- See test/Fail/AbstractTypeProjectionLike. 200 201-- | Turn a definition into a projection if it looks like a projection. 202-- 203-- Conditions for projection-likeness of @f@: 204-- 205-- 1. The type of @f@ must be of the shape @Γ → D Γ → C@ for @D@ 206-- a name (@Def@) which is 'eligibleForProjectionLike': 207-- @data@ / @record@ / @postulate@. 208-- 209-- 2. The application of f should only get stuck if the principal argument 210-- is inferable (neutral). Thus: 211-- 212-- a. @f@ cannot have absurd clauses (which are stuck even if the principal 213-- argument is a constructor). 214-- 215-- b. @f@ cannot be abstract as it does not reduce outside abstract blocks 216-- (always stuck). 217-- 218-- c. @f@ cannot match on other arguments than the principal argument. 219-- 220-- d. @f@ cannot match deeply. 221-- 222-- e. @f@s body may not mention the parameters. 223-- 224-- f. A rhs of @f@ cannot be a record expression, since this will be 225-- translated to copatterns by recordExpressionsToCopatterns. 226-- Thus, an application of @f@ waiting for a projection 227-- can be stuck even when the principal argument is a constructor. 228-- 229-- 230-- For internal reasons: 231-- 232-- 3. @f@ cannot be constructor headed 233-- 234-- 4. @f@ cannot be recursive, since we have not implemented a function 235-- which goes through the bodies of the @f@ and the mutually recursive 236-- functions and drops the parameters from all applications of @f@. 237-- 238-- Examples for these reasons: see test/Succeed/NotProjectionLike.agda 239 240makeProjection :: QName -> TCM () 241makeProjection x = whenM (optProjectionLike <$> pragmaOptions) $ do 242 inTopContext $ do 243 reportSLn "tc.proj.like" 70 $ "Considering " ++ prettyShow x ++ " for projection likeness" 244 defn <- getConstInfo x 245 let t = defType defn 246 reportSDoc "tc.proj.like" 20 $ sep 247 [ "Checking for projection likeness " 248 , prettyTCM x <+> " : " <+> prettyTCM t 249 ] 250 case theDef defn of 251 Function{funClauses = cls} 252 | any (isNothing . clauseBody) cls -> 253 reportSLn "tc.proj.like" 30 $ " projection-like functions cannot have absurd clauses" 254 | any (maybe __IMPOSSIBLE__ isRecordExpression . clauseBody) cls -> 255 reportSLn "tc.proj.like" 30 $ " projection-like functions cannot have record rhss" 256 -- Constructor-headed functions can't be projection-like (at the moment). The reason 257 -- for this is that invoking constructor-headedness will circumvent the inference of 258 -- the dropped arguments. 259 -- Nor can abstract definitions be projection-like since they won't reduce 260 -- outside the abstract block. 261 def@Function{funProjection = Nothing, funClauses = cls, 262 funSplitTree = st0, funCompiled = cc0, funInv = NotInjective, 263 funMutual = Just [], -- Andreas, 2012-09-28: only consider non-mutual funs 264 funAbstr = ConcreteDef} -> do 265 ps0 <- filterM validProj $ candidateArgs [] t 266 reportSLn "tc.proj.like" 30 $ if null ps0 then " no candidates found" 267 else " candidates: " ++ prettyShow ps0 268 unless (null ps0) $ do 269 -- Andreas 2012-09-26: only consider non-recursive functions for proj.like. 270 -- Issue 700: problems with recursive funs. in term.checker and reduction 271 ifM recursive (reportSLn "tc.proj.like" 30 $ " recursive functions are not considered for projection-likeness") $ do 272 {- else -} 273 case lastMaybe (filter (checkOccurs cls . snd) ps0) of 274 Nothing -> reportSDoc "tc.proj.like" 50 $ nest 2 $ vcat 275 [ "occurs check failed" 276 , nest 2 $ "clauses =" <?> vcat (map pretty cls) ] 277 Just (d, n) -> do 278 -- Yes, we are projection-like! 279 reportSDoc "tc.proj.like" 10 $ vcat 280 [ prettyTCM x <+> " : " <+> prettyTCM t 281 , nest 2 $ sep 282 [ "is projection like in argument", prettyTCM n, "for type", prettyTCM (unArg d) ] 283 ] 284 __CRASH_WHEN__ "tc.proj.like.crash" 1000 285 286 let cls' = map (dropArgs n) cls 287 cc = dropArgs n cc0 288 st = dropArgs n st0 289 reportSLn "tc.proj.like" 60 $ unlines 290 [ " rewrote clauses to" 291 , " " ++ show cc 292 ] 293 294 -- Andreas, 2013-10-20 build parameter dropping function 295 let pIndex = n + 1 296 tel = take pIndex $ telToList $ theTel $ telView' t 297 unless (length tel == pIndex) __IMPOSSIBLE__ 298 let projection = Projection 299 { projProper = Nothing 300 , projOrig = x 301 , projFromType = d 302 , projIndex = pIndex 303 , projLams = ProjLams $ map (argFromDom . fmap fst) tel 304 } 305 let newDef = def 306 { funProjection = Just projection 307 , funClauses = cls' 308 , funSplitTree = st 309 , funCompiled = cc 310 , funInv = dropArgs n $ funInv def 311 } 312 addConstant x $ defn { defPolarity = drop n $ defPolarity defn 313 , defArgOccurrences = drop n $ defArgOccurrences defn 314 , defDisplay = [] 315 , theDef = newDef 316 } 317 Function{funInv = Inverse{}} -> 318 reportSLn "tc.proj.like" 30 $ " injective functions can't be projections" 319 Function{funAbstr = AbstractDef} -> 320 reportSLn "tc.proj.like" 30 $ " abstract functions can't be projections" 321 Function{funProjection = Just{}} -> 322 reportSLn "tc.proj.like" 30 $ " already projection like" 323 Function{funMutual = Just (_:_)} -> 324 reportSLn "tc.proj.like" 30 $ " mutual functions can't be projections" 325 Function{funMutual = Nothing} -> 326 reportSLn "tc.proj.like" 30 $ " mutuality check has not run yet" 327 Axiom{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Axiom" 328 DataOrRecSig{} -> reportSLn "tc.proj.like" 30 $ " not a function, but DataOrRecSig" 329 GeneralizableVar{} -> reportSLn "tc.proj.like" 30 $ " not a function, but GeneralizableVar" 330 AbstractDefn{} -> reportSLn "tc.proj.like" 30 $ " not a function, but AbstractDefn" 331 Constructor{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Constructor" 332 Datatype{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Datatype" 333 Primitive{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Primitive" 334 PrimitiveSort{} -> reportSLn "tc.proj.like" 30 $ " not a function, but PrimitiveSort" 335 Record{} -> reportSLn "tc.proj.like" 30 $ " not a function, but Record" 336 where 337 -- If the user wrote a record expression as rhs, 338 -- the recordExpressionsToCopatterns translation will turn this into copatterns, 339 -- violating the conditions of projection-likeness. 340 -- Andreas, 2019-07-11, issue #3843. 341 isRecordExpression :: Term -> Bool 342 isRecordExpression = \case 343 Con _ ConORec _ -> True 344 _ -> False 345 -- @validProj (d,n)@ checks whether the head @d@ of the type of the 346 -- @n@th argument is injective in all args (i.d. being name of data/record/axiom). 347 validProj :: (Arg QName, Int) -> TCM Bool 348 validProj (_, 0) = return False 349 validProj (d, _) = eligibleForProjectionLike (unArg d) 350 351 -- NOTE: If the following definition turns out to be slow, then 352 -- one could perhaps reuse information computed by the termination 353 -- and/or positivity checkers. 354 recursive = do 355 occs <- computeOccurrences x 356 case Map.lookup (ADef x) occs of 357 Just n | n >= 1 -> return True -- recursive occurrence 358 _ -> return False 359 360 checkOccurs cls n = all (nonOccur n) cls 361 362 nonOccur n cl = 363 (take n p == [0..n - 1]) && 364 onlyMatch n ps && -- projection-like functions are only allowed to match on the eliminatee 365 -- otherwise we may end up projecting from constructor applications, in 366 -- which case we can't reconstruct the dropped parameters 367 checkBody m n b 368 where 369 Perm _ p = fromMaybe __IMPOSSIBLE__ $ clausePerm cl 370 ps = namedClausePats cl 371 b = compiledClauseBody cl -- Renumbers variables to match order in patterns 372 -- and includes dot patterns as variables. 373 m = size $ concatMap patternVars ps -- This also counts dot patterns! 374 375 376 onlyMatch n ps = all (shallowMatch . namedArg) (take 1 ps1) && 377 noMatches (ps0 ++ drop 1 ps1) 378 where 379 (ps0, ps1) = splitAt n ps 380 shallowMatch (ConP _ _ ps) = noMatches ps 381 shallowMatch _ = True 382 noMatches = all (noMatch . namedArg) 383 noMatch ConP{} = False 384 noMatch DefP{} = False 385 noMatch LitP{} = False 386 noMatch ProjP{}= False 387 noMatch VarP{} = True 388 noMatch DotP{} = True 389 noMatch IApplyP{} = True 390 391 -- Make sure non of the parameters occurs in the body of the function. 392 checkBody m n b = not . getAny $ runFree badVar IgnoreNot b 393 where badVar x = Any $ m - n <= x && x < m 394 395 -- @candidateArgs [var 0,...,var(n-1)] t@ adds @(n,d)@ to the output, 396 -- if @t@ is a function-type with domain @t 0 .. (n-1)@ 397 -- (the domain of @t@ is the type of the arg @n@). 398 -- 399 -- This means that from the type of arg @n@ all previous arguments 400 -- can be computed by a simple matching. 401 -- (Provided the @d@ is data/record/postulate, checked in @validProj@). 402 -- 403 -- E.g. f : {x : _}(y : _){z : _} -> D x y z -> ... 404 -- will return (D,3) as a candidate (amongst maybe others). 405 -- 406 candidateArgs :: [Term] -> Type -> [(Arg QName, Int)] 407 candidateArgs vs t = 408 case unEl t of 409 Pi a b 410 | Def d es <- unEl $ unDom a, 411 Just us <- allApplyElims es, 412 vs == map unArg us -> (d <$ argFromDom a, length vs) : candidateRec b 413 | otherwise -> candidateRec b 414 _ -> [] 415 where 416 candidateRec NoAbs{} = [] 417 candidateRec (Abs x t) = candidateArgs (var (size vs) : vs) t 418