input_syntax_tree

add_if_free(Id,Bound,In,Out) :-
    %(ordsets:is_ordset(Bound) -> true ; add_internal_error('Not ordset: ',add_if_free(Id,Bound))),
    (ord_member(Id,Bound) -> In=Out ; In=[Id|Out]).

create_fresh_identifier(PreferredName,Ast,Name) :-
    extract_raw_identifiers(Ast,UsedIds),
    ( memberchk(PreferredName,UsedIds) ->
    % Allready in use, find a fresh one by adding a number
    atom_codes(PreferredName,PreferredCodes),
    create_fresh_identifier_aux(PreferredCodes,UsedIds,1,Name)
    ;
    Name = PreferredName).

create_fresh_identifier_aux(PreferredCodes,UsedIds,I,Name) :-
    number_codes(I,ICodes),append(PreferredCodes,[95|ICodes],Codes),
    atom_codes(NewName,Codes),
    ( memberchk(NewName,UsedIds) ->
    % Allready in use, try again with a higher number
    I2 is I+1,
    create_fresh_identifier_aux(PreferredCodes,UsedIds,I2,Name)
    ;
    Name = NewName).

extract_raw_identifiers(Ast,Ids) :-
    extract_raw_identifiers2(Ast,[],Unsorted,[]),
    sort(Unsorted,Ids).

extract_raw_identifiers2([],_) --> !,[].

extract_raw_identifiers2([I|Irest],Bound) -->
    !,extract_raw_identifiers2(I,Bound),
    extract_raw_identifiers2(Irest,Bound).

extract_raw_identifiers2(identifier(_,I),Bound) --> !,add_if_free(I,Bound).

extract_raw_identifiers2(definition(_,I,Args),Bound) --> !,
    add_if_free(I,Bound),
    extract_raw_identifiers2(Args,Bound). % Note: we do not see the Ids inside the definition body!

extract_raw_identifiers2(Input,Bound) -->
    {raw_quantifier(Input,Ids,Subs)},!,
    %{append(Ids,Bound,NewBound)},
    {sort(Ids,SIds),ord_union(SIds,Bound,NewBound)},
    extract_raw_identifiers2(Subs,NewBound).

extract_raw_identifiers2(Input,Bound) -->
    {compound(Input),functor(Input,_Functor,Arity),Arity>1,!},
    extract_raw_identifiers3(2,Arity,Input,Bound).

extract_raw_identifiers2(_,_) --> [].

extract_raw_identifiers3(Pos,Arity,Input,Bound) -->
    {Pos=<Arity,!,Pos2 is Pos+1, arg(Pos,Input,Arg)},
    extract_raw_identifiers2(Arg,Bound),
    extract_raw_identifiers3(Pos2,Arity,Input,Bound).

extract_raw_identifiers3(_Pos,_Arity,_Input,_Bound) --> [].

flatten_couple_id_list(couple(_Pos,List)) --> !,
    % one could check that in Pos we have a pos_context with definition_call
    l_flatten_couple_id_list(List).

flatten_couple_id_list(OtherVal) --> {OtherVal=identifier(_,_)},[OtherVal].

get_definition_name(expression_definition(_Pos,Name,_Args,_Body),Name).

get_definition_name(predicate_definition(_Pos,Name,_Args,_Body),Name).

get_definition_name(substitution_definition(_Pos,Name,_Args,_Body),Name).

get_introduced_ids(Replaces,Ids) :- maplist(get_rhs_ids,Replaces,ListOfList),
    ord_union(ListOfList,Ids).

get_raw_position_info(Compound,Info) :-
    try_get_raw_position_info(Compound,Info),
    is_position(Info),!.

get_raw_position_info(Compound,Info) :-
    add_internal_error('Could not get position info: ',get_raw_position_info(Compound,Info)),
    Info = unknown.

get_rhs_ids(replace(_,New),Ids) :- extract_raw_identifiers(New,Ids).

l_flatten_couple_id_list([]) --> [].

l_flatten_couple_id_list([H|T]) --> !, flatten_couple_id_list(H), l_flatten_couple_id_list(T).

map_over(P,RawExpr,Res) :- map_over_raw_expr(RawExpr,P,Res).

map_over_raw_expr(RawExpr,P,Res) :- call(P,RawExpr,NewRawExpr),!,
    Res=NewRawExpr.

map_over_raw_expr(RawExpr,P,Res) :- recur_over_raw_expr(RawExpr,P,Res).

quantifier_capture_warning(Expr,IntroducedIds) :-
    raw_quantifier(Expr,SortedIds,_Body),
    ord_intersection(IntroducedIds,SortedIds,Clash),
    Clash \= [],
    % TO DO?: check if we really use a corresponding LHS identifier in Body: extract_raw_identifiers(Body,UsedIds), maplist(get_lhs_id,Replaces,LHSIds),
    %format('Quantifier ids: ~w~nIntroduced Ids: ~w~n',[SortedIds,IntroducedIds]),
    arg(1,Expr,Pos),
    add_warning(definition_variable_capture,'Quantifier may capture identifiers in DEFINITION arguments: ',Clash,Pos).

raw_conjunct([],truth(none)).

raw_conjunct([H|T],R) :-
    ( T=[] -> H=R
    ;
    R=conjunct(none,H,RT),
    raw_conjunct(T,RT)
).

raw_id(identifier(_,ID),ID).

raw_quantifier(Expr,SortedIds,Subs) :-
    raw_quantifier_aux(Expr,RawIds,Subs),
    maplist(raw_id,RawIds,Ids),
    sort(Ids,SortedIds).

raw_quantifier_aux(forall(_,Ids,P),Ids,[P]).

raw_quantifier_aux(exists(_,Ids,P),Ids,[P]).

raw_quantifier_aux(comprehension_set(_,Ids,P),Ids,[P]).

raw_quantifier_aux(event_b_comprehension_set(_,Ids,E,P),Ids,[E,P]).

raw_quantifier_aux(lambda(_,Ids,P,E),Ids,[P,E]).

raw_quantifier_aux(general_sum(_,Ids,P,E),Ids,[P,E]).

raw_quantifier_aux(general_product(_,Ids,P,E),Ids,[P,E]).

raw_quantifier_aux(quantified_union(_,Ids,P,E),Ids,[P,E]).

raw_quantifier_aux(quantified_intersection(_,Ids,P,E),Ids,[P,E]).

raw_quantifier_aux(any(_,Ids,P,S),Ids,[P,S]).

raw_quantifier_aux(let(_,Ids,P,S),Ids,[P,S]).

raw_quantifier_aux(var(_,Ids,S),Ids,[S]).

raw_quantifier_aux(recursive_let(_,Id,E),[Id],[E]).

raw_replace(Expr,[],Expr) :- !.

raw_replace(Old,Replaces,New) :-
    get_introduced_ids(Replaces,IntroducedIds), %print(intro(IntroducedIds)),nl,
    raw_replace2(Old,Replaces,IntroducedIds,New).

raw_replace2([],_,_,[]) :- !.

raw_replace2([E|Rest],Replaces,IntroducedIds,[N|NRest]) :- !,
    raw_replace2(E,Replaces,IntroducedIds,N),
    raw_replace2(Rest,Replaces,IntroducedIds,NRest).

raw_replace2(rewrite_protected(X),_Replaces,_,rewrite_protected(Y)) :- !,X=Y.

raw_replace2(becomes_such(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_such(Pos,NVars,NCond)) :- !,
    raw_replace2(Cond,Replaces,IntroducedIds,NCond),
    raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).

raw_replace2(becomes_element_of(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_element_of(Pos,NVars,NCond)) :- !,
    raw_replace2(Cond,Replaces,IntroducedIds,NCond),
    raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).

raw_replace2(identifier(Pos,Old),Replaces,_,New) :- !,
    (memberchk(replace(Old,New),Replaces) -> true ; New=identifier(Pos,Old)).

raw_replace2(record_field(RPos,Record,Field),Replaces,IntroducedIds,record_field(RPos,NRecord,NField)) :- !,
    raw_replace2(Record,Replaces,IntroducedIds,NRecord),
    (Field=identifier(_,FieldName),
    raw_replace2(Field,Replaces,IntroducedIds,NField)
    -> (NField=identifier(_,NewFieldName)
    -> (NewFieldName=FieldName -> true
    ; ajoin(['Rewriting field name ',FieldName,' during definition expansion to: '],Msg),
    add_message(definition_rewrite,Msg,NewFieldName,RPos)
    )
    ; translate_raw_bexpr_with_limit(NField,50,FS),
    ajoin(['Rewriting field name ',FieldName,' to an illegal expression: '],Msg),
    (try_get_raw_position_info(NField,NFPos) -> true ; NFPos=RPos),
    add_warning(definition_rewrite,Msg,FS,NFPos)
    )
    ; NField=Field).

raw_replace2(multiline_template(Pos,TS),Replaces,Ids,New) :- !, % rewrite template, it may contain expressions with ids
    transform_string_template(TS,Pos,RawExpr),
    raw_replace2(RawExpr,Replaces,Ids,New).

raw_replace2(Expr,_,IntroducedIds,_) :-
    quantifier_capture_warning(Expr,IntroducedIds),
    fail.

raw_replace2(X,_Replaces,_,Res) :- simple_expr(X), !,Res=X.

raw_replace2(Expr,Replaces,IntroducedIds,New) :-
    safe_functor(raw_replace2_expr,Expr,Functor,Arity),
    safe_functor(raw_replace2_new,New,Functor,Arity),
    raw_replace3(Arity,Expr,Replaces,IntroducedIds,New).

raw_replace3(0,_,_,_,_) :- !.

raw_replace3(N,Expr,Replaces,IntroducedIds,NExpr) :-
    arg(N,Expr,Old),
    arg(N,NExpr,New),
    raw_replace2(Old,Replaces,IntroducedIds,New),
    N2 is N-1,
    raw_replace3(N2,Expr,Replaces,IntroducedIds,NExpr).

raw_replace_id_list([],_,_,[]).

raw_replace_id_list([identifier(Pos,Old)|T],Replaces,Intro,Res) :- !,
    (memberchk(replace(Old,New),Replaces)
    -> (flatten_couple_id_list(New,Res,Tail) -> NT=Tail
    ; ajoin(['Rewriting identifier ',Old,' to an illegal value during definition expansion: '],Msg),
    add_warning(definition_rewrite,Msg,New,Pos),
    Res = [New|NT]
    )
    ; Res=[identifier(Pos,Old)|NT]
    ), raw_replace_id_list(T,Replaces,Intro,NT).

raw_replace_id_list([H|T],Replaces,Intro,[H|NT]) :-
    arg(1,H,Pos),
    add_warning(definition_rewrite,'Not an identifier in raw AST: ',H,Pos), % should not happen
    raw_replace_id_list(T,Replaces,Intro,NT).

raw_syntax_traversion(definitions(Pos,List),defs(Pos),List). % definitions section

raw_syntax_traversion(expression_definition(Pos,Name,Paras,Body),expression_definition(Pos,Name),[Body|Paras]).

raw_syntax_traversion(conjunct(Pos,List),con(Pos),List). % n-ary conjunct

raw_syntax_traversion(disjunct(Pos,List),disj(Pos),List). % n-ary disjunct

raw_syntax_traversion(comprehension_set(Pos,Ids,Body),cs(Pos,Ids),[Body]).

raw_syntax_traversion(lambda(Pos,Ids,Pred,Expr),lm(Pos,Ids),[Pred,Expr]).

raw_syntax_traversion(symbolic_comprehension_set(Pos,Ids,Body),sc(Pos,Ids),[Body]).

raw_syntax_traversion(symbolic_event_b_comprehension_set(Pos,Ids,Pred,Body),sc(Pos,Ids),[Pred,Body]).

raw_syntax_traversion(symbolic_lambda(Pos,Ids,Pred,Expr),symlam(Pos,Ids),[Pred,Expr]).

raw_syntax_traversion(function(Pos,Fun,List),fun(Pos),[Fun|List]). % function call

