From 9977de5fda9f366a03942a29212cec08c59196e8 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 19 Jun 2024 16:29:51 +0300 Subject: [PATCH] Add shrink for free foil tests --- .../Language/LambdaPi/Impl/FreeFoilSpec.hs | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs index 3801d686..63b3f527 100644 --- a/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs +++ b/haskell/lambda-pi/test/Language/LambdaPi/Impl/FreeFoilSpec.hs @@ -18,6 +18,14 @@ import Control.Monad.Foil import Control.Monad.Free.Foil import Language.LambdaPi.Impl.FreeFoil +shrinkLambdaPis :: (LambdaPi n, LambdaPi l) -> [(LambdaPi n, LambdaPi l)] +shrinkLambdaPis = \case + (App t1 t2, App t1' t2') -> [(t1, t1'), (t2, t2')] + (Lam x body, Lam x' body') -> + [ (Lam x t, Lam x' t') + | (t, t') <- shrinkLambdaPis (body, body')] + _ -> [] + genLambdaPi :: Distinct n => Scope n -> [Name n] -> Gen (LambdaPi n) genLambdaPi scope names = go where @@ -96,6 +104,15 @@ instance Arbitrary AlphaEquiv where (alt, n) <- runStateT (alterNames emptyScope [] t) 1 return (AlphaEquiv (n == 1) alt t') + -- cannot shrink non-equivalent pair + -- since we do not know which subterm contains non-equivalent part + shrink (AlphaEquiv False _ _) = [] + -- if terms are equivalent, then we can shrink + shrink (AlphaEquiv True t t') = + [ AlphaEquiv True s s' + | (s, s') <- shrinkLambdaPis (t, t') + ] + newtype AlphaEquivRefreshed = AlphaEquivRefreshed AlphaEquiv deriving (Arbitrary) @@ -114,6 +131,11 @@ instance Arbitrary LambdaPiWithFresh where (t, t') <- genAlphaEquivLambdaPis (\s _ -> withFresh s) emptyScope emptyScope [] return (LambdaPiWithFresh t t') + shrink (LambdaPiWithFresh t t') = + [ LambdaPiWithFresh s s' + | (s, s') <- shrinkLambdaPis (t, t') + ] + instance Show LambdaPiWithFresh where show (LambdaPiWithFresh t t') = unlines [ " t = " <> show t