From a5db482c7b116c1e4dc2242da30affea4f0bba2e Mon Sep 17 00:00:00 2001 From: Olle Fredriksson Date: Mon, 25 Mar 2024 15:13:28 +0100 Subject: [PATCH] Return Stuck values for (potentially) recursive terms And check if they are "unstuck" before unfolding them. --- src/Core/Evaluation.hs | 13 +++++- src/Elaboration/Context.hs | 89 ++++++++++++++++++++++++++++++-------- 2 files changed, 82 insertions(+), 20 deletions(-) diff --git a/src/Core/Evaluation.hs b/src/Core/Evaluation.hs index 3964ba7..a235d4e 100644 --- a/src/Core/Evaluation.hs +++ b/src/Core/Evaluation.hs @@ -16,6 +16,7 @@ import qualified Core.Domain.Telescope as Domain.Telescope import qualified Core.Syntax as Syntax import Data.OrderedHashMap (OrderedHashMap) import qualified Data.OrderedHashMap as OrderedHashMap +import qualified Data.Sequence as Seq import Data.Some (Some) import Data.Tsil (Tsil) import qualified Data.Tsil as Tsil @@ -28,6 +29,7 @@ import Plicity import Protolude hiding (IntMap, Seq, evaluate, force, head, try) import Query (Query) import qualified Query +import qualified Query.Mapped as Mapped import Rock import Telescope (Telescope) import qualified Telescope @@ -61,15 +63,19 @@ evaluate env term = Domain.var var Just value | Index.Succ index > Environment.glueableBefore env -> - Domain.Glued (Domain.Var var) mempty value + Domain.Glued (Domain.Var var) mempty $ Domain.Stuck (Domain.Var var) mempty value mempty | otherwise -> value Syntax.Global name -> do result <- try $ fetch $ Query.ElaboratedDefinition name case result of Right (Syntax.ConstantDefinition term', _) -> do + recursive <- fetch $ Query.TransitiveDependencies name $ Mapped.Query name value <- lazyEvaluate Environment.empty term' - pure $ Domain.Glued (Domain.Global name) mempty value + pure + if isJust recursive + then Domain.Glued (Domain.Global name) mempty $ Domain.Stuck (Domain.Global name) mempty value mempty + else Domain.Glued (Domain.Global name) mempty value Left (Cyclic (_ :: Some Query)) -> pure $ Domain.global name _ -> @@ -207,6 +213,9 @@ apply fun plicity arg = panic "Core.Evaluation: plicity mismatch" Domain.Neutral hd spine -> pure $ Domain.Neutral hd $ spine Domain.:> Domain.App plicity arg + Domain.Stuck hd args headApp Domain.Empty -> do + headApp' <- apply headApp plicity arg + pure $ Domain.Stuck hd (args Seq.:|> (plicity, arg)) headApp' Domain.Empty Domain.Stuck hd args value spine -> pure $ Domain.Stuck hd args value $ spine Domain.:> Domain.App plicity arg Domain.Glued hd spine value -> do diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs index 5a1e80a..e42fa4a 100644 --- a/src/Elaboration/Context.hs +++ b/src/Elaboration/Context.hs @@ -684,6 +684,40 @@ forceNeutral context head_ spine pure Nothing _ -> pure Nothing +isStuck :: Context v -> Domain.Value -> M Bool +isStuck outerContext outerHeadApp = + fmap (either identity (\() -> False)) $ runExceptT $ go True outerContext outerHeadApp + where + go :: Bool -> Context v -> Domain.Value -> ExceptT Bool M () + go lamIsStuck context headApp = do + headApp' <- lift $ forceHeadGlue context headApp + -- putText "isStuck.go:" + -- lift $ dumpValue context headApp' + case headApp' of + Domain.Glued _ (Domain.Apps args) value -> do + argsStuck <- lift $ fmap (either identity (\() -> False)) $ runExceptT $ mapM_ (mapM_ $ go False context) args + if not argsStuck + then pure () + else go False context value + Domain.Glued _ _ value -> + go False context value + Domain.AnyNeutral _ (Domain.Apps args) -> mapM_ (mapM_ $ go False context) args + Domain.Con _ args -> mapM_ (mapM_ $ go False context) args + Domain.Lit {} -> pure () + Domain.Pi binding domain _ targetClosure -> do + go False context domain + (context', var) <- lift $ extend context (Binding.toName binding) domain + target <- lift $ Evaluation.evaluateClosure targetClosure $ Domain.var var + go False context' target + Domain.Fun domain _ target -> do + go False context domain + go False context target + Domain.Lam {} | not lamIsStuck -> pure () + _ -> do + -- putText "isStuck.stuck:" + -- lift $ dumpValue context headApp' + throwError True + -- | Evaluate the head of a value further, if (now) possible due to meta -- solutions or new value bindings. Also evaluates through glued values. forceHead @@ -692,16 +726,16 @@ forceHead -> M Domain.Value forceHead context value = case value of - Domain.Neutral head_ spine -> do - maybeEqValue <- forceNeutral context head_ spine - case maybeEqValue of - Just meqValue -> do - value'' <- meqValue - forceHead context value'' - Nothing -> - pure value - Domain.Stuck head_ args value' spine -> - undefined -- TODO + Domain.Neutral head_ spine -> neutral head_ spine + Domain.Stuck head_ args headApp spine -> do + stuck <- isStuck context headApp + if stuck + then neutral head_ $ Domain.Apps args <> spine + else do + -- putText "forceHead.unstuck:" + -- dumpValue context headApp + value' <- Evaluation.applySpine headApp spine + forceHead context value' Domain.Glued _ _ value' -> forceHead context value' Domain.Lazy lazyValue -> do @@ -709,6 +743,15 @@ forceHead context value = forceHead context value' _ -> pure value + where + neutral head_ spine = do + maybeEqValue <- forceNeutral context head_ spine + case maybeEqValue of + Just meqValue -> do + value' <- meqValue + forceHead context value' + Nothing -> + pure value -- | Evaluate the head of a value further, if (now) possible due to meta -- solutions or new value bindings, returning glued values. @@ -718,7 +761,24 @@ forceHeadGlue -> M Domain.Value forceHeadGlue context value = case value of - Domain.Neutral head_ spine -> do + Domain.Neutral head_ spine -> neutral head_ spine + Domain.Stuck head_ args headApp spine -> do + let spine' = Domain.Apps args <> spine + stuck <- isStuck context headApp + if stuck + then neutral head_ spine' + else do + -- putText "forceHeadGlue.unstuck:" + -- dumpValue context headApp + value' <- Evaluation.applySpine headApp spine + forceHeadGlue context value' + Domain.Lazy lazyValue -> do + value' <- force lazyValue + forceHeadGlue context value' + _ -> + pure value + where + neutral head_ spine = do maybeEqValue <- forceNeutral context head_ spine case maybeEqValue of Just meqValue -> do @@ -726,13 +786,6 @@ forceHeadGlue context value = pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue Nothing -> pure value - Domain.Stuck head_ args value' spine -> - undefined -- TODO - Domain.Lazy lazyValue -> do - value' <- force lazyValue - forceHeadGlue context value' - _ -> - pure value instantiateType :: Context v