1:- module(cilog, [on_cilog_read/1,
2 3 op(1150, xfx, <- ),
4 5 6 op(1120, xfx, <= ),
7 8 op(950,xfy, &),
9 10 op(900,fy,~),
11 12 op(700,xfx,\=),
13
14 15 16 17 18 19 20 21 22 op(1170, fx, ask),
23 op(1170, fx, whynot),
24 op(1170, fx, how),
25 op(1170,fx,load),
26 op(1170,fx,prload),
27 op(1170,fx,bound),
28 op(1170,fx,stats),
29 30 op(1170,fx,clear),
31 op(1170,fx,askable),
32 op(1170,fx,assumable),
33 op(1170,fx,deterministic)]). 34
37
38cilog_version('0.14').
39
43
48
64get_runtime(T,U) :- catch((statistics(cputime,T),U=secs),_,
65 (statistics(runtime,[T,_]),U=ms)). 66
67
70mywhen(C,G) :-
71 C -> G
72 ; writeallonline(['Warning: ',C,' failing. Delaying not implemented.']),
73 fail.
74
77
78differ(X,Y) :- dif(X,Y). 80
81mywrite(T) :- write_term(T,[numbervars(true),portray(true)]). 82mywrite(T) :- write(T). 83
90
92:- op(1150, xfx, <- ). 95:- op(1120, xfx, <= ). 97:- op(950,xfy, &). 99:- op(900,fy,~). 101:- op(700,xfx,\=). 102
103:- op(1170, fx, tell). 104:- op(1170, fx, ask). 105:- op(1170, fx, whynot). 106:- op(1170, fx, how). 107:- op(1170,fx,load). 108:- op(1170,fx,prload). 109:- op(1170,fx,bound). 110:- op(1170,fx,stats). 111:- op(1170,fx,listing). 112:- op(1170,fx,clear). 113:- op(1170,fx,askable). 114:- op(1170,fx,assumable). 115:- op(1170,fx,deterministic). 116
117:- dynamic (<-)/2. 118:- dynamic failed/1. 119:- dynamic depth_bound/1. 120:- dynamic askabl/1. 121:- dynamic assumabl/1. 122:- dynamic asked/2. 123:- dynamic debugging_failure/0. 124:- dynamic answer_found/0. 125:- dynamic checking_runtime/0. 126:- dynamic lastruntime/1. 127:- dynamic deter/1. 128
129depth_bound(30).
130
134
135help_message(['
136CILOG Help','
137
138A clause is of the form','
139 Head <- Body','
140 Head','
141Head is an atom.','
142Body is an expression made up of','
143 Atom','
144 ~ B1 negation as finite failure','
145 B1 & B2 conjunction B1 and B2','
146where B1 and B2 are expressions.','
147 bagof(A,Q,L) true if L is the list of A''s where Q is true.','
148
149***** Basic commands:','
150
151tell CLAUSE. add the clause to the knowledge base','
152askable Atom. makes Atom askable.','
153assumable Atom. makes atom assumable.','
154
155ask QUERY. ask if expression QUERY is a consequence of the KB','
156whynot QUERY. find out why QEURY failed.','
157
158bound N. set search depth-bound to N (default=30)','
159listing. list all clauses in the knowledge base.','
160listing H. list clauses in the knowledge base with head H.','
161askables. list all askables.','
162assumables. list all assumables.','
163clear. clear the knowledge base','
164check. check the knowledge base for undefined predicates','
165clear H. clear clauses with head H from knowledge base','
166help. print this help message','
167stats runtime. give runtime statistics','
168quit. quit cilog','
169prolog. exit to Prolog. Type "start." to start cilog again.','
170
171***** Input/Output','
172
173load ''Filename''. load the clauses in file Filename','
174prload ''Filename''. load the clauses in Filename, using Prolog''s syntax.']).
175
176show_cilog_help:-
177 help_message(Help),
178 writeallonline(Help).
179
183
184interpret(help) :- !,
185 show_cilog_help.
186interpret(prolog) :- !,
187 writeallonline(['Returning to Prolog. Type "start." to start cilog.']),
188 prolog.
189interpret((tell _ :- _)) :- !,
190 writeallonline(['Illegal rule: ":-" is not a legal implication. Use "<-".']).
191interpret((tell C)) :- !,
192 tell_clause(C).
193
194interpret((ask Q)) :- !,
195 retractall(debugging_failure),
196 retractall(answer_found),
197 depth_bound(DB),
198 askq(Q,DB).
199
200interpret((whynot Q)) :- !,
201 depth_bound(DB),
202 whynotb(Q,DB,_,[],_).
203
204interpret((clear H)) :- !,
205 retractall((H <- _)),
206 retractall(assumabl(H)),
207 retractall(askabl(H)),
208 retractall(asked(H,_)).
209
210interpret((stats Cmd)) :- !,
211 stats_command(Cmd).
212
213interpret(clear) :- !,
214 interpret((clear _)).
215
216interpret((prload File)) :- !,
217 prolog_load(File).
218
219interpret((load File)) :- !,
220 ci_load(File).
221
222interpret((bound)) :- !,
223 depth_bound(N),
224 writeallonline(['Current depth bound is ',N]).
225
226interpret((bound N)) :- !,
227 (integer(N) ->
228 retract(depth_bound(_)),
229 asserta(depth_bound(N))
230 ; writeallonline(['Depth bound must be an integer'])).
231
232interpret(quit) :-
233 throw(quit).
234
235interpret(check) :- !,
236 check.
237
238interpret((askable G)) :- !,
239 assertz(askabl(G)).
240
241interpret((assumable G)) :- !,
242 assertz(assumabl(G)).
243
244interpret((deterministic G)) :- !,
245 assertz(deter(G)).
246
247interpret(askables) :-
248 askabl(G),
249 writeallonline(['askable ',G,'.']),
250 fail.
251interpret(askables) :- !.
252
253interpret(assumables) :-
254 assumabl(G),
255 writeallonline(['assumable ',G,'.']),
256 fail.
257interpret(assumables) :- !.
258
259interpret((listing)) :- !,
260 interpret((listing _)),
261 interpret(askables),
262 interpret(assumables).
263
264interpret((listing H)) :-
265 (H <- B),
266 (B = true
267 -> writeallonline([H,'.'])
268 ; writeallonline([H,' <- ',B,'.'])
269 ),
270 fail.
271interpret((listing _)) :- !.
272
273interpret((A <- B)) :- !,
274 writeallonline(['Illegal command, ',(A <- B),'. You have to "tell" a clause.']).
275
276interpret(C) :-
277 writeallonline(['Unknown Command, ',C,'. Type "help." for help.']).
278
279
283
284askq(Q,_) :-
285 illegal_body(Q,Why),!,
286 writeallonline(['Illegal query: '|Why]).
287askq(Q,DB) :-
288 retractall(failed(_)),
289 assert(failed(naturally)),
290 reset_runtime,
291 solve(Q,DB,Res,[wrule(yes,true,Q,true)],[],Ass),
292 (answer_found -> true ; assert(answer_found)),
294 report(Q,Res,Ass).
295askq(Q,_) :-
296 failed(naturally),!,
297 (answer_found
298 -> writeallonline(['No more answers.'])
299 ; writeallonline(['No. ',Q,' doesn''t follow from the knowledge base.'])),
300 report_runtime.
301askq(Q,DB) :- !,
302 ask_failing(Q,DB).
303
304ask_failing(Q,DB) :-
305 writeallonline(['Query failed due to depth-bound ',DB,'.']),
306 report_runtime,
307 writel([' [New-depth-bound,where,ok,help]: ']),
308 flush_and_read(Comm),
309 interpret_failing_question(Comm,Q,DB).
310
312interpret_failing_question(help,Q,DB) :- !,
313 writeallonline([
314 ' Give one of the following commands:',nl,
315 ' an integer > ',DB,' to use this depth bound.',nl,
316 ' (use "bound N." to set it permanently).',nl,
317 ' where. to explore the proof tree where the depth-bound was reached.',nl,
318 ' ok. to return to the cilog prompt.',nl,
319 ' help. to print this message.']),
320 ask_failing(Q,DB).
321interpret_failing_question(end_of_file,_,_) :- !.
322interpret_failing_question(ok,_,_) :- !.
323interpret_failing_question(where,Q,DB) :-
324 assert(debugging_failure),
325 askq(Q,DB).
326interpret_failing_question(Comm,Q,_) :-
327 integer(Comm),!,
328 askq(Q,Comm).
329interpret_failing_question(Comm,Q,DB) :-
330 writeallonline([' Unknown command, ',Comm,' type "help." for help.']),
331 ask_failing(Q,DB).
332
336
337tell_clause((~ H <- B)) :- !,
338 writeallonline(['Illegal rule: ~',H,' <- ',B,'.',nl,
339 'You cannot have negation in the head of a clause.']).
340tell_clause((H1 & H2 <- B)) :- !,
341 writeallonline(['Illegal rule: ',H1 & H2,' <- ',B,'.',nl,
342 'You cannot have a conjunction in the head of a clause.']).
343tell_clause((H1 , H2 <- B)) :- !,
344 writeallonline(['Illegal rule: ',H1 ,',', H2,' <- ',B,'.',nl,
345 'You cannot have a "," in the head of a clause.']).
346tell_clause((H <- B)) :-
347 !,
348 ( builtin(H,_) ->
349 writeallonline([H,' is built-in. It cannot be redefined.'])
350 ; illegal_body(B,Why) ->
351 writeallonline(['Illegal rule: ',H,'<-',B,'. '|Why])
352 ; assertz((H <- B))).
353tell_clause((H :- B)) :-
354 !,
355 writeallonline(['Illegal rule: ',H,':-',B,'. ":-" is not a legal implication. Use "<-".']).
356tell_clause((A, B)) :-
357 !,
358 writeallonline(['Error: ',(A,B),' is not a valid clause.']).
359tell_clause((A & B)) :-
360 !,
361 writeallonline(['Error: ',(A&B),' is not a valid clause.']).
362tell_clause((~A)) :-
363 !,
364 writeallonline(['Error: ',~A,' is not a valid clause.']).
365tell_clause(H) :-
366 builtin(H,_),!,
367 writeallonline([H,' is built-in. It cannot be redefined.']).
368tell_clause(H) :-
369 !,
370 assertz((H <- true)).
371
372illegal_body(X,['Variables cannot be atoms. Use call(',X,').']) :- var(X).
373illegal_body((_,_),[' "," is not a legal conjunction. Use "&".']).
374illegal_body((\+ _),[' "\\+" is not a legal negation. Use "~".']).
375illegal_body(!,[' "!" is not supported.']).
376illegal_body([_|_],[' Lists cannot be atoms.']).
377
378illegal_body((A&_),Why) :-
379 illegal_body(A,Why).
380illegal_body((_&A),Why) :-
381 illegal_body(A,Why).
382illegal_body((A;_),Why) :-
383 illegal_body(A,Why).
384illegal_body((_;A),Why) :-
385 illegal_body(A,Why).
386illegal_body((~A),Why) :-
387 illegal_body(A,Why).
388
392
396solve(true,_,true,_,Ass,Ass) :- !.
397solve((A&B),N,(AT&BT),[wrule(H,LT,_,RB)|WT],A0,A2) :- !,
398 solve(A,N,AT,[wrule(H,LT,A,(B&RB))|WT],A0,A1),
399 solve(B,N,BT,[wrule(H,(LT&AT),B,RB)|WT],A1,A2).
400solve(A \= B,_,if(A \= B,builtin),_,A0,A0) :- !,
401 differ(A,B).
402solve(call(G),_,_,WT,_,_) :-
403 var(G),!,
404 writeallonline(['Error: the argument to call must be bound when evaluated.']),
405 why_question(WT,_),
406 writeallonline(['Failing the call with unbound argument.']),!,
407 fail.
408solve(call(G),N,T,WT,A0,A1) :- !,
409 solve(G,N,T,WT,A0,A1).
410solve((~ G),N,if(~G,naf),WT,A0,A0) :- !,
411 mywhen( ground(G), failtoprove(G,N,WT)).
412solve(bagof(E,Q,L),N,BagTrees,WT,A0,A1) :- !,
413 solvebag(bagof(E,Q,L),N,BagTrees,WT,A0,A1).
414solve(G,_,if(G,assumed),_,A0,A1) :-
415 assumabl(G),
416 insert(G,A0,A1).
417solve(G,_,if(G,asked),WT,A0,A0) :-
418 askabl(G),
419 ask_user(G,WT,Ans),
420 Ans \== unknown,!, 421 Ans=yes.
422solve(H,_,if(H,builtin),WT,A0,A0) :-
423 builtin(H,C),!,
424 (C -> catch(H,_,debugging_builtin_error(H,WT))
425 ; writeallonline(['Error: "',H,'" can''t be called in this form, as ',C,' isn''t true.']),
426 debugging_builtin_error(H,WT)
427 ).
428solve(H,N0,if(H,BT),WT,A0,A1) :-
429 N0 > 0,
430 deter(H),
431 N1 is N0-1,
432 (H <- B),
433 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1), !.
434solve(H,N0,if(H,BT),WT,A0,A1) :-
435 N0 > 0,
436 N1 is N0-1,
437 (H <- B),
438 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1).
439solve(H,0,if(H,asked),WT,A0,A0) :-
440 debugging_failure,!,
441 debugging_failure_goal(H,WT).
442solve(_,0,_,_,_,_) :-
443 retractall(failed(_)),
444 assert(failed(unnaturally)),
445 fail.
446
447report(Q,Res,[]) :- !,
448 writeallonline(['Answer: ',Q,'.']),
449 report_runtime,
450 writel([' [ok,more,how,help]: ']),
451 flush_and_read(Comm),
452 interpret_report(Comm,Q,Res,[]).
453report(Q,Res,Ass) :-
454 writeallonline(['Answer: ',Q,'.']),
455 writeallonline(['Assuming: ',Ass,'.']),
456 report_runtime,
457 writel([' [more,ok,how,help]: ']),
458 flush_and_read(Comm),
459 interpret_report(Comm,Q,Res,Ass).
460
462interpret_report(ok,_,_,_) :- !.
463interpret_report(more,_,_,_) :- !,
464 reset_runtime,fail.
465interpret_report(end_of_file,_,_,_) :- !,
466 writeallonline(['^D']).
467interpret_report(how,Q,Res,Ass) :- !,
468 traverse(Res,Rep),
469 ( (Rep = top; Rep=up)
470 -> report(Q,Res,Ass)
471 ; Rep= retry
472 -> reset_runtime,fail
473 ; Rep=prompt
474 -> true
475 ; writeallonline(['This shouldn''t occur. Traverse reported ',Rep])
476 ).
477interpret_report(help,Q,Res,Ass) :- !,
478 writeallonline([
479 ' The system has proven an instance of your query.',nl,
480 ' You can give the following commands:',nl,
481 ' more. for more answers',nl,
482 ' ok. for no more answers',nl,
483 ' how. to enter a dialog to determine how the goal was proved.']),
484 report(Q,Res,Ass).
485interpret_report(Comm,Q,Res,Ass) :-
486 Comm \== more,
487 writeallonline(['Unknown command; ',Comm,'. Type "help." if you need help.']),
488 report(Q,Res,Ass).
489
491debugging_failure_goal(H,WT) :-
492 writeallonline([' Depth-bound reached. Current subgoal: ',H,'.']),
493 writel([' [fail,succeed,proceed,why,ok,help]: ']),
494 flush_and_read(Comm),
495 interpret_debugging_failure_command(Comm,H,WT).
496
497interpret_debugging_failure_command(help,H,WT) :- !,
498 writeallonline([
499 ' The system has reached the depth bound.',nl,
500 ' You can give the following commands:',nl,
501 ' fail. fail this subgoal.',nl,
502 ' succeed. make this subgoal succeed.',nl,
503 ' proceed. fail and don''t stop any more at failing subgoals.',nl,
504 ' why. determine why this subgoal was called.',nl,
505 ' ok. return to cilog prompt.',nl,
506 ' help. print this message.']),
507 debugging_failure_goal(H,WT).
508interpret_debugging_failure_command(fail,_,_) :- !,
509 retractall(failed(_)),
510 assert(failed(unnaturally)),
511 fail.
512interpret_debugging_failure_command(succeed,_,_) :- !.
513interpret_debugging_failure_command(proceed,_,_) :- !,
514 retractall(debugging_failure),
515 retractall(failed(_)),
516 assert(failed(unnaturally)),
517 fail.
518interpret_debugging_failure_command(ok,_,_) :- !,
519 throw(prompt).
520interpret_debugging_failure_command(end_of_file,_,_) :- !,
521 throw(prompt).
522interpret_debugging_failure_command(why,H,WT) :- !,
523 \+ \+ (numbervars(WT,0,_),why_question(WT,_)),
524 debugging_failure_goal(H,WT).
525interpret_debugging_failure_command(Comm,H,WT) :- !,
526 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
527 debugging_failure_goal(H,WT).
528
529
533builtin((A =< B), ground((A =< B))).
534builtin((A >= B), ground((A >= B))).
535builtin((A =\= B), ground((A =\= B))).
536builtin((A < B), ground((A<B))).
537builtin((A > B), ground((A>B))).
538builtin((_ is E),ground(E)).
539builtin(number(E),ground(E)).
540
542debugging_builtin_error(H,WT) :-
543 writeallonline([' Error in built-in predicate: ',H,'.']),
544 writel([' [fail,succeed,why,ok,help]: ']),
545 flush_and_read(Comm),
546 interpret_builtin_error_command(Comm,H,WT).
547
548interpret_builtin_error_command(help,H,WT) :- !,
549 writeallonline([
550 ' There is an error in a built-in predicate.',nl,
551 ' You can give the following commands:',nl,
552 ' fail. fail this subgoal.',nl,
553 ' succeed. make this subgoal succeed.',nl,
554 ' why. determine why this subgoal was called.',nl,
555 ' ok. return to cilog prompt.',nl,
556 ' help. print this message.']),
557 debugging_failure_goal(H,WT).
558interpret_builtin_error_command(fail,_,_) :- !,
559 fail.
560interpret_builtin_error_command(succeed,_,_) :- !.
561interpret_builtin_error_command(ok,_,_) :- !,
562 throw(prompt).
563interpret_builtin_error_command(end_of_file,_,_) :- !,
564 throw(prompt).
565interpret_builtin_error_command(why,H,WT) :- !,
566 \+ \+ (numbervars(WT,0,_),why_question(WT,_)),
567 debugging_builtin_error(H,WT).
568interpret_builtin_error_command(Comm,H,WT) :- !,
569 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
570 debugging_builtin_error(H,WT).
571
575
580ask_user(G,_,Ans) :-
581 ground(G),
582 asked(G,Ans1),!,Ans=Ans1.
583
584ask_user(G,WT,Ans) :-
585 ground(G),!,
586 writel(['Is ',G,' true? [yes,no,unknown,why,help]: ']),
587 flush_and_read(Rep),
588 interpret_ask_answer(Rep,G,WT,Ans).
589ask_user(G,WT,fail) :-
590 writeallonline([' Error: Askables with free variables not implemented.',nl,
591 ' The system wanted to ask ',G,'.',nl,
592 ' Entering why interation.']),
593 numbervars(WT,0,_),
594 why_question(WT,_),
595 writeallonline([' Askable subgoal ',G,' failing due to free variables.']).
596
597
599interpret_ask_answer(help,G,WT,Rep) :- !,
600 writeallonline([' The system is asking whether ',G,' is true or not. Give one of:',nl,
601 ' "yes." if ',G,' is known to be true.',nl,
602 ' "no." if ',G,' is known to be false.',nl,
603 ' "unknown." if ',G,' is unknown (so applicable clauses can be used).',nl,
604 ' "fail." to fail the subgoal (but not record an answer).',nl,
605 ' "why." to see why the system was asking this question.',nl,
606 ' "prompt." to return to the cilog prompt.',nl,
607 ' "help." to print this message.']),
608 ask_user(G,WT,Rep).
609interpret_ask_answer(yes,G,_,yes) :- !,
610 assertz(asked(G,yes)).
611interpret_ask_answer(no,G,_,no) :- !,
612 assertz(asked(G,no)).
613interpret_ask_answer(unknown,G,_,unknown) :- !,
614 assertz(asked(G,unknown)).
615interpret_ask_answer(fail,_,_,fail) :- !.
616interpret_ask_answer(prompt,_,_,_) :- !,
617 throw(prompt).
618interpret_ask_answer(end_of_file,_,_,_) :- !,
619 writeallonline(['^D']),
620 throw(prompt).
621
622interpret_ask_answer(why,G,WT,Rep) :- !,
623 \+ \+ ( numbervars(WT,0,_),why_question(WT,Rep),Rep \== prompt),
624 ask_user(G,WT,Rep).
625interpret_ask_answer(Ans,G,WT,Rep) :-
626 Ans \== fail,
627 writeallonline([' Unknown response "',Ans,'". For help type "help.".']),
628 ask_user(G,WT,Rep).
629
630
637why_question([wrule(H,LT,C,RB)|WT],Rep) :-
638 writeallonline([' ',C,' is used in the rule ']),
639 writeallonline([' ',H,' <-']),
640 print_tree_body(LT,1,Max),
641 writeallonline([' ** ',Max,': ',C]),
642 M1 is Max+1,
643 print_body(RB,M1,_),
644 writel([' [Number,why,help,ok]: ']),
645 flush_and_read(Comm),
646 interpret_why_ans(Comm,Max,[wrule(H,LT,C,RB)|WT],Rep).
647why_question([],down) :-
648 writeallonline([' This was the original query.']).
649
651interpret_why_ans(help,Max,[wrule(H,LT,C,RB)|WT],Rep) :- !,
652 writeallonline([
653' You can taverse the proof for a subgoal using following commands:',nl,
654' how i. show how element i (i<',Max,') of the body was proved.',nl,
655' how ',Max,'. show the rule being considered for ',C,'.',nl,
656' why. show why ',H,' is being proved.',nl,
657' prompt. return to the cilog prompt.',nl,
658' help. print this message.']),
659 why_question([wrule(H,LT,C,RB)|WT],Rep).
660interpret_why_ans(up,_,WT,Rep) :- !,
661 interpret_why_ans(why,_,WT,Rep).
662interpret_why_ans(why,_,[WR|WT],Rep) :- !,
663 why_question(WT,Rep1),
664 (Rep1 = down
665 -> why_question([WR|WT],Rep)
666 ; Rep=Rep1).
667interpret_why_ans((how N),Max,[wrule(H,LT,C,RB)|WT],Rep) :-
668 integer(N),!,
669 interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep).
670interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep) :-
671 integer(N),
672 N > 0,
673 N < Max, !,
674 nth(LT,1,_,N,E),
675 traverse(E,Rep1),
676 (Rep1=up -> why_question([wrule(H,LT,C,RB)|WT],Rep) ;
677 Rep1=top -> Rep=bottom ;
678 Rep1=retry
679 -> writeallonline([' retry doesn''t make sense here.']),
680 why_question([wrule(H,LT,C,RB)|WT],Rep) ;
681 Rep=Rep1).
682interpret_why_ans(Max,Max,_,down) :- !.
683interpret_why_ans(N,Max,WT,Rep) :-
684 integer(N),
685 N > Max, !,
686 writeallonline(['You can''t trace this, as it hasn''t been proved.']),
687 why_question(WT,Rep).
688interpret_why_ans(end_of_file,_,_,_) :- !,
689 writeallonline(['^D']),
690 throw(prompt).
691interpret_why_ans(prompt,_,_,_) :- !,
692 throw(prompt).
693interpret_why_ans(ok,_,_,bottom) :- !.
694
695interpret_why_ans(Comm,_,WT,Rep) :- !,
696 writeallonline(['Unknown command: ',Comm,'. Type "help." for help.']),
697 why_question(WT,Rep).
698
699
702print_body(true,N,N) :- !.
703print_body((A&B),N0,N2) :- !,
704 print_body(A,N0,N1),
705 print_body(B,N1,N2).
706print_body(H,N,N1) :-
707 writeallonline([' ',N,': ',H]),
708 N1 is N+1.
709
710
711
715
718
719failtoprove(G,N,WT) :-
720 (failed(naturally) ->
721 (solve(G,N,_,WT,[],_) ->
722 retract(failed(unnaturally)), asserta(failed(naturally)),fail
723 724 ; failed(naturally)
725 )
726 ; retract(failed(_)),
727 assert(failed(naturally)),
728 (solve(G,N,_,WT,[],_) ->
729 retract(failed(naturally)), asserta(failed(unnaturally)),fail
730 ; retract(failed(naturally)), asserta(failed(unnaturally))
731 732 )).
733
737
738solvebag(bagof(E,Q,L),N,bag(E,Q,BL),WT,A0,A1) :-
739 retract(failed(How)),
740 assert(failed(naturally)),
741 extractExistVars(Q,EVs,QR),
742 bagof(anstree(E,T),EVs^solve(QR,N,T,WT,A0,A1),BL), 743 ( failed(naturally) ->
744 firstOfAnstree(BL,L),
745 retract(failed(naturally)),
746 assert(failed(How))
747 ;
748 fail
749 ).
750
751firstOfAnstree([],[]).
752firstOfAnstree([anstree(E,_)|L],[E|R]) :-
753 firstOfAnstree(L,R).
754
(A^B^C,A^Vs,Q) :- !,
756 extractExistVars(B^C,Vs,Q).
757extractExistVars((A^Q&R),A,(Q&R)) :- !.
758extractExistVars(A^Q,A,Q) :- !.
759extractExistVars(Q,none,Q) :- !.
760
764
772traverse((A&B),Rep) :-
773 traverse(if(yes,(A&B)),Rep).
774traverse(if(H,true),up) :- !,
775 writeallonline([' ',H,' is a fact']).
776traverse(if(H,builtin),up) :- !,
777 writeallonline([' ',H,' is built-in.']).
778traverse(if(H,asked),up) :- !,
779 writeallonline([' You told me ',H,' is true.']).
780traverse(if(H,assumed),up) :- !,
781 writeallonline([' ',H,' is assumed.']).
782traverse(if(~G,naf),Rep) :- !,
783 writeallonline([' ',G,' finitely failed. You can examine the search space.']),
784 depth_bound(DB),
785 whynotb(G,DB,Rep,[],_).
786traverse(if(H,B),Rep) :-
787 writeallonline([' ',H,' <-']),
788 print_tree_body(B,1,Max),
789 writel([' How? [Number,up,retry,ok,prompt,help]: ']),
790 flush_and_read(Comm),
791 interpretcommand(Comm,B,Max,if(H,B),Rep).
792traverse(bag(E,Q,BL),Rep) :-
793 howbag(E,Q,BL,Rep).
794
797print_tree_body(true,N,N).
798print_tree_body((A&B),N0,N2) :-
799 print_tree_body(A,N0,N1),
800 print_tree_body(B,N1,N2).
801print_tree_body(if(H,_),N,N1) :-
802 writeallonline([' ',N,': ',H]),
803 N1 is N+1.
804print_tree_body(bag(E,Q,BL),N,N1) :-
805 firstOfAnstree(BL,L),
806 writeallonline([' ',N,': ',bagof(E,Q,L)]),
807 N1 is N+1.
808
810interpretcommand(help,_,Max,G,Rep) :- !,
811 writeallonline([
812 ' Give either (end each command with a period):',nl,
813 ' how i. explain how subgoal i (i<',Max,') was proved.',nl,
814 ' up. go up the proof tree one level.',nl,
815 ' retry. find another proof.',nl,
816 ' ok. stop traversing the proof tree.',nl,
817 ' prompt. return to the cilog prompt.',nl,
818 ' help. to print this message.']),
819 traverse(G,Rep).
820interpretcommand((how N),B,Max,G,Rep) :-
821 integer(N),
822 interpretcommand(N,B,Max,G,Rep).
823interpretcommand(N,B,Max,G,Rep) :-
824 integer(N),
825 N > 0,
826 N < Max,!,
827 nth(B,1,_,N,E),
828 traverse(E,Rep1),
829 ( Rep1= up
830 -> traverse(G,Rep)
831 ; Rep=Rep1
832 ).
833interpretcommand(N,_,Max,G,Rep) :-
834 integer(N),!,
835 836 M1 is Max-1,
837 writeallonline(['Number out of range: ',N,'. Use number in range: [1,',M1,'].']),
838 traverse(G,Rep).
839interpretcommand(up,_,_,_,up) :-!.
840interpretcommand(why,_,_,_,up) :-!.
841interpretcommand(ok,_,_,_,top) :-!.
842interpretcommand(prompt,_,_,_,_) :-!,
843 throw(prompt).
844interpretcommand(retry,_,_,_,retry) :-!.
845interpretcommand(end_of_file,_,_,_,prompt) :-!,
846 writeallonline(['^D']).
847interpretcommand(C,_,_,G,Rep) :-
848 writeallonline(['Illegal Command: ',C,' Type "help." for help.']),
849 traverse(G,Rep).
850
852nth((A&B),N0,N2,N,E) :- !,
853 nth(A,N0,N1,N,E),
854 nth(B,N1,N2,N,E).
855nth(true,N0,N0,_,_) :- !.
856nth(A,N,N1,N,A) :- !,
857 N1 is N+1.
858nth(_,N0,N1,_,_) :-
859 N1 is N0+1.
860
863howbag(E,Q,BL,Rep) :-
864 writeallonline([' The call ',bagof(E,Q,V),' returned with ',V,' containing']),
865 displaybaglist(BL,0,BLLen),
866 writel([' How? [Number,up,whynot,ok,prompt,help]: ']),
867 flush_and_read(Comm),
868 interpret_how_bag_command(Comm,E,Q,BL,BLLen,Rep).
869
871displaybaglist([],0,0) :- !,
872 writeallonline(['no elements.']).
873displaybaglist([],N,N) :- !.
874displaybaglist([anstree(E,_)|R],N,NN) :-
875 N1 is N+1,
876 writeallonline([' ',N1,': ',E]),
877 displaybaglist(R,N1,NN).
878
879interpret_how_bag_command(up,_,_,_,_,up) :- !.
880interpret_how_bag_command(ok,_,_,_,_,top) :- !.
881interpret_how_bag_command(prompt,_,_,_,_,_) :- !,
882 throw(prompt).
883interpret_how_bag_command(end_of_file,_,_,_,_,_) :- !,
884 writeallonline(['^D']),
885 throw(prompt).
886
887interpret_how_bag_command(help,E,Q,BL,Max,Rep) :- !,
888 writeallonline([
889 ' Give either (end each command with a period):',nl,
890 ' how i. explain how element i (i=<',Max,') was proved.',nl,
891 ' up. go up the proof tree one level.',nl,
892 ' retry. find another proof.',nl,
893 ' ok. stop traversing the proof tree.',nl,
894 ' prompt. return to the cilog prompt.',nl,
895 ' help. to print this message.']),
896 howbag(E,Q,BL,Rep).
897interpret_how_bag_command(N,E,Q,BL,BLLen,Rep) :-
898 integer(N),!,
899 ( N >= 0, N =< BLLen ->
900 nthList(N,BL,anstree(_,ET)),
901 traverse(ET,Repl),
902 ( Repl = up
903 -> howbag(E,Q,BL,Rep)
904 ; Rep=Repl
905 )
906 ; writeallonline([' Error: ',N,' must be in range ',[1,BLLen]]),
907 howbag(E,Q,BL,Rep)
908 ).
909interpret_how_bag_command((how N),E,Q,BL,BLLen,Rep) :- !,
910 interpret_how_bag_command(N,E,Q,BL,BLLen,Rep).
911
912interpret_how_bag_command(Comm,E,Q,BL,_,Rep) :- !,
913 writeallonline(['Unknown command ',Comm,' type "help." for help.']),
914 howbag(E,Q,BL,Rep).
915
917nthList(1,[E|_],E) :- !.
918nthList(N,[_|R],E) :-
919 N>1,
920 N1 is N-1,
921 nthList(N1,R,E).
922
926
934
935whynotb((A & B),DB,Rep,Ass0,Ass2) :-
936 retractall(failed(_)),
937 assert(failed(naturally)),
938 solve(A,DB,Res,[whynot],Ass0,Ass1),
939 report_whynot_conj(A,Res,B,DB,Rep,Ass1,Ass2).
940whynotb((A & _),DB,Rep,Ass0,Ass1) :- !,
941 whynotb(A,DB,Rep,Ass0,Ass1).
942
943whynotb(call(A),DB,Rep,Ass0,Ass1) :- !,
944 whynotb(A,DB,Rep,Ass0,Ass1).
945whynotb((~ A),DB,Rep,Ass0,Ass0) :- !,
946 retractall(failed(_)),
947 assert(failed(naturally)),
948 ( solve(A,DB,Res,[whynot],[],_) ->
949 writeallonline([' ',~A,' failed as ',A,' suceeded. Here is how:']),
950 traverse(Res,Rep)
951 ; failed(unnaturally) ->
952 writeallonline([' ',~A,' failed because of the depth-bound.']),
953 whynotb(A,DB,Rep,[],_)
954 ; writeallonline([' ',~A,' succeeds, as ',A,' finitely fails.']),
955 Rep=up
956 ).
957
958whynotb(A,_,up,Ass0,Ass0) :-
959 builtin(A,C),!,
960 (call(C)
961 -> (call(A)
962 -> writeallonline([' ',A,' is built-in and succeeds.'])
963 ; writeallonline([' ',A,' is built-in and fails.']))
964 ; writeallonline([' ',A,' is built-in and is insufficiently instanciated.'])).
965
966whynotb((A \= B),_,up,Ass0,Ass0) :-
967 ?=(A,B),!,
968 (A \== B
969 -> writeallonline([' ',(A \= B),' succeeds as they can never unify.'])
970 ; writeallonline([' ',(A \= B),' fails as they are identical.'])).
971whynotb((A \= B),_,up,Ass0,Ass0) :-
972 writeallonline([' ',(A \= B),' cannot be resolved. It is delayed.']),
973 when(?=(A,B),
974 (A \== B
975 -> writeallonline([' Resolving delayed ',(A \= B),'. It succeeded.'])
976 ; writeallonline([' Failure due to delayed constraint, ',(A \= B),'.']),
977 fail)).
978
979whynotb(Q,0,up,Ass0,Ass0) :- !,
980 writeallonline([' ',Q,' fails because of the depth-bound.']).
981
982whynotb(Q,DB,up,Ass0,Ass0) :-
983 DB > 0,
984 (Q <- true),!,
985 writeallonline([' ',Q,' is a fact. It doesn''t fail.']).
986
987whynotb(Q,DB,Rep,Ass0,Ass1) :-
988 DB > 0,
989 (Q <- B),
990 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
991whynotb(Q,_,up,Ass0,Ass0) :-
992 writeallonline([' There is no applicable rule for ',Q,'.']).
993
994whynotrule(Q,B,DB,Rep,Ass0,Ass1) :-
995 writeallonline([' ',Q,' <- ',B,'.']),
996 writel([' Trace this rule? [yes,no,up,help]: ']),
997 flush_and_read(Comm),
998 whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1).
999
1000whynotruleinterpret(yes,Q,B,DB,Rep,Ass0,Ass1) :- !,
1001 DB1 is DB-1,
1002 whynotb(B,DB1,Rep1,Ass0,Ass1),
1003 (Rep1 = up
1004 -> whynotrule(Q,B,DB,Rep,Ass0,Ass1)
1005 ; Rep=Rep1).
1006whynotruleinterpret(no,_,_,_,_,_,_) :- !,
1007 fail.
1008whynotruleinterpret(up,_,_,_,up,Ass0,Ass0) :- !.
1009whynotruleinterpret(end_of_file,_,_,_,prompt,_,_) :- !,
1010 writeallonline(['^D']).
1011whynotruleinterpret(ok,_,_,_,prompt,_,_) :- !.
1012whynotruleinterpret(help,Q,B,DB,Rep,Ass0,Ass1) :- !,
1013 writeallonline([
1014 ' Do you want to examine why this rule failed?',nl,
1015 ' yes. look at this rule',nl,
1016 ' no. try another rule',nl,
1017 ' up. go back to the rule this rule was called from',nl,
1018 ' ok. go to top-level prompt']),
1019 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
1020whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1) :-
1021 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
1022 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
1023
1024
1025report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1) :-
1026 writeallonline([' The proof for ',A,' succeeded.']),
1027 writel([' Should this answer lead to a successful proof? [yes,no,debug,help]: ']),
1028 flush_and_read(Comm),
1029 why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1).
1030
1031why_not_conj_interpret(debug,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
1032 traverse(Res,Rep1),
1033 (Rep1 = up
1034 -> report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1)
1035 ; Rep=Rep1).
1036why_not_conj_interpret(yes,_,_,B,DB,Rep,Ass0,Ass1) :- !,
1037 whynotb(B,DB,Rep,Ass0,Ass1).
1038why_not_conj_interpret(no,_,_,_,_,_,_,_) :- !,
1039 fail. 1040
1041why_not_conj_interpret(end_of_file,_,_,_,_,prompt,_,_) :- !,
1042 writeallonline(['^D']).
1043why_not_conj_interpret(ok,_,_,_,_,prompt,_,_) :- !,
1044 writeallonline(['^D']).
1045why_not_conj_interpret(help,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
1046 writeallonline([
1047 ' yes. this instance should have made the body succeed.',nl,
1048 ' no. this instance should lead to a failure of the body.',nl,
1049 ' debug. this instance is false, debug it.',nl,
1050 ' ok. I''ve had enough. Go to the prompt.',nl,
1051 ' help. print this message.']),
1052 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1053why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1) :-
1054 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
1055 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1056
1057
1061
1062read_termln(T):- read_termln([], T).
1063read_termln(PreCodes, T):- PreCodes\==[],
1064 text_to_string(PreCodes,String),
1065 normalize_space(chars(Chars), String),
1066 last(Chars,Char),Char=='.',
1067 !, fail.
1068read_termln(PreCodes, T):-
1069 read_line_to_codes(current_input,NewCodes),
1070 append(PreCodes,NewCodes,Codes),
1071 (read_term_from_codes(Codes,T,[module(cilog),syntax_errors(fail)]) -> true ;
1072 ( read_termln(Codes, T))).
1073
1074flush_and_read(T) :-
1075 flush_output,
1076 read_termln(T).
1077
1078with_file(File,Read,Input,Goal):-
1079 setup_call_cleanup(
1080 open(File,Read,Input),
1081 Goal,
1082 close(Input)).
1083
1084
1085with_input(Input,Goal):-
1086 current_input(OldFile),
1087 setup_call_cleanup(set_input(Input),
1088 Goal,
1089 set_input(OldFile)).
1090
1091ci_load(File) :-
1092 with_file(File,read,Input,
1093 with_input(Input,and_read_all)),
1094 writeallonline(['CILOG theory ',File,' loaded.']).
1095
1096and_read_all:-
1097 flush_and_read(T),
1098 read_all(T).
1099
1100read_all(end_of_file) :- !.
1101read_all(T) :-
1102 on_cilog_read(T),
1103 and_read_all.
1104
1105:- module_transparent(on_cilog_read/1). 1106on_cilog_read(end_of_file).
1107on_cilog_read(( :- B)) :- !, call(B).
1108on_cilog_read(T):- on_cilog_read1(T).
1109
1110on_cilog_read1((askable G)):- !,
1111 assertz(askabl(G)).
1112on_cilog_read1((assumable G)) :- !,
1113 assertz(assumabl(G)).
1114on_cilog_read1((H :- B)) :- !,
1115 writeallonline(['Error: Illegal Implication: ',H,' :- ',B,'. Use <- or prload.']).
1116on_cilog_read1(T) :-
1117 tell_clause(T).
1118
1119
1120prolog_load(File) :-
1121 with_file(File,read,Input,
1122 with_input(Input,and_prread_all)),
1123 writeallonline(['CILOG theory ',File,' consulted.']).
1124
1125and_prread_all:-
1126 flush_and_read(T),
1127 prread_all(T).
1128prread_all(end_of_file) :- !.
1129prread_all(T) :-
1130 prillegal(T,Mesg),!,
1131 writeallonline(Mesg).
1132prread_all(T) :-
1133 prtell(T),
1134 and_prread_all.
1135
1138prillegal((H <- B),['Error. Illegal Implication: ',H,' <- ',B,
1139 '. Use :- in prload.']) :- !.
1140prillegal((:- B),['Error. Commands not allowed. ":- ',B,'."']) :- !.
1141prillegal((_ :- B),Mesg) :- !,
1142 prillbody(B,Mesg).
1143prillbody((A,_),Mesg) :-
1144 prillbody(A,Mesg).
1145prillbody((_,B),Mesg) :-
1146 prillbody(B,Mesg).
1147prillbody((_;_),['Prolog rules assume disjunction ";". Define it before loading.']) :-
1148 \+ ((_;_) <- _).
1149prillbody((A;_),Mesg) :-
1150 prillbody(A,Mesg).
1151prillbody((_;B),Mesg) :-
1152 prillbody(B,Mesg).
1153prillbody((_&_),['Error. Illegal conjunction in Prolog rules: &']):- !.
1154prillbody(!,['Error. Cut (!) not allowed.']) :- !.
1155prillbody((_ -> _ ; _),['Error. "->" is not implemented.']) :- !.
1156
1158prtell((H :- B)) :- !,
1159 convert_body(B,B1),
1160 assertz((H <- B1)).
1161prtell(H) :-
1162 assertz((H <- true)).
1163
1165convert_body((A,B),(A1&B1)) :- !,
1166 convert_body(A,A1),
1167 convert_body(B,B1).
1168convert_body((A;B),(A1;B1)) :- !,
1169 convert_body(A,A1),
1170 convert_body(B,B1).
1171convert_body((\+ A),(~ A1)) :- !,
1172 convert_body(A,A1).
1173convert_body(A,A).
1174
1175
1179
1180start :-
1181 show_cilog_help,
1182 cilog_version(V),
1183 writeallonline([nl,
1184 'CILOG Version ',V,'. Copyright 1998-2004, David Poole.',nl,
1185 'CILOG comes with absolutely no warranty.',nl,
1186 'All inputs end with a period. Type "help." for help.']),
1187 start1.
1188
1189start1 :-
1190 catch(cilog,Exc,handle_exception(Exc)). 1192 1193go:- cilog.
1194cilog :-
1195 repeat,
1196 writel(['cilog: ']),
1197 flush_and_read(T),
1198 interpret(T),
1199 T == end_of_file,
1200 writeallonline(['Returning to Prolog. Type "start." to start cilog.']),!.
1201
1202handle_exception(prompt) :- !, start1.
1203handle_exception(quit) :- halt.
1204handle_exception(Exc) :-
1205 writeallonline(['Error: ',Exc]),
1206 start1.
1207
1211
1215check :-
1216 (H <- B),
1217 body_elt_undefined(B,H,B).
1218check.
1219
1220body_elt_undefined(true,_,_) :- !,fail.
1221body_elt_undefined((A&_),H,B) :-
1222 body_elt_undefined(A,H,B).
1223body_elt_undefined((_&A),H,B) :- !,
1224 body_elt_undefined(A,H,B).
1225body_elt_undefined((~ A),H,B) :- !,
1226 body_elt_undefined(A,H,B).
1227body_elt_undefined((A;_),H,B) :-
1228 body_elt_undefined(A,H,B).
1229body_elt_undefined((_;A),H,B) :- !,
1230 body_elt_undefined(A,H,B).
1231body_elt_undefined(call(A),H,B) :- !,
1232 body_elt_undefined(A,H,B).
1233body_elt_undefined(_ \= _,_,_) :- !,fail.
1234body_elt_undefined(A,_,_) :-
1235 askabl(A),!,fail.
1236body_elt_undefined(A,_,_) :-
1237 assumabl(A),!,fail.
1238body_elt_undefined(A,_,_) :-
1239 builtin(A,_),!,fail.
1240body_elt_undefined(A,_,_) :-
1241 (A <- _),!,fail.
1242body_elt_undefined(A,H,B) :-
1243 writeallonline(['Warning: no clauses for ',A,' in rule ',(H <- B),'.']),!,fail.
1244
1248
1250checking_runtime.
1251
1253stats_command(runtime) :- !,
1254 retractall(checking_runtime),
1255 asserta(checking_runtime),
1256 writeallonline(['Runtime report turned on. Type "stats none." to turn it off.']).
1257stats_command(none) :- !,
1258 retractall(checking_runtime).
1259stats_command(_) :-
1260 writeallonline(['The stats commands implemented are:']),
1261 writeallonline([' stats runtime. turn on report of runtime.']),
1262 writeallonline([' stats none. turn off report of runtime.']).
1263
1267
1268reset_runtime :-
1269 checking_runtime,
1270 retractall(lastruntime(_)),
1271 get_runtime(T,_),
1272 asserta(lastruntime(T)),!.
1273reset_runtime :-
1274 checking_runtime ->
1275 writeallonline([' Problem with runtime checking.'])
1276 ; true.
1277
1278report_runtime :-
1279 checking_runtime,
1280 lastruntime(T),
1281 get_runtime(T1,Units),
1282 RT is T1 - T,
1283 writeallonline([' Runtime since last report: ',RT,' ',Units,'.']),!.
1284report_runtime :-
1285 checking_runtime ->
1286 writeallonline([' Problem with runtime reporting.'])
1287 ; true.
1288
1289
1293
1295writeallonline(L) :-
1296 \+ \+ (numbervars(L,0,_),writel0(L)),
1297 nl.
1299writel(L) :-
1300 \+ \+ (numbervars(L,0,_),writel0(L)).
1301
1303writel0([]) :- !.
1304writel0([nl|T]) :- !,
1305 nl,
1306 writel0(T).
1307writel0([H|T]) :-
1308 mywrite(H),
1309 writel0(T).
1310
1311insert(A,[],[A]).
1312insert(A,[A1|R],[A|R]) :- A == A1,!.
1313insert(A,[B|R],[B|R1]) :-
1314 insert(A,R,R1).
1315
1316
1318different(X,Y) :-
1319 \+ (X=Y),!.
1320different(X,Y) :-
1321 X \== Y,
1322 writeallonline(['Warning: ',X\=Y,' failing. Delaying not implemented.']),!,
1323 fail.
1324
1325:- initialization(start, main). 1326
1327:- include(library(dialect/logicmoo/dialect_loader_incl)). 1328
1329prolog:dialect_reads(cilog, on_cilog_read)