Check-in [3a093317cf]

Not logged in

Overview
Comment: Added passist Pengine application to the server. This runs the live demo of the proof assistant. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders 3a093317cf4d94606b56297998bf1f7c7b7e3667 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

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