#!/usr/bin/lua -f
-- (find-es "lua" "dednat")
-- (find-angg "LUA/inc.lua")
-- (fooi "process_tatsuta" "tatsuta_process")
-- (fooi "test_donode" "iprint_donode" "process_test" "iprint_process")

-- (fooi "node_prepstrings" "prepstrings_node" "bar_prepstrings"  "prepstrings_bar")

-- «.part0»			(to "part0")
-- «.split_into_segments»	(to "split_into_segments")
-- «.segments_intersecting»	(to "segments_intersecting")
-- «.psegs»			(to "psegs")

-- «.part1»			(to "part1")
-- «.process_reeplspecline»	(to "process_reeplspecline")
-- «.collect_dednameseg»	(to "collect_dednameseg")
-- «.process_lines»		(to "process_lines")
-- «.process_stuff»		(to "process_stuff")

-- «.part2»			(to "part2")
-- «.traversal_helpers»		(to "traversal_helpers")
-- «.p_string»			(to "p_string")
-- «.nonrec_prepstrings_node»	(to "nonrec_prepstrings_node")
-- «.nonrec_prepstrings_bar»	(to "nonrec_prepstrings_bar")
-- «.prepstrings_node»		(to "prepstrings_node")
--
-- «.iprint_donode»		(to "iprint_donode")
-- «.iprint_process»		(to "iprint_process")
-- «.tatsuta_donode»		(to "tatsuta_donode")
-- «.tatsuta_process»		(to "tatsuta_process")
-- «.buss_donode»		(to "buss_donode")
-- «.buss_process»		(to "buss_process")
--
-- «.top_level»			(to "top_level")

-- dofile(getenv("HOME").."/LUA/inc.lua")
-- We must arrange for inc.lua to be loaded before this file... 
-- (find-angg "LATEX/Makefile" "dednat.lua")
--
-- DEDNATLUA         = lua $(HOME)/LUA/inc.lua -f $(HOME)/LUA/dednat.lua
-- DEDNATLUA_TATSUTA = $(DEDNATLUA) 'tatsuta(arg[2],arg[3])'
-- DEDNATLUA_BUSS    = $(DEDNATLUA) 'buss(arg[2],arg[3])'


-- lines[1] = "%:*->*\\to *"
-- lines[2] = ""
-- lines[3] = " a "
-- lines[4] = " -r "
-- lines[5] = " b "
-- lines[6] = ""
-- lines[6] = " ^tree1 "
-- repls[1].strfrom = "->"
-- repls[1].strto = "\\to "
-- repls[1].f = function (str) return gsub(str, "%-%>", "\\to ") end
-- segments[1] = {}
-- segments[2] = {}
-- segments[3].string = "a"
-- segments[3].string.pbeg = 2
-- segments[3].string.pend = 3
-- segments[3].string = {}
-- strto = "\\to "






----- «part0»  (to ".part0")
----- Part 0: basic functions for segments: split a line into
----- segments, check which segments of a line intersect a given
----- region, print a list of segments.
-----

-- «split_into_segments»  (to ".split_into_segments")
-- split_into_segments("  aa  bb  ")  --> {{string="aa", pbeg=2, pend=4}, ...}
function split_into_segments(line)
  local from, arr, p1, p2 = 1, {}
  from = 1
  while 1 do
    p1, p2 = strfind(line, "([^%s]+)", from)
    if not p1 then return arr end
    tinsert(arr, {string = strsub(line, p1, p2), pbeg = p1-1, pend = p2})
    from = p2 + 1
  end
end

-- «segments_intersecting»  (to ".segments_intersecting")
function segments_intersecting(segments, pbeg, pend)
  local isegments = {}
  if type(pbeg) == "table" then
    pbeg, pend = pbeg.pbeg, pbeg.pend
  end
  foreachi(segments, function (i, seg)
      if not (seg.pend <= %pbeg or %pend <= seg.pbeg) then
        tinsert(%isegments, seg)
      end
    end)
  return isegments
end

-- «psegs»  (to ".psegs")
-- Functions to print lists of segments (obsolete).
--
function segimager(seg)
  return format("{string=%q pbeg=%d pend=%d}", seg.string, seg.pbeg, seg.pend)
end
function psegs(segs)
  print(arrtostr(segs, "", " ", "", segimager))
end






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

-- «process_reeplspecline»  (to ".process_reeplspecline")
-- If a line has enough "^O"s process it as a replspec line and return
-- ""; else return it unchanged (which means "process it further").
--
-- (find-node "(lua)Patterns" "magic")
--
function process_replspecline(i)
  local _, strfrom, strto, qstrfrom
  if strsub(lines[i],1,2) ~= "%:" then
    return ""				-- hack: discard non-"%:" line
  end
  _, _, strfrom, strto = strfind(lines[i], "^%%?:?*(.*)*(.*)*")
  if strfrom then
    qstrfrom = gsub(strfrom, "([%^%$%(%)%%%.%[%]%*%+%-%?])", "%%%1")
    tinsert(repls, {
      strfrom = strfrom,
      strto = strto,
      f = function (str) return gsub(str, %qstrfrom, %strto) end
    })
    return ""		-- replspec lines should not be split into segments
  end
  return lines[i]	-- return unchanged for further processing
end


-- «collect_dednameseg»  (to ".collect_dednameseg")
-- If a segment starts with "^" store it into dednamesegs, prepare the
-- data structure that makes the thing above it into a deduction tree,
-- and return the seg; if it doesn't start with "^", return nil.
--
function collect_dednameseg(i, j)
  local seg, _, rest
  seg = segments[i][j]
  _, _, rest = strfind(seg.string, "^%^(.*)")
  if rest then
    tinsert(dednamesegs, seg)
    seg.dedname = rest
    seg.dedroot = segments_intersecting(segments[i-2], seg.pbeg, seg.pend)[1]
    if not seg.dedroot then
      printf("line %d col %d string \"%s\": no dedroot!\n",
             seg.line, seg.pbeg, seg.string)
    end
    return seg		-- signal that we may want to process its tree
  end
end



-- «process_lines»  (to ".process_lines")
-- If a line is a replspec, process it accordingly; else split it into
-- segments, and for each segment set some extra fields in it
-- (segsabove and line) and submit it to collect_dednamesegs; if it
-- was a dednameseg and travfunc was given then submit it to travfunc.
--
function process_lines(travfunc)
  local travstring, i, j, line, segs, prevsegs, seg
  travstring = ""
  for i = 1, getn(lines) do
    line = process_replspecline(i)  -- line="" if no further processing needed
    line = untabify_line(gsub(line, "^%%:", "  "))
    segments[i] = split_into_segments(line)
    segs = segments[i]
    prevsegs = segments[i-1] or {}
    for j = 1, getn(segs) do
      seg = segs[j]
      seg.line = i
      seg.segsabove = segments_intersecting(prevsegs, seg.pbeg, seg.pend)
      seg = collect_dednameseg(i, j)
      if seg then
        if travfunc then travstring = travstring .. travfunc(seg) end
      end
    end
  end
  return travstring
end


-- «process_stuff»  (to ".process_stuff")
-- Process a chunk of text (coming from a file or from an immediate
-- string) in the standard way: reset the global variables lines,
-- repls, segments and dednamesegs and invoke process_lines with
-- argument travfunc; return the string that process_lines return,
-- that is the concatenation of the results of doing travfunc on each
-- dednameseg.
--
-- (to "iprint_process")
--
function process_stuff(fname, filecontents, travfunc)
  if fname then
    filecontents = readfile(fname)
  end
  lines = split1(filecontents, "\n")
  repls = {}
  segments = {}
  dednamesegs = {}
  return process_lines(travfunc)
end





----- «part2»  (to ".part2")
----- Part 2: traversals. Here we define the functions that will act
----- on deduction trees, recursively from the dedroot (but starting
----- at the dednameseg); these functions are fed to process_stuff to
----- process a chunk of text in a certain way and produce the TeX
----- code for its deduction trees.

-- «traversal_helpers»  (to ".traversal_helpers")
-- Functions to help traversing a tree.
--
function spaces(n) return strrep(" ", n) end
function upbar(nodeseg) return nodeseg.segsabove and nodeseg.segsabove[1] end
function upnodes(barseg) return barseg.segsabove end     -- return {} if none

-- «p_string»  (to ".p_string")
-- Apply all the replacement operations on a string.
--
function p_string(str)
  local i
  for i = 1, getn(repls) do
    str = repls[i].f(str)
  end
  return str
end

-- «nonrec_prepstrings_node»  (to ".nonrec_prepstrings_node")
--
function nonrec_prepstrings_node(nodeseg)
  nodeseg.p_string = nodeseg.p_string or p_string(nodeseg.string)
end

-- «nonrec_prepstrings_bar»  (to ".nonrec_prepstrings_bar")
--
function nonrec_prepstrings_bar(barseg)
  if barseg.barchar then return end
  local _, barchar, rstr
  _, _, barstr, rstr = strfind(barseg.string, "^(-+)(.*)")
  if not barstr then
    _, _, barstr, rstr = strfind(barseg.string, "^(=+)(.*)")
  end
  if not barstr then
    printf("line %d col %d string \"%s\": bad bar!\n",
               barseg.line, barseg.pbeg, barseg.string)
  end
  barseg.barchar = strsub(barstr, 1, 1)
  barseg.rstring = rstr
  barseg.p_rstring = p_string(rstr)
end

-- «prepstrings_node»  (to ".prepstrings_node")
-- A function that recursively prepares the
-- replaced strings for an entire tree.
--
function prepstrings_node(nodeseg)
  nonrec_prepstrings_node(nodeseg)
  local upbarseg = upbar(nodeseg)
  if upbarseg then
    nonrec_prepstrings_bar(upbarseg)
    foreachi(upnodes(upbarseg), function (i, seg) prepstrings_node(seg) end)
  end
end







-- "iprint": a simple traversal that will print each node and bar in
-- an indented way.
--
-- «iprint_donode»  (to ".iprint_donode")
function iprint_donode(nodeseg, n)
  local upbarseg = upbar(nodeseg)
  print(spaces(n) .. nodeseg.p_string)
  if upbarseg then
    print(spaces(n+1) .. upbarseg.barchar .. " " .. upbarseg.p_rstring)
    foreachi(upnodes(upbarseg), function(i, x) iprint_donode(x, %n+2) end)
  end
end
-- «iprint_process»  (to ".iprint_process")
function iprint_process(fname, filecontents)
  return process_stuff(fname, filecontents, function (seg)
      prepstrings_node(seg.dedroot)
      iprint_donode(seg.dedroot, 1)
      return ""
    end)
end




-- A traversal that generates TeX code for the trees using the macros
-- in Makoto Tatsuta's proof.sty package.
-- (find-fline "~/LATEX/proof.edrx.sty" "infer[")

mathstrut = "\\mathstrut "

-- «tatsuta_donode»  (to ".tatsuta_donode")
function tatsuta_donode(nodeseg, indent)
  local upbarseg = upbar(nodeseg)
  if upbarseg then  
    local modifier = ""
    if upbarseg.barchar == "=" then modifier = "=" end
    if upbarseg.p_rstring ~= "" then
      modifier = modifier .. "[" .. upbarseg.p_rstring .. "]"
    end
    local upnodesegs = upnodes(upbarseg)
    local uppers = {}
    local i
    for i = 1, getn(upnodesegs) do
      tinsert(uppers, "\n" .. tatsuta_donode(upnodesegs[i], indent + 1) .. " ")
    end
    return format("%s\\infer%s{ %s %s }{%s}",
      spaces(indent),
      modifier,
      mathstrut,
      nodeseg.p_string,
      join(uppers, "&"))
  else
    return spaces(indent) .. mathstrut .. nodeseg.p_string
  end
end

-- «tatsuta_process»  (to ".tatsuta_process")
function tatsuta_process(fname, filecontents)
  return process_stuff(fname, filecontents, function (seg)
      prepstrings_node(seg.dedroot)
      return format("\\defded{%s}{\n%s }\n",
                    seg.dedname,
                    tatsuta_donode(seg.dedroot, 1))
    end)
