Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- begriff.lua: -- This file: -- http://angg.twu.net/dednat5/begriff.lua.html -- http://angg.twu.net/dednat5/begriff.lua -- (find-dn5 "begriff.lua") -- Author: Eduardo Ochs <eduardoochs@gmail.com> -- Version: 2011may15 -- License: GPL3 -- -- *** This is a prototype!!! *** -- I am still discussing with Alessandro Bandeira Duarte - -- see his homepage, at <http://frege.hdfree.com.br/> - -- which syntax we want this to support, its interface, etc. -- If you are interested in using this please get in touch!!!! -- (find-angg "LUA/begriff.lua") -- (find-fline "/usr/share/doc/texlive-doc/latex/begriff/README") -- \BGassert - generates an assertion sign -- \BGcontent - generates an assertion sign -- \BGnot - generates a negation sign -- \BGquant{v} - generates a universal quantifier with variable v -- \BGconditional{a}{c} - generates a conditional with antecendent -- a and consequent c. Note that in the Begriffsschrift, -- the antecendent is placed below the consequent. -- -- (the following three commands were introduced in version 1.5) -- -- \BGterm{x} - creates a right-justified terminal node x -- \BGstem{x} - inserts arbitrary LaTeX maths x into a non-terminal node -- \BGbracket{x} - places the expression x inside brackets -- (find-books "__frege/__frege.el" "heijenoort") -- «.begriff_classes» (to "begriff_classes") -- «.begriff_parse» (to "begriff_parse") -- «.begriff_head» (to "begriff_head") -- «.begriff_preamble» (to "begriff_preamble") --[[ * (eepitch-lua51) * (eepitch-kill) * (eepitch-lua51) require "begriff" --]] require "eoo" -- (find-dn5 "eoo.lua") require "process" -- (find-dn5 "process.lua") -- «begriff_classes» (to ".begriff_classes") BegCond = Class { type = "BegCond", __index = { TeX = function (o, p) local pp = p.." " local a, c = o.a:TeX(pp), o.c:TeX(pp) -- return "\\BGconditional{\n".. -- pp..a.."\n".. -- p.."}{"..c.."\n".. -- p.."}" return "\\BGrevconditional{\n".. pp..c.."\n".. p.."}{"..a.."\n".. p.."}" end, }, } BegNot = Class { type = "BegNot", __index = { TeX = function (o, p) return "\\BGnot"..o[1]:TeX(p) end, }, } BegAssert = Class { type = "BegAssert", __index = { TeX = function (o, p) return "\\BGassert"..o[1]:TeX(p) end, }, } BegQuant = Class { type = "BegQuant", __index = { TeX = function (o, p) return "\\BGquant{"..o.v.."}"..o[1]:TeX(p) end, }, } BegTerm = Class { type = "BegTerm", __index = { -- TeX = function (o) return "\\BGterm "..o[1] end, TeX = function (o, p) return " "..o[1] end, }, } -- «begriff_parse» (to ".begriff_parse") beglines = {} bperror = function (x, y, msg) error(format("x=%d y=%d msg=%s", x, y, msg or "?")) end bpterm = function (x, y) local xx = beglines[y]:match("^[^ ]*()", x) while 1 do local xxx = beglines[y]:match("^ [^ ]+()", xx) if xxx then xx = xxx else break end end return beglines[y]:sub(x, xx) end -- bprest = function (x, y) return beglines[y]:sub(x) end bpstart = function (x, y) if beglines[y]:match("^|", x) then return BegAssert {bptree(x+1, y)} end return bptree(x, y) end bptree = function (x, y) local hyphs = beglines[y]:match("^-+", x) if hyphs then return bptree(x+#hyphs, y) or bperror(x, y, "hyphs") end if beglines[y]:match("^~", x) then return BegNot {bptree(x+1, y) or bperror(x+1, y, "~")} end local quant = beglines[y]:match("^%b()", x) if quant then local v = quant:sub(2, -2) return BegQuant {v=v, bptree(x+#quant, y) or bperror(x+#quant, y, "()")} end if beglines[y]:match("^%.", x) then local ya = y + 1 while beglines[ya]:sub(x, x) == "|" do ya = ya + 1 end local c = bptree(x+1, y) or bperror(x+1, y, "c") local a = bptree(x+1, ya) or bperror(x+1, ya, "a") -- I am not testing for the "\\" yet return BegCond {a=a, c=c} end if beglines[y]:match("^ ", x) then return BegTerm {bpterm(x+1, y) or bperror(x, y, "term")} end bperror(x, y, "?") end -- «begriff_head» (to ".begriff_head") -- (find-dn5 "process.lua" "lua-head") registerhead "%B" { action = function () local chunkname = fname..":%B:"..nline beglines = { untabify(linestr) } -- get body of first line while nextheadstr() == "%B" do -- when the next line is also %B set_nline(nline + 1) -- advance pointer table.insert(beglines, untabify(linestr)) -- add its body to the chunk end processbeglines() end, } processbeglines = function () for y,line in ipairs(beglines) do for name,x in line:gmatch"([^ ]+) :+> ()" do local body = bpstart(x, y):TeX(" ") local link = " % no hyperlink yet" local def = format("\\defbegr{%s}{%s\n %s}", name, link, body) output(def) end end end -- «begriff_preamble» (to ".begriff_preamble") begriff_preamble = [[ % From: (find-dn5 "begriff.lua" "begriff_preamble") \usepackage{begriff} \def\defbegr#1#2{\expandafter\def\csname begr-#1\endcsname{#2}} \def\ifbegrundefined#1{\expandafter\ifx\csname begr-#1\endcsname\relax} \def\begr#1{\ifbegrundefined{#1} \errmessage{UNDEFINED BEGRIFFSSCHRIFT DIAGRAM: #1} \else \csname begr-#1\endcsname \fi } \def\BGrevconditional#1#2{\BGconditional{#2}{#1}} ]] -- dump-to: tests --[==[ * (eepitch-lua51) * (eepitch-kill) * (eepitch-lua51) require "begriff" A = BegAssert {BegCond {c=BegCond {c=BegTerm{"a"}, a=BegTerm{"b"}}, a=BegCond {c=BegTerm{"c"}, a=BegTerm{"d"}}}} print(A:TeX()) beglines = splitlines [[ |-.-~--.- a aa aaa | \- b \-(o).- c \-(\mathit{foo})- food ]] print(bpassert(1, 1):TeX()) beglines = splitlines [[ 52 ::> |-.-~--.----- a aa | \----- b \-(o).----- c \-(x)- d ]] processbeglines() = beglines[1]:sub(8) --]==] -- Local Variables: -- coding: raw-text-unix -- ee-anchor-format: "«%s»" -- End: