Check-in [52b0f899a0]

Not logged in

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

Overview
Comment:Fixed everything else to work with the new goal/clausal expansion.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst | working
Files: files | file ages | folders
SHA1:52b0f899a0525c7a30b54279701f218fe9429026
User & Date: andy 2015-04-21 15:47:54
Context
2015-04-21
16:25
Added proof demo example. check-in: 018383954d user: andy tags: bc-subst
15:47
Fixed everything else to work with the new goal/clausal expansion. check-in: 52b0f899a0 user: andy tags: bc-subst, working
15:47
Fixed module imports to avoid a (meaningless) warning. check-in: 8ad421112c user: andy tags: bc-subst
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
...
209
210
211
212
213
214
215
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
...
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
...
543
544
545
546
547
548
549
550


551
552
553
554
555
556
557
558
559
560
561
562


563
564
565
566
567
568
569
...
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856




857




858
859
860
subproofs(induction(_,_,Proof),             [Proof]).
subproofs(ih(Proof),                        [Proof]).
subproofs(generic(Proof),                   [Proof]).
subproofs(instan(_,Proof),                  [Proof]).
subproofs(product(Proofs),                  Proofs).
subproofs(choice(_,Proof),                  [Proof]).
subproofs(implies(Proof),                   [Proof]).
subproofs(backchain(_,Proof),                 [Proof]).
subproofs(case(false_left,_,_,[]),          []).
subproofs(case(and_left,_,_,[Proof]),       [Proof]).
subproofs(case(or_left,_,_,Proofs),         Proofs).
subproofs(case(forall_left(_),_,_,[Proof]), [Proof]).
subproofs(case(exists_left,_,_,[Proof]),    [Proof]).
subproofs(case(unify_left,_,_,[Proof]),     [Proof]).
subproofs(case(goal_left,_,_,[Proof]),      [Proof]). 

% replace_subproofs(Proof,Subproofs,NewProof)
% Replace the subproofs in a proof() object.
replace_subproofs(trivial,[],trivial) :- !.
replace_subproofs(hole,[],hole) :- !.
replace_subproofs(unify(A,B),[],unify(A,B)) :- !.
replace_subproofs(ctxmem(N),[],ctxmem(N)) :- !.
................................................................................
% elaborate atomic goals, `forall`s, or `exists`s.

% A path is a list of directions through a proof tree. A direction is just an
% index into the list of subproofs (generated by subproofs/2) of a proof. 
elaborate(Program,Tree,Path,What,Data,NewTree) :-

    % Fill in the target node with its elaboration
    elaborate(Program,Tree,Path,What,Data,NewTree),

    % The elaboration leaves the  arguments to proof(), other than the 
    % 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(Program,Proof,[],What,Data,EProof) :-
    Proof = proof(Goal,Ctx,_,_),
    elaborate_node(Program,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(Program,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(Program,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
................................................................................

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


% proof_complete(Proof)
% A proof is complete only if it contains no holes.

proof_complete(trivial).
proof_complete(ctxmem(_)).
proof_complete(unify(_,_)).
proof_complete(case(false_left,_,_,[])).
proof_complete(induction(_,_,Proof)) :- proof_complete(Proof).
proof_complete(ih(Proof)) :- proof_complete(Proof).
proof_complete(generic(Proof)) :- proof_complete(Proof).
proof_complete(instan(_,Proof)) :- proof_complete(Proof).
proof_complete(product(Proofs)) :- maplist(proof_complete,Proofs).
proof_complete(choice(_,Proof)) :- proof_complete(Proof).
proof_complete(implies(Proof)) :- proof_complete(Proof).
proof_complete(backchain(_,Proof)) :- proof_complete(Proof).
proof_complete(case(and_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(or_left,_,_,Proofs)) :- maplist(proof_complete,Proofs).
proof_complete(case(forall_left(_),_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(exists_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(unify_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(goal_left,_,_,[Proof])) :- proof_complete(Proof).


%%% ---------------------------------------------------------------------------

% Just check a proof (since it contains the goal)
check(Program,Proof) :-
  Proof = proof(Goal,_,_,_),
  check(Program,Goal,Proof).
................................................................................
    Rule = rule(Name,Head,Body),

    % From here on out it's very similar to backchaining on a normal goal
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % "Call" (expand) the Goal in the program consisting only of the IH
    program:call_goal([Rule],V2,Goal,Expansion),


    Proof = proof(Expansion,_,_,_),

    get_vars(Expansion,V3),
    union(V2,V3,V4),

    % Prove recursively on the expansion
    check(Program,
          state(V4,Ctx,Expansion),
          VOut,
          Proof),

    sub(Proof,Subst).



% generic
% Prove a forall generically, by introducing a new constant.
check(Program,
      state(Vars,Ctx,forall(V,Goal)),
      VOut,
      proof(forall(V,Goal),Ctx,NewSubst,generic(Proof))) :-
................................................................................

    % Expand the clause 
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    program:call_goal(Program,V2,Premise,Clauses),

    % Get variables from the expansion
    %get_vars(Clauses,V3),
    %union(V2,V3,NewVars),

    % Generate a subproof for each clause
    length(Clauses,N),
    length(Proofs,N),

    maplist(check_case_clause(Program,state(Vars,Ctx2,Goal)),
            Clauses,
            _,
            Proofs).

    % TODO: do we need to accumulate substitutions here?

% Check a subproof of the individual clauses
check_case_clause(Program,
                  state(Vars,Ctx,Goal),
                  Clause,
                  VOut,
                  Proof) :-





    NewCtx = [Clause|Ctx],




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









|
|
|
|
|
|
<
<







 







|








|







|






|







 







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







 







|
>
>











|
>
>







 







<
<
<
<

|
|






<
<



|



>
>
>
>
|
>
>
>
>
|


164
165
166
167
168
169
170
171
172
173
174
175
176


177
178
179
180
181
182
183
...
207
208
209
210
211
212
213
214
215
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
...
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
...
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
...
831
832
833
834
835
836
837




838
839
840
841
842
843
844
845
846


847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
subproofs(induction(_,_,Proof),             [Proof]).
subproofs(ih(Proof),                        [Proof]).
subproofs(generic(Proof),                   [Proof]).
subproofs(instan(_,Proof),                  [Proof]).
subproofs(product(Proofs),                  Proofs).
subproofs(choice(_,Proof),                  [Proof]).
subproofs(implies(Proof),                   [Proof]).
subproofs(backchain(_,Proof),               [Proof]).

% All cases have a list of proofs (although in most cases the list has
% a single element.)
subproofs(case(_,_,_,Proofs),               Proofs).




% replace_subproofs(Proof,Subproofs,NewProof)
% Replace the subproofs in a proof() object.
replace_subproofs(trivial,[],trivial) :- !.
replace_subproofs(hole,[],hole) :- !.
replace_subproofs(unify(A,B),[],unify(A,B)) :- !.
replace_subproofs(ctxmem(N),[],ctxmem(N)) :- !.
................................................................................
% elaborate atomic goals, `forall`s, or `exists`s.

% A path is a list of directions through a proof tree. A direction is just an
% index into the list of subproofs (generated by subproofs/2) of a proof. 
elaborate(Program,Tree,Path,What,Data,NewTree) :-

    % Fill in the target node with its elaboration
    elaborate_h(Program,Tree,Path,What,Data,NewTree),

    % The elaboration leaves the  arguments to proof(), other than the 
    % 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_h(Program,Proof,[],What,Data,EProof) :-
    Proof = proof(Goal,Ctx,_,_),
    elaborate_node(Program,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_h(Program,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_h(Program,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
................................................................................

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


% proof_complete(Proof)
% A proof is complete only if it contains no holes.
proof_complete(proof(_,_,_,Proof)) :- proof_complete_h(Proof).
proof_complete_h(trivial).
proof_complete_h(ctxmem(_)).
proof_complete_h(unify(_,_)).
proof_complete_h(case(false_left,_,_,[])).
proof_complete_h(induction(_,_,Proof)) :- proof_complete(Proof).
proof_complete_h(ih(Proof)) :- proof_complete(Proof).
proof_complete_h(generic(Proof)) :- proof_complete(Proof).
proof_complete_h(instan(_,Proof)) :- proof_complete(Proof).
proof_complete_h(product(Proofs)) :- maplist(proof_complete,Proofs).
proof_complete_h(choice(_,Proof)) :- proof_complete(Proof).
proof_complete_h(implies(Proof)) :- proof_complete(Proof).
proof_complete_h(backchain(_,Proof)) :- proof_complete(Proof).
proof_complete_h(case(and_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete_h(case(or_left,_,_,Proofs)) :- maplist(proof_complete,Proofs).
proof_complete_h(case(forall_left(_),_,_,[Proof])) :- proof_complete(Proof).
proof_complete_h(case(exists_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete_h(case(unify_left,_,_,[Proof])) :- proof_complete(Proof).

proof_complete_h(case(goal_left,_,_,Proofs)) :- maplist(proof_complete,Proofs).

%%% ---------------------------------------------------------------------------

% Just check a proof (since it contains the goal)
check(Program,Proof) :-
  Proof = proof(Goal,_,_,_),
  check(Program,Goal,Proof).
................................................................................
    Rule = rule(Name,Head,Body),

    % From here on out it's very similar to backchaining on a normal goal
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % "Call" (expand) the Goal in the program consisting only of the IH
    program:call_goal([Rule],V2,Goal,Clause),
    Clause = [clause(_,Sub1,Expansion)],

    Proof = proof(Expansion,_,_,_),

    get_vars(Expansion,V3),
    union(V2,V3,V4),

    % Prove recursively on the expansion
    check(Program,
          state(V4,Ctx,Expansion),
          VOut,
          Proof),

    % TODO: do we need to merge Sub1 and Sub2 like this?
    Proof = proof(_,_,Sub2,_),
    subst:merge(Sub1,Sub2,Subst).

% generic
% Prove a forall generically, by introducing a new constant.
check(Program,
      state(Vars,Ctx,forall(V,Goal)),
      VOut,
      proof(forall(V,Goal),Ctx,NewSubst,generic(Proof))) :-
................................................................................

    % Expand the clause 
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    program:call_goal(Program,V2,Premise,Clauses),





    % Generate a subproof for each clause
    length(Clauses,L),
    length(Proofs,L),

    maplist(check_case_clause(Program,state(Vars,Ctx2,Goal)),
            Clauses,
            _,
            Proofs).



% Check a subproof of the individual clauses
check_case_clause(Program,
                  state(Vars,Ctx,Goal),
                  clause(_,Subst,Clause),
                  VOut,
                  Proof) :-

    % For each clause/subproof, we have to apply the clause's substitution to
    % both the context and the goal.
    % It *should* be safe to reapply the Subst to Clause, as substitutions
    % application should be idempotent...
    apply_subst(Subst,[Clause|Ctx],NewCtx),
    exclude(==(true),NewCtx,NewCtx2), % No need to store true in the Ctx
    apply_subst(Subst,Goal,NewGoal),

    % Recursively check subproof
    check(Program,state(Vars,NewCtx2,NewGoal),VOut,Proof).


Changes to plsrc/program.pl.

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
% into P because by the time this is called P has already been processed.
normalize1(and([]),true) :- !.
normalize1(or([]),false) :- !.
normalize1(and([P]),P) :- !.
normalize1(or([P]),P) :- !.
normalize1(and(Ps),and(Ps)).
normalize1(or(Ps),or(Ps)).




% TODO: call_goal should be able to handle goals whose bodies aren't
% and([]). I.e., a single atomic goal, or true, should work fine.


% call_goal
% Generate the expansion of Goal, given the current set of bound variables.
% An expansion will have the form:
%   or([
%     and([v1 = t1, v2 = t2, ..., G1, G2, ...]),
%     and([v1 = t1, v2 = t2, ..., G1, G2, ...]),
%   ])
% Each and() corresponds to a clause in the definition of Goal. 
% - Note that we don't worry about any existing substitution at this point. If 
% needed, it can be applied to the expansion. 


% - Note that BVars *must* include any variables in Goal!
call_goal(Program,BVars,Goal,Expansion) :-
    call_goal_h(Program,BVars,Goal,Unnormalized),
    normalize(Unnormalized,Expansion).

call_goal_h(Program,BVars,Goal,or(Clauses)) :-
    % For inductive goals we split out the base goal, call it, and then
    % re-apply the smaller inductive size to the resulting subgoals.
    inductive(Goal,Base,Size), !,
    call_goal_h(Program,BVars,Base,NIClauses),
    inductive_shrink(Size,NewSize),
    maplist(inductify_subgoals(NewSize),NIClauses,Clauses).

% To call a normal goal, just get its definition and then call each clause.
call_goal_h(Program,BVars,Goal,Clauses) :-
    % Get all matching clauses (based on functor and arity only).
    % Defs will be a list of rule()s
    get_defs(Program,Goal,Defs),

................................................................................
    ( Defs = [] ->
        % We have to explicitly fail here, as call_clauses won't
        fail
    ;
        % Collect the results of "calling" all the clauses.
        call_clauses(BVars,Goal,Defs,Clauses)
    ).








% Note that if a given call fails (i.e., due to not unifying with the
% head of its clause) it is skipped rather than causing the entire
% collection to fail.
call_clauses(_,_,[],[]).
call_clauses(BVars,Goal,[D|Ds],[C|Cs]) :-
    call_clause(BVars,Goal,D,C), !,







>
>
>








|
|
|
|
|
|
|
>
>



|

|





|







 







>
>
>
>
>
>
>







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
% into P because by the time this is called P has already been processed.
normalize1(and([]),true) :- !.
normalize1(or([]),false) :- !.
normalize1(and([P]),P) :- !.
normalize1(or([P]),P) :- !.
normalize1(and(Ps),and(Ps)).
normalize1(or(Ps),or(Ps)).

normalize_clause(clause(Name,Subst,Body),clause(Name,Subst,NewBody)) :-
    normalize(Body,NewBody).

% TODO: call_goal should be able to handle goals whose bodies aren't
% and([]). I.e., a single atomic goal, or true, should work fine.


% call_goal
% Generate the expansion of Goal, given the current set of bound variables.
% An expansion will have the form:
%   [
%     clause(Name,Subst,and([G1, G2, ...]))
%     clause(Name,Subst,and([G1, G2, ...]),
%   ]
% Each and() corresponds to a clause in the definition of Goal. The collection
% of clauses is the disjunction of all the clauses that could unify with Goal,
% while the Substitution of each is the substitution that would result from
% the unification (note that this substitution has already been applied to the
% body of each clause).
% - Note that BVars *must* include any variables in Goal!
call_goal(Program,BVars,Goal,Expansion) :-
    call_goal_h(Program,BVars,Goal,Unnormalized),
    maplist(normalize_clause,Unnormalized,Expansion).

call_goal_h(Program,BVars,Goal,Clauses) :-
    % For inductive goals we split out the base goal, call it, and then
    % re-apply the smaller inductive size to the resulting subgoals.
    inductive(Goal,Base,Size), !,
    call_goal_h(Program,BVars,Base,NIClauses),
    inductive_shrink(Size,NewSize),
    maplist(inductify_clause(NewSize),NIClauses,Clauses).

% To call a normal goal, just get its definition and then call each clause.
call_goal_h(Program,BVars,Goal,Clauses) :-
    % Get all matching clauses (based on functor and arity only).
    % Defs will be a list of rule()s
    get_defs(Program,Goal,Defs),

................................................................................
    ( Defs = [] ->
        % We have to explicitly fail here, as call_clauses won't
        fail
    ;
        % Collect the results of "calling" all the clauses.
        call_clauses(BVars,Goal,Defs,Clauses)
    ).

% Helper to change the inductive size on all subgoals of a clause.
inductify_clause(Size,
                 clause(Name,Subst,Clauses),
                 clause(Name,Subst,NewClauses)) :-
    
    inductify_subgoals(Size,Clauses,NewClauses).

% Note that if a given call fails (i.e., due to not unifying with the
% head of its clause) it is skipped rather than causing the entire
% collection to fail.
call_clauses(_,_,[],[]).
call_clauses(BVars,Goal,[D|Ds],[C|Cs]) :-
    call_clause(BVars,Goal,D,C), !,