Fix tab completion for :t and :check

.github/ci.sh

@@ -25,7 +25,7 @@ deps() {
 # Finds the cabal-built '$1' executable and copies it to the '$2'
 # directory.
 extract_exe() {
-  exe="$(cabal v2-exec which "$1$EXT")"
+  exe="$(cabal list-bin -v0 "$1")"
   name="$(basename "$exe")"
   echo "Copying $name to $2"
   mkdir -p "$2"
@@ -53,22 +53,23 @@ retry() {
 }
 
 setup_dist_bins() {
-  extract_exe "cryptol" "dist/bin"
-  extract_exe "cryptol-html" "dist/bin"
-  extract_exe "cryptol-remote-api" "dist/bin"
-  extract_exe "cryptol-eval-server" "dist/bin"
+  extract_exe "exe:cryptol" "dist/bin"
+  extract_exe "exe:cryptol-html" "dist/bin"
+  extract_exe "exe:cryptol-remote-api" "dist/bin"
+  extract_exe "exe:cryptol-eval-server" "dist/bin"
   strip dist/bin/cryptol* || echo "Strip failed: Ignoring harmless error"
 }
 
 build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
   cabal v2-update
-  cabal v2-configure -j2 --minimize-conflict-set
+  cabal v2-configure -j2 --minimize-conflict-set --enable-tests
   git status --porcelain
   retry ./cry build exe:cryptol-html "$@" # retry due to flakiness with windows builds
   retry ./cry build exe:cryptol-remote-api "$@"
   retry ./cry build exe:cryptol-eval-server "$@"
+  retry ./cry build test:cryptol-api-tests "$@"
 }
 
 install_system_deps() {

.github/workflows/ci.yml

@@ -151,8 +151,13 @@ jobs:
         run: .github/ci.sh build
 
       - shell: bash
+        name: Extract Cryptol executables to dist/bin/
         run: .github/ci.sh setup_dist_bins
 
+      - shell: bash
+        name: Extract Cryptol API test suite executable to bin/
+        run: .github/ci.sh extract_exe "test:cryptol-api-tests" "bin"
+
       - shell: bash
         run: .github/ci.sh check_docs
         if: runner.os != 'Windows'
@@ -271,6 +276,10 @@ jobs:
         os: [ubuntu-22.04, macos-14, windows-2019]
         continue-on-error: [false]
         include:
+          - suite: api-tests
+            target: ''
+            os: ubuntu-22.04
+            continue-on-error: false
           - suite: rpc
             target: ''
             os: ubuntu-22.04
@@ -358,6 +367,7 @@ jobs:
           chmod +x dist/bin/cryptol
           chmod +x dist/bin/cryptol-remote-api
           chmod +x dist/bin/cryptol-eval-server
+          chmod +x bin/cryptol-api-tests
           chmod +x bin/test-runner
           .github/ci.sh install_system_deps
           .github/ci.sh deps bin/abc*
@@ -393,6 +403,13 @@ jobs:
           export PATH=$PWD/bin:$PWD/dist/bin:$PATH
           cryptol-remote-api/run_rpc_tests.sh
 
+      - if: matrix.suite == 'api-tests'
+        shell: bash
+        continue-on-error: ${{ matrix.continue-on-error }}
+        run: |
+          export PATH=$PWD/bin:$PWD/dist/bin:$PATH
+          ./bin/cryptol-api-tests
+
   build-push-image:
     runs-on: ubuntu-22.04
     needs: [config]

CHANGES.md

@@ -21,6 +21,9 @@
   invoked as `:dumptests - <EXPR>` allowing for easier experimentation and
   testing.
 
+* The REPL properly supports tab completion for the `:t` and `:check` commands.
+  ([#1780](https://github.com/GaloisInc/cryptol/issues/1780))
+
 # 3.2.0 -- 2024-08-20
 
 ## Language changes

api-tests/Main.hs

@@ -0,0 +1,114 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module Main (main) where
+
+import Data.Foldable (traverse_)
+import System.Console.Haskeline.Completion (Completion(..))
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import qualified Cryptol.REPL.Command as REPL
+import qualified Cryptol.REPL.Monad as REPL
+import Cryptol.REPL.Monad (REPL)
+import Cryptol.Utils.Logger (quietLogger)
+import Cryptol.Utils.PP (pp)
+
+import REPL.Haskeline (cryptolCommand)
+
+main :: IO ()
+main = defaultMain $
+  testGroup "Cryptol API tests"
+    [ testGroup "Tab completion tests" $
+      map (uncurry replTabCompletionTestCase)
+        [ (":ch", ":check")
+        , (":check", ":check")
+        , (":check ", ":check ")
+        , (":check rev", ":check reverse")
+        , (":check-docstrings", ":check-docstrings ")
+        , (":check-docstrings ", ":check-docstrings ")
+        , (":t", ":t")
+        , (":t rev", ":t reverse")
+        , (":time", ":time ")
+        , (":time ", ":time ")
+        , (":time rev", ":time reverse")
+        , (":type", ":type ")
+        , (":type ", ":type ")
+        , (":type rev", ":type reverse")
+        ]
+    ]
+
+-- | Assert a property in the 'REPL' monad and turn it into a test case.
+replTestCase :: TestName -> REPL () -> TestTree
+replTestCase name replAssertion =
+  testCase name $
+  REPL.runREPL
+    False       -- Don't use batch mode
+    False       -- Disable call stacks
+    quietLogger -- Ignore all log messages
+    replAssertion
+
+-- | Assert that the REPL will tab-complete the given input in one specific way.
+replTabCompletionTestCase ::
+  -- | The input before the cursor just prior to hitting the tab key.
+  String ->
+  -- | The expected terminal input after hitting the tab key. Note that although
+  -- this is specified as a single 'String', this may actually correspond to
+  -- multiple Haskeline 'Completion's under the hood. See the comments below for
+  -- details on how multiple 'Completion's are resolved to a single 'String'.
+  String ->
+  TestTree
+replTabCompletionTestCase beforeTab afterTabExpected =
+  replTestCase (show beforeTab ++ " --> " ++ show afterTabExpected) $
+  do -- Load the prelude so that the REPL knows how to tab-complete prelude
+     -- definitions.
+     REPL.loadPrelude
+     -- Perform the actual tab completion. (Oddly, Haskeline requires that the
+     -- input to the left of the cursor should be reversed.)
+     (_input, completions) <- cryptolCommand (reverse beforeTab, "")
+     -- Check that the results match what is expected. We have to do a bit of
+     -- additional work that Haskeline does not do:
+     --
+     -- 1. If there is exactly one Completion and its replacement value is
+     --    empty, then Haskeline will add a space character to the end of the
+     --    input on the terminal. Oddly, this space character is /not/ added in
+     --    the Completion itself. As such, we have to add this ourselves.
+     --
+     -- 2. If there are multiple completions, then Haskeline will complete the
+     --    terminal input up to the longest common prefix of all the
+     --    completions' replacement strings. As such, we compute this longest
+     --    common prefix ourselves.
+     REPL.io $
+       case completions of
+         [] -> assertFailure "Expected tab completions, but received none"
+         [completion] ->
+           do assertFinished completion
+              let replace = replacement completion
+                  afterTabActual
+                    | null replace = -- See (1) above
+                                     beforeTab ++ " "
+                    | otherwise    = beforeTab ++ replace
+              afterTabExpected @=? afterTabActual
+         _:_ ->
+           do traverse_ assertFinished completions
+              let replaceLcp =
+                    -- See (2) above
+                    longestCommonPrefix (map replacement completions)
+                  afterTabActual = beforeTab ++ replaceLcp
+              afterTabExpected @=? afterTabActual
+  `REPL.catch`
+    -- If something goes wrong run running the REPL, report it as a test
+    -- failure.
+    \x -> REPL.io $ assertFailure $ show $ pp x
+  where
+    assertFinished :: Completion -> Assertion
+    assertFinished completion =
+      assertBool ("Tab completion for " ++ display completion ++ " finished")
+                 (isFinished completion)
+
+-- | Compute the longest common prefix in a list of lists.
+longestCommonPrefix :: forall a. Eq a => [[a]] -> [a]
+longestCommonPrefix [] = []
+longestCommonPrefix s = foldr1 lcp s
+  where
+    lcp :: [a] -> [a] -> [a]
+    lcp xs ys = map fst $ takeWhile (uncurry (==))
+                        $ zip xs ys

cryptol/REPL/Haskeline.hs → cryptol-repl-internal/REPL/Haskeline.hs

@@ -225,20 +225,52 @@ cryptolCommand cursor@(l,r)
   | ":" `isPrefixOf` l'
   , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of
 
-      [c] | null rest && not (any isSpace l') -> do
+      [c] | cursorRightAfterCmd rest ->
             return (l, cmdComp cmd c)
-          | otherwise -> do
-            (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r)
-            return (unwords [rest', reverse cmd],cs)
-
-      cmds ->
-        return (l, concat [ cmdComp l' c | c <- cmds ])
+          | otherwise ->
+            completeCmdArgument cmd rest c
+
+      cmds
+        -- If the command name is a prefix of multiple commands, then as a
+        -- special case, check if (1) the name matches one command exactly, and
+        -- (2) there is already some input for an argument. If so, proceed to
+        -- tab-complete that argument. This ensures that something like
+        -- `:check rev` will complete to `:check reverse`, even though the
+        -- command name `:check` is a prefix for both the `:check` and
+        -- `:check-docstrings` commands (#1781).
+        | [c] <- nub (findCommandExact cmd)
+        , not (cursorRightAfterCmd rest) ->
+          completeCmdArgument cmd rest c
+
+        | otherwise ->
+          return (l, concat [ cmdComp l' c | c <- cmds ])
   -- Complete all : commands when the line is just a :
   | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ])
   | otherwise = completeExpr cursor
   where
   l' = sanitize (reverse l)
 
+  -- Check if the cursor is positioned immediately after the input for the
+  -- command, without any command arguments typed in after the command's name.
+  cursorRightAfterCmd ::
+    String
+      {- The rest of the input after the command. -} ->
+    Bool
+  cursorRightAfterCmd rest = null rest && not (any isSpace l')
+
+  -- Perform tab completion for a single argument to a command.
+  completeCmdArgument ::
+    String
+      {- The name of the command as a String. -} ->
+    String
+      {- The rest of the input after the command. -} ->
+    CommandDescr
+      {- The description of the command. -} ->
+    REPL (String, [Completion])
+  completeCmdArgument cmd rest c =
+    do (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r)
+       return (unwords [rest', reverse cmd],cs)
+
 -- | Generate completions from a REPL command definition.
 cmdComp :: String -> CommandDescr -> [Completion]
 cmdComp prefix c = do

cryptol.cabal

@@ -254,18 +254,22 @@ library
   if flag(relocatable)
       cpp-options: -DRELOCATABLE
 
-executable cryptol
-  Default-language:
-    Haskell2010
-  Main-is:             Main.hs
-  hs-source-dirs:      cryptol
+-- The portions of the Cryptol REPL that are specific to the Cryptol executable.
+-- We factor this out into a separate internal library because (1) it has some
+-- dependencies (e.g., ansi-terminal and haskeline) that the Cryptol library
+-- does not need to depend on, and (2) we want to be able to test this code in
+-- the cryptol-api-tests test suite.
+library cryptol-repl-internal
+  exposed-modules:     REPL.Haskeline
+                       REPL.Logo
   Autogen-modules:     Paths_cryptol
-
-  Other-modules:       OptParser,
-                       REPL.Haskeline,
-                       REPL.Logo,
-                       Paths_cryptol
-
+  Other-modules:       Paths_cryptol
+  hs-source-dirs:      cryptol-repl-internal
+  default-language:    Haskell2010
+  GHC-options:         -Wall -O2
+  if os(linux) && flag(static)
+      ld-options: -static -pthread
+      ghc-options: -optl-fuse-ld=bfd
   build-depends:       ansi-terminal
                      , base
                      , base-compat
@@ -278,6 +282,19 @@ executable cryptol
                      , monad-control
                      , text
                      , transformers
+
+executable cryptol
+  Default-language:
+    Haskell2010
+  Main-is:             Main.hs
+  hs-source-dirs:      cryptol
+  Other-modules:       OptParser
+  build-depends:       base
+                     , base-compat
+                     , cryptol
+                     , cryptol-repl-internal
+                     , directory
+                     , filepath
   GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
   if impl(ghc >= 8.0.1)
      ghc-options: -Wno-redundant-constraints
@@ -315,6 +332,26 @@ executable check-exercises
                      , temporary
                      , text
   GHC-options: -Wall
+
+-- Test cases that require the use of the Cryptol API to test effectively. Most
+-- other test cases should be added to the integration tests (which only require
+-- the Cryptol executable and/or the REPL) under tests/.
+test-suite cryptol-api-tests
+  type:                exitcode-stdio-1.0
+  main-is:             Main.hs
+  hs-source-dirs:      api-tests
+  default-language:    Haskell2010
+  GHC-options:         -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
+  if os(linux) && flag(static)
+      ld-options: -static -pthread
+      ghc-options: -optl-fuse-ld=bfd
+  build-depends:       base
+                     , cryptol
+                     , cryptol-repl-internal
+                     , haskeline
+                     , tasty
+                     , tasty-hunit
+
 benchmark cryptol-bench
   type:                exitcode-stdio-1.0
   main-is:             Main.hs