{-# LANGUAGE PatternGuards #-}

{-|

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

Some other tricks that improves performance:

- Memoise getConstInfo.

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

- Optimised case trees.

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

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

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

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

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

import Prelude hiding ((!!))

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

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

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

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

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

import Agda.Interaction.Options

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

import Agda.Utils.Impossible

import Debug.Trace

-- * Compact definitions

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

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

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

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

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

  -- WARNING: don't use isPropM here because it relies on reduction,
  -- which causes an infinite loop.
  let isPrp :: Bool
isPrp = case forall a. LensSort a => a -> Sort
getSort (Definition -> Type
defType Definition
def) of
        Prop{} -> Bool
True
        Sort
_      -> Bool
False
  let irr :: Bool
irr = Bool
isPrp Bool -> Bool -> Bool
|| forall a. LensRelevance a => a -> Bool
isIrrelevant (Definition -> ArgInfo
defArgInfo Definition
def)

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

  CompactDefn
cdefn <-
    case Definition -> Defn
theDef Definition
def of
      Defn
_ | Bool
irr Bool -> Bool -> Bool
|| Bool
dontReduce -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
      Defn
_ | forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) forall a. Eq a => a -> a -> Bool
== BuiltinEnv -> Maybe QName
bPrimForce BuiltinEnv
bEnv   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CForce
      Defn
_ | forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) 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
_ | forall a. Sized a => a -> Int
size Tele (Dom Type)
tel forall a. Eq a => a -> a -> Bool
== Int
5 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CErase
                       | Bool
otherwise     -> 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 forall a. Eq a => a -> a -> Bool
/= forall t. Blocked' t ()
notBlocked_ -> 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} -> 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} ->
        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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall a. a -> Maybe a
Just Either ProjectionLikenessMissing Projection
proj }
      Function{funClauses :: Defn -> [Clause]
funClauses = []}      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
      Function{}                     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther -- Incomplete definition
      Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
Nothing} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CTyCon
      Record{recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
Nothing}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CTyCon
      Datatype{}                     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther -- TODO
      Record{}                       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther -- TODO
      Axiom{}                        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
      DataOrRecSig{}                 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
      AbstractDefn{}                 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
      GeneralizableVar{}             -> forall a. HasCallStack => a
__IMPOSSIBLE__
      PrimitiveSort{}                -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther -- TODO
      Primitive{ primName :: Defn -> VerboseKey
primName = VerboseKey
name, primCompiled :: Defn -> Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
cc } ->
        case VerboseKey
name of
          -- "primShowInteger"            -- integers are not literals

          -- Natural numbers
          VerboseKey
"primNatPlus"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Literal] -> Term
natOp forall a. Num a => a -> a -> a
(+)
          VerboseKey
"primNatMinus"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Literal] -> Term
natOp (\ Integer
x Integer
y -> forall a. Ord a => a -> a -> a
max Integer
0 (Integer
x forall a. Num a => a -> a -> a
- Integer
y))
          VerboseKey
"primNatTimes"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Literal] -> Term
natOp forall a. Num a => a -> a -> a
(*)
          VerboseKey
"primNatDivSucAux"           -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
4 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer -> Integer -> Integer)
-> [Literal] -> Term
natOp4 forall {a}. Integral a => a -> a -> a -> a -> a
divAux
          VerboseKey
"primNatModSucAux"           -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
4 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer -> Integer -> Integer)
-> [Literal] -> Term
natOp4 forall {a}. Integral a => a -> a -> a -> a -> a
modAux
          VerboseKey
"primNatLess"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Bool) -> [Literal] -> Term
natRel forall a. Ord a => a -> a -> Bool
(<)
          VerboseKey
"primNatEquality"            -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Bool) -> [Literal] -> Term
natRel forall a. Eq a => a -> a -> Bool
(==)

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

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

          -- Floats
          VerboseKey
"primFloatInequality"        -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Bool) -> [Literal] -> Term
floatRel forall a. Ord a => a -> a -> Bool
(<=)
          VerboseKey
"primFloatEquality"          -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Bool) -> [Literal] -> Term
floatRel forall a. Eq a => a -> a -> Bool
(==)
          VerboseKey
"primFloatLess"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Bool) -> [Literal] -> Term
floatRel forall a. Ord a => a -> a -> Bool
(<)
          VerboseKey
"primFloatIsInfinite"        -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Bool) -> [Literal] -> Term
floatPred forall a. RealFloat a => a -> Bool
isInfinite
          VerboseKey
"primFloatIsNaN"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Bool) -> [Literal] -> Term
floatPred forall a. RealFloat a => a -> Bool
isNaN
          VerboseKey
"primFloatIsDenormalized"    -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Bool) -> [Literal] -> Term
floatPred forall a. RealFloat a => a -> Bool
isDenormalized
          VerboseKey
"primFloatIsNegativeZero"    -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Bool) -> [Literal] -> Term
floatPred forall a. RealFloat a => a -> Bool
isNegativeZero
          VerboseKey
"primFloatIsSafeInteger"     -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Bool) -> [Literal] -> Term
floatPred Double -> Bool
isSafeInteger
          -- "primFloatToWord64"          -- returns a maybe
          -- "primFloatToWord64Injective" -- identities are not literals
          VerboseKey
"primNatToFloat"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitNat Integer
a] -> Double -> Term
float (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
a)
          -- "primIntToFloat"             -- integers are not literals
          -- "primFloatRound"             -- integers and maybe are not literals
          -- "primFloatFloor"             -- integers and maybe are not literals
          -- "primFloatCeiling"           -- integers and maybe are not literals
          -- "primFloatToRatio"           -- integers and sigma are not literals
          -- "primRatioToFloat"           -- integers are not literals
          -- "primFloatDecode"            -- integers and sigma are not literals
          -- "primFloatEncode"            -- integers are not literals
          VerboseKey
"primFloatPlus"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp forall a. Num a => a -> a -> a
(+)
          VerboseKey
"primFloatMinus"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp (-)
          VerboseKey
"primFloatTimes"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp forall a. Num a => a -> a -> a
(*)
          VerboseKey
"primFloatNegate"            -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Num a => a -> a
negate
          VerboseKey
"primFloatDiv"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp forall a. Fractional a => a -> a -> a
(/)
          VerboseKey
"primFloatSqrt"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
sqrt
          VerboseKey
"primFloatExp"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
exp
          VerboseKey
"primFloatLog"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
log
          VerboseKey
"primFloatSin"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
sin
          VerboseKey
"primFloatCos"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
cos
          VerboseKey
"primFloatTan"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
tan
          VerboseKey
"primFloatASin"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
asin
          VerboseKey
"primFloatACos"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
acos
          VerboseKey
"primFloatATan"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
atan
          VerboseKey
"primFloatATan2"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp forall a. RealFloat a => a -> a -> a
atan2
          VerboseKey
"primFloatSinh"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
sinh
          VerboseKey
"primFloatCosh"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
cosh
          VerboseKey
"primFloatTanh"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
tanh
          VerboseKey
"primFloatASinh"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
asinh
          VerboseKey
"primFloatACosh"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
acosh
          VerboseKey
"primFloatATanh"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> [Literal] -> Term
floatFun forall a. Floating a => a -> a
atanh
          VerboseKey
"primFloatPow"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp forall a. Floating a => a -> a -> a
(**)
          VerboseKey
"primShowFloat"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitFloat Double
a] -> VerboseKey -> Term
string (forall a. Show a => a -> VerboseKey
show Double
a)

          -- Characters
          VerboseKey
"primCharEquality"           -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ (Char -> Char -> Bool) -> [Literal] -> Term
charRel forall a. Eq a => a -> a -> Bool
(==)
          VerboseKey
"primIsLower"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isLower
          VerboseKey
"primIsDigit"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isDigit
          VerboseKey
"primIsAlpha"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isAlpha
          VerboseKey
"primIsSpace"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isSpace
          VerboseKey
"primIsAscii"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isAscii
          VerboseKey
"primIsLatin1"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isLatin1
          VerboseKey
"primIsPrint"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isPrint
          VerboseKey
"primIsHexDigit"             -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isHexDigit
          VerboseKey
"primToUpper"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Literal] -> Term
charFun Char -> Char
toUpper
          VerboseKey
"primToLower"                -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Literal] -> Term
charFun Char -> Char
toLower
          VerboseKey
"primCharToNat"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitChar Char
a] -> Integer -> Term
nat (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Enum a => a -> Int
fromEnum Char
a))
          VerboseKey
"primNatToChar"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitNat Integer
a] -> Char -> Term
char (Integer -> Char
integerToChar Integer
a)
          VerboseKey
"primShowChar"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [Literal
a] -> VerboseKey -> Term
string (forall a. Pretty a => a -> VerboseKey
prettyShow Literal
a)

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

          -- "primErase"
          -- "primForce"
          -- "primForceLemma"
          VerboseKey
"primQNameEquality"          -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ \ [LitQName QName
a, LitQName QName
b] -> Bool -> Term
bool (QName
b forall a. Eq a => a -> a -> Bool
== QName
a)
          VerboseKey
"primQNameLess"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ \ [LitQName QName
a, LitQName QName
b] -> Bool -> Term
bool (QName
b forall a. Ord a => a -> a -> Bool
< QName
a)
          VerboseKey
"primShowQName"              -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitQName QName
a] -> VerboseKey -> Term
string (forall a. Pretty a => a -> VerboseKey
prettyShow QName
a)
          -- "primQNameFixity"            -- fixities are not literals (TODO)
          VerboseKey
"primMetaEquality"           -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ \ [LitMeta TopLevelModuleName
_ MetaId
a, LitMeta TopLevelModuleName
_ MetaId
b] -> Bool -> Term
bool (MetaId
b forall a. Eq a => a -> a -> Bool
== MetaId
a)
          VerboseKey
"primMetaLess"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
2 forall a b. (a -> b) -> a -> b
$ \ [LitMeta TopLevelModuleName
_ MetaId
a, LitMeta TopLevelModuleName
_ MetaId
b] -> Bool -> Term
bool (MetaId
b forall a. Ord a => a -> a -> Bool
< MetaId
a)
          VerboseKey
"primShowMeta"               -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim Int
1 forall a b. (a -> b) -> a -> b
$ \ [LitMeta TopLevelModuleName
_ MetaId
a] -> VerboseKey -> Term
string (forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
a)

          VerboseKey
_                            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
        where
          fcc :: Maybe FastCompiledClauses
fcc = BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> a -> a
div (forall a. Ord a => a -> a -> a
max a
0 forall a b. (a -> b) -> a -> b
$ a
n forall a. Num a => a -> a -> a
+ a
m forall a. Num a => a -> a -> a
- a
j) (a
m 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 forall a. Ord a => a -> a -> Bool
> a
j     = forall a. Integral a => a -> a -> a
mod (a
n forall a. Num a => a -> a -> a
- a
j forall a. Num a => a -> a -> a
- a
1) (a
m forall a. Num a => a -> a -> a
+ a
1)
                         | Bool
otherwise = a
k forall a. Num a => a -> a -> a
+ a
n

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

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

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

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

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

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

-- | Case tree with bodies.

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

fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv CompiledClauses
cc =
  case CompiledClauses
cc of
    Fail{}            -> FastCompiledClauses
FFail
    Done [Arg VerboseKey]
xs Term
b         -> [Arg VerboseKey] -> Term -> FastCompiledClauses
FDone [Arg VerboseKey]
xs Term
b
    Case (Arg ArgInfo
_ Int
n) Branches{ etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Just (ConHead
c, WithArity CompiledClauses
cc), catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe CompiledClauses
ca } ->
      Int
-> [Arg QName]
-> FastCompiledClauses
-> Maybe FastCompiledClauses
-> FastCompiledClauses
FEta Int
n (ConHead -> [Arg QName]
conFields ConHead
c) (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv forall a b. (a -> b) -> a -> b
$ forall c. WithArity c -> c
content WithArity CompiledClauses
cc) (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv 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    = forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (Name -> NameId
nameId forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. WithArity c -> c
content) (Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
stripSuc Map QName (WithArity CompiledClauses)
con)
    , fsucBranch :: Maybe FastCompiledClauses
fsucBranch      = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. WithArity c -> c
content) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map QName (WithArity CompiledClauses)
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BuiltinEnv -> Maybe ConHead
bSuc BuiltinEnv
env
    , flitBranches :: Map Literal FastCompiledClauses
flitBranches    = 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    = (forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
==) Maybe Bool
fT
    , fcatchAllBranch :: Maybe FastCompiledClauses
fcatchAllBranch = 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 = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (ConHead -> QName
conName ConHead
c)
             | Bool
otherwise          = 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
_) = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> NameId
nameId forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
c) Map NameId c
cons

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

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

-- * Fast reduction

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

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

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

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

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

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

-- * Closures

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

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

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

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

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

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

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

-- * Pointers and thunks

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

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

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

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

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


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

readPointer :: STPointer s -> ST s (Thunk (Closure s))
readPointer :: forall s. STPointer s -> ST s (Thunk (Closure s))
readPointer = 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 = forall s a. STRef s a -> a -> ST s ()
writeSTRef STPointer s
ptr (forall a. a -> Thunk a
Thunk Closure s
cl)
    -- Note the strict match. To prevent leaking memory in case of unnecessary updates.

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

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

-- | Create a thunk that is not shared or updated.
pureThunk :: Closure s -> Pointer s
pureThunk :: forall s. Closure s -> Pointer s
pureThunk = 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 = 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) = 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) = forall s. [Pointer s] -> Env s
Env (Pointer s
p forall a. a -> [a] -> [a]
: [Pointer s]
xs)

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

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

-- * The Agda Abstract Machine

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

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

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

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

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

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

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

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

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

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

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

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

-- * Compilation and decoding

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

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

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

decodeEnv :: Env s -> ST s [Term]
decodeEnv :: forall s. Env s -> ST s [Term]
decodeEnv Env s
env = forall s a. ST s a -> ST s a
unsafeInterleaveST forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall s. Pointer s -> ST s Term
decodePointer (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_ = forall t a. Blocked' t a -> a
ignoreBlocking forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall s. Closure s -> ST s (Blocked Term)
decodeClosure

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

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

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

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

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

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

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

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

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

-- * Running the abstract machine

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

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

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

    -- Checking for built-in zero and suc
    BuiltinEnv{ bZero :: BuiltinEnv -> Maybe ConHead
bZero = Maybe ConHead
zero, bSuc :: BuiltinEnv -> Maybe ConHead
bSuc = Maybe ConHead
suc, bRefl :: BuiltinEnv -> Maybe ConHead
bRefl = Maybe ConHead
refl0 } = BuiltinEnv
bEnv
    conNameId :: ConHead -> NameId
conNameId = Name -> NameId
nameId forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName 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 -> forall a b. a -> b -> a
const Bool
False
               Just ConHead
z  -> (ConHead -> NameId
conNameId ConHead
z forall a. Eq a => a -> a -> 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 -> forall a b. a -> b -> a
const Bool
False
               Just ConHead
s  -> (ConHead -> NameId
conNameId ConHead
s forall a. Eq a => a -> a -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ ConHead
c -> if CompactDefn -> Int
cconArity (CompactDef -> CompactDefn
cdefDef forall a b. (a -> b) -> a -> b
$ QName -> CompactDef
constInfo forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) forall a. Eq a => a -> a -> Bool
== Int
0
                            then forall a. a -> Maybe a
Just ConHead
c else forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

        -- Case: non-empty spine. If the focused term has a non-empty spine, we shift the
        -- eliminations onto the spine.
        Def QName
f   Elims
es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims (QName -> Elims -> Term
Def QName
f   []) 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 []) 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 -> forall s.
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM Spine s
spine [ControlFrame s]
ctrl forall a b. (a -> b) -> a -> b
$
          case MetaId -> Maybe MetaInstantiation
getMetaInst MetaId
m of
            Maybe MetaInstantiation
Nothing ->
              forall s. AM s -> ST s (Blocked Term)
runAM (forall s. Closure s -> ControlStack s -> AM s
Eval (forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (forall a t. MetaId -> a -> Blocked' t a
blocked MetaId
m ()) Closure s
cl) [ControlFrame s]
ctrl)
            Just (InstV Instantiation
i) -> do
              Spine s
spine' <- forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
              let ([Arg VerboseKey]
zs, Env s
env, !Spine s
spine'') = forall s.
[Arg VerboseKey] -> Spine s -> ([Arg VerboseKey], Env s, Spine s)
buildEnv (Instantiation -> [Arg VerboseKey]
instTel Instantiation
i) (Spine s
spine' forall a. Semigroup a => a -> a -> a
<> Spine s
spine)
              forall s. AM s -> ST s (Blocked Term)
runAM (forall {s}. Term -> Env s -> Spine s -> ControlStack s -> AM s
evalClosure ([Arg VerboseKey] -> Term -> Term
lams [Arg VerboseKey]
zs (Instantiation -> Term
instBody Instantiation
i)) Env s
env Spine s
spine'' [ControlFrame s]
ctrl)
            Just Open{}                         -> forall a. HasCallStack => a
__IMPOSSIBLE__
            Just OpenInstance{}                 -> forall a. HasCallStack => a
__IMPOSSIBLE__
            Just BlockedConst{}                 -> forall a. HasCallStack => a
__IMPOSSIBLE__
            Just PostponedTypeCheckingProblem{} -> 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{}    -> forall s. AM s -> ST s (Blocked Term)
fallbackAM AM s
s
        Sort{}     -> forall s. AM s -> ST s (Blocked Term)
fallbackAM AM s
s
        Dummy{}    -> forall s. AM s -> ST s (Blocked Term)
fallbackAM AM s
s

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

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

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

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

        -- We might get these from fallbackAM
        Def QName
f   Elims
es -> Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims (QName -> Elims -> Term
Def QName
f   []) 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 []) 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 []) forall s. Env s
emptyEnv Env s
env Elims
es

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

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

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

    -- Case: NatSucK m

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

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

    -- Case: PrimOpK

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        -- This the spine at this point in the matching. A catch-all match doesn't change the spine.
        catchallSpine :: Spine s
catchallSpine = Spine s
spine0 forall a. Semigroup a => a -> a -> a
<> [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i Pointer s
p] forall a. Semigroup a => a -> a -> a
<> Spine s
spine1
          where p :: Pointer s
p = 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 forall c. FastCase c -> Maybe c
fcatchAllBranch FastCase FastCompiledClauses
bs of
          Maybe FastCompiledClauses
Nothing -> MatchStack s
stack
          Just FastCompiledClauses
cc -> forall s. FastCompiledClauses -> Spine s -> CatchAllFrame s
CatchAll FastCompiledClauses
cc Spine s
catchallSpine 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 = 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 = forall c. QName -> FastCase c -> Maybe c
lookupCon QName
q FastCase FastCompiledClauses
bs forall {a} {b}. Maybe a -> (a -> b) -> b -> b
`ifJust` \ FastCompiledClauses
cc ->
          forall s. AM s -> ST s (Blocked Term)
runAM (forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> AM s
Match QName
f FastCompiledClauses
cc (Spine s
spine0 forall a. Semigroup a => a -> a -> a
<> Spine s
spine forall a. Semigroup a => a -> a -> a
<> Spine s
spine1) MatchStack s
catchallStack [ControlFrame s]
ctrl)

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

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

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

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

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

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

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

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

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

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

    -- Normalise the spine and apply the closure to the result. The closure must be a value closure.
    normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
    normaliseArgsAM :: forall s.
Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM Closure s
cl []    ControlStack s
ctrl = forall s. AM s -> ST s (Blocked Term)
runAM (forall s. Closure s -> ControlStack s -> AM s
Eval Closure s
cl ControlStack s
ctrl)  -- nothing to do
    normaliseArgsAM Closure s
cl [Elim' (Pointer s)]
spine ControlStack s
ctrl =
      case forall z. Zipper z => Carrier z -> Maybe (Element z, z)
firstHole [Elim' (Pointer 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       -> forall s. AM s -> ST s (Blocked Term)
runAM (forall s. Closure s -> ControlStack s -> AM s
Eval (forall s. Closure s -> Spine s -> Closure s
clApply_ Closure s
cl [Elim' (Pointer s)]
spine) ControlStack s
ctrl)
        Just (Element (SpineContext s)
p, SpineContext s
cxt) -> forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Element (SpineContext s)
p [] (forall s. ControlFrame s
NormaliseK forall a. a -> [a] -> [a]
: forall s. Closure s -> SpineContext s -> ControlFrame s
ArgK Closure s
cl SpineContext s
cxt forall a. a -> [a] -> [a]
: ControlStack s
ctrl)

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

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

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

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

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

    -- Only unfold delayed (corecursive) definitions if the result is being cased on.
    unfoldDelayed :: ControlStack s -> Bool
    unfoldDelayed :: forall s. ControlStack s -> Bool
unfoldDelayed []                     = Bool
False
    unfoldDelayed (CaseK{}       : [ControlFrame s]
_)    = Bool
True
    unfoldDelayed (PrimOpK{}     : [ControlFrame s]
_)    = Bool
False
    unfoldDelayed (NatSucK{}     : [ControlFrame s]
_)    = Bool
False
    unfoldDelayed (NormaliseK{}  : [ControlFrame s]
_)    = Bool
False
    unfoldDelayed (ArgK{}        : [ControlFrame s]
_)    = Bool
False
    unfoldDelayed (UpdateThunk{} : [ControlFrame s]
ctrl) = forall s. ControlStack s -> Bool
unfoldDelayed [ControlFrame s]
ctrl
    unfoldDelayed (ApplyK{}      : [ControlFrame s]
ctrl) = forall s. ControlStack s -> Bool
unfoldDelayed [ControlFrame s]
ctrl
    unfoldDelayed (ForceK{}      : [ControlFrame s]
ctrl) = forall s. ControlStack s -> Bool
unfoldDelayed [ControlFrame s]
ctrl
    unfoldDelayed (EraseK{}      : [ControlFrame s]
ctrl) = forall s. ControlStack s -> Bool
unfoldDelayed [ControlFrame s]
ctrl

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

    -- On a mismatch we find the next 'CatchAll' on the control stack and
    -- continue matching from there. If there isn't one we get an incomplete
    -- matching error (or get stuck if the function is marked partial).
    failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
    failedMatch :: forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f (CatchAll FastCompiledClauses
cc Spine s
spine : [CatchAllFrame s]
stack :> Closure s
cl) ControlStack s
ctrl = forall s. AM s -> ST s (Blocked Term)
runAM (forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> AM s
Match QName
f FastCompiledClauses
cc Spine s
spine ([CatchAllFrame s]
stack forall s. [CatchAllFrame s] -> Closure s -> MatchStack s
:> Closure s
cl) ControlStack s
ctrl)
    failedMatch QName
f ([] :> Closure s
cl) ControlStack s
ctrl
        -- Bad work-around for #3870: don't fail hard during instance search.
      | Bool
speculative          = forall s. AM s -> ST s (Blocked Term)
rewriteAM (forall s. Closure s -> ControlStack s -> AM s
Eval (forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) Closure s
cl) ControlStack s
ctrl)
      | QName
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
partialDefs = forall s. AM s -> ST s (Blocked Term)
rewriteAM (forall s. Closure s -> ControlStack s -> AM s
Eval (forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
f) ()) Closure s
cl) ControlStack s
ctrl)
      | Bool
hasRewriting         = forall s. AM s -> ST s (Blocked Term)
rewriteAM (forall s. Closure s -> ControlStack s -> AM s
Eval (forall {s}. Blocked_ -> Closure s -> Closure s
mkValue (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked ()) Closure s
cl) ControlStack s
ctrl)  -- See #5396
      | Bool
otherwise            = forall a. ReduceM a -> a
runReduce forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m a -> m a
traceSLn VerboseKey
"impossible" Int
10 (VerboseKey
"Incomplete pattern matching when applying " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> VerboseKey
prettyShow QName
f)
                   forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Some helper functions to build machine states and closures.
    evalClosure :: Term -> Env s -> Spine s -> ControlStack s -> AM s
evalClosure Term
t Env s
env Spine s
spine = forall s. Closure s -> ControlStack s -> AM s
Eval (forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled Term
t Env s
env Spine s
spine)
    evalValue :: Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue Blocked_
b Term
t Env s
env Spine s
spine = forall s. Closure s -> ControlStack s -> AM s
Eval (forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure (Blocked_ -> IsValue
Value Blocked_
b) Term
t Env s
env Spine s
spine)
    evalTrueValue :: Term -> Env s -> Spine s -> ControlStack s -> AM s
evalTrueValue           = forall {s}.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue forall a b. (a -> b) -> a -> b
$ 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   = forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure (Blocked_ -> IsValue
Value forall a b. (a -> b) -> a -> b
$ 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               = forall s. IsValue -> Closure s -> Closure s
setIsValue (Blocked_ -> IsValue
Value Blocked_
b)

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

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

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

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

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

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

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

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

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

instance Pretty (CatchAllFrame s) where
  pretty :: CatchAllFrame s -> Doc
pretty CatchAll{} = Doc
"CatchAll"

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

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