prob_rule_compiler

abstract_type(global(T),PrologVar,InAcc,OutAcc) :- b_supplementary_global_set(T), !,
    (member(type_par(T,PrologVar),InAcc) -> OutAcc=InAcc ; OutAcc = [type_par(T,PrologVar)|InAcc]).

abstract_type(set(T),set(AT)) --> !, abstract_type(T,AT).

abstract_type(seq(T),seq(AT)) --> !, abstract_type(T,AT).

abstract_type(couple(A,B),couple(AA,AB)) --> !, abstract_type(A,AA), abstract_type(B,AB).

abstract_type(T,T) --> [].

add_wd_condition(b(truth,pred,_),_,RHS,Res) :- !, Res=RHS.

add_wd_condition(WD,_Msg,RHS,Res) :- get_texpr_type(RHS,pred),!,
    print('Warning: WD conditions for predicates are translated using conjunction'),nl,
    conjunct_predicates([WD,RHS],Res).

add_wd_condition(WD,Msg,RHS,b(assertion_expression(WD,Msg,RHS),Type,[contains_wd_condition])) :-
    get_texpr_type(RHS,Type).

b_rewrite_rule(mandatory,['S'],['tt'],[additional_rhs_infos([prob_annotation('SYMBOLIC')])],
    'tree(S) = {tr|[]:dom(tr) & !(tt).(tt : dom(tr) => tt : seq(NATURAL1) & (tt /= [] => front(tt) : dom(tr) & (last(tt) > 1 => front(tt) <- last(tt) - 1 : dom(tr)))) & ran(tr) <: S}').

b_rewrite_rule(mandatory,['S'],['tt'],[additional_rhs_infos([prob_annotation('SYMBOLIC')])],
    'btree(S) = {tr|[]:dom(tr) & !(tt).(tt : dom(tr) => tt : seq(NATURAL1) & (tt /= [] => (front(tt) : dom(tr) & last(tt) : 1..2 & front(tt) <- (3-last(tt)) : dom(tr)))) & ran(tr) <: S}').

b_rewrite_rule(mandatory,['S'],[],[],
    'top(S) = S([])').

b_rewrite_rule(mandatory,['T','N'],[],[],
    'N:dom(T) => rank(T,N) = last(N)'). % should we check T:tree(_) ?

b_rewrite_rule(mandatory,['T','N'],[],[],
    'N:dom(T) => father(T,N) = front(N)'). % should we check T:tree(_) ?

b_rewrite_rule(mandatory,['T','N','I'],[],[],
    '(N:dom(T) & N <- I:dom(T)) => son(T,N,I) = N <- I'). % should we check T:tree(_) ?

b_rewrite_rule(mandatory,['X','Q'],[const_i,p,a,pi],[],
    'const(X,Q) = { [] |-> X} \\/ UNION(const_i).(const_i:dom(Q)| dom({pi,a,p| (p,a):Q(const_i) & pi=const_i->p}))').

b_rewrite_rule(mandatory,['T'],[son_x],[],
    '[] : dom(T) => sons(T) = dom({son_x,r,si|si:dom(T) & si/=[] & son_x=first(si) & r= {p,a|(son_x->p,a):T}})').

b_rewrite_rule(mandatory,['X'],[],[],'bin(X) = const(X,[])').

b_rewrite_rule(mandatory,['X','L','R'],[],[],'bin(L,X,R) = const(X,[L,R])').

b_rewrite_rule(mandatory,['X'],[],[],'left(X) = first(sons(X))').

b_rewrite_rule(mandatory,['X'],[],[],'right(X) = last(sons(X))').

b_rewrite_rule(mandatory,['T','N'],[],[],'subtree(T,N) = (%u.(u:(INTEGER<->INTEGER)|N^u) ; T)').

b_rewrite_rule(mandatory,['T','N'],[],[],'arity(T,N) = size(sons(subtree(T,N)))').

b_rewrite_rule(mandatory,['T'],[],[],'[]:dom(T) => sizet(T) = card(T)'). % TO DO: either recursive definition or better WD check

b_rewrite_rule(mandatory,['T'],['st','sn'],[],'prefix(T) = closure1(/*@ symbolic */ %(st,sn).(sn:(INTEGER<->ran(T)) & st /= [] & st:(INTEGER<->POW((INTEGER<->INTEGER)*ran(T))) | ((sons(first(st))^tail(st)) , sn <- top(first(st)) )))[{([T],[])}]([])'). % we could remove ran(T) typing

b_rewrite_rule(mandatory,['T'],['st','sn'],[],'postfix(T) = rev(closure1(/*@ symbolic */ %(st,sn).(sn:(INTEGER<->ran(T)) & st /= [] & st:(INTEGER<->POW((INTEGER<->INTEGER)*ran(T))) | ((rev(sons(first(st)))^tail(st)) , sn <- top(first(st)) )))[{([T],[])}]([]))'). % we could remove ran(T) typing

b_rewrite_rule(mandatory,['r'],[fnc_x],[],
    'fnc(r) = %(fnc_x).(fnc_x:dom(r)|r[{fnc_x}])'). % TO DO introduce LET for r if complex ?

b_rewrite_rule(mandatory,['r'],[rel_x,rel_y],[],
    'rel(r) = {rel_x,rel_y| rel_x:dom(r) & rel_y: union(r[{rel_x}])}').

b_rewrite_rule(optimize,['S'],[], [], '[] ^ S = S'). % TO DO: add SIDE CONDITION

b_rewrite_rule(optimize,['S'],[], [], 'S ^ [] = S'). % TO DO: add SIDE CONDITION

b_rewrite_rule(optimize,['X','D','R'],[xtf], [], 'D-->{R} = {%xtf.(xtf:D|R)}').

b_rewrite_rule(normalize,['X'],[pow_x],[],'POW(X) = {pow_x|pow_x<:X}').

b_rewrite_rule(normalize,['X'],[pow1_x],[],'POW1(X) = {pow1_x|pow1_x /= {} & pow1_x<:X}').

b_rewrite_rule(normalize,[],[],[],'NAT = 0..MAXINT').

b_rewrite_rule(normalize,[],[],[],'NAT1 = 1..MAXINT').

b_rewrite_rule(normalize,[],[],[],'INT = MININT..MAXINT').

b_rewrite_rule(normalize,[],[nat],[],'NATURAL = {nat|nat>=0}').

b_rewrite_rule(normalize,[],[nat1],[],'NATURAL1 = {nat1|nat1>=1}').

b_rewrite_rule(normalize,[],[id_x],[],'id(S) = %id_x.(id_x:S|id_x)').

check_grounding(LHS,RHS) :- copy_term((LHS,RHS),(L,R)),
    numbervars(L,0,_),
    (ground(R) -> true %,print('OK: Matching LHS grounds RHS')
    ; nl,print('### ILLEGAL RULE: RHS not grounded by matching LHS'),nl, print(R),nl
).

decompose_equality(b(implication(WD,Equality),pred,_),LHS,FullRHS) :- !,
    decompose_equality(Equality,LHS,RHS),
    get_texpr_expr(LHS,ELHS), functor(ELHS,Functor,_),
    ajoin(['WD Error for: ',Functor],Msg),
    add_wd_condition(WD,Msg,RHS,FullRHS).

decompose_equality(b(equal(LHS,RHS),pred,_),LHS,RHS) :- !.

decompose_equality(b(equivalence(LHS,RHS),pred,_),LHS,RHS) :- !.

decompose_equality(_,_,_) :- print('Cannot transform expression into Prolog rule: '),nl,
    print('Needs to be top-level equality or equivalence'),nl.

gen_id(ID,b(identifier(ID),_Type,[])).

gen_prolog_typevars(V,R) --> {var(V)},!,{R=V}.

gen_prolog_typevars(b(E,Type,I),b(E,AType,I)) --> abstract_type(Type,AType).

gen_prolog_vars(IDS,b(identifier(ID),Type,_),PROLOGVAR,Acc,NewAcc) :- member(ID,IDS),
    %print(c(ID,IDS,Type,Acc)),nl,
    ((member(metavar(ID,StoredType,PROLOGVAR),Acc),unify_types_strict(StoredType,Type))
    -> NewAcc=Acc ; NewAcc = [metavar(ID,Type,PROLOGVAR)|Acc]).

generate_rewrite_rule(IDS,Options,EqualityPred,PREDNAME,PrologRule) :-
    debug_println(parsing(EqualityPred)),
    parse_pred(EqualityPred,IDS,Equality),
    %print('PARSED : '), translate:print_bexpr(Equality),nl,
    decompose_equality(Equality,LHS,RHS),
    transform_bexpr(remove_info,LHS,CLHS),
    transform_bexpr(remove_pos,RHS,CRHS),
    debug_println(removed_pos),
    transform_bexpr_with_acc(gen_prolog_typevars,CLHS,PrologLHS1,[],Types1),
    transform_bexpr_with_acc(gen_prolog_typevars,CRHS,PrologRHS1,Types1,TypeParas),
    PrologLHS1 = b(Expr1,_,_), % still has typing info for sub arguments
    debug_println(type_parameters(TypeParas)),
    transform_bexpr_with_acc(gen_prolog_vars(IDS),PrologLHS1,PrologLHS,[],Vars1),
    transform_bexpr_with_acc(gen_prolog_vars(IDS),PrologRHS1,PrologRHS,Vars1,MetaVars),
    debug_println(vars(MetaVars)),
    PrologLHS=b(EXPR,TYPE,_),
    (member(additional_rhs_infos(Is),Options) -> append(Is,Info,Info1) ; Info1=Info),
    PrologRHS=b(NewEXPR,NewTYPE,_),
    functor(EXPR,Name,_), NewInfo=[was(Name)|Info1], % TO DO: propagate nodeid info into RHS
    % TO DO: add types of arguments as parameter
    safe_syntaxelement(Expr1,Subs,_,_,_),
    maplist(get_texpr_type,Subs,ArgTypes), % ArgTypes sometimes required to instantiate type variables in NewEXPR
    PrologRule =.. [PREDNAME,EXPR,TYPE,Info,ArgTypes,NewEXPR,NewTYPE,NewInfo,Name],
    %portray_clause(PrologRule),
    check_grounding((EXPR,TYPE,ArgTypes),(NewEXPR,NewTYPE)).

generate_rewrite_rules(Category,Stream) :-
    ajoin(['rewrite_rule_',Category],PREDNAME),
    format(':- module(rewrite_rules_db,[~w/8]).~n~n',[PREDNAME]),
    b_rewrite_rule(Category,IDS,_QuantifiedIDs,Options,EqualityPred),
    format(Stream,'~n% ~w~n',[EqualityPred]),
    (generate_rewrite_rule(IDS,Options,EqualityPred, PREDNAME,PrologRule) -> true
    ; format('*** GENERATING REWRITE RULE FAILED: ~w',[EqualityPred]),fail),
    portray_clause(Stream,PrologRule),
    fail.

generate_rewrite_rules(_,Stream) :- print('%-----'),nl,nl(Stream).

my_open(user_output,S) :- !, S=user_output.

my_open(File,Stream) :- open(File,write,Stream).

parse_expr(Atom,IDS,Res) :-
    temporary_set_preference(allow_untyped_identifiers,true,CHNG),
    atom_codes(Atom,Codes),
    maplist(gen_id,IDS,TIDS),
    b_parse_machine_expression_from_codes(Codes,[identifier(TIDS)],Res,_Type,true,_Error),
    reset_temporary_preference(allow_untyped_identifiers,CHNG).

parse_pred(Atom,IDS,Res) :-
    temporary_set_preference(allow_untyped_identifiers,true,CHNG),
    % TO DO: disable rewriting rules already in place ?!
    atom_codes(Atom,Codes),
    maplist(gen_id,IDS,TIDS),
    b_parse_machine_predicate_from_codes_open(no_quantifier,Codes,[identifier(TIDS)],[],Res),
    reset_temporary_preference(allow_untyped_identifiers,CHNG).

remove_info(b(E,T,_),b(E,T,_)).

remove_pos(b(E,T,I),b(E,T,NI)) :- (select(nodeid(_),I,NI) -> true ; NI=I).

testprc1 :-
    Atom = '{tr|!(tt).(tt : dom(tr) => tt : seq(NATURAL1) & (tt /= {} => front(tt) : dom(tr) & (last(tt) > 1 => front(tt) <- last(tt) - 1 : dom(tr)))) & ran(tr) <: S}',
    parse_expr(Atom,['S'],Res),
    translate:print_bexpr(Res),nl,
    print(Res),nl.

testprc2 :- %debug:tcltk_turn_debugging_on(2),
    generate_rewrite_rules(_,user_output).

write_rewrite_rules_to_file(Category,File) :- my_open(File,Stream),
    call_cleanup(generate_rewrite_rules(Category,Stream), close(Stream)).