Check-in [6ca1a452f3]

Not logged in

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

Overview
Comment:Fixed many small bugs in elaboration, checking of incomplete proofs.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:6ca1a452f31bea410ee5d9e7d79188f6a6501162
User & Date: andy 2015-04-16 22:02:07
Context
2015-04-18
16:44
Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk
2015-04-16
22:02
Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk
22:01
Fixed demo IH to conform to the new vertical-bar encoding. check-in: 925c93ea0a user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
...
216
217
218
219
220
221
222
223
224



225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
...
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
...
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
...
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
...
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
...
589
590
591
592
593
594
595
596
597
598
599


600
601
602
603
604
605
606
...
654
655
656
657
658
659
660

661
662
663
664
665
666
667
668
669
670
671
                  Subproofs,
                  case(Type,N,Keep,Subproofs)) :- !.

replace_subproofs(product(_),Subproofs,product(Subproofs)) :- !.

% All of the other proof types have a single subproof, and they store it in
% their last argument. So we can extract it without caring about the type.
replace_subproof(ProofTerm,[Subproof],NewProofTerm) :-
    ProofTerm =.. [Type|Args],
    length(Args,Len),
    Last is Len - 1,
    replace_nth0(Args,Last,Subproof,NewArgs),
    NewProofTerm =.. [Type|NewArgs].

% elaborate(Tree,Path,NewTree)
................................................................................
    % subproof itself, uninstantiated, so we now call check to let it fill in
    % the details.
    Tree = proof(Goal,_,_,_),
    check(Program, Goal, NewTree).

% If the path is empty, we've reached the node we're looking for, so all the 
elaborate(Proof,[],What,Data,EProof) :-
    Proof = proof(Goal,Ctx,Subst,_),
    elaborate_node(Goal,Ctx,What,Data,Elaboration),



    EProof = proof(Goal,Ctx,Subst,Elaboration).


elaborate(proof(Goal,Ctx,Subst,Proof), 
          [N|Ns],What,Data,
          proof(Goal,Ctx,Subst,NewProof)) :-

    % Find the Nth subproof and recurse down it
    subproofs(Proof,Subproofs),
    nth0(N,Subproofs,Branch),
    elaborate(Branch,Ns,What,Data,NewBranch),

    % Reconstruct the proof with the new branch spliced in.
    replace_nth0(Subproofs,N,NewBranch,NewSubproofs),
    replace_subproof(Proof,NewSubproofs,NewProof).

% elaborate_node(Goal,Ctx,What,Data,Elaboration)
% Elaborating a single node is just a matter of applying the translation from
% figs. 3 and 4 in the report. `What` tells us what to elaborate on:
% either `goal` or `ctx`
elaborate_node(true,        _, goal,_,  trivial).
elaborate_node(_ = _,       _, goal,_,  unify(_,_)).
................................................................................
    elaborate_ctx(Premise,Type,Elaboration).

% Elaborate an element of the context, based on its structure.
elaborate_ctx(false,       false_left,     []).
elaborate_ctx(and(_),      and_left,       [proof(_,_,_,hole)]).
elaborate_ctx(forall(_,_), forall_left(_), [proof(_,_,_,hole)]).
elaborate_ctx(exists(_,_), exists_left,    [proof(_,_,_,hole)]).
elaborate_ctx(unify(_,_),  unify_left,     [proof(_,_,_,hole)]).
elaborate_ctx(G,           goal_left,      [proof(_,_,_,hole)]) :-
    is_user_goal(G).

elaborate_ctx(or(Ps),      or_left,  Holes) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).


................................................................................
%%% ---------------------------------------------------------------------------

% check(Program, Goal, Proof)
% Check the Proof of Goal, in Program.

check(Program,Goal,proof(Goal,Ctx,Subst,Proof)) :-
  get_vars(Goal,Vars),
  Ctx = [],
  check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)).

% check(Program,State,VOut,Proof)
% -- State = state(Vars,Ctx,Goal)
% -- Proof = proof(Goal,Ctx,Subst,Proof)
% and Proof has one of the forms mentioned above.

