fixing refine

scmlab · Aug 22, 2024 · 5086c86 · 5086c86
1 parent 5fbb7ae
commit 5086c86
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 24 deletions.
diff --git a/src/Server/Handler/Guabao/Refine.hs b/src/Server/Handler/Guabao/Refine.hs
@@ -13,7 +13,7 @@ import qualified Data.Aeson as JSON
 import GHC.Generics ( Generic )
 import Data.Bifunctor ( bimap )
 import Control.Monad.Except           ( runExcept )
-import Server.Monad (ServerM, FileState(..), loadFileState, editTexts, pushSpecs, deleteSpec, Versioned, pushPos, updateIdCounter, logText)
+import Server.Monad (ServerM, FileState(..), loadFileState, editTexts, pushSpecs, deleteSpec, Versioned, pushPos, updateIdCounter, logText, saveFileState)
 import Server.Notification.Update (sendUpdateNotification)
 import Server.Notification.Error (sendErrorNotification)
 
@@ -134,28 +134,36 @@ handler _params@RefineParams{filePath, specLines, implText, implStart} onFinish
                             Left err -> onError (StructError err)
                             Right (innerPos, innerSpecs, warnings, idCount') -> do
                               logText "  swept\n"
+                              -- delete outer spec (by id)
+                              deleteSpec filePath spec
+                              logText "  outer spec deleted (refine)\n"
+                              -- add inner specs to fileState
+                              let FileState{editedVersion} = fileState
+                              updateIdCounter filePath idCount'
+                              logText "  counter updated (refine)\n"
+                              let innerSpecs' = predictAndTranslateSpecRanges innerSpecs
+                              let innerPos' = predictAndTranslatePosRanges innerPos
+                              pushSpecs (editedVersion + 1) filePath innerSpecs'
+                              pushPos (editedVersion + 1) filePath innerPos'
+                              -- let FileState{specifications, proofObligations} = fileState
+                              -- let fileState' = fileState
+                              --                   { specifications = specifications ++ Prelude.map (\spec -> (editedVersion + 1, spec)) innerSpecs'
+                              --                   , proofObligations = proofObligations ++ Prelude.map (\po -> (editedVersion + 1, po)) innerPos'
+                              --                   }
+
+                              -- saveFileState filePath fileState'
+
+                              logText "  new specs and POs added (refine)\n"
+                              -- send notification to update Specs and POs
+                              logText "refine: success\n"
+                              sendUpdateNotification filePath
+                              -- -- clear errors
+                              -- sendErrorNotification filePath []
+                              logText "refine: update notification sent\n"
                               -- edit source (dig holes + remove outer brackets)
-                              editTexts filePath [(specLines, holelessImplText)] do
-                                logText "  text edited (refine)\n"
-                                -- delete outer spec (by id)
-                                deleteSpec filePath spec
-                                logText "  outer spec deleted (refine)\n"
-                                -- add inner specs to fileState
-                                let FileState{editedVersion} = fileState
-                                updateIdCounter filePath idCount'
-                                logText "  counter updated (refine)\n"
-                                let innerSpecs' = predictAndTranslateSpecRanges innerSpecs
-                                let innerPos' = predictAndTranslatePosRanges innerPos
-                                pushSpecs editedVersion filePath innerSpecs'
-                                pushPos editedVersion filePath innerPos'
-                                logText "  new specs and POs added (refine)\n"
-                                -- send notification to update Specs and POs
-                                logText "refine: success\n"
-                                sendUpdateNotification filePath
-                                -- clear errors
-                                sendErrorNotification filePath []
-                                logText "refine: update notification sent\n"
-                                onFinish ()
+                              -- editTexts filePath [(specLines, holelessImplText)] do
+                              --   logText "  text edited (refine)\n"
+                              --   onFinish ()
   logText "refine: end\n"
   where
     onError :: Error -> ServerM ()

diff --git a/src/Server/Monad.hs b/src/Server/Monad.hs
@@ -17,7 +17,7 @@ import           Control.Concurrent             ( Chan
                                                 )
 import           Control.Monad.Reader
 import           Data.IORef                     ( IORef
-                                                , modifyIORef'
+                                                , modifyIORef
                                                 , readIORef
                                                 , newIORef
                                                 )
@@ -111,7 +111,7 @@ loadFileState filePath = do
 saveFileState :: FilePath -> FileState -> ServerM ()
 saveFileState filePath fileState = do
   fileStateRef <- lift $ asks filesState
-  liftIO $ modifyIORef' fileStateRef (Map.insert filePath fileState)
+  liftIO $ modifyIORef fileStateRef (Map.insert filePath fileState)
 
 logFileState :: Show a => FilePath -> (FileState -> a) -> ServerM ()
 logFileState filePath f = do