Check-in [f931058aa9]

Not logged in

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 2015-04-18 18:45:12
Context
2015-04-18
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
16:44
Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

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.