FilesExpand file tree

main

/

Option.qll

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

47 lines (39 loc) · 1.19 KB

main

/

Option.qll

Copy path

Top

File metadata and controls

• Code
• Blame

47 lines (39 loc) · 1.19 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

/** Provides a module for constructing optional versions of types. */

overlay[local?]

module;

/** A type with `toString`. */

private signature class TypeWithToString {

bindingset[this]

string toString();

}

/**

* Constructs an `Option` type that is a disjoint union of the given type and an

* additional singleton element.

*/

module Option<TypeWithToString T> {

private newtype TOption =

TNone() or

TSome(T c)

/**

* An option type. This is either a singleton `None` or a `Some` wrapping the

* given type.

*/

class Option extends TOption {

/** Gets a textual representation of this element. */

string toString() {

this = TNone() and result = "(none)"

or

exists(T c | this = TSome(c) and result = c.toString())

}

/** Gets the wrapped element, if any. */

T asSome() { this = TSome(result) }

/** Holds if this option is the singleton `None`. */

predicate isNone() { this = TNone() }

}

/** The singleton `None` element. */

class None extends Option, TNone { }

/** A wrapper for the given type. */

class Some extends Option, TSome { }

/** Gets the given element wrapped as an `Option`. */

Some some(T c) { result = TSome(c) }

}