Check-in [f84190c56c]

Not logged in

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

Overview
Comment:Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:f84190c56ccebea910b8edbc0acc99c9da41f87a
User & Date: andy 2015-04-15 11:48:44
Context
2015-04-15
14:31
Fixed a small logical mistake in a footnote. check-in: 556662b818 user: andy tags: trunk
11:48
Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself. check-in: f84190c56c user: andy tags: trunk
11:47
Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

9
10
11
12
13
14
15

16
17
18
19
20
21
22
...
149
150
151
152
153
154
155





156


157
158
159
160
161
162
163
...
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
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
357
358
359
360
361
362
363
364
365
366
367
368



369
370
371

372
373
374
375
376
377
378
379

// Since this isn't a "real" Arend module we don't play by the normal rules
// and install ourself into the module namespace. We just setup a global 
// renderTerm function.
(function() {

    var terms = arend['terms']; // Access the terms module


    var specialNames = {

        // Built-ins 
        "true" : "\u22A4",
        "false" : "\u22A5",

................................................................................
        //   rule(Name,Head,and([body...]))
        //     ih(Name,Head,and([body...]))
        // They are rendered as tables with the head on the bottom row and 
        // the elements of the body on top
        this.renderRule = function(t) {
            var name = t.body[0];
            var head = t.body[1];





            var body = terms.toArray(t.body[2].body[0]);



            var renderTerm = _.bind(this.renderTerm,this);
            var renderGoal = _.bind(this.renderGoal,this);

            var rule = $("<table class='rule'>" + 
                           "<caption>" + name + "</caption>" +
                           "<tr class='pline'><td></td></tr>" + 
................................................................................
                        forall_left : "&forall;-L",
                        exists_left : "&exist;-L",
                        unify_left : "=L",
                        goal_left : ""
                    }[t.body[3].body[0].head];
            }

            // Extract the array of subproof objects from a proof term
            function getSubProofs(t) {
                var proof = t.body[3];
                switch(proof.head) {
                    // 0 subproofs
                    case "trivial":
                    case "hole":
                    case "unify":
                    case "ctxmem":
                        return [];

                    // 1 subproof, first argument
                    case "ih":
                    case "generic":
                    case "implies":
                    case "backchain":
                        return [proof.body[0]];

                    // 1 subproof, second argument
                    case "induction":
                    case "instan":
                    case "choice":
                        return [proof.body[1]];

                    // Product
                    case "product":
                        return terms.toArray(proof.body[0]);
                }

                // The only other option is case, which always has a list of
                // subproofs (0,1, or N elements):
                return terms.toArray(proofs.body[3]);
            }

            // ----------------------------------
            // Rendering a proof
            // ----------------------------------
            // To render a proof, we render it like a rule, except that the
            // "premises" can now be subproofs. The conclusion line is
            // rendered as 
            //   context... |- conclusion
            // (Unless the context is empty, in which case it and the 
            // turnstile are hidden.)
            var conclusion = t.body[0];
            
            // Special cases if the conclusion is a hole, then we render the
            // entire proof as just "?"
            if(conclusion.head === "hole")
                return $("<span>?</span>");

            var context = terms.toArray(t.body[1]);
            var subproofs = getSubProofs(t);
            var rulename = getProofName(t);











            var proof = $('<span><table class="rule proof tab">' + 
                            //<caption>RuleName</caption>

                            '<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;
        }

        this.renderString = function(s) {
            return s; // makeMath(s)
        }
    }








>







 







>
>
>
>
>
|
>
>







 







<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<










|
<
<
<
<
<

|


>
>
>
>
>
>
>
>
>
>
|
<
>






|
|
|


|



|
>
>
|

|
|





|


|








>
>
>
|
|
|
>
|







9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
...
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
...
277
278
279
280
281
282
283


































284
285
286
287
288
289
290
291
292
293
294





295
296
297
298
299
300
301
302
303
304
305
306
307
308
309

310
311
312
313
314
315
316
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
357
358
359
360
361
362
363
364

// Since this isn't a "real" Arend module we don't play by the normal rules
// and install ourself into the module namespace. We just setup a global 
// renderTerm function.
(function() {

    var terms = arend['terms']; // Access the terms module
    var proof = arend['proof'];

    var specialNames = {

        // Built-ins 
        "true" : "\u22A4",
        "false" : "\u22A5",

................................................................................
        //   rule(Name,Head,and([body...]))
        //     ih(Name,Head,and([body...]))
        // They are rendered as tables with the head on the bottom row and 
        // the elements of the body on top
        this.renderRule = function(t) {
            var name = t.body[0];
            var head = t.body[1];
            var body;

            // If the body of a rule is a conjunction, then we get the list of
            // its conjuncts, otherwise we just get it as a single element.
            if(t.body[2].head === "and")
                body = terms.toArray(t.body[2].body[0]);
            else
                body = [t.body[2]];

            var renderTerm = _.bind(this.renderTerm,this);
            var renderGoal = _.bind(this.renderGoal,this);

            var rule = $("<table class='rule'>" + 
                           "<caption>" + name + "</caption>" +
                           "<tr class='pline'><td></td></tr>" + 
................................................................................
                        forall_left : "&forall;-L",
                        exists_left : "&exist;-L",
                        unify_left : "=L",
                        goal_left : ""
                    }[t.body[3].body[0].head];
            }



































            // ----------------------------------
            // Rendering a proof
            // ----------------------------------
            // To render a proof, we render it like a rule, except that the
            // "premises" can now be subproofs. The conclusion line is
            // rendered as 
            //   context... |- conclusion
            // (Unless the context is empty, in which case it and the 
            // turnstile are hidden.)
            var conclusion = t.body[0];






            var context = terms.toArray(t.body[1]);
            var subproofs = proof.getSubProofs(t);
            var rulename = getProofName(t);

            var hole = (t.body[3].head === "hole");

            // TODO: caption positions in derivations.
            // We can't just render rulenames as captions, because they'll
            // be centered in the height of the table which, if the subproofs
            // have tall derivations, may be much higher than the conclusion
            // line. We need to find a way to position the caption exactly
            // centered on the dividing line. Probably some position: relative
            // magic will do it.

            var pr = $('<span><table class="rule proof tab">' + 

                            //"<caption>" + rulename + "</caption>" +
                            '<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.
            chtml = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");
            var conc = this.conclusionHook.call(conclusion, chtml, path);
            chtml = typeof conc !== "undefined" ? conc : chtml;

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

            // If there are any, process the context
            if(context.length > 0) {
                var premiseHook = this.premiseHook;
                var renderGoal = _.bind(this.renderGoal,this);

                context.forEach(function(t,i) {
                    var premise = $(makeMath(renderGoal(t))).addClass("premise")
                    var prem = premiseHook.call(t, premise, path, i);
                    premise = typeof prem !== "undefined" ? prem : premise;
                    conclusionLine.append(premise);
                });

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

            // -------- Render the premises (subproofs) --------
            var premiseLine = $("td",pr).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 {
                if(hole)
                    premiseLine.text("?"); // Hole
                else
                    premiseLine.html("&nbsp;"); // Axiomatic
            }

            return pr;
        }

        this.renderString = function(s) {
            return s; // makeMath(s)
        }
    }