@@ -9,7 +9,7 @@ private signature class TypeWithToString {
99}
1010
1111/** A type with `toString` and `hasLocationInfo` */
12- private signature class TypeWithToStringAndLocation {
12+ private signature class TypeWithLocationInfo {
1313 bindingset [ this ]
1414 string toString ( ) ;
1515
@@ -59,8 +59,9 @@ module Option<TypeWithToString T> {
5959/**
6060 * Constructs an `Option` type that is a disjoint union of the given type and an
6161 * additional singleton element, and has a `hasLocationInfo` predicate.
62+ * `T` must have a `hasLocationInfo` predicate.
6263 */
63- module LocOption< TypeWithToStringAndLocation T> {
64+ module LocOption< TypeWithLocationInfo T> {
6465 private module O = Option< T > ;
6566
6667 final private class BOption = O:: Option ;
@@ -104,3 +105,64 @@ module LocOption<TypeWithToStringAndLocation T> {
104105 /** Gets the given element wrapped as an `Option`. */
105106 Some some ( T c ) { result = O:: some ( c ) }
106107}
108+
109+ private module GetLocationType< TypeWithLocationInfo Location> {
110+ signature class TypeWithGetLocation {
111+ bindingset [ this ]
112+ string toString ( ) ;
113+
114+ Location getLocation ( ) ;
115+ }
116+ }
117+
118+ /**
119+ * Constructs an `Option` type that is a disjoint union of the given type and an
120+ * additional singleton element, and has a `hasLocationInfo` predicate.
121+ * `T` must have a `getLocation` predicate with a result type of `Location`.
122+ */
123+ module LocOption2< TypeWithLocationInfo Location, GetLocationType< Location > :: TypeWithGetLocation T> {
124+ private module O = Option< T > ;
125+
126+ final private class BOption = O:: Option ;
127+
128+ final private class BNone = O:: None ;
129+
130+ final private class BSome = O:: Some ;
131+
132+ /**
133+ * An option type. This is either a singleton `None` or a `Some` wrapping the
134+ * given type.
135+ */
136+ class Option extends BOption {
137+ /**
138+ * Holds if this element is at the specified location.
139+ * The location spans column `startColumn` of line `startLine` to
140+ * column `endColumn` of line `endLine` in file `filepath`.
141+ * For more information, see
142+ * [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
143+ */
144+ predicate hasLocationInfo (
145+ string filePath , int startLine , int startColumn , int endLine , int endColumn
146+ ) {
147+ this .isNone ( ) and
148+ filePath = "" and
149+ startLine = 0 and
150+ startColumn = 0 and
151+ endLine = 0 and
152+ endColumn = 0
153+ or
154+ this .asSome ( )
155+ .getLocation ( )
156+ .hasLocationInfo ( filePath , startLine , startColumn , endLine , endColumn )
157+ }
158+ }
159+
160+ /** The singleton `None` element. */
161+ class None extends BNone , Option { }
162+
163+ /** A wrapper for the given type. */
164+ class Some extends BSome , Option { }
165+
166+ /** Gets the given element wrapped as an `Option`. */
167+ Some some ( T c ) { result = O:: some ( c ) }
168+ }
0 commit comments