|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- 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 <eduardoochs@gmail.com>
-- 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: