Bon language AST.

Bon.lean

class Expr (F : Type → Type) where
  bool : Bool → F Bool
  not : F Bool → F Bool
  and : F Bool → F Bool → F Bool
  or : F Bool → F Bool → F Bool

  int : Int → F Int
  add : F Int → F Int → F Int
  sub : F Int → F Int → F Int

  string : String → F String
  concat : F String → F String → F String

  ite {α : Type} : F Bool → F α → F α → F α
  eq {α : Type} [BEq α] : F α → F α → F Bool

  external {α : Type} : String → F String
  kv {β : Type} : String → F β → F (String × β)
  module {α β : Type} : String → List (F (String × β)) → F (List (String × β))
  root {α : Type} : List (F α) → F (List α)

structure Value (α : Type) where
  mk ::
  value : α
deriving Repr

instance {α : Type} [ToString α] : ToString (Value α) where
  toString v := toString v.value

#eval Value.mk true |> toString

instance : Expr Value where
  bool e := ⟨e⟩
  not e := ⟨not e.value⟩
  and lhs rhs := ⟨and lhs.value rhs.value⟩
  or lhs rhs := ⟨or lhs.value rhs.value⟩

  int e := ⟨e⟩
  add lhs rhs := ⟨lhs.value + rhs.value⟩
  sub lhs rhs := ⟨lhs.value - rhs.value⟩

  string e := ⟨e⟩
  concat lhs rhs := ⟨lhs.value ++ rhs.value⟩

  ite c t e := if c.value then t else e
  eq lhs rhs := ⟨lhs.value == rhs.value⟩

  external e := ⟨e⟩
  kv k v := ⟨(k, v.value)⟩
  module n es := ⟨es.map Value.value⟩
  root es := ⟨es.map Value.value⟩

open Expr

#eval (and (bool true) (bool false) : Value Bool) |> toString
#eval (add (int 10) (int 20) : Value Int) |> toString
#eval (concat (string "hello") (string "world") : Value String) |> toString
#eval (ite (eq (string "hello") (string "hello")) (int 10) (int 20) : Value Int) |> toString
#eval (ite (eq (int 0) (int 42)) (int 10) (int 20) : Value Int) |> toString
#eval (kv "foo" (int 10) : Value (String × Int)) |> toString
#eval (root [int 10, int 20, int 30] : Value (List Int)) |> toString
#eval (@module Value instExprValue String _ "foo" [kv "a" (int 10), kv "b" (int 20)] : Value (List (String × Int))) |> toString