feat: interpreter (faster evaluator-to-normal-form)

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,

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.EvalFull (
+import Primer.EvalFullInterp qualified as EFInterp
+import Primer.EvalFullStep (
   Dir (Syn),
-  EvalLog,
-  evalFull,
  )
+import Primer.EvalFullStep qualified as EFStep
 import Primer.Examples (
   mapOddPrimProg,
   mapOddProg,
@@ -79,17 +80,23 @@ 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
+          "interp (has no logs)"
+          [ benchExpectedInterp (mapEvenEnv 1) "mapEven 1" Syn
+          , benchExpectedInterp (mapEvenEnv 10) "mapEven 10" Syn
+          , benchExpectedInterp (mapEvenEnv 100) "mapEven 100" Syn
           ]
       ]
   , Group
@@ -106,23 +113,33 @@ 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 =
+        $ 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
         (f e')
         b
         (pure $ (@?= Right (zeroIDs $ expectedResult e')) . fmap zeroIDs . g)
 
-    benchExpectedPureLogs = benchExpected evalTestMPureLogs fst
-    benchExpectedDiscardLogs = benchExpected evalTestMDiscardLogs identity
+    -- 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
 

primer/gen/Primer/Gen/Core/Typed.hs

@@ -68,15 +68,15 @@ 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 (
-  TestM,
-  evalTestM,
+  TestT,
+  evalTestT,
   isolateTestM,
  )
 import Primer.TypeDef (
@@ -130,14 +130,15 @@ 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
     , Monad
     , MonadReader Cxt
     , MonadFresh NameCounter
     , MonadFresh ID
+    , MonadIO
     )
 
 -- | Run an action and ignore any effect on the fresh name/id state
@@ -198,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
@@ -701,8 +694,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.

primer/primer.cabal

@@ -33,7 +33,8 @@ library
     Primer.Def.Utils
     Primer.Eval
     Primer.Eval.Redex
-    Primer.EvalFull
+    Primer.EvalFullInterp
+    Primer.EvalFullStep
     Primer.Examples
     Primer.JSON
     Primer.Log
@@ -216,7 +217,8 @@ test-suite primer-test
     Tests.Database
     Tests.Eval
     Tests.Eval.Utils
-    Tests.EvalFull
+    Tests.EvalFullInterp
+    Tests.EvalFullStep
     Tests.Examples
     Tests.FreeVars
     Tests.Gen.App

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 (

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.

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

primer/src/Primer/Core/Utils.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE ViewPatterns #-}
+
 module Primer.Core.Utils (
   freshLocalName,
   freshLocalName',
@@ -23,15 +25,19 @@ module Primer.Core.Utils (
   freeGlobalVars,
   alphaEqTy,
   concreteTy,
+  alphaEq,
+  freshen,
 ) where
 
 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,
@@ -51,13 +57,14 @@ import Optics (
 
 import Primer.Core (
   CaseBranch' (..),
+  CaseFallback' (CaseExhaustive, CaseFallback),
   Expr,
   Expr' (..),
   GVarName,
   HasID (_id),
   ID,
   LVarName,
-  LocalName (unLocalName),
+  LocalName (LocalName, unLocalName),
   TmVarRef (GlobalVarRef, LocalVarRef),
   TyVarName,
   Type' (..),
@@ -72,6 +79,7 @@ import Primer.Core (
 import Primer.Core.Fresh (freshLocalName, freshLocalName')
 import Primer.Core.Type.Utils (
   alphaEqTy,
+  alphaEqTy',
   boundVarsTy,
   concreteTy,
   forgetKindMetadata,
@@ -86,7 +94,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 +202,73 @@ 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)
+
+-- 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
+    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