-- This file:
--   http://angg.twu.net/LUA/Fitch.lua.html
--   http://angg.twu.net/LUA/Fitch.lua
--           (find-angg "LUA/Fitch.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun n () (interactive) (find-angg "LUA/Fitch.lua"))
-- (defun o () (interactive) (find-angg "LUA/Fitch-old.lua"))

re = require "re"

fitch_gram = [=[
  s            <- ' '
  eol          <- !.

  left         <- {~ leftchar+ ~}
    leftchar   <- [^ /|\]

  vbars        <- {~ barchar (varorspace barchar)* ~}
    barchar    <- [/|\]
    varchar    <- [A-Za-z]
    varorspace <- varchar / s

  vbarlist     <- {| vbar+ |}
    vbar       <- {| ({:v: varchar :} / s*) {:b: barchar :} |}

  middle       <- {~ middlechar+ (s middlechar+)* ~}
    middlechar <- [^ /|\]

  hline        <- {~ '-' '-'+ ~}

  right        <- {~ rightchar+ (s rightchar+)* ~}
    rightchar  <- [^ ]

  sleft        <- {:left: s* left s+ :} / s+
  svbars       <- {:vbars: vbars :}
  smiddle      <- (s {:middle: middle :} / s? {:hline: hline :})
  sright       <- (s s+ {:right: right :} s*) / s*

  fitchline    <- {| sleft svbars smiddle sright |}
]=]

fitch_reP = Re { print = PP, grammar = fitch_gram }
fitch_re0 = Re {             grammar = fitch_gram }
fitch_parseline  = fitch_re0:cc 'top <- fitchline'
fitch_parsevbars = fitch_re0:cc 'top <- vbarlist'

FitchGrid = Class {
  type = "FitchGrid",
  from = function (bigstr)
      fg = FitchGrid {lines={}}
      for _,line in ipairs(splitlines(bigstr)) do
        local pline  = fitch_parseline(line)
        local pvbars = pline and fitch_parsevbars(pline.vbars)
        if pline then
          table.insert(fg.lines, line)
          pline.vbs = pvbars
          table.insert(fg, VTable(pline))
        end
      end
      return fg
    end,
  __tostring = function (fg) return table.concat(fg.lines, "\n") end,
  __index = {
    maxy = function (fg) return #fg end,
    maxx = function (fg, y) return #(fg[y].vbs) end,
    vb   = function (fg, x, y) return fg[y] and fg[y].vbs[x] end,
    v    = function (fg, x, y) return (fg:vb(x, y) or {}).v end,
    b    = function (fg, x, y) return (fg:vb(x, y) or {}).b end,
    ishline = function (fg, y) return fg[y] and fg[y].hline end,
    kluwerletter = function (fg, x, y)
        local isfirst = (fg:b(x,y) == "/")
        local isaboveline = (x == fg:maxx(y)) and fg:ishline(y + 1)
        if isfirst and isaboveline then return "h" end
        if isfirst     then return "b" end
        if isaboveline then return "j" end
        return "a"
      end,
    kluwervbars = function (fg, y)
        str = ""
        for x=1,fg:maxx(y) do
          str = str .. "\\f"..fg:kluwerletter(x, y).." "
        end
        return str
      end,
    kluwerline = function (fg, y)
        if fg:ishline(y) then return nil end
        local lefttex   = fg[y].left or ""
        local vbarstex  = fg:kluwervbars(y)
        local middletex = fg[y].middle
        local righttex  = fg[y].right or ""
        local body = format("\\ftag{%s}{%s%s} & %s \\\\",
                            lefttex, vbarstex, middletex, righttex)
        return body
      end,
    kluwer = function (fg, prefix)
        local lines = {}
        for y=1,fg:maxy() do
          local body = fg:kluwerline(y)
          if body then table.insert(lines, (prefix or "  ")..body) end
        end
        return table.concat(lines, "\n")
      end,
    defftch = function (fg, name)
        local body = fg:kluwer()
        local def = format("\\defftch{%s}{\n  \\begin{fitch}\n%s\n  \\end{fitch}}",
                       name, body)
        return def
      end,
  },
}




fitch_bigstr1 = [=[
  1 / ∃x∀y.P(x,y)
    |--------
  2 |v/u/ ∀y.P(u,y)
    | | |-----
  3 | | | P(u,v)       $∀$E, 2
  4 | | \ ∃x.P(x,v)    $∃$I, 3
  5 | \ ∃x.P(x,v)      $∃$E, 1, 2--5
  6 \ ∀y∃x.P(x,y)      $∀$I, 2--5
]=]


--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "Fitch.lua"

fg = FitchGrid.from(fitch_bigstr1)
= fg
= fg[3]
= fg[4]
= fg[5]
= fg:b(2, 3)
= fg:kluwer()
= fg:defftch("Foo bar")

for _,li in ipairs(splitlines(fitch_bigstr1)) do
  print(li)
  pli = fitch_parseline(li)
  pvb = pli and pli.vbars and fitch_parsevbars(pli.vbars)
  PP("parseline:",  pli)
  PP("parsevbars:", pvb)
  print()
end

--]]





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