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
|
(* test copied from ocaml's fragile_matching.ml test as of ocaml b02c7ca08 *)
Require Import Ltac2.Ltac2.
(* Tests for stack-overflow crashes caused by a combinatorial
explosition in fragile pattern checking. *)
Module SyntheticTest.
Ltac2 Type t := [ A | B ].
Ltac2 f x :=
match x with
| A,A,A,A,A, A,A,A,A,A, A,A,A,A,A, A,A,A => 1
| (A|B),(A|B),(A|B),(A|B),(A|B),
(A|B),(A|B),(A|B),(A|B),(A|B),
(A|B),(A|B),(A|B),(A|B),(A|B),
(A|B),(A|B),(A|B) => 2
end.
End SyntheticTest.
Module RealCodeTest.
(* from Alex Fedoseev *)
Ltac2 Type ('a,'b) result := [ Ok ('a) | Err ('b) ].
Ltac2 Type visibility := [Shown | Hidden].
Ltac2 Type ('outputValue, 'message) fieldStatus :=
[ Pristine
| Dirty (('outputValue, 'message) result, visibility) ].
Ltac2 Type message := string.
Ltac2 Type rec fieldsStatuses := {
iaasStorageConfigurations :
iaasStorageConfigurationFieldsStatuses array;
}
with iaasStorageConfigurationFieldsStatuses := {
startDate : (int, message) fieldStatus;
term : (int, message) fieldStatus;
rawStorageCapacity : (int, message) fieldStatus;
diskType : (string option, message) fieldStatus;
connectivityMethod : (string option, message) fieldStatus;
getRequest : (int option, message) fieldStatus;
getRequestUnit : (string option, message) fieldStatus;
putRequest : (int option, message) fieldStatus;
putRequestUnit : (string option, message) fieldStatus;
transferOut : (int option, message) fieldStatus;
transferOutUnit : (string option, message) fieldStatus;
region : (string option, message) fieldStatus;
cloudType : (string option, message) fieldStatus;
description : (string option, message) fieldStatus;
features : (string array, message) fieldStatus;
accessTypes : (string array, message) fieldStatus;
certifications : (string array, message) fieldStatus;
additionalRequirements : (string option, message) fieldStatus;
}.
Ltac2 Type interface := { dirty : unit -> bool }.
Ltac2 useForm () := {
dirty := fun () =>
Array.for_all
(fun item =>
match item with
| {
additionalRequirements := Pristine;
certifications := Pristine;
accessTypes := Pristine;
features := Pristine;
description := Pristine;
cloudType := Pristine;
region := Pristine;
transferOutUnit := Pristine;
transferOut := Pristine;
putRequestUnit := Pristine;
putRequest := Pristine;
getRequestUnit := Pristine;
getRequest := Pristine;
connectivityMethod := Pristine;
diskType := Pristine;
rawStorageCapacity := Pristine;
term := Pristine;
startDate := Pristine;
} =>
false
| {
additionalRequirements := Pristine | Dirty _ _;
certifications := Pristine | Dirty _ _;
accessTypes := Pristine | Dirty _ _;
features := Pristine | Dirty _ _;
description := Pristine | Dirty _ _;
cloudType := Pristine | Dirty _ _;
region := Pristine | Dirty _ _;
transferOutUnit := Pristine | Dirty _ _;
transferOut := Pristine | Dirty _ _;
putRequestUnit := Pristine | Dirty _ _;
putRequest := Pristine | Dirty _ _;
getRequestUnit := Pristine | Dirty _ _;
getRequest := Pristine | Dirty _ _;
connectivityMethod := Pristine | Dirty _ _;
diskType := Pristine | Dirty _ _;
rawStorageCapacity := Pristine | Dirty _ _;
term := Pristine | Dirty _ _;
startDate := Pristine | Dirty _ _;
} =>
true
end)
Array.empty
}.
End RealCodeTest.
|
