{-# LANGUAGE PatternGuards #-}

{-|

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

Some other tricks that improves performance:

- Memoise getConstInfo.

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

- Optimised case trees.

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

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

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

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

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

import Prelude hiding ((!!))

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

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

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

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

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

import Agda.Interaction.Options

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

import Agda.Utils.Impossible

import Debug.Trace

-- * Compact definitions

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Case tree with bodies.

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

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

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


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

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

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

-- * Fast reduction

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

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

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

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

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

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

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

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

-- * Closures

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

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

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

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

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

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

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

-- * Pointers and thunks

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

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

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

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

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


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

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

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

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

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

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

-- * Environments

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

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

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

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

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

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

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

-- * The Agda Abstract Machine

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

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

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

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

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

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

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

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

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

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

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

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

-- * Compilation and decoding

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

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

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

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

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

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

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

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

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

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

-- | Trim unused entries from an environment. Currently only trims closed terms for performance
--   reasons.
trimEnvironment :: FreeVariables -> Env s -> Env s
trimEnvironment :: forall s. FreeVariables -> Env s -> Env s
trimEnvironment FreeVariables
UnknownFVs Env s
env = Env s
env
trimEnvironment (KnownFVs IntSet
fvs) Env s
env
  | IntSet -> Bool
IntSet.null IntSet
fvs = Env s
forall s. Env s
emptyEnv
    -- Environment trimming is too expensive (costs 50% on some benchmarks), and while it does make
    -- some cases run in constant instead of linear space you need quite contrived examples to
    -- notice the effect.
  | Bool
otherwise       = Env s
env -- Env $ trim 0 $ envToList env
  where
    -- Important: strict enough that the trimming actually happens
    trim :: Int -> [Pointer 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 -> Term -> Blocked Term
reduceTm :: ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> Normalisation
-> Term
-> Blocked Term
reduceTm ReduceEnv
rEnv BuiltinEnv
bEnv !QName -> CompactDef
constInfo Normalisation
normalisation =
    Term -> Blocked Term
compileAndRun (Term -> Blocked Term) -> (Term -> Term) -> Term -> Blocked Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Term -> Term
forall a. Doc -> a -> a
traceDoc Doc
"-- fast reduce --"
  where
    -- Helpers to get information from the ReduceEnv.
    localMetas :: Map MetaId MetaVariable
localMetas     = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Lens' TCState (Map MetaId MetaVariable)
-> Map MetaId MetaVariable
forall o i. o -> Lens' o i -> i
^. (Map MetaId MetaVariable -> f (Map MetaId MetaVariable))
-> TCState -> f TCState
Lens' TCState (Map MetaId MetaVariable)
stSolvedMetaStore
    remoteMetas :: HashMap MetaId RemoteMetaVariable
remoteMetas    = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Lens' TCState (HashMap MetaId RemoteMetaVariable)
-> HashMap MetaId RemoteMetaVariable
forall o i. o -> Lens' o i -> i
^. (HashMap MetaId RemoteMetaVariable
 -> f (HashMap MetaId RemoteMetaVariable))
-> TCState -> f TCState
Lens' TCState (HashMap MetaId RemoteMetaVariable)
stImportedMetaStore
    -- Are we currently instance searching. In that case we don't fail hard on missing clauses. This
    -- is a (very unsatisfactory) work-around for #3870.
    speculative :: Bool
speculative    = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Lens' TCState Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stConsideringInstance
    getMetaInst :: MetaId -> Maybe MetaInstantiation
getMetaInst MetaId
m  = case MetaId -> Map MetaId MetaVariable -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m Map MetaId MetaVariable
localMetas of
                       Just MetaVariable
mv -> MetaInstantiation -> Maybe MetaInstantiation
forall a. a -> Maybe a
Just (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
                       Maybe MetaVariable
Nothing -> Instantiation -> MetaInstantiation
InstV (Instantiation -> MetaInstantiation)
-> (RemoteMetaVariable -> Instantiation)
-> RemoteMetaVariable
-> MetaInstantiation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemoteMetaVariable -> Instantiation
rmvInstantiation (RemoteMetaVariable -> MetaInstantiation)
-> Maybe RemoteMetaVariable -> Maybe MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                    MetaId
-> HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup MetaId
m HashMap MetaId RemoteMetaVariable
remoteMetas
    partialDefs :: Set QName
partialDefs    = ReduceM (Set QName) -> Set QName
forall a. ReduceM a -> a
runReduce ReduceM (Set QName)
forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
    rewriteRules :: QName -> RewriteRules
rewriteRules QName
f = CompactDef -> RewriteRules
cdefRewriteRules (QName -> CompactDef
constInfo QName
f)
    callByNeed :: Bool
callByNeed     = TCEnv -> Bool
envCallByNeed (ReduceEnv -> TCEnv
redEnv ReduceEnv
rEnv) Bool -> Bool -> Bool
&& Bool -> Bool
not (PragmaOptions -> Bool
optCallByName (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall a b. (a -> b) -> a -> b
$ ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Lens' TCState PragmaOptions -> PragmaOptions
forall o i. o -> Lens' o i -> i
^. (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions)
    iview :: Term -> IntervalView
iview          = ReduceM (Term -> IntervalView) -> Term -> IntervalView
forall a. ReduceM a -> a
runReduce ReduceM (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    -- Case: NatSucK m

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

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

    -- Case: PrimOpK

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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