解析

Idris 2 带有一个词法分析库和语法解析库，内置在 contrib 包中。

在本示例中，我们将写一个非常简单的 lambda 演算解析器，该解析器将接受以下语言：

let name = world in (\x.hello x) name

一旦我们写了一个 lambda 演算解析器，我们还将看到我们如何利用 Idris 2 中强大的内置表达式解析器来写一个小计算器，它应该足够聪明来解析以下表达式：

1 + 2 - 3 * 4 / 5

词法分析器

词法分析模块主要在 Text.Lexer 下。这个模块包含 toTokenMap ，这是一个转换 List (Lexer, k) -> TokenMap (Token k) 的函数，其中 k 是一个标记种类。这个函数可用于词法与 Token 的简单映射。该模块还包括高级词法，用于指定数量和常见的编程原语，如 alphas , intLit, lineComment 和 blockComment 。

Text.Lexer 模块还重新导出了 Text.Lexer.Core 、 Text.Quantity 和 Text.Token 。

Text.Lexer.Core 提供了词法的基本构建块，包括一个叫做 Recognise 的类型，它是词法的底层数据类型。这个模块提供的另一个重要功能是 lex ，它接收一个词法分析器并返回 token。

Text.Quantity 提供了一个数据类型 Quantity 可以与某些词法一起使用，以指定某些东西预计会出现多少次。

Text.Token 提供一个数据类型 Token 表示一个被解析的标记和它的种类以及文本。这个模块还提供了一个重要的接口，称为 TokenKind.，它告诉词法分析器如何将标记种类映射到 Idris 2 类型，以及如何将每种种类从字符串转换为一个值。

解析器

解析器模主要在 Text.Parser 下。这个模块包含不同的语法分析器，主要的语法分析器是 match 它接收一个 TokenKind 并返回 TokenKind 接口中定义的值。还有其他的语法分析器，但对于我们的例子，我们将只使用 match 。

Text.Parser 模块重新导出 Text.Parser.Core , Text.Quantity 和 Text.Token 。

Text.Parser.Core 提供了解析器的构建块，包括一个叫做 Grammar 的类型，它是解析器的底层数据类型。这个模块提供的另一个重要函数是 parse 它接收一个 Grammar 并返回解析后的表达式。

我们在 Lexer 部分介绍了 Text.Quantity 和 Text.Token ，所以我们不打算在这里重复它们的作用。

Lambda 演算的分析器和解析器

LambdaCalculus.idr
  1import Data.List
  2import Data.List1
  3import Text.Lexer
  4import Text.Parser
  5
  6%default total
  7
  8data Expr = App Expr Expr | Abs String Expr | Var String | Let String Expr Expr
  9
 10Show Expr where
 11  showPrec d (App e1 e2) = showParens (d == App) (showPrec (User 0) e1 ++ " " ++ showPrec App e2)
 12  showPrec d (Abs v e) = showParens (d > Open) ("\\" ++ v ++ "." ++ show e)
 13  showPrec d (Var v) = v
 14  showPrec d (Let v e1 e2) = showParens (d > Open) ("let " ++ v ++ " = " ++ show e1 ++ " in " ++ show e2)
 15
 16data LambdaTokenKind
 17  = LTLambda
 18  | LTIdentifier
 19  | LTDot
 20  | LTOParen
 21  | LTCParen
 22  | LTIgnore
 23  | LTLet
 24  | LTEqual
 25  | LTIn
 26
 27Eq LambdaTokenKind where
 28  (==) LTLambda LTLambda = True
 29  (==) LTDot LTDot = True
 30  (==) LTIdentifier LTIdentifier = True
 31  (==) LTOParen LTOParen = True
 32  (==) LTCParen LTCParen = True
 33  (==) LTLet LTLet = True
 34  (==) LTEqual LTEqual = True
 35  (==) LTIn LTIn = True
 36  (==) _ _ = False
 37
 38Show LambdaTokenKind where
 39  show LTLambda = "LTLambda"
 40  show LTDot = "LTDot"
 41  show LTIdentifier = "LTIdentifier"
 42  show LTOParen = "LTOParen"
 43  show LTCParen = "LTCParen"
 44  show LTIgnore = "LTIgnore"
 45  show LTLet = "LTLet"
 46  show LTEqual = "LTEqual"
 47  show LTIn = "LTIn"
 48
 49LambdaToken : Type
 50LambdaToken = Token LambdaTokenKind
 51
 52Show LambdaToken where
 53  show (Tok kind text) = "Tok kind: " ++ show kind ++ " text: " ++ text
 54
 55TokenKind LambdaTokenKind where
 56  TokType LTIdentifier = String
 57  TokType _ = ()
 58
 59  tokValue LTLambda _ = ()
 60  tokValue LTIdentifier s = s
 61  tokValue LTDot _ = ()
 62  tokValue LTOParen _ = ()
 63  tokValue LTCParen _ = ()
 64  tokValue LTIgnore _ = ()
 65  tokValue LTLet _ = ()
 66  tokValue LTEqual _ = ()
 67  tokValue LTIn _ = ()
 68
 69ignored : WithBounds LambdaToken -> Bool
 70ignored (MkBounded (Tok LTIgnore _) _ _) = True
 71ignored _ = False
 72
 73identifier : Lexer
 74identifier = alpha <+> many alphaNum
 75
 76keywords : List (String, LambdaTokenKind)
 77keywords = [
 78  ("let", LTLet),
 79  ("in", LTIn)
 80]
 81
 82lambdaTokenMap : TokenMap LambdaToken
 83lambdaTokenMap = toTokenMap [(spaces, LTIgnore)] ++
 84  [(identifier, \s =>
 85      case lookup s keywords of
 86        (Just kind) => Tok kind s
 87        Nothing => Tok LTIdentifier s
 88    )
 89  ] ++ toTokenMap [
 90    (exact "\\", LTLambda),
 91    (exact ".", LTDot),
 92    (exact "(", LTOParen),
 93    (exact ")", LTCParen),
 94    (exact "=", LTEqual)
 95  ]
 96
 97lexLambda : String -> Maybe (List (WithBounds LambdaToken))
 98lexLambda str =
 99  case lex lambdaTokenMap str of
