1{-# LANGUAGE PatternGuards #-} 2 3{-| 4 5This module implements the Agda Abstract Machine used for compile-time reduction. It's a 6call-by-need environment machine with an implicit heap maintained using 'STRef's. See the 'AM' type 7below for a description of the machine. 8 9Some other tricks that improves performance: 10 11- Memoise getConstInfo. 12 13 A big chunk of the time during reduction is spent looking up definitions in the signature. Any 14 long-running reduction will use only a handful definitions though, so memoising getConstInfo is a 15 big win. 16 17- Optimised case trees. 18 19 Since we memoise getConstInfo we can do some preprocessing of the definitions, returning a 20 'CompactDef' instead of a 'Definition'. In particular we streamline the case trees used for 21 matching in a few ways: 22 23 - Drop constructor arity information. 24 - Use NameId instead of QName as map keys. 25 - Special branch for natural number successor. 26 27 None of these changes would make sense to incorporate into the actual case trees. The first two 28 loses information that we need in other places and the third would complicate a lot of code 29 working with case trees. 30 31 'CompactDef' also has a special representation for built-in/primitive 32 functions that can be implemented as pure functions from 'Literal's. 33 34-} 35module Agda.TypeChecking.Reduce.Fast 36 ( fastReduce, fastNormalise ) where 37 38import Control.Applicative hiding (empty) 39import Control.Monad.ST 40import Control.Monad.ST.Unsafe (unsafeSTToIO, unsafeInterleaveST) 41 42import Data.Map (Map) 43import qualified Data.Map as Map 44import qualified Data.IntMap as IntMap 45import qualified Data.IntSet as IntSet 46import qualified Data.List as List 47import Data.Semigroup ((<>)) 48import Data.Text (Text) 49import qualified Data.Text as T 50 51import System.IO.Unsafe (unsafePerformIO) 52import Data.IORef 53import Data.STRef 54import Data.Char 55 56import Agda.Syntax.Internal 57import Agda.Syntax.Common 58import Agda.Syntax.Position 59import Agda.Syntax.Literal 60 61import Agda.TypeChecking.CompiledClause 62import Agda.TypeChecking.Monad hiding (Closure(..)) 63import Agda.TypeChecking.Reduce as R 64import Agda.TypeChecking.Rewriting (rewrite) 65import Agda.TypeChecking.Substitute 66 67import Agda.Interaction.Options 68 69import Agda.Utils.CallStack ( withCurrentCallStack ) 70import Agda.Utils.Char 71import Agda.Utils.Float 72import Agda.Utils.Lens 73import Agda.Utils.List 74import Agda.Utils.Maybe 75import Agda.Utils.Null (empty) 76import Agda.Utils.Functor 77import Agda.Utils.Pretty 78import Agda.Utils.Size 79import Agda.Utils.Zipper 80import qualified Agda.Utils.SmallSet as SmallSet 81 82import Agda.Utils.Impossible 83 84import Debug.Trace 85 86-- * Compact definitions 87 88-- This is what the memoised getConstInfo returns. We essentially pick out only the 89-- information needed for fast reduction from the definition. 90 91data CompactDef = 92 CompactDef { cdefDelayed :: Bool 93 , cdefNonterminating :: Bool 94 , cdefUnconfirmed :: Bool 95 , cdefDef :: CompactDefn 96 , cdefRewriteRules :: RewriteRules 97 } 98 99data CompactDefn 100 = CFun { cfunCompiled :: FastCompiledClauses, cfunProjection :: Maybe QName } 101 | CCon { cconSrcCon :: ConHead, cconArity :: Int } 102 | CForce -- ^ primForce 103 | CErase -- ^ primErase 104 | CTyCon -- ^ Datatype or record type. Need to know this for primForce. 105 | CAxiom -- ^ Axiom or abstract defn 106 | CPrimOp Int ([Literal] -> Term) (Maybe FastCompiledClauses) 107 -- ^ Literals in reverse argument order 108 | COther -- ^ In this case we fall back to slow reduction 109 110data BuiltinEnv = BuiltinEnv 111 { bZero, bSuc, bTrue, bFalse, bRefl :: Maybe ConHead 112 , bPrimForce, bPrimErase :: Maybe QName } 113 114-- | Compute a 'CompactDef' from a regular definition. 115compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef 116compactDef bEnv def rewr = do 117 118 -- WARNING: don't use isPropM here because it relies on reduction, 119 -- which causes an infinite loop. 120 let isPrp = case getSort (defType def) of 121 Prop{} -> True 122 _ -> False 123 let irr = isPrp || isIrrelevant (defArgInfo def) 124 125 dontReduce <- not <$> shouldReduceDef (defName def) 126 127 cdefn <- 128 case theDef def of 129 _ | irr || dontReduce -> pure CAxiom 130 _ | Just (defName def) == bPrimForce bEnv -> pure CForce 131 _ | Just (defName def) == bPrimErase bEnv -> 132 case telView' (defType def) of 133 TelV tel _ | size tel == 5 -> pure CErase 134 | otherwise -> pure COther 135 -- Non-standard equality. Fall back to slow reduce. 136 _ | defBlocked def /= notBlocked_ -> pure COther -- Blocked definition 137 Constructor{conSrcCon = c, conArity = n} -> pure CCon{cconSrcCon = c, cconArity = n} 138 Function{funCompiled = Just cc, funClauses = _:_, funProjection = proj} -> 139 pure CFun{ cfunCompiled = fastCompiledClauses bEnv cc 140 , cfunProjection = projOrig <$> proj } 141 Function{funClauses = []} -> pure CAxiom 142 Function{} -> pure COther -- Incomplete definition 143 Datatype{dataClause = Nothing} -> pure CTyCon 144 Record{recClause = Nothing} -> pure CTyCon 145 Datatype{} -> pure COther -- TODO 146 Record{} -> pure COther -- TODO 147 Axiom{} -> pure CAxiom 148 DataOrRecSig{} -> pure CAxiom 149 AbstractDefn{} -> pure CAxiom 150 GeneralizableVar{} -> __IMPOSSIBLE__ 151 PrimitiveSort{} -> pure COther -- TODO 152 Primitive{ primName = name, primCompiled = cc } -> 153 case name of 154 -- "primShowInteger" -- integers are not literals 155 156 -- Natural numbers 157 "primNatPlus" -> mkPrim 2 $ natOp (+) 158 "primNatMinus" -> mkPrim 2 $ natOp (\ x y -> max 0 (x - y)) 159 "primNatTimes" -> mkPrim 2 $ natOp (*) 160 "primNatDivSucAux" -> mkPrim 4 $ natOp4 divAux 161 "primNatModSucAux" -> mkPrim 4 $ natOp4 modAux 162 "primNatLess" -> mkPrim 2 $ natRel (<) 163 "primNatEquality" -> mkPrim 2 $ natRel (==) 164 165 -- Word64 166 "primWord64ToNat" -> mkPrim 1 $ \ [LitWord64 a] -> nat (fromIntegral a) 167 "primWord64FromNat" -> mkPrim 1 $ \ [LitNat a] -> word (fromIntegral a) 168 169 -- Levels 170 -- "primLevelZero" -- levels are not literals 171 -- "primLevelSuc" -- levels are not literals 172 -- "primLevelMax" -- levels are not literals 173 174 -- Floats 175 "primFloatInequality" -> mkPrim 2 $ floatRel (<=) 176 "primFloatEquality" -> mkPrim 2 $ floatRel (==) 177 "primFloatLess" -> mkPrim 2 $ floatRel (<) 178 "primFloatIsInfinite" -> mkPrim 1 $ floatPred isInfinite 179 "primFloatIsNaN" -> mkPrim 1 $ floatPred isNaN 180 "primFloatIsDenormalized" -> mkPrim 1 $ floatPred isDenormalized 181 "primFloatIsNegativeZero" -> mkPrim 1 $ floatPred isNegativeZero 182 "primFloatIsSafeInteger" -> mkPrim 1 $ floatPred isSafeInteger 183 "primFloatToWord64" -> mkPrim 1 $ \ [LitFloat a] -> word (doubleToWord64 a) 184 -- "primFloatToWord64Injective" -- identities are not literals 185 "primNatToFloat" -> mkPrim 1 $ \ [LitNat a] -> float (fromIntegral a) 186 -- "primIntToFloat" -- integers are not literals 187 -- "primFloatRound" -- integers and maybe are not literals 188 -- "primFloatFloor" -- integers and maybe are not literals 189 -- "primFloatCeiling" -- integers and maybe are not literals 190 -- "primFloatToRatio" -- integers and sigma are not literals 191 -- "primRatioToFloat" -- integers are not literals 192 -- "primFloatDecode" -- integers and sigma are not literals 193 -- "primFloatEncode" -- integers are not literals 194 "primFloatPlus" -> mkPrim 2 $ floatOp (+) 195 "primFloatMinus" -> mkPrim 2 $ floatOp (-) 196 "primFloatTimes" -> mkPrim 2 $ floatOp (*) 197 "primFloatNegate" -> mkPrim 1 $ floatFun negate 198 "primFloatDiv" -> mkPrim 2 $ floatOp (/) 199 "primFloatSqrt" -> mkPrim 1 $ floatFun sqrt 200 "primFloatExp" -> mkPrim 1 $ floatFun exp 201 "primFloatLog" -> mkPrim 1 $ floatFun log 202 "primFloatSin" -> mkPrim 1 $ floatFun sin 203 "primFloatCos" -> mkPrim 1 $ floatFun cos 204 "primFloatTan" -> mkPrim 1 $ floatFun tan 205 "primFloatASin" -> mkPrim 1 $ floatFun asin 206 "primFloatACos" -> mkPrim 1 $ floatFun acos 207 "primFloatATan" -> mkPrim 1 $ floatFun atan 208 "primFloatATan2" -> mkPrim 2 $ floatOp atan2 209 "primFloatSinh" -> mkPrim 1 $ floatFun sinh 210 "primFloatCosh" -> mkPrim 1 $ floatFun cosh 211 "primFloatTanh" -> mkPrim 1 $ floatFun tanh 212 "primFloatASinh" -> mkPrim 1 $ floatFun asinh 213 "primFloatACosh" -> mkPrim 1 $ floatFun acosh 214 "primFloatATanh" -> mkPrim 1 $ floatFun atanh 215 "primFloatPow" -> mkPrim 2 $ floatOp (**) 216 "primShowFloat" -> mkPrim 1 $ \ [LitFloat a] -> string (show a) 217 218 -- Characters 219 "primCharEquality" -> mkPrim 2 $ charRel (==) 220 "primIsLower" -> mkPrim 1 $ charPred isLower 221 "primIsDigit" -> mkPrim 1 $ charPred isDigit 222 "primIsAlpha" -> mkPrim 1 $ charPred isAlpha 223 "primIsSpace" -> mkPrim 1 $ charPred isSpace 224 "primIsAscii" -> mkPrim 1 $ charPred isAscii 225 "primIsLatin1" -> mkPrim 1 $ charPred isLatin1 226 "primIsPrint" -> mkPrim 1 $ charPred isPrint 227 "primIsHexDigit" -> mkPrim 1 $ charPred isHexDigit 228 "primToUpper" -> mkPrim 1 $ charFun toUpper 229 "primToLower" -> mkPrim 1 $ charFun toLower 230 "primCharToNat" -> mkPrim 1 $ \ [LitChar a] -> nat (fromIntegral (fromEnum a)) 231 "primNatToChar" -> mkPrim 1 $ \ [LitNat a] -> char (integerToChar a) 232 "primShowChar" -> mkPrim 1 $ \ [a] -> string (prettyShow a) 233 234 -- Strings 235 -- "primStringToList" -- lists are not literals (TODO) 236 -- "primStringFromList" -- lists are not literals (TODO) 237 "primStringAppend" -> mkPrim 2 $ \ [LitString a, LitString b] -> text (b <> a) 238 "primStringEquality" -> mkPrim 2 $ \ [LitString a, LitString b] -> bool (b == a) 239 "primShowString" -> mkPrim 1 $ \ [a] -> string (prettyShow a) 240 241 -- "primErase" 242 -- "primForce" 243 -- "primForceLemma" 244 "primQNameEquality" -> mkPrim 2 $ \ [LitQName a, LitQName b] -> bool (b == a) 245 "primQNameLess" -> mkPrim 2 $ \ [LitQName a, LitQName b] -> bool (b < a) 246 "primShowQName" -> mkPrim 1 $ \ [LitQName a] -> string (prettyShow a) 247 -- "primQNameFixity" -- fixities are not literals (TODO) 248 "primMetaEquality" -> mkPrim 2 $ \ [LitMeta _ a, LitMeta _ b] -> bool (b == a) 249 "primMetaLess" -> mkPrim 2 $ \ [LitMeta _ a, LitMeta _ b] -> bool (b < a) 250 "primShowMeta" -> mkPrim 1 $ \ [LitMeta _ a] -> string (prettyShow a) 251 252 _ -> pure COther 253 where 254 fcc = fastCompiledClauses bEnv <$> cc 255 mkPrim n op = pure $ CPrimOp n op fcc 256 257 divAux k m n j = k + div (max 0 $ n + m - j) (m + 1) 258 modAux k m n j | n > j = mod (n - j - 1) (m + 1) 259 | otherwise = k + n 260 261 ~(Just true) = bTrue bEnv <&> \ c -> Con c ConOSystem [] 262 ~(Just false) = bFalse bEnv <&> \ c -> Con c ConOSystem [] 263 264 bool a = if a then true else false 265 nat a = Lit . LitNat $! a 266 word a = Lit . LitWord64 $! a 267 float a = Lit . LitFloat $! a 268 text a = Lit . LitString $! a 269 string a = text (T.pack a) 270 char a = Lit . LitChar $! a 271 272 -- Remember reverse order! 273 natOp f [LitNat a, LitNat b] = nat (f b a) 274 natOp _ _ = __IMPOSSIBLE__ 275 276 natOp4 f [LitNat a, LitNat b, LitNat c, LitNat d] = nat (f d c b a) 277 natOp4 _ _ = __IMPOSSIBLE__ 278 279 natRel f [LitNat a, LitNat b] = bool (f b a) 280 natRel _ _ = __IMPOSSIBLE__ 281 282 floatFun f [LitFloat a] = float (f a) 283 floatFun _ _ = __IMPOSSIBLE__ 284 285 floatOp f [LitFloat a, LitFloat b] = float (f b a) 286 floatOp _ _ = __IMPOSSIBLE__ 287 288 floatPred f [LitFloat a] = bool (f a) 289 floatPred _ _ = __IMPOSSIBLE__ 290 291 floatRel f [LitFloat a, LitFloat b] = bool (f b a) 292 floatRel _ _ = __IMPOSSIBLE__ 293 294 charFun f [LitChar a] = char (f a) 295 charFun _ _ = __IMPOSSIBLE__ 296 297 charPred f [LitChar a] = bool (f a) 298 charPred _ _ = __IMPOSSIBLE__ 299 300 charRel f [LitChar a, LitChar b] = bool (f b a) 301 charRel _ _ = __IMPOSSIBLE__ 302 303 return $ 304 CompactDef { cdefDelayed = defDelayed def == Delayed 305 , cdefNonterminating = defNonterminating def 306 , cdefUnconfirmed = defTerminationUnconfirmed def 307 , cdefDef = cdefn 308 , cdefRewriteRules = rewr 309 } 310 311-- Faster case trees ------------------------------------------------------ 312 313data FastCase c = FBranches 314 { fprojPatterns :: Bool 315 -- ^ We are constructing a record here (copatterns). 316 -- 'conBranches' lists projections. 317 , fconBranches :: Map NameId c 318 -- ^ Map from constructor (or projection) names to their arity 319 -- and the case subtree. (Projections have arity 0.) 320 , fsucBranch :: Maybe c 321 , flitBranches :: Map Literal c 322 -- ^ Map from literal to case subtree. 323 , fcatchAllBranch :: Maybe c 324 -- ^ (Possibly additional) catch-all clause. 325 , ffallThrough :: Bool 326 -- ^ (if True) In case of non-canonical argument use catchAllBranch. 327 } 328 329--UNUSED Liang-Ting Chen 2019-07-16 330--noBranches :: FastCase a 331--noBranches = FBranches{ fprojPatterns = False 332-- , fconBranches = Map.empty 333-- , fsucBranch = Nothing 334-- , flitBranches = Map.empty 335-- , fcatchAllBranch = Nothing 336-- , ffallThrough = False } 337 338-- | Case tree with bodies. 339 340data FastCompiledClauses 341 = FCase Int (FastCase FastCompiledClauses) 342 -- ^ @Case n bs@ stands for a match on the @n@-th argument 343 -- (counting from zero) with @bs@ as the case branches. 344 -- If the @n@-th argument is a projection, we have only 'conBranches' 345 -- with arity 0. 346 | FEta Int [Arg QName] FastCompiledClauses (Maybe FastCompiledClauses) 347 -- ^ Match on record constructor. Can still have a catch-all though. Just 348 -- contains the fields, not the actual constructor. 349 | FDone [Arg ArgName] Term 350 -- ^ @Done xs b@ stands for the body @b@ where the @xs@ contains hiding 351 -- and name suggestions for the free variables. This is needed to build 352 -- lambdas on the right hand side for partial applications which can 353 -- still reduce. 354 | FFail 355 -- ^ Absurd case. 356 357fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses 358fastCompiledClauses bEnv cc = 359 case cc of 360 Fail{} -> FFail 361 Done xs b -> FDone xs b 362 Case (Arg _ n) Branches{ etaBranch = Just (c, cc), catchAllBranch = ca } -> 363 FEta n (conFields c) (fastCompiledClauses bEnv $ content cc) (fastCompiledClauses bEnv <$> ca) 364 Case (Arg _ n) bs -> FCase n (fastCase bEnv bs) 365 366fastCase :: BuiltinEnv -> Case CompiledClauses -> FastCase FastCompiledClauses 367fastCase env (Branches proj con _ lit wild fT _) = 368 FBranches 369 { fprojPatterns = proj 370 , fconBranches = Map.mapKeysMonotonic (nameId . qnameName) $ fmap (fastCompiledClauses env . content) (stripSuc con) 371 , fsucBranch = fmap (fastCompiledClauses env . content) $ flip Map.lookup con . conName =<< bSuc env 372 , flitBranches = fmap (fastCompiledClauses env) lit 373 , ffallThrough = (Just True ==) fT 374 , fcatchAllBranch = fmap (fastCompiledClauses env) wild } 375 where 376 stripSuc | Just c <- bSuc env = Map.delete (conName c) 377 | otherwise = id 378 379 380{-# INLINE lookupCon #-} 381lookupCon :: QName -> FastCase c -> Maybe c 382lookupCon c (FBranches _ cons _ _ _ _) = Map.lookup (nameId $ qnameName c) cons 383 384-- QName memo ------------------------------------------------------------- 385 386{-# NOINLINE memoQName #-} 387memoQName :: (QName -> a) -> (QName -> a) 388memoQName f = unsafePerformIO $ do 389 tbl <- newIORef Map.empty 390 return (unsafePerformIO . f' tbl) 391 where 392 f' tbl x = do 393 let i = nameId (qnameName x) 394 m <- readIORef tbl 395 case Map.lookup i m of 396 Just y -> return y 397 Nothing -> do 398 let y = f x 399 writeIORef tbl (Map.insert i y m) 400 return y 401 402-- * Fast reduction 403 404data Normalisation = WHNF | NF 405 deriving (Eq) 406 407data ReductionFlags = ReductionFlags 408 { allowNonTerminating :: Bool 409 , allowUnconfirmed :: Bool 410 , hasRewriting :: Bool } 411 412-- | The entry point to the reduction machine. 413fastReduce :: Term -> ReduceM (Blocked Term) 414fastReduce = fastReduce' WHNF 415 416fastNormalise :: Term -> ReduceM Term 417fastNormalise v = ignoreBlocking <$> fastReduce' NF v 418 419fastReduce' :: Normalisation -> Term -> ReduceM (Blocked Term) 420fastReduce' norm v = do 421 let name (Con c _ _) = c 422 name _ = __IMPOSSIBLE__ 423 zero <- fmap name <$> getBuiltin' builtinZero 424 suc <- fmap name <$> getBuiltin' builtinSuc 425 true <- fmap name <$> getBuiltin' builtinTrue 426 false <- fmap name <$> getBuiltin' builtinFalse 427 refl <- fmap name <$> getBuiltin' builtinRefl 428 force <- fmap primFunName <$> getPrimitive' "primForce" 429 erase <- fmap primFunName <$> getPrimitive' "primErase" 430 let bEnv = BuiltinEnv { bZero = zero, bSuc = suc, bTrue = true, bFalse = false, bRefl = refl, 431 bPrimForce = force, bPrimErase = erase } 432 allowedReductions <- asksTC envAllowedReductions 433 rwr <- optRewriting <$> pragmaOptions 434 constInfo <- unKleisli $ \f -> do 435 info <- getConstInfo f 436 rewr <- if rwr then instantiateRewriteRules =<< getRewriteRulesFor f 437 else return [] 438 compactDef bEnv info rewr 439 let flags = ReductionFlags{ allowNonTerminating = NonTerminatingReductions `SmallSet.member` allowedReductions 440 , allowUnconfirmed = UnconfirmedReductions `SmallSet.member` allowedReductions 441 , hasRewriting = rwr } 442 ReduceM $ \ redEnv -> reduceTm redEnv bEnv (memoQName constInfo) norm flags v 443 444unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b) 445unKleisli f = ReduceM $ \ env x -> unReduceM (f x) env 446 447-- * Closures 448 449-- | The abstract machine represents terms as closures containing a 'Term', an environment, and a 450-- spine of eliminations. Note that the environment doesn't necessarily bind all variables in the 451-- term. The variables in the context in which the abstract machine is started are free in 452-- closures. The 'IsValue' argument tracks whether the closure is in weak-head normal form. 453data Closure s = Closure IsValue Term (Env s) (Spine s) 454 -- ^ The environment applies to the 'Term' argument. The spine contains closures 455 -- with their own environments. 456 457-- | Used to track if a closure is @Unevaluated@ or a @Value@ (in weak-head normal form), and if so 458-- why it cannot reduce further. 459data IsValue = Value Blocked_ | Unevaled 460 461-- | The spine is a list of eliminations. Application eliminations contain pointers. 462type Spine s = [Elim' (Pointer s)] 463 464isValue :: Closure s -> IsValue 465isValue (Closure isV _ _ _) = isV 466 467setIsValue :: IsValue -> Closure s -> Closure s 468setIsValue isV (Closure _ t env spine) = Closure isV t env spine 469 470-- | Apply a closure to a spine of eliminations. Note that this does not preserve the 'IsValue' 471-- field. 472clApply :: Closure s -> Spine s -> Closure s 473clApply c [] = c 474clApply (Closure _ t env es) es' = Closure Unevaled t env (es <> es') 475 476-- | Apply a closure to a spine, preserving the 'IsValue' field. Use with care, since usually 477-- eliminations do not preserve the value status. 478clApply_ :: Closure s -> Spine s -> Closure s 479clApply_ c [] = c 480clApply_ (Closure b t env es) es' = Closure b t env (es <> es') 481 482-- * Pointers and thunks 483 484-- | Spines and environments contain pointers to closures to enable call-by-need evaluation. 485data Pointer s = Pure (Closure s) 486 -- ^ Not a pointer. Used for closures that do not need to be shared to avoid 487 -- unnecessary updates. 488 | Pointer {-# UNPACK #-} !(STPointer s) 489 -- ^ An actual pointer is an 'STRef' to a 'Thunk'. The thunk is set to 'BlackHole' 490 -- during the evaluation of its contents to make debugging loops easier. 491 492type STPointer s = STRef s (Thunk (Closure s)) 493 494-- | A thunk is either a black hole or contains a value. 495data Thunk a = BlackHole | Thunk a 496 deriving (Functor) 497 498derefPointer :: Pointer s -> ST s (Thunk (Closure s)) 499derefPointer (Pure x) = return (Thunk x) 500derefPointer (Pointer ptr) = readSTRef ptr 501 502-- | In most cases pointers that we dereference do not contain black holes. 503derefPointer_ :: Pointer s -> ST s (Closure s) 504derefPointer_ ptr = do 505 Thunk cl <- derefPointer ptr 506 return cl 507 508-- | Only use for debug printing! 509unsafeDerefPointer :: Pointer s -> Thunk (Closure s) 510unsafeDerefPointer (Pure x) = Thunk x 511unsafeDerefPointer (Pointer p) = unsafePerformIO (unsafeSTToIO (readSTRef p)) 512 513readPointer :: STPointer s -> ST s (Thunk (Closure s)) 514readPointer = readSTRef 515 516storePointer :: STPointer s -> Closure s -> ST s () 517storePointer ptr !cl = writeSTRef ptr (Thunk cl) 518 -- Note the strict match. To prevent leaking memory in case of unnecessary updates. 519 520blackHole :: STPointer s -> ST s () 521blackHole ptr = writeSTRef ptr BlackHole 522 523-- | Create a thunk. If the closure is a naked variable we can reuse the pointer from the 524-- environment to avoid creating long pointer chains. 525createThunk :: Closure s -> ST s (Pointer s) 526createThunk (Closure _ (Var x []) env spine) 527 | null spine, Just p <- lookupEnv x env = return p 528createThunk cl = Pointer <$> newSTRef (Thunk cl) 529 530-- | Create a thunk that is not shared or updated. 531pureThunk :: Closure s -> Pointer s 532pureThunk = Pure 533 534-- * Environments 535 536-- | The environment of a closure binds pointers to deBruijn indicies. 537newtype Env s = Env [Pointer s] 538 539emptyEnv :: Env s 540emptyEnv = Env [] 541--UNUSED Liang-Ting Chen 2019-07-16 542--isEmptyEnv :: Env s -> Bool 543--isEmptyEnv (Env xs) = null xs 544 545envSize :: Env s -> Int 546envSize (Env xs) = length xs 547 548envToList :: Env s -> [Pointer s] 549envToList (Env xs) = xs 550 551extendEnv :: Pointer s -> Env s -> Env s 552extendEnv p (Env xs) = Env (p : xs) 553 554-- | Unsafe. 555lookupEnv_ :: Int -> Env s -> Pointer s 556lookupEnv_ i (Env e) = indexWithDefault __IMPOSSIBLE__ e i 557 558-- Andreas, 2018-11-12, which isn't this just Agda.Utils.List.!!! ? 559lookupEnv :: Int -> Env s -> Maybe (Pointer s) 560lookupEnv i e | i < n = Just (lookupEnv_ i e) 561 | otherwise = Nothing 562 where n = envSize e 563 564-- * The Agda Abstract Machine 565 566-- | The abstract machine state has two states 'Eval' and 'Match' that determine what the machine is 567-- currently working on: evaluating a closure in the Eval state and matching a spine against a 568-- case tree in the Match state. Both states contain a 'ControlStack' of continuations for what to 569-- do next. The heap is maintained implicitly using 'STRef's, hence the @s@ parameter. 570data AM s = Eval (Closure s) !(ControlStack s) 571 -- ^ Evaluate the given closure (the focus) to weak-head normal form. If the 'IsValue' 572 -- field of the closure is 'Value' we look at the control stack for what to do. Being 573 -- strict in the control stack is important! We can spend a lot of steps with 574 -- unevaluated closures (where we update, but don't look at the control stack). For 575 -- instance, long chains of 'suc' constructors. 576 | Match QName FastCompiledClauses (Spine s) (MatchStack s) (ControlStack s) 577 -- ^ @Match f cc spine stack ctrl@ Match the arguments @spine@ against the case tree 578 -- @cc@. The match stack contains a (possibly empty) list of 'CatchAll' frames and a 579 -- closure to return in case of a stuck match. 580 581-- | The control stack contains a list of continuations, i.e. what to do with 582-- the result of the current focus. 583type ControlStack s = [ControlFrame s] 584 585-- | The control stack for matching. Contains a list of CatchAllFrame's and the closure to return in 586-- case of a stuck match. 587data MatchStack s = [CatchAllFrame s] :> Closure s 588infixr 2 :>, >: 589 590(>:) :: CatchAllFrame s -> MatchStack s -> MatchStack s 591(>:) c (cs :> cl) = c : cs :> cl 592-- Previously written as: 593-- c >: cs :> cl = c : cs :> cl 594-- 595-- However, some versions/tools fail to parse infix data constructors properly. 596-- For example, stylish-haskell@0.9.2.1 fails with the following error: 597-- Language.Haskell.Stylish.Parse.parseModule: could not parse 598-- src/full/Agda/TypeChecking/Reduce/Fast.hs: ParseFailed (SrcLoc 599-- "<unknown>.hs" 625 1) "Parse error in pattern: " 600-- 601-- See https://ghc.haskell.org/trac/ghc/ticket/10018 which may be related. 602 603data CatchAllFrame s = CatchAll FastCompiledClauses (Spine s) 604 -- ^ @CatchAll cc spine@. Case trees are not fully expanded, that is, 605 -- inner matches can be partial and covered by a catch-all at a higher 606 -- level. This catch-all is represented on the match stack as a 607 -- @CatchAll@. @cc@ is the case tree in the catch-all case and @spine@ is 608 -- the value of the pattern variables at the point of the catch-all. 609 610-- An Elim' with a hole. 611data ElimZipper a = ApplyCxt ArgInfo 612 | IApplyType a a | IApplyFst a a | IApplySnd a a 613 deriving (Eq, Ord, Show, Functor, Foldable, Traversable) 614 615instance Zipper (ElimZipper a) where 616 type Carrier (ElimZipper a) = Elim' a 617 type Element (ElimZipper a) = a 618 619 firstHole (Apply arg) = Just (unArg arg, ApplyCxt (argInfo arg)) 620 firstHole (IApply a x y) = Just (a, IApplyType x y) 621 firstHole Proj{} = Nothing 622 623 plugHole x (ApplyCxt i) = Apply (Arg i x) 624 plugHole a (IApplyType x y) = IApply a x y 625 plugHole x (IApplyFst a y) = IApply a x y 626 plugHole y (IApplySnd a x) = IApply a x y 627 628 nextHole a (IApplyType x y) = Right (x, IApplyFst a y) 629 nextHole x (IApplyFst a y) = Right (y, IApplySnd a x) 630 nextHole y (IApplySnd a x) = Left (IApply a x y) 631 nextHole x c@ApplyCxt{} = Left (plugHole x c) 632 633-- | A spine with a single hole for a pointer. 634type SpineContext s = ComposeZipper (ListZipper (Elim' (Pointer s))) 635 (ElimZipper (Pointer s)) 636 637-- | Control frames are continuations that act on value closures. 638data ControlFrame s = CaseK QName ArgInfo (FastCase FastCompiledClauses) (Spine s) (Spine s) (MatchStack s) 639 -- ^ @CaseK f i bs spine0 spine1 stack@. Pattern match on the focus (with 640 -- arg info @i@) using the @bs@ case tree. @f@ is the name of the function 641 -- doing the matching, and @spine0@ and @spine1@ are the values bound to 642 -- the pattern variables to the left and right (respectively) of the 643 -- focus. The match stack contains catch-all cases we need to consider if 644 -- this match fails. 645 | ArgK (Closure s) (SpineContext s) 646 -- ^ @ArgK cl cxt@. Used when computing full normal forms. The closure is 647 -- the head and the context is the spine with the current focus removed. 648 | NormaliseK 649 -- ^ Indicates that the focus should be evaluated to full normal form. 650 | ForceK QName (Spine s) (Spine s) 651 -- ^ @ForceK f spine0 spine1@. Evaluating @primForce@ of the focus. @f@ is 652 -- the name of @primForce@ and is used to build the result if evaluation 653 -- gets stuck. @spine0@ are the level and type arguments and @spine1@ 654 -- contains (if not empty) the continuation and any additional 655 -- eliminations. 656 | EraseK QName (Spine s) (Spine s) (Spine s) (Spine s) 657 -- ^ @EraseK f spine0 spine1 spine2 spine3@. Evaluating @primErase@. The 658 -- first contains the level and type arguments. @spine1@ and @spine2@ 659 -- contain at most one argument between them. If in @spine1@ it's the 660 -- value closure of the first argument to be compared and if in @spine2@ 661 -- it's the unevaluated closure of the second argument. 662 -- @spine3@ contains the proof of equality we are erasing. It is passed 663 -- around but never actually inspected. 664 | NatSucK Integer 665 -- ^ @NatSucK n@. Add @n@ to the focus. If the focus computes to a natural 666 -- number literal this returns a new literal, otherwise it constructs @n@ 667 -- calls to @suc@. 668 | PrimOpK QName ([Literal] -> Term) [Literal] [Pointer s] (Maybe FastCompiledClauses) 669 -- ^ @PrimOpK f op lits es cc@. Evaluate the primitive function @f@ using 670 -- the Haskell function @op@. @op@ gets a list of literal values in 671 -- reverse order for the arguments of @f@ and computes the result as a 672 -- term. The already computed arguments (in reverse order) are @lits@ and 673 -- @es@ are the arguments that should be computed after the current focus. 674 -- In case of built-in functions with corresponding Agda implementations, 675 -- @cc@ contains the case tree. 676 | UpdateThunk [STPointer s] 677 -- ^ @UpdateThunk ps@. Update the pointers @ps@ with the value of the 678 -- current focus. 679 | ApplyK (Spine s) 680 -- ^ @ApplyK spine@. Apply the current focus to the eliminations in @spine@. 681 -- This is used when a thunk needs to be updated with a partial 682 -- application of a function. 683 684-- * Compilation and decoding 685 686-- | The initial abstract machine state. Wrap the term to be evaluated in an empty closure. Note 687-- that free variables of the term are treated as constants by the abstract machine. If computing 688-- full normal form we start off the control stack with a 'NormaliseK' continuation. 689compile :: Normalisation -> Term -> AM s 690compile nf t = Eval (Closure Unevaled t emptyEnv []) [NormaliseK | nf == NF] 691 692decodePointer :: Pointer s -> ST s Term 693decodePointer p = decodeClosure_ =<< derefPointer_ p 694 695-- | Note: it's important to be lazy in the spine and environment when decoding. Hence the 696-- 'unsafeInterleaveST' here and in 'decodeEnv', and the special version of 'parallelS' in 697-- 'decodeClosure'. 698decodeSpine :: Spine s -> ST s Elims 699decodeSpine spine = unsafeInterleaveST $ (traverse . traverse) decodePointer spine 700 701decodeEnv :: Env s -> ST s [Term] 702decodeEnv env = unsafeInterleaveST $ traverse decodePointer (envToList env) 703 704decodeClosure_ :: Closure s -> ST s Term 705decodeClosure_ = ignoreBlocking <.> decodeClosure 706 707-- | Turning an abstract machine closure back into a term. This happens in three cases: 708-- * when reduction is finished and we return the weak-head normal term to the outside world. 709-- * when the abstract machine encounters something it cannot handle and falls back to the slow 710-- reduction engine 711-- * when there are rewrite rules to apply 712decodeClosure :: Closure s -> ST s (Blocked Term) 713decodeClosure (Closure isV t env spine) = do 714 vs <- decodeEnv env 715 es <- decodeSpine spine 716 return $ applyE (applySubst (parS vs) t) es <$ b 717 where 718 parS = foldr (:#) IdS -- parallelS is too strict 719 b = case isV of 720 Value b -> b 721 Unevaled -> notBlocked () -- only when falling back to slow reduce in which case the 722 -- blocking tag is immediately discarded 723 724-- | Turn a list of internal syntax eliminations into a spine. This builds closures and allocates 725-- thunks for all the 'Apply' elims. 726elimsToSpine :: Env s -> Elims -> ST s (Spine s) 727elimsToSpine env es = do 728 spine <- mapM thunk es 729 forceSpine spine `seq` return spine 730 where 731 -- Need to be strict in mkClosure to avoid memory leak 732 forceSpine = foldl (\ () -> forceEl) () 733 forceEl (Apply (Arg _ (Pure Closure{}))) = () 734 forceEl (Apply (Arg _ (Pointer{}))) = () 735 forceEl _ = () 736 737 -- We don't preserve free variables of closures (in the sense of their 738 -- decoding), since we freely add things to the spines. 739 unknownFVs = setFreeVariables unknownFreeVariables 740 741 thunk (Apply (Arg i t)) = Apply . Arg (unknownFVs i) <$> createThunk (closure (getFreeVariables i) t) 742 thunk (Proj o f) = return (Proj o f) 743 thunk (IApply a x y) = IApply <$> mkThunk a <*> mkThunk x <*> mkThunk y 744 where mkThunk = createThunk . closure UnknownFVs 745 746 -- Going straight for a value for literals is mostly to make debug traces 747 -- less verbose and doesn't really buy anything performance-wise. 748 closure _ t@Lit{} = Closure (Value $ notBlocked ()) t emptyEnv [] 749 closure fv t = env' `seq` Closure Unevaled t env' [] 750 where env' = trimEnvironment fv env 751 752-- | Trim unused entries from an environment. Currently only trims closed terms for performance 753-- reasons. 754trimEnvironment :: FreeVariables -> Env s -> Env s 755trimEnvironment UnknownFVs env = env 756trimEnvironment (KnownFVs fvs) env 757 | IntSet.null fvs = emptyEnv 758 -- Environment trimming is too expensive (costs 50% on some benchmarks), and while it does make 759 -- some cases run in constant instead of linear space you need quite contrived examples to 760 -- notice the effect. 761 | otherwise = env -- Env $ trim 0 $ envToList env 762 where 763 -- Important: strict enough that the trimming actually happens 764 trim _ [] = [] 765 trim i (p : ps) 766 | IntSet.member i fvs = (p :) $! trim (i + 1) ps 767 | otherwise = (unusedPointer :) $! trim (i + 1) ps 768 769-- | Build an environment for a body with some given free variables from a spine of arguments. 770-- Returns a triple containing 771-- * the left-over variable names (in case of partial application) 772-- * the environment 773-- * the remaining spine (in case of over-application) 774buildEnv :: [Arg String] -> Spine s -> ([Arg String], Env s, Spine s) 775buildEnv xs spine = go xs spine emptyEnv 776 where 777 go [] sp env = ([], env, sp) 778 go xs0@(x : xs) sp env = 779 case sp of 780 [] -> (xs0, env, sp) 781 Apply c : sp -> go xs sp (unArg c `extendEnv` env) 782 IApply x y r : sp -> go xs sp (r `extendEnv` env) 783 _ -> __IMPOSSIBLE__ 784 785unusedPointerString :: Text 786unusedPointerString = T.pack (show (withCurrentCallStack Impossible)) 787 788unusedPointer :: Pointer s 789unusedPointer = Pure (Closure (Value $ notBlocked ()) 790 (Lit (LitString unusedPointerString)) emptyEnv []) 791 792-- * Running the abstract machine 793 794-- | Evaluating a term in the abstract machine. It gets the type checking state and environment in 795-- the 'ReduceEnv' argument, some precomputed built-in mappings in 'BuiltinEnv', the memoised 796-- 'getConstInfo' function, a couple of flags (allow non-terminating function unfolding, and 797-- whether rewriting is enabled), and a term to reduce. The result is the weak-head normal form of 798-- the term with an attached blocking tag. 799reduceTm :: ReduceEnv -> BuiltinEnv -> (QName -> CompactDef) -> Normalisation -> ReductionFlags -> Term -> Blocked Term 800reduceTm rEnv bEnv !constInfo normalisation ReductionFlags{..} = 801 compileAndRun . traceDoc "-- fast reduce --" 802 where 803 -- Helpers to get information from the ReduceEnv. 804 metaStore = redSt rEnv ^. stMetaStore 805 -- Are we currently instance searching. In that case we don't fail hard on missing clauses. This 806 -- is a (very unsatisfactory) work-around for #3870. 807 speculative = redSt rEnv ^. stConsideringInstance 808 getMeta m = maybe __IMPOSSIBLE__ mvInstantiation (IntMap.lookup (metaId m) metaStore) 809 partialDefs = runReduce getPartialDefs 810 rewriteRules f = cdefRewriteRules (constInfo f) 811 callByNeed = envCallByNeed (redEnv rEnv) && not (optCallByName $ redSt rEnv ^. stPragmaOptions) 812 iview = runReduce intervalView' 813 814 runReduce :: ReduceM a -> a 815 runReduce m = unReduceM m rEnv 816 817 -- Debug output. Taking care that we only look at the verbosity level once. 818 hasVerb tag lvl = unReduceM (hasVerbosity tag lvl) rEnv 819 doDebug = hasVerb "tc.reduce.fast" 110 820 traceDoc :: Doc -> a -> a 821 traceDoc 822 | doDebug = trace . show 823 | otherwise = const id 824 825 -- Checking for built-in zero and suc 826 BuiltinEnv{ bZero = zero, bSuc = suc, bRefl = refl0 } = bEnv 827 conNameId = nameId . qnameName . conName 828 isZero = case zero of 829 Nothing -> const False 830 Just z -> (conNameId z ==) . conNameId 831 isSuc = case suc of 832 Nothing -> const False 833 Just s -> (conNameId s ==) . conNameId 834 835 -- If there's a non-standard equality (for instance doubly-indexed) we fall back to slow reduce 836 -- for primErase and "unbind" refl. 837 refl = refl0 >>= \ c -> if cconArity (cdefDef $ constInfo $ conName c) == 0 838 then Just c else Nothing 839 840 -- The entry point of the machine. 841 compileAndRun :: Term -> Blocked Term 842 compileAndRun t = runST (runAM (compile normalisation t)) 843 844 -- Run the machine in a given state. Prints the state if the right verbosity level is active. 845 runAM :: AM s -> ST s (Blocked Term) 846 runAM = if doDebug then \ s -> trace (prettyShow s) (runAM' s) 847 else runAM' 848 849 -- The main function. This is where the stuff happens! 850 runAM' :: AM s -> ST s (Blocked Term) 851 852 -- Base case: The focus is a value closure and the control stack is empty. Decode and return. 853 runAM' (Eval cl@(Closure Value{} _ _ _) []) = decodeClosure cl 854 855 -- Unevaluated closure: inspect the term and take the appropriate action. For instance, 856 -- - Change to the 'Match' state if a definition 857 -- - Look up in the environment if variable 858 -- - Perform a beta step if lambda and application elimination in the spine 859 -- - Perform a record beta step if record constructor and projection elimination in the spine 860 runAM' s@(Eval cl@(Closure Unevaled t env spine) !ctrl) = {-# SCC "runAM.Eval" #-} 861 case t of 862 863 -- Case: definition. Enter 'Match' state if defined function or shift to evaluating an 864 -- argument and pushing the appropriate control frame for primitive functions. Fall back to 865 -- slow reduce for unsupported definitions. 866 Def f [] -> 867 evalIApplyAM spine ctrl $ 868 let CompactDef{ cdefDelayed = delayed 869 , cdefNonterminating = nonterm 870 , cdefUnconfirmed = unconf 871 , cdefDef = def } = constInfo f 872 dontUnfold = (nonterm && not allowNonTerminating) || 873 (unconf && not allowUnconfirmed) || 874 (delayed && not (unfoldDelayed ctrl)) 875 in case def of 876 CFun{ cfunCompiled = cc } 877 | dontUnfold -> rewriteAM done 878 | otherwise -> runAM (Match f cc spine ([] :> cl) ctrl) 879 CAxiom -> rewriteAM done 880 CTyCon -> rewriteAM done 881 CCon{} -> runAM done -- Only happens for builtinSharp (which is a Def when you bind it) 882 CForce | (spine0, Apply v : spine1) <- splitAt 4 spine -> 883 evalPointerAM (unArg v) [] (ForceK f spine0 spine1 : ctrl) 884 CForce -> runAM done -- partially applied 885 CErase | (spine0, Apply v : spine1 : spine2) <- splitAt 2 spine -> 886 evalPointerAM (unArg v) [] (EraseK f spine0 [] [spine1] spine2 : ctrl) 887 CErase -> runAM done -- partially applied 888 CPrimOp n op cc | length spine == n, -- PrimOps can't be over-applied. They don't 889 Just (v : vs) <- allApplyElims spine -> -- return functions or records. 890 evalPointerAM (unArg v) [] (PrimOpK f op [] (map unArg vs) cc : ctrl) 891 CPrimOp{} -> runAM done -- partially applied 892 COther -> fallbackAM s 893 894 -- Case: zero. Return value closure with literal 0. 895 Con c i [] | isZero c -> 896 runAM (evalTrueValue (Lit (LitNat 0)) emptyEnv spine ctrl) 897 898 -- Case: suc. Suc is strict in its argument to make sure we return a literal whenever 899 -- possible. Push a 'NatSucK' frame on the control stack and evaluate the argument. 900 Con c i [] | isSuc c, Apply v : _ <- spine -> 901 evalPointerAM (unArg v) [] (sucCtrl ctrl) 902 903 -- Case: constructor. Perform beta reduction if projected from, otherwise return a value. 904 Con c i [] 905 -- Constructors of types in Prop are not representex as 906 -- CCon, so this match might fail! 907 | CCon{cconSrcCon = c', cconArity = ar} <- cdefDef (constInfo (conName c)) -> 908 evalIApplyAM spine ctrl $ 909 case splitAt ar spine of 910 (args, Proj _ p : spine') 911 -> evalPointerAM (unArg arg) spine' ctrl -- Andreas #2170: fit argToDontCare here?! 912 where 913 fields = map unArg $ conFields c 914 Just n = List.elemIndex p fields 915 Apply arg = args !! n 916 _ -> rewriteAM (evalTrueValue (Con c' i []) env spine ctrl) 917 | otherwise -> runAM done 918 919 -- Case: variable. Look up the variable in the environment and evaluate the resulting 920 -- pointer. If the variable is not in the environment it's a free variable and we adjust the 921 -- deBruijn index appropriately. 922 Var x [] -> 923 evalIApplyAM spine ctrl $ 924 case lookupEnv x env of 925 Nothing -> runAM (evalValue (notBlocked ()) (Var (x - envSize env) []) emptyEnv spine ctrl) 926 Just p -> evalPointerAM p spine ctrl 927 928 -- Case: lambda. Perform the beta reduction if applied. Otherwise it's a value. 929 Lam h b -> 930 case spine of 931 [] -> runAM done 932 elim : spine' -> 933 case b of 934 Abs _ b -> runAM (evalClosure b (getArg elim `extendEnv` env) spine' ctrl) 935 NoAbs _ b -> runAM (evalClosure b env spine' ctrl) 936 where 937 getArg (Apply v) = unArg v 938 getArg (IApply _ _ v) = v 939 getArg Proj{} = __IMPOSSIBLE__ 940 941 -- Case: values. Literals and function types are already in weak-head normal form. 942 -- We throw away the environment for literals mostly to make debug printing less verbose. 943 -- And we know the spine is empty since literals cannot be applied or projected. 944 Lit{} -> runAM (evalTrueValue t emptyEnv [] ctrl) 945 Pi{} -> runAM done 946 DontCare{} -> runAM done 947 948 -- Case: non-empty spine. If the focused term has a non-empty spine, we shift the 949 -- eliminations onto the spine. 950 Def f es -> shiftElims (Def f []) emptyEnv env es 951 Con c i es -> shiftElims (Con c i []) emptyEnv env es 952 Var x es -> shiftElims (Var x []) env env es 953 954 -- Case: metavariable. If it's instantiated evaluate the value. Meta instantiations are open 955 -- terms with a specified list of free variables. buildEnv constructs the appropriate 956 -- environment for the closure. Avoiding shifting spines for open metas 957 -- save a bit of performance. 958 MetaV m es -> evalIApplyAM spine ctrl $ 959 case getMeta m of 960 InstV xs t -> do 961 spine' <- elimsToSpine env es 962 let (zs, env, !spine'') = buildEnv xs (spine' <> spine) 963 runAM (evalClosure (lams zs t) env spine'' ctrl) 964 _ -> runAM (Eval (mkValue (blocked m ()) cl) ctrl) 965 966 -- Case: unsupported. These terms are not handled by the abstract machine, so we fall back 967 -- to slowReduceTerm for these. 968 Level{} -> fallbackAM s 969 Sort{} -> fallbackAM s 970 Dummy{} -> fallbackAM s 971 972 where done = Eval (mkValue (notBlocked ()) cl) ctrl 973 shiftElims t env0 env es = do 974 spine' <- elimsToSpine env es 975 runAM (evalClosure t env0 (spine' <> spine) ctrl) 976 977 -- If the current focus is a value closure, we look at the control stack. 978 979 -- Case NormaliseK: The focus is a weak-head value that should be fully normalised. 980 runAM' s@(Eval cl@(Closure b t env spine) (NormaliseK : ctrl)) = 981 case t of 982 Def _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl 983 Con _ _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl 984 Var _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl 985 MetaV _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl 986 987 Lit{} -> runAM done 988 989 -- We might get these from fallbackAM 990 Def f es -> shiftElims (Def f []) emptyEnv env es 991 Con c i es -> shiftElims (Con c i []) emptyEnv env es 992 Var x es -> shiftElims (Var x []) env env es 993 MetaV m es -> shiftElims (MetaV m []) emptyEnv env es 994 995 _ -> fallbackAM s -- fallbackAM knows about NormaliseK 996 997 where done = Eval (mkValue (notBlocked ()) cl) ctrl 998 shiftElims t env0 env es = do 999 spine' <- elimsToSpine env es 1000 runAM (Eval (Closure b t env0 (spine' <> spine)) (NormaliseK : ctrl)) 1001 1002 -- Case: ArgK: We successfully normalised an argument. Start on the next argument, or if there 1003 -- isn't one we're done. 1004 runAM' (Eval cl (ArgK cl0 cxt : ctrl)) = 1005 case nextHole (pureThunk cl) cxt of 1006 Left spine -> runAM (Eval (clApply_ cl0 spine) ctrl) 1007 Right (p, cxt') -> evalPointerAM p [] (NormaliseK : ArgK cl0 cxt' : ctrl) 1008 1009 -- Case: NatSucK m 1010 1011 -- If literal add m to the literal, 1012 runAM' (Eval cl@(Closure Value{} (Lit (LitNat n)) _ _) (NatSucK m : ctrl)) = 1013 runAM (evalTrueValue (Lit $! LitNat $! m + n) emptyEnv [] ctrl) 1014 1015 -- otherwise apply 'suc' m times. 1016 runAM' (Eval cl (NatSucK m : ctrl)) = 1017 runAM (Eval (mkValue (notBlocked ()) $ plus m cl) ctrl) 1018 where 1019 plus 0 cl = cl 1020 plus n cl = 1021 trueValue (Con (fromMaybe __IMPOSSIBLE__ suc) ConOSystem []) emptyEnv $ 1022 Apply (defaultArg arg) : [] 1023 where arg = pureThunk (plus (n - 1) cl) 1024 1025 -- Case: PrimOpK 1026 1027 -- If literal apply the primitive function if no more arguments, otherwise 1028 -- store the literal in the continuation and evaluate the next argument. 1029 runAM' (Eval (Closure _ (Lit a) _ _) (PrimOpK f op vs es cc : ctrl)) = 1030 case es of 1031 [] -> runAM (evalTrueValue (op (a : vs)) emptyEnv [] ctrl) 1032 e : es' -> evalPointerAM e [] (PrimOpK f op (a : vs) es' cc : ctrl) 1033 1034 -- If not a literal we use the case tree if there is one, otherwise we are stuck. 1035 runAM' (Eval cl@(Closure (Value blk) _ _ _) (PrimOpK f _ vs es mcc : ctrl)) = 1036 case mcc of 1037 Nothing -> rewriteAM (Eval stuck ctrl) 1038 Just cc -> runAM (Match f cc spine ([] :> notstuck) ctrl) 1039 where 1040 p = pureThunk cl 1041 lits = map (pureThunk . litClos) (reverse vs) 1042 spine = fmap (Apply . defaultArg) $ lits <> [p] <> es 1043 stuck = Closure (Value blk) (Def f []) emptyEnv spine 1044 notstuck = Closure Unevaled (Def f []) emptyEnv spine 1045 litClos l = trueValue (Lit l) emptyEnv [] 1046 1047 -- Case: ForceK. Here we need to check if the argument is a canonical form (i.e. not a variable 1048 -- or stuck function call) and if so apply the function argument to the value. If it's not 1049 -- canonical we are stuck. 1050 runAM' (Eval arg@(Closure (Value blk) t _ _) (ForceK pf spine0 spine1 : ctrl)) 1051 | isCanonical t = 1052 case spine1 of 1053 Apply k : spine' -> 1054 evalPointerAM (unArg k) (elim : spine') ctrl 1055 [] -> -- Partial application of primForce to canonical argument, return λ k → k arg. 1056 runAM (evalTrueValue (lam (defaultArg "k") $ Var 0 [Apply $ defaultArg $ Var 1 []]) 1057 (argPtr `extendEnv` emptyEnv) [] ctrl) 1058 _ -> __IMPOSSIBLE__ 1059 | otherwise = rewriteAM (Eval stuck ctrl) 1060 where 1061 argPtr = pureThunk arg 1062 elim = Apply (defaultArg argPtr) 1063 spine' = spine0 <> [elim] <> spine1 1064 stuck = Closure (Value blk) (Def pf []) emptyEnv spine' 1065 1066 isCanonical = \case 1067 Lit{} -> True 1068 Con{} -> True 1069 Lam{} -> True 1070 Pi{} -> True 1071 Sort{} -> True 1072 Level{} -> True 1073 DontCare{} -> True 1074 Dummy{} -> False 1075 MetaV{} -> False 1076 Var{} -> False 1077 Def q _ -- Type constructors (data/record) are considered canonical for 'primForce'. 1078 | CTyCon <- cdefDef (constInfo q) -> True 1079 | otherwise -> False 1080 1081 -- Case: EraseK. We evaluate both arguments to values, then do a simple check for the easy 1082 -- cases and otherwise fall back to slow reduce. 1083 runAM' (Eval cl2@(Closure Value{} arg2 _ _) (EraseK f spine0 [Apply p1] _ spine3 : ctrl)) = do 1084 cl1@(Closure _ arg1 _ sp1) <- derefPointer_ (unArg p1) 1085 case (arg1, arg2) of 1086 (Lit l1, Lit l2) | l1 == l2, isJust refl -> 1087 runAM (evalTrueValue (Con (fromJust refl) ConOSystem []) emptyEnv [] ctrl) 1088 _ -> 1089 let spine = spine0 ++ map (Apply . hide . defaultArg . pureThunk) [cl1, cl2] ++ spine3 in 1090 fallbackAM (evalClosure (Def f []) emptyEnv spine ctrl) 1091 runAM' (Eval cl1@(Closure Value{} _ _ _) (EraseK f spine0 [] [Apply p2] spine3 : ctrl)) = 1092 evalPointerAM (unArg p2) [] (EraseK f spine0 [Apply $ hide $ defaultArg $ pureThunk cl1] [] spine3 : ctrl) 1093 runAM' (Eval _ (EraseK{} : _)) = 1094 __IMPOSSIBLE__ 1095 1096 -- Case: UpdateThunk. Write the value to the pointers in the UpdateThunk frame. 1097 runAM' (Eval cl@(Closure Value{} _ _ _) (UpdateThunk ps : ctrl)) = 1098 mapM_ (`storePointer` cl) ps >> runAM (Eval cl ctrl) 1099 1100 -- Case: ApplyK. Application after thunk update. Add the spine from the control frame to the 1101 -- closure. 1102 runAM' (Eval cl@(Closure Value{} _ _ _) (ApplyK spine : ctrl)) = 1103 runAM (Eval (clApply cl spine) ctrl) 1104 1105 -- Case: CaseK. Pattern matching against a value. If it's a stuck value the pattern match is 1106 -- stuck and we return the closure from the match stack (see stuckMatch). Otherwise we need to 1107 -- find a matching branch switch to the Match state. If there is no matching branch we look for 1108 -- a CatchAll in the match stack, or fail if there isn't one (see failedMatch). If the current 1109 -- branches contain a catch-all case we need to push a CatchAll on the match stack if picking 1110 -- one of the other branches. 1111 runAM' (Eval cl@(Closure (Value blk) t env spine) ctrl0@(CaseK f i bs spine0 spine1 stack : ctrl)) = 1112 {-# SCC "runAM.CaseK" #-} 1113 case blk of 1114 Blocked{} | null [()|Con{} <- [t]] -> stuck -- we might as well check the blocking tag first 1115 _ -> case t of 1116 -- Case: suc constructor 1117 Con c ci [] | isSuc c -> matchSuc $ matchCatchall $ failedMatch f stack ctrl 1118 1119 -- Case: constructor 1120 Con c ci [] -> matchCon c ci (length spine) $ matchCatchall $ failedMatch f stack ctrl 1121 1122 -- Case: non-empty elims. We can get here from a fallback (which builds a value without 1123 -- shifting arguments onto spine) 1124 Con c ci es -> do 1125 spine' <- elimsToSpine env es 1126 runAM (evalValue blk (Con c ci []) emptyEnv (spine' <> spine) ctrl0) 1127 -- Case: natural number literals. Literal natural number patterns are translated to 1128 -- suc-matches, so there is no need to try matchLit. 1129 Lit (LitNat 0) -> matchLitZero $ matchCatchall $ failedMatch f stack ctrl 1130 Lit (LitNat n) -> matchLitSuc n $ matchCatchall $ failedMatch f stack ctrl 1131 1132 -- Case: literal 1133 Lit l -> matchLit l $ matchCatchall $ failedMatch f stack ctrl 1134 1135 -- Case: hcomp 1136 Def q [] | isJust $ lookupCon q bs -> matchCon' q (length spine) $ matchCatchall $ failedMatch f stack ctrl 1137 Def q es | isJust $ lookupCon q bs -> do 1138 spine' <- elimsToSpine env es 1139 runAM (evalValue blk (Def q []) emptyEnv (spine' <> spine) ctrl0) 1140 1141 -- Case: not constructor or literal. In this case we are stuck. 1142 _ -> stuck 1143 where 1144 -- If ffallThrough is set we take the catch-all (if any) rather than being stuck. I think 1145 -- this happens for partial functions with --cubical (@saizan: is this true?). 1146 stuck | ffallThrough bs = matchCatchall reallyStuck 1147 | otherwise = reallyStuck 1148 1149 reallyStuck = do 1150 -- Compute new reason for being stuck. See Agda.Syntax.Internal.stuckOn for the logic. 1151 blk' <- case blk of 1152 Blocked{} -> return blk 1153 NotBlocked r _ -> decodeClosure_ cl <&> \ v -> NotBlocked (stuckOn (Apply $ Arg i v) r) () 1154 stuckMatch blk' stack ctrl 1155 1156 -- This the spine at this point in the matching. A catch-all match doesn't change the spine. 1157 catchallSpine = spine0 <> [Apply $ Arg i p] <> spine1 1158 where p = pureThunk cl -- cl is already a value so no need to thunk it. 1159 1160 -- Push catch-all frame on the match stack if there is a catch-all (and we're not taking it 1161 -- right now). 1162 catchallStack = case fcatchAllBranch bs of 1163 Nothing -> stack 1164 Just cc -> CatchAll cc catchallSpine >: stack 1165 1166 -- The matchX functions below all take an extra argument which is what to do if there is no 1167 -- appropriate branch in the case tree. ifJust is maybe with a different argument order 1168 -- letting you chain a bunch if maybe matches in if-then-elseif fashion. 1169 (m `ifJust` f) z = maybe z f m 1170 1171 -- Matching constructor: Switch to the Match state, inserting the constructor arguments in 1172 -- the spine between spine0 and spine1. 1173 matchCon c ci ar = matchCon' (conName c) ar 1174 matchCon' q ar = lookupCon q bs `ifJust` \ cc -> 1175 runAM (Match f cc (spine0 <> spine <> spine1) catchallStack ctrl) 1176 1177 -- Catch-all: Don't add a CatchAll to the match stack since this _is_ the catch-all. 1178 matchCatchall = fcatchAllBranch bs `ifJust` \ cc -> 1179 runAM (Match f cc catchallSpine stack ctrl) 1180 1181 -- Matching literal: Switch to the Match state. There are no arguments to add to the spine. 1182 matchLit l = Map.lookup l (flitBranches bs) `ifJust` \ cc -> 1183 runAM (Match f cc (spine0 <> spine1) catchallStack ctrl) 1184 1185 -- Matching a 'suc' constructor: Insert the argument in the spine. 1186 matchSuc = fsucBranch bs `ifJust` \ cc -> 1187 runAM (Match f cc (spine0 <> spine <> spine1) catchallStack ctrl) 1188 1189 -- Matching a non-zero natural number literal: Subtract one from the literal and 1190 -- insert it in the spine for the Match state. 1191 matchLitSuc n = fsucBranch bs `ifJust` \ cc -> 1192 runAM (Match f cc (spine0 <> [Apply $ defaultArg arg] <> spine1) catchallStack ctrl) 1193 where n' = n - 1 1194 arg = pureThunk $ trueValue (Lit $ LitNat n') emptyEnv [] 1195 1196 -- Matching a literal 0. Simply calls matchCon with the zero constructor. 1197 matchLitZero = matchCon (fromMaybe __IMPOSSIBLE__ zero) ConOSystem 0 1198 -- If we have a nat literal we have builtin zero. 1199 1200 -- Case: Match state. Here we look at the case tree and take the appropriate action: 1201 -- - FFail: stuck 1202 -- - FDone: evaluate body 1203 -- - FEta: eta expand argument 1204 -- - FCase on projection: pick corresponding branch and keep matching 1205 -- - FCase on argument: push CaseK frame on control stack and evaluate argument 1206 runAM' (Match f cc spine stack ctrl) = {-# SCC "runAM.Match" #-} 1207 case cc of 1208 -- Absurd match. You can get here for open terms. 1209 FFail -> stuckMatch (NotBlocked AbsurdMatch ()) stack ctrl 1210 1211 -- Matching complete. Compute the environment for the body and switch to the Eval state. 1212 FDone xs body -> do 1213 -- Don't ask me why, but not being strict in the spine causes a memory leak. 1214 let (zs, env, !spine') = buildEnv xs spine 1215 runAM (Eval (Closure Unevaled (lams zs body) env spine') ctrl) 1216 1217 -- A record pattern match. This does not block evaluation (since that would violate eta 1218 -- equality), so in this case we replace the argument with its projections in the spine and 1219 -- keep matching. 1220 FEta n fs cc ca -> 1221 case splitAt n spine of -- Question: add lambda here? doesn't 1222 (_, []) -> done Underapplied -- matter for equality, but might for 1223 (spine0, Apply e : spine1) -> do -- rewriting or 'with'. 1224 -- Replace e by its projections in the spine. And don't forget a 1225 -- CatchAll frame if there's a catch-all. 1226 let projClosure (Arg ai f) = Closure Unevaled (Var 0 []) (extendEnv (unArg e) emptyEnv) [Proj ProjSystem f] 1227 projs <- mapM (createThunk . projClosure) fs 1228 let spine' = spine0 <> map (Apply . defaultArg) projs <> spine1 1229 stack' = caseMaybe ca stack $ \ cc -> CatchAll cc spine >: stack 1230 runAM (Match f cc spine' stack' ctrl) 1231 _ -> __IMPOSSIBLE__ 1232 1233 -- Split on nth elimination in the spine. Can be either a regular split or a copattern 1234 -- split. 1235 FCase n bs -> 1236 case splitAt n spine of 1237 -- If the nth elimination is not given, we're stuck. 1238 (_, []) -> done Underapplied 1239 -- Apply elim: push the current match on the control stack and evaluate the argument 1240 (spine0, Apply e : spine1) -> 1241 evalPointerAM (unArg e) [] $ CaseK f (argInfo e) bs spine0 spine1 stack : ctrl 1242 -- Projection elim: in this case we must be in a copattern split and find the projection 1243 -- in the case tree and keep going. If it's not there it might be because it's not the 1244 -- original projection (issue #2265). If so look up the original projection instead. 1245 -- That _really_ should be there since copattern splits cannot be partial. Except of 1246 -- course, the user might still have written a partial function so we should check 1247 -- partialDefs before throwing an impossible (#3012). 1248 (spine0, Proj o p : spine1) -> 1249 case lookupCon p bs <|> ((`lookupCon` bs) =<< op) of 1250 Nothing 1251 | f `elem` partialDefs -> stuckMatch (NotBlocked MissingClauses ()) stack ctrl 1252 | otherwise -> __IMPOSSIBLE__ 1253 Just cc -> runAM (Match f cc (spine0 <> spine1) stack ctrl) 1254 where CFun{ cfunProjection = op } = cdefDef (constInfo p) 1255 (_, IApply{} : _) -> __IMPOSSIBLE__ -- Paths cannot be defined by pattern matching 1256 where done why = stuckMatch (NotBlocked why ()) stack ctrl 1257 1258 -- 'evalPointerAM p spine ctrl'. Evaluate the closure pointed to by 'p' applied to 'spine' with 1259 -- the control stack 'ctrl'. If 'p' points to an unevaluated thunk, a 'BlackHole' is written to 1260 -- the pointer and an 'UpdateThunk' frame is pushed to the control stack. In this case the 1261 -- application to the spine has to be deferred until after the update through an 'ApplyK' frame. 1262 evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term) 1263 evalPointerAM (Pure cl) spine ctrl = runAM (Eval (clApply cl spine) ctrl) 1264 evalPointerAM (Pointer p) spine ctrl = readPointer p >>= \ case 1265 BlackHole -> __IMPOSSIBLE__ 1266 Thunk cl@(Closure Unevaled _ _ _) | callByNeed -> do 1267 blackHole p 1268 runAM (Eval cl $ updateThunkCtrl p $ [ApplyK spine | not (null spine)] ++ ctrl) 1269 Thunk cl -> runAM (Eval (clApply cl spine) ctrl) 1270 1271 -- 'evalIApplyAM spine ctrl fallback' checks if any 'IApply x y r' has a canonical 'r' (i.e. 0 or 1), 1272 -- in that case continues evaluating 'x' or 'y' with the rest of 'spine' and same 'ctrl'. 1273 -- If no such 'IApply' is found we continue with 'fallback'. 1274 evalIApplyAM :: Spine s -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term) 1275 evalIApplyAM es ctrl fallback = go es 1276 where 1277 -- written as a worker/wrapper to possibly trigger some 1278 -- specialization wrt fallback 1279 go [] = fallback 1280 go (IApply x y r : es) = do 1281 br <- evalPointerAM r [] [] 1282 case iview $ ignoreBlocking br of 1283 IZero -> evalPointerAM x es ctrl 1284 IOne -> evalPointerAM y es ctrl 1285 _ -> (<* br) <$> go es 1286 go (e : es) = go es 1287 1288 -- Normalise the spine and apply the closure to the result. The closure must be a value closure. 1289 normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term) 1290 normaliseArgsAM cl [] ctrl = runAM (Eval cl ctrl) -- nothing to do 1291 normaliseArgsAM cl spine ctrl = 1292 case firstHole spine of -- v Only projections, nothing to do. Note clApply_ and not clApply (or we'd loop) 1293 Nothing -> runAM (Eval (clApply_ cl spine) ctrl) 1294 Just (p, cxt) -> evalPointerAM p [] (NormaliseK : ArgK cl cxt : ctrl) 1295 1296 -- Fall back to slow reduction. This happens if we encounter a definition that's not supported 1297 -- by the machine (like a primitive function that does not work on literals), or a term that is 1298 -- not supported (Level and Sort at the moment). In this case we decode the current 1299 -- focus to a 'Term', call slow reduction and pack up the result in a value closure. If the top 1300 -- of the control stack is a 'NormaliseK' and the focus is a value closure (i.e. already in 1301 -- weak-head normal form) we call 'slowNormaliseArgs' and pop the 'NormaliseK' frame. Otherwise 1302 -- we use 'slowReduceTerm' to compute a weak-head normal form. 1303 fallbackAM :: AM s -> ST s (Blocked Term) 1304 fallbackAM (Eval c ctrl) = do 1305 v <- decodeClosure_ c 1306 runAM (mkValue $ runReduce $ slow v) 1307 where mkValue b = evalValue (() <$ b) (ignoreBlocking b) emptyEnv [] ctrl' 1308 (slow, ctrl') = case ctrl of 1309 NormaliseK : ctrl' 1310 | Value{} <- isValue c -> (notBlocked <.> slowNormaliseArgs, ctrl') 1311 _ -> (slowReduceTerm, ctrl) 1312 fallbackAM _ = __IMPOSSIBLE__ 1313 1314 -- If rewriting is enabled, try to apply rewrite rules to the current focus before considering 1315 -- it a value. The current state must be 'Eval' and the focus a value closure. Take care to only 1316 -- test the 'hasRewriting' flag once. 1317 rewriteAM :: AM s -> ST s (Blocked Term) 1318 rewriteAM = if hasRewriting then rewriteAM' else runAM 1319 1320 -- Applying rewrite rules to the current focus. This needs to decode the current focus, call 1321 -- rewriting and pack the result back up in a closure. In case some rewrite rules actually fired 1322 -- the next state is an unevaluated closure, otherwise it's a value closure. 1323 rewriteAM' :: AM s -> ST s (Blocked Term) 1324 rewriteAM' s@(Eval (Closure (Value blk) t env spine) ctrl) 1325 | null rewr = runAM s 1326 | otherwise = traceDoc ("R" <+> pretty s) $ do 1327 v0 <- decodeClosure_ (Closure Unevaled t env []) 1328 es <- decodeSpine spine 1329 case runReduce (rewrite blk (applyE v0) rewr es) of 1330 NoReduction b -> runAM (evalValue (() <$ b) (ignoreBlocking b) emptyEnv [] ctrl) 1331 YesReduction _ v -> runAM (evalClosure v emptyEnv [] ctrl) 1332 where rewr = case t of 1333 Def f [] -> rewriteRules f 1334 Con c _ [] -> rewriteRules (conName c) 1335 _ -> __IMPOSSIBLE__ 1336 rewriteAM' _ = 1337 __IMPOSSIBLE__ 1338 1339 -- Add a NatSucK frame to the control stack. Pack consecutive suc's into a single frame. 1340 sucCtrl :: ControlStack s -> ControlStack s 1341 sucCtrl (NatSucK !n : ctrl) = NatSucK (n + 1) : ctrl 1342 sucCtrl ctrl = NatSucK 1 : ctrl 1343 1344 -- Add a UpdateThunk frame to the control stack. Pack consecutive updates into a single frame. 1345 updateThunkCtrl :: STPointer s -> ControlStack s -> ControlStack s 1346 updateThunkCtrl p (UpdateThunk ps : ctrl) = UpdateThunk (p : ps) : ctrl 1347 updateThunkCtrl p ctrl = UpdateThunk [p] : ctrl 1348 1349 -- Only unfold delayed (corecursive) definitions if the result is being cased on. 1350 unfoldDelayed :: ControlStack s -> Bool 1351 unfoldDelayed [] = False 1352 unfoldDelayed (CaseK{} : _) = True 1353 unfoldDelayed (PrimOpK{} : _) = False 1354 unfoldDelayed (NatSucK{} : _) = False 1355 unfoldDelayed (NormaliseK{} : _) = False 1356 unfoldDelayed (ArgK{} : _) = False 1357 unfoldDelayed (UpdateThunk{} : ctrl) = unfoldDelayed ctrl 1358 unfoldDelayed (ApplyK{} : ctrl) = unfoldDelayed ctrl 1359 unfoldDelayed (ForceK{} : ctrl) = unfoldDelayed ctrl 1360 unfoldDelayed (EraseK{} : ctrl) = unfoldDelayed ctrl 1361 1362 -- When matching is stuck we return the closure from the 'MatchStack' with the appropriate 1363 -- 'IsValue' set. 1364 stuckMatch :: Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term) 1365 stuckMatch blk (_ :> cl) ctrl = rewriteAM (Eval (mkValue blk cl) ctrl) 1366 1367 -- On a mismatch we find the next 'CatchAll' on the control stack and 1368 -- continue matching from there. If there isn't one we get an incomplete 1369 -- matching error (or get stuck if the function is marked partial). 1370 failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term) 1371 failedMatch f (CatchAll cc spine : stack :> cl) ctrl = runAM (Match f cc spine (stack :> cl) ctrl) 1372 failedMatch f ([] :> cl) ctrl 1373 -- Bad work-around for #3870: don't fail hard during instance search. 1374 | speculative = rewriteAM (Eval (mkValue (NotBlocked MissingClauses ()) cl) ctrl) 1375 | f `elem` partialDefs = rewriteAM (Eval (mkValue (NotBlocked MissingClauses ()) cl) ctrl) 1376 | otherwise = runReduce $ 1377 traceSLn "impossible" 10 ("Incomplete pattern matching when applying " ++ prettyShow f) 1378 __IMPOSSIBLE__ 1379 1380 -- Some helper functions to build machine states and closures. 1381 evalClosure t env spine = Eval (Closure Unevaled t env spine) 1382 evalValue b t env spine = Eval (Closure (Value b) t env spine) 1383 evalTrueValue = evalValue $ notBlocked () 1384 trueValue t env spine = Closure (Value $ notBlocked ()) t env spine 1385 mkValue b = setIsValue (Value b) 1386 1387 -- Building lambdas 1388 lams :: [Arg String] -> Term -> Term 1389 lams xs t = foldr lam t xs 1390 1391 lam :: Arg String -> Term -> Term 1392 lam x t = Lam (argInfo x) (Abs (unArg x) t) 1393 1394-- Pretty printing -------------------------------------------------------- 1395 1396instance Pretty a => Pretty (FastCase a) where 1397 prettyPrec p (FBranches _cop cs suc ls m _) = 1398 mparens (p > 0) $ vcat (prettyMap_ cs ++ prettyMap_ ls ++ prSuc suc ++ prC m) 1399 where 1400 prC Nothing = [] 1401 prC (Just x) = ["_ ->" <?> pretty x] 1402 1403 prSuc Nothing = [] 1404 prSuc (Just x) = ["suc ->" <?> pretty x] 1405 1406instance Pretty FastCompiledClauses where 1407 pretty (FDone xs t) = ("done" <+> prettyList xs) <?> prettyPrec 10 t 1408 pretty FFail = "fail" 1409 pretty (FEta n _ cc ca) = 1410 text ("eta " ++ show n ++ " of") <?> 1411 vcat ("{} ->" <?> pretty cc : 1412 [ "_ ->" <?> pretty cc | Just cc <- [ca] ]) 1413 pretty (FCase n bs) | fprojPatterns bs = 1414 sep [ text $ "project " ++ show n 1415 , nest 2 $ pretty bs 1416 ] 1417 pretty (FCase n bs) = 1418 text ("case " ++ show n ++ " of") <?> pretty bs 1419 1420instance Pretty a => Pretty (Thunk a) where 1421 prettyPrec _ BlackHole = "<BLACKHOLE>" 1422 prettyPrec p (Thunk cl) = prettyPrec p cl 1423 1424instance Pretty (Pointer s) where 1425 prettyPrec p = prettyPrec p . unsafeDerefPointer 1426 1427instance Pretty (Closure s) where 1428 prettyPrec _ (Closure Value{} (Lit (LitString unused)) _ _) 1429 | unused == unusedPointerString = "_" 1430 prettyPrec p (Closure isV t env spine) = 1431 mparens (p > 9) $ fsep [ text tag 1432 , nest 2 $ prettyPrec 10 t 1433 , nest 2 $ prettyList $ zipWith envEntry [0..] (envToList env) 1434 , nest 2 $ prettyList spine ] 1435 where envEntry i c = text ("@" ++ show i ++ " =") <+> pretty c 1436 tag = case isV of Value{} -> "V"; Unevaled -> "E" 1437 1438instance Pretty (AM s) where 1439 prettyPrec p (Eval cl ctrl) = prettyPrec p cl <?> prettyList ctrl 1440 prettyPrec p (Match f cc sp stack ctrl) = 1441 mparens (p > 9) $ sep [ "M" <+> pretty f 1442 , nest 2 $ prettyList sp 1443 , nest 2 $ prettyPrec 10 cc 1444 , nest 2 $ pretty stack 1445 , nest 2 $ prettyList ctrl ] 1446 1447instance Pretty (CatchAllFrame s) where 1448 pretty CatchAll{} = "CatchAll" 1449 1450instance Pretty (MatchStack s) where 1451 pretty ([] :> _) = empty 1452 pretty (ca :> _) = prettyList ca 1453 1454instance Pretty (ControlFrame s) where 1455 prettyPrec p (CaseK f _ _ _ _ mc) = mparens (p > 9) $ ("CaseK" <+> pretty (qnameName f)) <?> pretty mc 1456 prettyPrec p (ForceK _ spine0 spine1) = mparens (p > 9) $ "ForceK" <?> prettyList (spine0 <> spine1) 1457 prettyPrec p (EraseK _ sp0 sp1 sp2 sp3) = mparens (p > 9) $ sep [ "EraseK" 1458 , nest 2 $ prettyList sp0 1459 , nest 2 $ prettyList sp1 1460 , nest 2 $ prettyList sp2 1461 , nest 2 $ prettyList sp3 ] 1462 prettyPrec _ (NatSucK n) = text ("+" ++ show n) 1463 prettyPrec p (PrimOpK f _ vs cls _) = mparens (p > 9) $ sep [ "PrimOpK" <+> pretty f 1464 , nest 2 $ prettyList vs 1465 , nest 2 $ prettyList cls ] 1466 prettyPrec p (UpdateThunk ps) = mparens (p > 9) $ "UpdateThunk" <+> text (show (length ps)) 1467 prettyPrec p (ApplyK spine) = mparens (p > 9) $ "ApplyK" <?> prettyList spine 1468 prettyPrec p NormaliseK = "NormaliseK" 1469 prettyPrec p (ArgK cl _) = mparens (p > 9) $ sep [ "ArgK" <+> prettyPrec 10 cl ] 1470