From 974b5ee7715b9d15707ac4685dafa7cd41535c94 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 29 Nov 2023 16:42:40 +0000 Subject: [PATCH 1/7] test: tasty_prim_hex_nat sensible directions We sometimes evaluate a `case` and sometimes an `app`. These should be evaluated with different directions. This was noticed when implementing a more efficient interpreter which gave a different output when evaluating the checkable `case` in a synthesis context. Signed-off-by: Ben Price --- primer/test/Tests/EvalFull.hs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 7a51080e1..6d76e9be3 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -1311,11 +1311,11 @@ tasty_prim_hex_nat :: Property tasty_prim_hex_nat = withTests 20 . property $ do n <- forAllT $ Gen.integral $ Range.constant 0 50 let ne = nat n - ((e, r, prims), maxID) = + ((dir, e, r, prims), maxID) = create $ if n <= 15 then - (,,) + (Chk,,,) <$> case_ ( pfun NatToHex `app` ne @@ -1332,16 +1332,15 @@ tasty_prim_hex_nat = withTests 20 . property $ do ) ] <*> con cJust [ne] - `ann` (tcon tMaybe `tapp` tcon tNat) <*> primDefs else - (,,) + (Syn,,,) <$> pfun NatToHex `app` ne <*> con cNothing [] `ann` (tcon tMaybe `tapp` tcon tChar) <*> primDefs - s <- evalFullTasty maxID builtinTypes prims 7 Syn e + s <- evalFullTasty maxID builtinTypes prims 7 dir e over evalResultExpr zeroIDs s === Right (zeroIDs r) unit_prim_char_eq_1 :: Assertion From 7e1e08eeec495368a99f36e56281266ea6faec10 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 5 Dec 2023 17:42:55 +0000 Subject: [PATCH 2/7] refactor: generalise TestM to a transformer, now have MonadIO WT This is needed to be able to run `IO` actions in `PropertyWT`, which will itself be needed when we implement a more efficient evaluator (due to using `System.Timeout` to avoid infinite loops). Another choice would be to generalise `WT` to be a transformer also. However, we only actually use the (hypothetical) `WT IO` and not any other `WT m`. Since testing showed that the extra polymorphism caused GHC to emit much less (memory) efficient code, we will use the monomorphic version. (I expect that sufficient use of specialization pragmas would fix the memory leaks for a transformer version of `WT`, but I have not verified this.) Signed-off-by: Ben Price --- primer/gen/Primer/Gen/Core/Typed.hs | 11 ++++++----- primer/test/Tests/Typecheck.hs | 6 +++--- primer/testlib/Primer/Test/TestM.hs | 27 +++++++++++++++++---------- 3 files changed, 26 insertions(+), 18 deletions(-) diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index fa7cee4ce..ee20cc077 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -75,8 +75,8 @@ import Primer.Name (Name, NameCounter, freshName, unName, unsafeMkName) import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine) import Primer.Subst (substTy, substTySimul) import Primer.Test.TestM ( - TestM, - evalTestM, + TestT, + evalTestT, isolateTestM, ) import Primer.TypeDef ( @@ -130,7 +130,7 @@ type TypeG = Type' () () type ExprG = Expr' () () () -newtype WT a = WT {unWT :: ReaderT Cxt TestM a} +newtype WT a = WT {unWT :: ReaderT Cxt (TestT IO) a} deriving newtype ( Functor , Applicative @@ -138,6 +138,7 @@ newtype WT a = WT {unWT :: ReaderT Cxt TestM a} , MonadReader Cxt , MonadFresh NameCounter , MonadFresh ID + , MonadIO ) -- | Run an action and ignore any effect on the fresh name/id state @@ -701,8 +702,8 @@ genInt = where intBound = fromIntegral (maxBound :: Word64) -- arbitrary -hoist' :: Applicative f => Cxt -> WT a -> f a -hoist' cxt = pure . evalTestM 0 . flip runReaderT cxt . unWT +hoist' :: Cxt -> WT a -> IO a +hoist' cxt = evalTestT 0 . flip runReaderT cxt . unWT -- | Convert a @PropertyT WT ()@ into a @Property@, which Hedgehog can test. -- It is recommended to do more than default number of tests when using this module. diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 7fcacb93f..dbf47c4f2 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -5,7 +5,7 @@ import Foreword import Control.Monad.Fresh (MonadFresh) import Data.Map qualified as Map -import Hedgehog hiding (Property, Var, check, property, withDiscards, withTests) +import Hedgehog hiding (Property, TestT, Var, check, property, withDiscards, withTests) import Hedgehog.Gen qualified as Gen import Hedgehog.Range qualified as Range import Optics (over, set, (%), (%~)) @@ -106,7 +106,7 @@ import Primer.Module (Module (..), builtinModule, primitiveModule) import Primer.Name (Name, NameCounter) import Primer.Primitives (PrimDef (HexToNat), tChar) import Primer.Primitives.DSL (pfun) -import Primer.Test.TestM (TestM, evalTestM) +import Primer.Test.TestM (TestT, evalTestM) import Primer.Test.Util ( tcn, vcn, @@ -1069,7 +1069,7 @@ smartSynthKindGives tIn tExpect = -- Compare result to input, ignoring any difference in IDs (Right (_, tGot), Right (_, tExpect')) -> on (@?=) zeroTypeIDs tGot tExpect' -newtype TypecheckTestM a = TypecheckTestM {unTypecheckTestM :: ExceptT TypeError (ReaderT Cxt TestM) a} +newtype TypecheckTestM a = TypecheckTestM {unTypecheckTestM :: ExceptT TypeError (ReaderT Cxt (TestT Identity)) a} deriving newtype ( Functor , Applicative diff --git a/primer/testlib/Primer/Test/TestM.hs b/primer/testlib/Primer/Test/TestM.hs index 03f27429c..3ae1b79c8 100644 --- a/primer/testlib/Primer/Test/TestM.hs +++ b/primer/testlib/Primer/Test/TestM.hs @@ -1,6 +1,8 @@ -- A test monad for generating names and IDs and typechecking module Primer.Test.TestM ( + TestT, TestM, + evalTestT, evalTestM, isolateTestM, ) where @@ -13,28 +15,33 @@ import Primer.Name (NameCounter) -- This monad is responsible for generating fresh IDs and names in tests. -- If we need other abilities, this will be the base monad. -newtype TestM a = TestM {unTestM :: State Int a} - deriving newtype (Functor, Applicative, Monad) +newtype TestT m a = TestT {unTestT :: StateT Int m a} + deriving newtype (Functor, Applicative, Monad, MonadIO) + +type TestM a = TestT Identity a -- | Run an action and ignore any effect on the fresh name/id state -isolateTestM :: TestM a -> TestM a -isolateTestM m = TestM $ do +isolateTestM :: Monad m => TestT m a -> TestT m a +isolateTestM m = TestT $ do st <- get - x <- unTestM m + x <- unTestT m put st pure x +evalTestT :: Monad m => ID -> TestT m a -> m a +evalTestT (ID id_) = flip evalStateT id_ . unTestT + evalTestM :: ID -> TestM a -> a -evalTestM (ID id_) = fst . flip runState id_ . unTestM +evalTestM id_ = runIdentity . evalTestT id_ -instance MonadFresh ID TestM where - fresh = TestM $ do +instance Monad m => MonadFresh ID (TestT m) where + fresh = TestT $ do i <- get put $ i + 1 pure $ ID i -instance MonadFresh NameCounter TestM where - fresh = TestM $ do +instance Monad m => MonadFresh NameCounter (TestT m) where + fresh = TestT $ do i <- get put $ i + 1 -- A bit of a hack: make the names generated a,a1,a2,... as the testsuite From c65ee5c90f66c91ec9c5f80dee8ac774977efc85 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 29 Nov 2023 16:33:45 +0000 Subject: [PATCH 3/7] refactor: generalise hasTypeLets There is no need for this to care about the metadata's type. Signed-off-by: Ben Price --- primer/test/Tests/Eval/Utils.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs index b0fd07fbe..b667b26cb 100644 --- a/primer/test/Tests/Eval/Utils.hs +++ b/primer/test/Tests/Eval/Utils.hs @@ -10,6 +10,7 @@ module Tests.Eval.Utils ( import Foreword import Control.Monad.Fresh (MonadFresh) +import Data.Data (Data) import Data.Generics.Uniplate.Data (universe, universeBi) import Data.Map qualified as Map import Hedgehog (PropertyT) @@ -94,7 +95,7 @@ x ~~= y = forgetTypeMetadata x @?= forgetTypeMetadata y -- | Does this expression have any unsupported-by-the-typechecker subterms? -- These are @let@s binding type variables, either a 'LetType' in a term, -- or a 'TLet' in an embedded type. -hasTypeLets :: Expr -> Bool +hasTypeLets :: (Data a, Data b, Data c) => Expr' a b c -> Bool hasTypeLets e = not $ null [() | LetType{} <- universe e] From b6bd70c3d2d5ef3f9f63229c8af5ad7bb3a0be79 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 15 Nov 2023 14:48:43 +0000 Subject: [PATCH 4/7] refactor: rename EvalFull to make room for new interpreter We will shortly implement a more efficient "full evaluator", and wish to disambiguate some naming. Signed-off-by: Ben Price --- primer-api/src/Primer/API.hs | 2 +- primer-benchmark/src/Benchmarks.hs | 22 +++++++++---------- primer/primer.cabal | 4 ++-- primer/src/Primer/App.hs | 2 +- .../Primer/{EvalFull.hs => EvalFullStep.hs} | 2 +- primer/test/Tests/Action/Available.hs | 2 +- .../Tests/{EvalFull.hs => EvalFullStep.hs} | 4 ++-- primer/test/Tests/Prelude/Polymorphism.hs | 2 +- primer/test/Tests/Prelude/Utils.hs | 4 ++-- primer/test/Tests/Shadowing.hs | 4 ++-- 10 files changed, 24 insertions(+), 24 deletions(-) rename primer/src/Primer/{EvalFull.hs => EvalFullStep.hs} (99%) rename primer/test/Tests/{EvalFull.hs => EvalFullStep.hs} (99%) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index a5bbb47bc..0e42a7843 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -240,7 +240,7 @@ import Primer.Def ( import Primer.Def qualified as Def import Primer.Eval (NormalOrderOptions (StopAtBinders)) import Primer.Eval.Redex (Dir (Chk), EvalLog) -import Primer.EvalFull (TerminationBound) +import Primer.EvalFullStep (TerminationBound) import Primer.JSON ( CustomJSON (..), FromJSON, diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs index 0a3c6d7b6..99a42ead4 100644 --- a/primer-benchmark/src/Benchmarks.hs +++ b/primer-benchmark/src/Benchmarks.hs @@ -25,7 +25,7 @@ import Primer.Eval ( RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets), ) -import Primer.EvalFull ( +import Primer.EvalFullStep ( Dir (Syn), EvalLog, evalFull, @@ -79,17 +79,17 @@ benchmarks = "evalTestM" [ Group "pure logs" - [ benchExpectedPureLogs (mapEvenEnv 1) "mapEven 1" 100 - , benchExpectedPureLogs (mapEvenEnv 10) "mapEven 10" 1000 + [ benchExpectedPureLogsStep (mapEvenEnv 1) "mapEven 1" 100 + , benchExpectedPureLogsStep (mapEvenEnv 10) "mapEven 10" 1000 -- This benchmark is too slow to be practical for CI. - -- , benchExpectedPureLogs (mapEvenEnv 100) "mapEven 100" 10000 + -- , benchExpectedPureLogsStep (mapEvenEnv 100) "mapEven 100" 10000 ] , Group "discard logs" - [ benchExpectedDiscardLogs (mapEvenEnv 1) "mapEven 1" 100 - , benchExpectedDiscardLogs (mapEvenEnv 10) "mapEven 10" 1000 + [ benchExpectedDiscardLogsStep (mapEvenEnv 1) "mapEven 1" 100 + , benchExpectedDiscardLogsStep (mapEvenEnv 10) "mapEven 10" 1000 -- This benchmark is too slow to be practical for CI. - -- , benchExpectedDiscardLogs (mapEvenEnv 100) "mapEven 100" 10000 + -- , benchExpectedDiscardLogsStep (mapEvenEnv 100) "mapEven 100" 10000 ] ] , Group @@ -106,11 +106,11 @@ benchmarks = evalOptionsN = UnderBinders evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False} evalOptionsR = RunRedexOptions{pushAndElide = True} - evalTestMPureLogs e maxEvals = + evalTestMPureLogsStep e maxEvals = evalTestM (maxID e) $ runPureLogT $ evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) - evalTestMDiscardLogs e maxEvals = + evalTestMDiscardLogsStep e maxEvals = evalTestM (maxID e) $ runDiscardLogT $ evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) @@ -121,8 +121,8 @@ benchmarks = b (pure $ (@?= Right (zeroIDs $ expectedResult e')) . fmap zeroIDs . g) - benchExpectedPureLogs = benchExpected evalTestMPureLogs fst - benchExpectedDiscardLogs = benchExpected evalTestMDiscardLogs identity + benchExpectedPureLogsStep = benchExpected evalTestMPureLogsStep fst + benchExpectedDiscardLogsStep = benchExpected evalTestMDiscardLogsStep identity tcTest id = evalTestM id . runExceptT @TypeError . tcWholeProgWithImports diff --git a/primer/primer.cabal b/primer/primer.cabal index dfb2a17c5..a1d7cd38e 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -33,7 +33,7 @@ library Primer.Def.Utils Primer.Eval Primer.Eval.Redex - Primer.EvalFull + Primer.EvalFullStep Primer.Examples Primer.JSON Primer.Log @@ -216,7 +216,7 @@ test-suite primer-test Tests.Database Tests.Eval Tests.Eval.Utils - Tests.EvalFull + Tests.EvalFullStep Tests.Examples Tests.FreeVars Tests.Gen.App diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 35b3c7a11..91149bd58 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -202,7 +202,7 @@ import Primer.Eval (AvoidShadowing (AvoidShadowing)) import Primer.Eval qualified as Eval import Primer.Eval.Detail (EvalDetail) import Primer.Eval.Redex (EvalLog, RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, groupedLets)) -import Primer.EvalFull (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull) +import Primer.EvalFullStep (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull) import Primer.JSON import Primer.Log (ConvertLogMessage) import Primer.Module ( diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFullStep.hs similarity index 99% rename from primer/src/Primer/EvalFull.hs rename to primer/src/Primer/EvalFullStep.hs index fdc7fd7bc..b826d6b4b 100644 --- a/primer/src/Primer/EvalFull.hs +++ b/primer/src/Primer/EvalFullStep.hs @@ -1,4 +1,4 @@ -module Primer.EvalFull ( +module Primer.EvalFullStep ( Dir (..), EvalFullError (..), TerminationBound, diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 266d5ee9b..e88159340 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -155,7 +155,7 @@ import Primer.Def ( defAST, ) import Primer.Eval (EvalError (NotRedex), NormalOrderOptions (StopAtBinders, UnderBinders)) -import Primer.EvalFull (Dir (Chk)) +import Primer.EvalFullStep (Dir (Chk)) import Primer.Examples (comprehensiveWellTyped) import Primer.Gen.App (genApp) import Primer.Gen.Core.Raw (genName) diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFullStep.hs similarity index 99% rename from primer/test/Tests/EvalFull.hs rename to primer/test/Tests/EvalFullStep.hs index 6d76e9be3..467ce9dc3 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFullStep.hs @@ -1,4 +1,4 @@ -module Tests.EvalFull where +module Tests.EvalFullStep where import Foreword hiding (unlines) @@ -46,7 +46,7 @@ import Primer.Core.Utils ( ) import Primer.Def (DefMap) import Primer.Eval -import Primer.EvalFull +import Primer.EvalFullStep import Primer.Examples qualified as Examples ( even, map, diff --git a/primer/test/Tests/Prelude/Polymorphism.hs b/primer/test/Tests/Prelude/Polymorphism.hs index 552c49048..a8772af99 100644 --- a/primer/test/Tests/Prelude/Polymorphism.hs +++ b/primer/test/Tests/Prelude/Polymorphism.hs @@ -39,7 +39,7 @@ import Tasty (Property, property) import Test.Tasty.HUnit ( Assertion, ) -import Tests.EvalFull ((<~==>)) +import Tests.EvalFullStep ((<~==>)) import Tests.Prelude.Utils (functionOutput', (<===>)) tasty_id_prop :: Property diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs index fb73cd7e5..c31e7867d 100644 --- a/primer/test/Tests/Prelude/Utils.hs +++ b/primer/test/Tests/Prelude/Utils.hs @@ -12,14 +12,14 @@ import Primer.Eval ( RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets), ) -import Primer.EvalFull (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull) +import Primer.EvalFullStep (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull) import Primer.Log (runPureLogT) import Primer.Module (builtinModule, moduleDefsQualified, moduleTypesQualified, primitiveModule) import Primer.Prelude (prelude) import Primer.Pretty (prettyExpr, sparse) import Primer.Test.TestM (TestM, evalTestM) import Primer.Test.Util (isSevereLog, zeroIDs) -import Tests.EvalFull (evalResultExpr) +import Tests.EvalFullStep (evalResultExpr) import Prelude (error) (<===>) :: (HasCallStack, MonadTest m) => Either EvalFullError Expr -> Either EvalFullError Expr -> m () diff --git a/primer/test/Tests/Shadowing.hs b/primer/test/Tests/Shadowing.hs index 86681f192..14611129e 100644 --- a/primer/test/Tests/Shadowing.hs +++ b/primer/test/Tests/Shadowing.hs @@ -32,7 +32,7 @@ import Primer.Eval ( redexes, step, ) -import Primer.EvalFull (EvalFullError (..), EvalLog, evalFullStepCount) +import Primer.EvalFullStep (EvalFullError (..), EvalLog, evalFullStepCount) import Primer.Gen.App (genApp) import Primer.Gen.Core.Typed (forAllT, propertyWT) import Primer.Log (runPureLog) @@ -57,7 +57,7 @@ import Tasty (Property, withDiscards, withTests) import Test.Tasty.HUnit (Assertion) import Tests.Action.Available (PA (..), genAction, toProgAction) import Tests.Eval.Utils (genDirTm, testModules) -import Tests.EvalFull (evalFullTestAvoidShadowing, (<~==>)) +import Tests.EvalFullStep (evalFullTestAvoidShadowing, (<~==>)) import Tests.Gen.Core.Typed (propertyWTInExtendedGlobalCxt) {- From 844020fbe17bbbd4a8664d67e5b05d6bd5176cb4 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Thu, 30 Nov 2023 14:10:32 +0000 Subject: [PATCH 5/7] refactor: move `freshen` This is to enable reuse in a subsequent commit. Signed-off-by: Ben Price --- primer/gen/Primer/Gen/Core/Typed.hs | 16 ++++------------ primer/src/Primer/Core/Utils.hs | 15 +++++++++++++-- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index ee20cc077..76cb6ed97 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -68,10 +68,10 @@ import Primer.Core ( qualifyName, ) import Primer.Core.DSL (S) -import Primer.Core.Utils (freeVarsTy) +import Primer.Core.Utils (freeVarsTy, freshen) import Primer.Gen.Core.Raw (genLVarName, genModuleName, genName, genTyVarName) import Primer.Module (Module (..)) -import Primer.Name (Name, NameCounter, freshName, unName, unsafeMkName) +import Primer.Name (Name, NameCounter, freshName) import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine) import Primer.Subst (substTy, substTySimul) import Primer.Test.TestM ( @@ -199,24 +199,16 @@ freshTyConNameForCxt = qualifyName <$> genModuleName <*> freshNameForCxt -- the original type variable "foo" by our new term variable "foo". genLVarNameAvoiding :: [TypeG] -> GenT WT LVarName genLVarNameAvoiding ty = - (\vs -> freshen (foldMap' freeVarsTy ty <> foldMap' freeVarsTy vs) 0) + (\vs -> freshen (foldMap' (S.map unLocalName . freeVarsTy) ty <> foldMap' (S.map unLocalName . freeVarsTy) vs)) <$> asks localTmVars <*> genLVarName genTyVarNameAvoiding :: TypeG -> GenT WT TyVarName genTyVarNameAvoiding ty = - (\vs -> freshen (freeVarsTy ty <> foldMap' freeVarsTy vs) 0) + (\vs -> freshen (S.map unLocalName (freeVarsTy ty) <> foldMap' (S.map unLocalName . freeVarsTy) vs)) <$> asks localTmVars <*> genTyVarName -freshen :: Set (LocalName k') -> Int -> LocalName k -> LocalName k -freshen fvs i n = - let suffix = if i > 0 then "_" <> show i else "" - m = LocalName $ unsafeMkName $ unName (unLocalName n) <> suffix - in if m `elem` fvs - then freshen fvs (i + 1) n - else m - -- genSyns T with cxt Γ should generate (e,S) st Γ |- e ∈ S and S ~ T (i.e. same up to holes and alpha) genSyns :: HasCallStack => TypeG -> GenT WT (ExprG, TypeG) genSyns ty = do diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index 49ef8b70b..20be0b715 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -23,6 +23,7 @@ module Primer.Core.Utils ( freeGlobalVars, alphaEqTy, concreteTy, + freshen, ) where import Foreword @@ -57,7 +58,7 @@ import Primer.Core ( HasID (_id), ID, LVarName, - LocalName (unLocalName), + LocalName (LocalName, unLocalName), TmVarRef (GlobalVarRef, LocalVarRef), TyVarName, Type' (..), @@ -86,7 +87,7 @@ import Primer.Core.Type.Utils ( typeIDs, _freeVarsTy, ) -import Primer.Name (Name) +import Primer.Name (Name (unName), unsafeMkName) -- | Regenerate all IDs (including in types and kinds), not changing any other metadata regenerateExprIDs :: (HasID a, HasID b, HasID c, MonadFresh ID m) => Expr' a b c -> m (Expr' a b c) @@ -194,3 +195,13 @@ freeGlobalVars e = S.fromList [v | Var _ (GlobalVarRef v) <- universe e] -- | Traverse the 'ID's in an 'Expr''. exprIDs :: (HasID a, HasID b, HasID c) => Traversal' (Expr' a b c) ID exprIDs = (_exprMeta % _id) `adjoin` (_exprTypeMeta % _id) `adjoin` (_exprKindMeta % _id) + +freshen :: Set Name -> LocalName k -> LocalName k +freshen fvs n = go (0 :: Int) + where + go i = + let suffix = if i > 0 then "_" <> show i else "" + m = LocalName $ unsafeMkName $ unName (unLocalName n) <> suffix + in if unLocalName m `elem` fvs + then go (i + 1) + else m From ab1c54795786e0f288e98caa5552a3d502b98f4a Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 15 Nov 2023 14:48:55 +0000 Subject: [PATCH 6/7] feat: A faster evaluator-to-normal-form This does not iterate the single-step redex evaluator, but instead uses Haskell's runtime to directly interpret primer ASTs. Signed-off-by: Ben Price --- primer-benchmark/src/Benchmarks.hs | 25 +- primer/primer.cabal | 2 + primer/src/Primer/Core.hs | 4 + primer/src/Primer/EvalFullInterp.hs | 437 +++++++++++ primer/test/Tests/EvalFullInterp.hs | 1108 +++++++++++++++++++++++++++ 5 files changed, 1572 insertions(+), 4 deletions(-) create mode 100644 primer/src/Primer/EvalFullInterp.hs create mode 100644 primer/test/Tests/EvalFullInterp.hs diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs index 99a42ead4..4c5f941a8 100644 --- a/primer-benchmark/src/Benchmarks.hs +++ b/primer-benchmark/src/Benchmarks.hs @@ -20,16 +20,17 @@ import Primer.App ( tcWholeProgWithImports, ) import Primer.App.Utils (forgetProgTypecache) +import Primer.Core.Utils (forgetMetadata) import Primer.Eval ( NormalOrderOptions (UnderBinders), RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets), ) +import Primer.EvalFullInterp qualified as EFInterp import Primer.EvalFullStep ( Dir (Syn), - EvalLog, - evalFull, ) +import Primer.EvalFullStep qualified as EFStep import Primer.Examples ( mapOddPrimProg, mapOddProg, @@ -91,6 +92,12 @@ benchmarks = -- This benchmark is too slow to be practical for CI. -- , benchExpectedDiscardLogsStep (mapEvenEnv 100) "mapEven 100" 10000 ] + , Group + "interp (has no logs)" + [ benchExpectedInterp (mapEvenEnv 1) "mapEven 1" Syn + , benchExpectedInterp (mapEvenEnv 10) "mapEven 10" Syn + , benchExpectedInterp (mapEvenEnv 100) "mapEven 100" Syn + ] ] , Group "typecheck" @@ -109,11 +116,13 @@ benchmarks = evalTestMPureLogsStep e maxEvals = evalTestM (maxID e) $ runPureLogT - $ evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + $ EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) evalTestMDiscardLogsStep e maxEvals = evalTestM (maxID e) $ runDiscardLogT - $ evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + $ EFStep.evalFull @EFStep.EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e) + evalTestMInterp e d = + EFInterp.interp' builtinTypes (EFInterp.mkGlobalEnv $ defMap e) d (forgetMetadata $ expr e) benchExpected f g e n b = EnvBench e n $ \e' -> NF @@ -121,8 +130,16 @@ benchmarks = b (pure $ (@?= Right (zeroIDs $ expectedResult e')) . fmap zeroIDs . g) + -- as benchExpected, but 'interp' works on un-metadata'd stuff + benchExpected' f e n b = EnvBench e n $ \e' -> + NF + (f e') + b + (pure (@?= (forgetMetadata $ expectedResult e'))) + benchExpectedPureLogsStep = benchExpected evalTestMPureLogsStep fst benchExpectedDiscardLogsStep = benchExpected evalTestMDiscardLogsStep identity + benchExpectedInterp = benchExpected' evalTestMInterp tcTest id = evalTestM id . runExceptT @TypeError . tcWholeProgWithImports diff --git a/primer/primer.cabal b/primer/primer.cabal index a1d7cd38e..e0aed856d 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -33,6 +33,7 @@ library Primer.Def.Utils Primer.Eval Primer.Eval.Redex + Primer.EvalFullInterp Primer.EvalFullStep Primer.Examples Primer.JSON @@ -216,6 +217,7 @@ test-suite primer-test Tests.Database Tests.Eval Tests.Eval.Utils + Tests.EvalFullInterp Tests.EvalFullStep Tests.Examples Tests.FreeVars diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index c41a055d3..587c619be 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -14,6 +14,7 @@ module Primer.Core ( CaseFallback' (..), caseBranchName, traverseFallback, + mapFallback, module Primer.Core.Meta, module Primer.Core.Type, TypeCache (..), @@ -348,6 +349,9 @@ traverseFallback f = \case CaseExhaustive -> pure CaseExhaustive CaseFallback e -> CaseFallback <$> f e +mapFallback :: (Expr' a b c -> Expr' a' b' c') -> CaseFallback' a b c -> CaseFallback' a' b' c' +mapFallback f = runIdentity . traverseFallback (Identity . f) + -- | Variable bindings -- These are used in case branches to represent the binding of a variable. -- They aren't currently used in lambdas or lets, but in the future that may change. diff --git a/primer/src/Primer/EvalFullInterp.hs b/primer/src/Primer/EvalFullInterp.hs new file mode 100644 index 000000000..df576f2fc --- /dev/null +++ b/primer/src/Primer/EvalFullInterp.hs @@ -0,0 +1,437 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE ViewPatterns #-} + +module Primer.EvalFullInterp ( + interp, + Timeout (MicroSec), + interp', + InterpError (..), + Dir (..), + mkEnv, + mkGlobalEnv, +) where + +import Foreword + +import Control.Exception (throw) +import Data.Map.Lazy qualified as Map +import Data.Set qualified as Set +import Primer.Core ( + Bind' (Bind), + CaseBranch' (CaseBranch), + CaseFallback' (CaseFallback), + Expr' (..), + GVarName, + LVarName, + LocalName, + Pattern (PatCon, PatPrim), + PrimCon, + TmVarRef (GlobalVarRef, LocalVarRef), + TyConName, + TyVarName, + Type' (..), + ValConName, + bindName, + caseBranchName, + mapFallback, + unLocalName, + ) +import Primer.Core.DSL.Meta (create') +import Primer.Core.Transform (decomposeTAppCon, unfoldApp) +import Primer.Core.Utils ( + concreteTy, + forgetMetadata, + forgetTypeMetadata, + freeVars, + freeVarsTy, + freshen, + ) +import Primer.Def (ASTDef (ASTDef), Def (DefAST, DefPrim), DefMap) +import Primer.Eval.Redex ( + Dir (Chk, Syn), + ) +import Primer.Name (Name) +import Primer.Primitives (primConName, primFunDef) +import Primer.Primitives.PrimDef (PrimDef) +import Primer.TypeDef ( + ASTTypeDef (ASTTypeDef), + TypeDef (TypeDefAST), + TypeDefMap, + ValCon (valConArgs, valConName), + ) +import System.Timeout (timeout) + +-- Invariant: vars is the set of free vars in the values of the map +-- Thus the binders we need to rename before going under them. +-- Invariant: the values in the env will be in normal form. +data EnvTm = EnvTm + { vars :: Set Name + , env :: Map.Map (Either GVarName LVarName) (Expr' () () ()) + , prims :: Map GVarName PrimDef + } +data EnvTy = EnvTy + { vars :: Set Name + , env :: Map.Map TyVarName (Type' () ()) + } + +-- | Convert an environment into the form needed for 'interp' +mkEnv :: + [(Either GVarName LVarName, Expr' a b c)] -> + Map GVarName PrimDef -> + [(TyVarName, Type' a b)] -> + (EnvTm, EnvTy) +mkEnv tms prims tys = + extendTmsEnv + (second forgetMetadata <$> tms) + ( EnvTm mempty mempty prims + , extendTysEnv' (second forgetTypeMetadata <$> tys) $ EnvTy mempty mempty + ) + +-- | Convert an environment into the form needed for 'interp' +mkGlobalEnv :: DefMap -> (EnvTm, EnvTy) +mkGlobalEnv defs = + mkEnv + ( mapMaybe + ( \(f, d) -> case d of + DefAST (ASTDef tm ty) -> Just (Left f, Ann () (forgetMetadata tm) (forgetTypeMetadata ty)) + _ -> Nothing + ) + $ Map.assocs defs + ) + ( Map.mapMaybe + ( \case + DefPrim p -> Just p + _ -> Nothing + ) + defs + ) + mempty + +data InterpError + = Timeout + | NoBranch (Either ValConName PrimCon) [Pattern] + | UnknownTyCon TyConName + | UnknownValCon TyConName ValConName + deriving stock (Eq, Show) + deriving anyclass (Exception) + +newtype Timeout = MicroSec Int + +-- | Wrap the interpreter in a IO-based timeout, and catch 'InterpError' exceptions +interp :: + Timeout -> + TypeDefMap -> + (EnvTm, EnvTy) -> + Dir -> + Expr' () () () -> + IO (Either InterpError (Expr' () () ())) +interp (MicroSec t) tydefs env dir e = do + e' <- timeout t (try $ evaluate $ force $ interp' tydefs env dir e) + pure $ case e' of + Nothing -> Left Timeout + Just e'' -> e'' + +{- HLINT ignore interp' "Avoid restricted function" -} +-- (we are intentionally using 'throw' here + +-- | A somewhat-efficient interpreter for primer terms. +-- +-- We fully evaluate the term, including under lambdas and +-- 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'. +-- +-- Warnings: +-- - Trying to evaluate a divergent term will (unsurprisingly) not terminate, +-- and may consume a lot of memory. +-- - We 'throw' IO-based exceptions of type 'InterpError' for obvious issues +-- in case expressions (though this will not happen with well-typed +-- terms). This function will not throw 'Timeout' (that will only be +-- thrown by the 'interp' wrapper). +-- - To avoid these pitfalls, consider using 'interp', which limits runtime +-- with 'timeout', and catches exceptions. +-- +-- The interpreter is designed to be fairly simple, and to stay in the +-- AST domain, but it does rely on subtle laziness properties (see below). +-- We attempt to make it reasonably fast, given the constraint of simplicity, +-- and maximally terminating. We evaluate terms in some environment of local +-- bindings, which enables us to share computation in @let x= +-- in f x x@ in a call-by-need fashion. This is accomplished by the +-- environment being a mapping of variable names to normal forms which +-- are computed lazily. The laziness is also used to avoid looping on +-- diverging subterms which do not need to be fully-evaluated, for example +-- in @head (letrec l=Cons True l in l)@, which should swiftly reduce +-- to @True@. Another somewhat-common source of diverging-but-productive +-- subterms are local recursive helper functions (since we evaluate under +-- lambdas and inside let bindings). +-- +-- We have made the design choice to use imprecise exceptions to be able to +-- write simple code which can report obvious problems without compromising +-- laziness. Another choice would be to not report errors (and letting these +-- subterms be stuck). A non-option would be to use ExceptT to report errors, +-- since that would destroy our critical laziness properties: the monadic +-- bind would force the top Left/Right constructor, and that in turn would +-- force the full evaluation of the relevant subterms. This design choice +-- unfortunately precludes returning a partial result if we detect we have +-- been evaluating for too long (it is possible to add a recursion depth +-- limit and bail out if we hit it (though then evaluating recursive lets +-- is less efficient), but we cannot easily then both report we timed out +-- and also rebuild the whole term. Finding a smarter design that would +-- allow this may be interesting future work. +-- +-- The laziness property we rely on is that where possible we return the +-- root node of an AST without forcing the evaluation of subterms. This +-- makes it possible to pattern match on recursive calls to 'interp'' without +-- incurring unbounded work. Note that this means we cannot make our 'Expr' +-- type spine-strict without refactoring this interpreter! +interp' :: + TypeDefMap -> + (EnvTm, EnvTy) -> + Dir -> + Expr' () () () -> + Expr' () () () +interp' tydefs env@(envTm, envTy) dir = \case + Hole m e -> Hole m $ interp' tydefs env Syn e + e@EmptyHole{} -> e + Ann _ e t -> ann dir (interp' tydefs env Chk e) (interpTy envTy t) + -- NB: for primitives, we attempt to reduce them + -- - with unevaluated arguments + -- - then with the first argument evaluated + -- - then with the first two arguments evaluated + -- - etc + -- and we do not assume the result of a primitive will be in normal form. + -- This means that we support lazy primitives. + -- Note that this left-to-right order of argument evaluation is the + -- same as EvalFullStep + e@App{} + -- The @upsilon Chk@ is a bit of a lie -- we are not really in a checkable + -- position. We simply wish to remove annotations around a primitive function's name + | (upsilon Chk . interp' tydefs env Syn -> Var _ (GlobalVarRef name), args) <- unfoldApp e + , Just r <- getFirst $ foldMap' (First . tryPrimFun' name envTm.prims) (evalPrefixes tydefs env args) -> + interp' tydefs env dir r + App _ f s -> case interp' tydefs env Syn f of + Ann _ (Lam _ v t) (TFun _ src tgt) -> + ann dir (interp' tydefs (extendTmsEnv [(Right v, Ann () (interp' tydefs env Chk s) src)] env) Chk t) tgt + f' -> App () f' $ interp' tydefs env Chk s + APP _ f s -> case interp' tydefs env Syn f of + Ann _ (LAM _ a t) (TForall _ b _ ty) -> + let s' = interpTy envTy s + in ann + dir + (interp' tydefs (extendTyEnv a s' env) Chk t) + (interpTy (extendTyEnv' b s' envTy) ty) + f' -> APP () f' (interpTy envTy s) + Con m c ts -> Con m c $ map (interp' tydefs env Chk) ts + Lam _ v t -> let v' = freshLike v env in Lam () v' $ interp' tydefs (renameTmEnv v v' env) Chk t + -- NB: we must evaluate under lambdas (given the rest of our interpretation strategy). + -- Consider @(λx.(λy.x) : A -> B -> A) s t@ we will + -- interp' @λy.x@ in context where @x:->t@, and this is the only time we have @x@ in the context! + LAM _ v t -> let v' = freshLike v env in LAM () v' $ interp' tydefs (extendTyEnv v (TVar () v') env) Chk t + Var _ (LocalVarRef v) -> upsilon dir $ envTm.env ! Right v -- recall the environment is in normal form + Var _ (GlobalVarRef v) -> upsilon dir $ envTm.env ! Left v -- recall the environment is in normal form + Let _ v e b -> interp' tydefs (extendTmEnv (Right v) (interp' tydefs env Syn e) env) dir b + LetType _ v t b -> interp' tydefs (extendTyEnv v (interpTy envTy t) env) dir b + -- this interpretation af letrec can easily cause deadlocked or infinite-size programs + -- and can't be detected but has advantage of being lazy and having sharing + Letrec _ v e t b -> + let e' = interp' tydefs env' Chk e + env' = + extendTmEnvWithFVs + (Right v) + (Ann () e' $ interpTy envTy t) + (Set.delete (unLocalName v) $ freeVars (Ann () e t)) + env + in interp' tydefs env' dir b + -- In step interpreter, case which does not discriminate is lazy. Same here for consistency. + Case _ _ [] (CaseFallback e) -> interp' tydefs env Chk e + Case _ e brs fb -> + -- recall @case C as : T A of ... ; C xs -> e ; ...@ steps to + -- @let xs=as:(lettype p=A in S) in e@ for @data T p = C S@ + case interp' tydefs env Syn e of + Ann _ (Con _ c as) (decomposeTAppCon -> Just (tycon, tyargs)) + | Just (CaseBranch _ xs t) <- find ((PatCon c ==) . caseBranchName) brs -> + let envTy' = extendTysEnv' (tyParamEnvExt tycon tyargs) envTy + in interp' + tydefs + ( extendTmsEnv + ( zip (Right . bindName <$> xs) + $ zipWith (\a argTy -> Ann () a $ interpTy envTy' argTy) as + $ ctorArgTys tycon c + ) + env + ) + Chk + t + | CaseFallback t <- fb -> interp' tydefs env Chk t + | otherwise -> throw $ NoBranch (Left c) $ caseBranchName <$> brs + -- Note that primitives never have Expr arguments + -- i.e. are always atomic + Ann _ (PrimCon _ c) (TCon _ ((== primConName c) -> True)) + | Just (CaseBranch _ [] t) <- find ((PatPrim c ==) . caseBranchName) brs -> interp' tydefs env Chk t + | CaseFallback t <- fb -> interp' tydefs env Chk t + | otherwise -> throw $ NoBranch (Right c) $ caseBranchName <$> brs + -- literals (primitive constructors) are actually synthesisable, so may come + -- without annotations + PrimCon _ c + | Just (CaseBranch _ [] t) <- find ((PatPrim c ==) . caseBranchName) brs -> interp' tydefs env Chk t + | CaseFallback t <- fb -> interp' tydefs env Chk t + | otherwise -> throw $ NoBranch (Right c) $ caseBranchName <$> brs + e' -> + let f = \case + CaseBranch pat binds rhs -> + let (env', binds') = + mapAccumL + (\env'' (bindName -> b) -> let b' = freshLike b env'' in (renameTmEnv b b' env'', Bind () b')) + env + binds + in CaseBranch pat binds' $ interp' tydefs env' Chk rhs + in Case () e' (f <$> brs) (mapFallback (interp' tydefs env Chk) fb) + e@PrimCon{} -> e + where + tyParamEnvExt tcon args = case Map.lookup tcon tydefs of + Just (TypeDefAST (ASTTypeDef ps _ _)) -> zipWith (\(p, _) a -> (p, a)) ps args + _ -> throw $ UnknownTyCon tcon + ctorArgTys tcon vcon = case Map.lookup tcon tydefs of + Just (TypeDefAST (ASTTypeDef _ as _)) -> + case find ((== vcon) . valConName) as of + Just vc -> valConArgs vc + Nothing -> throw $ UnknownValCon tcon vcon + _ -> throw $ UnknownTyCon tcon + ann d e t = upsilon d $ Ann () e t + -- Strip redundant annotations (recursively): we don't need a + -- top-level annotation if we are in a checkable context (at least if + -- the type is "concrete", else it could act as type-changing cast). + upsilon d = \case + Ann _ e t -> + -- We force t before emitting anything, so this is not very lazy. + -- However we know evaluation of types must terminate! + case (d, concreteTy t) of + (Chk, True) -> upsilon d e + _ -> Ann () e t + e -> e + renameTmEnv v v' = extendTmEnv (Right v) (Var () $ LocalVarRef v') + +-- Generate a fresh name (for a given context) similar to an existing name. +freshLike :: LocalName k -> (EnvTm, EnvTy) -> LocalName k +freshLike v (envTm, envTy) = + let avoid = + envTm.vars + <> envTy.vars + <> Set.delete + (unLocalName v) + ( Set.fromList (fmap unLocalName $ rights $ Map.keys envTm.env) + <> Set.map unLocalName (Map.keysSet envTy.env) + ) + in freshen avoid v + +freshLikeTy :: LocalName k -> EnvTy -> LocalName k +freshLikeTy v env = freshLike v (EnvTm mempty mempty mempty, env) + +interpTy :: EnvTy -> Type' () () -> Type' () () +interpTy env = \case + t@TEmptyHole{} -> t + THole _ t -> THole () $ interpTy env t + t@TCon{} -> t + TFun _ s t -> TFun () (interpTy env s) (interpTy env t) + TVar _ v -> env.env !! v + TApp _ s t -> TApp () (interpTy env s) (interpTy env t) + TForall _ v k t -> + let v' = freshLikeTy v env + in TForall () v' k (interpTy (extendTyEnv' v (TVar () v') env) t) + TLet _ v s t -> interpTy (extendTyEnv' v s env) t + +extendTmEnv :: + Either GVarName LVarName -> + Expr' () () () -> + (EnvTm, EnvTy) -> + (EnvTm, EnvTy) +extendTmEnv k v = extendTmsEnv [(k, v)] + +extendTmEnvWithFVs :: + Either GVarName LVarName -> + Expr' () () () -> + Set Name -> + (EnvTm, EnvTy) -> + (EnvTm, EnvTy) +extendTmEnvWithFVs k v fvs = extendTmsEnvWithFVs [(k, v, fvs)] + +extendTmsEnv :: + [(Either GVarName LVarName, Expr' () () ())] -> + (EnvTm, EnvTy) -> + (EnvTm, EnvTy) +extendTmsEnv tms = extendTmsEnvWithFVs $ (\(v, t) -> (v, t, freeVars t)) <$> tms + +extendTmsEnvWithFVs :: + [(Either GVarName LVarName, Expr' () () (), Set Name)] -> + (EnvTm, EnvTy) -> + (EnvTm, EnvTy) +extendTmsEnvWithFVs tms (envTm, envTy) = + ( EnvTm + { vars = envTm.vars <> Set.unions ((\(_, _, fvs) -> fvs) <$> tms) + , env = Map.fromList ((\(x, y, _) -> (x, y)) <$> tms) <> envTm.env + , prims = envTm.prims + } + , envTy + ) + +extendTyEnv' :: + TyVarName -> + Type' () () -> + EnvTy -> + EnvTy +extendTyEnv' k v = extendTysEnv' [(k, v)] + +extendTysEnv' :: + [(TyVarName, Type' () ())] -> + EnvTy -> + EnvTy +extendTysEnv' tys EnvTy{vars, env} = + EnvTy + { vars = vars <> Set.unions (map (Set.map unLocalName . freeVarsTy . snd) tys) + , env = Map.fromList tys <> env + } + +extendTyEnv :: + TyVarName -> + Type' () () -> + (EnvTm, EnvTy) -> + (EnvTm, EnvTy) +extendTyEnv k v (envTm, envTy) = (envTm, extendTyEnv' k v envTy) + +(!) :: Map.Map (Either GVarName LVarName) (Expr' () () ()) -> Either GVarName LVarName -> Expr' () () () +m ! k = case Map.lookup k m of + Just v -> v + Nothing -> case k of + Left v -> Var () $ GlobalVarRef v + Right v -> Var () $ LocalVarRef v + +(!!) :: Map.Map TyVarName (Type' () ()) -> TyVarName -> Type' () () +m !! k = case Map.lookup k m of + Just v -> v + Nothing -> TVar () k + +-- This is an ugly hack: we don't care about the IDs, but the underlying +-- primitives always return an ID-ful expression, or rather a monadic +-- computation to create an ID-ful expression, in an arbitrary +-- @MonadFresh ID@ monad. We will simply generate nonsense IDs and forget +-- them. +tryPrimFun' :: GVarName -> Map GVarName PrimDef -> [Expr' () () ()] -> Maybe (Expr' () () ()) +tryPrimFun' p ps as = do + d <- Map.lookup p ps + case primFunDef d as of + Left _ -> Nothing + Right res -> Just $ forgetMetadata $ create' res + +evalPrefixes :: + TypeDefMap -> + (EnvTm, EnvTy) -> + [Expr' () () ()] -> + [[Expr' () () ()]] +evalPrefixes tydefs env = map (uncurry (++)) . mapPrefixes (interp' tydefs env Chk) + +mapPrefixes :: (a -> b) -> [a] -> [([b], [a])] +mapPrefixes f = \case + [] -> [([], [])] + a : as -> ([], a : as) : map (first (f a :)) (mapPrefixes f as) diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs new file mode 100644 index 000000000..2ef46e0fe --- /dev/null +++ b/primer/test/Tests/EvalFullInterp.hs @@ -0,0 +1,1108 @@ +{-# LANGUAGE ViewPatterns #-} + +-- TODO: DRY with EvalFullStep tests +-- (This is copy-and-pasted from those tests with some tests dropped, in +-- particular we cannot test intermediate results. It was then hacked +-- to compile (mostly due to interp only working with empty metadata). +-- Finally, a few tests were added.) +module Tests.EvalFullInterp where + +import Foreword hiding (unlines) + +import Data.Map qualified as M +import Hedgehog hiding (Property, Var, check, property, test, withDiscards, withTests) +import Hedgehog.Gen qualified as Gen +import Hedgehog.Internal.Property (LabelName (LabelName)) +import Hedgehog.Range qualified as Range +import Primer.Builtins ( + cCons, + cFalse, + cJust, + cMakePair, + cNothing, + cSucc, + cTrue, + cZero, + tBool, + tList, + tMaybe, + tNat, + tPair, + ) +import Primer.Builtins.DSL (boolAnn, bool_, list_, nat) +import Primer.Core +import Primer.Core.DSL +import Primer.Core.Utils ( + forgetMetadata, + generateIDs, + ) +import Primer.Def (DefMap) +import Primer.Eval +import Primer.EvalFullInterp (InterpError (..), Timeout (MicroSec), interp, mkGlobalEnv) +import Primer.Examples qualified as Examples ( + even, + map, + map', + odd, + ) +import Primer.Gen.Core.Typed (forAllT, propertyWT) +import Primer.Module ( + builtinTypes, + moduleDefsQualified, + ) +import Primer.Primitives ( + PrimDef ( + EqChar, + HexToNat, + IntAdd, + IntEq, + IntFromNat, + IntGT, + IntGTE, + IntLT, + IntLTE, + IntMinus, + IntMul, + IntNeq, + IntQuot, + IntQuotient, + IntRem, + IntRemainder, + IntToNat, + IsSpace, + NatToHex, + PrimConst, + ToUpper + ), + tChar, + tInt, + ) +import Primer.Primitives.DSL (pfun) +import Primer.Test.Expected ( + Expected (defMap, expectedResult, expr), + mapEven, + ) +import Primer.Test.Util ( + primDefs, + ) +import Primer.TypeDef (TypeDefMap) +import Primer.Typecheck ( + typeDefs, + ) +import Tasty ( + Property, + property, + withDiscards, + withTests, + ) +import Test.Tasty.HUnit (Assertion, (@?=)) +import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules) +import Tests.Gen.Core.Typed (checkTest) + +unit_throw_no_branch :: Assertion +unit_throw_no_branch = + let e = create1 $ case_ (con0 cTrue `ann` tcon tBool) [branch cFalse [] emptyHole] + in do + s <- evalFullTest builtinTypes mempty Chk e + s @?= Left (NoBranch (Left cTrue) [PatCon cFalse]) + +unit_1 :: Assertion +unit_1 = + let e = create1 emptyHole + in do + s <- evalFullTest' (MicroSec 0) mempty mempty Syn e + s @?= Left Timeout + +unit_2 :: Assertion +unit_2 = + let e = create1 emptyHole + in do + s <- evalFullTest mempty mempty Syn e + s @?= Right e + +-- Check we don't have shadowing issues in types +unit_3 :: Assertion +unit_3 = + let (expr, expected) = create2 $ do + e <- letType "a" (tvar "b") $ emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "a" `tapp` tforall "a" ktype (tvar "a") `tapp` tforall "b" ktype (tcon' ["M"] "S" `tapp` tvar "a" `tapp` tvar "b")) + let b' = "b_1" + expect <- emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "b" `tapp` tforall "a" ktype (tvar "a") `tapp` tforall b' ktype (tcon' ["M"] "S" `tapp` tvar "b" `tapp` tvar b')) + pure (e, expect) + in do + s <- evalFullTest mempty mempty Syn expr + s @?= Right expected + +-- Check we don't have shadowing issues in terms +unit_4 :: Assertion +unit_4 = + let (expr, expected) = create2 $ do + e <- let_ "a" (lvar "b") $ con' ["M"] "C" [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [lvar "a", lvar "b"])] + let b' = "b_1" + expect <- con' ["M"] "C" [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [lvar "b", lvar b'])] + pure (e, expect) + in do + s <- evalFullTest mempty mempty Syn expr + s @?= Right expected + +unit_5 :: Assertion +unit_5 = + let e = forgetMetadata $ create' $ letrec "x" (lvar "x") (tcon tBool) (lvar "x") + in do + s <- evalFullTest' (MicroSec 10_000) mempty mempty Syn e + s @?= Left Timeout + +unit_6 :: Assertion +unit_6 = + let (e, expt) = create2 $ do + tr <- con0 cTrue + an <- ann (pure tr) (tcon tBool) + pure (an, tr) + in do + s <- evalFullTest mempty mempty Syn e + s @?= Right e + t <- evalFullTest mempty mempty Chk e + t @?= Right expt + +unit_7 :: Assertion +unit_7 = + let e = create1 $ do + let l = lam "x" $ lvar "x" `app` lvar "x" + (l `ann` tEmptyHole) `app` l + in do + s <- evalFullTest mempty mempty Syn e + s @?= Right e + +unit_8 :: Assertion +unit_8 = + let n = 10 + e = mapEven n + in do + s <- evalFullTest builtinTypes (defMap e) Syn (forgetMetadata $ expr e) + s @?= Right (forgetMetadata $ expectedResult e) + +-- A worker/wrapper'd map +unit_9 :: Assertion +unit_9 = + let n = 10 + modName = mkSimpleModuleName "TestModule" + (globals, forgetMetadata -> e, forgetMetadata -> expected) = create' $ do + (mapName, mapDef) <- Examples.map' modName + (evenName, evenDef) <- Examples.even modName + (oddName, oddDef) <- Examples.odd modName + let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero) + expr <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` gvar evenName `app` lst + let globs = [(mapName, mapDef), (evenName, evenDef), (oddName, oddDef)] + expect <- list_ (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool) + pure (globs, expr, expect) + in do + s <- evalFullTest builtinTypes (M.fromList globals) Syn e + s @?= Right expected + +-- A case redex must have an scrutinee which is an annotated constructor. +-- Plain constructors are not well-typed here, for bidirectionality reasons, +-- although they just fail to reduce rather than the evaluator throwing a type error. +unit_10 :: Assertion +unit_10 = + let (s, t, expected) = create3 $ do + annCase <- + case_ + (con0 cZero `ann` tcon tNat) + [ branch cZero [] $ con0 cTrue + , branch cSucc [("n", Nothing)] $ con0 cFalse + ] + noannCase <- + case_ + (con0 cZero) + [ branch cZero [] $ con0 cTrue + , branch cSucc [("n", Nothing)] $ con0 cFalse + ] + expect <- con0 cTrue + pure (annCase, noannCase, expect) + in do + s' <- evalFullTest builtinTypes mempty Syn s + s' @?= Right expected + t' <- evalFullTest builtinTypes mempty Syn t + t' @?= Right t + +unit_11 :: Assertion +unit_11 = + let modName = mkSimpleModuleName "TestModule" + (globals, forgetMetadata -> e, forgetMetadata -> expected) = create' $ do + (evenName, evenDef) <- Examples.even modName + (oddName, oddDef) <- Examples.odd modName + let ty = tcon tNat `tfun` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) + let expr1 = + let_ "x" (con0 cZero) + $ lam "n" (con cMakePair [gvar evenName `app` lvar "n", lvar "x"]) + `ann` ty + expr <- expr1 `app` con0 cZero + let globs = [(evenName, evenDef), (oddName, oddDef)] + expect <- + con cMakePair [con0 cTrue, con0 cZero] + `ann` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat) + pure (globs, expr, expect) + in do + s <- evalFullTest builtinTypes (M.fromList globals) Syn e + s @?= Right expected + +unit_12 :: Assertion +unit_12 = + let (e, expected) = create2 $ do + -- 'f' is a bit silly here, but could just as well be a definition of 'even' + let f = + lam "x" + $ case_ + (lvar "x") + [ branch cZero [] $ con0 cTrue + , branch cSucc [("i", Nothing)] $ lvar "f" `app` lvar "i" + ] + expr <- let_ "n" (con0 cZero) $ letrec "f" f (tcon tNat `tfun` tcon tBool) $ lvar "f" `app` lvar "n" + expect <- con0 cTrue `ann` tcon tBool + pure (expr, expect) + in do + s <- evalFullTest builtinTypes mempty Syn e + s @?= Right expected + +unit_13 :: Assertion +unit_13 = + let (e, expected) = create2 $ do + expr <- (lam "x" (con' ["M"] "C" [lvar "x", let_ "x" (con0 cTrue) (lvar "x"), lvar "x"]) `ann` (tcon tNat `tfun` tcon tBool)) `app` con0 cZero + expect <- con' ["M"] "C" [con0 cZero, con0 cTrue, con0 cZero] `ann` tcon tBool + pure (expr, expect) + in do + s <- evalFullTest builtinTypes mempty Syn e + s @?= Right expected + +unit_14 :: Assertion +unit_14 = + let (e, expected) = create2 $ do + expr <- (lam "x" (lam "x" $ lvar "x") `ann` (tcon tBool `tfun` (tcon tNat `tfun` tcon tNat))) `app` con0 cTrue `app` con0 cZero + expect <- con0 cZero `ann` tcon tNat + pure (expr, expect) + in do + s <- evalFullTest builtinTypes mempty Syn e + s @?= Right expected + +unit_15 :: Assertion +unit_15 = + let (expr, expected) = create2 $ do + let l = let_ "x" (lvar "y") + let c a b = con' ["M"] "C" [a, b] + e0 <- l $ lam "y" $ c (lvar "x") (lvar "y") + let y' = "y_1" + e5 <- lam y' $ c (lvar "y") (lvar y') + pure (e0, e5) + in do + s <- evalFullTest builtinTypes mempty Syn expr + s @?= Right expected + +unit_map_hole :: Assertion +unit_map_hole = + let n = 3 + modName = mkSimpleModuleName "TestModule" + (globals, forgetMetadata -> expr, forgetMetadata -> expected) = create' $ do + (mapName, mapDef) <- Examples.map modName + let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero) + e <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` emptyHole `app` lst + let globs = [(mapName, mapDef)] + expect <- list_ (take n $ ((emptyHole `ann` (tcon tNat `tfun` tcon tBool)) `app`) <$> iterate (con1 cSucc) (con0 cZero)) `ann` (tcon tList `tapp` tcon tBool) + pure (M.fromList globs, e, expect) + in do + sO <- evalFullTest builtinTypes globals Syn expr + sO @?= Right expected + +unit_hole_ann_case :: Assertion +unit_hole_ann_case = + let tm = create1 $ hole $ ann (case_ emptyHole []) (tcon tBool) + in do + t <- evalFullTest builtinTypes mempty Chk tm + t @?= Right tm + +-- Check we don't have variable capture in +-- let x = y in case ? of C x -> x ; D y -> x +unit_case_let_capture :: Assertion +unit_case_let_capture = + let (expr, expected) = create2 $ do + let l = let_ "x" (lvar "y") + e0 <- + l + $ case_ + emptyHole + [ branch' (["M"], "C") [("x", Nothing)] (lvar "x") + , branch' (["M"], "D") [("y", Nothing)] (lvar "x") + ] + e6 <- + case_ + emptyHole + [ branch' (["M"], "C") [("x", Nothing)] (lvar "x") + , branch' (["M"], "D") [("y_1", Nothing)] (lvar "y") + ] + pure (e0, e6) + in do + s <- evalFullTest builtinTypes mempty Syn expr + s @?= Right expected + +-- tlet x = C in D x x +-- ==> +-- D C C +unit_tlet :: Assertion +unit_tlet = + let (expr, expected) = create2 $ do + e0 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tvar "x" `tapp` tvar "x") + e4 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C" + pure (e0, e4) + in do + r <- evalFullTest mempty mempty Syn expr + r @?= Right expected + +-- tlet x = C in ty ==> ty when x not occur free in ty +unit_tlet_elide :: Assertion +unit_tlet_elide = do + let (expr, expected) = create2 $ do + e0 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D") + e1 <- ann emptyHole $ tcon' ["M"] "D" + pure (e0, e1) + in do + r <- evalFullTest mempty mempty Syn expr + r @?= Right expected + +-- tlet x = x in x +-- x +unit_tlet_self_capture :: Assertion +unit_tlet_self_capture = do + let (expr, expected) = create2 $ do + e0 <- ann emptyHole $ tlet "x" (tvar "x") $ tvar "x" + e1 <- ann emptyHole $ tvar "x" + pure (e0, e1) + in do + r <- evalFullTest mempty mempty Syn expr + r @?= Right expected + +unit_closed_let_beta :: Assertion +unit_closed_let_beta = + let (expr, expected) = create2 $ do + e0 <- + let_ + "x" + (con0 cFalse `ann` tcon tBool) + ( lam "y" (con cCons [lvar "x", lvar "y"]) + `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool)) + ) + `app` con0 cTrue + e8 <- + con + cCons + [ con0 cFalse + , con0 cTrue + ] + `ann` (tcon tList `tapp` tcon tBool) + pure (e0, e8) + in do + r <- evalFullTest mempty mempty Syn expr + r @?= Right expected + +unit_closed_single_lets :: Assertion +unit_closed_single_lets = + let (expr, expected) = create2 $ do + e0 <- + let_ "x" (con0 cFalse) + $ let_ "y" (con0 cTrue) + $ con + cMakePair + [ lvar "x" + , lvar "y" + ] + e4 <- + con + cMakePair + [ con0 cFalse + , con0 cTrue + ] + pure (e0, e4) + in do + r <- evalFullTest mempty mempty Syn expr + r @?= Right expected + +unit_let_self_capture :: Assertion +unit_let_self_capture = + let ( forgetMetadata -> expr2 + , forgetMetadata -> expected2 + , forgetMetadata -> expr3 + , forgetMetadata -> expected3b + ) = create' $ do + e2 <- lam "x" $ let_ "x" (lvar "x") (lvar "x") + expect2 <- lam "x" $ lvar "x" + e3 <- lAM "x" $ letType "x" (tvar "x") (emptyHole `ann` tvar "x") + expect3b <- lAM "x" $ emptyHole `ann` tvar "x" + pure + ( e2 + , expect2 + , e3 + , expect3b + ) + in do + s2 <- evalFullTest mempty mempty Chk expr2 + s2 @?= Right expected2 + s3 <- evalFullTest mempty mempty Chk expr3 + s3 @?= Right expected3b + +-- | Evaluation preserves types +-- (assuming we don't end with a 'LetType' in the term, as the typechecker +-- cannot currently deal with those) +tasty_type_preservation :: Property +tasty_type_preservation = withTests 1000 + $ withDiscards 2000 + $ propertyWT testModules + $ do + let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules + tds <- asks typeDefs + (dir, forgetMetadata -> t, ty) <- genDirTm + s <- liftIO (evalFullTest' (MicroSec 10_000) tds globs dir t) + case s of + Left err -> label ("error: " <> LabelName (show err)) >> success + Right s' -> do + label "NF" + annotateShow s' + if hasTypeLets s' + then label "skipped due to LetType" >> success + else do + s'' <- checkTest ty =<< generateIDs s' + s' === forgetMetadata s'' -- check no smart holes happened + +---- Unsaturated primitives are stuck terms +unit_prim_stuck :: Assertion +unit_prim_stuck = + let (forgetMetadata -> f, prims) = create' $ (,) <$> pfun ToUpper <*> primDefs + in do + s <- evalFullTest mempty prims Syn f + s @?= Right f + +unit_prim_toUpper :: Assertion +unit_prim_toUpper = + unaryPrimTest + ToUpper + (char 'a') + (char 'A') + +unit_prim_isSpace_1 :: Assertion +unit_prim_isSpace_1 = + unaryPrimTest + IsSpace + (char '\n') + (boolAnn True) + +unit_prim_isSpace_2 :: Assertion +unit_prim_isSpace_2 = + unaryPrimTest + IsSpace + (char 'a') + (boolAnn False) + +tasty_prim_hex_nat :: Property +tasty_prim_hex_nat = withTests 20 . property $ do + n <- forAllT $ Gen.integral $ Range.constant 0 50 + let ne = nat n + (dir, forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ if n <= 15 + then + (Chk,,,) + <$> case_ + ( pfun NatToHex + `app` ne + ) + [ branch + cNothing + [] + (con cNothing []) + , branch + cJust + [("x", Nothing)] + ( pfun HexToNat + `app` lvar "x" + ) + ] + <*> con cJust [ne] + <*> primDefs + else + (Syn,,,) + <$> pfun NatToHex + `app` ne + <*> con cNothing [] + `ann` (tcon tMaybe `tapp` tcon tChar) + <*> primDefs + s <- evalIO $ evalFullTest builtinTypes prims dir e + s === Right r + +unit_prim_char_eq_1 :: Assertion +unit_prim_char_eq_1 = + binaryPrimTest + EqChar + (char 'a') + (char 'a') + (con0 cTrue `ann` tcon tBool) + +unit_prim_char_eq_2 :: Assertion +unit_prim_char_eq_2 = + binaryPrimTest + EqChar + (char 'a') + (char 'A') + (con0 cFalse `ann` tcon tBool) + +unit_prim_char_partial :: Assertion +unit_prim_char_partial = + let (forgetMetadata -> e, prims) = + create' + $ (,) + <$> pfun EqChar + `app` char 'a' + <*> primDefs + in do + s <- evalFullTest mempty prims Syn e + s @?= Right e + +unit_prim_int_add :: Assertion +unit_prim_int_add = + binaryPrimTest + IntAdd + (int 2) + (int 2) + (int 4) + +unit_prim_int_add_big :: Assertion +unit_prim_int_add_big = + binaryPrimTest + IntAdd + (int big) + (int big) + (int (2 * big :: Integer)) + where + big = fromIntegral (maxBound :: Word64) + +unit_prim_int_sub :: Assertion +unit_prim_int_sub = + binaryPrimTest + IntMinus + (int 5) + (int 3) + (int 2) + +unit_prim_int_sub_negative :: Assertion +unit_prim_int_sub_negative = + binaryPrimTest + IntMinus + (int 3) + (int 5) + (int (-2)) + +unit_prim_int_mul :: Assertion +unit_prim_int_mul = + binaryPrimTest + IntMul + (int 3) + (int 2) + (int 6) + +unit_prim_int_quotient :: Assertion +unit_prim_int_quotient = + binaryPrimTest + IntQuotient + (int 7) + (int 3) + (con cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_quotient_negative :: Assertion +unit_prim_int_quotient_negative = + binaryPrimTest + IntQuotient + (int (-7)) + (int 3) + (con cJust [int (-3)] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_quotient_zero :: Assertion +unit_prim_int_quotient_zero = + binaryPrimTest + IntQuotient + (int (-7)) + (int 0) + (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_remainder :: Assertion +unit_prim_int_remainder = + binaryPrimTest + IntRemainder + (int 7) + (int 3) + (con cJust [int 1] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_remainder_negative_1 :: Assertion +unit_prim_int_remainder_negative_1 = + binaryPrimTest + IntRemainder + (int (-7)) + (int (-3)) + (con cJust [int (-1)] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_remainder_negative_2 :: Assertion +unit_prim_int_remainder_negative_2 = + binaryPrimTest + IntRemainder + (int (-7)) + (int 3) + (con cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_remainder_negative_3 :: Assertion +unit_prim_int_remainder_negative_3 = + binaryPrimTest + IntRemainder + (int 7) + (int (-3)) + (con cJust [int (-2)] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_remainder_zero :: Assertion +unit_prim_int_remainder_zero = + binaryPrimTest + IntRemainder + (int 7) + (int 0) + (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt)) + +unit_prim_int_quot :: Assertion +unit_prim_int_quot = + binaryPrimTest + IntQuot + (int 7) + (int 3) + (int 2) + +unit_prim_int_quot_negative :: Assertion +unit_prim_int_quot_negative = + binaryPrimTest + IntQuot + (int (-7)) + (int 3) + (int (-3)) + +unit_prim_int_quot_zero :: Assertion +unit_prim_int_quot_zero = + binaryPrimTest + IntQuot + (int (-7)) + (int 0) + (int 0) + +unit_prim_int_rem :: Assertion +unit_prim_int_rem = + binaryPrimTest + IntRem + (int 7) + (int 3) + (int 1) + +unit_prim_int_rem_negative_1 :: Assertion +unit_prim_int_rem_negative_1 = + binaryPrimTest + IntRem + (int (-7)) + (int (-3)) + (int (-1)) + +unit_prim_int_rem_negative_2 :: Assertion +unit_prim_int_rem_negative_2 = + binaryPrimTest + IntRem + (int (-7)) + (int 3) + (int 2) + +unit_prim_int_rem_negative_3 :: Assertion +unit_prim_int_rem_negative_3 = + binaryPrimTest + IntRem + (int 7) + (int (-3)) + (int (-2)) + +unit_prim_int_rem_zero :: Assertion +unit_prim_int_rem_zero = + binaryPrimTest + IntRem + (int 7) + (int 0) + (int 7) + +unit_prim_int_eq_1 :: Assertion +unit_prim_int_eq_1 = + binaryPrimTest + IntEq + (int 2) + (int 2) + (boolAnn True) + +unit_prim_int_eq_2 :: Assertion +unit_prim_int_eq_2 = + binaryPrimTest + IntEq + (int 2) + (int 1) + (boolAnn False) + +unit_prim_int_neq_1 :: Assertion +unit_prim_int_neq_1 = + binaryPrimTest + IntNeq + (int 2) + (int 2) + (boolAnn False) + +unit_prim_int_neq_2 :: Assertion +unit_prim_int_neq_2 = + binaryPrimTest + IntNeq + (int 2) + (int 1) + (boolAnn True) + +unit_prim_int_less_than_1 :: Assertion +unit_prim_int_less_than_1 = + binaryPrimTest + IntLT + (int 1) + (int 2) + (boolAnn True) + +unit_prim_int_less_than_2 :: Assertion +unit_prim_int_less_than_2 = + binaryPrimTest + IntLT + (int 1) + (int 1) + (boolAnn False) + +unit_prim_int_less_than_or_equal_1 :: Assertion +unit_prim_int_less_than_or_equal_1 = + binaryPrimTest + IntLTE + (int 1) + (int 2) + (boolAnn True) + +unit_prim_int_less_than_or_equal_2 :: Assertion +unit_prim_int_less_than_or_equal_2 = + binaryPrimTest + IntLTE + (int 1) + (int 1) + (boolAnn True) + +unit_prim_int_less_than_or_equal_3 :: Assertion +unit_prim_int_less_than_or_equal_3 = + binaryPrimTest + IntLTE + (int 2) + (int 1) + (boolAnn False) + +unit_prim_int_greater_than_1 :: Assertion +unit_prim_int_greater_than_1 = + binaryPrimTest + IntGT + (int 2) + (int 1) + (boolAnn True) + +unit_prim_int_greater_than_2 :: Assertion +unit_prim_int_greater_than_2 = + binaryPrimTest + IntGT + (int 1) + (int 1) + (boolAnn False) + +unit_prim_int_greater_than_or_equal_1 :: Assertion +unit_prim_int_greater_than_or_equal_1 = + binaryPrimTest + IntGTE + (int 1) + (int 2) + (boolAnn False) + +unit_prim_int_greater_than_or_equal_2 :: Assertion +unit_prim_int_greater_than_or_equal_2 = + binaryPrimTest + IntGTE + (int 1) + (int 1) + (boolAnn True) + +unit_prim_int_greater_than_or_equal_3 :: Assertion +unit_prim_int_greater_than_or_equal_3 = + binaryPrimTest + IntGTE + (int 2) + (int 1) + (boolAnn True) + +unit_prim_int_toNat :: Assertion +unit_prim_int_toNat = + unaryPrimTest + IntToNat + (int 0) + (con cJust [nat 0] `ann` (tcon tMaybe `tapp` tcon tNat)) + +unit_prim_int_toNat_negative :: Assertion +unit_prim_int_toNat_negative = + unaryPrimTest + IntToNat + (int (-1)) + (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tNat)) + +unit_prim_int_fromNat :: Assertion +unit_prim_int_fromNat = + unaryPrimTest + IntFromNat + (nat 4) + (int 4) + +unit_prim_ann :: Assertion +unit_prim_ann = + let (forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ (,,) + <$> ( pfun ToUpper + `ann` (tcon tChar `tfun` tcon tChar) + ) + `app` (char 'a' `ann` tcon tChar) + <*> char 'A' + <*> primDefs + in do + s <- evalFullTest builtinTypes prims Syn e + s @?= Right r + +unit_prim_lazy_1 :: Assertion +unit_prim_lazy_1 = + let (forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ (,,) + <$> pfun PrimConst + `app` bool_ True + `app` emptyHole + <*> bool_ True + `ann` tcon tBool + <*> primDefs + in do + s <- evalFullTest builtinTypes prims Syn e + s @?= Right r + +unit_prim_lazy_2 :: Assertion +unit_prim_lazy_2 = + let (forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ (,,) + <$> pfun PrimConst + `app` bool_ True + `app` letrec "x" (lvar "x") (tcon tNat) (lvar "x") + <*> bool_ True + `ann` tcon tBool + <*> primDefs + in do + s <- evalFullTest builtinTypes prims Syn e + s @?= Right r + +unit_prim_partial_map :: Assertion +unit_prim_partial_map = + let modName = mkSimpleModuleName "TestModule" + (forgetMetadata -> e, forgetMetadata -> r, gs, prims) = + create' $ do + (mapName, mapDef) <- Examples.map' modName + (,,,) + <$> gvar mapName + `aPP` tcon tChar + `aPP` tcon tChar + `app` pfun ToUpper + `app` list_ + [ char 'a' + , char 'b' + , char 'c' + ] + <*> list_ + [ char 'A' + , char 'B' + , char 'C' + ] + `ann` (tcon tList `tapp` tcon tChar) + <*> pure (M.singleton mapName mapDef) + <*> primDefs + in do + s <- evalFullTest builtinTypes (gs <> prims) Syn e + s @?= Right r + +-- TODO: enable when have EvalFullRequest with interp +---- Test that handleEvalFullRequest will reduce imported terms +-- unit_eval_full_modules :: Assertion +-- unit_eval_full_modules = +-- let test = do +-- builtinModule' <- builtinModule +-- primitiveModule' <- primitiveModule +-- importModules [primitiveModule', builtinModule'] +-- foo <- pfun ToUpper `app` char 'a' +-- resp <- +-- readerToState +-- $ handleEvalFullRequest +-- EvalFullReq +-- { evalFullReqExpr = foo +-- , evalFullCxtDir = Chk +-- , evalFullMaxSteps = 2 +-- , evalFullOptions = UnderBinders +-- } +-- expect <- char 'A' +-- pure $ case resp of +-- EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" +-- EvalFullRespNormal e -> e ~= expect +-- a = newEmptyApp +-- in runAppTestM a test <&> fst >>= \case +-- Left err -> assertFailure $ show err +-- Right assertion -> assertion + +---- TODO: enable when have EvalFullRequest with interp +---- Test that handleEvalFullRequest will reduce case analysis of imported types +-- unit_eval_full_modules_scrutinize_imported_type :: Assertion +-- unit_eval_full_modules_scrutinize_imported_type = +-- let test = do +-- m' <- m +-- importModules [m'] +-- foo <- +-- case_ +-- (con0 cTrue `ann` tcon tBool) +-- [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue] +-- resp <- +-- readerToState +-- $ handleEvalFullRequest +-- $ EvalFullReq +-- { evalFullReqExpr = foo +-- , evalFullCxtDir = Chk +-- , evalFullMaxSteps = 2 +-- , evalFullOptions = UnderBinders +-- } +-- expect <- con0 cFalse +-- pure $ case resp of +-- EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" +-- EvalFullRespNormal e -> e ~= expect +-- a = newEmptyApp +-- in runAppTestM a test <&> fst >>= \case +-- Left err -> assertFailure $ show err +-- Right assertion -> assertion +-- where +-- m = do +-- boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef +-- pure +-- $ Module +-- { moduleName = qualifiedModule tBool +-- , moduleTypes = Map.singleton (baseName tBool) boolDef' +-- , moduleDefs = mempty +-- } + +unit_wildcard :: Assertion +unit_wildcard = + let loop = letrec "x" (lvar "x") (tcon tNat) (lvar "x") + eTerm = create1 $ caseFB_ loop [] (con0 cTrue) + expectTerm = forgetMetadata $ create' $ con0 cTrue + eDiverge = create1 $ caseFB_ loop [branch cZero [] $ con0 cFalse] (con0 cTrue) + in do + s <- evalFullTest mempty mempty Syn eTerm + s @?= Right expectTerm + t <- evalFullTest' (MicroSec 10_000) mempty mempty Syn eDiverge + t @?= Left Timeout + +unit_case_prim :: Assertion +unit_case_prim = + let e1 = create1 $ caseFB_ (char 'a') [] (con0 cTrue) + expect1 = create1 $ con0 cTrue + e2 = create1 $ caseFB_ (char 'a') [branchPrim (PrimChar 'a') $ con0 cFalse] (con0 cTrue) + expect2 = create1 $ con0 cFalse + e3 = + create1 + $ caseFB_ + (char 'b') + [ branchPrim (PrimChar 'a') $ con0 cTrue + , branchPrim (PrimChar 'b') $ con0 cFalse + ] + (con0 cTrue) + expect3 = create1 $ con0 cFalse + e4 = + create1 + $ caseFB_ + ( (lam "x" (lvar "x") `ann` (tcon tChar `tfun` tcon tChar)) + `app` char 'a' + ) + [branchPrim (PrimChar 'a') $ con0 cFalse] + (con0 cTrue) + expect4 = create1 $ con0 cFalse + in do + s1 <- evalFullTest mempty mempty Syn e1 + s1 @?= Right expect1 + s2 <- evalFullTest mempty mempty Syn e2 + s2 @?= Right expect2 + s3 <- evalFullTest mempty mempty Syn e3 + s3 @?= Right expect3 + s4 <- evalFullTest mempty mempty Syn e4 + s4 @?= Right expect4 + +-- Taking the head of an infinite list works +-- (this tests our interpreter is lazy enough) +unit_lazy_head :: Assertion +unit_lazy_head = + let hd = lAM "a" $ lam "xs" $ caseFB_ (lvar "xs") [branch cCons [("y", Nothing), ("ys", Nothing)] $ lvar "y"] emptyHole + hdTy = tforall "a" ktype $ (tcon tList `tapp` tvar "a") `tfun` tvar "a" + repTrue = letrec "r" (con cCons [con0 cTrue, lvar "r"]) (tcon tList `tapp` tcon tBool) (lvar "r") + e = create1 $ (hd `ann` hdTy) `aPP` tcon tBool `app` repTrue + expect = create1 $ con0 cTrue `ann` tcon tBool + in do + s <- evalFullTest builtinTypes mempty Syn e + s @?= Right expect + +-- * Utilities + +evalFullTest' :: Timeout -> TypeDefMap -> DefMap -> Dir -> Expr' () () () -> IO (Either InterpError (Expr' () () ())) +evalFullTest' t tydefs = interp t tydefs . mkGlobalEnv + +evalFullTest :: TypeDefMap -> DefMap -> Dir -> Expr' () () () -> IO (Either InterpError (Expr' () () ())) +evalFullTest = evalFullTest' (MicroSec (-1)) -- negative time means wait forever + +unaryPrimTest :: HasCallStack => PrimDef -> S Expr -> S Expr -> Assertion +unaryPrimTest f x y = + let (forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ (,,) + <$> pfun f + `app` x + <*> y + <*> primDefs + in do + s <- evalFullTest mempty prims Syn e + s @?= Right r +binaryPrimTest :: HasCallStack => PrimDef -> S Expr -> S Expr -> S Expr -> Assertion +binaryPrimTest f x y z = + let (forgetMetadata -> e, forgetMetadata -> r, prims) = + create' + $ (,,) + <$> pfun f + `app` x + `app` y + <*> z + <*> primDefs + in do + s <- evalFullTest mempty prims Syn e + s @?= Right r + +create1 :: S (Expr' a b c) -> Expr' () () () +create1 = forgetMetadata . create' + +create2 :: S (Expr' a1 b1 c1, Expr' a2 b2 c2) -> (Expr' () () (), Expr' () () ()) +create2 = bimap forgetMetadata forgetMetadata . create' + +create3 :: + S (Expr' a1 b1 c1, Expr' a2 b2 c2, Expr' a3 b3 c3) -> + (Expr' () () (), Expr' () () (), Expr' () () ()) +create3 = (\(x, y, z) -> (forgetMetadata x, forgetMetadata y, forgetMetadata z)) . create' From c545482df9afc509ccd100322430b5fd45a1d0a5 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 29 Nov 2023 15:29:33 +0000 Subject: [PATCH 7/7] 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 =