feat(primer): add app-level handlers for eval via interpretation

This commit only adds these handlers at the `Primer.App` module level.
Hooking the interpreter up to the API and HTTP service will come in
subsequent commits.

Note that we add two handlers, one for time-bounded requests, and one
for unbounded requests. We will not expose the unbounded handler via
the HTTP API, since that would not be safe, but for local Haskell
programs, it might be useful to run the unbounded interpreter and
handle exceptions, timeouts, etc. in an application-specific manner,
which the time-bounded interpreter doesn't really make possible.

The time-bounded handler needs an additional `MonadIO` constraint
because the variant of the interpreter that it uses handles timeouts
and other imprecise exceptions that may be thrown by the interpreter.
This is unlike any other actions in `Primer.App`, but it's unavoidable
due to our particular lazy implementation of the interpreter. (See the
comments in the interpreter source for details.)

Signed-off-by: Drew Hess <src@drewhess.com>

primer/src/Primer/App.hs

@@ -54,12 +54,18 @@ module Primer.App (
   handleEditRequest,
   handleEvalRequest,
   handleEvalFullRequest,
+  handleEvalInterpRequest,
+  handleEvalBoundedInterpRequest,
   importModules,
   MutationRequest (..),
   EvalReq (..),
   EvalResp (..),
   EvalFullReq (..),
   EvalFullResp (..),
+  EvalInterpReq (..),
+  EvalInterpResp (..),
+  EvalBoundedInterpReq (..),
+  EvalBoundedInterpResp (..),
   lookupASTDef,
   liftError,
 ) where
@@ -181,7 +187,9 @@ import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
 import Primer.Core.DSL qualified as DSL
 import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp)
 import Primer.Core.Utils (
+  forgetMetadata,
   freeVars,
+  generateIDs,
   generateKindIDs,
   generateTypeIDs,
   regenerateExprIDs,
@@ -202,6 +210,13 @@ 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.EvalFullInterp (
+  InterpError,
+  Timeout,
+  interp,
+  interp',
+  mkGlobalEnv,
+ )
 import Primer.EvalFullStep (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull)
 import Primer.JSON
 import Primer.Log (ConvertLogMessage)
@@ -525,6 +540,53 @@ data EvalFullResp
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON EvalFullResp
 
+-- | A request to evaluate an expression to its normal form using the
+-- interpreter.
+--
+-- Caution: depending on the expression being evaluated, the
+-- evaluation may not terminate, and/or may grow in unbounded size.
+data EvalInterpReq = EvalInterpReq
+  { expr :: Expr
+  -- ^ The expression to evaluate.
+  , ctx :: Dir
+  -- ^ Indicates whether 'expr' is in a 'Syn' or 'Chk' context, so we
+  -- can tell if is an embedding.
+  }
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON EvalInterpReq
+
+-- | A response to a 'EvalBoundedInterpReq'.
+newtype EvalInterpResp
+  = -- | The evaluation succeeded, and the 'Expr' is the result.
+    EvalInterpRespNormal Expr
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON EvalInterpResp
+
+-- | A request to evaluate an expression to its normal form using the
+-- interpreter, but bounded in time.
+data EvalBoundedInterpReq = EvalBoundedInterpReq
+  { expr :: Expr
+  -- ^ The expression to evaluate.
+  , ctx :: Dir
+  -- ^ Indicates whether 'expr' is in a 'Syn' or 'Chk' context, so we
+  -- can tell if is an embedding.
+  , timeout :: Timeout
+  -- ^ An evaluation timeout, in microseconds. If the timeout is
+  -- exceeded, the evaluation will be halted, and no expression will
+  -- be returned; the interpreter's results are all-or-nothing.
+  }
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON EvalBoundedInterpReq
+
+-- | A response to a 'EvalBoundedInterpReq'.
+data EvalBoundedInterpResp
+  = -- | An 'InterpError' exception occurred during evaluation.
+    EvalBoundedInterpRespFailed InterpError
+  | -- | The evaluation succeeded, and the 'Expr' is the result.
+    EvalBoundedInterpRespNormal Expr
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON EvalBoundedInterpResp
+
 -- * Request handlers
 
 -- | Handle a question
@@ -633,6 +695,55 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf
 
+-- | Handle an 'EvalInterpReq'.
+--
+-- 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 'handleEvalBoundedInterpRequest', 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, as
+-- explained above.)
+handleEvalInterpRequest ::
+  (MonadQueryApp m e) =>
+  EvalInterpReq ->
+  m EvalInterpResp
+handleEvalInterpRequest (EvalInterpReq{expr, ctx}) = do
+  app <- ask
+  let prog = appProg app
+  let env = mkGlobalEnv (allDefs prog)
+  result <- runFreshM app $ generateIDs $ interp' (allTypes prog) env ctx (forgetMetadata expr)
+  pure $ EvalInterpRespNormal result
+
+-- | Handle an 'EvalBoundedInterpReq'.
+--
+-- Unlike 'handleEvalInterpRequest', this action will terminate the
+-- evaluation request if it exceeds the given timeout. Also unlike
+-- 'handleEvalInterpRequest', if an exception occurs during evaluation
+-- due to an ill typed term, the exception will be caught and reported
+-- via an appropriate 'EvalBoundedInterpResp' value.
+--
+-- Unlike other actions in this module, this action must be run within
+-- a 'MonadIO' context, because the exceptions it catches during
+-- interpretation can only be caught in the 'IO' monad.
+handleEvalBoundedInterpRequest ::
+  (MonadIO m, MonadQueryApp m e) =>
+  EvalBoundedInterpReq ->
+  m EvalBoundedInterpResp
+handleEvalBoundedInterpRequest (EvalBoundedInterpReq{expr, ctx, timeout}) = do
+  app <- ask
+  let prog = appProg app
+  let env = mkGlobalEnv (allDefs prog)
+  result <- liftIO $ interp timeout (allTypes prog) env ctx (forgetMetadata expr)
+  case result of
+    Left x -> pure $ EvalBoundedInterpRespFailed x
+    Right e' -> runFreshM app $ generateIDs e' <&> EvalBoundedInterpRespNormal
+
 -- | Handle a 'ProgAction'
 applyProgAction :: forall m. MonadEdit m ProgError => Prog -> ProgAction -> m Prog
 applyProgAction prog = \case

primer/src/Primer/EvalFullInterp.hs

@@ -51,6 +51,12 @@ import Primer.Def (ASTDef (ASTDef), Def (DefAST, DefPrim), DefMap)
 import Primer.Eval.Redex (
   Dir (Chk, Syn),
  )
+import Primer.JSON (
+  CustomJSON (..),
+  FromJSON,
+  PrimerJSON,
+  ToJSON,
+ )
 import Primer.Name (Name)
 import Primer.Primitives (primConName, primFunDef)
 import Primer.Primitives.PrimDef (PrimDef)
@@ -113,10 +119,13 @@ data InterpError
   | NoBranch (Either ValConName PrimCon) [Pattern]
   | UnknownTyCon TyConName
   | UnknownValCon TyConName ValConName
-  deriving stock (Eq, Show)
+  deriving stock (Eq, Show, Read, Generic)
   deriving anyclass (Exception)
+  deriving (FromJSON, ToJSON) via PrimerJSON InterpError
 
 newtype Timeout = MicroSec Int
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON Timeout
 
 -- | Wrap the interpreter in a IO-based timeout, and catch 'InterpError' exceptions
 interp ::