|
Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |
#######
#
# E-scripts on programs to typeset deduction trees.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/dednat.e>
# or at <http://angg.twu.net/e/dednat.e.html>.
# See also <http://angg.twu.net/emacs.html>,
# <http://angg.twu.net/.emacs[.html]>,
# <http://angg.twu.net/.zshrc[.html]>,
# <http://angg.twu.net/escripts.html>,
# and <http://angg.twu.net/>.
#
#######
# «.dednat.lua» (to "dednat.lua")
# «.dednat.icn» (to "dednat.icn")
# «.dednat4-tgz-tests» (to "dednat4-tgz-tests")
# «.thereplusxy» (to "thereplusxy")
# «.splitdist» (to "splitdist")
# «.phantom-nodes» (to "phantom-nodes")
# «.tex-src-tgz» (to "tex-src-tgz")
# «.eepitch-dednat4» (to "eepitch-dednat4")
# «.dednat4-test» (to "dednat4-test")
# «.dednat41-test» (to "dednat41-test")
# «.dednat4-demo1» (to "dednat4-demo1")
# «.dednat41-demo1» (to "dednat41-demo1")
# «.tgz:make-demo1» (to "tgz:make-demo1")
# «.visible-phantoms» (to "visible-phantoms")
# «.dednat4.el» (to "dednat4.el")
# «.symlinks» (to "symlinks")
# «.dednat4-log» (to "dednat4-log")
# «.2008filterp-texsrc» (to "2008filterp-texsrc")
# «.lpeg» (to "lpeg")
# «.bitlib» (to "bitlib")
# «.loop» (to "loop")
# «.ticked-arrowheads» (to "ticked-arrowheads")
# «.enddefdiag» (to "enddefdiag")
#####
#
# dednat.lua (obsolete)
# 2001may15
#
#####
# «dednat.lua» (to ".dednat.lua")
# (find-angg "LUA/dednat.lua")
# (find-angg "LATEX/Makefile")
# (find-angg "LATEX/Makefile" "dednat.lua")
# (find-angg "LATEX/Makefile" "dn_to_dnt")
#*
# (find-angg "LATEX/tese2.sty")
# (find-angg "LATEX/proof.edrx.sty")
cd ~/LATEX/
rm -v tmp.dn tmp.dnt
cat > tmp.tex <<'%%%'
% \input tese2.sty
\documentclass{book}
\usepackage{proof.edrx}
\def\ded#1{\csname ded-#1\endcsname}
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\input tmp.dnt
\begin{document}
%
%:*->*\to *
%:
%: a [a->b]^1
%: -----------
%: b
%: ---------1
%: (a->b)->b
%:
%: ^dedtest
%:
$$\ded{dedtest}$$
%
\end{document}
%%%
make tmp.dvi
rexdvi tmp.dvi
#*
#####
#
# dednat.icn (obsolete)
# 2001may15
#
#####
# «dednat.icn» (to ".dednat.icn")
# (find-angg "LATEX/dednat.icn")
#####
#
# dednat4: tgz and tests
# 2008may26
#
#####
# «dednat4-tgz-tests» (to ".dednat4-tgz-tests")
# (find-es "xypic")
# (find-es "xypic" "dednat41-test")
# (find-es "xypic" "dednat41-demo1")
# (find-es "xypic" "eepitch-dednat4")
# (find-angg ".emacs" "eepitch-dednat4")
# (find-angg ".emacs" "dednat4")
# (find-angg ".emacs" "eedn4a")
# (find-dn4 "")
# (find-dn4 "Makefile")
# The README is crap:
# (find-dn4file "README")
# This is ok - copy to the dednat4/ dir:
# (find-THLw3m "dednat4.html")
# (find-TH "dednat4")
# (find-sh "grep IMG ~/TH/dednat4.blogme")
# It needs a hacker's guide, though... get logs from:
# (find-es "xypic" "eepitch-dednat4")
# Add: at: x y tag
# .xy+= x y
# there+: x y tag
# (find-anggfile "IMAGES/Atimes-dnt.png")
# (find-anggfile "IMAGES/Atimes.png")
# (find-anggfile "IMAGES/TfromFtoG.png")
# (find-anggfile "IMAGES/eqfib-trans.png")
# (find-anggfile "IMAGES/lccc-bcc.png")
# (find-anggfile "IMAGES/lccc-frob.png")
# (find-anggfile "IMAGES/preslim.png")
# (find-zsh "
cd ~/IMAGES/
A=(
Atimes-dnt.png
Atimes.png
TfromFtoG.png
eqfib-trans.png
lccc-bcc.png
lccc-frob.png
preslim.png
)
laf $A
")
#####
#
# there+xy:
# 2008jun01
#
#####
# «thereplusxy» (to ".thereplusxy")
# (find-LATEXfile "2008sheaves.tex" "thereplusxy =")
#####
#
# understand harrownodes and varrownodes
# 2008jun02
#
#####
# «splitdist» (to ".splitdist")
# (find-dn4 "dednat41.lua")
# (find-dn4 "experimental.lua")
Suppose that we want to draw a diagram like this one:
A |-----> FA
| -
| |-> |
v v
B |-----> FB
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
require "experimental"
= splitdist(100, 200, nil, 20, nil)
--> 140 160
#####
#
# Documentation about phantom nodes
# 2008jun24
#
#####
# «phantom-nodes» (to ".phantom-nodes")
# Moved to: (find-dn4 "README.phantoms")
#####
#
# LaTeX source tarballs for my .texs
# 2008jun08
#
#####
# «tex-src-tgz» (to ".tex-src-tgz")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/te/
mkdir /tmp/te/
cd /tmp/te/
# (find-fline "~/LATEX/2008bcc.tex")
F=$HOME/LATEX/2008bcc.tex
cp -av $F .
cp -av ~/dednat4/examples/edrx08.sty .
cp -av ~/dednat4/examples/edrxdnt.tex .
cp -av ~/dednat4/examples/edrxdefs.tex .
cp -av ~/dednat4/examples/edrxheadfoot.tex .
~/dednat4/dednat41 $(basename $F)
cp -av $S/http/www.ctan.org/tex-archive/macros/latex/contrib/lkproof/proof.sty .
unzip -o $S/ftp/ftp.math.mcgill.ca/pub/barr/diagxy.zip diagxy.tex
latex $(basename $F)
# (find-fline "/tmp/te/")
# (find-dn4exfile "")
# (find-dn4file "Makefile")
# (find-dn4file "Makefile" "TATPROOFSFILE =")
# (find-dn4file "Makefile" "DIAGXYFILE")
# Add this?
# (find-dn4file "dednat41.lua")
# Generated by dednat41.lua
#####
#
# eepitch-dednat4
# 2008may11
#
#####
# «eepitch-dednat4» (to ".eepitch-dednat4")
# (find-angg ".emacs" "eepitch-dednat4")
# (find-angg "LUA/lua50init.lua" "load_dednat4")
# (find-dn4 "dednat41.lua")
# (find-dn4 "dednat41.lua" "tree-lib" "dolinenumbers")
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
PP(abbrevs)
process "/home/edrx/dednat4/examples/edrx08.sty"
PP(abbrevs)
PP(heads)
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
dolinenumbers = nil
diagram "miniadj"
dxy2Dx " 100 140 "
dxy2D " 140 a^L <= a "
dxy2D " - - "
dxy2D " | | "
dxy2D " v v "
dxy2D " 100 b => b^R "
PP("nodes =", nodes)
pushtag "a^L"; pushtag "a"; dof "<="
pushtag "a^L"; pushtag "b"; dof "|->"
pushtag "a"; pushtag "b^R"; dof "|->"
pushtag "b"; pushtag "b^R"; dof "=>"
PP("arrows =", arrows)
enddiagram()
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
dolinenumbers = nil
mytostringk = mytostringk2
dofs "diagram miniadj2"
dofs "2Dx 100 140 "
dofs "2D 140 a^L <= a "
dofs "2D - - "
dofs "2D | | "
dofs "2D v v "
dofs "2D 100 b => b^R "
dofs "(( a^L a <= a^L b |-> a b^R |->"
printf("xs = %s\n", mytostring(xs))
for i=1,#nodes do printf("nodes[%d] = %s\n", i, mytostring(nodes[i])) end
for i=1,#arrows do printf("arrows[%d] = %s\n", i, mytostring(arrows[i])) end
for i=1,#ds do printf("ds[%d] = %s\n", i, mytostring(ds[i])) end
for i=1,#depths do printf("depths[%d] = %s\n", i, mytostring(depths[i])) end
PP(keys(nodes))
dofs " b b^R => ))"
dofs "enddiagram"
Note: due to a bad design decision the elements of ds are "in the
wrong order" - to push a new element we move the old elements from the
positions 1..n to 2..n+1, and then we set ds[1] to the new element...
this simplifies accessing the elements at the top of the stack, but
complicates all the rest - especially "@" and operations with the
array "depths".
One possible fix (dirty trick): use a metatable with a "__call" entry
for the table "ds"; make ds(2) return ds[-2] for any value of 2.
Notes (obsolete):
%L at = function (index) return ds[#ds - depths[1] - index] end
%L PP("@ 0 =", at(0))
%L PP("@ 1 =", at(1))
%L PP("@ 2 =", at(2))
%L PP(ds[#ds])
%L PP(ds[#ds - 1])
%L PP(#ds)
%L PP(ds)
%L mytostringk = mytostringk2
%L printf("xs = %s\n", mytostring(xs))
%L for i=1,#nodes do printf("nodes[%d] = %s\n", i, mytostring(nodes[i])) end
%L for i=1,#arrows do printf("arrows[%d] = %s\n", i, mytostring(arrows[i])) end
%L for i=1,#ds do printf("ds[%d] = %s\n", i, mytostring(ds[i])) end
%L for i=1,#depths do printf("depths[%d] = %s\n", i, mytostring(depths[i])) end
%L PP(keys(nodes))
% (find-sh "cd ~/LATEX/ && lua51 ~/dednat4/dednat41.lua tmp.tex")
% (find-angg "LUA/lua50init.lua")
#####
#
# Testing dednat41
# 2008may19
#
#####
# «dednat4-test» (to ".dednat4-test")
# «dednat41-test» (to ".dednat41-test")
# (find-dn4 "Makefile")
# (find-node "(kpathsea)File lookup")
# (find-dn4exfile "dednat4.el")
# (find-eevtmpfile "")
# (find-eevtmpfile "ee.sh")
# (find-LATEXfile "" "tmp.tex")
# (find-LATEXfile "tmp.tex")
# (find-LATEXfile "ee.tex")
# (find-angg ".emacs")
# (find-angg ".emacs" "dednat4")
# (find-es "xypic" "eepitch-dednat4")
# (find-angg ".emacs" "eedn4a")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/dntest/
mkdir /tmp/dntest/
cd /tmp/dntest/
cd ~/dednat4/
make S=$S TEXDIR=/tmp/dntest texfiles
cd /tmp/dntest/
DN4EXDIR=$HOME/dednat4/examples/
cp -v $DN4EXDIR/edrxmain41a.tex tmp.tex
cp -v $DN4EXDIR/eedemo1.tex ee.tex
cp -v $DN4EXDIR/edrx08.sty edrx08.sty
~/dednat4/dednat41 tmp.tex
TEXINPUTS=$DN4EXDIR: latex tmp.tex
# (find-fline "/tmp/dntest/")
# (find-fline "/tmp/dntest/tmp.tex")
# (find-dvipage "/tmp/dntest/tmp.dvi")
# «dednat4-demo1» (to ".dednat4-demo1")
# «dednat41-demo1» (to ".dednat41-demo1")
# (find-dn4 "Makefile" "demo1")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/
rm -Rv demos/
mkdir demos/
make demo1
# (find-dn4 "demos/")
# (find-man "unzip")
#####
#
# dednat4: "make demo1" (from the tarball)
# 2008jun25
#
#####
# «tgz:make-demo1» (to ".tgz:make-demo1")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/dn4t/
mkdir /tmp/dn4t/
cd /tmp/dn4t/
tar -xvzf ~/dednat4/dednat4.tgz
make S=$S demo1 |& tee om
# (find-fline "/tmp/dn4t/")
#####
#
# visible phantoms
# 2008jun27
#
#####
# «visible-phantoms» (to ".visible-phantoms")
# (find-fline "~/tmp/phantom-nodes.png")
%*
% (eedn4a-bounded)
%L phantomnode = "\\myphantom{O}"
\def\myphantom{\phantom}
%D diagram harrowdemo
%D 2Dx 100 +30
%D 2D 100 A |-----> FA
%D 2D | -
%D 2D f | |-> | Ff
%D 2D v v
%D 2D +30 B |-----> FB
%D 2D
%D (( A FA |->
%D A B -> .plabel= l f
%D FA FB -> .plabel= r Ff
%D B FB |->
%D A FB harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{harrowdemo}
\qquad
{\def\myphantom{\red}
\diag{harrowdemo}
}
$$
%*
#####
#
# dednat4.el
# 2008jun27
#
#####
# «dednat4.el» (to ".dednat4.el")
# (find-dn4 "dednat4.el")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/
lua51 -e 'dofile"dednat41.lua"' -i
require "experimental"
#####
#
# symlinks: tmp.tex -> edrxmain41.tex and ee.tex -> eedemo1.tex
# 2008jun27
#
#####
# «symlinks» (to ".symlinks")
# (find-dn4file "Makefile")
# Removed from the makefile:
# Ooops - here I am symlinking tmp.tex -> edrxmain41a.tex... What
# happens if I copy something to tmp.tex later? Does it cease to be a
# symlink, or does it overwrite edrxmain41a.tex?
#
# Possible solution: do not symlink - edrxmain41a.tex has a header
# that explains from where it comes.
#demo1-old: dednat41 texfiles
# mkdir -p $(DEMODIR)
# ln -sf $(DN4EXDIR)/edrxmain41a.tex $(DEMODIR)/tmp.tex
# ln -sf $(DN4EXDIR)/edrx08.sty $(DEMODIR)/edrx08.sty
# ln -sf $(DN4EXDIR)/eedemo1.tex $(DEMODIR)/ee.tex
# cd $(DEMODIR) && $(PWD)/dednat41 tmp.tex
# cd $(DEMODIR) && TEXINPUTS=$(TEXDIR): latex tmp.tex
# cd $(DEMODIR) && ln -sf edrxmain41a.tex tmp.tex
# cd $(DEMODIR) && ln -sf eedemo1.tex ee.tex
#####
#
# dednat4-log.html
# 2008jul12
#
#####
# «dednat4-log» (to ".dednat4-log")
# (find-THgrep "grep -niH -e traffic *")
# (find-blogme3grep "grep -niH -e traffic *")
# (find-blogme3 "anggdefs.lua" "TRAFFIC")
# (find-TH "dednat4")
# (find-TH "dednat4-log")
# (find-es "blogme" "traffic-lights-glyphs")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd
rm -Rv mkdir /tmp/dn4/
cd ~/dednat4/
make tarball
mkdir /tmp/dn4/
cd /tmp/dn4/
wget http://angg.twu.net/dednat4/dednat4.tgz
tar -xvzf dednat4.tgz
make
make dednat4
make texfiles
make demo2
#####
#
# 2008filterp-texsrc.tar.gz
# 2008jul12
#
#####
# «2008filterp-texsrc» (to ".2008filterp-texsrc")
# http://angg.twu.net/math/
# (find-twusfile "")
# (find-twusfile "math/")
# (find-twusfile "LATEX/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/fi/
mkdir /tmp/fi/
cd ~/LATEX/
cp -aiv 2008filterp.{tex,dnt} filters.bib /tmp/fi/
cd /tmp/fi/
~/dednat4/.files.sh eval "{ texedrx ; texother; } | prepends"
cp -aiv $(~/dednat4/.files.sh eval "{ texedrx ; texother; } | prepends") .
rm -v edrxmain*.tex
tar -cvzf /tmp/2008filterp-texsrc.tar.gz *
laf /tmp/2008filterp-texsrc.tar.gz
laf
~/dednat4/dednat4 2008filterp.tex
latex 2008filterp.tex
bibtex 2008filterp
latex 2008filterp.tex
latex 2008filterp.tex
# (ee-cp "/tmp/2008filterp-texsrc.tar.gz" (ee-twusfile "LATEX/2008filterp-texsrc.tar.gz") 'over)
#####
#
# The "lpeg" and "bitlib" targets in the Makefile
# 2008jul21
#
#####
# «lpeg» (to ".lpeg")
# «bitlib» (to ".bitlib")
# (find-dn4 "Makefile" "lpeg")
# (find-dn4 "Makefile" "bitlib")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/ && make tmpdir
cd /tmp/dn4/
tar -xvzf /tmp/dulua.tgz
make S=$S luabuild
tar -cvzf /tmp/dulua.tgz usrc/lua-5.1.3/
make S=$S lpegbuild
make S=$S bitlibbuild
./lua51
require "lpeg"
PP(lpeg)
assert(package.loadlib("./lbitlib.so", "luaopen_bit"))()
print(bit.bxor(6,3))
os.exit()
#####
#
# \Loop
# 2008aug01
#
#####
# «loop» (to ".loop")
# (find-diagxypage 29 "\\Loop")
# (find-diagxytext "\\Loop")
# (find-dn4 "experimental.lua")
# (find-dn4 "experimental.lua" "loop")
%*
% (eedn4a-bounded)
%D diagram ??
%D 2Dx 100 +30 +30
%D 2D 100 a --> b
%D 2D v
%D 2D +20 c d
%D 2D
%D (( a b -> b c ->
%D a loop (ul,dl)_{aa}
%D b loop (u,r)
%D c loop (dl,dr)
%D d place
%D ))
%D enddiagram
%D
$$\diag{??}$$
%*
% (eedn4a-bounded)
$$\bfig
\morphism[A`B;f]
\Loop(0,0)A(ur,ul)_g
\Loop(0,0)A(ur,ul)^a
\Loop(500,0)B(dl,dr)_h
\Loop(1000,0)CC(dl,dr)
% \Loop(1500,0)DD
\efig
$$
%*
#####
#
# ticked arrowheads
# 2009feb26
#
#####
# «ticked-arrowheads» (to ".ticked-arrowheads")
from Michael Barr <barr@math.mcgill.ca>
to Categories list <categories@mta.ca>
date Wed, Feb 25, 2009 at 10:08 PM
subject categories: ticked arrowheads in xy-pic and diagxy
A month or two ago, Micah McCurdy wrote to ask me if it was possible to
make an arrow with a tick in the middle (that is ----+---->) and I said I
didn't know how to do that and suggested he ask Ross Moore. Ross told him
that xy-pic didn't have that capacity. Well, Micah discovered that it
did. Here are some samples, using diagxy, but that is just a front end to
xy-pic.
%*
% (eedn4a-bounded)
$$\bfig
\node a(0,0)[A]
\node b(300,400)[B]
\arrow/@{>}|-*@{>}/[a`b;f]
\efig$$
$$\bfig
\ptriangle/>`>`@{>}|-@{|}/[A`B`C;f`g`h]
\efig$$
$$\bfig
\morphism/@{>}|-@{+}/<700,0>[ABCDE`F;h]
\efig$$
$$\bfig
\morphism/@{>}|-*@{|}/<700,0>[ABCDE`F;h]
\efig$$
%*
As far as I can tell, the * between the - and the @ has no effect. The
one limitation is that what goes inside the -@{ } must be a \dir. This is
a limitation for me, since I cannot figure out the syntax of \newdir. For
this to work, it clearly has to be something that tex can rotate.
Michael
from Michael Barr <barr@math.mcgill.ca>
to Categories list <categories@mta.ca>
date Sat, Feb 28, 2009 at 1:55 PM
subject categories: More arrow decorations
By playing with Micah's discovery (which is actually documented on page
39, third line from the bottom of Fig. 13), I have come up with the
following potentially useful decorations:
%*
% (eedn4a-bounded)
$$\bfig \morphism/@{>}|-@{|}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{x}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{o}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{*}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{||}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{)}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{(}/<500,500>[A`B;f] \efig$$
%*
The same ideas also work in native xy-pic and, for all I know, in the
matrix version as well.
#####
#
# enddefdiag
# 2009aug11
#
#####
# «enddefdiag» (to ".enddefdiag")
# (find-dn4 "experimental.lua" "def")
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
%D diagram pmetauniv
%D 2Dx 100 +20
%D 2D 100 #1
%D 2D -
%D 2D #4|
%D 2D v
%D 2D +20 #2 ==> #3
%D 2D
%D (( #1 #3 |-> .plabel= l #4
%D #2 #3 =>
%D ))
%D enddefpdiagram 4
$$\pmetauniv abcd$$
%*
cat > ee.tex <<'%%%'
%D diagram miniadj
%D 2Dx 100 120
%D 2D 100 a^L <= a
%D 2D - -
%D 2D | |
%D 2D v v
%D 2D 120 b => b^R
%D a^L a <= a^L b |-> a b^R |-> b b^R =>
%D enddiagram
$$\diag{miniadj}$$
%:
%: [a,b]^1
%: -------
%: [a,b]^1 b b|->c
%: ------- ------------
%: a c
%: ---------------
%: a,c
%: ---------1
%: a,b|->a,c
%:
%: ^tree1
%:
$$\ded{tree1}$$
%%%
# Local Variables:
# coding: raw-text
# ee-delimiter-hash: "\n#*\n"
# ee-delimiter-percent: "\n%*\n"
# ee-anchor-format: "«%s»"
# End: