1{-# LANGUAGE NondecreasingIndentation #-} 2 3{-| 4 Translating from internal syntax to abstract syntax. Enables nice 5 pretty printing of internal syntax. 6 7 TODO 8 9 - numbers on metas 10 - fake dependent functions to independent functions 11 - meta parameters 12 - shadowing 13-} 14module Agda.Syntax.Translation.InternalToAbstract 15 ( Reify(..) 16 , MonadReify 17 , NamedClause(..) 18 , reifyPatterns 19 , reifyUnblocked 20 , blankNotInScope 21 , reifyDisplayFormP 22 ) where 23 24import Prelude hiding (null) 25 26import Control.Applicative (liftA2) 27import Control.Arrow ((&&&)) 28import Control.Monad.State 29 30import qualified Data.List as List 31import qualified Data.Map as Map 32import Data.Maybe 33import Data.Semigroup ( Semigroup, (<>) ) 34import Data.Set (Set) 35import qualified Data.Set as Set 36import qualified Data.Text as T 37import Data.Traversable (mapM) 38 39import Agda.Syntax.Literal 40import Agda.Syntax.Position 41import Agda.Syntax.Common 42import qualified Agda.Syntax.Concrete.Name as C 43import Agda.Syntax.Concrete (FieldAssignment'(..)) 44import Agda.Syntax.Info as Info 45import Agda.Syntax.Abstract as A hiding (Binder) 46import qualified Agda.Syntax.Abstract as A 47import Agda.Syntax.Abstract.Pattern 48import Agda.Syntax.Abstract.Pretty 49import Agda.Syntax.Internal as I 50import Agda.Syntax.Internal.Pattern as I 51import Agda.Syntax.Scope.Base (inverseScopeLookupName) 52 53import Agda.TypeChecking.Monad 54import Agda.TypeChecking.Reduce 55import {-# SOURCE #-} Agda.TypeChecking.Records 56import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail)) 57import Agda.TypeChecking.DisplayForm 58import Agda.TypeChecking.Level 59import {-# SOURCE #-} Agda.TypeChecking.Datatypes 60import Agda.TypeChecking.Free 61import Agda.TypeChecking.Substitute 62import Agda.TypeChecking.Telescope 63 64import Agda.Interaction.Options 65 66import Agda.Utils.Either 67import Agda.Utils.Functor 68import Agda.Utils.Lens 69import Agda.Utils.List 70import Agda.Utils.List1 (List1, pattern (:|)) 71import qualified Agda.Utils.List1 as List1 72import qualified Agda.Utils.Maybe.Strict as Strict 73import Agda.Utils.Maybe 74import Agda.Utils.Monad 75import Agda.Utils.Null 76import Agda.Utils.Permutation 77import Agda.Utils.Pretty 78import Agda.Utils.Singleton 79import Agda.Utils.Size 80import Agda.Utils.Tuple 81 82import Agda.Utils.Impossible 83 84 85-- | Like @reify@ but instantiates blocking metas, useful for reporting. 86reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i) 87reifyUnblocked t = locallyTCState stInstantiateBlocking (const True) $ reify t 88 89 90-- Composition of reified applications ------------------------------------ 91--UNUSED Liang-Ting 2019-07-16 92---- | Drops hidden arguments unless --show-implicit. 93--napps :: Expr -> [NamedArg Expr] -> TCM Expr 94--napps e = nelims e . map I.Apply 95 96-- | Drops hidden arguments unless --show-implicit. 97apps :: MonadReify m => Expr -> [Arg Expr] -> m Expr 98apps e = elims e . map I.Apply 99 100-- Composition of reified eliminations ------------------------------------ 101 102-- | Drops hidden arguments unless --show-implicit. 103nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr 104nelims e [] = return e 105nelims e (I.IApply x y r : es) = 106 nelims (A.App defaultAppInfo_ e $ defaultArg r) es 107nelims e (I.Apply arg : es) = do 108 arg <- reify arg -- This replaces the arg by _ if irrelevant 109 dontShowImp <- not <$> showImplicitArguments 110 let hd | notVisible arg && dontShowImp = e 111 | otherwise = A.App defaultAppInfo_ e arg 112 nelims hd es 113nelims e (I.Proj ProjPrefix d : es) = nelimsProjPrefix e d es 114nelims e (I.Proj o d : es) | isSelf e = nelims (A.Proj ProjPrefix $ unambiguous d) es 115 | otherwise = 116 nelims (A.App defaultAppInfo_ e (defaultNamedArg $ A.Proj o $ unambiguous d)) es 117 118nelimsProjPrefix :: MonadReify m => Expr -> QName -> [I.Elim' (Named_ Expr)] -> m Expr 119nelimsProjPrefix e d es = 120 nelims (A.App defaultAppInfo_ (A.Proj ProjPrefix $ unambiguous d) $ defaultNamedArg e) es 121 122-- | If we are referencing the record from inside the record definition, we don't insert an 123-- | A.App 124isSelf :: Expr -> Bool 125isSelf = \case 126 A.Var n -> nameIsRecordName n 127 _ -> False 128 129-- | Drops hidden arguments unless --show-implicit. 130elims :: MonadReify m => Expr -> [I.Elim' Expr] -> m Expr 131elims e = nelims e . map (fmap unnamed) 132 133-- Omitting information --------------------------------------------------- 134 135noExprInfo :: ExprInfo 136noExprInfo = ExprRange noRange 137 138-- Conditional reification to omit terms that are not shown -------------- 139 140reifyWhenE :: (Reify i, MonadReify m, Underscore (ReifiesTo i)) => Bool -> i -> m (ReifiesTo i) 141reifyWhenE True i = reify i 142reifyWhenE False t = return underscore 143 144-- Reification ------------------------------------------------------------ 145 146type MonadReify m = 147 ( PureTCM m 148 , MonadInteractionPoints m 149 , MonadFresh NameId m 150 ) 151 152class Reify i where 153 type ReifiesTo i 154 155 reify :: MonadReify m => i -> m (ReifiesTo i) 156 157 -- @reifyWhen False@ should produce an 'underscore'. 158 -- This function serves to reify hidden/irrelevant things. 159 reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i) 160 reifyWhen _ = reify 161 162instance Reify Bool where 163 type ReifiesTo Bool = Bool 164 reify = return 165 166instance Reify Name where 167 type ReifiesTo Name = Name 168 reify = return 169 170instance Reify Expr where 171 type ReifiesTo Expr = Expr 172 173 reifyWhen = reifyWhenE 174 reify = return 175 176instance Reify MetaId where 177 type ReifiesTo MetaId = Expr 178 179 reifyWhen = reifyWhenE 180 reify x@(MetaId n) = do 181 b <- asksTC envPrintMetasBare 182 mi <- mvInfo <$> lookupMeta x 183 let mi' = Info.MetaInfo 184 { metaRange = getRange $ miClosRange mi 185 , metaScope = clScope $ miClosRange mi 186 , metaNumber = if b then Nothing else Just x 187 , metaNameSuggestion = if b then "" else miNameSuggestion mi 188 } 189 underscore = return $ A.Underscore mi' 190 -- If we are printing a term that will be pasted into the user 191 -- source, we turn all unsolved (non-interaction) metas into 192 -- interaction points 193 isInteractionMeta x >>= \case 194 Nothing | b -> do 195 ii <- registerInteractionPoint False noRange Nothing 196 connectInteractionPoint ii x 197 return $ A.QuestionMark mi' ii 198 Just ii | b -> underscore 199 Nothing -> underscore 200 Just ii -> return $ A.QuestionMark mi' ii 201 202-- Does not print with-applications correctly: 203-- instance Reify DisplayTerm Expr where 204-- reifyWhen = reifyWhenE 205-- reify d = reifyTerm False $ dtermToTerm d 206 207instance Reify DisplayTerm where 208 type ReifiesTo DisplayTerm = Expr 209 210 reifyWhen = reifyWhenE 211 reify = \case 212 DTerm v -> reifyTerm False v 213 DDot v -> reify v 214 DCon c ci vs -> recOrCon (conName c) ci =<< reify vs 215 DDef f es -> elims (A.Def f) =<< reify es 216 DWithApp u us es0 -> do 217 (e, es) <- reify (u, us) 218 elims (if null es then e else A.WithApp noExprInfo e es) =<< reify es0 219 220-- | @reifyDisplayForm f vs fallback@ 221-- tries to rewrite @f vs@ with a display form for @f@. 222-- If successful, reifies the resulting display term, 223-- otherwise, does @fallback@. 224reifyDisplayForm :: MonadReify m => QName -> I.Elims -> m A.Expr -> m A.Expr 225reifyDisplayForm f es fallback = 226 ifNotM displayFormsEnabled fallback $ {- else -} 227 caseMaybeM (displayForm f es) fallback reify 228 229-- | @reifyDisplayFormP@ tries to recursively 230-- rewrite a lhs with a display form. 231-- 232-- Note: we are not necessarily in the empty context upon entry! 233reifyDisplayFormP 234 :: MonadReify m 235 => QName -- ^ LHS head symbol 236 -> A.Patterns -- ^ Patterns to be taken into account to find display form. 237 -> A.Patterns -- ^ Remaining trailing patterns ("with patterns"). 238 -> m (QName, A.Patterns) -- ^ New head symbol and new patterns. 239reifyDisplayFormP f ps wps = do 240 let fallback = return (f, ps ++ wps) 241 ifNotM displayFormsEnabled fallback $ {- else -} do 242 -- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt. 243 -- Andreas, 2014-06-11 Issue 1177: 244 -- I thought we need to add the placeholders for ps to the context, 245 -- because otherwise displayForm will not raise the display term 246 -- and we will have variable clashes. 247 -- But apparently, it has no influence... 248 -- Ulf, can you add an explanation? 249 md <- -- addContext (replicate (length ps) "x") $ 250 displayForm f $ zipWith (\ p i -> I.Apply $ p $> I.var i) ps [0..] 251 reportSLn "reify.display" 60 $ 252 "display form of " ++ prettyShow f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md 253 case md of 254 Just d | okDisplayForm d -> do 255 -- In the display term @d@, @var i@ should be a placeholder 256 -- for the @i@th pattern of @ps@. 257 -- Andreas, 2014-06-11: 258 -- Are we sure that @d@ did not use @var i@ otherwise? 259 (f', ps', wps') <- displayLHS ps d 260 reportSDoc "reify.display" 70 $ do 261 doc <- prettyA $ SpineLHS empty f' (ps' ++ wps' ++ wps) 262 return $ vcat 263 [ "rewritten lhs to" 264 , " lhs' = " <+> doc 265 ] 266 reifyDisplayFormP f' ps' (wps' ++ wps) 267 _ -> do 268 reportSLn "reify.display" 70 $ "display form absent or not valid as lhs" 269 fallback 270 where 271 -- Andreas, 2015-05-03: Ulf, please comment on what 272 -- is the idea behind okDisplayForm. 273 -- Ulf, 2016-04-15: okDisplayForm should return True if the display form 274 -- can serve as a valid left-hand side. That means checking that it is a 275 -- defined name applied to valid lhs eliminators (projections or 276 -- applications to constructor patterns). 277 okDisplayForm :: DisplayTerm -> Bool 278 okDisplayForm (DWithApp d ds es) = 279 okDisplayForm d && all okDisplayTerm ds && all okToDropE es 280 -- Andreas, 2016-05-03, issue #1950. 281 -- We might drop trailing hidden trivial (=variable) patterns. 282 okDisplayForm (DTerm (I.Def f vs)) = all okElim vs 283 okDisplayForm (DDef f es) = all okDElim es 284 okDisplayForm DDot{} = False 285 okDisplayForm DCon{} = False 286 okDisplayForm DTerm{} = False 287 288 okDisplayTerm :: DisplayTerm -> Bool 289 okDisplayTerm (DTerm v) = okTerm v 290 okDisplayTerm DDot{} = True 291 okDisplayTerm DCon{} = True 292 okDisplayTerm DDef{} = False 293 okDisplayTerm _ = False 294 295 okDElim :: Elim' DisplayTerm -> Bool 296 okDElim (I.IApply x y r) = okDisplayTerm r 297 okDElim (I.Apply v) = okDisplayTerm $ unArg v 298 okDElim I.Proj{} = True 299 300 okToDropE :: Elim' Term -> Bool 301 okToDropE (I.Apply v) = okToDrop v 302 okToDropE I.Proj{} = False 303 okToDropE (I.IApply x y r) = False 304 305 okToDrop :: Arg I.Term -> Bool 306 okToDrop arg = notVisible arg && case unArg arg of 307 I.Var _ [] -> True 308 I.DontCare{} -> True -- no matching on irrelevant things. __IMPOSSIBLE__ anyway? 309 I.Level{} -> True -- no matching on levels. __IMPOSSIBLE__ anyway? 310 _ -> False 311 312 okArg :: Arg I.Term -> Bool 313 okArg = okTerm . unArg 314 315 okElim :: Elim' I.Term -> Bool 316 okElim (I.IApply x y r) = okTerm r 317 okElim (I.Apply a) = okArg a 318 okElim I.Proj{} = True 319 320 okTerm :: I.Term -> Bool 321 okTerm (I.Var _ []) = True 322 okTerm (I.Con c ci vs) = all okElim vs 323 okTerm (I.Def x []) = isNoName $ qnameToConcrete x -- Handling wildcards in display forms 324 okTerm _ = False 325 326 -- Flatten a dt into (parentName, parentElims, withArgs). 327 flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm]) 328 flattenWith (DWithApp d ds1 es2) = 329 let (f, es, ds0) = flattenWith d 330 in (f, es, ds0 ++ map (I.Apply . defaultArg) ds1 ++ map (fmap DTerm) es2) 331 flattenWith (DDef f es) = (f, es, []) -- .^ hacky, but we should only hit this when printing debug info 332 flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, []) 333 flattenWith _ = __IMPOSSIBLE__ 334 335 displayLHS 336 :: MonadReify m 337 => A.Patterns -- Patterns to substituted into display term. 338 -> DisplayTerm -- Display term. 339 -> m (QName, A.Patterns, A.Patterns) -- New head, patterns, with-patterns. 340 displayLHS ps d = do 341 let (f, vs, es) = flattenWith d 342 ps <- mapM elimToPat vs 343 wps <- mapM (updateNamedArg (A.WithP empty) <.> elimToPat) es 344 return (f, ps, wps) 345 where 346 argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern) 347 argToPat arg = traverse termToPat arg 348 349 elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern) 350 elimToPat (I.IApply _ _ r) = argToPat (Arg defaultArgInfo r) 351 elimToPat (I.Apply arg) = argToPat arg 352 elimToPat (I.Proj o d) = return $ defaultNamedArg $ A.ProjP patNoRange o $ unambiguous d 353 354 -- Substitute variables in display term by patterns. 355 termToPat :: MonadReify m => DisplayTerm -> m (Named_ A.Pattern) 356 357 -- Main action HERE: 358 termToPat (DTerm (I.Var n [])) = return $ unArg $ fromMaybe __IMPOSSIBLE__ $ ps !!! n 359 360 termToPat (DCon c ci vs) = fmap unnamed <$> tryRecPFromConP =<< do 361 A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM argToPat vs 362 363 termToPat (DTerm (I.Con c ci vs)) = fmap unnamed <$> tryRecPFromConP =<< do 364 A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM (elimToPat . fmap DTerm) vs 365 366 termToPat (DTerm (I.Def _ [])) = return $ unnamed $ A.WildP patNoRange 367 termToPat (DDef _ []) = return $ unnamed $ A.WildP patNoRange 368 369 termToPat (DTerm (I.Lit l)) = return $ unnamed $ A.LitP patNoRange l 370 371 termToPat (DDot v) = unnamed . A.DotP patNoRange <$> termToExpr v 372 termToPat v = unnamed . A.DotP patNoRange <$> reify v 373 374 len = length ps 375 376 argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr] 377 argsToExpr = mapM (traverse termToExpr) 378 379 -- TODO: restructure this to avoid having to repeat the code for reify 380 termToExpr :: MonadReify m => Term -> m A.Expr 381 termToExpr v = do 382 reportSLn "reify.display" 60 $ "termToExpr " ++ show v 383 -- After unSpine, a Proj elimination is __IMPOSSIBLE__! 384 case unSpine v of 385 I.Con c ci es -> do 386 let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es 387 apps (A.Con (unambiguous (conName c))) =<< argsToExpr vs 388 I.Def f es -> do 389 let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es 390 apps (A.Def f) =<< argsToExpr vs 391 I.Var n es -> do 392 let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es 393 -- Andreas, 2014-06-11 Issue 1177 394 -- due to β-normalization in substitution, 395 -- even the pattern variables @n < len@ can be 396 -- applied to some args @vs@. 397 e <- if n < len 398 then return $ A.patternToExpr $ namedArg $ indexWithDefault __IMPOSSIBLE__ ps n 399 else reify (I.var (n - len)) 400 apps e =<< argsToExpr vs 401 _ -> return underscore 402 403instance Reify Literal where 404 type ReifiesTo Literal = Expr 405 406 reifyWhen = reifyWhenE 407 reify l = return $ A.Lit empty l 408 409instance Reify Term where 410 type ReifiesTo Term = Expr 411 412 reifyWhen = reifyWhenE 413 reify v = reifyTerm True v 414 415reifyPathPConstAsPath :: MonadReify m => QName -> Elims -> m (QName, Elims) 416reifyPathPConstAsPath x es@[I.Apply l, I.Apply t, I.Apply lhs, I.Apply rhs] = do 417 reportSLn "reify.def" 100 $ "reifying def path " ++ show (x,es) 418 mpath <- getBuiltinName' builtinPath 419 mpathp <- getBuiltinName' builtinPathP 420 let fallback = return (x,es) 421 case (,) <$> mpath <*> mpathp of 422 Just (path,pathp) | x == pathp -> do 423 let a = case unArg t of 424 I.Lam _ (NoAbs _ b) -> Just b 425 I.Lam _ (Abs _ b) 426 | not $ 0 `freeIn` b -> Just (strengthen impossible b) 427 _ -> Nothing 428 case a of 429 Just a -> return (path, [I.Apply l, I.Apply (setHiding Hidden $ defaultArg a), I.Apply lhs, I.Apply rhs]) 430 Nothing -> fallback 431 _ -> fallback 432reifyPathPConstAsPath x es = return (x,es) 433 434reifyTerm :: MonadReify m => Bool -> Term -> m Expr 435reifyTerm expandAnonDefs0 v0 = do 436 -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations. 437 metasBare <- asksTC envPrintMetasBare 438 v <- instantiate v0 >>= \case 439 I.MetaV x _ | metasBare -> return $ I.MetaV x [] 440 v -> return v 441 -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled 442 -- (i.e. when we don't care about nice printing) 443 expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled 444 -- Andreas, 2016-07-21 if --postfix-projections 445 -- then we print system-generated projections as postfix, else prefix. 446 havePfp <- optPostfixProjections <$> pragmaOptions 447 let pred = if havePfp then (== ProjPrefix) else (/= ProjPostfix) 448 case unSpine' pred v of 449 -- Hack to print generalized field projections with nicer names. Should 450 -- only show up in errors. Check the spined form! 451 _ | I.Var n (I.Proj _ p : es) <- v, 452 Just name <- getGeneralizedFieldName p -> do 453 let fakeName = (qnameName p) {nameConcrete = C.simpleName name} -- TODO: infix names!? 454 elims (A.Var fakeName) =<< reify es 455 I.Var n es -> do 456 x <- fromMaybeM (freshName_ $ "@" ++ show n) $ nameOfBV' n 457 elims (A.Var x) =<< reify es 458 I.Def x es -> do 459 reportSDoc "reify.def" 80 $ return $ "reifying def" <+> pretty x 460 (x, es) <- reifyPathPConstAsPath x es 461 reifyDisplayForm x es $ reifyDef expandAnonDefs x es 462 I.Con c ci vs -> do 463 let x = conName c 464 isR <- isGeneratedRecordConstructor x 465 if isR || ci == ConORec 466 then do 467 showImp <- showImplicitArguments 468 let keep (a, v) = showImp || visible a 469 r <- getConstructorData x 470 xs <- fromMaybe __IMPOSSIBLE__ <$> getRecordFieldNames_ r 471 vs <- map unArg <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs) 472 return $ A.Rec noExprInfo $ map (Left . uncurry FieldAssignment . mapFst unDom) $ filter keep $ zip xs vs 473 else reifyDisplayForm x vs $ do 474 def <- getConstInfo x 475 let Constructor {conPars = np} = theDef def 476 -- if we are the the module that defines constructor x 477 -- then we have to drop at least the n module parameters 478 n <- getDefFreeVars x 479 -- the number of parameters is greater (if the data decl has 480 -- extra parameters) or equal (if not) to n 481 when (n > np) __IMPOSSIBLE__ 482 let h = A.Con (unambiguous x) 483 if null vs 484 then return h 485 else do 486 es <- reify (map (fromMaybe __IMPOSSIBLE__ . isApplyElim) vs) 487 -- Andreas, 2012-04-20: do not reify parameter arguments of constructor 488 -- if the first regular constructor argument is hidden 489 -- we turn it into a named argument, in order to avoid confusion 490 -- with the parameter arguments which can be supplied in abstract syntax 491 -- 492 -- Andreas, 2012-09-17: this does not remove all sources of confusion, 493 -- since parameters could have the same name as regular arguments 494 -- (see for example the parameter {i} to Data.Star.Star, which is also 495 -- the first argument to the cons). 496 -- @data Star {i}{I : Set i} ... where cons : {i : I} ...@ 497 if np == 0 498 then apps h es 499 else do 500 -- Get name of first argument from type of constructor. 501 -- Here, we need the reducing version of @telView@ 502 -- because target of constructor could be a definition 503 -- expanding into a function type. See test/succeed/NameFirstIfHidden.agda. 504 TelV tel _ <- telView (defType def) 505 let (pars, rest) = splitAt np $ telToList tel 506 case rest of 507 -- Andreas, 2012-09-18 508 -- If the first regular constructor argument is hidden, 509 -- we keep the parameters to avoid confusion. 510 (Dom {domInfo = info} : _) | notVisible info -> do 511 let us = for (drop n pars) $ \(Dom {domInfo = ai}) -> 512 -- setRelevance Relevant $ 513 hideOrKeepInstance $ Arg ai underscore 514 apps h $ us ++ es -- Note: unless --show-implicit, @apps@ will drop @us@. 515 -- otherwise, we drop all parameters 516 _ -> apps h es 517 518-- I.Lam info b | isAbsurdBody b -> return $ A. AbsurdLam noExprInfo $ getHiding info 519 I.Lam info b -> do 520 (x,e) <- reify b 521 -- #4160: Hacky solution: if --show-implicit, treat all lambdas as user-written. This will 522 -- prevent them from being dropped by AbstractToConcrete (where we don't have easy access to 523 -- the --show-implicit flag. 524 info <- ifM showImplicitArguments (return $ setOrigin UserWritten info) (return info) 525 return $ A.Lam exprNoRange (mkDomainFree $ unnamedArg info $ mkBinder_ x) e 526 -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda 527 I.Lit l -> reify l 528 I.Level l -> reify l 529 I.Pi a b -> case b of 530 NoAbs _ b' 531 | visible a -> uncurry (A.Fun $ noExprInfo) <$> reify (a, b') 532 -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi 533 -- since (a) the syntax {A} -> B or {{A}} -> B is not legal 534 -- and (b) the name of the binder might matter. 535 -- See issue 951 (a) and 952 (b). 536 | otherwise -> mkPi b =<< reify a 537 b -> mkPi b =<< do 538 ifM (domainFree a (absBody b)) 539 {- then -} (pure $ Arg (domInfo a) underscore) 540 {- else -} (reify a) 541 where 542 mkPi b (Arg info a') = do 543 tac <- traverse reify $ domTactic a 544 (x, b) <- reify b 545 let xs = singleton $ Arg info $ Named (domName a) $ mkBinder_ x 546 return $ A.Pi noExprInfo (singleton $ TBind noRange tac xs a') b 547 -- We can omit the domain type if it doesn't have any free variables 548 -- and it's mentioned in the target type. 549 domainFree a b = do 550 df <- asksTC envPrintDomainFreePi 551 return $ df && freeIn 0 b && closed a 552 553 I.Sort s -> reify s 554 I.MetaV x es -> do 555 x' <- reify x 556 557 es' <- reify es 558 559 mv <- lookupMeta x 560 (msub1,meta_tel,msub2) <- do 561 local_chkpt <- viewTC eCurrentCheckpoint 562 (chkpt, tel, msub2) <- enterClosure mv $ \ _ -> 563 (,,) <$> viewTC eCurrentCheckpoint 564 <*> getContextTelescope 565 <*> viewTC (eCheckpoints . key local_chkpt) 566 (,,) <$> viewTC (eCheckpoints . key chkpt) <*> pure tel <*> pure msub2 567 568 opt_show_ids <- showIdentitySubstitutions 569 let 570 addNames [] es = map (fmap unnamed) es 571 addNames _ [] = [] 572 addNames xs (I.Proj{} : _) = __IMPOSSIBLE__ 573 addNames xs (I.IApply x y r : es) = 574 -- Needs to be I.Apply so it can have an Origin field. 575 addNames xs (I.Apply (defaultArg r) : es) 576 addNames (x:xs) (I.Apply arg : es) = 577 I.Apply (Named (Just x) <$> (setOrigin Substitution arg)) : addNames xs es 578 579 p = mvPermutation mv 580 applyPerm p vs = permute (takeP (size vs) p) vs 581 582 names = map (WithOrigin Inserted . unranged) $ p `applyPerm` teleNames meta_tel 583 named_es' = addNames names es' 584 585 dropIdentitySubs sub_local2G sub_tel2G = 586 let 587 args_G = applySubst sub_tel2G $ p `applyPerm` (teleArgs meta_tel :: [Arg Term]) 588 es_G = sub_local2G `applySubst` es 589 sameVar x (I.Apply y) = isJust xv && xv == deBruijnView (unArg y) 590 where 591 xv = deBruijnView $ unArg x 592 sameVar _ _ = False 593 dropArg = take (size names) $ zipWith sameVar args_G es_G 594 doDrop (b : xs) (e : es) = (if b then id else (e :)) $ doDrop xs es 595 doDrop [] es = es 596 doDrop _ [] = [] 597 in doDrop dropArg $ named_es' 598 599 simpl_named_es' | opt_show_ids = named_es' 600 | Just sub_mtel2local <- msub1 = dropIdentitySubs IdS sub_mtel2local 601 | Just sub_local2mtel <- msub2 = dropIdentitySubs sub_local2mtel IdS 602 | otherwise = named_es' 603 604 nelims x' simpl_named_es' 605 606 I.DontCare v -> do 607 showIrr <- optShowIrrelevant <$> pragmaOptions 608 if | showIrr -> reifyTerm expandAnonDefs v 609 | otherwise -> return underscore 610 I.Dummy s [] -> return $ A.Lit empty $ LitString (T.pack s) 611 I.Dummy "applyE" es | I.Apply (Arg _ h) : es' <- es -> do 612 h <- reify h 613 es' <- reify es' 614 elims h es' 615 | otherwise -> __IMPOSSIBLE__ 616 I.Dummy s es -> do 617 s <- reify (I.Dummy s []) 618 es <- reify es 619 elims s es 620 where 621 -- Andreas, 2012-10-20 expand a copy if not in scope 622 -- to improve error messages. 623 -- Don't do this if we have just expanded into a display form, 624 -- otherwise we loop! 625 reifyDef :: MonadReify m => Bool -> QName -> I.Elims -> m Expr 626 reifyDef True x es = 627 ifM (not . null . inverseScopeLookupName x <$> getScope) (reifyDef' x es) $ do 628 r <- reduceDefCopy x es 629 case r of 630 YesReduction _ v -> do 631 reportS "reify.anon" 60 632 [ "reduction on defined ident. in anonymous module" 633 , "x = " ++ prettyShow x 634 , "v = " ++ show v 635 ] 636 reify v 637 NoReduction () -> do 638 reportS "reify.anon" 60 639 [ "no reduction on defined ident. in anonymous module" 640 , "x = " ++ prettyShow x 641 , "es = " ++ show es 642 ] 643 reifyDef' x es 644 reifyDef _ x es = reifyDef' x es 645 646 reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr 647 reifyDef' x es = do 648 reportSLn "reify.def" 60 $ "reifying call to " ++ prettyShow x 649 -- We should drop this many arguments from the local context. 650 n <- getDefFreeVars x 651 reportSLn "reify.def" 70 $ "freeVars for " ++ prettyShow x ++ " = " ++ show n 652 -- If the definition is not (yet) in the signature, 653 -- we just do the obvious. 654 let fallback _ = elims (A.Def x) =<< reify (drop n es) 655 caseEitherM (getConstInfo' x) fallback $ \ defn -> do 656 let def = theDef defn 657 658 -- Check if we have an absurd lambda. 659 case def of 660 Function{ funCompiled = Just Fail{}, funClauses = [cl] } 661 | isAbsurdLambdaName x -> do 662 -- get hiding info from last pattern, which should be () 663 let (ps, p) = fromMaybe __IMPOSSIBLE__ $ initLast $ namedClausePats cl 664 let h = getHiding p 665 n = length ps -- drop all args before the absurd one 666 absLam = A.AbsurdLam exprNoRange h 667 if | n > length es -> do -- We don't have all arguments before the absurd one! 668 let name (I.VarP _ x) = patVarNameToString $ dbPatVarName x 669 name _ = __IMPOSSIBLE__ -- only variables before absurd pattern 670 vars = map (getArgInfo &&& name . namedArg) $ drop (length es) ps 671 lam (i, s) = do 672 x <- freshName_ s 673 return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg i $ A.mkBinder_ x) 674 foldr ($) absLam <$> mapM lam vars 675 | otherwise -> elims absLam =<< reify (drop n es) 676 677 -- Otherwise (no absurd lambda): 678 _ -> do 679 680 -- Andrea(s), 2016-07-06 681 -- Extended lambdas are not considered to be projection like, 682 -- as they are mutually recursive with their parent. 683 -- Thus we do not have to consider padding them. 684 685 -- Check whether we have an extended lambda and display forms are on. 686 df <- displayFormsEnabled 687 688 -- #3004: give up if we have to print a pattern lambda inside its own body! 689 alreadyPrinting <- viewTC ePrintingPatternLambdas 690 691 extLam <- case def of 692 Function{ funExtLam = Just{}, funProjection = Just{} } -> __IMPOSSIBLE__ 693 Function{ funExtLam = Just (ExtLamInfo m b sys) } -> 694 Just . (,Strict.toLazy sys) . size <$> lookupSection m 695 _ -> return Nothing 696 case extLam of 697 Just (pars, sys) | df, x `notElem` alreadyPrinting -> 698 locallyTC ePrintingPatternLambdas (x :) $ 699 reifyExtLam x (defArgInfo defn) pars sys 700 (defClauses defn) es 701 702 -- Otherwise (ordinary function call): 703 _ -> do 704 (pad, nes :: [Elim' (Named_ Term)]) <- case def of 705 706 Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do 707 reportSLn "reify.def" 70 $ " def. is a projection with projIndex = " ++ show np 708 709 -- This is tricky: 710 -- * getDefFreeVars x tells us how many arguments 711 -- are part of the local context 712 -- * some of those arguments might have been dropped 713 -- due to projection likeness 714 -- * when showImplicits is on we'd like to see the dropped 715 -- projection arguments 716 717 TelV tel _ <- telViewUpTo np (defType defn) 718 let (as, rest) = splitAt (np - 1) $ telToList tel 719 dom = headWithDefault __IMPOSSIBLE__ rest 720 721 -- These are the dropped projection arguments 722 scope <- getScope 723 let underscore = A.Underscore $ Info.emptyMetaInfo { metaScope = scope } 724 let pad :: [NamedArg Expr] 725 pad = for as $ \ (Dom{domInfo = ai, unDom = (x, _)}) -> 726 Arg ai $ Named (Just $ WithOrigin Inserted $ unranged x) underscore 727 -- TODO #3353 Origin from Dom? 728 729 -- Now pad' ++ es' = drop n (pad ++ es) 730 let pad' = drop n pad 731 es' = drop (max 0 (n - size pad)) es 732 -- Andreas, 2012-04-21: get rid of hidden underscores {_} and {{_}} 733 -- Keep non-hidden arguments of the padding. 734 -- 735 -- Andreas, 2016-12-20, issue #2348: 736 -- Let @padTail@ be the list of arguments of the padding 737 -- (*) after the last visible argument of the padding, and 738 -- (*) with the same visibility as the first regular argument. 739 -- If @padTail@ is not empty, we need to 740 -- print the first regular argument with name. 741 -- We further have to print all elements of @padTail@ 742 -- which have the same name and visibility of the 743 -- first regular argument. 744 showImp <- showImplicitArguments 745 746 -- Get the visible arguments of the padding and the rest 747 -- after the last visible argument. 748 let (padVisNamed, padRest) = filterAndRest visible pad' 749 750 -- Remove the names from the visible arguments. 751 let padVis = map (fmap $ unnamed . namedThing) padVisNamed 752 753 -- Keep only the rest with the same visibility of @dom@... 754 let padTail = filter (sameHiding dom) padRest 755 756 -- ... and even the same name. 757 let padSame = filter ((Just (fst $ unDom dom) ==) . bareNameOf) padTail 758 759 return $ if null padTail || not showImp 760 then (padVis , map (fmap unnamed) es') 761 else (padVis ++ padSame, nameFirstIfHidden dom es') 762 763 -- If it is not a projection(-like) function, we need no padding. 764 _ -> return ([], map (fmap unnamed) $ drop n es) 765 766 reportSDoc "reify.def" 100 $ return $ vcat 767 [ " pad =" <+> pshow pad 768 , " nes =" <+> pshow nes 769 ] 770 let hd0 | isProperProjection def = A.Proj ProjPrefix $ AmbQ $ singleton x 771 | otherwise = A.Def x 772 let hd = List.foldl' (A.App defaultAppInfo_) hd0 pad 773 nelims hd =<< reify nes 774 775 -- Andreas, 2016-07-06 Issue #2047 776 777 -- With parameter refinement, the "parameter" patterns of an extended 778 -- lambda can now be different from variable patterns. If we just drop 779 -- them (plus the associated arguments to the extended lambda), we produce 780 -- something 781 782 -- i) that violates internal invariants. In particular, the permutation 783 -- dbPatPerm from the patterns to the telescope can no longer be 784 -- computed. (And in fact, dropping from the start of the telescope is 785 -- just plainly unsound then.) 786 787 -- ii) prints the wrong thing (old fix for #2047) 788 789 -- What we do now, is more sound, although not entirely satisfying: 790 -- When the "parameter" patterns of an external lambdas are not variable 791 -- patterns, we fall back to printing the internal function created for the 792 -- extended lambda, instead trying to construct the nice syntax. 793 794 reifyExtLam 795 :: MonadReify m 796 => QName -> ArgInfo -> Int -> Maybe System -> [I.Clause] 797 -> I.Elims -> m Expr 798 reifyExtLam x i npars msys cls es = do 799 reportSLn "reify.def" 10 $ "reifying extended lambda " ++ prettyShow x 800 reportSLn "reify.def" 50 $ render $ nest 2 $ vcat 801 [ "npars =" <+> pretty npars 802 , "es =" <+> fsep (map (prettyPrec 10) es) 803 , "def =" <+> vcat (map pretty cls) ] 804 -- As extended lambda clauses live in the top level, we add the whole 805 -- section telescope to the number of parameters. 806 let (pares, rest) = splitAt npars es 807 let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims pares 808 809 -- Since we applying the clauses to the parameters, 810 -- we do not need to drop their initial "parameter" patterns 811 -- (this is taken care of by @apply@). 812 cls <- caseMaybe msys 813 (mapM (reify . NamedClause x False . (`apply` pars)) cls) 814 (reify . QNamed x . (`apply` pars)) 815 let cx = nameConcrete $ qnameName x 816 dInfo = mkDefInfo cx noFixity' PublicAccess ConcreteDef 817 (getRange x) 818 erased = case getQuantity i of 819 Quantity0 o -> Erased o 820 Quantityω o -> NotErased o 821 Quantity1 o -> __IMPOSSIBLE__ 822 elims (A.ExtendedLam exprNoRange dInfo erased x $ 823 List1.fromList cls) 824 =<< reify rest 825 826-- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@ 827nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)] 828nameFirstIfHidden dom (I.Apply (Arg info e) : es) | notVisible info = 829 I.Apply (Arg info (Named (Just $ WithOrigin Inserted $ unranged $ fst $ unDom dom) e)) : 830 map (fmap unnamed) es 831nameFirstIfHidden _ es = 832 map (fmap unnamed) es 833 834instance Reify i => Reify (Named n i) where 835 type ReifiesTo (Named n i) = Named n (ReifiesTo i) 836 837 reify = traverse reify 838 reifyWhen b = traverse (reifyWhen b) 839 840-- | Skip reification of implicit and irrelevant args if option is off. 841instance Reify i => Reify (Arg i) where 842 type ReifiesTo (Arg i) = Arg (ReifiesTo i) 843 844 reify (Arg info i) = Arg info <$> (flip reifyWhen i =<< condition) 845 where condition = (return (argInfoHiding info /= Hidden) `or2M` showImplicitArguments) 846 `and2M` (return (getRelevance info /= Irrelevant) `or2M` showIrrelevantArguments) 847 reifyWhen b i = traverse (reifyWhen b) i 848 849-- instance Reify Elim Expr where 850-- reifyWhen = reifyWhenE 851-- reify = \case 852-- I.IApply x y r -> appl "iapply" <$> reify (defaultArg r :: Arg Term) 853-- I.Apply v -> appl "apply" <$> reify v 854-- I.Proj f -> appl "proj" <$> reify ((defaultArg $ I.Def f []) :: Arg Term) 855-- where 856-- appl :: String -> Arg Expr -> Expr 857-- appl s v = A.App exprInfo (A.Lit empty (LitString s)) $ fmap unnamed v 858 859data NamedClause = NamedClause QName Bool I.Clause 860 -- ^ Also tracks whether module parameters should be dropped from the patterns. 861 862-- The Monoid instance for Data.Map doesn't require that the values are a 863-- monoid. 864newtype MonoidMap k v = MonoidMap { _unMonoidMap :: Map.Map k v } 865 866instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where 867 MonoidMap m1 <> MonoidMap m2 = MonoidMap (Map.unionWith mappend m1 m2) 868 869instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where 870 mempty = MonoidMap Map.empty 871 mappend = (<>) 872 873-- | Removes argument names. Preserves names present in the source. 874removeNameUnlessUserWritten :: (LensNamed a, LensOrigin (NameOf a)) => a -> a 875removeNameUnlessUserWritten a 876 | (getOrigin <$> getNameOf a) == Just UserWritten = a 877 | otherwise = setNameOf Nothing a 878 879 880-- | Removes implicit arguments that are not needed, that is, that don't bind 881-- any variables that are actually used and doesn't do pattern matching. 882-- Doesn't strip any arguments that were written explicitly by the user. 883stripImplicits :: MonadReify m => A.Patterns -> A.Patterns -> m A.Patterns 884stripImplicits params ps = do 885 -- if --show-implicit we don't need the names 886 ifM showImplicitArguments (return $ map (fmap removeNameUnlessUserWritten) ps) $ do 887 reportSDoc "reify.implicit" 100 $ return $ vcat 888 [ "stripping implicits" 889 , nest 2 $ "ps =" <+> pshow ps 890 ] 891 let ps' = blankDots $ strip ps 892 reportSDoc "reify.implicit" 100 $ return $ vcat 893 [ nest 2 $ "ps' =" <+> pshow ps' 894 ] 895 return ps' 896 where 897 -- Replace variables in dot patterns by an underscore _ if they are hidden 898 -- in the pattern. This is slightly nicer than making the implicts explicit. 899 blankDots ps = blank (varsBoundIn $ params ++ ps) ps 900 901 strip ps = stripArgs True ps 902 where 903 stripArgs _ [] = [] 904 stripArgs fixedPos (a : as) 905 -- A hidden non-UserWritten variable is removed if not needed for 906 -- correct position of the following hidden arguments. 907 | canStrip a = 908 if all canStrip $ takeWhile isUnnamedHidden as 909 then stripArgs False as 910 else goWild 911 -- Other arguments are kept. 912 | otherwise = stripName fixedPos (stripArg a) : stripArgs True as 913 where 914 a' = setNamedArg a $ A.WildP $ Info.PatRange $ getRange a 915 goWild = stripName fixedPos a' : stripArgs True as 916 917 stripName True = fmap removeNameUnlessUserWritten 918 stripName False = id 919 920 -- TODO: vars appearing in EqualPs shouldn't be stripped. 921 canStrip a = and 922 [ notVisible a 923 , getOrigin a `notElem` [ UserWritten , CaseSplit ] 924 , (getOrigin <$> getNameOf a) /= Just UserWritten 925 , varOrDot (namedArg a) 926 ] 927 928 isUnnamedHidden x = notVisible x && isNothing (getNameOf x) && isNothing (isProjP x) 929 930 stripArg a = fmap (fmap stripPat) a 931 932 stripPat = \case 933 p@(A.VarP _) -> p 934 A.ConP i c ps -> A.ConP i c $ stripArgs True ps 935 p@A.ProjP{} -> p 936 p@(A.DefP _ _ _) -> p 937 p@(A.DotP _ _e) -> p 938 p@(A.WildP _) -> p 939 p@(A.AbsurdP _) -> p 940 p@(A.LitP _ _) -> p 941 A.AsP i x p -> A.AsP i x $ stripPat p 942 A.PatternSynP _ _ _ -> __IMPOSSIBLE__ 943 A.RecP i fs -> A.RecP i $ map (fmap stripPat) fs -- TODO Andreas: is this right? 944 p@A.EqualP{} -> p -- EqualP cannot be blanked. 945 A.WithP i p -> A.WithP i $ stripPat p -- TODO #2822: right? 946 A.AnnP i a p -> A.AnnP i a $ stripPat p 947 948 varOrDot A.VarP{} = True 949 varOrDot A.WildP{} = True 950 varOrDot A.DotP{} = True 951 varOrDot (A.ConP cpi _ ps) | conPatOrigin cpi == ConOSystem 952 = conPatLazy cpi == ConPatLazy || all (varOrDot . namedArg) ps 953 varOrDot _ = False 954 955-- | @blankNotInScope e@ replaces variables in expression @e@ with @_@ 956-- if they are currently not in scope. 957blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a 958blankNotInScope e = do 959 names <- Set.fromList . filter ((== C.InScope) . C.isInScope) <$> getContextNames 960 return $ blank names e 961 962 963-- | @blank bound e@ replaces all variables in expression @e@ that are not in @bound@ by 964-- an underscore @_@. It is used for printing dot patterns: we don't want to 965-- make implicit variables explicit, so we blank them out in the dot patterns 966-- instead (this is fine since dot patterns can be inferred anyway). 967 968class BlankVars a where 969 blank :: Set Name -> a -> a 970 971 default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a 972 blank = fmap . blank 973 974instance BlankVars a => BlankVars (Arg a) 975instance BlankVars a => BlankVars (Named s a) 976instance BlankVars a => BlankVars [a] 977instance BlankVars a => BlankVars (List1 a) 978instance BlankVars a => BlankVars (FieldAssignment' a) 979-- instance BlankVars a => BlankVars (A.Pattern' a) -- see case EqualP ! 980 981instance (BlankVars a, BlankVars b) => BlankVars (a, b) where 982 blank bound (x, y) = (blank bound x, blank bound y) 983 984instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where 985 blank bound (Left x) = Left $ blank bound x 986 blank bound (Right y) = Right $ blank bound y 987 988instance BlankVars A.ProblemEq where 989 blank bound = id 990 991instance BlankVars A.Clause where 992 blank bound (A.Clause lhs strippedPats rhs wh ca) 993 | null wh = 994 A.Clause (blank bound' lhs) 995 (blank bound' strippedPats) 996 (blank bound' rhs) noWhereDecls ca 997 | otherwise = __IMPOSSIBLE__ 998 where bound' = varsBoundIn lhs `Set.union` bound 999 1000instance BlankVars A.LHS where 1001 blank bound (A.LHS i core) = A.LHS i $ blank bound core 1002 1003instance BlankVars A.LHSCore where 1004 blank bound (A.LHSHead f ps) = A.LHSHead f $ blank bound ps 1005 blank bound (A.LHSProj p b ps) = uncurry (A.LHSProj p) $ blank bound (b, ps) 1006 blank bound (A.LHSWith h wps ps) = uncurry (uncurry A.LHSWith) $ blank bound ((h, wps), ps) 1007 1008instance BlankVars A.Pattern where 1009 blank bound p = case p of 1010 A.VarP _ -> p -- do not blank pattern vars 1011 A.ConP c i ps -> A.ConP c i $ blank bound ps 1012 A.ProjP{} -> p 1013 A.DefP i f ps -> A.DefP i f $ blank bound ps 1014 A.DotP i e -> A.DotP i $ blank bound e 1015 A.WildP _ -> p 1016 A.AbsurdP _ -> p 1017 A.LitP _ _ -> p 1018 A.AsP i n p -> A.AsP i n $ blank bound p 1019 A.PatternSynP _ _ _ -> __IMPOSSIBLE__ 1020 A.RecP i fs -> A.RecP i $ blank bound fs 1021 A.EqualP{} -> p 1022 A.WithP i p -> A.WithP i (blank bound p) 1023 A.AnnP i a p -> A.AnnP i (blank bound a) (blank bound p) 1024 1025instance BlankVars A.Expr where 1026 blank bound e = case e of 1027 A.ScopedExpr i e -> A.ScopedExpr i $ blank bound e 1028 A.Var x -> if x `Set.member` bound then e 1029 else A.Underscore emptyMetaInfo -- Here is the action! 1030 A.Def' _ _ -> e 1031 A.Proj{} -> e 1032 A.Con _ -> e 1033 A.Lit _ _ -> e 1034 A.QuestionMark{} -> e 1035 A.Underscore _ -> e 1036 A.Dot i e -> A.Dot i $ blank bound e 1037 A.App i e1 e2 -> uncurry (A.App i) $ blank bound (e1, e2) 1038 A.WithApp i e es -> uncurry (A.WithApp i) $ blank bound (e, es) 1039 A.Lam i b e -> let bound' = varsBoundIn b `Set.union` bound 1040 in A.Lam i (blank bound b) (blank bound' e) 1041 A.AbsurdLam _ _ -> e 1042 A.ExtendedLam i d e f cs -> A.ExtendedLam i d e f $ blank bound cs 1043 A.Pi i tel e -> let bound' = varsBoundIn tel `Set.union` bound 1044 in uncurry (A.Pi i) $ blank bound' (tel, e) 1045 A.Generalized {} -> __IMPOSSIBLE__ 1046 A.Fun i a b -> uncurry (A.Fun i) $ blank bound (a, b) 1047 A.Let _ _ _ -> __IMPOSSIBLE__ 1048 A.Rec i es -> A.Rec i $ blank bound es 1049 A.RecUpdate i e es -> uncurry (A.RecUpdate i) $ blank bound (e, es) 1050 A.ETel _ -> __IMPOSSIBLE__ 1051 A.Quote {} -> __IMPOSSIBLE__ 1052 A.QuoteTerm {} -> __IMPOSSIBLE__ 1053 A.Unquote {} -> __IMPOSSIBLE__ 1054 A.Tactic {} -> __IMPOSSIBLE__ 1055 A.DontCare v -> A.DontCare $ blank bound v 1056 A.PatternSyn {} -> e 1057 A.Macro {} -> e 1058 1059instance BlankVars A.ModuleName where 1060 blank bound = id 1061 1062instance BlankVars RHS where 1063 blank bound (RHS e mc) = RHS (blank bound e) mc 1064 blank bound AbsurdRHS = AbsurdRHS 1065 blank bound (WithRHS _ es clauses) = __IMPOSSIBLE__ -- NZ 1066 blank bound (RewriteRHS xes spats rhs _) = __IMPOSSIBLE__ -- NZ 1067 1068instance BlankVars A.LamBinding where 1069 blank bound b@A.DomainFree{} = b 1070 blank bound (A.DomainFull bs) = A.DomainFull $ blank bound bs 1071 1072instance BlankVars TypedBinding where 1073 blank bound (TBind r t n e) = TBind r t n $ blank bound e 1074 blank bound (TLet _ _) = __IMPOSSIBLE__ -- Since the internal syntax has no let bindings left 1075 1076 1077-- | Collect the binders in some abstract syntax lhs. 1078 1079class Binder a where 1080 varsBoundIn :: a -> Set Name 1081 1082 default varsBoundIn :: (Foldable f, Binder b, f b ~ a) => a -> Set Name 1083 varsBoundIn = foldMap varsBoundIn 1084 1085instance Binder A.LHS where 1086 varsBoundIn (A.LHS _ core) = varsBoundIn core 1087 1088instance Binder A.LHSCore where 1089 varsBoundIn (A.LHSHead _ ps) = varsBoundIn ps 1090 varsBoundIn (A.LHSProj _ b ps) = varsBoundIn (b, ps) 1091 varsBoundIn (A.LHSWith h wps ps) = varsBoundIn ((h, wps), ps) 1092 1093instance Binder A.Pattern where 1094 varsBoundIn = foldAPattern $ \case 1095 A.VarP x -> varsBoundIn x 1096 A.AsP _ x _ -> empty -- Not x because of #2414 (?) 1097 A.ConP _ _ _ -> empty 1098 A.ProjP{} -> empty 1099 A.DefP _ _ _ -> empty 1100 A.WildP{} -> empty 1101 A.DotP{} -> empty 1102 A.AbsurdP{} -> empty 1103 A.LitP{} -> empty 1104 A.PatternSynP _ _ _ -> empty 1105 A.RecP _ _ -> empty 1106 A.EqualP{} -> empty 1107 A.WithP _ _ -> empty 1108 A.AnnP{} -> empty 1109 1110instance Binder a => Binder (A.Binder' a) where 1111 varsBoundIn (A.Binder p n) = varsBoundIn (p, n) 1112 1113instance Binder A.LamBinding where 1114 varsBoundIn (A.DomainFree _ x) = varsBoundIn x 1115 varsBoundIn (A.DomainFull b) = varsBoundIn b 1116 1117instance Binder TypedBinding where 1118 varsBoundIn (TBind _ _ xs _) = varsBoundIn xs 1119 varsBoundIn (TLet _ bs) = varsBoundIn bs 1120 1121instance Binder BindName where 1122 varsBoundIn x = singleton (unBind x) 1123 1124instance Binder LetBinding where 1125 varsBoundIn (LetBind _ _ x _ _) = varsBoundIn x 1126 varsBoundIn (LetPatBind _ p _) = varsBoundIn p 1127 varsBoundIn LetApply{} = empty 1128 varsBoundIn LetOpen{} = empty 1129 varsBoundIn LetDeclaredVariable{} = empty 1130 1131instance Binder a => Binder (FieldAssignment' a) 1132instance Binder a => Binder (Arg a) 1133instance Binder a => Binder (Named x a) 1134instance Binder a => Binder [a] 1135instance Binder a => Binder (List1 a) 1136instance Binder a => Binder (Maybe a) 1137 1138instance (Binder a, Binder b) => Binder (a, b) where 1139 varsBoundIn (x, y) = varsBoundIn x `Set.union` varsBoundIn y 1140 1141 1142-- | Assumes that pattern variables have been added to the context already. 1143-- Picks pattern variable names from context. 1144reifyPatterns :: MonadReify m => [NamedArg I.DeBruijnPattern] -> m [NamedArg A.Pattern] 1145reifyPatterns = mapM $ (stripNameFromExplicit . stripHidingFromPostfixProj) <.> 1146 traverse (traverse reifyPat) 1147 where 1148 -- #4399 strip also empty names 1149 stripNameFromExplicit :: NamedArg p -> NamedArg p 1150 stripNameFromExplicit a 1151 | visible a || maybe True (liftA2 (||) null isNoName) (bareNameOf a) = 1152 fmap (unnamed . namedThing) a 1153 | otherwise = a 1154 1155 stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p 1156 stripHidingFromPostfixProj a = case isProjP a of 1157 Just (o, _) | o /= ProjPrefix -> setHiding NotHidden a 1158 _ -> a 1159 1160 reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern 1161 reifyPat p = do 1162 reportSDoc "reify.pat" 80 $ return $ "reifying pattern" <+> pretty p 1163 keepVars <- optKeepPatternVariables <$> pragmaOptions 1164 case p of 1165 -- Possibly expanded literal pattern (see #4215) 1166 p | Just (PatternInfo PatOLit asB) <- patternInfo p -> do 1167 reduce (I.patternToTerm p) >>= \case 1168 I.Lit l -> addAsBindings asB $ return $ A.LitP empty l 1169 _ -> __IMPOSSIBLE__ 1170 I.VarP i x -> addAsBindings (patAsNames i) $ case patOrigin i of 1171 o@PatODot -> reifyDotP o $ var $ dbPatVarIndex x 1172 PatOWild -> return $ A.WildP patNoRange 1173 PatOAbsurd -> return $ A.AbsurdP patNoRange 1174 _ -> reifyVarP x 1175 I.DotP i v -> addAsBindings (patAsNames i) $ case patOrigin i of 1176 PatOWild -> return $ A.WildP patNoRange 1177 PatOAbsurd -> return $ A.AbsurdP patNoRange 1178 -- If Agda turned a user variable @x@ into @.x@, print it back as @x@. 1179 o@(PatOVar x) | I.Var i [] <- v -> do 1180 x' <- nameOfBV i 1181 if nameConcrete x == nameConcrete x' then 1182 return $ A.VarP $ mkBindName x' 1183 else 1184 reifyDotP o v 1185 o -> reifyDotP o v 1186 I.LitP i l -> addAsBindings (patAsNames i) $ return $ A.LitP empty l 1187 I.ProjP o d -> return $ A.ProjP patNoRange o $ unambiguous d 1188 I.ConP c cpi ps | conPRecord cpi -> addAsBindings (patAsNames $ conPInfo cpi) $ 1189 case patOrigin (conPInfo cpi) of 1190 PatOWild -> return $ A.WildP patNoRange 1191 PatOAbsurd -> return $ A.AbsurdP patNoRange 1192 PatOVar x | keepVars -> return $ A.VarP $ mkBindName x 1193 _ -> reifyConP c cpi ps 1194 I.ConP c cpi ps -> addAsBindings (patAsNames $ conPInfo cpi) $ reifyConP c cpi ps 1195 I.DefP i f ps -> addAsBindings (patAsNames i) $ case patOrigin i of 1196 PatOWild -> return $ A.WildP patNoRange 1197 PatOAbsurd -> return $ A.AbsurdP patNoRange 1198 PatOVar x | keepVars -> return $ A.VarP $ mkBindName x 1199 _ -> A.DefP patNoRange (unambiguous f) <$> reifyPatterns ps 1200 I.IApplyP i _ _ x -> addAsBindings (patAsNames i) $ case patOrigin i of 1201 o@PatODot -> reifyDotP o $ var $ dbPatVarIndex x 1202 PatOWild -> return $ A.WildP patNoRange 1203 PatOAbsurd -> return $ A.AbsurdP patNoRange 1204 _ -> reifyVarP x 1205 1206 reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern 1207 reifyVarP x = do 1208 n <- nameOfBV $ dbPatVarIndex x 1209 let y = dbPatVarName x 1210 if | y == "_" -> return $ A.VarP $ mkBindName n 1211 -- Andreas, 2017-09-03: TODO for #2580 1212 -- Patterns @VarP "()"@ should have been replaced by @AbsurdP@, but the 1213 -- case splitter still produces them. 1214 | prettyShow (nameConcrete n) == "()" -> return $ A.VarP (mkBindName n) 1215 -- Andreas, 2017-09-03, issue #2729 1216 -- Restore original pattern name. AbstractToConcrete picks unique names. 1217 | otherwise -> return $ A.VarP $ 1218 mkBindName n { nameConcrete = C.simpleName y } 1219 1220 reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern 1221 reifyDotP o v = do 1222 keepVars <- optKeepPatternVariables <$> pragmaOptions 1223 if | PatOVar x <- o , keepVars -> return $ A.VarP $ mkBindName x 1224 | otherwise -> A.DotP patNoRange <$> reify v 1225 1226 reifyConP :: MonadReify m 1227 => ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] 1228 -> m A.Pattern 1229 reifyConP c cpi ps = do 1230 tryRecPFromConP =<< do A.ConP ci (unambiguous (conName c)) <$> reifyPatterns ps 1231 where 1232 ci = ConPatInfo origin patNoRange lazy 1233 lazy | conPLazy cpi = ConPatLazy 1234 | otherwise = ConPatEager 1235 origin = fromConPatternInfo cpi 1236 1237 addAsBindings :: Functor m => [A.Name] -> m A.Pattern -> m A.Pattern 1238 addAsBindings xs p = foldr (fmap . AsP patNoRange . mkBindName) p xs 1239 1240 1241-- | If the record constructor is generated or the user wrote a record pattern, 1242-- turn constructor pattern into record pattern. 1243-- Otherwise, keep constructor pattern. 1244tryRecPFromConP :: MonadReify m => A.Pattern -> m A.Pattern 1245tryRecPFromConP p = do 1246 let fallback = return p 1247 case p of 1248 A.ConP ci c ps -> do 1249 reportSLn "reify.pat" 60 $ "tryRecPFromConP " ++ prettyShow c 1250 caseMaybeM (isRecordConstructor $ headAmbQ c) fallback $ \ (r, def) -> do 1251 -- If the record constructor is generated or the user wrote a record pattern, 1252 -- print record pattern. 1253 -- Otherwise, print constructor pattern. 1254 if recNamedCon def && conPatOrigin ci /= ConORec then fallback else do 1255 fs <- fromMaybe __IMPOSSIBLE__ <$> getRecordFieldNames_ r 1256 unless (length fs == length ps) __IMPOSSIBLE__ 1257 return $ A.RecP patNoRange $ zipWith mkFA fs ps 1258 where 1259 mkFA ax nap = FieldAssignment (unDom ax) (namedArg nap) 1260 _ -> __IMPOSSIBLE__ 1261 1262-- | If the record constructor is generated or the user wrote a record expression, 1263-- turn constructor expression into record expression. 1264-- Otherwise, keep constructor expression. 1265recOrCon :: MonadReify m => QName -> ConOrigin -> [Arg Expr] -> m A.Expr 1266recOrCon c co es = do 1267 reportSLn "reify.expr" 60 $ "recOrCon " ++ prettyShow c 1268 caseMaybeM (isRecordConstructor c) fallback $ \ (r, def) -> do 1269 -- If the record constructor is generated or the user wrote a record expression, 1270 -- print record expression. 1271 -- Otherwise, print constructor expression. 1272 if recNamedCon def && co /= ConORec then fallback else do 1273 fs <- fromMaybe __IMPOSSIBLE__ <$> getRecordFieldNames_ r 1274 unless (length fs == length es) __IMPOSSIBLE__ 1275 return $ A.Rec empty $ zipWith mkFA fs es 1276 where 1277 fallback = apps (A.Con (unambiguous c)) es 1278 mkFA ax = Left . FieldAssignment (unDom ax) . unArg 1279 1280instance Reify (QNamed I.Clause) where 1281 type ReifiesTo (QNamed I.Clause) = A.Clause 1282 1283 reify (QNamed f cl) = reify (NamedClause f True cl) 1284 1285instance Reify NamedClause where 1286 type ReifiesTo NamedClause = A.Clause 1287 1288 reify (NamedClause f toDrop cl) = addContext (clauseTel cl) $ do 1289 reportSDoc "reify.clause" 60 $ return $ vcat 1290 [ "reifying NamedClause" 1291 , " f =" <+> pretty f 1292 , " toDrop =" <+> pshow toDrop 1293 , " cl =" <+> pretty cl 1294 ] 1295 let ell = clauseEllipsis cl 1296 ps <- reifyPatterns $ namedClausePats cl 1297 lhs <- uncurry (SpineLHS $ empty { lhsEllipsis = ell }) <$> reifyDisplayFormP f ps [] 1298 -- Unless @toDrop@ we have already dropped the module patterns from the clauses 1299 -- (e.g. for extended lambdas). We still get here with toDrop = True and 1300 -- pattern lambdas when doing make-case, so take care to drop the right 1301 -- number of parameters. 1302 (params , lhs) <- if not toDrop then return ([] , lhs) else do 1303 nfv <- getDefModule f >>= \case 1304 Left _ -> return 0 1305 Right m -> size <$> lookupSection m 1306 return $ splitParams nfv lhs 1307 lhs <- stripImps params lhs 1308 reportSDoc "reify.clause" 100 $ return $ "reifying NamedClause, lhs =" <?> pshow lhs 1309 rhs <- caseMaybe (clauseBody cl) (return AbsurdRHS) $ \ e -> 1310 RHS <$> reify e <*> pure Nothing 1311 reportSDoc "reify.clause" 100 $ return $ "reifying NamedClause, rhs =" <?> pshow rhs 1312 let result = A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls (I.clauseCatchall cl) 1313 reportSDoc "reify.clause" 100 $ return $ "reified NamedClause, result =" <?> pshow result 1314 return result 1315 where 1316 splitParams n (SpineLHS i f ps) = 1317 let (params , pats) = splitAt n ps 1318 in (params , SpineLHS i f pats) 1319 stripImps :: MonadReify m => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS 1320 stripImps params (SpineLHS i f ps) = SpineLHS i f <$> stripImplicits params ps 1321 1322instance Reify (QNamed System) where 1323 type ReifiesTo (QNamed System) = [A.Clause] 1324 1325 reify (QNamed f (System tel sys)) = addContext tel $ do 1326 reportS "reify.system" 40 $ show tel : map show sys 1327 view <- intervalView' 1328 unview <- intervalUnview' 1329 sys <- flip filterM sys $ \ (phi,t) -> do 1330 allM phi $ \ (u,b) -> do 1331 u <- reduce u 1332 return $ case (view u, b) of 1333 (IZero, True) -> False 1334 (IOne, False) -> False 1335 _ -> True 1336 forM sys $ \ (alpha,u) -> do 1337 rhs <- RHS <$> reify u <*> pure Nothing 1338 ep <- fmap (A.EqualP patNoRange) . forM alpha $ \ (phi,b) -> do 1339 let 1340 d True = unview IOne 1341 d False = unview IZero 1342 reify (phi, d b) 1343 1344 ps <- reifyPatterns $ teleNamedArgs tel 1345 ps <- stripImplicits [] $ ps ++ [defaultNamedArg ep] 1346 let 1347 lhs = SpineLHS empty f ps 1348 result = A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls False 1349 return result 1350 1351instance Reify Type where 1352 type ReifiesTo Type = Expr 1353 1354 reifyWhen = reifyWhenE 1355 reify (I.El _ t) = reify t 1356 1357instance Reify Sort where 1358 type ReifiesTo Sort = Expr 1359 1360 reifyWhen = reifyWhenE 1361 reify s = do 1362 s <- instantiateFull s 1363 SortKit{..} <- sortKit 1364 case s of 1365 I.Type (I.ClosedLevel 0) -> return $ A.Def' nameOfSet A.NoSuffix 1366 I.Type (I.ClosedLevel n) -> return $ A.Def' nameOfSet (A.Suffix n) 1367 I.Type a -> do 1368 a <- reify a 1369 return $ A.App defaultAppInfo_ (A.Def nameOfSet) (defaultNamedArg a) 1370 I.Prop (I.ClosedLevel 0) -> return $ A.Def' nameOfProp A.NoSuffix 1371 I.Prop (I.ClosedLevel n) -> return $ A.Def' nameOfProp (A.Suffix n) 1372 I.Prop a -> do 1373 a <- reify a 1374 return $ A.App defaultAppInfo_ (A.Def nameOfProp) (defaultNamedArg a) 1375 I.Inf f 0 -> return $ A.Def' (nameOfSetOmega f) A.NoSuffix 1376 I.Inf f n -> return $ A.Def' (nameOfSetOmega f) (A.Suffix n) 1377 I.SSet a -> do 1378 I.Def sset [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinStrictSet 1379 a <- reify a 1380 return $ A.App defaultAppInfo_ (A.Def sset) (defaultNamedArg a) 1381 I.SizeUniv -> do 1382 I.Def sizeU [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeUniv 1383 return $ A.Def sizeU 1384 I.LockUniv -> do 1385 lockU <- fromMaybe __IMPOSSIBLE__ <$> getName' builtinLockUniv 1386 return $ A.Def lockU 1387 I.PiSort a s1 s2 -> do 1388 pis <- freshName_ ("piSort" :: String) -- TODO: hack 1389 (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2) 1390 let app x y = A.App defaultAppInfo_ x (defaultNamedArg y) 1391 return $ A.Var pis `app` e1 `app` e2 1392 I.FunSort s1 s2 -> do 1393 funs <- freshName_ ("funSort" :: String) -- TODO: hack 1394 (e1,e2) <- reify (s1 , s2) 1395 let app x y = A.App defaultAppInfo_ x (defaultNamedArg y) 1396 return $ A.Var funs `app` e1 `app` e2 1397 I.UnivSort s -> do 1398 univs <- freshName_ ("univSort" :: String) -- TODO: hack 1399 e <- reify s 1400 return $ A.App defaultAppInfo_ (A.Var univs) $ defaultNamedArg e 1401 I.MetaS x es -> reify $ I.MetaV x es 1402 I.DefS d es -> reify $ I.Def d es 1403 I.DummyS s -> return $ A.Lit empty $ LitString $ T.pack s 1404 1405instance Reify Level where 1406 type ReifiesTo Level = Expr 1407 1408 reifyWhen = reifyWhenE 1409 reify l = ifM haveLevels (reify =<< reallyUnLevelView l) $ {-else-} do 1410 -- Andreas, 2017-09-18, issue #2754 1411 -- While type checking the level builtins, they are not 1412 -- available for debug printing. Thus, print some garbage instead. 1413 name <- freshName_ (".#Lacking_Level_Builtins#" :: String) 1414 return $ A.Var name 1415 1416instance (Free i, Reify i) => Reify (Abs i) where 1417 type ReifiesTo (Abs i) = (Name, ReifiesTo i) 1418 1419 reify (NoAbs x v) = freshName_ x >>= \name -> (name,) <$> reify v 1420 reify (Abs s v) = do 1421 1422 -- If the bound variable is free in the body, then the name "_" is 1423 -- replaced by "z". 1424 s <- return $ if isUnderscore s && 0 `freeIn` v then "z" else s 1425 1426 x <- C.setNotInScope <$> freshName_ s 1427 e <- addContext x -- type doesn't matter 1428 $ reify v 1429 return (x,e) 1430 1431instance Reify I.Telescope where 1432 type ReifiesTo I.Telescope = A.Telescope 1433 1434 reify EmptyTel = return [] 1435 reify (ExtendTel arg tel) = do 1436 Arg info e <- reify arg 1437 (x, bs) <- reify tel 1438 let r = getRange e 1439 name = domName arg 1440 tac <- traverse reify $ domTactic arg 1441 let xs = singleton $ Arg info $ Named name $ A.mkBinder_ x 1442 return $ TBind r tac xs e : bs 1443 1444instance Reify i => Reify (Dom i) where 1445 type ReifiesTo (Dom i) = Arg (ReifiesTo i) 1446 1447 reify (Dom{domInfo = info, unDom = i}) = Arg info <$> reify i 1448 1449instance Reify i => Reify (I.Elim' i) where 1450 type ReifiesTo (I.Elim' i) = I.Elim' (ReifiesTo i) 1451 1452 reify = traverse reify 1453 reifyWhen b = traverse (reifyWhen b) 1454 1455instance Reify i => Reify [i] where 1456 type ReifiesTo [i] = [ReifiesTo i] 1457 1458 reify = traverse reify 1459 reifyWhen b = traverse (reifyWhen b) 1460 1461instance (Reify i1, Reify i2) => Reify (i1, i2) where 1462 type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo i2) 1463 reify (x,y) = (,) <$> reify x <*> reify y 1464 1465instance (Reify i1, Reify i2, Reify i3) => Reify (i1,i2,i3) where 1466 type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3) 1467 reify (x,y,z) = (,,) <$> reify x <*> reify y <*> reify z 1468 1469instance (Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1,i2,i3,i4) where 1470 type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4) 1471 reify (x,y,z,w) = (,,,) <$> reify x <*> reify y <*> reify z <*> reify w 1472