-- This file: -- https://anggtwu.net/LUA/TreeTeX1.lua.html -- https://anggtwu.net/LUA/TreeTeX1.lua -- (find-angg "LUA/TreeTeX1.lua") -- Author: Eduardo Ochs -- Version: 2026jul01 -- -- (defun e () (interactive) (find-angg "LUA/TreeTeX1.lua")) -- (defun o () (interactive) (find-dn6 "treetex.lua")) -- (defun o () (interactive) (find-angg "LUA/TreeSegs1.lua")) -- «.ProofSty» (to "ProofSty") -- «.ProofSty-DefDed» (to "ProofSty-DefDed") -- «.ProofSty-test» (to "ProofSty-test") -- «.BussProofs» (to "BussProofs") -- «.BussProofs-test» (to "BussProofs-test") -- «.EBProof» (to "EBProof") -- «.EBProof-DefDed» (to "EBProof-DefDed") -- «.EBProof-test» (to "EBProof-test") require "TreeSegs1" -- (find-angg "LUA/TreeSegs1.lua") require "Pict4" -- (find-angg "LUA/Pict4.lua") -- For tests unabbrev = unabbrev or id -- (find-angg "LUA/PictRect1.lua" "Pict") picts_concat = function (picts, sep) if #picts == 0 then return end local result = picts[1] for i=2,#picts do result = (result + sep) / picts[i] end return result end picts_mapconcat = function (f, objs, sep) return picts_concat(map(f, objs), sep) end -- ____ __ ____ _ -- | _ \ _ __ ___ ___ / _/ ___|| |_ _ _ -- | |_) | '__/ _ \ / _ \| |_\___ \| __| | | | -- | __/| | | (_) | (_) | _|___) | |_| |_| | -- |_| |_| \___/ \___/|_| |____/ \__|\__, | -- |___/ -- -- «ProofSty» (to ".ProofSty") -- A class that converts a TreeNode to a \defded using Makoto -- Tatsuta's proof.sty. ProofSty = Class { type = "ProofSty", new = function () return ProofSty {} end, __index = { unabbrev = function (psty, str) return unabbrev(str) end, tntopict = function (psty, tn) if not tn:hasbar() then return Pict {"\\mathstrut "..psty:unabbrev(tn:TeX_root())} else local f = function (tn) return psty:tntopict(tn) end local r_ = tn:TeX_root() local b_ = tn:barchar() local l_ = tn:TeX_label() local h_ = tn:hypslist() or {} local r = "\\mathstrut "..psty:unabbrev(r_) local b = ({["-"]="infer", ["="]="infer=", [":"]="infer*", ["."]="deduce"})[b_] local l = (l_ and "[{"..psty:unabbrev(l_).."}]") or "" local bb = "\\"..b..l.."{ "..r.." }{" local ee = "}" local hh = picts_mapconcat(f, h_, " &") or Pict {} if #hh == 0 then return Pict { bb.." "..ee } end return bb / (" " .. (hh + (" "..ee))) end end, defded = function (psty, name, rootnode, comment) local head = "\\defded{"..name.."}{"..comment local body = psty:tntopict(rootnode) return head / (" " .. (body + " }")) end, }, } proofsty = ProofSty.new() -- «ProofSty-DefDed» (to ".ProofSty-DefDed") -- Replaces: (find-angg "LUA/TreeSegs1.lua" "DefDed" "output =") DefDed.__index.output = function (dd) return dd:output_proofsty() end -- «ProofSty-test» (to ".ProofSty-test") --[==[  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) require "TreeTeX1" = treesegtest [[ %: H %: - ... %: A B C E F \Pi %: =======r ::::\phi ... %: D G I %: ------------------- %: J %: %: ^bars ]] = allsegments = allsegments[y-1][1] = allsegments[y-1][1]:rootnode() tn = allsegments[y-1][1]:rootnode():totreenode() = tn = proofsty:tntopict(tn) = proofsty:defded("Bars", tn, " % Foos") --]==] -- ____ ____ __ -- | __ ) _ _ ___ ___| _ \ _ __ ___ ___ / _|___ -- | _ \| | | / __/ __| |_) | '__/ _ \ / _ \| |_/ __| -- | |_) | |_| \__ \__ \ __/| | | (_) | (_) | _\__ \ -- |____/ \__,_|___/___/_| |_| \___/ \___/|_| |___/ -- -- «BussProofs» (to ".BussProofs") -- A class that converts a TreeNode to a \defded using bussproofs. -- Status: Buggy! Generated broken bussproofs code! Use EBProof instead! -- See: (find-es "tex" "bussproofs") BussProofs = Class { type = "BussProofs", new = function () return BussProofs {} end, __index = { unabbrev = function (bp, str) return unabbrev(str) end, tntopict = function (bp, tn) local f = function (tn) return bp:tntopict(tn) end if not tn:hasbar() then local r_ = tn:TeX_root() return Pict {"\\AxiomC{$"..bp:unabbrev(r_).."$}"} else local h_ = tn:hypslist() or {} local hp = map(f, h_) local hh = picts_concat(hp, "") or Pict {} local b_ = tn:barchar() local bb = ({["-"]=nil, ["="]="\\doubleLine", ["."]="\\noLine"})[b_] local l_ = tn:TeX_label() local ll = (l_ and l_~="" and format("\\RightLabel{$%s$}", l_)) or nil local r_ = tn:TeX_root() local rr = "\\mathstrut "..bp:unabbrev(r_) local i_ = ({[0] = "UnaryInfC", "UnaryInfC", "BinaryInfC", "TrinaryInfC", "QuaternaryInfC", "QuinaryInfC"})[#h_] or error("Hypslist too big") local ii = format("\\%s{$%s$}", i_, bp:unabbrev(r_)) return (" " * (hh/Pict{bb}/Pict{ll})) / ii end end, tntopict_d = function (bp,tn) return "\\DisplayProof" / bp:tntopict(tn) end, tntopict_db = function (bp,tn) return "\\hbox{$" / (" " .. (bp:tntopict_d(tn) / "$}")) end, defded = function (bp, name, rootnode, comment) local head = "\\defded{"..name.."}{"..comment local body = bp:tntopict_db(rootnode) return head / (" " .. (body + "}")) end, }, } bussproofs = BussProofs.new() -- «BussProofs-test» (to ".BussProofs-test") --[==[  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) dofile "TreeTeX1.lua" = treesegtest [[ %: H %: - ... %: A B C E F \Pi %: =======r ::::\phi ... %: D G I %: ------------------- %: J %: %: ^bars ]] = allsegments = allsegments[y-1][1] = allsegments[y-1][1]:rootnode() tn = allsegments[y-1][1]:rootnode():totreenode() = tn = tn[1] = tn[1][1] = bussproofs:tntopict (tn) = bussproofs:tntopict_d (tn) = bussproofs:tntopict_db(tn) = bussproofs:defded("Foo", tn, "") --]==] -- _____ ____ ____ __ -- | ____| __ )| _ \ _ __ ___ ___ / _| -- | _| | _ \| |_) | '__/ _ \ / _ \| |_ -- | |___| |_) | __/| | | (_) | (_) | _| -- |_____|____/|_| |_| \___/ \___/|_| -- -- «EBProof» (to ".EBProof") -- A class that converts a TreeNode to a \defded using ebproof. -- See: (find-es "tex" "ebproof") EBProof = Class { type = "EBProof", new = function () return EBProof {} end, __index = { unabbrev = function (eb, str) return unabbrev(str) end, tntopict = function (eb, tn) local f = function (tn) return eb:tntopict(tn) end if not tn:hasbar() then local r_ = tn:TeX_root() return Pict {"\\hypo{"..eb:unabbrev(r_).."}"} else local h_ = tn:hypslist() or {} local hp = map(f, h_) local hh = picts_concat(hp, "") or Pict {} local b_ = tn:barchar() local bb = ({["-"]="\\infer", ["="]="\\infer[double]", ["."]="\\infer[no rule]", [":"]="\\infer[dashed]", --[":"]="\\ellipsis"}, })[b_] local l_ = tn:TeX_label() local ll = (l_ and l_~="" and format("[$%s$]", l_)) or "" local r_ = tn:TeX_root() local rr = "\\mathstrut "..eb:unabbrev(r_) local ii = format("%s%d%s{%s}", bb, #h_, ll, rr) return (" " * hh) / ii end end, tntopict_b = function (eb,tn) return "\\begin{prooftree}" / (" "..eb:tntopict(tn)) / "\\end{prooftree}" end, defded = function (eb, name, rootnode, comment) local head = "\\defded{"..name.."}{"..comment local body = eb:tntopict_b(rootnode) return head / (" " .. (body + "}")) end, }, } ebproof = EBProof.new() -- «EBProof-DefDed» (to ".EBProof-DefDed") -- Replaces: (find-angg "LUA/TreeSegs1.lua" "DefDed" "output =") --DefDed.__index.output = function (dd) return dd:output_proofsty() end -- «EBProof-test» (to ".EBProof-test") --[==[  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) dofile "TreeTeX1.lua" = treesegtest [[ %: H %: - ... %: A B C E F \Pi %: =======r ::::\phi ... %: D G I %: ------------------- %: J %: %: ^bars ]] = allsegments = allsegments[y-1][1] = allsegments[y-1][1]:rootnode() tn = allsegments[y-1][1]:rootnode():totreenode() = tn = tn[1] = tn[1][1] = ebproof:tntopict (tn) = ebproof:tntopict_b(tn) = ebproof:defded("Foo", tn, "") --]==] -- Local Variables: -- coding: utf-8-unix -- End: