Check-in [4e6407ce10]

Not logged in

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

Overview
Comment:Updated checker module to work with the new atomic goal expansions.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst
Files: files | file ages | folders
SHA1:4e6407ce10dd60bc26dc1892af8da8aadd1ac4ab
User & Date: andy 2015-04-20 20:58:11
Context
2015-04-21
15:45
Fixed a bug in the translation of Uppercase atoms from Prolog. check-in: 223107a48f user: andy tags: bc-subst
2015-04-20
20:58
Updated checker module to work with the new atomic goal expansions. check-in: 4e6407ce10 user: andy tags: bc-subst
20:57
Fixed (maybe) the filtering of substitutions for "interesting" variables. check-in: abb4d08745 user: andy tags: bc-subst
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
...
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
...
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
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
...
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
...
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
...
589
590
591
592
593
594
595
596
597
598
599
600
601
602

603
604

605
606
607
608
609
610
611
612
613
614
...
679
680
681
682
683
684
685




686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703

704
705
706
707
708
709
710
711
712
...
780
781
782
783
784
785
786




787
788
789
790

791
792
793
794
795
796
797
798
799

800
801
802
803
804
805
806
807


808
809








810
811

812
813
814


815
816
817
proof(induction(_,_,Proof)) :- proof(Proof).
proof(ih(Proof)) :- proof(Proof).
proof(generic(Proof)) :- proof(Proof).
proof(instan(_,Proof)) :- proof(Proof).
proof(product(Proofs)) :- maplist(proof,Proofs).
proof(choice(_,Proof)) :- proof(Proof).
proof(implies(Proof)) :- proof(Proof).
proof(backchain(Proof)) :- proof(Proof).
proof(case(false_left,_,_,[])).
proof(case(and_left,_,_,[Proof])) :- proof(Proof).
proof(case(or_left,_,_,Proofs)) :- maplist(proof,Proofs).
proof(case(forall_left(_),_,_,[Proof])) :- proof(Proof).
proof(case(exists_left,_,_,[Proof])) :- proof(Proof).
proof(case(unify_left,_,_,[Proof])) :- proof(Proof).
proof(case(goal_left,_,_,[Proof])) :- proof(Proof).
................................................................................
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]). 
................................................................................
% 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(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(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_node(_,           _, goal,asm,ctxmem(_)).
elaborate_node(_ -> _,      _, goal,_,  implies(proof(_,_,_,hole))).
elaborate_node(forall(_,_), _, goal,_,  generic(proof(_,_,_,hole))).
elaborate_node(exists(_,_), _, goal,_,  instan(_,proof(_,_,_,hole))).
elaborate_node(and(Ps),     _, goal,_,  product(Holes)) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).

elaborate_node(or(_),       _, goal,N,  choice(N,proof(_,_,_,hole))).

% User goals can be elaborated by expansion, or by induction (in some cases)
% The Data argument specifies which, either `bc` or `ind`.
elaborate_node(Goal,        _, goal,bc,  backchain(proof(_,_,_,hole))) :-
    is_user_goal(Goal).
elaborate_node(Goal,        _, goal,ind, ih(proof(_,_,_,hole))) :-
    is_user_goal(Goal).

% Elaboration of antecedants into cases.
elaborate_node(_,           Ctx,ctx,N,  case(Type,N,false,Elaboration)) :-
    nth0(N,Ctx,Premise),







    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).


% proof_complete(Proof)
% A proof is complete only if it contains no holes.
................................................................................
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).

................................................................................
% Note that false is not always a failure! If false is a member of the 
% context the proof may succeed.

% Checking of user goals
check(Program,
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,backchain(SubProof))) :-
    
    is_user_goal(Goal),

    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % Note that because call_goal only generates the expansion, we don't need
    % to worry about looking for subgoals in the context; that can happen later 
    % via the assumption rule.
    program:call_goal(Program, V2, Goal, Expansion),

    % Add variables from the expansion to the set of bound vars
    get_vars(Expansion,V3),
    union(V2,V3,NewVars),

    % Check the expansion against its proof.
    check(Program,
          state(NewVars,Ctx,Expansion),





          VOut,
          SubProof),


    % We have to extract the substitution from the subproof
    sub(SubProof,Subst).







% Conjunctions:
% -- The empty conjunction is equivalent to true.
% -- A non-empty conjunction runs the head, collecting its results
%    (substituion, proof). The substitution is applied to the remainder of the
%    conjunction's goals, while the proof is collected into the product.
................................................................................
% 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,
................................................................................
    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, 
           Subst) :-

    % Get the new context and the target element (must an an or())
    keep_rest(N,Ctx,Keep,or(Ds),Ctx2),

    % For each disjunct, generate a new context and prove the Goal in it
    maplist(check_or_left(Program,Vars,Goal,Ctx2),Ds,VOuts,Proofs),

    % Flatten the list of VOuts into a set
    % TODO: Is this necessary?
    flatten(VOuts,VOutList),
    list_to_set(VOutList,VOut),

    % Merge all the resulting substitutions

    maplist(sub,Proofs,Substs),
    foldl(subst:merge,Substs,[],Subst).

% Helper predicate for checking a single disjunct.
check_or_left(Program,Vars,Goal,BaseCtx,
              Disjunct,
              VOut,
              Proof) :-
    
................................................................................

    % Recursively prove. Note that we *do not* change the outer substitution.
    check(Program,state(Vars,NewCtx,NewGoal),VOut,Proof),
    sub(Proof,Subst).

% goal_left
% Expand a user goal into the context.




check_case(case(goal_left,N,Keep,[Proof]),
           Program,
           state(Vars,Ctx,Goal),
           VOut,

           Subst) :-

    % Get the new context and target element (must be a user goal)
    keep_rest(N,Ctx,Keep,Clause,Ctx2),    
    is_user_goal(Clause),

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

    program:call_goal(Program,V2,Clause,Expansion),

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

    % Create the new context
    NewCtx = [Expansion|Ctx2],



    % Recursively check in the new context








    check(Program,
          state(NewVars,NewCtx,Goal),

          VOut,Proof),
    sub(Proof,Subst).













|







 







|







 







|








|

|





<
|






|









|
|
|
|
|
|
|


|



|

|



|

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







|
|







 







|







 







|









|


|


<
<
|
>
>
>
>
>
|
<
>

<
<
>
>
>
>
>







 







|





|
>

<
>


|







 







>
>
>
>




|










|


>
|
|







 







>
>
>
>
|


<
>
|


|
|




>
|


|
|

<
|
>
>

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

>
>


<
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
...
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
...
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
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
304
...
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
...
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
390
391
392
393
...
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626

627
628
629
630
631
632
633
634
635
636
637
...
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
...
808
809
810
811
812
813
814
815
816
817
818
819
820
821

822
823
824
825
826
827
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

proof(induction(_,_,Proof)) :- proof(Proof).
proof(ih(Proof)) :- proof(Proof).
proof(generic(Proof)) :- proof(Proof).
proof(instan(_,Proof)) :- proof(Proof).
proof(product(Proofs)) :- maplist(proof,Proofs).
proof(choice(_,Proof)) :- proof(Proof).
proof(implies(Proof)) :- proof(Proof).
proof(backchain(_,Proof)) :- proof(Proof).
proof(case(false_left,_,_,[])).
proof(case(and_left,_,_,[Proof])) :- proof(Proof).
proof(case(or_left,_,_,Proofs)) :- maplist(proof,Proofs).
proof(case(forall_left(_),_,_,[Proof])) :- proof(Proof).
proof(case(exists_left,_,_,[Proof])) :- proof(Proof).
proof(case(unify_left,_,_,[Proof])) :- proof(Proof).
proof(case(goal_left,_,_,[Proof])) :- proof(Proof).
................................................................................
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]). 
................................................................................
% 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
% 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_node(_,_,           _, goal,asm,ctxmem(_)).
elaborate_node(_,_ -> _,      _, goal,_,  implies(proof(_,_,_,hole))).
elaborate_node(_,forall(_,_), _, goal,_,  generic(proof(_,_,_,hole))).
elaborate_node(_,exists(_,_), _, goal,_,  instan(_,proof(_,_,_,hole))).
elaborate_node(_,and(Ps),     _, goal,_,  product(Holes)) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).

elaborate_node(_,or(_),       _, goal,N,  choice(N,proof(_,_,_,hole))).

% User goals can be elaborated by expansion, or by induction (in some cases)
% The Data argument specifies which, either `bc` or `ind`.
elaborate_node(_,Goal,        _, goal,bc,  backchain(_,proof(_,_,_,hole))) :-
    is_user_goal(Goal).
elaborate_node(_,Goal,        _, goal,ind, ih(proof(_,_,_,hole))) :-
    is_user_goal(Goal).

