Clean out the saw-core lexer

CHANGES.md

@@ -12,8 +12,8 @@
 ## Bug fixes
 
 * SAW now accepts Unicode input beyond characters 0..255, including in
-  embedded Cryptol fragments, and allows the same Unicode code points
-  in identifiers as Cryptol.
+  embedded Cryptol fragments and saw-core modules, and allows the same
+  Unicode code points in identifiers as Cryptol.
   It is thus now possible to refer to Cryptol objects whose names
   include extended characters.
   (#2042)

intTests/support/test-and-diff.sh

@@ -106,11 +106,19 @@ run-tests() {
         # We also need to shorten pathnames that contain the current
         # directory, because saw feels the need to expand pathnames
         # (see also saw-script #2082).
+        #
+        # In addition to that we also need to remove the current
+        # directory when it appears in double quotes, at least for
+        # now, because many error prints at the saw-core level seem to
+        # use default Show instances and the saw-core positions carry
+        # the directory and filename separately. This becomes
+        # "interesting" from a quoting perspective...
         sed < $TEST.rawlog > $TEST.log '
             /^\[[0-9][0-9]:[0-9][0-9]:[0-9][0-9]\.[0-9][0-9][0-9]\] /{
                 s/^..............//
             }
             s,'"$CURDIR"'/,,g
+            s,"'"$CURDIR"'",".",g
         '
 
         # Check the output against the expected version.

intTests/test1225/test.sh

@@ -0,0 +1,5 @@
+set -e
+
+! $SAW test1.saw
+$SAW test2.saw
+$SAW test3.saw

intTests/test1225/test1.saw

@@ -0,0 +1,2 @@
+let x = parse_core_mod "Prelude" "True {- ";
+print_term x;

intTests/test1225/test2.saw

@@ -0,0 +1,2 @@
+let x = parse_core_mod "Prelude" " {- -} True";
+print_term x;

intTests/test1225/test3.saw

@@ -0,0 +1,2 @@
+let x = parse_core_mod "Prelude" " {--- ---} True";
+print_term x;

intTests/test2042/test.sh

@@ -4,3 +4,7 @@ $SAW test1.saw
 ! $SAW test2.saw
 ! $SAW test3.saw
 
+$SAW test4.saw
+! $SAW test5.saw
+! $SAW test6.saw
+

intTests/test2042/test4.saw

@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "test4.sawcore";

intTests/test2042/test4.sawcore

@@ -0,0 +1,5 @@
+-- We should now be able to have non-ascii identifiers in saw-core
+module test4 where
+import Prelude;
+lá : Bool;
+lá = True;

intTests/test2042/test5.saw

@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "test5.sawcore";

intTests/test2042/test5.sawcore

@@ -0,0 +1,5 @@
+-- However, we shouldn't be able to use just anything as an identifier.
+module test5 where
+import Prelude;
+😸 : Bool;
+😸 = True;

intTests/test2042/test6.saw

@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "test6.sawcore";

intTests/test2042/test6.sawcore

@@ -0,0 +1,7 @@
+-- Nor should we be able to use just anything _in_ an identifier.
+module test5 where
+import Prelude;
+thingy_hook : Bool;
+thingy_hook = True;
+thingy_🪝 : Bool;
+thingy_🪝 = False;

intTests/test_parse_errors/corelexer001.log.good

@@ -0,0 +1,7 @@
+ Loading file "corelexer001.saw"
+ Stack trace:
+"load_sawcore_from_file" (corelexer001.saw:2:1-2:23)
+Module parsing failed:
+PosPair {_pos = Pos {posBase = ".", posPath = "corelexer001.sawcore", posLine = 1, posCol = 46}, val = UnexpectedToken TEnd}
+
+FAILED

intTests/test_parse_errors/corelexer001.saw

@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "corelexer001.sawcore";

intTests/test_parse_errors/corelexer001.sawcore

@@ -0,0 +1 @@
+-- line comment with no newline at end of file

intTests/test_parse_errors/corelexer002.log.good

@@ -0,0 +1,7 @@
+ Loading file "corelexer002.saw"
+ Stack trace:
+"load_sawcore_from_file" (corelexer002.saw:2:1-2:23)
+Module parsing failed:
+PosPair {_pos = Pos {posBase = ".", posPath = "corelexer002.sawcore", posLine = 1, posCol = 0}, val = ParseError "Unclosed Comment"}
+
+FAILED

intTests/test_parse_errors/corelexer002.saw

@@ -0,0 +1,2 @@
+enable_experimental;
+load_sawcore_from_file "corelexer002.sawcore";

intTests/test_parse_errors/corelexer002.sawcore

@@ -0,0 +1,3 @@
+{-
+ - Unclosed comment
+ -

saw-core/src/Verifier/SAW/Grammar.y

@@ -13,11 +13,8 @@ Portability : non-portable (language extensions)
 -}
 
 module Verifier.SAW.Grammar
-  ( Decl(..)
-  , Term(..)
-  , parseSAW
+  ( parseSAW
   , parseSAWTerm
-  , lexer
   ) where
 
 import Control.Applicative ((<$>))
@@ -28,6 +25,7 @@ import qualified Data.ByteString.Lazy.UTF8 as B
 import Data.Maybe (isJust)
 import Data.Text (Text)
 import qualified Data.Text as Text
+import qualified Data.Text.Lazy as LText
 import Data.Traversable
 import Data.Word
 import Numeric.Natural
@@ -46,7 +44,7 @@ import Verifier.SAW.Lexer
 
 %tokentype { PosPair Token }
 %monad { Parser }
-%lexer { lexer } { PosPair _ TEnd }
+%lexer { lexer >>= } { PosPair _ TEnd }
 %error { parseError }
 %expect 0
 
@@ -251,70 +249,47 @@ rlist1(p) :: { [p] }
 
 {
 data ParseError
-  = UnexpectedLex [Word8]
+  = UnexpectedLex Text
   | UnexpectedToken Token
   | ParseError String
   deriving (Show)
 
-newtype Parser a = Parser { _unParser :: ExceptT (PosPair ParseError) (State AlexInput) a }
+newtype Parser a = Parser { _unParser :: ExceptT (PosPair ParseError) (State LexerState) a }
   deriving (Applicative, Functor, Monad)
 
 addError :: Pos -> ParseError -> Parser a
 addError p err = Parser $ throwError (PosPair p err)
 
-setInput :: AlexInput -> Parser ()
-setInput inp = Parser $ put inp
-
 parsePos :: Parser Pos
 parsePos = Parser $ gets pos
 
-lexer :: (PosPair Token -> Parser a) -> Parser a
-lexer f = do
-  let go prevErr next = do
-        let addErrors =
-              case prevErr of
-                Nothing -> return ()
-                Just (po,l) -> addError po (UnexpectedLex (reverse l))
-        s <- Parser get
-        let inp@(PosPair p (Buffer _ b)) = s
-            end = addErrors >> next (PosPair p TEnd)
-        case alexScan inp 0 of
-          AlexEOF -> end
-          AlexError _ ->
-            case alexGetByte inp of
-              Just (w,inp') -> do
-                setInput inp'
-                case prevErr of
-                  Nothing -> go (Just (p,[w])) next
-                  Just (po,l) -> go (Just (po,w:l)) next
-              Nothing -> end
-          AlexSkip inp' _ -> addErrors >> setInput inp' >> go Nothing next
-          AlexToken inp' l act -> do
-            addErrors
-            setInput inp'
-            let v = act (B.toString (B.take (fromIntegral l) b))
-            next (PosPair p v)
-  let read i tkn =
-        case val tkn of
-          TCmntS -> go Nothing (read (i+1))
-          TCmntE | i > 0 -> go Nothing (read (i-1))
-                 | otherwise -> do
-                     addError (pos tkn) (UnexpectedLex (fmap (fromIntegral . fromEnum) "-}"))
-                     go Nothing (read 0)
-          _ | i > 0 -> go Nothing (read i)
-            | otherwise -> f tkn
-  go Nothing (read (0::Integer))
+lexer :: Parser (PosPair Token)
+lexer = do
+  inp <- Parser get
+  let (inp', errors, result) = lexSAWCore inp
+  Parser $ put inp'
+  let issue (pos, msg) = case msg of
+        InvalidInput chars -> addError pos $ UnexpectedLex chars
+        UnclosedComment -> addError pos $ ParseError "Unclosed Comment"
+        MissingEOL ->
+          -- XXX: this should be a warning but we have no such ability here yet
+          --addWarning pos $ "No newline at end of file"
+          return ()
+  -- XXX: this can only actually throw one error. Fix this up when we
+  -- clean out the error printing infrastructure.
+  mapM issue errors
+  return result
 
 -- | Run parser given a directory for the base (used for making pathname relative),
 -- bytestring to parse, and parser to run.
-runParser :: Parser a -> FilePath -> FilePath -> B.ByteString -> Either (PosPair ParseError) a
-runParser (Parser m) base path b = evalState (runExceptT m) initState
-  where initState = initialAlexInput base path b
+runParser :: Parser a -> FilePath -> FilePath -> LText.Text -> Either (PosPair ParseError) a
+runParser (Parser m) base path txt = evalState (runExceptT m) initState
+  where initState = initialLexerState base path txt
 
-parseSAW :: FilePath -> FilePath -> B.ByteString -> Either (PosPair ParseError) Module
+parseSAW :: FilePath -> FilePath -> LText.Text -> Either (PosPair ParseError) Module
 parseSAW = runParser parseSAW2
 
-parseSAWTerm :: FilePath -> FilePath -> B.ByteString -> Either (PosPair ParseError) Term
+parseSAWTerm :: FilePath -> FilePath -> LText.Text -> Either (PosPair ParseError) Term
 parseSAWTerm = runParser parseSAWTerm2
 
 parseError :: PosPair Token -> Parser a