-- Warning: this file uses "regmatch", defined in my (edrx's) modified
-- version of rtt's regexp libs...
-- (find-angg "lua-4.0/src/libdllua/lrexlib-new.c")
-- (find-angg "lua-4.0/src/libdllua/lrexlib-new.c" "regmatch")
-- (find-angg "LATEX/Makefile" "dednat.lua")
-- (find-angg "LATEX/Makefile" "dn_to_dnt")
regcomp = regex

treestuff = {}


-- «.store_macro»		(to "store_macro")
-- «.substitute_str»		(to "substitute_str")

-- «.hsplit»			(to "hsplit")
-- «.nodes_intersecting»		(to "nodes_intersecting")
-- «.hsplit_do_node»		(to "hsplit_do_node")
-- «.preprocess_tree_node»	(to "preprocess_tree_node")
-- «.preprocess_tree_rule»	(to "preprocess_tree_rule")

-- «.iprint_do_node»		(to "iprint_do_node")
-- «.iprint_do_tree»		(to "iprint_do_tree")
-- «.generate_tree_TeX_code»	(to "generate_tree_TeX_code")

-- «.tatsuta_do_node»		(to "tatsuta_do_node")
-- «.tatsuta_do_tree»		(to "tatsuta_do_tree")
-- «.buss_do_node»		(to "buss_do_node")
-- «.buss_do_node»		(to "buss_do_node")
-- «.tatsuta»			(to "tatsuta")
-- «.buss»			(to "buss")

-- «.getline»			(to "getline")
-- «.preprocess»		(to "preprocess")
-- «.preprocess_on»		(to "preprocess_on")
-- «.preprocess_off»		(to "preprocess_off")
-- «.process_macroline»		(to "process_macroline")
-- «.process_treeline»		(to "process_treeline")
-- «.process_lualine»		(to "process_lualine")
-- «.process_otherline»		(to "process_otherline")
-- «.process_line»		(to "process_line")
-- «.main_loop»			(to "main_loop")



--# How this program works (from the programmer's point of view):
--# It has a "main_loop" function that gets lines and processes them.
--# If a line is of the form "%:*...*...*" process it with "store_macro";
--# if not, and if it is of the form "%:...", process it as a part of
--# a tree diagram, with hsplit.

--#   Hsplit splits the "..." in "%:..." in words, and processes each
--#   of them as a "node"; for each "%:..." line, say the line linenum
--#   (where we start counting from 1), treestuff[linenum] is an array
--#   containing all the nodes from line linenum; for non-"%:..."
--#   lines treestuff[linenum] is nil.

--#   The processing of each node is done by the function "f_store",
--#   that is given as an argument to hsplit; f_store is usually
--#   hsplit_do_node. This processing includes adding the node (as a
--#   table with fields {str, p1, p2, linenum} -- other fields may be
--#   added later) to treestuff[linenum].

--#     If a node is of the form "^..." then it is a label with the
--#     name of a tree, and processing it is a complex task. We
--#     describe the other case first.

--#     If a node (say, "thisnode") is not the name of a tree then
--#     just build (with "nodes_intersecting") the array "aboves" of
--#     all the nodes in the preceding line that intersect thisnode,
--#     i.e., an array with the nodes that have some column in common
--#     with thisnode. If the array "aboves" turns out to be non-empty
--#     then set thisnode.aboves = aboves. Note that we are not yet
--#     doing anything special to distinguish nodes that are real tree
--#     nodes and nodes that are rules ("----..." or "====...").

--#     Each "^..." node points to another node, two lines above, that
--#     is the root of a tree. Issue an error if this tree-root node
--#     does not exist, and if it exists start the preprocessing of
--#     the tree -- note that now we will be able to determine which
--#     nodes are "tree node" nodes and which are "rule" nodes.

--#     Process these "tree node/rule" nodes recursively, preparing a
--#     field node.TeXstr for each of them; for "tree node" nodes this
--#     field is the result of running substitute_str on node.str, but
--#     for rule nodes node.str is split in a "rule" part (a sequence
--#     of "-"s or a sequence of "="s -- the field node.rulechar says
--#     which char) and a "right string" part, node.rightstr,
--#     containing the rest; for rule nodes node.TeXstr is the result
--#     of substitute_str(node.rightstr).

--#     If a tree node has a rule above it then it will have a
--#     "node.uprule" field pointing to the node of the rule. A rule
--#     node don't have any special field to point to the tree nodes
--#     above it; this data is in the field "node.aboves" (that for
--#     every node is always either nil or a non-empty array).

--#     The "^..." nodes get a "treelabel" field, containing the "..."
--#     string; after the preprocessing is done the function
--#     generate_tree_TeX_code is called, with the "^..." node as its
--#     only parameter. I haven't written generate_tree_TeX_code yet.







--###
--#
--# Functions to take care of macro substitution.
--# Store_macro will use the fields of a "%:*...*...*" line to update
--# the array of macros; substitute_str will apply all the
--# substitutions in the "macros" array on str.
--#
--###

macros = {}

-- «store_macro»  (to ".store_macro")
store_macro = function(fromstr, tostr)
  local n = macros[fromstr]		-- macros may be redefined
  local qfromstr = gsub(fromstr, "([%^%$%(%)%%%.%[%]%*%+%-%?])", "%%%1")
  local fun = function (str) return gsub(str, %qfromstr, %tostr) end
  if n then
    macros[n].tostr = tostr
    macros[n].fun = fun
  else
    tinsert(macros, {fromstr=fromstr, tostr=tostr, fun=fun})
    macros[fromstr] = getn(macros)
  end
end

-- «substitute_str»  (to ".substitute_str")
substitute_str = function(str)
  if str=="" then return str end	-- trivial optimization
  local i
  for i=1,getn(macros) do
    str = macros[i].fun(str)
  end
  return str
end



--###
--#
--# Functions to process "%:..." lines.
--# The outside will call hsplit for each "%:..." line; the functions
--# in this block will call generate_tree_TeX_code for each "^..."
--# node, after all the required preprocessing having been done.
--#
--###

-- «hsplit»  (to ".hsplit")
hsplit_re = regcomp("[^ ]+")
hsplit = function(linestr, arr, f_store)
  local pos, offset, newpos, str = 0
  f_store = f_store or hsplit_do_node
  while 1 do
    offset, str = regmatch(hsplit_re, linestr, pos)
    if offset==nil then
      return arr
    end
    f_store(arr, str, pos+offset, pos+offset+strlen(str))
    pos = pos+offset+strlen(str)
  end
end

-- «nodes_intersecting»  (to ".nodes_intersecting")
-- Return an array with the nodes of "ts" (i.e., ts[1], ts[2], etc)
-- that "intersect" the range (p1,p2). The array may be ={}.
function nodes_intersecting(p1, p2, ts)
  local arr, i, node = {}
  if ts then
    for i=1,getn(ts) do
      node = ts[i]
      if not (node.p2<=p1 or p2<=node.p1) then
        tinsert(arr, node)
      end
    end
  end
  return arr
end

-- «hsplit_do_node»  (to ".hsplit_do_node")
treelabel_re = regcomp("^\\^(.+)")
hsplit_do_node = function(arr, str, p1, p2)
  local linenum, thisnode, pos, m0, treelabel, treeroot, aboves
  linenum = arr.linenum
  thisnode = {str=str, p1=p1, p2=p2, linenum=linenum}
  tinsert(arr, thisnode)
  pos, m0, treelabel = regmatch(treelabel_re, str)
  if pos then
    thisnode.treelabel = treelabel
    treeroot = nodes_intersecting(p1, p2, treestuff[linenum - 2])[1]
    if not treeroot then
      printf("Tree name points to no root: %q, line %d\n", str, linenum)
      exit(1)
    end
    thisnode.treeroot = treeroot
    preprocess_tree_node(treeroot)
    generate_tree_TeX_code(thisnode)
  else
    aboves = nodes_intersecting(p1, p2, treestuff[linenum - 1])
    if getn(aboves)>0 then
      thisnode.aboves = aboves
    end
  end
end

-- «preprocess_tree_node»  (to ".preprocess_tree_node")
preprocess_tree_node = function(node)
  node.TeXstr = substitute_str(node.str)
  if node.aboves then
    node.uprule = node.aboves[1]
    preprocess_tree_rule(node.uprule)
  end
end

-- «preprocess_tree_rule»  (to ".preprocess_tree_rule")
preprocess_tree_rule_re = regcomp("^(-+|=+)(.*)")
preprocess_tree_rule = function(node)
  local pos, m0, rule, rightstr = regmatch(preprocess_tree_rule_re, node.str)
  if not pos then
    printf("Rule has no bar: %q, line %d\n", node.str, node.linenum)
    exit(1)
  end
  node.rulechar = strsub(rule, 1, 1)
  node.TeXstr = substitute_str(rightstr)
  if node.aboves then
    foreachi(node.aboves, function(i,node) preprocess_tree_node(node) end)
  end
end




--###
--#
--# Emitting trees (in TeX or in some debugging form)
--#
--###

function spaces(n) return strrep(" ", n) end

-- «iprint_do_node»  (to ".iprint_do_node")
function iprint_donode(indent, node)
  local uprule, i, upnode
  uprule = node.uprule
  if uprule then
    print(spaces(indent+2)..strrep(uprule.rulechar,4).." "..uprule.TeXstr)
    if uprule.aboves then
      for i=1,getn(uprule.aboves) do
        iprint_donode(indent+4, uprule.aboves[i])
      end
    end
  end
end

-- «iprint_do_tree»  (to ".iprint_do_tree")
function iprint_do_tree(treelabelnode)
  print(treelabelnode.str)
  iprint_donode(2, treelabelnode.treeroot)
  return ""
end

TeX_trees = {}
default_do_tree = iprint_do_tree

-- «generate_tree_TeX_code»  (to ".generate_tree_TeX_code")
generate_tree_TeX_code = function(treelabelnode)
  tinsert(TeX_trees, default_do_tree(treelabelnode))
end



--###
--#
--# Functions to generate TeX code for already-preprocessed trees
--#
--###

mathstrut = "\\mathstrut "

-- «tatsuta_do_node»  (to ".tatsuta_do_node")
-- (find-es "tex" "tatsutaproof")
function tatsuta_do_node(indent, node)
  local uprule = node.uprule
  if uprule then  
    local modifier = ""
    if uprule.rulechar == "=" then modifier = "=" end
    if uprule.TeXstr ~= "" then
      modifier = modifier .. "[{" .. uprule.TeXstr .. "}]"
    end
    local upnodes = uprule.aboves or {}
    local arr = {}
    local i
    for i=1,getn(upnodes) do
      tinsert(arr, "\n"..tatsuta_do_node(indent + 1, upnodes[i]).." ")
    end
    return format("%s\\infer%s{ %s %s }{%s}",
      spaces(indent),
      modifier,
      mathstrut,
      node.TeXstr,
      join(arr, "&"))
  else
    return spaces(indent) .. mathstrut .. node.TeXstr
  end
end

-- «tatsuta_do_tree»  (to ".tatsuta_do_tree")
function tatsuta_do_tree(treelabelnode)
  return format("\\defded{%s}{\n%s }\n",
                treelabelnode.treelabel,
                tatsuta_do_node(1, treelabelnode.treeroot))
end


-- «buss_do_node»  (to ".buss_do_node")
function buss_do_node(indent, node)
  local uprule = node.uprule
  local sp, sp1 = spaces(indent), spaces(indent + 1)
  local thispstring = mathstrut .. node.TeXstr
  if uprule then
    local modifier = ""
    if uprule.rulechar == "=" then modifier = "\\doubleLine " end
    if uprule.TeXstr ~= "" then
      modifier = modifier.."\\RightLabel{\\( "..uprule.TeXstr.." \\)} "
    end
    local upnodes = uprule.aboves or {}
    local n = getn(upnodes)
    local upstr = ""
    local i
    if n == 0 then
      return sp.."\\AxiomC{} "..modifier ..
        "\\UnaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 1 then
      return buss_do_node(indent + 1, upnodes[1]) ..
        sp..modifier.."\\UnaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 2 then
      return buss_do_node(indent + 1, upnodes[1]) ..
             buss_do_node(indent + 1, upnodes[2]) ..
        sp..modifier.."\\BinaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 3 then
      return buss_do_node(indent + 1, upnodes[1]) ..
             buss_do_node(indent + 1, upnodes[2]) ..
             buss_do_node(indent + 1, upnodes[3]) ..
        sp..modifier.."\\TrinaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n > 3 then
      return "\\AxiomC{!!!!(n>3)!!!!}\n"
    end
  else
    return sp.."\\AxiomC{\\( "..thispstring.." \\)}\n"
  end
end

-- «buss_do_node»  (to ".buss_do_node")
function buss_do_tree(treelabelnode)
  printf("\\defded{%s}{\n%s \\DisplayProof\n}\n",
         treelabelnode.treelabel,
         buss_do_node(1, treelabelnode.treeroot))
end



--###
--#
--# Functions to set the environment to use a certain TeX output
--# function (tatsuta_do_tree or buss_do_tree), a certain input file
--# and a certain output file
--#
--###

-- «tatsuta»  (to ".tatsuta")
tatsuta = function(srcfname, destfname, pp_destfname)
  default_do_tree = tatsuta_do_tree
  file_as_string = readfile(srcfname)
  TeX_trees.destfname = destfname
  pped_lines.destfname = pp_destfname
end

-- «buss»  (to ".buss")
buss = function(srcfname, destfname, pp_destfname)
  default_do_tree = buss_do_tree
  file_as_string = readfile(srcfname)
  TeX_trees.destfname = destfname
  pped_lines.destfname = pp_destfname
end



--###
--#
--# The main loop
--#
--###

file_as_string = ""	-- we set it later
file_pos = 0
file_linebeg = 0
linenum = 0
lines = {}

-- «getline»  (to ".getline")
getline_re = regex("^([^\n]*)(\n?)")
getline = function()
  file_linebeg = file_pos
  local p, all, bulk, nl = regmatch(getline_re, file_as_string, file_pos)
  if all=="" then
    return nil
  end
  linenum = linenum + 1
  file_pos = file_pos + strlen(all)
  tinsert(lines, bulk)
  return bulk
end


-- «preprocess»  (to ".preprocess")
-- «preprocess_on»  (to ".preprocess_on")
-- «preprocess_off»  (to ".preprocess_off")
pped_lines = {}		-- array of preprocessed lines (opt field: destfile)
preprocess_subst = function(linestr)
  tinsert(pped_lines, substitute_str(linestr))
end
preprocess_nochange = function(linestr)
  tinsert(pped_lines, linestr)
end
preprocess = preprocess_nochange
preprocess_on  = function() preprocess = preprocess_subst end
preprocess_off = function() preprocess = preprocess_nochange end



-- «process_macroline»  (to ".process_macroline")
macroline_re = regcomp("^%:*([^*]+)*([^*]*)*(.*)")
process_macroline = function(linestr)
  local p, all, fromstr, tostr, rest = regmatch(macroline_re, linestr)
  if p then
    store_macro(fromstr, tostr)
    return "processed"
  end
end

-- (eev "cd ~/LATEX/; touch tmp.tex; make tmp.auto.dnt")
-- (eev "cd ~/LATEX/; mylua -f ~/dednat/dednat2.lua 'tatsuta(arg[2],arg[3])' tmp.tex tmp.dnt")

-- «process_treeline»  (to ".process_treeline")
treeline_re = regcomp("^%:(.*)")
process_treeline = function(linestr)
  local pos, all, bulk = regmatch(treeline_re, linestr)
  if pos then
    treestuff[linenum] = {linenum=linenum}
    hsplit(untabify_line("  "..bulk), treestuff[linenum])
    return "processed"
  end
end

-- «process_lualine»  (to ".process_lualine")
bigluacode = ""
lualine_re = regcomp("^(.*?)%lua([^ \t]*)(.*)")
process_lualine = function(linestr)
  local pos, all, pre, special, luacode = regmatch(lualine_re, linestr)
  if pos then
    if special=="/" then	-- allow glueing lines before running the code
      bigluacode = bigluacode.."\n"..luacode
    else
      bigluacode = luacode
      dostring(bigluacode)
    end
    return "processed"
  end
end


-- «process_otherline»  (to ".process_otherline")
process_otherline = function(linestr)
  preprocess(linestr)
  return "processed"
end

-- «process_line»  (to ".process_line")
process_line = function(linestr)
  local dummy = process_macroline(linestr) or
                process_treeline(linestr) or
		process_lualine(linestr) or
		process_otherline(linestr)
end

-- «main_loop»  (to ".main_loop")
main_loop = function()
  local linestr
  while 1 do
    linestr = getline()
    if linestr==nil then break end
    process_line(linestr)
  end
end




--###
--#
--# a test
--#
--###

file_as_string = [[
%:*aa*<a>*
%:
%:  ==
%:  aa  bb
%:  ------aa
%:    cc
%:
%:    ^test
]]

if arg then
  dostring(arg[1])
end

-- (eev "cd ~/LUA/; mylua dednat2.lua")
-- (eev "mylua -f ~/dednat/dednat2.lua 'tatsuta(arg[2],arg[3])' ~/LATEX/tmp.tex /tmp/o")

main_loop()
if TeX_trees.destfname then
  writefile(TeX_trees.destfname, join(TeX_trees))
end
if pped_lines.destfname then
  writefile(pped_lines.destfname, join(pped_lines, "\n"))
end
print("finished.")