raw_syntax_traversion(sequence_extension(Pos,List),sqext(Pos),List).

raw_syntax_traversion(set_extension(Pos,List),sext(Pos),List).

raw_syntax_traversion(definition(Pos,Name,ParaList),defcall(Pos,Name),ParaList).

raw_syntax_traversion(rec(Pos,List),rec(Pos),List). % n-ary conjunct

raw_update_file_nrs(RawExpr,NewNrs,NewRawExpr) :-
    map_over_raw_expr(RawExpr,raw_update_file_nrs3(NewNrs),NewRawExpr).

raw_update_file_nrs3(NewNrs,OldRaw,NewRaw) :-
    update_raw_position_info(OldRaw,Pos,UpdatedRaw,NewPos),
    update_position_filenumber(Pos,OldNr,NewPos,NewNr),
    (nth1(OldNr,NewNrs,NewNr) -> true ; write(unknown_file_nr(OldNr)),nl,fail),
    !,
    recur_over_raw_expr(UpdatedRaw,raw_update_file_nrs3(NewNrs),NewRaw).

raw_update_file_nrs3(NewNrs,OldRaw,NewRaw) :-
    recur_over_raw_expr(OldRaw,raw_update_file_nrs3(NewNrs),NewRaw).

recur_over_raw_expr([A|T],P,[MA|MT]) :- !,
    map_over_raw_expr(A,P,MA),
    map_over_raw_expr(T,P,MT).

recur_over_raw_expr(conjunct(Pos,A,B),P,conjunct(Pos,MA,MB)) :- !,
    map_over_raw_expr(A,P,MA),
    map_over_raw_expr(B,P,MB).

recur_over_raw_expr(disjunct(Pos,A,B),P,disjunct(Pos,MA,MB)) :- !,
    map_over_raw_expr(A,P,MA),
    map_over_raw_expr(B,P,MB).

recur_over_raw_expr(equal(Pos,A,B),P,equal(Pos,MA,MB)) :- !,
    map_over_raw_expr(A,P,MA),
    map_over_raw_expr(B,P,MB).

recur_over_raw_expr(A,_,R) :- atomic(A),!,R=A.

recur_over_raw_expr(A,P,R) :- raw_syntax_traversion(A,Fixed,Args),!,
    functor(A,F,N), functor(R,F,N),
    raw_syntax_traversion(R,Fixed,NewArgs),
    maplist(map_over(P),Args,NewArgs).

recur_over_raw_expr(F,P,MF) :- F =.. [Functor,Pos|Args], % default: arg1 is position, rest is sub-arguments
    maplist(map_over(P),Args,NewArgs),
    MF =.. [Functor,Pos|NewArgs].

remove_raw_position_info([],Output) :- !,Output=[].

remove_raw_position_info([I|Irest],[O|Orest]) :-
    !,remove_raw_position_info(I,O),
    remove_raw_position_info(Irest,Orest).

remove_raw_position_info(Input,Output) :-
    compound(Input),functor(Input,Functor,Arity),Arity>0,!,
    Arity2 is Arity-1,
    functor(Output,Functor,Arity2),
    remove_raw_position_info2(1,Arity,Input,Output).

remove_raw_position_info(Input,Input).

remove_raw_position_info2(Pos,Arity,Input,Output) :-
    Pos < Arity,!,Pos2 is Pos+1,
    arg(Pos2,Input,IA), arg(Pos,Output,OA),
    remove_raw_position_info(IA,OA),
    remove_raw_position_info2(Pos2,Arity,Input,Output).

remove_raw_position_info2(_Pos,_Arity,_Input,_Output).

simple_expr(real(_,_)).

simple_expr(string(_,_)).

simple_expr(integer(_,_)).

try_get_raw_position_info(Compound,Info) :-
    compound(Compound),
    functor(Compound,_,Arity), Arity>0,
    arg(1,Compound,Info).

update_raw_position_info(Compound,Pos,NewCompound,NewPos) :-
    compound(Compound),
    Compound =.. [Functor,Pos|Rest],
    NewCompound =.. [Functor,NewPos|Rest].