Skip to content

Commit 452ebe6

Browse files
Merge branch 'develop-remove-parseSExpr'. Close #661.
**Description** The function `copilot-theorem:Copilot.Theorem.Misc.SExpr.parseSExpr` is not used anywhere in the implementation. The module is internal and not exposed to the user, so that function does not have and cannot have any users. **Type** - Bug: unused code included in the implementation. **Additional context** None. **Requester** - Ivan Perez. **Method to check presence of bug** The following search finds mentions of `parseSExpr` in the implementation, showing only the definition: ``` $ grep -nHre 'parseSExpr' copilot**/src copilot**/tests copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs:103:parseSExpr :: String -> Maybe (SExpr String) copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs:104:parseSExpr str = case parse parser "" str of ``` **Expected result** The string should be either empty (the function does not exist) or list further uses. The following dockerfile checks that `parseSExpr` is not mentioned anywhere in the code, after which it prints the message "Success": ```Dockerfile FROM ubuntu:jammy RUN apt-get update RUN apt-get install --yes git SHELL ["/bin/bash", "-c"] CMD git clone $REPO \ && cd $NAME \ && git checkout $COMMIT \ && ! grep -nHre '\<parseSExpr\>' --include='*.hs' \ && echo "Success" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-661 ``` **Solution implemented** Remove the function `Copilot.Theorem.Misc.SExpr.parseSExpr`, as well as any auxiliary functions or imports exclusively needed by that function, if any. Update Cabal file to remove any dependencies no longer necessary due to the removal of `parseSExpr` and any auxiliary functions. **Further notes** None.
2 parents f887b3c + b0d5e2b commit 452ebe6

File tree

3 files changed

+4
-37
lines changed

3 files changed

+4
-37
lines changed

copilot-theorem/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2025-09-07
2+
* Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. (#661)
3+
14
2025-07-07
25
* Version bump (4.5). (#642)
36
* Removed unused pragmas. (#613)

copilot-theorem/copilot-theorem.cabal

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,6 @@ library
5454
, libBF >= 0.6.2 && < 0.7
5555
, mtl >= 2.0 && < 2.4
5656
, panic >= 0.4.0 && < 0.5
57-
, parsec >= 2.0 && < 3.2
5857
, parameterized-utils >= 2.1.1 && < 2.2
5958
, pretty >= 1.0 && < 1.2
6059
, process >= 1.6 && < 1.7

copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs

Lines changed: 1 addition & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,9 @@
22
{-# LANGUAGE Safe #-}
33

44
-- | A representation for structured expression trees, with support for pretty
5-
-- printing and for parsing.
5+
-- printing.
66
module Copilot.Theorem.Misc.SExpr where
77

8-
import Text.ParserCombinators.Parsec
98
import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)
109

1110
import Control.Monad
@@ -70,37 +69,3 @@ toDoc shouldIndent printAtom expr = case expr of
7069
doc $$ indent (toDoc shouldIndent printAtom s)
7170
| otherwise =
7271
doc <+> toDoc shouldIndent printAtom s
73-
74-
-- | Parser for strings of characters separated by spaces into a structured
75-
-- tree.
76-
--
77-
-- Parentheses are interpreted as grouping elements, that is, defining a
78-
-- 'List', which may be empty.
79-
parser :: GenParser Char st (SExpr String)
80-
parser =
81-
choice [try unitP, nodeP, leafP]
82-
83-
where
84-
symbol = oneOf "!#$%&|*+-/:<=>?@^_~."
85-
lonelyStr = many1 (alphaNum <|> symbol)
86-
87-
unitP = string "()" >> return unit
88-
89-
leafP = atom <$> lonelyStr
90-
91-
nodeP = do void $ char '('
92-
spaces
93-
st <- sepBy parser spaces
94-
spaces
95-
void $ char ')'
96-
return $ List st
97-
98-
-- | Parser for strings of characters separated by spaces into a structured
99-
-- tree.
100-
--
101-
-- Parentheses are interpreted as grouping elements, that is, defining a
102-
-- 'List', which may be empty.
103-
parseSExpr :: String -> Maybe (SExpr String)
104-
parseSExpr str = case parse parser "" str of
105-
Left s -> error (show s) -- Nothing
106-
Right t -> Just t

0 commit comments

Comments
 (0)