################################################################
#
#	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:
procedure readli()
  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

procedure read_lines()
  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)
  return touching(struct[1], struct[2], struct[3] - 1)
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

  read_lines()

  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À->"]