Check-in [9e954b6b56]

Not logged in

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. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders 9e954b6b563442641afe3b37eed78150cbc296ce 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

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, foralls, or existss. % 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, foralls, or existss. % 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).