-- This file:
-- http://angg.twu.net/dednat6/dednat6/underbrace.lua
-- http://angg.twu.net/dednat6/dednat6/underbrace.lua.html
--         (find-angg "dednat6/dednat6/underbrace.lua")
--
-- This is obsolete, and has been superseded by:
-- http://angg.twu.net/dednat6/dednat6/underbrace2d.lua
-- http://angg.twu.net/dednat6/dednat6/underbrace2d.lua.html
--         (find-angg "dednat6/dednat6/underbrace2d.lua")
--
-- This was a quick hack that I used in early versions of my paper
-- "Planar Heyting Algebras for Children", but I replaced all code
-- that used this by code that uses underbrace2d.
--
--
-- The easiest way to work with user-given expressions in dednat6 is
-- to build them as syntactic trees using a stack-based, Forth-like
-- language. We want to generate two kinds of output from these
-- expressions: 1) 2D ascii diagrams, 2) LaTeX output, mainly for
-- "underbrace structures" like this one:
--
--    P & Q -> P
--   \-/ \-/  \-/
--    0   1    0
--   \-----/
--      0
--   \----------/
--          1
--
-- THIS IS NOT USED "OFICIALLY" YET, because the class Stack defined
-- here may conflict with: (find-dn6 "diagstacks.lua" "Stack")
-- See:
--   (find-ist "-handouts.tex" "brute-force")
--   (find-ist "all.lua" "Stack")


-- «.synttotex»		(to "synttotex")
-- «.ubs»		(to "ubs")
-- «.ubs-tests»		(to "ubs-tests")

require "stacks"   -- (find-dn6 "stacks.lua")
require "rect"     -- (find-dn6 "rect.lua")

-- «synttotex» (to ".synttotex")
-- This is used by ubstex to generate LaTeX from a tree object.
synttotex = function (o)
    if type(o) == "string" then return o end
    if type(o) == "table" then
      return (o.tex:gsub("<([%d])>", function (n) return synttotex(o[n+0]) end))
    end
    error()
  end

--        _         
--  _   _| |__  ___ 
-- | | | | '_ \/ __|
-- | |_| | |_) \__ \
--  \__,_|_.__/|___/
--                  
-- «ubs» (to ".ubs")
ubs_doword = function (s, word)
    local o = function ()    return s:pop() end
    local u = function (obj) return s:push(obj) end
    if     word == "()"  then u {"(", o(), ")", tex="(<2>)"}
    elseif word == "u"   then u {[0]=o(), o(), tex="\\underbrace{\n<1>\n}_{<0>}"}
    elseif word == "bin" then u {[2]=o(), [3]=o(), [1]=o(), tex="<1> <2>\n <3>"}
    elseif word == "Bin" then u {[3]=o(), [2]=o(), [1]=o(), tex="<1> <2>\n <3>"}
    elseif word == "pre" then u {[1]=o(), [2]=o(), tex="<1> <2>"}
    elseif word == "Pre" then u {[2]=o(), [1]=o(), tex="<1> <2>"}
    elseif word == "def" then u {[1]=o(), [2]=o(), tex="\\def\\<1>{<2>}"}
    elseif word == "output" then output(synttotex(s:pick(0)))
    else   u(word)
    end
    return s
  end
ubs0 = function (bigstr) return Stack.dowords(ubs_doword, bigstr) end
ubstree = function (bigstr) return synttorect(ubs0(bigstr)) end
ubstex  = function (bigstr) return synttotex (ubs0(bigstr)) end

ubs = function (bigstr) return ubstex(bigstr) end  -- quiet
ubs = function (bigstr)
    print(ubstree(bigstr)); print()        -- verbose behavior: print the tree
    return ubstex(bigstr)                  -- and return the LaTeX code
  end
ubs = function (bigstr)
    local syntree = ubs0(bigstr)
    print(synttorect(syntree)); print()    -- verbose behavior: print the tree
    return synttotex(syntree)               -- and return the LaTeX code
  end


--[==[
-- «ubs-tests» (to ".ubs-tests")
• (eepitch-lua51)
• (eepitch-kill)
• (eepitch-lua51)
dofile "underbrace.lua"
--
-- (find-istfile "1.org" "Some non-tautologies: DeMorgan")
--
-- !(P  & Q)->(! P v  ! Q)
--   10  01      10    01
--     00      02    20
-- 32              22
--          22
--
= ubs "P Q \\& bin () 2 + bin"
= ubs [[
  P 10 u   Q 01 u   \& bin 00 u    () \neg pre 32 u
  P 10 u   \neg pre 02 u   Q 01 u \neg pre 20 u   \lor bin 22 u ()
  \to bin 22 u
]]

PP(ubs("a () ()"))
= synttorect(ubs("a () ()"))
= synttorect(ubs([[ P 10 u ]]))
= synttorect(ubs([[ P 10 u Q 01 u \& bin ]]))
= synttorect(ubs([[ P 10 u Q 01 u \& bin 00 u    () \neg pre 32 u ]]))
= ubs [[ P 10 u Q 01 u \& bin 00 u    () \neg pre 32 u ]]

= ubstree [[ P 0 u Q 1 u \& bin 0 u ]] 
= ubstree  [[ P 0 u   Q 1 u   \& bin 0 u   P 0 u   -> bin 1 u ]] 
= ubs      [[ P 0 u   Q 1 u   \& bin 0 u   P 0 u   -> bin 1 u ]] 

• (eepitch-lua51)
• (eepitch-kill)
• (eepitch-lua51)
dofile "underbrace.lua"
-- (P <= Q & R) <-> (P <= Q) & (P <= R)
--       21 12           21         12
--       \---/       \----/     \----/
--         ?          \ra        \rb
-- \---------/      \-----------------/
--    \rd                   \rc
--
ubs_brute_force_and
= ubs [[
  P   Q 21 u   R 12 u  \& bin ? u   \le bin \rd u ()
  P   Q 21 u   \le bin \ra u ()
  P   R 21 u   \le bin \rb u ()
  \& bin \rc u
  \bij bin
]]
= ubs_brute_force_and

ubs_brute_force_imp
= ubs [[
  P   Q 21 u   R 12 u   \to bin ? u    \le bin \Rc u ()
  P   Q 21 u   \land bin \Ra u   R 12 u   \le bin \Rb u ()
  \bij bin
]]

• (eepitch-lua51)
• (eepitch-kill)
• (eepitch-lua51)
dofile "underbrace.lua"
output = function (str) print("<<"..str..">>") end
ubs0  [[ P 10 u   Q 01 u   \& bin 00 u   Foo def   output ]]
ubs   [[ P 10 u   Q 01 u   \& bin 00 u   Foo def   output ]]
= ubs [[ P 10 u   Q 01 u   \& bin 00 u   Foo def   output ]]

--]==]











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