Explicitely use "letrec" for recursive lets.
[matthijs/master-project/report.git] / pret-trans.lua
1 -- filename : type-trans.lua
2 -- comment  : Pretty printing of core transformations. Parses a specific
3 --            syntax, consisting of a before / after with a dashed lined in
4 --            between, and some extra conditions to the right of the line.
5 --            Recreates this layout using frames and line commands.
6 -- author   : Matthijs Kooijman, Universiteit Twente, NL
7 -- copyright: Matthijs Kooijman
8 -- license  : None
9
10 local utf = unicode.utf8
11
12 local vis = buffers.newvisualizer("trans")
13
14 local commands = {}
15 -- A command to create a horizontal rule.
16 commands.rule = "\\HLine[width=.40 * \\the\\textwidth]"
17 -- Typing environment to use for the stuff before and after the line. Will be
18 -- prefixed with \start and \stop automatically.
19 commands.beforeenv = "unboxedlambda"
20 commands.afterenv = "unboxedlambda"
21 -- Frame commands to use for the left (before + line + after) and right
22 -- (conditions) parts. Should include an opening {, which will be closed
23 -- automatically.
24 commands.leftframe = "\\framed[offset=0mm,location=middle,strut=no,align=right,frame=off,width=.48\\textwidth]{"
25 commands.rightframe = "\\framed[offset=0mm,location=middle,strut=no,align=right,frame=off,width=.48\\textwidth]{"
26
27 -- A table to keep the lines in this buffer, so we can process them all at
28 -- once at the end.
29 local lines
30 -- A counter to keep track of the mininum amount of indentation found in each
31 -- display.
32 local min_indent
33
34 -- Some helper functions
35 local function ltrim(s)
36     return (string.gsub(s, "^%s*", ""))
37 end
38
39 local function rtrim(s)
40     return (string.gsub(s, "%s*$", ""))
41 end
42
43 -- Insert n blank lines
44 local function blanks(n)
45     for i = 1,n do
46         buffers.visualizers.handlers.default.empty_line()
47     end
48 end
49
50 -- Prettyprint the given lines using the given pretty printer
51 local function prettyprint(ppr, lines)
52     -- Change the current visualizer
53     buffers.setvisualizer('lam')
54
55     -- Output the lines
56     buffers.hooks.begin_of_display()
57     line = 0
58     for i = 1,#lines do
59         _, line = buffers.typeline(lines[i], i, #lines, line)
60     end
61     buffers.hooks.end_of_display()
62
63     -- Change the visualizer back
64     buffers.setvisualizer('trans')
65 end
66
67 -- Capture all lines, without generating any output
68 function vis.begin_of_display()
69     lines = {}
70     min_indent = nil
71 end
72 function vis.begin_of_line(n)
73     -- Don't generate output here
74 end
75 function vis.flush_line(str, nested)
76     -- Keep track of the minimum indent level of all lines. Note that we don't
77     -- look at empty lines, of course.
78     indent = utf.len(utf.match(str, "^%s*"))
79         -- Find the lowest indent (but don't count empty lines)
80     if (not min_indent or indent < min_indent) then
81         min_indent = indent
82     end
83
84     table.insert(lines, str)
85     -- Don't generate output here
86 end
87 function vis.end_of_line(n)
88     -- Don't generate output here
89 end
90 function vis.empty_line()
91     table.insert(lines, '')
92     -- Don't generate output here
93 end
94
95 -- We do the actual work here. Process all the lines in the buffer and
96 -- generate output for them.
97 function vis.end_of_display()
98     -- Strip indent that is present on every line
99     min_indent = min_indent or 0 
100     for i = 1,#lines do
101         lines[i] = utf.sub(lines[i], min_indent + 1)
102     end
103
104     -- Find the horizontal rule, and see how long it is.
105     len = nil
106     for i = 1,#lines do
107         match = utf.match(lines[i], "^%-%-%-*")
108         if match then
109             len = utf.len(match)
110             break
111         end
112     end
113   
114     if not len then
115         error("No horizontal separator found in:\n" .. table.concat(lines, "\n"))
116     end
117
118     -- Split the input in three parts. Stuff before the line, stuff
119     -- after the line, stuff to the right of the line.
120     before, after, rights = {}, {}, {}
121     found_line = false
122     for i = 1,#lines do
123         line = lines[i]
124         -- Split the line into a left and right part
125         left = rtrim(utf.sub(line, 1, len))
126         right = ltrim(utf.sub(line, len + 1))
127         if utf.match(left, "^%-%-%-*") then
128             found_line = true
129         else
130             if utf.len(left) > 0 then
131                 if not found_line then
132                     table.insert(before, left)
133                 else
134                     table.insert(after, left)
135                 end
136             end
137         end
138         if utf.len(right) > 0 then
139             table.insert(rights, right)
140         end
141     end
142
143     --
144     -- Real output starts here
145     --
146
147     -- Let all the lambda pretty printing in this buffer use shared subscript
148     -- detection
149     tex.sprint("\\directlua{buffers.visualizers.handlers.lam.begin_of_block()}")
150
151     -- Ensure the left and right frames end up next to each other.
152     tex.sprint("\\dontleavehmode")
153
154     -- Open and fill the left frame
155     tex.sprint(commands.leftframe)
156
157     tex.sprint("\\start" .. commands.beforeenv)
158
159     tex.sprint(table.concat(before, "\n"))
160
161     tex.sprint("\\stop" .. commands.beforeenv)
162
163     tex.sprint(commands.rule)
164
165     tex.sprint("\\start" .. commands.afterenv)
166
167     tex.sprint(table.concat(after, "\n"))
168
169     tex.sprint("\\stop" .. commands.afterenv)
170
171     -- Close the left frame
172     tex.sprint("}")
173
174     -- Open and fill the right frame
175     tex.sprint(commands.rightframe)
176
177     -- Insert spacer blank lines to align the middle condition with the
178     -- conclusion rule
179     n_blanks = #before - math.ceil((#rights - 1) / 2)
180     n_blanks = math.max(0, n_blanks)
181     blanks(n_blanks)
182
183     -- Print the conditions
184     for i = 1,#rights do
185         tex.sprint(rights[i])
186         buffers.visualizers.handlers.default.end_of_line()
187     end
188
189     -- Fill up the remaining space with blanks
190     n_blanks = (#before + 1 + #after) - (n_blanks + #rights)
191     n_blanks = math.max(0, n_blanks)
192     blanks(n_blanks)
193
194     -- Close the right frame 
195     tex.sprint("}")
196
197     tex.sprint("\\directlua{buffers.visualizers.handlers.lam.end_of_block()}")
198     
199     -- Clean up
200     lines = {}
201 end
202
203 -- vim: set sw=4 sts=4 expandtab ai: