module Agda.TypeChecking.Reduce.Fast
( fastReduce ) where
import Control.Applicative
import Control.Monad.Reader
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable (traverse)
import System.IO.Unsafe
import Data.IORef
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
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.Interaction.Options
import Agda.Utils.Maybe
import Agda.Utils.Memo
import Agda.Utils.Function
import Agda.Utils.Functor
#include "undefined.h"
import Agda.Utils.Impossible
data CompactDef =
CompactDef { cdefDelayed :: Bool
, cdefNonterminating :: Bool
, cdefDef :: CompactDefn
, cdefRewriteRules :: RewriteRules
}
data CompactDefn
= CFun { cfunCompiled :: FastCompiledClauses, cfunProjection :: Maybe QName }
| CCon { cconSrcCon :: ConHead }
| CForce
| CTyCon
| COther
compactDef :: Maybe ConHead -> Maybe ConHead -> Maybe QName -> Definition -> RewriteRules -> ReduceM CompactDef
compactDef z s pf def rewr = do
cdefn <-
case theDef def of
_ | Just (defName def) == pf -> pure CForce
Constructor{conSrcCon = c} -> pure CCon{cconSrcCon = c}
Function{funCompiled = Just cc, funClauses = _:_, funProjection = proj} ->
pure CFun{ cfunCompiled = fastCompiledClauses z s cc
, cfunProjection = projOrig <$> proj }
Datatype{dataClause = Nothing} -> pure CTyCon
Record{recClause = Nothing} -> pure CTyCon
_ -> pure COther
return $
CompactDef { cdefDelayed = defDelayed def == Delayed
, cdefNonterminating = defNonterminating 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
}
data FastCompiledClauses
= FCase Int (FastCase FastCompiledClauses)
| FDone [Arg ArgName] Term
| FFail
type FastStack = [(FastCompiledClauses, MaybeReducedElims, Elims -> Elims)]
fastCompiledClauses :: Maybe ConHead -> Maybe ConHead -> CompiledClauses -> FastCompiledClauses
fastCompiledClauses z s cc =
case cc of
Fail -> FFail
Done xs b -> FDone xs b
Case (Arg _ n) bs -> FCase n (fastCase z s bs)
fastCase :: Maybe ConHead -> Maybe ConHead -> Case CompiledClauses -> FastCase FastCompiledClauses
fastCase z s (Branches proj con lit wild) =
FBranches
{ fprojPatterns = proj
, fconBranches = Map.mapKeysMonotonic (nameId . qnameName) $ fmap (fastCompiledClauses z s . content) con
, fsucBranch = fmap (fastCompiledClauses z s . content) $ flip Map.lookup con . conName =<< s
, flitBranches = fmap (fastCompiledClauses z s) lit
, fcatchAllBranch = fmap (fastCompiledClauses z s) wild }
lookupCon :: QName -> FastCase c -> Maybe c
lookupCon c (FBranches _ cons _ _ _) = Map.lookup (nameId $ qnameName c) cons
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
strictSubst :: Bool -> [Term] -> Term -> Term
strictSubst strict us
| not strict = applySubst rho
| otherwise = go 0
where
rho = parallelS us
go k v =
case v of
Var x es
| x < k -> Var x $! map' (goE k) es
| otherwise -> applyE (raise k $ us !! (x k)) $! map' (goE k) es
Def f es -> defApp f [] $! map' (goE k) es
Con c ci vs -> Con c ci $! map' (mapArg' $ go k) vs
Lam i b -> Lam i $! goAbs k b
Lit{} -> v
_ -> applySubst (liftS k rho) v
goE k (Apply v) = Apply $! mapArg' (go k) v
goE _ p = p
goAbs k (Abs x v) = Abs x $! go (k + 1) v
goAbs k (NoAbs x v) = NoAbs x $! go k v
map' :: (a -> b) -> [a] -> [b]
map' f [] = []
map' f (x : xs) = ((:) $! f x) $! map' f xs
mapArg' :: (a -> b) -> Arg a -> Arg b
mapArg' f (Arg i x) = Arg i $! f x
fastReduce :: Bool -> Term -> ReduceM (Blocked Term)
fastReduce allowNonTerminating v = do
let name (Con c _ _) = c
name _ = __IMPOSSIBLE__
z <- fmap name <$> getBuiltin' builtinZero
s <- fmap name <$> getBuiltin' builtinSuc
pf <- fmap primFunName <$> getPrimitive' "primForce"
rwr <- optRewriting <$> pragmaOptions
constInfo <- unKleisli $ \f -> do
info <- getConstInfo f
rewr <- getRewriteRulesFor f
compactDef z s pf info rewr
ReduceM $ \ env -> reduceTm env (memoQName constInfo) allowNonTerminating rwr z s v
unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
unKleisli f = ReduceM $ \ env x -> unReduceM (f x) env
reduceTm :: ReduceEnv -> (QName -> CompactDef) -> Bool -> Bool -> Maybe ConHead -> Maybe ConHead -> Term -> Blocked Term
reduceTm env !constInfo allowNonTerminating hasRewriting zero suc = reduceB' 0
where
strictEveryNth = 1000
runReduce m = unReduceM m env
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
reduceB' steps v =
case v of
Def f es -> unfoldDefinitionE steps False reduceB' (Def f []) f es
Con c ci vs ->
case unfoldDefinition steps False reduceB' (Con c ci []) (conName c) vs of
NotBlocked r v -> NotBlocked r $ reduceNat v
b -> b
Lit{} -> done
Var{} -> done
_ -> runReduce (slowReduceTerm v)
where
done = notBlocked v
reduceNat v@(Con c ci [])
| isZero c = Lit $ LitNat (getRange c) 0
reduceNat v@(Con c ci [a])
| isSuc c = inc . ignoreBlocking $ reduceB' 0 (unArg a)
where
inc (Lit (LitNat r n)) = Lit (LitNat noRange $ n + 1)
inc w = Con c ci [defaultArg w]
reduceNat v = v
originalProjection :: QName -> QName
originalProjection q =
case cdefDef $ constInfo q of
CFun{ cfunProjection = Just p } -> p
_ -> __IMPOSSIBLE__
unfoldCorecursionE :: Elim -> Blocked Elim
unfoldCorecursionE (Proj o p) = notBlocked $ Proj o $ originalProjection p
unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) $
unfoldCorecursion 0 v
unfoldCorecursion :: Int -> Term -> Blocked Term
unfoldCorecursion steps (Def f es) = unfoldDefinitionE steps True unfoldCorecursion (Def f []) f es
unfoldCorecursion steps v = reduceB' steps v
unfoldDefinition ::
Int -> Bool -> (Int -> Term -> Blocked Term) ->
Term -> QName -> Args -> Blocked Term
unfoldDefinition steps unfoldDelayed keepGoing v f args =
unfoldDefinitionE steps unfoldDelayed keepGoing v f (map Apply args)
unfoldDefinitionE ::
Int -> Bool -> (Int -> Term -> Blocked Term) ->
Term -> QName -> Elims -> Blocked Term
unfoldDefinitionE steps unfoldDelayed keepGoing v f es =
case unfoldDefinitionStep steps unfoldDelayed (constInfo f) v f es of
NoReduction v -> v
YesReduction _ v -> (keepGoing $! steps + 1) v
unfoldDefinitionStep :: Int -> Bool -> CompactDef -> Term -> QName -> Elims -> Reduced (Blocked Term) Term
unfoldDefinitionStep steps unfoldDelayed CompactDef{cdefDelayed = delayed, cdefNonterminating = nonterm, cdefDef = def, cdefRewriteRules = rewr} v0 f es =
let v = v0 `applyE` es
dontUnfold =
(not allowNonTerminating && nonterm)
|| (not unfoldDelayed && delayed)
in case def of
CCon{cconSrcCon = c} ->
if hasRewriting then
runReduce $ rewrite (notBlocked ()) (Con c ConOSystem []) rewr es
else
NoReduction $ notBlocked $ Con c ConOSystem [] `applyE` es
CFun{cfunCompiled = cc} ->
reduceNormalE steps v0 f (map notReduced es) dontUnfold cc
CForce -> reduceForce unfoldDelayed v0 f es
CTyCon -> if hasRewriting then
runReduce $ rewrite (notBlocked ()) v0 rewr es
else
NoReduction $ notBlocked v
COther -> runReduce $ R.unfoldDefinitionStep unfoldDelayed v0 f es
where
yesReduction = YesReduction NoSimplification
reduceForce :: Bool -> Term -> QName -> Elims -> Reduced (Blocked Term) Term
reduceForce unfoldDelayed v0 pf (Apply a : Apply b : Apply s : Apply t : Apply u : Apply f : es) =
case reduceB' 0 (unArg u) of
ub@Blocked{} -> noGo ub
ub@(NotBlocked _ u)
| isWHNF u -> yesReduction $ unArg f `applyE` (Apply (defaultArg u) : es)
| otherwise -> noGo ub
where
noGo ub = NoReduction $ ub <&> \ u -> Def pf (Apply a : Apply b : Apply s : Apply t : Apply (defaultArg u) : Apply f : es)
isWHNF u = case u of
Lit{} -> True
Con{} -> True
Lam{} -> True
Pi{} -> True
Sort{} -> True
Level{} -> True
DontCare{} -> True
MetaV{} -> False
Var{} -> False
Def q _ -> isTyCon q
Shared{} -> __IMPOSSIBLE__
isTyCon q =
case cdefDef $ constInfo q of
CTyCon -> True
_ -> False
reduceForce unfoldDelayed v0 pf es = runReduce $ R.unfoldDefinitionStep unfoldDelayed v0 f es
reduceNormalE :: Int -> Term -> QName -> [MaybeReduced Elim] -> Bool -> FastCompiledClauses -> Reduced (Blocked Term) Term
reduceNormalE steps v0 f es dontUnfold cc
| dontUnfold = defaultResult
| otherwise =
case match' steps f [(cc, es, id)] of
YesReduction s u -> YesReduction s u
NoReduction es' -> if hasRewriting then
runReduce $ rewrite (void es') v0 rewr (ignoreBlocking es')
else
NoReduction $ applyE v0 <$> es'
where defaultResult = if hasRewriting then
runReduce $ rewrite (NotBlocked AbsurdMatch ()) v0 rewr (map ignoreReduced es)
else
NoReduction $ NotBlocked AbsurdMatch vfull
vfull = v0 `applyE` map ignoreReduced es
match' :: Int -> QName -> FastStack -> Reduced (Blocked Elims) Term
match' steps f ((c, es, patch) : stack) =
let no blocking es = NoReduction $ blocking $ patch $ map ignoreReduced es
yes t = yesReduction t
in case c of
FFail -> no (NotBlocked AbsurdMatch) es
FDone xs t
| m == n -> yes $ doSubst es t
| m < n -> yes $ doSubst es $ foldr lam t (drop m xs)
| otherwise -> yes $ doSubst es0 t `applyE` map ignoreReduced es1
where
n = length xs
m = length es
useStrictSubst = rem steps strictEveryNth == 0
doSubst es t = strictSubst useStrictSubst (reverse $ map (unArg . argFromElim . ignoreReduced) es) t
(es0, es1) = splitAt n es
lam x t = Lam (argInfo x) (Abs (unArg x) t)
FCase n bs ->
case splitAt n es of
(_, []) -> no (NotBlocked Underapplied) es
(es0, MaybeRed red e0 : es1) ->
let eb = case red of
Reduced b -> e0 <$ b
NotReduced -> unfoldCorecursionE e0
e = ignoreBlocking eb
es' = es0 ++ [MaybeRed (Reduced $ () <$ eb) e] ++ es1
catchAllFrame stack = maybe stack (\c -> (c, es', patch) : stack) (fcatchAllBranch bs)
litFrame l stack =
case Map.lookup l (flitBranches bs) of
Nothing -> stack
Just cc -> (cc, es0 ++ es1, patchLit) : stack
conFrame c ci vs stack =
case lookupCon (conName c) bs of
Nothing -> stack
Just cc -> ( cc
, es0 ++ map (MaybeRed NotReduced . Apply) vs ++ es1
, patchCon c ci (length vs)
) : stack
sucFrame n stack =
case fsucBranch bs of
Nothing -> stack
Just cc -> (cc, es0 ++ [v] ++ es1, patchCon (fromJust suc) ConOSystem 1)
: stack
where v = MaybeRed (Reduced $ notBlocked ()) $ Apply $ defaultArg $ Lit $ LitNat noRange n
projFrame p stack =
case lookupCon p bs of
Nothing -> stack
Just cc -> (cc, es0 ++ es1, patchLit) : stack
patchLit es = patch (es0 ++ [e] ++ es1)
where (es0, es1) = splitAt n es
patchCon c ci m es = patch (es0 ++ [Con c ci vs <$ e] ++ es2)
where (es0, rest) = splitAt n es
(es1, es2) = splitAt m rest
vs = map argFromElim es1
in case eb of
Blocked x _ -> no (Blocked x) es'
NotBlocked blk elim ->
case elim of
Apply (Arg info v) ->
case v of
MetaV x _ -> no (Blocked x) es'
Lit l@(LitNat r n) ->
let cFrame stack
| n > 0 = sucFrame (n 1) stack
| n == 0, Just z <- zero = conFrame z ConOSystem [] stack
| otherwise = stack
in match' steps f $ litFrame l $ cFrame $ catchAllFrame stack
Lit l -> match' steps f $ litFrame l $ catchAllFrame stack
Con c ci vs -> match' steps f $ conFrame c ci vs $ catchAllFrame $ stack
_ -> no (NotBlocked $ stuckOn elim blk) es'
Proj _ p -> match' steps f $ projFrame p stack
match' _ f [] =
runReduce $
traceSLn "impossible" 10
("Incomplete pattern matching when applying " ++ show f)
__IMPOSSIBLE__