SaidScript

SaidScript.lean

import Lean.Data.AssocList
import Parser

namespace SaidScript

abbrev Env := Lean.AssocList String Int

inductive Op : Type
| add | sub | mul | div
deriving Repr

inductive Expr : Type
| var (name : String)
| const (val : Int)
| binOp (op : Op) (lhs rhs : Expr)
deriving Repr

inductive Stmt : Type
| declare (var : String)
| input (var : String)
| output (var : String)
| assign (var : String) (expr : Expr)
deriving Repr

open Op Expr Stmt

def Expr.eval (e : Expr) (env : Env) : Int := match e with
| var name => env.find? name |>.get!
| const val => val
| binOp op lhs rhs => match op with
  | add => lhs.eval env + rhs.eval env
  | sub => lhs.eval env - rhs.eval env
  | mul => lhs.eval env * rhs.eval env
  | div => lhs.eval env / rhs.eval env

def Stmt.interpret (s : Stmt) (env : Env) : IO Env := match s with
| declare name => pure $ env.insert name 0
| input name => do
  let input <- (String.toInt! ∘ String.trim) <$> (IO.getStdin >>= (·.getLine))
  pure $ env.insert name input
| output name => do
  env.find? name |>.get! |> IO.println
  pure env
| assign name expr => pure $ env.insert name (expr.eval env)

def run (ss : List Stmt) : IO Unit := loop ss default
where
  loop : List Stmt → Env → IO Unit
  | [], _ => pure ()
  | (s :: ss), env => do
    let e <- s.interpret env
    loop ss e

open Parser Char

protected abbrev Parser := SimpleParser Substring Char

def ws : SaidScript.Parser Unit := dropMany <| tokenFilter ([' ', '\n', '\r', '\t'].contains)

def integer : SaidScript.Parser Int := do
  let sign ← option? (char '-')
  let n <- takeMany ASCII.numeric
  pure ∘ String.toInt! ∘ n.foldl (·.push ·) $ match sign with
    | none => ""
    | some _ => "-"

end SaidScript