Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
-- zha.lua: the ZHA class for dednat6.
-- This file:
-- http://angg.twu.net/dednat6/zha.lua
-- http://angg.twu.net/dednat6/zha.lua.html
--  (find-angg        "dednat6/zha.lua")
--
-- From: (find-angg "sheavesforchildren/zhas.lua")
--
-- This implements a class for calculating with ZHAs.
-- Includes drawing tools, quick ways to compute and/or/imp/not/etc,
-- and a quick way to apply modalities.
--
-- This is mostly obsolete, as it has been replaced by:
--   (find-dn6 "newrect.lua" "ZHA")

-- «.ZHA»		(to "ZHA")
-- «.ZHA-tests»		(to "ZHA-tests")
-- «.ZHA-tests-bf»	(to "ZHA-tests-bf")
-- «.ZHA-tests-fourman»	(to "ZHA-tests-fourman")
-- «.ZHA-tests-imp»	(to "ZHA-tests-imp")

require "wrap"    -- (find-dn6file "wrap.lua" "__mul")
-- (find-angg "LUA/lua50init.lua" "eval-and-L")


-- «ZHA» (to ".ZHA")
ZHA = Class {
  type    = "ZHA",
  specN   = function (spec)
      local copydigit = function (s) return s:sub(1, 1):rep(#s) end
      return (spec:gsub("[1-9][LRV]+", copydigit))
    end,
  fromspec = function (spec)
      local z = ZHA {spec = spec}
      z.specN = ZHA.specN(spec)
      z.maxy  = #spec - 1
      local relL, relR = 0, 0
      local minx, maxx = 0, 0
      for y=1,z.maxy do
        local a, deltaL, deltaR = z:yaction(y)
        relL = relL + deltaL
        relR = relR + deltaR
        minx = min(relL, minx)
        maxx = max(relR, maxx)
      end
      z.x0 = - minx
      z.L = {[0] = z.x0}
      z.R = {[0] = z.x0}
      z.maxx = - minx + maxx
      for y=1,z.maxy do
        local a, deltaL, deltaR = z:yaction(y)
        z.L[y] = z.L[y-1] + deltaL
        z.R[y] = z.R[y-1] + deltaR
      end
      return z
    end,
  fromspeclr = function (spec)
      return ZHA.fromspec(spec):calclrminmax()
    end,
  --
  __index = {
    yC = function (z, y) return          z.spec :sub(y+1, y+1)  end,
    yN = function (z, y) return tonumber(z.specN:sub(y+1, y+1)) end,
    yaction = function (z, y)
          if z:yC(y) == "L"         then return "L", -1, -1 end
          if z:yC(y) == "R"         then return "R",  1,  1 end
          if z:yC(y) == "V"         then return "V",  0,  0 end
          if z:yN(y) == z:yN(y-1)+1 then return "+", -1,  1 end
          if z:yN(y) == z:yN(y-1)-1 then return "-",  1, -1 end
        end,
    --
    -- Coordinates, both (x,y) and (l,r)
    xytol   = function (z, x, y) return (y - (x - z.x0)) / 2 end,
    xytor   = function (z, x, y) return (y + (x - z.x0)) / 2 end,
    xytolr0 = function (z, x, y) return z:xytol(x, y), z:xytor(x, y) end,
    xytolr  = function (z, x, y) return z:xytol(x, y)..z:xytor(x, y) end,
    lrtoxy0 = function (z, l, r) return r - l + z.x0, l + r end,
    lrtolr0 = function (z, lr)
        return tonumber(lr:sub(1, 1)), tonumber(lr:sub(2, 2))
      end,
    lrtoxy  = function (lr)
        local l, r = tonumber(lr:sub(1, 1)), tonumber(lr:sub(2, 2))
        return lrtoxy0(l, r)
      end,
    --
    -- Compute minl[], maxl[], minr[], maxr[], lrtop
    calclrminmax = function (z)
        z.minl, z.minr, z.maxl, z.maxr = {}, {}, {}, {}
        local minmax = function (a, b, c)
            return min((a or b), b), max(b, (c or b))
          end
        local lrminmax = function (l, r)
            z.minl[r], z.maxl[r] = minmax(z.minl[r], l, z.maxl[r])
            z.minr[l], z.maxr[l] = minmax(z.minr[l], r, z.maxr[l])
          end
        for y=0,z.maxy do
          lrminmax(z:xytolr0(z.L[y], y))
          lrminmax(z:xytolr0(z.R[y], y))
        end
        z.lrtop = z:xytolr(z.L[z.maxy], z.maxy)
        return z
      end,
    --
    -- Drawing (in ascii)
    lrline = function (z, y, f)
        f = f or function (lr) return lr end
        s = string.rep("  ", z.L[y]) .. f(z:xytolr(z.L[y], y))
        for x=z.L[y]+2,z.R[y],2 do s = s .. "  " .. f(z:xytolr(x, y)) end
        return s
      end,
    odotline = function (z, y)
        return string.rep(" ", z.L[y]).."o"..string.rep(".o", z:yN(y) - 1)
      end,
    drawf = function (z, f)
        for y=z.maxy,0,-1 do print(z:lrline(y, f)) end
        return z
      end,
    drawL = function (z, str) z:drawf(L(str)); return z end,
    drawE = function (z, str)
        local f = L(str)
        z:drawf(function (P) return Eq(P, f(P)) end)
        return z
      end,
    --
    -- Less or equal (e.g., for testing adjunctions)
    le = function (z, Plr, Qlr)
        local Pl, Pr = z:lrtolr0(Plr)
        local Ql, Qr = z:lrtolr0(Qlr)
        return Pl <= Ql and Pr <= Qr
      end,
    le11 = function (z, Plr, Qlr) return z:le(Plr, Qlr) and "11" or "00" end,
    --
    -- And, Or, Implies, Not
    lrand = function (z, Plr, Qlr)
        local Pl, Pr = z:lrtolr0(Plr)
        local Ql, Qr = z:lrtolr0(Qlr)
        return min(Pl, Ql)..min(Pr, Qr)
      end,
    lror = function (z, Plr, Qlr)
        local Pl, Pr = z:lrtolr0(Plr)
        local Ql, Qr = z:lrtolr0(Qlr)
        return max(Pl, Ql)..max(Pr, Qr)
      end,
    lrimp = function (z, Plr, Qlr)
        local Pl, Pr = z:lrtolr0(Plr)
        local Ql, Qr = z:lrtolr0(Qlr)
        if Pl <= Ql and Pr <= Qr then return z.lrtop end
        if Pl >  Ql and Pr >  Qr then return Qlr end
        if Pl <= Ql then return z.maxl[Qr]..Qr end
        if Ql <= Pl then return Ql..z.maxr[Ql] end
        return "??"
      end,
    lrnot = function (z, Plr) return z:lrimp(Plr, "00") end,
    --
    -- Modalities
    topmostbelowlr0 = function (z, l, r)
        if z.maxr[l] <= r then
          return l..min(z.maxr[l], r)
        else
          return min(z.maxl[r], l)..r
        end
      end,
    topmostbelowlr = function (z, lr)
        return z:topmostbelowlr0(z:lrtolr0(lr))
      end,
    modality0 = function (z, lstr, rstr, l, r)
        local newl = tonumber(lstr:sub(l+1, l+1))
        local newr = tonumber(rstr:sub(r+1, r+1))
        return z:topmostbelowlr0(newl, newr)
      end,
    modality = function (z, lstr, rstr, lr)
        return z:modality0(lstr, rstr, z:lrtolr0(lr))
      end,
    --
    -- Drawing the contour and cuts (in LaTeX)
    lrtopcoords = function (z, dl, dr, l, r)
        -- return format("(%3.1f,%3.1f)", l, r)
        -- return format("(%3.1f,%3.1f)", dl+l, dr+r)
        local newl,newr = dl+l, dr+r
        local x,y = z:lrtoxy0(newl, newr)
        return format("(%3.1f,%3.1f)", x, y)
      end,
    --
    outerangles0 = function (z)
        local left, right = {}, {}
        local l,r = 0,0
        while true do
          l = z.maxl[r]
          table.insert(left, {l=l, r=r});    print("left", l, r)
          r = z.minr[l + 1]
          if not r then break end
          table.insert(left, {l=l, r=r});    print("left", l, r)
        end
        local l,r = 0,0
        while true do
          r = z.maxr[l]
          table.insert(right, {l=l, r=r});    print("right", l, r)
          l = z.minl[r + 1]
          if not l then break end
          table.insert(right, {l=l, r=r});    print("right", l, r)
        end
        return left, right
      end,
    leftcut0  = function (z, l) return z.minr[l+1], z.maxr[l] end,
    rightcut0 = function (z, l) return z.minl[r+1], z.maxr[l] end,
    --
    outerangles = function (z)
        local path = {}
        local corner = function (dl, dr, l, r)
            -- table.insert(path, format("(%f,%f)", l, r))
            table.insert(path, z:lrtopcoords(dl, dr, l, r))
          end
        corner(-0.5, -0.5, 0, 0)
        local ltop, rtop = z:lrtolr0(z.lrtop)
        local left, right = z:outerangles0()
        for _,lr in ipairs(left) do
          corner(0.5, -0.5, lr.l, lr.r)
        end
        corner(0.5, 0.5, ltop, rtop)
        for i=#right,1,-1 do
          local lr = right[i]
          corner(-0.5, 0.5, lr.l, lr.r)
        end
        corner(-0.5, -0.5, 0, 0)
        return "  \\draw[outer] "..table.concat(path, " -- ")..";\n"
      end,
    leftcut = function (z, l)
        local r1, r2 = z.minr[l+1], z.maxr[l]
        return "  \\draw[cut] "..z:lrtopcoords(0.5, -0.5, l, r1).." -- "..
                                 z:lrtopcoords(0.5,  0.5, l, r2)..";\n"
      end,
    rightcut = function (z, r)
        local l1, l2 = z.minl[r+1], z.maxl[r]
        return "  \\draw[cut] "..z:lrtopcoords(-0.5, 0.5, l1, r).." -- "..
                                 z:lrtopcoords( 0.5, 0.5, l2, r)..";\n"
      end,
    --
    genpoints = function (z)
        return cow(function ()
            for y=z.maxy,0,-1 do
              for x=z.L[y],z.R[y],2 do
                local l,r = z:xytolr0(x,y)
                coy(z, x, y, l, r)
              end
            end
          end)
      end,
  },
}


-- zha_utils(): define some global functions
-- for ZHAs, all with very short names
--
zha_utils = function ()
  -- Shorthands for some operations
  Le  = function (P, Q) return z:le11 (P, Q) end
  Or  = function (P, Q) return z:lror (P, Q) end
  And = function (P, Q) return z:lrand(P, Q) end
  Imp = function (P, Q) return z:lrimp(P, Q) end
  Not = function (P) return z:lrnot(P) end
  Top = function () return z.lrtop end
  --
  Eq  = function (P, Q) return P==Q and '11' or '00' end
  --
  -- Elementary J-operators
  -- (find-books "__cats/__cats.el" "fourman")
  -- (find-slnm0753page (+ 14 329)   "2.18 Elementary J-operators")
  Jo  = function (P) return
      function (Q) return Or(P, Q) end
    end
  Ji  = function (P) return
      function (Q) return Imp(P, Q) end
    end
  Jb  = function (R) return
      function (Q) return Imp(Imp(Q, R), R) end
    end
  Jf  = function (P, Q) return
      function (R) return And(Or(P, R), Imp(Q, R)) end
    end
  --
  Jand = function (J1, J2) return
      function (P) return And(J1(P), J2(P)) end
    end
  Jor = function (J1, J2) return
      function (P) return Or(J1(P), J2(P)) end
    end
  --
  -- The generic J-operator:
  Jm = function (lstr, rstr) return
      function (Q) return z:modality(lstr, rstr, Q) end
    end
end

-- M = L "P z:modality('1133556', '02244', P)"
-- M = Jm("1133556", "02244")



--[[

-- «ZHA-tests-bf» (to ".ZHA-tests-bf")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
-- 2015jun19: Tests for explaining brute force
z = ZHA.fromspeclr("1234567654321"):drawf()
z:drawL "P           Not(P)  "
q = '42'; r = '24'
z:drawL "P     Le(P,q)          "
z:drawL "P             Le(P,r)  "
z:drawL "P And(Le(P,q),Le(P,r)) "
q = '42'; r = '24'
z:drawL "P    And(P,q)     "
z:drawL "P Le(And(P,q), r) "
z:drawL "P Le(P, Imp(q,r)) "
= Imp(q,r)

-- «ZHA-tests-imp» (to ".ZHA-tests-imp")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
z = ZHA.fromspeclr("123454321"):drawf()
z:drawL "Q Imp(Q, '22')"
z:drawL "R Imp('22', R)"

-- «ZHA-tests» (to ".ZHA-tests")
-- (find-sfc "zhas.lua" "ZHA-tests")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
ZHA.fromspeclr("12L1RRR2RL1"):drawf()
ZHA.fromspeclr("123LLR432L1"):drawf()
ZHA.fromspeclr("123RRL432R1"):drawf()
ZHA.fromspeclr("12345RR"):drawf()
ZHA.fromspeclr("12345RRRR4321"):drawf()

z = ZHA.fromspec   "123LL432L1"
z = ZHA.fromspeclr("123LL432L1"):drawf()
z:drawL "P           Not(P)  "
z:drawL "P       Not(Not(P)) "
z:drawL "P Eq(P, Not(Not(P)))"
z:drawL "P And(P, '21')"
z:drawL "P Imp(P, '21')"
z:drawL "P Imp('21', P)"
z:drawL "P Le('21', P)"
z:drawL "P Le(P, '21')"

-- Test my definition of "implies":
-- For every Q and R the two "draw"s below
-- should draw the same down-set.
Q, R = "20", "11"
Q, R = "20", "00"
z:drawL "P Le(And(P, Q), R)"
z:drawL "P Le(P, Imp(Q, R))"


-- «ZHA-tests-fourman» (to ".ZHA-tests-fourman")
-- (find-sfc "zhas.lua" "ZHA-tests")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
-- Elementary J-operators
-- (find-books "__cats/__cats.el" "fourman")
-- (find-slnm0753page (+ 14 329)   "2.18 Elementary J-operators")
-- (find-xdvipage "~/LATEX/istanbulquotes.dvi")
Jsub = function (a) return function (p) return Or(a, p) end end
Jsup = function (a) return function (p) return Imp(a, p) end end
Bsub = function (a) return function (p) return Imp(Imp(p, a), a) end end
JJ = function (a, b) return function (p) return And(Or(a, p), Imp(b, p)) end end
z = ZHA.fromspeclr("123454321"):drawf()
z:drawL "p           Jsub'22'(p)  "
z:drawL "p           Jsup'22'(p)  "
z:drawL "p           Bsub'22'(p)  "
z:drawL "p      JJ('31','13')(p)  "
z = ZHA.fromspeclr("12345678987654321"):drawf()
z:drawL "p     JJ('52',       '25')(p)"
z:drawL "p     Or('52',p)             "
z:drawL "p                Imp('25',p) "
z:drawL "p And(Or('52',p),Imp('25',p))"

= Imp(Imp('12','23'),'40')
= JJ('12','23')('40')


* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()

z = ZHA.fromspeclr("1234567654321"):drawf()
My = Jm("0123456", "0123456")
My = Jm("0133456", "0144456")
z:drawf(L "P Eq(P, My(P))")
z:drawL   "P Eq(P, My(P))"
z:drawE   "P       My(P) "

-- (find-books "__cats/__cats.el" "fourman")
-- (find-slnm0753page (+ 14 329) "2.18 Elementary J-operators")
-- (find-slnm0753page (+ 14 329) "(i)  J_a p = a v p")
-- (find-slnm0753page (+ 14 330) "(ii) J^a p = a -> p")

z:drawE "P                Jo'25' (P)"
z:drawE "P        Jo'41'         (P)"
z:drawE "P                Ji'25' (P)"
z:drawE "P        Ji'41'         (P)"

-- (find-slnm0753page (+ 14 331) "(i) J_a v J_b = J_avb")
z:drawE "P Jor(Jo'41',  Jo'25')(P)"
z:drawE "P Jo(Or('41',   '25'))(P)"

-- (find-slnm0753page (+ 14 331) "(ii) J^a v J^b = J_a&b")
z:drawE "P Jor(Ji'41', Ji'25')(P)"
z:drawE "P Ji(And('41',  '25'))(P)"

-- (find-slnm0753page (+ 14 331) "(iii) J_a & J_b = J_a&b")
z:drawE "P Jand(Jo'41',  Jo'25')(P)"
z:drawE "P Jo(And('41',   '25'))(P)"

-- (find-slnm0753page (+ 14 331) "(iv) J^a & J^b = J^avb")
z:drawE "P Jand(Ji'41', Ji'25')(P)"
z:drawE "P Ji(Or('41',  '25'))(P)"

-- (find-slnm0753page (+ 14 331) "(v) J_a & J^a = bot")
z:drawE "P Jand(Jo'41', Ji'41')(P)"

-- (find-slnm0753page (+ 14 331) "(vi) J_a v J^a = top")
z:drawE "P Jor(Jo'41', Ji'41')(P)"

-- (find-slnm0753page (+ 14 331) "(vii) J_a v K = K o J_a")
z:drawE "P Jor(Jo'41', My)(P)"
z:drawE "P My(Jo'41'(P))"

-- (find-slnm0753page (+ 14 331) "(viii) J^a v K = J_a o K")
z:drawE "P Jor(Ji'41', My)(P)"
z:drawE "P Ji'41'(My(P))"

-- (find-slnm0753page (+ 14 331) "(ix) J_a v B_a = B_a")
z:drawE "P Jor(Jo'41', Jb'41')(P)"
z:drawE "P Jb'41'(P)"

-- (find-slnm0753page (+ 14 331) "(x) J^a v B_b = B_a->b")
z:drawE "P Jor(Ji'41', Jb'25')(P)"
z:drawE "P Jb(Imp('41', '25'))(P)"

z:drawE "P Jand(Jb'44', Jb'22')(P)"
z:drawE "P Jand(Jand(Jb'44', Jb'22'), Jb'00')(P)"



z:drawE "P Ji(Or('41',  '25'))(P)"
z:drawE "P Ji(Or('41',  '25'))(P)"
z:drawE "P Jb('23')(P)"
z:drawE "P Jb('41', '25')(P)"
z:drawE "P   Jand(Jo'41', Jo'25')(P)         "
z:drawE "P   Jo(And('41',  '25'))(P)         "
z:drawf(L "P Eq(P,     Jo'41'(P))            ")
z:drawf(L "P Eq(P,                Jo'25'(P)) ")
z:drawf(L "P Eq(P, And(Jo'41'(P), Jo'25'(P)))")
z:drawf(L "P Eq(P, Jo(And('41',   '25'))(P)) ")
z:drawf(L "P Eq(P,     Ji'41'(P))            ")
z:drawf(L "P Eq(P,                Ji'25'(P)) ")
z:drawf(L "P Eq(P, And(Ji'41'(P), Ji'25'(P)))")
z:drawf(L "P Eq(P, Jo(And('41',   '25'))(P)) ")

-- M = Jm("1133556", "02244")


--]]


-- Local Variables:
-- coding: raw-text-unix
-- End: