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. |