{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Reduce.Fast
( fastReduce, fastNormalise ) where
import Control.Arrow (first, second)
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.ST
import Control.Monad.ST.Unsafe (unsafeSTToIO, unsafeInterleaveST)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Traversable (traverse)
import Data.Coerce
import Data.Semigroup ((<>))
import System.IO.Unsafe (unsafePerformIO)
import Data.IORef
import Data.STRef
import Data.Char
import Debug.Trace (trace)
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad hiding (Closure(..))
import Agda.TypeChecking.Reduce as R
import Agda.TypeChecking.Rewriting (rewrite)
import Agda.TypeChecking.Reduce.Monad as RedM
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad.Builtin hiding (constructorForm)
import Agda.TypeChecking.CompiledClause.Match ()
import Agda.TypeChecking.Free.Precompute
import Agda.Interaction.Options
import Agda.Utils.Float
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Memo
import Agda.Utils.Null (empty)
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Size
import Agda.Utils.Zipper
#include "undefined.h"
import Agda.Utils.Impossible
import Debug.Trace
data CompactDef =
CompactDef { cdefDelayed :: Bool
, cdefNonterminating :: Bool
, cdefUnconfirmed :: Bool
, cdefDef :: CompactDefn
, cdefRewriteRules :: RewriteRules
}
data CompactDefn
= CFun { cfunCompiled :: FastCompiledClauses, cfunProjection :: Maybe QName }
| CCon { cconSrcCon :: ConHead, cconArity :: Int }
| CForce
| CTrustMe
| CTyCon
| CAxiom
| CPrimOp Int ([Literal] -> Term) (Maybe FastCompiledClauses)
| COther
data BuiltinEnv = BuiltinEnv
{ bZero, bSuc, bTrue, bFalse, bRefl :: Maybe ConHead
, bPrimForce, bPrimTrustMe :: Maybe QName }
compactDef :: BuiltinEnv -> Definition -> RewriteRules -> ReduceM CompactDef
compactDef bEnv def rewr = do
cdefn <-
case theDef def of
_ | Just (defName def) == bPrimForce bEnv -> pure CForce
_ | Just (defName def) == bPrimTrustMe bEnv ->
case telView' (defType def) of
TelV tel _ | size tel == 4 -> pure CTrustMe
| otherwise -> pure COther
Constructor{conSrcCon = c, conArity = n} -> pure CCon{cconSrcCon = c, cconArity = n}
Function{funCompiled = Just cc, funClauses = _:_, funProjection = proj} ->
pure CFun{ cfunCompiled = fastCompiledClauses bEnv cc
, cfunProjection = projOrig <$> proj }
Function{funClauses = []} -> pure CAxiom
Function{} -> pure COther
Datatype{dataClause = Nothing} -> pure CTyCon
Record{recClause = Nothing} -> pure CTyCon
Datatype{} -> pure COther
Record{} -> pure COther
Axiom{} -> pure CAxiom
AbstractDefn{} -> pure CAxiom
Primitive{ primName = name, primCompiled = cc } ->
case name of
"primNatPlus" -> mkPrim 2 $ natOp (+)
"primNatMinus" -> mkPrim 2 $ natOp (\ x y -> max 0 (x - y))
"primNatTimes" -> mkPrim 2 $ natOp (*)
"primNatDivSucAux" -> mkPrim 4 $ natOp4 divAux
"primNatModSucAux" -> mkPrim 4 $ natOp4 modAux
"primNatLess" -> mkPrim 2 $ natRel (<)
"primNatEquality" -> mkPrim 2 $ natRel (==)
"primWord64ToNat" -> mkPrim 1 $ \ [LitWord64 _ a] -> nat (fromIntegral a)
"primWord64FromNat" -> mkPrim 1 $ \ [LitNat _ a] -> word (fromIntegral a)
"primNatToFloat" -> mkPrim 1 $ \ [LitNat _ a] -> float (fromIntegral a)
"primFloatPlus" -> mkPrim 2 $ floatOp (+)
"primFloatMinus" -> mkPrim 2 $ floatOp (-)
"primFloatTimes" -> mkPrim 2 $ floatOp (*)
"primFloatNegate" -> mkPrim 1 $ floatFun negate
"primFloatDiv" -> mkPrim 2 $ floatOp (/)
"primFloatEquality" -> mkPrim 2 $ floatRel floatEq
"primFloatLess" -> mkPrim 2 $ floatRel floatLt
"primFloatNumericalEquality" -> mkPrim 2 $ floatRel (==)
"primFloatNumericalLess" -> mkPrim 2 $ floatRel (<)
"primFloatSqrt" -> mkPrim 1 $ floatFun sqrt
"primExp" -> mkPrim 1 $ floatFun exp
"primLog" -> mkPrim 1 $ floatFun log
"primSin" -> mkPrim 1 $ floatFun sin
"primCos" -> mkPrim 1 $ floatFun cos
"primTan" -> mkPrim 1 $ floatFun tan
"primASin" -> mkPrim 1 $ floatFun asin
"primACos" -> mkPrim 1 $ floatFun acos
"primATan" -> mkPrim 1 $ floatFun atan
"primATan2" -> mkPrim 2 $ floatOp atan2
"primShowFloat" -> mkPrim 1 $ \ [LitFloat _ a] -> string (show a)
"primCharEquality" -> mkPrim 2 $ charRel (==)
"primIsLower" -> mkPrim 1 $ charPred isLower
"primIsDigit" -> mkPrim 1 $ charPred isDigit
"primIsAlpha" -> mkPrim 1 $ charPred isAlpha
"primIsSpace" -> mkPrim 1 $ charPred isSpace
"primIsAscii" -> mkPrim 1 $ charPred isAscii
"primIsLatin1" -> mkPrim 1 $ charPred isLatin1
"primIsPrint" -> mkPrim 1 $ charPred isPrint
"primIsHexDigit" -> mkPrim 1 $ charPred isHexDigit
"primToUpper" -> mkPrim 1 $ charFun toUpper
"primToLower" -> mkPrim 1 $ charFun toLower
"primCharToNat" -> mkPrim 1 $ \ [LitChar _ a] -> nat (fromIntegral (fromEnum a))
"primNatToChar" -> mkPrim 1 $ \ [LitNat _ a] -> char (toEnum $ fromIntegral $ a `mod` 0x110000)
"primShowChar" -> mkPrim 1 $ \ a -> string (show $ pretty a)
"primStringAppend" -> mkPrim 2 $ \ [LitString _ a, LitString _ b] -> string (b ++ a)
"primStringEquality" -> mkPrim 2 $ \ [LitString _ a, LitString _ b] -> bool (b == a)
"primShowString" -> mkPrim 1 $ \ a -> string (show $ pretty a)
"primQNameEquality" -> mkPrim 2 $ \ [LitQName _ a, LitQName _ b] -> bool (b == a)
"primQNameLess" -> mkPrim 2 $ \ [LitQName _ a, LitQName _ b] -> bool (b < a)
"primShowQName" -> mkPrim 1 $ \ [LitQName _ a] -> string (show a)
"primMetaEquality" -> mkPrim 2 $ \ [LitMeta _ _ a, LitMeta _ _ b] -> bool (b == a)
"primMetaLess" -> mkPrim 2 $ \ [LitMeta _ _ a, LitMeta _ _ b] -> bool (b < a)
"primShowMeta" -> mkPrim 1 $ \ [LitMeta _ _ a] -> string (show (pretty a))
_ -> pure COther
where
fcc = fastCompiledClauses bEnv <$> cc
mkPrim n op = pure $ CPrimOp n op fcc
divAux k m n j = k + div (max 0 $ n + m - j) (m + 1)
modAux k m n j | n > j = mod (n - j - 1) (m + 1)
| otherwise = k + n
~(Just true) = bTrue bEnv <&> \ c -> Con c ConOSystem []
~(Just false) = bFalse bEnv <&> \ c -> Con c ConOSystem []
bool a = if a then true else false
nat a = Lit . LitNat noRange $! a
word a = Lit . LitWord64 noRange $! a
float a = Lit . LitFloat noRange $! a
string a = Lit . LitString noRange $! a
char a = Lit . LitChar noRange $! a
natOp f [LitNat _ a, LitNat _ b] = nat (f b a)
natOp _ _ = __IMPOSSIBLE__
natOp4 f [LitNat _ a, LitNat _ b, LitNat _ c, LitNat _ d] = nat (f d c b a)
natOp4 _ _ = __IMPOSSIBLE__
natRel f [LitNat _ a, LitNat _ b] = bool (f b a)
natRel _ _ = __IMPOSSIBLE__
floatFun f [LitFloat _ a] = float (f a)
floatFun _ _ = __IMPOSSIBLE__
floatOp f [LitFloat _ a, LitFloat _ b] = float (f b a)
floatOp _ _ = __IMPOSSIBLE__
floatRel f [LitFloat _ a, LitFloat _ b] = bool (f b a)
floatRel _ _ = __IMPOSSIBLE__
charFun f [LitChar _ a] = char (f a)
charFun _ _ = __IMPOSSIBLE__
charPred f [LitChar _ a] = bool (f a)
charPred _ _ = __IMPOSSIBLE__
charRel f [LitChar _ a, LitChar _ b] = bool (f b a)
charRel _ _ = __IMPOSSIBLE__
return $
CompactDef { cdefDelayed = defDelayed def == Delayed
, cdefNonterminating = defNonterminating def
, cdefUnconfirmed = defTerminationUnconfirmed def
, cdefDef = cdefn
, cdefRewriteRules = rewr
}
data FastCase c = FBranches
{ fprojPatterns :: Bool
, fconBranches :: Map NameId c
, fsucBranch :: Maybe c
, flitBranches :: Map Literal c
, fcatchAllBranch :: Maybe c
}
noBranches :: FastCase a
noBranches = FBranches{ fprojPatterns = False
, fconBranches = Map.empty
, fsucBranch = Nothing
, flitBranches = Map.empty
, fcatchAllBranch = Nothing }
data FastCompiledClauses
= FCase Int (FastCase FastCompiledClauses)
| FEta Int [QName] FastCompiledClauses (Maybe FastCompiledClauses)
| FDone [Arg ArgName] Term
| FFail
fastCompiledClauses :: BuiltinEnv -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses bEnv cc =
case cc of
Fail -> FFail
Done xs b -> FDone xs b
Case (Arg _ n) Branches{ etaBranch = Just (c, cc), catchAllBranch = ca } ->
FEta n (conFields c) (fastCompiledClauses bEnv $ content cc) (fastCompiledClauses bEnv <$> ca)
Case (Arg _ n) bs -> FCase n (fastCase bEnv bs)
fastCase :: BuiltinEnv -> Case CompiledClauses -> FastCase FastCompiledClauses
fastCase env (Branches proj con _ lit wild _) =
FBranches
{ fprojPatterns = proj
, fconBranches = Map.mapKeysMonotonic (nameId . qnameName) $ fmap (fastCompiledClauses env . content) (stripSuc con)
, fsucBranch = fmap (fastCompiledClauses env . content) $ flip Map.lookup con . conName =<< bSuc env
, flitBranches = fmap (fastCompiledClauses env) lit
, fcatchAllBranch = fmap (fastCompiledClauses env) wild }
where
stripSuc | Just c <- bSuc env = Map.delete (conName c)
| otherwise = id
{-# INLINE lookupCon #-}
lookupCon :: QName -> FastCase c -> Maybe c
lookupCon c (FBranches _ cons _ _ _) = Map.lookup (nameId $ qnameName c) cons
{-# NOINLINE memoQName #-}
memoQName :: (QName -> a) -> (QName -> a)
memoQName f = unsafePerformIO $ do
tbl <- newIORef Map.empty
return (unsafePerformIO . f' tbl)
where
f' tbl x = do
let i = nameId (qnameName x)
m <- readIORef tbl
case Map.lookup i m of
Just y -> return y
Nothing -> do
let y = f x
writeIORef tbl (Map.insert i y m)
return y
data Normalisation = WHNF | NF
deriving (Eq)
data ReductionFlags = ReductionFlags
{ allowNonTerminating :: Bool
, allowUnconfirmed :: Bool
, hasRewriting :: Bool }
fastReduce :: Term -> ReduceM (Blocked Term)
fastReduce = fastReduce' WHNF
fastNormalise :: Term -> ReduceM Term
fastNormalise v = ignoreBlocking <$> fastReduce' NF v
fastReduce' :: Normalisation -> Term -> ReduceM (Blocked Term)
fastReduce' norm v = do
let name (Con c _ _) = c
name _ = __IMPOSSIBLE__
zero <- fmap name <$> getBuiltin' builtinZero
suc <- fmap name <$> getBuiltin' builtinSuc
true <- fmap name <$> getBuiltin' builtinTrue
false <- fmap name <$> getBuiltin' builtinFalse
refl <- fmap name <$> getBuiltin' builtinRefl
force <- fmap primFunName <$> getPrimitive' "primForce"
trustme <- fmap primFunName <$> getPrimitive' "primTrustMe"
let bEnv = BuiltinEnv { bZero = zero, bSuc = suc, bTrue = true, bFalse = false, bRefl = refl,
bPrimForce = force, bPrimTrustMe = trustme }
allowedReductions <- asks envAllowedReductions
rwr <- optRewriting <$> pragmaOptions
constInfo <- unKleisli $ \f -> do
info <- getConstInfo f
rewr <- if rwr then instantiateRewriteRules =<< getRewriteRulesFor f
else return []
compactDef bEnv info rewr
let flags = ReductionFlags{ allowNonTerminating = elem NonTerminatingReductions allowedReductions
, allowUnconfirmed = elem UnconfirmedReductions allowedReductions
, hasRewriting = rwr }
ReduceM $ \ redEnv -> reduceTm redEnv bEnv (memoQName constInfo) norm flags v
unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli f = ReduceM $ \ env x -> unReduceM (f x) 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 isV _ _ _) = isV
setIsValue :: IsValue -> Closure s -> Closure s
setIsValue isV (Closure _ t env spine) = Closure isV t env spine
clApply :: Closure s -> Spine s -> Closure s
clApply c [] = c
clApply (Closure _ t env es) es' = Closure Unevaled t env (es <> es')
clApply_ :: Closure s -> Spine s -> Closure s
clApply_ c [] = c
clApply_ (Closure b t env es) es' = Closure b t env (es <> 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 (Functor)
derefPointer :: Pointer s -> ST s (Thunk (Closure s))
derefPointer (Pure x) = return (Thunk x)
derefPointer (Pointer ptr) = readSTRef ptr
derefPointer_ :: Pointer s -> ST s (Closure s)
derefPointer_ ptr = do
Thunk cl <- derefPointer ptr
return cl
unsafeDerefPointer :: Pointer s -> Thunk (Closure s)
unsafeDerefPointer (Pure x) = Thunk x
unsafeDerefPointer (Pointer p) = unsafePerformIO (unsafeSTToIO (readSTRef p))
readPointer :: STPointer s -> ST s (Thunk (Closure s))
readPointer = readSTRef
storePointer :: STPointer s -> Closure s -> ST s ()
storePointer ptr !cl = writeSTRef ptr (Thunk cl)
blackHole :: STPointer s -> ST s ()
blackHole ptr = writeSTRef ptr BlackHole
createThunk :: Closure s -> ST s (Pointer s)
createThunk (Closure _ (Var x []) env spine)
| null spine, Just p <- lookupEnv x env = return p
createThunk cl = Pointer <$> newSTRef (Thunk cl)
pureThunk :: Closure s -> Pointer s
pureThunk = Pure
newtype Env s = Env [Pointer s]
emptyEnv :: Env s
emptyEnv = Env []
isEmptyEnv :: Env s -> Bool
isEmptyEnv (Env xs) = null xs
envSize :: Env s -> Int
envSize (Env xs) = length xs
envToList :: Env s -> [Pointer s]
envToList (Env xs) = xs
extendEnv :: Pointer s -> Env s -> Env s
extendEnv p (Env xs) = Env (p : xs)
lookupEnv_ :: Int -> Env s -> Pointer s
lookupEnv_ i (Env e) = e !! i
lookupEnv :: Int -> Env s -> Maybe (Pointer s)
lookupEnv i e | i < n = Just (lookupEnv_ i e)
| otherwise = Nothing
where n = envSize 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
c >: cs :> cl = c : cs :> cl
data CatchAllFrame s = CatchAll FastCompiledClauses (Spine s)
data ElimZipper a = ApplyCxt ArgInfo
deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
instance Zipper (ElimZipper a) where
type Carrier (ElimZipper a) = Elim' a
type Element (ElimZipper a) = a
firstHole (Apply arg) = Just (unArg arg, ApplyCxt (argInfo arg))
firstHole Proj{} = Nothing
plugHole x (ApplyCxt i) = Apply (Arg i x)
nextHole x c = Left (plugHole x 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)
| TrustMeK QName (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 nf t = Eval (Closure Unevaled t emptyEnv []) [NormaliseK | nf == NF]
topMetaIsNotBlocked :: Blocked Term -> Blocked Term
topMetaIsNotBlocked (Blocked _ t@MetaV{}) = notBlocked t
topMetaIsNotBlocked b = b
decodePointer :: Pointer s -> ST s Term
decodePointer p = decodeClosure_ =<< derefPointer_ p
decodeSpine :: Spine s -> ST s Elims
decodeSpine spine = unsafeInterleaveST $ (traverse . traverse) decodePointer spine
decodeEnv :: Env s -> ST s [Term]
decodeEnv env = unsafeInterleaveST $ traverse decodePointer (envToList env)
decodeClosure_ :: Closure s -> ST s Term
decodeClosure_ = ignoreBlocking <.> decodeClosure
decodeClosure :: Closure s -> ST s (Blocked Term)
decodeClosure (Closure isV t env spine) = do
vs <- decodeEnv env
es <- decodeSpine spine
return $ topMetaIsNotBlocked (applyE (applySubst (parS vs) t) es <$ b)
where
parS = foldr (:#) IdS
b = case isV of
Value b -> b
Unevaled -> notBlocked ()
elimsToSpine :: Env s -> Elims -> ST s (Spine s)
elimsToSpine env es = do
spine <- mapM thunk es
forceSpine spine `seq` return spine
where
forceSpine = foldl (\ () -> forceEl) ()
forceEl (Apply (Arg _ (Pure Closure{}))) = ()
forceEl (Apply (Arg _ (Pointer{}))) = ()
forceEl _ = ()
unknownFVs = setFreeVariables unknownFreeVariables
thunk (Apply (Arg i t)) = Apply . Arg (unknownFVs i) <$> createThunk (closure (getFreeVariables i) t)
thunk (Proj o f) = return (Proj o f)
closure _ t@Lit{} = Closure (Value $ notBlocked ()) t emptyEnv []
closure fv t = env' `seq` Closure Unevaled t env' []
where env' = trimEnvironment fv env
trimEnvironment :: FreeVariables -> Env s -> Env s
trimEnvironment UnknownFVs env = env
trimEnvironment (KnownFVs fvs) env
| IntSet.null fvs = emptyEnv
| otherwise = env
where
trim _ [] = []
trim i (p : ps)
| IntSet.member i fvs = (p :) $! trim (i + 1) ps
| otherwise = (unusedPointer :) $! trim (i + 1) ps
buildEnv :: [Arg String] -> Spine s -> ([Arg String], Env s, Spine s)
buildEnv xs spine = go xs spine emptyEnv
where
go [] sp env = ([], env, sp)
go xs0@(x : xs) sp env =
case sp of
[] -> (xs0, env, sp)
Apply c : sp -> go xs sp (unArg c `extendEnv` env)
_ -> __IMPOSSIBLE__
unusedPointerString :: String
unusedPointerString = show (Impossible __FILE__ __LINE__)
unusedPointer :: Pointer s
unusedPointer = Pure (Closure (Value $ notBlocked ())
(Lit (LitString noRange unusedPointerString)) emptyEnv [])
reduceTm :: ReduceEnv -> BuiltinEnv -> (QName -> CompactDef) -> Normalisation -> ReductionFlags -> Term -> Blocked Term
reduceTm rEnv bEnv !constInfo normalisation ReductionFlags{..} =
compileAndRun . traceDoc (text "-- fast reduce --")
where
metaStore = redSt rEnv ^. stMetaStore
getMeta m = maybe __IMPOSSIBLE__ mvInstantiation (Map.lookup m metaStore)
partialDefs = runReduce getPartialDefs
rewriteRules f = cdefRewriteRules (constInfo f)
callByNeed = envCallByNeed (redEnv rEnv)
runReduce :: ReduceM a -> a
runReduce m = unReduceM m rEnv
hasVerb tag lvl = unReduceM (hasVerbosity tag lvl) rEnv
doDebug = hasVerb "tc.reduce.fast" 110
traceDoc :: Doc -> a -> a
traceDoc
| doDebug = trace . show
| otherwise = const id
BuiltinEnv{ bZero = zero, bSuc = suc, bRefl = refl0 } = bEnv
conNameId = nameId . qnameName . conName
isZero = case zero of
Nothing -> const False
Just z -> (conNameId z ==) . conNameId
isSuc = case suc of
Nothing -> const False
Just s -> (conNameId s ==) . conNameId
refl = refl0 >>= \ c -> if cconArity (cdefDef $ constInfo $ conName c) == 0
then Just c else Nothing
compileAndRun :: Term -> Blocked Term
compileAndRun t = runST (runAM (compile normalisation t))
runAM :: AM s -> ST s (Blocked Term)
runAM = if doDebug then \ s -> trace (prettyShow s) (runAM' s)
else runAM'
runAM' :: AM s -> ST s (Blocked Term)
runAM' (Eval cl@(Closure Value{} _ _ _) []) = decodeClosure cl
runAM' s@(Eval cl@(Closure Unevaled t env spine) !ctrl) = {-# SCC "runAM.Eval" #-}
case t of
Def f [] ->
let CompactDef{ cdefDelayed = delayed
, cdefNonterminating = nonterm
, cdefUnconfirmed = unconf
, cdefDef = def } = constInfo f
dontUnfold = (nonterm && not allowNonTerminating) ||
(unconf && not allowUnconfirmed) ||
(delayed && not (unfoldDelayed ctrl))
in case def of
CFun{ cfunCompiled = cc }
| dontUnfold -> rewriteAM done
| otherwise -> runAM (Match f cc spine ([] :> cl) ctrl)
CAxiom -> rewriteAM done
CTyCon -> rewriteAM done
CCon{} -> runAM done
CForce | (spine0, Apply v : spine1) <- splitAt 4 spine ->
evalPointerAM (unArg v) [] (ForceK f spine0 spine1 : ctrl)
CForce -> runAM done
CTrustMe | (spine0, Apply v : spine1) <- splitAt 2 spine ->
evalPointerAM (unArg v) [] (TrustMeK f spine0 [] spine1 : ctrl)
CTrustMe -> runAM done
CPrimOp n op cc | length spine == n,
Just (v : vs) <- allApplyElims spine ->
evalPointerAM (unArg v) [] (PrimOpK f op [] (map unArg vs) cc : ctrl)
CPrimOp{} -> runAM done
COther -> fallbackAM s
Con c i [] | isZero c ->
runAM (evalTrueValue (Lit (LitNat noRange 0)) emptyEnv spine ctrl)
Con c i [] | isSuc c, Apply v : _ <- spine ->
evalPointerAM (unArg v) [] (sucCtrl ctrl)
Con c i [] ->
case splitAt ar spine of
(args, Proj _ p : spine') -> evalPointerAM (unArg arg) spine' ctrl
where
fields = conFields c
Just n = List.elemIndex p fields
Apply arg = args !! n
_ -> rewriteAM (evalTrueValue (Con c' i []) env spine ctrl)
where CCon{cconSrcCon = c', cconArity = ar} = cdefDef (constInfo (conName c))
Var x [] ->
case lookupEnv x env of
Nothing -> runAM (evalValue (notBlocked ()) (Var (x - envSize env) []) emptyEnv spine ctrl)
Just p -> evalPointerAM p spine ctrl
Lam h b ->
case spine of
Apply v : spine' ->
case b of
Abs _ b -> runAM (evalClosure b (unArg v `extendEnv` env) spine' ctrl)
NoAbs _ b -> runAM (evalClosure b env spine' ctrl)
[] -> runAM done
_ -> __IMPOSSIBLE__
Lit{} -> runAM (evalTrueValue t emptyEnv [] ctrl)
Pi{} -> runAM done
Def f es -> shiftElims (Def f []) emptyEnv env es
Con c i es -> shiftElims (Con c i []) emptyEnv env es
Var x es -> shiftElims (Var x []) env env es
MetaV m es ->
case getMeta m of
InstV xs t -> do
spine' <- elimsToSpine env es
let (zs, env, !spine'') = buildEnv xs (spine' <> spine)
runAM (evalClosure (lams zs t) env spine'' ctrl)
_ -> runAM (Eval (mkValue (blocked m ()) cl) ctrl)
Level{} -> fallbackAM s
Sort{} -> fallbackAM s
DontCare{} -> fallbackAM s
where done = Eval (mkValue (notBlocked ()) cl) ctrl
shiftElims t env0 env es = do
spine' <- elimsToSpine env es
runAM (evalClosure t env0 (spine' <> spine) ctrl)
runAM' s@(Eval cl@(Closure b t env spine) (NormaliseK : ctrl)) =
case t of
Def _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl
Con _ _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl
Var _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl
MetaV _ [] -> normaliseArgsAM (Closure b t emptyEnv []) spine ctrl
Lit{} -> runAM done
Def f es -> shiftElims (Def f []) emptyEnv env es
Con c i es -> shiftElims (Con c i []) emptyEnv env es
Var x es -> shiftElims (Var x []) env env es
MetaV m es -> shiftElims (MetaV m []) emptyEnv env es
_ -> fallbackAM s
where done = Eval (mkValue (notBlocked ()) cl) ctrl
shiftElims t env0 env es = do
spine' <- elimsToSpine env es
runAM (Eval (Closure b t env0 (spine' <> spine)) (NormaliseK : ctrl))
runAM' (Eval cl (ArgK cl0 cxt : ctrl)) =
case nextHole (pureThunk cl) cxt of
Left spine -> runAM (Eval (clApply_ cl0 spine) ctrl)
Right (p, cxt') -> evalPointerAM p [] (NormaliseK : ArgK cl0 cxt' : ctrl)
runAM' (Eval cl@(Closure Value{} (Lit (LitNat r n)) _ _) (NatSucK m : ctrl)) =
runAM (evalTrueValue (Lit $! LitNat r $! m + n) emptyEnv [] ctrl)
runAM' (Eval cl (NatSucK m : ctrl)) =
runAM (Eval (mkValue (notBlocked ()) $ plus m cl) ctrl)
where
plus 0 cl = cl
plus n cl =
trueValue (Con (fromMaybe __IMPOSSIBLE__ suc) ConOSystem []) emptyEnv $
Apply (defaultArg arg) : []
where arg = pureThunk (plus (n - 1) cl)
runAM' (Eval (Closure _ (Lit a) _ _) (PrimOpK f op vs es cc : ctrl)) =
case es of
[] -> runAM (evalTrueValue (op (a : vs)) emptyEnv [] ctrl)
e : es' -> evalPointerAM e [] (PrimOpK f op (a : vs) es' cc : ctrl)
runAM' (Eval cl@(Closure (Value blk) _ _ _) (PrimOpK f _ vs es mcc : ctrl)) =
case mcc of
Nothing -> rewriteAM (Eval stuck ctrl)
Just cc -> runAM (Match f cc spine ([] :> notstuck) ctrl)
where
p = pureThunk cl
lits = map (pureThunk . litClos) (reverse vs)
spine = fmap (Apply . defaultArg) $ lits <> [p] <> es
stuck = Closure (Value blk) (Def f []) emptyEnv spine
notstuck = Closure Unevaled (Def f []) emptyEnv spine
litClos l = trueValue (Lit l) emptyEnv []
runAM' (Eval arg@(Closure (Value blk) t _ _) (ForceK pf spine0 spine1 : ctrl))
| isCanonical t =
case spine1 of
Apply k : spine' ->
evalPointerAM (unArg k) (elim : spine') ctrl
[] ->
runAM (evalTrueValue (lam (defaultArg "k") $ Var 0 [Apply $ defaultArg $ Var 1 []])
(argPtr `extendEnv` emptyEnv) [] ctrl)
_ -> __IMPOSSIBLE__
| otherwise = rewriteAM (Eval stuck ctrl)
where
argPtr = pureThunk arg
elim = Apply (defaultArg argPtr)
spine' = spine0 <> [elim] <> spine1
stuck = Closure (Value blk) (Def pf []) emptyEnv spine'
isCanonical u = case u of
Lit{} -> True
Con{} -> True
Lam{} -> True
Pi{} -> True
Sort{} -> True
Level{} -> True
DontCare{} -> True
MetaV{} -> False
Var{} -> False
Def q _
| CTyCon <- cdefDef (constInfo q) -> True
| otherwise -> False
runAM' (Eval cl2@(Closure Value{} arg2 _ _) (TrustMeK f spine0 [Apply p1] _ : ctrl)) = do
cl1@(Closure _ arg1 _ sp1) <- derefPointer_ (unArg p1)
case (arg1, arg2) of
(Lit l1, Lit l2) | l1 == l2, isJust refl ->
runAM (evalTrueValue (Con (fromJust refl) ConOSystem []) emptyEnv [] ctrl)
_ ->
fallbackAM (evalClosure (Def f []) emptyEnv (spine0 ++ map (Apply . hide . defaultArg . pureThunk) [cl1, cl2]) ctrl)
runAM' (Eval cl1@(Closure Value{} _ _ _) (TrustMeK f spine0 [] [Apply p2] : ctrl)) =
evalPointerAM (unArg p2) [] (TrustMeK f spine0 [Apply $ hide $ defaultArg $ pureThunk cl1] [] : ctrl)
runAM' (Eval _ (TrustMeK{} : _)) =
__IMPOSSIBLE__
runAM' (Eval cl@(Closure Value{} _ _ _) (UpdateThunk ps : ctrl)) =
mapM_ (`storePointer` cl) ps >> runAM (Eval cl ctrl)
runAM' (Eval cl@(Closure Value{} _ _ _) (ApplyK spine : ctrl)) =
runAM (Eval (clApply cl spine) ctrl)
runAM' (Eval cl@(Closure (Value blk) t env spine) ctrl0@(CaseK f i bs spine0 spine1 stack : ctrl)) =
{-# SCC "runAM.CaseK" #-}
case blk of
Blocked{} -> stuck
NotBlocked{} -> case t of
Con c ci [] | isSuc c -> matchSuc $ matchCatchall $ failedMatch f stack ctrl
Con c ci [] -> matchCon c ci (length spine) $ matchCatchall $ failedMatch f stack ctrl
Con c ci es -> do
spine' <- elimsToSpine env es
runAM (evalValue blk (Con c ci []) emptyEnv (spine' <> spine) ctrl0)
Lit (LitNat _ 0) -> matchLitZero $ matchCatchall $ failedMatch f stack ctrl
Lit (LitNat _ n) -> matchLitSuc n $ matchCatchall $ failedMatch f stack ctrl
Lit l -> matchLit l $ matchCatchall $ failedMatch f stack ctrl
_ -> stuck
where
stuck = do
blk' <- case blk of
Blocked{} -> return blk
NotBlocked r _ -> decodeClosure_ cl <&> \ v -> NotBlocked (stuckOn (Apply $ Arg i v) r) ()
stuckMatch blk' stack ctrl
catchallSpine = spine0 <> [Apply $ Arg i p] <> spine1
where p = pureThunk cl
catchallStack = case fcatchAllBranch bs of
Nothing -> stack
Just cc -> CatchAll cc catchallSpine >: stack
(m `ifJust` f) z = maybe z f m
matchCon c ci ar = lookupCon (conName c) bs `ifJust` \ cc ->
runAM (Match f cc (spine0 <> spine <> spine1) catchallStack ctrl)
matchCatchall = fcatchAllBranch bs `ifJust` \ cc ->
runAM (Match f cc catchallSpine stack ctrl)
matchLit l = Map.lookup l (flitBranches bs) `ifJust` \ cc ->
runAM (Match f cc (spine0 <> spine1) catchallStack ctrl)
matchSuc = fsucBranch bs `ifJust` \ cc ->
runAM (Match f cc (spine0 <> spine <> spine1) catchallStack ctrl)
matchLitSuc n = fsucBranch bs `ifJust` \ cc ->
runAM (Match f cc (spine0 <> [Apply $ defaultArg arg] <> spine1) catchallStack ctrl)
where n' = n - 1
arg = pureThunk $ trueValue (Lit $ LitNat noRange n') emptyEnv []
matchLitZero = matchCon (fromMaybe __IMPOSSIBLE__ zero) ConOSystem 0
runAM' (Match f cc spine stack ctrl) = {-# SCC "runAM.Match" #-}
case cc of
FFail -> stuckMatch (NotBlocked AbsurdMatch ()) stack ctrl
FDone xs body -> do
let (zs, env, !spine') = buildEnv xs spine
runAM (Eval (Closure Unevaled (lams zs body) env spine') ctrl)
FEta n fs cc ca ->
case splitAt n spine of
(_, []) -> done Underapplied
(spine0, Apply e : spine1) -> do
let projClosure f = Closure Unevaled (Var 0 []) (extendEnv (unArg e) emptyEnv) [Proj ProjSystem f]
projs <- mapM (createThunk . projClosure) fs
let spine' = spine0 <> map (Apply . defaultArg) projs <> spine1
stack' = caseMaybe ca stack $ \ cc -> CatchAll cc spine >: stack
runAM (Match f cc spine' stack' ctrl)
_ -> __IMPOSSIBLE__
FCase n bs ->
case splitAt n spine of
(_, []) -> done Underapplied
(spine0, Apply e : spine1) ->
evalPointerAM (unArg e) [] $ CaseK f (argInfo e) bs spine0 spine1 stack : ctrl
(spine0, Proj o p : spine1) ->
case lookupCon p bs <|> ((`lookupCon` bs) =<< op) of
Nothing
| elem f partialDefs -> stuckMatch (NotBlocked MissingClauses ()) stack ctrl
| otherwise -> __IMPOSSIBLE__
Just cc -> runAM (Match f cc (spine0 <> spine1) stack ctrl)
where CFun{ cfunProjection = op } = cdefDef (constInfo p)
where done why = stuckMatch (NotBlocked why ()) stack ctrl
evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
evalPointerAM (Pure cl) spine ctrl = runAM (Eval (clApply cl spine) ctrl)
evalPointerAM (Pointer p) spine ctrl = readPointer p >>= \ case
BlackHole -> __IMPOSSIBLE__
Thunk cl@(Closure Unevaled _ _ _) | callByNeed -> do
blackHole p
runAM (Eval cl $ updateThunkCtrl p $ [ApplyK spine | not (null spine)] ++ ctrl)
Thunk cl -> runAM (Eval (clApply cl spine) ctrl)
normaliseArgsAM :: Closure s -> Spine s -> ControlStack s -> ST s (Blocked Term)
normaliseArgsAM cl [] ctrl = runAM (Eval cl ctrl)
normaliseArgsAM cl spine ctrl =
case firstHole spine of
Nothing -> runAM (Eval (clApply_ cl spine) ctrl)
Just (p, cxt) -> evalPointerAM p [] (NormaliseK : ArgK cl cxt : ctrl)
fallbackAM :: AM s -> ST s (Blocked Term)
fallbackAM (Eval c ctrl) = do
v <- decodeClosure_ c
runAM (mkValue $ runReduce $ slow v)
where mkValue b = evalValue (() <$ b) (ignoreBlocking b) emptyEnv [] ctrl'
(slow, ctrl') = case ctrl of
NormaliseK : ctrl'
| Value{} <- isValue c -> (notBlocked <.> slowNormaliseArgs, ctrl')
_ -> (slowReduceTerm, ctrl)
fallbackAM _ = __IMPOSSIBLE__
rewriteAM :: AM s -> ST s (Blocked Term)
rewriteAM = if hasRewriting then rewriteAM' else runAM
rewriteAM' :: AM s -> ST s (Blocked Term)
rewriteAM' s@(Eval (Closure (Value blk) t env spine) ctrl)
| null rewr = runAM s
| otherwise = traceDoc (text "R" <+> pretty s) $ do
v0 <- decodeClosure_ (Closure Unevaled t env [])
es <- decodeSpine spine
case runReduce (rewrite blk v0 rewr es) of
NoReduction b -> runAM (evalValue (() <$ b) (ignoreBlocking b) emptyEnv [] ctrl)
YesReduction _ v -> runAM (evalClosure v emptyEnv [] ctrl)
where rewr = case t of
Def f [] -> rewriteRules f
Con c _ [] -> rewriteRules (conName c)
_ -> __IMPOSSIBLE__
rewriteAM' _ =
__IMPOSSIBLE__
sucCtrl :: ControlStack s -> ControlStack s
sucCtrl (NatSucK !n : ctrl) = NatSucK (n + 1) : ctrl
sucCtrl ctrl = NatSucK 1 : ctrl
updateThunkCtrl :: STPointer s -> ControlStack s -> ControlStack s
updateThunkCtrl p (UpdateThunk ps : ctrl) = UpdateThunk (p : ps) : ctrl
updateThunkCtrl p ctrl = UpdateThunk [p] : ctrl
unfoldDelayed :: ControlStack s -> Bool
unfoldDelayed [] = False
unfoldDelayed (CaseK{} : _) = True
unfoldDelayed (PrimOpK{} : _) = False
unfoldDelayed (NatSucK{} : _) = False
unfoldDelayed (NormaliseK{} : _) = False
unfoldDelayed (ArgK{} : _) = False
unfoldDelayed (UpdateThunk{} : ctrl) = unfoldDelayed ctrl
unfoldDelayed (ApplyK{} : ctrl) = unfoldDelayed ctrl
unfoldDelayed (ForceK{} : ctrl) = unfoldDelayed ctrl
unfoldDelayed (TrustMeK{} : ctrl) = unfoldDelayed ctrl
stuckMatch :: Blocked_ -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
stuckMatch blk (_ :> cl) ctrl = rewriteAM (Eval (mkValue blk cl) ctrl)
failedMatch :: QName -> MatchStack s -> ControlStack s -> ST s (Blocked Term)
failedMatch f (CatchAll cc spine : stack :> cl) ctrl = runAM (Match f cc spine (stack :> cl) ctrl)
failedMatch f ([] :> cl) ctrl
| elem f partialDefs = rewriteAM (Eval (mkValue (NotBlocked MissingClauses ()) cl) ctrl)
| otherwise = runReduce $
traceSLn "impossible" 10 ("Incomplete pattern matching when applying " ++ show f)
__IMPOSSIBLE__
evalClosure t env spine = Eval (Closure Unevaled t env spine)
evalValue b t env spine = Eval (Closure (Value b) t env spine)
evalTrueValue = evalValue $ notBlocked ()
trueValue t env spine = Closure (Value $ notBlocked ()) t env spine
mkValue b = setIsValue (Value b)
lams :: [Arg String] -> Term -> Term
lams xs t = foldr lam t xs
lam :: Arg String -> Term -> Term
lam x t = Lam (argInfo x) (Abs (unArg x) t)
instance Pretty a => Pretty (FastCase a) where
prettyPrec p (FBranches _cop cs suc ls m) =
mparens (p > 0) $ vcat (prettyMap cs ++ prettyMap ls ++ prSuc suc ++ prC m)
where
prC Nothing = []
prC (Just x) = [text "_ ->" <?> pretty x]
prSuc Nothing = []
prSuc (Just x) = [text "suc ->" <?> pretty x]
instance Pretty NameId where
pretty = text . show
instance Pretty FastCompiledClauses where
pretty (FDone xs t) = (text "done" <+> prettyList xs) <?> prettyPrec 10 t
pretty FFail = text "fail"
pretty (FEta n _ cc ca) =
text ("eta " ++ show n ++ " of") <?>
vcat ([ text "{} ->" <?> pretty cc ] ++
[ text "_ ->" <?> pretty cc | Just cc <- [ca] ])
pretty (FCase n bs) | fprojPatterns bs =
sep [ text $ "project " ++ show n
, nest 2 $ pretty bs
]
pretty (FCase n bs) =
text ("case " ++ show n ++ " of") <?> pretty bs
instance Pretty a => Pretty (Thunk a) where
prettyPrec _ BlackHole = text "<BLACKHOLE>"
prettyPrec p (Thunk cl) = prettyPrec p cl
instance Pretty (Pointer s) where
prettyPrec p = prettyPrec p . unsafeDerefPointer
instance Pretty (Closure s) where
prettyPrec _ (Closure Value{} (Lit (LitString _ unused)) _ _)
| unused == unusedPointerString = text "_"
prettyPrec p (Closure isV t env spine) =
mparens (p > 9) $ fsep [ text tag
, nest 2 $ prettyPrec 10 t
, nest 2 $ prettyList $ zipWith envEntry [0..] (envToList env)
, nest 2 $ prettyList spine ]
where envEntry i c = text ("@" ++ show i ++ " =") <+> pretty c
tag = case isV of Value{} -> "V"; Unevaled -> "E"
instance Pretty (AM s) where
prettyPrec p (Eval cl ctrl) = prettyPrec p cl <?> prettyList ctrl
prettyPrec p (Match f cc sp stack ctrl) =
mparens (p > 9) $ sep [ text "M" <+> pretty f
, nest 2 $ prettyList sp
, nest 2 $ prettyPrec 10 cc
, nest 2 $ pretty stack
, nest 2 $ prettyList ctrl ]
instance Pretty (CatchAllFrame s) where
pretty CatchAll{} = text "CatchAll"
instance Pretty (MatchStack s) where
pretty ([] :> _) = empty
pretty (ca :> _) = prettyList ca
instance Pretty (ControlFrame s) where
prettyPrec p (CaseK f _ _ _ _ mc) = mparens (p > 9) $ (text "CaseK" <+> pretty (qnameName f)) <?> pretty mc
prettyPrec p (ForceK _ spine0 spine1) = mparens (p > 9) $ text "ForceK" <?> prettyList (spine0 <> spine1)
prettyPrec p (TrustMeK _ sp0 sp1 sp2) = mparens (p > 9) $ sep [ text "TrustMeK"
, nest 2 $ prettyList sp0
, nest 2 $ prettyList sp1
, nest 2 $ prettyList sp2 ]
prettyPrec _ (NatSucK n) = text ("+" ++ show n)
prettyPrec p (PrimOpK f _ vs cls _) = mparens (p > 9) $ sep [ text "PrimOpK" <+> pretty f
, nest 2 $ prettyList vs
, nest 2 $ prettyList cls ]
prettyPrec p (UpdateThunk ps) = mparens (p > 9) $ text "UpdateThunk" <+> text (show (length ps))
prettyPrec p (ApplyK spine) = mparens (p > 9) $ text "ApplyK" <?> prettyList spine
prettyPrec p NormaliseK = text "NormaliseK"
prettyPrec p (ArgK cl _) = mparens (p > 9) $ sep [ text "ArgK" <+> prettyPrec 10 cl ]