end





-- (find-es "tex" "bussproofs")
-- (find-shttpfile "www.math.ucla.edu/~asl/bussproofs.sty")
-- (find-shttpfile "www.math.ucla.edu/~asl/bussproofs.sty" "doubleLine")
-- (find-shttpfile "www.math.ucla.edu/~asl/bussproofs.sty" "The above proof")
-- (find-shttpfile "www.math.ucla.edu/~asl/bussproofs.sty" "RightLabel{")

-- «buss_donode»  (to ".buss_donode")
function buss_donode(nodeseg, indent)
  local upbarseg = upbar(nodeseg)
  local sp, sp1 = spaces(indent), spaces(indent + 1)
  if upbarseg then  
    local modifier = ""
    if upbarseg.barchar == "=" then modifier = "\\doubleLine " end
    if upbarseg.p_rstring ~= "" then
      modifier = modifier.."\\RightLabel{\\( "..upbarseg.p_rstring.." \\)} "
    end
    local upnodesegs = upnodes(upbarseg)
    local n = getn(upnodesegs)
    local upstr = ""
    local thispstring = mathstrut .. nodeseg.p_string
    local i
    if n == 0 then
      return sp.."\\AxiomC{} "..modifier ..
        "\\UnaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 1 then
      return buss_donode(upnodesegs[1], indent + 1) ..
        sp..modifier.."\\UnaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 2 then
      return buss_donode(upnodesegs[1], indent + 1) ..
             buss_donode(upnodesegs[2], indent + 1) ..
        sp..modifier.."\\BinaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n == 3 then
      return buss_donode(upnodesegs[1], indent + 1) ..
             buss_donode(upnodesegs[2], indent + 1) ..
             buss_donode(upnodesegs[3], indent + 1) ..
        sp..modifier.."\\TrinaryInfC{\\( "..thispstring.." \\)}\n"
    elseif n > 3 then
      return "\\AxiomC{!!!!(n>3)!!!!}\n"
    end
  else
    return sp.."\\AxiomC{\\( "..thispstring.." \\)}\n"
  end
end

-- «buss_process»  (to ".buss_process")
function buss_process(fname, filecontents)
  return process_stuff(fname, filecontents, function (seg)
      prepstrings_node(seg.dedroot)
      return format("\\defded{%s}{\n%s \\DisplayProof\n}\n",
                    seg.dedname,
                    buss_donode(seg.dedroot, 1))
    end)
end







function demo ()
stuff = [[
*<->*\bij *
%:*->*\to *
               -
        ee  f  g
        ========
  a->b  b<->c
  -----------A->B
   a->c

   ^d
]]
  print("The trivial traversal:")
  iprint_process(nil, stuff)
  print()

  print("The Tatsuta traversal:")
  print(tatsuta_process(nil, stuff))
  print()

  print("The Buss traversal:")
  print(buss_process(nil, stuff))
  print()
end


-- «top_level»  (to ".top_level")
-- (find-angg "LUA/inc.lua" "file_functions")
--
function buss(fnamein, fnameout)
  writefile(fnameout, buss_process(fnamein))
end
function tatsuta(fnamein, fnameout)
  writefile(fnameout, tatsuta_process(fnamein))
end

if getn(arg) == 0 then
  demo()
else
  --  print(tatsuta_process(arg[1]))
  dostring(arg[1])
end



-- (find-fline "~/LATEX/tmp.dn")
-- lua ~/LUA/dednat.lua
-- fname = "/home/root/LATEX/tmp.dn"
-- filecontents = readfile(fname)

-- p(dednamesegs[1].dedroot)
-- p(lines, "lines")
-- p(repls, "repls")
-- p(segments, "segments")

-- (find-node "(lua)Patterns")
-- (find-node "(lua)strfind")
-- (find-node "(lua)foreachi")




--
-- Local Variables:
-- coding:               no-conversion
-- ee-anchor-format:     "«%s»"
-- ee-charset-indicator: "Ñ"
-- ee-comment-format:    "-- %s\n"
-- End: