ゼミの進捗

Monkey/Lexer/Lexer.lean

@@ -1,9 +1,17 @@
 import Monkey.Token.Token
 
+/-- 字句解析器 -/
 structure Lexer where
+  /-- 入力された文字列。字句解析中は不変 -/
   input : String
+
+  /-- 今読んでいる位置 -/
   position : Nat := 0
+
+  /-- 次に読む位置 -/
   readPosition : Nat := 0
+
+  /-- 現在の文字 -/
   ch : Char := '\x00'
 deriving Repr
 
@@ -32,11 +40,10 @@ def mkD (input : String) (position readPosition : Nat := 0)
     (ch : Char := '\x00') : Lexer :=
   { input := input, position := position, readPosition := readPosition, ch := ch }
 
+/-- 文字列から Lexer を初期化する -/
 def new (input : String) : Lexer :=
   StateT.run readChar (Lexer.mkD input) |> Id.run |>.snd
 
-#check StateT.run readChar
-
 /-- Lexer を更新しつつ、letter ではない文字列が出てくるまで読み進める -/
 def readIdentifier : StateM Lexer String := do
   let mut l ← get
@@ -48,18 +55,44 @@ def readIdentifier : StateM Lexer String := do
     |>.take l.position
     |>.drop position
 
+/-- Lexer を更新しつつ、Number ではない文字列が出てくるまで読み進める -/
+def readNumber : StateM Lexer String := do
+  let mut l ← get
+  let position := l.position
+  while l.ch.isDigit do
+    readChar
+    l ← get
+  return l.input
+    |>.take l.position
+    |>.drop position
+
 open TokenType
 
 -- Char を String に変換する関数
 #check String.singleton
 
+-- Char が数字かどうか判定する
+#check Char.isDigit
+
+/-- Lexer に空白スペースと改行を無視させる -/
+def skipWhitespace : StateM Lexer Unit := do
+  while (← get).ch.isWhitespace do
+    readChar
+
 /-- Lexer を更新しながら、次のトークンを読む -/
 def nextToken : StateM Lexer Token := do
+  skipWhitespace
   let mut l ← get
   let ch := String.singleton l.ch
   let mut tok := match l.ch with
     | '=' => ⟨.ASSIGN, ch⟩
     | '+' => ⟨.PLUS, ch⟩
+    | '-' => ⟨.MINUS, ch⟩
+    | '!' => ⟨.BANG, ch⟩
+    | '/' => ⟨.SLASH, ch⟩
+    | '*' => ⟨.ASTERISK, ch⟩
+    | '<' => ⟨.LT, ch⟩
+    | '>' => ⟨.GT, ch⟩
     | '(' => ⟨.LPAREN, ch⟩
     | ')' => ⟨.RPAREN, ch⟩
     | '{' => ⟨.LBRACE, ch⟩
@@ -70,7 +103,14 @@ def nextToken : StateM Lexer Token := do
     | _ => ⟨.ILLEGAL, ch⟩
   if l.ch.isLetter then
     let literal ← readIdentifier
-    tok := ⟨if literal == "let" then LET else IDENT, literal⟩
+    let tokenType := LookupIdent literal
+    tok := ⟨tokenType, literal⟩
+    return tok
+  else if l.ch.isDigit then
+    let literal ← readNumber
+    let tokenType := INT
+    tok := ⟨tokenType, literal⟩
+    return tok
   readChar
   return tok
 

Monkey/Lexer/LexerTest.lean

@@ -3,13 +3,14 @@ import Monkey.Token.Token
 
 open TokenType Lexer
 
+/-- NestToken 関数をテストする -/
 def testNextToken (input : String) (expected : Array (TokenType × String)) : IO Unit := do
   let mut l : Lexer := Lexer.new input
   for tt in expected do
     let ⟨tok, l'⟩ := l.nextToken |>.run
     l := l'
     if tok.type ≠ tt.fst then
-      throw <| .userError s!"tests failed: - tokentype wrong. expected={tt.fst}, got={tok.type}"
+      throw <| .userError s!"tests failed: - tokentype wrong at \"{tt.snd}\". expected={tt.fst}, got={tok.type}"
     if tok.literal ≠ tt.snd then
       throw <| .userError s!"tests failed: - literal wrong. expected={tt.snd}, got={tok.literal}"
 
@@ -29,50 +30,67 @@ def testNextToken (input : String) (expected : Array (TokenType × String)) : IO
     (EOF, "")
   ])
 