% Elaboration of antecedants into cases.
elaborate_node(P,_,           Ctx,ctx,N,  case(Type,N,false,Elaboration)) :-
    nth0(N,Ctx,Premise),

    % We have to do some extra work when elaborating atomic goals on the left:
    % lookup the goal and figure out how many clauses unify with the call, so
    % that we know how many branches (subproofs) to generate.
    (Type = goal_left ->
        elaborate_left_goal(P,Premise,Elaboration)
    ;
        elaborate_ctx(Premise,Type,Elaboration)
    ).

% Elaborate a call to an atomic goal in the context, by expanding it to N 
% subproofs (where N is the number of clauses whose heads can unify with the 
% goal.)
elaborate_left_goal(Program,Goal,Elaboration) :-
    is_user_goal(Goal),
    call_goal(Program,[],Goal,Clauses),
    length(Clauses,N),
    fill(Elaboration,proof(_,_,_,hole),N).

% 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).


% proof_complete(Proof)
% A proof is complete only if it contains no holes.
................................................................................
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).

................................................................................
% Note that false is not always a failure! If false is a member of the 
% context the proof may succeed.

% Checking of user goals
check(Program,
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,backchain(Name,SubProof))) :-
    
    is_user_goal(Goal),

    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % Note that because call_goal only generates the expansion, we don't need
    % to worry about looking for subgoals in the context; that can happen later 
    % via the assumption rule.
    program:call_goal(Program, V2, Goal, Clauses),

    % Add variables from the expansion to the set of bound vars
    get_vars(Clauses,V3),
    union(V2,V3,NewVars),



    check_clauses(Program,Clauses,state(NewVars,Ctx,Goal),
                  VOut,proof(_,_,Subst,backchain(Name,SubProof))).


% Check each clause in the expansion of the goal, 
check_clauses(Program,Clauses,state(Vars,Ctx,Goal),
              VOut,

              proof(Goal,Ctx,Subst,backchain(Name,Proof))) :-



    % For each clause in the expansion...
    member(clause(Name,Subst,Expansion), Clauses),

    % Check it 
    check(Program,state(Vars,Ctx,Expansion),VOut,Proof).


% Conjunctions:
% -- The empty conjunction is equivalent to true.
% -- A non-empty conjunction runs the head, collecting its results
%    (substituion, proof). The substitution is applied to the remainder of the
%    conjunction's goals, while the proof is collected into the product.
................................................................................
% 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,Subst,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.
    % If they unify, succeed and output the substitution.
    nth0(Index,Ctx,Goal2),

    get_subst(Goal,Goal2,Subst).

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

    nonvar(Hole),
    Hole = hole,
................................................................................
    check(Program,
          state(Vars,NewCtx,Goal),
          VOut,
          Proof).

% or_left
% Generate a sub-proof for every branch of the disjunction. 
% Note that this, like the goal-left case, returns an empty substitution. This
% is entirely correct; the subproofs of a disjunction-like construct in the
% context are real, independent subproofs, whose substitutions do not influence
% the parent proof at all. 
check_case(case(or_left,N,Keep,Proofs),
           Program,
           state(Vars,Ctx,Goal),
           VOut, 
           []) :-

    % Get the new context and the target element (must an an or())
    keep_rest(N,Ctx,Keep,or(Ds),Ctx2),

    % For each disjunct, generate a new context and prove the Goal in it
    maplist(check_or_left(Program,Vars,Goal,Ctx2),Ds,VOuts,Proofs),

    % Flatten the list of VOuts into a set
    % TODO: Is this necessary?
    flatten(VOuts,VOutList),
    list_to_set(VOutList,VOut).

    % Merge all the resulting substitutions
    % TODO: is this correct? I think not. But then what should subst be?
    %maplist(sub,Proofs,Substs),
    %foldl(subst:merge,Substs,[],Subst)

% Helper predicate for checking a single disjunct.
check_or_left(Program,Vars,Goal,BaseCtx,
              Disjunct,
              VOut,
              Proof) :-
    
................................................................................

    % Recursively prove. Note that we *do not* change the outer substitution.
    check(Program,state(Vars,NewCtx,NewGoal),VOut,Proof),
    sub(Proof,Subst).

% goal_left
% Expand a user goal into the context.
% Note that this, like the or-left case, returns an empty substitution. This
% is entirely correct; the subproofs of a disjunction-like construct in the
% context are real, independent subproofs, whose substitutions do not influence
% the parent proof at all. 
check_case(case(goal_left,N,Keep,Proofs),
           Program,
           state(Vars,Ctx,Goal),

           [],
           []) :-

    % Get the new context and target element (must be a user goal)
    keep_rest(N,Ctx,Keep,Premise,Ctx2),    
    is_user_goal(Premise),

    % 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).