    {-# LANGUAGE PatternGuards #-}

    {-|

    This module implements the Agda Abstract Machine used for compile-time reduction. It's a
    call-by-need environment machine with an implicit heap maintained using 'STRef's. See the 'AM' type
    below for a description of the machine.

    Some other tricks that improves performance:

    - Memoise getConstInfo.

      A big chunk of the time during reduction is spent looking up definitions in the signature. Any
      long-running reduction will use only a handful definitions though, so memoising getConstInfo is a
      big win.

    - Optimised case trees.

      Since we memoise getConstInfo we can do some preprocessing of the definitions, returning a
      'CompactDef' instead of a 'Definition'. In particular we streamline the case trees used for
      matching in a few ways:

        - Drop constructor arity information.
        - Use NameId instead of QName as map keys.
        - Special branch for natural number successor.

      None of these changes would make sense to incorporate into the actual case trees. The first two
      loses information that we need in other places and the third would complicate a lot of code
      working with case trees.

      'CompactDef' also has a special representation for built-in/primitive
      functions that can be implemented as pure functions from 'Literal's.

    -}
    module Agda.TypeChecking.Reduce.Fast
      ( fastReduce, fastNormalise ) where

    import Prelude hiding ((!!))

    import Control.Applicative hiding (empty)
    import Control.Monad.ST
    import Control.Monad.ST.Unsafe (unsafeSTToIO, unsafeInterleaveST)

    import qualified Data.HashMap.Strict as HMap
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Map.Strict as MapS
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Semigroup ((<>))
    import Data.Text (Text)
    import qualified Data.Text as T

    import System.IO.Unsafe (unsafePerformIO)
    import Data.IORef
    import Data.STRef
    import Data.Char

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Literal

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Monad hiding (Closure(..))
    import Agda.TypeChecking.Reduce as R
    import Agda.TypeChecking.Rewriting (rewrite)
    import Agda.TypeChecking.Substitute

    import Agda.Interaction.Options

    import Agda.Utils.CallStack ( withCurrentCallStack )
    import Agda.Utils.Char
    import Agda.Utils.Float
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null (empty)
    import Agda.Utils.Functor
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Size
    import Agda.Utils.Zipper
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

    import Debug.Trace

    -- * Compact definitions

    -- This is what the memoised getConstInfo returns. We essentially pick out only the
    -- information needed for fast reduction from the definition.

    data CompactDef =
      CompactDef { CompactDef -> Bool
    cdefNonterminating :: Bool
                 , CompactDef -> Bool
    cdefUnconfirmed    :: Bool
                 , CompactDef -> CompactDefn
    cdefDef            :: CompactDefn
                 , CompactDef -> RewriteRules
    cdefRewriteRules   :: RewriteRules
                 }

    data CompactDefn
      = CFun  { CompactDefn -> FastCompiledClauses
    cfunCompiled  :: FastCompiledClauses, CompactDefn -> Maybe QName
    cfunProjection :: Maybe QName }
      | CCon  { CompactDefn -> ConHead
    cconSrcCon :: ConHead, CompactDefn -> Int
    cconArity :: Int }
      | CForce   -- ^ primForce
      | CErase   -- ^ primErase
      | CTyCon   -- ^ Datatype or record type. Need to know this for primForce.
      | CAxiom   -- ^ Axiom or abstract defn
      | CPrimOp Int ([Literal] -> Term) (Maybe FastCompiledClauses)
                -- ^ Literals in reverse argument order
      | COther  -- ^ In this case we fall back to slow reduction

    data BuiltinEnv = BuiltinEnv
      { BuiltinEnv -> Maybe ConHead
    bZero, BuiltinEnv -> Maybe ConHead
    bSuc, BuiltinEnv -> Maybe ConHead
    bTrue, BuiltinEnv -> Maybe ConHead
    bFalse, BuiltinEnv -> Maybe ConHead
    bRefl :: Maybe ConHead
      , BuiltinEnv -> Maybe QName
    bPrimForce, BuiltinEnv -> Maybe QName
    bPrimErase  :: Maybe QName }

    -- | Compute a 'CompactDef' from a regular definition.
    compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
    compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
    compactDef BuiltinEnv
    bEnv Definition
    def RewriteRules
    rewr = do

      -- WARNING: don't use isPropM here because it relies on reduction,
      -- which causes an infinite loop.
      let isPrp :: Bool
    isPrp = Sort' Term -> Bool
    forall t. Sort' t -> Bool
    isProp (Sort' Term -> Bool) -> Sort' Term -> Bool
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort' Term
    forall a. LensSort a => a -> Sort' Term
    getSort (Type -> Sort' Term) -> Type -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def

      shouldReduce <- QName -> ReduceM Bool
    forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
    shouldReduceDef (Definition -> QName
    defName Definition
    def)
      allowed <- asksTC envAllowedReductions

      let isConOrProj = case Definition -> Defn
    theDef Definition
    def of
            Constructor{} -> Bool
    True
            Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right{} } -> Bool
    True
            Defn
    _ -> Bool
    False
      let allowReduce = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
            [ Bool
    shouldReduce
            , [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
              [ AllowedReduction
    RecursiveReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed
              , Bool
    isConOrProj Bool -> Bool -> Bool
    && AllowedReduction
    ProjectionReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed
              , Defn -> Bool
    isInlineFun (Definition -> Defn
    theDef Definition
    def) Bool -> Bool -> Bool
    && AllowedReduction
    InlineReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed
              , Defn -> Bool
    definitelyNonRecursive_ (Definition -> Defn
    theDef Definition
    def) Bool -> Bool -> Bool
    && [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
                [ Definition -> Bool
    defCopatternLHS Definition
    def Bool -> Bool -> Bool
    && AllowedReduction
    CopatternReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed
                , AllowedReduction
    FunctionReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed
                ]
              ]
            , Bool -> Bool
    not (Definition -> Bool
    defNonterminating Definition
    def) Bool -> Bool -> Bool
    || AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    SmallSet.member AllowedReduction
    NonTerminatingReductions AllowedReductions
    allowed
            , Bool -> Bool
    not (Definition -> Bool
    defTerminationUnconfirmed Definition
    def) Bool -> Bool -> Bool
    || AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    SmallSet.member AllowedReduction
    UnconfirmedReductions AllowedReductions
    allowed
            , Bool -> Bool
    not Bool
    isPrp
            , Bool -> Bool
    not (Definition -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Definition
    def)
            ]

      cdefn <-
        case theDef def of
          Defn
    _ | Bool -> Bool
    not Bool
    allowReduce -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          Defn
    _ | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (Definition -> QName
    defName Definition
    def) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == BuiltinEnv -> Maybe QName
    bPrimForce BuiltinEnv
    bEnv   -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CForce
          Defn
    _ | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (Definition -> QName
    defName Definition
    def) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == BuiltinEnv -> Maybe QName
    bPrimErase BuiltinEnv
    bEnv ->
              case Type -> TelView
    telView' (Definition -> Type
    defType Definition
    def) of
                TelV Tele (Dom Type)
    tel Type
    _ | Tele (Dom Type) -> Peano
    forall a. Sized a => a -> Peano
    natSize Tele (Dom Type)
    tel Peano -> Peano -> Bool
    forall a. Eq a => a -> a -> Bool
    == Peano
    5 -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CErase
                           | Bool
    otherwise        -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther
                              -- Non-standard equality. Fall back to slow reduce.
          Defn
    _ | Definition -> Blocked_
    defBlocked Definition
    def Blocked_ -> Blocked_ -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Blocked_
    forall t. Blocked' t ()
    notBlocked_ -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- Blocked definition
          Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c, conArity :: Defn -> Int
    conArity = Int
    n} -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CCon{cconSrcCon :: ConHead
    cconSrcCon = ConHead
    c, cconArity :: Int
    cconArity = Int
    n}
          Function{funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Just CompiledClauses
    cc, funClauses :: Defn -> [Clause]
    funClauses = Clause
    _:[Clause]
    _, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Either ProjectionLikenessMissing Projection
    proj} ->
            CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CFun{ cfunCompiled :: FastCompiledClauses
    cfunCompiled   = BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    bEnv CompiledClauses
    cc
                     , cfunProjection :: Maybe QName
    cfunProjection = Projection -> QName
    projOrig (Projection -> QName) -> Maybe Projection -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ProjectionLikenessMissing -> Maybe Projection)
    -> (Projection -> Maybe Projection)
    -> Either ProjectionLikenessMissing Projection
    -> Maybe Projection
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe Projection -> ProjectionLikenessMissing -> Maybe Projection
    forall a b. a -> b -> a
    const Maybe Projection
    forall a. Maybe a
    Nothing) Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Either ProjectionLikenessMissing Projection
    proj }
          Function{funClauses :: Defn -> [Clause]
    funClauses = []}      -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          Function{}                     -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- Incomplete definition
          Datatype{dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    Nothing} -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CTyCon
          Record{recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    Nothing}    -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CTyCon
          Datatype{}                     -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Record{}                       -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Axiom{}                        -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          DataOrRecSig{}                 -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          AbstractDefn{}                 -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          GeneralizableVar{}             -> ReduceM CompactDefn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PrimitiveSort{}                -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Primitive{}
            | Bool -> Bool
    not (AllowedReduction
    FunctionReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowed)
            -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          Primitive{ primName :: Defn -> PrimitiveId
    primName = PrimitiveId
    name, primCompiled :: Defn -> Maybe CompiledClauses
    primCompiled = Maybe CompiledClauses
    cc } ->
            case PrimitiveId
    name of
              -- "primShowInteger"            -- integers are not literals

              -- Natural numbers
              PrimitiveId
    PrimNatPlus                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer) -> [Literal] -> Term
    natOp Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+)
              PrimitiveId
    PrimNatMinus                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer) -> [Literal] -> Term
    natOp (\ Integer
    x Integer
    y -> Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    0 (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    y))
              PrimitiveId
    PrimNatTimes                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer) -> [Literal] -> Term
    natOp Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*)
              PrimitiveId
    PrimNatDivSucAux             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    4 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer -> Integer -> Integer)
    -> [Literal] -> Term
    natOp4 Integer -> Integer -> Integer -> Integer -> Integer
    forall {a}. Integral a => a -> a -> a -> a -> a
    divAux
              PrimitiveId
    PrimNatModSucAux             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    4 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer -> Integer -> Integer)
    -> [Literal] -> Term
    natOp4 Integer -> Integer -> Integer -> Integer -> Integer
    forall {a}. Integral a => a -> a -> a -> a -> a
    modAux
              PrimitiveId
    PrimNatLess                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Bool) -> [Literal] -> Term
    natRel Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    (<)
              PrimitiveId
    PrimNatEquality              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Bool) -> [Literal] -> Term
    natRel Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)

              -- Word64
              PrimitiveId
    PrimWord64ToNat              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitWord64 Word64
    a] -> Integer -> Term
    nat (Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    a)
              PrimitiveId
    PrimWord64FromNat            -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitNat Integer
    a]    -> Word64 -> Term
    word (Integer -> Word64
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    a)

              -- Levels
              -- "primLevelZero"              -- levels are not literals
              -- "primLevelSuc"               -- levels are not literals
              -- "primLevelMax"               -- levels are not literals

              -- Floats
              PrimitiveId
    PrimFloatInequality          -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Bool) -> [Literal] -> Term
    floatRel Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=)
              PrimitiveId
    PrimFloatEquality            -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Bool) -> [Literal] -> Term
    floatRel Double -> Double -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)
              PrimitiveId
    PrimFloatLess                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Bool) -> [Literal] -> Term
    floatRel Double -> Double -> Bool
    forall a. Ord a => a -> a -> Bool
    (<)
              PrimitiveId
    PrimFloatIsInfinite          -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Bool) -> [Literal] -> Term
    floatPred Double -> Bool
    forall a. RealFloat a => a -> Bool
    isInfinite
              PrimitiveId
    PrimFloatIsNaN               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Bool) -> [Literal] -> Term
    floatPred Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN
              PrimitiveId
    PrimFloatIsNegativeZero      -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Bool) -> [Literal] -> Term
    floatPred Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero
              PrimitiveId
    PrimFloatIsSafeInteger       -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Bool) -> [Literal] -> Term
    floatPred Double -> Bool
    isSafeInteger
              -- "primFloatToWord64"          -- returns a maybe
              -- "primFloatToWord64Injective" -- identities are not literals
              PrimitiveId
    PrimNatToFloat               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitNat Integer
    a] -> Double -> Term
    float (Integer -> Double
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    a)
              -- "primIntToFloat"             -- integers are not literals
              -- "primFloatRound"             -- integers and maybe are not literals
              -- "primFloatFloor"             -- integers and maybe are not literals
              -- "primFloatCeiling"           -- integers and maybe are not literals
              -- "primFloatToRatio"           -- integers and sigma are not literals
              -- "primRatioToFloat"           -- integers are not literals
              -- "primFloatDecode"            -- integers and sigma are not literals
              -- "primFloatEncode"            -- integers are not literals
              PrimitiveId
    PrimFloatPlus                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    forall a. Num a => a -> a -> a
    (+)
              PrimitiveId
    PrimFloatMinus               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp (-)
              PrimitiveId
    PrimFloatTimes               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    forall a. Num a => a -> a -> a
    (*)
              PrimitiveId
    PrimFloatNegate              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Num a => a -> a
    negate
              PrimitiveId
    PrimFloatDiv                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    forall a. Fractional a => a -> a -> a
    (/)
              PrimitiveId
    PrimFloatSqrt                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    sqrt
              PrimitiveId
    PrimFloatExp                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    exp
              PrimitiveId
    PrimFloatLog                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    log
              PrimitiveId
    PrimFloatSin                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    sin
              PrimitiveId
    PrimFloatCos                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    cos
              PrimitiveId
    PrimFloatTan                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    tan
              PrimitiveId
    PrimFloatASin                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    asin
              PrimitiveId
    PrimFloatACos                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    acos
              PrimitiveId
    PrimFloatATan                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    atan
              PrimitiveId
    PrimFloatATan2               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    forall a. RealFloat a => a -> a -> a
    atan2
              PrimitiveId
    PrimFloatSinh                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    sinh
              PrimitiveId
    PrimFloatCosh                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    cosh
              PrimitiveId
    PrimFloatTanh                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    tanh
              PrimitiveId
    PrimFloatASinh               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    asinh
              PrimitiveId
    PrimFloatACosh               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    acosh
              PrimitiveId
    PrimFloatATanh               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    forall a. Floating a => a -> a
    atanh
              PrimitiveId
    PrimFloatPow                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    forall a. Floating a => a -> a -> a
    (**)
              PrimitiveId
    PrimShowFloat                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitFloat Double
    a] -> VerboseKey -> Term
    string (Double -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Double
    a)

              -- Characters
              PrimitiveId
    PrimCharEquality             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Char -> Bool) -> [Literal] -> Term
    charRel Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)
              PrimitiveId
    PrimIsLower                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isLower
              PrimitiveId
    PrimIsDigit                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isDigit
              PrimitiveId
    PrimIsAlpha                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isAlpha
              PrimitiveId
    PrimIsSpace                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isSpace
              PrimitiveId
    PrimIsAscii                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isAscii
              PrimitiveId
    PrimIsLatin1                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isLatin1
              PrimitiveId
    PrimIsPrint                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isPrint
              PrimitiveId
    PrimIsHexDigit               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    isHexDigit
              PrimitiveId
    PrimToUpper                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Char) -> [Literal] -> Term
    charFun Char -> Char
    toUpper
              PrimitiveId
    PrimToLower                  -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ (Char -> Char) -> [Literal] -> Term
    charFun Char -> Char
    toLower
              PrimitiveId
    PrimCharToNat                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitChar Char
    a] -> Integer -> Term
    nat (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    a))
              PrimitiveId
    PrimNatToChar                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitNat Integer
    a] -> Char -> Term
    char (Integer -> Char
    integerToChar Integer
    a)
              PrimitiveId
    PrimShowChar                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [Literal
    a] -> VerboseKey -> Term
    string (Literal -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow Literal
    a)

              -- Strings
              -- "primStringToList"           -- lists are not literals (TODO)
              -- "primStringFromList"         -- lists are not literals (TODO)
              PrimitiveId
    PrimStringAppend             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitString Text
    a, LitString Text
    b] -> Text -> Term
    text (Text
    b Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    a)
              PrimitiveId
    PrimStringEquality           -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitString Text
    a, LitString Text
    b] -> Bool -> Term
    bool (Text
    b Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    a)
              PrimitiveId
    PrimShowString               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [Literal
    a] -> VerboseKey -> Term
    string (Literal -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow Literal
    a)

              -- "primErase"
              -- "primForce"
              -- "primForceLemma"
              PrimitiveId
    PrimQNameEquality            -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitQName QName
    a, LitQName QName
    b] -> Bool -> Term
    bool (QName
    b QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    a)
              PrimitiveId
    PrimQNameLess                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitQName QName
    a, LitQName QName
    b] -> Bool -> Term
    bool (QName
    b QName -> QName -> Bool
    forall a. Ord a => a -> a -> Bool
    < QName
    a)
              PrimitiveId
    PrimShowQName                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitQName QName
    a] -> VerboseKey -> Term
    string (QName -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow QName
    a)
              -- "primQNameFixity"            -- fixities are not literals (TODO)
              PrimitiveId
    PrimMetaEquality             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitMeta TopLevelModuleName' Range
    _ MetaId
    a, LitMeta TopLevelModuleName' Range
    _ MetaId
    b] -> Bool -> Term
    bool (MetaId
    b MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    a)
              PrimitiveId
    PrimMetaLess                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    2 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitMeta TopLevelModuleName' Range
    _ MetaId
    a, LitMeta TopLevelModuleName' Range
    _ MetaId
    b] -> Bool -> Term
    bool (MetaId
    b MetaId -> MetaId -> Bool
    forall a. Ord a => a -> a -> Bool
    < MetaId
    a)
              PrimitiveId
    PrimShowMeta                 -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    1 (([Literal] -> Term) -> ReduceM CompactDefn)
    -> ([Literal] -> Term) -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ \ [LitMeta TopLevelModuleName' Range
    _ MetaId
    a] -> VerboseKey -> Term
    string (MetaId -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow MetaId
    a)

              PrimitiveId
    _                            -> CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther
            where
              fcc :: Maybe FastCompiledClauses
    fcc = BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    bEnv (CompiledClauses -> FastCompiledClauses)
    -> Maybe CompiledClauses -> Maybe FastCompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CompiledClauses
    cc
              mkPrim :: Int -> ([Literal] -> Term) -> ReduceM CompactDefn
    mkPrim Int
    n [Literal] -> Term
    op = CompactDefn -> ReduceM CompactDefn
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CompactDefn -> ReduceM CompactDefn)
    -> CompactDefn -> ReduceM CompactDefn
    forall a b. (a -> b) -> a -> b
    $ Int
    -> ([Literal] -> Term) -> Maybe FastCompiledClauses -> CompactDefn
    CPrimOp Int
    n [Literal] -> Term
    op Maybe FastCompiledClauses
    fcc

              divAux :: a -> a -> a -> a -> a
    divAux a
    k a
    m a
    n a
    j = a
    k a -> a -> a
    forall a. Num a => a -> a -> a
    + a -> a -> a
    forall a. Integral a => a -> a -> a
    div (a -> a -> a
    forall a. Ord a => a -> a -> a
    max a
    0 (a -> a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    m a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    j) (a
    m a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1)
              modAux :: a -> a -> a -> a -> a
    modAux a
    k a
    m a
    n a
    j | a
    n a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    > a
    j     = a -> a -> a
    forall a. Integral a => a -> a -> a
    mod (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    j a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    1) (a
    m a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1)
                             | Bool
    otherwise = a
    k a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    n

              ~(Just Term
    true)  = BuiltinEnv -> Maybe ConHead
    bTrue  BuiltinEnv
    bEnv Maybe ConHead -> (ConHead -> Term) -> Maybe Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ ConHead
    c -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ConOSystem []
              ~(Just Term
    false) = BuiltinEnv -> Maybe ConHead
    bFalse BuiltinEnv
    bEnv Maybe ConHead -> (ConHead -> Term) -> Maybe Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ ConHead
    c -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ConOSystem []

              bool :: Bool -> Term
    bool   Bool
    a = if Bool
    a then Term
    true else Term
    false
              nat :: Integer -> Term
    nat    Integer
    a = Literal -> Term
    Lit (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Literal
    LitNat    (Integer -> Term) -> Integer -> Term
    forall a b. (a -> b) -> a -> b
    $! Integer
    a
              word :: Word64 -> Term
    word   Word64
    a = Literal -> Term
    Lit (Literal -> Term) -> (Word64 -> Literal) -> Word64 -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Literal
    LitWord64 (Word64 -> Term) -> Word64 -> Term
    forall a b. (a -> b) -> a -> b
    $! Word64
    a
              float :: Double -> Term
    float  Double
    a = Literal -> Term
    Lit (Literal -> Term) -> (Double -> Literal) -> Double -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Double -> Literal
    LitFloat  (Double -> Term) -> Double -> Term
    forall a b. (a -> b) -> a -> b
    $! Double
    a
              text :: Text -> Term
    text   Text
    a = Literal -> Term
    Lit (Literal -> Term) -> (Text -> Literal) -> Text -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Literal
    LitString (Text -> Term) -> Text -> Term
    forall a b. (a -> b) -> a -> b
    $! Text
    a
              string :: VerboseKey -> Term
    string VerboseKey
    a = Text -> Term
    text (VerboseKey -> Text
    T.pack VerboseKey
    a)
              char :: Char -> Term
    char   Char
    a = Literal -> Term
    Lit (Literal -> Term) -> (Char -> Literal) -> Char -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Literal
    LitChar   (Char -> Term) -> Char -> Term
    forall a b. (a -> b) -> a -> b
    $! Char
    a

              -- Remember reverse order!
              natOp :: (Integer -> Integer -> Integer) -> [Literal] -> Term
    natOp Integer -> Integer -> Integer
    f [LitNat Integer
    a, LitNat Integer
    b] = Integer -> Term
    nat (Integer -> Integer -> Integer
    f Integer
    b Integer
    a)
              natOp Integer -> Integer -> Integer
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              natOp4 :: (Integer -> Integer -> Integer -> Integer -> Integer)
    -> [Literal] -> Term
    natOp4 Integer -> Integer -> Integer -> Integer -> Integer
    f [LitNat Integer
    a, LitNat Integer
    b, LitNat Integer
    c, LitNat Integer
    d] = Integer -> Term
    nat (Integer -> Integer -> Integer -> Integer -> Integer
    f Integer
    d Integer
    c Integer
    b Integer
    a)
              natOp4 Integer -> Integer -> Integer -> Integer -> Integer
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              natRel :: (Integer -> Integer -> Bool) -> [Literal] -> Term
    natRel Integer -> Integer -> Bool
    f [LitNat Integer
    a, LitNat Integer
    b] = Bool -> Term
    bool (Integer -> Integer -> Bool
    f Integer
    b Integer
    a)
              natRel Integer -> Integer -> Bool
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              floatFun :: (Double -> Double) -> [Literal] -> Term
    floatFun Double -> Double
    f [LitFloat Double
    a] = Double -> Term
    float (Double -> Double
    f Double
    a)
              floatFun Double -> Double
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              floatOp :: (Double -> Double -> Double) -> [Literal] -> Term
    floatOp Double -> Double -> Double
    f [LitFloat Double
    a, LitFloat Double
    b] = Double -> Term
    float (Double -> Double -> Double
    f Double
    b Double
    a)
              floatOp Double -> Double -> Double
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              floatPred :: (Double -> Bool) -> [Literal] -> Term
    floatPred Double -> Bool
    f [LitFloat Double
    a] = Bool -> Term
    bool (Double -> Bool
    f Double
    a)
              floatPred Double -> Bool
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              floatRel :: (Double -> Double -> Bool) -> [Literal] -> Term
    floatRel Double -> Double -> Bool
    f [LitFloat Double
    a, LitFloat Double
    b] = Bool -> Term
    bool (Double -> Double -> Bool
    f Double
    b Double
    a)
              floatRel Double -> Double -> Bool
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              charFun :: (Char -> Char) -> [Literal] -> Term
    charFun Char -> Char
    f [LitChar Char
    a] = Char -> Term
    char (Char -> Char
    f Char
    a)
              charFun Char -> Char
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              charPred :: (Char -> Bool) -> [Literal] -> Term
    charPred Char -> Bool
    f [LitChar Char
    a] = Bool -> Term
    bool (Char -> Bool
    f Char
    a)
              charPred Char -> Bool
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              charRel :: (Char -> Char -> Bool) -> [Literal] -> Term
    charRel Char -> Char -> Bool
    f [LitChar Char
    a, LitChar Char
    b] = Bool -> Term
    bool (Char -> Char -> Bool
    f Char
    b Char
    a)
              charRel Char -> Char -> Bool
    _ [Literal]
    _ = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      return $
        CompactDef { cdefNonterminating = defNonterminating def
                   , cdefUnconfirmed    = defTerminationUnconfirmed def
                   , cdefDef            = cdefn
                   , cdefRewriteRules   = if allowReduce then rewr else []
                   }

    -- Faster case trees ------------------------------------------------------

    data FastCase c = FBranches
      { forall c. FastCase c -> Bool
    fprojPatterns   :: Bool
        -- ^ We are constructing a record here (copatterns).
        --   'conBranches' lists projections.
      , forall c. FastCase c -> Map NameId c
    fconBranches    :: Map NameId c
        -- ^ Map from constructor (or projection) names to their arity
        --   and the case subtree.  (Projections have arity 0.)
      , forall c. FastCase c -> Maybe c
    fsucBranch      :: Maybe c
      , forall c. FastCase c -> Map Literal c
    flitBranches    :: Map Literal c
        -- ^ Map from literal to case subtree.
      , forall c. FastCase c -> Maybe c
    fcatchallBranch :: Maybe c
        -- ^ (Possibly additional) catch-all clause.
      , forall c. FastCase c -> Bool
    ffallThrough    :: Bool
        -- ^ (if True) In case of non-canonical argument use catchallBranch.
      }

    --UNUSED Liang-Ting Chen 2019-07-16
    --noBranches :: FastCase a
    --noBranches = FBranches{ fprojPatterns   = False
    --                      , fconBranches    = Map.empty
    --                      , fsucBranch      = Nothing
    --                      , flitBranches    = Map.empty
    --                      , fcatchallBranch = Nothing
    --                      , ffallThrough    = False }

    -- | Case tree with bodies.

    data FastCompiledClauses
      = FCase Int (FastCase FastCompiledClauses)
        -- ^ @Case n bs@ stands for a match on the @n@-th argument
        -- (counting from zero) with @bs@ as the case branches.
        -- If the @n@-th argument is a projection, we have only 'conBranches'
        -- with arity 0.
      | FEta Int [Arg QName] FastCompiledClauses (Maybe FastCompiledClauses)
        -- ^ Match on record constructor. Can still have a catch-all though. Just
        --   contains the fields, not the actual constructor.
      | FDone [Arg ArgName] Term
        -- ^ @Done xs b@ stands for the body @b@ where the @xs@ contains hiding
        --   and name suggestions for the free variables. This is needed to build
        --   lambdas on the right hand side for partial applications which can
        --   still reduce.
      | FFail
        -- ^ Absurd case.

    fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    bEnv CompiledClauses
    cc =
      case CompiledClauses
    cc of
        Fail{}            -> FastCompiledClauses
    FFail
        Done [Arg VerboseKey]
    xs Term
    b         -> [Arg VerboseKey] -> Term -> FastCompiledClauses
    FDone [Arg VerboseKey]
    xs Term
    b
        Case (Arg ArgInfo
    _ Int
    n) Branches{ etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch = Just (ConHead
    c, WithArity CompiledClauses
    cc), catchallBranch :: forall c. Case c -> Maybe c
    catchallBranch = Maybe CompiledClauses
    ca } ->
          Int
    -> [Arg QName]
    -> FastCompiledClauses
    -> Maybe FastCompiledClauses
    -> FastCompiledClauses
    FEta Int
    n (ConHead -> [Arg QName]
    conFields ConHead
    c) (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    bEnv (CompiledClauses -> FastCompiledClauses)
    -> CompiledClauses -> FastCompiledClauses
    forall a b. (a -> b) -> a -> b
    $ WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content WithArity CompiledClauses
    cc) (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    bEnv (CompiledClauses -> FastCompiledClauses)
    -> Maybe CompiledClauses -> Maybe FastCompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CompiledClauses
    ca)
        Case (Arg ArgInfo
    _ Int
    n) Case CompiledClauses
    bs -> Int -> FastCase FastCompiledClauses -> FastCompiledClauses
    FCase Int
    n (BuiltinEnv -> Case CompiledClauses -> FastCase FastCompiledClauses
    fastCase BuiltinEnv
    bEnv Case CompiledClauses
    bs)

    fastCase :: BuiltinEnv -> Case CompiledClauses -> FastCase FastCompiledClauses
    fastCase :: BuiltinEnv -> Case CompiledClauses -> FastCase FastCompiledClauses
    fastCase BuiltinEnv
    env (Branches Bool
    proj Map QName (WithArity CompiledClauses)
    con Maybe (ConHead, WithArity CompiledClauses)
    _ Map Literal CompiledClauses
    lit Maybe CompiledClauses
    wild Maybe Bool
    fT Bool
    _) =
      FBranches
        { fprojPatterns :: Bool
    fprojPatterns   = Bool
    proj
        , fconBranches :: Map NameId FastCompiledClauses
    fconBranches    = (QName -> NameId)
    -> Map QName FastCompiledClauses -> Map NameId FastCompiledClauses
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic (Name -> NameId
    nameId (Name -> NameId) -> (QName -> Name) -> QName -> NameId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName) (Map QName FastCompiledClauses -> Map NameId FastCompiledClauses)
    -> Map QName FastCompiledClauses -> Map NameId FastCompiledClauses
    forall a b. (a -> b) -> a -> b
    $ (WithArity CompiledClauses -> FastCompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    -> Map QName FastCompiledClauses
    forall a b. (a -> b) -> Map QName a -> Map QName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    env (CompiledClauses -> FastCompiledClauses)
    -> (WithArity CompiledClauses -> CompiledClauses)
    -> WithArity CompiledClauses
    -> FastCompiledClauses
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content) (Map QName (WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    stripSuc Map QName (WithArity CompiledClauses)
    con)
        , fsucBranch :: Maybe FastCompiledClauses
    fsucBranch      = (WithArity CompiledClauses -> FastCompiledClauses)
    -> Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    env (CompiledClauses -> FastCompiledClauses)
    -> (WithArity CompiledClauses -> CompiledClauses)
    -> WithArity CompiledClauses
    -> FastCompiledClauses
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content) (Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses)
    -> Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses
    forall a b. (a -> b) -> a -> b
    $ (QName
     -> Map QName (WithArity CompiledClauses)
     -> Maybe (WithArity CompiledClauses))
    -> Map QName (WithArity CompiledClauses)
    -> QName
    -> Maybe (WithArity CompiledClauses)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QName
    -> Map QName (WithArity CompiledClauses)
    -> Maybe (WithArity CompiledClauses)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Map QName (WithArity CompiledClauses)
    con (QName -> Maybe (WithArity CompiledClauses))
    -> (ConHead -> QName)
    -> ConHead
    -> Maybe (WithArity CompiledClauses)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName (ConHead -> Maybe (WithArity CompiledClauses))
    -> Maybe ConHead -> Maybe (WithArity CompiledClauses)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< BuiltinEnv -> Maybe ConHead
    bSuc BuiltinEnv
    env
        , flitBranches :: Map Literal FastCompiledClauses
    flitBranches    = (CompiledClauses -> FastCompiledClauses)
    -> Map Literal CompiledClauses -> Map Literal FastCompiledClauses
    forall a b. (a -> b) -> Map Literal a -> Map Literal b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    env) Map Literal CompiledClauses
    lit
        , ffallThrough :: Bool
    ffallThrough    = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe Bool
    fT
        , fcatchallBranch :: Maybe FastCompiledClauses
    fcatchallBranch = (CompiledClauses -> FastCompiledClauses)
    -> Maybe CompiledClauses -> Maybe FastCompiledClauses
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
    fastCompiledClauses BuiltinEnv
    env) Maybe CompiledClauses
    wild }
      where
        stripSuc :: Map QName (WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    stripSuc | Just ConHead
    c <- BuiltinEnv -> Maybe ConHead
    bSuc BuiltinEnv
    env = QName
    -> Map QName (WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete (ConHead -> QName
    conName ConHead
    c)
                 | Bool
    otherwise          = Map QName (WithArity CompiledClauses)
    -> Map QName (WithArity CompiledClauses)
    forall a. a -> a
    id

    {-# INLINE lookupCon #-}
    lookupCon :: QName -> FastCase c -> Maybe c
    lookupCon :: forall c. QName -> FastCase c -> Maybe c
    lookupCon QName
    c (FBranches Bool
    _ Map NameId c
    cons Maybe c
    _ Map Literal c
    _ Maybe c
    _ Bool
    _) = NameId -> Map NameId c -> Maybe c
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> NameId
    nameId (Name -> NameId) -> Name -> NameId
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    c) Map NameId c
    cons

    -- QName memo -------------------------------------------------------------

    {-# NOINLINE memoQName #-}
    memoQName :: (QName -> a) -> (QName -> a)
    memoQName :: forall a. (QName -> a) -> QName -> a
    memoQName QName -> a
    f = IO (QName -> a) -> QName -> a
    forall a. IO a -> a
    unsafePerformIO (IO (QName -> a) -> QName -> a) -> IO (QName -> a) -> QName -> a
    forall a b. (a -> b) -> a -> b
    $ do
      tbl <- Map NameId a -> IO (IORef (Map NameId a))
    forall a. a -> IO (IORef a)
    newIORef Map NameId a
    forall k a. Map k a
    Map.empty
      return (unsafePerformIO . f' tbl)
      where
        f' :: IORef (Map NameId a) -> QName -> IO a
    f' IORef (Map NameId a)
    tbl QName
    x = do
          let i :: NameId
    i = Name -> NameId
    nameId (QName -> Name
    qnameName QName
    x)
          m <- IORef (Map NameId a) -> IO (Map NameId a)
    forall a. IORef a -> IO a
    readIORef IORef (Map NameId a)
    tbl
          case Map.lookup i m of
            Just a
    y  -> a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    y
            Maybe a
    Nothing -> do
              let y :: a
    y = QName -> a
    f QName
    x
              IORef (Map NameId a) -> Map NameId a -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef (Map NameId a)
    tbl (NameId -> a -> Map NameId a -> Map NameId a
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert NameId
    i a
    y Map NameId a
    m)
              a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    y

    -- * Fast reduction

    data Normalisation = WHNF | NF
      deriving (Normalisation -> Normalisation -> Bool
    (Normalisation -> Normalisation -> Bool)
    -> (Normalisation -> Normalisation -> Bool) -> Eq Normalisation
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Normalisation -> Normalisation -> Bool
    == :: Normalisation -> Normalisation -> Bool
    $c/= :: Normalisation -> Normalisation -> Bool
    /= :: Normalisation -> Normalisation -> Bool
    Eq)

    -- | The entry point to the reduction machine.
    fastReduce :: Term -> ReduceM (Blocked Term)
    fastReduce :: Term -> ReduceM (Blocked Term)
    fastReduce = Normalisation -> Term -> ReduceM (Blocked Term)
    fastReduce' Normalisation
    WHNF

    fastNormalise :: Term -> ReduceM Term
    fastNormalise :: Term -> ReduceM Term
    fastNormalise Term
    v = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking (Blocked Term -> Term) -> ReduceM (Blocked Term) -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Normalisation -> Term -> ReduceM (Blocked Term)
    fastReduce' Normalisation
    NF Term
    v

    fastReduce' :: Normalisation -> Term -> ReduceM (Blocked Term)
    fastReduce' :: Normalisation -> Term -> ReduceM (Blocked Term)
    fastReduce' Normalisation
    norm Term
    v = do
      tcState <- ReduceM TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      let name (Con ConHead
    c ConInfo
    _ Elims
    _) = ConHead
    c
          name Term
    _         = ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- Gather builtins using 'BuiltinAccess' rather than with the default
          -- 'HasBuiltins ReduceM' instance. This increases laziness, allowing us to
          -- avoid costly builtin lookups unless needed.
          builtinName   = (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> (BuiltinId -> Maybe Term) -> BuiltinId -> Maybe ConHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> BuiltinAccess (Maybe Term) -> Maybe Term
    forall a. TCState -> BuiltinAccess a -> a
    runBuiltinAccess TCState
    tcState (BuiltinAccess (Maybe Term) -> Maybe Term)
    -> (BuiltinId -> BuiltinAccess (Maybe Term))
    -> BuiltinId
    -> Maybe Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BuiltinId -> BuiltinAccess (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin'
          primitiveName = (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap PrimFun -> QName
    primFunName (Maybe PrimFun -> Maybe QName)
    -> (PrimitiveId -> Maybe PrimFun) -> PrimitiveId -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> BuiltinAccess (Maybe PrimFun) -> Maybe PrimFun
    forall a. TCState -> BuiltinAccess a -> a
    runBuiltinAccess TCState
    tcState (BuiltinAccess (Maybe PrimFun) -> Maybe PrimFun)
    -> (PrimitiveId -> BuiltinAccess (Maybe PrimFun))
    -> PrimitiveId
    -> Maybe PrimFun
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimitiveId -> BuiltinAccess (Maybe PrimFun)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe PrimFun)
    getPrimitive'

          zero  = BuiltinId -> Maybe ConHead
    builtinName BuiltinId
    builtinZero
          suc   = BuiltinId -> Maybe ConHead
    builtinName BuiltinId
    builtinSuc
          true  = BuiltinId -> Maybe ConHead
    builtinName BuiltinId
    builtinTrue
          false = BuiltinId -> Maybe ConHead
    builtinName BuiltinId
    builtinFalse
          refl  = BuiltinId -> Maybe ConHead
    builtinName BuiltinId
    builtinRefl

          force = PrimitiveId -> Maybe QName
    primitiveName PrimitiveId
    PrimForce
          erase = PrimitiveId -> Maybe QName
    primitiveName PrimitiveId
    PrimErase

          bEnv = BuiltinEnv { bZero :: Maybe ConHead
    bZero = Maybe ConHead
    zero, bSuc :: Maybe ConHead
    bSuc = Maybe ConHead
    suc, bTrue :: Maybe ConHead
    bTrue = Maybe ConHead
    true, bFalse :: Maybe ConHead
    bFalse = Maybe ConHead
    false, bRefl :: Maybe ConHead
    bRefl = Maybe ConHead
    refl,
                              bPrimForce :: Maybe QName
    bPrimForce = Maybe QName
    force, bPrimErase :: Maybe QName
    bPrimErase = Maybe QName
    erase }
      allowedReductions <- asksTC envAllowedReductions
      rwr <- optRewriting <$> pragmaOptions
      constInfo <- unKleisli $ \QName
    f -> do
        info <- QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
        rewr <- if rwr then instantiateRewriteRules =<< getRewriteRulesFor f
                       else return []
        compactDef bEnv info rewr
      ReduceM $ \ ReduceEnv
    redEnv -> ReduceEnv
    -> BuiltinEnv
    -> (QName -> CompactDef)
    -> Normalisation
    -> Term
    -> Blocked Term
    reduceTm ReduceEnv
    redEnv BuiltinEnv
    bEnv ((QName -> CompactDef) -> QName -> CompactDef
    forall a. (QName -> a) -> QName -> a
    memoQName QName -> CompactDef
    constInfo) Normalisation
    norm Term
    v

    -- * Closures

    -- | The abstract machine represents terms as closures containing a 'Term', an environment, and a
    --   spine of eliminations. Note that the environment doesn't necessarily bind all variables in the
    --   term. The variables in the context in which the abstract machine is started are free in
    --   closures. The 'IsValue' argument tracks whether the closure is in weak-head normal form.
    data Closure s = Closure IsValue Term (Env s) (Spine s)
                     -- ^ The environment applies to the 'Term' argument. The spine contains closures
                     --   with their own environments.

    -- | Used to track if a closure is @Unevaluated@ or a @Value@ (in weak-head normal form), and if so
    --   why it cannot reduce further.
    data IsValue = Value Blocked_ | Unevaled

    -- | The spine is a list of eliminations. Application eliminations contain pointers.
    type Spine s = [Elim' (Pointer s)]

    isValue :: Closure s -> IsValue
    isValue :: forall s. Closure s -> IsValue
    isValue (Closure IsValue
    isV Term
    _ Env s
    _ Spine s
    _) = IsValue
    isV

    setIsValue :: IsValue -> Closure s -> Closure s
    setIsValue :: forall s. IsValue -> Closure s -> Closure s
    setIsValue IsValue
    isV (Closure IsValue
    _ Term
    t Env s
    env Spine s
    spine) = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    isV Term
    t Env s
    env Spine s
    spine

    -- | Apply a closure to a spine of eliminations. Note that this does not preserve the 'IsValue'
    --   field.
    clApply :: Closure s -> Spine s -> Closure s
    clApply :: forall s. Closure s -> Spine s -> Closure s
    clApply Closure s
    c [] = Closure s
    c
    clApply (Closure IsValue
    _ Term
    t Env s
    env Spine s
    es) Spine s
    es' = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled Term
    t Env s
    env (Spine s
    es Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    es')

    -- | Apply a closure to a spine, preserving the 'IsValue' field. Use with care, since usually
    --   eliminations do not preserve the value status.
    clApply_ :: Closure s -> Spine s -> Closure s
    clApply_ :: forall s. Closure s -> Spine s -> Closure s
    clApply_ Closure s
    c [] = Closure s
    c
    clApply_ (Closure IsValue
    b Term
    t Env s
    env Spine s
    es) Spine s
    es' = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    b Term
    t Env s
    env (Spine s
    es Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    es')

    -- * Pointers and thunks

    -- | Spines and environments contain pointers to closures to enable call-by-need evaluation.
    data Pointer s = Pure (Closure s)
                     -- ^ Not a pointer. Used for closures that do not need to be shared to avoid
                     --   unnecessary updates.
                   | Pointer {-# UNPACK #-} !(STPointer s)
                     -- ^ An actual pointer is an 'STRef' to a 'Thunk'. The thunk is set to 'BlackHole'
                     --   during the evaluation of its contents to make debugging loops easier.

    type STPointer s = STRef s (Thunk (Closure s))

    -- | A thunk is either a black hole or contains a value.
    data Thunk a = BlackHole | Thunk a
      deriving ((forall a b. (a -> b) -> Thunk a -> Thunk b)
    -> (forall a b. a -> Thunk b -> Thunk a) -> Functor Thunk
    forall a b. a -> Thunk b -> Thunk a
    forall a b. (a -> b) -> Thunk a -> Thunk b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Thunk a -> Thunk b
    fmap :: forall a b. (a -> b) -> Thunk a -> Thunk b
    $c<$ :: forall a b. a -> Thunk b -> Thunk a
    <$ :: forall a b. a -> Thunk b -> Thunk a
    Functor)

    derefPointer :: Pointer s -> ST s (Thunk (Closure s))
    derefPointer :: forall s. Pointer s -> ST s (Thunk (Closure s))
    derefPointer (Pure Closure s
    x)      = Thunk (Closure s) -> ST s (Thunk (Closure s))
    forall a. a -> ST s a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Closure s -> Thunk (Closure s)
    forall a. a -> Thunk a
    Thunk Closure s
    x)
    derefPointer (Pointer STPointer s
    ptr) = STPointer s -> ST s (Thunk (Closure s))
    forall s a. STRef s a -> ST s a
    readSTRef STPointer s
    ptr

    -- | In most cases pointers that we dereference do not contain black holes.
    derefPointer_ :: Pointer s -> ST s (Closure s)
    derefPointer_ :: forall s. Pointer s -> ST s (Closure s)
    derefPointer_ Pointer s
    ptr =
      Pointer s -> ST s (Thunk (Closure s))
    forall s. Pointer s -> ST s (Thunk (Closure s))
    derefPointer Pointer s
    ptr ST s (Thunk (Closure s))
    -> (Thunk (Closure s) -> Closure s) -> ST s (Closure s)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        Thunk Closure s
    cl  -> Closure s
    cl
        Thunk (Closure s)
    BlackHole -> Closure s
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Only use for debug printing!
    unsafeDerefPointer :: Pointer s -> Thunk (Closure s)
    unsafeDerefPointer :: forall s. Pointer s -> Thunk (Closure s)
    unsafeDerefPointer (Pure Closure s
    x)    = Closure s -> Thunk (Closure s)
    forall a. a -> Thunk a
    Thunk Closure s
    x
    unsafeDerefPointer (Pointer STPointer s
    p) = IO (Thunk (Closure s)) -> Thunk (Closure s)
    forall a. IO a -> a
    unsafePerformIO (ST s (Thunk (Closure s)) -> IO (Thunk (Closure s))
    forall s a. ST s a -> IO a
    unsafeSTToIO (STPointer s -> ST s (Thunk (Closure s))
    forall s a. STRef s a -> ST s a
    readSTRef STPointer s
    p))

    readPointer :: STPointer s -> ST s (Thunk (Closure s))
    readPointer :: forall s. STPointer s -> ST s (Thunk (Closure s))
    readPointer = STRef s (Thunk (Closure s)) -> ST s (Thunk (Closure s))
    forall s a. STRef s a -> ST s a
    readSTRef

    storePointer :: STPointer s -> Closure s -> ST s ()
    storePointer :: forall s. STPointer s -> Closure s -> ST s ()
    storePointer STPointer s
    ptr !Closure s
    cl = STPointer s -> Thunk (Closure s) -> ST s ()
    forall s a. STRef s a -> a -> ST s ()
    writeSTRef STPointer s
    ptr (Closure s -> Thunk (Closure s)
    forall a. a -> Thunk a
    Thunk Closure s
    cl)
        -- Note the strict match. To prevent leaking memory in case of unnecessary updates.

    blackHole :: STPointer s -> ST s ()
    blackHole :: forall s. STPointer s -> ST s ()
    blackHole STPointer s
    ptr = STPointer s -> Thunk (Closure s) -> ST s ()
    forall s a. STRef s a -> a -> ST s ()
    writeSTRef STPointer s
    ptr Thunk (Closure s)
    forall a. Thunk a
    BlackHole

    -- | Create a thunk. If the closure is a naked variable we can reuse the pointer from the
    --   environment to avoid creating long pointer chains.
    createThunk :: Closure s -> ST s (Pointer s)
    createThunk :: forall s. Closure s -> ST s (Pointer s)
    createThunk (Closure IsValue
    _ (Var Int
    x []) Env s
    env Spine s
    spine)
      | Spine s -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Spine s
    spine, Just Pointer s
    p <- Int -> Env s -> Maybe (Pointer s)
    forall s. Int -> Env s -> Maybe (Pointer s)
    lookupEnv Int
    x Env s
    env = Pointer s -> ST s (Pointer s)
    forall a. a -> ST s a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pointer s
    p
    createThunk Closure s
    cl = STPointer s -> Pointer s
    forall s. STPointer s -> Pointer s
    Pointer (STPointer s -> Pointer s)
    -> ST s (STPointer s) -> ST s (Pointer s)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Thunk (Closure s) -> ST s (STPointer s)
    forall a s. a -> ST s (STRef s a)
    newSTRef (Closure s -> Thunk (Closure s)
    forall a. a -> Thunk a
    Thunk Closure s
    cl)

    -- | Create a thunk that is not shared or updated.
    pureThunk :: Closure s -> Pointer s
    pureThunk :: forall s. Closure s -> Pointer s
    pureThunk = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    Pure

    -- * Environments

    -- | The environment of a closure binds pointers to deBruijn indicies.
    newtype Env s = Env [Pointer s]

    emptyEnv :: Env s
    emptyEnv :: forall s. Env s
    emptyEnv = [Pointer s] -> Env s
    forall s. [Pointer s] -> Env s
    Env []
    --UNUSED Liang-Ting Chen 2019-07-16
    --isEmptyEnv :: Env s -> Bool
    --isEmptyEnv (Env xs) = null xs

    envSize :: Env s -> Int
    envSize :: forall s. Env s -> Int
    envSize (Env [Pointer s]
    xs) = [Pointer s] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Pointer s]
    xs

    envToList :: Env s -> [Pointer s]
    envToList :: forall s. Env s -> [Pointer s]
    envToList (Env [Pointer s]
    xs) = [Pointer s]
    xs

    extendEnv :: Pointer s -> Env s -> Env s
    extendEnv :: forall s. Pointer s -> Env s -> Env s
    extendEnv Pointer s
    p (Env [Pointer s]
    xs) = [Pointer s] -> Env s
    forall s. [Pointer s] -> Env s
    Env (Pointer s
    p Pointer s -> [Pointer s] -> [Pointer s]
    forall a. a -> [a] -> [a]
    : [Pointer s]
    xs)

    -- | Unsafe.
    lookupEnv_ :: Int -> Env s -> Pointer s
    lookupEnv_ :: forall s. Int -> Env s -> Pointer s
    lookupEnv_ Int
    i (Env [Pointer s]
    e) = Pointer s -> [Pointer s] -> Int -> Pointer s
    forall a. a -> [a] -> Int -> a
    indexWithDefault Pointer s
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Pointer s]
    e Int
    i

    -- Andreas, 2018-11-12, which isn't this just Agda.Utils.List.!!! ?
    lookupEnv :: Int -> Env s -> Maybe (Pointer s)
    lookupEnv :: forall s. Int -> Env s -> Maybe (Pointer s)
    lookupEnv Int
    i Env s
    e | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n     = Pointer s -> Maybe (Pointer s)
    forall a. a -> Maybe a
    Just (Int -> Env s -> Pointer s
    forall s. Int -> Env s -> Pointer s
    lookupEnv_ Int
    i Env s
    e)
                  | Bool
    otherwise = Maybe (Pointer s)
    forall a. Maybe a
    Nothing
      where n :: Int
    n = Env s -> Int
    forall s. Env s -> Int
    envSize Env s
    e

    -- * The Agda Abstract Machine

    -- | The abstract machine state has two states 'Eval' and 'Match' that determine what the machine is
    --   currently working on: evaluating a closure in the Eval state and matching a spine against a
    --   case tree in the Match state. Both states contain a 'ControlStack' of continuations for what to
    --   do next. The heap is maintained implicitly using 'STRef's, hence the @s@ parameter.
    data AM s = Eval (Closure s) !(ControlStack s)
                -- ^ Evaluate the given closure (the focus) to weak-head normal form. If the 'IsValue'
                --   field of the closure is 'Value' we look at the control stack for what to do. Being
                --   strict in the control stack is important! We can spend a lot of steps with
                --   unevaluated closures (where we update, but don't look at the control stack). For
                --   instance, long chains of 'suc' constructors.
              | Match QName FastCompiledClauses (Spine s) (MatchStack s) (ControlStack s)
                -- ^ @Match f cc spine stack ctrl@ Match the arguments @spine@ against the case tree
                --   @cc@. The match stack contains a (possibly empty) list of 'Catchall' frames and a
                --   closure to return in case of a stuck match.

    -- | The control stack contains a list of continuations, i.e. what to do with
    --   the result of the current focus.
    type ControlStack s = [ControlFrame s]

    -- | The control stack for matching. Contains a list of CatchallFrame's and the closure to return in
    --   case of a stuck match.
    data MatchStack s = [CatchallFrame s] :> Closure s
    infixr 2 :>, >:

    (>:) :: CatchallFrame s -> MatchStack s -> MatchStack s
    >: :: forall s. CatchallFrame s -> MatchStack s -> MatchStack s
    (>:) CatchallFrame s
    c ([CatchallFrame s]
    cs :> Closure s
    cl) = CatchallFrame s
    c CatchallFrame s -> [CatchallFrame s] -> [CatchallFrame s]
    forall a. a -> [a] -> [a]
    : [CatchallFrame s]
    cs [CatchallFrame s] -> Closure s -> MatchStack s
    forall s. [CatchallFrame s] -> Closure s -> MatchStack s
    :> Closure s
    cl
    -- Previously written as:
    --   c >: cs :> cl = c : cs :> cl
    --
    -- However, some versions/tools fail to parse infix data constructors properly.
    -- For example, stylish-haskell@0.9.2.1 fails with the following error:
    --   Language.Haskell.Stylish.Parse.parseModule: could not parse
    --   src/full/Agda/TypeChecking/Reduce/Fast.hs: ParseFailed (SrcLoc
    --   "<unknown>.hs" 625 1) "Parse error in pattern: "
    --
    -- See https://ghc.haskell.org/trac/ghc/ticket/10018 which may be related.

    data CatchallFrame s = Catchall FastCompiledClauses (Spine s)
                            -- ^ @Catchall cc spine@. Case trees are not fully expanded, that is,
                            --   inner matches can be partial and covered by a catch-all at a higher
                            --   level. This catch-all is represented on the match stack as a
                            --   @Catchall@. @cc@ is the case tree in the catch-all case and @spine@ is
                            --   the value of the pattern variables at the point of the catch-all.

    -- An Elim' with a hole.
    data ElimZipper a = ApplyCxt ArgInfo
                      | IApplyType a a | IApplyFst a a | IApplySnd a a
      deriving (ElimZipper a -> ElimZipper a -> Bool
    (ElimZipper a -> ElimZipper a -> Bool)
    -> (ElimZipper a -> ElimZipper a -> Bool) -> Eq (ElimZipper a)
    forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
    == :: ElimZipper a -> ElimZipper a -> Bool
    $c/= :: forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
    /= :: ElimZipper a -> ElimZipper a -> Bool
    Eq, Eq (ElimZipper a)
    Eq (ElimZipper a) =>
    (ElimZipper a -> ElimZipper a -> Ordering)
    -> (ElimZipper a -> ElimZipper a -> Bool)
    -> (ElimZipper a -> ElimZipper a -> Bool)
    -> (ElimZipper a -> ElimZipper a -> Bool)
    -> (ElimZipper a -> ElimZipper a -> Bool)
    -> (ElimZipper a -> ElimZipper a -> ElimZipper a)
    -> (ElimZipper a -> ElimZipper a -> ElimZipper a)
    -> Ord (ElimZipper a)
    ElimZipper a -> ElimZipper a -> Bool
    ElimZipper a -> ElimZipper a -> Ordering
    ElimZipper a -> ElimZipper a -> ElimZipper a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall a. Ord a => Eq (ElimZipper a)
    forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    forall a. Ord a => ElimZipper a -> ElimZipper a -> Ordering
    forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
    $ccompare :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Ordering
    compare :: ElimZipper a -> ElimZipper a -> Ordering
    $c< :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    < :: ElimZipper a -> ElimZipper a -> Bool
    $c<= :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    <= :: ElimZipper a -> ElimZipper a -> Bool
    $c> :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    > :: ElimZipper a -> ElimZipper a -> Bool
    $c>= :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    >= :: ElimZipper a -> ElimZipper a -> Bool
    $cmax :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
    max :: ElimZipper a -> ElimZipper a -> ElimZipper a
    $cmin :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
    min :: ElimZipper a -> ElimZipper a -> ElimZipper a
    Ord, Int -> ElimZipper a -> ShowS
    [ElimZipper a] -> ShowS
    ElimZipper a -> VerboseKey
    (Int -> ElimZipper a -> ShowS)
    -> (ElimZipper a -> VerboseKey)
    -> ([ElimZipper a] -> ShowS)
    -> Show (ElimZipper a)
    forall a. Show a => Int -> ElimZipper a -> ShowS
    forall a. Show a => [ElimZipper a] -> ShowS
    forall a. Show a => ElimZipper a -> VerboseKey
    forall a.
    (Int -> a -> ShowS)
    -> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> ElimZipper a -> ShowS
    showsPrec :: Int -> ElimZipper a -> ShowS
    $cshow :: forall a. Show a => ElimZipper a -> VerboseKey
    show :: ElimZipper a -> VerboseKey
    $cshowList :: forall a. Show a => [ElimZipper a] -> ShowS
    showList :: [ElimZipper a] -> ShowS
    Show, (forall a b. (a -> b) -> ElimZipper a -> ElimZipper b)
    -> (forall a b. a -> ElimZipper b -> ElimZipper a)
    -> Functor ElimZipper
    forall a b. a -> ElimZipper b -> ElimZipper a
    forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
    fmap :: forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
    $c<$ :: forall a b. a -> ElimZipper b -> ElimZipper a
    <$ :: forall a b. a -> ElimZipper b -> ElimZipper a
    Functor, (forall m. Monoid m => ElimZipper m -> m)
    -> (forall m a. Monoid m => (a -> m) -> ElimZipper a -> m)
    -> (forall m a. Monoid m => (a -> m) -> ElimZipper a -> m)
    -> (forall a b. (a -> b -> b) -> b -> ElimZipper a -> b)
    -> (forall a b. (a -> b -> b) -> b -> ElimZipper a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ElimZipper a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ElimZipper a -> b)
    -> (forall a. (a -> a -> a) -> ElimZipper a -> a)
    -> (forall a. (a -> a -> a) -> ElimZipper a -> a)
    -> (forall a. ElimZipper a -> [a])
    -> (forall a. ElimZipper a -> Bool)
    -> (forall a. ElimZipper a -> Int)
    -> (forall a. Eq a => a -> ElimZipper a -> Bool)
    -> (forall a. Ord a => ElimZipper a -> a)
    -> (forall a. Ord a => ElimZipper a -> a)
    -> (forall a. Num a => ElimZipper a -> a)
    -> (forall a. Num a => ElimZipper a -> a)
    -> Foldable ElimZipper
    forall a. Eq a => a -> ElimZipper a -> Bool
    forall a. Num a => ElimZipper a -> a
    forall a. Ord a => ElimZipper a -> a
    forall m. Monoid m => ElimZipper m -> m
    forall a. ElimZipper a -> Bool
    forall a. ElimZipper a -> Int
    forall a. ElimZipper a -> [a]
    forall a. (a -> a -> a) -> ElimZipper a -> a
    forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
    forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => ElimZipper m -> m
    fold :: forall m. Monoid m => ElimZipper m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    foldr1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    foldl1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    $ctoList :: forall a. ElimZipper a -> [a]
    toList :: forall a. ElimZipper a -> [a]
    $cnull :: forall a. ElimZipper a -> Bool
    null :: forall a. ElimZipper a -> Bool
    $clength :: forall a. ElimZipper a -> Int
    length :: forall a. ElimZipper a -> Int
    $celem :: forall a. Eq a => a -> ElimZipper a -> Bool
    elem :: forall a. Eq a => a -> ElimZipper a -> Bool
    $cmaximum :: forall a. Ord a => ElimZipper a -> a
    maximum :: forall a. Ord a => ElimZipper a -> a
    $cminimum :: forall a. Ord a => ElimZipper a -> a
    minimum :: forall a. Ord a => ElimZipper a -> a
    $csum :: forall a. Num a => ElimZipper a -> a
    sum :: forall a. Num a => ElimZipper a -> a
    $cproduct :: forall a. Num a => ElimZipper a -> a
    product :: forall a. Num a => ElimZipper a -> a
    Foldable, Functor ElimZipper
    Foldable ElimZipper
    (Functor ElimZipper, Foldable ElimZipper) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> ElimZipper a -> f (ElimZipper b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        ElimZipper (f a) -> f (ElimZipper a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> ElimZipper a -> m (ElimZipper b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        ElimZipper (m a) -> m (ElimZipper a))
    -> Traversable ElimZipper
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    ElimZipper (m a) -> m (ElimZipper a)
    forall (f :: * -> *) a.
    Applicative f =>
    ElimZipper (f a) -> f (ElimZipper a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ElimZipper a -> m (ElimZipper b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ElimZipper a -> f (ElimZipper b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ElimZipper a -> f (ElimZipper b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ElimZipper a -> f (ElimZipper b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ElimZipper (f a) -> f (ElimZipper a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ElimZipper (f a) -> f (ElimZipper a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ElimZipper a -> m (ElimZipper b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ElimZipper a -> m (ElimZipper b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    ElimZipper (m a) -> m (ElimZipper a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    ElimZipper (m a) -> m (ElimZipper a)
    Traversable)

    instance Zipper (ElimZipper a) where
      type Carrier (ElimZipper a) = Elim' a
      type Element (ElimZipper a) = a

      firstHole :: Carrier (ElimZipper a)
    -> Maybe (Element (ElimZipper a), ElimZipper a)
    firstHole (Apply Arg a
    arg)    = (a, ElimZipper a) -> Maybe (a, ElimZipper a)
    forall a. a -> Maybe a
    Just (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    arg, ArgInfo -> ElimZipper a
    forall a. ArgInfo -> ElimZipper a
    ApplyCxt (Arg a -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg a
    arg))
      firstHole (IApply a
    a a
    x a
    y) = (a, ElimZipper a) -> Maybe (a, ElimZipper a)
    forall a. a -> Maybe a
    Just (a
    a, a -> a -> ElimZipper a
    forall a. a -> a -> ElimZipper a
    IApplyType a
    x a
    y)
      firstHole Proj{}         = Maybe (a, ElimZipper a)
    Maybe (Element (ElimZipper a), ElimZipper a)
    forall a. Maybe a
    Nothing

      plugHole :: Element (ElimZipper a) -> ElimZipper a -> Carrier (ElimZipper a)
    plugHole Element (ElimZipper a)
    x (ApplyCxt ArgInfo
    i)     = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i a
    Element (ElimZipper a)
    x)
      plugHole Element (ElimZipper a)
    a (IApplyType a
    x a
    y) = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    Element (ElimZipper a)
    a a
    x a
    y
      plugHole Element (ElimZipper a)
    x (IApplyFst a
    a a
    y)  = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    a a
    Element (ElimZipper a)
    x a
    y
      plugHole Element (ElimZipper a)
    y (IApplySnd a
    a a
    x)  = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    a a
    x a
    Element (ElimZipper a)
    y

      nextHole :: Element (ElimZipper a)
    -> ElimZipper a
    -> Either
         (Carrier (ElimZipper a)) (Element (ElimZipper a), ElimZipper a)
    nextHole Element (ElimZipper a)
    a (IApplyType a
    x a
    y) = (a, ElimZipper a) -> Either (Elim' a) (a, ElimZipper a)
    forall a b. b -> Either a b
    Right (a
    x, a -> a -> ElimZipper a
    forall a. a -> a -> ElimZipper a
    IApplyFst a
    Element (ElimZipper a)
    a a
    y)
      nextHole Element (ElimZipper a)
    x (IApplyFst a
    a a
    y)  = (a, ElimZipper a) -> Either (Elim' a) (a, ElimZipper a)
    forall a b. b -> Either a b
    Right (a
    y, a -> a -> ElimZipper a
    forall a. a -> a -> ElimZipper a
    IApplySnd a
    a a
    Element (ElimZipper a)
    x)
      nextHole Element (ElimZipper a)
    y (IApplySnd a
    a a
    x)  = Elim' a -> Either (Elim' a) (a, ElimZipper a)
    forall a b. a -> Either a b
    Left (a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    a a
    x a
    Element (ElimZipper a)
    y)
      nextHole Element (ElimZipper a)
    x c :: ElimZipper a
    c@ApplyCxt{}     = Elim' a -> Either (Elim' a) (a, ElimZipper a)
    forall a b. a -> Either a b
    Left (Element (ElimZipper a) -> ElimZipper a -> Carrier (ElimZipper a)
    forall z. Zipper z => Element z -> z -> Carrier z
    plugHole Element (ElimZipper a)
    x ElimZipper a
    c)

    -- | A spine with a single hole for a pointer.
    type SpineContext s = ComposeZipper (ListZipper (Elim' (Pointer s)))
                                        (ElimZipper (Pointer s))

    -- | Control frames are continuations that act on value closures.
    data ControlFrame s = CaseK QName ArgInfo (FastCase FastCompiledClauses) (Spine s) (Spine s) (MatchStack s)
                            -- ^ @CaseK f i bs spine0 spine1 stack@. Pattern match on the focus (with
                            --   arg info @i@) using the @bs@ case tree. @f@ is the name of the function
                            --   doing the matching, and @spine0@ and @spine1@ are the values bound to
                            --   the pattern variables to the left and right (respectively) of the
                            --   focus. The match stack contains catch-all cases we need to consider if
                            --   this match fails.
                        | ArgK (Closure s) (SpineContext s)
                            -- ^ @ArgK cl cxt@. Used when computing full normal forms. The closure is
                            --   the head and the context is the spine with the current focus removed.
                        | NormaliseK
                            -- ^ Indicates that the focus should be evaluated to full normal form.
                        | ForceK QName (Spine s) (Spine s)
                            -- ^ @ForceK f spine0 spine1@. Evaluating @primForce@ of the focus. @f@ is
                            --   the name of @primForce@ and is used to build the result if evaluation
                            --   gets stuck. @spine0@ are the level and type arguments and @spine1@
                            --   contains (if not empty) the continuation and any additional
                            --   eliminations.
                        | EraseK QName (Spine s) (Spine s) (Spine s) (Spine s)
                            -- ^ @EraseK f spine0 spine1 spine2 spine3@. Evaluating @primErase@. The
                            --   first contains the level and type arguments. @spine1@ and @spine2@
                            --   contain at most one argument between them. If in @spine1@ it's the
                            --   value closure of the first argument to be compared and if in @spine2@
                            --   it's the unevaluated closure of the second argument.
                            --   @spine3@ contains the proof of equality we are erasing. It is passed
                            --   around but never actually inspected.
                        | NatSucK Integer
                            -- ^ @NatSucK n@. Add @n@ to the focus. If the focus computes to a natural
                            --   number literal this returns a new literal, otherwise it constructs @n@
                            --   calls to @suc@.
                        | PrimOpK QName ([Literal] -> Term) [Literal] [Pointer s] (Maybe FastCompiledClauses)
                            -- ^ @PrimOpK f op lits es cc@. Evaluate the primitive function @f@ using
                            --   the Haskell function @op@. @op@ gets a list of literal values in
                            --   reverse order for the arguments of @f@ and computes the result as a
                            --   term. The already computed arguments (in reverse order) are @lits@ and
                            --   @es@ are the arguments that should be computed after the current focus.
                            --   In case of built-in functions with corresponding Agda implementations,
                            --   @cc@ contains the case tree.
                        | UpdateThunk [STPointer s]
                            -- ^ @UpdateThunk ps@. Update the pointers @ps@ with the value of the
                            --   current focus.
                        | ApplyK (Spine s)
                            -- ^ @ApplyK spine@. Apply the current focus to the eliminations in @spine@.
                            --   This is used when a thunk needs to be updated with a partial
                            --   application of a function.

    -- * Compilation and decoding

    -- | The initial abstract machine state. Wrap the term to be evaluated in an empty closure. Note
    --   that free variables of the term are treated as constants by the abstract machine. If computing
    --   full normal form we start off the control stack with a 'NormaliseK' continuation.
    compile :: Normalisation -> Term -> AM s
    compile :: forall s. Normalisation -> Term -> AM s
    compile Normalisation
    nf Term
    t = Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled Term
    t Env s
    forall s. Env s
    emptyEnv []) [ControlFrame s
    forall s. ControlFrame s
    NormaliseK | Normalisation
    nf Normalisation -> Normalisation -> Bool
    forall a. Eq a => a -> a -> Bool
    == Normalisation
    NF]

    decodePointer :: Pointer s -> ST s Term
    decodePointer :: forall s. Pointer s -> ST s Term
    decodePointer Pointer s
    p = Closure s -> ST s Term
    forall s. Closure s -> ST s Term
    decodeClosure_ (Closure s -> ST s Term) -> ST s (Closure s) -> ST s Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Pointer s -> ST s (Closure s)
    forall s. Pointer s -> ST s (Closure s)
    derefPointer_ Pointer s
    p

    -- | Note: it's important to be lazy in the spine and environment when decoding. Hence the
    --   'unsafeInterleaveST' here and in 'decodeEnv', and the special version of 'parallelS' in
    --   'decodeClosure'.
    decodeSpine :: Spine s -> ST s Elims
    decodeSpine :: forall s. Spine s -> ST s Elims
    decodeSpine Spine s
    spine = ST s Elims -> ST s Elims
    forall s a. ST s a -> ST s a
    unsafeInterleaveST (ST s Elims -> ST s Elims) -> ST s Elims -> ST s Elims
    forall a b. (a -> b) -> a -> b
    $ ((Elim' (Pointer s) -> ST s Elim) -> Spine s -> ST s Elims
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Elim' (Pointer s) -> ST s Elim) -> Spine s -> ST s Elims)
    -> ((Pointer s -> ST s Term) -> Elim' (Pointer s) -> ST s Elim)
    -> (Pointer s -> ST s Term)
    -> Spine s
    -> ST s Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pointer s -> ST s Term) -> Elim' (Pointer s) -> ST s Elim
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse) Pointer s -> ST s Term
    forall s. Pointer s -> ST s Term
    decodePointer Spine s
    spine

    decodeEnv :: Env s -> ST s [Term]
    decodeEnv :: forall s. Env s -> ST s [Term]
    decodeEnv Env s
    env = ST s [Term] -> ST s [Term]
    forall s a. ST s a -> ST s a
    unsafeInterleaveST (ST s [Term] -> ST s [Term]) -> ST s [Term] -> ST s [Term]
    forall a b. (a -> b) -> a -> b
    $ (Pointer s -> ST s Term) -> [Pointer s] -> ST s [Term]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Pointer s -> ST s Term
    forall s. Pointer s -> ST s Term
    decodePointer (Env s -> [Pointer s]
    forall s. Env s -> [Pointer s]
    envToList Env s
    env)

    decodeClosure_ :: Closure s -> ST s Term
    decodeClosure_ :: forall s. Closure s -> ST s Term
    decodeClosure_ = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking (Blocked Term -> Term)
    -> (Closure s -> ST s (Blocked Term)) -> Closure s -> ST s Term
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Closure s -> ST s (Blocked Term)
    forall s. Closure s -> ST s (Blocked Term)
    decodeClosure

    -- | Turning an abstract machine closure back into a term. This happens in three cases:
    --    * when reduction is finished and we return the weak-head normal term to the outside world.
    --    * when the abstract machine encounters something it cannot handle and falls back to the slow
    --      reduction engine
    --    * when there are rewrite rules to apply
    decodeClosure :: Closure s -> ST s (Blocked Term)
    decodeClosure :: forall s. Closure s -> ST s (Blocked Term)
    decodeClosure (Closure IsValue
    isV Term
    t Env s
    env Spine s
    spine) = do
        vs <- Env s -> ST s [Term]
    forall s. Env s -> ST s [Term]
    decodeEnv Env s
    env
        es <- decodeSpine spine
        return $ applyE (applySubst (parS vs) t) es <$ b
      where
        parS :: [a] -> Substitution' a
    parS = (a -> Substitution' a -> Substitution' a)
    -> Substitution' a -> [a] -> Substitution' a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    (:#) Substitution' a
    forall a. Substitution' a
    IdS  -- parallelS is too strict
        b :: Blocked_
    b    = case IsValue
    isV of
                 Value Blocked_
    b  -> Blocked_
    b
                 IsValue
    Unevaled -> () -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()  -- only when falling back to slow reduce in which case the
                                            -- blocking tag is immediately discarded

    -- | Turn a list of internal syntax eliminations into a spine. This builds closures and allocates
    --   thunks for all the 'Apply' elims.
    elimsToSpine :: Env s -> Elims -> ST s (Spine s)
    elimsToSpine :: forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es = do
        spine <- (Elim -> ST s (Elim' (Pointer s)))
    -> Elims -> ST s [Elim' (Pointer s)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> ST s (Elim' (Pointer s))
    thunk Elims
    es
        forceSpine spine `seq` return spine
      where
        -- Need to be strict in mkClosure to avoid memory leak
        forceSpine :: [Elim' (Pointer s)] -> ()
    forceSpine = (() -> Elim' (Pointer s) -> ()) -> () -> [Elim' (Pointer s)] -> ()
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\ () -> Elim' (Pointer s) -> ()
    forall {s}. Elim' (Pointer s) -> ()
    forceEl) ()
        forceEl :: Elim' (Pointer s) -> ()
    forceEl (Apply (Arg ArgInfo
    _ (Pure Closure{}))) = ()
        forceEl (Apply (Arg ArgInfo
    _ (Pointer{})))      = ()
        forceEl Elim' (Pointer s)
    _                                = ()

        -- We don't preserve free variables of closures (in the sense of their
        -- decoding), since we freely add things to the spines.
        unknownFVs :: ArgInfo -> ArgInfo
    unknownFVs = FreeVariables -> ArgInfo -> ArgInfo
    forall a. LensFreeVariables a => FreeVariables -> a -> a
    setFreeVariables FreeVariables
    unknownFreeVariables

        thunk :: Elim -> ST s (Elim' (Pointer s))
    thunk (Apply (Arg ArgInfo
    i Term
    t)) = Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> (Pointer s -> Arg (Pointer s)) -> Pointer s -> Elim' (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Pointer s -> Arg (Pointer s)
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo -> ArgInfo
    unknownFVs ArgInfo
    i) (Pointer s -> Elim' (Pointer s))
    -> ST s (Pointer s) -> ST s (Elim' (Pointer s))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Closure s -> ST s (Pointer s)
    forall s. Closure s -> ST s (Pointer s)
    createThunk (FreeVariables -> Term -> Closure s
    closure (ArgInfo -> FreeVariables
    forall a. LensFreeVariables a => a -> FreeVariables
    getFreeVariables ArgInfo
    i) Term
    t)
        thunk (Proj ProjOrigin
    o QName
    f)        = Elim' (Pointer s) -> ST s (Elim' (Pointer s))
    forall a. a -> ST s a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProjOrigin -> QName -> Elim' (Pointer s)
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f)
        thunk (IApply Term
    a Term
    x Term
    y)    = Pointer s -> Pointer s -> Pointer s -> Elim' (Pointer s)
    forall a. a -> a -> a -> Elim' a
    IApply (Pointer s -> Pointer s -> Pointer s -> Elim' (Pointer s))
    -> ST s (Pointer s)
    -> ST s (Pointer s -> Pointer s -> Elim' (Pointer s))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> ST s (Pointer s)
    mkThunk Term
    a ST s (Pointer s -> Pointer s -> Elim' (Pointer s))
    -> ST s (Pointer s) -> ST s (Pointer s -> Elim' (Pointer s))
    forall a b. ST s (a -> b) -> ST s a -> ST s b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> ST s (Pointer s)
    mkThunk Term
    x ST s (Pointer s -> Elim' (Pointer s))
    -> ST s (Pointer s) -> ST s (Elim' (Pointer s))
    forall a b. ST s (a -> b) -> ST s a -> ST s b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> ST s (Pointer s)
    mkThunk Term
    y
          where mkThunk :: Term -> ST s (Pointer s)
    mkThunk = Closure s -> ST s (Pointer s)
    forall s. Closure s -> ST s (Pointer s)
    createThunk (Closure s -> ST s (Pointer s))
    -> (Term -> Closure s) -> Term -> ST s (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FreeVariables -> Term -> Closure s
    closure FreeVariables
    UnknownFVs

        -- Going straight for a value for literals is mostly to make debug traces
        -- less verbose and doesn't really buy anything performance-wise.
        closure :: FreeVariables -> Term -> Closure s
    closure FreeVariables
    _ t :: Term
    t@Lit{} = IsValue -> Term -> Env s -> [Elim' (Pointer s)] -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value (Blocked_ -> IsValue) -> Blocked_ -> IsValue
    forall a b. (a -> b) -> a -> b
    $ () -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) Term
    t Env s
    forall s. Env s
    emptyEnv []
        closure FreeVariables
    fv Term
    t      = Env s
    env' Env s -> Closure s -> Closure s
    forall a b. a -> b -> b
    `seq` IsValue -> Term -> Env s -> [Elim' (Pointer s)] -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled Term
    t Env s
    env' []
          where env' :: Env s
    env' = FreeVariables -> Env s -> Env s
    forall s. FreeVariables -> Env s -> Env s
    trimEnvironment FreeVariables
    fv Env s
    env

    -- | Trim unused entries from an environment. Currently only trims closed terms for performance
    --   reasons.
    trimEnvironment :: FreeVariables -> Env s -> Env s
    trimEnvironment :: forall s. FreeVariables -> Env s -> Env s
    trimEnvironment FreeVariables
    UnknownFVs Env s
    env = Env s
    env
    trimEnvironment (KnownFVs IntSet
    fvs) Env s
    env
      | IntSet -> Bool
    IntSet.null IntSet
    fvs = Env s
    forall s. Env s
    emptyEnv
        -- Environment trimming is too expensive (costs 50% on some benchmarks), and while it does make
        -- some cases run in constant instead of linear space you need quite contrived examples to
        -- notice the effect.
      | Bool
    otherwise       = Env s
    env -- Env $ trim 0 $ envToList env
      where
        -- Important: strict enough that the trimming actually happens
        trim :: Int -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    trim Int
    _ [] = []
        trim Int
    i (Pointer (ZonkAny 0)
    p : [Pointer (ZonkAny 0)]
    ps)
          | Int -> IntSet -> Bool
    IntSet.member Int
    i IntSet
    fvs = (Pointer (ZonkAny 0)
    p Pointer (ZonkAny 0)
    -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    forall a. a -> [a] -> [a]
    :)             ([Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)])
    -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    forall a b. (a -> b) -> a -> b
    $! Int -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    trim (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [Pointer (ZonkAny 0)]
    ps
          | Bool
    otherwise           = (Pointer (ZonkAny 0)
    forall s. Pointer s
    unusedPointer Pointer (ZonkAny 0)
    -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    forall a. a -> [a] -> [a]
    :) ([Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)])
    -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    forall a b. (a -> b) -> a -> b
    $! Int -> [Pointer (ZonkAny 0)] -> [Pointer (ZonkAny 0)]
    trim (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [Pointer (ZonkAny 0)]
    ps

    -- | Build an environment for a body with some given free variables from a spine of arguments.
    --   Returns a triple containing
    --    * the left-over variable names (in case of partial application)
    --    * the environment
    --    * the remaining spine (in case of over-application)
    buildEnv :: [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
    buildEnv :: forall s.
    [Arg VerboseKey] -> Spine s -> ([Arg VerboseKey], Env s, Spine s)
    buildEnv [Arg VerboseKey]
    xs Spine s
    spine = [Arg VerboseKey]
    -> Spine s -> Env s -> ([Arg VerboseKey], Env s, Spine s)
    forall {a} {s}.
    [a]
    -> [Elim' (Pointer s)]
    -> Env s
    -> ([a], Env s, [Elim' (Pointer s)])
    go [Arg VerboseKey]
    xs Spine s
    spine Env s
    forall s. Env s
    emptyEnv
      where
        go :: [a]
    -> [Elim' (Pointer s)]
    -> Env s
    -> ([a], Env s, [Elim' (Pointer s)])
    go [] [Elim' (Pointer s)]
    sp Env s
    env = ([], Env s
    env, [Elim' (Pointer s)]
    sp)
        go xs0 :: [a]
    xs0@(a
    x : [a]
    xs) [Elim' (Pointer s)]
    sp Env s
    env =
          case [Elim' (Pointer s)]
    sp of
            []           -> ([a]
    xs0, Env s
    env, [Elim' (Pointer s)]
    sp)
            Apply Arg (Pointer s)
    c : [Elim' (Pointer s)]
    sp -> [a]
    -> [Elim' (Pointer s)]
    -> Env s
    -> ([a], Env s, [Elim' (Pointer s)])
    go [a]
    xs [Elim' (Pointer s)]
    sp (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    c Pointer s -> Env s -> Env s
    forall s. Pointer s -> Env s -> Env s
    `extendEnv` Env s
    env)
            IApply Pointer s
    x Pointer s
    y Pointer s
    r : [Elim' (Pointer s)]
    sp -> [a]
    -> [Elim' (Pointer s)]
    -> Env s
    -> ([a], Env s, [Elim' (Pointer s)])
    go [a]
    xs [Elim' (Pointer s)]
    sp (Pointer s
    r Pointer s -> Env s -> Env s
    forall s. Pointer s -> Env s -> Env s
    `extendEnv` Env s
    env)
            [Elim' (Pointer s)]
    _            -> ([a], Env s, [Elim' (Pointer s)])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unusedPointerString :: Text
    unusedPointerString :: Text
    unusedPointerString = VerboseKey -> Text
    T.pack (Impossible -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show ((CallStack -> Impossible) -> Impossible
    forall b. HasCallStack => (CallStack -> b) -> b
    withCurrentCallStack CallStack -> Impossible
    Impossible))

    unusedPointer :: Pointer s
    unusedPointer :: forall s. Pointer s
    unusedPointer = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    Pure (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value (Blocked_ -> IsValue) -> Blocked_ -> IsValue
    forall a b. (a -> b) -> a -> b
    $ () -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ())
                         (Literal -> Term
    Lit (Text -> Literal
    LitString Text
    unusedPointerString)) Env s
    forall s. Env s
    emptyEnv [])

    -- * Running the abstract machine

    -- | Evaluating a term in the abstract machine. It gets the type checking state and environment in
    --   the 'ReduceEnv' argument, some precomputed built-in mappings in 'BuiltinEnv', the memoised
    --   'getConstInfo' function, a couple of flags (allow non-terminating function unfolding, and
    --   whether rewriting is enabled), and a term to reduce. The result is the weak-head normal form of
    --   the term with an attached blocking tag.
    reduceTm :: ReduceEnv -> BuiltinEnv -> (QName -> CompactDef) -> Normalisation -> Term -> Blocked Term
    reduceTm :: ReduceEnv
    -> BuiltinEnv
    -> (QName -> CompactDef)
    -> Normalisation
    -> Term
    -> Blocked Term
    reduceTm ReduceEnv
    rEnv BuiltinEnv
    bEnv !QName -> CompactDef
    constInfo Normalisation
    normalisation =
        Term -> Blocked Term
    compileAndRun (Term -> Blocked Term) -> (Term -> Term) -> Term -> Blocked Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Term -> Term
    forall a. Doc -> a -> a
    traceDoc Doc
    "-- fast reduce --"
      where
        -- Helpers to get information from the ReduceEnv.
        localMetas :: Map MetaId MetaVariable
    localMetas     = ReduceEnv -> TCState
    redSt ReduceEnv
    rEnv TCState
    -> Lens' TCState (Map MetaId MetaVariable)
    -> Map MetaId MetaVariable
    forall o i. o -> Lens' o i -> i
    ^. (Map MetaId MetaVariable -> f (Map MetaId MetaVariable))
    -> TCState -> f TCState
    Lens' TCState (Map MetaId MetaVariable)
    stSolvedMetaStore
        remoteMetas :: HashMap MetaId RemoteMetaVariable
    remoteMetas    = ReduceEnv -> TCState
    redSt ReduceEnv
    rEnv TCState
    -> Lens' TCState (HashMap MetaId RemoteMetaVariable)
    -> HashMap MetaId RemoteMetaVariable
    forall o i. o -> Lens' o i -> i
    ^. (HashMap MetaId RemoteMetaVariable
     -> f (HashMap MetaId RemoteMetaVariable))
    -> TCState -> f TCState
    Lens' TCState (HashMap MetaId RemoteMetaVariable)
    stImportedMetaStore
        -- Are we currently instance searching. In that case we don't fail hard on missing clauses. This
        -- is a (very unsatisfactory) work-around for #3870.
        speculative :: Bool
    speculative    = ReduceEnv -> TCState
    redSt ReduceEnv
    rEnv TCState -> Lens' TCState Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stConsideringInstance
        getMetaInst :: MetaId -> Maybe MetaInstantiation
    getMetaInst MetaId
    m  = case MetaId -> Map MetaId MetaVariable -> Maybe MetaVariable
    forall k a. Ord k => k -> Map k a -> Maybe a
    MapS.lookup MetaId
    m Map MetaId MetaVariable
    localMetas of
                           Just MetaVariable
    mv -> MetaInstantiation -> Maybe MetaInstantiation
    forall a. a -> Maybe a
    Just (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv)
                           Maybe MetaVariable
    Nothing -> Instantiation -> MetaInstantiation
    InstV (Instantiation -> MetaInstantiation)
    -> (RemoteMetaVariable -> Instantiation)
    -> RemoteMetaVariable
    -> MetaInstantiation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RemoteMetaVariable -> Instantiation
    rmvInstantiation (RemoteMetaVariable -> MetaInstantiation)
    -> Maybe RemoteMetaVariable -> Maybe MetaInstantiation
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                                        MetaId
    -> HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup MetaId
    m HashMap MetaId RemoteMetaVariable
    remoteMetas
        partialDefs :: Set QName
    partialDefs    = ReduceM (Set QName) -> Set QName
    forall a. ReduceM a -> a
    runReduce ReduceM (Set QName)
    forall (m :: * -> *). ReadTCState m => m (Set QName)
    getPartialDefs
        rewriteRules :: QName -> RewriteRules
    rewriteRules QName
    f = CompactDef -> RewriteRules
    cdefRewriteRules (QName -> CompactDef
    constInfo QName
    f)
        callByNeed :: Bool
    callByNeed     = TCEnv -> Bool
    envCallByNeed (ReduceEnv -> TCEnv
    redEnv ReduceEnv
    rEnv) Bool -> Bool -> Bool
    && Bool -> Bool
    not (PragmaOptions -> Bool
    optCallByName (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a b. (a -> b) -> a -> b
    $ ReduceEnv -> TCState
    redSt ReduceEnv
    rEnv TCState -> Lens' TCState PragmaOptions -> PragmaOptions
    forall o i. o -> Lens' o i -> i
    ^. (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions)
        iview :: Term -> IntervalView
    iview          = ReduceM (Term -> IntervalView) -> Term -> IntervalView
    forall a. ReduceM a -> a
    runReduce ReduceM (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'

        runReduce :: ReduceM a -> a
        runReduce :: forall a. ReduceM a -> a
    runReduce ReduceM a
    m = ReduceM a -> ReduceEnv -> a
    forall a. ReduceM a -> ReduceEnv -> a
    unReduceM ReduceM a
    m ReduceEnv
    rEnv

        -- Debug output. Taking care that we only look at the verbosity level once.
        hasVerb :: VerboseKey -> Int -> Bool
    hasVerb VerboseKey
    tag Int
    lvl = ReduceM Bool -> ReduceEnv -> Bool
    forall a. ReduceM a -> ReduceEnv -> a
    unReduceM (VerboseKey -> Int -> ReduceM Bool
    forall (m :: * -> *). MonadDebug m => VerboseKey -> Int -> m Bool
    hasVerbosity VerboseKey
    tag Int
    lvl) ReduceEnv
    rEnv
        doDebug :: Bool
    doDebug = VerboseKey -> Int -> Bool
    hasVerb VerboseKey
    "tc.reduce.fast" Int
    110
        traceDoc :: Doc -> a -> a
        traceDoc :: forall a. Doc -> a -> a
    traceDoc
          | Bool
    doDebug   = VerboseKey -> a -> a
    forall a. VerboseKey -> a -> a
    trace (VerboseKey -> a -> a) -> (Doc -> VerboseKey) -> Doc -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show
          | Bool
    otherwise = (a -> a) -> Doc -> a -> a
    forall a b. a -> b -> a
    const a -> a
    forall a. a -> a
    id

        -- Checking for built-in zero and suc
        BuiltinEnv{ bZero :: BuiltinEnv -> Maybe ConHead
    bZero = Maybe ConHead
    zero, bSuc :: BuiltinEnv -> Maybe ConHead
    bSuc = Maybe ConHead
    suc, bRefl :: BuiltinEnv -> Maybe ConHead
    bRefl = Maybe ConHead
    refl0 } = BuiltinEnv
    bEnv
        conNameId :: ConHead -> NameId
    conNameId = Name -> NameId
    nameId (Name -> NameId) -> (ConHead -> Name) -> ConHead -> NameId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName (QName -> Name) -> (ConHead -> QName) -> ConHead -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName
        isZero :: ConHead -> Bool
    isZero = case Maybe ConHead
    zero of
                   Maybe ConHead
    Nothing -> Bool -> ConHead -> Bool
    forall a b. a -> b -> a
    const Bool
    False
                   Just ConHead
    z  -> (ConHead -> NameId
    conNameId ConHead
    z NameId -> NameId -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (NameId -> Bool) -> (ConHead -> NameId) -> ConHead -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> NameId
    conNameId
        isSuc :: ConHead -> Bool
    isSuc  = case Maybe ConHead
    suc of
                   Maybe ConHead
    Nothing -> Bool -> ConHead -> Bool
    forall a b. a -> b -> a
    const Bool
    False
                   Just ConHead
    s  -> (ConHead -> NameId
    conNameId ConHead
    s NameId -> NameId -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (NameId -> Bool) -> (ConHead -> NameId) -> ConHead -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> NameId
    conNameId

        -- If there's a non-standard equality (for instance doubly-indexed) we fall back to slow reduce
        -- for primErase and "unbind" refl.
        refl :: Maybe ConHead
    refl = Maybe ConHead
    refl0 Maybe ConHead -> (ConHead -> Maybe ConHead) -> Maybe ConHead
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ ConHead
    c -> if CompactDefn -> Int
    cconArity (CompactDef -> CompactDefn
    cdefDef (CompactDef -> CompactDefn) -> CompactDef -> CompactDefn
    forall a b. (a -> b) -> a -> b
    $ QName -> CompactDef
    constInfo (QName -> CompactDef) -> QName -> CompactDef
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c) Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0
                                then ConHead -> Maybe ConHead
    forall a. a -> Maybe a
    Just ConHead
    c else Maybe ConHead
    forall a. Maybe a
    Nothing

        -- The entry point of the machine.
        compileAndRun :: Term -> Blocked Term
        compileAndRun :: Term -> Blocked Term
    compileAndRun Term
    t = (forall s. ST s (Blocked Term)) -> Blocked Term
    forall a. (forall s. ST s a) -> a
    runST (AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Normalisation -> Term -> AM s
    forall s. Normalisation -> Term -> AM s
    compile Normalisation
    normalisation Term
    t))

        -- Run the machine in a given state. Prints the state if the right verbosity level is active.
        runAM :: AM s -> ST s (Blocked Term)
        runAM :: forall s. AM s -> ST s (Blocked Term)
    runAM = if Bool
    doDebug then \ AM s
    s -> VerboseKey -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a. VerboseKey -> a -> a
    trace (AM s -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow AM s
    s) (AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM' AM s
    s)
                           else AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM'

        -- The main function. This is where the stuff happens!
        runAM' :: AM s -> ST s (Blocked Term)

        -- Base case: The focus is a value closure and the control stack is empty. Decode and return.
        runAM' :: forall s. AM s -> ST s (Blocked Term)
    runAM' (Eval cl :: Closure s
    cl@(Closure Value{} Term
    _ Env s
    _ Spine s
    _) []) = Closure s -> ST s (Blocked Term)
    forall s. Closure s -> ST s (Blocked Term)
    decodeClosure Closure s
    cl

        -- Unevaluated closure: inspect the term and take the appropriate action. For instance,
        --  - Change to the 'Match' state if a definition
        --  - Look up in the environment if variable
        --  - Perform a beta step if lambda and application elimination in the spine
        --  - Perform a record beta step if record constructor and projection elimination in the spine
        runAM' s :: AM s
    s@(Eval cl :: Closure s
    cl@(Closure IsValue
    Unevaled Term
    t Env s
    env Spine s
    spine) [ControlFrame s]
    ctrl) = {-# SCC "runAM.Eval" #-}
          case Term
    t of

            -- Case: definition. Enter 'Match' state if defined function or shift to evaluating an
            -- argument and pushing the appropriate control frame for primitive functions. Fall back to
            -- slow reduce for unsupported definitions.
            Def QName
    f [] ->
              Spine s
    -> [ControlFrame s] -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall s.
    Spine s
    -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
    evalIApplyAM Spine s
    spine [ControlFrame s]
    ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $
              let CompactDef{ cdefNonterminating :: CompactDef -> Bool
    cdefNonterminating = Bool
    nonterm
                            , cdefUnconfirmed :: CompactDef -> Bool
    cdefUnconfirmed    = Bool
    unconf
                            , cdefDef :: CompactDef -> CompactDefn
    cdefDef            = CompactDefn
    def } = QName -> CompactDef
    constInfo QName
    f
              in case CompactDefn
    def of
                CFun{ cfunCompiled :: CompactDefn -> FastCompiledClauses
    cfunCompiled = FastCompiledClauses
    cc } -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc Spine s
    spine ([] [CatchallFrame s] -> Closure s -> MatchStack s
    forall s. [CatchallFrame s] -> Closure s -> MatchStack s
    :> Closure s
    cl) [ControlFrame s]
    ctrl)
                CompactDefn
    CAxiom         -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM AM s
    done
                CompactDefn
    CTyCon         -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM AM s
    done
                CCon{}         -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done   -- Only happens for builtinSharp (which is a Def when you bind it)
                CompactDefn
    CForce | (Spine s
    spine0, Apply Arg (Pointer s)
    v : Spine s
    spine1) <- Int -> Spine s -> (Spine s, Spine s)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    4 Spine s
    spine ->
                  Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    v) [] (QName -> Spine s -> Spine s -> ControlFrame s
    forall s. QName -> Spine s -> Spine s -> ControlFrame s
    ForceK QName
    f Spine s
    spine0 Spine s
    spine1 ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)
                CompactDefn
    CForce -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done -- partially applied
                CompactDefn
    CErase | (Spine s
    spine0, Apply Arg (Pointer s)
    v : Elim' (Pointer s)
    spine1 : Spine s
    spine2) <- Int -> Spine s -> (Spine s, Spine s)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    2 Spine s
    spine ->
                  Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    v) [] (QName -> Spine s -> Spine s -> Spine s -> Spine s -> ControlFrame s
    forall s.
    QName -> Spine s -> Spine s -> Spine s -> Spine s -> ControlFrame s
    EraseK QName
    f Spine s
    spine0 [] [Elim' (Pointer s)
    spine1] Spine s
    spine2 ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)
                CompactDefn
    CErase -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done -- partially applied
                CPrimOp Int
    n [Literal] -> Term
    op Maybe FastCompiledClauses
    cc | Spine s -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Spine s
    spine Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n,                      -- PrimOps can't be over-applied. They don't
                                  Just (Arg (Pointer s)
    v : [Arg (Pointer s)]
    vs) <- Spine s -> Maybe [Arg (Pointer s)]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Spine s
    spine -> -- return functions or records.
                  Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    v) [] (QName
    -> ([Literal] -> Term)
    -> [Literal]
    -> [Pointer s]
    -> Maybe FastCompiledClauses
    -> ControlFrame s
    forall s.
    QName
    -> ([Literal] -> Term)
    -> [Literal]
    -> [Pointer s]
    -> Maybe FastCompiledClauses
    -> ControlFrame s
    PrimOpK QName
    f [Literal] -> Term
    op [] ((Arg (Pointer s) -> Pointer s) -> [Arg (Pointer s)] -> [Pointer s]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg [Arg (Pointer s)]
    vs) Maybe FastCompiledClauses
    cc ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)
                CPrimOp{} -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done  -- partially applied
                CompactDefn
    COther    -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM AM s
    s

            -- Case: zero. Return value closure with literal 0.
            Con ConHead
    c ConInfo
    i [] | ConHead -> Bool
    isZero ConHead
    c ->
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue (Literal -> Term
    Lit (Integer -> Literal
    LitNat Integer
    0)) Env s
    forall s. Env s
    emptyEnv Spine s
    spine [ControlFrame s]
    ctrl)

            -- Case: suc. Suc is strict in its argument to make sure we return a literal whenever
            -- possible. Push a 'NatSucK' frame on the control stack and evaluate the argument.
            Con ConHead
    c ConInfo
    i [] | ConHead -> Bool
    isSuc ConHead
    c, Apply Arg (Pointer s)
    v : Spine s
    _ <- Spine s
    spine ->
              Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    v) [] ([ControlFrame s] -> [ControlFrame s]
    forall s. ControlStack s -> ControlStack s
    sucCtrl [ControlFrame s]
    ctrl)

            -- Case: constructor. Perform beta reduction if projected from, otherwise return a value.
            Con ConHead
    c ConInfo
    i []
              -- Constructors of types in Prop are not representex as
              -- CCon, so this match might fail!
              | CCon{cconSrcCon :: CompactDefn -> ConHead
    cconSrcCon = ConHead
    c', cconArity :: CompactDefn -> Int
    cconArity = Int
    ar} <- CompactDef -> CompactDefn
    cdefDef (QName -> CompactDef
    constInfo (ConHead -> QName
    conName ConHead
    c)) ->
                Spine s
    -> [ControlFrame s] -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall s.
    Spine s
    -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
    evalIApplyAM Spine s
    spine [ControlFrame s]
    ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $
                case Int -> Spine s -> (Spine s, Spine s)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    ar Spine s
    spine of
                  (Spine s
    args, Proj ProjOrigin
    _ QName
    p : Spine s
    spine')
                      -> Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    arg) Spine s
    spine' [ControlFrame s]
    ctrl  -- Andreas #2170: fit argToDontCare here?!
                    where
                      fields :: [QName]
    fields    = (Arg QName -> QName) -> [Arg QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg QName -> QName
    forall e. Arg e -> e
    unArg ([Arg QName] -> [QName]) -> [Arg QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ ConHead -> [Arg QName]
    conFields ConHead
    c
                      Just Int
    n    = QName -> [QName] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex QName
    p [QName]
    fields
                      Apply Arg (Pointer s)
    arg = Spine s
    args Spine s -> Int -> Elim' (Pointer s)
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n
                  (Spine s, Spine s)
    _ -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c' ConInfo
    i []) Env s
    env Spine s
    spine [ControlFrame s]
    ctrl)
              | Bool
    otherwise -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done

            -- Case: variable. Look up the variable in the environment and evaluate the resulting
            -- pointer. If the variable is not in the environment it's a free variable and we adjust the
            -- deBruijn index appropriately.
            Var Int
    x []   ->
              Spine s
    -> [ControlFrame s] -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall s.
    Spine s
    -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
    evalIApplyAM Spine s
    spine [ControlFrame s]
    ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $
              case Int -> Env s -> Maybe (Pointer s)
    forall s. Int -> Env s -> Maybe (Pointer s)
    lookupEnv Int
    x Env s
    env of
                Maybe (Pointer s)
    Nothing -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Blocked_ -> Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}.
    Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalValue (() -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) (Int -> Elims -> Term
    Var (Int
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Env s -> Int
    forall s. Env s -> Int
    envSize Env s
    env) []) Env s
    forall s. Env s
    emptyEnv Spine s
    spine [ControlFrame s]
    ctrl)
                Just Pointer s
    p  -> Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Pointer s
    p Spine s
    spine [ControlFrame s]
    ctrl

            -- Case: lambda. Perform the beta reduction if applied. Otherwise it's a value.
            Lam ArgInfo
    h Abs Term
    b ->
              case Spine s
    spine of
                [] -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done
                Elim' (Pointer s)
    elim : Spine s
    spine' ->
                  case Abs Term
    b of
                    Abs   VerboseKey
    _ Term
    b -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalClosure Term
    b (Elim' (Pointer s) -> Pointer s
    forall {e}. Elim' e -> e
    getArg Elim' (Pointer s)
    elim Pointer s -> Env s -> Env s
    forall s. Pointer s -> Env s -> Env s
    `extendEnv` Env s
    env) Spine s
    spine' [ControlFrame s]
    ctrl)
                    NoAbs VerboseKey
    _ Term
    b -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalClosure Term
    b Env s
    env Spine s
    spine' [ControlFrame s]
    ctrl)
              where
                getArg :: Elim' e -> e
    getArg (Apply Arg e
    v)      = Arg e -> e
    forall e. Arg e -> e
    unArg Arg e
    v
                getArg (IApply e
    _ e
    _ e
    v) = e
    v
                getArg Proj{}         = e
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Case: values. Literals and function types are already in weak-head normal form.
            -- We throw away the environment for literals mostly to make debug printing less verbose.
            -- And we know the spine is empty since literals cannot be applied or projected.
            Lit{} -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue Term
    t Env s
    forall s. Env s
    emptyEnv [] [ControlFrame s]
    ctrl)
            Pi{}  -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done
            DontCare{} -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done

            -- Case: non-empty spine. If the focused term has a non-empty spine, we shift the
            -- eliminations onto the spine.
            Def QName
    f   Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (QName -> Elims -> Term
    Def QName
    f   []) Env s
    forall s. Env s
    emptyEnv Env s
    env Elims
    es
            Con ConHead
    c ConInfo
    i Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    i []) Env s
    forall s. Env s
    emptyEnv Env s
    env Elims
    es
            Var Int
    x   Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (Int -> Elims -> Term
    Var Int
    x   []) Env s
    env      Env s
    env Elims
    es

            -- Case: metavariable. If it's instantiated evaluate the value. Meta instantiations are open
            -- terms with a specified list of free variables. buildEnv constructs the appropriate
            -- environment for the closure. Avoiding shifting spines for open metas
            -- save a bit of performance.
            MetaV MetaId
    m Elims
    es -> Spine s
    -> [ControlFrame s] -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall s.
    Spine s
    -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
    evalIApplyAM Spine s
    spine [ControlFrame s]
    ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $
              case MetaId -> Maybe MetaInstantiation
    getMetaInst MetaId
    m of
                Maybe MetaInstantiation
    Nothing ->
                  AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (MetaId -> () -> Blocked_
    forall a t. MetaId -> a -> Blocked' t a
    blocked MetaId
    m ()) Closure s
    cl) [ControlFrame s]
    ctrl)
                Just (InstV Instantiation
    i) -> do
                  spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  let (zs, env, !spine'') = buildEnv (instTel i) (spine' <> spine)
                  runAM (evalClosure (lams zs (instBody i)) env spine'' ctrl)
                Just OpenMeta{}                     -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                Just BlockedConst{}                 -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                Just PostponedTypeCheckingProblem{} -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Case: unsupported. These terms are not handled by the abstract machine, so we fall back
            -- to slowReduceTerm for these.
            Level{}    -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM AM s
    s
            Sort{}     -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM AM s
    s
            Dummy{}    -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM AM s
    s

          where done :: AM s
    done = Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (() -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) Closure s
    cl) [ControlFrame s]
    ctrl
                shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims Term
    t Env s
    env0 Env s
    env Elims
    es = do
                  spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  runAM (evalClosure t env0 (spine' <> spine) ctrl)

        -- If the current focus is a value closure, we look at the control stack.

        -- Case NormaliseK: The focus is a weak-head value that should be fully normalised.
        runAM' s :: AM s
    s@(Eval cl :: Closure s
    cl@(Closure IsValue
    b Term
    t Env s
    env Spine s
    spine) (ControlFrame s
    NormaliseK : [ControlFrame s]
    ctrl)) =
          case Term
    t of
            Def QName
    _   [] -> Closure s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    b Term
    t Env s
    forall s. Env s
    emptyEnv []) Spine s
    spine [ControlFrame s]
    ctrl
            Con ConHead
    _ ConInfo
    _ [] -> Closure s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    b Term
    t Env s
    forall s. Env s
    emptyEnv []) Spine s
    spine [ControlFrame s]
    ctrl
            Var Int
    _   [] -> Closure s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    b Term
    t Env s
    forall s. Env s
    emptyEnv []) Spine s
    spine [ControlFrame s]
    ctrl
            MetaV MetaId
    _ [] -> Closure s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    b Term
    t Env s
    forall s. Env s
    emptyEnv []) Spine s
    spine [ControlFrame s]
    ctrl

            Lit{} -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    done

            -- We might get these from fallbackAM
            Def QName
    f   Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (QName -> Elims -> Term
    Def QName
    f   []) Env s
    forall s. Env s
    emptyEnv Env s
    env Elims
    es
            Con ConHead
    c ConInfo
    i Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    i []) Env s
    forall s. Env s
    emptyEnv Env s
    env Elims
    es
            Var Int
    x   Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (Int -> Elims -> Term
    Var Int
    x   []) Env s
    env      Env s
    env Elims
    es
            MetaV MetaId
    m Elims
    es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims (MetaId -> Elims -> Term
    MetaV MetaId
    m []) Env s
    forall s. Env s
    emptyEnv Env s
    env Elims
    es

            Term
    _ -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM AM s
    s -- fallbackAM knows about NormaliseK

          where done :: AM s
    done = Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (() -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) Closure s
    cl) [ControlFrame s]
    ctrl
                shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
    shiftElims Term
    t Env s
    env0 Env s
    env Elims
    es = do
                  spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  runAM (Eval (Closure b t env0 (spine' <> spine)) (NormaliseK : ctrl))

        -- Case: ArgK: We successfully normalised an argument. Start on the next argument, or if there
        -- isn't one we're done.
        runAM' (Eval Closure s
    cl (ArgK Closure s
    cl0 SpineContext s
    cxt : [ControlFrame s]
    ctrl)) =
          case Element (SpineContext s)
    -> SpineContext s
    -> Either
         (Carrier (SpineContext s))
         (Element (SpineContext s), SpineContext s)
    forall z.
    Zipper z =>
    Element z -> z -> Either (Carrier z) (Element z, z)
    nextHole (Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk Closure s
    cl) SpineContext s
    cxt of
            Left Carrier (SpineContext s)
    spine      -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Closure s -> Spine s -> Closure s
    forall s. Closure s -> Spine s -> Closure s
    clApply_ Closure s
    cl0 Spine s
    Carrier (SpineContext s)
    spine) [ControlFrame s]
    ctrl)
            Right (Element (SpineContext s)
    p, SpineContext s
    cxt') -> Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Element (SpineContext s)
    Pointer s
    p [] (ControlFrame s
    forall s. ControlFrame s
    NormaliseK ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : Closure s -> SpineContext s -> ControlFrame s
    forall s. Closure s -> SpineContext s -> ControlFrame s
    ArgK Closure s
    cl0 SpineContext s
    cxt' ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)

        -- Case: NatSucK m

        -- If literal add m to the literal,
        runAM' (Eval cl :: Closure s
    cl@(Closure Value{} (Lit (LitNat Integer
    n)) Env s
    _ Spine s
    _) (NatSucK Integer
    m : [ControlFrame s]
    ctrl)) =
          AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue (Literal -> Term
    Lit (Literal -> Term) -> Literal -> Term
    forall a b. (a -> b) -> a -> b
    $! Integer -> Literal
    LitNat (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $! Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n) Env s
    forall s. Env s
    emptyEnv [] [ControlFrame s]
    ctrl)

        -- otherwise apply 'suc' m times.
        runAM' (Eval Closure s
    cl (NatSucK Integer
    m : [ControlFrame s]
    ctrl)) =
            AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (() -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) (Closure s -> Closure s) -> Closure s -> Closure s
    forall a b. (a -> b) -> a -> b
    $ Integer -> Closure s -> Closure s
    plus Integer
    m Closure s
    cl) [ControlFrame s]
    ctrl)
          where
            plus :: Integer -> Closure s -> Closure s
    plus Integer
    0 Closure s
    cl = Closure s
    cl
            plus Integer
    n Closure s
    cl =
              Term -> Env s -> Spine s -> Closure s
    forall {s}. Term -> Env s -> Spine s -> Closure s
    trueValue (ConHead -> ConInfo -> Elims -> Term
    Con (ConHead -> Maybe ConHead -> ConHead
    forall a. a -> Maybe a -> a
    fromMaybe ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe ConHead
    suc) ConInfo
    ConOSystem []) Env s
    forall s. Env s
    emptyEnv (Spine s -> Closure s) -> Spine s -> Closure s
    forall a b. (a -> b) -> a -> b
    $
                         Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg Pointer s
    arg) Elim' (Pointer s) -> Spine s -> Spine s
    forall a. a -> [a] -> [a]
    : []
              where arg :: Pointer s
    arg = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk (Integer -> Closure s -> Closure s
    plus (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Closure s
    cl)

        -- Case: PrimOpK

        -- If literal apply the primitive function if no more arguments, otherwise
        -- store the literal in the continuation and evaluate the next argument.
        runAM' (Eval (Closure IsValue
    _ (Lit Literal
    a) Env s
    _ Spine s
    _) (PrimOpK QName
    f [Literal] -> Term
    op [Literal]
    vs [Pointer s]
    es Maybe FastCompiledClauses
    cc : [ControlFrame s]
    ctrl)) =
          case [Pointer s]
    es of
            []      -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue ([Literal] -> Term
    op (Literal
    a Literal -> [Literal] -> [Literal]
    forall a. a -> [a] -> [a]
    : [Literal]
    vs)) Env s
    forall s. Env s
    emptyEnv [] [ControlFrame s]
    ctrl)
            Pointer s
    e : [Pointer s]
    es' -> Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Pointer s
    e [] (QName
    -> ([Literal] -> Term)
    -> [Literal]
    -> [Pointer s]
    -> Maybe FastCompiledClauses
    -> ControlFrame s
    forall s.
    QName
    -> ([Literal] -> Term)
    -> [Literal]
    -> [Pointer s]
    -> Maybe FastCompiledClauses
    -> ControlFrame s
    PrimOpK QName
    f [Literal] -> Term
    op (Literal
    a Literal -> [Literal] -> [Literal]
    forall a. a -> [a] -> [a]
    : [Literal]
    vs) [Pointer s]
    es' Maybe FastCompiledClauses
    cc ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)

        -- If not a literal we use the case tree if there is one, otherwise we are stuck.
        runAM' (Eval cl :: Closure s
    cl@(Closure (Value Blocked_
    blk) Term
    _ Env s
    _ Spine s
    _) (PrimOpK QName
    f [Literal] -> Term
    _ [Literal]
    vs [Pointer s]
    es Maybe FastCompiledClauses
    mcc : [ControlFrame s]
    ctrl)) =
          case Maybe FastCompiledClauses
    mcc of
            Maybe FastCompiledClauses
    Nothing -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval Closure s
    stuck [ControlFrame s]
    ctrl)
            Just FastCompiledClauses
    cc -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc Spine s
    spine ([] [CatchallFrame s] -> Closure s -> MatchStack s
    forall s. [CatchallFrame s] -> Closure s -> MatchStack s
    :> Closure s
    notstuck) [ControlFrame s]
    ctrl)
          where
            p :: Pointer s
    p         = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk Closure s
    cl
            lits :: [Pointer s]
    lits      = (Literal -> Pointer s) -> [Literal] -> [Pointer s]
    forall a b. (a -> b) -> [a] -> [b]
    map (Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk (Closure s -> Pointer s)
    -> (Literal -> Closure s) -> Literal -> Pointer s
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Literal -> Closure s
    forall {s}. Literal -> Closure s
    litClos) ([Literal] -> [Literal]
    forall a. [a] -> [a]
    reverse [Literal]
    vs)
            spine :: Spine s
    spine     = (Pointer s -> Elim' (Pointer s)) -> [Pointer s] -> Spine s
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> (Pointer s -> Arg (Pointer s)) -> Pointer s -> Elim' (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg) ([Pointer s] -> Spine s) -> [Pointer s] -> Spine s
    forall a b. (a -> b) -> a -> b
    $ [Pointer s]
    lits [Pointer s] -> [Pointer s] -> [Pointer s]
    forall a. Semigroup a => a -> a -> a
    <> [Pointer s
    p] [Pointer s] -> [Pointer s] -> [Pointer s]
    forall a. Semigroup a => a -> a -> a
    <> [Pointer s]
    es
            stuck :: Closure s
    stuck     = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value Blocked_
    blk) (QName -> Elims -> Term
    Def QName
    f []) Env s
    forall s. Env s
    emptyEnv Spine s
    spine
            notstuck :: Closure s
    notstuck  = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled    (QName -> Elims -> Term
    Def QName
    f []) Env s
    forall s. Env s
    emptyEnv Spine s
    spine
            litClos :: Literal -> Closure s
    litClos Literal
    l = Term -> Env s -> Spine s -> Closure s
    forall {s}. Term -> Env s -> Spine s -> Closure s
    trueValue (Literal -> Term
    Lit Literal
    l) Env s
    forall s. Env s
    emptyEnv []

        -- Case: ForceK. Here we need to check if the argument is a canonical form (i.e. not a variable
        -- or stuck function call) and if so apply the function argument to the value. If it's not
        -- canonical we are stuck.
        runAM' (Eval arg :: Closure s
    arg@(Closure (Value Blocked_
    blk) Term
    t Env s
    _ Spine s
    _) (ForceK QName
    pf Spine s
    spine0 Spine s
    spine1 : [ControlFrame s]
    ctrl))
          | Term -> Bool
    isCanonical Term
    t =
            case Spine s
    spine1 of
              Apply Arg (Pointer s)
    k : Spine s
    spine' ->
                Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    k) (Elim' (Pointer s)
    elim Elim' (Pointer s) -> Spine s -> Spine s
    forall a. a -> [a] -> [a]
    : Spine s
    spine') [ControlFrame s]
    ctrl
              [] -> -- Partial application of primForce to canonical argument, return λ k → k arg.
                AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue (Arg VerboseKey -> Term -> Term
    lam (VerboseKey -> Arg VerboseKey
    forall a. a -> Arg a
    defaultArg VerboseKey
    "k") (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 [Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    1 []])
                                     (Pointer s
    argPtr Pointer s -> Env s -> Env s
    forall s. Pointer s -> Env s -> Env s
    `extendEnv` Env s
    forall s. Env s
    emptyEnv) [] [ControlFrame s]
    ctrl)
              Spine s
    _ -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          | Bool
    otherwise = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval Closure s
    stuck [ControlFrame s]
    ctrl)
          where
            argPtr :: Pointer s
    argPtr = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk Closure s
    arg
            elim :: Elim' (Pointer s)
    elim   = Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg Pointer s
    argPtr)
            spine' :: Spine s
    spine' = Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> [Elim' (Pointer s)
    elim] Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1
            stuck :: Closure s
    stuck  = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value Blocked_
    blk) (QName -> Elims -> Term
    Def QName
    pf []) Env s
    forall s. Env s
    emptyEnv Spine s
    spine'

            isCanonical :: Term -> Bool
    isCanonical = \case
              Lit{}      -> Bool
    True
              Con{}      -> Bool
    True
              Lam{}      -> Bool
    True
              Pi{}       -> Bool
    True
              Sort{}     -> Bool
    True
              Level{}    -> Bool
    True
              DontCare{} -> Bool
    True
              Dummy{}    -> Bool
    False
              MetaV{}    -> Bool
    False
              Var{}      -> Bool
    False
              Def QName
    q Elims
    _  -- Type constructors (data/record) are considered canonical for 'primForce'.
                | CompactDefn
    CTyCon <- CompactDef -> CompactDefn
    cdefDef (QName -> CompactDef
    constInfo QName
    q) -> Bool
    True
                | Bool
    otherwise                       -> Bool
    False

        -- Case: EraseK. We evaluate both arguments to values, then do a simple check for the easy
        -- cases and otherwise fall back to slow reduce.
        runAM' (Eval cl2 :: Closure s
    cl2@(Closure Value{} Term
    arg2 Env s
    _ Spine s
    _) (EraseK QName
    f Spine s
    spine0 [Apply Arg (Pointer s)
    p1] Spine s
    _ Spine s
    spine3 : [ControlFrame s]
    ctrl)) = do
          cl1@(Closure _ arg1 _ sp1) <- Pointer s -> ST s (Closure s)
    forall s. Pointer s -> ST s (Closure s)
    derefPointer_ (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    p1)
          case (arg1, arg2) of
            (Lit Literal
    l1, Lit Literal
    l2) | Literal
    l1 Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l2, Maybe ConHead -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe ConHead
    refl ->
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue (ConHead -> ConInfo -> Elims -> Term
    Con (Maybe ConHead -> ConHead
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe ConHead
    refl) ConInfo
    ConOSystem []) Env s
    forall s. Env s
    emptyEnv [] [ControlFrame s]
    ctrl)
            (Term, Term)
    _ ->
              let spine :: Spine s
    spine = Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. [a] -> [a] -> [a]
    ++ (Closure s -> Elim' (Pointer s)) -> [Closure s] -> Spine s
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> (Closure s -> Arg (Pointer s)) -> Closure s -> Elim' (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Pointer s) -> Arg (Pointer s)
    forall a. LensHiding a => a -> a
    hide (Arg (Pointer s) -> Arg (Pointer s))
    -> (Closure s -> Arg (Pointer s)) -> Closure s -> Arg (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg (Pointer s -> Arg (Pointer s))
    -> (Closure s -> Pointer s) -> Closure s -> Arg (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk) [Closure s
    cl1, Closure s
    cl2] Spine s -> Spine s -> Spine s
    forall a. [a] -> [a] -> [a]
    ++ Spine s
    spine3 in
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    fallbackAM (Term -> Env s -> Spine s -> [ControlFrame s] -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalClosure (QName -> Elims -> Term
    Def QName
    f []) Env s
    forall s. Env s
    emptyEnv Spine s
    spine [ControlFrame s]
    ctrl)
        runAM' (Eval cl1 :: Closure s
    cl1@(Closure Value{} Term
    _ Env s
    _ Spine s
    _) (EraseK QName
    f Spine s
    spine0 [] [Apply Arg (Pointer s)
    p2] Spine s
    spine3 : [ControlFrame s]
    ctrl)) =
          Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    p2) [] (QName -> Spine s -> Spine s -> Spine s -> Spine s -> ControlFrame s
    forall s.
    QName -> Spine s -> Spine s -> Spine s -> Spine s -> ControlFrame s
    EraseK QName
    f Spine s
    spine0 [Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> Arg (Pointer s) -> Elim' (Pointer s)
    forall a b. (a -> b) -> a -> b
    $ Arg (Pointer s) -> Arg (Pointer s)
    forall a. LensHiding a => a -> a
    hide (Arg (Pointer s) -> Arg (Pointer s))
    -> Arg (Pointer s) -> Arg (Pointer s)
    forall a b. (a -> b) -> a -> b
    $ Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg (Pointer s -> Arg (Pointer s)) -> Pointer s -> Arg (Pointer s)
    forall a b. (a -> b) -> a -> b
    $ Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk Closure s
    cl1] [] Spine s
    spine3 ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl)
        runAM' (Eval Closure s
    _ (EraseK{} : [ControlFrame s]
    _)) =
          ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Case: UpdateThunk. Write the value to the pointers in the UpdateThunk frame.
        runAM' (Eval cl :: Closure s
    cl@(Closure Value{} Term
    _ Env s
    _ Spine s
    _) (UpdateThunk [STPointer s]
    ps : [ControlFrame s]
    ctrl)) =
          (STPointer s -> ST s ()) -> [STPointer s] -> ST s ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (STPointer s -> Closure s -> ST s ()
    forall s. STPointer s -> Closure s -> ST s ()
    `storePointer` Closure s
    cl) [STPointer s]
    ps ST s () -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. ST s a -> ST s b -> ST s b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval Closure s
    cl [ControlFrame s]
    ctrl)

        -- Case: ApplyK. Application after thunk update. Add the spine from the control frame to the
        -- closure.
        runAM' (Eval cl :: Closure s
    cl@(Closure Value{} Term
    _ Env s
    _ Spine s
    _) (ApplyK Spine s
    spine : [ControlFrame s]
    ctrl)) =
          AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Closure s -> Spine s -> Closure s
    forall s. Closure s -> Spine s -> Closure s
    clApply Closure s
    cl Spine s
    spine) [ControlFrame s]
    ctrl)

        -- Case: CaseK. Pattern matching against a value. If it's a stuck value the pattern match is
        -- stuck and we return the closure from the match stack (see stuckMatch). Otherwise we need to
        -- find a matching branch switch to the Match state. If there is no matching branch we look for
        -- a Catchall in the match stack, or fail if there isn't one (see failedMatch). If the current
        -- branches contain a catch-all case we need to push a Catchall on the match stack if picking
        -- one of the other branches.
        runAM' (Eval cl :: Closure s
    cl@(Closure (Value Blocked_
    blk) Term
    t Env s
    env Spine s
    spine) ctrl0 :: [ControlFrame s]
    ctrl0@(CaseK QName
    f ArgInfo
    i FastCase FastCompiledClauses
    bs Spine s
    spine0 Spine s
    spine1 MatchStack s
    stack : [ControlFrame s]
    ctrl)) =
          {-# SCC "runAM.CaseK" #-}
          case Blocked_
    blk of
            Blocked{} | [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [()|Con{} <- [Term
    t]] -> ST s (Blocked Term)
    stuck -- we might as well check the blocking tag first
            Blocked_
    _ -> case Term
    t of
              -- Case: suc constructor
              Con ConHead
    c ConInfo
    ci [] | ConHead -> Bool
    isSuc ConHead
    c -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchSuc (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl

              -- Case: constructor
              Con ConHead
    c ConInfo
    ci [] -> ConHead
    -> ConInfo -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon ConHead
    c ConInfo
    ci (Spine s -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Spine s
    spine) (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl

              -- Case: non-empty elims. We can get here from a fallback (which builds a value without
              -- shifting arguments onto spine)
              Con ConHead
    c ConInfo
    ci Elims
    es -> do
                spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                runAM (evalValue blk (Con c ci []) emptyEnv (spine' <> spine) ctrl0)
              -- Case: natural number literals. Literal natural number patterns are translated to
              -- suc-matches, so there is no need to try matchLit.
              Lit (LitNat Integer
    0) -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchLitZero  (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl
              Lit (LitNat Integer
    n) -> Integer -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchLitSuc Integer
    n (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl

              -- Case: literal
              Lit Literal
    l -> Literal -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchLit Literal
    l (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl

              -- Case: hcomp
              Def QName
    q [] | Maybe FastCompiledClauses -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe FastCompiledClauses -> Bool)
    -> Maybe FastCompiledClauses -> Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. QName -> FastCase c -> Maybe c
    lookupCon QName
    q FastCase FastCompiledClauses
    bs -> QName -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon' QName
    q (Spine s -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Spine s
    spine) (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f MatchStack s
    stack [ControlFrame s]
    ctrl
              Def QName
    q Elims
    es | Maybe FastCompiledClauses -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe FastCompiledClauses -> Bool)
    -> Maybe FastCompiledClauses -> Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. QName -> FastCase c -> Maybe c
    lookupCon QName
    q FastCase FastCompiledClauses
    bs -> do
                spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                runAM (evalValue blk (Def q []) emptyEnv (spine' <> spine) ctrl0)

              -- Case: not constructor or literal. In this case we are stuck.
              Term
    _ -> ST s (Blocked Term)
    stuck
          where
            -- If ffallThrough is set we take the catch-all (if any) rather than being stuck. I think
            -- this happens for partial functions with --cubical (@saizan: is this true?).
            stuck :: ST s (Blocked Term)
    stuck | FastCase FastCompiledClauses -> Bool
    forall c. FastCase c -> Bool
    ffallThrough FastCase FastCompiledClauses
    bs = ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall ST s (Blocked Term)
    reallyStuck
                  | Bool
    otherwise       = ST s (Blocked Term)
    reallyStuck

            reallyStuck :: ST s (Blocked Term)
    reallyStuck = do
                -- Compute new reason for being stuck. See Agda.Syntax.Internal.stuckOn for the logic.
                blk' <- case Blocked_
    blk of
                          Blocked{}      -> Blocked_ -> ST s Blocked_
    forall a. a -> ST s a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocked_
    blk
                          NotBlocked NotBlocked' Term
    r ()
    _ -> Closure s -> ST s Term
    forall s. Closure s -> ST s Term
    decodeClosure_ Closure s
    cl ST s Term -> (Term -> Blocked_) -> ST s Blocked_
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Term
    v -> NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (Elim -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i Term
    v) NotBlocked' Term
    r) ()
                stuckMatch blk' stack ctrl

            -- This the spine at this point in the matching. A catch-all match doesn't change the spine.
            catchallSpine :: Spine s
    catchallSpine = Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> [Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> Arg (Pointer s) -> Elim' (Pointer s)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Pointer s -> Arg (Pointer s)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i Pointer s
    p] Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1
              where p :: Pointer s
    p = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk Closure s
    cl -- cl is already a value so no need to thunk it.

            -- Push catch-all frame on the match stack if there is a catch-all (and we're not taking it
            -- right now).
            catchallStack :: MatchStack s
    catchallStack = case FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. FastCase c -> Maybe c
    fcatchallBranch FastCase FastCompiledClauses
    bs of
              Maybe FastCompiledClauses
    Nothing -> MatchStack s
    stack
              Just FastCompiledClauses
    cc -> FastCompiledClauses -> Spine s -> CatchallFrame s
    forall s. FastCompiledClauses -> Spine s -> CatchallFrame s
    Catchall FastCompiledClauses
    cc Spine s
    catchallSpine CatchallFrame s -> MatchStack s -> MatchStack s
    forall s. CatchallFrame s -> MatchStack s -> MatchStack s
    >: MatchStack s
    stack

            -- The matchX functions below all take an extra argument which is what to do if there is no
            -- appropriate branch in the case tree. ifJust is maybe with a different argument order
            -- letting you chain a bunch if maybe matches in if-then-elseif fashion.
            (Maybe a
    m ifJust :: Maybe a -> (a -> b) -> b -> b
    `ifJust` a -> b
    f) b
    z = b -> (a -> b) -> Maybe a -> b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe b
    z a -> b
    f Maybe a
    m

            -- Matching constructor: Switch to the Match state, inserting the constructor arguments in
            -- the spine between spine0 and spine1.
            matchCon :: ConHead
    -> ConInfo -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon ConHead
    c ConInfo
    ci Int
    ar = QName -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon' (ConHead -> QName
    conName ConHead
    c) Int
    ar
            matchCon' :: QName -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon' QName
    q Int
    ar = QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. QName -> FastCase c -> Maybe c
    lookupCon QName
    q FastCase FastCompiledClauses
    bs Maybe FastCompiledClauses
    -> (FastCompiledClauses -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    -> ST s (Blocked Term)
    forall {a} {b}. Maybe a -> (a -> b) -> b -> b
    `ifJust` \ FastCompiledClauses
    cc ->
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1) MatchStack s
    catchallStack [ControlFrame s]
    ctrl)

            -- Catch-all: Don't add a Catchall to the match stack since this _is_ the catch-all.
            matchCatchall :: ST s (Blocked Term) -> ST s (Blocked Term)
    matchCatchall = FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. FastCase c -> Maybe c
    fcatchallBranch FastCase FastCompiledClauses
    bs Maybe FastCompiledClauses
    -> (FastCompiledClauses -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    -> ST s (Blocked Term)
    forall {a} {b}. Maybe a -> (a -> b) -> b -> b
    `ifJust` \ FastCompiledClauses
    cc ->
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc Spine s
    catchallSpine MatchStack s
    stack [ControlFrame s]
    ctrl)

            -- Matching literal: Switch to the Match state. There are no arguments to add to the spine.
            matchLit :: Literal -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchLit Literal
    l = Literal
    -> Map Literal FastCompiledClauses -> Maybe FastCompiledClauses
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Literal
    l (FastCase FastCompiledClauses -> Map Literal FastCompiledClauses
    forall c. FastCase c -> Map Literal c
    flitBranches FastCase FastCompiledClauses
    bs) Maybe FastCompiledClauses
    -> (FastCompiledClauses -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    -> ST s (Blocked Term)
    forall {a} {b}. Maybe a -> (a -> b) -> b -> b
    `ifJust` \ FastCompiledClauses
    cc ->
              AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1) MatchStack s
    catchallStack [ControlFrame s]
    ctrl)

            -- Matching a 'suc' constructor: Insert the argument in the spine.
            matchSuc :: ST s (Blocked Term) -> ST s (Blocked Term)
    matchSuc = FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. FastCase c -> Maybe c
    fsucBranch FastCase FastCompiledClauses
    bs Maybe FastCompiledClauses
    -> (FastCompiledClauses -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    -> ST s (Blocked Term)
    forall {a} {b}. Maybe a -> (a -> b) -> b -> b
    `ifJust` \ FastCompiledClauses
    cc ->
                AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1) MatchStack s
    catchallStack [ControlFrame s]
    ctrl)

            -- Matching a non-zero natural number literal: Subtract one from the literal and
            -- insert it in the spine for the Match state.
            matchLitSuc :: Integer -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchLitSuc Integer
    n = FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. FastCase c -> Maybe c
    fsucBranch FastCase FastCompiledClauses
    bs Maybe FastCompiledClauses
    -> (FastCompiledClauses -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    -> ST s (Blocked Term)
    forall {a} {b}. Maybe a -> (a -> b) -> b -> b
    `ifJust` \ FastCompiledClauses
    cc ->
                AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> [Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> Arg (Pointer s) -> Elim' (Pointer s)
    forall a b. (a -> b) -> a -> b
    $ Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg Pointer s
    arg] Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1) MatchStack s
    catchallStack [ControlFrame s]
    ctrl)
              where n' :: Integer
    n'  = Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
                    arg :: Pointer s
    arg = Closure s -> Pointer s
    forall s. Closure s -> Pointer s
    pureThunk (Closure s -> Pointer s) -> Closure s -> Pointer s
    forall a b. (a -> b) -> a -> b
    $ Term -> Env s -> Spine s -> Closure s
    forall {s}. Term -> Env s -> Spine s -> Closure s
    trueValue (Literal -> Term
    Lit (Literal -> Term) -> Literal -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Literal
    LitNat Integer
    n') Env s
    forall s. Env s
    emptyEnv []

            -- Matching a literal 0. Simply calls matchCon with the zero constructor.
            matchLitZero :: ST s (Blocked Term) -> ST s (Blocked Term)
    matchLitZero = ConHead
    -> ConInfo -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
    matchCon (ConHead -> Maybe ConHead -> ConHead
    forall a. a -> Maybe a -> a
    fromMaybe ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe ConHead
    zero) ConInfo
    ConOSystem Int
    0
                                -- If we have a nat literal we have builtin zero.

        -- Case: Match state. Here we look at the case tree and take the appropriate action:
        --   - FFail: stuck
        --   - FDone: evaluate body
        --   - FEta: eta expand argument
        --   - FCase on projection: pick corresponding branch and keep matching
        --   - FCase on argument: push CaseK frame on control stack and evaluate argument
        runAM' (Match QName
    f FastCompiledClauses
    cc Spine s
    spine MatchStack s
    stack [ControlFrame s]
    ctrl) = {-# SCC "runAM.Match" #-}
          case FastCompiledClauses
    cc of
            -- Absurd match. You can get here for open terms.
            FastCompiledClauses
    FFail -> Blocked_ -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    stuckMatch (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    AbsurdMatch ()) MatchStack s
    stack [ControlFrame s]
    ctrl

            -- Matching complete. Compute the environment for the body and switch to the Eval state.
            FDone [Arg VerboseKey]
    xs Term
    body -> do
                -- Don't ask me why, but not being strict in the spine causes a memory leak.
                let ([Arg VerboseKey]
    zs, Env s
    env, !Spine s
    spine') = [Arg VerboseKey] -> Spine s -> ([Arg VerboseKey], Env s, Spine s)
    forall s.
    [Arg VerboseKey] -> Spine s -> ([Arg VerboseKey], Env s, Spine s)
    buildEnv [Arg VerboseKey]
    xs Spine s
    spine
                AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> [ControlFrame s] -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled ([Arg VerboseKey] -> Term -> Term
    lams [Arg VerboseKey]
    zs Term
    body) Env s
    env Spine s
    spine') [ControlFrame s]
    ctrl)

            -- A record pattern match. This does not block evaluation (since that would violate eta
            -- equality), so in this case we replace the argument with its projections in the spine and
            -- keep matching.
            FEta Int
    n [Arg QName]
    fs FastCompiledClauses
    cc Maybe FastCompiledClauses
    ca ->
              case Int -> Spine s -> (Spine s, Spine s)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n Spine s
    spine of                           -- Question: add lambda here? doesn't
                (Spine s
    _, [])                    -> NotBlocked' Term -> ST s (Blocked Term)
    done NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied -- matter for equality, but might for
                (Spine s
    spine0, Apply Arg (Pointer s)
    e : Spine s
    spine1) -> do                -- rewriting or 'with'.
                  -- Replace e by its projections in the spine. And don't forget a
                  -- Catchall frame if there's a catch-all.
                  let projClosure :: Arg QName -> Closure s
    projClosure (Arg ArgInfo
    ai QName
    f) = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled (Int -> Elims -> Term
    Var Int
    0 []) (Pointer s -> Env s -> Env s
    forall s. Pointer s -> Env s -> Env s
    extendEnv (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    e) Env s
    forall s. Env s
    emptyEnv) [ProjOrigin -> QName -> Elim' (Pointer s)
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
                  projs <- (Arg QName -> ST s (Pointer s)) -> [Arg QName] -> ST s [Pointer s]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Closure s -> ST s (Pointer s)
    forall s. Closure s -> ST s (Pointer s)
    createThunk (Closure s -> ST s (Pointer s))
    -> (Arg QName -> Closure s) -> Arg QName -> ST s (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg QName -> Closure s
    projClosure) [Arg QName]
    fs
                  let spine' = Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> (Pointer s -> Elim' (Pointer s)) -> [Pointer s] -> Spine s
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg (Pointer s) -> Elim' (Pointer s)
    forall a. Arg a -> Elim' a
    Apply (Arg (Pointer s) -> Elim' (Pointer s))
    -> (Pointer s -> Arg (Pointer s)) -> Pointer s -> Elim' (Pointer s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pointer s -> Arg (Pointer s)
    forall a. a -> Arg a
    defaultArg) [Pointer s]
    projs Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1
                      stack' = Maybe FastCompiledClauses
    -> MatchStack s
    -> (FastCompiledClauses -> MatchStack s)
    -> MatchStack s
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe FastCompiledClauses
    ca MatchStack s
    stack ((FastCompiledClauses -> MatchStack s) -> MatchStack s)
    -> (FastCompiledClauses -> MatchStack s) -> MatchStack s
    forall a b. (a -> b) -> a -> b
    $ \ FastCompiledClauses
    cc -> FastCompiledClauses -> Spine s -> CatchallFrame s
    forall s. FastCompiledClauses -> Spine s -> CatchallFrame s
    Catchall FastCompiledClauses
    cc Spine s
    spine CatchallFrame s -> MatchStack s -> MatchStack s
    forall s. CatchallFrame s -> MatchStack s -> MatchStack s
    >: MatchStack s
    stack
                  runAM (Match f cc spine' stack' ctrl)
                (Spine s, Spine s)
    _ -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Split on nth elimination in the spine. Can be either a regular split or a copattern
            -- split.
            FCase Int
    n FastCase FastCompiledClauses
    bs ->
              case Int -> Spine s -> (Spine s, Spine s)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n Spine s
    spine of
                -- If the nth elimination is not given, we're stuck.
                (Spine s
    _, []) -> NotBlocked' Term -> ST s (Blocked Term)
    done NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied
                -- Apply elim: push the current match on the control stack and evaluate the argument
                (Spine s
    spine0, Apply Arg (Pointer s)
    e : Spine s
    spine1) ->
                  Pointer s -> Spine s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Arg (Pointer s) -> Pointer s
    forall e. Arg e -> e
    unArg Arg (Pointer s)
    e) [] ([ControlFrame s] -> ST s (Blocked Term))
    -> [ControlFrame s] -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ QName
    -> ArgInfo
    -> FastCase FastCompiledClauses
    -> Spine s
    -> Spine s
    -> MatchStack s
    -> ControlFrame s
    forall s.
    QName
    -> ArgInfo
    -> FastCase FastCompiledClauses
    -> Spine s
    -> Spine s
    -> MatchStack s
    -> ControlFrame s
    CaseK QName
    f (Arg (Pointer s) -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg (Pointer s)
    e) FastCase FastCompiledClauses
    bs Spine s
    spine0 Spine s
    spine1 MatchStack s
    stack ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl
                -- Projection elim: in this case we must be in a copattern split and find the projection
                -- in the case tree and keep going. If it's not there it might be because it's not the
                -- original projection (issue #2265). If so look up the original projection instead.
                -- That _really_ should be there since copattern splits cannot be partial. Except of
                -- course, the user might still have written a partial function so we should check
                -- partialDefs before throwing an impossible (#3012).
                (Spine s
    spine0, Proj ProjOrigin
    o QName
    p : Spine s
    spine1) ->
                  case QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. QName -> FastCase c -> Maybe c
    lookupCon QName
    p FastCase FastCompiledClauses
    bs Maybe FastCompiledClauses
    -> Maybe FastCompiledClauses -> Maybe FastCompiledClauses
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> ((QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
    forall c. QName -> FastCase c -> Maybe c
    `lookupCon` FastCase FastCompiledClauses
    bs) (QName -> Maybe FastCompiledClauses)
    -> Maybe QName -> Maybe FastCompiledClauses
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe QName
    op) of
                    Maybe FastCompiledClauses
    Nothing
                      | QName
    f QName -> Set QName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set QName
    partialDefs -> Blocked_ -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    stuckMatch (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    f) ()) MatchStack s
    stack [ControlFrame s]
    ctrl
                      | Bool
    otherwise          -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Just FastCompiledClauses
    cc -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> [ControlFrame s]
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1) MatchStack s
    stack [ControlFrame s]
    ctrl)
                  where CFun{ cfunProjection :: CompactDefn -> Maybe QName
    cfunProjection = Maybe QName
    op } = CompactDef -> CompactDefn
    cdefDef (QName -> CompactDef
    constInfo QName
    p)
                (Spine s
    _, IApply{} : Spine s
    _) -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Paths cannot be defined by pattern matching
          where done :: NotBlocked' Term -> ST s (Blocked Term)
    done NotBlocked' Term
    why = Blocked_ -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    stuckMatch (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    why ()) MatchStack s
    stack [ControlFrame s]
    ctrl

        -- 'evalPointerAM p spine ctrl'. Evaluate the closure pointed to by 'p' applied to 'spine' with
        -- the control stack 'ctrl'. If 'p' points to an unevaluated thunk, a 'BlackHole' is written to
        -- the pointer and an 'UpdateThunk' frame is pushed to the control stack. In this case the
        -- application to the spine has to be deferred until after the update through an 'ApplyK' frame.
        evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
        evalPointerAM :: forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM (Pure Closure s
    cl)   Spine s
    spine ControlStack s
    ctrl = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Closure s -> Spine s -> Closure s
    forall s. Closure s -> Spine s -> Closure s
    clApply Closure s
    cl Spine s
    spine) ControlStack s
    ctrl)
        evalPointerAM (Pointer STPointer s
    p) Spine s
    spine ControlStack s
    ctrl = STPointer s -> ST s (Thunk (Closure s))
    forall s. STPointer s -> ST s (Thunk (Closure s))
    readPointer STPointer s
    p ST s (Thunk (Closure s))
    -> (Thunk (Closure s) -> ST s (Blocked Term))
    -> ST s (Blocked Term)
    forall a b. ST s a -> (a -> ST s b) -> ST s b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
          Thunk (Closure s)
    BlackHole -> ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Thunk cl :: Closure s
    cl@(Closure IsValue
    Unevaled Term
    _ Env s
    _ Spine s
    _) | Bool
    callByNeed -> do
            STPointer s -> ST s ()
    forall s. STPointer s -> ST s ()
    blackHole STPointer s
    p
            AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval Closure s
    cl (ControlStack s -> AM s) -> ControlStack s -> AM s
    forall a b. (a -> b) -> a -> b
    $ STPointer s -> ControlStack s -> ControlStack s
    forall s. STPointer s -> ControlStack s -> ControlStack s
    updateThunkCtrl STPointer s
    p (ControlStack s -> ControlStack s)
    -> ControlStack s -> ControlStack s
    forall a b. (a -> b) -> a -> b
    $ [Spine s -> ControlFrame s
    forall s. Spine s -> ControlFrame s
    ApplyK Spine s
    spine | Bool -> Bool
    not (Spine s -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Spine s
    spine)] ControlStack s -> ControlStack s -> ControlStack s
    forall a. [a] -> [a] -> [a]
    ++ ControlStack s
    ctrl)
          Thunk Closure s
    cl -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Closure s -> Spine s -> Closure s
    forall s. Closure s -> Spine s -> Closure s
    clApply Closure s
    cl Spine s
    spine) ControlStack s
    ctrl)

        -- 'evalIApplyAM spine ctrl fallback' checks if any 'IApply x y r' has a canonical 'r' (i.e. 0 or 1),
        -- in that case continues evaluating 'x' or 'y' with the rest of 'spine' and same 'ctrl'.
        -- If no such 'IApply' is found we continue with 'fallback'.
        evalIApplyAM :: Spine s -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
        evalIApplyAM :: forall s.
    Spine s
    -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
    evalIApplyAM Spine s
    es ControlStack s
    ctrl ST s (Blocked Term)
    fallback = Spine s -> ST s (Blocked Term)
    go Spine s
    es
          where
            -- written as a worker/wrapper to possibly trigger some
            -- specialization wrt fallback
            go :: Spine s -> ST s (Blocked Term)
    go []                  = ST s (Blocked Term)
    fallback
            go (IApply Pointer s
    x Pointer s
    y Pointer s
    r : Spine s
    es) = do
              br <- Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Pointer s
    r [] []
              case iview $ ignoreBlocking br of
                IntervalView
    IZero -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Pointer s
    x Spine s
    es ControlStack s
    ctrl
                IntervalView
    IOne  -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Pointer s
    y Spine s
    es ControlStack s
    ctrl
                IntervalView
    _     -> (Blocked Term -> Blocked Term -> Blocked Term
    forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* Blocked Term
    br) (Blocked Term -> Blocked Term)
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Spine s -> ST s (Blocked Term)
    go Spine s
    es
            go (Elim' (Pointer s)
    e : Spine s
    es) = Spine s -> ST s (Blocked Term)
    go Spine s
    es

        -- Normalise the spine and apply the closure to the result. The closure must be a value closure.
        normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
        normaliseArgsAM :: forall s.
    Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM Closure s
    cl []    ControlStack s
    ctrl = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval Closure s
    cl ControlStack s
    ctrl)  -- nothing to do
        normaliseArgsAM Closure s
    cl [Elim' (Pointer s)]
    spine ControlStack s
    ctrl =
          case Carrier (SpineContext s)
    -> Maybe (Element (SpineContext s), SpineContext s)
    forall z. Zipper z => Carrier z -> Maybe (Element z, z)
    firstHole [Elim' (Pointer s)]
    Carrier (SpineContext s)
    spine of -- v Only projections, nothing to do. Note clApply_ and not clApply (or we'd loop)
            Maybe (Element (SpineContext s), SpineContext s)
    Nothing       -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Closure s -> [Elim' (Pointer s)] -> Closure s
    forall s. Closure s -> Spine s -> Closure s
    clApply_ Closure s
    cl [Elim' (Pointer s)]
    spine) ControlStack s
    ctrl)
            Just (Element (SpineContext s)
    p, SpineContext s
    cxt) -> Pointer s
    -> [Elim' (Pointer s)] -> ControlStack s -> ST s (Blocked Term)
    forall s.
    Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    evalPointerAM Element (SpineContext s)
    Pointer s
    p [] (ControlFrame s
    forall s. ControlFrame s
    NormaliseK ControlFrame s -> ControlStack s -> ControlStack s
    forall a. a -> [a] -> [a]
    : Closure s -> SpineContext s -> ControlFrame s
    forall s. Closure s -> SpineContext s -> ControlFrame s
    ArgK Closure s
    cl SpineContext s
    cxt ControlFrame s -> ControlStack s -> ControlStack s
    forall a. a -> [a] -> [a]
    : ControlStack s
    ctrl)

        -- Fall back to slow reduction. This happens if we encounter a definition that's not supported
        -- by the machine (like a primitive function that does not work on literals), or a term that is
        -- not supported (Level and Sort at the moment). In this case we decode the current
        -- focus to a 'Term', call slow reduction and pack up the result in a value closure. If the top
        -- of the control stack is a 'NormaliseK' and the focus is a value closure (i.e. already in
        -- weak-head normal form) we call 'slowNormaliseArgs' and pop the 'NormaliseK' frame. Otherwise
        -- we use 'slowReduceTerm' to compute a weak-head normal form.
        fallbackAM :: AM s -> ST s (Blocked Term)
        fallbackAM :: forall s. AM s -> ST s (Blocked Term)
    fallbackAM (Eval Closure s
    c ControlStack s
    ctrl) = do
            v <- Closure s -> ST s Term
    forall s. Closure s -> ST s Term
    decodeClosure_ Closure s
    c
            runAM (mkValue $ runReduce $ slow v)
          where mkValue :: Blocked Term -> AM s
    mkValue Blocked Term
    b = Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    forall {s}.
    Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalValue (() () -> Blocked Term -> Blocked_
    forall a b. a -> Blocked' Term b -> Blocked' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked Term
    b) (Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    b) Env s
    forall s. Env s
    emptyEnv [] ControlStack s
    ctrl'
                (Term -> ReduceM (Blocked Term)
    slow, ControlStack s
    ctrl') = case ControlStack s
    ctrl of
                  ControlFrame s
    NormaliseK : ControlStack s
    ctrl'
                    | Value{} <- Closure s -> IsValue
    forall s. Closure s -> IsValue
    isValue Closure s
    c -> (Term -> Blocked Term
    forall a t. a -> Blocked' t a
    notBlocked (Term -> Blocked Term)
    -> (Term -> ReduceM Term) -> Term -> ReduceM (Blocked Term)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Term -> ReduceM Term
    slowNormaliseArgs, ControlStack s
    ctrl')
                  ControlStack s
    _                        -> (Term -> ReduceM (Blocked Term)
    slowReduceTerm, ControlStack s
    ctrl)
        fallbackAM AM s
    _ = ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Applying rewrite rules to the current focus. This needs to decode the current focus, call
        -- rewriting and pack the result back up in a closure. In case some rewrite rules actually fired
        -- the next state is an unevaluated closure, otherwise it's a value closure.
        rewriteAM :: AM s -> ST s (Blocked Term)
        rewriteAM :: forall s. AM s -> ST s (Blocked Term)
    rewriteAM s :: AM s
    s@(Eval (Closure (Value Blocked_
    blk) Term
    t Env s
    env Spine s
    spine) ControlStack s
    ctrl)
          | RewriteRules -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null RewriteRules
    rewr = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM AM s
    s
          | Bool
    otherwise = Doc -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a. Doc -> a -> a
    traceDoc (Doc
    "R" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> AM s -> Doc
    forall a. Pretty a => a -> Doc
    pretty AM s
    s) (ST s (Blocked Term) -> ST s (Blocked Term))
    -> ST s (Blocked Term) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ do
            v0 <- Closure s -> ST s Term
    forall s. Closure s -> ST s Term
    decodeClosure_ (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled Term
    t Env s
    env [])
            es <- decodeSpine spine
            case runReduce (rewrite blk (applyE v0) rewr es) of
              NoReduction Blocked Term
    b    -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    forall {s}.
    Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalValue (() () -> Blocked Term -> Blocked_
    forall a b. a -> Blocked' Term b -> Blocked' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked Term
    b) (Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    b) Env s
    forall s. Env s
    emptyEnv [] ControlStack s
    ctrl)
              YesReduction Simplification
    _ Term
    v -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Term -> Env s -> Spine s -> ControlStack s -> AM s
    forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalClosure Term
    v Env s
    forall s. Env s
    emptyEnv [] ControlStack s
    ctrl)
          where rewr :: RewriteRules
    rewr = case Term
    t of
                         Def QName
    f []   -> QName -> RewriteRules
    rewriteRules QName
    f
                         Con ConHead
    c ConInfo
    _ [] -> QName -> RewriteRules
    rewriteRules (ConHead -> QName
    conName ConHead
    c)
                         Term
    _          -> RewriteRules
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        rewriteAM AM s
    _ =
          ST s (Blocked Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Add a NatSucK frame to the control stack. Pack consecutive suc's into a single frame.
        sucCtrl :: ControlStack s -> ControlStack s
        sucCtrl :: forall s. ControlStack s -> ControlStack s
    sucCtrl (NatSucK !Integer
    n : [ControlFrame s]
    ctrl) = Integer -> ControlFrame s
    forall s. Integer -> ControlFrame s
    NatSucK (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl
        sucCtrl               [ControlFrame s]
    ctrl  = Integer -> ControlFrame s
    forall s. Integer -> ControlFrame s
    NatSucK Integer
    1 ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl

        -- Add a UpdateThunk frame to the control stack. Pack consecutive updates into a single frame.
        updateThunkCtrl :: STPointer s -> ControlStack s -> ControlStack s
        updateThunkCtrl :: forall s. STPointer s -> ControlStack s -> ControlStack s
    updateThunkCtrl STPointer s
    p (UpdateThunk [STPointer s]
    ps : [ControlFrame s]
    ctrl) = [STPointer s] -> ControlFrame s
    forall s. [STPointer s] -> ControlFrame s
    UpdateThunk (STPointer s
    p STPointer s -> [STPointer s] -> [STPointer s]
    forall a. a -> [a] -> [a]
    : [STPointer s]
    ps) ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl
        updateThunkCtrl STPointer s
    p                   [ControlFrame s]
    ctrl  = [STPointer s] -> ControlFrame s
    forall s. [STPointer s] -> ControlFrame s
    UpdateThunk [STPointer s
    p] ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    ctrl

        -- When matching is stuck we return the closure from the 'MatchStack' with the appropriate
        -- 'IsValue' set.
        stuckMatch :: Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
        stuckMatch :: forall s.
    Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    stuckMatch Blocked_
    blk ([CatchallFrame s]
    _ :> Closure s
    cl) ControlStack s
    ctrl = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue Blocked_
    blk Closure s
    cl) ControlStack s
    ctrl)

        -- On a mismatch we find the next 'Catchall' on the control stack and
        -- continue matching from there. If there isn't one we get an incomplete
        -- matching error (or get stuck if the function is marked partial).
        failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
        failedMatch :: forall s.
    QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch QName
    f (Catchall FastCompiledClauses
    cc Spine s
    spine : [CatchallFrame s]
    stack :> Closure s
    cl) ControlStack s
    ctrl = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    forall s.
    QName
    -> FastCompiledClauses
    -> Spine s
    -> MatchStack s
    -> ControlStack s
    -> AM s
    Match QName
    f FastCompiledClauses
    cc Spine s
    spine ([CatchallFrame s]
    stack [CatchallFrame s] -> Closure s -> MatchStack s
    forall s. [CatchallFrame s] -> Closure s -> MatchStack s
    :> Closure s
    cl) ControlStack s
    ctrl)
        failedMatch QName
    f ([] :> Closure s
    cl) ControlStack s
    ctrl
            -- Bad work-around for #3870: don't fail hard during instance search.
          | Bool
    speculative          = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    f) ()) Closure s
    cl) ControlStack s
    ctrl)
          | QName
    f QName -> Set QName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set QName
    partialDefs = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    f) ()) Closure s
    cl) ControlStack s
    ctrl)
          | Bool
    otherwise            = AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM (Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (Blocked_ -> Closure s -> Closure s
    forall {s}. Blocked_ -> Closure s -> Closure s
    mkValue (NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()) Closure s
    cl) ControlStack s
    ctrl)  -- See #5396

        -- Some helper functions to build machine states and closures.
        evalClosure :: Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalClosure Term
    t Env s
    env Spine s
    spine = Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure IsValue
    Unevaled Term
    t Env s
    env Spine s
    spine)
        evalValue :: Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalValue Blocked_
    b Term
    t Env s
    env Spine s
    spine = Closure s -> ControlStack s -> AM s
    forall s. Closure s -> ControlStack s -> AM s
    Eval (IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value Blocked_
    b) Term
    t Env s
    env Spine s
    spine)
        evalTrueValue :: Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalTrueValue           = Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    forall {s}.
    Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    evalValue (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s)
    -> Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
    forall a b. (a -> b) -> a -> b
    $ () -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()
        trueValue :: Term -> Env s -> Spine s -> Closure s
    trueValue Term
    t Env s
    env Spine s
    spine   = IsValue -> Term -> Env s -> Spine s -> Closure s
    forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
    Closure (Blocked_ -> IsValue
    Value (Blocked_ -> IsValue) -> Blocked_ -> IsValue
    forall a b. (a -> b) -> a -> b
    $ () -> Blocked_
    forall a t. a -> Blocked' t a
    notBlocked ()) Term
    t Env s
    env Spine s
    spine
        mkValue :: Blocked_ -> Closure s -> Closure s
    mkValue Blocked_
    b               = IsValue -> Closure s -> Closure s
    forall s. IsValue -> Closure s -> Closure s
    setIsValue (Blocked_ -> IsValue
    Value Blocked_
    b)

        -- Building lambdas
        lams :: [Arg String] -> Term -> Term
        lams :: [Arg VerboseKey] -> Term -> Term
    lams [Arg VerboseKey]
    xs Term
    t = (Arg VerboseKey -> Term -> Term)
    -> Term -> [Arg VerboseKey] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Arg VerboseKey -> Term -> Term
    lam Term
    t [Arg VerboseKey]
    xs

        lam :: Arg String -> Term -> Term
        lam :: Arg VerboseKey -> Term -> Term
    lam Arg VerboseKey
    x Term
    t = ArgInfo -> Abs Term -> Term
    Lam (Arg VerboseKey -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg VerboseKey
    x) (VerboseKey -> Term -> Abs Term
    forall a. VerboseKey -> a -> Abs a
    Abs (Arg VerboseKey -> VerboseKey
    forall e. Arg e -> e
    unArg Arg VerboseKey
    x) Term
    t)

    -- Pretty printing --------------------------------------------------------

    instance Pretty a => Pretty (FastCase a) where
      prettyPrec :: Int -> FastCase a -> Doc
    prettyPrec Int
    p (FBranches Bool
    _cop Map NameId a
    cs Maybe a
    suc Map Literal a
    ls Maybe a
    m Bool
    _) =
        Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (Map NameId a -> [Doc]
    forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ Map NameId a
    cs [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Map Literal a -> [Doc]
    forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ Map Literal a
    ls [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Maybe a -> [Doc]
    forall {a}. Pretty a => Maybe a -> [Doc]
    prSuc Maybe a
    suc [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Maybe a -> [Doc]
    forall {a}. Pretty a => Maybe a -> [Doc]
    prC Maybe a
    m)
        where
          prC :: Maybe a -> [Doc]
    prC Maybe a
    Nothing = []
          prC (Just a
    x) = [Doc
    "_ ->" Doc -> Doc -> Doc
    <?> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    x]

          prSuc :: Maybe a -> [Doc]
    prSuc Maybe a
    Nothing  = []
          prSuc (Just a
    x) = [Doc
    "suc ->" Doc -> Doc -> Doc
    <?> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    x]

    instance Pretty FastCompiledClauses where
      pretty :: FastCompiledClauses -> Doc
    pretty (FDone [Arg VerboseKey]
    xs Term
    t) = (Doc
    "done" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Arg VerboseKey] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Arg VerboseKey]
    xs) Doc -> Doc -> Doc
    <?> Int -> Term -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    10 Term
    t
      pretty FastCompiledClauses
    FFail        = Doc
    "fail"
      pretty (FEta Int
    n [Arg QName]
    _ FastCompiledClauses
    cc Maybe FastCompiledClauses
    ca) =
        VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (VerboseKey
    "eta " VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Int
    n VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    " of") Doc -> Doc -> Doc
    <?>
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (Doc
    "{} ->" Doc -> Doc -> Doc
    <?> FastCompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty FastCompiledClauses
    cc Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :
                [ Doc
    "_ ->" Doc -> Doc -> Doc
    <?> FastCompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty FastCompiledClauses
    cc | Just FastCompiledClauses
    cc <- [Maybe FastCompiledClauses
    ca] ])
      pretty (FCase Int
    n FastCase FastCompiledClauses
    bs) | FastCase FastCompiledClauses -> Bool
    forall c. FastCase c -> Bool
    fprojPatterns FastCase FastCompiledClauses
    bs =
        [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (VerboseKey -> Doc) -> VerboseKey -> Doc
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "project " VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Int
    n
            , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ FastCase FastCompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty FastCase FastCompiledClauses
    bs
            ]
      pretty (FCase Int
    n FastCase FastCompiledClauses
    bs) =
        VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (VerboseKey
    "case " VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Int
    n VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    " of") Doc -> Doc -> Doc
    <?> FastCase FastCompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty FastCase FastCompiledClauses
    bs

    instance Pretty a => Pretty (Thunk a) where
      prettyPrec :: Int -> Thunk a -> Doc
    prettyPrec Int
    _ Thunk a
    BlackHole  = Doc
    "<BLACKHOLE>"
      prettyPrec Int
    p (Thunk a
    cl) = Int -> a -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p a
    cl

    instance Pretty (Pointer s) where
      prettyPrec :: Int -> Pointer s -> Doc
    prettyPrec Int
    p = Int -> Thunk (Closure s) -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p (Thunk (Closure s) -> Doc)
    -> (Pointer s -> Thunk (Closure s)) -> Pointer s -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pointer s -> Thunk (Closure s)
    forall s. Pointer s -> Thunk (Closure s)
    unsafeDerefPointer

    instance Pretty (Closure s) where
      prettyPrec :: Int -> Closure s -> Doc
    prettyPrec Int
    _ (Closure Value{} (Lit (LitString Text
    unused)) Env s
    _ Spine s
    _)
        | Text
    unused Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    unusedPointerString = Doc
    "_"
      prettyPrec Int
    p (Closure IsValue
    isV Term
    t Env s
    env Spine s
    spine) =
        Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep [ VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text VerboseKey
    tag
                               , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    10 Term
    t
                               , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Pointer s -> Doc) -> [Integer] -> [Pointer s] -> [Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Integer -> Pointer s -> Doc
    forall {a} {a}. (Show a, Pretty a) => a -> a -> Doc
    envEntry [Integer
    0..] (Env s -> [Pointer s]
    forall s. Env s -> [Pointer s]
    envToList Env s
    env)
                               , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Spine s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList Spine s
    spine ]
          where envEntry :: a -> a -> Doc
    envEntry a
    i a
    c = VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (VerboseKey
    "@" VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show a
    i VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    " =") Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    c
                tag :: VerboseKey
    tag = case IsValue
    isV of Value{} -> VerboseKey
    "V"; IsValue
    Unevaled -> VerboseKey
    "E"

    instance Pretty (AM s) where
      prettyPrec :: Int -> AM s -> Doc
    prettyPrec Int
    p (Eval Closure s
    cl ControlStack s
    ctrl)  = Int -> Closure s -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p Closure s
    cl Doc -> Doc -> Doc
    <?> ControlStack s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList ControlStack s
    ctrl
      prettyPrec Int
    p (Match QName
    f FastCompiledClauses
    cc Spine s
    sp MatchStack s
    stack ControlStack s
    ctrl) =
        Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "M" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
                              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Spine s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList Spine s
    sp
                              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> FastCompiledClauses -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    10 FastCompiledClauses
    cc
                              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ MatchStack s -> Doc
    forall a. Pretty a => a -> Doc
    pretty MatchStack s
    stack
                              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ControlStack s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList ControlStack s
    ctrl ]

    instance Pretty (CatchallFrame s) where
      pretty :: CatchallFrame s -> Doc
    pretty Catchall{} = Doc
    "Catchall"

    instance Pretty (MatchStack s) where
      pretty :: MatchStack s -> Doc
    pretty ([] :> Closure s
    _) = Doc
    forall a. Null a => a
    empty
      pretty ([CatchallFrame s]
    ca :> Closure s
    _) = [CatchallFrame s] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [CatchallFrame s]
    ca

    instance Pretty (ControlFrame s) where
      prettyPrec :: Int -> ControlFrame s -> Doc
    prettyPrec Int
    p (CaseK QName
    f ArgInfo
    _ FastCase FastCompiledClauses
    _ [Elim' (Pointer s)]
    _ [Elim' (Pointer s)]
    _ MatchStack s
    mc)       = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Doc
    "CaseK" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (QName -> Name
    qnameName QName
    f)) Doc -> Doc -> Doc
    <?> MatchStack s -> Doc
    forall a. Pretty a => a -> Doc
    pretty MatchStack s
    mc
      prettyPrec Int
    p (ForceK QName
    _ [Elim' (Pointer s)]
    spine0 [Elim' (Pointer s)]
    spine1)   = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ForceK" Doc -> Doc -> Doc
    <?> [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList ([Elim' (Pointer s)]
    spine0 [Elim' (Pointer s)] -> [Elim' (Pointer s)] -> [Elim' (Pointer s)]
    forall a. Semigroup a => a -> a -> a
    <> [Elim' (Pointer s)]
    spine1)
      prettyPrec Int
    p (EraseK QName
    _ [Elim' (Pointer s)]
    sp0 [Elim' (Pointer s)]
    sp1 [Elim' (Pointer s)]
    sp2 [Elim' (Pointer s)]
    sp3) = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "EraseK"
                                                                      , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Elim' (Pointer s)]
    sp0
                                                                      , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Elim' (Pointer s)]
    sp1
                                                                      , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Elim' (Pointer s)]
    sp2
                                                                      , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Elim' (Pointer s)]
    sp3 ]
      prettyPrec Int
    _ (NatSucK Integer
    n)              = VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (VerboseKey
    "+" VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Integer
    n)
      prettyPrec Int
    p (PrimOpK QName
    f [Literal] -> Term
    _ [Literal]
    vs [Pointer s]
    cls Maybe FastCompiledClauses
    _)   = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "PrimOpK" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
                                                                    , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Literal] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Literal]
    vs
                                                                    , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Pointer s] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Pointer s]
    cls ]
      prettyPrec Int
    p (UpdateThunk [STPointer s]
    ps)         = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "UpdateThunk" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> VerboseKey -> Doc
    forall a. VerboseKey -> Doc a
    text (Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show ([STPointer s] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [STPointer s]
    ps))
      prettyPrec Int
    p (ApplyK [Elim' (Pointer s)]
    spine)           = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ApplyK" Doc -> Doc -> Doc
    <?> [Elim' (Pointer s)] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList [Elim' (Pointer s)]
    spine
      prettyPrec Int
    p ControlFrame s
    NormaliseK               = Doc
    "NormaliseK"
      prettyPrec Int
    p (ArgK Closure s
    cl SpineContext s
    _)              = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "ArgK" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Closure s -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    10 Closure s
    cl ]