fix reload and refine with new sweep on elaborated

examples/fastmul_with_holes.gcl

@@ -13,9 +13,7 @@ do b ≠ 0 ->
 
         !]
     | odd b ->
-        [!
-
-        !]
+        ?
     fi
 od
 { r = A * B }

src/Server/Handler/Guabao/Refine.hs

@@ -13,7 +13,7 @@ import qualified Data.Aeson.Types 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)
+import Server.Monad (ServerM, FileState(..), loadFileState, editTexts, pushSpecs, deleteSpec, Versioned, pushPos, updateIdCounter)
 import Server.Notification.Update (sendUpdateNotification)
 
 import qualified Syntax.Parser                as Parser
@@ -96,16 +96,17 @@ handler _params@RefineParams{filePath, specRange, specText} onSuccess onError =
                         Left err -> onError (TypeError err)
                         Right typedImpl -> do
                           -- get POs and specs
-                          let maxSpecId = getMaximumSpecId specifications
-                          case sweepFragment (maxSpecId + 1) spec typedImpl of
+                          let FileState{idCount} = fileState
+                          case sweepFragment idCount spec typedImpl of
                             Left err -> onError (StructError err)
-                            Right (innerPos, innerSpecs, warnings) -> do
+                            Right (innerPos, innerSpecs, warnings, idCount') -> do
                               -- edit source (dig holes + remove outer brackets)
                               editTexts filePath [(specRange, holessImplText)] do
                                 -- delete outer spec (by id)
                                 deleteSpec filePath spec
                                 -- add inner specs to fileState
                                 let FileState{editedVersion} = fileState
+                                updateIdCounter filePath idCount'
                                 pushSpecs (editedVersion + 1) filePath innerSpecs
                                 pushPos (editedVersion + 1) filePath innerPos
                                 -- send notification to update Specs and POs
@@ -223,8 +224,9 @@ instance Elab [A.Stmt] where
     return (Nothing, typed, mempty)
 
 
-sweepFragment :: Int -> Spec -> [T.Stmt] -> Either StructError ([PO], [Spec], [StructWarning])
-sweepFragment _ (Specification _ pre post _ _) impl =
-   bimap id (\(_, _, (pos, specs, sws, _)) -> (pos, specs, sws))
-    $ runWP (structStmts Primary (pre, Nothing) impl post)
-            (Map.empty, [])  -- SCM: is this right?
+sweepFragment :: Int -> Spec -> [T.Stmt] -> Either StructError ([PO], [Spec], [StructWarning], Int)
+sweepFragment counter (Specification _ pre post _ _) impl = undefined
+-- FIXME: use counter and return updated counter
+  --  bimap id (\(_, _, (pos, specs, sws, _)) -> (pos, specs, sws))
+  --   $ runWP (structStmts Primary (pre, Nothing) impl post)
+  --           (Map.empty, [])  -- SCM: is this right?

src/Server/Load.hs

@@ -67,18 +67,18 @@ load filePath = do
                 load filePath
             Right abstract -> do
               logText "  all holes digged\n"
-              case undefined of -- was "WP.sweep abstract". TODO: fix it
-                Left  err -> do
-                  logText "  sweep error\n"
-                  onError (StructError err)
-                Right (pos, specs, warnings, redexes, counter) -> do
-                  logText "  abstract program generated\n"
-                  case elaborate abstract of
-                    Left err        -> do
-                      logText "  elaborate error\n"
-                      onError err
-                    Right elaborated -> do
-                      logText "  program elaborated\n"
+              logText "  abstract program generated\n"
+              case elaborate abstract of
+                Left err        -> do
+                  logText "  elaborate error\n"
+                  onError err
+                Right elaborated -> do
+                  logText "  program elaborated\n"
+                  case WP.sweep elaborated of
+                    Left  err -> do
+                      logText "  sweep error\n"
+                      onError (StructError err)
+                    Right (pos, specs, warnings, redexes, idCount) -> do
                       let fileState = FileState
                                         { refinedVersion   = currentVersion
                                         , specifications   = map (\spec -> (currentVersion, spec)) specs
@@ -91,7 +91,7 @@ load filePath = do
                                         , concrete         = concrete
                                         , semanticTokens   = collectHighlighting concrete
                                         , abstract         = abstract
-                                        , variableCounter  = counter
+                                        , idCount          = idCount
                                         , definitionLinks  = collectLocationLinks abstract
                                         , elaborated       = elaborated
                                         , hoverInfos       = collectHoverInfo elaborated
@@ -159,6 +159,3 @@ elaborate abstract = do
   case TypeChecking.runElaboration abstract mempty of
     Left  e -> Left (TypeError e)
     Right typedProgram -> return typedProgram
-
-sweepElaborated :: T.Program -> Either StructError ([PO], [Spec], [StructWarning])
-sweepElaborated elaborated = error "TODO"

src/Server/Monad.hs

@@ -62,7 +62,7 @@ data FileState = FileState
   , concrete         :: Concrete.Program
   , semanticTokens   :: [LSP.SemanticTokenAbsolute]
   , abstract         :: Abstract.Program
-  , variableCounter  :: Int
+  , idCount          :: Int
   , definitionLinks  :: IntervalMap LSP.LocationLink
   , hoverInfos       :: IntervalMap (LSP.Hover, Abstract.Type)
   , elaborated       :: Typed.Program
@@ -119,6 +119,11 @@ bumpVersion :: FilePath -> ServerM ()
 bumpVersion filePath = do
   modifyFileState filePath (\fileState@FileState{editedVersion} -> fileState {editedVersion = editedVersion + 1})
 
+updateIdCounter :: FilePath -> 
+  Int -> ServerM ()
+updateIdCounter filePath count = do
+  modifyFileState filePath (\fileState -> fileState {idCount = count})
+
 saveEditedVersion :: FilePath -> Int -> ServerM ()
 saveEditedVersion filePath version = do
   modifyFileState filePath (\fileState -> fileState {editedVersion = version})