-- This file:
--   http://angg.twu.net/LATEX/2021fitch.lua.html
--   http://angg.twu.net/LATEX/2021fitch.lua
--           (find-angg "LATEX/2021fitch.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LATEX/2021fitch.tex"))
-- (defun f () (interactive) (find-angg "LATEX/2021fitch.lua"))
--
-- See: (find-angg "LUA/Fitch.lua")
-- See: (find-angg "LUA/Fitch.lua")

-- «.fitch_gram»	(to "fitch_gram")
-- «.fitch_gram-tests»	(to "fitch_gram-tests")
-- «.FitchGrid»		(to "FitchGrid")
-- «.fitch-head»	(to "fitch-head")
-- «.defftch»		(to "defftch")

re = require "re"


--  ____                     
-- |  _ \ __ _ _ __ ___  ___ 
-- | |_) / _` | '__/ __|/ _ \
-- |  __/ (_| | |  \__ \  __/
-- |_|   \__,_|_|  |___/\___|
--                           
-- «fitch_gram»  (to ".fitch_gram")
--
fitch_gram = [=[
  s            <- ' '
  eol          <- !.

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

  vbars        <- { firstbar anotherbar* }
    firstbar   <-         barchar
    anotherbar <- var? s? barchar
    var        <- varchar+
    varchar    <- [A-Za-z]
    barchar    <-        [/|\]

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

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

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

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

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

  fitchline    <- {| sleft svbars s* 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'

-- «fitch_gram-tests»  (to ".fitch_gram-tests")
--[==[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2021fitch.lua"
pli = fitch_reP:cc 'top <- fitchline'
pvb = fitch_reP:cc 'top <- vbarlist'

pli = fitch_reP:cc 'top <- {| sleft svbars |}'
pli [=[ 4 | | .vdots    foo ]=]
pli [=[ 4 | | . vdots   foo ]=]
pli [=[ 4 | | vd\ot s   foo ]=]
pli [=[ 4 | | \vdot s   foo ]=]
pli [=[ 4 | | {\vdot s} foo ]=]
pli [=[ ab|c| de {\vdot s} foo ]=]
pli [=[ ab|c| de {\vdot s}  foo ]=]
pli [=[ ab|c | de {\vdot s}  foo ]=]
pli [=[ ab|c |  de {\vdot s}  foo ]=]
pli [=[ ab| c| de {\vdot s}  foo ]=]
pli [=[ ab| c|  de {\vdot s}  foo ]=]
pli [=[ ab|c |de {\vdot s}  foo ]=]
pli [=[ ab|c |----          foo ]=]

--]==]



--  _____ _ _       _      ____      _     _ 
-- |  ___(_) |_ ___| |__  / ___|_ __(_) __| |
-- | |_  | | __/ __| '_ \| |  _| '__| |/ _` |
-- |  _| | | || (__| | | | |_| | |  | | (_| |
-- |_|   |_|\__\___|_| |_|\____|_|  |_|\__,_|
--                                           
-- «FitchGrid»  (to ".FitchGrid")
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,
    texmiddle = function (fg, str) return str end,
    texright  = function (fg, str) 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:texmiddle(fg[y].middle)
        local righttex  = fg:texright(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
    | | \ \vdots
  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 "2021fitch.lua"

fg = FitchGrid.from(fitch_bigstr1)
= fg
= fg[2]
= fg[3]
= fg[4]
= fg[5]
= fg[6]
= 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

--]]


-- «fitch-head»  (to ".fitch-head")
-- (find-dednat6 "myverbatim.lua" "myverbatim-head")
registerhead = registerhead or function () return nop end
registerhead "%F" {
  name   = "ftch",
  action = function ()
      local i,j,origlines = tf:getblock()
      ftch_lines = origlines
    end,
}

-- «defftch»  (to ".defftch")
defftch = function (name)
    local bigstr = table.concat(ftch_lines, "\n")
    local fg = FitchGrid.from(bigstr)
    local def = fg:defftch(name)
    print(bigstr)
    output(def)
  end