-- 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"]

/- 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)


/- LT: structure and class
-/
inductive LT where
  | s (s : String) : LT
  | t (h : String) (l : List LT) : LT
  deriving Repr

partial def toLuaExpr0 : LT � String
  | .s s   => q s
  | .t h l => zconcat h (List.map toLuaExpr0 l)

class ToLT (α : Type) where
  toLT      : α â�� LT
  toLuaExpr : α â�� String  := fun o => toLuaExpr0 (toLT o)
  printTree : α â�� IO Unit := fun o => do IO.print (â�� luatreerun (toLuaExpr o))


/- LT: basic instances
-/
export ToLT (toLT toLuaExpr printTree)

instance : ToLT String     where toLT str := LT.s str
instance : ToLT Int        where toLT n   := LT.s (toString n)
instance : ToLT Nat        where toLT n   := LT.s (toString n)

instance {α} [ToLT α] : ToLT (List α)  where toLT as :=
  (LT.t "[]"  (List.map  toLT as))
instance {α} [ToLT α] : ToLT (Array α) where toLT as :=
  (LT.t "#[]" (Array.map toLT as).toList)

#eval toLT      [2, 3]
#eval toLuaExpr [2, 3]
#eval printTree [2, 3]




open Lean

partial def toLT_fromName (name : Name) : LT := match name with
  | .anonymous   => LT.s ".anon"
  | .str pre str => LT.t ".str" [toLT_fromName pre, toLT str]
  | .num _ _     => LT.s ".n"



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

#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