Merge branch 'release-v0.6.2'

* release-v0.6.2:
  Bump version and update changelogs
  Fix pretty-printer's layout
  Return well-typed declarations from partially well-typed modules
  Update rzk.nix
  Register the handler for text completion request
  Define a handler for the completions request
  Define default instances for text completion items
  Install the data-default-class package
  Improve order of error message information for LSP
  Fix handling LEM (speedup tope layer solver)
  Output entailment problems in debug mode

docs/docs/getting-started/changelog.md

@@ -6,6 +6,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.6.2 — 2023-09-26
+
+This version contains some improvements in efficiency and also to the language server:
+
+- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see [#102](https://github.com/rzk-lang/rzk/pull/102))
+- Support autocompleting definitions from previous modules (see [#102](https://github.com/rzk-lang/rzk/pull/103))
+  - Well-typed definitions from the same module also work if the module is only partially well-typed!
+- Improve information order in the error messages given in LSP diagnostics (see [#104](https://github.com/rzk-lang/rzk/pull/104))
+
 ## v0.6.1 — 2023-09-24
 
 This version contains a minor fix:

rzk/ChangeLog.md

@@ -6,6 +6,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.6.2 — 2023-09-26
+
+This version contains some improvements in efficiency and also to the language server:
+
+- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see [#102](https://github.com/rzk-lang/rzk/pull/102))
+- Support autocompleting definitions from previous modules (see [#102](https://github.com/rzk-lang/rzk/pull/103))
+  - Well-typed definitions from the same module also work if the module is only partially well-typed!
+- Improve information order in the error messages given in LSP diagnostics (see [#104](https://github.com/rzk-lang/rzk/pull/104))
+
 ## v0.6.1 — 2023-09-24
 
 This version contains a minor fix:

rzk/package.yaml

@@ -1,5 +1,5 @@
 name: rzk
-version: 0.6.1
+version: 0.6.2
 github: 'rzk-lang/rzk'
 license: BSD3
 author: 'Nikolai Kudasov'
@@ -37,6 +37,7 @@ dependencies:
   - filepath
   - stm
   - yaml
+  - data-default-class
 
 ghc-options:
   - -Wall

rzk/rzk.cabal

@@ -5,7 +5,7 @@ cabal-version: 1.12
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.6.1
+version:        0.6.2
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -54,6 +54,7 @@ library
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , data-default-class
     , filepath
     , lens
     , mtl
@@ -91,6 +92,7 @@ executable rzk
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , data-default-class
     , filepath
     , lens
     , mtl
@@ -122,6 +124,7 @@ test-suite doctests
     , base
     , bifunctors
     , bytestring
+    , data-default-class
     , doctest
     , filepath
     , lens
@@ -151,6 +154,7 @@ test-suite rzk-test
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , data-default-class
     , filepath
     , lens
     , mtl

rzk/rzk.nix

@@ -1,26 +1,28 @@
 { mkDerivation, aeson, alex, array, base, bifunctors, bytestring
-, doctest, filepath, Glob, happy, hpack, lens, lib, mtl
-, optparse-generic, QuickCheck, stm, template-haskell, text, yaml
+, data-default-class, doctest, filepath, Glob, happy, hpack, lens
+, lib, mtl, optparse-generic, QuickCheck, stm, template-haskell
+, text, yaml
 }:
 mkDerivation {
   pname = "rzk";
-  version = "0.6.1";
+  version = "0.6.2";
   src = ./.;
   isLibrary = true;
   isExecutable = true;
   libraryHaskellDepends = [
-    aeson array base bifunctors bytestring filepath Glob lens mtl
-    optparse-generic stm template-haskell text yaml
+    aeson array base bifunctors bytestring data-default-class filepath
+    Glob lens mtl optparse-generic stm template-haskell text yaml
   ];
   libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
-    aeson array base bifunctors bytestring filepath Glob lens mtl
-    optparse-generic stm template-haskell text yaml
+    aeson array base bifunctors bytestring data-default-class filepath
+    Glob lens mtl optparse-generic stm template-haskell text yaml
   ];
   executableToolDepends = [ alex happy ];
   testHaskellDepends = [
-    aeson array base bifunctors bytestring doctest filepath Glob lens
-    mtl optparse-generic QuickCheck stm template-haskell text yaml
+    aeson array base bifunctors bytestring data-default-class doctest
+    filepath Glob lens mtl optparse-generic QuickCheck stm
+    template-haskell text yaml
   ];
   testToolDepends = [ alex happy ];
   prePatch = "hpack";

rzk/src/Language/Rzk/Syntax/Print.hs

@@ -1,8 +1,8 @@
 -- File generated by the BNF Converter (bnfc 2.9.4.1).
 
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE CPP                  #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE LambdaCase           #-}
 #if __GLASGOW_HASKELL__ <= 708
 {-# LANGUAGE OverlappingInstances #-}
 #endif
@@ -11,16 +11,13 @@
 
 module Language.Rzk.Syntax.Print where
 
-import Prelude
-  ( ($), (.)
-  , Bool(..), (==), (<)
-  , Int, Integer, Double, (+), (-), (*)
-  , String, (++)
-  , ShowS, showChar, showString
-  , all, elem, foldr, id, map, null, replicate, shows, span
-  )
-import Data.Char ( Char, isSpace )
+import           Data.Char               (Char, isSpace)
 import qualified Language.Rzk.Syntax.Abs
+import           Prelude                 (Bool (..), Double, Int, Integer,
+                                          ShowS, String, all, elem, foldr, id,
+                                          map, null, replicate, showChar,
+                                          showString, shows, span, ($), (*),
+                                          (++), (.), (<), (==))
 
 -- | The top-level printing method.
 
@@ -43,9 +40,9 @@ render d = rend 0 False (map ($ "") $ d []) ""
   rend i p = \case
       "["      :ts -> char '[' . rend i False ts
       "("      :ts -> char '(' . rend i False ts
-      "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
-      "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-      "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+      -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+      -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+      -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
       [";"]        -> char ';'
       ";"      :ts -> char ';' . new i ts
       t  : ts@(s:_) | closingOrPunctuation s
@@ -70,8 +67,8 @@ render d = rend 0 False (map ($ "") $ d []) ""
   new j ts = showChar '\n' . rend j True ts
 
   -- Make sure we are on a fresh line.
-  onNewLine :: Int -> Bool -> ShowS
-  onNewLine i p = (if p then id else showChar '\n') . indent i
+  -- onNewLine :: Int -> Bool -> ShowS
+  -- onNewLine i p = (if p then id else showChar '\n') . indent i
 
   -- Separate given string from following text by a space (if needed).
   space :: String -> ShowS
@@ -124,10 +121,10 @@ printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
 mkEsc :: Char -> Char -> ShowS
 mkEsc q = \case
   s | s == q -> showChar '\\' . showChar s
-  '\\' -> showString "\\\\"
-  '\n' -> showString "\\n"
-  '\t' -> showString "\\t"
-  s -> showChar s
+  '\\'       -> showString "\\\\"
+  '\n'       -> showString "\\n"
+  '\t'       -> showString "\\t"
+  s          -> showChar s
 
 prPrec :: Int -> Int -> Doc -> Doc
 prPrec i j = if j < i then parenth else id
@@ -155,8 +152,8 @@ instance Print (Language.Rzk.Syntax.Abs.VarIdent' a) where
     Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken])
 
 instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where
-  prt _ [] = concatD []
-  prt _ [x] = concatD [prt 0 x]
+  prt _ []     = concatD []
+  prt _ [x]    = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where
@@ -182,7 +179,7 @@ instance Print (Language.Rzk.Syntax.Abs.Command' a) where
     Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Command' a] where
-  prt _ [] = concatD []
+  prt _ []     = concatD []
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where
@@ -201,8 +198,8 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where
     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
-  prt _ [] = concatD []
-  prt _ [x] = concatD [prt 0 x]
+  prt _ []     = concatD []
+  prt _ [x]    = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Param' a) where
@@ -213,8 +210,8 @@ instance Print (Language.Rzk.Syntax.Abs.Param' a) where
     Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")])
 
 instance Print [Language.Rzk.Syntax.Abs.Param' a] where
-  prt _ [] = concatD []
-  prt _ [x] = concatD [prt 0 x]
+  prt _ []     = concatD []
+  prt _ [x]    = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
@@ -231,8 +228,8 @@ instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
     Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where
-  prt _ [] = concatD []
-  prt _ [x] = concatD [prt 0 x]
+  prt _ []     = concatD []
+  prt _ [x]    = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Term' a) where
@@ -292,6 +289,6 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term])
 
 instance Print [Language.Rzk.Syntax.Abs.Term' a] where
-  prt _ [] = concatD []
-  prt _ [x] = concatD [prt 0 x]
+  prt _ []     = concatD []
+  prt _ [x]    = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]

rzk/src/Language/Rzk/VSCode/Handlers.hs

@@ -1,24 +1,36 @@
+{-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
 module Language.Rzk.VSCode.Handlers where
 
 import           Control.Exception             (SomeException, evaluate, try)
+import           Control.Lens
 import           Control.Monad.Cont            (MonadIO (liftIO), forM_)
+import           Data.Default.Class
 import           Data.List                     (sort, (\\))
+import           Data.Maybe                    (fromMaybe)
 import qualified Data.Text                     as T
 import qualified Data.Yaml                     as Yaml
 import           Language.LSP.Diagnostics      (partitionBySource)
+import           Language.LSP.Protocol.Lens    (HasDetail (detail),
+                                                HasDocumentation (documentation),
+                                                HasLabel (label),
+                                                HasParams (params),
+                                                HasTextDocument (textDocument),
+                                                HasUri (uri))
 import           Language.LSP.Protocol.Message
 import           Language.LSP.Protocol.Types
 import           Language.LSP.Server
-import           System.FilePath               ((</>))
+import           System.FilePath               (makeRelative, (</>))
 import           System.FilePath.Glob          (compile, globDir)
 
-import           Data.Maybe                    (fromMaybe)
-import           Language.Rzk.Free.Syntax      (VarIdent)
-import           Language.Rzk.Syntax           (Module, parseModuleFile)
+import           Language.Rzk.Free.Syntax      (RzkPosition (RzkPosition),
+                                                VarIdent (getVarIdent))
+import           Language.Rzk.Syntax           (Module, VarIdent' (VarIdent),
+                                                parseModuleFile, printTree)
 import           Language.Rzk.VSCode.Env
 import           Language.Rzk.VSCode.State     (ProjectConfig (include))
 import           Rzk.TypeCheck
@@ -121,7 +133,7 @@ typecheckFromConfigFile = do
                       (Just [])                 -- related information
                       Nothing                   -- data that is preserved between different calls
       where
-        msg = ppTypeErrorInScopedContext' err
+        msg = ppTypeErrorInScopedContext' TopDown err
 
         extractLineNumber :: TypeErrorInScopedContext var -> Maybe Int
         extractLineNumber (PlainTypeError e)    = do
@@ -142,3 +154,40 @@ typecheckFromConfigFile = do
                       Nothing
                       (Just [])
                       Nothing
+
+instance Default T.Text where def = ""
+instance Default CompletionItem
+instance Default CompletionItemLabelDetails
+
+provideCompletions :: Handler LSP 'Method_TextDocumentCompletion
+provideCompletions req res = do
+  root <- getRootPath
+  let rootDir = fromMaybe "/" root
+  cachedModules <- getCachedTypecheckedModules
+  let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri
+  -- Take all the modules up to and including the currently open one
+  let modules = takeWhileInc ((/= currentFile) . fst) cachedModules
+        where
+          takeWhileInc _ [] = []
+          takeWhileInc p (x:xs)
+            | p x       = x : takeWhileInc p xs
+            | otherwise = [x]
+
+  let items = concatMap (declsToItems rootDir) modules
+  res $ Right $ InL items
+  where
+    declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]
+    declsToItems root (path, decls) = map (declToItem root path) decls
+    declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem
+    declToItem rootDir path (Decl name type' _ _ _) = def
+      & label .~ T.pack (printTree $ getVarIdent name)
+      & detail ?~ T.pack (show type')
+      & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $
+          "---\nDefined" ++
+          (if line > 0 then " at line " ++ show line else "")
+          ++ " in *" ++ makeRelative rootDir path ++ "*")
+      where
+        (VarIdent pos _) = getVarIdent name
+        (RzkPosition _path pos') = pos
+        line = maybe 0 fst pos'
+        _col = maybe 0 snd pos'

rzk/src/Language/Rzk/VSCode/Lsp.hs

@@ -58,6 +58,7 @@ handlers =
     --         ms = mkMarkdown "Hello world"
     --         range' = Range pos pos
     --     responder (Right $ InL rsp)
+    , requestHandler SMethod_TextDocumentCompletion provideCompletions
     , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do
         let doc = req ^. params . textDocument . uri . to toNormalizedUri
         mdoc <- getVirtualFile doc

rzk/src/Rzk/Main.hs

@@ -35,7 +35,7 @@ main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categor
         putStrLn "An error occurred when typechecking!"
         putStrLn $ unlines
           [ "Type Error:"
-          , ppTypeErrorInScopedContext' err
+          , ppTypeErrorInScopedContext' BottomUp err
           ]
         exitFailure
       Right _declsByPath -> putStrLn "Everything is ok!"
@@ -93,7 +93,7 @@ typecheckString moduleString = do
       , "Rendering type error... (this may take a few seconds)"
       , unlines
         [ "Type Error:"
-        , ppTypeErrorInScopedContext' err
+        , ppTypeErrorInScopedContext' BottomUp err
         ]
       ]
     Right _ -> pure "Everything is ok!"