59
62:- module(common_logic_boxlog,
63 [ avoidHeadLoop/2,
64 body_for_mpred_1/5,
65 body_for_mpred_2/5,
66 body_for_pfc/5,
67 boxlog_to_pfc/2,
68 boxlog_to_pfc_pass_2/3,
69 boxlog_to_pfc_pass_3/4,
70 boxlog_to_pfc_pass_4/2,
71 can_use_hack/1,
72 73 conjoin_maybe/3,
74 correct_mode/3,
75 did_use_hack/1,
76 get_op_alias_compile/2,
77 get_reln/2,
78 head_for_skolem/3,
79 is_unit/2,
80 is_unit/0,
81 is_unit/3,
82 is_unit/4,
83 is_unit/5,
84 is_unit/6,
85 is_unit/7,
86 is_unit/8,
87 is_unit/9,
88 is_unit/10,
89 is_units_b/1,
90 is_units_h/1,
91 make_must_ground/3,
92 make_vg/4,
93 overlaping/3,
94 isk/2,
95 isk_bind/3,
96 overlapingFunctors/2,
97 reduce_literal/2,
98 set_clause_compile/1,
99 vg/1,
100 vg/3]). 101
102
103:- include(library('logicmoo/common_logic/common_header.pi')). 104
106:- reexport(baseKB:library('logicmoo/common_logic/common_logic_compiler.pl')).
107
108:- user:use_module(library(dialect/hprolog),[]). 109:- common_logic_boxlog:use_module(library(dialect/hprolog),[]). 110
113
114:- set_how_virtualize_file(bodies). 115
116:- system:((
117 op(1199,fx,('==>')),
118 op(1190,xfx,('::::')),
119 op(1180,xfx,('==>')),
120 op(1170,xfx,'<==>'),
121 op(1160,xfx,('<-')),
122 op(1150,xfx,'=>'),
123 op(1140,xfx,'<='),
124 op(1130,xfx,'<=>'),
125 op(600,yfx,'&'),
126 op(600,yfx,'v'),
127 op(350,xfx,'xor'),
128 op(300,fx,'~'),
129 op(300,fx,'-'))). 130
137is_units_h(A):-maplist(is_unit,A).
138
145is_units_b(A):-maplist(is_unit,A).
147
154is_unit :- dmsg(is_unit).
155
162is_unit(A,B):-is_unit(A),is_unit(B).
163
170is_unit(A,B,C):-is_unit(A),is_unit(B),is_unit(C).
171
178is_unit(A,B,C,D):-is_unit(A),is_unit(B),is_unit(C),is_unit(D).
179is_unit(A,B,C,D,E):-is_unit(A,B,C,D),is_unit(E).
180is_unit(A,B,C,D,E,F):-is_unit(A,B,C,D),is_unit(E,F).
181is_unit(A,B,C,D,E,F,G):-is_unit(A,B,C,D),is_unit(E,F,G).
182is_unit(A,B,C,D,E,F,G,H):-is_unit(A,B,C,D),is_unit(E,F,G,H).
183is_unit(A,B,C,D,E,F,G,H,I):-is_unit(A,B,C,D),is_unit(E,F,G,H,I).
184is_unit(A,B,C,D,E,F,G,H,I,J):-is_unit(A,B,C,D),is_unit(E,F,G,H,I,J).
185
188
195vg(G):- (ground(G); ( compound(G), \+ (arg(_,G,E),var(E)))),!.
196
203vg(_,B,C):-vg(B),vg(C).
204
212make_must_ground(H,BB,VG):-
213 term_slots(H,HVs)->
214 term_slots(BB,BBVs)->
215 hprolog:intersect_eq(HVs,BBVs,Shared),
216 hprolog:list_difference_eq(HVs,BBVs,UHVs),
217 hprolog:list_difference_eq(BBVs,HVs,UBBVs),
218 make_vg(UBBVs,Shared,UHVs,VG),!.
219
220
227make_vg([],[],[],true):-!.
228make_vg([],[],_,true):-!.
229make_vg(_,[],[],true):-!.
230make_vg([],Shared,[],{(S)}):- S=..[is_unit|Shared],!.
231make_vg(_,Shared,_,{(S)}):- S=..[is_unit|Shared],!.
232make_vg(B,S,H,{(CB,CS,CH)}):- CB=..[is_units_b,B],CS=..[is_unit|S],CH=..[is_units_h,H].
233
234
241set_clause_compile(TYPE):-op_alias((:-),TYPE).
242
243
250get_op_alias_compile(I,O):-get_op_alias(I,O),( I== (:-)),( O\== (:-)),!.
251get_op_alias_compile(_,fwc).
259boxlog_to_pfc(H0,H0):- \+ compound(H0),!.
260boxlog_to_pfc(H0,H0):- is_ftVar(H0),!.
261boxlog_to_pfc([H|T],[HH|TT]):- !,boxlog_to_pfc(H,HH),boxlog_to_pfc(T,TT).
262boxlog_to_pfc((A,B),C):- !, must_maplist(boxlog_to_pfc,[A,B],[AA,BB]),conjoin(AA,BB,C).
263boxlog_to_pfc('$unused'(P),'$unused'(P)):-!.
264boxlog_to_pfc( ('$unused'(H) :- B), ('$unused'(H) :- B)):-!.
265boxlog_to_pfc(H0,PFCO):-
266 sumo_to_pdkb(H0,H00),
267 subst(H00,('not'),('~'),H),
268 get_op_alias_compile((:-),TYPE),!,
269 with_vars_locked(throw,H,((maybe_notrace((boxlog_to_pfc_pass_1(TYPE,H,OUTPUTM))),!,
270 OUTPUTM=OUTPUT))),
271 subst(OUTPUT,('not'),('~'),PFCO).
272
273
274
275boxlog_to_pfc_pass_1(TYPE,HB,OUTPUTM):-
276 expand_to_hb(HB,H,B),
277 boxlog_to_pfc_pass_2(TYPE,(H:-B),OUTPUTM),!.
284boxlog_to_pfc_pass_2(Why,I,O):-nonvar(O),!,boxlog_to_pfc_pass_2(Why,I,M),!,mustvv(M=O).
285boxlog_to_pfc_pass_2(_,(H:-(Cwc,B)),(H:-(Cwc,B))):- Cwc == cwc,!.
286boxlog_to_pfc_pass_2(Mode,(H:-(Cwc,B)),(H:-(Cwc,B))):- Mode == Cwc,!.
287boxlog_to_pfc_pass_2(cwc,H,OUTPUT):-!, boxlog_to_pfc_pass_2((:-),H,OUTPUT).
288boxlog_to_pfc_pass_2(==>,H,OUTPUT):-!, boxlog_to_pfc_pass_2(fwc,H,OUTPUT).
289boxlog_to_pfc_pass_2(=>,H,OUTPUT):-!, boxlog_to_pfc_pass_2(fwc,H,OUTPUT).
290boxlog_to_pfc_pass_2(<=,H,OUTPUT):-!, boxlog_to_pfc_pass_2(fwc,H,OUTPUT).
291boxlog_to_pfc_pass_2(<-,H,OUTPUT):-!, boxlog_to_pfc_pass_2(bwc,H,OUTPUT).
292boxlog_to_pfc_pass_2(rev(==>),H,OUTPUT):-!, boxlog_to_pfc_pass_2(fwc,H,OUTPUT).
293boxlog_to_pfc_pass_2(rev(=>),H,OUTPUT):-!, boxlog_to_pfc_pass_2(fwc,H,OUTPUT).
294boxlog_to_pfc_pass_2(~(WHAT),(~(H):-B),OUTPUT):-!, boxlog_to_pfc_pass_2(WHAT,(~(H):-B),OUTPUT).
295boxlog_to_pfc_pass_2(~(WHAT),~(H),OUTPUT):-!, boxlog_to_pfc_pass_2(WHAT,~(H),OUTPUT).
296
297boxlog_to_pfc_pass_2((:-),(~(H):-B),unused_true((~(H):-B))):- nonvar(H),a(prologBuiltin,H),!.
298boxlog_to_pfc_pass_2((:-),(~(H):-B),(HH:-(cwc,BBB))):-body_for_pfc((:-),~(H),HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB).
299boxlog_to_pfc_pass_2((:-),(H:-B),OUT):- a(pfcControlled,H),boxlog_to_pfc_pass_2((bwc),(H:-B),OUT),!.
300boxlog_to_pfc_pass_2((:-),(H:-B),(HH:-(cwc,BBB))):- body_for_pfc((:-),H,HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB).
301boxlog_to_pfc_pass_2((:-),~(H),~(H)):- !.
302boxlog_to_pfc_pass_2((:-),H,H):- !.
303
304
305boxlog_to_pfc_pass_2(fwc,(~(H):-B),unused_true((~(H):-B))):- nonvar(H),H = skolem(_,_),!.
306boxlog_to_pfc_pass_2(fwc,(~(H):-B),OUT):- term_slots(H,HV),term_slots(B,BV), HV\==BV,!,boxlog_to_pfc_pass_2(bwc,(~(H):-B),OUT).
307boxlog_to_pfc_pass_2(fwc,(~(H):-B),(BBBHH)):- body_for_pfc(fwc,~(H),HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB),body_head_pfc(BBB,HH,BBBHH).
308boxlog_to_pfc_pass_2(fwc,(H:-B),(BBBHH)):- body_for_pfc(fwc,H,HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB),body_head_pfc(BBB,HH,BBBHH).
309boxlog_to_pfc_pass_2(fwc,~(H),~(H)):- !.
310boxlog_to_pfc_pass_2(fwc,H,H):- !.
311
312boxlog_to_pfc_pass_2(bwc,(~(H):-B),unused_true((~(H):-B))):- nonvar(H),H = skolem(_,_),!.
313boxlog_to_pfc_pass_2(bwc,(~(H):-B),(HH<-BBB)):-body_for_pfc(<-,~(H),HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB).
314boxlog_to_pfc_pass_2(bwc,(H:-B),OUT):- a(pfcRHS,H),term_slots(H,HV),term_slots(B,BV),HV==BV,boxlog_to_pfc_pass_2((fwc),(H:-B),OUT),!.
315boxlog_to_pfc_pass_2(bwc,(H:-B),(HH<-BBB)):- body_for_pfc(<-,H,HH,B,BB),make_must_ground(HH,BB,MMG),conjoin_body(BB,MMG,BBB).
316boxlog_to_pfc_pass_2(bwc,~(H),~(H)):- !.
317boxlog_to_pfc_pass_2(bwc,H,H):- !.
318
319boxlog_to_pfc_pass_2(TYPE,(H:-BB),OUTPUT):- !,boxlog_to_pfc_pass_3(TYPE,H,BB,OUTPUT).
320boxlog_to_pfc_pass_2(TYPE,~(H),OUTPUT):- !,boxlog_to_pfc_pass_3(TYPE,~(H),true,OUTPUT).
321boxlog_to_pfc_pass_2(TYPE,H,OUTPUT):- !,boxlog_to_pfc_pass_3(TYPE,H,true,OUTPUT).
322
323body_head_pfc(BBB,HH,HH):-is_true(BBB),!.
324body_head_pfc(BBB,HH,(BBB==>HH)).
325
332boxlog_to_pfc_pass_3(TYPE,~(H),BB,(~(H):-OUTPUT)):-!,conjoin_maybe(TYPE,BB,OUTPUT).
333boxlog_to_pfc_pass_3(TYPE,H,BB,(H:-OUTPUT)):- conjoin_maybe(TYPE,BB,OUTPUT).
334boxlog_to_pfc_pass_3(TYPE,H,BB,(H:-OUTPUT)):- conjoin_maybe(TYPE,BB,OUTPUT).
335
336
337
344conjoin_maybe(_X,true,true):-!.
345conjoin_maybe(TYPE,BB,OUTPUT):-conjoin(TYPE,BB,OUTPUT).
346
347
354correct_mode(_,O,O):-var(O),!.
355correct_mode((:-),{M},O):-!,correct_mode((:-),M,O).
356correct_mode(Mode,(A,B),O):-!,correct_mode(Mode,A,AA),correct_mode(Mode,B,BB),conjoin_body(AA,BB,O).
357correct_mode(_,O,O).
358
359
366body_for_pfc(Mode,Head,NewNewHead,I,O):-reduce_literal(Head,NewHead),!,body_for_mpred_1(Mode,NewHead,NewNewHead,I,O),!.
367body_for_pfc(Mode,Head,NewHead,B,BB):- body_for_mpred_1(Mode,Head,NewHead,B,BB),!.
368
369
376body_for_mpred_1(Mode,Head,HeadO,C,CO):- (Mode ==(:-);Mode==(cwc);Mode==(<-)),
377 overlaping(C,Head,Avoid),
378 body_for_mpred_1(Mode,Head,HeadM,zzAvoidHeadLoop,AA),
379 body_for_mpred_2(Mode,HeadM,HeadO,C,BB),!,
380 subst(AA,zzAvoidHeadLoop,{Avoid},AAA),
381 conjoin_body(AAA,BB,CM),correct_mode(Mode,CM,CO).
382body_for_mpred_1(Mode,Head,NewNewHead,I,O):-body_for_mpred_2(Mode,Head,NewNewHead,I,M),correct_mode(Mode,M,O).
383
384
385
392overlaping(C,Head,Avoid):- (is_ftVar(C);is_ftVar(Head)),!,Avoid=avoidHeadLoop(C,Head).
393overlaping(~(C),Head,Avoid):-is_ftNonvar(C),!,overlaping(C,Head,Avoid).
394overlaping(C,~(Head),Avoid):-is_ftNonvar(Head),!,overlaping(C,Head,Avoid).
395overlaping(C,Head,Avoid):-is_ftNonvar(Head),is_ftNonvar(C), compound(C),compound(Head),once((get_reln(C,FC),get_reln(Head,HC))),!,overlapingFunctors(FC,HC),!,Avoid=avoidHeadLoop(C,Head).
396
397
404overlapingFunctors(FC,HC):- (\+ \+ FC=HC),!.
405overlapingFunctors(t,_):-!.
406overlapingFunctors(_,t):-!.
407
408
415get_reln(C,F):-var(C),!,F=_.
416get_reln(C,F):-is_ftVar(C),!,F=_.
417get_reln(~(C),RO):-nonvar(C),!,get_reln(C,RO).
418get_reln(~(C),RO):-nonvar(C),!,get_reln(C,RO).
419get_reln(\+(C),RO):-nonvar(C),!,get_reln(C,RO).
420get_reln('{}'(C),RO):-nonvar(C),!,get_reln(C,RO).
421get_reln(C,RO):-get_functor(C,F),
422 (F==t->
423 (arg(1,C,R),(is_ftVar(R)->RO=t;RO=R));
424 RO=F),!.
425
426
433avoidHeadLoop(C,Head):- stack_check, ground(C),(C\=Head),\+ is_loop_checked(C).
434
435
436
443isk(Var,SK):- ignore((=(Var,SK))),!.
444isk(Var,SK):- when('?='(Var,Val),isk_bind(Var,Val,SK)).
445
452isk_bind(Var,Val,SK):-show_call(add_cond(Var,[Val,SK])).
453
458
465head_for_skolem(H,if_missing(H,HH),skolem(In,NewOut)):- contains_var(In,H),subst(H,In,NewOut,HH),!.
466
467is_skolem_arg(Var):- callable(Var),functor(Var,F,_),atom_concat('sk',_,F),atom_concat(_,'Fn',F).
476body_for_mpred_2(_Mode,Head,Head,A,A):-is_ftVar(A),!,sanity(\+ is_ftVar(Head)).
477
479
480body_for_mpred_2(Mode,Head,HeadO,(A,B), C):-!,body_for_mpred_1(Mode,Head,HeadM,A,AA),body_for_pfc(Mode,HeadM,HeadO,B,BB),conjoin_body(AA,BB,C).
481body_for_mpred_2(Mode,Head,HeadO,(A;B),(AA;BB)):-!,body_for_mpred_1(Mode,Head,HeadM,A,AA),body_for_pfc(Mode,HeadM,HeadO,B,BB).
482body_for_mpred_2((:-),Head,HeadO,(A/B),(AA,BB)):-!,body_for_mpred_1(Mode,Head,HeadM,A,AA),body_for_pfc(Mode,HeadM,HeadO,B,BB).
483body_for_mpred_2(Mode,Head,HeadO,(A/B),(AA/BB)):-!,body_for_mpred_1(Mode,Head,HeadM,A,AA),body_for_pfc(Mode,HeadM,HeadO,B,BB).
484
485body_for_mpred_2((fwc),H,HEAD,I,O):- H\=if_missing(_,_), sub_term(Var,H),attvar(Var),get_attr(Var,sk,Sk),
486 subst(H,Var,NewVar,NewH),head_for_skolem(NewH,SKHEAD,skolem(NewVar,Sk)), !,
487 body_for_mpred_2((fwc),SKHEAD,HEAD,I,O).
488
489body_for_mpred_2((fwc),HwSk,HEAD,I,O):- HwSk\=if_missing(_,_), sub_term(Sk,HwSk),is_skolem_arg(Sk),subst(HwSk,Sk,Var,H),
490 subst(H,Var,NewVar,NewH),head_for_skolem(NewH,SKHEAD,skolem(NewVar,Sk)), !,
491 body_for_mpred_2((fwc),SKHEAD,HEAD,I,O).
492
493body_for_mpred_2((fwc),H,HEAD,{skolem(In,NewOut)},true):- head_for_skolem(H,HEAD,skolem(In,NewOut)),!.
494body_for_mpred_2((fwc),H,HEAD,skolem(In,NewOut),true):- head_for_skolem(H,HEAD,skolem(In,NewOut)).
495body_for_mpred_2(_Mode,~(Head),~(Head),skolem(_,_),true).
497body_for_mpred_2(_Mode,Head,Head,skolem(In,Out),{ignore(In=Out)}).
498
499body_for_mpred_2(Mode,Head,HeadO,(X & Y),XY):-
500 body_for_mpred_2(Mode,Head,HeadM,X,XX),body_for_mpred_2(Mode,HeadM,HeadO,Y,YY),
501 conjoin_maybe(XX,YY,XY),!.
502
503body_for_mpred_2(Mode,Head,HeadO,(X , Y),XY):-
504 body_for_mpred_2(Mode,Head,HeadM,X,XX),body_for_mpred_2(Mode,HeadM,HeadO,Y,YY),
505 conjoin_maybe(XX,YY,XY),!.
506
507body_for_mpred_2(Mode,Head,HeadO,(X ; Y),(XX ; YY)):-
508 body_for_mpred_2(Mode,Head,HeadM,X,XX),
509 body_for_mpred_2(Mode,HeadM,HeadO,Y,YY),!.
510
511
512body_for_mpred_2(_Mode,Head,Head,poss(X),poss(X)).
513body_for_mpred_2(_Mode,Head,Head,poss(X),{loop_check(\+ ~(X),true)}).
516body_for_mpred_2(Mode,Head,NewHead,B,BBB):- once(reduce_literal(B,BB)),B\=@=BB,!,body_for_mpred_1(Mode,Head,NewHead,BB,BBB).
517body_for_mpred_2(Mode,Head,HeadO,proven_tru(H),(HH)):- !,body_for_mpred_2(Mode,Head,HeadO,H,HH).
518body_for_mpred_2(Mode,Head,HeadO,once(H),(HH)):- !,body_for_mpred_2(Mode,Head,HeadO,H,HH).
519body_for_mpred_2(Mode,Head,HeadO,proven_neg(H),(HH)):- !,body_for_mpred_2(Mode,Head,HeadO,~H,HH).
520body_for_mpred_2(_Mode,Head,Head,different(A,B),{dif:dif(A,B)}).
521body_for_mpred_2(_Mode,Head,Head,A,{A}):-a(prologBuiltin,A),!.
522body_for_mpred_2(_Mode,Head,Head,A,A).
523
524
531reduce_literal(A,A):-is_ftVar(A),!.
532reduce_literal(~(A),~(A)):-is_ftVar(A),!.
533reduce_literal(~(different(P3, R3)),not_different(P3, R3)).
534reduce_literal(~(mudEquals(P3, R3)),different(P3, R3)).
536reduce_literal(~(termOfUnit(P3, R3)),different(P3, R3)).
537reduce_literal(~(equals(P3, R3)),different(P3, R3)).
538reduce_literal(termOfUnit(P3, R3),skolem(P3, R3)).
539reduce_literal(~({A}),AA):- reduce_literal(~(A),AA), AA \=@= ~(A),!.
540reduce_literal(~(A),~(A)):-!.
541reduce_literal(A,A).
542
543
550can_use_hack(two_implications):-!,fail.
551can_use_hack(X):- did_use_hack(X).
552
559did_use_hack(X):-wdmsg(did_use_hack(X)).
560
561
562
569boxlog_to_pfc_pass_4(IN,OUT):-quietly(leave_as_is(IN)),!,IN=OUT.
570boxlog_to_pfc_pass_4(H, HH):-is_list(H),!,must_maplist(boxlog_to_pfc_pass_4,H,HH).
571boxlog_to_pfc_pass_4(IN,OUT):-once(demodal_sents('$VAR'('KB'),IN,MID)),IN\=@=MID,!,boxlog_to_pfc_pass_4(MID,OUT).
572boxlog_to_pfc_pass_4(IN,OUT):-once(subst_except(IN,not,~,MID)),IN\=@=MID,!,boxlog_to_pfc_pass_4(MID,OUT).
573boxlog_to_pfc_pass_4(IN,OUT):-once(subst_except(IN,poss,possible_t,MID)),IN\=@=MID,!,boxlog_to_pfc_pass_4(MID,OUT).
574
575boxlog_to_pfc_pass_4((V:- TRUE),VE):- is_true(TRUE),boxlog_to_pfc_pass_4(V,VE),!.
576boxlog_to_pfc_pass_4((H:- B),(HH:- BB)):- !,boxlog_to_pfc_pass_4(H,HH),boxlog_to_pfc_pass_4(B,BB).
577boxlog_to_pfc_pass_4((H & B),(HH , BB)):- !,boxlog_to_pfc_pass_4(H,HH),boxlog_to_pfc_pass_4(B,BB).
578boxlog_to_pfc_pass_4((H v B),(HH ; BB)):- !,boxlog_to_pfc_pass_4(H,HH),boxlog_to_pfc_pass_4(B,BB).
579boxlog_to_pfc_pass_4((H , B),(HH , BB)):- !,boxlog_to_pfc_pass_4(H,HH),boxlog_to_pfc_pass_4(B,BB).
580boxlog_to_pfc_pass_4((H ; B),(HH ; BB)):- !,boxlog_to_pfc_pass_4(H,HH),boxlog_to_pfc_pass_4(B,BB).
581boxlog_to_pfc_pass_4(H,O):- H=..[N,nesc(F)],kb_nlit(_,N),nonvar(F),!,HH=..[N,F],boxlog_to_pfc_pass_4(HH,O).
582
583boxlog_to_pfc_pass_4(IN,OUT):-demodal_sents(_KB,IN,M),IN\=@=M,!,boxlog_to_pfc_pass_4(M,OUT).
584
585
586boxlog_to_pfc_pass_4( H, HH):- H=..[F|ARGS],!,boxlog_to_pfc_pass_4(ARGS,ARGSO),!,HH=..[F|ARGSO].
587boxlog_to_pfc_pass_4(BL,PTTP):- baseKB:as_prolog_hook(BL,PTTP).
588
589:- fixup_exports.