From c545482df9afc509ccd100322430b5fd45a1d0a5 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 29 Nov 2023 15:29:33 +0000 Subject: [PATCH] test: EvalFullInterp gives same results as EvalFullStep This adds code to check for alpha equality of terms Signed-off-by: Ben Price --- primer/src/Primer/Core/Type/Utils.hs | 8 +++- primer/src/Primer/Core/Utils.hs | 67 ++++++++++++++++++++++++++++ primer/src/Primer/EvalFullInterp.hs | 4 +- primer/test/Tests/AlphaEquality.hs | 51 ++++++++++++++++++++- primer/test/Tests/EvalFullInterp.hs | 19 ++++++++ 5 files changed, 146 insertions(+), 3 deletions(-) diff --git a/primer/src/Primer/Core/Type/Utils.hs b/primer/src/Primer/Core/Type/Utils.hs index 782473f03..b2dc971ae 100644 --- a/primer/src/Primer/Core/Type/Utils.hs +++ b/primer/src/Primer/Core/Type/Utils.hs @@ -13,6 +13,7 @@ module Primer.Core.Type.Utils ( freeVarsTy, boundVarsTy, alphaEqTy, + alphaEqTy', concreteTy, ) where @@ -130,7 +131,12 @@ boundVarsTy = foldMap' getBoundHereDnTy . universe -- Note that we do not expand TLets, they must be structurally -- the same (perhaps with a different named binding) alphaEqTy :: Type' () () -> Type' () () -> Bool -alphaEqTy = go (0, mempty, mempty) +alphaEqTy = alphaEqTy' (0, mempty, mempty) + +-- Check two types for alpha equality where each may be from a +-- different alpha-related context +alphaEqTy' :: (Int, Map TyVarName Int, Map TyVarName Int) -> Type' () () -> Type' () () -> Bool +alphaEqTy' = go where go _ (TEmptyHole _) (TEmptyHole _) = True go bs (THole _ s) (THole _ t) = go bs s t diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index 20be0b715..c3387e310 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE ViewPatterns #-} + module Primer.Core.Utils ( freshLocalName, freshLocalName', @@ -23,6 +25,7 @@ module Primer.Core.Utils ( freeGlobalVars, alphaEqTy, concreteTy, + alphaEq, freshen, ) where @@ -31,8 +34,10 @@ import Foreword import Control.Monad.Fresh (MonadFresh, fresh) import Data.Data (Data) import Data.Generics.Uniplate.Data (universe) +import Data.Map.Strict qualified as M import Data.Set qualified as S import Data.Set.Optics (setOf) +import Data.Tuple.Extra (firstM) import Optics ( Fold, Traversal, @@ -52,6 +57,7 @@ import Optics ( import Primer.Core ( CaseBranch' (..), + CaseFallback' (CaseExhaustive, CaseFallback), Expr, Expr' (..), GVarName, @@ -73,6 +79,7 @@ import Primer.Core ( import Primer.Core.Fresh (freshLocalName, freshLocalName') import Primer.Core.Type.Utils ( alphaEqTy, + alphaEqTy', boundVarsTy, concreteTy, forgetKindMetadata, @@ -196,6 +203,66 @@ freeGlobalVars e = S.fromList [v | Var _ (GlobalVarRef v) <- universe e] exprIDs :: (HasID a, HasID b, HasID c) => Traversal' (Expr' a b c) ID exprIDs = (_exprMeta % _id) `adjoin` (_exprTypeMeta % _id) `adjoin` (_exprKindMeta % _id) +-- Check two terms for alpha equality +-- +-- it makes usage easier if this is pure +-- i.e. we don't want to need a fresh name supply +-- We assume both inputs are both from the same context +-- +-- Note that we do not expand let bindings, they must be structurally +-- the same (perhaps with a different named binding) +alphaEq :: Expr' () () () -> Expr' () () () -> Bool +alphaEq = go (0, mempty, mempty) + where + go bs (Hole _ t1) (Hole _ t2) = go bs t1 t2 + go _ (EmptyHole _) (EmptyHole _) = True + go bs (Ann _ t1 ty1) (Ann _ t2 ty2) = go bs t1 t2 && alphaEqTy' (extractTypeEnv bs) ty1 ty2 + go bs (App _ f1 t1) (App _ f2 t2) = go bs f1 f2 && go bs t1 t2 + go bs (APP _ e1 ty1) (APP _ e2 ty2) = go bs e1 e2 && alphaEqTy' (extractTypeEnv bs) ty1 ty2 + go bs (Con _ c1 as1) (Con _ c2 as2) = c1 == c2 && length as1 == length as2 && and (zipWith (go bs) as1 as2) + go bs (Lam _ v1 t1) (Lam _ v2 t2) = go (newTm bs v1 v2) t1 t2 + go bs (LAM _ v1 t1) (LAM _ v2 t2) = go (newTy bs v1 v2) t1 t2 + go (_, bs1, bs2) (Var _ (LocalVarRef v1)) (Var _ (LocalVarRef v2)) = bs1 ! Left v1 == bs2 ! Left v2 + go _ (Var _ (GlobalVarRef v1)) (Var _ (GlobalVarRef v2)) = v1 == v2 + go bs (Let _ v1 s1 t1) (Let _ v2 s2 t2) = go bs s1 s2 && go (newTm bs v1 v2) t1 t2 + go bs (LetType _ v1 ty1 t1) (LetType _ v2 ty2 t2) = alphaEqTy' (extractTypeEnv bs) ty1 ty2 && go (newTy bs v1 v2) t1 t2 + go bs (Letrec _ v1 t1 ty1 e1) (Letrec _ v2 t2 ty2 e2) = + go (newTm bs v1 v2) t1 t2 + && alphaEqTy' (extractTypeEnv bs) ty1 ty2 + && go (newTm bs v1 v2) e1 e2 + go bs (Case _ e1 brs1 fb1) (Case _ e2 brs2 fb2) = + go bs e1 e2 + && and + ( zipWith + ( \(CaseBranch c1 (fmap bindName -> vs1) t1) + (CaseBranch c2 (fmap bindName -> vs2) t2) -> + c1 + == c2 + && length vs1 + == length vs2 + && go (foldl' (uncurry . newTm) bs $ zip vs1 vs2) t1 t2 + ) + brs1 + brs2 + ) + && case (fb1, fb2) of + (CaseExhaustive, CaseExhaustive) -> True + (CaseFallback f1, CaseFallback f2) -> go bs f1 f2 + _ -> False + go _ (PrimCon _ c1) (PrimCon _ c2) = c1 == c2 + go _ _ _ = False + p ! n = case p M.!? n of + Nothing -> Left n -- free vars: compare by name + Just i -> Right i -- bound vars: up to alpha + -- Note that the maps 'p' and 'q' map names to "which forall + -- they came from", in some sense. The @c@ value is how many + -- binders we have gone under, and is thus the next value free + -- in the map. + new (c, bs1, bs2) n m = (c + 1 :: Int, M.insert n c bs1, M.insert m c bs2) + newTm bs v1 v2 = new bs (Left v1) (Left v2) + newTy bs v1 v2 = new bs (Right v1) (Right v2) + extractTypeEnv (c, bs1, bs2) = let f = M.fromList . mapMaybe (firstM rightToMaybe) . M.assocs in (c, f bs1, f bs2) + freshen :: Set Name -> LocalName k -> LocalName k freshen fvs n = go (0 :: Int) where diff --git a/primer/src/Primer/EvalFullInterp.hs b/primer/src/Primer/EvalFullInterp.hs index df576f2fc..cefaf08ab 100644 --- a/primer/src/Primer/EvalFullInterp.hs +++ b/primer/src/Primer/EvalFullInterp.hs @@ -141,7 +141,9 @@ interp (MicroSec t) tydefs env dir e = do -- inside holes, by convincing Haskell's runtime system to do the -- evaluation for us, in a call-by-need fashion. We return an AST -- of the evaluated term, which will be type-correct (assuming the --- input was): see 'Tests.EvalFullInterp.tasty_type_preservation'. +-- input was): see 'Tests.EvalFullInterp.tasty_type_preservation'; +-- and will agree with iterating the small-step interpreter: see +-- 'Tests.EvalFullInterp.tasty_two_interp_agree'. -- -- Warnings: -- - Trying to evaluate a divergent term will (unsurprisingly) not terminate, diff --git a/primer/test/Tests/AlphaEquality.hs b/primer/test/Tests/AlphaEquality.hs index d89a267f5..eb5c5e0bc 100644 --- a/primer/test/Tests/AlphaEquality.hs +++ b/primer/test/Tests/AlphaEquality.hs @@ -5,10 +5,11 @@ import Foreword import Hedgehog hiding (Property, check, property) import Primer.Builtins import Primer.Core ( + Expr, Type', ) import Primer.Core.DSL -import Primer.Core.Utils (alphaEqTy, forgetTypeMetadata) +import Primer.Core.Utils (alphaEq, alphaEqTy, forgetMetadata, forgetTypeMetadata) import Primer.Gen.Core.Raw ( evalExprGen, genTyVarName, @@ -101,6 +102,48 @@ tasty_alpha = property $ do where f v = create_ $ tforall v ktype $ tvar v +unit_tm_1 :: Assertion +unit_tm_1 = alphaNotEqTm (con0 cTrue) (con0 cFalse) + +unit_tm_2 :: Assertion +unit_tm_2 = alphaEqTm (con cCons [con0 cTrue, con0 cNil]) (con cCons [con0 cTrue, con0 cNil]) + +unit_tm_3 :: Assertion +unit_tm_3 = alphaNotEqTm (con cCons [con0 cFalse, con0 cNil]) (con cCons [con0 cTrue, con0 cNil]) + +unit_tm_4 :: Assertion +unit_tm_4 = alphaNotEqTm (con cCons [con0 cFalse, con0 cNil]) (con0 cTrue) + +unit_tm_5 :: Assertion +unit_tm_5 = alphaNotEqTm (lam "x" $ con0 cTrue) (con0 cTrue) + +unit_tm_6 :: Assertion +unit_tm_6 = alphaEqTm (lam "x" $ lvar "x") (lam "y" $ lvar "y") + +unit_tm_7 :: Assertion +unit_tm_7 = alphaNotEqTm (lam "x" $ lvar "x") (lam "y" $ con0 cTrue) + +unit_tm_8 :: Assertion +unit_tm_8 = alphaNotEqTm (lAM "x" emptyHole) (lam "y" emptyHole) + +unit_tm_9 :: Assertion +unit_tm_9 = alphaNotEqTm (lam "x" $ lam "y" $ lvar "x") (lam "x" $ lam "y" $ lvar "y") + +unit_tm_10 :: Assertion +unit_tm_10 = alphaNotEqTm (lam "x" $ con1 cJust $ lvar "x") (con1 cJust $ lam "x" $ lvar "x") + +unit_tm_11 :: Assertion +unit_tm_11 = alphaNotEqTm (lam "x" $ lvar "x" `app` con0 cTrue) (lam "x" (lvar "x") `app` con0 cTrue) + +unit_tm_repeated_names :: Assertion +unit_tm_repeated_names = alphaEqTm (lam "a" $ lam "b" $ lvar "x" `app` lvar "x") (lam "a" $ lam "a" $ lvar "x" `app` lvar "x") + +unit_tm_tmp :: Assertion +unit_tm_tmp = + alphaEqTm + (lAM "x" $ lAM "y" $ lam "x" $ hole $ case_ emptyHole [branch cTrue [("x", Nothing)] emptyHole]) + (lAM "x" $ lAM "y" $ lam "x0" $ hole $ case_ emptyHole [branch cTrue [("x1", Nothing)] emptyHole]) + create_ :: S (Type' a b) -> Alpha create_ = Alpha . forgetTypeMetadata . create' @@ -113,3 +156,9 @@ instance Eq Alpha where assertNotEqual :: Alpha -> Alpha -> Assertion assertNotEqual s t = assertBool "types are equal" $ s /= t + +alphaEqTm :: S Expr -> S Expr -> Assertion +alphaEqTm s t = assertBool "terms should be equal" $ alphaEq (forgetMetadata $ create' s) (forgetMetadata $ create' t) + +alphaNotEqTm :: S Expr -> S Expr -> Assertion +alphaNotEqTm s t = assertBool "terms should not be equal" $ not $ alphaEq (forgetMetadata $ create' s) (forgetMetadata $ create' t) diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs index 2ef46e0fe..439726f6c 100644 --- a/primer/test/Tests/EvalFullInterp.hs +++ b/primer/test/Tests/EvalFullInterp.hs @@ -33,12 +33,14 @@ import Primer.Builtins.DSL (boolAnn, bool_, list_, nat) import Primer.Core import Primer.Core.DSL import Primer.Core.Utils ( + alphaEq, forgetMetadata, generateIDs, ) import Primer.Def (DefMap) import Primer.Eval import Primer.EvalFullInterp (InterpError (..), Timeout (MicroSec), interp, mkGlobalEnv) +import Primer.EvalFullStep (evalFullStepCount) import Primer.Examples qualified as Examples ( even, map, @@ -83,6 +85,7 @@ import Primer.Test.Expected ( mapEven, ) import Primer.Test.Util ( + failWhenSevereLogs, primDefs, ) import Primer.TypeDef (TypeDefMap) @@ -469,6 +472,22 @@ tasty_type_preservation = withTests 1000 s'' <- checkTest ty =<< generateIDs s' s' === forgetMetadata s'' -- check no smart holes happened +tasty_two_interp_agree :: Property +tasty_two_interp_agree = withTests 1000 + $ withDiscards 2000 + $ propertyWT testModules + $ do + let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules + tds <- asks typeDefs + (dir, t, _ty) <- genDirTm + let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} + let optsR = RunRedexOptions{pushAndElide = True} + (_, ss) <- failWhenSevereLogs $ evalFullStepCount @EvalLog UnderBinders optsV optsR tds globs 100 dir t + si <- liftIO (evalFullTest' (MicroSec 10_000) tds globs dir $ forgetMetadata t) + case (ss, si) of + (Right ss', Right si') -> label "both terminated" >> Hedgehog.diff (forgetMetadata ss') alphaEq si' + _ -> label "one failed to terminate" + ---- Unsaturated primitives are stuck terms unit_prim_stuck :: Assertion unit_prim_stuck =