Check-in [b1dff5705c]

Not logged in

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

Overview
Comment:Added an exposed predicate for checking proofs (just checking, no elaboration).
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:b1dff5705c938bb34093ea74fe0e1e0921fc6eec
User & Date: andy 2015-04-18 18:45:52
Context
2015-04-18
18:46
Fixed tests to support the new definition of atoms (can be constructed from numbers). check-in: 51ec69316b user: andy tags: trunk
18:45
Added an exposed predicate for checking proofs (just checking, no elaboration). check-in: b1dff5705c user: andy tags: trunk
18:45
Fixed a bug in the checker, context was not being initialized to [] which made goals succeed once and then enter an infinite loop. check-in: f931058aa9 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to apps/passist/passist.pl.

1
2
3
4
5
6
7

8
9
10
11
12
13
14
..
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/5,
    complete/1,
    get_spec/1
]).

:- use_module(library(term_to_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).







>







 







>
>
>
>








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
..
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
%%%
%%% passist.pl
%%% Proof assistant/checker application for Pengines
%%%

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

:- use_module(library(term_to_json)).

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

check(Proof) :-
    spec(Program),
    checker:check(Program,Proof).

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