|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- This file:
-- https://anggtwu.net/LUA/TreeTeX1.lua.html
-- https://anggtwu.net/LUA/TreeTeX1.lua
-- (find-angg "LUA/TreeTeX1.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- 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: