{-# LANGUAGE PatternGuards #-}

{-|

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

Some other tricks that improves performance:

- Memoise getConstInfo.

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

- Optimised case trees.

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

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

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

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

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

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

import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Semigroup ((<>))
import Data.Text (Text)
import qualified Data.Text as T

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

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

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

import Agda.Interaction.Options

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

import Agda.Utils.Impossible

import Debug.Trace

-- * Compact definitions

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Case tree with bodies.

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

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

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


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

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

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

-- * Fast reduction

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

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

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

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

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

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

-- * Closures

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

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

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

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

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

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

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

-- * Pointers and thunks

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

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

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

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

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


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

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

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

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

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

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

-- * Environments

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

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

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

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

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

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

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

-- * The Agda Abstract Machine

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

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

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

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

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

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

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

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

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

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

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

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

-- * Compilation and decoding

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- * Running the abstract machine

-- | Evaluating a term in the abstract machine. It gets the type checking state and environment in
--   the 'ReduceEnv' argument, some precomputed built-in mappings in 'BuiltinEnv', the memoised
--   'getConstInfo' function, a couple of flags (allow non-terminating function unfolding, and
--   whether rewriting is enabled), and a term to reduce. The result is the weak-head normal form of
--   the term with an attached blocking tag.
reduceTm :: ReduceEnv -> BuiltinEnv -> (QName -> CompactDef) -> Normalisation -> ReductionFlags -> Term -> Blocked Term
reduceTm :: ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> Normalisation
-> ReductionFlags
-> Term
-> Blocked Term
reduceTm ReduceEnv
rEnv BuiltinEnv
bEnv !QName -> CompactDef
constInfo Normalisation
normalisation ReductionFlags{Bool
hasRewriting :: Bool
allowUnconfirmed :: Bool
allowNonTerminating :: Bool
hasRewriting :: ReductionFlags -> Bool
allowUnconfirmed :: ReductionFlags -> Bool
allowNonTerminating :: ReductionFlags -> Bool
..} =
    Term -> Blocked Term
compileAndRun (Term -> Blocked Term) -> (Term -> Term) -> Term -> Blocked Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Term -> Term
forall a. Doc -> a -> a
traceDoc Doc
"-- fast reduce --"
  where
    -- Helpers to get information from the ReduceEnv.
    metaStore :: IntMap MetaVariable
metaStore      = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Lens' (IntMap MetaVariable) TCState -> IntMap MetaVariable
forall o i. o -> Lens' i o -> i
^. Lens' (IntMap MetaVariable) TCState
stMetaStore
    -- Are we currently instance searching. In that case we don't fail hard on missing clauses. This
    -- is a (very unsatisfactory) work-around for #3870.
    speculative :: Bool
speculative    = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Lens' Bool TCState -> Bool
forall o i. o -> Lens' i o -> i
^. Lens' Bool TCState
stConsideringInstance
    getMeta :: MetaId -> MetaInstantiation
getMeta MetaId
m      = MetaInstantiation
-> (MetaVariable -> MetaInstantiation)
-> Maybe MetaVariable
-> MetaInstantiation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe MetaInstantiation
forall a. HasCallStack => a
__IMPOSSIBLE__ MetaVariable -> MetaInstantiation
mvInstantiation (Int -> IntMap MetaVariable -> Maybe MetaVariable
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (MetaId -> Int
metaId MetaId
m) IntMap MetaVariable
metaStore)
    partialDefs :: Set QName
partialDefs    = ReduceM (Set QName) -> Set QName
forall a. ReduceM a -> a
runReduce ReduceM (Set QName)
forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
    rewriteRules :: QName -> RewriteRules
rewriteRules QName
f = CompactDef -> RewriteRules
cdefRewriteRules (QName -> CompactDef
constInfo QName
f)
    callByNeed :: Bool
callByNeed     = TCEnv -> Bool
envCallByNeed (ReduceEnv -> TCEnv
redEnv ReduceEnv
rEnv) Bool -> Bool -> Bool
&& Bool -> Bool
not (PragmaOptions -> Bool
optCallByName (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall a b. (a -> b) -> a -> b
$ ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Lens' PragmaOptions TCState -> PragmaOptions
forall o i. o -> Lens' i o -> i
^. Lens' PragmaOptions TCState
stPragmaOptions)
    iview :: Term -> IntervalView
iview          = ReduceM (Term -> IntervalView) -> Term -> IntervalView
forall a. ReduceM a -> a
runReduce ReduceM (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    -- Case: NatSucK m

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

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

    -- Case: PrimOpK

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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