1% =========================================
    2% Goal/Plan translating
    3% =========================================
    4:- module(ec_loader,[load_e/1, fix_time_args/3,fix_goal/3, brk_on_bind/1,assert_axiom_2/2, is_e_toplevel/0,
    5  needs_proccess/3,process_ec/2]).    6
    7only_dec_pl(Goal):- into_dec_pl->call(Goal);true.
    8only_lps(Goal):- into_lps->call(Goal);true.
    9:- dynamic(translating_inline/0).   10:- dynamic(translating_files/0).   11:- thread_local(t_l:is_ec_cvt/1).   12into_lps :- (t_l:is_ec_cvt(lps) ; true),!.
   13into_dec_pl :- \+ t_l:is_ec_cvt(lps).
   14no_canon :- true. 
   15reduce_holds_at:- fail.
   16
   17major_debug(Goal):- nop(Goal).
   18
   19assert_to_lps(Stuff):- ignore(ec_lps_convert:assert_lps(Stuff)).
   20
   21
   22pprint_ecp_pl(Type,Form):- \+ into_lps, !, pprint_ecp(Type,Form),!.
   23pprint_ecp_pl(Type,Form):- major_debug(pprint_ecp_cmt(Type,Form)),!.
   24
   25:- use_module(library(logicmoo_common)).   26
   27is_e_toplevel :- prolog_load_context(source,File),prolog_load_context(file,File).
   28
   29:- if(\+ current_prolog_flag(lm_no_autoload,_)).   30:- set_prolog_flag(lm_no_autoload,false).   31:- wdmsg("WARNING: PFC_AUTOLOAD").   32:- endif.   33
   34:- if(\+ current_prolog_flag(lm_pfc_lean,_)).   35:- set_prolog_flag(lm_pfc_lean,false).   36:- wdmsg("WARNING: PFC_NOT_LEAN").   37:- endif.   38
   39:- use_module(library(logicmoo_utils_all)).   40
   41:- use_module(library(pfc_lib)).   42%:- include(library(pfc)).
   43:- baseKB:export(baseKB:spft/4).   44:- system:import(baseKB:spft/4).   45
   46%:- reexport(library('ec_planner/ec_planner_dmiles')).
   47:- reexport(library('ec_planner/ec_reader')).   48
   49
   50:- export_transparent(e_reader_teste/0).   51e_reader_teste:- with_e_sample_tests(load_e),e_reader_teste2.
   52
   53:- export_transparent(e_reader_testec/0).   54e_reader_testec:- with_e_sample_tests(cvt_e_pl).
   55
   56:- export_transparent(e_reader_testec_lps/0).   57e_reader_testec_lps:- with_e_sample_tests(translate_e_to_pfc).
   58
   59:- export_transparent(load_e/1).   60% load_e(F):- load_e_from_translation(F).
   61load_e(F):- into_dec_pl, !, load_e_cond(F, always),!.
   62load_e(F):- load_e_into_memory(F).
   63
   64load_e_from_translation(F):- 
   65  translate_e_to_pfc(F),
   66  calc_pel_filename(F,_,PL),
   67  consult(PL),!.
   68
   69foundations_file('foundations/EC.e').
   70foundations_file('foundations/Root.e').
   71:- export_transparent(load_e_cond/2).   72
   73load_e_cond(F,Cond):- into_dec_pl, cond_load_e(Cond,F).
   74load_e_cond(S0,How):-
   75 must((
   76  ((resolve_local_files(S0,SS), 
   77  SS\==[])
   78   -> must_maplist(load_e_cond(How), SS)
   79   ; pprint_ecp_cmt(red, load(How,S0))))),!.
   80
   81current_loading_proc(Proc1):- nb_current('$loading_proc',Proc1),!.
   82current_loading_proc(Proc1):- t_l:is_ec_cvt(FileType),filetype_to_proc(FileType,Proc1).
   83current_loading_proc(Proc1):- into_dec_pl, Proc1 = assert_ele_cond_load_e,!.
   84current_loading_proc(Proc1):- Proc1 = assert_e, !.
   85
   86% filetype_to_proc(FileType,Proc1).
   87filetype_to_proc(pl,assert_ele_cond_load_e).
   88filetype_to_proc(pel,pprint_ecp(blue)).
   89filetype_to_proc(lps,assert_e).
   90
   91:- export_transparent(cond_load_e/2).   92
   93assert_e(X):- ec_lps_convert:assert_ep(lps_test_mod,X).
   94% assert_e(X):- assert_ele(X).
   95
   96cond_load_e(Cond,EndsWith):- is_list(EndsWith),!,must_maplist(cond_load_e(Cond),EndsWith).
   97cond_load_e(changed,F):- etmp:ec_option(load(F), loaded),!.
   98cond_load_e(changed,EndsWith):- atom(EndsWith),foundations_file(Already),atom_concat(_,Already,EndsWith),!.
   99cond_load_e(Cond,F):- etmp:ec_option(load(F), loading), Cond\==recursed, !.
  100cond_load_e(Cond,F):- needs_resolve_local_files(F, L), !, must_maplist(cond_load_e(Cond), L).  
  101cond_load_e(_,F):- is_filename(F), \+ atom_concat(_,'.e',F), !.
  102cond_load_e(Cond,F):- needs_resolve_local_files(F, L), !, must_maplist(cond_load_e(Cond), L).  
  103%cond_load_e(include,_):- nb_current('$load_cond', cvt_e_pl),!. 
  104%cond_load_e(include,_):- nb_current('$load_cond', translate_e_to_filetype( PlExt)),!. 
  105cond_load_e(Cond,F):- Req = [pl],
  106   \+ nb_current('$output_lang',Req), !,
  107   locally(b_setval('$output_lang',Req), cond_load_e(Cond,F)).
  108cond_load_e(Cond, S0):- resolve_local_files(S0,SS), SS==[], !, pprint_ecp_cmt(red, load(Cond,S0)),!.
  109cond_load_e(Cond,F):-
  110   pprint_ecp_cmt(green, loading(Cond, F)),
  111   current_prolog_flag(occurs_check,Was),
  112   (nb_current('$load_cond', OldCond);OldCond=[]),
  113   setup_call_cleanup(
  114     % Setup
  115     (set_ec_option(load(F), loading),
  116      set_ec_option(load_cond, Cond),
  117      set_prolog_flag(occurs_check,error),
  118      nb_setval('$load_cond', Cond)),
  119     % Call
  120     (current_loading_proc(Proc1),with_e_file(Proc1, current_output, F)),
  121     % Cleanup
  122     (set_ec_option(load(F), unknown),
  123      set_prolog_flag(occurs_check,Was),
  124      nb_setval('$load_cond', OldCond))),
  125   set_ec_option(load(F), loaded).
  126
  127
  128load_e_into_memory(F):- 
  129  with_e_file(assert_e,current_output,F).
  130
  131
  132:- export_transparent(translate_e_to_pfc/1).  133translate_e_to_pfc(F):- translate_e_to_filetype(pfc,F),!.
  134
  135:- export_transparent(translate_e_to_filetype/2).  136translate_e_to_filetype(FileType,F):- needs_resolve_local_files(F, L), !, must_maplist(translate_e_to_filetype(FileType), L),!. 
  137translate_e_to_filetype(FileType,F):- calc_filename_ext(FileType,F,E,PL), translate_e_to_filetype( FileType,E,PL),!.
  138
  139filetype_to_dialect(pl,pfc).
  140filetype_to_dialect(pfc,pfc).
  141filetype_to_dialect(pel,ecalc).
  142filetype_to_dialect(lps,lps).
  143filetype_to_dialect(FileType,Dialect):- fail, FileType = Dialect,!.
  144
  145:- thread_local(t_l:is_ec_cvt/1).  146
  147:- export_transparent(translate_e_to_filetype/3).  148translate_e_to_filetype( FileType,F,OutputName):- absolute_file_name(F,FA),F\==FA,!,translate_e_to_filetype(FileType,FA,OutputName).
  149translate_e_to_filetype(_FileType,_,OutputName):- fail, \+ should_update(OutputName),!. 
  150translate_e_to_filetype(MFileType,F,MOutputName):- 
  151 strip_module(MOutputName,Mod,OutputName), MOutputName\==OutputName,!,
  152 strip_module(MFileType,_,FileType),
  153 translate_e_to_filetype_4(FileType, Mod, F,OutputName),!.
  154
  155translate_e_to_filetype(MFileType,F,OutputName):- 
  156 strip_module(MFileType,Mod,FileType),
  157 translate_e_to_filetype_4(FileType, Mod, F,OutputName),!.
  158
  159translate_e_to_filetype_4(FileType, Mod, F,OutputName):- 
  160  (\+ atom(FileType) ;  \+ filetype_to_dialect(FileType,_)),
  161  Proc1 = FileType,!,
  162  locally(b_setval('$loading_proc',Proc1),
  163    translate_e_to_filetype_5(FileType, Mod, F,OutputName)).
  164translate_e_to_filetype_4(FileType, Mod, F,OutputName):- 
  165  translate_e_to_filetype_5(FileType, Mod, F,OutputName),!.
  166 
  167translate_e_to_filetype_5(FileType, Mod, F, OutputName):- 
  168 setup_call_cleanup(flag('$ec_translate_depth', Was, Was),
  169   ((ignore((Was==0 -> retractall(etmp:ec_option(load(_), _)))),
  170   locally(t_l:is_ec_cvt(FileType),
  171     (current_loading_proc(Proc1),with_e_file(Mod:Proc1, OutputName, F))))),
  172   flag('$ec_translate_depth', _, Was)).
  173
  174calc_filename_ext(MEx,F,FE,PL):- strip_module(MEx,_,Ext), Ext\==MEx,!, calc_filename_ext(Ext,F,FE,PL).
  175calc_filename_ext(pel,F,FE,PL):- calc_pel_filename(F,FE,PL),!.
  176calc_filename_ext(Ext,F,FE,PL):- compound(Ext), compound_name_arity(Ext,Out,_),calc_filename_ext(Out,F,FE,PL).
  177calc_filename_ext(Ext,F,FE,PL):- atom_concat(Was,Ext,F),PL=F,!,calc_filename_ext(Ext,Was,FE,_).
  178calc_filename_ext(Ext,F,FE,PL):- atom_concat(Was,'.e',F),FE=F,!,calc_filename_ext(Ext,Was,_,PL).
  179calc_filename_ext(Ext,F,FE,OutputName):- FE=F, calc_where_to(outdir('.', Ext), F, OutputName).
  180                        
  181calc_pel_filename(F,FE,F):- atom_concat(Was,'.pel',F),!,atom_concat(Was,'.e',FE).
  182calc_pel_filename(F,FE,F):- atom_concat(Was,'.e.pl',F),!,atom_concat(Was,'.e',FE).
  183calc_pel_filename(F,FE,F):- atom_concat(Was,'.pl',F),!,atom_concat(Was,'.e',FE).
  184calc_pel_filename(F,F,PL):- atom_concat(Was,'.e',F), atom_concat(Was,'.pel',PL),exists_file(PL).
  185calc_pel_filename(F,F,PL):- atom_concat(Was,'.e',F), atom_concat(Was,'.e.pl',PL),exists_file(PL).
  186calc_pel_filename(F,F,PL):- atom_concat(Was,'.e',F), atom_concat(Was,'.pl',PL),exists_file(PL).
  187
  188:- export_transparent(load_e_pl/1).  189load_e_pl(F):- needs_resolve_local_files(F, L), !, must_maplist(load_e_pl, L),!. 
  190load_e_pl(F):- to_e_pl(F,E,PL),load_e_pl(E,PL),!.
  191
  192:- export_transparent(cvt_e_pl/1).  193cvt_e_pl(F):- needs_resolve_local_files(F, L), !, must_maplist(cvt_e_pl, L),!. 
  194cvt_e_pl(F):- to_e_pl(F,E,PL), cvt_e_pl(E,PL),!.
  195                        
  196to_e_pl(F,FE,PL):- calc_filename_ext(pel,F,FE,PL),!.
  197
  198:- export_transparent(load_e_pl/2).  199load_e_pl(ME,PL):- strip_module(ME,M,E),cvt_e_pl(E,PL),M:user:consult(PL),!.
  200
  201get_date_atom(Atom):- 
  202   get_time(Now),stamp_date_time(Now, Date, 'UTC'), 
  203   format_time(atom(Atom),'%a, %d %b %Y %T GMT', Date, posix),!.
  204
  205cvt_e_pl(F0,OutputName):-
  206 absolute_file_name(F0,F),
  207 ( 
  208 (( ( fail, \+ should_update(OutputName))) -> true ;
  209  setup_call_cleanup(open(OutputName, write, Outs),
  210  (must_maplist(format(Outs,'~N~q.~n'),
  211    [( :- include(library('ec_planner/ec_test_incl'))),
  212     ( :- expects_dialect(pfc))]),
  213       get_date_atom(Atom),format(Outs,'% ~w',[Atom]),
  214       nb_setval('$ec_output_stream',Outs),
  215  with_output_to(Outs, cond_load_e(load_e_pl,F))),
  216  (close(Outs),nb_setval('$ec_output_stream',[]))))), %trace, %consult(OutputName),
  217  !.
  218
  219/*
  220 
  221 state constraints:  
  222
  223      holds_at(Fluent)
  224          implies/equivalent_to
  225      holds_at(Fluent)
  226
  227
  228 effect axioms:  
  229
  230      happens_at(Event)
  231           terminates_at/initiates_at/releases_at
  232      holds_at(Fluent)
  233       
  234
  235 trigger axioms: 
  236  
  237      holds_at(Fluent)/happens_at(Event)
  238           triggers
  239      happens_at(Event)
  240
  241
  242 precondition axioms:  
  243  
  244      happens_at(Event)
  245           implies
  246      holds_at(Fluent)
  247
  248 
  249
  250happens_at(doorLock(Agent,Door),Time) -> 
  251  holds_at(awake(Agent),Time) &
  252  holds_at(doorUnlocked(Door),Time) &
  253  holds_at(nearPortal(Agent,Door),Time)
  254
  255
  256
  257
  258   
  259axiom(
  260 terminates_at(doorLock(Agent,Door),
  261            doorUnlocked(Door),Time), [])
  262
  263becomes 
  264...
  265
  266axiom(
  267 terminates_at(doorLock(Agent,Door),
  268            doorUnlocked(Door),Time),
  269   [ holds_at(awake(Agent),Time) &
  270     holds_at(doorUnlocked(Door),Time) &
  271     holds_at(nearPortal(Agent,Door),Time)]).
  272 
  273*/
  274functors_are(F,E):- \+ is_list(E), conjuncts_to_list(E, L), !, functors_are(F, L).
  275functors_are(\+ F,L):-  nonvar(F), !, forall(member(E,L), \+ functor_is(F, E)).
  276functors_are((F1,F2),L):- !,  
  277  partition(functors_are(F1),L,[_|_],RestOf),
  278  functors_are(F2,RestOf).
  279%functors_are((F1;F2),L):-  !, nonvar(F1), (functors_are(F1,L);functors_are(F2,L)).
  280functors_are(F,L):- must_maplist(functor_is(F),L).
  281
  282
  283functor_is(F, not(E)):- !, compound(E), functor_is(F, E).
  284functor_is(F, exists(_, E)):- !, compound(E), functor_is(F, E).
  285functor_is(F,(F1;F2)):- !, functor_is(F,F1), functor_is(F,F2).
  286functor_is(F,(F1,F2)):- !, functor_is(F,F1), functor_is(F,F2).
  287functor_is(\+ F,P):- !, nonvar(F), !,  \+ functor_is(F,P).
  288functor_is((F1;F2),P):- !, nonvar(F1), (functor_is(F1,P);functor_is(F2,P)).
  289functor_is(F,P):- compound(P), compound_name_arity(P,F,_).
  290
  291:- export_transparent(set_mpred_props/2).  292set_mpred_props(MF,E):- strip_module(MF,M,P),MF==P,!,must(set_mpred_props(M:P,E)).
  293set_mpred_props(M:F/A,E):- !, (is_ftVar(A)-> true ; ain(mpred_prop(M,F,A,E))).
  294set_mpred_props(M:P,E):- \+ compound(P),!,set_mpred_props(M:P/_,E).
  295set_mpred_props(M:P,E):- compound_name_arity(P,F,A),set_mpred_props(M:F/A,E),
  296   add_mat(P),!.
  297
  298add_mat(P):- compound_name_arity(P,_,0),!.
  299add_mat(P):-
  300   only_dec_pl(assert_ready(red, ('==>'(meta_argtypes(P))))),
  301   ain(meta_argtypes(P)).
  302
  303
  304
  305
  306is_4th_order_f0(axiom).
  307is_4th_order_f0(F):- upcase_atom(F,UD),upcase_atom(F,UD).
  308
  309get_arg_type(argIsa(W),1,W).
  310get_arg_type(F, Nth,Type):- arg_info(_,F,VTypes), compound(VTypes), arg(Nth,VTypes,Type), !.
  311get_arg_type(F,_,axiom_head):- is_4th_order_f0(F),!.
  312
  313coerce_arg_to_type(Time, axiom_head, H, HH):- !, show_fix_axiom_head(Time, H, HH).
  314
  315coerce_arg_to_type(_, axiom, HB, HB):- compound_gt(HB, 0), HB=..[RelType|_], fixed_already(RelType), !.
  316coerce_arg_to_type(Time, axiom, HB, axiom(AxHB,[])):-  coerce_arg_to_type(Time, axiom_head, HB, AxHB), !.
  317coerce_arg_to_type(Time, axiom, H, HH):- fix_assert(Time, H, HH).
  318coerce_arg_to_type(_Time, fluent, H, H):-
  319   assert_ele(fluent(H)).
  320
  321
  322fixed_already(mpred_prop).
  323fixed_already(meta_argtypes).
  324fixed_already(abducible).
  325fixed_already(executable).
  326fixed_already(axiom).
  327fixed_already(ignore).
  328fixed_already(load).
  329fixed_already(include).
  330fixed_already(set_ec_option).
  331fixed_already(F):- arg_info(domain,F,_).
  332fixed_already(F):- arg_info(abducible,F,_).
  333
  334fix_assert(_T, :-(B), :-(B)):- !. 
  335fix_assert(_T, '==>'(B), '==>'(B)):- !. 
  336fix_assert(Time, HT:-B, HTO:-B):- !, 
  337  fix_assert(Time, HT, HTO).
  338fix_assert(Time, HT, HTO):- 
  339 fix_argtypes(Time, 1, [argIsa(axiom)], HT, HTM),!,
  340 fix_assert_pass2(Time, HTM, HTO).
  341
  342fix_assert_pass2(_, HB, HB):- HB=..[RelType|_], fixed_already(RelType), !.
  343fix_assert_pass2(Time, G, axiom(GG, [])):- must(show_fix_axiom_head(Time, G, GG)),!.
  344
  345
  346fix_argtypes(Time, NthArg, [F|_], HT, HTO):-
  347    get_arg_type(F,NthArg,Type), 
  348    coerce_arg_to_type(Time,Type,HT,HTO),!.
  349fix_argtypes(_, _NthArg, _Type, HB, HB):- \+ compound_gt(HB, 0), !.
  350fix_argtypes(Time, _NthArg, Type, HT, HTO):-
  351 compound_name_arguments(HT, F, L), 
  352 fix_argtypes(Time, 1, [F|Type], L, LL),
  353 compound_name_arguments(HTO, F, LL).
  354
  355fix_numbered_argtypes(Time, NthArg, FType, [H|T], [HH|TT]):- !,
  356  fix_argtypes(Time, NthArg, FType, H, HH),
  357  NthArgPlus1 is NthArg + 1,
  358  fix_numbered_argtypes(Time, NthArgPlus1, FType, T, TT).
  359fix_numbered_argtypes(_Time, _NthArg, _FType, [], []).
  360
  361:- export_transparent(fix_axiom_head/3).  362
  363
  364fix_axiom_head(_, X, Y):-  (\+ callable(X);\+ compound(X)), !, X=Y.
  365fix_axiom_head(T, [G1|G2], [GG1|GG2]):- !, fix_axiom_head(T, G1, GG1),fix_axiom_head(T, G2, GG2). 
  366fix_axiom_head(T, (G1,G2), (GG1,GG2)):- !, fix_axiom_head(T, G1, GG1),fix_axiom_head(T, G2, GG2). 
  367fix_axiom_head(T, (G1;G2), (GG1;GG2)):- !, fix_axiom_head(T, G1, GG1),fix_axiom_head(T, G2, GG2). 
  368fix_axiom_head(T, (G1:-B), (GG1:-B)):- !, fix_axiom_head(T, G1, GG1),!.
  369
  370
  371fix_axiom_head(T, exists(X,G), (ex(X),GG)):- no_canon, !, fix_axiom_head(T, G, GG).
  372
  373fix_axiom_head(T, exists(X,G), exists(X,GG)):-!, fix_axiom_head(T, G, GG).
  374
  375fix_axiom_head(T, neg(II),O):- compound(II), II= neg(I), !, fix_axiom_head(T, I,O),!.
  376fix_axiom_head(T, neg(I),O):- !, fix_axiom_head(T, I,M), correct_holds(neg, not(M), O). 
  377fix_axiom_head(T, not(I),O):- !, fix_axiom_head(T, I,M), correct_holds(neg, not(M), O).
  378fix_axiom_head(T, G, GG):- must_or_dumpst(cvt0_full(T,G,Y)), (G==Y -> fail; fix_axiom_head(T,Y,GG)),!.
  379
  380fix_axiom_head(T, (G1G2), (GG1GG2)):- compound_name_arguments(G1G2,F,[G1,G2]),
  381   member(F,['->','<-','<->',';',',']), !,
  382   fix_axiom_head(T, G1, GG1),fix_axiom_head(T, G2, GG2),
  383   compound_name_arguments(GG1GG2,F,[GG1,GG2]).
  384
  385% EC to LPS
  386
  387fix_axiom_head(T, holds_at(G,T1), G):- reduce_holds_at, into_lps, same_times(T1,T), functor_skel(G,P), syntx_term_check(fluent(P)),!.
  388fix_axiom_head(T, holds_at(Event,T1), G):- reduce_holds_at, into_lps, nonvar(Event), same_times(T1,T), !, fix_axiom_head(T1, Event, G).
  389fix_axiom_head(T, happens_at(Event,T1), G):- into_lps, nonvar(Event), same_times(T1,T), !, fix_axiom_head(T1, Event, G).
  390fix_axiom_head(_, G, G):- into_lps, functor_skel(G,P), syntx_term_check(fluent(P)),!.
  391fix_axiom_head(_, G, G):- into_lps, functor_skel(G,P), syntx_term_check(predicate(P)),!.
  392
  393% EC to DEC_PL
  394fix_axiom_head(_, G, G):- into_dec_pl, safe_functor(G,F,A), already_good(F,A),!.
  395fix_axiom_head(T, G, holds_at(G,T)):- into_dec_pl, functor_skel(G,P), syntx_term_check(fluent(P)),!.
  396fix_axiom_head(T, G, happens_at(G,T)):- into_dec_pl,  functor_skel(G,P), \+ syntx_term_check(predicate(P)), (syntx_term_check(event(P);executable(P))),!.
  397fix_axiom_head(T, G, holds_at(G,T)):- into_dec_pl, functor_skel(G,P), syntx_term_check(fluent(P)),!.
  398
  399fix_axiom_head(_, G, G):- G\=not(_), functor_skel(G,P), syntx_term_check(predicate(P)),!.
  400
  401fix_axiom_head(T, P, PP):-  
  402   P =..[F|Args],functor(P,F,A), arg_info(AxH,F,Arity),
  403   functor(Arity,_,N),  correct_ax_args(T,F,A,Args,AxH,Arity,N,PP),!. 
  404fix_axiom_head(T, P, Out):- predicate_property(P,foreign),!,if_debugging(ec,((call(dumpST), wdmsg(fix_axiom_head(T, call(P))),break))),!,Out=call(P).
  405
  406fix_axiom_head(T, G, GG):- into_dec_pl, !, if_debugging(ec, ((call(dumpST), wdmsg(fix_axiom_head(T, G)), break))), GG = holds_at(G, T).
  407
  408% LPS Only
  409fix_axiom_head(_, P, P):-  functor(P,F,_),fixed_already(F),!.
  410fix_axiom_head(_, P, P):-  functor(P,F,_),atom_concat(F0,'s',F),fixed_already(F0),!.
  411
  412fix_axiom_head(T, G, GG):- if_debugging(ec, ((call(dumpST), wdmsg(fix_axiom_head(T, G)), break))),  \+ into_lps,
  413  GG = holds_at_oops(G, T).
  414fix_axiom_head(_T,G,G):-!.
  415
  416same_times(T1,T):- T1==T,!.
  417
  418%maybe_show_diff(T0, F, O):- copy_term_nat(T0+F+O,T+HT+HTTermO),
  419maybe_show_diff(T, HT, HTTermO):-
  420  ignore((HT\==HTTermO, HT \= not(holds_at(_,_)), 
  421    % pprint_ecp_cmt(blue,(axiom_head(T) -> HT)),
  422    major_debug(pprint_ecp_cmt(blue,(fix_axiom_head(T) -> [HT ,(->), HTTermO]))))),!.
  423
  424:- export(show_fix_axiom_head/3).  425show_fix_axiom_head(T, HT, HTTermO):- 
  426    fix_axiom_head(T, HT, HTTermO),!,
  427    ignore(maybe_show_diff(T, HT, HTTermO)).
  428    
  429show_fix_axiom_head(T, HT, HTTermO):- dumpST, 
  430 compound_name_arguments(HT, F, L),
  431 upcase_atom(F,U),downcase_atom(F,U),
  432 must_maplist(show_fix_axiom_head(T),L,LL),
  433 compound_name_arguments(HTTerm, F, LL),
  434 show_fix_axiom_head(T, HTTerm, HTTermO), !.
  435
  436show_fix_axiom_head(T, HT, HTTermO):- trace, rtrace(fix_axiom_head(T, HT, HTTermO)),!.
  437
  438:- dynamic(ec_tmp:do_next_axiom_uses/1).  439
  440call_ready_body(Type,Body):- 
  441   setup_call_cleanup(
  442    pprint_ecp(Type,':-'(if(is_e_toplevel))),
  443    ((notrace((echo_format('~N'))),
  444    pprint_ecp(Type,':-'(Body)),
  445    notrace((echo_format('~N'))),
  446    ignore(must((Body,!))),
  447    notrace((echo_format('~N'))))),
  448    pprint_ecp(Type,':-'(endif))).
  449
  450assert_ready(P):- assert_ready(pl,P).
  451
  452assert_ready(Type,(:-Body)):- 
  453   call_ready_body(Type,Body),!.
  454
  455assert_ready(Type,'==>'(next_axiom_uses(Value))):- 
  456     pprint_ecp_pl(Type,'next_axiom_uses'(Value)),
  457     assert(ec_tmp:do_next_axiom_uses(Value)),!.
  458
  459assert_ready(Type,'==>'(Value)):- 
  460  only_dec_pl( pprint_ecp_pl(Type,'==>'(Value))),
  461   mpred_fwc('==>'(Value)),
  462   Value = ValueO, % fix_assert(_Time,Value,ValueO),
  463   into_current_domain_db(ValueO),!.
  464
  465assert_ready(Type,axiom(H,B)):- select(I,B,NB),compound(I),I=ignore(Was==Into),
  466   subst(axiom(H,NB),Was,Into,axiom(HH,BB)),!,
  467   %append(BB,[ignore(ignore(Was==Into))],BBB),
  468   BB=BBB,
  469   assert_ready(Type,axiom(HH,BBB)), !.
  470
  471
  472assert_ready(Type,axiom(H,B)):- B ==[],compound(H),functor(H,F,_),verbatum_functor(F),!,
  473  assert_ready(Type,H).
  474
  475assert_ready(Type,Value):- 
  476  assert_ready_now(Type,Value).
  477
  478assert_ready_now(Type,Value):- 
  479   only_dec_pl(pprint_ecp_pl(Type,Type=Value)),
  480   notrace((echo_format('~N'))),
  481   mpred_fwc(Value),
  482   fix_assert(_Time,Value,ValueO),
  483   into_current_domain_db(ValueO),!.
  484
  485into_current_domain_db('==>'(Value)):-!,into_current_domain_db((Value)).
  486into_current_domain_db(ec_current_domain_db(Value)):- !, into_current_domain_db((Value)).
  487into_current_domain_db(ec_current_domain_db(Value,T)):- is_ftVar(T),!,into_current_domain_db(Value).
  488into_current_domain_db(ec_current_domain_db(Value,T)):- !, assertz_if_new_domain_db(Value,T).
  489into_current_domain_db(Value):- get_varname_list(Vs),=(Value-Vs,ValueO-VsO),
  490locally(b_setval('$variables',VsO),assertz_if_new_domain_db(ValueO,_)).
  491
  492
  493assertz_if_new_domain_db((H:-B),T):- !, assertz_if_new_msg((user:ec_current_domain_db(H,T):-B)).
  494assertz_if_new_domain_db(ValueO,_):- ValueO =@= axiom(holds_at(neg(raining), _), []),!,barf.
  495assertz_if_new_domain_db(ValueO,T):- assertz_if_new_msg(user:ec_current_domain_db(ValueO,T)).
  496
  497assertz_if_new_msg(Stuff):- clause_asserted(Stuff),major_debug(wdmsg(already(Stuff))), !, only_lps(assert_to_lps(Stuff)),!.
  498assertz_if_new_msg(Stuff):- assertz_if_new(Stuff), only_lps(assert_to_lps(Stuff)),!.
  499
  500some_renames(O,O):- \+ compound(O),!.
  501some_renames(HB,O):- sub_term(Sub,HB),compound(Sub),Sub=before(X,Y),!,
  502  subst(HB,Sub,b(X,Y),HTM),some_renames(HTM,O).
  503some_renames(HB,O):- sub_term(Sub,HB),compound(Sub),compound_name_arity(Sub,Name,0),!,
  504  subst(HB,Sub,Name,HTM),some_renames(HTM,O).
  505some_renames(O,O).
  506
  507:- export_transparent(assert_ele_cond_load_e/1).  508assert_ele_cond_load_e(EOF) :- must(brk_on_bind(EOF)), must(assert_ele(EOF)),!.
  509
  510predform_to_functionform(PF,equals(Fn,LastArg)):- notrace((PF=..[F|Args],append(FnArgs,[LastArg],Args),predname_to_fnname(F,FnF),Fn=..[FnF|FnArgs])).
  511functionform_to_predform(equals(Fn,LastArg),PF):- notrace((Fn=..[FnF|FnArgs],append(FnArgs,[LastArg],Args),fnname_to_predname(FnF,F),PF=..[F|Args])).
  512
  513predname_to_fnname(Pred,Fun):- notrace(clause_b(functional_predicate(Fun,Pred))),!.
  514predname_to_fnname(Pred,Fun):- atom(Pred),atom_concat(Pred,'Of',Fun),call_u(resultIsa(Templ,_)),functor(Templ,F,_),Fun==F,!.
  515predname_to_fnname(Pred,Fun):- atom(Pred),atom_concat(Pred,'Fn',Fun),!.
  516predname_to_fnname(Pred,Fun):- atom(Pred),atom_concat(Fun,'Pred',Pred),!.
  517
  518fnname_to_predname(Fun,Pred):- clause_b(functional_predicate(Fun,Pred)).
  519fnname_to_predname(Fun,Pred):- atom(Fun),atom_concat(Pred,'Fn',Fun),!.
  520fnname_to_predname(Fun,Pred):- atom(Fun),atom_concat(Pred,'Of',Fun),!.
  521fnname_to_predname(Fun,Pred):- atom(Fun),atom_concat(Fun,'Pred',Pred),!.
  522
  523:- export_transparent(assert_ele/1).  524assert_ele(EOF) :- notrace((EOF == end_of_file)),!.
  525assert_ele(I):- notrace(\+ callable(I)),!,assert_ele(uncallable(I)).
  526assert_ele(SS):- notrace(is_list(SS)),!,must_maplist(assert_ele,SS).
  527assert_ele(Cvt1):-  (some_renames(Cvt1,Cvt2) -> Cvt1\=@=Cvt2), !, assert_ele(Cvt2).
  528
  529
  530assert_ele(_):- notrace((echo_format('~N'), fail)).
  531assert_ele(translate(Event, Outfile)):- !, mention_s_l, echo_format('% translate: ~w  File: ~w ~n',[Event, Outfile]).
  532%assert_ele('==>'(S0)):- !, assert_ready( '==>'(S0)).
  533assert_ele(:- S0):- !, assert_ready( (:-(S0))).
  534
  535assert_ele(axiom(H,B)):- !, assert_axiom(H,B).
  536assert_ele(include(S0)):- !, assert_ready( :-(load_e_cond(S0,include))).
  537assert_ele(load(S0)):- !, assert_ready( :-(load_e_cond(S0,changed))).
  538assert_ele(load(Cond, S0)):- !, assert_ready( :-(load_e_cond(S0,Cond))).
  539assert_ele(ec_current_domain_db(P)):- !, assert_ready( ec_current_domain_db(P)).
  540
  541
  542assert_ele(HB):- \+ compound_gt(HB, 0), !, assert_axiom(HB, []).
  543
  544assert_ele(HB):- HB=..[=, Function, Value],
  545  %get_functor(RelSpec,F), get_mpred_prop(Function,function),
  546  %must(compound(Function)),
  547  %append_term(Function,Value,Predicate), !,
  548  assert_ele(equals(Function,Value)).
  549
  550assert_ele(HB):- HB=..[function, RelSpec, RetType], 
  551  %append_term(RelSpec,RetType,PredSpec),
  552  %assert_ele(functional_predicate(PredSpec)),
  553  must_det_l((
  554   assert_ele(function(RelSpec)),
  555
  556   functionform_to_predform(equals(RelSpec,RetType),PredSpec),
  557   assert_ele(predicate(PredSpec)),
  558   get_functor(RelSpec,F),
  559   get_functor(PredSpec,P),
  560   assert_ele(functional_predicate(F,P)),
  561   assert_ele(function_argtypes(P,RelSpec,RetType)),
  562   assert_ele('==>'(resultIsa(F, RetType))))).
  563
  564assert_ele(HB):- HB=..[RelType,RelSpec],arg_info(domain,RelType,arginfo), !, 
  565  functor_skel(RelSpec,P),!, 
  566  RelTypeOpen=..[RelType,P],
  567  only_dec_pl(assert_ready(blue, RelTypeOpen)),
  568  assert_ready(blue, HB),
  569  assert_ready(red, ('==>'(mpred_prop(RelSpec, RelType)))),
  570  must(set_mpred_props(RelSpec,RelType)).
  571
  572assert_ele(HB):- functor(HB,F, L), arg_info(abducible,F,Args),Args=..[v|ArgL], length(ArgL,L), !, assert_ready(yellow, '==>'(HB)).
  573assert_ele(subsort(F, W)):- !, must_maplist(assert_ready(yellow),[sort(F),sort(W),subsort(F, W)]).
  574assert_ele(option(X,Y)):- set_ec_option(X,Y), must_maplist(assert_ready(yellow),[:- set_ec_option(X,Y)]).
  575assert_ele(xor(XORS)):- conjuncts_to_list(XORS,List),  !, assert_ready(red, '==>'xor(List)).
  576assert_ele(t(F, W)):- !, must_maplist(assert_ready(yellow),['==>'(sort(F)), '==>'(t(F, W))]).
  577
  578% assert_ele(not(holds_at(H,T))):- assert_ele(holds_at(neg(H),T)).
  579assert_ele(Cvt1):- \+ into_lps,  (cvt0(_T, Cvt1,Cvt2) -> Cvt1\=@=Cvt2), !, assert_ele(Cvt2).
  580
  581  %locally(b_setval('$output_lang',[ec]), assert_ele(P)).
  582assert_ele('<->'(H,B)):- 
  583  pprint_ecp_cmt(green, '<->'(H,B)), !,
  584  only_dec_pl((atoms_of(H,HH), atoms_of(B,BB),pprint_ecp_cmt(yellow, '<->'(HH,BB)))), !,
  585  assert_ele('->'(H,B)),
  586  assert_ele('->'(B,H)).
  587
  588
  589% assert_ele(initially(F)):- !, assert_axiom(initially(F),[]).
  590assert_ele(directive(F)):- !, assert_ele(next_axiom_uses(F)).
  591
  592/*
  593assert_ele('->'(H,B)):- nonvar(B),
  594  B=(BP,(B1;B2)),!,
  595  assert_ele('->'(H,(BP,B1))), 
  596  must(assert_ele('->'(H,(BP,B2)))),!.
  597
  598assert_ele('->'(B,H)):- nonvar(B),
  599  B=(BP,(B1;B2)),!,
  600  assert_ele('->'((BP,B1),H)),assert_ele('->'((BP,B2),H)).
  601
  602assert_ele('->'(B,H)):- nonvar(B),B=((B1;B2)),!,assert_ele('->'(B1,H)),assert_ele('->'(B2,H)).
  603*/
  604
  605assert_ele('<-'(H,B)):- conjuncts_to_list(B,BL), !, must(assert_axiom(H,BL)).
  606assert_ele((H :- B)):- !,  assert_ready( (H :- B)).
  607% assert_ele((H :- B)):- (H=not(_);is_axiom_head(H)), !, conjuncts_to_list(B,BL), assert_axiom(H,BL).
  608assert_ele(axiom(H,B)):- echo_format('~N'), !,
  609  correct_axiom_time_args(t,H,B,HH,BB),
  610  assert_ready( axiom(HH,BB)).
  611
  612assert_ele(HB):- correct_holds(outward,HB, HBC), HB\=@=HBC, !, assert_ele(HBC).
  613
  614% , assert_ready(e, HB),
  615%assert_ele(SS):- syntx_term_check(SS),!.
  616
  617assert_ele('->'(Body,AxHead)):- AxHead=..[Effect|_],
  618  member(Effect,[initiates_at,terminates_at,releases_at]),
  619  conjuncts_to_list_body(Body, Conds), 
  620  assert_axiom(AxHead, Conds).
  621
  622assert_ele(AxHead):- AxHead=..[Effect|_],
  623  member(Effect,[initiates_at,terminates_at,releases_at]),
  624  assert_axiom(AxHead, []).
  625
  626/*
  627assert_ele(if(happens_at(A,T),Holds)):- 
  628  assert_m_axiom(if(not(Holds),not(happens_at(A,T)))).
  629*/
  630assert_ele(happens_at(A,T)):- number(T), !, assert_ele(happens_at(A,t+T)).
  631
  632assert_ele('->'(B,H)):-  fail, term_variables(B+H,Vars), Vars=[_,_|_], 
  633   atoms_of('->'(B,H),Atoms), \+ member(allDifferent,Atoms),!,
  634   assert_m_axiom('->'(allDifferent(Vars),'->'(B,H))).
  635
  636assert_ele('->'(B,H)):- no_canon, !, assert_m_axiom('->'(B,H)).
  637% assert_ele('->'(B,H)):-  conjuncts_to_list_body(B,BL), !, assert_axiom(H,BL).
  638
  639assert_ele(H):- compound_name_arity(H, F, 2),
  640  needs_cononicalization(F),
  641  e_to_pel(H,P), !, assert_m_axiom(P).
  642
  643assert_ele(not(H)):-  !,  assert_m_axiom(not(H)).
  644
  645assert_ele('==>'(SS)):- echo_format('~N'), !,
  646  assert_ready(red, '==>'(SS)).
  647
  648assert_ele(axiom(H)):- !, assert_ele(axiom(H,[])).
  649
  650% assert_ele(SS):- fix_time_args(T, SS),
  651assert_ele(SS):- echo_format('~N'), 
  652  % dmsg(warn(assert_ele(SS))),
  653  assert_axiom(SS,[]),!.
  654  %assert_ready(red, SS).
  655
  656correct_axiom_time_args(_Stem,H,B,HH,BB):- into_lps,!, H=HH,B=BB,!.
  657correct_axiom_time_args( Stem,H,B,HH,BB):- 
  658  visit_time_args(Stem,[],H,HH,Mid),
  659  visit_time_args(Stem,Mid,B,BBs,Out),
  660  append(BBs,Out,BB),!.
  661
  662/*
  663ForAll([event,animal,time],
  664 HoldsAt(DoneBy(event,animal),time) <->
  665 (Happens(event,time) &
  666  ((Exists([gate], event=Close(animal,gate))) |
  667   (Exists([animal1].  event=GetOff(animal,animal1)))|
  668   (Exists([animal1].  event=Mount(animal,animal1)))|
  669   (Exists([position].  event=Move(animal,position)))|
  670   (Exists([gate].  event=Open(animal,gate))) |
  671   (Exists([human1].  event=ThrowOff(animal,human1)))))).
  672*/
  673
  674barf:- dumpST,wdmsg(i_BaRfzzzzzzzzzzzzzzzzzzzzzzzzzzz), break.
  675use_inititally:- true.
  676
  677cvt0_full(T,G,GG):- must(cvt0(T,G,Y)), !, (G==Y -> G=GG ; cvt0(T,Y,GG)),!.
  678
  679is_start_t(Zero):- Zero == 0,!.
  680is_start_t(Zero):- Zero == start,!.
  681
  682start_plus(Zero,start):- is_start_t(Zero).
  683start_plus(Zero,start+Zero):- number(Zero),!.
  684
  685cvt0(_, X, Y):-  (\+ callable(X);\+ compound(X)), !, X=Y.
  686cvt0(_, X\=Y, diff(X,Y)) :- !.
  687cvt0(T, equals(X,Y), O):- is_ftVar(X), \+ is_ftVar(Y),!,cvt0(T, equals(Y,X), O),!.
  688cvt0(T, equals(X,Y), O):- \+compound(X), compound(Y),!,cvt0(T, equals(Y,X), O),!.
  689cvt0(_, equals(X,Y), O):-compound(X), functionform_to_predform(equals(X,Y),O),!.
  690cvt0(_, X=Y, Equals):- !,as_equals(X,Y,Equals).
  691cvt0(T0, holds_at(NotH,T),O):- compound(NotH),not(H)= NotH, !, cvt0(T0, holds_at(neg(H),T), O).
  692%cvt0(T, P, call(P)):- predicate_property(P,foreign),!.
  693%cvt0(_, not(exists(_Vars, holds_at(P, Time))),not(holds_at(neg(P), Time))).
  694cvt0(T, initially(N), Out):- \+ use_inititally, cvt0(T, holds_at(N, 0), Out).
  695cvt0(_, holds_at(N,Zero),initially(N)):- use_inititally, is_start_t(Zero),!.
  696cvt0(_, holds_at(N,Zero),holds_at(N,Expr)):- \+ into_lps, start_plus(Zero,Expr),!.
  697cvt0(_, happens_at(N,Zero),happens_at(N,Expr)):-  \+ into_lps, start_plus(Zero,Expr),!.
  698%cvt0(T, holds_at(N,AT),'<-'(holds_at(N,TN),(start(T),toffset(T,AT,TN)))):- number(AT),!,atom_concat(t,AT,TN).
  699
  700cvt0(_, before(X,Y),b(X,Y)).
  701%cvt0(_, '<-'(X,Y),'<-'(X,Y)).
  702cvt0(_T, option(X,Y),option(X,Y)):-!.
  703cvt0(T, X\=Y, O):- must(cvt0(T, not(X=Y), O)).
  704
  705cvt0(_, =(X,Y),P):- !, as_equals(X,Y,P).
  706cvt0(_, equals(X,Y),P):- !, as_equals(X,Y,P).
  707cvt0(T, axiom_uses(V),axiom_uses(V,T)):- !.
  708
  709
  710cvt0(T, neg(II),O):- compound(II), II= neg(I), !, cvt0(T, I,O),!.
  711cvt0(T, neg(I),O):- !, cvt0(T, I,M), correct_holds(neg, not(M), O). 
  712cvt0(T, not(I),O):- !, cvt0(T, I,M), correct_holds(neg, not(M), O). 
  713cvt0(T, happens_at(F, T1, T2), O):- T1==T2, cvt0(T, happens_at(F, T1), O).
  714% cvt0(_T, happens_at(F, T1), happens_at(F, T1)):- !.
  715cvt0(_, ec_current_domain_db(X), ec_current_domain_db(X)).
  716cvt0(T, ec_current_domain_db(X,Y), ec_current_domain_db(X,Y)):- ignore(Y=T).
  717
  718/*
  719cvt0(T, [G1|G2], [GG1|GG2]):- !, cvt0(T, G1, GG1),cvt0(T, G2, GG2). 
  720cvt0(T, (G1,G2), (GG1,GG2)):- !, cvt0(T, G1, GG1),cvt0(T, G2, GG2). 
  721cvt0(T, (G1;G2), (GG1;GG2)):- !, cvt0(T, G1, GG1),cvt0(T, G2, GG2). 
  722
  723cvt0(_, happens_at(G, T), happens_at(G, T)):-!.
  724cvt0(_, happens_at(G, T, T2), happens_at(G, T, T2)):-!.
  725cvt0(_, holds_at(G, T), holds_at(G, T)):-!.
  726cvt0(_, holds_at(G, T, T2), holds_at(G, T, T2)):-!.
  727*/
  728cvt0(T, G, Gs):-  \+ into_lps, fix_goal_add_on_arg( T, G, Gs, _TExtra),!.
  729%cvt0(T,(G1,G2),GGs):- !, cvt0(T,G1,GG1),cvt0(T,G2,GG2).
  730%cvt0(T, P, P).
  731%cvt0(T,X,Y):- trace, ec_to_ax(T, X,Y).
  732cvt0(T, P, PP):-  \+ into_lps,
  733   P =..[F|Args],functor(P,F,A), arg_info(AxH,F,Arity),
  734   functor(Arity,_,N), 
  735   correct_ax_args(T,F,A,Args,AxH,Arity,N,PP),!. 
  736% cvt0(_T, exists(X,Y), exists(X,Y)):-!.
  737cvt0(T, HT, HTTerm):-  
  738 compound_name_arguments(HT, F, L),
  739 % upcase_atom(F,U),downcase_atom(F,U),
  740 must_maplist(cvt0(T),L,LL),
  741 ( LL\==L -> compound_name_arguments(HTTerm, F, LL) ; HT = HTTerm ), !.
  742cvt0(_, G, G).
  743
  744must_or_dumpst(G):- call(G),!.
  745must_or_dumpst(G):- ignore(rtrace(G)),dumpST,break.
  746
  747needs_cononicalization(_):- into_lps, no_canon, !, fail.
  748needs_cononicalization(',').
  749needs_cononicalization(';').
  750needs_cononicalization('exists').
  751needs_cononicalization('all').
  752needs_cononicalization('if').
  753needs_cononicalization('iff').
  754needs_cononicalization('equiv').
  755needs_cononicalization('implies').
  756needs_cononicalization('->').
  757needs_cononicalization('<->').
  758needs_cononicalization('and').
  759needs_cononicalization('xor').
  760needs_cononicalization('or').
  761needs_cononicalization('&').
  762needs_cononicalization('|').
  763needs_cononicalization('dia').
  764needs_cononicalization('box').
  765needs_cononicalization('cir').
  766needs_cononicalization(X):-  fix_predname(X, Y),!, X\==Y, needs_cononicalization(X).
  767
  768
  769
  770
  771negations_inward_to_list(C,L):- negations_inward(C,I),conjuncts_to_list(I, L).
  772%  must(convert_to_axiom(lsvm(L,F,Vs,M),HB,NEWHB)),
  773%  do_process_ec(assert_ele,M, NEWHB),
  774conjuncts_to_list_body(Body, Conds):- 
  775  conjuncts_to_list(Body, CondsL),
  776  must_maplist(negations_inward_to_list,CondsL,CondsLI),
  777  append(CondsLI,Conds).
  778  
  779
  780skipped_head(H):- \+ compound(H),!,fail.
  781skipped_head(diff(_,_)).
  782skipped_head(equals(_,_)).
  783skipped_head(equals(_,_)).
  784skipped_head(not(H)):- !, skipped_negated_head(H).
  785skipped_negated_head(H):- \+ compound(H),!,fail.
  786skipped_negated_head(allDifferent(_)).
  787skipped_negated_head(equals(_,_)).
  788skipped_negated_head(diff(_,_)).
  789skipped_negated_head(axiom_uses(_,_)).
  790skipped_negated_head(some(_,_)).
  791skipped_negated_head(comparison(_,_,_)).
  792
  793assert_ele_clauses(X,L,L):- is_list(L), !, 
  794 length(L,N), 
  795 ((N > 19, false )
  796  -> 
  797   (assert_ready(magenta,
  798         todo_later1(N,X)),
  799     must_maplist(pprint_ecp_cmt(blue),L),
  800      sleep(1.0))
  801   ; must_maplist(assert_ele_clauses(X,L),L)).
  802
  803
  804assert_ele_clauses(_X,_L,(H:-B)):- skipped_head(H), !,
  805   nop((pprint_ecp_cmt(yellow,skipped_head(H):-B))),!.
  806
  807assert_ele_clauses(_X,_L,(H:-B)):- !,
  808  only_dec_pl(pprint_ecp_cmt(red,(H:-B))),
  809  conjuncts_to_list_body(B, BL),
  810  assert_axiom(H , BL).
  811assert_ele_clauses(_X,_L,H):-  
  812  assert_axiom(H , []). 
  813
  814%assert_m_axiom(Ax):- (e_to_pel(Ax,X)->Ax\==X),!,assert_m_axiom(Ax).
  815assert_m_axiom(Ax):- 
  816  retract(ec_tmp:do_next_axiom_uses(Value)),!,
  817  assert_m_axiom(axiom_uses(Value)->Ax).
  818assert_m_axiom('<->'(A,B)):- into_lps, !, assert_m_axiom(A->B), assert_m_axiom(B->A). 
  819assert_m_axiom('<-'(A,B)):- into_lps, !, assert_m_axiom(A->B). 
  820assert_m_axiom(X):- \+ no_canon,
  821  major_debug(pprint_ecp_cmt(green, clausify_pnf=X)),
  822  with_output_to(string(_), clausify_pnf(X,Conds)), 
  823  conjuncts_to_list(Conds,CondsL),
  824  assert_ele_clauses(X,CondsL,CondsL).
  825
  826% assert_m_axiom(A->B):- into_lps, !, assert_lps(A->B),!. 
  827assert_m_axiom(H):- assert_axiom(H, []),!.
  828
  829:- export_transparent(assert_axiom/2).  830
  831
  832assert_axiom(Conds, []):- is_list(Conds),!, must_maplist(assert_ele,Conds).
  833assert_axiom(AxHead, append3(L1,L2,LL)):- 
  834   conjuncts_to_list_body(L1,LL1),conjuncts_to_list_body(L2,LL2),
  835   append([LL1,LL2,LL],L12),!,
  836   assert_axiom(AxHead, L12).
  837assert_axiom(AxHead, B) :- \+ is_list(B), !,
  838  conjuncts_to_list_body(B,Bs),
  839  assert_axiom(AxHead, Bs).
  840
  841assert_axiom(AxHead, B):- 
  842  retract(ec_tmp:do_next_axiom_uses(Value)),!,
  843  assert_axiom(AxHead, [axiom_uses(Value)|B]).
  844
  845
  846/*
  847assert_axiom_unused(happens_at(A,T), []):- number(T), !,
  848   assert_axiom(happens_at(A,T), [is_time(T)]).
  849
  850assert_axiom_unused(happens_at(A,T), []):- !,
  851   assert_axiom(happens_at(A,T), [is_time(T)]).  
  852*/
  853
  854assert_axiom(Conds, [happens_at(A,T)]):-
  855   conjuncts_to_list_body(Conds, B ), 
  856   functors_are(\+ happens_at, B), !,
  857   %trace,
  858   debug_var(when,T),
  859   assert_axiom(requires(A,T),holds_at(metreqs(A),T)),
  860   assert_axiom(holds_at(metreqs(A),T),B).
  861
  862/*
  863assert_axiom_unused(Conds, [happens_at(A,T)]):-
  864   conjuncts_to_list(Conds, B ), 
  865   functors_are(\+ happens_at, B), !,
  866   assert_axiom(requires(A,T),Conds),!.
  867*/
  868
  869assert_axiom(AxHead, Some):- is_list(Some), select(E,Some,Rest), compound(E), E = (A,B), !,
  870   conjuncts_to_list_body((A,B), Conds),
  871   append(Conds,Rest,BReast),
  872   assert_axiom(AxHead, BReast).
  873
  874assert_axiom(AxHead, B):-
  875  semi_legit_time(AxHead,TimeBase),
  876  (is_ftVar(TimeBase) -> must(TimeBase = T) ; T = _),
  877  fix_goal(T,B,Bs), B\=@=Bs, !, 
  878  assert_axiom(AxHead, Bs).
  879
  880assert_axiom(AxHead, B):-
  881  AxHead=..[Effect,Event,Fluent,T],
  882  callable(Event),
  883  member(Effect,[initiates_at,terminates_at,releases_at]),
  884  assert_effect(Effect,Event,Fluent, T, B), !.
  885
  886assert_axiom(H,B) :- 
  887  ignore((semi_legit_time(H+B,TimeBase),is_ftVar(TimeBase));semi_legit_time(H+B,TimeBase)),
  888  (is_ftVar(TimeBase) -> must(TimeBase = Time) ; Time = _ ),
  889
  890  must_maplist(show_fix_axiom_head(Time),[H|B],[HH|BB]),
  891
  892  correct_axiom_time_args_other(Time,HH,BB,HHH,BBB),
  893  only_dec_pl(report_time_values(Time,HH,BB,HHH,BBB)),
  894  must(assert_axiom_2(HHH,BBB)),!.
  895
  896
  897report_time_values(Time,HH,BB,HHH,BBB):-
  898  get_time_values(axiom(HH,BB),TimeVs1),
  899  get_time_values(axiom(HHH,BBB),TimeVs2),
  900  %ignore(TimeVs2=TimeVs1),
  901  pprint_ecp_cmt(green,BBB->ta(Time,tvs1=TimeVs1,tvs2=TimeVs2,HHH)),!.
  902
  903hide_compound(ignore(_)).
  904msub_term(X, X).
  905msub_term(X, Term) :-
  906    compound(Term),
  907    \+ hide_compound(Term),
  908    arg(_, Term, Arg),
  909    msub_term(X, Arg).
  910
  911correct_axiom_time_args_other(_Time,HH,BB,HHH,BBB):- into_lps,!, HH=HHH,BB=BBB,!.
  912correct_axiom_time_args_other(_Time,HH,BB,HHH,BBB):- correct_axiom_time_args(t,HH,BB,HHH,BBB), (HH\==HHH;BB\==BBB),!.
  913correct_axiom_time_args_other(Time,HH,BB,HHH,BBB):- atom(Time),subst(HH+BB,Time,NewTime,H+B),
  914  correct_axiom_time_args_other(NewTime,H,B,HHH,BBB),!.
  915correct_axiom_time_args_other(Time,HH,BB,HHH,[ignore(Sub==NewTime),b(Lo,Hi)|BBB]):- 
  916   msub_term(Sub,axiom(HH,BB)),compound(Sub),functor(Sub,F,2),member(F,[(+),(-)]),
  917   sub_term(SV,Sub),SV==Time,!,
  918   % gensym(newTime,NewTime), 
  919   subst(HH+BB,Sub,NewTime,H+B),
  920   ((F == +) -> Lo+Hi=Time+NewTime ; Lo+Hi=NewTime+Time),correct_axiom_time_args_other(NewTime,H,B,HHH,BBB),!.
  921correct_axiom_time_args_other(_Time,HH,BB,HHH,BBB):- correct_axiom_time_args(t,HH,BB,HHH,BBB),!.
  922
  923is_symetric_pred(equals).
  924is_symetric_pred(diff).
  925
  926fix_symetrics(_,O,O):- \+ compound(O),!.
  927fix_symetrics(_, allDifferent(List), allDifferent(List2)):- sort(List,List2),!.
  928fix_symetrics(H, BXY, BYX):- compound_name_arguments(BXY, F, [X,Y]), 
  929  is_symetric_pred(F), \+ compound(X),
  930  contains_var(Y,H), \+ contains_var(X,H), !, 
  931  compound_name_arguments(BYX, F, [Y,X]).
  932
  933fix_symetrics(H, BT, BTTerm):-  
  934 compound_name_arguments(BT, F, L),
  935 must_maplist(fix_symetrics(H),L,LL),
  936 compound_name_arguments(BTTerm, F, LL), !.
  937
  938/*
  939assert_axiom(AxHead, Some):- select(E,Some,Rest), E = (A;B), !, nnf(A,NotA), nnf(B,NotB),
  940   assert_axiom(AxHead, append3(A,NotB,Rest)),
  941   assert_axiom(AxHead, append3(B,NotA,Rest)).
  942*/
  943assert_axiom_2(AxHead, B) :- \+ is_list(B), !,
  944  conjuncts_to_list_body(B,Bs),
  945  assert_axiom_2(AxHead, Bs).
  946
  947assert_axiom_2(AxHead, B) :- 
  948  must_maplist(fix_symetrics(AxHead), B,Bs)-> B\== Bs,
  949  assert_axiom_2(AxHead, Bs).
  950
  951assert_axiom_2(AxHead, Some):- use_proxy_kr, Some=[_,_|_],  member(E,Some), E = (_;_), 
  952   term_variables(E,Vars),
  953   gensym(disj_,Ref),
  954   P =.. [Ref|Vars],
  955   subst(Some,E,P,NewSome), !,
  956   assert_ele('->'(E,P)),
  957   assert_axiom_2(AxHead, NewSome).
  958
  959assert_axiom_2(AxHead, Some):- use_proxy_kr, select(E,Some,Rest), E = (_;_), Rest\==[], !,
  960   term_variables(E,Vars),
  961   gensym(disj_,Ref),
  962   P =.. [Ref|Vars],
  963   assert_ele('->'(E,P)),
  964   assert_axiom_2(AxHead, [P|Rest]).
  965
  966assert_axiom_2(AxHead, Some):- breakup_ors, select(E,Some,Rest), E = (A;B), !,
  967   assert_axiom_2(AxHead, [A|Rest]),
  968   assert_axiom_2(AxHead, [B|Rest]).
  969
  970/*
  971assert_axiom((A1,A2), B):- 
  972  assert_axiom(A1, [possible(A2)|B]),
  973  assert_axiom(A2, [possible(A1)|B]).
  974assert_axiom(A1;A2, B):- 
  975  assert_axiom(A1, [not(A2)|B]),
  976  assert_axiom(A2, [not(A1)|B]).
  977*/
  978
  979assert_axiom_2(H,B):- 
  980  compound(H), compound_name_arity(H, F, 2), needs_cononicalization(F), !,
  981  list_to_conjuncts(B, BB),
  982  assert_m_axiom('->'(BB,H)).
  983
  984assert_axiom_2(H,B):-
  985  assert_ready(axiom(H,B)).
  986
  987% Normals
  988assert_effect(Effect,(A1,A2),Fluent,T,B):- !,
  989   assert_effect(Effect,A1,Fluent,T,[possible(A2)|B]),
  990   assert_effect(Effect,A2,Fluent,T,[possible(A1)|B]).
  991assert_effect(Effect,(A1;A2),Fluent,T,B):- !,
  992   assert_effect(Effect,A1,Fluent,T,[possible(not(A2))|B]),
  993   assert_effect(Effect,A2,Fluent,T,[possible(not(A2))|B]).
  994
  995breakup_ors:- fail.
  996use_proxy_kr:- fail.
  997
  998:- use_module(ec_nnf).  999
 1000
 1001:- export_transparent(rect/0).    
 1002
 1003% recompiles and restart tests everytime source is updated
 1004rect:- once(ect), % first run
 1005   repeat,
 1006   wait_for_input([current_input],Was,0.5), 
 1007   make:modified_file(_Any),
 1008   once(ect), 
 1009   Was == [current_input]. 
 1010
 1011rect2:- 
 1012   once(ect), % first 
 1013   wait_for_input([current_input],Was,0.5), 
 1014   ( \+ make:modified_file(_Any) -> rect2; 
 1015   ( Was \== [current_input] -> rect2; true)). 
 1016  
 1017                         
 1018
 1019% event calc tests
 1020:- export_transparent(ect/0). 1021ect:- call(call,ect1).
 1022
 1023:- export_transparent(ect1/0). 1024ect1:- 
 1025   cls, update_changed_files,  Out = translate_e_to_pfc,
 1026   call(Out, ['../*/*/*/*.e','../*/*/*.e','../*/*.e']),
 1027   list_undefined,
 1028   list_void_declarations,  
 1029  !.
 1030
 1031:- export_transparent(ect2/0). 1032ect2:- 
 1033   cls, update_changed_files,  Out = translate_e_to_pfc,
 1034   call(Out, 'examples/FrankEtAl2003/Story1.e'),
 1035   % call(Out, 'ectest/ec_reader_test_ecnet.e'),
 1036   call(Out, 'ecnet/GSpace.e'),
 1037   call(Out, 'ecnet/Diving.e'),
 1038   call(Out, 'ecnet/RTSpace.e'),
 1039   call(Out, 'ecnet/SpeechAct.e'),
 1040   call(Out, 'ecnet/Kidnapping.e'),
 1041   call(Out,'examples/Mueller2006/Exercises/MixingPaints.e'),
 1042   call(Out,'examples/Mueller2006/Chapter11/HungryCat.e'),
 1043   call(Out, 'examples/AkmanEtAl2004/ZooWorld.e'),   
 1044   % call(Out,'examples/Mueller2006/Chapter11/*.e'),
 1045
 1046   list_undefined,
 1047   list_void_declarations,  
 1048  !.
 1049
 1050:- export_transparent(ect1_cvt_e_pl/0). 1051ect1_cvt_e_pl:- 
 1052   cls, update_changed_files,  Out = cvt_e_pl,
 1053   call(Out, ['../*/*/*/*.e','../*/*/*.e','../*/*.e']),
 1054   list_undefined,
 1055   list_void_declarations,  
 1056  !.
 1057
 1058:- export_transparent(ect2_cvt_e_pl/0). 1059ect2_cvt_e_pl:- 
 1060   cls, update_changed_files,  Out = cvt_e_pl,
 1061   call(Out, 'examples/FrankEtAl2003/Story1.e'),
 1062   % call(Out, 'ectest/ec_reader_test_ecnet.e'),
 1063   call(Out, 'ecnet/GSpace.e'),
 1064   call(Out, 'ecnet/Diving.e'),
 1065   call(Out, 'ecnet/RTSpace.e'),
 1066   call(Out, 'ecnet/SpeechAct.e'),
 1067   call(Out, 'ecnet/Kidnapping.e'),
 1068   call(Out,'examples/Mueller2006/Exercises/MixingPaints.e'),
 1069   call(Out,'examples/Mueller2006/Chapter11/HungryCat.e'),
 1070   call(Out, 'examples/AkmanEtAl2004/ZooWorld.e'),   
 1071   % call(Out,'examples/Mueller2006/Chapter11/*.e'),
 1072
 1073   list_undefined,
 1074   list_void_declarations,  
 1075  !.
 1076
 1077
 1078
 1079fix_goal_add_on_arg(T, G, G0, [b(T,T2),b(T2,end)]):- G =.. [F,A], already_good(F,2), G0 =.. [F,A,T].%, next_t(T,T2).
 1080fix_goal_add_on_arg(T, G, G0, [b(T,T2),b(T2,end)]):- G =.. [F,A,B], already_good(F,3), \+ already_good(F,2), G0 =.. [F,A,B,T]. %, next_t(T,T2).
 1081
 1082
 1083:- export_transparent(fix_goal/3). 1084
 1085
 1086to_axiom_head(T,G,GG) :-  notrace(fix_axiom_head(T,G,GG)),!.
 1087to_axiom_head(T,G,GG) :-  trace,fix_axiom_head(T,G,GG),!.
 1088
 1089
 1090fix_goal(_, Nil,[]):- Nil==[],!.
 1091fix_goal(T,[G|Gs],GGs):- !, fix_goal(T,G,G0),fix_goal(T,Gs,Gs0),append(G0,Gs0,GGs),!.
 1092fix_goal(T,(G,Gs),GGs):- !, fix_goal(T,G,G0),fix_goal(T,Gs,Gs0),append(G0,Gs0,GGs),!.
 1093fix_goal(T,{Gs},{GGs}):- !, fix_goal(T,Gs,GGs).
 1094fix_goal(T, G, GGs):- into_lps, (fix_axiom_head(T,G,GG)-> G\==GG), !, fix_goal(T, GG, GGs).
 1095fix_goal(T, G, GGs):- fix_axiom_head(T,G,GG),!, listify(GG,GGs).
 1096fix_goal(T, G, [Gs| TExtra]):-  \+ into_lps, fix_goal_add_on_arg( T, G, Gs, TExtra),!.
 1097fix_goal(T, G, GGs):- to_axiom_head(T,G,GG),!, listify(GG,GGs).
 1098fix_goal(_, holds_at(G, T3), [holds_at(G, T3)]):- into_dec_pl,!.
 1099fix_goal(T, G, [holds_at(G, T)]):- into_dec_pl,!.
 1100
 1101
 1102ec_to_ax(_, X,Y):-  (\+ callable(X) ; \+ compound(X)), !, X=Y.
 1103%ec_to_ax(T, (Pre -> iff(HB,BH)), HBO):- ec_to_ax(T, (iff((Pre,HB),(Pre,BH))), HBO).
 1104%ec_to_ax(T, or(Pre , '->'(HB,BH)), HBO):- ec_to_ax(T, '->'(or(Pre , HB),BH), HBO).
 1105%ec_to_ax(T, (H<-B),O):- !, into_axiom(T,H,B,O).
 1106ec_to_ax(T, '->'(B,H),O):- !, into_axiom(T,H,B,O).
 1107ec_to_ax(T, '<->'(HB1,HB2),[A,B]):- !, ec_to_ax(T, '->'(HB1,HB2),A),ec_to_ax(T, '->'(HB2,HB1),B).
 1108ec_to_ax(T, axiom(H,B),O):- into_axiom(T,H,B,O), !.
 1109ec_to_ax(_, axiom(H,B), axiom(H,B)):- !.
 1110ec_to_ax(T,X,O):- fix_axiom_head(T,X,Y), !, (X==Y -> X=O ; ec_to_ax(T,Y,O)),!.
 1111ec_to_ax(_, X,X).
 1112
 1113to_axiom_body(T,G,GGs) :-  fix_goal(T,G,GGs).
 1114
 1115%into_axiom(T,H,happens_at(E,T),OUT):- into_axiom(T,not(happens_at(E,T)),not(H),OUT).
 1116into_axiom(T,H,B,'->'(ABNonList,AH)):- to_axiom_head(T1,H,AH),
 1117  to_axiom_body(T2,B,AB),!,ignore(T=T1),ignore(T2=T1),
 1118  list_to_conjuncts(AB, ABNonList),!.
 1119
 1120
 1121
 1122
 1123
 1124%as_equals(X,Y,=(X,Y)):-!.
 1125%as_equals(X,Y,Equals):- compound(X),append_term(X,Y, Equals),!.
 1126as_equals(X,Y,equals(X,Y)).
 1127
 1128
 1129syntx_term_check(G):- var(G),!,fail.
 1130syntx_term_check(G):- is_ftVar(G),!,fail.
 1131syntx_term_check((G1;G2)):- !, syntx_term_check(G1); syntx_term_check(G2).
 1132syntx_term_check(G):- predicate_property(G,clause_count(_)), clause(G,_).
 1133syntx_term_check(G):- clause(ec_current_domain_db(G, _),_).
 1134syntx_term_check(G):- into_lps, G=..[F,A], ec_lps_convert:argtype_pred(F,FS),GS=..[FS,[A]],syntx_term_check(GS).
 1135
 1136
 1137functor_skel(G,P):- compound(G), compound_name_arity(G,F,A), compound_name_arity(P,F,A),!.
 1138functor_skel(G,P):- atom(G),P=G.
 1139
 1140between_r(H,L,N):- nonvar(N),!,between(L,H,N).
 1141between_r(H,L,N):- Hm1 is H - L, !, between(L,H,NN), N is NN + Hm1.
 1142
 1143can_be_time_arg(Var):- is_ftVar(Var),!.
 1144can_be_time_arg(_+_):-!.
 1145can_be_time_arg(_-_):-!.
 1146can_be_time_arg(A):- atom(A).
 1147
 1148semi_legit_time(V,_):- \+ compound_gt(V,0), !, fail.
 1149semi_legit_time(Holds,T1):- sub_term(Holds1,Holds),compound_gt(Holds1,0),
 1150   functor(Holds1,F,_),
 1151   time_arg(F,N), arg(N,Holds1,T1),can_be_time_arg(T1).
 1152semi_legit_time(Holds,T1):- sub_term(Holds1,Holds),compound_gt(Holds1,0),
 1153   functor(Holds1,F,_),
 1154   time_arg(F,N), arg(N,Holds1,T1),\+ can_be_time_arg(T1).
 1155
 1156/*
 1157semi_legit_time(Holds1,T1):- 
 1158   functor(Holds1,_,A), 
 1159   member(P1,[number,string,atom]),
 1160   (arg(A,Holds1,T1);arg(_,Holds1,T1)), 
 1161   T1\==[], call(P1,T1).
 1162*/
 1163
 1164:- export_transparent(compare_on_time_arg/3). 1165compare_on_time_arg(Result,Holds1,Holds2):- 
 1166   (((semi_legit_time(Holds1,T1),semi_legit_time(Holds2,T2),
 1167      compare(Result,T1,T2), Result\== (=))) 
 1168     -> true;
 1169        compare_on_time_arg(Result,Holds1,Holds2)).
 1170
 1171time_arg(b, N):- between(1,2,N).
 1172time_arg(beq, N):- between(1,2,N).
 1173time_arg(holds_at, 2).
 1174time_arg(is_time, 1).
 1175time_arg(happens_at, N):- between_r(3,2,N), N\=1.
 1176time_arg(clipped, N):- between_r(3,1,N), N\=2.
 1177time_arg(declipped, N):- between_r(3,1,N), N\=2.
 1178time_arg(F, N):- arg_info(axiom_head,F,V),compound(V),arg(N,V,time).
 1179
 1180get_time_values(G,Set):- (setof(ST,semi_legit_time(G,ST),List),list_to_set(List,Set))->true;Set=[].
 1181:- export_transparent(fix_time_args/3). 1182fix_time_args(T,G,Gss):- \+ is_list(G), conjuncts_to_list_body(G, Gs), !,fix_time_args(T,Gs,Gss)   .
 1183fix_time_args(T,[G|Gs],Gss):- 
 1184  semi_legit_time([G|Gs],ST),
 1185  fix_time_args1(ST,[G|Gs],Gs0),
 1186  fix_time_args2(T,Gs0,Gss).
 1187
 1188%fix_time_args2(_,Gs,Gs):-!.
 1189fix_time_args2(_,Gs,Gss):-
 1190  list_to_set([b(start,t),b(t,end)|Gs],Gss),!.
 1191
 1192visit_time_args(_,   In,G,G,In):- \+ compound(G),!.
 1193visit_time_args(Stem,In,[G|Gs],[GO|GsO],Out):- !, 
 1194    visit_time_args(Stem,In,G,GO,Mid),
 1195    visit_time_args(Stem,Mid,Gs,GsO,Out).
 1196visit_time_args(Stem,In,holds_at(A,T1),holds_at(A,T1R),Out):- !,
 1197   correct_time_arg(Stem,In,T1,T1R,Out).
 1198visit_time_args(Stem,In,happens_at(A,T1,T2),happens_at(A,T1R,T2R),Out):- !,
 1199   correct_time_arg(Stem,In,T1,T1R,B0),
 1200   correct_time_arg(Stem,B0,T2,T2R,Out).
 1201visit_time_args(Stem,In,happens_at(A,T1),happens_at(A,T1R),Out):- !,
 1202   correct_time_arg(Stem,In,T1,T1R,Out).
 1203visit_time_args(Stem,In,b(T1,T2),b(T1R,T2R),Out):- !,
 1204   correct_time_arg(Stem,In,T1,T1R,B0),
 1205   correct_time_arg(Stem,B0,T2,T2R,Out).
 1206visit_time_args(Stem,In,not(G),not(GG),Out):- !, visit_time_args(Stem,In,G,GG,Out).
 1207visit_time_args(Stem,In,beq(T1,T2),beq(T1R,T2R),Out):- !,
 1208   correct_time_arg(Stem,In,T1,T1R,B0),
 1209   correct_time_arg(Stem,B0,T2,T2R,Out).
 1210visit_time_args(Stem,In,clipped(T1,A,T2),clipped(T1R,A,T2R),Out):- !,
 1211   correct_time_arg(Stem,In,T1,T1R,B0),
 1212   correct_time_arg(Stem,B0,T2,T2R,Out).
 1213visit_time_args(Stem,In,declipped(T1,A,T2),declipped(T1R,A,T2R),Out):- !,
 1214   correct_time_arg(Stem,In,T1,T1R,B0),
 1215   correct_time_arg(Stem,B0,T2,T2R,Out).
 1216visit_time_args(Stem,In, HT, HTO,Out):- compound_name_arguments(HT, F, L), !,
 1217  visit_time_f_args(Stem,In,F,1,L, LL,Out),
 1218  compound_name_arguments(HTO, F, LL).
 1219
 1220visit_time_f_args(_Stem,InOut,_, _, [], [],InOut):-!.
 1221visit_time_f_args(Stem,In,F, N, [T2|L], [T2R|LL],Out):- time_arg(F,N),!,
 1222   correct_time_arg(Stem,In, T2,T2R,MID),N2 is N+1,
 1223   visit_time_f_args(Stem,MID,F, N2, L, LL,Out).
 1224visit_time_f_args(Stem,In,F, N, [HT|L], [HTO|LL], Out):- N2 is N+1,
 1225   visit_time_args(Stem,In, HT, HTO, MID),
 1226   visit_time_f_args(Stem,MID,F, N2, L, LL,Out).
 1227
 1228
 1229correct_time_arg(_Stem,In, TN, TN, In):- is_ftVar(TN), !.
 1230correct_time_arg(_Stem,In, TN, TN, In):- TN==start, !.
 1231correct_time_arg(_Stem,In, TN, TN, In):- atom(TN), !.
 1232correct_time_arg(_Stem,In, AM1,T, In):- compound(AM1),(AM1 = (AfterT- N)),compound(AfterT),after(T)=AfterT, N==1, is_ftVar(T), !.
 1233correct_time_arg(Stem, In, TN, TpN, Out):- number(TN), !, correct_time_arg(Stem,In, Stem+TN, TpN, Out).
 1234correct_time_arg(_Stem,In, v, _, In):- !.
 1235correct_time_arg(_Stem,In, TN, TpN, In):- lookup_time_val(TN,TpN,In),!.
 1236correct_time_arg(Stem,In, TN, TpN, [ignore(TN==TpN)|Out]):-  number(TN), !, correct_time_arg(Stem,In, Stem+TN, TpN, Out).
 1237correct_time_arg(Stem,In, T-N, TpN, Out):- number(N), N<0, NN is abs(N),!,correct_time_arg(Stem,In, T+NN, TpN, Out).
 1238correct_time_arg(Stem,In, T+N, TpN, Out):- number(N), N<0, NN is abs(N),!,correct_time_arg(Stem,In, T-NN, TpN, Out).
 1239correct_time_arg(Stem,In, Now+N, T, [ignore(Now+N==T)|Out]):- concat_time_arg_syms, number(N), N>1, NN is N-1, correct_time_arg(_Stem,In, Now+1, Tm2, Mid),
 1240  correct_time_arg(Stem, Mid, Tm2+NN, T, Out).
 1241correct_time_arg(Stem,In, Now-N, T, [ignore(Now-N==T)|Out]):- concat_time_arg_syms, number(N), N<1, NN is N+1, correct_time_arg(_Stem,In, Now-1, Tm2, Mid),
 1242  correct_time_arg(Stem, Mid, Tm2-NN, T, Out).
 1243correct_time_arg(_Stem,In, T+N, T, In):- N==0,!.
 1244correct_time_arg(_Stem,In, T-N, T, In):- N==0,!.
 1245correct_time_arg(_Stem,In, T-N, TN, Out):- !, t_plus_or_minus_1(In, T-N, TN, Out).
 1246correct_time_arg(_Stem,In, T+N, TN, Out):- !, t_plus_or_minus_1(In, T+N, TN, Out).
 1247correct_time_arg(_Stem,In, TN, TN, In).
 1248
 1249concat_time_arg_syms:- fail.
 1250
 1251lookup_time_val(TN,TpN,In):- copy_term(TN,TNS),member(ignore(TNS==TpN),In),TNS=@=TN,!.
 1252
 1253t_plus_or_minus_1(In, TN, TpN, In):- lookup_time_val(TN,TpN,In),!.
 1254t_plus_or_minus_1(In, T-N, TN, In):- N==1, memberchk(b(TN,T),In),!.
 1255t_plus_or_minus_1(In, T+N, TN, In):- N==1, memberchk(b(T,TN),In),!.
 1256t_plus_or_minus_1(In, T-N, TN, [b(TN,T),ignore(T-N==TN)|In]):- N==1,!.
 1257t_plus_or_minus_1(In, T+N, TN, [b(T,TN),ignore(T+N==TN)|In]):- N==1,!.
 1258t_plus_or_minus_1(In, T+N, TN, [b(T,TN),toffset(T,N,TN),ignore(T+N==TN)|In]):- is_ftVar(N),!.
 1259t_plus_or_minus_1(In, T-N, TN, [b(TN,T),toffset(TN,N,T),ignore(T-N==TN)|In]):- is_ftVar(N),!.
 1260t_plus_or_minus_1(In, T+N, TN, [b(T,TN),toffset(T,N,TN),ignore(T+N==TN)|In]):- number(N),!,debug_var([T,N],TN).
 1261t_plus_or_minus_1(In, T-N, TN, [b(TN,T),toffset(TN,N,T),ignore(T-N==TN)|In]):- number(N),!,debug_var([T,minus,N],TN).
 1262%t_plus_or_minus_1(In, T-N, TN, [b(TN,T),ignore(T-N==TN)|In]):- N==1, must((next_t(TN,T))),!.
 1263%t_plus_or_minus_1(In, T+N, TN, [b(T,TN),ignore(T+N==TN)|In]):- N==1, must((next_t(T,TN))),!.
 1264t_plus_or_minus_1(In, T-N, TN, [b(TN,T),ignore(T-N==TN)|In]):- ((ground(T+N), atomic_list_concat([T,N],minus,TN))),!.
 1265t_plus_or_minus_1(In, T+N, TN, [b(T,TN),ignore(T+N==TN)|In]):- ((ground(T+N), atom_concat(T,N,TN))),!.
 1266t_plus_or_minus_1(In, T-N, TN, [b(TN,T),ignore(T-N==TN)|In]):- gensym(t_less,TN).
 1267t_plus_or_minus_1(In, T+N, TN, [b(T,TN),ignore(T+N==TN)|In]):- gensym(t_more,TN).
 1268/*
 1269next_t(T,Var):- is_ftVar(T),is_ftVar(Var),!.
 1270next_t(start,t).
 1271next_t(T,Var):- is_ftVar(T),!,Var=after(T).
 1272next_t(t,now).
 1273next_t(now,aft).
 1274next_t(aft,Aft_1):- is_ftVar(Aft_1),!,gensym(aft_,Aft_1).
 1275next_t(aft,completeFn(_)).
 1276*/
 1277
 1278fix_time_args1(T,G,Gs):- 
 1279  visit_time_args(T,[],G,Gs,_Mid).
 1280
 1281
 1282
 1283already_good(comparison, 3).
 1284already_good(some, 2).
 1285already_good(some, 1).
 1286already_good(call, 1).
 1287already_good(requires, 2).
 1288already_good(equals, 2).
 1289already_good(axiom_uses, 2).
 1290already_good(is, 2).
 1291already_good(diff, 2).
 1292already_good(dif, 2).
 1293already_good(allDifferent, 1).
 1294already_good(terms_or_rels,3).
 1295already_good(ignore, 1).
 1296already_good(F,A):- into_dec_pl, already_good_dec_pl(F,A).
 1297
 1298already_good_dec_pl(happens_at, 2).
 1299already_good_dec_pl(happens_at, 3).
 1300already_good_dec_pl(holds_at, 2).
 1301already_good_dec_pl(holds_at, 3).
 1302already_good_dec_pl(b, 2).
 1303already_good_dec_pl(toffset, 3).
 1304already_good_dec_pl(F, 1):- arg_info(domain,F,arginfo).
 1305already_good_dec_pl(F, N):- arg_info(axiom_head,F,Args),compound(Args),functor(Args,v,N).
 1306already_good_dec_pl(F, 1):- fixed_already(F).
 1307already_good_dec_pl(F,A):- functor(P,F,A),syntx_term_check(abducible(PP)),compound(PP),PP=P.
 1308already_good_dec_pl(F,A):- functor(P,F,A),syntx_term_check(predicate(PP)),compound(PP),PP=P.
 1309
 1310
 1311
 1312%predicate, option range load fluent event noninertial xor completion
 1313
 1314
 1315%special_directive('!').
 1316%special_directive('neg').
 1317
 1318% builtin_pred(releasedAt).
 1319
 1320%xfr_body(true,[]).
 1321
 1322
 1323
 1324:- export_transparent(get_linfo/1). 1325
 1326get_linfo(lsvm(L,F,Vs,M)):- 
 1327  quietly((must(ec_reader:s_l(F,L)),!,
 1328  '$current_source_module'(M),
 1329  nb_current('$variable_names',Vs))).
 1330
 1331
 1332
 1333                    
 1334
 1335brk_on:attr_unify_hook(Var,Vars):- brk_on_unify_hook(Var,Vars).
 1336brk_on:attribute_goals(Var,[brk_on(Vars,Var)|L],L):- get_attr(Var,brk_on,Vars).
 1337
 1338brk_on_unify_hook(Var,Vars):- 
 1339 (is_ftVar(Var), \+ ( member(E,Vars), E==Var)) -> true ;
 1340    if_debugging(ec,((dumpST,wdmsg(brk_on(Var)),break))).
 1341
 1342brk_on_bind(HB):- term_variables(HB,Vars),must_maplist(brk_on(Vars),Vars).
 1343brk_on(Vars,X):- ord_del_element(Vars,X,Rest),put_attr(X,brk_on,Rest).
 1344
 1345
 1346
 1347needs_process_axiom(C):- \+ compound(C), !, fail.
 1348needs_process_axiom(axiom(_,_)).
 1349needs_process_axiom(axiom(_)).
 1350needs_process_axiom(abducible(_)).
 1351needs_process_axiom(executable(_)).
 1352needs_process_axiom(P):- compound_name_arity(P,F,A),needs_process_axiom_fa(F,A).
 1353
 1354needs_process_axiom_fa(iff,2).
 1355%needs_process_axiom_fa('<-',2).
 1356needs_process_axiom_fa('->',2).
 1357needs_process_axiom_fa(F,A):- arg_info(_,F,Args), (Args==arginfo-> true; functor(Args,_,A)).
 1358
 1359
 1360:- export_transparent(needs_proccess/3). 1361needs_proccess(_File, PA,_):- \+ compound(PA),!,fail.
 1362needs_proccess( File, M:H, How):- !, M\==system, nonvar(H),!,needs_proccess(File, H,How).
 1363needs_proccess(_File, PA, process_ec):- needs_process_axiom(PA),!.
 1364needs_proccess( File, (axiom(_,_) :- _),process_ec):- \+ skipped_ec_file(File), !.
 1365needs_proccess( File, (H :- _),How):- \+ skipped_ec_file(File), !, nonvar(H),!,needs_proccess(File, H,How).
 1366
 1367:- export_transparent(process_ec/1). 1368
 1369process_ec( HB ):- notrace(must(get_linfo(T))), process_ec( T, HB ).
 1370%:- export_transparent(process_ec/2).
 1371%process_ec( _, HB , T):- !,process_ec( T, HB ).
 1372
 1373
 1374:- export_transparent(process_ec/2). 1375
 1376process_ec( _, HB ):- brk_on_bind(HB), assert_ele(HB),!.
 1377process_ec( lsvm(L,S,Vs,M), HB ):- fail,  
 1378  must(convert_to_axiom(lsvm(L,S,Vs,M),HB,NEWHB)),
 1379  do_process_ec(assertz,M, NEWHB).
 1380
 1381merge_into_body(X,_Y,Z):- Z = X.
 1382
 1383:- export_transparent(do_process_ec/3). 1384do_process_ec(_Why, M, NonCallable) :- break, assertion((current_module(M),callable(NonCallable))), fail.
 1385do_process_ec(Why, M, NEWHB):- is_list(NEWHB), !, must_maplist(do_process_ec(Why, M), NEWHB).
 1386do_process_ec(_Why, M, (:- GOAL)):- !, must(M:GOAL).
 1387do_process_ec(_Why, M, (?- GOAL)):- !, (M:forall(GOAL, true)).
 1388% How to? M:assertz('$source_location'(S, L):NEWHB),
 1389%do_process_ec(Why, M, NEWHB):- wdmsg(do_process_ec(Why, M, NEWHB)),fail.
 1390do_process_ec(Why, M, NEWHB):- M:call(Why, NEWHB).
 1391
 1392e_reader_teste2:- 
 1393     convert_to_axiom(fff,
 1394  ((holds_at(beWaiter3(waiterOf(Restaurant)), Time),
 1395    exists([Agent], holds_at(knowOrder(waiterOf(Restaurant), Agent, Food), Time))) ->
 1396       ( happens_at(order(waiterOf(Restaurant),
 1397                      cookOf(Restaurant),
 1398                      Food),
 1399                Time))),O),
 1400     assert_ready(e,O).
 1401
 1402:- export_transparent(convert_to_axiom/3). 1403convert_to_axiom(T,A,A):- into_lps, throw(convert_to_axiom(T,A,A)),!.
 1404convert_to_axiom(T, M:H, [M:HH]):- !, convert_to_axiom(T, H, HH).
 1405convert_to_axiom(T, (H:-B),[(HH:- B)]):- !, convert_to_axiom(T, H,HH).
 1406convert_to_axiom(_, abducible(H), abducible(H)):- !.
 1407convert_to_axiom(_, t(C, E), List):- !, to_fact_head([sort(C),t(C, E)],List).
 1408
 1409convert_to_axiom(L,[H|T],ABC):- % trace, 
 1410   once((convert_to_axiom(L,H,A), convert_to_axiom(L,T,B),append(A,B,AB))), 
 1411   AB\=@= [H|T],
 1412   convert_to_axiom(L,AB,ABC).
 1413
 1414convert_to_axiom(T, (Pre -> '<->'(HB,BH)), HBO):-
 1415  convert_to_axiom(T, ('<->'((Pre,HB),(Pre,BH))), HBO),!.
 1416
 1417convert_to_axiom(T, '<->'(HB,BH), HBOO):-
 1418  convert_to_axiom(T, '->'(HB,BH), HBO1),
 1419  convert_to_axiom(T, '->'(BH,HB), HBO2),
 1420   % convert_to_axiom(T, '<-'(HB,BH), HBO2),
 1421  flatten([HBO1,HBO2],HBO),
 1422  convert_to_axiom1(T,HBO,HBOO),!.
 1423
 1424
 1425convert_to_axiom(T, exists(Vars,BH), HBO):- convert_exists(exists(Vars,BH), Conj),!,
 1426  convert_to_axiom(T, Conj , HBO).
 1427%convert_to_axiom(T, exists(Vars,Info), HBO):- !, convert_to_axiom(T, Info, HB), 
 1428%  merge_into_body(HB,some(Vars),HBO).
 1429
 1430%  compound_name_arity(P,F,A),compound_name_arity(PP,F,A).
 1431
 1432
 1433convert_to_axiom(T, X, O):- nop(debug_var('AxTime',Time)), ec_to_ax(Time, X,Y), 
 1434  (is_list(Y)->convert_to_axiom1(T, Y, O); (X\=Y -> convert_to_axiom(T, Y, O);convert_to_axiom1(T, Y, O))), !.
 1435convert_to_axiom(T, Y, O):- convert_to_axiom1(T, Y, O).
 1436
 1437% convert_to_axiom1(T, '->'(E,B), HBO2):- convert_to_axiom(T, precond(B,E), HBO2).
 1438to_fact_head(H,List):- H=List.
 1439
 1440
 1441convert_to_axiom1(_, EOF, []) :- EOF = end_of_file,!.
 1442convert_to_axiom1(T, P, O):- is_axiom_head(P),!, convert_to_axiom1(T, axiom(P), O).
 1443convert_to_axiom1(T, axiom(P), O):- convert_to_axiom1(T, axiom(P ,[]), O).
 1444convert_to_axiom1(_LSV, axiom(X,Y), [axiom(X,Y)]).
 1445convert_to_axiom1(LSV, Pred, [ec_current_domain_db(Pred,LSV)]).
 1446
 1447convert_exists( exists(Vars,B -> H), (B -> Conj)):- conjoin(H,some(Vars),Conj), !.
 1448convert_exists( exists(Vars, H), HBO):- conjoin(H,some(Vars),Conj), !,  Conj = HBO.
 1449
 1450is_axiom_head(P):- compound_name_arity(P,F,_), arg_info(axiom_head,F,_),!.
 1451is_axiom_head(P):- functor_skel(P, G), syntx_term_check(predicate(G)),!.
 1452
 1453
 1454arg_info(domain,event,arginfo).
 1455arg_info(domain,fluent,arginfo).
 1456arg_info(domain,action,arginfo).
 1457arg_info(domain,predicate,arginfo).
 1458arg_info(domain,function,arginfo).
 1459arg_info(domain,functional_predicate,v(pred,function)).
 1460
 1461arg_info(domain,reified_sort,arginfo).
 1462
 1463arg_info(abducible,noninertial,v(pred)).
 1464arg_info(abducible,completion,v(pred)).
 1465arg_info(abducible,next_axiom_uses,v(pred)).
 1466arg_info(abducible,sort,v(sort)).
 1467arg_info(abducible,subsort,v(sort,sort)).
 1468arg_info(abducible,range,v(atomic,int,int)).
 1469arg_info(abducible,t,v(sort,term)).
 1470%arg_info(domain,axiom,v(axiom,list)).
 1471
 1472%arg_info(axiom_head,b,v(time,time)).
 1473arg_info(axiom_head,requires,v(event,time)).
 1474arg_info(axiom_head,happens_at,v(event,time)).
 1475arg_info(axiom_head,happens_at,v(event,time,time)).
 1476
 1477arg_info(axiom_head,holds_at,v(fluent,time)).
 1478arg_info(axiom_head,holds_at,v(fluent,time,time)).
 1479arg_info(axiom_head,initially,v(fluent)).
 1480arg_info(axiom_head,initiates_at,v(event,fluent,time)).
 1481arg_info(axiom_head,terminates_at,v(event,fluent,time)).
 1482arg_info(axiom_head,releases_at,v(event,fluent,time)). 
 1483arg_info(axiom_head,released_at,v(fluent,time)). 
 1484arg_info(axiom_head,clipped,v(time,fluent,time)).
 1485arg_info(axiom_head,declipped,v(time,fluent,time)).
 1486arg_info(axiom_head,trajectory,v(fluent,time,fluent,offset)).
 1487arg_info(axiom_head,anti_trajectory,v(fluent,time,fluent,offset)).
 1488%arg_info(axiom_head,releasesAt,v(fluent,time)).
 1489arg_info_arity(Type,F,A):- arg_info(Type,F,Info), (atom(Info) -> A=1 ; functor(Info,_,A)).
 1490
 1491:- export(lock_ec_pred/2). 1492lock_ec_pred(F,A):- current_predicate(system:F/A),!.
 1493lock_ec_pred(F,A):- 
 1494  module_transparent(system:F/A),
 1495  functor(P,F,A),
 1496  assert((system:P:- ec_current_domain(P))),
 1497  compile_predicates([system:P]),
 1498  export(system:F/A),
 1499  user:import(system:F/A),
 1500  ec:import(system:F/A),
 1501  ec_loader:import(system:F/A),
 1502  ec_reader:import(system:F/A),
 1503  user:export(system:F/A),
 1504  lock_predicate(system:F/A),
 1505  listing(F/A).
 1506
 1507
 1508:- lock_ec_pred(axiom,2). 1509:- lock_ec_pred(executable,1). 1510:- lock_ec_pred(abducible,1). 1511:- forall((arg_info_arity(_,F,A),F\==t), lock_ec_pred(F,A)). 1512
 1513
 1514correct_ax_args(T,F,A,Args,axiom_head,_Arity,N, PP):-  N is A +1 ,!, append(Args,[T],NewArgs), PP =.. [F|NewArgs].
 1515correct_ax_args(_T,F,A,Args,axiom_head,_Arity,N,PP):- A=N, PP =.. [F|Args].
 1516correct_ax_args(_T,F,1,Args,domain,arginfo,0,PP):- PP =.. [F|Args].
 1517correct_ax_args(_T,F,2,[P,R],domain,arginfo,0,PP):- append_term(P,R,AB),PP =.. [F,AB].
 1518%orrect_ax_args(_4456,function,2,[side1(portal),location],domain,arginfo,0,_4470))
 1519
 1520%correct_ax_args(_T,initiates_at,2,[go(_1694),at(_1694)],axiom_head,3,v(event,fluent,time),_1684)
 1521%failed_must(correct_ax_args(_T,initiates_at,2,[go(_1694),at(_1694)],axiom_head,3,v(event,fluent,time),_1684))
 1522
 1523
 1524skipped_ec_file(File):- is_ftVar(File),fail.
 1525
 1526:- export_transparent(hook_ec_axioms/2). 1527
 1528:- (prolog:(import(hook_ec_axioms/2))). 1529
 1530hook_ec_axioms(What, File):- is_ftVar(File), !, current_input(Input), hook_ec_axioms(What, Input).
 1531hook_ec_axioms(What, file(_File,AbsFile)):- !, hook_ec_axioms(What, file(AbsFile)).
 1532hook_ec_axioms(What, file(AbsFile)):- !, hook_ec_axioms(What, AbsFile).
 1533hook_ec_axioms(What, File):- fail, 
 1534    prolog_load_context(module, M),
 1535    dmsg(hook_ec_axioms(M, What, File)),fail.
 1536hook_ec_axioms(_What, _File):- !.
 1537/*
 1538hook_ec_axioms(_What, File):- atom(File), exists_file(File),
 1539    forall(((clause(axiom(_, _), _Body, Ref), File==S)),
 1540       erase(Ref)),!.
 1541*/
 1542:- export(falling_edges/6). 1543
 1544falling_edges(V2,Stem_plus_, T_minus_1_Start, [Haps|List], Edges, Out):-
 1545  make_falling_edges(V2,Stem_plus_, T_minus_1_Start, [], [Haps|List], Edges, Out).
 1546  
 1547
 1548make_falling_edges(V2,Stem_plus_, T_minus_1_Start, SoFar, [Haps|List], Edges, Out):-
 1549  make_falling_edges(V2,Stem_plus_, T_minus_1_Start, SoFar, Haps, Edges1, Out1),
 1550  make_falling_edges(V2,Stem_plus_, T_minus_1_Start, Out1, List, Edges2, Out),
 1551  append(Edges1,Edges2,Edges).
 1552
 1553make_falling_edges(V2,Stem_plus_, T_minus_1_Start, SoFar, happens_at(Event,Time), Edges, Out):-
 1554  nop(vars(V2,Stem_plus_, T_minus_1_Start, SoFar, Edges, Out)),
 1555  Edges = [holds_at(has_occured(Event),Time)],
 1556  Out = SoFar,!.
 1557make_falling_edges(V2,Stem_plus_, T_minus_1_Start, SoFar, Was, Edges, Out):- 
 1558  nop(vars(V2,Stem_plus_, T_minus_1_Start, SoFar, Was, Edges, Out)),
 1559  Edges = [Was], Out = SoFar,!.
 1560
 1561
 1562%:- use_module(library(ec_planner/code_icl/'icl_int.tex')).
 1563%:- reexport(library(ec_planner/code_icl/'icl_int.tex')).
 1564
 1565:- fixup_exports. 1566
 1567:- multifile(user:message_hook/3). 1568:- dynamic(user:message_hook/3). 1569:- export_transparent(user:message_hook/3). 1570user:message_hook(load_file(start(_Level, File)),_,_):- hook_ec_axioms(load,File),fail.
 1571user:message_hook(include_file(start(_Level, File)),_,_):- hook_ec_axioms(include,File),fail.
 1572:- multifile(prolog:make_hook/2). 1573:- export_transparent(prolog:make_hook/2). 1574prolog:make_hook(before, Files):-  must_maplist(hook_ec_axioms(make(before)),Files), fail.
 1575
 1576:- multifile prolog:message//1. 1577prolog:message(welcome) -->  {hook_ec_axioms(welcome, welcome),fail}.
 1578
 1579
 1580
 1581:- multifile(user:term_expansion/4). 1582:- dynamic(user:term_expansion/4). 1583:- export_transparent(user:term_expansion/4). 1584:- user:import(ec_loader:needs_proccess/3). 1585:- user:import(ec_loader:process_ec/2). 1586user:term_expansion(In,P,Out,PO):-  fail,  \+ into_lps,
 1587  (\+ current_prolog_flag(ec_loader,false)),
 1588  source_location(File,_), 
 1589  notrace((nonvar(P),compound(In), In\=(:- _), 
 1590      needs_proccess(File, In, Type),PO=P)),
 1591  Out = ( :- call(Type, In) ).
 1592
 1593  
 1594
 1595
 1596% :- dynamic(axiom/2).
 1597/*
 1598axiom(initiates_at(wake_up(X), awake(X), _T), []).
 1599axiom(initiates_at(open(_, Y), opened(Y), _T), []).
 1600axiom(terminates_at(fall_asleep(X), awake(X), _T), []). 
 1601axiom(initially(neg(awake(N))), [N=nathan]). 
 1602axiom(initially(neg(opened(cont1))), []). 
 1603
 1604
 1605%:- dynamic(executable/1).
 1606executable(wake_up(_X)).
 1607executable(fall_asleep(_X)).
 1608executable(open(_X, _Y)).
 1609*/
 1610%:- dynamic(abducible/1).
 1611%abducible(dummy).
 1612% :- ec:abdemo([holds_at(awake(nathan), t)], R), writeq(R).
 1613/*
 1614  R = [[happens_at(wake_up(nathan), t1, t1)], [before(t1, t)]]
 1615
 1616                                            abdemo([holds_at(awake(nathan), t), holds_at(opened(foo), t)], R)
 1617*/
 1618
 1619%:- ec:abdemo([holds_at(awake(nathan), t), before(t, t2), holds_at(neg(awake(nathan)), t2)], R),writeq(R).