Aug23 progress

Monkey/Lexer/Lexer.lean

@@ -35,6 +35,11 @@ def readChar : StateM Lexer Unit := do
     else { l with ch := l.input.get ⟨l.readPosition⟩}
   set { l' with position := l.readPosition, readPosition := l.readPosition + 1 }
 
+/-- Lexer を進めることなく、入力を覗き見(peek)する `readChar` の変種 -/
+def peekChar (l : Lexer) : Char :=
+  if l.readPosition ≥ l.input.length then '\x00'
+  else l.input.get ⟨l.readPosition⟩
+
 /-- デフォルト値を持たせたコンストラクタの変種 -/
 def mkD (input : String) (position readPosition : Nat := 0)
     (ch : Char := '\x00') : Lexer :=
@@ -84,6 +89,19 @@ def skipWhitespace : StateM Lexer Unit := do
 def nextToken : StateM Lexer Token := do
   skipWhitespace
   let mut l ← get
+
+  /- 2文字トークンの処理 -/
+  if l.ch == '=' && l.peekChar == '=' then
+    readChar
+    readChar
+    return EQ
+
+  if l.ch == '!' && l.peekChar == '=' then
+    readChar
+    readChar
+    return NOT_EQ
+
+  /- 1文字トークンの処理 -/
   let mut tok := match l.ch with
     | '=' => ASSIGN
     | '+' => PLUS

Monkey/Lexer/LexerTest.lean

@@ -15,6 +15,7 @@ def testNextToken (input : String) (expected : Array Token) : IO Unit := do
     if tok = EOF then break
 
   if actualTokens.size ≠ expected.size then
+    dbg_trace actualTokens
     throw <| .userError s!"tests failed: - token count wrong. expected={expected.size}, got={actualTokens.size}"
 
   let testCases := Array.zip expected actualTokens
@@ -106,6 +107,7 @@ def testNextToken (input : String) (expected : Array Token) : IO Unit := do
     EOF
   ])
 
+-- return とか true とかのテスト
 #eval testNextToken
   (input := "if (5 < 10) {
   return true;
@@ -132,3 +134,19 @@ def testNextToken (input : String) (expected : Array Token) : IO Unit := do
     RBRACE,
     EOF
   ])
+
+-- `==` とか `!=` とかのテスト
+#eval testNextToken
+  (input := "10 == 10;
+  10 != 9;")
+  (expected := #[
+    INT 10,
+    EQ,
+    INT 10,
+    SEMICOLON,
+    INT 10,
+    NOT_EQ,
+    INT 9,
+    SEMICOLON,
+    EOF
+  ])

Monkey/Repl/Repl.lean

@@ -0,0 +1,25 @@
+import Monkey.Lexer.Lexer
+import Monkey.Token.Token
+
+open IO Token
+
+/-- REPL を表す。
+`lake env lean --run Monkey/Repl/Repl.lean` で実行できる。
+標準入力に入れた Monkey のコードを読みこむ。 -/
+partial def main : IO Unit := do
+  IO.print ">> "
+  let inputStream ← getStdin
+  let input ← inputStream.getLine
+  if input.trim = "" then return ()
+
+  let mut l : Lexer := Lexer.new input
+  let mut tokens : Array Token := #[]
+
+  while True do
+    let ⟨tok, l'⟩ := l.nextToken |>.run
+    l := l'
+    tokens := tokens.push tok
+    if tok = EOF then break
+
+  IO.println tokens
+  main

Monkey/Token/Token.lean

@@ -46,6 +46,10 @@ inductive Token where
   | LT
   /-- 大なり ">" -/
   | GT
+  /-- 等号 `==` -/
+  | EQ
+  /-- 等しくない `!=` -/
+  | NOT_EQ
   /-- true : Bool -/
   | TRUE
   /-- false : Bool -/
@@ -81,6 +85,8 @@ def Token.toString (t : Token) : String :=
   | .SLASH => "/"
   | .LT => "<"
   | .GT => ">"
+  | .EQ => "=="
+  | .NOT_EQ => "!="
   | .TRUE => "TRUE"
   | .FALSE => "FALSE"
   | .IF => "IF"