fix to pass type check

gcl.cabal

@@ -65,9 +65,16 @@ library
       Server.Handler.Hover
       Server.Handler2
       Server.Handler2.CustomMethod
+      Server.Handler2.CustomMethod.HelloWorld
+      Server.Handler2.CustomMethod.InsertProofTemplate
+      Server.Handler2.CustomMethod.Inspect
+      Server.Handler2.CustomMethod.Refine
+      Server.Handler2.CustomMethod.Reload
+      Server.Handler2.CustomMethod.SubstituteRedex
+      Server.Handler2.CustomMethod.Utils
       Server.Handler2.GoToDefinition
       Server.Handler2.Hover
-      Server.Handler2.TextDocumentSemanticTokensFull
+      Server.Handler2.SemanticTokens
       Server.Handler2.Utils
       Server.Highlighting
       Server.Hover
@@ -222,9 +229,16 @@ test-suite gcl-test
       Server.Handler.Hover
       Server.Handler2
       Server.Handler2.CustomMethod
+      Server.Handler2.CustomMethod.HelloWorld
+      Server.Handler2.CustomMethod.InsertProofTemplate
+      Server.Handler2.CustomMethod.Inspect
+      Server.Handler2.CustomMethod.Refine
+      Server.Handler2.CustomMethod.Reload
+      Server.Handler2.CustomMethod.SubstituteRedex
+      Server.Handler2.CustomMethod.Utils
       Server.Handler2.GoToDefinition
       Server.Handler2.Hover
-      Server.Handler2.TextDocumentSemanticTokensFull
+      Server.Handler2.SemanticTokens
       Server.Handler2.Utils
       Server.Highlighting
       Server.Hover

src/Server/CustomMethod.hs

@@ -71,6 +71,7 @@ data ReqKind
   | ReqReload
   | ReqRefine2 Range Text
   | ReqInsertProofTemplate Range Text
+  deriving Generic
 
 instance FromJSON ReqKind
 

src/Server/Handler2/CustomMethod.hs

@@ -21,6 +21,7 @@ import qualified Server.Handler2.CustomMethod.InsertProofTemplate
 import qualified Server.Handler2.CustomMethod.SubstituteRedex
                                                         as SubstituteRedex (handler)
 import qualified Server.Handler2.CustomMethod.HelloWorld as HelloWorld (handler)
+import qualified Data.Text as Text
 
 
 handler :: JSON.Value -> (Response -> ServerM ()) -> ServerM ()
@@ -40,9 +41,9 @@ handler params responder = do
       case reqKind of
         ReqReload                         -> Reload.handler filePath respondResult reportError
         ReqInspect range                  -> Inspect.handler range respondResult reportError
-        ReqRefine' range text             -> Refine.slowHandler range text respondResult reportError
+        ReqRefine2 range text             -> Refine.slowHandler range text respondResult reportError
         ReqInsertProofTemplate range hash -> InsertProofTemplate.slowHandler filePath range hash respondResult reportError
-        ReqSubstitute redexNumber         -> SubstituteRedex.handler redexNumber respondResult reportError
+        ReqSubstitute redexNumber         -> SubstituteRedex.handler filePath redexNumber respondResult reportError
         ReqHelloWorld range               -> HelloWorld.handler range respondResult reportError
         _                                 -> reportError (Others "Not implemented yet.")
       where

src/Server/Handler2/CustomMethod/HelloWorld.hs

@@ -11,6 +11,9 @@ import Error (Error(..))
 
 import Server.Monad (ServerM)
 import Server.Handler2.Utils
+import Server.CustomMethod (ResKind (..))
+import Data.Loc (Pos (..), posFile, posLine, posCol, posCoff)
+import Server.Handler.Diagnostic (makeDiagnostic)
 
 
 handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()

src/Server/Handler2/CustomMethod/InsertProofTemplate.hs

@@ -1,3 +1,6 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Server.Handler2.CustomMethod.InsertProofTemplate (slowHandler) where
 
@@ -8,27 +11,28 @@ import qualified Data.List as List
 import Data.Loc.Range (Range (..), rangeFile)
 import Render.Predicate (exprOfPred)
 import GCL.Predicate (PO(..))
-import Pretty (docToText)
+import Pretty (docToText, Pretty (..))
 
 import Server.Monad (ServerM, LoadedProgram(..))
 import Server.Handler2.Utils
-import Server.Handler2.CustomMethod.Utils
 import Server.Handler2.CustomMethod.Reload as Reload
+import Server.CustomMethod (ResKind)
+import Error (Error (..))
 
 slowHandler :: FilePath -> Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
 slowHandler sourceFilePath rangeToInsertProof proofObligationHash onFinish onError = do
   -- reload source
-  reload sourceFilePath (\loadedProgram -> do
+  Reload.reload sourceFilePath (\loadedProgram -> do
       -- find proof obligation by hash
       let proofObligations :: [PO] = _proofObligations loadedProgram
       case findProofObligationByHash proofObligations proofObligationHash of
         Nothing -> onError (Others "Proof obligation not found.")
         Just proofObligation -> do
           -- insert proof template
           let proofTemplate :: Text = makeProofTemplate proofObligation
-          editText rangeToInsertProof ("\n\n" <> template) do
+          editText rangeToInsertProof ("\n\n" <> proofTemplate) do
             -- reload, send diagnostics and respond hint updates
-            Reload.handler filepath onFinsih onError
+            Reload.handler sourceFilePath onFinish onError
     ) onError
   where
     findProofObligationByHash :: [PO] -> Text -> Maybe PO

src/Server/Handler2/CustomMethod/Inspect.hs

@@ -5,14 +5,17 @@ import Data.Loc.Range (Range (..), rangeFile)
 
 import Server.Handler2.Utils (dumpProgram)
 import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram)
+import Server.CustomMethod (ResKind)
+import Server.Monad (ServerM)
+import Error (Error (..))
 
 handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
 handler rangeToInspect onFinish onError = do
-  let filePath :: FilePath = rangeFile range
+  let filePath :: FilePath = rangeFile rangeToInspect
   maybeLoadedProgram <- dumpProgram filePath
   case maybeLoadedProgram of
     Nothing -> onError (Others "Please reload before inspect.")
     Just loadedProgam -> do
-      response <- sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgam rangeToInspect
+      response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgam (Just rangeToInspect)
       onFinish response
 

src/Server/Handler2/CustomMethod/Refine.hs

@@ -1,48 +1,56 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Server.Handler2.CustomMethod.Refine (slowHandler) where
 
 import Data.Loc.Range (Range (..), rangeFile)
 
-import Server.Monad (ServerM)
+import Server.Monad (ServerM, LoadedProgram (..))
 import Server.Handler2.Utils
 import Server.Handler2.CustomMethod.Utils
 import Server.Handler2.CustomMethod.Reload as Reload
+import Data.Text (Text)
+import Server.CustomMethod (ResKind)
+import Error (Error)
 
 slowHandler :: Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
 slowHandler specRange filledText onFinish onError = do
   -- remove brackets
   editText specRange filledText do
     -- reload source
-    Reload.handler filepath onFinsih onError
+    let filePath :: FilePath = rangeFile specRange
+    Reload.handler filePath onFinish onError
 
 -- 檢查 text typecheck 過了的話
 -- 更新 loadedProgram (concrete/ abstract/ pos/ specs ...etc)
 -- (會比重新load有效率嗎？laziness?
 -- 用新的loadedProgram更新view
 
-handler :: Range -> Text -> ServerM ()
-handler specRange filledText = do
-  let filepath :: FilePath = rangeFile specRange
-  maybeLoadedProgram <- dumpProgram filepath
-  case maybeLoadedProgram of
-    Nothing -> _
-    Just loadedProgram -> do
-      let (refinedProgram, newRangeToFocus) = refine loadedProgram specRange filledText
-      _ <- cacheProgram filePath refinedProgram
-      response <- sendDiagnosticsAndMakeResponseFromLoadedProgram refinedProgram newRangeToFocus
-      onFinish response
+-- handler :: Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
+-- handler specRange filledText onFinish onError = do
+--   let filePath :: FilePath = rangeFile specRange
+--   maybeLoadedProgram <- dumpProgram filePath
+--   case maybeLoadedProgram of
+--     Nothing -> _
+--     Just loadedProgram -> do
+--       let (refinedProgram, newRangeToFocus) = refine loadedProgram specRange filledText
+--       _ <- cacheProgram filePath refinedProgram
+--       response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath refinedProgram newRangeToFocus
+--       onFinish response
 
-refine :: LoadedProgram -> Range -> Text -> (LoadedProgram, Maybe Range)
-refine loadedProgram specRange filledText =
-  LoadedProgram
-  { _concreteProgram   = _
-  , _highlightingInfos = _
-  , _abstractProgram   = _
-  , _scopingInfo       = _
-  , _typeCheckingInfo  = _
-  , _proofObligations  = _
-  , _specifiations     = _
-  , _warnings          = _
-  , _redexes           = _
-  , _variableCounter   = _
-  }
+-- refine :: LoadedProgram -> Range -> Text -> (LoadedProgram, Maybe Range)
+-- refine loadedProgram specRange filledText =
+--   ( LoadedProgram
+--       { _concreteProgram   = _
+--       , _highlightingInfos = _
+--       , _abstractProgram   = _
+--       , _scopingInfo       = _
+--       , _typeCheckingInfo  = _
+--       , _proofObligations  = _
+--       , _specifiations     = _
+--       , _warnings          = _
+--       , _redexes           = _
+--       , _variableCounter   = _
+--       }
+--   , _
+--   )

src/Server/Handler2/CustomMethod/Reload.hs

@@ -1,12 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE BlockArguments #-}
-module Server.Handler2.CustomMethod.Reload (handler) where
+module Server.Handler2.CustomMethod.Reload (handler, reload) where
 
-import qualified Data.Aeson.Types as JSON
-
-
-import Data.Loc.Range (Range (..), rangeStart, withinRange, fromLoc)
 import Data.Text (Text)
 
 import qualified GCL.WP                        as WP
@@ -21,30 +17,23 @@ import Data.Loc hiding ( fromLoc )
 import GCL.Type (ScopeTreeZipper)
 import qualified GCL.Type as TypeChecking
 import qualified Data.List as List
-import Syntax.Abstract (Expr)
-import GCL.WP.Type (StructWarning)
-import GCL.Predicate (PO (..), Spec (..))
-import Data.IntMap (IntMap)
-import Render (Render (..), RenderSection (..))
-import Data.String (fromString)
 import Data.List (sortOn)
-import Data.Maybe (mapMaybe)
 
-import Server.CustomMethod (Response (..), Request (..), ReqKind (..), ResKind (..))
+import Server.CustomMethod (ResKind (..))
 import Server.Monad (ServerM, LoadedProgram (..))
-import Server.Handler.Diagnostic (makeDiagnostic, Collect (collect))
 import Server.Highlighting (collectHighlighting)
 import Server.Hover (collectHoverInfo)
 import Server.GoToDefn (collectLocationLinks)
 
 import Server.Handler2.Utils
 import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram)
+import Data.Loc.Range (Range, rangeStart)
 
 
 handler :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
-handler filepath onFinsih onError = do
-  reload filepath (\loadedProgram -> do
-      response <- sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgram Nothing
+handler filePath onFinsih onError = do
+  reload filePath (\loadedProgram -> do
+      response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgram Nothing
       onFinsih response
     ) onError
 
@@ -70,18 +59,18 @@ reload filepath onFinish onError = do
                   Left  err -> onError (StructError err)
                   Right (pos, specs, warnings, redexes, counter) -> do
                     -- cache all results
-                    loadedProgram = LoadedProgram
-                      { _concreteProgram   = concrete
-                      , _highlightingInfos = collectHighlighting concrete
-                      , _abstractProgram   = abstract
-                      , _scopingInfo       = collectLocationLinks abstract
-                      , _typeCheckingInfo  = collectHoverInfo abstract scopeTree
-                      , _proofObligations  = List.sort pos
-                      , _specifiations     = sortOn locOf specs
-                      , _warnings          = warnings
-                      , _redexes           = redexes
-                      , _variableCounter   = counter
-                      }
+                    let loadedProgram = LoadedProgram
+                          { _concreteProgram   = concrete
+                          , _highlightingInfos = collectHighlighting concrete
+                          , _abstractProgram   = abstract
+                          , _scopingInfo       = collectLocationLinks abstract
+                          , _typeCheckingInfo  = collectHoverInfo abstract scopeTree
+                          , _proofObligations  = List.sort pos
+                          , _specifiations     = sortOn locOf specs
+                          , _warnings          = warnings
+                          , _redexes           = redexes
+                          , _variableCounter   = counter
+                          }
                     _ <- cacheProgram filepath loadedProgram
                     onFinish loadedProgram
           ) onError

src/Server/Handler2/CustomMethod/SubstituteRedex.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Server.Handler2.CustomMethod.SubstituteRedex (handler) where
 
@@ -7,9 +8,16 @@ 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
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Map (Map)
+import Data.Text (Text)
+import Syntax.Abstract.Types (Expr)
+import qualified Syntax.Abstract.Util as A
+import Control.Monad.State (runState)
+import Render (Render(..))
 
 handler :: FilePath -> Int -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
 handler filePath redexNumber onFinish onError = do
@@ -31,5 +39,5 @@ handler filePath redexNumber onFinish onError = do
                 { _variableCounter = variableCounter'
                 , _redexes         = redexes <> redexesInNewExpr
                 }
-          _ <- cacheLoadedProgram filePath loadedProgram'
-          onFinish [ResSubstitute i (render newExpr)]
+          _ <- cacheProgram filePath loadedProgram'
+          onFinish [ResSubstitute redexNumber (render newExpr)]

src/Server/Handler2/CustomMethod/Utils.hs

@@ -1,17 +1,31 @@
-
+{-# LANGUAGE OverloadedStrings #-}
 module Server.Handler2.CustomMethod.Utils where
+import Server.Monad (LoadedProgram(..), ServerM)
+import qualified Syntax.Abstract as A
+import Data.Loc.Range (Range, fromLoc, withinRange, rangeFile)
+import Syntax.Abstract (Expr)
+import GCL.Predicate (PO (..), Spec (..))
+import GCL.WP.Type (StructWarning)
+import Server.CustomMethod (ResKind (..))
+import Data.Text (Text)
+import Render (Section (..), Render (..), RenderSection (..), Block (..), Deco (..))
+import Server.Handler.Diagnostic (Collect(..))
+import Server.Handler2.Utils (sendDiagnostics, bumpVersion)
+import Data.Maybe (mapMaybe)
+import Data.Loc (locOf)
+import Pretty (toText)
 
-sendDiagnosticsAndMakeResponseFromLoadedProgram :: LoadedProgram -> Maybe Range -> ServerM ()
-sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgram rangeToFocus = do
+sendDiagnosticsAndMakeResponseFromLoadedProgram :: FilePath -> LoadedProgram -> Maybe Range -> ServerM [ResKind]
+sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgram rangeToFocus = do
   -- destructure and get needed data
   let (LoadedProgram
-        _ (A.Program _ _ globalProperties _)
-        _ _ proofObligations specs warnings _ _
-      ) = loadedProgram
+          _ _ (A.Program _ _ globalProperties _ _)
+          _ _ proofObligations specs warnings _ _
+        ) = loadedProgram
 
   -- send warnings as diagnostics
   let diagnostics = concatMap collect warnings
-  sendDiagnostics filepath diagnostics
+  sendDiagnostics filePath diagnostics
 
   -- send reponse for client to render hints
   version' <- bumpVersion

src/Server/Handler2/SemanticTokens.hs

@@ -22,7 +22,7 @@ handler fileUri responder = do
             Left errorMessage    -> respondError (LSP.ResponseError LSP.InternalError errorMessage Nothing)
             Right semanticTokens -> respondResult semanticTokens
   where
-    respondResult :: Maybe LSP.SemanticTokens -> ServerM ()
-    respondResult result = responder (Right result)
-    respondError :: Error -> ServerM ()
+    respondResult :: LSP.SemanticTokens -> ServerM ()
+    respondResult result = responder (Right $ Just result)
+    respondError :: LSP.ResponseError -> ServerM ()
     respondError err = responder (Left err)