-- This file:
--   http://anggtwu.net/LEAN/luatree2.lean.html
--   http://anggtwu.net/LEAN/luatree2.lean
--          (find-angg "LEAN/luatree2.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun l1 () (interactive) (find-angg "LEAN/luatree1.lean"))
-- (defun l2 () (interactive) (find-angg "LEAN/luatree2.lean"))
-- variable (s head fname content : String)
-- variable (strs : List String)

import Lean

/- Trees as Lua expressions,
-- like this: {[0]="a", "b", "c"}
-/
namespace LuaTree
open String

def q   s  :=     "\"" ++ s ++ "\""   -- quote
def zq  s  := "[0]=\"" ++ s ++ "\""   -- zero/quote
def br  s  :=      "{" ++ s ++ "}"    -- bracket
def ac  s  :=     ", " ++ s           -- add comma

def acs (strs : List String) : String := join (List.map ac strs)
def zacs (head : String) (strs : List String) : String :=
  br ((zq head) ++ (acs strs))
def zconcat := zacs

#eval zconcat "a" [  "b",   "c"]
#eval zconcat "a" [q "b", q "c"]

inductive LT where
  | s : String
  | t : String
  deriving Repr

/- IO
-- See: (find-angg "luatree/luatree.lua")
-/

def mkfilepath (fname : String) : System.FilePath :=
  System.mkFilePath [fname]
def readfile   (fname : String) : IO String :=
  IO.FS.readFile (mkfilepath fname)
def writefile  (fname content : String) : IO Unit :=
  IO.FS.writeFile (mkfilepath fname) content
def getoutput (cmd : String) (args : Array String) : IO String := do
  let out ← IO.Process.output { cmd := cmd, args := args }
  return out.stdout

def luatreescript  := "/home/edrx/luatree/luatree.lua"
def luatreetmpfile := "/tmp/o1.lua"

def luatreerun (luaexpr : String) : IO String := do
  writefile luatreetmpfile luaexpr
  return (← getoutput luatreescript #[luatreetmpfile])
def luatreeprint (luaexpr : String) : IO Unit := do
  IO.println (← luatreerun luaexpr)

#eval do IO.print (← luatreerun (zconcat "a" [q "b", q "c"]))

/- ToLuaTree
-/
class      ToLuaTree (α : Type) where toLuaTree : α → String
export     ToLuaTree                 (toLuaTree)
instance : ToLuaTree String     where toLuaTree str := q str
instance : ToLuaTree Int        where toLuaTree n   := toString n
instance : ToLuaTree Nat        where toLuaTree n   := toString n

instance {α} [ToLuaTree α] : ToLuaTree (List  α) where toLuaTree as :=
  (zconcat  "[]" (List.map   toLuaTree as))
instance {α} [ToLuaTree α] : ToLuaTree (Array α) where toLuaTree as :=
  (zconcat "#[]" (Array.map  toLuaTree as).toList)

open Lean

#check Expr

def fromName (name : Name) : String := match name with
  | .anonymous   => q ".anon"
  | .str pre str => zconcat ".str" [fromName pre, q str]
  | .num _ _     => q ".n"

def fromSyntax (s : Syntax) : String := match s with
  | .missing        => ".m"
  | .node   _ _ _   => ".n"
  | .atom   _ _     => ".a"
  | .ident  _ _ _ _ => "i"

def fromTSyntax (_ : TSyntax ks) : String := ".r"

instance : ToLuaTree Name         where toLuaTree := fromName
instance : ToLuaTree Syntax       where toLuaTree := fromSyntax
instance : ToLuaTree (TSyntax ks) where toLuaTree := fromTSyntax

#eval  toLuaTree "ab"
#eval  toLuaTree  42
#eval  toLuaTree  [2, 3]
#eval  toLuaTree #[2, 3]
#eval  toLuaTree `Lean
#eval  toLuaTree `Lean.Name
#check  `(1 + "42")
#check  toLuaTree `(1 + "42")
--#eval  toLuaTree `(1 + "42")
#eval do IO.print (← luatreerun (toLuaTree `Lean.Name))

#check Lean.Syntax



partial def toLuaTreeName2 (name : Name) : String :=
  let _ : ToLuaTree Name := ⟨toLuaTreeName2⟩
  match name with
  | .anonymous   => "(.anon)"
  | .str pre str => zconcat ".str" [toLuaTree pre, q str]
  | .num pre i   => "(.n)"

instance : ToLuaTree Name := ⟨toLuaTreeName2⟩

end LuaTree