fix: an eval&undo/redo "lost ID" bug (#1086)

primer/src/Primer/API.hs

@@ -299,7 +299,7 @@ sessionsTransaction f = do
 
 data SessionOp l a where
   EditApp :: (App -> PureLog l (a, App)) -> SessionOp l a
-  QueryApp :: (App -> a) -> SessionOp l a
+  QueryApp :: (App -> PureLog l a) -> SessionOp l a
   OpGetSessionName :: SessionOp l Text
   GetSessionData :: SessionOp l SessionData
   OpRenameSession :: Text -> SessionOp l Text
@@ -346,7 +346,7 @@ withSession' sid op = do
             writeTBQueue q $ Database.UpdateApp sid appl' now
             -- We return an action which, when run, will log the messages
             pure $ Right (res, traverse_ logMessage logs)
-          QueryApp f -> pure $ Right (f appl, pure ())
+          QueryApp f -> pure $ Right $ second (traverse_ logMessage) $ runPureLog $ f appl
           OpGetSessionName -> pure $ Right (fromSessionName n, pure ())
           GetSessionData -> pure $ Right (s, pure ())
           OpRenameSession n' ->
@@ -574,15 +574,19 @@ renameSession = curry $ logAPI (noError RenameSession) $ \(sid, n) -> withSessio
 -- pass in the app state for that session.
 liftEditAppM ::
   forall m l e a.
-  (MonadIO m, MonadThrow m, MonadLog (WithSeverity l) m) =>
-  EditAppM (PureLog (WithSeverity l)) e a ->
+  (MonadIO m, MonadThrow m, MonadLog l m) =>
+  EditAppM (PureLog l) e a ->
   SessionId ->
   PrimerM m (Either e a)
 liftEditAppM h sid = withSession' sid (EditApp $ runEditAppM h)
 
 -- Run a 'QueryAppM' action, using the given session ID to look up and
 -- pass in the app state for that session.
-liftQueryAppM :: (MonadIO m, MonadThrow m, MonadLog l m) => QueryAppM a -> SessionId -> PrimerM m (Either ProgError a)
+liftQueryAppM ::
+  (MonadIO m, MonadThrow m, MonadLog l m) =>
+  QueryAppM (PureLog l) e a ->
+  SessionId ->
+  PrimerM m (Either e a)
 liftQueryAppM h sid = withSession' sid (QueryApp $ runQueryAppM h)
 
 -- | Given a 'SessionId', return the session's 'App'.
@@ -591,7 +595,7 @@ liftQueryAppM h sid = withSession' sid (QueryApp $ runQueryAppM h)
 -- expect typical API clients to use it. Its primary use is for
 -- testing.
 getApp :: (MonadIO m, MonadThrow m, MonadAPILog l m) => SessionId -> PrimerM m App
-getApp = logAPI (noError GetApp) $ \sid -> withSession' sid $ QueryApp identity
+getApp = logAPI (noError GetApp) $ \sid -> withSession' sid $ QueryApp pure
 
 -- | Given a 'SessionId', return the session's 'Prog'.
 --
@@ -602,7 +606,7 @@ getProgram' = logAPI (noError GetProgram') (fmap viewProg . getProgram)
 
 -- | Given a 'SessionId', return the session's 'App.Prog'.
 getProgram :: (MonadIO m, MonadThrow m, MonadAPILog l m) => SessionId -> PrimerM m App.Prog
-getProgram = logAPI (noError GetProgram) $ \sid -> withSession' sid $ QueryApp handleGetProgramRequest
+getProgram = logAPI (noError GetProgram) $ \sid -> withSession' sid $ QueryApp $ pure . handleGetProgramRequest
 
 -- | A frontend will be mostly concerned with rendering, and does not need the
 -- full complexity of our AST for that task. 'Tree' is a simplified view with
@@ -1075,15 +1079,15 @@ evalStep ::
   EvalReq ->
   PrimerM m (Either ProgError EvalResp)
 evalStep = curry $ logAPI (leftResultError EvalStep) $ \(sid, req) ->
-  liftEditAppM (handleEvalRequest req) sid
+  liftQueryAppM (handleEvalRequest req) sid
 
 evalFull ::
   (MonadIO m, MonadThrow m, MonadAPILog l m, ConvertLogMessage EvalLog l) =>
   SessionId ->
   EvalFullReq ->
   PrimerM m (Either ProgError App.EvalFullResp)
 evalFull = curry $ logAPI (leftResultError EvalFull) $ \(sid, req) ->
-  liftEditAppM (handleEvalFullRequest req) sid
+  liftQueryAppM (handleEvalFullRequest req) sid
 
 -- | This type is the API's view of a 'App.EvalFullResp
 -- (this is expected to evolve as we flesh out the API)
@@ -1105,14 +1109,19 @@ evalFull' ::
   GVarName ->
   PrimerM m EvalFullResp
 evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
-  noErr <$> liftEditAppM (q lim d) sid
+  noErr <$> liftQueryAppM (q lim d) sid
   where
     q ::
       Maybe TerminationBound ->
       GVarName ->
-      EditAppM (PureLog (WithSeverity l)) Void EvalFullResp
+      QueryAppM (PureLog (WithSeverity l)) Void EvalFullResp
     q lim d = do
-      e <- DSL.gvar d
+      -- We don't care about uniqueness of this ID, and we do not want to
+      -- disturb any FreshID state, since that could break undo/redo.
+      -- The reason we don't care about uniqueness is that this node will never
+      -- exist alongside anything else that it may clash with, as the first
+      -- evaluation step will be to inline this definition, removing the node.
+      let e = create' $ DSL.gvar d
       x <-
         handleEvalFullRequest $
           EvalFullReq

primer/src/Primer/App.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- This module defines the high level application functions.
@@ -24,6 +25,7 @@ module Primer.App (
   checkProgWellFormed,
   EditAppM,
   QueryAppM,
+  FreshViaApp (FreshViaApp),
   runEditAppM,
   runQueryAppM,
   Prog (..),
@@ -65,6 +67,7 @@ import Foreword hiding (mod)
 import Control.Monad.Fresh (MonadFresh (..))
 import Control.Monad.Log (MonadLog, WithSeverity)
 import Control.Monad.NestedError (MonadNestedError, throwError')
+import Control.Monad.Trans (MonadTrans)
 import Data.Data (Data)
 import Data.Generics.Uniplate.Operations (transform, transformM)
 import Data.Generics.Uniplate.Zipper (
@@ -495,7 +498,7 @@ data EvalFullResp
 -- Note that these only consider the non-imported module as a location of which
 -- to ask a question. However, they will return variables which are in scope by
 -- dint of being imported.
-handleQuestion :: MonadQueryApp m => Question a -> m a
+handleQuestion :: MonadQueryApp m ProgError => Question a -> m a
 handleQuestion = \case
   VariablesInScope defid exprid -> do
     node <- focusNode' defid exprid
@@ -559,15 +562,17 @@ handleEditRequest actions = do
 
 -- | Handle an eval request (we assume that all such requests are implicitly in a synthesisable context)
 handleEvalRequest ::
-  ( MonadEditApp l e m
+  ( MonadQueryApp m e
+  , MonadLog (WithSeverity l) m
   , MonadNestedError Eval.EvalError e m
   , ConvertLogMessage EvalLog l
   ) =>
   EvalReq ->
   m EvalResp
 handleEvalRequest req = do
-  prog <- gets appProg
-  result <- Eval.step (allTypes prog) (allDefs prog) (evalReqExpr req) Syn (evalReqRedex req)
+  app <- ask
+  let prog = appProg app
+  result <- runFreshM app $ Eval.step (allTypes prog) (allDefs prog) (evalReqExpr req) Syn (evalReqRedex req)
   case result of
     Left err -> throwError' err
     Right (expr, detail) -> do
@@ -580,10 +585,14 @@ handleEvalRequest req = do
           }
 
 -- | Handle an eval-to-normal-form request
-handleEvalFullRequest :: (MonadEditApp l e m, ConvertLogMessage EvalLog l) => EvalFullReq -> m EvalFullResp
+handleEvalFullRequest ::
+  (MonadQueryApp m e, MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  EvalFullReq ->
+  m EvalFullResp
 handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do
-  prog <- gets appProg
-  result <- evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  app <- ask
+  let prog = appProg app
+  result <- runFreshM app $ evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf
@@ -1182,6 +1191,16 @@ replay = mapM_ handleEditRequest
 --
 -- Note we do not want @MonadFresh Name m@, as @fresh :: m Name@ has
 -- no way of avoiding student-specified names. Instead, use 'freshName'.
+--
+-- Note that we have both a @MonadState App m@ and a @MonadFresh ID m@
+-- constraint (also a @MonadFresh NameCounter m@, to which similar comments
+-- apply). Note that an @App@ stores a fresh ID state. The @MonadFresh@
+-- instance should update this state; to achieve this behaviour for a custom
+-- monad with @MonadState App M@, use
+-- > deriving via FreshViaApp M instance MonadFresh ID M
+-- (This essentially mimics (pointwise) the effect of providing a @instance
+-- MonadState App m => MonadFresh ID m@, without having an orphan instance, or
+-- bad resolution behaviour.)
 type MonadEditApp l e m = (MonadLog (WithSeverity l) m, MonadEdit m e, MonadState App m)
 
 -- | A shorthand for constraints needed when doing low-level mutation
@@ -1192,7 +1211,7 @@ type MonadEdit m e = (MonadFresh ID m, MonadFresh NameCounter m, MonadError e m)
 
 -- | A shorthand for the constraints we need when performing read-only
 -- operations on the application.
-type MonadQueryApp m = (Monad m, MonadReader App m, MonadError ProgError m)
+type MonadQueryApp m e = (Monad m, MonadReader App m, MonadError e m)
 
 -- | The 'EditApp' monad.
 --
@@ -1215,14 +1234,12 @@ runEditAppM (EditAppM m) appState =
 --
 -- Actions run in this monad cannot modify the 'App'. We use 'ExceptT'
 -- here for compatibility with 'EditApp'.
-newtype QueryAppM a = QueryAppM (ReaderT App (Except ProgError) a)
-  deriving newtype (Functor, Applicative, Monad, MonadReader App, MonadError ProgError)
+newtype QueryAppM m e a = QueryAppM (ReaderT App (ExceptT e m) a)
+  deriving newtype (Functor, Applicative, Monad, MonadReader App, MonadError e, MonadLog l)
 
 -- | Run a 'QueryAppM' action, returning a result.
-runQueryAppM :: QueryAppM a -> App -> Either ProgError a
-runQueryAppM (QueryAppM m) appState = case runExcept (runReaderT m appState) of
-  Left err -> Left err
-  Right res -> Right res
+runQueryAppM :: QueryAppM m e a -> App -> m (Either e a)
+runQueryAppM (QueryAppM m) appState = runExceptT (runReaderT m appState)
 
 -- | The student's application's state.
 --
@@ -1368,6 +1385,16 @@ instance MonadFresh NameCounter (M e) where
 runTC :: App -> M e a -> Either e a
 runTC a = runExcept . flip evalStateT (appIdCounter a, appNameCounter a) . unM
 
+newtype FreshM m a = FreshM {unFreshM :: StateT (ID, NameCounter) m a}
+  deriving newtype (Functor, Applicative, Monad, MonadError e, MonadTrans)
+instance Monad m => MonadFresh ID (FreshM m) where
+  fresh = FreshM $ _1 <<%= succ
+instance Monad m => MonadFresh NameCounter (FreshM m) where
+  fresh = FreshM $ _2 <<%= succ
+instance MonadLog l m => MonadLog l (FreshM m)
+runFreshM :: Monad m => App -> FreshM m a -> m a
+runFreshM a = flip evalStateT (appIdCounter a, appNameCounter a) . unFreshM
+
 checkProgWellFormed ::
   ( MonadFresh ID m
   , MonadFresh NameCounter m
@@ -1400,21 +1427,27 @@ newType = do
   id_ <- fresh
   pure $ TEmptyHole (Meta id_ Nothing Nothing)
 
+newtype FreshViaApp m a = FreshViaApp (m a)
+  deriving newtype (Functor, Applicative, Monad)
+
 -- | Support for generating fresh IDs
-instance Monad m => MonadFresh ID (EditAppM m e) where
-  fresh = do
+instance MonadState App m => MonadFresh ID (FreshViaApp m) where
+  fresh = FreshViaApp $ do
     id_ <- gets appIdCounter
     modify (\s -> s & #currentState % #idCounter .~ id_ + 1)
     pure id_
 
 -- | Support for generating names. Basically just a counter so we don't
 -- generate the same automatic name twice.
-instance Monad m => MonadFresh NameCounter (EditAppM m e) where
-  fresh = do
+instance MonadState App m => MonadFresh NameCounter (FreshViaApp m) where
+  fresh = FreshViaApp $ do
     nc <- gets appNameCounter
     modify (\s -> s & #currentState % #nameCounter .~ succ nc)
     pure nc
 
+deriving via FreshViaApp (EditAppM m e) instance Monad m => MonadFresh ID (EditAppM m e)
+deriving via FreshViaApp (EditAppM m e) instance Monad m => MonadFresh NameCounter (EditAppM m e)
+
 copyPasteSig :: MonadEdit m ProgError => Prog -> (GVarName, ID) -> GVarName -> [Action] -> m Prog
 copyPasteSig p (fromDefName, fromTyId) toDefName setup = do
   c' <- focusNodeImports p fromDefName fromTyId

primer/test/Tests/API.hs

@@ -3,6 +3,7 @@ module Tests.API where
 import Foreword
 
 import Data.ByteString.Lazy qualified as BSL
+import Data.Map qualified as M
 import Data.Text qualified as Text
 import Data.Text.Lazy qualified as TL
 import Data.UUID.V4 (nextRandom)
@@ -13,18 +14,27 @@ import Primer.API (
   addSession,
   copySession,
   deleteSession,
+  edit,
+  evalFull',
   findSessions,
   flushSessions,
   getApp,
+  getProgram,
   getSessionName,
   getVersion,
   listSessions,
   newSession,
+  redo,
   renameSession,
+  undo,
   viewTreeExpr,
   viewTreeType,
  )
+import Primer.Action (Action (ConstructPrim, InsertSaturatedVar, SetCursor))
 import Primer.App (
+  MutationRequest (Edit),
+  Prog (progModules),
+  ProgAction (BodyAction, MoveToDef),
   newApp,
  )
 import Primer.Core
@@ -42,6 +52,8 @@ import Primer.Examples (
   even3App,
  )
 import Primer.Gen.Core.Raw (evalExprGen, genExpr, genType)
+import Primer.Module (moduleDefsQualified)
+import Primer.Prelude.Integer qualified as Integer
 import Primer.Test.Util (
   ExceptionPredicate,
   assertException,
@@ -436,3 +448,67 @@ test_renameSession_too_long =
       name <- renameSession sid $ toS $ replicate 65 'a'
       step "it should be truncated at 64 characters"
       name @?= toS (replicate 64 'a')
+
+test_eval_undo :: TestTree
+test_eval_undo =
+  testCaseSteps "eval plays nicely with undo/redo" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      let expectSuccess m =
+            m >>= \case
+              Left err -> liftIO $ assertFailure $ show err
+              Right x -> pure x
+      step "create session"
+      sid <- newSession $ NewSessionReq "a new session" True
+      let scope = mkSimpleModuleName "Main"
+      step "eval"
+      void $ evalFull' sid (Just 100) $ qualifyName scope "main"
+      step "insert λ"
+      let getMain = do
+            p <- getProgram sid
+            pure $ fmap astDefExpr . defAST =<< foldMap' moduleDefsQualified (progModules p) M.!? qualifyName scope "main"
+      i1 <-
+        getMain >>= \case
+          Just e@EmptyHole{} -> pure $ getID e
+          _ -> liftIO $ assertFailure "unexpected form of main"
+      _ <-
+        expectSuccess $
+          edit sid $
+            Edit
+              [ MoveToDef $ qualifyName scope "main"
+              , BodyAction
+                  [ SetCursor i1
+                  , InsertSaturatedVar $ GlobalVarRef Integer.even
+                  ]
+              ]
+      step "insert 4"
+      i2 <-
+        getMain >>= \case
+          Just (App _ _ e) -> pure $ getID e
+          _ -> liftIO $ assertFailure "unexpected form of main"
+      _ <-
+        expectSuccess $
+          edit sid $
+            Edit
+              [ MoveToDef $ qualifyName scope "main"
+              , BodyAction
+                  [ SetCursor i2
+                  , ConstructPrim $ PrimInt 4
+                  ]
+              ]
+      step "get edited App"
+      app0 <- getApp sid
+      step "undo"
+      _ <- undo sid
+      step "redo"
+      _ <- redo sid
+      step "undo *2"
+      _ <- undo sid >> undo sid
+      step "redo"
+      _ <- redo sid
+      step "redo"
+      _ <- redo sid
+      step "get final App"
+      app1 <- getApp sid
+      step "edited and redone progAllModules identical"
+      app1 @?= app0

primer/test/Tests/Action/Available.hs

@@ -734,7 +734,7 @@ offeredActionTest' sh l inputDef position action = do
   x <- for action'' $ \action''' -> do
     let result = defAST <=< flip findGlobalByName exprDefName
     let assertJust = maybe (assertFailure "Lost 'main' after action") pure
-    (res, _) <- runAppTestM (nextProgID prog) (mkEmptyTestApp prog) (handleEditRequest action''')
+    (res, _) <- runAppTestM (mkEmptyTestApp prog) (handleEditRequest action''')
     rr <- traverse (assertJust . result) res
     pure $ first ErrorRunningAction rr
   pure $ join x