-- This file: -- http://angg.twu.net/dednat6/extra-modules.txt.html -- http://angg.twu.net/dednat6/extra-modules.txt -- (find-dednat6 "extra-modules.txt") -- -- Dednat6's main page is at: -- http://angg.twu.net/dednat6.html -- -- This is a hacker's guide to the modules of dednat6 that deal with -- Planar Heyting Algebras and 2-column graphs - the ZHAs and 2CGs of -- this series of papers: -- -- http://angg.twu.net/math-b.html#zhas-for-children-2 -- -- I doubt that other people would want to use those modules, at least -- in their present messy form, but I hope that this text will give -- people some ideas on how they can write their own extensions to -- dednat6 - as quick hacks or not. -- -- This file is made of "executable notes" in the sense of: -- -- http://angg.twu.net/emacsconf2019.html -- http://angg.twu.net/#eev -- -- it is made of text intermixed with sexp hyperlinks and eepitch -- blocks. If you want to _read_ this, just access this URL: -- -- http://angg.twu.net/dednat6/extra-modules.txt.html -- -- all the sexp hyperlinks should work there (in htmlized form). -- If you want to execute by yourself the executable parts you will -- need Emacs, eev, this patch to eepitch, -- -- (find-es "eev" "eepitch-indented") -- -- and a couple of customizations. Please nudge me if you're -- interested! -- -- Eduardo Ochs -- http://angg.twu.net/contact.html -- Version: 2020apr18 -- Public domain. «.introduction» (to "introduction") «.ZHA» (to "ZHA") «.AsciiPicture» (to "AsciiPicture") «.BoundingBox» (to "BoundingBox") «.Cuts» (to "Cuts") «.MixedPicture» (to "MixedPicture") «.J-operators» (to "J-operators") «.LPicture» (to "LPicture") «.AsciiRect» (to "AsciiRect") «introduction» (to ".introduction") 0. Introduction =============== Main resources: http://angg.twu.net/dednat6.html http://angg.twu.net/dednat6.html#a-big-example http://angg.twu.net/dednat6/tug-slides.pdf (find-pdf-page "~/dednat6/tug-slides.pdf") (find-pdf-page "~/dednat6/tug-slides.pdf" 17 "Extensions") (find-pdf-page "~/dednat6/tug-slides.pdf" 23 "get in touch") http://angg.twu.net/dednat6/tugboat-rev2.pdf (find-pdf-page "~/dednat6/tugboat-rev2.pdf") http://angg.twu.net/dednat6.html#quick-start http://angg.twu.net/#eev http://angg.twu.net/emacsconf2019.html ^ "How to record executable notes with eev - and how to play them back"  (eepitch-shell)  (eepitch-kill)  (eepitch-shell) rm -Rfv /tmp/dednat6/ mkdir /tmp/dednat6/ cd /tmp/dednat6/ wget http://angg.twu.net/dednat6.zip unzip dednat6.zip make veryclean # (find-fline "/tmp/dednat6/") # (find-fline "/tmp/dednat6/demo-minimal.tex") lualatex demo-minimal.tex xpdf -fullscreen demo-minimal.pdf «ZHA» (to ".ZHA") 1. ZHAs in ASCII ================ Dednat6 comes with some .lua files that implement extensions that are only useful to me ("me" = Eduardo Ochs). This is the part of dednat6/dednat6.lua that loads them: -- From: -- (find-dednat6 "dednat6/dednat6.lua" "requires") -- (find-dednat6 "dednat6/dednat6.lua" "requires" "Code for" "ZHAs:") -- Code for handling and drawing ZHAs: require "picture" -- (find-dn6 "picture.lua") require "zhas" -- (find-dn6 "zhas.lua") require "zhaspecs" -- (find-dn6 "zhaspecs.lua") require "tcgs" -- (find-dn6 "tcgs.lua") require "luarects" -- (find-dn6 "luarects.lua") I started writing them because I needed to draw ZHAs in ascii and LaTeX in several ways. I started with code to represent ZHA objects in Lua, draw them in ascii, and calculate with them (the implication is non-trivial): -- See: -- (find-dednat6 "dednat6/zhas.lua" "ZHA-tests") -- (find-dednat6 "dednat6/zhas.lua" "MixedPicture-tests")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() z = ZHA.fromspec("12321L") = z z:PP() My class for 2D vectors supports LR coordinates, and the class for ZHAs uses that to refer to the elements of a ZHA: -- See: -- (find-dednat6 "dednat6/picture.lua" "V") -- (find-dednat6 "dednat6/picture.lua" "V-tests") -- (find-dednat6 "dednat6/zhas.lua" "ZHA-connectives")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() = V.fromab(-2, 2) = V.fromab("(-2,2)") = V.fromab("20") = v(-2, 2) = v"20" = v"20":xy() = v"20":lr() z = ZHA.fromspec("1234321L") = z = z:Imp(v"21", v"12"):lr() The ZHA class has a methods :points() that generates all the points in a ZHA: -- See: -- (find-dednat6 "dednat6/zhas.lua" "ZHA") -- (find-dednat6 "dednat6/zhas.lua" "ZHA" "points =") -- (find-dednat6 "dednat6/zhas.lua" "ZHA-test-generators")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() z = ZHA.fromspec("12321L") = z for p in z:points() do print(p:lr()) end If you look at the source for the method :points() you will see that it uses "cow" and "coy", that are my abbreviations for coroutine.wrap and coroutine.yield: -- (find-dednat6 "dednat6/zhas.lua" "ZHA") -- (find-dednat6 "dednat6/zhas.lua" "ZHA" "points =") -- (find-dednat6 "dednat6/edrxlib.lua" "cow-and-coy") The __tostring method of the ZHA class constructs the lines of the ascii representation of the ZHA one by one in a low-level way, using the method tolines(): -- (find-dednat6 "dednat6/zhas.lua" "ZHA") -- (find-dednat6 "dednat6/zhas.lua" "ZHA" "__tostring =") -- (find-dednat6 "dednat6/zhas.lua" "ZHA" " tostring =") -- (find-dednat6 "dednat6/zhas.lua" "ZHA" "tolines =") The methods :tolines() works roughly like this, but it returns a string:  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() z = ZHA.fromspec("12321L") = z for y = z.maxy, 0, -1 do for x = z.minx, z.maxx do printf(z:xycontents(x, y) or " ") end print() end Note that points (x,y) that do not belong to the ZHA z are printed as exactly two spaces. «AsciiPicture» (to ".AsciiPicture") 2. AsciiPicture =============== Ater I implemented a class AsciiPicture that generalized the idea behind :tolines(), of a 2D rectangle of 2-char wide "cells" that are somehow concatenated into a string with newlines: -- (find-dednat6 "dednat6/picture.lua" "AsciiPicture") -- (find-dednat6 "dednat6/picture.lua" "AsciiPicture-tests")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() z = ZHA.fromspec("12321L") = z ap = AsciiPicture.new(" ") for p in z:points() do ap:put(p, "..") end = ap ap = AsciiPicture.new(" ") for p in z:points() do ap:put(p, p:lr()) end = ap ap = AsciiPicture.new(" ") for p in z:points() do ap:put(p, p:xy()) end = ap PPV(ap) PP(ap.s) = ap ap.s = " " = ap «BoundingBox» (to ".BoundingBox") 3. BoundingBox ============== An AsciiPicture object uses a BoundingBox object to store the coordinates of the lower left cell and upper right cell, and to adjust these coordinates as more cells are added. See: -- (find-dednat6 "dednat6/picture.lua" "BoundingBox") -- (find-dednat6 "dednat6/picture.lua" "BoundingBox-tests")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() bb = BoundingBox.new() = bb = bb:addpoint(v(2, 4)) = bb:addpoint(v(5, 10)) = bb:addbox(v(5, 10), v(.5, .5)) = bb:addbox(v(1, 2), v(.5, .5)) «Cuts» (to ".Cuts") 4. Cuts in ASCII ================ -- See: -- (find-dednat6 "dednat6/zhas.lua" "Cuts") -- (find-dednat6 "dednat6/zhas.lua" "Cuts-tests")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() c = Cuts.new() = c:addcuts0{v"00":w(), v"01":n(), v"01":e()} = c.asciibb = c.latexbb = c.minicuts z = ZHA.fromspec("12321L") = z = c:addcontour(z) = c.minicuts = c.latex «MixedPicture» (to ".MixedPicture") 5. MixedPicture =============== -- See: -- (find-dednat6 "dednat6/zhas.lua" "MixedPicture") -- (find-dednat6 "dednat6/zhas.lua" "MixedPicture-tests") -- (find-dednat6 "dednat6/zhas.lua" "mpnew")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() mp = mpnew({}, "12321L") = mp = mp:addcontour() = mp:addlrs() PPV(mp) = mp.zha -- a ZHA object = mp.cuts -- a Cuts object = mp.ap -- an AsciiPicture object = mp.lp -- an LPicture object (explained below) = mp.cuts.latex -- a string = mp:tolatex()  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() kite = ".1.\n" .. "2.3\n" .. ".4.\n" .. ".5." kite = ".1.|2.3|.4.|.5." mp = MixedPicture.new({def="dagKite"}):zfunction(kite) = mp = mp:tolatex() «J-operators» (to ".J-operators") 6. J-operators ============== -- See: -- (find-dednat6 "dednat6/zhas.lua" "mpnewJ") -- (find-dednat6 "dednat6/zhas.lua" "MixedPicture-J-tests") -- (find-dednat6 "dednat6/zhas.lua" "shortoperators") -- (jopp 17 "polynomial-J-ops") -- (joa "polynomial-J-ops")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() = mpnewJ({}, "1234RR321", "P -> z:Or(P, v'12')") = mpnewJ({}, "1234RR321", "P -> z:Imp(v'12', P)") mp = mpnewJ({}, "1234RR321", "P -> z:Imp(v'12', P)") = mp.zha:getcuts(mp.J) shortoperators() = mpnewJ({}, "123454321", Cloq(v"22")):zhaPs("22") = mpnewJ({}, "1234567654321", Opnq(v"23")) :zhaPs("23") = mpnewJ({}, "1234567654321", Cloq(v"23")) :zhaPs("23") = mpnewJ({}, "1234567654321", Booq(v"23")) :zhaPs("23") = mpnewJ({}, "1234567654321", Forq(v"42", v"24")):zhaPs("42 24") = mpnewJ({}, "1234567654321", Jand(Booq(v"21"), Booq(v"12")) ):zhaPs("21 12") = mpnewJ({}, "1234567654321", Mixq (v"33")) :zhaPs("33") = mpnewJ({}, "1234567654321", Mixq2(v"33")) :zhaPs("33") = mpnewJ({}, "1234567654321", Truq()) :zhaPs("") = mpnewJ({}, "1234567654321", Falq()) :zhaPs("") «LPicture» (to ".LPicture") 6. LPicture =========== -- See: -- (find-dednat6 "dednat6/picture.lua" "LPicture") -- (find-dednat6 "dednat6/picture.lua" "LPicture" "__tostring =") -- (find-dednat6 "dednat6/picture.lua" "LPicture" "tolatex =") -- (find-dednat6 "dednat6/picture.lua" "makepicture-tests") -- (find-dednat6 "dednat6/picture.lua" "copyopts") -- (find-dednat6 "dednat6/picture.lua" "copyopts-tests")  (eepitch-lua51)  (eepitch-kill)  (eepitch-lua51) loaddednat6() lp = LPicture.new {scale="8pt"} lp = LPicture.new {cellfont="\\scriptsize"} lp = LPicture.new {} for l=0,1 do for r=0,1 do local pos=lr(l, r) lp:put(pos, pos:lr()) end end = lp lp.scale = "8pt" lp.cellfont = "\\scriptsize" lp.def = "FOO" = lp PPV(lp) «AsciiRect» (to ".AsciiRect") 7. AsciiRect ============ -- (find-dednat6 "dednat6/luarects.lua") -- (find-dednat6 "dednat6/luarects.lua" "AsciiRect") -- (find-dednat6 "dednat6/luarects.lua" "LuaWithRects") -- (find-dednat6 "dednat6/heads6.lua" "luarect-head") -- (ph1p 12 "prop-calc-ZHA") -- (ph1 "prop-calc-ZHA") -- (ph1 "prop-calc-ZHA" "%R") -- Local Variables: -- coding: utf-8-unix -- modes: (fundamental-mode lua-mode) -- End: