diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 0fbe2107a..7137ed5ce 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -59,6 +59,8 @@ import Paths_cryptol IDENT { $$@(Located _ (Token (Ident [] _) _))} QIDENT { $$@(Located _ (Token Ident{} _))} + SELECTOR { $$@(Located _ (Token (Selector _) _))} + 'include' { Located $$ (Token (KW KW_include) _)} 'import' { Located $$ (Token (KW KW_import) _)} 'as' { Located $$ (Token (KW KW_as) _)} @@ -95,7 +97,7 @@ import Paths_cryptol ')' { Located $$ (Token (Sym ParenR ) _)} ',' { Located $$ (Token (Sym Comma ) _)} ';' { Located $$ (Token (Sym Semi ) _)} - '.' { Located $$ (Token (Sym Dot ) _)} + -- '.' { Located $$ (Token (Sym Dot ) _)} '{' { Located $$ (Token (Sym CurlyL ) _)} '}' { Located $$ (Token (Sym CurlyR ) _)} '<|' { Located $$ (Token (Sym TriL ) _)} @@ -355,6 +357,10 @@ apats_indices :: { ([Pattern PName], [Pattern PName]) } : apats indices { ($1, $2) } | '@' indices1 { ([], $2) } +opt_apats_indices :: { ([Pattern PName], [Pattern PName]) } + : {- empty -} { ([],[]) } + | apats_indices { $1 } + decls :: { [Decl PName] } : decl ';' { [$1] } | decls decl ';' { $2 : $1 } @@ -484,8 +490,8 @@ aexpr :: { Expr PName } no_sel_aexpr :: { Expr PName } : qname { at $1 $ EVar (thing $1) } - | NUM { at $1 $ numLit (tokenType (thing $1)) } - | FRAC { at $1 $ fracLit (tokenType (thing $1)) } + | NUM { at $1 $ numLit (thing $1) } + | FRAC { at $1 $ fracLit (thing $1) } | STRLIT { at $1 $ ELit $ ECString $ getStr $1 } | CHARLIT { at $1 $ ELit $ ECChar $ getChr $1 } | '_' { at $1 $ EVar $ mkUnqual $ mkIdent "_" } @@ -507,9 +513,11 @@ no_sel_aexpr :: { Expr PName } | '<|' poly_terms '|>' {% mkPoly (rComb $1 $3) $2 } sel_expr :: { Expr PName } - : no_sel_aexpr '.' selector { at ($1,$3) $ ESel $1 (thing $3) } - | sel_expr '.' selector { at ($1,$3) $ ESel $1 (thing $3) } + : no_sel_aexpr selector { at ($1,$2) $ ESel $1 (thing $2) } + | sel_expr selector { at ($1,$2) $ ESel $1 (thing $2) } +selector :: { Located Selector } + : SELECTOR { mkSelector `fmap` $1 } poly_terms :: { [(Bool, Integer)] } : poly_term { [$1] } @@ -520,11 +528,6 @@ poly_term :: { (Bool, Integer) } | 'x' {% polyTerm $1 1 1 } | 'x' '^^' NUM {% polyTerm (rComb $1 (srcRange $3)) 1 (getNum $3) } - -selector :: { Located Selector } - : ident { fmap (`RecordSel` Nothing) $1 } - | NUM {% mkTupleSel (srcRange $1) (getNum $1) } - tuple_exprs :: { [Expr PName] } : expr ',' expr { [ $3, $1] } | tuple_exprs ',' expr { $3 : $1 } @@ -535,25 +538,22 @@ rec_expr :: { Either (Expr PName) [Named (Expr PName)] } | '_' '|' field_exprs { Left (EUpd Nothing (reverse $3)) } | field_exprs {% Right `fmap` mapM ufToNamed $1 } -field_expr :: { UpdField PName } - : selector field_how expr { UpdField $2 [$1] $3 } - | sels field_how expr { UpdField $2 $1 $3 } - | sels apats_indices field_how expr - { UpdField $3 $1 (mkIndexedExpr $2 $4) } - | selector apats_indices field_how expr - { UpdField $3 [$1] (mkIndexedExpr $2 $4) } - -field_how :: { UpdHow } - : '=' { UpdSet } - | '->' { UpdFun } - -sels :: { [ Located Selector ] } - : sel_expr {% selExprToSels $1 } - field_exprs :: { [UpdField PName] } : field_expr { [$1] } | field_exprs ',' field_expr { $3 : $1 } +field_expr :: { UpdField PName } + : field_path opt_apats_indices + field_how expr { UpdField $3 $1 (mkIndexedExpr $2 $4) } + +field_path :: { [Located Selector] } + : aexpr {% exprToFieldPath $1 } + +field_how :: { UpdHow } + : '=' { UpdSet } + | '->' { UpdFun } + + list_expr :: { Expr PName } : expr '|' list_alts { EComp $1 (reverse $3) } | expr { EList [$1] } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 16ef2af1d..bfe032205 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -279,18 +279,18 @@ data TopLevel a = TopLevel { tlExport :: ExportType -- | Infromation about the representation of a numeric constant. -data NumInfo = BinLit Int -- ^ n-digit binary literal - | OctLit Int -- ^ n-digit octal literal - | DecLit -- ^ overloaded decimal literal - | HexLit Int -- ^ n-digit hex literal +data NumInfo = BinLit Text Int -- ^ n-digit binary literal + | OctLit Text Int -- ^ n-digit octal literal + | DecLit Text -- ^ overloaded decimal literal + | HexLit Text Int -- ^ n-digit hex literal | PolyLit Int -- ^ polynomial literal deriving (Eq, Show, Generic, NFData) -- | Information about fractional literals. -data FracInfo = BinFrac - | OctFrac - | DecFrac - | HexFrac +data FracInfo = BinFrac Text + | OctFrac Text + | DecFrac Text + | HexFrac Text deriving (Eq,Show,Generic,NFData) -- | Literals. @@ -648,10 +648,10 @@ ppFracLit :: Rational -> FracInfo -> Doc ppFracLit x i | toRational dbl == x = case i of - BinFrac -> frac - OctFrac -> frac - DecFrac -> text (showFloat dbl "") - HexFrac -> text (showHFloat dbl "") + BinFrac _ -> frac + OctFrac _ -> frac + DecFrac _ -> text (showFloat dbl "") + HexFrac _ -> text (showHFloat dbl "") | otherwise = frac where dbl = fromRational x :: Double @@ -662,11 +662,11 @@ ppFracLit x i ppNumLit :: Integer -> NumInfo -> Doc ppNumLit n info = case info of - DecLit -> integer n - BinLit w -> pad 2 "0b" w - OctLit w -> pad 8 "0o" w - HexLit w -> pad 16 "0x" w - PolyLit w -> text "<|" <+> poly w <+> text "|>" + DecLit _ -> integer n + BinLit _ w -> pad 2 "0b" w + OctLit _ w -> pad 8 "0o" w + HexLit _ w -> pad 16 "0x" w + PolyLit w -> text "<|" <+> poly w <+> text "|>" where pad base pref w = let txt = showIntAtBase base ("0123456789abcdef" !!) n "" diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 1a6390b55..074290b4f 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -45,17 +45,10 @@ $unitick = \x7 @qual_id = @qual @id @qual_op = @qual @op -@digits2 = (_*[0-1])+ -@digits8 = (_*[0-7])+ -@digits16 = (_*[0-9A-Fa-f])+ -@num2 = "0b" @digits2 -@num8 = "0o" @digits8 -@num10 = [0-9](_*[0-9])* -@num16 = "0x" @digits16 -@fnum2 = @num2 "." @digits2 ([pP] [\+\-]? @num10)? -@fnum8 = @num8 "." @digits8 ([pP] [\+\-]? @num10)? -@fnum10 = @num10 "." @num10 ([eE] [\+\-]? @num10)? -@fnum16 = @num16 "." @digits16 ([pP] [\+\-]? @num10)? +@num = [0-9] @id_next* +@fnum = [0-9] @id_next* "." (@id_next | [pPeE][\+\-])+ + +@selector = "." @id_next+ @strPart = [^\\\"]+ @chrPart = [^\\\']+ @@ -130,19 +123,12 @@ $white+ { emit $ White Space } "Prop" { emit $ KW KW_Prop } -@num2 { emitS (numToken 2 . Text.drop 2) } -@num8 { emitS (numToken 8 . Text.drop 2) } -@num10 { emitS (numToken 10 . Text.drop 0) } -@num16 { emitS (numToken 16 . Text.drop 2) } -@fnum2 { emitS (fnumToken 2 . Text.drop 2) } -@fnum8 { emitS (fnumToken 8 . Text.drop 2) } -@fnum10 { emitS (fnumToken 10 . Text.drop 0) } -@fnum16 { emitS (fnumToken 16 . Text.drop 2) } - - +@num { emitS numToken } +@fnum { emitFancy fnumTokens } "_" { emit $ Sym Underscore } @id { mkIdent } +@selector { emitS selectorToken } "\" { emit $ Sym Lambda } "->" { emit $ Sym ArrR } @@ -152,7 +138,6 @@ $white+ { emit $ White Space } "=" { emit $ Sym EqDef } "," { emit $ Sym Comma } ";" { emit $ Sym Semi } -"." { emit $ Sym Dot } ":" { emit $ Sym Colon } "`" { emit $ Sym BackTick } ".." { emit $ Sym DotDot } @@ -261,9 +246,7 @@ primLexer cfg cs = run inp Normal let txt = Text.take l (input i) (mtok,s') = act cfg (alexPos i) txt s (rest,pos) = run i' $! s' - in case mtok of - Nothing -> (rest, pos) - Just t -> (t : rest, pos) + in (mtok ++ rest, pos) -- vim: ft=haskell } diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index 3d7e09aca..f7a88adec 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -10,6 +10,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE BlockArguments #-} module Cryptol.Parser.LexerUtils where import Cryptol.Parser.Position @@ -17,10 +18,13 @@ import Cryptol.Parser.Unlit(PreProc(None)) import Cryptol.Utils.PP import Cryptol.Utils.Panic -import Data.Char(toLower,generalCategory,isAscii,ord,isSpace) +import Control.Monad(guard) +import Data.Char(toLower,generalCategory,isAscii,ord,isSpace, + isAlphaNum,isAlpha) import qualified Data.Char as Char import Data.Text(Text) import qualified Data.Text as T +import qualified Data.Text.Read as T import Data.Word(Word8) import GHC.Generics (Generic) @@ -47,7 +51,7 @@ defaultConfig = Config type Action = Config -> Position -> Text -> LexS - -> (Maybe (Located Token), LexS) + -> ([Located Token], LexS) data LexS = Normal | InComment Bool Position ![Position] [Text] @@ -56,7 +60,7 @@ data LexS = Normal startComment :: Bool -> Action -startComment isDoc _ p txt s = (Nothing, InComment d p stack chunks) +startComment isDoc _ p txt s = ([], InComment d p stack chunks) where (d,stack,chunks) = case s of Normal -> (isDoc, [], [txt]) InComment doc q qs cs -> (doc, q : qs, txt : cs) @@ -65,8 +69,8 @@ startComment isDoc _ p txt s = (Nothing, InComment d p stack chunks) endComment :: Action endComment cfg p txt s = case s of - InComment d f [] cs -> (Just (mkToken d f cs), Normal) - InComment d _ (q:qs) cs -> (Nothing, InComment d q qs (txt : cs)) + InComment d f [] cs -> ([mkToken d f cs], Normal) + InComment d _ (q:qs) cs -> ([], InComment d q qs (txt : cs)) _ -> panic "[Lexer] endComment" ["outside comment"] where mkToken isDoc f cs = @@ -77,7 +81,7 @@ endComment cfg p txt s = in Located { srcRange = r, thing = Token (White tok) str } addToComment :: Action -addToComment _ _ txt s = (Nothing, InComment doc p stack (txt : chunks)) +addToComment _ _ txt s = ([], InComment doc p stack (txt : chunks)) where (doc, p, stack, chunks) = case s of @@ -87,7 +91,7 @@ addToComment _ _ txt s = (Nothing, InComment doc p stack (txt : chunks)) startEndComment :: Action startEndComment cfg p txt s = case s of - Normal -> (Just tok, Normal) + Normal -> ([tok], Normal) where tok = Located { srcRange = Range { from = p , to = moves p txt @@ -95,15 +99,15 @@ startEndComment cfg p txt s = } , thing = Token (White BlockComment) txt } - InComment d p1 ps cs -> (Nothing, InComment d p1 ps (txt : cs)) + InComment d p1 ps cs -> ([], InComment d p1 ps (txt : cs)) _ -> panic "[Lexer] startEndComment" ["in string or char?"] startString :: Action -startString _ p txt _ = (Nothing,InString p txt) +startString _ p txt _ = ([],InString p txt) endString :: Action endString cfg pe txt s = case s of - InString ps str -> (Just (mkToken ps str), Normal) + InString ps str -> ([mkToken ps str], Normal) _ -> panic "[Lexer] endString" ["outside string"] where parseStr s1 = case reads s1 of @@ -126,17 +130,17 @@ endString cfg pe txt s = case s of addToString :: Action addToString _ _ txt s = case s of - InString p str -> (Nothing,InString p (str `T.append` txt)) + InString p str -> ([],InString p (str `T.append` txt)) _ -> panic "[Lexer] addToString" ["outside string"] startChar :: Action -startChar _ p txt _ = (Nothing,InChar p txt) +startChar _ p txt _ = ([],InChar p txt) endChar :: Action endChar cfg pe txt s = case s of - InChar ps str -> (Just (mkToken ps str), Normal) + InChar ps str -> ([mkToken ps str], Normal) _ -> panic "[Lexer] endString" ["outside character"] where @@ -161,38 +165,40 @@ endChar cfg pe txt s = addToChar :: Action addToChar _ _ txt s = case s of - InChar p str -> (Nothing,InChar p (str `T.append` txt)) + InChar p str -> ([],InChar p (str `T.append` txt)) _ -> panic "[Lexer] addToChar" ["outside character"] mkIdent :: Action -mkIdent cfg p s z = (Just Located { srcRange = r, thing = Token t s }, z) +mkIdent cfg p s z = ([Located { srcRange = r, thing = Token t s }], z) where r = Range { from = p, to = moves p s, source = cfgSource cfg } t = Ident [] s mkQualIdent :: Action -mkQualIdent cfg p s z = (Just Located { srcRange = r, thing = Token t s}, z) +mkQualIdent cfg p s z = ([Located { srcRange = r, thing = Token t s}], z) where r = Range { from = p, to = moves p s, source = cfgSource cfg } t = Ident ns i (ns,i) = splitQual s mkQualOp :: Action -mkQualOp cfg p s z = (Just Located { srcRange = r, thing = Token t s}, z) +mkQualOp cfg p s z = ([Located { srcRange = r, thing = Token t s}], z) where r = Range { from = p, to = moves p s, source = cfgSource cfg } t = Op (Other ns i) (ns,i) = splitQual s emit :: TokenT -> Action -emit t cfg p s z = (Just Located { srcRange = r, thing = Token t s }, z) +emit t cfg p s z = ([Located { srcRange = r, thing = Token t s }], z) where r = Range { from = p, to = moves p s, source = cfgSource cfg } - emitS :: (Text -> TokenT) -> Action emitS t cfg p s z = emit (t s) cfg p s z +emitFancy :: (FilePath -> Position -> Text -> [Located Token]) -> Action +emitFancy f = \cfg p s z -> (f (cfgSource cfg) p s, z) + -- | Split out the prefix and name part of an identifier/operator. splitQual :: T.Text -> ([T.Text], T.Text) @@ -213,51 +219,119 @@ splitQual t = -------------------------------------------------------------------------------- -numToken :: Int {- ^ base -} -> Text -> TokenT -numToken rad ds = Num (toVal ds') rad (T.length ds') +numToken :: Text -> TokenT +numToken ds = case toVal of + Just v -> Num v rad (T.length ds') + Nothing -> Err MalformedLiteral where - ds' = T.filter (/= '_') ds - toVal = T.foldl' (\x c -> toInteger rad * x + fromDigit c) 0 + rad + | "0b" `T.isPrefixOf` ds = 2 + | "0o" `T.isPrefixOf` ds = 8 + | "0x" `T.isPrefixOf` ds = 16 + | otherwise = 10 + + ds1 = if rad == 10 then ds else T.drop 2 ds + + ds' = T.filter (/= '_') ds1 + toVal = T.foldl' step (Just 0) ds' + irad = toInteger rad + step mb x = do soFar <- mb + d <- fromDigit irad x + pure $! (irad * soFar + d) + +fromDigit :: Integer -> Char -> Maybe Integer +fromDigit r x' = + do d <- v + guard (d < r) + pure d + where + x = toLower x' + v | '0' <= x && x <= '9' = Just $ toInteger $ fromEnum x - fromEnum '0' + | 'a' <= x && x <= 'z' = Just $ toInteger $ 10 + fromEnum x - fromEnum 'a' + | otherwise = Nothing + + +-- | Interpret something either as a fractional token, +-- a number followed by a selector, or an error. +fnumTokens :: FilePath -> Position -> Text -> [Located Token] +fnumTokens file pos ds = + case wholeNum of + Nothing -> [ tokFrom pos ds (Err MalformedLiteral) ] + Just i + | Just f <- fracNum, Just e <- expNum -> + [ tokFrom pos ds (Frac ((fromInteger i + f) * (eBase ^^ e)) rad) ] + | otherwise -> + [ tokFrom pos whole (Num i rad (T.length whole)) + , tokFrom afterWhole rest (selectorToken rest) + ] -fromDigit :: Char -> Integer -fromDigit x' - | 'a' <= x && x <= 'z' = toInteger (10 + fromEnum x - fromEnum 'a') - | otherwise = toInteger (fromEnum x - fromEnum '0') - where x = toLower x' + where + tokFrom tpos txt t = + Located { srcRange = + Range { from = tpos, to = moves tpos txt, source = file } + , thing = Token { tokenText = txt, tokenType = t } + } + afterWhole = moves pos whole + + rad + | "0b" `T.isPrefixOf` ds = 2 + | "0o" `T.isPrefixOf` ds = 8 + | "0x" `T.isPrefixOf` ds = 16 + | otherwise = 10 --- XXX: For now we just keep the number as a rational. --- It might be better to keep the exponent representation, --- to avoid making huge numbers, and using up all the memory though... -fnumToken :: Int -> Text -> TokenT -fnumToken rad ds = Frac ((wholenNum + fracNum) * (eBase ^^ expNum)) rad - where radI = fromIntegral rad :: Integer radR = fromIntegral rad :: Rational - (whole,rest) = T.break (== '.') ds + (whole,rest) = T.break (== '.') (if rad == 10 then ds else T.drop 2 ds) digits = T.filter (/= '_') expSym e = if rad == 10 then toLower e == 'e' else toLower e == 'p' (frac,mbExp) = T.break expSym (T.drop 1 rest) + wholeStep mb c = do soFar <- mb + d <- fromDigit radI c + pure $! (radI * soFar + d) + + wholeNum = T.foldl' wholeStep (Just 0) (digits whole) - wholenNum = fromInteger - $ T.foldl' (\x c -> radI * x + fromDigit c) 0 - $ digits whole + fracStep mb c = do soFar <- mb + d <- fromInteger <$> fromDigit radI c + pure $! ((soFar + d) / radR) - fracNum = T.foldl' (\x c -> (x + fromInteger (fromDigit c)) / radR) 0 - $ T.reverse $ digits frac + fracNum = do let fds = T.reverse (digits frac) + guard (T.length fds > 0) + T.foldl' fracStep (Just 0) fds expNum = case T.uncons mbExp of - Nothing -> 0 :: Integer + Nothing -> Just (0 :: Integer) Just (_,es) -> case T.uncons es of - Just ('+', more) -> read $ T.unpack more - _ -> read $ T.unpack es + Just ('+', more) -> readDecimal more + Just ('-', more) -> negate <$> readDecimal more + _ -> readDecimal es eBase = if rad == 10 then 10 else 2 :: Rational +-- assumes we start with a dot +selectorToken :: Text -> TokenT +selectorToken txt + | Just n <- readDecimal body, n >= 0 = Selector (TupleSelectorTok n) + | Just (x,xs) <- T.uncons body + , ok isAlpha x + , T.all (ok isAlphaNum) xs = Selector (RecordSelectorTok body) + | otherwise = Err MalformedSelector + + where + body = T.drop 1 txt + ok p x = p x || x == '_' + + +readDecimal :: Integral a => Text -> Maybe a +readDecimal txt = case T.decimal txt of + Right (a,more) | T.null more -> Just a + _ -> Nothing + ------------------------------------------------------------------------------- @@ -462,6 +536,11 @@ data TokenErr = UnterminatedComment | InvalidString | InvalidChar | LexicalError + | MalformedLiteral + | MalformedSelector + deriving (Eq, Show, Generic, NFData) + +data SelectorType = RecordSelectorTok Text | TupleSelectorTok Int deriving (Eq, Show, Generic, NFData) data TokenT = Num !Integer !Int !Int -- ^ value, base, number of digits @@ -469,6 +548,7 @@ data TokenT = Num !Integer !Int !Int -- ^ value, base, number of digits | ChrLit !Char -- ^ character literal | Ident ![T.Text] !T.Text -- ^ (qualified) identifier | StrLit !String -- ^ string literal + | Selector !SelectorType -- ^ .hello or .123 | KW !TokenKW -- ^ keyword | Op !TokenOp -- ^ operator | Sym !TokenSym -- ^ symbol diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index a34a39074..930ba5aa6 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -22,6 +22,7 @@ import qualified Control.Monad.Fail as Fail import Data.Text(Text) import qualified Data.Text as T import qualified Data.Map as Map +import Text.Read(readMaybe) import GHC.Generics (Generic) import Control.DeepSeq @@ -32,6 +33,7 @@ import Prelude.Compat import Cryptol.Parser.AST import Cryptol.Parser.Lexer +import Cryptol.Parser.LexerUtils(SelectorType(..)) import Cryptol.Parser.Position import Cryptol.Parser.Utils (translateExprToNumT,widthIdent) import Cryptol.Utils.Ident(packModName) @@ -67,11 +69,15 @@ lexerP k = P $ \cfg p s -> UnterminatedComment -> "unterminated comment" UnterminatedString -> "unterminated string" UnterminatedChar -> "unterminated character" - InvalidString -> "invalid string literal:" ++ + InvalidString -> "invalid string literal: " ++ T.unpack (tokenText it) - InvalidChar -> "invalid character literal:" ++ + InvalidChar -> "invalid character literal: " ++ T.unpack (tokenText it) - LexicalError -> "unrecognized character:" ++ + LexicalError -> "unrecognized character: " ++ + T.unpack (tokenText it) + MalformedLiteral -> "malformed literal: " ++ + T.unpack (tokenText it) + MalformedSelector -> "malformed selector: " ++ T.unpack (tokenText it) where it = thing t @@ -201,23 +207,23 @@ getStr l = case thing l of Token (StrLit x) _ -> x _ -> panic "[Parser] getStr" ["not a string:", show l] -numLit :: TokenT -> Expr PName -numLit (Num x base digs) - | base == 2 = ELit $ ECNum x (BinLit digs) - | base == 8 = ELit $ ECNum x (OctLit digs) - | base == 10 = ELit $ ECNum x DecLit - | base == 16 = ELit $ ECNum x (HexLit digs) +numLit :: Token -> Expr PName +numLit Token { tokenText = txt, tokenType = Num x base digs } + | base == 2 = ELit $ ECNum x (BinLit txt digs) + | base == 8 = ELit $ ECNum x (OctLit txt digs) + | base == 10 = ELit $ ECNum x (DecLit txt) + | base == 16 = ELit $ ECNum x (HexLit txt digs) numLit x = panic "[Parser] numLit" ["invalid numeric literal", show x] -fracLit :: TokenT -> Expr PName +fracLit :: Token -> Expr PName fracLit tok = - case tok of + case tokenType tok of Frac x base - | base == 2 -> ELit $ ECFrac x BinFrac - | base == 8 -> ELit $ ECFrac x OctFrac - | base == 10 -> ELit $ ECFrac x DecFrac - | base == 16 -> ELit $ ECFrac x HexFrac + | base == 2 -> ELit $ ECFrac x $ BinFrac $ tokenText tok + | base == 8 -> ELit $ ECFrac x $ OctFrac $ tokenText tok + | base == 10 -> ELit $ ECFrac x $ DecFrac $ tokenText tok + | base == 16 -> ELit $ ECFrac x $ HexFrac $ tokenText tok _ -> panic "[Parser] fracLit" [ "Invalid fraction", show tok ] @@ -234,14 +240,6 @@ mkFixity assoc tok qns = (errorMessage (srcRange tok) "Fixity levels must be between 1 and 100") return (DFixity (Fixity assoc (fromInteger l)) qns) -mkTupleSel :: Range -> Integer -> ParseM (Located Selector) -mkTupleSel pos n - | n < 0 = errorMessage pos - (show n ++ " is not a valid tuple selector (they start from 0).") - | toInteger asInt /= n = errorMessage pos "Tuple selector is too large." - | otherwise = return $ Located pos $ TupleSel asInt Nothing - where asInt = fromInteger n - fromStrLit :: Located Token -> ParseM (Located String) fromStrLit loc = case tokenType (thing loc) of StrLit str -> return loc { thing = str } @@ -712,8 +710,8 @@ ufToNamed (UpdField h ls e) = _ -> errorMessage (srcRange (head ls)) "Invalid record field. Perhaps you meant to update a record?" -selExprToSels :: Expr PName -> ParseM [Located Selector] -selExprToSels e0 = reverse <$> go noLoc e0 +exprToFieldPath :: Expr PName -> ParseM [Located Selector] +exprToFieldPath e0 = reverse <$> go noLoc e0 where noLoc = panic "selExprToSels" ["Missing location?"] go loc expr = @@ -725,10 +723,35 @@ selExprToSels e0 = reverse <$> go noLoc e0 pure (Located { thing = s, srcRange = rng } : ls) EVar (UnQual l) -> pure [ Located { thing = RecordSel l Nothing, srcRange = loc } ] - ELit (ECNum n _) -> - do ts <- mkTupleSel loc n - pure [ ts ] + + ELit (ECNum n (DecLit {})) -> + pure [ Located { thing = TupleSel (fromInteger n) Nothing + , srcRange = loc } ] + + ELit (ECFrac _ (DecFrac txt)) + | (as,bs') <- T.break (== '.') txt + , Just a <- readMaybe (T.unpack as) + , Just (_,bs) <- T.uncons bs' + , Just b <- readMaybe (T.unpack bs) + , let fromP = from loc + , let midP = fromP { col = col fromP + T.length as + 1 } -> + -- these are backward because we reverse above + pure [ Located { thing = TupleSel b Nothing + , srcRange = loc { from = midP } + } + , Located { thing = TupleSel a Nothing + , srcRange = loc { to = midP } + } + ] + _ -> errorMessage loc "Invalid label in record update." +mkSelector :: Token -> Selector +mkSelector tok = + case tokenType tok of + Selector (TupleSelectorTok n) -> TupleSel n Nothing + Selector (RecordSelectorTok t) -> RecordSel (mkIdent t) Nothing + _ -> panic "mkSelector" + [ "Unexpected selector token", show tok ] diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 697ce151d..6862a1048 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -116,19 +116,19 @@ desugarLiteral lit = P.ECNum num info -> number $ [ ("val", P.TNum num) ] ++ case info of - P.BinLit n -> [ ("rep", tBits (1 * toInteger n)) ] - P.OctLit n -> [ ("rep", tBits (3 * toInteger n)) ] - P.HexLit n -> [ ("rep", tBits (4 * toInteger n)) ] - P.DecLit -> [ ] + P.BinLit _ n -> [ ("rep", tBits (1 * toInteger n)) ] + P.OctLit _ n -> [ ("rep", tBits (3 * toInteger n)) ] + P.HexLit _ n -> [ ("rep", tBits (4 * toInteger n)) ] + P.DecLit _ -> [ ] P.PolyLit _n -> [ ("rep", P.TSeq P.TWild P.TBit) ] P.ECFrac fr info -> let arg f = P.PosInst (P.TNum (f fr)) rnd = P.PosInst (P.TNum (case info of - P.DecFrac -> 0 - P.BinFrac -> 1 - P.OctFrac -> 1 - P.HexFrac -> 1)) + P.DecFrac _ -> 0 + P.BinFrac _ -> 1 + P.OctFrac _ -> 1 + P.HexFrac _ -> 1)) in P.EAppT fracPrim [ arg numerator, arg denominator, rnd ] P.ECChar c -> @@ -244,7 +244,7 @@ checkE expr tGoal = do prim <- mkPrim "generate" checkE (P.EApp prim e) tGoal - P.ELit l@(P.ECNum _ P.DecLit) -> + P.ELit l@(P.ECNum _ (P.DecLit _)) -> do e <- desugarLiteral l -- NOTE: When 'l' is a decimal literal, 'desugarLiteral' does -- not generate an instantiation for the 'rep' type argument diff --git a/tests/issues/issue713.icry b/tests/issues/issue713.icry new file mode 100644 index 000000000..faec408b4 --- /dev/null +++ b/tests/issues/issue713.icry @@ -0,0 +1 @@ +(True, True).0x1 diff --git a/tests/issues/issue713.icry.stdout b/tests/issues/issue713.icry.stdout new file mode 100644 index 000000000..5bb213c97 --- /dev/null +++ b/tests/issues/issue713.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol + +Parse error at :1:13--1:17 + malformed selector: .0x1 diff --git a/tests/issues/issue818.icry b/tests/issues/issue818.icry new file mode 100644 index 000000000..357c4edb5 --- /dev/null +++ b/tests/issues/issue818.icry @@ -0,0 +1,3 @@ +(+) 0b012 +(+) 2z where z = 0x3 +(+) 2z where z = (+) 0b012 diff --git a/tests/issues/issue818.icry.stdout b/tests/issues/issue818.icry.stdout new file mode 100644 index 000000000..19b2dc415 --- /dev/null +++ b/tests/issues/issue818.icry.stdout @@ -0,0 +1,10 @@ +Loading module Cryptol + +Parse error at :1:5--1:10 + malformed literal: 0b012 + +Parse error at :1:5--1:7 + malformed literal: 2z + +Parse error at :1:5--1:7 + malformed literal: 2z diff --git a/tests/issues/issue876.icry b/tests/issues/issue876.icry new file mode 100644 index 000000000..65eec8854 --- /dev/null +++ b/tests/issues/issue876.icry @@ -0,0 +1,4 @@ +((1,2),3).0.1 +{ (0,2) | 0 = 1 } +{ ((1,2),3) | 0.0 = 1 } +{ (0,1,(2,(3,4))) | 2.1.0 = 17 } diff --git a/tests/issues/issue876.icry.stdout b/tests/issues/issue876.icry.stdout new file mode 100644 index 000000000..68cf9c1b0 --- /dev/null +++ b/tests/issues/issue876.icry.stdout @@ -0,0 +1,20 @@ +Loading module Cryptol +Showing a specific instance of polymorphic result: + * Using 'Integer' for the type of '(expression)' +2 +Showing a specific instance of polymorphic result: + * Using 'Integer' for type of 1st tuple field + * Using 'Integer' for type of 0th tuple field +(1, 2) +Showing a specific instance of polymorphic result: + * Using 'Integer' for type of 1st tuple field + * Using 'Integer' for type of 1st tuple field + * Using 'Integer' for type of 0th tuple field +((1, 2), 3) +Showing a specific instance of polymorphic result: + * Using 'Integer' for type of 0th tuple field + * Using 'Integer' for type of 1st tuple field + * Using 'Integer' for type of 0th tuple field + * Using 'Integer' for type of 1st tuple field + * Using 'Integer' for type of 0th tuple field +(0, 1, (2, (17, 4))) diff --git a/utils/CryHtml.hs b/utils/CryHtml.hs index f6166e52c..4b264b374 100755 --- a/utils/CryHtml.hs +++ b/utils/CryHtml.hs @@ -54,6 +54,7 @@ cl tok = Num {} -> "number" Frac {} -> "number" Ident {} -> "identifier" + Selector {} -> "selector" KW {} -> "keyword" Op {} -> "operator" Sym {} -> "symbol" @@ -72,6 +73,7 @@ sty = unlines [ "body { font-family: monospace }" , ".number { color: #cc00cc }" , ".identifier { }" + , ".selector { color: #33033 }" , ".keyword { color: blue; }" , ".operator { color: #cc00cc }" , ".symbol { color: blue }"