Check-in [afb3b37674]

Not logged in

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

Overview
Comment:Fixed a bug in case analysis of atomic goals.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:afb3b37674cd0a42c8c74b85e62c9d71d8651bb2
User & Date: andy 2015-04-15 19:42:19
Context
2015-04-15
19:43
Fixed a couple bugs in the handling of non-string atoms (coerce to string). check-in: 808229ea10 user: andy tags: trunk
19:42
Fixed a bug in case analysis of atomic goals. check-in: afb3b37674 user: andy tags: trunk
14:32
Fixed module declarations/imports for the new argument pattern for `elaborate`. check-in: 207908bad1 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
...
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
...
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
...
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
...
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
% Succeeds if Proof is a structurally-valid proof. We mostly use this for 
% elaborating partial proofs by replacing a `hole` with a variable and then
% asking how it could succeed.
proof(trivial).
proof(hole).
proof(unify(_,_)).
proof(ctxmem(_)).
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).
................................................................................
% subproofs(proof,Subproofs)
% Given a proof object, output the list of its subproofs. (children, not 
% descendants).
subproofs(trivial,                          []).
subproofs(hole,                             []).
subproofs(unify(_,_),                       []).
subproofs(ctxmem(_),                        []).
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]).
................................................................................
    % 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,hole),
    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)) :-
................................................................................

% 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).
................................................................................
    program:call_goal(Program,V2,Clause,Expansion),

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

    % Create the new context
    append(Expansion,Ctx2,NewCtx),

    % Recursively check in the new context
    check(Program,
          state(NewVars,NewCtx,Goal),
          VOut,Proof),
    sub(Proof,Subst).











|







 







|







 







|







 







|







 







|










131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
...
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
...
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
...
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
...
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
% Succeeds if Proof is a structurally-valid proof. We mostly use this for 
% elaborating partial proofs by replacing a `hole` with a variable and then
% asking how it could succeed.
proof(trivial).
proof(hole).
proof(unify(_,_)).
proof(ctxmem(_)).
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).
................................................................................
% subproofs(proof,Subproofs)
% Given a proof object, output the list of its subproofs. (children, not 
% descendants).
subproofs(trivial,                          []).
subproofs(hole,                             []).
subproofs(unify(_,_),                       []).
subproofs(ctxmem(_),                        []).
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]).
................................................................................
    % 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)) :-
................................................................................

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