FilesExpand file tree

master

/

PolymorphicDatatypeExample.java

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

138 lines (104 loc) · 5.28 KB

master

/

PolymorphicDatatypeExample.java

Copy path

Top

File metadata and controls

• Code
• Blame

138 lines (104 loc) · 5.28 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

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

/**

Copyright (c) 2024 Microsoft Corporation

Module Name:

PolymorphicDatatypeExample.java

Abstract:

Example demonstrating the use of polymorphic (parametric) datatypes in Z3's Java API.

This example creates a polymorphic List[T] datatype and demonstrates its usage.

Author:

GitHub Copilot 2024-01-30

Notes:

**/

import com.microsoft.z3.*;

public class PolymorphicDatatypeExample {

/**

* Create a polymorphic List[T] datatype.

* This is equivalent to:

* datatype List[T] = nil | cons(head: T, tail: List[T])

*/

static void polymorphicListExample(Context ctx) {

System.out.println("PolymorphicListExample");

// Create a type variable T

TypeVarSort T = ctx.mkTypeVariable("T");

// Create constructors for the List[T] datatype

// nil constructor (no arguments)

Constructor<Object> nil = ctx.mkConstructor("nil", "is_nil", null, null, null);

// cons constructor with head:T and tail:List[T]

String[] fieldNames = new String[] { "head", "tail" };

Sort[] fieldSorts = new Sort[] { T, null }; // null means recursive reference

int[] sortRefs = new int[] { 0, 0 }; // both refer to the datatype being defined

Constructor<Object> cons = ctx.mkConstructor("cons", "is_cons", fieldNames, fieldSorts, sortRefs);

// Create the polymorphic List[T] datatype

Constructor<Object>[] constructors = new Constructor[] { nil, cons };

DatatypeSort<Object> listSort = ctx.mkPolymorphicDatatypeSort("List", new Sort[]{T}, constructors);

System.out.println("Created polymorphic List datatype: " + listSort);

// Get the constructor and accessor functions

FuncDecl<?>[] listConstructors = listSort.getConstructors();

FuncDecl<?> nilDecl = listConstructors[0];

FuncDecl<?> consDecl = listConstructors[1];

System.out.println("nil constructor: " + nilDecl);

System.out.println("cons constructor: " + consDecl);

// Get accessors

FuncDecl<?>[][] accessors = listSort.getAccessors();

if (accessors.length > 1 && accessors[1].length == 2) {

FuncDecl<?> headAccessor = accessors[1][0];

FuncDecl<?> tailAccessor = accessors[1][1];

System.out.println("head accessor: " + headAccessor);

System.out.println("tail accessor: " + tailAccessor);

}

System.out.println("Polymorphic List example completed successfully!");

}

/**

* Create a polymorphic Option[T] datatype (like Maybe in Haskell).

* This is equivalent to:

* datatype Option[T] = none | some(value: T)

*/

static void polymorphicOptionExample(Context ctx) {

System.out.println("\nPolymorphicOptionExample");

// Create a type variable T

TypeVarSort T = ctx.mkTypeVariable("T");

// Create constructors for Option[T]

Constructor<Object> none = ctx.mkConstructor("none", "is_none", null, null, null);

String[] fieldNames = new String[] { "value" };

Sort[] fieldSorts = new Sort[] { T };

int[] sortRefs = new int[] { 0 }; // not used since T is not recursive

Constructor<Object> some = ctx.mkConstructor("some", "is_some", fieldNames, fieldSorts, sortRefs);

// Create the polymorphic Option[T] datatype

Constructor<Object>[] constructors = new Constructor[] { none, some };

DatatypeSort<Object> optionSort = ctx.mkPolymorphicDatatypeSort("Option", new Sort[]{T}, constructors);

System.out.println("Created polymorphic Option datatype: " + optionSort);

FuncDecl<?>[] optionConstructors = optionSort.getConstructors();

System.out.println("none constructor: " + optionConstructors[0]);

System.out.println("some constructor: " + optionConstructors[1]);

System.out.println("Polymorphic Option example completed successfully!");

}

/**

* Demonstrate type variables can be created with different names

*/

static void typeVariableExample(Context ctx) {

System.out.println("\nTypeVariableExample");

TypeVarSort T = ctx.mkTypeVariable("T");

TypeVarSort U = ctx.mkTypeVariable("U");

TypeVarSort V = ctx.mkTypeVariable("V");

System.out.println("Created type variable T: " + T);

System.out.println("Created type variable U: " + U);

System.out.println("Created type variable V: " + V);

// Type variables can be used as sort parameters

System.out.println("Type variables can be used as parameters for polymorphic datatypes");

}

public static void main(String[] args) {

try {

// Use try-with-resources to ensure proper cleanup

try (Context ctx = new Context()) {

typeVariableExample(ctx);

polymorphicListExample(ctx);

polymorphicOptionExample(ctx);

System.out.println("\n=== All polymorphic datatype examples completed successfully! ===");

}

} catch (Exception e) {

System.err.println("Error: " + e.getMessage());

e.printStackTrace();

System.exit(1);

}

}

}