handler2 - new custom method SubstituteRedex

src/Server/Handler2/CustomMethod.hs

@@ -18,6 +18,8 @@ import qualified Server.Handler2.CustomMethod.Inspect    as Inspect (handler)
 import qualified Server.Handler2.CustomMethod.Refine     as Refine (slowHandler)
 import qualified Server.Handler2.CustomMethod.InsertProofTemplate 
                                                          as InsertProofTemplate (slowHandler)
+import qualified Server.Handler2.CustomMethod.SubstituteRedex
+                                                        as SubstituteRedex (handler)
 import qualified Server.Handler2.CustomMethod.HelloWorld as HelloWorld (handler)
 
 
@@ -42,6 +44,7 @@ handler params responder = do
         ReqInspect range                  -> Inspect.handler range respondResult respondError
         ReqRefine' range text             -> Refine.slowHandler range text respondResult respondError
         ReqInsertProofTemplate range hash -> InsertProofTemplate.slowHandler filePath range hash respondResult respondError
+        ReqSubstitute redexNumber         -> SubstituteRedex.handler redexNumber respondResult respondError
         ReqHelloWorld range               -> HelloWorld.handler range respondResult respondError
         _                                 -> respondError (Others "Not implemented yet.")
       where

src/Server/Handler2/CustomMethod/SubstituteRedex.hs

@@ -0,0 +1,36 @@
+
+module Server.Handler2.CustomMethod.SubstituteRedex (handler) where
+
+import qualified Syntax.Abstract as A
+import Error (Error(..))
+
+import Server.Monad (ServerM, LoadedProgram(..))
+import Server.CustomMethod (ResKind(..))
+import Server.Handler2.Utils
+import Server.Handler2.CustomMethod.Utils
+
+
+import qualified GCL.Substitution as Substitution
+
+handler :: FilePath -> Int -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
+handler filePath redexNumber onFinish onError = do
+  maybeLoadedProgram <- dumpProgram filePath
+  case maybeLoadedProgram of
+    Nothing -> onError (Others "Please reload before inspect.")
+    Just loadedProgram -> do
+      let redexes :: IntMap (Int, A.Expr) = _redexes loadedProgram
+      let abstract :: A.Program = _abstractProgram loadedProgram
+      let variableCounter :: Int = _variableCounter loadedProgram
+      case IntMap.lookup redexNumber redexes of
+        Nothing -> onError (Others "Redex not found.")
+        Just (_, redex) -> do
+          let scope :: Map Text (Maybe Expr) = A.programToScopeForSubstitution abstract
+          let (newExpr, variableCounter') =
+                runState (Substitution.step scope redex) variableCounter
+          let redexesInNewExpr = Substitution.buildRedexMap newExpr
+          let loadedProgram' = loadedProgram
+                { _variableCounter = variableCounter'
+                , _redexes         = redexes <> redexesInNewExpr
+                }
+          _ <- cacheLoadedProgram filePath loadedProgram'
+          onFinish [ResSubstitute i (render newExpr)]