Skip to content

Commit

Permalink
Make Cryptol REPL accept input lines containing only comments.
Browse files Browse the repository at this point in the history
Fixes #838.
  • Loading branch information
Brian Huffman committed Sep 23, 2020
1 parent 5a2d770 commit b06c45c
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 2 deletions.
1 change: 1 addition & 0 deletions src/Cryptol/Parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -371,6 +371,7 @@ decls_layout :: { [Decl PName] }
repl :: { ReplInput PName }
: expr { ExprInput $1 }
| let_decl { LetInput $1 }
| {- empty -} { EmptyInput }


--------------------------------------------------------------------------------
Expand Down
5 changes: 3 additions & 2 deletions src/Cryptol/Parser/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -258,10 +258,11 @@ data PrimType name = PrimType { primTName :: Located name
, primTFixity :: Maybe Fixity
} deriving (Show,Generic,NFData)

-- | Input at the REPL, which can either be an expression or a @let@
-- statement.
-- | Input at the REPL, which can be an expression, a @let@
-- statement, or empty (possibly a comment).
data ReplInput name = ExprInput (Expr name)
| LetInput (Decl name)
| EmptyInput
deriving (Eq, Show)

-- | Export information for a declaration.
Expand Down
3 changes: 3 additions & 0 deletions src/Cryptol/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -359,6 +359,9 @@ evalCmd str = do
-- explicitly make this a top-level declaration, so that it will
-- be generalized if mono-binds is enabled
replEvalDecl decl
P.EmptyInput ->
-- comment or empty input does nothing
pure ()

printCounterexample :: CounterExampleType -> P.Expr P.PName -> [Concrete.Value] -> REPL ()
printCounterexample cexTy pexpr vs =
Expand Down

0 comments on commit b06c45c

Please sign in to comment.