Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
-- treetex.lua: derivation trees and functions to convert them to TeX.
-- Here we define the TreeNode class: a TreeNode object has a
-- "conclusion" and may have a bar, a bar label, and hypotheses (that
-- are also TreeNode objects). TreeNode objects can be converted to
-- LaTeX code using the commands from Makoto Tatsuta's "proof.sty"
-- package, and to Rects for debugging. If you are interested in
-- generating code for other proof packages - e.g., Sam Buss's -
-- please get in touch! That should be easy to do, but I need help
-- with the syntax...
--
-- This file:
--   http://angg.twu.net/dednat6/dednat6/treetex.lua.html
--   http://angg.twu.net/dednat6/dednat6/treetex.lua
--           (find-angg "dednat6/dednat6/treetex.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 2019jan18
-- License: GPL3
--
-- Old versions:
--   (find-angg "dednat4/dednat4.lua" "tree-out")
--   (find-angg "dednat/dednat3.lua" "tatsuta")
--   (find-angg "dednat/dednat2.lua" "tatsuta_do_node")
--   (find-angg "dednat/dednat.lua" "tatsuta_donode")

-- «.TreeNode»			(to "TreeNode")
-- «.TreeNode-tests»		(to "TreeNode-tests")
-- «.tatsuta»			(to "tatsuta")
--   «.unabbrev_tatsuta»	(to "unabbrev_tatsuta")
--   «.TeX_subtree_tatsuta»	(to "TeX_subtree_tatsuta")
--   «.TeX_deftree_tatsuta»	(to "TeX_deftree_tatsuta")
--
-- «.ProofSty»			(to "ProofSty")
-- «.ProofSty-test»		(to "ProofSty-test")
-- «.BussProofs»		(to "BussProofs")
-- «.BussProofs-test»		(to "BussProofs-test")



require "eoo"       -- (find-dn6 "eoo.lua")
require "abbrevs"   -- (find-dn6 "abbrevs.lua")
require "rect"      -- (find-dn6 "rect.lua")



-- «TreeNode» (to ".TreeNode")
-- A TreeNode object "tn" has fields:
--
--   [0]: the tree root (a string)
--   bar: the strings "-", "=", or ":" if tn has a bar, nil otherwise
--   label: the label at the right of the bar (as a string), or nil
--   [1], [2], ..., [#tn]: other TreeNode objects; each one is a hypothesis.
--
-- Note that the TreeNode object format is much more strict than the
-- format that dedtorect() accepts. TreeNode.from(o) receives an
-- object o that dedtorect() accepts and converts it to a TreeNode
-- object. See:
--
--   (find-dn6 "rect.lua")
--   (find-dn6 "rect.lua" "dedtorect-tests")
--
TreeNode = Class {
  type = "TreeNode",
  from = function (o)
      if type(o) == "string" then return TreeNode {[0]=o} end
      if type(o) == "table"  then
        local tn = {[0]=o[0], bar=o.bar, label=o.label}
        for i=1,#o do tn[i] = TreeNode.from(o[i]) end
        if #tn > 0 then tn.bar = tn.bar or "-" end
        return TreeNode(tn)
      end
      Error("TreeNode.from(o) failed")
    end,
  __tostring  = function (tn) return tostring(tn:torect()) end,
  __index = {
    torect    = function (tn) return dedtorect(tn) end,
    hasbar    = function (tn) return tn.bar ~= nil end,
    barchar   = function (tn) return tn.bar end,
    TeX_root  = function (tn) return tn[0] end,
    TeX_label = function (tn) return tn.label end,
    nhyps     = function (tn) return #tn end,
    hypslist  = function (tn) return tn end,
    TeX_subtree = function (tn, i_)
        return TeX_subtree_tatsuta(tn, i_)
      end,
    TeX_deftree = function (tn, name, link)
        return TeX_deftree_tatsuta(tn, name, link)
      end,
  },
}


-- «TreeNode-tests» (to ".TreeNode-tests")
-- See: (find-dn6 "rect.lua" "dedtorect-tests")
--[==[
 (eepitch-lua51)
 (eepitch-kill)
 (eepitch-lua51)
require "treetex"
ded = {[0]="a", "b", {[0]="c", "d",      "e",           bar="=", label="foo"}}
ded = {[0]="a", "b", {[0]="c", "d", {[0]="e", bar="-"}, bar="=", label="foo"}}
= dedtorect(ded)
tn = TreeNode.from(ded)
PPV(ded)
PPV(tn)
= tn
= otype(tn)
= otype(tn[1])
= otype(ded)
= otype(ded[1])
= tn:TeX_subtree("")
= tn:TeX_subtree("  ")
= tn:TeX_deftree("foo", "?")

--]==]




--  _        _             _        
-- | |_ __ _| |_ ___ _   _| |_ __ _ 
-- | __/ _` | __/ __| | | | __/ _` |
-- | || (_| | |_\__ \ |_| | || (_| |
--  \__\__,_|\__|___/\__,_|\__\__,_|
--                                  
-- «tatsuta»  (to ".tatsuta")
-- This is the original way to convert a TreeNode to a \defded.
-- It is super-old (modulo minimal changes). It doesn't uses classes
-- and it uses the name "tatsuta" to refers to Makoto Tatsuta's
-- proof.sty package, instead of calling it "proof.sty". This code
-- will be obsoleted soon (where "now" = 2020aug24).




-- «unabbrev_tatsuta» (to ".unabbrev_tatsuta")
-- One easy way to change the way that tree nodes are converted from
-- ascii to TeX is to change this function temporarily.
unabbrev_tatsuta = unabbrev

-- «TeX_subtree_tatsuta» (to ".TeX_subtree_tatsuta")
TeX_subtree_tatsuta = function (tn, i_)
    if not tn:hasbar() then
      return i_.."\\mathstrut "..unabbrev_tatsuta(tn:TeX_root())
    else
      local r_ = tn:TeX_root()
      local b_ = tn:barchar()
      local l_ = tn:TeX_label()
      local h_ = tn:hypslist()
      local r  = "\\mathstrut "..unabbrev_tatsuta(r_)
      -- local b  = ({["-"]="", ["="]="=", [":"]="*"})[b_]
      local b  = ({["-"]="infer",
                   ["="]="infer=",
                   [":"]="infer*",
                   ["."]="deduce"})[b_]
      local l  = (l_ and "[{"..unabbrev(l_).."}]") or ""
      local i  = i_.." "
      local f  = function (tn) return TeX_subtree_tatsuta(tn, i) end
      local h  = mapconcat(f, h_, " &\n")
      -- return i_.."\\infer"..b..l.."{ "..r.." }{\n"..h.." }"
      return i_.."\\"..b..l.."{ "..r.." }{\n"..h.." }"
    end
  end

-- «TeX_deftree_tatsuta» (to ".TeX_deftree_tatsuta")
TeX_deftree_tatsuta = function (tn, name, link)
    local comment = "   % "..(link or tf:hyperlink())
    return "\\defded{"..name.."}{"..comment.."\n"..
           TeX_subtree_tatsuta(tn, " ").." }"
  end





treetex_mapconcat = function (f, arr, sep, ifempty)
    if #arr > 0 then return mapconcat(f, arr, sep) end
    return ifempty   -- return this string if the array has length 0
  end




--  ____                   __ ____  _         
-- |  _ \ _ __ ___   ___  / _/ ___|| |_ _   _ 
-- | |_) | '__/ _ \ / _ \| |_\___ \| __| | | |
-- |  __/| | | (_) | (_) |  _|___) | |_| |_| |
-- |_|   |_|  \___/ \___/|_| |____/ \__|\__, |
--                                      |___/ 
--
-- «ProofSty»  (to ".ProofSty")
-- A class that converts a TreeNode to a \defded using Makoto
-- Tatsuta's proof.sty. This is intended as a replacement for the
-- functions TeX_subtree_tatsuta and TeX_deftree_tatsuta defined above.
-- Experimental. Version: 2020aug24.

ProofSty = Class {
  type = "ProofSty",
  new  = function () return ProofSty {} end,
  __index = {
    unabbrev = function (ps, str) return unabbrev(str) end,
    subtreetolatex = function (ps, tn, i)
        if not tn:hasbar() then
          return i.."\\mathstrut "..ps:unabbrev(tn:TeX_root())
        else
          local r_ = tn:TeX_root()
          local b_ = tn:barchar()
          local l_ = tn:TeX_label()
          local h_ = tn:hypslist()
          local r  = "\\mathstrut "..ps:unabbrev(r_)
          local b  = ({["-"]="infer",
                       ["="]="infer=",
                       [":"]="infer*",
                       ["."]="deduce"})[b_]
          local l  = (l_ and "[{"..ps:unabbrev(l_).."}]") or ""
          local i_ = i.." "
          local f  = function (tn) return ps:subtreetolatex(tn, i_) end
          local h  = treetex_mapconcat(f, h_, " &\n", " ")
          return i.."\\"..b..l.."{ "..r.." }{\n"..h.." }"
        end
      end,
    todefded = function (ps, tn, name, link)
        local comment = "   % "..(link or tf:hyperlink())
        return "\\defded{"..name.."}{"..comment.."\n"..
               ps:subtreetolatex(tn, " ").." }"
      end,
  },
}

proofsty = ProofSty.new()

-- To experiment with the new classes, do something like:
--
--   TreeNode.__index.TeX_deftree = function (tn, name, link)
--       return proofsty:todefded(tn, name, link)
--     end
--
-- or:
--
--   TreeNode.__index.TeX_deftree = function (tn, name, link)
--       return bussproofs:todefded(tn, name, link)
--     end
--
-- To replace a method in proofsty, do something like:
--
--   proofsty.unabbrev = function (ps, str)
--       return "?"..unabbrev(str)
--     end


-- «ProofSty-test»  (to ".ProofSty-test")
--[==[
 (eepitch-lua51)
 (eepitch-kill)
 (eepitch-lua51)
loaddednat6()
require "block"
bigstr = [[
%:                       H
%:  -                   ...
%:  A  B  C   E  F      \Pi
%:  =======r  ::::\phi  ...
%:     D       G         I
%:     -------------------
%:             J
%:
%:             ^bars
%:
]]
output = print
texlines = TexLines.new("test", bigstr)
tf = texlines:toblock()
tf:processuntil(texlines:nlines())
PP(headblocks)
= allsegments[9]
seg = allsegments[9][1]
name = "bars"
output(seg:rootnode():totreenode():TeX_deftree(name))
= seg:rootnode()
= seg:rootnode():totreenode()
tree = seg:rootnode():totreenode()
= tree
= tree[1]
PPV(tree)
PPV(tree[3][1][1])

print(bigstr)
= proofsty:subtreetolatex(tree, "")
= proofsty:todefded(tree, "NAME")

proofsty.unabbrev = function (ps, str) return "?"..unabbrev(str) end
= proofsty:todefded(tree, "NAME")

--]==]


--  ____                ____                   __     
-- | __ ) _   _ ___ ___|  _ \ _ __ ___   ___  / _|___ 
-- |  _ \| | | / __/ __| |_) | '__/ _ \ / _ \| |_/ __|
-- | |_) | |_| \__ \__ \  __/| | | (_) | (_) |  _\__ \
-- |____/ \__,_|___/___/_|   |_|  \___/ \___/|_| |___/
--                                                    
-- «BussProofs»  (to ".BussProofs")
-- A class that converts a TreeNode to a \defded using bussproofs.
-- Experimental. Version: 2020aug24.

BussProofs = Class {
  type = "BussProofs",
  new  = function () return BussProofs {} end,
  __index = {
    unabbrev = function (bp, str) return unabbrev(str) end,
    subtreetolatex = function (bp, tn, i)
        local i_,i__ = i.." ", i.."  "
        if not tn:hasbar() then
          local r_ = tn:TeX_root()
          return i.."\\AxiomC{$"..bp:unabbrev(r_).."$}"
        else
          local r_ = tn:TeX_root()
          local b_ = tn:barchar()
          local l_ = tn:TeX_label()
          local h_ = tn:hypslist()
          local r  = "\\mathstrut "..bp:unabbrev(r_)
          local s  = function (indent, str)
	                 return str and (indent..str.."\n") or ""
                       end
          local Lines = {["-"]=nil,
                         ["="]="\\doubleLine",
                         ["."]="\\noLine"}
          local Line  = Lines[b_]
          local Label = l_ and l_ ~= "" and format("\\RightLabel{$%s$}", l_)
          local Infs  = {[0] = "\\UnaryInfC",
                         "\\UnaryInfC",
                         "\\BinaryInfC",
                         "\\TrinaryInfC",
                         "\\QuaternaryInfC",
                         "\\QuinaryInfC"}
          local Inf   = format("%s{$%s$}", Infs[#h_], bp:unabbrev(r_))
          local f  = function (tn) return bp:subtreetolatex(tn, i__) end
          local Hyps  = treetex_mapconcat(f, h_, i__.."\n", i__.."\\AxiomC{}")
          return Hyps.."\n"..s(i_,Line)..s(i_,Label)..i..Inf
        end
      end,
    treetolatex = function (bp, tn, i)
        return i.."\\hbox{$\n"..
               bp:subtreetolatex(tn, i).."\n"..
	       i.."\\DisplayProof\n"..
               i.."$}\n"
      end,
    todefded = function (bp, tn, name, link)
        local comment = "   % "..(link or tf:hyperlink())
        return "\\defded{"..name.."}{"..comment.."\n"..
	       bp:treetolatex(tn, "  ")..
               " }"
      end,
  },
}

bussproofs = BussProofs.new()

-- «BussProofs-test»  (to ".BussProofs-test")
--[==[
 (eepitch-lua51)
 (eepitch-kill)
 (eepitch-lua51)
loaddednat6()
require "block"
bigstr = [[
%:                       H
%:  -                   ...
%:  A  B  C   E  F      \Pi
%:  =======r  ::::\phi  ...
%:     D       G         I
%:     -------------------
%:             J
%:
%:             ^bars
%:
]]
output = print
output("foo")
texlines = TexLines.new("test", bigstr)
tf = texlines:toblock()
PP(headblocks)
tf:processuntil(texlines:nlines())
PP(headblocks)
= allsegments[9]
seg = allsegments[9][1]
name = "bars"
output(seg:rootnode():totreenode():TeX_deftree(name))
= seg:rootnode()
= seg:rootnode():totreenode()
tree = seg:rootnode():totreenode()
= tree
= tree[1]
= tree[3]
= tree[3][1]
= tree[3][1][1]
PPV(tree)
PPV(tree[3][1][1])

bp = BussProofs.new()
= bp:subtreetolatex(tree, "")
= bp:treetolatex(tree, "")
= bp:todefded(tree, "NAME")

--]==]



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