Check-in [9e954b6b56]

Not logged in

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

Overview
Comment:Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:9e954b6b563442641afe3b37eed78150cbc296ce
User & Date: andy 2015-04-15 11:47:37
Context
2015-04-15
11:48
Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself. check-in: f84190c56c user: andy tags: trunk
11:47
Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk
11:44
Added screen shot of the proof assistant, starting a proof. check-in: caa7fbdd73 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to apps/passist/passist.pl.

2
3
4
5
6
7
8
9

10
11
12
13
14
15
16





17
18
19
20
21
22
23
24
25


26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
%%% passist.pl
%%% Proof assistant/checker application for Pengines
%%%

:- module(passist, [
    check/2,
    elaborate/4,
    complete/1

]).

:- use_module(library(term_to_json)).

% Load the interpreter and the Nat specification
:- use_module(plsrc(checker)).
:- use_module(plsrc(nat_spec_demo)).






% Initial proof state for the demo. This sets up the initial proof for the
% Goal with the induction done and ->R done. 
demo_proof(Proof) :-

    Proof = proof((nat(' x') -> add(' x', z, ' x')),[],Subst,
        induction(0,('nat\\sml'(' x')->add(' x', z, ' x')),
            proof(('nat\\big'(' x')->add(' x', z, ' x')),[],Subst,
                implies(proof(add(' x', z, ' x'),['nat\\big'(' x')],Subst,hole))))).



% check(Statement,Proof)
% Check the statement against the Proof
check(Statement,JSON) :-
    spec(Program),
    check(Program,Statement,Proof),
    term_to_json(Proof,JSON).

% elaborate(Proof,Path,What,Result)
% Elaborate a hole into a 1-level subproof.
elaborate(Proof,Path,What,JSON) :-
    spec(Program),
    elaborate(Program,Proof,Path,What,Result),
    term_to_json(Result,JSON).

complete(Proof) :- checker:complete(Proof).







|
>







>
>
>
>
>



|

|

|
|
>
>










|

|


|
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
%%% passist.pl
%%% Proof assistant/checker application for Pengines
%%%

:- module(passist, [
    check/2,
    elaborate/4,
    complete/1,
    get_spec/1
]).

:- use_module(library(term_to_json)).

% Load the interpreter and the Nat specification
:- use_module(plsrc(checker)).
:- use_module(plsrc(nat_spec_demo)).

% Get the current specification
get_spec(JSON) :-
    spec(Program),
    term_to_json(Program,JSON).

% Initial proof state for the demo. This sets up the initial proof for the
% Goal with the induction done and ->R done. 
demo_proof(JSON) :-

    Proof = proof((nat(' x') -> add(' x', z, ' x')),[],_,
        induction(0,('nat\\sml'(' x')->add(' x', z, ' x')),
            proof(('nat\\big'(' x')->add(' x', z, ' x')),[],_,
                implies(proof(add(' x', z, ' x'),['nat\\big'(' x')],_,hole))))),

    term_to_json(Proof,JSON).

% check(Statement,Proof)
% Check the statement against the Proof
check(Statement,JSON) :-
    spec(Program),
    check(Program,Statement,Proof),
    term_to_json(Proof,JSON).

% elaborate(Proof,Path,What,Result)
% Elaborate a hole into a 1-level subproof.
elaborate(Proof,Path,What,Data,JSON) :-
    spec(Program),
    elaborate(Program,Proof,Path,What,Data,Result),
    term_to_json(Result,JSON).

complete(Proof) :- proof_complete(Proof).

Changes to plsrc/checker.pl.

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
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
% everything we need in the nodes of the tree). This is because an incomplete
% proof is essentially a suspended recursion. The most important thing we need
% to rebuild is the set of variables in scope. Without it, we cannot 
% 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,NewTree) :-

    % Fill in the target node with its elaboration
    elaborate(Tree,Path,What,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,EProof) :-
    Proof = proof(Goal,Ctx,Subst,hole),
    elaborate_node(Goal,Ctx,What,Elaboration),
    EProof = proof(Goal,Ctx,Subst,Elaboration).


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

    % Find the Nth subproof and recurse down it
    subproofs(Proof,Subproofs),
    nth0(N,Subproofs,Branch),
    elaborate(Branch,Ns,What,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,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(N)`
elaborate_node(true,        _, goal,  trivial).
elaborate_node(_ = _,       _, goal,  unify(_,_)).
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,  choice(_,proof(_,_,_,hole))).





elaborate_node(Goal,        _, goal,  backchain(proof(_,_,_,hole))) :-
    is_user_goal(Goal).


elaborate_node(_, Ctx, ctx(N), case(Type,N,false,Elaboration)) :-
    nth0(N,Ctx,Premise),
    elaborate_ctx(Premise,Type,Elaboration).


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







|


|








|

|




|





|





|


|
|
|
|
|
|
|

>
|

>
>
>
>
|


>
|



>







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
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
% everything we need in the nodes of the tree). This is because an incomplete
% proof is essentially a suspended recursion. The most important thing we need
% to rebuild is the set of variables in scope. Without it, we cannot 
% 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,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)) :-

    % 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_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(_,_),  unify_left,     [proof(_,_,_,hole)]).
elaborate_ctx(G,           goal_left,      [proof(_,_,_,hole)]) :-
    is_user_goal(G).