    {-# 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 Control.Applicative hiding (empty)
    import Control.Monad.ST
    import Control.Monad.ST.Unsafe (unsafeSTToIO, unsafeInterleaveST)

    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.IntMap as IntMap
    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.Internal
    import Agda.Syntax.Common
    import Agda.Syntax.Position
    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.Utils.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
    cdefDelayed        :: Bool
                 , 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 = case Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Definition -> Type
    defType Definition
    def) of
            Prop{} -> Bool
    True
            Sort
    _      -> Bool
    False
      let irr :: Bool
    irr = Bool
    isPrp Bool -> Bool -> Bool
    || ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant (Definition -> ArgInfo
    defArgInfo Definition
    def)

      Bool
    dontReduce <- Bool -> Bool
    not (Bool -> Bool) -> ReduceM Bool -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ReduceM Bool
    forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
    shouldReduceDef (Definition -> QName
    defName Definition
    def)

      CompactDefn
    cdefn <-
        case Definition -> Defn
    theDef Definition
    def of
          Defn
    _ | Bool
    irr Bool -> Bool -> Bool
    || Bool
    dontReduce -> CompactDefn -> ReduceM CompactDefn
    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 (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) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    5 -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CErase
                           | Bool
    otherwise     -> CompactDefn -> ReduceM CompactDefn
    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 (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 (f :: * -> *) a. Applicative f => a -> f a
    pure CCon :: ConHead -> Int -> CompactDefn
    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 -> Maybe Projection
    funProjection = Maybe Projection
    proj} ->
            CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CFun :: FastCompiledClauses -> Maybe QName -> CompactDefn
    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
    <$> Maybe Projection
    proj }
          Function{funClauses :: Defn -> [Clause]
    funClauses = []}      -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          Function{}                     -> CompactDefn -> ReduceM CompactDefn
    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 (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CTyCon
          Record{recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    Nothing}    -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CTyCon
          Datatype{}                     -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Record{}                       -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Axiom{}                        -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          DataOrRecSig{}                 -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          AbstractDefn{}                 -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    CAxiom
          GeneralizableVar{}             -> ReduceM CompactDefn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PrimitiveSort{}                -> CompactDefn -> ReduceM CompactDefn
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CompactDefn
    COther -- TODO
          Primitive{ primName :: Defn -> VerboseKey
    primName = VerboseKey
    name, primCompiled :: Defn -> Maybe CompiledClauses
    primCompiled = Maybe CompiledClauses
    cc } ->
            case VerboseKey
    name of
              -- "primShowInteger"            -- integers are not literals

              -- Natural numbers
              VerboseKey
    "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
    (+)
              VerboseKey
    "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))
              VerboseKey
    "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
    (*)
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
    (<)
              VerboseKey
    "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
              VerboseKey
    "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)
              VerboseKey
    "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
              VerboseKey
    "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
    (<=)
              VerboseKey
    "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
    (==)
              VerboseKey
    "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
    (<)
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "primFloatIsDenormalized"    -> 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
    isDenormalized
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "primFloatToWord64"          -> 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] -> Word64 -> Term
    word (Double -> Word64
    doubleToWord64 Double
    a)
              -- "primFloatToWord64Injective" -- identities are not literals
              VerboseKey
    "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
              VerboseKey
    "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
    (+)
              VerboseKey
    "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 (-)
              VerboseKey
    "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
    (*)
              VerboseKey
    "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
              VerboseKey
    "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
    (/)
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
    (**)
              VerboseKey
    "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
              VerboseKey
    "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
    (==)
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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
              VerboseKey
    "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))
              VerboseKey
    "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)
              VerboseKey
    "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)
              VerboseKey
    "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)
              VerboseKey
    "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)
              VerboseKey
    "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"
              VerboseKey
    "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)
              VerboseKey
    "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)
              VerboseKey
    "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)
              VerboseKey
    "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 AbsolutePath
    _ MetaId
    a, LitMeta AbsolutePath
    _ MetaId
    b] -> Bool -> Term
    bool (MetaId
    b MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    a)
              VerboseKey
    "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 AbsolutePath
    _ MetaId
    a, LitMeta AbsolutePath
    _ MetaId
    b] -> Bool -> Term
    bool (MetaId
    b MetaId -> MetaId -> Bool
    forall a. Ord a => a -> a -> Bool
    < MetaId
    a)
              VerboseKey
    "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 AbsolutePath
    _ MetaId
    a] -> VerboseKey -> Term
    string (MetaId -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow MetaId
    a)

              VerboseKey
    _                            -> CompactDefn -> ReduceM CompactDefn
    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 (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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__

      CompactDef -> ReduceM CompactDef
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompactDef -> ReduceM CompactDef)
    -> CompactDef -> ReduceM CompactDef
    forall a b. (a -> b) -> a -> b
    $
        CompactDef :: Bool -> Bool -> Bool -> CompactDefn -> RewriteRules -> CompactDef
    CompactDef { cdefDelayed :: Bool
    cdefDelayed        = Definition -> Delayed
    defDelayed Definition
    def Delayed -> Delayed -> Bool
    forall a. Eq a => a -> a -> Bool
    == Delayed
    Delayed
                   , cdefNonterminating :: Bool
    cdefNonterminating = Definition -> Bool
    defNonterminating Definition
    def
                   , cdefUnconfirmed :: Bool
    cdefUnconfirmed    = Definition -> Bool
    defTerminationUnconfirmed Definition
    def
                   , cdefDef :: CompactDefn
    cdefDef            = CompactDefn
    cdefn
                   , cdefRewriteRules :: RewriteRules
    cdefRewriteRules   = RewriteRules
    rewr
                   }

    -- 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 :: forall c.
    Bool
    -> Map NameId c
    -> Maybe c
    -> Map Literal c
    -> Maybe c
    -> Bool
    -> FastCase c
    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 (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 (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 (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 (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
      IORef (Map NameId a)
    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
      (QName -> a) -> IO (QName -> a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IO a -> a
    forall a. IO a -> a
    unsafePerformIO (IO a -> a) -> (QName -> IO a) -> QName -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IORef (Map NameId a) -> QName -> IO a
    f' IORef (Map NameId a)
    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)
          Map NameId a
    m <- IORef (Map NameId a) -> IO (Map NameId a)
    forall a. IORef a -> IO a
    readIORef IORef (Map NameId a)
    tbl
          case NameId -> Map NameId a -> Maybe a
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup NameId
    i Map NameId a
    m of
            Just a
    y  -> 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 (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
    /= :: Normalisation -> Normalisation -> Bool
    $c/= :: Normalisation -> Normalisation -> Bool
    == :: Normalisation -> Normalisation -> Bool
    $c== :: Normalisation -> Normalisation -> Bool
    Eq)

    data ReductionFlags = ReductionFlags
      { ReductionFlags -> Bool
    allowNonTerminating :: Bool
      , ReductionFlags -> Bool
    allowUnconfirmed    :: Bool
      , ReductionFlags -> Bool
    hasRewriting        :: Bool }

    -- | 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
      let name :: Term -> ConHead
    name (Con ConHead
    c ConInfo
    _ Elims
    _) = ConHead
    c
          name Term
    _         = ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Maybe ConHead
    zero  <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
    getBuiltin' VerboseKey
    builtinZero
      Maybe ConHead
    suc   <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
    getBuiltin' VerboseKey
    builtinSuc
      Maybe ConHead
    true  <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
    getBuiltin' VerboseKey
    builtinTrue
      Maybe ConHead
    false <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
    getBuiltin' VerboseKey
    builtinFalse
      Maybe ConHead
    refl  <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> ConHead
    name (Maybe Term -> Maybe ConHead)
    -> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
    getBuiltin' VerboseKey
    builtinRefl
      Maybe QName
    force <- (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap PrimFun -> QName
    primFunName (Maybe PrimFun -> Maybe QName)
    -> ReduceM (Maybe PrimFun) -> ReduceM (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe PrimFun)
    forall (m :: * -> *).
    HasBuiltins m =>
    VerboseKey -> m (Maybe PrimFun)
    getPrimitive' VerboseKey
    "primForce"
      Maybe QName
    erase <- (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap PrimFun -> QName
    primFunName (Maybe PrimFun -> Maybe QName)
    -> ReduceM (Maybe PrimFun) -> ReduceM (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseKey -> ReduceM (Maybe PrimFun)
    forall (m :: * -> *).
    HasBuiltins m =>
    VerboseKey -> m (Maybe PrimFun)
    getPrimitive' VerboseKey
    "primErase"
      let bEnv :: BuiltinEnv
    bEnv = BuiltinEnv :: Maybe ConHead
    -> Maybe ConHead
    -> Maybe ConHead
    -> Maybe ConHead
    -> Maybe ConHead
    -> Maybe QName
    -> Maybe QName
    -> BuiltinEnv
    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
    allowedReductions <- (TCEnv -> AllowedReductions) -> ReduceM AllowedReductions
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> AllowedReductions
    envAllowedReductions
      Bool
    rwr <- PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      QName -> CompactDef
    constInfo <- (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
    forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
    unKleisli ((QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef))
    -> (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
    forall a b. (a -> b) -> a -> b
    $ \QName
    f -> do
        Definition
    info <- QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
        RewriteRules
    rewr <- if Bool
    rwr then RewriteRules -> ReduceM RewriteRules
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    RewriteRules -> m RewriteRules
    instantiateRewriteRules (RewriteRules -> ReduceM RewriteRules)
    -> ReduceM RewriteRules -> ReduceM RewriteRules
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> ReduceM RewriteRules
    forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
    getRewriteRulesFor QName
    f
                       else RewriteRules -> ReduceM RewriteRules
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
    compactDef BuiltinEnv
    bEnv Definition
    info RewriteRules
    rewr
      let flags :: ReductionFlags
    flags = ReductionFlags :: Bool -> Bool -> Bool -> ReductionFlags
    ReductionFlags{ allowNonTerminating :: Bool
    allowNonTerminating = AllowedReduction
    NonTerminatingReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowedReductions
                                , allowUnconfirmed :: Bool
    allowUnconfirmed    = AllowedReduction
    UnconfirmedReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    allowedReductions
                                , hasRewriting :: Bool
    hasRewriting        = Bool
    rwr }
      (ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term)
    forall a. (ReduceEnv -> a) -> ReduceM a
    ReduceM ((ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term))
    -> (ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ \ ReduceEnv
    redEnv -> ReduceEnv
    -> BuiltinEnv
    -> (QName -> CompactDef)
    -> Normalisation
    -> ReductionFlags
    -> Term
    -> Blocked Term
    reduceTm ReduceEnv
    redEnv BuiltinEnv
    bEnv ((QName -> CompactDef) -> QName -> CompactDef
    forall a. (QName -> a) -> QName -> a
    memoQName QName -> CompactDef
    constInfo) Normalisation
    norm ReductionFlags
    flags Term
    v

    unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
    unKleisli :: forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
    unKleisli a -> ReduceM b
    f = (ReduceEnv -> a -> b) -> ReduceM (a -> b)
    forall a. (ReduceEnv -> a) -> ReduceM a
    ReduceM ((ReduceEnv -> a -> b) -> ReduceM (a -> b))
    -> (ReduceEnv -> a -> b) -> ReduceM (a -> b)
    forall a b. (a -> b) -> a -> b
    $ \ ReduceEnv
    env a
    x -> ReduceM b -> ReduceEnv -> b
    forall a. ReduceM a -> ReduceEnv -> a
    unReduceM (a -> ReduceM b
    f a
    x) ReduceEnv
    env

    -- * 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
    <$ :: forall a b. a -> Thunk b -> Thunk a
    $c<$ :: forall a b. a -> Thunk b -> Thunk a
    fmap :: forall a b. (a -> b) -> Thunk a -> Thunk b
    $cfmap :: forall a b. (a -> b) -> Thunk a -> Thunk b
    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 (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (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 (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 (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
    /= :: ElimZipper a -> ElimZipper a -> Bool
    $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
    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
    min :: ElimZipper a -> ElimZipper a -> ElimZipper a
    $cmin :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
    max :: ElimZipper a -> ElimZipper a -> ElimZipper a
    $cmax :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
    >= :: 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
    $c< :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
    compare :: ElimZipper a -> ElimZipper a -> Ordering
    $ccompare :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Ordering
    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
    showList :: [ElimZipper a] -> ShowS
    $cshowList :: forall a. Show a => [ElimZipper a] -> ShowS
    show :: ElimZipper a -> VerboseKey
    $cshow :: forall a. Show a => ElimZipper a -> VerboseKey
    showsPrec :: Int -> ElimZipper a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> 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
    <$ :: forall a b. a -> ElimZipper b -> ElimZipper a
    $c<$ :: forall a b. a -> ElimZipper b -> ElimZipper a
    fmap :: forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
    $cfmap :: forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
    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
    product :: forall a. Num a => ElimZipper a -> a
    $cproduct :: forall a. Num a => ElimZipper a -> a
    sum :: forall a. Num a => ElimZipper a -> a
    $csum :: forall a. Num a => ElimZipper a -> a
    minimum :: forall a. Ord a => ElimZipper a -> a
    $cminimum :: forall a. Ord a => ElimZipper a -> a
    maximum :: forall a. Ord a => ElimZipper a -> a
    $cmaximum :: forall a. Ord a => ElimZipper a -> a
    elem :: forall a. Eq a => a -> ElimZipper a -> Bool
    $celem :: forall a. Eq a => a -> ElimZipper a -> Bool
    length :: forall a. ElimZipper a -> Int
    $clength :: forall a. ElimZipper a -> Int
    null :: forall a. ElimZipper a -> Bool
    $cnull :: forall a. ElimZipper a -> Bool
    toList :: forall a. ElimZipper a -> [a]
    $ctoList :: forall a. ElimZipper a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    foldr1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
    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
    $cfoldl :: forall b a. (b -> a -> 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
    $cfoldr :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
    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
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
    fold :: forall m. Monoid m => ElimZipper m -> m
    $cfold :: forall m. Monoid m => ElimZipper m -> m
    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)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    ElimZipper (m a) -> m (ElimZipper a)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    ElimZipper (m a) -> m (ElimZipper a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ElimZipper a -> m (ElimZipper b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ElimZipper a -> m (ElimZipper b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ElimZipper (f a) -> f (ElimZipper a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ElimZipper (f a) -> f (ElimZipper a)
    traverse :: 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)
    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 (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' Term)) -> Spine s -> ST s Elims
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Elim' (Pointer s) -> ST s (Elim' Term)) -> Spine s -> ST s Elims)
    -> ((Pointer s -> ST s Term)
        -> Elim' (Pointer s) -> ST s (Elim' Term))
    -> (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' Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t 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)
    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
        [Term]
    vs <- Env s -> ST s [Term]
    forall s. Env s -> ST s [Term]
    decodeEnv Env s
    env
        Elims
    es <- Spine s -> ST s Elims
    forall s. Spine s -> ST s Elims
    decodeSpine Spine s
    spine
        Blocked Term -> ST s (Blocked Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Blocked Term -> ST s (Blocked Term))
    -> Blocked Term -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([Term] -> Substitution' Term
    forall {a}. [a] -> Substitution' a
    parS [Term]
    vs) Term
    t) Elims
    es Term -> Blocked_ -> Blocked Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked_
    b
      where
        parS :: [a] -> Substitution' a
    parS = (a -> Substitution' a -> Substitution' a)
    -> Substitution' a -> [a] -> Substitution' a
    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 s
    spine <- (Elim' Term -> ST s (Elim' (Pointer s))) -> Elims -> ST s (Spine s)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Elim' Term -> ST s (Elim' (Pointer s))
    thunk Elims
    es
        Spine s -> ()
    forall {s}. [Elim' (Pointer s)] -> ()
    forceSpine Spine s
    spine () -> ST s (Spine s) -> ST s (Spine s)
    `seq` Spine s -> ST s (Spine s)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Spine s
    spine
      where
        -- Need to be strict in mkClosure to avoid memory leak
        forceSpine :: [Elim' (Pointer s)] -> ()
    forceSpine = (() -> Elim' (Pointer s) -> ()) -> () -> [Elim' (Pointer s)] -> ()
    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' Term -> 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 (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 (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 (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 -> 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
    forall s. Env s
    emptyEnv []
        closure FreeVariables
    fv Term
    t      = Env s
    env' Env s -> Closure s -> Closure s
    `seq` 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' []
          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 Any] -> [Pointer Any]
    trim Int
    _ [] = []
        trim Int
    i (Pointer Any
    p : [Pointer Any]
    ps)
          | Int -> IntSet -> Bool
    IntSet.member Int
    i IntSet
    fvs = (Pointer Any
    p Pointer Any -> [Pointer Any] -> [Pointer Any]
    forall a. a -> [a] -> [a]
    :)             ([Pointer Any] -> [Pointer Any]) -> [Pointer Any] -> [Pointer Any]
    forall a b. (a -> b) -> a -> b
    $! Int -> [Pointer Any] -> [Pointer Any]
    trim (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [Pointer Any]
    ps
          | Bool
    otherwise           = (Pointer Any
    forall s. Pointer s
    unusedPointer Pointer Any -> [Pointer Any] -> [Pointer Any]
    forall a. a -> [a] -> [a]
    :) ([Pointer Any] -> [Pointer Any]) -> [Pointer Any] -> [Pointer Any]
    forall a b. (a -> b) -> a -> b
    $! Int -> [Pointer Any] -> [Pointer Any]
    trim (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [Pointer Any]
    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 -> ReductionFlags -> Term -> Blocked Term
    reduceTm :: ReduceEnv
    -> BuiltinEnv
    -> (QName -> CompactDef)
    -> Normalisation
    -> ReductionFlags
    -> Term
    -> Blocked Term
    reduceTm ReduceEnv
    rEnv BuiltinEnv
    bEnv !QName -> CompactDef
    constInfo Normalisation
    normalisation ReductionFlags{Bool
    hasRewriting :: Bool
    allowUnconfirmed :: Bool
    allowNonTerminating :: Bool
    hasRewriting :: ReductionFlags -> Bool
    allowUnconfirmed :: ReductionFlags -> Bool
    allowNonTerminating :: ReductionFlags -> Bool
    ..} =
        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.
        metaStore :: IntMap MetaVariable
    metaStore      = ReduceEnv -> TCState
    redSt ReduceEnv
    rEnv TCState
    -> Lens' (IntMap MetaVariable) TCState -> IntMap MetaVariable
    forall o i. o -> Lens' i o -> i
    ^. Lens' (IntMap MetaVariable) TCState
    stMetaStore
        -- 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' Bool TCState -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool TCState
    stConsideringInstance
        getMeta :: MetaId -> MetaInstantiation
    getMeta MetaId
    m      = MetaInstantiation
    -> (MetaVariable -> MetaInstantiation)
    -> Maybe MetaVariable
    -> MetaInstantiation
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe MetaInstantiation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MetaVariable -> MetaInstantiation
    mvInstantiation (Int -> IntMap MetaVariable -> Maybe MetaVariable
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (MetaId -> Int
    metaId MetaId
    m) IntMap MetaVariable
    metaStore)
        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' PragmaOptions TCState -> PragmaOptions
    forall o i. o -> Lens' i o -> i
    ^. Lens' PragmaOptions TCState
    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 (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{ cdefDelayed :: CompactDef -> Bool
    cdefDelayed        = Bool
    delayed
                            , cdefNonterminating :: CompactDef -> Bool
    cdefNonterminating = Bool
    nonterm
                            , cdefUnconfirmed :: CompactDef -> Bool
    cdefUnconfirmed    = Bool
    unconf
                            , cdefDef :: CompactDef -> CompactDefn
    cdefDef            = CompactDefn
    def } = QName -> CompactDef
    constInfo QName
    f
                  dontUnfold :: Bool
    dontUnfold = (Bool
    nonterm Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    allowNonTerminating) Bool -> Bool -> Bool
    ||
                               (Bool
    unconf  Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    allowUnconfirmed)    Bool -> Bool -> Bool
    ||
                               (Bool
    delayed Bool -> Bool -> Bool
    && Bool -> Bool
    not ([ControlFrame s] -> Bool
    forall s. ControlStack s -> Bool
    unfoldDelayed [ControlFrame s]
    ctrl))
              in case CompactDefn
    def of
                CFun{ cfunCompiled :: CompactDefn -> FastCompiledClauses
    cfunCompiled = FastCompiledClauses
    cc }
                  | Bool
    dontUnfold -> AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM AM s
    done
                  | Bool
    otherwise  -> 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 (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. [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 -> MetaInstantiation
    getMeta MetaId
    m of
                InstV [Arg VerboseKey]
    xs Term
    t -> do
                  Spine s
    spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  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' Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine)
                  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 ([Arg VerboseKey] -> Term -> Term
    lams [Arg VerboseKey]
    zs Term
    t) Env s
    env Spine s
    spine'' [ControlFrame s]
    ctrl)
                MetaInstantiation
    _ -> 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)

            -- 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 s
    spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  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
    t Env s
    env0 (Spine s
    spine' Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine) [ControlFrame s]
    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 s
    spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                  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
    b Term
    t Env s
    env0 (Spine s
    spine' Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine)) (ControlFrame s
    forall s. ControlFrame s
    NormaliseK ControlFrame s -> [ControlFrame s] -> [ControlFrame s]
    forall a. a -> [a] -> [a]
    : [ControlFrame s]
    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 (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' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    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 s
    cl1@(Closure IsValue
    _ Term
    arg1 Env s
    _ Spine s
    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 (Term
    arg1, Term
    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 (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 (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 (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 s
    spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                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_
    blk (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci []) Env s
    forall s. Env s
    emptyEnv (Spine s
    spine' Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine) [ControlFrame s]
    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 (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 s
    spine' <- Env s -> Elims -> ST s (Spine s)
    forall s. Env s -> Elims -> ST s (Spine s)
    elimsToSpine Env s
    env Elims
    es
                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_
    blk (QName -> Elims -> Term
    Def QName
    q []) Env s
    forall s. Env s
    emptyEnv (Spine s
    spine' Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine) [ControlFrame s]
    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.
                Blocked_
    blk' <- case Blocked_
    blk of
                          Blocked{}      -> Blocked_ -> ST s Blocked_
    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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Term
    v -> NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (Elim' Term -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    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) ()
                Blocked_ -> MatchStack s -> [ControlFrame s] -> ST s (Blocked Term)
    forall s.
    Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    stuckMatch Blocked_
    blk' MatchStack s
    stack [ControlFrame s]
    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]
                  [Pointer s]
    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)
    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
    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' :: MatchStack s
    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
                  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' MatchStack s
    stack' [ControlFrame s]
    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 (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 (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 NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses ()) 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 (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 (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
              Blocked Term
    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 Term -> IntervalView
    iview (Term -> IntervalView) -> Term -> IntervalView
    forall a b. (a -> b) -> a -> b
    $ Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    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 (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
            Term
    v <- Closure s -> ST s Term
    forall s. Closure s -> ST s Term
    decodeClosure_ Closure s
    c
            AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM (Blocked Term -> AM s
    mkValue (Blocked Term -> AM s) -> Blocked Term -> AM s
    forall a b. (a -> b) -> a -> b
    $ ReduceM (Blocked Term) -> Blocked Term
    forall a. ReduceM a -> a
    runReduce (ReduceM (Blocked Term) -> Blocked Term)
    -> ReduceM (Blocked Term) -> Blocked Term
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM (Blocked Term)
    slow Term
    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 (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__

        -- If rewriting is enabled, try to apply rewrite rules to the current focus before considering
        -- it a value. The current state must be 'Eval' and the focus a value closure. Take care to only
        -- test the 'hasRewriting' flag once.
        rewriteAM :: AM s -> ST s (Blocked Term)
        rewriteAM :: forall s. AM s -> ST s (Blocked Term)
    rewriteAM = if Bool
    hasRewriting then AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    rewriteAM' else AM s -> ST s (Blocked Term)
    forall s. AM s -> ST s (Blocked Term)
    runAM

        -- 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 (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
    <+> 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
            Term
    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 [])
            Elims
    es <- Spine s -> ST s Elims
    forall s. Spine s -> ST s Elims
    decodeSpine Spine s
    spine
            case ReduceM (Reduced (Blocked Term) Term)
    -> Reduced (Blocked Term) Term
    forall a. ReduceM a -> a
    runReduce (Blocked_
    -> (Elims -> Term)
    -> RewriteRules
    -> Elims
    -> ReduceM (Reduced (Blocked Term) Term)
    rewrite Blocked_
    blk (Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE Term
    v0) RewriteRules
    rewr Elims
    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 (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

        -- Only unfold delayed (corecursive) definitions if the result is being cased on.
        unfoldDelayed :: ControlStack s -> Bool
        unfoldDelayed :: forall s. ControlStack s -> Bool
    unfoldDelayed []                     = Bool
    False
        unfoldDelayed (CaseK{}       : [ControlFrame s]
    _)    = Bool
    True
        unfoldDelayed (PrimOpK{}     : [ControlFrame s]
    _)    = Bool
    False
        unfoldDelayed (NatSucK{}     : [ControlFrame s]
    _)    = Bool
    False
        unfoldDelayed (NormaliseK{}  : [ControlFrame s]
    _)    = Bool
    False
        unfoldDelayed (ArgK{}        : [ControlFrame s]
    _)    = Bool
    False
        unfoldDelayed (UpdateThunk{} : [ControlFrame s]
    ctrl) = [ControlFrame s] -> Bool
    forall s. ControlStack s -> Bool
    unfoldDelayed [ControlFrame s]
    ctrl
        unfoldDelayed (ApplyK{}      : [ControlFrame s]
    ctrl) = [ControlFrame s] -> Bool
    forall s. ControlStack s -> Bool
    unfoldDelayed [ControlFrame s]
    ctrl
        unfoldDelayed (ForceK{}      : [ControlFrame s]
    ctrl) = [ControlFrame s] -> Bool
    forall s. ControlStack s -> Bool
    unfoldDelayed [ControlFrame s]
    ctrl
        unfoldDelayed (EraseK{}      : [ControlFrame s]
    ctrl) = [ControlFrame s] -> Bool
    forall s. ControlStack s -> Bool
    unfoldDelayed [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 NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses ()) Closure s
    cl) ControlStack s
    ctrl)
          | QName
    f QName -> Set QName -> 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 NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses ()) Closure s
    cl) ControlStack s
    ctrl)
          | Bool
    hasRewriting         = 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
          | Bool
    otherwise            = ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term)
    forall a. ReduceM a -> a
    runReduce (ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term))
    -> ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $
              VerboseKey
    -> Int
    -> VerboseKey
    -> ReduceM (ST s (Blocked Term))
    -> ReduceM (ST s (Blocked Term))
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> Int -> VerboseKey -> m a -> m a
    traceSLn VerboseKey
    "impossible" Int
    10 (VerboseKey
    "Incomplete pattern matching when applying " VerboseKey -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> VerboseKey
    forall a. Pretty a => a -> VerboseKey
    prettyShow QName
    f)
                       ReduceM (ST s (Blocked Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- 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 (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
    <+> [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
    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
    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
    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
    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
    text VerboseKey
    tag
                               , Int -> Doc -> Doc
    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
    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
    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
    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
    <+> 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
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
                              , Int -> Doc -> Doc
    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
    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
    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
    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
    _ Spine s
    _ Spine 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
    <+> 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
    _ Spine s
    spine0 Spine 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
    <?> Spine s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList (Spine s
    spine0 Spine s -> Spine s -> Spine s
    forall a. Semigroup a => a -> a -> a
    <> Spine s
    spine1)
      prettyPrec Int
    p (EraseK QName
    _ Spine s
    sp0 Spine s
    sp1 Spine s
    sp2 Spine 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
    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
    sp0
                                                                      , Int -> Doc -> Doc
    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
    sp1
                                                                      , Int -> Doc -> Doc
    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
    sp2
                                                                      , Int -> Doc -> Doc
    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
    sp3 ]
      prettyPrec Int
    _ (NatSucK Integer
    n)              = VerboseKey -> Doc
    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
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
                                                                    , Int -> Doc -> Doc
    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
    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
    <+> VerboseKey -> Doc
    text (Int -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show ([STPointer s] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [STPointer s]
    ps))
      prettyPrec Int
    p (ApplyK 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
    "ApplyK" Doc -> Doc -> Doc
    <?> Spine s -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList Spine 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
    <+> Int -> Closure s -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    10 Closure s
    cl ]