    1% File: /opt/PrologMUD/pack/logicmoo_base/prolog/logicmoo/mpred/mpred_type_wff.pl
    2
    3:- module(mpred_type_wff, []).     
    4
    5%:- include('mpred_header.pi').

mpred_type_wff

% Provides a common set of operators in translation between the several logical languages % % Logicmoo Project PrologMUD: A MUD server written in Prolog % Maintainer: Douglas Miles % Dec 13, 2035 % */

   16:- meta_predicate 
   17        call_last_is_var(0).
   18
   19
   20:- set_how_virtualize_file(bodies).
   21
   22:- kb_shared(functionCorrespondingPredicate/3).
   23
   24
   25
   26is_pfc_clause(B):- mpred_term_expansion(B,Out),!, Out= ((:- cl_assert(pfc(_),_))).
   27
   28is_prolog_clause(B):- compound(B),functor(B,F,_),arg(_,v((:-)),F).

subst_except(:TermSUB, ?Var, ?VarS, :TermSUB) is semidet: Subst Except.

   35subst_except( SUB, Var, VarS,SUB ) :- Var==VarS,!.
   36subst_except(  Var, VarS,SUB,SUB ) :- Var==VarS,!.
   37subst_except(  Var, _,_,Var ) :- \+ compound(Var),!.
   38subst_except(  Var, _,_,Var ) :- leave_as_is(Var),!.
   39subst_except([H|T],B,A,[HH|TT]):- !,subst_except(H,B,A,HH),subst_except(T,B,A,TT).
   40subst_except(HT,B,A,HHTT):- HT=..FARGS,subst_except(FARGS,B,A,[FM|MARGS]),
   41   (atom(FM)->HHTT=..[FM|MARGS];append_termlist(FM,MARGS,HHTT)).
   42
   43
   44
   45:- thread_local t_l:override_hilog/1.

current_hilog(?Dbase_t) is semidet: Current Hilog.

   54current_hilog(Dbase_t):- t_l:override_hilog(Dbase_t),!.
   55current_hilog(t).
   56
   57
   58% ===================================================================
   59% EXPORTS
   60% ===================================================================

isNonVar(?Denotation) is semidet: If Is A Not Variable.

   68isNonVar(Denotation):-not(isSlot(Denotation)).
   69
   70% ===============================================================================================
   71% ===============================================================================================

isSlot(?Denotation, ?Denotation) is semidet: If Is A Slot.

   81isSlot(Denotation,Denotation):- isVarProlog(Denotation),!.
   82isSlot(Denotation,PrologVar):- isVarObject(Denotation,PrologVar),!.
   83
   84% ===============================================================================================
   85% ===============================================================================================

isHiddenSlot(?Term) is semidet: If Is A Hidden Slot.

   94isHiddenSlot(_Term):-fail.
   95
   96% ===============================================================================================
   97% ===============================================================================================

isVarProlog(?A) is semidet: If Is A Variable Prolog.

  106isVarProlog(A):-((var(A);A='$VAR'(_))).
  107
  108% ===============================================================================================
  109% ===============================================================================================

isVarObject(?Denotation) is semidet: If Is A Variable Object.

  118isVarObject(Denotation):-((
  119		  isObject(Denotation,_BaseType),
  120		  arg(1,Denotation,Value),!,isSlot(Value))).

isVarObject(?Denotation, ?Value) is semidet: If Is A Variable Object.

  129isVarObject(Denotation,Value):-((
  130		  isObject(Denotation,_BaseType),
  131		  arg(1,Denotation,Value),!,isSlot(Value))).
  132
  133% ===============================================================================================
  134% ===============================================================================================

isObject(?Denotation, ?BaseType) is semidet: If Is A Object.

  143isObject(Denotation,BaseType):-
  144	(((atom(BaseType) ->
  145		  (atom_concat('$',BaseType,F),functor(Denotation,F,2));
  146		  (functor(Denotation,F,2),atom_concat('$',BaseType,F))
  147		 ),!)).
  148
  149% ===============================================================================================
  150% ===============================================================================================

isQualifiableAsClass(:TermAtom) is semidet: If Is A Qualifiable Converted To Class.

  159isQualifiableAsClass(Atom):-atom(Atom),!.
  160isQualifiableAsClass('$Class'(Atom,_)):-atom(Atom),!.

isQualifiableAs(?Denotation, ?BaseType, ?Value) is semidet: If Is A Qualifiable Converted To.

  169isQualifiableAs(Denotation,BaseType,Value):-
  170		  isObject(Denotation,BaseType),
  171		  arg(1,Denotation,Value).
  172
  173% ===============================================================================================
  174% ===============================================================================================

isQualifiedAs(?Denotation, ?VALUE2, ?VALUE3) is semidet: If Is A Qualified Converted To.

  183isQualifiedAs(Denotation,_,_):-not(compound(Denotation)),!,fail.
  184isQualifiedAs(Denotation,BaseType,Value):-
  185		  isQualifiedAs(Denotation,BaseType,Value,_SubType).

isQualifiedAs(?Denotation, ?BaseType, ?Value, ?SubType) is semidet: If Is A Qualified Converted To.

  193isQualifiedAs(Denotation,BaseType,Value,SubType):-
  194		  isObject(Denotation,BaseType),
  195		  arg(1,Denotation,Value),
  196		  arg(2,Denotation,List),
  197		  lastImproperMember(BaseType,SubType,List).
  198
  199% ===============================================================================================
  200% ===============================================================================================
  201:- style_check(-singleton).

lastImproperMember(?Default, ?Default, :TermList) is semidet: Last Improper Member.

  210lastImproperMember(Default,Default,List):-isVarProlog(List),!.
  211lastImproperMember(Default,Default,[]):-!.
  212lastImproperMember(Default,SubType,List):-proper_list(List),last(SubType,List).
  213lastImproperMember(Default,SubType,[SubType|End]):-isVarProlog(End),!.
  214lastImproperMember(Default,SubType,[_|Rest]):-
  215	lastImproperMember(Default,SubType,Rest),!.
  216	
  217% ===============================================================================================
  218% ===============================================================================================

isQualifiedAndKnownAs(?Denotation, ?BaseType, ?Value) is semidet: If Is A Qualified And Known Converted To.

  227isQualifiedAndKnownAs(Denotation,BaseType,Value):-
  228		  isQualifiedAs(Denotation,BaseType,Value),!,
  229		  not(isVarProlog(Value)).
  230
  231% ===============================================================================================
  232% ===============================================================================================

isQualifiedAndVarAs(?Denotation, ?BaseType, ?Value) is semidet: If Is A Qualified And Variable Converted To.

  241isQualifiedAndVarAs(Denotation,BaseType,Value):-
  242		  isQualifiedAs(Denotation,BaseType,Value),!,
  243		  isVarProlog(Value).
  244
  245% ===============================================================================================
  246% ===============================================================================================

isQualifiedAndVarAndUnifiable(?Denotation, ?BaseType, ?NValue) is semidet: If Is A Qualified And Variable And Unifiable.

  255isQualifiedAndVarAndUnifiable(Denotation,BaseType,NValue):-
  256		  isQualifiedAs(Denotation,BaseType,Value),!,
  257		  (isVarProlog(Value);
  258		  (\+ \+ NValue=Value)),!.
  259
  260% ===============================================================================================
  261% ===============================================================================================
  262/*
  263:- dynamic(isBodyConnective/1).
  264
  265
  266
  267%% isBodyConnective( ?Funct) is semidet.
  268%
  269% If Is A Body Connective.
  270%
  271isBodyConnective(Funct):-atom_concat(_,'_',Funct),!.
  272isBodyConnective(Funct):-atom_concat('t~',_,Funct),!.
  273isBodyConnective(Funct):-atom_concat('f~',_,Funct),!.
  274isBodyConnective(Funct):-member(Funct,[and,or,until,',',';',':-',unless,xor,holdsDuring]). % Other Propositional Wrhtml_appers
  275*/

isEntityref(?Var, ?Var) is semidet: If Is A Entityref.

  283isEntityref(Var,Var):-isSlot(Var),!.
  284isEntityref(Term,A):-Term=..[F,A,B],!,atom_concat('$',_,F),!.
  285
  286
  287% ===============================================================================================
  288% ===============================================================================================

isLiteralTerm(:TermA) is semidet: If Is A Literal Term.

  297isLiteralTerm(A):-isLiteralTerm_util(A),!.
  298isLiteralTerm(not(A)):-isLiteralTerm_util(A),!.

isLiteralTerm_util(?A) is semidet: If Is A Literal Term Util.

  307isLiteralTerm_util(A):-var(A),!.
  308isLiteralTerm_util('$VAR'(_)):-!.
  309isLiteralTerm_util(string(_)):-!.
  310isLiteralTerm_util(A):-not(compound(A)),!.
  311isLiteralTerm_util(A):-string(A).
  312
  313% ===============================================================================================
  314% ===============================================================================================

isEntitySlot(?Term) is semidet: If Is A Entity Slot.

  323isEntitySlot(Term):-isSlot(Term),!.
  324isEntitySlot(Term):-not(compound(Term)),!.
  325isEntitySlot(Term):-isEntityFunction(Term,FnT,ArgsT),!.
  326
  327% ===============================================================================================
  328% ===============================================================================================

isEntityFunction(?Term, ?FnT, ?ArgsT) is semidet: If Is A Entity Function.

  337isEntityFunction(Term,FnT,ArgsT):-isSlot(Term),!,fail.
  338isEntityFunction(Term,FnT,ArgsT):-atomic(Term),!,fail.
  339isEntityFunction(Term,FnT,ArgsT):-Term=..[FnT|ArgsT],is_function(FnT).
  340
  341% ===============================================================================================
  342% ===============================================================================================

isNonCompound(:TermVar) is semidet: If Is A Not Compound.

  351isNonCompound(Var):-isSlot(Var),!.
  352isNonCompound(Var):-not(compound(Var)),!.
  353isNonCompound(svar(_,_)):-!.
  354isNonCompound(Var):-is_ftText(Var),!.
  355isNonCompound(string(Var)):-!.
  356
  357% ===============================================================================================
  358% ===============================================================================================

logical_functor_ft(?F) is semidet: Logical Functor Format Type.

  367logical_functor_ft(F):-is_sentence_functor(F).
  368logical_functor_ft((':-')).
  369logical_functor_ft((',')).
  370
  371% ===============================================================================================
  372% ===============================================================================================

non_assertable(:TermWW, ?WW) is semidet: Not Assertable.

  381non_assertable(WW,isVar(WW)):- var(WW),!.
  382non_assertable(_:WW,Why):- !,non_assertable(WW,Why).
  383non_assertable(W,notAssertable(F)):- compound(W),get_functor(W,F),cheaply_u(notAssertable(F)).
  384% non_assertable(WW,Why):- db_prop_add
  385
  386% ===============================================================================================
  387% ===============================================================================================
  388
  389:- was_export(logical_functor_pttp/1).

logical_functor_pttp(?X) is semidet: Logical Functor Pttp.

  398logical_functor_pttp(X):-not(atom(X)),!,fail.
  399logical_functor_pttp(props):-!,fail.
  400logical_functor_pttp(X):-pttp_nnf_pre_clean_functor(A,B,_),(X==A;X==B),!.
  401logical_functor_pttp(&).
  402logical_functor_pttp(~).
  403logical_functor_pttp(<=>).
  404logical_functor_pttp(=>).
  405logical_functor_pttp(v).

is_quantifier(?F) is semidet: If Is A Quantifier.

  412is_quantifier(F):- pttp_nnf_pre_clean_functor(F,(all),[]);pttp_nnf_pre_clean_functor(F,(ex),[]).
  413
  414
  415
  416%% pttp_nnf_pre_clean_functor( ?A, ?A, ?VALUE3) is semidet.
  417%
  418% Pttp Negated Normal Form Pre Clean Functor.
  419%
  420pttp_nnf_pre_clean_functor('&',(,),[]).
  421pttp_nnf_pre_clean_functor('v',(;),[]).
  422pttp_nnf_pre_clean_functor(and,(,),[]).
  423pttp_nnf_pre_clean_functor(('/\\'), (,),[]).
  424pttp_nnf_pre_clean_functor(or,(;),[]).
  425pttp_nnf_pre_clean_functor(('\\/'),(;),[]).
  426% pttp_nnf_pre_clean_functor('::',(:),[]).
  427pttp_nnf_pre_clean_functor(~,(-),[]).
  428pttp_nnf_pre_clean_functor(not,(-),[]).
  429pttp_nnf_pre_clean_functor(~,(-),[]).
  430pttp_nnf_pre_clean_functor(implies,(=>),[]).
  431pttp_nnf_pre_clean_functor(imp,(=>),[]).
  432pttp_nnf_pre_clean_functor(equiv,(<=>),[]).
  433%pttp_nnf_pre_clean_functor(->,(=>),[]).
  434pttp_nnf_pre_clean_functor(entailed_from,(:-),[]).
  435pttp_nnf_pre_clean_functor(implied_by,(:-),[]).
  436pttp_nnf_pre_clean_functor(forAll,(all),[]).
  437pttp_nnf_pre_clean_functor(thereExists,(ex),[]).
  438pttp_nnf_pre_clean_functor(forall,(all),[]).
  439pttp_nnf_pre_clean_functor(exists,(ex),[]).
  440pttp_nnf_pre_clean_functor(A,A,[]):-atom(A).
  441pttp_nnf_pre_clean_functor(A,A,[]).

pttp_nnf_post_clean_functor(?VALUE1, ?VALUE2) is semidet: Pttp Negated Normal Form Post Clean Functor.

  450pttp_nnf_post_clean_functor('&',',').
  451pttp_nnf_post_clean_functor('v',';').
  452
  453
  454% ===============================================================================================
  455% ===============================================================================================

is_neg(:TermARG1) is semidet: If Is A Negated.

  464is_neg(not(_)).

is_pos(?One) is semidet: If Is A Pos.

  472is_pos(One):- get_functor(One,F),!,not(is_log_op(F)).
  473
  474%= %= :- was_export(is_log_sent/1).

is_log_sent(?S) is semidet: If Is A Log Sentence.

  482is_log_sent(S):- get_functor(S,F,_),is_log_op(F).

not_log_op(?OP) is semidet: Not Log Oper..

  491not_log_op(OP):- not(is_log_op(OP)).
  492%= %= :- was_export(is_log_op/1).

is_log_op(?OP) is semidet: If Is A Log Oper..

  500 % is_log_op(OP):- current_predicate(OP,M:P),current_predicate(G,meta_predicate(_)),!.
  501is_log_op(OP):- atomic(OP),if_defined(to_dlog_ops(OPS)),!,(member(OP=_,OPS);member(_=OP,OPS)).

quant_singles(?Wff, ?VALUE2, :TermARG3, ?Wff) is semidet: Quanitify Single Vars

  509quant_singles(Wff,_,[],Wff).
  510quant_singles(Wff,Exists,[S|Singles],NewWff):-   
  511   (already_quantified(Wff,S) 
  512     -> WffM = Wff ; 
  513     add_1quantifier(Exists,S,Wff,WffM)),!,
  514   quant_singles(WffM,Exists,Singles,NewWff),!.
  515
  516add_1quantifier(Exists,S,Wff,WffM) :- \+ compound(Wff),!,WffM =..[Exists,S,Wff].
  517add_1quantifier(Exists,S,Wff,WffM) :- Wff=..[Q,X,Fml],is_quant_f(Q),add_1quantifier(Exists,S,Fml,Wff1),WffM=..[Q,X,Wff1].
  518add_1quantifier(Exists,S,Wff,WffM) :- Wff=..[Q,N,X,Fml],is_quant_f(Q),add_1quantifier(Exists,S,Fml,Wff1),WffM=..[Q,N,X,Wff1].
  519add_1quantifier(Exists,S,Wff,WffM) :- WffM =..[Exists,S,Wff].
  520
  521
  522already_quantified(Wff,S) :- each_subterm(Wff,SubTerm),compound(SubTerm), already_quanted_01(SubTerm,S).
  523
  524already_quanted_01(SubTerm,S):- SubTerm=..[OtherExists,SO,_],
  525   member(OtherExists,[all,exists]),!,
  526  (is_list(SO)->member(V,SO);V=SO),
  527   same_vars(V,S).
  528
  529already_quanted_01(SubTerm,S):- 
  530    SubTerm=..[OtherExists,_,SO,_],
  531    member(OtherExists,[atleast,quant,atmost,exactly]),
  532    same_vars(SO,S).
  533    
  534is_quant_f(Q):- arg(_,v(atleast,atmost,exactly,all,exists),Q).
  535is_quant_f(Q):- arg(_,v(no,some,one,two,quant),Q).
  536
  537
  538%= %= :- was_export(defunctionalize/2).
  539
  540
  541
  542
  543
  544
  545/*
  546
  547
  548  defunctionalize( +FmlIn, -FmlOut, [options...]).
  549
  550
  551   converts terms like...
  552
  553         loves(joe,mary)
  554
  555   Into...
  556
  557         poss(loves(joe,mary)) => nesc(loves(joe,mary)).
  558
  559   settings are...
  560
  561*/

defunctionalize(?Wff, ?WffO) is det: Defunctionalize.

  570defunctionalize((H:-B),WffO):- nonvar(H),!,defunctionalize(':-',(H:-B),WffO),!.
  571defunctionalize(Wff,WffO):- defunctionalize('=>',Wff,WffO),!.
  572% defunctionalize(Wff,WffO):- locally_tl(dont_use_mudEquals,defunctionalize(',',Wff,WffO)).
  573
  574defunctionalize_each(Wff,WffO):-must_maplist(defunctionalize,Wff,WffO).

