Skip to content

Commit d9b1c13

Browse files
msprotzmsprotz
authored
Merge branch 'master' into protz-Small-helper
2 parents 0d27005 + 4af7e13 commit d9b1c13

30 files changed

+1335
-455
lines changed

‎krmllib/dist/generic/FStar_Attributes.c‎

Lines changed: 201 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,201 @@
1+
/*
2+
Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
3+
Licensed under the Apache 2.0 and MIT Licenses.
4+
*/
5+
6+
7+
#include "FStar_Attributes.h"
8+
9+
bool
10+
FStar_Attributes_uu___is_PpxDerivingShow(
11+
FStar_Attributes___internal_ocaml_attributes projectee
12+
)
13+
{
14+
if (projectee.tag == FStar_Attributes_PpxDerivingShow)
15+
{
16+
return true;
17+
}
18+
else
19+
{
20+
return false;
21+
}
22+
}
23+
24+
bool
25+
FStar_Attributes_uu___is_PpxDerivingShowConstant(
26+
FStar_Attributes___internal_ocaml_attributes projectee
27+
)
28+
{
29+
if (projectee.tag == FStar_Attributes_PpxDerivingShowConstant)
30+
{
31+
return true;
32+
}
33+
else
34+
{
35+
return false;
36+
}
37+
}
38+
39+
bool
40+
FStar_Attributes_uu___is_PpxDerivingYoJson(
41+
FStar_Attributes___internal_ocaml_attributes projectee
42+
)
43+
{
44+
if (projectee.tag == FStar_Attributes_PpxDerivingYoJson)
45+
{
46+
return true;
47+
}
48+
else
49+
{
50+
return false;
51+
}
52+
}
53+
54+
bool FStar_Attributes_uu___is_CInline(FStar_Attributes___internal_ocaml_attributes projectee)
55+
{
56+
if (projectee.tag == FStar_Attributes_CInline)
57+
{
58+
return true;
59+
}
60+
else
61+
{
62+
return false;
63+
}
64+
}
65+
66+
bool
67+
FStar_Attributes_uu___is_Substitute(FStar_Attributes___internal_ocaml_attributes projectee)
68+
{
69+
if (projectee.tag == FStar_Attributes_Substitute)
70+
{
71+
return true;
72+
}
73+
else
74+
{
75+
return false;
76+
}
77+
}
78+
79+
bool FStar_Attributes_uu___is_Gc(FStar_Attributes___internal_ocaml_attributes projectee)
80+
{
81+
if (projectee.tag == FStar_Attributes_Gc)
82+
{
83+
return true;
84+
}
85+
else
86+
{
87+
return false;
88+
}
89+
}
90+
91+
bool FStar_Attributes_uu___is_Comment(FStar_Attributes___internal_ocaml_attributes projectee)
92+
{
93+
if (projectee.tag == FStar_Attributes_Comment)
94+
{
95+
return true;
96+
}
97+
else
98+
{
99+
return false;
100+
}
101+
}
102+
103+
bool FStar_Attributes_uu___is_CPrologue(FStar_Attributes___internal_ocaml_attributes projectee)
104+
{
105+
if (projectee.tag == FStar_Attributes_CPrologue)
106+
{
107+
return true;
108+
}
109+
else
110+
{
111+
return false;
112+
}
113+
}
114+
115+
bool FStar_Attributes_uu___is_CEpilogue(FStar_Attributes___internal_ocaml_attributes projectee)
116+
{
117+
if (projectee.tag == FStar_Attributes_CEpilogue)
118+
{
119+
return true;
120+
}
121+
else
122+
{
123+
return false;
124+
}
125+
}
126+
127+
bool FStar_Attributes_uu___is_CConst(FStar_Attributes___internal_ocaml_attributes projectee)
128+
{
129+
if (projectee.tag == FStar_Attributes_CConst)
130+
{
131+
return true;
132+
}
133+
else
134+
{
135+
return false;
136+
}
137+
}
138+
139+
bool FStar_Attributes_uu___is_CCConv(FStar_Attributes___internal_ocaml_attributes projectee)
140+
{
141+
if (projectee.tag == FStar_Attributes_CCConv)
142+
{
143+
return true;
144+
}
145+
else
146+
{
147+
return false;
148+
}
149+
}
150+
151+
bool
152+
FStar_Attributes_uu___is_CAbstractStruct(
153+
FStar_Attributes___internal_ocaml_attributes projectee
154+
)
155+
{
156+
if (projectee.tag == FStar_Attributes_CAbstractStruct)
157+
{
158+
return true;
159+
}
160+
else
161+
{
162+
return false;
163+
}
164+
}
165+
166+
bool FStar_Attributes_uu___is_CIfDef(FStar_Attributes___internal_ocaml_attributes projectee)
167+
{
168+
if (projectee.tag == FStar_Attributes_CIfDef)
169+
{
170+
return true;
171+
}
172+
else
173+
{
174+
return false;
175+
}
176+
}
177+
178+
bool FStar_Attributes_uu___is_CMacro(FStar_Attributes___internal_ocaml_attributes projectee)
179+
{
180+
if (projectee.tag == FStar_Attributes_CMacro)
181+
{
182+
return true;
183+
}
184+
else
185+
{
186+
return false;
187+
}
188+
}
189+
190+
bool FStar_Attributes_uu___is_CNoInline(FStar_Attributes___internal_ocaml_attributes projectee)
191+
{
192+
if (projectee.tag == FStar_Attributes_CNoInline)
193+
{
194+
return true;
195+
}
196+
else
197+
{
198+
return false;
199+
}
200+
}
201+

‎krmllib/dist/generic/FStar_Attributes.h‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
/*
2+
Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
3+
Licensed under the Apache 2.0 and MIT Licenses.
4+
*/
5+
6+
7+
#ifndef __FStar_Attributes_H
8+
#define __FStar_Attributes_H
9+
10+
#include <inttypes.h>
11+
#include "krmllib.h"
12+
#include "krml/internal/compat.h"
13+
#include "krml/internal/target.h"
14+
15+
#define FStar_Attributes_PpxDerivingShow 0
16+
#define FStar_Attributes_PpxDerivingShowConstant 1
17+
#define FStar_Attributes_PpxDerivingYoJson 2
18+
#define FStar_Attributes_CInline 3
19+
#define FStar_Attributes_Substitute 4
20+
#define FStar_Attributes_Gc 5
21+
#define FStar_Attributes_Comment 6
22+
#define FStar_Attributes_CPrologue 7
23+
#define FStar_Attributes_CEpilogue 8
24+
#define FStar_Attributes_CConst 9
25+
#define FStar_Attributes_CCConv 10
26+
#define FStar_Attributes_CAbstractStruct 11
27+
#define FStar_Attributes_CIfDef 12
28+
#define FStar_Attributes_CMacro 13
29+
#define FStar_Attributes_CNoInline 14
30+
31+
typedef uint8_t FStar_Attributes___internal_ocaml_attributes_tags;
32+
33+
typedef struct FStar_Attributes___internal_ocaml_attributes_s
34+
{
35+
FStar_Attributes___internal_ocaml_attributes_tags tag;
36+
union {
37+
Prims_string case_PpxDerivingShowConstant;
38+
Prims_string case_Comment;
39+
Prims_string case_CPrologue;
40+
Prims_string case_CEpilogue;
41+
Prims_string case_CConst;
42+
Prims_string case_CCConv;
43+
}
44+
;
45+
}
46+
FStar_Attributes___internal_ocaml_attributes;
47+
48+
bool
49+
FStar_Attributes_uu___is_PpxDerivingShow(
50+
FStar_Attributes___internal_ocaml_attributes projectee
51+
);
52+
53+
bool
54+
FStar_Attributes_uu___is_PpxDerivingShowConstant(
55+
FStar_Attributes___internal_ocaml_attributes projectee
56+
);
57+
58+
bool
59+
FStar_Attributes_uu___is_PpxDerivingYoJson(
60+
FStar_Attributes___internal_ocaml_attributes projectee
61+
);
62+
63+
bool FStar_Attributes_uu___is_CInline(FStar_Attributes___internal_ocaml_attributes projectee);
64+
65+
bool
66+
FStar_Attributes_uu___is_Substitute(FStar_Attributes___internal_ocaml_attributes projectee);
67+
68+
bool FStar_Attributes_uu___is_Gc(FStar_Attributes___internal_ocaml_attributes projectee);
69+
70+
bool FStar_Attributes_uu___is_Comment(FStar_Attributes___internal_ocaml_attributes projectee);
71+
72+
bool
73+
FStar_Attributes_uu___is_CPrologue(FStar_Attributes___internal_ocaml_attributes projectee);
74+
75+
bool
76+
FStar_Attributes_uu___is_CEpilogue(FStar_Attributes___internal_ocaml_attributes projectee);
77+
78+
bool FStar_Attributes_uu___is_CConst(FStar_Attributes___internal_ocaml_attributes projectee);
79+
80+
bool FStar_Attributes_uu___is_CCConv(FStar_Attributes___internal_ocaml_attributes projectee);
81+
82+
bool
83+
FStar_Attributes_uu___is_CAbstractStruct(
84+
FStar_Attributes___internal_ocaml_attributes projectee
85+
);
86+
87+
bool FStar_Attributes_uu___is_CIfDef(FStar_Attributes___internal_ocaml_attributes projectee);
88+
89+
bool FStar_Attributes_uu___is_CMacro(FStar_Attributes___internal_ocaml_attributes projectee);
90+
91+
bool
92+
FStar_Attributes_uu___is_CNoInline(FStar_Attributes___internal_ocaml_attributes projectee);
93+
94+
95+
#define __FStar_Attributes_H_DEFINED
96+
#endif

‎krmllib/dist/generic/FStar_Int16.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ extern krml_checked_int_t FStar_Int16___proj__Mk__item__v(int16_t projectee);
2020

2121
extern krml_checked_int_t FStar_Int16_v(int16_t x);
2222

23+
typedef void *FStar_Int16_fits;
24+
2325
extern int16_t FStar_Int16_int_to_t(krml_checked_int_t x);
2426

2527
extern int16_t FStar_Int16_zero;

‎krmllib/dist/generic/FStar_Int32.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ extern krml_checked_int_t FStar_Int32___proj__Mk__item__v(int32_t projectee);
2020

2121
extern krml_checked_int_t FStar_Int32_v(int32_t x);
2222

23+
typedef void *FStar_Int32_fits;
24+
2325
extern int32_t FStar_Int32_int_to_t(krml_checked_int_t x);
2426

2527
extern int32_t FStar_Int32_zero;

‎krmllib/dist/generic/FStar_Int64.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ extern krml_checked_int_t FStar_Int64___proj__Mk__item__v(int64_t projectee);
2020

2121
extern krml_checked_int_t FStar_Int64_v(int64_t x);
2222

23+
typedef void *FStar_Int64_fits;
24+
2325
extern int64_t FStar_Int64_int_to_t(krml_checked_int_t x);
2426

2527
extern int64_t FStar_Int64_zero;

‎krmllib/dist/generic/FStar_Int8.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ extern krml_checked_int_t FStar_Int8___proj__Mk__item__v(int8_t projectee);
2020

2121
extern krml_checked_int_t FStar_Int8_v(int8_t x);
2222

23+
typedef void *FStar_Int8_fits;
24+
2325
extern int8_t FStar_Int8_int_to_t(krml_checked_int_t x);
2426

2527
extern int8_t FStar_Int8_zero;

‎krmllib/dist/generic/FStar_Issue.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,8 @@ FStar_Issue_range_of_issue(FStar_Issue_issue i);
4646

4747
extern Prims_list__Prims_string *FStar_Issue_context_of_issue(FStar_Issue_issue i);
4848

49+
extern FStar_Pprint_document FStar_Issue_issue_to_doc(FStar_Issue_issue i);
50+
4951
extern Prims_string FStar_Issue_render_issue(FStar_Issue_issue i);
5052

5153
extern FStar_Issue_issue

0 commit comments

Comments
 (0)