100    (tokens, _, _, "") => Just tokens
101    _ => Nothing
102
103mutual
104  expr : Grammar state LambdaToken True Expr
105  expr = do
106    t <- term
107    app t <|> pure t
108
109  term : Grammar state LambdaToken True Expr
110  term = abs
111    <|> var
112    <|> paren
113    <|> letE
114
115  app : Expr -> Grammar state LambdaToken True Expr
116  app e1 = do
117    e2 <- term
118    app1 $ App e1 e2
119
120  app1 : Expr -> Grammar state LambdaToken False Expr
121  app1 e = app e <|> pure e
122
123  abs : Grammar state LambdaToken True Expr
124  abs = do
125    match LTLambda
126    commit
127    argument <- match LTIdentifier
128    match LTDot
129    e <- expr
130    pure $ Abs argument e
131
132  var : Grammar state LambdaToken True Expr
133  var = map Var $ match LTIdentifier
134
135  paren : Grammar state LambdaToken True Expr
136  paren = do
137    match LTOParen
138    e <- expr
139    match LTCParen
140    pure e
141
142  letE : Grammar state LambdaToken True Expr
143  letE = do
144    match LTLet
145    commit
146    argument <- match LTIdentifier
147    match LTEqual
148    e1 <- expr
149    match LTIn
150    e2 <- expr
151    pure $ Let argument e1 e2
152
153parseLambda : List (WithBounds LambdaToken) -> Either String Expr
154parseLambda toks =
155  case parse expr $ filter (not . ignored) toks of
156    Right (l, []) => Right l
157    Right e => Left "contains tokens that were not consumed"
158    Left e => Left (show e)
159
160parse : String -> Either String Expr
161parse x =
162  case lexLambda x of
163    Just toks => parseLambda toks
164    Nothing => Left "Failed to lex."

测试一下我们的分析器，得到的输出结果如下：

$ idris2 -p contrib LambdaCalculus.idr
Main> :exec printLn $ parse "let name = world in (\\x.hello x) name"
Right (let name = world in (\x.hello x) name)

表达式解析器

Idris 2 还在 Text.Parser.Expression 中配备了一个非常方便的表达式解析器，可以明确优先权和关联性。

名为 buildExpressionParser 的主函数接受一个 OperatorTable 和一个表示术语的 Grammar ，并返回一个解析后的表达式。魔法来自 OperatorTable ，因为该表定义了所有运算符及其语法、优先级和关联性。

一个 OperatorTable 是一个包含 Op 类型的列表。 Op 类型允许你指定 Prefix, Postfix, 和 Infix 运算符以及它们的语法。 Infix 也包含了名为 Assoc 的关联性，可以指定左关联性 AssocLeft ，右关联性 AssocRight ，以及非关联性 AssocNone 。

我们将在计算器中使用的运算符表的一个例子是：

[
  [ Infix (match CTMultiply >> pure (*)) AssocLeft
  , Infix (match CTDivide >> pure (/)) AssocLeft
  ],
  [ Infix (match CTPlus >> pure (+)) AssocLeft
  , Infix (match CTMinus >> pure (-)) AssocLeft
  ]
]

这张表定义了4个运算符，用于乘法、除法、加法和减法。乘法和除法出现在第一个表中，因为它们的优先级高于加法和减法，后者出现在第二个表中。我们还将它们定义为 infix 运算符，有一个特定的语法，并且都是通过 AssocLeft 进行左关联。

构建一个计算器

Calculator.idr
  1import Data.List1
  2import Text.Lexer
  3import Text.Parser
  4import Text.Parser.Expression
  5
  6%default total
  7
  8data CalculatorTokenKind
  9  = CTNum
 10  | CTPlus
 11  | CTMinus
 12  | CTMultiply
 13  | CTDivide
 14  | CTOParen
 15  | CTCParen
 16  | CTIgnore
 17
 18Eq CalculatorTokenKind where
 19  (==) CTNum CTNum = True
 20  (==) CTPlus CTPlus = True
 21  (==) CTMinus CTMinus = True
 22  (==) CTMultiply CTMultiply = True
 23  (==) CTDivide CTDivide = True
 24  (==) CTOParen CTOParen = True
 25  (==) CTCParen CTCParen = True
 26  (==) _ _ = False
 27
 28Show CalculatorTokenKind where
 29  show CTNum = "CTNum"
 30  show CTPlus = "CTPlus"
 31  show CTMinus = "CTMinus"
 32  show CTMultiply = "CTMultiply"
 33  show CTDivide = "CTDivide"
 34  show CTOParen = "CTOParen"
 35  show CTCParen = "CTCParen"
 36  show CTIgnore = "CTIgnore"
 37
 38CalculatorToken : Type
 39CalculatorToken = Token CalculatorTokenKind
 40
 41Show CalculatorToken where
 42    show (Tok kind text) = "Tok kind: " ++ show kind ++ " text: " ++ text
 43
 44TokenKind CalculatorTokenKind where
 45  TokType CTNum = Double
 46  TokType _ = ()
 47
 48  tokValue CTNum s = cast s
 49  tokValue CTPlus _ = ()
 50  tokValue CTMinus _ = ()
 51  tokValue CTMultiply _ = ()
 52  tokValue CTDivide _ = ()
 53  tokValue CTOParen _ = ()
 54  tokValue CTCParen _ = ()
 55  tokValue CTIgnore _ = ()
 56
 57ignored : WithBounds CalculatorToken -> Bool
 58ignored (MkBounded (Tok CTIgnore _) _ _) = True
 59ignored _ = False
 60
 61number : Lexer
 62number = digits
 63
 64calculatorTokenMap : TokenMap CalculatorToken
 65calculatorTokenMap = toTokenMap [
 66  (spaces, CTIgnore),
 67  (digits, CTNum),
 68  (exact "+", CTPlus),
 69  (exact "-", CTMinus),
 70  (exact "*", CTMultiply),
 71  (exact "/", CTDivide)
 72]
 73
 74lexCalculator : String -> Maybe (List (WithBounds CalculatorToken))
 75lexCalculator str =
 76  case lex calculatorTokenMap str of
 77    (tokens, _, _, "") => Just tokens
 78    _ => Nothing
 79
 80mutual
 81  term : Grammar state CalculatorToken True Double
 82  term = do
 83    num <- match CTNum
 84    pure num
 85
 86  expr : Grammar state CalculatorToken True Double
 87  expr = buildExpressionParser [
 88    [ Infix ((*) <$ match CTMultiply) AssocLeft
 89    , Infix ((/) <$ match CTDivide) AssocLeft
 90    ],
 91    [ Infix ((+) <$ match CTPlus) AssocLeft
 92    , Infix ((-) <$ match CTMinus) AssocLeft
 93    ]
 94  ] term
 95
 96parseCalculator : List (WithBounds CalculatorToken) -> Either String Double
 97parseCalculator toks =
 98  case parse expr $ filter (not . ignored) toks of
 99    Right (l, []) => Right l
100    Right e => Left "contains tokens that were not consumed"
101    Left e => Left (show e)
102
103parse1 : String -> Either String Double
104parse1 x =
105  case lexCalculator x of
106    Just toks => parseCalculator toks
107    Nothing => Left "Failed to lex."

测试一下我们的计算器，就可以得到以下输出：

$ idris2 -p contrib Calculator.idr
Main> :exec printLn $ parse1 "1 + 2 - 3 * 4 / 5"
Right 0.6000000000000001