feat: expose UnderBinders/StopAtBinders to OpenAPI

Note that we are only adding an extra (optional) parameter to the api, thus this is not a breaking change. However, we are changing the default behaviour of the eval-full api. Signed-off-by: Ben Price <[email protected]>
hackworthltd · Jul 25, 2023 · 476ba69 · 476ba69
1 parent 6be7b00
commit 476ba69
Show file tree

Hide file tree

Showing 5 changed files with 31 additions and 8 deletions.
diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs
@@ -216,7 +216,7 @@ import Primer.Def (
   defAST,
  )
 import Primer.Def qualified as Def
-import Primer.Eval (NormalOrderOptions (UnderBinders))
+import Primer.Eval (NormalOrderOptions (StopAtBinders))
 import Primer.Eval.Redex (Dir (Chk), EvalLog)
 import Primer.EvalFull (TerminationBound)
 import Primer.JSON (
@@ -403,7 +403,7 @@ data APILog
   | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe Kind))) (Either ProgError [Name.Name]))
   | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp))
   | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp))
-  | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, GVarName) EvalFullResp)
+  | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp)
   | FlushSessions (ReqResp () ())
   | CreateDef (ReqResp (SessionId, ModuleName, Maybe Text) Prog)
   | CreateTypeDef (ReqResp (SessionId, TyConName, [ValConName]) Prog)
@@ -1107,16 +1107,18 @@ evalFull' ::
   (MonadIO m, MonadThrow m, MonadAPILog l m, ConvertLogMessage EvalLog l) =>
   SessionId ->
   Maybe TerminationBound ->
+  Maybe NormalOrderOptions ->
   GVarName ->
   PrimerM m EvalFullResp
-evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
-  noErr <$> liftQueryAppM (q lim d) sid
+evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) ->
+  noErr <$> liftQueryAppM (q lim closed d) sid
   where
     q ::
       Maybe TerminationBound ->
+      Maybe NormalOrderOptions ->
       GVarName ->
       QueryAppM (PureLog (WithSeverity l)) Void EvalFullResp
-    q lim d = do
+    q lim closed 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
@@ -1129,7 +1131,7 @@ evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
             { evalFullReqExpr = e
             , evalFullCxtDir = Chk
             , evalFullMaxSteps = fromMaybe 10 lim
-            , evalFullOptions = UnderBinders -- TODO/REVIEW: should we expose this to the actual api? If so, the BREAKING CHANGE commit message needs updating
+            , evalFullOptions = fromMaybe StopAtBinders closed
             }
       pure $ case x of
         App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e'

diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs
@@ -48,6 +48,7 @@ import Primer.Database (
   fromSessionName,
  )
 import Primer.Def (astDefExpr, astDefType, defAST)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.Examples (
   comprehensive,
   even3App,
@@ -462,7 +463,7 @@ test_eval_undo =
       sid <- newSession $ NewSessionReq "a new session" True
       let scope = mkSimpleModuleName "Main"
       step "eval"
-      void $ evalFull' sid (Just 100) $ qualifyName scope "main"
+      void $ evalFull' sid (Just 100) (Just UnderBinders) $ qualifyName scope "main"
       step "insert λ"
       let getMain = do
             p <- getProgram sid

diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs
@@ -81,6 +81,7 @@ import Primer.Database (
   Session,
   SessionName,
  )
+import Primer.Eval (NormalOrderOptions)
 import Primer.JSON (CustomJSON (CustomJSON), PrimerJSON)
 import Primer.Name (Name)
 import Servant.API (FromHttpApiData (parseQueryParam), ToHttpApiData (toQueryParam))
@@ -195,6 +196,11 @@ instance FromHttpApiData Level where
   parseQueryParam = parseQueryParamRead "level"
 instance ToHttpApiData Level where
   toQueryParam = show
+deriving anyclass instance ToParamSchema NormalOrderOptions
+instance FromHttpApiData NormalOrderOptions where
+  parseQueryParam = parseQueryParamRead "NormalOrderOptions"
+instance ToHttpApiData NormalOrderOptions where
+  toQueryParam = show
 parseQueryParamRead :: Read a => Text -> Text -> Either Text a
 parseQueryParamRead m t = maybeToEither ("unknown " <> m <> ": " <> t) $ readMaybe t
 

diff --git a/primer-service/src/Primer/Servant/OpenAPI.hs b/primer-service/src/Primer/Servant/OpenAPI.hs
@@ -23,6 +23,7 @@ import Primer.Core (GVarName, ModuleName)
 import Primer.Database (
   SessionId,
  )
+import Primer.Eval (NormalOrderOptions)
 import Primer.Finite (Finite)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.OpenAPI ()
@@ -124,6 +125,7 @@ data SessionAPI mode = SessionAPI
           :> Summary "Evaluate the named definition to normal form (or time out)"
           :> OperationId "eval-full"
           :> QueryParam "stepLimit" (Finite 0 EvalFullStepLimit)
+          :> QueryParam "closed" NormalOrderOptions
           :> ReqBody '[JSON] GVarName
           :> Post '[JSON] EvalFullResp
   , undo ::

diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json
@@ -1452,6 +1452,18 @@
                             "minimum": 0,
                             "type": "integer"
                         }
+                    },
+                    {
+                        "in": "query",
+                        "name": "closed",
+                        "required": false,
+                        "schema": {
+                            "enum": [
+                                "UnderBinders",
+                                "StopAtBinders"
+                            ],
+                            "type": "string"
+                        }
                     }
                 ],
                 "requestBody": {
@@ -1475,7 +1487,7 @@
                         "description": ""
                     },
                     "400": {
-                        "description": "Invalid `body` or `stepLimit`"
+                        "description": "Invalid `body` or `closed` or `stepLimit`"
                     },
                     "404": {
                         "description": "`sessionId` not found"