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 Side-by-Side Diffs Ignore Whitespace Patch

Changes to apps/passist/passist.pl.

     1      1   %%%
     2      2   %%% passist.pl
     3      3   %%% Proof assistant/checker application for Pengines
     4      4   %%%
     5      5   
     6      6   :- module(passist, [
     7      7       check/2,
            8  +    check/1,
     8      9       elaborate/5,
     9     10       complete/1,
    10     11       get_spec/1
    11     12   ]).
    12     13   
    13     14   :- use_module(library(term_to_json)).
    14     15   
................................................................................
    35     36   % check(Statement,Proof)
    36     37   % Check the statement against the Proof
    37     38   check(Statement,JSON) :-
    38     39       spec(Program),
    39     40       check(Program,Statement,Proof),
    40     41       term_to_json(Proof,JSON).
    41     42   
           43  +check(Proof) :-
           44  +    spec(Program),
           45  +    checker:check(Program,Proof).
           46  +
    42     47   % elaborate(Proof,Path,What,Result)
    43     48   % Elaborate a hole into a 1-level subproof.
    44     49   elaborate(Proof,Path,What,Data,JSON) :-
    45     50       spec(Program),
    46     51       elaborate(Program,Proof,Path,What,Data,Result),
    47     52       term_to_json(Result,JSON).
    48     53   
    49     54   complete(Proof) :- proof_complete(Proof).