................................................................................
    % Apply substitution to remaining conjuncts
    apply_subst(S2,Cs,Cs2),

    % Check remaining conjuncts
    check(Program,
          state(Vars,Ctx,and(Cs2)),
          V3,
          SubProofs),
    SubProofs = proof(_,_,S3,product(Ps)),

    % Merge substitutions and variable bindings
    subst:merge(S3,S2,Subst),
    union(V2,V3,VOut).

% Disjunction:
% Handled non-deterministically (if Proof is unbound). Note that unlike in
................................................................................
% ctxmem(Index)
% Assumption rule: prove that the given element of the context is 
% *identical* to the current goal.
% Note that for convenience we do not restrict this to user goals.
check(_,
      state(Vars,Ctx,Goal),
      Vars,
      proof(Goal,Ctx,_,Proof)) :-

    % Don't ever generate a ctxmem proof, it must be supplied.
    %nonvar(Proof), 
    Proof = ctxmem(Index),

    % Get the element of the context and compare it to the current goal
    nth0(Index,Ctx,Goal2),
................................................................................
    Goal == Goal2.

% hole
% An asofyet unproved branch of the proof.
check(_,
      state(_,Ctx,Goal),
      _,
      proof(Goal,Ctx,_,Hole)) :-

    nonvar(Hole),
    Hole = hole.



%%% ---------------------------------------------------------------------------
%%% Case analysis
%%% ---------------------------------------------------------------------------

check(Program,
      state(Vars,Ctx,Goal),
................................................................................
    % Get the element of the context (must be an and())
    keep_rest(N,Ctx,Keep,and(Cs),Ctx2),

    % Add the elements of the conjunction to the context
    append(Cs,Ctx2,NewCtx),

    % Prove goal recursively in the new context.

    check(Program,
          state(Vars,NewCtx,Goal),
          VOut,
          proof(Goal,NewCtx,Subst,Proof)).

% or_left
% Generate a sub-proof for every branch of the disjunction. 
check_case(case(or_left,N,Keep,Proofs),
           Program,
           state(Vars,Ctx,Goal),
           VOut, 







|







 







|

>
>
>
|













|







 







|







 







|







 







<
|







 







|







 







|


|
>
>







 







>



|







185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
...
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
...
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
...
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
...
377
378
379
380
381
382
383

384
385
386
387
388
389
390
391
...
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
...
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
...
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
                  Subproofs,
                  case(Type,N,Keep,Subproofs)) :- !.

replace_subproofs(product(_),Subproofs,product(Subproofs)) :- !.

% All of the other proof types have a single subproof, and they store it in
% their last argument. So we can extract it without caring about the type.
replace_subproofs(ProofTerm,[Subproof],NewProofTerm) :-
    ProofTerm =.. [Type|Args],
    length(Args,Len),
    Last is Len - 1,
    replace_nth0(Args,Last,Subproof,NewArgs),
    NewProofTerm =.. [Type|NewArgs].

% elaborate(Tree,Path,NewTree)
................................................................................
    % subproof itself, uninstantiated, so we now call check to let it fill in
    % the details.
    Tree = proof(Goal,_,_,_),
    check(Program, Goal, NewTree).

% If the path is empty, we've reached the node we're looking for, so all the 
elaborate(Proof,[],What,Data,EProof) :-
    Proof = proof(Goal,Ctx,_,_),
    elaborate_node(Goal,Ctx,What,Data,Elaboration),

    % During elaborate we replace all the Substs with _, because
    % check will fill them in. 
    EProof = proof(Goal,Ctx,_,Elaboration).


elaborate(proof(Goal,Ctx,Subst,Proof), 
          [N|Ns],What,Data,
          proof(Goal,Ctx,Subst,NewProof)) :-

    % Find the Nth subproof and recurse down it
    subproofs(Proof,Subproofs),
    nth0(N,Subproofs,Branch),
    elaborate(Branch,Ns,What,Data,NewBranch),

    % Reconstruct the proof with the new branch spliced in.
    replace_nth0(Subproofs,N,NewBranch,NewSubproofs),
    replace_subproofs(Proof,NewSubproofs,NewProof).

% elaborate_node(Goal,Ctx,What,Data,Elaboration)
% Elaborating a single node is just a matter of applying the translation from
% figs. 3 and 4 in the report. `What` tells us what to elaborate on:
% either `goal` or `ctx`
elaborate_node(true,        _, goal,_,  trivial).
elaborate_node(_ = _,       _, goal,_,  unify(_,_)).
................................................................................
    elaborate_ctx(Premise,Type,Elaboration).

% Elaborate an element of the context, based on its structure.
elaborate_ctx(false,       false_left,     []).
elaborate_ctx(and(_),      and_left,       [proof(_,_,_,hole)]).
elaborate_ctx(forall(_,_), forall_left(_), [proof(_,_,_,hole)]).
elaborate_ctx(exists(_,_), exists_left,    [proof(_,_,_,hole)]).
elaborate_ctx(_ = _,       unify_left,     [proof(_,_,_,hole)]).
elaborate_ctx(G,           goal_left,      [proof(_,_,_,hole)]) :-
    is_user_goal(G).

elaborate_ctx(or(Ps),      or_left,  Holes) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).