defunctionalize(?OP, ?Wff, ?WffO) is det: Defunctionalize.

  580defunctionalize(OP ,Wff,WffO):- defunctionalize_op(OP,Wff,WffM),!,WffO=WffM.
  581
  582
  583defunctionalize_op(_OP,WffO,WffO):- not_ftCompound(WffO),!.
  584defunctionalize_op(OP,(H:- B),WffO):- 
  585   quietly(defunctionalize_did(OP,B,PREB,POSTB,Function,NewVar)),
  586   subst(H,Function,NewVar,HH),
  587   occurrences_of_var(Function,B,Count),
  588   (HH\==H -> defunctionalize(OP,(HH:- (ignore(PREB),POSTB)),WffO);
  589   (Count>1 -> defunctionalize(OP,(H:- (POSTB , ignore(PREB))),WffO);
  590     defunctionalize(OP,(H:- (POSTB)),WffO))).
  591 
  592
  593defunctionalize_op(OP,(H:- B),WffO):- 
  594   quietly(defunctionalize_did(OP,H,PREH,POSTH,Function,NewVar)),!,
  595   subst(B,Function,NewVar,BB),
  596   (BB==B -> 
  597     =((H:- (B)),WffO) ; 
  598     defunctionalize(OP,(POSTH:- (BB,PREH)),WffO)).
  599
  600defunctionalize_op(OP,Wff,WffO):- 
  601  (defunctionalize_did(OP,Wff,PREWff,POSTWff,_Function,_NewVar)),!,
  602  WffM=..[OP,PREWff,POSTWff],
  603  defunctionalize_op(OP,WffM,WffO).
  604defunctionalize_op(_,Wff,Wff).
  605
  606
  607defunctionalize_did(OP,Wff,PredifiedFunction,NextWff,Function,NewVar):- 
  608  sub_term(SubTerm,Wff),
  609  compound(SubTerm),
  610  \+ is_precond_like(SubTerm),
  611  arg(N,SubTerm,Function), N<4,
  612  compound(Function),
  613  quietly(is_function_expr(OP,Function)),
  614  quietly(\+ has_function(OP,Function)),
  615  must(quietly((function_to_predicate(Function,NewVar,PredifiedFunction),
  616  subst(Wff,Function,NewVar,NextWff)))),!.
  617
  618
  619
  620is_precond_like(Var):- \+ compound(Var),!.
  621is_precond_like(SubTerm):- is_ftEquality(SubTerm),!.
  622is_precond_like(spft(_,_,_)):- !.
  623is_precond_like({_}).
  624
  625has_function(OP,Term):- 
  626 compound(Term),
  627 \+ is_precond_like(Term),
  628 arg(_,Term,Function), 
  629 (is_function_expr(OP,Function);has_function(OP,Function)),!.

correct_negations(?Op, :TermX, ?O) is semidet: Correct Negations.

  636correct_negations(Op,(~({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).
  637correct_negations(Op,(-({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).
  638correct_negations(Op,(not({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).
  639correct_negations(Op,(notz({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).
  640correct_negations(Op,(assertable_not({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).
  641correct_negations(Op,(\+({X})),O):-nonvar(X),wrap_in_neg_functor(Op,X,O).

wrap_in_neg_functor(?VALUE1, ?X, ?X) is semidet: Wrap In Negated Functor.

  650wrap_in_neg_functor(clause,X,assertable_neg(X)).
  651wrap_in_neg_functor(mpred,X,not(X)).
  652wrap_in_neg_functor(callable,X, (\+(X))).

contains_no_negs(?X) is semidet: Contains No Negateds.

  663contains_no_negs(X):- \+ contains_negs(X).

contains_negs(?X) is semidet: Contains Negateds.

  672contains_negs(X):-sub_term(Sub, X),compound(Sub),Sub=not(_).

is_modal(?MODAL, ?VALUE2) is semidet: If Is A Modal.

  682is_modal(MODAL,_):- \+ compound(MODAL),!,fail.
  683is_modal(MODAL,BDT):- (MODAL = nesc(BDT,_) ; MODAL = poss(BDT,_)),!,nop(nonvar(BDT)).
  684is_modal(MODAL,BDT):- (MODAL = nesc(BDT) ; MODAL = poss(BDT)),!.
  685is_modal(MODAL,BDT):- arg(_,MODAL,ARG),is_modal(ARG,BDT).
  686
  687
  688contains_modal(G):- is_modal(G,_),!.
  689contains_modal(G):- contains_modalization_pred(G),!.

contains_modalization_pred(?MODAL, ?VALUE2) is semidet: Contains a modalizion predicate like possible_t or known_t

  696contains_modalization_pred(MODAL):- compound(MODAL),functor(MODAL,F,_),
  697  (atom_concat(_,'_t',F);atom_concat(_,'_f',F);(arg(_,MODAL,ARG),contains_modalization_pred(ARG))).

contains_var_lits(?Fml, ?Var, ?Lits) is semidet: Contains Variable Literals.

  706contains_var_lits(Fml,Var,Lits):- findall(Lit,contains_t_var(Fml,Var,Lit),Lits).

same_var(?Var, ?Fml) is semidet: Same Variable.

  713same_var(Var,Fml):- Var=@=Fml,!.

contains_type_lits(?Fml, ?Var, ?Lits) is semidet: Contains Type Literals.

  721contains_type_lits(Fml,Var,Lits):- findall(T,(contains_t_var(Fml,Var,Lit),get_isa(Lit,O,T),same_var(O,Var)),Lits).

contains_t_var(?Fml, ?Var, ?Term) is semidet: Contains True Structure Variable.

  729contains_t_var(Fml,Var,Term):- each_subterm(Fml,Term),compound(Term),arg(_,Term,O),same_var(O,Var).

get_isa(?Lit, ?I, ?TT) is semidet: get (isa/2).

  739get_isa(Lit,I,TT):- compound(Lit),get_isa0(Lit,I,TT).

get_isa0(?IT, ?I, ?TT) is semidet: get (isa/2) Primary Helper.

  747get_isa0(isa(I,T),I,TT):- guess_type_name(T,TT),!.
  748get_isa0(IT,I,TT):- IT=..[T,I],is_colection_name(IT,T,TT),!.

is_colection_name(?IT, ?T, ?TT) is semidet: If Is A Colection Name.

  757is_colection_name(_,-,_):- !,fail.
  758is_colection_name(IT,T,TT):- atom(T),atom_length(T,TL),TL>2,not(atom_contains(T,'_')),not(predicate_property(IT,_)),guess_type_name(T,TT).

leave_as_is(:TermV) is semidet: Leave Converted To If Is A.

  767leave_as_is(V):- is_ftVar(V),!.
  768leave_as_is(V):- \+ compound(V),!.
  769leave_as_is(poss(_,_)):-!,fail.
  770leave_as_is((_,_)):-!,fail.
  771leave_as_is((_ :-_ )):-!,fail.
  772leave_as_is((_;_)):-!,fail.
  773leave_as_is((_/_)):-!,fail.
  774leave_as_is([_|_]):-!,fail.
  775leave_as_is(not(_)):-!,fail.
  776leave_as_is(~_):-!,fail.
  777leave_as_is(V):-loop_check(leave_as_is_db(V)),!.

leave_as_is_db(:TermP) is semidet: Leave Converted To If Is A Database.

  788leave_as_is_db('$VAR'(_)).
  789leave_as_is_db('aNARTFn'(_)).
  790leave_as_is_db('comment'(_,_)).
  791
  792leave_as_is_db(infer_by(_)).
  793leave_as_is_db(b_d(_,_,_)).
  794leave_as_is_db(ct(_,_)).
  795% leave_as_is_db('tColOfCollectionSubsetFn'(_,_)).
  796leave_as_is_db(ignore(_)).
  797leave_as_is_db(isa(_,_)).
  798leave_as_is_db(P):-prequent(P).
  799leave_as_is_db(C):-get_functor(C,F),loop_check(leave_as_is_functor(F)).

leave_as_is_functor(?Atom) is semidet: Leave Converted To If Is A Functor.

  809leave_as_is_functor(Atom):- \+ atom(Atom),!,fail.
  810leave_as_is_functor('TINYKB-ASSERTION').
  811leave_as_is_functor('skolem').
  812leave_as_is_functor('$VAR').
  813leave_as_is_functor('kbMark').
  814leave_as_is_functor('z_unused').
  815leave_as_is_functor('wid').
  816leave_as_is_functor('genlMt').
  817% leave_as_is_functor('{}').
  818leave_as_is_functor(F):-cheaply_u(rtArgsVerbatum(F)).
  819% leave_as_is_functor(F):-loop_check(cheaply_u(rtReformulatorDirectivePredicate(F))).

prequent(:TermG) is semidet: Prequent.

  828prequent(original(_)).
  829prequent(mudEquals(_,_)).
  830prequent(skolem(_,_,_)).
  831prequent(different(_,_)).
  832prequent(argInst(_,_,_)).
  833prequent(G):-functor(G,call_builtin,_).
  834prequent(G):-functor(G,call_u,_).
  835prequent(G):-functor(G,not_call_builtin,_).

kb_nlit(?KB, ?Neg) is semidet: Knowledge Base Nlit.

  844kb_nlit(_KB,Neg):-member(Neg,[(not),(~),(-),(~)]).

set_is_lit(?A) is semidet: Set If Is A Literal.

  853set_is_lit(A):-when(nonvar(A),\+ is_ftVar(A)),!.
  854
  855
  856
  857
  858
  859
  860
  861
  862%= %= :- was_export(term_slots/2).

term_slots(?Term, ?Slots) is semidet: Term Slots.
term_slots(Term,Slots):-term_singleslots(Term, [],NS, [],S),append(NS,S,Slots).

  873:- export(head_singletons/2).
  874%head_singletons(Pre,Post):-  !, quietly((\+ ignore(must( \+ head_singles0(Pre,Post))))).

head_singletons(?Pre, ?Post) is semidet: Head Singletons.

  882head_singletons(Pre,Post):-   quietly((\+ ignore(show_failure(why, \+ head_singles0(Pre,Post))))),!,dumpST.
  883:- export(head_singles0/2).
  884:- export(head_singles01/2).
  885% TODO how to adderess head_singles0(true, if_missing(foob(_G754993), foob(a)))?
  886% also should fix  (head_singles0(true, nt( foob(_G764659),  (call_u(foob(_G764666)), foob(_G764666)\==foob(a)), rhs([foob(a)]))))).

head_singles0(?Pre, :TermPost) is semidet: Head Singles Primary Helper.

  894head_singles0(Pre,Post):-is_ftVar(Post),!,head_singles01(Pre,Post).
  895head_singles0(_,Post):- \+ compound(Post),!,fail.
  896head_singles0(Pre,M:Post):-atom(M),!,head_singles0(Pre,Post).
  897head_singles0(Pre,[Post|More]):-nonvar(Post),!,head_singles0(Pre,Post),head_singles0((Pre,Post),More).
  898head_singles0(Pre,'if_missing'(_,Post)):-nonvar(Post),!,head_singles0((Pre,Pre2),Post).
  899head_singles0(Pre,'->'(Pre2,Post)):-nonvar(Post),!,head_singles0((Pre,Pre2),Post).
  900head_singles0(Pre,'/'(Post,Pre2)):-nonvar(Post),!,head_singles0((Pre,Pre2),Post).
  901head_singles0(Pre,rhs(Post)):- nonvar(Post),mpred_rule_hb(Post,Post2,Pre2), !,head_singles0((Pre,Pre2),Post2).
  902head_singles0(Pre,mdefault(Post)):- nonvar(Post),mpred_rule_hb(Post,Post2,Pre2), !,head_singles0((Pre,Pre2),Post2).
  903head_singles0(Pre,nt(_,Pre2,Pre3,Post)):-nonvar(Post),!,head_singles0((Pre,Pre2,Pre3),Post).
  904head_singles0(Pre,pt(_,Pre2,Post)):-nonvar(Post),!,head_singles0((Pre,Pre2),Post).
  905head_singles0(Pre,Post):- nonvar(Post),mpred_rule_hb(Post,Post2,Pre2),Post2\=@=Post,!,head_singles0((Pre,Pre2),Post2).
  906head_singles0(Pre,Post):-head_singles01(Pre,Post).

head_singles01(?Pre, ?Post) is semidet: Head Singles Primary Helper Secondary Helper.

  915head_singles01(Pre,Post):-
  916  quietly((
  917    term_singleslots(Post,_,CSingles),
  918    term_slots(Pre,PreVars),!,
  919    subtract_eq(CSingles,PreVars,Bad),!,Bad\==[])).

get_kv(?KV, ?X, ?Y) is semidet: Get Kv.

  928/*get_kv(X=Y,X,Y):- !.
  929get_kv(X-Y,X,Y):- !.
  930get_kv(KV,X,Y):- functor(KV,_,1),KV=..[X,Y],!.
  931get_kv(KV,X,Y):- arg(1,KV,X),arg(2,KV,Y),!.
  932*/

is_function(?F) is semidet: If Is A Function.

  941is_function(F):- is_ftVar(F),!,fail.
  942is_function(F):- clause_b(tFunction(F)).
  943is_function(F):- \+ atom(F),!,fail.
  944is_function(uU).
  945is_function(F):- atom_concat('sk',_Was,F),!,fail.
  946is_function(F):- atom_concat(_Was,'Fn',F),!.
  947
  948is_function_expr(OP,Function):- compound(Function),!,compound_name_arity(Function,F,A),is_function_pfa(OP,Function,F,A).
  949
  950is_function_expr(Function):- is_function_expr(assert,Function).
  951
  952
  953has_ftVar(Body):-is_ftVar(Body),!.
  954has_ftVar(Body):-compound(Body),arg(_,Body,Arg),has_ftVar(Arg),!.

is_function_pfa(OP, ?VALUE1, ?F, ?VALUE3) is semidet: If Is A Function.

  960is_function_pfa(_,_,F,_):- \+ atom(F),!,fail.
  961is_function_pfa(_,_,spft,_):-!,fail.
  962is_function_pfa(_,_,'uSubLQuoteFn',_):- !,fail.
  963is_function_pfa(_,_,'xQuoteFn',_):- !,fail.
  964is_function_pfa(_,_,'uNARTFn',_):- !,fail.
  965is_function_pfa(_,Body,F,_):- has_ftVar(Body),is_function(F).
  966is_function_pfa(_,_,'tCol_CollectionSubsetFn',_).
  967is_function_pfa((:-),_,F,_):- atom_concat(_Was,'Fn',F),!.
  968
  969% is_function_pfa(OP,P,_,_):- loop_check(leave_as_is(P)),!,fail.
  970% is_function_pfa(OP,_,F,_):- loop_check(is_log_op(F)),!,fail.
  971% is_function_pfa(OP,_,F,A):- A2 is A+1, current_predicate(F/A2), \+ current_predicate(F/A).
  972
  973%:- ain(isa(I,C)<=(ttRelationType(C),baseKB:isa(I,C))).

is_ftEquality(:TermTerm) is semidet: If Is A Format Type Equality.

  982is_ftEquality(Term):- is_ftVar(Term),!,fail.
  983%is_ftEquality(Term):- get_pred(Term,Pred),is),!,(Pred==mudEquals;genlPreds(Pred,equals);clause_asserted(prologEquality(Pred))),!.
  984is_ftEquality(mudEquals(_,_)).
  985is_ftEquality(skolem(_,_,_)).
  986is_ftEquality(equals(_,_)).
  987is_ftEquality(termOfUnit(_,_)).
  988
  989
  990:- thread_local(t_l:dont_use_mudEquals/0).
  991
  992
  993
  994
  995:- export(mpred_functor/3).
  996mpred_functor(Pred,Pred,A):-var(Pred),!,between(1,9,A).
  997mpred_functor(F/A,F,A):-!,probably_arity(F,A).
  998mpred_functor(_:Pred,F,A):-!,mpred_functor(Pred,F,A).
  999mpred_functor(F,F,A):-atom(F),!,probably_arity(F,A).
 1000mpred_functor(Pred,F,A):-functor_safe(Pred,F,A).
 1001
 1002probably_arity(F,A):-(integer(A)->true;(arity(F,A)*->true;between(1,9,A))).

ensure_quantifiers(?Wff, ?WffO) is semidet: Ensure Quantifiers.

 1012ensure_quantifiers(Wff:- B,WffO):- B== true,!, ensure_quantifiers(Wff,WffO).
 1013ensure_quantifiers(Wff:- B,Wff:- B):- !.
 1014% ensure_quantifiers(Wff,Wff):-!.
 1015ensure_quantifiers(WffI,WffO):-
 1016 subst(WffI,forall,all,Wff),
 1017 must_det_l((show_failure(why,term_singleslots(Wff,NonSingles,Singles)),
 1018  quant_singles(Wff,'exists',Singles,WffM),quant_singles(WffM,'all',NonSingles,WffO))).

get_pred(?Pred, ?F) is semidet: Get Predicate.

 1028get_pred(Pred,F):- get_functor(Pred,F).
 1029
 1030
 1031
 1032
 1033
 1034:- kb_shared(function_corisponding_predicate/2).

function_to_predicate(?Function, ?NewVar, ?PredifiedFunction) is semidet: Function Converted To Predicate.

 1042function_to_predicate(Function,NewVar,PredifiedFunction):- 
 1043 Function = 'tColOfCollectionSubsetFn'(Col,'tSetOfTheSetOfFn'(NewVar,Formulas)), 
 1044 must(is_ftVar(NewVar)), % \+ is_ftVar(Col),!,
 1045 PredifiedFunction = '&'(isa(NewVar,Col) , Formulas).
 1046
 1047
 1048function_to_predicate(Function,NewVar,PredifiedFunction):- 
 1049  Function=.. [F|ARGS],
 1050  cheaply_u(functionCorrespondingPredicate(F,P,N)),
 1051  fresh_varname(Function,NewVar),
 1052  list_insert_at([P|ARGS],NewVar,N,[PR|Edified]),
 1053  (atom(PR) -> PredifiedFunction=..[PR|Edified] ; PredifiedFunction=..[t,PR|Edified]),!.
 1054
 1055
 1056function_to_predicate(Function,NewVar,mudEquals(NewVar,Function)):- 
 1057 % \+ t_l:dont_use_mudEquals, 
 1058  fresh_varname(Function,NewVar),!.
 1059
 1060
 1061
 1062list_insert_at([A],NewVar,_,[A,NewVar]):-!.  % will append it to the last if too deep
 1063list_insert_at(List,NewVar,0,[NewVar|List]):- !.
 1064list_insert_at([A|List],NewVar,1,[A,NewVar|List]):-!.
 1065list_insert_at([A|List],NewVar,N,[A|NewList]):- N2 is N -1,
 1066   list_insert_at(List,NewVar,N2,NewList).
 1067
 1068
 1069%=

fresh_varname(:TermF, ?NewVar) is semidet: Fresh Varname.

 1075fresh_varname(F,NewVar):-is_ftVar(F),NewVar=F.
 1076fresh_varname(F,NewVar):-var(F),fresh_varname('mudEquals',NewVar).
 1077fresh_varname([F0|_],NewVar):-!,fresh_varname(F0,NewVar).
 1078fresh_varname(F,NewVar):- compound(F),arg(_,F,F1),atom(F1),!,functor(F,F0,_),atom_concat(F0,F1,FN),upcase_atom(FN,FUP),gensym(FUP,VARNAME),NewVar = '$VAR'(VARNAME),!.
 1079fresh_varname(F,NewVar):- functor(F,FN,_),!, upcase_atom(FN,FUP),gensym(FUP,VARNAME),NewVar = '$VAR'(VARNAME),!.
 1080
 1081:- fixup_exports.