diff --git a/idris2.ipkg b/idris2.ipkg index bb43c45cf..54b6c23d0 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -82,6 +82,7 @@ modules = Idris.Syntax, Idris.Version, + Parser.Lexer.Common, Parser.Lexer.Source, Parser.Rule.Common, Parser.Rule.Source, diff --git a/idris2api.ipkg b/idris2api.ipkg index 0efa6ea30..e530493e7 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -82,6 +82,7 @@ modules = Idris.Syntax, Idris.Version, + Parser.Lexer.Common, Parser.Lexer.Source, Parser.Rule.Common, Parser.Rule.Source, diff --git a/idris2rkt.ipkg b/idris2rkt.ipkg index a010fc18f..04aeb9011 100644 --- a/idris2rkt.ipkg +++ b/idris2rkt.ipkg @@ -82,6 +82,7 @@ modules = Idris.Syntax, Idris.Version, + Parser.Lexer.Common, Parser.Lexer.Source, Parser.Rule.Common, Parser.Rule.Source, diff --git a/src/Parser/Lexer/Common.idr b/src/Parser/Lexer/Common.idr new file mode 100644 index 000000000..afd2851e8 --- /dev/null +++ b/src/Parser/Lexer/Common.idr @@ -0,0 +1,47 @@ +module Parser.Lexer.Common + +import public Text.Lexer + +%default total + +||| In `comment` we are careful not to parse closing delimiters as +||| valid comments. i.e. you may not write many dashes followed by +||| a closing brace and call it a valid comment. +export +comment : Lexer +comment + = is '-' <+> is '-' -- comment opener + <+> many (is '-') <+> reject (is '}') -- not a closing delimiter + <+> many (isNot '\n') -- till the end of line + +-- Identifier Lexer +-- There are multiple variants. + +public export +data Flavour = Capitalised | AllowDashes | Normal + +export +isIdentStart : Flavour -> Char -> Bool +isIdentStart _ '_' = True +isIdentStart Capitalised x = isUpper x || x > chr 160 +isIdentStart _ x = isAlpha x || x > chr 160 + +export +isIdentTrailing : Flavour -> Char -> Bool +isIdentTrailing AllowDashes '-' = True +isIdentTrailing _ '\'' = True +isIdentTrailing _ '_' = True +isIdentTrailing _ x = isAlphaNum x || x > chr 160 + +export %inline +isIdent : Flavour -> String -> Bool +isIdent flavour string = + case unpack string of + [] => False + (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs + +export %inline +ident : Flavour -> Lexer +ident flavour = + (pred $ isIdentStart flavour) <+> + (many . pred $ isIdentTrailing flavour) diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index aa15891e9..661a7571b 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -1,9 +1,10 @@ module Parser.Lexer.Source +import public Parser.Lexer.Common + import Data.List import Data.Strings -import public Text.Lexer import Utils.Hex import Utils.Octal import Utils.String @@ -52,17 +53,7 @@ Show SourceToken where dotSep [x] = x dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs] -||| In `comment` we are careful not to parse closing delimiters as -||| valid comments. i.e. you may not write many dashes followed by -||| a closing brace and call it a valid comment. -comment : Lexer -comment - = is '-' <+> is '-' -- comment opener - <+> many (is '-') <+> reject (is '}') -- not a closing delimiter - <+> many (isNot '\n') -- till the end of line - mutual - ||| The mutually defined functions represent different states in a ||| small automaton. ||| `toEndComment` is the default state and it will munch through @@ -111,35 +102,6 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1 docComment : Lexer docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n') --- Identifier Lexer --- There are multiple variants. - -data Flavour = Capitalised | AllowDashes | Normal - -isIdentStart : Flavour -> Char -> Bool -isIdentStart _ '_' = True -isIdentStart Capitalised x = isUpper x || x > chr 160 -isIdentStart _ x = isAlpha x || x > chr 160 - -isIdentTrailing : Flavour -> Char -> Bool -isIdentTrailing AllowDashes '-' = True -isIdentTrailing _ '\'' = True -isIdentTrailing _ '_' = True -isIdentTrailing _ x = isAlphaNum x || x > chr 160 - -%inline -isIdent : Flavour -> String -> Bool -isIdent flavour string = - case unpack string of - [] => False - (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs - -%inline -ident : Flavour -> Lexer -ident flavour = - (pred $ isIdentStart flavour) <+> - (many . pred $ isIdentTrailing flavour) - export isIdentNormal : String -> Bool isIdentNormal = isIdent Normal