Check-in [23db977deb]

Not logged in

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

Overview
Comment:Changed the encoding for inductive goals from \size to |size. The backslash was getting lost in the string encoding in some places.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:23db977debac1e859bb6eac1e7401289a641cd74
User & Date: andy 2015-04-15 21:36:57
Context
2015-04-15
21:37
Some additional styles for rendering of derivations. check-in: 9c0eace5aa user: andy tags: trunk
21:36
Changed the encoding for inductive goals from \size to |size. The backslash was getting lost in the string encoding in some places. check-in: 23db977deb user: andy tags: trunk
20:17
Added a new "PVar" subtype of Term, for Prolog variables that need to be preserved as such (i.e., distinguished from specification variables). check-in: 8949a9e372 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Show Whitespace Changes Patch

Changes to plsrc/checker.pl.

447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481



482
483
484
485
486
487
488
    % Get the premises and goal of the induction hypothesis
    get_ind_premises(Goal, Gs, R),

    % Get the target of the induction
    nth0(Index,Gs,G),

    % Get the small/large versions of it
    inductify_goal('\\sml',G,GSmall),
    inductify_goal('\\big',G,GBig),

    % Rewrite the goal to use the big version
    replace_nth0(Gs,Index,GBig,BigGs),
    andify(BigGs,AndBig),
    NewGoal = (AndBig -> R),

    % For IH, rewrite the goal to use the small version
    replace_nth0(Gs,Index,GSmall,SmallGs),
    andify(SmallGs,AndSmall),
    IH = (AndSmall -> R),

    % Add IH to the program, but only if it isn't already there.
    (member(ih(_,_,_),Program) -> 
      NewProgram = Program
    ;  
      NewProgram = [ih('IH',R,AndSmall)|Program]
    ),

    % Prove recursively
    check(NewProgram,
          state(Vars,Ctx,NewGoal),
          VOut,
          Proof),

    sub(Proof,Subst)
    .




% Helper to get the "list" of inductive premises
get_ind_premises(and(Gs) -> R, Gs, R) :- !.
get_ind_premises(G -> R, [G], R).

% Helper to do the opposite, turn a single and into itself
andify([G],G).







|
|












|
<
|
<
<
<
|





|
|
>
>
>







447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468

469



470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
    % Get the premises and goal of the induction hypothesis
    get_ind_premises(Goal, Gs, R),

    % Get the target of the induction
    nth0(Index,Gs,G),

    % Get the small/large versions of it
    inductify_goal('|sml',G,GSmall),
    inductify_goal('|big',G,GBig),

    % Rewrite the goal to use the big version
    replace_nth0(Gs,Index,GBig,BigGs),
    andify(BigGs,AndBig),
    NewGoal = (AndBig -> R),

    % For IH, rewrite the goal to use the small version
    replace_nth0(Gs,Index,GSmall,SmallGs),
    andify(SmallGs,AndSmall),
    IH = (AndSmall -> R), 

    % Add IH to the program, but only if it isn't already there.
    inductify_program(ih('IH',R,AndSmall),Program,NewProgram),





    % Prove recursively in new program
    check(NewProgram,
          state(Vars,Ctx,NewGoal),
          VOut,
          Proof),

    sub(Proof,Subst).

inductify_program(_,Program,Program) :-
    member(ih(_,_,_), Program), !.
inductify_program(IH,Program,[IH|Program]).

% Helper to get the "list" of inductive premises
get_ind_premises(and(Gs) -> R, Gs, R) :- !.
get_ind_premises(G -> R, [G], R).

% Helper to do the opposite, turn a single and into itself
andify([G],G).

Changes to plsrc/program.pl.

73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
...
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
    Goal =.. [Head|Args],

    % Check to see if the head ends with '\big' or '\sml'
    atom_length(Head,Hlen),
    Hlen >= 4,
    SubLen is Hlen - 4,
    atom_length(Head,Hlen),
    sub_atom(Head,SubLen,4,0,'\\sml'), !,

    Size = '\\sml',
    sub_atom(Head,0,SubLen,_,BaseHead),
    Base =.. [BaseHead|Args].

inductive(Goal,Base,Size) :-
    Goal =.. [Head|Args],

    % Check to see if the head ends with '\big' or '\sml'
    atom_length(Head,Hlen),
    Hlen >= 4,
    SubLen is Hlen - 4,
    atom_length(Head,Hlen),
    sub_atom(Head,SubLen,4,0,'\\big'), !,

    Size = '\\big',
    sub_atom(Head,0,SubLen,_,BaseHead),
    Base =.. [BaseHead|Args].

% Add the inductive prefix Size ('\sml' or '\big') onto Goal
inductify_goal(Size,Goal,IGoal) :-
    is_user_goal(Goal), !,
    Goal =.. [Head|Args],
................................................................................
    inductify_subgoals(Size,R,IR).

inductify_subgoals(Size,UGoal,IGoal) :-
    inductify_goal(Size,UGoal,IGoal).


% "Shrink" an inductive size to the next smaller size.
inductive_shrink('\\sml','\\sml').
inductive_shrink('\\big','\\sml').

%%% --------------------------------------------------------------------------
%%% Goal expansion
%%% --------------------------------------------------------------------------

% These are low-level routines related to expanding calls to user goals. Because
% we don't yet know the context of the call (antecedant or succedant) we expand







|

|











|

|







 







|
|







73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
...
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
    Goal =.. [Head|Args],

    % Check to see if the head ends with '\big' or '\sml'
    atom_length(Head,Hlen),
    Hlen >= 4,
    SubLen is Hlen - 4,
    atom_length(Head,Hlen),
    sub_atom(Head,SubLen,4,0,'|sml'), !,

    Size = '|sml',
    sub_atom(Head,0,SubLen,_,BaseHead),
    Base =.. [BaseHead|Args].

inductive(Goal,Base,Size) :-
    Goal =.. [Head|Args],

    % Check to see if the head ends with '\big' or '\sml'
    atom_length(Head,Hlen),
    Hlen >= 4,
    SubLen is Hlen - 4,
    atom_length(Head,Hlen),
    sub_atom(Head,SubLen,4,0,'|big'), !,

    Size = '|big',
    sub_atom(Head,0,SubLen,_,BaseHead),
    Base =.. [BaseHead|Args].

% Add the inductive prefix Size ('\sml' or '\big') onto Goal
inductify_goal(Size,Goal,IGoal) :-
    is_user_goal(Goal), !,
    Goal =.. [Head|Args],
................................................................................
    inductify_subgoals(Size,R,IR).

inductify_subgoals(Size,UGoal,IGoal) :-
    inductify_goal(Size,UGoal,IGoal).


% "Shrink" an inductive size to the next smaller size.
inductive_shrink('|sml','|sml').
inductive_shrink('|big','|sml').

%%% --------------------------------------------------------------------------
%%% Goal expansion
%%% --------------------------------------------------------------------------

% These are low-level routines related to expanding calls to user goals. Because
% we don't yet know the context of the call (antecedant or succedant) we expand

Changes to src/term_render.js.

50
51
52
53
54
55
56









57
58
59
60
61
62
63
..
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
...
238
239
240
241
242
243
244






245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
...
291
292
293
294
295
296
297

298
299
300
301
302
303
304
...
309
310
311
312
313
314
315


























316
317




















318
319

320
321
322
323
324
325
326

        // Hooks for rendering various parts of rules/proofs.
        this.premiseHook = 'premiseHook' in options ? options['premiseHook'] :
                            function(e) { return e; };
        this.conclusionHook = 'conclusionHook' in options ? options['conclusionHook'] :
                            function(e) { return e; };










        // Currently does nothing, as all the "mathification" happens in the
        // 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) {

