forked from anakrish/Rego-FStar
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRego.Ast.fsti
112 lines (92 loc) · 2.42 KB
/
Rego.Ast.fsti
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
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
module Rego.Ast
#push-options "--warn_error -331"
type binOp =
| And
| Or
and arithOp =
| Add
| Sub
| Mul
| Divv
| Mod
and boolOp =
| Lt
| Le
| Eq
| Ge
| Gt
| Ne
and assignOp =
| EqAssign (* Changed name to differentiate from Assign in boolOp *)
| ColEq
and ident = string
(* without eqtype annotation "Failed to solve universe inequalities for inductives" *)
and expr:eqtype =
| Value of Rego.Value.value
| Var of ident
| Array of (items:list expr)
| Set of (items:list expr)
| Object of (fields:list (expr * expr))
| ArrayCompr of query
| SetCompr of query
| ObjectCompr of query
| Call of (fcn:expr) * (params:list expr)
| UnaryExpr of expr
| RefDot of (refr:expr) * (field:string)
| RefBrack of (refr:expr) * (index:expr)
| BinExpr of binOp * (lhs:expr) * (rhs:expr)
| BoolExpr of boolOp * (lhs:expr) * (rhs:expr)
| ArithExpr of arithOp * (lhs:expr) * (rhs:expr)
| AssignExpr of assignOp * (lhs:expr) * (rhs:expr)
| MembershipExpr of (key:expr) * (value:expr) * (collection:expr)
and literal =
| SomeVars of (var:list ident)
| SomeIn of (key:option expr) * (value:expr) * (collection:expr)
| Expr of expr
| NotExpr of (a:expr)
| Every of (key:option ident) * (value:ident) * (domain:expr) * query
| ArrayComprOutput of (e:expr)
| SetComprOutput of (e:expr)
| ObjectComprOutput of (k:expr) * (v:expr)
and withModifier = {
refr: expr;
as_: expr;
}
and literalStmt = {
literal: literal;
with_mods: list withModifier;
}
and query = {
stmts: list literalStmt
}
and ruleAssign = {
op: assignOp;
value: expr;
}
and ruleBody = {
assign: option ruleAssign;
query: query;
}
and ruleHead =
| Compr of (refr:expr) * (assign: option ruleAssign)
| Set_ of (refr:expr) * (key:option expr)
| Func of (refr:expr) * (args:list expr) * (assign: option ruleAssign)
and rule =
| Spec of (head:ruleHead) * (bodies: list ruleBody)
| Default of (refr:expr) * (args:list expr) * (op:assignOp) * (value:expr)
and package = {
refr: expr;
}
and import = {
refr: expr;
as_: option ident;
}
and regoModule = {
package: package;
imports: list import;
policy: list rule;
rego_v1: bool;
}
#pop-options