Check-in [3a093317cf]

Not logged in

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

Overview
Comment:Added `passist` Pengine application to the server. This runs the live demo of the proof assistant.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:3a093317cf4d94606b56297998bf1f7c7b7e3667
User & Date: andy 2015-04-14 20:21:28
Context
2015-04-14
20:21
Added a specialized version of the nat specification, for demonstration purposes. check-in: 4a035bbfc0 user: andy tags: trunk
20:21
Added `passist` Pengine application to the server. This runs the live demo of the proof assistant. check-in: 3a093317cf user: andy tags: trunk
20:19
Changed the way the induction tactic handles repeated use (previous IHs are just ignored). check-in: c82ab7e9b6 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Show Whitespace Changes Patch

Added apps/passist/passist.pl.



















































































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

Changes to server.pl.

33
34
35
36
37
38
39
40
41
42
43



44
45
46
47
48
49
50

% This makes ./plsrc available so we can do things like
% use_module(plsrc(program)).
user:file_search_path(plsrc,ResPath) :-
    absolute_file_name('.',WD),
    atom_concat(WD,'/plsrc',ResPath).

% Install PEngine applications (repl, check)
:- pengine_application(repl).
:- use_module(repl:'./apps/repl/repl').




% This makes it so that all users are authenticated, and all authenticated users
% can run non-sandboxed code. 
pengines:not_sandboxed(_,_).
pengines:authentication_hook(_,_,user).

:- http_handler(root(src), serve_files_in_directory(src), [prefix]).
:- http_handler(root(res), serve_files_in_directory(res), [prefix]).







|



>
>
>







33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

% This makes ./plsrc available so we can do things like
% use_module(plsrc(program)).
user:file_search_path(plsrc,ResPath) :-
    absolute_file_name('.',WD),
    atom_concat(WD,'/plsrc',ResPath).

% Install PEngine applications (repl, passist)
:- pengine_application(repl).
:- use_module(repl:'./apps/repl/repl').

:- pengine_application(passist).
:- use_module(passist:'./apps/passist/passist').

% This makes it so that all users are authenticated, and all authenticated users
% can run non-sandboxed code. 
pengines:not_sandboxed(_,_).
pengines:authentication_hook(_,_,user).

:- http_handler(root(src), serve_files_in_directory(src), [prefix]).
:- http_handler(root(res), serve_files_in_directory(res), [prefix]).