................................................................................
         *
         * There are two hooks available to help with building interactive 
         * proofs:
         *   premiseHook -- Is passed every premise when rendering the context.
         *                  It should require a jQuery node object that will be
         *                  used for the actual element of the context.
         *   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",
                        hole : "",
                        unify : "=R",
                        ctxmem : "", // Assumption
                        induction : "By induction",
                        ih : "IH",
                        generic : "&forall;-R",
                        instan : "&exist;-R",
                        product : "&and;-R",
                        choice : "&or;-R",
                        implies : "&rarr;R",
                        backchain : "", 
                    }[t];
                else 
                    return {
                        false_left : "&perp;-L",
                        and_left : "&and;-L",
                        or_left : "&or;-L",
                        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
................................................................................
            // (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
................................................................................
            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;







>
>
>
>
>
>
>
>
>







 







|

|







 







>
>
>
>
>
>











|
|













|









|







 







>







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
|
>







50
51
52
53
54
55
56
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
84
85
86
87
88
89
...
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
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
...
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
...
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
380
381
382
383
384
385
386
387
388
389

        // Hooks for rendering various parts of rules/proofs.
        this.premiseHook = 'premiseHook' in options ? options['premiseHook'] :
                            function(e) { return e; };
        this.conclusionHook = 'conclusionHook' in options ? options['conclusionHook'] :
                            function(e) { return e; };

        // Optional hooks for disjuncts, inductive goals.
        this.disjunctHook = null;
        this.inductionHook = null;

        // In an inductive proof, the head of the inductive goal (note:
        // NOT the inductive premise). This is used so that we know when it
        // is possible to backchain the goal against the IH.
        this.inductionHead = 'inductionHead' in this ? this.inductionHead : null;

        // Currently does nothing, as all the "mathification" happens in the
        // 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) {

................................................................................
         *
         * There are two hooks available to help with building interactive 
         * proofs:
         *   premiseHook -- Is passed every premise when rendering the context.
         *                  It should require a jQuery node object that will be
         *                  used for the actual element of the context.
         *   conclusionHook -- The same, but for the conclusion.
         *   disjunctHook -- If the goal is a disjunction, and this is
         *                   not null, then it will be called *instead of*
         *                   conclusionHook for each disjunct.
         *   inductionHook -- In an inductive proof, if the head/arity of the
         *                    goal matches that of the IH, then this will be
         *                    called on the goal *instead of* conclusionHook.
         *
         * 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 name = proof.body[3].head;
                if(name !== "case")
                    return {
                        trivial : "\u22A4-R",
                        hole : "",
                        unify : "=R",
                        ctxmem : "", // Assumption
                        induction : "By induction",
                        ih : "IH",
                        generic : "&forall;-R",
                        instan : "&exist;-R",
                        product : "&and;-R",
                        choice : "&or;-R",
                        implies : "&rarr;R",
                        backchain : "", 
                    }[name];
                else 
                    return {
                        false_left : "&perp;-L",
                        and_left : "&and;-L",
                        or_left : "&or;-L",
                        forall_left : "&forall;-L",
                        exists_left : "&exist;-L",
                        unify_left : "=L",
                        goal_left : ""
                    }[proof.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
................................................................................
            // (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 chtml;

            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
................................................................................
            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 --------
            // For normal conclusions we just render as usual, with 
            // conclusionHook
            if(conclusion.head === "or" && this.disjunctHook !== null) {
                // For disjunctions we render each disjunct separately and then
                // call disjunctHook on each. 
                chtml = $("<span class='or conclusion'></span>");

                var disjuncts = terms.toArray(conclusion.body[0]);
                var renderGoal = _.bind(this.renderGoal,this);
                var disjunctHook = this.disjunctHook;

                // Render each disjunct and then call the hook on it
                disjuncts.map(function(t,i) {
                    var tm = renderGoal(t);
                    var tm2 = disjunctHook.call(t,tm,path,i);
                    tm2 = typeof tm2 === "undefined" ? tm : tm2;
                    return tm;
                });

                chtml.append(disjuncts.join("&or;"));
            }
            else if(conclusion.head == this.inductionHead &&
                    this.inductionHook !== null) {

                // Goal is the same as the inductive target, so we just call
                // inductionHook instead of conclusionHook. 
                // Render conclusion, and call the hook for it.
                chtml = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");
                chtml.addClass("inductive");

                // We class the conclusion element with its head. This allows us
                // to use custom styles for things like and, or, etc.
                chtml.addClass(conclusion.head);

                // Call the conclusion hook
                var conc = this.inductionHook.call(conclusion, chtml, path);
                chtml = typeof conc !== "undefined" ? conc : chtml;                
            }
            else {

                // Render conclusion, and call the hook for it.
                chtml = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");

                // We class the conclusion element with its head. This allows us
                // to use custom styles for things like and, or, etc.
                chtml.addClass(conclusion.head);

                // Call the conclusion hook
                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;

Changes to src/terms.js.

335
336
337
338
339
340
341



342
343
344
345
346
347
348
349
            // so we have to make sure that numeric-ish atoms get sent 
            // unquoted.
            if(!isNaN(parseInt(t.head,10)))
                return " " + parseInt(t.head,10).toString() + " ";
            else if(t.head === "[]")
                return "[]"
            else



                return " '" + t + "' ";
        }
        else if(t.isList())
            return "[ " + terms.toArray(t).map(stringify).join(",") + " ]";
        else if(t.isCompound())
            return " '" + t.head + 
                   "'(" + t.body.map(stringify).join(" , ") + ") ";
    }







>
>
>
|







335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
            // so we have to make sure that numeric-ish atoms get sent 
            // unquoted.
            if(!isNaN(parseInt(t.head,10)))
                return " " + parseInt(t.head,10).toString() + " ";
            else if(t.head === "[]")
                return "[]"
            else
                // even in normal atoms we have to escape \s.
                // We convert them to Prolog's unicode escapes, as I've had
                // trouble with the \\ escape for a single \ getting "eaten"
                return " '" + t.head.replace("\\","\\u005") + "' ";
        }
        else if(t.isList())
            return "[ " + terms.toArray(t).map(stringify).join(",") + " ]";
        else if(t.isCompound())
            return " '" + t.head + 
                   "'(" + t.body.map(stringify).join(" , ") + ") ";
    }