[IF not(DN4) [INCLUDE TH/speedbar.blogme]] [# (defun c () (interactive) (find-blogme3-sh0-if "dednat4")) ;; http://angg.twu.net/dednat4.html ;; file:///home/edrx/TH/L/dednat4.html #] [lua: load_TARGETS() loada2html() ] [lua: L = R; LR = R -- (find-blogmefile "blogme2-outer.lua") -- (find-blogmefile "blogme2-outer.lua" "add_entities =") -- entities[""] = "*" -- entities_chars = entities_chars.."" -- entities_re = "(["..entities_chars.."])" -- print(Q("abc")) def [[ QQ 1Q body TT(Q(body)) ]] -- def [[ QQQ 1Q body PRE(Q(two_d_trim(body))) ]] -- def [[ QQQBOX 1 body -- _G["BORDERLESSBOX+"](STYLE("background: #fff7e7;"), body) ]] -- def [[ QQQ 1Q body QQQBOX(PRE(Q(two_d_trim(body)))) ]] -- def [[ INDEXIMG 2 url,alt "\"$alt\"\n" ]] -- html_favicon = -- "\n" -- def [[ html_head 1 title -- HEAD(TITLE(title)..html_meta..html_favicon..html_style) ]] def [[ STANDOUT 1 text "$text" ]] ] [SETFAVICON dednat4/dednat4-icon.png] [SETHEADSTYLE .red { color: red; } ] [# ------------------------------------------------------------------ #] [htmlize [J Dednat4 - a TeX preprocessor to typeset trees and diagrams] [# # «.quick-start» (to "quick-start") # «.heads» (to "heads") # «.trees» (to "trees") # «.words» (to "words") # «.trees_and_abbrevs» (to "trees_and_abbrevs") # «.2Da» (to "2Da") # «.grid» (to "grid") # «.arrows» (to "arrows") # «.2Db» (to "2Db") # «.diagram-bcc» (to "diagram-bcc") # «.install» (to "install") # «.help_needed» (to "help_needed") #] [WITHINDEX [# HLIST2 [J Quick index:] [HREF #quick-start News, and a "quick start guide"] [HREF #heads How it works: heads] [HREF #trees A first example] [HREF #words Words] [HREF #trees_and_abbrevs Everything about "%:" lines (and abbreviations)] [HREF #2Da Second example: categorical diagrams] [HREF #grid The 2D grid] [HREF #arrows Building arrows] [HREF #2Db More tricks for 2D diagrams] [HREF #2Db install Installing dednat4 and running the demos] [HREF #help_needed Help needed (mainly on xypic features that I don't understand)] [J The images below are also links.] ] [P The images below are also links.] [P [HREF #trees [IMG IMAGES/Atimes-dnt.png deduction tree]] [HREF #2Da [IMG IMAGES/TfromFtoG.png simple 2D diagram]] [HREF #2Db [IMG IMAGES/lccc-frob.png complex 2D diagram]]] [_TARGETS dednat4/ -> (find-dn4 "") dednat4.tgz -> (find-dn4file "dednat4.tgz") Makefile#help -> (find-dn4 "Makefile" "help") help -> (find-dn4 "Makefile" "help") eedemo1.tex -> (find-dn4ex "eedemo1.tex") eedemo2.tex -> (find-dn4ex "eedemo2.tex") demo1.dnt -> (find-dn4ex "demo1.dnt") demo1.pdf -> (find-dn4exfile "demo1.pdf") demo2.dnt -> (find-dn4ex "demo2.dnt") demo2.pdf -> (find-dn4exfile "demo2.pdf") edrxmain41a.tex -> (find-dn4 "examples/edrxmain41a.tex") eedemo1.tex -> (find-dn4 "examples/eedemo1.tex") eedemo2.tex -> (find-dn4 "examples/eedemo2.tex") build-log -> (find-TH "dednat4-log") ] [# (find-dn4sh ".files.sh tarballfiles") #] [_TARGETS VERSION -> (find-dn4file "VERSION") TODO -> (find-dn4 "TODO") README -> (find-dn4 "README") README.ee -> (find-dn4 "README.ee") README.interact -> (find-dn4 "README.interact") README.phantoms -> (find-dn4 "README.phantoms") README.windows -> (find-dn4 "README.windows") .files.sh -> (find-dn4 ".files.sh") dednat4.el -> (find-dn4 "dednat4.el") Makefile -> (find-dn4 "Makefile") dednat4.lua -> (find-dn4 "dednat4.lua") edrxlib.lua -> (find-dn4 "edrxlib.lua") experimental.lua -> (find-dn4 "experimental.lua") examples/ -> (find-dn4 "examples/") examples/edrx08.sty -> (find-dn4 "examples/edrx08.sty") examples/edrxdnt.tex -> (find-dn4 "examples/edrxdnt.tex") examples/edrxdefs.tex -> (find-dn4 "examples/edrxdefs.tex") examples/edrxheadfoot.tex -> (find-dn4 "examples/edrxheadfoot.tex") examples/edrxmain41.tex -> (find-dn4 "examples/edrxmain41.tex") examples/edrxmain41a.tex -> (find-dn4 "examples/edrxmain41a.tex") examples/eedemo1.tex -> (find-dn4 "examples/eedemo1.tex") examples/eedemo2.tex -> (find-dn4 "examples/eedemo2.tex") ] [RULE ----------------------------------------] [sec «quick-start» (to ".quick-start") H1 News, and a "quick start guide"] [P [STANDOUT 2008jul12]: Hey! The rest of these docs are somewhat outdated - I just rewrote the [_ Makefile], simplified the build process a lot, and added new READMEs and examples...] [P Running dednat4 should be almost trivial now - just unpack [_ dednat4.tgz] somewhere, and run "make" there a first time without any parameters to get some [_ help]; then run "make demo2" (or "make LUAOS=macosx demo2" on MacOSX). The makefile will download Lua, build it in a subdirectory, download a few TeX files, and generate files "[__ demo2.dnt demos/demo2.dnt]" and "[__ demo2.pdf demos/demo2.dvi]" from [_ eedemo2.tex]. [__ build-log Here is a typical build log].] [# (find-dn4sh "make") [_ README.phantoms], [_ README.ee], [_ README.interact], and [_ README.windows] -, and at the [__ dednat4/ source code directory] #] [P So (the "make dednat4" line is optional - "dednat4" is a subtarget of "demo2"):] [PREBOXBLOGME mkdir /tmp/dn4/ cd /tmp/dn4/ wget [R http://angg.twu.net/dednat4/dednat4.tgz] tar -xvzf dednat4.tgz make ;# Print a [_ help] message make dednat4 ;# Download Lua and some TeX files, compile everything # (on MacOSX, use "make LUAOS=macosx dednat4" instead). make demo2 ;# Copy [_ edrxmain41a.tex] and [_ eedemo2.tex] to # demos/{tmp.tex,ee.tex}, # run "dednat4 tmp.tex" to generate a [__ demo2.dnt dnt file], # run "latex tmp.tex" to generate a [__ demo2.pdf dvi file]. xdvi demos/demo2.dvi ;# Visualize the [__ demo2.pdf dvi file]. ] [P Here's what is in the tarball:] [PREBOXBLOGME [_ Makefile] does lots of things - [_ help], compilation, demos [_ .files.sh] a script used by several of the targets in the makefile [_ VERSION] the current version of the tarball [_ TODO] future features that are planned but not yet implemented [_ README] the main README - currently practically just a stub [_ README.ee] explains the tmp.tex/ee.tex trick and some eev-isms [_ README.interact] how to hack and debug dednat4, how run it interactively [_ README.phantoms] explains some tricks using phantom nodes [_ README.windows] how to install and run dednat4 on Windows (untested!) [_ dednat4.lua] the main program [_ edrxlib.lua] some basic functions - loaded by dednat4.lua [_ experimental.lua] extra features (mainly phantom nodes) [_ dednat4.el] (just a stub at this moment) [_ examples/edrxmain41.tex] becomes a "tmp.tex" and "\input"s the rest [_ examples/edrxmain41a.tex] becomes a "tmp.tex" and "\input"s the rest (alt) [_ examples/edrx08.sty] the defs and "usepackage"s that I use more often [_ examples/edrxdnt.tex] defines \diag, \ded, and friends [_ examples/edrxdefs.tex] some defs that I've been using for ages [_ examples/edrxheadfoot.tex] include the date and the \jobname in the footer [_ examples/eedemo1.tex] used by "make demo1" (to produce [__ demo1.dnt this] and [__ demo1.pdf this]) [_ examples/eedemo2.tex] used by "make demo2" (to produce [__ demo2.dnt this] and [__ demo2.pdf this]) ] [RULE ----------------------------------------] [# ------------------------------------------------------------------ #] [sec «heads» (to ".heads") H1 How it works: heads] [P (La)TeX treats lines starting with "[QQ %]" as comments, and ignores them. This means that we can put anything we want in these "[QQ %]" lines - even code to be processed by other programs besides TeX.] [P Dednat4 is a Lua script that reads TeX files and pays attention only to the lines that begin with some special sequences of characters (called "heads"), all starting with "[QQ %]":] [TABLE+ border=1 [TR [TH Head] [TH interpreted as]] [TR [TD [QQ %L]] [TD Lua code]] [TR [TD [QQ %:]] [TD definitions of abbreviations]] [TR [TD [QQ %:]] [TD derivation trees (two-dimensional)]] [TR [TD [QQ %D]] [TD definitions or diagrams (in a stack language)]] ] [P (Note: all the red stars ("[QQ ]"s) in this document are in fact "\^O"s; see [AL eev-current/eev-glyphs.el eev-glyphs.el].)] [P Dednat4 processes a TeX file, say, foo.tex, and produces an auxiliary TeX file, foo.dnt, containing the TeX code to typeset the derivation trees and diagrams of foo.tex.] [# ----------------------------------------------------------------------] [sec «trees» (to ".trees") H1 A first example] [P if foo.tex contains:] [# ~/dednat4/dednat4.lua foo.tex TEXINPUTS="::$HOME/usrc/diagxy:$HOME/LATEX" latex foo.tex #] [BE' \documentclass{book} \usepackage{proof} \def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}} \def\ded#1{\csname ded-#1\endcsname} \begin{document} \input foo.dnt \def\<{\langle} \def\>{\rangle} %:|->\mapsto  %:->\to  %:\\\lambda  %::{:} %: %: [a,b]^1 [d:A×B]^1 %: ------- --------- %: [a,b]^1 b b|->c [d:A×B]^1 \pi_2d:B f:B->C %: ------- ----------- --------- ------------------- %: a c a:A f(\pi_2b):C %: -------------- ----------------------- %: a,c \:A×C %: ---------1 --------------------------------1 %: a,b|->a,c \\d:A×B.\:A×B->A×C %: %: ^Atimes-DNC-notation ^Atimes-conventional %: $$\ded{Atimes-DNC-notation} \qquad \ded{Atimes-conventional}$$ \end{document} ] [P then running "[QQ dednat4.lua foo.tex]" and then "[QQ latex foo.tex]" will produce this,] [P [IMG IMAGES/Atimes.png]] [P because "[QQ dednat4.lua foo.tex]" creates a a file foo.dnt containing this:] [BE' \defded{Atimes-DNC-notation}{ % (find-fline "foo.tex" 27) \infer[{1}]{ \mathstrut a,b\mapsto a,c }{ \infer{ \mathstrut a,c }{ \infer{ \mathstrut a }{ \mathstrut [a,b]^1 } & \infer{ \mathstrut c }{ \infer{ \mathstrut b }{ \mathstrut [a,b]^1 } & \mathstrut b\mapsto c } } } } \defded{Atimes-conventional}{ % (find-fline "foo.tex" 27) \infer[{1}]{ \mathstrut \lambda d{:}A×B.\{:}A×B\to A×C }{ \infer{ \mathstrut \{:}A×C }{ \infer{ \mathstrut a{:}A }{ \mathstrut [d{:}A×B]^1 } & \infer{ \mathstrut f(\pi_2b){:}C }{ \infer{ \mathstrut \pi_2d{:}B }{ \mathstrut [d{:}A×B]^1 } & \mathstrut f{:}B\to C } } } } ] [P "[QQ \usepackage{proof}]" loads Makoto Tatsuta's [LR http://www.ctan.org/tex-archive/macros/latex/contrib/proof/ proof.sty] package, which defines [QQ \infer]. Dednat4's [AL dednat4/dednat4.lua#tree-out routines for tree output] also support Paul Taylor's "[LR http://www.cs.man.ac.uk/~pt/proofs/index.html proofs]" package, and inserting a line like] [BE' %L tex_tree_function = tex_tree_paultaylor ] [P in foo.tex anywhere before the] [BE' %: ^Atimes-DNC-notation ^Atimes-conventional ] [P line would make dednat4.lua spit out code for Paul Taylor's package instead.] [# ------------------------------------------------------------] [sec «words» (to ".words") H2 Words] [P A [IT word] in dednat4's terminology (and in Forth terminology) is a sequence of non-whitespace characters, delimited by whitespace; the only characters that dednat4 considers as whitespace are " ", TAB, NL and CR (chars 32, 9, 10 and 13 respectively). The characters in the head of a line are removed before splitting it into words.] [# ------------------------------------------------------------] [sec «trees_and_abbrevs» (to ".trees_and_abbrevs") H2 Everything about "[QQ %:]" lines (and abbreviations)] [P The "[QQ %:]" lines -- and also the "[QQ %D]" lines, that we will describe soon -- are processed word by word. As heads don't count to form words, the line] [BE' %: ^Atimes-DNC-notation ^Atimes-conventional ] [P has two words, "[QQ ^Atimes-DNC-notation]" and "[QQ ^Atimes-conventional]". In "[QQ %:]" lines only the words that start with "[QQ ^]" are "active": "[QQ ^Atimes-conventional]" means "process the deduction tree whose root node is two lines above the "[QQ ^]" and output a block of TeX code of the form [QQ \defded{Atimes-conventional}{...}] -- a definition for a deduction called [QQ Atimes-conventional]; the definition is invoked with [QQ \ded{Atimes-conventional}].] [P Deduction trees are made of "nodes" and "bars". Both nodes and bars are words. The TeX code for a node is obtained by expanding all the abbreviations in the word (the functions that do that are [AL dednat4/dednat4.lua#abbrevs here]). Note that the expansion of an abbreviation can contain spaces -- for example:] [BE' %:|->\mapsto ] [P Bars are always words that start with either a sequence of one or more "-"s, [IT or] a sequence of one or more "="s (for double bars). The "rest" of the word of a bar, when it exists, has its abbreviations expanded and the resulting TeX code is typeset at the right of the bar.] [P A node can either have a bar above it or have nothing above it; a bar can have any number of nodes above it. Here "above" means "immediately above", and two words are only considered to be one above the other when their horizontal ranges have at least one character in common. In the example below the node "[QQ notabove]" is not considered to be above the bar.] [BE' %: abovethebar alsoabove notabove %: ===stuffattheright %: belowthebar ] [RULE ------------------------------------------------------------------] [sec «2Da» (to ".2Da") H1 Second Example: Categorical Diagrams] [P The part of the source file that starts at [AL dednat4/dednat4.lua#diag-out this point] implements the support for "[QQ %D]" lines. This part of dednat4 is a front-end for Michael Barr's [AL eev-current/examples/tex.e#diagxy diagxy] package, which in its turn is a front-end for [LR http://www.ctan.org/tex-archive/macros/generic/diagrams/xypic/ XYpic].] [P "[QQ %D]" lines are processed one by one, and each word in them (except the head) is parsed (the code for the parser starts [AL dednat4/dednat4.lua#diag-forth-parser here]) and then is executed. And there is a trick: some words advance the input pointer during their execution, and process the text between the old "pos" and the new "pos" in their own ways; usually they either read some words or read everything up to the end of the line.] [P Here is our first example of code with "[QQ %D]" lines. Suppose that the file foo2.tex contains this:] [# ~/dednat4/dednat4.lua foo2.tex TEXINPUTS="::$HOME/usrc/diagxy" latex foo2.tex #] [BE' \documentclass{book} \input diagxy \def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{#2}} \def\diag#1{\bfig\csname diag-#1\endcsname\efig} \begin{document} \input foo2.dnt %D diagram T:F->G %D 2Dx 100 +20 +20 %D 2D 100 A %D 2D / - \ %D 2D / | \ %D 2D v v v %D 2D +25 FA ------> GA %D 2D TA %L PP(nodes) -- Lua code: dump the table `nodes' %D (( A FA -> A GA -> %L PP(ds) -- Lua code: dump the table `ds' %D FA GA -> .plabel= b TA %D A FA GA midpoint |-> %D )) %D enddiagram $$\diag{T:F->G}$$ \end{document} ] [P The first word parsed is "[QQ diagram]". When it is executed it reads the next word, "[QQ T:F->G]", sets the name of the current diagram to that, clears the tables that hold the catalog of known nodes and arrows, and does a few other things; its code is [AL dednat4/dednat4.lua#diag-words here] and [AL dednat4/dednat4.lua#diagram here].] [sec «grid» (to ".grid") H3 The 2D grid] [P Both "[QQ 2Dx]" and "[QQ 2D]" are words that parse everything to the end of the line and treat what they read in their own ways - as a grid with coordinates and nodes. Only columns that are below the first character of a number in the "[QQ 2Dx]" line have a horizontal coordinate; only lines that start with a number have a vertical coordinate (these "numbers" can start with "+", that means "the previous value plus this"). In the grid in foo2.tex only these six positions, marked as `a', `b', `c', `d', `e', and `f' below, have both a horizontal and a vertical coordinates; `e' has coordinates (140, 125).] [BE' %D 2Dx 100 +20 +20 %D 2D 100 a b c %D 2D %D 2D %D 2D %D 2D +25 c d e %D 2D ] [P Some words in the grid in foo2.tex -- namely, "[QQ A]", "[QQ FA]", "[QQ ------>]", and "[QQ GA]", are over positions with both coordinates; those words become names of nodes with those coordinates. Most of the things that we drew on the grid are just "decorations" that are ignored by "[QQ 2D]"; they are there just to make the ASCII diagram look like a textual representation of the real diagram. Note that the "[QQ ------>]", that in a sense is just a decoration, is [IT not] ignored -- it becomes a node, but as unused nodes don't show on the picture and don't generate TeX code, [IT we] can ignore it.] [P After the grid in foo2.tex there's a Lua line with a command to dump the array of nodes; the source for PP is [AL dednat4/edrxlib.lua#PP here], and the result (that is printed to stdout) is this, modulo whitespace:] [BE' {1={"noden"=1, "tag"="A", "x"=120, "y"=100}, 2={"noden"=2, "tag"="FA", "x"=100, "y"=125}, 3={"noden"=3, "tag"="------>", "x"=120, "y"=125}, 4={"noden"=4, "tag"="GA", "x"=140, "y"=125}, "------>"={"noden"=3, "tag"="------>", "x"=120, "y"=125}, "A"={"noden"=1, "tag"="A", "x"=120, "y"=100}, "FA"={"noden"=2, "tag"="FA", "x"=100, "y"=125}, "GA"={"noden"=4, "tag"="GA", "x"=140, "y"=125} } ] [P Note that entries in that table can be accessed either by a numeric id (the "noden") or by the name of the node ("tag"); some of the subtables are shared -- [QQ nodes[1] = nodes["A"]] -- but the output of PP doesn't make that explicit.] [P There's also a table called "[QQ arrows]", but at this point it is empty.] [sec «arrows» (to ".arrows") H3 Building arrows] [P After that comes this code:] [BE' %D (( A FA -> A GA -> %L PP(ds) -- Lua code: dump the table `ds' %D FA GA -> .plabel= b TA %D A FA GA midpoint |-> %D )) ] [P Dednat4 has a data stack ("[QQ ds]"; we will see a dump of it soon), like Forth; it doesn't have a "return stack" like the one in Forth, as we don't need subroutines in the obvious sense of the term, at least not in the kernel; it's easy to define new words in Lua, and usually that's enough.] [P "[QQ ((]" puts a value in an auxiliary stack, called "[QQ depths]", to remember how deep is the data stack at that point; in the next lines we will put many new objects in the data stack, and the "[QQ ))]" will get rid of all these new objects: it will drop everything above the stored depth. "[QQ ((]" and "[QQ ))]" help keeping the data stack tidy.] [P "[QQ A]" and "[QQ FA]" put two nodes on the data stack; "[QQ ->]" (the words for arrows are defined [AL dednat4/dednat4.lua#diag-arrows here]) creates a new arrow, going from "[QQ A]" to "[QQ FA]", and puts it both on the data stack (after "[QQ A]" and "[QQ FA]") and on the list of arrows; the main thing that "[QQ enddiagram]" does is to output TeX code for all the defined arrows, i.e., to draw them. This can only be done at the end, because some words modify attributes of arrows: the code "[QQ .plabel= b TA]", a few lines after that, adds a "label" and a "position" to the arrow at the top of the stack: the text of the label is "TA", and it is to be TeXed below the arrow.] [P When "[QQ PP(ds)]" (in Lua) dumps the data stack what we see is this, modulo whitespace:] [BE' {1={"arrown"=2, "from"=1, "shape"="->", "to"=4}, 2={"noden"=4, "tag"="GA", "x"=140, "y"=125}, 3={"noden"=1, "tag"="A", "x"=120, "y"=100}, 4={"arrown"=1, "from"=1, "shape"="->", "to"=2}, 5={"noden"=2, "tag"="FA", "x"=100, "y"=125}, 6={"noden"=1, "tag"="A", "x"=120, "y"=100} } ] [P A full description of the "node" and "arrow" structures can be found [AL dednat4/dednat4.lua#diag-out here]; arrows have many optional fields. Note that the top of the stack is [QQ ds[1]].] [P The only other new thing in this diagram is "[QQ midpoint]". It is defined [AL dednat4/experimental.lua here], and it takes the two nodes at the top of the stack and replaces them (on the stack only!) by a new node, lying halfway between them.] [P We have already described "[Q ))]"; in this case it makes the depth of ds go back to zero. After it "[QQ enddiagram]" appends this to foo2.dnt,] [BE' \defdiag{T:F->G}{ % (find-fline "foo2.tex" 9) \morphism(300,0)/->/<-300,-375>[{A}`{FA};{}] \morphism(300,0)/->/<300,-375>[{A}`{GA};{}] \morphism(0,-375)|b|/->/<600,0>[{FA}`{GA};{TA}] \morphism(300,0)/|->/<0,-375>[{A}`{\phantom{O}};{}] } ] [P And TeX typesets it into this:] [P [IMG IMAGES/TfromFtoG.png]] [RULE ------------------------------------------------------------] [sec «2Db» (to ".2Db") H1 More tricks for 2D diagrams] [P (Describe "@", how to have several nodes with the same TeX text, other "shapes" of floating arrows ([QQ =>], for example), "place" and the pullback symbol; discuss the source code of the BCC diagram below; discuss the extensions in [HREF dednat4/experimental.lua.html experimental.lua])] [sec «diagram-bcc» (to ".diagram-bcc") H1 A bigger diagram] [P The diagram below - the Beck-Chevalley condition in a certain notation -] [P [IMG IMAGES/lccc-bcc.png]] [P was produced by this code:] [BE' %D diagram LCCC-BCC %D 2Dx 100 +30 +25 +30 %D 2D 100 {}d ===============> c,d{} %D 2D - /\ - ^ %D 2D | \\ |-> | |\BCC %D 2D v \\ v - %D 2D +20 {}c,d <=\\=========== c,d{}{} %D 2D /\ \\ /\ %D 2D +10 \\ d ===============> c,d{{}} %D 2D \\ - \\ - %D 2D \\ | <-| \\ |\id %D 2D \\ v \\ v %D 2D +20 c,d <============== c,d{{}}{} %D 2D %D 2D +10 a,b,c |----------> a,b %D 2D - _| - %D 2D \ \ %D 2D v v %D 2D +35 a,c |--------------> a %D 2D %D (( {}d c,d{} # 0 1 %D {}c,d c,d{}{} # 2 3 %D d c,d{{}} # 4 5 %D c,d c,d{{}}{} # 6 7 %D @ 0 @ 1 => %D @ 0 @ 2 |-> @ 1 @ 3 |-> sl_ .plabel= l \natural %D @ 1 @ 3 <-| sl^ .plabel= r \mathrm{BCC} %D @ 0 @ 3 harrownodes nil 20 nil |-> %D @ 2 @ 3 <= %D @ 0 @ 4 <= @ 2 @ 6 <= @ 3 @ 7 <= %D @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 14 nil <-| %D @ 4 @ 5 => @ 4 @ 6 |-> @ 5 @ 7 |-> .plabel= r \mathrm{id} %D @ 4 @ 7 harrownodes nil 20 nil <-| %D @ 6 @ 7 <= %D )) %D (( a,b,c a,b %D a,c a %D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |-> %D @ 0 relplace 15 7 \pbsymbol{7} %D )) ] [RULE ------------------------------------------------------------] [sec «install» (to ".install") H2 Installing dednat4 and running the demos] [sec «help_needed» (to ".help_needed") H2 Help needed (mainly on xypic features that I don't understand)] [RULE ------------------------------------------------------------] [P Old stuff / to do: the a stack-based language inspired by Forth (mainly by the idea that words are allowed to interfere on the parsing), and built around [L [-> miniforth] miniforth]; explain "@"; explain other advanced/experimental words like harrownodes; apologize for the current ugliness (among other things, I'm very bad at naming functions) and encourage questions and all kinds of feedback; describe the demos and how the default [QQ \ded] and [QQ \diag] are a bit smarter than the ones in the examples - they complain on undefined deductions/diagrams...] [# (find-dn4file "") #] [RULE ------------------------------------------------------------------] [NAME dednat4] [H1 Typesetting categorical diagrams in LaTeX] [P (This section was just copied from my [R [--> (find-TH "math-b" "dednat4") ] math page]...)] [P My PhD thesis included lots of hairy categorical diagrams, and I ended up writing a [R dednat4/ LaTeX preprocessor] in Lua to help me typeset them. Currently (March 2005) I'm trying to pack that preprocessor and document it; its [R dednat4/README.html README] is still horribly incomplete. The source code for the examples below is [R dednat4/eqfibs.metatex.html here].] [lua: def [[ TABLE 1 text "$text\n
\n" ]] def [[ TR 1 text "$text\n\n" ]] def [[ TD 1 text "$text\n\n" ]] def [[ TDcolspan 2 n,text "$text\n\n" ]] def [[ DIAGTEXT 1 text BR()..COLOR("red",text) ]] def [[ DIAGTEXT 1 text "
\n" ..text.."\n
\n" ]] ] [TABLE [TR [TDcolspan 3 [IMG IMAGES/preslim.png] [DIAGTEXT if a functor R has a left adjont [BR] then it preserves limits] ] ] [TR [TD [IMG IMAGES/lccc-bcc.png] [DIAGTEXT The Beck-Chevalley map [BR] in an LCCC] ] [TD [IMG IMAGES/lccc-frob.png] [DIAGTEXT The Frobenius map [BR] in an LCCC] ] [TD [IMG IMAGES/eqfib-trans.png] [DIAGTEXT Proving transitivity [BR] in an EqFibration [BR] (slightly wrong)] ] ] ] ] ] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]