{-# LANGUAGE CPP #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternGuards #-}
-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}
{-# OPTIONS_GHC -fmax-worker-args=15 #-}
#if  __GLASGOW_HASKELL__ > 902
{-# OPTIONS_GHC -fworker-wrapper-cbv #-}
#endif


{-|

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

Some other tricks that improves performance:

- Memoise getConstInfo.

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

- Optimised case trees.

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

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

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

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

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

import Prelude hiding ((!!), null)

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

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

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

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

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

import Agda.Interaction.Options

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

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
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 -> Bool -> RewriteRules
  -> ReduceM CompactDef
compactDef :: BuiltinEnv
-> Definition -> Bool -> RewriteRules -> ReduceM CompactDef
compactDef BuiltinEnv
bEnv Definition
def Bool
copatterns RewriteRules
rewr = do

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

  let isConOrProj = case Definition -> Defn
theDef Definition
def of
        Constructor{} -> Bool
True
        Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right{} } -> Bool
True
        Defn
_ -> Bool
False

  let allowReduce =
             Bool
shouldReduce
          Bool -> Bool -> Bool
&& (
                   (AllowedReduction
RecursiveReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed)
                Bool -> Bool -> Bool
|| (Bool
isConOrProj Bool -> Bool -> Bool
&& AllowedReduction
ProjectionReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed)
                Bool -> Bool -> Bool
|| (Defn -> Bool
isInlineFun (Definition -> Defn
theDef Definition
def) Bool -> Bool -> Bool
&& AllowedReduction
InlineReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed)
                Bool -> Bool -> Bool
|| (Defn -> Bool
definitelyNonRecursive_ (Definition -> Defn
theDef Definition
def) Bool -> Bool -> Bool
&& (
                       (Bool
copatterns Bool -> Bool -> Bool
&& AllowedReduction
CopatternReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed)
                    Bool -> Bool -> Bool
|| (AllowedReduction
FunctionReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet AllowedReduction
allowed))
                   )
             )
          Bool -> Bool -> Bool
&& (Bool -> Bool
not (Definition -> Bool
defNonterminating Definition
def) Bool -> Bool -> Bool
|| AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
SmallSet.member AllowedReduction
NonTerminatingReductions SmallSet AllowedReduction
allowed)
             -- WARNING: don't use isPropM here because it relies on reduction,
             -- which causes an infinite loop.
          Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Bool
forall t. Sort' t -> Bool
isProp (Sort' Term -> Bool) -> Sort' Term -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort (Type -> Sort' Term) -> Type -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def)
          Bool -> Bool -> Bool
&& (Bool -> Bool
not (Definition -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Definition
def))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Case tree with bodies.

data FastCompiledClauses
  = FCase !Int (FastCase FastCompiledClauses)
    -- ^ @Case n bs@ stands for a match on the @n@-th argument
    -- (counting from zero) with @bs@ as the case branches.
    -- If the @n@-th argument is a projection, we have only 'conBranches'
    -- with arity 0.
  | FEta !Int [Arg QName] FastCompiledClauses (Maybe FastCompiledClauses)
    -- ^ Match on record constructor. Can still have a catch-all though. Just
    --   contains the fields, not the actual constructor.
  | FDone (CCDone Term)
    -- ^ See 'Done'.
    --   @FDone (CCDone _ mr 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.
    --   @mr@ indicates whether this leaf containts recursive mutually recursive calls.
  | FFail
    -- ^ Absurd case.

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

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


{-# INLINE lookupCon #-}
lookupCon :: QName -> FastCase c -> Maybe c
lookupCon :: forall c. QName -> FastCase c -> Maybe c
lookupCon QName
c (FBranches Bool
_ Map NameId c
cons Maybe c
_ Map Literal c
_ Maybe c
_ Bool
_) = NameId -> Map NameId c -> Maybe c
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (QName -> NameId
forall a. HasNameId a => a -> NameId
nameId 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
unsafeDupablePerformIO (IO (QName -> a) -> QName -> a) -> IO (QName -> a) -> QName -> a
forall a b. (a -> b) -> a -> b
$ do
  tbl <- Map NameId a -> IO (IORef (Map NameId a))
forall a. a -> IO (IORef a)
newIORef Map NameId a
forall k a. Map k a
Map.empty
  return (unsafeDupablePerformIO . f' tbl)
  where
    f' :: IORef (Map NameId a) -> QName -> IO a
f' IORef (Map NameId a)
tbl QName
x = do
      let i :: NameId
i = QName -> NameId
forall a. HasNameId a => a -> NameId
nameId QName
x
      m <- IORef (Map NameId a) -> IO (Map NameId a)
forall a. IORef a -> IO a
readIORef IORef (Map NameId a)
tbl
      case Map.lookup i m of
        Just a
y  -> a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y
        Maybe a
Nothing -> do
          let y :: a
y = QName -> a
f QName
x
          IORef (Map NameId a) -> Map NameId a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Map NameId a)
tbl (Map NameId a -> IO ()) -> Map NameId a -> IO ()
forall a b. (a -> b) -> a -> b
$! NameId -> a -> Map NameId a -> Map NameId a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NameId
i a
y Map NameId a
m
          a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y

-- * Fast reduction

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

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

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

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

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

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

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

      bEnv = BuiltinEnv { bZero :: Maybe ConHead
bZero = Maybe ConHead
zero, bSuc :: Maybe ConHead
bSuc = Maybe ConHead
suc, bTrue :: Maybe ConHead
bTrue = Maybe ConHead
true, bFalse :: Maybe ConHead
bFalse = Maybe ConHead
false, bRefl :: Maybe ConHead
bRefl = Maybe ConHead
refl,
                          bPrimForce :: Maybe QName
bPrimForce = Maybe QName
force, bPrimErase :: Maybe QName
bPrimErase = Maybe QName
erase }
  rwr    <- rewritingOption
  rwrLoc <- localRewritingOption

  constInfo <- case rwr || rwrLoc of -- András 2026-04-06: TODO more fine-grained choice
    Bool
True -> (QName -> CompactDef) -> QName -> CompactDef
forall a. (QName -> a) -> QName -> a
memoQName ((QName -> CompactDef) -> QName -> CompactDef)
-> ReduceM (QName -> CompactDef) -> ReduceM (QName -> CompactDef)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli \QName
f -> do
      info <- QName -> ReduceM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      copatterns <- defCopatternLHS f info
      rewr <- getAllRewriteRulesForDefHead f
      compactDef bEnv info copatterns rewr
    Bool
False -> (QName -> CompactDef) -> QName -> CompactDef
forall a. (QName -> a) -> QName -> a
memoQName ((QName -> CompactDef) -> QName -> CompactDef)
-> ReduceM (QName -> CompactDef) -> ReduceM (QName -> CompactDef)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli \QName
f -> do
      info <- QName -> ReduceM Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      let copatterns = Definition -> Bool
defCopatternLHS' Definition
info
      compactDef bEnv info copatterns []

  localRewr <- case rwrLoc of
    Bool
True  -> (Int -> RewriteRules) -> Int -> RewriteRules
forall a. (Int -> a) -> Int -> a
memoUnsafeInt ((Int -> RewriteRules) -> Int -> RewriteRules)
-> ReduceM (Int -> RewriteRules) -> ReduceM (Int -> RewriteRules)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (Int -> ReduceM RewriteRules) -> ReduceM (Int -> RewriteRules)
forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli Int -> ReduceM RewriteRules
forall (m :: * -> *). HasConstInfo m => Int -> m RewriteRules
getAllRewriteRulesForVarHead
    Bool
False -> (Int -> RewriteRules) -> ReduceM (Int -> RewriteRules)
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\Int
_ -> [])

  ReduceM \ReduceEnv
redEnv ->
    ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> (Int -> RewriteRules)
-> Normalisation
-> Term
-> Blocked Term
reduceTm ReduceEnv
redEnv BuiltinEnv
bEnv QName -> CompactDef
constInfo Int -> RewriteRules
localRewr Normalisation
norm Term
v


-- * Closures

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

-- | A thunk can be a 'BlackHole' while a plain 'Closure' can't. This is not enforced in types. We
--   could distinguish these by making 'Closure' an indexed GADT, but I don't think it's worth it.
type Thunk s = Closure s

-- | 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

#if __GLASGOW_HASKELL__ < 906
data SElim s
  = SApply !ArgInfo !(Pointer s)
  | SProj !ProjOrigin !QName
  | SIApply !(Pointer s)
            !(Pointer s)
            !(Pointer s)
#else
data SElim s
  = SApply !ArgInfo {-# UNPACK #-} !(Pointer s)
  | SProj !ProjOrigin !QName
  | SIApply {-# UNPACK #-} !(Pointer s)
            {-# UNPACK #-} !(Pointer s)
            {-# UNPACK #-} !(Pointer s)
#endif

sElimToElim :: SElim s -> Elim' (Pointer s)
sElimToElim :: forall s. SElim s -> Elim' (Pointer s)
sElimToElim = \case
  SApply ArgInfo
i Pointer s
t -> Arg (Pointer s) -> Elim' (Pointer s)
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Pointer s -> Arg (Pointer s)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i Pointer s
t)
  SProj ProjOrigin
o QName
x -> ProjOrigin -> QName -> Elim' (Pointer s)
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
x
  SIApply Pointer s
l Pointer s
r Pointer s
t -> Pointer s -> Pointer s -> Pointer s -> Elim' (Pointer s)
forall a. a -> a -> a -> Elim' a
IApply Pointer s
l Pointer s
r Pointer s
t

-- | The spine is a list of eliminations. Application eliminations contain pointers.
type Spine s = [SElim s]

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

sAllApplyElims :: Spine s -> Maybe# [Pointer s]
sAllApplyElims :: forall s. Spine s -> Maybe# [Pointer s]
sAllApplyElims = \case
  []              -> [Pointer s] -> Maybe# [Pointer s]
forall a. a -> Maybe# a
Just# []
  SApply ArgInfo
_ Pointer s
p : Spine s
es -> case Spine s -> Maybe# [Pointer s]
forall s. Spine s -> Maybe# [Pointer s]
sAllApplyElims Spine s
es of
    Maybe# [Pointer s]
Nothing# -> Maybe# [Pointer s]
forall a. Maybe# a
Nothing#
    Just# [Pointer s]
ps -> [Pointer s] -> Maybe# [Pointer s]
forall a. a -> Maybe# a
Just# (Pointer s
pPointer s -> [Pointer s] -> [Pointer s]
forall a. a -> [a] -> [a]
:[Pointer s]
ps)
  SIApply Pointer s
_ Pointer s
_ Pointer s
p : Spine s
es -> case Spine s -> Maybe# [Pointer s]
forall s. Spine s -> Maybe# [Pointer s]
sAllApplyElims Spine s
es of
    Maybe# [Pointer s]
Nothing# -> Maybe# [Pointer s]
forall a. Maybe# a
Nothing#
    Just# [Pointer s]
ps -> [Pointer s] -> Maybe# [Pointer s]
forall a. a -> Maybe# a
Just# (Pointer s
pPointer s -> [Pointer s] -> [Pointer s]
forall a. a -> [a] -> [a]
:[Pointer s]
ps)
  Spine s
_ -> Maybe# [Pointer s]
forall a. Maybe# a
Nothing#

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
setIsValue IsValue
isV Closure s
_ = Closure s
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 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 [SElim s]
es) [SElim s]
es' = IsValue -> Term -> Env s -> [SElim s] -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled Term
t Env s
env ([SElim s]
es [SElim s] -> [SElim s] -> [SElim s]
forall a. [a] -> [a] -> [a]
++! [SElim s]
es')
clApply Closure s
_ [SElim s]
_ = Closure s
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 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 [SElim s]
es) [SElim s]
es' = IsValue -> Term -> Env s -> [SElim s] -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
b Term
t Env s
env ([SElim s]
es [SElim s] -> [SElim s] -> [SElim s]
forall a. [a] -> [a] -> [a]
++! [SElim s]
es')
clApply_ Closure s
_ [SElim s]
_ = Closure s
forall a. HasCallStack => a
__IMPOSSIBLE__

-- * 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 s)

thunk :: Closure s -> Thunk s
thunk :: forall s. Closure s -> Closure s
thunk = Closure s -> Closure s
forall a. a -> a
id

derefPointer :: Pointer s -> ST s (Thunk s)
derefPointer :: forall s. Pointer s -> ST s (Thunk s)
derefPointer (Pure Closure s
cl)     = Closure s -> ST s (Closure s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure s -> ST s (Closure s)) -> Closure s -> ST s (Closure s)
forall a b. (a -> b) -> a -> b
$ Closure s -> Closure s
forall s. Closure s -> Closure s
thunk Closure s
cl
derefPointer (Pointer STPointer s
ptr) = STPointer s -> ST s (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 (Thunk s)
derefPointer_ Pointer s
ptr =
  Pointer s -> ST s (Thunk s)
forall s. Pointer s -> ST s (Thunk s)
derefPointer Pointer s
ptr ST s (Thunk s) -> (Thunk s -> Thunk s) -> ST s (Thunk s)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Thunk s
BlackHole -> Thunk s
forall a. HasCallStack => a
__IMPOSSIBLE__
    Thunk s
cl        -> Thunk s
cl

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

readPointer :: STPointer s -> ST s (Thunk s)
readPointer :: forall s. STPointer s -> ST s (Thunk s)
readPointer = STRef s (Thunk s) -> ST s (Thunk 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 -> Closure s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STPointer s
ptr (Closure s -> Closure s
forall s. Closure s -> Closure s
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 s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STPointer s
ptr Thunk s
forall s. Closure s
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 cl :: Closure s
cl@(Closure IsValue
_ (Var Int
x []) Env s
env []) =
  Int
-> Env s
-> (Pointer s -> ST s (Pointer s))
-> (() -> ST s (Pointer s))
-> ST s (Pointer s)
forall s a. Int -> Env s -> (Pointer s -> a) -> (() -> a) -> a
lookupEnv Int
x Env s
env (\Pointer s
p -> Pointer s -> ST s (Pointer s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Pointer s
p)
                  (\()
_ -> STPointer s -> Pointer s
forall s. STPointer s -> Pointer s
Pointer (STPointer s -> Pointer s)
-> ST s (STPointer s) -> ST s (Pointer s)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Closure s -> ST s (STPointer s)
forall a s. a -> ST s (STRef s a)
newSTRef (Closure s -> Closure s
forall s. Closure s -> Closure s
thunk Closure s
cl))
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 (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Closure s -> ST s (STPointer s)
forall a s. a -> ST s (STRef s a)
newSTRef (Closure s -> Closure s
forall s. Closure s -> Closure s
thunk Closure s
cl)

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

-- * Environments

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

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

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

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

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

{-# INLINE lookupEnv #-}
lookupEnv :: Int -> Env s -> (Pointer s -> a) -> (() -> a) -> a
lookupEnv :: forall s a. Int -> Env s -> (Pointer s -> a) -> (() -> a) -> a
lookupEnv Int
i (Env [Pointer s]
e) Pointer s -> a
found () -> a
notfound = Int -> [Pointer s] -> a
go Int
i [Pointer s]
e where
  go :: Int -> [Pointer s] -> a
go Int
0 (Pointer s
p:[Pointer s]
ps) = Pointer s -> a
found Pointer s
p
  go Int
i (Pointer s
p:[Pointer s]
ps) = Int -> [Pointer s] -> a
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Pointer s]
ps
  go Int
_ [Pointer s]
_      = () -> a
notfound ()

-- * 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.

-- | 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.
data Eval s = Eval !(Closure 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.
data Match s = Match QName FastCompiledClauses (Spine s) {-# UNPACK #-} !(MatchStack s) !(ControlStack s)

data CatchallFrames s
  = CAFNil
  | CAFCons {-# UNPACK #-} !(CatchallFrame s) !(CatchallFrames 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 = !(CatchallFrames s) :> (Closure s)
infixr 2 :>, >:

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

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

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

instance Zipper (ElimZipper (Pointer s)) where
  type Carrier (ElimZipper (Pointer s)) = SElim s
  type Element (ElimZipper (Pointer s)) = Pointer s

  firstHole :: Carrier (ElimZipper (Pointer s))
-> Maybe (Element (ElimZipper (Pointer s)), ElimZipper (Pointer s))
firstHole (SApply ArgInfo
i Pointer s
arg)  = (Pointer s, ElimZipper (Pointer s))
-> Maybe (Pointer s, ElimZipper (Pointer s))
forall a. a -> Maybe a
Just (Pointer s
arg, ArgInfo -> ElimZipper (Pointer s)
forall a. ArgInfo -> ElimZipper a
ApplyCxt ArgInfo
i)
  firstHole (SIApply Pointer s
a Pointer s
x Pointer s
y) = (Pointer s, ElimZipper (Pointer s))
-> Maybe (Pointer s, ElimZipper (Pointer s))
forall a. a -> Maybe a
Just (Pointer s
a, Pointer s -> Pointer s -> ElimZipper (Pointer s)
forall a. a -> a -> ElimZipper a
IApplyType Pointer s
x Pointer s
y)
  firstHole SProj{}         = Maybe (Element (ElimZipper (Pointer s)), ElimZipper (Pointer s))
Maybe (Pointer s, ElimZipper (Pointer s))
forall a. Maybe a
Nothing

  plugHole :: Element (ElimZipper (Pointer s))
-> ElimZipper (Pointer s) -> Carrier (ElimZipper (Pointer s))
plugHole Element (ElimZipper (Pointer s))
x (ApplyCxt ArgInfo
i)     = ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
i Element (ElimZipper (Pointer s))
Pointer s
x
  plugHole Element (ElimZipper (Pointer s))
a (IApplyType Pointer s
x Pointer s
y) = Pointer s -> Pointer s -> Pointer s -> SElim s
forall s. Pointer s -> Pointer s -> Pointer s -> SElim s
SIApply Element (ElimZipper (Pointer s))
Pointer s
a Pointer s
x Pointer s
y
  plugHole Element (ElimZipper (Pointer s))
x (IApplyFst Pointer s
a Pointer s
y)  = Pointer s -> Pointer s -> Pointer s -> SElim s
forall s. Pointer s -> Pointer s -> Pointer s -> SElim s
SIApply Pointer s
a Element (ElimZipper (Pointer s))
Pointer s
x Pointer s
y
  plugHole Element (ElimZipper (Pointer s))
y (IApplySnd Pointer s
a Pointer s
x)  = Pointer s -> Pointer s -> Pointer s -> SElim s
forall s. Pointer s -> Pointer s -> Pointer s -> SElim s
SIApply Pointer s
a Pointer s
x Element (ElimZipper (Pointer s))
Pointer s
y

  nextHole :: Element (ElimZipper (Pointer s))
-> ElimZipper (Pointer s)
-> Either
     (Carrier (ElimZipper (Pointer s)))
     (Element (ElimZipper (Pointer s)), ElimZipper (Pointer s))
nextHole Element (ElimZipper (Pointer s))
a (IApplyType Pointer s
x Pointer s
y) = (Pointer s, ElimZipper (Pointer s))
-> Either (SElim s) (Pointer s, ElimZipper (Pointer s))
forall a b. b -> Either a b
Right (Pointer s
x, Pointer s -> Pointer s -> ElimZipper (Pointer s)
forall a. a -> a -> ElimZipper a
IApplyFst Element (ElimZipper (Pointer s))
Pointer s
a Pointer s
y)
  nextHole Element (ElimZipper (Pointer s))
x (IApplyFst Pointer s
a Pointer s
y)  = (Pointer s, ElimZipper (Pointer s))
-> Either (SElim s) (Pointer s, ElimZipper (Pointer s))
forall a b. b -> Either a b
Right (Pointer s
y, Pointer s -> Pointer s -> ElimZipper (Pointer s)
forall a. a -> a -> ElimZipper a
IApplySnd Pointer s
a Element (ElimZipper (Pointer s))
Pointer s
x)
  nextHole Element (ElimZipper (Pointer s))
y (IApplySnd Pointer s
a Pointer s
x)  = SElim s -> Either (SElim s) (Pointer s, ElimZipper (Pointer s))
forall a b. a -> Either a b
Left (Pointer s -> Pointer s -> Pointer s -> SElim s
forall s. Pointer s -> Pointer s -> Pointer s -> SElim s
SIApply Pointer s
a Pointer s
x Element (ElimZipper (Pointer s))
Pointer s
y)
  nextHole Element (ElimZipper (Pointer s))
x c :: ElimZipper (Pointer s)
c@ApplyCxt{}     = SElim s -> Either (SElim s) (Pointer s, ElimZipper (Pointer s))
forall a b. a -> Either a b
Left (SElim s -> Either (SElim s) (Pointer s, ElimZipper (Pointer s)))
-> SElim s -> Either (SElim s) (Pointer s, ElimZipper (Pointer s))
forall a b. (a -> b) -> a -> b
$! Element (ElimZipper (Pointer s))
-> ElimZipper (Pointer s) -> Carrier (ElimZipper (Pointer s))
forall z. Zipper z => Element z -> z -> Carrier z
plugHole Element (ElimZipper (Pointer s))
x ElimZipper (Pointer s)
c

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

-- | Control frames are continuations that act on value closures.
data ControlStack s
  = CaseK QName ArgInfo (FastCase FastCompiledClauses) (Spine s) (Spine s) {-# UNPACK #-} !(MatchStack s) !(ControlStack 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) !(ControlStack 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 !(ControlStack s)
      -- ^ Indicates that the focus should be evaluated to full normal form.
  | ForceK QName (Spine s) (Spine s) !(ControlStack 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) !(ControlStack 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 !(ControlStack s)
      -- ^ @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) !(ControlStack s)
      -- ^ @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] !(ControlStack s)
      -- ^ @UpdateThunk ps@. Update the pointers @ps@ with the value of the
      --   current focus.
  | ApplyK (Spine s) !(ControlStack 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.
  | EmptyK
      -- ^ Finished execution.

-- * 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 -> Eval s
compile :: forall s. Normalisation -> Term -> Eval s
compile Normalisation
nf Term
t =
  let !k :: ControlStack s
k = if Normalisation
nf Normalisation -> Normalisation -> Bool
forall a. Eq a => a -> a -> Bool
== Normalisation
NF then ControlStack s -> ControlStack s
forall s. ControlStack s -> ControlStack s
NormaliseK ControlStack s
forall s. ControlStack s
EmptyK else ControlStack s
forall s. ControlStack s
EmptyK in
  Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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 []) ControlStack s
k

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 (Thunk 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
$ Spine s -> ST s Elims
forall s. Spine s -> ST s Elims
go Spine s
spine where
  go :: [SElim s] -> ST s Elims
go [] = Elims -> ST s Elims
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  go (SElim s
e:[SElim s]
es) = case SElim s
e of
    SApply ArgInfo
i Pointer s
t -> do
      t <- Pointer s -> ST s Term
forall s. Pointer s -> ST s Term
decodePointer Pointer s
t
      (Apply (Arg i t):) <$!> go es
    SProj ProjOrigin
o QName
x -> (ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
xElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> ST s Elims -> ST s Elims
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> [SElim s] -> ST s Elims
go [SElim s]
es
    SIApply Pointer s
l Pointer s
r Pointer s
t -> do
      l <- Pointer s -> ST s Term
forall s. Pointer s -> ST s Term
decodePointer Pointer s
l
      r <- decodePointer r
      t <- decodePointer t
      (IApply l r t:) <$!> go es

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

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

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

-- | Turn a list of internal syntax eliminations into a spine. This builds closures and allocates
--   thunks for all the 'Apply' elims. We append the result onto the @Spine s@ argument.
elimsToSpine :: Env s -> Elims -> Spine s -> ST s (Spine s)
elimsToSpine :: forall s. Env s -> Elims -> Spine s -> ST s (Spine s)
elimsToSpine Env s
env Elims
es Spine s
sp0 = Elims -> Env s -> Spine s -> ST s (Spine s)
forall {s}. Elims -> Env s -> [SElim s] -> ST s [SElim s]
goETS Elims
es Env s
env Spine s
sp0 where
  -- We don't preserve free variables of closures (in the sense of their
  -- decoding), since we freely add things to the spines.
  unknownFVs :: a -> a
unknownFVs a
i
    | a -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables a
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = a
i
    | Bool
otherwise = FreeVariables -> a -> a
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables a
i

  -- Going straight for a value for literals is mostly to make debug traces
  -- less verbose and doesn't really buy anything performance-wise.
  closure :: Env s -> FreeVariables -> Term -> Closure s
closure Env s
_ FreeVariables
_ t :: Term
t@Lit{} = let !v :: IsValue
v = Blocked_ -> IsValue
Value (Blocked_ -> IsValue) -> Blocked_ -> IsValue
forall a b. (a -> b) -> a -> b
$! () -> Blocked_
forall a t. a -> Blocked' t a
notBlocked () in IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
v Term
t Env s
forall s. Env s
emptyEnv []
  closure Env s
env FreeVariables
fv Term
t    = let !env' :: Env s
env' = FreeVariables -> Env s -> Env s
forall s. FreeVariables -> Env s -> Env s
trimEnvironment FreeVariables
fv Env s
env in 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' []

  goETS :: Elims -> Env s -> [SElim s] -> ST s [SElim s]
goETS (Elim' Term
e:Elims
es) Env s
env [SElim s]
sp0 = case Elim' Term
e of
    (Apply (Arg ArgInfo
i Term
t)) -> do
      !t <- Closure s -> ST s (Pointer s)
forall s. Closure s -> ST s (Pointer s)
createThunk (Env s -> FreeVariables -> Term -> Closure s
forall {s}. Env s -> FreeVariables -> Term -> Closure s
closure Env s
env (ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i) Term
t)
      let !i' = ArgInfo -> ArgInfo
forall {a}. LensFreeVariables a => a -> a
unknownFVs ArgInfo
i
      (SApply i' t:) <$!> goETS es env sp0
    (Proj ProjOrigin
o QName
f)     -> (ProjOrigin -> QName -> SElim s
forall s. ProjOrigin -> QName -> SElim s
SProj ProjOrigin
o QName
fSElim s -> [SElim s] -> [SElim s]
forall a. a -> [a] -> [a]
:) ([SElim s] -> [SElim s]) -> ST s [SElim s] -> ST s [SElim s]
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Elims -> Env s -> [SElim s] -> ST s [SElim s]
goETS Elims
es Env s
env [SElim s]
sp0
    (IApply Term
a Term
x Term
y) -> do
      let 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
. Env s -> FreeVariables -> Term -> Closure s
forall {s}. Env s -> FreeVariables -> Term -> Closure s
closure Env s
env FreeVariables
UnknownFVs
      !e <- Pointer s -> Pointer s -> Pointer s -> SElim s
forall s. Pointer s -> Pointer s -> Pointer s -> SElim s
SIApply (Pointer s -> Pointer s -> Pointer s -> SElim s)
-> ST s (Pointer s) -> ST s (Pointer s -> Pointer s -> SElim s)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Term -> ST s (Pointer s)
mkThunk Term
a ST s (Pointer s -> Pointer s -> SElim s)
-> ST s (Pointer s) -> ST s (Pointer s -> SElim s)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Term -> ST s (Pointer s)
mkThunk Term
x ST s (Pointer s -> SElim s) -> ST s (Pointer s) -> ST s (SElim s)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Term -> ST s (Pointer s)
mkThunk Term
y
      (e:) <$!> goETS es env sp0
  goETS [] Env s
_ [SElim s]
sp0 = [SElim s] -> ST s [SElim s]
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SElim s]
sp0


-- | 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 VarSet
fvs) Env s
env
  | VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
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 _ [] = []
  --   trim i (p : ps)
  --     | VarSet.member i fvs = (p :)             $! trim (i + 1) ps
  --     | otherwise           = (unusedPointer :) $! trim (i + 1) 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 String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv [Arg String]
xs Spine s
spine = [Arg String] -> Spine s -> Env s -> ([Arg String], Env s, Spine s)
forall {a} {s}.
[a] -> [SElim s] -> Env s -> ([a], Env s, [SElim s])
go [Arg String]
xs Spine s
spine Env s
forall s. Env s
emptyEnv
  where
    go :: [a] -> [SElim s] -> Env s -> ([a], Env s, [SElim s])
go [] ![SElim s]
sp !Env s
env = ([], Env s
env, [SElim s]
sp)
    go xs0 :: [a]
xs0@(a
x : [a]
xs) [SElim s]
sp Env s
env = case [SElim s]
sp of
      []                  -> ([a]
xs0, Env s
env, [SElim s]
sp)
      SApply ArgInfo
_ Pointer s
c     : [SElim s]
sp -> [a] -> [SElim s] -> Env s -> ([a], Env s, [SElim s])
go [a]
xs [SElim s]
sp (Pointer s
c Pointer s -> Env s -> Env s
forall s. Pointer s -> Env s -> Env s
`extendEnv` Env s
env)
      SIApply Pointer s
x Pointer s
y Pointer s
r  : [SElim s]
sp -> [a] -> [SElim s] -> Env s -> ([a], Env s, [SElim s])
go [a]
xs [SElim s]
sp (Pointer s
r Pointer s -> Env s -> Env s
forall s. Pointer s -> Env s -> Env s
`extendEnv` Env s
env)
      [SElim s]
_                   -> ([a], Env s, [SElim s])
forall a. HasCallStack => a
__IMPOSSIBLE__

unusedPointerString :: Text
unusedPointerString :: Text
unusedPointerString = String -> Text
T.pack (Impossible -> String
forall a. Show a => a -> String
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 memoised function to lookup local rewrite rules, 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) -> (Nat -> RewriteRules)
  -> Normalisation -> Term -> Blocked Term
reduceTm :: ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> (Int -> RewriteRules)
-> Normalisation
-> Term
-> Blocked Term
reduceTm ReduceEnv
rEnv BuiltinEnv
bEnv !QName -> CompactDef
constInfo !Int -> RewriteRules
localRewr Normalisation
normalisation = Term -> Blocked Term
compileAndRun (Term -> Blocked Term) -> (Term -> Term) -> Term -> Blocked Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Term -> Term
forall a. Doc -> a -> a
traceDoc Doc
"-- fast reduce --"
  where
    -- Helpers to get information from the ReduceEnv.
    localMetas :: LocalMetaStore
localMetas     = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Getting LocalMetaStore TCState LocalMetaStore -> LocalMetaStore
forall s a. s -> Getting a s a -> a
^. Getting LocalMetaStore TCState LocalMetaStore
Lens' TCState LocalMetaStore
stSolvedMetaStore
    remoteMetas :: RemoteMetaStore
remoteMetas    = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Getting RemoteMetaStore TCState RemoteMetaStore
-> RemoteMetaStore
forall s a. s -> Getting a s a -> a
^. Getting RemoteMetaStore TCState RemoteMetaStore
Lens' TCState RemoteMetaStore
stImportedMetaStore
    -- Are we currently instance searching. In that case we don't fail hard on missing clauses. This
    -- is a (very unsatisfactory) work-around for #3870.
    speculative :: Bool
speculative    = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Getting Bool TCState Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCState Bool
Lens' TCState Bool
stConsideringInstance
    getMetaInst :: MetaId -> Maybe MetaInstantiation
getMetaInst MetaId
m  = case MetaId -> LocalMetaStore -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m LocalMetaStore
localMetas of
                       Just MetaVariable
mv -> MetaInstantiation -> Maybe MetaInstantiation
forall a. a -> Maybe a
Just (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
                       Maybe MetaVariable
Nothing -> Instantiation -> MetaInstantiation
InstV (Instantiation -> MetaInstantiation)
-> (RemoteMetaVariable -> Instantiation)
-> RemoteMetaVariable
-> MetaInstantiation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemoteMetaVariable -> Instantiation
rmvInstantiation (RemoteMetaVariable -> MetaInstantiation)
-> Maybe RemoteMetaVariable -> Maybe MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                    MetaId -> RemoteMetaStore -> Maybe RemoteMetaVariable
forall k v. Hashable k => k -> HashMap k v -> Maybe v
HMap.lookup MetaId
m RemoteMetaStore
remoteMetas
    partialDefs :: Set QName
partialDefs    = ReduceM (Set QName) -> Set QName
forall a. ReduceM a -> a
runReduce ReduceM (Set QName)
forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
    rewriteRules :: QName -> RewriteRules
rewriteRules QName
f = CompactDef -> RewriteRules
cdefRewriteRules (QName -> CompactDef
constInfo QName
f)
    callByNeed :: Bool
callByNeed     = (ReduceEnv -> TCEnv
redEnv ReduceEnv
rEnv TCEnv -> Getting Bool TCEnv Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCEnv Bool
Lens' TCEnv Bool
eCallByNeed) 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
-> Getting PragmaOptions TCState PragmaOptions -> PragmaOptions
forall s a. s -> Getting a s a -> a
^. Getting PragmaOptions TCState PragmaOptions
Lens' TCState PragmaOptions
stPragmaOptions)
    iview :: Term -> IntervalView
iview          = ReduceM (Term -> IntervalView) -> Term -> IntervalView
forall a. ReduceM a -> a
runReduce ReduceM (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

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

#ifdef DEBUG
    -- Debug output. Taking care that we only look at the verbosity level once.
    hasVerb tag lvl = unReduceM (hasVerbosity tag lvl) rEnv
    doDebug = hasVerb "tc.reduce.fast" 110
    traceDoc :: Doc -> a -> a
    traceDoc
      | doDebug   = trace . show
      | otherwise = const id

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

    -- Run the machine in a given state. Prints the state if the right verbosity level is active.
    runMatch :: Match s -> ST s (Blocked Term)
    runMatch = if doDebug then \s -> trace (prettyShow s) (runMatch' s)
                          else runMatch'
#else
    {-# INLINE traceDoc #-}
    traceDoc :: Doc -> a -> a
    traceDoc :: forall a. Doc -> a -> a
traceDoc Doc
_ a
a = a
a

    {-# INLINE runEval #-}
    -- Run the machine in a given state. Prints the state if the right verbosity level is active.
    runEval :: Eval s -> ST s (Blocked Term)
    runEval :: forall s. Eval s -> ST s (Blocked Term)
runEval = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval'

    {-# INLINE runMatch #-}
    -- Run the machine in a given state. Prints the state if the right verbosity level is active.
    runMatch :: Match s -> ST s (Blocked Term)
    runMatch :: forall s. Match s -> ST s (Blocked Term)
runMatch = Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch'
#endif


    -- 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 = QName -> NameId
forall a. HasNameId a => a -> NameId
nameId (QName -> NameId) -> (ConHead -> QName) -> ConHead -> NameId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName
    isZero :: ConHead -> Bool
isZero = case Maybe ConHead
zero of
               Maybe ConHead
Nothing -> Bool -> ConHead -> Bool
forall a b. a -> b -> a
const Bool
False
               Just ConHead
z  -> (ConHead -> NameId
conNameId ConHead
z NameId -> NameId -> Bool
forall a. Eq a => a -> a -> Bool
==) (NameId -> Bool) -> (ConHead -> NameId) -> ConHead -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> NameId
conNameId
    isSuc :: ConHead -> Bool
isSuc  = case Maybe ConHead
suc of
               Maybe ConHead
Nothing -> Bool -> ConHead -> Bool
forall a b. a -> b -> a
const Bool
False
               Just ConHead
s  -> (ConHead -> NameId
conNameId ConHead
s NameId -> NameId -> Bool
forall a. Eq a => a -> a -> Bool
==) (NameId -> Bool) -> (ConHead -> NameId) -> ConHead -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> NameId
conNameId

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

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


    -- The main function. This is where the stuff happens!
    runEval' :: Eval s -> ST s (Blocked Term)
    runEval' :: forall s. Eval s -> ST s (Blocked Term)
runEval' (Eval Closure s
BlackHole ControlStack s
_) = ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Base case: The focus is a value closure and the control stack is empty. Decode and return.
    runEval' (Eval cl :: Closure s
cl@(Closure Value{} Term
_ Env s
_ Spine s
_) ControlStack s
EmptyK) = 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
    runEval' s :: Eval s
s@(Eval cl :: Closure s
cl@(Closure IsValue
Unevaled Term
t Env s
env Spine s
spine) ControlStack s
ctrl) = {-# SCC "runEval" #-}

      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
-> ControlStack 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 ControlStack 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 CompactDef -> CompactDefn
cdefDef (QName -> CompactDef
constInfo QName
f) of
            CFun{ cfunCompiled :: CompactDefn -> FastCompiledClauses
cfunCompiled = FastCompiledClauses
cc } -> Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc Spine s
spine (CatchallFrames s
forall s. CatchallFrames s
CAFNil CatchallFrames s -> Closure s -> MatchStack s
forall s. CatchallFrames s -> Closure s -> MatchStack s
:> Closure s
cl) ControlStack s
ctrl)
            CompactDefn
CAxiom         -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval Eval s
done
            CompactDefn
CTyCon         -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval Eval s
done
            CCon{}         -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done   -- Only happens for builtinSharp (which is a Def when you bind it)
            CompactDefn
CForce | (Spine s
spine0, SApply ArgInfo
_ 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 -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
v [] (QName -> Spine s -> Spine s -> ControlStack s -> ControlStack s
forall s.
QName -> Spine s -> Spine s -> ControlStack s -> ControlStack s
ForceK QName
f Spine s
spine0 Spine s
spine1 ControlStack s
ctrl)
            CompactDefn
CForce -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done -- partially applied
            CompactDefn
CErase | (Spine s
spine0, SApply ArgInfo
_ Pointer s
v : SElim 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 -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
v [] (QName
-> Spine s
-> Spine s
-> Spine s
-> Spine s
-> ControlStack s
-> ControlStack s
forall s.
QName
-> Spine s
-> Spine s
-> Spine s
-> Spine s
-> ControlStack s
-> ControlStack s
EraseK QName
f Spine s
spine0 [] [SElim s
spine1] Spine s
spine2 ControlStack s
ctrl)
            CompactDefn
CErase -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done -- partially applied
            CPrimOp Int
n [Literal] -> Term
op Maybe FastCompiledClauses
cc | Spine s -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Spine s
spine Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n,                      -- PrimOps can't be over-applied. They don't
                              Just# (Pointer s
v : [Pointer s]
vs) <- Spine s -> Maybe# [Pointer s]
forall s. Spine s -> Maybe# [Pointer s]
sAllApplyElims Spine s
spine -> -- return functions or records.
              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
v [] (QName
-> ([Literal] -> Term)
-> [Literal]
-> [Pointer s]
-> Maybe FastCompiledClauses
-> ControlStack s
-> ControlStack s
forall s.
QName
-> ([Literal] -> Term)
-> [Literal]
-> [Pointer s]
-> Maybe FastCompiledClauses
-> ControlStack s
-> ControlStack s
PrimOpK QName
f [Literal] -> Term
op [] [Pointer s]
vs Maybe FastCompiledClauses
cc ControlStack s
ctrl)
            CPrimOp{} -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done  -- partially applied
            CompactDefn
COther    -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
fallbackEval Eval s
s

        -- Case: zero. Return value closure with literal 0.
        Con ConHead
c ConInfo
i [] | ConHead -> Bool
isZero ConHead
c ->
          Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalTrueValue (Literal -> Term
Lit (Integer -> Literal
LitNat Integer
0)) Env s
forall s. Env s
emptyEnv Spine s
spine ControlStack 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, SApply ArgInfo
_ Pointer s
v : Spine s
_ <- Spine s
spine ->
          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
v [] (ControlStack s -> ControlStack s
forall s. ControlStack s -> ControlStack s
sucCtrl ControlStack 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 represented 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
-> ControlStack 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 ControlStack 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
$ do
              let dontProject :: ST s (Blocked Term)
dontProject = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalTrueValue (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c' ConInfo
i []) Env s
env Spine s
spine ControlStack s
ctrl)

              let doProj :: QName -> [Arg QName] -> Spine s -> Spine s -> ST s (Blocked Term)
doProj QName
p (Arg QName
f:[Arg QName]
fs) (SElim s
a:Spine s
sp) Spine s
restOfElims
                    | Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
p = case SElim s
a of
                                     -- Andreas #2170: fit argToDontCare here?!
                        SApply ArgInfo
_ Pointer s
arg -> 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
arg Spine s
restOfElims ControlStack s
ctrl
                        SElim s
_            -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
                    | Bool
otherwise = QName -> [Arg QName] -> Spine s -> Spine s -> ST s (Blocked Term)
doProj QName
p [Arg QName]
fs Spine s
sp Spine s
restOfElims
                  doProj QName
_ [Arg QName]
_ Spine s
_ Spine s
_ = ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

              let shouldProj :: Spine s -> Int -> ST s (Blocked Term)
shouldProj Spine s
sp Int
0 = case Spine s
sp of
                    SProj ProjOrigin
_ QName
p : Spine s
rest -> QName -> [Arg QName] -> Spine s -> Spine s -> ST s (Blocked Term)
doProj QName
p (ConHead -> [Arg QName]
conFields ConHead
c) Spine s
spine Spine s
rest
                    Spine s
_                -> ST s (Blocked Term)
dontProject
                  shouldProj (SElim s
_ : Spine s
sp) Int
ar = Spine s -> Int -> ST s (Blocked Term)
shouldProj Spine s
sp (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                  shouldProj []       Int
ar = ST s (Blocked Term)
dontProject

              Spine s -> Int -> ST s (Blocked Term)
shouldProj Spine s
spine Int
ar

          | Bool
otherwise -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval 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
-> ControlStack 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 ControlStack 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
$
          Int
-> Env s
-> (Pointer s -> ST s (Blocked Term))
-> (() -> ST s (Blocked Term))
-> ST s (Blocked Term)
forall s a. Int -> Env s -> (Pointer s -> a) -> (() -> a) -> a
lookupEnv Int
x Env s
env
            (\Pointer s
p -> 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
p Spine s
spine ControlStack s
ctrl)
            (\()
_ -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Eval s -> ST s (Blocked Term)) -> Eval s -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval 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 ControlStack 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
            []            -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done
            SElim s
elim : Spine s
spine' ->
               let getArg :: SElim s -> Pointer s
getArg (SApply ArgInfo
_ Pointer s
v)    = Pointer s
v
                   getArg (SIApply Pointer s
_ Pointer s
_ Pointer s
v) = Pointer s
v
                   getArg SProj{}         = Pointer s
forall a. HasCallStack => a
__IMPOSSIBLE__ in
               case Abs Term
b of
                 Abs   String
_ Term
b -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalClosure Term
b (SElim s -> Pointer s
forall {s}. SElim s -> Pointer s
getArg SElim s
elim Pointer s -> Env s -> Env s
forall s. Pointer s -> Env s -> Env s
`extendEnv` Env s
env) Spine s
spine' ControlStack s
ctrl)
                 NoAbs String
_ Term
b -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalClosure Term
b Env s
env Spine s
spine' ControlStack s
ctrl)

        -- 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{} -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalTrueValue Term
t Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl)
        Pi{}  -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done
        DontCare{} -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval 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
-> ControlStack 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 ControlStack s
ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
          case MetaId -> Maybe MetaInstantiation
getMetaInst MetaId
m of
            Maybe MetaInstantiation
Nothing ->
              Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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) ControlStack s
ctrl)
            Just (InstV Instantiation
i) -> do
              spine' <- Env s -> Elims -> Spine s -> ST s (Spine s)
forall s. Env s -> Elims -> Spine s -> ST s (Spine s)
elimsToSpine Env s
env Elims
es Spine s
spine
              let (zs, env, !spine'') = buildEnv (instTel i) spine'
              runEval (evalClosure (lams zs (instBody i)) env spine'' ctrl)
            Just OpenMeta{}                     -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
            Just BlockedConst{}                 -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
            Just PostponedTypeCheckingProblem{} -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

      where done :: Eval s
done = Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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) ControlStack s
ctrl
            shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims Term
t Env s
env0 Env s
env Elims
es = do
              spine' <- Env s -> Elims -> Spine s -> ST s (Spine s)
forall s. Env s -> Elims -> Spine s -> ST s (Spine s)
elimsToSpine Env s
env Elims
es Spine s
spine
              runEval (evalClosure t env0 spine' ctrl)

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

    -- Case NormaliseK: The focus is a weak-head value that should be fully normalised.
    runEval' s :: Eval s
s@(Eval cl :: Closure s
cl@(Closure IsValue
b Term
t Env s
env Spine s
spine) (NormaliseK ControlStack s
ctrl)) =
      case Term
t of
        Def QName
_   [] -> Closure s -> Spine s -> ControlStack 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 ControlStack s
ctrl
        Con ConHead
_ ConInfo
_ [] -> Closure s -> Spine s -> ControlStack 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 ControlStack s
ctrl
        Var Int
_   [] -> Closure s -> Spine s -> ControlStack 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 ControlStack s
ctrl
        MetaV MetaId
_ [] -> Closure s -> Spine s -> ControlStack 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 ControlStack s
ctrl

        Lit{} -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
done

        -- We might get these from fallbackEval
        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
_ -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
fallbackEval Eval s
s -- fallbackEval knows about NormaliseK

      where done :: Eval s
done = Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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) ControlStack s
ctrl
            shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims Term
t Env s
env0 Env s
env Elims
es = do
              spine' <- Env s -> Elims -> Spine s -> ST s (Spine s)
forall s. Env s -> Elims -> Spine s -> ST s (Spine s)
elimsToSpine Env s
env Elims
es Spine s
spine
              runEval (Eval (Closure b t env0 spine') (NormaliseK ctrl))

    -- Case: ArgK: We successfully normalised an argument. Start on the next argument, or if there
    -- isn't one we're done.
    runEval' (Eval Closure s
cl (ArgK Closure s
cl0 SpineContext s
cxt ControlStack 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      -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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) ControlStack s
ctrl)
        Right (Element (SpineContext s)
p, SpineContext s
cxt') -> Pointer s -> Spine 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 [] (ControlStack s -> ControlStack s
forall s. ControlStack s -> ControlStack s
NormaliseK (Closure s -> SpineContext s -> ControlStack s -> ControlStack s
forall s.
Closure s -> SpineContext s -> ControlStack s -> ControlStack s
ArgK Closure s
cl0 SpineContext s
cxt' ControlStack s
ctrl))

    -- Case: NatSucK m

    -- If literal add m to the literal,
    runEval' (Eval cl :: Closure s
cl@(Closure Value{} (Lit (LitNat Integer
n)) Env s
_ Spine s
_) (NatSucK Integer
m ControlStack s
ctrl)) =
      Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval 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 [] ControlStack s
ctrl)

    -- otherwise apply 'suc' m times.
    runEval' (Eval Closure s
cl (NatSucK Integer
m ControlStack s
ctrl)) =
        Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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) ControlStack s
ctrl)
      where
        plus :: Integer -> Closure s -> Closure s
plus Integer
0 Closure s
cl = Closure s
cl
        plus Integer
n Closure s
cl =
          let !(Arg ArgInfo
i Pointer s
arg) = Pointer s -> Arg (Pointer s)
forall a. a -> Arg a
defaultArg (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)) in
          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
$ ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
i Pointer s
arg SElim s -> Spine s -> Spine s
forall a. a -> [a] -> [a]
: []

    -- Case: PrimOpK

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

    -- If not a literal we use the case tree if there is one, otherwise we are stuck.
    runEval' (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 ControlStack s
ctrl)) =
      case Maybe FastCompiledClauses
mcc of
        Maybe FastCompiledClauses
Nothing -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval Closure s
stuck ControlStack s
ctrl)
        Just FastCompiledClauses
cc -> Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc Spine s
spine (CatchallFrames s
forall s. CatchallFrames s
CAFNil CatchallFrames s -> Closure s -> MatchStack s
forall s. CatchallFrames s -> Closure s -> MatchStack s
:> Closure s
notstuck) ControlStack 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 -> SElim s) -> [Pointer s] -> Spine s
forall a b. (a -> b) -> [a] -> [b]
map' (ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
defaultArgInfo) ([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. [a] -> [a] -> [a]
++! (Pointer s
p Pointer s -> [Pointer s] -> [Pointer s]
forall 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.
    runEval' (Eval arg :: Closure s
arg@(Closure (Value Blocked_
blk) Term
t Env s
_ Spine s
_) (ForceK QName
pf Spine s
spine0 Spine s
spine1 ControlStack s
ctrl))
      | Term -> Bool
isCanonical Term
t =
        case Spine s
spine1 of
          SApply ArgInfo
_ Pointer s
k : Spine s
spine' ->
            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
k (SElim s
elim SElim s -> Spine s -> Spine s
forall a. a -> [a] -> [a]
: Spine s
spine') ControlStack s
ctrl
          [] -> -- Partial application of primForce to canonical argument, return λ k → k arg.
            Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalTrueValue (Arg String -> Term -> Term
lam (String -> Arg String
forall a. a -> Arg a
defaultArg String
"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 (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (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) [] ControlStack s
ctrl)
          Spine s
_ -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval Closure s
stuck ControlStack s
ctrl)
      where
        argPtr :: Pointer s
argPtr = Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk Closure s
arg
        elim :: SElim s
elim   = ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
defaultArgInfo Pointer s
argPtr
        spine' :: Spine s
spine' = Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! (SElim s
elim SElim s -> Spine s -> Spine s
forall 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.
    runEval' (Eval cl2 :: Closure s
cl2@(Closure Value{} Term
arg2 Env s
_ Spine s
_) (EraseK QName
f Spine s
spine0 [SApply ArgInfo
_ Pointer s
p1] Spine s
_ Spine s
spine3 ControlStack s
ctrl)) =
      Pointer s -> ST s (Closure s)
forall s. Pointer s -> ST s (Thunk s)
derefPointer_ Pointer s
p1 ST s (Closure s)
-> (Closure s -> ST s (Blocked Term)) -> ST s (Blocked Term)
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Closure s
BlackHole -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
        cl1 :: Closure s
cl1@(Closure IsValue
_ Term
arg1 Env s
_ Spine s
sp1) -> 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 ->
            Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval 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 [] ControlStack s
ctrl)
          (Term, Term)
_ ->
            let !i :: ArgInfo
i = ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
hide ArgInfo
defaultArgInfo
                !spine :: Spine s
spine = Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! (Closure s -> SElim s) -> [Closure s] -> Spine s
forall a b. (a -> b) -> [a] -> [b]
map' (ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
i (Pointer s -> SElim s)
-> (Closure s -> Pointer s) -> Closure s -> SElim 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
            Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
fallbackEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalClosure (QName -> Elims -> Term
Def QName
f []) Env s
forall s. Env s
emptyEnv Spine s
spine ControlStack s
ctrl)
    runEval' (Eval cl1 :: Closure s
cl1@(Closure Value{} Term
_ Env s
_ Spine s
_) (EraseK QName
f Spine s
spine0 [] [SApply ArgInfo
_ Pointer s
p2] Spine s
spine3 ControlStack s
ctrl)) =
      let !i :: ArgInfo
i = ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
hide ArgInfo
defaultArgInfo
          !thcl1 :: Pointer s
thcl1 = Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk Closure s
cl1 in
      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
p2 [] (QName
-> Spine s
-> Spine s
-> Spine s
-> Spine s
-> ControlStack s
-> ControlStack s
forall s.
QName
-> Spine s
-> Spine s
-> Spine s
-> Spine s
-> ControlStack s
-> ControlStack s
EraseK QName
f Spine s
spine0 [ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
i Pointer s
thcl1] [] Spine s
spine3 ControlStack s
ctrl)
    runEval' (Eval Closure s
_ (EraseK{})) =
      ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

    -- Case: ApplyK. Application after thunk update. Add the spine from the control frame to the
    -- closure.
    runEval' (Eval cl :: Closure s
cl@(Closure Value{} Term
_ Env s
_ Spine s
_) (ApplyK Spine s
spine ControlStack s
ctrl)) =
      Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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)

    -- 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.
    runEval' (Eval cl :: Closure s
cl@(Closure (Value Blocked_
blk) Term
t Env s
env Spine s
spine) ctrl0 :: ControlStack s
ctrl0@(CaseK QName
f ArgInfo
i FastCase FastCompiledClauses
bs Spine s
spine0 Spine s
spine1 MatchStack s
stack ControlStack s
ctrl)) =
      {-# SCC "runEval.CaseK" #-}
      case Blocked_
blk of
        Blocked{} | [()] -> Bool
forall a. Null a => 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 -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl

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

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

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

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

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

        -- This the spine at this point in the matching. A catch-all match doesn't change the spine.
        catchallSpine :: Spine s
catchallSpine = Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! (ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
i Pointer s
p SElim s -> Spine s -> Spine s
forall 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 ->
          Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine1) MatchStack s
catchallStack ControlStack 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 ->
          Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc Spine s
catchallSpine MatchStack s
stack ControlStack 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 ->
          Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine1) MatchStack s
catchallStack ControlStack 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 ->
            Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine1) MatchStack s
catchallStack ControlStack 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 ->
            let !arg' :: SElim s
arg' = ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
defaultArgInfo Pointer s
arg in
            Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! (SElim s
arg' SElim s -> Spine s -> Spine s
forall a. a -> [a] -> [a]
: Spine s
spine1)) MatchStack s
catchallStack ControlStack 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
    runMatch' :: Match s -> ST s (Blocked Term)
    runMatch' :: forall s. Match s -> ST s (Blocked Term)
runMatch' (Match QName
f FastCompiledClauses
cc Spine s
spine MatchStack s
stack ControlStack s
ctrl) = {-# SCC "runMatch" #-}
      case FastCompiledClauses
cc of
        -- Absurd match. You can get here for open terms.
        FastCompiledClauses
FFail -> Blocked_ -> MatchStack s -> ControlStack 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 ControlStack s
ctrl

        -- Matching complete. Compute the environment for the body and switch to the Eval state.
        FDone (CCDone Int
_ ClauseRecursive
mr [Arg String]
xs Term
body) -> do
          let allowedReductions :: SmallSet AllowedReduction
allowedReductions = ReduceEnv -> TCEnv
redEnv ReduceEnv
rEnv TCEnv
-> Getting
     (SmallSet AllowedReduction) TCEnv (SmallSet AllowedReduction)
-> SmallSet AllowedReduction
forall s a. s -> Getting a s a -> a
^. Getting
  (SmallSet AllowedReduction) TCEnv (SmallSet AllowedReduction)
Lens' TCEnv (SmallSet AllowedReduction)
eAllowedReductions
          let undo :: ST s (Blocked Term)
undo = Blocked_ -> MatchStack s -> ControlStack 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
ReallyNotBlocked ()) MatchStack s
stack ControlStack s
ctrl
          let abort :: Bool
abort =
                  ClauseRecursive -> Bool
couldBeRecursive ClauseRecursive
mr
               Bool -> Bool -> Bool
&& CompactDef -> Bool
cdefUnconfirmed (QName -> CompactDef
constInfo QName
f)
               Bool -> Bool -> Bool
&& (AllowedReduction
UnconfirmedReductions AllowedReduction -> SmallSet AllowedReduction -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.notMember` SmallSet AllowedReduction
allowedReductions)
          if Bool
abort then ST s (Blocked Term)
undo else do
            let (![Arg String]
zs, !Env s
env, !Spine s
spine') = [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
forall s. [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv [Arg String]
xs Spine s
spine
            Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled ([Arg String] -> Term -> Term
lams [Arg String]
zs Term
body) Env s
env Spine s
spine') ControlStack 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 -> do

              -- Recurse down to the application, replace it by projections
              -- in the spine, rebuild the spine. If we don't have enough
              -- arguments, return Nothing#
          let go :: Int -> Spine s -> ST s (Maybe# (Spine s))
go Int
0 (SApply ArgInfo
_ Pointer s
e : Spine s
spine1) = do Spine s -> Maybe# (Spine s)
forall a. a -> Maybe# a
Just# (Spine s -> Maybe# (Spine s))
-> ST s (Spine s) -> ST s (Maybe# (Spine s))
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> [Arg QName] -> Pointer s -> Spine s -> ST s (Spine s)
forall {s}. [Arg QName] -> Pointer s -> [SElim s] -> ST s [SElim s]
goFs [Arg QName]
fs Pointer s
e Spine s
spine1
              go Int
n (SElim s
e : Spine s
spine1) = Int -> Spine s -> ST s (Maybe# (Spine s))
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Spine s
spine1 ST s (Maybe# (Spine s))
-> (Maybe# (Spine s) -> ST s (Maybe# (Spine s)))
-> ST s (Maybe# (Spine s))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Maybe# (Spine s)
Nothing# -> Maybe# (Spine s) -> ST s (Maybe# (Spine s))
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe# (Spine s)
forall a. Maybe# a
Nothing#
                Just# Spine s
sp -> Maybe# (Spine s) -> ST s (Maybe# (Spine s))
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe# (Spine s) -> ST s (Maybe# (Spine s)))
-> Maybe# (Spine s) -> ST s (Maybe# (Spine s))
forall a b. (a -> b) -> a -> b
$! Spine s -> Maybe# (Spine s)
forall a. a -> Maybe# a
Just# (Spine s -> Maybe# (Spine s)) -> Spine s -> Maybe# (Spine s)
forall a b. (a -> b) -> a -> b
$! SElim s
eSElim s -> Spine s -> Spine s
forall a. a -> [a] -> [a]
:Spine s
sp
              go Int
_ [] = Maybe# (Spine s) -> ST s (Maybe# (Spine s))
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe# (Spine s)
forall a. Maybe# a
Nothing#

              -- Replace e by its projections in the spine.
              goFs :: [Arg QName] -> Pointer s -> [SElim s] -> ST s [SElim s]
goFs []     Pointer s
e [SElim s]
spine1 = [SElim s] -> ST s [SElim s]
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SElim s]
spine1
              goFs (Arg QName
f:[Arg QName]
fs) Pointer s
e [SElim s]
spine1 = do
                let projClosure :: Arg QName -> Closure s
projClosure (Arg ArgInfo
ai QName
f) =
                       IsValue -> Term -> Env s -> [SElim 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 Pointer s
e Env s
forall s. Env s
emptyEnv) [ProjOrigin -> QName -> SElim s
forall s. ProjOrigin -> QName -> SElim s
SProj ProjOrigin
ProjSystem QName
f]
                !t <- ArgInfo -> Pointer s -> SElim s
forall s. ArgInfo -> Pointer s -> SElim s
SApply ArgInfo
defaultArgInfo (Pointer s -> SElim s) -> ST s (Pointer s) -> ST s (SElim s)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Closure s -> ST s (Pointer s)
forall s. Closure s -> ST s (Pointer s)
createThunk (Arg QName -> Closure s
projClosure Arg QName
f)
                (t:) <$!> goFs fs e spine1

          Int -> Spine s -> ST s (Maybe# (Spine s))
go Int
n Spine s
spine ST s (Maybe# (Spine s))
-> (Maybe# (Spine s) -> ST s (Blocked Term)) -> ST s (Blocked Term)
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe# (Spine s)
Nothing# ->
              -- Question: add lambda here? doesn't matter for equality, but might for
              -- rewriting or 'with'
              NotBlocked' Term -> ST s (Blocked Term)
done NotBlocked' Term
forall t. NotBlocked' t
Underapplied
            Just# Spine s
spine' -> do
              let !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
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
              Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc Spine s
spine' MatchStack s
stack' ControlStack s
ctrl)

        -- 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, SApply ArgInfo
i Pointer s
e : Spine s
spine1) ->
              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
e [] (ControlStack s -> ST s (Blocked Term))
-> ControlStack s -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName
-> ArgInfo
-> FastCase FastCompiledClauses
-> Spine s
-> Spine s
-> MatchStack s
-> ControlStack s
-> ControlStack s
forall s.
QName
-> ArgInfo
-> FastCase FastCompiledClauses
-> Spine s
-> Spine s
-> MatchStack s
-> ControlStack s
-> ControlStack s
CaseK QName
f ArgInfo
i FastCase FastCompiledClauses
bs Spine s
spine0 Spine s
spine1 MatchStack s
stack ControlStack 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, SProj ProjOrigin
o QName
p : Spine s
spine1) ->
              case QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
lookupCon QName
p FastCase FastCompiledClauses
bs Maybe FastCompiledClauses
-> Maybe FastCompiledClauses -> Maybe FastCompiledClauses
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
`lookupCon` FastCase FastCompiledClauses
bs) (QName -> Maybe FastCompiledClauses)
-> Maybe QName -> Maybe FastCompiledClauses
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe QName
op) of
                Maybe FastCompiledClauses
Nothing
                  | QName
f QName -> Set QName -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
partialDefs -> Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch (NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) MatchStack s
stack ControlStack s
ctrl
                  | Bool
otherwise          -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
                Just FastCompiledClauses
cc -> Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine1) MatchStack s
stack ControlStack s
ctrl)
              where CFun{ cfunProjection :: CompactDefn -> Maybe QName
cfunProjection = Maybe QName
op } = CompactDef -> CompactDefn
cdefDef (QName -> CompactDef
constInfo QName
p)
            (Spine s
_, SIApply{} : 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 -> ControlStack 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 ControlStack 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 = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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 (Closure s)
forall s. STPointer s -> ST s (Thunk s)
readPointer STPointer s
p ST s (Closure s)
-> (Closure s -> ST s (Blocked Term)) -> ST s (Blocked Term)
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      Closure s
BlackHole -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
      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
        let !ctrl' :: ControlStack s
ctrl' = if Bool -> Bool
not (Spine s -> Bool
forall a. Null a => a -> Bool
null Spine s
spine) then Spine s -> ControlStack s -> ControlStack s
forall s. Spine s -> ControlStack s -> ControlStack s
ApplyK Spine s
spine ControlStack s
ctrl else ControlStack s
ctrl
        Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval Closure s
cl (STPointer s -> ControlStack s -> ControlStack s
forall s. STPointer s -> ControlStack s -> ControlStack s
updateThunkCtrl STPointer s
p ControlStack s
ctrl'))
      cl :: Closure s
cl@(Closure IsValue
_ Term
_ Env s
_ Spine s
_) -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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)

    {-# INLINE evalIApplyAM #-}
    -- '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 (SIApply Pointer s
x Pointer s
y Pointer s
r : Spine s
es) = do
          br <- Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
r [] ControlStack s
forall s. ControlStack s
EmptyK
          case iview $ ignoreBlocking br of
            IntervalView
IZero -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
x Spine s
es ControlStack s
ctrl
            IntervalView
IOne  -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
y Spine s
es ControlStack s
ctrl
            IntervalView
_     -> (Blocked Term -> Blocked Term -> Blocked Term
forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Blocked Term
br) (Blocked Term -> Blocked Term)
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spine s -> ST s (Blocked Term)
go Spine s
es
        go (SElim 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 = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval Closure s
cl ControlStack s
ctrl)  -- nothing to do
    normaliseArgsAM Closure s
cl [SElim 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 [SElim 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       -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval (Closure s -> [SElim s] -> Closure s
forall s. Closure s -> Spine s -> Closure s
clApply_ Closure s
cl [SElim s]
spine) ControlStack s
ctrl)
        Just (Element (SpineContext s)
p, SpineContext s
cxt) -> Pointer s -> [SElim 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 [] (ControlStack s -> ControlStack s
forall s. ControlStack s -> ControlStack s
NormaliseK (Closure s -> SpineContext s -> ControlStack s -> ControlStack s
forall s.
Closure s -> SpineContext s -> ControlStack s -> ControlStack s
ArgK Closure s
cl SpineContext s
cxt 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.
    fallbackEval :: Eval s -> ST s (Blocked Term)
    fallbackEval :: forall s. Eval s -> ST s (Blocked Term)
fallbackEval (Eval Closure s
c ControlStack s
ctrl) = do
        v <- Closure s -> ST s Term
forall s. Closure s -> ST s Term
decodeClosure_ Closure s
c
        runEval (mkValue $ runReduce $ slow v)
      where mkValue :: Blocked Term -> Eval s
mkValue Blocked Term
b = Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalValue (() () -> Blocked Term -> Blocked_
forall a b. a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked Term
b) (Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
b) Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl'
            (Term -> ReduceM (Blocked Term)
slow, ControlStack s
ctrl') = case ControlStack s
ctrl of
              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)

    -- 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.
    rewriteEval :: Eval s -> ST s (Blocked Term)
    rewriteEval :: forall s. Eval s -> ST s (Blocked Term)
rewriteEval s :: Eval s
s@(Eval (Closure (Value Blocked_
blk) Term
t Env s
env Spine s
spine) ControlStack s
ctrl)
      | RewriteRules -> Bool
forall a. Null a => a -> Bool
null RewriteRules
rewr = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval Eval s
s
      | Bool
otherwise = Doc -> ST s (Blocked Term) -> ST s (Blocked Term)
forall a. Doc -> a -> a
traceDoc (Doc
"R" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Eval s -> Doc
forall a. Pretty a => a -> Doc
pretty Eval s
s) (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ do
        v0 <- Closure s -> ST s Term
forall s. Closure s -> ST s Term
decodeClosure_ (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled Term
t Env s
env [])
        es <- decodeSpine spine
        case runReduce (rewrite blk (applyE v0) rewr es) of
          NoReduction Blocked Term
b    -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalValue (() () -> Blocked Term -> Blocked_
forall a b. a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked Term
b) (Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
b) Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl)
          YesReduction Simplification
_ Term
v -> Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
runEval (Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}. Term -> Env s -> Spine s -> ControlStack s -> Eval 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)
                     Var Int
x Elims
_    -> Int -> RewriteRules
localRewr Int
x
                     Term
_          -> RewriteRules
forall a. HasCallStack => a
__IMPOSSIBLE__
    rewriteEval Eval 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 ControlStack s
ctrl) = Integer -> ControlStack s -> ControlStack s
forall s. Integer -> ControlStack s -> ControlStack s
NatSucK (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) ControlStack s
ctrl
    sucCtrl             ControlStack s
ctrl  = Integer -> ControlStack s -> ControlStack s
forall s. Integer -> ControlStack s -> ControlStack s
NatSucK Integer
1 ControlStack 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 ControlStack s
ctrl) = [STPointer s] -> ControlStack s -> ControlStack s
forall s. [STPointer s] -> ControlStack s -> ControlStack s
UpdateThunk (STPointer s
p STPointer s -> [STPointer s] -> [STPointer s]
forall a. a -> [a] -> [a]
: [STPointer s]
ps) ControlStack s
ctrl
    updateThunkCtrl STPointer s
p                 ControlStack s
ctrl  = [STPointer s] -> ControlStack s -> ControlStack s
forall s. [STPointer s] -> ControlStack s -> ControlStack s
UpdateThunk [STPointer s
p] ControlStack 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 (CatchallFrames s
_ :> Closure s
cl) ControlStack s
ctrl = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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 (CAFCons (Catchall FastCompiledClauses
cc Spine s
spine) CatchallFrames s
stack :> Closure s
cl) ControlStack s
ctrl = Match s -> ST s (Blocked Term)
forall s. Match s -> ST s (Blocked Term)
runMatch (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> Match s
Match QName
f FastCompiledClauses
cc Spine s
spine (CatchallFrames s
stack CatchallFrames s -> Closure s -> MatchStack s
forall s. CatchallFrames s -> Closure s -> MatchStack s
:> Closure s
cl) ControlStack s
ctrl)
    failedMatch QName
f (CatchallFrames s
CAFNil :> Closure s
cl) ControlStack s
ctrl
        -- Bad work-around for #3870: don't fail hard during instance search.
      | Bool
speculative          = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval (Blocked_ -> Closure s -> Closure s
forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) Closure s
cl) ControlStack s
ctrl)
      | QName
f QName -> Set QName -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
partialDefs = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval (Blocked_ -> Closure s -> Closure s
forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) Closure s
cl) ControlStack s
ctrl)
      | Bool
otherwise            = Eval s -> ST s (Blocked Term)
forall s. Eval s -> ST s (Blocked Term)
rewriteEval (Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval s
Eval (Blocked_ -> Closure s -> Closure s
forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()) Closure s
cl) ControlStack s
ctrl)  -- See #5396

    -- Some helper functions to build machine states and closures.
    evalClosure :: Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalClosure Term
t Env s
env Spine s
spine = Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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 -> Eval s
evalValue Blocked_
b Term
t Env s
env Spine s
spine = Closure s -> ControlStack s -> Eval s
forall s. Closure s -> ControlStack s -> Eval 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 -> Eval s
evalTrueValue           = Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
forall {s}.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s
evalValue (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval s)
-> Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> Eval 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 String] -> Term -> Term
lams [Arg String]
xs Term
t = (Arg String -> Term -> Term) -> Term -> [Arg String] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' Arg String -> Term -> Term
lam Term
t [Arg String]
xs

    lam :: Arg String -> Term -> Term
    lam :: Arg String -> Term -> Term
lam Arg String
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Arg String -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg String
x) (String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs (Arg String -> String
forall e. Arg e -> e
unArg Arg String
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 CCDone Term
done) = CCDone Term -> Doc
forall a. Pretty a => a -> Doc
pretty CCDone Term
done
  pretty FastCompiledClauses
FFail        = Doc
"fail"
  pretty (FEta Int
n [Arg QName]
_ FastCompiledClauses
cc Maybe FastCompiledClauses
ca) =
    String -> Doc
forall a. String -> Doc a
text (String
"eta " String -> ShowS
forall a. [a] -> [a] -> [a]
++! Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++! String
" 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 [ String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"project " String -> ShowS
forall a. [a] -> [a] -> [a]
++! Int -> String
forall a. Show a => a -> String
show Int
n
        , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FastCase FastCompiledClauses -> Doc
forall a. Pretty a => a -> Doc
pretty FastCase FastCompiledClauses
bs
        ]
  pretty (FCase Int
n FastCase FastCompiledClauses
bs) =
    String -> Doc
forall a. String -> Doc a
text (String
"case " String -> ShowS
forall a. [a] -> [a] -> [a]
++! Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++! String
" of") Doc -> Doc -> Doc
<?> FastCase FastCompiledClauses -> Doc
forall a. Pretty a => a -> Doc
pretty FastCase FastCompiledClauses
bs

instance Pretty (Pointer s) where
  prettyPrec :: Int -> Pointer s -> Doc
prettyPrec Int
p = Int -> Thunk s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p (Thunk s -> Doc) -> (Pointer s -> Thunk s) -> Pointer s -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pointer s -> Thunk s
forall s. Pointer s -> Thunk 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 [ String -> Doc
forall a. String -> Doc a
text String
tag
                           , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Term
t
                           , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Integer -> Pointer s -> Doc) -> [Integer] -> [Pointer s] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Integer -> Pointer s -> Doc
forall {a} {a}. (Show a, Pretty a) => a -> a -> Doc
envEntry [Integer
0..] (Env s -> [Pointer s]
forall s. Env s -> [Pointer s]
envToList Env s
env)
                           , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ((SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
spine) ]
      where envEntry :: a -> a -> Doc
envEntry a
i a
c = String -> Doc
forall a. String -> Doc a
text (String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++! a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++! String
" =") Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
c
            tag :: String
tag = case IsValue
isV of Value{} -> String
"V"; IsValue
Unevaled -> String
"E"
  prettyPrec Int
_ Closure s
BlackHole         = Doc
"<BLACKHOLE>"

instance Pretty (Eval s) where
  prettyPrec :: Int -> Eval 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
pretty ControlStack s
ctrl

instance Pretty (Match s) where
  prettyPrec :: Int -> Match s -> Doc
prettyPrec Int
p (Match QName
f FastCompiledClauses
cc Spine s
sp MatchStack s
stack ControlStack s
ctrl) =
    Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"M" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
                          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ((SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
sp)
                          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> FastCompiledClauses -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 FastCompiledClauses
cc
                          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ MatchStack s -> Doc
forall a. Pretty a => a -> Doc
pretty MatchStack s
stack
                          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ControlStack s -> Doc
forall a. Pretty a => a -> Doc
pretty 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 (CatchallFrames s
CAFNil :> Closure s
_) = Doc
forall a. Null a => a
empty
  pretty (CatchallFrames s
ca     :> Closure s
_) = [CatchallFrame s] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([CatchallFrame s] -> Doc) -> [CatchallFrame s] -> Doc
forall a b. (a -> b) -> a -> b
$ CatchallFrames s -> [CatchallFrame s]
forall {s}. CatchallFrames s -> [CatchallFrame s]
asList CatchallFrames s
ca where
    asList :: CatchallFrames s -> [CatchallFrame s]
asList CatchallFrames s
CAFNil         = []
    asList (CAFCons CatchallFrame s
c CatchallFrames s
cs) = (CatchallFrame s
c CatchallFrame s -> [CatchallFrame s] -> [CatchallFrame s]
forall a. a -> [a] -> [a]
:) ([CatchallFrame s] -> [CatchallFrame s])
-> [CatchallFrame s] -> [CatchallFrame s]
forall a b. (a -> b) -> a -> b
$! CatchallFrames s -> [CatchallFrame s]
asList CatchallFrames s
cs

instance Pretty (ControlStack s) where
  prettyPrec :: Int -> ControlStack s -> Doc
prettyPrec Int
p (CaseK QName
f ArgInfo
_ FastCase FastCompiledClauses
_ Spine s
_ Spine s
_ MatchStack s
mc ControlStack s
ct)       = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ((Doc
"CaseK" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty (QName -> Name
qnameName QName
f)) Doc -> Doc -> Doc
<?> MatchStack s -> Doc
forall a. Pretty a => a -> Doc
pretty MatchStack s
mc)
                                               Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct

  prettyPrec Int
p (ForceK QName
_ Spine s
spine0 Spine s
spine1 ControlStack s
ct)   = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (
                                               Doc
"ForceK" Doc -> Doc -> Doc
<?> [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ((SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. [a] -> [a] -> [a]
++! Spine s
spine1)))
                                               Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (EraseK QName
_ Spine s
sp0 Spine s
sp1 Spine s
sp2 Spine s
sp3 ControlStack s
ct) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
                                               [ Doc
"EraseK"
                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([Elim' (Pointer s)] -> Doc) -> [Elim' (Pointer s)] -> Doc
forall a b. (a -> b) -> a -> b
$ (SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
sp0
                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([Elim' (Pointer s)] -> Doc) -> [Elim' (Pointer s)] -> Doc
forall a b. (a -> b) -> a -> b
$ (SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
sp1
                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([Elim' (Pointer s)] -> Doc) -> [Elim' (Pointer s)] -> Doc
forall a b. (a -> b) -> a -> b
$ (SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
sp2
                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([Elim' (Pointer s)] -> Doc) -> [Elim' (Pointer s)] -> Doc
forall a b. (a -> b) -> a -> b
$ (SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
sp3 ])
                                               Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct

  prettyPrec Int
p (NatSucK Integer
n ControlStack s
ct)            = String -> Doc
forall a. String -> Doc a
text (String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++! Integer -> String
forall a. Show a => a -> String
show Integer
n)
                                           Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (PrimOpK QName
f [Literal] -> Term
_ [Literal]
vs [Pointer s]
cls Maybe FastCompiledClauses
_ ControlStack s
ct) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"PrimOpK" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
                                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Literal] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Literal]
vs
                                                                , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Pointer s] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Pointer s]
cls ])
                                          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (UpdateThunk [STPointer s]
ps ControlStack s
ct)      = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc
"UpdateThunk" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text (Int -> String
forall a. Show a => a -> String
show ([STPointer s] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [STPointer s]
ps)))
                                          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (ApplyK Spine s
spine ControlStack s
ct)        = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc
"ApplyK" Doc -> Doc -> Doc
<?> [Elim' (Pointer s)] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ((SElim s -> Elim' (Pointer s)) -> Spine s -> [Elim' (Pointer s)]
forall a b. (a -> b) -> [a] -> [b]
map' SElim s -> Elim' (Pointer s)
forall s. SElim s -> Elim' (Pointer s)
sElimToElim Spine s
spine))
                                          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (NormaliseK ControlStack s
ct)          = Doc
"NormaliseK"
                                          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p (ArgK Closure s
cl SpineContext s
_ ControlStack s
ct)           = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"ArgK" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Closure s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Closure s
cl ])
                                          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> ControlStack s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p ControlStack s
ct
  prettyPrec Int
p ControlStack s
EmptyK                   = Doc
"EmptyK"