{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Reduce.Fast
( fastReduce, fastNormalise ) where
import Control.Applicative hiding (empty)
import Control.Monad.ST
import Control.Monad.ST.Unsafe (unsafeSTToIO, unsafeInterleaveST)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Traversable (traverse)
import Data.Semigroup ((<>))
import System.IO.Unsafe (unsafePerformIO)
import Data.IORef
import Data.STRef
import Data.Char
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Irrelevance (isPropM)
import Agda.TypeChecking.Monad hiding (Closure(..))
import Agda.TypeChecking.Reduce as R
import Agda.TypeChecking.Rewriting (rewrite)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Builtin hiding (constructorForm)
import Agda.Interaction.Options
import Agda.Utils.Float
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (empty)
import Agda.Utils.Functor
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Zipper
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Impossible
import Debug.Trace
data CompactDef =
CompactDef { CompactDef -> Bool
cdefDelayed :: Bool
, CompactDef -> Bool
cdefNonterminating :: Bool
, CompactDef -> Bool
cdefUnconfirmed :: Bool
, CompactDef -> CompactDefn
cdefDef :: CompactDefn
, CompactDef -> RewriteRules
cdefRewriteRules :: RewriteRules
}
data CompactDefn
= CFun { CompactDefn -> FastCompiledClauses
cfunCompiled :: FastCompiledClauses, CompactDefn -> Maybe QName
cfunProjection :: Maybe QName }
| CCon { CompactDefn -> ConHead
cconSrcCon :: ConHead, CompactDefn -> Int
cconArity :: Int }
| CForce
| CErase
| CTyCon
| CAxiom
| CPrimOp Int ([Literal] -> Term) (Maybe FastCompiledClauses)
| COther
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 }
compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
compactDef bEnv :: BuiltinEnv
bEnv def :: Definition
def rewr :: RewriteRules
rewr = do
let isPrp :: Bool
isPrp = case Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Definition -> Type
defType Definition
def) of
Prop{} -> Bool
True
_ -> Bool
False
let irr :: Bool
irr = Bool
isPrp Bool -> Bool -> Bool
|| ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant (Definition -> ArgInfo
defArgInfo Definition
def)
CompactDefn
cdefn <-
case Definition -> Defn
theDef Definition
def of
_ | Bool
irr -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinEnv -> Maybe QName
bPrimForce BuiltinEnv
bEnv -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CForce
_ | 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 tel :: Tele (Dom Type)
tel _ | Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 5 -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CErase
| Bool
otherwise -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
_ | Definition -> Blocked_
defBlocked Definition
def Blocked_ -> Blocked_ -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocked_
notBlocked_ -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
Constructor{conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c, conArity :: Defn -> Int
conArity = Int
n} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CCon :: ConHead -> Int -> CompactDefn
CCon{cconSrcCon :: ConHead
cconSrcCon = ConHead
c, cconArity :: Int
cconArity = Int
n}
Function{funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just cc :: CompiledClauses
cc, funClauses :: Defn -> [Clause]
funClauses = _:_, funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
proj} ->
CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CFun :: FastCompiledClauses -> Maybe QName -> CompactDefn
CFun{ cfunCompiled :: FastCompiledClauses
cfunCompiled = BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv CompiledClauses
cc
, cfunProjection :: Maybe QName
cfunProjection = Projection -> QName
projOrig (Projection -> QName) -> Maybe Projection -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Projection
proj }
Function{funClauses :: Defn -> [Clause]
funClauses = []} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
Function{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
Datatype{dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
Nothing} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CTyCon
Record{recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
Nothing} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CTyCon
Datatype{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
Record{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
Axiom{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
DataOrRecSig{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
AbstractDefn{} -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
CAxiom
GeneralizableVar{} -> ReduceM CompactDefn
forall a. HasCallStack => a
__IMPOSSIBLE__
Primitive{ primName :: Defn -> String
primName = String
name, primCompiled :: Defn -> Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
cc } ->
case String
name of
"primNatPlus" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(+)
"primNatMinus" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Literal] -> Term
natOp (\ x :: Integer
x y :: Integer
y -> Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max 0 (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y))
"primNatTimes" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(*)
"primNatDivSucAux" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primNatModSucAux" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primNatLess" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(<)
"primNatEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(==)
"primWord64ToNat" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitWord64 _ a :: Word64
a] -> Integer -> Term
nat (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
a)
"primWord64FromNat" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitNat _ a :: Integer
a] -> Word64 -> Term
word (Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
a)
"primNatToFloat" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitNat _ a :: Integer
a] -> Double -> Term
float (Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
a)
"primFloatPlus" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(+)
"primFloatMinus" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Double -> Double -> Double) -> [Literal] -> Term
floatOp (-)
"primFloatTimes" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(*)
"primFloatNegate" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primFloatDiv" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(/)
"primFloatEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
floatEq
"primFloatLess" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
floatLt
"primFloatNumericalEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(==)
"primFloatNumericalLess" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(<)
"primFloatSqrt" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primExp" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primLog" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primSin" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primCos" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primTan" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primASin" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primACos" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primATan" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primATan2" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
"primShowFloat" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitFloat _ a :: Double
a] -> String -> Term
string (Double -> String
forall a. Show a => a -> String
show Double
a)
"primCharEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 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
(==)
"primIsLower" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isLower
"primIsDigit" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isDigit
"primIsAlpha" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isAlpha
"primIsSpace" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isSpace
"primIsAscii" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isAscii
"primIsLatin1" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isLatin1
"primIsPrint" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isPrint
"primIsHexDigit" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> [Literal] -> Term
charPred Char -> Bool
isHexDigit
"primToUpper" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Literal] -> Term
charFun Char -> Char
toUpper
"primToLower" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Literal] -> Term
charFun Char -> Char
toLower
"primCharToNat" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitChar _ a :: 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))
"primNatToChar" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitNat _ a :: Integer
a] -> Char -> Term
char (Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` 0x110000)
"primShowChar" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [a :: Literal
a] -> String -> Term
string (Literal -> String
forall a. Pretty a => a -> String
prettyShow Literal
a)
"primStringAppend" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitString _ a :: String
a, LitString _ b :: String
b] -> String -> Term
string (String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a)
"primStringEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitString _ a :: String
a, LitString _ b :: String
b] -> Bool -> Term
bool (String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
a)
"primShowString" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [a :: Literal
a] -> String -> Term
string (Literal -> String
forall a. Pretty a => a -> String
prettyShow Literal
a)
"primQNameEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitQName _ a :: QName
a, LitQName _ b :: QName
b] -> Bool -> Term
bool (QName
b QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
a)
"primQNameLess" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitQName _ a :: QName
a, LitQName _ b :: QName
b] -> Bool -> Term
bool (QName
b QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
< QName
a)
"primShowQName" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitQName _ a :: QName
a] -> String -> Term
string (QName -> String
forall a. Show a => a -> String
show QName
a)
"primMetaEquality" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitMeta _ _ a :: MetaId
a, LitMeta _ _ b :: MetaId
b] -> Bool -> Term
bool (MetaId
b MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
a)
"primMetaLess" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 2 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitMeta _ _ a :: MetaId
a, LitMeta _ _ b :: MetaId
b] -> Bool -> Term
bool (MetaId
b MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
< MetaId
a)
"primShowMeta" -> Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim 1 (([Literal] -> Term) -> ReduceM CompactDefn)
-> ([Literal] -> Term) -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ \ [LitMeta _ _ a :: MetaId
a] -> String -> Term
string (Doc -> String
forall a. Show a => a -> String
show (MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
a))
_ -> CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompactDefn
COther
where
fcc :: Maybe FastCompiledClauses
fcc = BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
bEnv (CompiledClauses -> FastCompiledClauses)
-> Maybe CompiledClauses -> Maybe FastCompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CompiledClauses
cc
mkPrim :: Int -> ([Literal] -> Term) -> ReduceM CompactDefn
mkPrim n :: Int
n op :: [Literal] -> Term
op = CompactDefn -> ReduceM CompactDefn
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CompactDefn -> ReduceM CompactDefn)
-> CompactDefn -> ReduceM CompactDefn
forall a b. (a -> b) -> a -> b
$ Int
-> ([Literal] -> Term) -> Maybe FastCompiledClauses -> CompactDefn
CPrimOp Int
n [Literal] -> Term
op Maybe FastCompiledClauses
fcc
divAux :: a -> a -> a -> a -> a
divAux k :: a
k m :: a
m n :: a
n j :: 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 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
+ 1)
modAux :: a -> a -> a -> a -> a
modAux k :: a
k m :: a
m n :: a
n j :: 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
- 1) (a
m a -> a -> a
forall a. Num a => a -> a -> a
+ 1)
| Bool
otherwise = a
k a -> a -> a
forall a. Num a => a -> a -> a
+ a
n
~(Just true :: Term
true) = BuiltinEnv -> Maybe ConHead
bTrue BuiltinEnv
bEnv Maybe ConHead -> (ConHead -> Term) -> Maybe Term
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ c :: ConHead
c -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem []
~(Just false :: Term
false) = BuiltinEnv -> Maybe ConHead
bFalse BuiltinEnv
bEnv Maybe ConHead -> (ConHead -> Term) -> Maybe Term
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ c :: ConHead
c -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem []
bool :: Bool -> Term
bool a :: Bool
a = if Bool
a then Term
true else Term
false
nat :: Integer -> Term
nat a :: Integer
a = Literal -> Term
Lit (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange (Integer -> Term) -> Integer -> Term
forall a b. (a -> b) -> a -> b
$! Integer
a
word :: Word64 -> Term
word a :: Word64
a = Literal -> Term
Lit (Literal -> Term) -> (Word64 -> Literal) -> Word64 -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Word64 -> Literal
LitWord64 Range
forall a. Range' a
noRange (Word64 -> Term) -> Word64 -> Term
forall a b. (a -> b) -> a -> b
$! Word64
a
float :: Double -> Term
float a :: Double
a = Literal -> Term
Lit (Literal -> Term) -> (Double -> Literal) -> Double -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Double -> Literal
LitFloat Range
forall a. Range' a
noRange (Double -> Term) -> Double -> Term
forall a b. (a -> b) -> a -> b
$! Double
a
string :: String -> Term
string a :: String
a = Literal -> Term
Lit (Literal -> Term) -> (String -> Literal) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> String -> Literal
LitString Range
forall a. Range' a
noRange (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$! String
a
char :: Char -> Term
char a :: Char
a = Literal -> Term
Lit (Literal -> Term) -> (Char -> Literal) -> Char -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Char -> Literal
LitChar Range
forall a. Range' a
noRange (Char -> Term) -> Char -> Term
forall a b. (a -> b) -> a -> b
$! Char
a
natOp :: (Integer -> Integer -> Integer) -> [Literal] -> Term
natOp f :: Integer -> Integer -> Integer
f [LitNat _ a :: Integer
a, LitNat _ b :: Integer
b] = Integer -> Term
nat (Integer -> Integer -> Integer
f Integer
b Integer
a)
natOp _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
natOp4 :: (Integer -> Integer -> Integer -> Integer -> Integer)
-> [Literal] -> Term
natOp4 f :: Integer -> Integer -> Integer -> Integer -> Integer
f [LitNat _ a :: Integer
a, LitNat _ b :: Integer
b, LitNat _ c :: Integer
c, LitNat _ d :: Integer
d] = Integer -> Term
nat (Integer -> Integer -> Integer -> Integer -> Integer
f Integer
d Integer
c Integer
b Integer
a)
natOp4 _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
natRel :: (Integer -> Integer -> Bool) -> [Literal] -> Term
natRel f :: Integer -> Integer -> Bool
f [LitNat _ a :: Integer
a, LitNat _ b :: Integer
b] = Bool -> Term
bool (Integer -> Integer -> Bool
f Integer
b Integer
a)
natRel _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
floatFun :: (Double -> Double) -> [Literal] -> Term
floatFun f :: Double -> Double
f [LitFloat _ a :: Double
a] = Double -> Term
float (Double -> Double
f Double
a)
floatFun _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
floatOp :: (Double -> Double -> Double) -> [Literal] -> Term
floatOp f :: Double -> Double -> Double
f [LitFloat _ a :: Double
a, LitFloat _ b :: Double
b] = Double -> Term
float (Double -> Double -> Double
f Double
b Double
a)
floatOp _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
floatRel :: (Double -> Double -> Bool) -> [Literal] -> Term
floatRel f :: Double -> Double -> Bool
f [LitFloat _ a :: Double
a, LitFloat _ b :: Double
b] = Bool -> Term
bool (Double -> Double -> Bool
f Double
b Double
a)
floatRel _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
charFun :: (Char -> Char) -> [Literal] -> Term
charFun f :: Char -> Char
f [LitChar _ a :: Char
a] = Char -> Term
char (Char -> Char
f Char
a)
charFun _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
charPred :: (Char -> Bool) -> [Literal] -> Term
charPred f :: Char -> Bool
f [LitChar _ a :: Char
a] = Bool -> Term
bool (Char -> Bool
f Char
a)
charPred _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
charRel :: (Char -> Char -> Bool) -> [Literal] -> Term
charRel f :: Char -> Char -> Bool
f [LitChar _ a :: Char
a, LitChar _ b :: Char
b] = Bool -> Term
bool (Char -> Char -> Bool
f Char
b Char
a)
charRel _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
CompactDef -> ReduceM CompactDef
forall (m :: * -> *) a. Monad m => a -> m a
return (CompactDef -> ReduceM CompactDef)
-> CompactDef -> ReduceM CompactDef
forall a b. (a -> b) -> a -> b
$
CompactDef :: Bool -> Bool -> Bool -> CompactDefn -> RewriteRules -> CompactDef
CompactDef { cdefDelayed :: Bool
cdefDelayed = Definition -> Delayed
defDelayed Definition
def Delayed -> Delayed -> Bool
forall a. Eq a => a -> a -> Bool
== Delayed
Delayed
, cdefNonterminating :: Bool
cdefNonterminating = Definition -> Bool
defNonterminating Definition
def
, cdefUnconfirmed :: Bool
cdefUnconfirmed = Definition -> Bool
defTerminationUnconfirmed Definition
def
, cdefDef :: CompactDefn
cdefDef = CompactDefn
cdefn
, cdefRewriteRules :: RewriteRules
cdefRewriteRules = RewriteRules
rewr
}
data FastCase c = FBranches
{ FastCase c -> Bool
fprojPatterns :: Bool
, FastCase c -> Map NameId c
fconBranches :: Map NameId c
, FastCase c -> Maybe c
fsucBranch :: Maybe c
, FastCase c -> Map Literal c
flitBranches :: Map Literal c
, FastCase c -> Maybe c
fcatchAllBranch :: Maybe c
, FastCase c -> Bool
ffallThrough :: Bool
}
data FastCompiledClauses
= FCase Int (FastCase FastCompiledClauses)
| FEta Int [Arg QName] FastCompiledClauses (Maybe FastCompiledClauses)
| FDone [Arg ArgName] Term
| FFail
fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses bEnv :: BuiltinEnv
bEnv cc :: CompiledClauses
cc =
case CompiledClauses
cc of
Fail -> FastCompiledClauses
FFail
Done xs :: [Arg String]
xs b :: Term
b -> [Arg String] -> Term -> FastCompiledClauses
FDone [Arg String]
xs Term
b
Case (Arg _ n :: Int
n) Branches{ etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Just (c :: ConHead
c, cc :: 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 _ n :: Int
n) bs :: 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 env :: BuiltinEnv
env (Branches proj :: Bool
proj con :: Map QName (WithArity CompiledClauses)
con _ lit :: Map Literal CompiledClauses
lit wild :: Maybe CompiledClauses
wild fT :: Maybe Bool
fT _) =
FBranches :: forall c.
Bool
-> Map NameId c
-> Maybe c
-> Map Literal c
-> Maybe c
-> Bool
-> FastCase c
FBranches
{ fprojPatterns :: Bool
fprojPatterns = Bool
proj
, fconBranches :: Map NameId FastCompiledClauses
fconBranches = (QName -> NameId)
-> Map QName FastCompiledClauses -> Map NameId FastCompiledClauses
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (Name -> NameId
nameId (Name -> NameId) -> (QName -> Name) -> QName -> NameId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName) (Map QName FastCompiledClauses -> Map NameId FastCompiledClauses)
-> Map QName FastCompiledClauses -> Map NameId FastCompiledClauses
forall a b. (a -> b) -> a -> b
$ (WithArity CompiledClauses -> FastCompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> Map QName FastCompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env (CompiledClauses -> FastCompiledClauses)
-> (WithArity CompiledClauses -> CompiledClauses)
-> WithArity CompiledClauses
-> FastCompiledClauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArity CompiledClauses -> CompiledClauses
forall c. WithArity c -> c
content) (Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
stripSuc Map QName (WithArity CompiledClauses)
con)
, fsucBranch :: Maybe FastCompiledClauses
fsucBranch = (WithArity CompiledClauses -> FastCompiledClauses)
-> Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env (CompiledClauses -> FastCompiledClauses)
-> (WithArity CompiledClauses -> CompiledClauses)
-> WithArity CompiledClauses
-> FastCompiledClauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArity CompiledClauses -> CompiledClauses
forall c. WithArity c -> c
content) (Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses)
-> Maybe (WithArity CompiledClauses) -> Maybe FastCompiledClauses
forall a b. (a -> b) -> a -> b
$ (QName
-> Map QName (WithArity CompiledClauses)
-> Maybe (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
-> QName
-> Maybe (WithArity CompiledClauses)
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName
-> Map QName (WithArity CompiledClauses)
-> Maybe (WithArity CompiledClauses)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map QName (WithArity CompiledClauses)
con (QName -> Maybe (WithArity CompiledClauses))
-> (ConHead -> QName)
-> ConHead
-> Maybe (WithArity CompiledClauses)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName (ConHead -> Maybe (WithArity CompiledClauses))
-> Maybe ConHead -> Maybe (WithArity CompiledClauses)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BuiltinEnv -> Maybe ConHead
bSuc BuiltinEnv
env
, flitBranches :: Map Literal FastCompiledClauses
flitBranches = (CompiledClauses -> FastCompiledClauses)
-> Map Literal CompiledClauses -> Map Literal FastCompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env) Map Literal CompiledClauses
lit
, ffallThrough :: Bool
ffallThrough = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False Maybe Bool
fT
, fcatchAllBranch :: Maybe FastCompiledClauses
fcatchAllBranch = (CompiledClauses -> FastCompiledClauses)
-> Maybe CompiledClauses -> Maybe FastCompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses BuiltinEnv
env) Maybe CompiledClauses
wild }
where
stripSuc :: Map QName (WithArity CompiledClauses)
-> Map QName (WithArity CompiledClauses)
stripSuc | Just c :: 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 :: QName -> FastCase c -> Maybe c
lookupCon c :: QName
c (FBranches _ cons :: Map NameId c
cons _ _ _ _) = 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
{-# NOINLINE memoQName #-}
memoQName :: (QName -> a) -> (QName -> a)
memoQName :: (QName -> a) -> QName -> a
memoQName f :: QName -> a
f = IO (QName -> a) -> QName -> a
forall a. IO a -> a
unsafePerformIO (IO (QName -> a) -> QName -> a) -> IO (QName -> a) -> QName -> a
forall a b. (a -> b) -> a -> b
$ do
IORef (Map NameId a)
tbl <- Map NameId a -> IO (IORef (Map NameId a))
forall a. a -> IO (IORef a)
newIORef Map NameId a
forall k a. Map k a
Map.empty
(QName -> a) -> IO (QName -> a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> (QName -> IO a) -> QName -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Map NameId a) -> QName -> IO a
f' IORef (Map NameId a)
tbl)
where
f' :: IORef (Map NameId a) -> QName -> IO a
f' tbl :: IORef (Map NameId a)
tbl x :: QName
x = do
let i :: NameId
i = Name -> NameId
nameId (QName -> Name
qnameName QName
x)
Map NameId a
m <- IORef (Map NameId a) -> IO (Map NameId a)
forall a. IORef a -> IO a
readIORef IORef (Map NameId a)
tbl
case NameId -> Map NameId a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup NameId
i Map NameId a
m of
Just y :: a
y -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y
Nothing -> do
let y :: a
y = QName -> a
f QName
x
IORef (Map NameId a) -> Map NameId a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Map NameId a)
tbl (NameId -> a -> Map NameId a -> Map NameId a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NameId
i a
y Map NameId a
m)
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y
data Normalisation = WHNF | NF
deriving (Normalisation -> Normalisation -> Bool
(Normalisation -> Normalisation -> Bool)
-> (Normalisation -> Normalisation -> Bool) -> Eq Normalisation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Normalisation -> Normalisation -> Bool
$c/= :: Normalisation -> Normalisation -> Bool
== :: Normalisation -> Normalisation -> Bool
$c== :: Normalisation -> Normalisation -> Bool
Eq)
data ReductionFlags = ReductionFlags
{ ReductionFlags -> Bool
allowNonTerminating :: Bool
, ReductionFlags -> Bool
allowUnconfirmed :: Bool
, ReductionFlags -> Bool
hasRewriting :: Bool }
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 v :: Term
v = Blocked Term -> Term
forall t. Blocked t -> t
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' norm :: Normalisation
norm v :: Term
v = do
let name :: Term -> ConHead
name (Con c :: ConHead
c _ _) = ConHead
c
name _ = ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__
Maybe ConHead
zero <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ConHead
name (Maybe Term -> Maybe ConHead)
-> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinZero
Maybe ConHead
suc <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ConHead
name (Maybe Term -> Maybe ConHead)
-> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSuc
Maybe ConHead
true <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ConHead
name (Maybe Term -> Maybe ConHead)
-> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinTrue
Maybe ConHead
false <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ConHead
name (Maybe Term -> Maybe ConHead)
-> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinFalse
Maybe ConHead
refl <- (Term -> ConHead) -> Maybe Term -> Maybe ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ConHead
name (Maybe Term -> Maybe ConHead)
-> ReduceM (Maybe Term) -> ReduceM (Maybe ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinRefl
Maybe QName
force <- (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PrimFun -> QName
primFunName (Maybe PrimFun -> Maybe QName)
-> ReduceM (Maybe PrimFun) -> ReduceM (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe PrimFun)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' "primForce"
Maybe QName
erase <- (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PrimFun -> QName
primFunName (Maybe PrimFun -> Maybe QName)
-> ReduceM (Maybe PrimFun) -> ReduceM (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReduceM (Maybe PrimFun)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' "primErase"
let bEnv :: BuiltinEnv
bEnv = BuiltinEnv :: Maybe ConHead
-> Maybe ConHead
-> Maybe ConHead
-> Maybe ConHead
-> Maybe ConHead
-> Maybe QName
-> Maybe QName
-> BuiltinEnv
BuiltinEnv { bZero :: Maybe ConHead
bZero = Maybe ConHead
zero, bSuc :: Maybe ConHead
bSuc = Maybe ConHead
suc, bTrue :: Maybe ConHead
bTrue = Maybe ConHead
true, bFalse :: Maybe ConHead
bFalse = Maybe ConHead
false, bRefl :: Maybe ConHead
bRefl = Maybe ConHead
refl,
bPrimForce :: Maybe QName
bPrimForce = Maybe QName
force, bPrimErase :: Maybe QName
bPrimErase = Maybe QName
erase }
AllowedReductions
allowedReductions <- (TCEnv -> AllowedReductions) -> ReduceM AllowedReductions
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AllowedReductions
envAllowedReductions
Bool
rwr <- PragmaOptions -> Bool
optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
QName -> CompactDef
constInfo <- (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
forall a b. (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli ((QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef))
-> (QName -> ReduceM CompactDef) -> ReduceM (QName -> CompactDef)
forall a b. (a -> b) -> a -> b
$ \f :: QName
f -> do
Definition
info <- QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
RewriteRules
rewr <- if Bool
rwr then RewriteRules -> ReduceM RewriteRules
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
RewriteRules -> m RewriteRules
instantiateRewriteRules (RewriteRules -> ReduceM RewriteRules)
-> ReduceM RewriteRules -> ReduceM RewriteRules
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> ReduceM RewriteRules
forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
f
else RewriteRules -> ReduceM RewriteRules
forall (m :: * -> *) a. Monad m => a -> m a
return []
BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
compactDef BuiltinEnv
bEnv Definition
info RewriteRules
rewr
let flags :: ReductionFlags
flags = ReductionFlags :: Bool -> Bool -> Bool -> ReductionFlags
ReductionFlags{ allowNonTerminating :: Bool
allowNonTerminating = AllowedReduction
NonTerminatingReductions AllowedReduction -> AllowedReductions -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` AllowedReductions
allowedReductions
, allowUnconfirmed :: Bool
allowUnconfirmed = AllowedReduction
UnconfirmedReductions AllowedReduction -> AllowedReductions -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` AllowedReductions
allowedReductions
, hasRewriting :: Bool
hasRewriting = Bool
rwr }
(ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term)
forall a. (ReduceEnv -> a) -> ReduceM a
ReduceM ((ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term))
-> (ReduceEnv -> Blocked Term) -> ReduceM (Blocked Term)
forall a b. (a -> b) -> a -> b
$ \ redEnv :: ReduceEnv
redEnv -> ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> Normalisation
-> ReductionFlags
-> Term
-> Blocked Term
reduceTm ReduceEnv
redEnv BuiltinEnv
bEnv ((QName -> CompactDef) -> QName -> CompactDef
forall a. (QName -> a) -> QName -> a
memoQName QName -> CompactDef
constInfo) Normalisation
norm ReductionFlags
flags Term
v
unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli f :: a -> ReduceM b
f = (ReduceEnv -> a -> b) -> ReduceM (a -> b)
forall a. (ReduceEnv -> a) -> ReduceM a
ReduceM ((ReduceEnv -> a -> b) -> ReduceM (a -> b))
-> (ReduceEnv -> a -> b) -> ReduceM (a -> b)
forall a b. (a -> b) -> a -> b
$ \ env :: ReduceEnv
env x :: a
x -> ReduceM b -> ReduceEnv -> b
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (a -> ReduceM b
f a
x) ReduceEnv
env
data Closure s = Closure IsValue Term (Env s) (Spine s)
data IsValue = Value Blocked_ | Unevaled
type Spine s = [Elim' (Pointer s)]
isValue :: Closure s -> IsValue
isValue :: Closure s -> IsValue
isValue (Closure isV :: IsValue
isV _ _ _) = IsValue
isV
setIsValue :: IsValue -> Closure s -> Closure s
setIsValue :: IsValue -> Closure s -> Closure s
setIsValue isV :: IsValue
isV (Closure _ t :: Term
t env :: Env s
env spine :: 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
clApply :: Closure s -> Spine s -> Closure s
clApply :: Closure s -> Spine s -> Closure s
clApply c :: Closure s
c [] = Closure s
c
clApply (Closure _ t :: Term
t env :: Env s
env es :: Spine s
es) 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')
clApply_ :: Closure s -> Spine s -> Closure s
clApply_ :: Closure s -> Spine s -> Closure s
clApply_ c :: Closure s
c [] = Closure s
c
clApply_ (Closure b :: IsValue
b t :: Term
t env :: Env s
env es :: Spine s
es) 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')
data Pointer s = Pure (Closure s)
| Pointer {-# UNPACK #-} !(STPointer s)
type STPointer s = STRef s (Thunk (Closure s))
data Thunk a = BlackHole | Thunk a
deriving (a -> Thunk b -> Thunk a
(a -> b) -> Thunk a -> Thunk b
(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
<$ :: a -> Thunk b -> Thunk a
$c<$ :: forall a b. a -> Thunk b -> Thunk a
fmap :: (a -> b) -> Thunk a -> Thunk b
$cfmap :: forall a b. (a -> b) -> Thunk a -> Thunk b
Functor)
derefPointer :: Pointer s -> ST s (Thunk (Closure s))
derefPointer :: Pointer s -> ST s (Thunk (Closure s))
derefPointer (Pure x :: Closure s
x) = Thunk (Closure s) -> ST s (Thunk (Closure s))
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure s -> Thunk (Closure s)
forall a. a -> Thunk a
Thunk Closure s
x)
derefPointer (Pointer ptr :: STPointer s
ptr) = STPointer s -> ST s (Thunk (Closure s))
forall s a. STRef s a -> ST s a
readSTRef STPointer s
ptr
derefPointer_ :: Pointer s -> ST s (Closure s)
derefPointer_ :: Pointer s -> ST s (Closure s)
derefPointer_ ptr :: Pointer s
ptr = do
Thunk cl :: Closure s
cl <- Pointer s -> ST s (Thunk (Closure s))
forall s. Pointer s -> ST s (Thunk (Closure s))
derefPointer Pointer s
ptr
Closure s -> ST s (Closure s)
forall (m :: * -> *) a. Monad m => a -> m a
return Closure s
cl
unsafeDerefPointer :: Pointer s -> Thunk (Closure s)
unsafeDerefPointer :: Pointer s -> Thunk (Closure s)
unsafeDerefPointer (Pure x :: Closure s
x) = Closure s -> Thunk (Closure s)
forall a. a -> Thunk a
Thunk Closure s
x
unsafeDerefPointer (Pointer p :: 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 :: STPointer s -> ST s (Thunk (Closure s))
readPointer = STPointer s -> ST s (Thunk (Closure s))
forall s a. STRef s a -> ST s a
readSTRef
storePointer :: STPointer s -> Closure s -> ST s ()
storePointer :: STPointer s -> Closure s -> ST s ()
storePointer ptr :: 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)
blackHole :: STPointer s -> ST s ()
blackHole :: STPointer s -> ST s ()
blackHole ptr :: 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
createThunk :: Closure s -> ST s (Pointer s)
createThunk :: Closure s -> ST s (Pointer s)
createThunk (Closure _ (Var x :: Int
x []) env :: Env s
env spine :: Spine s
spine)
| Spine s -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Spine s
spine, Just p :: Pointer s
p <- Int -> Env s -> Maybe (Pointer s)
forall s. Int -> Env s -> Maybe (Pointer s)
lookupEnv Int
x Env s
env = Pointer s -> ST s (Pointer s)
forall (m :: * -> *) a. Monad m => a -> m a
return Pointer s
p
createThunk cl :: 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)
pureThunk :: Closure s -> Pointer s
pureThunk :: Closure s -> Pointer s
pureThunk = Closure s -> Pointer s
forall s. Closure s -> Pointer s
Pure
newtype Env s = Env [Pointer s]
emptyEnv :: Env s
emptyEnv :: Env s
emptyEnv = [Pointer s] -> Env s
forall s. [Pointer s] -> Env s
Env []
envSize :: Env s -> Int
envSize :: Env s -> Int
envSize (Env xs :: [Pointer s]
xs) = [Pointer s] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pointer s]
xs
envToList :: Env s -> [Pointer s]
envToList :: Env s -> [Pointer s]
envToList (Env xs :: [Pointer s]
xs) = [Pointer s]
xs
extendEnv :: Pointer s -> Env s -> Env s
extendEnv :: Pointer s -> Env s -> Env s
extendEnv p :: Pointer s
p (Env xs :: [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)
lookupEnv_ :: Int -> Env s -> Pointer s
lookupEnv_ :: Int -> Env s -> Pointer s
lookupEnv_ i :: Int
i (Env e :: [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
lookupEnv :: Int -> Env s -> Maybe (Pointer s)
lookupEnv :: Int -> Env s -> Maybe (Pointer s)
lookupEnv i :: Int
i e :: 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
data AM s = Eval (Closure s) !(ControlStack s)
| Match QName FastCompiledClauses (Spine s) (MatchStack s) (ControlStack s)
type ControlStack s = [ControlFrame s]
data MatchStack s = [CatchAllFrame s] :> Closure s
infixr 2 :>, >:
(>:) :: CatchAllFrame s -> MatchStack s -> MatchStack s
>: :: CatchAllFrame s -> MatchStack s -> MatchStack s
(>:) c :: CatchAllFrame s
c (cs :: [CatchAllFrame s]
cs :> cl :: 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
data CatchAllFrame s = CatchAll FastCompiledClauses (Spine s)
data ElimZipper a = ApplyCxt ArgInfo
| IApplyType a a | IApplyFst a a | IApplySnd a a
deriving (ElimZipper a -> ElimZipper a -> Bool
(ElimZipper a -> ElimZipper a -> Bool)
-> (ElimZipper a -> ElimZipper a -> Bool) -> Eq (ElimZipper a)
forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ElimZipper a -> ElimZipper a -> Bool
$c/= :: forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
== :: ElimZipper a -> ElimZipper a -> Bool
$c== :: forall a. Eq a => ElimZipper a -> ElimZipper a -> Bool
Eq, Eq (ElimZipper a)
Eq (ElimZipper a) =>
(ElimZipper a -> ElimZipper a -> Ordering)
-> (ElimZipper a -> ElimZipper a -> Bool)
-> (ElimZipper a -> ElimZipper a -> Bool)
-> (ElimZipper a -> ElimZipper a -> Bool)
-> (ElimZipper a -> ElimZipper a -> Bool)
-> (ElimZipper a -> ElimZipper a -> ElimZipper a)
-> (ElimZipper a -> ElimZipper a -> ElimZipper a)
-> Ord (ElimZipper a)
ElimZipper a -> ElimZipper a -> Bool
ElimZipper a -> ElimZipper a -> Ordering
ElimZipper a -> ElimZipper a -> ElimZipper a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (ElimZipper a)
forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
forall a. Ord a => ElimZipper a -> ElimZipper a -> Ordering
forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
min :: ElimZipper a -> ElimZipper a -> ElimZipper a
$cmin :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
max :: ElimZipper a -> ElimZipper a -> ElimZipper a
$cmax :: forall a. Ord a => ElimZipper a -> ElimZipper a -> ElimZipper a
>= :: ElimZipper a -> ElimZipper a -> Bool
$c>= :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
> :: ElimZipper a -> ElimZipper a -> Bool
$c> :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
<= :: ElimZipper a -> ElimZipper a -> Bool
$c<= :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
< :: ElimZipper a -> ElimZipper a -> Bool
$c< :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Bool
compare :: ElimZipper a -> ElimZipper a -> Ordering
$ccompare :: forall a. Ord a => ElimZipper a -> ElimZipper a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ElimZipper a)
Ord, Int -> ElimZipper a -> String -> String
[ElimZipper a] -> String -> String
ElimZipper a -> String
(Int -> ElimZipper a -> String -> String)
-> (ElimZipper a -> String)
-> ([ElimZipper a] -> String -> String)
-> Show (ElimZipper a)
forall a. Show a => Int -> ElimZipper a -> String -> String
forall a. Show a => [ElimZipper a] -> String -> String
forall a. Show a => ElimZipper a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [ElimZipper a] -> String -> String
$cshowList :: forall a. Show a => [ElimZipper a] -> String -> String
show :: ElimZipper a -> String
$cshow :: forall a. Show a => ElimZipper a -> String
showsPrec :: Int -> ElimZipper a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> ElimZipper a -> String -> String
Show, a -> ElimZipper b -> ElimZipper a
(a -> b) -> ElimZipper a -> ElimZipper b
(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
<$ :: a -> ElimZipper b -> ElimZipper a
$c<$ :: forall a b. a -> ElimZipper b -> ElimZipper a
fmap :: (a -> b) -> ElimZipper a -> ElimZipper b
$cfmap :: forall a b. (a -> b) -> ElimZipper a -> ElimZipper b
Functor, ElimZipper a -> Bool
(a -> m) -> ElimZipper a -> m
(a -> b -> b) -> b -> ElimZipper a -> b
(forall m. Monoid m => ElimZipper m -> m)
-> (forall m a. Monoid m => (a -> m) -> ElimZipper a -> m)
-> (forall m a. Monoid m => (a -> m) -> ElimZipper a -> m)
-> (forall a b. (a -> b -> b) -> b -> ElimZipper a -> b)
-> (forall a b. (a -> b -> b) -> b -> ElimZipper a -> b)
-> (forall b a. (b -> a -> b) -> b -> ElimZipper a -> b)
-> (forall b a. (b -> a -> b) -> b -> ElimZipper a -> b)
-> (forall a. (a -> a -> a) -> ElimZipper a -> a)
-> (forall a. (a -> a -> a) -> ElimZipper a -> a)
-> (forall a. ElimZipper a -> [a])
-> (forall a. ElimZipper a -> Bool)
-> (forall a. ElimZipper a -> Int)
-> (forall a. Eq a => a -> ElimZipper a -> Bool)
-> (forall a. Ord a => ElimZipper a -> a)
-> (forall a. Ord a => ElimZipper a -> a)
-> (forall a. Num a => ElimZipper a -> a)
-> (forall a. Num a => ElimZipper a -> a)
-> Foldable ElimZipper
forall a. Eq a => a -> ElimZipper a -> Bool
forall a. Num a => ElimZipper a -> a
forall a. Ord a => ElimZipper a -> a
forall m. Monoid m => ElimZipper m -> m
forall a. ElimZipper a -> Bool
forall a. ElimZipper a -> Int
forall a. ElimZipper a -> [a]
forall a. (a -> a -> a) -> ElimZipper a -> a
forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: ElimZipper a -> a
$cproduct :: forall a. Num a => ElimZipper a -> a
sum :: ElimZipper a -> a
$csum :: forall a. Num a => ElimZipper a -> a
minimum :: ElimZipper a -> a
$cminimum :: forall a. Ord a => ElimZipper a -> a
maximum :: ElimZipper a -> a
$cmaximum :: forall a. Ord a => ElimZipper a -> a
elem :: a -> ElimZipper a -> Bool
$celem :: forall a. Eq a => a -> ElimZipper a -> Bool
length :: ElimZipper a -> Int
$clength :: forall a. ElimZipper a -> Int
null :: ElimZipper a -> Bool
$cnull :: forall a. ElimZipper a -> Bool
toList :: ElimZipper a -> [a]
$ctoList :: forall a. ElimZipper a -> [a]
foldl1 :: (a -> a -> a) -> ElimZipper a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
foldr1 :: (a -> a -> a) -> ElimZipper a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ElimZipper a -> a
foldl' :: (b -> a -> b) -> b -> ElimZipper a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
foldl :: (b -> a -> b) -> b -> ElimZipper a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ElimZipper a -> b
foldr' :: (a -> b -> b) -> b -> ElimZipper a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
foldr :: (a -> b -> b) -> b -> ElimZipper a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ElimZipper a -> b
foldMap' :: (a -> m) -> ElimZipper a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
foldMap :: (a -> m) -> ElimZipper a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ElimZipper a -> m
fold :: ElimZipper m -> m
$cfold :: forall m. Monoid m => ElimZipper m -> m
Foldable, Functor ElimZipper
Foldable ElimZipper
(Functor ElimZipper, Foldable ElimZipper) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ElimZipper a -> f (ElimZipper b))
-> (forall (f :: * -> *) a.
Applicative f =>
ElimZipper (f a) -> f (ElimZipper a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ElimZipper a -> m (ElimZipper b))
-> (forall (m :: * -> *) a.
Monad m =>
ElimZipper (m a) -> m (ElimZipper a))
-> Traversable ElimZipper
(a -> f b) -> ElimZipper a -> f (ElimZipper b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
ElimZipper (m a) -> m (ElimZipper a)
forall (f :: * -> *) a.
Applicative f =>
ElimZipper (f a) -> f (ElimZipper a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ElimZipper a -> m (ElimZipper b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ElimZipper a -> f (ElimZipper b)
sequence :: ElimZipper (m a) -> m (ElimZipper a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
ElimZipper (m a) -> m (ElimZipper a)
mapM :: (a -> m b) -> ElimZipper a -> m (ElimZipper b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ElimZipper a -> m (ElimZipper b)
sequenceA :: ElimZipper (f a) -> f (ElimZipper a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
ElimZipper (f a) -> f (ElimZipper a)
traverse :: (a -> f b) -> ElimZipper a -> f (ElimZipper b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ElimZipper a -> f (ElimZipper b)
$cp2Traversable :: Foldable ElimZipper
$cp1Traversable :: Functor ElimZipper
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, 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 x y) = (a, ElimZipper a) -> Maybe (a, ElimZipper a)
forall a. a -> Maybe a
Just (a
a, a -> a -> ElimZipper a
forall a. a -> a -> ElimZipper a
IApplyType a
x a
y)
firstHole Proj{} = Maybe (Element (ElimZipper a), ElimZipper a)
forall a. Maybe a
Nothing
plugHole :: Element (ElimZipper a) -> ElimZipper a -> Carrier (ElimZipper a)
plugHole x :: Element (ElimZipper a)
x (ApplyCxt i :: 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 a :: Element (ElimZipper a)
a (IApplyType x :: a
x y :: 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 x :: Element (ElimZipper a)
x (IApplyFst a :: a
a y :: 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 y :: Element (ElimZipper a)
y (IApplySnd a :: a
a x :: 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 a :: Element (ElimZipper a)
a (IApplyType x :: a
x y :: 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 x :: Element (ElimZipper a)
x (IApplyFst a :: a
a y :: 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 y :: Element (ElimZipper a)
y (IApplySnd a :: a
a x :: 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 x :: 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)
type SpineContext s = ComposeZipper (ListZipper (Elim' (Pointer s)))
(ElimZipper (Pointer s))
data ControlFrame s = CaseK QName ArgInfo (FastCase FastCompiledClauses) (Spine s) (Spine s) (MatchStack s)
| ArgK (Closure s) (SpineContext s)
| NormaliseK
| ForceK QName (Spine s) (Spine s)
| EraseK QName (Spine s) (Spine s) (Spine s) (Spine s)
| NatSucK Integer
| PrimOpK QName ([Literal] -> Term) [Literal] [Pointer s] (Maybe FastCompiledClauses)
| UpdateThunk [STPointer s]
| ApplyK (Spine s)
compile :: Normalisation -> Term -> AM s
compile :: Normalisation -> Term -> AM s
compile nf :: Normalisation
nf t :: 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]
topMetaIsNotBlocked :: Blocked Term -> Blocked Term
topMetaIsNotBlocked :: Blocked Term -> Blocked Term
topMetaIsNotBlocked (Blocked _ t :: Term
t@MetaV{}) = Term -> Blocked Term
forall a. a -> Blocked a
notBlocked Term
t
topMetaIsNotBlocked b :: Blocked Term
b = Blocked Term
b
decodePointer :: Pointer s -> ST s Term
decodePointer :: Pointer s -> ST s Term
decodePointer p :: 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
decodeSpine :: Spine s -> ST s Elims
decodeSpine :: Spine s -> ST s Elims
decodeSpine spine :: Spine s
spine = ST s Elims -> ST s Elims
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s Elims -> ST s Elims) -> ST s Elims -> ST s Elims
forall a b. (a -> b) -> a -> b
$ ((Elim' (Pointer s) -> ST s (Elim' Term)) -> Spine s -> ST s Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Elim' (Pointer s) -> ST s (Elim' Term)) -> Spine s -> ST s Elims)
-> ((Pointer s -> ST s Term)
-> Elim' (Pointer s) -> ST s (Elim' Term))
-> (Pointer s -> ST s Term)
-> Spine s
-> ST s Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pointer s -> ST s Term) -> Elim' (Pointer s) -> ST s (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) Pointer s -> ST s Term
forall s. Pointer s -> ST s Term
decodePointer Spine s
spine
decodeEnv :: Env s -> ST s [Term]
decodeEnv :: Env s -> ST s [Term]
decodeEnv env :: Env s
env = ST s [Term] -> ST s [Term]
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s [Term] -> ST s [Term]) -> ST s [Term] -> ST s [Term]
forall a b. (a -> b) -> a -> b
$ (Pointer s -> ST s Term) -> [Pointer s] -> ST s [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Pointer s -> ST s Term
forall s. Pointer s -> ST s Term
decodePointer (Env s -> [Pointer s]
forall s. Env s -> [Pointer s]
envToList Env s
env)
decodeClosure_ :: Closure s -> ST s Term
decodeClosure_ :: Closure s -> ST s Term
decodeClosure_ = Blocked Term -> Term
forall t. Blocked t -> t
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
decodeClosure :: Closure s -> ST s (Blocked Term)
decodeClosure :: Closure s -> ST s (Blocked Term)
decodeClosure (Closure isV :: IsValue
isV t :: Term
t env :: Env s
env spine :: Spine s
spine) = do
[Term]
vs <- Env s -> ST s [Term]
forall s. Env s -> ST s [Term]
decodeEnv Env s
env
Elims
es <- Spine s -> ST s Elims
forall s. Spine s -> ST s Elims
decodeSpine Spine s
spine
Blocked Term -> ST s (Blocked Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Term -> ST s (Blocked Term))
-> Blocked Term -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Blocked Term
topMetaIsNotBlocked (Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst ([Term] -> Substitution' Term
forall a. [a] -> Substitution' a
parS [Term]
vs) Term
t) Elims
es Term -> Blocked_ -> Blocked Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked_
b)
where
parS :: [a] -> Substitution' a
parS = (a -> Substitution' a -> Substitution' a)
-> Substitution' a -> [a] -> Substitution' a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) Substitution' a
forall a. Substitution' a
IdS
b :: Blocked_
b = case IsValue
isV of
Value b :: Blocked_
b -> Blocked_
b
Unevaled -> () -> Blocked_
forall a. a -> Blocked a
notBlocked ()
elimsToSpine :: Env s -> Elims -> ST s (Spine s)
elimsToSpine :: Env s -> Elims -> ST s (Spine s)
elimsToSpine env :: Env s
env es :: Elims
es = do
Spine s
spine <- (Elim' Term -> ST s (Elim' (Pointer s))) -> Elims -> ST s (Spine s)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim' Term -> ST s (Elim' (Pointer s))
thunk Elims
es
Spine s -> ()
forall s. [Elim' (Pointer s)] -> ()
forceSpine Spine s
spine () -> ST s (Spine s) -> ST s (Spine s)
forall a b. a -> b -> b
`seq` Spine s -> ST s (Spine s)
forall (m :: * -> *) a. Monad m => a -> m a
return Spine s
spine
where
forceSpine :: [Elim' (Pointer s)] -> ()
forceSpine = (() -> Elim' (Pointer s) -> ()) -> () -> [Elim' (Pointer s)] -> ()
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ () -> Elim' (Pointer s) -> ()
forall s. Elim' (Pointer s) -> ()
forceEl) ()
forceEl :: Elim' (Pointer s) -> ()
forceEl (Apply (Arg _ (Pure Closure{}))) = ()
forceEl (Apply (Arg _ (Pointer{}))) = ()
forceEl _ = ()
unknownFVs :: ArgInfo -> ArgInfo
unknownFVs = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables
thunk :: Elim' Term -> ST s (Elim' (Pointer s))
thunk (Apply (Arg i :: ArgInfo
i t :: 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 o :: ProjOrigin
o f :: QName
f) = Elim' (Pointer s) -> ST s (Elim' (Pointer s))
forall (m :: * -> *) a. Monad m => a -> m a
return (ProjOrigin -> QName -> Elim' (Pointer s)
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f)
thunk (IApply a :: Term
a x :: Term
x y :: Term
y) = Pointer s -> Pointer s -> Pointer s -> Elim' (Pointer s)
forall a. a -> a -> a -> Elim' a
IApply (Pointer s -> Pointer s -> Pointer s -> Elim' (Pointer s))
-> ST s (Pointer s)
-> ST s (Pointer s -> Pointer s -> Elim' (Pointer s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ST s (Pointer s)
mkThunk Term
a ST s (Pointer s -> Pointer s -> Elim' (Pointer s))
-> ST s (Pointer s) -> ST s (Pointer s -> Elim' (Pointer s))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ST s (Pointer s)
mkThunk Term
x ST s (Pointer s -> Elim' (Pointer s))
-> ST s (Pointer s) -> ST s (Elim' (Pointer s))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ST s (Pointer s)
mkThunk Term
y
where mkThunk :: Term -> ST s (Pointer s)
mkThunk = Closure s -> ST s (Pointer s)
forall s. Closure s -> ST s (Pointer s)
createThunk (Closure s -> ST s (Pointer s))
-> (Term -> Closure s) -> Term -> ST s (Pointer s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeVariables -> Term -> Closure s
closure FreeVariables
UnknownFVs
closure :: FreeVariables -> Term -> Closure s
closure _ t :: Term
t@Lit{} = IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure (Blocked_ -> IsValue
Value (Blocked_ -> IsValue) -> Blocked_ -> IsValue
forall a b. (a -> b) -> a -> b
$ () -> Blocked_
forall a. a -> Blocked a
notBlocked ()) Term
t Env s
forall s. Env s
emptyEnv []
closure fv :: FreeVariables
fv t :: Term
t = Env s
env' Env s -> Closure s -> Closure s
forall a b. a -> b -> b
`seq` IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled Term
t Env s
env' []
where env' :: Env s
env' = FreeVariables -> Env s -> Env s
forall s. FreeVariables -> Env s -> Env s
trimEnvironment FreeVariables
fv Env s
env
trimEnvironment :: FreeVariables -> Env s -> Env s
trimEnvironment :: FreeVariables -> Env s -> Env s
trimEnvironment UnknownFVs env :: Env s
env = Env s
env
trimEnvironment (KnownFVs fvs :: IntSet
fvs) env :: Env s
env
| IntSet -> Bool
IntSet.null IntSet
fvs = Env s
forall s. Env s
emptyEnv
| Bool
otherwise = Env s
env
where
trim :: Int -> [Pointer Any] -> [Pointer Any]
trim _ [] = []
trim i :: Int
i (p :: Pointer Any
p : ps :: [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
+ 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
+ 1) [Pointer Any]
ps
buildEnv :: [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv :: [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv xs :: [Arg String]
xs spine :: Spine s
spine = [Arg String] -> Spine s -> Env s -> ([Arg String], Env s, Spine s)
forall a s.
[a]
-> [Elim' (Pointer s)]
-> Env s
-> ([a], Env s, [Elim' (Pointer s)])
go [Arg String]
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 [] sp :: [Elim' (Pointer s)]
sp env :: Env s
env = ([], Env s
env, [Elim' (Pointer s)]
sp)
go xs0 :: [a]
xs0@(x :: a
x : xs :: [a]
xs) sp :: [Elim' (Pointer s)]
sp env :: Env s
env =
case [Elim' (Pointer s)]
sp of
[] -> ([a]
xs0, Env s
env, [Elim' (Pointer s)]
sp)
Apply c :: Arg (Pointer s)
c : sp :: [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 x :: Pointer s
x y :: Pointer s
y r :: Pointer s
r : sp :: [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)
_ -> ([a], Env s, [Elim' (Pointer s)])
forall a. HasCallStack => a
__IMPOSSIBLE__
unusedPointerString :: String
unusedPointerString :: String
unusedPointerString = Impossible -> String
forall a. Show a => a -> String
show ((String -> Integer -> Impossible) -> Impossible
forall a b. (HasCallStack, Integral a) => (String -> a -> b) -> b
withFileAndLine String -> Integer -> Impossible
Impossible)
unusedPointer :: Pointer s
unusedPointer :: 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. a -> Blocked a
notBlocked ())
(Literal -> Term
Lit (Range -> String -> Literal
LitString Range
forall a. Range' a
noRange String
unusedPointerString)) Env s
forall s. Env s
emptyEnv [])
reduceTm :: ReduceEnv -> BuiltinEnv -> (QName -> CompactDef) -> Normalisation -> ReductionFlags -> Term -> Blocked Term
reduceTm :: ReduceEnv
-> BuiltinEnv
-> (QName -> CompactDef)
-> Normalisation
-> ReductionFlags
-> Term
-> Blocked Term
reduceTm rEnv :: ReduceEnv
rEnv bEnv :: BuiltinEnv
bEnv !QName -> CompactDef
constInfo normalisation :: Normalisation
normalisation ReductionFlags{..} =
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 "-- fast reduce --"
where
metaStore :: IntMap MetaVariable
metaStore = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState
-> Lens' (IntMap MetaVariable) TCState -> IntMap MetaVariable
forall o i. o -> Lens' i o -> i
^. Lens' (IntMap MetaVariable) TCState
stMetaStore
speculative :: Bool
speculative = ReduceEnv -> TCState
redSt ReduceEnv
rEnv TCState -> Lens' Bool TCState -> Bool
forall o i. o -> Lens' i o -> i
^. Lens' Bool TCState
stConsideringInstance
getMeta :: MetaId -> MetaInstantiation
getMeta m :: MetaId
m = MetaInstantiation
-> (MetaVariable -> MetaInstantiation)
-> Maybe MetaVariable
-> MetaInstantiation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe MetaInstantiation
forall a. HasCallStack => a
__IMPOSSIBLE__ MetaVariable -> MetaInstantiation
mvInstantiation (Int -> IntMap MetaVariable -> Maybe MetaVariable
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (MetaId -> Int
metaId MetaId
m) IntMap MetaVariable
metaStore)
partialDefs :: Set QName
partialDefs = ReduceM (Set QName) -> Set QName
forall a. ReduceM a -> a
runReduce ReduceM (Set QName)
forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
rewriteRules :: QName -> RewriteRules
rewriteRules f :: QName
f = CompactDef -> RewriteRules
cdefRewriteRules (QName -> CompactDef
constInfo QName
f)
callByNeed :: Bool
callByNeed = TCEnv -> Bool
envCallByNeed (ReduceEnv -> TCEnv
redEnv ReduceEnv
rEnv)
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 :: ReduceM a -> a
runReduce m :: ReduceM a
m = ReduceM a -> ReduceEnv -> a
forall a. ReduceM a -> ReduceEnv -> a
unReduceM ReduceM a
m ReduceEnv
rEnv
hasVerb :: String -> Int -> Bool
hasVerb tag :: String
tag lvl :: Int
lvl = ReduceM Bool -> ReduceEnv -> Bool
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (String -> Int -> ReduceM Bool
forall (m :: * -> *). MonadDebug m => String -> Int -> m Bool
hasVerbosity String
tag Int
lvl) ReduceEnv
rEnv
doDebug :: Bool
doDebug = String -> Int -> Bool
hasVerb "tc.reduce.fast" 110
traceDoc :: Doc -> a -> a
traceDoc :: Doc -> a -> a
traceDoc
| Bool
doDebug = String -> a -> a
forall a. String -> a -> a
trace (String -> a -> a) -> (Doc -> String) -> Doc -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show
| Bool
otherwise = (a -> a) -> Doc -> a -> a
forall a b. a -> b -> a
const a -> a
forall a. a -> a
id
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
Nothing -> Bool -> ConHead -> Bool
forall a b. a -> b -> a
const Bool
False
Just z :: 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
Nothing -> Bool -> ConHead -> Bool
forall a b. a -> b -> a
const Bool
False
Just s :: 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
refl :: Maybe ConHead
refl = Maybe ConHead
refl0 Maybe ConHead -> (ConHead -> Maybe ConHead) -> Maybe ConHead
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ c :: 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
== 0
then ConHead -> Maybe ConHead
forall a. a -> Maybe a
Just ConHead
c else Maybe ConHead
forall a. Maybe a
Nothing
compileAndRun :: Term -> Blocked Term
compileAndRun :: Term -> Blocked Term
compileAndRun t :: 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))
runAM :: AM s -> ST s (Blocked Term)
runAM :: AM s -> ST s (Blocked Term)
runAM = if Bool
doDebug then \ s :: AM s
s -> String -> ST s (Blocked Term) -> ST s (Blocked Term)
forall a. String -> a -> a
trace (AM s -> String
forall a. Pretty a => a -> String
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'
runAM' :: AM s -> ST s (Blocked Term)
runAM' :: AM s -> ST s (Blocked Term)
runAM' (Eval cl :: Closure s
cl@(Closure Value{} _ _ _) []) = Closure s -> ST s (Blocked Term)
forall s. Closure s -> ST s (Blocked Term)
decodeClosure Closure s
cl
runAM' s :: AM s
s@(Eval cl :: Closure s
cl@(Closure Unevaled t :: Term
t env :: Env s
env spine :: Spine s
spine) !ControlStack s
ctrl) = {-# SCC "runAM.Eval" #-}
case Term
t of
Def f :: QName
f [] ->
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
forall s.
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM Spine s
spine ControlStack s
ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
let CompactDef{ cdefDelayed :: CompactDef -> Bool
cdefDelayed = Bool
delayed
, cdefNonterminating :: CompactDef -> Bool
cdefNonterminating = Bool
nonterm
, cdefUnconfirmed :: CompactDef -> Bool
cdefUnconfirmed = Bool
unconf
, cdefDef :: CompactDef -> CompactDefn
cdefDef = CompactDefn
def } = QName -> CompactDef
constInfo QName
f
dontUnfold :: Bool
dontUnfold = (Bool
nonterm Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
allowNonTerminating) Bool -> Bool -> Bool
||
(Bool
unconf Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
allowUnconfirmed) Bool -> Bool -> Bool
||
(Bool
delayed Bool -> Bool -> Bool
&& Bool -> Bool
not (ControlStack s -> Bool
forall s. ControlStack s -> Bool
unfoldDelayed ControlStack s
ctrl))
in case CompactDefn
def of
CFun{ cfunCompiled :: CompactDefn -> FastCompiledClauses
cfunCompiled = FastCompiledClauses
cc }
| Bool
dontUnfold -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
rewriteAM AM s
done
| Bool
otherwise -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> 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] -> Closure s -> MatchStack s
forall s. [CatchAllFrame s] -> Closure s -> MatchStack s
:> Closure s
cl) ControlStack s
ctrl)
CAxiom -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
rewriteAM AM s
done
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
CForce | (spine0 :: Spine s
spine0, Apply v :: Arg (Pointer s)
v : spine1 :: Spine s
spine1) <- Int -> Spine s -> (Spine s, Spine s)
forall a. Int -> [a] -> ([a], [a])
splitAt 4 Spine s
spine ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
CForce -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
done
CErase | (spine0 :: Spine s
spine0, Apply v :: Arg (Pointer s)
v : spine1 :: Elim' (Pointer s)
spine1 : spine2 :: Spine s
spine2) <- Int -> Spine s -> (Spine s, Spine s)
forall a. Int -> [a] -> ([a], [a])
splitAt 2 Spine s
spine ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
CErase -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
done
CPrimOp n :: Int
n op :: [Literal] -> Term
op cc :: Maybe FastCompiledClauses
cc | Spine s -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Spine s
spine Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n,
Just (v :: Arg (Pointer s)
v : vs :: [Arg (Pointer s)]
vs) <- Spine s -> Maybe [Arg (Pointer s)]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Spine s
spine ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
CPrimOp{} -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
done
COther -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
fallbackAM AM s
s
Con c :: ConHead
c i :: 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 -> ControlStack s -> AM s
forall s. Term -> Env s -> Spine s -> ControlStack s -> AM s
evalTrueValue (Literal -> Term
Lit (Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange 0)) Env s
forall s. Env s
emptyEnv Spine s
spine ControlStack s
ctrl)
Con c :: ConHead
c i :: ConInfo
i [] | ConHead -> Bool
isSuc ConHead
c, Apply v :: Arg (Pointer s)
v : _ <- Spine s
spine ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (Arg (Pointer s) -> Pointer s
forall e. Arg e -> e
unArg Arg (Pointer s)
v) [] (ControlStack s -> ControlStack s
forall s. ControlStack s -> ControlStack s
sucCtrl ControlStack s
ctrl)
Con c :: ConHead
c i :: ConInfo
i []
| CCon{cconSrcCon :: CompactDefn -> ConHead
cconSrcCon = ConHead
c', cconArity :: CompactDefn -> Int
cconArity = Int
ar} <- CompactDef -> CompactDefn
cdefDef (QName -> CompactDef
constInfo (ConHead -> QName
conName ConHead
c)) ->
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
forall s.
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM Spine s
spine ControlStack s
ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
case Int -> Spine s -> (Spine s, Spine s)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
ar Spine s
spine of
(args :: Spine s
args, Proj _ p :: QName
p : spine' :: Spine s
spine')
-> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (Arg (Pointer s) -> Pointer s
forall e. Arg e -> e
unArg Arg (Pointer s)
arg) Spine s
spine' ControlStack s
ctrl
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 n :: Int
n = QName -> [QName] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex QName
p [QName]
fields
Apply arg :: Arg (Pointer s)
arg = Spine s
args Spine s -> Int -> Elim' (Pointer s)
forall a. [a] -> Int -> a
!! Int
n
_ -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
rewriteAM (Term -> Env s -> Spine s -> ControlStack 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 ControlStack s
ctrl)
| Bool
otherwise -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
done
Var x :: Int
x [] ->
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
forall s.
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM Spine s
spine ControlStack s
ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
case Int -> Env s -> Maybe (Pointer s)
forall s. Int -> Env s -> Maybe (Pointer s)
lookupEnv Int
x Env s
env of
Nothing -> 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_
forall a. a -> Blocked a
notBlocked ()) (Int -> Elims -> Term
Var (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Env s -> Int
forall s. Env s -> Int
envSize Env s
env) []) Env s
forall s. Env s
emptyEnv Spine s
spine ControlStack s
ctrl)
Just p :: Pointer s
p -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
p Spine s
spine ControlStack s
ctrl
Lam h :: ArgInfo
h b :: 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 :: Elim' (Pointer s)
elim : spine' :: Spine s
spine' ->
case Abs Term
b of
Abs _ b :: Term
b -> 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
b (Elim' (Pointer s) -> Pointer s
forall p. Elim' p -> p
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' ControlStack s
ctrl)
NoAbs _ b :: Term
b -> 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
b Env s
env Spine s
spine' ControlStack s
ctrl)
where
getArg :: Elim' p -> p
getArg (Apply v :: Arg p
v) = Arg p -> p
forall e. Arg e -> e
unArg Arg p
v
getArg (IApply _ _ v :: p
v) = p
v
getArg Proj{} = p
forall a. HasCallStack => a
__IMPOSSIBLE__
Lit{} -> 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
evalTrueValue Term
t Env s
forall s. Env s
emptyEnv [] ControlStack 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
Def f :: QName
f es :: 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 c :: ConHead
c i :: ConInfo
i es :: 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 x :: Int
x es :: 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 m :: MetaId
m es :: Elims
es -> Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
forall s.
Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM Spine s
spine ControlStack s
ctrl (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
case MetaId -> MetaInstantiation
getMeta MetaId
m of
InstV xs :: [Arg String]
xs t :: Term
t -> do
Spine s
spine' <- Env s -> Elims -> ST s (Spine s)
forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
let (zs :: [Arg String]
zs, env :: Env s
env, !Spine s
spine'') = [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
forall s. [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv [Arg String]
xs (Spine s
spine' Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine)
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s. Term -> Env s -> Spine s -> ControlStack s -> AM s
evalClosure ([Arg String] -> Term -> Term
lams [Arg String]
zs Term
t) Env s
env 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 (Blocked_ -> Closure s -> Closure s
forall s. Blocked_ -> Closure s -> Closure s
mkValue (MetaId -> () -> Blocked_
forall a. MetaId -> a -> Blocked a
blocked MetaId
m ()) Closure s
cl) ControlStack s
ctrl)
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 -> 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_
forall a. a -> Blocked a
notBlocked ()) Closure s
cl) ControlStack s
ctrl
shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims t :: Term
t env0 :: Env s
env0 env :: Env s
env es :: Elims
es = do
Spine s
spine' <- Env s -> Elims -> ST s (Spine s)
forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s. Term -> Env s -> Spine s -> ControlStack s -> AM s
evalClosure Term
t Env s
env0 (Spine s
spine' Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine) ControlStack s
ctrl)
runAM' s :: AM s
s@(Eval cl :: Closure s
cl@(Closure b :: IsValue
b t :: Term
t env :: Env s
env spine :: Spine s
spine) (NormaliseK : ctrl :: ControlStack s
ctrl)) =
case Term
t of
Def _ [] -> Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
b Term
t Env s
forall s. Env s
emptyEnv []) Spine s
spine ControlStack s
ctrl
Con _ _ [] -> Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
b Term
t Env s
forall s. Env s
emptyEnv []) Spine s
spine ControlStack s
ctrl
Var _ [] -> Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
b Term
t Env s
forall s. Env s
emptyEnv []) Spine s
spine ControlStack s
ctrl
MetaV _ [] -> Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
b Term
t Env s
forall s. Env s
emptyEnv []) Spine s
spine ControlStack s
ctrl
Lit{} -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
done
Def f :: QName
f es :: 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 c :: ConHead
c i :: ConInfo
i es :: 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 x :: Int
x es :: 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 m :: MetaId
m es :: 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
_ -> 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 -> 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_
forall a. a -> Blocked a
notBlocked ()) Closure s
cl) ControlStack s
ctrl
shiftElims :: Term -> Env s -> Env s -> Elims -> ST s (Blocked Term)
shiftElims t :: Term
t env0 :: Env s
env0 env :: Env s
env es :: Elims
es = do
Spine s
spine' <- Env s -> Elims -> ST s (Spine s)
forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Closure s -> 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
b Term
t Env s
env0 (Spine s
spine' Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine)) (ControlFrame s
forall s. ControlFrame s
NormaliseK ControlFrame s -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl))
runAM' (Eval cl :: Closure s
cl (ArgK cl0 :: Closure s
cl0 cxt :: SpineContext s
cxt : ctrl :: ControlStack s
ctrl)) =
case Element (SpineContext s)
-> SpineContext s
-> Either
(Carrier (SpineContext s))
(Element (SpineContext s), SpineContext s)
forall z.
Zipper z =>
Element z -> z -> Either (Carrier z) (Element z, z)
nextHole (Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk Closure s
cl) SpineContext s
cxt of
Left spine :: Carrier (SpineContext s)
spine -> 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
cl0 Spine s
Carrier (SpineContext s)
spine) ControlStack s
ctrl)
Right (p :: Element (SpineContext s)
p, cxt' :: SpineContext s
cxt') -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Element (SpineContext s)
Pointer s
p [] (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
cl0 SpineContext s
cxt' ControlFrame s -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
runAM' (Eval cl :: Closure s
cl@(Closure Value{} (Lit (LitNat r :: Range
r n :: Integer
n)) _ _) (NatSucK m :: Integer
m : ctrl :: ControlStack s
ctrl)) =
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
evalTrueValue (Literal -> Term
Lit (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$! Range -> Integer -> Literal
LitNat Range
r (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$! Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl)
runAM' (Eval cl :: Closure s
cl (NatSucK m :: Integer
m : ctrl :: 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 (Blocked_ -> Closure s -> Closure s
forall s. Blocked_ -> Closure s -> Closure s
mkValue (() -> Blocked_
forall a. a -> Blocked a
notBlocked ()) (Closure s -> Closure s) -> Closure s -> Closure s
forall a b. (a -> b) -> a -> b
$ Integer -> Closure s -> Closure s
plus Integer
m Closure s
cl) ControlStack s
ctrl)
where
plus :: Integer -> Closure s -> Closure s
plus 0 cl :: Closure s
cl = Closure s
cl
plus n :: Integer
n cl :: 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
- 1) Closure s
cl)
runAM' (Eval (Closure _ (Lit a :: Literal
a) _ _) (PrimOpK f :: QName
f op :: [Literal] -> Term
op vs :: [Literal]
vs es :: [Pointer s]
es cc :: Maybe FastCompiledClauses
cc : ctrl :: ControlStack 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 -> ControlStack 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 [] ControlStack s
ctrl)
e :: Pointer s
e : es' :: [Pointer s]
es' -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
e [] (QName
-> ([Literal] -> Term)
-> [Literal]
-> [Pointer s]
-> Maybe FastCompiledClauses
-> 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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
runAM' (Eval cl :: Closure s
cl@(Closure (Value blk :: Blocked_
blk) _ _ _) (PrimOpK f :: QName
f _ vs :: [Literal]
vs es :: [Pointer s]
es mcc :: Maybe FastCompiledClauses
mcc : ctrl :: ControlStack s
ctrl)) =
case Maybe FastCompiledClauses
mcc of
Nothing -> 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 Closure s
stuck ControlStack s
ctrl)
Just cc :: FastCompiledClauses
cc -> 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] -> Closure s -> MatchStack s
forall s. [CatchAllFrame s] -> Closure s -> MatchStack s
:> Closure s
notstuck) ControlStack s
ctrl)
where
p :: Pointer s
p = Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk Closure s
cl
lits :: [Pointer s]
lits = (Literal -> Pointer s) -> [Literal] -> [Pointer s]
forall a b. (a -> b) -> [a] -> [b]
map (Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk (Closure s -> Pointer s)
-> (Literal -> Closure s) -> Literal -> Pointer s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Closure s
forall s. Literal -> Closure s
litClos) ([Literal] -> [Literal]
forall a. [a] -> [a]
reverse [Literal]
vs)
spine :: Spine s
spine = (Pointer s -> Elim' (Pointer s)) -> [Pointer s] -> Spine s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg (Pointer s) -> Elim' (Pointer s)
forall a. Arg a -> Elim' a
Apply (Arg (Pointer s) -> Elim' (Pointer s))
-> (Pointer s -> Arg (Pointer s)) -> Pointer s -> Elim' (Pointer s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pointer s -> Arg (Pointer s)
forall a. a -> Arg a
defaultArg) ([Pointer s] -> Spine s) -> [Pointer s] -> Spine s
forall a b. (a -> b) -> a -> b
$ [Pointer s]
lits [Pointer s] -> [Pointer s] -> [Pointer s]
forall a. Semigroup a => a -> a -> a
<> [Pointer s
p] [Pointer s] -> [Pointer s] -> [Pointer s]
forall a. Semigroup a => a -> a -> a
<> [Pointer s]
es
stuck :: Closure s
stuck = IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure (Blocked_ -> IsValue
Value Blocked_
blk) (QName -> Elims -> Term
Def QName
f []) Env s
forall s. Env s
emptyEnv Spine s
spine
notstuck :: Closure s
notstuck = IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled (QName -> Elims -> Term
Def QName
f []) Env s
forall s. Env s
emptyEnv Spine s
spine
litClos :: Literal -> Closure s
litClos l :: 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 []
runAM' (Eval arg :: Closure s
arg@(Closure (Value blk :: Blocked_
blk) t :: Term
t _ _) (ForceK pf :: QName
pf spine0 :: Spine s
spine0 spine1 :: Spine s
spine1 : ctrl :: ControlStack s
ctrl))
| Term -> Bool
isCanonical Term
t =
case Spine s
spine1 of
Apply k :: Arg (Pointer s)
k : spine' :: Spine s
spine' ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (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') ControlStack s
ctrl
[] ->
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
evalTrueValue (Arg String -> Term -> Term
lam (String -> Arg String
forall a. a -> Arg a
defaultArg "k") (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var 0 [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var 1 []])
(Pointer s
argPtr Pointer s -> Env s -> Env s
forall s. Pointer s -> Env s -> Env s
`extendEnv` Env s
forall s. Env s
emptyEnv) [] ControlStack s
ctrl)
_ -> 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 -> ControlStack s -> AM s
forall s. Closure s -> ControlStack s -> AM s
Eval Closure s
stuck ControlStack s
ctrl)
where
argPtr :: Pointer s
argPtr = Closure s -> Pointer s
forall s. Closure s -> Pointer s
pureThunk Closure s
arg
elim :: 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 u :: Term
u = case Term
u of
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 q :: QName
q _
| CompactDefn
CTyCon <- CompactDef -> CompactDefn
cdefDef (QName -> CompactDef
constInfo QName
q) -> Bool
True
| Bool
otherwise -> Bool
False
runAM' (Eval cl2 :: Closure s
cl2@(Closure Value{} arg2 :: Term
arg2 _ _) (EraseK f :: QName
f spine0 :: Spine s
spine0 [Apply p1 :: Arg (Pointer s)
p1] _ spine3 :: Spine s
spine3 : ctrl :: ControlStack s
ctrl)) = do
cl1 :: Closure s
cl1@(Closure _ arg1 :: Term
arg1 _ sp1 :: Spine s
sp1) <- Pointer s -> ST s (Closure s)
forall s. Pointer s -> ST s (Closure s)
derefPointer_ (Arg (Pointer s) -> Pointer s
forall e. Arg e -> e
unArg Arg (Pointer s)
p1)
case (Term
arg1, Term
arg2) of
(Lit l1 :: Literal
l1, Lit l2 :: 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 -> ControlStack 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 [] ControlStack s
ctrl)
_ ->
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 -> ControlStack 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 ControlStack s
ctrl)
runAM' (Eval cl1 :: Closure s
cl1@(Closure Value{} _ _ _) (EraseK f :: QName
f spine0 :: Spine s
spine0 [] [Apply p2 :: Arg (Pointer s)
p2] spine3 :: Spine s
spine3 : ctrl :: ControlStack s
ctrl)) =
Pointer s -> Spine s -> ControlStack 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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl)
runAM' (Eval _ (EraseK{} : _)) =
ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
runAM' (Eval cl :: Closure s
cl@(Closure Value{} _ _ _) (UpdateThunk ps :: [STPointer s]
ps : ctrl :: ControlStack s
ctrl)) =
(STPointer s -> ST s ()) -> [STPointer s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (STPointer s -> Closure s -> ST s ()
forall s. STPointer s -> Closure s -> ST s ()
`storePointer` Closure s
cl) [STPointer s]
ps ST s () -> ST s (Blocked Term) -> ST s (Blocked Term)
forall (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 -> ControlStack s -> AM s
forall s. Closure s -> ControlStack s -> AM s
Eval Closure s
cl ControlStack s
ctrl)
runAM' (Eval cl :: Closure s
cl@(Closure Value{} _ _ _) (ApplyK spine :: Spine s
spine : ctrl :: 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)
runAM' (Eval cl :: Closure s
cl@(Closure (Value blk :: Blocked_
blk) t :: Term
t env :: Env s
env spine :: Spine s
spine) ctrl0 :: ControlStack s
ctrl0@(CaseK f :: QName
f i :: ArgInfo
i bs :: FastCase FastCompiledClauses
bs spine0 :: Spine s
spine0 spine1 :: Spine s
spine1 stack :: MatchStack s
stack : ctrl :: ControlStack s
ctrl)) =
{-# SCC "runAM.CaseK" #-}
case Blocked_
blk of
Blocked{} | [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [()|Con{} <- [Term
t]] -> ST s (Blocked Term)
stuck
_ -> case Term
t of
Con c :: ConHead
c ci :: ConInfo
ci [] | ConHead -> Bool
isSuc ConHead
c -> ST s (Blocked Term) -> ST s (Blocked Term)
matchSuc (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Con c :: ConHead
c ci :: ConInfo
ci [] -> ConHead
-> ConInfo -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
matchCon ConHead
c ConInfo
ci (Spine s -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Spine s
spine) (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Con c :: ConHead
c ci :: ConInfo
ci es :: Elims
es -> do
Spine s
spine' <- Env s -> Elims -> ST s (Spine s)
forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue Blocked_
blk (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) Env s
forall s. Env s
emptyEnv (Spine s
spine' Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine) ControlStack s
ctrl0)
Lit (LitNat _ 0) -> ST s (Blocked Term) -> ST s (Blocked Term)
matchLitZero (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Lit (LitNat _ n :: Integer
n) -> Integer -> ST s (Blocked Term) -> ST s (Blocked Term)
matchLitSuc Integer
n (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Lit l :: Literal
l -> Literal -> ST s (Blocked Term) -> ST s (Blocked Term)
matchLit Literal
l (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Def q :: QName
q [] | Maybe FastCompiledClauses -> Bool
forall a. Maybe a -> Bool
isJust (Maybe FastCompiledClauses -> Bool)
-> Maybe FastCompiledClauses -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
lookupCon QName
q FastCase FastCompiledClauses
bs -> QName -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
matchCon' QName
q (Spine s -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Spine s
spine) (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ ST s (Blocked Term) -> ST s (Blocked Term)
matchCatchall (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch QName
f MatchStack s
stack ControlStack s
ctrl
Def q :: QName
q es :: Elims
es | Maybe FastCompiledClauses -> Bool
forall a. Maybe a -> Bool
isJust (Maybe FastCompiledClauses -> Bool)
-> Maybe FastCompiledClauses -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
lookupCon QName
q FastCase FastCompiledClauses
bs -> do
Spine s
spine' <- Env s -> Elims -> ST s (Spine s)
forall s. Env s -> Elims -> ST s (Spine s)
elimsToSpine Env s
env Elims
es
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue Blocked_
blk (QName -> Elims -> Term
Def QName
q []) Env s
forall s. Env s
emptyEnv (Spine s
spine' Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine) ControlStack s
ctrl0)
_ -> ST s (Blocked Term)
stuck
where
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
Blocked_
blk' <- case Blocked_
blk of
Blocked{} -> Blocked_ -> ST s Blocked_
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked_
blk
NotBlocked r :: NotBlocked
r _ -> Closure s -> ST s Term
forall s. Closure s -> ST s Term
decodeClosure_ Closure s
cl ST s Term -> (Term -> Blocked_) -> ST s Blocked_
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ v :: Term
v -> NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked (Elim' Term -> NotBlocked -> NotBlocked
stuckOn (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i Term
v) NotBlocked
r) ()
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch Blocked_
blk' MatchStack s
stack ControlStack s
ctrl
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
catchallStack :: MatchStack s
catchallStack = case FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. FastCase c -> Maybe c
fcatchAllBranch FastCase FastCompiledClauses
bs of
Nothing -> MatchStack s
stack
Just cc :: 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
(m :: Maybe a
m ifJust :: Maybe a -> (a -> b) -> b -> b
`ifJust` f :: a -> b
f) z :: 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
matchCon :: ConHead
-> ConInfo -> Int -> ST s (Blocked Term) -> ST s (Blocked Term)
matchCon c :: ConHead
c ci :: ConInfo
ci ar :: 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' q :: QName
q ar :: 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` \ cc :: FastCompiledClauses
cc ->
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
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 ControlStack s
ctrl)
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` \ cc :: FastCompiledClauses
cc ->
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
catchallSpine MatchStack s
stack ControlStack s
ctrl)
matchLit :: Literal -> ST s (Blocked Term) -> ST s (Blocked Term)
matchLit l :: 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` \ cc :: FastCompiledClauses
cc ->
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
spine0 Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine1) MatchStack s
catchallStack ControlStack s
ctrl)
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` \ cc :: FastCompiledClauses
cc ->
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
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 ControlStack s
ctrl)
matchLitSuc :: Integer -> ST s (Blocked Term) -> ST s (Blocked Term)
matchLitSuc n :: 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` \ cc :: FastCompiledClauses
cc ->
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
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 ControlStack s
ctrl)
where n' :: Integer
n' = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 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
$ Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange Integer
n') Env s
forall s. Env s
emptyEnv []
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 0
runAM' (Match f :: QName
f cc :: FastCompiledClauses
cc spine :: Spine s
spine stack :: MatchStack s
stack ctrl :: ControlStack s
ctrl) = {-# SCC "runAM.Match" #-}
case FastCompiledClauses
cc of
FFail -> Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch (NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
AbsurdMatch ()) MatchStack s
stack ControlStack s
ctrl
FDone xs :: [Arg String]
xs body :: Term
body -> do
let (zs :: [Arg String]
zs, env :: Env s
env, !Spine s
spine') = [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
forall s. [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv [Arg String]
xs Spine s
spine
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 (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled ([Arg String] -> Term -> Term
lams [Arg String]
zs Term
body) Env s
env Spine s
spine') ControlStack s
ctrl)
FEta n :: Int
n fs :: [Arg QName]
fs cc :: FastCompiledClauses
cc ca :: Maybe FastCompiledClauses
ca ->
case Int -> Spine s -> (Spine s, Spine s)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Spine s
spine of
(_, []) -> NotBlocked -> ST s (Blocked Term)
done NotBlocked
Underapplied
(spine0 :: Spine s
spine0, Apply e :: Arg (Pointer s)
e : spine1 :: Spine s
spine1) -> do
let projClosure :: Arg QName -> Closure s
projClosure (Arg ai :: ArgInfo
ai f :: 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 0 []) (Pointer s -> Env s -> Env s
forall s. Pointer s -> Env s -> Env s
extendEnv (Arg (Pointer s) -> Pointer s
forall e. Arg e -> e
unArg Arg (Pointer s)
e) Env s
forall s. Env s
emptyEnv) [ProjOrigin -> QName -> Elim' (Pointer s)
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
[Pointer s]
projs <- (Arg QName -> ST s (Pointer s)) -> [Arg QName] -> ST s [Pointer s]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Closure s -> ST s (Pointer s)
forall s. Closure s -> ST s (Pointer s)
createThunk (Closure s -> ST s (Pointer s))
-> (Arg QName -> Closure s) -> Arg QName -> ST s (Pointer s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> Closure s
projClosure) [Arg QName]
fs
let spine' :: Spine s
spine' = Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> (Pointer s -> Elim' (Pointer s)) -> [Pointer s] -> Spine s
forall a b. (a -> b) -> [a] -> [b]
map (Arg (Pointer s) -> Elim' (Pointer s)
forall a. Arg a -> Elim' a
Apply (Arg (Pointer s) -> Elim' (Pointer s))
-> (Pointer s -> Arg (Pointer s)) -> Pointer s -> Elim' (Pointer s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pointer s -> Arg (Pointer s)
forall a. a -> Arg a
defaultArg) [Pointer s]
projs Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine1
stack' :: MatchStack s
stack' = Maybe FastCompiledClauses
-> MatchStack s
-> (FastCompiledClauses -> MatchStack s)
-> MatchStack s
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe FastCompiledClauses
ca MatchStack s
stack ((FastCompiledClauses -> MatchStack s) -> MatchStack s)
-> (FastCompiledClauses -> MatchStack s) -> MatchStack s
forall a b. (a -> b) -> a -> b
$ \ cc :: FastCompiledClauses
cc -> FastCompiledClauses -> Spine s -> CatchAllFrame s
forall s. FastCompiledClauses -> Spine s -> CatchAllFrame s
CatchAll FastCompiledClauses
cc Spine s
spine CatchAllFrame s -> MatchStack s -> MatchStack s
forall s. CatchAllFrame s -> MatchStack s -> MatchStack s
>: MatchStack s
stack
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> AM s
forall s.
QName
-> FastCompiledClauses
-> Spine s
-> MatchStack s
-> ControlStack s
-> AM s
Match QName
f FastCompiledClauses
cc Spine s
spine' MatchStack s
stack' ControlStack s
ctrl)
_ -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
FCase n :: Int
n bs :: FastCase FastCompiledClauses
bs ->
case Int -> Spine s -> (Spine s, Spine s)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Spine s
spine of
(_, []) -> NotBlocked -> ST s (Blocked Term)
done NotBlocked
Underapplied
(spine0 :: Spine s
spine0, Apply e :: Arg (Pointer s)
e : spine1 :: Spine s
spine1) ->
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (Arg (Pointer s) -> Pointer s
forall e. Arg e -> e
unArg Arg (Pointer s)
e) [] (ControlStack s -> ST s (Blocked Term))
-> ControlStack s -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ QName
-> ArgInfo
-> FastCase FastCompiledClauses
-> Spine s
-> Spine s
-> MatchStack s
-> 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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl
(spine0 :: Spine s
spine0, Proj o :: ProjOrigin
o p :: QName
p : spine1 :: Spine s
spine1) ->
case QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
lookupCon QName
p FastCase FastCompiledClauses
bs Maybe FastCompiledClauses
-> Maybe FastCompiledClauses -> Maybe FastCompiledClauses
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((QName -> FastCase FastCompiledClauses -> Maybe FastCompiledClauses
forall c. QName -> FastCase c -> Maybe c
`lookupCon` FastCase FastCompiledClauses
bs) (QName -> Maybe FastCompiledClauses)
-> Maybe QName -> Maybe FastCompiledClauses
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe QName
op) of
Nothing
| QName
f QName -> Set QName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
partialDefs -> Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch (NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
MissingClauses ()) MatchStack s
stack ControlStack s
ctrl
| Bool
otherwise -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
Just cc :: FastCompiledClauses
cc -> 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
spine0 Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine1) MatchStack s
stack ControlStack s
ctrl)
where CFun{ cfunProjection :: CompactDefn -> Maybe QName
cfunProjection = Maybe QName
op } = CompactDef -> CompactDefn
cdefDef (QName -> CompactDef
constInfo QName
p)
(_, IApply{} : _) -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
where done :: NotBlocked -> ST s (Blocked Term)
done why :: NotBlocked
why = Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
forall s.
Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch (NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
why ()) MatchStack s
stack ControlStack s
ctrl
evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (Pure cl :: Closure s
cl) spine :: Spine s
spine ctrl :: 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 p :: STPointer s
p) spine :: Spine s
spine ctrl :: ControlStack s
ctrl = STPointer s -> ST s (Thunk (Closure s))
forall s. STPointer s -> ST s (Thunk (Closure s))
readPointer STPointer s
p ST s (Thunk (Closure s))
-> (Thunk (Closure s) -> ST s (Blocked Term))
-> ST s (Blocked Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
BlackHole -> ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
Thunk cl :: Closure s
cl@(Closure Unevaled _ _ _) | Bool
callByNeed -> do
STPointer s -> ST s ()
forall s. STPointer s -> ST s ()
blackHole STPointer s
p
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Closure s -> ControlStack s -> AM s
forall s. Closure s -> ControlStack s -> AM s
Eval Closure s
cl (ControlStack s -> AM s) -> ControlStack s -> AM s
forall a b. (a -> b) -> a -> b
$ STPointer s -> ControlStack s -> ControlStack s
forall s. STPointer s -> ControlStack s -> ControlStack s
updateThunkCtrl STPointer s
p (ControlStack s -> ControlStack s)
-> ControlStack s -> ControlStack s
forall a b. (a -> b) -> a -> b
$ [Spine s -> ControlFrame s
forall s. Spine s -> ControlFrame s
ApplyK Spine s
spine | Bool -> Bool
not (Spine s -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Spine s
spine)] ControlStack s -> ControlStack s -> ControlStack s
forall a. [a] -> [a] -> [a]
++ ControlStack s
ctrl)
Thunk cl :: 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 s -> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM :: Spine s
-> ControlStack s -> ST s (Blocked Term) -> ST s (Blocked Term)
evalIApplyAM es :: Spine s
es ctrl :: ControlStack s
ctrl fallback :: ST s (Blocked Term)
fallback = Spine s -> ST s (Blocked Term)
go Spine s
es
where
go :: Spine s -> ST s (Blocked Term)
go [] = ST s (Blocked Term)
fallback
go (IApply x :: Pointer s
x y :: Pointer s
y r :: Pointer s
r : es :: Spine s
es) = do
Blocked Term
br <- Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Pointer s
r [] []
case Term -> IntervalView
iview (Term -> IntervalView) -> Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
br of
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
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
_ -> (Blocked Term -> Blocked_ -> Blocked Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Blocked Term -> Blocked_
blockedOrMeta 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 (e :: Elim' (Pointer s)
e : es :: Spine s
es) = Spine s -> ST s (Blocked Term)
go Spine s
es
normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM cl :: Closure s
cl [] ctrl :: 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)
normaliseArgsAM cl :: Closure s
cl spine :: Spine s
spine ctrl :: ControlStack s
ctrl =
case Carrier (SpineContext s)
-> Maybe (Element (SpineContext s), SpineContext s)
forall z. Zipper z => Carrier z -> Maybe (Element z, z)
firstHole Spine s
Carrier (SpineContext s)
spine of
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 -> Spine s -> Closure s
forall s. Closure s -> Spine s -> Closure s
clApply_ Closure s
cl Spine s
spine) ControlStack s
ctrl)
Just (p :: Element (SpineContext s)
p, cxt :: SpineContext s
cxt) -> Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
forall s.
Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM Element (SpineContext s)
Pointer s
p [] (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)
fallbackAM :: AM s -> ST s (Blocked Term)
fallbackAM :: AM s -> ST s (Blocked Term)
fallbackAM (Eval c :: Closure s
c ctrl :: ControlStack s
ctrl) = do
Term
v <- Closure s -> ST s Term
forall s. Closure s -> ST s Term
decodeClosure_ Closure s
c
AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Blocked Term -> AM s
mkValue (Blocked Term -> AM s) -> Blocked Term -> AM s
forall a b. (a -> b) -> a -> b
$ ReduceM (Blocked Term) -> Blocked Term
forall a. ReduceM a -> a
runReduce (ReduceM (Blocked Term) -> Blocked Term)
-> ReduceM (Blocked Term) -> Blocked Term
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM (Blocked Term)
slow Term
v)
where mkValue :: Blocked Term -> AM s
mkValue b :: Blocked Term
b = Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue (() () -> Blocked Term -> Blocked_
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked Term
b) (Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
b) Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl'
(slow :: Term -> ReduceM (Blocked Term)
slow, ctrl' :: ControlStack s
ctrl') = case ControlStack s
ctrl of
NormaliseK : ctrl' :: ControlStack s
ctrl'
| Value{} <- Closure s -> IsValue
forall s. Closure s -> IsValue
isValue Closure s
c -> (Term -> Blocked Term
forall a. a -> Blocked 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')
_ -> (Term -> ReduceM (Blocked Term)
slowReduceTerm, ControlStack s
ctrl)
fallbackAM _ = ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
rewriteAM :: AM s -> ST s (Blocked Term)
rewriteAM :: AM s -> ST s (Blocked Term)
rewriteAM = if Bool
hasRewriting then AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
rewriteAM' else AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM
rewriteAM' :: AM s -> ST s (Blocked Term)
rewriteAM' :: AM s -> ST s (Blocked Term)
rewriteAM' s :: AM s
s@(Eval (Closure (Value blk :: Blocked_
blk) t :: Term
t env :: Env s
env spine :: Spine s
spine) ctrl :: ControlStack s
ctrl)
| RewriteRules -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null RewriteRules
rewr = AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM AM s
s
| Bool
otherwise = Doc -> ST s (Blocked Term) -> ST s (Blocked Term)
forall a. Doc -> a -> a
traceDoc ("R" Doc -> Doc -> Doc
<+> AM s -> Doc
forall a. Pretty a => a -> Doc
pretty AM s
s) (ST s (Blocked Term) -> ST s (Blocked Term))
-> ST s (Blocked Term) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$ do
Term
v0 <- Closure s -> ST s Term
forall s. Closure s -> ST s Term
decodeClosure_ (IsValue -> Term -> Env s -> Spine s -> Closure s
forall s. IsValue -> Term -> Env s -> Spine s -> Closure s
Closure IsValue
Unevaled Term
t Env s
env [])
Elims
es <- Spine s -> ST s Elims
forall s. Spine s -> ST s Elims
decodeSpine Spine s
spine
case ReduceM (Reduced (Blocked Term) Term)
-> Reduced (Blocked Term) Term
forall a. ReduceM a -> a
runReduce (Blocked_
-> Term
-> RewriteRules
-> Elims
-> ReduceM (Reduced (Blocked Term) Term)
rewrite Blocked_
blk Term
v0 RewriteRules
rewr Elims
es) of
NoReduction b :: Blocked Term
b -> AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
runAM (Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
forall s.
Blocked_ -> Term -> Env s -> Spine s -> ControlStack s -> AM s
evalValue (() () -> Blocked Term -> Blocked_
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked Term
b) (Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
b) Env s
forall s. Env s
emptyEnv [] ControlStack s
ctrl)
YesReduction _ v :: 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 f :: QName
f [] -> QName -> RewriteRules
rewriteRules QName
f
Con c :: ConHead
c _ [] -> QName -> RewriteRules
rewriteRules (ConHead -> QName
conName ConHead
c)
_ -> RewriteRules
forall a. HasCallStack => a
__IMPOSSIBLE__
rewriteAM' _ =
ST s (Blocked Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
sucCtrl :: ControlStack s -> ControlStack s
sucCtrl :: ControlStack s -> ControlStack s
sucCtrl (NatSucK !Integer
n : ctrl :: ControlStack s
ctrl) = Integer -> ControlFrame s
forall s. Integer -> ControlFrame s
NatSucK (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) ControlFrame s -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl
sucCtrl ctrl :: ControlStack s
ctrl = Integer -> ControlFrame s
forall s. Integer -> ControlFrame s
NatSucK 1 ControlFrame s -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl
updateThunkCtrl :: STPointer s -> ControlStack s -> ControlStack s
updateThunkCtrl :: STPointer s -> ControlStack s -> ControlStack s
updateThunkCtrl p :: STPointer s
p (UpdateThunk ps :: [STPointer s]
ps : ctrl :: ControlStack 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 -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl
updateThunkCtrl p :: STPointer s
p ctrl :: ControlStack s
ctrl = [STPointer s] -> ControlFrame s
forall s. [STPointer s] -> ControlFrame s
UpdateThunk [STPointer s
p] ControlFrame s -> ControlStack s -> ControlStack s
forall a. a -> [a] -> [a]
: ControlStack s
ctrl
unfoldDelayed :: ControlStack s -> Bool
unfoldDelayed :: ControlStack s -> Bool
unfoldDelayed [] = Bool
False
unfoldDelayed (CaseK{} : _) = Bool
True
unfoldDelayed (PrimOpK{} : _) = Bool
False
unfoldDelayed (NatSucK{} : _) = Bool
False
unfoldDelayed (NormaliseK{} : _) = Bool
False
unfoldDelayed (ArgK{} : _) = Bool
False
unfoldDelayed (UpdateThunk{} : ctrl :: ControlStack s
ctrl) = ControlStack s -> Bool
forall s. ControlStack s -> Bool
unfoldDelayed ControlStack s
ctrl
unfoldDelayed (ApplyK{} : ctrl :: ControlStack s
ctrl) = ControlStack s -> Bool
forall s. ControlStack s -> Bool
unfoldDelayed ControlStack s
ctrl
unfoldDelayed (ForceK{} : ctrl :: ControlStack s
ctrl) = ControlStack s -> Bool
forall s. ControlStack s -> Bool
unfoldDelayed ControlStack s
ctrl
unfoldDelayed (EraseK{} : ctrl :: ControlStack s
ctrl) = ControlStack s -> Bool
forall s. ControlStack s -> Bool
unfoldDelayed ControlStack s
ctrl
stuckMatch :: Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch :: Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch blk :: Blocked_
blk (_ :> cl :: Closure s
cl) ctrl :: 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)
failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch f :: QName
f (CatchAll cc :: FastCompiledClauses
cc spine :: Spine s
spine : stack :: [CatchAllFrame s]
stack :> cl :: Closure s
cl) ctrl :: 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 f :: QName
f ([] :> cl :: Closure s
cl) ctrl :: ControlStack s
ctrl
| 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 -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
MissingClauses ()) Closure s
cl) ControlStack s
ctrl)
| QName
f QName -> Set QName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
partialDefs = AM s -> ST s (Blocked Term)
forall s. AM s -> ST s (Blocked Term)
rewriteAM (Closure s -> ControlStack s -> AM s
forall s. Closure s -> ControlStack s -> AM s
Eval (Blocked_ -> Closure s -> Closure s
forall s. Blocked_ -> Closure s -> Closure s
mkValue (NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
MissingClauses ()) Closure s
cl) ControlStack s
ctrl)
| Bool
otherwise = ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term)
forall a. ReduceM a -> a
runReduce (ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term))
-> ReduceM (ST s (Blocked Term)) -> ST s (Blocked Term)
forall a b. (a -> b) -> a -> b
$
String
-> Int
-> String
-> ReduceM (ST s (Blocked Term))
-> ReduceM (ST s (Blocked Term))
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
traceSLn "impossible" 10 ("Incomplete pattern matching when applying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
f)
ReduceM (ST s (Blocked Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
evalClosure :: Term -> Env s -> Spine s -> ControlStack s -> AM s
evalClosure t :: Term
t env :: Env s
env spine :: 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 b :: Blocked_
b t :: Term
t env :: Env s
env spine :: 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. a -> Blocked a
notBlocked ()
trueValue :: Term -> Env s -> Spine s -> Closure s
trueValue t :: Term
t env :: Env s
env spine :: 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. a -> Blocked a
notBlocked ()) Term
t Env s
env Spine s
spine
mkValue :: Blocked_ -> Closure s -> Closure s
mkValue b :: Blocked_
b = IsValue -> Closure s -> Closure s
forall s. IsValue -> Closure s -> Closure s
setIsValue (Blocked_ -> IsValue
Value Blocked_
b)
lams :: [Arg String] -> Term -> Term
lams :: [Arg String] -> Term -> Term
lams xs :: [Arg String]
xs t :: Term
t = (Arg String -> Term -> Term) -> Term -> [Arg String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg String -> Term -> Term
lam Term
t [Arg String]
xs
lam :: Arg String -> Term -> Term
lam :: Arg String -> Term -> Term
lam x :: Arg String
x t :: Term
t = ArgInfo -> Abs Term -> Term
Lam (Arg String -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg String
x) (String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs (Arg String -> String
forall e. Arg e -> e
unArg Arg String
x) Term
t)
instance Pretty a => Pretty (FastCase a) where
prettyPrec :: Int -> FastCase a -> Doc
prettyPrec p :: Int
p (FBranches _cop :: Bool
_cop cs :: Map NameId a
cs suc :: Maybe a
suc ls :: Map Literal a
ls m :: Maybe a
m _) =
Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [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 Nothing = []
prC (Just x :: a
x) = ["_ ->" Doc -> Doc -> Doc
<?> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x]
prSuc :: Maybe a -> [Doc]
prSuc Nothing = []
prSuc (Just x :: a
x) = ["suc ->" Doc -> Doc -> Doc
<?> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x]
instance Pretty FastCompiledClauses where
pretty :: FastCompiledClauses -> Doc
pretty (FDone xs :: [Arg String]
xs t :: Term
t) = ("done" Doc -> Doc -> Doc
<+> [Arg String] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Arg String]
xs) Doc -> Doc -> Doc
<?> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec 10 Term
t
pretty FFail = "fail"
pretty (FEta n :: Int
n _ cc :: FastCompiledClauses
cc ca :: Maybe FastCompiledClauses
ca) =
String -> Doc
text ("eta " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " of") Doc -> Doc -> Doc
<?>
[Doc] -> Doc
vcat ([ "{} ->" 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
<?> FastCompiledClauses -> Doc
forall a. Pretty a => a -> Doc
pretty FastCompiledClauses
cc | Just cc :: FastCompiledClauses
cc <- [Maybe FastCompiledClauses
ca] ])
pretty (FCase n :: Int
n bs :: FastCase FastCompiledClauses
bs) | FastCase FastCompiledClauses -> Bool
forall c. FastCase c -> Bool
fprojPatterns FastCase FastCompiledClauses
bs =
[Doc] -> Doc
sep [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "project " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
, Int -> Doc -> Doc
nest 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 n :: Int
n bs :: FastCase FastCompiledClauses
bs) =
String -> Doc
text ("case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 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 _ BlackHole = "<BLACKHOLE>"
prettyPrec p :: Int
p (Thunk cl :: 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 p :: 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 _ (Closure Value{} (Lit (LitString _ unused :: String
unused)) _ _)
| String
unused String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
unusedPointerString = "_"
prettyPrec p :: Int
p (Closure isV :: IsValue
isV t :: Term
t env :: Env s
env spine :: Spine s
spine) =
Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep [ String -> Doc
text String
tag
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec 10 Term
t
, Int -> Doc -> Doc
nest 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 [0..] (Env s -> [Pointer s]
forall s. Env s -> [Pointer s]
envToList Env s
env)
, Int -> Doc -> Doc
nest 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 i :: a
i c :: a
c = String -> Doc
text ("@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " =") Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
c
tag :: String
tag = case IsValue
isV of Value{} -> "V"; Unevaled -> "E"
instance Pretty (AM s) where
prettyPrec :: Int -> AM s -> Doc
prettyPrec p :: Int
p (Eval cl :: Closure s
cl ctrl :: 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 p :: Int
p (Match f :: QName
f cc :: FastCompiledClauses
cc sp :: Spine s
sp stack :: MatchStack s
stack ctrl :: ControlStack s
ctrl) =
Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ "M" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
sp
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> FastCompiledClauses -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec 10 FastCompiledClauses
cc
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ MatchStack s -> Doc
forall a. Pretty a => a -> Doc
pretty MatchStack s
stack
, Int -> Doc -> Doc
nest 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{} = "CatchAll"
instance Pretty (MatchStack s) where
pretty :: MatchStack s -> Doc
pretty ([] :> _) = Doc
forall a. Null a => a
empty
pretty (ca :: [CatchAllFrame s]
ca :> _) = [CatchAllFrame s] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [CatchAllFrame s]
ca
instance Pretty (ControlFrame s) where
prettyPrec :: Int -> ControlFrame s -> Doc
prettyPrec p :: Int
p (CaseK f :: QName
f _ _ _ _ mc :: MatchStack s
mc) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ("CaseK" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty (QName -> Name
qnameName QName
f)) Doc -> Doc -> Doc
<?> MatchStack s -> Doc
forall a. Pretty a => a -> Doc
pretty MatchStack s
mc
prettyPrec p :: Int
p (ForceK _ spine0 :: Spine s
spine0 spine1 :: Spine s
spine1) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "ForceK" Doc -> Doc -> Doc
<?> Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList (Spine s
spine0 Spine s -> Spine s -> Spine s
forall a. Semigroup a => a -> a -> a
<> Spine s
spine1)
prettyPrec p :: Int
p (EraseK _ sp0 :: Spine s
sp0 sp1 :: Spine s
sp1 sp2 :: Spine s
sp2 sp3 :: Spine s
sp3) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ "EraseK"
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
sp0
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
sp1
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
sp2
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
sp3 ]
prettyPrec _ (NatSucK n :: Integer
n) = String -> Doc
text ("+" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n)
prettyPrec p :: Int
p (PrimOpK f :: QName
f _ vs :: [Literal]
vs cls :: [Pointer s]
cls _) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ "PrimOpK" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Literal] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Literal]
vs
, Int -> Doc -> Doc
nest 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 p :: Int
p (UpdateThunk ps :: [STPointer s]
ps) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "UpdateThunk" Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
forall a. Show a => a -> String
show ([STPointer s] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [STPointer s]
ps))
prettyPrec p :: Int
p (ApplyK spine :: Spine s
spine) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "ApplyK" Doc -> Doc -> Doc
<?> Spine s -> Doc
forall a. Pretty a => [a] -> Doc
prettyList Spine s
spine
prettyPrec p :: Int
p NormaliseK = "NormaliseK"
prettyPrec p :: Int
p (ArgK cl :: Closure s
cl _) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ "ArgK" Doc -> Doc -> Doc
<+> Int -> Closure s -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec 10 Closure s
cl ]