--- #eval testNextToken
---   (input := "let five = 5;
---   let ten = 10;
---   let add = fn(x, y) {
---   x + y;
---   };
---   let result = add(five, ten);
---   ")
---   (expected := #[
---     (LET, "let"),
---     (IDENT, "five"),
---     (ASSIGN, "="),
---     (INT, "5"),
---     (SEMICOLON, ";"),
---     (LET, "let"),
---     (IDENT, "ten"),
---     (ASSIGN, "="),
---     (INT, "10"),
---     (SEMICOLON, ";"),
---     (LET, "let"),
---     (IDENT, "add"),
---     (ASSIGN, "="),
---     (FUNCTION, "fn"),
---     (LPAREN, "("),
---     (IDENT, "x"),
---     (COMMA, ","),
---     (IDENT, "y"),
---     (RPAREN, ")"),
---     (LBRACE, "{"),
---     (IDENT, "x"),
---     (PLUS, "+"),
---     (IDENT, "y"),
---     (SEMICOLON, ";"),
---     (RBRACE, "}"),
---     (SEMICOLON, ";"),
---     (LET, "let"),
---     (IDENT, "result"),
---     (ASSIGN, "="),
---     (IDENT, "add"),
---     (LPAREN, "("),
---     (IDENT, "five"),
---     (COMMA, ","),
---     (IDENT, "ten"),
---     (RPAREN, ")"),
---     (SEMICOLON, ";"),
---     (EOF, "")
---   ])
+#eval testNextToken
+  (input := "let five = 5;
+  let ten = 10;
+  let add = fn(x, y) {
+  x + y;
+  };
+  let result = add(five, ten);
+  ")
+  (expected := #[
+    (LET, "let"),
+    (IDENT, "five"),
+    (ASSIGN, "="),
+    (INT, "5"),
+    (SEMICOLON, ";"),
+    (LET, "let"),
+    (IDENT, "ten"),
+    (ASSIGN, "="),
+    (INT, "10"),
+    (SEMICOLON, ";"),
+    (LET, "let"),
+    (IDENT, "add"),
+    (ASSIGN, "="),
+    (FUNCTION, "fn"),
+    (LPAREN, "("),
+    (IDENT, "x"),
+    (COMMA, ","),
+    (IDENT, "y"),
+    (RPAREN, ")"),
+    (LBRACE, "{"),
+    (IDENT, "x"),
+    (PLUS, "+"),
+    (IDENT, "y"),
+    (SEMICOLON, ";"),
+    (RBRACE, "}"),
+    (SEMICOLON, ";"),
+    (LET, "let"),
+    (IDENT, "result"),
+    (ASSIGN, "="),
+    (IDENT, "add"),
+    (LPAREN, "("),
+    (IDENT, "five"),
+    (COMMA, ","),
+    (IDENT, "ten"),
+    (RPAREN, ")"),
+    (SEMICOLON, ";"),
+    (EOF, "")
+  ])
+
+#eval testNextToken
+  (input := "!-/*5;
+  5 < 10 > 5;")
+  (expected := #[
+    (BANG, "!"),
+    (MINUS, "-"),
+    (SLASH, "/"),
+    (ASTERISK, "*"),
+    (INT, "5"),
+    (SEMICOLON, ";"),
+    (INT, "5"),
+    (LT, "<"),
+    (INT, "10"),
+    (GT, ">"),
+    (INT, "5")
+  ])

Monkey/Token/Token.lean

@@ -1,21 +1,50 @@
+import Lean.Data.HashMap
 
+/-- Token の種類 -/
 inductive TokenType where
+  /-- 受け入れ不能エラー -/
   | ILLEGAL
+  /-- ファイル終端 -/
   | EOF
+  /-- 識別子 -/
   | IDENT
+  /-- 整数 -/
   | INT
+  /-- 代入記号 "=" -/
   | ASSIGN
+  /-- 足し算記号 + -/
   | PLUS
+  /-- コンマ , -/
   | COMMA
+  /-- セミコロン ; -/
   | SEMICOLON
+  /-- 開き括弧 ( -/
   | LPAREN
+  /-- 閉じ括弧 ) -/
   | RPAREN
+  /-- 開き波括弧 -/
   | LBRACE
+  /-- 閉じ波括弧 -/
   | RBRACE
+  /-- 無名関数 fn -/
   | FUNCTION
+  /-- LET キーワード -/
   | LET
+  /-- 引き算記号 "-" -/
+  | MINUS
+  /-- ビックリマーク ! -/
+  | BANG
+  /-- アスタリスク * -/
+  | ASTERISK
+  /-- スラッシュ "/" -/
+  | SLASH
+  /-- 小なり "<" -/
+  | LT
+  /-- 大なり ">" -/
+  | GT
 deriving Repr, DecidableEq
 
+/-- TokenType を文字列に変換する -/
 def TokenType.toString (t : TokenType) : String :=
   match t with
   | .ILLEGAL => "ILLEGAL"
@@ -32,11 +61,33 @@ def TokenType.toString (t : TokenType) : String :=
   | .RBRACE => "}"
   | .FUNCTION => "FUNCTION"
   | .LET => "LET"
+  | .MINUS => "-"
+  | .BANG => "!"
+  | .ASTERISK => "*"
+  | .SLASH => "/"
+  | .LT => "<"
+  | .GT => ">"
 
 instance : ToString TokenType where
   toString := TokenType.toString
 
+set_option linter.missingDocs false in
+
+/-- トークン -/
 structure Token where
   type : TokenType
   literal : String
 deriving Repr, BEq, DecidableEq
+
+open TokenType Lean
+
+/-- 言語のキーワード -/
+def keywords : HashMap String TokenType :=
+  let list : List (String × TokenType) := [("fn", FUNCTION), ("let", LET)]
+  HashMap.ofList list
+
+/-- ユーザ定義の識別子なのか、言語のキーワードなのか分類する -/
+def LookupIdent (ident : String) : TokenType :=
+  match keywords.find? ident with
+  | some tok => tok
+  | none => IDENT

lakefile.lean

@@ -5,7 +5,8 @@ package "InterpreterBook" where
   -- add package configuration options here
   leanOptions := #[
     ⟨`autoImplicit, false⟩,
-    ⟨`relaxedAutoImplicit, false⟩
+    ⟨`relaxedAutoImplicit, false⟩,
+    ⟨`linter.missingDocs, true⟩
   ]
 
 @[default_target]