| 1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | ||
| 6 | :- module(tools_positions, | |
| 7 | [is_position/1, | |
| 8 | is_valid_position/1, | |
| 9 | get_position_filenumber/2, | |
| 10 | get_position_row_cols/5, | |
| 11 | row_col_to_position/3, | |
| 12 | add_col_offset_to_position/3, | |
| 13 | add_line_col_offset_to_position/4 | |
| 14 | ]). | |
| 15 | ||
| 16 | :- use_module(module_information). | |
| 17 | ||
| 18 | :- module_info(group,infrastructure). | |
| 19 | :- module_info(description,'A few utilities on raw positions as provided by the B Parser.'). | |
| 20 | ||
| 21 | is_position(none). | |
| 22 | is_position(pos(_,_,_,_,_,_)). % old pos/6 format with unused ID | |
| 23 | is_position(p5(_,_,_,_,_)). % new format without ID | |
| 24 | is_position(p4(_,_,_,_)). % new format without ID and for end line = start line | |
| 25 | is_position(p3(_,_,_)). % new format without ID and for file number 1 and with end line = start line | |
| 26 | is_position(rodinpos(_Model,_Name,_Internal)). % created by Event-B export | |
| 27 | is_position(rodinpos(_,_)). % old style positions, e.g., for test 362 | |
| 28 | is_position(pos_context(_,_,_)). % created by combine_pos; not generated by B parser | |
| 29 | ||
| 30 | % same but with more stringent checks | |
| 31 | is_valid_position(none). | |
| 32 | is_valid_position(pos(Id,F,SL,SC,EL,EC)) :- | |
| 33 | number(Id),atomic(F),number(SL),number(SC),number(EL),number(EC). | |
| 34 | is_valid_position(p5(F,SL,SC,EL,EC)) :- | |
| 35 | atomic(F),number(SL),number(SC),number(EL),number(EC). | |
| 36 | is_valid_position(p4(File,SL,SC,EC)) :- | |
| 37 | atomic(File),number(SL),number(SC),number(EC). | |
| 38 | is_valid_position(p3(SL,SC,EC)) :- | |
| 39 | number(SL),number(SC),number(EC). | |
| 40 | is_valid_position(pos_context(P1,_Ctxt,P2)) :- | |
| 41 | is_valid_position(P1), is_valid_position(P2). | |
| 42 | ||
| 43 | get_position_filenumber(pos(_,FN,_Srow,_Scol,_Erow,_Ecol),FN). | |
| 44 | get_position_filenumber(p5(FN,_Srow,_Scol,_Erow,_Ecol),FN). | |
| 45 | get_position_filenumber(p4(FN,_Srow,_Scol,_Ecol),FN). | |
| 46 | get_position_filenumber(p3(_Srow,_Scol,_Ecol),1). | |
| 47 | ||
| 48 | % get start and end row/column information: | |
| 49 | get_position_row_cols(pos(_,_FN,Srow,Scol,Erow,Ecol),Srow,Scol,Erow,Ecol). | |
| 50 | get_position_row_cols(p5(_FN,Srow,Scol,Erow,Ecol),Srow,Scol,Erow,Ecol). | |
| 51 | get_position_row_cols(p4(_FN,Srow,Scol,Ecol),Srow,Scol,Srow,Ecol). | |
| 52 | get_position_row_cols(p3(Srow,Scol,Ecol),Srow,Scol,Srow,Ecol). | |
| 53 | ||
| 54 | % construct position in main file (number 1) | |
| 55 | row_col_to_position(Row,Col,p3(Row,Col,Col)). | |
| 56 | ||
| 57 | % add column offset to position: | |
| 58 | add_col_offset_to_position(Span,0,R) :- !, R=Span. | |
| 59 | add_col_offset_to_position(p3(Line,Scol,Ecol),Offset,p3(Line,S2,E2)) :- !, | |
| 60 | S2 is Scol+Offset, E2 is Ecol+Offset. | |
| 61 | add_col_offset_to_position(p4(File,Line,Scol,Ecol),Offset,p4(File,Line,S2,E2)) :- !, | |
| 62 | S2 is Scol+Offset, E2 is Ecol+Offset. | |
| 63 | add_col_offset_to_position(p5(FN,Srow,Scol,Srow,Ecol),Offset,p4(FN,Srow,S2,E2)) :- !, | |
| 64 | S2 is Scol+Offset, E2 is Ecol+Offset. | |
| 65 | add_col_offset_to_position(p5(FN,Srow,Scol,Erow,Ecol),Offset,p5(FN,Srow,S2,Erow,Ecol)) :- !, | |
| 66 | S2 is Scol+Offset. | |
| 67 | add_col_offset_to_position(pos(BC,FN,Srow,Scol,Srow,Ecol),Offset,pos(BC,FN,Srow,S2,Srow,E2)) :- !, | |
| 68 | S2 is Scol+Offset, E2 is Ecol+Offset. | |
| 69 | add_col_offset_to_position(pos(BC,FN,Srow,Scol,Erow,Ecol),Offset,pos(BC,FN,Srow,S2,Erow,Ecol)) :- !, | |
| 70 | S2 is Scol+Offset. | |
| 71 | add_col_offset_to_position(pos_context(Span,C,S2),Offset,pos_context(Res,C,S2)) :- !, | |
| 72 | add_col_offset_to_position(Span,Offset,Res). | |
| 73 | add_col_offset_to_position(Span,_,Res) :- is_position(Span),!,Res=Span. | |
| 74 | add_col_offset_to_position(Span,Offset,Span) :- write(cannot_add_offset_to_unknown_span(Offset,Span)),nl. | |
| 75 | ||
| 76 | ||
| 77 | % add line and column offset to position: | |
| 78 | add_line_col_offset_to_position(Span,0,C,R) :- !, add_col_offset_to_position(Span,C,R). | |
| 79 | add_line_col_offset_to_position(p3(Line,Scol,Ecol),LineOffset,ColOffset,p3(L2,S2,E2)) :- !, | |
| 80 | L2 is Line+LineOffset, S2 is ColOffset+1, % column numbers start at 1 | |
| 81 | E2 is Ecol-Scol+ColOffset. | |
| 82 | add_line_col_offset_to_position(p4(File,Line,Scol,Ecol),LineOffset,ColOffset,p4(File,L2,S2,E2)) :- !, | |
| 83 | L2 is Line+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1. | |
| 84 | add_line_col_offset_to_position(p5(FN,Srow,Scol,Srow,Ecol),LineOffset,ColOffset,p4(FN,L2,S2,E2)) :- !, | |
| 85 | L2 is Srow+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1. | |
| 86 | add_line_col_offset_to_position(p5(FN,Srow,_Scol,Erow,Ecol),LineOffset,ColOffset,p5(FN,SL2,S2,EL2,Ecol)) :- !, | |
| 87 | SL2 is Srow+LineOffset, EL2 is Erow+LineOffset, S2 is ColOffset+1. | |
| 88 | add_line_col_offset_to_position(pos(BC,FN,Srow,Scol,Srow,Ecol),LineOffset,ColOffset,pos(BC,FN,L2,S2,L2,E2)) :- !, | |
| 89 | L2 is Srow+LineOffset, S2 is ColOffset+1, E2 is Ecol-Scol+ColOffset+1. | |
| 90 | add_line_col_offset_to_position(pos(BC,FN,Srow,_Scol,Erow,Ecol),LineOffset,ColOffset,pos(BC,FN,SL2,S2,EL2,Ecol)) :- !, | |
| 91 | SL2 is Srow+LineOffset, EL2 is Erow+LineOffset, S2 is ColOffset+1. | |
| 92 | add_line_col_offset_to_position(pos_context(Span,C,S2),LineOffset,ColOffset,pos_context(Res,C,S2)) :- !, | |
| 93 | add_line_col_offset_to_position(Span,LineOffset,ColOffset,Res). | |
| 94 | add_line_col_offset_to_position(Span,_,_,Res) :- is_position(Span),!,Res=Span. | |
| 95 | add_line_col_offset_to_position(Span,LineOffset,ColOffset,Span) :- | |
| 96 | write(cannot_add_offset_to_unknown_span(LineOffset,ColOffset,Span)),nl. |