#!/usr/bin/env lua50
# -*- coding: raw-text-unix -*-
-- dednat, rewritten for lua5.0
-- intended to be much faster than the previous versions.
-- unfinished.
-- 2003jul13

-- «.segsabove»		(to "segsabove")
-- «.abbrevs»		(to "abbrevs")
-- «.untabify»		(to "untabify")
-- «.auxtreefunctions»	(to "auxtreefunctions")
-- «.tatsuta»		(to "tatsuta")
-- «.paul.taylor»	(to "paul.taylor")
-- «.heads»		(to "heads")
-- «.processfile»	(to "processfile")
-- «.luahead»		(to "luahead")
-- «.abbrevhead»	(to "abbrevhead")
-- «.treehead»		(to "treehead")
-- «.processfile-tree»	(to "processfile-tree")
-- «.main»		(to "main")

-- The data structures:
--
-- lines	an array of "line"s; only have entries for the "%:" lines
--
-- line.linen	an integer
-- line.text	a  string
-- line.segs	an array of "seg"s
--
-- seg.linen	an integer
-- seg.segn	an integer - for any seg s we have lines[s.linen][s.segn]==s
-- seg.lcol	an integer
-- seg.rcol	an integer
-- seg.text	a  string
--
-- isprefix	a table - isprefix[str] is either true or nil
-- abbrevs	a table - abbrevs[str] is the expansion of str, or nil if none


--%%%%
--%
--% «segsabove»  (to ".segsabove")
--%
--%%%%

relativeplacement = function (upperseg, lowerseg)
    if upperseg.rcol <= lowerseg.lcol then return "L" end
    if upperseg.lcol >= lowerseg.rcol then return "R" end
    return "I"
  end

nextseg = function (seg) return lines[seg.linen].segs[seg.segn+1] end

firstsegabove = function (lowerseg, nlines)
    local upperseg
    upperseg = lines[lowerseg.linen - (nlines or 1)] and
               lines[lowerseg.linen - (nlines or 1)].segs[1]
    while upperseg and relativeplacement(upperseg, lowerseg)=="L" do
        upperseg = nextseg(upperseg)
      end
    if upperseg and relativeplacement(upperseg, lowerseg)=="I" then
      return upperseg
    end
  end

nextsegabove = function (upperseg, lowerseg)
    local nextupperseg = nextseg(upperseg)
    return nextupperseg and
      relativeplacement(nextupperseg, lowerseg)=="I" and nextupperseg
  end

stuffabovenode = function (lowerseg)
    local barseg, firstupperseg, upperseg, n
    barseg = firstsegabove(lowerseg)
    if not barseg then return -1 end
    firstupperseg = firstsegabove(barseg)
    if not firstupperseg then return 0, barseg end
    n = 1
    upperseg = firstupperseg
    while 1 do
      upperseg = nextsegabove(upperseg, barseg)
      if upperseg then n = n+1 else return n, barseg, firstupperseg end
    end
  end


--%%%%
--%
--% «abbrevs»  (to ".abbrevs")
--%
--%%%%

isprefix = {}
abbrevs = {}
addabbrev = function (abbrev, expansion)
    for i = 1,string.len(abbrev)-1 do
      isprefix[string.sub(abbrev, 1, i)] = true
    end
    abbrevs[abbrev] = expansion
  end

unabbrev = function (str)
    local len, newstr, i = string.len(str), "", 1
    local j, teststr, longest
    while i<=len do
      longest = nil
      for j=i,len do
        teststr = string.sub(str, i, j)
        if abbrevs[teststr] then longest = teststr
        else
          if not isprefix[teststr] then break end
        end
      end
      if longest then
        newstr = newstr .. abbrevs[longest]
        i = i + string.len(longest)
      else
        newstr = newstr .. string.sub(str, i, i)
        i = i + 1
      end
    end
    return newstr
  end

-- these are mainly for tests and demos:
addabbrevs = function (...)
    for i=1,table.getn(arg),2 do
      addabbrev(arg[i], arg[i+1])
    end
  end
standardabbrevs = function ()
    addabbrevs(
      "->^", "\\ton ",   "`->", "\\ito ", "-.>", "\\tnto ",
      "=>",  "\\funto ", "<->", "\\bij ", "->",  "\\to ",
      "|-",  "\\vdash ", "÷>",  "\\mto ", "|->", "\\mto ",
      "\"",  " ")
  end


--%%%%
--%
--% «untabify»  (to ".untabify")
--%
--%%%%

do
local
reps = {"        ", "       ", "      ", "     ", "    ", "   ", "  ", " "}
--reps={"--------", "-------", "------", "-----", "----", "---", "--", "-"}
untabify = function (str, col)
    local pos, newstr, _, nontab, tab = 0, ""
    col = col or 0	-- 0-based: ((col mod 8)==2) -> (tab -> 6 spaces)
    while 1 do
      _, pos, nontab, tab = string.find(str, "^([^\t]*)(\t?)", pos+1)
      if tab=="" then
        return newstr..nontab
      end
      col = math.mod(col + string.len(nontab), 8)
      newstr = newstr..nontab..reps[col+1]
      col = 0
    end
  end
end

--[[
P(untabify("34\t\t01234567\t0123\t", 3))
P("3456701234567012345670123456701234567")
--]]


--%%%%
--%
--% «auxtreefunctions»  (to ".auxtreefunctions")
--%
--%%%%

dolinenumbers = "eev"
optionalhyperlink = function (pre, linen, post)
    if dolinenumbers == "eev" then
     return format("%s(find-fline \"%s\" %d)%s", pre, sourcefname, linen, post)
    elseif dolinenumbers then
      return format("%sfile %s line %d%s", pre, sourcefname, linen, post)
    else
      return ""
    end
  end

barcharandtext = function (barseg)
    local _, __, text
    _, __, text = string.find(barseg.text, "^-+(.*)")
    if text then return "-",text end
    _, __, text = string.find(barseg.text, "^=+(.*)")
    if text then return "=",text end
    errprintf("Bad bar at line %d, col %d: %s\n", barseg.linen, barseg.lcol,
      barseg.text)
  end


--%%%%
--%
--% «tatsuta»  (to ".tatsuta")
--%
--%%%%

-- (find-angg "dednat/dednat2.lua" "tatsuta_do_node")
-- (find-lua50ref "Precedence")

mathstrut = mathstrut or "\\mathstrut "

tex_node_tatsuta = function (indent, lowerseg)
    local n, barseg, upperseg = stuffabovenode(lowerseg)
    if not barseg then
      return indent..mathstrut..unabbrev(lowerseg.text)
    end
    local barchar, bartext = barcharandtext(barseg)
    local rulemodifier =
      (barchar=="=" and "=" or "") ..
      (bartext=="" and "" or "[{"..unabbrev(bartext).."}]")
    local newindent = indent.." "
    local uppertex
    if n==0 then
      return format("%s\\infer%s{ %s%s }{ }", indent, rulemodifier,
          mathstrut, unabbrev(lowerseg.text))
    else
      uppertex = tex_node_tatsuta(newindent, upperseg)
      for i=2,n do
        upperseg = nextseg(upperseg)
        uppertex = uppertex .. " &\n" .. tex_node_tatsuta(newindent, upperseg)
      end
    end
    return format("%s\\infer%s{ %s%s }{\n%s }",
        indent, rulemodifier,
        mathstrut, unabbrev(lowerseg.text),
        uppertex)
  end

function tex_tree_tatsuta(treetagseg, treelabel, treerootseg)
    return format("\\defded{%s}{%s\n%s }\n",
                  treelabel, optionalhyperlink("    % ", treetagseg.linen, ""),
                  tex_node_tatsuta(" ", treerootseg))
  end

tex_tree_function = tex_tree_tatsuta



--%%%%
--%
--% «paul.taylor»  (to ".paul.taylor")
--%
--%%%%

-- (find-es "tex" "ptproof")

tex_node_paultaylor = function (indent, lowerseg)
    local n, barseg, upperseg = stuffabovenode(lowerseg)
    if not barseg then
      return unabbrev(lowerseg.text)
    end
    local barchar, bartext = barcharandtext(barseg)
    local justifies = (barchar=="=" and "\\Justifies" or "\\justifies")
    local using = (bartext=="" and "" or "\\using "..unabbrev(bartext).." ")
    local newindent = indent.."   "
    local uppertex, segtex, istree, previstree
    if n==0 then
      return "\\[ "..using..justifies.."\n"..
             indent..unabbrev(lowerseg.text).." \\]", "tree"
    else
      uppertex, istree = tex_node_paultaylor(newindent, upperseg)
      for i=2,n do
        upperseg = nextseg(upperseg)
        previstree = istree
	segtex, istree = tex_node_paultaylor(newindent, upperseg)
        if previstree or istree then quad = "" else quad = " \\quad" end
        uppertex = uppertex..quad.."\n"..
                   newindent..segtex
      end
    end
    return "\\[ "..uppertex.." "..using..justifies.."\n"..
           indent..unabbrev(lowerseg.text).." \\]", "tree"
  end

function tex_tree_paultaylor(treetagseg, treelabel, treerootseg)
  return "\\defded{"..treelabel.."}{"..
         optionalhyperlink("    % ", treetagseg.linen, "")..
         "\n  \\begin{prooftree}\n  "..
            tex_node_paultaylor("  ", treerootseg)..
         "\n  \\end{prooftree}}"
end

-- tex_tree_function = tex_tree_paultaylor





--%%%%
--%
--% «heads»  (to ".heads")
--%
--%%%%

-- heads	a table of "head"s, indexed by strings - ex: heads["%:"]=...
-- head.code	a function taking no parameters, executed after each line
-- head.after	a function taking no parameters, executed after the block
-- head.headstr	the prefix string - ex: "%:"
-- stickyhead	nil or a "sticky head", a head with a non-nil head.after
--
-- other globals used: linestr, linen, sourcefname

heads = {}

registerhead = function (headstr, head)
    head.headstr = headstr
    heads[headstr] = head
  end
registerhead("", {})

doflushstickyblocks = function ()
    local after = stickyhead and stickyhead.after
    stickyhead = nil
    if after then after() end
  end
dolineinnewblock = function ()
    if head.code then head.code() end
    stickyhead = head.after and head
  end
doline = function ()
    head = heads[string.sub(linestr, 1, 3)] or
           heads[string.sub(linestr, 1, 2)] or
           heads[string.sub(linestr, 1, 1)] or
           heads[""]
    if stickyhead then
      if head.headstr == stickyhead.headstr then
        if head.code then head.code() end
      else
        doflushstickyblocks()
        dolineinnewblock()
      end
    else
      dolineinnewblock()
    end
  end

-- «processfile»  (to ".processfile")
-- minimal version without any head-specific code.
-- See: (to "processfile-tree")
processfile = function (fname)
    local _sourcefname, _linen, _linestr, _head, _lines =
           sourcefname,  linen,  linestr,  head,  lines
    sourcefname = fname
    linen = 0
    stickyhead = nil
    for _linestr in io.lines(fname) do
      linen = linen + 1
      linestr = _linestr
      doline()
    end
    doflushstickyblocks()
     sourcefname,  linen,  linestr,  head =
    _sourcefname, _linen, _linestr, _head
  end


--%%%%
--%
--% «luahead»  (to ".luahead")
--%
--%%%%

luaheadcode = function ()
    if luacode then
      luacode = luacode..string.sub(linestr, 3).."\n"
    else
      luacode = string.sub(linestr, 3).."\n"
      luacodestartlinen = linen
    end
  end

luaheadafter = function ()
    local chunkname = "\"%L\" chunk starting at line "..luacodestartlinen
    local code = luacode
    -- Pvars("luastartlinen", "luacode")
    luacode = nil
    luacodestartlinen = nil
    -- print(" assert(loadstring(code, chunkname))()")
    assert(loadstring(code, chunkname))()
  end

registerhead("%L", {code=luaheadcode, after=luaheadafter})

-- One of the uses of "%L"s is for loading extensions into dednat3.
-- For example, a line like this:
--   %L require "diagxy.lua"
-- will load the "diagxy" extension, that interprets lines starting
-- with "%D" in a certain special way.
-- To make these "require" commands simpler we add to LUA_PATH the
-- directory where dednat3.lua was found (unless it was the current
-- directory).

do local _, __, arg0path = string.find(arg[0], "^(.*)/[^/]*$")
   if arg0path then
     LUA_PATH = (LUA_PATH or getenv("LUA_PATH") or "?;?.lua")..
                ";"..arg0path.."/?"
   end
end




--%%%%
--%
--% «abbrevhead»  (to ".abbrevhead")
--%
--%%%%

abbrevheadcode = function ()
    local _, __, abbrev, expansion = string.find(linestr, "^%%:*(.-)*(.-)*")
    addabbrev(abbrev, expansion)
  end

registerhead("%:*", {code=abbrevheadcode})


--%%%%
--%
--% «treehead»  (to ".treehead")
--%
--%%%%

lines = {}
treetagsegs = {}

splitintosegs = function (line)
    local col, nsegs, _, __, spaces, text = 1, 0
    line.segs = {}
    while 1 do
      _, __, spaces, text = string.find(line.text, "^( *)([^ ]*)", col)
      if text and text ~= "" then
        nsegs = nsegs + 1
        local nspaces, nchars = string.len(spaces), string.len(text)
        line.segs[nsegs] = {linen=line.linen, segn=nsegs,
          lcol=col+nspaces, rcol=col+nspaces+nchars, text=text}
        col = col + nspaces + nchars
      else
        break
      end
    end
  end

processtreetags = function (line)
    seg = line.segs[1]
    while seg do
      if string.sub(seg.text, 1, 1)=="^" then
        local treelabel = string.sub(seg.text, 2)
        if treetagsegs[treelabel] then
          errprintf("Tree redefined: tree %s, lines %d and %d\n",
            treelabel, line.linen, treetagsegs[treelabel].linen)
        end
        local treerootseg = firstsegabove(seg, 2)
        if not treerootseg then
          errprintf("No root seg: line %d, tree %s\n", line.linen, treelabel)
        end
        print(tex_tree_function(seg, treelabel, treerootseg))
      end
      seg = nextseg(seg)
    end
  end

treeheadcode = function ()
    lines[linen] = {linen=linen, text=untabify(string.sub(linestr, 3), 2)}
    splitintosegs(lines[linen])
    processtreetags(lines[linen])
  end

registerhead("%:", {code=treeheadcode})

-- «processfile-tree»  (to ".processfile-tree")
-- This is a wrapper, see (to "processfile")
do
local _processfile = processfile
processfile = function (fname)
    local _lines = lines
    lines = {}		-- "%:"-specific
    _processfile(fname)
    lines = _lines
  end
end




--%%%%
--%
--% «main»  (to ".main")
--%
--%%%%

-- (find-lua50ref "Input and Output Facilities")
-- (find-lua50ref "file:write")
-- (find-lua50ref "string.find")

treetagsegs = {}

if arg and arg[1] and arg[1]~="" then processfile(arg[1]) end


--[[
#*
cat > /tmp/dn3test.tex <<'%%%'
bla
%:*->*\to *    .
%:*<->*\bij *  .
%:*=>*\funto * .
%:*-.>*\tnto * .
%:
%:     -
%:     c  d
%:     ====?
%:  a  a->b
%:  -------
%:     b
%:
%:  ^tree1
%:
%L require "diagxy.lua"
%D diagram miniadj
%D 2Dx     100   140
%D 2D 140 a^L <= a
%D 2D      -     -
%D 2D      | <-> |
%D 2D      v     v
%D 2D 100  b => b^R
%D a (( a^L => drop b |-> drop b^R => )) b^R |->
%D enddiagram
%%%
cd /tmp/
~/dednat/dednat3.lua dn3test.tex | tee ~/o
# ~/dednat/dednat3.lua ~/LATEX/2002h.tex > 2002h.dnt
#*
]]