Warning: this is an htmlized version!
The original is across this link,
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: