Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
Overview
Comment:  Fixed a bug in the checker, context was not being initialized to [] which made goals succeed once and then enter an infinite loop. 

Downloads:  Tarball  ZIP archive  SQL archive 
Timelines:  family  ancestors  descendants  both  trunk 
Files:  files  file ages  folders 
SHA1:  f931058aa9b95fc2c019d12d68629d1026ad99ba 
User & Date:  andy 20150418 18:45:12 
Context
20150418
 
18:45  Added an exposed predicate for checking proofs (just checking, no elaboration). checkin: 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. checkin: f931058aa9 user: andy tags: trunk  
16:44  Fixed a bug in proofs that involve backchaining on the IH. checkin: c4c963bcde user: andy tags: trunk  
Changes
Changes to plsrc/checker.pl.
301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 
proof_complete(case(forall_left(_),_,_,[Proof])) : proof_complete(Proof).
proof_complete(case(exists_left,_,_,[Proof])) : proof_complete(Proof).
proof_complete(case(unify_left,_,_,[Proof])) : proof_complete(Proof).
proof_complete(case(goal_left,_,_,[Proof])) : proof_complete(Proof).
%%% 
check(Program,Proof) :
Proof = proof(Goal,_,_,_),
check(Program,Goal,Proof).
% check(Program, Goal, Proof)
% Check the Proof of Goal, in Program.
check(Program,Goal,proof(Goal,Ctx,Subst,Proof)) :
get_vars(Goal,Vars),
% Ctx = [],
check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)).
% check(Program,State,VOut,Proof)
%  State = state(Vars,Ctx,Goal)
%  Proof = proof(Goal,Ctx,Subst,Proof)
% and Proof has one of the forms mentioned above.

> > > > >  < 
301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 
proof_complete(case(forall_left(_),_,_,[Proof])) : proof_complete(Proof). proof_complete(case(exists_left,_,_,[Proof])) : proof_complete(Proof). proof_complete(case(unify_left,_,_,[Proof])) : proof_complete(Proof). proof_complete(case(goal_left,_,_,[Proof])) : proof_complete(Proof). %%%  % Just check a proof (since it contains the goal) check(Program,Proof) : Proof = proof(Goal,_,_,_), check(Program,Goal,Proof). % check(Program, Goal, Proof) % Check the Proof of Goal, in Program. check(Program,Goal,Proof) : check_with_ctx(Program,Goal,[],Proof). % Check a goal with a given context. Normally the initial context is empty. check_with_ctx(Program,Goal,Ctx,proof(Goal,Ctx,Subst,Proof)) : get_vars(Goal,Vars), check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)). % check(Program,State,VOut,Proof) %  State = state(Vars,Ctx,Goal) %  Proof = proof(Goal,Ctx,Subst,Proof) % and Proof has one of the forms mentioned above. 