Fix/refine

app/Main.hs

@@ -1,5 +1,6 @@
-{-# LANGUAGE OverloadedStrings #-}
+
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Main where
 
@@ -8,18 +9,18 @@ import Pretty ()
 import System.Console.GetOpt
 import System.Environment
 import Prelude
-import Server (run)
+import Server (runOnPort, runOnStdio)
 
 main :: IO ()
 main = do
   (Options mode port, _) <- getArgs >>= parseOpts
   case mode of
     ModeHelp -> putStrLn $ usageInfo usage options
     ModeLSP -> do
-      _ <- run False port
+      _ <- runOnStdio "/Users/vince/Documents/gcl-vscode/server_log.txt"
       return ()
     ModeDev -> do
-      _ <- run True port
+      _ <- runOnPort port
       return ()
 
 --------------------------------------------------------------------------------

examples/divmod.gcl

@@ -6,6 +6,10 @@ var q, b, r : Int
 b := B
 { PowOf2 b, bnd: A - b }
 do b ≤ A -> b := b * 2 od
+
+[!
+
+!]
 { PowOf2 b  ∧  b > A }
 
 q, r := 0, A

examples/factor.gcl

@@ -3,9 +3,15 @@ var p, x, y, n : Int
 var mod : Int -> Int -> Int
 
 {:  P = x * y + p = N
-    Q = x > 0 ∧ y > 0
+    Q = x > 0 ∧ y > 0 ∧ 1 > 0
 :}
+p := p + 1
+[!
 
+!]
+[!
+
+!]
 p,x,y := N-1, 1, 1
 
 { P ∧ Q, bnd: p }

examples/fastmul_with_holes.gcl

@@ -0,0 +1,30 @@
+con A, B : Int { A ≥ 0 ∧ B ≥ 0 }
+con even, odd : Int -> Bool
+var r, a, b : Int
+
+{: INV = a * b + r = A * B ∧ 0 ≤ b :}
+
+a, b, r := A, B, 0
+{ INV, bnd: b }
+do b ≠ 0 ->
+    if even b -> 
+        b := b / 2
+    | odd b ->
+        a := 3
+        a := 3
+        [!
+
+        !]
+        [!
+        ?
+
+        !]
+        r := a
+    fi
+od
+{ r = A * B }
+
+
+
+
+

gcl.cabal

@@ -36,7 +36,7 @@ library
       GCL.WP.Explanation
       GCL.WP.SP
       GCL.WP.Struct
-      GCL.WP.Type
+      GCL.WP.Types
       GCL.WP.Util
       GCL.WP.WP
       Pretty
@@ -45,6 +45,7 @@ library
       Pretty.Concrete
       Pretty.Error
       Pretty.Predicate
+      Pretty.Typed
       Pretty.Util
       Pretty.Variadic
       Render
@@ -54,34 +55,26 @@ library
       Render.Predicate
       Render.Syntax.Abstract
       Render.Syntax.Common
+      Render.Syntax.Typed
       Server
-      Server.CustomMethod
       Server.GoToDefn
       Server.Handler
       Server.Handler.AutoCompletion
-      Server.Handler.CustomMethod
-      Server.Handler.Diagnostic
-      Server.Handler.GoToDefn
+      Server.Handler.GoToDefinition
+      Server.Handler.Guabao.Refine
+      Server.Handler.Guabao.Reload
       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.Initialized
-      Server.Handler2.SemanticTokens
-      Server.Handler2.Utils
+      Server.Handler.Initialized
+      Server.Handler.OnDidChangeTextDocument
+      Server.Handler.SemanticTokens
       Server.Highlighting
       Server.Hover
       Server.IntervalMap
+      Server.Load
       Server.Monad
-      Server.Pipeline
+      Server.Notification.Error
+      Server.Notification.Update
+      Server.PositionMapping
       Server.SrcLoc
       Syntax.Abstract
       Syntax.Abstract.Instances.Json
@@ -105,16 +98,24 @@ library
       Syntax.Parser.Util
       Syntax.Substitution
       Syntax.Typed
+      Syntax.Typed.Instances.Free
+      Syntax.Typed.Instances.Located
+      Syntax.Typed.Instances.Substitution
+      Syntax.Typed.Operator
+      Syntax.Typed.Types
+      Syntax.Typed.Util
   other-modules:
       Paths_gcl
   hs-source-dirs:
       src
   ghc-options: -Wall -Werror=incomplete-patterns -fno-warn-orphans
   build-depends:
-      aeson
+      Diff
+    , aeson
     , base >=4.7 && <5
     , bytestring
     , containers
+    , deepseq
     , free
     , hashable
     , lens
@@ -145,10 +146,12 @@ executable gcl
       app
   ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans
   build-depends:
-      aeson
+      Diff
+    , aeson
     , base >=4.7 && <5
     , bytestring
     , containers
+    , deepseq
     , free
     , gcl
     , hashable
@@ -202,7 +205,7 @@ test-suite gcl-test
       GCL.WP.Explanation
       GCL.WP.SP
       GCL.WP.Struct
-      GCL.WP.Type
+      GCL.WP.Types
       GCL.WP.Util
       GCL.WP.WP
       Pretty
@@ -211,6 +214,7 @@ test-suite gcl-test
       Pretty.Concrete
       Pretty.Error
       Pretty.Predicate
+      Pretty.Typed
       Pretty.Util
       Pretty.Variadic
       Render
@@ -220,34 +224,26 @@ test-suite gcl-test
       Render.Predicate
       Render.Syntax.Abstract
       Render.Syntax.Common
+      Render.Syntax.Typed
       Server
-      Server.CustomMethod
       Server.GoToDefn
       Server.Handler
       Server.Handler.AutoCompletion
-      Server.Handler.CustomMethod
-      Server.Handler.Diagnostic
-      Server.Handler.GoToDefn
+      Server.Handler.GoToDefinition
+      Server.Handler.Guabao.Refine
+      Server.Handler.Guabao.Reload
       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.Initialized
-      Server.Handler2.SemanticTokens
-      Server.Handler2.Utils
+      Server.Handler.Initialized
+      Server.Handler.OnDidChangeTextDocument
+      Server.Handler.SemanticTokens
       Server.Highlighting
       Server.Hover
       Server.IntervalMap
+      Server.Load
       Server.Monad
-      Server.Pipeline
+      Server.Notification.Error
+      Server.Notification.Update
+      Server.PositionMapping
       Server.SrcLoc
       Syntax.Abstract
       Syntax.Abstract.Instances.Json
@@ -271,16 +267,24 @@ test-suite gcl-test
       Syntax.Parser.Util
       Syntax.Substitution
       Syntax.Typed
+      Syntax.Typed.Instances.Free
+      Syntax.Typed.Instances.Located
+      Syntax.Typed.Instances.Substitution
+      Syntax.Typed.Operator
+      Syntax.Typed.Types
+      Syntax.Typed.Util
       Paths_gcl
   hs-source-dirs:
       test
       src
   ghc-options: -Wall -Werror=incomplete-patterns -fno-warn-orphans
   build-depends:
-      aeson
+      Diff
+    , aeson
     , base >=4.7 && <5
     , bytestring
     , containers
+    , deepseq
     , directory
     , filepath
     , free

log.txt

@@ -0,0 +1,22 @@
+=== Log file Start ===
+SInitialized is called.
+STextDocumentDidOpen is called.
+load start
+load start
+load start 2
+load start 3
+loaded file state
+current version determined
+load: source read
+load: file read
+load: source parsed
+load: swept
+load: elaborated
+load: fileState created
+load: fileState saved
+STextDocumentDidOpen is finished.
+
+ ---> Syntax Highlighting
+ ---> Syntax Highlighting
+ ---> Syntax Highlighting
+ ---> Syntax Highlighting<-- Goto Definition

package.yaml

@@ -1,15 +1,15 @@
-name:                gcl
-version:             0.1.0.0
+name: gcl
+version: 0.1.0.0
 #synopsis:
 #description:
-homepage:            https://github.com/scmlab/gcl
-license:             BSD3
-author:              Author name here
-maintainer:          [email protected]
-copyright:           something
-category:            language
+homepage: https://github.com/scmlab/gcl
+license: BSD3
+author: Author name here
+maintainer: [email protected]
+copyright: something
+category: language
 extra-source-files:
-- README.md
+  - README.md
 
 dependencies:
   - base >= 4.7 && < 5
@@ -30,12 +30,14 @@ dependencies:
   - regex-applicative
   - random
   - vector
-  - lsp 
+  - lsp
   - lens
   - multiset
   - transformers
   - template-haskell
   - multistate
+  - deepseq
+  - Diff
 
 library:
   source-dirs: src
@@ -60,7 +62,6 @@ executables:
       - -Werror=incomplete-patterns
       - -fno-warn-orphans
 
-
 tests:
   gcl-test:
     main: Test.hs