................................................................................
%%% ---------------------------------------------------------------------------

% check(Program, Goal, Proof)
% Check the Proof of Goal, in Program.

check(Program,Goal,proof(Goal,Ctx,Subst,Proof)) :-
  get_vars(Goal,Vars),
  % Ctx = [],
  check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)).

% check(Program,State,VOut,Proof)
% -- State = state(Vars,Ctx,Goal)
% -- Proof = proof(Goal,Ctx,Subst,Proof)
% and Proof has one of the forms mentioned above.

................................................................................
    % Apply substitution to remaining conjuncts
    apply_subst(S2,Cs,Cs2),

    % Check remaining conjuncts
    check(Program,
          state(Vars,Ctx,and(Cs2)),
          V3,

          proof(_,_,S3,product(Ps))),

    % Merge substitutions and variable bindings
    subst:merge(S3,S2,Subst),
    union(V2,V3,VOut).

% Disjunction:
% Handled non-deterministically (if Proof is unbound). Note that unlike in
................................................................................
% ctxmem(Index)
% Assumption rule: prove that the given element of the context is 
% *identical* to the current goal.
% Note that for convenience we do not restrict this to user goals.
check(_,
      state(Vars,Ctx,Goal),
      Vars,
      proof(Goal,Ctx,[],Proof)) :-

    % Don't ever generate a ctxmem proof, it must be supplied.
    %nonvar(Proof), 
    Proof = ctxmem(Index),

    % Get the element of the context and compare it to the current goal
    nth0(Index,Ctx,Goal2),
................................................................................
    Goal == Goal2.

% hole
% An asofyet unproved branch of the proof.
check(_,
      state(_,Ctx,Goal),
      _,
      proof(Goal,Ctx,Subst,Hole)) :-

    nonvar(Hole),
    Hole = hole,
    % I'm not sure if this is correct...
    Subst = [].

%%% ---------------------------------------------------------------------------
%%% Case analysis
%%% ---------------------------------------------------------------------------

check(Program,
      state(Vars,Ctx,Goal),
................................................................................
    % Get the element of the context (must be an and())
    keep_rest(N,Ctx,Keep,and(Cs),Ctx2),

    % Add the elements of the conjunction to the context
    append(Cs,Ctx2,NewCtx),

    % Prove goal recursively in the new context.
    Proof = proof(Goal,NewCtx,Subst,_),
    check(Program,
          state(Vars,NewCtx,Goal),
          VOut,
          Proof).

% or_left
% Generate a sub-proof for every branch of the disjunction. 
check_case(case(or_left,N,Keep,Proofs),
           Program,
           state(Vars,Ctx,Goal),
           VOut,