From e3dbb308d3ff36b761e561c1383c87c41cb99857 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Mon, 12 Sep 2022 11:21:39 +0200 Subject: [PATCH] Detect nested patterns as smaller in the termination checker (#1524) --- .../Compiler/Abstract/Extra/Functions.hs | 20 ++++++++++++++++--- .../Analysis/Termination/Data/SizeInfo.hs | 18 +++++++---------- .../Analysis/Termination/FunctionCall.hs | 16 +++++++-------- test/Termination/Positive.hs | 1 + tests/positive/Termination/Fib.juvix | 18 +++++++++++++++++ 5 files changed, 51 insertions(+), 22 deletions(-) create mode 100644 tests/positive/Termination/Fib.juvix diff --git a/src/Juvix/Compiler/Abstract/Extra/Functions.hs b/src/Juvix/Compiler/Abstract/Extra/Functions.hs index 0bd5db7fd6..08a881913f 100644 --- a/src/Juvix/Compiler/Abstract/Extra/Functions.hs +++ b/src/Juvix/Compiler/Abstract/Extra/Functions.hs @@ -34,12 +34,26 @@ idenName = \case IdenInductive (InductiveRef i) -> i IdenAxiom (AxiomRef a) -> a -smallerPatternVariables :: Traversal' Pattern VarName -smallerPatternVariables f p = case p of +-- | A fold over all transitive children, including self +patternCosmos :: SimpleFold Pattern Pattern +patternCosmos f p = case p of + PatternVariable {} -> f p + PatternWildcard {} -> f p + PatternEmpty {} -> f p + PatternConstructorApp (ConstructorApp r args) -> + f p *> do + args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args + pure (PatternConstructorApp (ConstructorApp r args')) + +-- | A fold over all transitive children, excluding self +patternSubCosmos :: SimpleFold Pattern Pattern +patternSubCosmos f p = case p of PatternVariable {} -> pure p PatternWildcard {} -> pure p PatternEmpty {} -> pure p - PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app + PatternConstructorApp (ConstructorApp r args) -> do + args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args + pure (PatternConstructorApp (ConstructorApp r args')) viewApp :: Expression -> (Expression, [ApplicationArg]) viewApp e = diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/SizeInfo.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/SizeInfo.hs index 3a40491404..312efd682e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/SizeInfo.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/SizeInfo.hs @@ -1,13 +1,12 @@ module Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination.Data.SizeInfo where -import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Abstract.Extra import Juvix.Prelude -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function. -- Indexes are 0 based data SizeInfo = SizeInfo - { _sizeSmaller :: HashMap VarName Int, + { _sizeSmaller :: [[Pattern]], _sizeEqual :: [Pattern] } @@ -21,15 +20,12 @@ emptySizeInfo = } mkSizeInfo :: [PatternArg] -> SizeInfo -mkSizeInfo ps = SizeInfo {..} +mkSizeInfo args = SizeInfo {..} where - ps' :: [Pattern] - ps' = map (^. patternArgPattern) (filter (not . isBrace) ps) + ps :: [Pattern] + ps = map (^. patternArgPattern) (filter (not . isBrace) args) isBrace :: PatternArg -> Bool isBrace = (== Implicit) . (^. patternArgIsImplicit) - _sizeEqual = map (^. patternArgPattern) ps - _sizeSmaller :: HashMap VarName Int - _sizeSmaller = - HashMap.fromList - [ (v, i) | (i, p) <- zip [0 ..] ps', v <- p ^.. smallerPatternVariables - ] + _sizeEqual = ps + _sizeSmaller :: [[Pattern]] + _sizeSmaller = map (^.. patternSubCosmos) ps diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/FunctionCall.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/FunctionCall.hs index d254082edc..4fcd51cbb0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/FunctionCall.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/FunctionCall.hs @@ -22,20 +22,20 @@ viewCall = \case where callArg :: Sem r (CallRow, Expression) callArg = do - lt <- lessThan - eq <- equalTo - return (CallRow ((lt ^. callRow) `mplus` (eq ^. callRow)), x) + lt <- (^. callRow) <$> lessThan + eq <- (^. callRow) <$> equalTo + return (CallRow (lt `mplus` eq), x) where lessThan :: Sem r CallRow - lessThan = case x of - ExpressionIden (IdenVar v) -> do - s :: Maybe Int <- asks (HashMap.lookup v . (^. sizeSmaller)) + lessThan = case viewExpressionAsPattern x of + Nothing -> return (CallRow Nothing) + Just x' -> do + s <- asks (findIndex (elem x') . (^. sizeSmaller)) return $ case s of Nothing -> CallRow Nothing Just s' -> CallRow (Just (s', RLe)) - _ -> return (CallRow Nothing) equalTo :: Sem r CallRow - equalTo = do + equalTo = case viewExpressionAsPattern x of Just x' -> do s <- asks (elemIndex x' . (^. sizeEqual)) diff --git a/test/Termination/Positive.hs b/test/Termination/Positive.hs index 1ffa1183d4..74997806f5 100644 --- a/test/Termination/Positive.hs +++ b/test/Termination/Positive.hs @@ -53,6 +53,7 @@ testDescrFlag N.NegTest {..} = tests :: [PosTest] tests = [ PosTest "Ackerman nice def. is terminating" "." "Ack.juvix", + PosTest "Fibonacci with nested pattern" "." "Fib.juvix", PosTest "Recursive functions on Lists" "." "Data/List.juvix" ] diff --git a/tests/positive/Termination/Fib.juvix b/tests/positive/Termination/Fib.juvix new file mode 100644 index 0000000000..7e5cec23bf --- /dev/null +++ b/tests/positive/Termination/Fib.juvix @@ -0,0 +1,18 @@ +module Fib; + +inductive Nat { + zero : Nat; + suc : Nat → Nat; +}; + +infixl 6 +; ++ : Nat → Nat → Nat; ++ zero b ≔ b; ++ (suc a) b ≔ suc (a + b); + +fib : Nat -> Nat; +fib zero := zero; +fib (suc (zero)) := suc zero; +fib (suc (suc n)) := fib (suc n) + fib n; + +end;