Check-in [98ef3fd317]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added support for rendering inductive goals with the up/down arrows.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:98ef3fd3178e3c09487cf6b5dc238903645bd770
User & Date: andy 2015-04-14 20:49:15
Context
2015-04-14
21:05
Added support for rendering rule names next to rules (as table captions). Names are *not* rendered on rule applications in derivations, mostly because names are not stored in the proof tree. check-in: 0672529592 user: andy tags: trunk
20:49
Added support for rendering inductive goals with the up/down arrows. check-in: 98ef3fd317 user: andy tags: trunk
20:21
Added a specialized version of the nat specification, for demonstration purposes. check-in: 4a035bbfc0 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

57
58
59
60
61
62
63













64
65
66
67
68
69
70
...
108
109
110
111
112
113
114

115
116
117
118
119
120
121
122
123
124
...
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
...
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347

348

349
350
351
352
353
354
355
356
        // rendering itself.
        function makeMath(s,display) {
            var element = display ? $("<div></div>") : $("<span></span>");
            element.html(s);

            return element;
        }














        this.renderTerm = function(t,isgoal) {

            function render(t,isgoal) {

                switch(t.tt()) {
                    case 'compound':
................................................................................
                            var args = t.body.map(render);

                            if(t.head in specialNames) {
                                // Render children+operator using the special name
                                return specialNames[t.head](args);
                            }
                            else {

                                var cls = isgoal === true ? 'goal' : 'comp';

                                return "<span class='" + cls + "'>" + t.head + 
                                    "</span>(" + args.join(", ") + ")";
                            }
                        }

                    // Variables are rendered in bold.
                    case 'variable':
                        return "<span class='var'>" + renderName(t.name) + "</span>";
................................................................................
         *   conclusionHook -- The same, but for the conclusion.
         *
         * Note that you have to pass a target element, which *must* already
         * be part of the document, because jQuery/FireFox have trouble 
         * constructing nested tables on un-inserted elements. Eventually this
         * will be remedied by using divs with CSS table layout classes.
         */
        this.renderProof = function(t) {

            var renderProof = _.bind(this.renderProof,this);

            // Get the human-readable name of a derivation step (rule)
            function getProofName(proof) {
                var t = proof.body[3].head;
                if(t !== "case")
                    return {
                        trivial : "\u22A4-R",
................................................................................
                            '<tr class="pline"><td></td></tr>' +
                            '<tr class="cline"><td></td></tr>' +
                          '</table></span>');

            // -------- Construct conclusion line --------
            // Render conclusion, and call the hook for it.
            conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");
            var conc = this.conclusionHook(conclusion);
            conclusion = typeof conc !== "undefined" ? conc : conclusion;

            var entails = $("<span>&nbsp;\u22A2&nbsp;</span>");
            var conclusionLine = $("td",proof).eq(1);

            // If there are any, process the context
            if(context.length > 0) {
                var premiseHook = this.premiseHook;
                context.forEach(function(t) {
                    var premise = $(makeMath(renderGoal(t))).addClass("premise")
                    var prem = premiseHook(premise);
                    premise = typeof prem !== "undefined" ? prem : 
                    conclusionLine.append(premise);
                });

                conclusionLine.append(entails);
            }
            conclusionLine.append(conclusion);

            // -------- Render the premises (subproofs) --------
            var premiseLine = $("td",proof).eq(0);
            if(subproofs.length > 0) {
                // Render all sub-proofs, add to premises

                subproofs.forEach(function(p) {

                    premiseLine.append(renderProof(p));
                });
            }
            else
                premiseLine.html("&nbsp;"); // Axiomatic

            return proof;
        }







>
>
>
>
>
>
>
>
>
>
>
>
>







 







>


|







 







|
|
<







 







|







|


|












>
|
>
|







57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
...
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
...
235
236
237
238
239
240
241
242
243

244
245
246
247
248
249
250
...
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
        // rendering itself.
        function makeMath(s,display) {
            var element = display ? $("<div></div>") : $("<span></span>");
            element.html(s);

            return element;
        }

        // Render the head of a compound. All this does is check for the 
        // presence of a trailing \sml or \big and render the head as 
        // inductive, as appropriate.
        function renderHead(h) {
            var m;
            if(m = h.match(/(.+)\\big$/))
                return m[1] + "<span class='ind-up'>&uarr;</span>";
            else if(m = h.match(/(.+)\\sml$/))
                return m[1] + "<span class='ind-down'>&darr;</span>";
            else
                return h; // Nothing special
        }

        this.renderTerm = function(t,isgoal) {

            function render(t,isgoal) {

                switch(t.tt()) {
                    case 'compound':
................................................................................
                            var args = t.body.map(render);

                            if(t.head in specialNames) {
                                // Render children+operator using the special name
                                return specialNames[t.head](args);
                            }
                            else {
                                var head = renderHead(t.head);
                                var cls = isgoal === true ? 'goal' : 'comp';

                                return "<span class='" + cls + "'>" + head + 
                                    "</span>(" + args.join(", ") + ")";
                            }
                        }

                    // Variables are rendered in bold.
                    case 'variable':
                        return "<span class='var'>" + renderName(t.name) + "</span>";
................................................................................
         *   conclusionHook -- The same, but for the conclusion.
         *
         * Note that you have to pass a target element, which *must* already
         * be part of the document, because jQuery/FireFox have trouble 
         * constructing nested tables on un-inserted elements. Eventually this
         * will be remedied by using divs with CSS table layout classes.
         */
        this.renderProof = function(t, path) {
            path = path === undefined ? [] : path;


            // Get the human-readable name of a derivation step (rule)
            function getProofName(proof) {
                var t = proof.body[3].head;
                if(t !== "case")
                    return {
                        trivial : "\u22A4-R",
................................................................................
                            '<tr class="pline"><td></td></tr>' +
                            '<tr class="cline"><td></td></tr>' +
                          '</table></span>');

            // -------- Construct conclusion line --------
            // Render conclusion, and call the hook for it.
            conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");
            var conc = this.conclusionHook(conclusion, path);
            conclusion = typeof conc !== "undefined" ? conc : conclusion;

            var entails = $("<span>&nbsp;\u22A2&nbsp;</span>");
            var conclusionLine = $("td",proof).eq(1);

            // If there are any, process the context
            if(context.length > 0) {
                var premiseHook = _.bind(this.premiseHook, this);
                context.forEach(function(t) {
                    var premise = $(makeMath(renderGoal(t))).addClass("premise")
                    var prem = premiseHook(premise, path);
                    premise = typeof prem !== "undefined" ? prem : 
                    conclusionLine.append(premise);
                });

                conclusionLine.append(entails);
            }
            conclusionLine.append(conclusion);

            // -------- Render the premises (subproofs) --------
            var premiseLine = $("td",proof).eq(0);
            if(subproofs.length > 0) {
                // Render all sub-proofs, add to premises
                var renderProof = _.bind(this.renderProof,this);
                subproofs.forEach(function(p,i) {
                    var newpath = path.concat(i);
                    premiseLine.append(renderProof(p, newpath));
                });
            }
            else
                premiseLine.html("&nbsp;"); // Axiomatic

            return proof;
        }