-- This file:
--   http://anggtwu.net/LEAN/luatree1.lean.html
--   http://anggtwu.net/LEAN/luatree1.lean
--          (find-angg "LEAN/luatree1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/luatree1.lean"))

-- Index:
-- «.zconcat»		(to "zconcat")
-- «.arith»		(to "arith")
-- «.arithToString»	(to "arithToString")
-- «.fileio»		(to "fileio")


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


-- «arith»  (to ".arith")
-- (find-leanmetadocrfile "main/01_intro.lean" "inductive Arith : Type")

inductive Arith : Type where
  | add : Arith → Arith → Arith -- e + f
  | mul : Arith → Arith → Arith -- e * f
  | nat : Nat → Arith           -- constant
  | var : String → Arith        -- variable

declare_syntax_cat arith
syntax num                        : arith -- nat for Arith.nat
syntax str                        : arith -- strings for Arith.var
syntax:50 arith:50 " + " arith:51 : arith -- Arith.add
syntax:60 arith:60 " * " arith:61 : arith -- Arith.mul
syntax " ( " arith " ) "          : arith -- bracketed expressions

syntax " ⟪ " arith " ⟫ " : term

macro_rules
  | `(⟪ $s:str ⟫)              => `(Arith.var $s)
  | `(⟪ $num:num ⟫)            => `(Arith.nat $num)
  | `(⟪ $x:arith + $y:arith ⟫) => `(Arith.add ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ $x:arith * $y:arith ⟫) => `(Arith.mul ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ ( $x ) ⟫)              => `( ⟪ $x ⟫ )

#check ⟪ "x" * "y" ⟫
#check ⟪ "x" + "y" ⟫
#check ⟪ "x" + 20 ⟫
#check ⟪ "x" + "y" * "z" ⟫ -- precedence
#check ⟪ "x" * "y" + "z" ⟫ -- precedence
#check ⟪ ("x" + "y") * "z" ⟫ -- brackets



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

section
open Arith
def  arithToString (o : Arith) : String := match o with
  | nat n => q (toString n)
  | var s => q s
  | mul a b => zconcat "*" [arithToString a, arithToString b]
  | add a b => zconcat "+" [arithToString a, arithToString b]
end

#eval arithToString ⟪ ("x" + "y") * 42 ⟫

def   tree1.lua := arithToString ⟪ ("x" + "y") * 42 ⟫
#eval tree1.lua



-- «fileio»  (to ".fileio")
-- (find-angg "LEAN/feline1.lean")

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

#eval writefile "/tmp/o1.lua" tree1.lua

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

-- (find-sh "~/luatree/luatree.lua /tmp/o1.lua")

def luatreerun : IO String := do
  let out ← IO.Process.output { cmd := luatreescript, args := #[luatreetmpfile] }
  return out.stdout

#eval luatreerun
#eval do IO.println (← luatreerun)



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