Add support for pretty printing lambda calculus.

diff --git a/Core2Core.tex b/Core2Core.tex
index 1c972d1c7cb1ec1cb32d0d49ddfdffbfe0258eb0..bc385a68324b210e435dbe1f42cbfed975099f8a 100644 (file)
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -36,6 +36,9 @@
   \stopframedtext
 }
 
   \stopframedtext
 }
 

+% Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
+\installprettytype [LAM] [LAM]
+

 % A helper to print a single example in the half the page width. The example
 % text should be in a buffer whose name is given in an argument.
 %
 % A helper to print a single example in the half the page width. The example
 % text should be in a buffer whose name is given in an argument.
 %

diff --git a/pret-lam.lua b/pret-lam.lua
new file mode 100644 (file)
index 0000000..15fcf9a
--- /dev/null
+++ b/pret-lam.lua
@@ -0,0 +1,62 @@
+-- filename : type-lam.lua
+-- comment  : Pretty printing of (extended) lambda calculus
+-- author   : Matthijs Kooijman, Universiteit Twente, NL
+-- copyright: Matthijs Kooijman
+-- license  : None
+
+local utf = unicode.utf8
+
+if not buffers                 then buffers                 = { } end
+if not buffers.visualizers     then buffers.visualizers     = { } end
+if not buffers.visualizers.lam then buffers.visualizers.lam = { } end
+
+buffers.visualizers.lam.colors = {
+    "prettytwo",
+    "prettyone",
+    "prettythree",
+    "prettyfour"
+}
+
+buffers.visualizers.lam.tokens = {
+    [' '] = {repr = '\\obs '},
+    ['->'] = {repr = '\\rightarrow'},
+    ['case'] = {style = 'bold'},
+    ['of'] = {style = 'bold'},
+    ['let'] = {style = 'bold'},
+}
+
+function buffers.visualizers.lam.flush_line(str,nested)
+    local result, state = { }, 0
+    local finish, change = buffers.finish_state, buffers.change_state
+    -- Set the colorscheme, which is used by finish_state and change_state
+    buffers.currentcolors = buffers.visualizers.lam.colors
+
+    while str ~= "" do
+        found = false
+        for tok,props in pairs(buffers.visualizers.lam.tokens) do
+            -- Try to remove tok from the start of str 
+            str, count = utf.gsub(str, "^" .. tok, "")
+            if count ~= 0 then
+                -- Replace the token with the repr, or just itself
+                result[#result+1] = props.repr or tok
+                -- Enclose the token in {\style .. }
+                if props.style then
+                    result[#result] = "{\\" .. props.style ..
+                                        " " .. result[#result] ..
+                                        "}"
+                end
+                -- We found a token, now start over
+                found = true
+                break
+            end
+        end
+        if not found then
+            result[#result+1] = utf.sub(str, 1, 1)
+            str = utf.sub(str, 2)
+        end
+    end
+    state = finish(state, result)
+    buffers.flush_result(result,nested)
+end
+
+-- vim: set sw=4 sts=4 expandtab ai: