Warning: this is an htmlized version! The original is across this link, and the conversion rules are here.
################################################################
#
#	File:	  dednat.icn
#
#	Subject:  convert 2D deduction trees to something that
#		  can be digested by Makoto Tatsuta's proof.sty.
#
#	Author:	  Edrx
#
#	Date:	  started at may 98 (?); last changed 99jan20
#
################################################################
#
# See:
# (find-fline "\$SCTAN/macros/latex/contrib/other/proof/proof.sty")
# (find-fline "~/LATEX/proof.edrx.sty")
# (find-fline "~/LATEX/mar99a.dn")
# (find-fline "~/LATEX/mar99a.dnt")
# (find-fline "~/LATEX/tese2.sty")
# (find-fline "~/LATEX/zinc.icn")
# (find-fline "~/LATEX/zlib.icn")
# (find-fline "~/LATEX/Makefile")
#
################################################################

\$include "zinc.icn"

# a "struct" is something of the form [x0,x2,y,txt].

global lines, lines0
global bigtable				# y->(x0->[x0,x2,y,txt])
global substs
global outfile

\$define MS "° "

# 99sep09:
if li := read() then {
if li ? ="%:*" then		# new hack for embedded "tmp.dn"s
li := li[3:0]
else if li ? ="%:" then
li := "  " || li[3:0]	# don't disturb the tabs
return li
}
fail
end

if /lines then {
lines0 := []
lines := []
while put(lines0, li := readli()) do
put(lines, trim(detab(li)))
#     put(lines, write(trim(detab(li))))
}

# if lines[1]?="%(" then
#   while (*lines > 0) & (lines[1] ~== "%") do
#     pop(lines)[2:0]		# or put(foolines, pop(lines))
#     write(pop(lines)[2:0])	# or put(foolines, pop(lines))

maxwid := 0
every li := !lines do
if *li > maxwid then maxwid := *li

bigtable := []
every y := 1 to *lines do {
li := left(lines[y], maxwid)	# make rectangular
# if li[1] == "%" then		# strip TeX's comment sign
#   li[1] := " "

A := splitwpos(li)
T := table()
every i := 1 to *A do {
x0 := splitpos[i]
txt := A[i]
x2 := x0 + *txt
T[x0] := [x0, x2, y, txt]
}
put(bigtable, T)
}
end

procedure writ(args[])
return write ! ([outfile] ||| args)
# s := ""
# every s ||:= !args
# put(B, s)
# return s
end

procedure intercept(l1, r1, l2, r2)
if (l1 >= r2) | (r1 <= l2) then
fail
return
end

procedure hlist(y)
A := []
every put(A, !(bigtable[y]))
return sortf(A, 1)
end

procedure touching(x0, x2, y)
A := hlist(y)
B := []
every struct := !A do
if intercept(struct[1], struct[2], x0, x2) then
put(B, struct)
if *B > 0 then return B
end

procedure over(struct)
end

procedure barstrtolabel(str)
str ? {
s := ""
c := str[1]
tab(many(c))
if c == "=" then
s := "="
if (rest := tab(0)) ~== "" then
s ||:= "[" || rest || "]"
return s
}
end

procedure node_and_over(indent, struct, rightstr)
text := struct[4]
if not (bar := over(struct)[1]) then
writ(indent, subst(text), rightstr)
else {
label := subst(barstrtolabel(bar[4]))
if not(A := over(bar)) then
writ(indent, "\\infer", label, "{ ", MS, subst(text), " }{}", rightstr)
else {
writ(indent, "\\infer", label, "{ ", MS, subst(text), " }{")
every i := 1 to *A - 1 do
node_and_over(indent || " ", A[i], " &")
node_and_over(indent || " ", A[*A], " }" || rightstr)
}
}
end

procedure structs_array()
A := []
every i := 1 to *bigtable do		# uses that bigtable is an array
every put(A, !(hlist(i)))
return A
end

procedure isdef(struct)
if struct[4]?="^" then
return struct[4][2:0]
end

procedure def(struct)
if s := isdef(struct) then {
struct := copy(struct)
struct[3] -:= 1
root := over(struct)[1]
writ("\\defded{", s, "}{")
node_and_over(" ", root, " }")
return
}
end

procedure subst(s)
every i := 1 to *substs - 1 by 2 do {
s2 := ""
while pos := find(sfrom := substs[i], s) do {
s2 ||:= s[1:pos] || (sto := substs[i + 1])
s := s[pos + *sfrom : 0]
}
s := s2 || s
}
return s
end

procedure main(args)
if args[1] == "-o" then {
outfile := myopen(args[2], "w")
args := args[3:0]
}
else
outfile := &output

substs := []
if args[1] == "-inner" then {
every li := !lines0 do
if li ? ="*" then
substs |||:= split(li, '*\t')
pop(args)
}

every i := 1 to *args - 1 by 2 do
if args[i] == "" then
substs |||:= split(args[i + 1], ' \t\n')
else
substs |||:= [args[i], args[i + 1]]

SA := structs_array()

# Hey. The last struct of all must be a def? Strange. I commented
# out the code that (I guess) converted files without a last def
# to a single immediate tree in \$\$s.
#
#if isdef(SA[-1]) then
every def(!SA)
#else {
#  writ("\$\$")
#  node_and_over("", SA[-1], "")
#  writ("\$\$")
#}
# if \outfile then {
writ("\\endinput")
close(outfile)
# }
end

#   demo_lines := [
# "       acb=ab,cb_À->",
# "       -------------",
# "          cb_À->",
# "          ------",
# "          cbd_eq",
# "          ------",
# "          cbd_=",
# "         ------",
# "  ibk_eq  acbd_= acb=ab",
# "  ------  -------------",
# "  ibk_=       abd_=      abk_cok",
# "  ------      ------------------",
# "  ibkd_=         bkd=bd",
# "  ---------------------",
# "           ibd_=         cbd_eq  ibk_eq",
# "           --------------------  ------",
# "                  icb=ib         ib_À->",
# "                  ---------------------",
# "                          icÀ->"]