-- This file:
--   http://anggtwu.net/LEAN/luatree.lean.html
--   http://anggtwu.net/LEAN/luatree.lean
--          (find-angg "LEAN/luatree.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- Superseded by:
--   (find-angg "LEAN/luatree1.lean")
--
-- (defun e () (interactive) (find-angg "LEAN/luatree.lean"))
--
-- (find-angg "LEAN/luatree.lean")
-- (find-fplean4page 71 "def twice (action : IO Unit) : IO Unit")
-- (find-fplean4text 71 "def twice (action : IO Unit) : IO Unit")
-- (find-fplean4page 79 "Worked Example: cat")
-- (find-fplean4text 79 "Worked Example: cat")
-- (find-fplean4page 164 "The Monad Type Class")
-- (find-fplean4text 164 "The Monad Type Class")
-- (find-fplean4page 165 "General Monad Operations")
-- (find-fplean4text 165 "General Monad Operations")



-- Local Variables:
-- coding:  utf-8-unix
-- End:
-- (find-anggfile "luatree/luatree.lua" "[0]=")
-- (find-anggfile "luatree/luatree.lua" "-- Process stdin:")
-- (find-angg "LUA/GetOpt1.lua")

-- strings, concat, add quotes, namespace, 

-- import IO.Process
-- (find-anggfile "LEAN/overloaded1.lean")
-- (find-angg "LEAN/ioprocess1.lean")
-- (find-es "lean" "instance")

-- Index:
-- «.zconcat»		(to "zconcat")
-- «.ToLuaTree»		(to "ToLuaTree")


-----------------------------
-- «zconcat»  (to ".zconcat")

def q  s :=     "\"" ++ s ++ "\""
def zq s := "[0]=\"" ++ s ++ "\""
def br s :=      "{" ++ s ++ "}"
def ac s :=     ", " ++ s

def myconcat0 := List.foldl String.append ""
def acs (ss : List String) : String := myconcat0 (List.map ac ss)
def zacs (head : String) (ss : List String) : String := br ((zq head) ++ (acs ss))
def zconcat := zacs

#check            List.map
#check            List.map ac
#check            List.map ac ["a", "b", "c"]
#eval             List.map ac ["a", "b", "c"]
#eval  myconcat0              ["a", "b", "c"]
#eval  myconcat0 (List.map ac ["a", "b", "c"])
#eval  acs                    ["a", "b", "c"]
#eval  zacs    "foo"          ["a", "b", "c"]
#eval  zconcat "foo"          ["a", "b", "c"]

-- (find-lean4prefile "Init/Prelude.lean" "def List.foldl")


---------------------------------
-- «ToLuaTree»  (to ".ToLuaTree")

#eval toString 42

class ToLuaTree (α : Type) where
  toLuaTree0 : α → String

instance : ToLuaTree String where
  toLuaTree0 s := q s

instance : ToLuaTree Nat where
  toLuaTree0 n := toString n

instance : ToLuaTree Int where
  toLuaTree0 n := toString n

#check ToLuaTree
#check ToLuaTree.toLuaTree0
#eval  ToLuaTree.toLuaTree0 "foo"
#eval  ToLuaTree.toLuaTree0 42
#eval  ToLuaTree.toLuaTree0 (42 : Int)
#check 42

#check toString 42


----------------------------------------

open String


def f (_ : Nat) (_ : Nat) : Nat := 4

#print f
#check f
-- #eval f 2

#eval append "Hello, " "Lean!"
#print List


def main : IO Unit :=
  IO.println "Hello, world!\nfoo"

#eval main

-- (find-es "lean" "def")
-- (find-es "lean" "fun")
-- (find-es "lean" "inductive")

inductive mytree where
  | um   (str  : String) : mytree
  | dois (head : String) (a b : mytree) : mytree
deriving Repr

#check mytree.um
#check mytree.um "foo"
#eval  mytree.um "foo"

def foo := 42
def mt1 := mytree.um "foo"
def t1 : mytree := mytree.um "foo"

-- (find-es "lean" "string-interpolation")
-- (find-es "lean" "let")


def mytree.tostring (o : mytree) : String :=
  match o with
    | mytree.um s       => q s
    | mytree.dois a b c => zconcat a [b.tostring, c.tostring]

#eval (mytree.um "a").tostring
#eval (mytree.dois "a" (mytree.um "b") (mytree.um "c")).tostring


#check repr
#check reprStr
#eval reprStr 42


/-
| (find-elan4leanfile "Lean/")
| (find-lean4file "doc/")
| (find-lean4file "doc/tour.md")
| (find-angg ".emacs.papers" "fplean4")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
lean --run luatree.lean
lean -q --run luatree.lean
lean


-/



-- Local Variables:
-- coding:  utf-8-unix
-- End: