tools_positions

add_col_offset_to_position(Span,0,R) :- !, R=Span.

add_col_offset_to_position(p3(Line,Scol,Ecol),Offset,p3(Line,S2,E2)) :- !,
    S2 is Scol+Offset, E2 is Ecol+Offset.

add_col_offset_to_position(p4(File,Line,Scol,Ecol),Offset,p4(File,Line,S2,E2)) :- !,
    S2 is Scol+Offset, E2 is Ecol+Offset.

add_col_offset_to_position(p5(FN,Srow,Scol,Srow,Ecol),Offset,p4(FN,Srow,S2,E2)) :- !,
    S2 is Scol+Offset, E2 is Ecol+Offset.

add_col_offset_to_position(p5(FN,Srow,Scol,Erow,Ecol),Offset,p5(FN,Srow,S2,Erow,Ecol)) :- !,
    S2 is Scol+Offset.

add_col_offset_to_position(pos(BC,FN,Srow,Scol,Srow,Ecol),Offset,pos(BC,FN,Srow,S2,Srow,E2)) :- !,
    S2 is Scol+Offset, E2 is Ecol+Offset.

add_col_offset_to_position(pos(BC,FN,Srow,Scol,Erow,Ecol),Offset,pos(BC,FN,Srow,S2,Erow,Ecol)) :- !,
    S2 is Scol+Offset.

add_col_offset_to_position(pos_context(Span,C,S2),Offset,pos_context(Res,C,S2)) :- !,
    add_col_offset_to_position(Span,Offset,Res).

add_col_offset_to_position(Span,_,Res) :- is_position(Span),!,Res=Span.

add_col_offset_to_position(Span,Offset,Span) :- write(cannot_add_offset_to_unknown_span(Offset,Span)),nl.

add_line_col_offset_to_position(Span,0,C,R) :- !, add_col_offset_to_position(Span,C,R).

add_line_col_offset_to_position(p3(Line,Scol,Ecol),LineOffset,ColOffset,p3(L2,S2,E2)) :- !,
    L2 is Line+LineOffset, S2 is ColOffset+1, % column numbers start at 1
    E2 is Ecol-Scol+ColOffset.

add_line_col_offset_to_position(p4(File,Line,Scol,Ecol),LineOffset,ColOffset,p4(File,L2,S2,E2)) :- !,
    L2 is Line+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1.

add_line_col_offset_to_position(p5(FN,Srow,Scol,Srow,Ecol),LineOffset,ColOffset,p4(FN,L2,S2,E2)) :- !,
    L2 is Srow+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1.

add_line_col_offset_to_position(p5(FN,Srow,_Scol,Erow,Ecol),LineOffset,ColOffset,p5(FN,SL2,S2,EL2,Ecol)) :- !,
    SL2 is Srow+LineOffset, EL2 is Erow+LineOffset, S2 is ColOffset+1.

add_line_col_offset_to_position(pos(BC,FN,Srow,Scol,Srow,Ecol),LineOffset,ColOffset,pos(BC,FN,L2,S2,L2,E2)) :- !,
    L2 is Srow+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1.

add_line_col_offset_to_position(pos(BC,FN,Srow,_Scol,Erow,Ecol),LineOffset,ColOffset,pos(BC,FN,SL2,S2,EL2,Ecol)) :- !,
    SL2 is Srow+LineOffset, EL2 is Erow+LineOffset, S2 is ColOffset+1.

add_line_col_offset_to_position(pos_context(Span,C,S2),LineOffset,ColOffset,pos_context(Res,C,S2)) :- !,
    add_line_col_offset_to_position(Span,LineOffset,ColOffset,Res).

add_line_col_offset_to_position(Span,_,_,Res) :- is_position(Span),!,Res=Span.

add_line_col_offset_to_position(Span,LineOffset,ColOffset,Span) :-
    write(cannot_add_offset_to_unknown_span(LineOffset,ColOffset,Span)),nl.

get_position_filenumber(pos(_,FN,_Srow,_Scol,_Erow,_Ecol),FN).

get_position_filenumber(p5(FN,_Srow,_Scol,_Erow,_Ecol),FN).

get_position_filenumber(p4(FN,_Srow,_Scol,_Ecol),FN).

get_position_filenumber(p3(_Srow,_Scol,_Ecol),1).

get_position_row_cols(pos(_,_FN,Srow,Scol,Erow,Ecol),Srow,Scol,Erow,Ecol).

get_position_row_cols(p5(_FN,Srow,Scol,Erow,Ecol),Srow,Scol,Erow,Ecol).

get_position_row_cols(p4(_FN,Srow,Scol,Ecol),Srow,Scol,Srow,Ecol).

get_position_row_cols(p3(Srow,Scol,Ecol),Srow,Scol,Srow,Ecol).

is_position(none).

is_position(pos(_,_,_,_,_,_)). % old pos/6 format with unused ID

is_position(p5(_,_,_,_,_)). % new format without ID

is_position(p4(_,_,_,_)). % new format without ID and for end line = start line

is_position(p3(_,_,_)). % new format without ID and for file number 1 and with end line = start line

is_position(rodinpos(_Model,_Name,_Internal)). % created by Event-B export

is_position(rodinpos(_,_)). % old style positions, e.g., for test 362

is_position(pos_context(_,_,_)). % created by combine_pos; not generated by B parser

is_valid_position(none).

is_valid_position(pos(Id,F,SL,SC,EL,EC)) :-
    number(Id),atomic(F),number(SL),number(SC),number(EL),number(EC).

is_valid_position(p5(F,SL,SC,EL,EC)) :-
    atomic(F),number(SL),number(SC),number(EL),number(EC).

is_valid_position(p4(File,SL,SC,EC)) :-
    atomic(File),number(SL),number(SC),number(EC).

is_valid_position(p3(SL,SC,EC)) :-
    number(SL),number(SC),number(EC).

is_valid_position(pos_context(P1,_Ctxt,P2)) :-
    is_valid_position(P1), is_valid_position(P2).

row_col_to_position(Row,Col,p3(Row,Col,Col)).

update_position_filenumber(pos(A,OldFN,Srow,Scol,Erow,Ecol),OldFN,
    pos(A,NewFN,Srow,Scol,Erow,Ecol),NewFN).

update_position_filenumber(p5(OldFN,Srow,Scol,Erow,Ecol),OldFN,
    p5(NewFN,Srow,Scol,Erow,Ecol),NewFN).

update_position_filenumber(p4(OldFN,Srow,Scol,Ecol),OldFN,
    p4(NewFN,Srow,Scol,Ecol),NewFN).

update_position_filenumber(p3(Srow,Scol,Ecol),1,
    p4(NewFN,Srow,Scol,Ecol),NewFN).