From 2016c8a50fadeaf4ddc4eb41b32f5ab7c2f13290 Mon Sep 17 00:00:00 2001 From: Drew Hess Date: Thu, 18 Apr 2024 01:36:03 +0100 Subject: [PATCH] chore(primer-api): expose the interpreter via the API Signed-off-by: Drew Hess --- primer-api/src/Primer/API.hs | 173 +++++++++++++++++++++++++++++++++++ primer-api/test/Tests/API.hs | 8 +- primer/src/Primer/App.hs | 2 +- 3 files changed, 181 insertions(+), 2 deletions(-) diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index e36e781b3..944a86f92 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -54,6 +54,12 @@ module Primer.API ( evalFull, EvalFullResp (..), evalFull', + evalBoundedInterp, + EvalBoundedInterpResp (..), + evalBoundedInterp', + evalInterp, + EvalInterpResp (..), + evalInterp', flushSessions, createDefinition, createTypeDef, @@ -127,7 +133,9 @@ import Primer.App ( DefSelection (..), EditAppM, Editable, + EvalBoundedInterpReq (..), EvalFullReq (..), + EvalInterpReq (..), EvalReq (..), EvalResp (..), Level, @@ -141,7 +149,9 @@ import Primer.App ( TypeDefParamSelection (..), TypeDefSelection (..), appProg, + handleEvalBoundedInterpRequest, handleEvalFullRequest, + handleEvalInterpRequest, handleEvalRequest, handleGetProgramRequest, handleMutationRequest, @@ -240,6 +250,10 @@ import Primer.Def ( import Primer.Def qualified as Def import Primer.Eval (NormalOrderOptions (StopAtBinders)) import Primer.Eval.Redex (Dir (Chk), EvalLog) +import Primer.EvalFullInterp ( + InterpError, + Timeout (MicroSec), + ) import Primer.EvalFullStep (TerminationBound) import Primer.JSON ( CustomJSON (..), @@ -432,6 +446,10 @@ data APILog | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp)) | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp)) | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp) + | EvalBoundedInterp (ReqResp (SessionId, EvalBoundedInterpReq) (Either ProgError App.EvalBoundedInterpResp)) + | EvalBoundedInterp' (ReqResp (SessionId, Maybe Timeout, GVarName) EvalBoundedInterpResp) + | EvalInterp (ReqResp (SessionId, EvalInterpReq) (Either ProgError App.EvalInterpResp)) + | EvalInterp' (ReqResp (SessionId, GVarName) EvalInterpResp) | FlushSessions (ReqResp () ()) | CreateDef (ReqResp (SessionId, ModuleName, Maybe Text) Prog) | CreateTypeDef (ReqResp (SessionId, TyConName, [ValConName]) Prog) @@ -1253,6 +1271,161 @@ evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) -> do Right a -> a Left v -> absurd v +-- | Using the interpreter, evaluate an expression given by the +-- 'EvalInterpReq', in the context of the application contained +-- in the given 'SessionId'. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. If +-- your application is not prepared to handle this situation, you may +-- want to use 'evalBoundedInterp', instead. +-- +-- N.B.: this action may 'Control.Exception.throw' an imprecise +-- exception of type 'InterpError' in the event that the expression to +-- be evaluated is not well typed. In normal use, however, this +-- condition should not arise. See 'Primer.EvalFullInterp.interp'', +-- which this action uses, for details. (Note that the +-- 'InterpError.Timeout' exception value will never be thrown by this +-- action, as explained above.) +evalInterp :: + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + EvalInterpReq -> + PrimerM m (Either ProgError App.EvalInterpResp) +evalInterp = curry $ logAPI (leftResultError EvalInterp) $ \(sid, req) -> do + app <- getApp sid + runQueryAppM (handleEvalInterpRequest req) app + +-- | This type is the API's view of a 'App.EvalInterpResp'. +newtype EvalInterpResp + = EvalInterpRespNormal Tree + deriving stock (Show, Read, Generic) + deriving (ToJSON, FromJSON) via PrimerJSON EvalInterpResp + +-- | Using the interpreter, evaluate the top-level definition whose +-- name is given in the 'GVarName', in the context of the application +-- contained in the given 'SessionId'. +-- +-- This is a simplified version of 'evalInterp', intended for +-- non-Haskell clients. +-- +-- Caution: depending on the expression being evaluated, the +-- evaluation may not terminate, and/or may grow in unbounded size. If +-- your application is not prepared to handle this situation, you may +-- want to use 'evalBoundedInterp'', instead. +-- +-- N.B.: this action may 'Control.Exception.throw' an imprecise +-- exception of type 'InterpError' in the event that the expression to +-- be evaluated is not well typed. In normal use, however, this +-- condition should not arise. See 'Primer.EvalFullInterp.interp'', +-- which this action uses, for details. (Note that the +-- 'InterpError.Timeout' exception value will never be thrown by this +-- action, as explained above.) +evalInterp' :: + forall m l. + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + GVarName -> + PrimerM m EvalInterpResp +evalInterp' = curry $ logAPI (noError EvalInterp') $ \(sid, d) -> do + app <- getApp sid + noErr <$> runQueryAppM (q d) app + where + q :: + GVarName -> + QueryAppM (PrimerM m) Void EvalInterpResp + q d = do + -- 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 + (App.EvalInterpRespNormal e') <- + handleEvalInterpRequest + $ EvalInterpReq + { expr = e + , dir = Chk + } + pure $ EvalInterpRespNormal $ viewTreeExpr e' + noErr :: Either Void a -> a + noErr = \case + Right a -> a + Left v -> absurd v + +-- | Using the interpreter, evaluate an expression given by the +-- 'EvalBoundedInterpReq', in the context of the application contained +-- in the given 'SessionId'. The evaluation time is bounded by the +-- timeout provided in the same 'EvalBoundedInterpReq'. +-- +-- Note that, unlike evaluation requests that use the step evaluator, +-- if this action times out during evaluation, the result is an error, +-- not a partially-evaluated expression. +evalBoundedInterp :: + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + EvalBoundedInterpReq -> + PrimerM m (Either ProgError App.EvalBoundedInterpResp) +evalBoundedInterp = curry $ logAPI (leftResultError EvalBoundedInterp) $ \(sid, req) -> do + app <- getApp sid + runQueryAppM (handleEvalBoundedInterpRequest req) app + +-- | This type is the API's view of a 'App.EvalBoundedInterpResp'. +data EvalBoundedInterpResp + = EvalBoundedInterpRespFailed InterpError + | EvalBoundedInterpRespNormal Tree + deriving stock (Show, Read, Generic) + deriving (ToJSON, FromJSON) via PrimerJSON EvalBoundedInterpResp + +-- | Using the interpreter, evaluate the top-level definition whose +-- name is given in the 'GVarName', in the context of the application +-- contained in the given 'SessionId'. The evaluation time is bounded +-- by the 'Timeout' argument, or is limited to 10 microseconds if the +-- timeout is not provided. +-- +-- Note that, unlike evaluation requests that use the step evaluator, +-- if this action times out during evaluation, the result is an error, +-- not a partially-evaluated expression. +-- +-- This is a simplified version of 'evalBoundedInterp', intended for +-- non-Haskell clients. +evalBoundedInterp' :: + forall m l. + (MonadIO m, MonadThrow m, MonadAPILog l m) => + SessionId -> + Maybe Timeout -> + GVarName -> + PrimerM m EvalBoundedInterpResp +evalBoundedInterp' = curry3 $ logAPI (noError EvalBoundedInterp') $ \(sid, timeout, d) -> do + app <- getApp sid + noErr <$> runQueryAppM (q timeout d) app + where + q :: + Maybe Timeout -> + GVarName -> + QueryAppM (PrimerM m) Void EvalBoundedInterpResp + q timeout d = do + -- 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 <- + handleEvalBoundedInterpRequest + $ EvalBoundedInterpReq + { expr = e + , dir = Chk + , timeout = fromMaybe (MicroSec 10) timeout + } + pure $ case x of + App.EvalBoundedInterpRespFailed err -> EvalBoundedInterpRespFailed err + App.EvalBoundedInterpRespNormal e' -> EvalBoundedInterpRespNormal $ viewTreeExpr e' + noErr :: Either Void a -> a + noErr = \case + Right a -> a + Left v -> absurd v + flushSessions :: (MonadIO m, MonadAPILog l m) => PrimerM m () flushSessions = logAPI' FlushSessions $ do sessionsTransaction $ \ss _ -> do diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 5de63b9e9..c6b0c3c43 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -18,6 +18,7 @@ import Primer.API ( copySession, deleteSession, edit, + evalBoundedInterp', evalFull', findSessions, flushSessions, @@ -73,6 +74,9 @@ import Primer.Database ( ) import Primer.Def (astDefExpr, astDefType, defAST) import Primer.Eval (NormalOrderOptions (UnderBinders)) +import Primer.EvalFullInterp ( + Timeout (MicroSec), + ) import Primer.Examples ( comprehensive, even3App, @@ -491,7 +495,7 @@ test_eval_undo = step "create session" sid <- newSession $ NewSessionReq "a new session" True let scope = mkSimpleModuleName "Main" - step "eval" + step "evalFull'" void $ evalFull' sid (Just 100) (Just UnderBinders) $ qualifyName scope "main" step "insert λ" let getMain = do @@ -532,6 +536,8 @@ test_eval_undo = _ <- undo sid step "redo" _ <- redo sid + step "evalBoundedInterp'" + void $ evalBoundedInterp' sid (Just $ MicroSec 100) $ qualifyName scope "main" step "undo *2" _ <- undo sid >> undo sid step "redo" diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d5eee4187..5e281b14b 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1494,7 +1494,7 @@ runEditAppM (EditAppM m) appState = -- Actions run in this monad cannot modify the 'App'. We use 'ExceptT' -- here for compatibility with 'EditApp'. newtype QueryAppM m e a = QueryAppM (ReaderT App (ExceptT e m) a) - deriving newtype (Functor, Applicative, Monad, MonadReader App, MonadError e, MonadLog l) + deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader App, MonadError e, MonadLog l) -- | Run a 'QueryAppM' action, returning a result. runQueryAppM :: QueryAppM m e a -> App -> m (Either e a)