From f8f19a65e90bcad055f5ee08ddf3eafba9d304d5 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 31 Jan 2024 17:07:09 +0100 Subject: [PATCH] Build with GHC-9.8: no more head, tail, init, last (x-partial warning) --- .../Agda/Termination/TypeBased/Definitions.hs | 5 ++- src/full/Agda/Termination/TypeBased/Graph.hs | 9 ++-- src/full/Agda/Termination/TypeBased/Monad.hs | 42 +++++++++++++------ .../Agda/Termination/TypeBased/Patterns.hs | 12 +++--- 4 files changed, 43 insertions(+), 25 deletions(-) diff --git a/src/full/Agda/Termination/TypeBased/Definitions.hs b/src/full/Agda/Termination/TypeBased/Definitions.hs index e48491f7d98..a768e9acba2 100644 --- a/src/full/Agda/Termination/TypeBased/Definitions.hs +++ b/src/full/Agda/Termination/TypeBased/Definitions.hs @@ -59,6 +59,7 @@ import qualified Agda.Termination.Order as Order import Data.List (unfoldr) import qualified Agda.Benchmarking as Benchmark import Agda.TypeChecking.Monad.Benchmark (billTo) +import qualified Agda.Utils.List1 as List1 -- | 'initSizeTypeEncoding names' computes size types for every definition in 'names' @@ -377,8 +378,8 @@ encodeDatatypeDomain :: Bool -> Bool -> [Bool] -> Tele (Dom Type) -> SizeType encodeDatatypeDomain isRecursive _ params EmptyTel = let size = if isRecursive then SDefined 0 else SUndefined -- tail because scanl inserts the given starting element in the beginning - treeArgs = tail $ - scanl (\(ind, t) isGeneric -> if isGeneric then (ind + 1, SizeGenericVar 0 ind) else (ind, UndefinedSizeType)) + treeArgs = List1.tail $ List1.scanl + (\(ind, t) isGeneric -> if isGeneric then (ind + 1, SizeGenericVar 0 ind) else (ind, UndefinedSizeType)) (0, UndefinedSizeType) params actualArgs = reverse (map snd treeArgs) diff --git a/src/full/Agda/Termination/TypeBased/Graph.hs b/src/full/Agda/Termination/TypeBased/Graph.hs index c5443ad62e9..da6c0d06d54 100644 --- a/src/full/Agda/Termination/TypeBased/Graph.hs +++ b/src/full/Agda/Termination/TypeBased/Graph.hs @@ -42,6 +42,7 @@ import qualified Agda.Benchmarking as Benchmark import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as DGraph import Agda.TypeChecking.Monad.Benchmark (billTo) import Data.Either +import Agda.Utils.List (headWithDefault) -- A size expression is represented as a minimum of a set of rigid size variables, -- where the length of the set is equal to the number of clusters. @@ -81,7 +82,7 @@ simplifySizeGraph rigidContext graph = billTo [Benchmark.TypeBasedTermination, B -- Lazy map representing an approximate cluster of each variable let rigidClusters = (mapMaybe (\(i, b) -> (i,) <$> findCluster rigidContext i) rigidContext) - let rememberNeighbor v1 v2 = IntMap.insertWith (\n old -> head n : old) v1 [v2] + let rememberNeighbor v1 v2 = IntMap.insertWith (\n old -> headWithDefault __IMPOSSIBLE__ n : old) v1 [v2] let neighbourMap = foldr (\(SConstraint _ from to) -> rememberNeighbor to from . rememberNeighbor from to) IntMap.empty enrichedGraph let clusterMapping = gatherClusters rigidClusters neighbourMap (IntMap.fromList rigidClusters) @@ -146,7 +147,7 @@ instantiateComponents baseSize rigids clusterMapping graph subst (comp : is) = d -- Some element in the component has is bigger or equal than infinity, -- which means that the component should be assigned to infinity baseSize - | head comp `IntSet.member` bottomVars = + | headWithDefault __IMPOSSIBLE__ comp `IntSet.member` bottomVars = -- The component corresponds to a non-recursive constructor, -- which means that it should be assigned to the least available size expression, -- which is a meet of certain rigids @@ -154,7 +155,7 @@ instantiateComponents baseSize rigids clusterMapping graph subst (comp : is) = d | null lowerBoundSizes = -- There are no lower bounds for the component, which means that we can try to do some witchcraft -- It won't be worse than infinity, right? - case (IntMap.lookup (head comp) fallback, ((head comp) `IntMap.lookup` clusterMapping)) of + case (IntMap.lookup (headWithDefault __IMPOSSIBLE__ comp) fallback, ((headWithDefault __IMPOSSIBLE__ comp) `IntMap.lookup` clusterMapping)) of (Just r, _) -> -- The component corresponds to a freshened variable of some recursive call, we can try to assign it to the original variable fromMaybe baseSize (subst IntMap.!? r) @@ -210,7 +211,7 @@ findLowestClusterVariable bounds target = fst $ go 0 target l -> let inner = map (go (depth + 1)) l maxLevel = maximum (map snd inner) maxLevelVars = filter (\(a, d) -> d == maxLevel) inner - in head maxLevelVars + in headWithDefault __IMPOSSIBLE__ maxLevelVars collectIncoherentRigids :: IntMap SizeExpression -> [SConstraint] -> TCM IntSet collectIncoherentRigids m g = billTo [Benchmark.TypeBasedTermination, Benchmark.SizeGraphSolving] $ collectIncoherentRigids' m g diff --git a/src/full/Agda/Termination/TypeBased/Monad.hs b/src/full/Agda/Termination/TypeBased/Monad.hs index 8ac265bf74a..57fdd99a997 100644 --- a/src/full/Agda/Termination/TypeBased/Monad.hs +++ b/src/full/Agda/Termination/TypeBased/Monad.hs @@ -25,6 +25,8 @@ import Control.Arrow ( first ) import Control.Monad import Data.Maybe import Data.Set (Set ) + +import Agda.Utils.List (headWithDefault) import Agda.Utils.Impossible import qualified Agda.Utils.Benchmark as B @@ -113,18 +115,21 @@ getConstraints :: MonadSizeChecker [[SConstraint]] getConstraints = MSC $ gets scsConstraints getCurrentConstraints :: MonadSizeChecker [SConstraint] -getCurrentConstraints = MSC $ head <$> gets scsConstraints +getCurrentConstraints = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsConstraints getCurrentRigids :: MonadSizeChecker [(Int, SizeBound)] -getCurrentRigids = MSC $ head <$> gets scsRigidSizeVars +getCurrentRigids = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsRigidSizeVars -- | Adds a new rigid variable. This function is fragile, since bound might not be expressed in terms of current rigids. -- Unfortunately we have to live with it if we want to support record projections in arbitrary places. addNewRigid :: Int -> SizeBound -> MonadSizeChecker () -addNewRigid x bound = MSC $ modify (\s -> let rigids = scsRigidSizeVars s in s { scsRigidSizeVars = ((x, bound) : head rigids) : tail rigids }) +addNewRigid x bound = MSC $ modify \s -> + case scsRigidSizeVars s of + rs:rss -> s { scsRigidSizeVars = ((x, bound) : rs) : rss } + _ -> __IMPOSSIBLE__ getCurrentCoreContext :: MonadSizeChecker [SizeContextEntry] -getCurrentCoreContext = MSC $ head <$> gets scsCoreContext +getCurrentCoreContext = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsCoreContext -- | Initializes internal data strustures that will be filled by the processing of a clause initNewClause :: [SizeBound] -> MonadSizeChecker () @@ -150,7 +155,10 @@ getArity :: QName -> MonadSizeChecker Int getArity qn = sizeSigArity . fromJust . defSizedType <$> getConstInfo qn storeConstraint :: SConstraint -> MonadSizeChecker () -storeConstraint c = MSC $ modify (\s -> s { scsConstraints = let constraints = scsConstraints s in ((c : head constraints) : tail constraints) }) +storeConstraint c = MSC $ modify \ s -> + case scsConstraints s of + cs:css -> s { scsConstraints = (c:cs):css } + [] -> __IMPOSSIBLE__ reportCall :: QName -> QName -> [Int] -> [Int] -> Closure Term -> MonadSizeChecker () reportCall q1 q2 sizes1 sizes2 place = MSC $ modify (\s -> s { scsRecCalls = (q1, q2, sizes1, sizes2, place) : scsRecCalls s }) @@ -189,10 +197,13 @@ getUndefinedSizes = MSC $ gets scsUndefinedVariables abstractCoreContext :: Int -> Either FreeGeneric SizeType -> MonadSizeChecker a -> MonadSizeChecker a abstractCoreContext i tele action = do contexts <- MSC $ gets scsCoreContext - MSC $ modify (\s -> s { scsCoreContext = ((i, tele) : (map (incrementDeBruijnEntry tele) (head contexts))) : tail contexts }) - res <- action - MSC $ modify (\s -> s { scsCoreContext = contexts }) - pure res + case contexts of + cs:css -> do + MSC $ modify \s -> s { scsCoreContext = ((i, tele) : map (incrementDeBruijnEntry tele) cs) : css } + res <- action + MSC $ modify \s -> s { scsCoreContext = contexts } + pure res + [] -> __IMPOSSIBLE__ incrementDeBruijnEntry :: Either FreeGeneric SizeType -> (Int, Either FreeGeneric SizeType) -> (Int, Either FreeGeneric SizeType) incrementDeBruijnEntry (Left _) (x, Left fg) = (x + 1, Left $ fg { fgIndex = fgIndex fg + 1 }) @@ -240,12 +251,17 @@ requestNewRigidVariables bound pack = do SizeBounded i -> newBound) pack currentRigids <- gets scsRigidSizeVars - - modify (\s -> s { scsRigidSizeVars = ((zip newVarIdxs newBounds) ++ (head currentRigids)) : tail currentRigids }) - return $ newVarIdxs + case currentRigids of + rs:rss -> do + modify \s -> s { scsRigidSizeVars = (zip newVarIdxs newBounds ++ rs) : rss } + return newVarIdxs + [] -> __IMPOSSIBLE__ appendCoreVariable :: Int -> Either FreeGeneric SizeType -> MonadSizeChecker () -appendCoreVariable i tele = MSC $ modify (\s -> s { scsCoreContext = let cc = (scsCoreContext s) in ((i, tele) : head cc) : tail cc }) +appendCoreVariable i tele = MSC $ modify \s -> + case scsCoreContext s of + c:cc -> s { scsCoreContext = ((i, tele) : c) : cc } + [] -> __IMPOSSIBLE__ runSizeChecker :: QName -> Set QName -> MonadSizeChecker a -> TCM (a, SizeCheckerState) runSizeChecker rootName mutualNames (MSC action) = do diff --git a/src/full/Agda/Termination/TypeBased/Patterns.hs b/src/full/Agda/Termination/TypeBased/Patterns.hs index 29a431597ea..3dfb244e417 100644 --- a/src/full/Agda/Termination/TypeBased/Patterns.hs +++ b/src/full/Agda/Termination/TypeBased/Patterns.hs @@ -53,7 +53,7 @@ import Agda.Termination.CallGraph import Agda.Termination.Monad import Agda.Termination.TypeBased.Graph import Data.Foldable (traverse_) -import Agda.Utils.List ((!!!)) +import Agda.Utils.List ((!!!), initWithDefault, headWithDefault, lastWithDefault, tailWithDefault) import Data.Functor ((<&>)) import Agda.Termination.CallMatrix import qualified Agda.Termination.CallMatrix @@ -109,7 +109,7 @@ matchPatterns tele patterns = do currentRootArity <- getArity currentRoot let finalLeaves = peDepthStack modifiedState let leafVariables = map (\i -> case IntMap.lookup i finalLeaves of - Just l@(_ : _) -> last l + Just l@(_ : _) -> lastWithDefault __IMPOSSIBLE__ l _ -> -1 ) [0..currentRootArity - 1] pure (leafVariables, sizeTypeOfClause) @@ -302,7 +302,7 @@ getOrRequestDepthVar cluster level = do pure $ currentLeaves List.!! level else do -- We need to populate a depth stack with a new level - let actualBound = if (head currentLeaves == -1) then SUndefined else SDefined (last currentLeaves) + let actualBound = if (headWithDefault __IMPOSSIBLE__ currentLeaves == -1) then SUndefined else SDefined (lastWithDefault __IMPOSSIBLE__ currentLeaves) [var] <- lift $ requestNewRigidVariables actualBound [SizeBounded (-1)] modify (\s -> s { peDepthStack = IntMap.insert cluster (currentLeaves ++ [var]) (peDepthStack s) }) pure var @@ -330,12 +330,12 @@ freshenPatternConstructor conName codomainDataVar domainDataVar expectedCodomain let (SizeTree topSize datatypeParameters) = expectedCodomain let shouldBeUnbounded b = b == SizeUnbounded || codomainDataVar == (-1) -- We need to strip the codomain size from the constructor here. - let modifier = if codomainDataVar /= -1 then init else id + let modifier = if codomainDataVar /= -1 then initWithDefault __IMPOSSIBLE__ else id newVarsRaw <- lift $ requestNewRigidVariables topSize (modifier (filter shouldBeUnbounded bounds)) -- tail for stripping codomain TODO -- It is important to call `domainDataVar` lazily, -- because otherwise leaf variables would gain access to a cluster var with lower level than expected domainVar <- if length newVarsRaw + 1 == length bounds then pure (-1) else domainDataVar - let newVars = snd $ List.mapAccumL (\nv bound -> if shouldBeUnbounded bound then (tail nv, head nv) else (nv, domainVar)) newVarsRaw (modifier bounds) + let newVars = snd $ List.mapAccumL (\nv bound -> if shouldBeUnbounded bound then (tailWithDefault __IMPOSSIBLE__ nv, headWithDefault __IMPOSSIBLE__ nv) else (nv, domainVar)) newVarsRaw (modifier bounds) reportSDoc "term.tbt" 70 $ vcat [ "New variables for instantiation: " <+> text (show newVars) , "Raw variables: " <+> text (show newVarsRaw) @@ -353,7 +353,7 @@ freshenCopatternProjection :: Int -> [SizeBound] -> SizeType -> PatternEncoder S freshenCopatternProjection newCoDepthVar bounds tele = do let isNewPatternSizeVar b = b == SizeUnbounded || newCoDepthVar == (-1) newVarsRaw <- lift $ requestNewRigidVariables SUndefined (filter isNewPatternSizeVar bounds) - let newVars = snd $ List.mapAccumL (\nv bound -> if isNewPatternSizeVar bound then (tail nv, head nv) else (nv, newCoDepthVar)) newVarsRaw bounds + let newVars = snd $ List.mapAccumL (\nv bound -> if isNewPatternSizeVar bound then (tailWithDefault __IMPOSSIBLE__ nv, headWithDefault __IMPOSSIBLE__ nv) else (nv, newCoDepthVar)) newVarsRaw bounds reportSDoc "term.tbt" 70 $ "Raw size type of copattern projection: " <+> pretty tele <+> "With new variabless:" <+> text (show newVars) let instantiatedSig = instantiateSizeType tele newVars pure instantiatedSig